diff options
Diffstat (limited to 'src/sat/satoko/solver.c')
-rw-r--r-- | src/sat/satoko/solver.c | 87 |
1 files changed, 69 insertions, 18 deletions
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c index 51befd16..b35574ab 100644 --- a/src/sat/satoko/solver.c +++ b/src/sat/satoko/solver.c @@ -362,14 +362,16 @@ static inline void solver_handle_conflict(solver_t *s, unsigned confl_cref) static inline void solver_analyze_final(solver_t *s, unsigned lit) { - int i; + unsigned i; + // printf("[Satoko] Analize final..\n"); + // printf("[Satoko] Conflicting lit: %d\n", lit); vec_uint_clear(s->final_conflict); vec_uint_push_back(s->final_conflict, lit); if (solver_dlevel(s) == 0) return; vec_char_assign(s->seen, lit2var(lit), 1); - for (i = (int) vec_uint_size(s->trail) - 1; i >= (int) vec_uint_at(s->trail_lim, 0); i--) { + for (i = vec_uint_size(s->trail); i --> vec_uint_at(s->trail_lim, 0);) { unsigned var = lit2var(vec_uint_at(s->trail, i)); if (vec_char_at(s->seen, var)) { @@ -385,10 +387,11 @@ static inline void solver_analyze_final(solver_t *s, unsigned lit) vec_char_assign(s->seen, lit2var(clause->data[j].lit), 1); } } - vec_char_assign(s->seen, var, 0); + vec_char_assign(s->seen, var, 0); } } vec_char_assign(s->seen, lit2var(lit), 0); + // solver_debug_check_unsat(s); } static inline void solver_garbage_collect(solver_t *s) @@ -511,12 +514,12 @@ unsigned solver_clause_create(solver_t *s, vec_uint_t *lits, unsigned f_learnt) void solver_cancel_until(solver_t *s, unsigned level) { - int i; + unsigned i; if (solver_dlevel(s) <= level) return; - for (i = (int) vec_uint_size(s->trail) - 1; i >= (int) vec_uint_at(s->trail_lim, level); i--) { - unsigned var = lit2var(vec_uint_at(s->trail, (unsigned) i)); + for (i = vec_uint_size(s->trail); i --> vec_uint_at(s->trail_lim, level);) { + unsigned var = lit2var(vec_uint_at(s->trail, i)); vec_char_assign(s->polarity, var, vec_char_at(s->assigns, var)); vec_char_assign(s->assigns, var, VAR_UNASSING); @@ -636,6 +639,7 @@ char solver_search(solver_t *s) b_queue_clean(s->bq_lbd); solver_handle_conflict(s, confl_cref); } else { + // solver_debug_check_clauses(s); /* No conflict */ unsigned next_lit; @@ -675,8 +679,10 @@ char solver_search(solver_t *s) if (next_lit == UNDEF) { s->stats.n_decisions++; next_lit = solver_decide(s); - if (next_lit == UNDEF) + if (next_lit == UNDEF) { + // solver_debug_check(s, SATOKO_SAT); return SATOKO_SAT; + } } solver_new_decision(s, next_lit); } @@ -684,23 +690,66 @@ char solver_search(solver_t *s) } //===------------------------------------------------------------------------=== -// Debug procedure +// Debug procedures //===------------------------------------------------------------------------=== -void solver_debug_check(solver_t *s, int result) +void solver_debug_check_trail(solver_t *s) { - unsigned cref, i; + unsigned i; unsigned *array; - - printf("Checking for trail(%u) inconsistencies...", vec_uint_size(s->trail)); - array = vec_uint_data(s->trail); - for (i = 1; i < vec_uint_size(s->trail); i++) + vec_uint_t *trail_dup = vec_uint_alloc(0); + fprintf(stdout, "[Satoko] Checking for trail(%u) inconsistencies...\n", vec_uint_size(s->trail)); + vec_uint_duplicate(trail_dup, s->trail); + vec_uint_sort(trail_dup, 1); + array = vec_uint_data(trail_dup); + for (i = 1; i < vec_uint_size(trail_dup); i++) { if (array[i - 1] == lit_compl(array[i])) { - printf("Inconsistent trail: %u %u\n", array[i - 1], array[i]); + fprintf(stdout, "[Satoko] Inconsistent trail: %u %u\n", array[i - 1], array[i]); + assert(0); return; } - printf(" TRAIL OK\n"); + } + for (i = 0; i < vec_uint_size(trail_dup); i++) { + if (var_value(s, lit2var(array[i])) != lit_polarity(array[i])) { + fprintf(stdout, "[Satoko] Inconsistent trail assignment: %u, %u\n", vec_char_at(s->assigns, lit2var(array[i])), array[i]); + assert(0); + return; + } + } + fprintf(stdout, "[Satoko] Trail OK.\n"); + vec_uint_print(trail_dup); + vec_uint_free(trail_dup); - printf("Checking clauses... \n"); +} + +void solver_debug_check_clauses(solver_t *s) +{ + unsigned cref, i; + + fprintf(stdout, "[Satoko] Checking clauses (%d)...\n", vec_uint_size(s->originals)); + vec_uint_foreach(s->originals, cref, i) { + unsigned j; + struct clause *clause = clause_fetch(s, cref); + for (j = 0; j < clause->size; j++) { + if (vec_uint_find(s->trail, lit_compl(clause->data[j].lit))) { + continue; + } + break; + } + if (j == clause->size) { + vec_uint_print(s->trail); + fprintf(stdout, "[Satoko] FOUND UNSAT CLAUSE]: (%d) ", i); + clause_print(clause); + assert(0); + } + } + fprintf(stdout, "[Satoko] All SAT - OK\n"); +} + +void solver_debug_check(solver_t *s, int result) +{ + unsigned cref, i; + solver_debug_check_trail(s); + fprintf(stdout, "[Satoko] Checking clauses (%d)... \n", vec_uint_size(s->originals)); vec_uint_foreach(s->originals, cref, i) { unsigned j; struct clause *clause = clause_fetch(s, cref); @@ -710,10 +759,12 @@ void solver_debug_check(solver_t *s, int result) } } if (result == SATOKO_SAT && j == clause->size) { - printf("FOUND UNSAT CLAUSE!!!!\n"); + fprintf(stdout, "[Satoko] FOUND UNSAT CLAUSE: (%d) ", i); clause_print(clause); + assert(0); } } + fprintf(stdout, "[Satoko] All SAT - OK\n"); } ABC_NAMESPACE_IMPL_END |