From e448191212c319f9388e0ddf6845b55de1348465 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 3 Jan 2023 11:08:57 +0000 Subject: [PATCH] array rewriter: expand select of store with const array into an ite This: (simplify (select (store ((as const (Array (_ BitVec 4) (_ BitVec 4))) #x0) x #x1) y)) => (ite (= x y) #x1 #x0) --- src/ast/rewriter/array_rewriter.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index dd0e7e86930..08173d430be 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -228,14 +228,17 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args, } return true; }; + expr *array = to_app(args[0])->get_arg(0); + bool is_leaf = m_util.is_const(array); bool should_expand = m_blast_select_store || + is_leaf || are_values() || - (m_expand_select_store && to_app(args[0])->get_arg(0)->get_ref_count() == 1); + (m_expand_select_store && array->get_ref_count() == 1); if (should_expand) { // select(store(a, I, v), J) --> ite(I=J, v, select(a, J)) ptr_buffer new_args; - new_args.push_back(to_app(args[0])->get_arg(0)); + new_args.push_back(array); new_args.append(num_args-1, args+1); expr * sel_a_j = m().mk_app(get_fid(), OP_SELECT, num_args, new_args.data()); expr * v = to_app(args[0])->get_arg(num_args);