diff options
Diffstat (limited to 'src/parser/cvc/Cvc.g')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 3eddf438f..29bc84510 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -222,6 +222,7 @@ tokens { STRING_CHARAT_TOK = 'CHARAT'; STRING_INDEXOF_TOK = 'INDEXOF'; STRING_REPLACE_TOK = 'REPLACE'; + STRING_REPLACE_ALL_TOK = 'REPLACE_ALL'; STRING_PREFIXOF_TOK = 'PREFIXOF'; STRING_SUFFIXOF_TOK = 'SUFFIXOF'; STRING_STOI_TOK = 'STRING_TO_INTEGER'; @@ -2028,6 +2029,8 @@ stringTerm[CVC4::Expr& f] { f = MK_EXPR(CVC4::kind::STRING_STRIDOF, f, f2, f3); } | STRING_REPLACE_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN { f = MK_EXPR(CVC4::kind::STRING_STRREPL, f, f2, f3); } + | STRING_REPLACE_ALL_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN + { f = MK_EXPR(CVC4::kind::STRING_STRREPLALL, f, f2, f3); } | STRING_PREFIXOF_TOK LPAREN formula[f] COMMA formula[f2] RPAREN { f = MK_EXPR(CVC4::kind::STRING_PREFIX, f, f2); } | STRING_SUFFIXOF_TOK LPAREN formula[f] COMMA formula[f2] RPAREN |