Eliminate most of the internal representation infrastructure for tuples and records, replace with datatypes throughout, update cvc printer for tuples/records. Minor changes to API for records and tuples.

7 files changed, 59 insertions, 508 deletions

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 1e7e714cf..0c00ed8df 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -100,43 +100,6 @@ 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_TOTAL &&
-       (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_TOTAL && in[0].getKind() == kind::APPLY_CONSTRUCTOR) {
       // Have to be careful not to rewrite well-typed expressions
       // where the selector doesn't match the constructor,
@@ -236,45 +199,6 @@ public:
         return RewriteResponse(REWRITE_AGAIN_FULL, res );
       }
     }
-    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.getOperator().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,
@@ -306,10 +230,7 @@ public:
 
   static bool checkClash( Node n1, Node n2, std::vector< Node >& rew ) {
     Trace("datatypes-rewrite-debug") << "Check clash : " << n1 << " " << n2 << std::endl;
-    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) ) {
-      //n1.getKind()==kind::APPLY_CONSTRUCTOR
+    if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) {
       if( n1.getOperator() != n2.getOperator() ) {
         Trace("datatypes-rewrite-debug") << "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator() << " " << n2.getOperator() << std::endl;
         return true;
@@ -459,12 +380,10 @@ public:
   /** is this term a datatype */
   static bool isTermDatatype( TNode n ){
     TypeNode tn = n.getType();
-    return tn.isDatatype() || tn.isParametricDatatype() ||
-           tn.isTuple() || tn.isRecord();
+    return tn.isDatatype() || tn.isParametricDatatype();
   }
   static bool isTypeDatatype( TypeNode tn ){
-    return tn.isDatatype() || tn.isParametricDatatype() ||
-           tn.isTuple() || tn.isRecord();
+    return tn.isDatatype() || tn.isParametricDatatype();
   }
 private:
   static Node collectRef( Node n, std::vector< Node >& sk, std::map< Node, Node >& rf, std::vector< Node >& rf_pending,
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 749d6b58a..c31a462bd 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -91,30 +91,6 @@ typerule MU ::CVC4::theory::datatypes::DatatypeMuTypeRule
 # mu applications are constant expressions
 construle MU ::CVC4::theory::datatypes::DatatypeMuTypeRule
 
-operator TUPLE_TYPE 0: "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 0: "a tuple (N-ary)"
-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; payload is an instance of the CVC4::TupleSelect class"
-parameterized TUPLE_SELECT TUPLE_SELECT_OP 1 "tuple select; first parameter is a TUPLE_SELECT_OP, second is the tuple"
-typerule TUPLE_SELECT ::CVC4::theory::datatypes::TupleSelectTypeRule
-
 constant TUPLE_UPDATE_OP \
         ::CVC4::TupleUpdate \
         ::CVC4::TupleUpdateHashFunction \
@@ -129,33 +105,21 @@ constant RECORD_TYPE \
     "expr/record.h" \
     "record type"
 cardinality RECORD_TYPE \
-    "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \
+    "::CVC4::theory::datatypes::RecordProperties::computeCardinality(%TYPE%)" \
     "theory/datatypes/theory_datatypes_type_rules.h"
 well-founded RECORD_TYPE \
-    "::CVC4::theory::datatypes::TupleProperties::isWellFounded(%TYPE%)" \
+    "::CVC4::theory::datatypes::RecordProperties::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 0: "a record; first parameter is a RECORD_TYPE; remaining parameters (if any) are the individual values for fields, in order"
-typerule RECORD ::CVC4::theory::datatypes::RecordTypeRule
-construle RECORD ::CVC4::theory::datatypes::RecordProperties
-
-constant RECORD_SELECT_OP \
-        ::CVC4::RecordSelect \
-        ::CVC4::RecordSelectHashFunction \
-        "expr/record.h" \
-        "operator for a record select; payload is an instance CVC4::RecordSelect class"
-parameterized RECORD_SELECT RECORD_SELECT_OP 1 "record select; first parameter is a RECORD_SELECT_OP, second is a record term to select from"
-typerule RECORD_SELECT ::CVC4::theory::datatypes::RecordSelectTypeRule
-
 constant RECORD_UPDATE_OP \
         ::CVC4::RecordUpdate \
         ::CVC4::RecordUpdateHashFunction \
         "expr/record.h" \
-        "operator for a record update; payload is an instance CVC4::RecordSelect class"
+        "operator for a record update; payload is an instance CVC4::RecordUpdate class"
 parameterized RECORD_UPDATE RECORD_UPDATE_OP 2 "record update; first parameter is a RECORD_UPDATE_OP (which references a field), second is a record term to update, third is the element to store in the record in the given field"
 typerule RECORD_UPDATE ::CVC4::theory::datatypes::RecordUpdateTypeRule
 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index c8d7338a7..ad2b1a297 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -147,12 +147,8 @@ void TheoryDatatypes::check(Effort e) {
 
     // 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 ),
+            ( atom[0].getKind() != kind::TUPLE_UPDATE && atom[1].getKind() != kind::TUPLE_UPDATE &&
+              atom[0].getKind() != kind::RECORD_UPDATE && atom[1].getKind() != kind::RECORD_UPDATE),
             "tuple/record escaped into datatypes decision procedure; should have been rewritten away" );
 
     //assert the fact
@@ -550,86 +546,21 @@ void TheoryDatatypes::presolve() {
 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_TOTAL, 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_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]);
-  }
-
   TypeNode t = in.getType();
 
-  // 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) {
-    if((t.isTuple() || t.isRecord()) && in.hasAttribute(smt::BooleanTermAttr())) {
-      Debug("tuprec") << "should map " << in << " of type " << t << " back to " << in.getAttribute(smt::BooleanTermAttr()).getType() << endl;
-      Debug("tuprec") << "so " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getDatatype() << " goes to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getDatatype() << endl;
-      if(t.isTuple()) {
-        Debug("tuprec") << "current datatype-tuple-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeTupleAttr()) << endl;
-        Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()) << endl;
-        NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeTupleAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()));
-      } else {
-        Debug("tuprec") << "current datatype-record-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeRecordAttr()) << endl;
-        Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()) << endl;
-        NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeRecordAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()));
-      }
-    }
-
-    if( in.getKind()==EQUAL ){
-      Node nn;
-      std::vector< Node > rew;
-      if( DatatypesRewriter::checkClash(in[0], in[1], rew) ){
-        nn = NodeManager::currentNM()->mkConst(false);
-      }else{
-        nn = rew.size()==0 ? d_true :
-                  ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) );
-      }
-      return nn;
-    }
-
-    // nothing to do
-    return in;
-  }
-
-  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) {
+  if(in.getKind() == kind::TUPLE_UPDATE || in.getKind() == kind::RECORD_UPDATE) {
+    Assert( t.isDatatype() );
+    const Datatype& dt = DatatypeType(t.toType()).getDatatype();
     NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
     b << Node::fromExpr(dt[0].getConstructor());
     size_t size, updateIndex;
     if(in.getKind() == kind::TUPLE_UPDATE) {
-      size = t.getNumChildren();
+      Assert( t.isTuple() );
+      size = t.getTupleLength();
       updateIndex = in.getOperator().getConst<TupleUpdate>().getIndex();
     } else { // kind::RECORD_UPDATE
-      const Record& record = t.getConst<Record>();
+      Assert( t.isRecord() );
+      const Record& record = t.getRecord();
       size = record.getNumFields();
       updateIndex = record.getIndex(in.getOperator().getConst<RecordUpdate>().getField());
     }
@@ -647,15 +578,39 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
       }
     }
     Debug("tuprec") << "builder says " << b << std::endl;
