diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-24 14:45:06 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-26 11:30:05 -0600 |
| commit | bf17613c183531217ff5f95741c2216cfb67ee36 (patch) | |
| tree | e48f1de8a80fe4425d26576d43b81d1b6bbfb234 /src/parser/cvc/Cvc.g | |
| parent | c8a989214aaca61697b08c48102971a86c2e399d (diff) | |
smt-lib syntax change: str.contain -> str.contains; add some prefix syntax for cvc format
Diffstat (limited to 'src/parser/cvc/Cvc.g')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 78be92966..792c3cf9d 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -199,6 +199,15 @@ tokens { STRING_TOK = 'STRING'; SCONCAT_TOK = 'SCONCAT'; + SCONTAINS_TOK = 'CONTAINS'; + SSUBSTR_TOK = 'SUBSTR'; + SINDEXOF_TOK = 'INDEXOF'; + SREPLACE_TOK = 'REPLACE'; + SPREFIXOF_TOK = 'PREFIXOF'; + SSUFFIXOF_TOK = 'SUFFIXOF'; + STOINTEGER_TOK = 'TO_INTEGER'; + STOSTRING_TOK = 'TO_STRING'; + STORE_TOK = 'TO_RE'; // these are parsed by special NUMBER_OR_RANGEOP rule, below DECIMAL_LITERAL; @@ -1824,6 +1833,7 @@ bvTerm[CVC4::Expr& f] stringTerm[CVC4::Expr& f] @init { Expr f2; + Expr f3; std::string s; std::vector<Expr> args; } @@ -1831,6 +1841,24 @@ stringTerm[CVC4::Expr& f] : SCONCAT_TOK LPAREN formula[f] { args.push_back(f); } ( COMMA formula[f2] { args.push_back(f2); } )+ RPAREN { f = MK_EXPR(CVC4::kind::STRING_CONCAT, args); } + | SCONTAINS_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::STRING_STRCTN, f, f2); } + | SSUBSTR_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN + { f = MK_EXPR(CVC4::kind::STRING_SUBSTR, f, f2, f3); } + | SINDEXOF_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN + { f = MK_EXPR(CVC4::kind::STRING_STRIDOF, f, f2, f3); } + | SREPLACE_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN + { f = MK_EXPR(CVC4::kind::STRING_STRREPL, f, f2, f3); } + | SPREFIXOF_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::STRING_PREFIX, f, f2); } + | SSUFFIXOF_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::STRING_SUFFIX, f, f2); } + | STOINTEGER_TOK LPAREN formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::STRING_STOI, f); } + | STOSTRING_TOK LPAREN formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::STRING_ITOS, f); } + | STORE_TOK LPAREN formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::STRING_TO_REGEXP, f); } /* string literal */ | str[s] |