Within node I added printAst(..) for general purpose debugging use throughout the...

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index b87acb1f2fea6c262f39127cdca2c76ad9bfe568..0212b4fdd98b58339c0df80e09daa176992b6bae 100644 (file)
--- 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 67af6aa18fa4c2b674673b6062b24775b7365248..ab5007a34e0cf53698cbbb071492a726c8aa404b 100644 (file)
--- 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 */