diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-11-01 13:36:51 -0400 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-11-01 13:36:51 -0400 |
| commit | a564e2ab8184f330e87da811cedfd3faf2ee4041 (patch) | |
| tree | c356f2df0bc385b936e9bb68f68b31cda822a975 /src/proof | |
| parent | a509fa8ea89cc6374c7a13e7632cb51bc455ce43 (diff) | |
| download | abc-a564e2ab8184f330e87da811cedfd3faf2ee4041.tar.gz abc-a564e2ab8184f330e87da811cedfd3faf2ee4041.tar.bz2 abc-a564e2ab8184f330e87da811cedfd3faf2ee4041.zip | |
Sweeper internal verification and new switch for &cfraig.
Diffstat (limited to 'src/proof')
| -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 ); |