Variable timeframe abstraction.

src/aig/gia/giaAbsVta.c

@@ -654,7 +654,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
     Gia_Obj_t * pObj;
     int i, Counter;
 
-//    Vta_ManSatVerify( p );
+    Vta_ManSatVerify( p );
 
     // collect nodes in a topological order
     vOrder = Vta_ManCollectNodes( p, f );
@@ -664,7 +664,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
         pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0;
         pThis->fVisit = 0;
     }
-/*
+
     // verify
     Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
     {
@@ -691,7 +691,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
             else assert( 0 );
         }
     }
-*/
+
     // compute distance in reverse order
     pThis = Vta_ManObj( p, Vec_IntEntryLast(vOrder) );
     pThis->Prio  = 1;
@@ -883,7 +883,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
             assert( 0 );
     }
 
-/*
+
     // verify
     Vta_ManForEachObjVec( vOrder, p, pThis, i )
         pThis->Value = VTA_VARX;
@@ -948,7 +948,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
         printf( "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" );
 //    else
 //        printf( "Verification OK.\n" );
-*/
+
 
     // produce true counter-example
     if ( pTop->Prio == 0 )

src/sat/bsat/satSolver2.c

@@ -498,35 +498,55 @@ static inline int solver2_assume(sat_solver2* s, lit l)
 }
 
 static void solver2_canceluntil(sat_solver2* s, int level) {
-    lit*     trail;   
     int      bound;
     int      lastLev;
     int      c, x;
    
-    if (solver2_dlevel(s) < level)
+    if (solver2_dlevel(s) <= level)
         return;
+    assert( solver2_dlevel(s) > 0 );
 
-    trail   = s->trail;
     bound   = (veci_begin(&s->trail_lim))[level];
     lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1];
 
     for (c = s->qtail-1; c >= bound; c--) 
     {
-        x = lit_var(trail[c]);
+        x = lit_var(s->trail[c]);
         var_set_value(s, x, varX);
         s->reasons[x] = 0;
         s->units[x] = 0; // temporary?
         if ( c < lastLev )
-            var_set_polar(s, x, !lit_sign(trail[c]));
+            var_set_polar(s, x, !lit_sign(s->trail[c]));
     }
 
     for (c = s->qhead-1; c >= bound; c--)
-        order_unassigned(s,lit_var(trail[c]));
+        order_unassigned(s,lit_var(s->trail[c]));
 
     s->qhead = s->qtail = bound;
     veci_resize(&s->trail_lim,level);
 }
 
+static void solver2_canceluntil_rollback(sat_solver2* s, int NewBound) {
+    int      c, x;
+   
+    assert( solver2_dlevel(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;
+        s->units[x] = 0; // temporary?
+    }
+
+    for (c = s->qhead-1; c >= NewBound; c--)
+        order_unassigned(s,lit_var(s->trail[c]));
+
+    s->qhead = s->qtail = NewBound;
+}
+
 
 static void solver2_record(sat_solver2* s, veci* cls, int proof_id)
 {
@@ -1513,9 +1533,8 @@ void sat_solver2_rollback( sat_solver2* s )
         }
     }
     // reset implication queue
-    assert( (&s->trail_lim)->ptr[0] >= s->iSimpPivot );
-    (&s->trail_lim)->ptr[0] = s->iSimpPivot;
-    solver2_canceluntil( s, 0 );
+    assert( solver2_dlevel(s) == 0 );
+    solver2_canceluntil_rollback( s, s->iSimpPivot );
     // reset problem clauses
     if ( s->hClausePivot < veci_size(&s->clauses) )
     {