Merge branch 'master' into petar/constraint-order

deps/k_release

@@ -1 +1 @@
-6.3.75
+6.3.77

docs/conf.py

@@ -9,8 +9,8 @@
 project = 'pyk'
 author = 'Runtime Verification, Inc'
 copyright = '2024, Runtime Verification, Inc'
-version = '0.1.778'
-release = '0.1.778'
+version = '0.1.779'
+release = '0.1.779'
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

package/version

@@ -1 +1 @@
-0.1.778
+0.1.779

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.778"
+version = "0.1.779"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-K_VERSION: Final = '6.3.75'
+K_VERSION: Final = '6.3.77'

src/pyk/konvert/_module_to_kore.py

@@ -722,20 +722,27 @@ def simplified_module(definition: KDefinition, module_name: str | None = None) -
         PullUpRewrites(),
         DiscardSymbolAtts(
             [
+                Atts.ASSOC,
                 Atts.CELL,
                 Atts.CELL_FRAGMENT,
                 Atts.CELL_NAME,
                 Atts.CELL_OPT_ABSENT,
+                Atts.COLOR,
+                Atts.COLORS,
+                Atts.COMM,
+                Atts.FORMAT,
                 Atts.GROUP,
                 Atts.IMPURE,
                 Atts.INDEX,
                 Atts.INITIALIZER,
+                Atts.LEFT,
                 Atts.MAINCELL,
                 Atts.PREDICATE,
                 Atts.PREFER,
                 Atts.PRIVATE,
                 Atts.PRODUCTION,
                 Atts.PROJECTION,
+                Atts.RIGHT,
                 Atts.SEQSTRICT,
                 Atts.STRICT,
                 Atts.USER_LIST,
@@ -747,14 +754,6 @@ def simplified_module(definition: KDefinition, module_name: str | None = None) -
         AddSymbolAtts(Atts.FUNCTIONAL(None), _is_functional),
         AddSymbolAtts(Atts.INJECTIVE(None), _is_injective),
         AddSymbolAtts(Atts.CONSTRUCTOR(None), _is_constructor),
-        AddDefaultFormatAtts(),
-        DiscardFormatAtts(),
-        InlineFormatTerminals(),
-        AddColorAtts(),
-        DiscardSymbolAtts([Atts.COLOR]),
-        AddTerminalAtts(),
-        AddPrioritiesAtts(),
-        AddAssocAtts(),
     )
     definition = reduce(lambda defn, step: step.execute(defn), pipeline, definition)
     module = definition.modules[0]
@@ -1118,6 +1117,11 @@ def _update(self, production: KProduction) -> KProduction:
         return production.let(att=production.att.discard(self.keys))
 
 
+# -----------------
+# Syntax attributes
+# -----------------
+
+
 @dataclass
 class AddDefaultFormatAtts(SingleModulePass):
     """Add a default format attribute value to each symbol profuction missing one."""

src/pyk/kore/manip.py

@@ -2,14 +2,22 @@
 
 from typing import TYPE_CHECKING
 
-from .syntax import Assoc, EVar, MLQuant
+from .syntax import And, Assoc, EVar, MLQuant, Top
 
 if TYPE_CHECKING:
     from collections.abc import Collection
 
     from .syntax import Pattern
 
 
+def conjuncts(pattern: Pattern) -> tuple[Pattern, ...]:
+    if isinstance(pattern, Top):
+        return ()
+    if isinstance(pattern, And):
+        return tuple(conjunct for op in pattern.ops for conjunct in conjuncts(op))
+    return (pattern,)
+
+
 def free_occs(pattern: Pattern, *, bound_vars: Collection[str] = ()) -> dict[str, list[EVar]]:
     occurrences: dict[str, list[EVar]] = {}
 

src/pyk/kore/prelude.py

@@ -143,6 +143,7 @@ def le_int(left: Pattern, right: Pattern) -> Pattern:
 SORT_K_ITEM: Final = SortApp('SortKItem')
 SORT_K_CONFIG_VAR: Final = SortApp('SortKConfigVar')
 SORT_GENERATED_TOP_CELL: Final = SortApp('SortGeneratedTopCell')
+SORT_GENERATED_COUNTER_CELL: Final = SortApp('SortGeneratedCounterCell')
 
 LBL_INIT_GENERATED_TOP_CELL: Final = SymbolId('LblinitGeneratedTopCell')
 LBL_GENERATED_TOP: Final = SymbolId("Lbl'-LT-'generatedTop'-GT-'")

src/pyk/kore/rpc.py

@@ -18,8 +18,10 @@
 
 from psutil import Process
 
-from ..utils import check_dir_path, check_file_path, filter_none, run_process
-from .syntax import And, SortApp, kore_term
+from ..utils import FrozenDict, check_dir_path, check_file_path, filter_none, run_process
+from . import manip
+from .prelude import SORT_GENERATED_TOP_CELL
+from .syntax import And, Equals, EVar, kore_term
 
 if TYPE_CHECKING:
     from collections.abc import Iterable, Mapping
@@ -457,24 +459,83 @@ class StopReason(str, Enum):
 @dataclass(frozen=True)
 class State:
     term: Pattern
-    substitution: Pattern | None
+    substitution: FrozenDict[EVar, Pattern] | None
     predicate: Pattern | None
+    rule_id: str | None
+    rule_substitution: FrozenDict[EVar, Pattern] | None
+    rule_predicate: Pattern | None
+
+    def __init__(
+        self,
+        term: Pattern,
+        *,
+        substitution: Mapping[EVar, Pattern] | None = None,
+        predicate: Pattern | None = None,
+        rule_id: str | None = None,
+        rule_substitution: Mapping[EVar, Pattern] | None = None,
+        rule_predicate: Pattern | None = None,
+    ):
+        substitution = FrozenDict(substitution) if substitution is not None else None
+        rule_substitution = FrozenDict(rule_substitution) if rule_substitution is not None else None
+        object.__setattr__(self, 'term', term)
+        object.__setattr__(self, 'substitution', substitution)
+        object.__setattr__(self, 'predicate', predicate)
+        object.__setattr__(self, 'rule_id', rule_id)
+        object.__setattr__(self, 'rule_substitution', rule_substitution)
+        object.__setattr__(self, 'rule_predicate', rule_predicate)
 
     @staticmethod
     def from_dict(dct: Mapping[str, Any]) -> State:
         return State(
             term=kore_term(dct['term']),
-            substitution=kore_term(dct['substitution']) if 'substitution' in dct else None,
+            substitution=State._subst_to_dict(kore_term(dct['substitution'])) if 'substitution' in dct else None,
             predicate=kore_term(dct['predicate']) if 'predicate' in dct else None,
+            rule_id=dct.get('rule-id'),
+            rule_substitution=(
+                State._subst_to_dict(kore_term(dct['rule-substitution'])) if 'rule-substitution' in dct else None
+            ),
+            rule_predicate=kore_term(dct['rule-predicate']) if 'rule-predicate' in dct else None,
+        )
+
+    @staticmethod
+    def _subst_to_dict(pattern: Pattern) -> dict[EVar, Pattern]:
+        def extract_entry(pattern: Pattern) -> tuple[EVar, Pattern]:
+            if not isinstance(pattern, Equals):
+                raise ValueError(fr'Expected \equals as substituion entry, got: {pattern.text}')
+            if pattern.sort != SORT_GENERATED_TOP_CELL:
+                raise ValueError(
+                    f'Expected {SORT_GENERATED_TOP_CELL.text} as substitution entry sort, got: {pattern.sort.text}'
+                )
+            if not isinstance(pattern.left, EVar):
+                raise ValueError(f'Expected EVar as substitution entry key, got: {pattern.left.text}')
+            if pattern.left.sort != pattern.op_sort:
+                raise ValueError(
+                    f'Mismatch between substitution entry and key sort: {pattern.op_sort.text} and {pattern.left.sort.text}'
+                )
+            return pattern.left, pattern.right
+
+        res: dict[EVar, Pattern] = {}
+        for conjunct in manip.conjuncts(pattern):
+            key, value = extract_entry(conjunct)
+            if key in res:
+                raise ValueError(f'Duplicate substitution entry key: {key.text}')
+            res[key] = value
+        return res
+
+    @staticmethod
+    def _dict_to_subst(dct: Mapping[EVar, Pattern]) -> And:
+        return And(
+            SORT_GENERATED_TOP_CELL,
+            tuple(Equals(var.sort, SORT_GENERATED_TOP_CELL, var, val) for var, val in dct.items()),
         )
 
     @property
     def kore(self) -> Pattern:
         _kore = self.term
         if self.substitution is not None:
-            _kore = And(SortApp('SortGeneratedTopCell'), (_kore, self.substitution))
+            _kore = And(SORT_GENERATED_TOP_CELL, (_kore,) + self._dict_to_subst(self.substitution).ops)
         if self.predicate is not None:
-            _kore = And(SortApp('SortGeneratedTopCell'), (_kore, self.predicate))
+            _kore = And(SORT_GENERATED_TOP_CELL, (_kore, self.predicate))
         return _kore
 
 

src/tests/integration/kore/test_kore_client.py

@@ -12,7 +12,9 @@
 from pyk.kore.prelude import (
     BOOL,
     INT,
+    SORT_GENERATED_COUNTER_CELL,
     SORT_GENERATED_TOP_CELL,
+    SORT_K,
     SORT_K_ITEM,
     TRUE,
     and_bool,
@@ -89,11 +91,38 @@ def term(n: int) -> Pattern:
 
 
 def state(n: int) -> State:
-    return State(term=term(n), substitution=None, predicate=None)
+    return State(term=term(n))
 
 
 EXECUTE_TEST_DATA: Final[tuple[tuple[str, int, Mapping[str, Any], ExecuteResult], ...]] = (
-    ('branching', 0, {}, BranchingResult(state=state(2), depth=2, next_states=(state(4), state(3)), logs=())),
+    (
+        'branching',
+        0,
+        {},
+        BranchingResult(
+            state=state(2),
+            depth=2,
+            next_states=(
+                State(
+                    term=term(3),
+                    rule_id='ae0c978867ef4cc5cbfbadf7be2ff55e30e59465697ceaffa1d9fd5343a21fc6',
+                    rule_substitution={
+                        EVar('GCC', SORT_GENERATED_COUNTER_CELL): EVar("Var'Unds'DotVar0", SORT_GENERATED_COUNTER_CELL),
+                        EVar('K', SORT_K): EVar("Var'Unds'DotVar1", SORT_K),
+                    },
+                ),
+                State(
+                    term=term(4),
+                    rule_id='37a544ff4b6da9b4fb839f86d2ad51b770bcaf3dd578b716c38cf0da33458374',
+                    rule_substitution={
+                        EVar('GCC', SORT_GENERATED_COUNTER_CELL): EVar("Var'Unds'DotVar0", SORT_GENERATED_COUNTER_CELL),
+                        EVar('K', SORT_K): EVar("Var'Unds'DotVar1", SORT_K),
+                    },
+                ),
+            ),
+            logs=(),
+        ),
+    ),
     ('depth-bound', 0, {'max_depth': 2}, DepthBoundResult(state=state(2), depth=2, logs=())),
     ('stuck', 4, {}, StuckResult(state=state(6), depth=2, logs=())),
     (
@@ -473,7 +502,7 @@ def rule(lhs: int, rhs: int) -> Axiom:
     def test_base_module(self, kore_client: KoreClient) -> None:
         # Given
         config = self.config(0)
-        expected = StuckResult(State(term=config, substitution=None, predicate=None), depth=0, logs=())
+        expected = StuckResult(State(term=config), depth=0, logs=())
 
         # When
         actual = kore_client.execute(config)
@@ -484,7 +513,7 @@ def test_base_module(self, kore_client: KoreClient) -> None:
     def test_base_module_explicitly(self, kore_client: KoreClient) -> None:
         # Given
         config = self.config(0)
-        expected = StuckResult(State(term=config, substitution=None, predicate=None), depth=0, logs=())
+        expected = StuckResult(State(term=config), depth=0, logs=())
 
         # When
         actual = kore_client.execute(config, module_name=self.KOMPILE_MAIN_MODULE)
@@ -496,7 +525,7 @@ def test_add_a_single_module(self, kore_client: KoreClient) -> None:
         # Given
         config = self.config(0)
         module = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1)))
-        expected = StuckResult(State(term=self.config(1), substitution=None, predicate=None), depth=1, logs=())
+        expected = StuckResult(State(term=self.config(1)), depth=1, logs=())
 
         # When
         module_id = kore_client.add_module(module)
@@ -509,7 +538,7 @@ def test_add_a_single_module_but_dont_use_it(self, kore_client: KoreClient) -> N
         # Given
         config = self.config(0)
         module = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1)))
