Add rewrite for array selects of chain of stores of a same value #6526
Conversation
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)) ```
|
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. |
src/ast/rewriter/array_rewriter.cpp
Outdated
| // 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); |
There was a problem hiding this comment.
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) \ |
There was a problem hiding this comment.
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
There was a problem hiding this comment.
Sorry, I didn't understand the suggestion.
arg0 is only used in this new loop; it's not used in the old code.
…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
Example: