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

Renaming several Satoko APIs to avoid collision with MiniSAT.

This commit is contained in:
Alan Mishchenko 2017-08-13 17:52:25 +07:00
parent 0d307b1c85
commit 21289bf08a
4 changed files with 29 additions and 29 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/sat/satoko/act_clause.h
View File

@ -21,7 +21,7 @@ static inline void clause_act_rescale(solver_t *s)
struct clause *clause;
vec_uint_foreach(s->learnts, cref, i) {
clause = clause_read(s, cref);
clause = clause_fetch(s, cref);
clause->data[clause->size].act >>= 10;
}
s->clause_act_inc = stk_uint_max((s->clause_act_inc >> 10), (1 << 11));

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

@ -39,7 +39,7 @@ static inline int lit_is_removable(solver_t* s, unsigned lit, unsigned min_level
while (vec_uint_size(s->stack)) {
unsigned i;
unsigned var = vec_uint_pop_back(s->stack);
struct clause *c = clause_read(s, var_reason(s, var));
struct clause *c = clause_fetch(s, var_reason(s, var));
unsigned *lits = &(c->data[0].lit);
assert(var_reason(s, var) != UNDEF);
@ -106,7 +106,7 @@ static inline void clause_bin_resolution(solver_t *s, vec_uint_t *clause_lits)
unsigned *lits = vec_uint_data(clause_lits);
unsigned counter, sz, i;
unsigned lit;
unsigned neg_lit = lit_neg(lits[0]);
unsigned neg_lit = lit_compl(lits[0]);
struct watcher *w;
s->cur_stamp++;
@ -267,7 +267,7 @@ static inline void solver_analyze(solver_t *s, unsigned cref, vec_uint_t *learnt
unsigned j;
assert(cref != UNDEF);
clause = clause_read(s, cref);
clause = clause_fetch(s, cref);
lits = &(clause->data[0].lit);
if (p != UNDEF && clause->size == 2 && lit_value(s, lits[0]) == LIT_FALSE) {
@ -295,7 +295,7 @@ static inline void solver_analyze(solver_t *s, unsigned cref, vec_uint_t *learnt
var_act_bump(s, var);
if (var_dlevel(s, var) == solver_dlevel(s)) {
n_paths++;
if (var_reason(s, var) != UNDEF && clause_read(s, var_reason(s, var))->f_learnt)
if (var_reason(s, var) != UNDEF && clause_fetch(s, var_reason(s, var))->f_learnt)
vec_uint_push_back(s->last_dlevel, var);
} else
vec_uint_push_back(learnt, lits[j]);
@ -309,14 +309,14 @@ static inline void solver_analyze(solver_t *s, unsigned cref, vec_uint_t *learnt
n_paths--;
} while (n_paths > 0);
vec_uint_data(learnt)[0] = lit_neg(p);
vec_uint_data(learnt)[0] = lit_compl(p);
clause_minimize(s, learnt);
*bt_level = solver_calc_bt_level(s, learnt);
*lbd = clause_clac_lbd(s, vec_uint_data(learnt), vec_uint_size(learnt));
if (vec_uint_size(s->last_dlevel) > 0) {
vec_uint_foreach(s->last_dlevel, var, i) {
if (clause_read(s, var_reason(s, var))->lbd < *lbd)
if (clause_fetch(s, var_reason(s, var))->lbd < *lbd)
var_act_bump(s, var);
}
vec_uint_clear(s->last_dlevel);
@ -376,10 +376,10 @@ static inline void solver_analyze_final(solver_t *s, unsigned lit)
unsigned reason = var_reason(s, var);
if (reason == UNDEF) {
assert(var_dlevel(s, var) > 0);
vec_uint_push_back(s->final_conflict, lit_neg(vec_uint_at(s->trail, i)));
vec_uint_push_back(s->final_conflict, lit_compl(vec_uint_at(s->trail, i)));
} else {
unsigned j;
struct clause *clause = clause_read(s, reason);
struct clause *clause = clause_fetch(s, reason);
for (j = (clause->size == 2 ? 0 : 1); j < clause->size; j++) {
if (lit_dlevel(s, clause->data[j].lit) > 0)
vec_char_assign(s->seen, lit2var(clause->data[j].lit), 1);
@ -433,7 +433,7 @@ static inline void solver_reduce_cdb(solver_t *s)
learnts_cls = satoko_alloc(struct clause *, n_learnts);
vec_uint_foreach_start(s->learnts, cref, i, s->book_cl_lrnt)
learnts_cls[i] = clause_read(s, cref);
learnts_cls[i] = clause_fetch(s, cref);
limit = (unsigned)(n_learnts * s->opts.learnt_ratio);
@ -488,7 +488,7 @@ unsigned solver_clause_create(solver_t *s, vec_uint_t *lits, unsigned f_learnt)
n_words = 3 + f_learnt + vec_uint_size(lits);
cref = cdb_append(s->all_clauses, n_words);
clause = clause_read(s, cref);
clause = clause_fetch(s, cref);
clause->f_learnt = f_learnt;
clause->f_mark = 0;
clause->f_reallocd = 0;
@ -569,11 +569,11 @@ unsigned solver_propagate(solver_t *s)
continue;
}
clause = clause_read(s, i->cref);
clause = clause_fetch(s, i->cref);
lits = &(clause->data[0].lit);
// Make sure the false literal is data[1]:
neg_lit = lit_neg(p);
neg_lit = lit_compl(p);
if (lits[0] == neg_lit)
stk_swap(unsigned, lits[0], lits[1]);
assert(lits[1] == neg_lit);
@ -591,7 +591,7 @@ unsigned solver_propagate(solver_t *s)
if (lit_value(s, lits[k]) != LIT_FALSE) {
lits[1] = lits[k];
lits[k] = neg_lit;
watch_list_push(vec_wl_at(s->watches, lit_neg(lits[1])), w, 0);
watch_list_push(vec_wl_at(s->watches, lit_compl(lits[1])), w, 0);
goto next;
}
}
@ -663,7 +663,7 @@ char solver_search(solver_t *s)
if (lit_value(s, lit) == LIT_TRUE) {
vec_uint_push_back(s->trail_lim, vec_uint_size(s->trail));
} else if (lit_value(s, lit) == LIT_FALSE) {
solver_analyze_final(s, lit_neg(lit));
solver_analyze_final(s, lit_compl(lit));
return SATOKO_UNSAT;
} else {
next_lit = lit;
@ -693,7 +693,7 @@ void solver_debug_check(solver_t *s, int result)
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_neg(array[i])) {
if (array[i - 1] == lit_compl(array[i])) {
printf("Inconsistent trail: %u %u\n", array[i - 1], array[i]);
return;
}
@ -702,7 +702,7 @@ void solver_debug_check(solver_t *s, int result)
printf("Checking clauses... \n");
vec_uint_foreach(s->originals, cref, i) {
unsigned j;
struct clause *clause = clause_read(s, cref);
struct clause *clause = clause_fetch(s, cref);
for (j = 0; j < clause->size; j++) {
if (vec_uint_find(s->trail, clause->data[j].lit)) {
break;

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

@ -166,7 +166,7 @@ static inline void var_clean_mark(solver_t *s, unsigned var)
//===------------------------------------------------------------------------===
// Inline lit functions
//===------------------------------------------------------------------------===
static inline unsigned lit_neg(unsigned lit)
static inline unsigned lit_compl(unsigned lit)
{
return lit ^ 1;
}
@ -238,7 +238,7 @@ static inline void solver_set_stop(solver_t *s, int * pstop)
//===------------------------------------------------------------------------===
// Inline clause functions
//===------------------------------------------------------------------------===
static inline struct clause *clause_read(solver_t *s, unsigned cref)
static inline struct clause *clause_fetch(solver_t *s, unsigned cref)
{
return cdb_handler(s->all_clauses, cref);
}
@ -253,15 +253,15 @@ static inline void clause_watch(solver_t *s, unsigned cref)
w2.cref = cref;
w1.blocker = clause->data[1].lit;
w2.blocker = clause->data[0].lit;
watch_list_push(vec_wl_at(s->watches, lit_neg(clause->data[0].lit)), w1, (clause->size == 2));
watch_list_push(vec_wl_at(s->watches, lit_neg(clause->data[1].lit)), w2, (clause->size == 2));
watch_list_push(vec_wl_at(s->watches, lit_compl(clause->data[0].lit)), w1, (clause->size == 2));
watch_list_push(vec_wl_at(s->watches, lit_compl(clause->data[1].lit)), w2, (clause->size == 2));
}
static inline void clause_unwatch(solver_t *s, unsigned cref)
{
struct clause *clause = cdb_handler(s->all_clauses, cref);
watch_list_remove(vec_wl_at(s->watches, lit_neg(clause->data[0].lit)), cref, (clause->size == 2));
watch_list_remove(vec_wl_at(s->watches, lit_neg(clause->data[1].lit)), cref, (clause->size == 2));
watch_list_remove(vec_wl_at(s->watches, lit_compl(clause->data[0].lit)), cref, (clause->size == 2));
watch_list_remove(vec_wl_at(s->watches, lit_compl(clause->data[1].lit)), cref, (clause->size == 2));
}
ABC_NAMESPACE_HEADER_END

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

@ -202,7 +202,7 @@ int satoko_simplify(solver_t * s)
return SATOKO_OK;
vec_uint_foreach(s->originals, cref, i) {
struct clause *clause = clause_read(s, cref);
struct clause *clause = clause_fetch(s, cref);
if (clause_is_satisfied(s, clause)) {
clause->f_mark = 1;
@ -252,7 +252,7 @@ int satoko_add_clause(solver_t *s, int *lits, int size)
j = 0;
prev_lit = UNDEF;
for (i = 0; i < (unsigned)size; i++) {
if ((unsigned)lits[i] == lit_neg(prev_lit) || lit_value(s, lits[i]) == LIT_TRUE)
if ((unsigned)lits[i] == lit_compl(prev_lit) || lit_value(s, lits[i]) == LIT_TRUE)
return SATOKO_OK;
else if ((unsigned)lits[i] != prev_lit && var_value(s, lit2var(lits[i])) == VAR_UNASSING) {
prev_lit = lits[i];
@ -404,9 +404,9 @@ void satoko_rollback(satoko_t *s)
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)
cl_to_remove[i] = clause_read(s, cref);
cl_to_remove[i] = clause_fetch(s, cref);
vec_uint_foreach_start(s->learnts, cref, i, s->book_cl_lrnt)
cl_to_remove[n_originals + i] = clause_read(s, cref);
cl_to_remove[n_originals + i] = clause_fetch(s, cref);
for (i = 0; i < n_originals + n_learnts; i++) {
clause_unwatch(s, cdb_cref(s->all_clauses, (unsigned *)cl_to_remove[i]));
cl_to_remove[i]->f_mark = 1;
@ -487,12 +487,12 @@ void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var)
array = vec_uint_data(s->originals);
for (i = 0; i < vec_uint_size(s->originals); i++)
clause_dump(file, clause_read(s, array[i]), !zero_var);
clause_dump(file, clause_fetch(s, array[i]), !zero_var);
if (wrt_lrnt) {
array = vec_uint_data(s->learnts);
for (i = 0; i < n_lrnts; i++)
clause_dump(file, clause_read(s, array[i]), !zero_var);
clause_dump(file, clause_fetch(s, array[i]), !zero_var);
}
}