diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-24 14:45:06 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-26 11:30:05 -0600 |
| commit | bf17613c183531217ff5f95741c2216cfb67ee36 (patch) | |
| tree | e48f1de8a80fe4425d26576d43b81d1b6bbfb234 /src/parser/smt2 | |
| parent | c8a989214aaca61697b08c48102971a86c2e399d (diff) | |
smt-lib syntax change: str.contain -> str.contains; add some prefix syntax for cvc format
Diffstat (limited to 'src/parser/smt2')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index f1888de39..9b598e113 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1294,8 +1294,8 @@ builtinOp[CVC4::Kind& kind] | STRREPL_TOK { $kind = CVC4::kind::STRING_STRREPL; } | STRPREF_TOK { $kind = CVC4::kind::STRING_PREFIX; } | STRSUFF_TOK { $kind = CVC4::kind::STRING_SUFFIX; } - | SITOS_TOK { $kind = CVC4::kind::STRING_ITOS; } - | SSTOI_TOK { $kind = CVC4::kind::STRING_STOI; } + | STRITOS_TOK { $kind = CVC4::kind::STRING_ITOS; } + | STRSTOI_TOK { $kind = CVC4::kind::STRING_STOI; } | STRINRE_TOK { $kind = CVC4::kind::STRING_IN_REGEXP; } | STRTORE_TOK { $kind = CVC4::kind::STRING_TO_REGEXP; } | RECON_TOK { $kind = CVC4::kind::REGEXP_CONCAT; } @@ -1688,14 +1688,14 @@ INT2BV_TOK : 'int2bv'; STRCON_TOK : 'str.++'; STRLEN_TOK : 'str.len'; STRSUB_TOK : 'str.substr' ; -STRCTN_TOK : 'str.contain' ; +STRCTN_TOK : 'str.contains' ; STRCAT_TOK : 'str.at' ; STRIDOF_TOK : 'str.indexof' ; STRREPL_TOK : 'str.replace' ; STRPREF_TOK : 'str.prefixof' ; STRSUFF_TOK : 'str.suffixof' ; -SITOS_TOK : 'int.to.str' ; -SSTOI_TOK : 'str.to.int' ; +STRITOS_TOK : 'int.to.str' ; +STRSTOI_TOK : 'str.to.int' ; STRINRE_TOK : 'str.in.re'; STRTORE_TOK : 'str.to.re'; RECON_TOK : 're.++'; |