diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/attribute.cpp | 43 | ||||
-rw-r--r-- | src/expr/attribute.h | 227 | ||||
-rw-r--r-- | src/expr/expr.cpp | 2 | ||||
-rw-r--r-- | src/expr/expr.h | 2 | ||||
-rw-r--r-- | src/expr/expr_manager.cpp | 24 | ||||
-rw-r--r-- | src/expr/expr_manager.h | 22 | ||||
-rw-r--r-- | src/expr/node.h | 4 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 18 | ||||
-rw-r--r-- | src/expr/node_manager.h | 59 | ||||
-rw-r--r-- | src/expr/type.cpp | 33 | ||||
-rw-r--r-- | src/expr/type.h | 76 |
11 files changed, 362 insertions, 148 deletions
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index e8e93f6ff..be54a973e 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -17,24 +17,43 @@ #include "expr/node_value.h" #include "util/output.h" +#include <utility> + +using namespace std; + namespace CVC4 { namespace expr { namespace attr { +/** + * Search for the NodeValue in all attribute tables and remove it, + * calling the cleanup function if one is defined. + */ +template <class T> +inline void AttributeManager::deleteFromTable(AttrHash<T>& table, + NodeValue* nv) { + for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::s_id; ++id) { + typedef AttributeTraits<T, false> traits_t; + typedef AttrHash<T> hash_t; + pair<uint64_t, NodeValue*> pr = std::make_pair(id, nv); + if(traits_t::cleanup[id] != NULL) { + typename hash_t::iterator i = table.find(pr); + if(i != table.end()) { + traits_t::cleanup[id]((*i).second); + table.erase(pr); + } + } else { + table.erase(pr); + } + } +} + void AttributeManager::deleteAllAttributes(NodeValue* nv) { d_bools.erase(nv); - for(unsigned id = 0; id < attr::LastAttributeId<uint64_t, false>::s_id; ++id) { - d_ints.erase(std::make_pair(id, nv)); - } - for(unsigned id = 0; id < attr::LastAttributeId<TNode, false>::s_id; ++id) { - d_exprs.erase(std::make_pair(id, nv)); - } - for(unsigned id = 0; id < attr::LastAttributeId<std::string, false>::s_id; ++id) { - d_strings.erase(std::make_pair(id, nv)); - } - for(unsigned id = 0; id < attr::LastAttributeId<void*, false>::s_id; ++id) { - d_ptrs.erase(std::make_pair(id, nv)); - } + deleteFromTable(d_ints, nv); + deleteFromTable(d_exprs, nv); + deleteFromTable(d_strings, nv); + deleteFromTable(d_ptrs, nv); // FIXME CD-bools in optimized table /* diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 4dc050648..62619e2b6 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -389,28 +389,139 @@ public: namespace attr { /** Default cleanup for unmanaged Attribute<> */ -template <class T> -struct AttributeCleanupFcn { - static inline void cleanup(const T&) {} -}; +struct NullCleanupFcn { +};/* struct NullCleanupFcn */ /** Default cleanup for ManagedAttribute<> */ template <class T> struct ManagedAttributeCleanupFcn { -}; +};/* struct ManagedAttributeCleanupFcn<> */ /** Specialization for T* */ template <class T> struct ManagedAttributeCleanupFcn<T*> { static inline void cleanup(T* p) { delete p; } -}; +};/* struct ManagedAttributeCleanupFcn<T*> */ /** Specialization for const T* */ template <class T> struct ManagedAttributeCleanupFcn<const T*> { static inline void cleanup(const T* p) { delete p; } +};/* struct ManagedAttributeCleanupFcn<const T*> */ + +/** + * Helper for Attribute<> class below to determine whether a cleanup + * is defined or not. + */ +template <class T, class C> +struct getCleanupFcn { + typedef T value_type; + typedef KindValueToTableValueMapping<value_type> mapping; + static void fn(typename mapping::table_value_type t) { + C::cleanup(mapping::convertBack(t)); + } +};/* struct getCleanupFcn<> */ + +/** + * Specialization for NullCleanupFcn. + */ +template <class T> +struct getCleanupFcn<T, NullCleanupFcn> { + typedef T value_type; + typedef KindValueToTableValueMapping<value_type> mapping; + static void (*const fn)(typename mapping::table_value_type); +};/* struct getCleanupFcn<T, NullCleanupFcn> */ + +// out-of-class initialization required (because it's a non-integral type) +template <class T> +void (*const getCleanupFcn<T, NullCleanupFcn>::fn)(typename getCleanupFcn<T, NullCleanupFcn>::mapping::table_value_type) = NULL; + +/** + * Specialization for ManagedAttributeCleanupFcn<T>. + */ +template <class T> +struct getCleanupFcn<T, ManagedAttributeCleanupFcn<T> > { + typedef T value_type; + typedef KindValueToTableValueMapping<value_type> mapping; + static void (*const fn)(typename mapping::table_value_type); +};/* struct getCleanupFcn<T, ManagedAttributeCleanupFcn<T> > */ + +// out-of-class initialization required (because it's a non-integral type) +template <class T> +void (*const getCleanupFcn<T, ManagedAttributeCleanupFcn<T> >::fn)(typename getCleanupFcn<T, ManagedAttributeCleanupFcn<T> >::mapping::table_value_type) = NULL; + +/** + * Specialization for ManagedAttributeCleanupFcn<T*>. + */ +template <class T> +struct getCleanupFcn<T*, ManagedAttributeCleanupFcn<T*> > { + typedef T* value_type; + typedef ManagedAttributeCleanupFcn<value_type> C; + typedef KindValueToTableValueMapping<value_type> mapping; + static void fn(typename mapping::table_value_type t) { + C::cleanup(mapping::convertBack(t)); + } +};/* struct getCleanupFcn<T*, ManagedAttributeCleanupFcn<T*> > */ + +/** + * Specialization for ManagedAttributeCleanupFcn<const T*>. + */ +template <class T> +struct getCleanupFcn<const T*, ManagedAttributeCleanupFcn<const T*> > { + typedef const T* value_type; + typedef ManagedAttributeCleanupFcn<value_type> C; + typedef KindValueToTableValueMapping<value_type> mapping; + static void fn(typename mapping::table_value_type t) { + C::cleanup(mapping::convertBack(t)); + } +};/* struct getCleanupFcn<const T*, ManagedAttributeCleanupFcn<const T*> > */ + +/** + * Cause compile-time error for improperly-instantiated + * getCleanupFcn<>. + */ +template <class T, class U> +struct getCleanupFcn<T, ManagedAttributeCleanupFcn<U> >; + +}/* CVC4::expr::attr namespace */ + +// ATTRIBUTE IDENTIFIER ASSIGNMENT TEMPLATE ==================================== + +namespace attr { + +/** + * This is the last-attribute-assigner. IDs are not globally + * unique; rather, they are unique for each table_value_type. + */ +template <class T, bool context_dep> +struct LastAttributeId { + static uint64_t s_id; +}; + +/** Initially zero. */ +template <class T, bool context_dep> +uint64_t LastAttributeId<T, context_dep>::s_id = 0; + +}/* CVC4::expr::attr namespace */ + +// ATTRIBUTE TRAITS ============================================================ + +namespace attr { + +/** + * This is the last-attribute-assigner. IDs are not globally + * unique; rather, they are unique for each table_value_type. + */ +template <class T, bool context_dep> +struct AttributeTraits { + typedef void (*cleanup_t)(T); + static std::vector<cleanup_t> cleanup; }; +template <class T, bool context_dep> +std::vector<typename AttributeTraits<T, context_dep>::cleanup_t> + AttributeTraits<T, context_dep>::cleanup; + }/* CVC4::expr::attr namespace */ // ATTRIBUTE DEFINITION ======================================================== @@ -431,9 +542,16 @@ struct ManagedAttributeCleanupFcn<const T*> { */ template <class T, class value_t, - class CleanupFcn = attr::AttributeCleanupFcn<value_t>, + class CleanupFcn = attr::NullCleanupFcn, bool context_dep = false> -struct Attribute { +class Attribute { + /** + * The unique ID associated to this attribute. Assigned statically, + * at load time. + */ + static const uint64_t s_id; + +public: /** The value type for this attribute. */ typedef value_t value_type; @@ -454,20 +572,43 @@ struct Attribute { */ static const bool context_dependent = context_dep; -private: - /** - * The unique ID associated to this attribute. Assigned statically, - * at load time. + * Register this attribute kind and check that the ID is a valid ID + * for bool-valued attributes. Fail an assert if not. Otherwise + * return the id. */ - static const uint64_t s_id; + static inline uint64_t registerAttribute() { + typedef typename attr::KindValueToTableValueMapping<value_t>::table_value_type table_value_type; + typedef attr::AttributeTraits<table_value_type, context_dep> traits; + uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::s_id++; + Assert(traits::cleanup.size() == id);// sanity check + traits::cleanup.push_back(attr::getCleanupFcn<value_t, CleanupFcn>::fn); + return id; + } +};/* class Attribute<> */ + +/** + * An "attribute type" structure for boolean flags (special). The + * full one is below; the existence of this one disallows for boolean + * flag attributes with a specialized cleanup function. + */ +/* -- doesn't work; other specialization is "more specific" ?? +template <class T, class CleanupFcn, bool context_dep> +class Attribute<T, bool, CleanupFcn, context_dep> { + template <bool> struct ERROR_bool_attributes_cannot_have_cleanup_functions; + ERROR_bool_attributes_cannot_have_cleanup_functions<true> blah; }; +*/ /** * An "attribute type" structure for boolean flags (special). */ -template <class T, class CleanupFcn, bool context_dep> -struct Attribute<T, bool, CleanupFcn, context_dep> { +template <class T, bool context_dep> +class Attribute<T, bool, attr::NullCleanupFcn, context_dep> { + /** IDs for bool-valued attributes are actually bit assignments. */ + static const uint64_t s_id; + +public: /** The value type for this attribute; here, bool. */ typedef bool value_type; @@ -495,21 +636,18 @@ struct Attribute<T, bool, CleanupFcn, context_dep> { static const bool context_dependent = context_dep; /** - * Check that the ID is a valid ID for bool-valued attributes. Fail - * an assert if not. Otherwise return the id. + * Register this attribute kind and check that the ID is a valid ID + * for bool-valued attributes. Fail an assert if not. Otherwise + * return the id. */ - static inline uint64_t checkID(uint64_t id) { + static inline uint64_t registerAttribute() { + uint64_t id = attr::LastAttributeId<bool, context_dep>::s_id++; AlwaysAssert( id <= 63, "Too many boolean node attributes registered " "during initialization !" ); return id; } - -private: - - /** IDs for bool-valued attributes are actually bit assignments. */ - static const uint64_t s_id; -}; +};/* class Attribute<..., bool, ...> */ /** * This is a context-dependent attribute kind (the only difference @@ -520,7 +658,7 @@ private: template <class T, class value_type> struct CDAttribute : - public Attribute<T, value_type, attr::AttributeCleanupFcn<value_type>, true> {}; + public Attribute<T, value_type, attr::NullCleanupFcn, true> {}; /** * This is a managed attribute kind (the only difference between @@ -541,35 +679,21 @@ struct ManagedAttribute : // ATTRIBUTE IDENTIFIER ASSIGNMENT ============================================= -namespace attr { - -/** - * This is the last-attribute-assigner. IDs are not globally - * unique; rather, they are unique for each table_value_type. - */ -template <class T, bool context_dep> -struct LastAttributeId { - static uint64_t s_id; -}; - -/** Initially zero. */ -template <class T, bool context_dep> -uint64_t LastAttributeId<T, context_dep>::s_id = 0; - -}/* CVC4::expr::attr namespace */ - /** Assign unique IDs to attributes at load time. */ +// Use of the comma-operator here forces instantiation (and +// initialization) of the AttributeTraits<> structure and its +// "cleanup" vector before registerAttribute() is called. This is +// important because otherwise the vector is initialized later, +// clearing the first-pushed cleanup function. template <class T, class value_t, class CleanupFcn, bool context_dep> const uint64_t Attribute<T, value_t, CleanupFcn, context_dep>::s_id = - attr::LastAttributeId<typename attr::KindValueToTableValueMapping<value_t>::table_value_type, context_dep>::s_id++; + ( attr::AttributeTraits<typename attr::KindValueToTableValueMapping<value_t>::table_value_type, context_dep>::cleanup.size(), + Attribute<T, value_t, CleanupFcn, context_dep>::registerAttribute() ); -/** - * Assign unique IDs to bool-valued attributes at load time, checking - * that they are in range. - */ -template <class T, class CleanupFcn, bool context_dep> -const uint64_t Attribute<T, bool, CleanupFcn, context_dep>::s_id = - Attribute<T, bool, CleanupFcn, context_dep>::checkID(attr::LastAttributeId<bool, context_dep>::s_id++); +/** Assign unique IDs to attributes at load time. */ +template <class T, bool context_dep> +const uint64_t Attribute<T, bool, attr::NullCleanupFcn, context_dep>::s_id = + Attribute<T, bool, attr::NullCleanupFcn, context_dep>::registerAttribute(); // ATTRIBUTE MANAGER =========================================================== @@ -609,6 +733,9 @@ class AttributeManager { /** Underlying hash table for context-dependent pointer-valued attributes */ CDAttrHash<void*> d_cdptrs; + template <class T> + void deleteFromTable(AttrHash<T>& table, NodeValue* nv); + /** * getTable<> is a helper template that gets the right table from an * AttributeManager given its type. diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index 2f84f018b..6f611cf95 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -91,7 +91,7 @@ size_t Expr::getNumChildren() const { return d_node->getNumChildren(); } -const Type* Expr::getType() const { +Type* Expr::getType() const { ExprManagerScope ems(*this); return d_node->getType(); } diff --git a/src/expr/expr.h b/src/expr/expr.h index b297be6fb..c5478b1da 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -106,7 +106,7 @@ public: /** Returns the type of the expression, if it has been computed. * Returns NULL if the type of the expression is not known. */ - const Type* getType() const; + Type* getType() const; /** * Returns the string representation of the expression. diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index f0a35e5f1..0b0139118 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -42,12 +42,12 @@ ExprManager::~ExprManager() { delete d_ctxt; } -const BooleanType* ExprManager::booleanType() const { +BooleanType* ExprManager::booleanType() const { NodeManagerScope nms(d_nodeManager); return d_nodeManager->booleanType(); } -const KindType* ExprManager::kindType() const { +KindType* ExprManager::kindType() const { NodeManagerScope nms(d_nodeManager); return d_nodeManager->kindType(); } @@ -106,32 +106,30 @@ Expr ExprManager::mkExpr(Kind kind, const vector<Expr>& children) { } /** Make a function type from domain to range. */ -const FunctionType* -ExprManager::mkFunctionType(const Type* domain, - const Type* range) { +FunctionType* ExprManager::mkFunctionType(Type* domain, + Type* range) { NodeManagerScope nms(d_nodeManager); - return d_nodeManager->mkFunctionType(domain,range); + return d_nodeManager->mkFunctionType(domain, range); } /** Make a function type with input types from argTypes. */ -const FunctionType* -ExprManager::mkFunctionType(const std::vector<const Type*>& argTypes, - const Type* range) { +FunctionType* ExprManager::mkFunctionType(const std::vector<Type*>& argTypes, + Type* range) { NodeManagerScope nms(d_nodeManager); - return d_nodeManager->mkFunctionType(argTypes,range); + return d_nodeManager->mkFunctionType(argTypes, range); } -const Type* ExprManager::mkSort(const std::string& name) { +Type* ExprManager::mkSort(const std::string& name) { NodeManagerScope nms(d_nodeManager); return d_nodeManager->mkSort(name); } -Expr ExprManager::mkVar(const Type* type, const std::string& name) { +Expr ExprManager::mkVar(Type* type, const std::string& name) { NodeManagerScope nms(d_nodeManager); return Expr(this, new Node(d_nodeManager->mkVar(type, name))); } -Expr ExprManager::mkVar(const Type* type) { +Expr ExprManager::mkVar(Type* type) { NodeManagerScope nms(d_nodeManager); return Expr(this, new Node(d_nodeManager->mkVar(type))); } diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index ff4e0db6b..3c73e1ced 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -51,10 +51,10 @@ public: ~ExprManager(); /** Get the type for booleans */ - const BooleanType* booleanType() const; + BooleanType* booleanType() const; /** Get the type for sorts. */ - const KindType* kindType() const; + KindType* kindType() const; /** * Make a unary expression of a given kind (TRUE, FALSE,...). @@ -95,21 +95,21 @@ public: Expr mkExpr(Kind kind, const std::vector<Expr>& children); /** Make a function type from domain to range. */ - const FunctionType* - mkFunctionType(const Type* domain, - const Type* range); + FunctionType* + mkFunctionType(Type* domain, + Type* range); /** Make a function type with input types from argTypes. */ - const FunctionType* - mkFunctionType(const std::vector<const Type*>& argTypes, - const Type* range); + FunctionType* + mkFunctionType(const std::vector<Type*>& argTypes, + Type* range); /** Make a new sort with the given name. */ - const Type* mkSort(const std::string& name); + Type* mkSort(const std::string& name); // variables are special, because duplicates are permitted - Expr mkVar(const Type* type, const std::string& name); - Expr mkVar(const Type* type); + Expr mkVar(Type* type, const std::string& name); + Expr mkVar(Type* type); private: /** The context */ diff --git a/src/expr/node.h b/src/expr/node.h index d1bb8f3b3..25990cedf 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -240,7 +240,7 @@ public: * Returns the type of this node. * @return the type */ - const Type* getType() const; + Type* getType() const; /** * Returns the kind of this node. @@ -707,7 +707,7 @@ bool NodeTemplate<ref_count>::hasOperator() const { } template <bool ref_count> -const Type* NodeTemplate<ref_count>::getType() const { +Type* NodeTemplate<ref_count>::getType() const { Assert( NodeManager::currentNM() != NULL, "There is no current CVC4::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?" ); diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 7be593575..7b171a48b 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -25,9 +25,18 @@ namespace CVC4 { __thread NodeManager* NodeManager::s_current = 0; +NodeManager::~NodeManager() { + NodeManagerScope nms(this); + while(!d_zombies.empty()) { + reclaimZombies(); + } + + poolRemove( &expr::NodeValue::s_null ); +} + NodeValue* NodeManager::poolLookup(NodeValue* nv) const { - NodeValueSet::const_iterator find = d_nodeValueSet.find(nv); - if(find == d_nodeValueSet.end()) { + NodeValuePool::const_iterator find = d_nodeValuePool.find(nv); + if(find == d_nodeValuePool.end()) { return NULL; } else { return *find; @@ -87,7 +96,7 @@ void NodeManager::reclaimZombies() { NodeValue* nv = *i; // collect ONLY IF still zero - if((*i)->d_rc == 0) { + if(nv->d_rc == 0) { Debug("gc") << "deleting node value " << nv << " [" << nv->d_id << "]: " << nv->toString() << "\n"; @@ -101,8 +110,7 @@ void NodeManager::reclaimZombies() { // decr ref counts of children nv->decrRefCounts(); - //free(nv); -#warning NOT FREEING NODEVALUES + free(nv); } } } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index b40ec2978..a3be61e48 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -30,6 +30,7 @@ #include "expr/expr.h" #include "expr/node_value.h" #include "context/context.h" +#include "expr/type.h" namespace CVC4 { @@ -44,7 +45,7 @@ struct Type {}; }/* CVC4::expr::attr namespace */ typedef Attribute<attr::VarName, std::string> VarNameAttr; -typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr; +typedef ManagedAttribute<attr::Type, CVC4::Type*, attr::TypeCleanupFcn> TypeAttr; }/* CVC4::expr namespace */ @@ -55,12 +56,12 @@ class NodeManager { typedef __gnu_cxx::hash_set<expr::NodeValue*, expr::NodeValueInternalHashFcn, - expr::NodeValue::NodeValueEq> NodeValueSet; + expr::NodeValue::NodeValueEq> NodeValuePool; typedef __gnu_cxx::hash_set<expr::NodeValue*, expr::NodeValueIDHashFcn, expr::NodeValue::NodeValueEq> ZombieSet; - NodeValueSet d_nodeValueSet; + NodeValuePool d_nodeValuePool; expr::attr::AttributeManager d_attrManager; @@ -108,6 +109,8 @@ public: poolInsert( &expr::NodeValue::s_null ); } + ~NodeManager(); + static NodeManager* currentNM() { return s_current; } // general expression-builders @@ -121,8 +124,8 @@ public: Node mkNode(Kind kind, const std::vector<Node>& children); // variables are special, because duplicates are permitted - Node mkVar(const Type* type, const std::string& name); - Node mkVar(const Type* type); + Node mkVar(Type* type, const std::string& name); + Node mkVar(Type* type); Node mkVar(); template <class AttrKind> @@ -172,27 +175,26 @@ public: const typename AttrKind::value_type& value); /** Get the type for booleans. */ - inline const BooleanType* booleanType() const { + inline BooleanType* booleanType() const { return BooleanType::getInstance(); } /** Get the type for sorts. */ - inline const KindType* kindType() const { + inline KindType* kindType() const { return KindType::getInstance(); } /** Make a function type from domain to range. */ - inline const FunctionType* - mkFunctionType(const Type* domain, const Type* range) const; + inline FunctionType* mkFunctionType(Type* domain, Type* range) const; /** Make a function type with input types from argTypes. */ - inline const FunctionType* - mkFunctionType(const std::vector<const Type*>& argTypes, const Type* range) const; + inline FunctionType* mkFunctionType(const std::vector<Type*>& argTypes, + Type* range) const; /** Make a new sort with the given name. */ - inline const Type* mkSort(const std::string& name) const; + inline Type* mkSort(const std::string& name) const; - inline const Type* getType(TNode n) const; + inline Type* getType(TNode n) const; }; /** @@ -308,41 +310,39 @@ inline void NodeManager::setAttribute(TNode n, /** Make a function type from domain to range. * TODO: Function types should be unique for this manager. */ -const FunctionType* -NodeManager::mkFunctionType(const Type* domain, - const Type* range) const { - std::vector<const Type*> argTypes; +FunctionType* NodeManager::mkFunctionType(Type* domain, + Type* range) const { + std::vector<Type*> argTypes; argTypes.push_back(domain); return new FunctionType(argTypes, range); } /** Make a function type with input types from argTypes. * TODO: Function types should be unique for this manager. */ -const FunctionType* -NodeManager::mkFunctionType(const std::vector<const Type*>& argTypes, - const Type* range) const { +FunctionType* NodeManager::mkFunctionType(const std::vector<Type*>& argTypes, + Type* range) const { Assert( argTypes.size() > 0 ); return new FunctionType(argTypes, range); } -const Type* -NodeManager::mkSort(const std::string& name) const { +Type* NodeManager::mkSort(const std::string& name) const { return new SortType(name); } -inline const Type* NodeManager::getType(TNode n) const { + +inline Type* NodeManager::getType(TNode n) const { return getAttribute(n, CVC4::expr::TypeAttr()); } inline void NodeManager::poolInsert(expr::NodeValue* nv) { - Assert(d_nodeValueSet.find(nv) == d_nodeValueSet.end(), + Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(), "NodeValue already in the pool!"); - d_nodeValueSet.insert(nv);// FIXME multithreading + d_nodeValuePool.insert(nv);// FIXME multithreading } inline void NodeManager::poolRemove(expr::NodeValue* nv) { - Assert(d_nodeValueSet.find(nv) != d_nodeValueSet.end(), + Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end(), "NodeValue is not in the pool!"); - d_nodeValueSet.erase(nv);// FIXME multithreading + d_nodeValuePool.erase(nv);// FIXME multithreading } }/* CVC4 namespace */ @@ -382,14 +382,15 @@ inline Node NodeManager::mkNode(Kind kind, const std::vector<Node>& children) { return NodeBuilder<>(this, kind).append(children); } -inline Node NodeManager::mkVar(const Type* type, const std::string& name) { +inline Node NodeManager::mkVar(Type* type, const std::string& name) { Node n = mkVar(type); n.setAttribute(expr::VarNameAttr(), name); return n; } -inline Node NodeManager::mkVar(const Type* type) { +inline Node NodeManager::mkVar(Type* type) { Node n = mkVar(); + type->inc();// reference-count the type n.setAttribute(expr::TypeAttr(), type); return n; } diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 4bdda6810..2549f02ca 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -26,11 +26,12 @@ std::ostream& operator<<(std::ostream& out, const Type& e) { } Type::Type() : - d_name(std::string("<undefined>")) { + d_name(std::string("<undefined>")), + d_rc(0) { } Type::Type(std::string name) : - d_name(name) { + d_name(name) { } std::string Type::getName() const { @@ -39,7 +40,9 @@ std::string Type::getName() const { BooleanType BooleanType::s_instance; -BooleanType::BooleanType() : Type(std::string("BOOLEAN")) { +BooleanType::BooleanType() : + Type(std::string("BOOLEAN")) { + d_rc = RC_MAX;// singleton, not heap-allocated } BooleanType::~BooleanType() { @@ -54,22 +57,23 @@ bool BooleanType::isBoolean() const { return true; } -FunctionType::FunctionType(const std::vector<const Type*>& argTypes, - const Type* range) - : d_argTypes(argTypes), - d_rangeType(range) { +FunctionType::FunctionType(const std::vector<Type*>& argTypes, + Type* range) : + d_argTypes(argTypes), + d_rangeType(range) { + Assert( argTypes.size() > 0 ); } - // FIXME: What becomes of argument types? +// FIXME: What becomes of argument types? FunctionType::~FunctionType() { } -const std::vector<const Type*> FunctionType::getArgTypes() const { +const std::vector<Type*> FunctionType::getArgTypes() const { return d_argTypes; } -const Type* FunctionType::getRangeType() const { +Type* FunctionType::getRangeType() const { return d_rangeType; } @@ -100,7 +104,9 @@ void FunctionType::toStream(std::ostream& out) const { KindType KindType::s_instance; -KindType::KindType() : Type(std::string("KIND")) { +KindType::KindType() : + Type(std::string("KIND")) { + d_rc = RC_MAX;// singleton, not heap-allocated } KindType::~KindType() { @@ -115,12 +121,11 @@ KindType::getInstance() { return &s_instance; } -SortType::SortType(std::string name) - : Type(name) { +SortType::SortType(std::string name) : + Type(name) { } SortType::~SortType() { } - } diff --git a/src/expr/type.h b/src/expr/type.h index 7009ed504..fd9ea01d7 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -17,19 +17,32 @@ #define __CVC4__TYPE_H #include "cvc4_config.h" +#include "util/output.h" +#include "util/Assert.h" #include <string> #include <vector> +#include <limits.h> namespace CVC4 { +namespace expr { + namespace attr { + struct TypeCleanupFcn; + }/* CVC4::expr::attr namespace */ +}/* CVC4::expr namespace */ + class NodeManager; /** * Class encapsulating CVC4 expression types. */ class CVC4_PUBLIC Type { +protected: + static const unsigned RC_MAX = UINT_MAX; + public: + /** Comparision for equality */ bool operator==(const Type& t) const; @@ -72,11 +85,38 @@ protected: /** Create a type with the given name. */ Type(std::string name); - /** Destructor */ - virtual ~Type() { }; - /** The name of the type (may be empty). */ std::string d_name; + + /** + * The reference count for this Type (how many times it's referred + * to in the Type attribute table) + */ + unsigned d_rc; + + /** Force a virtual destructor for safety. */ + virtual ~Type() { + Assert(d_rc == RC_MAX || d_rc == 0, + "illegal ref count %u for destructed Type", d_rc); + } + + /** Increment the reference count */ + void inc() { + if(d_rc != RC_MAX) { + ++d_rc; + } + } + + /** Decrement the reference count */ + void dec() { + if(d_rc != RC_MAX) { + Assert(d_rc != 0, "illegal ref count %u for dec()", d_rc); + --d_rc; + } + } + + friend class ::CVC4::NodeManager; + friend struct ::CVC4::expr::attr::TypeCleanupFcn; }; /** @@ -117,10 +157,10 @@ class FunctionType : public Type { public: /** Retrieve the argument types. The vector will be non-empty. */ - const std::vector<const Type*> getArgTypes() const; + const std::vector<Type*> getArgTypes() const; /** Get the range type (i.e., the type of the result). */ - const Type* getRangeType() const; + Type* getRangeType() const; /** Is this as function type? (Returns true.) */ bool isFunction() const; @@ -141,17 +181,17 @@ private: * @param argTypes a non-empty vector of input types * @param range the result type */ - FunctionType(const std::vector<const Type*>& argTypes, - const Type* range); + FunctionType(const std::vector<Type*>& argTypes, + Type* range); /** Destructor */ ~FunctionType(); /** The list of input types. */ - const std::vector<const Type*> d_argTypes; + const std::vector<Type*> d_argTypes; /** The result type. */ - const Type* d_rangeType; + Type* d_rangeType; friend class NodeManager; }; @@ -211,6 +251,22 @@ private: */ std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC; -} +namespace expr { +namespace attr { + +struct TypeCleanupFcn { + static void cleanup(Type* t) { + // reference-count the Type + t->dec(); + if(t->d_rc == 0) { + delete t; + } + } +}; + +}/* CVC4::expr::attr namespace */ +}/* CVC4::expr namespace */ + +}/* CVC4 namespace */ #endif /* __CVC4__TYPE_H */ |