summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
authorTianyi Liang <tianyi-liang@uiowa.edu>2014-01-09 16:23:59 -0600
committerTianyi Liang <tianyi-liang@uiowa.edu>2014-01-09 16:24:43 -0600
commit12dae128053342fef8af2f560fd98e1ab6a71cca (patch)
tree96d854b38d819affe72d551aee70315821e21e57 /src/parser
parent780448ae48ed8755b11570a6843ab6871d94abef (diff)
add constant replace, indexof
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/smt2/Smt2.g6
1 files changed, 4 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 39329e424..497705cb6 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1254,6 +1254,8 @@ builtinOp[CVC4::Kind& kind]
| STRSUB_TOK { $kind = CVC4::kind::STRING_SUBSTR; }
| STRCTN_TOK { $kind = CVC4::kind::STRING_STRCTN; }
| STRCAT_TOK { $kind = CVC4::kind::STRING_CHARAT; }
+ | STRIDOF_TOK { $kind = CVC4::kind::STRING_STRIDOF; }
+ | STRREPL_TOK { $kind = CVC4::kind::STRING_STRREPL; }
| STRINRE_TOK { $kind = CVC4::kind::STRING_IN_REGEXP; }
| STRTORE_TOK { $kind = CVC4::kind::STRING_TO_REGEXP; }
| RECON_TOK { $kind = CVC4::kind::REGEXP_CONCAT; }
@@ -1630,8 +1632,8 @@ STRLEN_TOK : 'str.len';
STRSUB_TOK : 'str.substr' ;
STRCTN_TOK : 'str.contain' ;
STRCAT_TOK : 'str.at' ;
-//STRIDOF_TOK : 'str.indexof' ;
-//STRREPL_TOK : 'str.repalce' ;
+STRIDOF_TOK : 'str.indexof' ;
+STRREPL_TOK : 'str.replace' ;
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