string fmf changes

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 66cc2a434..b8f3f496f 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