diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-04-07 14:10:51 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-04-07 14:10:51 -0700 |
| commit | 42927d5ebb7b7a828790394dc555cd129aa2481b (patch) | |
| tree | e608e44763ffb52169a8e7d19021643fb8a27bdc /src/sat/bsat/satSolver.c | |
| parent | af6705a8b1c75d069ef1fc504080b7bc6ee1c8f5 (diff) | |
| download | abc-42927d5ebb7b7a828790394dc555cd129aa2481b.tar.gz abc-42927d5ebb7b7a828790394dc555cd129aa2481b.tar.bz2 abc-42927d5ebb7b7a828790394dc555cd129aa2481b.zip | |
Adding command to dump UNSAT core of BMC instance.
Diffstat (limited to 'src/sat/bsat/satSolver.c')
| -rw-r--r-- | src/sat/bsat/satSolver.c | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 922f1eb7..5ea0b348 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -1153,6 +1153,7 @@ void sat_solver_delete(sat_solver* s) // veci_delete(&s->model); veci_delete(&s->act_vars); veci_delete(&s->unit_lits); + veci_delete(&s->pivot_vars); veci_delete(&s->temp_clause); veci_delete(&s->conf_final); @@ -1490,10 +1491,17 @@ void sat_solver_rollback( sat_solver* s ) int sat_solver_addclause(sat_solver* s, lit* begin, lit* end) { + int fVerbose = 0; lit *i,*j; int maxvar; lit last; assert( begin < end ); + if ( fVerbose ) + { + for ( i = begin; i < end; i++ ) + printf( "%s%d ", (*i)&1 ? "!":"", (*i)>>1 ); + printf( "\n" ); + } veci_resize( &s->temp_clause, 0 ); for ( i = begin; i < end; i++ ) |