Other improvements to &vta and &gla.

5 files changed, 257 insertions, 188 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 40c74d8a..0d1c6ff1 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -213,6 +213,7 @@ struct Gia_ParVta_t_
     int            fUseTermVars;  // use terminal variables
     int            fUseRollback;  // use rollback to the starting number of frames
     int            fPropFanout;   // propagate fanout implications
+    int            fAddLayer;     // refinement strategy by adding layers
     int            fDumpVabs;     // dumps the abstracted model
     char *         pFileVabs;     // dumps the abstracted model into this file
     int            fVerbose;      // verbose flag
@@ -704,7 +705,8 @@ extern int                 Gia_GlaPerform( Gia_Man_t * p, Gia_ParVta_t * pPars,
 extern void                Gia_VtaSetDefaultParams( Gia_ParVta_t * p );
 extern Vec_Ptr_t *         Gia_VtaAbsToFrames( Vec_Int_t * vAbs );
 extern Vec_Int_t *         Gia_VtaFramesToAbs( Vec_Vec_t * vFrames );
-extern Vec_Int_t *         Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vAbs );
+extern Vec_Int_t *         Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta );
+extern Vec_Int_t *         Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames );
 extern int                 Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars );
 /*=== giaAiger.c ===========================================================*/
 extern int                 Gia_FileSize( char * pFileName );
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 53c95650..f6ada0c8 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -445,7 +445,7 @@ void Gla_ManCollect( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int
 ***********************************************************************/
 void Gia_ManRefSetAndPropFanout_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSelect, int Sign )
 {
-    int i, Id = Gia_ObjId(p->pGia, pObj);
+    int i;//, Id = Gia_ObjId(p->pGia, pObj);
     Rfn_Obj_t * pRef0, * pRef1, * pRef = Gla_ObjRef( p, pObj, f );
     Gia_Obj_t * pFanout;
     int k;
@@ -506,7 +506,7 @@ void Gia_ManRefSetAndPropFanout_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec
 ***********************************************************************/
 void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSelect, int Sign )
 { 
-    int i, Id = Gia_ObjId(p->pGia, pObj);
+    int i;//, Id = Gia_ObjId(p->pGia, pObj);
     Rfn_Obj_t * pRef = Gla_ObjRef( p, pObj, f );
     assert( (int)pRef->Sign == Sign );
     if ( pRef->fVisit )
@@ -1100,6 +1100,8 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
     // other 
     p->vCla2Obj  = Vec_IntAlloc( 1000 );  Vec_IntPush( p->vCla2Obj, -1 );
     p->pSat      = sat_solver2_new();
+//    p->pSat->fVerbose = p->pPars->fVerbose;
+    sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax );
     p->nSatVars  = 1;
     return p;
 }
@@ -1214,7 +1216,7 @@ void Gla_ManStop( Gla_Man_t * p )
     Gla_Obj_t * pGla;
     int i;
 //    if ( p->pPars->fVerbose )
-        Abc_Print( 1, "SAT solver:  Vars = %d. Clauses = %d. Confs = %d. Cexes = %d. ObjAdded = %d\n", 
+        Abc_Print( 1, "SAT solver:  Vars = %d  Clauses = %d  Confs = %d  Cexes = %d  ObjsAdded = %d\n", 
             sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes, p->nObjAdded );
     for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
         ABC_FREE( p->pvRefis[i].pArray );
@@ -1754,8 +1756,6 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
     clk = clock();
     p = Gla_ManStart( pAig, pPars );
     p->timeInit = clock() - clk;
-    p->pSat->fVerbose = p->pPars->fVerbose;
-    sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax );
     // set runtime limit
     if ( p->pPars->nTimeOut )
         sat_solver2_set_runtime_limit( p->pSat, time(NULL) + p->pPars->nTimeOut - 1 );
@@ -1763,21 +1763,23 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
     if ( p->pPars->fVerbose )
     {
         Abc_Print( 1, "Running gate-level abstraction (GLA) with the following parameters:\n" );
-        Abc_Print( 1, "FrameStart = %d  FrameMax = %d  Conf = %d  Timeout = %d. RatioMin = %d %%.\n", 
-            p->pPars->nFramesStart, p->pPars->nFramesMax, p->pPars->nConfLimit, p->pPars->nTimeOut, pPars->nRatioMin );
-        Abc_Print( 1, "Frame   %%   Abs  PPI   FF   AND   Confl  Cex    SatVar   Core     Time\n" );
+        Abc_Print( 1, "FrameMax = %d  ConfMax = %d  LearnMax = %d  Timeout = %d  RatioMin = %d %%.\n", 
+            pPars->nFramesMax, pPars->nConfLimit, pPars->nLearntMax, pPars->nTimeOut, pPars->nRatioMin );
+        Abc_Print( 1, "Frame   %%   Abs  PPI   FF   LUT   Confl  Cex    SatVar   Core     Time\n" );
     }
     for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
     {
         int nConflsBeg = sat_solver2_nconflicts(p->pSat);
         p->pPars->iFrame = f;
+
         // load timeframe
         Gia_GlaAddTimeFrame( p, f );
+
         // create bookmark to be used for rollback
-//            sat_solver2_reducedb( p->pSat );
         sat_solver2_bookmark( p->pSat );
         Vec_IntClear( p->vAddedNew );
         p->nAbsOld = Vec_IntSize( p->vAbs );
+
         // iterate as long as there are counter-examples
         for ( i = 0; ; i++ )
         { 
@@ -1805,17 +1807,20 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
             p->nCexes++;
             // perform the refinement
             clk2 = clock();
-
-            vPPis = Gla_ManRefinement( p );
-            if ( vPPis == NULL )
+            if ( pPars->fAddLayer )
             {
-                pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL;
-                break;
+                vPPis = Gla_ManCollectPPis( p, NULL );
+//                Gla_ManExplorePPis( p, vPPis );
+            }
+            else
+            {
+                vPPis = Gla_ManRefinement( p );
+                if ( vPPis == NULL )
+                {
+                    pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL;
+                    break;
+                }
             }
-
-//            vPPis = Gla_ManCollectPPis( p, NULL );
-//            Gla_ManExplorePPis( p, vPPis );
-
             Gia_GlaAddToAbs( p, vPPis, 1 );
             Gia_GlaAddOneSlice( p, f, vPPis );
             Vec_IntFree( vPPis );
@@ -1905,7 +1910,10 @@ finish:
                 Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d.  ", f );
         }
         else
+        {
+            p->pPars->iFrame++;
             Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction.  ", f );
+        }
     }
     else
     {
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index c6f5e238..1a442a79 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -61,6 +61,7 @@ struct Vta_Man_t_
     Vec_Ptr_t *   vFrames;      // start abstraction for each frame
     int           nWords;       // the number of words in the record
     int           nCexes;       // the number of CEXes
+    int           nObjAdded;    // objects added to the abstraction
     Vec_Int_t *   vSeens;       // seen objects
     Vec_Bit_t *   vSeenGla;     // seen objects in all frames
     int           nSeenGla;     // seen objects in all frames
@@ -149,10 +150,10 @@ void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
 {
     memset( p, 0, sizeof(Gia_ParVta_t) );
     p->nFramesMax    =      0;   // maximum frames
-    p->nFramesStart  =      5;   // starting frame 
+    p->nFramesStart  =      0;   // starting frame 
     p->nFramesPast   =      4;   // overlap frames
     p->nConfLimit    =      0;   // conflict limit
-    p->nLearntMax    =  15000;   // max number of learned clauses
+    p->nLearntMax    =   1000;   // max number of learned clauses
     p->nTimeOut      =      0;   // timeout in seconds
     p->nRatioMin     =     10;   // stop when less than this % of object is abstracted
     p->fUseTermVars  =      1;   // use terminal variables
@@ -236,31 +237,31 @@ Vec_Int_t * Gia_VtaFramesToAbs( Vec_Vec_t * vFrames )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vAbs )
+Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta )
 {
     Gia_Obj_t * pObj;
-    Vec_Int_t * vPresent;
+    Vec_Int_t * vGla;
     int nObjMask, nObjs = Gia_ManObjNum(p);
-    int i, Entry, nFrames = Vec_IntEntry( vAbs, 0 );
-    assert( Vec_IntEntry(vAbs, nFrames+1) == Vec_IntSize(vAbs) );
+    int i, Entry, nFrames = Vec_IntEntry( vVta, 0 );
+    assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
     // get the bitmask
     nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
     assert( nObjs <= nObjMask );
     // go through objects
-    vPresent = Vec_IntStart( nObjs );
-    Vec_IntWriteEntry( vPresent, 0, 1 );
-    Vec_IntForEachEntryStart( vAbs, Entry, i, nFrames+2 )
+    vGla = Vec_IntStart( nObjs );
+    Vec_IntWriteEntry( vGla, 0, 1 );
+    Vec_IntForEachEntryStart( vVta, Entry, i, nFrames+2 )
     {
         pObj = Gia_ManObj( p, (Entry &  nObjMask) );
         assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsConst0(pObj) );
-        Vec_IntWriteEntry( vPresent, (Entry &  nObjMask), 1 );
+        Vec_IntWriteEntry( vGla, (Entry &  nObjMask), 1 );
     }
