Add least_common_supersort(), use in sort(), use sort() in anti_unify, move anti_unify to KDefinition

Author: nwatson22

src/pyk/kast/manip.py

@@ -6,7 +6,7 @@
 
 from ..prelude.k import DOTS, GENERATED_TOP_CELL
 from ..prelude.kbool import FALSE, TRUE, andBool, impliesBool, notBool, orBool
-from ..prelude.ml import mlAnd, mlEqualsTrue, mlImplies, mlOr, mlTop
+from ..prelude.ml import mlAnd, mlEqualsTrue, mlOr
 from ..utils import find_common_items, hash_str
 from .inner import KApply, KRewrite, KSequence, KToken, KVariable, Subst, bottom_up, top_down, var_occurrences
 from .kast import EMPTY_ATT, KAtt, WithKAtt
@@ -582,58 +582,6 @@ def _abstract(k: KInner) -> KVariable:
     return new_var
 
 
-def anti_unify(state1: KInner, state2: KInner) -> tuple[KInner, Subst, Subst]:
-    def _rewrites_to_abstractions(_kast: KInner) -> KInner:
-        if type(_kast) is KRewrite:
-            return abstract_term_safely(_kast)
-        return _kast
-
-    minimized_rewrite = push_down_rewrites(KRewrite(state1, state2))
-    abstracted_state = bottom_up(_rewrites_to_abstractions, minimized_rewrite)
-    subst1 = abstracted_state.match(state1)
-    subst2 = abstracted_state.match(state2)
-    if subst1 is None or subst2 is None:
-        raise ValueError('Anti-unification failed to produce a more general state!')
-    return (abstracted_state, subst1, subst2)
-
-
-def anti_unify_with_constraints(
-    constrained_term_1: KInner,
-    constrained_term_2: KInner,
-    implications: bool = False,
-    constraint_disjunct: bool = False,
-    abstracted_disjunct: bool = False,
-) -> KInner:
-    def disjunction_from_substs(subst1: Subst, subst2: Subst) -> KInner:
-        if KToken('true', 'Bool') in [subst1.pred, subst2.pred]:
-            return mlTop()
-        return mlEqualsTrue(orBool([subst1.pred, subst2.pred]))
-
-    state1, constraint1 = split_config_and_constraints(constrained_term_1)
-    state2, constraint2 = split_config_and_constraints(constrained_term_2)
-    constraints1 = flatten_label('#And', constraint1)
-    constraints2 = flatten_label('#And', constraint2)
-    state, subst1, subst2 = anti_unify(state1, state2)
-
-    constraints = [c for c in constraints1 if c in constraints2]
-    constraint1 = mlAnd([c for c in constraints1 if c not in constraints])
-    constraint2 = mlAnd([c for c in constraints2 if c not in constraints])
-    implication1 = mlImplies(constraint1, subst1.ml_pred)
-    implication2 = mlImplies(constraint2, subst2.ml_pred)
-
-    if abstracted_disjunct:
-        constraints.append(disjunction_from_substs(subst1, subst2))
-
-    if implications:
-        constraints.append(implication1)
-        constraints.append(implication2)
-
-    if constraint_disjunct:
-        constraints.append(mlOr([constraint1, constraint2]))
-
-    return mlAnd([state] + constraints)
-
-
 def apply_existential_substitutions(constrained_term: KInner) -> KInner:
     state, constraint = split_config_and_constraints(constrained_term)
     constraints = flatten_label('#And', constraint)

src/pyk/kast/outer.py

@@ -10,8 +10,8 @@
 from functools import cached_property
 from typing import TYPE_CHECKING, final
 
