1 files changed, 37 insertions, 27 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 6d8497a60..525f8ead3 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -645,46 +645,52 @@ SetType ExprManager::mkSetType(Type elementType) const {
   return SetType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSetType(*elementType.d_typeNode))));
 }
 
-DatatypeType ExprManager::mkDatatypeType(const 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);
-  vector<DatatypeType> result = mkMutualDatatypeTypes(datatypes);
+  std::vector<DatatypeType> result;
+  mkMutualDatatypeTypes(datatypes, result);
   Assert(result.size() == 1);
   return result.front();
 }
 
-std::vector<DatatypeType>
-ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
-  return mkMutualDatatypeTypes(datatypes, set<Type>());
+void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::vector<DatatypeType>& dtts) {
+  std::set<Type> unresolvedTypes;
+  return mkMutualDatatypeTypes(datatypes, unresolvedTypes, dtts);
 }
 
-std::vector<DatatypeType>
-ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
-                                   const std::set<Type>& unresolvedTypes) {
+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;
-  std::vector<DatatypeType> dtts;
 
+  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 ) );
+  //}
+  
+  
   // 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>::const_iterator i = datatypes.begin(),
-        i_end = datatypes.end();
-      i != i_end;
-      ++i) {
+  for(std::vector<Datatype*>::iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; ++i) {
     TypeNode* typeNode;
-    if( (*i).getNumParameters() == 0 ) {
-      typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i));
+    if( (*i)->getNumParameters() == 0 ) {
+      unsigned index = d_nodeManager->registerDatatype( *i );
+      typeNode = new TypeNode(d_nodeManager->mkTypeConst(DatatypeIndexConstant(index)));
+      //typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i));
     } else {
-      TypeNode cons = d_nodeManager->mkTypeConst(*i);
+      unsigned index = d_nodeManager->registerDatatype( *i );
+      TypeNode cons = d_nodeManager->mkTypeConst(DatatypeIndexConstant(index));
+      //TypeNode cons = d_nodeManager->mkTypeConst(*i);
       std::vector< TypeNode > params;
       params.push_back( cons );
-      for( unsigned int ip = 0; ip < (*i).getNumParameters(); ++ip ) {
-        params.push_back( TypeNode::fromType( (*i).getParameter( ip ) ) );
+      for( unsigned int ip = 0; ip < (*i)->getNumParameters(); ++ip ) {
+        params.push_back( TypeNode::fromType( (*i)->getParameter( ip ) ) );
       }
 
       typeNode = new TypeNode(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, params));
@@ -692,15 +698,19 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
     Type type(d_nodeManager, typeNode);
     DatatypeType dtt(type);
     PrettyCheckArgument(
-        nameResolutions.find((*i).getName()) == nameResolutions.end(),
+        nameResolutions.find((*i)->getName()) == nameResolutions.end(),
         datatypes,
         "cannot construct two datatypes at the same time "
         "with the same name `%s'",
-        (*i).getName().c_str());
-    nameResolutions.insert(std::make_pair((*i).getName(), dtt));
+        (*i)->getName().c_str());
+    nameResolutions.insert(std::make_pair((*i)->getName(), dtt));
     dtts.push_back(dtt);
+    //d_keep_dtt.push_back(dtt);
+    //d_keep_dt.push_back(*i);
+    //Assert( dtt.getDatatype()==(*i) );
   }
 
+  Trace("ajr-temp") << "Set up map..." << std::endl;
   // Second, set up the type substitution map for complex type
   // resolution (e.g. if "list" is the type we're defining, and it has
   // a selector of type "ARRAY INT OF list", this can't be taken care
@@ -714,10 +724,7 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
   std::vector< DatatypeType > paramReplacements;
   std::vector<Type> placeholders;// to hold the "unresolved placeholders"
   std::vector<Type> replacements;// to hold our final, resolved types
-  for(std::set<Type>::const_iterator i = unresolvedTypes.begin(),
-        i_end = unresolvedTypes.end();
-      i != i_end;
-      ++i) {
+  for(std::set<Type>::iterator i = unresolvedTypes.begin(), i_end = unresolvedTypes.end(); i != i_end; ++i) {
     std::string name;
     if( (*i).isSort() ) {
       name = SortType(*i).getName();
@@ -746,12 +753,14 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
     }
   }
 
+  Trace("ajr-temp") << "Resolve..." << std::endl;
   // Lastly, perform the final resolutions and checks.
   for(std::vector<DatatypeType>::iterator i = dtts.begin(),
         i_end = dtts.end();
       i != i_end;
       ++i) {
     const Datatype& dt = (*i).getDatatype();
+    Trace("ajr-temp") << "Resolve " << dt.getName() << std::endl;
     if(!dt.isResolved()) {
       const_cast<Datatype&>(dt).resolve(this, nameResolutions,
                                         placeholders, replacements,
@@ -763,11 +772,12 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
     checkResolvedDatatype(*i);
   }
 
+  Trace("ajr-temp") << "Notify..." << std::endl;
   for(std::vector<NodeManagerListener*>::iterator i = d_nodeManager->d_listeners.begin(); i != d_nodeManager->d_listeners.end(); ++i) {
     (*i)->nmNotifyNewDatatypes(dtts);
   }
 
-  return dtts;
+  Trace("ajr-temp") << "Finish..." << std::endl;
 }
 
 void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {