More simplification to internal implementation of tuples and records.

15 files changed, 144 insertions, 382 deletions

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 52174dce0..a9982e336 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -1818,8 +1818,7 @@ Expr ValidityChecker::recordExpr(const std::vector<std::string>& fields,
 Expr ValidityChecker::recSelectExpr(const Expr& record, const std::string& field) {
   Type t = record.getType();
   const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype();
-  const CVC4::Record& rec = ((CVC4::DatatypeType)t).getRecord();
-  unsigned index = rec.getIndex(field);
+  unsigned index = CVC4::Datatype::indexOf( dt[0].getSelector(field) );
   return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR_TOTAL, dt[0][index].getSelector(), record);
 }
 
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 32c0bb6dd..99698df99 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -51,6 +51,10 @@ typedef expr::Attribute<expr::attr::DatatypeFiniteComputedTag, bool> DatatypeFin
 typedef expr::Attribute<expr::attr::DatatypeUFiniteTag, bool> DatatypeUFiniteAttr;
 typedef expr::Attribute<expr::attr::DatatypeUFiniteComputedTag, bool> DatatypeUFiniteComputedAttr;
 
+Datatype::~Datatype(){
+  delete d_record;
+}
+
 const Datatype& Datatype::datatypeOf(Expr item) {
   ExprManagerScope ems(item);
   TypeNode t = Node::fromExpr(item).getType();
@@ -133,6 +137,14 @@ void Datatype::resolve(ExprManager* em,
       d_involvesUt =  true;
     }
   }
+
+  if( d_isRecord ){
+    std::vector< std::pair<std::string, Type> > fields;
+    for( unsigned i=0; i<(*this)[0].getNumArgs(); i++ ){
+      fields.push_back( std::pair<std::string, Type>( (*this)[0][i].getName(), (*this)[0][i].getRangeType() ) );
+    }
+    d_record = new Record(fields);
+  }
 }
 
 void Datatype::addConstructor(const DatatypeConstructor& c) {
@@ -152,10 +164,12 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){
 }
 
 void Datatype::setTuple() {
+  PrettyCheckArgument(!d_resolved, this, "cannot set tuple to a finalized Datatype");
   d_isTuple = true;
 }
 
 void Datatype::setRecord() {
+  PrettyCheckArgument(!d_resolved, this, "cannot set record to a finalized Datatype");
   d_isRecord = true;
 }
 
@@ -974,6 +988,10 @@ SelectorType DatatypeConstructorArg::getType() const {
   return getSelector().getType();
 }
 
+Type DatatypeConstructorArg::getRangeType() const {
+  return getType().getRangeType();
+}
+
 bool DatatypeConstructorArg::isUnresolvedSelf() const throw() {
   return d_selector.isNull() && d_name.size() == d_name.find('\0') + 1;
 }
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 625fbb5d4..c64b71f5a 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -155,6 +155,11 @@ public:
   SelectorType getType() const;
 
   /**
+   * Get the range type of this argument.
+   */
+  Type getRangeType() const;
+
+  /**
    * Get the name of the type of this constructor argument
    * (Datatype field).  Can be used for not-yet-resolved Datatypes
    * (in which case the name of the unresolved type, or "[self]"
@@ -474,6 +479,7 @@ private:
   bool d_isCo;
   bool d_isTuple;
   bool d_isRecord;
+  Record * d_record;
   std::vector<DatatypeConstructor> d_constructors;
   bool d_resolved;
   Type d_self;
@@ -553,6 +559,8 @@ public:
    */
   inline Datatype(std::string name, const std::vector<Type>& params, bool isCo = false);
 
+  ~Datatype();
+
   /**
    * Add a constructor to this Datatype.  Constructor names need not
    * be unique; they are for convenience and pretty-printing only.
@@ -602,6 +610,9 @@ public:
   /** is this a record datatype? */
   inline bool isRecord() const;
 