-from ..prelude.kbool import TRUE
-from ..prelude.ml import ML_QUANTIFIERS
+from ..prelude.kbool import TRUE, orBool
+from ..prelude.ml import ML_QUANTIFIERS, mlAnd, mlEqualsTrue, mlImplies, mlOr, mlTop
 from ..utils import filter_none, single, unique
 from .inner import (
     KApply,
@@ -35,6 +35,8 @@
     from os import PathLike
     from typing import Any, Final, TypeVar
 
+    from ..cterm import CTerm
+
     RL = TypeVar('RL', bound='KRuleLike')
 
 _LOGGER: Final = logging.getLogger(__name__)
@@ -1057,6 +1059,61 @@ def production_for_klabel(self, klabel: KLabel) -> KProduction:
                 raise ValueError(f'Expected a single production for label {klabel}, not: {prods}') from err
         return self._production_for_klabel[klabel]
 
+    def anti_unify(self, state1: KInner, state2: KInner) -> tuple[KInner, Subst, Subst]:
+        from .manip import abstract_term_safely, push_down_rewrites
+
+        def _rewrites_to_abstractions(_kast: KInner) -> KInner:
+            if type(_kast) is KRewrite:
+                return abstract_term_safely(_kast, sort=self.sort(_kast))
+            return _kast
+
+        minimized_rewrite = push_down_rewrites(KRewrite(state1, state2))
+        abstracted_state = bottom_up(_rewrites_to_abstractions, minimized_rewrite)
+        subst1 = abstracted_state.match(state1)
+        subst2 = abstracted_state.match(state2)
+        if subst1 is None or subst2 is None:
+            raise ValueError('Anti-unification failed to produce a more general state!')
+        return (abstracted_state, subst1, subst2)
+
+    def anti_unify_with_constraints(
+        self,
+        constrained_term_1: CTerm,
+        constrained_term_2: CTerm,
+        implications: bool = False,
+        constraint_disjunct: bool = False,
+        abstracted_disjunct: bool = False,
+    ) -> KInner:
+        from .manip import flatten_label, split_config_and_constraints
+
+        def disjunction_from_substs(subst1: Subst, subst2: Subst) -> KInner:
+            if KToken('true', 'Bool') in [subst1.pred, subst2.pred]:
+                return mlTop()
+            return mlEqualsTrue(orBool([subst1.pred, subst2.pred]))
+
+        state1, constraint1 = split_config_and_constraints(constrained_term_1.kast)
+        state2, constraint2 = split_config_and_constraints(constrained_term_2.kast)
+        constraints1 = flatten_label('#And', constraint1)
+        constraints2 = flatten_label('#And', constraint2)
+        state, subst1, subst2 = self.anti_unify(state1, state2)
+
+        constraints = [c for c in constraints1 if c in constraints2]
+        constraint1 = mlAnd([c for c in constraints1 if c not in constraints])
+        constraint2 = mlAnd([c for c in constraints2 if c not in constraints])
+        implication1 = mlImplies(constraint1, subst1.ml_pred)
+        implication2 = mlImplies(constraint2, subst2.ml_pred)
+
+        if abstracted_disjunct:
+            constraints.append(disjunction_from_substs(subst1, subst2))
+
+        if implications:
+            constraints.append(implication1)
+            constraints.append(implication2)
+
+        if constraint_disjunct:
+            constraints.append(mlOr([constraint1, constraint2]))
+
+        return mlAnd([state] + constraints)
+
     def production_for_cell_sort(self, sort: KSort) -> KProduction:
         # Typical cell production has 3 productions:
         #     syntax KCell ::= "project:KCell" "(" K ")" [function, projection]
@@ -1101,8 +1158,11 @@ def sort(self, kast: KInner) -> KSort | None:
             case KToken(_, sort) | KVariable(_, sort):
                 return sort
             case KRewrite(lhs, rhs):
-                sort = self.sort(lhs)
-                return sort if sort == self.sort(rhs) else None
+                lhs_sort = self.sort(lhs)
+                rhs_sort = self.sort(rhs)
+                if lhs_sort and rhs_sort:
+                    return self.least_common_supersort(lhs_sort, rhs_sort)
+                return None
             case KSequence(_):
                 return KSort('K')
             case KApply(label, _):
@@ -1128,6 +1188,15 @@ def sort_strict(self, kast: KInner) -> KSort:
             raise ValueError(f'Could not determine sort of term: {kast}')
         return sort
 
+    def least_common_supersort(self, sort1: KSort, sort2: KSort) -> KSort | None:
+        if sort1 == sort2:
+            return sort1
+        if sort1 in self.subsorts(sort2):
+            return sort2
+        if sort2 in self.subsorts(sort1):
+            return sort1
+        return None
+
     def greatest_common_subsort(self, sort1: KSort, sort2: KSort) -> KSort | None:
         if sort1 == sort2:
             return sort1

src/tests/integration/kcfg/test_imp.py

@@ -8,10 +8,10 @@
 
 from pyk.cterm import CSubst, CTerm
 from pyk.kast.inner import KApply, KSequence, KSort, KToken, KVariable, Subst
-from pyk.kast.manip import minimize_term
+from pyk.kast.manip import get_cell, minimize_term
 from pyk.kcfg.semantics import KCFGSemantics
 from pyk.kcfg.show import KCFGShow
-from pyk.prelude.kbool import BOOL, notBool
+from pyk.prelude.kbool import BOOL, notBool, orBool
 from pyk.prelude.kint import intToken
 from pyk.prelude.ml import mlAnd, mlBottom, mlEqualsFalse, mlEqualsTrue, mlTop
 from pyk.proof import APRBMCProof, APRBMCProver, APRProof, APRProver, ProofStatus
@@ -1147,3 +1147,70 @@ def test_fail_fast(
         assert len(proof.pending) == 1
         assert len(proof.terminal) == 1
         assert len(proof.failing) == 1
+
+    def test_anti_unify_with_constraints(
+        self,
+        kprint: KPrint,
+    ) -> None:
+        cterm1 = self.config(
+            kprint=kprint,
+            k='int $n ; { }',
+            state='$s |-> 0',
+            constraint=KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]),
+        )
+        cterm2 = self.config(
+            kprint=kprint,
+            k='int $n ; { }',
+            state='$s |-> 1',
+            constraint=KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]),
+        )
+
+        anti_unifier = kprint.definition.anti_unify_with_constraints(cterm1, cterm2, abstracted_disjunct=True)
+
+        k_cell = get_cell(anti_unifier, 'STATE_CELL')
+        assert type(k_cell) is KApply
+        assert k_cell.label.name == '_|->_'
+        assert type(k_cell.args[1]) is KVariable
+        abstracted_var: KVariable = k_cell.args[1]
+
+        expected_anti_unifier = self.config(
+            kprint=kprint,
+            k='int $n ; { }',
+            state=f'$s |-> {abstracted_var.name}:Int',
+            constraint=mlAnd(
+                [
+                    KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]),
+                    mlEqualsTrue(
+                        orBool(
+                            [
+                                KApply('_==K_', [KVariable(name=abstracted_var.name), intToken(0)]),
+                                KApply('_==K_', [KVariable(name=abstracted_var.name), intToken(1)]),
+                            ]
+                        )
+                    ),
+                ]
+            ),
+        ).kast
+
+        assert anti_unifier == expected_anti_unifier
+
+    def test_anti_unify_with_constraints_subst_true(
+        self,
+        kprint: KPrint,
+    ) -> None:
+        cterm1 = self.config(
+            kprint=kprint,
+            k='int $n ; { }',
+            state='$s |-> 0',
+            constraint=KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]),
+        )
+        cterm2 = self.config(
+            kprint=kprint,
+            k='int $n ; { }',
+            state='$s |-> 0',
+            constraint=KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]),
+        )
+
+        anti_unifier = kprint.definition.anti_unify_with_constraints(cterm1, cterm2, abstracted_disjunct=True)
+
+        assert anti_unifier == cterm1.kast

