From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Thu, 10 Oct 2013 17:06:25 +0000 (-0500)
Subject: adds native regexp.
X-Git-Tag: cvc5-1.0.0~7275^2~23^2~1^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8ed41bf909d1ed04a8c7a9bd3b5dfb302582ba28;p=cvc5.git

adds native regexp.
---

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index f303fd333..64425ea03 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -58,16 +58,6 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret
 				simplifyRegExp( s, r[i], ret );
 			}
 			break;
-		case kind::REGEXP_STAR:
-		{
-			Node sk = NodeManager::currentNM()->mkSkolem( "ressym_$$", s.getType(), "created for regular expression star" );
-			Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL,
-						NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, s ),
-						NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, s, sk ));
-			ret.push_back( eq );
-			simplifyRegExp( sk, r[0], ret );
-		}
-			break;
 		case kind::REGEXP_OPT:
 		{
 			Node eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, s, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) );
@@ -77,13 +67,27 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret
 			ret.push_back( NodeManager::currentNM()->mkNode( kind::OR, eq_empty, nrr) );
 		}
 			break;
+		//TODO:
+		case kind::REGEXP_STAR:
+		case kind::REGEXP_PLUS:
+			Assert( false );
+			break;
 		default:
-			//TODO:case kind::REGEXP_PLUS:
 			//TODO: special sym: sigma, none, all
 			break;
 	}
 }
 
+bool StringsPreprocess::checkStarPlus( Node t ) {
+	if( t.getKind() != kind::REGEXP_STAR && t.getKind() != kind::REGEXP_PLUS ) {
+		for( unsigned i = 0; i<t.getNumChildren(); ++i ) {
+			if( checkStarPlus(t[i]) ) return true;
+		}
+		return false;
+	} else {
+		return true;
+	}
+}
 
 Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
@@ -94,13 +98,19 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 	if( t.getKind() == kind::STRING_IN_REGEXP ){
 		// t0 in t1
 		Node t0 = simplify( t[0], new_nodes );
-		//rewrite it
-		std::vector< Node > ret;
-		simplifyRegExp( t0, t[1], ret );
+		
+		if(!checkStarPlus( t[1] )) {
+			//rewrite it
+			std::vector< Node > ret;
+			simplifyRegExp( t0, t[1], ret );
 
-		Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret );
-		d_cache[t] = (t == n) ? Node::null() : n;
-		return n;
+			Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret );
+			d_cache[t] = (t == n) ? Node::null() : n;
+			return n;
+		} else {
+			// TODO
+			return (t0 == t[0]) ? t : NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, t0, t[1] );
+		}
 	}else if( t.getKind() == kind::STRING_SUBSTR ){
 		Node sk1 = NodeManager::currentNM()->mkSkolem( "st1sym_$$", t.getType(), "created for substr" );
 		Node sk2 = NodeManager::currentNM()->mkSkolem( "st2sym_$$", t.getType(), "created for substr" );
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index d07249a02..ce00a75ce 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -31,6 +31,7 @@ class StringsPreprocess {
 	// NOTE: this class is NOT context-dependent
 	std::hash_map<TNode, Node, TNodeHashFunction> d_cache;
 private:
+	bool checkStarPlus( Node t );
 	void simplifyRegExp( Node s, Node r, std::vector< Node > &ret );
 	Node simplify( Node t, std::vector< Node > &new_nodes );
 public:
diff --git a/src/util/regexp.h b/src/util/regexp.h
index 58f58a40f..d4ad38b0f 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -28,81 +28,6 @@
 
 namespace CVC4 {
 
-class CVC4_PUBLIC Char {
-
-private:
-  unsigned int d_char;
-
-public:
-  Char() {}
-
-  Char(const unsigned int c)
-      : d_char(c) {}
-
-  ~Char() {}
-
-  Char& operator =(const Char& y) {
-    if(this != &y) d_char = y.d_char;
-    return *this;
-  }
-
-  bool operator ==(const Char& y) const {
-    return d_char == y.d_char ;
-  }
-
-  bool operator !=(const Char& y) const {
-    return d_char != y.d_char ;
-  }
-
-  bool operator <(const Char& y) const {
-    return d_char < y.d_char;
-  }
-
-  bool operator >(const Char& y) const {
-    return d_char > y.d_char ;
-  }
-
-  bool operator <=(const Char& y) const {
-    return d_char <= y.d_char;
-  }
-
-  bool operator >=(const Char& y) const {
-    return d_char >= y.d_char ;
-  }
-
-  /*
-   * Convenience functions
-   */
-  std::string toString() const {
-    std::string str = "1";
-    str[0] = (char) d_char;
-    return str;
-  }
-
-  unsigned size() const {
-    return 1;
-  }
-
-  const char* c_str() const {
-    return toString().c_str();
-  }
-};/* class Char */
-
-namespace strings {
-
-struct CharHashFunction {
-  size_t operator()(const ::CVC4::Char& c) const {
-    return __gnu_cxx::hash<const char*>()(c.toString().c_str());
-  }
-};/* struct CharHashFunction */
-
-}
-
-inline std::ostream& operator <<(std::ostream& os, const Char& c) CVC4_PUBLIC;
-inline std::ostream& operator <<(std::ostream& os, const Char& c) {
-  return os << "\"" << c.toString() << "\"";
-}
-
 class CVC4_PUBLIC String {
 
 private:
@@ -330,9 +255,6 @@ public:
     return d_str;
   }
 
-  unsigned size() const {
-    return d_str.size();
-  }
 };/* class String */
 
 /**