From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Thu, 16 Apr 2015 04:04:50 +0000 (-0400)
Subject: update comment
X-Git-Tag: cvc5-1.0.0~6344^2~1^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8250ed75d47b4c1c230e45324f957dbd39c06595;p=cvc5.git

update comment
---

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]