From: Andrew Reynolds Date: Fri, 22 May 2020 04:40:44 +0000 (-0500) Subject: Update string kind names in new API (#4509) X-Git-Tag: cvc5-1.0.0~3302 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=026f7ae7bb3678281fb46defff4a1202c69d5f4e;p=cvc5.git 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 d990b3e22..052b62efc 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -253,10 +253,10 @@ const static std::unordered_map 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 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::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::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 05423a952..e084daf1e 100644 --- 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& 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& 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& 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& 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 7babf2e56..8e4152e2e 100644 --- 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 437f5aa2f..91260d1db 100644 --- 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.++");