From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 19 Feb 2010 20:29:58 +0000 (+0000)
Subject: * Attribute infrastructure -- static design.  Documentation is coming.
X-Git-Tag: cvc5-1.0.0~9242
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ce0e796ad92f040fb75435bd7880bc28a60b0374;p=cvc5.git

* Attribute infrastructure -- static design.  Documentation is coming.
  See test/unit/expr/node_white.h for use examples, including how to
  define new attribute kinds.

Also:

* fixes to test infrastructure
* minor changes to code formatting throughout
* attribute tests in test/unit/expr/node_white.h
* fixes to NodeManagerScope ordering
* use NodeValue::getKind() to properly deal with UNDEFINED_KIND
  (removing compiler warning)
* ExprManager: add proper NodeManagerScope to public-facing member
  functions
* store variable names and types in attributes
* SoftNode is a placeholder, not a real implementation
---

diff --git a/config/cvc4.m4 b/config/cvc4.m4
index 661631b4d..42dfaead5 100644
--- a/config/cvc4.m4
+++ b/config/cvc4.m4
@@ -2,6 +2,7 @@
 # ------------
 # Do early initialization/diversion of autoconf things for CVC4 build process.
 AC_DEFUN([CVC4_AC_INIT],
+dnl _AS_ME_PREPARE
 [CVC4_REWRITE_ARGS_FOR_BUILD_PROFILE
 ])# CVC4_AC_INIT
 
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index dd5b2a2f6..7393f27a5 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -6,8 +6,6 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden
 noinst_LTLIBRARIES = libexpr.la
 
 libexpr_la_SOURCES = \
-	attr_type.h \
-	attr_var_name.h \
 	node.h \
 	node_builder.h \
 	expr.h \
@@ -15,7 +13,8 @@ libexpr_la_SOURCES = \
 	node_value.h \
 	node_manager.h \
 	expr_manager.h \
-	node_attribute.h \
+	attribute.h \
+	attribute.cpp \
 	@srcdir@/kind.h \
 	node.cpp \
 	node_builder.cpp \
diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h
deleted file mode 100644
index f19491b70..000000000
--- a/src/expr/attr_type.h
+++ /dev/null
@@ -1,43 +0,0 @@
-/*********************                                                        */
-/** attr_type.h
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): dejan, taking
- ** 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.
- **
- ** Node attribute describing the type of a node.
- **/
-
-#ifndef __CVC4__EXPR__ATTR_TYPE_H
-#define __CVC4__EXPR__ATTR_TYPE_H
-
-#include "expr_attribute.h"
-
-namespace CVC4 {
-namespace expr {
-
-class Type;
-
-// an "attribute type" for types
-// this is essentially a traits structure
-class Type_attr {
-public:
-
-  // could use typeid but then different on different machines/compiles
-  enum { hash_value = 11 };
-
-  typedef Type value_type;//Node?
-  static const Type_attr marker;
-};
-
-extern AttrTable<Type_attr> type_table;
-
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__EXPR__ATTR_TYPE_H */
diff --git a/src/expr/attr_var_name.h b/src/expr/attr_var_name.h
deleted file mode 100644
index b3267c7dc..000000000
--- a/src/expr/attr_var_name.h
+++ /dev/null
@@ -1,40 +0,0 @@
-/*********************                                                        */
-/** attr_var_name.h
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): dejan
- ** 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.
- **
- ** The node attribute describing variable names.
- **/
-
-#ifndef __CVC4__EXPR__ATTR_VAR_NAME_H
-#define __CVC4__EXPR__ATTR_VAR_NAME_H
-
-#include "expr_attribute.h"
-
-namespace CVC4 {
-namespace expr {
-
-class VarName;
-
-// an "attribute type" for types
-// this is essentially a traits structure
-class VarName_attr {
-public:
-  enum { hash_value = 11 }; // could use typeid but then different on different machines/compiles
-  typedef Type value_type;//Node?
-  static const Type_attr marker;
-};
-
-extern AttrTable<Type_attr> type_table;
-
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__EXPR__ATTR_TYPE_H */
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
new file mode 100644
index 000000000..ea672b514
--- /dev/null
+++ b/src/expr/attribute.cpp
@@ -0,0 +1,30 @@
+/*********************                                           -*- C++ -*-  */
+/** attribute.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.
+ **
+ ** Node attributes.
+ **/
+
+#include "expr/attribute.h"
+
+#include <string>
+
+using std::string;
+
+namespace CVC4 {
+namespace expr {
+namespace attr {
+
+unsigned BitAssignment::s_bit = 0;
+
+}/* CVC4::expr::attr namespace */
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
new file mode 100644
index 000000000..b8cddacbf
--- /dev/null
+++ b/src/expr/attribute.h
@@ -0,0 +1,573 @@
+/*********************                                           -*- C++ -*-  */
+/** attribute.h
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** 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.
+ **
+ ** Node attributes.
+ **
+ ** Attribute structures:
+ **
+ ** An attribute structure looks like the following:
+ **
+ ** struct VarName_attr {
+ **
+ **   // the value type for this attribute
+ **   typedef std::string value_type;
+ **
+ **   // an extra hash value (to avoid same-value-type collisions)
+ **   enum { hash_value = 1 };
+ **
+ **   // whether inclusion in the table keeps the (key) Node live or not
+ **   static const bool hard_key = false;
+ **
+ **   // cleanup routine when the Node goes away
+ **   static inline void cleanup(const std::string&) {
+ **   }
+ ** }
+ **/
+
+/* There are strong constraints on ordering of declarations of
+ * attributes and nodes due to template use */
+#include "expr/node.h"
+
+#ifndef __CVC4__EXPR__ATTRIBUTE_H
+#define __CVC4__EXPR__ATTRIBUTE_H
+
+#include <stdint.h>
+
+#include <string>
+#include <ext/hash_map>
+
+#include "config.h"
+#include "context/context.h"
+#include "expr/soft_node.h"
+#include "expr/type.h"
+
+#include "util/output.h"
+
+namespace CVC4 {
+namespace expr {
+
+struct AttrHashFcn {
+  enum { LARGE_PRIME = 1 };
+  std::size_t operator()(const std::pair<unsigned, SoftNode>& p) const {
+    return p.first * LARGE_PRIME + p.second.hash();
+  }
+};
+
+struct AttrHashBoolFcn {
+  std::size_t operator()(const SoftNode& n) const {
+    return n.hash();
+  }
+};
+
+/*
+template <class T>
+class AttrTable;
+
+template <>
+class AttrTable<bool> {
+public:
+  class BitAccessor {
+
+    uint64_t& d_word;
+
+    unsigned d_bit;
+
+  public:
+
+    BitAccessor(uint64_t& word, unsigned bit) :
+      d_word(word),
+      d_bit(bit) {
+    }
+
+    BitAccessor& operator=(bool b) {
+      if(b) {
+        // set the bit
+        d_word |= (1 << d_bit);
+      } else {
+        // clear the bit
+        d_word &= ~(1 << d_bit);
+      }
+
+      return *this;
+    }
+  };
+
+  // bool specialization
+  //static AttrHash<uint64_t>* s_hash;
+
+  //typedef AttrHash<SoftNode, uint64_t>::iterator iterator;
+  //typedef AttrHash<SoftNode, uint64_t>::const_iterator const_iterator;
+
+  template <class Attr>
+  BitAccessor& find(Node e, const Attr&);
+
+  template <class Attr>
+  bool find(Node e, const Attr&) const;
+};
+
+template <>
+class AttrTable<uint64_t> {
+public:  
+  // int(egral) specialization
+  //static AttrHash<uint64_t>* s_hash;
+  typedef AttrHash<uint64_t>::iterator iterator;
+  typedef AttrHash<uint64_t>::const_iterator const_iterator;
+  uint64_t& find(TNode);
+};
+
+template <class T>
+class AttrTable<T*> {
+public:
+  // pointer specialization
+  //static AttrHash<void*>* s_hash;
+  typedef AttrHash<void*>::iterator iterator;
+  typedef AttrHash<void*>::const_iterator const_iterator;
+};
+
+template <>
+class AttrTable<Node> {
+public:
+  // Node specialization
+  //static AttrHash<SoftNode>* s_hash;
+  typedef AttrHash<SoftNode>::iterator iterator;
+  typedef AttrHash<SoftNode>::const_iterator const_iterator;
+  Node find(TNode);
+};
+
+template <>
+class AttrTable<std::string> {
+public:
+  // string specialization
+  //static AttrHash<std::string>* s_hash;
+  typedef AttrHash<std::string>::iterator iterator;
+  typedef AttrHash<std::string>::const_iterator const_iterator;
+  Node find(TNode);
+};
+
+*/
+
+/*
+template <class T>
+AttrHash<void*>*    AttrTable<T*>::s_hash       = &g_hash_ptr;
+*/
+
+template <class T>
+struct KindValueToTableValueMapping {
+  typedef T table_value_type;
+  inline static T convert(const T& t) { return t; }
+  inline static T convertBack(const T& t) { return t; }
+};
+
+template <>
+struct KindValueToTableValueMapping<bool> {
+  typedef uint64_t table_value_type;
+  inline static uint64_t convert(const bool& t) { return t; }
+  inline static bool convertBack(const uint64_t& t) { return t; }
+};
+
+template <class T>
+struct KindValueToTableValueMapping<T*> {
+  typedef void* table_value_type;
+  inline static void* convert(const T*& t) {
+    return reinterpret_cast<void*>(t);
+  }
+  inline static T* convertBack(void*& t) {
+    return reinterpret_cast<T*>(t);
+  }
+};
+
+template <class T>
+struct KindValueToTableValueMapping<const T*> {
+  typedef void* table_value_type;
+  inline static void* convert(const T* const& t) {
+    return reinterpret_cast<void*>(const_cast<T*>(t));
+  }
+  inline static const T* convertBack(const void*& t) {
+    return reinterpret_cast<const T*>(t);
+  }
+};
+
+template <class AttrKind, class T>
+struct OwnTable;
+
+template <class AttrKind, class T>
+struct KindValueToTableValueMapping<OwnTable<AttrKind, T> > {
+  typedef typename KindValueToTableValueMapping<T>::table_value_type table_value_type;
+};
+
+template <class AttrKind>
+struct KindTableMapping {
+  typedef typename AttrKind::value_type table_identifier;
+};
+
+// use a TAG to indicate which table it should be in
+template <class value_type>
+struct AttrHash : public __gnu_cxx::hash_map<std::pair<unsigned, SoftNode>, value_type, AttrHashFcn> {};
+
+/*
+template <>
+class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHashBoolFcn> {
+
+  typedef __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHashBoolFcn> super;
+
+  class BitAccessor {
+
+    uint64_t& d_word;
+
+    unsigned d_bit;
+
+  public:
+
+    BitAccessor(uint64_t& word, unsigned bit) :
+      d_word(word),
+      d_bit(bit) {
+    }
+
+    BitAccessor& operator=(bool b) {
+      if(b) {
+        // set the bit
+        d_word |= (1 << d_bit);
+      } else {
+        // clear the bit
+        d_word &= ~(1 << d_bit);
+      }
+
+      return *this;
+    }
+  };
+
+  class BitIterator {
+
+    std::pair<SoftNode, uint64_t>& d_word;
+
+    int d_bit;
+
+  public:
+
+    BitIterator() :
+      d_word((uint64_t&) d_bit),
+      d_bit(-1) {
+    }
+
+    BitIterator(std::pair<SoftNode, uint64_t>& entry, unsigned bit) :
+      d_entry(entry),
+      d_bit(bit) {
+    }
+
+    BitAccessor operator*() {
+      return BitAccessor(d_word, d_bit);
+    }
+  };
+
+  class ConstBitIterator {
+
+    uint64_t& d_word;
+
+    unsigned d_bit;
+
+  public:
+
+    ConstBitIterator(uint64_t& word, unsigned bit) :
+      d_word(word),
+      d_bit(bit) {
+    }
+
+    bool operator*() {
+      return (d_word & (1 << d_bit)) ? true : false;
+    }
+  };
+
+public:
+
+  typedef std::pair<unsigned, SoftNode> key_type;
+  typedef bool data_type;
+  typedef std::pair<const key_type, data_type> value_type;
+
+  typedef BitIterator iterator;
+  typedef ConstBitIterator const_iterator;
+
+  BitIterator find(const std::pair<unsigned, SoftNode>& k) {
+    super::iterator i = super::find(k.second);
+    if(i == super::end()) {
+      return BitIterator();
+    }
+    return BitIterator(*i, k.first);
+  }
+
+  ConstBitIterator find(const std::pair<unsigned, SoftNode>& k) const {
+    super::const_iterator i = super::find(k.second);
+    return ConstBitIterator(*i, k.first);
+  }
+
+  BitAccessor operator[](const std::pair<unsigned, SoftNode>& k) {
+    uint64_t& word = super::operator[](k.second);
+    return BitAccessor(word, k.first);
+  }
+};
+*/
+
+/**
+ * An "attribute type" structure.
+ */
+template <class T, class value_t>
+struct Attribute {
+
+  /** the value type for this attribute */
+  typedef value_t value_type;
+
+  /** cleanup routine when the Node goes away */
+  static inline void cleanup(const value_t&) {}
+
+  static inline unsigned getId() { return s_id; }
+  static inline unsigned getHashValue() { return s_hashValue; }
+
+private:
+
+  /** an id */
+  static unsigned s_id;
+
+  /** an extra hash value (to avoid same-value-type collisions) */
+  static unsigned s_hashValue;
+};
+
+/**
+ * An "attribute type" structure for boolean flags (special).
+ */
+template <class T>
+struct Attribute<T, bool> {
+
+  /** the value type for this attribute */
+  typedef bool value_type;
+
+  /** cleanup routine when the Node goes away */
+  static inline void cleanup(const bool&) {}
+
+  static inline unsigned getId() { return s_id; }
+  static inline unsigned getBit() { return s_bit; }
+  static inline unsigned getHashValue() { return s_hashValue; }
+
+private:
+
+  /** an id */
+  static unsigned s_id;
+
+  /** a bit assignment */
+  static unsigned s_bit;
+
+  /** an extra hash value (to avoid same-value-type collisions) */
+  static unsigned s_hashValue;
+};
+
+namespace attr {
+  struct VarName {};
+  struct Type {};
+
+  template <class T>
+  struct LastAttributeId {
+    static unsigned s_id;
+  };
+
+  template <class T>
+  unsigned LastAttributeId<T>::s_id = 0;
+
+  struct BitAssignment {
+    static unsigned s_bit;
+  };
+}/* CVC4::expr::attr namespace */
+
+typedef Attribute<attr::VarName, std::string> VarNameAttr;
+typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr;
+
+/*
+template <class Attr>
+class AttributeTable {
+  typedef typename Attr::value_type value_type;
+
+  AttrTable<value_type>& d_table;
+  
+};
+*/
+
+/*
+template <class T>
+struct AttrTables {
+  
+};
+*/
+
+template <class T, class value_t>
+unsigned Attribute<T, value_t>::s_id =
+  attr::LastAttributeId<typename KindValueToTableValueMapping<value_t>::table_value_type>::s_id++;
+template <class T, class value_t>
+unsigned Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id;
+
+template <class T>
+unsigned Attribute<T, bool>::s_id =
+  attr::LastAttributeId<bool>::s_id++;
+template <class T>
+unsigned Attribute<T, bool>::s_bit =
+  attr::BitAssignment::s_bit++;
+template <class T>
+unsigned Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id;
+
+class AttributeManager;
+
+template <class T>
+struct getTable {
+  //inline AttrHash<KindTableValueMapping<T> >& get(AttributeManager& am);
+};
+
+class AttributeManager {
+  NodeManager* d_nm;
+
+  AttrHash<uint64_t>    d_bools;
+  AttrHash<uint64_t>    d_ints;
+  AttrHash<SoftNode>    d_exprs;
+  AttrHash<std::string> d_strings;
+  AttrHash<void*>       d_ptrs;
+
+  template <class T>
+  friend struct getTable;
+
+public:
+  AttributeManager(NodeManager* nm) : d_nm(nm) {}
+
+  template <class AttrKind>
+  typename AttrKind::value_type getAttribute(const Node& n,
+                                             const AttrKind&);
+
+  template <class AttrKind>
+  bool hasAttribute(const Node& n,
+                    const AttrKind&,
+                    typename AttrKind::value_type* = NULL);
+
+  template <class AttrKind>
+  void setAttribute(const Node& n,
+                    const AttrKind&,
+                    const typename AttrKind::value_type& value);
+};
+
+template <>
+struct getTable<bool> {
+  typedef AttrHash<uint64_t> table_type;
+  static inline table_type& get(AttributeManager& am) {
+    return am.d_bools;
+  }
+};
+
+template <>
+struct getTable<uint64_t> {
+  typedef AttrHash<uint64_t> table_type;
+  static inline table_type& get(AttributeManager& am) {
+    return am.d_ints;
+  }
+};
+
+template <>
+struct getTable<Node> {
+  typedef AttrHash<SoftNode> table_type;
+  static inline table_type& get(AttributeManager& am) {
+    return am.d_exprs;
+  }
+};
+
+template <>
+struct getTable<std::string> {
+  typedef AttrHash<std::string> table_type;
+  static inline table_type& get(AttributeManager& am) {
+    return am.d_strings;
+  }
+};
+
+template <class T>
+struct getTable<T*> {
+  typedef AttrHash<void*> table_type;
+  static inline table_type& get(AttributeManager& am) {
+    return am.d_ptrs;
+  }
+};
+
+template <class AttrKind>
+typename AttrKind::value_type AttributeManager::getAttribute(const Node& n,
+                                                             const AttrKind& marker) {
+
+  typedef typename AttrKind::value_type value_type;
+  typedef KindValueToTableValueMapping<value_type> mapping;
+  typedef typename getTable<value_type>::table_type table_type;
+
+  table_type& ah = getTable<value_type>::get(*this);
+  typename table_type::iterator i = ah.find(std::make_pair(AttrKind::getId(), n));
+
+  if(i == ah.end()) {
+    return typename AttrKind::value_type();
+  }
+
+  return mapping::convertBack(i->second);
+}
+
+template <class AttrKind>
+bool AttributeManager::hasAttribute(const Node& n,
+                                    const AttrKind&,
+                                    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;
+
+  table_type& ah = getTable<value_type>::get(*this);
+  typename table_type::iterator i = ah.find(std::make_pair(AttrKind::getId(), n));
+
+  if(i == ah.end()) {
+    return false;
+  }
+
+  if(ret != NULL) {
+    *ret = mapping::convertBack(i->second);
+  }
+
+  return true;
+}
+
+template <class AttrKind>
+inline void AttributeManager::setAttribute(const Node& n,
+                                           const AttrKind&,
+                                           const typename AttrKind::value_type& value) {
+
+  typedef typename AttrKind::value_type value_type;
+  typedef KindValueToTableValueMapping<value_type> mapping;
+  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);
+}
+
+/*
+
+template <class attr>
+struct last_attribute_id {
+  static unsigned value;
+};
+
+template <class attr>
+unsigned last_attribute_id<attr>::value = 0;
+
+template <class attr>
+unsigned register_attribute_kind() {
+  return last_attribute_id<attr>::value++;
+}
+
+*/
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR__ATTRIBUTE_H */
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index 8bd9b21f6..506c118bc 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -30,8 +30,8 @@ using namespace std;
 
 namespace CVC4 {
 
-ExprManager::ExprManager()
-  : d_nm(new NodeManager()) {
+ExprManager::ExprManager() :
+  d_nm(new NodeManager()) {
 }
 
 ExprManager::~ExprManager() {
@@ -39,34 +39,41 @@ ExprManager::~ExprManager() {
 }
 
 const BooleanType* ExprManager::booleanType() {
+  NodeManagerScope nms(d_nm);
   return BooleanType::getInstance();
 }
 
 const KindType* ExprManager::kindType() {
+  NodeManagerScope nms(d_nm);
   return KindType::getInstance();
 }
 
 Expr ExprManager::mkExpr(Kind kind) {
+  NodeManagerScope nms(d_nm);
   return Expr(this, new Node(d_nm->mkNode(kind)));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
+  NodeManagerScope nms(d_nm);
   return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode())));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
+  NodeManagerScope nms(d_nm);
   return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
                                           child2.getNode())));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                          const Expr& child3) {
+  NodeManagerScope nms(d_nm);
   return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
                                           child2.getNode(), child3.getNode())));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                          const Expr& child3, const Expr& child4) {
+  NodeManagerScope nms(d_nm);
   return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
                                           child2.getNode(), child3.getNode(),
                                           child4.getNode())));
