Add the remaining smtlib string operators excluding the regex and the…

… conversion operators (#335)
stanford-centaur · Nov 10, 2023 · e2a9d54 · e2a9d54
1 parent a019770
commit e2a9d54
Show file tree

Hide file tree

Showing 10 changed files with 326 additions and 11 deletions.
diff --git a/cvc5/src/cvc5_solver.cpp b/cvc5/src/cvc5_solver.cpp
@@ -98,6 +98,15 @@ const std::unordered_map<PrimOp, ::cvc5::Kind> primop2kind(
       { StrLeq, ::cvc5::Kind::STRING_LEQ },
       { StrLen, ::cvc5::Kind::STRING_LENGTH }, 
       { StrConcat, ::cvc5::Kind::STRING_CONCAT },
+      { StrSubstr, ::cvc5::Kind::STRING_SUBSTR },
+      { StrAt, ::cvc5::Kind::STRING_CHARAT },
+      { StrContains, ::cvc5::Kind::STRING_CONTAINS },
+      { StrIndexof, ::cvc5::Kind::STRING_INDEXOF },
+      { StrReplace, ::cvc5::Kind::STRING_REPLACE },
+      { StrReplaceAll, ::cvc5::Kind::STRING_REPLACE_ALL },
+      { StrPrefixof, ::cvc5::Kind::STRING_PREFIX },
+      { StrSuffixof, ::cvc5::Kind::STRING_SUFFIX },
+      { StrIsDigit, ::cvc5::Kind::STRING_IS_DIGIT },
       // Indexed Op
       { Select, ::cvc5::Kind::SELECT },
       { Store, ::cvc5::Kind::STORE },

diff --git a/cvc5/src/cvc5_term.cpp b/cvc5/src/cvc5_term.cpp
@@ -109,6 +109,15 @@ const std::unordered_map<::cvc5::Kind, PrimOp> kind2primop(
       { ::cvc5::Kind::STRING_LEQ, StrLeq },
       { ::cvc5::Kind::STRING_LENGTH, StrLen },
       { ::cvc5::Kind::STRING_CONCAT, StrConcat },
+      { ::cvc5::Kind::STRING_SUBSTR, StrSubstr },
+      { ::cvc5::Kind::STRING_CHARAT, StrAt },
+      { ::cvc5::Kind::STRING_CONTAINS, StrContains },
+      { ::cvc5::Kind::STRING_INDEXOF, StrIndexof },
+      { ::cvc5::Kind::STRING_REPLACE, StrReplace },
+      { ::cvc5::Kind::STRING_REPLACE_ALL, StrReplaceAll },
+      { ::cvc5::Kind::STRING_PREFIX, StrPrefixof },
+      { ::cvc5::Kind::STRING_SUFFIX, StrSuffixof },
+      { ::cvc5::Kind::STRING_IS_DIGIT, StrIsDigit },
       // Indexed Op
       { ::cvc5::Kind::INT_TO_BITVECTOR, Int_To_BV },
       { ::cvc5::Kind::SELECT, Select },

diff --git a/include/ops.h b/include/ops.h
@@ -103,6 +103,15 @@ enum PrimOp
   StrLeq,
   StrLen,
   StrConcat,
+  StrSubstr,
+  StrAt,
+  StrContains,
+  StrIndexof,
+  StrReplace,
+  StrReplaceAll,
+  StrPrefixof,
+  StrSuffixof,
+  StrIsDigit,
   /* Array Theory */
   Select,
   Store,

diff --git a/include/smtlibparser_maps.h b/include/smtlibparser_maps.h
@@ -99,9 +99,19 @@ const std::unordered_map<std::string, std::unordered_map<std::string, PrimOp>>
           // Strings
           { "S",
             { { "str.<", StrLt },
-              { "str.<=", StrLeq},
-              { "str.len", StrLen}, 
-              { "str.++", StrConcat} } },
+              { "str.<=", StrLeq },
+              { "str.len", StrLen }, 
+              { "str.++", StrConcat }, 
+              { "str.substr", StrSubstr }, 
+              { "str.at", StrAt },
+              { "str.contains", StrContains },
+              { "str.indexof", StrIndexof },
+              { "str.replace", StrReplace },
+              { "str.replace_all", StrReplaceAll },
+              { "str.prefixof", StrPrefixof },
+              { "str.suffixof", StrSuffixof },
+              { "str.is_digit", StrIsDigit }, 
+            } },
           // ArraysEx
           { "A",
             {

diff --git a/include/sort_inference.h b/include/sort_inference.h
@@ -163,6 +163,27 @@ bool check_tester_sorts(const SortVec & sorts);
 
 bool check_store_sorts(const SortVec & sorts);
 
+/** Checks if the sorts are well-sorted for a substring operator
+ *  @param sorts the vector of sorts
+ *  @param returns true iff the first sort is the string sort
+ *         and the next two match the int sort
+ */
+bool check_substr_sorts(const SortVec & sorts);
+
+/** Checks if the sorts are well-sorted for a char at operator
+ *  @param sorts the vector of sorts
+ *  @param returns true iff the first sort is the string sort
+ *         and the second is the int sort
+ */
+bool check_charat_sorts(const SortVec & sorts);
+
+/** Checks if the sorts are well-sorted for an index of operator
+ *  @param sorts the vector of sorts
+ *  @param returns true iff the first two sorts are the string sort
+ *         and the third is the int sort
+ */
+bool check_indexof_sorts(const SortVec & sorts);
+
 bool bool_sorts(const SortVec & sorts);
 
 bool bv_sorts(const SortVec & sorts);

diff --git a/src/ops.cpp b/src/ops.cpp
@@ -89,6 +89,15 @@ const std::unordered_map<PrimOp, std::string> primop2str(
       { StrLeq, "str.<="},
       { StrLen, "str.len"}, 
       { StrConcat, "str.++"},
+      { StrSubstr, "str.substr"},
+      { StrAt, "str.at"},
+      { StrContains, "str.contains"},
+      { StrIndexof, "str.indexof"},
+      { StrReplace, "str.replace"},
+      { StrReplaceAll, "str.replace_all"},
+      { StrPrefixof, "str.prefixof"},
+      { StrSuffixof, "str.suffixof"},
+      { StrIsDigit, "str.is_digit"},
       { Select, "select" },
       { Store, "store" },
       { Forall, "forall" },
@@ -175,6 +184,15 @@ const std::unordered_map<PrimOp, std::pair<size_t, size_t>> primop2arity(
       { StrLeq, { 2, 2} },
       { StrLen, { 1, 1} },
       { StrConcat, { 2, INT_MAX} },
+      { StrSubstr, { 3, 3} },
+      { StrAt, { 2, 2} },
+      { StrContains, { 2, 2} },
+      { StrIndexof, { 3, 3} },
+      { StrReplace, { 3, 3} },
+      { StrReplaceAll, { 3, 3} },
+      { StrPrefixof, { 2, 2} },
+      { StrSuffixof, { 2, 2} },
+      { StrIsDigit, { 1, 1} },
       { Select, { 2, 2 } },
       { Store, { 3, 3 } },
       // to make term traversal easier considering the differences

diff --git a/src/sort_inference.cpp b/src/sort_inference.cpp
@@ -97,6 +97,15 @@ const std::unordered_map<PrimOp, std::function<bool(const SortVec & sorts)>>
                           { StrLeq, string_sorts },
                           { StrConcat, string_sorts },
                           { StrLen, string_sorts },
+                          { StrSubstr, check_substr_sorts },
+                          { StrAt, check_charat_sorts },
+                          { StrContains, string_sorts },
+                          { StrIndexof, check_indexof_sorts },
+                          { StrReplace, string_sorts },
+                          { StrReplaceAll, string_sorts },
+                          { StrPrefixof, string_sorts },
+                          { StrSuffixof, string_sorts },
+                          { StrIsDigit, string_sorts },
                           { Select, check_select_sorts },
                           { Store, check_store_sorts },
                           { Forall, check_quantifier_sorts },
@@ -182,7 +191,16 @@ const std::unordered_map<
         { StrLt, bool_sort },
         { StrLeq, bool_sort },
         { StrConcat, string_sort },
-        { StrLen, int_sort },        
+        { StrLen, int_sort },
+        { StrSubstr, string_sort },
+        { StrAt, string_sort },
+        { StrContains, bool_sort },
+        { StrIndexof, int_sort },
+        { StrReplace, string_sort },
+        { StrReplaceAll, string_sort },
+        { StrPrefixof, bool_sort },
+        { StrSuffixof, bool_sort },
+        { StrIsDigit, bool_sort },
         { Select, select_sort },
         { Store, store_sort },
         { Forall, bool_sort },
@@ -444,6 +462,80 @@ bool check_store_sorts(const SortVec & sorts)
   return true;
 }
 
+bool check_substr_sorts(const SortVec & sorts)
+{
+  assert(sorts.size());
+  if (sorts.size() != 3)
+  {
+    return false;
+  }
+
+  Sort strsort = sorts[0];
+  if (strsort->get_sort_kind() != STRING)
+  {
+    return false;
+  }
+
+  if (sorts[1]->get_sort_kind() != INT)
+  {
+    return false;
+  }
+  else if (sorts[2]->get_sort_kind() != INT)
+  {
+    return false;
+  }
+
+  return true;
+}
+
+bool check_charat_sorts(const SortVec & sorts)
+{
+  assert(sorts.size());
+  if (sorts.size() != 2)
+  {
+    return false;
+  }
+
+  Sort strsort = sorts[0];
+  if (strsort->get_sort_kind() != STRING)
+  {
+    return false;
+  }
+
+  if (sorts[1]->get_sort_kind() != INT)
+  {
+    return false;
+  }
+
+  return true;
+}
+
+bool check_indexof_sorts(const SortVec & sorts)
+{
+  assert(sorts.size());
+  if (sorts.size() != 3)
+  {
+    return false;
+  }
+
+  Sort strsort = sorts[0];
+  if (strsort->get_sort_kind() != STRING)
+  {
+    return false;
+  }
+
+  if (sorts[1]->get_sort_kind() != STRING)
+  {
+    return false;
+  }
+  else if (sorts[2]->get_sort_kind() != INT)
+  {
+    return false;
+  }
+
+  return true;
+}
+
 bool bool_sorts(const SortVec & sorts)
 {
   return check_sortkind_matches(BOOL, sorts);

diff --git a/tests/cvc5/cvc5-str.cpp b/tests/cvc5/cvc5-str.cpp
@@ -33,17 +33,32 @@ int main()
   Sort intsort = s->make_sort(INT);
 
   Term zero = s->make_term(0, intsort);
+  Term one = s->make_term(1, intsort);
+  Term minusone = s->make_term(-1, intsort);
+  Term A = s->make_term("A", false, strsort);
+  Term str1 = s->make_term("1", false, strsort);
+  Term str10 = s->make_term("10", false, strsort);
+  Term n = s->make_symbol("n", intsort);
 
   Term x = s->make_symbol("x", strsort);
   Term y = s->make_symbol("y", strsort);
   Term z = s->make_symbol("z", strsort);
+  Term empty = s->make_symbol("empty", strsort);
 
   Term lenx = s->make_term(StrLen, x);
   Term leny = s->make_term(StrLen, y);
   Term lenz = s->make_term(StrLen, z);
+  Term lenempty = s->make_term(StrLen, empty);
 
+  Term xx = s->make_term(StrConcat, x, x);
   Term xy = s->make_term(StrConcat, x, y);
   Term yx = s->make_term(StrConcat, y, x);
+  Term xxx = s->make_term(StrConcat, xx, x);
+  Term xyy = s->make_term(StrConcat, xy, y);
+
+  Term substryx = s->make_term(StrSubstr, yx, leny, lenx);
+
+  s->assert_formula(s->make_term(Equal, lenempty, zero));
 
   //StrLt
   s->assert_formula(s->make_term(StrLt, x, y));
@@ -54,14 +69,46 @@ int main()
   s->assert_formula(s->make_term(Lt, zero, lenz));
   //StrConcat
   s->assert_formula(s->make_term(Not, s->make_term(Equal, xy, yx)));
-
-
+  //StrSubstr
+  s->assert_formula(s->make_term(Equal, x, substryx));
+  s->assert_formula(s->make_term(Not, s->make_term(Equal, y, substryx)));
+  s->assert_formula(s->make_term(Equal, empty, s->make_term(StrSubstr, x, lenx, lenx)));
+  s->assert_formula(s->make_term(Equal, empty, s->make_term(StrSubstr, x, minusone, lenx)));
+  //StrAt
+  s->assert_formula(s->make_term(Equal, s->make_term(StrLen, s->make_term(StrAt, y, zero)), one));
+  s->assert_formula(s->make_term(Equal, empty, s->make_term(StrAt, x, lenx)));
+  s->assert_formula(s->make_term(Equal, empty, s->make_term(StrAt, x, minusone)));
+  //StrContains
+  s->assert_formula(s->make_term(Not, s->make_term(StrContains, x, y)));
+  s->assert_formula(s->make_term(StrContains, xy, y));
+  //StrIndexof
+  s->assert_formula(s->make_term(Equal, lenx, s->make_term(StrIndexof, xyy, y, s->make_term(Minus, lenx, one))));
+  s->assert_formula(s->make_term(Equal, zero, s->make_term(StrIndexof, xy, empty, zero)));
+  s->assert_formula(s->make_term(Equal, minusone, s->make_term(StrIndexof, xy, x, minusone)));
+  s->assert_formula(s->make_term(Equal, minusone, s->make_term(StrIndexof, x, y, lenx)));
+  s->assert_formula(s->make_term(Equal, minusone, s->make_term(StrIndexof, x, y, zero)));
+  //StrReplace
+  s->assert_formula(s->make_term(Equal, xx, s->make_term(StrReplace, xy, y, x)));
+  s->assert_formula(s->make_term(Equal, xy, s->make_term(StrReplace, y, empty, x)));
+  //StrReplaceAll
+  s->assert_formula(s->make_term(Equal, xxx, s->make_term(StrReplaceAll, xyy, y, x)));
+  s->assert_formula(s->make_term(Equal, xyy, s->make_term(StrReplaceAll, xyy, empty, x)));
+  //StrPrefixof
+  s->assert_formula(s->make_term(StrPrefixof, x, xyy));
+  s->assert_formula(s->make_term(Not, s->make_term(StrPrefixof, str1, A)));
+  //StrSuffixof
+  s->assert_formula(s->make_term(StrSuffixof, y, xyy));
+  s->assert_formula(s->make_term(Not, s->make_term(StrSuffixof, str1, A)));
+  //StrIsDigit
+  s->assert_formula(s->make_term(StrIsDigit, str1));
+  s->assert_formula(s->make_term(Not, s->make_term(StrIsDigit, A)));
+  s->assert_formula(s->make_term(Not, s->make_term(StrIsDigit, str10)));
 
   Result r = s->check_sat();
   assert(r.is_sat());
 
   cout << "Model Values:" << endl;
-  for (auto t : TermVec({ x, y, z }))
+  for (auto t : TermVec({ x, y, z}))
   {
     cout << "\t" << t << " = " << s->get_value(t) << endl;
   }

diff --git a/tests/smt2/qf_s/test-ops-SLIA.smt2 b/tests/smt2/qf_s/test-ops-SLIA.smt2
@@ -3,18 +3,30 @@
 (declare-const x String)
 (declare-const y String)
 (declare-const z String)
+(declare-const substryx String)
+(declare-const empty String)
 (declare-const lenx Int)
 (declare-const leny Int)
 (declare-const lenz Int)
 
 (assert (= lenx (str.len x)))
 (assert (= leny (str.len y)))
+(assert (= lenz (str.len z)))
 
+(declare-const xx String)
 (declare-const xy String)
 (declare-const yx String)
+(declare-const xxx String)
+(declare-const xyy String)
 
+(assert (= xx (str.++ x x)))
 (assert (= xy (str.++ x y)))
 (assert (= yx (str.++ y x)))
+(assert (= xxx (str.++ xx x)))
+(assert (= xyy (str.++ xy y)))
+
+(assert (= substryx (str.substr yx leny lenx)))
+(assert (= empty ""))
 
 ;StrLt
 (assert (str.< x y))
@@ -25,5 +37,39 @@
 (assert (< 0 lenz))
 ;StrConcat
 (assert (not (= xy yx)))
+;StrSubstr
+(assert (= x substryx))
+(assert (not (= y substryx)))
+(assert (= empty (str.substr x lenx lenx)))
+(assert (= empty (str.substr x (- 1) lenx)))
+;StrAt
+(assert (= (str.len (str.at y 0)) 1))
+(assert (= empty (str.at x lenx)))
+(assert (= empty (str.at x (- 1))))
+;StrContains
+(assert (not (str.contains x y)))
+(assert (str.contains xy y))
+;StrIndexof
+(assert (= lenx (str.indexof xyy y (- lenx 1))))
+(assert (= 0 (str.indexof xy empty 0)))
+(assert (= (- 1) (str.indexof xy x (- 1))))
+(assert (= (- 1) (str.indexof x y lenx)))
+(assert (= (- 1) (str.indexof x y 0)))
+;StrReplace
+(assert (= xx (str.replace xy y x)))
+(assert (= xy (str.replace y empty x)))
+;StrReplaceAll
+(assert (= xxx (str.replace_all xyy y x)))
+(assert (= xyy (str.replace_all xyy empty x)))
+;StrPrefixof
+(assert (str.prefixof x xyy))
+(assert (not (str.prefixof "1" "A")))
+;StrSuffixof
+(assert (str.suffixof y xyy))
+(assert (not (str.suffixof "1" "A")))
+;StrIsDigit
+(assert (str.is_digit "1"))
+(assert (not (str.is_digit "A")))
+(assert (not (str.is_digit "10")))
 
 (check-sat)