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

Evaluate bitwise operations on values

Browse source
This commit is contained in:
Clemens Eisenhofer 2022-11-21 09:38:53 +01:00
parent 5c3180562d
commit 133f3d0a02
1 changed files with 9 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -329,14 +329,23 @@ namespace polysat {
}
pdd constraint_manager::lshr(pdd const& p, pdd const& q) {
if (p.is_val() && q.is_val() && q.val().is_unsigned()) {
return p.manager().mk_val(div(p.val(), rational::power_of_two(q.val().get_unsigned())));
}
return mk_op_term(op_constraint::code::lshr_op, p, q);
}
pdd constraint_manager::shl(pdd const& p, pdd const& q) {
if (p.is_val() && q.is_val() && q.val().is_unsigned()) {
return p.manager().mk_val(p.val() * rational::power_of_two(q.val().get_unsigned()));
}
return mk_op_term(op_constraint::code::shl_op, p, q);
}
pdd constraint_manager::band(pdd const& p, pdd const& q) {
if (p.is_val() && q.is_val()) {
return p.manager().mk_val(bitwise_and(p.val(), q.val()));
}
return mk_op_term(op_constraint::code::and_op, p, q);
}