diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-10-01 18:25:41 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-10-01 18:25:41 -0700 |
| commit | 7d29663720b02b02ceaae5b75fb8fe05ba4aae73 (patch) | |
| tree | 93e9ee9d03bf6220ec2a8931b03db491d3c9194f /src/proof/dch/dchCore.c | |
| parent | 73ab6aac1fad7cf7a4f15bccafff1eabebf8cce6 (diff) | |
| download | abc-7d29663720b02b02ceaae5b75fb8fe05ba4aae73.tar.gz abc-7d29663720b02b02ceaae5b75fb8fe05ba4aae73.tar.bz2 abc-7d29663720b02b02ceaae5b75fb8fe05ba4aae73.zip | |
Fixed several important problems in choice computation (command 'dch').
Diffstat (limited to 'src/proof/dch/dchCore.c')
| -rw-r--r-- | src/proof/dch/dchCore.c | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/src/proof/dch/dchCore.c b/src/proof/dch/dchCore.c index 654ed359..da103e0e 100644 --- a/src/proof/dch/dchCore.c +++ b/src/proof/dch/dchCore.c @@ -106,19 +106,13 @@ p->timeSimInit = clock() - clk; // free memory ahead of time p->timeTotal = clock() - clkTotal; Dch_ManStop( p ); - // try something different - { -// extern void Gia_ManNormalizeChoicesTest( Aig_Man_t * pAig ); -// Gia_ManNormalizeChoicesTest( pAig ); - } - // create choices ABC_FREE( pAig->pTable ); pResult = Dch_DeriveChoiceAig( pAig, pPars->fSkipRedSupp ); // count the number of representatives if ( pPars->fVerbose ) Abc_Print( 1, "STATS: Reprs = %6d. Equivs = %6d. Choices = %6d.\n", - Dch_DeriveChoiceCountReprs( pAig ), + Dch_DeriveChoiceCountReprs( pResult ), Dch_DeriveChoiceCountEquivs( pResult ), Aig_ManChoiceNum( pResult ) ); return pResult; |