Merge CTerm

pyk/src/pyk/cterm/cterm.py

@@ -6,7 +6,7 @@
 from typing import TYPE_CHECKING
 
 from ..kast import KInner
-from ..kast.inner import KApply, KRewrite, KToken, Subst, bottom_up
+from ..kast.inner import KApply, KRewrite, KToken, KVariable, Subst, bottom_up, var_occurrences
 from ..kast.manip import (
     abstract_term_safely,
     build_claim,
@@ -21,8 +21,8 @@
     split_config_from,
 )
 from ..prelude.k import GENERATED_TOP_CELL
-from ..prelude.kbool import andBool, orBool
-from ..prelude.ml import is_bottom, is_top, mlAnd, mlBottom, mlEqualsTrue, mlImplies, mlTop
+from ..prelude.kbool import TRUE, andBool, orBool
+from ..prelude.ml import is_bottom, is_top, mlAnd, mlBottom, mlEquals, mlEqualsTrue, mlImplies, mlTop
 from ..utils import unique
 
 if TYPE_CHECKING:
@@ -253,6 +253,48 @@ def remove_useless_constraints(self, keep_vars: Iterable[str] = ()) -> CTerm:
         return CTerm(self.config, new_constraints)
 
 
+def merge_cterms(t1: CTerm, t2: CTerm) -> CTerm | None:
+    """Return a `CTerm` which is the merge of the two input `CTerm` instances.
+
+    Args:
+        t1: First `CTerm` to merge.
+        t2: Second `CTerm` to merge.
+
+    Returns:
+        A `CTerm` which is the merge of the two input `CTerm` instances.
+    """
+    # check all cells in t1 and t1, if they are the same, keep them, otherwise, create a new free variable for them
+    t1_config, t1_subst = split_config_from(t1.config)
+    t2_config, t2_subst = split_config_from(t2.config)
+
+    if t1_config != t2_config:
+        # cannot merge two configurations with different structure
+        return None
+
+    new_subst: Subst = Subst({})
+    new_t1_subst = Subst({})
+    new_t2_subst = Subst({})
+
+    for cell in t1_subst:
+        if t1_subst[cell] == t2_subst[cell] and not var_occurrences(t1_subst[cell]):
+            # keep the cell if it is the same & exists no free variables
+            new_subst = new_subst * Subst({cell: t1_subst[cell]})
+        else:
+            # create a new free variable for the cell
+            new_t1_subst = new_t1_subst * Subst({cell: t1_subst[cell]})
+            new_t2_subst = new_t2_subst * Subst({cell: t2_subst[cell]})
+    new_config = new_subst(t1_config)
+
+    new_constraints: list[KInner] = []
+    for new_subst, t in [(new_t1_subst, t1), (new_t2_subst, t2)]:
+        if new_subst:
+            antecedent = mlAnd([mlEquals(KVariable(cell), new_subst[cell]) for cell in new_subst])
+            consequent = mlAnd(t.constraints) if t.constraints else TRUE
+            new_constraints.append(mlImplies(antecedent, consequent))
+
+    return CTerm(new_config, new_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.
 

pyk/src/tests/unit/test_cterm.py

@@ -6,14 +6,16 @@
 import pytest
 
 from pyk.cterm import CTerm, cterm_build_claim, cterm_build_rule
+from pyk.cterm.cterm import merge_cterms
 from pyk.kast import Atts, KAtt
 from pyk.kast.inner import KApply, KLabel, KRewrite, KSequence, KSort, KVariable
 from pyk.kast.outer import KClaim
 from pyk.prelude.k import GENERATED_TOP_CELL
+from pyk.prelude.kbool import TRUE
 from pyk.prelude.kint import INT, intToken
-from pyk.prelude.ml import mlAnd, mlEqualsTrue
+from pyk.prelude.ml import mlAnd, mlEquals, mlEqualsTrue, mlImplies
 
-from .utils import a, b, c, f, g, h, k, x, y, z
+from .utils import a, b, c, config, config_int, f, g, ge, h, k, lt, x, y, z
 
 if TYPE_CHECKING:
     from typing import Final
@@ -186,3 +188,104 @@ def test_from_kast(test_id: str, kast: KInner, expected: CTerm) -> None:
 
     # Then
     assert cterm == expected
+
+
+MERGE_TEST_DATA: Final = (
+    (CTerm.top(), CTerm.top(), CTerm.top()),
+    (CTerm.bottom(), CTerm.top(), None),
+    (CTerm(config_int(1)), CTerm(config_int(1)), CTerm(config_int(1))),
+    (
+        CTerm(config('X')),
+        CTerm(config('X')),
+        CTerm(config('TOP_CELL'), [mlImplies(mlEquals(KVariable('TOP_CELL'), KVariable('X')), TRUE)]),
+    ),
+    (
+        CTerm(config('X')),
+        CTerm(config('Y')),
+        CTerm(
+            config('TOP_CELL'),
+            [
+                mlImplies(mlEquals(KVariable('TOP_CELL'), KVariable('X')), TRUE),
+                mlImplies(mlEquals(KVariable('TOP_CELL'), KVariable('Y')), TRUE),
+            ],
+        ),
+    ),
+    (
+        CTerm(config_int(1)),
+        CTerm(config_int(2)),
+        CTerm(
+            config('TOP_CELL'),
+            [
+                mlImplies(mlEquals(KVariable('TOP_CELL'), intToken(1)), TRUE),
+                mlImplies(mlEquals(KVariable('TOP_CELL'), intToken(2)), TRUE),
+            ],
+        ),
+    ),
+    (
+        CTerm(
+            config('X'),
+            [ge('X', 0)],
+        ),
+        CTerm(
+            config('X'),
+            [ge('X', 0)],
+        ),
+        CTerm(
+            config('TOP_CELL'),
+            [
+                mlImplies(mlEquals(KVariable('TOP_CELL'), KVariable('X')), ge('X', 0)),
+            ],
+        ),
+    ),
+    (
+        CTerm(
+            config('X'),
+            [ge('X', 0), lt('X', 3)],
+        ),
+        CTerm(
+            config('X'),
+            [ge('X', 0), lt('X', 5)],
+        ),
+        CTerm(
+            config('TOP_CELL'),
+            [
+                mlImplies(mlEquals(KVariable('TOP_CELL'), KVariable('X')), mlAnd([lt('X', 3), ge('X', 0)])),
+                mlImplies(
+                    mlEquals(KVariable('TOP_CELL'), KVariable('X')),
+                    mlAnd(
+                        [
+                            lt('X', 5),
+                            ge('X', 0),
+                        ]
+                    ),
+                ),
+            ],
+        ),
+    ),
+    (
+        CTerm(
+            config('X'),
+            [ge('X', 0), lt('X', 3)],
+        ),
+        CTerm(
+            config('Y'),
+            [ge('Y', 0), lt('Y', 5)],
+        ),
+        CTerm(
+            config('TOP_CELL'),
+            [
+                mlImplies(mlEquals(KVariable('TOP_CELL'), KVariable('X')), mlAnd([lt('X', 3), ge('X', 0)])),
+                mlImplies(mlEquals(KVariable('TOP_CELL'), KVariable('Y')), mlAnd([lt('Y', 5), ge('Y', 0)])),
+            ],
+        ),
+    ),
+)
+
+
+@pytest.mark.parametrize('t1,t2,expected', MERGE_TEST_DATA, ids=count())
+def test_cterm_merge(t1: CTerm, t2: CTerm, expected: CTerm) -> None:
+    # When
+    merged = merge_cterms(t1, t2)
+
+    # Then
+    assert merged == 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,19 @@
 f, g, h = map(KLabel, ('f', 'g', 'h'))
 
 k = KLabel('<k>')
+
+
+def lt(var: str, n: int) -> KApply:
+    return mlEqualsTrue(ltInt(KVariable(var), intToken(n)))
+
+
+def ge(var: str, n: int) -> KApply:
+    return mlEqualsTrue(geInt(KVariable(var), intToken(n)))
+
+
+def config(var: str) -> KApply:
+    return KApply('<top>', KVariable(var))
+
+
+def config_int(n: int) -> KApply:
+    return KApply('<top>', intToken(n))