-        expected = StuckResult(State(term=self.config(0), substitution=None, predicate=None), depth=0, logs=())
+        expected = StuckResult(State(term=self.config(0)), depth=0, logs=())
 
         # When
         kore_client.add_module(module)
@@ -522,7 +551,7 @@ def test_name_as_id(self, kore_client: KoreClient) -> None:
         # Given
         config = self.config(0)
         module = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1)))
-        expected = StuckResult(State(term=self.config(1), substitution=None, predicate=None), depth=1, logs=())
+        expected = StuckResult(State(term=self.config(1)), depth=1, logs=())
 
         # When
         kore_client.add_module(module, name_as_id=True)
@@ -545,7 +574,7 @@ def test_add_module_twice(self, kore_client: KoreClient) -> None:
         # Given
         config = self.config(0)
         module = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1)))
-        expected = StuckResult(State(term=self.config(1), substitution=None, predicate=None), depth=1, logs=())
+        expected = StuckResult(State(term=self.config(1)), depth=1, logs=())
 
         # When
         module_id = kore_client.add_module(module)
@@ -564,7 +593,7 @@ def test_add_module_twice_with_name(self, kore_client: KoreClient) -> None:
         # Given
         config = self.config(0)
         module = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1)))
-        expected = StuckResult(State(term=self.config(1), substitution=None, predicate=None), depth=1, logs=())
+        expected = StuckResult(State(term=self.config(1)), depth=1, logs=())
 
         # When
         module_id = kore_client.add_module(module, name_as_id=True)
