Within node I added printAst(..) for general purpose debugging use throughout the code. I also added debugPrint() to Node for use within gdb.

2 files changed, 31 insertions, 0 deletions

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index b87acb1f2..0212b4fdd 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -116,4 +116,30 @@ Node Node::xorExpr(const Node& right) const {
   return NodeManager::currentNM()->mkNode(XOR, *this, right);
 }
 
+void indent(ostream & o, int indent){
+  for(int i=0; i < indent; i++)
+    o << ' ';
+}
+
+void Node::printAst(ostream & o, int ind) const{
+  indent(o, ind);
+  o << '(';
+  o << getKind();
+  if(getKind() == VARIABLE){
+    o << ' ' << getId();
+
+  }else if(getNumChildren() > 1){
+    for(Node::iterator child = begin(); child != end(); ++child){
+      (*child).printAst(o, ind+1);
+    }
+    indent(o, ind);
+  }
+  o << ')';
+}
+  
+void Node::debugPrint(){
+  printAst(Warning(), 0);
+  Warning().flush();
+}
+
 }/* CVC4 namespace */
diff --git a/src/expr/node.h b/src/expr/node.h
index 67af6aa18..ab5007a34 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -154,6 +154,11 @@ public:
 
   bool isNull() const;
 
+  void printAst(std::ostream & o, int indent = 0) const;
+  
+private:
+  void debugPrint();
+
 };/* class Node */
 
 }/* CVC4 namespace */