Implemented rollback in the main SAT solver and updated PDR to use it (saves about 5% of runtime).

3 files changed, 17 insertions, 13 deletions

diff --git a/src/sat/pdr/pdrCnf.c b/src/sat/pdr/pdrCnf.c
index 4b42262c..fddd292b 100644
--- a/src/sat/pdr/pdrCnf.c
+++ b/src/sat/pdr/pdrCnf.c
@@ -261,11 +261,11 @@ int Pdr_ManFreeVar( Pdr_Man_t * p, int k )
   SeeAlso     []
 
 ***********************************************************************/
-static inline sat_solver * Pdr_ManNewSolver1( Pdr_Man_t * p, int k, int fInit )
+static inline sat_solver * Pdr_ManNewSolver1( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit )
 {
-    sat_solver * pSat;
     Aig_Obj_t * pObj;
     int i;
+    assert( pSat );
     if ( p->pCnf1 == NULL )
     {
         int nRegs = p->pAig->nRegs;
@@ -277,7 +277,7 @@ static inline sat_solver * Pdr_ManNewSolver1( Pdr_Man_t * p, int k, int fInit )
         Saig_ManForEachLi( p->pAig, pObj, i )
             Vec_IntWriteEntry( p->vVar2Reg, Pdr_ObjSatVar(p, k, pObj), i );
     }
-    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf1, 1, fInit );
+    pSat = (sat_solver *)Cnf_DataWriteIntoSolverInt( pSat, p->pCnf1, 1, fInit );
     sat_solver_set_runtime_limit( pSat, p->timeToStop );
     return pSat;
 }
@@ -293,11 +293,11 @@ static inline sat_solver * Pdr_ManNewSolver1( Pdr_Man_t * p, int k, int fInit )
   SeeAlso     []
 
 ***********************************************************************/
-static inline sat_solver * Pdr_ManNewSolver2( Pdr_Man_t * p, int k, int fInit )
+static inline sat_solver * Pdr_ManNewSolver2( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit )
 {
-    sat_solver * pSat;
     Vec_Int_t * vVar2Ids;
     int i, Entry;
+    assert( pSat );
     if ( p->pCnf2 == NULL )
     {
         p->pCnf2     = Cnf_DeriveOther( p->pAig );
@@ -321,7 +321,7 @@ static inline sat_solver * Pdr_ManNewSolver2( Pdr_Man_t * p, int k, int fInit )
     Vec_IntClear( vVar2Ids );
     Vec_IntPush( vVar2Ids, -1 );
     // start the SAT solver
-    pSat = sat_solver_new();
+//    pSat = sat_solver_new();
     sat_solver_setnvars( pSat, 500 );
     sat_solver_set_runtime_limit( pSat, p->timeToStop );
     return pSat;
@@ -338,12 +338,13 @@ static inline sat_solver * Pdr_ManNewSolver2( Pdr_Man_t * p, int k, int fInit )
   SeeAlso     []
 
 ***********************************************************************/
-sat_solver * Pdr_ManNewSolver( Pdr_Man_t * p, int k, int fInit )
+sat_solver * Pdr_ManNewSolver( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit )
 {
+    assert( pSat != NULL );
     if ( p->pPars->fMonoCnf )
-        return Pdr_ManNewSolver1( p, k, fInit );
+        return Pdr_ManNewSolver1( pSat, p, k, fInit );
     else
-        return Pdr_ManNewSolver2( p, k, fInit );
+        return Pdr_ManNewSolver2( pSat, p, k, fInit );
 }
 
 
diff --git a/src/sat/pdr/pdrInt.h b/src/sat/pdr/pdrInt.h
index 39fffc48..f49ee7d0 100644
--- a/src/sat/pdr/pdrInt.h
+++ b/src/sat/pdr/pdrInt.h
@@ -138,7 +138,7 @@ extern Abc_Cex_t *     Pdr_ManDeriveCex( Pdr_Man_t * p );
 extern int             Pdr_ObjSatVar( Pdr_Man_t * p, int k, Aig_Obj_t * pObj );
 extern int             Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar );
 extern int             Pdr_ManFreeVar( Pdr_Man_t * p, int k );
-extern sat_solver *    Pdr_ManNewSolver( Pdr_Man_t * p, int k, int fInit );
+extern sat_solver *    Pdr_ManNewSolver( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit );
 /*=== pdrCore.c ==========================================================*/
 extern int             Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet );
 /*=== pdrInv.c ==========================================================*/
diff --git a/src/sat/pdr/pdrSat.c b/src/sat/pdr/pdrSat.c
index 627cb654..cc4c2b1b 100644
--- a/src/sat/pdr/pdrSat.c
+++ b/src/sat/pdr/pdrSat.c
@@ -49,7 +49,8 @@ sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k )
     assert( Vec_VecSize(p->vClauses) == k );
     assert( Vec_IntSize(p->vActVars) == k );
     // create new solver
-    pSat = Pdr_ManNewSolver( p, k, (int)(k == 0) );
+    pSat = sat_solver_new();
+    pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
     Vec_PtrPush( p->vSolvers, pSat );
     Vec_VecExpand( p->vClauses, k );
     Vec_IntPush( p->vActVars, 0 );
@@ -80,9 +81,11 @@ sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k )
         return pSat;
     assert( k < Vec_PtrSize(p->vSolvers) - 1 );
     p->nStarts++;
-    sat_solver_delete( pSat );
+//    sat_solver_delete( pSat );
+//    pSat = sat_solver_new();
+    sat_solver_rollback( pSat );
     // create new SAT solver
-    pSat = Pdr_ManNewSolver( p, k, (int)(k == 0) );
+    pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
     // write new SAT solver
     Vec_PtrWriteEntry( p->vSolvers, k, pSat );
     Vec_IntWriteEntry( p->vActVars, k, 0 );