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

1 files changed, 14 insertions, 6 deletions

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);
   }
 
   /**
@@ -692,6 +694,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.
    * @param indent number of spaces to indent the formula by.
@@ -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;
 }