luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

[Satoko] Correcting bug found when integrating with pdr. 

The head of the propagation queue was not begin properly reset.

Adding some debugging functions.
This commit is contained in:
Bruno Schmitt 2017-08-28 10:59:30 +02:00
parent d80bbe7400
commit 3df049f37d
4 changed files with 105 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/sat/satoko/cnf_reader.c
View File

@ -142,8 +142,9 @@ int satoko_parse_dimacs(char *fname, satoko_t **solver)
}
read_clause(&token, lits);
if (!satoko_add_clause(p, (int*)vec_uint_data(lits), vec_uint_size(lits))) {
printf("Unable to add clause: ");
vec_uint_print(lits);
return 0;
return SATOKO_ERR;
}
}
}

93
src/sat/satoko/solver.c
View File

@ -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_trail(solver_t *s)
{
unsigned i;
unsigned *array;
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])) {
fprintf(stdout, "[Satoko] Inconsistent trail: %u %u\n", array[i - 1], array[i]);
assert(0);
return;
}
}
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);
}
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;
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++)
if (array[i - 1] == lit_compl(array[i])) {
printf("Inconsistent trail: %u %u\n", array[i - 1], array[i]);
return;
}
printf(" TRAIL OK\n");
printf("Checking clauses... \n");
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

5
src/sat/satoko/solver.h
View File

