* (define-fun...) now has proper type checking in non-debug builds

  (resolves bug #212)

* also closed some other type checking loopholes in SmtEngine

* small fixes to define-sort (resolves bug #214)

* infrastructural support for printing expressions in languages
  other than the internal representation language using an IO
  manipulator, e.g.:

    cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << expr;

  main() sets the output language for all streams to correspond to
  the input language

* support delaying type checking in debug builds, so that one can debug
  the type checker itself (before it was difficult, because debug builds did
  all the type checking on Node creation!): new command-line flag
  --no-early-type-checking (only makes sense for debug builds)

* disallowed copy-construction of ExprManager and NodeManager, and made other
  constructors explicit; previously it was easy to unintentionally create
  duplicate managers, with really weird results (i.e., disappearing
  attributes!)

5 files changed, 10 insertions, 37 deletions

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index b919c3bd5..39c8e11b3 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -141,6 +141,8 @@ AntlrInputStream::newStringInputStream(const std::string& input,
 }
 
 AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStream) {
+  using namespace language::input;
+
   AntlrInput* input;
 
   switch(lang) {
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 139795494..f53d7cc9c 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -58,7 +58,7 @@ public:
 
 ParserBuilder::ParserBuilder(ExprManager& exprManager, const std::string& filename) :
     d_inputType(FILE_INPUT),
-    d_lang(LANG_AUTO),
+    d_lang(language::input::LANG_AUTO),
     d_filename(filename),
     d_streamInput(NULL),
     d_exprManager(exprManager),
@@ -85,9 +85,9 @@ Parser *ParserBuilder::build() throw (InputStreamException,AssertionException) {
     Unreachable();
   }
   switch(d_lang) {
-  case LANG_SMTLIB:
+  case language::input::LANG_SMTLIB:
     return new Smt(&d_exprManager, input, d_strictMode);
-  case LANG_SMTLIB_V2:
+  case language::input::LANG_SMTLIB_V2:
     return new Smt2(&d_exprManager, input, d_strictMode);
   default:
     return new Parser(&d_exprManager, input, d_strictMode);
diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h
index 2ae38622d..9a5b654a8 100644
--- a/src/parser/parser_exception.h
+++ b/src/parser/parser_exception.h
@@ -91,7 +91,7 @@ protected:
   std::string d_filename;
   unsigned long d_line;
   unsigned long d_column;
-}; // end of class ParserException
+};/* class ParserException */
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/parser_options.h b/src/parser/parser_options.h
index b3fd203e2..b6c61786b 100644
--- a/src/parser/parser_options.h
+++ b/src/parser/parser_options.h
@@ -23,41 +23,12 @@
 
 #include <iostream>
 
+#include "util/language.h"
+
 namespace CVC4 {
 namespace parser {
 
-/** The input language option */
-enum InputLanguage {
-  /** The SMTLIB input language */
-  LANG_SMTLIB,
-  /** The SMTLIB v2 input language */
-  LANG_SMTLIB_V2,
-  /** The CVC4 input language */
-  LANG_CVC4,
-  /** Auto-detect the language */
-  LANG_AUTO
-};/* enum InputLanguage */
-
-inline std::ostream& operator<<(std::ostream& out, InputLanguage lang) {
-  switch(lang) {
-  case LANG_SMTLIB:
-    out << "LANG_SMTLIB";
-    break;
-  case LANG_SMTLIB_V2:
-    out << "LANG_SMTLIB_V2";
-    break;
-  case LANG_CVC4:
-    out << "LANG_CVC4";
-    break;
-  case LANG_AUTO:
-    out << "LANG_AUTO";
-    break;
-  default:
-    out << "undefined_language";
-  }
-
-  return out;
-}
+// content moved to util/language.h
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index a2792eaac..2c460c831 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -250,7 +250,7 @@ command returns [CVC4::Command* cmd]
     }
   | /* assertion */
     ASSERT_TOK term[expr]
-    { cmd = new AssertCommand(expr);   }
+    { cmd = new AssertCommand(expr); }
   | /* checksat */
     CHECKSAT_TOK
     { cmd = new CheckSatCommand(MK_CONST(true)); }