Tuning SAT solver for QBF instances.

src/base/abci/abc.c

@@ -21828,7 +21828,8 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( argc == globalUtilOptind + 1 )
     {
-        extern int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int fVerbose );
+        int * pModel = NULL;
+        extern int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int ** ppModel );
         // get the input file name
         char * pFileName = argv[globalUtilOptind];
         FILE * pFile = fopen( pFileName, "rb" );
@@ -21838,10 +21839,18 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 0;
         }
         fclose( pFile );
-        Cnf_DataSolveFromFile( pFileName, nConfLimit, fVerbose );
+        Cnf_DataSolveFromFile( pFileName, nConfLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fVerbose, &pModel );
+        if ( pModel && pNtk )
+        {
+            int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pModel );
+            if ( pSimInfo[0] != 1 )
+                Abc_Print( 1, "ERROR in Abc_NtkMiterSat(): Generated counter example is invalid.\n" );
+            ABC_FREE( pSimInfo );
+            pAbc->pCex = Abc_CexCreate( 0, Abc_NtkPiNum(pNtk), pNtk->pModel, 0, 0, 0 );
+        }
+        ABC_FREE( pModel );
         return 0;
     }
-
     if ( pNtk == NULL )
     {
         Abc_Print( -1, "Empty network.\n" );

src/proof/fra/fraCec.c

@@ -194,7 +194,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
         }
 
         if ( nLearnedStart )
-            pSat->nLearntStart = nLearnedStart;
+            pSat->nLearntStart = pSat->nLearntMax = nLearnedStart;
         if ( nLearnedDelta )
             pSat->nLearntDelta = nLearnedDelta;
         if ( nLearnedPerce )

src/sat/cnf/cnfUtil.c

@@ -399,7 +399,7 @@ finish:
   SeeAlso     []
 
 ***********************************************************************/
-int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int fVerbose )
+int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int ** ppModel )
 {
     abctime clk = Abc_Clock();
     Cnf_Dat_t * pCnf = Cnf_DataReadFromFile( pFileName );
@@ -420,9 +420,15 @@ int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int fVerbose )
         printf( "The problem is trivially UNSAT.\n" );
         return 1;
     }
+    if ( nLearnedStart )
+        pSat->nLearntStart = pSat->nLearntMax = nLearnedStart;
+    if ( nLearnedDelta )
+        pSat->nLearntDelta = nLearnedDelta;
+    if ( nLearnedPerce )
+        pSat->nLearntRatio = nLearnedPerce;
+    if ( fVerbose )
+        pSat->fVerbose = fVerbose;
     // solve the miter
-//    if ( fVerbose )
-//        pSat->verbosity = 1;
     status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( status == l_Undef )
         RetValue = -1;