From 1cb7ca8dfcdd91ed86ae7cfb77b158587062674c Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 24 Jan 2022 14:15:10 +0100 Subject: [PATCH] match additional cases in forbidden intervals --- src/math/polysat/forbidden_intervals.cpp | 70 +++++++++++++++++++++--- src/math/polysat/forbidden_intervals.h | 5 ++ src/test/polysat.cpp | 20 +++++++ 3 files changed, 87 insertions(+), 8 deletions(-) diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index 57e766069..9586b820d 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -54,22 +54,28 @@ namespace polysat { auto [ok2, a2, e2, b2] = linear_decompose(v, c->to_ule().rhs(), fi.side_cond); _backtrack.released = true; - + + + // a*v <= 0, a odd + if (ok1 && ok2 && match_zero(c, a1, b1, e1, a2, b2, e2, fi)) + return true; + // v > q + // 2^k*a*v + b > 0 + // TODO: is !ok2 required? if (ok1 && !ok2 && match_non_zero(c, a1, b1, e1, fi)) return true; // p > v if (!ok1 && ok2 && match_non_max(c, a2, b2, e2, fi)) return true; - + if (!ok1 || !ok2 || (a1.is_zero() && a2.is_zero())) { _backtrack.released = false; return false; } SASSERT(b1.is_val()); SASSERT(b2.is_val()); - if (match_linear1(c, a1, b1, e1, a2, b2, e2, fi)) return true; @@ -262,12 +268,36 @@ namespace polysat { return false; } + /** + * a*v <= 0, a odd + * forbidden interval for v is [1,0[ + */ + bool forbidden_intervals::match_zero( + signed_constraint const& c, + rational const & a1, pdd const& b1, pdd const& e1, + rational const & a2, pdd const& b2, pdd const& e2, + fi_record& fi) { + if (c.is_positive() && a1.is_odd() && b1.is_zero() && a2.is_zero() && b2.is_zero()) { + auto& m = e1.manager(); + rational lo_val(1); + auto lo = m.one(); + rational hi_val(0); + auto hi = m.zero(); + fi.coeff = 1; + fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val); + if (b1 != e1) + fi.side_cond.push_back(s.eq(b1, e1)); + if (b2 != e2) + fi.side_cond.push_back(s.eq(b2, e2)); + return true; + } + return false; + } + /** * v > q * forbidden interval for v is [0,1[ * - * Generalizations todo: - * * v - k > q * forbidden interval for v is [k,k+1[ * @@ -290,6 +320,21 @@ namespace polysat { fi.side_cond.push_back(s.eq(b1, e1)); return true; } + if (a1.is_odd() && b1.is_val() && !c.is_positive()) { + auto& m = e1.manager(); + rational const& mod_value = m.two_to_N(); + rational a1_inv; + VERIFY(a1.mult_inverse(m.power_of_2(), a1_inv)); + rational lo_val(mod(-b1.val() * a1_inv, mod_value)); + auto lo = -e1 * a1_inv; + rational hi_val(mod(lo_val + 1, mod_value)); + auto hi = lo + 1; + fi.coeff = 1; + fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val); + if (b1 != e1) + fi.side_cond.push_back(s.eq(b1, e1)); + return true; + } return false; } @@ -303,9 +348,18 @@ namespace polysat { signed_constraint const& c, rational const & a2, pdd const& b2, pdd const& e2, fi_record& fi) { - if (a2.is_one() && b2.is_zero() && !c.is_positive()) { - // todo - + if (a2.is_one() && b2.is_val() && !c.is_positive()) { + auto& m = e2.manager(); + rational const& mod_value = m.two_to_N(); + rational lo_val(mod(-b2.val() - 1, mod_value)); + auto lo = -e2 - 1; + rational hi_val(mod(lo_val + 1, mod_value)); + auto hi = -e2; + fi.coeff = 1; + fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val); + if (b2 != e2) + fi.side_cond.push_back(s.eq(b2, e2)); + return true; } return false; } diff --git a/src/math/polysat/forbidden_intervals.h b/src/math/polysat/forbidden_intervals.h index 463ec884f..4b8dc2d3e 100644 --- a/src/math/polysat/forbidden_intervals.h +++ b/src/math/polysat/forbidden_intervals.h @@ -52,6 +52,11 @@ namespace polysat { void add_non_unit_side_conds(fi_record& fi, pdd const& b1, pdd const& e1, pdd const& b2, pdd const& e2); + bool match_zero(signed_constraint const& c, + rational const & a1, pdd const& b1, pdd const& e1, + rational const & a2, pdd const& b2, pdd const& e2, + fi_record& fi); + bool match_non_zero(signed_constraint const& c, rational const & a1, pdd const& b1, pdd const& e1, fi_record& fi); diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index 33edc45fd..275a28ce6 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -1069,6 +1069,22 @@ public: } } + static void test_fi_nonzero() { + scoped_solver s(__func__); + auto a = s.var(s.add_var(5)); + auto b = s.var(s.add_var(5)); + s.add_ult(b*b*b, 7*a + 6); + s.check(); + } + + static void test_fi_nonmax() { + scoped_solver s(__func__); + auto a = s.var(s.add_var(5)); + auto b = s.var(s.add_var(5)); + s.add_ult(a + 8, b*b*b); + s.check(); + } + // Goal: we probably mix up polysat variables and PDD variables at several points; try to uncover such cases // NOTE: actually, add_var seems to keep them in sync, so this is not an issue at the moment (but we should still test it later) // static void test_mixed_vars() { @@ -1321,6 +1337,10 @@ public: void tst_polysat() { using namespace polysat; + test_polysat::test_fi_nonzero(); + test_polysat::test_fi_nonmax(); + return; + test_polysat::test_l2(); #if 0