Add parameter to advance_proof to split into subproofs after enough branches have been created

package/version

@@ -1 +1 @@
-0.1.445
+0.1.446

pyproject.toml

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

src/pyk/kcfg/kcfg.py

@@ -459,6 +459,8 @@ def create_node(self, cterm: CTerm) -> Node:
         term = cterm.kast
         term = remove_source_attributes(term)
         cterm = CTerm.from_kast(term)
+        while self._node_id in self._nodes:
+            self._node_id += 1
         node = KCFG.Node(self._node_id, cterm)
         self._node_id += 1
         self._nodes[node.id] = node

src/pyk/kcfg/show.py

@@ -282,6 +282,7 @@ def _sorted_init_nodes() -> tuple[list[KCFG.Node], list[KCFG.Node]]:
             return (init_nodes + init_leaf_nodes, remaining_nodes)
 
         init, _ = _sorted_init_nodes()
+
         while init:
             ret_lines.append(('unknown', ['']))
             _print_subgraph('', init[0], [])

src/pyk/proof/proof.py

@@ -182,6 +182,10 @@ def failed(self) -> bool:
     def passed(self) -> bool:
         return self.status == ProofStatus.PASSED
 
+    @property
+    def is_proof_pending(self) -> bool:
+        return self.status == ProofStatus.PENDING
+
     @property
     def dict(self) -> dict[str, Any]:
         return {

src/pyk/proof/reachability.py

@@ -3,7 +3,7 @@
 import json
 import logging
 from dataclasses import dataclass
-from typing import TYPE_CHECKING
+from typing import TYPE_CHECKING, Callable
 
 from pyk.kore.rpc import LogEntry
 
@@ -43,10 +43,12 @@ class APRProof(Proof, KCFGExploration):
     """
 
     node_refutations: dict[int, RefutationProof]  # TODO _node_refutatations
+    subproof_nodes: set[int]
     init: int
     target: int
     logs: dict[int, tuple[LogEntry, ...]]
     circularity: bool
+    generate_subproof_name: Callable[[APRProof, int], str] | None
     failure_info: APRFailureInfo | None
 
     def __init__(
@@ -58,10 +60,12 @@ def __init__(
         target: NodeIdLike,
         logs: dict[int, tuple[LogEntry, ...]],
         proof_dir: Path | None = None,
+        subproof_nodes: Iterable[int] | None = None,
         node_refutations: dict[int, str] | None = None,
         subproof_ids: Iterable[str] = (),
         circularity: bool = False,
         admitted: bool = False,
+        generate_subproof_name: Callable[[APRProof, int], str] | None = None,
     ):
         Proof.__init__(self, id, proof_dir=proof_dir, subproof_ids=subproof_ids, admitted=admitted)
         KCFGExploration.__init__(self, kcfg, terminal)
@@ -73,11 +77,14 @@ def __init__(
         self.circularity = circularity
         self.node_refutations = {}
         self.kcfg.cfg_dir = self.proof_subdir / 'kcfg' if self.proof_subdir else None
+        self.generate_subproof_name = generate_subproof_name
 
         if self.proof_dir is not None and self.proof_subdir is not None:
             ensure_dir_path(self.proof_dir)
             ensure_dir_path(self.proof_subdir)
 
+        self.subproof_nodes = set(subproof_nodes) if subproof_nodes is not None else set()
+
         if node_refutations is not None:
             refutations_not_in_subprroofs = set(node_refutations.values()).difference(
                 set(subproof_ids if subproof_ids else [])
@@ -103,11 +110,19 @@ def is_refuted(self, node_id: NodeIdLike) -> bool:
         return self.kcfg._resolve(node_id) in self.node_refutations.keys()
 
     def is_pending(self, node_id: NodeIdLike) -> bool:
-        return self.is_explorable(node_id) and not self.is_target(node_id) and not self.is_refuted(node_id)
+        return (
+            self.is_explorable(node_id)
+            and not self.is_target(node_id)
+            and not self.is_refuted(node_id)
+            and not self.is_subproof_node(node_id)
+        )
 
     def is_init(self, node_id: NodeIdLike) -> bool:
         return self.kcfg._resolve(node_id) == self.kcfg._resolve(self.init)
 
+    def is_subproof_node(self, node_id: NodeIdLike) -> bool:
+        return self.kcfg._resolve(node_id) in self.subproof_nodes
+
     def is_target(self, node_id: NodeIdLike) -> bool:
         return self.kcfg._resolve(node_id) == self.kcfg._resolve(self.target)
 
@@ -117,9 +132,13 @@ def is_failing(self, node_id: NodeIdLike) -> bool:
             and not self.is_explorable(node_id)
             and not self.is_target(node_id)
             and not self.is_refuted(node_id)
+            and not self.is_subproof_node(node_id)
             and not self.kcfg.is_vacuous(node_id)
         )
 
+    def add_subproof_node(self, node_id: int) -> None:
+        self.subproof_nodes.add(node_id)
+
     def shortest_path_to(self, node_id: NodeIdLike) -> tuple[KCFG.Successor, ...]:
         spb = self.kcfg.shortest_path_between(self.init, node_id)
         assert spb is not None
@@ -158,6 +177,7 @@ def from_dict(cls: type[APRProof], dct: Mapping[str, Any], proof_dir: Path | Non
         id = dct['id']
         circularity = dct.get('circularity', False)
         admitted = dct.get('admitted', False)
+        subproof_nodes = dct['subproof_nodes'] if 'subproof_nodes' in dct else []
         subproof_ids = dct['subproof_ids'] if 'subproof_ids' in dct else []
         node_refutations: dict[int, str] = {}
         if 'node_refutation' in dct:
@@ -177,6 +197,7 @@ def from_dict(cls: type[APRProof], dct: Mapping[str, Any], proof_dir: Path | Non
             circularity=circularity,
             admitted=admitted,
             proof_dir=proof_dir,
+            subproof_nodes=subproof_nodes,
             subproof_ids=subproof_ids,
             node_refutations=node_refutations,
         )
@@ -231,6 +252,7 @@ def dict(self) -> dict[str, Any]:
         dct['terminal'] = sorted(self._terminal)
         dct['init'] = self.init
         dct['target'] = self.target
+        dct['subproof_nodes'] = sorted(self.subproof_nodes)
         dct['node_refutations'] = {node_id: proof.id for (node_id, proof) in self.node_refutations.items()}
         dct['circularity'] = self.circularity
         logs = {int(k): [l.to_dict() for l in ls] for k, ls in self.logs.items()}
@@ -253,6 +275,7 @@ def summary(self) -> CompositeSummary:
                     len(self.kcfg.stuck),
                     len(self._terminal),
                     len(self.node_refutations),
+                    len(self.subproof_nodes),
                     len(self.subproof_ids),
                 ),
                 *subproofs_summaries,
@@ -271,6 +294,7 @@ def read_proof_data(proof_dir: Path, id: str) -> APRProof:
         kcfg = KCFG.read_cfg_data(cfg_dir, id)
         init = int(proof_dict['init'])
         target = int(proof_dict['target'])
+        subproof_nodes = proof_dict['subproof_nodes']
         circularity = bool(proof_dict['circularity'])
         admitted = bool(proof_dict['admitted'])
         terminal = proof_dict['terminal']
@@ -284,6 +308,7 @@ def read_proof_data(proof_dir: Path, id: str) -> APRProof:
             terminal=terminal,
             init=init,
             target=target,
+            subproof_nodes=subproof_nodes,
             logs=logs,
             circularity=circularity,
             admitted=admitted,
@@ -307,6 +332,7 @@ def write_proof_data(self) -> None:
         dct['type'] = 'APRProof'
         dct['init'] = self.kcfg._resolve(self.init)
         dct['target'] = self.kcfg._resolve(self.target)
+        dct['subproof_nodes'] = sorted(self.subproof_nodes)
         dct['terminal'] = sorted(self._terminal)
         dct['node_refutations'] = {
             self.kcfg._resolve(node_id): proof.id for (node_id, proof) in self.node_refutations.items()
@@ -337,6 +363,7 @@ def __init__(
         bmc_depth: int,
         bounded: Iterable[int] | None = None,
         proof_dir: Path | None = None,
+        subproof_nodes: Iterable[int] | None = None,
         subproof_ids: Iterable[str] = (),
         node_refutations: dict[int, str] | None = None,
         circularity: bool = False,
@@ -350,6 +377,7 @@ def __init__(
             target,
             logs,
             proof_dir=proof_dir,
+            subproof_nodes=subproof_nodes,
             subproof_ids=subproof_ids,
             node_refutations=node_refutations,
             circularity=circularity,
@@ -367,6 +395,7 @@ def read_proof_data(proof_dir: Path, id: str) -> APRBMCProof:
         kcfg = KCFG.read_cfg_data(cfg_dir, id)
         init = int(proof_dict['init'])
         target = int(proof_dict['target'])
+        subproof_nodes = proof_dict['subproof_nodes']
         circularity = bool(proof_dict['circularity'])
         terminal = proof_dict['terminal']
         admitted = bool(proof_dict['admitted'])
@@ -382,6 +411,7 @@ def read_proof_data(proof_dir: Path, id: str) -> APRBMCProof:
             terminal=terminal,
             init=init,
             target=target,
+            subproof_nodes=subproof_nodes,
             logs=logs,
             circularity=circularity,
             admitted=admitted,
@@ -407,6 +437,7 @@ def write_proof_data(self) -> None:
         dct['type'] = 'APRBMCProof'
         dct['init'] = self.kcfg._resolve(self.init)
         dct['target'] = self.kcfg._resolve(self.target)
+        dct['subproof_nodes'] = sorted(self.subproof_nodes)
         dct['node_refutations'] = {
             self.kcfg._resolve(node_id): proof.id for (node_id, proof) in self.node_refutations.items()
         }
@@ -522,6 +553,7 @@ def summary(self) -> CompositeSummary:
                     len(self.kcfg.stuck),
                     len(self._terminal),
                     len(self.node_refutations),
+                    len(self.subproof_nodes),
                     len(self._bounded),
                     len(self.subproof_ids),
                 ),
@@ -635,13 +667,23 @@ def advance_proof(
         cut_point_rules: Iterable[str] = (),
         terminal_rules: Iterable[str] = (),
         fail_fast: bool = False,
+        max_branches: int | None = None,
     ) -> None:
         iterations = 0
 
         self._check_all_terminals()
 
         while self.proof.pending:
             self.proof.write_proof_data()
+
+            if max_branches is not None and len(self.proof.pending) > max_branches:
+                _LOGGER.info(
+                    f'Reached max_branches={max_branches} bound on number of pending nodes. Nodes {self.proof.pending} will be turned into subproofs.'
+                )
+                for pending_node in self.proof.pending:
+                    self.delegate_to_subproof(pending_node)
+                break
+
             if fail_fast and self.proof.failed:
                 _LOGGER.warning(
                     f'Terminating proof early because fail_fast is set {self.proof.id}, failing nodes: {[nd.id for nd in self.proof.failing]}'
@@ -672,6 +714,38 @@ def advance_proof(
 
         self.proof.write_proof_data()
 
+    def delegate_to_subproof(self, node: KCFG.Node) -> None:
+        _LOGGER.info(f'Delegating node {node.id} to a new proof.')
+        subproof = self.construct_node_subproof(node)
+        self.proof.add_subproof(subproof)
+        self.proof.add_subproof_node(node.id)
+
+    def construct_node_subproof(self, node: KCFG.Node) -> APRProof:
+        kcfg = KCFG(self.proof.proof_dir)
+        target_node = self.proof.kcfg.node(self.proof.target)
+
+        node_cterm, _ = self.kcfg_explore.cterm_simplify(node.cterm)
+        (
+            target_node_cterm,
+            _,
+        ) = self.kcfg_explore.cterm_simplify(target_node.cterm)
+
+        new_init = kcfg.create_node(node_cterm)
+        new_target = kcfg.create_node(target_node_cterm)
+
+        assert self.proof.generate_subproof_name is not None
+
+        return APRProof(
+            id=self.proof.generate_subproof_name(self.proof, node.id),
+            kcfg=kcfg,
+            terminal=[],
+            init=new_init.id,
+            target=new_target.id,
+            logs={},
+            proof_dir=self.proof.proof_dir,
+            generate_subproof_name=self.proof.generate_subproof_name,
+        )
+
     def refute_node(self, node: KCFG.Node) -> RefutationProof | None:
         _LOGGER.info(f'Attempting to refute node {node.id}')
         refutation = self.construct_node_refutation(node)
@@ -757,6 +831,7 @@ class APRSummary(ProofSummary):
     stuck: int
     terminal: int
     refuted: int
+    subproof_nodes: int
     subproofs: int
 
     @property
@@ -772,6 +847,7 @@ def lines(self) -> list[str]:
             f'    stuck: {self.stuck}',
             f'    terminal: {self.terminal}',
             f'    refuted: {self.refuted}',
+            f'    subproof_nodes: {self.subproof_nodes}',
             f'Subproofs: {self.subproofs}',
         ]
 
@@ -935,6 +1011,7 @@ class APRBMCSummary(ProofSummary):
     stuck: int
     terminal: int
     refuted: int
+    subproof_nodes: int
     bounded: int
     subproofs: int
 
@@ -950,6 +1027,7 @@ def lines(self) -> list[str]:
             f'    stuck: {self.stuck}',
             f'    terminal: {self.terminal}',
             f'    refuted: {self.refuted}',
+            f'    subproof_nodes: {self.subproof_nodes}',
             f'    bounded: {self.bounded}',
             f'Subproofs: {self.subproofs}',
         ]

src/pyk/proof/show.py

@@ -36,6 +36,8 @@ def node_attrs(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
             attrs.append('target')
         if self.proof.is_pending(node.id):
             attrs.append('pending')
+        if self.proof.is_subproof_node(node.id):
+            attrs.append('subproof')
         if self.proof.is_terminal(node.id):
             attrs.append('terminal')
             if 'stuck' in attrs:

src/tests/integration/kcfg/test_imp.py

@@ -1242,6 +1242,40 @@ def test_anti_unify_forget_values(
 
         assert anti_unifier.kast == expected_anti_unifier.kast
 
+    def test_delegate_to_subproof(
+        self,
+        kcfg_explore: KCFGExplore,
+        proof_dir: Path,
+        kprove: KProve,
+    ) -> None:
+        claim = single(
+            kprove.get_claims(
+                K_FILES / 'imp-simple-spec.k',
+                spec_module_name='IMP-SIMPLE-SPEC',
+                claim_labels=['IMP-SIMPLE-SPEC.failing-if'],
+            )
+        )
+
+        proof = APRProof.from_claim(
+            kprove.definition,
+            claim,
+            logs={},
+            proof_dir=proof_dir,
+        )
+
+        prover = APRProver(
+            proof,
+            kcfg_explore=kcfg_explore,
+        )
+
+        assert len(list(proof.subproofs)) == 0
+        assert len(proof.pending) == 1
+
+        prover.advance_proof(max_branches=1)
+
+        assert len(list(proof.subproofs)) == 2
+        assert len(proof.pending) == 0
+
     def test_anti_unify_keep_values(
         self,
         kcfg_explore: KCFGExplore,