From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Fri, 25 Jul 2014 19:50:10 +0000 (-0500)
Subject: fix for regexp union rewriting
X-Git-Tag: cvc5-1.0.0~6686
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=215b2b1e8435703f513bcdd02082cd485f2e4bf9;p=cvc5.git

fix for regexp union rewriting
---

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 20fbf2870..e769eb712 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -1304,14 +1304,14 @@ bool RegExpOpr::containC2(unsigned cnt, Node n) {
   return false;
 }
 Node RegExpOpr::convert1(unsigned cnt, Node n) {
-  Trace("regexp-debug") << "Converting " << n << " ... " << std::endl;
+  Trace("regexp-debug") << "Converting " << n << " at " << cnt << "... " << std::endl;
   Node r1, r2;
   convert2(cnt, n, r1, r2);
   Trace("regexp-debug") << "... getting r1=" << r1 << ", and r2=" << r2 << std::endl;
   Node ret = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, 
      NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, r1), r2);
   ret = Rewriter::rewrite( ret );
-  Trace("regexp-debug") << "... done convert, with return " << ret << std::endl;
+  Trace("regexp-debug") << "... done convert at " << cnt << ", with return " << ret << std::endl;
   return ret;
 }
 void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) {
@@ -1379,6 +1379,13 @@ void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) {
 }
 Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node > cache, bool &spflag, unsigned cnt ) {
   Trace("regexp-intersect") << "Starting INTERSECT:\n  "<< mkString(r1) << ",\n  " << mkString(r2) << std::endl;
+  //if(Trace.isOn("regexp-debug")) {
+  //  Trace("regexp-debug") << "... with cache:\n";
+  //  for(std::map< PairNodes, Node >::const_iterator itr=cache.begin();
+  //      itr!=cache.end();itr++) {
+  //        Trace("regexp-debug") << "(" << itr->first.first << "," << itr->first.second << ")->" << itr->second << std::endl;
+  //      }
+  //}
   if(spflag) {
     //TODO: var
     return Node::null();
@@ -1408,7 +1415,7 @@ Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node
       PairNodes p(r1, r2);
       std::map< PairNodes, Node >::const_iterator itrcache = cache.find(p);
       if(itrcache != cache.end()) {
-        rNode = convert1(cnt, itrcache->second);
+        rNode = itrcache->second;
       } else {
         if(checkConstRegExp(r1) && checkConstRegExp(r2)) {
           std::vector< unsigned > cset;
@@ -1445,7 +1452,7 @@ Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node
             Node r1l = derivativeSingle(r1, c);
             Node r2l = derivativeSingle(r2, c);
             std::map< PairNodes, Node > cache2(cache);
-            PairNodes p(r1l, r2l);
+            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);
@@ -1725,6 +1732,12 @@ std::string RegExpOpr::mkString( Node r ) {
         retStr += "]";
         break;
       }
+      case kind::REGEXP_RV: {
+        retStr += "<";
+        retStr += r[0].getConst<Rational>().getNumerator().toString();
+        retStr += ">";
+        break;
+      }
       default:
         Trace("strings-error") << "Unsupported term: " << r << " in RegExp." << std::endl;
         //Assert( false );
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 1014a95db..ca45cd794 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -164,8 +164,12 @@ Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) {
   for(unsigned i=0; i<node.getNumChildren(); ++i) {
     if(node[i].getKind() == kind::REGEXP_UNION) {
       Node tmpNode = prerewriteOrRegExp( node[i] );
-      for(unsigned int j=0; j<tmpNode.getNumChildren(); ++j) {
-        node_vec.push_back( tmpNode[j] );
+      if(tmpNode.getKind() == kind::REGEXP_UNION) {
+        for(unsigned int j=0; j<tmpNode.getNumChildren(); ++j) {
+          node_vec.push_back( tmpNode[j] );
+        }
+      } else {
+        node_vec.push_back( tmpNode );
       }
       flag = true;
     } else if(node[i].getKind() == kind::REGEXP_EMPTY) {