From 48c6bea3314fd2e22fec051faf296d6a859af911 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 21 Jul 2022 12:38:00 +0200 Subject: [PATCH] umul 2 --- src/math/polysat/CMakeLists.txt | 4 +- src/math/polysat/constraint.cpp | 14 +++---- src/math/polysat/constraint.h | 14 +++---- src/math/polysat/forbidden_intervals.cpp | 14 +++---- src/math/polysat/forbidden_intervals.h | 4 +- src/math/polysat/solver.h | 4 +- ...onstraint.cpp => umul_ovfl_constraint.cpp} | 38 +++++++++---------- ...fl_constraint.h => umul_ovfl_constraint.h} | 6 +-- 8 files changed, 48 insertions(+), 50 deletions(-) rename src/math/polysat/{mul_ovfl_constraint.cpp => umul_ovfl_constraint.cpp} (74%) rename src/math/polysat/{mul_ovfl_constraint.h => umul_ovfl_constraint.h} (91%) diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt index b5a36967a..c18ca7189 100644 --- a/src/math/polysat/CMakeLists.txt +++ b/src/math/polysat/CMakeLists.txt @@ -11,7 +11,6 @@ z3_add_component(polysat justification.cpp linear_solver.cpp log.cpp - mul_ovfl_constraint.cpp op_constraint.cpp restart.cpp saturation.cpp @@ -20,8 +19,9 @@ z3_add_component(polysat smul_fl_constraint.cpp solver.cpp ule_constraint.cpp - viable.cpp + umul_ovfl_constraint.cpp variable_elimination.cpp + viable.cpp COMPONENT_DEPENDENCIES util dd diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index d2caf645f..ec0a2df69 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -18,7 +18,7 @@ Author: #include "math/polysat/log.h" #include "math/polysat/log_helper.h" #include "math/polysat/ule_constraint.h" -#include "math/polysat/mul_ovfl_constraint.h" +#include "math/polysat/umul_ovfl_constraint.h" #include "math/polysat/smul_fl_constraint.h" #include "math/polysat/op_constraint.h" @@ -236,8 +236,8 @@ namespace polysat { return ule(p.manager().mk_val(msb), q); } - signed_constraint constraint_manager::mul_ovfl(pdd const& a, pdd const& b) { - return { dedup(alloc(mul_ovfl_constraint, *this, a, b)), true }; + 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) { @@ -294,12 +294,12 @@ namespace polysat { return *dynamic_cast(this); } - mul_ovfl_constraint& constraint::to_mul_ovfl() { - return *dynamic_cast(this); + umul_ovfl_constraint& constraint::to_umul_ovfl() { + return *dynamic_cast(this); } - mul_ovfl_constraint const& constraint::to_mul_ovfl() const { - return *dynamic_cast(this); + umul_ovfl_constraint const& constraint::to_umul_ovfl() const { + return *dynamic_cast(this); } smul_fl_constraint& constraint::to_smul_fl() { diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index d8bb5da8b..d6a38304c 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -22,11 +22,11 @@ Author: namespace polysat { - enum ckind_t { ule_t, mul_ovfl_t, smul_fl_t, op_t }; + enum ckind_t { ule_t, umul_ovfl_t, smul_fl_t, op_t }; class constraint; class ule_constraint; - class mul_ovfl_constraint; + class umul_ovfl_constraint; class smul_fl_constraint; class op_constraint; class signed_constraint; @@ -99,7 +99,7 @@ namespace polysat { 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 mul_ovfl(pdd const& p, pdd const& q); + 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); @@ -142,7 +142,7 @@ namespace polysat { friend class constraint_manager; friend class clause; friend class ule_constraint; - friend class mul_ovfl_constraint; + friend class umul_ovfl_constraint; friend class smul_fl_constraint; friend class op_constraint; @@ -169,7 +169,7 @@ namespace polysat { virtual bool is_eq() const { return false; } virtual bool is_diseq() const { return false; } bool is_ule() const { return m_kind == ckind_t::ule_t; } - bool is_mul_ovfl() const { return m_kind == ckind_t::mul_ovfl_t; } + bool is_umul_ovfl() const { return m_kind == ckind_t::umul_ovfl_t; } bool is_smul_fl() const { return m_kind == ckind_t::smul_fl_t; } bool is_op() const { return m_kind == ckind_t::op_t; } ckind_t kind() const { return m_kind; } @@ -186,8 +186,8 @@ namespace polysat { ule_constraint& to_ule(); ule_constraint const& to_ule() const; - mul_ovfl_constraint& to_mul_ovfl(); - mul_ovfl_constraint const& to_mul_ovfl() const; + umul_ovfl_constraint& to_umul_ovfl(); + umul_ovfl_constraint const& to_umul_ovfl() const; smul_fl_constraint& to_smul_fl(); smul_fl_constraint const& to_smul_fl() const; op_constraint& to_op(); diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index 4aea096aa..a767f6733 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -17,7 +17,7 @@ Author: #include "math/polysat/interval.h" #include "math/polysat/solver.h" #include "math/polysat/log.h" -#include "math/polysat/mul_ovfl_constraint.h" +#include "math/polysat/umul_ovfl_constraint.h" namespace polysat { @@ -31,14 +31,12 @@ namespace polysat { bool forbidden_intervals::get_interval(signed_constraint const& c, pvar v, fi_record& fi) { if (c->is_ule()) return get_interval_ule(c, v, fi); - if (c->is_mul_ovfl()) - return get_interval_mul_ovfl(c, v, fi); + if (c->is_umul_ovfl()) + return get_interval_umul_ovfl(c, v, fi); return false; } - - - bool forbidden_intervals::get_interval_mul_ovfl(signed_constraint const& c, pvar v, fi_record& fi) { + bool forbidden_intervals::get_interval_umul_ovfl(signed_constraint const& c, pvar v, fi_record& fi) { backtrack _backtrack(fi.side_cond); @@ -48,8 +46,8 @@ namespace polysat { // eval(lhs) = a1*v + eval(e1) = a1*v + b1 // eval(rhs) = a2*v + eval(e2) = a2*v + b2 // We keep the e1, e2 around in case we need side conditions such as e1=b1, e2=b2. - auto [ok1, a1, e1, b1] = linear_decompose(v, c->to_mul_ovfl().p(), fi.side_cond); - auto [ok2, a2, e2, b2] = linear_decompose(v, c->to_mul_ovfl().q(), fi.side_cond); + auto [ok1, a1, e1, b1] = linear_decompose(v, c->to_umul_ovfl().p(), fi.side_cond); + auto [ok2, a2, e2, b2] = linear_decompose(v, c->to_umul_ovfl().q(), fi.side_cond); auto& m = e1.manager(); rational bound = m.max_value(); diff --git a/src/math/polysat/forbidden_intervals.h b/src/math/polysat/forbidden_intervals.h index 17e84c370..a61fe1c26 100644 --- a/src/math/polysat/forbidden_intervals.h +++ b/src/math/polysat/forbidden_intervals.h @@ -71,8 +71,8 @@ namespace polysat { fi_record& fi); bool get_interval_ule(signed_constraint const& c, pvar v, fi_record& fi); - - bool get_interval_mul_ovfl(signed_constraint const& c, pvar v, fi_record& fi); + + bool get_interval_umul_ovfl(signed_constraint const& c, pvar v, fi_record& fi); struct backtrack { bool released = false; diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index ee6d2ff89..a424e28e7 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -60,7 +60,7 @@ namespace polysat { friend class constraint; friend class ule_constraint; - friend class mul_ovfl_constraint; + friend class umul_ovfl_constraint; friend class smul_fl_constraint; friend class op_constraint; friend class signed_constraint; @@ -344,7 +344,7 @@ namespace polysat { signed_constraint sgt(pdd const& p, pdd const& q) { return slt(q, p); } signed_constraint sgt(pdd const& p, int n) { return slt(n, p); } signed_constraint sgt(int n, pdd const& p) { return slt(p, n); } - signed_constraint umul_ovfl(pdd const& p, pdd const& q) { return m_constraints.mul_ovfl(p, q); } + signed_constraint umul_ovfl(pdd const& p, pdd const& q) { return m_constraints.umul_ovfl(p, q); } signed_constraint umul_ovfl(rational const& p, pdd const& q) { return umul_ovfl(q.manager().mk_val(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); } diff --git a/src/math/polysat/mul_ovfl_constraint.cpp b/src/math/polysat/umul_ovfl_constraint.cpp similarity index 74% rename from src/math/polysat/mul_ovfl_constraint.cpp rename to src/math/polysat/umul_ovfl_constraint.cpp index 5ad4d3218..1081abed9 100644 --- a/src/math/polysat/mul_ovfl_constraint.cpp +++ b/src/math/polysat/umul_ovfl_constraint.cpp @@ -10,13 +10,13 @@ Author: Jakob Rath, Nikolaj Bjorner (nbjorner) 2021-12-09 --*/ -#include "math/polysat/mul_ovfl_constraint.h" +#include "math/polysat/umul_ovfl_constraint.h" #include "math/polysat/solver.h" namespace polysat { - mul_ovfl_constraint::mul_ovfl_constraint(constraint_manager& m, pdd const& p, pdd const& q): - constraint(m, ckind_t::mul_ovfl_t), m_p(p), m_q(q) { + umul_ovfl_constraint::umul_ovfl_constraint(constraint_manager& m, pdd const& p, pdd const& q): + constraint(m, ckind_t::umul_ovfl_t), m_p(p), m_q(q) { simplify(); m_vars.append(m_p.free_vars()); for (auto v : m_q.free_vars()) @@ -24,7 +24,7 @@ namespace polysat { m_vars.push_back(v); } - void mul_ovfl_constraint::simplify() { + void umul_ovfl_constraint::simplify() { if (m_p.is_zero() || m_q.is_zero() || m_p.is_one() || m_q.is_one()) { m_q = 0; @@ -35,7 +35,7 @@ namespace polysat { std::swap(m_p, m_q); } - std::ostream& mul_ovfl_constraint::display(std::ostream& out, lbool status) const { + std::ostream& umul_ovfl_constraint::display(std::ostream& out, lbool status) const { switch (status) { case l_true: return display(out); case l_false: return display(out << "~"); @@ -44,11 +44,11 @@ namespace polysat { return out; } - std::ostream& mul_ovfl_constraint::display(std::ostream& out) const { + std::ostream& umul_ovfl_constraint::display(std::ostream& out) const { return out << "ovfl*(" << m_p << ", " << m_q << ")"; } - lbool mul_ovfl_constraint::eval(pdd const& p, pdd const& q) const { + lbool umul_ovfl_constraint::eval(pdd const& p, pdd const& q) const { if (p.is_zero() || q.is_zero() || p.is_one() || q.is_one()) return l_false; @@ -61,7 +61,7 @@ namespace polysat { return l_undef; } - bool mul_ovfl_constraint::is_always_false(bool is_positive, pdd const& p, pdd const& q) const { + bool umul_ovfl_constraint::is_always_false(bool is_positive, pdd const& p, pdd const& q) const { switch (eval(p, q)) { case l_true: return !is_positive; case l_false: return is_positive; @@ -69,7 +69,7 @@ namespace polysat { } } - bool mul_ovfl_constraint::is_always_true(bool is_positive, pdd const& p, pdd const& q) const { + bool umul_ovfl_constraint::is_always_true(bool is_positive, pdd const& p, pdd const& q) const { switch (eval(p, q)) { case l_true: return is_positive; case l_false: return !is_positive; @@ -77,20 +77,20 @@ namespace polysat { } } - bool mul_ovfl_constraint::is_always_false(bool is_positive) const { + bool umul_ovfl_constraint::is_always_false(bool is_positive) const { return is_always_false(is_positive, m_p, m_q); } - bool mul_ovfl_constraint::is_currently_false(solver& s, bool is_positive) const { + bool umul_ovfl_constraint::is_currently_false(solver& s, bool is_positive) const { return is_always_false(is_positive, s.subst(p()), s.subst(q())); } - bool mul_ovfl_constraint::is_currently_true(solver& s, bool is_positive) const { + bool umul_ovfl_constraint::is_currently_true(solver& s, bool is_positive) const { return is_always_true(is_positive, s.subst(p()), s.subst(q())); } - void mul_ovfl_constraint::narrow(solver& s, bool is_positive, bool first) { + void umul_ovfl_constraint::narrow(solver& s, bool is_positive, bool first) { auto p1 = s.subst(p()); auto q1 = s.subst(q()); @@ -115,7 +115,7 @@ namespace polysat { /** * if p constant, q, propagate inequality */ - bool mul_ovfl_constraint::narrow_bound(solver& s, bool is_positive, + bool umul_ovfl_constraint::narrow_bound(solver& s, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q) { if (!p.is_val()) @@ -151,7 +151,7 @@ namespace polysat { return true; } - bool mul_ovfl_constraint::try_viable( + bool umul_ovfl_constraint::try_viable( solver& s, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q) { signed_constraint sc(this, is_positive); @@ -159,15 +159,15 @@ namespace polysat { } - unsigned mul_ovfl_constraint::hash() const { + unsigned umul_ovfl_constraint::hash() const { return mk_mix(p().hash(), q().hash(), kind()); } - bool mul_ovfl_constraint::operator==(constraint const& other) const { - return other.is_mul_ovfl() && p() == other.to_mul_ovfl().p() && q() == other.to_mul_ovfl().q(); + bool umul_ovfl_constraint::operator==(constraint const& other) const { + return other.is_umul_ovfl() && p() == other.to_umul_ovfl().p() && q() == other.to_umul_ovfl().q(); } - void mul_ovfl_constraint::add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const { + void umul_ovfl_constraint::add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const { auto p_coeff = s.subst(p()).get_univariate_coefficients(); auto q_coeff = s.subst(q()).get_univariate_coefficients(); us.add_umul_ovfl(p_coeff, q_coeff, !is_positive, dep); diff --git a/src/math/polysat/mul_ovfl_constraint.h b/src/math/polysat/umul_ovfl_constraint.h similarity index 91% rename from src/math/polysat/mul_ovfl_constraint.h rename to src/math/polysat/umul_ovfl_constraint.h index e296c95c0..d3c8f357f 100644 --- a/src/math/polysat/mul_ovfl_constraint.h +++ b/src/math/polysat/umul_ovfl_constraint.h @@ -17,13 +17,13 @@ namespace polysat { class solver; - class mul_ovfl_constraint final : public constraint { + class umul_ovfl_constraint final : public constraint { friend class constraint_manager; pdd m_p; pdd m_q; - mul_ovfl_constraint(constraint_manager& m, pdd const& p, pdd const& q); + umul_ovfl_constraint(constraint_manager& m, pdd const& p, pdd const& q); void simplify(); bool is_always_false(bool is_positive, pdd const& p, pdd const& q) const; bool is_always_true(bool is_positive, pdd const& p, pdd const& q) const; @@ -32,7 +32,7 @@ namespace polysat { lbool eval(pdd const& p, pdd const& q) const; public: - ~mul_ovfl_constraint() override {} + ~umul_ovfl_constraint() override {} pdd const& p() const { return m_p; } pdd const& q() const { return m_q; } std::ostream& display(std::ostream& out, lbool status) const override;