diff options
| -rw-r--r-- | src/sat/satoko/solver.c | 2 | ||||
| -rw-r--r-- | src/sat/satoko/solver.h | 5 |
2 files changed, 6 insertions, 1 deletions
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c index 6554f653..3e5fc8ee 100644 --- a/src/sat/satoko/solver.c +++ b/src/sat/satoko/solver.c @@ -195,7 +195,7 @@ static inline unsigned solver_decide(solver_t *s) if (solver_has_marks(s) && !var_mark(s, next_var)) next_var = UNDEF; } - return var2lit(next_var, vec_char_at(s->polarity, next_var)); + return var2lit(next_var, var_polarity(s, next_var)); } static inline void solver_new_decision(solver_t *s, unsigned lit) diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h index 68cc97dc..dcae8f6e 100644 --- a/src/sat/satoko/solver.h +++ b/src/sat/satoko/solver.h @@ -132,6 +132,11 @@ static inline char var_value(solver_t *s, unsigned var) return vec_char_at(s->assigns, var); } +static inline char var_polarity(solver_t *s, unsigned var) +{ + return vec_char_at(s->polarity, var); +} + static inline unsigned var_dlevel(solver_t *s, unsigned var) { return vec_uint_at(s->levels, var); |