-    n = b;
+    Node n = b;
+    return n;
   }
 
-  Assert(!n.isNull());
+  if((t.isTuple() || t.isRecord()) && in.hasAttribute(smt::BooleanTermAttr())) {
+    Debug("tuprec") << "should map " << in << " of type " << t << " back to " << in.getAttribute(smt::BooleanTermAttr()).getType() << endl;
+    Debug("tuprec") << "so " << t.getDatatype() << " goes to " << in.getAttribute(smt::BooleanTermAttr()).getType().getDatatype() << endl;
+    if(t.isTuple()) {
+      Debug("tuprec") << "current datatype-tuple-attr is " << t.getAttribute(expr::DatatypeTupleAttr()) << endl;
+      Debug("tuprec") << "setting to " << in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeTupleAttr()) << endl;
+      t.setAttribute(expr::DatatypeTupleAttr(), in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeTupleAttr()));
+    } else {
+      Debug("tuprec") << "current datatype-record-attr is " << t.getAttribute(expr::DatatypeRecordAttr()) << endl;
+      Debug("tuprec") << "setting to " << in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeRecordAttr()) << endl;
+      t.setAttribute(expr::DatatypeRecordAttr(), in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeRecordAttr()));
+    }
+  }
 
+  if( in.getKind()==EQUAL ){
+    Node nn;
+    std::vector< Node > rew;
+    if( DatatypesRewriter::checkClash(in[0], in[1], rew) ){
+      nn = NodeManager::currentNM()->mkConst(false);
+    }else{
+      nn = rew.size()==0 ? d_true :
+                ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) );
+    }
+    return nn;
+  }
 
