Update string kind names in new API (#4509)

To match the smt2 Unicode standard. The internal ones are left unchanged for now.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index d990b3e22d4db7fe0d12b2d4d8d0d963979e07d1..052b62efce75bf1ff7e21114ecc6ce0838fb6c96 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -253,10 +253,10 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
     {STRING_LENGTH, CVC4::Kind::STRING_LENGTH},
     {STRING_SUBSTR, CVC4::Kind::STRING_SUBSTR},
     {STRING_CHARAT, CVC4::Kind::STRING_CHARAT},
-    {STRING_STRCTN, CVC4::Kind::STRING_STRCTN},
-    {STRING_STRIDOF, CVC4::Kind::STRING_STRIDOF},
-    {STRING_STRREPL, CVC4::Kind::STRING_STRREPL},
-    {STRING_STRREPLALL, CVC4::Kind::STRING_STRREPLALL},
+    {STRING_CONTAINS, CVC4::Kind::STRING_STRCTN},
+    {STRING_INDEXOF, CVC4::Kind::STRING_STRIDOF},
+    {STRING_REPLACE, CVC4::Kind::STRING_STRREPL},
+    {STRING_REPLACE_ALL, CVC4::Kind::STRING_STRREPLALL},
     {STRING_TOLOWER, CVC4::Kind::STRING_TOLOWER},
     {STRING_TOUPPER, CVC4::Kind::STRING_TOUPPER},
     {STRING_REV, CVC4::Kind::STRING_REV},
@@ -267,8 +267,8 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
     {STRING_PREFIX, CVC4::Kind::STRING_PREFIX},
     {STRING_SUFFIX, CVC4::Kind::STRING_SUFFIX},
     {STRING_IS_DIGIT, CVC4::Kind::STRING_IS_DIGIT},
-    {STRING_ITOS, CVC4::Kind::STRING_ITOS},
-    {STRING_STOI, CVC4::Kind::STRING_STOI},
+    {STRING_FROM_INT, CVC4::Kind::STRING_ITOS},
+    {STRING_TO_INT, CVC4::Kind::STRING_STOI},
     {CONST_STRING, CVC4::Kind::CONST_STRING},
     {STRING_TO_REGEXP, CVC4::Kind::STRING_TO_REGEXP},
     {REGEXP_CONCAT, CVC4::Kind::REGEXP_CONCAT},
@@ -522,10 +522,10 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         {CVC4::Kind::STRING_LENGTH, STRING_LENGTH},
         {CVC4::Kind::STRING_SUBSTR, STRING_SUBSTR},
         {CVC4::Kind::STRING_CHARAT, STRING_CHARAT},
-        {CVC4::Kind::STRING_STRCTN, STRING_STRCTN},
-        {CVC4::Kind::STRING_STRIDOF, STRING_STRIDOF},
-        {CVC4::Kind::STRING_STRREPL, STRING_STRREPL},
-        {CVC4::Kind::STRING_STRREPLALL, STRING_STRREPLALL},
+        {CVC4::Kind::STRING_STRCTN, STRING_CONTAINS},
+        {CVC4::Kind::STRING_STRIDOF, STRING_INDEXOF},
+        {CVC4::Kind::STRING_STRREPL, STRING_REPLACE},
+        {CVC4::Kind::STRING_STRREPLALL, STRING_REPLACE_ALL},
         {CVC4::Kind::STRING_TOLOWER, STRING_TOLOWER},
         {CVC4::Kind::STRING_TOUPPER, STRING_TOUPPER},
         {CVC4::Kind::STRING_REV, STRING_REV},
@@ -536,8 +536,8 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         {CVC4::Kind::STRING_PREFIX, STRING_PREFIX},
         {CVC4::Kind::STRING_SUFFIX, STRING_SUFFIX},
         {CVC4::Kind::STRING_IS_DIGIT, STRING_IS_DIGIT},
-        {CVC4::Kind::STRING_ITOS, STRING_ITOS},
-        {CVC4::Kind::STRING_STOI, STRING_STOI},
+        {CVC4::Kind::STRING_ITOS, STRING_FROM_INT},
+        {CVC4::Kind::STRING_STOI, STRING_TO_INT},
         {CVC4::Kind::CONST_STRING, CONST_STRING},
         {CVC4::Kind::STRING_TO_REGEXP, STRING_TO_REGEXP},
         {CVC4::Kind::REGEXP_CONCAT, REGEXP_CONCAT},

diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index 05423a95225447ddec4e5f12fd48bcf9c5bd13aa..e084daf1e26a9d8a09da7478209128b98652e417 100644 (file)
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -1961,7 +1961,7 @@ enum CVC4_PUBLIC Kind : int32_t
    *   mkTerm(Kind kind, Term child1, Term child2)
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
-  STRING_STRCTN,
+  STRING_CONTAINS,
   /**
    * String index-of.
    * Returns the index of a substring s2 in a string s1 starting at index i. If
@@ -1975,7 +1975,7 @@ enum CVC4_PUBLIC Kind : int32_t
    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
-  STRING_STRIDOF,
+  STRING_INDEXOF,
   /**
    * String replace.
    * Replaces a string s2 in a string s1 with string s3. If s2 does not appear
@@ -1988,7 +1988,7 @@ enum CVC4_PUBLIC Kind : int32_t
    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
-  STRING_STRREPL,
+  STRING_REPLACE,
   /**
    * String replace all.
    * Replaces all occurrences of a string s2 in a string s1 with string s3.
@@ -2001,7 +2001,7 @@ enum CVC4_PUBLIC Kind : int32_t
    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
-  STRING_STRREPLALL,
+  STRING_REPLACE_ALL,
   /**
    * String to lower case.
    * Parameters: 1
@@ -2113,7 +2113,7 @@ enum CVC4_PUBLIC Kind : int32_t
    * Create with:
    *   mkTerm(Kind kind, Term child)
    */
-  STRING_ITOS,
+  STRING_FROM_INT,
   /**
    * String to integer (total function).
    * If the string does not contain an integer or the integer is negative, the
@@ -2123,7 +2123,7 @@ enum CVC4_PUBLIC Kind : int32_t
    * Create with:
    *   mkTerm(Kind kind, Term child)
    */
-  STRING_STOI,
+  STRING_TO_INT,
   /**
    * Constant string.
    * Parameters:

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 7babf2e56007b3f179834d05cbea2322903366ce..8e4152e2e9664cfb14ab9132b4477df677768536 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -2032,25 +2032,25 @@ stringTerm[CVC4::api::Term& f]
   | STRING_LENGTH_TOK LPAREN formula[f] RPAREN
     { f = MK_TERM(CVC4::api::STRING_LENGTH, f); }
   | STRING_CONTAINS_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
-    { f = MK_TERM(CVC4::api::STRING_STRCTN, f, f2); }
+    { f = MK_TERM(CVC4::api::STRING_CONTAINS, f, f2); }
   | STRING_SUBSTR_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN
     { f = MK_TERM(CVC4::api::STRING_SUBSTR, f, f2, f3); }
   | STRING_CHARAT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
     { f = MK_TERM(CVC4::api::STRING_CHARAT, f, f2); }
   | STRING_INDEXOF_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN
-    { f = MK_TERM(CVC4::api::STRING_STRIDOF, f, f2, f3); }
+    { f = MK_TERM(CVC4::api::STRING_INDEXOF, f, f2, f3); }
   | STRING_REPLACE_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN
-    { f = MK_TERM(CVC4::api::STRING_STRREPL, f, f2, f3); }
+    { f = MK_TERM(CVC4::api::STRING_REPLACE, f, f2, f3); }
   | STRING_REPLACE_ALL_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN
-    { f = MK_TERM(CVC4::api::STRING_STRREPLALL, f, f2, f3); }
+    { f = MK_TERM(CVC4::api::STRING_REPLACE_ALL, f, f2, f3); }
   | STRING_PREFIXOF_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
     { f = MK_TERM(CVC4::api::STRING_PREFIX, f, f2); }
   | STRING_SUFFIXOF_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
     { f = MK_TERM(CVC4::api::STRING_SUFFIX, f, f2); }
   | STRING_STOI_TOK LPAREN formula[f] RPAREN
-    { f = MK_TERM(CVC4::api::STRING_STOI, f); }
+    { f = MK_TERM(CVC4::api::STRING_TO_INT, f); }
   | STRING_ITOS_TOK LPAREN formula[f] RPAREN
-    { f = MK_TERM(CVC4::api::STRING_ITOS, f); }
+    { f = MK_TERM(CVC4::api::STRING_FROM_INT, f); }
   | STRING_TO_REGEXP_TOK LPAREN formula[f] RPAREN
     { f = MK_TERM(CVC4::api::STRING_TO_REGEXP, f); }
   | STRING_TOLOWER_TOK LPAREN formula[f] RPAREN

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 437f5aa2f7211174cf301e8bf4fd8d1517abee1c..91260d1db2a53cd6b24013577b953426c4c457e9 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -152,10 +152,10 @@ void Smt2::addStringOperators() {
   addOperator(api::STRING_CONCAT, "str.++");
   addOperator(api::STRING_LENGTH, "str.len");
   addOperator(api::STRING_SUBSTR, "str.substr");
-  addOperator(api::STRING_STRCTN, "str.contains");
+  addOperator(api::STRING_CONTAINS, "str.contains");
   addOperator(api::STRING_CHARAT, "str.at");
-  addOperator(api::STRING_STRIDOF, "str.indexof");
-  addOperator(api::STRING_STRREPL, "str.replace");
+  addOperator(api::STRING_INDEXOF, "str.indexof");
+  addOperator(api::STRING_REPLACE, "str.replace");
   if (!strictModeEnabled())
   {
     addOperator(api::STRING_TOLOWER, "str.tolower");
@@ -170,21 +170,21 @@ void Smt2::addStringOperators() {
   if (getLanguage() == language::input::LANG_SMTLIB_V2_6
       || getLanguage() == language::input::LANG_SYGUS_V2)
   {
-    addOperator(api::STRING_ITOS, "str.from_int");
-    addOperator(api::STRING_STOI, "str.to_int");
+    addOperator(api::STRING_FROM_INT, "str.from_int");
+    addOperator(api::STRING_TO_INT, "str.to_int");
     addOperator(api::STRING_IN_REGEXP, "str.in_re");
     addOperator(api::STRING_TO_REGEXP, "str.to_re");
     addOperator(api::STRING_TO_CODE, "str.to_code");
-    addOperator(api::STRING_STRREPLALL, "str.replace_all");
+    addOperator(api::STRING_REPLACE_ALL, "str.replace_all");
   }
   else
   {
-    addOperator(api::STRING_ITOS, "int.to.str");
-    addOperator(api::STRING_STOI, "str.to.int");
+    addOperator(api::STRING_FROM_INT, "int.to.str");
+    addOperator(api::STRING_TO_INT, "str.to.int");
     addOperator(api::STRING_IN_REGEXP, "str.in.re");
     addOperator(api::STRING_TO_REGEXP, "str.to.re");
     addOperator(api::STRING_TO_CODE, "str.code");
-    addOperator(api::STRING_STRREPLALL, "str.replaceall");
+    addOperator(api::STRING_REPLACE_ALL, "str.replaceall");
   }
 
   addOperator(api::REGEXP_CONCAT, "re.++");