diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index e5d35a4f9..a191c85b2 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -35,6 +35,12 @@ z3_add_component(sat_smt pb_internalize.cpp pb_pb.cpp pb_solver.cpp + polysat_assignment.cpp + polysat_constraints.cpp + polysat_core.cpp + polysat_internalize.cpp + polysat_model.cpp + polysat_solver.cpp q_clause.cpp q_ematch.cpp q_eval.cpp diff --git a/src/sat/smt/polysat_assignment.cpp b/src/sat/smt/polysat_assignment.cpp new file mode 100644 index 000000000..a985188fa --- /dev/null +++ b/src/sat/smt/polysat_assignment.cpp @@ -0,0 +1,119 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat substitution and assignment + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-06 + +--*/ + +#include "sat/smt/polysat_assignment.h" +#include "sat/smt/polysat_core.h" + +namespace polysat { + + substitution::substitution(pdd p) + : m_subst(std::move(p)) { } + + substitution::substitution(dd::pdd_manager& m) + : m_subst(m.one()) { } + + substitution substitution::add(pvar var, rational const& value) const { + return {m_subst.subst_add(var, value)}; + } + + pdd substitution::apply_to(pdd const& p) const { + return p.subst_val(m_subst); + } + + bool substitution::contains(pvar var) const { + rational out_value; + return value(var, out_value); + } + + bool substitution::value(pvar var, rational& out_value) const { + return m_subst.subst_get(var, out_value); + } + + assignment::assignment(core& s) + : m_core(s) { } + + + assignment assignment::clone() const { + assignment a(s()); + a.m_pairs = m_pairs; + a.m_subst.reserve(m_subst.size()); + for (unsigned i = m_subst.size(); i-- > 0; ) + if (m_subst[i]) + a.m_subst.set(i, alloc(substitution, *m_subst[i])); + a.m_subst_trail = m_subst_trail; + return a; + } + + bool assignment::contains(pvar var) const { + return subst(s().size(var)).contains(var); + } + + bool assignment::value(pvar var, rational& out_value) const { + return subst(s().size(var)).value(var, out_value); + } + + substitution& assignment::subst(unsigned sz) { + return const_cast(std::as_const(*this).subst(sz)); + } + + substitution const& assignment::subst(unsigned sz) const { + m_subst.reserve(sz + 1); + if (!m_subst[sz]) + m_subst.set(sz, alloc(substitution, s().sz2pdd(sz))); + return *m_subst[sz]; + } + + void assignment::push(pvar var, rational const& value) { + SASSERT(all_of(m_pairs, [var](assignment_item_t const& item) { return item.first != var; })); + m_pairs.push_back({var, value}); + unsigned const sz = s().size(var); + substitution& sub = subst(sz); + m_subst_trail.push_back(sub); + sub = sub.add(var, value); + SASSERT_EQ(sub, *m_subst[sz]); + } + + void assignment::pop() { + substitution& sub = m_subst_trail.back(); + unsigned sz = sub.bit_width(); + SASSERT_EQ(sz, s().size(m_pairs.back().first)); + *m_subst[sz] = sub; + m_subst_trail.pop_back(); + m_pairs.pop_back(); + } + + pdd assignment::apply_to(pdd const& p) const { + unsigned const sz = p.power_of_2(); + return subst(sz).apply_to(p); + } + + std::ostream& substitution::display(std::ostream& out) const { + char const* delim = ""; + pdd p = m_subst; + while (!p.is_val()) { + SASSERT(p.lo().is_val()); + out << delim << "v" << p.var() << " := " << p.lo(); + delim = " "; + p = p.hi(); + } + return out; + } + + std::ostream& assignment::display(std::ostream& out) const { + char const* delim = ""; + for (auto const& [var, value] : m_pairs) + out << delim << var << " == " << value, delim = " "; + return out; + } +} diff --git a/src/sat/smt/polysat_assignment.h b/src/sat/smt/polysat_assignment.h new file mode 100644 index 000000000..daff03dd5 --- /dev/null +++ b/src/sat/smt/polysat_assignment.h @@ -0,0 +1,120 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat substitution and assignment + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-06 + +--*/ +#pragma once +#include "util/scoped_ptr_vector.h" +#include "sat/smt/polysat_types.h" + +namespace polysat { + + class core; + + using assignment_item_t = std::pair; + + class substitution_iterator { + pdd m_current; + substitution_iterator(pdd current) : m_current(std::move(current)) {} + friend class substitution; + + public: + using value_type = assignment_item_t; + using difference_type = std::ptrdiff_t; + using pointer = value_type const*; + using reference = value_type const&; + using iterator_category = std::input_iterator_tag; + + substitution_iterator& operator++() { + SASSERT(!m_current.is_val()); + m_current = m_current.hi(); + return *this; + } + + value_type operator*() const { + SASSERT(!m_current.is_val()); + return { m_current.var(), m_current.lo().val() }; + } + + bool operator==(substitution_iterator const& other) const { return m_current == other.m_current; } + bool operator!=(substitution_iterator const& other) const { return !operator==(other); } + }; + + /** Substitution for a single bit width. */ + class substitution { + pdd m_subst; + + substitution(pdd p); + + public: + substitution(dd::pdd_manager& m); + [[nodiscard]] substitution add(pvar var, rational const& value) const; + [[nodiscard]] pdd apply_to(pdd const& p) const; + + [[nodiscard]] bool contains(pvar var) const; + [[nodiscard]] bool value(pvar var, rational& out_value) const; + + [[nodiscard]] bool empty() const { return m_subst.is_one(); } + + pdd const& to_pdd() const { return m_subst; } + unsigned bit_width() const { return to_pdd().power_of_2(); } + + bool operator==(substitution const& other) const { return &m_subst.manager() == &other.m_subst.manager() && m_subst == other.m_subst; } + bool operator!=(substitution const& other) const { return !operator==(other); } + + std::ostream& display(std::ostream& out) const; + + using const_iterator = substitution_iterator; + const_iterator begin() const { return {m_subst}; } + const_iterator end() const { return {m_subst.manager().one()}; } + }; + + /** Full variable assignment, may include variables of varying bit widths. */ + class assignment { + core& m_core; + vector m_pairs; + mutable scoped_ptr_vector m_subst; + vector m_subst_trail; + + substitution& subst(unsigned sz); + core& s() const { return m_core; } + public: + assignment(core& s); + // prevent implicit copy, use clone() if you do need a copy + assignment(assignment const&) = delete; + assignment& operator=(assignment const&) = delete; + assignment(assignment&&) = default; + assignment& operator=(assignment&&) = default; + assignment clone() const; + + void push(pvar var, rational const& value); + void pop(); + + pdd apply_to(pdd const& p) const; + + bool contains(pvar var) const; + bool value(pvar var, rational& out_value) const; + rational value(pvar var) const { rational val; VERIFY(value(var, val)); return val; } + bool empty() const { return pairs().empty(); } + substitution const& subst(unsigned sz) const; + vector const& pairs() const { return m_pairs; } + using const_iterator = decltype(m_pairs)::const_iterator; + const_iterator begin() const { return pairs().begin(); } + const_iterator end() const { return pairs().end(); } + + std::ostream& display(std::ostream& out) const; + }; + + inline std::ostream& operator<<(std::ostream& out, substitution const& sub) { return sub.display(out); } + + inline std::ostream& operator<<(std::ostream& out, assignment const& a) { return a.display(out); } +} + diff --git a/src/sat/smt/polysat_constraints.cpp b/src/sat/smt/polysat_constraints.cpp new file mode 100644 index 000000000..1c9de327c --- /dev/null +++ b/src/sat/smt/polysat_constraints.cpp @@ -0,0 +1,25 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat constraints + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-06 + +--*/ +#include "sat/smt/polysat_core.h" +#include "sat/smt/polysat_solver.h" +#include "sat/smt/polysat_constraints.h" + +namespace polysat { + + signed_constraint constraints::ule(pdd const& p, pdd const& q) { + auto* c = alloc(ule_constraint, p, q); + m_trail.push(new_obj_trail(c)); + return signed_constraint(ckind_t::ule_t, c); + } +} diff --git a/src/sat/smt/polysat_constraints.h b/src/sat/smt/polysat_constraints.h new file mode 100644 index 000000000..24c7f9a11 --- /dev/null +++ b/src/sat/smt/polysat_constraints.h @@ -0,0 +1,128 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat constraints + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-06 + +--*/ + + +#pragma once +#include "sat/smt/polysat_types.h" + +namespace polysat { + + class core; + + using pdd = dd::pdd; + using pvar = unsigned; + + enum ckind_t { ule_t, umul_ovfl_t, smul_fl_t, op_t }; + + class constraint { + unsigned_vector m_vars; + public: + virtual ~constraint() {} + unsigned_vector& vars() { return m_vars; } + unsigned_vector const& vars() const { return m_vars; } + unsigned var(unsigned idx) const { return m_vars[idx]; } + bool contains_var(pvar v) const { return m_vars.contains(v); } + }; + + class ule_constraint : public constraint { + pdd m_lhs, m_rhs; + public: + ule_constraint(pdd const& lhs, pdd const& rhs) : m_lhs(lhs), m_rhs(rhs) {} + }; + + class signed_constraint { + bool m_sign = false; + ckind_t m_op = ule_t; + constraint* m_constraint = nullptr; + public: + signed_constraint() {} + signed_constraint(ckind_t c, constraint* p) : m_op(c), m_constraint(p) {} + signed_constraint operator~() const { signed_constraint r(*this); r.m_sign = !r.m_sign; return r; } + bool sign() const { return m_sign; } + unsigned_vector& vars() { return m_constraint->vars(); } + unsigned_vector const& vars() const { return m_constraint->vars(); } + unsigned var(unsigned idx) const { return m_constraint->var(idx); } + bool contains_var(pvar v) const { return m_constraint->contains_var(v); } + bool is_ule() const { return m_op == ule_t; } + ule_constraint& to_ule() { return *reinterpret_cast(m_constraint); } + bool is_eq(pvar& v, rational& val) { throw default_exception("nyi"); } + }; + + using dependent_constraint = std::pair; + + class constraints { + trail_stack& m_trail; + public: + constraints(trail_stack& c) : m_trail(c) {} + + signed_constraint eq(pdd const& p) { return ule(p, p.manager().mk_val(0)); } + signed_constraint eq(pdd const& p, rational const& v) { return eq(p - p.manager().mk_val(v)); } + signed_constraint ule(pdd const& p, pdd const& q); + signed_constraint sle(pdd const& p, pdd const& q) { throw default_exception("nyi"); } + signed_constraint ult(pdd const& p, pdd const& q) { throw default_exception("nyi"); } + signed_constraint slt(pdd const& p, pdd const& q) { throw default_exception("nyi"); } + signed_constraint umul_ovfl(pdd const& p, pdd const& q) { throw default_exception("nyi"); } + signed_constraint smul_ovfl(pdd const& p, pdd const& q) { throw default_exception("nyi"); } + signed_constraint smul_udfl(pdd const& p, pdd const& q) { throw default_exception("nyi"); } + signed_constraint bit(pdd const& p, unsigned i) { throw default_exception("nyi"); } + + signed_constraint diseq(pdd const& p) { return ~eq(p); } + signed_constraint diseq(pdd const& p, pdd const& q) { return diseq(p - q); } + signed_constraint diseq(pdd const& p, rational const& q) { return diseq(p - q); } + signed_constraint diseq(pdd const& p, int q) { return diseq(p, rational(q)); } + signed_constraint diseq(pdd const& p, unsigned q) { return diseq(p, rational(q)); } + + signed_constraint ule(pdd const& p, rational const& q) { return ule(p, p.manager().mk_val(q)); } + signed_constraint ule(rational const& p, pdd const& q) { return ule(q.manager().mk_val(p), q); } + signed_constraint ule(pdd const& p, int q) { return ule(p, rational(q)); } + signed_constraint ule(pdd const& p, unsigned q) { return ule(p, rational(q)); } + signed_constraint ule(int p, pdd const& q) { return ule(rational(p), q); } + signed_constraint ule(unsigned p, pdd const& q) { return ule(rational(p), q); } + + signed_constraint uge(pdd const& p, pdd const& q) { return ule(q, p); } + signed_constraint uge(pdd const& p, rational const& q) { return ule(q, p); } + + signed_constraint ult(pdd const& p, rational const& q) { return ult(p, p.manager().mk_val(q)); } + signed_constraint ult(rational const& p, pdd const& q) { return ult(q.manager().mk_val(p), q); } + signed_constraint ult(int p, pdd const& q) { return ult(rational(p), q); } + signed_constraint ult(unsigned p, pdd const& q) { return ult(rational(p), q); } + signed_constraint ult(pdd const& p, int q) { return ult(p, rational(q)); } + signed_constraint ult(pdd const& p, unsigned q) { return ult(p, rational(q)); } + + signed_constraint slt(pdd const& p, rational const& q) { return slt(p, p.manager().mk_val(q)); } + signed_constraint slt(rational const& p, pdd const& q) { return slt(q.manager().mk_val(p), q); } + signed_constraint slt(pdd const& p, int q) { return slt(p, rational(q)); } + signed_constraint slt(pdd const& p, unsigned q) { return slt(p, rational(q)); } + signed_constraint slt(int p, pdd const& q) { return slt(rational(p), q); } + signed_constraint slt(unsigned p, pdd const& q) { return slt(rational(p), q); } + + + signed_constraint sgt(pdd const& p, pdd const& q) { return slt(q, p); } + signed_constraint sgt(pdd const& p, int q) { return slt(q, p); } + signed_constraint sgt(pdd const& p, unsigned q) { return slt(q, p); } + signed_constraint sgt(int p, pdd const& q) { return slt(q, p); } + signed_constraint sgt(unsigned p, pdd const& q) { return slt(q, p); } + + signed_constraint umul_ovfl(pdd const& p, rational const& q) { return umul_ovfl(p, p.manager().mk_val(q)); } + signed_constraint umul_ovfl(rational const& p, pdd const& q) { return umul_ovfl(q.manager().mk_val(p), q); } + signed_constraint umul_ovfl(pdd const& p, int q) { return umul_ovfl(p, rational(q)); } + signed_constraint umul_ovfl(pdd const& p, unsigned q) { return umul_ovfl(p, rational(q)); } + signed_constraint umul_ovfl(int p, pdd const& q) { return umul_ovfl(rational(p), q); } + signed_constraint umul_ovfl(unsigned p, pdd const& q) { return umul_ovfl(rational(p), q); } + + + //signed_constraint even(pdd const& p) { return parity_at_least(p, 1); } + //signed_constraint odd(pdd const& p) { return ~even(p); } + }; +} \ No newline at end of file diff --git a/src/sat/smt/polysat_core.cpp b/src/sat/smt/polysat_core.cpp new file mode 100644 index 000000000..27d6ee731 --- /dev/null +++ b/src/sat/smt/polysat_core.cpp @@ -0,0 +1,276 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + polysat_core.cpp + +Abstract: + + PolySAT core functionality + +Author: + + Nikolaj Bjorner (nbjorner) 2022-01-26 + Jakob Rath 2021-04-06 + +Notes: + +polysat::solver +- adds assignments +- calls propagation and check + +polysat::core +- propagates literals +- crates case splits by value assignment (equalities) +- detects conflicts based on Literal assignmets +- adds lemmas based on projections + +--*/ + +#include "params/bv_rewriter_params.hpp" +#include "sat/smt/polysat_solver.h" +#include "sat/smt/euf_solver.h" + +namespace polysat { + + class core::mk_assign_var : public trail { + pvar m_var; + core& c; + public: + mk_assign_var(pvar v, core& c) : m_var(v), c(c) {} + void undo() { + c.m_justification[m_var] = nullptr; + c.m_assignment.pop(); + } + }; + + class core::mk_dqueue_var : public trail { + pvar m_var; + core& c; + public: + mk_dqueue_var(pvar v, core& c) : m_var(v), c(c) {} + void undo() { + c.m_var_queue.unassign_var_eh(m_var); + } + }; + + class core::mk_add_var : public trail { + core& c; + public: + mk_add_var(core& c) : c(c) {} + void undo() override { + c.del_var(); + } + }; + + class core::mk_add_watch : public trail { + core& c; + unsigned m_idx; + public: + mk_add_watch(core& c, unsigned idx) : c(c), m_idx(idx) {} + void undo() override { + auto& sc = c.m_prop_queue[m_idx].first; + auto& vars = sc.vars(); + if (vars.size() > 0) + c.m_watch[vars[0]].pop_back(); + if (vars.size() > 1) + c.m_watch[vars[1]].pop_back(); + } + }; + + core::core(solver& s) : + s(s), + m_viable(*this), + m_constraints(s.get_trail_stack()), + m_assignment(*this), + m_dep(s.get_region()), + m_var_queue(m_activity) + {} + + pdd core::value(rational const& v, unsigned sz) { + return sz2pdd(sz).mk_val(v); + } + + dd::pdd_manager& core::sz2pdd(unsigned sz) const { + m_pdd.reserve(sz + 1); + if (!m_pdd[sz]) + m_pdd.set(sz, alloc(dd::pdd_manager, 1000, dd::pdd_manager::semantics::mod2N_e, sz)); + return *m_pdd[sz]; + } + + dd::pdd_manager& core::var2pdd(pvar v) const { + return sz2pdd(size(v)); + } + + pvar core::add_var(unsigned sz) { + unsigned v = m_vars.size(); + m_vars.push_back(sz2pdd(sz).mk_var(v)); + m_activity.push_back({ sz, 0 }); + m_justification.push_back(nullptr); + m_watch.push_back({}); + m_var_queue.mk_var_eh(v); + s.ctx.push(mk_add_var(*this)); + return v; + } + + void core::del_var() { + unsigned v = m_vars.size() - 1; + m_vars.pop_back(); + m_activity.pop_back(); + m_justification.pop_back(); + m_watch.pop_back(); + m_var_queue.del_var_eh(v); + } + + // case split on unassigned variables until all are assigned values. + // create equality literal for unassigned variable. + // return new_eq if there is a new literal. + + sat::check_result core::check() { + if (m_var_queue.empty()) + return sat::check_result::CR_DONE; + m_var = m_var_queue.next_var(); + s.ctx.push(mk_dqueue_var(m_var, *this)); + switch (m_viable.find_viable(m_var, m_value)) { + case find_t::empty: + m_unsat_core = m_viable.explain(); + propagate_unsat_core(); + return sat::check_result::CR_CONTINUE; + case find_t::singleton: + s.propagate(m_constraints.eq(var2pdd(m_var), m_value), m_viable.explain()); + return sat::check_result::CR_CONTINUE; + case find_t::multiple: + return sat::check_result::CR_CONTINUE; + case find_t::resource_out: + return sat::check_result::CR_GIVEUP; + } + UNREACHABLE(); + return sat::check_result::CR_GIVEUP; + } + + // First propagate Boolean assignment, then propagate value assignment + bool core::propagate() { + if (m_qhead == m_prop_queue.size() && m_vqhead == m_prop_queue.size()) + return false; + s.ctx.push(value_trail(m_qhead)); + for (; m_qhead < m_prop_queue.size() && !s.ctx.inconsistent(); ++m_qhead) + propagate_constraint(m_qhead, m_prop_queue[m_qhead]); + s.ctx.push(value_trail(m_vqhead)); + for (; m_vqhead < m_prop_queue.size() && !s.ctx.inconsistent(); ++m_vqhead) + propagate_value(m_vqhead, m_prop_queue[m_vqhead]); + return true; + } + + void core::propagate_constraint(unsigned idx, dependent_constraint& dc) { + auto [sc, dep] = dc; + if (sc.is_eq(m_var, m_value)) { + propagate_assignment(m_var, m_value, dep); + return; + } + add_watch(idx, sc); + } + + void core::add_watch(unsigned idx, signed_constraint& sc) { + auto& vars = sc.vars(); + unsigned i = 0, j = 0, sz = vars.size(); + for (; i < sz && j < 2; ++i) + if (!is_assigned(vars[i])) + std::swap(vars[i], vars[j++]); + if (vars.size() > 0) + add_watch(idx, vars[0]); + if (vars.size() > 1) + add_watch(idx, vars[1]); + s.ctx.push(mk_add_watch(*this, idx)); + } + + void core::add_watch(unsigned idx, unsigned var) { + m_watch[var].push_back(idx); + } + + void core::propagate_assignment(pvar v, rational const& value, stacked_dependency* dep) { + if (is_assigned(v)) + return; + if (m_var_queue.contains(v)) { + m_var_queue.del_var_eh(v); + s.ctx.push(mk_dqueue_var(v, *this)); + } + m_values[v] = value; + m_justification[v] = dep; + m_assignment.push(v , value); + s.ctx.push(mk_assign_var(v, *this)); + + // update the watch lists for pvars + // remove constraints from m_watch[v] that have more than 2 free variables. + // for entries where there is only one free variable left add to viable set + unsigned j = 0; + for (auto idx : m_watch[v]) { + auto [sc, dep] = m_prop_queue[idx]; + auto& vars = sc.vars(); + if (vars[0] != v) + std::swap(vars[0], vars[1]); + SASSERT(vars[0] == v); + bool swapped = false; + for (unsigned i = vars.size(); i-- > 2; ) { + if (!is_assigned(vars[i])) { + add_watch(idx, vars[i]); + std::swap(vars[i], vars[0]); + swapped = true; + break; + } + } + if (!swapped) { + m_watch[v][j++] = idx; + } + + // constraint is unitary, add to viable set + if (vars.size() >= 2 && is_assigned(vars[0]) && !is_assigned(vars[1])) { + // m_viable.add_unitary(vars[1], idx); + } + } + m_watch[v].shrink(j); + } + + void core::propagate_value(unsigned idx, dependent_constraint const& dc) { + auto [sc, dep] = dc; + // check if sc evaluates to false + switch (eval(sc)) { + case l_true: + return; + case l_false: + m_unsat_core = explain_eval(dc); + propagate_unsat_core(); + return; + default: + break; + } + // if sc is v == value, then check the watch list for v if they evaluate to false. + if (sc.is_eq(m_var, m_value)) { + for (auto idx : m_watch[m_var]) { + auto [sc, dep] = m_prop_queue[idx]; + if (eval(sc) == l_false) { + m_unsat_core = explain_eval({ sc, dep }); + propagate_unsat_core(); + return; + } + } + } + + throw default_exception("nyi"); + } + + bool core::propagate_unsat_core() { + // default is to use unsat core: + s.set_conflict(m_unsat_core); + // if core is based on viable, use s.set_lemma(); + throw default_exception("nyi"); + } + + void core::assign_eh(signed_constraint const& sc, dependency const& dep) { + m_prop_queue.push_back({ sc, m_dep.mk_leaf(dep) }); + s.ctx.push(push_back_vector(m_prop_queue)); + } + + + +} diff --git a/src/sat/smt/polysat_core.h b/src/sat/smt/polysat_core.h new file mode 100644 index 000000000..7fdf8c88c --- /dev/null +++ b/src/sat/smt/polysat_core.h @@ -0,0 +1,128 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + polysat_core.h + +Abstract: + + Core solver for polysat + +Author: + + Nikolaj Bjorner (nbjorner) 2020-08-30 + Jakob Rath 2021-04-06 + +--*/ +#pragma once + +#include "util/dependency.h" +#include "math/dd/dd_pdd.h" +#include "sat/smt/sat_th.h" +#include "sat/smt/polysat_types.h" +#include "sat/smt/polysat_constraints.h" +#include "sat/smt/polysat_viable.h" +#include "sat/smt/polysat_assignment.h" + +namespace polysat { + + class core; + class solver; + + class core { + class mk_add_var; + class mk_dqueue_var; + class mk_assign_var; + class mk_add_watch; + typedef svector> activity; + friend class viable; + friend class constraints; + friend class assignment; + + solver& s; + viable m_viable; + constraints m_constraints; + assignment m_assignment; + unsigned m_qhead = 0, m_vqhead = 0; + svector m_prop_queue; + stacked_dependency_manager m_dep; + mutable scoped_ptr_vector m_pdd; + dependency_vector m_unsat_core; + + + // attributes associated with variables + vector m_vars; // for each variable a pdd + vector m_values; // current value of assigned variable + ptr_vector m_justification; // justification for assignment + activity m_activity; // activity of variables + var_queue m_var_queue; // priority queue of variables to assign + vector m_watch; // watch lists for variables for constraints on m_prop_queue where they occur + + vector m_subst; // substitution, one for each size. + + // values to split on + rational m_value; + pvar m_var = 0; + + dd::pdd_manager& sz2pdd(unsigned sz) const; + dd::pdd_manager& var2pdd(pvar v) const; + unsigned size(pvar v) const { return var2pdd(v).power_of_2(); } + void del_var(); + + bool is_assigned(pvar v) { return nullptr != m_justification[v]; } + void propagate_constraint(unsigned idx, dependent_constraint& dc); + void propagate_value(unsigned idx, dependent_constraint const& dc); + void propagate_assignment(pvar v, rational const& value, stacked_dependency* dep); + bool propagate_unsat_core(); + + void add_watch(unsigned idx, signed_constraint& sc); + void add_watch(unsigned idx, unsigned var); + + lbool eval(signed_constraint sc) { throw default_exception("nyi"); } + dependency_vector explain_eval(dependent_constraint const& dc) { throw default_exception("nyi"); } + + public: + core(solver& s); + + sat::check_result check(); + + bool propagate(); + void assign_eh(signed_constraint const& sc, dependency const& dep); + + expr_ref constraint2expr(signed_constraint const& sc) const { throw default_exception("nyi"); } + + pdd value(rational const& v, unsigned sz); + + signed_constraint eq(pdd const& p) { return m_constraints.eq(p); } + signed_constraint eq(pdd const& p, pdd const& q) { return m_constraints.eq(p - q); } + signed_constraint ule(pdd const& p, pdd const& q) { return m_constraints.ule(p, q); } + signed_constraint sle(pdd const& p, pdd const& q) { return m_constraints.sle(p, q); } + signed_constraint umul_ovfl(pdd const& p, pdd const& q) { return m_constraints.umul_ovfl(p, q); } + signed_constraint smul_ovfl(pdd const& p, pdd const& q) { return m_constraints.smul_ovfl(p, q); } + signed_constraint smul_udfl(pdd const& p, pdd const& q) { return m_constraints.smul_udfl(p, q); } + signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); } + + + pdd lshr(pdd a, pdd b) { throw default_exception("nyi"); } + pdd ashr(pdd a, pdd b) { throw default_exception("nyi"); } + pdd shl(pdd a, pdd b) { throw default_exception("nyi"); } + pdd band(pdd a, pdd b) { throw default_exception("nyi"); } + pdd bxor(pdd a, pdd b) { throw default_exception("nyi"); } + pdd bor(pdd a, pdd b) { throw default_exception("nyi"); } + pdd bnand(pdd a, pdd b) { throw default_exception("nyi"); } + pdd bxnor(pdd a, pdd b) { throw default_exception("nyi"); } + pdd bnor(pdd a, pdd b) { throw default_exception("nyi"); } + pdd bnot(pdd a) { throw default_exception("nyi"); } + std::pair quot_rem(pdd const& n, pdd const& d) { throw default_exception("nyi"); } + pdd zero_ext(pdd a, unsigned sz) { throw default_exception("nyi"); } + pdd sign_ext(pdd a, unsigned sz) { throw default_exception("nyi"); } + pdd extract(pdd src, unsigned hi, unsigned lo) { throw default_exception("nyi"); } + pdd concat(unsigned n, pdd const* args) { throw default_exception("nyi"); } + pvar add_var(unsigned sz); + pdd var(pvar p) { return m_vars[p]; } + + std::ostream& display(std::ostream& out) const { throw default_exception("nyi"); } + }; + +} diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp new file mode 100644 index 000000000..80c2fb19b --- /dev/null +++ b/src/sat/smt/polysat_internalize.cpp @@ -0,0 +1,343 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + polysat_model.cpp + +Abstract: + + PolySAT model generation + +Author: + + Nikolaj Bjorner (nbjorner) 2022-01-26 + +--*/ + +#include "params/bv_rewriter_params.hpp" +#include "sat/smt/polysat_solver.h" +#include "sat/smt/euf_solver.h" + +namespace polysat { + + euf::theory_var solver::mk_var(euf::enode* n) { + return euf::th_euf_solver::mk_var(n); + } + + sat::literal solver::internalize(expr* e, bool sign, bool root) { + force_push(); + SASSERT(m.is_bool(e)); + if (!visit_rec(m, e, sign, root)) + return sat::null_literal; + sat::literal lit = expr2literal(e); + if (sign) + lit.neg(); + return lit; + } + + void solver::internalize(expr* e) { + force_push(); + visit_rec(m, e, false, false); + } + + bool solver::visit(expr* e) { + force_push(); + if (!is_app(e) || to_app(e)->get_family_id() != get_id()) { + ctx.internalize(e); + return true; + } + m_stack.push_back(sat::eframe(e)); + return false; + } + + bool solver::visited(expr* e) { + euf::enode* n = expr2enode(e); + return n && n->is_attached_to(get_id()); + } + + bool solver::post_visit(expr* e, bool sign, bool root) { + euf::enode* n = expr2enode(e); + app* a = to_app(e); + + if (visited(e)) + return true; + + SASSERT(!n || !n->is_attached_to(get_id())); + if (!n) + n = mk_enode(e, false); + + SASSERT(!n->is_attached_to(get_id())); + mk_var(n); + SASSERT(n->is_attached_to(get_id())); + internalize_polysat(a); + return true; + } + + void solver::internalize_polysat(app* a) { + +#define if_unary(F) if (a->get_num_args() == 1) { internalize_unary(a, [&](pdd const& p) { return F(p); }); break; } + + switch (a->get_decl_kind()) { + case OP_BMUL: internalize_binary(a, [&](pdd const& p, pdd const& q) { return p * q; }); break; + case OP_BADD: internalize_binary(a, [&](pdd const& p, pdd const& q) { return p + q; }); break; + case OP_BSUB: internalize_binary(a, [&](pdd const& p, pdd const& q) { return p - q; }); break; + case OP_BLSHR: internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.lshr(p, q); }); break; + case OP_BSHL: internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.shl(p, q); }); break; + case OP_BAND: internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.band(p, q); }); break; + case OP_BOR: internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.bor(p, q); }); break; + case OP_BXOR: internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.bxor(p, q); }); break; + case OP_BNAND: if_unary(m_core.bnot); internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.bnand(p, q); }); break; + case OP_BNOR: if_unary(m_core.bnot); internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.bnor(p, q); }); break; + case OP_BXNOR: if_unary(m_core.bnot); internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.bxnor(p, q); }); break; + case OP_BNOT: internalize_unary(a, [&](pdd const& p) { return m_core.bnot(p); }); break; + case OP_BNEG: internalize_unary(a, [&](pdd const& p) { return -p; }); break; + case OP_MKBV: internalize_mkbv(a); break; + case OP_BV_NUM: internalize_num(a); break; + case OP_ULEQ: internalize_le(a); break; + case OP_SLEQ: internalize_le(a); break; + case OP_UGEQ: internalize_le(a); break; + case OP_SGEQ: internalize_le(a); break; + case OP_ULT: internalize_le(a); break; + case OP_SLT: internalize_le(a); break; + case OP_UGT: internalize_le(a); break; + case OP_SGT: internalize_le(a); break; + + case OP_BUMUL_NO_OVFL: internalize_binaryc(a, [&](pdd const& p, pdd const& q) { return m_core.umul_ovfl(p, q); }); break; + case OP_BSMUL_NO_OVFL: internalize_binaryc(a, [&](pdd const& p, pdd const& q) { return m_core.smul_ovfl(p, q); }); break; + case OP_BSMUL_NO_UDFL: internalize_binaryc(a, [&](pdd const& p, pdd const& q) { return m_core.smul_udfl(p, q); }); break; + + case OP_BUMUL_OVFL: + case OP_BSMUL_OVFL: + case OP_BSDIV_OVFL: + case OP_BNEG_OVFL: + case OP_BUADD_OVFL: + case OP_BSADD_OVFL: + case OP_BUSUB_OVFL: + case OP_BSSUB_OVFL: + // handled by bv_rewriter for now + UNREACHABLE(); + break; + + case OP_BUDIV_I: internalize_div_rem_i(a, true); break; + case OP_BUREM_I: internalize_div_rem_i(a, false); break; + + case OP_BUDIV: internalize_div_rem(a, true); break; + case OP_BUREM: internalize_div_rem(a, false); break; + case OP_BSDIV0: UNREACHABLE(); break; + case OP_BUDIV0: UNREACHABLE(); break; + case OP_BSREM0: UNREACHABLE(); break; + case OP_BUREM0: UNREACHABLE(); break; + case OP_BSMOD0: UNREACHABLE(); break; + + case OP_EXTRACT: internalize_extract(a); break; + case OP_CONCAT: internalize_concat(a); break; + case OP_ZERO_EXT: internalize_par_unary(a, [&](pdd const& p, unsigned sz) { return m_core.zero_ext(p, sz); }); break; + case OP_SIGN_EXT: internalize_par_unary(a, [&](pdd const& p, unsigned sz) { return m_core.sign_ext(p, sz); }); break; + + // polysat::solver should also support at least: + case OP_BREDAND: // x == 2^K - 1 unary, return single bit, 1 if all input bits are set. + case OP_BREDOR: // x > 0 unary, return single bit, 1 if at least one input bit is set. + case OP_BCOMP: // x == y binary, return single bit, 1 if the arguments are equal. + case OP_BSDIV: + case OP_BSREM: + case OP_BSMOD: + case OP_BSDIV_I: + case OP_BSREM_I: + case OP_BSMOD_I: + case OP_BASHR: + IF_VERBOSE(0, verbose_stream() << mk_pp(a, m) << "\n"); + NOT_IMPLEMENTED_YET(); + return; + default: + IF_VERBOSE(0, verbose_stream() << mk_pp(a, m) << "\n"); + NOT_IMPLEMENTED_YET(); + return; + } +#undef if_unary + } + + class solver::mk_atom_trail : public trail { + solver& th; + sat::bool_var m_var; + public: + mk_atom_trail(sat::bool_var v, solver& th) : th(th), m_var(v) {} + void undo() override { + solver::atom* a = th.get_bv2a(m_var); + a->~atom(); + th.erase_bv2a(m_var); + } + }; + + solver::atom* solver::mk_atom(sat::bool_var bv) { + atom* a = get_bv2a(bv); + if (a) + return a; + a = new (get_region()) atom(bv); + insert_bv2a(bv, a); + ctx.push(mk_atom_trail(bv, *this)); + return a; + } + + void solver::internalize_binaryc(app* e, std::function const& fn) { + auto p = expr2pdd(e->get_arg(0)); + auto q = expr2pdd(e->get_arg(1)); + auto sc = ~fn(p, q); + sat::literal lit = expr2literal(e); + mk_atom(lit.var())->m_sc = sc; + } + + void solver::internalize_div_rem_i(app* e, bool is_div) { + auto p = expr2pdd(e->get_arg(0)); + auto q = expr2pdd(e->get_arg(1)); + auto [quot, rem] = m_core.quot_rem(p, q); + internalize_set(e, is_div ? quot : rem); + } + + void solver::internalize_div_rem(app* e, bool is_div) { + bv_rewriter_params p(s().params()); + if (p.hi_div0()) { + internalize_div_rem_i(e, is_div); + return; + } + expr* arg1 = e->get_arg(0); + expr* arg2 = e->get_arg(1); + unsigned sz = bv.get_bv_size(e); + expr_ref zero(bv.mk_numeral(0, sz), m); + sat::literal eqZ = eq_internalize(arg2, zero); + sat::literal eqU = eq_internalize(e, is_div ? bv.mk_bv_udiv0(arg1) : bv.mk_bv_urem0(arg1)); + sat::literal eqI = eq_internalize(e, is_div ? bv.mk_bv_udiv_i(arg1, arg2) : bv.mk_bv_urem_i(arg1, arg2)); + add_clause(~eqZ, eqU); + add_clause(eqZ, eqI); + ctx.add_aux(~eqZ, eqU); + ctx.add_aux(eqZ, eqI); + } + + void solver::internalize_num(app* a) { + rational val; + unsigned sz = 0; + VERIFY(bv.is_numeral(a, val, sz)); + auto p = m_core.value(val, sz); + internalize_set(a, p); + } + + // TODO - test that internalize works with recursive call on bit2bool + void solver::internalize_mkbv(app* a) { + unsigned i = 0; + for (expr* arg : *a) { + expr_ref b2b(m); + b2b = bv.mk_bit2bool(a, i); + sat::literal bit_i = ctx.internalize(b2b, false, false); + sat::literal lit = expr2literal(arg); + add_equiv(lit, bit_i); +#if 0 + ctx.add_aux_equiv(lit, bit_i); +#endif + ++i; + } + } + + void solver::internalize_extract(app* e) { + unsigned const hi = bv.get_extract_high(e); + unsigned const lo = bv.get_extract_low(e); + auto const src = expr2pdd(e->get_arg(0)); + auto const p = m_core.extract(src, hi, lo); + SASSERT_EQ(p.power_of_2(), hi - lo + 1); + internalize_set(e, p); + } + + void solver::internalize_concat(app* e) { + SASSERT(bv.is_concat(e)); + vector args; + for (expr* arg : *e) + args.push_back(expr2pdd(arg)); + auto const p = m_core.concat(args.size(), args.data()); + internalize_set(e, p); + } + + void solver::internalize_par_unary(app* e, std::function const& fn) { + pdd const p = expr2pdd(e->get_arg(0)); + unsigned const par = e->get_parameter(0).get_int(); + internalize_set(e, fn(p, par)); + } + + void solver::internalize_binary(app* e, std::function const& fn) { + SASSERT(e->get_num_args() >= 1); + auto p = expr2pdd(e->get_arg(0)); + for (unsigned i = 1; i < e->get_num_args(); ++i) + p = fn(p, expr2pdd(e->get_arg(i))); + internalize_set(e, p); + } + + void solver::internalize_unary(app* e, std::function const& fn) { + SASSERT(e->get_num_args() == 1); + auto p = expr2pdd(e->get_arg(0)); + internalize_set(e, fn(p)); + } + + template + void solver::internalize_le(app* e) { + auto p = expr2pdd(e->get_arg(0)); + auto q = expr2pdd(e->get_arg(1)); + if (Rev) + std::swap(p, q); + auto sc = Signed ? m_core.sle(p, q) : m_core.ule(p, q); + if (Negated) + sc = ~sc; + + sat::literal lit = expr2literal(e); + atom* a = mk_atom(lit.var()); + a->m_sc = sc; + } + + void solver::internalize_bit2bool(atom* a, expr* e, unsigned idx) { + pdd p = expr2pdd(e); + a->m_sc = m_core.bit(p, idx); + } + + dd::pdd solver::expr2pdd(expr* e) { + return var2pdd(get_th_var(e)); + } + + dd::pdd solver::var2pdd(euf::theory_var v) { + if (!m_var2pdd_valid.get(v, false)) { + unsigned bv_size = get_bv_size(v); + pvar pv = m_core.add_var(bv_size); + m_pddvar2var.setx(pv, v, UINT_MAX); + pdd p = m_core.var(pv); + internalize_set(v, p); + return p; + } + return m_var2pdd[v]; + } + + void solver::apply_sort_cnstr(euf::enode* n, sort* s) { + if (!bv.is_bv(n->get_expr())) + return; + theory_var v = n->get_th_var(get_id()); + if (v == euf::null_theory_var) + v = mk_var(n); + var2pdd(v); + } + + void solver::internalize_set(expr* e, pdd const& p) { + internalize_set(get_th_var(e), p); + } + + void solver::internalize_set(euf::theory_var v, pdd const& p) { + SASSERT_EQ(get_bv_size(v), p.power_of_2()); + m_var2pdd.reserve(get_num_vars(), p); + m_var2pdd_valid.reserve(get_num_vars(), false); + ctx.push(set_bitvector_trail(m_var2pdd_valid, v)); +#if 0 + m_var2pdd[v].reset(p.manager()); +#endif + m_var2pdd[v] = p; + } + + void solver::eq_internalized(euf::enode* n) { + SASSERT(m.is_eq(n->get_expr())); + } + + +} diff --git a/src/sat/smt/polysat_model.cpp b/src/sat/smt/polysat_model.cpp new file mode 100644 index 000000000..383a3f692 --- /dev/null +++ b/src/sat/smt/polysat_model.cpp @@ -0,0 +1,58 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + polysat_model.cpp + +Abstract: + + PolySAT model generation + +Author: + + Nikolaj Bjorner (nbjorner) 2022-01-26 + +--*/ + +#include "params/bv_rewriter_params.hpp" +#include "sat/smt/polysat_solver.h" +#include "sat/smt/euf_solver.h" + +namespace polysat { + + + void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) { +#if 0 + auto p = expr2pdd(n->get_expr()); + rational val; + VERIFY(m_polysat.try_eval(p, val)); + values[n->get_root_id()] = bv.mk_numeral(val, get_bv_size(n)); +#endif + } + + + bool solver::check_model(sat::model const& m) const { + return false; + } + + void solver::finalize_model(model& mdl) { + + } + + std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const { + return out; + } + + std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const { + return out; + } + + std::ostream& solver::display(std::ostream& out) const { + m_core.display(out); + for (unsigned v = 0; v < get_num_vars(); ++v) + if (m_var2pdd_valid.get(v, false)) + out << ctx.bpp(var2enode(v)) << " := " << m_var2pdd[v] << "\n"; + return out; + } +} diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp new file mode 100644 index 000000000..cee129327 --- /dev/null +++ b/src/sat/smt/polysat_solver.cpp @@ -0,0 +1,191 @@ +/*--- +Copyright (c 2022 Microsoft Corporation + +Module Name: + + polysat_internalize.cpp + +Abstract: + + PolySAT interface to bit-vector + +Author: + + Nikolaj Bjorner (nbjorner) 2022-01-26 + +Notes: +The solver adds literals to polysat::core, calls propagation and check +The result of polysat::core::check is one of: +- is_sat: the model is complete +- is_unsat: there is a Boolean conflict. The SAT solver backtracks and resolves the conflict. +- new_eq: the solver adds a new equality literal to the SAT solver. +- new_lemma: there is a conflict, but it is resolved by backjumping and adding a lemma to the SAT solver. +- giveup: Polysat was unable to determine satisfiability. + +--*/ + +#include "ast/euf/euf_bv_plugin.h" +#include "sat/smt/polysat_solver.h" +#include "sat/smt/euf_solver.h" + + +namespace polysat { + + solver::solver(euf::solver& ctx, theory_id id): + euf::th_euf_solver(ctx, symbol("bv"), id), + bv(ctx.get_manager()), + m_autil(ctx.get_manager()), + m_core(*this), + m_lemma(ctx.get_manager()) + { + ctx.get_egraph().add_plugin(alloc(euf::bv_plugin, ctx.get_egraph())); + } + + unsigned solver::get_bv_size(euf::enode* n) { + return bv.get_bv_size(n->get_expr()); + } + + unsigned solver::get_bv_size(theory_var v) { + return bv.get_bv_size(var2expr(v)); + } + + bool solver::unit_propagate() { + return m_core.propagate(); + } + + sat::check_result solver::check() { + return m_core.check(); + } + + void solver::asserted(literal l) { + atom* a = get_bv2a(l.var()); + TRACE("bv", tout << "asserted: " << l << "\n";); + if (!a) + return; + force_push(); + auto sc = a->m_sc; + if (l.sign()) + sc = ~sc; + m_core.assign_eh(sc, dependency(l, s().lvl(l))); + } + + void solver::set_conflict(dependency_vector const& core) { + auto [lits, eqs] = explain_deps(core); + auto ex = euf::th_explain::conflict(*this, lits, eqs, nullptr); + ctx.set_conflict(ex); + } + + std::pair solver::explain_deps(dependency_vector const& deps) { + sat::literal_vector core; + euf::enode_pair_vector eqs; + for (auto d : deps) { + if (d.is_literal()) { + core.push_back(d.literal()); + } + else { + auto const [v1, v2] = m_var_eqs[d.index()]; + euf::enode* const n1 = var2enode(v1); + euf::enode* const n2 = var2enode(v2); + VERIFY(n1->get_root() == n2->get_root()); + eqs.push_back(euf::enode_pair(n1, n2)); + } + } + DEBUG_CODE({ + for (auto lit : core) + VERIFY(s().value(lit) == l_true); + for (auto const& [n1, n2] : eqs) + VERIFY(n1->get_root() == n2->get_root()); + }); + IF_VERBOSE(10, + for (auto lit : core) + verbose_stream() << " " << lit << ": " << mk_ismt2_pp(literal2expr(lit), m) << "\n"; + for (auto const& [n1, n2] : eqs) + verbose_stream() << " " << ctx.bpp(n1) << " == " << ctx.bpp(n2) << "\n";); + + return { core, eqs }; + } + + void solver::set_lemma(vector const& lemma, unsigned level, dependency_vector const& core) { + auto [lits, eqs] = explain_deps(core); + auto ex = euf::th_explain::conflict(*this, lits, eqs, nullptr); + ctx.push(value_trail(m_has_lemma)); + m_has_lemma = true; + m_lemma_level = level; + m_lemma.reset(); + for (auto sc : lemma) + m_lemma.push_back(m_core.constraint2expr(sc)); + ctx.set_conflict(ex); + } + + // If an MCSat lemma is added, then backjump based on the lemma level and + // add the lemma to the solver with potentially fresh literals. + // return l_false to signal sat::solver that backjumping has been taken care of internally. + lbool solver::resolve_conflict() { + if (!m_has_lemma) + return l_undef; + + unsigned num_scopes = s().scope_lvl() - m_lemma_level; + + // s().pop_reinit(num_scopes); + + sat::literal_vector lits; + for (auto* e : m_lemma) + lits.push_back(ctx.mk_literal(e)); + s().add_clause(lits.size(), lits.data(), sat::status::th(true, get_id(), nullptr)); + return l_false; + } + + // Create an equality literal that represents the value assignment + // Prefer case split to true. + // The equality gets added in a callback using asserted(). + void solver::add_eq_literal(pvar pvar, rational const& val) { + auto v = m_pddvar2var[pvar]; + auto n = var2enode(v); + auto eq = eq_internalize(n->get_expr(), bv.mk_numeral(val, get_bv_size(v))); + s().set_phase(eq); + } + + void solver::new_eq_eh(euf::th_eq const& eq) { + auto v1 = eq.v1(), v2 = eq.v2(); + pdd p = var2pdd(v1); + pdd q = var2pdd(v2); + auto sc = m_core.eq(p, q); + m_var_eqs.setx(m_var_eqs_head, std::make_pair(v1, v2), std::make_pair(v1, v2)); + ctx.push(value_trail(m_var_eqs_head)); + m_core.assign_eh(sc, dependency(m_var_eqs_head, s().scope_lvl())); + m_var_eqs_head++; + } + + void solver::new_diseq_eh(euf::th_eq const& ne) { + euf::theory_var v1 = ne.v1(), v2 = ne.v2(); + pdd p = var2pdd(v1); + pdd q = var2pdd(v2); + auto sc = ~m_core.eq(p, q); + sat::literal neq = ~expr2literal(ne.eq()); + TRACE("bv", tout << neq << " := " << s().value(neq) << " @" << s().scope_lvl() << "\n"); + m_core.assign_eh(sc, dependency(neq, s().lvl(neq))); + } + + // Core uses the propagate callback to add unit propagations to the trail. + // The polysat::solver takes care of translating signed constraints into expressions, which translate into literals. + // Everything goes over expressions/literals. polysat::core is not responsible for replaying expressions. + void solver::propagate(signed_constraint sc, dependency_vector const& deps) { + sat::literal lit = ctx.mk_literal(m_core.constraint2expr(sc)); + auto [core, eqs] = explain_deps(deps); + auto ex = euf::th_explain::propagate(*this, core, eqs, lit, nullptr); + ctx.propagate(lit, ex); + } + + void solver::add_lemma(vector const& lemma) { + sat::literal_vector lits; + for (auto sc : lemma) + lits.push_back(ctx.mk_literal(m_core.constraint2expr(sc))); + s().add_clause(lits.size(), lits.data(), sat::status::th(true, get_id(), nullptr)); + } + + void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) { + auto& jst = euf::th_explain::from_index(idx); + ctx.get_th_antecedents(l, jst, r, probing); + } + +} diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h new file mode 100644 index 000000000..5d9cd19a3 --- /dev/null +++ b/src/sat/smt/polysat_solver.h @@ -0,0 +1,187 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + polysat_solver.h + +Abstract: + + Theory plugin for bit-vectors + +Author: + + Nikolaj Bjorner (nbjorner) 2020-08-30 + +--*/ +#pragma once + +#include "sat/smt/sat_th.h" +#include "math/dd/dd_pdd.h" +#include "sat/smt/polysat_core.h" + +namespace euf { + class solver; +} + +namespace polysat { + + + class solver : public euf::th_euf_solver { + typedef euf::theory_var theory_var; + typedef euf::theory_id theory_id; + typedef sat::literal literal; + typedef sat::bool_var bool_var; + typedef sat::literal_vector literal_vector; + using pdd = dd::pdd; + + struct stats { + void reset() { memset(this, 0, sizeof(stats)); } + stats() { reset(); } + }; + + struct atom { + bool_var m_bv; + signed_constraint m_sc; + atom(bool_var b) :m_bv(b) {} + ~atom() { } + }; + + class polysat_proof : public euf::th_proof_hint { + public: + ~polysat_proof() override {} + expr* get_hint(euf::solver& s) const override { return nullptr; } + }; + + friend class core; + + bv_util bv; + arith_util m_autil; + stats m_stats; + core m_core; + polysat_proof m_proof; + + vector m_var2pdd; // theory_var 2 pdd + bool_vector m_var2pdd_valid; // valid flag + unsigned_vector m_pddvar2var; // pvar -> theory_var + ptr_vector m_bool_var2atom; // bool_var -> atom + + svector> m_var_eqs; + unsigned m_var_eqs_head = 0; + + bool m_has_lemma = false; + unsigned m_lemma_level = 0; + expr_ref_vector m_lemma; + + // internalize + bool visit(expr* e) override; + bool visited(expr* e) override; + bool post_visit(expr* e, bool sign, bool root) override; + unsigned get_bv_size(euf::enode* n); + unsigned get_bv_size(theory_var v); + theory_var get_var(euf::enode* n); + void fixed_var_eh(theory_var v); + bool is_fixed(euf::theory_var v, expr_ref& val, sat::literal_vector& lits) override { return false; } + bool is_bv(theory_var v) const { return bv.is_bv(var2expr(v)); } + void register_true_false_bit(theory_var v, unsigned i); + void add_bit(theory_var v, sat::literal lit); + void eq_internalized(sat::bool_var b1, sat::bool_var b2, unsigned idx, theory_var v1, theory_var v2, sat::literal eq, euf::enode* n); + + void insert_bv2a(bool_var bv, atom* a) { m_bool_var2atom.setx(bv, a, nullptr); } + void erase_bv2a(bool_var bv) { m_bool_var2atom[bv] = nullptr; } + atom* get_bv2a(bool_var bv) const { return m_bool_var2atom.get(bv, nullptr); } + class mk_atom_trail; + atom* mk_atom(sat::bool_var bv); + void set_bit_eh(theory_var v, literal l, unsigned idx); + void init_bits(expr* e, expr_ref_vector const & bits); + void mk_bits(theory_var v); + void add_def(sat::literal def, sat::literal l); + void internalize_unary(app* e, std::function const& fn); + void internalize_binary(app* e, std::function const& fn); + void internalize_binaryc(app* e, std::function const& fn); + void internalize_par_unary(app* e, std::function const& fn); + void internalize_novfl(app* n, std::function& fn); + void internalize_interp(app* n, std::function& ibin, std::function& un); + void internalize_num(app * n); + void internalize_concat(app * n); + void internalize_bv2int(app* n); + void internalize_int2bv(app* n); + void internalize_mkbv(app* n); + void internalize_xor3(app* n); + void internalize_carry(app* n); + void internalize_sub(app* n); + void internalize_extract(app* n); + void internalize_repeat(app* n); + void internalize_bit2bool(app* n); + void internalize_udiv_i(app* n); + template + void internalize_le(app* n); + void internalize_div_rem_i(app* e, bool is_div); + void internalize_div_rem(app* e, bool is_div); + void internalize_polysat(app* a); + void assert_bv2int_axiom(app * n); + void assert_int2bv_axiom(app* n); + void internalize_bit2bool(atom* a, expr* e, unsigned idx); + + pdd expr2pdd(expr* e); + pdd var2pdd(euf::theory_var v); + void internalize_set(expr* e, pdd const& p); + void internalize_set(euf::theory_var v, pdd const& p); + + // callbacks from core + void add_eq_literal(pvar v, rational const& val); + void set_conflict(dependency_vector const& core); + void set_lemma(vector const& lemma, unsigned level, dependency_vector const& core); + void propagate(signed_constraint sc, dependency_vector const& deps); + void add_lemma(vector const& lemma); + + std::pair explain_deps(dependency_vector const& deps); + + public: + solver(euf::solver& ctx, theory_id id); + void set_lookahead(sat::lookahead* s) override { } + void init_search() override {} + double get_reward(literal l, sat::ext_constraint_idx idx, sat::literal_occs_fun& occs) const override { return 0; } + bool is_extended_binary(sat::ext_justification_idx idx, literal_vector& r) override { return false; } + bool is_external(bool_var v) override { return false; } + void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector & r, bool probing) override; + void asserted(literal l) override; + sat::check_result check() override; + void simplify() override {} + void clauses_modifed() override {} + lbool get_phase(bool_var v) override { return l_undef; } + std::ostream& display(std::ostream& out) const override; + std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override; + std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override; + void collect_statistics(statistics& st) const override {} + euf::th_solver* clone(euf::solver& ctx) override { throw default_exception("nyi"); } + extension* copy(sat::solver* s) override { throw default_exception("nyi"); } + void find_mutexes(literal_vector& lits, vector & mutexes) override {} + void gc() override {} + void pop_reinit() override {} + lbool resolve_conflict() override; + bool validate() override { return true; } + void init_use_list(sat::ext_use_list& ul) override {} + bool is_blocked(literal l, sat::ext_constraint_idx) override { return false; } + bool check_model(sat::model const& m) const override; + void finalize_model(model& mdl) override; + + void new_eq_eh(euf::th_eq const& eq) override; + void new_diseq_eh(euf::th_eq const& ne) override; + bool use_diseqs() const override { return true; } + bool unit_propagate() override; + + void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override; + + bool extract_pb(std::function& card, + std::function& pb) override { return false; } + + bool to_formulas(std::function& l2e, expr_ref_vector& fmls) override { return false; } + sat::literal internalize(expr* e, bool sign, bool root) override; + void internalize(expr* e) override; + void eq_internalized(euf::enode* n) override; + euf::theory_var mk_var(euf::enode* n) override; + void apply_sort_cnstr(euf::enode * n, sort * s) override; + }; + +} diff --git a/src/sat/smt/polysat_substitution.h b/src/sat/smt/polysat_substitution.h new file mode 100644 index 000000000..a30c6b710 --- /dev/null +++ b/src/sat/smt/polysat_substitution.h @@ -0,0 +1,212 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat substitution + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-06 + +--*/ +#pragma once +#include "sat/smt/polysat_types.h" + +namespace polysat { + + using assignment_item_t = std::pair; + + class substitution_iterator { + pdd m_current; + substitution_iterator(pdd current) : m_current(std::move(current)) {} + friend class substitution; + + public: + using value_type = assignment_item_t; + using difference_type = std::ptrdiff_t; + using pointer = value_type const*; + using reference = value_type const&; + using iterator_category = std::input_iterator_tag; + + substitution_iterator& operator++() { + SASSERT(!m_current.is_val()); + m_current = m_current.hi(); + return *this; + } + + value_type operator*() const { + SASSERT(!m_current.is_val()); + return { m_current.var(), m_current.lo().val() }; + } + + bool operator==(substitution_iterator const& other) const { return m_current == other.m_current; } + bool operator!=(substitution_iterator const& other) const { return !operator==(other); } + }; + + /** Substitution for a single bit width. */ + class substitution { + pdd m_subst; + + substitution(pdd p); + + public: + substitution(dd::pdd_manager& m); + [[nodiscard]] substitution add(pvar var, rational const& value) const; + [[nodiscard]] pdd apply_to(pdd const& p) const; + + [[nodiscard]] bool contains(pvar var) const; + [[nodiscard]] bool value(pvar var, rational& out_value) const; + + [[nodiscard]] bool empty() const { return m_subst.is_one(); } + + pdd const& to_pdd() const { return m_subst; } + unsigned bit_width() const { return to_pdd().power_of_2(); } + + bool operator==(substitution const& other) const { return &m_subst.manager() == &other.m_subst.manager() && m_subst == other.m_subst; } + bool operator!=(substitution const& other) const { return !operator==(other); } + + std::ostream& display(std::ostream& out) const; + + using const_iterator = substitution_iterator; + const_iterator begin() const { return {m_subst}; } + const_iterator end() const { return {m_subst.manager().one()}; } + }; + + /** Full variable assignment, may include variables of varying bit widths. */ + class assignment { + vector m_pairs; + mutable scoped_ptr_vector m_subst; + vector m_subst_trail; + + substitution& subst(unsigned sz); + solver& s() const { return *m_solver; } + public: + assignment(solver& s); + // prevent implicit copy, use clone() if you do need a copy + assignment(assignment const&) = delete; + assignment& operator=(assignment const&) = delete; + assignment(assignment&&) = default; + assignment& operator=(assignment&&) = default; + assignment clone() const; + + void push(pvar var, rational const& value); + void pop(); + + pdd apply_to(pdd const& p) const; + + bool contains(pvar var) const; + bool value(pvar var, rational& out_value) const; + rational value(pvar var) const { rational val; VERIFY(value(var, val)); return val; } + bool empty() const { return pairs().empty(); } + substitution const& subst(unsigned sz) const; + vector const& pairs() const { return m_pairs; } + using const_iterator = decltype(m_pairs)::const_iterator; + const_iterator begin() const { return pairs().begin(); } + const_iterator end() const { return pairs().end(); } + + std::ostream& display(std::ostream& out) const; + }; + + inline std::ostream& operator<<(std::ostream& out, substitution const& sub) { return sub.display(out); } + + inline std::ostream& operator<<(std::ostream& out, assignment const& a) { return a.display(out); } +} + +namespace polysat { + + enum class search_item_k + { + assignment, + boolean, + }; + + class search_item { + search_item_k m_kind; + union { + pvar m_var; + sat::literal m_lit; + }; + bool m_resolved = false; // when marked as resolved it is no longer valid to reduce the conflict state + + search_item(pvar var): m_kind(search_item_k::assignment), m_var(var) {} + search_item(sat::literal lit): m_kind(search_item_k::boolean), m_lit(lit) {} + public: + static search_item assignment(pvar var) { return search_item(var); } + static search_item boolean(sat::literal lit) { return search_item(lit); } + bool is_assignment() const { return m_kind == search_item_k::assignment; } + bool is_boolean() const { return m_kind == search_item_k::boolean; } + bool is_resolved() const { return m_resolved; } + search_item_k kind() const { return m_kind; } + pvar var() const { SASSERT(is_assignment()); return m_var; } + sat::literal lit() const { SASSERT(is_boolean()); return m_lit; } + void set_resolved() { m_resolved = true; } + }; + + class search_state { + solver& s; + + vector m_items; + assignment m_assignment; + + // store index into m_items + unsigned_vector m_pvar_to_idx; + unsigned_vector m_bool_to_idx; + + bool value(pvar v, rational& r) const; + + public: + search_state(solver& s): s(s), m_assignment(s) {} + unsigned size() const { return m_items.size(); } + search_item const& back() const { return m_items.back(); } + search_item const& operator[](unsigned i) const { return m_items[i]; } + + assignment const& get_assignment() const { return m_assignment; } + substitution const& subst(unsigned sz) const { return m_assignment.subst(sz); } + + // TODO: implement the following method if we actually need the assignments without resolved items already during conflict resolution + // (no separate trail needed, just a second m_subst and an index into the trail, I think) + // (update on set_resolved? might be one iteration too early, looking at the old solver::resolve_conflict loop) + substitution const& unresolved_assignment(unsigned sz) const; + + void push_assignment(pvar v, rational const& r); + void push_boolean(sat::literal lit); + void pop(); + + unsigned get_pvar_index(pvar v) const; + unsigned get_bool_index(sat::bool_var var) const; + unsigned get_bool_index(sat::literal lit) const { return get_bool_index(lit.var()); } + + void set_resolved(unsigned i) { m_items[i].set_resolved(); } + + using const_iterator = decltype(m_items)::const_iterator; + const_iterator begin() const { return m_items.begin(); } + const_iterator end() const { return m_items.end(); } + + std::ostream& display(std::ostream& out) const; + std::ostream& display(search_item const& item, std::ostream& out) const; + std::ostream& display_verbose(std::ostream& out) const; + std::ostream& display_verbose(search_item const& item, std::ostream& out) const; + }; + + struct search_state_pp { + search_state const& s; + bool verbose; + search_state_pp(search_state const& s, bool verbose = false) : s(s), verbose(verbose) {} + }; + + struct search_item_pp { + search_state const& s; + search_item const& i; + bool verbose; + search_item_pp(search_state const& s, search_item const& i, bool verbose = false) : s(s), i(i), verbose(verbose) {} + }; + + inline std::ostream& operator<<(std::ostream& out, search_state const& s) { return s.display(out); } + + inline std::ostream& operator<<(std::ostream& out, search_state_pp const& p) { return p.verbose ? p.s.display_verbose(out) : p.s.display(out); } + + inline std::ostream& operator<<(std::ostream& out, search_item_pp const& p) { return p.verbose ? p.s.display_verbose(p.i, out) : p.s.display(p.i, out); } + +} diff --git a/src/sat/smt/polysat_types.h b/src/sat/smt/polysat_types.h new file mode 100644 index 000000000..4296a8247 --- /dev/null +++ b/src/sat/smt/polysat_types.h @@ -0,0 +1,45 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-06 + +--*/ +#pragma once + +#include "math/dd/dd_pdd.h" +#include "util/sat_literal.h" +#include "util/dependency.h" + +namespace polysat { + + using pdd = dd::pdd; + using pvar = unsigned; + + + class dependency { + unsigned m_index; + unsigned m_level; + public: + dependency(sat::literal lit, unsigned level) : m_index(2 * lit.index()), m_level(level) {} + dependency(unsigned var_idx, unsigned level) : m_index(1 + 2 * var_idx), m_level(level) {} + bool is_literal() const { return m_index % 2 == 0; } + sat::literal literal() const { SASSERT(is_literal()); return sat::to_literal(m_index / 2); } + unsigned index() const { SASSERT(!is_literal()); return (m_index - 1) / 2; } + unsigned level() const { return m_level; } + }; + + using stacked_dependency = stacked_dependency_manager::dependency; + + inline std::ostream& operator<<(std::ostream& out, dependency d) { + if (d.is_literal()) + return out << d.literal() << "@" << d.level(); + else + return out << "v" << d.index() << "@" << d.level(); + } + + using dependency_vector = vector; + +} diff --git a/src/sat/smt/polysat_viable.h b/src/sat/smt/polysat_viable.h new file mode 100644 index 000000000..def069652 --- /dev/null +++ b/src/sat/smt/polysat_viable.h @@ -0,0 +1,55 @@ +/*++ +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-06 + +--*/ +#pragma once + +#include "util/rational.h" +#include "sat/smt/polysat_types.h" + +namespace polysat { + + enum class find_t { + empty, + singleton, + multiple, + resource_out, + }; + + class core; + + class viable { + core& c; + public: + viable(core& c) : c(c) {} + + /** + * Find a next viable value for variable. + */ + find_t find_viable(pvar v, rational& out_val) { throw default_exception("nyi"); } + + /* + * Explain why the current variable is not viable or signleton. + */ + dependency_vector explain() { throw default_exception("nyi"); } + + /* + * Register constraint at index 'idx' as unitary in v. + */ + void add_unitary(pvar v, unsigned idx) { throw default_exception("nyi"); } + + }; + +}