diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/kinds | 4 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 9 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 44 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 40 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.h | 7 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_type_rules.h | 21 |
6 files changed, 123 insertions, 2 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index df6085422..715ea8f50 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -28,6 +28,8 @@ operator STRING_SUFFIX 2 "string suffixof" operator STRING_ITOS 1 "integer to string" operator STRING_STOI 1 "string to integer (total function)" operator STRING_CODE 1 "string to code, returns the code of the first character of the string if it has length one, -1 otherwise" +operator STRING_TOLOWER 1 "string to lowercase conversion" +operator STRING_TOUPPER 1 "string to uppercase conversion" sort STRING_TYPE \ Cardinality::INTEGERS \ @@ -100,6 +102,8 @@ typerule STRING_SUFFIX ::CVC4::theory::strings::StringSuffixOfTypeRule typerule STRING_ITOS ::CVC4::theory::strings::StringIntToStrTypeRule typerule STRING_STOI ::CVC4::theory::strings::StringStrToIntTypeRule typerule STRING_CODE ::CVC4::theory::strings::StringStrToIntTypeRule +typerule STRING_TOUPPER ::CVC4::theory::strings::StringStrToStrTypeRule +typerule STRING_TOLOWER ::CVC4::theory::strings::StringStrToStrTypeRule typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index ac6c0c102..435d1d8c7 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -140,6 +140,8 @@ TheoryStrings::TheoryStrings(context::Context* c, getExtTheory()->addFunctionKind(kind::STRING_IN_REGEXP); getExtTheory()->addFunctionKind(kind::STRING_LEQ); getExtTheory()->addFunctionKind(kind::STRING_CODE); + getExtTheory()->addFunctionKind(kind::STRING_TOLOWER); + getExtTheory()->addFunctionKind(kind::STRING_TOUPPER); // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::STRING_LENGTH); @@ -156,6 +158,8 @@ TheoryStrings::TheoryStrings(context::Context* c, d_equalityEngine.addFunctionKind(kind::STRING_STRIDOF); d_equalityEngine.addFunctionKind(kind::STRING_STRREPL); d_equalityEngine.addFunctionKind(kind::STRING_STRREPLALL); + d_equalityEngine.addFunctionKind(kind::STRING_TOLOWER); + d_equalityEngine.addFunctionKind(kind::STRING_TOUPPER); d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); @@ -527,7 +531,8 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd) NodeManager* nm = NodeManager::currentNM(); Assert(k == STRING_SUBSTR || k == STRING_STRCTN || k == STRING_STRIDOF || k == STRING_ITOS || k == STRING_STOI || k == STRING_STRREPL - || k == STRING_STRREPLALL || k == STRING_LEQ); + || k == STRING_STRREPLALL || k == STRING_LEQ || k == STRING_TOLOWER + || k == STRING_TOUPPER); std::vector<Node> new_nodes; Node res = d_preproc.simplify(n, new_nodes); Assert(res != n); @@ -854,7 +859,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { if (k == kind::STRING_STRIDOF || k == kind::STRING_ITOS || k == kind::STRING_STOI || k == kind::STRING_STRREPL || k == kind::STRING_STRREPLALL || k == kind::STRING_STRCTN - || k == STRING_LEQ) + || k == STRING_LEQ || k == STRING_TOLOWER || k == STRING_TOUPPER) { std::stringstream ss; ss << "Term of kind " << k diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 6ceeff6f2..e3634f84f 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -486,6 +486,50 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // Thus, replaceall( x, y, z ) = rpaw retNode = rpaw; + } + else if (t.getKind() == STRING_TOLOWER || t.getKind() == STRING_TOUPPER) + { + Node x = t[0]; + Node r = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r"); + + Node lent = nm->mkNode(STRING_LENGTH, t); + Node lenr = nm->mkNode(STRING_LENGTH, r); + Node eqLenA = lent.eqNode(lenr); + + Node i = nm->mkBoundVar(nm->integerType()); + Node bvi = nm->mkNode(BOUND_VAR_LIST, i); + + Node ci = nm->mkNode(STRING_CODE, nm->mkNode(STRING_SUBSTR, x, i, d_one)); + Node ri = nm->mkNode(STRING_CODE, nm->mkNode(STRING_SUBSTR, r, i, d_one)); + + Node lb = nm->mkConst(Rational(t.getKind() == STRING_TOUPPER ? 97 : 65)); + Node ub = nm->mkConst(Rational(t.getKind() == STRING_TOUPPER ? 122 : 90)); + Node offset = + nm->mkConst(Rational(t.getKind() == STRING_TOUPPER ? -32 : 32)); + + Node res = nm->mkNode( + ITE, + nm->mkNode(AND, nm->mkNode(LEQ, lb, ci), nm->mkNode(LEQ, ci, ub)), + nm->mkNode(PLUS, ci, offset), + ci); + + Node bound = + nm->mkNode(AND, nm->mkNode(LEQ, d_zero, i), nm->mkNode(LEQ, i, lenr)); + Node rangeA = + nm->mkNode(FORALL, bvi, nm->mkNode(OR, bound.negate(), ri.eqNode(res))); + + // upper 65 ... 90 + // lower 97 ... 122 + // assert: + // len(r) = len(x) ^ + // forall i. 0 <= i < len(r) => + // str.code( str.substr(r,i,1) ) = ite( 97 <= ci <= 122, ci-32, ci) + // where ci = str.code( str.substr(x,i,1) ) + Node assert = nm->mkNode(AND, eqLenA, rangeA); + new_nodes.push_back(assert); + + // Thus, toLower( x ) = r + retNode = r; } else if( t.getKind() == kind::STRING_STRCTN ){ Node x = t[0]; Node s = t[1]; diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index cb5508fb7..37e7d004f 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1484,6 +1484,10 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { { retNode = rewriteReplaceAll(node); } + else if (nk == STRING_TOLOWER || nk == STRING_TOUPPER) + { + retNode = rewriteStrConvert(node); + } else if (nk == kind::STRING_PREFIX || nk == kind::STRING_SUFFIX) { retNode = rewritePrefixSuffix(node); @@ -2974,6 +2978,42 @@ Node TheoryStringsRewriter::rewriteReplaceInternal(Node node) return Node::null(); } +Node TheoryStringsRewriter::rewriteStrConvert(Node node) +{ + Kind nk = node.getKind(); + Assert(nk == STRING_TOLOWER || nk == STRING_TOUPPER); + 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 = CVC4::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 = CVC4::String::convertCodeToUnsignedInt(newChar); + nvec[i] = newChar; + } + Node retNode = NodeManager::currentNM()->mkConst(String(nvec)); + return returnRewrite(node, retNode, "str-conv-const"); + } + return node; +} + Node TheoryStringsRewriter::rewriteStringLeq(Node n) { Assert(n.getKind() == kind::STRING_LEQ); diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index c273ef40e..ee92828de 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -226,6 +226,13 @@ class TheoryStringsRewriter { * str.replaceall. If it returns a non-null ret, then node rewrites to ret. */ static Node rewriteReplaceInternal(Node node); + /** rewrite string convert + * + * This is the entry point for post-rewriting terms n of the form + * str.tolower( s ) and str.toupper( s ) + * Returns the rewritten form of node. + */ + static Node rewriteStrConvert(Node node); /** rewrite string less than or equal * This is the entry point for post-rewriting terms n of the form * str.<=( t, s ) diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 91de8ac01..de77315fc 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -240,6 +240,27 @@ public: } }; +class StringStrToStrTypeRule +{ + public: + inline static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check) + { + if (check) + { + TypeNode t = n[0].getType(check); + if (!t.isString()) + { + std::stringstream ss; + ss << "expecting a string term in argument of " << n.getKind(); + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + } + return nodeManager->stringType(); + } +}; + class RegExpConcatTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) |