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

add intersection rewriting
---

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)