Skip to content

Commit

Permalink
Free intermediate BDD nodes early during LibBDD reconstruction
Browse files Browse the repository at this point in the history
Partially resolves #138 by decreasing the number of concurrent BDD roots. Yet,
this does not as such solve the problem but only push it to further. Sylvan
will still crash, if a single level is wider than the Lace stack (or prior,
if BDD nodes from multiple levels are still alive).
  • Loading branch information
SSoelvsten committed Nov 1, 2024
1 parent bd1c740 commit 179e64f
Showing 1 changed file with 9 additions and 0 deletions.
9 changes: 9 additions & 0 deletions src/common/libbdd_parser.h
Original file line number Diff line number Diff line change
Expand Up @@ -430,6 +430,13 @@ namespace lib_bdd
return adapter.build();
}

// Reference count
std::vector<int> ref_count(in.size(), 0);
for (const auto& n : in) {
ref_count[n.low()] += 1;
ref_count[n.high()] += 1;
}

// Vector of converted DD nodes
std::unordered_map<int, typename Adapter::build_node_t> out;

Expand Down Expand Up @@ -457,9 +464,11 @@ namespace lib_bdd

assert(out.find(n.low()) != out.end());
const auto low = out[n.low()];
if (--ref_count[n.low()] == 0) { out.erase(n.low()); }

assert(out.find(n.high()) != out.end());
const auto high = out[n.high()];
if (--ref_count[n.high()] == 0) { out.erase(n.high()); }

out[*iter] = adapter.build_node(var->second, low, high);
}
Expand Down

0 comments on commit 179e64f

Please sign in to comment.