From fdf00d8044661738aac2eed776520f5511d32607 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 18 Sep 2015 08:38:53 -0700
Subject: Tuning SAT solver for QBF instances.

---
 src/sat/cnf/cnfUtil.c | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

(limited to 'src/sat/cnf')

diff --git a/src/sat/cnf/cnfUtil.c b/src/sat/cnf/cnfUtil.c
index 7900b08c..a5037718 100644
--- a/src/sat/cnf/cnfUtil.c
+++ b/src/sat/cnf/cnfUtil.c
@@ -399,12 +399,12 @@ finish:
   SeeAlso     []
 
 ***********************************************************************/
-int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int ** ppModel )
+int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int ** ppModel, int nPis )
 {
     abctime clk = Abc_Clock();
     Cnf_Dat_t * pCnf = Cnf_DataReadFromFile( pFileName );
     sat_solver * pSat;
-    int status, RetValue = -1;
+    int i, status, RetValue = -1;
     if ( pCnf == NULL )
         return -1;
     if ( fVerbose )
@@ -414,10 +414,10 @@ int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart,
     }
     // convert into SAT solver
     pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
-    Cnf_DataFree( pCnf );
     if ( pSat == NULL )
     {
         printf( "The problem is trivially UNSAT.\n" );
+        Cnf_DataFree( pCnf );
         return 1;
     }
     if ( nLearnedStart )
@@ -440,7 +440,6 @@ int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart,
         assert( 0 );
     if ( fVerbose )
         Sat_SolverPrintStats( stdout, pSat );
-    sat_solver_delete( pSat );
     if ( RetValue == -1 )
         Abc_Print( 1, "UNDECIDED      " );
     else if ( RetValue == 0 )
@@ -449,6 +448,15 @@ int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart,
         Abc_Print( 1, "UNSATISFIABLE  " );
     //Abc_Print( -1, "\n" );
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    // derive SAT assignment
+    if ( RetValue == 0 )
+    {
+        *ppModel = ABC_ALLOC( int, nPis );
+        for ( i = 0; i < nPis; i++ )
+            (*ppModel)[i] = sat_solver_var_value( pSat, pCnf->nVars - nPis + i );
+    }
+    Cnf_DataFree( pCnf );
+    sat_solver_delete( pSat );
     return RetValue;
 }
 
-- 
cgit v1.2.3