From b22928bfc95b633e07a0c50eb9059168029cd28c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 22 May 2021 14:16:50 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/math/polysat/constraint.cpp | 1 + src/math/polysat/fixplex.h | 27 +++++++++++- src/math/polysat/fixplex_def.h | 66 +++++++++++++++++++++++++++--- src/math/polysat/linear_solver.cpp | 9 +++- src/math/polysat/linear_solver.h | 1 + 5 files changed, 96 insertions(+), 8 deletions(-) diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index 2d731b108..b4610b757 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -15,6 +15,7 @@ Author: #include "math/polysat/constraint.h" #include "math/polysat/solver.h" #include "math/polysat/log.h" +#include "math/polysat/log_helper.h" #include "math/polysat/var_constraint.h" #include "math/polysat/eq_constraint.h" #include "math/polysat/ule_constraint.h" diff --git a/src/math/polysat/fixplex.h b/src/math/polysat/fixplex.h index 5a4f53a98..7d890de1c 100644 --- a/src/math/polysat/fixplex.h +++ b/src/math/polysat/fixplex.h @@ -43,6 +43,7 @@ namespace polysat { virtual void restore_bound() = 0; virtual void add_le(var_t v, var_t w) = 0; virtual void add_lt(var_t v, var_t w) = 0; + virtual void restore_ineq() = 0; }; @@ -128,6 +129,15 @@ namespace polysat { fix_entry():x(null_var), r(0) {} }; + struct ineq { + var_t v { null_var }; + var_t w { null_var }; + bool strict { false }; + bool is_active { true }; + ineq(var_t v, var_t w, bool s): + v(v), w(w), strict(s) {} + }; + static const var_t null_var = UINT_MAX; reslimit& m_limit; mutable manager m; @@ -148,6 +158,13 @@ namespace polysat { vector m_stashed_bounds; map m_value2fixed_var; + // inequalities + svector m_ineqs; + unsigned_vector m_ineqs_to_check; + bool_vector m_var_is_touched; + vector m_var2ineqs; + svector m_vars_to_untouch; + public: fixplex(reslimit& lim): m_limit(lim), @@ -164,8 +181,9 @@ namespace polysat { void set_bounds(var_t v, rational const& lo, rational const& hi) override; void set_value(var_t v, rational const& val) override; void restore_bound() override; - void add_le(var_t v, var_t w) override; - void add_lt(var_t v, var_t w) override; + void add_le(var_t v, var_t w) override { add_ineq(v, w, false); } + void add_lt(var_t v, var_t w) override { add_ineq(v, w, true); } + virtual void restore_ineq() override; void set_bounds(var_t v, numeral const& lo, numeral const& hi); void unset_bounds(var_t v) { m_vars[v].set_free(); } @@ -235,6 +253,11 @@ namespace polysat { pivot_strategy_t pivot_strategy() { return m_bland ? S_BLAND : S_DEFAULT; } var_t select_error_var(bool least); + // facilities for handling inequalities + void add_ineq(var_t v, var_t w, bool strict); + void touch_var(var_t x); + lbool check_ineqs(); + bool is_solved(row const& r) const; bool is_solved(var_t v) const { SASSERT(is_base(v)); return is_solved(base2row(v)); } diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h index 404667e3d..b072a9b54 100644 --- a/src/math/polysat/fixplex_def.h +++ b/src/math/polysat/fixplex_def.h @@ -76,11 +76,13 @@ namespace polysat { return l_false; case l_undef: m_to_patch.insert(v); + if (l_false == check_ineqs()) + return l_false; return l_undef; } } SASSERT(well_formed()); - return l_true; + return check_ineqs(); } template @@ -226,6 +228,7 @@ namespace polysat { if (delta == 0) return; m_vars[v].m_value += delta; + touch_var(v); SASSERT(!is_base(v)); // @@ -473,15 +476,66 @@ namespace polysat { } template - void fixplex::add_le(var_t v, var_t w) { - NOT_IMPLEMENTED_YET(); + void fixplex::add_ineq(var_t v, var_t w, bool strict) { + unsigned idx = m_ineqs.size(); + m_var2ineqs.reserve(std::max(v, w) + 1); + m_var2ineqs[v].push_back(idx); + m_var2ineqs[w].push_back(idx); + m_ineqs_to_check.push_back(idx); + m_ineqs.push_back(ineq(v, w, strict)); } template - void fixplex::add_lt(var_t v, var_t w) { - NOT_IMPLEMENTED_YET(); + void fixplex::restore_ineq() { + auto ineq = m_ineqs.back(); + m_var2ineqs[ineq.v].pop_back(); + m_var2ineqs[ineq.w].pop_back(); + m_ineqs.pop_back(); } + template + void fixplex::touch_var(var_t v) { + if (v >= m_var2ineqs.size()) + return; + if (m_var_is_touched.get(v, false)) + return; + m_var_is_touched.set(v, true); + for (auto idx : m_var2ineqs[v]) { + if (!m_ineqs[idx].is_active) { + m_ineqs[idx].is_active = true; + m_ineqs_to_check.push_back(idx); + } + } + } + + template + lbool fixplex::check_ineqs() { + m_vars_to_untouch.reset(); + for (auto idx : m_ineqs_to_check) { + if (idx >= m_ineqs.size()) + continue; + auto& ineq = m_ineqs[idx]; + var_t v = ineq.v; + var_t w = ineq.w; + if (ineq.strict && value(v) >= value(w)) { + IF_VERBOSE(0, verbose_stream() << "violated v" << v << " < v" << w << "\n"); + return l_false; + } + if (ineq.strict && value(v) > value(w)) { + IF_VERBOSE(0, verbose_stream() << "violated v" << v << " <= v" << w << "\n"); + return l_false; + } + ineq.is_active = false; + m_vars_to_untouch.push_back(v); + m_vars_to_untouch.push_back(w); + } + for (auto v : m_vars_to_untouch) + m_var_is_touched.set(v, false); + m_ineqs_to_check.reset(); + m_vars_to_untouch.reset(); + return l_true; + } + /** * Check if the coefficient b of y has the minimal number of trailing zeros. @@ -615,6 +669,7 @@ namespace polysat { set_base_value(y); xI.m_is_base = false; xI.m_value = new_value; + touch_var(x); row r_x(rx); add_patch(y); SASSERT(well_formed_row(r_x)); @@ -815,6 +870,7 @@ namespace polysat { SASSERT(is_base(x)); row r = base2row(x); m_vars[x].m_value = solve_for(row2value(r), row2base_coeff(r)); + touch_var(x); bool was_integral = row_is_integral(r); m_rows[r.id()].m_integral = is_solved(r); if (was_integral && !row_is_integral(r)) diff --git a/src/math/polysat/linear_solver.cpp b/src/math/polysat/linear_solver.cpp index 308629dcb..80203481c 100644 --- a/src/math/polysat/linear_solver.cpp +++ b/src/math/polysat/linear_solver.cpp @@ -53,6 +53,12 @@ namespace polysat { m_rows.pop_back(); break; } + case trail_i::add_ineq_i: { + auto [v, sz] = m_rows.back(); + sz2fixplex(sz).restore_ineq(); + m_rows.pop_back(); + break; + } default: UNREACHABLE(); } @@ -179,7 +185,8 @@ namespace polysat { fp.add_le(v, w); else fp.add_lt(w, v); - + m_trail.push_back(trail_i::add_ineq_i); + m_rows.push_back(std::make_pair(v, sz)); } void linear_solver::new_bit(var_constraint& c) { diff --git a/src/math/polysat/linear_solver.h b/src/math/polysat/linear_solver.h index bd05dc6d1..6c2aaadb6 100644 --- a/src/math/polysat/linear_solver.h +++ b/src/math/polysat/linear_solver.h @@ -42,6 +42,7 @@ namespace polysat { add_var_i, add_mono_i, set_bound_i, + add_ineq_i, add_row_i };