Experiments with don't-cares.

2 files changed, 15 insertions, 0 deletions

diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 787626d6..673a6b66 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1334,6 +1334,9 @@ void sat_solver_delete(sat_solver* s)
     veci_delete(&s->temp_clause);
     veci_delete(&s->conf_final);
 
+    veci_delete(&s->user_vars);
+    veci_delete(&s->user_values);
+
     // delete arrays
     if (s->reasons != 0){
         int i;
@@ -1963,6 +1966,13 @@ int sat_solver_solve_internal(sat_solver* s)
         printf("==============================================================================\n");
 
     sat_solver_canceluntil(s,s->root_level);
+    // save variable values
+    if ( status == l_True && s->user_vars.size )
+    {
+        int v;
+        for ( v = 0; v < s->user_vars.size; v++ )
+            veci_push(&s->user_values, sat_solver_var_value(s, s->user_vars.ptr[v]));
+    }
     return status;
 }
 
@@ -2186,6 +2196,7 @@ int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int
         s->nConfLimit = nConfLimit;
         status = sat_solver_solve_internal( s );
         s->nConfLimit = Temp;
+        //printf( "%c", status == l_False ? 'u' : 's' );
         return (int)(status != l_False); // return 1 if the problem is not UNSAT
     }
     assert( nLits >= 2 );
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index e8a350ca..6ec437f7 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -193,6 +193,10 @@ struct sat_solver_t
 
     veci        temp_clause;    // temporary storage for a CNF clause
 
+    // assignment storage
+    veci        user_vars;      // variable IDs
+    veci        user_values;    // values of these variables
+
     // CNF loading
     void *      pCnfMan;           // external CNF manager
     int(*pCnfFunc)(void * p, int); // external callback