projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: dd98af7) | patch
Remove redundant strings rewrite. (#2422)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 4 Sep 2018 23:35:54 +0000 (18:35 -0500)
committerAndres Noetzli <andres.noetzli@gmail.com>
Tue, 4 Sep 2018 23:35:54 +0000 (16:35 -0700)
commitdbe3d6da12fc30eb3bdf00d640e7457fba67e8dc
tree273142b94ba9be3837e062c4df2ca0ff15c64eb4tree
parentdd98af783ca7236acca3ee5d5bbcd0bf1df7828acommit | diff
Remove redundant strings rewrite. (#2422)

str.in.re( x, re.++( str.to.re(y), str.to.re(z) ) ) ---> x = str.++( y, z ) is not necessary since

re.++( str.to.re(y), str.to.re(z) ) -> str.to.re( str.++( y, z ) )
str.in.re( x, str.to.re( str.++(y, z) ) ) ---> x = str.++( y, z )

This PR removes the above rewrite, which was implemented incorrectly and was dead code.
src/theory/strings/theory_strings_rewriter.cpp diff | blob | history