disable inter cache

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index adfd9a3f6c4b6aabc9b86d11ac4a9861bb10b6a7..0169830594dbb5d9f986e0fc565e3cb52e46f0ff 100644 (file)
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -1383,7 +1383,8 @@ 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;
+  //(checkConstRegExp(r1) && checkConstRegExp(r2))
+  Trace("regexp-intersect") << "Starting INTERSECT(" << cnt << "):\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();
@@ -1398,9 +1399,9 @@ Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node
   std::pair < Node, Node > p(r1, r2);
   std::map < std::pair< Node, Node >, Node >::const_iterator itr = d_inter_cache.find(p);
   Node rNode;
-  if(itr != d_inter_cache.end()) {
-    rNode = itr->second;
-  } else {
+//  if(itr != d_inter_cache.end()) {
+//    rNode = itr->second;
+//  } else {
     if(r1 == d_emptyRegexp || r2 == d_emptyRegexp) {
       rNode = d_emptyRegexp;
     } else if(r1 == d_emptySingleton || r2 == d_emptySingleton) {
@@ -1422,66 +1423,60 @@ Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node
       if(itrcache != cache.end()) {
         rNode = itrcache->second;
       } else {
-        if(checkConstRegExp(r1) && checkConstRegExp(r2)) {
-          std::vector< unsigned > cset;
-          std::set< unsigned > cset1, cset2;
-          std::set< Node > vset1, vset2;
-          firstChars(r1, cset1, vset1);
-          firstChars(r2, cset2, vset2);
-          std::set_intersection(cset1.begin(), cset1.end(), cset2.begin(), cset1.end(),
-               std::inserter(cset, cset.begin()));
-          std::vector< Node > vec_nodes;
-          Node delta_exp;
-          int flag = delta(r1, delta_exp);
-          int flag2 = delta(r2, delta_exp);
-          if(flag != 2 && flag2 != 2) {
-            if(flag == 1 && flag2 == 1) {
-              vec_nodes.push_back(d_emptySingleton);
-            } else {
-              //TODO
-              spflag = true;
-            }
-          }
-          if(Trace.isOn("regexp-debug")) {
-            Trace("regexp-debug") << "Try CSET( " << cset.size() << " ) = ";
-            for(std::vector<unsigned>::const_iterator itr = cset.begin();
-              itr != cset.end(); itr++) {
-              CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) );
-              Trace("regexp-debug") << c << ", ";
-            }
-            Trace("regexp-debug") << std::endl;
+        std::vector< unsigned > cset;
+        std::set< unsigned > cset1, cset2;
+        std::set< Node > vset1, vset2;
+        firstChars(r1, cset1, vset1);
+        firstChars(r2, cset2, vset2);
+        std::set_intersection(cset1.begin(), cset1.end(), cset2.begin(), cset1.end(),
+             std::inserter(cset, cset.begin()));
+        std::vector< Node > vec_nodes;
+        Node delta_exp;
+        int flag = delta(r1, delta_exp);
+        int flag2 = delta(r2, delta_exp);
+        if(flag != 2 && flag2 != 2) {
+          if(flag == 1 && flag2 == 1) {
+            vec_nodes.push_back(d_emptySingleton);
+          } else {
+            //TODO
+            spflag = true;
           }
+        }
+        if(Trace.isOn("regexp-debug")) {
+          Trace("regexp-debug") << "Try CSET( " << cset.size() << " ) = ";
           for(std::vector<unsigned>::const_iterator itr = cset.begin();
             itr != cset.end(); itr++) {
             CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) );
-            Node r1l = derivativeSingle(r1, c);
-            Node r2l = derivativeSingle(r2, c);
-            std::map< PairNodes, Node > cache2(cache);
-            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);
-            if(spflag) {
-              //TODO:
-              return Node::null();
-            }
-            rt = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT,
-              NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c)), rt) );
-            vec_nodes.push_back(rt);
+            Trace("regexp-debug") << c << ", ";
           }
-          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;
+          Trace("regexp-debug") << std::endl;
         }
