roll back to uf implementation for substr and charat

3 files changed, 25 insertions, 4 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 3209a92ec..2b1bb2b63 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -62,7 +62,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
     d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
     d_true = NodeManager::currentNM()->mkConst( true );
     d_false = NodeManager::currentNM()->mkConst( false );
-
+	
 	d_all_warning = true;
 	d_regexp_incomplete = false;
 	d_opt_regexp_gcd = true;
@@ -1709,6 +1709,21 @@ void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) {
 
 bool TheoryStrings::checkSimple() {
   bool addedLemma = false;
+
+  //Initialize UF
+  if(d_undefSubstr.isNull()) {
+	std::vector< TypeNode > argTypes;
+	argTypes.push_back(NodeManager::currentNM()->stringType());
+	argTypes.push_back(NodeManager::currentNM()->integerType());
+	argTypes.push_back(NodeManager::currentNM()->integerType());
+	d_undefSubstr = NodeManager::currentNM()->mkSkolem("__undefSS", 
+						NodeManager::currentNM()->mkFunctionType(
+							argTypes, NodeManager::currentNM()->stringType()),
+						"undefined substr",
+						NodeManager::SKOLEM_EXACT_NAME);
+  }
+
+
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
   while( !eqcs_i.isFinished() ) {
 	Node eqc = (*eqcs_i);
@@ -1760,7 +1775,8 @@ bool TheoryStrings::checkSimple() {
 								Node len_sk1_eq_i = n[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
 								Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 ));
 								Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i );
-								lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, lemma ) );
+								Node uf = sk.eqNode( NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_undefSubstr, n[0], n[1], d_one));
+								lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, lemma, uf) );
 								Trace("strings-lemma") << "Strings::Lemma CHARAT : " << lemma << std::endl;
 								d_out->lemma(lemma);
 							} else if( n.getKind() == kind::STRING_SUBSTR ) {
@@ -1778,7 +1794,8 @@ bool TheoryStrings::checkSimple() {
 
 								Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i );
 								Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
-								lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, lemma ) );
+								Node uf = sk.eqNode( NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_undefSubstr, n[0], n[1], n[2]));
+								lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, lemma, uf ) );
 								Trace("strings-lemma") << "Strings::Lemma SUBSTR : " << lemma << std::endl;
 								d_out->lemma(lemma);
 							}
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index d15a76aad..81748d607 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -115,6 +115,7 @@ private:
     Node d_false;
     Node d_zero;
 	Node d_one;
+	Node d_undefSubstr;
 	// Options
 	bool d_all_warning;
 	bool d_opt_fmf;
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 7bf016d29..1dc9cbe85 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -353,7 +353,10 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
             }
         }
     } else if(node.getKind() == kind::STRING_SUBSTR) {
-		if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) {
+		Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
+		if(node[2] == zero) {
+			retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
+		} else if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) {
 			int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
 			int j = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
 			if( node[0].getConst<String>().size() >= (unsigned) (i + j) ) {