Fix `collectEmptyEqs()` in string utils (#6562)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 18 May 2021 21:32:51 +0000 (14:32 -0700)
committerGitHub <noreply@github.com>
Tue, 18 May 2021 21:32:51 +0000 (21:32 +0000)
commitc214051068aefdf831bf67e6b7d72591e5a91ece
treed46b4f6082fa107c30c6aa784de9bd38e6e4899d
parent626a1634fc21aed6e1149e5579ce112c1efc72bc
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.
src/theory/strings/theory_strings_utils.cpp
test/regress/CMakeLists.txt
test/regress/regress2/strings/issue6483.smt2 [new file with mode: 0644]
test/unit/theory/CMakeLists.txt
test/unit/theory/theory_strings_utils_white.cpp [new file with mode: 0644]