removing unecessary files

3 files changed, 0 insertions, 720 deletions

diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index d5b6ce5bf..1ab00bf8d 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -4,7 +4,6 @@ UNIT_TESTS = \
 	theory/theory_engine_white \
 	theory/theory_white \
 	theory/theory_arith_white \
-	theory/union_find_black \
 	theory/theory_bv_white \
 	theory/type_enumerator_white \
 	expr/expr_public \
@@ -41,7 +40,6 @@ UNIT_TESTS = \
 	util/bitvector_black \
 	util/datatype_black \
 	util/configuration_black \
-	util/congruence_closure_white \
 	util/output_black \
 	util/exception_black \
 	util/integer_black \
diff --git a/test/unit/theory/union_find_black.h b/test/unit/theory/union_find_black.h
deleted file mode 100644
index fead619d2..000000000
--- a/test/unit/theory/union_find_black.h
+++ /dev/null
@@ -1,189 +0,0 @@
-/*********************                                                        */
-/*! \file union_find_black.h
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
- **
- ** \brief Black box testing of CVC4::datatypes::UnionFind
- **
- ** Black box testing of CVC4::theory::datatypes::UnionFind.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "context/context.h"
-#include "expr/node.h"
-#include "theory/datatypes/union_find.h"
-
-using namespace CVC4;
-using namespace CVC4::theory::datatypes;
-using namespace CVC4::context;
-
-using namespace std;
-
-/**
- * Test the UnionFind.
- */
-class UnionFindBlack : public CxxTest::TestSuite {
-  Context* d_ctxt;
-  UnionFind<TNode, TNodeHashFunction>* d_uf;
-  NodeManager* d_nm;
-  NodeManagerScope* d_scope;
-
-  Node a, b, c, d, e, f, g;
-
-public:
-
-  void setUp() {
-    d_ctxt = new Context;
-    d_nm = new NodeManager(d_ctxt, NULL);
-    d_scope = new NodeManagerScope(d_nm);
-    d_uf = new UnionFind<TNode, TNodeHashFunction>(d_ctxt);
-
-    a = d_nm->mkVar("a", d_nm->realType());
-    b = d_nm->mkVar("b", d_nm->realType());
-    c = d_nm->mkVar("c", d_nm->realType());
-    d = d_nm->mkVar("d", d_nm->realType());
-    e = d_nm->mkVar("e", d_nm->realType());
-    f = d_nm->mkVar("f", d_nm->realType());
-    g = d_nm->mkVar("g", d_nm->realType());
-  }
-
-  void tearDown() {
-    g = Node::null();
-    f = Node::null();
-    e = Node::null();
-    d = Node::null();
-    c = Node::null();
-    b = Node::null();
-    a = Node::null();
-
-    delete d_uf;
-    delete d_scope;
-    delete d_nm;
-    delete d_ctxt;
-  }
-
-  void testSimpleContextual() {
-    TS_ASSERT(d_uf->find(a) == a);
-    TS_ASSERT(d_uf->find(b) == b);
-    TS_ASSERT(d_uf->find(c) == c);
-    TS_ASSERT(d_uf->find(d) == d);
-    TS_ASSERT(d_uf->find(e) == e);
-    TS_ASSERT(d_uf->find(f) == f);
-    TS_ASSERT(d_uf->find(g) == g);
-
-    d_ctxt->push();
-
-    d_uf->setCanon(a, b);
-
-    TS_ASSERT(d_uf->find(a) == b);
-    TS_ASSERT(d_uf->find(b) == b);
-    TS_ASSERT(d_uf->find(c) == c);
-    TS_ASSERT(d_uf->find(d) == d);
-    TS_ASSERT(d_uf->find(e) == e);
-    TS_ASSERT(d_uf->find(f) == f);
-    TS_ASSERT(d_uf->find(g) == g);
-
-    d_ctxt->push();
-    {
-      TS_ASSERT(d_uf->find(a) == b);
-      TS_ASSERT(d_uf->find(b) == b);
-      TS_ASSERT(d_uf->find(c) == c);
-      TS_ASSERT(d_uf->find(d) == d);
-      TS_ASSERT(d_uf->find(e) == e);
-      TS_ASSERT(d_uf->find(f) == f);
-      TS_ASSERT(d_uf->find(g) == g);
-
-      d_uf->setCanon(c, d);
-      d_uf->setCanon(f, e);
-
-      TS_ASSERT(d_uf->find(a) == b);
-      TS_ASSERT(d_uf->find(b) == b);
-      TS_ASSERT(d_uf->find(c) == d);
-      TS_ASSERT(d_uf->find(d) == d);
-      TS_ASSERT(d_uf->find(e) == e);
-      TS_ASSERT(d_uf->find(f) == e);
-      TS_ASSERT(d_uf->find(g) == g);
-
-      d_ctxt->push();
-      {
-
-        TS_ASSERT(d_uf->find(a) == b);
-        TS_ASSERT(d_uf->find(b) == b);
-        TS_ASSERT(d_uf->find(c) == d);
-        TS_ASSERT(d_uf->find(d) == d);
-        TS_ASSERT(d_uf->find(e) == e);
-        TS_ASSERT(d_uf->find(f) == e);
-        TS_ASSERT(d_uf->find(g) == g);
-
-#ifdef CVC4_ASSERTIONS
-        TS_ASSERT_THROWS(d_uf->setCanon(a, c), AssertionException);
-        TS_ASSERT_THROWS(d_uf->setCanon(d_uf->find(a), c), AssertionException);
-        TS_ASSERT_THROWS(d_uf->setCanon(a, d_uf->find(c)), AssertionException);
-#endif /* CVC4_ASSERTIONS */
-        d_uf->setCanon(d_uf->find(a), d_uf->find(c));
-        d_uf->setCanon(d_uf->find(f), g);
-        d_uf->setCanon(d_uf->find(e), d);
-#ifdef CVC4_ASSERTIONS
-        TS_ASSERT_THROWS(d_uf->setCanon(d_uf->find(c), f), AssertionException);
-#endif /* CVC4_ASSERTIONS */
-        d_uf->setCanon(d_uf->find(c), d_uf->find(f));
-
-        TS_ASSERT(d_uf->find(a) == d);
-        TS_ASSERT(d_uf->find(b) == d);
-        TS_ASSERT(d_uf->find(c) == d);
-        TS_ASSERT(d_uf->find(d) == d);
-        TS_ASSERT(d_uf->find(e) == d);
-        TS_ASSERT(d_uf->find(f) == d);
-        TS_ASSERT(d_uf->find(g) == d);
-
-        d_uf->setCanon(d_uf->find(g), d_uf->find(a));
-
-        TS_ASSERT(d_uf->find(a) == d);
-        TS_ASSERT(d_uf->find(b) == d);
-        TS_ASSERT(d_uf->find(c) == d);
-        TS_ASSERT(d_uf->find(d) == d);
-        TS_ASSERT(d_uf->find(e) == d);
-        TS_ASSERT(d_uf->find(f) == d);
-        TS_ASSERT(d_uf->find(g) == d);
-
-      }
-      d_ctxt->pop();
-
-      TS_ASSERT(d_uf->find(a) == b);
-      TS_ASSERT(d_uf->find(b) == b);
-      TS_ASSERT(d_uf->find(c) == d);
-      TS_ASSERT(d_uf->find(d) == d);
-      TS_ASSERT(d_uf->find(e) == e);
-      TS_ASSERT(d_uf->find(f) == e);
-      TS_ASSERT(d_uf->find(g) == g);
-    }
-    d_ctxt->pop();
-
-    TS_ASSERT(d_uf->find(a) == b);
-    TS_ASSERT(d_uf->find(b) == b);
-    TS_ASSERT(d_uf->find(c) == c);
-    TS_ASSERT(d_uf->find(d) == d);
-    TS_ASSERT(d_uf->find(e) == e);
-    TS_ASSERT(d_uf->find(f) == f);
-    TS_ASSERT(d_uf->find(g) == g);
-
-    d_ctxt->pop();
-
-    TS_ASSERT(d_uf->find(a) == a);
-    TS_ASSERT(d_uf->find(b) == b);
-    TS_ASSERT(d_uf->find(c) == c);
-    TS_ASSERT(d_uf->find(d) == d);
-    TS_ASSERT(d_uf->find(e) == e);
-    TS_ASSERT(d_uf->find(f) == f);
-    TS_ASSERT(d_uf->find(g) == g);
-  }
-};
diff --git a/test/unit/util/congruence_closure_white.h b/test/unit/util/congruence_closure_white.h
deleted file mode 100644
index 0c14160f7..000000000
--- a/test/unit/util/congruence_closure_white.h
+++ /dev/null
@@ -1,529 +0,0 @@
-/*********************                                                        */
-/*! \file congruence_closure_white.h
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
- **
- ** \brief White box testing of CVC4::CongruenceClosure.
- **
- ** White box testing of CVC4::CongruenceClosure.
- **/
-
-#include <cxxtest/TestSuite.h>
-#include <sstream>
-
-#include "context/context.h"
-#include "context/cdhashset.h"
-#include "context/cdhashmap.h"
-#include "expr/node.h"
-#include "expr/kind.h"
-#include "expr/node_manager.h"
-#include "util/congruence_closure.h"
-
-
-using namespace CVC4;
-using namespace CVC4::context;
-using namespace std;
-
-
-struct MyOutputChannel {
-  CDHashSet<Node, NodeHashFunction> d_notifications;
-  CDHashMap<Node, Node, NodeHashFunction> d_equivalences;
-  NodeManager* d_nm;
-
-  MyOutputChannel(Context* ctxt, NodeManager* nm) :
-    d_notifications(ctxt),
-    d_equivalences(ctxt),
-    d_nm(nm) {
-  }
-
-  bool saw(TNode a, TNode b) {
-    return d_notifications.contains(d_nm->mkNode(kind::EQUAL, a, b)) ||
-      d_notifications.contains(d_nm->mkNode(kind::EQUAL, b, a));
-  }
-
-  TNode find(TNode n) {
-    CDHashMap<Node, Node, NodeHashFunction>::iterator i = d_equivalences.find(n);
-    if(i == d_equivalences.end()) {
-      return n;
-    } else {
-      // lazy path compression
-      TNode p = (*i).second; // parent
-      TNode f = d_equivalences[n] = find(p); // compress
-      return f;
-    }
-  }
-
-  bool areCongruent(TNode a, TNode b) {
-    Debug("cc") << "=== a is  " << a << std::endl
-                << "=== a' is " << find(a) << std::endl
-                << "=== b is  " << b << std::endl
-                << "=== b' is " << find(b) << std::endl;
-
-    return find(a) == find(b);
-  }
-
-  void notifyCongruent(TNode a, TNode b) {
-    Debug("cc") << "======OI!  I've been notified of: "
-                << a << " == " << b << std::endl;
-
-    Node eq = d_nm->mkNode(kind::EQUAL, a, b);
-    Node eqRev = d_nm->mkNode(kind::EQUAL, b, a);
-
-    TS_ASSERT(!d_notifications.contains(eq));
-    TS_ASSERT(!d_notifications.contains(eqRev));
-
-    d_notifications.insert(eq);
-
-    d_equivalences.insert(a, b);
-  }
-};/* class MyOutputChannel */
-
-
-class CongruenceClosureWhite : public CxxTest::TestSuite {
-  Context* d_context;
-  NodeManager* d_nm;
-  NodeManagerScope* d_scope;
-  MyOutputChannel* d_out;
-  CongruenceClosure<MyOutputChannel, CongruenceOperator<kind::APPLY_UF> >* d_cc;
-  CongruenceClosure<MyOutputChannel, CONGRUENCE_OPERATORS_2(kind::SELECT, kind::STORE)>* d_ccArray;
-
-  TypeNode U;
-  Node a, f, fa, ffa, fffa, ffffa, b, fb, ffb, fffb, ffffb;
-  Node g, gab, gba, gfafb, gfbfa, gfaa, gbfb;
-  Node h, hab, hba, hfaa;
-  Node a_eq_b, fa_eq_b, a_eq_fb, fa_eq_fb, h_eq_g;
-
-  Node ar, ar_a, ar_b;
-  Node arar, arar_a, arar_b;
-
-public:
-
-  void setUp() {
-    d_context = new Context;
-    d_nm = new NodeManager(d_context, NULL);
-    d_scope = new NodeManagerScope(d_nm);
-    d_out = new MyOutputChannel(d_context, d_nm);
-    d_cc = new CongruenceClosure<MyOutputChannel, CongruenceOperator<kind::APPLY_UF> >(d_context, d_out);
-    d_ccArray = new CongruenceClosure<MyOutputChannel, CONGRUENCE_OPERATORS_2(kind::SELECT, kind::STORE)>(d_context, d_out);
-
-    U = d_nm->mkSort("U");
-
-    f = d_nm->mkVar("f", d_nm->mkFunctionType(U, U));
-    a = d_nm->mkVar("a", U);
-    fa = d_nm->mkNode(kind::APPLY_UF, f, a);
-    ffa = d_nm->mkNode(kind::APPLY_UF, f, fa);
-    fffa = d_nm->mkNode(kind::APPLY_UF, f, ffa);
-    ffffa = d_nm->mkNode(kind::APPLY_UF, f, fffa);
-    b = d_nm->mkVar("b", U);
-    fb = d_nm->mkNode(kind::APPLY_UF, f, b);
-    ffb = d_nm->mkNode(kind::APPLY_UF, f, fb);
-    fffb = d_nm->mkNode(kind::APPLY_UF, f, ffb);
-    ffffb = d_nm->mkNode(kind::APPLY_UF, f, fffb);
-    vector<TypeNode> args(2, U);
-    g = d_nm->mkVar("g", d_nm->mkFunctionType(args, U));
-    gab = d_nm->mkNode(kind::APPLY_UF, g, a, b);
-    gfafb = d_nm->mkNode(kind::APPLY_UF, g, fa, fb);
-    gba = d_nm->mkNode(kind::APPLY_UF, g, b, a);
-    gfbfa = d_nm->mkNode(kind::APPLY_UF, g, fb, fa);
-    gfaa = d_nm->mkNode(kind::APPLY_UF, g, fa, a);
-    gbfb = d_nm->mkNode(kind::APPLY_UF, g, b, fb);
-    h = d_nm->mkVar("h", d_nm->mkFunctionType(args, U));
-    hab = d_nm->mkNode(kind::APPLY_UF, h, a, b);
-    hba = d_nm->mkNode(kind::APPLY_UF, h, b, a);
-    hfaa = d_nm->mkNode(kind::APPLY_UF, h, fa, a);
-
-    a_eq_b = d_nm->mkNode(kind::EQUAL, a, b);
-    fa_eq_b = d_nm->mkNode(kind::EQUAL, fa, b);
-    a_eq_fb = d_nm->mkNode(kind::EQUAL, a, fb);
-    fa_eq_fb = d_nm->mkNode(kind::EQUAL, fa, fb);
-
-    h_eq_g = d_nm->mkNode(kind::EQUAL, h, g);
-
-    // arrays
-    ar = d_nm->mkVar("ar", d_nm->mkArrayType(U, U));
-    ar_a = d_nm->mkNode(kind::SELECT, ar, a);
-    ar_b = d_nm->mkNode(kind::SELECT, ar, b);
-
-    arar = d_nm->mkVar("arar", d_nm->mkArrayType(U, d_nm->mkArrayType(U, U)));
-    arar_a = d_nm->mkNode(kind::SELECT, arar, a);
-    arar_b = d_nm->mkNode(kind::SELECT, arar, b);
-  }
-
-  void tearDown() {
-    try {
-      arar = arar_a = arar_b = Node::null();
-      ar = ar_a = ar_b = Node::null();
-
-      f = a = fa = ffa = fffa = ffffa = Node::null();
-      b = fb = ffb = fffb = ffffb = Node::null();
-      g = gab = gba = gfafb = gfbfa = gfaa = gbfb = Node::null();
-      h = hab = hba = hfaa = Node::null();
-      a_eq_b = fa_eq_b = a_eq_fb = fa_eq_fb = h_eq_g = Node::null();
-      U = TypeNode::null();
-
-      delete d_ccArray;
-      delete d_cc;
-      delete d_out;
-      delete d_scope;
-      delete d_nm;
-      delete d_context;
-    } catch(Exception& e) {
-      cout << "\n\n" << e << "\n\n";
-      throw;
-    }
-  }
-
-  void testSimple() {
-    //Debug.on("cc");
-    // add terms, then add equalities
-
-    d_cc->addTerm(fa);
-    d_cc->addTerm(fb);
-
-    d_cc->addEquality(a_eq_b);
-
-    TS_ASSERT(d_out->areCongruent(fa, fb));
-    TS_ASSERT(d_cc->areCongruent(fa, fb));
-
-    TS_ASSERT(!d_out->areCongruent(a, b));
-    TS_ASSERT(d_cc->areCongruent(a, b));
-  }
-
-  void testSimpleReverse() {
-    // add equalities, then add terms; should get the same as
-    // testSimple()
-
-    d_cc->addEquality(a_eq_b);
-
-    d_cc->addTerm(fa);
-    d_cc->addTerm(fb);
-
-    TS_ASSERT(d_out->areCongruent(fa, fb));
-    TS_ASSERT(d_cc->areCongruent(fa, fb));
-
-    TS_ASSERT(!d_out->areCongruent(a, b));
-    TS_ASSERT(d_cc->areCongruent(a, b));
-  }
-
-  void testSimpleContextual() {
-    TS_ASSERT(!d_out->areCongruent(fa, fb));
-    TS_ASSERT(!d_cc->areCongruent(fa, fb));
-
-    TS_ASSERT(!d_out->areCongruent(a, b));
-    TS_ASSERT(!d_cc->areCongruent(a, b));
-
-    {
-      d_context->push();
-
-      d_cc->addTerm(fa);
-      d_cc->addTerm(fb);
-
-      TS_ASSERT(!d_out->areCongruent(fa, fb));
-      TS_ASSERT(!d_cc->areCongruent(fa, fb));
-
-      TS_ASSERT(!d_out->areCongruent(a, b));
-      TS_ASSERT(!d_cc->areCongruent(a, b));
-
-      {
-        d_context->push();
-
-        d_cc->addEquality(a_eq_b);
-
-        TS_ASSERT(d_out->areCongruent(fa, fb));
-        TS_ASSERT(d_cc->areCongruent(fa, fb));
-
-        TS_ASSERT(!d_out->areCongruent(a, b));
-        TS_ASSERT(d_cc->areCongruent(a, b));
-
-        d_context->pop();
-      }
-
-      TS_ASSERT(!d_out->areCongruent(fa, fb));
-      TS_ASSERT(!d_cc->areCongruent(fa, fb));
-
-      TS_ASSERT(!d_out->areCongruent(a, b));
-      TS_ASSERT(!d_cc->areCongruent(a, b));
-
-      d_context->pop();
-    }
-
-    TS_ASSERT(!d_out->areCongruent(fa, fb));
-    TS_ASSERT(!d_cc->areCongruent(fa, fb));
-
-    TS_ASSERT(!d_out->areCongruent(a, b));
-    TS_ASSERT(!d_cc->areCongruent(a, b));
-  }
-
-  void testSimpleContextualReverse() {
-    TS_ASSERT(!d_out->areCongruent(fa, fb));
-    TS_ASSERT(!d_cc->areCongruent(fa, fb));
-
-    TS_ASSERT(!d_out->areCongruent(a, b));
-    TS_ASSERT(!d_cc->areCongruent(a, b));
-
-    {
-      d_context->push();
-
-      d_cc->addEquality(a_eq_b);
-
-      TS_ASSERT(!d_out->areCongruent(fa, fb));
-      TS_ASSERT(d_cc->areCongruent(fa, fb));
-
-      TS_ASSERT(!d_out->areCongruent(a, b));
-      TS_ASSERT(d_cc->areCongruent(a, b));
-
-      {
-        d_context->push();
-
-        d_cc->addTerm(fa);
-        d_cc->addTerm(fb);
-
-        TS_ASSERT(d_out->areCongruent(fa, fb));
-        TS_ASSERT(d_cc->areCongruent(fa, fb));
-
-        TS_ASSERT(!d_out->areCongruent(a, b));
-        TS_ASSERT(d_cc->areCongruent(a, b));
-
-        d_context->pop();
-      }
-
-      TS_ASSERT(!d_out->areCongruent(fa, fb));
-      TS_ASSERT(d_cc->areCongruent(fa, fb));
-
-      TS_ASSERT(!d_out->areCongruent(a, b));
-      TS_ASSERT(d_cc->areCongruent(a, b));
-
-      d_context->pop();
-    }
-
-    TS_ASSERT(!d_out->areCongruent(fa, fb));
-    TS_ASSERT(!d_cc->areCongruent(fa, fb));
-
-    TS_ASSERT(!d_out->areCongruent(a, b));
-    TS_ASSERT(!d_cc->areCongruent(a, b));
-  }
-
-  void test_f_of_f_of_something() {
-    d_cc->addTerm(ffa);
-    d_cc->addTerm(ffb);
-
-    d_cc->addEquality(a_eq_b);
-
-    TS_ASSERT(d_out->areCongruent(ffa, ffb));
-    TS_ASSERT(d_cc->areCongruent(ffa, ffb));
-
-    TS_ASSERT(!d_out->areCongruent(fa, fb));
-    TS_ASSERT(d_cc->areCongruent(fa, fb));
-
-    TS_ASSERT(!d_out->areCongruent(a, b));
-    TS_ASSERT(d_cc->areCongruent(a, b));
-  }
-
-  void test_f4_of_something() {
-    d_cc->addTerm(ffffa);
-    d_cc->addTerm(ffffb);
-
-    d_cc->addEquality(a_eq_b);
-
-    TS_ASSERT(d_out->areCongruent(ffffa, ffffb));
-    TS_ASSERT(d_cc->areCongruent(ffffa, ffffb));
-
-    TS_ASSERT(!d_out->areCongruent(fffa, fffb));
-    TS_ASSERT(d_cc->areCongruent(fffa, fffb));
-
-    TS_ASSERT(!d_out->areCongruent(ffa, ffb));
-    TS_ASSERT(d_cc->areCongruent(ffa, ffb));
-
-    TS_ASSERT(!d_out->areCongruent(fa, fb));
-    TS_ASSERT(d_cc->areCongruent(fa, fb));
-
-    TS_ASSERT(!d_out->areCongruent(a, b));
-    TS_ASSERT(d_cc->areCongruent(a, b));
-  }
-
-  void testSimpleBinaryFunction() {
-    d_cc->addTerm(gab);
-    d_cc->addTerm(gba);
-
-    d_cc->addEquality(a_eq_b);
-
-    TS_ASSERT(d_out->areCongruent(gab, gba));
-    TS_ASSERT(d_cc->areCongruent(gab, gba));
-  }
-
-  void testSimpleBinaryFunction2() {
-
-    //Debug.on("cc");
-    try {
-
-    d_cc->addTerm(gfafb);
-    d_cc->addTerm(gba);
-    d_cc->addTerm(gfaa);
-    d_cc->addTerm(hfaa);
-
-    d_cc->addEquality(a_eq_fb);
-    d_cc->addEquality(fa_eq_b);
-
-    TS_ASSERT(d_cc->areCongruent(a, fb));
-    TS_ASSERT(d_cc->areCongruent(b, fa));
-    TS_ASSERT(d_cc->areCongruent(fb, ffa));
-
-    Debug("cc") << "\n\n\n"
-                << "a norm:     " << d_cc->normalize(a) << std::endl
-                << "fb norm:    " << d_cc->normalize(fb) << std::endl
-                << "b norm:     " << d_cc->normalize(b) << std::endl
-                << "fa norm:    " << d_cc->normalize(fa) << std::endl
-                << "ffa norm:   " << d_cc->normalize(ffa) << std::endl
-                << "ffffa norm  " << d_cc->normalize(ffffa) << std::endl
-                << "ffffb norm  " << d_cc->normalize(ffffb) << std::endl
-                << "gba norm:   " << d_cc->normalize(gba) << std::endl
-                << "gfaa norm:  " << d_cc->normalize(gfaa) << std::endl
-                << "gbfb norm:  " << d_cc->normalize(gbfb) << std::endl
-                << "gfafb norm: " << d_cc->normalize(gfafb) << std::endl
-                << "hab norm:   " << d_cc->normalize(hab) << std::endl
-                << "hba norm:   " << d_cc->normalize(hba) << std::endl
-                << "hfaa norm:  " << d_cc->normalize(hfaa) << std::endl;
-
-    TS_ASSERT(d_out->areCongruent(gfafb, gba));
-    TS_ASSERT(d_cc->areCongruent(b, fa));
-    TS_ASSERT(d_cc->areCongruent(gfafb, gba));
-    TS_ASSERT(d_cc->areCongruent(hba, hba));
-    TS_ASSERT(d_cc->areCongruent(hfaa, hba));
-    TS_ASSERT(d_out->areCongruent(gfaa, gba));
-    TS_ASSERT(d_cc->areCongruent(gfaa, gba));
-
-    } catch(Exception& e) {
-      cout << "\n\n" << e << "\n\n";
-      throw;
-    }
-  }
-
-  void testUF() {
-    //Debug.on("cc");
-    try{
-    Node c_0 = d_nm->mkVar("c_0", U);
-    Node c_1 = d_nm->mkVar("c_1", U);
-    Node c_2 = d_nm->mkVar("c_2", U);
-    Node c2 = d_nm->mkVar("c2", U);
-    Node c3 = d_nm->mkVar("c3", U);
-    Node c4 = d_nm->mkVar("c4", U);
-    Node c5 = d_nm->mkVar("c5", U);
-    Node c6 = d_nm->mkVar("c6", U);
-    Node c7 = d_nm->mkVar("c7", U);
-    Node c8 = d_nm->mkVar("c8", U);
-    Node c9 = d_nm->mkVar("c9", U);
-    vector<TypeNode> args2U(2, U);
-    Node f1 = d_nm->mkVar("f1", d_nm->mkFunctionType(args2U, U));
-
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_0),c_0),d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_0))));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_0),c_2),d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_2))));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_1),c_1),d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_1))));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_1),c_2),d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_2))));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_1),c_2),d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_2))));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_2),c_0),d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_0))));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_2),c_1),d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_1))));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_0)))),d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_2))))));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c2,c8),d_nm->mkNode(kind::APPLY_UF, f1,c4,c9)));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c9,c_0));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c8,c_0));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c4,c_0));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c2,c_0));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c5,c_0));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c7,c_0));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c3,c_0));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c6,c_1));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_2),c_0));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_1),c_0));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_0),c_0));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_2),c_0));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_1),c_0));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_0),c_1));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_1),c_0));
-    d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_0),c_0));
-    } catch(Exception& e) {
-      cout << "\n\n" << e << "\n\n";
-      throw e;
-    }
-  }
-
-  void testUF2() {
-    Node f = d_nm->mkVar("f", d_nm->mkFunctionType(U, U));
-    Node x = d_nm->mkVar("x", U);
-    Node y = d_nm->mkVar("y", U);
-    Node z = d_nm->mkVar("z", U);
-    Node ffx = d_nm->mkNode(kind::APPLY_UF, f, d_nm->mkNode(kind::APPLY_UF, f, x));
-    Node fffx = d_nm->mkNode(kind::APPLY_UF, f, ffx);
-    Node ffffx = d_nm->mkNode(kind::APPLY_UF, f, fffx);
-    Node ffx_eq_fffx = ffx.eqNode(fffx);
-    Node ffx_eq_y = ffx.eqNode(y);
-    Node ffffx_eq_z = ffffx.eqNode(z);
-
-    d_cc->addEquality(ffx_eq_fffx);
-    d_cc->addEquality(ffx_eq_y);
-    d_cc->addEquality(ffffx_eq_z);
-  }
-
-  void testSimpleArray() {
-    //Debug.on("cc");
-    // add terms, then add equalities
-    try {
-    d_ccArray->addTerm(ar_a);
-    d_ccArray->addTerm(ar_b);
-
-    d_ccArray->addEquality(a_eq_b);
-
-    TS_ASSERT(d_out->areCongruent(ar_a, ar_b));
-    TS_ASSERT(d_ccArray->areCongruent(ar_a, ar_b));
-
-    TS_ASSERT(!d_out->areCongruent(a, b));
-    TS_ASSERT(d_ccArray->areCongruent(a, b));
-    } catch(Exception& e) {
-      cout << "\n\n" << e << "\n\n";
-      throw;
-    }
-  }
-
-  void testSimpleReverseArray() {
-    // add equalities, then add terms; should get the same as
-    // testSimple()
-
-    d_ccArray->addEquality(a_eq_b);
-
-    d_ccArray->addTerm(ar_a);
-    d_ccArray->addTerm(ar_b);
-
-    TS_ASSERT(d_out->areCongruent(ar_a, ar_b));
-    TS_ASSERT(d_ccArray->areCongruent(ar_a, ar_b));
-
-    TS_ASSERT(!d_out->areCongruent(a, b));
-    TS_ASSERT(d_ccArray->areCongruent(a, b));
-  }
-
-  void testArray() {
-    Node ar_eq_arar_a = d_nm->mkNode(kind::EQUAL, ar, arar_a);
-    Node ar2 = d_nm->mkVar("ar2", d_nm->mkArrayType(U, U));
-    Node store_arar_b_ar2 = d_nm->mkNode(kind::STORE, arar, b, ar2);
-    Node select__store_arar_b_ar2__a =
-      d_nm->mkNode(kind::SELECT, store_arar_b_ar2, a);
-    Node select__store_arar_b_ar2__a__eq__arar_a =
-      d_nm->mkNode(kind::EQUAL, select__store_arar_b_ar2__a, arar_a);
-
-    d_ccArray->addTerm(ar);
-    d_ccArray->addTerm(select__store_arar_b_ar2__a);
-
-    d_ccArray->addEquality(ar_eq_arar_a);
-    d_ccArray->addEquality(select__store_arar_b_ar2__a__eq__arar_a);
-
-    TS_ASSERT(d_ccArray->areCongruent(ar, select__store_arar_b_ar2__a));
-    TS_ASSERT(d_out->areCongruent(ar, select__store_arar_b_ar2__a));
-  }
-
-};/* class CongruenceClosureWhite */