Merge from "cc" branch:

CongruenceClosure implementation; CongruenceClosure white-box test.

New UF theory implementation based on new CC module.  This one
supports predicates.  The two UF implementations exist in parallel
(they can be selected at runtime via the new command line option
"--uf").

Added type infrastructure for TUPLE.

Fixes to unit tests that failed in 16-August-2010 regressions.
Needed to instantiate TheoryEngine with an Options structure, and
explicitly call ->shutdown() on it before destruction (like the
SMTEngine does).

Fixed test makefiles to (1) perform all tests even in the presence of
failures, (2) give proper summaries of subdirectory tests
(e.g. regress0/uf and regress0/precedence)

Other minor changes.

13 files changed, 485 insertions, 17 deletions

diff --git a/test/Makefile.am b/test/Makefile.am
index 2b79c5045..501f85090 100644
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -26,7 +26,7 @@ test "X$(AM_COLOR_TESTS)" != Xno \
   blu=''; \
   std=''; \
 }
-subdirs_to_check = unit system regress/regress0 regress/regress1 regress/regress2 regress/regress3
+subdirs_to_check = unit system regress/regress0 regress/regress0/uf regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3
 check-recursive: check-pre
 .PHONY: check-pre
 check-pre:
diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am
index a3808b751..80e8da387 100644
--- a/test/regress/Makefile.am
+++ b/test/regress/Makefile.am
@@ -1,6 +1,8 @@
 SUBDIRS = regress0
 DIST_SUBDIRS = regress0 regress1 regress2 regress3
 
+MAKEFLAGS = -k
+
 export VERBOSE = 1
 
 .PHONY: regress0 regress1 regress2 regress3
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 09dc52ce4..7f732b17f 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,6 +1,7 @@
 SUBDIRS = . precedence uf
 
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
+MAKEFLAGS = -k
 
 # These are run for all build profiles.
 # If a test shouldn't be run in e.g. competition mode,
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index bf516107e..452024309 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -16,9 +16,9 @@ TESTS =	\
 	euf_simp11.smt \
 	euf_simp12.smt \
 	euf_simp13.smt \
+	eq_diamond1.smt \
 	dead_dnd002.smt \
 	iso_brn001.smt \
-	SEQ032_size2.smt \
 	simple.01.cvc \
 	simple.02.cvc \
 	simple.03.cvc \
diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am
index abc4efcc7..4e4a42a31 100644
--- a/test/regress/regress1/Makefile.am
+++ b/test/regress/regress1/Makefile.am
@@ -1,6 +1,7 @@
 SUBDIRS = .
 
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
+MAKEFLAGS = -k
 
 # These are run for all build profiles.
 # If a test shouldn't be run in e.g. competition mode,
diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am
index 51d145859..1651865fd 100644
--- a/test/regress/regress2/Makefile.am
+++ b/test/regress/regress2/Makefile.am
@@ -1,6 +1,7 @@
 SUBDIRS = .
 
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
+MAKEFLAGS = -k
 
 # These are run for all build profiles.
 # If a test shouldn't be run in e.g. competition mode,
diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am
index 81fb8616e..744ec5775 100644
--- a/test/regress/regress3/Makefile.am
+++ b/test/regress/regress3/Makefile.am
@@ -1,6 +1,7 @@
 SUBDIRS = .
 
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
+MAKEFLAGS = -k
 
 # These are run for all build profiles.
 # If a test shouldn't be run in e.g. competition mode,
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index f25862b54..eb920e6c5 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -3,7 +3,7 @@ UNIT_TESTS = \
 	theory/shared_term_manager_black \
 	theory/theory_engine_white \
 	theory/theory_black \
-	theory/theory_uf_white \
+	theory/theory_uf_tim_white \
 	theory/theory_arith_white \
 	expr/expr_public \
         expr/expr_manager_public \
@@ -29,6 +29,7 @@ UNIT_TESTS = \
 	util/assert_white \
 	util/bitvector_black \
 	util/configuration_black \