src/tests/unit/kast/test_manip.py

@@ -5,9 +5,8 @@
 
 import pytest
 
-from pyk.kast.inner import KApply, KLabel, KRewrite, KSequence, KSort, KToken, KVariable, Subst
+from pyk.kast.inner import KApply, KLabel, KRewrite, KSequence, KSort, KVariable, Subst
 from pyk.kast.manip import (
-    anti_unify_with_constraints,
     bool_to_ml_pred,
     collapse_dots,
     minimize_term,
@@ -16,13 +15,12 @@
     remove_generated_cells,
     rename_generated_vars,
     simplify_bool,
-    split_config_and_constraints,
     split_config_from,
 )
 from pyk.prelude.k import DOTS, GENERATED_TOP_CELL
-from pyk.prelude.kbool import BOOL, FALSE, TRUE, andBool, notBool, orBool
+from pyk.prelude.kbool import BOOL, FALSE, TRUE, andBool, notBool
 from pyk.prelude.kint import INT, intToken
-from pyk.prelude.ml import mlAnd, mlEqualsTrue, mlTop
+from pyk.prelude.ml import mlEqualsTrue, mlTop
 
 from ..utils import a, b, c, f, k, x
 
@@ -341,94 +339,3 @@ def test_split_config_from(term: KInner, expected_config: KInner, expected_subst
     # Then
     assert actual_config == expected_config
     assert actual_subst == expected_subst
-
-
-def test_anti_unify_with_constraints() -> None:
-    cterm1 = mlAnd(
-        [
-            KApply(
-                '<generatedTop>',
-                [
-                    KApply('<k>', KToken('1', 'Int')),
-                    KApply('<generatedCounter>', KVariable('GENERATEDCOUNTER_CELL')),
-                ],
-            ),
-            mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])),
-        ]
-    )
-    cterm2 = mlAnd(
-        [
-            KApply(
-                '<generatedTop>',
-                [
-                    KApply('<k>', KToken('2', 'Int')),
-                    KApply('<generatedCounter>', KVariable('GENERATEDCOUNTER_CELL')),
-                ],
-            ),
-            mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])),
-        ]
-    )
-
-    anti_unifier = anti_unify_with_constraints(cterm1, cterm2, abstracted_disjunct=True)
-
-    config, constraints = split_config_and_constraints(anti_unifier)
-
-    assert type(config) is KApply
-    assert type(config.args[0]) is KApply
-    assert type(config.args[0].args[0]) is KVariable
-    var_name = config.args[0].args[0].name
-
-    expected = mlAnd(
-        [
-            mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])),
-            mlEqualsTrue(
-                orBool(
-                    [
-                        KApply('_==K_', [KVariable(var_name), KToken('1', 'Int')]),
-                        KApply('_==K_', [KVariable(var_name), KToken('2', 'Int')]),
-                    ]
-                )
-            ),
-        ]
-    )
-
-    assert expected == constraints
-
-
-def test_anti_unify_with_constraints_subst_true() -> None:
-    cterm1 = mlAnd(
-        [
-            KApply(
-                '<generatedTop>',
-                [
-                    KApply('<k>', KToken('1', 'Int')),
-                    KApply('<generatedCounter>', KVariable('GENERATEDCOUNTER_CELL')),
-                ],
-            ),
-            mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])),
-        ]
-    )
-    cterm2 = mlAnd(
-        [
-            KApply(
-                '<generatedTop>',
-                [
-                    KApply('<k>', KToken('1', 'Int')),
-                    KApply('<generatedCounter>', KVariable('GENERATEDCOUNTER_CELL')),
-                ],
-            ),
-            mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])),
-        ]
-    )
-
-    anti_unifier = anti_unify_with_constraints(cterm1, cterm2, abstracted_disjunct=True)
-
-    config, constraints = split_config_and_constraints(anti_unifier)
-
-    expected = mlAnd(
-        [
-            mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])),
-        ]
-    )
-
-    assert expected == constraints