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 {