diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-01 13:33:38 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-01 13:33:38 -0500 |
commit | f4c783f97201753bf63c70c5c16b7861a236d57c (patch) | |
tree | 8e4a9e85d7485200bdfb52b5afc5032993938488 /src/expr | |
parent | 8e0fce94790249ff7aff84ff4500bb96e2ebb9e9 (diff) |
Revert change to datatypes API for passing pointers, instead make deep copy during call to mkMutualDatatypes.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 22 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 6 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 12 | ||||
-rw-r--r-- | src/expr/node_manager.h | 2 |
4 files changed, 21 insertions, 21 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 525f8ead3..d36ff5a3d 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -645,10 +645,10 @@ SetType ExprManager::mkSetType(Type elementType) const { return SetType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSetType(*elementType.d_typeNode)))); } -DatatypeType ExprManager::mkDatatypeType(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); std::vector<DatatypeType> result; mkMutualDatatypeTypes(datatypes, result); @@ -656,28 +656,28 @@ DatatypeType ExprManager::mkDatatypeType(Datatype*& datatype) { return result.front(); } -void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::vector<DatatypeType>& dtts) { +void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, std::vector<DatatypeType>& dtts) { std::set<Type> unresolvedTypes; return mkMutualDatatypeTypes(datatypes, unresolvedTypes, dtts); } -void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::set<Type>& unresolvedTypes, std::vector<DatatypeType>& dtts) { +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; 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 ) ); - //} - + //have to build deep copy so that datatypes will live in NodeManager + 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*>::iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; ++i) { + for(std::vector<Datatype*>::iterator i = dt_copies.begin(), i_end = dt_copies.end(); i != i_end; ++i) { TypeNode* typeNode; if( (*i)->getNumParameters() == 0 ) { unsigned index = d_nodeManager->registerDatatype( *i ); @@ -699,7 +699,7 @@ void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std:: DatatypeType dtt(type); PrettyCheckArgument( nameResolutions.find((*i)->getName()) == nameResolutions.end(), - datatypes, + dt_copies, "cannot construct two datatypes at the same time " "with the same name `%s'", (*i)->getName().c_str()); diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 3f29396a3..d08c53e3d 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -374,13 +374,13 @@ public: SetType mkSetType(Type elementType) const; /** Make a type representing the given datatype. */ - DatatypeType mkDatatypeType(Datatype*& datatype); + DatatypeType mkDatatypeType(Datatype& datatype); /** * Make a set of types representing the given datatypes, which may be * mutually recursive. */ - void mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::vector<DatatypeType>& dtts); + void mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, std::vector<DatatypeType>& dtts); /** * 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); + void mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, std::set<Type>& unresolvedTypes, std::vector<DatatypeType>& dtts); /** * Make a type representing a constructor with the given parameterization. diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index af0b1a2d0..2e6792bdd 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -489,15 +489,15 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds) TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) { if( index==types.size() ){ if( d_data.isNull() ){ - Datatype* dt = new Datatype("__cvc4_tuple"); - dt->setTuple(); + Datatype dt("__cvc4_tuple"); + dt.setTuple(); DatatypeConstructor c("__cvc4_tuple_ctor"); for (unsigned i = 0; i < types.size(); ++ i) { std::stringstream ss; ss << "__cvc4_tuple_stor_" << i; c.addArg(ss.str().c_str(), types[i].toType()); } - dt->addConstructor(c); + dt.addConstructor(c); d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt)); Debug("tuprec-debug") << "Return type : " << d_data << std::endl; } @@ -511,13 +511,13 @@ TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Recor if( index==rec.getNumFields() ){ if( d_data.isNull() ){ const Record::FieldVector& fields = rec.getFields(); - Datatype* dt = new Datatype("__cvc4_record"); - dt->setRecord(); + Datatype dt("__cvc4_record"); + dt.setRecord(); DatatypeConstructor c("__cvc4_record_ctor"); for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) { c.addArg((*i).first, (*i).second); } - dt->addConstructor(c); + dt.addConstructor(c); d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt)); Debug("tuprec-debug") << "Return type : " << d_data << std::endl; } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 9342a02c4..5e6fcf3d3 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 void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype>&, std::set<Type>&, std::vector<DatatypeType>&); /** Predicate for use with STL algorithms */ struct NodeValueReferenceCountNonZero { |