From 4236830a8e23a745f8249566f04eedf5a6152592 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 27 Jan 2022 12:23:57 +0100 Subject: [PATCH] Also check clauses when returning SAT --- src/math/polysat/mul_ovfl_constraint.h | 4 ++-- src/math/polysat/solver.cpp | 22 ++++++++++++++++++---- 2 files changed, 20 insertions(+), 6 deletions(-) diff --git a/src/math/polysat/mul_ovfl_constraint.h b/src/math/polysat/mul_ovfl_constraint.h index 075509d3b..8932c10d6 100644 --- a/src/math/polysat/mul_ovfl_constraint.h +++ b/src/math/polysat/mul_ovfl_constraint.h @@ -38,8 +38,8 @@ namespace polysat { std::ostream& display(std::ostream& out) const override; bool is_always_false(bool is_positive) const override; void narrow(solver& s, bool is_positive) override; - bool is_currently_false(solver & s, bool is_positive) const; - bool is_currently_true(solver& s, bool is_positive) const; + bool is_currently_false(solver & s, bool is_positive) const override; + bool is_currently_true(solver& s, bool is_positive) const override; bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const override { return false; } bool is_currently_true(solver& s, assignment_t const& sub, bool is_positive) const override { return false; } diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index d057d5a97..0101176f5 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -144,12 +144,12 @@ namespace polysat { // Axioms for quotient/remainder: // a = b*q + r // multiplication does not overflow in b*q - // addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r + // addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r (TODO: maybe the version with disjunction is easier for the solver; should compare later) // b ≠ 0 ==> r < b // b = 0 ==> q = -1 - add_eq(b * q + r - a); + add_eq(a, b * q + r); add_noovfl(b, q); - add_ule(r, b*q+r); + add_ule(r, b * q + r); auto c1 = eq(b); auto c2 = ult(r, b); auto c3 = diseq(b); @@ -1081,8 +1081,22 @@ namespace polysat { all_ok = all_ok && ok; } } + for (auto clauses : m_constraints.clauses()) { + for (auto cl : clauses) { + bool clause_ok = false; + for (sat::literal lit : *cl) { + bool ok = lit2cnstr(lit).is_currently_true(*this); + if (ok) { + clause_ok = true; + break; + } + } + LOG((clause_ok ? "PASS" : "FAIL") << ": " << show_deref(cl) << (cl->is_redundant() ? " (redundant)" : "")); + all_ok = all_ok && clause_ok; + } + } if (all_ok) LOG("All good!"); - return true; + return all_ok; } }