void widen_with_internal()

in source/AbstractTreeDomain.h [285:347]
49 lines of code
10 McCabe index (conditional complexity)

  void widen_with_internal(
      const AbstractTreeDomain& other,
      const Elements& accumulator,
      std::size_t max_height) {
    if (max_height == 0) {
      collapse_inplace();
      other.collapse_into(elements_);
      elements_.difference_with(accumulator);
      return;
    }

    // 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_)) {
      collapse_deeper_than(max_height);
      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.widen_with_internal(
            other_subtree, new_accumulator_tree.elements_, max_height - 1);

        if (!subtree_copy.is_bottom()) {
          new_children.insert_or_assign(path_element, std::move(subtree_copy));
        }
      } else {
        if (!subtree.leq(new_accumulator_tree)) {
          auto subtree_copy = subtree;
          subtree_copy.collapse_deeper_than(max_height - 1);
          new_children.insert_or_assign(path_element, subtree_copy);
        }
      }
    }

    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)) {
        auto other_subtree_copy = other_subtree;
        other_subtree_copy.collapse_deeper_than(max_height - 1);
        new_children.insert_or_assign(path_element, other_subtree_copy);
      }
    }

    children_ = new_children;
  }