Pretty-printer infrastructure created (in src/printer) and SMT-LIBv2 printer

implemented.  This new infrastructure removes support for pretty-printing
(even in the AST language) an Expr with reference count 0.  Previously,
this was supported in a few places internally to the expr package, for
example in NodeBuilder.  (Now, a NodeBuilder cannot be prettyprinted, you
must extract the Node before printing it.)

1 files changed, 2 insertions, 61 deletions

diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index a5fff2095..666462875 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -25,6 +25,7 @@
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "util/language.h"
+#include "printer/printer.h"
 #include <sstream>
 
 using namespace std;
@@ -44,67 +45,7 @@ string NodeValue::toString() const {
 
 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;
-
-  switch(language) {
-  case LANG_CVC4:
-    // FIXME support cvc output 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();
-
-      // 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, language);
-      }
-    } else {
-      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 << ')';
-    }
-    break;
-
-  default:
-    out << "[output language " << language << " unsupported]";
-  }// end switch(language)
+  Printer::getPrinter(language)->toStream(out, TNode(this), toDepth, types);
 }
 
 void NodeValue::printAst(std::ostream& out, int ind) const {