diff options
Diffstat (limited to 'src/proof/ssc')
| -rw-r--r-- | src/proof/ssc/ssc.h | 1 | ||||
| -rw-r--r-- | src/proof/ssc/sscCore.c | 10 |
2 files changed, 9 insertions, 2 deletions
diff --git a/src/proof/ssc/ssc.h b/src/proof/ssc/ssc.h index 1112719c..aee29713 100644 --- a/src/proof/ssc/ssc.h +++ b/src/proof/ssc/ssc.h @@ -49,6 +49,7 @@ struct Ssc_Pars_t_ int nCallsRecycle; // calls to perform before recycling SAT solver int fAppend; // append constraints to the resulting AIG int fVerbose; // verbose stats + int fVerify; // enable internal verification }; //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c index bb89d936..0fb16103 100644 --- a/src/proof/ssc/sscCore.c +++ b/src/proof/ssc/sscCore.c @@ -261,7 +261,7 @@ int Ssc_PerformVerification( Gia_Man_t * p0, Gia_Man_t * p1, Gia_Man_t * pC ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars ) +Gia_Man_t * Ssc_PerformSweepingInt( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars ) { Ssc_Man_t * p; Gia_Man_t * pResult, * pTemp; @@ -410,6 +410,13 @@ p->timeSimSat += Abc_Clock() - clk; } return pResult; } +Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars ) +{ + Gia_Man_t * pResult = Ssc_PerformSweepingInt( pAig, pCare, pPars ); + if ( pPars->fVerify ) + Ssc_PerformVerification( pAig, pResult, pCare ); + return pResult; +} Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars ) { Gia_Man_t * pAig, * pCare, * pResult; @@ -443,7 +450,6 @@ Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars ) pAig = Gia_ManDupLevelized( pResult = pAig ); Gia_ManStop( pResult ); pResult = Ssc_PerformSweeping( pAig, pCare, pPars ); - Ssc_PerformVerification( pAig, pResult, pCare ); if ( pPars->fAppend ) { Gia_ManDupAppendShare( pResult, pCare ); |