@@ -583,7 +612,7 @@ def test_add_module_without_name_then_with_name(self, kore_client: KoreClient) -
         # Given
         config = self.config(0)
         module = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1)))
-        expected = StuckResult(State(term=self.config(1), substitution=None, predicate=None), depth=1, logs=())
+        expected = StuckResult(State(term=self.config(1)), depth=1, logs=())
 
         # When
         module_id = kore_client.add_module(module)
@@ -608,7 +637,7 @@ def test_add_module_with_name_then_without_name(self, kore_client: KoreClient) -
         # Given
         config = self.config(0)
         module = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1)))
-        expected = StuckResult(State(term=self.config(1), substitution=None, predicate=None), depth=1, logs=())
+        expected = StuckResult(State(term=self.config(1)), depth=1, logs=())
 
         # When
         module_id = kore_client.add_module(module, name_as_id=True)
@@ -650,8 +679,8 @@ def test_add_two_modules_second_with_same_name_as_id(self, kore_client: KoreClie
         config = self.config(0)
         module_1 = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1)))
         module_2 = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 2)))
-        expected_1 = StuckResult(State(term=self.config(1), substitution=None, predicate=None), depth=1, logs=())
-        expected_2 = StuckResult(State(term=self.config(2), substitution=None, predicate=None), depth=1, logs=())
+        expected_1 = StuckResult(State(term=self.config(1)), depth=1, logs=())
+        expected_2 = StuckResult(State(term=self.config(2)), depth=1, logs=())
 
         # When
         module_id = kore_client.add_module(module_1)
