CVC4_THREADLOCAL(NodeManager*) NodeManager::s_current = NULL;
+namespace {
+
/**
* This class sets it reference argument to true and ensures that it gets set
* to false on destruction. This can be used to make sure a flag gets toggled
}
};
+} // namespace
+
+
NodeManager::NodeManager(ExprManager* exprManager) :
d_options(new Options()),
d_statisticsRegistry(new StatisticsRegistry()),
for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
d_operators[i] = Node::null();
}
-
+
d_unique_vars.clear();
TypeNode 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();
+ 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();
Assert(!d_attrManager->inGarbageCollection() );
- while(!d_zombies.empty()) {
- reclaimZombies();
+
+ std::vector<NodeValue*> order = TopologicalSort(d_maxedOut);
+ d_maxedOut.clear();
+
+ while (!d_zombies.empty() || !order.empty()) {
+ if (d_zombies.empty()) {
+ // Delete the maxed out nodes in toplogical order once we know
+ // there are no additional zombies, or other nodes to worry about.
+ Assert(!order.empty());
+ // We process these in reverse to reverse the topological order.
+ NodeValue* greatest_maxed_out = order.back();
+ order.pop_back();
+ Assert(greatest_maxed_out->HasMaximizedReferenceCount());
+ Debug("gc") << "Force zombify " << greatest_maxed_out << std::endl;
+ greatest_maxed_out->d_rc = 0;
+ markForDeletion(greatest_maxed_out);
+ } else {
+ reclaimZombies();
+ }
}
poolRemove( &expr::NodeValue::null() );
}
}/* NodeManager::reclaimZombies() */
+std::vector<NodeValue*> NodeManager::TopologicalSort(
+ const std::vector<NodeValue*>& roots) {
+ std::vector<NodeValue*> order;
+ std::vector<std::pair<bool, NodeValue*> > stack;
+ NodeValueIDSet visited;
+ const NodeValueIDSet root_set(roots.begin(), roots.end());
+
+ for (size_t index = 0; index < roots.size(); index++) {
+ NodeValue* root = roots[index];
+ if (visited.find(root) == visited.end()) {
+ stack.push_back(std::make_pair(false, root));
+ }
+ while (!stack.empty()) {
+ NodeValue* current = stack.back().second;
+ const bool visited_children = stack.back().first;
+ Debug("gc") << "Topological sort " << current << " " << visited_children
+ << std::endl;
+ if (visited_children) {
+ if (root_set.find(current) != root_set.end()) {
+ order.push_back(current);
+ }
+ stack.pop_back();
+ } else {
+ stack.back().first = true;
+ Assert(visited.count(current) == 0);
+ visited.insert(current);
+ for (int i = 0; i < current->getNumChildren(); ++i) {
+ expr::NodeValue* child = current->getChild(i);
+ if (visited.find(child) == visited.end()) {
+ stack.push_back(std::make_pair(false, child));
+ }
+ }
+ }
+ }
+ }
+ Assert(order.size() == roots.size());
+ return order;
+} /* NodeManager::TopologicalSort() */
+
TypeNode NodeManager::getType(TNode n, bool check)
throw(TypeCheckingExceptionPrivate, AssertionException) {
* to NodeManager events via NodeManager::subscribeEvents(this).
*/
class NodeManagerListener {
-public:
- virtual ~NodeManagerListener() { }
- virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) { }
- virtual void nmNotifyNewSortConstructor(TypeNode tn) { }
- virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort, uint32_t flags) { }
- virtual void nmNotifyNewDatatypes(const std::vector<DatatypeType>& datatypes) { }
- virtual void nmNotifyNewVar(TNode n, uint32_t flags) { }
- virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) { }
+ public:
+ virtual ~NodeManagerListener() {}
+ virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) {}
+ virtual void nmNotifyNewSortConstructor(TypeNode tn) {}
+ virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort,
+ uint32_t flags) {}
+ virtual void nmNotifyNewDatatypes(
+ const std::vector<DatatypeType>& datatypes) {}
+ virtual void nmNotifyNewVar(TNode n, uint32_t flags) {}
+ virtual void nmNotifyNewSkolem(TNode n, const std::string& comment,
+ uint32_t flags) {}
/**
- * Notify a listener of a Node that's being GCed. If this function stores a reference
+ * Notify a listener of a Node that's being GCed. If this function stores a
+ * reference
* to the Node somewhere, very bad things will happen.
*/
- virtual void nmNotifyDeleteNode(TNode n) { }
-};/* class NodeManagerListener */
+ virtual void nmNotifyDeleteNode(TNode n) {}
+}; /* class NodeManagerListener */
class NodeManager {
template <unsigned nchild_thresh> friend class CVC4::NodeBuilder;
expr::NodeValuePoolEq> NodeValuePool;
typedef __gnu_cxx::hash_set<expr::NodeValue*,
expr::NodeValueIDHashFunction,
- expr::NodeValueIDEquality> ZombieSet;
+ expr::NodeValueIDEquality> NodeValueIDSet;
static CVC4_THREADLOCAL(NodeManager*) s_current;
* we might like to delete nodes in least-recently-used order. But
* we also need to avoid processing a zombie twice.
*/
- ZombieSet d_zombies;
+ NodeValueIDSet d_zombies;
+
+ /**
+ * NodeValues with maxed out reference counts. These live as long as the
+ * NodeManager. They have a custom deallocation procedure at the very end.
+ */
+ std::vector<expr::NodeValue*> d_maxedOut;
/**
* A set of operator singletons (w.r.t. to this NodeManager
* plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back.
*/
Node d_operators[kind::LAST_KIND];
-
+
/** unique vars per (Kind,Type) */
std::map< Kind, std::map< TypeNode, Node > > d_unique_vars;
* A list of subscribers for NodeManager events.
*/
std::vector<NodeManagerListener*> d_listeners;
-
+
/** A list of datatypes owned by this node manager. */
std::vector<Datatype*> d_ownedDatatypes;
}
}
+ /**
+ * Register a NodeValue as having a maxed out reference count. This NodeValue
+ * will live as long as its containing NodeManager.
+ */
+ inline void markRefCountMaxedOut(expr::NodeValue* nv) {
+ Assert(nv->HasMaximizedReferenceCount());
+ if(Debug.isOn("gc")) {
+ Debug("gc") << "marking node value " << nv
+ << " [" << nv->d_id << "]: as maxed out" << std::endl;
+ }
+ d_maxedOut.push_back(nv);
+ }
+
/**
* Reclaim all zombies.
*/
*/
bool safeToReclaimZombies() const;
+ /**
+ * Returns a reverse topological sort of a list of NodeValues. The NodeValues
+ * must be valid and have ids. The NodeValues are not modified (including ref
+ * counts).
+ */
+ static std::vector<expr::NodeValue*> TopologicalSort(
+ const std::vector<expr::NodeValue*>& roots);
+
/**
* This template gives a mechanism to stack-allocate a NodeValue
* with enough space for N children (where N is a compile-time
string NodeValue::toString() const {
stringstream ss;
- OutputLanguage outlang = (this == &null()) ? language::output::LANG_AUTO : options::outputLanguage();
+ OutputLanguage outlang = (this == &null()) ? language::output::LANG_AUTO
+ : options::outputLanguage();
toStream(ss, -1, false, false, outlang);
return ss.str();
}
// count, even just for printing.
RefCountGuard guard(this);
- Printer::getPrinter(language)->toStream(out, TNode(this), toDepth, types, dag);
+ Printer::getPrinter(language)->toStream(out, TNode(this), toDepth, types,
+ dag);
}
void NodeValue::printAst(std::ostream& out, int ind) const {
indent(out, ind);
out << '(';
out << getKind();
- if(getMetaKind() == kind::metakind::VARIABLE) {
+ if (getMetaKind() == kind::metakind::VARIABLE) {
out << ' ' << getId();
- } else if(getMetaKind() == kind::metakind::CONSTANT) {
+ } else if (getMetaKind() == kind::metakind::CONSTANT) {
out << ' ';
kind::metakind::NodeValueConstPrinter::toStream(out, this);
} else {
- if(nv_begin() != nv_end()) {
- for(const_nv_iterator child = nv_begin(); child != nv_end(); ++child) {
+ if (nv_begin() != nv_end()) {
+ for (const_nv_iterator child = nv_begin(); child != nv_end(); ++child) {
out << std::endl;
(*child)->printAst(out, ind + 1);
}
out << ')';
}
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
+} /* CVC4::expr namespace */
+} /* CVC4 namespace */
void inc();
void dec();
+ // Returns true if the reference count is maximized.
+ inline bool HasMaximizedReferenceCount() { return d_rc == MAX_RC; }
+
/**
* Uninitializing constructor for NodeBuilder's use.
*/
private:
+ /**
+ * RAII guard that increases the reference count if the reference count to be > 0.
+ * Otherwise, this does nothing. This does not just increment the reference
+ * count to avoid maxing out the d_rc field. This is only for low level functions.
+ */
class RefCountGuard {
NodeValue* d_nv;
+ bool d_increased;
public:
RefCountGuard(const NodeValue* nv) :
d_nv(const_cast<NodeValue*>(nv)) {
- // inc()
- if(__builtin_expect( ( d_nv->d_rc < MAX_RC ), true )) {
- ++d_nv->d_rc;
+ d_increased = (d_nv->d_rc == 0);
+ if(d_increased) {
+ d_nv->d_rc = 1;
}
}
~RefCountGuard() {
// E.g., this can happen when debugging code calls the print
// routines below. As RefCountGuards are scoped on the stack,
// this should be fine---but not in multithreaded contexts!
- if(__builtin_expect( ( d_nv->d_rc < MAX_RC ), true )) {
+ if(d_increased) {
--d_nv->d_rc;
}
}
// FIXME multithreading
if(__builtin_expect( ( d_rc < MAX_RC ), true )) {
++d_rc;
+ if(__builtin_expect( ( d_rc == MAX_RC ), false )) {
+ Assert(NodeManager::currentNM() != NULL,
+ "No current NodeManager on incrementing of NodeValue: "
+ "maybe a public CVC4 interface function is missing a "
+ "NodeManagerScope ?");
+ NodeManager::currentNM()->markRefCountMaxedOut(this);
+ }
}
}
if(__builtin_expect( ( d_rc == 0 ), false )) {
Assert(NodeManager::currentNM() != NULL,
"No current NodeManager on destruction of NodeValue: "
- "maybe a public CVC4 interface function is missing a NodeManagerScope ?");
+ "maybe a public CVC4 interface function is missing a "
+ "NodeManagerScope ?");
NodeManager::currentNM()->markForDeletion(this);
}
}
TS_ASSERT(a_bool->getType(true) == d_em->booleanType());
TS_ASSERT(b_bool->getType(false) == d_em->booleanType());
TS_ASSERT(b_bool->getType(true) == d_em->booleanType());
- TS_ASSERT_THROWS(d_em->mkExpr(MULT,*a_bool,*b_bool).getType(true),
+ TS_ASSERT_THROWS(d_em->mkExpr(MULT,*a_bool,*b_bool).getType(true),
TypeCheckingException);
// These need better support for operators
// TS_ASSERT(and_op->getType().isNull());
#include <string>
#include <vector>
+#include "base/output.h"
#include "expr/node_manager.h"
#include "expr/node_manager_attributes.h"
#include "util/integer.h"
std::vector<Node> vars;
const unsigned int max = metakind::getUpperBoundForKind(AND);
TypeNode boolType = d_nodeManager->booleanType();
- Node skolem = d_nodeManager->mkSkolem("i", boolType);
- for( unsigned int i = 0; i <= max; ++i ) {
- vars.push_back( skolem );
+ Node skolem_i = d_nodeManager->mkSkolem("i", boolType);
+ Node skolem_j = d_nodeManager->mkSkolem("j", boolType);
+ Node andNode = skolem_i.andNode(skolem_j);
+ Node orNode = skolem_i.orNode(skolem_j);
+ while (vars.size() <= max) {
+ vars.push_back(andNode);
+ vars.push_back(skolem_j);
+ vars.push_back(orNode);
}
- TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, vars), AssertionException );
+ TS_ASSERT_THROWS(d_nodeManager->mkNode(AND, vars), AssertionException);
#endif
}
-
};
projects / cvc5.git / commitdiff