mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

Fix eval_lshr

Browse source
This commit is contained in:
Jakob Rath 2022-11-17 11:47:12 +01:00
parent 2c4e3184d7
commit 097454cf37
1 changed files with 11 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -221,17 +221,22 @@ namespace polysat {
} }
} }
/** Evaluate constraint: r == p >> q */
lbool op_constraint::eval_lshr(pdd const& p, pdd const& q, pdd const& r) { lbool op_constraint::eval_lshr(pdd const& p, pdd const& q, pdd const& r) {
auto& m = p.manager(); auto& m = p.manager();
if (p.is_val() && q.is_val() && r.is_val())
return r == p * m.mk_val(rational::power_of_two(q.val().get_unsigned())) ? l_true : l_false;
if (q.is_val() && q.val() >= m.power_of_2() && r.is_val()) if (q.is_val() && q.val() >= m.power_of_2() && r.is_val())
return r.is_zero() ? l_true : l_false; return to_lbool(r.is_zero());
// other cases when we know lower if (p.is_val() && q.is_val() && r.is_val()) {
// bound of q, e.g, q = 2^k*q1 + q2, where q2 is a constant. SASSERT(q.val().is_unsigned()); // otherwise, previous condition should have been triggered
// TODO: use right-shift operation instead of division
auto divisor = rational::power_of_two(q.val().get_unsigned());
return to_lbool(r.val() == div(p.val(), divisor));
}
// TODO: other cases when we know lower bound of q,
// e.g, q = 2^k*q1 + q2, where q2 is a constant.
return l_undef; return l_undef;
} }