Adding rollback for the other solver.

4 files changed, 142 insertions, 4 deletions

diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c
index 8bd45026..a68bbee4 100644
--- a/src/proof/pdr/pdrSat.c
+++ b/src/proof/pdr/pdrSat.c
@@ -87,7 +87,7 @@ sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k )
     p->nStarts++;
 //    sat_solver_delete( pSat );
 //    pSat = sat_solver_new();
-    sat_solver_rollback( pSat );
+    sat_solver_restart( pSat );
     // create new SAT solver
     pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
     // write new SAT solver
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index ab1203ea..8f3098d8 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -531,6 +531,26 @@ static void sat_solver_canceluntil(sat_solver* s, int level) {
     veci_resize(&s->trail_lim,level);
 }
 
+static void sat_solver_canceluntil_rollback(sat_solver* s, int NewBound) {
+    int      c, x;
+   
+    assert( sat_solver_dl(s) == 0 );
+    assert( s->qtail == s->qhead );
+    assert( s->qtail >= NewBound );
+
+    for (c = s->qtail-1; c >= NewBound; c--) 
+    {
+        x = lit_var(s->trail[c]);
+        var_set_value(s, x, varX);
+        s->reasons[x] = 0;
+    }
+
+    for (c = s->qhead-1; c >= NewBound; c--)
+        order_unassigned(s,lit_var(s->trail[c]));
+
+    s->qhead = s->qtail = NewBound;
+}
+
 static void sat_solver_record(sat_solver* s, veci* cls)
 {
     lit*    begin = veci_begin(cls);
@@ -1011,6 +1031,7 @@ void sat_solver_setnvars(sat_solver* s,int n)
         s->activity  = ABC_REALLOC(double,   s->activity, s->cap);
 #else
         s->activity  = ABC_REALLOC(unsigned, s->activity, s->cap);
+        s->activity2 = ABC_REALLOC(unsigned, s->activity2,s->cap);
 #endif
         if ( s->factors )
         s->factors   = ABC_REALLOC(double, s->factors,  s->cap);
@@ -1084,6 +1105,7 @@ void sat_solver_delete(sat_solver* s)
         ABC_FREE(s->polarity );
         ABC_FREE(s->tags     );
         ABC_FREE(s->activity );
+        ABC_FREE(s->activity2);
         ABC_FREE(s->factors  );
         ABC_FREE(s->orderpos );
         ABC_FREE(s->reasons  );
@@ -1095,7 +1117,7 @@ void sat_solver_delete(sat_solver* s)
     ABC_FREE(s);
 }
 
-void sat_solver_rollback( sat_solver* s )
+void sat_solver_restart( sat_solver* s )
 {
     int i;
     Sat_MemRestart( &s->Mem );
@@ -1160,6 +1182,8 @@ double sat_solver_memory( sat_solver* s )
     Mem += s->cap * sizeof(double);   // ABC_FREE(s->activity );
 #else
     Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity );
+    if ( s->activity2 )
+    Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity2);
 #endif
     if ( s->factors )
     Mem += s->cap * sizeof(double);   // ABC_FREE(s->factors  );
@@ -1305,6 +1329,99 @@ void sat_solver_reducedb(sat_solver* s)
     }
 }
 
