diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-03-28 21:02:37 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-03-28 23:02:37 -0500 |
commit | a1decafaf4c7c46a4eda3d816e9a8799b4c96ad3 (patch) | |
tree | 72ea26e545fd904738158c326f2c78c152479d2a | |
parent | 952ee3698e7760ccbd90fac5691d455d807af3a6 (diff) |
Fix freeing nodes with maxed refcounts (#2903)
-rw-r--r-- | src/expr/node_manager.cpp | 16 | ||||
-rw-r--r-- | test/unit/expr/node_manager_white.h | 20 |
2 files changed, 31 insertions, 5 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index c9d772b26..66d597a36 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -363,7 +363,10 @@ void NodeManager::reclaimZombies() { std::vector<NodeValue*> NodeManager::TopologicalSort( const std::vector<NodeValue*>& roots) { std::vector<NodeValue*> order; + // The stack of nodes to visit. The Boolean value is false when visiting the + // node in preorder and true when visiting it in postorder. std::vector<std::pair<bool, NodeValue*> > stack; + // Nodes that have been visited in both pre- and postorder NodeValueIDSet visited; const NodeValueIDSet root_set(roots.begin(), roots.end()); @@ -382,17 +385,20 @@ std::vector<NodeValue*> NodeManager::TopologicalSort( order.push_back(current); } stack.pop_back(); - } else { + } + else if (visited.find(current) == visited.end()) + { stack.back().first = true; - Assert(visited.count(current) == 0); visited.insert(current); for (unsigned 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)); - } + stack.push_back(std::make_pair(false, child)); } } + else + { + stack.pop_back(); + } } } Assert(order.size() == roots.size()); diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h index 99ee171b7..0e5d550a9 100644 --- a/test/unit/expr/node_manager_white.h +++ b/test/unit/expr/node_manager_white.h @@ -70,4 +70,24 @@ class NodeManagerWhite : public CxxTest::TestSuite { TS_ASSERT_THROWS(nb.realloc(67108863), AssertionException&); #endif /* CVC4_ASSERTIONS */ } + + void testTopologicalSort() + { + TypeNode boolType = d_nm->booleanType(); + Node i = d_nm->mkSkolem("i", boolType); + Node j = d_nm->mkSkolem("j", boolType); + Node n1 = d_nm->mkNode(kind::AND, j, j); + Node n2 = d_nm->mkNode(kind::AND, i, n1); + + { + std::vector<NodeValue*> roots = {n1.d_nv}; + TS_ASSERT_EQUALS(NodeManager::TopologicalSort(roots), roots); + } + + { + std::vector<NodeValue*> roots = {n2.d_nv, n1.d_nv}; + std::vector<NodeValue*> result = {n1.d_nv, n2.d_nv}; + TS_ASSERT_EQUALS(NodeManager::TopologicalSort(roots), result); + } + } }; |