@@ -672,8 +701,8 @@ def test_add_two_modules_first_with_same_name_as_id(self, kore_client: KoreClien
         config = self.config(0)
         module_1 = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1)))
         module_2 = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 2)))
-        expected_1 = StuckResult(State(term=self.config(1), substitution=None, predicate=None), depth=1, logs=())
-        expected_2 = StuckResult(State(term=self.config(2), substitution=None, predicate=None), depth=1, logs=())
+        expected_1 = StuckResult(State(term=self.config(1)), depth=1, logs=())
+        expected_2 = StuckResult(State(term=self.config(2)), depth=1, logs=())
 
         # When
         kore_client.add_module(module_1, name_as_id=True)
@@ -693,7 +722,7 @@ def test_add_module_with_import(self, kore_client: KoreClient) -> None:
         # Given
         config = self.config(0)
         module_1 = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1)))
-        expected = StuckResult(State(term=self.config(2), substitution=None, predicate=None), depth=2, logs=())
+        expected = StuckResult(State(term=self.config(2)), depth=2, logs=())
 
         # When
         module_1_id = kore_client.add_module(module_1)
@@ -709,7 +738,7 @@ def test_add_module_with_named_import(self, kore_client: KoreClient) -> None:
         config = self.config(0)
         module_1 = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1)))
         module_2 = Module('B', sentences=(Import('A'), self.rule(1, 2)))
-        expected = StuckResult(State(term=self.config(2), substitution=None, predicate=None), depth=2, logs=())
+        expected = StuckResult(State(term=self.config(2)), depth=2, logs=())
 
         # When
         kore_client.add_module(module_1, name_as_id=True)