-    return vPresent;
+    return vGla;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Detects how many frames are completed.]
+  Synopsis    [Converting GLA vector to VTA vector.]
 
   Description []
                
@@ -269,26 +270,31 @@ Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vAbs )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Vta_ManReadFrameStart( Vec_Int_t * p, int nWords )
+Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames )
 {
-    unsigned * pTotal, * pThis;
-    int i, w, nObjs = Vec_IntSize(p) / nWords;
-    assert( Vec_IntSize(p) % nWords == 0 );
-    pTotal = ABC_CALLOC( unsigned, nWords );
-    for ( i = 0; i < nObjs; i++ )
-    {
-        pThis = (unsigned *)Vec_IntEntryP( p, nWords * i );
-        for ( w = 0; w < nWords; w++ )
-            pTotal[w] |= pThis[i];
-    }
-    for ( i = nWords * 32 - 1; i >= 0; i-- )
-        if ( Abc_InfoHasBit(pTotal, i) )
-        {
-            ABC_FREE( pTotal );
-            return i+1;
-        }
-    ABC_FREE( pTotal );
-    return -1;
+    Vec_Int_t * vVta;
+    int nObjBits, nObjMask, nObjs = Gia_ManObjNum(p);
+    int i, k, j, Entry, Counter, nGlaSize;
+    //. get the GLA size
+    nGlaSize = Vec_IntSum(vGla);
+    // get the bitmask
+    nObjBits = Abc_Base2Log(nObjs);
+    nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
+    assert( nObjs <= nObjMask );
+    // go through objects
+    vVta = Vec_IntAlloc( 1000 );
+    Vec_IntPush( vVta, nFrames );
+    Counter = nFrames + 2;
+    for ( i = 0; i <= nFrames; i++, Counter += i * nGlaSize )
+        Vec_IntPush( vVta, Counter );
+    for ( i = 0; i < nFrames; i++ )
+        for ( k = 0; k <= i; k++ )
+            Vec_IntForEachEntry( vGla, Entry, j )
+                if ( Entry ) 
+                    Vec_IntPush( vVta, (k << nObjBits) | j );
+    Counter = Vec_IntEntry(vVta, nFrames+1);
+    assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
+    return vVta;
 }
 
 /**Function*************************************************************
@@ -949,25 +955,28 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
             assert( 0 );
     }
 
-    // mark those currently included
-    Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
-    {
-        assert( pThis->fVisit == 0 );
-        pThis->fVisit = 1;
-    }
-    // add used terms, which have close relationship
-    Counter = Vec_IntSize(vTermsToAdd);
-    Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
+    if ( p->pPars->fAddLayer )
     {
-        if ( pThis->fVisit )
-            continue;
-//        Vta_ObjPreds( p, pThis, Gia_ManObj(p->pGia, pThis->iObj), &pThis0, &pThis1 );
-//        if ( (pThis0 && (pThis0->fAdded || pThis0->fVisit)) || (pThis1 && (pThis1->fAdded || pThis1->fVisit)) )
-            Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) );
+        // mark those currently included
+        Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
+        {
+            assert( pThis->fVisit == 0 );
+            pThis->fVisit = 1;
+        }
+        // add used terms, which have close relationship
+        Counter = Vec_IntSize(vTermsToAdd);
+        Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
+        {
+            if ( pThis->fVisit )
+                continue;
+    //        Vta_ObjPreds( p, pThis, Gia_ManObj(p->pGia, pThis->iObj), &pThis0, &pThis1 );
+    //        if ( (pThis0 && (pThis0->fAdded || pThis0->fVisit)) || (pThis1 && (pThis1->fAdded || pThis1->fVisit)) )
+                Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) );
+        }
+        // remove those currenty included
+        Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
+            pThis->fVisit = 0;
     }
-    // remove those currenty included
-    Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
-        pThis->fVisit = 0;
 //    printf( "\n%d -> %d\n", Counter, Vec_IntSize(vTermsToAdd) );
 //Vec_IntReverseOrder( vTermsToAdd );
 //Vec_IntSort( vTermsToAdd, 1 );
@@ -1054,6 +1063,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
                 Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
         sat_solver2_simplify( p->pSat );
     }
+    p->nObjAdded += Vec_IntSize(vTermsToAdd);
     Vec_IntFree( vTermsToAdd );
     return pCex;
 }
@@ -1091,28 +1101,15 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
     p->vSeenGla    = Vec_BitStart( Gia_ManObjNum(pGia) );
     p->nSeenGla    = 1;
     p->nSeenAll    = 1;
-    // start the abstraction
-    if ( pGia->vObjClasses == NULL )
-        p->vFrames = Gia_ManUnrollAbs( pGia, pPars->nFramesStart );
-    else
-    {
-        p->vFrames = Gia_VtaAbsToFrames( pGia->vObjClasses );
-        // update parameters
-        if ( pPars->nFramesStart != Vec_PtrSize(p->vFrames) )
-        {
-            Abc_Print( 1, "Starting frame count is changed to match the abstraction (from %d to %d).\n", pPars->nFramesStart, Vec_PtrSize(p->vFrames) ); 
-            pPars->nFramesStart = Vec_PtrSize(p->vFrames);
-        }
-        if ( pPars->nFramesMax && pPars->nFramesMax < pPars->nFramesStart )
-        {
-            Abc_Print( 1, "Maximum frame count is changed to match the starting frames (from %d to %d).\n", pPars->nFramesMax, pPars->nFramesStart ); 
-            pPars->nFramesMax = Abc_MaxInt( pPars->nFramesMax, pPars->nFramesStart );
-        }
-    }
     // other data
     p->vCla2Var    = Vec_IntAlloc( 1000 );  Vec_IntPush( p->vCla2Var, -1 );
     p->vCores      = Vec_PtrAlloc( 100 );
     p->pSat        = sat_solver2_new();
+//    p->pSat->fVerbose = p->pPars->fVerbose;
+    sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax );
+    // start the abstraction
+    assert( pGia->vObjClasses != NULL );
+    p->vFrames = Gia_VtaAbsToFrames( pGia->vObjClasses );
     p->vAddedNew   = Vec_IntAlloc( 1000 );
     return p;
 }
@@ -1131,9 +1128,8 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
 void Vga_ManStop( Vta_Man_t * p )
 {
 //    if ( p->pPars->fVerbose )
-        Abc_Print( 1, "SAT solver:  Variables = %d. Clauses = %d. Conflicts = %d. Cexes = %d.\n", 
-            sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes );
-
+        Abc_Print( 1, "SAT solver:  Vars = %d  Clauses = %d  Confs = %d  Cexes = %d  ObjsAdded = %d\n", 
+            sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes, p->nObjAdded );
     Vec_VecFreeP( (Vec_Vec_t **)&p->vCores );
     Vec_VecFreeP( (Vec_Vec_t **)&p->vFrames );
     Vec_BitFreeP( &p->vSeenGla );
@@ -1624,8 +1620,6 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
     // preconditions
     assert( Gia_ManPoNum(pAig) == 1 );
     assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
-
-/*
     // compute intial abstraction
     if ( pAig->vObjClasses == NULL )
     {
@@ -1635,11 +1629,8 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
         Vec_IntPush( pAig->vObjClasses, 4 );
         Vec_IntPush( pAig->vObjClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)) );
     }
-*/
     // start the manager
     p = Vga_ManStart( pAig, pPars );
