Variable timeframe abstraction.

src/aig/gia/giaAbsVta.c

@@ -1366,7 +1366,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
         if ( f == p->nWords * 32 )
             p->nWords = Vec_IntDoubleWidth( p->vSeens, p->nWords );
         // check this timeframe
-        i = 0;
+        i = 0; 
         if ( f < p->pPars->nFramesStart )
             Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
         else
@@ -1380,7 +1380,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                 Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i );
             // iterate as long as there are counter-examples
             for ( i = 0; ; i++ )
-            {
+            { 
                 clk2 = clock();
                 vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
                 assert( (vCore != NULL) == (Status == 1) );
@@ -1410,7 +1410,6 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
             Vga_ManRollBack( p, nObjOld );
             Vec_IntShrink( p->vCla2Var, (int)p->pSat->stats.clauses+1 );
             // load this timeframe
-            nObjOld = p->nObjs;
             Vga_ManLoadSlice( p, vCore, 0 );
             Vec_IntFree( vCore );
         }

src/sat/bsat/satSolver2.c

@@ -1492,8 +1492,8 @@ void sat_solver2_rollback( sat_solver2* s )
     assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size );
     veci_resize(&s->order, 0);
     if ( s->hClausePivot > 1 || s->hLearntPivot > 1 )
-    {
-        // update order
+    { 
+        // update order 
         for ( i = 0; i < s->iVarPivot; i++ )
         {
             if ( var_value(s, i) != varX )
@@ -1511,16 +1511,6 @@ void sat_solver2_rollback( sat_solver2* s )
                     pArray[j++] = pArray[k];
             veci_resize(&s->wlists[i],j);
         }
-        // compact units
-        if ( s->fProofLogging ) {
-            for ( i = 0; i < s->size; i++ )
-                if ( s->units[i] && !clause_is_used(s, s->units[i]) )
-                {
-                    var_set_value(s, i, varX);
-                    s->reasons[i] = 0;
-                    s->units[i] = 0;
-                }
-        }
     }
     // reset implication queue
     assert( (&s->trail_lim)->ptr[0] >= s->iSimpPivot );
@@ -1535,7 +1525,7 @@ void sat_solver2_rollback( sat_solver2* s )
     }
     // resetn learned clauses
     if ( s->hLearntPivot < veci_size(&s->learnts) )
-    {
+    { 
         satset* first = satset_read(&s->learnts, s->hLearntPivot);
         veci_resize(&s->claActs,   first->Id);
         if ( s->fProofLogging ) {
@@ -1548,6 +1538,20 @@ void sat_solver2_rollback( sat_solver2* s )
     // reset watcher lists
     for ( i = 2*s->iVarPivot; i < 2*s->size; i++ )
         s->wlists[i].size = 0;
+    for ( i = s->iVarPivot; i < s->size; i++ )
+    {
+        *((int*)s->vi + i) = 0;
+        s->levels  [i] = 0;
+        s->assigns [i] = varX;
+        s->reasons [i] = 0;        
+        s->units   [i] = 0;        
+#ifdef USE_FLOAT_ACTIVITY2
+        s->activity[i] = 0;
+#else
+        s->activity[i] = (1<<10);
+#endif
+        s->model   [i] = 0; 
+    }
     s->size = s->iVarPivot;
     // initialize other vars
     if ( s->size == 0 )