diff --git a/pyk/package/version b/pyk/package/version index 72f33e90694..6db6ec0231c 100644 --- a/pyk/package/version +++ b/pyk/package/version @@ -1 +1 @@ -0.1.522 +0.1.523 diff --git a/pyk/pyproject.toml b/pyk/pyproject.toml index 3054f4eaad8..88eb5e109dd 100644 --- a/pyk/pyproject.toml +++ b/pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.522" +version = "0.1.523" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/pyk/src/pyk/kllvm/runtime.py b/pyk/src/pyk/kllvm/runtime.py index a46b2b0879c..e22a24750c5 100644 --- a/pyk/src/pyk/kllvm/runtime.py +++ b/pyk/src/pyk/kllvm/runtime.py @@ -6,7 +6,7 @@ from types import ModuleType from typing import Any - from .ast import Pattern + from .ast import Pattern, Sort class Runtime: @@ -32,6 +32,12 @@ def step(self, pattern: Pattern, depth: int | None = 1) -> Pattern: def run(self, pattern: Pattern) -> Pattern: return self.step(pattern, depth=None) + def simplify(self, pattern: Pattern, sort: Sort) -> Pattern: + return self._module.simplify_pattern(pattern, sort) + + def simplify_bool(self, pattern: Pattern) -> bool: + return self._module.simplify_bool_pattern(pattern) + class Term: _block: Any # module.InternalTerm diff --git a/pyk/src/tests/integration/kllvm/test_simplify.py b/pyk/src/tests/integration/kllvm/test_simplify.py new file mode 100644 index 00000000000..865d640db6a --- /dev/null +++ b/pyk/src/tests/integration/kllvm/test_simplify.py @@ -0,0 +1,66 @@ +from __future__ import annotations + +from typing import TYPE_CHECKING + +import pytest + +import pyk.kllvm.load # noqa: F401 +from pyk.kllvm import parser +from pyk.testing import RuntimeTest + +from ..utils import K_FILES + +if TYPE_CHECKING: + from pyk.kllvm.runtime import Runtime + + +SIMPLIFY_TEST_DATA = ( + ('literal', r'\dv{SortInt{}}("0")', r'inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("0"))'), + ( + 'plus', + r"""Lbl'UndsPlus'Int'Unds'{}(\dv{SortInt{}}("1"), \dv{SortInt{}}("2"))""", + r'inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3"))', + ), +) + +SIMPLIFY_BOOL_TEST_DATA = ( + ('true', r'\dv{SortBool{}}("true")', True), + ('false', r'\dv{SortBool{}}("false")', False), + ('true andBool false', r"""Lbl'Unds'andBool'Unds'{}(\dv{SortBool{}}("true"), \dv{SortBool{}}("false"))""", False), + ('false orBool true', r"""Lbl'Unds'orBool'Unds'{}(\dv{SortBool{}}("false"), \dv{SortBool{}}("true"))""", True), +) + + +class TestSimplify(RuntimeTest): + KOMPILE_MAIN_FILE = K_FILES / 'imp.k' + + @pytest.mark.parametrize( + 'test_id,pattern_text,expected', + SIMPLIFY_TEST_DATA, + ids=[test_id for test_id, *_ in SIMPLIFY_TEST_DATA], + ) + def test_simplify(self, runtime: Runtime, test_id: str, pattern_text: str, expected: str) -> None: + # Given + pattern = parser.parse_pattern(pattern_text) + sort = parser.parse_sort('SortInt{}') + + # When + simplified = runtime.simplify(pattern, sort) + + # Then + assert str(simplified) == expected + + @pytest.mark.parametrize( + 'test_id,pattern_text,expected', + SIMPLIFY_BOOL_TEST_DATA, + ids=[test_id for test_id, *_ in SIMPLIFY_BOOL_TEST_DATA], + ) + def test_simplify_bool(self, runtime: Runtime, test_id: str, pattern_text: str, expected: bool) -> None: + # Given + pattern = parser.parse_pattern(pattern_text) + + # When + actual = runtime.simplify_bool(pattern) + + # Then + assert actual == expected diff --git a/pyk/src/tests/integration/kllvm/test_step.py b/pyk/src/tests/integration/kllvm/test_step.py index aff3718a67f..2415f261071 100644 --- a/pyk/src/tests/integration/kllvm/test_step.py +++ b/pyk/src/tests/integration/kllvm/test_step.py @@ -3,7 +3,7 @@ from typing import TYPE_CHECKING import pyk.kllvm.load # noqa: F401 -from pyk.kllvm.parser import Parser +from pyk.kllvm.parser import parse_pattern from pyk.testing import RuntimeTest from ..utils import K_FILES @@ -65,7 +65,7 @@ def start_pattern() -> Pattern: ) ) """ - return Parser.from_string(text).pattern() + return parse_pattern(text) def foo_output(n: int) -> str: