add prefixof, suffixof

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 497705cb62c0fb92efcbc217a6041fc17fb9f208..1bfae498a75ca1134347a8cf1485b81ab1135609 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1256,6 +1256,8 @@ builtinOp[CVC4::Kind& kind]
   | STRCAT_TOK     { $kind = CVC4::kind::STRING_CHARAT; }
   | STRIDOF_TOK    { $kind = CVC4::kind::STRING_STRIDOF; }
   | STRREPL_TOK    { $kind = CVC4::kind::STRING_STRREPL; }
+  | STRPREF_TOK    { $kind = CVC4::kind::STRING_PREFIX; }
+  | STRSUFF_TOK    { $kind = CVC4::kind::STRING_SUFFIX; }
   | STRINRE_TOK    { $kind = CVC4::kind::STRING_IN_REGEXP; }
   | STRTORE_TOK    { $kind = CVC4::kind::STRING_TO_REGEXP; }
   | RECON_TOK      { $kind = CVC4::kind::REGEXP_CONCAT; }
@@ -1634,6 +1636,8 @@ STRCTN_TOK : 'str.contain' ;
 STRCAT_TOK : 'str.at' ;
 STRIDOF_TOK : 'str.indexof' ;
 STRREPL_TOK : 'str.replace' ;
+STRPREF_TOK : 'str.prefixof' ;
+STRSUFF_TOK : 'str.suffixof' ;
 STRINRE_TOK : 'str.in.re';
 STRTORE_TOK : 'str.to.re';
 RECON_TOK : 're.++';

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index aae9938b7b3225ef50bcfee7884a7f6455f94252..d97c070637e9c76174fa2797bfd3bcf2c471fb19 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -283,6 +283,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::STRING_STRCTN: out << "str.contain "; break;
   case kind::STRING_STRIDOF: out << "str.indexof "; break;
   case kind::STRING_STRREPL: out << "str.replace "; break;
+  case kind::STRING_PREFIX: out << "str.prefixof "; break;
+  case kind::STRING_SUFFIX: out << "str.suffixof "; break;
   case kind::STRING_TO_REGEXP: out << "str.to.re "; break;
   case kind::REGEXP_CONCAT: out << "re.++ "; break;
   case kind::REGEXP_OR: out << "re.or "; break;

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index e55891ec2852af8f53ef6da9b7d371ea9d754af9..b3a75a560205422bef2ba91d48dc0e170c130198 100644 (file)
--- 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 0a8781abb4eeb46e6275992f9210875ef692c0f8..3209a92ec86ae32175ed4497e89bcb26ec767024 100644 (file)
--- 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 ddfe1a39ca665ca8a88c12b82b17ae5da6fac9ec..7bf016d2916cb72c1fd16d9736e524ab8f5966b3 100644 (file)
--- 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 29fdf27a6a8837070aef2bd815062d6e507b452b..2b198892b725de4edc1169b1cef0c940ffcdf3f3 100644 (file)
--- 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)