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

9 files changed, 126 insertions, 24 deletions

diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index beed07bb..129375d2 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -156,6 +156,7 @@ extern void            Cnf_DataFlipLastLiteral( Cnf_Dat_t * p );
 extern void            Cnf_DataPrint( Cnf_Dat_t * p, int fReadable );
 extern void            Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable );
 extern void *          Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );
+extern void *          Cnf_DataWriteIntoSolverInt( void * pSat, Cnf_Dat_t * p, int nFrames, int fInit );
 extern int             Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf );
 extern int             Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf );
 extern void            Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf, int fTransformPos );
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index 85311229..07c52b05 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -334,12 +334,12 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable )
   SeeAlso     []
 
 ***********************************************************************/
-void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit )
+void * Cnf_DataWriteIntoSolverInt( sat_solver * pSat, Cnf_Dat_t * p, int nFrames, int fInit )
 {
-    sat_solver * pSat;
     int i, f, status;
     assert( nFrames > 0 );
-    pSat = sat_solver_new();
+    assert( pSat );
+//    pSat = sat_solver_new();
     sat_solver_setnvars( pSat, p->nVars * nFrames );
     for ( i = 0; i < p->nClauses; i++ )
     {
@@ -426,6 +426,22 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit )
   SeeAlso     []
 
 ***********************************************************************/
+void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit )
+{
+    return Cnf_DataWriteIntoSolverInt( sat_solver_new(), p, nFrames, fInit );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes CNF into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit )
 {
     sat_solver2 * pSat;
diff --git a/src/sat/bsat/satMem.c b/src/sat/bsat/satMem.c
index 30861993..e947cbf0 100644
--- a/src/sat/bsat/satMem.c
+++ b/src/sat/bsat/satMem.c
@@ -239,6 +239,9 @@ void Sat_MmFixedRestart( Sat_MmFixed_t * p )
 {
     int i;
     char * pTemp;
+    if ( p->nChunks == 0 )
+        return;
+    assert( p->nChunks > 0 );
 
     // deallocate all chunks except the first one
     for ( i = 1; i < p->nChunks; i++ )
@@ -482,6 +485,30 @@ void Sat_MmStepStop( Sat_MmStep_t * p, int fVerbose )
 
 /**Function*************************************************************
 
+  Synopsis    [Stops the memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_MmStepRestart( Sat_MmStep_t * p )
+{
+    int i;
+    if ( p->nChunksAlloc )
+    {
+        for ( i = 0; i < p->nChunks; i++ )
+            ABC_FREE( p->pChunks[i] );
+        p->nChunks = 0;
+    }
+    for ( i = 0; i < p->nMems; i++ )
+        Sat_MmFixedRestart( p->pMems[i] );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Creates the entry.]
 
   Description []
diff --git a/src/sat/bsat/satMem.h b/src/sat/bsat/satMem.h
index 13afa9b9..128e6c9f 100644
--- a/src/sat/bsat/satMem.h
+++ b/src/sat/bsat/satMem.h
@@ -66,6 +66,7 @@ extern int                 Sat_MmFlexReadMemUsage( Sat_MmFlex_t * p );
 // hierarchical memory manager
 extern Sat_MmStep_t *      Sat_MmStepStart( int nSteps );
 extern void                Sat_MmStepStop( Sat_MmStep_t * p, int fVerbose );
+extern void                Sat_MmStepRestart( Sat_MmStep_t * p );
 extern char *              Sat_MmStepEntryFetch( Sat_MmStep_t * p, int nBytes );
 extern void                Sat_MmStepEntryRecycle( Sat_MmStep_t * p, char * pEntry, int nBytes );
 extern int                 Sat_MmStepReadMemUsage( Sat_MmStep_t * p );
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 97213e0d..32adeb7c 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -994,8 +994,6 @@ sat_solver* sat_solver_new(void)
 #ifdef USE_FLOAT_ACTIVITY
     s->var_inc                = 1;
     s->cla_inc                = 1;
-//    s->var_decay              = 1;
-//    s->cla_decay              = 1;
     s->var_decay              = (float)(1 / 0.95  );
     s->cla_decay              = (float)(1 / 0.999 );
 #else
@@ -1035,7 +1033,7 @@ void sat_solver_setnvars(sat_solver* s,int n)
     int var;
 
     if (s->cap < n){
-
+        int old_cap = s->cap;
         while (s->cap < n) s->cap = s->cap*2+1;
 
         s->wlists    = ABC_REALLOC(vecp,   s->wlists,   s->cap*2);
@@ -1052,11 +1050,16 @@ void sat_solver_setnvars(sat_solver* s,int n)
         s->tags      = ABC_REALLOC(lbool,  s->tags,     s->cap);
         s->trail     = ABC_REALLOC(lit,    s->trail,    s->cap);
         s->polarity  = ABC_REALLOC(char,   s->polarity, s->cap);
+        memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(vecp) );
     }
 
     for (var = s->size; var < n; var++){
-        vecp_new(&s->wlists[2*var]);
-        vecp_new(&s->wlists[2*var+1]);
+        assert(!s->wlists[2*var].size);
+        assert(!s->wlists[2*var+1].size);
+        if ( s->wlists[2*var].ptr == NULL )
+            vecp_new(&s->wlists[2*var]);
+        if ( s->wlists[2*var+1].ptr == NULL )
+            vecp_new(&s->wlists[2*var+1]);
 #ifdef USE_FLOAT_ACTIVITY
         s->activity[var] = 0;
 #else
@@ -1109,10 +1112,8 @@ void sat_solver_delete(sat_solver* s)
     // delete arrays
     if (s->wlists != 0){
         int i;
-        for (i = 0; i < s->size*2; i++)
+        for (i = 0; i < s->cap*2; i++)
             vecp_delete(&s->wlists[i]);
-
-        // if one is different from null, all are
         ABC_FREE(s->wlists   );
         ABC_FREE(s->activity );
         ABC_FREE(s->factors  );
@@ -1129,6 +1130,57 @@ void sat_solver_delete(sat_solver* s)
     ABC_FREE(s);
 }
 
+void sat_solver_rollback( sat_solver* s )
+{
+    int i;
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+    for (i = 0; i < vecp_size(&s->clauses); i++)
+        ABC_FREE(vecp_begin(&s->clauses)[i]);
+    for (i = 0; i < vecp_size(&s->learnts); i++)
+        ABC_FREE(vecp_begin(&s->learnts)[i]);
+#else
+    Sat_MmStepRestart( s->pMem );
+#endif
+    vecp_resize(&s->clauses, 0);
+    vecp_resize(&s->learnts, 0);
+    veci_resize(&s->trail_lim, 0);
+    veci_resize(&s->order, 0);
+    for ( i = 0; i < s->size*2; i++ )
+        s->wlists[i].size = 0;
+
+    // initialize other vars
+    s->size                   = 0;
+//    s->cap                    = 0;
+    s->qhead                  = 0;
+    s->qtail                  = 0;
+#ifdef USE_FLOAT_ACTIVITY
+    s->var_inc                = 1;
+    s->cla_inc                = 1;
+    s->var_decay              = (float)(1 / 0.95  );
+    s->cla_decay              = (float)(1 / 0.999 );
+#else
+    s->var_inc                = (1 <<  5);
+    s->cla_inc                = (1 << 11);
+#endif
+    s->root_level             = 0;
+    s->simpdb_assigns         = 0;
+    s->simpdb_props           = 0;
+    s->random_seed            = 91648253;
+    s->progress_estimate      = 0;
+    s->verbosity              = 0;
+
+    s->stats.starts           = 0;
+    s->stats.decisions        = 0;
+    s->stats.propagations     = 0;
+    s->stats.inspects         = 0;
+    s->stats.conflicts        = 0;
+    s->stats.clauses          = 0;
+    s->stats.clauses_literals = 0;
+    s->stats.learnts          = 0;
+    s->stats.learnts_literals = 0;
+    s->stats.tot_literals     = 0;
+}
+
 
 int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
 {
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index ac85300a..4c577b1e 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -47,6 +47,7 @@ extern void        sat_solver_delete(sat_solver* s);
 extern int         sat_solver_addclause(sat_solver* s, lit* begin, lit* end);
 extern int         sat_solver_simplify(sat_solver* s);
 extern int         sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
+extern void        sat_solver_rollback( sat_solver* s );
 
 extern int         sat_solver_nvars(sat_solver* s);
 extern int         sat_solver_nclauses(sat_solver* s);
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 );