From 7662427d92fc04602947da838b5f36b41d65e2f6 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 7 Nov 2022 13:33:48 +0100 Subject: [PATCH] Split constraint_manager into separate file --- src/math/polysat/CMakeLists.txt | 1 + src/math/polysat/clause_builder.h | 1 + src/math/polysat/conflict.h | 2 +- src/math/polysat/constraint.cpp | 254 +-------------------- src/math/polysat/constraint.h | 99 +------- src/math/polysat/constraint_manager.cpp | 288 ++++++++++++++++++++++++ src/math/polysat/constraint_manager.h | 122 ++++++++++ src/math/polysat/solver.h | 1 + 8 files changed, 419 insertions(+), 349 deletions(-) create mode 100644 src/math/polysat/constraint_manager.cpp create mode 100644 src/math/polysat/constraint_manager.h diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt index e89a362ec..26c3c63de 100644 --- a/src/math/polysat/CMakeLists.txt +++ b/src/math/polysat/CMakeLists.txt @@ -5,6 +5,7 @@ z3_add_component(polysat clause_builder.cpp conflict.cpp constraint.cpp + constraint_manager.cpp eq_explain.cpp explain.cpp forbidden_intervals.cpp diff --git a/src/math/polysat/clause_builder.h b/src/math/polysat/clause_builder.h index 00c2a7dc2..ac8bc7bfb 100644 --- a/src/math/polysat/clause_builder.h +++ b/src/math/polysat/clause_builder.h @@ -16,6 +16,7 @@ Notes: --*/ #pragma once +#include "math/polysat/clause.h" #include "math/polysat/constraint.h" #include "math/polysat/types.h" diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h index d6a8df195..59816dffe 100644 --- a/src/math/polysat/conflict.h +++ b/src/math/polysat/conflict.h @@ -69,7 +69,7 @@ Lemma: y < z or xz <= xy or O(x,y) --*/ #pragma once #include "math/polysat/types.h" -#include "math/polysat/constraint.h" +#include "math/polysat/constraint_manager.h" #include "math/polysat/inference_logger.h" #include diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index 857ddff04..ffca72b5a 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -8,7 +8,7 @@ Module Name: Author: Nikolaj Bjorner (nbjorner) 2021-03-19 - Jakob Rath 2021-04-6 + Jakob Rath 2021-04-06 --*/ @@ -24,200 +24,6 @@ Author: namespace polysat { - void constraint_manager::assign_bv2c(sat::bool_var bv, constraint* c) { - SASSERT_EQ(get_bv2c(bv), nullptr); - SASSERT(!c->has_bvar()); - c->m_bvar = bv; - m_bv2constraint.setx(bv, c, nullptr); - } - - void constraint_manager::erase_bv2c(constraint* c) { - SASSERT(c->has_bvar()); - SASSERT_EQ(get_bv2c(c->bvar()), c); - m_bv2constraint[c->bvar()] = nullptr; - c->m_bvar = sat::null_bool_var; - } - - constraint* constraint_manager::get_bv2c(sat::bool_var bv) const { - return m_bv2constraint.get(bv, nullptr); - } - - void constraint_manager::ensure_bvar(constraint* c) { - if (!c->has_bvar()) - assign_bv2c(m_bvars.new_var(), c); - } - - void constraint_manager::erase_bvar(constraint* c) { - if (c->has_bvar()) - erase_bv2c(c); - } - - /** Add constraint to per-level storage */ - void constraint_manager::store(constraint* c) { - LOG_V("Store constraint: " << show_deref(c)); - m_constraints.push_back(c); - } - - - void constraint_manager::register_clause(clause* cl, solver& s) { - while (m_clauses.size() <= s.base_level()) - m_clauses.push_back({}); - m_clauses[s.base_level()].push_back(cl); - } - - void constraint_manager::store(clause* cl, solver& s, bool value_propagate) { - register_clause(cl, s); - watch(*cl, s, value_propagate); - } - - // Release constraints at the given level and above. - void constraint_manager::release_level(unsigned lvl) { - for (unsigned l = m_clauses.size(); l-- > lvl; ) { - for (auto& cl : m_clauses[l]) { - unwatch(*cl); - SASSERT_EQ(cl->m_ref_count, 1); // otherwise there is a leftover reference somewhere - } - m_clauses[l].reset(); - } - } - - // find literals that are not propagated to false - // if clause is unsat then assign arbitrary - // solver handles unsat clauses by creating a conflict. - // solver also can propagate, but need to check that it does indeed. - void constraint_manager::watch(clause& cl, solver& s, bool value_propagate) { - if (cl.empty()) - return; - - bool first = true; - for (unsigned i = 0; i < cl.size(); ++i) { - if (m_bvars.is_false(cl[i])) - continue; - signed_constraint sc = s.lit2cnstr(cl[i]); - if (value_propagate && sc.is_currently_false(s)) { - if (m_bvars.is_true(cl[i])) { - s.set_conflict(sc); - return; - } - s.assign_eval(~cl[i]); - continue; - } - - m_bvars.watch(cl[i]).push_back(&cl); - std::swap(cl[!first], cl[i]); - if (!first) - return; - first = false; - } - - if (first) - m_bvars.watch(cl[0]).push_back(&cl); - if (cl.size() > 1) - m_bvars.watch(cl[1]).push_back(&cl); - if (m_bvars.is_true(cl[0])) - return; - if (first) - s.set_conflict(cl); - else - s.assign_propagate(cl[0], cl); - } - - void constraint_manager::unwatch(clause& cl) { - if (cl.size() <= 1) - return; - m_bvars.watch(~cl[0]).erase(&cl); - m_bvars.watch(~cl[1]).erase(&cl); - } - - constraint_manager::~constraint_manager() { - // Release explicitly to check for leftover references in debug mode, - // and to make sure all constraints are destructed before the bvar->constraint mapping. - release_level(0); - } - - constraint* constraint_manager::lookup(sat::bool_var var) const { - return get_bv2c(var); - } - - signed_constraint constraint_manager::lookup(sat::literal lit) const { - return {lookup(lit.var()), lit}; - } - - /** Look up constraint among stored constraints. */ - constraint* constraint_manager::dedup(constraint* c1) { - constraint* c2 = nullptr; - if (m_constraint_table.find(c1, c2)) { - dealloc(c1); - return c2; - } - else { - SASSERT(!c1->has_bvar()); - ensure_bvar(c1); - m_constraint_table.insert(c1); - store(c1); - return c1; - } - } - - void constraint_manager::gc(solver& s) { - LOG_H1("gc"); - gc_clauses(s); - gc_constraints(s); - } - - void constraint_manager::gc_clauses(solver& s) { - LOG_H3("gc_clauses"); - // place to gc redundant clauses - } - - void constraint_manager::gc_constraints(solver& s) { - LOG_H3("gc_constraints"); - uint_set used_vars; - for (auto const& cls : m_clauses) - for (auto const& cl : cls) - for (auto lit : *cl) - used_vars.insert(lit.var()); - // anything on the search stack is justified by a clause? - for (auto const& a : s.m_search) - if (a.is_boolean()) - used_vars.insert(a.lit().var()); - for (unsigned i = 0; i < m_constraints.size(); ++i) { - constraint* c = m_constraints[i]; - if (c->has_bvar() && used_vars.contains(c->bvar())) - continue; - if (c->is_external()) - continue; - LOG("Erasing: " << show_deref(c)); - erase_bvar(c); - m_constraints.swap(i, m_constraints.size() - 1); - m_constraints.pop_back(); - --i; - } - - } - - bool constraint_manager::should_gc() { - return false; - // TODO control gc decay rate - return m_constraints.size() > m_num_external + 100; - } - - signed_constraint constraint_manager::ule(pdd const& a, pdd const& b) { - bool is_positive = true; - pdd lhs = a; - pdd rhs = b; - ule_constraint::simplify(is_positive, lhs, rhs); - return { dedup(alloc(ule_constraint, *this, lhs, rhs)), is_positive }; - } - - signed_constraint constraint_manager::eq(pdd const& p) { - return ule(p, p.manager().zero()); - } - - signed_constraint constraint_manager::ult(pdd const& a, pdd const& b) { - return ~ule(b, a); - } - bool signed_constraint::is_eq() const { return is_positive() && m_constraint->is_eq(); } @@ -227,63 +33,6 @@ namespace polysat { return m_constraint->to_ule().lhs(); } - /** - * encode that the i'th bit of p is 1. - * It holds if p << (K - i - 1) >= 2^{K-1}, where K is the bit-width. - */ - signed_constraint constraint_manager::bit(pdd const& p, unsigned i) { - unsigned K = p.manager().power_of_2(); - pdd q = p * rational::power_of_two(K - i - 1); - rational msb = rational::power_of_two(K - 1); - return ule(p.manager().mk_val(msb), q); - } - - signed_constraint constraint_manager::umul_ovfl(pdd const& a, pdd const& b) { - return { dedup(alloc(umul_ovfl_constraint, *this, a, b)), true }; - } - - signed_constraint constraint_manager::smul_ovfl(pdd const& a, pdd const& b) { - return { dedup(alloc(smul_fl_constraint, *this, a, b, true)), true }; - } - - signed_constraint constraint_manager::smul_udfl(pdd const& a, pdd const& b) { - return { dedup(alloc(smul_fl_constraint, *this, a, b, false)), true }; - } - - signed_constraint constraint_manager::lshr(pdd const& p, pdd const& q, pdd const& r) { - return { dedup(alloc(op_constraint, *this, op_constraint::code::lshr_op, p, q, r)), true }; - } - - signed_constraint constraint_manager::band(pdd const& p, pdd const& q, pdd const& r) { - return { dedup(alloc(op_constraint, *this, op_constraint::code::and_op, p, q, r)), true }; - } - - // To do signed comparison of bitvectors, flip the msb and do unsigned comparison: - // - // x <=s y <=> x + 2^(w-1) <=u y + 2^(w-1) - // - // Example for bit width 3: - // 111 -1 - // 110 -2 - // 101 -3 - // 100 -4 - // 011 3 - // 010 2 - // 001 1 - // 000 0 - // - // Argument: flipping the msb swaps the negative and non-negative blocks - // - signed_constraint constraint_manager::sle(pdd const& a, pdd const& b) { - auto shift = rational::power_of_two(a.power_of_2() - 1); - return ule(a + shift, b + shift); - } - - signed_constraint constraint_manager::slt(pdd const& a, pdd const& b) { - auto shift = rational::power_of_two(a.power_of_2() - 1); - return ult(a + shift, b + shift); - } - signed_constraint inequality::as_signed_constraint() const { return signed_constraint(const_cast(src), !is_strict); } @@ -348,4 +97,5 @@ namespace polysat { else return out << ""; } + } diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index 3c8df311b..9126b9c77 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -8,12 +8,11 @@ Module Name: Author: Nikolaj Bjorner (nbjorner) 2021-03-19 - Jakob Rath 2021-04-6 + Jakob Rath 2021-04-06 --*/ #pragma once #include "math/polysat/boolean.h" -#include "math/polysat/clause.h" #include "math/polysat/types.h" #include "math/polysat/interval.h" #include "math/polysat/search_state.h" @@ -24,6 +23,7 @@ namespace polysat { enum ckind_t { ule_t, umul_ovfl_t, smul_fl_t, op_t }; + class constraint_manager; class constraint; class ule_constraint; class umul_ovfl_constraint; @@ -31,99 +31,6 @@ namespace polysat { class op_constraint; class signed_constraint; - using constraint_hash = obj_ptr_hash; - using constraint_eq = deref_eq; - using constraint_table = ptr_hashtable; - - using constraints = ptr_vector; - using signed_constraints = vector; - - // Manage constraint lifetime, deduplication, and connection to boolean variables/literals. - class constraint_manager { - friend class constraint; - - bool_var_manager& m_bvars; - - // Constraints indexed by their boolean variable - ptr_vector m_bv2constraint; - // Constraints that have a boolean variable, for deduplication - constraint_table m_constraint_table; - scoped_ptr_vector m_constraints; - - // Clause storage per level - vector> m_clauses; - - // Association to external dependency values (i.e., external names for constraints) - u_map m_external_constraints; - unsigned m_num_external = 0; - - // Manage association of constraints to boolean variables - void assign_bv2c(sat::bool_var bv, constraint* c); - void erase_bv2c(constraint* c); - constraint* get_bv2c(sat::bool_var bv) const; - - void store(constraint* c); - void erase(constraint* c); - - constraint* dedup(constraint* c); - - void gc_constraints(solver& s); - void gc_clauses(solver& s); - - void watch(clause& cl, solver& s, bool value_propagate); - void unwatch(clause& cl); - - void register_clause(clause* cl, solver& s); - - void ensure_bvar(constraint* c); - void erase_bvar(constraint* c); - - public: - constraint_manager(bool_var_manager& bvars): m_bvars(bvars) {} - ~constraint_manager(); - - void store(clause* cl, solver& s, bool value_propagate); - - /// Release clauses at the given level and above. - void release_level(unsigned lvl); - - /// Garbage-collect temporary constraints (i.e., those that do not have a boolean variable). - void gc(solver& s); - bool should_gc(); - - constraint* lookup(sat::bool_var var) const; - signed_constraint lookup(sat::literal lit) const; - - signed_constraint eq(pdd const& p); - signed_constraint ule(pdd const& a, pdd const& b); - signed_constraint ult(pdd const& a, pdd const& b); - signed_constraint sle(pdd const& a, pdd const& b); - signed_constraint slt(pdd const& a, pdd const& b); - signed_constraint umul_ovfl(pdd const& p, pdd const& q); - signed_constraint smul_ovfl(pdd const& p, pdd const& q); - signed_constraint smul_udfl(pdd const& p, pdd const& q); - signed_constraint bit(pdd const& p, unsigned i); - signed_constraint lshr(pdd const& p, pdd const& q, pdd const& r); - signed_constraint band(pdd const& p, pdd const& q, pdd const& r); - - constraint* const* begin() const { return m_constraints.data(); } - constraint* const* end() const { return m_constraints.data() + m_constraints.size(); } - - using clause_iterator = decltype(m_clauses)::const_iterator; - clause_iterator clauses_begin() const { return m_clauses.begin(); } - clause_iterator clauses_end() const { return m_clauses.end(); } - - class clauses_t { - constraint_manager const* m_cm; - public: - clauses_t(constraint_manager const& cm): m_cm(&cm) {} - auto begin() const { return m_cm->clauses_begin(); } - auto end() const { return m_cm->clauses_end(); } - }; - clauses_t clauses() const { return {*this}; } - }; - - /// Normalized inequality: /// lhs <= rhs, if !is_strict /// lhs < rhs, otherwise @@ -246,7 +153,7 @@ namespace polysat { bool is_negative() const { return !is_positive(); } bool is_always_false() const { return get()->is_always_false(is_positive()); } - bool is_always_true() const { return get()->is_always_false(is_negative()); } + bool is_always_true() const { return get()->is_always_false(is_negative()); } bool is_currently_false(solver& s) const { return get()->is_currently_false(s, is_positive()); } bool is_currently_true(solver& s) const { return get()->is_currently_false(s, is_negative()); } bool is_currently_false(solver& s, assignment_t const& sub) const { return get()->is_currently_false(s, sub, is_positive()); } diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp new file mode 100644 index 000000000..39c3a8a1b --- /dev/null +++ b/src/math/polysat/constraint_manager.cpp @@ -0,0 +1,288 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat constraint manager + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-06 + +--*/ + +#include "math/polysat/constraint_manager.h" +#include "math/polysat/clause.h" +#include "math/polysat/solver.h" +#include "math/polysat/log.h" +#include "math/polysat/log_helper.h" +#include "math/polysat/ule_constraint.h" +#include "math/polysat/umul_ovfl_constraint.h" +#include "math/polysat/smul_fl_constraint.h" +#include "math/polysat/op_constraint.h" + +namespace polysat { + + // class constraint_dedup { + // public: + // using op_constraint_args_eq = default_eq; + // using op_constraint_args_hash = obj_hash; + // map op_constraint_vars; + // }; + + constraint_manager::constraint_manager(bool_var_manager& bvars) + : m_bvars(bvars) /*, m_dedup(alloc(constraint_dedup))*/ {} + + void constraint_manager::assign_bv2c(sat::bool_var bv, constraint* c) { + SASSERT_EQ(get_bv2c(bv), nullptr); + SASSERT(!c->has_bvar()); + c->m_bvar = bv; + m_bv2constraint.setx(bv, c, nullptr); + } + + void constraint_manager::erase_bv2c(constraint* c) { + SASSERT(c->has_bvar()); + SASSERT_EQ(get_bv2c(c->bvar()), c); + m_bv2constraint[c->bvar()] = nullptr; + c->m_bvar = sat::null_bool_var; + } + + constraint* constraint_manager::get_bv2c(sat::bool_var bv) const { + return m_bv2constraint.get(bv, nullptr); + } + + void constraint_manager::ensure_bvar(constraint* c) { + if (!c->has_bvar()) + assign_bv2c(m_bvars.new_var(), c); + } + + void constraint_manager::erase_bvar(constraint* c) { + if (c->has_bvar()) + erase_bv2c(c); + } + + /** Add constraint to per-level storage */ + void constraint_manager::store(constraint* c) { + LOG_V("Store constraint: " << show_deref(c)); + m_constraints.push_back(c); + } + + + void constraint_manager::register_clause(clause* cl, solver& s) { + while (m_clauses.size() <= s.base_level()) + m_clauses.push_back({}); + m_clauses[s.base_level()].push_back(cl); + } + + void constraint_manager::store(clause* cl, solver& s, bool value_propagate) { + register_clause(cl, s); + watch(*cl, s, value_propagate); + } + + // Release constraints at the given level and above. + void constraint_manager::release_level(unsigned lvl) { + for (unsigned l = m_clauses.size(); l-- > lvl; ) { + for (auto& cl : m_clauses[l]) { + unwatch(*cl); + SASSERT_EQ(cl->m_ref_count, 1); // otherwise there is a leftover reference somewhere + } + m_clauses[l].reset(); + } + } + + // find literals that are not propagated to false + // if clause is unsat then assign arbitrary + // solver handles unsat clauses by creating a conflict. + // solver also can propagate, but need to check that it does indeed. + void constraint_manager::watch(clause& cl, solver& s, bool value_propagate) { + if (cl.empty()) + return; + + bool first = true; + for (unsigned i = 0; i < cl.size(); ++i) { + if (m_bvars.is_false(cl[i])) + continue; + signed_constraint sc = s.lit2cnstr(cl[i]); + if (value_propagate && sc.is_currently_false(s)) { + if (m_bvars.is_true(cl[i])) { + s.set_conflict(sc); + return; + } + s.assign_eval(~cl[i]); + continue; + } + + m_bvars.watch(cl[i]).push_back(&cl); + std::swap(cl[!first], cl[i]); + if (!first) + return; + first = false; + } + + if (first) + m_bvars.watch(cl[0]).push_back(&cl); + if (cl.size() > 1) + m_bvars.watch(cl[1]).push_back(&cl); + if (m_bvars.is_true(cl[0])) + return; + if (first) + s.set_conflict(cl); + else + s.assign_propagate(cl[0], cl); + } + + void constraint_manager::unwatch(clause& cl) { + if (cl.size() <= 1) + return; + m_bvars.watch(~cl[0]).erase(&cl); + m_bvars.watch(~cl[1]).erase(&cl); + } + + constraint_manager::~constraint_manager() { + // Release explicitly to check for leftover references in debug mode, + // and to make sure all constraints are destructed before the bvar->constraint mapping. + release_level(0); + } + + constraint* constraint_manager::lookup(sat::bool_var var) const { + return get_bv2c(var); + } + + signed_constraint constraint_manager::lookup(sat::literal lit) const { + return {lookup(lit.var()), lit}; + } + + /** Look up constraint among stored constraints. */ + constraint* constraint_manager::dedup(constraint* c1) { + constraint* c2 = nullptr; + if (m_constraint_table.find(c1, c2)) { + dealloc(c1); + return c2; + } + else { + SASSERT(!c1->has_bvar()); + ensure_bvar(c1); + m_constraint_table.insert(c1); + store(c1); + return c1; + } + } + + void constraint_manager::gc(solver& s) { + LOG_H1("gc"); + gc_clauses(s); + gc_constraints(s); + } + + void constraint_manager::gc_clauses(solver& s) { + LOG_H3("gc_clauses"); + // place to gc redundant clauses + } + + void constraint_manager::gc_constraints(solver& s) { + LOG_H3("gc_constraints"); + uint_set used_vars; + for (auto const& cls : m_clauses) + for (auto const& cl : cls) + for (auto lit : *cl) + used_vars.insert(lit.var()); + // anything on the search stack is justified by a clause? + for (auto const& a : s.m_search) + if (a.is_boolean()) + used_vars.insert(a.lit().var()); + for (unsigned i = 0; i < m_constraints.size(); ++i) { + constraint* c = m_constraints[i]; + if (c->has_bvar() && used_vars.contains(c->bvar())) + continue; + if (c->is_external()) + continue; + LOG("Erasing: " << show_deref(c)); + erase_bvar(c); + m_constraints.swap(i, m_constraints.size() - 1); + m_constraints.pop_back(); + --i; + } + + } + + bool constraint_manager::should_gc() { + return false; + // TODO control gc decay rate + return m_constraints.size() > m_num_external + 100; + } + + signed_constraint constraint_manager::ule(pdd const& a, pdd const& b) { + bool is_positive = true; + pdd lhs = a; + pdd rhs = b; + ule_constraint::simplify(is_positive, lhs, rhs); + return { dedup(alloc(ule_constraint, *this, lhs, rhs)), is_positive }; + } + + signed_constraint constraint_manager::eq(pdd const& p) { + return ule(p, p.manager().zero()); + } + + signed_constraint constraint_manager::ult(pdd const& a, pdd const& b) { + return ~ule(b, a); + } + + /** + * encode that the i'th bit of p is 1. + * It holds if p << (K - i - 1) >= 2^{K-1}, where K is the bit-width. + */ + signed_constraint constraint_manager::bit(pdd const& p, unsigned i) { + unsigned K = p.manager().power_of_2(); + pdd q = p * rational::power_of_two(K - i - 1); + rational msb = rational::power_of_two(K - 1); + return ule(p.manager().mk_val(msb), q); + } + + signed_constraint constraint_manager::umul_ovfl(pdd const& a, pdd const& b) { + return { dedup(alloc(umul_ovfl_constraint, *this, a, b)), true }; + } + + signed_constraint constraint_manager::smul_ovfl(pdd const& a, pdd const& b) { + return { dedup(alloc(smul_fl_constraint, *this, a, b, true)), true }; + } + + signed_constraint constraint_manager::smul_udfl(pdd const& a, pdd const& b) { + return { dedup(alloc(smul_fl_constraint, *this, a, b, false)), true }; + } + + signed_constraint constraint_manager::lshr(pdd const& p, pdd const& q, pdd const& r) { + return { dedup(alloc(op_constraint, *this, op_constraint::code::lshr_op, p, q, r)), true }; + } + + signed_constraint constraint_manager::band(pdd const& p, pdd const& q, pdd const& r) { + return { dedup(alloc(op_constraint, *this, op_constraint::code::and_op, p, q, r)), true }; + } + + // To do signed comparison of bitvectors, flip the msb and do unsigned comparison: + // + // x <=s y <=> x + 2^(w-1) <=u y + 2^(w-1) + // + // Example for bit width 3: + // 111 -1 + // 110 -2 + // 101 -3 + // 100 -4 + // 011 3 + // 010 2 + // 001 1 + // 000 0 + // + // Argument: flipping the msb swaps the negative and non-negative blocks + // + signed_constraint constraint_manager::sle(pdd const& a, pdd const& b) { + auto shift = rational::power_of_two(a.power_of_2() - 1); + return ule(a + shift, b + shift); + } + + signed_constraint constraint_manager::slt(pdd const& a, pdd const& b) { + auto shift = rational::power_of_two(a.power_of_2() - 1); + return ult(a + shift, b + shift); + } + +} diff --git a/src/math/polysat/constraint_manager.h b/src/math/polysat/constraint_manager.h new file mode 100644 index 000000000..1913450a5 --- /dev/null +++ b/src/math/polysat/constraint_manager.h @@ -0,0 +1,122 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat constraint manager + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-06 + +--*/ +#pragma once +#include "math/polysat/constraint.h" +#include "math/polysat/clause.h" +#include + +namespace polysat { + + class constraint; + class ule_constraint; + class umul_ovfl_constraint; + class smul_fl_constraint; + class op_constraint; + class signed_constraint; + + using constraint_hash = obj_ptr_hash; + using constraint_eq = deref_eq; + using constraint_table = ptr_hashtable; + + using constraints = ptr_vector; + using signed_constraints = vector; + + // Manage constraint lifetime, deduplication, and connection to boolean variables/literals. + class constraint_manager { + friend class constraint; + + bool_var_manager& m_bvars; + + // Constraints indexed by their boolean variable + ptr_vector m_bv2constraint; + // Constraints that have a boolean variable, for deduplication + constraint_table m_constraint_table; + scoped_ptr_vector m_constraints; + + // scoped_ptr m_dedup; + + // Clause storage per level + vector> m_clauses; + + // Association to external dependency values (i.e., external names for constraints) + u_map m_external_constraints; + unsigned m_num_external = 0; + + // Manage association of constraints to boolean variables + void assign_bv2c(sat::bool_var bv, constraint* c); + void erase_bv2c(constraint* c); + constraint* get_bv2c(sat::bool_var bv) const; + + void store(constraint* c); + void erase(constraint* c); + + constraint* dedup(constraint* c); + + void gc_constraints(solver& s); + void gc_clauses(solver& s); + + void watch(clause& cl, solver& s, bool value_propagate); + void unwatch(clause& cl); + + void register_clause(clause* cl, solver& s); + + void ensure_bvar(constraint* c); + void erase_bvar(constraint* c); + + public: + constraint_manager(bool_var_manager& bvars); + ~constraint_manager(); + + void store(clause* cl, solver& s, bool value_propagate); + + /// Release clauses at the given level and above. + void release_level(unsigned lvl); + + /// Garbage-collect temporary constraints (i.e., those that do not have a boolean variable). + void gc(solver& s); + bool should_gc(); + + constraint* lookup(sat::bool_var var) const; + signed_constraint lookup(sat::literal lit) const; + + signed_constraint eq(pdd const& p); + signed_constraint ule(pdd const& a, pdd const& b); + signed_constraint ult(pdd const& a, pdd const& b); + signed_constraint sle(pdd const& a, pdd const& b); + signed_constraint slt(pdd const& a, pdd const& b); + signed_constraint umul_ovfl(pdd const& p, pdd const& q); + signed_constraint smul_ovfl(pdd const& p, pdd const& q); + signed_constraint smul_udfl(pdd const& p, pdd const& q); + signed_constraint bit(pdd const& p, unsigned i); + signed_constraint lshr(pdd const& p, pdd const& q, pdd const& r); + signed_constraint band(pdd const& p, pdd const& q, pdd const& r); + + constraint* const* begin() const { return m_constraints.data(); } + constraint* const* end() const { return m_constraints.data() + m_constraints.size(); } + + using clause_iterator = decltype(m_clauses)::const_iterator; + clause_iterator clauses_begin() const { return m_clauses.begin(); } + clause_iterator clauses_end() const { return m_clauses.end(); } + + class clauses_t { + constraint_manager const* m_cm; + public: + clauses_t(constraint_manager const& cm): m_cm(&cm) {} + auto begin() const { return m_cm->clauses_begin(); } + auto end() const { return m_cm->clauses_end(); } + }; + clauses_t clauses() const { return {*this}; } + }; + +} diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index e4c871725..ab341661b 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -22,6 +22,7 @@ Author: #include "math/polysat/boolean.h" #include "math/polysat/conflict.h" #include "math/polysat/constraint.h" +#include "math/polysat/constraint_manager.h" #include "math/polysat/clause_builder.h" #include "math/polysat/simplify_clause.h" #include "math/polysat/simplify.h"