new functions in strings

4 files changed, 134 insertions, 19 deletions

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 20db916c9..a421d6fa8 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -11,12 +11,11 @@ typechecker "theory/strings/theory_strings_type_rules.h"
 
 
 operator STRING_CONCAT 2: "string concat"
-
 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"
 
 #sort CHAR_TYPE \
 #    Cardinality::INTEGERS \
@@ -104,6 +103,8 @@ typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule
 typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule
 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_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule
 
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index ff01b1887..355b182c9 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -136,6 +136,58 @@ 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 ){
+		if(options::stringExp()) {
+			Node w = simplify( t[0], new_nodes );
+			Node y = simplify( t[1], new_nodes );
+			Node emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
+			std::vector< Node > or_vec;
+			or_vec.push_back( w.eqNode(y) );
+			Node x1 = NodeManager::currentNM()->mkBoundVar( t[0].getType() );
+			Node c1 = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::AND,
+							x1.eqNode( emptyString ).negate(),
+							w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, x1, y ) )));
+			or_vec.push_back( c1 );
+			Node z2 = NodeManager::currentNM()->mkBoundVar( t[0].getType() );
+			Node c2 = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::AND,
+							z2.eqNode( emptyString ).negate(),
+							w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, y, z2 ) )));
+			or_vec.push_back( c2 );
+			Node x3 = NodeManager::currentNM()->mkBoundVar( t[0].getType() );
+			Node z3 = NodeManager::currentNM()->mkBoundVar( t[0].getType() );
+			Node c3 = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::AND,
+							x3.eqNode( emptyString ).negate(), z3.eqNode( emptyString ).negate(),
+							w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, x3, y, z3 ) )));
+			or_vec.push_back( c3 );
+
+			Node cc = NodeManager::currentNM()->mkNode( kind::OR, or_vec );
+
+			d_cache[t] = cc;
+			retNode = cc;
+		} else {
+			throw LogicException("string contain not supported in this release");
+		}
+	}  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" );
+			Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3sym_$$", t.getType(), "created for charat" );
+			Node x = simplify( t[0], new_nodes );
+			Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL,
+								NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x );
+			new_nodes.push_back( x_eq_123 );
+			Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1],
+									NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
+			new_nodes.push_back( len_sk1_eq_i );
+			Node len_sk2_eq_1 = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkConst( Rational( 1 ) ),
+									NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) );
+			new_nodes.push_back( len_sk2_eq_1 );
+
+			d_cache[t] = sk2;
+			retNode = sk2;
+		} else {
+			throw LogicException("string char at 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 0e37367bf..af19095a0 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -341,21 +341,35 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
             }
         }
     } else if(node.getKind() == kind::STRING_SUBSTR) {
-		if(options::stringExp()) {
-			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) ) {
-					retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, j) );
-				} else {
-					// TODO: some issues, must be guarded by users
-					retNode = NodeManager::currentNM()->mkConst( false );
-				}
+		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) ) {
+				retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, j) );
 			} else {
-				//handled by preprocess
+				// TODO: some issues, must be guarded by users
+				retNode = NodeManager::currentNM()->mkConst( false );
+			}
+		}
+	} else if(node.getKind() == kind::STRING_STRCTN) {
+		if( node[0].isConst() && node[1].isConst() ) {
+			CVC4::String s = node[0].getConst<String>();
+			CVC4::String t = node[1].getConst<String>();
+			if( s.find(t) != std::string::npos ) {
+				retNode = NodeManager::currentNM()->mkConst( true );
+			} else {
+				retNode = NodeManager::currentNM()->mkConst( false );
+			}
+		}
+	} else if(node.getKind() == kind::STRING_CHARAT) {
+		if( node[0].isConst() && node[1].isConst() ) {
+			int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
+			if( node[0].getConst<String>().size() > (unsigned) i ) {
+				retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, 1) );
+			} else {
+				// TODO: some issues, must be guarded by users
+				retNode = NodeManager::currentNM()->mkConst( false );
 			}
-		} else {
-			throw LogicException("substring not supported in this release");
 		}
 	} 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 d5019ab39..df9d29f0f 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -57,6 +57,9 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ){
+		if(n.getNumChildren() != 1) {
+          throw TypeCheckingExceptionPrivate(n, "expecting 1 term in string length");
+		}
         TypeNode t = n[0].getType(check);
         if (!t.isString()) {
           throw TypeCheckingExceptionPrivate(n, "expecting string terms in string length");
@@ -71,17 +74,62 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ){
+		if(n.getNumChildren() != 3) {
+          throw TypeCheckingExceptionPrivate(n, "expecting 3 terms in substr");
+		}
         TypeNode t = n[0].getType(check);
         if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting string terms in substr");
+          throw TypeCheckingExceptionPrivate(n, "expecting a string term in substr");
         }
 		t = n[1].getType(check);
         if (!t.isInteger()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting start int terms in substr");
+          throw TypeCheckingExceptionPrivate(n, "expecting a start int term in substr");
         }
 		t = n[2].getType(check);
         if (!t.isInteger()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting length int terms in substr");
+          throw TypeCheckingExceptionPrivate(n, "expecting a length int term in substr");
+        }
+    }
+    return nodeManager->stringType();
+  }
+};
+
+class StringContainTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    if( check ){
+		if(n.getNumChildren() != 2) {
+          throw TypeCheckingExceptionPrivate(n, "expecting 2 terms in string contain");
+		}
+        TypeNode t = n[0].getType(check);
+        if (!t.isString()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting an orginal string term in string contain");
+        }
+		t = n[1].getType(check);
+        if (!t.isString()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting a target string term in string contain");
+        }
+    }
+    return nodeManager->stringType();
+  }
+};
+
+class StringCharAtTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    if( check ){
+		if(n.getNumChildren() != 2) {
+          throw TypeCheckingExceptionPrivate(n, "expecting 2 terms in string char at");
+		}
+        TypeNode t = n[0].getType(check);
+        if (!t.isString()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string char at");
+        }
+		t = n[1].getType(check);
+        if (!t.isInteger()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting an integer string term in string char at");
         }
     }
     return nodeManager->stringType();