Adding APIs to mark cones. Creating test-bench for incremental solving &satoko -i.

2 files changed, 12 insertions, 8 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f10be02b..bb0b8c8d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -23410,13 +23410,13 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Satoko( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Gia_ManCallSatoko( Gia_Man_t * p, satoko_opts_t * opts, int fSplit );
-    int c, fSplit = 0;
+    extern void Gia_ManSatokoCall( Gia_Man_t * p, satoko_opts_t * opts, int fSplit, int fIncrem );
+    int c, fSplit = 0, fIncrem = 0;
 
     satoko_opts_t opts;
     satoko_default_opts(&opts);
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Csvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Csivh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -23434,6 +23434,9 @@ int Abc_CommandAbc9Satoko( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 's':
             fSplit ^= 1;
             break;
+        case 'i':
+            fIncrem ^= 1;
+            break;
         case 'v':
             opts.verbose ^= 1;
             break;
@@ -23449,13 +23452,14 @@ int Abc_CommandAbc9Satoko( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Satoko(): There is no AIG.\n" );
         return 1;
     }
-    Gia_ManCallSatoko( pAbc->pGia, &opts, fSplit );
+    Gia_ManSatokoCall( pAbc->pGia, &opts, fSplit, fIncrem );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &satoko [-C num] [-svh]\n" );
+    Abc_Print( -2, "usage: &satoko [-C num] [-sivh]\n" );
     Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n", opts.conf_limit );
     Abc_Print( -2, "\t-s     : split multi-output miter into individual outputs [default = %s]\n", fSplit? "yes": "no" );
+    Abc_Print( -2, "\t-i     : split multi-output miter and solve incrementally [default = %s]\n", fIncrem? "yes": "no" );
     Abc_Print( -2, "\t-v     : prints verbose information [default = %s]\n", opts.verbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/cmd/cmdAuto.c b/src/base/cmd/cmdAuto.c
index e279b19d..8151c2e5 100644
--- a/src/base/cmd/cmdAuto.c
+++ b/src/base/cmd/cmdAuto.c
@@ -47,7 +47,7 @@ ABC_NAMESPACE_IMPL_START
 #define CMD_AUTO_LINE_MAX 1000  // max number of chars in the string
 #define CMD_AUTO_ARG_MAX   100  // max number of arguments in the call
 
-extern int Gia_ManCallSatokoOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput );
+extern int Gia_ManSatokoCallOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -92,7 +92,7 @@ int Cmd_RunAutoTunerEvalSimple( Vec_Ptr_t * vAigs, satoko_opts_t * pOpts )
     //printf( "Tuning with options: " );
     //Cmd_RunAutoTunerPrintOptions( pOpts );
     Vec_PtrForEachEntry( Gia_Man_t *, vAigs, pGia, i )
-        TotalCost += Gia_ManCallSatokoOne( pGia, pOpts, -1 );
+        TotalCost += Gia_ManSatokoCallOne( pGia, pOpts, -1 );
     return TotalCost;
 }
 
@@ -142,7 +142,7 @@ void * Cmd_RunAutoTunerEvalWorkerThread( void * pArg )
             assert( 0 );
             return NULL;
         }
-        pThData->Result = Gia_ManCallSatokoOne( pThData->pGia, pThData->pOpts, -1 );
+        pThData->Result = Gia_ManSatokoCallOne( pThData->pGia, pThData->pOpts, -1 );
         pThData->fWorking = 0;
     }
     assert( 0 );