Variable timeframe abstraction.

abc.rc

@@ -118,6 +118,7 @@ alias drwsat2     "st; drw; b -l; drw; drf; ifraig -C 20; drw; b -l; drw; drf"
 alias share       "st; multi -m; fx; resyn2"
 alias addinit     "read_init; undc; strash; zero"
 alias blif2aig    "undc; strash; zero"
+alias v2p         "&vta_gla; &ps; &gla_derive; &put; w 1.aig; pdr -v"
 
 # resubstitution scripts for the IWLS paper
 alias src_rw      "st; rw -l; rwz -l; rwz -l" 

src/aig/gia/gia.h

@@ -209,6 +209,7 @@ struct Gia_ParVta_t_
     int            nTimeOut;      // timeout in seconds
     int            nRatioMin;     // stop when less than this % of object is abstracted
     int            fUseTermVars;  // use terminal variables
+    int            fUseRollback;  // use rollback to the starting number of frames
     int            fVerbose;      // verbose flag
     int            iFrame;        // the number of frames covered 
 };

src/aig/gia/giaAbsVta.c

@@ -59,6 +59,7 @@ struct Vta_Man_t_
     unsigned      nObjMask;     // object mask
     Vec_Ptr_t *   vFrames;      // start abstraction for each frame
     int           nWords;       // the number of words in the record
+    int           nCexes;       // the number of CEXes
     Vec_Int_t *   vSeens;       // seen objects
     Vec_Bit_t *   vSeenGla;     // seen objects in all frames
     int           nSeenGla;     // seen objects in all frames
@@ -154,6 +155,7 @@ void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
     p->nTimeOut      =      0;   // timeout in seconds
     p->nRatioMin     =     10;   // stop when less than this % of object is abstracted
     p->fUseTermVars  =      1;   // use terminal variables
+    p->fUseRollback  =      0;   // use rollback to the starting number of frames
     p->fVerbose      =      0;   // verbose flag
     p->iFrame        =     -1;   // the number of frames covered 
 }
@@ -969,8 +971,6 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
             if ( !Gia_ObjIsPi(p->pGia, pObj) )
                 Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
         sat_solver2_simplify( p->pSat );
-
-//        printf( "VecCla grew to %d.       \n\n", Vec_IntSize(p->vCla2Var) );
     }
     Vec_IntFree( vTermsToAdd );
     return pCex;
@@ -1049,8 +1049,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 )
-        printf( "SAT solver:  Variables = %d. Clauses = %d. Conflicts = %d.\n", 
-            sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat) );
+        printf( "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 );
 
     Vec_VecFreeP( (Vec_Vec_t **)&p->vCores );
     Vec_VecFreeP( (Vec_Vec_t **)&p->vFrames );
@@ -1399,12 +1399,12 @@ void Vga_ManRollBack( Vta_Man_t * p, int nObjOld )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
+int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
 {
     Vta_Man_t * p;
     Vec_Int_t * vCore;
     Abc_Cex_t * pCex = NULL;
-    int i, f, nConfls, Status, RetValue = -1;
+    int i, f, nConfls, Status, nObjOld, RetValue = -1;
     int clk = clock(), clk2;
     // preconditions
     assert( Gia_ManPoNum(pAig) == 1 );
@@ -1437,13 +1437,11 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
         {
             Vga_ManAddClausesOne( p, 0, f );
             Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
-
-//            printf( "VecCla grew ttto %d.        \n\n", Vec_IntSize(p->vCla2Var) );
         }
         else
         {
             // create bookmark to be used for rollback
-            int nObjOld = p->nObjs;
+            nObjOld = p->nObjs;
 //            sat_solver2_reducedb( p->pSat );
             sat_solver2_bookmark( p->pSat );
             Vec_IntClear( p->vAddedNew );
@@ -1465,12 +1463,16 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                 }
                 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
                 if ( p->pPars->fVerbose )
                     Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk );
@@ -1501,6 +1503,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
             // make sure, there was no initial abstraction (otherwise, it was invalid)
             assert( pAig->vObjClasses == NULL && f < p->pPars->nFramesStart );
             pCex = Vga_ManDeriveCex( p );
+            RetValue = 0;
             break;
         }
         // add the core
@@ -1548,6 +1551,7 @@ finish:
         if ( !Gia_ManVerifyCex( p->pGia, pCex, 0 ) )
             printf( "    Gia_VtaPerform(): CEX verification has failed!\n" );
         printf( "Counter-example detected in frame %d.  ", f );
+        p->pPars->iFrame = pCex->iFrame - 1;
     }
     Abc_PrintTime( 1, "Time", clock() - clk );
 
@@ -1559,11 +1563,36 @@ finish:
     ABC_PRTP( "TOTAL       ", clock() - clk, clock() - clk );
 
     Vga_ManStop( p );
-
     fflush( stdout );
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Collect nodes/flops involved in different timeframes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
+{
+    int RetValue = -1;
+    if ( pAig->vObjClasses == NULL && pPars->fUseRollback )
+    {
+        int nFramesMaxOld = pPars->nFramesMax;
+        pPars->nFramesMax = pPars->nFramesStart;
+        RetValue = Gia_VtaPerformInt( pAig, pPars );
+        pPars->nFramesMax = nFramesMaxOld;
+    }
+    if ( RetValue == 0 )
+        return RetValue;
+    return Gia_VtaPerformInt( pAig, pPars );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abci/abc.c

@@ -26723,7 +26723,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, "FSPCLTRtvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRtrvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -26807,6 +26807,9 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 't':
             pPars->fUseTermVars ^= 1;
             break;
+        case 'r':
+            pPars->fUseRollback ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -26841,13 +26844,18 @@ 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;
+    }
     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] [-tvh]\n" );
+    Abc_Print( -2, "usage: &vta [-FSPCLTR num] [-trvh]\n" );
     Abc_Print( -2, "\t         refines abstracted object map with proof-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 );
@@ -26857,6 +26865,7 @@ usage:
     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-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-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;