From 6218931ddec7bd404d2f663ac00bfea86b1b3826 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 29 Sep 2022 17:19:47 +0200 Subject: [PATCH] We only need one of is_true/is_false --- src/math/polysat/constraint.h | 9 ++++++--- src/math/polysat/op_constraint.cpp | 10 +--------- src/math/polysat/op_constraint.h | 2 -- src/math/polysat/smul_fl_constraint.h | 2 -- src/math/polysat/ule_constraint.cpp | 8 -------- src/math/polysat/ule_constraint.h | 2 -- src/math/polysat/umul_ovfl_constraint.cpp | 11 +---------- src/math/polysat/umul_ovfl_constraint.h | 2 -- 8 files changed, 8 insertions(+), 38 deletions(-) diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index 88f7ec34b..4e596b7e6 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -177,9 +177,11 @@ namespace polysat { virtual bool is_always_false(bool is_positive) const = 0; virtual bool is_currently_false(solver& s, bool is_positive) const = 0; - virtual bool is_currently_true(solver& s, bool is_positive) const = 0; virtual bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const = 0; - virtual bool is_currently_true(solver& s, assignment_t const& sub, bool is_positive) const = 0; + bool is_always_true(bool is_positive) const { return is_always_false(!is_positive); } + bool is_currently_true(solver& s, bool is_positive) const { return is_currently_false(s, !is_positive); } + bool is_currently_true(solver& s, assignment_t const& sub, bool is_positive) const { return is_currently_false(s, sub, !is_positive); } + virtual void narrow(solver& s, bool is_positive, bool first) = 0; virtual inequality as_inequality(bool is_positive) const = 0; @@ -246,8 +248,9 @@ namespace polysat { bool is_always_false() const { return get()->is_always_false(is_positive()); } bool is_always_true() const { return get()->is_always_false(is_negative()); } bool is_currently_false(solver& s) const { return get()->is_currently_false(s, is_positive()); } - bool is_currently_true(solver& s) const { return get()->is_currently_true(s, is_positive()); } + bool is_currently_true(solver& s) const { return get()->is_currently_false(s, is_negative()); } bool is_currently_false(solver& s, assignment_t const& sub) const { return get()->is_currently_false(s, sub, is_positive()); } + bool is_currently_true(solver& s, assignment_t const& sub) const { return get()->is_currently_false(s, sub, is_negative()); } lbool bvalue(solver& s) const; unsigned level(solver& s) const { return get()->level(s); } void narrow(solver& s, bool first) { get()->narrow(s, is_positive(), first); } diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp index 7f3340477..f9f62ca93 100644 --- a/src/math/polysat/op_constraint.cpp +++ b/src/math/polysat/op_constraint.cpp @@ -67,11 +67,7 @@ namespace polysat { } bool op_constraint::is_always_true(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const { - switch (eval(p, q, r)) { - case l_true: return is_positive; - case l_false: return !is_positive; - default: return false; - } + return is_always_false(!is_positive, p, q, r); } bool op_constraint::is_always_false(bool is_positive) const { @@ -82,10 +78,6 @@ namespace polysat { return is_always_false(is_positive, s.subst(p()), s.subst(q()), s.subst(r())); } - bool op_constraint::is_currently_true(solver& s, bool is_positive) const { - return is_always_true(is_positive, s.subst(p()), s.subst(q()), s.subst(r())); - } - std::ostream& op_constraint::display(std::ostream& out, lbool status) const { switch (status) { case l_true: return display(out); diff --git a/src/math/polysat/op_constraint.h b/src/math/polysat/op_constraint.h index de34be74a..4a5d572fc 100644 --- a/src/math/polysat/op_constraint.h +++ b/src/math/polysat/op_constraint.h @@ -57,9 +57,7 @@ namespace polysat { std::ostream& display(std::ostream& out) const override; bool is_always_false(bool is_positive) const override; 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; } void narrow(solver& s, bool is_positive, bool first) override; inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); } unsigned hash() const override; diff --git a/src/math/polysat/smul_fl_constraint.h b/src/math/polysat/smul_fl_constraint.h index 1937b259c..dffd0be6b 100644 --- a/src/math/polysat/smul_fl_constraint.h +++ b/src/math/polysat/smul_fl_constraint.h @@ -37,9 +37,7 @@ namespace polysat { bool is_always_false(bool is_positive) const override { return false; } void narrow(solver& s, bool is_positive, bool first) override; bool is_currently_false(solver & s, bool is_positive) const override { return false; } - bool is_currently_true(solver& s, bool is_positive) const override { return false; } 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; } inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); } unsigned hash() const override; diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index 2ea9193d0..9e3ca4200 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -224,14 +224,6 @@ namespace polysat { return is_always_false(is_positive, p, q); } - bool ule_constraint::is_currently_true(solver& s, assignment_t const& sub, bool is_positive) const { - return is_currently_false(s, sub, !is_positive); - } - - bool ule_constraint::is_currently_true(solver& s, bool is_positive) const { - return is_currently_false(s, !is_positive); - } - inequality ule_constraint::as_inequality(bool is_positive) const { if (is_positive) return inequality(lhs(), rhs(), false, this); diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h index 71cf98f4e..01eb57b93 100644 --- a/src/math/polysat/ule_constraint.h +++ b/src/math/polysat/ule_constraint.h @@ -38,9 +38,7 @@ namespace polysat { static bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs); bool is_always_false(bool is_positive) const override; 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; - bool is_currently_true(solver& s, assignment_t const& sub, bool is_positive) const override; void narrow(solver& s, bool is_positive, bool first) override; inequality as_inequality(bool is_positive) const override; unsigned hash() const override; diff --git a/src/math/polysat/umul_ovfl_constraint.cpp b/src/math/polysat/umul_ovfl_constraint.cpp index 1081abed9..d91c055af 100644 --- a/src/math/polysat/umul_ovfl_constraint.cpp +++ b/src/math/polysat/umul_ovfl_constraint.cpp @@ -70,26 +70,17 @@ namespace polysat { } bool umul_ovfl_constraint::is_always_true(bool is_positive, pdd const& p, pdd const& q) const { - switch (eval(p, q)) { - case l_true: return is_positive; - case l_false: return !is_positive; - default: return false; - } + return is_always_false(!is_positive, p, q); } bool umul_ovfl_constraint::is_always_false(bool is_positive) const { return is_always_false(is_positive, m_p, m_q); } - bool umul_ovfl_constraint::is_currently_false(solver& s, bool is_positive) const { return is_always_false(is_positive, s.subst(p()), s.subst(q())); } - bool umul_ovfl_constraint::is_currently_true(solver& s, bool is_positive) const { - return is_always_true(is_positive, s.subst(p()), s.subst(q())); - } - void umul_ovfl_constraint::narrow(solver& s, bool is_positive, bool first) { auto p1 = s.subst(p()); auto q1 = s.subst(q()); diff --git a/src/math/polysat/umul_ovfl_constraint.h b/src/math/polysat/umul_ovfl_constraint.h index d3c8f357f..53771ab4e 100644 --- a/src/math/polysat/umul_ovfl_constraint.h +++ b/src/math/polysat/umul_ovfl_constraint.h @@ -40,9 +40,7 @@ namespace polysat { bool is_always_false(bool is_positive) const override; void narrow(solver& s, bool is_positive, bool first) override; 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; } inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); } unsigned hash() const override;