* 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

1 files changed, 25 insertions, 7 deletions

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 {