From 8378d5ed6b692cd6d0e1a970d958a0d17c531746 Mon Sep 17 00:00:00 2001
From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Tue, 15 Oct 2013 14:23:08 -0500
Subject: [PATCH] removes some junks

---
 .../strings/theory_strings_preprocess.cpp     | 10 ++-
 .../strings/theory_strings_rewriter.cpp       | 78 +------------------
 src/theory/strings/theory_strings_rewriter.h  |  1 -
 3 files changed, 11 insertions(+), 78 deletions(-)

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 378fa3428..c54cbb3b2 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -34,9 +34,13 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret
 		{
 			std::vector< Node > cc;
 			for(unsigned i=0; i<r.getNumChildren(); ++i) {
-				Node sk = NodeManager::currentNM()->mkSkolem( "recsym_$$", s.getType(), "created for regular expression concat" );
-				simplifyRegExp( sk, r[i], ret, nn );
-				cc.push_back( sk );
+				if(r[i].getKind() == kind::STRING_TO_REGEXP) {
+					cc.push_back( r[i][0] );
+				} else {
+					Node sk = NodeManager::currentNM()->mkSkolem( "recsym_$$", s.getType(), "created for regular expression concat" );
+					simplifyRegExp( sk, r[i], ret, nn );
+					cc.push_back( sk );
+				}
 			}
 			Node cc_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, 
 						NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, cc ) );
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 7b74a95ac..5ba67c25f 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -145,56 +145,6 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) {
     return retNode;
 }
 
-void TheoryStringsRewriter::simplifyRegExp( Node s, Node r, std::vector< Node > &ret ) {
-	int k = r.getKind();
-	switch( k ) {
-		case kind::STRING_TO_REGEXP:
-		{
-			Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, r[0] );
-			ret.push_back( eq );
-		}
-			break;
-		case kind::REGEXP_CONCAT:
-		{
-			std::vector< Node > cc;
-			for(unsigned i=0; i<r.getNumChildren(); ++i) {
-				Node sk = NodeManager::currentNM()->mkSkolem( "recsym_$$", s.getType(), "created for regular expression concat" );
-				simplifyRegExp( sk, r[i], ret );
-				cc.push_back( sk );
-			}
-			Node cc_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, 
-						NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, cc ) );
-			ret.push_back( cc_eq );
-		}
-			break;
-		case kind::REGEXP_OR:
-		{
-			std::vector< Node > c_or;
-			for(unsigned i=0; i<r.getNumChildren(); ++i) {
-				simplifyRegExp( s, r[i], c_or );
-			}
-			Node eq = NodeManager::currentNM()->mkNode( kind::OR, c_or );
-			ret.push_back( eq );
-		}
-			break;
-		case kind::REGEXP_INTER:
-			for(unsigned i=0; i<r.getNumChildren(); ++i) {
-				simplifyRegExp( s, r[i], ret );
-			}
-			break;
-		case kind::REGEXP_STAR:
-		{
-			Node eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r );
-			ret.push_back( eq );
-		}
-			break;
-		default:
-			//TODO: special sym: sigma, none, all
-			Trace("strings-prerewrite") << "Unsupported term: " << r << " in simplifyRegExp." << std::endl;
-			Assert( false );
-			break;
-	}
-}
 bool TheoryStringsRewriter::checkConstRegExp( TNode t ) {
 	if( t.getKind() != kind::STRING_TO_REGEXP ) {
 		for( unsigned i = 0; i<t.getNumChildren(); ++i ) {
@@ -299,15 +249,11 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i
 	}
 }
 Node TheoryStringsRewriter::rewriteMembership(TNode node) {
-	Node retNode;
+	Node retNode = node;
+	Node x = node[0];
 
-    //Trace("strings-postrewrite") << "Strings::rewriteMembership start " << node << std::endl;
-	
-	Node x;
 	if(node[0].getKind() == kind::STRING_CONCAT) {
 		x = rewriteConcatString(node[0]);
-	} else {
-		x = node[0];
 	}
 
 	if( x.getKind() == kind::CONST_STRING && checkConstRegExp(node[1]) ) {
@@ -315,26 +261,10 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
 		CVC4::String s = x.getConst<String>();
 		retNode = NodeManager::currentNM()->mkConst( testConstStringInRegExp( s, 0, node[1] ) );
 	} else {
-		//if( node[1].getKind() == kind::REGEXP_STAR ) {
-			if( x == node[0] ) {
-				retNode = node;
-			} else {
-				retNode = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, node[1] );
-			}
-		/*
-		} else {
-			std::vector<Node> node_vec;
-			simplifyRegExp( x, node[1], node_vec );
-
-			if(node_vec.size() > 1) {
-				retNode = NodeManager::currentNM()->mkNode(kind::AND, node_vec);
-			} else {
-				retNode = node_vec[0];
-			}
+		if( x != node[0] ) {
+			retNode = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, node[1] );
 		}
-		*/
 	}
-    //Trace("strings-prerewrite") << "Strings::rewriteMembership end " << retNode << std::endl;
     return retNode;
 }
 
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index c416abd69..e7d7eccb5 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -32,7 +32,6 @@ class TheoryStringsRewriter {
 public:
   static bool checkConstRegExp( TNode t );
   static bool testConstStringInRegExp( CVC4::String &s, unsigned int index_start, TNode r );
-  static void simplifyRegExp( Node s, Node r, std::vector< Node > &ret );
 
   static Node rewriteConcatString(TNode node);
   static Node prerewriteConcatRegExp(TNode node);
-- 
2.30.2