diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-23 10:04:38 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-23 10:04:38 +0100 |
| commit | 7ff0098a91df9c912cbe98fb128fcf2cbc71e95c (patch) | |
| tree | 07aee959b4e48eda5ccc1580f4bc56adb7c53387 /src/parser | |
| parent | 732dc4232ccf62d9b4a3ddf49fcfbd56efabcd41 (diff) | |
Rework inst-closure.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 81e93ebe6..e536ed7cc 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2002,6 +2002,8 @@ builtinOp[CVC4::Kind& kind] | FMFCARD_TOK { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; } + | INST_CLOSURE_TOK { $kind = CVC4::kind::INST_CLOSURE; } + | FP_TOK { $kind = CVC4::kind::FLOATINGPOINT_FP; } | FP_EQ_TOK { $kind = CVC4::kind::FLOATINGPOINT_EQ; } | FP_ABS_TOK { $kind = CVC4::kind::FLOATINGPOINT_ABS; } @@ -2470,6 +2472,8 @@ DTSIZE_TOK : 'dt.size'; FMFCARD_TOK : 'fmf.card'; +INST_CLOSURE_TOK : 'inst-closure'; + EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset'; // Other set theory operators are not // tokenized and handled directly when |