diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-18 13:44:57 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-18 13:44:57 -0700 |
commit | c2faac74261f433927ecf7f1c21cf623a2103321 (patch) | |
tree | 6288f82df026fa45bce7a973688914f7eb0ac8f5 /src/theory/arith/kinds | |
parent | 626a1634fc21aed6e1149e5579ce112c1efc72bc (diff) |
Fixes #6483. The benchmark in the issue was performing the following
incorrect rewrite:
```
Rewrite (str.replace "B" (str.replace (str.++ (str.replace "B" a "B") a) "B" "") "B") to (str.replace "B" a "B") by RPL_X_Y_X_SIMP.
```
The rewrite `RPL_X_Y_X_SIMP` rewrites terms of the form `(str.replace x
y x)`, where `x` is of length one and `(= y "")` rewrites to a
conjunction of equalities of the form `(= y_i "")` where `y_i` is some
term. The function responsible for collecting the terms `y_i` from this
conjunction, `collectEmptyEqs()`, returns a `bool` and a vector of
`Node`s. The `bool` indicates whether all equalities in the conjunction
were of the form `(= y_i "")`. The rewrite `RPL_X_Y_X_SIMP` only applies
if this is true. However, `collectEmptyEqs()` had a bug where it would
not return false when all of the conjuncts were equalities but not all
of them were equalities with the empty string. This commit fixes
`collectEmptyEqs()` and adds tests.
Diffstat (limited to 'src/theory/arith/kinds')
0 files changed, 0 insertions, 0 deletions