Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Adjust the sort of mlEquals #4633

Merged
merged 4 commits into from
Sep 6, 2024
Merged

Adjust the sort of mlEquals #4633

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
95c02af
pyk/prelude/ml: remove default setting of arg_sort for mlEquals
ehildenb Sep 5, 2024
7577443
pyk/prelude/ml: sort K as default argument sort for mlEquals
ehildenb Sep 5, 2024
18c334a
pyk/tests/test_subst: fix merge conflict typo
ehildenb Sep 6, 2024
74a4626
Merge branch 'develop' into ml-equals-sort
ehildenb Sep 6, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions pyk/src/pyk/prelude/ml.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -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)
Expand Down
4 changes: 2 additions & 2 deletions pyk/src/tests/integration/proof/test_imp.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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,
),
(
Expand Down
32 changes: 16 additions & 16 deletions pyk/src/tests/unit/kast/test_subst.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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()),
)
Expand All @@ -161,7 +161,7 @@ def test_propagate_subst() -> None:
bar_x = KApply('bar', [x])
config = KApply('<k>', [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])
Expand All @@ -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)}),
Expand All @@ -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,
Expand All @@ -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)])),
]
),
Expand Down
3 changes: 2 additions & 1 deletion pyk/src/tests/unit/test_kcfg.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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:
Expand Down
Loading