From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Thu, 27 Nov 2014 01:32:32 +0000 (-0600)
Subject: add more regexp rewriting
X-Git-Tag: cvc5-1.0.0~6478^2~4
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4bd4eb16ff7666321f16805b3aa0602019ef54ec;p=cvc5.git

add more regexp rewriting
---

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],