diff options
-rw-r--r-- | src/expr/expr_manager_template.cpp | 19 | ||||
-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 | 16 | ||||
-rw-r--r-- | src/expr/type.cpp | 2 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 30 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 3 |
7 files changed, 64 insertions, 46 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 1981d0a7d..8bf8d9e54 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -115,10 +115,11 @@ ExprManager::~ExprManager() } } #endif + // clear the datatypes + d_ownedDatatypes.clear(); delete d_nodeManager; d_nodeManager = NULL; - } catch(Exception& e) { Warning() << "CVC4 threw an exception during cleanup." << std::endl << e << std::endl; @@ -676,10 +677,11 @@ std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes( std::map<std::string, DatatypeType> nameResolutions; std::vector<DatatypeType> dtts; - //have to build deep copy so that datatypes will live in NodeManager + // have to build deep copy so that datatypes will live in this class 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 ) ); + d_ownedDatatypes.push_back(std::unique_ptr<Datatype>(new Datatype(*i))); + dt_copies.push_back(d_ownedDatatypes.back().get()); } // First do some sanity checks, set up the final Type to be used for @@ -689,12 +691,12 @@ std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes( // pred selector. for(std::vector<Datatype*>::iterator i = dt_copies.begin(), i_end = dt_copies.end(); i != i_end; ++i) { TypeNode* typeNode; + // register datatype with the node manager + unsigned index = d_nodeManager->registerDatatype((*i)->d_internal); 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 { - unsigned index = d_nodeManager->registerDatatype( *i ); TypeNode cons = d_nodeManager->mkTypeConst(DatatypeIndexConstant(index)); //TypeNode cons = d_nodeManager->mkTypeConst(*i); std::vector< TypeNode > params; @@ -1098,6 +1100,13 @@ Type ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapColle new TypeNode(expr::exportTypeInternal(*t.d_typeNode, t.d_nodeManager, em->d_nodeManager, vmap))); } +const Datatype& ExprManager::getDatatypeForIndex(unsigned index) const +{ + // when the Node-level API is in place, this function will be deleted. + Assert(index < d_ownedDatatypes.size()); + return *d_ownedDatatypes[index]; +} + ${mkConst_implementations} }/* CVC4 namespace */ diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 44871ff99..c61c7e012 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -79,9 +79,11 @@ private: // undefined, private copy constructor and assignment op (disallow copy) ExprManager(const ExprManager&) = delete; ExprManager& operator=(const ExprManager&) = delete; - -public: + /** A list of datatypes owned by this expr manager. */ + std::vector<std::unique_ptr<Datatype> > d_ownedDatatypes; + + public: /** * Creates an expression manager with default options. */ @@ -571,6 +573,12 @@ public: /** Returns the maximum arity of the given kind. */ static unsigned maxArity(Kind kind); + /** + * Return the datatype at the given index owned by this class. Type nodes are + * associated with datatypes through the DatatypeIndexConstant class. The + * argument index is intended to be a value taken from that class. + */ + const Datatype& getDatatypeForIndex(unsigned index) const; };/* class ExprManager */ ${mkConst_instantiations} diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 0c3f1b4cb..39be675ec 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -187,15 +187,7 @@ NodeManager::~NodeManager() { d_rt_cache.d_children.clear(); d_rt_cache.d_data = dummy; - // TODO: switch to DType - for (std::vector<Datatype*>::iterator - datatype_iter = d_ownedDatatypes.begin(), - datatype_end = d_ownedDatatypes.end(); - datatype_iter != datatype_end; ++datatype_iter) { - Datatype* datatype = *datatype_iter; - delete datatype; - } - d_ownedDatatypes.clear(); + d_ownedDTypes.clear(); Assert(!d_attrManager->inGarbageCollection()); @@ -248,23 +240,17 @@ NodeManager::~NodeManager() { d_options = NULL; } -unsigned NodeManager::registerDatatype(Datatype* dt) { - unsigned sz = d_ownedDatatypes.size(); - d_ownedDatatypes.push_back( dt ); +size_t NodeManager::registerDatatype(std::shared_ptr<DType> dt) +{ + size_t sz = d_ownedDTypes.size(); + d_ownedDTypes.push_back(dt); return sz; } -const Datatype & NodeManager::getDatatypeForIndex( unsigned index ) const{ - // when the Node-level API is in place, this function will be deleted. - Assert(index < d_ownedDatatypes.size()); - return *d_ownedDatatypes[index]; -} - const DType& NodeManager::getDTypeForIndex(unsigned index) const { - const Datatype& d = getDatatypeForIndex(index); - // return its internal representation - return *d.d_internal; + Assert(index < d_ownedDTypes.size()); + return *d_ownedDTypes[index]; } void NodeManager::reclaimZombies() { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 61ef1d39d..eced00c48 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -178,7 +178,7 @@ class NodeManager { std::vector<NodeManagerListener*> d_listeners; /** A list of datatypes owned by this node manager. */ - std::vector<Datatype*> d_ownedDatatypes; + std::vector<std::shared_ptr<DType> > d_ownedDTypes; /** * A map of tuple and record types to their corresponding datatype. @@ -428,9 +428,17 @@ public: } /** register datatype */ - unsigned registerDatatype(Datatype* dt); - /** get datatype for index */ - const Datatype & getDatatypeForIndex( unsigned index ) const; + size_t registerDatatype(std::shared_ptr<DType> dt); + /** + * Return the datatype at the given index owned by this class. Type nodes are + * associated with datatypes through the DatatypeIndexConstant class. The + * argument index is intended to be a value taken from that class. + * + * Type nodes must access their DTypes through a level of indirection to + * prevent cycles in the Node AST (as DTypes themselves contain Nodes), which + * would lead to memory leaks. Thus TypeNode are given a DatatypeIndexConstant + * which is used as an index to retrieve the DType via this call. + */ const DType& getDTypeForIndex(unsigned index) const; /** Get a Kind from an operator expression */ diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 99fe73c22..031dcb3f0 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -576,7 +576,7 @@ const Datatype& DatatypeType::getDatatype() const { if (d_typeNode->getKind() == kind::DATATYPE_TYPE) { DatatypeIndexConstant dic = d_typeNode->getConst<DatatypeIndexConstant>(); - return d_nodeManager->getDatatypeForIndex(dic.getIndex()); + return d_nodeManager->toExprManager()->getDatatypeForIndex(dic.getIndex()); } Assert(d_typeNode->getKind() == kind::PARAMETRIC_DATATYPE); return DatatypeType((*d_typeNode)[0].toType()).getDatatype(); diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 22a491af5..f8448f1e9 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -24,11 +24,12 @@ #include <typeinfo> #include <vector> -#include "expr/expr.h" // for ExprSetDepth etc.. -#include "expr/node_manager_attributes.h" // for VarNameAttr -#include "options/language.h" // for LANG_AST -#include "printer/dagification_visitor.h" +#include "expr/dtype.h" +#include "expr/expr.h" // for ExprSetDepth etc.. +#include "expr/node_manager_attributes.h" // for VarNameAttr +#include "options/language.h" // for LANG_AST #include "options/smt_options.h" +#include "printer/dagification_visitor.h" #include "smt/command.h" #include "smt/smt_engine.h" #include "smt_util/node_visitor.h" @@ -179,7 +180,9 @@ void CvcPrinter::toStream( break; case kind::DATATYPE_TYPE: { - const Datatype& dt = (NodeManager::currentNM()->getDatatypeForIndex( n.getConst< DatatypeIndexConstant >().getIndex() )); + const Datatype& dt = + NodeManager::currentNM()->toExprManager()->getDatatypeForIndex( + n.getConst<DatatypeIndexConstant>().getIndex()); if( dt.isTuple() ){ out << '['; for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) { @@ -347,14 +350,17 @@ void CvcPrinter::toStream( // DATATYPES case kind::PARAMETRIC_DATATYPE: { - const Datatype & dt = (NodeManager::currentNM()->getDatatypeForIndex( n[0].getConst< DatatypeIndexConstant >().getIndex() )); - out << dt.getName() << '['; - for(unsigned i = 1; i < n.getNumChildren(); ++i) { - if(i > 1) { - out << ','; - } - out << n[i]; + const DType& dt = NodeManager::currentNM()->getDTypeForIndex( + n[0].getConst<DatatypeIndexConstant>().getIndex()); + out << dt.getName() << '['; + for (unsigned i = 1; i < n.getNumChildren(); ++i) + { + if (i > 1) + { + out << ','; } + out << n[i]; + } out << ']'; } return; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 006895df7..f0a1e740f 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -21,6 +21,7 @@ #include <typeinfo> #include <vector> +#include "expr/dtype.h" #include "expr/node_manager_attributes.h" #include "options/bv_options.h" #include "options/language.h" @@ -246,7 +247,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::DATATYPE_TYPE: { - const Datatype& dt = (NodeManager::currentNM()->getDatatypeForIndex( + const DType& dt = (NodeManager::currentNM()->getDTypeForIndex( n.getConst<DatatypeIndexConstant>().getIndex())); if (dt.isTuple()) { |