minor change: add a heuristic for preventing constant splitting.

2 files changed, 43 insertions, 21 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index f2172071d..d03faa72a 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -65,7 +65,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
 	d_curr_cardinality(c, 0)
 {
     // The kinds we are treating as function application in congruence
-    //d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
+    d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
     d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
     d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
     d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
@@ -418,7 +418,7 @@ void TheoryStrings::preRegisterTerm(TNode n) {
 		break;
 	case kind::STRING_IN_REGEXP:
 		//do not add trigger here
-		//d_equalityEngine.addTriggerPredicate(n);
+		d_equalityEngine.addTriggerPredicate(n);
 		break;
 	case kind::STRING_SUBSTR_TOTAL: {
 		Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, 
@@ -560,7 +560,7 @@ void TheoryStrings::check(Effort e) {
 	//must record string in regular expressions
 	if ( atom.getKind() == kind::STRING_IN_REGEXP ) {
 		addMembership(assertion);
-		//d_equalityEngine.assertPredicate(atom, polarity, fact);
+		d_equalityEngine.assertPredicate(atom, polarity, fact);
 	} else if (atom.getKind() == kind::STRING_STRCTN) {
 		if(polarity) {
 			d_str_pos_ctn.push_back( atom );
@@ -1232,18 +1232,37 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
 									Assert( other_str.getKind()!=kind::CONST_STRING, "Other string is not constant." );
 									Assert( other_str.getKind()!=kind::STRING_CONCAT, "Other string is not CONCAT." );
 									antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-									Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
-										NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
-									//split the string
-									Node eq1 = Rewriter::rewrite( other_str.eqNode( d_emptyString ) );
-									Node eq2 = mkSplitEq( "c_spt_$$", "created for v/c split", other_str, firstChar, false );
-									d_pending_req_phase[ eq1 ] = true;
-									conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
-									Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;
-
-									Node ant = mkExplain( antec );
-									sendLemma( ant, conc, "CST-SPLIT" );
-									++(d_statistics.d_eq_splits);
+									//Opt
+									bool optflag = false;
+									if( normal_forms[nconst_k].size() > nconst_index_k + 1 &&
+										normal_forms[nconst_k][nconst_index_k + 1].isConst() ) {
+										CVC4::String stra = const_str.getConst<String>();
+										CVC4::String strb = normal_forms[nconst_k][nconst_index_k + 1].getConst<String>();
+										CVC4::String fc = strb.substr(0, 1);
+										if( stra.find(fc) == std::string::npos ||
+											(stra.find(strb) == std::string::npos &&
+											 !stra.overlap(strb)) ) {
+											Node sk = NodeManager::currentNM()->mkSkolem( "sopt_$$", NodeManager::currentNM()->stringType(), "created for string sp" );
+											Node eq = other_str.eqNode( mkConcat(const_str, sk) );
+											Node ant = mkExplain( antec );
+											sendLemma(ant, eq, "CST-EPS");
+											optflag = true;
+										}
+									}
+									if(!optflag){
+										Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
+											NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
+										//split the string
+										Node eq1 = Rewriter::rewrite( other_str.eqNode( d_emptyString ) );
+										Node eq2 = mkSplitEq( "c_spt_$$", "created for v/c split", other_str, firstChar, false );
+										d_pending_req_phase[ eq1 ] = true;
+										conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
+										Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;
+
+										Node ant = mkExplain( antec );
+										sendLemma( ant, conc, "CST-SPLIT" );
+										++(d_statistics.d_eq_splits);
+									}
 									return true;
 								} else {
 									std::vector< Node > antec_new_lits;
@@ -1785,10 +1804,7 @@ void TheoryStrings::sendSplit( Node a, Node b, const char * c, bool preq ) {
 }
 
 Node TheoryStrings::mkConcat( Node n1, Node n2 ) {
-	std::vector< Node > c;
-	c.push_back( n1 );
-	c.push_back( n2 );
-	return mkConcat( c );
+	return NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2 );
 }
 
 Node TheoryStrings::mkConcat( std::vector< Node >& c ) {
@@ -2888,6 +2904,11 @@ void TheoryStrings::addMembership(Node assertion) {
 	d_regexp_memberships.push_back( assertion );
 }
 
+Node TheoryStrings::instantiateSymRegExp(Node r) {
+	//TODO:
+	return r;
+}
+
 //// Finite Model Finding
 
 Node TheoryStrings::getNextDecisionRequest() {
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 9f99012df..33283d1cf 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -272,8 +272,8 @@ protected:
 	void sendInfer( Node eq_exp, Node eq, const char * c );
 	void sendSplit( Node a, Node b, const char * c, bool preq = true );
 	/** mkConcat **/
-	Node mkConcat( Node n1, Node n2 );
-	Node mkConcat( std::vector< Node >& c );
+	inline Node mkConcat( Node n1, Node n2 );
+	inline Node mkConcat( std::vector< Node >& c );
 	/** mkExplain **/
 	Node mkExplain( std::vector< Node >& a );
 	Node mkExplain( std::vector< Node >& a, std::vector< Node >& an );
@@ -323,6 +323,7 @@ private:
 	bool splitRegExp( Node x, Node r, Node ant );
 	bool addMembershipLength(Node atom);
 	void addMembership(Node assertion);
+	Node instantiateSymRegExp(Node r);
 
 
 	// Finite Model Finding