* 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

4 files changed, 241 insertions, 38 deletions

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()));
+
+  }
 };