* (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, 54 insertions, 39 deletions

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 {