Adding switch to replace proved outputs by const0.

6 files changed, 13 insertions, 10 deletions

diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index 3414842c..791955e4 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -219,7 +219,7 @@ extern void          Cec_ManCecSetDefaultParams( Cec_ParCec_t * p );
 extern void          Cec_ManCorSetDefaultParams( Cec_ParCor_t * p );
 extern void          Cec_ManChcSetDefaultParams( Cec_ParChc_t * p );
 extern Gia_Man_t *   Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSilent );
-extern Gia_Man_t *   Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars );
+extern Gia_Man_t *   Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars, int f0Proved );
 extern void          Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars );
 /*=== cecSeq.c ==========================================================*/
 extern int           Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Abc_Cex_t * pCex );
diff --git a/src/proof/cec/cecChoice.c b/src/proof/cec/cecChoice.c
index 47d6a478..780a1196 100644
--- a/src/proof/cec/cecChoice.c
+++ b/src/proof/cec/cecChoice.c
@@ -256,7 +256,7 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
         // found counter-examples to speculation
         clk2 = Abc_Clock();
         if ( pPars->fUseCSat )
-            vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
+            vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0, 0 );
         else
             vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
         Gia_ManStop( pSrm );
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index 51debba6..4e8e5497 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -232,14 +232,14 @@ void Cec_ManChcSetDefaultParams( Cec_ParChc_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
+Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars, int f0Proved )
 {
     Gia_Man_t * pNew;
     Cec_ManPat_t * pPat;
     pPat = Cec_ManPatStart();
-    Cec_ManSatSolve( pPat, pAig, pPars, NULL, NULL, NULL );
+    Cec_ManSatSolve( pPat, pAig, pPars, NULL, NULL, NULL, f0Proved );
 //    pNew = Gia_ManDupDfsSkip( pAig );
-    pNew = Gia_ManDup( pAig );
+    pNew = Gia_ManCleanup( pAig );
     Cec_ManPatStop( pPat );
     pNew->vSeqModelVec = pAig->vSeqModelVec;
     pAig->vSeqModelVec = NULL;
@@ -445,7 +445,7 @@ clk = Abc_Clock();
         if ( pPars->fRunCSat )
             Cec_ManSatSolveCSat( pPat, pSrm, pParsSat ); 
         else
-            Cec_ManSatSolve( pPat, pSrm, pParsSat, p->pAig->vIdsOrig, p->vXorNodes, pAig->vIdsEquiv ); 
+            Cec_ManSatSolve( pPat, pSrm, pParsSat, p->pAig->vIdsOrig, p->vXorNodes, pAig->vIdsEquiv, 0 ); 
 p->timeSat += Abc_Clock() - clk;
         if ( Cec_ManFraClassesUpdate( p, pSim, pPat, pSrm ) )
         {
diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c
index 8f708910..ce7e0885 100644
--- a/src/proof/cec/cecCorr.c
+++ b/src/proof/cec/cecCorr.c
@@ -996,7 +996,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
         // found counter-examples to speculation
         clk2 = Abc_Clock();
         if ( pPars->fUseCSat )
-            vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
+            vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0, 0 );
         else
             vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
         Gia_ManStop( pSrm );
diff --git a/src/proof/cec/cecInt.h b/src/proof/cec/cecInt.h
index d5456897..80663db9 100644
--- a/src/proof/cec/cecInt.h
+++ b/src/proof/cec/cecInt.h
@@ -204,7 +204,7 @@ extern int                  Cec_ManCountNonConstOutputs( Gia_Man_t * pAig );
 extern int                  Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig );
 /*=== cecSolve.c ============================================================*/
 extern int                  Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj );
-extern void                 Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs );
+extern void                 Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs, int f0Proved );
 extern void                 Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
 extern Vec_Str_t *          Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats );
 extern Vec_Int_t *          Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus );
diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c
index af6a4fdb..f8342859 100644
--- a/src/proof/cec/cecSolve.c
+++ b/src/proof/cec/cecSolve.c
@@ -696,7 +696,7 @@ Abc_Cex_t * Cex_ManGenCex( Cec_ManSat_t * p, int iOut )
     }
     return pCex;
 }
-void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs )
+void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs, int f0Proved )
 {
     Bar_Progress_t * pProgress = NULL;
     Cec_ManSat_t * p;
@@ -747,6 +747,9 @@ clk2 = Abc_Clock();
         if ( pPars->fSaveCexes && status != -1 )
             Vec_PtrWriteEntry( pAig->vSeqModelVec, i, status ? (Abc_Cex_t *)(ABC_PTRINT_T)1 : Cex_ManGenCex(p, i) );
 
+        if ( f0Proved && status == 1 )
+            Gia_ManPatchCoDriver( pAig, i, 0 );
+
 /*
         if ( status == -1 )
         {
@@ -807,7 +810,7 @@ void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t *
 {
     Vec_Str_t * vStatus;
     Vec_Int_t * vPat = Vec_IntAlloc( 1000 );
-    Vec_Int_t * vCexStore = Cbs_ManSolveMiterNc( pAig, pPars->nBTLimit, &vStatus, 0 );
+    Vec_Int_t * vCexStore = Cbs_ManSolveMiterNc( pAig, pPars->nBTLimit, &vStatus, 0, 0 );
     Gia_Obj_t * pObj;
     int i, status, iStart = 0;
     assert( Vec_StrSize(vStatus) == Gia_ManCoNum(pAig) );