From 72a7164e2dea289aa6370e7642dc1d7e2f62b513 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 8 Feb 2018 13:03:57 -0800 Subject: [PATCH] add model checker to external Signed-off-by: Nikolaj Bjorner --- src/sat/ba_solver.cpp | 81 +++++++++++++++++++++++++++++++++++------ src/sat/ba_solver.h | 8 +++- src/sat/sat_extension.h | 1 + src/sat/sat_solver.cpp | 4 +- 4 files changed, 80 insertions(+), 14 deletions(-) diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index 41d043526..428577de7 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -1641,7 +1641,6 @@ namespace sat { xr* x = new (mem) xr(next_id(), lits); x->set_learned(learned); add_constraint(x); - for (literal l : lits) s().set_external(l.var()); // TBD: determine if goal2sat does this. return x; } @@ -1715,7 +1714,6 @@ namespace sat { } - void ba_solver::ensure_parity_size(bool_var v) { if (m_parity_marks.size() <= static_cast(v)) { m_parity_marks.resize(static_cast(v) + 1, 0); @@ -2087,6 +2085,17 @@ namespace sat { return l_undef; } + lbool ba_solver::eval(model const& m, constraint const& c) const { + lbool v1 = c.lit() == null_literal ? l_true : value(c.lit()); + switch (c.tag()) { + case card_t: return eval(v1, eval(m, c.to_card())); + case pb_t: return eval(v1, eval(m, c.to_pb())); + case xr_t: return eval(v1, eval(m, c.to_xr())); + default: UNREACHABLE(); break; + } + return l_undef; + } + lbool ba_solver::eval(lbool a, lbool b) const { if (a == l_undef || b == l_undef) return l_undef; return (a == b) ? l_true : l_false; @@ -2106,6 +2115,34 @@ namespace sat { return l_undef; } + lbool ba_solver::eval(model const& m, card const& c) const { + unsigned trues = 0, undefs = 0; + for (literal l : c) { + switch (l.sign() ? ~m[l.var()] : m[l.var()]) { + case l_true: trues++; break; + case l_undef: undefs++; break; + default: break; + } + } + if (trues + undefs < c.k()) return l_false; + if (trues >= c.k()) return l_true; + return l_undef; + } + + lbool ba_solver::eval(model const& m, pb const& p) const { + unsigned trues = 0, undefs = 0; + for (wliteral wl : p) { + switch (wl.second.sign() ? ~m[wl.second.var()] : m[wl.second.var()]) { + case l_true: trues += wl.first; break; + case l_undef: undefs += wl.first; break; + default: break; + } + } + if (trues + undefs < p.k()) return l_false; + if (trues >= p.k()) return l_true; + return l_undef; + } + lbool ba_solver::eval(pb const& p) const { unsigned trues = 0, undefs = 0; for (wliteral wl : p) { @@ -2133,6 +2170,19 @@ namespace sat { return odd ? l_true : l_false; } + lbool ba_solver::eval(model const& m, xr const& x) const { + bool odd = false; + + for (auto l : x) { + switch (l.sign() ? ~m[l.var()] : m[l.var()]) { + case l_true: odd = !odd; break; + case l_false: break; + default: return l_undef; + } + } + return odd ? l_true : l_false; + } + bool ba_solver::validate() { if (!validate_watch_literals()) { return false; @@ -2903,7 +2953,6 @@ namespace sat { remove_constraint(c, "contains eliminated var"); break; } - s().set_external(v); } } return ext; @@ -2984,14 +3033,6 @@ namespace sat { m_constraint_removed = false; } - void ba_solver::ensure_external(constraint const& c) { - literal_vector lits(c.literals()); - for (literal l : lits) { - s().set_external(l.var()); - } - } - - void ba_solver::cleanup_constraints(ptr_vector& cs, bool learned) { ptr_vector::iterator it = cs.begin(); ptr_vector::iterator it2 = it; @@ -3004,7 +3045,6 @@ namespace sat { m_allocator.deallocate(c.obj_size(), &c); } else if (learned && !c.learned()) { - ensure_external(c); m_constraints.push_back(&c); } else { @@ -4051,6 +4091,23 @@ namespace sat { return value < p.m_k; } + bool ba_solver::check_model(model const& m) const { + bool ok = true; + for (constraint const* c : m_constraints) { + if (!check_model(m, *c)) ok = false; + } + return ok; + } + + bool ba_solver::check_model(model const& m, constraint const& c) const { + if (eval(m, c) != l_true) { + IF_VERBOSE(0, verbose_stream() << "failed checking " << c.id() << ": " << c << "\n";); + return false; + } + else { + return true; + } + } }; diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index 9e17b0594..8ed303469 100644 --- a/src/sat/ba_solver.h +++ b/src/sat/ba_solver.h @@ -302,7 +302,6 @@ namespace sat { void cleanup_clauses(); void cleanup_constraints(); void cleanup_constraints(ptr_vector& cs, bool learned); - void ensure_external(constraint const& c); void remove_constraint(constraint& c, char const* reason); // constraints @@ -328,6 +327,7 @@ namespace sat { void attach_constraint(constraint const& c); void detach_constraint(constraint const& c); lbool eval(constraint const& c) const; + lbool eval(model const& m, constraint const& c) const; lbool eval(lbool a, lbool b) const; void assert_unconstrained(literal lit, literal_vector const& lits); void flush_roots(constraint& c); @@ -348,6 +348,7 @@ namespace sat { bool clausify(card& c); bool clausify(literal lit, unsigned n, literal const* lits, unsigned k); lbool eval(card const& c) const; + lbool eval(model const& m, card const& c) const; double get_reward(card const& c, literal_occs_fun& occs) const; @@ -362,6 +363,7 @@ namespace sat { bool clausify(xr& x); void flush_roots(xr& x); lbool eval(xr const& x) const; + lbool eval(model const& m, xr const& x) const; // pb functionality unsigned m_a_max; @@ -379,6 +381,7 @@ namespace sat { bool clausify(pb& p); bool is_cardinality(pb const& p, literal_vector& lits); lbool eval(pb const& p) const; + lbool eval(model const& m, pb const& p) const; double get_reward(pb const& p, literal_occs_fun& occs) const; // access solver @@ -463,6 +466,8 @@ namespace sat { void copy_core(ba_solver* result, bool learned); void copy_constraints(ba_solver* result, ptr_vector const& constraints); + + bool check_model(model const& m, constraint const& c) const; public: ba_solver(); virtual ~ba_solver(); @@ -497,6 +502,7 @@ namespace sat { virtual bool is_extended_binary(ext_justification_idx idx, literal_vector & r); virtual void init_use_list(ext_use_list& ul); virtual bool is_blocked(literal l, ext_constraint_idx idx); + virtual bool check_model(model const& m) const; ptr_vector const & constraints() const { return m_constraints; } void display(std::ostream& out, constraint const& c, bool values) const; diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h index ff23c9be7..e687ab2b0 100644 --- a/src/sat/sat_extension.h +++ b/src/sat/sat_extension.h @@ -79,6 +79,7 @@ namespace sat { virtual bool validate() = 0; virtual void init_use_list(ext_use_list& ul) = 0; virtual bool is_blocked(literal l, ext_constraint_idx) = 0; + virtual bool check_model(model const& m) const = 0; }; }; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index b8850ce95..e384a944d 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -244,7 +244,6 @@ namespace sat { void solver::set_external(bool_var v) { if (m_external[v] != 0) return; m_external[v] = 1; - if (!m_ext) return; lbool val = value(v); @@ -1707,6 +1706,9 @@ namespace sat { ok = false; } } + if (m_ext && !m_ext->check_model(m)) { + ok = false; + } return ok; }