+	util/congruence_closure_white \
 	util/output_black \
 	util/exception_black \
 	util/integer_black \
@@ -182,13 +183,13 @@ no-cxxtest-available:
 	else \
 		echo; \
 		echo "ERROR:"; \
-        	echo "ERROR: You cannot make dist in this build directory, you do not have CxxTest."; \
-        	echo "ERROR: The tests should be generated for the user and included in the tarball,"; \
+		echo "ERROR: You cannot make dist in this build directory, you do not have CxxTest."; \
+		echo "ERROR: The tests should be generated for the user and included in the tarball,"; \
 		echo "ERROR: otherwise they'll be required to have CxxTest just to test the standard"; \
 		echo "ERROR: distribution built correctly."; \
 		echo "ERROR: If you really want to do this, append the following to your make command."; \
 		echo "ERROR:"; \
-        	echo "ERROR:     I_REALLY_WANT_TO_BUILD_CVC4_DIST_WITHOUT_TESTS=1"; \
+		echo "ERROR:     I_REALLY_WANT_TO_BUILD_CVC4_DIST_WITHOUT_TESTS=1"; \
 		echo "ERROR:"; \
 		echo; \
 		exit 1; \
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index e18aeb975..ea1f40eac 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -104,8 +104,8 @@ public:
     TS_ASSERT_DIFFERS(VarNameAttr::s_id, TestStringAttr2::s_id);
     TS_ASSERT_DIFFERS(TestStringAttr1::s_id, TestStringAttr2::s_id);
 
-    lastId = attr::LastAttributeId<void*, false>::s_id;
-    TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId);
+    //lastId = attr::LastAttributeId<void*, false>::s_id;
+    //TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId);
 
     lastId = attr::LastAttributeId<bool, false>::s_id;
     TS_ASSERT_LESS_THAN(theory::Theory::PreRegisteredAttr::s_id, lastId);
diff --git a/test/unit/theory/shared_term_manager_black.h b/test/unit/theory/shared_term_manager_black.h
index 4393d99cd..def2f7049 100644
--- a/test/unit/theory/shared_term_manager_black.h
+++ b/test/unit/theory/shared_term_manager_black.h
@@ -31,6 +31,7 @@
 #include "context/context.h"
 #include "util/rational.h"
 #include "util/integer.h"
+#include "util/options.h"
 #include "util/Assert.h"
 
 using namespace CVC4;
