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