Merge

7 files changed, 38 insertions, 3 deletions

diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index 10b06c28..65d2e24e 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -144,6 +144,7 @@ struct Cec_ParCor_t_
     int              fUseCSat;      // use circuit-based solver
 //    int              fFirstStop;    // stop on the first sat output
     int              fUseSmartCnf;  // use smart CNF computation
+    int              fStopWhenGone; // quit when PO is not a candidate constant
     int              fVerboseFlops; // verbose stats
     int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats
diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c
index f35cd952..f3a84d3a 100644
--- a/src/proof/cec/cecCorr.c
+++ b/src/proof/cec/cecCorr.c
@@ -753,6 +753,7 @@ void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIte
             nFail++;
     }
     Abc_Print( 1, "p =%6d  d =%6d  f =%6d  ", nProve, nDispr, nFail );
+    Abc_Print( 1, "%c  ", Gia_ObjIsConst( p, Gia_ObjFaninId0p(p, Gia_ManPo(p, 0)) ) ? '+' : '-' );
     Abc_PrintTime( 1, "T", Time );
 }
 
@@ -950,6 +951,14 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
 //Gia_ManEquivPrintClasses( pAig, 1, 0 );
         if ( pPars->pFunc )
             ((int (*)(void *))pPars->pFunc)( pPars->pData );
+        // quit if const is no longer there
+        if ( pPars->fStopWhenGone && Gia_ManPoNum(pAig) == 1 && !Gia_ObjIsConst( pAig, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)) ) )
+        {
+            printf( "Iterative refinement is stopped after iteration %d\n", r );
+            printf( "because the property output is no longer a candidate constant.\n" );
+            Cec_ManSimStop( pSim );
+            return 0;
+        }
     }
     if ( pPars->fVerbose )
         Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk );
@@ -1071,7 +1080,11 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     ABC_FREE( pAig->pReprs );
     ABC_FREE( pAig->pNexts );
     if ( pPars->nPrefix == 0 )
+    {
         RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars );
+        if ( RetValue == 0 )
+            return Gia_ManDup( pAig );
+    }
     else
     {
         // compute the cycles AIG
diff --git a/src/proof/dch/dchChoice.c b/src/proof/dch/dchChoice.c
index 783202e2..3f097ecc 100644
--- a/src/proof/dch/dchChoice.c
+++ b/src/proof/dch/dchChoice.c
@@ -95,7 +95,7 @@ int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig )
         pEquiv = Aig_ObjEquiv( pAig, pObj );
         if ( pEquiv == NULL )
             continue;
-        assert( pEquiv->Id > pObj->Id );
+        assert( pEquiv->Id < pObj->Id );
         nEquivs++;
     }
     return nEquivs;
diff --git a/src/proof/dch/dchCore.c b/src/proof/dch/dchCore.c
index 0d2e8c0d..b92de8a6 100644
--- a/src/proof/dch/dchCore.c
+++ b/src/proof/dch/dchCore.c
@@ -111,7 +111,9 @@ p->timeTotal = clock() - clkTotal;
     pResult = Dch_DeriveChoiceAig( pAig, pPars->fSkipRedSupp );
     // count the number of representatives
     if ( pPars->fVerbose ) 
-        Abc_Print( 1, "STATS:  Reprs = %6d.  Equivs = %6d.  Choices = %6d.\n", 
+        Abc_Print( 1, "STATS:  Ands:%8d  ->%8d.  Reprs:%7d  ->%7d.  Choices =%7d.\n", 
+               Aig_ManNodeNum(pAig), 
+               Aig_ManNodeNum(pResult), 
                Dch_DeriveChoiceCountReprs( pAig ),
                Dch_DeriveChoiceCountEquivs( pResult ),
                Aig_ManChoiceNum( pResult ) );
diff --git a/src/proof/llb/llb4Map.c b/src/proof/llb/llb4Map.c
index 51f1fec6..4b46f308 100644
--- a/src/proof/llb/llb4Map.c
+++ b/src/proof/llb/llb4Map.c
@@ -48,7 +48,7 @@ Vec_Int_t * Llb_AigMap( Aig_Man_t * pAig, int nLutSize, int nLutMin )
 {
     extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
     extern If_Man_t *  Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
-    extern void        Gia_ManSetIfParsDefault( If_Par_t * pPars );
+    extern void        Gia_ManSetIfParsDefault( void * pPars );
     If_Par_t Pars, * pPars = &Pars;
     If_Man_t * pIfMan;
     If_Obj_t * pAnd;
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 7e2e66da..7a9d4b9f 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;