diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-23 17:18:19 -0600 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-23 15:18:19 -0800 |
commit | b3471b719f1cd031d35e9a431027088b0dec156b (patch) | |
tree | bc5e55a278f9e927471ce99146e9fdc992bc716b /src/theory/strings | |
parent | f5ca3e5d09b457ac21b10793eb5d1efe3fbe40f6 (diff) |
Initial support for string reverse (#3581)
Type rules, parsing and printing, basic rewriting including constant evaluation, reduction for string reverse (`str.rev`).
Also improves support in a few places for tolower/toupper.
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/kinds | 2 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 7 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 41 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 43 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.h | 7 |
5 files changed, 94 insertions, 6 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 4e90d1583..aa1e2627a 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -30,6 +30,7 @@ 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" +operator STRING_REV 1 "string reverse" sort STRING_TYPE \ Cardinality::INTEGERS \ @@ -104,6 +105,7 @@ typerule STRING_STOI "SimpleTypeRule<RInteger, AString>" typerule STRING_CODE "SimpleTypeRule<RInteger, AString>" typerule STRING_TOUPPER "SimpleTypeRule<RString, AString>" typerule STRING_TOLOWER "SimpleTypeRule<RString, AString>" +typerule STRING_REV "SimpleTypeRule<RString, AString>" typerule STRING_IN_REGEXP "SimpleTypeRule<RBool, AString, ARegExp>" diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 7b00ed2e2..1bc104096 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -129,6 +129,7 @@ TheoryStrings::TheoryStrings(context::Context* c, getExtTheory()->addFunctionKind(kind::STRING_CODE); getExtTheory()->addFunctionKind(kind::STRING_TOLOWER); getExtTheory()->addFunctionKind(kind::STRING_TOUPPER); + getExtTheory()->addFunctionKind(kind::STRING_REV); // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::STRING_LENGTH); @@ -147,6 +148,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_equalityEngine.addFunctionKind(kind::STRING_STRREPLALL); d_equalityEngine.addFunctionKind(kind::STRING_TOLOWER); d_equalityEngine.addFunctionKind(kind::STRING_TOUPPER); + d_equalityEngine.addFunctionKind(kind::STRING_REV); d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); @@ -437,7 +439,7 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd) 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_TOLOWER - || k == STRING_TOUPPER); + || k == STRING_TOUPPER || k == STRING_REV); std::vector<Node> new_nodes; Node res = d_preproc.simplify(n, new_nodes); Assert(res != n); @@ -765,7 +767,8 @@ 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_TOLOWER || k == STRING_TOUPPER) + || k == STRING_LEQ || k == STRING_TOLOWER || k == STRING_TOUPPER + || k == STRING_REV) { 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 4d1067583..a3b864089 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -476,9 +476,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node x = t[0]; Node r = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r"); - Node lent = nm->mkNode(STRING_LENGTH, t); + Node lenx = nm->mkNode(STRING_LENGTH, x); Node lenr = nm->mkNode(STRING_LENGTH, r); - Node eqLenA = lent.eqNode(lenr); + Node eqLenA = lenx.eqNode(lenr); Node i = nm->mkBoundVar(nm->integerType()); Node bvi = nm->mkNode(BOUND_VAR_LIST, i); @@ -498,7 +498,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { ci); Node bound = - nm->mkNode(AND, nm->mkNode(LEQ, d_zero, i), nm->mkNode(LEQ, i, lenr)); + nm->mkNode(AND, nm->mkNode(LEQ, d_zero, i), nm->mkNode(LT, i, lenr)); Node rangeA = nm->mkNode(FORALL, bvi, nm->mkNode(OR, bound.negate(), ri.eqNode(res))); @@ -514,7 +514,40 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // Thus, toLower( x ) = r retNode = r; - } else if( t.getKind() == kind::STRING_STRCTN ){ + } + else if (t.getKind() == STRING_REV) + { + Node x = t[0]; + Node r = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r"); + + Node lenx = nm->mkNode(STRING_LENGTH, x); + Node lenr = nm->mkNode(STRING_LENGTH, r); + Node eqLenA = lenx.eqNode(lenr); + + Node i = nm->mkBoundVar(nm->integerType()); + Node bvi = nm->mkNode(BOUND_VAR_LIST, i); + + Node revi = nm->mkNode( + MINUS, nm->mkNode(STRING_LENGTH, x), nm->mkNode(PLUS, i, d_one)); + Node ssr = nm->mkNode(STRING_SUBSTR, r, i, d_one); + Node ssx = nm->mkNode(STRING_SUBSTR, x, revi, d_one); + + Node bound = + nm->mkNode(AND, nm->mkNode(LEQ, d_zero, i), nm->mkNode(LT, i, lenr)); + Node rangeA = nm->mkNode( + FORALL, bvi, nm->mkNode(OR, bound.negate(), ssr.eqNode(ssx))); + // assert: + // len(r) = len(x) ^ + // forall i. 0 <= i < len(r) => + // substr(r,i,1) = substr(x,len(x)-(i+1),1) + Node assert = nm->mkNode(AND, eqLenA, rangeA); + new_nodes.push_back(assert); + + // Thus, (str.rev x) = r + retNode = r; + } + else if (t.getKind() == kind::STRING_STRCTN) + { Node x = t[0]; Node s = t[1]; //negative contains reduces to existential diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 5ae0d87b3..f17944027 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1600,6 +1600,12 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { retNode = nm->mkNode(STRING_LENGTH, node[0][0]); } } + else if (nk0 == STRING_TOLOWER || nk0 == STRING_TOUPPER + || nk0 == STRING_REV) + { + // len( f( x ) ) == len( x ) where f is tolower, toupper, or rev. + retNode = nm->mkNode(STRING_LENGTH, node[0][0]); + } } else if (nk == kind::STRING_CHARAT) { @@ -1641,6 +1647,10 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { { retNode = rewriteStrConvert(node); } + else if (nk == STRING_REV) + { + retNode = rewriteStrReverse(node); + } else if (nk == kind::STRING_PREFIX || nk == kind::STRING_SUFFIX) { retNode = rewritePrefixSuffix(node); @@ -3217,6 +3227,39 @@ Node TheoryStringsRewriter::rewriteStrConvert(Node node) return node; } +Node TheoryStringsRewriter::rewriteStrReverse(Node node) +{ + Assert(node.getKind() == STRING_REV); + NodeManager* nm = NodeManager::currentNM(); + Node x = node[0]; + if (x.isConst()) + { + std::vector<unsigned> nvec = node[0].getConst<String>().getVec(); + std::reverse(nvec.begin(), nvec.end()); + Node retNode = nm->mkConst(String(nvec)); + return returnRewrite(node, retNode, "str-conv-const"); + } + else if (x.getKind() == STRING_CONCAT) + { + std::vector<Node> children; + for (const Node& nc : x) + { + children.push_back(nm->mkNode(STRING_REV, nc)); + } + std::reverse(children.begin(), children.end()); + // rev( x1 ++ x2 ) --> rev( x2 ) ++ rev( x1 ) + Node retNode = nm->mkNode(STRING_CONCAT, children); + return returnRewrite(node, retNode, "str-rev-minscope-concat"); + } + else if (x.getKind() == STRING_REV) + { + // rev( rev( x ) ) --> x + Node retNode = x[0]; + return returnRewrite(node, retNode, "str-rev-idem"); + } + 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 35805e1c2..dd83df24f 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -232,6 +232,13 @@ class TheoryStringsRewriter : public TheoryRewriter * Returns the rewritten form of node. */ static Node rewriteStrConvert(Node node); + /** rewrite string reverse + * + * This is the entry point for post-rewriting terms n of the form + * str.rev( s ) + * Returns the rewritten form of node. + */ + static Node rewriteStrReverse(Node node); /** rewrite string less than or equal * This is the entry point for post-rewriting terms n of the form * str.<=( t, s ) |