adds partial function substr. the use of this function should be guarded, especially for disequalities

6 files changed, 118 insertions, 60 deletions

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 814276a7c..fe7b9b3d9 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -16,6 +16,8 @@ operator STRING_IN_REGEXP 2 "membership"
 
 operator STRING_LENGTH 1 "string length"
 
+operator STRING_SUBSTR 3 "string substr"
+
 #sort CHAR_TYPE \
 #    Cardinality::INTEGERS \
 #    well-founded \
@@ -99,6 +101,7 @@ 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_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule
 
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index bf61d3852..291af408b 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -364,7 +364,7 @@ void TheoryStrings::check(Effort e) {
   bool addedLemma = false;
   if( e == EFFORT_FULL && !d_conflict ) {
       eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
-      while( !eqcs_i.isFinished() ){
+      while( !eqcs_i.isFinished() ) {
         Node eqc = (*eqcs_i);
         //if eqc.getType is string
         if (eqc.getType().isString()) {
@@ -372,60 +372,59 @@ void TheoryStrings::check(Effort e) {
             //get the constant for the equivalence class
             //int c_len = ...;
             eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-            while( !eqc_i.isFinished() ){
-              Node n = (*eqc_i);
-
-              //if n is concat, and
-              //if n has not instantiatied the concat..length axiom
-              //then, add lemma
-              if( n.getKind() == kind::STRING_CONCAT || n.getKind() == kind::CONST_STRING ){
-                if( d_length_inst.find(n)==d_length_inst.end() ){
-                    d_length_inst[n] = true;
-                    Trace("strings-debug") << "get n: " << n << endl;
-                    Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" );
-					d_length_intro_vars.push_back( sk );
-                    Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n );
-                    eq = Rewriter::rewrite(eq);
-                    Trace("strings-lemma") << "Strings: Add lemma " << eq << std::endl;
-                    d_out->lemma(eq);
-                    Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
-                    Node lsum;
-                    if( n.getKind() == kind::STRING_CONCAT ){
-                        //add lemma
-                        std::vector<Node> node_vec;
-                        for( unsigned i=0; i<n.getNumChildren(); i++ ) {
-                            Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
-                            node_vec.push_back(lni);
-                        }
-                        lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec );
-                    }else{
-                        //add lemma
-                        lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
-                    }
-                    Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
-                    ceq = Rewriter::rewrite(ceq);
-                    Trace("strings-lemma") << "Strings: Add lemma " << ceq << std::endl;
-                    d_out->lemma(ceq);
-                    addedLemma = true;
-                }
-              }
-              ++eqc_i;
-            }
+			while( !eqc_i.isFinished() ){
+				Node n = (*eqc_i);
+				//if n is concat, and
+				//if n has not instantiatied the concat..length axiom
+				//then, add lemma
+				if( n.getKind() == kind::STRING_CONCAT || n.getKind() == kind::CONST_STRING ){
+					if( d_length_inst.find(n)==d_length_inst.end() ){
+						d_length_inst[n] = true;
+						Trace("strings-debug") << "get n: " << n << endl;
+						Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" );
+						d_length_intro_vars.push_back( sk );
+						Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n );
+						eq = Rewriter::rewrite(eq);
+						Trace("strings-lemma") << "Strings: Add term lemma " << eq << std::endl;
+						d_out->lemma(eq);
+						Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
+						Node lsum;
+						if( n.getKind() == kind::STRING_CONCAT ){
+							//add lemma
+							std::vector<Node> node_vec;
+							for( unsigned i=0; i<n.getNumChildren(); i++ ) {
+								Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
+								node_vec.push_back(lni);
+							}
+							lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec );
+						}else{
+							//add lemma
+							lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
+						}
+						Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
+						ceq = Rewriter::rewrite(ceq);
+						Trace("strings-lemma") << "Strings: Add length lemma " << ceq << std::endl;
+						d_out->lemma(ceq);
+						addedLemma = true;
+					}
+				}
+				++eqc_i;
+			}
         }
         ++eqcs_i;
-  }
-  if( !addedLemma ){
-      addedLemma = checkNormalForms();
-	  Trace("strings-process") << "Done check normal forms, 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;
-          if( !d_conflict && !addedLemma ){
-            addedLemma = checkInductiveEquations();
-			Trace("strings-process") << "Done check inductive equations, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
-          }
-      }
-  }
+	  }
+	  if( !addedLemma ){
+		  addedLemma = checkNormalForms();
+		  Trace("strings-process") << "Done check normal forms, 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;
+			  if( !d_conflict && !addedLemma ){
+				addedLemma = checkInductiveEquations();
+				Trace("strings-process") << "Done check inductive equations, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+			  }
+		  }
+	  }
   }
   Trace("strings-check") << "Theory of strings, done check : " << e << std::endl;
   Trace("strings-process") << "Theory of strings, done check : " << e << std::endl;
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 8fa4345e5..f303fd333 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -84,7 +84,8 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret
 	}
 }
 
