summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus_inst.h
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2021-05-18 14:32:51 -0700
committerGitHub <noreply@github.com>2021-05-18 21:32:51 +0000
commitc214051068aefdf831bf67e6b7d72591e5a91ece (patch)
treed46b4f6082fa107c30c6aa784de9bd38e6e4899d /src/theory/quantifiers/sygus_inst.h
parent626a1634fc21aed6e1149e5579ce112c1efc72bc (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 'src/theory/quantifiers/sygus_inst.h')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback