reorganize substr, fix some potential bugs, adds cache for preprocessing

5 files changed, 116 insertions, 66 deletions

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index e7079081b..3b81ae4a5 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -645,6 +645,79 @@ Node RegExpOpr::complement( Node r ) {
 	return retNode;

 }

 

+//simplify

+void RegExpOpr::simplify(Node t, std::vector< Node > &new_nodes) {

+	Assert(t.getKind() == kind::STRING_IN_REGEXP);

+	Node str = Rewriter::rewrite(t[0]);

+	Node re  = Rewriter::rewrite(t[1]);

+	simplifyRegExp( str, re, new_nodes );

+}

+void RegExpOpr::simplifyRegExp( Node s, Node r, std::vector< Node > &new_nodes ) {

+	std::pair < Node, Node > p(s, r);

+	std::map < std::pair< Node, Node >, Node >::const_iterator itr = d_simpl_cache.find(p);

+	if(itr != d_simpl_cache.end()) {

+		new_nodes.push_back( itr->second );

+		return;

+	} else {

+		int k = r.getKind();

+		switch( k ) {

+			case kind::STRING_TO_REGEXP:

+			{

+				Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, r[0] );

+				new_nodes.push_back( eq );

+				d_simpl_cache[p] = eq;

+			}

+				break;

+			case kind::REGEXP_CONCAT:

+			{

+				std::vector< Node > cc;

+				for(unsigned i=0; i<r.getNumChildren(); ++i) {

+					if(r[i].getKind() == kind::STRING_TO_REGEXP) {

+						cc.push_back( r[i][0] );

+					} else {

+						Node sk = NodeManager::currentNM()->mkSkolem( "rcon_$$", s.getType(), "created for regular expression concat" );

+						simplifyRegExp( sk, r[i], new_nodes );

+						cc.push_back( sk );

+					}

+				}

+				Node cc_eq = s.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, cc) );

+				new_nodes.push_back( cc_eq );

+				d_simpl_cache[p] = 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 );

+				new_nodes.push_back( eq );

+				d_simpl_cache[p] = eq;

+			}

+				break;

+			case kind::REGEXP_INTER:

+				for(unsigned i=0; i<r.getNumChildren(); ++i) {

+					simplifyRegExp( s, r[i], new_nodes );

+				}

+				break;

+			case kind::REGEXP_STAR:

+			{

+				Node eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r );

+				new_nodes.push_back( eq );

+				d_simpl_cache[p] = eq;

+			}

+				break;

+			default:

+				//TODO: special sym: sigma, none, all

+				Trace("strings-preprocess") << "Unsupported term: " << r << " in simplifyRegExp." << std::endl;

+				Assert( false );

+				break;

+		}

+	}

+}

+

+//printing

 std::string RegExpOpr::niceChar( Node r ) {

 	if(r.isConst()) {

 		std::string s = r.getConst<CVC4::String>().toString() ;

diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index 9ed4be0c3..d7dde018a 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -37,20 +37,20 @@ private:
 	Node d_sigma;

 	Node d_sigma_star;

 	

+	std::map< std::pair< Node, Node >, Node > d_simpl_cache;

 	std::map< Node, Node > d_compl_cache;

 	std::map< Node, int > d_delta_cache;

 	std::map< PairDvStr, Node > d_dv_cache;

 	std::map< Node, bool > d_cstre_cache;

 	//bool checkStarPlus( Node t );

-	//void simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn );

-	//Node simplify( Node t, std::vector< Node > &new_nodes );

+	void simplifyRegExp( Node s, Node r, std::vector< Node > &new_nodes );

 	std::string niceChar( Node r );

 	int gcd ( int a, int b );

 

 public:

 	RegExpOpr();

 	bool checkConstRegExp( Node r );

-    //void simplify(std::vector< Node > &vec_node);

+    void simplify(Node t, std::vector< Node > &new_nodes);

 	Node mkAllExceptOne( char c );

 	Node complement( Node r );

 	int delta( Node r );

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 3c9f5902e..ba36aa371 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -46,7 +46,6 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
 	//d_var_lmax( c ),
 	d_str_pos_ctn( c ),
 	d_str_neg_ctn( c ),
-	d_int_to_str( c ),
 	d_reg_exp_mem( c ),
 	d_curr_cardinality( c, 0 )
 {
@@ -286,6 +285,7 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
 		}
 	}
 	////step 2 : assign arbitrary values for unknown lengths?
+	// confirmed by calculus invariant, see paper
 	//for( unsigned i=0; i<col.size(); i++ ){
 	//	if(
 	//}
@@ -404,15 +404,29 @@ void TheoryStrings::preRegisterTerm(TNode n) {
 	//do not add trigger here
     //d_equalityEngine.addTriggerPredicate(n);
     break;
-  case kind::CONST_STRING:
-  case kind::STRING_CONCAT:
   case kind::STRING_SUBSTR_TOTAL:
-  case kind::STRING_ITOS:
-  case kind::STRING_STOI:
-	d_equalityEngine.addTerm(n);
-	break;
+	{
+		Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, 
+							NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ),
+							NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) );
+		Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], d_zero);
+		Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[2], d_zero);
+		Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
+		Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
+		Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
+		d_statistics.d_new_skolems += 2;
+		Node x_eq_123 = n[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, n, sk3 ) );
+		Node len_sk1_eq_i = n[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
+		Node lenc = n[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n ) );
+		Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, 
+			NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, lenc ),
+			n.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") )) ) );
+		Trace("strings-lemma") << "Strings::Lemma SUBSTR : " << lemma << std::endl;
+		d_out->lemma(lemma);
+	}
+	//d_equalityEngine.addTerm(n);
   default:
-    if(n.getType().isString() ) {
+    if(n.getType().isString() && n.getKind()!=kind::STRING_CONCAT && n.getKind()!=kind::CONST_STRING ) {
 	  if( std::find( d_length_intro_vars.begin(), d_length_intro_vars.end(), n )==d_length_intro_vars.end() ) {
 		  Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
 		  Node n_len_eq_z = n_len.eqNode( d_zero );
@@ -1762,8 +1776,7 @@ bool TheoryStrings::checkSimple() {
 			//if n is concat, and
 			//if n has not instantiatied the concat..length axiom
 			//then, add lemma
-			if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT 
-				|| n.getKind() == kind::STRING_SUBSTR_TOTAL ) {
+			if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) {
 				if( d_length_nodes.find(n)==d_length_nodes.end() ) {
 					if( d_length_inst.find(n)==d_length_inst.end() ) {
 						//Node nr = d_equalityEngine.getRepresentative( n );
@@ -1790,25 +1803,6 @@ bool TheoryStrings::checkSimple() {
 							} else if( n.getKind() == kind::CONST_STRING ) {
 								//add lemma
 								lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
-							} else if( n.getKind() == kind::STRING_SUBSTR_TOTAL ) {
-								Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
-													NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ),
-													NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) );
-								Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], d_zero);
-								Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[2], d_zero);
-								Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
-								lsum = NodeManager::currentNM()->mkNode( kind::ITE, cond, n[2], d_zero );
-								/*
-								Node sk1 = NodeManager::currentNM()->mkSkolem( "st1_$$", NodeManager::currentNM()->stringType(), "created for substr" );
-								Node sk3 = NodeManager::currentNM()->mkSkolem( "st3_$$", NodeManager::currentNM()->stringType(), "created for substr" );
-								d_statistics.d_new_skolems += 2;
-								Node x_eq_123 = n[0].eqNode(NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk, sk3 ));
-								Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, n[1],
-														NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
-								Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i );
-								lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, lemma ) );
-								Trace("strings-lemma") << "Strings::Lemma SUBSTR : " << lemma << std::endl;
-								d_out->lemma(lemma);*/
 							}
 							Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
 							ceq = Rewriter::rewrite(ceq);
@@ -2240,21 +2234,14 @@ bool TheoryStrings::unrollStar( Node atom ) {
 			cc.push_back(unr0);
 		} else {
 			std::vector< Node > urc;
-			urc.push_back( unr1 );
-
-			StringsPreprocess spp;
-			spp.simplify( urc );
-			for( unsigned i=1; i<urc.size(); i++ ){
-				//add the others as lemmas
-				sendLemma( d_true, urc[i], "RegExp Definition");
-			}
+			d_regexp_opr.simplify(unr1, urc);
 			Node unr0 = sk_s.eqNode( d_emptyString ).negate();
-			cc.push_back(unr0);	cc.push_back(urc[0]);
+			cc.push_back(unr0);	//cc.push_back(urc1);
+			cc.insert(cc.end(), urc.begin(), urc.end());
 		}
 
 		Node unr2 = x.eqNode( mkConcat( sk_s, sk_xp ) );
 		Node unr3 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_xp, r );
