From bc4055d4543f3b697ade38b810f7ac3cf02dc3c8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 30 Mar 2020 18:15:07 -0500 Subject: Rewrites for all remaining return statements in strings rewriter (#4178) Towards proofs for string rewrites. All return statements all now associated with an enum value. An indentation in a block of code changed in rewriteMembership. --- src/theory/strings/strings_rewriter.cpp | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) (limited to 'src/theory/strings/strings_rewriter.cpp') diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp index 275c2e25e..28ed14095 100644 --- a/src/theory/strings/strings_rewriter.cpp +++ b/src/theory/strings/strings_rewriter.cpp @@ -143,6 +143,16 @@ Node StringsRewriter::rewriteStrConvert(Node node) return node; } +Node StringsRewriter::rewriteStringLt(Node n) +{ + Assert(n.getKind() == kind::STRING_LT); + NodeManager* nm = NodeManager::currentNM(); + // eliminate s < t ---> s != t AND s <= t + Node retNode = nm->mkNode( + AND, n[0].eqNode(n[1]).negate(), nm->mkNode(STRING_LEQ, n[0], n[1])); + return returnRewrite(n, retNode, Rewrite::STR_LT_ELIM); +} + Node StringsRewriter::rewriteStringLeq(Node n) { Assert(n.getKind() == kind::STRING_LEQ); @@ -241,6 +251,18 @@ Node StringsRewriter::rewriteStringToCode(Node n) return n; } +Node StringsRewriter::rewriteStringIsDigit(Node n) +{ + Assert(n.getKind() == kind::STRING_IS_DIGIT); + NodeManager* nm = NodeManager::currentNM(); + // eliminate str.is_digit(s) ----> 48 <= str.to_code(s) <= 57 + Node t = nm->mkNode(STRING_TO_CODE, n[0]); + Node retNode = nm->mkNode(AND, + nm->mkNode(LEQ, nm->mkConst(Rational(48)), t), + nm->mkNode(LEQ, t, nm->mkConst(Rational(57)))); + return returnRewrite(n, retNode, Rewrite::IS_DIGIT_ELIM); +} + } // namespace strings } // namespace theory } // namespace CVC4 -- cgit v1.2.3