+  /** get the record representation for this datatype */
+  inline Record * getRecord() const;
+
   /**
    * Return the cardinality of this datatype (the sum of the
    * cardinalities of its constructors).  The Datatype must be
@@ -772,6 +783,7 @@ inline Datatype::Datatype(std::string name, bool isCo) :
   d_isCo(isCo),
   d_isTuple(false),
   d_isRecord(false),
+  d_record(NULL),
   d_constructors(),
   d_resolved(false),
   d_self(),
@@ -788,6 +800,7 @@ inline Datatype::Datatype(std::string name, const std::vector<Type>& params, boo
   d_isCo(isCo),
   d_isTuple(false),
   d_isRecord(false),
+  d_record(NULL),
   d_constructors(),
   d_resolved(false),
   d_self(),
@@ -844,6 +857,10 @@ inline bool Datatype::isRecord() const {
   return d_isRecord;
 }
 
+inline Record * Datatype::getRecord() const {
+  return d_record;
+}
+
 inline bool Datatype::operator!=(const Datatype& other) const throw() {
   return !(*this == other);
 }
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index ce7a92b48..39a2a268c 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -791,7 +791,7 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
         j != j_end;
         ++j) {
       const DatatypeConstructorArg& a = *j;
-      Type selectorType = a.getSelector().getType();
+      Type selectorType = a.getType();
       Assert(a.isResolved() &&
              selectorType.isSelector() &&
              SelectorType(selectorType).getDomain() == dtt,
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index e6e44928d..db4269ca6 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -170,7 +170,9 @@ NodeManager::~NodeManager() {
     d_operators[i] = Node::null();
   }
 
-  d_tupleAndRecordTypes.clear();
+  //d_tupleAndRecordTypes.clear();
+  d_tt_cache.d_children.clear();
+  d_rt_cache.d_children.clear();
 
   Assert(!d_attrManager->inGarbageCollection() );
   while(!d_zombies.empty()) {
@@ -461,6 +463,47 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds)
   return TypeNode(mkTypeConst(bounds));
 }
 
+TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) {
+  if( index==types.size() ){
+    if( d_data.isNull() ){
+      Datatype dt("__cvc4_tuple");
+      dt.setTuple();
+      DatatypeConstructor c("__cvc4_tuple_ctor");
+      for (unsigned i = 0; i < types.size(); ++ i) {
+        std::stringstream ss;
+        ss << "__cvc4_tuple_stor_" << i;
+        c.addArg(ss.str().c_str(), types[i].toType());
+      }
+      dt.addConstructor(c);
+      d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt));
+      Debug("tuprec-debug") << "Return type : " << d_data << std::endl;
+    }
+    return d_data;
+  }else{
+    return d_children[types[index]].getTupleType( nm, types, index+1 );
+  }
+}
+
+TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Record& rec, unsigned index ) {
+  if( index==rec.getNumFields() ){
+    if( d_data.isNull() ){
+      const Record::FieldVector& fields = rec.getFields();
+      Datatype dt("__cvc4_record");
+      dt.setRecord();
+      DatatypeConstructor c("__cvc4_record_ctor");
+      for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
+        c.addArg((*i).first, (*i).second);
+      }
+      dt.addConstructor(c);
+      d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt));
+      Debug("tuprec-debug") << "Return type : " << d_data << std::endl;
+    }
+    return d_data;
+  }else{
+    return d_children[TypeNode::fromType( rec[index].second )][rec[index].first].getRecordType( nm, rec, index+1 );
+  }
+}
+
 TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
   std::vector< TypeNode > ts;
   Debug("tuprec-debug") << "Make tuple type : ";
@@ -470,60 +513,11 @@ TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
     Debug("tuprec-debug") << types[i] << " ";
   }
   Debug("tuprec-debug") << std::endl;
-  //index based on function type
-  TypeNode tindex;
-  if( types.empty() ){
-    //do nothing (will index on null type)
-  }else if( types.size()==1 ){
-    tindex = types[0];
-  }else{
-    TypeNode tt = ts.back();
-    ts.pop_back();
-    tindex = mkFunctionType( ts, tt );
-    ts.push_back( tt );
-  }
-  TypeNode& dtt = d_tupleAndRecordTypes[tindex];
-  if(dtt.isNull()) {
-    Datatype dt("__cvc4_tuple");
-    dt.setTuple();
-    DatatypeConstructor c("__cvc4_tuple_ctor");
-    for (unsigned i = 0; i < ts.size(); ++ i) {
-      std::stringstream ss;
-      ss << "__cvc4_tuple_stor_" << i;
-      c.addArg(ss.str().c_str(), ts[i].toType());
-    }
-    dt.addConstructor(c);
-    dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt));
-    dtt.setAttribute(DatatypeTupleAttr(), tindex);
-    Debug("tuprec-debug") << "Return type : " << dtt << std::endl;
-  }else{
-    Debug("tuprec-debug") << "Return cached type : " << dtt << std::endl;
-  }
-  Assert(!dtt.isNull());
-  return dtt;
+  return d_tt_cache.getTupleType( this, ts );
 }
 
 TypeNode NodeManager::mkRecordType(const Record& rec) {
-  //index based on type constant
-  TypeNode tindex = mkTypeConst(rec);
-  TypeNode& dtt = d_tupleAndRecordTypes[tindex];
-  if(dtt.isNull()) {
-    const Record::FieldVector& fields = rec.getFields();
-    Datatype dt("__cvc4_record");
-    dt.setRecord();
-    DatatypeConstructor c("__cvc4_record_ctor");
-    for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
-      c.addArg((*i).first, (*i).second);
-    }
-    dt.addConstructor(c);
-    dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt));
-    dtt.setAttribute(DatatypeRecordAttr(), tindex);
-    Debug("tuprec-debug") << "Return type : " << dtt << std::endl;
-  }else{
-    Debug("tuprec-debug") << "Return cached type : " << dtt << std::endl;
-  }
-  Assert(!dtt.isNull());
-  return dtt;
+  return d_rt_cache.getRecordType( this, rec );
 }
 
 void NodeManager::reclaimAllZombies(){
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 45c9afbde..974a1ed94 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -166,7 +166,20 @@ class NodeManager {
   /**
    * A map of tuple and record types to their corresponding datatype.
    */
-  std::hash_map<TypeNode, TypeNode, TypeNodeHashFunction> d_tupleAndRecordTypes;
+  class TupleTypeCache {
+  public:
+    std::map< TypeNode, TupleTypeCache > d_children;
+    TypeNode d_data;
+    TypeNode getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index = 0 );
+  };
+  class RecTypeCache {
+  public:
+    std::map< TypeNode, std::map< std::string, RecTypeCache > > d_children;
+    TypeNode d_data;
+    TypeNode getRecordType( NodeManager * nm, const Record& rec, unsigned index = 0 );
+  };
+  TupleTypeCache d_tt_cache;
+  RecTypeCache d_rt_cache;
 
   /**
    * Keep a count of all abstract values produced by this NodeManager.
diff --git a/src/expr/node_manager_attributes.h b/src/expr/node_manager_attributes.h
index 41086ac21..1f67a09a5 100644
--- a/src/expr/node_manager_attributes.h
+++ b/src/expr/node_manager_attributes.h
@@ -28,8 +28,6 @@ namespace attr {
   struct VarNameTag { };
   struct GlobalVarTag { };
   struct SortArityTag { };
-  struct DatatypeTupleTag { };
-  struct DatatypeRecordTag { };
   struct TypeTag { };
   struct TypeCheckedTag { };
 }/* CVC4::expr::attr namespace */
