* NodeBuilder work: specifically, convenience builders. "a && b && c || d && e"

  (etc.) now work for Nodes a, b, c, d, e.  Also refcounting fixes for
  NodeBuilder in certain cases

* (various places) don't overload __gnu_cxx::hash<>, instead provide
  an explicit hash function to hash_maps and hash_sets.

* add a new kind of assert, DtorAssert(), which doesn't throw
  exceptions (right now it operates like a usual C assert()).  For use
  in destructors.

* don't import NodeValue into CVC4 namespace (leave under CVC4::expr::).

* fix some Make rule dependencies

* reformat node.h as per code formatting policy

* added Theory and NodeBuilder unit tests

2 files changed, 117 insertions, 60 deletions

diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 8aff0faf0..871e93dca 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -15,7 +15,6 @@
 
 #include <cxxtest/TestSuite.h>
 
-//Used in some of the tests
 #include <vector>
 #include <limits.h>
 #include <sstream>
@@ -65,7 +64,7 @@ public:
   /**
    * Tests just constructors. No modification is done to the node.
    */
-  void testNodeConstructors(){
+  void testNodeConstructors() {
 
     //inline NodeBuilder();
     //inline NodeBuilder(Kind k);
@@ -151,14 +150,14 @@ public:
 
   }
 
-  void testDestructor(){
+  void testDestructor() {
     //inline ~NodeBuilder();
     NodeBuilder<K>* nb = new NodeBuilder<K>();
     delete nb;
     //Not sure what to test other than survival
   }
 
-  void testBeginEnd(){
+  void testBeginEnd() {
     /* Test begin and ends without resizing */
     NodeBuilder<K> ws;
     TS_ASSERT_EQUALS(ws.begin(), ws.end());
@@ -203,12 +202,12 @@ public:
     TS_ASSERT_EQUALS(smaller_citer, smaller.end());
   }
 
-  void testIterator(){
+  void testIterator() {
     NodeBuilder<> b;
     Node x = d_nm->mkVar();
     Node y = d_nm->mkVar();
     Node z = d_nm->mkVar();
-    b << x << y << z << kind::AND;
+    b << x << y << z << AND;
 
     {
       NodeBuilder<>::iterator i = b.begin();
@@ -228,7 +227,7 @@ public:
     }
   }
 
-  void testGetKind(){
+  void testGetKind() {
     /*  Kind getKind() const; */
     NodeBuilder<> noKind;
     TS_ASSERT_EQUALS(noKind.getKind(), UNDEFINED_KIND);
@@ -244,15 +243,13 @@ public:
     TS_ASSERT_THROWS_ANYTHING(noKind.getKind(););
 #endif
 
-
     NodeBuilder<> spec(specKind);
     TS_ASSERT_EQUALS(spec.getKind(), specKind);
     push_back(spec, K);
     TS_ASSERT_EQUALS(spec.getKind(), specKind);
-
   }
 
-  void testGetNumChildren(){
+  void testGetNumChildren() {
     /* unsigned getNumChildren() const; */
 
     NodeBuilder<> noKind;
@@ -282,7 +279,7 @@ public:
 #endif
   }
 
-  void testOperatorSquare(){
+  void testOperatorSquare() {
     /*
       Node operator[](int i) const {
       Assert(i >= 0 && i < d_ev->getNumChildren());
@@ -332,7 +329,7 @@ public:
 #endif
   }
 
-  void testClear(){
+  void testClear() {
     /* void clear(Kind k = UNDEFINED_KIND); */
     NodeBuilder<> nb;
 
@@ -378,7 +375,7 @@ public:
 
   }
 
-  void testStreamInsertionKind(){
+  void testStreamInsertionKind() {
     /* NodeBuilder& operator<<(const Kind& k); */
 
 #ifdef CVC4_DEBUG
@@ -420,7 +417,7 @@ public:
                      specKind);
   }
 
-  void testStreamInsertionNode(){
+  void testStreamInsertionNode() {
     /* NodeBuilder& operator<<(const Node& n); */
     NodeBuilder<K> nb(specKind);
     TS_ASSERT_EQUALS(nb.getKind(), specKind);
@@ -449,7 +446,7 @@ public:
 
   }
 
-  void testAppend(){
+  void testAppend() {
     Node x = d_nm->mkVar();
     Node y = d_nm->mkVar();
     Node z = d_nm->mkVar();
@@ -499,7 +496,7 @@ public:
     TS_ASSERT(b[8] == m);
   }
 
-  void testOperatorNodeCast(){
+  void testOperatorNodeCast() {
     /* operator Node();*/
     NodeBuilder<K> implicit(specKind);
     NodeBuilder<K> explic(specKind);
@@ -521,7 +518,7 @@ public:
 #endif
   }
 
-  void testToStream(){
+  void testToStream() {
     /* inline void toStream(std::ostream& out) const {
        d_ev->toStream(out);
        }
@@ -571,4 +568,61 @@ public:
     TS_ASSERT_EQUALS(astr, bstr);
     TS_ASSERT_DIFFERS(astr, cstr);
   }
+
+  void testConvenienceBuilders() {
+    Node a = d_nm->mkVar();
+    Node b = d_nm->mkVar();
+    Node c = d_nm->mkVar();
+    Node d = d_nm->mkVar();
+    Node e = d_nm->mkVar();
+    Node f = d_nm->mkVar();
+
+    Node m = a && b;
+    Node n = a && b || c;
+    Node o = d + e - b;
+    Node p = a && o || c;
+
+    Node x = d + e + o - m;
+    Node y = f - a - c + e;
+
+    Node q = a && b && c;
+
+    Node r = e && d && b && a || x && y || f || q && a;
+
+    TS_ASSERT_EQUALS(m, d_nm->mkNode(AND, a, b));
+    TS_ASSERT_EQUALS(n, d_nm->mkNode(OR, m, c));
+    TS_ASSERT_EQUALS(o, d_nm->mkNode(PLUS, d, e, d_nm->mkNode(UMINUS, b)));
+    TS_ASSERT_EQUALS(p, d_nm->mkNode(OR, d_nm->mkNode(AND, a, o), c));
+
+    TS_ASSERT_EQUALS(x, d_nm->mkNode(PLUS, d, e, o, d_nm->mkNode(UMINUS, m)));
+    TS_ASSERT_EQUALS(y, d_nm->mkNode(PLUS,
+                                     f,
+                                     d_nm->mkNode(UMINUS, a),
+                                     d_nm->mkNode(UMINUS, c),
+                                     e));
+
+    TS_ASSERT_EQUALS(q, d_nm->mkNode(AND, a, b, c));
+
+    TS_ASSERT_EQUALS(r, d_nm->mkNode(OR,
+                                     d_nm->mkNode(AND, e, d, b, a),
+                                     d_nm->mkNode(AND, x, y),
+                                     f,
+                                     d_nm->mkNode(AND, q, a)));
+
+    Node assoc1 = (a && b) && c;
+    Node assoc2 = a && (b && c);
+
+    TS_ASSERT_EQUALS(assoc1, d_nm->mkNode(AND, a, b, c));
+    TS_ASSERT_EQUALS(assoc2, d_nm->mkNode(AND, a, d_nm->mkNode(AND, b, c)));
+
+    Node prec1 = (a && b) || c;
+    Node prec2 = a || (b && c);
+    Node prec3 = a && (b || c);
+    Node prec4 = (a || b) && c;
+
+    TS_ASSERT_EQUALS(prec1, d_nm->mkNode(OR, d_nm->mkNode(AND, a, b), c));
+    TS_ASSERT_EQUALS(prec2, d_nm->mkNode(OR, a, d_nm->mkNode(AND, b, c)));
+    TS_ASSERT_EQUALS(prec3, d_nm->mkNode(AND, a, d_nm->mkNode(OR, b, c)));
+    TS_ASSERT_EQUALS(prec4, d_nm->mkNode(AND, d_nm->mkNode(OR, a, b), c));
+  }
 };
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index ee914090e..17fefd07b 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -29,17 +29,17 @@ using namespace CVC4::context;
 
 using namespace std;
 
-
 /**
  * Very basic OutputChannel for testing simple Theory Behaviour.
  * Stores a call sequence for the output channel
  */
-enum OutputChannelCallType{CONFLICT, PROPOGATE, LEMMA, EXPLANATION};
+enum OutputChannelCallType{CONFLICT, PROPAGATE, LEMMA, EXPLANATION};
 class TestOutputChannel : public OutputChannel {
 private:
-  void push(OutputChannelCallType call, TNode n){
-    d_callHistory.push_back(make_pair(call,n));
+  void push(OutputChannelCallType call, TNode n) {
+    d_callHistory.push_back(make_pair(call, n));
   }
+
 public:
   vector< pair<OutputChannelCallType, Node> > d_callHistory;
 
@@ -49,71 +49,78 @@ public:
 
   void safePoint() throw(Interrupted) {}
 
-  void conflict(TNode n, bool safe = false) throw(Interrupted){
+  void conflict(TNode n, bool safe = false) throw(Interrupted) {
     push(CONFLICT, n);
   }
 
-  void propagate(TNode n, bool safe = false) throw(Interrupted){
-    push(PROPOGATE, n);
+  void propagate(TNode n, bool safe = false) throw(Interrupted) {
+    push(PROPAGATE, n);
   }
 
-  void lemma(TNode n, bool safe = false) throw(Interrupted){
+  void lemma(TNode n, bool safe = false) throw(Interrupted) {
     push(LEMMA, n);
   }
-  void explanation(TNode n, bool safe = false) throw(Interrupted){
+  void explanation(TNode n, bool safe = false) throw(Interrupted) {
     push(EXPLANATION, n);
   }
 
-  void clear(){
+  void clear() {
     d_callHistory.clear();
   }
-  Node getIthNode(int i){
+
+  Node getIthNode(int i) {
     Node tmp = (d_callHistory[i]).second;
     return tmp;
   }
 
-  OutputChannelCallType getIthCallType(int i){
+  OutputChannelCallType getIthCallType(int i) {
     return (d_callHistory[i]).first;
   }
 
-  unsigned getNumCalls(){
+  unsigned getNumCalls() {
     return d_callHistory.size();
   }
 };
 
 class DummyTheory : public TheoryImpl<DummyTheory> {
 public:
-  vector<Node> d_registerSequence;
+  set<Node> d_registered;
   vector<Node> d_getSequence;
 
   DummyTheory(context::Context* ctxt, OutputChannel& out) :
     TheoryImpl<DummyTheory>(ctxt, out) {}
 
-  void registerTerm(TNode n){
-    d_registerSequence.push_back(n);
-  }
+  void registerTerm(TNode n) {
+    // check that we registerTerm() a term only once
+    TS_ASSERT(d_registered.find(n) == d_registered.end());
 
+    for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
+      // check that registerTerm() is called in reverse topological order
+      TS_ASSERT(d_registered.find(*i) != d_registered.end());
+    }
+
+    d_registered.insert(n);
+  }
 
-  Node getWrapper(){
+  Node getWrapper() {
     Node n = get();
     d_getSequence.push_back(n);
     return n;
   }
 
-  bool doneWrapper(){
+  bool doneWrapper() {
     return done();
   }
 
-  void check(Effort e){
-    while(!done()){
+  void check(Effort e) {
+    while(!done()) {
       getWrapper();
     }
   }
 
-  void preRegisterTerm(TNode n ){}
-  void propagate(Effort level = FULL_EFFORT){}
-  void explain(TNode n, Effort level = FULL_EFFORT){}
-
+  void preRegisterTerm(TNode n) {}
+  void propagate(Effort level) {}
+  void explain(TNode n, Effort level) {}
 };
 
 class TheoryBlack : public CxxTest::TestSuite {
@@ -132,7 +139,7 @@ class TheoryBlack : public CxxTest::TestSuite {
 
 public:
 
-  TheoryBlack() { }
+  TheoryBlack() {}
 
   void setUp() {
     d_nm = new NodeManager();
@@ -187,15 +194,13 @@ public:
     TS_ASSERT( Theory::quickCheckOrMore(s));
     TS_ASSERT( Theory::quickCheckOrMore(f));
 
-
     TS_ASSERT(!Theory::standardEffortOrMore(m));
     TS_ASSERT(!Theory::standardEffortOrMore(q));
     TS_ASSERT( Theory::standardEffortOrMore(s));
     TS_ASSERT( Theory::standardEffortOrMore(f));
-
   }
 
-  void testDone(){
+  void testDone() {
     TS_ASSERT(d_dummy->doneWrapper());
 
     d_dummy->assertFact(atom0);
@@ -208,7 +213,7 @@ public:
     TS_ASSERT(d_dummy->doneWrapper());
   }
 
-  void testRegisterSequence(){
+  void testRegisterTerm() {
     TS_ASSERT(d_dummy->doneWrapper());
 
     Node x = d_nm->mkVar();
@@ -218,7 +223,6 @@ public:
     Node f_x_eq_x = f_x.eqNode(x);
     Node x_eq_f_f_x = x.eqNode(f_f_x);
 
-
     d_dummy->assertFact(f_x_eq_x);
     d_dummy->assertFact(x_eq_f_f_x);
 
@@ -226,11 +230,13 @@ public:
 
     TS_ASSERT_EQUALS(got, f_x_eq_x);
 
-    TS_ASSERT_EQUALS(4, d_dummy-> d_registerSequence.size());
-    TS_ASSERT_EQUALS(x, d_dummy-> d_registerSequence[0]);
-    TS_ASSERT_EQUALS(f, d_dummy-> d_registerSequence[1]);
-    TS_ASSERT_EQUALS(f_x, d_dummy-> d_registerSequence[2]);
-    TS_ASSERT_EQUALS(f_x_eq_x, d_dummy-> d_registerSequence[3]);
+    TS_ASSERT_EQUALS(4, d_dummy->d_registered.size());
+    TS_ASSERT(d_dummy->d_registered.find(x) != d_dummy->d_registered.end());
+    TS_ASSERT(d_dummy->d_registered.find(f) != d_dummy->d_registered.end());
+    TS_ASSERT(d_dummy->d_registered.find(f_x) != d_dummy->d_registered.end());
+    TS_ASSERT(d_dummy->d_registered.find(f_x_eq_x) != d_dummy->d_registered.end());
+    TS_ASSERT(d_dummy->d_registered.find(f_f_x) == d_dummy->d_registered.end());
+    TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) == d_dummy->d_registered.end());
 
     TS_ASSERT(!d_dummy->doneWrapper());
 
@@ -238,15 +244,14 @@ public:
 
     TS_ASSERT_EQUALS(got, x_eq_f_f_x);
 
-    TS_ASSERT_EQUALS(6, d_dummy-> d_registerSequence.size());
-    TS_ASSERT_EQUALS(f_f_x, d_dummy-> d_registerSequence[4]);
-    TS_ASSERT_EQUALS(x_eq_f_f_x, d_dummy-> d_registerSequence[5]);
+    TS_ASSERT_EQUALS(6, d_dummy->d_registered.size());
+    TS_ASSERT(d_dummy->d_registered.find(f_f_x) != d_dummy->d_registered.end());
+    TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) != d_dummy->d_registered.end());
 
     TS_ASSERT(d_dummy->doneWrapper());
   }
 
-
-  void testOutputChannelAccessors(){
+  void testOutputChannelAccessors() {
     /* void setOutputChannel(OutputChannel& out)  */
     /* OutputChannel& getOutputChannel() */
 
@@ -261,7 +266,5 @@ public:
     const OutputChannel& oc = d_dummy->getOutputChannel();
 
     TS_ASSERT_EQUALS(&oc, &theOtherChannel);
-
   }
-
 };