diff options
Diffstat (limited to 'src/expr/node_value.cpp')
-rw-r--r-- | src/expr/node_value.cpp | 63 |
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 { |