diff options
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 74 | ||||
-rw-r--r-- | src/theory/strings/regexp_operation.h | 2 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 75 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.h | 1 | ||||
-rw-r--r-- | test/regress/regress0/strings/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/strings/regexp003.smt2 | 13 |
6 files changed, 154 insertions, 12 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index da8410a94..adfd9a3f6 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -1484,11 +1484,75 @@ Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node Trace("regexp-intersect") << "End of INTERSECT( " << mkString(r1) << ", " << mkString(r2) << " ) = " << mkString(rNode) << std::endl; return rNode; } + +Node RegExpOpr::removeIntersection(Node r) { + Assert( checkConstRegExp(r) ); + std::map < Node, Node >::const_iterator itr = d_rm_inter_cache.find(r); + Node retNode; + if(itr != d_rm_inter_cache.end()) { + retNode = itr->second; + } else { + switch(r.getKind()) { + case kind::REGEXP_EMPTY: { + retNode = r; + break; + } + case kind::REGEXP_SIGMA: { + retNode = r; + break; + } + case kind::STRING_TO_REGEXP: { + retNode = r; + break; + } + case kind::REGEXP_CONCAT: { + std::vector< Node > vec_nodes; + for(unsigned i=0; i<r.getNumChildren(); i++) { + Node tmpNode = removeIntersection( r[i] ); + vec_nodes.push_back( tmpNode ); + } + retNode = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_nodes) ); + break; + } + case kind::REGEXP_UNION: { + std::vector< Node > vec_nodes; + for(unsigned i=0; i<r.getNumChildren(); i++) { + Node tmpNode = removeIntersection( r[i] ); + vec_nodes.push_back( tmpNode ); + } + retNode = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes) ); + break; + } + case kind::REGEXP_INTER: { + retNode = removeIntersection( r[0] ); + for(unsigned i=1; i<r.getNumChildren(); i++) { + bool spflag = false; + Node tmpNode = removeIntersection( r[i] ); + retNode = intersect( retNode, tmpNode, spflag ); + } + break; + } + case kind::REGEXP_STAR: { + retNode = removeIntersection( r[0] ); + retNode = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, retNode) ); + break; + } + default: { + Unreachable(); + } + } + d_rm_inter_cache[r] = retNode; + } + Trace("regexp-intersect") << "Remove INTERSECTION( " << mkString(r) << " ) = " << mkString(retNode) << std::endl; + return retNode; +} + Node RegExpOpr::intersect(Node r1, Node r2, bool &spflag) { - //std::map< unsigned, std::set< PairNodes > > cache; - std::map< PairNodes, Node > cache; if(checkConstRegExp(r1) && checkConstRegExp(r2)) { - return intersectInternal2(r1, r2, cache, spflag, 1); + Node rr1 = removeIntersection(r1); + Node rr2 = removeIntersection(r2); + std::map< PairNodes, Node > cache; + return intersectInternal2(rr1, rr2, cache, spflag, 1); } else { spflag = true; return Node::null(); @@ -1775,12 +1839,12 @@ std::string RegExpOpr::niceChar(Node r) { std::string RegExpOpr::mkString( Node r ) { std::string retStr; if(r.isNull()) { - retStr = "Empty"; + retStr = "Phi"; } else { int k = r.getKind(); switch( k ) { case kind::REGEXP_EMPTY: { - retStr += "Empty"; + retStr += "Phi"; break; } case kind::REGEXP_SIGMA: { diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index 6a31a23fb..3b898e5f5 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -64,6 +64,7 @@ private: std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_cset_cache; std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_fset_cache; std::map< PairNodes, Node > d_inter_cache; + std::map< Node, Node > d_rm_inter_cache; std::map< Node, std::vector< PairNodes > > d_split_cache; //bool checkStarPlus( Node t ); void simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes ); @@ -79,6 +80,7 @@ private: Node convert1(unsigned cnt, Node n); void convert2(unsigned cnt, Node n, Node &r1, Node &r2); Node intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node > cache, bool &spflag, unsigned cnt ); + Node removeIntersection(Node r); void firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset ); //TODO: for intersection diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 99a062f20..fc9a7c058 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -163,26 +163,38 @@ Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) { Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp start " << node << std::endl; Node retNode = node; std::vector<Node> node_vec; - bool flag = false; - //bool allflag = false; + 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) { - node_vec.push_back( tmpNode[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) { + //nothing + } else if(tmpNode.getKind() == kind::REGEXP_STAR && tmpNode[0].getKind() == kind::REGEXP_SIGMA) { + allflag = true; + retNode = tmpNode; + break; } else { - node_vec.push_back( tmpNode ); + if(std::find(node_vec.begin(), node_vec.end(), tmpNode) == node_vec.end()) { + node_vec.push_back( tmpNode ); + } } - flag = true; } else if(node[i].getKind() == kind::REGEXP_EMPTY) { - flag = true; + //nothing + } else if(node[i].getKind() == kind::REGEXP_STAR && node[i][0].getKind() == kind::REGEXP_SIGMA) { + allflag = true; + retNode = node[i]; + break; } else { node_vec.push_back( node[i] ); } } - if(flag) { + 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); @@ -191,6 +203,53 @@ Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) { return retNode; } +Node TheoryStringsRewriter::prerewriteAndRegExp(TNode node) { + Assert( node.getKind() == kind::REGEXP_INTER ); + Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp start " << node << std::endl; + Node retNode = node; + std::vector<Node> node_vec; + bool emptyflag = false; + //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) { + emptyflag = true; + 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 ); + } + } + } else if(node[i].getKind() == kind::REGEXP_EMPTY) { + emptyflag = true; + retNode = node[i]; + break; + } else if(node[i].getKind() == kind::REGEXP_STAR && node[i][0].getKind() == kind::REGEXP_SIGMA) { + //allNode = node[i]; + } else { + node_vec.push_back( node[i] ); + } + } + if(!emptyflag) { + 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); + } + Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp end " << retNode << std::endl; + return retNode; +} + bool TheoryStringsRewriter::checkConstRegExp( TNode t ) { if( t.getKind() != kind::STRING_TO_REGEXP ) { for( unsigned i = 0; i<t.getNumChildren(); ++i ) { @@ -618,6 +677,8 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { 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]; diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index 9d04f107f..dafab75cb 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -37,6 +37,7 @@ public: static Node rewriteConcatString(TNode node); static Node prerewriteConcatRegExp(TNode node); static Node prerewriteOrRegExp(TNode node); + static Node prerewriteAndRegExp(TNode node); static Node rewriteMembership(TNode node); static RewriteResponse postRewrite(TNode node); diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index c15e93cd8..865d05cd2 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -37,6 +37,7 @@ TESTS = \ model001.smt2 \ substr001.smt2 \ regexp001.smt2 \ + regexp003.smt2 \ leadingzero001.smt2 \ loop001.smt2 \ loop002.smt2 \ diff --git a/test/regress/regress0/strings/regexp003.smt2 b/test/regress/regress0/strings/regexp003.smt2 new file mode 100644 index 000000000..601689958 --- /dev/null +++ b/test/regress/regress0/strings/regexp003.smt2 @@ -0,0 +1,13 @@ +(set-logic QF_S)
+(set-info :status sat)
+(set-option :strings-exp true)
+
+(declare-const s String)
+
+(assert (str.in.re s (re.inter
+ (re.++ (str.to.re "a") (re.* (str.to.re "b"))
+ (re.inter (str.to.re "c") (re.* (str.to.re "c"))))
+ (re.++ (str.to.re "a") (re.* (str.to.re "b")) (re.* (str.to.re "c")))
+ )))
+
+(check-sat)
|