-    p->pSat->fVerbose = p->pPars->fVerbose;
-    sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax );
     // set runtime limit
     if ( p->pPars->nTimeOut )
         sat_solver2_set_runtime_limit( p->pSat, time(NULL) + p->pPars->nTimeOut - 1 );
@@ -1647,11 +1638,11 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
     if ( p->pPars->fVerbose )
     {
         Abc_Print( 1, "Running variable-timeframe abstraction (VTA) with the following parameters:\n" );
-        Abc_Print( 1, "FrameStart = %d  FramePast = %d  FrameMax = %d  Conf = %d  Timeout = %d. RatioMin = %d %%.\n", 
-            p->pPars->nFramesStart, p->pPars->nFramesPast, p->pPars->nFramesMax, 
-            p->pPars->nConfLimit, p->pPars->nTimeOut, pPars->nRatioMin );
+        Abc_Print( 1, "FramePast = %d  FrameMax = %d  ConfMax = %d  LearnMax = %d  Timeout = %d  RatioMin = %d %%\n", 
+            pPars->nFramesPast, pPars->nFramesMax, pPars->nConfLimit, pPars->nLearntMax, pPars->nTimeOut, pPars->nRatioMin );
         Abc_Print( 1, "Frame   %%   Abs   %%   Confl  Cex    SatVar   Core   F0   F1   F2  ...\n" );
     }
