diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2020-12-16 10:31:25 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2020-12-16 10:31:25 -0800 |
| commit | 8066fdbcb53f0e9ea617f24de1a73bc9f0cb69f6 (patch) | |
| tree | d3598205018861c6ea65a24f7d3f3ca83634df39 /src/proof | |
| parent | 06094ade87fbec6000619bf007aaad596e8bc0a2 (diff) | |
| download | abc-8066fdbcb53f0e9ea617f24de1a73bc9f0cb69f6.tar.gz abc-8066fdbcb53f0e9ea617f24de1a73bc9f0cb69f6.tar.bz2 abc-8066fdbcb53f0e9ea617f24de1a73bc9f0cb69f6.zip | |
Adding generation of combinational speculative miters.
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 /// |