-  Debug("tuprec") << "REWROTE " << in << " to " << n << std::endl;
+  // nothing to do
+  return in;
 
-  return n;
 }
 
 void TheoryDatatypes::addSharedTerm(TNode t) {
@@ -2123,9 +2078,7 @@ Node TheoryDatatypes::mkAnd( std::vector< TNode >& assumptions ) {
 }
 
 bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand ) {
-  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.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) {
     if( n1.getOperator() != n2.getOperator() ) {
       return true;
     } else {
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 8b723f43e..477ce6ba5 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -267,44 +267,6 @@ 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);
-    if(n.getOperator().getKind() != kind::TUPLE_SELECT_OP) {
-      throw TypeCheckingExceptionPrivate(n, "Tuple-select expression requires TupleSelect operator");
-    }
-    const TupleSelect& ts = n.getOperator().getConst<TupleSelect>();
-    TypeNode tupleType = n[0].getType(check);
-    if(!tupleType.isTuple()) {
-      if(!tupleType.hasAttribute(expr::DatatypeTupleAttr())) {
-        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);
@@ -313,16 +275,14 @@ struct TupleUpdateTypeRule {
     TypeNode newValue = n[1].getType(check);
     if(check) {
       if(!tupleType.isTuple()) {
-        if(!tupleType.hasAttribute(expr::DatatypeTupleAttr())) {
-          throw TypeCheckingExceptionPrivate(n, "Tuple-update expression formed over non-tuple");
-        }
+        throw TypeCheckingExceptionPrivate(n, "Tuple-update expression formed over non-tuple");
         tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr());
       }
-      if(tu.getIndex() >= tupleType.getNumChildren()) {
+      if(tu.getIndex() >= tupleType.getTupleLength()) {
         std::stringstream ss;
         ss << "Tuple-update expression index `" << tu.getIndex()
            << "' is not a valid index; tuple type only has "
-           << tupleType.getNumChildren() << " fields";
+           << tupleType.getTupleLength() << " fields";
         throw TypeCheckingExceptionPrivate(n, ss.str().c_str());
       }
     }
@@ -330,138 +290,6 @@ struct TupleUpdateTypeRule {
   }
 };/* 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>();
-    const Record::FieldVector& fields = rec.getFields();
-    if(check) {
-      Record::FieldVector::const_iterator i = fields.begin();
-      for(TNode::iterator child_it = n.begin(), child_it_end = n.end();
-          child_it != child_it_end;
-          ++child_it, ++i) {
-        if(i == fields.end()) {
-          throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal");
-        }
-        if(!(*child_it).getType(check).isComparableTo(TypeNode::fromType((*i).second))) {
-          std::stringstream ss;
-          ss << "record description types differ from record literal types\nDescription type: " << (*child_it).getType() << "\nLiteral type: " << (*i).second;
-          throw TypeCheckingExceptionPrivate(n, ss.str());
-        }
-      }
-      if(i != fields.end()) {
-        throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal");
-      }
-    }
-    return nodeManager->mkRecordType(rec);
-  }
-};/* struct RecordTypeRule */
-
-struct RecordSelectTypeRule {
-  inline static Record::FieldVector::const_iterator record_find(const Record::FieldVector& fields, std::string name){
-    for(Record::FieldVector::const_iterator i = fields.begin(), i_end = fields.end(); i != i_end; ++i){
-      if((*i).first == name) {
-        return i;
-      }
-    }
-    return fields.end();
-  }
-
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
-    Assert(n.getKind() == kind::RECORD_SELECT);
-    NodeManagerScope nms(nodeManager);
-    if(n.getOperator().getKind() != kind::RECORD_SELECT_OP) {
-      throw TypeCheckingExceptionPrivate(n, "Tuple-select expression requires TupleSelect operator");
-    }
-    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();
-    const Record::FieldVector& fields = rec.getFields();
-    Record::FieldVector::const_iterator field = record_find(fields, rs.getField());
-    if(field == fields.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);
@@ -471,10 +299,7 @@ struct RecordUpdateTypeRule {
     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());
+        throw TypeCheckingExceptionPrivate(n, "Record-update expression formed over non-record");
       }
       const Record& rec = recordType.getRecord();
       if(!rec.contains(ru.getField())) {
@@ -491,33 +316,16 @@ struct RecordUpdateTypeRule {
 struct RecordProperties {
   inline static Node mkGroundTerm(TypeNode type) {
     Assert(type.getKind() == kind::RECORD_TYPE);
-
-    const Record& rec = type.getRecord();
-    const Record::FieldVector& fields = rec.getFields();
-    std::vector<Node> children;
-    for(Record::FieldVector::const_iterator i = fields.begin(),
-          i_end = fields.end();
-        i != i_end;
-        ++i) {
-      children.push_back((*i).second.mkGroundTerm());
-    }
-
-    return NodeManager::currentNM()->mkNode(NodeManager::currentNM()->mkConst(rec), children);
+    return Node::null();
   }
-
   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;
+  }
+  inline static Cardinality computeCardinality(TypeNode type) {
+    Cardinality card(1);
+    return card;
+  }
+  inline static bool isWellFounded(TypeNode type) {
     return true;
   }
 };/* struct RecordProperties */
diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index 62446a937..77db1968a 100644
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -221,3 +221,4 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
    ++*this; //increment( d_ctor );
    AlwaysAssert( !isFinished() );
 }
+
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 921ba403c..1f30498d6 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -177,90 +177,6 @@ public:
 
 };/* DatatypesEnumerator */
 
-class TupleEnumerator : public TypeEnumeratorBase<TupleEnumerator> {
-  TypeEnumeratorProperties * d_tep;
-  TypeEnumerator** d_enumerators;
-
-  /** Allocate and initialize the delegate enumerators */
-  void newEnumerators() {
-    d_enumerators = new TypeEnumerator*[getType().getNumChildren()];
-    for(size_t i = 0; i < getType().getNumChildren(); ++i) {
-      d_enumerators[i] = new TypeEnumerator(getType()[i], d_tep);
-    }
-  }
-
-  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, TypeEnumeratorProperties * tep = NULL) throw() :
-    TypeEnumeratorBase<TupleEnumerator>(type), d_tep(tep) {
-    Assert(type.isTuple());
-    newEnumerators();
-  }
-
-  TupleEnumerator(const TupleEnumerator& te) throw() :
-    TypeEnumeratorBase<TupleEnumerator>(te.getType()),
-    d_tep(te.d_tep),
-    d_enumerators(NULL) {
-
-    if(te.d_enumerators != NULL) {
-      newEnumerators();
-      for(size_t i = 0; i < getType().getNumChildren(); ++i) {
-        *d_enumerators[i] = TypeEnumerator(*te.d_enumerators[i]);
-      }
-    }
-  }
-
-  virtual ~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], d_tep);
-      } else {
-        ++*d_enumerators[i];
-        return *this;
-      }
-    }
-
-    deleteEnumerators();
-
-    return *this;
-  }
-
-  bool isFinished() throw() {
-    return d_enumerators == NULL;
-  }
-
-};/* TupleEnumerator */
 
 class RecordEnumerator : public TypeEnumeratorBase<RecordEnumerator> {
   TypeEnumeratorProperties * d_tep;
@@ -316,15 +232,8 @@ public:
       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);
+
+    return Node::null();
   }
 
   RecordEnumerator& operator++() throw() {
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index d024e0270..0eff9bd5d 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -784,9 +784,6 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
         continue;
       }
       TypeNode t = TypeSet::getType(it);
-      if(t.isTuple() || t.isRecord()) {
-        t = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
-      }
       
       //get properties of this type
       bool isCorecursive = false;