replace charat uf with internal one

5 files changed, 37 insertions, 80 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index effbbca2e..4deb0a9d9 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -44,7 +44,6 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
 	d_length_nodes(c),
 	//d_var_lmin( c ),
 	//d_var_lmax( c ),
-	d_charAtUF(),
 	d_str_pos_ctn( c ),
 	d_str_neg_ctn( c ),
 	d_reg_exp_mem( c ),
@@ -55,10 +54,11 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
     d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
     d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
     d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
-    //d_equalityEngine.addFunctionKind(kind::STRING_CHARAT_TOTAL);
+    d_equalityEngine.addFunctionKind(kind::STRING_CHARAT_TOTAL);
     //d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL);
 
     d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
+    d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
     d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
     d_true = NodeManager::currentNM()->mkConst( true );
     d_false = NodeManager::currentNM()->mkConst( false );
@@ -384,13 +384,19 @@ void TheoryStrings::preRegisterTerm(TNode n) {
   default:
     if(n.getType().isString() && n.getKind() != kind::CONST_STRING && n.getKind()!=kind::STRING_CONCAT ) {
 	  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 );
-		  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(n.getKind() == kind::STRING_CHARAT_TOTAL) {
+			  Node lenc_eq_one = d_one.eqNode(NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n));
+			  Trace("strings-lemma") << "Strings::Lemma LEN(CHAR) = 1 : " << lenc_eq_one << std::endl;
+			  d_out->lemma(lenc_eq_one);
+		  } else {
+			  Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
+			  Node n_len_eq_z = n_len.eqNode( d_zero );
+			  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() && 
@@ -469,14 +475,14 @@ void TheoryStrings::check(Effort e) {
 			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;
+				addedLemma = checkContains();
+				Trace("strings-process") << "Done check contain constraints, 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 = checkContains();
-						Trace("strings-process") << "Done check contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+						addedLemma = checkCardinality();
+						Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
 					}
 				}
 			}
@@ -994,12 +1000,11 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
 				bool success;
 				do
 				{
-					//---------------------do simple stuff first
+					//simple check
 					if( processSimpleNEq( normal_forms, normal_form_src, curr_exp, i, j, index_i, index_j, false ) ){
 						//added a lemma, return
 						return true;
 					}
-					//----------------------
 
 					success = false;
 					//if we are at the end
@@ -1097,11 +1102,6 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
 										}
 									}
 
-									//Node sk = NodeManager::currentNM()->mkSkolem( "v_spt_$$", normal_forms[i][index_i].getType(), "created for v/v split" );
-									//Node eq1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i],
-									//			NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) ) );
-									//Node eq2 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j],
-									//			NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) ) );
 									Node eq1 = mkSplitEq( "v_spt_l_$$", "created for v/v split", normal_forms[i][index_i], normal_forms[j][index_j], true );
 									Node eq2 = mkSplitEq( "v_spt_r_$$", "created for v/v split", normal_forms[j][index_j], normal_forms[i][index_i], true );
 									conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
@@ -1358,10 +1358,10 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) {
 		std::vector< Node > nfj;
 		nfj.insert( nfj.end(), d_normal_forms[nj].begin(), d_normal_forms[nj].end() );
 
-		//int revRet = processReverseDeq( nfi, nfj, ni, nj );
-		//if( revRet!=0 ){
-		//	return revRet==-1;
-		//}
+		int revRet = processReverseDeq( nfi, nfj, ni, nj );
+		if( revRet!=0 ){
+			return revRet==-1;
+		}
 		
 		nfi.clear();
 		nfi.insert( nfi.end(), d_normal_forms[ni].begin(), d_normal_forms[ni].end() );
@@ -2366,19 +2366,8 @@ bool TheoryStrings::checkNegContains() {
 							Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ),
 										NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::MINUS, lenx, lens ), b1 ) ) );
 							Node b2 = NodeManager::currentNM()->mkBoundVar("bj", NodeManager::currentNM()->integerType());
-							if(d_charAtUF.isNull()) {
-								std::vector< TypeNode > argTypes;
-								argTypes.push_back(NodeManager::currentNM()->stringType());
-								argTypes.push_back(NodeManager::currentNM()->integerType());
-								d_charAtUF = NodeManager::currentNM()->mkSkolem("charAt", 
-												NodeManager::currentNM()->mkFunctionType(
-												argTypes,
-												NodeManager::currentNM()->stringType()),
-												"total charat",
-												NodeManager::SKOLEM_EXACT_NAME);
-							}
-							Node s2 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ));
-							Node s5 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, s, b2);
+							Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT_TOTAL, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ));
+							Node s5 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT_TOTAL, s, b2);
 
 							Node s1 = NodeManager::currentNM()->mkBoundVar("s1", NodeManager::currentNM()->stringType());
 							Node s3 = NodeManager::currentNM()->mkBoundVar("s3", NodeManager::currentNM()->stringType());
@@ -2398,10 +2387,6 @@ bool TheoryStrings::checkNegContains() {
 							vec_nodes.push_back(cc);
 							cc = s2.eqNode(s5).negate();
 							vec_nodes.push_back(cc);
-							cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s2).eqNode(NodeManager::currentNM()->mkConst( Rational(1)));
-							vec_nodes.push_back(cc);
-							cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s5).eqNode(NodeManager::currentNM()->mkConst( Rational(1)));
-							vec_nodes.push_back(cc);
 							cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s1).eqNode(NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ));
 							vec_nodes.push_back(cc);
 							cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s4).eqNode(b2);
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 1f69c81be..1dae73360 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -114,6 +114,7 @@ private:
     Node d_true;
     Node d_false;
     Node d_zero;
+	Node d_one;
 	// Options
 	bool d_all_warning;
 	bool d_opt_fmf;
@@ -286,7 +287,6 @@ private:
 	int getMaxPossibleLength( Node x );
 
 	// Special String Functions
-	Node d_charAtUF;
 	NodeList d_str_pos_ctn;
 	NodeList d_str_neg_ctn;
 	std::map< Node, bool > d_str_ctn_eqlen;
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 11642a4d2..00d02e015 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -27,12 +27,6 @@ StringsPreprocess::StringsPreprocess() {
 	std::vector< TypeNode > argTypes;
 	argTypes.push_back(NodeManager::currentNM()->stringType());
 	argTypes.push_back(NodeManager::currentNM()->integerType());
-	d_charAtUF = NodeManager::currentNM()->mkSkolem("charAt", 
-						NodeManager::currentNM()->mkFunctionType(
-							argTypes,
-							NodeManager::currentNM()->stringType()),
-						"total charat",
-						NodeManager::SKOLEM_EXACT_NAME);
 }
 
 void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn ) {
@@ -137,14 +131,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 		int v_id = 1 - c_id;
 		int len = t[c_id].getConst<Rational>().getNumerator().toUnsignedInt();
 		if(len > 1) {
-			Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
 			std::vector< Node > vec;
 			for(int i=0; i<len; i++) {
 				Node num = NodeManager::currentNM()->mkConst( ::CVC4::Rational(i) );
-				Node sk = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, t[v_id][0], num);
+				Node sk = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT_TOTAL, t[v_id][0], num);
 				vec.push_back(sk);
-				Node lem = one.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ) );
-				new_nodes.push_back( lem );
 			}
 			Node lem = t[v_id][0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, vec ) );
 			lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, t, lem );
@@ -191,26 +182,6 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 
 		d_cache[t] = sk2;
 		retNode = sk2;
