support vacuous in ARPBMCProof and update Proof summaries

Author: anvacaru

src/pyk/proof/reachability.py

@@ -273,6 +273,7 @@ def summary(self) -> CompositeSummary:
                     len(self.kcfg.nodes),
                     len(self.pending),
                     len(self.failing),
+                    len(self.kcfg.vacuous),
                     len(self.kcfg.stuck),
                     len(self.terminal),
                     len(self.node_refutations),
@@ -448,12 +449,17 @@ def is_bounded(self, node_id: NodeIdLike) -> bool:
 
     def is_failing(self, node_id: NodeIdLike) -> bool:
         return self.kcfg.is_leaf(node_id) and not (
-            self.is_pending(node_id) or self.is_target(node_id) or self.is_refuted(node_id) or self.is_bounded(node_id)
+            self.is_pending(node_id)
+            or self.is_target(node_id)
+            or self.is_refuted(node_id)
+            or self.is_bounded(node_id)
+            or self.kcfg.is_vacuous(node_id)
         )
 
     def is_pending(self, node_id: NodeIdLike) -> bool:
         return self.kcfg.is_leaf(node_id) and not (
             self.is_terminal(node_id)
+            or self.kcfg.is_vacuous(node_id)
             or self.kcfg.is_stuck(node_id)
             or self.is_bounded(node_id)
             or self.is_target(node_id)
@@ -543,6 +549,7 @@ def summary(self) -> CompositeSummary:
                     len(self.kcfg.nodes),
                     len(self.pending),
                     len(self.failing),
+                    len(self.kcfg.vacuous),
                     len(self.kcfg.stuck),
                     len(self.terminal),
                     len(self.node_refutations),
@@ -759,6 +766,7 @@ class APRSummary(ProofSummary):
     nodes: int
     pending: int
     failing: int
+    vacuous: int
     stuck: int
     terminal: int
     refuted: int
@@ -773,6 +781,7 @@ def lines(self) -> list[str]:
             f'    nodes: {self.nodes}',
             f'    pending: {self.pending}',
             f'    failing: {self.failing}',
+            f'    vacuous: {self.vacuous}',
             f'    stuck: {self.stuck}',
             f'    terminal: {self.terminal}',
             f'    refuted: {self.refuted}',
@@ -897,6 +906,7 @@ class APRBMCSummary(ProofSummary):
     nodes: int
     pending: int
     failing: int
+    vacuous: int
     stuck: int
     terminal: int
     refuted: int
@@ -911,6 +921,7 @@ def lines(self) -> list[str]:
             f'    nodes: {self.nodes}',
             f'    pending: {self.pending}',
             f'    failing: {self.failing}',
+            f'    vacuous: {self.vacuous}',
             f'    stuck: {self.stuck}',
             f'    terminal: {self.terminal}',
             f'    refuted: {self.refuted}',

src/tests/unit/test_proof.py

@@ -321,6 +321,7 @@ def test_apr_proof_summary(proof_dir: Path) -> None:
                 nodes=1,
                 pending=0,
                 failing=0,
+                vacuous=0,
                 stuck=0,
                 terminal=0,
                 refuted=0,
@@ -343,6 +344,7 @@ def test_aprbmc_proof_summary(proof_dir: Path) -> None:
                 nodes=1,
                 pending=0,
                 failing=0,
+                vacuous=0,
                 stuck=0,
                 terminal=0,
                 refuted=0,
@@ -379,6 +381,7 @@ def test_apr_proof_summary_subproofs(proof_dir: Path) -> None:
         nodes=1,
         pending=0,
         failing=0,
+        vacuous=0,
         stuck=0,
         terminal=0,
         refuted=0,
@@ -394,6 +397,7 @@ def test_apr_proof_summary_subproofs(proof_dir: Path) -> None:
                 nodes=2,
                 pending=1,
                 failing=0,
+                vacuous=0,
                 stuck=0,
                 terminal=0,
                 refuted=0,