diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-05-27 22:16:02 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-05-27 22:16:02 +0000 |
commit | 4806691be59909eeaecb0fa652d84e40c966fe2e (patch) | |
tree | 129b7317783271f6eb5189d8356963a2ee0549d6 /src/expr | |
parent | 9eb5f5516f3b72fd1d5e5fa6b5960122541a2e93 (diff) |
fix bug #134: infinite deallocation loop
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/node_manager.cpp | 8 | ||||
-rw-r--r-- | src/expr/node_manager.h | 5 |
2 files changed, 10 insertions, 3 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 6c9785413..7c8fb229a 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -24,6 +24,7 @@ #include "theory/bv/theory_bv_type_rules.h" #include <ext/hash_set> +#include <algorithm> using namespace std; using namespace CVC4::expr; @@ -140,9 +141,10 @@ void NodeManager::reclaimZombies() { vector<NodeValue*> zombies; zombies.reserve(d_zombies.size()); - std::copy(d_zombies.begin(), - d_zombies.end(), - std::back_inserter(zombies)); + std::remove_copy_if(d_zombies.begin(), + d_zombies.end(), + std::back_inserter(zombies), + NodeValueReferenceCountNonZero()); d_zombies.clear(); for(vector<NodeValue*>::iterator i = zombies.begin(); diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 098694c3d..a5f82b489 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -54,6 +54,11 @@ class NodeManager { friend class NodeManagerScope; friend class expr::NodeValue; + /** Predicate for use with STL algorithms */ + struct NodeValueReferenceCountNonZero { + bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; } + }; + typedef __gnu_cxx::hash_set<expr::NodeValue*, expr::NodeValuePoolHashFcn, expr::NodeValuePoolEq> NodeValuePool; |