From a2b5a76d0f3607227f0e63d3019851c8a227a19c Mon Sep 17 00:00:00 2001 From: Noah Watson <107630091+nwatson22@users.noreply.github.com> Date: Wed, 7 Aug 2024 03:00:40 -0500 Subject: [PATCH] Status bar improvements (#4575) - Adds the number of refuted nodes to the proof status bar. - Adds a separator which separates the one line summary into 3 parts, one which is the proof status, one to do with structure, and one to do with status of the leaves. - Changes the definition of `branches` to mean "how many `Split` and `NDBranch` targets are there?" instead of "how many `Split`s and `NDBranch`es are there?" to more accurately reflect the degree of branching in a proof. --- pyk/src/pyk/proof/reachability.py | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 53b1b26e586..fab28f6cc60 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -507,14 +507,17 @@ def one_line_summary(self) -> str: nodes = len(self.kcfg.nodes) pending = len(self.pending) failing = len(self.failing) - branches = len(self.kcfg.ndbranches()) + len(self.kcfg.splits()) + branches = 0 + for branch in self.kcfg.ndbranches() + self.kcfg.splits(): + branches += len(branch.targets) vacuous = len(self.kcfg.vacuous) terminal = len(self.terminal) stuck = len(self.kcfg.stuck) passed = len([cover for cover in self.kcfg.covers() if cover.target.id == self.target]) + refuted = len(self.node_refutations) return ( super().one_line_summary - + f'|{nodes} nodes|{pending} pending|{passed} passed|{failing} failing|{branches} branches|{vacuous} vacuous|{terminal} terminal|{stuck} stuck' + + f' --- {nodes} nodes|{branches} branches|{terminal} terminal --- {pending} pending|{passed} passed|{failing} failing|{vacuous} vacuous|{refuted} refuted|{stuck} stuck' ) def get_refutation_id(self, node_id: int) -> str: