* 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

7 files changed, 90 insertions, 52 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 27c64e9ef..1aa2e61fa 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -7,6 +7,7 @@ noinst_LTLIBRARIES = libexpr.la
 
 libexpr_la_SOURCES = \
 	node.h \
+	node.cpp \
 	node_builder.h \
 	expr.h \
 	type.h \
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 4bc569620..c56725f18 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -45,8 +45,8 @@ namespace attr {
  */
 struct AttrHashFcn {
   enum { LARGE_PRIME = 32452843ul };
-  std::size_t operator()(const std::pair<uint64_t, TNode>& p) const {
-    return p.first * LARGE_PRIME + p.second.hash();
+  std::size_t operator()(const std::pair<uint64_t, NodeValue*>& p) const {
+    return p.first * LARGE_PRIME + p.second->hash();
   }
 };
 
@@ -56,8 +56,8 @@ struct AttrHashFcn {
  * in [0..63] for each attribute
  */
 struct AttrHashBoolFcn {
-  std::size_t operator()(TNode n) const {
-    return n.hash();
+  std::size_t operator()(NodeValue* nv) const {
+    return nv->hash();
   }
 };
 
@@ -157,7 +157,7 @@ namespace attr {
  */
 template <class value_type>
 struct AttrHash :
-    public __gnu_cxx::hash_map<std::pair<uint64_t, TNode>,
+    public __gnu_cxx::hash_map<std::pair<uint64_t, NodeValue*>,
                                value_type,
                                AttrHashFcn> {
 };
@@ -168,12 +168,12 @@ struct AttrHash :
  */
 template <>
 class AttrHash<bool> :
-    protected __gnu_cxx::hash_map<TNode,
+    protected __gnu_cxx::hash_map<NodeValue*,
                                   uint64_t,
                                   AttrHashBoolFcn> {
 
   /** A "super" type, like in Java, for easy reference below. */
-  typedef __gnu_cxx::hash_map<TNode, uint64_t, AttrHashBoolFcn> super;
+  typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrHashBoolFcn> super;
 
   /**
    * BitAccessor allows us to return a bit "by reference."  Of course,
@@ -218,7 +218,7 @@ class AttrHash<bool> :
    */
   class BitIterator {
 
-    std::pair<const TNode, uint64_t>* d_entry;
+    std::pair<NodeValue* const, uint64_t>* d_entry;
 
     unsigned d_bit;
 
@@ -229,12 +229,12 @@ class AttrHash<bool> :
       d_bit(0) {
     }
 
-    BitIterator(std::pair<const TNode, uint64_t>& entry, unsigned bit) :
+    BitIterator(std::pair<NodeValue* const, uint64_t>& entry, unsigned bit) :
       d_entry(&entry),
       d_bit(bit) {
     }
 
-    std::pair<const TNode, BitAccessor> operator*() {
+    std::pair<NodeValue* const, BitAccessor> operator*() {
       return std::make_pair(d_entry->first, BitAccessor(d_entry->second, d_bit));
     }
 
@@ -251,7 +251,7 @@ class AttrHash<bool> :
    */
   class ConstBitIterator {
 
-    const std::pair<const TNode, uint64_t>* d_entry;
+    const std::pair<NodeValue* const, uint64_t>* d_entry;
 
     unsigned d_bit;
 
@@ -262,12 +262,12 @@ class AttrHash<bool> :
       d_bit(0) {
     }
 
-    ConstBitIterator(const std::pair<const TNode, uint64_t>& entry, unsigned bit) :
+    ConstBitIterator(const std::pair<NodeValue* const, uint64_t>& entry, unsigned bit) :
       d_entry(&entry),
       d_bit(bit) {
     }
 
-    std::pair<const TNode, bool> operator*() {
+    std::pair<NodeValue* const, bool> operator*() {
       return std::make_pair(d_entry->first, (d_entry->second & (1 << d_bit)) ? true : false);
     }
 
@@ -278,7 +278,7 @@ class AttrHash<bool> :
 
 public:
 
-  typedef std::pair<uint64_t, TNode> key_type;
+  typedef std::pair<uint64_t, NodeValue*> key_type;
   typedef bool data_type;
   typedef std::pair<const key_type, data_type> value_type;
 
@@ -291,7 +291,7 @@ public:
    * Find the boolean value in the hash table.  Returns something ==
    * end() if not found.
    */
-  BitIterator find(const std::pair<uint64_t, TNode>& k) {
+  BitIterator find(const std::pair<uint64_t, NodeValue*>& k) {
     super::iterator i = super::find(k.second);
     if(i == super::end()) {
       return BitIterator();
@@ -313,7 +313,7 @@ public:
    * Find the boolean value in the hash table.  Returns something ==
    * end() if not found.
    */
-  ConstBitIterator find(const std::pair<uint64_t, TNode>& k) const {
+  ConstBitIterator find(const std::pair<uint64_t, NodeValue*>& k) const {
     super::const_iterator i = super::find(k.second);
     if(i == super::end()) {
       return ConstBitIterator();
@@ -336,7 +336,7 @@ public:
    * the key into the table (associated to default value) if it's not
    * already there.
    */
-  BitAccessor operator[](const std::pair<uint64_t, TNode>& k) {
+  BitAccessor operator[](const std::pair<uint64_t, NodeValue*>& k) {
     uint64_t& word = super::operator[](k.second);
     return BitAccessor(word, k.first);
   }
@@ -708,7 +708,7 @@ typename AttrKind::value_type AttributeManager::getAttribute(TNode n,
   typedef typename getTable<value_type>::table_type table_type;
 
   const table_type& ah = getTable<value_type>::get(*this);
-  typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n));
+  typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n.d_nv));
 
   if(i == ah.end()) {
     return typename AttrKind::value_type();
@@ -731,7 +731,7 @@ template <class AttrKind>
 struct HasAttribute<true, AttrKind> {
   /** This implementation is simple; it's always true. */
   static inline bool hasAttribute(const AttributeManager* am,
-                                  TNode n) {
+                                  NodeValue* nv) {
     return true;
   }
 
@@ -740,14 +740,14 @@ struct HasAttribute<true, AttrKind> {
    * Node doesn't have the given attribute.
    */
   static inline bool hasAttribute(const AttributeManager* am,
-                                  TNode n,
+                                  NodeValue* nv,
                                   typename AttrKind::value_type& ret) {
     typedef typename AttrKind::value_type value_type;
     typedef KindValueToTableValueMapping<value_type> mapping;
     typedef typename getTable<value_type>::table_type table_type;
 
     const table_type& ah = getTable<value_type>::get(*am);
-    typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n));
+    typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv));
 
     if(i == ah.end()) {
       ret = AttrKind::default_value;
@@ -766,13 +766,13 @@ struct HasAttribute<true, AttrKind> {
 template <class AttrKind>
 struct HasAttribute<false, AttrKind> {
   static inline bool hasAttribute(const AttributeManager* am,
-                                  TNode n) {
+                                  NodeValue* nv) {
     typedef typename AttrKind::value_type value_type;
     typedef KindValueToTableValueMapping<value_type> mapping;
     typedef typename getTable<value_type>::table_type table_type;
 
     const table_type& ah = getTable<value_type>::get(*am);
-    typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n));
+    typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv));
 
     if(i == ah.end()) {
       return false;
@@ -782,14 +782,14 @@ struct HasAttribute<false, AttrKind> {
   }
 
   static inline bool hasAttribute(const AttributeManager* am,
-                                  TNode n,
+                                  NodeValue* nv,
                                   typename AttrKind::value_type& ret) {
     typedef typename AttrKind::value_type value_type;
     typedef KindValueToTableValueMapping<value_type> mapping;
     typedef typename getTable<value_type>::table_type table_type;
 
     const table_type& ah = getTable<value_type>::get(*am);
-    typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n));
+    typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv));
 
     if(i == ah.end()) {
       return false;
@@ -804,14 +804,14 @@ struct HasAttribute<false, AttrKind> {
 template <class AttrKind>
 bool AttributeManager::hasAttribute(TNode n,
                                     const AttrKind&) const {
-  return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, n);
+  return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, n.d_nv);
 }
 
 template <class AttrKind>
 bool AttributeManager::hasAttribute(TNode n,
                                     const AttrKind&,
                                     typename AttrKind::value_type& ret) const {
-  return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, n, ret);
+  return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, n.d_nv, ret);
 }
 
 template <class AttrKind>
@@ -824,7 +824,7 @@ inline void AttributeManager::setAttribute(TNode n,
   typedef typename getTable<value_type>::table_type table_type;
 
   table_type& ah = getTable<value_type>::get(*this);
-  ah[std::make_pair(AttrKind::getId(), n)] = mapping::convert(value);
+  ah[std::make_pair(AttrKind::getId(), n.d_nv)] = mapping::convert(value);
 }
 
 }/* CVC4::expr::attr namespace */
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 */
diff --git a/src/expr/node.h b/src/expr/node.h
index 19e50c5c2..474a175b1 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -36,7 +36,6 @@ class Type;
 class NodeManager;
 template<bool ref_count>
   class NodeTemplate;
-
 /**
  * The Node class encapsulates the NodeValue with reference counting.
  */
@@ -48,7 +47,11 @@ typedef NodeTemplate<true> Node;
 typedef NodeTemplate<false> TNode;
 
 namespace expr {
-class NodeValue;
+  class NodeValue;
+
+  namespace attr {
+    class AttributeManager;
+  }/* CVC4::expr::attr namespace */
 }/* CVC4::expr namespace */
 
 using CVC4::expr::NodeValue;
@@ -93,6 +96,7 @@ template<bool ref_count>
     friend class NodeManager;
     template<unsigned>
       friend class NodeBuilder;
+    friend class ::CVC4::expr::attr::AttributeManager;
 
     /**
      * Assigns the expression value and does reference counting. No assumptions
@@ -355,20 +359,9 @@ template<bool ref_count>
     NodeTemplate impNode(const NodeTemplate& right) const;
     NodeTemplate xorNode(const NodeTemplate& right) const;
 
-    NodeTemplate plusNode(const NodeTemplate& right) const;
-    NodeTemplate uMinusNode() const;
-    NodeTemplate multNode(const NodeTemplate& right) const;
-
   private:
 
     /**
-     * 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.
-     */
-    void debugPrint();
-
-    /**
      * Indents the given stream a given amount of spaces.
      * @param out the stream to indent
      * @param indent the numer of spaces
@@ -607,12 +600,6 @@ template<bool ref_count>
   }
 
 template<bool ref_count>
-  void NodeTemplate<ref_count>::debugPrint() {
-    printAst(Warning(), 0);
-    Warning().flush();
-  }
-
-template<bool ref_count>
   const Type* NodeTemplate<ref_count>::getType() const {
     Assert( NodeManager::currentNM() != NULL,
         "There is no current CVC4::NodeManager associated to this thread.\n"
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 0b89fcb5e..03936c89a 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -509,7 +509,7 @@ void NodeBuilder<nchild_thresh>::clear(Kind k) {
   d_used = false;
   d_nv = &d_inlineNv;
   d_inlineNv.d_kind = k;
-  d_inlineNv.d_nchildren = 0;
+  d_inlineNv.d_nchildren = 0;//FIXME leak
 }
 
 template <unsigned nchild_thresh>
@@ -551,6 +551,8 @@ void NodeBuilder<nchild_thresh>::realloc(size_t toSize, bool copy) {
       std::copy(d_inlineNv.d_children,
                 d_inlineNv.d_children + nchild_thresh,
                 d_nv->d_children);
+      // inhibit decr'ing refcounts of children in dtor
+      d_inlineNv.d_nchildren = 0;
     }
   }
 }
@@ -583,7 +585,7 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const
     Assert(d_nv->d_nchildren == 0);
     NodeValue *nv = (NodeValue*)
       std::malloc(sizeof(NodeValue) +
-                  ( sizeof(NodeValue*) * d_inlineNv.d_nchildren ));
+                  (sizeof(NodeValue*) * d_inlineNv.d_nchildren ));// FIXME :: WTF??
     nv->d_nchildren = 0;
     nv->d_kind = kind::VARIABLE;
     nv->d_id = NodeValue::next_id++;// FIXME multithreading
@@ -641,6 +643,7 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const
             ev->d_children);
   d_used = true;
   d_nv = NULL;
+  d_inlineNv.d_nchildren = 0;// inhibit decr'ing refcounts of children in dtor
 
   // Make the new expression
   d_nm->poolInsert(ev);
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index bcb5f6d47..a200a6d77 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -160,7 +160,7 @@ inline void NodeManager::setAttribute(TNode n,
 }
 
 inline const Type* NodeManager::getType(TNode n) {
-  return getAttribute(n,CVC4::expr::TypeAttr());
+  return getAttribute(n, CVC4::expr::TypeAttr());
 }
 
 inline void NodeManager::poolInsert(NodeValue* nv) {
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index ad558e115..efd2911ef 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -58,8 +58,9 @@ public:
    * Indicate a theory conflict has arisen.
    *
    * @param n - a conflict at the current decision level.  This should
-   * be an OR-kinded node of literals that are false in the current
-   * assignment.
+   * be an AND-kinded node of literals that are TRUE in the current
+   * assignment and are in conflict (i.e., at least one must be
+   * assigned false).
    *
    * @param safe - whether it is safe to be interrupted
    */