diff options
Diffstat (limited to 'src/expr/node_value.cpp')
-rw-r--r-- | src/expr/node_value.cpp | 37 |
1 files changed, 29 insertions, 8 deletions
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 840f41143..0138aa2a5 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -19,6 +19,8 @@ #include "expr/node_value.h" #include "expr/node.h" +#include "expr/kind.h" +#include "expr/metakind.h" #include <sstream> using namespace std; @@ -36,9 +38,19 @@ string NodeValue::toString() const { return ss.str(); } -void NodeValue::toStream(std::ostream& out) const { - if(d_kind == kind::VARIABLE) { +void NodeValue::toStream(std::ostream& out, int toDepth) const { + using namespace CVC4::kind; + using namespace CVC4; + + if(getKind() == kind::NULL_EXPR) { + out << "null"; + } else if(getMetaKind() == kind::metakind::VARIABLE) { + if(getKind() != kind::VARIABLE) { + out << getKind() << ':'; + } + string s; + // conceptually "this" is const, and hasAttribute() doesn't change // its argument, but it requires a non-const key arg (for now) if(NodeManager::currentNM()->getAttribute(const_cast<NodeValue*>(this), @@ -48,14 +60,23 @@ void NodeValue::toStream(std::ostream& out) const { out << "var_" << d_id; } } else { - out << "(" << Kind(d_kind); - for(const_nv_iterator i = nv_begin(); i != nv_end(); ++i) { - if(i != nv_end()) { - 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); + } else { + out << "(...)"; + } } - (*i)->toStream(out); } - out << ")"; + out << ')'; } } |