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

propagate values in euf_bv_plugin over extract

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-13 11:46:53 -08:00
parent 93be3d2b2c
commit 73b032ae4e
1 changed files with 13 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/ast/euf/euf_bv_plugin.cpp
View file

@ -161,18 +161,25 @@ namespace euf {
void bv_plugin::propagate_values(enode* x) { void bv_plugin::propagate_values(enode* x) {
if (!is_value(x)) if (!is_value(x))
return; return;
auto val_x = get_value(x);
enode* a, * b; enode* a, * b;
for (enode* p : enode_parents(x)) unsigned lo, hi;
if (is_concat(p, a, b) && is_value(a) && is_value(b) && !is_value(p)) for (enode* p : enode_parents(x)) {
if (is_concat(p, a, b) && is_value(a) && is_value(b))
push_merge(mk_concat(a->get_interpreted(), b->get_interpreted()), mk_value_concat(a, b)); push_merge(mk_concat(a->get_interpreted(), b->get_interpreted()), mk_value_concat(a, b));
if (is_extract(p, lo, hi)) {
auto val_p = mod2k(machine_div2k(val_x, lo), hi - lo + 1);
push_merge(p, mk_value(val_p, width(p)));
}
}
for (enode* sib : enode_class(x)) { for (enode* sib : enode_class(x)) {
if (is_concat(sib, a, b)) { if (is_concat(sib, a, b)) {
if (!is_value(a) || !is_value(b)) { if (!is_value(a) || !is_value(b)) {
auto val = get_value(x); auto val_a = machine_div2k(val_x, width(b));
auto val_a = machine_div2k(val, width(b)); auto val_b = mod2k(val_x, width(b));
auto val_b = mod2k(val, width(b));
push_merge(mk_concat(mk_value(val_a, width(a)), mk_value(val_b, width(b))), x->get_interpreted()); push_merge(mk_concat(mk_value(val_a, width(a)), mk_value(val_b, width(b))), x->get_interpreted());
} }
} }