-Node StringsPreprocess::simplify( Node t ) {
+
+Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
     if(i != d_cache.end()) {
       return (*i).second.isNull() ? t : (*i).second;
@@ -92,21 +93,39 @@ Node StringsPreprocess::simplify( Node t ) {
 
 	if( t.getKind() == kind::STRING_IN_REGEXP ){
 		// t0 in t1
+		Node t0 = simplify( t[0], new_nodes );
 		//rewrite it
 		std::vector< Node > ret;
-		simplifyRegExp( t[0], t[1], ret );
+		simplifyRegExp( t0, t[1], ret );
 
 		Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret );
 		d_cache[t] = (t == n) ? Node::null() : n;
 		return n;
-    }else if( t.getNumChildren()>0 ){
+	}else if( t.getKind() == kind::STRING_SUBSTR ){
+		Node sk1 = NodeManager::currentNM()->mkSkolem( "st1sym_$$", t.getType(), "created for substr" );
+		Node sk2 = NodeManager::currentNM()->mkSkolem( "st2sym_$$", t.getType(), "created for substr" );
+		Node sk3 = NodeManager::currentNM()->mkSkolem( "st3sym_$$", t.getType(), "created for substr" );
+		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_j = NodeManager::currentNM()->mkNode( kind::EQUAL, t[2],
+								NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) );
+		new_nodes.push_back( len_sk2_eq_j );
+
+		d_cache[t] = sk2;
+		return sk2;
+	} else if( t.getNumChildren()>0 ){
 		std::vector< Node > cc;
 		if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {
 			cc.push_back(t.getOperator());
 		}
 		bool changed = false;
 		for( unsigned i=0; i<t.getNumChildren(); i++ ){
-			Node tn = simplify( t[i] );
+			Node tn = simplify( t[i], new_nodes );
 			cc.push_back( tn );
 			changed = changed || tn!=t[i];
 		}
@@ -125,9 +144,11 @@ Node StringsPreprocess::simplify( Node t ) {
 }
 
 void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
+	std::vector< Node > new_nodes;
 	for( unsigned i=0; i<vec_node.size(); i++ ){
-		vec_node[i] = simplify( vec_node[i] );
+		vec_node[i] = simplify( vec_node[i], new_nodes );
 	}
+	vec_node.insert( vec_node.end(), new_nodes.begin(), new_nodes.end() );
 }
 
 }/* CVC4::theory::strings namespace */
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index f82a3cf24..d07249a02 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -32,7 +32,7 @@ class StringsPreprocess {
 	std::hash_map<TNode, Node, TNodeHashFunction> d_cache;
 private:
 	void simplifyRegExp( Node s, Node r, std::vector< Node > &ret );
-	Node simplify( Node t );
+	Node simplify( Node t, std::vector< Node > &new_nodes );
 public:
 void simplify(std::vector< Node > &vec_node);
 };
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 412135675..3a7ad1ee0 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -137,7 +137,20 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                 retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec);
             }
         }
-    }
+    } else if(node.getKind() == kind::STRING_SUBSTR) {
+		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 );
+			}
+		} else {
+			//handled by preprocess
+		}
+	}
 
   Trace("strings-postrewrite") << "Strings::postRewrite returning " << node << std::endl;
   return RewriteResponse(REWRITE_DONE, retNode);
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 8fc630206..ef8f58f80 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -61,6 +61,28 @@ public:
   }
 };
 
+class StringSubstrTypeRule {
+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 string terms in substr");
+        }
+		t = n[1].getType(check);
+        if (!t.isInteger()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting start int terms in substr");
+        }
+		t = n[2].getType(check);
+        if (!t.isInteger()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting length int terms in substr");
+        }
+    }
+    return nodeManager->stringType();
+  }
+};
+
 class RegExpConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)