Repository: PermutaTriangle/comb_spec_searcher (language: python)

Issue:
Nonbijectiverules



Discussion / hints:

Fix patch:
diff --git a/CHANGELOG.md b/CHANGELOG.md
index a98fcca6d..c6a9f9f63 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -11,6 +11,16 @@ and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.
   `NotImplementedError`
 - `find_bijection_between` tries to find a bijection between classes given
   a `CombinatorialSpecificationSearcher` object for both.
+- Special forward and backward maps, called indexed forward and backward maps.
+  They are to be used for bijections and their purposes is to support bijections
+  for non-injective forward maps by labelling the resulting objects or map from 
+  an labelled object.
+- `NonBijectiveRule` will implement a labelling system for indexed forward
+  and backward maps.
+- `EqPathParallelSpecFinder` that, on top of the base class, validates any
+  potential path contained in equivalence labels.
+- `PartialSpecificationRuleExtractor` that extracts rules from partially built
+  specifications and two subclasses with specific applications of that.
 
 ### Changed
 - If a rule in a specification cannot be sanity checked (e.g., counting is not
diff --git a/README.rst b/README.rst
index 4f70acbcb..40db83208 100644
--- a/README.rst
+++ b/README.rst
@@ -467,7 +467,8 @@ We will first need a couple of imports.
 
 .. code:: python
 
-   >>> from comb_spec_searcher import find_bijection_between, Bijection
+   >>> from comb_spec_searcher.bijection import ParallelSpecFinder
+   >>> from comb_spec_searcher.isomorphism import Bijection
 
 We start by defining our two classes that we wish to find a bijection between.
 
@@ -494,9 +495,13 @@ We get two parallel specs if successful, ``None`` otherwise.
 
 .. code:: python
 
-   >>> specs = find_bijection_between(searcher1, searcher2)
-   >>> spec1, spec2 = specs
-   >>> bijection = Bijection.construct(spec1, spec2)
+   >>> specs = ParallelSpecFinder(searcher1, searcher2).find()
+
+We then construct the bijection from the parallel specifications.
+
+.. code:: python
+
+   >>> bijection = Bijection.construct(*specs)
 
 We can use the `Bijection` object to map (either way) sampled objects
 from the sepcifications.
@@ -504,9 +509,9 @@ from the sepcifications.
 .. code:: python
 
    >>> for i in range(10):
-   ...     for w in spec1.generate_objects_of_size(i):
+   ...     for w in bijection.domain.generate_objects_of_size(i):
    ...         assert w == bijection.inverse_map(bijection.map(w))
-   ...     for w in spec2.generate_objects_of_size(i):
+   ...     for w in bijection.codomain.generate_objects_of_size(i):
    ...         assert w == bijection.map(bijection.inverse_map(w))
    ...
 
diff --git a/comb_spec_searcher/__init__.py b/comb_spec_searcher/__init__.py
index 84a7afeaa..2ed1f1382 100644
--- a/comb_spec_searcher/__init__.py
+++ b/comb_spec_searcher/__init__.py
@@ -1,7 +1,5 @@
-from .bijection import find_bijection_between
 from .comb_spec_searcher import CombinatorialSpecificationSearcher
 from .combinatorial_class import CombinatorialClass, CombinatorialObject
-from .isomorphism import Bijection
 from .specification import CombinatorialSpecification
 from .specification_drawer import ForestSpecificationDrawer, SpecificationDrawer
 from .strategies import (
@@ -38,6 +36,4 @@
     "StrategyPack",
     "SymmetryStrategy",
     "VerificationStrategy",
-    "find_bijection_between",
-    "Bijection",
 ]
diff --git a/comb_spec_searcher/bijection.py b/comb_spec_searcher/bijection.py
index 55647b881..a646a2c1f 100644
--- a/comb_spec_searcher/bijection.py
+++ b/comb_spec_searcher/bijection.py
@@ -1,124 +1,226 @@
 from collections import defaultdict, deque
-from itertools import product
-from typing import DefaultDict, Dict, List, Optional, Set, Tuple
+from typing import (
+    TYPE_CHECKING,
+    DefaultDict,
+    Dict,
+    Generic,
+    List,
+    Optional,
+    Set,
+    Tuple,
+    TypeVar,
+    Union,
+)
 
 from comb_spec_searcher.comb_spec_searcher import CombinatorialSpecificationSearcher
-from comb_spec_searcher.combinatorial_class import CombinatorialClass
 from comb_spec_searcher.exception import NoMoreClassesToExpandError
 from comb_spec_searcher.rule_db.base import RuleDB
 from comb_spec_searcher.specification import CombinatorialSpecification
-from comb_spec_searcher.specification_extrator import SpecificationRuleExtractor
-from comb_spec_searcher.strategies.rule import Rule
+from comb_spec_searcher.specification_extrator import (
+    EquivalenceRuleExtractor,
+    SpecificationRuleExtractor,
+)
+from comb_spec_searcher.strategies.constructor.base import Constructor
+from comb_spec_searcher.strategies.rule import AbstractRule, Rule
 from comb_spec_searcher.tree_searcher import Node, prune
-from comb_spec_searcher.typing import RuleKey
+from comb_spec_searcher.typing import (
+    CombinatorialClassType,
+    CombinatorialObjectType,
+    RuleKey,
+    Terms,
+)
 
+if TYPE_CHECKING:
+    from comb_spec_searcher.combinatorial_class import (
+        CombinatorialClass,
+        CombinatorialObject,
+    )
+
+
+ClassType1 = TypeVar("ClassType1", bound="CombinatorialClass")
+ObjType1 = TypeVar("ObjType1", bound="CombinatorialObject")
+ClassType2 = TypeVar("ClassType2", bound="CombinatorialClass")
+ObjType2 = TypeVar("ObjType2", bound="CombinatorialObject")
 NO_CONSTRUCTOR = None.__class__
 MatchingInfo = DefaultDict[
-    Tuple[int, int], Set[Tuple[Tuple[int, ...], Tuple[int, ...]]]
+    Tuple[int, int], Dict[Tuple[Tuple[int, ...], Tuple[int, ...]], List[int]]
 ]
 MatchingInfoSingle = DefaultDict[int, DefaultDict[int, Set[Tuple[int, ...]]]]
 SpecMap = Dict[int, Tuple[int, ...]]
+RuleClassification = DefaultDict[
+    int,
+    DefaultDict[
+        int,
+        List[
+            Tuple[
+                Tuple[int, ...],
+                Union[
+                    Constructor[CombinatorialClassType, CombinatorialObjectType],
+                    None,
+                ],
+            ]
+        ],
+    ],
+]
+EqPathTracker = DefaultDict[
+    Tuple[int, int],
+    DefaultDict[
+        Tuple[int, int],
+        Dict[Tuple[Tuple[int, ...], Tuple[int, ...]], bool],
+    ],
+]
 
 
-class ParallelInfo:
+class ParallelInfo(Generic[CombinatorialClassType, CombinatorialObjectType]):
     """Information from searcher essential to finding bijection with another and then
     to create specifications.
     """
 
-    def __init__(self, searcher: CombinatorialSpecificationSearcher):
-        self.searcher: CombinatorialSpecificationSearcher = searcher
-        self._expand()
+    def __init__(
+        self,
+        searcher: CombinatorialSpecificationSearcher[CombinatorialClassType],
+        additional_levels: int = 0,
+    ):
+        self.searcher = searcher
+        self._expand(additional_levels)
         if not isinstance(self.searcher.ruledb, RuleDB):
             raise RuntimeError("Only searcher supported rule db is `RuleDB`.")
-        self.r_db: RuleDB = self.searcher.ruledb
-        self.root_eq_label: int = self.r_db.equivdb[self.searcher.start_label]
-        self.atom_map: Dict[int, CombinatorialClass] = {}
-        self.root_class: Optional[CombinatorialClass] = None
-        self.eq_label_rules: DefaultDict[
-            int, DefaultDict[type, DefaultDict[int, Set[Tuple[int, ...]]]]
-        ] = self._construct_eq_label_rules()
-
-    def _expand(self):
+        self.ruledb: RuleDB = self.searcher.ruledb
+
+        # Root eq label and actual class
+        self.root_eq_label: int = self.searcher.ruledb.equivdb[
+            self.searcher.start_label
+        ]
+        self.root_class = self.searcher.classdb.get_class(self.searcher.start_label)
+
+        # Atom information for comparing them
+        self.atom_map: Dict[int, Tuple[int, Terms]] = {}
+
+        # Used to filter out impossible matchings to avoid unnecessary expansions
+        self.eq_label_rules = self._construct_eq_label_rules()
+
+    def _expand(self, additional_levels: int) -> None:
+        """Expand until at least one spec exists and after that some
+        additional expansions can be done (optionally)."""
+        self._expand_until_spec()
+        self._additional_expands(additional_levels)
+
+    def _expand_until_spec(self) -> None:
         try:
             while not self.searcher.has_specification():
                 self.searcher.do_level()
+        except NoMoreClassesToExpandError as ex:
+            if not self.searcher.has_specification():
+                raise ValueError("No specifications were found") from ex
+
+    def _additional_expands(self, additional_levels: int) -> None:
+        try:
+            for _ in range(additional_levels):
+                self.searcher.do_level()
         except NoMoreClassesToExpandError:
-            assert (
-                self.searcher.get_specification(minimization_time_limit=0) is not None
-            )
+            pass
 
     def _construct_eq_label_rules(
         self,
-    ) -> DefaultDict[int, DefaultDict[type, DefaultDict[int, Set[Tuple[int, ...]]]]]:
+    ) -> RuleClassification[CombinatorialClassType, CombinatorialObjectType]:
         """
         Creates a dictionary d such that
-            d[label][rule_type][number_of_children]
-        is a set of possible resulting children ids (grouped into tuples of length
-        number_of_children) by applying rule_type to label.
+            d[eq_label][child_count]
+        is a set of possible resulting children eq_labels and the corresponding
+        constructor if any.
         """
-        lis, rule_dict, eq_label_rules = self._construct_eq_labels_init()
+        lis = self._pruned_rules_up_to_eq()
+        rule_dict = self.ruledb.rule_from_equivalence_rule_dict(lis)
+        eq_label_rules: RuleClassification[
+            CombinatorialClassType, CombinatorialObjectType
+        ] = defaultdict(lambda: defaultdict(list))
 
         for eq_par, eq_chi in lis:
-            actual_par, actual_children = rule_dict[(eq_par, eq_chi)]
-            strategy = self.r_db.rule_to_strategy[(actual_par, actual_children)]
-            parent = self.searcher.classdb.get_class(actual_par)
-            children = tuple(map(self.searcher.classdb.get_class, actual_children))
-            rule = strategy(parent, children)
-            if eq_par == self.root_eq_label and self.root_class is None:
-                self.root_class = parent
+            parent, rule = self._get_class_and_rule(eq_par, eq_chi, rule_dict)
             if parent.is_atom():
