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/cvc/Cvc.g | |
| 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/cvc/Cvc.g')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 12 |
1 files changed, 6 insertions, 6 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 |