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

have propagate return whether it did something

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-01-11 11:45:05 -08:00
parent 4a2217a3e8
commit a2df3cb828
7 changed files with 45 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/polysat/constraints.h
View file

@ -49,7 +49,7 @@ namespace polysat {
virtual lbool weak_eval(assignment const& a) const = 0;
virtual lbool strong_eval(assignment const& a) const = 0;
virtual void activate(core& c, bool sign, dependency const& d) = 0;
virtual void propagate(core& c, lbool value, dependency const& d) = 0;
virtual bool propagate(core& c, lbool value, dependency const& d) = 0;
virtual bool is_linear() const { return false; }
};
@ -75,7 +75,7 @@ namespace polysat {
unsigned num_watch() const { return m_constraint->num_watch(); }
void set_num_watch(unsigned n) { m_constraint->set_num_watch(n); }
void activate(core& c, dependency const& d) { m_constraint->activate(c, m_sign, d); }
void propagate(core& c, lbool value, dependency const& d) { m_constraint->propagate(c, value, d); }
bool propagate(core& c, lbool value, dependency const& d) { return m_constraint->propagate(c, value, d); }
bool is_always_true() const { return eval() == l_true; }
bool is_always_false() const { return eval() == l_false; }
bool is_linear() const { return m_constraint->is_linear(); }

58
src/sat/smt/polysat/op_constraint.cpp
View file

@ -264,36 +264,31 @@ namespace polysat {
}
}
void op_constraint::propagate(core& c, lbool value, dependency const& dep) {
bool op_constraint::propagate(core& c, lbool value, dependency const& dep) {
SASSERT(value == l_true);
switch (m_op) {
case code::lshr_op:
propagate_lshr(c);
break;
return propagate_lshr(c);
case code::ashr_op:
propagate_ashr(c);
break;
return propagate_ashr(c);
case code::shl_op:
propagate_shl(c);
break;
return propagate_shl(c);
case code::and_op:
propagate_and(c);
break;
return propagate_and(c);
case code::or_op:
propagate_or(c);
break;
return propagate_or(c);
case code::inv_op:
propagate_inv(c);
break;
return propagate_inv(c);
default:
verbose_stream() << "not implemented yet: " << *this << "\n";
NOT_IMPLEMENTED_YET();
break;
}
return false;
}
void op_constraint::propagate_inv(core& s) {
bool op_constraint::propagate_inv(core& s) {
return false;
}
bool op_constraint::propagate(core& c, signed_constraint const& sc) {
@ -352,11 +347,10 @@ namespace polysat {
bool c1 = add_conflict(c, "q = k & 0 < k < N -> 2^k (p >>l q) <= p", { ~C.eq(q, k), C.ule(r * twoK, p)});
bool c2 = add_conflict(c, "q = k & 0 < k < N -> p <= 2^k*(p >>l q) + 2^k - 1", { ~C.eq(q, k), C.ule(p, r * twoK + twoK - 1) });
bool c3 = add_conflict(c, "q = k & 0 < k < N -> (p >>l q) < 2^{N-k}", { ~C.eq(q, k), C.ult(r, twoNK) });
VERIFY(c1 || c2 || c3);
return true;
return c1 || c2 || c3;
}
void op_constraint::propagate_ashr(core& c) {
bool op_constraint::propagate_ashr(core& c) {
//
// Suppose q = k, p >= 0:
// p = ab, where b has length k, a has length N - k
@ -400,8 +394,9 @@ namespace polysat {
bool c2 = add_conflict(c, "q = k & 0 < k < N -> p <= 2^k*r + 2^k - 1", { ~C.eq(q, k), C.ule(p, r * twoK + twoK - 1) });
bool c3 = add_conflict(c, "p < 0 & q = k -> r >= 2^N - 2^{N-k-1}", { ~C.eq(q, k), ~C.slt(p, 0), C.uge(r, twoN - twoNk1) });
bool c4 = add_conflict(c, "p >= 0 & q = k -> r < 2^{N-k-1}", { ~C.eq(q, k), C.slt(p, 0), C.ult(r, twoNk1)});
VERIFY(c1 || c2 || c3 || c4);
return c1 || c2 || c3 || c4;
}
return false;
}
@ -414,7 +409,7 @@ namespace polysat {
* q >= k -> r = 0 \/ r >= 2^k
* q >= k -> r[i] = 0 for i < k
*/
void op_constraint::propagate_shl(core& c) {
bool op_constraint::propagate_shl(core& c) {
auto& m = p.manager();
auto const pv = c.subst(p);
auto const qv = c.subst(q);
@ -423,16 +418,16 @@ namespace polysat {
auto& C = c.cs();
if (!qv.is_val())
return;
return false;
if (qv.is_zero() || qv.val() >= N)
return;
return false;
auto k = qv.val().get_unsigned();
auto twoK = rational::power_of_two(k);
add_conflict(c, "p << k = 2^k*p", { ~C.eq(q, k), C.eq(r, p * twoK) });
return add_conflict(c, "p << k = 2^k*p", { ~C.eq(q, k), C.eq(r, p * twoK) });
}
/**
@ -448,7 +443,7 @@ namespace polysat {
* p = 2^k - 1 && r = 0 && q != 0 => q >= 2^k
* q = 2^k - 1 && r = 0 && p != 0 => p >= 2^k
*/
void op_constraint::propagate_and(core& c) {
bool op_constraint::propagate_and(core& c) {
auto& m = p.manager();
auto pv = c.subst(p);
auto qv = c.subst(q);
@ -456,13 +451,16 @@ namespace polysat {
auto& C = c.cs();
if (!pv.is_val() || !qv.is_val() || !rv.is_val())
return;
return false;
if (eval_and(pv, qv, rv) == l_true)
return false;
if (propagate_mask(c, p, q, r, pv.val(), qv.val(), rv.val()))
return;
return true;
if (propagate_mask(c, q, p, r, qv.val(), pv.val(), rv.val()))
return;
return true;
unsigned const N = m.power_of_2();
for (unsigned i = 0; i < N; ++i) {
@ -479,8 +477,9 @@ namespace polysat {
add_conflict(c, "p&q[i] = p[i]&q[i]", { C.bit(q, i), ~C.bit(r, i) });
else
UNREACHABLE();
return;
return true;
}
return false;
}
bool op_constraint::propagate_or(core& c) {
@ -493,6 +492,9 @@ namespace polysat {
if (!pv.is_val() || !qv.is_val() || !rv.is_val())
return false;
if (eval_or(pv, qv, rv) == l_true)
return false;
if (pv.is_max() && pv != rv)
return add_conflict(c, "p = -1 => p & q = p", { ~C.eq(p, m.max_value()), C.eq(p, r)});

10
src/sat/smt/polysat/op_constraint.h
View file

@ -61,11 +61,11 @@ namespace polysat {
static lbool eval_or(pdd const& p, pdd const& q, pdd const& r);
bool propagate_lshr(core& c);
void propagate_ashr(core& c);
void propagate_shl(core& c);
void propagate_and(core& c);
bool propagate_ashr(core& c);
bool propagate_shl(core& c);
bool propagate_and(core& c);
bool propagate_or(core& c);
void propagate_inv(core& c);
bool propagate_inv(core& c);
bool propagate_mask(core& c, pdd const& p, pdd const& q, pdd const& r, rational const& pv, rational const& qv, rational const& rv);
bool propagate(core& c, signed_constraint const& sc);
@ -84,7 +84,7 @@ namespace polysat {
bool is_always_true() const { return false; }
bool is_always_false() const { return false; }
void activate(core& c, bool sign, dependency const& dep) override;
void propagate(core& c, lbool value, dependency const& dep) override;
bool propagate(core& c, lbool value, dependency const& dep) override;
};
}

2
src/sat/smt/polysat/saturation.cpp
View file

@ -243,7 +243,7 @@ namespace polysat {
void saturation::try_op(pvar v, signed_constraint& sc, dependency const& d) {
SASSERT(sc.is_op());
sc.propagate(c, l_true, d);
VERIFY(sc.propagate(c, l_true, d));
}
// possible algebraic rule:

2
src/sat/smt/polysat/ule_constraint.h
View file

@ -42,7 +42,7 @@ namespace polysat {
lbool strong_eval(assignment const& a) const override;
bool is_linear() const override { return lhs().is_linear_or_value() && rhs().is_linear_or_value(); }
void activate(core& c, bool sign, dependency const& dep);
void propagate(core& c, lbool value, dependency const& dep) {}
bool propagate(core& c, lbool value, dependency const& dep) { return false; }
bool is_eq() const { return m_rhs.is_zero(); }
unsigned power_of_2() const { return m_lhs.power_of_2(); }

9
src/sat/smt/polysat/umul_ovfl_constraint.cpp
View file

@ -80,16 +80,17 @@ namespace polysat {
}
void umul_ovfl_constraint::propagate(core& c, lbool value, dependency const& dep) {
bool umul_ovfl_constraint::propagate(core& c, lbool value, dependency const& dep) {
if (value == l_undef)
return;
return false;
auto& C = c.cs();
auto p1 = c.subst(p());
auto q1 = c.subst(q());
if (narrow_bound(c, value == l_true, p(), q(), p1, q1, dep))
return;
return true;
if (narrow_bound(c, value == l_true, q(), p(), q1, p1, dep))
return;
return true;
return false;
}
/**

2
src/sat/smt/polysat/umul_ovfl_constraint.h
View file

@ -38,7 +38,7 @@ namespace polysat {
lbool weak_eval(assignment const& a) const override;
lbool strong_eval(assignment const& a) const override;
void activate(core& c, bool sign, dependency const& dep) override;
void propagate(core& c, lbool value, dependency const& dep) override;
bool propagate(core& c, lbool value, dependency const& dep) override;
bool is_linear() const override { return p().is_linear_or_value() && q().is_linear_or_value(); }
};