Merge from my post-smtcomp branch. Includes:

Dumping infrastructure.  Can dump preprocessed queries and clauses.  Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc.  For a
full list of options see --dump=help.

CUDD building much cleaner.

Documentation and assertion fixes.

Printer improvements, printing of commands in language-defined way, etc.

Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.

CVC3 compatibility layer (builds as libcompat).

SWIG detection and language binding support (infrastructure).

Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).

Copyright and file headers regenerated.

6 files changed, 32 insertions, 22 deletions

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 707fc0ef3..8f1d54a3a 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -2,8 +2,8 @@
 /*! \file interactive_shell.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, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -237,11 +237,14 @@ Command* InteractiveShell::readCommand() {
         break;
       } else {
 #if HAVE_LIBREADLINE
-        DeclarationCommand* dcmd =
-          dynamic_cast<DeclarationCommand*>(cmd);
-        if(dcmd != NULL) {
-          const vector<string>& ids = dcmd->getDeclaredSymbols();
-          s_declarations.insert(ids.begin(), ids.end());
+        if(dynamic_cast<DeclareFunctionCommand*>(cmd) != NULL) {
+          s_declarations.insert(dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol());
+        } else if(dynamic_cast<DefineFunctionCommand*>(cmd) != NULL) {
+          s_declarations.insert(dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol());
+        } else if(dynamic_cast<DeclareTypeCommand*>(cmd) != NULL) {
+          s_declarations.insert(dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol());
+        } else if(dynamic_cast<DefineTypeCommand*>(cmd) != NULL) {
+          s_declarations.insert(dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol());
         }
 #endif /* HAVE_LIBREADLINE */
       }
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index 4fa2d6e96..f6852b95b 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -2,7 +2,7 @@
 /*! \file interactive_shell.h
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 1423befb6..ef19e1604 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -183,6 +183,7 @@ int runCvc4(int argc, char* argv[]) {
     Chat.setStream(CVC4::null_os);
     Message.setStream(CVC4::null_os);
     Warning.setStream(CVC4::null_os);
+    Dump.setStream(CVC4::null_os);
   } else {
     if(options.verbosity < 2) {
       Chat.setStream(CVC4::null_os);
@@ -228,7 +229,10 @@ int runCvc4(int argc, char* argv[]) {
     }
   }
 
-  OutputLanguage outLang = language::toOutputLanguage(options.inputLanguage);
+  if(options.outputLanguage == language::output::LANG_AUTO) {
+    options.outputLanguage = language::toOutputLanguage(options.inputLanguage);
+  }
+
   // Determine which messages to show based on smtcomp_mode and verbosity
   if(Configuration::isMuzzledBuild()) {
     Debug.setStream(CVC4::null_os);
@@ -237,6 +241,7 @@ int runCvc4(int argc, char* argv[]) {
     Chat.setStream(CVC4::null_os);
     Message.setStream(CVC4::null_os);
     Warning.setStream(CVC4::null_os);
+    Dump.setStream(CVC4::null_os);
   } else {
     if(options.verbosity < 2) {
       Chat.setStream(CVC4::null_os);
@@ -249,12 +254,15 @@ int runCvc4(int argc, char* argv[]) {
       Warning.setStream(CVC4::null_os);
     }
 
-    Debug.getStream() << Expr::setlanguage(outLang);
-    Trace.getStream() << Expr::setlanguage(outLang);
-    Notice.getStream() << Expr::setlanguage(outLang);
-    Chat.getStream() << Expr::setlanguage(outLang);
-    Message.getStream() << Expr::setlanguage(outLang);
-    Warning.getStream() << Expr::setlanguage(outLang);
+    Debug.getStream() << Expr::setlanguage(options.outputLanguage);
+    Trace.getStream() << Expr::setlanguage(options.outputLanguage);
+    Notice.getStream() << Expr::setlanguage(options.outputLanguage);
+    Chat.getStream() << Expr::setlanguage(options.outputLanguage);
+    Message.getStream() << Expr::setlanguage(options.outputLanguage);
+    Warning.getStream() << Expr::setlanguage(options.outputLanguage);
+    Dump.getStream() << Expr::setlanguage(options.outputLanguage)
+                     << Expr::setdepth(-1)
+                     << Expr::printtypes(false);
   }
 
   Parser* replayParser = NULL;
@@ -271,7 +279,7 @@ int runCvc4(int argc, char* argv[]) {
     options.replayStream = new Parser::ExprStream(replayParser);
   }
   if( options.replayLog != NULL ) {
-    *options.replayLog << Expr::setlanguage(outLang) << Expr::setdepth(-1);
+    *options.replayLog << Expr::setlanguage(options.outputLanguage) << Expr::setdepth(-1);
   }
 
   // Parse and execute commands until we are done
@@ -296,8 +304,7 @@ int runCvc4(int argc, char* argv[]) {
       delete cmd;
     }
   } else {
-    ParserBuilder parserBuilder =
-      ParserBuilder(&exprMgr, filename, options);
+    ParserBuilder parserBuilder(&exprMgr, filename, options);
 
     if( inputFromStdin ) {
       parserBuilder.withStreamInput(cin);
diff --git a/src/main/main.h b/src/main/main.h
index e472b43f1..1771198f4 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): dejan, barrett
+ ** Minor contributors (to current version): cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/main/usage.h b/src/main/usage.h
index 5ad96aea6..c11a2b73e 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): cconway
  ** 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
diff --git a/src/main/util.cpp b/src/main/util.cpp
index bf42025a0..255d84205 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): acsys
+ ** Minor contributors (to current version): acsys, cconway
  ** 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