From 9b3c5499d253e964c7bf0239271940ac756a67fb Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 1 Nov 2016 14:23:30 -0500 Subject: [PATCH] Revert change to Datatypes API to return vector of DatatypeTypes, as before. ASAN failures with datatypes should now be mostly fixed. --- src/compat/cvc3_compat.cpp | 3 +-- src/expr/expr_manager_template.cpp | 11 ++++++----- src/expr/expr_manager_template.h | 4 ++-- src/expr/node_manager.h | 2 +- src/parser/cvc/Cvc.g | 4 +--- src/parser/parser.cpp | 8 ++++++-- src/parser/parser.h | 3 ++- src/parser/smt2/Smt2.g | 7 ++----- src/smt/boolean_terms.cpp | 4 ++-- 9 files changed, 23 insertions(+), 23 deletions(-) diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 5de62a458..8c9992164 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -1415,8 +1415,7 @@ void ValidityChecker::dataType(const std::vector& names, } // Make the datatypes. - vector dtts; - d_em->mkMutualDatatypeTypes(dv, dtts); + vector 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 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 datatypes; datatypes.push_back(datatype); - std::vector result; - mkMutualDatatypeTypes(datatypes, result); + std::vector result = mkMutualDatatypeTypes(datatypes); Assert(result.size() == 1); return result.front(); } -void ExprManager::mkMutualDatatypeTypes(std::vector& datatypes, std::vector& dtts) { +std::vector ExprManager::mkMutualDatatypeTypes(std::vector& datatypes) { std::set unresolvedTypes; - return mkMutualDatatypeTypes(datatypes, unresolvedTypes, dtts); + return mkMutualDatatypeTypes(datatypes, unresolvedTypes); } -void ExprManager::mkMutualDatatypeTypes(std::vector& datatypes, std::set& unresolvedTypes, std::vector& dtts) { +std::vector ExprManager::mkMutualDatatypeTypes(std::vector& datatypes, std::set& unresolvedTypes) { NodeManagerScope nms(d_nodeManager); std::map nameResolutions; + std::vector 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& 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& datatypes, std::vector& dtts); + std::vector mkMutualDatatypeTypes(std::vector& 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& datatypes, std::set& unresolvedTypes, std::vector& dtts); + std::vector mkMutualDatatypeTypes(std::vector& datatypes, std::set& 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&, std::set&, std::vector&); + friend std::vector ExprManager::mkMutualDatatypeTypes(std::vector&, std::set&); /** Predicate for use with STL algorithms */ struct NodeValueReferenceCountNonZero { 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 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& datatypes, std::vector& types) { +std::vector +Parser::mkMutualDatatypeTypes(std::vector& datatypes) { try { - d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved, types); + std::vector types = + d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved); assert(datatypes.size() == types.size()); @@ -371,6 +373,8 @@ void Parser::mkMutualDatatypeTypes(std::vector& 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& datatypes, std::vector& dtts); + std::vector + mkMutualDatatypeTypes(std::vector& 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 datatypeTypes; - PARSER_STATE->mkMutualDatatypeTypes(datatypes, datatypeTypes); + std::vector datatypeTypes = PARSER_STATE->mkMutualDatatypeTypes(datatypes); seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes)); std::map evals; if( sorts[0]!=range ){ @@ -1326,7 +1325,6 @@ extendedCommand[CVC4::Command*& cmd] datatypesDefCommand[bool isCo, CVC4::Command*& cmd] @declarations { std::vector dts; - std::vector dtts; std::string name; std::vector 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 0771cfc06..51ae0fd11 100644 --- 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 newDttVector; - NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(newDtVector, unresolvedTypes, newDttVector); + vector newDttVector = + NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(newDtVector, unresolvedTypes); DatatypeType& newDtt = newDttVector.front(); const Datatype& newD = newDtt.getDatatype(); for(c = dt.begin(); c != dt.end(); ++c) { -- 2.30.2