diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-04-16 00:04:50 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-04-16 00:04:50 -0400 |
| commit | 8250ed75d47b4c1c230e45324f957dbd39c06595 (patch) | |
| tree | 6db4ac294b657590b4d6a0f909da41148db365ad /src/parser | |
| parent | e439cc095fdef2991fd41c5350de18dc96eb16b7 (diff) | |
update comment
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 0fa048763..78fd510fb 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2044,12 +2044,15 @@ builtinOp[CVC4::Kind& kind] } } | DTSIZE_TOK { $kind = CVC4::kind::DT_SIZE; } - | FMFCARD_TOK { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; } - | INST_CLOSURE_TOK { $kind = CVC4::kind::INST_CLOSURE; } - // NOTE: Theory operators go here + // NOTE: Theory operators no longer go here, add to smt2.cpp. Only + // special cases may go here. When this comment was written (2015 + // Apr), the special cases were: core theory operators, arith + // operators which start with symbols like * / + >= etc, quantifier + // theory operators, and operators which depended on parser's state + // to accept or reject. ; quantOp[CVC4::Kind& kind] |