Adding conflict limit and timeout to &simap.

Author: alanminko

src/aig/gia/giaSatLut.c

@@ -1233,7 +1233,7 @@ void Gia_ManLutSat( Gia_Man_t * pGia, int LutSize, int nNumber, int nImproves, i
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int TimeOut, int fVerbose )
+Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int nBTLimit, int TimeOut, int fVerbose )
 {
     extern Vec_Int_t * Exa4_ManParse( char *pFileName );
     int fVerboseSolver = 0;
@@ -1245,10 +1245,18 @@ Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int TimeOut
     char * pKadical = "kadical";
 #endif
     char Command[1000], * pCommand = (char *)&Command;
-    if ( TimeOut )
-        sprintf( pCommand, "%s -t %d %s %s > %s", pKadical, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
-    else
-        sprintf( pCommand, "%s %s %s > %s", pKadical, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
+    if ( nBTLimit ) {
+        if ( TimeOut )
+            sprintf( pCommand, "%s -c %d -t %d %s %s > %s", pKadical, nBTLimit, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
+        else
+            sprintf( pCommand, "%s -c %d  %s %s > %s", pKadical, nBTLimit, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
+    }
+    else {
+        if ( TimeOut )
+            sprintf( pCommand, "%s -t %d %s %s > %s", pKadical, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
+        else
+            sprintf( pCommand, "%s %s %s > %s", pKadical, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
+    }
 #ifdef __wasm
     if ( 1 )
 #else
@@ -1266,7 +1274,7 @@ Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int TimeOut
         else if ( vRes == NULL && TimeOut == 0 )
             printf( "The problem has no solution. " );
         else if ( vRes == NULL )
-            printf( "The problem has no solution or timed out after %d sec. ", TimeOut );
+            printf( "The problem has no solution or reached a resource limit after %d sec. ", TimeOut );
         Abc_PrintTime( 1, "SAT solver time", Abc_Clock() - clkTotal );
     }
     return vRes;
@@ -1527,7 +1535,7 @@ int Gia_ManDumpCnf( char * pFileName, Vec_Str_t * vStr, int nVars )
     fclose( pFile );
     return 1;
 }
-int Gia_ManSimpleMapping( Gia_Man_t * p, int nBTLimit, int nBound, int fVerbose )
+int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int nBTLimit, int nTimeout, int fVerbose )
 {
     char * pFileNameI = (char *)"__temp__.cnf"; 
     char * pFileNameO = (char *)"__temp__.out";
@@ -1540,11 +1548,12 @@ int Gia_ManSimpleMapping( Gia_Man_t * p, int nBTLimit, int nBound, int fVerbose
         return 0;
     }
     if ( fVerbose )
-        printf( "SAT variables = %d. SAT clauses = %d. Cardinality bound = %d.\n", nVars, Vec_StrCountEntry(vStr, '\n'), nBound );
+        printf( "SAT variables = %d. SAT clauses = %d. Cardinality bound = %d. Conflict limit = %d. Timeout = %d.\n", 
+            nVars, Vec_StrCountEntry(vStr, '\n'), nBound, nBTLimit, nTimeout );
     //char pFileName[100]; sprintf( pFileName, "temp%02d.cnf", nBound/2 );
     //Gia_ManDumpCnf( pFileName, vStr, nVars );
     Vec_StrFree( vStr );
-    Vec_Int_t * vRes = Gia_RunKadical( pFileNameI, pFileNameO, 0, 1 );
+    Vec_Int_t * vRes = Gia_RunKadical( pFileNameI, pFileNameO, nBTLimit, nTimeout, 1 );
     unlink( pFileNameI );
     //unlink( pFileNameO );
     if ( vRes == NULL )

src/base/abci/abc.c

@@ -44383,13 +44383,27 @@ int Abc_CommandAbc9Of( Abc_Frame_t * pAbc, int argc, char ** argv )
 int Abc_CommandAbc9Simap( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Mio_IntallSimpleLibrary();
-    extern int Gia_ManSimpleMapping( Gia_Man_t * p, int nBTLimit, int nBound, int fVerbose );
-    int c, nBTLimit = 0, nBound = 0, fVerbose = 0;
+    extern int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int nBTLimit, int nTimeout, int fVerbose );
+    int c, nBTLimit = 0, nBound = 0, nTimeout = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CBvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "BCTvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'B':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nBound = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nBound < 0 )
+            {
+                Abc_Print( -1, "Bound on a solution should be a positive integer.\n" );
+                goto usage;
+            }
+            break;
         case 'C':
             if ( globalUtilOptind >= argc )
             {
@@ -44404,20 +44418,15 @@ int Abc_CommandAbc9Simap( Abc_Frame_t * pAbc, int argc, char ** argv )
                 goto usage;
             }
             break;
-        case 'B':
+        case 'T':
             if ( globalUtilOptind >= argc )
             {
-                Abc_Print( -1, "Command line switch \"-N\" should be followed by a positive integer.\n" );
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by a positive integer.\n" );
                 goto usage;
             }
-            nBound = atoi(argv[globalUtilOptind]);
+            nTimeout = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nBound < 0 )
-            {
-                Abc_Print( -1, "Bound on a solution should be a positive integer.\n" );
-                goto usage;
-            }
-            break;
+            break;            
         case 'v':
             fVerbose ^= 1;
             break;
@@ -44432,15 +44441,16 @@ int Abc_CommandAbc9Simap( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     Mio_IntallSimpleLibrary();
-    if ( !Gia_ManSimpleMapping( pAbc->pGia, nBTLimit, nBound, fVerbose ) )
+    if ( !Gia_ManSimpleMapping( pAbc->pGia, nBound, nBTLimit, nTimeout, fVerbose ) )
         printf( "Simple mapping has failed.\n" );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &simap [-CB num] [-vh]\n" );
+    Abc_Print( -2, "usage: &simap [-BCT num] [-vh]\n" );
     Abc_Print( -2, "\t           performs simple mapping of the AIG\n" );
-    Abc_Print( -2, "\t-C num   : the conflict limit [default = %d]\n", nBTLimit );
     Abc_Print( -2, "\t-B num   : the bound on the solution size [default = %d]\n", nBound );
+    Abc_Print( -2, "\t-C num   : the conflict limit [default = %d]\n", nBTLimit );
+    Abc_Print( -2, "\t-T num   : runtime limit in seconds [default = %d]\n", nTimeout );    
     Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : prints the command usage\n");
     return 1;