From 28864e563c439eec293d58e340af839d3c0e62d6 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 23 Dec 2021 18:36:27 +0100 Subject: [PATCH] First version of refine_disequal_lin --- src/math/dd/dd_pdd.h | 2 +- src/math/polysat/forbidden_intervals.cpp | 38 ++++++++++++-- src/math/polysat/forbidden_intervals.h | 5 ++ src/math/polysat/viable.cpp | 63 +++++++++++++++++++++++- src/math/polysat/viable.h | 3 +- 5 files changed, 103 insertions(+), 8 deletions(-) diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index ca8b73fd3..0b73be6e5 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -405,7 +405,7 @@ namespace dd { bool is_zero() const { return m.is_zero(root); } bool is_linear() const { return m.is_linear(root); } bool is_var() const { return m.is_var(root); } - /** Polynomial is of the form: a * x + b */ + /** Polynomial is of the form a * x + b for numerals a, b. */ bool is_unilinear() const { return !is_val() && lo().is_val() && hi().is_val(); } bool is_unary() const { return !is_val() && lo().is_zero() && hi().is_val(); } bool is_binary() const { return m.is_binary(root); } diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index dc2d223f7..a1b92de4f 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -47,17 +47,15 @@ namespace polysat { fi.coeff = 1; fi.src = c; + // eval(lhs) = a1*v + eval(e1) = a1*v + b1 + // eval(rhs) = a2*v + eval(e2) = a2*v + b2 + // We keep the e1, e2 around in case we need side conditions such as e1=b1, e2=b2. auto [ok1, a1, e1, b1] = linear_decompose(v, c->to_ule().lhs(), fi.side_cond); auto [ok2, a2, e2, b2] = linear_decompose(v, c->to_ule().rhs(), fi.side_cond); if (!ok1 || !ok2 || (a1.is_zero() && a2.is_zero())) return false; SASSERT(b1.is_val()); SASSERT(b2.is_val()); - - // TBD: use fi.coeff = -1 to tell caller to treat it as a diseq_lin. - // record a1, a2, b1, b2 for fast access, add non_unit side conditions on b1 = e1, b2 = e2? - if (a1 != a2 && !a1.is_zero() && !a2.is_zero()) - return false; _backtrack.released = true; @@ -67,6 +65,8 @@ namespace polysat { return true; if (match_linear3(c, a1, b1, e1, a2, b2, e2, fi)) return true; + if (match_linear4(c, a1, b1, e1, a2, b2, e2, fi)) + return true; _backtrack.released = false; return false; @@ -88,12 +88,16 @@ namespace polysat { pdd e = m.zero(); unsigned const deg = p.degree(v); if (deg == 0) + // p = 0*v + e e = p; else if (deg == 1) + // p = q*v + e p.factor(v, 1, q, e); else return std::tuple(false, rational(0), q, e); + // r := eval(q) + // Add side constraint q = r. if (!q.is_val()) { pdd r = q.subst_val(s.assignment()); if (!r.is_val()) @@ -221,6 +225,30 @@ namespace polysat { return false; } + /** + * e1 + t <= e2 + t', with t = a1*y, t' = a2*y, a1 != a2, a1, a2 non-zero + */ + bool forbidden_intervals::match_linear4(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 (a1 != a2 && !a1.is_zero() && !a2.is_zero()) { + // NOTE: we don't have an interval here in the same sense as in the other cases. + // We use the interval to smuggle out the values a1,b1,a2,b2 without adding additional fields. + // to_interval flips a1,b1 with a2,b2 for negative constraints, which we also need for this case. + auto lo = b1; + rational lo_val = a1; + auto hi = b2; + rational hi_val = a2; + // We use fi.coeff = -1 to tell the caller to treat it as a diseq_lin. + fi.coeff = -1; + fi.interval = to_interval(c, false, fi.coeff, lo_val, lo, hi_val, hi); + add_non_unit_side_conds(fi, b1, e1, b2, e2); + return true; + } + return false; + } + void forbidden_intervals::add_non_unit_side_conds(fi_record& fi, pdd const& b1, pdd const& e1, pdd const& b2, pdd const& e2) { if (fi.coeff == 1) return; diff --git a/src/math/polysat/forbidden_intervals.h b/src/math/polysat/forbidden_intervals.h index 6eef58eb0..062a49c7d 100644 --- a/src/math/polysat/forbidden_intervals.h +++ b/src/math/polysat/forbidden_intervals.h @@ -45,6 +45,11 @@ namespace polysat { rational const & a2, pdd const& b2, pdd const& e2, fi_record& fi); + bool match_linear4(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); + void add_non_unit_side_conds(fi_record& fi, pdd const& b1, pdd const& e1, pdd const& b2, pdd const& e2); public: diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 29dcce50e..912b29b25 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -276,7 +276,67 @@ namespace polysat { auto* e = m_diseq_lin[v]; if (!e) return true; - LOG("refine-disequal-lin is TBD"); + entry* first = e; + rational const& max_value = s.var2pdd(v).max_value(); + rational mod_value = max_value + 1; + + do { + LOG("refine-disequal-lin for src: " << e->src); + // We have: + // a1*v + b1 > a2*v + b2 if e->src.is_positive() + // a1*v + b1 >= a2*v + b2 if e->src.is_negative() + // Note that e->interval is meaningless in this case, + // we just use it to transport the values a1,b1,a2,b2. + rational const& a1 = e->interval.lo_val(); + rational const& b1 = e->interval.lo().val(); + rational const& a2 = e->interval.hi_val(); + rational const& b2 = e->interval.hi().val(); + rational lhs = a1 * val + b1; + rational rhs = a2 * val + b2; + + auto delta_l = [&](rational const& val) { + rational m1 = ceil((rhs + 1) / a2); + int corr = e->src.is_negative() ? 1 : 0; + rational m3 = (lhs - rhs + corr) / (a1 - a2); + if (m3 <= 0) + m3 = m1; // remove m3 from the minimum + + return std::min(m1, m3) - 1; + }; + auto delta_u = [&](rational const& val) { + rational m1 = ceil((mod_value - lhs) / a1); + rational m2 = mod_value - val; + int corr = e->src.is_negative() ? 1 : 0; + rational m3 = (lhs - rhs + corr) / (a2 - a1); + if (m3 <= 0) + m3 = m2; // remove m3 from the minimum + + return std::min(m1, std::min(m2, m3)) - 1; + }; + + if (lhs > rhs || (e->src.is_negative() && lhs == rhs)) { + rational lo = val - delta_l(val); + rational hi = val + delta_u(val) + 1; + + // TODO: increase interval + LOG("refine-disequal-lin: " << " [" << lo << ", " << hi << "["); + // SASSERT(false); + + SASSERT(0 <= lo); + SASSERT(hi <= max_value); + pdd lop = s.var2pdd(v).mk_val(lo); + pdd hip = s.var2pdd(v).mk_val(hi); + entry* ne = alloc_entry(); + ne->src = e->src; + ne->side_cond = e->side_cond; + ne->coeff = 1; + ne->interval = eval_interval::proper(lop, lo, hip, hi); + intersect(v, ne); + return false; + } + e = e->next(); + } + while (e != first); return true; } @@ -313,6 +373,7 @@ namespace polysat { } while (e != first); return false; +#undef CHECK_RETURN } bool viable::is_viable(pvar v, rational const& val) { diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index feb01af25..1297cd039 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -74,7 +74,8 @@ namespace polysat { /** * update state of viable for pvar v - * based on affine constraints + * based on affine constraints. + * Returns true if the state has been changed. */ bool intersect(pvar v, signed_constraint const& c);