summaryrefslogtreecommitdiff
path: root/src/expr/node_manager.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r--src/expr/node_manager.h130
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);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback