Adding preprocessing to command &splitsat.

src/base/abci/abc.c

@@ -46097,10 +46097,10 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9SplitSat( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Cnf_SplitSat( char * pFileName, int iVarBeg, int iVarEnd, int nLits, int Value, int TimeOut, int nProcs, int nIters, int Seed, int fVerbose );
-    int c, iVarBeg = 0, iVarEnd = ABC_INFINITY, nLits = 10, Value = 2, TimeOut = 5, nProcs = 1, nIters = 1, Seed = 0, fVerbose = 0; char * pFileName = NULL;
+    extern void Cnf_SplitSat( char * pFileName, int iVarBeg, int iVarEnd, int nLits, int Value, int TimeOut, int nProcs, int nIters, int Seed, int fPrepro, int fVerbose );
+    int c, iVarBeg = 0, iVarEnd = ABC_INFINITY, nLits = 10, Value = 2, TimeOut = 5, nProcs = 1, nIters = 1, Seed = 0, fPrepro = 0, fVerbose = 0; char * pFileName = NULL;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "BENVTPISvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "BENVTPISpvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -46192,6 +46192,9 @@ int Abc_CommandAbc9SplitSat( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( Seed < 0 )
                 goto usage;
             break;            
+        case 'p':
+            fPrepro ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -46218,11 +46221,11 @@ int Abc_CommandAbc9SplitSat( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
         fclose( pFile );
     }
-    Cnf_SplitSat( pFileName, iVarBeg, iVarEnd, nLits, Value, TimeOut, nProcs, nIters, Seed, fVerbose );
+    Cnf_SplitSat( pFileName, iVarBeg, iVarEnd, nLits, Value, TimeOut, nProcs, nIters, Seed, fPrepro, fVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &splitsat [-BENVTPIS num] [-vh]\n" );
+    Abc_Print( -2, "usage: &splitsat [-BENVTPIS num] [-pvh]\n" );
     Abc_Print( -2, "\t         solves CNF-based SAT problem by randomized case-splitting\n" );
     Abc_Print( -2, "\t-B num : the first CNF variable to use for splitting [default = %d]\n",         iVarBeg );
     Abc_Print( -2, "\t-E num : the last CNF variable to use for splitting [default = %d]\n",          iVarEnd );
@@ -46232,6 +46235,7 @@ usage:
     Abc_Print( -2, "\t-P num : the number of concurrent processes [default = %d]\n",                  nProcs );
     Abc_Print( -2, "\t-I num : the max number of iterations (0 = infinity) [default = %d]\n",         nIters );
     Abc_Print( -2, "\t-S num : the random seed used to generate cofactors [default = %d]\n",          Seed );    
+    Abc_Print( -2, "\t-p     : toggle using SatELIte (http://minisat.se/SatELite.html) [default = %s]\n", fPrepro? "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;

src/sat/cnf/cnfUtil.c

@@ -74,11 +74,15 @@ Vec_Int_t *Cnf_RunSolverOnce(int Id, int Rand, int TimeOut, int fVerbose)
     else
         sprintf(pCommand, "%s --seed=%d %s %s > %s", pKissat, Rand, fVerboseSolver ? "" : "-q", FileNameIn, FileNameOut);
     //printf( "Thread command: %s\n", pCommand);
-    if (system(pCommand) == -1) {
-        fprintf(stdout, "Command \"%s\" did not succeed.\n", pCommand);
-        return 0;
+    FILE * pFile = fopen(FileNameIn, "rb");
+    if ( pFile != NULL ) {
+        fclose( pFile );
+        if (system(pCommand) == -1) {
+            fprintf(stdout, "Command \"%s\" did not succeed.\n", pCommand);
+            return 0;
+        }
+        vRes = Exa4_ManParse(FileNameOut); // FileNameOut is removed here
     }
-    vRes = Exa4_ManParse(FileNameOut); // FileNameOut is removed here
     if (fVerbose) {
         double SolvingTime = ((double)(Abc_Clock() - clkTotal))/((double)CLOCKS_PER_SEC);
         if (vRes)
@@ -741,7 +745,7 @@ Vec_Int_t *Cnf_GenRandLits(int iVarBeg, int iVarEnd, int nLits, int Value, int R
     fflush(stdout);
     return vLits;
 }
-void Cnf_SplitCnfFile(char * pFileName, int nParts, int iVarBeg, int iVarEnd, int nLits, int Value, int Rand, int fVerbose)
+void Cnf_SplitCnfFile(char * pFileName, int nParts, int iVarBeg, int iVarEnd, int nLits, int Value, int Rand, int fPrepro, int fVerbose)
 {
     Cnf_Dat_t *p = Cnf_DataReadFromFile(pFileName); int k;
     if (iVarEnd == ABC_INFINITY)
@@ -751,7 +755,18 @@ void Cnf_SplitCnfFile(char * pFileName, int nParts, int iVarBeg, int iVarEnd, in
         Vec_Int_t *vLits = Cnf_GenRandLits(iVarBeg, iVarEnd, nLits, Value, Rand, fVerbose);
         Cnf_Dat_t *pCnf = Cnf_DataDupCofArray(p, vLits);
         char FileName[100];  sprintf(FileName, "%02d.cnf", k);
-        Cnf_DataWriteIntoFile(pCnf, FileName, 0, NULL, NULL);
+        if ( fPrepro ) {
+            char Command[1000];   
+            sprintf(Command, "satelite --verbosity=0 -pre temp.cnf %s", FileName);
+            Cnf_DataWriteIntoFile(pCnf, "temp.cnf", 0, NULL, NULL);
+            if (system(Command) == -1) {
+                fprintf(stdout, "Command \"%s\" did not succeed. Preprocessing skipped.\n", Command);
+                Cnf_DataWriteIntoFile(pCnf, FileName, 0, NULL, NULL);
+            }
+            unlink("temp.cnf");
+        }
+        else 
+            Cnf_DataWriteIntoFile(pCnf, FileName, 0, NULL, NULL);
         Cnf_DataFree(pCnf);
         Vec_IntFree(vLits);
     }    
@@ -765,7 +780,7 @@ void Cnf_SplitCnfCleanup(int nParts)
         unlink(FileName);
     }   
 }
-void Cnf_SplitSat(char *pFileName, int iVarBeg, int iVarEnd, int nLits, int Value, int TimeOut, int nProcs, int nIters, int Seed, int fVerbose)
+void Cnf_SplitSat(char *pFileName, int iVarBeg, int iVarEnd, int nLits, int Value, int TimeOut, int nProcs, int nIters, int Seed, int fPrepro, int fVerbose)
 {
     abctime clk = Abc_Clock();
     Vec_Int_t *vSol = NULL;
@@ -778,9 +793,14 @@ void Cnf_SplitSat(char *pFileName, int iVarBeg, int iVarEnd, int nLits, int Valu
     Rand = Abc_Random(0);
     for (i = 0; i < nIters && !vSol; i++)
     {
-        Cnf_SplitCnfFile(pFileName, nProcs, iVarBeg, iVarEnd, nLits, Value, Rand, fVerbose);
+        abctime clk2 = Abc_Clock();
+        Cnf_SplitCnfFile(pFileName, nProcs, iVarBeg, iVarEnd, nLits, Value, Rand, fPrepro, fVerbose);
         vSol = Cnf_RunSolver(nProcs, TimeOut, fVerbose);
         Cnf_SplitCnfCleanup(nProcs);
+        if (fVerbose) {
+            printf( "Finished iteration %d.  ", i);    
+            Abc_PrintTime(0, "Time", Abc_Clock() - clk2);
+        }
     }
     printf("%solution is found.  ", vSol ? "S" : "No s");
     Abc_PrintTime(0, "Total time", Abc_Clock() - clk);