add constant replace, indexof

5 files changed, 111 insertions, 29 deletions

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index a421d6fa8..9e0897c00 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -15,7 +15,9 @@ operator STRING_IN_REGEXP 2 "membership"
 operator STRING_LENGTH 1 "string length"
 operator STRING_SUBSTR 3 "string substr"
 operator STRING_STRCTN 2 "string contains"
-operator STRING_CHARAT 2 "string char at"
+operator STRING_CHARAT 2 "string charat"
+operator STRING_STRIDOF 3 "string indexof"
+operator STRING_STRREPL 3 "string replace"
 
 #sort CHAR_TYPE \
 #    Cardinality::INTEGERS \
@@ -105,6 +107,8 @@ typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule
 typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule
 typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule
 typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule
+typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule
+typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule
 
 typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule
 
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index ddc729e1e..c667aedf0 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2036,33 +2036,18 @@ bool TheoryStrings::checkMemberships() {
 			}
 		} else {
 			//TODO: negative membership
-			//Node r = Rewriter::rewrite( atom[1] );
-			//r = d_regexp_opr.complement( r );
-			//Trace("strings-regexp-test") << "Compl( " << d_regexp_opr.mkString( atom[1] ) << " ) is " << d_regexp_opr.mkString( r ) << std::endl;
-			//Trace("strings-regexp-test") << "Delta( " << d_regexp_opr.mkString( atom[1] ) << " ) is " << d_regexp_opr.delta( atom[1] ) << std::endl;
-			//Trace("strings-regexp-test") << "Delta( " << d_regexp_opr.mkString( r ) << " ) is " << d_regexp_opr.delta( r ) << std::endl;
-			//Trace("strings-regexp-test") << "Deriv( " << d_regexp_opr.mkString( r ) << ", c='b' ) is " << d_regexp_opr.mkString( d_regexp_opr.derivativeSingle( r, ::CVC4::String("b") ) ) << std::endl;
-			//Trace("strings-regexp-test") << "FHC( " << d_regexp_opr.mkString( r ) <<" ) is " << std::endl;
-			//d_regexp_opr.firstChar( r );
-			//r = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, atom[0], r );
-			/*
-			std::vector< Node > vec_r;
-			vec_r.push_back( r );
-
-			StringsPreprocess spp;
-			spp.simplify( vec_r );
-			for( unsigned i=1; i<vec_r.size(); i++ ){
-				if(vec_r[i].getKind() == kind::STRING_IN_REGEXP) {
-					d_reg_exp_mem.push_back( vec_r[i] );
-				} else if(vec_r[i].getKind() == kind::EQUAL) {
-					d_equalityEngine.assertEquality(vec_r[i], true, vec_r[i]);
-				} else {
-					Assert(false);
-				}
+			Node x = atom[0];
+			Node r = atom[1];
+			Assert( r.getKind()==kind::REGEXP_STAR );
+			if( areEqual( x, d_emptyString ) ) {
+				Node ant = NodeManager::currentNM()->mkNode( kind::AND, assertion, x.eqNode( d_emptyString ) );
+				Node conc = Node::null();
+				sendLemma( ant, conc, "RegExp Empty Conflict" );
+				addedLemma = true;
+			} else {
+				Trace("strings-regexp") << "RegEx is incomplete due to " << assertion << "." << std::endl;
+				is_unk = true;
 			}
-			*/
-			Trace("strings-regexp") << "RegEx is incomplete due to " << assertion << "." << std::endl;
-			is_unk = true;
 		}
 	}
 	if( addedLemma ){
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 4d1643fbd..ca48d2fef 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -157,6 +157,20 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 		} else {
 			throw LogicException("string char at not supported in this release");
 		}
+	} else if( t.getKind() == kind::STRING_STRIDOF ){
+		//if(options::stringExp()) {
+		////	d_cache[t] = t;
+		//	retNode = t;
+		//} else {
+			throw LogicException("string indexof not supported in this release");
+		//}
+	} else if( t.getKind() == kind::STRING_STRREPL ){
+		//if(options::stringExp()) {
+		//	d_cache[t] = t;
+		//	retNode = t;
+		//} else {
+			throw LogicException("string replace not supported in this release");
+		//}
 	} else if( t.getNumChildren()>0 ){
 		std::vector< Node > cc;
 		if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index af19095a0..f68deda54 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -371,6 +371,41 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
 				retNode = NodeManager::currentNM()->mkConst( false );
 			}
 		}
+	} else if(node.getKind() == kind::STRING_STRIDOF) {
+		if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) {
+			CVC4::String s = node[0].getConst<String>();
+			CVC4::String t = node[1].getConst<String>();
+			int i = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
+			std::size_t ret = s.find(t, i);
+			if( ret != std::string::npos ) {
+				retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational((int) ret) );
+			} else {
+				retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
+			}
+		}
+	} else if(node.getKind() == kind::STRING_STRREPL) {
+		if(node[1] != node[2]) {
+			if(node[0].isConst() && node[1].isConst()) {
+				CVC4::String s = node[0].getConst<String>();
+				CVC4::String t = node[1].getConst<String>();
+				std::size_t p = s.find(t);
+				if( p != std::string::npos ) {
+					if(node[2].isConst()) {
+						CVC4::String r = node[2].getConst<String>();
+						CVC4::String ret = s.replace(t, r);
+						retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(ret) );
+					} else {
+						CVC4::String s1 = s.substr(0, (int)p);
+						CVC4::String s3 = s.substr((int)p + (int)t.size());
+						Node ns1 = NodeManager::currentNM()->mkConst( ::CVC4::String(s1) );
+						Node ns3 = NodeManager::currentNM()->mkConst( ::CVC4::String(s3) );
+						retNode = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, ns1, node[2], ns3 );
+					}
+				} else {
+					retNode = node[0];
+				}
+			}
+		}
 	} else if(node.getKind() == kind::STRING_IN_REGEXP) {
 		retNode = rewriteMembership(node);
 	}
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 9d3197517..29fdf27a6 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -113,11 +113,55 @@ public:
     if( check ){
         TypeNode t = n[0].getType(check);
         if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string char at");
+          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string char at 0");
         }
 		t = n[1].getType(check);
         if (!t.isInteger()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting an integer string term in string char at");
+          throw TypeCheckingExceptionPrivate(n, "expecting an integer term in string char at 1");
+        }
+    }
+    return nodeManager->stringType();
+  }
+};
+
+class StringIndexOfTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    if( check ){
+        TypeNode t = n[0].getType(check);
+        if (!t.isString()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string indexof 0");
+        }
+		t = n[1].getType(check);
+        if (!t.isString()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string indexof 1");
+        }
+		t = n[2].getType(check);
+        if (!t.isInteger()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting an integer term in string indexof 2");
+        }
+    }
+    return nodeManager->integerType();
+  }
+};
+
+class StringReplaceTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    if( check ){
+        TypeNode t = n[0].getType(check);
+        if (!t.isString()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 0");
+        }
+		t = n[1].getType(check);
+        if (!t.isString()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 1");
+        }
+		t = n[2].getType(check);
+        if (!t.isString()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 2");
         }
     }
     return nodeManager->stringType();