Adding a bit of documentation to the SMT parser

2 files changed, 63 insertions, 68 deletions

diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp
index 57914c9de..827d5fcaa 100644
--- a/src/parser/parser_state.cpp
+++ b/src/parser/parser_state.cpp
@@ -46,7 +46,6 @@ ParserState::ParserState(ExprManager* exprManager, const std::string& filename,
 Expr ParserState::getSymbol(const std::string& name, SymbolType type) {
   Assert( isDeclared(name, type) );
 
-
   switch( type ) {
 
   case SYM_VARIABLE: // Functions share var namespace
@@ -125,15 +124,6 @@ ParserState::undefineVar(const std::string& name) {
 }
 */
 
-void
-ParserState::setLogic(const std::string& name) {
-  if( name == "QF_UF" ) {
-    mkSort("U");
-  } else {
-    Unhandled(name);
-  }
-}
-
 Type
 ParserState::mkSort(const std::string& name) {
   Debug("parser") << "newSort(" << name << ")" << std::endl;
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 15f0c8844..67290ada2 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -77,6 +77,22 @@ using namespace CVC4::parser;
 #define MK_EXPR EXPR_MANAGER->mkExpr
 #undef MK_CONST
 #define MK_CONST EXPR_MANAGER->mkConst
+
+/**   
+ * Sets the logic for the current benchmark. Declares any logic symbols.
+ *
+ * @param parserState pointer to the current parser state
+ * @param name the name of the logic (e.g., QF_UF, AUFLIA)
+ */
+void
+setLogic(ParserState *parserState, const std::string& name) {
+  if( name == "QF_UF" ) {
+    parserState->mkSort("U");
+  } else {
+    // NOTE: Theory types go here
+    Unhandled(name);
+  }
+}
 }
 
 
@@ -131,7 +147,7 @@ benchAttribute returns [CVC4::Command* smt_command]
   Expr expr;
 }
   : LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE]
-    { PARSER_STATE->setLogic(name);
+    { setLogic(PARSER_STATE,name);
       smt_command = new SetBenchmarkLogicCommand(name);   }
   | ASSUMPTION_TOK annotatedFormula[expr]
     { smt_command = new AssertCommand(expr);   }
@@ -183,7 +199,7 @@ annotatedFormula[CVC4::Expr& expr]
     { expr = MK_EXPR(CVC4::kind::APPLY_UF,args); }
 
   | /* An ite expression */
-    LPAREN_TOK (ITE_TOK | IF_THEN_ELSE_TOK) 
+    LPAREN_TOK ITE_TOK 
     annotatedFormula[expr]
     { args.push_back(expr); } 
     annotatedFormula[expr]
@@ -213,6 +229,7 @@ annotatedFormula[CVC4::Expr& expr]
     /* constants */
   | TRUE_TOK          { expr = MK_CONST(true); }
   | FALSE_TOK         { expr = MK_CONST(false); }
+    // NOTE: Theory constants go here
     /* TODO: let, flet, quantifiers, arithmetic constants */
   ;
 
@@ -229,8 +246,7 @@ annotatedFormulas[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
   ;
 
 /**
-* Matches on of the unary Boolean connectives.
-* @return the kind of the Bollean connective
+* Matches a builtin operator symbol and sets kind to its associated Expr kind.
 */
 builtinOp[CVC4::Kind& kind]
 @init {
@@ -244,6 +260,7 @@ builtinOp[CVC4::Kind& kind]
   | IFF_TOK      { $kind = CVC4::kind::IFF;     }
   | EQUAL_TOK    { $kind = CVC4::kind::EQUAL;   }
   | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; }
+    // NOTE: Theory operators go here
     /* TODO: lt, gt, plus, minus, etc. */
   ;
 
@@ -410,72 +427,65 @@ flet_identifier[std::string& id,
       PARSER_STATE->checkDeclaration(id, check); }
   ;
 
-
 // Base SMT-LIB tokens
-DISTINCT_TOK      : 'distinct';
-ITE_TOK           : 'ite';
-IF_THEN_ELSE_TOK  : 'if_then_else';
-TRUE_TOK          : 'true';
-FALSE_TOK         : 'false';
-NOT_TOK           : 'not';
-IMPLIES_TOK       : 'implies';
-AND_TOK           : 'and';
-OR_TOK            : 'or';
-XOR_TOK           : 'xor';
-IFF_TOK           : 'iff';
-EXISTS_TOK        : 'exists';
-FORALL_TOK        : 'forall';
-LET_TOK           : 'let';
-FLET_TOK          : 'flet';
-THEORY_TOK        : 'theory';
-SAT_TOK           : 'sat';
-UNSAT_TOK         : 'unsat';
-UNKNOWN_TOK       : 'unknown';
-BENCHMARK_TOK     : 'benchmark';
-
-// The SMT attribute tokens
-LOGIC_TOK       : ':logic';
 ASSUMPTION_TOK  : ':assumption';
-FORMULA_TOK     : ':formula';
-STATUS_TOK      : ':status';
-EXTRASORTS_TOK  : ':extrasorts';
+BENCHMARK_TOK   : 'benchmark';
 EXTRAFUNS_TOK   : ':extrafuns';
 EXTRAPREDS_TOK  : ':extrapreds';
+EXTRASORTS_TOK  : ':extrasorts';
+FALSE_TOK       : 'false';
+FLET_TOK        : 'flet';
+FORMULA_TOK     : ':formula';
+ITE_TOK         : 'ite' | 'if_then_else';
+LET_TOK         : 'let';
+LOGIC_TOK       : ':logic';
+LPAREN_TOK      : '(';
 NOTES_TOK       : ':notes';
+RPAREN_TOK      : ')';
+SAT_TOK         : 'sat';
+STATUS_TOK      : ':status';
+THEORY_TOK      : 'theory';
+TRUE_TOK        : 'true';
+UNKNOWN_TOK     : 'unknown';
+UNSAT_TOK       : 'unsat';
 
-// arithmetic symbols
-EQUAL_TOK         : '=';
-LESS_THAN_TOK     : '<';
-GREATER_THAN_TOK  : '>';
+// operators (NOTE: theory symbols go here)
 AMPERSAND_TOK     : '&';
+AND_TOK           : 'and';
 AT_TOK            : '@';
-POUND_TOK         : '#';
-PLUS_TOK          : '+';
-MINUS_TOK         : '-';
-STAR_TOK          : '*';
+DISTINCT_TOK      : 'distinct';
 DIV_TOK           : '/';
+EQUAL_TOK         : '=';
+EXISTS_TOK        : 'exists';
+FORALL_TOK        : 'forall';
+GREATER_THAN_TOK  : '>';
+IFF_TOK           : 'iff';
+IMPLIES_TOK       : 'implies';
+LESS_THAN_TOK     : '<';
+MINUS_TOK         : '-';
+NOT_TOK           : 'not';
+OR_TOK            : 'or';
 PERCENT_TOK       : '%';
 PIPE_TOK          : '|';
+PLUS_TOK          : '+';
+POUND_TOK         : '#';
+STAR_TOK          : '*';
 TILDE_TOK         : '~';
+XOR_TOK           : 'xor';
 
-// Language meta-symbols
-//QUESTION_TOK      : '?';
-//DOLLAR_TOK        : '$';
-LPAREN_TOK        : '(';
-RPAREN_TOK        : ')';
 
 /**
  * Matches an identifier from the input. An identifier is a sequence of letters,
  * digits and "_", "'", "." symbols, starting with a letter.
  */
-IDENTIFIER /*options { paraphrase = 'an identifier'; testLiterals = true; }*/
+IDENTIFIER
   :  ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*
   ;
 
 /**
  * Matches an identifier starting with a colon.
  */
-ATTR_IDENTIFIER /*options { paraphrase = 'an identifier starting with a colon'; testLiterals = true; }*/
+ATTR_IDENTIFIER 
   :  ':' IDENTIFIER
   ;
 
@@ -507,14 +517,14 @@ USER_VALUE
 /**
  * Matches and skips whitespace in the input.
  */
-WHITESPACE /*options { paraphrase = 'whitespace'; }*/
+WHITESPACE
   :  (' ' | '\t' | '\f' | '\r' | '\n')+             { $channel = HIDDEN;; }
   ;
 
 /**
  * Matches a numeral from the input (non-empty sequence of digits).
  */
-NUMERAL_TOK /*options { paraphrase = 'a numeral'; }*/
+NUMERAL_TOK
   :  (DIGIT)+
   ;
 
@@ -522,14 +532,14 @@ NUMERAL_TOK /*options { paraphrase = 'a numeral'; }*/
  * Matches a double quoted string literal. Escaping is supported, and escape
  * character '\' has to be escaped.
  */
-STRING_LITERAL /*options { paraphrase = 'a string literal'; }*/
+STRING_LITERAL 
   :  '"' (ESCAPE | ~('"'|'\\'))* '"'
   ;
 
 /**
  * Matches the comments and ignores them
  */
-COMMENT /*options { paraphrase = 'comment'; }*/
+COMMENT 
   : ';' (~('\n' | '\r'))*                    { $channel = HIDDEN;; }
   ;
 
@@ -538,7 +548,7 @@ COMMENT /*options { paraphrase = 'comment'; }*/
  * Matches any letter ('a'-'z' and 'A'-'Z').
  */
 fragment
-ALPHA /*options { paraphrase = 'a letter'; }*/
+ALPHA 
   :  'a'..'z'
   |  'A'..'Z'
   ;
@@ -546,16 +556,11 @@ ALPHA /*options { paraphrase = 'a letter'; }*/
 /**
  * Matches the digits (0-9)
  */
-fragment
-DIGIT /*options { paraphrase = 'a digit'; }*/
-  :   '0'..'9'
-  ;
+fragment DIGIT :   '0'..'9';
 
 
 /**
  * Matches an allowed escaped character.
  */
-fragment ESCAPE
-  : '\\' ('"' | '\\' | 'n' | 't' | 'r')
-  ;
+fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r');