mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 07:13:41 +00:00
Code Activity

Update op_constraint simplifications

Browse source
This commit is contained in:
Jakob Rath 2023-01-12 13:31:16 +01:00
parent 0a2c69332d
commit 057e115bbc
1 changed files with 34 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -453,12 +453,13 @@ namespace polysat {
return -p - 1; return -p - 1;
} }
static unsigned min_coefficient_power_of_2(const pdd& p) { static unsigned common_coefficient_power_of_2(const pdd& p) {
#if 0
if (p.is_zero()) if (p.is_zero())
return 0; // TODO: Or something different? return 0; // TODO: Or something different? ==> if p == 0, we can divide by any 2^k, so just return UINT_MAX. (but the case p.is_val() is handled separately, anyway.)
#endif
unsigned min_power = UINT32_MAX; unsigned min_power = UINT32_MAX;
for (auto& m : p) for (auto& m : p) // TODO: add coefficient iterator? we don't need the variable vectors here.
min_power = std::min(min_power, m.coeff.trailing_zeros()); min_power = std::min(min_power, m.coeff.trailing_zeros());
return min_power; return min_power;
} }
@ -480,32 +481,50 @@ namespace polysat {
} }
pdd constraint_manager::lshr(pdd const& p, pdd const& q) { pdd constraint_manager::lshr(pdd const& p, pdd const& q) {
if (p.is_zero())
return p;
if (q.is_zero())
return p;
if (q.is_val()) { if (q.is_val()) {
if (!q.val().is_unsigned()) auto& m = p.manager();
return p.manager().zero(); // TODO: The number is huge. We will for sure shift out all bits unsigned N = m.power_of_2();
if (q.val() >= N)
return m.zero();
SASSERT(q.val().is_unsigned());
if (p.is_val()) if (p.is_val())
return p.manager().mk_val(div(p.val(), rational::power_of_two(q.val().get_unsigned()))); return m.mk_val(machine_div2k(p.val(), q.val().get_unsigned()));
// 2^i * p' >> q ==> 2^(i-q) * p' if i >= q
unsigned common = min_coefficient_power_of_2(p); unsigned common = common_coefficient_power_of_2(p);
pdd div = p.manager().zero(); if (common >= q.val())
for (auto& m : p) return p.div(rational::power_of_two(common));
div += machine_div(m.coeff, rational::power_of_two(common));
return div;
} }
return mk_op_term(op_constraint::code::lshr_op, p, q); return mk_op_term(op_constraint::code::lshr_op, p, q);
} }
pdd constraint_manager::shl(pdd const& p, pdd const& q) { pdd constraint_manager::shl(pdd const& p, pdd const& q) {
if (p.is_zero())
return p;
if (q.is_zero())
return p;
if (q.is_val()) { if (q.is_val()) {
if (!q.val().is_unsigned()) unsigned N = p.power_of_2();
if (q.val() >= N)
return p.manager().zero(); return p.manager().zero();
SASSERT(q.val().is_unsigned());
return p * rational::power_of_two(q.val().get_unsigned()); return p * rational::power_of_two(q.val().get_unsigned());
} }
return mk_op_term(op_constraint::code::shl_op, p, q); return mk_op_term(op_constraint::code::shl_op, p, q);
} }
pdd constraint_manager::band(pdd const& p, pdd const& q) { pdd constraint_manager::band(pdd const& p, pdd const& q) {
if (p.is_zero())
return p;
if (q.is_zero())
return q;
if (p.is_max())
return q;
if (q.is_max())
return p;
if (p.is_val() && q.is_val()) if (p.is_val() && q.is_val())
return p.manager().mk_val(bitwise_and(p.val(), q.val())); return p.manager().mk_val(bitwise_and(p.val(), q.val()));
return mk_op_term(op_constraint::code::and_op, p, q); return mk_op_term(op_constraint::code::and_op, p, q);