diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-05 19:39:25 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-05 19:39:25 -0700 |
| commit | cd2bd70865c6362b8162bef2b3d98125df984b85 (patch) | |
| tree | 5718add2060ce0fcbed127a75c028d157639ffa8 /src/proof/dch/dchCore.c | |
| parent | c1f4545e073d27ac874103068f80a3e3162d3cd3 (diff) | |
| download | abc-cd2bd70865c6362b8162bef2b3d98125df984b85.tar.gz abc-cd2bd70865c6362b8162bef2b3d98125df984b85.tar.bz2 abc-cd2bd70865c6362b8162bef2b3d98125df984b85.zip | |
Added switch 'dch -r' to skip choices with structural support redundancy.
Diffstat (limited to 'src/proof/dch/dchCore.c')
| -rw-r--r-- | src/proof/dch/dchCore.c | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/proof/dch/dchCore.c b/src/proof/dch/dchCore.c index bfef8d8c..0d2e8c0d 100644 --- a/src/proof/dch/dchCore.c +++ b/src/proof/dch/dchCore.c @@ -53,6 +53,7 @@ void Dch_ManSetDefaultParams( Dch_Pars_t * p ) p->fSimulateTfo = 1; // simulate TFO p->fPower = 0; // power-aware rewriting p->fLightSynth = 0; // uses lighter version of synthesis + p->fSkipRedSupp = 0; // skips choices with redundant structural support p->fVerbose = 0; // verbose stats p->nNodesAhead = 1000; // the lookahead in terms of nodes p->nCallsRecycle = 100; // calls to perform before recycling SAT solver @@ -107,7 +108,7 @@ p->timeTotal = clock() - clkTotal; Dch_ManStop( p ); // create choices ABC_FREE( pAig->pTable ); - pResult = Dch_DeriveChoiceAig( pAig ); + 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", |