diff options
Diffstat (limited to 'src/proof/dch')
-rw-r--r-- | src/proof/dch/dch.h | 1 | ||||
-rw-r--r-- | src/proof/dch/dchCore.c | 4 |
2 files changed, 4 insertions, 1 deletions
diff --git a/src/proof/dch/dch.h b/src/proof/dch/dch.h index 5d644643..07f6a1d2 100644 --- a/src/proof/dch/dch.h +++ b/src/proof/dch/dch.h @@ -52,6 +52,7 @@ struct Dch_Pars_t_ int fPower; // uses power-aware rewriting int fUseGia; // uses GIA package int fUseCSat; // uses circuit-based solver + int fUseNew; // uses new implementation int fLightSynth; // uses lighter version of synthesis int fSkipRedSupp; // skip choices with redundant support vars int fVerbose; // verbose stats diff --git a/src/proof/dch/dchCore.c b/src/proof/dch/dchCore.c index 0da65bee..eef53e73 100644 --- a/src/proof/dch/dchCore.c +++ b/src/proof/dch/dchCore.c @@ -90,7 +90,7 @@ Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars ) { Dch_Man_t * p; Aig_Man_t * pResult; - abctime clk, clkTotal = Abc_Clock(); + abctime clk, clk2 = Abc_Clock(), clkTotal = Abc_Clock(); // reset random numbers Aig_ManRandom(1); // start the choicing manager @@ -106,6 +106,8 @@ p->timeSimInit = Abc_Clock() - clk; // free memory ahead of time p->timeTotal = Abc_Clock() - clkTotal; Dch_ManStop( p ); + //if ( pPars->fVerbose ) + Abc_PrintTime( 1, "Old choice computation time", Abc_Clock() - clk2 ); // create choices ABC_FREE( pAig->pTable ); pResult = Dch_DeriveChoiceAig( pAig, pPars->fSkipRedSupp ); |