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.

2 files changed, 104 insertions, 77 deletions

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]
   ;
-