From 1a39def7a1002d3bdd6656973dd5d6722e6de17f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Dec 2023 15:53:07 -0800 Subject: [PATCH] v2 of polysat --- src/sat/smt/polysat_assignment.cpp | 119 +++++++ src/sat/smt/polysat_assignment.h | 120 +++++++ src/sat/smt/polysat_constraints.cpp | 25 ++ src/sat/smt/polysat_constraints.h | 128 +++++++ src/sat/smt/polysat_core.cpp | 276 +++++++++++++++ src/sat/smt/polysat_core.h | 128 +++++++ src/sat/smt/polysat_internalize.cpp | 526 ---------------------------- src/sat/smt/polysat_substitution.h | 212 +++++++++++ src/sat/smt/polysat_types.h | 45 +++ src/sat/smt/polysat_viable.h | 55 +++ 10 files changed, 1108 insertions(+), 526 deletions(-) create mode 100644 src/sat/smt/polysat_assignment.cpp create mode 100644 src/sat/smt/polysat_assignment.h create mode 100644 src/sat/smt/polysat_constraints.cpp create mode 100644 src/sat/smt/polysat_constraints.h create mode 100644 src/sat/smt/polysat_core.cpp create mode 100644 src/sat/smt/polysat_core.h delete mode 100644 src/sat/smt/polysat_internalize.cpp create mode 100644 src/sat/smt/polysat_substitution.h create mode 100644 src/sat/smt/polysat_types.h create mode 100644 src/sat/smt/polysat_viable.h 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 deleted file mode 100644 index ef469fe6f..000000000 --- a/src/sat/smt/polysat_internalize.cpp +++ /dev/null @@ -1,526 +0,0 @@ -/*++ -Copyright (c) 2022 Microsoft Corporation - -Module Name: - - polysat_internalize.cpp - -Abstract: - - PolySAT internalize - -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) { - theory_var v = euf::th_euf_solver::mk_var(n); - ctx.attach_th_var(n, this, v); - return v; - } - - 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_lshr(a); break; - case OP_BSHL: internalize_shl(a); break; - case OP_BASHR: internalize_ashr(a); break; - case OP_BAND: internalize_band(a); break; - case OP_BOR: internalize_bor(a); break; - case OP_BXOR: internalize_bxor(a); break; - case OP_BNAND: if_unary(m_core.bnot); internalize_bnand(a); break; - case OP_BNOR: if_unary(m_core.bnot); internalize_bnor(a); break; - case OP_BXNOR: if_unary(m_core.bnot); internalize_bxnor(a); 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: - verbose_stream() << mk_pp(a, m) << "\n"; - // handled by bv_rewriter for now - UNREACHABLE(); - break; - - case OP_BUDIV_I: internalize_udiv_i(a); break; - case OP_BUREM_I: internalize_urem_i(a); 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_zero_extend(a); break; - case OP_SIGN_EXT: internalize_sign_extend(a); 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: - - 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 { - th.erase_bv2a(m_var); - } - }; - - void solver::mk_atom(sat::bool_var bv, signed_constraint& sc) { - if (get_bv2a(bv)) - return; - sat::literal lit(bv, false); - auto index = m_core.register_constraint(sc, dependency(lit, 0)); - auto a = new (get_region()) atom(bv, index); - insert_bv2a(bv, a); - ctx.push(mk_atom_trail(bv, *this)); - } - - 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); - if (lit.sign()) - sc = ~sc; - mk_atom(lit.var(), sc); - } - - void solver::internalize_udiv_i(app* e) { - expr* x, *y; - expr_ref rm(m); - if (bv.is_bv_udivi(e, x, y)) - rm = bv.mk_bv_urem_i(x, y); - else if (bv.is_bv_udiv(e, x, y)) - rm = bv.mk_bv_urem(x, y); - else - UNREACHABLE(); - internalize(rm); - } - - // From "Hacker's Delight", section 2-2. Addition Combined with Logical Operations; - // found via Int-Blasting paper; see https://doi.org/10.1007/978-3-030-94583-1_24 - // (p + q) - band(p, q); - void solver::internalize_bor(app* n) { - internalize_binary(n, [&](expr* const& x, expr* const& y) { return bv.mk_bv_sub(bv.mk_bv_add(x, y), bv.mk_bv_and(x, y)); }); - } - - // From "Hacker's Delight", section 2-2. Addition Combined with Logical Operations; - // found via Int-Blasting paper; see https://doi.org/10.1007/978-3-030-94583-1_24 - // (p + q) - 2*band(p, q); - void solver::internalize_bxor(app* n) { - internalize_binary(n, [&](expr* const& x, expr* const& y) { - return bv.mk_bv_sub(bv.mk_bv_add(x, y), bv.mk_bv_add(bv.mk_bv_and(x, y), bv.mk_bv_and(x, y))); - }); - } - - void solver::internalize_bnor(app* n) { - internalize_binary(n, [&](expr* const& x, expr* const& y) { return bv.mk_bv_not(bv.mk_bv_or(x, y)); }); - } - - void solver::internalize_bnand(app* n) { - internalize_binary(n, [&](expr* const& x, expr* const& y) { return bv.mk_bv_not(bv.mk_bv_and(x, y)); }); - } - - void solver::internalize_bxnor(app* n) { - internalize_binary(n, [&](expr* const& x, expr* const& y) { return bv.mk_bv_not(bv.mk_bv_xor(x, y)); }); - } - - void solver::internalize_band(app* n) { - if (n->get_num_args() == 2) { - expr* x, * y; - VERIFY(bv.is_bv_and(n, x, y)); - m_core.band(expr2pdd(x), expr2pdd(y), expr2pdd(n)); - } - else { - expr_ref z(n->get_arg(0), m); - for (unsigned i = 1; i < n->get_num_args(); ++i) { - z = bv.mk_bv_and(z, n->get_arg(i)); - ctx.internalize(z); - } - internalize_set(n, expr2pdd(z)); - } - } - - void solver::internalize_lshr(app* n) { - expr* x, * y; - VERIFY(bv.is_bv_lshr(n, x, y)); - m_core.lshr(expr2pdd(x), expr2pdd(y), expr2pdd(n)); - } - - void solver::internalize_ashr(app* n) { - expr* x, * y; - VERIFY(bv.is_bv_ashr(n, x, y)); - m_core.ashr(expr2pdd(x), expr2pdd(y), expr2pdd(n)); - } - - void solver::internalize_shl(app* n) { - expr* x, * y; - VERIFY(bv.is_bv_shl(n, x, y)); - m_core.shl(expr2pdd(x), expr2pdd(y), expr2pdd(n)); - } - - void solver::internalize_urem_i(app* rem) { - expr* x, *y; - euf::enode* n = expr2enode(rem); - SASSERT(n && n->is_attached_to(get_id())); - theory_var v = n->get_th_var(get_id()); - if (m_var2pdd_valid.get(v, false)) - return; - expr_ref quot(m); - if (bv.is_bv_uremi(rem, x, y)) - quot = bv.mk_bv_udiv_i(x, y); - else if (bv.is_bv_urem(rem, x, y)) - quot = bv.mk_bv_udiv(x, y); - else - UNREACHABLE(); - m_var2pdd_valid.setx(v, true, false); - ctx.internalize(quot); - m_var2pdd_valid.setx(v, false, false); - quot_rem(quot, rem, x, y); - } - - void solver::quot_rem(expr* quot, expr* rem, expr* x, expr* y) { - pdd a = expr2pdd(x); - pdd b = expr2pdd(y); - euf::enode* qn = expr2enode(quot); - euf::enode* rn = expr2enode(rem); - auto& m = a.manager(); - unsigned sz = m.power_of_2(); - if (b.is_zero()) { - // By SMT-LIB specification, b = 0 ==> q = -1, r = a. - internalize_set(quot, m.mk_val(m.max_value())); - internalize_set(rem, a); - return; - } - if (b.is_one()) { - internalize_set(quot, a); - internalize_set(rem, m.zero()); - return; - } - - if (a.is_val() && b.is_val()) { - rational const av = a.val(); - rational const bv = b.val(); - SASSERT(!bv.is_zero()); - rational rv; - rational qv = machine_div_rem(av, bv, rv); - pdd q = m.mk_val(qv); - pdd r = m.mk_val(rv); - SASSERT_EQ(a, b * q + r); - SASSERT(b.val() * q.val() + r.val() <= m.max_value()); - SASSERT(r.val() <= (b * q + r).val()); - SASSERT(r.val() < b.val()); - internalize_set(quot, q); - internalize_set(rem, r); - return; - } - - pdd r = var2pdd(rn->get_th_var(get_id())); - pdd q = var2pdd(qn->get_th_var(get_id())); - - // Axioms for quotient/remainder - // - // a = b*q + r - // multiplication does not overflow in b*q - // addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r - // b ≠ 0 ==> r < b - // b = 0 ==> q = -1 - // TODO: when a,b become evaluable, can we actually propagate q,r? doesn't seem like it. - // Maybe we need something like an op_constraint for better propagation. - add_polysat_clause("[axiom] quot_rem 1", { m_core.eq(b * q + r - a) }, false); - add_polysat_clause("[axiom] quot_rem 2", { ~m_core.umul_ovfl(b, q) }, false); - // r <= b*q+r - // { apply equivalence: p <= q <=> q-p <= -p-1 } - // b*q <= -r-1 - add_polysat_clause("[axiom] quot_rem 3", { m_core.ule(b * q, -r - 1) }, false); - - auto c_eq = m_core.eq(b); - if (!c_eq.is_always_true()) - add_polysat_clause("[axiom] quot_rem 4", { c_eq, ~m_core.ule(b, r) }, false); - if (!c_eq.is_always_false()) - add_polysat_clause("[axiom] quot_rem 5", { ~c_eq, m_core.eq(q + 1) }, false); - } - - void solver::internalize_sign_extend(app* e) { - expr* arg = e->get_arg(0); - unsigned sz = bv.get_bv_size(e); - unsigned arg_sz = bv.get_bv_size(arg); - unsigned sz2 = sz - arg_sz; - var2pdd(expr2enode(e)->get_th_var(get_id())); - if (arg_sz == sz) - add_clause(eq_internalize(e, arg), nullptr); - else { - sat::literal lt0 = ctx.mk_literal(bv.mk_slt(arg, bv.mk_numeral(0, arg_sz))); - // arg < 0 ==> e = concat(arg, 1...1) - // arg >= 0 ==> e = concat(arg, 0...0) - add_clause(lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(rational::power_of_two(sz2) - 1, sz2))), nullptr); - add_clause(~lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz2))), nullptr); - } - } - - void solver::internalize_zero_extend(app* e) { - expr* arg = e->get_arg(0); - unsigned sz = bv.get_bv_size(e); - unsigned arg_sz = bv.get_bv_size(arg); - unsigned sz2 = sz - arg_sz; - var2pdd(expr2enode(e)->get_th_var(get_id())); - if (arg_sz == sz) - add_clause(eq_internalize(e, arg), nullptr); - else - // e = concat(arg, 0...0) - add_clause(eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz2))), nullptr); - } - - void solver::internalize_div_rem(app* e, bool is_div) { - bv_rewriter_params p(s().params()); - if (p.hi_div0()) { - if (is_div) - internalize_udiv_i(e); - else - internalize_urem_i(e); - 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) { - var2pdd(expr2enode(e)->get_th_var(get_id())); - } - - void solver::internalize_concat(app* e) { - SASSERT(bv.is_concat(e)); - var2pdd(expr2enode(e)->get_th_var(get_id())); - } - - 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_binary(app* e, std::function const& fn) { - SASSERT(e->get_num_args() >= 1); - expr* r = e->get_arg(0); - for (unsigned i = 1; i < e->get_num_args(); ++i) - r = fn(r, e->get_arg(i)); - ctx.internalize(r); - internalize_set(e, var2pdd(expr2enode(r)->get_th_var(get_id()))); - } - - 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) { - SASSERT(e->get_num_args() == 2); - 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); - if (lit.sign()) - sc = ~sc; - mk_atom(lit.var(), sc); - } - - 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_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"); } + + }; + +}