diff options
Diffstat (limited to 'src/sat/satoko/solver.h')
-rw-r--r-- | src/sat/satoko/solver.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h index 68cc97dc..33f8ce88 100644 --- a/src/sat/satoko/solver.h +++ b/src/sat/satoko/solver.h @@ -95,6 +95,7 @@ struct solver_t_ { /* Bookmark */ unsigned book_cl_orig; /* Bookmark for orignal problem clauses vector */ unsigned book_cl_lrnt; /* Bookmark for learnt clauses vector */ + unsigned book_cdb; /* Bookmark clause database size */ unsigned book_vars; /* Bookmark number of variables */ unsigned book_trail; /* Bookmark trail size */ @@ -132,6 +133,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); |