Tuesday end-of-day commit.

Expected performance impact outside of datatypes/CVC parser is
negligible.

* CVC language LAMBDA, functional LET, type LET, precedence fixes,
  bitvectors, and arrays, with partial parsing support also for
  quantifiers, tuples, subranges, subtypes, and records
* support for complex recursive DATATYPE selectors, e.g.
    tree = node(children:ARRAY INT OF tree) | leaf(data:INT)
  these are complicated because they have to be left unresolved
  at parse time and dealt with in a second pass.
* bugfix for Exprs/Types that occurred when setting them to null
  (not Nodes/TypeNodes, just Exprs/Types).
* Cleanup/code review items

4 files changed, 16 insertions, 11 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index d27abc735..4f141891b 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -673,8 +673,8 @@ symbol[std::string& id,
   : SYMBOL
     { id = AntlrInput::tokenText($SYMBOL);
       Debug("parser") << "symbol: " << id
-                      << " check? " << toString(check)
-                      << " type? " << toString(type) << std::endl;
+                      << " check? " << check
+                      << " type? " << type << std::endl;
       PARSER_STATE->checkDeclaration(id, check, type); }
   ;
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 03b901164..4bc90ec8f 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -2,10 +2,10 @@
 /*! \file smt2.cpp
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -24,8 +24,8 @@
 namespace CVC4 {
 namespace parser {
 
-Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode) :
-  Parser(exprManager,input,strictMode),
+Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
+  Parser(exprManager,input,strictMode,parseOnly),
   d_logicSet(false) {
   if( !strictModeEnabled() ) {
     addTheory(Smt2::THEORY_CORE);
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index ef5f5e729..e9363b970 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -2,10 +2,10 @@
 /*! \file smt2.h
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -48,7 +48,7 @@ private:
   Smt::Logic d_logic;
 
 protected:
-  Smt2(ExprManager* exprManager, Input* input, bool strictMode = false);
+  Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
 
 public:
   /**
diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index 836472107..04fe48fe1 100644
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -64,6 +64,11 @@ public:
   /** Destructor. Frees the lexer and the parser. */
   virtual ~Smt2Input();
 
+  /** Get the language that this Input is reading. */
+  InputLanguage getLanguage() const throw() {
+    return language::input::LANG_SMTLIB_V2;
+  }
+
 protected:
 
   /**