From e7c77a22abc0c905f102534d9b8755887997b863 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 7 Nov 2022 15:25:05 +0100 Subject: [PATCH] Dedup quot_rem and lshr too --- src/math/polysat/constraint_manager.cpp | 56 ++++++++++++++++++++++++- src/math/polysat/constraint_manager.h | 14 +++++++ src/math/polysat/solver.cpp | 33 --------------- src/math/polysat/solver.h | 8 ++-- 4 files changed, 71 insertions(+), 40 deletions(-) diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp index 3c6ccadf0..c675c9f73 100644 --- a/src/math/polysat/constraint_manager.cpp +++ b/src/math/polysat/constraint_manager.cpp @@ -277,19 +277,71 @@ namespace polysat { return ult(a + shift, b + shift); } + std::pair constraint_manager::quot_rem(pdd const& a, pdd const& b) { + auto& m = a.manager(); + unsigned sz = m.power_of_2(); + if (a.is_val() && b.is_val()) { + // TODO: just evaluate? + } + + constraint_dedup::quot_rem_args args({a, b}); + auto it = m_dedup.quot_rem_expr.find_iterator(args); + if (it != m_dedup.quot_rem_expr.end()) + return { m.mk_var(it->m_value.first), m.mk_var(it->m_value.second) }; + + pdd q = m.mk_var(s.add_var(sz)); // quotient + pdd r = m.mk_var(s.add_var(sz)); // remainder + m_dedup.quot_rem_expr.insert(args, { q.var(), r.var() }); + + // 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 (TODO: maybe the version with disjunction is easier for the solver; should compare later) + // b ≠ 0 ==> r < b + // b = 0 ==> q = -1 + s.add_eq(a, b * q + r); + s.add_umul_noovfl(b, q); + s.add_ule(r, b*q+r); + + auto c_eq = eq(b); + s.add_clause(c_eq, ult(r, b), false); + s.add_clause(~c_eq, eq(q + 1), false); + + return {q, r}; + } + + pdd constraint_manager::lshr(pdd const& p, pdd const& q) { + auto& m = p.manager(); + unsigned sz = m.power_of_2(); + + op_constraint_args const args(op_constraint::code::lshr_op, p, q); + 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); + + pdd r = m.mk_var(s.add_var(sz)); + m_dedup.op_constraint_expr.insert(args, r.var()); + + s.assign_eh(lshr(p, q, r), null_dependency); + return r; + } + pdd constraint_manager::bnot(pdd const& p) { return -p - 1; } 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(); + unsigned sz = m.power_of_2(); + + op_constraint_args const args(op_constraint::code::and_op, p, q); 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(); + 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 f302633ed..9e0da588a 100644 --- a/src/math/polysat/constraint_manager.h +++ b/src/math/polysat/constraint_manager.h @@ -29,6 +29,16 @@ namespace polysat { using op_constraint_args_hash = obj_hash; using op_constraint_expr_map = map; op_constraint_expr_map op_constraint_expr; + + using quot_rem_args = std::optional>; // NOTE: this is only wrapped in optional because table2map requires a default constructor + using quot_rem_args_eq = default_eq; + struct quot_rem_args_hash { + unsigned operator()(quot_rem_args const& args) const { + return args ? combine_hash(args->first.hash(), args->second.hash()) : 0; + } + }; + using quot_rem_expr_map = map, quot_rem_args_hash, quot_rem_args_eq>; + quot_rem_expr_map quot_rem_expr; }; // Manage constraint lifetime, deduplication, and connection to boolean variables/literals. @@ -100,6 +110,10 @@ namespace polysat { signed_constraint lshr(pdd const& p, pdd const& q, pdd const& r); signed_constraint band(pdd const& p, pdd const& q, pdd const& r); + std::pair quot_rem(pdd const& a, pdd const& b); + + pdd lshr(pdd const& p, pdd const& q); + pdd bnot(pdd const& p); pdd band(pdd const& p, pdd const& q); pdd bor(pdd const& p, pdd const& q); diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 7c3346d56..915851557 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -133,39 +133,6 @@ namespace polysat { m_free_pvars.del_var_eh(v); } - std::tuple solver::quot_rem(pdd const& a, pdd const& b) { - auto& m = a.manager(); - unsigned sz = m.power_of_2(); - if (a.is_val() && b.is_val()) { - // TODO: just evaluate? - } - pdd q = m.mk_var(add_var(sz)); // quotient - pdd r = m.mk_var(add_var(sz)); // remainder - // 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 (TODO: maybe the version with disjunction is easier for the solver; should compare later) - // b ≠ 0 ==> r < b - // b = 0 ==> q = -1 - add_eq(a, b * q + r); - add_umul_noovfl(b, q); - add_ule(r, b*q+r); - - auto c_eq = eq(b); - add_clause(c_eq, ult(r, b), false); - add_clause(~c_eq, eq(q + 1), false); - - return std::tuple(q, r); - } - - pdd solver::lshr(pdd const& p, pdd const& q) { - auto& m = p.manager(); - unsigned sz = m.power_of_2(); - pdd r = m.mk_var(add_var(sz)); - assign_eh(m_constraints.lshr(p, q, r), null_dependency); - return r; - } - void solver::assign_eh(signed_constraint c, dependency dep) { backjump(base_level()); SASSERT(at_base_level()); diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 67eb8e9a9..6bd34cebb 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -305,12 +305,10 @@ namespace polysat { * ~ovfl(b*quot) * rem < b or b = 0 */ - std::tuple quot_rem(pdd const& a, pdd const& b); + std::pair quot_rem(pdd const& a, pdd const& b) { return m_constraints.quot_rem(a, b); } - /** - * Create expression for the logical right shift of p by q. - */ - pdd lshr(pdd const& p, pdd const& q); + /** Create expression for the logical right shift of p by q. */ + pdd lshr(pdd const& p, pdd const& q) { return m_constraints.lshr(p, q); } /** Create expression for the bit-wise negation of p. */ pdd bnot(pdd const& p) { return m_constraints.bnot(p); }