+    assert( Vec_PtrSize(p->vFrames) > 0 );
     for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
     {
         int nConflsBeg = sat_solver2_nconflicts(p->pSat);
@@ -1659,72 +1650,72 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
         // realloc storage for abstraction marks
         if ( f == p->nWords * 32 )
             p->nWords = Vec_IntDoubleWidth( p->vSeens, p->nWords );
-        // check this timeframe
-        if ( f < p->pPars->nFramesStart )
-        {
-            Vga_ManAddClausesOne( p, 0, f );
+
+        // create bookmark to be used for rollback
+        nObjOld = p->nObjs;
+        sat_solver2_bookmark( p->pSat );
+        Vec_IntClear( p->vAddedNew );
+
+        // load new timeframe
+        Vga_ManAddClausesOne( p, 0, f );
+        if ( f < Vec_PtrSize(p->vFrames) )
             Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
-        }
         else
         {
-            // create bookmark to be used for rollback
-            nObjOld = p->nObjs;
-//            sat_solver2_reducedb( p->pSat );
-            sat_solver2_bookmark( p->pSat );
-            Vec_IntClear( p->vAddedNew );
-            // load the time frame
-            for ( i = 1; i <= Abc_MinInt(p->pPars->nFramesPast, p->pPars->nFramesStart); i++ )
+            for ( i = 1; i <= Abc_MinInt(p->pPars->nFramesPast, f); i++ )
                 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) );
-                if ( Status == -1 ) // resource limit is reached
-                {
-                    Vga_ManRollBack( p, nObjOld );
-                    goto finish;
-                }
-                // check timeout
-                if ( p->pSat->nRuntimeLimit && time(NULL) > p->pSat->nRuntimeLimit )
-                {
-                    Vga_ManRollBack( p, nObjOld );
-                    goto finish;
-                }
-                if ( vCore != NULL )
-                {
-                    p->timeUnsat += clock() - clk2;
-                    break;
-                }
-                p->timeSat += clock() - clk2;
-                assert( Status == 0 );
-                p->nCexes++;
-                // perform the refinement
-                clk2 = clock();
-                pCex = Vta_ManRefineAbstraction( p, f );
-                p->timeCex += clock() - clk2;
-                if ( pCex != NULL )
-                {
-                    RetValue = 0;
-                    goto finish;
-                }
-                // print the result (do not count it towards change)
-                Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk, p->pPars->fVerbose );
+        }
+
+        // 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) );
+            if ( Status == -1 ) // resource limit is reached
+            {
+                Vga_ManRollBack( p, nObjOld );
+                goto finish;
+            }
+            // check timeout
+            if ( p->pSat->nRuntimeLimit && time(NULL) > p->pSat->nRuntimeLimit )
+            {
+                Vga_ManRollBack( p, nObjOld );
+                goto finish;
+            }
+            if ( vCore != NULL )
+            {
+                p->timeUnsat += clock() - clk2;
+                break;
+            }
+            p->timeSat += clock() - clk2;
+            assert( Status == 0 );
+            p->nCexes++;
+            // perform the refinement
+            clk2 = clock();
+            pCex = Vta_ManRefineAbstraction( p, f );
+            p->timeCex += clock() - clk2;
+            if ( pCex != NULL )
+            {
+                RetValue = 0;
+                goto finish;
             }
