From 29ff8d01acc443477e0766e3e1fca5544095868b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 11 Dec 2023 09:36:27 +0000 Subject: [PATCH 01/15] Extract class `CTermExecute` --- src/pyk/kcfg/explore.py | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index 72011022f..6e7dd9875 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -3,7 +3,7 @@ import logging from abc import ABC from dataclasses import dataclass, field -from typing import TYPE_CHECKING, final +from typing import TYPE_CHECKING, NamedTuple, final from ..cterm import CSubst, CTerm from ..kast.inner import KApply, KLabel, KRewrite, KVariable, Subst @@ -47,6 +47,14 @@ _LOGGER: Final = logging.getLogger(__name__) +class CTermExecute(NamedTuple): + vacuous: bool + depth: int + next_state: CTerm + next_states: list[CTerm] + logs: tuple[LogEntry, ...] + + class KCFGExplore: kprint: KPrint _kore_client: KoreClient @@ -77,7 +85,7 @@ def cterm_execute( cut_point_rules: Iterable[str] | None = None, terminal_rules: Iterable[str] | None = None, module_name: str | None = None, - ) -> tuple[bool, int, CTerm, list[CTerm], tuple[LogEntry, ...]]: + ) -> CTermExecute: _LOGGER.debug(f'Executing: {cterm}') kore = self.kprint.kast_to_kore(cterm.kast, GENERATED_TOP_CELL) er = self._kore_client.execute( @@ -103,13 +111,13 @@ def cterm_execute( next_states = [CTerm.from_kast(self.kprint.kore_to_kast(ns.kore)) for ns in _next_states] next_states = [cterm for cterm in next_states if not cterm.is_bottom] if len(next_states) == 1 and len(next_states) < len(_next_states): - return _is_vacuous, depth + 1, next_states[0], [], er.logs + return CTermExecute(_is_vacuous, depth + 1, next_states[0], [], er.logs) elif len(next_states) == 1: if er.reason == StopReason.CUT_POINT_RULE: - return _is_vacuous, depth, next_state, next_states, er.logs + return CTermExecute(_is_vacuous, depth, next_state, next_states, er.logs) else: next_states = [] - return _is_vacuous, depth, next_state, next_states, er.logs + return CTermExecute(_is_vacuous, depth, next_state, next_states, er.logs) def cterm_simplify(self, cterm: CTerm) -> tuple[CTerm, tuple[LogEntry, ...]]: _LOGGER.debug(f'Simplifying: {cterm}') From 60f3e91c8e02bb2c5185f0e3fe9bb667e214cc7a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 11 Dec 2023 09:51:31 +0000 Subject: [PATCH 02/15] Replace filtering with assertion --- src/pyk/kcfg/explore.py | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index 6e7dd9875..e620ef984 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -109,9 +109,12 @@ def cterm_execute( next_state = CTerm.from_kast(self.kprint.kore_to_kast(er.state.kore)) _next_states = er.next_states if er.next_states is not None else [] next_states = [CTerm.from_kast(self.kprint.kore_to_kast(ns.kore)) for ns in _next_states] - next_states = [cterm for cterm in next_states if not cterm.is_bottom] + + if any(cterm.is_bottom for cterm in next_states): + raise AssertionError(f'#Bottom value in next-states in response: {er}') + if len(next_states) == 1 and len(next_states) < len(_next_states): - return CTermExecute(_is_vacuous, depth + 1, next_states[0], [], er.logs) + raise AssertionError('Should be unreachable') elif len(next_states) == 1: if er.reason == StopReason.CUT_POINT_RULE: return CTermExecute(_is_vacuous, depth, next_state, next_states, er.logs) From 720dd961bb8f541afff09b47142d919188d5355d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 11 Dec 2023 13:31:57 +0000 Subject: [PATCH 03/15] Remove unreachable branch --- src/pyk/kcfg/explore.py | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index e620ef984..90bb3a8d6 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -113,9 +113,7 @@ def cterm_execute( if any(cterm.is_bottom for cterm in next_states): raise AssertionError(f'#Bottom value in next-states in response: {er}') - if len(next_states) == 1 and len(next_states) < len(_next_states): - raise AssertionError('Should be unreachable') - elif len(next_states) == 1: + if len(next_states) == 1: if er.reason == StopReason.CUT_POINT_RULE: return CTermExecute(_is_vacuous, depth, next_state, next_states, er.logs) else: From c997388755d20b2c6126ff8cee712a89afe9960d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 11 Dec 2023 13:48:33 +0000 Subject: [PATCH 04/15] Remove unreachable branch --- src/pyk/kcfg/explore.py | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index 90bb3a8d6..8a497c41d 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -114,10 +114,8 @@ def cterm_execute( raise AssertionError(f'#Bottom value in next-states in response: {er}') if len(next_states) == 1: - if er.reason == StopReason.CUT_POINT_RULE: - return CTermExecute(_is_vacuous, depth, next_state, next_states, er.logs) - else: - next_states = [] + assert er.reason is StopReason.CUT_POINT_RULE: + return CTermExecute(_is_vacuous, depth, next_state, next_states, er.logs) return CTermExecute(_is_vacuous, depth, next_state, next_states, er.logs) def cterm_simplify(self, cterm: CTerm) -> tuple[CTerm, tuple[LogEntry, ...]]: From 699693c98c8095084b53854fca169792cdb83b4b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 11 Dec 2023 13:51:56 +0000 Subject: [PATCH 05/15] Remove spurious return statement --- src/pyk/kcfg/explore.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index 8a497c41d..8ec0bea22 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -115,7 +115,7 @@ def cterm_execute( if len(next_states) == 1: assert er.reason is StopReason.CUT_POINT_RULE: - return CTermExecute(_is_vacuous, depth, next_state, next_states, er.logs) + return CTermExecute(_is_vacuous, depth, next_state, next_states, er.logs) def cterm_simplify(self, cterm: CTerm) -> tuple[CTerm, tuple[LogEntry, ...]]: From e176e5f5c757b0305aa7d88eb231a49b14742e58 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 11 Dec 2023 13:53:25 +0000 Subject: [PATCH 06/15] Simplify assertions --- src/pyk/kcfg/explore.py | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index 8ec0bea22..9e15e792c 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -110,11 +110,8 @@ def cterm_execute( _next_states = er.next_states if er.next_states is not None else [] next_states = [CTerm.from_kast(self.kprint.kore_to_kast(ns.kore)) for ns in _next_states] - if any(cterm.is_bottom for cterm in next_states): - raise AssertionError(f'#Bottom value in next-states in response: {er}') - - if len(next_states) == 1: - assert er.reason is StopReason.CUT_POINT_RULE: + assert all(not cterm.is_bottom for cterm in next_states) + assert len(next_states) != 1 or er.reason is StopReason.CUT_POINT_RULE return CTermExecute(_is_vacuous, depth, next_state, next_states, er.logs) From 5e0e3960b6cde980631642d9b0ad2c78817001fd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 11 Dec 2023 13:59:49 +0000 Subject: [PATCH 07/15] Simplify arguments --- src/pyk/kcfg/explore.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index 9e15e792c..c492f5170 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -94,10 +94,10 @@ def cterm_execute( cut_point_rules=cut_point_rules, terminal_rules=terminal_rules, module_name=module_name, - log_successful_rewrites=self._trace_rewrites if self._trace_rewrites else None, - log_failed_rewrites=self._trace_rewrites if self._trace_rewrites else None, - log_successful_simplifications=self._trace_rewrites if self._trace_rewrites else None, - log_failed_simplifications=self._trace_rewrites if self._trace_rewrites else None, + log_successful_rewrites=self._trace_rewrites, + log_failed_rewrites=self._trace_rewrites, + log_successful_simplifications=self._trace_rewrites, + log_failed_simplifications=self._trace_rewrites, ) if isinstance(er, AbortedResult): From aa850d59010109b1b8fe45f9206677888a9c1bd0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 11 Dec 2023 14:03:43 +0000 Subject: [PATCH 08/15] Inline some arguments --- src/pyk/kcfg/explore.py | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index c492f5170..89bdc0ad4 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -104,8 +104,6 @@ def cterm_execute( unknown_predicate = er.unknown_predicate.text if er.unknown_predicate else None raise ValueError(f'Backend responded with aborted state. Unknown predicate: {unknown_predicate}') - _is_vacuous = er.reason is StopReason.VACUOUS - depth = er.depth next_state = CTerm.from_kast(self.kprint.kore_to_kast(er.state.kore)) _next_states = er.next_states if er.next_states is not None else [] next_states = [CTerm.from_kast(self.kprint.kore_to_kast(ns.kore)) for ns in _next_states] @@ -113,7 +111,13 @@ def cterm_execute( assert all(not cterm.is_bottom for cterm in next_states) assert len(next_states) != 1 or er.reason is StopReason.CUT_POINT_RULE - return CTermExecute(_is_vacuous, depth, next_state, next_states, er.logs) + return CTermExecute( + vacuous=er.reason is StopReason.VACUOUS, + depth=er.depth, + next_state=next_state, + next_states=next_states, + logs=er.logs, + ) def cterm_simplify(self, cterm: CTerm) -> tuple[CTerm, tuple[LogEntry, ...]]: _LOGGER.debug(f'Simplifying: {cterm}') From 20f16e3d7551e3d0ed77dbbdc8ca81df98a1991f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 11 Dec 2023 14:08:57 +0000 Subject: [PATCH 09/15] Rename `next_state` to `state` --- src/pyk/kcfg/explore.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index 89bdc0ad4..bbef890de 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -50,7 +50,7 @@ class CTermExecute(NamedTuple): vacuous: bool depth: int - next_state: CTerm + state: CTerm next_states: list[CTerm] logs: tuple[LogEntry, ...] @@ -104,7 +104,7 @@ def cterm_execute( unknown_predicate = er.unknown_predicate.text if er.unknown_predicate else None raise ValueError(f'Backend responded with aborted state. Unknown predicate: {unknown_predicate}') - next_state = CTerm.from_kast(self.kprint.kore_to_kast(er.state.kore)) + state = CTerm.from_kast(self.kprint.kore_to_kast(er.state.kore)) _next_states = er.next_states if er.next_states is not None else [] next_states = [CTerm.from_kast(self.kprint.kore_to_kast(ns.kore)) for ns in _next_states] @@ -114,7 +114,7 @@ def cterm_execute( return CTermExecute( vacuous=er.reason is StopReason.VACUOUS, depth=er.depth, - next_state=next_state, + state=state, next_states=next_states, logs=er.logs, ) From b9e987e6d8a24f884e609239a62d281b36e49125 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 11 Dec 2023 14:11:08 +0000 Subject: [PATCH 10/15] Replace `if` with `or` --- src/pyk/kcfg/explore.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index bbef890de..7122bac97 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -105,8 +105,8 @@ def cterm_execute( raise ValueError(f'Backend responded with aborted state. Unknown predicate: {unknown_predicate}') state = CTerm.from_kast(self.kprint.kore_to_kast(er.state.kore)) - _next_states = er.next_states if er.next_states is not None else [] - next_states = [CTerm.from_kast(self.kprint.kore_to_kast(ns.kore)) for ns in _next_states] + resp_next_states = er.next_states or () + next_states = [CTerm.from_kast(self.kprint.kore_to_kast(ns.kore)) for ns in resp_next_states] assert all(not cterm.is_bottom for cterm in next_states) assert len(next_states) != 1 or er.reason is StopReason.CUT_POINT_RULE From 80edd875c2d0964610e1d0456f3f1a7c6d814e18 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 11 Dec 2023 14:12:16 +0000 Subject: [PATCH 11/15] Rename `er` to `response` --- src/pyk/kcfg/explore.py | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index 7122bac97..2bb6c39a2 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -88,7 +88,7 @@ def cterm_execute( ) -> CTermExecute: _LOGGER.debug(f'Executing: {cterm}') kore = self.kprint.kast_to_kore(cterm.kast, GENERATED_TOP_CELL) - er = self._kore_client.execute( + response = self._kore_client.execute( kore, max_depth=depth, cut_point_rules=cut_point_rules, @@ -100,23 +100,23 @@ def cterm_execute( log_failed_simplifications=self._trace_rewrites, ) - if isinstance(er, AbortedResult): - unknown_predicate = er.unknown_predicate.text if er.unknown_predicate else None + if isinstance(response, AbortedResult): + unknown_predicate = response.unknown_predicate.text if response.unknown_predicate else None raise ValueError(f'Backend responded with aborted state. Unknown predicate: {unknown_predicate}') - state = CTerm.from_kast(self.kprint.kore_to_kast(er.state.kore)) - resp_next_states = er.next_states or () + state = CTerm.from_kast(self.kprint.kore_to_kast(response.state.kore)) + resp_next_states = response.next_states or () next_states = [CTerm.from_kast(self.kprint.kore_to_kast(ns.kore)) for ns in resp_next_states] assert all(not cterm.is_bottom for cterm in next_states) - assert len(next_states) != 1 or er.reason is StopReason.CUT_POINT_RULE + assert len(next_states) != 1 or response.reason is StopReason.CUT_POINT_RULE return CTermExecute( - vacuous=er.reason is StopReason.VACUOUS, - depth=er.depth, + vacuous=response.reason is StopReason.VACUOUS, + depth=response.depth, state=state, next_states=next_states, - logs=er.logs, + logs=response.logs, ) def cterm_simplify(self, cterm: CTerm) -> tuple[CTerm, tuple[LogEntry, ...]]: From a9526413b488b539da8c2d77fb6917288edc7d3b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 11 Dec 2023 14:14:37 +0000 Subject: [PATCH 12/15] Replace `list` by `tuple` --- src/pyk/kcfg/explore.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index 2bb6c39a2..a1639df66 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -51,7 +51,7 @@ class CTermExecute(NamedTuple): vacuous: bool depth: int state: CTerm - next_states: list[CTerm] + next_states: tuple[CTerm, ...] logs: tuple[LogEntry, ...] @@ -106,7 +106,7 @@ def cterm_execute( state = CTerm.from_kast(self.kprint.kore_to_kast(response.state.kore)) resp_next_states = response.next_states or () - next_states = [CTerm.from_kast(self.kprint.kore_to_kast(ns.kore)) for ns in resp_next_states] + next_states = tuple(CTerm.from_kast(self.kprint.kore_to_kast(ns.kore)) for ns in resp_next_states) assert all(not cterm.is_bottom for cterm in next_states) assert len(next_states) != 1 or response.reason is StopReason.CUT_POINT_RULE From d6323661b28268e1d174f731ac3ec9ce6d00ce73 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 11 Dec 2023 14:35:17 +0000 Subject: [PATCH 13/15] Eliminate unpacking --- src/pyk/kcfg/explore.py | 14 +++++------- .../kcfg/test_multiple_definitions.py | 22 ++++++++----------- src/tests/integration/kcfg/test_simple.py | 11 +++++----- src/tests/integration/proof/test_cell_map.py | 7 +++--- src/tests/integration/proof/test_imp.py | 11 +++++----- 5 files changed, 28 insertions(+), 37 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index a1639df66..642bd6e69 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -310,16 +310,14 @@ def step( if len(successors) != 0 and type(successors[0]) is KCFG.Split: raise ValueError(f'Cannot take step from split node {self.id}: {shorten_hashes(node.id)}') _LOGGER.info(f'Taking {depth} steps from node {self.id}: {shorten_hashes(node.id)}') - _, actual_depth, cterm, next_cterms, next_node_logs = self.cterm_execute( - node.cterm, depth=depth, module_name=module_name - ) - if actual_depth != depth: - raise ValueError(f'Unable to take {depth} steps from node, got {actual_depth} steps {self.id}: {node.id}') - if len(next_cterms) > 0: + exec_res = self.cterm_execute(node.cterm, depth=depth, module_name=module_name) + if exec_res.depth != depth: + raise ValueError(f'Unable to take {depth} steps from node, got {exec_res.depth} steps {self.id}: {node.id}') + if len(exec_res.next_states) > 0: raise ValueError(f'Found branch within {depth} steps {self.id}: {node.id}') - new_node = cfg.create_node(cterm) + new_node = cfg.create_node(exec_res.state) _LOGGER.info(f'Found new node at depth {depth} {self.id}: {shorten_hashes((node.id, new_node.id))}') - logs[new_node.id] = next_node_logs + logs[new_node.id] = exec_res.logs out_edges = cfg.edges(source_id=node.id) if len(out_edges) == 0: cfg.create_edge(node.id, new_node.id, depth=depth) diff --git a/src/tests/integration/kcfg/test_multiple_definitions.py b/src/tests/integration/kcfg/test_multiple_definitions.py index b6fd399f2..e2de82cf1 100644 --- a/src/tests/integration/kcfg/test_multiple_definitions.py +++ b/src/tests/integration/kcfg/test_multiple_definitions.py @@ -44,12 +44,12 @@ def test_execute( kcfg_explore: KCFGExplore, test_id: str, ) -> None: - _, split_depth, split_post_term, split_next_terms, _logs = kcfg_explore.cterm_execute(self.config(), depth=1) + exec_res = kcfg_explore.cterm_execute(self.config(), depth=1) + split_next_terms = exec_res.next_states + split_k = kcfg_explore.kprint.pretty_print(exec_res.state.cell('K_CELL')) + split_next_k = [kcfg_explore.kprint.pretty_print(exec_res.state.cell('K_CELL')) for _ in split_next_terms] - 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 exec_res.depth == 0 assert len(split_next_terms) == 2 assert 'a ( X:KItem )' == split_k assert [ @@ -57,14 +57,10 @@ def test_execute( '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')) + step_1_res = kcfg_explore.cterm_execute(split_next_terms[0], depth=1) + step_1_k = kcfg_explore.kprint.pretty_print(step_1_res.state.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')) + step_2_res = kcfg_explore.cterm_execute(split_next_terms[1], depth=1) + step_2_k = kcfg_explore.kprint.pretty_print(step_2_res.state.cell('K_CELL')) assert 'c' == step_2_k diff --git a/src/tests/integration/kcfg/test_simple.py b/src/tests/integration/kcfg/test_simple.py index b48c35e9f..df185a5de 100644 --- a/src/tests/integration/kcfg/test_simple.py +++ b/src/tests/integration/kcfg/test_simple.py @@ -78,17 +78,16 @@ def test_execute( expected_k, expected_state, *_ = expected_post # When - _, actual_depth, actual_post_term, actual_next_terms, _logs = kcfg_explore.cterm_execute( - self.config(kcfg_explore.kprint, *pre), depth=depth - ) - actual_k = kcfg_explore.kprint.pretty_print(actual_post_term.cell('K_CELL')) - actual_state = kcfg_explore.kprint.pretty_print(actual_post_term.cell('STATE_CELL')) + exec_res = kcfg_explore.cterm_execute(self.config(kcfg_explore.kprint, *pre), depth=depth) + actual_k = kcfg_explore.kprint.pretty_print(exec_res.state.cell('K_CELL')) + actual_state = kcfg_explore.kprint.pretty_print(exec_res.state.cell('STATE_CELL')) + actual_depth = exec_res.depth actual_next_states = [ ( kcfg_explore.kprint.pretty_print(s.cell('K_CELL')), kcfg_explore.kprint.pretty_print(s.cell('STATE_CELL')), ) - for s in actual_next_terms + for s in exec_res.next_states ] # Then diff --git a/src/tests/integration/proof/test_cell_map.py b/src/tests/integration/proof/test_cell_map.py index 02247d470..dd26354ca 100644 --- a/src/tests/integration/proof/test_cell_map.py +++ b/src/tests/integration/proof/test_cell_map.py @@ -104,10 +104,9 @@ def test_execute( expected_k, _, _ = expected_post # When - _, actual_depth, actual_post_term, _, _logs = kcfg_explore.cterm_execute( - self.config(kcfg_explore.kprint, k, aacounts, accounts), depth=depth - ) - actual_k = kcfg_explore.kprint.pretty_print(actual_post_term.cell('K_CELL')) + exec_res = kcfg_explore.cterm_execute(self.config(kcfg_explore.kprint, k, aacounts, accounts), depth=depth) + actual_k = kcfg_explore.kprint.pretty_print(exec_res.state.cell('K_CELL')) + actual_depth = exec_res.depth # Then assert actual_depth == expected_depth diff --git a/src/tests/integration/proof/test_imp.py b/src/tests/integration/proof/test_imp.py index dbd6b0869..d840b38ac 100644 --- a/src/tests/integration/proof/test_imp.py +++ b/src/tests/integration/proof/test_imp.py @@ -780,18 +780,17 @@ def test_execute( expected_k, expected_state = expected_post # When - _, actual_depth, actual_post_term, actual_next_terms, _logs = kcfg_explore.cterm_execute( - self.config(kcfg_explore.kprint, k, state), depth=depth - ) - actual_k = kcfg_explore.kprint.pretty_print(actual_post_term.cell('K_CELL')) - actual_state = kcfg_explore.kprint.pretty_print(actual_post_term.cell('STATE_CELL')) + exec_res = kcfg_explore.cterm_execute(self.config(kcfg_explore.kprint, k, state), depth=depth) + actual_k = kcfg_explore.kprint.pretty_print(exec_res.state.cell('K_CELL')) + actual_state = kcfg_explore.kprint.pretty_print(exec_res.state.cell('STATE_CELL')) + actual_depth = exec_res.depth actual_next_states = [ ( kcfg_explore.kprint.pretty_print(s.cell('K_CELL')), kcfg_explore.kprint.pretty_print(s.cell('STATE_CELL')), ) - for s in actual_next_terms + for s in exec_res.next_states ] # Then From 0e181c650a85e9e0940773a6589b0f7e5f24daaf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 11 Dec 2023 15:18:10 +0000 Subject: [PATCH 14/15] Reorder attributes --- src/pyk/kcfg/explore.py | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index 642bd6e69..22b19f792 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -48,10 +48,10 @@ class CTermExecute(NamedTuple): - vacuous: bool - depth: int state: CTerm next_states: tuple[CTerm, ...] + depth: int + vacuous: bool logs: tuple[LogEntry, ...] @@ -112,10 +112,10 @@ def cterm_execute( assert len(next_states) != 1 or response.reason is StopReason.CUT_POINT_RULE return CTermExecute( - vacuous=response.reason is StopReason.VACUOUS, - depth=response.depth, state=state, next_states=next_states, + depth=response.depth, + vacuous=response.reason is StopReason.VACUOUS, logs=response.logs, ) @@ -411,7 +411,7 @@ def extend_cterm( if len(branches) > 1: return Branch(branches, heuristic=True) - _is_vacuous, depth, cterm, next_cterms, next_node_logs = self.cterm_execute( + cterm, next_cterms, depth, vacuous, next_node_logs = self.cterm_execute( _cterm, depth=execute_depth, cut_point_rules=cut_point_rules, @@ -425,7 +425,7 @@ def extend_cterm( # Stuck or vacuous if not next_cterms: - if _is_vacuous: + if vacuous: return Vacuous() return Stuck() From 11268be263e4192f558470f64c4044d345665404 Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 11 Dec 2023 15:38:41 +0000 Subject: [PATCH 15/15] Set Version: 0.1.543 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 30cc14098..466fedc56 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.542 +0.1.543 diff --git a/pyproject.toml b/pyproject.toml index 3aaf7d337..6ef193834 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.542" +version = "0.1.543" description = "" authors = [ "Runtime Verification, Inc. ",