diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-01 13:20:49 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-01 13:20:49 -0500 |
commit | 8e0fce94790249ff7aff84ff4500bb96e2ebb9e9 (patch) | |
tree | 25e65718cff712f13688e452ffc1d4b459cd7367 /src/expr | |
parent | 3506b13f4d298095e8405b32b05e838f17dbe809 (diff) |
Working memory leak free version, changes interface to pointers.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/datatype.cpp | 4 | ||||
-rw-r--r-- | src/expr/datatype.h | 9 | ||||
-rw-r--r-- | src/expr/datatype.i | 14 | ||||
-rw-r--r-- | src/expr/expr.i | 2 | ||||
-rw-r--r-- | src/expr/expr_manager.i | 2 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 64 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 12 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 28 | ||||
-rw-r--r-- | src/expr/node_manager.h | 7 | ||||
-rw-r--r-- | src/expr/type.cpp | 2 | ||||
-rw-r--r-- | src/expr/type_node.h | 4 |
11 files changed, 100 insertions, 48 deletions
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index a7039110f..26ab2f2da 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -52,6 +52,7 @@ typedef expr::Attribute<expr::attr::DatatypeUFiniteTag, bool> DatatypeUFiniteAtt typedef expr::Attribute<expr::attr::DatatypeUFiniteComputedTag, bool> DatatypeUFiniteComputedAttr; Datatype::~Datatype(){ + Trace("ajr-temp") << "delete datatype " << getName() << " " << this << std::endl; delete d_record; } @@ -1109,5 +1110,8 @@ DatatypeIndexConstant::DatatypeIndexConstant(unsigned index) throw(IllegalArgume } +std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic) { + return out << "index_" << dic.getIndex(); +} }/* CVC4 namespace */ diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 06735262d..f81d2358d 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -28,7 +28,8 @@ namespace CVC4 { // messy; Expr needs Datatype (because it's the payload of a // CONSTANT-kinded expression), and Datatype needs Expr. - class CVC4_PUBLIC Datatype; + //class CVC4_PUBLIC Datatype; + class CVC4_PUBLIC DatatypeIndexConstant; }/* CVC4 namespace */ #include "base/exception.h" @@ -792,9 +793,11 @@ private: const unsigned d_index; };/* class DatatypeIndexConstant */ +std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic) CVC4_PUBLIC; + struct CVC4_PUBLIC DatatypeIndexConstantHashFunction { - inline size_t operator()(const DatatypeIndexConstant& uc) const { - return IntegerHashFunction()(uc.getIndex()); + inline size_t operator()(const DatatypeIndexConstant& dic) const { + return IntegerHashFunction()(dic.getIndex()); } };/* struct DatatypeIndexConstantHashFunction */ diff --git a/src/expr/datatype.i b/src/expr/datatype.i index a7456df38..a903e0241 100644 --- a/src/expr/datatype.i +++ b/src/expr/datatype.i @@ -75,6 +75,20 @@ %feature("valuewrapper") CVC4::DatatypeUnresolvedType; %feature("valuewrapper") CVC4::DatatypeConstructor; + +%rename(equals) CVC4::DatatypeIndexConstant::operator==(const DatatypeIndexConstant&) const; +%ignore CVC4::DatatypeIndexConstant::operator!=(const DatatypeIndexConstant&) const; + +%rename(less) CVC4::DatatypeIndexConstant::operator<(const DatatypeIndexConstant&) const; +%rename(lessEqual) CVC4::DatatypeIndexConstant::operator<=(const DatatypeIndexConstant&) const; +%rename(greater) CVC4::DatatypeIndexConstant::operator>(const DatatypeIndexConstant&) const; +%rename(greaterEqual) CVC4::DatatypeIndexConstant::operator>=(const DatatypeIndexConstant&) const; + +%rename(apply) CVC4::DatatypeIndexConstantFunction::operator()(const DatatypeIndexConstant&) const; + +%ignore CVC4::operator<<(std::ostream& out, const DatatypeIndexConstant& es); + + #ifdef SWIGJAVA // Instead of Datatype::begin() and end(), create an diff --git a/src/expr/expr.i b/src/expr/expr.i index 354cacdc0..49cb24321 100644 --- a/src/expr/expr.i +++ b/src/expr/expr.i @@ -150,7 +150,7 @@ namespace CVC4 { %template(getConstBitVectorRotateRight) CVC4::Expr::getConst<CVC4::BitVectorRotateRight>; %template(getConstUninterpretedConstant) CVC4::Expr::getConst<CVC4::UninterpretedConstant>; %template(getConstKind) CVC4::Expr::getConst<CVC4::kind::Kind_t>; -%template(getConstDatatype) CVC4::Expr::getConst<CVC4::Datatype>; +%template(getConstDatatypeIndexConstant) CVC4::Expr::getConst<CVC4::DatatypeIndexConstant>; %template(getConstRational) CVC4::Expr::getConst<CVC4::Rational>; %template(getConstBitVector) CVC4::Expr::getConst<CVC4::BitVector>; %template(getConstPredicate) CVC4::Expr::getConst<CVC4::Predicate>; diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i index 11c1e284d..f8bb55523 100644 --- a/src/expr/expr_manager.i +++ b/src/expr/expr_manager.i @@ -65,7 +65,7 @@ //%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToSBV>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::UninterpretedConstant>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::kind::Kind_t>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Datatype>; +%template(mkConst) CVC4::ExprManager::mkConst<CVC4::DatatypeIndexConstant>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleUpdate>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordUpdate>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::Rational>; diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 6d8497a60..525f8ead3 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -645,46 +645,52 @@ SetType ExprManager::mkSetType(Type elementType) const { return SetType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSetType(*elementType.d_typeNode)))); } -DatatypeType ExprManager::mkDatatypeType(const 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); - vector<DatatypeType> result = mkMutualDatatypeTypes(datatypes); + std::vector<DatatypeType> result; + mkMutualDatatypeTypes(datatypes, result); Assert(result.size() == 1); return result.front(); } -std::vector<DatatypeType> -ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { - return mkMutualDatatypeTypes(datatypes, set<Type>()); +void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::vector<DatatypeType>& dtts) { + std::set<Type> unresolvedTypes; + return mkMutualDatatypeTypes(datatypes, unresolvedTypes, dtts); } -std::vector<DatatypeType> -ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes, - const std::set<Type>& unresolvedTypes) { +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; - std::vector<DatatypeType> dtts; + 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 ) ); + //} + + // 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>::const_iterator i = datatypes.begin(), - i_end = datatypes.end(); - i != i_end; - ++i) { + for(std::vector<Datatype*>::iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; ++i) { TypeNode* typeNode; - if( (*i).getNumParameters() == 0 ) { - typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i)); + if( (*i)->getNumParameters() == 0 ) { + unsigned index = d_nodeManager->registerDatatype( *i ); + typeNode = new TypeNode(d_nodeManager->mkTypeConst(DatatypeIndexConstant(index))); + //typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i)); } else { - TypeNode cons = d_nodeManager->mkTypeConst(*i); + unsigned index = d_nodeManager->registerDatatype( *i ); + TypeNode cons = d_nodeManager->mkTypeConst(DatatypeIndexConstant(index)); + //TypeNode cons = d_nodeManager->mkTypeConst(*i); std::vector< TypeNode > params; params.push_back( cons ); - for( unsigned int ip = 0; ip < (*i).getNumParameters(); ++ip ) { - params.push_back( TypeNode::fromType( (*i).getParameter( ip ) ) ); + for( unsigned int ip = 0; ip < (*i)->getNumParameters(); ++ip ) { + params.push_back( TypeNode::fromType( (*i)->getParameter( ip ) ) ); } typeNode = new TypeNode(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, params)); @@ -692,15 +698,19 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes, Type type(d_nodeManager, typeNode); DatatypeType dtt(type); PrettyCheckArgument( - nameResolutions.find((*i).getName()) == nameResolutions.end(), + nameResolutions.find((*i)->getName()) == nameResolutions.end(), datatypes, "cannot construct two datatypes at the same time " "with the same name `%s'", - (*i).getName().c_str()); - nameResolutions.insert(std::make_pair((*i).getName(), dtt)); + (*i)->getName().c_str()); + nameResolutions.insert(std::make_pair((*i)->getName(), dtt)); dtts.push_back(dtt); + //d_keep_dtt.push_back(dtt); + //d_keep_dt.push_back(*i); + //Assert( dtt.getDatatype()==(*i) ); } + Trace("ajr-temp") << "Set up map..." << std::endl; // Second, set up the type substitution map for complex type // resolution (e.g. if "list" is the type we're defining, and it has // a selector of type "ARRAY INT OF list", this can't be taken care @@ -714,10 +724,7 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes, std::vector< DatatypeType > paramReplacements; std::vector<Type> placeholders;// to hold the "unresolved placeholders" std::vector<Type> replacements;// to hold our final, resolved types - for(std::set<Type>::const_iterator i = unresolvedTypes.begin(), - i_end = unresolvedTypes.end(); - i != i_end; - ++i) { + for(std::set<Type>::iterator i = unresolvedTypes.begin(), i_end = unresolvedTypes.end(); i != i_end; ++i) { std::string name; if( (*i).isSort() ) { name = SortType(*i).getName(); @@ -746,12 +753,14 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes, } } + Trace("ajr-temp") << "Resolve..." << std::endl; // Lastly, perform the final resolutions and checks. for(std::vector<DatatypeType>::iterator i = dtts.begin(), i_end = dtts.end(); i != i_end; ++i) { const Datatype& dt = (*i).getDatatype(); + Trace("ajr-temp") << "Resolve " << dt.getName() << std::endl; if(!dt.isResolved()) { const_cast<Datatype&>(dt).resolve(this, nameResolutions, placeholders, replacements, @@ -763,11 +772,12 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes, checkResolvedDatatype(*i); } + Trace("ajr-temp") << "Notify..." << std::endl; for(std::vector<NodeManagerListener*>::iterator i = d_nodeManager->d_listeners.begin(); i != d_nodeManager->d_listeners.end(); ++i) { (*i)->nmNotifyNewDatatypes(dtts); } - return dtts; + Trace("ajr-temp") << "Finish..." << std::endl; } void ExprManager::checkResolvedDatatype(DatatypeType dtt) const { diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 95b9c60bf..3f29396a3 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -87,6 +87,9 @@ private: ExprManager(const ExprManager&) CVC4_UNDEFINED; ExprManager& operator=(const ExprManager&) CVC4_UNDEFINED; + std::vector<DatatypeType> d_keep_dtt; + std::vector<Datatype> d_keep_dt; + public: /** @@ -371,14 +374,13 @@ public: SetType mkSetType(Type elementType) const; /** Make a type representing the given datatype. */ - DatatypeType mkDatatypeType(const Datatype& datatype); + DatatypeType mkDatatypeType(Datatype*& datatype); /** * Make a set of types representing the given datatypes, which may be * mutually recursive. */ - std::vector<DatatypeType> - mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes); + void mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::vector<DatatypeType>& dtts); /** * Make a set of types representing the given datatypes, which may @@ -409,9 +411,7 @@ public: * then no complicated Type needs to be created, and the above, * simpler form of mkMutualDatatypeTypes() is enough. */ - std::vector<DatatypeType> - mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes, - const std::set<Type>& unresolvedTypes); + 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 af4f89da1..af0b1a2d0 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -172,9 +172,11 @@ NodeManager::~NodeManager() { d_unique_vars.clear(); - //d_tupleAndRecordTypes.clear(); + TypeNode dummy; d_tt_cache.d_children.clear(); + d_tt_cache.d_data = dummy; d_rt_cache.d_children.clear(); + d_rt_cache.d_data = dummy; for( std::vector<Datatype*>::iterator datatype_iter = d_ownedDatatypes.begin(), datatype_end = d_ownedDatatypes.end(); datatype_iter != datatype_end; ++datatype_iter) { @@ -217,6 +219,18 @@ NodeManager::~NodeManager() { d_options = NULL; } +unsigned NodeManager::registerDatatype(Datatype* dt) { + Trace("ajr-temp") << "Register datatype : " << dt->getName() << " " << dt << std::endl; + unsigned sz = d_ownedDatatypes.size(); + d_ownedDatatypes.push_back( dt ); + return sz; +} + +const Datatype & NodeManager::getDatatypeForIndex( unsigned index ) const{ + Assert( index<d_ownedDatatypes.size() ); + return *d_ownedDatatypes[index]; +} + void NodeManager::reclaimZombies() { // FIXME multithreading Assert(!d_attrManager->inGarbageCollection()); @@ -475,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("__cvc4_tuple"); - dt.setTuple(); + Datatype* dt = new Datatype("__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; } @@ -497,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("__cvc4_record"); - dt.setRecord(); + Datatype* dt = new Datatype("__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 aa78c9627..9342a02c4 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 std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>&, const std::set<Type>&); + friend void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype*>&, std::set<Type>&, std::vector<DatatypeType>&); /** Predicate for use with STL algorithms */ struct NodeValueReferenceCountNonZero { @@ -380,6 +380,11 @@ public: Assert(elt != d_listeners.end(), "listener not subscribed"); d_listeners.erase(elt); } + + /** register datatype */ + unsigned registerDatatype(Datatype* dt); + /** get datatype for index */ + const Datatype & getDatatypeForIndex( unsigned index ) const; /** Get a Kind from an operator expression */ static inline Kind operatorToKind(TNode n); diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 18157016f..11a45db79 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -608,7 +608,7 @@ std::vector<Type> DatatypeType::getParamTypes() const { DatatypeType DatatypeType::instantiate(const std::vector<Type>& params) const { NodeManagerScope nms(d_nodeManager); - TypeNode cons = d_nodeManager->mkTypeConst( getDatatype() ); + TypeNode cons = d_nodeManager->mkTypeConst( (*d_typeNode)[0].getConst<DatatypeIndexConstant>() ); vector<TypeNode> paramsNodes; paramsNodes.push_back( cons ); for(vector<Type>::const_iterator i = params.begin(), diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 0cada0df2..9fffbdeb2 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -1023,7 +1023,9 @@ inline bool TypeNode::isBitVector(unsigned size) const { /** Get the datatype specification from a datatype type */ inline const Datatype& TypeNode::getDatatype() const { Assert(isDatatype()); - return getConst<Datatype>(); + //return getConst<Datatype>(); + DatatypeIndexConstant dic = getConst<DatatypeIndexConstant>(); + return NodeManager::currentNM()->getDatatypeForIndex( dic.getIndex() ); } /** Get the exponent size of this floating-point type */ |