diff --git a/pyk/src/pyk/kcfg/explore.py b/pyk/src/pyk/kcfg/explore.py index f1d06cc3ea..5562132e3e 100644 --- a/pyk/src/pyk/kcfg/explore.py +++ b/pyk/src/pyk/kcfg/explore.py @@ -220,7 +220,7 @@ def extend_cterm( module_name: str | None = None, ) -> list[KCFGExtendResult]: - custom_step_result = self.kcfg_semantics.custom_step(_cterm, self.cterm_symbolic) + custom_step_result = self.kcfg_semantics.custom_step(_cterm, self.cterm_symbolic, node_id) if custom_step_result is not None: return [custom_step_result] diff --git a/pyk/src/pyk/kcfg/semantics.py b/pyk/src/pyk/kcfg/semantics.py index 89569e300e..4f35656571 100644 --- a/pyk/src/pyk/kcfg/semantics.py +++ b/pyk/src/pyk/kcfg/semantics.py @@ -35,9 +35,18 @@ def can_make_custom_step(self, c: CTerm) -> bool: ... """Check whether or not the semantics can make a custom step from a given ``CTerm``.""" @abstractmethod - def custom_step(self, c: CTerm, cs: CTermSymbolic) -> KCFGExtendResult | None: ... - - """Implement a custom semantic step.""" + def custom_step(self, c: CTerm, cs: CTermSymbolic, node_id: int) -> KCFGExtendResult | None: ... + + """Implement a custom semantic step. + + Args: + c: Current constrained term representing the state. + cs: ``CTermSymbolic`` for computing the custom step result. + node_id: Current node id. + + Returns: + The ``KCFGExtendResult`` produced by this custom step if this custom step can produce one, ``None`` otherwise. + """ @abstractmethod def is_mergeable(self, c1: CTerm, c2: CTerm) -> bool: ... @@ -61,7 +70,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool: def can_make_custom_step(self, c: CTerm) -> bool: return False - def custom_step(self, c: CTerm, cs: CTermSymbolic) -> KCFGExtendResult | None: + def custom_step(self, c: CTerm, cs: CTermSymbolic, node_id: int) -> KCFGExtendResult | None: return None def is_mergeable(self, c1: CTerm, c2: CTerm) -> bool: diff --git a/pyk/src/tests/integration/proof/test_custom_step.py b/pyk/src/tests/integration/proof/test_custom_step.py index 141f95b3a1..4330c21ae5 100644 --- a/pyk/src/tests/integration/proof/test_custom_step.py +++ b/pyk/src/tests/integration/proof/test_custom_step.py @@ -70,7 +70,7 @@ def can_make_custom_step(self, c: CTerm) -> bool: and k_cell[0].label.name == 'c_CUSTOM-STEP-SYNTAX_Step' ) - def custom_step(self, c: CTerm, cs: CTermSymbolic) -> KCFGExtendResult | None: + def custom_step(self, c: CTerm, cs: CTermSymbolic, node_id: int) -> KCFGExtendResult | None: if self.can_make_custom_step(c): new_cterm = CTerm.from_kast(set_cell(c.kast, 'K_CELL', KSequence(KApply('d_CUSTOM-STEP-SYNTAX_Step')))) return Step(new_cterm, 1, (), ['CUSTOM-STEP.c.d'], cut=True) @@ -153,7 +153,7 @@ def test_custom_step_exec( # When kcfg_semantics = CustomStepSemanticsWithStep() - actual = kcfg_semantics.custom_step(cterm, cterm_symbolic) + actual = kcfg_semantics.custom_step(cterm, cterm_symbolic, node_id=0) # Then assert expected == actual diff --git a/pyk/src/tests/integration/proof/test_prove_rpc.py b/pyk/src/tests/integration/proof/test_prove_rpc.py index 5ffbfc449e..bdb90314be 100644 --- a/pyk/src/tests/integration/proof/test_prove_rpc.py +++ b/pyk/src/tests/integration/proof/test_prove_rpc.py @@ -71,7 +71,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool: def can_make_custom_step(self, c: CTerm) -> bool: return False - def custom_step(self, c: CTerm, cs: CTermSymbolic) -> KCFGExtendResult | None: + def custom_step(self, c: CTerm, cs: CTermSymbolic, node_id: int) -> KCFGExtendResult | None: return None