diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-04-04 03:17:24 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-04-04 03:17:24 -0700 |
commit | 44605f5af647cc6963603116091fcbe98080d660 (patch) | |
tree | bc66da01347346fc47726d72e4cb92a9d93fb132 /src/sat | |
parent | f765e666ca4608f8dfe3ab2ecbacaf9966d25129 (diff) | |
download | abc-44605f5af647cc6963603116091fcbe98080d660.tar.gz abc-44605f5af647cc6963603116091fcbe98080d660.tar.bz2 abc-44605f5af647cc6963603116091fcbe98080d660.zip |
Experiments with don't-cares.
Diffstat (limited to 'src/sat')
-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 |