@@ -50,6 +51,7 @@ class SharedTermManagerBlack : public CxxTest::TestSuite {
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
   TheoryEngine* d_theoryEngine;
+  Options d_options;
 
 public:
 
@@ -59,11 +61,11 @@ public:
     d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
 
-    d_theoryEngine = new TheoryEngine(d_ctxt);
-
+    d_theoryEngine = new TheoryEngine(d_ctxt, &d_options);
   }
 
   void tearDown() {
+    d_theoryEngine->shutdown();
     delete d_theoryEngine;
 
     delete d_scope;
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index ead879336..1ec523148 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -35,6 +35,7 @@
 #include "context/context.h"
 #include "util/rational.h"
 #include "util/integer.h"
+#include "util/options.h"
 #include "util/Assert.h"
 
 using namespace CVC4;
@@ -214,6 +215,7 @@ class TheoryEngineWhite : public CxxTest::TestSuite {
   FakeOutputChannel *d_nullChannel;
   FakeTheory *d_builtin, *d_bool, *d_uf, *d_arith, *d_arrays, *d_bv;
   TheoryEngine* d_theoryEngine;
+  Options d_options;
 
 public:
 
@@ -234,7 +236,7 @@ public:
     d_bv = new FakeTheory(d_ctxt, *d_nullChannel, "BV");
 
     // create the TheoryEngine
-    d_theoryEngine = new TheoryEngine(d_ctxt);
+    d_theoryEngine = new TheoryEngine(d_ctxt, &d_options);
 
     // insert our fake versions into the TheoryEngine's theoryOf table
     d_theoryEngine->d_theoryOfTable.
@@ -254,6 +256,7 @@ public:
   }
 
   void tearDown() {
+    d_theoryEngine->shutdown();
     delete d_theoryEngine;
 
     delete d_bv;
diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_tim_white.h
index f273de30f..aec999293 100644
--- a/test/unit/theory/theory_uf_white.h
+++ b/test/unit/theory/theory_uf_tim_white.h
@@ -11,15 +11,16 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief White box testing of CVC4::theory::uf::TheoryUF.
+ ** \brief White box testing of CVC4::theory::uf::tim::TheoryUFTim.
  **
- ** White box testing of CVC4::theory::uf::TheoryUF.
+ ** White box testing of CVC4::theory::uf::tim::TheoryUFTim.
  **/
 
 #include <cxxtest/TestSuite.h>
 
 #include "theory/theory.h"
 #include "theory/uf/theory_uf.h"
+#include "theory/uf/tim/theory_uf_tim.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"
 #include "context/context.h"
@@ -31,13 +32,14 @@
 using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::uf;
+using namespace CVC4::theory::uf::tim;
 using namespace CVC4::expr;
 using namespace CVC4::context;
 
 using namespace std;
 
 
-class TheoryUFWhite : public CxxTest::TestSuite {
+class TheoryUFTimWhite : public CxxTest::TestSuite {
 
   Context* d_ctxt;
   NodeManager* d_nm;
@@ -46,20 +48,20 @@ class TheoryUFWhite : public CxxTest::TestSuite {
   TestOutputChannel d_outputChannel;
   Theory::Effort d_level;
 
-  TheoryUF* d_euf;
+  TheoryUFTim* d_euf;
 
   TypeNode* d_booleanType;
 
 public:
 
-  TheoryUFWhite() : d_level(Theory::FULL_EFFORT) {}
+  TheoryUFTimWhite() : d_level(Theory::FULL_EFFORT) {}
 
   void setUp() {
     d_ctxt = new Context;
     d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
     d_outputChannel.clear();
-    d_euf = new TheoryUF(0, d_ctxt, d_outputChannel);
+    d_euf = new TheoryUFTim(0, d_ctxt, d_outputChannel);
 
     d_booleanType = new TypeNode(d_nm->booleanType());
   }
diff --git a/test/unit/util/congruence_closure_white.h b/test/unit/util/congruence_closure_white.h
new file mode 100644
index 000000000..273f9cfa5
--- /dev/null
+++ b/test/unit/util/congruence_closure_white.h
@@ -0,0 +1,454 @@
+/*********************                                                        */
+/*! \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  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/cdset.h"
+#include "context/cdmap.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 {
+  CDSet<Node, NodeHashFunction> d_notifications;
+  CDMap<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) {
+    CDMap<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>* d_cc;
+
+  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;
+public:
+
+  void setUp() {
+    d_context = new Context;
+    d_nm = new NodeManager(d_context);
+    d_scope = new NodeManagerScope(d_nm);
+    d_out = new MyOutputChannel(d_context, d_nm);
+    d_cc = new CongruenceClosure<MyOutputChannel>(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);
+  }
+
+  void tearDown() {
+    try {
+      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_cc;
+      delete d_out;
+      delete d_scope;
+      delete d_nm;
+      delete d_context;
+
+    } catch(Exception& e) {
+      Warning() << std::endl << e << std::endl;
+      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(hfaa);
+
+    d_cc->addEquality(a_eq_fb);
+    d_cc->addEquality(fa_eq_b);
+    d_cc->addEquality(h_eq_g);
+
+    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, hba));
+    TS_ASSERT(d_cc->areCongruent(gfafb, gba));
+    TS_ASSERT(d_cc->areCongruent(hba, gba));
+    TS_ASSERT(d_cc->areCongruent(hfaa, hba));
+    TS_ASSERT(d_out->areCongruent(hfaa, gba));// fails due to problem with care lists
+    TS_ASSERT(d_cc->areCongruent(hfaa, 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 << e << "\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);
+  }
+
+};/* class CongruenceClosureWhite */