From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 8 Oct 2010 23:12:28 +0000 (+0000)
Subject: * (define-fun...) now has proper type checking in non-debug builds
X-Git-Tag: cvc5-1.0.0~8818
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e63abd23b45a078a42cafb277a4817abb4d044a1;p=cvc5.git

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

diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 98aea9707..f5ecf84c5 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -562,7 +562,8 @@ inline void AttributeManager::deleteFromTable(CDAttrHash<T>& table,
 }
 
 /**
- * Remove all attributes from the table calling the cleanup function if one is defined.
+ * Remove all attributes from the table calling the cleanup function
+ * if one is defined.
  */
 template <class T>
 inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
@@ -575,7 +576,7 @@ inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
     }
   }
 
-  if(anyRequireClearing){
+  if(anyRequireClearing) {
     typename hash_t::iterator it = table.begin();
     typename hash_t::iterator it_end = table.end();
 
diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp
index bd128267a..0c76ea845 100644
--- a/src/expr/declaration_scope.cpp
+++ b/src/expr/declaration_scope.cpp
@@ -136,7 +136,6 @@ Type DeclarationScope::lookupType(const std::string& name,
 
     return instantiation;
   } else {
-    Assert(p.second.isSort());
     if(Debug.isOn("sort")) {
       Debug("sort") << "instantiating using a sort substitution" << endl;
       Debug("sort") << "have formals [";
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 55b59d13c..5cf3373c2 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -34,9 +34,9 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 
-ExprManager::ExprManager() :
+ExprManager::ExprManager(bool earlyTypeChecking) :
   d_ctxt(new Context),
-  d_nodeManager(new NodeManager(d_ctxt)) {
+  d_nodeManager(new NodeManager(d_ctxt, earlyTypeChecking)) {
 }
 
 ExprManager::~ExprManager() {
@@ -75,7 +75,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
   try {
     return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode()));
   } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage());
+    throw TypeCheckingException(this, &e);
   }
 }
 
@@ -92,8 +92,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
                                                child1.getNode(),
                                                child2.getNode()));
   } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(Expr(this, new Node(e.getNode())),
-                                e.getMessage());
+    throw TypeCheckingException(this, &e);
   }
 }
 
@@ -112,8 +111,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                                                child2.getNode(),
                                                child3.getNode()));
   } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(Expr(this, new Node(e.getNode())),
-                                e.getMessage());
+    throw TypeCheckingException(this, &e);
   }
 }
 
@@ -133,8 +131,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                                                child3.getNode(),
                                                child4.getNode()));
   } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(Expr(this, new Node(e.getNode())),
-                                e.getMessage());
+    throw TypeCheckingException(this, &e);
   }
 }
 
@@ -156,8 +153,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                                                child4.getNode(),
                                                child5.getNode()));
   } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(Expr(this, new Node(e.getNode())),
-                                e.getMessage());
+    throw TypeCheckingException(this, &e);
   }
 }
 
@@ -181,8 +177,7 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
   try {
     return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
   } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(Expr(this, new Node(e.getNode())),
-                                e.getMessage());
+    throw TypeCheckingException(this, &e);
   }
 }
 
@@ -207,7 +202,7 @@ Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
   try {
     return Expr(this,d_nodeManager->mkNodePtr(opExpr.getNode(), nodes));
   } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage());
+    throw TypeCheckingException(this, &e);
   }
 }
 
@@ -309,16 +304,19 @@ Type ExprManager::getType(const Expr& e, bool check) throw (TypeCheckingExceptio
   NodeManagerScope nms(d_nodeManager);
   Type t;
   try {
-    t = Type(d_nodeManager, new TypeNode(d_nodeManager->getType(e.getNode(), check)));
+    t = Type(d_nodeManager,
+             new TypeNode(d_nodeManager->getType(e.getNode(), check)));
   } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage());
+    throw TypeCheckingException(this, &e);
   }
   return t;
 }
 
 Expr ExprManager::mkVar(const std::string& name, const Type& type) {
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, d_nodeManager->mkVarPtr(name, *type.d_typeNode));
+  Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode);
+  Debug("nm") << "set " << name << " on " << *n << std::endl;
+  return Expr(this, n);
 }
 
 Expr ExprManager::mkVar(const Type& type) {
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 92d039bd3..7946a734e 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -74,12 +74,18 @@ private:
   /** ExprManagerScope reaches in to get the NodeManager */
   friend class ExprManagerScope;
 
+  // undefined, private copy constructor (disallow copy)
+  ExprManager(const ExprManager&);
+
 public:
 
   /**
    * Creates an expression manager.
+   * @param earlyTypeChecking whether to do type checking early (at Expr
+   * creation time); only used in debug builds---for other builds, type
+   * checking is never done early.
    */
-  ExprManager();
+  explicit ExprManager(bool earlyTypeChecking = true);
 
   /**
    * Destroys the expression manager. No will be deallocated at this point, so
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 5fb931a65..eb618a8c9 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -39,6 +39,7 @@ namespace expr {
 
 const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc();
 const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc();
+const int ExprSetLanguage::s_iosIndex = std::ios_base::xalloc();
 
 }/* CVC4::expr namespace */
 
@@ -47,8 +48,8 @@ std::ostream& operator<<(std::ostream& out, const TypeCheckingException& e) {
 }
 
 std::ostream& operator<<(std::ostream& out, const Expr& e) {
-  e.toStream(out);
-  return out;
+  ExprManagerScope ems(*e.getExprManager());
+  return out << e.getNode();
 }
 
 TypeCheckingException::TypeCheckingException(const TypeCheckingException& t)
@@ -61,6 +62,12 @@ TypeCheckingException::TypeCheckingException(const Expr& expr, std::string messa
 {
 }
 
+TypeCheckingException::TypeCheckingException(ExprManager* em,
+                                             const TypeCheckingExceptionPrivate* exc)
+: Exception(exc->getMessage()), d_expr(new Expr(em, new Node(exc->getNode())))
+{
+}
+
 TypeCheckingException::~TypeCheckingException() throw () {
   delete d_expr;
 }
@@ -218,9 +225,10 @@ bool Expr::isConst() const {
   return d_node->isConst();
 }
 
-void Expr::toStream(std::ostream& out, int depth, bool types) const {
+void Expr::toStream(std::ostream& out, int depth, bool types,
+                    OutputLanguage language) const {
   ExprManagerScope ems(*this);
-  d_node->toStream(out, depth, types);
+  d_node->toStream(out, depth, types, language);
 }
 
 Node Expr::getNode() const throw() {
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 29164ffa5..2eac4ab62 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -26,6 +26,7 @@
 #include <stdint.h>
 
 #include "util/exception.h"
+#include "util/language.h"
 
 ${includes}
 
@@ -33,7 +34,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 37 "${template}"
+#line 38 "${template}"
 
 namespace CVC4 {
 
@@ -45,6 +46,8 @@ class Expr;
 class ExprManager;
 class SmtEngine;
 class Type;
+class TypeCheckingException;
+class TypeCheckingExceptionPrivate;
 
 namespace smt {
   class SmtEnginePrivate;
@@ -53,6 +56,7 @@ namespace smt {
 namespace expr {
   class CVC4_PUBLIC ExprSetDepth;
   class CVC4_PUBLIC ExprPrintTypes;
+  class CVC4_PUBLIC ExprSetLanguage;
 }/* CVC4::expr namespace */
 
 /**
@@ -61,6 +65,7 @@ namespace expr {
 class CVC4_PUBLIC TypeCheckingException : public Exception {
 
   friend class SmtEngine;
+  friend class smt::SmtEnginePrivate;
 
 private:
 
@@ -69,8 +74,10 @@ private:
 
 protected:
 
-  TypeCheckingException(): Exception() {}
+  TypeCheckingException() : Exception() {}
   TypeCheckingException(const Expr& expr, std::string message);
+  TypeCheckingException(ExprManager* em,
+                        const TypeCheckingExceptionPrivate* exc);
 
 public:
 
@@ -96,6 +103,14 @@ public:
 std::ostream& operator<<(std::ostream& out,
                          const TypeCheckingException& e) CVC4_PUBLIC;
 
+/**
+ * Output operator for expressions
+ * @param out the stream to output to
+ * @param e the expression to output
+ * @return the stream
+ */
+std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC;
+
 /**
  * Class encapsulating CVC4 expressions and methods for constructing new
  * expressions.
@@ -281,7 +296,7 @@ public:
    * type checking is not requested, getType() will do the minimum
    * amount of checking required to return a valid result.
    *
-   * @param check whether we should check the type as we compute it 
+   * @param check whether we should check the type as we compute it
    * (default: false)
    */
   Type getType(bool check = false) const throw (TypeCheckingException);
@@ -296,7 +311,8 @@ public:
    * Outputs the string representation of the expression to the stream.
    * @param out the output stream
    */
-  void toStream(std::ostream& out, int depth = -1, bool types = false) const;
+  void toStream(std::ostream& out, int depth = -1, bool types = false,
+                OutputLanguage lang = language::output::LANG_AST) const;
 
   /**
    * Check if this is a null expression.
@@ -366,6 +382,11 @@ public:
    */
   typedef expr::ExprPrintTypes printtypes;
 
+  /**
+   * IOStream manipulator to set the output language for Exprs.
+   */
+  typedef expr::ExprSetLanguage setlanguage;
+
   /**
    * Very basic pretty printer for Expr.
    * This is equivalent to calling e.getNode().printAst(...)
@@ -402,15 +423,10 @@ protected:
   friend class SmtEngine;
   friend class smt::SmtEnginePrivate;
   friend class ExprManager;
-};
+  friend class TypeCheckingException;
+  friend std::ostream& operator<<(std::ostream& out, const Expr& e);
 
-/**
- * Output operator for expressions
- * @param out the stream to output to
- * @param e the expression to output
- * @return the stream
- */
-std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC;
+};/* class Expr */
 
 /**
  * Extending the expression with the capability to construct Boolean
@@ -551,7 +567,7 @@ public:
   static inline void setDepth(std::ostream& out, long depth) {
     out.iword(s_iosIndex) = depth;
   }
-};
+};/* class ExprSetDepth */
 
 /**
  * IOStream manipulator to print type ascriptions or not.
@@ -598,11 +614,50 @@ public:
   }
 };/* class ExprPrintTypes */
 
+/**
+ * IOStream manipulator to set the output language for Exprs.
+ */
+class CVC4_PUBLIC ExprSetLanguage {
+  /**
+   * The allocated index in ios_base for our depth setting.
+   */
+  static const int s_iosIndex;
+
+  /**
+   * The default language to use, for ostreams that haven't yet had a
+   * setlanguage() applied to them.
+   */
+  static const int s_defaultLanguage = language::output::LANG_AST;
+
+  /**
+   * When this manipulator is used, the setting is stored here.
+   */
+  OutputLanguage d_language;
+
+public:
+  /**
+   * Construct a ExprSetLanguage with the given setting.
+   */
+  ExprSetLanguage(OutputLanguage l) : d_language(l) {}
+
+  inline void applyLanguage(std::ostream& out) {
+    out.iword(s_iosIndex) = int(d_language);
+  }
+
+  static inline OutputLanguage getLanguage(std::ostream& out) {
+    return OutputLanguage(out.iword(s_iosIndex));
+  }
+
+  static inline void setLanguage(std::ostream& out, OutputLanguage l) {
+    out.iword(s_iosIndex) = int(l);
+  }
+};/* class ExprSetLanguage */
+
 }/* CVC4::expr namespace */
 
 ${getConst_instantiations}
 
-#line 566 "${template}"
+#line 659 "${template}"
 
 namespace expr {
 
@@ -634,6 +689,20 @@ inline std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) {
   return out;
 }
 
+/**
+ * Sets the output language when pretty-printing a Expr to an ostream.
+ * Use like this:
+ *
+ *   // let out be an ostream, e an Expr
+ *   out << Expr::setlanguage(LANG_SMTLIB_V2) << e << endl;
+ *
+ * The setting stays permanently (until set again) with the stream.
+ */
+inline std::ostream& operator<<(std::ostream& out, ExprSetLanguage l) {
+  l.applyLanguage(out);
+  return out;
+}
+
 }/* CVC4::expr namespace */
 
 // for hash_maps, hash_sets..
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index aaecff800..c4968af26 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -198,7 +198,7 @@ function registerOperatorToKind {
 	operatorKind=$1
 	applyKind=$2
 	metakind_operatorKinds="${metakind_operatorKinds}    case kind::$applyKind: return kind::$operatorKind;
-"; 
+";
 }
 
 function register_metakind {
diff --git a/src/expr/node.h b/src/expr/node.h
index 871f1e0d7..1427bb9c2 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -36,6 +36,8 @@
 #include "util/Assert.h"
 #include "util/configuration.h"
 #include "util/output.h"
+#include "util/exception.h"
+#include "util/language.h"
 
 namespace CVC4 {
 
@@ -58,7 +60,7 @@ private:
 
 protected:
 
-  TypeCheckingExceptionPrivate(): Exception() {}
+  TypeCheckingExceptionPrivate() : Exception() {}
 
 public:
 
@@ -656,12 +658,12 @@ public:
   /**
    * Converst this node into a string representation and sends it to the
    * given stream
-   * @param out the sream to serialise this node to
+   * @param out the stream to serialize this node to
    */
-  inline void toStream(std::ostream& out, int toDepth = -1,
-                       bool types = false) const {
+  inline void toStream(std::ostream& out, int toDepth = -1, bool types = false,
+                       OutputLanguage language = language::output::LANG_AST) const {
     assertTNodeNotExpired();
-    d_nv->toStream(out, toDepth, types);
+    d_nv->toStream(out, toDepth, types, language);
   }
 
   /**
@@ -691,6 +693,11 @@ public:
    */
   typedef expr::ExprPrintTypes printtypes;
 
+  /**
+   * IOStream manipulator to set the output language for Exprs.
+   */
+  typedef expr::ExprSetLanguage setlanguage;
+
   /**
    * Very basic pretty printer for Node.
    * @param o output stream to print to.
@@ -720,7 +727,8 @@ public:
 inline std::ostream& operator<<(std::ostream& out, TNode n) {
   n.toStream(out,
              Node::setdepth::getDepth(out),
-             Node::printtypes::getPrintTypes(out));
+             Node::printtypes::getPrintTypes(out),
+             Node::setlanguage::getLanguage(out));
   return out;
 }
 
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 2f10668c7..4c8bc578a 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -664,11 +664,11 @@ private:
   inline void debugCheckType(const TNode n) const {
     // force an immediate type check, if we are in debug mode
     // and the current node isn't a variable or constant
-    if( IS_DEBUG_BUILD ) {
+    if( IS_DEBUG_BUILD && d_nm->d_earlyTypeChecking ) {
       kind::MetaKind mk = n.getMetaKind();
       if( mk != kind::metakind::VARIABLE 
           && mk != kind::metakind::CONSTANT ) {
-        d_nm->getType(n,true);
+        d_nm->getType(n, true);
       }
     }
   }
@@ -692,11 +692,11 @@ public:
   operator Node();
   operator Node() const;
 
-  inline void toStream(std::ostream& out, int depth = -1,
-                       bool types = false) const {
+  inline void toStream(std::ostream& out, int depth = -1, bool types = false,
+                       OutputLanguage language = language::output::LANG_AST) const {
     Assert(!isUsed(), "NodeBuilder is one-shot only; "
            "attempt to access it after conversion");
-    d_nv->toStream(out, depth, types);
+    d_nv->toStream(out, depth, types, language);
   }
 
   NodeBuilder<nchild_thresh>& operator&=(TNode);
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 4653ee95f..5c24699b8 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -82,10 +82,11 @@ struct NVReclaim {
 };
 
 
-NodeManager::NodeManager(context::Context* ctxt) :
+NodeManager::NodeManager(context::Context* ctxt, bool earlyTypeChecking) :
   d_attrManager(ctxt),
   d_nodeUnderDeletion(NULL),
-  d_inReclaimZombies(false) {
+  d_inReclaimZombies(false),
+  d_earlyTypeChecking(earlyTypeChecking) {
   poolInsert( &expr::NodeValue::s_null );
 
   for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 0860365bc..6453a84d5 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -117,6 +117,12 @@ class NodeManager {
    */
   Node d_operators[kind::LAST_KIND];
 
+  /**
+   * Whether to do early type checking (only effective in debug
+   * builds; other builds never do early type checking.
+   */
+  const bool d_earlyTypeChecking;
+
   /**
    * Look up a NodeValue in the pool associated to this NodeManager.
    * The NodeValue argument need not be a "completely-constructed"
@@ -233,9 +239,12 @@ class NodeManager {
   // bool containsDecision(TNode); // is "atomic"
   // bool properlyContainsDecision(TNode); // all children are atomic
 
+  // undefined private copy constructor (disallow copy)
+  NodeManager(const NodeManager&);
+
 public:
 
-  NodeManager(context::Context* ctxt);
+  explicit NodeManager(context::Context* ctxt, bool earlyTypeChecking = true);
   ~NodeManager();
 
   /** The node manager in the current context. */
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index a10b43c48..004f0c9a9 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -24,6 +24,7 @@
 #include "expr/node.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
+#include "util/language.h"
 #include <sstream>
 
 using namespace std;
@@ -41,53 +42,67 @@ string NodeValue::toString() const {
   return ss.str();
 }
 
-void NodeValue::toStream(std::ostream& out, int toDepth, bool types) const {
-  using namespace CVC4::kind;
+void NodeValue::toStream(std::ostream& out, int toDepth, bool types,
+                         OutputLanguage language) const {
   using namespace CVC4;
+  using namespace CVC4::kind;
+  using namespace CVC4::language::output;
 
-  if(getKind() == kind::NULL_EXPR) {
-    out << "null";
-  } else if(getMetaKind() == kind::metakind::VARIABLE) {
-    if(getKind() != kind::VARIABLE &&
-       getKind() != kind::SORT_TYPE) {
-      out << getKind() << ':';
-    }
+  switch(language) {
+  case LANG_SMTLIB:
+    // FIXME support smt-lib output language
+  case LANG_SMTLIB_V2:
+    // FIXME support smt-lib v2 output language
+  case LANG_AST:
+    if(getKind() == kind::NULL_EXPR) {
+      out << "null";
+    } else if(getMetaKind() == kind::metakind::VARIABLE) {
+      if(getKind() != kind::VARIABLE &&
+         getKind() != kind::SORT_TYPE) {
+        out << getKind() << ':';
+      }
 
-    string s;
-    NodeManager* nm = NodeManager::currentNM();
+      string s;
+      NodeManager* nm = NodeManager::currentNM();
 
-    // conceptually "this" is const, and hasAttribute() doesn't change
-    // its argument, but it requires a non-const key arg (for now)
-    if(nm->getAttribute(const_cast<NodeValue*>(this),
-                        VarNameAttr(), s)) {
-      out << s;
-    } else {
-      out << "var_" << d_id;
-    }
-    if(types) {
-      // print the whole type, but not *its* type
-      out << ":";
-      nm->getType(TNode(this)).toStream(out, -1, false);
-    }
-  } else {
-    out << '(' << Kind(d_kind);
-    if(getMetaKind() == kind::metakind::CONSTANT) {
-      out << ' ';
-      kind::metakind::NodeValueConstPrinter::toStream(out, this);
+      // conceptually "this" is const, and hasAttribute() doesn't change
+      // its argument, but it requires a non-const key arg (for now)
+      if(nm->getAttribute(const_cast<NodeValue*>(this),
+                          VarNameAttr(), s)) {
+        out << s;
+      } else {
+        out << "var_" << d_id << "[" << this << "]";
+      }
+      if(types) {
+        // print the whole type, but not *its* type
+        out << ":";
+        nm->getType(TNode(this)).toStream(out, -1, false, language);
+      }
     } else {
-      for(const_nv_iterator i = nv_begin(); i != nv_end(); ++i) {
-        if(i != nv_end()) {
-          out << ' ';
-        }
-        if(toDepth != 0) {
-          (*i)->toStream(out, toDepth < 0 ? toDepth : toDepth - 1, types);
-        } else {
-          out << "(...)";
+      out << '(' << Kind(d_kind);
+      if(getMetaKind() == kind::metakind::CONSTANT) {
+        out << ' ';
+        kind::metakind::NodeValueConstPrinter::toStream(out, this);
+      } else {
+        for(const_nv_iterator i = nv_begin(); i != nv_end(); ++i) {
+          if(i != nv_end()) {
+            out << ' ';
+          }
+          if(toDepth != 0) {
+            (*i)->toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
+                           types, language);
+          } else {
+            out << "(...)";
+          }
         }
       }
+      out << ')';
     }
-    out << ')';
-  }
+    break;
+
+  default:
+    out << "[output language " << language << " unsupported]";
+  }// end switch(language)
 }
 
 void NodeValue::printAst(std::ostream& out, int ind) const {
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index b91196559..bc592b4e5 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -29,6 +29,7 @@
 #define __CVC4__EXPR__NODE_VALUE_H
 
 #include "expr/kind.h"
+#include "util/language.h"
 
 #include <stdint.h>
 #include <string>
@@ -260,7 +261,8 @@ public:
   }
 
   std::string toString() const;
-  void toStream(std::ostream& out, int toDepth = -1, bool types = false) const;
+  void toStream(std::ostream& out, int toDepth = -1, bool types = false,
+                OutputLanguage = language::output::LANG_AST) const;
 
   static inline unsigned kindToDKind(Kind k) {
     return ((unsigned) k) & kindMask;
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 8cf555eb0..b8b2e4754 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -29,9 +29,9 @@ using namespace std;
 
 namespace CVC4 {
 
-ostream& operator<<(ostream& out, const Type& e) {
-  e.toStream(out);
-  return out;
+ostream& operator<<(ostream& out, const Type& t) {
+  NodeManagerScope nms(t.d_nodeManager);
+  return out << *Type::getTypeNode(t);
 }
 
 Type Type::makeType(const TypeNode& typeNode) const {
@@ -123,6 +123,13 @@ void Type::toStream(ostream& out) const {
   return;
 }
 
+string Type::toString() const {
+  NodeManagerScope nms(d_nodeManager);
+  stringstream ss;
+  ss << *d_typeNode;
+  return ss.str();
+}
+
 /** Is this the Boolean type? */
 bool Type::isBoolean() const {
   NodeManagerScope nms(d_nodeManager);
diff --git a/src/expr/type.h b/src/expr/type.h
index 19c3d27f3..435d640d0 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -55,6 +55,14 @@ struct CVC4_PUBLIC TypeHashStrategy {
   static size_t hash(const CVC4::Type& t);
 };/* struct TypeHashStrategy */
 
+/**
+ * Output operator for types
+ * @param out the stream to output to
+ * @param t the type to output
+ * @return the stream
+ */
+std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC;
+
 /**
  * Class encapsulating CVC4 expression types.
  */
@@ -65,6 +73,7 @@ class CVC4_PUBLIC Type {
   friend class ExprManager;
   friend class TypeNode;
   friend class TypeHashStrategy;
+  friend std::ostream& operator<<(std::ostream& out, const Type& t);
 
 protected:
 
@@ -283,7 +292,12 @@ public:
    * @param out the stream to output to
    */
   void toStream(std::ostream& out) const;
-};
+
+  /**
+   * Constructs a string representation of this type.
+   */
+  std::string toString() const;
+};/* class Type */
 
 /**
  * Singleton class encapsulating the Boolean type.
@@ -294,7 +308,7 @@ public:
 
   /** Construct from the base type */
   BooleanType(const Type& type) throw(AssertionException);
-};
+};/* class BooleanType */
 
 /**
  * Singleton class encapsulating the integer type.
@@ -305,7 +319,7 @@ public:
 
   /** Construct from the base type */
   IntegerType(const Type& type) throw(AssertionException);
-};
+};/* class IntegerType */
 
 /**
  * Singleton class encapsulating the real type.
@@ -316,8 +330,7 @@ public:
 
   /** Construct from the base type */
   RealType(const Type& type) throw(AssertionException);
-};
-
+};/* class RealType */
 
 /**
  * Class encapsulating a function type.
@@ -334,7 +347,7 @@ public:
 
   /** Get the range type (i.e., the type of the result). */
   Type getRangeType() const;
-};
+};/* class FunctionType */
 
 /**
  * Class encapsulating a tuple type.
@@ -348,7 +361,7 @@ public:
 
   /** Get the constituent types */
   std::vector<Type> getTypes() const;
-};
+};/* class TupleType */
 
 /**
  * Class encapsulating an array type.
@@ -365,7 +378,7 @@ public:
 
   /** Get the constituent type */
   Type getConstituentType() const;
-};
+};/* class ArrayType */
 
 /**
  * Class encapsulating a user-defined sort.
@@ -379,7 +392,7 @@ public:
 
   /** Get the name of the sort */
   std::string getName() const;
-};
+};/* class SortType */
 
 /**
  * Class encapsulating a user-defined sort constructor.
@@ -399,7 +412,7 @@ public:
 
   /** Instantiate a sort using this sort constructor */
   SortType instantiate(const std::vector<Type>& params) const;
-};
+};/* class SortConstructorType */
 
 /**
  * Class encapsulating the kind type (the type of types).
@@ -410,8 +423,7 @@ public:
 
   /** Construct from the base type */
   KindType(const Type& type) throw(AssertionException);
-};
-
+};/* class KindType */
 
 /**
  * Class encapsulating the bit-vector type.
@@ -428,15 +440,7 @@ public:
    * @return the width of the bit-vector type (> 0)
    */
   unsigned getSize() const;
-};
-
-/**
- * Output operator for types
- * @param out the stream to output to
- * @param t the type to output
- * @return the stream
- */
-std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC;
+};/* class BitVectorType */
 
 }/* CVC4 namespace */
 
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 0e763128f..cc368e8c0 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -310,14 +310,14 @@ public:
   }
 
   /**
-   * Converst this node into a string representation and sends it to the
+   * Converts this node into a string representation and sends it to the
    * given stream
    *
-   * @param out the sream to serialise this node to
+   * @param out the stream to serialize this node to
    */
-  inline void toStream(std::ostream& out, int toDepth = -1,
-                       bool types = false) const {
-    d_nv->toStream(out, toDepth, types);
+  inline void toStream(std::ostream& out, int toDepth = -1, bool types = false,
+                       OutputLanguage language = language::output::LANG_AST) const {
+    d_nv->toStream(out, toDepth, types, language);
   }
 
   /**
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 113b8a5f7..8faaefac4 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -30,7 +30,7 @@
 #include "util/configuration.h"
 #include "util/output.h"
 #include "util/options.h"
-#include "parser/parser_options.h"
+#include "util/language.h"
 #include "expr/expr.h"
 
 #include "cvc4autoconfig.h"
@@ -75,7 +75,8 @@ enum OptionValue {
   INTERACTIVE,
   NO_INTERACTIVE,
   PRODUCE_MODELS,
-  PRODUCE_ASSIGNMENTS
+  PRODUCE_ASSIGNMENTS,
+  NO_EARLY_TYPE_CHECKING
 };/* enum OptionValue */
 
 /**
@@ -127,6 +128,7 @@ static struct option cmdlineOptions[] = {
   { "no-interactive", no_argument   , NULL, NO_INTERACTIVE },
   { "produce-models", no_argument   , NULL, PRODUCE_MODELS},
   { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS},
+  { "no-early-type-checking", no_argument, NULL, NO_EARLY_TYPE_CHECKING},
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
@@ -183,16 +185,16 @@ throw(OptionException) {
 
     case 'L':
       if(!strcmp(optarg, "cvc4") || !strcmp(optarg, "pl")) {
-        opts->lang = parser::LANG_CVC4;
+        opts->inputLanguage = language::input::LANG_CVC4;
         break;
       } else if(!strcmp(optarg, "smtlib") || !strcmp(optarg, "smt")) {
-        opts->lang = parser::LANG_SMTLIB;
+        opts->inputLanguage = language::input::LANG_SMTLIB;
         break;
       } else if(!strcmp(optarg, "smtlib2") || !strcmp(optarg, "smt2")) {
-        opts->lang = parser::LANG_SMTLIB_V2;
+        opts->inputLanguage = language::input::LANG_SMTLIB_V2;
         break;
       } else if(!strcmp(optarg, "auto")) {
-        opts->lang = parser::LANG_AUTO;
+        opts->inputLanguage = language::input::LANG_AUTO;
         break;
       }
 
@@ -300,12 +302,16 @@ throw(OptionException) {
       opts->produceAssignments = true;
       break;
 
+    case NO_EARLY_TYPE_CHECKING:
+      opts->earlyTypeChecking = false;
+      break;
+
     case SHOW_CONFIG:
       fputs(Configuration::about().c_str(), stdout);
       printf("\n");
-      printf("version   : %s\n", Configuration::getVersionString().c_str());
+      printf("version    : %s\n", Configuration::getVersionString().c_str());
       printf("\n");
-      printf("library   : %u.%u.%u\n",
+      printf("library    : %u.%u.%u\n",
              Configuration::getVersionMajor(),
              Configuration::getVersionMinor(),
              Configuration::getVersionRelease());
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 4f261378d..7fd866112 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -120,7 +120,7 @@ int runCvc4(int argc, char* argv[]) {
   }
 
   // Create the expression manager
-  ExprManager exprMgr;
+  ExprManager exprMgr(options.earlyTypeChecking);
 
   // Create the SmtEngine
   SmtEngine smt(&exprMgr, &options);
@@ -131,19 +131,19 @@ int runCvc4(int argc, char* argv[]) {
   ReferenceStat< const char* > s_statFilename("filename", filename);
   StatisticsRegistry::registerStat(&s_statFilename);
 
-  if(options.lang == parser::LANG_AUTO) {
+  if(options.inputLanguage == language::input::LANG_AUTO) {
     if( inputFromStdin ) {
       // We can't do any fancy detection on stdin
-      options.lang = parser::LANG_CVC4;
+      options.inputLanguage = language::input::LANG_CVC4;
     } else {
       unsigned len = strlen(filename);
       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
-        options.lang = parser::LANG_SMTLIB_V2;
+        options.inputLanguage = language::input::LANG_SMTLIB_V2;
       } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
-        options.lang = parser::LANG_SMTLIB;
+        options.inputLanguage = language::input::LANG_SMTLIB;
       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
-        options.lang = parser::LANG_CVC4;
+        options.inputLanguage = language::input::LANG_CVC4;
       }
     }
   }
@@ -167,11 +167,19 @@ int runCvc4(int argc, char* argv[]) {
       Message.setStream(CVC4::null_os);
       Warning.setStream(CVC4::null_os);
     }
+
+    OutputLanguage language = language::toOutputLanguage(options.inputLanguage);
+    Debug.getStream() << Expr::setlanguage(language);
+    Trace.getStream() << Expr::setlanguage(language);
+    Notice.getStream() << Expr::setlanguage(language);
+    Chat.getStream() << Expr::setlanguage(language);
+    Message.getStream() << Expr::setlanguage(language);
+    Warning.getStream() << Expr::setlanguage(language);
   }
 
   ParserBuilder parserBuilder =
       ParserBuilder(exprMgr, filename)
-        .withInputLanguage(options.lang)
+        .withInputLanguage(options.inputLanguage)
         .withMmap(options.memoryMap)
         .withChecks(options.semanticChecks &&
                     !Configuration::isMuzzledBuild() )
diff --git a/src/main/usage.h b/src/main/usage.h
index 15a30a426..ed35e76e8 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -51,7 +51,8 @@ CVC4 options:\n\
    --no-interactive       do not run interactively\n\
    --produce-models       support the get-value command\n\
    --produce-assignments  support the get-assignment command\n\
-   --lazy-definition-expansion expand define-fun lazily\n";
+   --lazy-definition-expansion expand define-fun lazily\n\
+   --no-early-type-checking don't typecheck at Expr creation [non-DEBUG builds never do]\n";
 
 }/* CVC4::main namespace */
 }/* CVC4 namespace */
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)); }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index fc2c8550e..de2fa4ebc 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -199,11 +199,12 @@ void SmtEngine::defineFunction(Expr func,
   Type formulaType = formula.getType(true);// type check body
   if(formulaType != FunctionType(func.getType()).getRangeType()) {
     stringstream ss;
-    ss << "Defined function's declared type does not match type of body\n"
-       << "The function: " << func << "\n"
-       << "Its type    : " << func.getType() << "\n"
-       << "The body    : " << formula << "\n"
-       << "Body type   : " << formulaType << "\n";
+    ss << "Defined function's declared type does not match that of body\n"
+       << "The function  : " << func << "\n"
+       << "Its range type: "
+       << FunctionType(func.getType()).getRangeType() << "\n"
+       << "The body      : " << formula << "\n"
+       << "Body type     : " << formulaType;
     throw TypeCheckingException(func, ss.str());
   }
   TNode funcNode = func.getTNode();
@@ -305,9 +306,22 @@ void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n)
   smt.d_propEngine->assertFormula(SmtEnginePrivate::preprocess(smt, n));
 }
 
