diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-28 22:56:45 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-28 22:59:00 -0600 |
| commit | 0e7bfa71e7bea8b832df00d00332b42bf8bca60b (patch) | |
| tree | ce0ac17a6c67030f36b1fa662535a0e84233da29 /src/parser | |
| parent | fb4104e7c5a88741f9ffd55384198af31435df9e (diff) | |
add re.nostr for the empty regular expression; add re.allchar for the regular expresssion containing all charactors
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 873f3dce6..6e9f04ce9 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1032,6 +1032,12 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] | str[s,false] { expr = MK_CONST( ::CVC4::String(s) ); } + | RENOSTR_TOK + { std::vector< Expr > nvec; expr = MK_EXPR( CVC4::kind::REGEXP_EMPTY, nvec ); } + + | REALLCHAR_TOK + { std::vector< Expr > nvec; expr = MK_EXPR( CVC4::kind::REGEXP_SIGMA, nvec ); } + | EMPTYSET_TOK { expr = MK_CONST( ::CVC4::EmptySet()); } @@ -1294,12 +1300,12 @@ builtinOp[CVC4::Kind& kind] | STRREPL_TOK { $kind = CVC4::kind::STRING_STRREPL; } | STRPREF_TOK { $kind = CVC4::kind::STRING_PREFIX; } | STRSUFF_TOK { $kind = CVC4::kind::STRING_SUFFIX; } - | STRITOS_TOK { $kind = CVC4::kind::STRING_ITOS; } - | STRSTOI_TOK { $kind = CVC4::kind::STRING_STOI; } + | STRITOS_TOK { $kind = CVC4::kind::STRING_ITOS; } + | STRSTOI_TOK { $kind = CVC4::kind::STRING_STOI; } | STRINRE_TOK { $kind = CVC4::kind::STRING_IN_REGEXP; } | STRTORE_TOK { $kind = CVC4::kind::STRING_TO_REGEXP; } | RECON_TOK { $kind = CVC4::kind::REGEXP_CONCAT; } - | REUNION_TOK { $kind = CVC4::kind::REGEXP_UNION; } + | REUNION_TOK { $kind = CVC4::kind::REGEXP_UNION; } | REINTER_TOK { $kind = CVC4::kind::REGEXP_INTER; } | RESTAR_TOK { $kind = CVC4::kind::REGEXP_STAR; } | REPLUS_TOK { $kind = CVC4::kind::REGEXP_PLUS; } @@ -1705,6 +1711,8 @@ RESTAR_TOK : 're.*'; REPLUS_TOK : 're.+'; REOPT_TOK : 're.opt'; RERANGE_TOK : 're.range'; +RENOSTR_TOK : 're.nostr'; +REALLCHAR_TOK : 're.allchar'; SETUNION_TOK: 'union'; SETINT_TOK: 'intersection'; |