From 444084f39608ecb257026053a6fcd34b895fa976 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Sep 2021 11:30:50 -0700 Subject: [PATCH] add notes and tangent lemma Signed-off-by: Nikolaj Bjorner --- src/math/polysat/saturation.cpp | 25 ++++++++++++++++++++++++ src/math/polysat/saturation.h | 2 ++ src/math/polysat/solver.cpp | 2 -- src/math/polysat/solver.h | 2 ++ src/math/polysat/ule_constraint.cpp | 30 ++++++++++++++++++----------- src/math/polysat/ule_constraint.h | 1 + 6 files changed, 49 insertions(+), 13 deletions(-) diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index 50153256e..785e63292 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -42,6 +42,8 @@ namespace polysat { return true; if (try_y_l_ax_and_x_l_z(v, core, c)) return true; + if (try_tangent(v, core, c)) + return true; } return false; } @@ -380,4 +382,27 @@ namespace polysat { return propagate(core, z_l_y, yx_l_zx, z_l_y.is_strict || yx_l_zx.is_strict, y * x, y_prime * x, new_constraints); } + // [x] p(x) <= q(x) where value(p) > value(q) + // ==> q <= value(q) => p <= value(q) + + bool inf_saturate::try_tangent(pvar v, conflict& core, inequality const& c) { + if (!c.src->contains_var(v)) + return false; + if (c.lhs.is_val() || c.rhs.is_val()) + return false; + if (!c.as_signed_constraint().is_currently_false(s())) + return false; + rational l_val, r_val; + if (!s().try_eval(c.lhs, l_val)) + return false; + if (!s().try_eval(c.rhs, r_val)) + return false; + SASSERT(c.is_strict || l_val > r_val); + SASSERT(!c.is_strict || l_val >= r_val); + vector new_constraints; + new_constraints.push_back(c.as_signed_constraint()); + new_constraints.push_back(s().ule(c.rhs, r_val)); + return propagate(core, c, c, c.is_strict ? s().ult(c.lhs, r_val) : s().ule(c.lhs, r_val), new_constraints); + } + } diff --git a/src/math/polysat/saturation.h b/src/math/polysat/saturation.h index 612f7b3a6..e334c56ed 100644 --- a/src/math/polysat/saturation.h +++ b/src/math/polysat/saturation.h @@ -54,6 +54,8 @@ namespace polysat { bool try_ugt_z(pvar z, conflict& core, inequality const& c); bool try_ugt_z(pvar z, conflict& core, inequality const& x_l_z0, inequality const& yz_l_xz, pdd const& y, pdd const& x); + bool try_tangent(pvar v, conflict& core, inequality const& c); + // c := lhs ~ v // where ~ is < or <= bool is_l_v(pvar v, inequality const& c); diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 221dc3612..b1c0ee320 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -640,8 +640,6 @@ namespace polysat { } m_conflict.reset(); - std::cout << "reason " << *reason << "\n"; - // The lemma where 'lit' comes from. // Currently, boolean decisions always come from guessing a literal of a learned non-unit lemma. clause* lemma = m_bvars.lemma(var); // need to grab this while 'lit' is still assigned diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index f9584dfae..9ea25554a 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -267,7 +267,9 @@ namespace polysat { signed_constraint eq(pdd const& p, rational const& q) { return eq(p - q); } signed_constraint diseq(pdd const& p, rational const& q) { return diseq(p - q); } signed_constraint ule(pdd const& p, pdd const& q) { return m_constraints.ule(p, q); } + signed_constraint ule(pdd const& p, rational const& q) { return m_constraints.ule(p, p.manager().mk_val(q)); } signed_constraint ult(pdd const& p, pdd const& q) { return m_constraints.ult(p, q); } + signed_constraint ult(pdd const& p, rational const& q) { return m_constraints.ult(p, p.manager().mk_val(q)); } signed_constraint sle(pdd const& p, pdd const& q) { return m_constraints.sle(p, q); } signed_constraint slt(pdd const& p, pdd const& q) { return m_constraints.slt(p, q); } diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index d68bb4089..1b6cb7843 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -12,16 +12,17 @@ Author: Notes: - TODO: Maybe we want to rewrite some of the following into equalities? (i.e., into p<=0) + TODO: add rewrite rules to simplify expressions + + - k1 <= k2 ==> 0 <= 0 if k1 <= k2 + - k1 <= k2 ==> 1 <= 0 if k1 > k2 + - 0 <= p ==> 0 <= 0 + - p <= -1 ==> 0 <= 0 + - k*p <= 0 ==> p <= 0 if k is odd - p <= 0 <==> p = 0 - -1 <= p <==> p = -1 - 1 <= p <==> p != 0 - p <= -2 <==> p != -1 - - e.g. - x - 2 >= 1 <==> x != 2 - 2 - x >= -1 <==> x = 3 + - k <= p ==> p - k <= k - 1 + - p <= p + q ==> p <= -q - 1 + - p + k <= p ==> p + k <= k - 1 for k > 0 --*/ @@ -33,10 +34,17 @@ namespace polysat { ule_constraint::ule_constraint(constraint_manager& m, pdd const& l, pdd const& r) : constraint(m, ckind_t::ule_t), m_lhs(l), m_rhs(r) { - m_vars.append(l.free_vars()); - for (auto v : r.free_vars()) + + simplify(); + + m_vars.append(m_lhs.free_vars()); + for (auto v : m_rhs.free_vars()) if (!m_vars.contains(v)) m_vars.push_back(v); + + } + + void ule_constraint::simplify() { if (m_lhs.is_val() && m_rhs.is_val()) { if (m_lhs.val() <= m_rhs.val()) m_lhs = m_rhs = 0; diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h index 6ccfd5b0b..f5e732d54 100644 --- a/src/math/polysat/ule_constraint.h +++ b/src/math/polysat/ule_constraint.h @@ -24,6 +24,7 @@ namespace polysat { pdd m_rhs; ule_constraint(constraint_manager& m, pdd const& l, pdd const& r); + void simplify(); public: ~ule_constraint() override {}