Merge branch 'create-split-by-nodes-alternative' into create-split-by…

…-nodes

pyk/src/pyk/cterm/cterm.py

@@ -334,7 +334,8 @@ def add_constraint(self, constraint: KInner) -> CSubst:
     def apply(self, cterm: CTerm) -> CTerm:
         """Apply this `CSubst` to the given `CTerm` (instantiating the free variables, and adding the constraints)."""
         config = self.subst(cterm.config)
-        return CTerm(config, [self.constraint])
+        constraints = [self.subst(constraint) for constraint in cterm.constraints] + list(self.constraints)
+        return CTerm(config, constraints)
 
 
 def cterm_build_claim(

pyk/src/pyk/kcfg/kcfg.py

@@ -1044,10 +1044,15 @@ def create_split_by_nodes(self, source_id: NodeIdLike, target_ids: Iterable[Node
         """Create a split without crafting a CSubst."""
         source = self.node(source_id)
         targets = [self.node(nid) for nid in target_ids]
-        substs = [source.cterm.config.match(target.cterm.config) for target in targets]
-        if None in substs:
-            return None
-        csubsts = [CSubst(subst, target.cterm.constraints) for subst, target in zip(substs, targets, strict=True)]
+        csubsts: list[CSubst] = []
+
+        for target in targets:
+            subst = source.cterm.config.match(target.cterm.config)
+            if subst is None:
+                return None
+            constraints = [c for c in target.cterm.constraints if c not in source.cterm.constraints]
+            csubsts.append(CSubst(subst, constraints))
+
         return self.create_split(source.id, zip(target_ids, csubsts, strict=True))
 
     def ndbranches(self, *, source_id: NodeIdLike | None = None, target_id: NodeIdLike | None = None) -> list[NDBranch]:

pyk/src/tests/unit/test_kcfg.py

@@ -866,50 +866,3 @@ def test_no_cell_rewrite_to_dots() -> None:
 
     result = no_cell_rewrite_to_dots(term)
     assert result == term
-
-
-def split_kcfg0() -> KCFG:
-    kcfg = KCFG()
-    kcfg.create_node(CTerm(config('X'), (ge('X', 0),)))
-    kcfg.create_node(CTerm(config('X'), (ge('X', 0), lt('X', 3))))
-    kcfg.create_node(CTerm(config('Y'), (ge('Y', 3), lt('Y', 5))))
-    kcfg.create_node(CTerm(config('Z'), (ge('Z', 5),)))
-    return kcfg
-
-
-def split_kcfg1() -> KCFG:
-    """KCFG for split with uncovered constraints."""
-    kcfg = KCFG()
-    kcfg.create_node(CTerm(config('X'), (ge('X', 0),)))
-    kcfg.create_node(CTerm(config('Y'), (ge('Y', 3), lt('Y', 5))))
-    kcfg.create_node(CTerm(config('Z'), (ge('Z', 5),)))
-    return kcfg
-
-
-def split_kcfg2() -> KCFG:
-    """KCFG for split with conflicting constraints."""
-    kcfg = KCFG()
-    kcfg.create_node(CTerm(config('X'), (ge('X', 0),)))
-    kcfg.create_node(CTerm(config('Y'), (lt('X', 3),)))
-    kcfg.create_node(CTerm(config('Z'), (ge('Z', 5),)))
-    return kcfg
-
-
-SPLIT_TEST_CASES = [
-    (split_kcfg0(), 1, [2, 3, 4]),
-    (split_kcfg1(), 1, [2, 3]),
-    (split_kcfg2(), 1, [2, 3]),
-]
-
-
-@pytest.mark.parametrize('kcfg, source_id, target_ids', SPLIT_TEST_CASES)
-def test_create_split_by_nodes(kcfg: KCFG, source_id: int, target_ids: Iterable[int]) -> None:
-    # When
-    new_split = kcfg.create_split_by_nodes(source_id, target_ids)
-
-    # Then
-    assert new_split
-    assert new_split.source == kcfg.node(source_id)
-    assert new_split.targets == tuple(kcfg.node(target_id) for target_id in target_ids)
-    for target_id, csubst in new_split.splits.items():
-        assert csubst.apply(kcfg.node(source_id).cterm) == kcfg.node(target_id).cterm