mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

Draft: Made division/remainder to op_constraints (not yet used - old code still called)

Browse source
This commit is contained in:
Clemens Eisenhofer 2023-02-09 23:36:15 +01:00
parent e31eb9a6b1
commit 6b48b25beb
6 changed files with 219 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

45
src/math/polysat/constraint_manager.cpp
View file

@ -528,4 +528,49 @@ namespace polysat {
return p.manager().mk_val(p.val().pseudo_inverse(p.power_of_2()));
return mk_op_term(op_constraint::code::inv_op, p, p.manager().zero());
}
pdd constraint_manager::udiv(pdd const& p, pdd const& q) {
return div_rem_op_constraint(p, q).first;
}
pdd constraint_manager::urem(pdd const& p, pdd const& q) {
return div_rem_op_constraint(p, q).second;
}
/** unsigned quotient/remainder */
std::pair<pdd, pdd> constraint_manager::div_rem_op_constraint(pdd const& a, pdd const& b) {
auto& m = a.manager();
unsigned sz = m.power_of_2();
if (b.is_zero()) {
// By SMT-LIB specification, b = 0 ==> q = -1, r = a.
return {m.mk_val(m.max_value()), a};
}
if (b.is_one()) {
return {a, m.zero()};
}
if (a.is_val() && b.is_val()) {
rational const av = a.val();
rational const bv = b.val();
SASSERT(!bv.is_zero());
rational rv;
rational qv = machine_div_rem(av, bv, rv);
pdd q = m.mk_val(qv);
pdd r = m.mk_val(rv);
SASSERT_EQ(a, b * q + r);
SASSERT(b.val()*q.val() + r.val() <= m.max_value());
SASSERT(r.val() <= (b*q+r).val());
SASSERT(r.val() < b.val());
return {std::move(q), std::move(r)};
}
pdd quot = mk_op_term(op_constraint::code::udiv_op, a, b);
pdd rem = mk_op_term(op_constraint::code::urem_op, a, b);
op_constraint* op1 = (op_constraint*)mk_op_constraint(op_constraint::code::udiv_op, a, b, quot).get();
op_constraint* op2 = (op_constraint*)mk_op_constraint(op_constraint::code::urem_op, a, b, quot).get();
op1->m_linked = op2;
op2->m_linked = op1;
return {std::move(quot), std::move(rem)};
}
}

5
src/math/polysat/constraint_manager.h
View file

