Skip to content
This repository was archived by the owner on Apr 25, 2024. It is now read-only.

Commit 2a28e9f

Browse files
committed
kcfg/kcfg: implement KCFG.pullback_covers which minimizes covers
1 parent 312cc67 commit 2a28e9f

File tree

1 file changed

+12
-0
lines changed

1 file changed

+12
-0
lines changed

src/pyk/kcfg/kcfg.py

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -659,6 +659,18 @@ def create_merge(self, node_ids: Iterable[NodeIdLike]) -> NodeIdLike:
659659
self.create_cover(nid, new_node.id)
660660
return new_node.id
661661

662+
def pullback_covers(self, target_id: NodeIdLike) -> tuple[list[NodeIdLike], NodeIdLike] | None:
663+
covers = self.covers(target_id=target_id)
664+
source_ids: list[NodeIdLike] = [cover.source.id for cover in covers]
665+
if len(source_ids) < 2:
666+
return None
667+
merge_id = self.create_merge(source_ids)
668+
for cover in covers:
669+
self.remove_cover(cover.source.id, target_id)
670+
self.create_cover(cover.source.id, merge_id)
671+
self.create_cover(merge_id, target_id)
672+
return source_ids, merge_id
673+
662674
def ndbranches(self, *, source_id: NodeIdLike | None = None, target_id: NodeIdLike | None = None) -> list[NDBranch]:
663675
source_id = self._resolve(source_id) if source_id is not None else None
664676
target_id = self._resolve(target_id) if target_id is not None else None

0 commit comments

Comments
 (0)