Create Split without CSubst (#4617)

1. generate `CSubst` from the targets for `Split`
2. fix a bug in `CSubst.apply`.

pyk/src/pyk/cterm/cterm.py

@@ -38,7 +38,7 @@ class CTerm:
 
     Contains the data:
     - `config`: the _configuration_ (structural component of the state, potentially containing free variabls)
-    - `constraints`: conditiions which limit/constraint the free variables from the `config`
+    - `constraints`: conditions which limit/constraint the free variables from the `config`
     """
 
     config: KInner  # TODO Optional?
@@ -253,6 +253,25 @@ def remove_useless_constraints(self, keep_vars: Iterable[str] = ()) -> CTerm:
         return CTerm(self.config, new_constraints)
 
 
+def cterm_match(cterm1: CTerm, cterm2: CTerm) -> CSubst | None:
+    """Find a substitution which can instantiate `cterm1` to `cterm2`.
+
+    Args:
+        cterm1: `CTerm` to instantiate to `cterm2`.
+        cterm2: `CTerm` to instantiate `cterm1` to.
+
+    Returns:
+        A `CSubst` which can instantiate `cterm1` to `cterm2`, or `None` if no such `CSubst` exists.
+    """
+    # todo: delete this function and use cterm1.match_with_constraint(cterm2) directly after closing #4496
+    subst = cterm1.config.match(cterm2.config)
+    if subst is None:
+        return None
+    source_constraints = [subst(c) for c in cterm1.constraints]
+    constraints = [c for c in cterm2.constraints if c not in source_constraints]
+    return CSubst(subst, constraints)
+
+
 def anti_unify(state1: KInner, state2: KInner, kdef: KDefinition | None = None) -> tuple[KInner, Subst, Subst]:
     """Return a generalized state over the two input states.
 
@@ -333,8 +352,13 @@ 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)."""
-        _kast = self.subst(cterm.kast)
-        return CTerm(_kast, [self.constraint])
+        config = self.subst(cterm.config)
+        constraints = [self.subst(constraint) for constraint in cterm.constraints] + list(self.constraints)
+        return CTerm(config, constraints)
+
+    def __call__(self, cterm: CTerm) -> CTerm:
+        """Overload for `CSubst.apply`."""
+        return self.apply(cterm)
 
 
 def cterm_build_claim(

pyk/src/pyk/kcfg/kcfg.py

@@ -9,6 +9,8 @@
 from threading import RLock
 from typing import TYPE_CHECKING, Final, List, Union, cast, final
 
+from pyk.cterm.cterm import cterm_match
+
 from ..cterm import CSubst, CTerm, cterm_build_claim, cterm_build_rule
 from ..kast import EMPTY_ATT
 from ..kast.inner import KApply
@@ -1040,6 +1042,16 @@ def create_split(self, source_id: NodeIdLike, splits: Iterable[tuple[NodeIdLike,
         self.add_successor(split)
         return split
 
+    def create_split_by_nodes(self, source_id: NodeIdLike, target_ids: Iterable[NodeIdLike]) -> KCFG.Split | None:
+        """Create a split without crafting a CSubst."""
+        source = self.node(source_id)
+        targets = [self.node(nid) for nid in target_ids]
+        try:
+            csubsts = [not_none(cterm_match(source.cterm, target.cterm)) for target in targets]
+        except ValueError:
+            return None
+        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]:
         source_id = self._resolve(source_id) if source_id is not None else None
         target_id = self._resolve(target_id) if target_id is not None else None

pyk/src/tests/unit/test_cterm.py

@@ -5,15 +5,15 @@
 
 import pytest
 
-from pyk.cterm import CTerm, cterm_build_claim, cterm_build_rule
+from pyk.cterm import CSubst, CTerm, cterm_build_claim, cterm_build_rule
 from pyk.kast import Atts, KAtt
-from pyk.kast.inner import KApply, KLabel, KRewrite, KSequence, KSort, KVariable
+from pyk.kast.inner import KApply, KLabel, KRewrite, KSequence, KSort, KVariable, Subst
 from pyk.kast.outer import KClaim
 from pyk.prelude.k import GENERATED_TOP_CELL
 from pyk.prelude.kint import INT, intToken
 from pyk.prelude.ml import mlAnd, mlEqualsTrue
 
-from .utils import a, b, c, f, g, h, k, x, y, z
+from .utils import a, b, c, f, g, ge_ml, h, k, lt_ml, x, y, z
 
 if TYPE_CHECKING:
     from typing import Final
@@ -186,3 +186,41 @@ def test_from_kast(test_id: str, kast: KInner, expected: CTerm) -> None:
 
     # Then
     assert cterm == expected
+
+
+APPLY_TEST_DATA: Final = (
+    (CTerm.top(), CSubst(), CTerm.top()),
+    (CTerm.bottom(), CSubst(), CTerm.bottom()),
+    (
+        CTerm(k(KVariable('X'))),
+        CSubst(),
+        CTerm(k(KVariable('X'))),
+    ),
+    (
+        CTerm(k(KVariable('X'))),
+        CSubst(Subst({'X': intToken(5)})),
+        CTerm(k(intToken(5))),
+    ),
+    (
+        CTerm(k(KVariable('X'))),
+        CSubst(Subst({'X': KVariable('Y')})),
+        CTerm(k(KVariable('Y'))),
+    ),
+    (
+        CTerm(k(KVariable('X')), [lt_ml('X', 5)]),
+        CSubst(Subst({'X': KVariable('Y')}), [ge_ml('Y', 0)]),
+        CTerm(k(KVariable('Y')), [ge_ml('Y', 0), lt_ml('Y', 5)]),
+    ),
+)
+
+
+@pytest.mark.parametrize(
+    'term,subst,expected',
+    APPLY_TEST_DATA,
+)
+def test_csubst_apply(term: CTerm, subst: CSubst, expected: CTerm) -> None:
+    # When
+    actual = subst(term)
+
+    # Then
+    assert actual == expected

pyk/src/tests/unit/test_kcfg.py

@@ -1,8 +1,9 @@
 from __future__ import annotations
 
-from typing import TYPE_CHECKING
+from typing import TYPE_CHECKING, Final
 
 import pytest
+from unit.utils import ge_ml, k, lt_ml
 
 from pyk.cterm import CSubst, CTerm
 from pyk.kast.inner import KApply, KRewrite, KToken, KVariable, Subst
@@ -880,3 +881,96 @@ def test_no_cell_rewrite_to_dots() -> None:
 
     result = no_cell_rewrite_to_dots(term)
     assert result == term
+
+
+CREATE_SPLIT_BY_NODES_TEST_DATA: Final = (
+    (CTerm.bottom(), [CTerm.top(), CTerm.bottom()], None),
+    (CTerm.top(), [CTerm.top(), CTerm.bottom()], None),
+    (
+        CTerm.top(),
+        [CTerm(k(KVariable('X'))), CTerm(k(KVariable('Y')))],
+        None,  # todo: support split from top, because top means anything can be matched
+    ),
+    # not mutually exclusive
+    (
+        CTerm.top(),
+        [CTerm.top(), CTerm.top()],
+        KCFG.Split(
+            KCFG.Node(1, CTerm.top()), [(KCFG.Node(2, CTerm.top()), CSubst()), (KCFG.Node(3, CTerm.top()), CSubst())]
+        ),
+    ),
+    # not mutually exclusive
+    (
+        CTerm(k(KVariable('X'))),
+        [CTerm(k(KVariable('X'))), CTerm(k(KVariable('Y'))), CTerm(k(KVariable('Z')))],
+        KCFG.Split(
+            KCFG.Node(1, CTerm(k(KVariable('X')))),
+            [
+                (KCFG.Node(2, CTerm(k(KVariable('X')))), CSubst(Subst({'X': KVariable('X')}))),
+                (KCFG.Node(3, CTerm(k(KVariable('Y')))), CSubst(Subst({'X': KVariable('Y')}))),
+                (KCFG.Node(4, CTerm(k(KVariable('Z')))), CSubst(Subst({'X': KVariable('Z')}))),
+            ],
+        ),
+    ),
+    (CTerm(k(KVariable('X'))), [CTerm(k(KVariable('Y'))), CTerm(KApply('<bot>', [KVariable('Z')]))], None),
+    # not mutually exclusive
+    # this target doesn't meet the implication relationship with source.
+    # So the CTerm of target and CSubst.apply(target) are not logically equal.
+    # But source -> CSubst.apply(target) can always be true.
+    (
+        CTerm(k(KVariable('X')), [ge_ml('X', 0), lt_ml('X', 10)]),
+        [CTerm(k(KVariable('Y')), [ge_ml('Y', 0)]), CTerm(k(KVariable('Z')), [ge_ml('Z', 5)])],
+        KCFG.Split(
+            KCFG.Node(1, CTerm(k(KVariable('X')), [ge_ml('X', 0), lt_ml('X', 10)])),
+            [
+                (
+                    KCFG.Node(2, CTerm(k(KVariable('Y')), [ge_ml('Y', 0)])),
+                    CSubst(Subst({'X': KVariable('Y')}), []),
+                ),
+                (
+                    KCFG.Node(3, CTerm(k(KVariable('Z')), [ge_ml('Z', 5)])),
+                    CSubst(
+                        Subst({'X': KVariable('Z')}),
+                        [
+                            ge_ml('Z', 5),
+                        ],
+                    ),
+                ),
+            ],
+        ),
+    ),
+    (
+        CTerm(k(KVariable('X')), [ge_ml('X', 0), lt_ml('X', 10)]),
+        [
+            CTerm(k(KVariable('Y')), [ge_ml('Y', 0), lt_ml('Y', 5)]),
+            CTerm(k(KVariable('Z')), [ge_ml('Z', 5), lt_ml('Z', 10)]),
+        ],
+        KCFG.Split(
+            KCFG.Node(1, CTerm(k(KVariable('X')), [ge_ml('X', 0), lt_ml('X', 10)])),
+            [
+                (
+                    KCFG.Node(2, CTerm(k(KVariable('Y')), [ge_ml('Y', 0), lt_ml('Y', 5)])),
+                    CSubst(Subst({'X': KVariable('Y')}), [lt_ml('Y', 5)]),
+                ),
+                (
+                    KCFG.Node(3, CTerm(k(KVariable('Z')), [ge_ml('Z', 5), lt_ml('Z', 10)])),
+                    CSubst(Subst({'X': KVariable('Z')}), [ge_ml('Z', 5)]),
+                ),
+            ],
+        ),
+    ),
+)
+
+
+@pytest.mark.parametrize('source,targets,expected', CREATE_SPLIT_BY_NODES_TEST_DATA)
+def test_create_split_by_nodes(source: CTerm, targets: Iterable[CTerm], expected: KCFG.Split | None) -> None:
+    # Given
+    cfg = KCFG()
+    source_node = cfg.create_node(source)
+    target_nodes = [cfg.create_node(target) for target in targets]
+
+    # When
+    actual = cfg.create_split_by_nodes(source_node.id, [n.id for n in target_nodes])
+
+    # Then
+    assert actual == expected

pyk/src/tests/unit/utils.py

@@ -4,6 +4,8 @@
 from typing import TYPE_CHECKING
 
 from pyk.kast.inner import KApply, KLabel, KVariable
+from pyk.prelude.kint import geInt, intToken, ltInt
+from pyk.prelude.ml import mlEqualsTrue
 
 if TYPE_CHECKING:
     from typing import Final
@@ -16,3 +18,11 @@
 f, g, h = map(KLabel, ('f', 'g', 'h'))
 
 k = KLabel('<k>')
+
+
+def lt_ml(var: str, n: int) -> KApply:
+    return mlEqualsTrue(ltInt(KVariable(var), intToken(n)))
+
+
+def ge_ml(var: str, n: int) -> KApply:
+    return mlEqualsTrue(geInt(KVariable(var), intToken(n)))