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.

1 files changed, 55 insertions, 68 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index e52776fce..e6e44928d 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -461,79 +461,66 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds)
   return TypeNode(mkTypeConst(bounds));
 }
 
-TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
-  Assert(t.isTuple() || t.isRecord());
-
-  //AJR: not sure why .getBaseType() was used in two cases below,
-  //     disabling this, which is necessary to fix bug 605/667,
-  //     which involves records of INT which were mapped to records of REAL below.
-  TypeNode tOrig = t;
-  if(t.isTuple()) {
-    vector<TypeNode> v;
-    bool changed = false;
-    for(size_t i = 0; i < t.getNumChildren(); ++i) {
-      TypeNode tn = t[i];
-      TypeNode base;
-      if(tn.isTuple() || tn.isRecord()) {
-        base = getDatatypeForTupleRecord(tn);
-      } else {
-        base = tn;//.getBaseType();
-      }
-      changed = changed || (tn != base);
-      v.push_back(base);
-    }
-    if(changed) {
-      t = mkTupleType(v);
-    }
-  } else {
-    const Record& r = t.getRecord();
-    std::vector< std::pair<std::string, Type> > v;
-    bool changed = false;
-    const Record::FieldVector& fields = r.getFields();
-    for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
-      Type tn = (*i).second;
-      Type base;
-      if(tn.isTuple() || tn.isRecord()) {
-        base = getDatatypeForTupleRecord(TypeNode::fromType(tn)).toType();
-      } else {
-        base = tn;//.getBaseType();
-      }
-      changed = changed || (tn != base);
-      v.push_back(std::make_pair((*i).first, base));
-    }
-    if(changed) {
-      t = mkRecordType(Record(v));
+TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
+  std::vector< TypeNode > ts;
+  Debug("tuprec-debug") << "Make tuple type : ";
+  for (unsigned i = 0; i < types.size(); ++ i) {
+    CheckArgument(!types[i].isFunctionLike(), types, "cannot put function-like types in tuples");
+    ts.push_back( types[i] );
+    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;
+}
 
-  // if the type doesn't have an associated datatype, then make one for it
-  TypeNode& dtt = d_tupleAndRecordTypes[t];
+TypeNode NodeManager::mkRecordType(const Record& rec) {
+  //index based on type constant
+  TypeNode tindex = mkTypeConst(rec);
+  TypeNode& dtt = d_tupleAndRecordTypes[tindex];
   if(dtt.isNull()) {
-    if(t.isTuple()) {
-      Datatype dt("__cvc4_tuple");
-      DatatypeConstructor c("__cvc4_tuple_ctor");
-      for(TypeNode::const_iterator i = t.begin(); i != t.end(); ++i) {
-        c.addArg("__cvc4_tuple_stor", (*i).toType());
-      }
-      dt.addConstructor(c);
-      dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt));
-      Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl;
-      dtt.setAttribute(DatatypeTupleAttr(), tOrig);
-    } else {
-      const Record& rec = t.getRecord();
-      const Record::FieldVector& fields = rec.getFields();
-      Datatype dt("__cvc4_record");
-      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));
-      Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl;
-      dtt.setAttribute(DatatypeRecordAttr(), tOrig);
+    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);
     }
-  } else {
-    Debug("tuprec") << "REUSING cached " << t << ": " << dtt << std::endl;
+    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;