Tuples and records merge. Resolves bug 270.

Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together.

(this commit was certified error- and warning-free by the test-and-commit script.)

10 files changed, 657 insertions, 86 deletions

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index bcf787f6b..e3bc506e2 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -296,7 +296,6 @@ operator DISTINCT 2: "disequality"
 variable VARIABLE "variable"
 variable BOUND_VARIABLE "bound variable"
 variable SKOLEM "skolem var"
-operator TUPLE 1: "a tuple"
 operator SEXPR 0: "a symbolic expression"
 
 operator LAMBDA 2 "lambda"
@@ -313,14 +312,6 @@ cardinality FUNCTION_TYPE \
     "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
     "theory/builtin/theory_builtin_type_rules.h"
 well-founded FUNCTION_TYPE false
-operator TUPLE_TYPE 1: "tuple type"
-cardinality TUPLE_TYPE \
-    "::CVC4::theory::builtin::TupleProperties::computeCardinality(%TYPE%)" \
-    "theory/builtin/theory_builtin_type_rules.h"
-well-founded TUPLE_TYPE \
-    "::CVC4::theory::builtin::TupleProperties::isWellFounded(%TYPE%)" \
-    "::CVC4::theory::builtin::TupleProperties::mkGroundTerm(%TYPE%)" \
-    "theory/builtin/theory_builtin_type_rules.h"
 operator SEXPR_TYPE 0: "symbolic expression type"
 cardinality SEXPR_TYPE \
     "::CVC4::theory::builtin::SExprProperties::computeCardinality(%TYPE%)" \
@@ -350,7 +341,6 @@ typerule CONST_STRING ::CVC4::theory::builtin::StringConstantTypeRule
 typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule
 typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
 typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
-typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule
 typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule
 typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
 construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 720e55be3..4aa7c0982 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -115,19 +115,6 @@ public:
   }
 };/* 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 */
-
 class SExprTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
@@ -269,58 +256,6 @@ public:
   }
 };/* class FuctionProperties */
 
-class TupleProperties {
-public:
-  inline static Cardinality computeCardinality(TypeNode type) {
-    // Don't assert this; allow other theories to use this cardinality
-    // computation.
-    //
-    // Assert(type.getKind() == kind::TUPLE_TYPE);
-
-    Cardinality card(1);
-    for(TypeNode::iterator i = type.begin(),
-          i_end = type.end();
-        i != i_end;
-        ++i) {
-      card *= (*i).getCardinality();
-    }
-
-    return card;
-  }
-
-  inline static bool isWellFounded(TypeNode type) {
-    // Don't assert this; allow other theories to use this
-    // wellfoundedness computation.
-    //
-    // Assert(type.getKind() == kind::TUPLE_TYPE);
-
-    for(TypeNode::iterator i = type.begin(),
-          i_end = type.end();
-        i != i_end;
-        ++i) {
-      if(! (*i).isWellFounded()) {
-        return false;
-      }
-    }
-
-    return true;
-  }
-
-  inline static Node mkGroundTerm(TypeNode type) {
-    Assert(type.getKind() == kind::TUPLE_TYPE);
-
-    std::vector<Node> children;
-    for(TypeNode::iterator i = type.begin(),
-          i_end = type.end();
-        i != i_end;
-        ++i) {
-      children.push_back((*i).mkGroundTerm());
-    }
-
-    return NodeManager::currentNM()->mkNode(kind::TUPLE, children);
-  }
-};/* class TupleProperties */
-
 class SExprProperties {
 public:
   inline static Cardinality computeCardinality(TypeNode type) {
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 42b999561..f9fb00a75 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -54,6 +54,43 @@ public:
         }
       }
     }
