* (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!)

6 files changed, 181 insertions, 9 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 78f91edc5..02315143d 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -35,7 +35,8 @@ libutil_la_SOURCES = \
 	stats.h \
 	stats.cpp \
 	triple.h \
-	dynamic_array.h
+	dynamic_array.h \
+	language.h
 
 BUILT_SOURCES = \
 	rational.h \
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index c1b7acd71..403f6f84b 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -12,7 +12,7 @@
  ** information.\endverbatim
  **
  ** \brief Implementation of Configuration class, which provides compile-time
- ** configuration information about the CVC4 library.
+ ** configuration information about the CVC4 library
  **
  ** Implementation of Configuration class, which provides compile-time
  ** configuration information about the CVC4 library.
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index e59eacf4d..d04efe0aa 100644
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -85,7 +85,7 @@ namespace CVC4 {
 #endif /* TLS */
 
 #define CVC4_ABOUT_STRING string("\
-This is a pre-release of CVC4.\n\
+This is CVC4 version " CVC4_RELEASE_STRING "\n\n\
 Copyright (C) 2009, 2010\n\
   The ACSys Group\n\
   Courant Institute of Mathematical Sciences\n\
@@ -99,7 +99,8 @@ this CVC4 library cannot be used in proprietary applications.  Please\n\
 consult the CVC4 documentation for instructions about building a version\n\
 of CVC4 that links against GMP, and can be used in such applications.\n" : \
 "This CVC4 library uses GMP as its multi-precision arithmetic library.\n\n\
-CVC4 is open-source and is covered by the BSD license (modified).\n")
+CVC4 is open-source and is covered by the BSD license (modified).\n\n\
+THIS SOFTWARE PROVIDED AS-IS, WITHOUT ANY WARRANTIES. USE IT AT YOUR OWN RISK.\n")
 
 }/* CVC4 namespace */
 
diff --git a/src/util/language.h b/src/util/language.h
new file mode 100644
index 000000000..5446357c4
--- /dev/null
+++ b/src/util/language.h
@@ -0,0 +1,157 @@
+/*********************                                                        */
+/*! \file language.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** 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)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Definition of input and output languages
+ **
+ ** Definition of input and output languages.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__LANGUAGE_H
+#define __CVC4__LANGUAGE_H
+
+#include <sstream>
+#include <string>
+
+#include "util/exception.h"
+
+namespace CVC4 {
+namespace language {
+
+namespace input {
+
+enum Language {
+  // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
+
+  /** Auto-detect the language */
+  LANG_AUTO = -1,
+
+  // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,999]
+  // AND SHOULD CORRESPOND IN PLACEMENT WITH OUTPUTLANGUAGE
+  //
+  // EVEN IF A LANGUAGE ISN'T CURRENTLY SUPPORTED AS AN INPUT OR
+  // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE,
+  // INCLUDE IT HERE
+
+  /** The SMTLIB input language */
+  LANG_SMTLIB = 0,
+  /** The SMTLIB v2 input language */
+  LANG_SMTLIB_V2,
+  /** The CVC4 input language */
+  LANG_CVC4
+
+  // START INPUT-ONLY LANGUAGES AT ENUM VALUE 1000
+  // THESE ARE IN PRINCIPLE NOT POSSIBLE OUTPUT LANGUAGES
+
+};/* enum Language */
+
+inline std::ostream& operator<<(std::ostream& out, Language 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_input_language";
+  }
+  return out;
+}
+
+}/* CVC4::language::input namespace */
+
+namespace output {
+
+enum Language {
+  // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
+
+  // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,999]
+  // AND SHOULD CORRESPOND IN PLACEMENT WITH INPUTLANGUAGE
+  //
+  // EVEN IF A LANGUAGE ISN'T CURRENTLY SUPPORTED AS AN INPUT OR
+  // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE,
+  // INCLUDE IT HERE
+
+  /** The SMTLIB output language */
+  LANG_SMTLIB = input::LANG_SMTLIB,
+  /** The SMTLIB v2 output language */
+  LANG_SMTLIB_V2 = input::LANG_SMTLIB_V2,
+  /** The CVC4 output language */
+  LANG_CVC4 = input::LANG_CVC4,
+
+  // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 1000
+  // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES
+
+  /** The AST output language */
+  LANG_AST = 1000
+
+};/* enum Language */
+
+inline std::ostream& operator<<(std::ostream& out, Language 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_AST:
+    out << "LANG_AUTO";
+    break;
+  default:
+    out << "undefined_output_language";
+  }
+  return out;
+}
+
+}/* CVC4::language::output namespace */
+
+}/* CVC4::language namespace */
+
+typedef language::input::Language InputLanguage;
+typedef language::output::Language OutputLanguage;
+
+namespace language {
+
+inline OutputLanguage toOutputLanguage(InputLanguage language) {
+  switch(language) {
+  case input::LANG_SMTLIB:
+  case input::LANG_SMTLIB_V2:
+  case input::LANG_CVC4:
+    // these entries correspond
+    return OutputLanguage(int(language));
+
+  default: {
+    std::stringstream ss;
+    ss << "Cannot map input language `" << language
+       << "' to an output language.";
+    throw CVC4::Exception(ss.str());
+  }
+  }/* switch(language) */
+}/* toOutputLanguage() */
+
+}/* CVC4::language namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__LANGUAGE_H */
diff --git a/src/util/options.h b/src/util/options.h
index 08de590d8..af254dabf 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -21,10 +21,16 @@
 #ifndef __CVC4__OPTIONS_H
 #define __CVC4__OPTIONS_H
 
