Revert change to Datatypes API to return vector of DatatypeTypes, as before. ASAN failures with datatypes should now be mostly fixed.

3 files changed, 9 insertions, 8 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index d36ff5a3d..1eb94140d 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -650,20 +650,20 @@ DatatypeType ExprManager::mkDatatypeType(Datatype& datatype) {
   // code anyway.
   vector<Datatype> datatypes;
   datatypes.push_back(datatype);
-  std::vector<DatatypeType> result;
-  mkMutualDatatypeTypes(datatypes, result);
+  std::vector<DatatypeType> result = mkMutualDatatypeTypes(datatypes);
   Assert(result.size() == 1);
   return result.front();
 }
 
-void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, std::vector<DatatypeType>& dtts) {
+std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(std::vector<Datatype>& datatypes) {
   std::set<Type> unresolvedTypes;
-  return mkMutualDatatypeTypes(datatypes, unresolvedTypes, dtts);
+  return mkMutualDatatypeTypes(datatypes, unresolvedTypes);
 }
 
-void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, std::set<Type>& unresolvedTypes, std::vector<DatatypeType>& dtts) {
+std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, std::set<Type>& unresolvedTypes) {
   NodeManagerScope nms(d_nodeManager);
   std::map<std::string, DatatypeType> nameResolutions;
+  std::vector<DatatypeType> dtts;
 
   Trace("ajr-temp") << "Build datatypes..." << std::endl;
   //have to build deep copy so that datatypes will live in NodeManager
@@ -778,6 +778,7 @@ void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, std::s
   }
 
   Trace("ajr-temp") << "Finish..." << std::endl;
+  return dtts;
 }
 
 void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index d08c53e3d..ed9247e5e 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -380,7 +380,7 @@ public:
    * Make a set of types representing the given datatypes, which may be
    * mutually recursive.
    */
-  void mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, std::vector<DatatypeType>& dtts);
+  std::vector<DatatypeType> mkMutualDatatypeTypes(std::vector<Datatype>& datatypes);
 
   /**
    * 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);
+  std::vector<DatatypeType> mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, std::set<Type>& unresolvedTypes);
 
   /**
    * Make a type representing a constructor with the given parameterization.
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 5e6fcf3d3..0b3830f4b 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 std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(std::vector<Datatype>&, std::set<Type>&);
 
   /** Predicate for use with STL algorithms */
   struct NodeValueReferenceCountNonZero {