+    if(in.getKind() == kind::TUPLE_SELECT && in[0].getKind() == kind::APPLY_CONSTRUCTOR) {
+      return RewriteResponse(REWRITE_DONE, in[0][in.getOperator().getConst<TupleSelect>().getIndex()]);
+    }
+    if(in.getKind() == kind::RECORD_SELECT && in[0].getKind() == kind::APPLY_CONSTRUCTOR) {
+      const Record& rec = in[0].getType().getAttribute(expr::DatatypeRecordAttr()).getConst<Record>();
+      return RewriteResponse(REWRITE_DONE, in[0][rec.getIndex(in.getOperator().getConst<RecordSelect>().getField())]);
+    }
+    if(in.getKind() == kind::APPLY_SELECTOR &&
+       (in[0].getKind() == kind::TUPLE || in[0].getKind() == kind::RECORD)) {
+      // These strange (half-tuple-converted) terms can be created by
+      // the system if you have something like "foo.1" for a tuple
+      // term foo.  The select is rewritten to "select_1(foo)".  If
+      // foo gets a value in the model from the TypeEnumerator, you
+      // then have a select of a tuple, and we should flatten that
+      // here.  Ditto for records, below.
+      Expr selectorExpr = in.getOperator().toExpr();
+      const Datatype& dt CVC4_UNUSED = Datatype::datatypeOf(selectorExpr);
+      TypeNode dtt CVC4_UNUSED = TypeNode::fromType(dt.getDatatypeType());
+      size_t selectorIndex = Datatype::indexOf(selectorExpr);
+      Debug("tuprec") << "looking at " << in << ", got selector index " << selectorIndex << std::endl;
+#ifdef CVC4_ASSERTIONS
+      // sanity checks: tuple- and record-converted datatypes should have one constructor
+      Assert(NodeManager::currentNM()->getDatatypeForTupleRecord(in[0].getType()) == dtt);
+      if(in[0].getKind() == kind::TUPLE) {
+        Assert(dtt.hasAttribute(expr::DatatypeTupleAttr()));
+        Assert(dtt.getAttribute(expr::DatatypeTupleAttr()) == in[0].getType());
+      } else {
+        Assert(dtt.hasAttribute(expr::DatatypeRecordAttr()));
+        Assert(dtt.getAttribute(expr::DatatypeRecordAttr()) == in[0].getType());
+      }
+      Assert(dt.getNumConstructors() == 1);
+      Assert(dt[0].getNumArgs() > selectorIndex);
+      Assert(dt[0][selectorIndex].getSelector() == selectorExpr);
+#endif /* CVC4_ASSERTIONS */
+      Debug("tuprec") << "==> returning " << in[0][selectorIndex] << std::endl;
+      return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]);
+    }
     if(in.getKind() == kind::APPLY_SELECTOR &&
        in[0].getKind() == kind::APPLY_CONSTRUCTOR) {
       // Have to be careful not to rewrite well-typed expressions
@@ -90,6 +127,45 @@ public:
         }
       }
     }