+void SmtEngine::ensureBoolean(const BoolExpr& e) {
+  Type type = e.getType(true);
+  Type boolType = d_exprManager->booleanType();
+  if(type != boolType) {
+    stringstream ss;
+    ss << "Expected " << boolType << "\n"
+       << "The assertion : " << e << "\n"
+       << "Its type      : " << type;
+    throw TypeCheckingException(e, ss.str());
+  }
+}
+
 Result SmtEngine::checkSat(const BoolExpr& e) {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT checkSat(" << e << ")" << endl;
+  ensureBoolean(e);// ensure expr is type-checked at this point
   SmtEnginePrivate::addFormula(*this, e.getNode());
   Result r = check().asSatisfiabilityResult();
   Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << endl;
@@ -317,6 +331,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
 Result SmtEngine::query(const BoolExpr& e) {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT query(" << e << ")" << endl;
+  ensureBoolean(e);// ensure expr is type-checked at this point
   SmtEnginePrivate::addFormula(*this, e.getNode().notNode());
   Result r = check().asValidityResult();
   Debug("smt") << "SMT query(" << e << ") ==> " << r << endl;
@@ -326,12 +341,14 @@ Result SmtEngine::query(const BoolExpr& e) {
 Result SmtEngine::assertFormula(const BoolExpr& e) {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT assertFormula(" << e << ")" << endl;
+  ensureBoolean(e);// type check node
   SmtEnginePrivate::addFormula(*this, e.getNode());
   return quickCheck().asValidityResult();
 }
 
 Expr SmtEngine::simplify(const Expr& e) {
   NodeManagerScope nms(d_nodeManager);
+  e.getType(true);// ensure expr is type-checked at this point
   Debug("smt") << "SMT simplify(" << e << ")" << endl;
   Unimplemented();
 }
@@ -352,6 +369,8 @@ Expr SmtEngine::getValue(Expr term)
   // assertions
 
   NodeManagerScope nms(d_nodeManager);
+  Type type = term.getType(true);// ensure expr is type-checked at this point
+  SmtEnginePrivate::preprocess(*this, term.getNode());
 
   Unimplemented();
 }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index fd132a0c6..1fd68d2a5 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -132,6 +132,12 @@ class CVC4_PUBLIC SmtEngine {
    */
   Result quickCheck();
 
+  /**
+   * Fully type-check the argument, and also type-check that it's
+   * actually Boolean.
+   */
+  void ensureBoolean(const BoolExpr& e);
+
   friend class ::CVC4::smt::SmtEnginePrivate;
 
 public:
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"
diff --git a/test/regress/regress0/simple-rdl-definefun.smt2 b/test/regress/regress0/simple-rdl-definefun.smt2
index 08e99867a..6b38c6a70 100644
--- a/test/regress/regress0/simple-rdl-definefun.smt2
+++ b/test/regress/regress0/simple-rdl-definefun.smt2
@@ -1,14 +1,15 @@
 (set-logic QF_RDL)
 (set-info :status unsat)
+(set-info :notes | Simple test, based on simple-rdl.smt2, of define-sort and define-fun |)
 (declare-fun x () Real)
 (declare-fun y () Real)
 (declare-sort U 0)
-(declare-sort A 2)
-(define-sort F (x) (A Real Real))
+(define-sort A (x y) y)
+(define-sort F (x) (A x x))
 (declare-fun x2 () (F Real))
-(define-fun minus ((x Real) (z Real)) Real (- x z))
+(define-fun minus ((x Real) (z Real)) (A (A U Bool) (A (F U) Real)) (- x z))
 (define-fun less ((x Real) (z Real)) Bool (< x z))
-(define-fun foo ((x Real) (z Real)) Bool (less x z))
+(define-fun foo ((x (F Real)) (z (A U Real))) (F (F Bool)) (less x z))
 (assert (not (=> (foo (minus x y) 0) (less x y))))
 (check-sat)
 (exit)
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 88a6eaf57..4f55edad5 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -32,6 +32,7 @@
 
 using namespace CVC4;
 using namespace CVC4::parser;
+using namespace CVC4::language::input;
 using namespace std;
 
 class ParserBlack {
diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h
index b130501f5..c661f00d9 100644
--- a/test/unit/parser/parser_builder_black.h
+++ b/test/unit/parser/parser_builder_black.h
@@ -34,6 +34,7 @@ typedef __gnu_cxx::stdio_filebuf<char> filebuf_gnu;
 
 using namespace CVC4;
 using namespace CVC4::parser;
+using namespace CVC4::language::input;
 using namespace std;
 
 class ParserBuilderBlack : public CxxTest::TestSuite {