@ -87,6 +87,8 @@ namespace polysat {
signed_constraint mk_op_constraint(op_constraint::code op, pdd const& p, pdd const& q, pdd const& r);
pdd mk_op_term(op_constraint::code op, pdd const& p, pdd const& q);
std::pair<pdd, pdd> div_rem_op_constraint(const pdd& p, const pdd& q);
public:
constraint_manager(solver& s);
~constraint_manager();
@ -131,6 +133,9 @@ namespace polysat {
pdd bnand(pdd const& p, pdd const& q);
pdd bnor(pdd const& p, pdd const& q);
pdd pseudo_inv(pdd const& p);
pdd udiv(pdd const& a, pdd const& b);
pdd urem(pdd const& a, pdd const& b);
constraint* const* begin() const { return m_constraints.data(); }
constraint* const* end() const { return m_constraints.data() + m_constraints.size(); }

150
src/math/polysat/op_constraint.cpp
View file

@ -65,6 +65,10 @@ namespace polysat {
return eval_and(p, q, r);
case code::inv_op:
return eval_inv(p, r);
case code::udiv_op:
return eval_udiv(p, q, r);
case code::urem_op:
return eval_urem(p, q, r);
default:
return l_undef;
}
@ -90,6 +94,10 @@ namespace polysat {
return out << "&";
case op_constraint::code::inv_op:
return out << "inv";
case op_constraint::code::udiv_op:
return out << "/";
case op_constraint::code::urem_op:
return out << "%";
default:
UNREACHABLE();
return out;
@ -142,6 +150,10 @@ namespace polysat {
return propagate_bits_shl(s, is_positive);
case code::and_op:
return propagate_bits_and(s, is_positive);
case code::inv_op:
case code::udiv_op:
case code::urem_op:
return false;
default:
NOT_IMPLEMENTED_YET();
return false;
@ -180,15 +192,12 @@ namespace polysat {
void op_constraint::activate(solver& s) {
switch (m_op) {
case code::lshr_op:
break;
case code::shl_op:
break;
case code::and_op:
// handle masking of high order bits
activate_and(s);
break;
case code::inv_op:
case code::udiv_op: // division & remainder axioms (as they always occur as pairs; we do this only for divisions)
activate_udiv(s);
break;
default:
break;
@ -699,6 +708,131 @@ namespace polysat {
return to_lbool(p.val().pseudo_inverse(p.power_of_2()) == r.val());
}
void op_constraint::activate_udiv(solver& s) {
// signed_constraint const udivc(this, true); Do we really need this premiss? We anyway assert these constraints as unit clauses
pdd const& quot = r();
pdd const& rem = m_linked->r();
// 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
// b ≠ 0 ==> r < b
// b = 0 ==> q = -1
// TODO: when a,b become evaluable, can we actually propagate q,r? doesn't seem like it.
// Maybe we need something like an op_constraint for better propagation.
s.add_clause(s.eq(q() * quot + rem - p()), false);
s.add_clause(~s.umul_ovfl(q(), quot), false);
// r <= b*q+r
// { apply equivalence: p <= q <=> q-p <= -p-1 }
// b*q <= -r-1
s.add_clause(s.ule(q() * quot, -rem - 1), false);
auto c_eq = s.eq(q());
s.add_clause(c_eq, s.ult(rem, q()), false);
s.add_clause(~c_eq, s.eq(quot + 1), false);
}
/**
* Produce lemmas for constraint: r == p / q
* q = 0 ==> r = max_value
* p = 0 ==> r = 0 || r = max_value
* q = 1 ==> r = p
*/
clause_ref op_constraint::lemma_udiv(solver& s, assignment const& a) {
auto& m = p().manager();
auto pv = a.apply_to(p());
auto qv = a.apply_to(q());
auto rv = a.apply_to(r());
if (eval_udiv(pv, qv, rv) == l_true)
return {};
signed_constraint const udivc(this, true);
if (qv.is_zero() && !rv.is_val())
return s.mk_clause(~udivc, ~s.eq(q()), s.eq(r(), r().manager().max_value()), true);
if (pv.is_zero() && !rv.is_val())
return s.mk_clause(~udivc, ~s.eq(p()), s.eq(r()), s.eq(r(), r().manager().max_value()), true);
if (qv.is_one())
return s.mk_clause(~udivc, ~s.eq(q(), 1), s.eq(r(), p()), true);
if (pv.is_val() && qv.is_val() && !rv.is_val()) {
SASSERT(!qv.is_zero());
// TODO: We could actually propagate an interval. Instead of p = 9 & q = 4 => r = 2 we could do p >= 8 && p < 12 && q = 4 => r = 2
return s.mk_clause(~udivc, ~s.eq(p(), pv.val()), ~s.eq(q(), qv.val()), s.eq(r(), div(pv.val(), qv.val())), true);
}
return {};
}
/** Evaluate constraint: r == p / q */
lbool op_constraint::eval_udiv(pdd const& p, pdd const& q, pdd const& r) {
if (q.is_zero() && r.is_val()) {
return r.val() == r.manager().max_value() ? l_true : l_false;
}
if (q.is_one()) {
if (r == p)
return l_true;
}
if (!p.is_val() || !q.is_val() || !r.is_val())
return l_undef;
return r.val() == div(p.val(), q.val()) ? l_true : l_false;
}
/**
* Produce lemmas for constraint: r == p % q
* p = 0 ==> r = 0
* q = 1 ==> r = 0
* q = 0 ==> r = p
*/
clause_ref op_constraint::lemma_urem(solver& s, assignment const& a) {
auto& m = p().manager();
auto pv = a.apply_to(p());
auto qv = a.apply_to(q());
auto rv = a.apply_to(r());
if (eval_urem(pv, qv, rv) == l_true)
return {};
signed_constraint const urem(this, true);
if (pv.is_zero() && !rv.is_val())
return s.mk_clause(~urem, ~s.eq(p()), s.eq(r()), true);
if (qv.is_one() && !rv.is_val())
return s.mk_clause(~urem, ~s.eq(q(), 1), s.eq(r()), true);
if (qv.is_zero())
return s.mk_clause(~urem, ~s.eq(q()), s.eq(r(), p()), true);
if (pv.is_val() && qv.is_val() && !rv.is_val()) {
SASSERT(!qv.is_zero());
return s.mk_clause(~urem, ~s.eq(p(), pv.val()), ~s.eq(q(), qv.val()), s.eq(r(), mod(pv.val(), qv.val())), true);
}
return {};
}
/** Evaluate constraint: r == p % q */
lbool op_constraint::eval_urem(pdd const& p, pdd const& q, pdd const& r) {
if (q.is_one() && r.is_val()) {
return r.val().is_zero() ? l_true : l_false;
}
if (q.is_zero()) {
if (r == p)
return l_true;
}
if (!p.is_val() || !q.is_val() || !r.is_val())
return l_undef;
return r.val() == mod(p.val(), q.val()) ? l_true : l_false; // mod == rem as we know hat q > 0
}
void op_constraint::add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const {
pdd pv = s.subst(p());
@ -723,6 +857,12 @@ namespace polysat {
case code::inv_op:
us.add_inv(pv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, dep);
break;
case code::udiv_op:
us.add_udiv(pv.get_univariate_coefficients(), qv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, dep);
break;
case code::urem_op:
us.add_urem(pv.get_univariate_coefficients(), qv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, dep);
break;
default:
NOT_IMPLEMENTED_YET();
break;

15
src/math/polysat/op_constraint.h
View file

@ -38,7 +38,11 @@ namespace polysat {
/// r is the smallest multiplicative pseudo-inverse of p;
/// by definition we set r == 0 when p == 0.
/// Note that in general, there are 2^parity(p) many pseudo-inverses of p.
inv_op
inv_op,
// r is the quotient of dividing p by q
udiv_op,
// r is the remainder of dividing p by q
urem_op,
};
protected:
friend class constraint_manager;
@ -47,6 +51,8 @@ namespace polysat {
pdd m_p; // operand1
pdd m_q; // operand2
pdd m_r; // result
op_constraint* m_linked; // for linking remainder/quotient
op_constraint(code c, pdd const& p, pdd const& q, pdd const& r);
lbool eval(pdd const& p, pdd const& q, pdd const& r) const;
@ -66,12 +72,19 @@ namespace polysat {
clause_ref lemma_inv(solver& s, assignment const& a);
static lbool eval_inv(pdd const& p, pdd const& r);
clause_ref lemma_udiv(solver& s, assignment const& a);
static lbool eval_udiv(pdd const& p, pdd const& q, pdd const& r);
clause_ref lemma_urem(solver& s, assignment const& a);
static lbool eval_urem(pdd const& p, pdd const& q, pdd const& r);
std::ostream& display(std::ostream& out, char const* eq) const;
void activate(solver& s);
void activate_and(solver& s);
void activate_udiv(solver& s);
public:
~op_constraint() override {}

8
src/math/polysat/univariate/univariate_solver.cpp
View file

@ -255,6 +255,14 @@ namespace polysat {
add(bv->mk_ule(v_inv, v_inv_max), false, dep);
}
void add_udiv(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) override {
add(m.mk_eq(bv->mk_bv_udiv(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep);
}
void add_urem(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) override {
add(m.mk_eq(bv->mk_bv_urem(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep);
}
void add_ule_const(rational const& val, bool sign, dep_t dep) override {
if (val == 0)
add(m.mk_eq(x, mk_poly(val)), sign, dep);

2
src/math/polysat/univariate/univariate_solver.h
View file

@ -105,6 +105,8 @@ namespace polysat {
virtual void add_xor(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) = 0;
virtual void add_not(univariate const& in, univariate const& out, bool sign, dep_t dep) = 0;
virtual void add_inv(univariate const& in, univariate const& out, bool sign, dep_t dep) = 0;
virtual void add_udiv(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) = 0;
virtual void add_urem(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) = 0;
/// Add x <= val or x > val, depending on sign
virtual void add_ule_const(rational const& val, bool sign, dep_t dep) = 0;