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.

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

support write MergedEdge during proof #4689

Closed
wants to merge 6 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
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
24 changes: 22 additions & 2 deletions pyk/src/pyk/kcfg/kcfg.py
Original file line number Diff line number Diff line change
Expand Up @@ -264,18 +264,36 @@ class MergedEdge(EdgeLike):
edges: tuple[KCFG.Edge, ...]

def to_dict(self) -> dict[str, Any]:

def _merged_edge_to_dict(edge: KCFG.Edge) -> dict[str, Any]:
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
def _merged_edge_to_dict(edge: KCFG.Edge) -> dict[str, Any]:
def merged_edge_to_dict(edge: KCFG.Edge) -> dict[str, Any]:

(The functions is only visible from to_dict anyways.)

return {
'source': edge.source.to_dict(),
'target': edge.target.to_dict(),
'depth': edge.depth,
'rules': list(edge.rules),
}

return {
'source': self.source.id,
'target': self.target.id,
'edges': [edge.to_dict() for edge in self.edges],
'edges': [_merged_edge_to_dict(e) for e in self.edges],
}

@staticmethod
def from_dict(dct: dict[str, Any], nodes: Mapping[int, KCFG.Node]) -> KCFG.Successor:

def _merged_edge_from_dict(dct: dict[str, Any]) -> KCFG.Edge:
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
def _merged_edge_from_dict(dct: dict[str, Any]) -> KCFG.Edge:
def merged_edge_from_dict(dct: dict[str, Any]) -> KCFG.Edge:

return KCFG.Edge(
KCFG.Node.from_dict(dct['source']),
KCFG.Node.from_dict(dct['target']),
dct['depth'],
tuple(dct['rules']),
)

return KCFG.MergedEdge(
nodes[dct['source']],
nodes[dct['target']],
tuple(KCFG.Edge.from_dict(edge, nodes) for edge in dct['edges']),
tuple(_merged_edge_from_dict(e) for e in dct['edges']),
)

def replace_source(self, node: KCFG.Node) -> KCFG.Successor:
Expand Down Expand Up @@ -606,6 +624,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()]
Expand All @@ -616,6 +635,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,
Expand Down
12 changes: 11 additions & 1 deletion pyk/src/tests/unit/test_kcfg.py
Original file line number Diff line number Diff line change
Expand Up @@ -113,9 +113,19 @@ def _make_edge_dict(i: int, j: int, depth: int = 1, rules: tuple[str, ...] = ())


def merged_edge_dicts(*merged_edges: Iterable) -> list[dict[str, Any]]:
def _make_edge_dicts(*edges: Iterable) -> list[dict[str, Any]]:
def _make_edge_dict(i: int, j: int, depth: int = 1, rules: tuple[str, ...] = ()) -> dict[str, Any]:
Comment on lines +116 to +117
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These two functions can be on the same level.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
def _make_edge_dicts(*edges: Iterable) -> list[dict[str, Any]]:
def _make_edge_dict(i: int, j: int, depth: int = 1, rules: tuple[str, ...] = ()) -> dict[str, Any]:
def make_edge_dicts(*edges: Iterable) -> list[dict[str, Any]]:
def make_edge_dict(i: int, j: int, depth: int = 1, rules: tuple[str, ...] = ()) -> dict[str, Any]:

return {
'source': node_dicts(1, start=i)[0],
'target': node_dicts(1, start=j)[0],
'depth': depth,
'rules': list(rules),
}

return [_make_edge_dict(*edge) for edge in edges]

def _make_merged_edge_dict(s: int, t: int, *edges: Iterable) -> dict[str, Any]:
return {'source': s, 'target': t, 'edges': edge_dicts(*edges)}
return {'source': s, 'target': t, 'edges': _make_edge_dicts(*edges)}

return [_make_merged_edge_dict(*merged_edge) for merged_edge in merged_edges]

Expand Down
Loading