add prefixof, suffixof

4 files changed, 79 insertions, 2 deletions

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index e55891ec2..b3a75a560 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -18,6 +18,8 @@ operator STRING_CHARAT 2 "string charat (user symbol)"
 operator STRING_STRCTN 2 "string contains"
 operator STRING_STRIDOF 3 "string indexof"
 operator STRING_STRREPL 3 "string replace"
+operator STRING_PREFIX 2 "string prefixof"
+operator STRING_SUFFIX 2 "string suffixof"
 
 #sort CHAR_TYPE \
 #    Cardinality::INTEGERS \
@@ -109,6 +111,8 @@ typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule
 typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule
 typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule
 typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule
+typerule STRING_PREFIX ::CVC4::theory::strings::StringPrefixOfTypeRule
+typerule STRING_SUFFIX ::CVC4::theory::strings::StringSuffixOfTypeRule
 
 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 0a8781abb..3209a92ec 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1758,8 +1758,9 @@ bool TheoryStrings::checkSimple() {
 								Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, n[1], d_zero);
 								Node x_eq_123 = n[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk, sk3 ) );
 								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, lenxgti, lemma ) );
+								lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, lemma ) );
 								Trace("strings-lemma") << "Strings::Lemma CHARAT : " << lemma << std::endl;
 								d_out->lemma(lemma);
 							} else if( n.getKind() == kind::STRING_SUBSTR ) {
@@ -1776,7 +1777,7 @@ bool TheoryStrings::checkSimple() {
 														NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
 
 								Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i );
-								Node cond = NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 );
+								Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
 								lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, lemma ) );
 								Trace("strings-lemma") << "Strings::Lemma SUBSTR : " << lemma << std::endl;
 								d_out->lemma(lemma);
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index ddfe1a39c..7bf016d29 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -414,6 +414,42 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
 				}
 			}
 		}
+	} else if(node.getKind() == kind::STRING_PREFIX) {
+		if(node[0].isConst() && node[1].isConst()) {
+			CVC4::String s = node[1].getConst<String>();
+			CVC4::String t = node[0].getConst<String>();
+			retNode = NodeManager::currentNM()->mkConst( false );
+			if(s.size() >= t.size()) {
+				if(t == s.substr(0, t.size())) {
+					retNode = NodeManager::currentNM()->mkConst( true );
+				}
+			}
+		} else {
+			Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[0]);
+			Node lent = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]);
+			retNode = NodeManager::currentNM()->mkNode(kind::AND,
+						NodeManager::currentNM()->mkNode(kind::GEQ, lent, lens),
+						node[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, node[1],
+										NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ), lens)));
+		}
+	} else if(node.getKind() == kind::STRING_SUFFIX) {
+		if(node[0].isConst() && node[1].isConst()) {
+			CVC4::String s = node[1].getConst<String>();
+			CVC4::String t = node[0].getConst<String>();
+			retNode = NodeManager::currentNM()->mkConst( false );
+			if(s.size() >= t.size()) {
+				if(t == s.substr(s.size() - t.size(), t.size())) {
+					retNode = NodeManager::currentNM()->mkConst( true );
+				}
+			}
+		} else {
+			Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[0]);
+			Node lent = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]);
+			retNode = NodeManager::currentNM()->mkNode(kind::AND,
+						NodeManager::currentNM()->mkNode(kind::GEQ, lent, lens),
+						node[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, node[1],
+										NodeManager::currentNM()->mkNode(kind::MINUS, lent, lens), lens)));
+		}
 	} 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 29fdf27a6..2b198892b 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -168,6 +168,42 @@ public:
   }
 };
 
+class StringPrefixOfTypeRule {
+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 prefixof 0");
+        }
+		t = n[1].getType(check);
+        if (!t.isString()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string prefixof 1");
+        }
+    }
+    return nodeManager->booleanType();
+  }
+};
+
+class StringSuffixOfTypeRule {
+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 suffixof 0");
+        }
+		t = n[1].getType(check);
+        if (!t.isString()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string suffixof 1");
+        }
+    }
+    return nodeManager->booleanType();
+  }
+};
+
 class RegExpConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)