+#ifdef CVC4_DEBUG
+#  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
+#else /* CVC4_DEBUG */
+#  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false
+#endif /* CVC4_DEBUG */
+
 #include <iostream>
 #include <string>
 
-#include "parser/parser_options.h"
+#include "util/language.h"
 
 namespace CVC4 {
 
@@ -45,7 +51,7 @@ struct CVC4_PUBLIC Options {
   int verbosity;
 
   /** The input language */
-  parser::InputLanguage lang;
+  InputLanguage inputLanguage;
 
   /** Enumeration of UF implementation choices */
   typedef enum { TIM, MORGAN } UfImplementation;
@@ -83,13 +89,16 @@ struct CVC4_PUBLIC Options {
   /** Whether we support SmtEngine::getAssignment() for this run. */
   bool produceAssignments;
 
+  /** Whether we support SmtEngine::getAssignment() for this run. */
+  bool earlyTypeChecking;
+
   Options() :
     binary_name(),
     statistics(false),
     out(0),
     err(0),
     verbosity(0),
-    lang(parser::LANG_AUTO),
+    inputLanguage(language::input::LANG_AUTO),
     uf_implementation(MORGAN),
     parseOnly(false),
     semanticChecks(true),
@@ -99,7 +108,8 @@ struct CVC4_PUBLIC Options {
     interactive(false),
     interactiveSetByUser(false),
     produceModels(false),
-    produceAssignments(false) {
+    produceAssignments(false),
+    earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT) {
   }
 };/* struct Options */
 
@@ -121,4 +131,6 @@ inline std::ostream& operator<<(std::ostream& out,
 
 }/* CVC4 namespace */
 
+#undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
+
 #endif /* __CVC4__OPTIONS_H */
diff --git a/src/util/triple.h b/src/util/triple.h
index 50bf30c4a..3a6f841c4 100644
--- a/src/util/triple.h
+++ b/src/util/triple.h
@@ -13,7 +13,8 @@
  **
  ** \brief Similar to std::pair<>, for triples
  **
- ** Similar to std::pair<>, for triples.
+ ** Similar to std::pair<>, for triples.  Once we move to c++0x, this
+ ** can be removed in favor of (standard-provided) N-ary tuples.
  **/
 
 #include "cvc4_private.h"