diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-02-05 10:09:15 -0800 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-02-05 12:09:15 -0600 |
commit | 104b28b4c16b90a819c8f79d60f94a42fb0c0261 (patch) | |
tree | 3e2f508eadc02ccb7d2e6d20a25cbda15f413224 /src/theory | |
parent | b396d78982e109dc642611d32578bbca82b210cd (diff) |
Make stripConstantEndpoints() less aggressive (#2830)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index e8abc37a5..eff68ebe6 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -3647,26 +3647,6 @@ bool TheoryStringsRewriter::stripConstantEndpoints(std::vector<Node>& n1, overlap = s.size() - ret; } } - else if (n2[index1].getKind() == kind::STRING_ITOS) - { - const std::vector<unsigned>& svec = s.getVec(); - // can remove up to the first occurrence of a digit - unsigned svsize = svec.size(); - for (unsigned i = 0; i < svsize; i++) - { - unsigned sindex = r == 0 ? i : (svsize - 1) - i; - if (String::isDigit(svec[sindex])) - { - break; - } - else if (sss.empty()) // only if not substr - { - // e.g. str.contains( str.++( "a", x ), int.to.str(y) ) --> - // str.contains( x, int.to.str(y) ) - overlap--; - } - } - } else { // inconclusive |