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

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 },

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 },

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,

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",
             {

include/sort_inference.h

@@ -163,6 +163,30 @@ 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);

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

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);

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;
   }