diff options
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 478 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.h | 32 |
2 files changed, 289 insertions, 221 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 8c589640c..9651fe980 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -307,8 +307,8 @@ Node TheoryStringsRewriter::rewriteEquality(Node node) Node TheoryStringsRewriter::rewriteConcat(Node node) { Assert(node.getKind() == kind::STRING_CONCAT); - Trace("strings-prerewrite") << "Strings::rewriteConcat start " << node - << std::endl; + Trace("strings-rewrite-debug") + << "Strings::rewriteConcat start " << node << std::endl; Node retNode = node; std::vector<Node> node_vec; Node preNode = Node::null(); @@ -380,16 +380,17 @@ Node TheoryStringsRewriter::rewriteConcat(Node node) std::sort(node_vec.begin() + lastIdx, node_vec.end()); retNode = mkConcat( kind::STRING_CONCAT, node_vec ); - Trace("strings-prerewrite") << "Strings::rewriteConcat end " << retNode - << std::endl; + Trace("strings-rewrite-debug") + << "Strings::rewriteConcat end " << retNode << std::endl; return retNode; } -Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) { +Node TheoryStringsRewriter::rewriteConcatRegExp(TNode node) +{ Assert( node.getKind() == kind::REGEXP_CONCAT ); NodeManager* nm = NodeManager::currentNM(); - Trace("strings-prerewrite") - << "Strings::prerewriteConcatRegExp flatten " << node << std::endl; + Trace("strings-rewrite-debug") + << "Strings::rewriteConcatRegExp flatten " << node << std::endl; Node retNode = node; std::vector<Node> vec; bool changed = false; @@ -437,8 +438,8 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) { } return returnRewrite(node, retNode, "re.concat-flatten"); } - Trace("strings-prerewrite") - << "Strings::prerewriteConcatRegExp start " << node << std::endl; + Trace("strings-rewrite-debug") + << "Strings::rewriteConcatRegExp start " << node << std::endl; std::vector<Node> cvec; std::vector<Node> preReStr; for (unsigned i = 0, size = vec.size(); i <= size; i++) @@ -498,99 +499,200 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) { return node; } -Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) { - Assert( node.getKind() == kind::REGEXP_UNION ); - Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp start " << node << std::endl; +Node TheoryStringsRewriter::rewriteStarRegExp(TNode node) +{ + Assert(node.getKind() == REGEXP_STAR); + NodeManager* nm = NodeManager::currentNM(); Node retNode = node; - std::vector<Node> node_vec; - bool allflag = false; - for(unsigned i=0; i<node.getNumChildren(); ++i) { - if(node[i].getKind() == kind::REGEXP_UNION) { - Node tmpNode = prerewriteOrRegExp( node[i] ); - if(tmpNode.getKind() == kind::REGEXP_UNION) { - for(unsigned int j=0; j<tmpNode.getNumChildren(); ++j) { - if(std::find(node_vec.begin(), node_vec.end(), tmpNode[j]) == node_vec.end()) { - if(std::find(node_vec.begin(), node_vec.end(), tmpNode[j]) == node_vec.end()) { - node_vec.push_back( tmpNode[j] ); - } - } + if (node[0].getKind() == REGEXP_STAR) + { + // ((R)*)* ---> R* + return returnRewrite(node, node[0], "re-star-nested-star"); + } + else if (node[0].getKind() == STRING_TO_REGEXP + && node[0][0].getKind() == CONST_STRING + && node[0][0].getConst<String>().isEmptyString()) + { + // ("")* ---> "" + return returnRewrite(node, node[0], "re-star-empty-string"); + } + else if (node[0].getKind() == REGEXP_EMPTY) + { + // (empty)* ---> "" + retNode = nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String(""))); + return returnRewrite(node, retNode, "re-star-empty"); + } + else if (node[0].getKind() == REGEXP_UNION) + { + // simplification of unions under star + if (hasEpsilonNode(node[0])) + { + bool changed = false; + std::vector<Node> node_vec; + for (const Node& nc : node[0]) + { + if (nc.getKind() == STRING_TO_REGEXP && nc[0].getKind() == CONST_STRING + && nc[0].getConst<String>().isEmptyString()) + { + // can be removed + changed = true; } - } else if(tmpNode.getKind() == kind::REGEXP_EMPTY) { - //nothing - } else if(tmpNode.getKind() == kind::REGEXP_STAR && tmpNode[0].getKind() == kind::REGEXP_SIGMA) { - allflag = true; - retNode = tmpNode; - break; - } else { - if(std::find(node_vec.begin(), node_vec.end(), tmpNode) == node_vec.end()) { - node_vec.push_back( tmpNode ); + else + { + node_vec.push_back(nc); } } - } else if(node[i].getKind() == kind::REGEXP_EMPTY) { - //nothing - } else if(node[i].getKind() == kind::REGEXP_STAR && node[i][0].getKind() == kind::REGEXP_SIGMA) { - allflag = true; - retNode = node[i]; - break; - } else { - if(std::find(node_vec.begin(), node_vec.end(), node[i]) == node_vec.end()) { - node_vec.push_back( node[i] ); + if (changed) + { + retNode = node_vec.size() == 1 ? node_vec[0] + : nm->mkNode(REGEXP_UNION, node_vec); + retNode = nm->mkNode(REGEXP_STAR, retNode); + // simplification of union beneath star based on loop above + // for example, ( "" | "a" )* ---> ("a")* + return returnRewrite(node, retNode, "re-star-union"); } } } - if(!allflag) { - std::vector< Node > nvec; - retNode = node_vec.size() == 0 ? NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec ) : - node_vec.size() == 1 ? node_vec[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, node_vec); - } - Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp end " << retNode << std::endl; - return retNode; + return node; } -Node TheoryStringsRewriter::prerewriteAndRegExp(TNode node) { - Assert( node.getKind() == kind::REGEXP_INTER ); - Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp start " << node << std::endl; - Node retNode = node; +Node TheoryStringsRewriter::rewriteAndOrRegExp(TNode node) +{ + Kind nk = node.getKind(); + Assert(nk == REGEXP_UNION || nk == REGEXP_INTER); + Trace("strings-rewrite-debug") + << "Strings::rewriteAndOrRegExp start " << node << std::endl; std::vector<Node> node_vec; - //Node allNode = Node::null(); - for(unsigned i=0; i<node.getNumChildren(); ++i) { - if(node[i].getKind() == kind::REGEXP_INTER) { - Node tmpNode = prerewriteAndRegExp( node[i] ); - if(tmpNode.getKind() == kind::REGEXP_INTER) { - for(unsigned int j=0; j<tmpNode.getNumChildren(); ++j) { - if(std::find(node_vec.begin(), node_vec.end(), tmpNode[j]) == node_vec.end()) { - node_vec.push_back( tmpNode[j] ); - } - } - } else if(tmpNode.getKind() == kind::REGEXP_EMPTY) { - retNode = tmpNode; - break; - } else if(tmpNode.getKind() == kind::REGEXP_STAR && tmpNode[0].getKind() == kind::REGEXP_SIGMA) { - //allNode = tmpNode; - } else { - if(std::find(node_vec.begin(), node_vec.end(), tmpNode) == node_vec.end()) { - node_vec.push_back( tmpNode ); + for (const Node& ni : node) + { + if (ni.getKind() == nk) + { + for (const Node& nic : ni) + { + if (std::find(node_vec.begin(), node_vec.end(), nic) == node_vec.end()) + { + node_vec.push_back(nic); } } - } else if(node[i].getKind() == kind::REGEXP_EMPTY) { - retNode = node[i]; - break; - } else if(node[i].getKind() == kind::REGEXP_STAR && node[i][0].getKind() == kind::REGEXP_SIGMA) { - //allNode = node[i]; - } else { - if(std::find(node_vec.begin(), node_vec.end(), node[i]) == node_vec.end()) { - node_vec.push_back( node[i] ); + } + else if (ni.getKind() == REGEXP_EMPTY) + { + if (nk == REGEXP_INTER) + { + return returnRewrite(node, ni, "re.and-empty"); } + // otherwise, can ignore + } + else if (ni.getKind() == REGEXP_STAR && ni[0].getKind() == REGEXP_SIGMA) + { + if (nk == REGEXP_UNION) + { + return returnRewrite(node, ni, "re.or-all"); + } + // otherwise, can ignore + } + else if (std::find(node_vec.begin(), node_vec.end(), ni) == node_vec.end()) + { + node_vec.push_back(ni); } } - if( retNode==node ){ - std::vector< Node > nvec; - retNode = node_vec.size() == 0 ? - NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, NodeManager::currentNM()->mkNode(kind::REGEXP_SIGMA, nvec)) : - node_vec.size() == 1 ? node_vec[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_INTER, node_vec); + NodeManager* nm = NodeManager::currentNM(); + std::vector<Node> nvec; + Node retNode; + if (node_vec.empty()) + { + if (nk == REGEXP_INTER) + { + retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA, nvec)); + } + else + { + retNode = nm->mkNode(kind::REGEXP_EMPTY, nvec); + } } - Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp end " << retNode << std::endl; - return retNode; + else + { + retNode = node_vec.size() == 1 ? node_vec[0] : nm->mkNode(nk, node_vec); + } + if (retNode != node) + { + // flattening and removing children, based on loop above + return returnRewrite(node, retNode, "re.andor-flatten"); + } + return node; +} + +Node TheoryStringsRewriter::rewriteLoopRegExp(TNode node) +{ + Assert(node.getKind() == REGEXP_LOOP); + Node retNode = node; + Node r = node[0]; + if (r.getKind() == REGEXP_STAR) + { + return returnRewrite(node, r, "re.loop-star"); + } + TNode n1 = node[1]; + NodeManager* nm = NodeManager::currentNM(); + CVC4::Rational RMAXINT(LONG_MAX); + AlwaysAssert(n1.isConst(), "re.loop contains non-constant integer (1)."); + AlwaysAssert(n1.getConst<Rational>().sgn() >= 0, + "Negative integer in string REGEXP_LOOP (1)"); + Assert(n1.getConst<Rational>() <= RMAXINT, + "Exceeded LONG_MAX in string REGEXP_LOOP (1)"); + unsigned l = n1.getConst<Rational>().getNumerator().toUnsignedInt(); + std::vector<Node> vec_nodes; + for (unsigned i = 0; i < l; i++) + { + vec_nodes.push_back(r); + } + if (node.getNumChildren() == 3) + { + TNode n2 = Rewriter::rewrite(node[2]); + Node n = + vec_nodes.size() == 0 + ? nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String(""))) + : vec_nodes.size() == 1 ? r : nm->mkNode(REGEXP_CONCAT, vec_nodes); + AlwaysAssert(n2.isConst(), "re.loop contains non-constant integer (2)."); + AlwaysAssert(n2.getConst<Rational>().sgn() >= 0, + "Negative integer in string REGEXP_LOOP (2)"); + Assert(n2.getConst<Rational>() <= RMAXINT, + "Exceeded LONG_MAX in string REGEXP_LOOP (2)"); + unsigned u = n2.getConst<Rational>().getNumerator().toUnsignedInt(); + if (u <= l) + { + retNode = n; + } + else + { + std::vector<Node> vec2; + vec2.push_back(n); + for (unsigned j = l; j < u; j++) + { + vec_nodes.push_back(r); + n = mkConcat(REGEXP_CONCAT, vec_nodes); + vec2.push_back(n); + } + retNode = nm->mkNode(REGEXP_UNION, vec2); + } + } + else + { + Node rest = nm->mkNode(REGEXP_STAR, r); + retNode = vec_nodes.size() == 0 + ? rest + : vec_nodes.size() == 1 + ? nm->mkNode(REGEXP_CONCAT, r, rest) + : nm->mkNode(REGEXP_CONCAT, + nm->mkNode(REGEXP_CONCAT, vec_nodes), + rest); + } + Trace("strings-lp") << "Strings::lp " << node << " => " << retNode + << std::endl; + if (retNode != node) + { + return returnRewrite(node, retNode, "re.loop"); + } + return node; } bool TheoryStringsRewriter::isConstRegExp( TNode t ) { @@ -887,12 +989,17 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { NodeManager* nm = NodeManager::currentNM(); Node retNode = node; Node orig = retNode; - - if(node.getKind() == kind::STRING_CONCAT) { + Kind nk = node.getKind(); + if (nk == kind::STRING_CONCAT) + { retNode = rewriteConcat(node); - } else if(node.getKind() == kind::EQUAL) { + } + else if (nk == kind::EQUAL) + { retNode = rewriteEquality(node); - } else if(node.getKind() == kind::STRING_LENGTH) { + } + else if (nk == kind::STRING_LENGTH) + { if( node[0].isConst() ){ retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst<String>().size() ) ); }else if( node[0].getKind() == kind::STRING_CONCAT ){ @@ -921,34 +1028,45 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { retNode = nm->mkNode(STRING_LENGTH, node[0][0]); } } - }else if( node.getKind() == kind::STRING_CHARAT ){ + } + else if (nk == kind::STRING_CHARAT) + { Node one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); retNode = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, node[0], node[1], one); - }else if( node.getKind() == kind::STRING_SUBSTR ){ + } + else if (nk == kind::STRING_SUBSTR) + { retNode = rewriteSubstr(node); - }else if( node.getKind() == kind::STRING_STRCTN ){ + } + else if (nk == kind::STRING_STRCTN) + { retNode = rewriteContains( node ); } - else if (node.getKind() == kind::STRING_LT) + else if (nk == kind::STRING_LT) { // eliminate s < t ---> s != t AND s <= t retNode = nm->mkNode(AND, node[0].eqNode(node[1]).negate(), nm->mkNode(STRING_LEQ, node[0], node[1])); } - else if (node.getKind() == kind::STRING_LEQ) + else if (nk == kind::STRING_LEQ) { retNode = rewriteStringLeq(node); - }else if( node.getKind()==kind::STRING_STRIDOF ){ + } + else if (nk == kind::STRING_STRIDOF) + { retNode = rewriteIndexof( node ); - }else if( node.getKind() == kind::STRING_STRREPL ){ + } + else if (nk == kind::STRING_STRREPL) + { retNode = rewriteReplace( node ); } - else if (node.getKind() == kind::STRING_PREFIX - || node.getKind() == kind::STRING_SUFFIX) + else if (nk == kind::STRING_PREFIX || nk == kind::STRING_SUFFIX) { retNode = rewritePrefixSuffix(node); - }else if(node.getKind() == kind::STRING_ITOS) { + } + else if (nk == kind::STRING_ITOS) + { if(node[0].isConst()) { if( node[0].getConst<Rational>().sgn()==-1 ){ retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); @@ -958,7 +1076,9 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(stmp) ); } } - }else if(node.getKind() == kind::STRING_STOI) { + } + else if (nk == kind::STRING_STOI) + { if(node[0].isConst()) { CVC4::String s = node[0].getConst<String>(); if(s.isNumber()) { @@ -977,13 +1097,49 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } } } - } else if(node.getKind() == kind::STRING_IN_REGEXP) { + } + else if (nk == kind::STRING_IN_REGEXP) + { retNode = rewriteMembership(node); } - else if (node.getKind() == STRING_CODE) + else if (nk == STRING_CODE) { retNode = rewriteStringCode(node); } + else if (nk == REGEXP_CONCAT) + { + retNode = rewriteConcatRegExp(node); + } + else if (nk == REGEXP_UNION || nk == REGEXP_INTER) + { + retNode = rewriteAndOrRegExp(node); + } + else if (nk == REGEXP_STAR) + { + retNode = rewriteStarRegExp(node); + } + else if (nk == REGEXP_PLUS) + { + retNode = + nm->mkNode(REGEXP_CONCAT, node[0], nm->mkNode(REGEXP_STAR, node[0])); + } + else if (nk == REGEXP_OPT) + { + retNode = nm->mkNode(REGEXP_UNION, + nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String(""))), + node[0]); + } + else if (nk == REGEXP_RANGE) + { + if (node[0] == node[1]) + { + retNode = nm->mkNode(STRING_TO_REGEXP, node[0]); + } + } + else if (nk == REGEXP_LOOP) + { + retNode = rewriteLoopRegExp(node); + } Trace("strings-postrewrite") << "Strings::postRewrite returning " << retNode << std::endl; if( orig!=retNode ){ @@ -1002,121 +1158,7 @@ bool TheoryStringsRewriter::hasEpsilonNode(TNode node) { } RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { - Node retNode = node; - Node orig = retNode; - Trace("strings-prerewrite") << "Strings::preRewrite start " << node << std::endl; - NodeManager* nm = NodeManager::currentNM(); - - if (node.getKind() == kind::REGEXP_CONCAT) - { - retNode = prerewriteConcatRegExp(node); - } else if(node.getKind() == kind::REGEXP_UNION) { - retNode = prerewriteOrRegExp(node); - } else if(node.getKind() == kind::REGEXP_INTER) { - retNode = prerewriteAndRegExp(node); - } - else if(node.getKind() == kind::REGEXP_STAR) { - if(node[0].getKind() == kind::REGEXP_STAR) { - retNode = node[0]; - } else if(node[0].getKind() == kind::STRING_TO_REGEXP && node[0][0].getKind() == kind::CONST_STRING && node[0][0].getConst<String>().isEmptyString()) { - retNode = node[0]; - } else if(node[0].getKind() == kind::REGEXP_EMPTY) { - retNode = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ); - } else if(node[0].getKind() == kind::REGEXP_UNION) { - Node tmpNode = prerewriteOrRegExp(node[0]); - if(tmpNode.getKind() == kind::REGEXP_UNION) { - if(hasEpsilonNode(node[0])) { - std::vector< Node > node_vec; - for(unsigned int i=0; i<node[0].getNumChildren(); i++) { - if(node[0][i].getKind() == kind::STRING_TO_REGEXP && node[0][i][0].getKind() == kind::CONST_STRING && node[0][i][0].getConst<String>().isEmptyString()) { - //return true; - } else { - node_vec.push_back(node[0][i]); - } - } - retNode = node_vec.size()==1 ? node_vec[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, node_vec); - retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, retNode); - } - } else if(tmpNode.getKind() == kind::STRING_TO_REGEXP && tmpNode[0].getKind() == kind::CONST_STRING && tmpNode[0].getConst<String>().isEmptyString()) { - retNode = tmpNode; - } else { - retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, tmpNode); - } - } - } else if(node.getKind() == kind::REGEXP_PLUS) { - retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, node[0], NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, node[0])); - } else if(node.getKind() == kind::REGEXP_OPT) { - retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, - NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ), - node[0]); - } else if(node.getKind() == kind::REGEXP_RANGE) { - if(node[0] == node[1]) { - retNode = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, node[0] ); - } - } else if(node.getKind() == kind::REGEXP_LOOP) { - Node r = node[0]; - if(r.getKind() == kind::REGEXP_STAR) { - retNode = r; - } else { - // eager - TNode n1 = Rewriter::rewrite( node[1] ); - // - if(!n1.isConst()) { - throw LogicException("re.loop contains non-constant integer (1)."); - } - CVC4::Rational rz(0); - CVC4::Rational RMAXINT(LONG_MAX); - AlwaysAssert(rz <= n1.getConst<Rational>(), "Negative integer in string REGEXP_LOOP (1)"); - Assert(n1.getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string REGEXP_LOOP (1)"); - // - unsigned l = n1.getConst<Rational>().getNumerator().toUnsignedInt(); - std::vector< Node > vec_nodes; - for(unsigned i=0; i<l; i++) { - vec_nodes.push_back(r); - } - if(node.getNumChildren() == 3) { - TNode n2 = Rewriter::rewrite( node[2] ); - //if(!n2.isConst()) { - // throw LogicException("re.loop contains non-constant integer (2)."); - //} - Node n = vec_nodes.size() == 0 - ? nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String(""))) - : vec_nodes.size() == 1 - ? r - : nm->mkNode(REGEXP_CONCAT, vec_nodes); - //Assert(n2.getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string REGEXP_LOOP (2)"); - unsigned u = n2.getConst<Rational>().getNumerator().toUnsignedInt(); - if(u <= l) { - retNode = n; - } else { - std::vector< Node > vec2; - vec2.push_back(n); - for(unsigned j=l; j<u; j++) { - vec_nodes.push_back(r); - n = mkConcat(REGEXP_CONCAT, vec_nodes); - vec2.push_back(n); - } - retNode = prerewriteOrRegExp(nm->mkNode(REGEXP_UNION, vec2)); - } - } else { - Node rest = nm->mkNode(REGEXP_STAR, r); - retNode = vec_nodes.size() == 0 - ? rest - : vec_nodes.size() == 1 - ? nm->mkNode(REGEXP_CONCAT, r, rest) - : nm->mkNode(REGEXP_CONCAT, - nm->mkNode(REGEXP_CONCAT, vec_nodes), - rest); - } - } - Trace("strings-lp") << "Strings::lp " << node << " => " << retNode << std::endl; - } - - Trace("strings-prerewrite") << "Strings::preRewrite returning " << retNode << std::endl; - if( orig!=retNode ){ - Trace("strings-rewrite-debug") << "Strings: pre-rewrite " << orig << " to " << retNode << std::endl; - } - return RewriteResponse(orig==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode); + return RewriteResponse(REWRITE_DONE, node); } Node TheoryStringsRewriter::rewriteSubstr(Node node) diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index 732d64095..1a3f388ba 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -61,9 +61,35 @@ class TheoryStringsRewriter { static bool isConstRegExp( TNode t ); static bool testConstStringInRegExp( CVC4::String &s, unsigned int index_start, TNode r ); - static Node prerewriteConcatRegExp(TNode node); - static Node prerewriteOrRegExp(TNode node); - static Node prerewriteAndRegExp(TNode node); + /** rewrite regular expression concatenation + * + * This is the entry point for post-rewriting applications of re.++. + * Returns the rewritten form of node. + */ + static Node rewriteConcatRegExp(TNode node); + /** rewrite regular expression star + * + * This is the entry point for post-rewriting applications of re.*. + * Returns the rewritten form of node. + */ + static Node rewriteStarRegExp(TNode node); + /** rewrite regular expression intersection/union + * + * This is the entry point for post-rewriting applications of re.inter and + * re.union. Returns the rewritten form of node. + */ + static Node rewriteAndOrRegExp(TNode node); + /** rewrite regular expression loop + * + * This is the entry point for post-rewriting applications of re.loop. + * Returns the rewritten form of node. + */ + static Node rewriteLoopRegExp(TNode node); + /** rewrite regular expression membership + * + * This is the entry point for post-rewriting applications of str.in.re + * Returns the rewritten form of node. + */ static Node rewriteMembership(TNode node); static bool hasEpsilonNode(TNode node); |