Variable timeframe abstraction.

3 files changed, 248 insertions, 176 deletions

diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 3e7f2a01..52101dc0 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -38,7 +38,7 @@ struct Vta_Obj_t_
     unsigned      Prio   : 28;  // related to VTA_LARGE
     unsigned      Value  :  2;
     unsigned      fAdded :  1;
-    unsigned      fNew   :  1;
+    unsigned      fVisit :  1;
 };
 
 typedef struct Vta_Man_t_ Vta_Man_t; // manager
@@ -68,6 +68,9 @@ struct Vta_Man_t_
     sat_solver2 * pSat;         // incremental SAT solver
 };
 
+
+// ternary simulation
+
 #define VTA_VAR0   1
 #define VTA_VAR1   2
 #define VTA_VARX   3
@@ -84,16 +87,23 @@ static inline int Vta_ValIs1( Vta_Obj_t * pThis, int fCompl )
 static inline Vta_Obj_t *  Vta_ManObj( Vta_Man_t * p, int i )           { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL;                     }
 static inline int          Vta_ObjId( Vta_Man_t * p, Vta_Obj_t * pObj ) { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs;      }
 
-//static inline unsigned *   Vta_ObjAbsOld( Vta_Man_t * p, int i )   { assert( i >= 0 && i < p->nObjs ); return (unsigned *)Vec_IntEntryP( p->vAbs,    i*p->nWords ); }
-//static inline unsigned *   Vta_ObjAbsNew( Vta_Man_t * p, int i )   { assert( i >= 0 && i < p->nObjs ); return (unsigned *)Vec_IntEntryP( p->vAbsNew, i*p->nWords ); }
-
 #define Vta_ManForEachObj( p, pObj, i )                                 \
     for ( i = 1; (i < p->nObjs) && ((pObj) = Vta_ManObj(p, i)); i++ )
 #define Vta_ManForEachObjVec( vVec, p, pObj, i )                        \
     for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i++ )
-#define Vta_ManForEachObjVecReverse( vVec, p, pObj, i )                        \
+#define Vta_ManForEachObjVecReverse( vVec, p, pObj, i )                 \
     for ( i = Vec_IntSize(vVec) - 1; (i >= 1) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i-- )
 
+#define Vta_ManForEachObjObjVec( vVec, p, pObj, pObjG, i )              \
+    for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i++ )
+#define Vta_ManForEachObjObjVecReverse( vVec, p, pObj, pObjG, i )       \
+    for ( i = Vec_IntSize(vVec) - 1; (i >= 1) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i-- )
+
+#define Vta_ManForEachObjObj( p, pObjVta, pObjGia, i )                  \
+    for ( i = 1; (i < p->nObjs) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )
+#define Vta_ManForEachObjObjReverse( p, pObjVta, pObjGia, i )           \
+    for ( i = Vec_IntSize(vVec) - 1; (i >= 1) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )
+
 // abstraction is given as an array of integers:
 // - the first entry is the number of timeframes (F)
 // - the next (F+1) entries give the beginning position of each timeframe
@@ -365,7 +375,6 @@ static inline Vta_Obj_t * Vga_ManFindOrAdd( Vta_Man_t * p, int iObj, int iFrame
     pThis = Vta_ManObj(p, *pPlace);
     pThis->iObj   = iObj;
     pThis->iFrame = iFrame;
-    pThis->fNew   = 1;
     return pThis;
 }
 static inline void Vga_ManDelete( Vta_Man_t * p, int iObj, int iFrame )
@@ -377,6 +386,33 @@ static inline void Vga_ManDelete( Vta_Man_t * p, int iObj, int iFrame )
     pThis->iNext = -1;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Derives counter-example using current assignments.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Vga_ManDeriveCex( Vta_Man_t * p )
