Variable timeframe abstraction.

3 files changed, 274 insertions, 132 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 98766396..d80c0963 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -196,9 +196,17 @@ struct Gia_ParSim_t_
     int            iOutFail;      // index of the failed output
 };
 
-extern void Gia_ManSimSetDefaultParams( Gia_ParSim_t * p );
-extern int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars );
-
+// abstraction parameters
+typedef struct Gia_ParVta_t_ Gia_ParVta_t;
+struct Gia_ParVta_t_
+{
+    int            nFramesStart;  // starting frame 
+    int            nFramesMax;    // maximum frames
+    int            nConfLimit;    // conflict limit
+    int            nTimeOut;      // timeout in seconds
+    int            fVerbose;      // verbose flag
+    int            iFrame;        // the number of frames covered 
+};
 
 static inline int          Gia_IntAbs( int n )                    { return (n < 0)? -n : n;                                     }
 static inline int          Gia_Float2Int( float Val )             { union { int x; float y; } v; v.y = Val; return v.x;         }
@@ -611,6 +619,12 @@ extern int                 Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int
 extern int                 Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars );
 extern int                 Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf );
 extern int                 Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver );
+/*=== giaAbsVta.c ===========================================================*/
+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 int                 Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars );
 /*=== giaAiger.c ===========================================================*/
 extern int                 Gia_FileSize( char * pFileName );
 extern Gia_Man_t *         Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck );
@@ -783,6 +797,7 @@ extern Gia_Man_t *         Gia_ManPerformMapShrink( Gia_Man_t * p, int fKeepLeve
 /*=== giaSort.c ============================================================*/
 extern int *               Gia_SortFloats( float * pArray, int * pPerm, int nSize );
 /*=== giaSim.c ============================================================*/
+extern void                Gia_ManSimSetDefaultParams( Gia_ParSim_t * p );
 extern int                 Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars );
 /*=== giaSpeedup.c ============================================================*/
 extern float               Gia_ManDelayTraceLut( Gia_Man_t * p );
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 06988cf9..881cde6d 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -46,13 +46,8 @@ struct Vta_Man_t_
 {
     // user data
     Gia_Man_t *   pGia;         // AIG manager
-    int           nFramesStart; // the number of starting frames
-    int           nFramesMax;   // maximum number of frames
-    int           nConfMax;     // conflict limit
-    int           nTimeMax;     // runtime limit
-    int           fVerbose;     // verbose flag
+    Gia_ParVta_t* pPars;        // parameters
     // internal data
-    int           iFrame;       // current frame
     int           nObjs;        // the number of objects
     int           nObjsAlloc;   // the number of objects allocated
     int           nBins;        // number of hash table entries
@@ -109,6 +104,27 @@ static inline int          Vta_ObjId( Vta_Man_t * p, Vta_Obj_t * pObj ) { assert
 
 /**Function*************************************************************
 
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
+{
+    memset( p, 0, sizeof(Gia_ParVta_t) );
+    p->nFramesStart  =   10;  
+    p->nFramesMax    =    0;
+    p->nConfLimit    =    0;
+    p->nTimeOut      =   60;
+    p->fVerbose      =    1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Converting from one array to per-frame arrays.]
 
   Description []
@@ -118,7 +134,7 @@ static inline int          Vta_ObjId( Vta_Man_t * p, Vta_Obj_t * pObj ) { assert
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Vta_ManAbsToFrames( Vec_Int_t * vAbs )
+Vec_Ptr_t * Gia_VtaAbsToFrames( Vec_Int_t * vAbs )
 {
     Vec_Ptr_t * vFrames;
     Vec_Int_t * vFrame;
@@ -150,7 +166,7 @@ Vec_Ptr_t * Vta_ManAbsToFrames( Vec_Int_t * vAbs )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Vta_ManFramesToAbs( Vec_Vec_t * vFrames )
+Vec_Int_t * Gia_VtaFramesToAbs( Vec_Vec_t * vFrames )
 {
     Vec_Int_t * vOne, * vAbs;
     int i, k, Entry, nSize;
@@ -173,6 +189,33 @@ Vec_Int_t * Vta_ManFramesToAbs( Vec_Vec_t * vFrames )
 
 /**Function*************************************************************
 
+  Synopsis    [Converting VTA vector to GLA vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vAbs )
+{
+    Vec_Int_t * vPresent;
+    int nObjMask, nObjs = Gia_ManObjNum(p);
+    int i, Entry, nFrames = Vec_IntEntry( vAbs, 0 );
+    assert( Vec_IntEntry(vAbs, nFrames+1) == Vec_IntSize(vAbs) );
+    // get the bitmask
+    nObjMask = (1 << Gia_Base2Log(nObjs)) - 1;
+    assert( nObjs <= nObjMask );
+    // go through objects
+    vPresent = Vec_IntAlloc( nObjs );
+    Vec_IntForEachEntryStart( vAbs, Entry, i, nFrames+2 )
+        Vec_IntWriteEntry( vPresent, (Entry &  nObjMask), 1 );
+    return vPresent;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Detects how many frames are completed.]
 
   Description []
@@ -326,22 +369,17 @@ void Vta_ManAbsPrint( Vta_Man_t * p, int fThis )
   SeeAlso     []
 
 ***********************************************************************/
-Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, int nFramesStart, int nFramesMax, int nConfMax, int nTimeMax, int fVerbose )
+Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
 {
     Vta_Man_t * p;
-    assert( nFramesMax == 0 || nFramesStart <= nFramesMax );
     p = ABC_CALLOC( Vta_Man_t, 1 );
     p->pGia         = pGia;
-    p->nFramesStart = nFramesStart;    
-    p->nFramesMax   = nFramesMax;    
-    p->nConfMax     = nConfMax;
-    p->nTimeMax     = nTimeMax;
-    p->fVerbose     = fVerbose;
+    p->pPars        = pPars;
     // internal data
     p->nObjsAlloc   = (1 << 20);
     p->pObjs        = ABC_CALLOC( Vta_Obj_t, p->nObjsAlloc );
     p->nObjs        = 1;
-    p->nBins        = Gia_PrimeCudd( p->nObjsAlloc/2 );
+    p->nBins        = Abc_PrimeCudd( p->nObjsAlloc/2 );
     p->pBins        = ABC_CALLOC( int, p->nBins );
     p->vOrder       = Vec_IntAlloc( 1013 );
     // abstraction
@@ -351,17 +389,22 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, int nFramesStart, int nFramesMax, in
     p->nWords       = 1;
     p->vSeens       = Vec_IntStart( Gia_ManObjNum(pGia) * p->nWords );
     // start the abstraction
-    if ( pGia->vObjClasses )
-        p->vFrames  = Vta_ManAbsToFrames( pGia->vObjClasses );
+    if ( pGia->vObjClasses == NULL )
+        p->vFrames  = Gia_ManUnrollAbs( pGia, pPars->nFramesStart );
     else
-        p->vFrames  = Gia_ManUnrollAbs( pGia, nFramesStart );
+    {
+        p->vFrames  = Gia_VtaAbsToFrames( pGia->vObjClasses );
+        // update parameters
+        if ( pPars->nFramesStart != Vec_PtrSize(p->vFrames) )
+            printf( "Starting frame count is set in accordance with abstraction (%d).\n", Vec_PtrSize(p->vFrames) ); 
+        pPars->nFramesStart = Vec_PtrSize(p->vFrames);
+        if ( pPars->nFramesMax )
+            pPars->nFramesMax = Abc_MaxInt( pPars->nFramesMax, pPars->nFramesStart );
+    }
     // other data
     p->vCla2Var     = Vec_IntAlloc( 1000 );
     p->vCores       = Vec_PtrAlloc( 100 );
     p->pSat         = sat_solver2_new();
-
-
-
     return p;
 }
 
@@ -379,6 +422,7 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, int nFramesStart, int nFramesMax, in
 void Vga_ManStop( Vta_Man_t * p )
 {
     Vec_VecFreeP( (Vec_Vec_t **)&p->vCores );
+    Vec_VecFreeP( (Vec_Vec_t **)&p->vFrames );
     Vec_IntFreeP( &p->vSeens );
     Vec_IntFreeP( &p->vOrder );
     Vec_IntFreeP( &p->vCla2Var );
@@ -651,6 +695,26 @@ int Vta_ManComputeDepthIncrease( Vta_Obj_t ** pp1, Vta_Obj_t ** pp2 )
     return 0; 
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the object is already used.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Vta_ManObjIsUsed( Vta_Man_t * p, int iObj )
+{
+    int i;
+    unsigned * pInfo = (unsigned *)Vec_IntEntryP( p->vSeens, p->nWords * iObj );
+    for ( i = 0; i < p->nWords; i++ )
+        if ( pInfo[i] )
+            return 1;
+    return 0;
+}
 
 /**Function*************************************************************
 
@@ -701,14 +765,8 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p )
         assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
         if ( !pThis->fAdded )
         {
-            unsigned * pInfo = (unsigned *)Vec_IntEntryP( p->vSeens, p->nWords * pThis->iObj );
-            int i;
-            for ( i = 0; i < p->nWords; i++ )
-                if ( pInfo[i] )
-                    break;
             assert( pThis->Prio > 0 || pThis->Prio < VTA_LARGE );
-//            if ( Vec_IntEntry(p->vAbsAll, pThis->iObj) )
-            if ( i < p->nWords )
+            if ( Vta_ManObjIsUsed(p, pThis->iObj) )
                 Vec_PtrPush( vTermsUsed, pThis );
             else
                 Vec_PtrPush( vTermsUnused, pThis );
@@ -914,9 +972,9 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p )
     if ( pTop->Prio == 0 )
     {
         pCex = NULL;
-        pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->iFrame+1 );
+        pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 );
         pCex->iPo = 0;
-        pCex->iFrame = p->iFrame;
+        pCex->iFrame = p->pPars->iFrame;
         Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
         {
             assert( pThis->Value == VTA_VAR0 || pThis->Value == VTA_VAR1 );
@@ -972,69 +1030,18 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Vga_ManUnroll_rec( Vta_Man_t * p, int iObj, int iFrame )
+void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames )
 {
-    int iVar;
-    Gia_Obj_t * pObj;
-    Vta_Obj_t * pThis;
-//    if ( !Gia_InfoHasBit( Vta_ObjAbsOld(p, iObj), iFrame ) )
-//        return;
-    pThis = Vga_ManFindOrAdd( p, iObj, iFrame );
-    if ( !pThis->fNew )
-        return;
-    pThis->fNew = 0;
-    iVar = Vta_ObjId( p, pThis );
-    pObj = Gia_ManObj( p->pGia, iObj );
-    assert( !Gia_ObjIsCo(pObj) );
-    if ( Gia_ObjIsAnd(pObj) )
-    {
-        Vga_ManUnroll_rec( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame );
-        Vga_ManUnroll_rec( p, Gia_ObjFaninId1p(p->pGia, pObj), iFrame );
-    }
-    else if ( Gia_ObjIsRo(p->pGia, pObj) )
-    {
-        if ( iFrame == 0 )
-        {
-            pThis = Vga_ManFindOrAdd( p, iObj, -1 );
-            assert( pThis->fNew );
-            pThis->fNew = 0;
-        }
-        else
-        {
-            pObj = Gia_ObjRoToRi( p->pGia, pObj );
-            Vga_ManUnroll_rec( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame-1 );
-        }
-    }
-    else if ( Gia_ObjIsPi(p->pGia, pObj) )
-    {}
-    else if ( Gia_ObjIsConst0(pObj) )
-    {}
-    else assert( 0 );   
-    Vec_IntPush( p->vOrder, iVar );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int iFrame )
-{
-    int i, k, iObj, Entry;
     unsigned * pInfo, * pCountAll, * pCountUni;
+    int i, k, iFrame, iObj, Entry;
     // print info about frames
-    pCountAll = ABC_CALLOC( int, iFrame + 2 );
-    pCountUni = ABC_CALLOC( int, iFrame + 2 );
+    pCountAll = ABC_CALLOC( int, nFrames + 1 );
+    pCountUni = ABC_CALLOC( int, nFrames + 1 );
     Vec_IntForEachEntry( vCore, Entry, i )
     {
         iObj   = (Entry &  p->nObjMask);
         iFrame = (Entry >> p->nObjBits);
+        assert( iFrame < nFrames );
         pInfo  = (unsigned *)Vec_IntEntryP( p->vSeens, p->nWords * iObj );
         if ( Gia_InfoHasBit(pInfo, iFrame) == 0 )
         {
@@ -1046,7 +1053,7 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int iFrame )
         pCountAll[0]++;
 
         printf( "%5d%5d  ", pCountAll[0], pCountUni[0] ); 
-        for ( k = 0; k <= iFrame; k++ )
+        for ( k = 0; k < nFrames; k++ )
             printf( "%5d%5d  ", pCountAll[k+1], pCountUni[k+1] ); 
         printf( "\n" );
     }
@@ -1065,11 +1072,13 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int iFrame )
   SeeAlso     []
 
 ***********************************************************************/
-void Vga_ManAddOneSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift )
+void Vga_ManLoadSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift )
 {
-    int Entry, i;
+    int i, Entry, iObjPrev = p->nObjs;
     Vec_IntForEachEntry( vOne, Entry, i )
         Vga_ManFindOrAdd( p, Entry & p->nObjMask, (Entry >> p->nObjBits) + Lift );
+    for ( i = iObjPrev; i < p->nObjs; i++ )
+        Vga_ManAddClausesOne( p, Vta_ManObj(p, i) );
 }
 
 /**Function*************************************************************
@@ -1083,62 +1092,53 @@ void Vga_ManAddOneSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_VtaTest( Gia_Man_t * pAig, int nFramesStart, int nFramesMax, int nConfMax, int nTimeMax, int fVerbose )
+int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
 {
     Vta_Man_t * p;
-    Gia_Obj_t * pObj;
+    Vec_Int_t * vCore;
     Abc_Cex_t * pCex = NULL;
-    Vec_Int_t * vCore, * vOne;
-    int f, i, iObjPrev, RetValue, Limit;
+    int f, i, Limit, Status, RetValue = -1;
+    // preconditions
     assert( Gia_ManPoNum(pAig) == 1 );
-    pObj = Gia_ManPo( pAig, 0 );
+    assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
     // start the manager
-    p = Vga_ManStart( pAig, nFramesStart, nFramesMax, nConfMax, nTimeMax, fVerbose );
+    p = Vga_ManStart( pAig, pPars );
     // perform initial abstraction
-    for ( f = 0; f < nFramesMax; f++ )
+    for ( f = 0; f < p->pPars->nFramesMax; f++ )
     {
+        if ( p->pPars->fVerbose )
+            printf( "Frame %4d : ", f );
+        p->pPars->iFrame = f;
+        // realloc storage for abstraction marks
         if ( f == p->nWords * 32 )
             p->nWords = Vec_IntDoubleWidth( p->vSeens, p->nWords );
-        p->iFrame = f;
-        if ( fVerbose )
-            printf( "Frame %4d : ", f );
-        if ( f < nFramesStart )
+        // check this timeframe
+        if ( f < p->pPars->nFramesStart )
         {
-            // load the time frame
-            iObjPrev = p->nObjs;
-            vOne = Vec_PtrEntry( p->vFrames, f );
-            Vga_ManAddOneSlice( p, vOne, 0 );
-            for ( i = iObjPrev; i < p->nObjs; i++ )
-                Vga_ManAddClausesOne( p, Vta_ManObj(p, i) );
+            // load this timeframe
+            Vga_ManLoadSlice( p, Vec_PtrEntry(p->vFrames, f), 0 );
             // run SAT solver
-            vCore = Vta_ManUnsatCore( p->vCla2Var, p->pSat, nConfMax, fVerbose, &RetValue );
-            if ( vCore == NULL && RetValue == 0 )
+            vCore = Vta_ManUnsatCore( p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status );
+            if ( vCore == NULL && Status == 0 )
             {
                 // make sure, there was no initial abstraction (otherwise, it was invalid)
                 assert( pAig->vObjClasses == NULL );
                 // derive counter-example
                 pCex = NULL;
-                break;
             }
         }
         else
         {
             break;
 
-            Limit = Abc_MinInt(3, nFramesStart);
             // load the time frame
-            iObjPrev = p->nObjs;
+            Limit = Abc_MinInt(3, p->pPars->nFramesStart);
             for ( i = 1; i <= Limit; i++ )
-            {
-                vOne = Vec_PtrEntry( p->vCores, f-i );
-                Vga_ManAddOneSlice( p, vOne, i );
-            }
-            for ( i = iObjPrev; i < p->nObjs; i++ )
-                Vga_ManAddClausesOne( p, Vta_ManObj(p, i) );
+                Vga_ManLoadSlice( p, Vec_PtrEntry(p->vCores, f-i), i );
             // iterate as long as there are counter-examples
             while ( 1 )
             {
-                vCore = Vta_ManUnsatCore( p->vCla2Var, p->pSat, nConfMax, fVerbose, &RetValue );
+                vCore = Vta_ManUnsatCore( p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &RetValue );
                 if ( RetValue ) // resource limit is reached
                 {
                     assert( vCore == NULL );
@@ -1157,24 +1157,33 @@ void Gia_VtaTest( Gia_Man_t * pAig, int nFramesStart, int nFramesMax, int nConfM
         }
         if ( pCex != NULL )
         {
-            // the problem is SAT
+            printf( "True CEX is detected.\n" );
+            RetValue = 0;
+            break;
         }
         if ( vCore == NULL )
         {
-            // resource limit is reached
+            printf( "Resource limit is exhausted.\n" );
+            RetValue = -1;
+            break;
         }
         // add the core
+        Vta_ManUnsatCoreRemap( p, vCore );
         Vec_PtrPush( p->vCores, vCore );
         // print the result
-        if ( fVerbose )
+        if ( p->pPars->fVerbose )
             Vta_ManAbsPrintFrame( p, vCore, f );
     }
-    assert( Vec_PtrSize(p->vCores) > 0 );
-    if ( pAig->vObjClasses != NULL )
-        printf( "Replacing the old abstraction by a new one.\n" );
-    Vec_IntFreeP( &pAig->vObjClasses );
-    pAig->vObjClasses = Vta_ManFramesToAbs( (Vec_Vec_t *)p->vCores );
+    if ( pCex == NULL )
+    {
+        assert( Vec_PtrSize(p->vCores) > 0 );
+        if ( pAig->vObjClasses != NULL )
+            printf( "Replacing the old abstraction by a new one.\n" );
+        Vec_IntFreeP( &pAig->vObjClasses );
+        pAig->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
+    }
     Vga_ManStop( p );
+    return RetValue;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 13cfad9c..da3a71ce 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -383,6 +383,7 @@ static int Abc_CommandAbc9AbsPba             ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9GlaDerive          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9GlaCba             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9GlaPba             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Vta                ( 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 );
@@ -841,6 +842,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&gla_derive",   Abc_CommandAbc9GlaDerive,    0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&gla_cba",      Abc_CommandAbc9GlaCba,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&gla_pba",      Abc_CommandAbc9GlaPba,       0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&vta",          Abc_CommandAbc9Vta,          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 );
@@ -29457,6 +29459,122 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_ParVta_t Pars, * pPars = &Pars;
+    int c;
+    Gia_VtaSetDefaultParams( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFramesStart = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFramesStart < 0 ) 
+                goto usage;
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFramesMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFramesMax < 0 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nConfLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nConfLimit < 0 ) 
+                goto usage;
+            break;
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nTimeOut = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nTimeOut < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9AbsCba(): There is no AIG.\n" );
+        return 1;
+    } 
+    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
+    {
+        Abc_Print( -1, "The network is combinational.\n" );
+        return 0;
+    }
+    if ( Gia_ManPoNum(pAbc->pGia) > 1 )
+    {
+        Abc_Print( 1, "The network is more than one PO (run \"orpos\").\n" );
+        return 0;
+    }
+    if ( pPars->nFramesMax > 0 )
+    {
+        Abc_Print( 1, "The number of starting frames should be a positive integer.\n" );
+        return 0;
+    }
+    if ( pPars->nFramesMax && pPars->nFramesStart > pPars->nFramesMax )
+    {
+        Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" );
+        return 0;
+    }
+    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 [-SFCT num] [-vh]\n" );
+    Abc_Print( -2, "\t         refines abstracted object map with proof-based abstraction\n" );
+    Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart );
+    Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
+    Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit );
+    Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
+    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;
+} 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Reparam( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp = NULL;
@@ -30330,7 +30448,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fSwitch = 0;
 //    extern Gia_Man_t * Gia_VtaTest( Gia_Man_t * p );
 //    extern int Gia_ManSuppSizeTest( Gia_Man_t * p );
-    extern void Gia_VtaTest( Gia_Man_t * p, int nFramesStart, int nFramesMax, int nConfMax, int nTimeMax, int fVerbose );
+//    extern void Gia_VtaTest( Gia_Man_t * p, int nFramesStart, int nFramesMax, int nConfMax, int nTimeMax, int fVerbose );
 
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
@@ -30368,7 +30486,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Gia_ManStopP( &pTemp );
 //    Gia_ManSuppSizeTest( pAbc->pGia );
 
-    Gia_VtaTest( pAbc->pGia, 10, 100000, 0, 0, 1 );
+//    Gia_VtaTest( pAbc->pGia, 10, 100000, 0, 0, 1 );
     return 0;
 usage:
     Abc_Print( -2, "usage: &test [-svh]\n" );