From 3ed865aa12a94e935038d70b130701045b84a8b8 Mon Sep 17 00:00:00 2001
From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Mon, 10 Mar 2014 17:30:18 -0500
Subject: [PATCH] adds intro vars length cache

---
 src/theory/strings/theory_strings.cpp | 28 +++++++++++++++------------
 src/theory/strings/theory_strings.h   |  3 ++-
 2 files changed, 18 insertions(+), 13 deletions(-)

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 64f3cd578..448b94fd2 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -42,6 +42,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
     d_infer_exp(c),
     d_nf_pairs(c),
 	d_loop_antec(u),
+	d_length_intro_vars(u),
 	d_length_inst(u),
 	d_length_nodes(c),
 	d_str_pos_ctn(c),
@@ -50,7 +51,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
 	d_neg_ctn_ulen(u),
 	d_pos_ctn_cached(u),
 	d_neg_ctn_cached(u),
-	d_reg_exp_mem(c),
+	d_regexp_memberships(c),
 	d_regexp_ucached(u),
 	d_regexp_ccached(c),
 	d_regexp_ant(c),
@@ -432,14 +433,16 @@ void TheoryStrings::preRegisterTerm(TNode n) {
 	}
 	default: {
 		if(n.getType().isString() && n.getKind()!=kind::STRING_CONCAT && n.getKind()!=kind::CONST_STRING ) {
-		  Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
-		  Node n_len_eq_z = n.eqNode(d_emptyString); //n_len.eqNode( d_zero );
-		  n_len_eq_z = Rewriter::rewrite( n_len_eq_z );
-		  Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, n_len_eq_z,
-									NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
-		  Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl;
-		  d_out->lemma(n_len_geq_zero);
-		  d_out->requirePhase( n_len_eq_z, true );
+		  if( d_length_intro_vars.find(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 );
+			  n_len_eq_z = Rewriter::rewrite( n_len_eq_z );
+			  Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, n_len_eq_z,
+										NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
+			  Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl;
+			  d_out->lemma(n_len_geq_zero);
+			  d_out->requirePhase( n_len_eq_z, true );
+		  }
 		  // FMF
 		  if( n.getKind() == kind::VARIABLE && options::stringFMF() ) {
 			  d_input_vars.insert(n);
@@ -485,7 +488,7 @@ void TheoryStrings::check(Effort e) {
     atom = polarity ? fact : fact[0];
 	//must record string in regular expressions
 	if ( atom.getKind() == kind::STRING_IN_REGEXP ) {
-		d_reg_exp_mem.push_back( assertion );
+		d_regexp_memberships.push_back( assertion );
 		//d_equalityEngine.assertPredicate(atom, polarity, fact);
 	} else if (atom.getKind() == kind::STRING_STRCTN) {
 		if(polarity) {
@@ -1792,6 +1795,7 @@ bool TheoryStrings::checkSimple() {
 							Trace("strings-debug") << "get n: " << n << endl;
 							Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for length" );
 							d_statistics.d_new_skolems += 1;
+							d_length_intro_vars.insert( sk );
 							Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n );
 							eq = Rewriter::rewrite(eq);
 							Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl;
@@ -2229,9 +2233,9 @@ bool TheoryStrings::checkMemberships() {
 	bool addedLemma = false;
 	std::vector< Node > processed;
 	std::vector< Node > cprocessed;
-	for( unsigned i=0; i<d_reg_exp_mem.size(); i++ ){
+	for( unsigned i=0; i<d_regexp_memberships.size(); i++ ){
 		//check regular expression membership
-		Node assertion = d_reg_exp_mem[i];
+		Node assertion = d_regexp_memberships[i];
 		if( d_regexp_ucached.find(assertion) == d_regexp_ucached.end() 
 			&& d_regexp_ccached.find(assertion) == d_regexp_ccached.end() ) {
 			Trace("strings-regexp") << "We have regular expression assertion : " << assertion << std::endl;
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index cbfa481c3..c8a374893 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -156,6 +156,7 @@ private:
 	bool isNormalFormPair2( Node n1, Node n2 );
 	// loop ant
 	NodeSet d_loop_antec;
+	NodeSet d_length_intro_vars;
 
 	/////////////////////////////////////////////////////////////////////////////
 	// MODEL GENERATION
@@ -295,7 +296,7 @@ private:
 	// Regular Expression
 private:
 	// regular expression memberships
-	NodeList d_reg_exp_mem;
+	NodeList d_regexp_memberships;
 	NodeSet d_regexp_ucached;
 	NodeSet d_regexp_ccached;
 	// antecedant for why regexp membership must be true
-- 
2.30.2