in include/WeakPartialOrdering.h [376:557]
void construct_wpo() {
std::vector<uint32_t> rank(get_next_dfn());
std::vector<uint32_t> parent(get_next_dfn());
// A partition of vertices. Each subset is known to be strongly connected.
boost::disjoint_sets<uint32_t*, uint32_t*> dsets(&rank[0], &parent[0]);
// Maps representative of a set to the vertex with minimum DFN.
std::vector<uint32_t> rep(get_next_dfn());
// Maps a head to its exit.
std::vector<uint32_t> exit(get_next_dfn());
// Maps a vertex to original non-back edges that now target the vertex.
std::vector<std::vector<std::pair<uint32_t, uint32_t>>> origin(
get_next_dfn());
// Maps a head to its size of components.
std::vector<uint32_t> size(get_next_dfn());
// Index of WpoNode in wpo space.
m_d2i.resize(2 * get_next_dfn());
// DFN that will be assigned to the next exit.
uint32_t dfn = get_next_dfn();
// Initialization.
for (uint32_t v = 1; v < get_next_dfn(); v++) {
dsets.make_set(v);
rep[v] = exit[v] = v;
const auto& non_back_preds_v = m_non_back_preds[v];
auto& origin_v = origin[v];
origin_v.reserve(origin_v.size() + non_back_preds_v.size());
for (auto u : non_back_preds_v) {
origin_v.emplace_back(u, v);
}
}
// In reverse DFS order, build WPOs for SCCs bottom-up.
for (uint32_t h = get_next_dfn() - 1; h > 0; h--) {
// Restore cross/fwd edges which has h as the LCA.
auto it = m_cross_fwds.find(h);
if (it != m_cross_fwds.end()) {
for (auto& edge : it->second) {
// edge: u -> v
auto& u = edge.first;
auto& v = edge.second;
auto rep_v = rep[dsets.find_set(v)];
m_non_back_preds[rep_v].push_back(u);
origin[rep_v].emplace_back(u, v);
}
}
// Find nested SCCs.
bool is_SCC = false;
std::unordered_set<uint32_t> backpreds_h;
for (auto v : m_back_preds[h]) {
if (v != h) {
backpreds_h.insert(rep[dsets.find_set(v)]);
} else {
// Self-loop.
is_SCC = true;
}
}
if (!backpreds_h.empty()) {
is_SCC = true;
}
// Invariant: h \notin backpreds_h.
std::unordered_set<uint32_t> nested_SCCs_h(backpreds_h);
std::vector<uint32_t> worklist_h(backpreds_h.begin(), backpreds_h.end());
while (!worklist_h.empty()) {
auto v = worklist_h.back();
worklist_h.pop_back();
for (auto p : m_non_back_preds[v]) {
auto rep_p = rep[dsets.find_set(p)];
auto p_it = nested_SCCs_h.find(rep_p);
if (p_it == nested_SCCs_h.end() && rep_p != h) {
nested_SCCs_h.insert(rep_p);
worklist_h.push_back(rep_p);
}
}
}
// Invariant: h \notin nested_SCCs_h.
// h is a Trivial SCC.
if (!is_SCC) {
size[h] = 1;
add_node(h, get_ref(h), Type::Plain, /*size=*/1);
// Invariant: wpo_space = ...::h
continue;
}
// Compute the size of the component C_h.
// Size of this component is initialized to 2: the head and the exit.
uint32_t size_h = 2;
for (auto v : nested_SCCs_h) {
size_h += size[v];
}
size[h] = size_h;
// Invariant: size_h = size[h] = number of nodes in the component C_h.
// Add new exit x_h.
auto x_h = dfn++;
add_node(x_h, get_ref(h), Type::Exit, size_h);
add_node(h, get_ref(h), Type::Head, size_h);
// Invariant: wpo_space = ...::x_h::h
if (backpreds_h.empty()) {
// Add scheduling constraints from h to x_h
add_successor(/*from=*/h,
/*to=*/x_h,
/*exit=*/x_h,
/*outer_pred?=*/false);
} else {
for (auto p : backpreds_h) {
add_successor(/*from=*/exit[p],
/*to=*/x_h,
/*exit=*/x_h,
/*outer_pred?=*/false);
}
}
// Invariant: Scheduling contraints to x_h are all constructed.
// Add scheduling constraints between the WPOs for nested SCCs.
for (auto v : nested_SCCs_h) {
for (auto& edge : origin[v]) {
auto& u = edge.first;
auto& vv = edge.second;
auto& x_u = exit[rep[dsets.find_set(u)]];
auto& x_v = exit[v];
// Invariant: u -> vv, u \notin C_v, vv \in C_v, u \in C_h, v \in C_h.
if (m_lift) {
add_successor(/*from=*/x_u,
/*to=*/v,
/*exit=*/x_v,
/*outer_pred?=*/x_v != v);
// Invariant: x_u \in get_predecessors(v).
} else {
add_successor(/*from=*/x_u,
/*to=*/vv,
/*exit=*/x_v,
/*outer_pred?=*/x_v != v);
// Invariant: x_u \in get_predecessors(vv).
}
}
}
// Invariant: WPO for SCC with h as its header is constructed.
// Update the partition by merging.
for (auto v : nested_SCCs_h) {
dsets.union_set(v, h);
rep[dsets.find_set(v)] = h;
m_parent[index_of(v)] = index_of(h);
}
// Set exit of h to x_h.
exit[h] = x_h;
// Invariant: exit[h] = h if C_h is trivial SCC, x_h otherwise.
}
// Add scheduling constraints between the WPOs for maximal SCCs.
m_toplevel.reserve(get_next_dfn());
for (uint32_t v = 1; v < get_next_dfn(); v++) {
if (rep[dsets.find_set(v)] == v) {
add_toplevel(v);
m_parent[index_of(v)] = index_of(v);
for (auto& edge : origin[v]) {
auto& u = edge.first;
auto& vv = edge.second;
auto& x_u = exit[rep[dsets.find_set(u)]];
auto& x_v = exit[v];
// Invariant: u -> vv, u \notin C_v, vv \in C_v, u \in C_h, v \in C_h.
if (m_lift) {
add_successor(/*from=*/x_u,
/*to=*/v,
/*exit=*/x_v,
/*outer_pred?=*/x_v != v);
// Invariant: x_u \in get_predecessors(v).
} else {
add_successor(/*from=*/x_u,
/*to=*/vv,
/*exit=*/x_v,
/*outer_pred?=*/x_v != v);
// Invariant: x_u \in get_predecessors(vv).
}
}
}
}
// Invariant: WPO for the CFG is constructed.
}