diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-18 14:32:51 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-18 21:32:51 +0000 |
| commit | c214051068aefdf831bf67e6b7d72591e5a91ece (patch) | |
| tree | d46b4f6082fa107c30c6aa784de9bd38e6e4899d /test/regress/regress2 | |
| parent | 626a1634fc21aed6e1149e5579ce112c1efc72bc (diff) | |
Fix `collectEmptyEqs()` in string utils (#6562)
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
Nodes. 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 'test/regress/regress2')
| -rw-r--r-- | test/regress/regress2/strings/issue6483.smt2 | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test/regress/regress2/strings/issue6483.smt2 b/test/regress/regress2/strings/issue6483.smt2 new file mode 100644 index 000000000..3ee748d27 --- /dev/null +++ b/test/regress/regress2/strings/issue6483.smt2 @@ -0,0 +1,15 @@ +(set-logic QF_SLIA) +(declare-fun a () String) +(assert + (xor + (= (= (str.replace "B" (str.replace (str.++ (str.replace "B" a "B") a) "B" "") "B") + (str.replace "B" (str.replace "B" a (str.++ a "B")) a)) + (not + (= (str.replace "B" (str.replace a "B" "") "B") + (str.replace "B" a (str.++ a "B"))))) + (= (str.replace "B" a "") + (str.replace "B" a + (ite (not (= (str.replace "" (str.replace a "" a) "") "")) "" + (str.replace "" (str.replace a "B" "") "B")))))) +(set-info :status unsat) +(check-sat) |