Revert change to Datatypes API to return vector of DatatypeTypes, as before. ASAN...

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 5de62a458ac21114ceb143940e3274f60f72fde6..8c9992164e0461ceca78987ecce94fafa2fc5771 100644 (file)
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -1415,8 +1415,7 @@ void ValidityChecker::dataType(const std::vector<std::string>& names,
   }
 
   // Make the datatypes.
-  vector<CVC4::DatatypeType> dtts; 
-  d_em->mkMutualDatatypeTypes(dv, dtts);
+  vector<CVC4::DatatypeType> dtts = d_em->mkMutualDatatypeTypes(dv);
 
   // Post-process to register the names of everything with this validity checker.
   // This is necessary for the compatibility layer because cons/sel operations are

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index d36ff5a3ddd260d25ad583d431012f9612267eed..1eb94140d3ab174c8725303ff922bddcb708b944 100644 (file)
--- 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 d08c53e3dba5ee0b82051227af70d9151a3a3c56..ed9247e5e843de7b7751e6c52716a6e533f75f7f 100644 (file)
--- 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 5e6fcf3d39f3bf9b58271e9f88dcc98ecdc4f5b2..0b3830f4b01e1b7a802427004e9e097de6c9f184 100644 (file)
--- 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 {

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 8c5d972548a16f4a92fc8e382f0cba59e85f3568..e6d7f9d86fd0961e487107a17ce8fab7e1a330e4 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -769,9 +769,7 @@ mainCommand[CVC4::Command*& cmd]
     ( COMMA datatypeDef[dts] )*
     END_TOK
     { PARSER_STATE->popScope();
-      std::vector<DatatypeType> dtts;
-      PARSER_STATE->mkMutualDatatypeTypes(dts, dtts);
-      cmd = new DatatypeDeclarationCommand(dtts); }
+      cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
 
   | CONTEXT_TOK
     ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index cef8c4be4690a50e2372a2dddae1482062456c75..c3c533576c8d61a9dd45de0b78bb0e677396677f 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -303,10 +303,12 @@ bool Parser::isUnresolvedType(const std::string& name) {
   return d_unresolved.find(getSort(name)) != d_unresolved.end();
 }
 
-void Parser::mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, std::vector<DatatypeType>& types) {
+std::vector<DatatypeType>
+Parser::mkMutualDatatypeTypes(std::vector<Datatype>& datatypes) {
 
   try {
-    d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved, types);
+    std::vector<DatatypeType> types =
+      d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
 
     assert(datatypes.size() == types.size());
 
@@ -371,6 +373,8 @@ void Parser::mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, std::vector
         throw ParserException(dt.getName() + " is not well-founded");
       }
     }
+    
+    return types;
   } catch(IllegalArgumentException& ie) {
     throw ParserException(ie.getMessage());
   }

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 7c9870edbbc400549d18cb4fd38066d07d7b4ad0..351aa858abb4b0081d15c5a7a3caa78a3cf9cf66 100644 (file)
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -501,7 +501,8 @@ public:
   /**
    * Create sorts of mutually-recursive datatypes.
    */
-  void mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, std::vector<DatatypeType>& dtts);
+  std::vector<DatatypeType>
+  mkMutualDatatypeTypes(std::vector<Datatype>& datatypes);
 
   /**
    * Add an operator to the current legal set.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 3bd308559c026293b4075d00bd84999797238f8a..f88b302123880530c8d9b1bf98190bbe70fc911d 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -640,8 +640,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
         Debug("parser-sygus") << "  " << i << " : " << datatypes[i].getName() << std::endl;
       }
       seq = new CommandSequence();
-      std::vector<DatatypeType> datatypeTypes; 
-      PARSER_STATE->mkMutualDatatypeTypes(datatypes, datatypeTypes);
+      std::vector<DatatypeType> datatypeTypes = PARSER_STATE->mkMutualDatatypeTypes(datatypes);
       seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes));
       std::map<DatatypeType, Expr> evals;
       if( sorts[0]!=range ){
@@ -1326,7 +1325,6 @@ extendedCommand[CVC4::Command*& cmd]
 datatypesDefCommand[bool isCo, CVC4::Command*& cmd]
 @declarations {
   std::vector<CVC4::Datatype> dts;
-  std::vector<CVC4::DatatypeType> dtts;
   std::string name;
   std::vector<Type> sorts;
 }
@@ -1340,8 +1338,7 @@ datatypesDefCommand[bool isCo, CVC4::Command*& cmd]
   RPAREN_TOK
   LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK
   { PARSER_STATE->popScope();
-    PARSER_STATE->mkMutualDatatypeTypes(dts, dtts);
-    cmd = new DatatypeDeclarationCommand(dtts); }
+    cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
   ;
 
 rewriterulesCommand[CVC4::Command*& cmd]

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 0771cfc064862b65a9fd5d61084e8a0cdc716533..51ae0fd11b35128b73c4223496481adadc109d95 100644 (file)
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -288,8 +288,8 @@ const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw(
           }
           newDt.addConstructor(ctor);
         }
-        vector<DatatypeType> newDttVector;
-        NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(newDtVector, unresolvedTypes, newDttVector);
+        vector<DatatypeType> newDttVector =
+          NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(newDtVector, unresolvedTypes);
         DatatypeType& newDtt = newDttVector.front();
         const Datatype& newD = newDtt.getDatatype();
         for(c = dt.begin(); c != dt.end(); ++c) {