diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-24 10:45:47 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-07-24 10:45:47 -0500 |
commit | 1c57b6f8e0847d682dbee2f79717290cb3449883 (patch) | |
tree | 92d2aa56878de1758924d6e5a9251707a7d01456 /src | |
parent | 892718a5925075ad9024e2183060c4c25d2716e0 (diff) |
Minor refactoring of regexp operation (#3116)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 106 |
1 files changed, 47 insertions, 59 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 0d422e823..bd693c6c3 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -1432,70 +1432,58 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > 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::REGEXP_RANGE: { - 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; - } - case kind::REGEXP_LOOP: { - retNode = removeIntersection( r[0] ); - retNode = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_LOOP, retNode, r[1], r[2]) ); - break; + return itr->second; + } + Node retNode; + Kind rk = r.getKind(); + switch (rk) + { + case REGEXP_EMPTY: + case REGEXP_SIGMA: + case REGEXP_RANGE: + case STRING_TO_REGEXP: + { + retNode = r; + break; + } + case REGEXP_CONCAT: + case REGEXP_UNION: + case REGEXP_STAR: + { + NodeBuilder<> nb(rk); + for (const Node& rc : r) + { + nb << removeIntersection(rc); } - default: { - Unreachable(); + retNode = Rewriter::rewrite(nb.constructNode()); + break; + } + + case REGEXP_INTER: + { + retNode = removeIntersection(r[0]); + for (size_t i = 1, nchild = r.getNumChildren(); i < nchild; i++) + { + bool spflag = false; + Node tmpNode = removeIntersection(r[i]); + retNode = intersect(retNode, tmpNode, spflag); } + break; + } + case REGEXP_LOOP: + { + retNode = removeIntersection(r[0]); + retNode = Rewriter::rewrite( + NodeManager::currentNM()->mkNode(REGEXP_LOOP, retNode, r[1], r[2])); + break; + } + default: + { + Unreachable(); } - d_rm_inter_cache[r] = retNode; } + d_rm_inter_cache[r] = retNode; Trace("regexp-intersect") << "Remove INTERSECTION( " << mkString(r) << " ) = " << mkString(retNode) << std::endl; return retNode; } |