mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

add smul over and underflow predicate

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-02-20 11:39:45 +02:00
parent dc3b921712
commit 1faccffd0d
8 changed files with 88 additions and 50 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/CMakeLists.txt
View file

@ -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

16
src/math/polysat/constraint.cpp
View file

@ -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<mul_ovfl_constraint const*>(this);
}
smul_ovfl_constraint& constraint::to_smul_ovfl() {
return *dynamic_cast<smul_ovfl_constraint*>(this);
smul_fl_constraint& constraint::to_smul_fl() {
return *dynamic_cast<smul_fl_constraint*>(this);
}
smul_ovfl_constraint const& constraint::to_smul_ovfl() const {
return *dynamic_cast<smul_ovfl_constraint const*>(this);
smul_fl_constraint const& constraint::to_smul_fl() const {
return *dynamic_cast<smul_fl_constraint const*>(this);
}
op_constraint& constraint::to_op() {

13
src/math/polysat/constraint.h
View file

@ -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; }

69
src/math/polysat/smul_ovfl_constraint.cpp
View file

@ -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 <s 0 => 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 <s 0 => ~ovfl(p, -q) & p*q <s 0
* ~sudfl(p, q) & p <s 0 & q >s 0 => ~ovfl(-p, q) & p*q <s 0
*/
void smul_ovfl_constraint::narrow(solver& s, bool is_positive, bool first) {
if (!first)
return;
signed_constraint sc(this, is_positive);
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.slt(p()*q(), 0), s.mul_ovfl(p(), q()), false);
s.add_clause(~sc, s.sgt(p(), 0), s.slt(p()*q(), 0), s.mul_ovfl(-p(), -q()), false);
if (m_is_overflow) {
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.slt(p()*q(), 0), s.mul_ovfl(p(), q()), false);
s.add_clause(~sc, s.sgt(p(), 0), s.slt(p()*q(), 0), s.mul_ovfl(-p(), -q()), false);
}
else {
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);
}
}
else {
// smul_noovfl(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);
}
}
}

7
src/math/polysat/smul_ovfl_constraint.h
View file

@ -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 {}

3
src/math/polysat/solver.h
View file

@ -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. */

25
src/sat/smt/bv_polysat.cpp
View file

@ -33,8 +33,10 @@ namespace bv {
void solver::internalize_polysat(app* a) {
std::function<polysat::pdd(polysat::pdd, polysat::pdd)> bin;
std::function<polysat::signed_constraint(polysat::pdd, polysat::pdd)> 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<false, false, true>(a); break;
case OP_SGT: polysat_le<true, false, true>(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<polysat::signed_constraint(polysat::pdd, polysat::pdd)>& 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;

3
src/sat/smt/bv_solver.h
View file

@ -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<polysat::signed_constraint(polysat::pdd, polysat::pdd)>& 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);