summaryrefslogtreecommitdiff
path: root/src/parser/smt2/Smt2.g
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r--src/parser/smt2/Smt2.g4
1 files changed, 0 insertions, 4 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index a83299d3b..81e93ebe6 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2002,8 +2002,6 @@ 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; }
@@ -2472,8 +2470,6 @@ 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback