Variable timeframe abstraction.

3 files changed, 36 insertions, 6 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 3a0fb150..803fff51 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -206,6 +206,7 @@ struct Gia_ParVta_t_
     int            nFramesOver;   // overlap frames
     int            nConfLimit;    // conflict limit
     int            nTimeOut;      // timeout in seconds
+    int            nRatioMin;     // stop when less than this % of object is abstracted
     int            fUseTermVars;  // use terminal variables
     int            fVerbose;      // verbose flag
     int            iFrame;        // the number of frames covered 
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 21e31cd2..09ed91ab 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -146,10 +146,11 @@ void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
 {
     memset( p, 0, sizeof(Gia_ParVta_t) );
     p->nFramesStart  =    5;   // starting frame 
-    p->nFramesOver   =    2;   // overlap frames
+    p->nFramesOver   =    4;   // overlap frames
     p->nFramesMax    =    0;   // maximum frames
     p->nConfLimit    =    0;   // conflict limit
     p->nTimeOut      =    0;   // timeout in seconds
+    p->nRatioMin     =   10;   // stop when less than this % of object is abstracted
     p->fUseTermVars  =    0;   // use terminal variables
     p->fVerbose      =    0;   // verbose flag
     p->iFrame        =   -1;   // the number of frames covered 
@@ -647,6 +648,7 @@ void Vta_ManSatVerify( Vta_Man_t * p )
 ***********************************************************************/
 Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
 {
+    int fVerify = 0;
     Abc_Cex_t * pCex = NULL;
     Vec_Int_t * vOrder, * vTermsToAdd;
     Vec_Ptr_t * vTermsUsed, * vTermsUnused;
@@ -654,6 +656,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
     Gia_Obj_t * pObj;
     int i, Counter;
 
+    if ( fVerify )
     Vta_ManSatVerify( p );
 
     // collect nodes in a topological order
@@ -666,6 +669,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
     }
 
     // verify
+    if ( fVerify )
     Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
     {
         if ( !pThis->fAdded )
@@ -884,6 +888,8 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
     }
 
 
+    if ( fVerify )
+    {
     // verify
     Vta_ManForEachObjVec( vOrder, p, pThis, i )
         pThis->Value = VTA_VARX;
@@ -948,6 +954,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
         printf( "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" );
 //    else
 //        printf( "Verification OK.\n" );
+    }
 
 
     // produce true counter-example
@@ -1400,8 +1407,10 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
     // perform initial abstraction
     if ( p->pPars->fVerbose )
     {
-        printf( "Running VTA with FrameStart = %d  FramePast = %d  FrameMax = %d  Conf = %d  Timeout = %d.\n", 
-            p->pPars->nFramesStart, p->pPars->nFramesOver, p->pPars->nFramesMax, p->pPars->nConfLimit, p->pPars->nTimeOut );
+        printf( "Running variable-timeframe abstraction (VTA) with the following parameters:\n" );
+        printf( "FrameStart = %d  FramePast = %d  FrameMax = %d  Conf = %d  Timeout = %d. RatioMin = %d %%.\n", 
+            p->pPars->nFramesStart, p->pPars->nFramesOver, p->pPars->nFramesMax, 
+            p->pPars->nConfLimit, p->pPars->nTimeOut, pPars->nRatioMin );
         printf( "Frame   Abs   Confl  Cex   Core   F0   F1   F2   F3  ...\n" );
     }
     for ( f = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
@@ -1489,6 +1498,12 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
         // print the result
         if ( p->pPars->fVerbose )
             Vta_ManAbsPrintFrame( p, vCore, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk );
+        // chech if the number of objects is below limit
+        if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 )
+        {
+            Status = -1;
+            break;
+        }
     }
 finish:
     // analize the results
@@ -1505,8 +1520,10 @@ finish:
                 printf( "SAT solver ran out of time at %d sec in frame %d.  ", p->pPars->nTimeOut, f );
             else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
                 printf( "SAT solver ran out of resources at %d conflicts in frame %d.  ", pPars->nConfLimit, f );
+            else if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 )
+                printf( "Percentage of abstracted objects is less than %d in frame %d.  ", pPars->nRatioMin, f );
             else
-                printf( "SAT solver ran out of resources in frame %d.  ", f );
+                printf( "Abstraction stopped for unknown reason in frame %d.  ", f );
         }
         else
             printf( "SAT solver completed %d frames and produced an abstraction.  ", f );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 477adf06..6b8f117b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -26711,7 +26711,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, "SFPCTtvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFPCTRtvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -26770,6 +26770,17 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nTimeOut < 0 ) 
                 goto usage;
             break;
+        case 'R':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nRatioMin = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nRatioMin < 0 ) 
+                goto usage;
+            break;
         case 't':
             pPars->fUseTermVars ^= 1;
             break;
@@ -26813,13 +26824,14 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &vta [-SFPCT num] [-tvh]\n" );
+    Abc_Print( -2, "usage: &vta [-SFPCTR num] [-tvh]\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-P num : the number of previous frames for UNSAT core [default = %d]\n", pPars->nFramesOver );
     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-R num : stop when less than this %% of object is abstracted (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-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");