Expose pattern simplification from KLLVM bindings (#736)

~Blocked on
runtimeverification/llvm-backend#897
~Blocked on
runtimeverification/llvm-backend#910

Adds runtime methods `simplify` and `simplify_bool`.

---------

Co-authored-by: devops <devops@runtimeverification.com>

pyk/package/version

@@ -1 +1 @@
-0.1.522
+0.1.523

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. <contact@runtimeverification.com>",

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

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

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: