mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

Add rewrite for array selects of chain of stores of a same value (#6526)

Browse source 
* Add rewrite for array selects of chain of stores of a same value

Example:
```smt
(declare-fun mem () (Array (_ BitVec 4) (_ BitVec 4)))
(declare-const x (_ BitVec 4))
(declare-const y (_ BitVec 4))
; simplifies to #x1
(simplify (select (store (store (store mem #x1 #x1) y #x1) x #x1) #x1))
```

* Update array_rewriter.cpp

* Update array_rewriter.cpp
This commit is contained in:
Nuno Lopes 2023-01-09 03:09:01 +00:00 committed by GitHub
parent 1ddef117a2
commit 5899fe3cea
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 86 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

134
src/ast/rewriter/array_rewriter.cpp
View file

@ -198,13 +198,96 @@ bool array_rewriter::squash_store(unsigned n, expr* const* args, expr_ref& resul
br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(num_args >= 2);
expr *arg0 = args[0];
expr_ref tmp(m());
bool first = true;
#define RET(x, status) \
tmp = x; \
if (first || tmp == result) { \
result = std::move(tmp); \
return status; \
} \
goto exit
while (true) {
if (m_util.is_store(arg0)) {
SASSERT(to_app(arg0)->get_num_args() == num_args+1);
switch (compare_args(num_args - 1, args+1, to_app(arg0)->get_args()+1)) {
case l_true:
// select(store(a, I, v), I) --> v
RET(to_app(arg0)->get_arg(num_args), BR_DONE);
case l_false:
// select(store(a, I, v), J) --> select(a, J) if I != J
arg0 = to_app(arg0)->get_arg(0);
continue;
case l_undef:
// check if loading from subsequent arrays yields the same value
if (first) {
result = to_app(arg0)->get_arg(num_args);
first = false;
} else if (result != to_app(arg0)->get_arg(num_args)) {
goto exit;
}
arg0 = to_app(arg0)->get_arg(0);
continue;
}
}
if (m_util.is_const(arg0)) {
// select(const(v), I) --> v
RET(to_app(arg0)->get_arg(0), BR_DONE);
}
if (is_lambda(arg0)) {
// anywhere lambda reduction as opposed to whnf
// select(lambda(X) M, N) -> M[N/X]
quantifier* q = to_quantifier(arg0);
SASSERT(q->get_num_decls() == num_args - 1);
var_subst subst(m());
expr_ref_vector _args(m());
var_shifter sh(m());
for (unsigned i = 1; i < num_args; ++i) {
sh(args[i], num_args-1, result);
_args.push_back(result);
}
expr_ref tmp2 = subst(q->get_expr(), _args.size(), _args.data());
inv_var_shifter invsh(m());
invsh(tmp2, _args.size(), tmp2);
RET(std::move(tmp2), BR_REWRITE_FULL);
}
if (m_util.is_map(arg0)) {
app* a = to_app(arg0);
func_decl* f0 = m_util.get_map_func_decl(a);
expr_ref_vector args0(m());
for (expr* arg : *a) {
ptr_vector<expr> args1;
args1.push_back(arg);
args1.append(num_args-1, args + 1);
args0.push_back(m_util.mk_select(args1.size(), args1.data()));
}
RET(m().mk_app(f0, args0.size(), args0.data()), BR_REWRITE2);
}
if (m_util.is_as_array(arg0)) {
// select(as-array[f], I) --> f(I)
func_decl * f = m_util.get_as_array_func_decl(to_app(arg0));
RET(m().mk_app(f, num_args - 1, args + 1), BR_REWRITE1);
}
break;
}
exit:
result.reset();
if (m_util.is_store(args[0])) {
SASSERT(to_app(args[0])->get_num_args() == num_args+1);
switch (compare_args(num_args - 1, args+1, to_app(args[0])->get_args()+1)) {
case l_true:
// select(store(a, I, v), I) --> v
result = to_app(args[0])->get_arg(num_args);
return BR_DONE;
UNREACHABLE();
case l_false: {
expr* arg0 = to_app(args[0])->get_arg(0);
while (m_util.is_store(arg0) && compare_args(num_args-1, args + 1, to_app(arg0)->get_args() + 1) == l_false) {
@ -261,51 +344,6 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args,
}
}
if (m_util.is_const(args[0])) {
// select(const(v), I) --> v
result = to_app(args[0])->get_arg(0);
return BR_DONE;
}
if (is_lambda(args[0])) {
// anywhere lambda reduction as opposed to whnf
// select(lambda(X) M, N) -> M[N/X]
quantifier* q = to_quantifier(args[0]);
SASSERT(q->get_num_decls() == num_args - 1);
var_subst subst(m());
expr_ref_vector _args(m());
var_shifter sh(m());
for (unsigned i = 1; i < num_args; ++i) {
sh(args[i], num_args-1, result);
_args.push_back(result);
}
result = subst(q->get_expr(), _args.size(), _args.data());
inv_var_shifter invsh(m());
invsh(result, _args.size(), result);
return BR_REWRITE_FULL;
}
if (m_util.is_map(args[0])) {
app* a = to_app(args[0]);
func_decl* f0 = m_util.get_map_func_decl(a);
expr_ref_vector args0(m());
for (expr* arg : *a) {
ptr_vector<expr> args1;
args1.push_back(arg);
args1.append(num_args-1, args + 1);
args0.push_back(m_util.mk_select(args1.size(), args1.data()));
}
result = m().mk_app(f0, args0.size(), args0.data());
return BR_REWRITE2;
}
if (m_util.is_as_array(args[0])) {
// select(as-array[f], I) --> f(I)
func_decl * f = m_util.get_as_array_func_decl(to_app(args[0]));
result = m().mk_app(f, num_args - 1, args + 1);
return BR_REWRITE1;
}
expr* c, *th, *el;
if (m().is_ite(args[0], c, th, el) && (m_expand_select_ite || (th->get_ref_count() == 1 || el->get_ref_count() == 1))) {
ptr_vector<expr> args1, args2;