void join_with_internal()

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;
  }