+    if(in.getKind() == kind::TUPLE_SELECT &&
+       in[0].getKind() == kind::TUPLE) {
+      return RewriteResponse(REWRITE_DONE, in[0][in.getOperator().getConst<TupleSelect>().getIndex()]);
+    }
+    if(in.getKind() == kind::TUPLE_UPDATE &&
+       in[0].getKind() == kind::TUPLE) {
+      size_t ix = in.getOperator().getConst<TupleUpdate>().getIndex();
+      NodeBuilder<> b(kind::TUPLE);
+      for(TNode::const_iterator i = in[0].begin(); i != in[0].end(); ++i, --ix) {
+        if(ix == 0) {
+          b << in[1];
+        } else {
+          b << *i;
+        }
+      }
+      Node n = b;
+      Assert(n.getType().isSubtypeOf(in.getType()));
+      return RewriteResponse(REWRITE_DONE, n);
+    }
+    if(in.getKind() == kind::RECORD_SELECT &&
+       in[0].getKind() == kind::RECORD) {
+      return RewriteResponse(REWRITE_DONE, in[0][in[0].getOperator().getConst<Record>().getIndex(in.getOperator().getConst<RecordSelect>().getField())]);
+    }
+    if(in.getKind() == kind::RECORD_UPDATE &&
+       in[0].getKind() == kind::RECORD) {
+      size_t ix = in[0].getOperator().getConst<Record>().getIndex(in.getConst<RecordUpdate>().getField());
+      NodeBuilder<> b(kind::RECORD);
+      b << in[0].getOperator();
+      for(TNode::const_iterator i = in[0].begin(); i != in[0].end(); ++i, --ix) {
+        if(ix == 0) {
+          b << in[1];
+        } else {
+          b << *i;
+        }
+      }
+      Node n = b;
+      Assert(n.getType().isSubtypeOf(in.getType()));
+      return RewriteResponse(REWRITE_DONE, n);
+    }
 
     if(in.getKind() == kind::EQUAL && in[0] == in[1]) {
       return RewriteResponse(REWRITE_DONE,
@@ -113,7 +189,9 @@ public:
   static inline void shutdown() {}
 
   static bool checkClash( Node n1, Node n2 ) {
-    if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) {
+    if( (n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR) ||
+        (n1.getKind() == kind::TUPLE && n2.getKind() == kind::TUPLE) ||
+        (n1.getKind() == kind::RECORD && n2.getKind() == kind::RECORD) ) {
       if( n1.getOperator() != n2.getOperator() ) {
         return true;
       } else {
@@ -137,7 +215,8 @@ public:
   /** is this term a datatype */
   static bool isTermDatatype( Node n ){
     TypeNode tn = n.getType();
-    return tn.isDatatype() || tn.isParametricDatatype();
+    return tn.isDatatype() || tn.isParametricDatatype() ||
+           tn.isTuple() || tn.isRecord();
   }
 
 };/* class DatatypesRewriter */
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index eac3d6eac..d1fbf82bc 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -84,4 +84,72 @@ typerule APPLY_TYPE_ASCRIPTION ::CVC4::theory::datatypes::DatatypeAscriptionType
 # constructor applications are constant if they are applied only to constants
 construle APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule
 
+operator TUPLE_TYPE 1: "tuple type"
+cardinality TUPLE_TYPE \
+    "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \
+    "theory/datatypes/theory_datatypes_type_rules.h"
+well-founded TUPLE_TYPE \
+    "::CVC4::theory::datatypes::TupleProperties::isWellFounded(%TYPE%)" \
+    "::CVC4::theory::datatypes::TupleProperties::mkGroundTerm(%TYPE%)" \
+    "theory/datatypes/theory_datatypes_type_rules.h"
+enumerator TUPLE_TYPE \
+    "::CVC4::theory::datatypes::TupleEnumerator" \
+    "theory/datatypes/type_enumerator.h"
+
+operator TUPLE 1: "a tuple"
+typerule TUPLE ::CVC4::theory::datatypes::TupleTypeRule
+construle TUPLE ::CVC4::theory::datatypes::TupleProperties
+
+constant TUPLE_SELECT_OP \
+        ::CVC4::TupleSelect \
+        ::CVC4::TupleSelectHashFunction \
+        "util/tuple.h" \
+        "operator for a tuple select"
+parameterized TUPLE_SELECT TUPLE_SELECT_OP 1 "tuple select"
+typerule TUPLE_SELECT ::CVC4::theory::datatypes::TupleSelectTypeRule
+
+constant TUPLE_UPDATE_OP \
+        ::CVC4::TupleUpdate \
+        ::CVC4::TupleUpdateHashFunction \
+        "util/tuple.h" \
+        "operator for a tuple update"
+parameterized TUPLE_UPDATE TUPLE_UPDATE_OP 2 "tuple update"
+typerule TUPLE_UPDATE ::CVC4::theory::datatypes::TupleUpdateTypeRule
+
+constant RECORD_TYPE \
+    ::CVC4::Record \
+    "::CVC4::RecordHashFunction" \
+    "util/record.h" \
+    "record type"
+cardinality RECORD_TYPE \
+    "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \
+    "theory/datatypes/theory_datatypes_type_rules.h"
+well-founded RECORD_TYPE \
+    "::CVC4::theory::datatypes::TupleProperties::isWellFounded(%TYPE%)" \
+    "::CVC4::theory::datatypes::RecordProperties::mkGroundTerm(%TYPE%)" \
+    "theory/datatypes/theory_datatypes_type_rules.h"
+enumerator RECORD_TYPE \
+    "::CVC4::theory::datatypes::RecordEnumerator" \
+    "theory/datatypes/type_enumerator.h"
+
+parameterized RECORD RECORD_TYPE 1: "a record"
+typerule RECORD ::CVC4::theory::datatypes::RecordTypeRule
+construle RECORD ::CVC4::theory::datatypes::RecordProperties
+
+constant RECORD_SELECT_OP \
+        ::CVC4::RecordSelect \
+        ::CVC4::RecordSelectHashFunction \
+        "util/record.h" \
+        "operator for a record select"
+parameterized RECORD_SELECT RECORD_SELECT_OP 1 "record select"
+typerule RECORD_SELECT ::CVC4::theory::datatypes::RecordSelectTypeRule
+
+constant RECORD_UPDATE_OP \
+        ::CVC4::RecordUpdate \
+        ::CVC4::RecordUpdateHashFunction \
+        "util/record.h" \
+        "operator for a record update"
+parameterized RECORD_UPDATE RECORD_UPDATE_OP 2 "record update"
+typerule RECORD_UPDATE ::CVC4::theory::datatypes::RecordUpdateTypeRule
+
 endtheory
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 8ec45efb9..6273eb2c2 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -22,6 +22,7 @@
 #include "util/cvc4_assert.h"
 #include "theory/datatypes/theory_datatypes_instantiator.h"
 #include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/datatypes/theory_datatypes_type_rules.h"
 #include "theory/model.h"
 #include "smt/options.h"
 
@@ -94,6 +95,19 @@ void TheoryDatatypes::check(Effort e) {
     Assertion assertion = get();
     TNode fact = assertion.assertion;
     Trace("datatypes-assert") << "Assert " << fact << std::endl;
+
+    TNode atom CVC4_UNUSED = fact.getKind() == kind::NOT ? fact[0] : fact;
+
+    // extra debug check to make sure that the rewriter did its job correctly
+    Assert( atom.getKind() != kind::EQUAL ||
+            ( atom[0].getKind() != kind::TUPLE && atom[1].getKind() != kind::TUPLE &&
+              atom[0].getKind() != kind::RECORD && atom[1].getKind() != kind::RECORD &&
+              atom[0].getKind() != kind::TUPLE_UPDATE && atom[1].getKind() != kind::TUPLE_UPDATE &&
+              atom[0].getKind() != kind::RECORD_UPDATE && atom[1].getKind() != kind::RECORD_UPDATE &&
+              atom[0].getKind() != kind::TUPLE_SELECT && atom[1].getKind() != kind::TUPLE_SELECT &&
+              atom[0].getKind() != kind::RECORD_SELECT && atom[1].getKind() != kind::RECORD_SELECT ),
+            "tuple/record escaped into datatypes decision procedure; should have been rewritten away" );
+
     //assert the fact
     assertFact( fact, fact );
     flushPendingFacts();
@@ -275,6 +289,90 @@ void TheoryDatatypes::presolve() {
   Debug("datatypes") << "TheoryDatatypes::presolve()" << endl;
 }
 
+Node TheoryDatatypes::ppRewrite(TNode in) {
+  Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl;
+
+  if(in.getKind() == kind::TUPLE_SELECT) {
+    TypeNode t = in[0].getType();
+    if(t.hasAttribute(expr::DatatypeTupleAttr())) {
+      t = t.getAttribute(expr::DatatypeTupleAttr());
+    }
+    TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
+    const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
+    return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<TupleSelect>().getIndex()].getSelector()), in[0]);
+  } else if(in.getKind() == kind::RECORD_SELECT) {
+    TypeNode t = in[0].getType();
+    if(t.hasAttribute(expr::DatatypeRecordAttr())) {
+      t = t.getAttribute(expr::DatatypeRecordAttr());
+    }
+    TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
+    const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
+    return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]);
+  }
+
+  // we only care about tuples and records here
+  if(in.getKind() != kind::TUPLE && in.getKind() != kind::TUPLE_UPDATE &&
+     in.getKind() != kind::RECORD && in.getKind() != kind::RECORD_UPDATE) {
+    // nothing to do
+    return in;
+  }
+
+  TypeNode t = in.getType();
+
+  if(t.hasAttribute(expr::DatatypeTupleAttr())) {
+    t = t.getAttribute(expr::DatatypeTupleAttr());
+  } else if(t.hasAttribute(expr::DatatypeRecordAttr())) {
+    t = t.getAttribute(expr::DatatypeRecordAttr());
+  }
+
+  // if the type doesn't have an associated datatype, then make one for it
+  TypeNode dtt = (t.isTuple() || t.isRecord()) ? NodeManager::currentNM()->getDatatypeForTupleRecord(t) : t;
+
+  const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
+
+  // now rewrite the expression
+  Node n;
+  if(in.getKind() == kind::TUPLE || in.getKind() == kind::RECORD) {
+    NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
+    b << Node::fromExpr(dt[0].getConstructor());
+    b.append(in.begin(), in.end());
+    n = b;
+  } else if(in.getKind() == kind::TUPLE_UPDATE || in.getKind() == kind::RECORD_UPDATE) {
+    NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
+    b << Node::fromExpr(dt[0].getConstructor());
+    size_t size, updateIndex;
+    if(in.getKind() == kind::TUPLE_UPDATE) {
+      size = t.getNumChildren();
+      updateIndex = in.getOperator().getConst<TupleUpdate>().getIndex();
+    } else { // kind::RECORD_UPDATE
+      const Record& record = t.getConst<Record>();
+      size = record.getNumFields();
+      updateIndex = record.getIndex(in.getOperator().getConst<RecordUpdate>().getField());
+    }
+    Debug("tuprec") << "expr is " << in << std::endl;
+    Debug("tuprec") << "updateIndex is " << updateIndex << std::endl;
+    Debug("tuprec") << "t is " << t << std::endl;
+    Debug("tuprec") << "t has arity " << size << std::endl;
+    for(size_t i = 0; i < size; ++i) {
+      if(i == updateIndex) {
+        b << in[1];
+        Debug("tuprec") << "arg " << i << " gets updated to " << in[1] << std::endl;
+      } else {
+        b << NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][i].getSelector()), in[0]);
+        Debug("tuprec") << "arg " << i << " copies " << b[b.getNumChildren() - 1] << std::endl;
+      }
+    }
+    Debug("tuprec") << "builder says " << b << std::endl;
+    n = b;
+  }
+
+  Assert(!n.isNull());
+
+  Debug("tuprec") << "REWROTE " << in << " to " << n << std::endl;
+
+  return n;
+}
+
 void TheoryDatatypes::addSharedTerm(TNode t) {
   Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): "
                      << t << endl;
