More simplification to internal implementation of tuples and records.

7 files changed, 140 insertions, 173 deletions

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();