From 0bec8520e19ac9ecb85a51e0fa3af128952597e1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 10 Nov 2021 08:23:45 -0800 Subject: [PATCH] adding new viable using forbidden intervals Signed-off-by: Nikolaj Bjorner --- src/math/polysat/CMakeLists.txt | 1 + src/math/polysat/conflict.cpp | 6 +- src/math/polysat/forbidden_intervals.cpp | 30 ++--- src/math/polysat/forbidden_intervals.h | 3 +- src/math/polysat/solver.h | 1 + src/math/polysat/viable.cpp | 143 ----------------------- src/math/polysat/viable.h | 96 +-------------- src/math/polysat/viable2.cpp | 74 ++++++++++++ src/math/polysat/viable2.h | 101 ++++++++++++++++ 9 files changed, 201 insertions(+), 254 deletions(-) create mode 100644 src/math/polysat/viable2.cpp create mode 100644 src/math/polysat/viable2.h diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt index ddc5e7edc..f1a28ef58 100644 --- a/src/math/polysat/CMakeLists.txt +++ b/src/math/polysat/CMakeLists.txt @@ -15,6 +15,7 @@ z3_add_component(polysat solver.cpp ule_constraint.cpp viable.cpp + viable2.cpp variable_elimination.cpp COMPONENT_DEPENDENCIES util diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index b75a1fdd7..8d93243a8 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -264,8 +264,8 @@ namespace polysat { for (auto v : m_vars) a.push_back(std::make_pair(v, s.get_value(v))); for (unsigned i = 0; i < a.size(); ++i) { - auto save = a[i]; - auto last = a.back(); + std::pair save = a[i]; + std::pair last = a.back(); a[i] = last; a.pop_back(); if (c.is_currently_false(a)) @@ -278,7 +278,7 @@ namespace polysat { if (a.size() == m_vars.num_elems()) return; m_vars.reset(); - for (auto [v, val] : a) + for (auto const& [v, val] : a) m_vars.insert(v); LOG("reduced " << m_vars); } diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index 46220c748..b010ca8b8 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -147,9 +147,9 @@ namespace polysat { unsigned const next_i = seq[(seq_i + 1) % seq.size()]; // Build constraint: upper bound of each interval is not contained in the next interval, // using the equivalence: t \in [l;h[ <=> t-l < h-l - auto hi = records[i].interval.hi(); - auto next_lo = records[next_i].interval.lo(); - auto next_hi = records[next_i].interval.hi(); + auto const& hi = records[i].interval.hi(); + auto const& next_lo = records[next_i].interval.lo(); + auto const& next_hi = records[next_i].interval.hi(); auto lhs = hi - next_lo; auto rhs = next_hi - next_lo; signed_constraint c = s.m_constraints.ult(lhs, rhs); @@ -315,9 +315,9 @@ namespace polysat { bool is_trivial = (b2 + 1).is_zero(); push_eq(is_trivial, e2 + 1, side_cond); auto lo = e2 - e1 + 1; - auto lo_val = (b2 - b1 + 1).val(); + rational lo_val = (b2 - b1 + 1).val(); auto hi = -e1; - auto hi_val = (-b1).val(); + rational hi_val = (-b1).val(); interval = to_interval(c, is_trivial, a1, lo_val, lo, hi_val, hi); return true; } @@ -337,9 +337,9 @@ namespace polysat { bool is_trivial = b1.is_zero(); push_eq(is_trivial, e1, side_cond); auto lo = -e2; - auto lo_val = (-b2).val(); + rational lo_val = (-b2).val(); auto hi = e1 - e2; - auto hi_val = (b1 - b2).val(); + rational hi_val = (b1 - b2).val(); interval = to_interval(c, is_trivial, a2, lo_val, lo, hi_val, hi); return true; } @@ -358,9 +358,9 @@ namespace polysat { bool is_trivial = b1.val() == b2.val(); push_eq(is_trivial, e1 - e2, side_cond); auto lo = -e2; - auto lo_val = (-b2).val(); + rational lo_val = (-b2).val(); auto hi = -e1; - auto hi_val = (-b1).val(); + rational hi_val = (-b1).val(); interval = to_interval(c, is_trivial, a1, lo_val, lo, hi_val, hi); return true; } @@ -432,8 +432,8 @@ namespace polysat { a2 < b1.val() && e1.is_val()) { if (!e2.is_val()) side_cond.push_back(s.eq(e2)); - auto lo_val = rational::zero(); - auto hi_val = floor((b1.val() - 1) / a2) + 1; + rational lo_val = rational::zero(); + rational hi_val = floor((b1.val() - 1) / a2) + 1; SASSERT(lo_val < hi_val); auto lo = m.mk_val(lo_val); auto hi = m.mk_val(hi_val); @@ -447,8 +447,8 @@ namespace polysat { a1.is_zero() && e1.is_val() && a2 < b1.val()) { if (!e2.is_val()) side_cond.push_back(s.eq(e2)); - auto lo_val = ceil(b1.val() / a2); - auto hi_val = floor(m.max_value() / a2) + 1; + rational lo_val = ceil(b1.val() / a2); + rational hi_val = floor(m.max_value() / a2) + 1; auto lo = m.mk_val(lo_val); auto hi = m.mk_val(hi_val); interval = eval_interval::proper(lo, lo_val, hi, hi_val); @@ -461,8 +461,8 @@ namespace polysat { a2.is_zero() && e2.is_val() && a1 <= b2.val()) { if (!e1.is_val()) side_cond.push_back(s.eq(e2)); - auto lo_val = rational::zero(); - auto hi_val = floor(b2.val() / a1) + 1; + rational lo_val = rational::zero(); + rational hi_val = floor(b2.val() / a1) + 1; auto lo = m.mk_val(lo_val); auto hi = m.mk_val(hi_val); interval = eval_interval::proper(lo, lo_val, hi, hi_val); diff --git a/src/math/polysat/forbidden_intervals.h b/src/math/polysat/forbidden_intervals.h index 2eaec2920..d8e067c35 100644 --- a/src/math/polysat/forbidden_intervals.h +++ b/src/math/polysat/forbidden_intervals.h @@ -24,7 +24,7 @@ namespace polysat { solver& s; void revert_core(conflict& core); void full_interval_conflict(signed_constraint c, vector const & side_cond, conflict& core); - bool get_interval(signed_constraint const& c, pvar v, eval_interval& out_interval, vector& side_cond); + void push_eq(bool is_trivial, pdd const& p, vector& side_cond); eval_interval to_interval(signed_constraint const& c, bool is_trivial, rational const& coeff, rational & lo_val, pdd & lo, rational & hi_val, pdd & hi); @@ -61,5 +61,6 @@ namespace polysat { public: forbidden_intervals(solver& s) :s(s) {} bool perform(pvar v, vector const& just, conflict& core); + bool get_interval(signed_constraint const& c, pvar v, eval_interval& out_interval, vector& side_cond); }; } diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 19743ee16..cee4db49c 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -60,6 +60,7 @@ namespace polysat { friend class forbidden_intervals; friend class linear_solver; friend class viable; + friend class viable2; friend class assignment_pp; friend class assignments_pp; friend class ex_polynomial_superposition; diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 5015065d2..1a2fcd540 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -12,47 +12,25 @@ Author: Notes: -Use cheap heuristics to narrow viable sets whenever possible. -If the cheap heuristics fail, compute a BDD representing the viable sets -and narrow the range using the BDDs that are cached. - - --*/ #include "math/polysat/viable.h" #include "math/polysat/solver.h" -#if NEW_VIABLE -#include "math/polysat/viable_set_def.h" -#endif - namespace polysat { - viable::viable(solver& s): s(s), m_bdd(1000) {} viable::~viable() { -#if NEW_VIABLE - ptr_vector entries; - for (auto* e : m_constraint_cache) - entries.push_back(e); - m_constraint_cache.reset(); - for (auto* e : entries) - dealloc(e); -#endif } void viable::push_viable(pvar v) { s.m_trail.push_back(trail_instr_t::viable_i); -#if NEW_VIALBLE - m_viable_trail.push_back(std::make_pair(v, alloc(viable_set, *m_viable[v]))); -#else m_viable_trail.push_back(std::make_pair(v, m_viable[v])); -#endif } @@ -65,13 +43,6 @@ namespace polysat { // a*v + b == 0 or a*v + b != 0 void viable::intersect_eq(rational const& a, pvar v, rational const& b, bool is_positive) { -#if NEW_VIABLE - push_viable(v); - if (!m_viable[v]->intersect_eq(a, b, is_positive)) - intersect_eq_bdd(v, a, b, is_positive); - if (m_viable[v]->is_empty()) - s.set_conflict(v); -#else bddv const& x = var2bits(v).var(); if (b == 0 && a.is_odd()) { @@ -94,17 +65,9 @@ namespace polysat { bdd xs = is_positive ? lhs.all0() : !lhs.all0(); intersect_viable(v, xs); } -#endif } void viable::intersect_ule(pvar v, rational const& a, rational const& b, rational const& c, rational const& d, bool is_positive) { -#if NEW_VIABLE - push_viable(v); - if (!m_viable[v]->intersect_le(a, b, c, d, is_positive)) - intersect_ule_bdd(v, a, b, c, d, is_positive); - if (m_viable[v]->is_empty()) - s.set_conflict(v); -#else bddv const& x = var2bits(v).var(); // hacky special case if (a == 1 && b == 0 && c == 0 && d == 0) @@ -117,144 +80,40 @@ namespace polysat { bdd xs = is_positive ? (l <= r) : (l > r); intersect_viable(v, xs); } -#endif } -#if NEW_VIABLE - - viable::cached_constraint& viable::cache_constraint(pvar v, cached_constraint& entry0, std::function& mk_constraint) { - cached_constraint* other = nullptr; - if (!m_constraint_cache.find(&entry0, other)) { - gc_cached_constraints(); - other = alloc(cached_constraint, entry0); - other->repr = mk_constraint(); - m_constraint_cache.insert(other); - } - other->m_activity++; - return *other; - } - - void viable::gc_cached_constraints() { - // - // TODO: instead of using activity for GC, use the Move-To-Front approach - // see sat/smt/bv_ackerman.h or sat/smt/euf_ackerman.h - // where hash table entries use a dll_base. - // - unsigned max_entries = 10000; - if (m_constraint_cache.size() > max_entries) { - ptr_vector entries; - for (auto* e : m_constraint_cache) - entries.push_back(e); - std::stable_sort(entries.begin(), entries.end(), [&](cached_constraint* a, cached_constraint* b) { return a->m_activity < b->m_activity; }); - for (auto* e : entries) - e->m_activity /= 2; - for (unsigned i = 0; i < max_entries/2; ++i) { - m_constraint_cache.remove(entries[i]); - dealloc(entries[i]); - } - } - } - - void viable::narrow(pvar v, bdd const& is_false) { - rational bound = m_viable[v]->lo; - if (var2bits(v).sup(is_false, bound)) - m_viable[v]->update_lo(m_viable[v]->next(bound)); - bound = m_viable[v]->prev(m_viable[v]->hi); - if (var2bits(v).inf(is_false, bound)) - m_viable[v]->update_hi(m_viable[v]->prev(bound)); - } - - void viable::intersect_ule_bdd(pvar v, rational const& a, rational const& b, rational const& c, rational const& d, bool is_positive) { - unsigned sz = var2bits(v).num_bits(); - std::function le = [&]() { - bddv const& x = var2bits(v).var(); - return ((a * x) + b) <= ((c * x) + d); - }; - cached_constraint entry0(sz, a, b, c, d, m_bdd.mk_true()); - cached_constraint& entry = cache_constraint(v, entry0, le); - - // le(lo) is false: find min x >= lo, such that le(x) is false, le(x+1) is true - // le(hi) is false: find max x =< hi, such that le(x) is false, le(x-1) is true - bdd gt = is_positive ? !entry.repr : entry.repr; - narrow(v, gt); - } - - void viable::intersect_eq_bdd(pvar v, rational const& a, rational const& b, bool is_positive) { - unsigned sz = var2bits(v).num_bits(); - std::function eq = [&]() { - bddv const& x = var2bits(v).var(); - return ((a * x) + b) == rational(0); - }; - cached_constraint entry0(sz, a, b, m_bdd.mk_true()); - cached_constraint& entry = cache_constraint(v, entry0, eq); - - bdd ne = is_positive ? !entry.repr : entry.repr; - narrow(v, ne); - } -#endif - bool viable::has_viable(pvar v) { -#if NEW_VIABLE - return !m_viable[v]->is_empty(); -#else return !m_viable[v].is_false(); -#endif } bool viable::is_viable(pvar v, rational const& val) { -#if NEW_VIABLE - return m_viable[v]->contains(val); -#else return var2bits(v).contains(m_viable[v], val); -#endif } void viable::add_non_viable(pvar v, rational const& val) { -#if NEW_VIABLE - push_viable(v); - IF_VERBOSE(10, verbose_stream() << " v" << v << " != " << val << "\n"); - m_viable[v]->intersect_diff(val); - if (m_viable[v]->is_empty()) - s.set_conflict(v); -#else LOG("pvar " << v << " /= " << val); SASSERT(is_viable(v, val)); auto const& bits = var2bits(v); intersect_viable(v, bits.var() != val); -#endif } -#if !NEW_VIABLE void viable::intersect_viable(pvar v, bdd vals) { push_viable(v); m_viable[v] &= vals; if (m_viable[v].is_false()) s.set_conflict(v); } -#endif dd::find_t viable::find_viable(pvar v, rational & val) { -#if NEW_VIABLE - return m_viable[v]->find_hint(s.m_value[v], val); -#else return var2bits(v).find_hint(m_viable[v], s.m_value[v], val); -#endif } rational viable::min_viable(pvar v) { -#if !NEW_VIABLE return var2bits(v).min(m_viable[v]); -#else - return rational(0); -#endif } rational viable::max_viable(pvar v) { -#if NEW_VIABLE - return m_viable[v]->max(); -#else return var2bits(v).max(m_viable[v]); -#endif } dd::fdd const& viable::sz2bits(unsigned sz) { @@ -267,7 +126,6 @@ namespace polysat { return *bits; } -#if POLYSAT_LOGGING_ENABLED void viable::log() { // only for small problems for (pvar v = 0; v < std::min(10u, m_viable.size()); ++v) @@ -284,7 +142,6 @@ namespace polysat { LOG("Viable for v" << v << ": " << xs); } } -#endif dd::fdd const& viable::var2bits(pvar v) { return sz2bits(s.size(v)); } diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index a954c01d0..6946ce1ae 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -14,63 +14,15 @@ Author: Notes: NEW_VIABLE uses cheaper book-keeping, but is partial. - - -Alternative to using rational, instead use fixed-width numerals. - - -map from num_bits to template set - -class viable_trail_base { -public: - virtual pop(pvar v) = 0; - virtual push(pvar v) = 0; - static viable_trail_base* mk_trail(unsigned num_bits); -}; - -class viable_trail : public viable_trail_base { - vector> m_viable; - vector> m_trail; -public: - void pop(pvar v) override { - m_viable[v] = m_trail.back(); - m_trail.pop_back(); - } - void push(pvar v) override { - m_trail.push_back(m_viable[v]); - } -}; - -// from num-bits to viable_trail_base* -scoped_ptr_vector m_viable_trails; - -viable_set_base& to_viable(pvar v) { - return (*m_viable_trails[num_bits(v)])[v]; -} - -viable_set_base is required to expose functions: -lo, hi, -prev, next alternative as bit-vectors -update_lo (a) -update_hi (a) -intersect_le (a, b, c, d) -intersect_diff (a, b) -intersect_eq (a, b) -is_empty -contains + --*/ #pragma once -#define NEW_VIABLE 0 - #include - #include "math/dd/dd_bdd.h" #include "math/polysat/types.h" -#if NEW_VIABLE -#include "math/polysat/viable_set.h" -#endif + namespace polysat { @@ -82,43 +34,7 @@ namespace polysat { typedef dd::fdd fdd; solver& s; dd::bdd_manager m_bdd; - scoped_ptr_vector m_bits; -#if NEW_VIABLE - struct cached_constraint { - enum op_code { is_ule, is_eq }; - op_code m_op; - unsigned m_num_bits; - rational a, b, c, d; - bdd repr; - unsigned m_activity = 0; - cached_constraint(unsigned n, rational const& a, rational const& b, rational const& c, rational const& d, bdd& f) : - m_op(op_code::is_ule), m_num_bits(n), a(a), b(b), c(c), d(d), repr(f) {} - cached_constraint(unsigned n, rational const& a, rational const& b, bdd& f) : - m_op(op_code::is_eq), m_num_bits(n), a(a), b(b), repr(f) {} - - struct hash { - unsigned operator()(cached_constraint const* e) const { - return mk_mix(e->a.hash(), e->b.hash(), mk_mix(e->c.hash(), e->d.hash(), e->m_num_bits)) + e->m_op; - } - }; - struct eq { - bool operator()(cached_constraint const* x, cached_constraint const* y) const { - return x->m_op == y->m_op && x->a == y->a && x->b == y->b && x->c == y->c && x->d == y->d && x->m_num_bits == y->m_num_bits; - } - }; - }; - scoped_ptr_vector m_viable; - vector> m_viable_trail; - hashtable m_constraint_cache; - - void intersect_ule_bdd(pvar v, rational const& a, rational const& b, rational const& c, rational const& d, bool is_positive); - void intersect_eq_bdd(pvar v, rational const& a, rational const& b, bool is_positive); - cached_constraint& cache_constraint(pvar v, cached_constraint& entry0, std::function& mk_constraint); - void gc_cached_constraints(); - void narrow(pvar v, bdd const& is_false); -#else - - + scoped_ptr_vector m_bits; vector m_viable; // set of viable values. vector> m_viable_trail; @@ -127,7 +43,7 @@ namespace polysat { * Register all values that are not contained in vals as non-viable. */ void intersect_viable(pvar v, bdd vals); -#endif + dd::bdd_manager& get_bdd() { return m_bdd; } dd::fdd const& sz2bits(unsigned sz); dd::fdd const& var2bits(pvar v); @@ -139,11 +55,7 @@ namespace polysat { ~viable(); void push(unsigned num_bits) { -#if NEW_VIABLE - m_viable.push_back(alloc(viable_set, num_bits)); -#else m_viable.push_back(m_bdd.mk_true()); -#endif } void pop() { diff --git a/src/math/polysat/viable2.cpp b/src/math/polysat/viable2.cpp new file mode 100644 index 000000000..65a0e0798 --- /dev/null +++ b/src/math/polysat/viable2.cpp @@ -0,0 +1,74 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + maintain viable domains + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-6 + + +--*/ + + +#include "math/polysat/viable2.h" +#include "math/polysat/solver.h" + + +namespace polysat { + + viable2::viable2(solver& s) : s(s) {} + + viable2::~viable2() {} + + void viable2::push_viable(pvar v) { + m_trail.push_back(std::make_pair(v, m_viable[v])); + } + + void viable2::pop_viable() { + auto const& [v, s] = m_trail.back(); + m_viable[v] = s; + m_trail.pop_back(); + } + + void viable2::intersect(pvar v, signed_constraint const& c) { + auto& fi = s.m_forbidden_intervals; + vector side_cond; + eval_interval interval = eval_interval::full(); + if (!fi.get_interval(c, v, interval, side_cond)) + return; + auto& s = m_viable[v]; + for (unsigned i = 0; i < s.size(); ++i) { + + } + } + + bool viable2::has_viable(pvar v) { return true; } + + bool viable2::is_viable(pvar v, rational const& val) { return true; } + + void viable2::add_non_viable(pvar v, rational const& val) { } + + rational viable2::min_viable(pvar v) { return rational::zero(); } + + rational viable2::max_viable(pvar v) { return rational::zero(); } + + dd::find_t viable2::find_viable(pvar v, rational& val) { return dd::find_t::multiple; } + + void viable2::log(pvar v) { + auto const& s = m_viable[v]; + for (auto const& [i, c] : s) + LOG("v" << v << ": " << i); + } + + void viable2::log() { + for (pvar v = 0; v < std::min(10u, m_viable.size()); ++v) + log(v); + } + + +} + diff --git a/src/math/polysat/viable2.h b/src/math/polysat/viable2.h new file mode 100644 index 000000000..149ef8658 --- /dev/null +++ b/src/math/polysat/viable2.h @@ -0,0 +1,101 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + maintain viable domains + It uses the interval extraction functions from forbidden intervals. + An empty viable set corresponds directly to a conflict that does not rely on + the non-viable variable. + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-6 + +--*/ +#pragma once + + +#include + +#include "math/polysat/types.h" +#include "math/polysat/constraint.h" + + +namespace polysat { + + class solver; + + class viable2 { + solver& s; + + typedef std::tuple> entry; + typedef vector state; + + vector m_viable; // set of viable values. + vector> m_trail; + + + public: + viable2(solver& s); + + ~viable2(); + + void push(unsigned) { + m_viable.push_back({}); + } + + void pop() { + m_viable.pop_back(); + } + + void push_viable(pvar v); + + void pop_viable(); + + /** + * update state of viable for pvar v + * based on affine constraints + */ + void intersect(pvar v, signed_constraint const& c); + + /** + * Check whether variable v has any viable values left according to m_viable. + */ + bool has_viable(pvar v); + + /** + * check if value is viable according to m_viable. + */ + bool is_viable(pvar v, rational const& val); + + /** + * register that val is non-viable for var. + */ + void add_non_viable(pvar v, rational const& val); + + /* + * Extract min and max viable values for v + */ + rational min_viable(pvar v); + + rational max_viable(pvar v); + + /** + * Find a next viable value for variable. + */ + dd::find_t find_viable(pvar v, rational & val); + + /** Log all viable values for the given variable. + * (Inefficient, but useful for debugging small instances.) + */ + void log(pvar v); + + /** Like log(v) but for all variables */ + void log(); + + }; +} + +