@@ -719,7 +817,7 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index
     Node n_ic = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
     collectTerms( n_ic );
     //add type ascription for ambiguous constructor types
-    if( n_ic.getType()!=n.getType() ){
+    if(!n_ic.getType().isComparableTo(n.getType())) {
       Assert( dt.isParametric() );
       Debug("datatypes-parametric") << "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to " << n.getType() << std::endl;
       Debug("datatypes-parametric") << "Constructor is " << dt[index] << std::endl;
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 5cda9eeae..4380eca58 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -52,6 +52,7 @@ private:
   /** inferences */
   NodeList d_infer;
   NodeList d_infer_exp;
+
 private:
   //notification class for equality engine
   class NotifyClass : public eq::EqualityEngineNotify {
@@ -202,6 +203,7 @@ public:
 
   void check(Effort e);
   void preRegisterTerm(TNode n);
+  Node ppRewrite(TNode n);
   void presolve();
   void addSharedTerm(TNode t);
   EqualityStatus getEqualityStatus(TNode a, TNode b);
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index eb50def01..ade9ffc26 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -20,6 +20,7 @@
 #define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
 
 #include "util/matcher.h"
+#include "expr/attribute.h"
 
 namespace CVC4 {
 
@@ -70,7 +71,7 @@ struct DatatypeConstructorTypeRule {
           TypeNode childType = (*child_it).getType(check);
           Debug("typecheck-idt") << "typecheck cons arg: " << childType << " " << (*tchild_it) << std::endl;
           TypeNode argumentType = *tchild_it;
-          if(!childType.isSubtypeOf(argumentType)) {
+          if(!childType.isComparableTo(argumentType)) {
             std::stringstream ss;
             ss << "bad type for constructor argument:\nexpected: " << argumentType << "\ngot     : " << childType;
             throw TypeCheckingExceptionPrivate(n, ss.str());
@@ -127,7 +128,7 @@ struct DatatypeSelectorTypeRule {
         Debug("typecheck-idt") << "typecheck sel: " << n << std::endl;
         Debug("typecheck-idt") << "sel type: " << selType << std::endl;
         TypeNode childType = n[0].getType(check);
-        if(selType[0] != childType) {
+        if(!selType[0].isComparableTo(childType)) {
           Debug("typecheck-idt") << "ERROR: " << selType[0].getKind() << " " << childType.getKind() << std::endl;
           throw TypeCheckingExceptionPrivate(n, "bad type for selector argument");
         }
@@ -150,16 +151,16 @@ struct DatatypeTesterTypeRule {
       Type t = testType[0].toType();
       Assert( t.isDatatype() );
       DatatypeType dt = DatatypeType(t);
-      if( dt.isParametric() ){
+      if(dt.isParametric()) {
         Debug("typecheck-idt") << "typecheck parameterized tester: " << n << std::endl;
         Matcher m( dt );
         if( !m.doMatching( testType[0], childType ) ){
           throw TypeCheckingExceptionPrivate(n, "matching failed for tester argument of parameterized datatype");
         }
-      }else{
+      } else {
         Debug("typecheck-idt") << "typecheck test: " << n << std::endl;
         Debug("typecheck-idt") << "test type: " << testType << std::endl;
-        if(testType[0] != childType) {
+        if(!testType[0].isComparableTo(childType)) {
           throw TypeCheckingExceptionPrivate(n, "bad type for tester argument");
         }
       }
@@ -265,6 +266,231 @@ struct ConstructorProperties {
   }
 };/* struct ConstructorProperties */
 
+struct TupleTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    Assert(n.getKind() == kind::TUPLE);
+    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);
+  }
+};/* struct TupleTypeRule */
+
+struct TupleSelectTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    Assert(n.getKind() == kind::TUPLE_SELECT);
+    const TupleSelect& ts = n.getOperator().getConst<TupleSelect>();
+    TypeNode tupleType = n[0].getType(check);
+    if(!tupleType.isTuple()) {
+      if(!tupleType.hasAttribute(expr::DatatypeRecordAttr())) {
+        throw TypeCheckingExceptionPrivate(n, "Tuple-select expression formed over non-tuple");
+      }
+      tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr());
+    }
+    if(ts.getIndex() >= tupleType.getNumChildren()) {
+      std::stringstream ss;
+      ss << "Tuple-select expression index `" << ts.getIndex()
+         << "' is not a valid index; tuple type only has "
+         << tupleType.getNumChildren() << " fields";
+      throw TypeCheckingExceptionPrivate(n, ss.str().c_str());
+    }
+    return tupleType[ts.getIndex()];
+  }
+};/* struct TupleSelectTypeRule */
+
+struct TupleUpdateTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    Assert(n.getKind() == kind::TUPLE_UPDATE);
+    const TupleUpdate& tu = n.getOperator().getConst<TupleUpdate>();
+    TypeNode tupleType = n[0].getType(check);
+    TypeNode newValue = n[1].getType(check);
+    if(check) {
+      if(!tupleType.isTuple()) {
+        if(!tupleType.hasAttribute(expr::DatatypeRecordAttr())) {
+          throw TypeCheckingExceptionPrivate(n, "Tuple-update expression formed over non-tuple");
+        }
+        tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr());
+      }
+      if(tu.getIndex() >= tupleType.getNumChildren()) {
+        std::stringstream ss;
+        ss << "Tuple-update expression index `" << tu.getIndex()
+           << "' is not a valid index; tuple type only has "
+           << tupleType.getNumChildren() << " fields";
+        throw TypeCheckingExceptionPrivate(n, ss.str().c_str());
+      }
+    }
+    return tupleType;
+  }
+};/* struct TupleUpdateTypeRule */
+
+struct TupleProperties {
+  inline static Cardinality computeCardinality(TypeNode type) {
+    // Don't assert this; allow other theories to use this cardinality
+    // computation.
+    //
+    // Assert(type.getKind() == kind::TUPLE_TYPE);
+
+    Cardinality card(1);
+    for(TypeNode::iterator i = type.begin(),
+          i_end = type.end();
+        i != i_end;
+        ++i) {
+      card *= (*i).getCardinality();
+    }
+
+    return card;
+  }
+
+  inline static bool isWellFounded(TypeNode type) {
+    // Don't assert this; allow other theories to use this
+    // wellfoundedness computation.
+    //
+    // Assert(type.getKind() == kind::TUPLE_TYPE);
+
+    for(TypeNode::iterator i = type.begin(),
+          i_end = type.end();
+        i != i_end;
+        ++i) {
+      if(! (*i).isWellFounded()) {
+        return false;
+      }
+    }
+
+    return true;
+  }
+
+  inline static Node mkGroundTerm(TypeNode type) {
+    Assert(type.getKind() == kind::TUPLE_TYPE);
+
+    std::vector<Node> children;
+    for(TypeNode::iterator i = type.begin(),
+          i_end = type.end();
+        i != i_end;
+        ++i) {
+      children.push_back((*i).mkGroundTerm());
+    }
+
+    return NodeManager::currentNM()->mkNode(kind::TUPLE, children);
+  }
+
+  inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
+    Assert(n.getKind() == kind::TUPLE);
+    NodeManagerScope nms(nodeManager);
+
+    for(TNode::iterator i = n.begin(),
+          i_end = n.end();
+        i != i_end;
+        ++i) {
+      if(! (*i).isConst()) {
+        return false;
+      }
+    }
+
+    return true;
+  }
+};/* struct TupleProperties */
+
+struct RecordTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    Assert(n.getKind() == kind::RECORD);
+    NodeManagerScope nms(nodeManager);
+    const Record& rec = n.getOperator().getConst<Record>();
+    if(check) {
+      Record::iterator i = rec.begin();
+      for(TNode::iterator child_it = n.begin(), child_it_end = n.end();
+          child_it != child_it_end;
+          ++child_it, ++i) {
+        if(i == rec.end()) {
+          throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal");
+        }
+        if(!(*child_it).getType(check).isComparableTo(TypeNode::fromType((*i).second))) {
+          throw TypeCheckingExceptionPrivate(n, "record description types differ from record literal types");
+        }
+      }
+      if(i != rec.end()) {
+        throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal");
+      }
+    }
+    return nodeManager->mkRecordType(rec);
+  }
+};/* struct RecordTypeRule */
+
+struct RecordSelectTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    Assert(n.getKind() == kind::RECORD_SELECT);
+    NodeManagerScope nms(nodeManager);
+    const RecordSelect& rs = n.getOperator().getConst<RecordSelect>();
+    TypeNode recordType = n[0].getType(check);
+    if(!recordType.isRecord()) {
+      if(!recordType.hasAttribute(expr::DatatypeRecordAttr())) {
+        throw TypeCheckingExceptionPrivate(n, "Record-select expression formed over non-record");
+      }
+      recordType = recordType.getAttribute(expr::DatatypeRecordAttr());
+    }
+    const Record& rec = recordType.getRecord();
+    Record::const_iterator field = rec.find(rs.getField());
+    if(field == rec.end()) {
+      std::stringstream ss;
+      ss << "Record-select field `" << rs.getField()
+         << "' is not a valid field name for the record type";
+      throw TypeCheckingExceptionPrivate(n, ss.str().c_str());
+    }
+    return TypeNode::fromType((*field).second);
+  }
+};/* struct RecordSelectTypeRule */
+
+struct RecordUpdateTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    Assert(n.getKind() == kind::RECORD_UPDATE);
+    NodeManagerScope nms(nodeManager);
+    const RecordUpdate& ru = n.getOperator().getConst<RecordUpdate>();
+    TypeNode recordType = n[0].getType(check);
+    TypeNode newValue = n[1].getType(check);
+    if(check) {
+      if(!recordType.isRecord()) {
+        if(!recordType.hasAttribute(expr::DatatypeRecordAttr())) {
+          throw TypeCheckingExceptionPrivate(n, "Record-update expression formed over non-record");
+        }
+        recordType = recordType.getAttribute(expr::DatatypeRecordAttr());
+      }
+      const Record& rec = recordType.getRecord();
+      Record::const_iterator field = rec.find(ru.getField());
+      if(field == rec.end()) {
+        std::stringstream ss;
+        ss << "Record-update field `" << ru.getField()
+           << "' is not a valid field name for the record type";
+        throw TypeCheckingExceptionPrivate(n, ss.str().c_str());
+      }
+    }
+    return recordType;
+  }
+};/* struct RecordUpdateTypeRule */
+
+struct RecordProperties {
+  inline static Node mkGroundTerm(TypeNode type) {
+    Unimplemented();
+  }
+
+  inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
+    Assert(n.getKind() == kind::RECORD);
+    NodeManagerScope nms(nodeManager);
+
+    for(TNode::iterator i = n.begin(),
+          i_end = n.end();
+        i != i_end;
+        ++i) {
+      if(! (*i).isConst()) {
+        return false;
+      }
+    }
+
+    return true;
+  }
+};/* struct RecordProperties */
+
 }/* CVC4::theory::datatypes namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 0f365bd71..ea68e8957 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -147,6 +147,146 @@ public:
 
 };/* DatatypesEnumerator */
 
