Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

APRProof get_steps optimizations #4585

Merged
merged 6 commits into from
Aug 14, 2024
+16 −3
Merged

APRProof get_steps optimizations #4585

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
bb49b6d
Remove extra unnecessary call to nonzero_depth, short-circuit travers…
nwatson22 Aug 13, 2024
705688b
Fix edge case where nodes are the same node
nwatson22 Aug 13, 2024
df2ea88
Merge branch 'develop' into noah/zero-depth-optimization
nwatson22 Aug 14, 2024
ffb6b5f
Clean up
nwatson22 Aug 14, 2024
55098ae
Merge branch 'noah/zero-depth-optimization' of https://github.com/run…
nwatson22 Aug 14, 2024
d792bf4
Merge branch 'develop' into noah/zero-depth-optimization
PetarMax Aug 14, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 13 additions & 1 deletion pyk/src/pyk/kcfg/kcfg.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1188,7 +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:
shortest_distance = self.shortest_distance_between(node_1_id, node_2_id)
_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.
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

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, ...]]:
Expand Down
5 changes: 3 additions & 2 deletions pyk/src/pyk/proof/reachability.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand All @@ -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}',
)
)
Expand Down
Loading