diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-08 23:49:47 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-08 23:49:47 +0000 |
commit | cf4d347cbbbb4c1a1e1db99337cfd2b22b84b756 (patch) | |
tree | ceea43e3d37525038bed10b115c73a8aa08ce68d /src/expr/node_manager.h | |
parent | de0160112edbed8ce9b62bf87172ae2f0e99a013 (diff) |
This fixes regressions at levels >= 1 which were failing
* implement zombification and garbage collection of NodeValues
(but GC not turned on yet)
* implement removal of key nodes from all attribute tables
* audit NodeBuilder and fix memory leaks and improper reference-count
management. This is in many places a re-write. Clearly documented
invariants on NodeBuilder state. (Closes Bug 38)
* created a "BackedNodeBuilder" that can be used to construct
NodeBuilders with a stack-based backing store for a size that's not
a compile-time constant.
* NodeValues no longer depend on Node for toStream()'ing
* make unit test-building "silent" with --enable-silent-rules
* (Makefile.am, Makefile.builds.in) fix top-level build system so that
"make regressN" works with unbuilt/out-of-date source trees in the
expected way.
* (various) code cleanup, documentation, formatting
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 130 |
1 files changed, 110 insertions, 20 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index c4f54727a..32c1cd210 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -28,6 +28,7 @@ #include "expr/kind.h" #include "expr/expr.h" +#include "expr/node_value.h" #include "context/context.h" namespace CVC4 { @@ -50,31 +51,65 @@ typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr; class NodeManager { static __thread NodeManager* s_current; - template <unsigned> friend class CVC4::NodeBuilder; + template <class Builder> friend class CVC4::NodeBuilderBase; typedef __gnu_cxx::hash_set<expr::NodeValue*, expr::NodeValueInternalHashFcn, expr::NodeValue::NodeValueEq> NodeValueSet; + typedef __gnu_cxx::hash_set<expr::NodeValue*, + expr::NodeValueIDHashFcn, + expr::NodeValue::NodeValueEq> ZombieSet; + NodeValueSet d_nodeValueSet; expr::attr::AttributeManager d_attrManager; expr::NodeValue* poolLookup(expr::NodeValue* nv) const; void poolInsert(expr::NodeValue* nv); + void poolRemove(expr::NodeValue* nv); friend class NodeManagerScope; friend class expr::NodeValue; - std::vector<expr::NodeValue*> d_zombieList; + bool d_reclaiming; + ZombieSet d_zombies; + /** + * Register a NodeValue as a zombie. + */ inline void gc(expr::NodeValue* nv) { Assert(nv->d_rc == 0); - d_zombieList.push_back(nv); + if(d_reclaiming) {// FIXME multithreading + // currently reclaiming zombies; just push onto the list + Debug("gc") << "zombifying node value " << nv + << " [" << nv->d_id << "]: " << nv->toString() + << " [CURRENTLY-RECLAIMING]\n"; + d_zombies.insert(nv);// FIXME multithreading + } else { + Debug("gc") << "zombifying node value " << nv + << " [" << nv->d_id << "]: " << nv->toString() << "\n"; + d_zombies.insert(nv);// FIXME multithreading + + // for now, collect eagerly. can add heuristic here later.. + reclaimZombies(); + } } + /** + * Reclaim all zombies. + */ + void reclaimZombies(); + + /** + * Reclaim a particular zombie. + */ + void reclaimZombie(expr::NodeValue* nv); + public: - NodeManager(context::Context* ctxt) : d_attrManager(ctxt) { + NodeManager(context::Context* ctxt) : + d_attrManager(ctxt), + d_reclaiming(false) { poolInsert( &expr::NodeValue::s_null ); } @@ -96,6 +131,29 @@ public: Node mkVar(); template <class AttrKind> + inline typename AttrKind::value_type getAttribute(expr::NodeValue* nv, + const AttrKind&) const; + + // Note that there are two, distinct hasAttribute() declarations for + // a reason (rather than using a pointer-valued argument with a + // default value): they permit more optimized code in the underlying + // hasAttribute() implementations. + + template <class AttrKind> + inline bool hasAttribute(expr::NodeValue* nv, + const AttrKind&) const; + + template <class AttrKind> + inline bool hasAttribute(expr::NodeValue* nv, + const AttrKind&, + typename AttrKind::value_type&) const; + + template <class AttrKind> + inline void setAttribute(expr::NodeValue* nv, + const AttrKind&, + const typename AttrKind::value_type& value); + + template <class AttrKind> inline typename AttrKind::value_type getAttribute(TNode n, const AttrKind&) const; @@ -118,7 +176,6 @@ public: const AttrKind&, const typename AttrKind::value_type& value); - /** Get the type for booleans. */ inline const BooleanType* booleanType() const { return BooleanType::getInstance(); @@ -131,16 +188,16 @@ public: /** Make a function type from domain to range. */ inline const FunctionType* - mkFunctionType(const Type* domain, const Type* range); + mkFunctionType(const Type* domain, const 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); + mkFunctionType(const std::vector<const Type*>& argTypes, const Type* range) const; /** Make a new sort with the given name. */ - inline const Type* mkSort(const std::string& name); + inline const Type* mkSort(const std::string& name) const; - inline const Type* getType(TNode n); + inline const Type* getType(TNode n) const; }; /** @@ -203,36 +260,62 @@ public: }; template <class AttrKind> +inline typename AttrKind::value_type NodeManager::getAttribute(expr::NodeValue* nv, + const AttrKind&) const { + return d_attrManager.getAttribute(nv, AttrKind()); +} + +template <class AttrKind> +inline bool NodeManager::hasAttribute(expr::NodeValue* nv, + const AttrKind&) const { + return d_attrManager.hasAttribute(nv, AttrKind()); +} + +template <class AttrKind> +inline bool NodeManager::hasAttribute(expr::NodeValue* nv, + const AttrKind&, + typename AttrKind::value_type& ret) const { + return d_attrManager.hasAttribute(nv, AttrKind(), ret); +} + +template <class AttrKind> +inline void NodeManager::setAttribute(expr::NodeValue* nv, + const AttrKind&, + const typename AttrKind::value_type& value) { + d_attrManager.setAttribute(nv, AttrKind(), value); +} + +template <class AttrKind> inline typename AttrKind::value_type NodeManager::getAttribute(TNode n, const AttrKind&) const { - return d_attrManager.getAttribute(n, AttrKind()); + return d_attrManager.getAttribute(n.d_nv, AttrKind()); } template <class AttrKind> inline bool NodeManager::hasAttribute(TNode n, const AttrKind&) const { - return d_attrManager.hasAttribute(n, AttrKind()); + return d_attrManager.hasAttribute(n.d_nv, AttrKind()); } template <class AttrKind> inline bool NodeManager::hasAttribute(TNode n, const AttrKind&, typename AttrKind::value_type& ret) const { - return d_attrManager.hasAttribute(n, AttrKind(), ret); + return d_attrManager.hasAttribute(n.d_nv, AttrKind(), ret); } template <class AttrKind> inline void NodeManager::setAttribute(TNode n, const AttrKind&, const typename AttrKind::value_type& value) { - d_attrManager.setAttribute(n, AttrKind(), value); + d_attrManager.setAttribute(n.d_nv, AttrKind(), value); } /** Make a function type from domain to range. - * TODO: Function types should be unique for this manager. */ + * TODO: Function types should be unique for this manager. */ const FunctionType* NodeManager::mkFunctionType(const Type* domain, - const Type* range) { + const Type* range) const { std::vector<const Type*> argTypes; argTypes.push_back(domain); return new FunctionType(argTypes, range); @@ -242,23 +325,29 @@ NodeManager::mkFunctionType(const Type* domain, * TODO: Function types should be unique for this manager. */ const FunctionType* NodeManager::mkFunctionType(const std::vector<const Type*>& argTypes, - const Type* range) { + const Type* range) const { Assert( argTypes.size() > 0 ); return new FunctionType(argTypes, range); } const Type* -NodeManager::mkSort(const std::string& name) { +NodeManager::mkSort(const std::string& name) const { return new SortType(name); } -inline const Type* NodeManager::getType(TNode n) { +inline const 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(), "NodeValue already in the pool!"); - d_nodeValueSet.insert(nv); + d_nodeValueSet.insert(nv);// FIXME multithreading +} + +inline void NodeManager::poolRemove(expr::NodeValue* nv) { + Assert(d_nodeValueSet.find(nv) != d_nodeValueSet.end(), + "NodeValue is not in the pool!"); + d_nodeValueSet.erase(nv);// FIXME multithreading } }/* CVC4 namespace */ @@ -305,12 +394,13 @@ inline Node NodeManager::mkVar(const Type* type, const std::string& name) { } inline Node NodeManager::mkVar(const Type* type) { - Node n = NodeBuilder<>(this, kind::VARIABLE); + Node n = mkVar(); n.setAttribute(expr::TypeAttr(), type); return n; } inline Node NodeManager::mkVar() { + // TODO: rewrite to not use NodeBuilder return NodeBuilder<>(this, kind::VARIABLE); } |