diff options
Diffstat (limited to 'src/sat/bsat')
| -rw-r--r-- | src/sat/bsat/satSolver.c | 11 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver.h | 4 |
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 |