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

remove unused propagation in umul_overflow code. Rename propagate to saturate to reflect where it gets used

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-02-01 09:57:28 -08:00
parent 111dee9143
commit 6e72182194
9 changed files with 25 additions and 121 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 bool propagate(core& c, lbool value, dependency const& d) = 0;
virtual bool saturate(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); }
bool propagate(core& c, lbool value, dependency const& d) { return m_constraint->propagate(c, value, d); }
bool saturate(core& c, lbool value, dependency const& d) { return m_constraint->saturate(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(); }

15
src/sat/smt/polysat/core.cpp
View file

@ -487,21 +487,6 @@ namespace polysat {
return d;
}
void core::propagate(constraint_id id, signed_constraint& sc, lbool value, dependency const& d) {
lbool eval_value = weak_eval(sc);
if (eval_value == l_undef)
sc.propagate(*this, value, d);
else if (value == l_undef)
s.propagate(d, eval_value != l_true, explain_weak_eval(sc), "constraint-propagate");
else if (value != eval_value) {
m_unsat_core = explain_weak_eval(sc);
m_unsat_core.push_back(m_constraint_index[id.id].d);
verbose_stream() << "infeasible propagation " << m_unsat_core << "\n";
s.set_conflict(m_unsat_core, "polysat-constraint-core");
decay_activity();
}
}
void core::get_bitvector_suffixes(pvar v, offset_slices& out) {
s.get_bitvector_suffixes(v, out);
}

1
src/sat/smt/polysat/core.h
View file

@ -98,7 +98,6 @@ namespace polysat {
void propagate_eval(constraint_id idx);
void propagate_assignment(pvar v, rational const& value, dependency dep);
void propagate_activation(constraint_id idx, signed_constraint& sc, dependency dep);
void propagate(constraint_id id, signed_constraint& sc, lbool value, dependency const& d);
dependency_vector explain_weak_eval(unsigned_vector const& vars);
void add_watch(unsigned idx, unsigned var);

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

@ -264,21 +264,21 @@ namespace polysat {
}
}
bool op_constraint::propagate(core& c, lbool value, dependency const& dep) {
bool op_constraint::saturate(core& c, lbool value, dependency const& dep) {
SASSERT(value == l_true);
switch (m_op) {
case code::lshr_op:
return propagate_lshr(c);
return saturate_lshr(c);
case code::ashr_op:
return propagate_ashr(c);
return saturate_ashr(c);
case code::shl_op:
return propagate_shl(c);
return saturate_shl(c);
case code::and_op:
return propagate_and(c);
return saturate_and(c);
case code::or_op:
return propagate_or(c);
return saturate_or(c);
case code::inv_op:
return propagate_inv(c);
return saturate_inv(c);
default:
verbose_stream() << "not implemented yet: " << *this << "\n";
NOT_IMPLEMENTED_YET();
@ -287,7 +287,7 @@ namespace polysat {
return false;
}
bool op_constraint::propagate_inv(core& s) {
bool op_constraint::saturate_inv(core& s) {
return false;
}
@ -323,7 +323,7 @@ namespace polysat {
* when q is a constant, several axioms can be enforced at activation time.
*
*/
bool op_constraint::propagate_lshr(core& c) {
bool op_constraint::saturate_lshr(core& c) {
auto& m = p.manager();
auto const pv = c.subst(p);
auto const qv = c.subst(q);
@ -350,7 +350,7 @@ namespace polysat {
return c1 || c2 || c3;
}
bool op_constraint::propagate_ashr(core& c) {
bool op_constraint::saturate_ashr(core& c) {
//
// Suppose q = k, p >= 0:
// p = ab, where b has length k, a has length N - k
@ -409,7 +409,7 @@ namespace polysat {
* q >= k -> r = 0 \/ r >= 2^k
* q >= k -> r[i] = 0 for i < k
*/
bool op_constraint::propagate_shl(core& c) {
bool op_constraint::saturate_shl(core& c) {
auto& m = p.manager();
auto const pv = c.subst(p);
auto const qv = c.subst(q);
@ -443,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
*/
bool op_constraint::propagate_and(core& c) {
bool op_constraint::saturate_and(core& c) {
auto& m = p.manager();
auto pv = c.subst(p);
auto qv = c.subst(q);
@ -482,7 +482,7 @@ namespace polysat {
return false;
}
bool op_constraint::propagate_or(core& c) {
bool op_constraint::saturate_or(core& c) {
auto& m = p.manager();
auto pv = c.subst(p);
auto qv = c.subst(q);

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

@ -60,12 +60,12 @@ namespace polysat {
static lbool eval_inv(pdd const& p, pdd const& r);
static lbool eval_or(pdd const& p, pdd const& q, pdd const& r);
bool propagate_lshr(core& c);
bool propagate_ashr(core& c);
bool propagate_shl(core& c);
bool propagate_and(core& c);
bool propagate_or(core& c);
bool propagate_inv(core& c);
bool saturate_lshr(core& c);
bool saturate_ashr(core& c);
bool saturate_shl(core& c);
bool saturate_and(core& c);
bool saturate_or(core& c);
bool saturate_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;
bool propagate(core& c, lbool value, dependency const& dep) override;
bool saturate(core& c, lbool value, dependency const& dep) override;
};
}

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

@ -342,7 +342,7 @@ namespace polysat {
void saturation::try_op(pvar v, signed_constraint& sc, dependency const& d) {
SASSERT(sc.is_op());
VERIFY(sc.propagate(c, l_true, d));
VERIFY(sc.saturate(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) override;
bool propagate(core& c, lbool value, dependency const& dep) override { return false; }
bool saturate(core& c, lbool value, dependency const& dep) override { return false; }
bool is_eq() const { return m_rhs.is_zero(); }
unsigned power_of_2() const { return m_lhs.power_of_2(); }

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

@ -80,83 +80,5 @@ namespace polysat {
}
bool umul_ovfl_constraint::propagate(core& c, lbool value, dependency const& dep) {
if (value == l_undef)
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 true;
if (narrow_bound(c, value == l_true, q(), p(), q1, p1, dep))
return true;
return false;
}
/**
* if p constant, q, propagate inequality
*/
bool umul_ovfl_constraint::narrow_bound(core& c, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q, dependency const& d) {
LOG("p: " << p0 << " := " << p);
LOG("q: " << q0 << " := " << q);
if (!p.is_val())
return false;
SASSERT(!p.is_zero() && !p.is_one()); // evaluation should catch this case
rational const& M = p.manager().two_to_N();
auto& C = c.cs();
// q_bound
// = min q . Ovfl(p_val, q)
// = min q . p_val * q >= M
// = min q . q >= M / p_val
// = ceil(M / p_val)
rational const q_bound = ceil(M / p.val());
SASSERT(2 <= q_bound && q_bound <= M / 2);
SASSERT(p.val() * q_bound >= M);
SASSERT(p.val() * (q_bound - 1) < M);
// LOG("q_bound: " << q.manager().mk_val(q_bound));
// We need the following properties for the bounds:
//
// p_bound * (q_bound - 1) < M
// p_bound * q_bound >= M
//
// With these properties we get:
//
// p <= p_bound & q < q_bound ==> ~Ovfl(p, q)
// p >= p_bound & q >= q_bound ==> Ovfl(p, q)
//
// Written as lemmas:
//
// Ovfl(p, q) & p <= p_bound ==> q >= q_bound
// ~Ovfl(p, q) & p >= p_bound ==> q < q_bound
//
if (is_positive) {
// Find largest bound for p such that q_bound is still correct.
// p_bound = max p . (q_bound - 1)*p < M
// = max p . p < M / (q_bound - 1)
// = ceil(M / (q_bound - 1)) - 1
rational const p_bound = ceil(M / (q_bound - 1)) - 1;
SASSERT(p.val() <= p_bound);
SASSERT(p_bound * q_bound >= M);
SASSERT(p_bound * (q_bound - 1) < M);
// LOG("p_bound: " << p.manager().mk_val(p_bound));
c.add_axiom("~Ovfl(p, q) & p <= p_bound -> q < q_bound", { d, ~C.ule(p0, p_bound), C.ule(q_bound, q0) }, true);
}
else {
// Find lowest bound for p such that q_bound is still correct.
// p_bound = min p . Ovfl(p, q_bound) = ceil(M / q_bound)
rational const p_bound = ceil(M / q_bound);
SASSERT(p_bound <= p.val());
SASSERT(p_bound * q_bound >= M);
SASSERT(p_bound * (q_bound - 1) < M);
// LOG("p_bound: " << p.manager().mk_val(p_bound));
c.add_axiom("~Ovfl(p, q) & p >= p_bound -> q < q_bound", { d, ~C.ule(p_bound, p0), C.ult(q0, q_bound) }, true);
}
return true;
}
}

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

@ -25,8 +25,6 @@ namespace polysat {
static bool is_always_false(bool is_positive, pdd const& p, pdd const& q) { return is_always_true(!is_positive, p, q); }
static lbool eval(pdd const& p, pdd const& q);
bool narrow_bound(core& c, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q, dependency const& d);
public:
umul_ovfl_constraint(pdd const& p, pdd const& q);
~umul_ovfl_constraint() override {}
@ -38,7 +36,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;
bool propagate(core& c, lbool value, dependency const& dep) override;
bool saturate(core& c, lbool value, dependency const& dep) override { return false; }
bool is_linear() const override { return p().is_linear_or_value() && q().is_linear_or_value(); }
};