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.

2 files changed, 20 insertions, 3 deletions

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index dfa94a66d..d3b9d12fb 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -127,3 +127,4 @@ constant TYPE_CONSTANT \
     "expr/type_constant.h" \
     "basic types"
 operator FUNCTION_TYPE 2: "function type"
+operator TUPLE_TYPE 2: "tuple type"
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 354bf02bd..42c9902e5 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -44,7 +44,7 @@ class EqualityTypeRule {
         std::stringstream ss;
         ss << "Types do not match in equation ";
         ss << "[" << lhsType << "<>" << rhsType << "]";
-        
+
         throw TypeCheckingExceptionPrivate(n, ss.str());
       }
 
@@ -54,7 +54,8 @@ class EqualityTypeRule {
     }
     return booleanType;
   }
-};
+};/* class EqualityTypeRule */
+
 
 class DistinctTypeRule {
 public:
@@ -71,7 +72,22 @@ public:
     }
     return nodeManager->booleanType();
   }
-};
+};/* class DistinctTypeRule */
+
+
+class TupleTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    std::vector<TypeNode> types;
+    for(TNode::iterator child_it = n.begin(), child_it_end = n.end();
+        child_it != child_it_end;
+        ++child_it) {
+      types.push_back((*child_it).getType(check));
+    }
+    return nodeManager->mkTupleType(types);
+  }
+};/* class TupleTypeRule */
+
 
 }/* CVC4::theory::builtin namespace */
 }/* CVC4::theory namespace */