Revert change to datatypes API for passing pointers, instead make deep copy during call to mkMutualDatatypes.

4 files changed, 21 insertions, 21 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 525f8ead3..d36ff5a3d 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -645,10 +645,10 @@ SetType ExprManager::mkSetType(Type elementType) const {
   return SetType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSetType(*elementType.d_typeNode))));
 }
 
-DatatypeType ExprManager::mkDatatypeType(Datatype*& datatype) {
+DatatypeType ExprManager::mkDatatypeType(Datatype& datatype) {
   // Not worth a special implementation; this doesn't need to be fast
   // code anyway.
-  vector<Datatype*> datatypes;
+  vector<Datatype> datatypes;
   datatypes.push_back(datatype);
   std::vector<DatatypeType> result;
   mkMutualDatatypeTypes(datatypes, result);
@@ -656,28 +656,28 @@ DatatypeType ExprManager::mkDatatypeType(Datatype*& datatype) {
   return result.front();
 }
 
-void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::vector<DatatypeType>& dtts) {
+void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, std::vector<DatatypeType>& dtts) {
   std::set<Type> unresolvedTypes;
   return mkMutualDatatypeTypes(datatypes, unresolvedTypes, dtts);
 }
 
-void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::set<Type>& unresolvedTypes, std::vector<DatatypeType>& dtts) {
+void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, std::set<Type>& unresolvedTypes, std::vector<DatatypeType>& dtts) {
   NodeManagerScope nms(d_nodeManager);
   std::map<std::string, DatatypeType> nameResolutions;
 
   Trace("ajr-temp") << "Build datatypes..." << std::endl;
-  //std::vector< Datatype* > dt_copies;
-  //for(std::vector<Datatype*>::iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; ++i) {
-  //  dt_copies.push_back( new Datatype( **i ) );
-  //}
-  
+  //have to build deep copy so that datatypes will live in NodeManager
+  std::vector< Datatype* > dt_copies;
+  for(std::vector<Datatype>::iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; ++i) {
+    dt_copies.push_back( new Datatype( *i ) );
+  }
   
   // First do some sanity checks, set up the final Type to be used for
   // each datatype, and set up the "named resolutions" used to handle
   // simple self- and mutual-recursion, for example in the definition
   // "nat = succ(pred:nat) | zero", a named resolution can handle the
   // pred selector.
-  for(std::vector<Datatype*>::iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; ++i) {
+  for(std::vector<Datatype*>::iterator i = dt_copies.begin(), i_end = dt_copies.end(); i != i_end; ++i) {
     TypeNode* typeNode;
     if( (*i)->getNumParameters() == 0 ) {
       unsigned index = d_nodeManager->registerDatatype( *i );
@@ -699,7 +699,7 @@ void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::
     DatatypeType dtt(type);
     PrettyCheckArgument(
         nameResolutions.find((*i)->getName()) == nameResolutions.end(),
-        datatypes,
+        dt_copies,
         "cannot construct two datatypes at the same time "
         "with the same name `%s'",
         (*i)->getName().c_str());
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 3f29396a3..d08c53e3d 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -374,13 +374,13 @@ public:
   SetType mkSetType(Type elementType) const;
 
   /** Make a type representing the given datatype. */
-  DatatypeType mkDatatypeType(Datatype*& datatype);
+  DatatypeType mkDatatypeType(Datatype& datatype);
 
   /**
    * Make a set of types representing the given datatypes, which may be
    * mutually recursive.
    */
-  void mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::vector<DatatypeType>& dtts);
+  void mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, std::vector<DatatypeType>& dtts);
 
   /**
    * Make a set of types representing the given datatypes, which may
@@ -411,7 +411,7 @@ public:
    * then no complicated Type needs to be created, and the above,
    * simpler form of mkMutualDatatypeTypes() is enough.
    */
-  void mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::set<Type>& unresolvedTypes, std::vector<DatatypeType>& dtts);
+  void mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, std::set<Type>& unresolvedTypes, std::vector<DatatypeType>& dtts);
 
   /**
    * Make a type representing a constructor with the given parameterization.
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index af0b1a2d0..2e6792bdd 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -489,15 +489,15 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds)
 TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) {
   if( index==types.size() ){
     if( d_data.isNull() ){
-      Datatype* dt = new Datatype("__cvc4_tuple");
-      dt->setTuple();
+      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);
+      dt.addConstructor(c);
       d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt));
       Debug("tuprec-debug") << "Return type : " << d_data << std::endl;
     }
@@ -511,13 +511,13 @@ TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Recor
   if( index==rec.getNumFields() ){
     if( d_data.isNull() ){
       const Record::FieldVector& fields = rec.getFields();
-      Datatype* dt = new Datatype("__cvc4_record");
-      dt->setRecord();
+      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);
+      dt.addConstructor(c);
       d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt));
       Debug("tuprec-debug") << "Return type : " << d_data << std::endl;
     }
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 9342a02c4..5e6fcf3d3 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -84,7 +84,7 @@ class NodeManager {
   friend Expr ExprManager::mkVar(Type, uint32_t flags);
 
   // friend so it can access NodeManager's d_listeners and notify clients
-  friend void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype*>&, std::set<Type>&, std::vector<DatatypeType>&);
+  friend void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype>&, std::set<Type>&, std::vector<DatatypeType>&);
 
   /** Predicate for use with STL algorithms */
   struct NodeValueReferenceCountNonZero {