in source/AbstractTreeDomain.h [215:264]
void join_with_internal(
const AbstractTreeDomain& other,
const Elements& accumulator) {
// The read semantics implies that an element on a node is implicitly
// propagated to all its children. The `accumulator` contains all elements
// of the ancestors/parents. If the elements on a child are included in
// the accumulator, we can remove them.
elements_.join_with(other.elements_);
elements_.difference_with(accumulator);
if (children_.reference_equals(other.children_)) {
return;
}
const auto new_accumulator_tree =
AbstractTreeDomain{accumulator.join(elements_)};
Map new_children;
for (const auto& [path_element, subtree] : children_) {
const auto& other_subtree = other.children_.at(path_element);
if (!other_subtree.is_bottom()) {
auto subtree_copy = subtree;
subtree_copy.join_with_internal(
other_subtree, new_accumulator_tree.elements_);
if (!subtree_copy.is_bottom()) {
new_children.insert_or_assign(path_element, std::move(subtree_copy));
}
} else {
if (!subtree.leq(new_accumulator_tree)) {
new_children.insert_or_assign(path_element, subtree);
}
}
}
for (const auto& [path_element, other_subtree] : other.children_) {
const auto& subtree = children_.at(path_element);
if (!subtree.is_bottom()) {
continue; // Already handled.
}
if (!other_subtree.leq(new_accumulator_tree)) {
new_children.insert_or_assign(path_element, other_subtree);
}
}
children_ = new_children;
}