-		unr3 = Rewriter::rewrite( unr3 );
 		d_reg_exp_unroll_depth[unr3] = depth + 1;
 		if( d_reg_exp_ant.find( atom )!=d_reg_exp_ant.end() ){
 			d_reg_exp_ant[unr3] = d_reg_exp_ant[atom];
@@ -2575,15 +2562,6 @@ bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) {
 		// send lemma
 		if(flag) {
 			if(x.isConst()) {
-				/*
-				left = d_emptyString;
-				if(d_regexp_opr.delta(dc) == 1) {
-					//TODO yes possible?
-				} else if(d_regexp_opr.delta(dc) == 0) {
-					//TODO possible?
-				} else {
-					// TODO conflict possible?
-				}*/
 				Assert(false, "Impossible: TheoryStrings::splitRegExp: const string in const regular expression.");
 				return false;
 			} else {
@@ -2597,16 +2575,12 @@ bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) {
 				conc = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, left, dc );
 
 				std::vector< Node > sdc;
-				sdc.push_back( conc );
-
-				StringsPreprocess spp;
-				spp.simplify( sdc );
-				for( unsigned i=1; i<sdc.size(); i++ ){
-					//add the others as lemmas
-					sendLemma( d_true, sdc[i], "RegExp-DEF");
+				d_regexp_opr.simplify(conc, sdc);
+				if(sdc.size() == 1) {
+					conc = sdc[0];
+				} else {
+					conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, conc));
 				}
-
-				conc = sdc[0];
 			}
 		}
 		sendLemma(ant, conc, "RegExp-CST-SP");
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 87cc3330a..ea92865b2 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -290,12 +290,10 @@ private:
 	// Special String Functions
 	NodeList d_str_pos_ctn;
 	NodeList d_str_neg_ctn;
-	NodeList d_int_to_str;
 	std::map< Node, bool > d_str_ctn_eqlen;
 	std::map< Node, bool > d_str_neg_ctn_ulen;
 	std::map< Node, bool > d_str_pos_ctn_rewritten;
 	std::map< Node, bool > d_str_neg_ctn_rewritten;
-	std::map< std::pair <Node, int>, bool > d_int_to_str_rewritten;
 
 	// Regular Expression
 private:
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index ca4a4e75e..964f5d8e1 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -227,7 +227,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 			d_cache[t] = skk;
 			retNode = skk;
 		} else {
-			throw LogicException("string indexof not supported in this release");
+			throw LogicException("string indexof not supported in default mode, try --string-exp");
 		}
 	} else if( t.getKind() == kind::STRING_ITOS ) {
 		if(options::stringExp()) {
@@ -333,7 +333,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 			d_cache[t] = t;
 			retNode = t;
 		} else {
-			throw LogicException("string int.to.str not supported in this release");
+			throw LogicException("string int.to.str not supported in default mode, try --string-exp");
 		}
 	} else if( t.getKind() == kind::STRING_STOI ) {
 		if(options::stringExp()) {
@@ -463,7 +463,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 			d_cache[t] = t;
 			retNode = t;
 		} else {
-			throw LogicException("string int.to.str not supported in this release");
+			throw LogicException("string int.to.str not supported in default mode, try --string-exp");
 		}
 	} else if( t.getKind() == kind::STRING_STRREPL ) {
 		if(options::stringExp()) {
@@ -485,7 +485,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 			d_cache[t] = skw;
 			retNode = skw;
 		} else {
-			throw LogicException("string replace not supported in this release");
+			throw LogicException("string replace not supported in default mode, try --string-exp");
 		}
 	} else{
 		d_cache[t] = Node::null();
@@ -525,6 +525,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 }
 
 Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes) {
+    std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
+    if(i != d_cache.end()) {
+      return (*i).second.isNull() ? t : (*i).second;
+    }
+
 	unsigned num = t.getNumChildren();
 	if(num == 0) {
 		return simplify(t, new_nodes);