diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-05-21 23:40:44 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-05-21 23:40:44 -0500 |
| commit | 026f7ae7bb3678281fb46defff4a1202c69d5f4e (patch) | |
| tree | 46789ea4793e51f8f7154a7422c44d8d74457c48 /src/parser | |
| parent | 0f9b0dd69bef6a108b1ccc185223733f1d8fa40d (diff) | |
Update string kind names in new API (#4509)
To match the smt2 Unicode standard. The internal ones are left unchanged for now.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 12 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 18 |
2 files changed, 15 insertions, 15 deletions
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.++"); |