Updating &gla_refine to perform suffic refinement.

1 files changed, 18 insertions, 5 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 25c77048..f24f9e12 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27820,14 +27820,26 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9GlaRefine( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose );
+    extern int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int fVerbose );
+    int iFrameStart = 0;
     int fMinCut = 1;
     int c, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Fmvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            iFrameStart = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( iFrameStart < 0 ) 
+                goto usage;
+            break;
         case 'm':
             fMinCut ^= 1;
             break;
@@ -27855,14 +27867,15 @@ int Abc_CommandAbc9GlaRefine( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9GlaRefine(): There is no counter-example.\n" );
         return 1;
     } 
-    pAbc->Status = Gia_ManGlaRefine( pAbc->pGia, pAbc->pCex, fMinCut, fVerbose );
+    pAbc->Status = Gia_ManNewRefine( pAbc->pGia, pAbc->pCex, iFrameStart, fVerbose );
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &gla_refine [-mvh]\n" );
+    Abc_Print( -2, "usage: &gla_refine [-F num] [-vh]\n" );
     Abc_Print( -2, "\t         refines the pre-computed gate map using the counter-example\n" );
-    Abc_Print( -2, "\t-m     : toggle using min-cut to derive the refinements [default = %s]\n", fMinCut? "yes": "no" );
+    Abc_Print( -2, "\t-F num : starting timeframe for suffix refinement [default = %d]\n", iFrameStart );
+//    Abc_Print( -2, "\t-m     : toggle using min-cut to derive the refinements [default = %s]\n", fMinCut? "yes": "no" );
     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;