string contain changes

4 files changed, 111 insertions, 23 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 62e71327e..bb5e3718a 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -44,6 +44,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
 	//d_var_lmin( c ),
 	//d_var_lmax( c ),
 	d_reg_exp_mem( c ),
+	d_str_ctn( c ),
 	d_curr_cardinality( c, 0 )
 {
     // The kinds we are treating as function application in congruence
@@ -387,14 +388,13 @@ void TheoryStrings::check(Effort e) {
   bool polarity;
   TNode atom;
 
-  if( !done() && !hasTerm( d_emptyString ) ){
+  if( !done() && !hasTerm( d_emptyString ) ) {
 	 preRegisterTerm( d_emptyString );
   }
 
  // Trace("strings-process") << "Theory of strings, check : " << e << std::endl;
   Trace("strings-check") << "Theory of strings, check : " << e << std::endl;
-  while ( !done() && !d_conflict)
-  {
+  while ( !done() && !d_conflict ) {
     // Get all the assertions
     Assertion assertion = get();
     TNode fact = assertion.assertion;
@@ -406,7 +406,10 @@ void TheoryStrings::check(Effort e) {
 	//must record string in regular expressions
 	if ( atom.getKind() == kind::STRING_IN_REGEXP ) {
 		d_reg_exp_mem.push_back( assertion );
-	}else if (atom.getKind() == kind::EQUAL) {
+	} else if (atom.getKind() == kind::STRING_STRCTN) {
+		d_str_ctn.push_back( assertion );
+		d_equalityEngine.assertPredicate(atom, polarity, fact);
+    } else if (atom.getKind() == kind::EQUAL) {
 		d_equalityEngine.assertEquality(atom, polarity, fact);
     } else {
 		d_equalityEngine.assertPredicate(atom, polarity, fact);
@@ -417,24 +420,28 @@ void TheoryStrings::check(Effort e) {
 
   bool addedLemma = false;
   if( e == EFFORT_FULL && !d_conflict ) {
-      addedLemma = checkLengths();
-	  Trace("strings-process") << "Done check (constant) lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
-	  if( !addedLemma ){
-		  addedLemma = checkNormalForms();
-		  Trace("strings-process") << "Done check normal forms, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
-		  if(!d_conflict && !addedLemma) {
-			  addedLemma = checkLengthsEqc();
-			  Trace("strings-process") << "Done check lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
-			  if(!d_conflict && !addedLemma) {
-				  addedLemma = checkCardinality();
-				  Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
-				  if( !d_conflict && !addedLemma ){
+	addedLemma = checkLengths();
+	Trace("strings-process") << "Done check (constant) lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+	if( !addedLemma ) {
+		addedLemma = checkNormalForms();
+		Trace("strings-process") << "Done check normal forms, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+		if(!d_conflict && !addedLemma) {
+			addedLemma = checkLengthsEqc();
+			Trace("strings-process") << "Done check lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+			if(!d_conflict && !addedLemma) {
+				addedLemma = checkCardinality();
+				Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+				if( !d_conflict && !addedLemma ) {
 					addedLemma = checkMemberships();
 					Trace("strings-process") << "Done check membership constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
-				  }
-			  }
-		  }
-	  }
+					if( !d_conflict && !addedLemma ) {
+						addedLemma = checkInclusions();
+						Trace("strings-process") << "Done check inclusion constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+					}
+				}
+			}
+		}
+	}
   }
   Trace("strings-check") << "Theory of strings, done check : " << e << std::endl;
   Trace("strings-process") << "Theory of strings, done check : " << e << std::endl;
@@ -2077,6 +2084,80 @@ bool TheoryStrings::checkMemberships() {
 	}
 }
 
+bool TheoryStrings::checkInclusions() {
+	bool is_unk = false;
+	bool addedLemma = false;
+	for( unsigned i=0; i<d_str_ctn.size(); i++ ){
+		Node assertion = d_str_ctn[i];
+		Trace("strings-inc") << "We have inclusion assertion : " << assertion << std::endl;
+		Node atom = assertion.getKind()==kind::NOT ? assertion[0] : assertion;
+		bool polarity = assertion.getKind()!=kind::NOT;
+		if( polarity ) {
+			Assert( atom.getKind()==kind::STRING_STRCTN );
+			Node x = atom[0];
+			Node s = atom[1];
+			if( !areEqual( s, d_emptyString ) && !areEqual( s, x ) ) {
+				if(d_str_ctn_rewritten.find(atom) == d_str_ctn_rewritten.end()) {
+					// Add lemma
+					Node sk1 = NodeManager::currentNM()->mkSkolem( "sc1_$$", s.getType(), "created for inclusion" );
+					Node sk2 = NodeManager::currentNM()->mkSkolem( "sc2_$$", s.getType(), "created for inclusion" );
+					Node eq = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, s, sk2 ) ) );
+					sendLemma( assertion, eq, "inclusion" );
+					addedLemma = true;
+					d_str_ctn_rewritten[ atom ] = true;
+				} else {
+					Trace("strings-inc") << "... is already rewritten." << std::endl;
+				}
+			} else {
+				Trace("strings-inc") << "... is satisfied." << std::endl;
+			}
+		} else {
+			//TODO: negative inclusion
+			if( areEqual( atom[1], d_emptyString ) ) {
+				Node ant = NodeManager::currentNM()->mkNode( kind::AND, assertion, atom[1].eqNode( d_emptyString ) );
+				Node conc = Node::null();
+				sendLemma( ant, conc, "inclusion conflict 1" );
+				addedLemma = true;
+			} else if( areEqual( atom[1], atom[0] ) ) {
+				Node ant = NodeManager::currentNM()->mkNode( kind::AND, assertion, atom[1].eqNode( atom[0] ) );
+				Node conc = Node::null();
+				sendLemma( ant, conc, "inclusion conflict 2" );
+				addedLemma = true;
+			} else {
+				if(d_str_ctn_rewritten.find(assertion) == d_str_ctn_rewritten.end()) {
+					Node b1 = NodeManager::currentNM()->mkBoundVar( atom[0].getType() );
+					Node b2 = NodeManager::currentNM()->mkBoundVar( atom[0].getType() );
+					Node bvar = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, b1, b2 );
+					Node lena0 = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, atom[0] );
+					Node lena1 = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, atom[1] );
+					Node len_eq = Rewriter::rewrite( lena0.eqNode( NodeManager::currentNM()->mkNode( kind::PLUS, lena1,
+						NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, b1 ),
+						NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, b2 ) ) ) );
+					Node conc = NodeManager::currentNM()->mkNode( kind::FORALL, bvar,
+									NodeManager::currentNM()->mkNode( kind::IMPLIES, len_eq,
+									atom[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, b1, atom[1], b2 ) ).negate() )
+								);
+					d_str_ctn_rewritten[ assertion ] = true;
+					sendLemma( assertion, conc, "negative inclusion" );
+					addedLemma = true;
+				}
+				//Trace("strings-inc") << "Inclusion is incomplete due to " << assertion << "." << std::endl;
+				//is_unk = true;
+			}
+		}
+	}
+	if( addedLemma ){
+		doPendingLemmas();
+		return true;
+	} else {
+		if( is_unk ){
+			Trace("strings-inc") << "Strings::inc: possibly incomplete." << std::endl;
+			d_out->setIncomplete();
+		}
+		return false;
+	}
+}
+
 CVC4::String TheoryStrings::getHeadConst( Node x ) {
 	if( x.isConst() ) {
 		return x.getConst< String >();
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 875f407c5..62524ee14 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -216,6 +216,7 @@ private:
     bool checkCardinality();
     bool checkInductiveEquations();
 	bool checkMemberships();
+	bool checkInclusions();
 
 public:
 	void preRegisterTerm(TNode n);
@@ -269,6 +270,10 @@ private:
 	Node mkSplitEq( const char * c, const char * info, Node lhs, Node rhs, bool lgtZero );
 	int getMaxPossibleLength( Node x );
 
+	// Special String Functions
+	NodeList d_str_ctn;
+	std::map< Node, bool > d_str_ctn_rewritten;
+
 	// Regular Expression
 private:
 	// regular expression memberships
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 111c4f51d..08ebe7f10 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -136,7 +136,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 		} else {
 			throw LogicException("substring not supported in this release");
 		}
-	}  else if( t.getKind() == kind::STRING_STRCTN ){
+	}
+	/* else if( t.getKind() == kind::STRING_STRCTN ){
 		if(options::stringExp()) {
 			Node w = simplify( t[0], new_nodes );
 			Node y = simplify( t[1], new_nodes );
@@ -170,7 +171,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 		} else {
 			throw LogicException("string contain not supported in this release");
 		}
-	}  else if( t.getKind() == kind::STRING_CHARAT ){
+	} */
+	else if( t.getKind() == kind::STRING_CHARAT ){
 		if(options::stringExp()) {
 			Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1sym_$$", t.getType(), "created for charat" );
 			Node sk2 = NodeManager::currentNM()->mkSkolem( "ca2sym_$$", t.getType(), "created for charat" );
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index df1d2ebde..0d6c93719 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1152,7 +1152,7 @@ void EqualityEngine::addTriggerEquality(TNode eq) {
 
 void EqualityEngine::addTriggerPredicate(TNode predicate) {
   Assert(predicate.getKind() != kind::NOT && predicate.getKind() != kind::EQUAL);
-  Assert(d_congruenceKinds.tst(predicate.getKind()), "No point in adding non-congruence predicates");
+  //Assert(d_congruenceKinds.tst(predicate.getKind()), "No point in adding non-congruence predicates");
 
   if (d_done) {
     return;