diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-20 14:07:37 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-20 14:07:37 -0500 |
commit | 964760cf81eb7414a11bbd89ef3a16e8927d6947 (patch) | |
tree | 0c574e99433c722e69af6efeeefbe0901010f7b7 /src/theory/strings/strings_rewriter.cpp | |
parent | aa44c35f035f1cab03de0c5fe7c0f16b20f44696 (diff) |
Split string-specific operators from TheoryStringsRewriter (#3920)
Organization towards theory of sequences.
The motivation of this PR is to ensure that string-specific operators in the rewriter are in their own file; thus the use of mkConst<String> / getConst<String> is allowable in rewriter_str.cpp.
Diffstat (limited to 'src/theory/strings/strings_rewriter.cpp')
-rw-r--r-- | src/theory/strings/strings_rewriter.cpp | 247 |
1 files changed, 247 insertions, 0 deletions
diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp new file mode 100644 index 000000000..75dfe7432 --- /dev/null +++ b/src/theory/strings/strings_rewriter.cpp @@ -0,0 +1,247 @@ +/********************* */ +/*! \file strings_rewriter.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Andres Noetzli, Tianyi Liang + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of rewrite rules for string-specific operators in + ** theory of strings. + **/ + +#include "theory/strings/strings_rewriter.h" + +#include "expr/node_builder.h" +#include "theory/strings/theory_strings_utils.h" +#include "util/rational.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace strings { + +Node StringsRewriter::rewriteStrToInt(Node node) +{ + Assert(node.getKind() == STRING_STOI); + NodeManager* nm = NodeManager::currentNM(); + if (node[0].isConst()) + { + Node ret; + String s = node[0].getConst<String>(); + if (s.isNumber()) + { + ret = nm->mkConst(s.toNumber()); + } + else + { + ret = nm->mkConst(Rational(-1)); + } + return returnRewrite(node, ret, "stoi-eval"); + } + else if (node[0].getKind() == STRING_CONCAT) + { + for (TNode nc : node[0]) + { + if (nc.isConst()) + { + String t = nc.getConst<String>(); + if (!t.isNumber()) + { + Node ret = nm->mkConst(Rational(-1)); + return returnRewrite(node, ret, "stoi-concat-nonnum"); + } + } + } + } + return node; +} + +Node StringsRewriter::rewriteIntToStr(Node node) +{ + Assert(node.getKind() == STRING_ITOS); + NodeManager* nm = NodeManager::currentNM(); + if (node[0].isConst()) + { + Node ret; + if (node[0].getConst<Rational>().sgn() == -1) + { + ret = nm->mkConst(String("")); + } + else + { + std::string stmp = node[0].getConst<Rational>().getNumerator().toString(); + Assert(stmp[0] != '-'); + ret = nm->mkConst(String(stmp)); + } + return returnRewrite(node, ret, "itos-eval"); + } + return node; +} + +Node StringsRewriter::rewriteStrConvert(Node node) +{ + Kind nk = node.getKind(); + Assert(nk == STRING_TOLOWER || nk == STRING_TOUPPER); + NodeManager* nm = NodeManager::currentNM(); + if (node[0].isConst()) + { + std::vector<unsigned> nvec = node[0].getConst<String>().getVec(); + for (unsigned i = 0, nvsize = nvec.size(); i < nvsize; i++) + { + unsigned newChar = String::convertUnsignedIntToCode(nvec[i]); + // transform it + // upper 65 ... 90 + // lower 97 ... 122 + if (nk == STRING_TOUPPER) + { + if (newChar >= 97 && newChar <= 122) + { + newChar = newChar - 32; + } + } + else if (nk == STRING_TOLOWER) + { + if (newChar >= 65 && newChar <= 90) + { + newChar = newChar + 32; + } + } + newChar = String::convertCodeToUnsignedInt(newChar); + nvec[i] = newChar; + } + Node retNode = nm->mkConst(String(nvec)); + return returnRewrite(node, retNode, "str-conv-const"); + } + else if (node[0].getKind() == STRING_CONCAT) + { + NodeBuilder<> concatBuilder(STRING_CONCAT); + for (const Node& nc : node[0]) + { + concatBuilder << nm->mkNode(nk, nc); + } + // tolower( x1 ++ x2 ) --> tolower( x1 ) ++ tolower( x2 ) + Node retNode = concatBuilder.constructNode(); + return returnRewrite(node, retNode, "str-conv-minscope-concat"); + } + else if (node[0].getKind() == STRING_TOLOWER + || node[0].getKind() == STRING_TOUPPER) + { + // tolower( tolower( x ) ) --> tolower( x ) + // tolower( toupper( x ) ) --> tolower( x ) + Node retNode = nm->mkNode(nk, node[0][0]); + return returnRewrite(node, retNode, "str-conv-idem"); + } + else if (node[0].getKind() == STRING_ITOS) + { + // tolower( str.from.int( x ) ) --> str.from.int( x ) + return returnRewrite(node, node[0], "str-conv-itos"); + } + return node; +} + +Node StringsRewriter::rewriteStringLeq(Node n) +{ + Assert(n.getKind() == kind::STRING_LEQ); + NodeManager* nm = NodeManager::currentNM(); + if (n[0] == n[1]) + { + Node ret = nm->mkConst(true); + return returnRewrite(n, ret, "str-leq-id"); + } + if (n[0].isConst() && n[1].isConst()) + { + String s = n[0].getConst<String>(); + String t = n[1].getConst<String>(); + Node ret = nm->mkConst(s.isLeq(t)); + return returnRewrite(n, ret, "str-leq-eval"); + } + // empty strings + for (unsigned i = 0; i < 2; i++) + { + if (n[i].isConst() && n[i].getConst<String>().isEmptyString()) + { + Node ret = i == 0 ? nm->mkConst(true) : n[0].eqNode(n[1]); + return returnRewrite(n, ret, "str-leq-empty"); + } + } + + std::vector<Node> n1; + utils::getConcat(n[0], n1); + std::vector<Node> n2; + utils::getConcat(n[1], n2); + Assert(!n1.empty() && !n2.empty()); + + // constant prefixes + if (n1[0].isConst() && n2[0].isConst() && n1[0] != n2[0]) + { + String s = n1[0].getConst<String>(); + String t = n2[0].getConst<String>(); + // only need to truncate if s is longer + if (s.size() > t.size()) + { + s = s.prefix(t.size()); + } + // if prefix is not leq, then entire string is not leq + if (!s.isLeq(t)) + { + Node ret = nm->mkConst(false); + return returnRewrite(n, ret, "str-leq-cprefix"); + } + } + return n; +} + +Node StringsRewriter::rewriteStringFromCode(Node n) +{ + Assert(n.getKind() == kind::STRING_FROM_CODE); + NodeManager* nm = NodeManager::currentNM(); + + if (n[0].isConst()) + { + Integer i = n[0].getConst<Rational>().getNumerator(); + Node ret; + if (i >= 0 && i < strings::utils::getAlphabetCardinality()) + { + std::vector<unsigned> svec = {i.toUnsignedInt()}; + ret = nm->mkConst(String(svec)); + } + else + { + ret = nm->mkConst(String("")); + } + return returnRewrite(n, ret, "from-code-eval"); + } + return n; +} + +Node StringsRewriter::rewriteStringToCode(Node n) +{ + Assert(n.getKind() == kind::STRING_TO_CODE); + if (n[0].isConst()) + { + NodeManager* nm = NodeManager::currentNM(); + String s = n[0].getConst<String>(); + Node ret; + if (s.size() == 1) + { + std::vector<unsigned> vec = s.getVec(); + Assert(vec.size() == 1); + ret = nm->mkConst(Rational(String::convertUnsignedIntToCode(vec[0]))); + } + else + { + ret = nm->mkConst(Rational(-1)); + } + return returnRewrite(n, ret, "to-code-eval"); + } + return n; +} + +} // namespace strings +} // namespace theory +} // namespace CVC4 |