diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-23 22:25:16 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-23 22:25:16 -0800 |
commit | 89427d48962dc22db14a3bab62e8542f9014fa67 (patch) | |
tree | 2b677352a36beff717b2031eb39044a5337d4f8f /src/theory | |
parent | b6dcaeb9b1e430941f1f4345152ebad21634a0be (diff) |
Revert "Minor"
This reverts commit b6dcaeb9b1e430941f1f4345152ebad21634a0be.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 16 |
1 files changed, 6 insertions, 10 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 8e69b6faf..f1cdcb9e9 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -2061,17 +2061,13 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { } else if (node[0].getKind() == kind::STRING_SUBSTR) { - if (checkEntailNonEmpty(node[1])) + Node zero = nm->mkConst(Rational(0)); + if (node[0][1] == zero && node[0][2].getKind() == kind::STRING_STRIDOF + && node[0][0] == node[0][2][0] && node[0][2][1] == node[1] + && node[0][2][2] == zero && checkEntailNonEmpty(node[1])) { - Node lenNonCtn = nm->mkNode( - MINUS, - nm->mkNode(STRING_STRIDOF, node[0][0], node[1], node[0][1]), - node[0][1]); - if (checkEntailArith(lenNonCtn, node[0][2])) - { - Node ret = nm->mkConst(false); - return returnRewrite(node, ret, "ctn-substr-idof"); - } + Node ret = nm->mkConst(false); + return returnRewrite(node, ret, "ctn-substr-idof"); } Node substr = node[0]; |