From 190b74a41a97f8078f8c3b957b43d1f31559d74c Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 6 Nov 2023 10:13:19 +0100 Subject: [PATCH] Extract viable_fallback into separate file --- src/math/polysat/CMakeLists.txt | 1 + src/math/polysat/solver.h | 1 + src/math/polysat/viable.cpp | 114 +---------------------- src/math/polysat/viable.h | 33 ------- src/math/polysat/viable_fallback.cpp | 132 +++++++++++++++++++++++++++ src/math/polysat/viable_fallback.h | 52 +++++++++++ 6 files changed, 187 insertions(+), 146 deletions(-) create mode 100644 src/math/polysat/viable_fallback.cpp create mode 100644 src/math/polysat/viable_fallback.h diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt index 00eaa2745..2444f3d1b 100644 --- a/src/math/polysat/CMakeLists.txt +++ b/src/math/polysat/CMakeLists.txt @@ -30,6 +30,7 @@ z3_add_component(polysat umul_ovfl_constraint.cpp variable_elimination.cpp viable.cpp + viable_fallback.cpp COMPONENT_DEPENDENCIES bigfix dd diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index e651ffe4d..de97ebc8e 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -36,6 +36,7 @@ Author: #include "math/polysat/trail.h" #include "math/polysat/pvar_queue.h" #include "math/polysat/viable.h" +#include "math/polysat/viable_fallback.h" #include "math/polysat/log.h" #include #include diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 588209049..af93c0d26 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -8,7 +8,7 @@ Module Name: Author: Nikolaj Bjorner (nbjorner) 2021-03-19 - Jakob Rath 2021-04-6 + Jakob Rath 2021-04-06 Notes: @@ -18,11 +18,6 @@ In other cases, the phase of a variable assignment across branches might be used in a call to is_viable. With phase caching on, it may just check if the cached phase is viable without detecting that it is a propagation. -TODO: improve management of the fallback univariate solvers: - - use a solver pool and recycle the least recently used solver - - incrementally add/remove constraints - - set resource limit of univariate solver - TODO: plan to fix the FI "pumping": 1. simple looping detection and bitblasting fallback. -- done 2. intervals at multiple bit widths @@ -37,7 +32,6 @@ TODO: plan to fix the FI "pumping": #include "math/polysat/viable.h" #include "math/polysat/solver.h" #include "math/polysat/number.h" -#include "math/polysat/univariate/univariate_solver.h" namespace polysat { @@ -2312,110 +2306,4 @@ namespace { return true; } - //************************************************************************ - // viable_fallback - //************************************************************************ - - viable_fallback::viable_fallback(solver& s): - s(s) { - m_usolver_factory = mk_univariate_bitblast_factory(); - } - - void viable_fallback::push_var(unsigned bit_width) { - m_constraints.push_back({}); - } - - void viable_fallback::pop_var() { - m_constraints.pop_back(); - } - - void viable_fallback::push_constraint(pvar v, signed_constraint const& c) { - // v is the only unassigned variable in c. - SASSERT(c->vars().size() == 1 || !s.is_assigned(v)); - DEBUG_CODE(for (pvar w : c->vars()) { if (v != w) SASSERT(s.is_assigned(w)); }); - m_constraints[v].push_back(c); - m_constraints_trail.push_back(v); - s.m_trail.push_back(trail_instr_t::viable_constraint_i); - } - - void viable_fallback::pop_constraint() { - pvar v = m_constraints_trail.back(); - m_constraints_trail.pop_back(); - m_constraints[v].pop_back(); - } - - signed_constraint viable_fallback::find_violated_constraint(assignment const& a, pvar v) { - for (signed_constraint const c : m_constraints[v]) { - // for this check, all variables need to be assigned - DEBUG_CODE(for (pvar w : c->vars()) { SASSERT(a.contains(w)); }); - if (c.is_currently_false(a)) { - LOG(assignment_pp(s, v, a.value(v)) << " violates constraint " << lit_pp(s, c)); - return c; - } - SASSERT(c.is_currently_true(a)); - } - return {}; - } - - univariate_solver* viable_fallback::usolver(unsigned bit_width) { - univariate_solver* us; - - auto it = m_usolver.find_iterator(bit_width); - if (it != m_usolver.end()) { - us = it->m_value.get(); - us->pop(1); - } - else { - auto& mk_solver = *m_usolver_factory; - m_usolver.insert(bit_width, mk_solver(bit_width)); - us = m_usolver[bit_width].get(); - } - SASSERT_EQ(us->scope_level(), 0); - - // push once on the empty solver so we can reset it before the next use - us->push(); - - return us; - } - - find_t viable_fallback::find_viable(pvar v, rational& out_val) { - unsigned const bit_width = s.m_size[v]; - univariate_solver* us = usolver(bit_width); - - auto const& cs = m_constraints[v]; - for (unsigned i = cs.size(); i-- > 0; ) { - signed_constraint const c = cs[i]; - LOG("Univariate constraint: " << c); - c.add_to_univariate_solver(v, s, *us, c.blit().to_uint()); - } - - switch (us->check()) { - case l_true: - out_val = us->model(); - // we don't know whether the SMT instance has a unique solution - return find_t::multiple; - case l_false: - s.set_conflict_by_viable_fallback(v, *us); - return find_t::empty; - default: - return find_t::resource_out; - } - } - - std::ostream& operator<<(std::ostream& out, find_t x) { - switch (x) { - case find_t::empty: - return out << "empty"; - case find_t::singleton: - return out << "singleton"; - case find_t::multiple: - return out << "multiple"; - case find_t::resource_out: - return out << "resource_out"; - } - UNREACHABLE(); - return out; - } - } - diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index 4807f99fa..dfcc3c848 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -452,37 +452,4 @@ namespace polysat { return v.v.display(out, v.var); } - class viable_fallback { - friend class viable; - - solver& s; - - scoped_ptr m_usolver_factory; - u_map> m_usolver; // univariate solver for each bit width - vector m_constraints; - svector m_constraints_trail; - - univariate_solver* usolver(unsigned bit_width); - - public: - viable_fallback(solver& s); - - // declare and remove var - void push_var(unsigned bit_width); - void pop_var(); - - // add/remove constraints stored in the fallback solver - void push_constraint(pvar v, signed_constraint const& c); - void pop_constraint(); - - // Check whether all constraints for 'v' are satisfied; - // or find an arbitrary violated constraint. - bool check_constraints(assignment const& a, pvar v) { return !find_violated_constraint(a, v); } - signed_constraint find_violated_constraint(assignment const& a, pvar v); - - find_t find_viable(pvar v, rational& out_val); - }; - } - - diff --git a/src/math/polysat/viable_fallback.cpp b/src/math/polysat/viable_fallback.cpp new file mode 100644 index 000000000..bb576de4b --- /dev/null +++ b/src/math/polysat/viable_fallback.cpp @@ -0,0 +1,132 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + viable fallback to univariate solvers + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-06 + +Notes: + +TODO: improve management of the fallback univariate solvers: + - use a solver pool and recycle the least recently used solver + - incrementally add/remove constraints + - set resource limit of univariate solver + +--*/ + + +#include "util/debug.h" +#include "math/polysat/viable_fallback.h" +#include "math/polysat/solver.h" +#include "math/polysat/univariate/univariate_solver.h" + +namespace polysat { + + viable_fallback::viable_fallback(solver& s): + s(s) { + m_usolver_factory = mk_univariate_bitblast_factory(); + } + + void viable_fallback::push_var(unsigned bit_width) { + m_constraints.push_back({}); + } + + void viable_fallback::pop_var() { + m_constraints.pop_back(); + } + + void viable_fallback::push_constraint(pvar v, signed_constraint const& c) { + // v is the only unassigned variable in c. + SASSERT(c->vars().size() == 1 || !s.is_assigned(v)); + DEBUG_CODE(for (pvar w : c->vars()) { if (v != w) SASSERT(s.is_assigned(w)); }); + m_constraints[v].push_back(c); + m_constraints_trail.push_back(v); + s.m_trail.push_back(trail_instr_t::viable_constraint_i); + } + + void viable_fallback::pop_constraint() { + pvar v = m_constraints_trail.back(); + m_constraints_trail.pop_back(); + m_constraints[v].pop_back(); + } + + signed_constraint viable_fallback::find_violated_constraint(assignment const& a, pvar v) { + for (signed_constraint const c : m_constraints[v]) { + // for this check, all variables need to be assigned + DEBUG_CODE(for (pvar w : c->vars()) { SASSERT(a.contains(w)); }); + if (c.is_currently_false(a)) { + LOG(assignment_pp(s, v, a.value(v)) << " violates constraint " << lit_pp(s, c)); + return c; + } + SASSERT(c.is_currently_true(a)); + } + return {}; + } + + univariate_solver* viable_fallback::usolver(unsigned bit_width) { + univariate_solver* us; + + auto it = m_usolver.find_iterator(bit_width); + if (it != m_usolver.end()) { + us = it->m_value.get(); + us->pop(1); + } + else { + auto& mk_solver = *m_usolver_factory; + m_usolver.insert(bit_width, mk_solver(bit_width)); + us = m_usolver[bit_width].get(); + } + SASSERT_EQ(us->scope_level(), 0); + + // push once on the empty solver so we can reset it before the next use + us->push(); + + return us; + } + + find_t viable_fallback::find_viable(pvar v, rational& out_val) { + unsigned const bit_width = s.m_size[v]; + univariate_solver* us = usolver(bit_width); + + auto const& cs = m_constraints[v]; + for (unsigned i = cs.size(); i-- > 0; ) { + signed_constraint const c = cs[i]; + LOG("Univariate constraint: " << c); + c.add_to_univariate_solver(v, s, *us, c.blit().to_uint()); + } + + switch (us->check()) { + case l_true: + out_val = us->model(); + // we don't know whether the SMT instance has a unique solution + return find_t::multiple; + case l_false: + s.set_conflict_by_viable_fallback(v, *us); + return find_t::empty; + default: + return find_t::resource_out; + } + } + + std::ostream& operator<<(std::ostream& out, find_t x) { + switch (x) { + case find_t::empty: + return out << "empty"; + case find_t::singleton: + return out << "singleton"; + case find_t::multiple: + return out << "multiple"; + case find_t::resource_out: + return out << "resource_out"; + } + UNREACHABLE(); + return out; + } + +} + diff --git a/src/math/polysat/viable_fallback.h b/src/math/polysat/viable_fallback.h new file mode 100644 index 000000000..7b43f3e18 --- /dev/null +++ b/src/math/polysat/viable_fallback.h @@ -0,0 +1,52 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + viable_fallback to univariate solvers + (bit-blasting or int-blasting over a single variable) + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-06 + +--*/ +#pragma once + +#include "math/polysat/viable.h" + +namespace polysat { + + class viable_fallback { + friend class viable; + + solver& s; + + scoped_ptr m_usolver_factory; + u_map> m_usolver; // univariate solver for each bit width + vector m_constraints; + svector m_constraints_trail; + + univariate_solver* usolver(unsigned bit_width); + + public: + viable_fallback(solver& s); + + // declare and remove var + void push_var(unsigned bit_width); + void pop_var(); + + // add/remove constraints stored in the fallback solver + void push_constraint(pvar v, signed_constraint const& c); + void pop_constraint(); + + // Check whether all constraints for 'v' are satisfied; + // or find an arbitrary violated constraint. + bool check_constraints(assignment const& a, pvar v) { return !find_violated_constraint(a, v); } + signed_constraint find_violated_constraint(assignment const& a, pvar v); + + find_t find_viable(pvar v, rational& out_val); + }; + +}