diff --git a/docs/conf.py b/docs/conf.py index f5e7bca76..683a6c0a9 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -9,8 +9,8 @@ project = 'pyk' author = 'Runtime Verification, Inc' copyright = '2024, Runtime Verification, Inc' -version = '0.1.622' -release = '0.1.622' +version = '0.1.623' +release = '0.1.623' # -- General configuration --------------------------------------------------- # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration diff --git a/package/version b/package/version index a502218f6..cc5737c83 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.622 +0.1.623 diff --git a/pyproject.toml b/pyproject.toml index 0bde8c37b..c701d7d49 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.622" +version = "0.1.623" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 818ca5af3..e4812847a 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -198,7 +198,9 @@ def from_dict(cls: type[APRProof], dct: Mapping[str, Any], proof_dir: Path | Non subproof_ids = dct['subproof_ids'] if 'subproof_ids' in dct else [] node_refutations: dict[int, str] = {} if 'node_refutation' in dct: - node_refutations = {kcfg._resolve(node_id): proof_id for (node_id, proof_id) in dct['node_refutations']} + node_refutations = { + kcfg._resolve(int(node_id)): proof_id for node_id, proof_id in dct['node_refutations'].items() + } if 'logs' in dct: logs = {int(k): tuple(LogEntry.from_dict(l) for l in ls) for k, ls in dct['logs'].items()} else: @@ -404,7 +406,9 @@ def read_proof_data(proof_dir: Path, id: str) -> APRProof: terminal = proof_dict['terminal'] logs = {int(k): tuple(LogEntry.from_dict(l) for l in ls) for k, ls in proof_dict['logs'].items()} subproof_ids = proof_dict['subproof_ids'] - node_refutations = {kcfg._resolve(node_id): proof_id for (node_id, proof_id) in proof_dict['node_refutations']} + node_refutations = { + kcfg._resolve(int(node_id)): proof_id for node_id, proof_id in proof_dict['node_refutations'].items() + } return APRProof( id=id, @@ -474,6 +478,10 @@ def unrefute_node(self, node: KCFG.Node) -> None: _LOGGER.info(f'Disabled refutation of node {node.id}.') def construct_node_refutation(self, node: KCFG.Node) -> RefutationProof | None: # TODO put into prover class + if len(self.kcfg.successors(node.id)) > 0: + _LOGGER.error(f'Cannot refute node {node.id} that already has successors') + return None + path = single(self.kcfg.paths_between(source_id=self.init, target_id=node.id)) branches_on_path = list(filter(lambda x: type(x) is KCFG.Split or type(x) is KCFG.NDBranch, reversed(path))) if len(branches_on_path) == 0: diff --git a/src/pyk/proof/show.py b/src/pyk/proof/show.py index 5564e8d6e..31a990939 100644 --- a/src/pyk/proof/show.py +++ b/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_refuted(node.id): + attrs.append('refuted') if self.proof.is_terminal(node.id): attrs.append('terminal') if 'stuck' in attrs: