diff options
Diffstat (limited to 'src/expr/node.h')
-rw-r--r-- | src/expr/node.h | 70 |
1 files changed, 29 insertions, 41 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index e3fb42ead..09a1ad8bc 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -455,12 +455,13 @@ public: * given stream * @param out the sream to serialise this node to */ - inline void toStream(std::ostream& out, int toDepth = -1) const { + inline void toStream(std::ostream& out, int toDepth = -1, + bool types = false) const { if(!ref_count) { Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" ); } - d_nv->toStream(out, toDepth); + d_nv->toStream(out, toDepth, types); } /** @@ -480,11 +481,22 @@ public: typedef expr::ExprSetDepth setdepth; /** + * IOStream manipulator to print type ascriptions or not. + * + * // let a, b, c, and d be variables of sort U + * Node n = nm->mkNode(OR, a, b, nm->mkNode(AND, c, nm->mkNode(NOT, d))) + * out << n; + * + * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but + */ + typedef expr::ExprPrintTypes printtypes; + + /** * Very basic pretty printer for Node. * @param o output stream to print to. * @param indent number of spaces to indent the formula by. */ - void printAst(std::ostream & o, int indent = 0) const; + inline void printAst(std::ostream& out, int indent = 0) const; NodeTemplate<true> eqNode(const NodeTemplate& right) const; @@ -497,19 +509,6 @@ public: NodeTemplate<true> impNode(const NodeTemplate& right) const; NodeTemplate<true> xorNode(const NodeTemplate& right) const; -private: - - /** - * Indents the given stream a given amount of spaces. - * @param out the stream to indent - * @param indent the numer of spaces - */ - static void indent(std::ostream& out, int indent) { - for(int i = 0; i < indent; i++) { - out << ' '; - } - } - };/* class NodeTemplate<ref_count> */ /** @@ -519,7 +518,9 @@ private: * @return the changed stream. */ inline std::ostream& operator<<(std::ostream& out, TNode n) { - n.toStream(out, Node::setdepth::getDepth(out)); + n.toStream(out, + Node::setdepth::getDepth(out), + Node::printtypes::getPrintTypes(out)); return out; } @@ -805,30 +806,9 @@ NodeTemplate<ref_count>::xorNode(const NodeTemplate<ref_count>& right) const { } template <bool ref_count> -void NodeTemplate<ref_count>::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, d_nv); - } else { - if(hasOperator()) { - out << std::endl; - getOperator().printAst(out, ind + 1); - } - if(getNumChildren() >= 1) { - for(const_iterator child = begin(); child != end(); ++child) { - out << std::endl; - (*child).printAst(out, ind + 1); - } - out << std::endl; - indent(out, ind); - } - } - out << ')'; +inline void +NodeTemplate<ref_count>::printAst(std::ostream& out, int indent) const { + d_nv->printAst(out, indent); } /** @@ -910,11 +890,19 @@ TypeNode NodeTemplate<ref_count>::getType() const * to meet. A cleaner solution is welcomed. */ static void __attribute__((used)) debugPrintNode(const NodeTemplate<true>& n) { + Warning() << Node::setdepth(-1) << n << std::endl; + Warning().flush(); +} +static void __attribute__((used)) debugPrintRawNode(const NodeTemplate<true>& n) { n.printAst(Warning(), 0); Warning().flush(); } static void __attribute__((used)) debugPrintTNode(const NodeTemplate<false>& n) { + Warning() << Node::setdepth(-1) << n << std::endl; + Warning().flush(); +} +static void __attribute__((used)) debugPrintRawTNode(const NodeTemplate<false>& n) { n.printAst(Warning(), 0); Warning().flush(); } |