summaryrefslogtreecommitdiff
path: root/src/parser/smt2/Smt2.g
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r--src/parser/smt2/Smt2.g4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 9c2ac4c1b..6e8e9ea00 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1280,6 +1280,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; }
+ | 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; }
@@ -1660,6 +1662,8 @@ STRIDOF_TOK : 'str.indexof' ;
STRREPL_TOK : 'str.replace' ;
STRPREF_TOK : 'str.prefixof' ;
STRSUFF_TOK : 'str.suffixof' ;
+STRITOS_TOK : 'int.to.str' ;
+STRSTOI_TOK : 'str.to.int' ;
STRINRE_TOK : 'str.in.re';
STRTORE_TOK : 'str.to.re';
RECON_TOK : 're.++';
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback