From 7bcb4936c7ecb176d08db4ed2b22d898dca2d3a0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Dec 2023 20:45:33 -0800 Subject: [PATCH] remove stale files Signed-off-by: Nikolaj Bjorner --- 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_substitution.h | 212 ---------------------------- src/sat/smt/polysat_viable.h | 130 ----------------- 6 files changed, 734 deletions(-) delete mode 100644 src/sat/smt/polysat_assignment.cpp delete mode 100644 src/sat/smt/polysat_assignment.h delete mode 100644 src/sat/smt/polysat_constraints.cpp delete mode 100644 src/sat/smt/polysat_constraints.h delete mode 100644 src/sat/smt/polysat_substitution.h delete mode 100644 src/sat/smt/polysat_viable.h diff --git a/src/sat/smt/polysat_assignment.cpp b/src/sat/smt/polysat_assignment.cpp deleted file mode 100644 index a985188fa..000000000 --- a/src/sat/smt/polysat_assignment.cpp +++ /dev/null @@ -1,119 +0,0 @@ -/*++ -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 deleted file mode 100644 index daff03dd5..000000000 --- a/src/sat/smt/polysat_assignment.h +++ /dev/null @@ -1,120 +0,0 @@ -/*++ -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 deleted file mode 100644 index 1c9de327c..000000000 --- a/src/sat/smt/polysat_constraints.cpp +++ /dev/null @@ -1,25 +0,0 @@ -/*++ -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 deleted file mode 100644 index 24c7f9a11..000000000 --- a/src/sat/smt/polysat_constraints.h +++ /dev/null @@ -1,128 +0,0 @@ -/*++ -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_substitution.h b/src/sat/smt/polysat_substitution.h deleted file mode 100644 index a30c6b710..000000000 --- a/src/sat/smt/polysat_substitution.h +++ /dev/null @@ -1,212 +0,0 @@ -/*++ -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_viable.h b/src/sat/smt/polysat_viable.h deleted file mode 100644 index e268d67a3..000000000 --- a/src/sat/smt/polysat_viable.h +++ /dev/null @@ -1,130 +0,0 @@ -/*++ -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 "util/dlist.h" -#include "util/map.h" -#include "util/small_object_allocator.h" - -#include "sat/smt/polysat_types.h" -#include "sat/smt/polysat_fi.h" - -namespace polysat { - - enum class find_t { - empty, - singleton, - multiple, - resource_out, - }; - - class core; - class constraints; - - class viable { - core& c; - constraints& cs; - forbidden_intervals m_forbidden_intervals; - - struct entry final : public dll_base, public fi_record { - /// whether the entry has been created by refinement (from constraints in 'fi_record::src') - bool refined = false; - /// whether the entry is part of the current set of intervals, or stashed away for backtracking - bool active = true; - bool valid_for_lemma = true; - pvar var = null_var; - - void reset() { - // dll_base::init(this); // we never did this in alloc_entry either - fi_record::reset(); - refined = false; - active = true; - valid_for_lemma = true; - var = null_var; - } - }; - - enum class entry_kind { unit_e, equal_e, diseq_e }; - - struct layer final { - entry* entries = nullptr; - unsigned bit_width = 0; - layer(unsigned bw) : bit_width(bw) {} - }; - - class layers final { - svector m_layers; - public: - svector const& get_layers() const { return m_layers; } - layer& ensure_layer(unsigned bit_width); - layer* get_layer(unsigned bit_width); - layer* get_layer(entry* e) { return get_layer(e->bit_width); } - layer const* get_layer(unsigned bit_width) const; - layer const* get_layer(entry* e) const { return get_layer(e->bit_width); } - entry* get_entries(unsigned bit_width) const { layer const* l = get_layer(bit_width); return l ? l->entries : nullptr; } - }; - - ptr_vector m_alloc; - vector m_units; // set of viable values based on unit multipliers, layered by bit-width in descending order - ptr_vector m_equal_lin; // entries that have non-unit multipliers, but are equal - ptr_vector m_diseq_lin; // entries that have distinct non-zero multipliers - - bool well_formed(entry* e); - bool well_formed(layers const& ls); - - entry* alloc_entry(pvar v); - - std::ostream& display_one(std::ostream& out, pvar v, entry const* e) const; - std::ostream& display_all(std::ostream& out, pvar v, entry const* e, char const* delimiter = "") const; - void log(); - void log(pvar v); - - struct pop_viable_trail; - void pop_viable(entry* e, pvar v, entry_kind k); - struct push_viable_trail; - void push_viable(entry* e, pvar v, entry_kind k); - - void insert(entry* e, pvar v, ptr_vector& entries, entry_kind k); - - bool intersect(pvar v, entry* e); - - void ensure_var(pvar v); - - public: - viable(core& c); - - ~viable(); - - /** - * Find a next viable value for variable. - */ - find_t find_viable(pvar v, rational& out_val); - - /* - * Explain why the current variable is not viable or signleton. - */ - dependency_vector explain(); - - /* - * Register constraint at index 'idx' as unitary in v. - */ - void add_unitary(pvar v, unsigned idx); - - }; - -}