+
+// reverses to the previously bookmarked point
+void sat_solver_rollback( sat_solver* s )
+{
+    Sat_Mem_t * pMem = &s->Mem;
+    int i, k, j;
+    static int Count = 0;
+    Count++;
+    assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size );
+    assert( s->iTrailPivot >= 0 && s->iTrailPivot <= s->qtail );
+    // reset implication queue
+    sat_solver_canceluntil_rollback( s, s->iTrailPivot );
+    // update order 
+    if ( s->iVarPivot < s->size )
+    { 
+        if ( s->activity2 )
+        {
+            s->var_inc = s->var_inc2;
+            memcpy( s->activity, s->activity2, sizeof(unsigned) * s->iVarPivot );
+        }
+        veci_resize(&s->order, 0);
+        for ( i = 0; i < s->iVarPivot; i++ )
+        {
+            if ( var_value(s, i) != varX )
+                continue;
+            s->orderpos[i] = veci_size(&s->order);
+            veci_push(&s->order,i);
+            order_update(s, i);
+        }
+    }
+    // compact watches
+    for ( i = 0; i < s->iVarPivot*2; i++ )
+    {
+        cla* pArray = veci_begin(&s->wlists[i]);
+        for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
+            if ( Sat_MemClauseUsed(pMem, pArray[k]) )
+                pArray[j++] = pArray[k];
+        veci_resize(&s->wlists[i],j);
+    }
+    // reset watcher lists
+    for ( i = 2*s->iVarPivot; i < 2*s->size; i++ )
+        s->wlists[i].size = 0;
+
+    // reset clause counts
+    s->stats.clauses = pMem->BookMarkE[0];
+    s->stats.learnts = pMem->BookMarkE[1];
+    // rollback clauses
+    Sat_MemRollBack( pMem );
+
+    // resize learned arrays
+    veci_resize(&s->act_clas,  s->stats.learnts);
+
+    // initialize other vars
+    s->size = s->iVarPivot;
+    if ( s->size == 0 )
+    {
+    //    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->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;
+
+        // initialize rollback
+        s->iVarPivot              =  0; // the pivot for variables
+        s->iTrailPivot            =  0; // the pivot for trail
+        s->hProofPivot            =  1; // the pivot for proof records
+    }
+}
+
+
 int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
 {
     lit *i,*j;
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 56936088..acaceef9 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_restart( sat_solver* s );
 extern void        sat_solver_rollback( sat_solver* s );
 
 extern int         sat_solver_nvars(sat_solver* s);
@@ -101,6 +102,11 @@ struct sat_solver_t
     veci*       wlists;        // watcher lists
     veci        act_clas;      // contain clause activities
 
+    // rollback
+    int         iVarPivot;     // the pivot for variables
+    int         iTrailPivot;   // the pivot for trail
+    int         hProofPivot;   // the pivot for proof records
+
     // activities
 #ifdef USE_FLOAT_ACTIVITY
     double      var_inc;       // Amount to bump next variable with.
@@ -110,8 +116,10 @@ struct sat_solver_t
     double*     activity;      // A heuristic measurement of the activity of a variable.
 #else
     int         var_inc;       // Amount to bump next variable with.
+    int         var_inc2;      // Amount to bump next variable with.
     int         cla_inc;       // Amount to bump next clause with.
     unsigned*   activity;      // A heuristic measurement of the activity of a variable.
+    unsigned*   activity2;     // backup variable activity
 #endif
 
 //    varinfo *   vi;            // variable information
@@ -227,6 +235,19 @@ static int sat_solver_set_random(sat_solver* s, int fNotUseRandom)
     return fNotUseRandomOld;
 }
 
+static inline void sat_solver_bookmark(sat_solver* s)
+{
+    assert( s->qhead == s->qtail );
+    s->iVarPivot    = s->size;
+    s->iTrailPivot  = s->qhead;
+    Sat_MemBookMark( &s->Mem );
+    if ( s->activity2 )
+    {
+        s->var_inc2 = s->var_inc;
+        memcpy( s->activity2, s->activity, sizeof(unsigned) * s->iVarPivot );
+    }
+}
+
 static inline int sat_solver_add_const( sat_solver * pSat, int iVar, int fCompl )
 {
     lit Lits[1];
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 951940b3..a3dad126 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -1638,7 +1638,7 @@ void sat_solver2_rollback( sat_solver2* s )
     //    s->cap                    = 0;
         s->qhead                  = 0;
         s->qtail                  = 0;
-#ifdef USE_FLOAT_ACTIVITY
+#ifdef USE_FLOAT_ACTIVITY2
         s->var_inc                = 1;
         s->cla_inc                = 1;
         s->var_decay              = (float)(1 / 0.95  );
@@ -1689,7 +1689,7 @@ double sat_solver2_memory( sat_solver2* s, int fAll )
     Mem += s->cap * sizeof(varinfo2); // ABC_FREE(s->vi       );
     Mem += s->cap * sizeof(int);      // ABC_FREE(s->levels   );
     Mem += s->cap * sizeof(char);     // ABC_FREE(s->assigns  );
-#ifdef USE_FLOAT_ACTIVITY
+#ifdef USE_FLOAT_ACTIVITY2
     Mem += s->cap * sizeof(double);   // ABC_FREE(s->activity );
 #else
     Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity );