diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-11-26 19:32:32 -0600 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-11-26 19:33:53 -0600 |
commit | 4bd4eb16ff7666321f16805b3aa0602019ef54ec (patch) | |
tree | 56f54e4e10a70e48295326a741520ac6cd396dbc | |
parent | 34e2436636d7a43dd6b9ec5439884f0d8960f06b (diff) |
add more regexp rewriting
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 12 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 10 |
2 files changed, 15 insertions, 7 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 2752886cf..da8410a94 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -1157,9 +1157,10 @@ void RegExpOpr::getCharSet( Node r, std::set<unsigned> &pcset, SetNodes &pvset ) } case kind::REGEXP_INTER: { //TODO: Overapproximation for now - for(unsigned i=0; i<r.getNumChildren(); i++) { - getCharSet(r[i], cset, vset); - } + //for(unsigned i=0; i<r.getNumChildren(); i++) { + //getCharSet(r[i], cset, vset); + //} + getCharSet(r[0], cset, vset); break; } case kind::REGEXP_STAR: { @@ -1414,7 +1415,7 @@ Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node rNode = d_emptyRegexp; } } else if(r1 == r2) { - rNode = convert1(cnt, r1); + rNode = r1; //convert1(cnt, r1); } else { PairNodes p(r1, r2); std::map< PairNodes, Node >::const_iterator itrcache = cache.find(p); @@ -1459,7 +1460,6 @@ Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node PairNodes p(r1, r2); cache2[ p ] = NodeManager::currentNM()->mkNode(kind::REGEXP_RV, NodeManager::currentNM()->mkConst(CVC4::Rational(cnt))); Node rt = intersectInternal2(r1l, r2l, cache2, spflag, cnt+1); - rt = convert1(cnt, rt); if(spflag) { //TODO: return Node::null(); @@ -1471,6 +1471,8 @@ Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node rNode = vec_nodes.size()==0 ? d_emptyRegexp : vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes); rNode = Rewriter::rewrite( rNode ); + rNode = convert1(cnt, rNode); + rNode = Rewriter::rewrite( rNode ); } else { //TODO: non-empty var set spflag = true; diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index c952a7b3c..99a062f20 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -100,7 +100,7 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) { if(!preNode.isNull()) { if(tmpNode[0].getKind() == kind::STRING_TO_REGEXP) { preNode = rewriteConcatString( - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0][0] ) ); + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0][0] ) ); node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) ); preNode = Node::null(); } else { @@ -143,7 +143,10 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) { retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec ); } else { if(!preNode.isNull()) { - node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) ); + bool bflag = (preNode.getKind() == kind::CONST_STRING && preNode.getConst<String>().isEmptyString() ); + if(node_vec.empty() || !bflag ) { + node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) ); + } } if(node_vec.size() > 1) { retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, node_vec); @@ -161,6 +164,7 @@ Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) { Node retNode = node; std::vector<Node> node_vec; bool flag = false; + //bool allflag = false; for(unsigned i=0; i<node.getNumChildren(); ++i) { if(node[i].getKind() == kind::REGEXP_UNION) { Node tmpNode = prerewriteOrRegExp( node[i] ); @@ -617,6 +621,8 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode 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.getKind() == kind::REGEXP_PLUS) { retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, node[0], |