Merge remote-tracking branch 'origin/develop'

runtimeverification · Nov 27, 2024 · fb3a650 · fb3a650
2 parents 89a3ef5 + c15d153
commit fb3a650
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 4 deletions.
diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py
@@ -606,6 +606,7 @@ def log(message: str, *, warning: bool = False) -> None:
     def to_dict_no_nodes(self) -> dict[str, Any]:
         nodes = list(self._nodes.keys())
         edges = [edge.to_dict() for edge in self.edges()]
+        merged_edges = [merged_edge.to_dict() for merged_edge in self.merged_edges()]
         covers = [cover.to_dict() for cover in self.covers()]
         splits = [split.to_dict() for split in self.splits()]
         ndbranches = [ndbranch.to_dict() for ndbranch in self.ndbranches()]
@@ -616,6 +617,7 @@ def to_dict_no_nodes(self) -> dict[str, Any]:
             'next': self._node_id,
             'nodes': nodes,
             'edges': edges,
+            'merged_edges': merged_edges,
             'covers': covers,
             'splits': splits,
             'ndbranches': ndbranches,
@@ -758,11 +760,15 @@ def create_node(self, cterm: CTerm) -> KCFG.Node:
         return node
 
     def remove_node(self, node_id: NodeIdLike) -> None:
-        node_id = self._resolve(node_id)
+        self.remove_edges_around(node_id)
 
-        node = self._nodes.pop(node_id)
+        node_id = self._resolve(node_id)
+        self._nodes.pop(node_id)
+        self._deleted_nodes.add(node_id)
         self._created_nodes.discard(node_id)
-        self._deleted_nodes.add(node.id)
+
+    def remove_edges_around(self, node_id: NodeIdLike) -> None:
+        node_id = self._resolve(node_id)
 
         self._edges = {k: s for k, s in self._edges.items() if k != node_id and node_id not in s.target_ids}
         self._merged_edges = {

diff --git a/pyk/src/pyk/kcfg/minimize.py b/pyk/src/pyk/kcfg/minimize.py
@@ -229,7 +229,7 @@ def _is_mergeable(x: KCFG.Edge | KCFG.MergedEdge, y: KCFG.Edge | KCFG.MergedEdge
                     continue
                 for e in p:
                     # TODO: remove the split and edges, then safely remove the nodes.
-                    self.kcfg.remove_node(e.source.id)
+                    self.kcfg.remove_edges_around(e.source.id)
 
             # Create A -|MergedEdge|-> Merged_Bi -|Split|-> Bi, if one edge partition covers all the splits
             if len(edge_partitions) == 1: