mapping : mapOfSets.entrySet()) {
+ if (mapping.getValue().contains(pE)) {
+ return mapping.getKey();
+ }
+ }
+
+ throw new IllegalArgumentException("Element not contained");
+ }
+
+ /**
+ * Merges the sets represented by the two input values according to standard Union-Find behaviour.
+ *
+ * USES: Add new element as new set: pass it as both pE1 and pE2. Add new element to existing
+ * set: one input value is the new element, the other the canonical element of the set to be added
+ * to. Merge two existing sets: pE1, pE2 canonical elements of sets to be merged.
+ *
+ * @param pE1 first element
+ * @param pE2 second element
+ */
+ @Override
+ public void union(T pE1, T pE2) {
+
+ Preconditions.checkNotNull(pE1);
+ Preconditions.checkNotNull(pE2);
+
+ if (pE1.equals(pE2)) {
+ addElementAsNewSet(pE1);
+ } else {
+ Set canonicalElements = mapOfSets.keySet();
+
+ if (canonicalElements.contains(pE1)) {
+ if (canonicalElements.contains(pE2)) {
+ mergeExistingSets(pE1, pE2);
+ } else {
+ addElementToExistingSet(pE2, pE1);
+ }
+ } else if (canonicalElements.contains(pE2)) {
+ addElementToExistingSet(pE1, pE2);
+ } else {
+
+ if (contains(pE1)) {
+ if (contains(pE2)) {
+ mergeExistingSets(find(pE1), find(pE2));
+ } else {
+ addElementToExistingSet(pE2, find(pE1));
+ }
+ } else {
+ addElementAsNewSet(pE1);
+ addElementToExistingSet(pE2, pE1);
+ }
+ }
+ }
+ }
+
+ @SuppressWarnings("unchecked")
+ private void addElementAsNewSet(T pE) {
+
+ if (!contains(pE)) {
+ S newSet = (S) getEmptySet();
+ newSet.add(pE);
+ mapOfSets.put(pE, newSet);
+ }
+ }
+
+ private void addElementToExistingSet(T pE, T pCanon) {
+
+ if (!contains(pE)) {
+ mapOfSets.get(pCanon).add(pE);
+ } else {
+ mergeExistingSets(find(pE), pCanon);
+ }
+ }
+
+ // pE1 will be new canonical element only if its set is actually bigger, otherwise pE2 new canon
+ private void mergeExistingSets(T pE1, T pE2) {
+
+ S set1 = mapOfSets.get(pE1);
+ S set2 = mapOfSets.get(pE2);
+
+ assert set1 != null;
+ assert set2 != null;
+
+ int size1 = set1.size();
+ int size2 = set2.size();
+
+ if (size1 > size2) {
+ set1.addAll(set2);
+ assert mapOfSets.remove(pE2, set2);
+ } else {
+ set2.addAll(set1);
+ assert mapOfSets.remove(pE1, set1);
+ }
+ }
+
+ /**
+ * Provides a {@link Collection} containing all current subsets.
+ *
+ * @return {@link Collection} containing all current subsets
+ */
+ @Override
+ public Collection getAllSubsets() {
+ return mapOfSets.values();
+ }
+
+ /**
+ * Checks whether the provided element is contained in any current subset and returns true or
+ * false accordingly.
+ *
+ * @param pE element to be searched for
+ * @return true if contained, false if not
+ */
+ @Override
+ public boolean contains(T pE) {
+
+ Preconditions.checkNotNull(pE);
+
+ for (S current : mapOfSets.values()) {
+ if (current.contains(pE)) {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ protected abstract Set getEmptySet();
+
+ protected abstract Map> getEmptyMap();
+}
diff --git a/src/org/sosy_lab/common/collect/union_find/AbstractImmutableParentPointerTreeBuilder.java b/src/org/sosy_lab/common/collect/union_find/AbstractImmutableParentPointerTreeBuilder.java
new file mode 100644
index 000000000..c9ba77f8e
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/AbstractImmutableParentPointerTreeBuilder.java
@@ -0,0 +1,80 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find;
+
+import com.google.errorprone.annotations.CanIgnoreReturnValue;
+import com.google.errorprone.annotations.Immutable;
+import java.util.Collection;
+import java.util.Set;
+import org.sosy_lab.common.collect.union_find.ParentPointerTreeUnionFind.UnionType;
+
+/**
+ * Abstract builder class which first collects the data in a mutable Union-Find and converts it to
+ * an immutable Union-Find when {@code build()} is called. From then onward, previously modifying
+ * methods will not cause further modifications to the Union-Find instance inside. See documentation
+ * in {@link ParentPointerTreeUnionFind} for explanations on {@code union()}, {@code add()} and
+ * {@code addAll()} as the methods in this builder simply pass to their aforementioned namesakes.
+ *
+ * @param type of elements added to the Union-Find
+ */
+@Immutable(containerOf = "T")
+public abstract class AbstractImmutableParentPointerTreeBuilder {
+
+ // union-find not immutable but only used internally and never mutated passed outward
+ // build() returns an immutable union-find that contains a copy of this union-find's map
+ @SuppressWarnings("Immutable")
+ final ParentPointerTreeUnionFind unionFind;
+
+ // prevents further modifications after build()
+ // is never modified once having been switched to false
+ @SuppressWarnings("Immutable")
+ boolean modificationsAllowed;
+
+ protected AbstractImmutableParentPointerTreeBuilder(UnionType pUnionType) {
+ unionFind = new ParentPointerTreeUnionFind<>(pUnionType);
+ modificationsAllowed = true;
+ }
+
+ @CanIgnoreReturnValue
+ public AbstractImmutableParentPointerTreeBuilder union(T pE1, T pE2) {
+
+ if (modificationsAllowed) {
+
+ unionFind.union(pE1, pE2);
+ }
+
+ return this;
+ }
+
+ @CanIgnoreReturnValue
+ public AbstractImmutableParentPointerTreeBuilder add(Set pSet) {
+
+ if (modificationsAllowed) {
+
+ unionFind.add(pSet);
+ }
+
+ return this;
+ }
+
+ @CanIgnoreReturnValue
+ public AbstractImmutableParentPointerTreeBuilder addAll(Collection> pSets) {
+
+ if (modificationsAllowed) {
+
+ unionFind.addAll(pSets);
+ }
+
+ return this;
+ }
+
+ // get map from mutable Union-Find instance and convert to immutable map, then pass to constructor
+ // set modificationsAllowed to false!!
+ public abstract AbstractImmutableUnionFind build();
+}
diff --git a/src/org/sosy_lab/common/collect/union_find/AbstractImmutableSortedUnionFind.java b/src/org/sosy_lab/common/collect/union_find/AbstractImmutableSortedUnionFind.java
new file mode 100644
index 000000000..dab872d08
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/AbstractImmutableSortedUnionFind.java
@@ -0,0 +1,20 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find;
+
+import com.google.errorprone.annotations.Immutable;
+
+/**
+ * An abstract class for sorted immutable Union-Find implementations.
+ *
+ * @param type of elements added to the Union-Find. Must be comparable.
+ */
+@Immutable(containerOf = "T")
+public abstract class AbstractImmutableSortedUnionFind>
+ extends AbstractImmutableUnionFind implements SortedUnionFind {}
diff --git a/src/org/sosy_lab/common/collect/union_find/AbstractImmutableUnionFind.java b/src/org/sosy_lab/common/collect/union_find/AbstractImmutableUnionFind.java
new file mode 100644
index 000000000..940b1903c
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/AbstractImmutableUnionFind.java
@@ -0,0 +1,28 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find;
+
+import com.google.errorprone.annotations.DoNotCall;
+import com.google.errorprone.annotations.Immutable;
+
+/**
+ * An abstract class for immutable Union-Find implementations.
+ *
+ * @param type of elements added to the Union-Find
+ */
+@Immutable(containerOf = "T")
+public abstract class AbstractImmutableUnionFind implements UnionFind {
+
+ @Deprecated
+ @Override
+ @DoNotCall
+ public final void union(T pE1, T pE2) {
+ throw new UnsupportedOperationException();
+ }
+}
diff --git a/src/org/sosy_lab/common/collect/union_find/AbstractTreeNode.java b/src/org/sosy_lab/common/collect/union_find/AbstractTreeNode.java
new file mode 100644
index 000000000..b8351c0dc
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/AbstractTreeNode.java
@@ -0,0 +1,55 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find;
+
+/**
+ * An abstract class of nodes from which a simple parent pointer tree can be built.
+ *
+ * @param type of elements each node holds as value
+ */
+public abstract class AbstractTreeNode {
+
+ private AbstractTreeNode parent;
+ private final T value;
+
+ /**
+ * Constructor for a root node. The parent variable points to itself, thus indicating this is a
+ * root node. If appended to another tree, parent can be reallocated to the new parent node, while
+ * the current node simply functions as a non-root node from then on.
+ *
+ * @param pValue element to be stored in the node
+ */
+ protected AbstractTreeNode(T pValue) {
+ parent = this;
+ value = pValue;
+ }
+
+ /**
+ * Constructor for a non-root node.
+ *
+ * @param pParent pParent node (can be root or non-root)
+ * @param pValue element to be stored in the node
+ */
+ protected AbstractTreeNode(AbstractTreeNode pParent, T pValue) {
+ parent = pParent;
+ value = pValue;
+ }
+
+ public AbstractTreeNode getParent() {
+ return parent;
+ }
+
+ public void setParent(AbstractTreeNode pParent) {
+ parent = pParent;
+ }
+
+ public T getValue() {
+ return value;
+ }
+}
diff --git a/src/org/sosy_lab/common/collect/union_find/ImmutableParentPointerTreeUnionFind.java b/src/org/sosy_lab/common/collect/union_find/ImmutableParentPointerTreeUnionFind.java
new file mode 100644
index 000000000..32c367466
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/ImmutableParentPointerTreeUnionFind.java
@@ -0,0 +1,143 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find;
+
+import com.google.common.base.Preconditions;
+import com.google.common.collect.ImmutableMap;
+import com.google.errorprone.annotations.Immutable;
+import com.google.errorprone.annotations.Var;
+import java.util.Collection;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Map;
+import java.util.Set;
+import org.sosy_lab.common.collect.union_find.ParentPointerTreeUnionFind.UnionType;
+
+/**
+ * An implementation of {@link UnionFind} using a {@link ImmutableMap} of each element to its {@link
+ * AbstractTreeNode}. Each node contains a reference to its respective parent node, thus resulting
+ * in a parent pointer tree structure for each subset. These are each represented by canonical
+ * elements which are the root of each tree. This is always the first element added to the subset,
+ * unless it has changed due to union operations. The union can be performed either by size or by
+ * rank, * determined by a constructor parameter.
+ *
+ * @param type of elements added to the Union-Find.
+ */
+@Immutable(containerOf = "T")
+public class ImmutableParentPointerTreeUnionFind extends AbstractImmutableUnionFind {
+
+ // tree nodes are not immutable but only used internally and never mutated after creation
+ // immutable tree nodes would make conversion during build() difficult and time-consuming
+ @SuppressWarnings("Immutable")
+ private final ImmutableMap> allNodes;
+
+ /**
+ * Only for internal use by the builder.
+ *
+ * @param pAllNodes finished immutable map storing all nodes contained in this Union-Find
+ */
+ protected ImmutableParentPointerTreeUnionFind(ImmutableMap> pAllNodes) {
+ allNodes = pAllNodes;
+ }
+
+ /**
+ * Returns the canonical element of the set containing the provided element.
+ *
+ * @param pE element for which set is to be found
+ * @return canonical element of the found set
+ * @throws IllegalArgumentException if element is not contained in any subset
+ */
+ @Override
+ public T find(T pE) {
+
+ Preconditions.checkNotNull(pE);
+
+ @Var AbstractTreeNode node = allNodes.get(pE);
+
+ if (node != null) {
+ @Var AbstractTreeNode parent = node.getParent();
+
+ while (!node.equals(parent)) {
+ node = parent;
+ parent = node.getParent();
+ }
+
+ return parent.getValue();
+ }
+
+ throw new IllegalArgumentException("Element not contained.");
+ }
+
+ /**
+ * Provides a {@link Collection} containing all current subsets.
+ *
+ * @return {@link Collection} containing all current subsets
+ */
+ @Override
+ public Collection extends Set> getAllSubsets() {
+
+ Map> allSubsets = new HashMap<>();
+
+ for (AbstractTreeNode node : allNodes.values()) {
+
+ T canon = find(node.getValue());
+
+ if (allSubsets.containsKey(canon)) {
+ allSubsets.get(canon).add(node.getValue());
+ } else {
+ Set set = new HashSet<>();
+ set.add(node.getValue());
+ allSubsets.put(canon, set);
+ }
+ }
+
+ return allSubsets.values();
+ }
+
+ /**
+ * Checks whether the provided element is contained in any current subset and returns true or
+ * false accordingly.
+ *
+ * @param pE element to be searched for
+ * @return true if contained, false if not
+ */
+ @Override
+ public boolean contains(T pE) {
+
+ return allNodes.containsKey(pE);
+ }
+
+ /**
+ * Builder class which first collects the data in a mutable Union-Find and converts it to an
+ * immutable Union-Find when {@code build()} is called. See documentation in {@link
+ * ParentPointerTreeUnionFind} for explanations on {@code union()}, {@code add()} and {@code
+ * addAll()} as the methods in this builder simply pass to their aforementioned namesakes.
+ *
+ * @param type of elements added to the Union-Find
+ */
+ public static final class Builder extends AbstractImmutableParentPointerTreeBuilder {
+
+ private Builder(UnionType pUnionType) {
+ super(pUnionType);
+ }
+
+ public static AbstractImmutableParentPointerTreeBuilder getBuilder(
+ UnionType pUnionType) {
+ return new Builder<>(pUnionType);
+ }
+
+ @Override
+ public ImmutableParentPointerTreeUnionFind build() {
+
+ modificationsAllowed = false;
+
+ return new ImmutableParentPointerTreeUnionFind<>(ImmutableMap.copyOf(unionFind.allNodes));
+ }
+ }
+}
diff --git a/src/org/sosy_lab/common/collect/union_find/ImmutableSortedParentPointerTreeUnionFind.java b/src/org/sosy_lab/common/collect/union_find/ImmutableSortedParentPointerTreeUnionFind.java
new file mode 100644
index 000000000..06e3050fa
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/ImmutableSortedParentPointerTreeUnionFind.java
@@ -0,0 +1,149 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find;
+
+import com.google.common.base.Preconditions;
+import com.google.common.collect.ImmutableMap;
+import com.google.errorprone.annotations.Immutable;
+import com.google.errorprone.annotations.Var;
+import java.util.Collection;
+import java.util.NavigableMap;
+import java.util.NavigableSet;
+import java.util.TreeMap;
+import java.util.TreeSet;
+import org.sosy_lab.common.collect.union_find.ParentPointerTreeUnionFind.UnionType;
+
+/**
+ * A sorted implementation of {@link UnionFind} using a {@link ImmutableMap} of each element to its
+ * {@link AbstractTreeNode}. Each node contains a reference to its respective parent node, thus
+ * resulting in a parent pointer tree structure for each subset. These are each represented by
+ * canonical elements which are the root of each tree. This is always the first element added to the
+ * subset, unless it has changed due to union operations. The union can be performed either by size
+ * or by rank, * determined by a constructor parameter. The elements are stored in unsorted
+ * structures, but {@code getAllSubsets()} returns a sorted view.
+ *
+ * @param type of elements added to the Union-Find. Must be comparable.
+ */
+@Immutable(containerOf = "T")
+public class ImmutableSortedParentPointerTreeUnionFind>
+ extends AbstractImmutableSortedUnionFind {
+
+ // tree nodes are not immutable but only used internally and never mutated after creation
+ // immutable tree nodes would make conversion during build() difficult and time-consuming
+ @SuppressWarnings("Immutable")
+ private final ImmutableMap> allNodes;
+
+ /**
+ * Only for internal use by the builder.
+ *
+ * @param pAllNodes finished immutable map storing all nodes contained in this Union-Find
+ */
+ protected ImmutableSortedParentPointerTreeUnionFind(
+ ImmutableMap> pAllNodes) {
+ allNodes = pAllNodes;
+ }
+
+ /**
+ * Returns the canonical element of the set containing the provided element.
+ *
+ * @param pE element for which set is to be found
+ * @return canonical element of the found set
+ * @throws IllegalArgumentException if element is not contained in any subset
+ */
+ @Override
+ public T find(T pE) {
+
+ Preconditions.checkNotNull(pE);
+
+ @Var AbstractTreeNode node = allNodes.get(pE);
+
+ if (node != null) {
+ @Var AbstractTreeNode parent = node.getParent();
+
+ while (!node.equals(parent)) {
+ node = parent;
+ parent = node.getParent();
+ }
+
+ return parent.getValue();
+ }
+
+ throw new IllegalArgumentException("Element not contained.");
+ }
+
+ /**
+ * Provides a {@link Collection} containing all current subsets. The subsets are sorted by their
+ * canonical elements in ascending order. The contents of each subset are equally sorted in
+ * ascending order.
+ *
+ * @return {@link Collection} containing all current subsets
+ */
+ @Override
+ public Collection extends NavigableSet> getAllSubsets() {
+
+ NavigableMap> allSubsets = new TreeMap<>();
+
+ for (AbstractTreeNode node : allNodes.values()) {
+
+ T canon = find(node.getValue());
+
+ if (allSubsets.containsKey(canon)) {
+ allSubsets.get(canon).add(node.getValue());
+ } else {
+ NavigableSet set = new TreeSet<>();
+ set.add(node.getValue());
+ allSubsets.put(canon, set);
+ }
+ }
+
+ return allSubsets.values();
+ }
+
+ /**
+ * Checks whether the provided element is contained in any current subset and returns true or
+ * false accordingly.
+ *
+ * @param pE element to be searched for
+ * @return true if contained, false if not
+ */
+ @Override
+ public boolean contains(T pE) {
+
+ return allNodes.containsKey(pE);
+ }
+
+ /**
+ * Builder class which first collects the data in a mutable sorted Union-Find and converts it to
+ * an immutable Union-Find when {@code build()} is called. See documentation in {@link
+ * ParentPointerTreeUnionFind} for explanations on {@code union()}, {@code add()} and {@code
+ * addAll()} as the methods in this builder simply pass to their aforementioned namesakes.
+ *
+ * @param type of elements added to the Union-Find
+ */
+ public static final class Builder>
+ extends AbstractImmutableParentPointerTreeBuilder {
+
+ private Builder(UnionType pUnionType) {
+ super(pUnionType);
+ }
+
+ public static > Builder getBuilder(UnionType pUnionType) {
+ return new Builder<>(pUnionType);
+ }
+
+ @Override
+ public ImmutableSortedParentPointerTreeUnionFind build() {
+
+ modificationsAllowed = false;
+
+ return new ImmutableSortedParentPointerTreeUnionFind<>(
+ ImmutableMap.copyOf(unionFind.allNodes));
+ }
+ }
+}
diff --git a/src/org/sosy_lab/common/collect/union_find/NonRootNode.java b/src/org/sosy_lab/common/collect/union_find/NonRootNode.java
new file mode 100644
index 000000000..e318015b3
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/NonRootNode.java
@@ -0,0 +1,28 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find;
+
+/**
+ * An implementation of {@link AbstractTreeNode} resulting in nodes that can only be used as
+ * non-root nodes but not as root nodes.
+ *
+ * @param type of elements each node holds as value
+ */
+public final class NonRootNode extends AbstractTreeNode {
+
+ /**
+ * Constructor for a non-root node.
+ *
+ * @param pParent parent node (can be root or non-root)
+ * @param pValue element to be stored in the node
+ */
+ public NonRootNode(AbstractTreeNode pParent, T pValue) {
+ super(pParent, pValue);
+ }
+}
diff --git a/src/org/sosy_lab/common/collect/union_find/ParentPointerTreeUnionFind.java b/src/org/sosy_lab/common/collect/union_find/ParentPointerTreeUnionFind.java
new file mode 100644
index 000000000..74ef081d7
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/ParentPointerTreeUnionFind.java
@@ -0,0 +1,302 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find;
+
+import com.google.common.base.Preconditions;
+import com.google.errorprone.annotations.Var;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+
+/**
+ * An implementation of {@link UnionFind} using a {@link Map} of {@link AbstractTreeNode}s. In order
+ * to represent subsets by canonical elements, each one is mapped to its representative canonical
+ * element. This is always the first element added to the subset, unless it has changed due to union
+ * operations. Each subset is stored as a parent pointer tree comprised of {@link NonRootNode}s with
+ * exactly one {@link RootNode} as the root. The union can be performed either by size or by rank,
+ * determined by a constructor parameter.
+ *
+ * @param type of elements added to the Union-Find.
+ */
+public class ParentPointerTreeUnionFind implements UnionFind {
+
+ public enum UnionType {
+ UNION_BY_RANK,
+ UNION_BY_SIZE
+ }
+
+ protected final Map> allNodes;
+ private final UnionType unionType;
+
+ /**
+ * Creates an empty instance.
+ *
+ * @param pUnionType type of union to be performed for all unions on this instance
+ */
+ public ParentPointerTreeUnionFind(UnionType pUnionType) {
+ allNodes = new HashMap<>();
+ unionType = pUnionType;
+ }
+
+ /**
+ * Returns the canonical element of the set containing the provided element. Applies path
+ * compression where possible.
+ *
+ * @param pE element for which set is to be found
+ * @return canonical element of the found set
+ * @throws IllegalArgumentException if element is not contained in any subset
+ */
+ @Override
+ public T find(T pE) {
+
+ Preconditions.checkNotNull(pE);
+
+ List> toBeCompressed = new ArrayList<>();
+ @Var AbstractTreeNode node = allNodes.get(pE);
+
+ if (node != null) {
+ @Var AbstractTreeNode parent = node.getParent();
+
+ while (!node.equals(parent)) {
+ toBeCompressed.add(node);
+ node = parent;
+ parent = node.getParent();
+ }
+
+ for (AbstractTreeNode current : toBeCompressed) {
+
+ current.setParent(parent);
+ }
+
+ return parent.getValue();
+ }
+
+ throw new IllegalArgumentException("Element not contained.");
+ }
+
+ /**
+ * Merges the sets represented by the two input values according to standard Union-Find behaviour.
+ *
+ * USES: Add new element as new set: pass it as both pE1 and pE2. Add new element to existing
+ * set: one input value is the new element, the other the canonical element of the set to be added
+ * to. Merge two existing sets: pE1, pE2 canonical elements of sets to be merged.
+ *
+ * @param pE1 first element
+ * @param pE2 second element
+ */
+ @Override
+ public void union(T pE1, T pE2) {
+
+ Preconditions.checkNotNull(pE1);
+ Preconditions.checkNotNull(pE2);
+
+ if (pE1.equals(pE2)) {
+ addElementAsNewSet(pE1);
+ } else {
+ if (contains(pE1)) {
+ if (contains(pE2)) {
+ T canon1 = find(pE1);
+ T canon2 = find(pE2);
+
+ if (!canon1.equals(canon2)) {
+ mergeExistingSets(findNode(canon1), findNode(canon2));
+ }
+ } else {
+ addElementToExistingSet(pE2, findNode(pE1));
+ }
+ } else if (contains(pE2)) {
+ addElementToExistingSet(pE1, findNode(pE2));
+ } else {
+ addElementAsNewSet(pE1);
+ addElementToExistingSet(pE2, findNode(pE1));
+ }
+ }
+ }
+
+ /**
+ * Provides a {@link Collection} containing all current subsets.
+ *
+ * @return {@link Collection} containing all current subsets
+ */
+ @Override
+ public Collection extends Set> getAllSubsets() {
+
+ Map> allSubsets = new HashMap<>();
+
+ for (AbstractTreeNode node : allNodes.values()) {
+
+ T canon = find(node.getValue());
+
+ if (allSubsets.containsKey(canon)) {
+ allSubsets.get(canon).add(node.getValue());
+ } else {
+ Set set = new HashSet<>();
+ set.add(canon);
+ set.add(node.getValue());
+ allSubsets.put(canon, set);
+ }
+ }
+
+ return allSubsets.values();
+ }
+
+ /**
+ * Checks whether the provided element is contained in any current subset and returns true or
+ * false accordingly.
+ *
+ * @param pE element to be searched for
+ * @return true if contained, false if not
+ */
+ @Override
+ public boolean contains(T pE) {
+
+ return allNodes.containsKey(pE);
+ }
+
+ /**
+ * Adds the contents of a set of elements to the Union-Find. A random element in the set (the
+ * first one accessed) will be used as the canonical element. If the set contains elements already
+ * found elsewhere in the Union-Find, these sets will be merged accordingly.
+ *
+ * @param pSet set to be added to the Union-Find
+ */
+ public void add(Set pSet) {
+
+ Preconditions.checkNotNull(pSet);
+
+ @Var T canon = null;
+
+ for (T current : pSet) {
+
+ if (canon == null) {
+ canon = current;
+ addElementAsNewSet(canon);
+ }
+
+ addElementToExistingSet(current, findNode(canon));
+ }
+ }
+
+ /**
+ * Adds multiple sets of elements to the Union-Find. For each set, a random element in the set
+ * (the first one accessed) will be used as the canonical element. If a set contains elements
+ * already found elsewhere in the Union-Find, these sets will be merged accordingly.
+ *
+ * @param pSets sets to be added to the Union-Find
+ */
+ public void addAll(Collection> pSets) {
+
+ Preconditions.checkNotNull(pSets);
+
+ for (Set set : pSets) {
+ add(set);
+ }
+ }
+
+ private void addElementAsNewSet(T pE) {
+
+ if (!contains(pE)) {
+ RootNode root = new RootNode<>(pE);
+ allNodes.put(pE, root);
+ }
+ }
+
+ // only call with elements that are definitely canonical!
+ private void mergeExistingSets(RootNode pCanon1, RootNode pCanon2) {
+
+ Preconditions.checkNotNull(pCanon1);
+ Preconditions.checkNotNull(pCanon2);
+
+ if (unionType == UnionType.UNION_BY_SIZE) {
+ unionBySize(pCanon1, pCanon2);
+ } else {
+ unionByRank(pCanon1, pCanon2);
+ }
+ }
+
+ private void addElementToExistingSet(T pE, RootNode pCanon) {
+
+ NonRootNode newNode = new NonRootNode<>(pCanon, pE);
+ pCanon.incrementSizeByOne();
+
+ if (pCanon.getRank() == 0) {
+ pCanon.incrementRankByOne();
+ }
+
+ allNodes.put(pE, newNode);
+ }
+
+ // pCanon1 will be new canonical element only if its set is actually bigger, otherwise pCanon2 new
+ // canon
+ private void unionBySize(RootNode pCanon1, RootNode pCanon2) {
+
+ int size1 = pCanon1.getSize();
+ int size2 = pCanon2.getSize();
+
+ if (size1 > size2) {
+ pCanon2.setParent(pCanon1);
+ pCanon1.incrementSizeBy(pCanon2.getSize());
+ } else {
+ pCanon1.setParent(pCanon2);
+ pCanon2.incrementSizeBy(pCanon1.getSize());
+ }
+ }
+
+ // pCanon1 will be new canonical element only if its rank is actually greater, otherwise pCanon2
+ // new
+ // canon
+ private void unionByRank(RootNode pCanon1, RootNode pCanon2) {
+
+ int rank1 = pCanon1.getRank();
+ int rank2 = pCanon2.getRank();
+
+ if (rank1 > rank2) {
+ pCanon2.setParent(pCanon1);
+ } else {
+ pCanon1.setParent(pCanon2);
+
+ // as rank only changes if both ranks are the same
+ if (rank1 == rank2) {
+ pCanon2.incrementRankByOne();
+ }
+ }
+ }
+
+ // like find; returns node of canonical element of the set pE belongs to, not value
+ private RootNode findNode(T pE) {
+
+ Preconditions.checkNotNull(pE);
+
+ List> toBeCompressed = new ArrayList<>();
+ @Var AbstractTreeNode node = allNodes.get(pE);
+
+ if (node != null) {
+ @Var AbstractTreeNode parent = node.getParent();
+
+ while (!node.equals(parent)) {
+ toBeCompressed.add(node);
+ node = parent;
+ parent = node.getParent();
+ }
+
+ for (AbstractTreeNode current : toBeCompressed) {
+
+ current.setParent(parent);
+ }
+
+ return (RootNode) parent;
+ }
+
+ throw new IllegalArgumentException("Element not contained.");
+ }
+}
diff --git a/src/org/sosy_lab/common/collect/union_find/PersistentParentPointerTreeUnionFind.java b/src/org/sosy_lab/common/collect/union_find/PersistentParentPointerTreeUnionFind.java
new file mode 100644
index 000000000..d645e31ee
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/PersistentParentPointerTreeUnionFind.java
@@ -0,0 +1,306 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find;
+
+import com.google.common.base.Preconditions;
+import com.google.errorprone.annotations.CheckReturnValue;
+import com.google.errorprone.annotations.Immutable;
+import com.google.errorprone.annotations.Var;
+import java.util.Collection;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Map;
+import java.util.Set;
+import org.sosy_lab.common.collect.union_find.ParentPointerTreeUnionFind.UnionType;
+
+/**
+ * Implementation of a persistent union-find. A persistent data structure is immutable, but provides
+ * cheap copy-and-write operations. Thus, all write operations ({@link #union(Object, Object)}) will
+ * not modify the current instance, but return a new instance instead. The union can be performed
+ * either by size or by rank, determined by a constructor parameter.
+ *
+ * All modifying operations inherited from {@link UnionFind} are not supported and will always
+ * throw {@link UnsupportedOperationException}.
+ *
+ * @param The type of elements added to the Union-Find.
+ */
+@Immutable(containerOf = "T")
+public final class PersistentParentPointerTreeUnionFind extends AbstractImmutableUnionFind
+ implements PersistentUnionFind {
+
+ // map only used internally and never mutated after creation
+ // TODO convert to ImmutableMap once Guava upgraded to 31.1 and buildKeepingLast() available
+ @SuppressWarnings("Immutable")
+ private final Map mapOfNodesToParents;
+
+ // map only used internally and never mutated after creation
+ // TODO convert to ImmutableMap once Guava upgraded to 31.1 and buildKeepingLast() available
+ @SuppressWarnings("Immutable")
+ private final Map mapOfRootsToWeights;
+
+ private final UnionType unionType;
+
+ private PersistentParentPointerTreeUnionFind(UnionType pUnionType) {
+ mapOfNodesToParents = new HashMap<>();
+ mapOfRootsToWeights = new HashMap<>();
+ unionType = pUnionType;
+ }
+
+ private PersistentParentPointerTreeUnionFind(
+ Map pMapOfNodesToParents, Map pMapOfRootsToWeights, UnionType pUnionType) {
+ mapOfNodesToParents = pMapOfNodesToParents;
+ mapOfRootsToWeights = pMapOfRootsToWeights;
+ unionType = pUnionType;
+ }
+
+ /**
+ * Returns a fresh, empty Union-Find instance of the given union type.
+ *
+ * @param pUnionType specifies whether the union is performed by rank or by size
+ * @return empty instance
+ * @param type of elements added to the Union-Find.
+ */
+ public static PersistentUnionFind of(UnionType pUnionType) {
+ return new PersistentParentPointerTreeUnionFind<>(pUnionType);
+ }
+
+ /**
+ * Provides a {@link Collection} containing all current subsets.
+ *
+ * @return {@link Collection} containing all current subsets
+ */
+ @Override
+ public Collection extends Set> getAllSubsets() {
+
+ Map> allSubsets = new HashMap<>();
+
+ for (T current : mapOfNodesToParents.keySet()) {
+
+ T root = find(current);
+
+ if (allSubsets.containsKey(root)) {
+ allSubsets.get(root).add(current);
+ } else {
+ Set set = new HashSet<>();
+ set.add(root);
+ set.add(current);
+ allSubsets.put(root, set);
+ }
+ }
+
+ return allSubsets.values();
+ }
+
+ /**
+ * Checks whether the provided element is contained in any current subset and returns true or
+ * false accordingly.
+ *
+ * @param pE element to be searched for
+ * @return true if contained, false if not
+ */
+ @Override
+ public boolean contains(T pE) {
+
+ Preconditions.checkNotNull(pE);
+
+ return mapOfNodesToParents.containsKey(pE);
+ }
+
+ /**
+ * Returns the canonical element of the set containing the provided element.
+ *
+ * @param pE element for which set is to be found
+ * @return canonical element of the found set
+ * @throws IllegalArgumentException if element is not contained in any subset
+ */
+ @Override
+ public T find(T pE) {
+
+ Preconditions.checkNotNull(pE);
+
+ @Var T currentNode = pE;
+ @Var T parent = mapOfNodesToParents.get(pE);
+
+ if (parent != null) {
+ while (!currentNode.equals(parent)) {
+ currentNode = parent;
+ parent = mapOfNodesToParents.get(currentNode);
+ }
+
+ return parent;
+ }
+
+ throw new IllegalArgumentException("Element not contained.");
+ }
+
+ /**
+ * Merges the sets represented by the two input values according to standard Union-Find behaviour.
+ * This operation does not mutate the existing object, but returns a fresh instance to which the
+ * changes in question have been applied.
+ *
+ * USES: Add new element as new set: pass it as both pE1 and pE2. Add new element to existing
+ * set: one input value is the new element, the other the canonical element of the set to be added
+ * to. Merge two existing sets: pE1, pE2 canonical elements of sets to be merged.
+ *
+ * @param pE1 first element
+ * @param pE2 second element
+ */
+ @CheckReturnValue
+ @Override
+ public PersistentUnionFind unionAndCopy(T pE1, T pE2) {
+
+ Preconditions.checkNotNull(pE1);
+ Preconditions.checkNotNull(pE2);
+
+ if (pE1.equals(pE2)) {
+ return addElementAsNewSetAndCopy(pE1);
+ } else {
+ if (contains(pE1)) {
+ if (contains(pE2)) {
+ T canon1 = find(pE1);
+ T canon2 = find(pE2);
+
+ if (!canon1.equals(canon2)) {
+ return mergeExistingSetsAndCopy(canon1, canon2);
+ }
+ } else {
+ return addElementToExistingSetAndCopy(pE2, find(pE1));
+ }
+ } else if (contains(pE2)) {
+ return addElementToExistingSetAndCopy(pE1, find(pE2));
+ } else {
+ return addTwoElementsAsSetAndCopy(pE1, pE2);
+ }
+ }
+
+ return this;
+ }
+
+ private PersistentUnionFind addElementAsNewSetAndCopy(T pE) {
+
+ if (!contains(pE)) {
+ Map updatedNodesToParents = new HashMap<>(mapOfNodesToParents);
+ updatedNodesToParents.put(pE, pE);
+
+ Map updatedRootsToWeights = new HashMap<>(mapOfRootsToWeights);
+ if (unionType == UnionType.UNION_BY_RANK) {
+ updatedRootsToWeights.put(pE, 0); // rank
+ } else {
+ updatedRootsToWeights.put(pE, 1); // size
+ }
+
+ return new PersistentParentPointerTreeUnionFind<>(
+ updatedNodesToParents, updatedRootsToWeights, unionType);
+ }
+
+ return this;
+ }
+
+ // only call with elements that are definitely canonical!
+ private PersistentUnionFind mergeExistingSetsAndCopy(T pCanon1, T pCanon2) {
+
+ Preconditions.checkNotNull(pCanon1);
+ Preconditions.checkNotNull(pCanon2);
+
+ if (unionType == UnionType.UNION_BY_SIZE) {
+ return unionBySize(pCanon1, pCanon2);
+ } else {
+ return unionByRank(pCanon1, pCanon2);
+ }
+ }
+
+ private PersistentUnionFind addElementToExistingSetAndCopy(T pE, T pCanon) {
+
+ Preconditions.checkNotNull(pCanon);
+
+ Map updatedNodesToParents = new HashMap<>(mapOfNodesToParents);
+ updatedNodesToParents.put(pE, pCanon);
+
+ Map updatedRootsToWeights = new HashMap<>(mapOfRootsToWeights);
+ if (unionType == UnionType.UNION_BY_RANK) {
+ @Var int rank = mapOfRootsToWeights.get(pCanon);
+
+ if (rank == 0) {
+ updatedRootsToWeights.put(pCanon, ++rank);
+ }
+ } else {
+ @Var int size = mapOfRootsToWeights.get(pCanon);
+ updatedRootsToWeights.put(pCanon, ++size);
+ }
+
+ return new PersistentParentPointerTreeUnionFind<>(
+ updatedNodesToParents, updatedRootsToWeights, unionType);
+ }
+
+ private PersistentUnionFind addTwoElementsAsSetAndCopy(T pE1, T pE2) {
+
+ Map updatedNodesToParents = new HashMap<>(mapOfNodesToParents);
+ updatedNodesToParents.put(pE1, pE1);
+ updatedNodesToParents.put(pE2, pE1);
+
+ Map updatedRootsToWeights = new HashMap<>(mapOfRootsToWeights);
+ if (unionType == UnionType.UNION_BY_RANK) {
+ updatedRootsToWeights.put(pE1, 1); // rank
+ } else {
+ updatedRootsToWeights.put(pE1, 2); // size
+ }
+
+ return new PersistentParentPointerTreeUnionFind<>(
+ updatedNodesToParents, updatedRootsToWeights, unionType);
+ }
+
+ // pCanon1 will be new canonical element only if its set is actually bigger, otherwise pCanon2 new
+ // canon
+ private PersistentUnionFind unionBySize(T pCanon1, T pCanon2) {
+
+ int size1 = mapOfRootsToWeights.get(pCanon1);
+ int size2 = mapOfRootsToWeights.get(pCanon2);
+
+ Map updatedNodesToParents = new HashMap<>(mapOfNodesToParents);
+ Map updatedRootsToWeights = new HashMap<>(mapOfRootsToWeights);
+
+ if (size1 > size2) {
+ updatedNodesToParents.put(pCanon2, pCanon1);
+
+ updatedRootsToWeights.put(pCanon1, size1 + size2);
+ } else {
+ updatedNodesToParents.put(pCanon1, pCanon2);
+
+ updatedRootsToWeights.put(pCanon2, size2 + size1);
+ }
+
+ return new PersistentParentPointerTreeUnionFind<>(
+ updatedNodesToParents, updatedRootsToWeights, unionType);
+ }
+
+ // pCanon1 will be new canonical element only if its rank is actually greater, otherwise pCanon2
+ // new
+ // canon
+ private PersistentUnionFind unionByRank(T pCanon1, T pCanon2) {
+
+ int rank1 = mapOfRootsToWeights.get(pCanon1);
+ @Var int rank2 = mapOfRootsToWeights.get(pCanon2);
+
+ Map updatedNodesToParents = new HashMap<>(mapOfNodesToParents);
+ Map updatedRootsToWeights = new HashMap<>(mapOfRootsToWeights);
+
+ if (rank1 > rank2) {
+ updatedNodesToParents.put(pCanon2, pCanon1);
+ } else {
+ updatedNodesToParents.put(pCanon1, pCanon2);
+
+ if (rank1 == rank2) {
+ updatedRootsToWeights.put(pCanon2, ++rank2);
+ }
+ }
+
+ return new PersistentParentPointerTreeUnionFind<>(
+ updatedNodesToParents, updatedRootsToWeights, unionType);
+ }
+}
diff --git a/src/org/sosy_lab/common/collect/union_find/PersistentSortedParentPointerTreeUnionFind.java b/src/org/sosy_lab/common/collect/union_find/PersistentSortedParentPointerTreeUnionFind.java
new file mode 100644
index 000000000..e22051447
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/PersistentSortedParentPointerTreeUnionFind.java
@@ -0,0 +1,309 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find;
+
+import com.google.common.base.Preconditions;
+import com.google.errorprone.annotations.CheckReturnValue;
+import com.google.errorprone.annotations.Immutable;
+import com.google.errorprone.annotations.Var;
+import java.util.Collection;
+import java.util.NavigableMap;
+import java.util.NavigableSet;
+import java.util.TreeMap;
+import java.util.TreeSet;
+import org.sosy_lab.common.collect.PathCopyingPersistentTreeMap;
+import org.sosy_lab.common.collect.PersistentSortedMap;
+import org.sosy_lab.common.collect.union_find.ParentPointerTreeUnionFind.UnionType;
+
+/**
+ * Implementation of a persistent and sorted union-find. A persistent data structure is immutable,
+ * but provides cheap copy-and-write operations. Thus, all write operations ({@link
+ * #union(Comparable, Comparable)}) will not modify the current instance, but return a new instance
+ * instead. The union can be performed either by size or by rank, determined by a constructor
+ * parameter.
+ *
+ * All modifying operations inherited from {@link SortedUnionFind} are not supported and will
+ * always throw {@link UnsupportedOperationException}.
+ *
+ * @param The type of elements added to the Union-Find. Must be comparable.
+ */
+@Immutable(containerOf = "T")
+public final class PersistentSortedParentPointerTreeUnionFind>
+ extends AbstractImmutableSortedUnionFind implements PersistentSortedUnionFind {
+
+ private final PersistentSortedMap mapOfNodesToParents;
+ private final PersistentSortedMap mapOfRootsToWeights;
+ private final UnionType unionType;
+
+ private PersistentSortedParentPointerTreeUnionFind(UnionType pUnionType) {
+ mapOfNodesToParents = PathCopyingPersistentTreeMap.of();
+ mapOfRootsToWeights = PathCopyingPersistentTreeMap.of();
+ unionType = pUnionType;
+ }
+
+ private PersistentSortedParentPointerTreeUnionFind(
+ PersistentSortedMap pMapOfNodesToParents,
+ PersistentSortedMap pMapOfRootsToWeights,
+ UnionType pUnionType) {
+ mapOfNodesToParents = pMapOfNodesToParents;
+ mapOfRootsToWeights = pMapOfRootsToWeights;
+ unionType = pUnionType;
+ }
+
+ /**
+ * Returns a fresh, empty Union-Find instance of the given union type.
+ *
+ * @param pUnionType specifies whether the union is performed by rank or by size
+ * @return empty instance
+ * @param type of elements added to the Union-Find. Must be comparable.
+ */
+ public static > PersistentSortedUnionFind of(UnionType pUnionType) {
+ return new PersistentSortedParentPointerTreeUnionFind<>(pUnionType);
+ }
+
+ /**
+ * Provides a {@link Collection} containing all current subsets. The subsets are sorted by their
+ * canonical elements in ascending order. The contents of each subset are equally sorted in
+ * ascending order.
+ *
+ * @return {@link Collection} containing all current subsets
+ */
+ @Override
+ public Collection extends NavigableSet> getAllSubsets() {
+
+ NavigableMap> allSubsets = new TreeMap<>();
+
+ for (T current : mapOfNodesToParents.keySet()) {
+
+ T root = find(current);
+
+ if (allSubsets.containsKey(root)) {
+ allSubsets.get(root).add(current);
+ } else {
+ NavigableSet set = new TreeSet<>();
+ set.add(root);
+ set.add(current);
+ allSubsets.put(root, set);
+ }
+ }
+
+ return allSubsets.values();
+ }
+
+ /**
+ * Checks whether the provided element is contained in any current subset and returns true or
+ * false accordingly.
+ *
+ * @param pE element to be searched for
+ * @return true if contained, false if not
+ */
+ @Override
+ public boolean contains(T pE) {
+
+ Preconditions.checkNotNull(pE);
+
+ return mapOfNodesToParents.containsKey(pE);
+ }
+
+ /**
+ * Returns the canonical element of the set containing the provided element.
+ *
+ * @param pE element for which set is to be found
+ * @return canonical element of the found set
+ * @throws IllegalArgumentException if element is not contained in any subset
+ */
+ @Override
+ public T find(T pE) {
+
+ Preconditions.checkNotNull(pE);
+
+ @Var T currentNode = pE;
+ @Var T parent = mapOfNodesToParents.get(pE);
+
+ if (parent != null) {
+ while (!currentNode.equals(parent)) {
+ currentNode = parent;
+ parent = mapOfNodesToParents.get(currentNode);
+ }
+
+ return parent;
+ }
+
+ throw new IllegalArgumentException("Element not contained.");
+ }
+
+ /**
+ * Merges the sets represented by the two input values according to standard Union-Find behaviour.
+ * This operation does not mutate the existing object, but returns a fresh instance to which the
+ * changes in question have been applied.
+ *
+ * USES: Add new element as new set: pass it as both pE1 and pE2. Add new element to existing
+ * set: one input value is the new element, the other the canonical element of the set to be added
+ * to. Merge two existing sets: pE1, pE2 canonical elements of sets to be merged.
+ *
+ * @param pE1 first element
+ * @param pE2 second element
+ */
+ @CheckReturnValue
+ @Override
+ public PersistentSortedUnionFind unionAndCopy(T pE1, T pE2) {
+
+ Preconditions.checkNotNull(pE1);
+ Preconditions.checkNotNull(pE2);
+
+ if (pE1.equals(pE2)) {
+ return addElementAsNewSetAndCopy(pE1);
+ } else {
+ if (contains(pE1)) {
+ if (contains(pE2)) {
+ T canon1 = find(pE1);
+ T canon2 = find(pE2);
+
+ if (!canon1.equals(canon2)) {
+ return mergeExistingSetsAndCopy(canon1, canon2);
+ }
+ } else {
+ return addElementToExistingSetAndCopy(pE2, find(pE1));
+ }
+ } else if (contains(pE2)) {
+ return addElementToExistingSetAndCopy(pE1, find(pE2));
+ } else {
+ return addTwoElementsAsSetAndCopy(pE1, pE2);
+ }
+ }
+
+ return this;
+ }
+
+ private PersistentSortedUnionFind addElementAsNewSetAndCopy(T pE) {
+
+ if (!contains(pE)) {
+ PersistentSortedMap updatedNodesToParents = mapOfNodesToParents.putAndCopy(pE, pE);
+
+ PersistentSortedMap updatedRootsToWeights;
+ if (unionType == UnionType.UNION_BY_RANK) {
+ updatedRootsToWeights = mapOfRootsToWeights.putAndCopy(pE, 0); // rank
+ } else {
+ updatedRootsToWeights = mapOfRootsToWeights.putAndCopy(pE, 1); // size
+ }
+
+ return new PersistentSortedParentPointerTreeUnionFind<>(
+ updatedNodesToParents, updatedRootsToWeights, unionType);
+ }
+
+ return this;
+ }
+
+ // only call with elements that are definitely canonical!
+ private PersistentSortedUnionFind mergeExistingSetsAndCopy(T pCanon1, T pCanon2) {
+
+ Preconditions.checkNotNull(pCanon1);
+ Preconditions.checkNotNull(pCanon2);
+
+ if (unionType == UnionType.UNION_BY_SIZE) {
+ return unionBySize(pCanon1, pCanon2);
+ } else {
+ return unionByRank(pCanon1, pCanon2);
+ }
+ }
+
+ private PersistentSortedUnionFind addElementToExistingSetAndCopy(T pE, T pCanon) {
+
+ Preconditions.checkNotNull(pCanon);
+
+ PersistentSortedMap updatedNodesToParents = mapOfNodesToParents.putAndCopy(pE, pCanon);
+
+ PersistentSortedMap updatedRootsToWeights;
+ if (unionType == UnionType.UNION_BY_RANK) {
+ @Var int rank = mapOfRootsToWeights.get(pCanon);
+
+ if (rank == 0) {
+ updatedRootsToWeights = mapOfRootsToWeights.putAndCopy(pCanon, ++rank);
+ } else {
+ updatedRootsToWeights = mapOfRootsToWeights;
+ }
+ } else {
+ @Var int size = mapOfRootsToWeights.get(pCanon);
+ updatedRootsToWeights = mapOfRootsToWeights.putAndCopy(pCanon, ++size);
+ }
+
+ return new PersistentSortedParentPointerTreeUnionFind<>(
+ updatedNodesToParents, updatedRootsToWeights, unionType);
+ }
+
+ private PersistentSortedUnionFind addTwoElementsAsSetAndCopy(T pE1, T pE2) {
+
+ @Var PersistentSortedMap updatedNodesToParents;
+ updatedNodesToParents = mapOfNodesToParents.putAndCopy(pE1, pE1);
+ updatedNodesToParents = updatedNodesToParents.putAndCopy(pE2, pE1);
+
+ PersistentSortedMap updatedRootsToWeights;
+ if (unionType == UnionType.UNION_BY_RANK) {
+ updatedRootsToWeights = mapOfRootsToWeights.putAndCopy(pE1, 1); // rank
+ } else {
+ updatedRootsToWeights = mapOfRootsToWeights.putAndCopy(pE1, 2); // size
+ }
+
+ return new PersistentSortedParentPointerTreeUnionFind<>(
+ updatedNodesToParents, updatedRootsToWeights, unionType);
+ }
+
+ // pCanon1 will be new canonical element only if its set is actually bigger, otherwise pCanon2 new
+ // canon
+ private PersistentSortedUnionFind unionBySize(T pCanon1, T pCanon2) {
+
+ int size1 = mapOfRootsToWeights.get(pCanon1);
+ int size2 = mapOfRootsToWeights.get(pCanon2);
+
+ PersistentSortedMap updatedNodesToParents;
+ PersistentSortedMap updatedRootsToWeights;
+
+ if (size1 > size2) {
+ updatedNodesToParents = mapOfNodesToParents.putAndCopy(pCanon2, pCanon1);
+
+ updatedRootsToWeights = mapOfRootsToWeights.putAndCopy(pCanon1, size1 + size2);
+ } else {
+ updatedNodesToParents = mapOfNodesToParents.putAndCopy(pCanon1, pCanon2);
+
+ updatedRootsToWeights = mapOfRootsToWeights.putAndCopy(pCanon2, size2 + size1);
+ }
+
+ return new PersistentSortedParentPointerTreeUnionFind<>(
+ updatedNodesToParents, updatedRootsToWeights, unionType);
+ }
+
+ // pCanon1 will be new canonical element only if its rank is actually greater, otherwise pCanon2
+ // new
+ // canon
+ private PersistentSortedUnionFind unionByRank(T pCanon1, T pCanon2) {
+
+ int rank1 = mapOfRootsToWeights.get(pCanon1);
+ @Var int rank2 = mapOfRootsToWeights.get(pCanon2);
+
+ PersistentSortedMap updatedNodesToParents;
+ PersistentSortedMap updatedRootsToWeights;
+
+ if (rank1 > rank2) {
+ updatedNodesToParents = mapOfNodesToParents.putAndCopy(pCanon2, pCanon1);
+
+ updatedRootsToWeights = mapOfRootsToWeights;
+ } else {
+ updatedNodesToParents = mapOfNodesToParents.putAndCopy(pCanon1, pCanon2);
+
+ if (rank1 == rank2) {
+ updatedRootsToWeights = mapOfRootsToWeights.putAndCopy(pCanon2, ++rank2);
+ } else {
+ updatedRootsToWeights = mapOfRootsToWeights;
+ }
+ }
+
+ return new PersistentSortedParentPointerTreeUnionFind<>(
+ updatedNodesToParents, updatedRootsToWeights, unionType);
+ }
+}
diff --git a/src/org/sosy_lab/common/collect/union_find/PersistentSortedUnionFind.java b/src/org/sosy_lab/common/collect/union_find/PersistentSortedUnionFind.java
new file mode 100644
index 000000000..004075b3d
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/PersistentSortedUnionFind.java
@@ -0,0 +1,48 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find;
+
+import com.google.errorprone.annotations.CheckReturnValue;
+import com.google.errorprone.annotations.DoNotCall;
+import com.google.errorprone.annotations.Immutable;
+
+/**
+ * Interface for a persistent and sorted union-find. A persistent data structure is immutable, but
+ * provides cheap copy-and-write operations. Thus, all write operations ({@link #union(Comparable,
+ * Comparable)}) will not modify the current instance, but return a new instance instead.
+ *
+ * All modifying operations inherited from {@link SortedUnionFind} are not supported and will
+ * always throw {@link UnsupportedOperationException}.
+ *
+ * @param The type of values.
+ */
+@Immutable(containerOf = "T")
+public interface PersistentSortedUnionFind>
+ extends SortedUnionFind, PersistentUnionFind {
+
+ /**
+ * Replacement for {@link #union(Comparable, Comparable)} that returns a fresh new instance.
+ *
+ * @param pE1 first element
+ * @param pE2 second element
+ * @return new instance that the desired changes have been applied to
+ */
+ @Override
+ @CheckReturnValue
+ PersistentSortedUnionFind unionAndCopy(T pE1, T pE2);
+
+ /**
+ * @throws UnsupportedOperationException Always.
+ * @deprecated Unsupported operation.
+ */
+ @Deprecated
+ @Override
+ @DoNotCall
+ void union(T pE1, T pE2);
+}
diff --git a/src/org/sosy_lab/common/collect/union_find/PersistentUnionFind.java b/src/org/sosy_lab/common/collect/union_find/PersistentUnionFind.java
new file mode 100644
index 000000000..4d3d03abb
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/PersistentUnionFind.java
@@ -0,0 +1,46 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find;
+
+import com.google.errorprone.annotations.CheckReturnValue;
+import com.google.errorprone.annotations.DoNotCall;
+import com.google.errorprone.annotations.Immutable;
+
+/**
+ * Interface for a persistent union-find. A persistent data structure is immutable, but provides
+ * cheap copy-and-write operations. Thus, all write operations ({@link #union(Object, Object)}) will
+ * not modify the current instance, but return a new instance instead.
+ *
+ * All modifying operations inherited from {@link UnionFind} are not supported and will always
+ * throw {@link UnsupportedOperationException}.
+ *
+ * @param The type of values.
+ */
+@Immutable(containerOf = "T")
+public interface PersistentUnionFind extends UnionFind {
+
+ /**
+ * Replacement for {@link #union(Object, Object)} that returns a fresh new instance.
+ *
+ * @param pE1 first element
+ * @param pE2 second element
+ * @return new instance that the desired changes have been applied to
+ */
+ @CheckReturnValue
+ PersistentUnionFind unionAndCopy(T pE1, T pE2);
+
+ /**
+ * @throws UnsupportedOperationException Always.
+ * @deprecated Unsupported operation.
+ */
+ @Deprecated
+ @Override
+ @DoNotCall
+ void union(T pE1, T pE2);
+}
diff --git a/src/org/sosy_lab/common/collect/union_find/RootNode.java b/src/org/sosy_lab/common/collect/union_find/RootNode.java
new file mode 100644
index 000000000..0860d3944
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/RootNode.java
@@ -0,0 +1,66 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find;
+
+/**
+ * An implementation of {@link AbstractTreeNode} resulting in nodes that can be used as non-root
+ * nodes or root nodes. Their primary intended use is as root nodes. Rank describes the maximum
+ * height of the tree of this node and its child nodes (i.e. without path compression). Size
+ * describes the total number of elements in the tree represented by this root node.
+ *
+ * @param type of elements each node holds as value
+ */
+public final class RootNode extends AbstractTreeNode {
+
+ private int rank;
+ private int size;
+
+ /**
+ * Constructor for a root node. The parent variable points to itself, thus indicating this is a
+ * root node. If appended to another tree, parent can be reallocated to the new parent node, while
+ * the current node simply functions as a non-root node from then on. In the beginning, rank is 0
+ * and size is 1.
+ *
+ * @param pValue element to be stored in the node
+ */
+ public RootNode(T pValue) {
+
+ super(pValue);
+
+ this.rank = 0;
+ this.size = 1;
+ }
+
+ public int getRank() {
+ return rank;
+ }
+
+ public int getSize() {
+ return size;
+ }
+
+ /** Increments rank by one. */
+ public void incrementRankByOne() {
+ rank++;
+ }
+
+ /** Increments size by one. */
+ public void incrementSizeByOne() {
+ size++;
+ }
+
+ /**
+ * Increments size by pN.
+ *
+ * @param pN number by which size is to be increased.
+ */
+ public void incrementSizeBy(int pN) {
+ size += pN;
+ }
+}
diff --git a/src/org/sosy_lab/common/collect/union_find/SortedParentPointerTreeUnionFind.java b/src/org/sosy_lab/common/collect/union_find/SortedParentPointerTreeUnionFind.java
new file mode 100644
index 000000000..d2097dd93
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/SortedParentPointerTreeUnionFind.java
@@ -0,0 +1,69 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find;
+
+import java.util.Collection;
+import java.util.Map;
+import java.util.NavigableMap;
+import java.util.NavigableSet;
+import java.util.TreeMap;
+import java.util.TreeSet;
+
+/**
+ * A sorted implementation of {@link UnionFind} using a {@link Map} of {@link AbstractTreeNode}s. In
+ * order to represent subsets by canonical elements, each one is mapped to its representative
+ * canonical element. This is always the first element added to the subset, unless it has changed
+ * due to union operations. Each subset is stored as a parent pointer tree comprised of {@link
+ * NonRootNode}s with exactly one {@link RootNode} as the root. The union can be performed either by
+ * size or by rank, determined by a constructor parameter.
+ *
+ * @param type of elements added to the Union-Find. Must be comparable.
+ */
+public class SortedParentPointerTreeUnionFind>
+ extends ParentPointerTreeUnionFind implements SortedUnionFind {
+
+ /**
+ * Creates an empty instance.
+ *
+ * @param pUnionType type of union to be performed for all unions on this instance
+ */
+ public SortedParentPointerTreeUnionFind(UnionType pUnionType) {
+ super(pUnionType);
+ }
+
+ /**
+ * Provides a {@link Collection} containing all current subsets. It contains the subsets sorted by
+ * their canonical elements in ascending order. The contents of the subsets are also sorted in
+ * ascending order.
+ *
+ * @return sorted {@link Collection} containing all current subsets
+ */
+ // subsets are in order of their canonical elements; elements in subsets are sorted as well
+ @Override
+ public Collection extends NavigableSet> getAllSubsets() {
+
+ NavigableMap> allSubsets = new TreeMap<>();
+
+ for (AbstractTreeNode node : allNodes.values()) {
+
+ T canon = find(node.getValue());
+
+ if (allSubsets.containsKey(canon)) {
+ allSubsets.get(canon).add(node.getValue());
+ } else {
+ NavigableSet set = new TreeSet<>();
+ set.add(canon);
+ set.add(node.getValue());
+ allSubsets.put(canon, set);
+ }
+ }
+
+ return allSubsets.values();
+ }
+}
diff --git a/src/org/sosy_lab/common/collect/union_find/SortedTreeSetUnionFind.java b/src/org/sosy_lab/common/collect/union_find/SortedTreeSetUnionFind.java
new file mode 100644
index 000000000..869422969
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/SortedTreeSetUnionFind.java
@@ -0,0 +1,44 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find;
+
+import java.util.HashMap;
+import java.util.Map;
+import java.util.NavigableMap;
+import java.util.NavigableSet;
+import java.util.Set;
+import java.util.TreeMap;
+import java.util.TreeSet;
+
+/**
+ * An implementation of {@link SortedUnionFind} using a {@link HashMap} of {@link TreeSet}s. In
+ * order to represent subsets by canonical elements, each one is mapped to its representative
+ * canonical element. This is always the first element added to the subset, unless it has changed
+ * due to union operations. The union is implemented as union by size.
+ *
+ * @param type of elements added to the Union-Find. Must be {@link Comparable} to ensure correct
+ * ordering.
+ */
+public class SortedTreeSetUnionFind>
+ extends AbstractGenericUnionFind, NavigableMap>>
+ implements SortedUnionFind {
+
+ /** Generates an empty {@link SortedTreeSetUnionFind}. */
+ public SortedTreeSetUnionFind() {}
+
+ @Override
+ protected Set getEmptySet() {
+ return new TreeSet<>();
+ }
+
+ @Override
+ protected Map> getEmptyMap() {
+ return new TreeMap<>();
+ }
+}
diff --git a/src/org/sosy_lab/common/collect/union_find/SortedUnionFind.java b/src/org/sosy_lab/common/collect/union_find/SortedUnionFind.java
new file mode 100644
index 000000000..66f2f9da0
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/SortedUnionFind.java
@@ -0,0 +1,31 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find;
+
+import java.util.Collection;
+import java.util.NavigableSet;
+import java.util.Set;
+
+/**
+ * Interface for a sorted Union-Find or Disjoint-Set data structure. Uses a {@link Collection} of
+ * {@link Set}s.
+ *
+ * @param type of elements added to the Union-Find. Must be {@link Comparable} to ensure correct
+ * ordering.
+ */
+public interface SortedUnionFind> extends UnionFind {
+
+ /**
+ * Provides a {@link Collection} containing all current subsets.
+ *
+ * @return {@link Collection} containing all current subsets
+ */
+ @Override
+ Collection extends NavigableSet> getAllSubsets();
+}
diff --git a/src/org/sosy_lab/common/collect/union_find/UnionFind.java b/src/org/sosy_lab/common/collect/union_find/UnionFind.java
new file mode 100644
index 000000000..03cfb99a7
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/UnionFind.java
@@ -0,0 +1,52 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find;
+
+import java.util.Collection;
+import java.util.Set;
+
+/**
+ * Interface for a sorted Union-Find or Disjoint-Set data structure. Uses a {@link Collection} of
+ * {@link Set}s.
+ *
+ * @param type of elements added to the Union-Find.
+ */
+public interface UnionFind {
+ /**
+ * Returns the canonical element of the set containing the provided element.
+ *
+ * @param pE element for which set is to be found
+ * @return canonical element of the found set
+ */
+ T find(T pE);
+
+ /**
+ * Merges the sets represented by the two input values according to standard Union-Find behaviour.
+ *
+ * @param pE1 first element
+ * @param pE2 second element
+ */
+ void union(T pE1, T pE2);
+
+ /**
+ * Provides a {@link Collection} containing all current subsets.
+ *
+ * @return {@link Collection} containing all current subsets
+ */
+ Collection extends Set> getAllSubsets();
+
+ /**
+ * Checks whether the provided element is contained in any current subset and returns true or
+ * false accordingly.
+ *
+ * @param pE element to be searched for
+ * @return true if contained, false if not
+ */
+ boolean contains(T pE);
+}
diff --git a/src/org/sosy_lab/common/collect/union_find/benchmarking/Algs4DatasetBenchmark.java b/src/org/sosy_lab/common/collect/union_find/benchmarking/Algs4DatasetBenchmark.java
new file mode 100644
index 000000000..b13b28ece
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/benchmarking/Algs4DatasetBenchmark.java
@@ -0,0 +1,191 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find.benchmarking;
+
+import com.google.common.base.Preconditions;
+import com.google.common.base.Splitter;
+import com.google.errorprone.annotations.CanIgnoreReturnValue;
+import com.google.errorprone.annotations.Var;
+import java.io.IOException;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.util.ArrayList;
+import java.util.Iterator;
+import java.util.List;
+import java.util.regex.Pattern;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.common.collect.union_find.AbstractImmutableParentPointerTreeBuilder;
+import org.sosy_lab.common.collect.union_find.AbstractImmutableUnionFind;
+import org.sosy_lab.common.collect.union_find.ImmutableParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.ImmutableSortedParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.ParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.ParentPointerTreeUnionFind.UnionType;
+import org.sosy_lab.common.collect.union_find.PersistentParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.PersistentSortedParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.PersistentUnionFind;
+import org.sosy_lab.common.collect.union_find.SortedParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.SortedTreeSetUnionFind;
+import org.sosy_lab.common.collect.union_find.UnionFind;
+
+public final class Algs4DatasetBenchmark {
+
+ static final Pattern PATTERN = Pattern.compile("\\s+");
+
+ public static void main(String[] args) {
+
+ @Var boolean naive = false;
+ @Var boolean immutable = false;
+ @Var boolean persistent = false;
+ @Var boolean sorted = false;
+ @Var boolean unionByRank = false;
+ @Var
+ @Nullable Path filePath = null;
+ List unionInput = new ArrayList<>();
+
+ if (args.length == 0) {
+ System.exit(1);
+ }
+
+ for (String string : args) {
+
+ switch (string) {
+ case "-naive" -> naive = true;
+
+ case "-immutable" -> immutable = true;
+
+ case "-persistent" -> persistent = true;
+
+ case "-sorted" -> sorted = true;
+
+ case "-rank" -> unionByRank = true;
+
+ default -> {
+ filePath = Path.of(string);
+ }
+ }
+ }
+
+ try {
+ Preconditions.checkNotNull(filePath);
+
+ for (String line : Files.readAllLines(filePath)) {
+
+ String trimmedLine = line.trim();
+
+ if (trimmedLine.isEmpty()) {
+ continue;
+ }
+
+ List tokens = Splitter.on(PATTERN).splitToList(trimmedLine);
+
+ unionInput.add(Integer.parseInt(tokens.get(0)));
+ unionInput.add(Integer.parseInt(tokens.get(1)));
+ }
+ } catch (IOException e) {
+ System.exit(1);
+ }
+
+ Iterator iterator = unionInput.iterator();
+
+ if (naive) {
+ mutable(new SortedTreeSetUnionFind<>(), iterator);
+ } else if (!immutable && !persistent && !sorted) {
+ if (unionByRank) {
+ mutable(new ParentPointerTreeUnionFind<>(UnionType.UNION_BY_RANK), iterator);
+ } else {
+ mutable(new ParentPointerTreeUnionFind<>(UnionType.UNION_BY_SIZE), iterator);
+ }
+ } else if (!immutable && !persistent && sorted) {
+ if (unionByRank) {
+ mutable(new SortedParentPointerTreeUnionFind<>(UnionType.UNION_BY_RANK), iterator);
+ } else {
+ mutable(new SortedParentPointerTreeUnionFind<>(UnionType.UNION_BY_SIZE), iterator);
+ }
+ } else if (immutable && !sorted) {
+ if (unionByRank) {
+ immutable(
+ ImmutableParentPointerTreeUnionFind.Builder.getBuilder(UnionType.UNION_BY_RANK),
+ iterator);
+ } else {
+ immutable(
+ ImmutableParentPointerTreeUnionFind.Builder.getBuilder(UnionType.UNION_BY_SIZE),
+ iterator);
+ }
+ } else if (immutable && sorted) {
+ if (unionByRank) {
+ immutable(
+ ImmutableSortedParentPointerTreeUnionFind.Builder.getBuilder(UnionType.UNION_BY_RANK),
+ iterator);
+ } else {
+ immutable(
+ ImmutableSortedParentPointerTreeUnionFind.Builder.getBuilder(UnionType.UNION_BY_SIZE),
+ iterator);
+ }
+ } else if (persistent && !sorted) {
+ if (unionByRank) {
+ persistent(PersistentParentPointerTreeUnionFind.of(UnionType.UNION_BY_RANK), iterator);
+ } else {
+ persistent(PersistentParentPointerTreeUnionFind.of(UnionType.UNION_BY_SIZE), iterator);
+ }
+ } else if (persistent && sorted) {
+ if (unionByRank) {
+ persistent(
+ PersistentSortedParentPointerTreeUnionFind.of(UnionType.UNION_BY_RANK), iterator);
+ } else {
+ persistent(
+ PersistentSortedParentPointerTreeUnionFind.of(UnionType.UNION_BY_SIZE), iterator);
+ }
+ } else {
+ System.exit(1);
+ }
+ System.exit(0);
+ }
+
+ private static void mutable(UnionFind pUnionFind, Iterator pIterator) {
+
+ while (pIterator.hasNext()) {
+
+ int a = pIterator.next();
+ int b = pIterator.next();
+
+ pUnionFind.union(a, b);
+ }
+ }
+
+ @CanIgnoreReturnValue
+ private static AbstractImmutableUnionFind immutable(
+ AbstractImmutableParentPointerTreeBuilder pBuilder, Iterator pIterator) {
+
+ while (pIterator.hasNext()) {
+
+ int a = pIterator.next();
+ int b = pIterator.next();
+
+ pBuilder.union(a, b);
+ }
+
+ return pBuilder.build();
+ }
+
+ private static void persistent(
+ PersistentUnionFind pUnionFind, Iterator pIterator) {
+
+ @Var PersistentUnionFind unionFind = pUnionFind;
+
+ while (pIterator.hasNext()) {
+
+ int a = pIterator.next();
+ int b = pIterator.next();
+
+ unionFind = unionFind.unionAndCopy(a, b);
+ }
+ }
+
+ private Algs4DatasetBenchmark() {}
+}
diff --git a/src/org/sosy_lab/common/collect/union_find/benchmarking/FindNewToOldSingleSetBenchmark.java b/src/org/sosy_lab/common/collect/union_find/benchmarking/FindNewToOldSingleSetBenchmark.java
new file mode 100644
index 000000000..40ca67586
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/benchmarking/FindNewToOldSingleSetBenchmark.java
@@ -0,0 +1,164 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find.benchmarking;
+
+import com.google.errorprone.annotations.CanIgnoreReturnValue;
+import com.google.errorprone.annotations.Var;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+import org.sosy_lab.common.collect.union_find.AbstractImmutableParentPointerTreeBuilder;
+import org.sosy_lab.common.collect.union_find.ImmutableParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.ImmutableSortedParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.ParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.ParentPointerTreeUnionFind.UnionType;
+import org.sosy_lab.common.collect.union_find.PersistentParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.PersistentSortedParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.PersistentUnionFind;
+import org.sosy_lab.common.collect.union_find.SortedParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.SortedTreeSetUnionFind;
+import org.sosy_lab.common.collect.union_find.UnionFind;
+
+public final class FindNewToOldSingleSetBenchmark {
+
+ static final Pattern PATTERN = Pattern.compile("n_(\\d+)\\.txt$");
+
+ public static void main(String[] args) {
+
+ @Var boolean naive = false;
+ @Var boolean immutable = false;
+ @Var boolean persistent = false;
+ @Var boolean sorted = false;
+ @Var boolean unionByRank = false;
+ @Var int n = 0;
+
+ if (args.length == 0) {
+ System.exit(1);
+ }
+
+ for (String string : args) {
+
+ switch (string) {
+ case "-naive" -> naive = true;
+
+ case "-immutable" -> immutable = true;
+
+ case "-persistent" -> persistent = true;
+
+ case "-sorted" -> sorted = true;
+
+ case "-rank" -> unionByRank = true;
+
+ default -> {
+ Matcher matcher = PATTERN.matcher(string);
+
+ if (matcher.find()) {
+ n = Integer.parseInt(matcher.group(1));
+ } else {
+ throw new IllegalArgumentException("Incompatible args");
+ }
+ }
+ }
+ }
+
+ if (naive) {
+ mutable(new SortedTreeSetUnionFind<>(), n);
+ } else if (!immutable && !persistent && !sorted) {
+ if (unionByRank) {
+ mutable(new ParentPointerTreeUnionFind<>(UnionType.UNION_BY_RANK), n);
+ } else {
+ mutable(new ParentPointerTreeUnionFind<>(UnionType.UNION_BY_SIZE), n);
+ }
+ } else if (!immutable && !persistent && sorted) {
+ if (unionByRank) {
+ mutable(new SortedParentPointerTreeUnionFind<>(UnionType.UNION_BY_RANK), n);
+ } else {
+ mutable(new SortedParentPointerTreeUnionFind<>(UnionType.UNION_BY_SIZE), n);
+ }
+ } else if (immutable && !sorted) {
+ if (unionByRank) {
+ immutable(
+ ImmutableParentPointerTreeUnionFind.Builder.getBuilder(UnionType.UNION_BY_RANK), n);
+ } else {
+ immutable(
+ ImmutableParentPointerTreeUnionFind.Builder.getBuilder(UnionType.UNION_BY_SIZE), n);
+ }
+ } else if (immutable && sorted) {
+ if (unionByRank) {
+ immutable(
+ ImmutableSortedParentPointerTreeUnionFind.Builder.getBuilder(UnionType.UNION_BY_RANK),
+ n);
+ } else {
+ immutable(
+ ImmutableSortedParentPointerTreeUnionFind.Builder.getBuilder(UnionType.UNION_BY_SIZE),
+ n);
+ }
+ } else if (persistent && !sorted) {
+ if (unionByRank) {
+ persistent(PersistentParentPointerTreeUnionFind.of(UnionType.UNION_BY_RANK), n);
+ } else {
+ persistent(PersistentParentPointerTreeUnionFind.of(UnionType.UNION_BY_SIZE), n);
+ }
+ } else if (persistent && sorted) {
+ if (unionByRank) {
+ persistent(PersistentSortedParentPointerTreeUnionFind.of(UnionType.UNION_BY_RANK), n);
+ } else {
+ persistent(PersistentSortedParentPointerTreeUnionFind.of(UnionType.UNION_BY_SIZE), n);
+ }
+ } else {
+ System.exit(1);
+ }
+
+ System.exit(0);
+ }
+
+ private static void mutable(UnionFind pUnionFind, int pN) {
+
+ for (int i = 0; i < pN; i++) {
+ pUnionFind.union(0, i);
+ }
+
+ performFinds(pUnionFind, pN);
+ }
+
+ private static void immutable(
+ AbstractImmutableParentPointerTreeBuilder pBuilder, int pN) {
+
+ for (int i = 0; i < pN; i++) {
+ pBuilder.union(0, i);
+ }
+
+ performFinds(pBuilder.build(), pN);
+ }
+
+ private static void persistent(PersistentUnionFind pUnionFind, int pN) {
+
+ @Var PersistentUnionFind unionFind = pUnionFind;
+
+ for (int i = 0; i < pN; i++) {
+ unionFind = unionFind.unionAndCopy(0, i);
+ }
+
+ performFinds(unionFind, pN);
+ }
+
+ @CanIgnoreReturnValue
+ private static int performFinds(UnionFind pUnionFind, int pN) {
+
+ @Var int root = 0;
+
+ for (int i = pN; i >= 0; --i) {
+
+ root = pUnionFind.find(i);
+ }
+
+ return root;
+ }
+
+ private FindNewToOldSingleSetBenchmark() {}
+}
diff --git a/src/org/sosy_lab/common/collect/union_find/benchmarking/FindOldToNewSingleSetBenchmark.java b/src/org/sosy_lab/common/collect/union_find/benchmarking/FindOldToNewSingleSetBenchmark.java
new file mode 100644
index 000000000..6a6ce3949
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/benchmarking/FindOldToNewSingleSetBenchmark.java
@@ -0,0 +1,164 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find.benchmarking;
+
+import com.google.errorprone.annotations.CanIgnoreReturnValue;
+import com.google.errorprone.annotations.Var;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+import org.sosy_lab.common.collect.union_find.AbstractImmutableParentPointerTreeBuilder;
+import org.sosy_lab.common.collect.union_find.ImmutableParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.ImmutableSortedParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.ParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.ParentPointerTreeUnionFind.UnionType;
+import org.sosy_lab.common.collect.union_find.PersistentParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.PersistentSortedParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.PersistentUnionFind;
+import org.sosy_lab.common.collect.union_find.SortedParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.SortedTreeSetUnionFind;
+import org.sosy_lab.common.collect.union_find.UnionFind;
+
+public final class FindOldToNewSingleSetBenchmark {
+
+ static final Pattern PATTERN = Pattern.compile("n_(\\d+)\\.txt$");
+
+ public static void main(String[] args) {
+
+ @Var boolean naive = false;
+ @Var boolean immutable = false;
+ @Var boolean persistent = false;
+ @Var boolean sorted = false;
+ @Var boolean unionByRank = false;
+ @Var int n = 0;
+
+ if (args.length == 0) {
+ System.exit(1);
+ }
+
+ for (String string : args) {
+
+ switch (string) {
+ case "-naive" -> naive = true;
+
+ case "-immutable" -> immutable = true;
+
+ case "-persistent" -> persistent = true;
+
+ case "-sorted" -> sorted = true;
+
+ case "-rank" -> unionByRank = true;
+
+ default -> {
+ Matcher matcher = PATTERN.matcher(string);
+
+ if (matcher.find()) {
+ n = Integer.parseInt(matcher.group(1));
+ } else {
+ throw new IllegalArgumentException("Incompatible args");
+ }
+ }
+ }
+ }
+
+ if (naive) {
+ mutable(new SortedTreeSetUnionFind<>(), n);
+ } else if (!immutable && !persistent && !sorted) {
+ if (unionByRank) {
+ mutable(new ParentPointerTreeUnionFind<>(UnionType.UNION_BY_RANK), n);
+ } else {
+ mutable(new ParentPointerTreeUnionFind<>(UnionType.UNION_BY_SIZE), n);
+ }
+ } else if (!immutable && !persistent && sorted) {
+ if (unionByRank) {
+ mutable(new SortedParentPointerTreeUnionFind<>(UnionType.UNION_BY_RANK), n);
+ } else {
+ mutable(new SortedParentPointerTreeUnionFind<>(UnionType.UNION_BY_SIZE), n);
+ }
+ } else if (immutable && !sorted) {
+ if (unionByRank) {
+ immutable(
+ ImmutableParentPointerTreeUnionFind.Builder.getBuilder(UnionType.UNION_BY_RANK), n);
+ } else {
+ immutable(
+ ImmutableParentPointerTreeUnionFind.Builder.getBuilder(UnionType.UNION_BY_SIZE), n);
+ }
+ } else if (immutable && sorted) {
+ if (unionByRank) {
+ immutable(
+ ImmutableSortedParentPointerTreeUnionFind.Builder.getBuilder(UnionType.UNION_BY_RANK),
+ n);
+ } else {
+ immutable(
+ ImmutableSortedParentPointerTreeUnionFind.Builder.getBuilder(UnionType.UNION_BY_SIZE),
+ n);
+ }
+ } else if (persistent && !sorted) {
+ if (unionByRank) {
+ persistent(PersistentParentPointerTreeUnionFind.of(UnionType.UNION_BY_RANK), n);
+ } else {
+ persistent(PersistentParentPointerTreeUnionFind.of(UnionType.UNION_BY_SIZE), n);
+ }
+ } else if (persistent && sorted) {
+ if (unionByRank) {
+ persistent(PersistentSortedParentPointerTreeUnionFind.of(UnionType.UNION_BY_RANK), n);
+ } else {
+ persistent(PersistentSortedParentPointerTreeUnionFind.of(UnionType.UNION_BY_SIZE), n);
+ }
+ } else {
+ System.exit(1);
+ }
+
+ System.exit(0);
+ }
+
+ private static void mutable(UnionFind pUnionFind, int pN) {
+
+ for (int i = 0; i < pN; i++) {
+ pUnionFind.union(0, i);
+ }
+
+ performFinds(pUnionFind, pN);
+ }
+
+ private static void immutable(
+ AbstractImmutableParentPointerTreeBuilder pBuilder, int pN) {
+
+ for (int i = 0; i < pN; i++) {
+ pBuilder.union(0, i);
+ }
+
+ performFinds(pBuilder.build(), pN);
+ }
+
+ private static void persistent(PersistentUnionFind pUnionFind, int pN) {
+
+ @Var PersistentUnionFind unionFind = pUnionFind;
+
+ for (int i = 0; i < pN; i++) {
+ unionFind = unionFind.unionAndCopy(0, i);
+ }
+
+ performFinds(unionFind, pN);
+ }
+
+ @CanIgnoreReturnValue
+ private static int performFinds(UnionFind pUnionFind, int pN) {
+
+ @Var int root = 0;
+
+ for (int i = 0; i < pN; i++) {
+
+ root = pUnionFind.find(i);
+ }
+
+ return root;
+ }
+
+ private FindOldToNewSingleSetBenchmark() {}
+}
diff --git a/src/org/sosy_lab/common/collect/union_find/benchmarking/UnionSingleElementsIntoExistingSetBenchmark.java b/src/org/sosy_lab/common/collect/union_find/benchmarking/UnionSingleElementsIntoExistingSetBenchmark.java
new file mode 100644
index 000000000..322a1ffc6
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/benchmarking/UnionSingleElementsIntoExistingSetBenchmark.java
@@ -0,0 +1,148 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find.benchmarking;
+
+import com.google.errorprone.annotations.CanIgnoreReturnValue;
+import com.google.errorprone.annotations.Var;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+import org.sosy_lab.common.collect.union_find.AbstractImmutableParentPointerTreeBuilder;
+import org.sosy_lab.common.collect.union_find.AbstractImmutableUnionFind;
+import org.sosy_lab.common.collect.union_find.ImmutableParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.ImmutableSortedParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.ParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.ParentPointerTreeUnionFind.UnionType;
+import org.sosy_lab.common.collect.union_find.PersistentParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.PersistentSortedParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.PersistentUnionFind;
+import org.sosy_lab.common.collect.union_find.SortedParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.SortedTreeSetUnionFind;
+import org.sosy_lab.common.collect.union_find.UnionFind;
+
+public final class UnionSingleElementsIntoExistingSetBenchmark {
+
+ static final Pattern PATTERN = Pattern.compile("n_(\\d+)\\.txt$");
+
+ public static void main(String[] args) {
+
+ @Var boolean naive = false;
+ @Var boolean immutable = false;
+ @Var boolean persistent = false;
+ @Var boolean sorted = false;
+ @Var boolean unionByRank = false;
+ @Var int n = 0;
+
+ if (args.length == 0) {
+ System.exit(1);
+ }
+
+ for (String string : args) {
+
+ switch (string) {
+ case "-naive" -> naive = true;
+
+ case "-immutable" -> immutable = true;
+
+ case "-persistent" -> persistent = true;
+
+ case "-sorted" -> sorted = true;
+
+ case "-rank" -> unionByRank = true;
+
+ default -> {
+ Matcher matcher = PATTERN.matcher(string);
+
+ if (matcher.find()) {
+ n = Integer.parseInt(matcher.group(1));
+ } else {
+ throw new IllegalArgumentException("Incompatible args");
+ }
+ }
+ }
+ }
+
+ if (naive) {
+ mutable(new SortedTreeSetUnionFind<>(), n);
+ } else if (!immutable && !persistent && !sorted) {
+ if (unionByRank) {
+ mutable(new ParentPointerTreeUnionFind<>(UnionType.UNION_BY_RANK), n);
+ } else {
+ mutable(new ParentPointerTreeUnionFind<>(UnionType.UNION_BY_SIZE), n);
+ }
+ } else if (!immutable && !persistent && sorted) {
+ if (unionByRank) {
+ mutable(new SortedParentPointerTreeUnionFind<>(UnionType.UNION_BY_RANK), n);
+ } else {
+ mutable(new SortedParentPointerTreeUnionFind<>(UnionType.UNION_BY_SIZE), n);
+ }
+ } else if (immutable && !sorted) {
+ if (unionByRank) {
+ immutable(
+ ImmutableParentPointerTreeUnionFind.Builder.getBuilder(UnionType.UNION_BY_RANK), n);
+ } else {
+ immutable(
+ ImmutableParentPointerTreeUnionFind.Builder.getBuilder(UnionType.UNION_BY_SIZE), n);
+ }
+ } else if (immutable && sorted) {
+ if (unionByRank) {
+ immutable(
+ ImmutableSortedParentPointerTreeUnionFind.Builder.getBuilder(UnionType.UNION_BY_RANK),
+ n);
+ } else {
+ immutable(
+ ImmutableSortedParentPointerTreeUnionFind.Builder.getBuilder(UnionType.UNION_BY_SIZE),
+ n);
+ }
+ } else if (persistent && !sorted) {
+ if (unionByRank) {
+ persistent(PersistentParentPointerTreeUnionFind.of(UnionType.UNION_BY_RANK), n);
+ } else {
+ persistent(PersistentParentPointerTreeUnionFind.of(UnionType.UNION_BY_SIZE), n);
+ }
+ } else if (persistent && sorted) {
+ if (unionByRank) {
+ persistent(PersistentSortedParentPointerTreeUnionFind.of(UnionType.UNION_BY_RANK), n);
+ } else {
+ persistent(PersistentSortedParentPointerTreeUnionFind.of(UnionType.UNION_BY_SIZE), n);
+ }
+ } else {
+ System.exit(1);
+ }
+ System.exit(0);
+ }
+
+ private static void mutable(UnionFind pUnionFind, int pN) {
+
+ for (int i = 0; i < pN; i++) {
+ pUnionFind.union(0, i);
+ }
+ }
+
+ @CanIgnoreReturnValue
+ private static AbstractImmutableUnionFind immutable(
+ AbstractImmutableParentPointerTreeBuilder pBuilder, int pN) {
+
+ for (int i = 0; i < pN; i++) {
+ pBuilder.union(0, i);
+ }
+
+ return pBuilder.build();
+ }
+
+ private static void persistent(PersistentUnionFind pUnionFind, int pN) {
+
+ @Var PersistentUnionFind unionFind = pUnionFind;
+
+ for (int i = 0; i < pN; i++) {
+ unionFind = unionFind.unionAndCopy(0, i);
+ }
+ }
+
+ private UnionSingleElementsIntoExistingSetBenchmark() {}
+}
diff --git a/src/org/sosy_lab/common/collect/union_find/benchmarking/package-info.java b/src/org/sosy_lab/common/collect/union_find/benchmarking/package-info.java
new file mode 100644
index 000000000..acce67737
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/benchmarking/package-info.java
@@ -0,0 +1,14 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+/** This package contains all benchmarking classes related to union-find. */
+@com.google.errorprone.annotations.CheckReturnValue
+@javax.annotation.ParametersAreNonnullByDefault
+@org.sosy_lab.common.annotations.ReturnValuesAreNonnullByDefault
+@org.sosy_lab.common.annotations.FieldsAreNonnullByDefault
+package org.sosy_lab.common.collect.union_find.benchmarking;
diff --git a/src/org/sosy_lab/common/collect/union_find/package-info.java b/src/org/sosy_lab/common/collect/union_find/package-info.java
new file mode 100644
index 000000000..0061c6a88
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/package-info.java
@@ -0,0 +1,14 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+/** This package contains all interfaces and classes related to union-find. */
+@com.google.errorprone.annotations.CheckReturnValue
+@javax.annotation.ParametersAreNonnullByDefault
+@org.sosy_lab.common.annotations.ReturnValuesAreNonnullByDefault
+@org.sosy_lab.common.annotations.FieldsAreNonnullByDefault
+package org.sosy_lab.common.collect.union_find;
diff --git a/src/org/sosy_lab/common/collect/union_find/tests/ImmutableParentPointerTreeUnionFindSortednessTest.java b/src/org/sosy_lab/common/collect/union_find/tests/ImmutableParentPointerTreeUnionFindSortednessTest.java
new file mode 100644
index 000000000..3eefe2a2a
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/union_find/tests/ImmutableParentPointerTreeUnionFindSortednessTest.java
@@ -0,0 +1,193 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect.union_find.tests;
+
+import static com.google.common.truth.Truth.assertThat;
+
+import java.util.Collection;
+import java.util.Iterator;
+import java.util.NavigableSet;
+import org.junit.Test;
+import org.sosy_lab.common.collect.union_find.ImmutableSortedParentPointerTreeUnionFind;
+import org.sosy_lab.common.collect.union_find.ParentPointerTreeUnionFind.UnionType;
+
+public class ImmutableParentPointerTreeUnionFindSortednessTest {
+
+ private static ImmutableSortedParentPointerTreeUnionFind