Node attribute storage in nodes (runtimeverification/pyk#1002)

Fixes: runtimeverification/pyk#965

Stores node attributes `terminal`,`stuck`, and `vacuous` in nodes rather
than in KCFG or KCFGExploration.
- adds `attr` field to KCFG.Node
- adds enums `NodeAttr` (base), `KCFGNodeAttr`, and
`KCFGExplorationNodeAttr`
- adds `add_attr`, `remove_attr`, and `discard_attr` to kcfg for
updating the attrs of a given node, which replaces the node with a new
one, since nodes are immutable.
- `replace_node` now takes a node. `let_node` is now for updating
specific fields of nodes.
- Checks `terminal`, `stuck`, and `vacuous` by reference to the
attributes on the node
- Removes separate `terminal`, `stuck` and `vacuous` lists.
- `from_dict` and `to_dict` on `Node` and `KCFG` updated to store
relevant attributes in the node dicts. `KCFGStore` translates to and
from the existing on-disk format.
- Tests in `test_proof.py` previously using `read_proof` and
`write_proof` are now using `read_proof_data` and `write_proof_data`,
since the older way of reading and writing does not use the `KCFGStore`
and relies on `KCFG.to_dict` directly, without the translation.

---------

Co-authored-by: devops <[email protected]>

Author: nwatson22

pyk/docs/conf.py

@@ -9,8 +9,8 @@
 project = 'pyk'
 author = 'Runtime Verification, Inc'
 copyright = '2024, Runtime Verification, Inc'
-version = '0.1.756'
-release = '0.1.756'
+version = '0.1.757'
+release = '0.1.757'
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

pyk/package/version

@@ -1 +1 @@
-0.1.756
+0.1.757

pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.756"
+version = "0.1.757"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

pyk/src/pyk/kcfg/exploration.py

@@ -2,7 +2,7 @@
 
 from typing import TYPE_CHECKING
 
-from pyk.kcfg.kcfg import KCFG
+from pyk.kcfg.kcfg import KCFG, NodeAttr
 
 if TYPE_CHECKING:
     from collections.abc import Iterable, Mapping
@@ -11,21 +11,30 @@
     from pyk.kcfg.kcfg import NodeIdLike
 
 
+class KCFGExplorationNodeAttr(NodeAttr):
+    TERMINAL = NodeAttr('terminal')
+
+
 class KCFGExploration:
     kcfg: KCFG
-    _terminal: set[int]
 
     def __init__(self, kcfg: KCFG, terminal: Iterable[NodeIdLike] | None = None) -> None:
         self.kcfg = kcfg
-        self._terminal = {kcfg._resolve(node_id) for node_id in terminal} if terminal is not None else set()
+        if terminal:
+            for node_id in terminal:
+                self.add_terminal(node_id)
+
+    @property
+    def terminal_ids(self) -> set[int]:
+        return {node.id for node in self.kcfg.nodes if KCFGExplorationNodeAttr.TERMINAL in node.attrs}
 
     #
     # Recognisers
     #
 
     # Terminal node recogniser
     def is_terminal(self, node_id: NodeIdLike) -> bool:
-        return self.kcfg._resolve(node_id) in self._terminal
+        return KCFGExplorationNodeAttr.TERMINAL in self.kcfg.node(node_id).attrs
 
     # Explorable node recogniser
     def is_explorable(self, node_id: NodeIdLike) -> bool:
@@ -56,11 +65,11 @@ def explorable(self) -> list[KCFG.Node]:
 
     # Marking a given node as terminal
     def add_terminal(self, node_id: NodeIdLike) -> None:
-        self._terminal.add(self.kcfg._resolve(node_id))
+        self.kcfg.add_attr(node_id, KCFGExplorationNodeAttr.TERMINAL)
 
     # Unmarking a given node as terminal
     def remove_terminal(self, node_id: int) -> None:
-        self._terminal.discard(node_id)
+        self.kcfg.remove_attr(node_id, KCFGExplorationNodeAttr.TERMINAL)
 
     #
     # Lifted KCFG functions that may affect terminal nodes
@@ -70,14 +79,10 @@ def remove_terminal(self, node_id: int) -> None:
     def remove_node(self, node_id: NodeIdLike) -> None:
         node_id = self.kcfg._resolve(node_id)
         self.kcfg.remove_node(node_id)
-        self.remove_terminal(node_id)
 
     # Pruning a KCFG subtree starting from a given node
     def prune(self, node_id: NodeIdLike, keep_nodes: Iterable[NodeIdLike] = ()) -> list[int]:
-        pruned_nodes = self.kcfg.prune(node_id, keep_nodes=keep_nodes)
-        for node_id in pruned_nodes:
-            self.remove_terminal(node_id)
-        return pruned_nodes
+        return self.kcfg.prune(node_id, keep_nodes=keep_nodes)
 
     #
     # Dictionarisation
@@ -95,7 +100,7 @@ def from_dict(dct: Mapping[str, Any]) -> KCFGExploration:
     def to_dict(self) -> dict[str, Any]:
         dct: dict[str, Any] = {}
         dct['kcfg'] = self.kcfg.to_dict()
-        dct['terminal'] = sorted(self._terminal)
+        dct['terminal'] = sorted(node.id for node in self.kcfg.nodes if self.is_terminal(node.id))
         return dct
 
     #
@@ -105,4 +110,3 @@ def to_dict(self) -> dict[str, Any]:
     # Minimizing the KCFG
     def minimize_kcfg(self) -> None:
         self.kcfg.minimize()
-        self._terminal = self._terminal.difference(self.kcfg._deleted_nodes)

pyk/src/pyk/kcfg/explore.py

@@ -116,7 +116,7 @@ def simplify(self, cfg: KCFG, logs: dict[int, tuple[LogEntry, ...]]) -> None:
             _LOGGER.info(f'Simplifying node {self.id}: {shorten_hashes(node.id)}')
             new_term, next_node_logs = self.cterm_symbolic.simplify(node.cterm)
             if new_term != node.cterm:
-                cfg.replace_node(node.id, new_term)
+                cfg.let_node(node.id, cterm=new_term)
                 if node.id in logs:
                     logs[node.id] += next_node_logs
                 else: