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.h | |
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.h')
-rw-r--r-- | src/expr/node_value.h | 40 |
1 files changed, 38 insertions, 2 deletions
diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 8b2056560..9f8a8f45b 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -213,7 +213,7 @@ public: } std::string toString() const; - void toStream(std::ostream& out, int toDepth = -1) const; + void toStream(std::ostream& out, int toDepth = -1, bool types = false) const; static inline unsigned kindToDKind(Kind k) { return ((unsigned) k) & kindMask; @@ -235,6 +235,21 @@ public: NodeValue* getChild(int i) const; + void printAst(std::ostream& out, int indent = 0) const; + +private: + + /** + * Indents the given stream a given amount of spaces. + * @param out the stream to indent + * @param indent the numer of spaces + */ + static inline void indent(std::ostream& out, int indent) { + for(int i = 0; i < indent; i++) { + out << ' '; + } + } + };/* class NodeValue */ /** @@ -264,6 +279,7 @@ inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv); }/* CVC4 namespace */ #include "expr/node_manager.h" +#include "expr/type_node.h" namespace CVC4 { namespace expr { @@ -363,11 +379,31 @@ inline T NodeValue::iterator<T>::operator*() { } inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) { - nv.toStream(out, Node::setdepth::getDepth(out)); + nv.toStream(out, + Node::setdepth::getDepth(out), + Node::printtypes::getPrintTypes(out)); return out; } }/* CVC4::expr namespace */ + +#ifdef CVC4_DEBUG +/** + * Pretty printer for use within gdb. This is not intended to be used + * outside of gdb. This writes to the Warning() stream and immediately + * flushes the stream. + */ +static void __attribute__((used)) debugPrintNodeValue(const expr::NodeValue* nv) { + Warning() << Node::setdepth(-1) << *nv << std::endl; + Warning().flush(); +} + +static void __attribute__((used)) debugPrintRawNodeValue(const expr::NodeValue* nv) { + nv->printAst(Warning(), 0); + Warning().flush(); +} +#endif /* CVC4_DEBUG */ + }/* CVC4 namespace */ #endif /* __CVC4__EXPR__NODE_VALUE_H */ |