-            assert( Status == 1 );
-            // valid core is obtained
-            Vta_ManUnsatCoreRemap( p, vCore );
-            Vec_IntSort( vCore, 1 );
-            // update the SAT solver
-            sat_solver2_rollback( p->pSat );
-            // update storage
-            Vga_ManRollBack( p, nObjOld );
-            Vec_IntShrink( p->vCla2Var, (int)p->pSat->stats.clauses+1 );
-            // load this timeframe
-            Vga_ManLoadSlice( p, vCore, 0 );
-            Vec_IntFree( vCore );
-        } 
+            // print the result (do not count it towards change)
+            Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk, p->pPars->fVerbose );
+        }
+        assert( Status == 1 );
+        // valid core is obtained
+        Vta_ManUnsatCoreRemap( p, vCore );
+        Vec_IntSort( vCore, 1 );
+        // update the SAT solver
+        sat_solver2_rollback( p->pSat );
+        // update storage
+        Vga_ManRollBack( p, nObjOld );
+        Vec_IntShrink( p->vCla2Var, (int)p->pSat->stats.clauses+1 );
+        // load this timeframe
+        Vga_ManLoadSlice( p, vCore, 0 );
+        Vec_IntFree( vCore );
+
         // run SAT solver
         clk2 = clock();
         vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
@@ -1808,7 +1799,10 @@ finish:
                     Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d.  ", f );
             }
             else
+            {
+                p->pPars->iFrame++;
                 Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction.  ", f );
+            }
         }
     }
     else
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index c116f5e7..0ab6c091 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -202,6 +202,7 @@ void Gia_ManPrintFlopClasses( Gia_Man_t * p )
 void Gia_ManPrintGateClasses( Gia_Man_t * p )
 {
     Vec_Int_t * vPis, * vPPis, * vFlops, * vNodes;
+    int nTotal;
     if ( p->vGateClasses == NULL )
         return;
     if ( Vec_IntSize(p->vGateClasses) != Gia_ManObjNum(p) )
@@ -211,10 +212,12 @@ void Gia_ManPrintGateClasses( Gia_Man_t * p )
     }
     // create additional arrays
     Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, &vFlops, &vNodes );
-    printf( "Gate-level abstraction:  PI = %d  PPI = %d  FF = %d  (%.2f %%)  AND = %d  (%.2f %%)\n", 
+    nTotal = 1 + Vec_IntSize(vFlops) + Vec_IntSize(vNodes);
+    printf( "Gate-level abstraction:  PI = %d  PPI = %d  FF = %d (%.2f %%)  AND = %d (%.2f %%)  Obj = %d (%.2f %%)\n", 
         Vec_IntSize(vPis), Vec_IntSize(vPPis), 
         Vec_IntSize(vFlops), 100.0*Vec_IntSize(vFlops)/(Gia_ManRegNum(p)+1), 
-        Vec_IntSize(vNodes), 100.0*Vec_IntSize(vNodes)/(Gia_ManAndNum(p)+1) );
+        Vec_IntSize(vNodes), 100.0*Vec_IntSize(vNodes)/(Gia_ManAndNum(p)+1), 
+        nTotal,              100.0*nTotal             /(Gia_ManRegNum(p)+Gia_ManAndNum(p)+1) );
     Vec_IntFree( vPis );
     Vec_IntFree( vPPis );
     Vec_IntFree( vFlops );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d1c1e5a9..8983ba39 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -352,6 +352,7 @@ static int Abc_CommandAbc9GlaPba             ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Gla                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Vta                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Vta2Gla            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Gla2Vta            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Reparam            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9BackReach          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Posplit            ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -797,6 +798,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&gla",          Abc_CommandAbc9Gla,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&vta",          Abc_CommandAbc9Vta,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&vta_gla",      Abc_CommandAbc9Vta2Gla,      0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&gla_vta",      Abc_CommandAbc9Gla2Vta,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&reparam",      Abc_CommandAbc9Reparam,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&back_reach",   Abc_CommandAbc9BackReach,    0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&posplit",      Abc_CommandAbc9Posplit,      0 );
