Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 3 commits into from
Jan 9, 2023
Merged

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

merged 3 commits into from
Jan 9, 2023

Conversation

nunoplopes
Copy link
Collaborator

Example:

(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))

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))
```
@nunoplopes
Copy link
Collaborator Author

Traverses a chain of stores until it finds a store whose idx is equal to the select. Rewrite works if all stores until that guaranteed store have same value.
Quicks in Alive2 benchmarks.

// select(store(a, I, v), J) --> select(a, J) if I != J
do {
arg0 = to_app(arg0)->get_arg(0);
} while (m_util.is_store(arg0) && compare_args(num_args-1, args + 1, to_app(arg0)->get_args() + 1) == l_false);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

inner loop optimization is similar to what is going on in outer loop.
Move m_util.is_store(arg0) up to beginning for "every instruction is holy" optimization.

expr_ref tmp(m());
bool first = true;

#define RET(x, status) \
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why not a separate function that returns a status? BR_FAILED results in trying the next rewrite.
The local variable arg0 is updated in the first part of the code and should not be used in the second part because it could be unrelated to args

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry, I didn't understand the suggestion.
arg0 is only used in this new loop; it's not used in the old code.

@NikolajBjorner NikolajBjorner merged commit 5899fe3 into Z3Prover:master Jan 9, 2023
hgvk94 pushed a commit to hgvk94/z3 that referenced this pull request Mar 27, 2023
…rover#6526)

* 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants