From 73b032ae4e00790d1142875fad82b893abaace07 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 13 Jan 2024 11:46:53 -0800 Subject: [PATCH] propagate values in euf_bv_plugin over extract Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_bv_plugin.cpp | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp index 420975b8e..e2bfc0d3b 100644 --- a/src/ast/euf/euf_bv_plugin.cpp +++ b/src/ast/euf/euf_bv_plugin.cpp @@ -161,18 +161,25 @@ namespace euf { void bv_plugin::propagate_values(enode* x) { if (!is_value(x)) return; - + + auto val_x = get_value(x); enode* a, * b; - for (enode* p : enode_parents(x)) - if (is_concat(p, a, b) && is_value(a) && is_value(b) && !is_value(p)) + unsigned lo, hi; + 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)); + + 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)) { if (is_concat(sib, a, b)) { if (!is_value(a) || !is_value(b)) { - auto val = get_value(x); - auto val_a = machine_div2k(val, width(b)); - auto val_b = mod2k(val, width(b)); + auto val_a = machine_div2k(val_x, width(b)); + auto val_b = mod2k(val_x, width(b)); push_merge(mk_concat(mk_value(val_a, width(a)), mk_value(val_b, width(b))), x->get_interpreted()); } }