-	} else if( t.getKind() == kind::STRING_CHARAT_TOTAL ){
-		Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", NodeManager::currentNM()->stringType(), "created for charat" );
-		Node sk2 = NodeManager::currentNM()->mkSkolem( "ca2_$$", NodeManager::currentNM()->stringType(), "created for charat" );
-		Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", NodeManager::currentNM()->stringType(), "created for charat" );
-		Node x = simplify( t[0], new_nodes );
-		Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, 
-							NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ), t[1] );
-		Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL,
-							NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x );
-		Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1],
-								NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
-		Node len_sk2_eq_1 = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkConst( Rational( 1 ) ),
-								NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) );
-
-		Node tp = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, len_sk2_eq_1 );
-		tp = NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, tp );
-		new_nodes.push_back( tp );
-
-		d_cache[t] = sk2;
-		retNode = sk2;
 	} else if( t.getKind() == kind::STRING_STRIDOF ){
 		if(options::stringExp()) {
 			Node sk1 = NodeManager::currentNM()->mkSkolem( "io1_$$", t[0].getType(), "created for indexof" );
@@ -278,7 +249,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 			throw LogicException("string replace not supported in this release");
 		}
 	} else if(t.getKind() == kind::STRING_CHARAT) {
-		Node sk2 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, t[0], t[1]);
+		Node sk2 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT_TOTAL, t[0], t[1]);
 		Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", NodeManager::currentNM()->stringType(), "created for charat" );
 		Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", NodeManager::currentNM()->stringType(), "created for charat" );
 		Node x = simplify( t[0], new_nodes );
@@ -288,16 +259,12 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 		Node len_sk1_eq_i = t[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
 		Node tp = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i );
 		tp = NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, tp );
-		Node len_sk2_eq_1 = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkConst( Rational( 1 ) ),
-								NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) );
-		tp = NodeManager::currentNM()->mkNode( kind::AND, len_sk2_eq_1, tp );
-
 		new_nodes.push_back( tp );
 
 		d_cache[t] = sk2;
 		retNode = sk2;
 	} else if(t.getKind() == kind::STRING_SUBSTR) {
-		InternalError("CharAt and Substr should not be reached here.");
+		InternalError("Substr should not be reached here.");
 	} else if( t.getNumChildren()>0 ) {
 		std::vector< Node > cc;
 		if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 27808f0b2..99312ddc0 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -31,7 +31,6 @@ namespace strings {
 class StringsPreprocess {
 	// NOTE: this class is NOT context-dependent
 	std::hash_map<TNode, Node, TNodeHashFunction> d_cache;
-	Node d_charAtUF;
 private:
 	bool checkStarPlus( Node t );
 	int checkFixLenVar( Node t );
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 78731d469..86af2ffa8 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -323,16 +323,22 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
     } else if(node.getKind() == kind::STRING_LENGTH) {
         if(node[0].isConst()) {
             retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst<String>().size() ) );
+        } else if(node[0].getKind() == kind::STRING_CHARAT_TOTAL) {
+            retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) );
         } else if(node[0].getKind() == kind::STRING_CONCAT) {
             Node tmpNode = rewriteConcatString(node[0]);
             if(tmpNode.isConst()) {
                 retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode.getConst<String>().size() ) );
+            } else if(tmpNode.getKind() == kind::STRING_CHARAT_TOTAL) {
+				retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) );
             } else {
                 // it has to be string concat
                 std::vector<Node> node_vec;
                 for(unsigned int i=0; i<tmpNode.getNumChildren(); ++i) {
                     if(tmpNode[i].isConst()) {
                         node_vec.push_back( NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode[i].getConst<String>().size() ) ) );
+					} else if(tmpNode[i].getKind() == kind::STRING_CHARAT_TOTAL) {
+                        node_vec.push_back( NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) ) );
                     } else {
                         node_vec.push_back( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, tmpNode[i]) );
                     }
@@ -360,7 +366,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
 				retNode = NodeManager::currentNM()->mkConst( false );
 			}
 		}
-	} else if(node.getKind() == kind::STRING_CHARAT) {
+	} else if(node.getKind() == kind::STRING_CHARAT || node.getKind() == kind::STRING_CHARAT_TOTAL) {
 		if( node[0].isConst() && node[1].isConst() ) {
 			int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
 			if( node[0].getConst<String>().size() > (unsigned) i ) {