diff options
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/cec/cecSatG2.c | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index a6e99a3e..19349986 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -1651,7 +1651,7 @@ Gia_Obj_t * Cec4_ManFindRepr( Gia_Man_t * p, Cec4_Man_t * pMan, int iObj ) pMan->timeResimLoc += Abc_Clock() - clk; return NULL; } -int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** ppNew ) +int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** ppNew, int fSimOnly ) { Cec4_Man_t * pMan = Cec4_ManCreate( p, pPars ); Gia_Obj_t * pObj, * pRepr; @@ -1699,6 +1699,8 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p if ( i && i % (pPars->nRounds / 5) == 0 && pPars->fVerbose ) Cec4_ManPrintStats( p, pPars, pMan, 1 ); } + if ( fSimOnly ) + goto finalize; // perform additional simulation Cec4_ManCandIterStart( pMan ); @@ -1789,7 +1791,7 @@ finalize: Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ) { Gia_Man_t * pNew = NULL; - Cec4_ManPerformSweeping( p, pPars, &pNew ); + Cec4_ManPerformSweeping( p, pPars, &pNew, 0 ); return pNew; } void Cec4_ManSimulateTest2( Gia_Man_t * p, int fVerbose ) @@ -1797,7 +1799,7 @@ void Cec4_ManSimulateTest2( Gia_Man_t * p, int fVerbose ) abctime clk = Abc_Clock(); Cec_ParFra_t ParsFra, * pPars = &ParsFra; Cec4_ManSetParams( pPars ); - Cec4_ManPerformSweeping( p, pPars, NULL ); + Cec4_ManPerformSweeping( p, pPars, NULL, 0 ); pPars->fVerbose = fVerbose; if ( fVerbose ) Abc_PrintTime( 1, "New choice computation time", Abc_Clock() - clk ); @@ -1809,9 +1811,16 @@ Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose ) Cec4_ManSetParams( pPars ); pPars->fVerbose = fVerbose; pPars->nBTLimit = nBTLimit; - Cec4_ManPerformSweeping( p, pPars, &pNew ); + Cec4_ManPerformSweeping( p, pPars, &pNew, 0 ); return pNew; } +int Cec4_ManSimulateOnlyTest( Gia_Man_t * p, int fVerbose ) +{ + Cec_ParFra_t ParsFra, * pPars = &ParsFra; + Cec4_ManSetParams( pPars ); + pPars->fVerbose = fVerbose; + return Cec4_ManPerformSweeping( p, pPars, NULL, 1 ); +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// |