+{
+    Abc_Cex_t * pCex;
+    Vta_Obj_t * pThis;
+    Gia_Obj_t * pObj;
+    int i;
+    pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 );
+    pCex->iPo = 0;
+    pCex->iFrame = p->pPars->iFrame;
+    Vta_ManForEachObjObj( p, pThis, pObj, i )
+        if ( Gia_ObjIsPi(p->pGia, pObj) && sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) )
+            Abc_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) );
+    return pCex;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Remaps core into frame/node pairs.]
@@ -451,6 +487,77 @@ int Vta_ManObjIsUsed( Vta_Man_t * p, int iObj )
 
 /**Function*************************************************************
 
+  Synopsis    [Finds predecessors of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vta_ObjPreds( Vta_Man_t * p, Vta_Obj_t * pThis, Gia_Obj_t * pObj, Vta_Obj_t ** ppThis0, Vta_Obj_t ** ppThis1 )
+{
+    *ppThis0 = NULL;
+    *ppThis1 = NULL;
+    if ( !pThis->fAdded )
+        return;
+    assert( !Gia_ObjIsPi(p->pGia, pObj) );
+    if ( Gia_ObjIsConst0(pObj) || (Gia_ObjIsCi(pObj) && pThis->iFrame == 0) )
+        return;
+    if ( Gia_ObjIsAnd(pObj) )
+    {
+        *ppThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
+        *ppThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
+        assert( *ppThis0 && *ppThis1 );
+        return;
+    }
+    assert( Gia_ObjIsRo(p->pGia, pObj) && pThis->iFrame > 0 );
+    pObj = Gia_ObjRoToRi( p->pGia, pObj );
+    *ppThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
+    assert( *ppThis0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect const/PI/RO/AND in a topological order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Vta_ManCollectNodes_rec( Vta_Man_t * p, Vta_Obj_t * pThis, Vec_Int_t * vOrder )
+{
+    Gia_Obj_t * pObj;
+    Vta_Obj_t * pThis0, * pThis1;
+    if ( !pThis->fVisit )
+        return;
+    pThis->fVisit = 1;
+    pObj = Gia_ManObj( p->pGia, pThis->iObj );
+    Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
+    if ( pThis0 ) Vta_ManCollectNodes_rec( p, pThis0, vOrder );
+    if ( pThis1 ) Vta_ManCollectNodes_rec( p, pThis1, vOrder );
+    Vec_IntPush( vOrder, Vta_ObjId(p, pThis) );
+}
+Vec_Int_t * Vta_ManCollectNodes( Vta_Man_t * p, int f )
+{
+    Vta_Obj_t * pThis;
+    Gia_Obj_t * pObj;
+    Vec_IntClear( p->vOrder );
+    pObj = Gia_ManPo( p->pGia, 0 );
+    pThis = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
+    assert( pThis != NULL );
+    assert( !pThis->fVisit );
+    Vta_ManCollectNodes_rec( p, pThis, p->vOrder );
+    assert( pThis->fVisit );
+    return p->vOrder;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Refines abstraction.]
 
   Description []
@@ -460,45 +567,45 @@ int Vta_ManObjIsUsed( Vta_Man_t * p, int iObj )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p )
+Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
 {
     Abc_Cex_t * pCex = NULL;
+    Vec_Int_t * vOrder, * vTermsToAdd;
     Vec_Ptr_t * vTermsUsed, * vTermsUnused;
     Vta_Obj_t * pThis, * pThis0, * pThis1, * pTop;
     Gia_Obj_t * pObj;
     int i, Counter;
-    assert( Vec_IntSize(p->vOrder) == p->nObjs - 1 );
-    // clean depth field
-    Vta_ManForEachObj( p, pThis, i )
+
+    // collect nodes in a topological order
+    vOrder = Vta_ManCollectNodes( p, f );
+    Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
     {
         pThis->Prio = VTA_LARGE;
         pThis->Value = sat_solver2_var_value(p->pSat, i) ? VTA_VAR1 : VTA_VAR0;
+        pThis->fVisit = 0;
     }
 
-    // set the last node
-    pThis = Vta_ManObj( p, Vec_IntEntryLast(p->vOrder) );
-    pThis->Prio = 1;
-
-    // consider nodes in the reverse order
+    // compute distance in reverse order
+    pThis = Vta_ManObj( p, p->nObjs - 1 );
+    pThis->Prio  = 1;
+    // collect used and unused terms
     vTermsUsed   = Vec_PtrAlloc( 1015 );
     vTermsUnused = Vec_PtrAlloc( 1016 );
-    Vta_ManForEachObjVecReverse( p->vOrder, p, pThis, i )
+    Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
     {
-        // skip unreachable ones
-        if ( pThis->Prio == VTA_LARGE )
-            continue;
-        // skip contants and PIs
-        pObj = Gia_ManObj( p->pGia, pThis->iObj );
+        // there is no unreachable states
+        assert( pThis->Prio < VTA_LARGE );
+        // skip constants and PIs
         if ( Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) )
         {
-            pThis->Prio = 0;
+            pThis->Prio = 0; // set highest priority
             continue;
         }
         // collect useful terminals
         assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
         if ( !pThis->fAdded )
         {
-            assert( pThis->Prio > 0 || pThis->Prio < VTA_LARGE );
+            assert( pThis->Prio > 0 );
             if ( Vta_ManObjIsUsed(p, pThis->iObj) )
                 Vec_PtrPush( vTermsUsed, pThis );
             else
@@ -506,57 +613,45 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p )
             continue;
         }
         // propagate
-        if ( Gia_ObjIsAnd(pObj) )
-        {
-            pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
-            pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
-            assert( pThis0 && pThis1 );
+        Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
+        if ( pThis0 ) 
             pThis0->Prio = Abc_MinInt( pThis0->Prio, pThis->Prio + 1 );
+        if ( pThis1 ) 
             pThis1->Prio = Abc_MinInt( pThis1->Prio, pThis->Prio + 1 );
-        }
-        else if ( Gia_ObjIsRo(p->pGia, pObj) )
-        {
-            if ( pThis->iFrame == 0 )
-                pThis->Prio = 0;
-            else
-            {
-                pObj = Gia_ObjRoToRi( p->pGia, pObj );
-                pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
-                assert( pThis0 );
-                pThis0->Prio = Abc_MinInt( pThis0->Prio, pThis->Prio + 1 );
-            }
-        }
-        else assert( 0 );
     }
     // objects with equal distance should receive priority based on number
     // those objects whose prototypes have been added in other timeframes
     // should have higher priority than the current object
     Vec_PtrSort( vTermsUsed,   (int (*)(void))Vta_ManComputeDepthIncrease );
     Vec_PtrSort( vTermsUnused, (int (*)(void))Vta_ManComputeDepthIncrease );
+    if ( Vec_PtrSize(vTermsUsed) > 1 )
+    {
+        pThis0 = (Vta_Obj_t *)Vec_PtrEntry(vTermsUsed, 0);
+        pThis1 = (Vta_Obj_t *)Vec_PtrEntryLast(vTermsUsed);
+        assert( pThis0->Prio <= pThis1->Prio );
+    }
     // assign the priority based on these orders
     Counter = 1;
     Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
         pThis->Prio = Counter++;
     Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
         pThis->Prio = Counter++;
+    Vec_PtrFree( vTermsUsed );
+    Vec_PtrFree( vTermsUnused );
 
 
     // propagate in the direct order
-    Vta_ManForEachObjVec( p->vOrder, p, pThis, i )
+    Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
     {
-        assert( pThis->fNew == 0 );
-        // skip unreachable ones
-        if ( pThis->Prio == VTA_LARGE )
-            continue;
+        assert( pThis->fVisit == 0 );
+        assert( pThis->Prio < VTA_LARGE );
         // skip terminal objects
         if ( !pThis->fAdded )
             continue;
         // assumes that values are assigned!!!
         assert( pThis->Value != 0 );
         // propagate
-        pObj = Gia_ManObj( p->pGia, pThis->iObj );
         assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
-
         if ( Gia_ObjIsAnd(pObj) )
         {
             pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
@@ -570,7 +665,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p )
             else if ( pThis->Value == VTA_VAR0 )
             {
                 if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
-                    pThis->Prio = Abc_MinInt( pThis0->Prio, pThis1->Prio );
+                    pThis->Prio = Abc_MinInt( pThis0->Prio, pThis1->Prio ); // choice!!!
                 else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
                     pThis->Prio = pThis0->Prio;
                 else if ( Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
@@ -591,27 +686,25 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p )
         }
     }
 
-    Vec_PtrClear( vTermsUsed );
-
     // select important values
     pTop = Vta_ManObj( p, Vec_IntEntryLast(p->vOrder) );
-    pTop->fNew = 1;
-    Vta_ManForEachObjVec( p->vOrder, p, pThis, i )
+    pTop->fVisit = 1;
+    vTermsToAdd = Vec_IntAlloc( 100 );
+    Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
     {
-        if ( pThis->fNew == 0 )
+        if ( !pThis->fVisit )
             continue;
-        pThis->fNew = 0;
+        pThis->fVisit = 0;
         assert( pThis->Prio >= 0 && pThis->Prio <= pTop->Prio );
         // skip terminal objects
         if ( !pThis->fAdded )
         {
-            Vec_PtrPush( vTermsUsed, pThis );
+            Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) );
             continue;
         }
         // assumes that values are assigned!!!
         assert( pThis->Value != 0 );
         // propagate
-        pObj = Gia_ManObj( p->pGia, pThis->iObj );
         assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
         if ( Gia_ObjIsAnd(pObj) )
         {
@@ -621,24 +714,36 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p )
             if ( pThis->Value == VTA_VAR1 )
             {
                 assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
-                pThis0->fNew = 1;
-                pThis1->fNew = 1;
+                assert( pThis0->Prio <= pThis->Prio );
+                assert( pThis1->Prio <= pThis->Prio );
+                pThis0->fVisit = 1;
+                pThis1->fVisit = 1;
             }
             else if ( pThis->Value == VTA_VAR0 )
             {
                 if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
                 {
-                    assert( pThis0->Prio <= pThis->Prio );
-                    assert( pThis1->Prio <= pThis->Prio );
-                    if ( pThis0->Prio <= pThis1->Prio )
-                        pThis0->fNew = 1;
+                    if ( pThis0->Prio <= pThis1->Prio ) // choice!!!
+                    {
+                        pThis0->fVisit = 1;
+                        assert( pThis0->Prio == pThis->Prio );
+                    }
                     else
-                        pThis1->fNew = 1;
+                    {
+                        pThis1->fVisit = 1;
+                        assert( pThis1->Prio == pThis->Prio );
+                    }
                 }
                 else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
-                    pThis0->fNew = 1;
+                {
+                    pThis0->fVisit = 1;
+                    assert( pThis0->Prio == pThis->Prio );
+                }
                 else if ( Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
-                    pThis1->fNew = 1;
+                {
+                    pThis1->fVisit = 1;
+                    assert( pThis1->Prio == pThis->Prio );
+                }
                 else assert( 0 );
             }
             else assert( 0 );
@@ -650,21 +755,22 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p )
                 pObj = Gia_ObjRoToRi( p->pGia, pObj );
                 pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
                 assert( pThis0 );
-                pThis0->fNew = 1;
+                pThis0->fVisit = 1;
+                assert( pThis0->Prio == pThis->Prio );
             }
         }
+        else assert( 0 );
     }
 
     // verify
-    Vta_ManForEachObj( p, pThis, i )
+    Vta_ManForEachObjVec( p->vOrder, p, pThis, i )
         pThis->Value = VTA_VARX;
-    Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
+    Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
         pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0;
     // simulate 
-    Vta_ManForEachObjVec( p->vOrder, p, pThis, i )
+    Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
     {
-        assert( pThis->fNew == 0 );
-        pObj = Gia_ManObj( p->pGia, pThis->iObj );
+        assert( pThis->fVisit == 0 );
         if ( Gia_ObjIsAnd(pObj) )
         {
             pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
@@ -691,10 +797,11 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p )
                 else
                     pThis->Value = VTA_VARX;
             }
+            else
+                pThis->Value = VTA_VAR0;
         }
         // double check the solver
-        if ( pThis->Value != VTA_VARX )
-            assert( (int)pThis->Value == (sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0) );
+        assert( pThis->Value == VTA_VARX || (int)pThis->Value == (sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0) );
     }
 
     // check the output
@@ -703,15 +810,15 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p )
 
     // produce true counter-example
     if ( pTop->Prio == 0 )
+        pCex = Vga_ManDeriveCex( p );
+/*
     {
-        pCex = NULL;
         pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 );
         pCex->iPo = 0;
         pCex->iFrame = p->pPars->iFrame;
-        Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
+        Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
         {
             assert( pThis->Value == VTA_VAR0 || pThis->Value == VTA_VAR1 );
-            pObj = Gia_ManObj( p->pGia, pThis->iObj );
             assert( Gia_ObjIsConst0(pObj) || Gia_ObjIsCi(pObj) );
             if ( Gia_ObjIsRo(p->pGia, pObj) )
                 assert( pThis->iFrame == 0 && pThis->Value == VTA_VAR0 );
@@ -719,35 +826,14 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p )
                 Abc_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) );
         }
     }
+*/
     // perform refinement
     else
     {
-        Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
-        {
-            assert( !pThis->fAdded );
-            pObj = Gia_ManObj( p->pGia, pThis->iObj );
-            if ( Gia_ObjIsAnd(pObj) )
-            {
-                Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
-                Vga_ManFindOrAdd( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
-            }
-            else if ( Gia_ObjIsRo(p->pGia, pObj) )
-            {
-                if ( pThis->iFrame > 0 )
-                {
-                    pObj = Gia_ObjRoToRi( p->pGia, pObj );
-                    Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
-                }
-            }
-            else assert( 0 );
-        }
-        // add clauses
-        Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
+        Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
             Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
     }
-
-    Vec_PtrFree( vTermsUsed );
-    Vec_PtrFree( vTermsUnused );
+    Vec_IntFree( vTermsToAdd );
     return pCex;
 }
 
@@ -848,7 +934,7 @@ void Vga_ManStop( Vta_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue )
+Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls )
 {
     Vec_Int_t * vPres;
     Vec_Int_t * vCore;
@@ -856,6 +942,8 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat
     int nConfPrev = pSat->stats.conflicts;
     if ( piRetValue )
         *piRetValue = 1;
+    if ( pnConfls )
+        *pnConfls = 0;
     // solve the problem
     RetValue = sat_solver2_solve( pSat, &iLit, &iLit+1, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( RetValue == l_Undef )
@@ -870,9 +958,11 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat
             *piRetValue = 0;
         return NULL;
     }
+    if ( pnConfls )
+        *pnConfls = (int)pSat->stats.conflicts - nConfPrev;
     if ( fVerbose )
     {
-        printf( "%6d", (int)pSat->stats.conflicts - nConfPrev );
+//        printf( "%6d", (int)pSat->stats.conflicts - nConfPrev );
 //        printf( "UNSAT after %7d conflicts.      ", pSat->stats.conflicts );
 //        Abc_PrintTime( 1, "Time", clock() - clk );
     }
@@ -920,7 +1010,7 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat
   SeeAlso     []
 
 ***********************************************************************/
-void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames )
+void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int fVerbose )
 {
     unsigned * pInfo;
     int * pCountAll, * pCountUni;
@@ -934,7 +1024,7 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames )
         iFrame = (Entry >> p->nObjBits);
         assert( iFrame < nFrames );
         pInfo  = (unsigned *)Vec_IntEntryP( p->vSeens, p->nWords * iObj );
-        if ( Abc_InfoHasBit(pInfo, iFrame) == 0 )
+        if ( !Abc_InfoHasBit(pInfo, iFrame) )
         {
             Abc_InfoSetBit( pInfo, iFrame );
             pCountUni[iFrame+1]++;
@@ -948,14 +1038,17 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames )
             p->nSeenGla++;
         }
     }
-//    printf( "%5d%5d", pCountAll[0], pCountUni[0] ); 
-    printf( "%6d", p->nSeenGla ); 
-    printf( "%6d", pCountAll[0] ); 
-    for ( k = 0; k < nFrames; k++ )
-//        printf( "%5d%5d  ", pCountAll[k+1], pCountUni[k+1] ); 
-        printf( "%4d", pCountAll[k+1] ); 
-    printf( "\n" );
-    fflush( stdout );
+    if ( fVerbose )
+    {
+    //    printf( "%5d%5d", pCountAll[0], pCountUni[0] ); 
+        printf( "%6d", p->nSeenGla ); 
+        printf( "%6d", pCountAll[0] ); 
+        for ( k = 0; k < nFrames; k++ )
+    //        printf( "%5d%5d  ", pCountAll[k+1], pCountUni[k+1] ); 
+            printf( "%4d", pCountAll[k+1] ); 
+        printf( "\n" );
+        fflush( stdout );
+    }
     ABC_FREE( pCountAll );
     ABC_FREE( pCountUni );
 }
@@ -1066,6 +1159,7 @@ static inline int Vga_ManGetOutLit( Vta_Man_t * p, int f )
     return Abc_Var2Lit( Vta_ObjId(p, pThis), Gia_ObjFaninC0(pObj) );
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Collect nodes/flops involved in different timeframes.]
@@ -1080,11 +1174,9 @@ static inline int Vga_ManGetOutLit( Vta_Man_t * p, int f )
 int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
 {
     Vta_Man_t * p;
-    Vta_Obj_t * pThis;
     Vec_Int_t * vCore;
     Abc_Cex_t * pCex = NULL;
-    Gia_Obj_t * pObj;
-    int i, f, Status, RetValue = -1;
+    int i, f, nConfls, Status, RetValue = -1;
     int clk = clock();
     // preconditions
     assert( Gia_ManPoNum(pAig) == 1 );
@@ -1104,78 +1196,61 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
             p->nWords = Vec_IntDoubleWidth( p->vSeens, p->nWords );
         // check this timeframe
         if ( f < p->pPars->nFramesStart )
-        {
-            // load this timeframe
             Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
-            // run SAT solver
-            vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status );
-            assert( (vCore != NULL) == (Status == 1) );
-            if ( Status == -1 )
-                break;
-            if ( Status == 0 )
-            {
-                // make sure, there was no initial abstraction (otherwise, it was invalid)
-                assert( pAig->vObjClasses == NULL );
-                // derive counter-example
-                pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 );
-                pCex->iPo = 0;
-                pCex->iFrame = p->pPars->iFrame;
-                Vta_ManForEachObj( p, pThis, i )
-                {
-                    pObj = Gia_ManObj( p->pGia, pThis->iObj );
-                    if ( Gia_ObjIsPi(p->pGia, pObj) && sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) )
-                        Abc_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) );
-                }
-            }
-        }
         else
         {
-/*
+            // create bookmark to be used for rollback
+            sat_solver2_bookmark( p->pSat );
             // load the time frame
-            int Limit = Abc_MinInt(5, p->pPars->nFramesStart);
-            for ( i = 1; i <= Limit; i++ )
+            for ( i = 1; i <= Abc_MinInt(4, p->pPars->nFramesStart); i++ )
                 Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i );
             // iterate as long as there are counter-examples
-            do {
-                vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status );
+            while ( 1 )
+            {
+                vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, NULL );
                 assert( (vCore != NULL) == (Status == 1) );
                 if ( Status == -1 ) // resource limit is reached
-                    break;
+                    goto finish;
                 if ( vCore != NULL )
-                {
-                    // rollback and add the core
-                    // return and double check
                     break;
-                }
-                pCex = Vta_ManRefineAbstraction( p );
-            } 
-            while ( pCex == NULL );
-            if ( Status == -1 ) // resource limit is reached
-                break;
-*/
-        }
-        if ( pCex != NULL )
-        {
-            printf( "True CEX is detected.\n" );
-            RetValue = 0;
-            break;
+                assert( Status == 0 );
+                pCex = Vta_ManRefineAbstraction( p, f );
+                goto finish;
+            }
+            assert( Status == 1 );
+            // valid core is obtained
+            Vta_ManUnsatCoreRemap( p, vCore );
+            Vec_IntSort( vCore, 0 );
+            // update the SAT solver
+            sat_solver2_rollback( p->pSat );
+            // load this timeframe
+            Vga_ManLoadSlice( p, vCore, 0 );
+            Vec_IntFree( vCore );
         }
