Addressed many of the concerns of bug 10 (build system code review).

Some parts split into other bugs: 19, 20, 21.

Addressed concerns of bug 11 (util package code review).

Slight parser source file modifications: file comments, #included
headers in generated parsers/lexers

Added CVC4::Result propagation back through
MiniSat->PropEngine->SmtEngine->main().  Silenced MiniSat when
verbosity is not requested.

8 files changed, 234 insertions, 175 deletions

diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 4fcaed14d..fe906cbe0 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -10,9 +10,6 @@
 #   set to zero if interfaces have been removed
 #   or changed
 #
-# LIBCVC4PARSER_RELEASE (-release) should match the CVC4 release version
-#
-LIBCVC4PARSER_RELEASE = @CVC4_LIBRARY_RELEASE_CODE@
 LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@
 
 AM_CPPFLAGS = \
@@ -25,7 +22,8 @@ SUBDIRS = smt cvc
 nobase_lib_LTLIBRARIES = libcvc4parser.la
 noinst_LTLIBRARIES = libcvc4parser_noinst.la
 
-libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS)
+libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS) \
+	-version-info $(LIBCVC4PARSER_VERSION)
 libcvc4parser_la_LIBADD = libcvc4parser_noinst.la
 libcvc4parser_la_LINK = $(CXXLINK)
 
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 3522bfd75..34bf4bc82 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -25,6 +25,7 @@
 #include "antlr_parser.h"
 #include "util/output.h"
 #include "util/Assert.h"
+#include "util/command.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index ae84318c8..a3015eb22 100644
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -25,11 +25,13 @@
 
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
-#include "util/command.h"
 #include "util/Assert.h"
 #include "parser/symbol_table.h"
 
 namespace CVC4 {
+
+class Command;
+
 namespace parser {
 
 /**
diff --git a/src/parser/cvc/cvc_lexer.g b/src/parser/cvc/cvc_lexer.g
index 52c58a38f..db40be3a8 100644
--- a/src/parser/cvc/cvc_lexer.g
+++ b/src/parser/cvc/cvc_lexer.g
@@ -1,12 +1,26 @@
+/* cvc_lexer.g
+ * Original author: dejan
+ * Major contributors:
+ * Minor contributors (to current version): none
+ * This file is part of the CVC4 prototype.
+ * Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ * Courant Institute of Mathematical Sciences
+ * New York University
+ * See the file COPYING in the top-level source directory for licensing
+ * information.
+ *
+ * Lexer for CVC presentation language.
+ */
+
 options {
   language = "Cpp";            // C++ output for antlr
   namespaceStd  = "std";       // Cosmetic option to get rid of long defines in generated code
   namespaceAntlr = "antlr";    // Cosmetic option to get rid of long defines in generated code
   namespace = "CVC4::parser";  // Wrap everything in the smtparser namespace
 }
-   
+
 /**
- * AntlrCvcLexer class is a stream tokenizer (lexer) for the CVC language. 
+ * AntlrCvcLexer class is a stream tokenizer (lexer) for the CVC language.
  */
 class AntlrCvcLexer extends Lexer;
 
@@ -14,15 +28,15 @@ options {
   exportVocab = CvcVocabulary;  // Name of the shared token vocabulary
   testLiterals = false;         // Do not check for literals by default
   defaultErrorHandler = false;  // Skip the defaul error handling, just break with exceptions
-  k = 2;  
+  k = 2;
 }
- 
+
 /*
  * The tokens that might match with the identifiers go here. Otherwise define
  * them below.
  */
 tokens {
-  // Types 
+  // Types
   BOOLEAN       = "BOOLEAN";
   // Boolean oparators
   AND           = "AND";
@@ -42,7 +56,7 @@ tokens {
   CHECKSAT      = "CHECKSAT";
   PRINT         = "PRINT";
   ECHO          = "ECHO";
-  
+
   PUSH          = "PUSH";
   POP           = "POP";
   POPTO         = "POPTO";
@@ -56,56 +70,56 @@ IFF     : "<=>";
 /**
  * Matches any letter ('a'-'z' and 'A'-'Z').
  */
-protected 
-ALPHA options { paraphrase = "a letter"; } 
-  : 'a'..'z' 
+protected
+ALPHA options { paraphrase = "a letter"; }
+  : 'a'..'z'
   | 'A'..'Z'
   ;
-  
+
 /**
  * Matches the digits (0-9)
  */
-protected 
-DIGIT options { paraphrase = "a digit"; } 
+protected
+DIGIT options { paraphrase = "a digit"; }
   : '0'..'9'
   ;
 
 /**
  * Matches the ':'
  */
-COLON options { paraphrase = "a colon"; } 
+COLON options { paraphrase = "a colon"; }
   : ':'
   ;
 
 /**
  * Matches the 'l'
  */
-SEMICOLON options { paraphrase = "a semicolon"; } 
+SEMICOLON options { paraphrase = "a semicolon"; }
   : ';'
   ;
 
 /**
  * Matches an identifier from the input. An identifier is a sequence of letters,
- * digits and "_", "'", "." symbols, starting with a letter. 
+ * digits and "_", "'", "." symbols, starting with a letter.
  */
 IDENTIFIER options { paraphrase = "an identifier"; testLiterals = true; }
   : ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*
   ;
-      
+
 /**
  * Matches the left bracket ('(').
  */
-LPAREN options { paraphrase = "a left parenthesis '('"; }      
+LPAREN options { paraphrase = "a left parenthesis '('"; }
   : '(';
-  
+
 /**
  * Matches the right bracket ('(').
  */
-RPAREN options { paraphrase = "a right parenthesis ')'"; }  
+RPAREN options { paraphrase = "a right parenthesis ')'"; }
   : ')';
 
 /**
- * Matches and skips whitespace in the input and ignores it. 
+ * Matches and skips whitespace in the input and ignores it.
  */
 WHITESPACE options { paraphrase = "whitespace"; }
   : (' ' | '\t' | '\f')              { $setType(antlr::Token::SKIP); }
@@ -114,7 +128,7 @@ WHITESPACE options { paraphrase = "whitespace"; }
 /**
  * Matches and skips the newline symbols in the input.
  */
-NEWLINE options { paraphrase = "a newline"; }  
+NEWLINE options { paraphrase = "a newline"; }
   : ('\r' '\n' | '\r' | '\n')       { $setType(antlr::Token::SKIP); newline(); }
   ;
 
@@ -124,11 +138,10 @@ NEWLINE options { paraphrase = "a newline"; }
 COMMENT options { paraphrase = "comment"; }
   : '%' (~('\n' | '\r'))*                    { $setType(antlr::Token::SKIP); }
   ;
-      
+
 /**
  * Matches a numeral from the input (non-empty sequence of digits).
  */
 NUMERAL options { paraphrase = "a numeral"; }
   : (DIGIT)+
   ;
-     
\ No newline at end of file
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index eb21283a3..ce61deae2 100644
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -1,24 +1,39 @@
+/* cvc_parser.g
+ * Original author: dejan
+ * Major contributors:
+ * Minor contributors (to current version): none
+ * This file is part of the CVC4 prototype.
+ * Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ * Courant Institute of Mathematical Sciences
+ * New York University
+ * See the file COPYING in the top-level source directory for licensing
+ * information.
+ *
+ * Parser for CVC presentation language.
+ */
+
 header "post_include_hpp" {
 #include "parser/antlr_parser.h"
+#include "util/command.h"
 }
 
 header "post_include_cpp" {
-#include <vector> 
+#include <vector>
 
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::parser;
 }
-    
+
 options {
   language = "Cpp";                  // C++ output for antlr
   namespaceStd = "std";              // Cosmetic option to get rid of long defines in generated code
   namespaceAntlr = "antlr";          // Cosmetic option to get rid of long defines in generated code
   namespace = "CVC4::parser";        // Wrap everything in the smtparser namespace
 }
- 
+
 /**
- * AntlrCvcParser class is the parser for the files in CVC format. 
+ * AntlrCvcParser class is the parser for the files in CVC format.
  */
 class AntlrCvcParser extends Parser("AntlrParser");
 options {
@@ -27,7 +42,7 @@ options {
   defaultErrorHandler = false;      // Skip the defaul error handling, just break with exceptions
   k = 2;
 }
- 
+
 /**
  * Parses the next command.
  * @return command or 0 if EOF
@@ -44,9 +59,9 @@ parseExpr returns [CVC4::Expr expr]
   : expr = formula
   | EOF
   ;
-  
+
 /**
- * Matches a command of the input. If a declaration, it will return an empty 
+ * Matches a command of the input. If a declaration, it will return an empty
  * command.
  */
 command returns [CVC4::Command* cmd = 0]
@@ -58,36 +73,36 @@ command returns [CVC4::Command* cmd = 0]
   | QUERY    f = formula  SEMICOLON { cmd = new QueryCommand(f);    }
   | CHECKSAT f = formula  SEMICOLON { cmd = new CheckSatCommand(f); }
   | CHECKSAT              SEMICOLON { cmd = new CheckSatCommand();  }
-  | identifierList[ids, CHECK_UNDECLARED] COLON type { 
+  | identifierList[ids, CHECK_UNDECLARED] COLON type {
       // FIXME: switch on type (may not be predicates)
       vector<string> sorts;
-      newPredicates(ids,sorts); 
-      cmd = new DeclarationCommand(ids); 
+      newPredicates(ids,sorts);
+      cmd = new DeclarationCommand(ids);
     }
     SEMICOLON
-  | EOF 
+  | EOF
   ;
 
 /**
- * Mathches a list of identifiers separated by a comma and puts them in the 
+ * Mathches a list of identifiers separated by a comma and puts them in the
  * given list.
  * @param idList the list to fill with identifiers.
- * @param check what kinds of check to perform on the symbols 
+ * @param check what kinds of check to perform on the symbols
  */
 identifierList[std::vector<std::string>& idList, DeclarationCheck check = CHECK_NONE]
 {
   string id;
 }
-  : id = identifier[check] { idList.push_back(id); } 
+  : id = identifier[check] { idList.push_back(id); }
       (COMMA id = identifier[check] { idList.push_back(id); })*
   ;
- 
+
 
 /**
  * Matches an identifier and returns a string.
  */
 identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id]
-  : x:IDENTIFIER 
+  : x:IDENTIFIER
     { id = x->getText(); }
     { checkDeclaration(id, check) }?
     exception catch [antlr::SemanticException& ex] {
@@ -95,11 +110,11 @@ identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id]
         case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared");
         case CHECK_UNDECLARED: rethrow(ex, "Symbol " + id + " already declared");
         default: throw ex;
-      }          
-    }    
+      }
+    }
   ;
-  
-/** 
+
+/**
  * Matches a type.
  * TODO: parse more types
  */
@@ -107,10 +122,10 @@ type
   : BOOLEAN
   ;
 
-/** 
+/**
  * Matches a CVC4 formula.
  * @return the expression representing the formula
- */ 
+ */
 formula returns [CVC4::Expr formula]
   :  formula = boolFormula
   ;
@@ -121,69 +136,69 @@ formula returns [CVC4::Expr formula]
  * createPrecedenceExpr method to build the expression using the precedence
  * and associativity of the operators.
  * @return the expression representing the formula
- */ 
+ */
 boolFormula returns [CVC4::Expr formula]
-  : formula = boolAndFormula 
+  : formula = boolAndFormula
   ;
 
 /**
- * Matches a Boolean AND formula of a given kind by doing a recursive descent. 
+ * Matches a Boolean AND formula of a given kind by doing a recursive descent.
  */
 boolAndFormula returns [CVC4::Expr andFormula]
 {
   Expr e;
   vector<Expr> exprs;
 }
-  : e = boolXorFormula { exprs.push_back(e); } 
+  : e = boolXorFormula { exprs.push_back(e); }
       ( AND e = boolXorFormula { exprs.push_back(e); } )*
-    { 
-      andFormula = (exprs.size() > 1 ? mkExpr(CVC4::AND, exprs) : exprs[0]); 
-    }  
+    {
+      andFormula = (exprs.size() > 1 ? mkExpr(CVC4::AND, exprs) : exprs[0]);
+    }
   ;
 
 /**
- * Matches a Boolean XOR formula of a given kind by doing a recursive descent. 
+ * Matches a Boolean XOR formula of a given kind by doing a recursive descent.
  */
 boolXorFormula returns [CVC4::Expr xorFormula]
 {
   Expr e;
   vector<Expr> exprs;
 }
-  : e = boolOrFormula { exprs.push_back(e); } 
+  : e = boolOrFormula { exprs.push_back(e); }
       ( XOR e = boolOrFormula { exprs.push_back(e); } )*
-    { 
-      xorFormula = (exprs.size() > 1 ? mkExpr(CVC4::XOR, exprs) : exprs[0]); 
-    }  
+    {
+      xorFormula = (exprs.size() > 1 ? mkExpr(CVC4::XOR, exprs) : exprs[0]);
+    }
   ;
 
 /**
- * Matches a Boolean OR formula of a given kind by doing a recursive descent. 
+ * Matches a Boolean OR formula of a given kind by doing a recursive descent.
  */
 boolOrFormula returns [CVC4::Expr orFormula]
 {
   Expr e;
   vector<Expr> exprs;
 }
-  : e = boolImpliesFormula { exprs.push_back(e); } 
+  : e = boolImpliesFormula { exprs.push_back(e); }
       ( OR e = boolImpliesFormula { exprs.push_back(e); } )*
-    { 
-      orFormula = (exprs.size() > 1 ? mkExpr(CVC4::OR, exprs) : exprs[0]); 
-    }  
+    {
+      orFormula = (exprs.size() > 1 ? mkExpr(CVC4::OR, exprs) : exprs[0]);
+    }
   ;
 
 /**
- * Matches a Boolean IMPLIES formula of a given kind by doing a recursive descent. 
+ * Matches a Boolean IMPLIES formula of a given kind by doing a recursive descent.
  */
 boolImpliesFormula returns [CVC4::Expr impliesFormula]
 {
   vector<Expr> exprs;
   Expr e;
 }
-  : e = boolIffFormula { exprs.push_back(e); } 
-    ( IMPLIES e = boolIffFormula { exprs.push_back(e); } 
+  : e = boolIffFormula { exprs.push_back(e); }
+    ( IMPLIES e = boolIffFormula { exprs.push_back(e); }
     )*
     {
-      impliesFormula = exprs.back(); 
+      impliesFormula = exprs.back();
       for (int i = exprs.size() - 2; i >= 0; -- i) {
         impliesFormula = mkExpr(CVC4::IMPLIES, exprs[i], impliesFormula);
       }
@@ -191,21 +206,21 @@ boolImpliesFormula returns [CVC4::Expr impliesFormula]
   ;
 
 /**
- * Matches a Boolean IFF formula of a given kind by doing a recursive descent. 
+ * Matches a Boolean IFF formula of a given kind by doing a recursive descent.
  */
 boolIffFormula returns [CVC4::Expr iffFormula]
 {
   Expr e;
 }
-  : iffFormula = primaryBoolFormula  
-    ( IFF e = primaryBoolFormula 
-        { iffFormula = mkExpr(CVC4::IFF, iffFormula, e); } 
+  : iffFormula = primaryBoolFormula
+    ( IFF e = primaryBoolFormula
+        { iffFormula = mkExpr(CVC4::IFF, iffFormula, e); }
     )*
   ;
-  
+
 /**
- * Parses a primary Boolean formula. A primary Boolean formula is either a 
- * Boolean atom (variables and predicates) a negation of a primary Boolean 
+ * Parses a primary Boolean formula. A primary Boolean formula is either a
+ * Boolean atom (variables and predicates) a negation of a primary Boolean
  * formula or a formula enclosed in parenthesis.
  * @return the expression representing the formula
  */
@@ -247,7 +262,7 @@ iteElseFormula returns [CVC4::Expr formula]
 /**
  * Parses the Boolean atoms (variables and predicates).
  * @return the expression representing the atom.
- */    
+ */
 boolAtom returns [CVC4::Expr atom]
 {
   string p;
@@ -259,13 +274,12 @@ boolAtom returns [CVC4::Expr atom]
   | TRUE  { atom = getTrueExpr(); }
   | FALSE { atom = getFalseExpr(); }
   ;
- 
+
 /**
  * Parses a predicate symbol (an identifier).
- * @param what kind of check to perform on the id 
+ * @param what kind of check to perform on the id
  * @return the predicate symol
  */
 predicateSymbol[DeclarationCheck check = CHECK_NONE] returns [std::string pSymbol]
   : pSymbol = identifier[check]
   ;
- 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 618b1c8ab..4f0502f24 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -18,10 +18,10 @@
 
 #include <string>
 #include <iostream>
+
 #include "cvc4_config.h"
 #include "parser/parser_exception.h"
 #include "util/Assert.h"
-#include "antlr_parser.h"
 
 namespace antlr {
   class CharScanner;
@@ -36,6 +36,8 @@ class ExprManager;
 
 namespace parser {
 
+class AntlrParser;
+
 /**
  * The parser. The parser should be obtained by calling the static methods
  * getNewParser, and should be deleted when done.
diff --git a/src/parser/smt/smt_lexer.g b/src/parser/smt/smt_lexer.g
index a82e54e30..e9abab61a 100644
--- a/src/parser/smt/smt_lexer.g
+++ b/src/parser/smt/smt_lexer.g
@@ -1,13 +1,27 @@
+/* smt_lexer.g
+ * Original author: dejan
+ * Major contributors:
+ * Minor contributors (to current version): none
+ * This file is part of the CVC4 prototype.
+ * Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ * Courant Institute of Mathematical Sciences
+ * New York University
+ * See the file COPYING in the top-level source directory for licensing
+ * information.
+ *
+ * Lexer for SMT-LIB input language.
+ */
+
 options {
   language = "Cpp";            // C++ output for antlr
   namespaceStd  = "std";       // Cosmetic option to get rid of long defines in generated code
   namespaceAntlr = "antlr";    // Cosmetic option to get rid of long defines in generated code
   namespace = "CVC4::parser";  // Wrap everything in the smtparser namespace
 }
-   
+
 /**
- * AntlrSmtLexer class is a stream tokenizer (lexer) for the SMT-LIB benchmark 
- * language. 
+ * AntlrSmtLexer class is a stream tokenizer (lexer) for the SMT-LIB benchmark
+ * language.
  */
 class AntlrSmtLexer extends Lexer;
 
@@ -15,9 +29,9 @@ options {
   exportVocab = SmtVocabulary;  // Name of the shared token vocabulary
   testLiterals = false;         // Do not check for literals by default
   defaultErrorHandler = false;  // Skip the default error handling, just break with exceptions
-  k = 2;  
+  k = 2;
 }
- 
+
 tokens {
   // Base SMT-LIB tokens
   DISTINCT      = "distinct";
@@ -55,28 +69,28 @@ tokens {
 /**
  * Matches any letter ('a'-'z' and 'A'-'Z').
  */
-protected 
-ALPHA options { paraphrase = "a letter"; } 
-  :  'a'..'z' 
+protected
+ALPHA options { paraphrase = "a letter"; }
+  :  'a'..'z'
   |  'A'..'Z'
   ;
-  
+
 /**
  * Matches the digits (0-9)
  */
-protected 
-DIGIT options { paraphrase = "a digit"; } 
+protected
+DIGIT options { paraphrase = "a digit"; }
   :   '0'..'9'
   ;
 
 /**
  * Matches an identifier from the input. An identifier is a sequence of letters,
- * digits and "_", "'", "." symbols, starting with a letter. 
+ * digits and "_", "'", "." symbols, starting with a letter.
  */
 IDENTIFIER options { paraphrase = "an identifier"; testLiterals = true; }
   :  ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*
   ;
-  
+
 /**
  * Matches an identifier starting with a colon. An identifier is a sequence of letters,
  * digits and "_", "'", "." symbols, starting with a colon.
@@ -84,47 +98,47 @@ IDENTIFIER options { paraphrase = "an identifier"; testLiterals = true; }
 C_IDENTIFIER options { paraphrase = "an identifier starting with a colon"; testLiterals = true; }
   :  ':' ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*
   ;
-  
+
 /**
  * Matches the value of user-defined annotations or attributes. The only constraint imposed on a user-defined value is that it start with
  * an open brace and end with closed brace.
  */
 USER_VALUE
-  :   '{' 
+  :   '{'
       ( '\n' { newline(); }
-      | ~('{' | '}' | '\n') 
-        )* 
+      | ~('{' | '}' | '\n')
+        )*
     '}'
   ;
-  
+
 /**
- * Matches the question mark symbol ('?'). 
+ * Matches the question mark symbol ('?').
  */
-QUESTION_MARK options { paraphrase = "a question mark '?'"; } 
+QUESTION_MARK options { paraphrase = "a question mark '?'"; }
   :  '?'
   ;
-  
+
 /**
  * Matches the dollar sign ('$').
  */
-DOLLAR_SIGN options { paraphrase = "a dollar sign '$'"; }   
+DOLLAR_SIGN options { paraphrase = "a dollar sign '$'"; }
   :  '$'
   ;
-    
+
 /**
  * Matches the left bracket ('(').
  */
-LPAREN options { paraphrase = "a left parenthesis '('"; }      
+LPAREN options { paraphrase = "a left parenthesis '('"; }
   :   '(';
-  
+
 /**
  * Matches the right bracket ('(').
  */
-RPAREN options { paraphrase = "a right parenthesis ')'"; }  
+RPAREN options { paraphrase = "a right parenthesis ')'"; }
   :   ')';
 
 /**
- * Matches and skips whitespace in the input. 
+ * Matches and skips whitespace in the input.
  */
 WHITESPACE options { paraphrase = "whitespace"; }
   :  (' ' | '\t' | '\f')              { $setType(antlr::Token::SKIP); }
@@ -133,32 +147,32 @@ WHITESPACE options { paraphrase = "whitespace"; }
 /**
  * Matches and skips the newline symbols in the input.
  */
-NEWLINE options { paraphrase = "a newline"; }  
+NEWLINE options { paraphrase = "a newline"; }
   :   ('\r' '\n' | '\r' | '\n')       { $setType(antlr::Token::SKIP); newline(); }
   ;
-      
+
 /**
  * Matches a numeral from the input (non-empty sequence of digits).
  */
 NUMERAL options { paraphrase = "a numeral"; }
   :  (DIGIT)+
   ;
-   
+
 /**
  * Matches an allowed escaped character.
- */   
+ */
 protected ESCAPE
   : '\\' ('"' | '\\' | 'n' | 't' | 'r')
-  ;      
-      
+  ;
+
 /**
  * Matches a double quoted string literal. Escaping is supported, and escape
- * character '\' has to be escaped. 
+ * character '\' has to be escaped.
  */
-STRING_LITERAL options { paraphrase = "a string literal"; } 
+STRING_LITERAL options { paraphrase = "a string literal"; }
   :  '"' (ESCAPE | ~('"'|'\\'))* '"'
   ;
-  
+
 /**
  * Matches the comments and ignores them
  */
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index 0db89d4f1..3933a04f0 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -1,24 +1,39 @@
+/* smt_parser.g
+ * Original author: dejan
+ * Major contributors:
+ * Minor contributors (to current version): none
+ * This file is part of the CVC4 prototype.
+ * Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ * Courant Institute of Mathematical Sciences
+ * New York University
+ * See the file COPYING in the top-level source directory for licensing
+ * information.
+ *
+ * Parser for SMT-LIB input language.
+ */
+
 header "post_include_hpp" {
 #include "parser/antlr_parser.h"
+#include "util/command.h"
 }
 
 header "post_include_cpp" {
-#include <vector> 
+#include <vector>
 
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::parser;
 }
-    
+
 options {
   language = "Cpp";                  // C++ output for antlr
   namespaceStd = "std";              // Cosmetic option to get rid of long defines in generated code
   namespaceAntlr = "antlr";          // Cosmetic option to get rid of long defines in generated code
   namespace = "CVC4::parser";        // Wrap everything in the smtparser namespace
 }
- 
+
 /**
- * AntlrSmtParser class is the parser for the SMT-LIB files. 
+ * AntlrSmtParser class is the parser for the SMT-LIB files.
  */
 class AntlrSmtParser extends Parser("AntlrParser");
 options {
@@ -43,50 +58,50 @@ parseExpr returns [CVC4::Expr expr]
  */
 parseCommand returns [CVC4::Command* cmd]
   : cmd = benchmark
-  ; 
- 
+  ;
+
 /**
  * Matches the whole SMT-LIB benchmark.
  * @return the sequence command containing the whole problem
- */  
+ */
 benchmark returns [Command* cmd]
   : LPAREN BENCHMARK IDENTIFIER cmd = benchAttributes RPAREN
-  | EOF { cmd = 0; } 
+  | EOF { cmd = 0; }
   ;
 
 /**
- * Matches a sequence of benchmark attributes and returns a pointer to a 
+ * Matches a sequence of benchmark attributes and returns a pointer to a
  * command sequence.
- * @return the command sequence 
+ * @return the command sequence
  */
 benchAttributes returns [CVC4::CommandSequence* cmd_seq = new CommandSequence()]
 {
   Command* cmd;
 }
-  : (cmd = benchAttribute { if (cmd) cmd_seq->addCommand(cmd); } )+ 
+  : (cmd = benchAttribute { if (cmd) cmd_seq->addCommand(cmd); } )+
   ;
-  
+
 /**
- * Matches a benchmark attribute, sucha as ':logic', ':formula', and returns 
+ * Matches a benchmark attribute, sucha as ':logic', ':formula', and returns
  * a corresponding command
  * @retrurn a command corresponding to the attribute
  */
 benchAttribute returns [Command* smt_command = 0]
 {
-  Expr formula;  
-  string logic; 
+  Expr formula;
+  string logic;
   SetBenchmarkStatusCommand::BenchmarkStatus b_status = SetBenchmarkStatusCommand::SMT_UNKNOWN;
 }
-  : LOGIC_ATTR logic = identifier 
-    { smt_command = new SetBenchmarkLogicCommand(logic);   }      
-  | ASSUMPTION_ATTR formula = annotatedFormula          
-    { smt_command = new AssertCommand(formula);   }       
-  | FORMULA_ATTR formula = annotatedFormula          
+  : LOGIC_ATTR logic = identifier
+    { smt_command = new SetBenchmarkLogicCommand(logic);   }
+  | ASSUMPTION_ATTR formula = annotatedFormula
+    { smt_command = new AssertCommand(formula);   }
+  | FORMULA_ATTR formula = annotatedFormula
     { smt_command = new CheckSatCommand(formula); }
-  | STATUS_ATTR b_status = status                   
-    { smt_command = new SetBenchmarkStatusCommand(b_status); }        
-  | EXTRAPREDS_ATTR LPAREN (predicateDeclaration)+ RPAREN  
-  | NOTES_ATTR STRING_LITERAL        
+  | STATUS_ATTR b_status = status
+    { smt_command = new SetBenchmarkStatusCommand(b_status); }
+  | EXTRAPREDS_ATTR LPAREN (predicateDeclaration)+ RPAREN
+  | NOTES_ATTR STRING_LITERAL
   | annotation
   ;
 
@@ -96,38 +111,38 @@ benchAttribute returns [Command* smt_command = 0]
  * @return the id string
  */
 identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id]
-  : x:IDENTIFIER 
+  : x:IDENTIFIER
     { id = x->getText(); }
-    { checkDeclaration(id, check) }? 
+    { checkDeclaration(id, check) }?
     exception catch [antlr::SemanticException& ex] {
       switch (check) {
         case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared");
         case CHECK_UNDECLARED: rethrow(ex, "Symbol " + id + " already declared");
         default: throw ex;
-      }          
-    }    
+      }
+    }
   ;
 
-/** 
+/**
  * Matches an annotated formula.
- * @return the expression representing the formula 
+ * @return the expression representing the formula
  */
-annotatedFormula returns [CVC4::Expr formula] 
-{ 
-  Kind kind; 
+annotatedFormula returns [CVC4::Expr formula]
+{
+  Kind kind;
   vector<Expr> children;
 }
-  :  formula = annotatedAtom 
-  |  LPAREN kind = boolConnective annotatedFormulas[children] RPAREN { formula = mkExpr(kind, children);  }    
+  :  formula = annotatedAtom
+  |  LPAREN kind = boolConnective annotatedFormulas[children] RPAREN { formula = mkExpr(kind, children);  }
   ;
 
 /**
- * Matches an annotated proposition atom, which is either a propositional atom 
- * or built of other atoms using a predicate symbol.  
+ * Matches an annotated proposition atom, which is either a propositional atom
+ * or built of other atoms using a predicate symbol.
  * @return expression representing the atom
  */
-annotatedAtom returns [CVC4::Expr atom] 
-  : atom = propositionalAtom  
+annotatedAtom returns [CVC4::Expr atom]
+  : atom = propositionalAtom
   ;
 
 /**
@@ -135,7 +150,7 @@ annotatedAtom returns [CVC4::Expr atom]
 * @return the kind of the Bollean connective
 */
 boolConnective returns [CVC4::Kind kind]
-  : NOT      { kind = CVC4::NOT;     } 
+  : NOT      { kind = CVC4::NOT;     }
   | IMPLIES  { kind = CVC4::IMPLIES; }
   | AND      { kind = CVC4::AND;     }
   | OR       { kind = CVC4::OR;      }
@@ -147,7 +162,7 @@ boolConnective returns [CVC4::Kind kind]
  * Mathces a sequence of annotaed formulas and puts them into the formulas
  * vector.
  * @param formulas the vector to fill with formulas
- */   
+ */
 annotatedFormulas[std::vector<Expr>& formulas]
 {
   Expr f;
@@ -157,40 +172,40 @@ annotatedFormulas[std::vector<Expr>& formulas]
 
 /**
  * Matches a propositional atom and returns the expression of the atom.
- * @return atom the expression of the atom 
+ * @return atom the expression of the atom
  */
 propositionalAtom returns [CVC4::Expr atom]
 {
   std::string p;
-} 
+}
    : p = predicateName[CHECK_DECLARED] { atom = getVariable(p); }
    | TRUE          { atom = getTrueExpr(); }
    | FALSE         { atom = getFalseExpr(); }
    ;
 
 /**
- * Matches a predicate symbol. 
+ * Matches a predicate symbol.
  * @param check what kind of check to do with the symbol
  */
 predicateName[DeclarationCheck check = CHECK_NONE] returns [std::string p]
   :  p = identifier[check]
   ;
-  
+
 /**
  * Matches an attribute name from the input (:attribute_name).
- */ 
-attribute 
+ */
+attribute
   :  C_IDENTIFIER
   ;
-      
+
 /**
  * Matches the sort symbol, which can be an arbitrary identifier.
  * @param check the check to perform on the name
  */
-sortName[DeclarationCheck check = CHECK_NONE] returns [std::string s] 
+sortName[DeclarationCheck check = CHECK_NONE] returns [std::string s]
   : s = identifier[check]
   ;
-              
+
 /**
  * Matches the declaration of a predicate and declares it
  */
@@ -199,9 +214,9 @@ predicateDeclaration
   string p_name;
   vector<string> p_sorts;
 }
-  :  LPAREN p_name = predicateName[CHECK_UNDECLARED] sortNames[p_sorts] RPAREN { newPredicate(p_name, p_sorts); } 
+  :  LPAREN p_name = predicateName[CHECK_UNDECLARED] sortNames[p_sorts] RPAREN { newPredicate(p_name, p_sorts); }
   ;
-  
+
 /**
  * Matches a sequence of sort symbols and fills them into the given vector.
  */
@@ -209,7 +224,7 @@ sortNames[std::vector<std::string>& sorts]
 {
   std::string sort;
 }
-  : ( sort = sortName[CHECK_UNDECLARED] { sorts.push_back(sort); })* 
+  : ( sort = sortName[CHECK_UNDECLARED] { sorts.push_back(sort); })*
   ;
 
 /**
@@ -222,9 +237,9 @@ status returns [ SetBenchmarkStatusCommand::BenchmarkStatus status ]
   ;
 
 /**
- * Matches an annotation, which is an attribute name, with an optional user 
+ * Matches an annotation, which is an attribute name, with an optional user
  */
-annotation 
+annotation
   : attribute (USER_VALUE)?
   ;
-    
+