@@ -27384,10 +27386,8 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_ParVta_t Pars, * pPars = &Pars;
     int c, fStartVta = 0;
     Gia_VtaSetDefaultParams( pPars );
-    pPars->nFramesStart = 30;
-    pPars->nLearntMax   = 100000;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrfdavh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrfkadvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -27486,11 +27486,14 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'f':
             pPars->fPropFanout ^= 1;
             break;
-        case 'd':
-            pPars->fDumpVabs ^= 1;
+        case 'k':
+            fStartVta ^= 1;
             break;
         case 'a':
-            fStartVta ^= 1;
+            pPars->fAddLayer ^= 1;
+            break;
+        case 'd':
+            pPars->fDumpVabs ^= 1;
             break;
         case 'v':
             pPars->fVerbose ^= 1;
@@ -27526,32 +27529,25 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" );
         return 0;
     }
-    if ( pPars->nFramesStart < 1 )
-    {
-        Abc_Print( 1, "The starting frame should be 1 or larger.\n" );
-        return 0;
-    }
     pAbc->Status  = Gia_GlaPerform( pAbc->pGia, pPars, fStartVta );
     pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &gla [-FSCLTR num] [-A file] [-fdavh]\n" );
-    Abc_Print( -2, "\t          performs gate-level abstraction of a sequential miter\n" );
+    Abc_Print( -2, "usage: &gla [-FSCLTR num] [-A file] [-fkadvh]\n" );
+    Abc_Print( -2, "\t          fixed-time-frame gate-level proof- and cex-based abstraction\n" );
     Abc_Print( -2, "\t-F num  : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
     Abc_Print( -2, "\t-S num  : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart );
-//    Abc_Print( -2, "\t-P num  : the number of previous frames for UNSAT core [default = %d]\n", pPars->nFramesPast );
     Abc_Print( -2, "\t-C num  : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit );
     Abc_Print( -2, "\t-L num  : the max number of learned clauses to keep (0=unused) [default = %d]\n", pPars->nLearntMax );
     Abc_Print( -2, "\t-T num  : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
     Abc_Print( -2, "\t-R num  : minimum percentage of abstracted objects (0<=num<=100) [default = %d]\n", pPars->nRatioMin );
     Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"glabs.aig\"]\n" );
-//    Abc_Print( -2, "\t-t      : toggle using terminal variables [default = %s]\n", pPars->fUseTermVars? "yes": "no" );
-//    Abc_Print( -2, "\t-r      : toggle using rollback after the starting frames [default = %s]\n", pPars->fUseRollback? "yes": "no" );
     Abc_Print( -2, "\t-f      : toggle propagating fanout implications [default = %s]\n", pPars->fPropFanout? "yes": "no" );
+    Abc_Print( -2, "\t-k      : toggle using VTA to kick start GLA for starting frames [default = %s]\n", fStartVta? "yes": "no" );
+    Abc_Print( -2, "\t-a      : toggle refinement by adding one layers of gates [default = %s]\n", pPars->fAddLayer? "yes": "no" );
     Abc_Print( -2, "\t-d      : toggle dumping abstracted model into a file [default = %s]\n", pPars->fDumpVabs? "yes": "no" );
-    Abc_Print( -2, "\t-a      : toggle using VTA to kick start GLA [default = %s]\n", fStartVta? "yes": "no" );
     Abc_Print( -2, "\t-v      : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h      : print the command usage\n");
     return 1;
@@ -27574,7 +27570,7 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Gia_VtaSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrdvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtradvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -27670,6 +27666,9 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'r':
             pPars->fUseRollback ^= 1;
             break;
+        case 'a':
+            pPars->fAddLayer ^= 1;
+            break;
         case 'd':
             pPars->fDumpVabs ^= 1;
             break;
@@ -27707,21 +27706,14 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" );
         return 0;
     }
-    if ( pPars->nFramesStart < 1 )
-    {
-        Abc_Print( 1, "The starting frame should be 1 or larger.\n" );
-        return 0;
-    }
-//    if ( argc == globalUtilOptind + 1 )
-//        pPars->pFileVabs = argv[globalUtilOptind];
     pAbc->Status  = Gia_VtaPerform( pAbc->pGia, pPars );
     pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &vta [-FSPCLTR num] [-A file] [-trdvh]\n" );
-    Abc_Print( -2, "\t          refines abstracted object map with proof-based abstraction\n" );
+    Abc_Print( -2, "usage: &vta [-FSPCLTR num] [-A file] [-tradvh]\n" );
+    Abc_Print( -2, "\t          variable-time-frame gate-level proof- and cex-based abstraction\n" );
     Abc_Print( -2, "\t-F num  : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
     Abc_Print( -2, "\t-S num  : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart );
     Abc_Print( -2, "\t-P num  : the number of previous frames for UNSAT core [default = %d]\n", pPars->nFramesPast );
@@ -27732,6 +27724,7 @@ usage:
     Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"vabs.aig\"]\n" );
     Abc_Print( -2, "\t-t      : toggle using terminal variables [default = %s]\n", pPars->fUseTermVars? "yes": "no" );
     Abc_Print( -2, "\t-r      : toggle using rollback after the starting frames [default = %s]\n", pPars->fUseRollback? "yes": "no" );
+    Abc_Print( -2, "\t-a      : toggle refinement by adding one layers of gates [default = %s]\n", pPars->fAddLayer? "yes": "no" );
     Abc_Print( -2, "\t-d      : toggle dumping abstracted model into a file [default = %s]\n", pPars->fDumpVabs? "yes": "no" );
     Abc_Print( -2, "\t-v      : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h      : print the command usage\n");
@@ -27773,7 +27766,7 @@ int Abc_CommandAbc9Vta2Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pGia->vObjClasses == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9Vta2Gla(): There is no variable-time-frame abstraction defines.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9Vta2Gla(): There is no variable-time-frame abstraction is defined.\n" );
         return 1;
     }
     Vec_IntFreeP( &pAbc->pGia->vGateClasses );
@@ -27783,7 +27776,7 @@ int Abc_CommandAbc9Vta2Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     Abc_Print( -2, "usage: &vta_gla [-vh]\n" );
-    Abc_Print( -2, "\t        maps variable- into fixed-time-frame abstraction\n" );
+    Abc_Print( -2, "\t        maps variable- into fixed-time-frame gate-level abstraction\n" );
     Abc_Print( -2, "\t-v    : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;
@@ -27800,6 +27793,75 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Gla2Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    int c, fVerbose = 0;
+    int nFrames = pAbc->nFrames;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Fvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Gla2Vta(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( pAbc->pGia->vGateClasses == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Gla2Vta(): There is no gate-level abstraction is defined.\n" );
+        return 1;
+    }
+    if ( pAbc->nFrames < 1 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Gla2Vta(): The number of timeframes (%d) should be a positive integer.\n", nFrames );
+        return 1;
+    }
+    Vec_IntFreeP( &pAbc->pGia->vObjClasses );
+    pAbc->pGia->vObjClasses = Gia_VtaConvertFromGla( pAbc->pGia, pAbc->pGia->vGateClasses, nFrames );
+    Vec_IntFreeP( &pAbc->pGia->vGateClasses );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &gla_vta [-F num] [-vh]\n" );
+    Abc_Print( -2, "\t          maps fixed- into variable-time-frame gate-level abstraction\n" );
+    Abc_Print( -2, "\t-F num  : timeframes in the resulting variable-time-frame abstraction [default = %d]\n", nFrames );
+    Abc_Print( -2, "\t-v      : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h      : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Reparam( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp = NULL;