diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-06-22 23:04:59 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-06-22 23:04:59 -0700 |
commit | da65e88e3b346bcd70198b980e918ea9f1e11b4e (patch) | |
tree | ce660cd8d798ddd41787322db32e6ae21b2ceb11 /src/aig/dch | |
parent | 270f6db24625e4838dcafe7d45e69cc9522d703e (diff) | |
download | abc-da65e88e3b346bcd70198b980e918ea9f1e11b4e.tar.gz abc-da65e88e3b346bcd70198b980e918ea9f1e11b4e.tar.bz2 abc-da65e88e3b346bcd70198b980e918ea9f1e11b4e.zip |
Version abc90804
committer: Baruch Sterin <baruchs@gmail.com>
Diffstat (limited to 'src/aig/dch')
-rw-r--r-- | src/aig/dch/dch.h | 2 | ||||
-rw-r--r-- | src/aig/dch/dchCore.c | 34 |
2 files changed, 34 insertions, 2 deletions
diff --git a/src/aig/dch/dch.h b/src/aig/dch/dch.h index 38978164..7271d256 100644 --- a/src/aig/dch/dch.h +++ b/src/aig/dch/dch.h @@ -68,7 +68,7 @@ struct Dch_Pars_t_ /*=== dchCore.c ==========================================================*/ extern void Dch_ManSetDefaultParams( Dch_Pars_t * p ); extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars ); - +extern void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars ); #ifdef __cplusplus } diff --git a/src/aig/dch/dchCore.c b/src/aig/dch/dchCore.c index 4a8d8b53..d38d5668 100644 --- a/src/aig/dch/dchCore.c +++ b/src/aig/dch/dchCore.c @@ -90,7 +90,7 @@ p->timeTotal = clock() - clkTotal; ABC_FREE( pAig->pTable ); pResult = Dch_DeriveChoiceAig( pAig ); // count the number of representatives - if ( pPars->fVerbose ) + if ( pPars->fVerbose ) printf( "STATS: Reprs = %6d. Equivs = %6d. Choices = %6d.\n", Dch_DeriveChoiceCountReprs( pAig ), Dch_DeriveChoiceCountEquivs( pResult ), @@ -98,6 +98,38 @@ p->timeTotal = clock() - clkTotal; return pResult; } +/**Function************************************************************* + + Synopsis [Performs computation of AIGs with choices.] + + Description [Takes several AIGs and performs choicing.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars ) +{ + Dch_Man_t * p; + int clk, clkTotal = clock(); + // reset random numbers + Aig_ManRandom(1); + // start the choicing manager + p = Dch_ManCreate( pAig, pPars ); + // compute candidate equivalence classes +clk = clock(); + p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose ); +p->timeSimInit = clock() - clk; +// Dch_ClassesPrint( p->ppClasses, 0 ); + p->nLits = Dch_ClassesLitNum( p->ppClasses ); + // perform SAT sweeping + Dch_ManSweep( p ); + // free memory ahead of time +p->timeTotal = clock() - clkTotal; + Dch_ManStop( p ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |