diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-11-21 14:44:44 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-11-21 14:44:44 -0600 |
commit | 2c05402119dba7e90e24621c5768514ab2f5042c (patch) | |
tree | cec74ac8b51d20c622205bfa39e6ef6e44d510dc /src/parser | |
parent | b3b1fffb390d19312227d7095fb404e9e0447d95 (diff) |
Support string replace all (#2704)
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 3 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 1 |
2 files changed, 4 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 diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 2fd61aabc..d52dd948b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -129,6 +129,7 @@ void Smt2::addStringOperators() { addOperator(kind::STRING_CHARAT, "str.at" ); addOperator(kind::STRING_STRIDOF, "str.indexof" ); addOperator(kind::STRING_STRREPL, "str.replace" ); + addOperator(kind::STRING_STRREPLALL, "str.replaceall"); addOperator(kind::STRING_PREFIX, "str.prefixof" ); addOperator(kind::STRING_SUFFIX, "str.suffixof" ); // at the moment, we only use this syntax for smt2.6.1 |