Deduplicate productions

package/version

@@ -1 +1 @@
-0.1.340
+0.1.341

pyproject.toml

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

src/pyk/kast/outer.py

@@ -1029,10 +1029,20 @@ def production_for_klabel(self, klabel: KLabel) -> KProduction:
             prods = [prod for prod in self.productions if prod.klabel and prod.klabel.name == klabel.name]
             _prods = [prod for prod in prods if 'unparseAvoid' not in prod.att]
             if len(_prods) < len(prods):
-                prods = _prods
                 _LOGGER.warning(
                     f'Discarding {len(prods) - len(_prods)} productions with `unparseAvoid` attribute for label: {klabel}'
                 )
+                prods = _prods
+            # Automatically defined symbols like isInt may get multiple
+            # definitions in different modules.
+            unique_no_att: dict[KProduction, KProduction] = {}
+            for prod in prods:
+                trimmed_prod = prod.let_att(EMPTY_ATT)
+                unique_no_att[trimmed_prod] = prod
+            _prods = list(unique_no_att.values())
+            if len(_prods) < len(prods):
+                _LOGGER.warning(f'Discarding {len(prods) - len(_prods)} equivalent productions')
+                prods = _prods
             try:
                 self._production_for_klabel[klabel] = single(prods)
             except ValueError as err:

src/tests/integration/k-files/multiple-definitions.k

@@ -0,0 +1,20 @@
+module MULTIPLE-DEFINITIONS
+  imports A
+  imports B
+  imports BOOL
+
+  syntax KItem  ::= a(KItem) [symbol, label(a)]
+                  | "b" [symbol, label(b)]
+                  | "c" [symbol, label(c)]
+  rule a(X) => b requires isInt(X)
+  rule a(X) => b requires notBool isInt(X)
+  rule b => c
+endmodule
+
+module A
+  syntax Int
+endmodule
+
+module B
+  syntax Int
+endmodule

src/tests/integration/kcfg/test_multiple_definitions.py

@@ -0,0 +1,70 @@
+from __future__ import annotations
+
+from typing import TYPE_CHECKING
+
+import pytest
+
+from pyk.cterm import CTerm
+from pyk.kast.inner import KApply, KSequence, KVariable
+from pyk.prelude.ml import mlTop
+from pyk.testing import KCFGExploreTest
+
+from ..utils import K_FILES
+
+if TYPE_CHECKING:
+    from collections.abc import Iterable
+
+    from pyk.kcfg import KCFGExplore
+
+
+EXECUTE_TEST_DATA: Iterable[tuple[str]] = (('branch',),)
+
+
+class TestMultipleDefinitionsProof(KCFGExploreTest):
+    KOMPILE_MAIN_FILE = K_FILES / 'multiple-definitions.k'
+
+    @staticmethod
+    def config() -> CTerm:
+        return CTerm(
+            KApply(
+                '<generatedTop>',
+                KApply('<k>', KSequence(KApply('a', [KVariable('X')]))),
+                KVariable('GENERATED_COUNTER_CELL'),
+            ),
+            (mlTop(),),
+        )
+
+    @pytest.mark.parametrize(
+        'test_id',
+        EXECUTE_TEST_DATA,
+        ids=[test_id for test_id, *_ in EXECUTE_TEST_DATA],
+    )
+    def test_execute(
+        self,
+        kcfg_explore: KCFGExplore,
+        test_id: str,
+    ) -> None:
+        split_depth, split_post_term, split_next_terms, _logs = kcfg_explore.cterm_execute(self.config(), depth=1)
+
+        split_k = kcfg_explore.kprint.pretty_print(split_post_term.cell('K_CELL'))
+        split_next_k = [kcfg_explore.kprint.pretty_print(split_post_term.cell('K_CELL')) for term in split_next_terms]
+
+        assert split_depth == 0
+        assert len(split_next_terms) == 2
+        assert 'a ( X:KItem )' == split_k
+        assert [
+            'a ( X:KItem )',
+            'a ( X:KItem )',
+        ] == split_next_k
+
+        step_1_depth, step_1_post_term, step_1_next_terms, _logs = kcfg_explore.cterm_execute(
+            split_next_terms[0], depth=1
+        )
+        step_1_k = kcfg_explore.kprint.pretty_print(step_1_post_term.cell('K_CELL'))
+        assert 'c' == step_1_k
+
+        step_2_depth, step_2_post_term, step_2_next_terms, _logs = kcfg_explore.cterm_execute(
+            split_next_terms[1], depth=1
+        )
+        step_2_k = kcfg_explore.kprint.pretty_print(step_1_post_term.cell('K_CELL'))
+        assert 'c' == step_2_k