From 1e3c3dc48f747f4d3c9ffada53fd7c9ea74f69cd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Aug 2021 11:58:19 -0700 Subject: [PATCH] enable fixed propagation from inequalities Signed-off-by: Nikolaj Bjorner --- src/math/bigfix/u256.cpp | 5 ++ src/math/bigfix/u256.h | 1 + src/math/polysat/fixplex.h | 35 ++++++++----- src/math/polysat/fixplex_def.h | 84 +++++++++++++++++------------- src/math/polysat/linear_solver.cpp | 1 + 5 files changed, 76 insertions(+), 50 deletions(-) diff --git a/src/math/bigfix/u256.cpp b/src/math/bigfix/u256.cpp index c0cb61a68..71bfe34ff 100644 --- a/src/math/bigfix/u256.cpp +++ b/src/math/bigfix/u256.cpp @@ -43,6 +43,11 @@ u256::u256(uint64_t const* v) { std::uninitialized_copy(v, v + 4, m_num); } +unsigned u256::hash() const { + uint64_t h = m_num[0] + m_num[1] + m_num[2] + m_num[3]; + return static_cast(h ^ (h >> 32ull)); +} + u256 u256::operator*(u256 const& other) const { // TBD: maybe just use mpn_manager::mul? uint64_t result[8]; diff --git a/src/math/bigfix/u256.h b/src/math/bigfix/u256.h index 41a146d48..54f57e319 100644 --- a/src/math/bigfix/u256.h +++ b/src/math/bigfix/u256.h @@ -16,6 +16,7 @@ public: *this = u256(n); return *this; } + unsigned hash() const; u256 operator*(u256 const& other) const; u256 operator+(u256 const& other) const { u256 r = *this; return r += other; } u256 operator-(u256 const& other) const { u256 r = *this; return r -= other; } diff --git a/src/math/polysat/fixplex.h b/src/math/polysat/fixplex.h index 888184b98..34571b897 100644 --- a/src/math/polysat/fixplex.h +++ b/src/math/polysat/fixplex.h @@ -33,6 +33,11 @@ Author: inline rational to_rational(uint64_t n) { return rational(n, rational::ui64()); } inline unsigned trailing_zeros(unsigned short n) { return trailing_zeros((uint32_t)n); } inline unsigned trailing_zeros(unsigned char n) { return trailing_zeros((uint32_t)n); } +inline unsigned numeral2hash(unsigned char const& n) { return n; } +inline unsigned numeral2hash(unsigned short const& n) { return n; } +inline unsigned numeral2hash(uint32_t const& n) { return n; } +inline unsigned numeral2hash(uint64_t const& n) { return static_cast(n ^ (n >> 32)); } + namespace polysat { @@ -86,9 +91,9 @@ namespace polysat { struct var_eq { var_t x, y; - row r1, r2; - var_eq(var_t x, var_t y, row const& r1, row const& r2): - x(x), y(y), r1(r1), r2(r2) {} + u_dependency* dep; + var_eq(var_t x, var_t y, u_dependency* dep): + x(x), y(y), dep(dep) {} }; protected: @@ -152,10 +157,10 @@ namespace polysat { }; struct fix_entry { - var_t x; - row r; - fix_entry(var_t x, row const& r): x(x), r(r) {} - fix_entry():x(null_var), r(0) {} + var_t x = null_var; + u_dependency* dep = nullptr; + fix_entry(var_t x, u_dependency* dep): x(x), dep(dep) {} + fix_entry() {} }; enum trail_i { @@ -163,7 +168,9 @@ namespace polysat { set_bound_i, set_inconsistent_i, add_ineq_i, - add_row_i + add_row_i, + add_eq_i, + fixed_val_i }; static const var_t null_var = UINT_MAX; @@ -177,6 +184,7 @@ namespace polysat { vector m_vars; vector m_rows; vector m_var_eqs; + vector m_fixed_vals; bool m_bland = false ; unsigned m_blands_rule_threshold = 1000; unsigned m_num_repeated = 0; @@ -238,12 +246,11 @@ namespace polysat { unsigned get_num_vars() const { return m_vars.size(); } void reset(); - svector> stack; + svector> stack; uint_set on_stack; - lbool propagate_ineqs(ineq& i0); + lbool propagate_ineqs(unsigned idx); void propagate_eqs(); vector const& var_eqs() const { return m_var_eqs; } - void reset_eqs() { m_var_eqs.reset(); } void add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs); @@ -268,8 +275,8 @@ namespace polysat { bool is_offset_row(row const& r, numeral& cx, var_t& x, numeral& cy, var_t & y) const; void lookahead_eq(row const& r1, numeral const& cx, var_t x, numeral const& cy, var_t y); void get_offset_eqs(row const& r); - void fixed_var_eh(row const& r, var_t x); - void eq_eh(var_t x, var_t y, row const& r1, row const& r2); + void fixed_var_eh(u_dependency* dep, var_t x); + void eq_eh(var_t x, var_t y, u_dependency* dep); bool propagate_row(row const& r); bool propagate_ineq(ineq const& i); bool propagate_strict_bounds(ineq const& i); @@ -349,7 +356,7 @@ namespace polysat { typedef uint_type numeral; struct hash { unsigned operator()(numeral const& n) const { - return static_cast(n); + return numeral2hash(n); } }; struct eq { diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h index 86353ede8..6eaf17b03 100644 --- a/src/math/polysat/fixplex_def.h +++ b/src/math/polysat/fixplex_def.h @@ -82,7 +82,6 @@ namespace polysat { reset(); } - template void fixplex::updt_params(params_ref const& p) { m_max_iterations = p.get_uint("max_iterations", m_max_iterations); @@ -117,6 +116,13 @@ namespace polysat { m_inconsistent = false; m_unsat_core.reset(); break; + case trail_i::add_eq_i: + m_var_eqs.pop_back(); + break; + case trail_i::fixed_val_i: + m_value2fixed_var.erase(m_fixed_vals.back()); + m_fixed_vals.pop_back(); + break; default: UNREACHABLE(); } @@ -142,7 +148,6 @@ namespace polysat { m_rows.reset(); m_left_basis.reset(); m_base_vars.reset(); - m_var_eqs.reset(); } template @@ -275,7 +280,6 @@ namespace polysat { template void fixplex::del_row(row const& r) { - m_var_eqs.reset(); var_t var = row2base(r); m_vars[var].m_is_base = false; m_vars[var].set_free(); @@ -668,13 +672,12 @@ namespace polysat { template bool fixplex::propagate() { lbool r; - for (unsigned idx : m_ineqs_to_propagate) { - if (idx >= m_ineqs.size()) - continue; - if (r = propagate_ineqs(m_ineqs[idx]), r == l_false) + while (!m_ineqs_to_propagate.empty()) { + unsigned idx = *m_ineqs_to_propagate.begin(); + if (idx < m_ineqs.size() && (r = propagate_ineqs(idx), r == l_false)) return false; - } - m_ineqs_to_propagate.reset(); + m_ineqs_to_propagate.remove(idx); + } return true; } @@ -1111,9 +1114,9 @@ namespace polysat { std::swap(cz, cu); } if (z == x && u != y && cx == cz && cu == cy && value(u) == value(y)) - eq_eh(u, y, r1, r2); + eq_eh(u, y, m_deps.mk_join(row2dep(r1), row2dep(r2))); if (z == x && u != y && cx + cz == 0 && cu + cy == 0 && value(u) == value(y)) - eq_eh(u, y, r1, r2); + eq_eh(u, y, m_deps.mk_join(row2dep(r1), row2dep(r2))); } } @@ -1122,18 +1125,24 @@ namespace polysat { * Accumulate equalities between variables fixed to the same values. */ template - void fixplex::fixed_var_eh(row const& r, var_t x) { + void fixplex::fixed_var_eh(u_dependency* dep, var_t x) { numeral val = value(x); fix_entry e; - if (m_value2fixed_var.find(val, e) && is_valid_variable(e.x) && is_fixed(e.x) && value(e.x) == val && e.x != x) - eq_eh(x, e.x, e.r, r); - else - m_value2fixed_var.insert(val, fix_entry(x, r)); + if (m_value2fixed_var.find(val, e)) { + SASSERT(x != e.x); + eq_eh(x, e.x, m_deps.mk_join(e.dep, dep)); + } + else { + m_value2fixed_var.insert(val, fix_entry(x, dep)); + m_fixed_vals.push_back(val); + m_trail.push_back(trail_i::fixed_val_i); + } } template - void fixplex::eq_eh(var_t x, var_t y, row const& r1, row const& r2) { - m_var_eqs.push_back(var_eq(x, y, r1, r2)); + void fixplex::eq_eh(var_t x, var_t y, u_dependency* dep) { + m_var_eqs.push_back(var_eq(x, y, dep)); + m_trail.push_back(trail_i::add_eq_i); } #if 0 @@ -1165,7 +1174,8 @@ namespace polysat { // template - lbool fixplex::propagate_ineqs(ineq& i0) { + lbool fixplex::propagate_ineqs(unsigned i0_idx) { + ineq i0 = m_ineqs[i0_idx]; numeral old_lo = m_vars[i0.w].lo; SASSERT(!m_inconsistent); // std::cout << "propagate " << i0 << "\n"; @@ -1173,12 +1183,13 @@ namespace polysat { return l_false; on_stack.reset(); stack.reset(); - stack.push_back(std::make_pair(0, i0)); + stack.push_back(std::make_pair(0, i0_idx)); on_stack.insert(i0.v); while (!stack.empty()) { if (!m_limit.inc()) return l_undef; - auto [ineq_out, i] = stack.back(); + auto [ineq_out, i_idx] = stack.back(); + ineq i = m_ineqs[i_idx]; auto const& ineqs = m_var2ineqs[i.w]; for (; ineq_out < ineqs.size(); ++ineq_out) { auto& i_out = m_ineqs[ineqs[ineq_out]]; @@ -1192,10 +1203,10 @@ namespace polysat { return l_false; bool is_onstack = on_stack.contains(i_out.w); - if ((old_lo != m_vars[i_out.w].lo) && !is_onstack) { + if ((old_lo != m_vars[i_out.w].lo || m_ineqs_to_propagate.contains(ineqs[ineq_out])) && !is_onstack) { on_stack.insert(i_out.w); stack.back().first = ineq_out + 1; - stack.push_back(std::make_pair(0, i_out)); + stack.push_back(std::make_pair(0, ineqs[ineq_out])); break; } @@ -1208,7 +1219,7 @@ namespace polysat { auto bound = m_vars[i_out.w]; unsigned j = stack.size(); for (; !found && j-- > 0; ) { - ineq i2 = stack[j].second; + ineq i2 = m_ineqs[stack[j].second]; strict |= i2.strict; bound &= m_vars[i2.w]; if (i2.v == i_out.w) @@ -1219,12 +1230,13 @@ namespace polysat { if ((empty || strict) && found) { auto* d = i_out.dep; for (; j < stack.size(); ++j) - d = m_deps.mk_join(d, stack[j].second.dep); + d = m_deps.mk_join(d, m_ineqs[stack[j].second].dep); conflict(d); return l_false; } } if (ineq_out == ineqs.size()) { + m_ineqs_to_propagate.remove(i_idx); on_stack.remove(i.w); stack.pop_back(); } @@ -1523,36 +1535,36 @@ namespace polysat { d = m_deps.mk_join(m_vars[v].m_lo_dep, d); d = m_deps.mk_join(m_vars[v].m_hi_dep, d); } -return d; + return d; } template bool fixplex::new_bound(ineq const& i, var_t x, numeral const& l, numeral const& h, u_dependency* a, u_dependency* b, u_dependency* c, u_dependency* d) { - bool was_fixed = lo(x) + 1 == hi(x); + bool was_fixed = is_fixed(x); SASSERT(!inconsistent()); u_dependency* dep = m_deps.mk_join(i.dep, m_deps.mk_join(a, m_deps.mk_join(b, m_deps.mk_join(c, d)))); update_bounds(x, l, h, dep); if (inconsistent()) return false; - else if (!was_fixed && lo(x) + 1 == hi(x)) { - // TBD: track based on inequality not row - // fixed_var_eh(r, x); - } + if (!was_fixed && is_fixed(x)) + fixed_var_eh(dep, x); + return true; } template bool fixplex::new_bound(row const& r, var_t x, mod_interval const& range) { - if (range.is_free()) + if (range.contains(m_vars[x])) return l_true; SASSERT(!inconsistent()); - bool was_fixed = lo(x) + 1 == hi(x); - update_bounds(x, range.lo, range.hi, row2dep(r)); + bool was_fixed = is_fixed(x); + u_dependency* dep = row2dep(r); + update_bounds(x, range.lo, range.hi, dep); IF_VERBOSE(0, verbose_stream() << "new-bound v" << x << " " << m_vars[x] << "\n"); if (inconsistent()) return false; - else if (!was_fixed && lo(x) + 1 == hi(x)) - fixed_var_eh(r, x); + if (!was_fixed && is_fixed(x)) + fixed_var_eh(dep, x); return true; } diff --git a/src/math/polysat/linear_solver.cpp b/src/math/polysat/linear_solver.cpp index bb4ff01a2..fbd61999e 100644 --- a/src/math/polysat/linear_solver.cpp +++ b/src/math/polysat/linear_solver.cpp @@ -17,6 +17,7 @@ Author: #include "math/polysat/fixplex_def.h" #include "math/polysat/solver.h" +inline unsigned numeral2hash(u256 const& n) { return n.hash(); } namespace polysat {