From bb49b6d663717a6fbe6ffb5011183d13c320e837 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Tue, 13 Aug 2024 15:11:58 -0500 Subject: [PATCH 1/3] Remove extra unnecessary call to nonzero_depth, short-circuit traversal in most cases --- pyk/src/pyk/kcfg/kcfg.py | 7 +++++++ pyk/src/pyk/proof/reachability.py | 5 +++-- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index d3f9247e49f..6316b43ce24 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -1188,6 +1188,13 @@ def shortest_distance_between(self, node_1_id: NodeIdLike, node_2_id: NodeIdLike return distance def zero_depth_between(self, node_1_id: NodeIdLike, node_2_id: NodeIdLike) -> bool: + # Short-circuit and don't run pathing algorithm if there is no 0 length path on the first step. + node_1_successors = self.successors(node_1_id) + node_2_successors = self.successors(node_2_id) + path_lengths = [self.path_length([successor]) for successor in node_1_successors + node_2_successors] + if 0 not in path_lengths: + return False + shortest_distance = self.shortest_distance_between(node_1_id, node_2_id) return shortest_distance is not None and shortest_distance == 0 diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 2a62fe37f5b..58c9bb24df0 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -167,7 +167,8 @@ def get_steps(self) -> list[APRProofStep]: else: shortest_path.append(succ.source) - module_name = self.circularities_module_name if self.nonzero_depth(node) else self.dependencies_module_name + nonzero_depth = self.nonzero_depth(node) + module_name = self.circularities_module_name if nonzero_depth else self.dependencies_module_name steps.append( APRProofStep( @@ -179,7 +180,7 @@ def get_steps(self) -> list[APRProofStep]: shortest_path_to_node=tuple(shortest_path), prior_loops_cache=FrozenDict(self.prior_loops_cache), circularity=self.circularity, - nonzero_depth=self.nonzero_depth(node), + nonzero_depth=nonzero_depth, circularity_rule_id=f'{self.rule_id}-{self.init}-TO-{self.target}', ) ) From 705688b4c704164acec4865232fda66d3241ad7e Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Tue, 13 Aug 2024 17:01:27 -0500 Subject: [PATCH 2/3] Fix edge case where nodes are the same node --- pyk/src/pyk/kcfg/kcfg.py | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 6316b43ce24..8b0ddba0237 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -1188,14 +1188,19 @@ def shortest_distance_between(self, node_1_id: NodeIdLike, node_2_id: NodeIdLike return distance def zero_depth_between(self, node_1_id: NodeIdLike, node_2_id: NodeIdLike) -> bool: + _node_1_id = self._resolve(node_1_id) + _node_2_id = self._resolve(node_2_id) + if _node_1_id == _node_2_id: + return True # Short-circuit and don't run pathing algorithm if there is no 0 length path on the first step. - node_1_successors = self.successors(node_1_id) - node_2_successors = self.successors(node_2_id) + node_1_successors = self.successors(_node_1_id) + node_2_successors = self.successors(_node_2_id) path_lengths = [self.path_length([successor]) for successor in node_1_successors + node_2_successors] if 0 not in path_lengths: return False - shortest_distance = self.shortest_distance_between(node_1_id, node_2_id) + shortest_distance = self.shortest_distance_between(_node_1_id, _node_2_id) + return shortest_distance is not None and shortest_distance == 0 def paths_between(self, source_id: NodeIdLike, target_id: NodeIdLike) -> list[tuple[Successor, ...]]: From ffb6b5f5f202598c1b5ea97343a9f0c36a713fbb Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 14 Aug 2024 11:02:37 -0500 Subject: [PATCH 3/3] Clean up --- pyk/src/pyk/kcfg/kcfg.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 8b0ddba0237..835aea290c5 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -1193,9 +1193,9 @@ def zero_depth_between(self, node_1_id: NodeIdLike, node_2_id: NodeIdLike) -> bo if _node_1_id == _node_2_id: return True # Short-circuit and don't run pathing algorithm if there is no 0 length path on the first step. - node_1_successors = self.successors(_node_1_id) - node_2_successors = self.successors(_node_2_id) - path_lengths = [self.path_length([successor]) for successor in node_1_successors + node_2_successors] + path_lengths = [ + self.path_length([successor]) for successor in self.successors(_node_1_id) + self.successors(_node_2_id) + ] if 0 not in path_lengths: return False