* src/expr/node_builder.h: fixed some overly-aggressive refcount decrementing.

  There remain memory leaks (and some over-decrementing of refcounts) that
  I've identified; another commit forthcoming.

* src/expr/attribute.h: keys are now NodeValue* instead of TNode

* src/theory/output_channel.h: change OutputChannel::conflict() to the
  negation of what we had before: it now takes an AND of TRUE literals
  as a conflict clause rather than an OR of FALSE ones.

* src/expr/node.cpp: (non-template) CVC4::expr::debugPrint() routine
  for use inside gdb

* src/expr/node.h: remove Node::debugPrint() member (now a function
  instead of a member function, since Node is now a template it wasn't
  being properly instantiated(?) and couldn't be called from gdb)

* src/expr/Makefile.am: add node.cpp

* src/expr/node_manager.h: code formatting

1 files changed, 46 insertions, 0 deletions

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
new file mode 100644
index 000000000..213171124
--- /dev/null
+++ b/src/expr/node.cpp
@@ -0,0 +1,46 @@
+/*********************                                                        */
+/** node.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Reference-counted encapsulation of a pointer to node information.
+ **/
+
+#include "expr/node.h"
+#include "util/output.h"
+
+namespace CVC4 {
+namespace expr {
+
+#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.
+ *
+ * Note that this function cannot be a template, since the compiler
+ * won't instantiate it.  Even if we explicitly instantiate.  (Odd?)
+ * So we implement twice.
+ */
+void CVC4_PUBLIC debugPrint(const NodeTemplate<true>& n) {
+  n.printAst(Warning(), 0);
+  Warning().flush();
+}
+
+void CVC4_PUBLIC debugPrint(const NodeTemplate<false>& n) {
+  n.printAst(Warning(), 0);
+  Warning().flush();
+}
+
+#endif /* CVC4_DEBUG */
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */