diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-23 21:54:23 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-23 21:54:23 -0800 |
commit | b6dcaeb9b1e430941f1f4345152ebad21634a0be (patch) | |
tree | a1b788d1742bf37070b530bd2ab3b26457c63da7 | |
parent | 77a9cac1975f30153c16493fba673b50e0331509 (diff) |
MinorstrongerContainsRew
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index f1cdcb9e9..8e69b6faf 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -2061,13 +2061,17 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { } else if (node[0].getKind() == kind::STRING_SUBSTR) { - 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])) + if (checkEntailNonEmpty(node[1])) { - Node ret = nm->mkConst(false); - return returnRewrite(node, ret, "ctn-substr-idof"); + 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 substr = node[0]; |