@@ -37,10 +35,6 @@ namespace attr {
 typedef Attribute<attr::VarNameTag, std::string> VarNameAttr;
 typedef Attribute<attr::GlobalVarTag(), bool> GlobalVarAttr;
 typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr;
-/** Attribute true for datatype types that are replacements for tuple types */
-typedef expr::Attribute<expr::attr::DatatypeTupleTag, TypeNode> DatatypeTupleAttr;
-/** Attribute true for datatype types that are replacements for record types */
-typedef expr::Attribute<expr::attr::DatatypeRecordTag, TypeNode> DatatypeRecordAttr;
 typedef expr::Attribute<expr::attr::TypeTag, TypeNode> TypeAttr;
 typedef expr::Attribute<expr::attr::TypeCheckedTag, bool> TypeCheckedAttr;
 
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 755b16e46..eecb2c206 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -93,37 +93,21 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
           t.getConst<TypeConstant>() == REAL_TYPE );
     }
   }
-  if(isTuple() || isRecord()) {
-    if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) {
+  if(isTuple() && t.isTuple()) {
+    const Datatype& dt1 = getDatatype();
+    const Datatype& dt2 = t.getDatatype();
+    if( dt1[0].getNumArgs()!=dt2[0].getNumArgs() ){
       return false;
     }
-    if(isTuple()) {
-      if(getNumChildren() != t.getNumChildren()) {
+    // r1's fields must be subtypes of r2's, in order
+    for( unsigned i=0; i<dt1[0].getNumArgs(); i++ ){
+      if( !dt1[0][i].getRangeType().isSubtypeOf( dt2[0][i].getRangeType() ) ){
         return false;
       }
-      // children must be subtypes of t's, in order
-      for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) {
-        if(!(*i).isSubtypeOf(*j)) {
-          return false;
-        }
-      }
-    } else {
-      const Record& r1 = getRecord();
-      const Record& r2 = t.getRecord();
-      if(r1.getNumFields() != r2.getNumFields()) {
-        return false;
-      }
-      const Record::FieldVector& fields1 = r1.getFields();
-      const Record::FieldVector& fields2 = r2.getFields();
-      // r1's fields must be subtypes of r2's, in order
-      // names must match also
-      for(Record::FieldVector::const_iterator i = fields1.begin(), j = fields2.begin(); i != fields1.end(); ++i, ++j) {
-        if((*i).first != (*j).first || !(*i).second.isSubtypeOf((*j).second)) {
-          return false;
-        }
-      }
     }
     return true;
+  }else if( t.isRecord() && t.isRecord() ){
+    //TBD
   }
   if(isFunction()) {
     // A function is a subtype of another if the args are the same type, and
@@ -163,39 +147,21 @@ bool TypeNode::isComparableTo(TypeNode t) const {
   if(isSubtypeOf(NodeManager::currentNM()->realType())) {
     return t.isSubtypeOf(NodeManager::currentNM()->realType());
   }
-  if(isTuple() || isRecord()) {
-    if(t.isTuple() || t.isRecord()) {
-      if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) {
+  if(isTuple() && t.isTuple()) {
+    const Datatype& dt1 = getDatatype();
+    const Datatype& dt2 = t.getDatatype();
+    if( dt1[0].getNumArgs()!=dt2[0].getNumArgs() ){
+      return false;
+    }
+    // r1's fields must be subtypes of r2's, in order
+    for( unsigned i=0; i<dt1[0].getNumArgs(); i++ ){
+      if( !dt1[0][i].getRangeType().isComparableTo( dt2[0][i].getRangeType() ) ){
         return false;
       }
-      if(isTuple()) {
-        if(getNumChildren() != t.getNumChildren()) {
-          return false;
-        }
-        // children must be comparable to t's, in order
-        for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) {
-          if(!(*i).isComparableTo(*j)) {
-            return false;
-          }
-        }
-      } else {
-        const Record& r1 = getRecord();
-        const Record& r2 = t.getRecord();
-        if(r1.getNumFields() != r2.getNumFields()) {
-          return false;
-        }
-        // r1's fields must be comparable to r2's, in order
-        // names must match also
-        const Record::FieldVector& fields1 = r1.getFields();
-        const Record::FieldVector& fields2 = r2.getFields();
-        for(Record::FieldVector::const_iterator i = fields1.begin(), j = fields2.begin(); i != fields1.end(); ++i, ++j) {
-          if((*i).first != (*j).first || !(*i).second.isComparableTo((*j).second)) {
-            return false;
-          }
-        }
-      }
-      return true;
     }
+    return true;
+  }else if( isRecord() && t.isRecord() ){
+    //TBD
   } else if(isParametricDatatype() && t.isParametricDatatype()) {
     Assert(getKind() == kind::PARAMETRIC_DATATYPE);
     Assert(t.getKind() == kind::PARAMETRIC_DATATYPE);
@@ -271,13 +237,13 @@ std::vector<TypeNode> TypeNode::getParamTypes() const {
 
 /** Is this a tuple type? */
 bool TypeNode::isTuple() const {
-  return ( getKind() == kind::DATATYPE_TYPE && hasAttribute(expr::DatatypeTupleAttr()) ) ||
+  return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isTuple() ) ||
     ( isPredicateSubtype() && getSubtypeParentType().isTuple() );
 }
 
 /** Is this a record type? */
 bool TypeNode::isRecord() const {
-  return ( getKind() == kind::DATATYPE_TYPE && hasAttribute(expr::DatatypeRecordAttr()) )  ||
+  return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isRecord() )  ||
     ( isPredicateSubtype() && getSubtypeParentType().isRecord() );
 }
 
@@ -294,14 +260,16 @@ vector<TypeNode> TypeNode::getTupleTypes() const {
   Assert(dt.getNumConstructors()==1);
   vector<TypeNode> types;
   for(unsigned i = 0; i < dt[0].getNumArgs(); ++i) {
-    types.push_back(TypeNode::fromType(((SelectorType)dt[0][i].getSelector().getType()).getRangeType()));
+    types.push_back(TypeNode::fromType(dt[0][i].getRangeType()));
   }
   return types;
 }
 
 const Record& TypeNode::getRecord() const {
   Assert(isRecord());
-  return getAttribute(expr::DatatypeRecordAttr()).getConst<Record>();
+  const Datatype & dt = getDatatype();
+  return *(dt.getRecord());
+  //return getAttribute(expr::DatatypeRecordAttr()).getConst<Record>();
 }
 
 vector<TypeNode> TypeNode::getSExprTypes() const {
@@ -449,61 +417,24 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
       Assert(t1.isInteger());
       return TypeNode();
     }
-/*
-  case kind::TUPLE_TYPE: {
-    // if the other == this one, we returned already, above
-    if(t0.getBaseType() == t1) {
-      return t1;
-    }
-    if(!t1.isTuple() || t0.getNumChildren() != t1.getNumChildren()) {
-      // no compatibility between t0, t1
-      return TypeNode();
-    }
-    std::vector<TypeNode> types;
-    // construct childwise leastCommonType, if one exists
-    for(const_iterator i = t0.begin(), j = t1.begin(); i != t0.end(); ++i, ++j) {
-      TypeNode kid = leastCommonTypeNode(*i, *j);
-      if(kid.isNull()) {
-        // no common supertype: types t0, t1 not compatible
-        return TypeNode();
-      }
-      types.push_back(kid);
-    }
-    // if we make it here, we constructed the least common type
-    return NodeManager::currentNM()->mkTupleType(types);
-  }
-  case kind::RECORD_TYPE: {
-    // if the other == this one, we returned already, above
-    if(t0.getBaseType() == t1) {
-      return t1;
-    }
-    const Record& r0 = t0.getConst<Record>();
-    if(!t1.isRecord() || r0.getNumFields() != t1.getConst<Record>().getNumFields()) {
-      // no compatibility between t0, t1
-      return TypeNode();
-    }
-    std::vector< std::pair<std::string, Type> > fields;
-    const Record& r1 = t1.getConst<Record>();
-    const Record::FieldVector& fields0 = r0.getFields();
-    const Record::FieldVector& fields1 = r1.getFields();
-    // construct childwise leastCommonType, if one exists
-    for(Record::FieldVector::const_iterator i = fields0.begin(), j = fields1.begin(); i != fields0.end(); ++i, ++j) {
-      TypeNode kid = leastCommonTypeNode(TypeNode::fromType((*i).second), TypeNode::fromType((*j).second));
-      if((*i).first != (*j).first || kid.isNull()) {
-        // if field names differ, or no common supertype, then
-        // types t0, t1 not compatible
-        return TypeNode();
-      }
-      fields.push_back(std::make_pair((*i).first, kid.toType()));
-    }
-    // if we make it here, we constructed the least common type
-    return NodeManager::currentNM()->mkRecordType(Record(fields));
-  }
-*/
   case kind::DATATYPE_TYPE:
-    // t1 might be a subtype tuple or record
-    if(t1.getBaseType() == t0) {
-      return t0;
+    if( t0.isTuple() && t1.isTuple() ){
+      const Datatype& dt1 = t0.getDatatype();
+      const Datatype& dt2 = t1.getDatatype();
+      if( dt1[0].getNumArgs()==dt2[0].getNumArgs() ){
+        std::vector< TypeNode > lc_types;
+        for( unsigned i=0; i<dt1[0].getNumArgs(); i++ ){
+          TypeNode tc = leastCommonTypeNode( TypeNode::fromType( dt1[0][i].getRangeType() ), TypeNode::fromType( dt2[0][i].getRangeType() ) );
+          if( tc.isNull() ){
+            return tc;
+          }else{
+            lc_types.push_back( tc );
+          }
+        }
+        return NodeManager::currentNM()->mkTupleType( lc_types );
+      }
+    }else if( t0.isRecord() && t1.isRecord() ){
+      //TBD
     }
     // otherwise no common ancestor
     return TypeNode();
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 07d78a6fd..1adc71d70 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -137,26 +137,6 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode,
   TypeNode in_t = in.getType();
   if( processing.find( in_t )==processing.end() ){
     processing[in_t] = true;
-    if(in.getType().isRecord()) {
-      Assert(as.isRecord());
-      const Record& inRec = in.getType().getRecord();
-      const Record& asRec = as.getRecord();
-      Assert(inRec.getNumFields() == asRec.getNumFields());
-      const Datatype & dt = ((DatatypeType)in.getType().toType()).getDatatype();
-      NodeBuilder<> nb(kind::APPLY_CONSTRUCTOR);
-      nb << NodeManager::currentNM()->mkConst(asRec);
-      for(size_t i = 0; i < asRec.getNumFields(); ++i) {
-        Assert(inRec[i].first == asRec[i].first);
-        Node arg = NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, dt[0][i].getSelector(), in);
-        if(inRec[i].second != asRec[i].second) {
-          arg = rewriteAs(arg, TypeNode::fromType(asRec[i].second), processing);
-        }
-        nb << arg;
-      }
-      Node out = nb;
-      processing.erase( in_t );
-      return out;
-    }
     if(in.getType().isDatatype()) {
       if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) {
         processing.erase( in_t );
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index c31a462bd..d035f0fa7 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -85,12 +85,6 @@ 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
 
-## for co-datatypes
-operator MU 2 "a mu operator, first argument is a bound variable, second argument is body"
-typerule MU ::CVC4::theory::datatypes::DatatypeMuTypeRule
-# mu applications are constant expressions
-construle MU ::CVC4::theory::datatypes::DatatypeMuTypeRule
-
 constant TUPLE_UPDATE_OP \
         ::CVC4::TupleUpdate \
         ::CVC4::TupleUpdateHashFunction \
@@ -99,22 +93,6 @@ constant TUPLE_UPDATE_OP \
 parameterized TUPLE_UPDATE TUPLE_UPDATE_OP 2 "tuple update; first parameter is a TUPLE_UPDATE_OP (which references an index), second is the tuple, third is the element to store in the tuple at the given index"
 typerule TUPLE_UPDATE ::CVC4::theory::datatypes::TupleUpdateTypeRule
 
-constant RECORD_TYPE \
-    ::CVC4::Record \
-    ::CVC4::RecordHashFunction \
-    "expr/record.h" \
-    "record type"
-cardinality RECORD_TYPE \
-    "::CVC4::theory::datatypes::RecordProperties::computeCardinality(%TYPE%)" \
-    "theory/datatypes/theory_datatypes_type_rules.h"
-well-founded RECORD_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"
-
 constant RECORD_UPDATE_OP \
         ::CVC4::RecordUpdate \
         ::CVC4::RecordUpdateHashFunction \
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index ad2b1a297..51300bfba 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -582,20 +582,6 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
     return n;
   }
 
-  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;
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 477ce6ba5..e50d714e7 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -210,49 +210,6 @@ struct DatatypeAscriptionTypeRule {
   }
 };/* struct DatatypeAscriptionTypeRule */
 
-/* For co-datatypes */
-class DatatypeMuTypeRule {
-private:
-  //a Mu-expression is constant iff its body is composed of constructors applied to constant expr and bound variables only
-  inline static bool computeIsConstNode(TNode n, std::vector< TNode >& fv ){
-    if( n.getKind()==kind::MU ){
-      fv.push_back( n[0] );
-      bool ret = computeIsConstNode( n[1], fv );
-      fv.pop_back();
-      return ret;
-    }else if( n.isConst() || std::find( fv.begin(), fv.end(), n )!=fv.end() ){
-      return true;
-    }else if( n.getKind()==kind::APPLY_CONSTRUCTOR ){
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        if( !computeIsConstNode( n[i], fv ) ){
-          return false;
-        }
-      }
-      return true; 
-    }else{
-      return false;
-    }
-  }
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
-    if( n[0].getKind()!=kind::BOUND_VARIABLE  ) {
-      std::stringstream ss;
-      ss << "expected a bound var for MU expression, got `"
-         << n[0] << "'";
-      throw TypeCheckingExceptionPrivate(n, ss.str());
-    }
-    return n[1].getType(check);
-  }
-  inline static bool computeIsConst(NodeManager* nodeManager, TNode n)
-    throw(AssertionException) {
-    Assert(n.getKind() == kind::MU);
-    NodeManagerScope nms(nodeManager);
-    std::vector< TNode > fv;
-    return computeIsConstNode( n, fv );
-  }
-};
-
-
 struct ConstructorProperties {
   inline static Cardinality computeCardinality(TypeNode type) {
     // Constructors aren't exactly functions, they're like
@@ -276,7 +233,6 @@ struct TupleUpdateTypeRule {
     if(check) {
       if(!tupleType.isTuple()) {
         throw TypeCheckingExceptionPrivate(n, "Tuple-update expression formed over non-tuple");
-        tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr());
       }
       if(tu.getIndex() >= tupleType.getTupleLength()) {
         std::stringstream ss;
@@ -313,23 +269,6 @@ struct RecordUpdateTypeRule {
   }
 };/* struct RecordUpdateTypeRule */
 
-struct RecordProperties {
-  inline static Node mkGroundTerm(TypeNode type) {
-    Assert(type.getKind() == kind::RECORD_TYPE);
-    return Node::null();
-  }
-  inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
-    return true;
-  }
-  inline static Cardinality computeCardinality(TypeNode type) {
-    Cardinality card(1);
-    return card;
-  }
-  inline static bool isWellFounded(TypeNode type) {
-    return true;
-  }
-};/* struct RecordProperties */
-
 class DtSizeTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 1f30498d6..2cf72e8e9 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -177,92 +177,6 @@ public:
 
 };/* DatatypesEnumerator */
 
-
-class RecordEnumerator : public TypeEnumeratorBase<RecordEnumerator> {
-  TypeEnumeratorProperties * d_tep;
-  TypeEnumerator** d_enumerators;
-
-  /** Allocate and initialize the delegate enumerators */
-  void newEnumerators() {
-    const Record& rec = getType().getConst<Record>();
-    d_enumerators = new TypeEnumerator*[rec.getNumFields()];
-    for(size_t i = 0; i < rec.getNumFields(); ++i) {
-      d_enumerators[i] = new TypeEnumerator(TypeNode::fromType(rec[i].second));
-    }
-  }
-
-  void deleteEnumerators() throw() {
-    if(d_enumerators != NULL) {
-      const Record& rec = getType().getConst<Record>();
-      for(size_t i = 0; i < rec.getNumFields(); ++i) {
-        delete d_enumerators[i];
-      }
-      delete [] d_enumerators;
-      d_enumerators = NULL;
-    }
-  }
-
-public:
-
-  RecordEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() :
-    TypeEnumeratorBase<RecordEnumerator>(type), d_tep(tep) {
-    Assert(type.isRecord());
-    newEnumerators();
-  }
-
-  RecordEnumerator(const RecordEnumerator& re) throw() :
-    TypeEnumeratorBase<RecordEnumerator>(re.getType()),
-    d_tep(re.d_tep),
-    d_enumerators(NULL) {
-
-    if(re.d_enumerators != NULL) {
-      newEnumerators();
-      for(size_t i = 0; i < getType().getNumChildren(); ++i) {
-        *d_enumerators[i] = TypeEnumerator(*re.d_enumerators[i]);
-      }
-    }
-  }
-
-  virtual ~RecordEnumerator() throw() {
-    deleteEnumerators();
-  }
-
-  Node operator*() throw(NoMoreValuesException) {
-    if(isFinished()) {
-      throw NoMoreValuesException(getType());
-    }
-
-
-    return Node::null();
-  }
-
-  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/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index afe8cd598..881210d78 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -932,8 +932,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto
       newChildren.push_back( Node::fromExpr( c.getConstructor() ) );
       std::vector< Node > newVars;
       for( unsigned j=0; j<c.getNumArgs(); j++ ){
-        TypeNode tn = TypeNode::fromType( c[j].getSelector().getType() );
-        tn = tn[1];
+        TypeNode tn = TypeNode::fromType( c[j].getRangeType() );
         Node v = NodeManager::currentNM()->mkBoundVar( tn );
         newChildren.push_back( v );
         newVars.push_back( v );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 560f68810..a679ccfa8 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -855,7 +855,7 @@ Node TermDb::getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ) {
 
 void getSelfSel( const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){
   for( unsigned j=0; j<dc.getNumArgs(); j++ ){
-    TypeNode tn = TypeNode::fromType( ((SelectorType)dc[j].getSelector().getType()).getRangeType() );
+    TypeNode tn = TypeNode::fromType( dc[j].getRangeType() );
     std::vector< Node > ssc;
     if( tn==ntn ){
       ssc.push_back( n );
@@ -1050,7 +1050,7 @@ bool TermDb::isClosedEnumerableType( TypeNode tn ) {
       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
       for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
         for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
-          TypeNode ctn = TypeNode::fromType( ((SelectorType)dt[i][j].getSelector().getType()).getRangeType() );
+          TypeNode ctn = TypeNode::fromType( dt[i][j].getRangeType() );
           if( tn!=ctn && !isClosedEnumerableType( ctn ) ){
             ret = false;
             break;