+        for(std::vector<unsigned>::const_iterator itr = cset.begin();
+          itr != cset.end(); itr++) {
+          CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) );
+          Node r1l = derivativeSingle(r1, c);
+          Node r2l = derivativeSingle(r2, c);
+          std::map< PairNodes, Node > cache2(cache);
+          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);
+          //if(spflag) {
+            //return Node::null();
+          //}
+          rt = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT,
+            NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c)), rt) );
+          vec_nodes.push_back(rt);
+        }
+        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 );
       }
     }
-    d_inter_cache[p] = rNode;
-  }
-  Trace("regexp-intersect") << "End of INTERSECT( " << mkString(r1) << ", " << mkString(r2) << " ) = " << mkString(rNode) << std::endl;
+//    d_inter_cache[p] = rNode;
+//  }
+  Trace("regexp-intersect") << "End(" << cnt << ") of INTERSECT( " << mkString(r1) << ", " << mkString(r2) << " ) = " << mkString(rNode) << std::endl;
   return rNode;
 }
 

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index fc9a7c05847552169db0c661d0bc92bdeb36b17e..dfec0a7957a8271f2c862f86416c498790730ef3 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -170,7 +170,9 @@ Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) {
       if(tmpNode.getKind() == kind::REGEXP_UNION) {
         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] );
+            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) {
@@ -191,7 +193,9 @@ Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) {
       retNode = node[i];
       break;
     } else {
-      node_vec.push_back( node[i] );
+      if(std::find(node_vec.begin(), node_vec.end(), node[i]) == node_vec.end()) {
+        node_vec.push_back( node[i] );
+      }
     }
   }
   if(!allflag) {
@@ -237,7 +241,9 @@ Node TheoryStringsRewriter::prerewriteAndRegExp(TNode node) {
     } 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(std::find(node_vec.begin(), node_vec.end(), node[i]) == node_vec.end()) {
+        node_vec.push_back( node[i] );
+      }
     }
   }
   if(!emptyflag) {
@@ -666,6 +672,15 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
   return RewriteResponse(orig==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode);
 }
 
+bool TheoryStringsRewriter::hasEpsilonNode(TNode node) {
+  for(unsigned int i=0; i<node.getNumChildren(); i++) {
+    if(node[i].getKind() == kind::STRING_TO_REGEXP && node[i][0].getKind() == kind::CONST_STRING && node[i][0].getConst<String>().isEmptyString()) {
+      return true;
+    }
+  }
+  return false;
+}
+
 RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) {
   Node retNode = node;
   Node orig = retNode;
@@ -684,6 +699,29 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) {
       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[0].getKind() == kind::REGEXP_EMPTY) {
+      retNode = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP,
+        NodeManager::currentNM()->mkConst( ::CVC4::String("") ) );
+    } else if(node[0].getKind() == kind::REGEXP_UNION) {
+      Node tmpNode = prerewriteOrRegExp(node[0]);
+      if(tmpNode.getKind() == kind::REGEXP_UNION) {
+        if(hasEpsilonNode(node[0])) {
+          std::vector< Node > node_vec;
+          for(unsigned int i=0; i<node[0].getNumChildren(); i++) {
+            if(node[0][i].getKind() == kind::STRING_TO_REGEXP && node[0][i][0].getKind() == kind::CONST_STRING && node[0][i][0].getConst<String>().isEmptyString()) {
+              //return true;
+            } else {
+              node_vec.push_back(node[0][i]);
+            }
+          }
+          retNode = node_vec.size()==1 ? node_vec[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, node_vec);
+          retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, retNode);
+        }
+      } else if(tmpNode.getKind() == kind::STRING_TO_REGEXP && tmpNode[0].getKind() == kind::CONST_STRING && tmpNode[0].getConst<String>().isEmptyString()) {
+        retNode = tmpNode;
+      } else {
+        retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, tmpNode);
+      }
     }
   } else if(node.getKind() == kind::REGEXP_PLUS) {
     retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, node[0],

diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index dafab75cbb7dbc54bedfee372ce29cbb1a0b44db..a1098f631c5336b3e47e348abb69cd07c904dbfd 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -42,6 +42,7 @@ public:
 
   static RewriteResponse postRewrite(TNode node);
 
+  static bool hasEpsilonNode(TNode node);
   static RewriteResponse preRewrite(TNode node);
 
   static inline void init() {}