From 95c02af5b83461478f2b9647f2a6ff2bac495541 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 5 Sep 2024 15:43:03 +0000 Subject: [PATCH 1/3] pyk/prelude/ml: remove default setting of arg_sort for mlEquals --- pyk/src/pyk/prelude/ml.py | 2 +- pyk/src/tests/integration/proof/test_imp.py | 4 +-- pyk/src/tests/unit/kast/test_subst.py | 32 ++++++++++----------- pyk/src/tests/unit/test_kcfg.py | 3 +- 4 files changed, 21 insertions(+), 20 deletions(-) diff --git a/pyk/src/pyk/prelude/ml.py b/pyk/src/pyk/prelude/ml.py index ab926469925..acd2558cf70 100644 --- a/pyk/src/pyk/prelude/ml.py +++ b/pyk/src/pyk/prelude/ml.py @@ -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, 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..4a564695fb4 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 9ba68366a07..2e401f13d4e 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: From 7577443d6314ca9b84f5403eded73fa41c245767 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 5 Sep 2024 21:05:40 +0000 Subject: [PATCH 2/3] pyk/prelude/ml: sort K as default argument sort for mlEquals --- pyk/src/pyk/prelude/ml.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/prelude/ml.py b/pyk/src/pyk/prelude/ml.py index acd2558cf70..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, + arg_sort: str | KSort = K, sort: str | KSort = GENERATED_TOP_CELL, ) -> KApply: return KLabel('#Equals', arg_sort, sort)(term1, term2) From 18c334a10bdf2f513c3eba72ace3d5e72beb598e Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 6 Sep 2024 15:19:25 +0000 Subject: [PATCH 3/3] pyk/tests/test_subst: fix merge conflict typo --- pyk/src/tests/unit/kast/test_subst.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/tests/unit/kast/test_subst.py b/pyk/src/tests/unit/kast/test_subst.py index 4a564695fb4..fa5fd1c628c 100644 --- a/pyk/src/tests/unit/kast/test_subst.py +++ b/pyk/src/tests/unit/kast/test_subst.py @@ -135,7 +135,7 @@ def test_ml_pred(test_id: str, subst: Subst, pred: KInner) -> None: (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))), + (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)),