diff options
Diffstat (limited to 'src/proof/ssw')
-rw-r--r-- | src/proof/ssw/ssw.h | 1 | ||||
-rw-r--r-- | src/proof/ssw/sswCore.c | 18 |
2 files changed, 19 insertions, 0 deletions
diff --git a/src/proof/ssw/ssw.h b/src/proof/ssw/ssw.h index 35d41a35..df73c357 100644 --- a/src/proof/ssw/ssw.h +++ b/src/proof/ssw/ssw.h @@ -70,6 +70,7 @@ struct Ssw_Pars_t_ int fVerbose; // verbose stats int fFlopVerbose; // verbose printout of redundant flops int fEquivDump; // enables dumping equivalences + int fStopWhenGone; // stop when PO output is not a candidate constant // optimized latch correspondence int fLatchCorrOpt; // perform register correspondence (optimized) int nSatVarMax; // max number of SAT vars before recycling SAT solver (optimized latch corr only) diff --git a/src/proof/ssw/sswCore.c b/src/proof/ssw/sswCore.c index b27e7eaf..8a08b227 100644 --- a/src/proof/ssw/sswCore.c +++ b/src/proof/ssw/sswCore.c @@ -346,6 +346,24 @@ clk = clock(); } // if ( p->pPars->fDynamic && p->nSatCallsSat-nSatCallsSat < 100 ) // p->pPars->nBTLimit = 10000; + + if ( p->pPars->fStopWhenGone && Saig_ManPoNum(p->pAig) == 1 && !Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManCo(p->pAig,0))) ) + { + printf( "Iterative refinement is stopped after iteration %d\n", nIter ); + printf( "because the property output is no longer a candidate constant.\n" ); + // prepare to quite + p->nLitsEnd = p->nLitsBeg; + p->nNodesEnd = p->nNodesBeg; + p->nRegsEnd = p->nRegsBeg; + // cleanup + Ssw_SatStop( p->pMSat ); + p->pMSat = NULL; + Ssw_ManCleanup( p ); + // cleanup + Aig_ManSetPhase( p->pAig ); + Aig_ManCleanMarkB( p->pAig ); + return Aig_ManDupSimple( p->pAig ); + } } nSatProof = p->nSatProof; nSatCallsSat = p->nSatCallsSat; |