From 2953b1c093f459f7a9d4370ea0a409fa29640a16 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 7 Nov 2022 15:02:48 +0100 Subject: [PATCH] Dedup op constraints --- src/math/polysat/constraint.h | 5 ++-- src/math/polysat/constraint_manager.cpp | 17 ++++++------- src/math/polysat/constraint_manager.h | 32 ++++++++++++------------- src/math/polysat/op_constraint.cpp | 20 +++++++++------- src/math/polysat/op_constraint.h | 27 ++++++++++++++++++--- 5 files changed, 61 insertions(+), 40 deletions(-) diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index acf738580..763bed7eb 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -31,6 +31,9 @@ namespace polysat { class op_constraint; class signed_constraint; + using constraints = ptr_vector; + using signed_constraints = vector; + /// Normalized inequality: /// lhs <= rhs, if !is_strict /// lhs < rhs, otherwise @@ -44,7 +47,6 @@ namespace polysat { signed_constraint as_signed_constraint() const; }; - class constraint { friend class constraint_manager; friend class signed_constraint; @@ -126,7 +128,6 @@ namespace polysat { inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); } - class signed_constraint final { public: using ptr_t = constraint*; diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp index 078d92aaf..3c6ccadf0 100644 --- a/src/math/polysat/constraint_manager.cpp +++ b/src/math/polysat/constraint_manager.cpp @@ -24,13 +24,6 @@ Author: 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(solver& s): s(s) {} void constraint_manager::assign_bv2c(sat::bool_var bv, constraint* c) { @@ -155,14 +148,14 @@ namespace polysat { /** Look up constraint among stored constraints. */ constraint* constraint_manager::dedup(constraint* c1) { constraint* c2 = nullptr; - if (m_constraint_table.find(c1, c2)) { + if (m_dedup.constraints.find(c1, c2)) { dealloc(c1); return c2; } else { SASSERT(!c1->has_bvar()); ensure_bvar(c1); - m_constraint_table.insert(c1); + m_dedup.constraints.insert(c1); store(c1); return c1; } @@ -289,10 +282,14 @@ namespace polysat { } pdd constraint_manager::band(pdd const& p, pdd const& q) { + op_constraint_args const args(op_constraint::code::and_op, p, q); auto& m = p.manager(); + auto it = m_dedup.op_constraint_expr.find_iterator(args); + if (it != m_dedup.op_constraint_expr.end()) + return m.mk_var(it->m_value); unsigned sz = m.power_of_2(); - // TODO: return existing r if we call again with the same arguments pdd r = m.mk_var(s.add_var(sz)); + m_dedup.op_constraint_expr.insert(args, r.var()); s.assign_eh(band(p, q, r), null_dependency); return r; } diff --git a/src/math/polysat/constraint_manager.h b/src/math/polysat/constraint_manager.h index edc8849e6..f302633ed 100644 --- a/src/math/polysat/constraint_manager.h +++ b/src/math/polysat/constraint_manager.h @@ -12,25 +12,24 @@ Author: --*/ #pragma once -#include "math/polysat/constraint.h" #include "math/polysat/clause.h" -#include +#include "math/polysat/constraint.h" +#include "math/polysat/op_constraint.h" namespace polysat { - class constraint; - class ule_constraint; - class umul_ovfl_constraint; - class smul_fl_constraint; - class op_constraint; - class signed_constraint; + class constraint_dedup { + public: + using constraint_hash = obj_ptr_hash; + using constraint_eq = deref_eq; + using constraint_table = ptr_hashtable; + constraint_table constraints; - using constraint_hash = obj_ptr_hash; - using constraint_eq = deref_eq; - using constraint_table = ptr_hashtable; - - using constraints = ptr_vector; - using signed_constraints = vector; + using op_constraint_args_eq = default_eq; + using op_constraint_args_hash = obj_hash; + using op_constraint_expr_map = map; + op_constraint_expr_map op_constraint_expr; + }; // Manage constraint lifetime, deduplication, and connection to boolean variables/literals. class constraint_manager { @@ -40,11 +39,10 @@ namespace polysat { // 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; + constraint_dedup m_dedup; // Clause storage per level vector> m_clauses; diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp index f9f62ca93..cca3fd976 100644 --- a/src/math/polysat/op_constraint.cpp +++ b/src/math/polysat/op_constraint.cpp @@ -75,7 +75,11 @@ namespace polysat { } bool op_constraint::is_currently_false(solver& s, bool is_positive) const { - return is_always_false(is_positive, s.subst(p()), s.subst(q()), s.subst(r())); + return is_always_false(is_positive, s.subst(p()), s.subst(q()), s.subst(r())); + } + + bool op_constraint::is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const { + return is_always_false(is_positive, s.subst(sub, p()), s.subst(sub, q()), s.subst(sub, r())); } std::ostream& op_constraint::display(std::ostream& out, lbool status) const { @@ -189,7 +193,7 @@ namespace polysat { // q = 0 -> p = r s.add_clause(~lshr, ~s.eq(q()), s.eq(p(), r()), true); else if (qv.is_val() && !qv.is_zero() && pv.is_val() && rv.is_val() && !pv.is_zero() && pv.val() <= rv.val()) - // q != 0 & p > 0 => r < p + // q != 0 & p > 0 => r < p s.add_clause(~lshr, s.eq(q()), s.ule(p(), 0), s.ult(r(), p()), true); else if (qv.is_val() && !qv.is_zero() && qv.val() < K && rv.is_val() && rv.val() > rational::power_of_two(K - qv.val().get_unsigned() - 1)) @@ -197,7 +201,7 @@ namespace polysat { s.add_clause(~lshr, ~s.ule(qv.val(), q()), s.ule(r(), rational::power_of_two(K - qv.val().get_unsigned() - 1)), true); else if (qv.is_val() && qv.val() >= K && rv.is_val() && !rv.is_zero()) // q >= K -> r = 0 - s.add_clause(~lshr, ~s.ule(K, q()), s.eq(r()), true); + s.add_clause(~lshr, ~s.ule(K, q()), s.eq(r()), true); // q = k -> r[i - k] = p[i] for K - k <= i < K else if (pv.is_val() && rv.is_val() && qv.is_val() && !qv.is_zero()) { unsigned k = qv.val().get_unsigned(); @@ -222,11 +226,11 @@ namespace polysat { if (p.is_val() && q.is_val() && r.is_val()) return r == p * m.mk_val(rational::power_of_two(q.val().get_unsigned())) ? l_true : l_false; - + if (q.is_val() && q.val() >= m.power_of_2() && r.is_val()) return r.is_zero() ? l_true : l_false; - - // other cases when we know lower + + // other cases when we know lower // bound of q, e.g, q = 2^k*q1 + q2, where q2 is a constant. return l_undef; } @@ -239,7 +243,7 @@ namespace polysat { * p = 0 => r = 0 * q = 0 => r = 0 * p[i] && q[i] = r[i] - * + * * Possible other: * p = max_value => q = r * q = max_value => p = r @@ -248,7 +252,7 @@ namespace polysat { auto pv = s.subst(p()); auto qv = s.subst(q()); auto rv = s.subst(r()); - + signed_constraint andc(this, true); if (pv.is_val() && rv.is_val() && rv.val() > pv.val()) s.add_clause(~andc, s.ule(r(), p()), true); diff --git a/src/math/polysat/op_constraint.h b/src/math/polysat/op_constraint.h index 4a5d572fc..79f9db563 100644 --- a/src/math/polysat/op_constraint.h +++ b/src/math/polysat/op_constraint.h @@ -12,7 +12,7 @@ Module Name: or: r == p | q not: r == ~p xor: r == p ^ q - + Author: Jakob Rath, Nikolaj Bjorner (nbjorner) 2021-12-09 @@ -20,6 +20,7 @@ Author: --*/ #pragma once #include "math/polysat/constraint.h" +#include namespace polysat { @@ -48,7 +49,7 @@ namespace polysat { void narrow_and(solver& s); static lbool eval_and(pdd const& p, pdd const& q, pdd const& r); - public: + public: ~op_constraint() override {} pdd const& p() const { return m_p; } pdd const& q() const { return m_q; } @@ -57,7 +58,7 @@ namespace polysat { std::ostream& display(std::ostream& out) const override; bool is_always_false(bool is_positive) const override; bool is_currently_false(solver& s, bool is_positive) const override; - bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const override { return false; } + bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const override; void narrow(solver& s, bool is_positive, bool first) override; inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); } unsigned hash() const override; @@ -67,4 +68,24 @@ namespace polysat { void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override; }; + struct op_constraint_args { + op_constraint::code op; + // NOTE: this is only optional because table2map requires a default constructor + std::optional> args; + + op_constraint_args() = default; + op_constraint_args(op_constraint::code op, pdd lhs, pdd rhs) + : op(op), args({std::move(lhs), std::move(rhs)}) {} + + bool operator==(op_constraint_args const& other) const { + return op == other.op && args == other.args; + } + + unsigned hash() const { + unsigned const lhs_hash = args ? args->first.hash() : 0; + unsigned const rhs_hash = args ? args->second.hash() : 0; + return mk_mix(static_cast(op), lhs_hash, rhs_hash); + } + }; + }