summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
authorTianyi Liang <tianyi-liang@uiowa.edu>2014-01-29 10:32:17 -0600
committerTianyi Liang <tianyi-liang@uiowa.edu>2014-01-29 10:32:17 -0600
commit8c4a79a1dfc47572e81506cc1de9372370199f74 (patch)
tree61ed1305e95a65f8add66aa50d22681e6dbf8d45 /src/parser
parent6b2b7c90c9dccb596181fcf399a8830b05db5408 (diff)
add prefixof, suffixof
Diffstat (limited to 'src/parser')
-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 497705cb6..1bfae498a 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1256,6 +1256,8 @@ builtinOp[CVC4::Kind& kind]
| STRCAT_TOK { $kind = CVC4::kind::STRING_CHARAT; }
| STRIDOF_TOK { $kind = CVC4::kind::STRING_STRIDOF; }
| STRREPL_TOK { $kind = CVC4::kind::STRING_STRREPL; }
+ | STRPREF_TOK { $kind = CVC4::kind::STRING_PREFIX; }
+ | STRSUFF_TOK { $kind = CVC4::kind::STRING_SUFFIX; }
| STRINRE_TOK { $kind = CVC4::kind::STRING_IN_REGEXP; }
| STRTORE_TOK { $kind = CVC4::kind::STRING_TO_REGEXP; }
| RECON_TOK { $kind = CVC4::kind::REGEXP_CONCAT; }
@@ -1634,6 +1636,8 @@ STRCTN_TOK : 'str.contain' ;
STRCAT_TOK : 'str.at' ;
STRIDOF_TOK : 'str.indexof' ;
STRREPL_TOK : 'str.replace' ;
+STRPREF_TOK : 'str.prefixof' ;
+STRSUFF_TOK : 'str.suffixof' ;
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