From fd0a1cf8d0d6bf0c4d897d4d9f331c82c9743348 Mon Sep 17 00:00:00 2001
From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Thu, 21 Nov 2013 12:36:44 -0600
Subject: [PATCH] string fmf changes

---
 src/theory/strings/regexp_operation.cpp | 78 +++++++++++++++++++++++++
 src/theory/strings/regexp_operation.h   |  3 +
 src/theory/strings/theory_strings.cpp   | 50 +++++++++++-----
 src/theory/strings/theory_strings.h     |  5 +-
 4 files changed, 121 insertions(+), 15 deletions(-)

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index a3921bb42..f26037cf0 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -30,6 +30,14 @@ RegExpOpr::RegExpOpr() {
 	d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma );
 }
 
+int RegExpOpr::gcd ( int a, int b ) {
+  int c;
+  while ( a != 0 ) {
+     c = a; a = b%a;  b = c;
+  }
+  return b;
+}
+
 bool RegExpOpr::checkConstRegExp( Node r ) {
 	Trace("strings-regexp-cstre") << "RegExp-CheckConstRegExp starts with " << mkString( r ) << std::endl;
 	bool ret = true;
@@ -325,6 +333,76 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {
 	return retNode;
 }
 
+//TODO:
+bool RegExpOpr::guessLength( Node r, int &co ) {
+	int k = r.getKind();
+	switch( k ) {
+		case kind::STRING_TO_REGEXP:
+		{
+			if(r[0].isConst()) {
+				co += r[0].getConst< CVC4::String >().size();
+				return true;
+			} else {
+				return false;
+			}
+		}
+			break;
+		case kind::REGEXP_CONCAT:
+		{
+			for(unsigned i=0; i<r.getNumChildren(); ++i) {
+				if(!guessLength( r[i], co)) {
+					return false;
+				}
+			}
+			return true;
+		}
+			break;
+		case kind::REGEXP_OR:
+		{
+			int g_co;
+			for(unsigned i=0; i<r.getNumChildren(); ++i) {
+				int cop = 0;
+				if(!guessLength( r[i], cop)) {
+					return false;
+				}
+				if(i == 0) {
+					g_co = cop;
+				} else {
+					g_co = gcd(g_co, cop);
+				}
+			}
+			return true;
+		}
+			break;
+		case kind::REGEXP_INTER:
+		{
+			int g_co;
+			for(unsigned i=0; i<r.getNumChildren(); ++i) {
+				int cop = 0;
+				if(!guessLength( r[i], cop)) {
+					return false;
+				}
+				if(i == 0) {
+					g_co = cop;
+				} else {
+					g_co = gcd(g_co, cop);
+				}
+			}
+			return true;
+		}
+			break;
+		case kind::REGEXP_STAR:
+		{
+			co = 0;
+			return true;
+		}
+			break;
+		default:
+			Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in membership of RegExp." << std::endl;
+			return false;
+	}
+}
+
 void RegExpOpr::firstChar( Node r ) {
 	Trace("strings-regexp-firstchar") << "Head characters: ";
 	for(char ch = d_char_start; ch <= d_char_end; ++ch) {
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index 5f0eab2e0..702e5ba84 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -45,6 +45,8 @@ private:
 	//void simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn );
 	//Node simplify( Node t, std::vector< Node > &new_nodes );
 	std::string niceChar( Node r );
+	int gcd ( int a, int b );
+
 public:
 	RegExpOpr();
 	bool checkConstRegExp( Node r );
@@ -53,6 +55,7 @@ public:
 	Node complement( Node r );
 	int delta( Node r );
 	Node derivativeSingle( Node r, CVC4::String c );
+	bool guessLength( Node r, int &co );
 	void firstChar( Node r );
 	bool follow( Node r, CVC4::String c, std::vector< char > &vec_chars );
 	std::string mkString( Node r );
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index b7576659a..4e20ac248 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -57,6 +57,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
     d_false = NodeManager::currentNM()->mkConst( false );
 
 	d_regexp_incomplete = false;
+	d_opt_regexp_gcd = true;
 }
 
 TheoryStrings::~TheoryStrings() {
@@ -1818,14 +1819,6 @@ bool TheoryStrings::checkCardinality() {
   return false;
 }
 
-int TheoryStrings::gcd ( int a, int b ) {
-  int c;
-  while ( a != 0 ) {
-     c = a; a = b%a;  b = c;
-  }
-  return b;
-}
-
 void TheoryStrings::getEquivalenceClasses( std::vector< Node >& eqcs ) {
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
     while( !eqcs_i.isFinished() ) {
@@ -2009,6 +2002,14 @@ bool TheoryStrings::checkMemberships() {
 			Node r = atom[1];
 			Assert( r.getKind()==kind::REGEXP_STAR );
 			if( !areEqual( x, d_emptyString ) ) {
+				/*if(d_opt_regexp_gcd) {
+					if(d_membership_length.find(atom) == d_membership_length.end()) {
+						addedLemma = addMembershipLength(atom);
+						d_membership_length[atom] = true;
+					} else {
+						Trace("strings-regexp") << "Membership length is already added." << std::endl;
+					}
+				}*/
 				bool flag = true;
 				if( d_reg_exp_deriv.find(atom)==d_reg_exp_deriv.end() ) {
 					if(splitRegExp( x, r, atom )) {
@@ -2020,12 +2021,12 @@ bool TheoryStrings::checkMemberships() {
 					Trace("strings-regexp-derivative") << "... is processed by deriv." << std::endl;
 				}
 				if( flag && d_reg_exp_unroll.find(atom)==d_reg_exp_unroll.end() ) {
-						if( unrollStar( atom ) ) {
-							addedLemma = true;
-						} else {
-							Trace("strings-regexp") << "RegExp is incomplete due to " << assertion << ", depth = " << d_regexp_unroll_depth << std::endl;
-							is_unk = true;
-						}
+					if( unrollStar( atom ) ) {
+						addedLemma = true;
+					} else {
+						Trace("strings-regexp") << "RegExp is incomplete due to " << assertion << ", depth = " << d_regexp_unroll_depth << std::endl;
+						is_unk = true;
+					}
 				} else {
 					Trace("strings-regexp") << "...is already unrolled or splitted." << std::endl;
 				}
@@ -2097,6 +2098,27 @@ CVC4::String TheoryStrings::getHeadConst( Node x ) {
 	}
 }
 
+bool TheoryStrings::addMembershipLength(Node atom) {
+	Node x = atom[0];
+	Node r = atom[1];
+
+	/*std::vector< int > co;
+	co.push_back(0);
+	for(unsigned int k=0; k<lts.size(); ++k) {
+		if(lts[k].isConst() && lts[k].getType().isInteger()) {
+			int len = lts[k].getConst<Rational>().getNumerator().toUnsignedInt();
+			co[0] += cols[k].size() * len;
+		} else {
+			co.push_back( cols[k].size() );
+		}
+	}
+	int g_co = co[0];
+	for(unsigned k=1; k<co.size(); ++k) {
+		g_co = gcd(g_co, co[k]);
+	}*/
+	return false;
+}
+
 bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) {
 	// TODO cstr in vre
 	Assert(x != d_emptyString);
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 6ac8cf995..fb6599919 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -116,6 +116,7 @@ private:
     Node d_zero;
 	// Options
 	bool d_opt_fmf;
+	bool d_opt_regexp_gcd;
 	// Helper functions
 	Node getRepresentative( Node t );
 	bool hasTerm( Node a );
@@ -202,7 +203,6 @@ private:
     bool checkCardinality();
     bool checkInductiveEquations();
 	bool checkMemberships();
-	int gcd(int a, int b);
 
 public:
 	void preRegisterTerm(TNode n);
@@ -267,6 +267,8 @@ private:
 	bool d_regexp_incomplete;
 	int d_regexp_unroll_depth;
 	int d_regexp_max_depth;
+	// membership length
+	std::map< Node, bool > d_membership_length;
 	// regular expression derivative
 	std::map< Node, bool > d_reg_exp_deriv;
 	// regular expression operations
@@ -274,6 +276,7 @@ private:
 
 	CVC4::String getHeadConst( Node x );
 	bool splitRegExp( Node x, Node r, Node ant );
+	bool addMembershipLength(Node atom);
 
 
 	// Finite Model Finding
-- 
2.30.2