-        if ( vCore == NULL )
+        // run SAT solver
+        vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
+        if ( p->pPars->fVerbose )
+            printf( "%6d", nConfls );
+        assert( (vCore != NULL) == (Status == 1) );
+        if ( Status == -1 ) // resource limit is reached
+            goto finish;
+        if ( Status == 0 )
         {
-            printf( "Resource limit is exhausted.\n" );
-            RetValue = -1;
-            break;
+            // make sure, there was no initial abstraction (otherwise, it was invalid)
+            assert( pAig->vObjClasses == NULL && f < p->pPars->nFramesStart );
+            pCex = Vga_ManDeriveCex( p );
         }
         // add the core
         Vta_ManUnsatCoreRemap( p, vCore );
+        // add in direct topological order
+        Vec_IntSort( vCore, 0 );
         Vec_PtrPush( p->vCores, vCore );
         // print the result
-        if ( p->pPars->fVerbose )
-            Vta_ManAbsPrintFrame( p, vCore, f+1 );
-
+        Vta_ManAbsPrintFrame( p, vCore, f+1, p->pPars->fVerbose );
         if ( f == p->pPars->nFramesStart-1 )
-            break;
+           break;
     }
+finish:
     // analize the results
     if ( pCex == NULL )
     {
diff --git a/src/aig/gia/giaFrames.c b/src/aig/gia/giaFrames.c
index 237e6c5c..a14122ae 100644
--- a/src/aig/gia/giaFrames.c
+++ b/src/aig/gia/giaFrames.c
@@ -200,6 +200,8 @@ Vec_Ptr_t * Gia_ManUnrollAbs( Gia_Man_t * p, int nFrames )
             }
 //            printf( "\n" );
         }
+        // add in reverse topological order
+        Vec_IntSort( vOne, 1 );
         Vec_PtrPush( vFrames, vOne );
         assert( Vec_IntSize(vOne) <= Size - 1 );
     }
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index 29279b86..221ba3e8 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -55,11 +55,6 @@ extern void         Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * p );
 extern int *        Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars );
 extern void         Sat_Solver2DoubleClauses( sat_solver2 * p, int iVar );
 
-// trace recording
-extern void         sat_solver2TraceStart( sat_solver2 * pSat, char * pName );
-extern void         sat_solver2TraceStop( sat_solver2 * pSat );
-extern void         sat_solver2TraceWrite( sat_solver2 * pSat, int * pBeg, int * pEnd, int fRoot );
-
 // global variables
 extern int          var_is_partA (sat_solver2* s, int v);
 extern void         var_set_partA(sat_solver2* s, int v, int partA);
@@ -257,7 +252,7 @@ static inline int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom)
     return fNotUseRandomOld;
 }
 
-static inline int sat_solver2_bookmark(sat_solver2* s)
+static inline void sat_solver2_bookmark(sat_solver2* s)
 {
     s->hLearntPivot = veci_size(&s->learnts);
     s->hClausePivot = veci_size(&s->clauses);