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

4 files changed, 11 insertions, 11 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 8c5d97254..e6d7f9d86 100644
--- 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 cef8c4be4..c3c533576 100644
--- 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 7c9870edb..351aa858a 100644
--- 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 3bd308559..f88b30212 100644
--- 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]