@@ -75,12 +82,15 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                          const Expr& child3, const Expr& child4,
                          const Expr& child5) {
+  NodeManagerScope nms(d_nm);
   return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
                                           child2.getNode(), child3.getNode(),
                                           child5.getNode())));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const vector<Expr>& children) {
+  NodeManagerScope nms(d_nm);
+
   vector<Node> nodes;
   vector<Expr>::const_iterator it = children.begin();
   vector<Expr>::const_iterator it_end = children.end();
@@ -95,24 +105,32 @@ Expr ExprManager::mkExpr(Kind kind, const vector<Expr>& children) {
 const FunctionType* 
 ExprManager::mkFunctionType(const Type* domain, 
                             const Type* range) {
-  return FunctionType::getInstance(this,domain,range);
+  NodeManagerScope nms(d_nm);
+  return FunctionType::getInstance(this, domain, range);
 }
 
 /** Make a function type with input types from argTypes. */
 const FunctionType* 
 ExprManager::mkFunctionType(const std::vector<const Type*>& argTypes, 
                             const Type* range) {
-  return FunctionType::getInstance(this,argTypes,range);
+  NodeManagerScope nms(d_nm);
+  return FunctionType::getInstance(this, argTypes, range);
 }
 
 const Type* ExprManager::mkSort(std::string name) {
   // FIXME: Sorts should be unique per-ExprManager
-  return new SortType(this,name);
+  NodeManagerScope nms(d_nm);
+  return new SortType(this, name);
+}
+
+Expr ExprManager::mkVar(const Type* type, string name) {
+  NodeManagerScope nms(d_nm);
+  return Expr(this, new Node(d_nm->mkVar(type, name)));
 }
 
 Expr ExprManager::mkVar(const Type* type) {
-  // FIXME: put the type into an attribute table
-  return Expr(this, new Node(d_nm->mkVar()));
+  NodeManagerScope nms(d_nm);
+  return Expr(this, new Node(d_nm->mkVar(type)));
 }
 
 NodeManager* ExprManager::getNodeManager() const {
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index 1ca707fae..5bfef2aa7 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -103,6 +103,7 @@ public:
   const Type* mkSort(std::string name);
 
   // variables are special, because duplicates are permitted
+  Expr mkVar(const Type* type, std::string name);
   Expr mkVar(const Type* type);
 
 private:
diff --git a/src/expr/node.h b/src/expr/node.h
index 39eb3bcd7..463ff8144 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -28,10 +28,8 @@
 #include "util/Assert.h"
 
 namespace CVC4 {
-  class Node;
-}/* CVC4 namespace */
 
-namespace CVC4 {
+class Node;
 
 inline std::ostream& operator<<(std::ostream&, const Node&);
 
@@ -50,6 +48,7 @@ using CVC4::expr::NodeValue;
 class Node {
 
   friend class NodeValue;
+  friend class SoftNode;
 
   /** A convenient null-valued encapsulated pointer */
   static Node s_null;
@@ -155,7 +154,18 @@ public:
   bool isNull() const;
   bool isAtomic() const;
 
-   /**
+  template <class AttrKind>
+  inline typename AttrKind::value_type getAttribute(const AttrKind&);
+
+  template <class AttrKind>
+  inline bool hasAttribute(const AttrKind&,
+                           typename AttrKind::value_type* = NULL);
+
+  template <class AttrKind>
+  inline void setAttribute(const AttrKind&,
+                           const typename AttrKind::value_type& value);
+
+  /**
    * Very basic pretty printer for Node.
    * @param o output stream to print to.
    * @param indent number of spaces to indent the formula by.
@@ -176,7 +186,20 @@ private:
 
 }/* CVC4 namespace */
 
-#include "expr/node_value.h"
+#include <ext/hash_map>
+
+// for hashtables
+namespace __gnu_cxx {
+  template <>
+  struct hash<CVC4::Node> {
+    size_t operator()(const CVC4::Node& node) const {
+      return (size_t)node.hash();
+    }
+  };
+}/* __gnu_cxx namespace */
+
+#include "expr/attribute.h"
+#include "expr/node_manager.h"
 
 namespace CVC4 {
 
@@ -237,6 +260,23 @@ inline size_t Node::getNumChildren() const {
   return d_ev->d_nchildren;
 }
 
+template <class AttrKind>
+inline typename AttrKind::value_type Node::getAttribute(const AttrKind&) {
+  return NodeManager::currentNM()->getAttribute(*this, AttrKind());
+}
+
+template <class AttrKind>
+inline bool Node::hasAttribute(const AttrKind&,
+                               typename AttrKind::value_type* ret) {
+  return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret);
+}
+
+template <class AttrKind>
+inline void Node::setAttribute(const AttrKind&,
+                               const typename AttrKind::value_type& value) {
+  NodeManager::currentNM()->setAttribute(*this, AttrKind(), value);
+}
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__NODE_H */
diff --git a/src/expr/node_attribute.h b/src/expr/node_attribute.h
deleted file mode 100644
index f43013a27..000000000
--- a/src/expr/node_attribute.h
+++ /dev/null
@@ -1,102 +0,0 @@
-/*********************                                                        */
-/** node_attribute.h
- ** Original author: mdeters
- ** Major contributors: dejan
- ** 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.
- **
- ** Node attributes.
- **/
-
-#ifndef __CVC4__EXPR__NODE_ATTRIBUTE_H
-#define __CVC4__EXPR__NODE_ATTRIBUTE_H
-
-#include <stdint.h>
-#include "config.h"
-#include "context/context.h"
-#include "expr/node.h"
-
-namespace CVC4 {
-namespace expr {
-
-template <class value_type>
-class AttrTables;
-
-// global (or TSS)
-extern CDMap<uint64_t> g_hash_bool;
-extern CDMap<uint64_t> g_hash_int;
-extern CDMap<Node>     g_hash_expr;
-extern CDMap<void*>    g_hash_ptr;
-
-template <class T>
-class AttrTable;
-
-template <>
-class AttrTable<bool> {
-public:
-  class BitAccessor {
-    uint64_t& d_word;
-    unsigned d_bit;
-  public:
-    BitAccessor& operator=(bool b);
-    // continue...
-  };
-
-  // bool specialization
-  static CDMap<uint64_t> *s_hash;
-
-  template <class Attr>
-  BitAccessor& find(Node e, const Attr&);
-
-  template <class Attr>
-  bool find(Node e, const Attr&) const;
-};
-
-template <>
-class AttrTable<uint64_t> {
-public:  
-  // int(egral) specialization
-  static CDMap<uint64_t> *s_hash;
-  uint64_t& find(Node);
-  uint64_t& find(Node) const;
-};
-
-template <class T>
-class AttrTable<T*> {
-  // pointer specialization
-  static CDMap<void*> *s_hash;
-public:
-};
-
-template <>
-class AttrTable<Node> {
-public:
-  // Node specialization
-  static CDMap<Node> *s_hash;
-  Node find(Node);
-};
-
-CDMap<uint64_t>* AttrTable<bool>::s_hash     = &g_hash_bool;
-CDMap<uint64_t>* AttrTable<uint64_t>::s_hash = &g_hash_int;
-CDMap<Node>*     AttrTable<Node>::s_hash     = &g_hash_expr;
-
-template <class T>
-CDMap<void*>*    AttrTable<T*>::s_hash       = &g_hash_ptr;
-
-template <class Attr>
-class AttributeTable {
-  typedef typename Attr::value_type value_type;
-
-  AttrTable<value_type>& d_table;
-  
-};
-
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__EXPR__EXPR_ATTRIBUTE_H */
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 08a879600..093f09a79 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -171,7 +171,7 @@ public:
 
   NodeBuilder& operator<<(const Kind& k) {
     Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
-    Assert(d_ev->d_kind == UNDEFINED_KIND);
+    Assert(d_ev->getKind() == UNDEFINED_KIND);
     d_ev->d_kind = k;
     return *this;
   }
@@ -563,7 +563,7 @@ inline void NodeBuilder<nchild_thresh>::dealloc() {
 template <unsigned nchild_thresh>
 NodeBuilder<nchild_thresh>::operator Node() {// not const
   Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
-  Assert(d_ev->d_kind != UNDEFINED_KIND,
+  Assert(d_ev->getKind() != UNDEFINED_KIND,
          "Can't make an expression of an undefined kind!");
 
   if(d_ev->d_kind == VARIABLE) {
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 3561f2119..12a6d1732 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -16,16 +16,16 @@
 #include "node_builder.h"
 #include "node_manager.h"
 #include "expr/node.h"
+#include "expr/attribute.h"
 #include "util/output.h"
 
+using namespace std;
+using namespace CVC4::expr;
+
 namespace CVC4 {
 
 __thread NodeManager* NodeManager::s_current = 0;
 
-NodeManager::NodeManager() {
-  poolInsert(&NodeValue::s_null);
-}
-
 NodeValue* NodeManager::poolLookup(NodeValue* nv) const {
   NodeValueSet::const_iterator find = d_nodeValueSet.find(nv);
   if (find == d_nodeValueSet.end()) {
@@ -68,10 +68,23 @@ Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, cons
 }
 
 // N-ary version
-Node NodeManager::mkNode(Kind kind, const std::vector<Node>& children) {
+Node NodeManager::mkNode(Kind kind, const vector<Node>& children) {
   return NodeBuilder<>(this, kind).append(children);
 }
 
+Node NodeManager::mkVar(const Type* type, string name) {
+  Node n = NodeBuilder<>(this, VARIABLE);
+  n.setAttribute(TypeAttr(), type);
+  n.setAttribute(VarNameAttr(), name);
+  return n;
+}
+
+Node NodeManager::mkVar(const Type* type) {
+  Node n = NodeBuilder<>(this, VARIABLE);
+  n.setAttribute(TypeAttr(), type);
+  return n;
+}
+
 Node NodeManager::mkVar() {
   return NodeBuilder<>(this, VARIABLE);
 }
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 0abd86130..2862203db 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -17,23 +17,26 @@
 #define __CVC4__NODE_MANAGER_H
 
 #include <vector>
+#include <string>
 #include <ext/hash_set>
 
-#include "node.h"
-#include "kind.h"
+#include "expr/node.h"
+#include "expr/kind.h"
 
 namespace __gnu_cxx {
-template<>
+  template<>
   struct hash<CVC4::NodeValue*> {
     size_t operator()(const CVC4::NodeValue* nv) const {
       return (size_t)nv->hash();
     }
   };
-} /* __gnu_cxx namespace */
+}/* __gnu_cxx namespace */
 
 
 namespace CVC4 {
 
+class Type;
+
 class NodeManager {
   static __thread NodeManager* s_current;
 
@@ -42,6 +45,8 @@ class NodeManager {
   typedef __gnu_cxx::hash_set<NodeValue*, __gnu_cxx::hash<NodeValue*>, NodeValue::NodeValueEq> NodeValueSet;
   NodeValueSet d_nodeValueSet;
 
+  expr::AttributeManager d_am;
+
   NodeValue* poolLookup(NodeValue* nv) const;
   void poolInsert(NodeValue* nv);
 
@@ -49,7 +54,9 @@ class NodeManager {
 
 public:
 
-  NodeManager();
+  NodeManager() : d_am(this) {
+    poolInsert( &NodeValue::s_null );
+  }
 
   static NodeManager* currentNM() { return s_current; }
 
@@ -64,22 +71,61 @@ public:
   Node mkNode(Kind kind, const std::vector<Node>& children);
 
   // variables are special, because duplicates are permitted
+  Node mkVar(const Type* type, std::string name);
+  Node mkVar(const Type* type);
   Node mkVar();
-};
 
+  template <class AttrKind>
+  inline typename AttrKind::value_type getAttribute(const Node& n,
+                                                    const AttrKind&);
+
+  template <class AttrKind>
+  inline bool hasAttribute(const Node& n,
+                           const AttrKind&,
+                           typename AttrKind::value_type* = NULL);
+
+  template <class AttrKind>
+  inline void setAttribute(const Node& n,
+                           const AttrKind&,
+                           const typename AttrKind::value_type& value);
+};
 
 class NodeManagerScope {
   NodeManager *d_oldNodeManager;
 
 public:
+
   NodeManagerScope(NodeManager* nm) : d_oldNodeManager(NodeManager::s_current) {
     NodeManager::s_current = nm;
+    Debug("current") << "node manager scope: " << NodeManager::s_current << "\n";
   }
+
   ~NodeManagerScope() {
     NodeManager::s_current = d_oldNodeManager;
+    Debug("current") << "node manager scope: returning to " << NodeManager::s_current << "\n";
   }
 };
 
+template <class AttrKind>
+inline typename AttrKind::value_type NodeManager::getAttribute(const Node& n,
+                                                               const AttrKind&) {
+  return d_am.getAttribute(n, AttrKind());
+}
+
+template <class AttrKind>
+inline bool NodeManager::hasAttribute(const Node& n,
+                                      const AttrKind&,
+                                      typename AttrKind::value_type* ret) {
+  return d_am.hasAttribute(n, AttrKind(), ret);
+}
+
+template <class AttrKind>
+inline void NodeManager::setAttribute(const Node& n,
+                                      const AttrKind&,
+                                      const typename AttrKind::value_type& value) {
+  d_am.setAttribute(n, AttrKind(), value);
+}
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__EXPR_MANAGER_H */
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index f8bf33b5c..36d634b8b 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -17,7 +17,8 @@
  ** reference count on NodeValue instances and
  **/
 
-#include "node_value.h"
+#include "expr/node_value.h"
+#include "expr/node.h"
 #include <sstream>
 
 using namespace std;
@@ -27,11 +28,17 @@ namespace CVC4 {
 size_t NodeValue::next_id = 1;
 
 NodeValue::NodeValue() :
-  d_id(0), d_rc(MAX_RC), d_kind(NULL_EXPR), d_nchildren(0) {
+  d_id(0),
+  d_rc(MAX_RC),
+  d_kind(NULL_EXPR),
+  d_nchildren(0) {
 }
 
 NodeValue::NodeValue(int) :
-  d_id(0), d_rc(0), d_kind(unsigned(UNDEFINED_KIND)), d_nchildren(0) {
+  d_id(0),
+  d_rc(0),
+  d_kind(kindToDKind(UNDEFINED_KIND)),
+  d_nchildren(0) {
 }
 
 NodeValue::~NodeValue() {
@@ -98,7 +105,13 @@ string NodeValue::toString() const {
 void NodeValue::toStream(std::ostream& out) const {
   out << "(" << Kind(d_kind);
   if(d_kind == VARIABLE) {
-    out << ":" << this;
+    Node n(this);
+    string s;
+    if(n.hasAttribute(VarNameAttr(), &s)) {
+      out << ":" << s;
+    } else {
+      out << ":" << this;
+    }
   } else {
     for(const_ev_iterator i = ev_begin(); i != ev_end(); ++i) {
       if(i != ev_end()) {
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index d86822b8d..2d84967c6 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -51,6 +51,12 @@ class NodeValue {
    *  reference-counting.  Should be (1 << num_bits(d_rc)) - 1 */
   static const unsigned MAX_RC = 255;
 
+  /** Number of bits assigned to the kind in the NodeValue header */
+  static const unsigned KINDBITS = 8;
+
+  /** A mask for d_kind */
+  static const unsigned kindMask = (1u << KINDBITS) - 1;
+
   // this header fits into one 64-bit word
 
   /** The ID (0 is reserved for the null value) */
@@ -60,7 +66,7 @@ class NodeValue {
   unsigned d_rc        :  8;
 
   /** Kind of the expression */
-  unsigned d_kind      :  8;
+  unsigned d_kind      : KINDBITS;
 
   /** Number of children */
   unsigned d_nchildren : 16;
@@ -178,13 +184,19 @@ public:
     }
   };
 
-
   unsigned getId() const { return d_id; }
-  Kind getKind() const { return (Kind) d_kind; }
+  Kind getKind() const { return dKindToKind(d_kind); }
   unsigned getNumChildren() const { return d_nchildren; }
 
   std::string toString() const;
   void toStream(std::ostream& out) const;
+
+  static inline unsigned kindToDKind(Kind k) {
+    return ((unsigned) k) & kindMask;
+  }
+  static inline Kind dKindToKind(unsigned d) {
+    return (d == kindMask) ? UNDEFINED_KIND : Kind(d);
+  }
 };
 
 }/* CVC4::expr namespace */
diff --git a/src/expr/soft_node.h b/src/expr/soft_node.h
new file mode 100644
index 000000000..fe71a4d1a
--- /dev/null
+++ b/src/expr/soft_node.h
@@ -0,0 +1,36 @@
+/*********************                                           -*- C++ -*-  */
+/** soft_node.h
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): taking
+ ** 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.
+ **
+ ** Encapsulation of a pointer to node information that is explicitly
+ ** NOT reference-counted.  These "smart pointers" do NOT keep live
+ ** the NodeValue object to which they refer.
+ **/
+
+#ifndef __CVC4__SOFT_NODE_H
+#define __CVC4__SOFT_NODE_H
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace expr {
+
+/**
+ * For now, treat SoftNodes as regular Nodes.  We'll address this
+ * later.
+ */
+typedef CVC4::Node SoftNode;
+typedef CVC4::Node TNode;
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SOFT_NODE_H */
diff --git a/src/expr/type.h b/src/expr/type.h
index e5fda779e..19d0c831e 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -29,7 +29,7 @@ class ExprManager;
  * Class encapsulating CVC4 expression types.
  */
 class Type {
- public:
+public:
   /** Comparision for equality */
   bool operator==(const Type& t) const;
 
@@ -229,7 +229,8 @@ public:
  * @param e the type to output
  * @return the stream
  */
-std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC ;
+std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC;
+
 }
 
-#endif // __CVC4__TYPE_H
+#endif /* __CVC4__TYPE_H */
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 533e2cb2d..30fb33a32 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -49,23 +49,26 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) :
 }
 
 Expr AntlrParser::getSymbol(std::string name, SymbolType type) {
-  Assert( isDeclared(name,type) );
+  Assert( isDeclared(name, type) );
+
 
   switch( type ) {
+
   case SYM_VARIABLE: // Functions share var namespace
   case SYM_FUNCTION:
     return d_varSymbolTable.getObject(name);
+
   default:
     Unhandled("Unhandled symbol type!");
   }
 }
 
 Expr AntlrParser::getVariable(std::string name) {
-  return getSymbol(name,SYM_VARIABLE);
+  return getSymbol(name, SYM_VARIABLE);
 }
 
 Expr AntlrParser::getFunction(std::string name) {
-  return getSymbol(name,SYM_FUNCTION);
+  return getSymbol(name, SYM_FUNCTION);
 }
 
 const Type* 
@@ -77,24 +80,24 @@ AntlrParser::getType(std::string var_name,
 }
 
 const Type* AntlrParser::getSort(std::string name) {
-  Assert( isDeclared(name,SYM_SORT) );
+  Assert( isDeclared(name, SYM_SORT) );
   const Type* t = d_sortTable.getObject(name);
   return t;
 }
 
 /* Returns true if name is bound to a boolean variable. */
 bool AntlrParser::isBoolean(std::string name) {
-  return isDeclared(name,SYM_VARIABLE) && getType(name)->isBoolean();
+  return isDeclared(name, SYM_VARIABLE) && getType(name)->isBoolean();
 }
 
 /* Returns true if name is bound to a function. */
 bool AntlrParser::isFunction(std::string name) {
-  return isDeclared(name,SYM_FUNCTION) && getType(name)->isFunction();
+  return isDeclared(name, SYM_FUNCTION) && getType(name)->isFunction();
 }
 
 /* Returns true if name is bound to a function returning boolean. */
 bool AntlrParser::isPredicate(std::string name) {
-  return isDeclared(name,SYM_FUNCTION) && getType(name)->isPredicate();
+  return isDeclared(name, SYM_FUNCTION) && getType(name)->isPredicate();
 }
 
 Expr AntlrParser::getTrueExpr() const {
@@ -160,7 +163,7 @@ const Type* AntlrParser::predicateType(const std::vector<const Type*>& sorts) {
   if(sorts.size() == 0) {
     return d_exprManager->booleanType();
   } else {
-    return d_exprManager->mkFunctionType(sorts,d_exprManager->booleanType());
+    return d_exprManager->mkFunctionType(sorts, d_exprManager->booleanType());
   }
 }
 
@@ -168,7 +171,7 @@ Expr
 AntlrParser::mkVar(const std::string name, const Type* type) {
   Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl;
   Assert( !isDeclared(name) ) ;
-  Expr expr = d_exprManager->mkVar(type);
+  Expr expr = d_exprManager->mkVar(type, name);
   d_varSymbolTable.bindName(name, expr);
   d_varTypeTable.bindName(name,type);
   Assert( isDeclared(name) ) ;
@@ -189,10 +192,10 @@ AntlrParser::mkVars(const std::vector<std::string> names,
 const Type* 
 AntlrParser::newSort(std::string name) {
   Debug("parser") << "newSort(" << name << ")" << std::endl;
-  Assert( !isDeclared(name,SYM_SORT) ) ;
+  Assert( !isDeclared(name, SYM_SORT) ) ;
   const Type* type = d_exprManager->mkSort(name);
-  d_sortTable.bindName(name,type);
-  Assert( isDeclared(name,SYM_SORT) ) ;
+  d_sortTable.bindName(name, type);
+  Assert( isDeclared(name, SYM_SORT) ) ;
   return type;
 }
 
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 9fb5858b3..1bb71860c 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -22,20 +22,12 @@
 #ifndef __CVC4__CNF_STREAM_H
 #define __CVC4__CNF_STREAM_H
 
+
 #include "expr/node.h"
 #include "prop/sat.h"
 
 #include <ext/hash_map>
 
-namespace __gnu_cxx {
-template<>
-  struct hash<CVC4::Node> {
-    size_t operator()(const CVC4::Node& node) const {
-      return (size_t)node.hash();
-    }
-  };
-} /* __gnu_cxx namespace */
-
 namespace CVC4 {
 namespace prop {
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8bca39df4..24795111f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -75,8 +75,8 @@ void SmtEngine::addFormula(const Node& e) {
 }
 
 Result SmtEngine::checkSat(const BoolExpr& e) {
-  Debug("smt") << "SMT checkSat(" << e << ")" << std::endl;
   NodeManagerScope nms(d_nodeManager);
+  Debug("smt") << "SMT checkSat(" << e << ")" << std::endl;
   Node node_e = preprocess(e.getNode());
   addFormula(node_e);
   Result r = check().asSatisfiabilityResult();
@@ -85,8 +85,8 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
 }
 
 Result SmtEngine::query(const BoolExpr& e) {
-  Debug("smt") << "SMT query(" << e << ")" << std::endl;
   NodeManagerScope nms(d_nodeManager);
+  Debug("smt") << "SMT query(" << e << ")" << std::endl;
   Node node_e = preprocess(d_nodeManager->mkNode(NOT, e.getNode()));
   addFormula(node_e);
   Result r = check().asValidityResult();
@@ -95,25 +95,34 @@ Result SmtEngine::query(const BoolExpr& e) {
 }
 
 Result SmtEngine::assertFormula(const BoolExpr& e) {
-  Debug("smt") << "SMT assertFormula(" << e << ")" << std::endl;
   NodeManagerScope nms(d_nodeManager);
+  Debug("smt") << "SMT assertFormula(" << e << ")" << std::endl;
   Node node_e = preprocess(e.getNode());
   addFormula(node_e);
   return quickCheck().asValidityResult();
 }
 
 Expr SmtEngine::simplify(const Expr& e) {
+  NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT simplify(" << e << ")" << std::endl;
-  Expr simplify(const Expr& e);
+  Unimplemented();
+}
+
+Model SmtEngine::getModel() {
+  NodeManagerScope nms(d_nodeManager);
   Unimplemented();
 }
 
 void SmtEngine::push() {
+  NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT push()" << std::endl;
+  Unimplemented();
 }
 
 void SmtEngine::pop() {
+  NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT pop()" << std::endl;
+  Unimplemented();
 }
 
 }/* CVC4 namespace */
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 7a1b75cbc..84465127b 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -24,8 +24,6 @@ TEST_DEPS = \
 	$(TEST_DEPS_DIST) \
 	$(TEST_DEPS_NODIST)
 
-@mk_include@ @srcdir@/Makefile.tests
-
 if HAVE_CXXTESTGEN
 
 AM_CPPFLAGS = \
@@ -46,8 +44,6 @@ AM_LDFLAGS_BLACK = \
 AM_LDFLAGS_PUBLIC = \
 	@abs_top_builddir@/src/libcvc4.la
 
-TESTS = $(UNIT_TESTS)
-
 EXTRA_DIST = \
 	no_cxxtest \
 	$(TEST_DEPS_DIST)
@@ -57,9 +53,17 @@ noinst_LTLIBRARIES = libdummy.la
 libdummy_la_SOURCES = expr/node_black.cpp
 libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la
 
-$(TESTS:%=%.cpp): %.cpp: %.h
+MOSTLYCLEANFILES = $(UNIT_TESTS) $(UNIT_TESTS:%=%.cpp)
+
+@mk_include@ @srcdir@/Makefile.tests
+
+# We leave "TESTS" empty here; it's handled in Makefile.tests (see
+# that file for comment)
+# TESTS =
+
+$(UNIT_TESTS:%=%.cpp): %.cpp: %.h
 	mkdir -p `dirname "$@"`
-	@CXXTESTGEN@ --have-eh --have-std --error-printer -o "$@" "$<"
+	$(CXXTESTGEN) --have-eh --have-std --error-printer -o "$@" "$<"
 $(WHITE_TESTS): %_white: %_white.cpp $(TEST_DEPS)
 	$(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo $<
 	$(CXXLINK) $(AM_LDFLAGS_WHITE) $@.lo
@@ -70,15 +74,13 @@ $(PUBLIC_TESTS): %_public: %_public.cpp $(TEST_DEPS)
 	$(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo $<
 	$(CXXLINK) $(AM_LDFLAGS_PUBLIC) $@.lo
 
-MOSTLYCLEANFILES = $(TESTS) $(TESTS:%=%.cpp)
-
 else
 
 # force a user-visible failure for "make check"
 TESTS = no_cxxtest
 
 EXTRA_DIST = \
-	$(UNIT_TESTS) \
+	$(UNIT_TESTS:%=%.cpp) \
 	$(TEST_DEPS_DIST)
 
 endif
diff --git a/test/unit/Makefile.tests b/test/unit/Makefile.tests
index c542259b1..4f2f3dd5f 100644
--- a/test/unit/Makefile.tests
+++ b/test/unit/Makefile.tests
@@ -1,5 +1,20 @@
-TESTS := $(filter $(TEST_PREFIX)%,$(TESTS))
+# This makefile is separated because it's not under automake control.
+# This gets confusing, because we want:
+#
+#  1. to (re)build only the tests in the "filtered" set of tests
+#     (those that we're going to run)
+#  2. run only the tests in the "filtered" set of tests.
+#
+# It's a pain to make automake happy.
 
-WHITE_TESTS = $(filter %_white,$(TESTS))
-BLACK_TESTS = $(filter %_black,$(TESTS))
-PUBLIC_TESTS = $(filter %_public,$(TESTS))
+# Add "filtered" tests to the set of TESTS
+TESTS = $(filter $(TEST_PREFIX)%,$(UNIT_TESTS))
+
+# subsets of the tests, based on name
+WHITE_TESTS = $(filter %_white,$(UNIT_TESTS))
+BLACK_TESTS = $(filter %_black,$(UNIT_TESTS))
+PUBLIC_TESTS = $(filter %_public,$(UNIT_TESTS))
+
+# This rule forces automake to correctly build our filtered
+# set of tests
+check-TESTS: $(TESTS)
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index fd2cf3332..0693b48db 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -39,7 +39,7 @@ public:
     d_scope = new NodeManagerScope(d_nm);
   }
 
-  void tearDown(){
+  void tearDown() {
     delete d_nm;
     delete d_scope;
   }
@@ -55,7 +55,7 @@ public:
     Node::null();
   }
 
-  void testIsNull(){
+  void testIsNull() {
     /* bool isNull() const; */
 
     Node a = Node::null();
@@ -73,7 +73,7 @@ public:
     Node e(Node::null());
   }
 
-  void testDestructor(){
+  void testDestructor() {
     /* No access to internals ?
      * Makes sense to only test that this is crash free.
      */
@@ -84,7 +84,7 @@ public:
   }
 
   /*tests:  bool operator==(const Node& e) const  */
-  void testOperatorEquals(){
+  void testOperatorEquals() {
     Node a, b, c;
     
     b = d_nm->mkVar();
@@ -122,7 +122,7 @@ public:
   }
 
   /* operator!= */
-  void testOperatorNotEquals(){
+  void testOperatorNotEquals() {
 
 
     Node a, b, c;
@@ -157,7 +157,7 @@ public:
 
   }
 
-  void testOperatorSquare(){  
+  void testOperatorSquare() {  
     /*Node operator[](int i) const */
 
     //Basic bounds check on a node w/out children
@@ -183,7 +183,7 @@ public:
   }
 
   /*tests:   Node& operator=(const Node&); */
-  void testOperatorAssign(){
+  void testOperatorAssign() {
     Node a, b;
     Node c = d_nm->mkNode(NOT);
     
@@ -197,7 +197,7 @@ public:
     TS_ASSERT(a==c);
   }
   
-  void testOperatorLessThan(){
+  void testOperatorLessThan() {
     /* We don't have access to the ids so we can't test the implementation
      * in the black box tests. 
      */
@@ -232,13 +232,13 @@ public:
     std::vector<Node> chain;
     int N = 500;
     Node curr = d_nm->mkNode(NULL_EXPR);
-    for(int i=0;i<N;i++){
+    for(int i=0;i<N;i++) {
       chain.push_back(curr);
       curr = d_nm->mkNode(AND,curr);
     }
     
-    for(int i=0;i<N;i++){
-      for(int j=i+1;j<N;j++){
+    for(int i=0;i<N;i++) {
+      for(int j=i+1;j<N;j++) {
 	Node chain_i = chain[i];
 	Node chain_j = chain[j];
 	TS_ASSERT(chain_i<chain_j);
@@ -247,7 +247,7 @@ public:
     
   }
 
-  void testHash(){
+  void testHash() {
     /* Not sure how to test this except survial... */
     Node a = d_nm->mkNode(ITE);
     Node b = d_nm->mkNode(ITE);
@@ -257,7 +257,7 @@ public:
 
   
 
-  void testEqExpr(){
+  void testEqExpr() {
     /*Node eqExpr(const Node& right) const;*/
 
     Node left = d_nm->mkNode(TRUE);
@@ -272,7 +272,7 @@ public:
     TS_ASSERT(eq[1] == right);
   }
 
-  void testNotExpr(){
+  void testNotExpr() {
     /*  Node notExpr() const;*/
 
     Node child = d_nm->mkNode(TRUE);
@@ -284,7 +284,7 @@ public:
     TS_ASSERT(parent[0] == child);
     
   }
-  void testAndExpr(){
+  void testAndExpr() {
     /*Node andExpr(const Node& right) const;*/
     
     Node left = d_nm->mkNode(TRUE);
@@ -300,7 +300,7 @@ public:
     
   }
 
-  void testOrExpr(){
+  void testOrExpr() {
     /*Node orExpr(const Node& right) const;*/
      
     Node left = d_nm->mkNode(TRUE);
@@ -316,7 +316,7 @@ public:
 
   }
 
-  void testIteExpr(){
+  void testIteExpr() {
     /*Node iteExpr(const Node& thenpart, const Node& elsepart) const;*/
 
     Node cnd = d_nm->mkNode(PLUS);
@@ -333,7 +333,7 @@ public:
     TS_ASSERT(*(++(++ite.begin())) == elseBranch);
   }
 
-  void testIffExpr(){
+  void testIffExpr() {
     /*  Node iffExpr(const Node& right) const; */
      
     Node left = d_nm->mkNode(TRUE);
@@ -349,7 +349,7 @@ public:
   }
 
   
-  void testImpExpr(){
+  void testImpExpr() {
     /* Node impExpr(const Node& right) const; */
     Node left = d_nm->mkNode(TRUE);
     Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE)));
@@ -363,7 +363,7 @@ public:
     TS_ASSERT(*(++eq.begin()) == right);
   }
 
-  void testXorExpr(){
+  void testXorExpr() {
     /*Node xorExpr(const Node& right) const;*/
     Node left = d_nm->mkNode(TRUE);
     Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE)));
@@ -377,26 +377,26 @@ public:
     TS_ASSERT(*(++eq.begin()) == right);
   }
 
-  void testPlusExpr(){
+  void testPlusExpr() {
     /*Node plusExpr(const Node& right) const;*/
     TS_WARN( "TODO: No implementation to test." );
   }
 
-  void testUMinusExpr(){
+  void testUMinusExpr() {
     /*Node uMinusExpr() const;*/
     TS_WARN( "TODO: No implementation to test." );
   }
-  void testMultExpr(){
+  void testMultExpr() {
     /*  Node multExpr(const Node& right) const;*/
     TS_WARN( "TODO: No implementation to test." );    
   }
 
-  void testKindSingleton(Kind k){
+  void testKindSingleton(Kind k) {
     Node n = d_nm->mkNode(k);
     TS_ASSERT(k == n.getKind());
   }
 
-  void testGetKind(){
+  void testGetKind() {
     /*inline Kind getKind() const; */
 
     testKindSingleton(NOT);
diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index c097f2758..73a7b1a54 100644
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -15,13 +15,46 @@
 
 #include <cxxtest/TestSuite.h>
 
+#include <string>
+
+#include "expr/node_value.h"
+#include "expr/node_builder.h"
+#include "expr/node_manager.h"
 #include "expr/node.h"
+#include "expr/attribute.h"
 
 using namespace CVC4;
+using namespace CVC4::expr;
+using namespace std;
+
+struct Test1;
+struct Test2;
+struct Test3;
+struct Test4;
+
+typedef Attribute<Test1, std::string> TestStringAttr1;
+typedef Attribute<Test2, std::string> TestStringAttr2;
+
+typedef Attribute<Test3, bool> TestFlag1;
+typedef Attribute<Test4, bool> TestFlag2;
 
 class NodeWhite : public CxxTest::TestSuite {
+
+  NodeManagerScope *d_scope;
+  NodeManager *d_nm;
+
 public:
 
+  void setUp() {
+    d_nm = new NodeManager();
+    d_scope = new NodeManagerScope(d_nm);
+  }
+
+  void tearDown() {
+    delete d_nm;
+    delete d_scope;
+  }
+
   void testNull() {
     Node::s_null;
   }
@@ -29,4 +62,157 @@ public:
   void testCopyCtor() {
     Node e(Node::s_null);
   }
+
+  void testBuilder() {
+    NodeBuilder<> b;
+    TS_ASSERT(b.d_ev->getId() == 0);
+    TS_ASSERT(b.d_ev->getKind() == UNDEFINED_KIND);
+    TS_ASSERT(b.d_ev->getNumChildren() == 0);
+    /* etc. */
+  }
+
+  void testAttributeIds() {
+    TS_ASSERT(VarNameAttr::s_id == 0);
+    TS_ASSERT(TestStringAttr1::s_id == 1);
+    TS_ASSERT(TestStringAttr2::s_id == 2);
+    TS_ASSERT(attr::LastAttributeId<string>::s_id == 3);
+
+    TS_ASSERT(TypeAttr::s_id == 0);
+    TS_ASSERT(attr::LastAttributeId<void*>::s_id == 1);
+
+    TS_ASSERT(TestFlag1::s_id == 0);
+    TS_ASSERT(TestFlag2::s_id == 1);
+    TS_ASSERT(attr::LastAttributeId<bool>::s_id == 2);
+    TS_ASSERT(TestFlag1::s_bit == 0);
+    TS_ASSERT(TestFlag2::s_bit == 1);
+    TS_ASSERT(attr::BitAssignment::s_bit == 2);
+  }
+
+  void testAttributes() {
+    AttributeManager& am = d_nm->d_am;
+
+    Node a = d_nm->mkVar();
+    Node b = d_nm->mkVar();
+    Node c = d_nm->mkVar();
+    Node unnamed = d_nm->mkVar();
+
+    a.setAttribute(VarNameAttr(), "a");
+    b.setAttribute(VarNameAttr(), "b");
+    c.setAttribute(VarNameAttr(), "c");
+
+    a.setAttribute(TestFlag1(), true);
+    b.setAttribute(TestFlag1(), false);
+    c.setAttribute(TestFlag1(), false);
+    unnamed.setAttribute(TestFlag1(), true);
+
+    a.setAttribute(TestFlag2(), false);
+    b.setAttribute(TestFlag2(), true);
+    c.setAttribute(TestFlag2(), true);
+    unnamed.setAttribute(TestFlag2(), false);
+
+    TS_ASSERT(a.getAttribute(VarNameAttr()) == "a");
+    TS_ASSERT(a.getAttribute(VarNameAttr()) != "b");
+    TS_ASSERT(a.getAttribute(VarNameAttr()) != "c");
+    TS_ASSERT(a.getAttribute(VarNameAttr()) != "");
+
+    TS_ASSERT(b.getAttribute(VarNameAttr()) != "a");
+    TS_ASSERT(b.getAttribute(VarNameAttr()) == "b");
+    TS_ASSERT(b.getAttribute(VarNameAttr()) != "c");
+    TS_ASSERT(b.getAttribute(VarNameAttr()) != "");
+
+    TS_ASSERT(c.getAttribute(VarNameAttr()) != "a");
+    TS_ASSERT(c.getAttribute(VarNameAttr()) != "b");
+    TS_ASSERT(c.getAttribute(VarNameAttr()) == "c");
+    TS_ASSERT(c.getAttribute(VarNameAttr()) != "");
+
+    TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "a");
+    TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "b");
+    TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "c");
+    TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == "");
+
+    TS_ASSERT(! unnamed.hasAttribute(VarNameAttr()));
+
+    TS_ASSERT(! a.hasAttribute(TestStringAttr1()));
+    TS_ASSERT(! b.hasAttribute(TestStringAttr1()));
+    TS_ASSERT(! c.hasAttribute(TestStringAttr1()));
+    TS_ASSERT(! unnamed.hasAttribute(TestStringAttr1()));
+
+    TS_ASSERT(! a.hasAttribute(TestStringAttr2()));
+    TS_ASSERT(! b.hasAttribute(TestStringAttr2()));
+    TS_ASSERT(! c.hasAttribute(TestStringAttr2()));
+    TS_ASSERT(! unnamed.hasAttribute(TestStringAttr2()));
+
+    TS_ASSERT(a.getAttribute(TestFlag1()));
+    TS_ASSERT(! b.getAttribute(TestFlag1()));
+    TS_ASSERT(! c.getAttribute(TestFlag1()));
+    TS_ASSERT(unnamed.getAttribute(TestFlag1()));
+
+    TS_ASSERT(! a.getAttribute(TestFlag2()));
+    TS_ASSERT(b.getAttribute(TestFlag2()));
+    TS_ASSERT(c.getAttribute(TestFlag2()));
+    TS_ASSERT(! unnamed.getAttribute(TestFlag2()));
+
+    a.setAttribute(TestStringAttr1(), "foo");
+    b.setAttribute(TestStringAttr1(), "bar");
+    c.setAttribute(TestStringAttr1(), "baz");
+
+    TS_ASSERT(a.getAttribute(VarNameAttr()) == "a");
+    TS_ASSERT(a.getAttribute(VarNameAttr()) != "b");
+    TS_ASSERT(a.getAttribute(VarNameAttr()) != "c");
+    TS_ASSERT(a.getAttribute(VarNameAttr()) != "");
+
+    TS_ASSERT(b.getAttribute(VarNameAttr()) != "a");
+    TS_ASSERT(b.getAttribute(VarNameAttr()) == "b");
+    TS_ASSERT(b.getAttribute(VarNameAttr()) != "c");
+    TS_ASSERT(b.getAttribute(VarNameAttr()) != "");
+
+    TS_ASSERT(c.getAttribute(VarNameAttr()) != "a");
+    TS_ASSERT(c.getAttribute(VarNameAttr()) != "b");
+    TS_ASSERT(c.getAttribute(VarNameAttr()) == "c");
+    TS_ASSERT(c.getAttribute(VarNameAttr()) != "");
+
+    TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "a");
+    TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "b");
+    TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "c");
+    TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == "");
+
+    TS_ASSERT(! unnamed.hasAttribute(VarNameAttr()));
+
+    TS_ASSERT(a.hasAttribute(TestStringAttr1()));
+    TS_ASSERT(b.hasAttribute(TestStringAttr1()));
+    TS_ASSERT(c.hasAttribute(TestStringAttr1()));
+    TS_ASSERT(! unnamed.hasAttribute(TestStringAttr1()));
+
+    TS_ASSERT(! a.hasAttribute(TestStringAttr2()));
+    TS_ASSERT(! b.hasAttribute(TestStringAttr2()));
+    TS_ASSERT(! c.hasAttribute(TestStringAttr2()));
+    TS_ASSERT(! unnamed.hasAttribute(TestStringAttr2()));
+
+    a.setAttribute(VarNameAttr(), "b");
+    b.setAttribute(VarNameAttr(), "c");
+    c.setAttribute(VarNameAttr(), "a");
+
+    TS_ASSERT(c.getAttribute(VarNameAttr()) == "a");
+    TS_ASSERT(c.getAttribute(VarNameAttr()) != "b");
+    TS_ASSERT(c.getAttribute(VarNameAttr()) != "c");
+    TS_ASSERT(c.getAttribute(VarNameAttr()) != "");
+
+    TS_ASSERT(a.getAttribute(VarNameAttr()) != "a");
+    TS_ASSERT(a.getAttribute(VarNameAttr()) == "b");
+    TS_ASSERT(a.getAttribute(VarNameAttr()) != "c");
+    TS_ASSERT(a.getAttribute(VarNameAttr()) != "");
+
+    TS_ASSERT(b.getAttribute(VarNameAttr()) != "a");
+    TS_ASSERT(b.getAttribute(VarNameAttr()) != "b");
+    TS_ASSERT(b.getAttribute(VarNameAttr()) == "c");
+    TS_ASSERT(b.getAttribute(VarNameAttr()) != "");
+
+    TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "a");
+    TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "b");
+    TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "c");
+    TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == "");
+
+    TS_ASSERT(! unnamed.hasAttribute(VarNameAttr()));
+
+  }
 };