+class TupleEnumerator : public TypeEnumeratorBase<TupleEnumerator> {
+  TypeEnumerator** d_enumerators;
+
+  void deleteEnumerators() throw() {
+    if(d_enumerators != NULL) {
+      for(size_t i = 0; i < getType().getNumChildren(); ++i) {
+        delete d_enumerators[i];
+      }
+      delete [] d_enumerators;
+      d_enumerators = NULL;
+    }
+  }
+
+public:
+
+  TupleEnumerator(TypeNode type) throw() :
+    TypeEnumeratorBase<TupleEnumerator>(type) {
+    Assert(type.isTuple());
+    d_enumerators = new TypeEnumerator*[type.getNumChildren()];
+    for(size_t i = 0; i < type.getNumChildren(); ++i) {
+      d_enumerators[i] = new TypeEnumerator(type[i]);
+    }
+  }
+
+  ~TupleEnumerator() throw() {
+    deleteEnumerators();
+  }
+
+  Node operator*() throw(NoMoreValuesException) {
+    if(isFinished()) {
+      throw NoMoreValuesException(getType());
+    }
+
+    NodeBuilder<> nb(kind::TUPLE);
+    for(size_t i = 0; i < getType().getNumChildren(); ++i) {
+      nb << **d_enumerators[i];
+    }
+    return Node(nb);
+  }
+
+  TupleEnumerator& operator++() throw() {
+    if(isFinished()) {
+      return *this;
+    }
+
+    size_t i;
+    for(i = 0; i < getType().getNumChildren(); ++i) {
+      if(d_enumerators[i]->isFinished()) {
+        *d_enumerators[i] = TypeEnumerator(getType()[i]);
+      } else {
+        ++*d_enumerators[i];
+        return *this;
+      }
+    }
+
+    deleteEnumerators();
+
+    return *this;
+  }
+
+  bool isFinished() throw() {
+    return d_enumerators == NULL;
+  }
+
+};/* TupleEnumerator */
+
+class RecordEnumerator : public TypeEnumeratorBase<RecordEnumerator> {
+  TypeEnumerator** d_enumerators;
+
+  void deleteEnumerators() throw() {
+    if(d_enumerators != NULL) {
+      for(size_t i = 0; i < getType().getNumChildren(); ++i) {
+        delete d_enumerators[i];
+      }
+      delete [] d_enumerators;
+      d_enumerators = NULL;
+    }
+  }
+
+public:
+
+  RecordEnumerator(TypeNode type) throw() :
+    TypeEnumeratorBase<RecordEnumerator>(type) {
+    Assert(type.isRecord());
+    const Record& rec = getType().getConst<Record>();
+    Debug("te") << "creating record enumerator for " << type << std::endl;
+    d_enumerators = new TypeEnumerator*[rec.getNumFields()];
+    for(size_t i = 0; i < rec.getNumFields(); ++i) {
+      Debug("te") << " - sub-enumerator for " << rec[i].second << std::endl;
+      d_enumerators[i] = new TypeEnumerator(TypeNode::fromType(rec[i].second));
+    }
+  }
+
+  ~RecordEnumerator() throw() {
+    deleteEnumerators();
+  }
+
+  Node operator*() throw(NoMoreValuesException) {
+    if(isFinished()) {
+      throw NoMoreValuesException(getType());
+    }
+
+    NodeBuilder<> nb(kind::RECORD);
+    Debug("te") << "record enumerator: creating record of type " << getType() << std::endl;
+    nb << getType();
+    const Record& rec = getType().getConst<Record>();
+    for(size_t i = 0; i < rec.getNumFields(); ++i) {
+      Debug("te") << " - " << i << " " << std::flush << "=> " << **d_enumerators[i] << std::endl;
+      nb << **d_enumerators[i];
+    }
+    return Node(nb);
+  }
+
+  RecordEnumerator& operator++() throw() {
+    if(isFinished()) {
+      return *this;
+    }
+
+    size_t i;
+    const Record& rec = getType().getConst<Record>();
+    for(i = 0; i < rec.getNumFields(); ++i) {
+      if(d_enumerators[i]->isFinished()) {
+        *d_enumerators[i] = TypeEnumerator(TypeNode::fromType(rec[i].second));
+      } else {
+        ++*d_enumerators[i];
+        return *this;
+      }
+    }
+
+    deleteEnumerators();
+
+    return *this;
+  }
+
+  bool isFinished() throw() {
+    return d_enumerators == NULL;
+  }
+
+};/* RecordEnumerator */
+
 }/* CVC4::theory::datatypes namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 8dacf86e9..66f0c8824 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -17,6 +17,7 @@
 #include "theory/theory_engine.h"
 #include "theory/type_enumerator.h"
 #include "smt/options.h"
+#include "smt/smt_engine.h"
 #include "theory/uf/theory_uf_model.h"
 
 using namespace std;
@@ -56,7 +57,7 @@ Node TheoryModel::getValue( TNode n ) const{
 Expr TheoryModel::getValue( Expr expr ) const{
   Node n = Node::fromExpr( expr );
   Node ret = getValue( n );
-  return ret.toExpr();
+  return d_smt.postprocess(ret).toExpr();
 }
 
 /** get cardinality for sort */
diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h
index 9add67441..42cb998be 100644
--- a/src/theory/type_enumerator.h
+++ b/src/theory/type_enumerator.h
@@ -97,8 +97,40 @@ public:
 
   ~TypeEnumerator() { delete d_te; }
 
-  bool isFinished() throw() { return d_te->isFinished(); }
-  Node operator*() throw(NoMoreValuesException) { return **d_te; }
+  bool isFinished() throw() {
+#ifdef CVC4_ASSERTIONS
+    if(d_te->isFinished()) {
+      try {
+        **d_te;
+        Assert(false, "expected an NoMoreValuesException to be thrown");
+      } catch(NoMoreValuesException&) {
+        // ignore the exception, we're just asserting that it would be thrown
+      }
+    } else {
+      try {
+        **d_te;
+      } catch(NoMoreValuesException&) {
+        Assert(false, "didn't expect a NoMoreValuesException to be thrown");
+      }
+    }
+#endif /* CVC4_ASSERTIONS */
+    return d_te->isFinished();
+  }
+  Node operator*() throw(NoMoreValuesException) {
+#ifdef CVC4_ASSERTIONS
+    try {
+      Node n = **d_te;
+      Assert(n.isConst());
+      Assert(! isFinished());
+      return n;
+    } catch(NoMoreValuesException&) {
+      Assert(isFinished());
+      throw;
+    }
+#else /* CVC4_ASSERTIONS */
+    return **d_te;
+#endif /* CVC4_ASSERTIONS */
+  }
   TypeEnumerator& operator++() throw() { ++*d_te; return *this; }
   TypeEnumerator operator++(int) throw() { TypeEnumerator te = *this; ++*d_te; return te; }