diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-07-02 00:09:52 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-07-02 00:09:52 +0000 |
commit | 83a143b1dd78e5d7f07666fbec1362dd60348116 (patch) | |
tree | 08400222d94f4760c7155fea787ac7e78b7b0dfc /src/expr/node_value.cpp | |
parent | a8566c313e9b5eb8248eaeea642a9c72c803dcfa (diff) |
* Added white-box TheoryEngine test that tests the rewriter
* Added regression documentation to test/regress/README
* Added ability to print types of vars in expr printouts
with iomanipulator Node::printtypes(true)... for example,
Warning() << Node::printtypes(true) << n << std::endl;
* Types-printing can be specified on the command line with
--print-expr-types
* Improved type handling facilities and theoryOf().
For now, SORT_TYPE moved from builtin theory to UF theory
to match old behavior.
* Additional gdb debug functionality. Now we have:
debugPrintNode(Node) debugPrintRawNode(Node)
debugPrintTNode(TNode) debugPrintRawTNode(TNode)
debugPrintTypeNode(TypeNode) debugPrintRawTypeNode(TypeNode)
debugPrintNodeValue(NodeValue*) debugPrintRawNodeValue(NodeValue*)
they all print a {Node,TNode,NodeValue*} from the debugger.
The "Raw" versions print a very low-level AST-like form.
The regular versions do the same as operator<<, but force
full printing on (no depth-limiting).
* Other trivial fixes
Diffstat (limited to 'src/expr/node_value.cpp')
-rw-r--r-- | src/expr/node_value.cpp | 39 |
1 files changed, 34 insertions, 5 deletions
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index c64a608fb..8add462e0 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -41,27 +41,34 @@ string NodeValue::toString() const { return ss.str(); } -void NodeValue::toStream(std::ostream& out, int toDepth) const { +void NodeValue::toStream(std::ostream& out, int toDepth, bool types) 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) { + 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(NodeManager::currentNM()->getAttribute(const_cast<NodeValue*>(this), - VarNameAttr(), s)) { + 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) { @@ -73,7 +80,7 @@ void NodeValue::toStream(std::ostream& out, int toDepth) const { out << ' '; } if(toDepth != 0) { - (*i)->toStream(out, toDepth < 0 ? toDepth : toDepth - 1); + (*i)->toStream(out, toDepth < 0 ? toDepth : toDepth - 1, types); } else { out << "(...)"; } @@ -83,5 +90,27 @@ void NodeValue::toStream(std::ostream& out, int toDepth) const { } } +void NodeValue::printAst(std::ostream& out, int ind) const { + indent(out, ind); + out << '('; + out << getKind(); + if(getMetaKind() == kind::metakind::VARIABLE) { + out << ' ' << getId(); + } else if(getMetaKind() == kind::metakind::CONSTANT) { + out << ' '; + kind::metakind::NodeValueConstPrinter::toStream(out, this); + } else { + if(nv_begin() != nv_end()) { + for(const_nv_iterator child = nv_begin(); child != nv_end(); ++child) { + out << std::endl; + (*child)->printAst(out, ind + 1); + } + out << std::endl; + indent(out, ind); + } + } + out << ')'; +} + }/* CVC4::expr namespace */ }/* CVC4 namespace */ |