@ -99,6 +99,7 @@ struct solver_t_ {
unsigned book_cdb; /* Bookmark clause database size */
unsigned book_vars; /* Bookmark number of variables */
unsigned book_trail; /* Bookmark trail size */
// unsigned book_qhead; /* Bookmark propagation queue head */
/* Temporary data used for solving cones */
vec_char_t *marks;
@ -118,7 +119,11 @@ extern unsigned solver_clause_create(solver_t *, vec_uint_t *, unsigned);
extern char solver_search(solver_t *);
extern void solver_cancel_until(solver_t *, unsigned);
extern unsigned solver_propagate(solver_t *);
/* Debuging */
extern void solver_debug_check(solver_t *, int);
extern void solver_debug_check_trail(solver_t *);
extern void solver_debug_check_clauses(solver_t *);
//===------------------------------------------------------------------------===
// Inline var/lit functions

28
src/sat/satoko/solver_api.c
View File

@ -43,6 +43,11 @@ static inline int clause_is_satisfied(solver_t *s, struct clause *clause)
return SATOKO_ERR;
}
static inline void solver_clean_stats(solver_t *s)
{
memset(&(s->stats), 0, sizeof(struct satoko_stats));
}
static inline void print_opts(solver_t *s)
{
printf( "+-[ BLACK MAGIC - PARAMETERS ]-+\n");
@ -282,12 +287,15 @@ int satoko_add_clause(solver_t *s, int *lits, int size)
void satoko_assump_push(solver_t *s, int lit)
{
assert(lit2var(lit) < solver_varnum(s));
// printf("[Satoko] Push assumption: %d\n", lit);
vec_uint_push_back(s->assumptions, lit);
}
void satoko_assump_pop(solver_t *s)
{
assert(vec_uint_size(s->assumptions) > 0);
// printf("[Satoko] Pop assumption: %d\n", vec_uint_pop_back(s->assumptions));
vec_uint_pop_back(s->assumptions);
solver_cancel_until(s, vec_uint_size(s->assumptions));
}
@ -297,6 +305,7 @@ int satoko_solve(solver_t *s)
int status = SATOKO_UNDEC;
assert(s);
solver_clean_stats(s);
//if (s->opts.verbose)
// print_opts(s);
if (s->status == SATOKO_ERR) {
@ -327,6 +336,12 @@ int satoko_solve(solver_t *s)
int satoko_solve_assumptions(solver_t *s, int * plits, int nlits)
{
int i, status;
// printf("\n[Satoko] Solve with assumptions.. (%d)\n", vec_uint_size(s->assumptions));
// printf("[Satoko] + Variables: %d\n", solver_varnum(s));
// printf("[Satoko] + Clauses: %d\n", solver_clausenum(s));
// printf("[Satoko] + Trail size: %d\n", vec_uint_size(s->trail));
// printf("[Satoko] + Queue head: %d\n", s->i_qhead);
// solver_debug_check_trail(s);
for ( i = 0; i < nlits; i++ )
satoko_assump_push( s, plits[i] );
status = satoko_solve( s );
@ -357,28 +372,33 @@ satoko_stats_t satoko_stats(satoko_t *s)
void satoko_bookmark(satoko_t *s)
{
// printf("[Satoko] Bookmark.\n");
assert(s->status == SATOKO_OK);
assert(solver_dlevel(s) == 0);
s->book_cl_orig = vec_uint_size(s->originals);
s->book_cl_lrnt = vec_uint_size(s->learnts);
s->book_vars = vec_char_size(s->assigns);
s->book_trail = vec_uint_size(s->trail);
// s->book_qhead = s->i_qhead;
s->opts.no_simplify = 1;
}
void satoko_unbookmark(satoko_t *s)
{
// printf("[Satoko] Unbookmark.\n");
assert(s->status == SATOKO_OK);
s->book_cl_orig = 0;
s->book_cl_lrnt = 0;
s->book_cdb = 0;
s->book_vars = 0;
s->book_trail = 0;
// s->book_qhead = 0;
s->opts.no_simplify = 0;
}
void satoko_reset(satoko_t *s)
{
// printf("[Satoko] Reset.\n");
vec_uint_clear(s->assumptions);
vec_uint_clear(s->final_conflict);
cdb_clear(s->all_clauses);
@ -412,6 +432,7 @@ void satoko_reset(satoko_t *s)
s->book_cdb = 0;
s->book_vars = 0;
s->book_trail = 0;
s->i_qhead = 0;
}
void satoko_rollback(satoko_t *s)
@ -421,13 +442,13 @@ void satoko_rollback(satoko_t *s)
unsigned n_learnts = vec_uint_size(s->learnts) - s->book_cl_lrnt;
struct clause **cl_to_remove;
// printf("[Satoko] rollback.\n");
assert(s->status == SATOKO_OK);
assert(solver_dlevel(s) == 0);
if (!s->book_vars) {
satoko_reset(s);
return;
}
cl_to_remove = satoko_alloc(struct clause *, n_originals + n_learnts);
/* Mark clauses */
vec_uint_foreach_start(s->originals, cref, i, s->book_cl_orig)
@ -446,6 +467,7 @@ void satoko_rollback(satoko_t *s)
vec_wl_at(s->watches, i)->size = 0;
vec_wl_at(s->watches, i)->n_bin = 0;
}
// s->i_qhead = s->book_qhead;
s->watches->size = s->book_vars;
vec_act_shrink(s->activity, s->book_vars);
vec_uint_shrink(s->levels, s->book_vars);
@ -464,6 +486,7 @@ void satoko_rollback(satoko_t *s)
s->book_cl_lrnt = 0;
s->book_vars = 0;
s->book_trail = 0;
// s->book_qhead = 0;
}
void satoko_mark_cone(satoko_t *s, int * pvars, int n_vars)
@ -510,7 +533,7 @@ void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var)
fprintf(file, "p cnf %d %d\n", n_vars, wrt_lrnt ? n_orig + n_lrnts : n_orig);
for (i = 0; i < vec_char_size(s->assigns); i++)
if ( var_value(s, i) != VAR_UNASSING )
fprintf(file, "%d\n", var_value(s, i) == LIT_FALSE ? -(int)(i + !zero_var) : i + !zero_var);
fprintf(file, "%d %d\n", var_value(s, i) == LIT_FALSE ? -(int)(i + !zero_var) : i + !zero_var, zero_var ? : 0);
array = vec_uint_data(s->originals);
for (i = 0; i < vec_uint_size(s->originals); i++)
@ -521,6 +544,7 @@ void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var)
for (i = 0; i < n_lrnts; i++)
clause_dump(file, clause_fetch(s, array[i]), !zero_var);
}
fclose(file);
}