From 417a5320c710b8b6eb8b4db63546188fad6d45f3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 22 Jan 2022 11:14:53 +0100 Subject: [PATCH] forbidden intervals for strict inequalities Signed-off-by: Nikolaj Bjorner --- src/math/polysat/explain.cpp | 1 - src/math/polysat/forbidden_intervals.cpp | 65 +++++++++++++++++++++++- src/math/polysat/forbidden_intervals.h | 8 +++ src/math/polysat/solver.cpp | 2 +- src/math/polysat/ule_constraint.cpp | 38 ++++++++------ 5 files changed, 95 insertions(+), 19 deletions(-) diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp index 0b12155d9..6d09e59cf 100644 --- a/src/math/polysat/explain.cpp +++ b/src/math/polysat/explain.cpp @@ -176,7 +176,6 @@ namespace polysat { core.reset(); LOG_H3("Polynomial superposition " << eq << " " << c << " reduced to " << c2); if (c2.bvalue(s) == l_false) { - UNREACHABLE(); // TODO this loops or crashes depending on whether we // return true or false. core.insert(eq); diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index b0f154a30..1960079e0 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -52,12 +52,24 @@ namespace polysat { // 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())) + + _backtrack.released = true; + + // v > q + 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()); - _backtrack.released = true; if (match_linear1(c, a1, b1, e1, a2, b2, e2, fi)) return true; @@ -250,6 +262,55 @@ namespace polysat { return false; } + /** + * v > q + * forbidden interval for v is [0,1[ + * + * Generalizations todo: + * + * v - k > q + * forbidden interval for v is [k,k+1[ + * + * a*v - k > q, a odd + * forbidden interval for v is [a^-1*k, a^-1*k + 1[ + */ + bool forbidden_intervals::match_non_zero( + signed_constraint const& c, + rational const & a1, pdd const& b1, pdd const& e1, + fi_record& fi) { + if (a1.is_odd() && b1.is_zero() && !c.is_positive()) { + auto& m = e1.manager(); + rational lo_val(0); + auto lo = m.zero(); + rational hi_val(1); + auto hi = m.one(); + 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; + } + + /** + * p > v + * forbidden interval for v is [-1,0[ + * p > v + k + * forbidden interval for v is [-k-1,-k[ + */ + bool forbidden_intervals::match_non_max( + 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 + + } + 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 062a49c7d..463ec884f 100644 --- a/src/math/polysat/forbidden_intervals.h +++ b/src/math/polysat/forbidden_intervals.h @@ -52,6 +52,14 @@ 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_non_zero(signed_constraint const& c, + rational const & a1, pdd const& b1, pdd const& e1, + fi_record& fi); + + bool match_non_max(signed_constraint const& c, + rational const & a2, pdd const& b2, pdd const& e2, + fi_record& fi); + public: forbidden_intervals(solver& s) :s(s) {} bool get_interval(signed_constraint const& c, pvar v, fi_record& fi); diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 07191f63c..cf66b3c48 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -831,7 +831,7 @@ namespace polysat { // Add lemma to storage void solver::add_clause(clause& clause) { - LOG("Lemma: " << clause); + LOG((clause.is_redundant() ? "Lemma: ": "Aux: ") << clause); for (sat::literal lit : clause) { LOG(" Literal " << lit << " is: " << lit2cnstr(lit)); // SASSERT(m_bvars.value(lit) != l_true); diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index 4581bb581..4e7510aff 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -125,7 +125,9 @@ namespace polysat { auto p = lhs().subst_val(s.assignment()); auto q = rhs().subst_val(s.assignment()); - LOG_H3("Narrowing " << *this); + signed_constraint sc(this, is_positive); + + LOG_H3("Narrowing " << sc); LOG("Assignment: " << assignments_pp(s)); LOG("Substituted LHS: " << lhs() << " := " << p); LOG("Substituted RHS: " << rhs() << " := " << q); @@ -141,26 +143,32 @@ namespace polysat { } pvar v = null_var; + bool first = true; if (p.is_unilinear()) v = p.var(); else if (q.is_unilinear()) - v = q.var(); + v = q.var(), first = false; else return; - signed_constraint sc(this, is_positive); - if (!s.m_viable.intersect(v, sc)) - return; - rational val; - switch (s.m_viable.find_viable(v, val)) { - case dd::find_t::singleton: - s.propagate(v, val, sc); // TBD why is sc used as justification? It should be all of viable - break; - case dd::find_t::empty: - s.set_conflict(v); - break; - default: - break; + try_viable: + if (s.m_viable.intersect(v, sc)) { + rational val; + switch (s.m_viable.find_viable(v, val)) { + case dd::find_t::singleton: + s.propagate(v, val, sc); // TBD why is sc used as justification? It should be all of viable + break; + case dd::find_t::empty: + s.set_conflict(v); + return; + default: + break; + } + } + if (first && q.is_unilinear() && q.var() != v) { + v = q.var(); + first = false; + goto try_viable; } }