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

Small fix in satoko.

This commit is contained in:
Bruno Schmitt 2018-02-20 20:31:39 +01:00
parent 76b00a2d3e
commit eb4bee3e1d
2 changed files with 1 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -521,7 +521,6 @@ void solver_cancel_until(solver_t *s, unsigned level)
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, SATOKO_VAR_UNASSING);
vec_uint_assign(s->reasons, var, UNDEF);
if (!heap_in_heap(s->var_order, var))

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

@ -209,8 +209,7 @@ static inline int solver_enqueue(solver_t *s, unsigned lit, unsigned reason)
unsigned var = lit2var(lit);
vec_char_assign(s->assigns, var, lit_polarity(lit));
if ( solver_dlevel(s) == 0 )
vec_char_assign(s->polarity, var, lit_polarity(lit));
vec_char_assign(s->polarity, var, lit_polarity(lit));
vec_uint_assign(s->levels, var, solver_dlevel(s));
vec_uint_assign(s->reasons, var, reason);
vec_uint_push_back(s->trail, lit);