diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt index 87633140a..d387a1a5c 100644 --- a/src/math/polysat/CMakeLists.txt +++ b/src/math/polysat/CMakeLists.txt @@ -17,7 +17,7 @@ z3_add_component(polysat saturation.cpp search_state.cpp simplify.cpp - smul_ovfl_constraint.cpp + smul_fl_constraint.cpp solver.cpp ule_constraint.cpp viable.cpp diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index a3ae7a1d5..81347c5ea 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -19,7 +19,7 @@ Author: #include "math/polysat/log_helper.h" #include "math/polysat/ule_constraint.h" #include "math/polysat/mul_ovfl_constraint.h" -#include "math/polysat/smul_ovfl_constraint.h" +#include "math/polysat/smul_fl_constraint.h" #include "math/polysat/op_constraint.h" namespace polysat { @@ -239,7 +239,11 @@ namespace polysat { } signed_constraint constraint_manager::smul_ovfl(pdd const& a, pdd const& b) { - return { dedup(alloc(smul_ovfl_constraint, *this, a, b)), true }; + 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) { @@ -296,12 +300,12 @@ namespace polysat { return *dynamic_cast(this); } - smul_ovfl_constraint& constraint::to_smul_ovfl() { - return *dynamic_cast(this); + smul_fl_constraint& constraint::to_smul_fl() { + return *dynamic_cast(this); } - smul_ovfl_constraint const& constraint::to_smul_ovfl() const { - return *dynamic_cast(this); + smul_fl_constraint const& constraint::to_smul_fl() const { + return *dynamic_cast(this); } op_constraint& constraint::to_op() { diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index ec508a55c..a8d65be05 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -20,12 +20,12 @@ Author: namespace polysat { - enum ckind_t { ule_t, mul_ovfl_t, smul_ovfl_t, op_t }; + enum ckind_t { ule_t, mul_ovfl_t, smul_fl_t, op_t }; class constraint; class ule_constraint; class mul_ovfl_constraint; - class smul_ovfl_constraint; + class smul_fl_constraint; class op_constraint; class signed_constraint; @@ -100,6 +100,7 @@ namespace polysat { signed_constraint slt(pdd const& a, pdd const& b); signed_constraint mul_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); @@ -141,7 +142,7 @@ namespace polysat { friend class clause; friend class ule_constraint; friend class mul_ovfl_constraint; - friend class smul_ovfl_constraint; + friend class smul_fl_constraint; friend class op_constraint; // constraint_manager* m_manager; @@ -170,7 +171,7 @@ namespace polysat { 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_smul_ovfl() const { return m_kind == ckind_t::smul_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; } virtual std::ostream& display(std::ostream& out, lbool status) const = 0; @@ -190,8 +191,8 @@ namespace polysat { ule_constraint const& to_ule() const; mul_ovfl_constraint& to_mul_ovfl(); mul_ovfl_constraint const& to_mul_ovfl() const; - smul_ovfl_constraint& to_smul_ovfl(); - smul_ovfl_constraint const& to_smul_ovfl() const; + smul_fl_constraint& to_smul_fl(); + smul_fl_constraint const& to_smul_fl() const; op_constraint& to_op(); op_constraint const& to_op() const; unsigned_vector& vars() { return m_vars; } diff --git a/src/math/polysat/smul_ovfl_constraint.cpp b/src/math/polysat/smul_ovfl_constraint.cpp index a0209c393..deb94fc60 100644 --- a/src/math/polysat/smul_ovfl_constraint.cpp +++ b/src/math/polysat/smul_ovfl_constraint.cpp @@ -15,8 +15,8 @@ Author: namespace polysat { - smul_ovfl_constraint::smul_ovfl_constraint(constraint_manager& m, pdd const& p, pdd const& q): - constraint(m, ckind_t::smul_ovfl_t), m_p(p), m_q(q) { + smul_ovfl_constraint::smul_ovfl_constraint(constraint_manager& m, pdd const& p, pdd const& q, bool is_overflow): + constraint(m, ckind_t::smul_ovfl_t), m_is_overflow(is_overflow), m_p(p), m_q(q) { simplify(); m_vars.append(m_p.free_vars()); for (auto v : m_q.free_vars()) @@ -45,27 +45,66 @@ namespace polysat { } std::ostream& smul_ovfl_constraint::display(std::ostream& out) const { - return out << "sovfl*(" << m_p << ", " << m_q << ")"; + if (m_is_overflow) + return out << "sovfl*(" << m_p << ", " << m_q << ")"; + else + return out << "sudfl*(" << m_p << ", " << m_q << ")"; } + /** + * TODO - verify the rules for small bit-widths. + * + * sovfl(p,q) => p >= 2, q >= 2 + * sovfl(p,q) => p >s 0 <=> q >s 0 + * sovfl(p,q) & p >s 0 => p*q < 0 or ovfl(p,q) + * sovfl(p,q) & p p*q < 0 or ovfl(-p,-q) + + * ~sovfl(p,q) & p >s 0 = q >s 0 => q > 0 => ~ovfl(p,q) & p*q >=s 0 + * smul_noovfl(p,q) => sign(p) != sign(q) or p'*q' < 2^{K-1} + + * sudfl(p, q) => p >= 2, q >= 2 + * sudfl(p, q) => p >s 0 xor q >s 0 + * sudfl(p, q) & p >s 0 => p*q > 0 or ovfl(p, -q) + * sudfl(p, q) & q >s 0 => p*q > 0 or ovfl(-p, q) + * + * ~sudfl(p, q) & p >s 0 & q ~ovfl(p, -q) & p*q s 0 => ~ovfl(-p, q) & p*q sign(p) != sign(q) or p'*q' < 2^{K-1} - s.add_clause(~sc, ~s.sgt(p(), 0), ~s.sgt(q(), 0), ~s.mul_ovfl(p(), q()), false); - s.add_clause(~sc, ~s.sgt(p(), 0), ~s.sgt(q(), 0), ~s.slt(p()*q(), 0), false); - s.add_clause(~sc, ~s.slt(p(), 0), ~s.slt(q(), 0), ~s.mul_ovfl(-p(), -q()), false); - s.add_clause(~sc, ~s.slt(p(), 0), ~s.slt(q(), 0), ~s.slt((-p())*(-q()), 0), false); + if (is_positive) { + s.add_clause(~sc, s.ule(2, p()), false); + s.add_clause(~sc, s.ule(2, q()), false); + s.add_clause(~sc, ~s.sgt(p(), 0), ~s.sgt(q(), 0), false); + s.add_clause(~sc, s.sgt(q(), 0), s.sgt(p(), 0), false); + s.add_clause(~sc, ~s.sgt(p(), 0), s.sgt(p()*q(), 0), s.mul_ovfl(p(), -q()), false); + s.add_clause(~sc, ~s.sgt(q(), 0), s.sgt(p()*q(), 0), s.mul_ovfl(-p(), q()), false); + } + else { + s.add_clause(sc, ~s.sgt(p(), 0), ~s.slt(q(), 0), s.mul_ovfl(p(), -q()), false); + s.add_clause(sc, ~s.sgt(p(), 0), ~s.slt(q(), 0), s.slt(p()*q(), 0), false); + s.add_clause(sc, ~s.slt(p(), 0), ~s.sgt(q(), 0), s.mul_ovfl(-p(), q()), false); + s.add_clause(sc, ~s.slt(p(), 0), ~s.sgt(q(), 0), s.slt(p()*q(), 0), false); + } } } diff --git a/src/math/polysat/smul_ovfl_constraint.h b/src/math/polysat/smul_ovfl_constraint.h index 4c07d7ac1..a2cba19f2 100644 --- a/src/math/polysat/smul_ovfl_constraint.h +++ b/src/math/polysat/smul_ovfl_constraint.h @@ -20,11 +20,12 @@ namespace polysat { class smul_ovfl_constraint final : public constraint { friend class constraint_manager; - pdd m_p; - pdd m_q; + bool m_is_overflow; + pdd m_p; + pdd m_q; void simplify(); - smul_ovfl_constraint(constraint_manager& m, pdd const& p, pdd const& q); + smul_ovfl_constraint(constraint_manager& m, pdd const& p, pdd const& q, bool is_overflow); public: ~smul_ovfl_constraint() override {} diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index e77266940..468a77b97 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -56,7 +56,7 @@ namespace polysat { friend class constraint; friend class ule_constraint; friend class mul_ovfl_constraint; - friend class smul_ovfl_constraint; + friend class smul_fl_constraint; friend class op_constraint; friend class signed_constraint; friend class clause; @@ -344,6 +344,7 @@ namespace polysat { signed_constraint mul_ovfl(pdd const& p, pdd const& q) { return m_constraints.mul_ovfl(p, q); } signed_constraint mul_ovfl(rational const& p, pdd const& q) { return mul_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); } signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); } /** Create and activate polynomial constraints. */ diff --git a/src/sat/smt/bv_polysat.cpp b/src/sat/smt/bv_polysat.cpp index 00a929da4..7d05d97ab 100644 --- a/src/sat/smt/bv_polysat.cpp +++ b/src/sat/smt/bv_polysat.cpp @@ -33,8 +33,10 @@ namespace bv { void solver::internalize_polysat(app* a) { std::function bin; + std::function binc; #define mk_binary(a, fn) bin = fn; polysat_binary(a, bin); +#define mk_binaryc(a, fn) binc = fn; polysat_binaryc(a, binc); switch (to_app(a)->get_decl_kind()) { case OP_BMUL: mk_binary(a, [&](pdd const& p, pdd const& q) { return p * q; }); break; @@ -56,9 +58,10 @@ namespace bv { case OP_UGT: polysat_le(a); break; case OP_SGT: polysat_le(a); break; - case OP_BUMUL_NO_OVFL: polysat_umul_noovfl(a); break; - case OP_BSMUL_NO_OVFL: polysat_smul_noovfl(a); break; - + case OP_BUMUL_NO_OVFL: mk_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.mul_ovfl(p, q); }); break; + case OP_BSMUL_NO_OVFL: mk_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.smul_ovfl(p, q); }); break; + case OP_BSMUL_NO_UDFL: mk_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.smul_udfl(p, q); }); break; + case OP_BUDIV_I: polysat_div_rem_i(a, true); break; case OP_BUREM_I: polysat_div_rem_i(a, false); break; @@ -75,8 +78,7 @@ namespace bv { case OP_BREDOR: // x > 0 case OP_BSDIV: case OP_BSREM: - case OP_BSMOD: - case OP_BSMUL_NO_UDFL: + case OP_BSMOD: case OP_BSDIV_I: case OP_BSREM_I: case OP_BSMOD_I: @@ -102,19 +104,10 @@ namespace bv { } } - void solver::polysat_umul_noovfl(app* e) { + void solver::polysat_binaryc(app* e, std::function& fn) { auto p = expr2pdd(e->get_arg(0)); auto q = expr2pdd(e->get_arg(1)); - auto sc = ~m_polysat.mul_ovfl(p, q); - sat::literal lit = expr2literal(e); - atom* a = mk_atom(lit.var()); - a->m_sc = sc; - } - - void solver::polysat_smul_noovfl(app* e) { - auto p = expr2pdd(e->get_arg(0)); - auto q = expr2pdd(e->get_arg(1)); - auto sc = ~m_polysat.smul_ovfl(p, q); + auto sc = ~fn(p, q); sat::literal lit = expr2literal(e); atom* a = mk_atom(lit.var()); a->m_sc = sc; diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index 39fbd6d18..345f3421a 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -280,8 +280,7 @@ namespace bv { void polysat_neg(app* a); void polysat_num(app* a); void polysat_mkbv(app* a); - void polysat_umul_noovfl(app* e); - void polysat_smul_noovfl(app* e); + void polysat_binaryc(app* e, std::function& fn); void polysat_div_rem_i(app* e, bool is_div); void polysat_div_rem(app* e, bool is_div); void polysat_bit2bool(atom* a, expr* e, unsigned idx);