-                eq_label_rules[eq_par][NO_CONSTRUCTOR][len(children)].add(eq_chi)
-                self.atom_map[eq_par] = parent
+                eq_label_rules[eq_par][0].append((eq_chi, None))
+                sz = next(
+                    parent.objects_of_size(parent.minimum_size_of_object())
+                ).size()
+                self.atom_map[eq_par] = (sz, rule.get_terms(sz))
             else:
-                assert isinstance(rule, Rule)
-                non_empty_children = tuple(
-                    eq_chi[i] for i, c in enumerate(children) if not c.is_empty()
-                )
-                eq_label_rules[eq_par][rule.constructor.__class__][
-                    len(non_empty_children)
-                ].add(non_empty_children)
+                if not isinstance(rule, Rule):
+                    raise ValueError("Only atoms can be verified.")
+                assert len(eq_chi) > 0
+                eq_label_rules[eq_par][len(eq_chi)].append((eq_chi, rule.constructor))
         return eq_label_rules
 
-    def _construct_eq_labels_init(
-        self,
+    def _get_class_and_rule(
+        self, eq_par: int, eq_chi: Tuple[int, ...], rule_dict: Dict[RuleKey, RuleKey]
     ) -> Tuple[
-        List[Tuple[int, Tuple[int, ...]]],
-        Dict[RuleKey, RuleKey],
-        DefaultDict[int, DefaultDict[type, DefaultDict[int, Set[Tuple[int, ...]]]]],
+        CombinatorialClassType,
+        AbstractRule[CombinatorialClassType, CombinatorialObjectType],
     ]:
-        rules_up_to_eq = self.r_db.rules_up_to_equivalence()
+        actual_par, actual_children = rule_dict[(eq_par, eq_chi)]
+        strategy = self.ruledb.rule_to_strategy[(actual_par, actual_children)]
+        parent = self.searcher.classdb.get_class(actual_par)
+        rule: AbstractRule[CombinatorialClassType, CombinatorialObjectType] = strategy(
+            parent
+        )
+        return parent, rule
+
+    def _pruned_rules_up_to_eq(
+        self,
+    ) -> List[Tuple[int, Tuple[int, ...]]]:
+        rules_up_to_eq = self.ruledb.rules_up_to_equivalence()
         prune(rules_up_to_eq)
-        lis = [(k, c) for k, v in rules_up_to_eq.items() for c in v]
-        rule_dict = self.r_db.rule_from_equivalence_rule_dict(lis)
-        eq_label_rules: DefaultDict[
-            int, DefaultDict[type, DefaultDict[int, Set[Tuple[int, ...]]]]
-        ] = defaultdict(lambda: defaultdict(lambda: defaultdict(set)))
-        return lis, rule_dict, eq_label_rules
+        return [(k, c) for k, v in rules_up_to_eq.items() for c in v]
 
 
-class ParallelSpecFinder:
-    """Finder for paralell specs."""
+class ParallelSpecFinder(Generic[ClassType1, ObjType1, ClassType2, ObjType2]):
+    """
+    Finder for paralell specs. This version assumes that any classes that share
+    equivalence labels are in fact equivalent.
+    """
 
     _INVALID, _UNKNOWN, _VALID = range(-1, 2)
 
     def __init__(
         self,
-        searcher1: CombinatorialSpecificationSearcher,
-        searcher2: CombinatorialSpecificationSearcher,
+        searcher1: CombinatorialSpecificationSearcher[ClassType1],
+        searcher2: CombinatorialSpecificationSearcher[ClassType2],
     ):
-        self._pi1 = ParallelInfo(searcher1)
-        self._pi2 = ParallelInfo(searcher2)
+        self._pre_expand(searcher1, searcher2)
+        self._pi1 = ParallelInfo[ClassType1, ObjType1](searcher1)
+        self._pi2 = ParallelInfo[ClassType2, ObjType2](searcher2)
         self._ancestors: Set[Tuple[int, int]] = set()
 
+    def _pre_expand(
+        self,
+        searcher1: CombinatorialSpecificationSearcher[ClassType1],
+        searcher2: CombinatorialSpecificationSearcher[ClassType2],
+    ) -> None:
+        """When overwritten, this method can be implemented and will be called
+        prior to the searcher expanding the universe."""
+
+    # First search
+
     def find(
         self,
-    ) -> Optional[Tuple[CombinatorialSpecification, CombinatorialSpecification]]:
+    ) -> Optional[
+        Tuple[
+            CombinatorialSpecification[ClassType1, ObjType1],
+            CombinatorialSpecification[ClassType2, ObjType2],
+        ]
+    ]:
         """Find bijections between the two universes."""
-        matching_info: MatchingInfo = defaultdict(set)
+        # d[(p1,p2)][(c1,c2)] = permutation of children such that they match
+        matching_info: MatchingInfo = defaultdict(dict)
+
+        # Failed matches
         visited: Set[Tuple[int, int]] = set()
+
+        # Find matching eq lables
         found = self._find(
             self._pi1.root_eq_label, self._pi2.root_eq_label, matching_info, visited
         )
+
+        # Try to construct valid specs from said eq-label matchings
         return self._matching_info_to_specs(found, matching_info)
 
     def _find(
@@ -128,29 +230,62 @@ def _find(
         matching_info: MatchingInfo,
         visited: Set[Tuple[int, int]],
     ) -> bool:
+        """Recursion call to find matching for eq labels (id1,id2)."""
+
+        # Check for base cases (invalid = -1, valid = 1)
         known = self._base_case(id1, id2, matching_info, visited)
         if known:
             return bool(known + 1)
+
+        # Store pair as ancestors ids checked with further recursions
         self._ancestors.add((id1, id2))
-        found = False
+
         for children1, children2, n in self._potential_children(id1, id2):
+            # The permutation of matched children indices
+            child_order: List[int] = [-1] * n
+
+            # Iterative stack with elements:
+            # (index1, index2, indices of the second rule's children already matched)
             stack = [(0, i, {i}) for i in range(n - 1, -1, -1)]
+
+            # To avoid repeated index pairs, since outside choices have no effect.
             blacklist: Set[Tuple[int, int]] = set()
+
+            # Check all pairings of children. Any pairing hat exhaust all nonempty
+            # children, such that all are valid will result in current nodes being
+            # matched. This is done with backtracking.
             while stack:
                 i1, i2, in_use = stack.pop()
+
+                # Already failed
                 if (i1, i2) in blacklist:
                     continue
+
+                # Recursion. Blacklist children pair if we fail.
                 if not self._find(children1[i1], children2[i2], matching_info, visited):
                     blacklist.add((i1, i2))
                     continue
+
+                # Update permutation
+                child_order[i2] = i1
+
+                # If we reach the last index we have succeeded. Gather this matching and
+                # keep trying other children as we want to collect all that are valid.
                 if i1 == n - 1:
-                    matching_info[(id1, id2)].add((children1, children2))
-                    found = True
+                    matching_info[(id1, id2)][(children1, children2)] = child_order
                     break
+
+                # Extand stack if we are not done.
                 ParallelSpecFinder._extend_stack(i1, n, in_use, stack)
+
+        # Remove self as ancestors if we are done.
         self._ancestors.remove((id1, id2))
+
+        # Store pair in memory of failures.
         visited.add((id1, id2))
-        return found
+
+        # Return true if any valid matching was found.
+        return (id1, id2) in matching_info
 
     def _base_case(
         self,
@@ -159,19 +294,15 @@ def _base_case(
         matching_info: MatchingInfo,
         visited: Set[Tuple[int, int]],
     ) -> int:
-        # If rule type has no constructor we compare atoms
-        if NO_CONSTRUCTOR in self._pi1.eq_label_rules[id1]:
-            if NO_CONSTRUCTOR in self._pi2.eq_label_rules[id2]:
-                atomic1, atomic2 = self._pi1.atom_map[id1], self._pi2.atom_map[id2]
-                atom1 = next(atomic1.objects_of_size(atomic1.minimum_size_of_object()))
-                atom2 = next(atomic2.objects_of_size(atomic2.minimum_size_of_object()))
-                if atom1.size() == atom2.size():
-                    matching_info[(id1, id2)] = {((), ())}
-                    return ParallelSpecFinder._VALID
-                if len(self._pi2.eq_label_rules[id2]) == 1:
-                    return ParallelSpecFinder._INVALID
-            if len(self._pi1.eq_label_rules[id1]) == 1:
-                return ParallelSpecFinder._INVALID
+        # If no children we compare atoms
+        if (
+            id1 in self._pi1.atom_map
+            and id2 in self._pi2.atom_map
+            and self._atom_match(id1, id2)
+        ):
+            matching_info[(id1, id2)] = {((), ()): []}
+            return ParallelSpecFinder._VALID
+
         # Already matched
         if (id1, id2) in matching_info:
             return ParallelSpecFinder._VALID
@@ -183,6 +314,12 @@ def _base_case(
             return ParallelSpecFinder._VALID
         return ParallelSpecFinder._UNKNOWN
 
+    def _atom_match(self, id1: int, id2: int) -> bool:
+        """Returns true if atoms match."""
+        sz1, terms1 = self._pi1.atom_map[id1]
+        sz2, terms2 = self._pi2.atom_map[id2]
+        return sz1 == sz2 and terms1 == terms2
+
     def _potential_children(
         self, id1: int, id2: int
     ) -> List[Tuple[Tuple[int, ...], Tuple[int, ...], int]]:
@@ -191,10 +328,11 @@ def _potential_children(
         """
         return [
             (c1, c2, n)
-            for rule_type, child_cnt_map in self._pi1.eq_label_rules[id1].items()
-            for n, child_set in child_cnt_map.items()
-            for c2 in self._pi2.eq_label_rules[id2][rule_type][n]
-            for c1 in child_set
+            for n, child_rule_pairs in self._pi1.eq_label_rules[id1].items()
+            for c1, r1 in child_rule_pairs
+            for c2, r2 in self._pi2.eq_label_rules[id2][n]
+            if (r1 is None and r2 is None)
+            or (r1 is not None and r2 is not None and r1.equiv(r2)[0])
         ]
 
     @staticmethod
@@ -206,13 +344,22 @@ def _extend_stack(
                 continue
             stack.append((i1 + 1, i, in_use.union({i})))
 
+    # Second search
+
     def _matching_info_to_specs(
         self,
         found: bool,
         matching_info: MatchingInfo,
-    ) -> Optional[Tuple[CombinatorialSpecification, CombinatorialSpecification]]:
+    ) -> Optional[
+        Tuple[
+            CombinatorialSpecification[ClassType1, ObjType1],
+            CombinatorialSpecification[ClassType2, ObjType2],
+        ]
+    ]:
+        # If first search was unsuccessful
         if not found:
             return None
+        # Attempt to construct specifications from matches
         spec_rules = self._search_matching_info(matching_info)
         if spec_rules is None:
             return None
@@ -224,6 +371,9 @@ def _matching_info_to_specs(
     def _search_matching_info(
         self, matching_info: MatchingInfo
     ) -> Optional[Tuple[SpecMap, SpecMap]]:
+        # Matching info 1 and 2 are flatten dictionaries of matching_info
+        # for the perspective of each spec. The maps sp1 and sp2 are the
+        # gathered specifications (in terms of eq labels), initially empty.
         (
             matching_info1,
             matching_info2,
@@ -231,35 +381,81 @@ def _search_matching_info(
             sp2,
         ) = ParallelSpecFinder._search_matching_info_init(matching_info)
 
-        def _rec(id1: int, id2: int, id_sets: Tuple[Set[int], Set[int]]) -> bool:
+        # Recursive helper function that tries to populate the spec maps in a way
+        # that no label appears on the LHS more than one time.
+        def _rec(
+            id1: int,
+            id2: int,
+            id_sets: Tuple[Set[int], Set[int]],
+        ) -> bool:
+            # Check base cases (invalid = -1, valid = 1)
             bc = ParallelSpecFinder._search_matching_info_recursion_base_cases(
                 id1, id2, matching_info, matching_info1, matching_info2, sp1, sp2
             )
             if bc:
                 return bool(bc + 1)
+
+            # If ids have appeared before, we don't want to clean them when done
+            rec1, rec2 = id1 in sp1, id2 in sp2
+
+            # For all children that matches for given parent pair where they are either
+            # not in spec maps or they are mapped to the children we are looking at.
             for children1, children2 in filter(
                 lambda c: (id1 not in sp1 or c[0] == sp1[id1])
                 and (id2 not in sp2 or c[1] == sp2[id2]),
                 matching_info[(id1, id2)],
             ):
+                # Add rule for spec to (id -> children) for both specs
                 sp1[id1], sp2[id2] = children1, children2
+
+                # Construct cleaning sets that are passed down the recursion
                 to_clean: Tuple[Set[int], Set[int]] = (set(), set())
+
+                # If all the children are valid, compared one at a time in the order
+                # they were matched in the first search.
                 if all(
                     _rec(child1, child2, to_clean)
-                    for child1, child2 in filter(
-                        lambda m: m in matching_info, product(children1, children2)
+                    for child1, child2 in zip(
+                        (
+                            children1[i]
+                            for i in matching_info[(id1, id2)][(children1, children2)]
+                        ),
+                        children2,
                     )
                 ):
-                    id_sets[0].update(to_clean[0], (id1,))
-                    id_sets[1].update(to_clean[1], (id2,))
+                    # Update the cleaning set so any failing ancestor can remove.
+                    id_sets[0].update(to_clean[0], () if rec1 else (id1,))
+                    id_sets[1].update(to_clean[1], () if rec2 else (id2,))
                     return True
-                ParallelSpecFinder._clean_descendants(*to_clean, id1, id2, sp1, sp2)
+                # If failed, remove all descendants that populated the spec maps.
+                ParallelSpecFinder._clean_descendants(
+                    *to_clean, id1, id2, sp1, sp2, rec1, rec2
+                )
             return False
 
-        if _rec(self._pi1.root_eq_label, self._pi1.root_eq_label, (set(), set())):
+        if _rec(
+            self._pi1.root_eq_label,
+            self._pi2.root_eq_label,
+            (set(), set()),
+        ):
             return sp1, sp2
         return None
 
+    @staticmethod
+    def _search_matching_info_init(
+        matching_info: MatchingInfo,
+    ) -> Tuple[MatchingInfoSingle, MatchingInfoSingle, SpecMap, SpecMap]:
+        matching_info_1: MatchingInfoSingle = defaultdict(lambda: defaultdict(set))
+        matching_info_2: MatchingInfoSingle = defaultdict(lambda: defaultdict(set))
+        # convert (p1,p2) -> children to p1 -> p2 -> children and p2-> p1 -> children.
+        for (p1, p2), children in matching_info.items():
+            for ch1, ch2 in children:
+                matching_info_1[p1][p2].add(ch1)
+                matching_info_2[p2][p1].add(ch2)
+        sp1: SpecMap = {}
+        sp2: SpecMap = {}
+        return matching_info_1, matching_info_2, sp1, sp2
+
     @staticmethod
     def _search_matching_info_recursion_base_cases(
         id1: int,
@@ -270,32 +466,37 @@ def _search_matching_info_recursion_base_cases(
         sp1: SpecMap,
         sp2: SpecMap,
     ) -> int:
-        if (id1, id2) not in matching_info:
+        if ParallelSpecFinder._inconsistent_with_matching_info(
+            id1, id2, matching_info, matching_info1, matching_info2, sp1, sp2
+        ):
             return ParallelSpecFinder._INVALID
-        if matching_info[(id1, id2)] == {((), ())}:
+        # If atoms, there is only one possible outcome
+        if ((), ()) in matching_info[(id1, id2)]:
             sp1[id1], sp2[id2] = (), ()
             return ParallelSpecFinder._VALID
+        # If both are assigned, we are done
         if id1 in sp1 and id2 in sp2:
             return ParallelSpecFinder._VALID
-        if id1 in sp1 and sp1[id1] not in matching_info1[id1][id2]:
-            return ParallelSpecFinder._INVALID
-        if id2 in sp2 and sp2[id2] not in matching_info2[id2][id1]:
-            return ParallelSpecFinder._INVALID
         return ParallelSpecFinder._UNKNOWN
 
     @staticmethod
-    def _search_matching_info_init(
+    def _inconsistent_with_matching_info(
+        id1: int,
+        id2: int,
         matching_info: MatchingInfo,
-    ) -> Tuple[MatchingInfoSingle, MatchingInfoSingle, SpecMap, SpecMap]:
-        matching_info_1: MatchingInfoSingle = defaultdict(lambda: defaultdict(set))
-        matching_info_2: MatchingInfoSingle = defaultdict(lambda: defaultdict(set))
-        for (p1, p2), children in matching_info.items():
-            for ch1, ch2 in children:
-                matching_info_1[p1][p2].add(ch1)
-                matching_info_2[p2][p1].add(ch2)
-        sp1: SpecMap = {}
-        sp2: SpecMap = {}
-        return matching_info_1, matching_info_2, sp1, sp2
+        matching_info1: MatchingInfoSingle,
+        matching_info2: MatchingInfoSingle,
+        sp1: SpecMap,
+        sp2: SpecMap,
+    ):
+        """If ids are not in the matching order or if one is assigned but those
+        children aren't compatible with the other.
+        """
+        return (
+            (id1, id2) not in matching_info
+            or (id1 in sp1 and sp1[id1] not in matching_info1[id1][id2])
+            or (id2 in sp2 and sp2[id2] not in matching_info2[id2][id1])
+        )
 
     @staticmethod
     def _clean_descendants(
@@ -305,23 +506,40 @@ def _clean_descendants(
         id2: int,
         sp1: SpecMap,
         sp2: SpecMap,
+        rec1: bool,
+        rec2: bool,
     ):
+        # Clean descendants
         for i in to_clean1:
             if i in sp1:
                 del sp1[i]
         for i in to_clean2:
             if i in sp2:
                 del sp2[i]
-        if id1 in sp1:
+        # Clean self if no prior assignments
+        if not rec1 and id1 in sp1:
             del sp1[id1]
-        if id2 in sp2:
+        if not rec2 and id2 in sp2:
             del sp2[id2]
 
+    # specification construction helpers
+
     @staticmethod
     def _create_spec(d: SpecMap, pi: ParallelInfo) -> CombinatorialSpecification:
+        rules = SpecificationRuleExtractor(
+            pi.root_eq_label,
+            ParallelSpecFinder._create_tree(d, pi.root_eq_label),
+            pi.ruledb,
+            pi.searcher.classdb,
+        ).rules()
+        return CombinatorialSpecification(pi.root_class, rules)
+
+    @staticmethod
+    def _create_tree(d: SpecMap, root_eq_label: int) -> Node:
         visited: Set[int] = set()
-        root_node = Node(pi.root_eq_label)
+        root_node = Node(root_eq_label)
         queue = deque([root_node])
+        # BFS to consume spec map.
         while queue:
             v = queue.popleft()
             rule = d.get(v.label, ())
@@ -330,16 +548,189 @@ def _create_spec(d: SpecMap, pi: ParallelInfo) -> CombinatorialSpecification:
                 queue.extend(children)
                 v.children = children
             visited.add(v.label)
-        rules = SpecificationRuleExtractor(
-            pi.root_eq_label, root_node, pi.r_db, pi.searcher.classdb
-        ).rules()
-        return CombinatorialSpecification(pi.root_class, rules)
+        return root_node
+
+
+class EqPathParallelSpecFinder(
+    ParallelSpecFinder[ClassType1, ObjType1, ClassType2, ObjType2]
+):
+    """
+    A version of ParallelSpecFinder that supports nonequivalent
+    classes sharing equivalence labels.
+    """
+
+    def __init__(
+        self,
+        searcher1: CombinatorialSpecificationSearcher[ClassType1],
+        searcher2: CombinatorialSpecificationSearcher[ClassType2],
+    ):
+        super().__init__(searcher1, searcher2)
 
+        # Tracks the path taken in the second search
+        self._path: List[Tuple[int, int, int, int]] = [(-1, -1, -1, -1)]
+
+    def _search_matching_info(
+        self, matching_info: MatchingInfo
+    ) -> Optional[Tuple[SpecMap, SpecMap]]:
+        # This will differ (from super's) that equiv lables must
+        # be validated given the path that has been taken.
+
+        (
+            matching_info1,
+            matching_info2,
+            sp1,
+            sp2,
+        ) = EqPathParallelSpecFinder._search_matching_info_init(matching_info)
 
-def find_bijection_between(
-    searcher1: CombinatorialSpecificationSearcher,
-    searcher2: CombinatorialSpecificationSearcher,
-) -> Optional[Tuple[CombinatorialSpecification, CombinatorialSpecification]]:
-    """Find bijections between two universes. If they are not of the same type, a
-    custom atom comparator is needed."""
-    return ParallelSpecFinder(searcher1, searcher2).find()
+        # For storing results of eq path checking.
+        eq_path_tracker: EqPathTracker = defaultdict(lambda: defaultdict(dict))
+
+        def _rec(
+            id1: int,
+            id2: int,
+            id_sets: Tuple[Set[int], Set[int]],
+        ) -> bool:
+            bc = self._search_matching_info_recursion_base_cases_eq(
+                id1,
+                id2,
+                matching_info,
+                matching_info1,
+                matching_info2,
+                sp1,
+                sp2,
+                self._path[-1],
+                eq_path_tracker,
+            )
+            if bc:
+                return bool(bc + 1)
+            rec1, rec2 = id1 in sp1, id2 in sp2
+            for children1, children2 in filter(
+                lambda c: (id1 not in sp1 or c[0] == sp1[id1])
+                and (id2 not in sp2 or c[1] == sp2[id2]),
+                matching_info[(id1, id2)],
+            ):
+                sp1[id1], sp2[id2] = children1, children2
+                to_clean: Tuple[Set[int], Set[int]] = (set(), set())
+
+                # Check if the path required for the eq labels actually matches
+                if self._eq_path_matches(
+                    id1, id2, *self._path[-1], sp1, sp2, eq_path_tracker
+                ):
+                    valid = True
+                    for j2, ((j1, child1), child2) in enumerate(
+                        zip(
+                            (
+                                (i, children1[i])
+                                for i in matching_info[(id1, id2)][
+                                    (children1, children2)
+                                ]
+                            ),
+                            children2,
+                        )
+                    ):
+                        self._path.append((id1, id2, j1, j2))
+                        if not _rec(child1, child2, to_clean):
+                            valid = False
+                            self._path.pop()
+                            break
+                        self._path.pop()
+                    if valid:
+                        id_sets[0].update(to_clean[0], () if rec1 else (id1,))
+                        id_sets[1].update(to_clean[1], () if rec2 else (id2,))
+                        return True
+                EqPathParallelSpecFinder._clean_descendants(
+                    *to_clean, id1, id2, sp1, sp2, rec1, rec2
+                )
+            return False
+
+        if _rec(
+            self._pi1.root_eq_label,
+            self._pi2.root_eq_label,
+            (set(), set()),
+        ):
+            return sp1, sp2
+        return None
+
+    def _search_matching_info_recursion_base_cases_eq(
+        self,
+        id1: int,
+        id2: int,
+        matching_info: MatchingInfo,
+        matching_info1: MatchingInfoSingle,
+        matching_info2: MatchingInfoSingle,
+        sp1: SpecMap,
+        sp2: SpecMap,
+        relations: Tuple[int, int, int, int],
+        eq_path_tracker: EqPathTracker,
+    ) -> int:
+        pid1, pid2, idx1, idx2 = relations
+        if EqPathParallelSpecFinder._inconsistent_with_matching_info(
+            id1, id2, matching_info, matching_info1, matching_info2, sp1, sp2
+        ):
+            return EqPathParallelSpecFinder._INVALID
+        # These atoms will have matches in the first searcher but we do offer
+        # additional checks which will, by default, always return true.
+        if ((), ()) in matching_info[(id1, id2)]:
+            if not self._atom_path_match(id1, id2, sp1, sp2):
+                return EqPathParallelSpecFinder._INVALID
+            sp1[id1], sp2[id2] = (), ()
+            return EqPathParallelSpecFinder._VALID
+        # If both ids are set we still need to check if they are valid in terms
+        # of eq paths since we may have arrived from different parents.
+        if id1 in sp1 and id2 in sp2:
+            if self._eq_path_matches(
+                id1, id2, pid1, pid2, idx1, idx2, sp1, sp2, eq_path_tracker
+            ):
+                return EqPathParallelSpecFinder._VALID
+            return EqPathParallelSpecFinder._INVALID
+        return EqPathParallelSpecFinder._UNKNOWN
+
+    def _atom_path_match(self, id1: int, id2: int, sp1: SpecMap, sp2: SpecMap) -> bool:
+        """This can be overwritten if the path can affect the validity of the pair."""
+        # pylint: disable=no-self-use
+        return True
+
+    def _eq_path_matches(
+        self,
+        id1,
+        id2,
+        pid1,
+        pid2,
+        idx1: int,
+        idx2: int,
+        sp1: SpecMap,
+        sp2: SpecMap,
+        cache: EqPathTracker,
+    ) -> bool:
+        """
+        Given (grandparent, parent, children) eq labels in both specs, this will check
+        if the actual rules required (disregarding actual equivalence rules) to traverse
+        this path match.
+        """
+        children = (sp1[id1], sp2[id2])
+        children_cache = cache[(id1, id2)][(pid1, pid2)]
+        if children not in children_cache:
+            path1 = EquivalenceRuleExtractor(
+                self._pi1.root_eq_label,
+                self._pi1.searcher.start_label,
+                EqPathParallelSpecFinder._create_tree(sp1, self._pi1.root_eq_label),
+                self._pi1.ruledb,
+                self._pi1.searcher.classdb,
+                id1,
+                pid1,
+                idx1,
+            ).nonequivalent_rules_in_equiv_path()
+            path2 = EquivalenceRuleExtractor(
+                self._pi2.root_eq_label,
+                self._pi2.searcher.start_label,
+                EqPathParallelSpecFinder._create_tree(sp2, self._pi2.root_eq_label),
+                self._pi2.ruledb,
+                self._pi2.searcher.classdb,
+                id2,
+                pid2,
+                idx2,
+            ).nonequivalent_rules_in_equiv_path()
+            children_cache[children] = len(path1) == len(path2) and all(
+                r1.constructor.equiv(r2.constructor)[0] for r1, r2 in zip(path1, path2)
+            )
+        return children_cache[children]
diff --git a/comb_spec_searcher/isomorphism.py b/comb_spec_searcher/isomorphism.py
index c08ee89b1..7a2c571f3 100644
--- a/comb_spec_searcher/isomorphism.py
+++ b/comb_spec_searcher/isomorphism.py
@@ -1,107 +1,190 @@
 from itertools import product
-from typing import TYPE_CHECKING, Callable, Dict, List, Optional, Set, Tuple
-
-from .combinatorial_class import CombinatorialClass, CombinatorialObject
+from typing import (
+    TYPE_CHECKING,
+    Any,
+    Callable,
+    Dict,
+    Generic,
+    List,
+    Optional,
+    Set,
+    Tuple,
+    TypeVar,
+)
+
+from .combinatorial_class import CombinatorialClass
 from .strategies.rule import AbstractRule, Rule
 
 if TYPE_CHECKING:
+    from .combinatorial_class import CombinatorialObject
     from .specification import CombinatorialSpecification
 
 
-AtomEquals = Callable[["CombinatorialClass", "CombinatorialClass"], bool]
-OrderMap = Dict[Tuple[CombinatorialClass, CombinatorialClass], List[int]]
+ObjType1 = TypeVar("ObjType1", bound="CombinatorialObject")
+ClassType1 = TypeVar("ClassType1", bound="CombinatorialClass")
+ClassType2 = TypeVar("ClassType2", bound="CombinatorialClass")
+ObjType2 = TypeVar("ObjType2", bound="CombinatorialObject")
+OrderMap = Dict[Tuple[ClassType1, ClassType2], List[int]]
+IndexDataMap = Optional[Dict[Tuple[ClassType1, ClassType2], object]]
 
 
-class Isomorphism:
+class Isomorphism(Generic[ClassType1, ObjType1, ClassType2, ObjType2]):
     """Isomorphism checker."""
 
     _INVALID, _UNKNOWN, _VALID = range(-1, 2)
 
     @classmethod
     def check(
-        cls, spec1: "CombinatorialSpecification", spec2: "CombinatorialSpecification"
+        cls,
+        spec1: "CombinatorialSpecification[ClassType1, ObjType1]",
+        spec2: "CombinatorialSpecification[ClassType2, ObjType2]",
     ) -> bool:
         """Check if two specs are isomorphic."""
         return cls(spec1, spec2).are_isomorphic()
 
     def __init__(
-        self, spec1: "CombinatorialSpecification", spec2: "CombinatorialSpecification"
+        self,
+        spec1: "CombinatorialSpecification[ClassType1, ObjType1]",
+        spec2: "CombinatorialSpecification[ClassType2, ObjType2]",
     ) -> None:
-        self._rules1: Dict[CombinatorialClass, AbstractRule] = spec1.rules_dict
-        self._rules2: Dict[CombinatorialClass, AbstractRule] = spec2.rules_dict
-        self._ancestors: Set[Tuple[CombinatorialClass, CombinatorialClass]] = set()
-        self._order_map: Dict[
-            Tuple[CombinatorialClass, CombinatorialClass], List[int]
-        ] = {}
-        self._failed: Set[Tuple[CombinatorialClass, CombinatorialClass]] = set()
+        # The specs
+        self._rules1: Dict[
+            ClassType1, AbstractRule[ClassType1, ObjType1]
+        ] = spec1.rules_dict
+        self._rules2: Dict[
+            ClassType2, AbstractRule[ClassType2, ObjType2]
+        ] = spec2.rules_dict
+        self.root1 = spec1.root
+        self.root2 = spec2.root
+
+        # Tracking recursion
+        self._ancestors: Set[Tuple[ClassType1, ClassType2]] = set()
+
+        # Tracking matchin permutations
+        self._order_map: Dict[Tuple[ClassType1, ClassType2], List[int]] = {}
+
+        # Tracking failed matchings
+        self._failed: Set[Tuple[ClassType1, ClassType2]] = set()
+
+        # Tracking additional data
+        self._index_data: Dict[Tuple[ClassType1, ClassType2], object] = {}
+
+        # Tracking paths in terms of child indices
+        self._path_tracker: List[Tuple[Tuple[int, ...], Tuple[int, ...]]] = []
+
+        # Store results
         self._isomorphic = self._are_isomorphic(spec1.root, spec2.root)
 
+    def get_order_data(
+        self,
+    ) -> Dict[Tuple[ClassType1, ClassType2], object]:
+        """Return any index data for nonbijective matches."""
+        return self._index_data
+
     def are_isomorphic(self) -> bool:
         """Check if the two specs are isomorphic."""
         return self._isomorphic
 
     def get_order(
         self,
-    ) -> OrderMap:
+    ) -> OrderMap[ClassType1, ClassType2]:
         """Get order map of corresponding nodes."""
         return self._order_map
 
-    def _are_isomorphic(
-        self, node1: CombinatorialClass, node2: CombinatorialClass
-    ) -> bool:
-        # If there are equivilances, we use the 'latest' one
-        # but we check for recursion for any possible pairing
-        eq_path1, eq_path2 = Isomorphism._get_eq_descendant(
-            node1, self._rules1, node2, self._rules2
-        )
+    def _are_isomorphic(self, node1: ClassType1, node2: ClassType2) -> bool:
+        # Both ends of equivilance paths (len = 1 if none)
+        eq_path1, eq_path2 = self._get_eq_descendant(node1, node2)
+
+        # The ones that are not on the LHS of equivalence rules
         curr1, curr2 = eq_path1[-1], eq_path2[-1]
+
+        # Rules from curr1 and curr2 to their respective children
         rule1, rule2 = self._rules1[curr1], self._rules2[curr2]
 
+        # Any empty children are ignored
         non_empty_ind1, non_empty_ind2 = (
             tuple(i for i, c in enumerate(rule1.children) if not c.is_empty()),
             tuple(i for i, c in enumerate(rule2.children) if not c.is_empty()),
         )
 
+        # Check for base cases (invalid = -1, valid = 1)
         is_base_case = self._base_cases(
             eq_path1, rule1, non_empty_ind1, eq_path2, rule2, non_empty_ind2
         )
         if is_base_case:
             return bool(is_base_case + 1)
 
+        # Update ancestors for recursion
         self._ancestors.update(product(eq_path1, eq_path2))
 
-        # Check all matches of children, if any are valid then trees are isomorphic
+        # The number of nonempty children
         n = len(non_empty_ind1)
+
+        # The permutation of matched children indices
         child_order: List[int] = [-1] * n
-        stack = [(0, i, {i}) for i in range(n - 1, -1, -1)]
+
+        # To avoid repeated index pairs, since outside choices have no effect.
         blacklist: Set[Tuple[int, int]] = set()
+
+        # Iterative stack with elements:
+        # (index1, index2, indices of the second rule's children already matched)
+        stack = [(0, i, {i}) for i in range(n - 1, -1, -1)]
+
+        # Check all pairings of children. Any pairing hat exhaust all nonempty children,
+        # such that all are valid will result in current nodes being matched. This is
+        # done with backtracking.
         while stack:
             i1, i2, in_use = stack.pop()
+
+            # Already failed
             if (i1, i2) in blacklist:
                 continue
+
+            # Track path
+            self._path_tracker_push(
+                non_empty_ind1[i1],
+                non_empty_ind2[i2],
+                len(eq_path1) > 1,
+                len(eq_path2) > 1,
+            )
+
+            # Call _are_isomorphic recursively for current pair
+            # and add to blacklist and try again if we fail.
             if not self._are_isomorphic(
                 rule1.children[non_empty_ind1[i1]], rule2.children[non_empty_ind2[i2]]
             ):
                 blacklist.add((i1, i2))
+                self._path_tracker_pop()
                 continue
+            self._path_tracker_pop()
+
+            # Update permutation
             child_order[i2] = i1
+
+            # If we reach the last index we have succeeded
             if i1 == n - 1:
                 self._order_map[(curr1, curr2)] = child_order
+                # Since we did not conclude this match by recursion we can remove our
+                # current ids from the ancestor set since the next ones we check are
+                # not descendants of the current ids (or their equivalences).
                 self._ancestors.difference_update(product(eq_path1, eq_path2))
                 return True
+
+            # If we have indices to expand, that is done here
             Isomorphism._extend_stack(i1, n, in_use, stack)
+
+        # If stack has been exhausted we have failed to match the ids. We remove them
+        # from the ancestors set, memorize the failure and remove any data gathered.
         self._ancestors.difference_update(product(eq_path1, eq_path2))
         self._failed.add((curr1, curr2))
+        self._index_data.pop((curr1, curr2), None)
         return False
 
-    @staticmethod
     def _get_eq_descendant(
-        node1: CombinatorialClass,
-        rules1: Dict[CombinatorialClass, AbstractRule],
-        node2: CombinatorialClass,
-        rules2: Dict[CombinatorialClass, AbstractRule],
-    ) -> Tuple[List[CombinatorialClass], List[CombinatorialClass]]:
-        rule1, rule2 = rules1[node1], rules2[node2]
+        self, node1: ClassType1, node2: ClassType2
+    ) -> Tuple[List[ClassType1], List[ClassType2]]:
+        """Get path to nodes that are not on the LHS of equivalence rules."""
+        rule1, rule2 = self._rules1[node1], self._rules2[node2]
         nodes1, nodes2 = [node1], [node2]
         if rule1.is_equivalence():
             nodes1.append(rule1.children[0])
@@ -111,13 +194,14 @@ def _get_eq_descendant(
 
     def _base_cases(
         self,
-        eq_nodes1: List[CombinatorialClass],
-        rule1: AbstractRule,
+        eq_nodes1: List[ClassType1],
+        rule1: AbstractRule[ClassType1, ObjType1],
         non_empty_children1: Tuple[int, ...],
-        eq_nodes2: List[CombinatorialClass],
-        rule2: AbstractRule,
+        eq_nodes2: List[ClassType2],
+        rule2: AbstractRule[ClassType2, ObjType2],
         non_empty_children2: Tuple[int, ...],
     ) -> int:
+        # The ones that are not on the LHS of equivalence rules
         curr1, curr2 = eq_nodes1[-1], eq_nodes2[-1]
 
         # Already matched
@@ -135,16 +219,13 @@ def _base_cases(
         # Atoms
         if not rule1.children and not rule2.children:
             if curr1.is_atom() and curr2.is_atom():
-                atom1 = next(curr1.objects_of_size(curr1.minimum_size_of_object()))
-                atom2 = next(curr2.objects_of_size(curr2.minimum_size_of_object()))
-                if atom1.size() == atom2.size():
+                if self._atom_match(curr1, curr2, rule1, rule2):
                     return Isomorphism._VALID
             return Isomorphism._INVALID
 
         # If different type of rules are applied, the trees are not isomorphic
-        # TODO: Use == when implemented
         assert isinstance(rule1, Rule) and isinstance(rule2, Rule)
-        if rule1.constructor.__class__ != rule2.constructor.__class__:
+        if not self._constructor_match(rule1, rule2, curr1, curr2):
             return Isomorphism._INVALID
 
         # Check for recursive match
@@ -153,6 +234,45 @@ def _base_cases(
 
         return Isomorphism._UNKNOWN
 
+    def _path_tracker_push(
+        self, c1: int, c2: int, eq_path1: bool, eq_path2: bool
+    ) -> None:
+        """Store the path being taken."""
+        t1 = (0, c1) if eq_path1 else (c1,)
+        t2 = (0, c2) if eq_path2 else (c2,)
+        self._path_tracker.append((t1, t2))
+
+    def _path_tracker_pop(self) -> None:
+        """Remove last stored step in path."""
+        self._path_tracker.pop()
+
+    def _atom_match(
+        self,
+        atom1: ClassType1,
+        atom2: ClassType2,
+        rule1: AbstractRule[ClassType1, ObjType1],
+        rule2: AbstractRule[ClassType2, ObjType2],
+    ) -> bool:
+        """Returns true if atoms match, false otherwise."""
+        # pylint: disable=no-self-use
+        sz1 = next(atom1.objects_of_size(atom1.minimum_size_of_object())).size()
+        sz2 = next(atom2.objects_of_size(atom2.minimum_size_of_object())).size()
+        return sz1 == sz2 and rule1.get_terms(sz1) == rule2.get_terms(sz2)
+
+    def _constructor_match(
+        self,
+        rule1: Rule[ClassType1, ObjType1],
+        rule2: Rule[ClassType2, ObjType2],
+        curr1: ClassType1,
+        curr2: ClassType2,
+    ) -> bool:
+        are_eq, data = rule1.constructor.equiv(rule2.constructor)
+        if not are_eq:
+            return False
+        if data is not None:
+            self._index_data[(curr1, curr2)] = data
+        return True
+
     @staticmethod
     def _extend_stack(
         i1: int, n: int, in_use: Set[int], stack: List[Tuple[int, int, Set[int]]]
@@ -163,120 +283,136 @@ def _extend_stack(
             stack.append((i1 + 1, i, in_use.union({i})))
 
 
-class Node:
+class Node(Generic[ClassType1, ObjType1, ClassType2, ObjType2]):
     """Parse tree node."""
 
     def __init__(
         self,
-        rule: AbstractRule,
-        obj: CombinatorialObject,
-        get_rule: Callable[[CombinatorialClass], AbstractRule],
+        rule: AbstractRule[ClassType1, ObjType1],
+        obj: ObjType1,
+        get_rule: Callable[[ClassType1], AbstractRule[ClassType1, ObjType1]],
     ):
         self.obj = obj
         self._rule = rule
         if not rule.children:
-            self._children: Tuple[Optional["Node"], ...] = tuple()
+            self._children: Tuple[
+                Optional["Node[ClassType1, ObjType1, ClassType2, ObjType2]"], ...
+            ] = tuple()
         else:
             assert isinstance(rule, Rule)
+            children, self.idx = rule.indexed_forward_map(obj)
             self._children = tuple(
                 type(self)(get_rule(child), child_obj, get_rule)
                 if child_obj is not None
                 else None
-                for child, child_obj in zip(rule.children, rule.forward_map(obj))
+                for child, child_obj in zip(rule.children, children)
                 if not child.is_empty()
             )
 
     def build_obj(
         self,
-        rule: AbstractRule,
-        get_order: OrderMap,
-        get_rule: Callable[[CombinatorialClass], AbstractRule],
-    ) -> CombinatorialObject:
+        rule: AbstractRule[ClassType2, ObjType2],
+        get_order: OrderMap[ClassType1, ClassType2],
+        get_rule: Callable[[ClassType2], AbstractRule[ClassType2, ObjType2]],
+        index_data: Dict[Tuple[ClassType1, ClassType2], object],
+    ) -> ObjType2:
         """Parse tree's recursive build object function."""
 
-        if not self._children:
-            # TODO: stop special casing verification rules!
-            obj: CombinatorialObject = next(
+        atom = not self._children
+        if atom:
+            obj: ObjType2 = next(
                 rule.comb_class.objects_of_size(
                     rule.comb_class.minimum_size_of_object()
                 )
             )
             return obj
+
         if rule.is_equivalence():
             if not self._rule.is_equivalence():
                 assert isinstance(rule, Rule)
-                val: CombinatorialObject = next(
-                    rule.backward_map(
-                        (
-                            self.build_obj(
-                                get_rule(rule.children[0]), get_order, get_rule
-                            ),
-                        )
-                    )
+                val: ObjType2 = rule.indexed_backward_map(
+                    (
+                        self.build_obj(
+                            get_rule(rule.children[0]), get_order, get_rule, index_data
+                        ),
+                    ),
+                    self.idx,
                 )
                 return val
-            order = [0]
+            order = [0]  # If both are equivalences
         elif self._rule.is_equivalence():
             assert self._children[0] is not None
-            return self._children[0].build_obj(rule, get_order, get_rule)
+            return self._children[0].build_obj(rule, get_order, get_rule, index_data)
         else:
             order = get_order[(self._rule.comb_class, rule.comb_class)]
         children = (self._children[idx] for idx in order)
         assert isinstance(rule, Rule)
-        val = next(
-            rule.backward_map(
-                tuple(
-                    c[0].build_obj(get_rule(c[1]), get_order, get_rule)
-                    if c is not None and c[0] is not None
-                    else None
-                    for c in (
-                        None if child.is_empty() else (next(children), child)
-                        for child in rule.children
-                    )
+
+        # Deal with avoiding empty children and supplying ibm with data if any
+        val = rule.indexed_backward_map(
+            tuple(
+                c[0].build_obj(get_rule(c[1]), get_order, get_rule, index_data)
+                if c is not None and c[0] is not None
+                else None
+                for c in (
+                    None if child.is_empty() else (next(children), child)
+                    for child in rule.children
                 )
-            )
+            ),
+            self.idx,
+            index_data.get((self._rule.comb_class, rule.comb_class)),
         )
         return val
 
 
-class ParseTree:
+class ParseTree(Generic[ClassType1, ObjType1, ClassType2, ObjType2]):
     """Parse tree that parses an object and can reconstruct it for the other
     specification."""
 
-    def __init__(self, obj: CombinatorialObject, spec: "CombinatorialSpecification"):
-        self._root = Node(spec.root_rule, obj, spec.get_rule)
+    def __init__(
+        self, obj: ObjType1, spec: "CombinatorialSpecification[ClassType1, ObjType1]"
+    ):
+        self._root = Node[ClassType1, ObjType1, ClassType2, ObjType2](
+            spec.root_rule, obj, spec.get_rule
+        )
 
     def build_obj(
         self,
-        root: AbstractRule,
-        get_order: OrderMap,
-        get_rule: Callable[[CombinatorialClass], AbstractRule],
-    ) -> CombinatorialObject:
+        root: AbstractRule[ClassType2, ObjType2],
+        get_order: OrderMap[ClassType1, ClassType2],
+        get_rule: Callable[[ClassType2], AbstractRule[ClassType2, ObjType2]],
+        index_data: Dict[Tuple[ClassType1, ClassType2], object],
+    ) -> ObjType2:
         """Build object from the other specification."""
-        return self._root.build_obj(root, get_order, get_rule)
+        return self._root.build_obj(root, get_order, get_rule, index_data)
 
 
-class Bijection:
+class Bijection(Generic[ClassType1, ObjType1, ClassType2, ObjType2]):
     """A bijection object that contains a map between two specifications."""
 
     @classmethod
     def construct(
         cls,
-        spec: "CombinatorialSpecification",
-        other: "CombinatorialSpecification",
-    ) -> Optional["Bijection"]:
+        spec: "CombinatorialSpecification[ClassType1, ObjType1]",
+        other: "CombinatorialSpecification[ClassType2, ObjType2]",
+    ) -> Optional["Bijection[ClassType1, ObjType1, ClassType2, ObjType2]"]:
         """Create a bijection object between two specifications if possible."""
-        iso = Isomorphism(spec, other)
+        iso = Isomorphism[ClassType1, ObjType1, ClassType2, ObjType2](spec, other)
         if not iso.are_isomorphic():
             return None
-        return cls(spec, other, iso.get_order())
+        return cls(spec, other, iso.get_order(), iso.get_order_data())
 
     def __init__(
         self,
-        spec: "CombinatorialSpecification",
-        other: "CombinatorialSpecification",
-        get_order: OrderMap,
+        spec: "CombinatorialSpecification[ClassType1, ObjType1]",
+        other: "CombinatorialSpecification[ClassType2, ObjType2]",
+        get_order: OrderMap[ClassType1, ClassType2],
+        index_data: IndexDataMap = None,
     ):
+        self._index_data = {} if index_data is None else index_data
+        self._inv_index_data = {
+            (t2, t1): data for (t1, t2), data in self._index_data.items()
+        }
         self._spec = spec
         self._other = other
         self._get_order = get_order
@@ -285,11 +421,13 @@ def __init__(
         }
 
     @property
-    def domain(self) -> "CombinatorialSpecification":
+    def domain(self) -> "CombinatorialSpecification[ClassType1, ObjType1]":
+        """The root class of the first specification."""
         return self._spec
 
     @property
-    def codomain(self) -> "CombinatorialSpecification":
+    def codomain(self) -> "CombinatorialSpecification[ClassType2, ObjType2]":
+        """The root class of the second specification."""
         return self._other
 
     @staticmethod
@@ -299,21 +437,48 @@ def _perm_inv(perm: List[int]) -> List[int]:
             inv[v] = i
         return inv
 
-    def map(self, obj: CombinatorialObject) -> CombinatorialObject:
-        """Map an object of the root of one specification to the root of the other."""
-        parse_tree = ParseTree(obj, self._spec)
+    def map(self, obj: ObjType1) -> ObjType2:
+        """Map an object of the domain to an object of the codomain."""
+        parse_tree = ParseTree[ClassType1, ObjType1, ClassType2, ObjType2](
+            obj, self._spec
+        )
         return parse_tree.build_obj(
-            self._other.root_rule, self._get_order, self._other.get_rule
+            self._other.root_rule,
+            self._get_order,
+            self._other.get_rule,
+            self._index_data,
         )
 
-    def inverse_map(self, obj: CombinatorialObject) -> CombinatorialObject:
-        parse_tree = ParseTree(obj, self._other)
+    def inverse_map(self, obj: ObjType2) -> ObjType1:
+        """Map an object of the codomain to an object of the domain."""
+        # Swap types and use inverse versions of tuple maps
+        parse_tree = ParseTree[ClassType2, ObjType2, ClassType1, ObjType1](
+            obj, self._other
+        )
         return parse_tree.build_obj(
-            self._spec.root_rule, self._get_inverse_order, self._spec.get_rule
+            self._spec.root_rule,
+            self._get_inverse_order,
+            self._spec.get_rule,
+            self._inv_index_data,
         )
 
     def to_jsonable(self) -> dict:
         """Return a JSON serializable dictionary for the bijection."""
+        id_map, classes = self._classes_to_array()
+        reconstructed_order: Dict[str, Dict[str, List[int]]] = {}
+        reconstructed_data: Dict[str, Dict[str, object]] = {}
+        Bijection._populate_json_map(self._get_order, reconstructed_order, id_map)
+        Bijection._populate_json_map(self._index_data, reconstructed_data, id_map)
+        return {
+            "spec": self._spec.to_jsonable(),
+            "other": self._other.to_jsonable(),
+            "order": reconstructed_order,
+            "index_data": reconstructed_data,
+            "classes": classes,
+        }
+
+    def _classes_to_array(self) -> Tuple[Dict[CombinatorialClass, str], List[dict]]:
+        """Dump classes into an array with indices as keys to simplify maps."""
         id_map: Dict[CombinatorialClass, str] = {}
         classes: List[dict] = []
         for c1, c2 in self._get_order.keys():
@@ -323,35 +488,41 @@ def to_jsonable(self) -> dict:
             if c2 not in id_map:
                 id_map[c2] = f"{len(classes)}"
                 classes.append(c2.to_jsonable())
+        return id_map, classes
 
-        reconstructed_map: Dict[str, Dict[str, List[int]]] = {}
-        for (c1, c2), lis in self._get_order.items():
+    @staticmethod
+    def _populate_json_map(
+        tuple_map: Dict[Tuple[ClassType1, ClassType2], Any],
+        json_map: Dict[str, Dict[str, Any]],
+        id_map: Dict[CombinatorialClass, str],
+    ) -> None:
+        """Convert tuple maps into valid json maps."""
+        for (c1, c2), value in tuple_map.items():
             i1, i2 = id_map[c1], id_map[c2]
-            if i1 not in reconstructed_map:
-                reconstructed_map[i1] = {i2: lis}
+            if i1 not in json_map:
+                json_map[i1] = {i2: value}
             else:
-                reconstructed_map[i1][i2] = lis
-        return {
-            "spec": self._spec.to_jsonable(),
-            "other": self._other.to_jsonable(),
-            "order": reconstructed_map,
-            "classes": classes,
-        }
+                json_map[i1][i2] = value
 
     @classmethod
-    def from_dict(cls, d):
+    def from_dict(cls, d) -> "Bijection":
         """Return the bijection with the dictionary outputter by
         the 'to_jsonable' method.
         """
         # pylint: disable=import-outside-toplevel
         from comb_spec_searcher import CombinatorialSpecification
 
-        spec1 = CombinatorialSpecification.from_dict(d["spec"])
-        spec2 = CombinatorialSpecification.from_dict(d["other"])
+        spec1 = CombinatorialSpecification[ClassType1, ObjType1].from_dict(d["spec"])
+        spec2 = CombinatorialSpecification[ClassType2, ObjType2].from_dict(d["other"])
         order = [CombinatorialClass.from_dict(c) for c in d["classes"]]
         get_order = {
             (order[int(idx1)], order[int(idx2)]): lis
             for idx1, sub_map in d["order"].items()
             for idx2, lis in sub_map.items()
         }
-        return cls(spec1, spec2, get_order)
+        index_data = {
+            (order[int(idx1)], order[int(idx2)]): data
+            for idx1, sub_map in d["index_data"].items()
+            for idx2, data in sub_map.items()
+        }
+        return cls(spec1, spec2, get_order, index_data)  # type: ignore
diff --git a/comb_spec_searcher/specification_extrator.py b/comb_spec_searcher/specification_extrator.py
index c6bd34891..b8dec2aad 100644
--- a/comb_spec_searcher/specification_extrator.py
+++ b/comb_spec_searcher/specification_extrator.py
@@ -1,9 +1,12 @@
 import itertools
-from typing import TYPE_CHECKING, Dict, Iterator, Tuple
+from collections import deque
+from operator import itemgetter
+from typing import TYPE_CHECKING, Deque, Dict, Iterator, List, Set, Tuple
 
 from comb_spec_searcher.class_db import ClassDB
 from comb_spec_searcher.strategies.rule import AbstractRule, Rule
 from comb_spec_searcher.tree_searcher import Node
+from comb_spec_searcher.typing import RuleKey
 
 if TYPE_CHECKING:
     from comb_spec_searcher.rule_db.base import RuleDBBase
@@ -39,13 +42,7 @@ def _populate_equivalences(self) -> None:
         Populate the rules dict with the labels of equivalences rules needed to make
         every class be on a right hand side.
         """
-        all_rhs = itertools.chain.from_iterable(self.rules_dict.values())
-        no_lhs_labels = set(
-            itertools.filterfalse(self.rules_dict.__contains__, all_rhs)
-        )
-        if self.root_label not in self.rules_dict:
-            no_lhs_labels.add(self.root_label)
-        for label in no_lhs_labels:
+        for label in self._no_lhs_labels():
             eqv_label = self.ruledb.equivdb[label]
             path = self.ruledb.equivdb.find_path(
                 label, self.eqvparent_to_parent[eqv_label]
@@ -57,6 +54,18 @@ def _populate_equivalences(self) -> None:
                     break
                 self.rules_dict[parent] = (child,)
 
+    def _no_lhs_labels(self) -> Set[int]:
+        """
+        Find labels that are not a lhs of any rule.
+        """
+        all_rhs = itertools.chain.from_iterable(self.rules_dict.values())
+        no_lhs_labels = set(
+            itertools.filterfalse(self.rules_dict.__contains__, all_rhs)
+        )
+        if self.root_label not in self.rules_dict:
+            no_lhs_labels.add(self.root_label)
+        return no_lhs_labels
+
     def _check(self):
         """
         Perform a check to make sure that the spec make sense.
@@ -113,3 +122,189 @@ def _missing_rule_error(self, parent: int, children: Tuple[int, ...]) -> ValueEr
     def rules(self) -> Iterator[AbstractRule]:
         for parent, children in self.rules_dict.items():
             yield self._find_rule(parent, children)
+
+
+class PartialSpecificationRuleExtractor(SpecificationRuleExtractor):
+    """A base class for extractors for incomplete specifications."""
+
+    def _populate_decompositions(self) -> None:
+        pass
+
+    def _populate_equivalences(self) -> None:
+        # SpecificationRuleExtractor's with a try-catch do deal with incomplete spec
+        for label in self._no_lhs_labels():
+            eqv_label = self.ruledb.equivdb[label]
+            # Might not exist because spec is incomplete.
+            try:
+                path = self.ruledb.equivdb.find_path(
+                    label, self.eqvparent_to_parent[eqv_label]
+                )
+            except KeyError:
+                continue
+            for parent, child in zip(path[:-1], path[1:]):
+                if parent in self.rules_dict:
+                    break
+                self.rules_dict[parent] = (child,)
+
+    def _check(self):
+        pass
+
+    def _ordered_eqvrule_to_rule(
+        self,
+    ) -> Tuple[Dict[RuleKey, RuleKey], Dict[RuleKey, Tuple[int, ...]]]:
+        """Altered version of rule_from_equivalence_rule_dict that deals with order."""
+        eqv_rules = set(self.eqv_rulekeys)
+        eqvrule_to_rule: Dict[RuleKey, RuleKey] = {}
+        # Maps our children index order to that of the actual rules
+        index_order_map: Dict[RuleKey, Tuple[int, ...]] = {}
+        for start, ends in self.ruledb.rule_to_strategy:
+            eqv_start = self.ruledb.equivdb[start]
+            # Sort but keep knowledge of original order
+            index_order, eqv_ends = (
+                zip(
+                    *sorted(
+                        enumerate(map(self.ruledb.equivdb.__getitem__, ends)),
+                        key=itemgetter(1),
+                    )
+                )
+                if ends
+                else ((), ())
+            )
+
+            eqv_key = (eqv_start, eqv_ends)
+            index_order_map[eqv_key] = index_order
+            if eqv_key in eqv_rules:
+                eqvrule_to_rule[eqv_key] = (start, ends)
+        return eqvrule_to_rule, index_order_map
+
+
+class EquivalenceRuleExtractor(PartialSpecificationRuleExtractor):
+    """
+    This class extracts the actual rules that would be created for an equivalence
+    label given a partial spec that is traversable from root. Suppose we want the
+    rules for the parent in `grandparent-parent-children` than what rules are used
+    will depend on the grandparent and children and we are looking for the rules
+    that have the same equivalance label on both the LHS and RHS and in the order they
+    would be traversed from the root.
+    """
+
+    def __init__(
+        self,
+        root_eq_label: int,
+        root_class_label: int,
+        root_node: Node,
+        ruledb: "RuleDBBase",
+        classdb: ClassDB,
+        target: int,
+        parent_of_target: int,
+        idx: int,
+    ):
+        # parent
+        self.target = target
+        # grandparent
+        self.parent_of_target = parent_of_target
+        # grandparent.children[idx] is parent
+        self.idx = idx
+        # class label of the LHS of the first rule for the eq path, updated later
+        self.start = root_class_label
+        # class label of the RHS of the last rule for the eq path, updated later
+        self.end = -1
+        # Children are included in the tree
+        super().__init__(root_eq_label, root_node, ruledb, classdb)
+
+    def _populate_decompositions(self) -> None:
+        eqvrule_to_rule, index_order_map = self._ordered_eqvrule_to_rule()
+        for eqvrule in self.eqv_rulekeys:
+            # Might not exist because spec is incomplete.
+            try:
+                parent, children = eqvrule_to_rule[eqvrule]
+            except KeyError:
+                continue
+            self.rules_dict[parent] = children
+            self.eqvparent_to_parent[eqvrule[0]] = parent
+            # If grandparent, then we can find our starting point
+            # If no grandparent exists, this will always be the root.
+            if eqvrule[0] == self.parent_of_target:
+                self.start = children[index_order_map[eqvrule][self.idx]]
+            # If parent, we have our end point
+            if eqvrule[0] == self.target:
+                self.end = parent
+
+    def nonequivalent_rules_in_equiv_path(self) -> List[Rule]:
+        return list(self._nonequivalent_rules_in_equiv_path())
+
+    def _nonequivalent_rules_in_equiv_path(self) -> Iterator[Rule]:
+        path = self.ruledb.equivdb.find_path(self.start, self.end)
+        for p, c in zip(path, path[1:]):
+            rule = self._find_rule(p, (c,))
+            # If rule is an actual equivalence rule, we don't care and ignore it.
+            if not rule.is_equivalence():
+                assert isinstance(rule, Rule)
+                yield rule
+
+
+class RulePathToAtomExtractor(PartialSpecificationRuleExtractor):
+    """
+    This class extracts rules from the root down to an atom in a specification (in terms
+    of eq label maps) that is not complete but contains a path from root to said atom.
+    """
+
+    def __init__(
+        self,
+        root_class_label: int,
+        root_label: int,
+        root_node: Node,
+        ruledb: "RuleDBBase",
+        classdb: ClassDB,
+        path: List[Tuple[int, int]],
+    ):
+        self.root_class_label = root_class_label
+        self.path = path
+        self.path.pop()  # remove padded -1
+        self.search_order: Dict[int, Tuple[int, ...]] = {}
+        super().__init__(root_label, root_node, ruledb, classdb)
+
+    def _populate_decompositions(self) -> None:
+        eqvrule_to_rule, index_order_map = self._ordered_eqvrule_to_rule()
+        for eqvrule in self.eqv_rulekeys:
+            try:
+                parent, children = eqvrule_to_rule[eqvrule]
+            except KeyError:
+                continue
+            self.rules_dict[parent] = children
+            self.eqvparent_to_parent[eqvrule[0]] = parent
+
+            # Order in searcher
+            order = index_order_map[eqvrule]
+            self.search_order[parent] = tuple(
+                children[order[i]] for i in range(len(children))
+            )
+
+    def rule_path(self) -> Deque[Tuple[AbstractRule, int]]:
+        curr_class = self.root_class_label
+        path: Deque[Tuple[AbstractRule, int]] = deque([])
+        while self.path:
+            children = self.rules_dict[curr_class]
+            if (
+                len(children) == 1
+                and self.ruledb.equivdb[curr_class] == self.ruledb.equivdb[children[0]]
+            ):
+                # If rule is within eq class, we add it with idx 0
+                path.append((self._find_rule(curr_class, children), 0))
+                curr_class = children[0]
+            else:
+                _, idx = self.path.pop()
+                rule = self._find_rule(curr_class, children)
+                # The idx given by the searcher might differ from that of rule_dict
+                # and we use search_order to get the corresponding index in rule_dict
+                next_child = self.search_order[curr_class][idx]
+                # Get the first child that matches the label of the child we want.
+                # If there are multiple, it does not matter which one.
+                rule_idx = next(
+                    i
+                    for i, c in enumerate(rule.children)
+                    if self.classdb.get_label(c) == next_child
+                )
+                path.append((rule, rule_idx))
+                curr_class = next_child
+        return path
diff --git a/comb_spec_searcher/strategies/__init__.py b/comb_spec_searcher/strategies/__init__.py
index 2bba8ad17..8a67a3ff2 100644
--- a/comb_spec_searcher/strategies/__init__.py
+++ b/comb_spec_searcher/strategies/__init__.py
@@ -5,7 +5,13 @@
     DisjointUnion,
     Quotient,
 )
-from .rule import EquivalencePathRule, ReverseRule, Rule, VerificationRule
+from .rule import (
+    EquivalencePathRule,
+    NonBijectiveRule,
+    ReverseRule,
+    Rule,
+    VerificationRule,
+)
 from .strategy import (
     AbstractStrategy,
     AtomStrategy,
@@ -28,6 +34,7 @@
     "EquivalencePathRule",
     "ReverseRule",
     "Rule",
+    "NonBijectiveRule",
     "VerificationRule",
     "AbstractStrategy",
     "AtomStrategy",
diff --git a/comb_spec_searcher/strategies/constructor/base.py b/comb_spec_searcher/strategies/constructor/base.py
index 6301d5500..e2015902a 100644
--- a/comb_spec_searcher/strategies/constructor/base.py
+++ b/comb_spec_searcher/strategies/constructor/base.py
@@ -3,8 +3,9 @@
 enumeration, generate objects, and sample objects.
 """
 import abc
+from collections import Counter
 from functools import partial
-from typing import Callable, Generic, Iterator, List, Optional, Tuple
+from typing import Callable, Dict, Generic, Iterator, List, Optional, Set, Tuple
 
 import sympy
 
@@ -96,3 +97,75 @@ def build_param_map(
             child_pos_to_parent_pos,
             num_parent_params,
         )
+
+    @abc.abstractmethod
+    def equiv(self, other: "Constructor") -> Tuple[bool, Optional[object]]:
+        """Two constructors are equiv if A <self> B and C <obj> D are isomorphic for any
+        combinatorial classes A, B, C and D where A and C are isomorphic and B and D.
+        This must be implemented for bijections. The second returned value is optional
+        data for bijections. It is used to pass additional arguments to determine index
+        ordering. It needs to be JSON compatible for bijection's to_jsonable and
+        from_dict to work.
+        """
+
+    @staticmethod
+    def extra_params_equiv(
+        params1: Tuple[Dict[str, str], ...],
+        params2: Tuple[Dict[str, str], ...],
+    ) -> bool:
+        """A base equiv for extra params that will suffice for most constructors."""
+        non_empty1 = tuple(par for par in params1 if par)
+        non_empty2 = tuple(par for par in params2 if par)
+        n = len(non_empty1)
+        if len(non_empty2) != n:
+            return False
+        if n == 0:
+            return True
+        return Constructor._extra_params_match_bijection(n, non_empty1, non_empty2)
+
+    @staticmethod
+    def _extra_params_match_single(par1: Dict[str, str], par2: Dict[str, str]) -> bool:
+        """Two parameter dictionaries are equivalent if they have the same number
+        of keys if there is a value with k keys mapping to it, then there is a
+        corresponding value with k keys mapping to it in the other one.
+        """
+        return len(par1) == len(par2) and sorted(
+            Counter(par1.values()).values()
+        ) == sorted(Counter(par2.values()).values())
+
+    @staticmethod
+    def _extra_params_match_bijection(
+        n: int, p1: Tuple[Dict[str, str], ...], p2: Tuple[Dict[str, str], ...]
+    ) -> bool:
+        """Check if there is a bijection between the two tuples of params
+        such that they are pairwise equivalent."""
+
+        # Shared variables in recursion
+        bijection: List[int] = []
+        in_use: Set[int] = set()
+        cache: Dict[Tuple[int, int], bool] = {}
+
+        def _backtracking() -> bool:
+            for i in range(n):
+                if i in in_use:
+                    continue
+                bijection.append(i)
+                in_use.add(i)
+
+                k = len(bijection)
+                key = (k - 1, i)
+                res = cache.get(key, None)
+                if res is None:
+                    res = Constructor._extra_params_match_single(p1[key[0]], p2[key[1]])
+                    cache[key] = res
+
+                # Check if consistent and either done or recursive success.
+                res = res and (k == n or _backtracking())
+
+                bijection.pop()
+                in_use.remove(i)
+                if res:
+                    return True
+            return False
+
+        return _backtracking()
diff --git a/comb_spec_searcher/strategies/constructor/cartesian.py b/comb_spec_searcher/strategies/constructor/cartesian.py
index 18307bc7f..184bcf2e5 100644
--- a/comb_spec_searcher/strategies/constructor/cartesian.py
+++ b/comb_spec_searcher/strategies/constructor/cartesian.py
@@ -351,6 +351,15 @@ def get_op_symbol() -> str:
     def __str__(self) -> str:
         return "Cartesian product"
 
+    def equiv(self, other: "Constructor") -> Tuple[bool, Optional[object]]:
+        return (
+            isinstance(other, type(self))
+            and CartesianProduct.extra_params_equiv(
+                self.extra_parameters, other.extra_parameters
+            ),
+            None,
+        )
+
 
 class Quotient(Constructor[CombinatorialClassType, CombinatorialObjectType]):
     """
@@ -606,3 +615,12 @@ def random_sample_sub_objects(
 
     def __str__(self):
         return "quotient"
+
+    def equiv(self, other: "Constructor") -> Tuple[bool, Optional[object]]:
+        return (
+            isinstance(other, type(self))
+            and Quotient.extra_params_equiv(
+                self.extra_parameters, other.extra_parameters
+            ),
+            None,
+        )
diff --git a/comb_spec_searcher/strategies/constructor/disjoint.py b/comb_spec_searcher/strategies/constructor/disjoint.py
index 0233ec26e..cbd750b90 100644
--- a/comb_spec_searcher/strategies/constructor/disjoint.py
+++ b/comb_spec_searcher/strategies/constructor/disjoint.py
@@ -194,6 +194,15 @@ def get_op_symbol() -> str:
     def __str__(self):
         return "disjoint union"
 
+    def equiv(self, other: "Constructor") -> Tuple[bool, Optional[object]]:
+        return (
+            isinstance(other, type(self))
+            and DisjointUnion.extra_params_equiv(
+                self.extra_parameters, other.extra_parameters
+            ),
+            None,
+        )
+
 
 class Complement(Constructor[CombinatorialClassType, CombinatorialObjectType]):
     """
@@ -338,3 +347,12 @@ def random_sample_sub_objects(
 
     def __str__(self):
         return "complement"
+
+    def equiv(self, other: "Constructor") -> Tuple[bool, Optional[object]]:
+        return (
+            isinstance(other, type(self))
+            and Complement.extra_params_equiv(
+                self.extra_parameters, other.extra_parameters
+            ),
+            None,
+        )
diff --git a/comb_spec_searcher/strategies/rule.py b/comb_spec_searcher/strategies/rule.py
index 4a7501c76..1b14a0ff5 100644
--- a/comb_spec_searcher/strategies/rule.py
+++ b/comb_spec_searcher/strategies/rule.py
@@ -1,8 +1,12 @@
+# pylint: disable=too-many-lines
+
 """
 The rule class is used for a specific application of a strategy on a combinatorial
 class. This is not something the user should implement, as it is just a wrapper for
 calling the Strategy class and storing its results.
 """
+
+
 import abc
 import random
 from collections import defaultdict
@@ -389,6 +393,29 @@ def forward_map(
         """
         return self.strategy.forward_map(self.comb_class, obj, self.children)
 
+    def indexed_forward_map(
+        self,
+        obj: CombinatorialObjectType,
+        data: Optional[object] = None,
+    ) -> Tuple[Tuple[Optional[CombinatorialObjectType], ...], int]:
+        """
+        A version of forward_map that is used for bijections. The idx is used
+        create a bijection from a nonbijective rule.
+        """
+        return self.forward_map(obj), 0
+
+    def indexed_backward_map(
+        self,
+        objs: Tuple[Optional[CombinatorialObjectType], ...],
+        idx: int,
+        data: Optional[object] = None,
+    ) -> CombinatorialObjectType:
+        """
+        A version of backward_map that is used for bijections. The idx is used
+        create a bijection from a nonbijective rule.
+        """
+        return next(self.backward_map(objs))
+
     def to_equivalence_rule(self) -> "EquivalenceRule":
         """
         Return the version of the rule where the empty children are removed.
@@ -578,6 +605,49 @@ def subrec(n: int, **parameters: int) -> int:
         return True
 
 
+class NonBijectiveRule(Rule[CombinatorialClassType, CombinatorialObjectType]):
+    def indexed_forward_map(
+        self,
+        obj: CombinatorialObjectType,
+        data: Optional[object] = None,
+    ) -> Tuple[Tuple[Optional[CombinatorialObjectType], ...], int]:
+        img = self.forward_map(obj)
+        return img, self._forward_order(obj, img, data)
+
+    def indexed_backward_map(
+        self,
+        objs: Tuple[Optional[CombinatorialObjectType], ...],
+        idx: int,
+        data: Optional[object] = None,
+    ) -> CombinatorialObjectType:
+        return self._backward_order_item(idx, objs, data)
+
+    @abc.abstractmethod
+    def _forward_order(
+        self,
+        obj: CombinatorialObjectType,
+        image: Tuple[Optional[CombinatorialObjectType], ...],
+        data: Optional[object] = None,
+    ) -> int:
+        """For rules that do not have an injective forward_map, we can mark the
+        resulting object with a number i (that depends on the object we map from)
+        in order to achieve a bijection. The backward map will then take said
+        number and yield the i-th element (by some predefined order). This requires
+        the backward_map's order to be deterministic.
+        """
+
+    @abc.abstractmethod
+    def _backward_order_item(
+        self,
+        idx: int,
+        objs: Tuple[Optional[CombinatorialObjectType], ...],
+        data: Optional[object] = None,
+    ) -> CombinatorialObjectType:
+        """Given an iterator of all possible domain elements for an indexed forward map
+        and an index, this method will return the element that maps to said index.
+        """
+
+
 class EquivalenceRule(Rule[CombinatorialClassType, CombinatorialObjectType]):
     def __init__(self, rule: Rule[CombinatorialClassType, CombinatorialObjectType]):
         non_empty_children = rule.non_empty_children()
diff --git a/example.py b/example.py
index defe846db..f5ea46659 100644
--- a/example.py
+++ b/example.py
@@ -40,15 +40,15 @@
 
 from comb_spec_searcher import (
     AtomStrategy,
-    Bijection,
     CartesianProductStrategy,
     CombinatorialClass,
     CombinatorialObject,
     CombinatorialSpecificationSearcher,
     DisjointUnionStrategy,
     StrategyPack,
-    find_bijection_between,
 )
+from comb_spec_searcher.bijection import ParallelSpecFinder
+from comb_spec_searcher.isomorphism import Bijection
 
 
 class Word(str, CombinatorialObject):
@@ -366,22 +366,20 @@ def __repr__(self) -> str:
         "(press any key to continue)"
     )
 
-    specs = find_bijection_between(
+    specs = ParallelSpecFinder[AvoidingWithPrefix, Word, AvoidingWithPrefix, Word](
         CombinatorialSpecificationSearcher(
             AvoidingWithPrefix(Word(), ["00"], ["0", "1"]), pack
         ),
         CombinatorialSpecificationSearcher(
             AvoidingWithPrefix(Word(), ["11"], ["0", "1"]), pack
         ),
-    )
-    if specs is None:
-        print("No bijection found")
-    else:
-        spec1, spec2 = specs
-        bijection = Bijection.construct(spec1, spec2)
-        assert bijection is not None
-        for i in range(5):
-            for word in bijection.domain.generate_objects_of_size(i):
-                mapped_to = bijection.map(word)
-                assert bijection.inverse_map(mapped_to) == word
-                print(f"{word} -> {mapped_to}")
+    ).find()
+    assert specs is not None
+    spec1, spec2 = specs
+    bijection = Bijection.construct(spec1, spec2)
+    assert bijection is not None
+    for i in range(5):
+        for word in bijection.domain.generate_objects_of_size(i):
+            mapped_to = bijection.map(word)
+            assert bijection.inverse_map(mapped_to) == word
+            print(f"{word} -> {mapped_to}")


Test patch:
diff --git a/tests/test_bijections.py b/tests/test_bijections.py
index 45887adb2..067df1995 100644
--- a/tests/test_bijections.py
+++ b/tests/test_bijections.py
@@ -1,13 +1,26 @@
 import json
+from typing import Optional
 
 from comb_spec_searcher import (
     AtomStrategy,
     CombinatorialSpecificationSearcher,
     StrategyPack,
 )
-from comb_spec_searcher.bijection import find_bijection_between
+from comb_spec_searcher.bijection import ParallelSpecFinder
 from comb_spec_searcher.isomorphism import Bijection
-from example import AvoidingWithPrefix, ExpansionStrategy, RemoveFrontOfPrefix
+from example import AvoidingWithPrefix, ExpansionStrategy, RemoveFrontOfPrefix, Word
+
+
+def find_bijection_between(
+    searcher1: CombinatorialSpecificationSearcher[AvoidingWithPrefix],
+    searcher2: CombinatorialSpecificationSearcher[AvoidingWithPrefix],
+) -> Optional[Bijection]:
+    specs = ParallelSpecFinder[AvoidingWithPrefix, Word, AvoidingWithPrefix, Word](
+        searcher1, searcher2
+    ).find()
+    if specs is not None:
+        s1, s2 = specs
+        return Bijection.construct(s1, s2)
 
 
 def get_word_searcher(avoid, alphabet):
@@ -23,7 +36,7 @@ def get_word_searcher(avoid, alphabet):
     return searcher
 
 
-def get_specs(alphabet1, avoid1, alphabet2, avoid2):
+def get_bijection(alphabet1, avoid1, alphabet2, avoid2):
     s1, s2 = get_word_searcher(avoid1, alphabet1), get_word_searcher(avoid2, alphabet2)
     return find_bijection_between(s1, s2)
 
@@ -47,26 +60,26 @@ def assert_mappings(bijection):
 
 
 def test_finding_bijection_and_map_in_words():
-    specs = get_specs(["0", "1"], ["00"], ["0", "1"], ["11"])
-    assert specs is not None
-    assert_mappings(Bijection.construct(*specs))
+    bijection = get_bijection(["0", "1"], ["00"], ["0", "1"], ["11"])
+    assert bijection is not None
+    assert_mappings(bijection)
 
 
 def test_finding_bijection_and_map_in_words2():
-    specs = get_specs(["a", "b"], ["aa"], ["0", "1"], ["11"])
-    assert specs is not None
-    assert_mappings(Bijection.construct(*specs))
+    bijection = get_bijection(["a", "b"], ["aa"], ["0", "1"], ["11"])
+    assert bijection is not None
+    assert_mappings(bijection)
 
 
 def test_finding_bijection_and_map_in_words3():
-    specs = get_specs(["0", "1"], ["1011", "101"], ["0", "1"], ["010", "0101"])
-    assert specs is not None
-    assert_mappings(Bijection.construct(*specs))
+    bijection = get_bijection(["0", "1"], ["1011", "101"], ["0", "1"], ["010", "0101"])
+    assert bijection is not None
+    assert_mappings(bijection)
 
 
 def test_non_equal_classes():
-    specs = get_specs(["0", "1"], ["00"], ["0", "1"], ["101"])
-    assert specs is None
+    bijection = get_bijection(["0", "1"], ["00"], ["0", "1"], ["101"])
+    assert bijection is None
 
 
 def test_constructing_bijection_non_eq_classes():
@@ -80,10 +93,8 @@ def test_constructing_bijection_non_eq_classes():
 
 
 def test_bijection_jsonable():
-    specs = get_specs(["0", "1"], ["1011", "101"], ["0", "1"], ["010", "0101"])
-    assert specs is not None
+    bijection = get_bijection(["0", "1"], ["1011", "101"], ["0", "1"], ["010", "0101"])
+    assert bijection is not None
     assert_mappings(
-        Bijection.from_dict(
-            json.loads(json.dumps(Bijection.construct(*specs).to_jsonable()))
-        )
+        Bijection.from_dict(json.loads(json.dumps(bijection.to_jsonable())))
     )