diff --git a/pyk/src/pyk/prelude/ml.py b/pyk/src/pyk/prelude/ml.py index ab926469925..224c11fc7ea 100644 --- a/pyk/src/pyk/prelude/ml.py +++ b/pyk/src/pyk/prelude/ml.py @@ -5,7 +5,7 @@ from pyk.utils import single from ..kast.inner import KApply, KLabel, build_assoc, flatten_label -from .k import GENERATED_TOP_CELL, K_ITEM +from .k import GENERATED_TOP_CELL, K_ITEM, K from .kbool import BOOL, FALSE, TRUE if TYPE_CHECKING: @@ -55,7 +55,7 @@ def is_bottom(term: KInner, *, weak: bool = False) -> bool: def mlEquals( # noqa: N802 term1: KInner, term2: KInner, - arg_sort: str | KSort = GENERATED_TOP_CELL, + arg_sort: str | KSort = K, sort: str | KSort = GENERATED_TOP_CELL, ) -> KApply: return KLabel('#Equals', arg_sort, sort)(term1, term2) diff --git a/pyk/src/tests/integration/proof/test_imp.py b/pyk/src/tests/integration/proof/test_imp.py index 8acbcd60cc7..da4a8082006 100644 --- a/pyk/src/tests/integration/proof/test_imp.py +++ b/pyk/src/tests/integration/proof/test_imp.py @@ -12,7 +12,7 @@ from pyk.kast.manip import minimize_term, sort_ac_collections from pyk.kcfg.semantics import KCFGSemantics from pyk.kcfg.show import KCFGShow -from pyk.prelude.kbool import FALSE, andBool, orBool +from pyk.prelude.kbool import BOOL, FALSE, andBool, orBool from pyk.prelude.kint import intToken from pyk.prelude.ml import mlAnd, mlBottom, mlEquals, mlEqualsFalse, mlEqualsTrue, mlTop from pyk.proof import APRProver, ProofStatus @@ -700,7 +700,7 @@ def custom_step(self, c: CTerm) -> KCFGExtendResult | None: 'failing-if', 0, 1, - (mlEquals(KVariable('_B', 'Bool'), FALSE),), + (mlEquals(KVariable('_B', 'Bool'), FALSE, arg_sort=BOOL),), False, ), ( diff --git a/pyk/src/tests/unit/kast/test_subst.py b/pyk/src/tests/unit/kast/test_subst.py index 1ce2b11d2d6..fa5fd1c628c 100644 --- a/pyk/src/tests/unit/kast/test_subst.py +++ b/pyk/src/tests/unit/kast/test_subst.py @@ -8,7 +8,7 @@ from pyk.kast.inner import KApply, KLabel, KVariable, Subst from pyk.kast.manip import extract_subst from pyk.prelude.kbool import TRUE -from pyk.prelude.kint import intToken +from pyk.prelude.kint import INT, intToken from pyk.prelude.ml import mlAnd, mlEquals, mlEqualsTrue, mlOr, mlTop from ..utils import a, b, c, f, g, h, x, y, z @@ -131,14 +131,14 @@ def test_ml_pred(test_id: str, subst: Subst, pred: KInner) -> None: _EQ = KLabel('_==Int_') EXTRACT_SUBST_TEST_DATA: Final[tuple[tuple[KInner, dict[str, KInner], KInner], ...]] = ( (a, {}, a), - (mlEquals(a, b), {}, mlEquals(a, b)), - (mlEquals(x, a), {'x': a}, mlTop()), - (mlEquals(x, _0), {'x': _0}, mlTop()), - (mlEquals(x, y), {'x': y}, mlTop()), - (mlEquals(x, f(x)), {}, mlEquals(x, f(x))), - (mlAnd([mlEquals(x, y), mlEquals(x, b)]), {'x': y}, mlEquals(x, b)), - (mlAnd([mlEquals(x, b), mlEquals(x, y)]), {'x': b}, mlEquals(x, y)), - (mlAnd([mlEquals(a, b), mlEquals(x, a)]), {'x': a}, mlEquals(a, b)), + (mlEquals(a, b, arg_sort=INT), {}, mlEquals(a, b, arg_sort=INT)), + (mlEquals(x, a, arg_sort=INT), {'x': a}, mlTop()), + (mlEquals(x, _0, arg_sort=INT), {'x': _0}, mlTop()), + (mlEquals(x, y, arg_sort=INT), {'x': y}, mlTop()), + (mlEquals(x, f(x), arg_sort=INT), {}, mlEquals(x, f(x), arg_sort=INT)), + (mlAnd([mlEquals(x, y, arg_sort=INT), mlEquals(x, b, arg_sort=INT)]), {'x': y}, mlEquals(x, b, arg_sort=INT)), + (mlAnd([mlEquals(x, b, arg_sort=INT), mlEquals(x, y, arg_sort=INT)]), {'x': b}, mlEquals(x, y, arg_sort=INT)), + (mlAnd([mlEquals(a, b, arg_sort=INT), mlEquals(x, a, arg_sort=INT)]), {'x': a}, mlEquals(a, b, arg_sort=INT)), (mlEqualsTrue(_EQ(a, b)), {}, mlEqualsTrue(_EQ(a, b))), (mlEqualsTrue(_EQ(x, a)), {'x': a}, mlTop()), ) @@ -161,7 +161,7 @@ def test_propagate_subst() -> None: bar_x = KApply('bar', [x]) config = KApply('', [bar_x]) - subst_conjunct = mlEquals(v1, bar_x) + subst_conjunct = mlEquals(v1, bar_x, arg_sort=INT) other_conjunct = mlEqualsTrue(KApply('_<=Int_', [v1, KApply('foo', [x, bar_x])])) term = mlAnd([config, subst_conjunct, other_conjunct]) @@ -184,8 +184,8 @@ def test_propagate_subst() -> None: 'positive', mlAnd( [ - mlEquals(KVariable('X'), intToken(1)), - mlEquals(KVariable('Y'), intToken(2)), + mlEquals(KVariable('X'), intToken(1), arg_sort=INT), + mlEquals(KVariable('Y'), intToken(2), arg_sort=INT), ] ), Subst({'X': intToken(1), 'Y': intToken(2)}), @@ -194,8 +194,8 @@ def test_propagate_subst() -> None: 'wrong-connective', mlOr( [ - mlEquals(KVariable('X'), intToken(1)), - mlEquals(KVariable('Y'), intToken(2)), + mlEquals(KVariable('X'), intToken(1), arg_sort=INT), + mlEquals(KVariable('Y'), intToken(2), arg_sort=INT), ] ), None, @@ -204,8 +204,8 @@ def test_propagate_subst() -> None: 'not-subst', mlAnd( [ - mlEquals(KVariable('X'), intToken(1)), - mlEquals(KVariable('Y'), intToken(2)), + mlEquals(KVariable('X'), intToken(1), arg_sort=INT), + mlEquals(KVariable('Y'), intToken(2), arg_sort=INT), mlEqualsTrue(KApply('_==K_', [KVariable('Y'), intToken(2)])), ] ), diff --git a/pyk/src/tests/unit/test_kcfg.py b/pyk/src/tests/unit/test_kcfg.py index a2ab05b69d6..fc5958f44fe 100644 --- a/pyk/src/tests/unit/test_kcfg.py +++ b/pyk/src/tests/unit/test_kcfg.py @@ -10,6 +10,7 @@ from pyk.kcfg import KCFG, KCFGShow from pyk.kcfg.kcfg import KCFGNodeAttr from pyk.kcfg.show import NodePrinter +from pyk.prelude.kint import INT from pyk.prelude.ml import mlEquals, mlTop from pyk.prelude.utils import token from pyk.utils import not_none, single @@ -41,7 +42,7 @@ def to_csubst_id(source_id: int, target_id: int, constraints: Iterable[KInner]) def x_equals(i: int) -> KInner: - return mlEquals(KVariable('X'), token(i)) + return mlEquals(KVariable('X'), token(i), arg_sort=INT) def x_config() -> KInner: