Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add variable_names_mapping to APRProof, counterexample generation #4574

Closed
wants to merge 3 commits into from
Closed

Add variable_names_mapping to APRProof, counterexample generation #4574

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
87036cd
Add `variable_names_mapping` to `APRProof`, counterexample generation
palinatolmach Aug 6, 2024
2085e40
Merge branch 'develop' into map-input-names
palinatolmach Aug 22, 2024
6729100
Merge branch 'develop' into map-input-names
palinatolmach Aug 29, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 13 additions & 1 deletion pyk/src/pyk/proof/reachability.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -114,6 +114,7 @@ class APRProof(Proof[APRProofStep, APRProofResult], KCFGExploration):
_exec_time: float
error_info: Exception | None
prior_loops_cache: dict[int, tuple[int, ...]]
variable_names_mapping: dict[str, str] | None

_checked_for_bounded: set[int]
_next_steps: dict[NodeIdLike, KCFGExtendResult]
Expand All @@ -136,6 +137,7 @@ def __init__(
_exec_time: float = 0,
error_info: Exception | None = None,
prior_loops_cache: dict[int, tuple[int, ...]] | None = None,
variable_names_mapping: dict[str, str] | None = None,
):
Proof.__init__(self, id, proof_dir=proof_dir, subproof_ids=subproof_ids, admitted=admitted)
KCFGExploration.__init__(self, kcfg, terminal)
Expand All @@ -152,6 +154,7 @@ def __init__(
self.kcfg._kcfg_store = KCFGStore(self.proof_subdir / 'kcfg') if self.proof_subdir else None
self._exec_time = _exec_time
self.error_info = error_info
self.variable_names_mapping = variable_names_mapping

self._checked_for_bounded = set()
self._next_steps = {}
Expand Down Expand Up @@ -582,6 +585,7 @@ 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']
variable_names_mapping = proof_dict.get('variable_names_mapping', None)
node_refutations = {
kcfg._resolve(int(node_id)): proof_id for node_id, proof_id in proof_dict['node_refutations'].items()
}
Expand All @@ -604,6 +608,7 @@ def read_proof_data(proof_dir: Path, id: str) -> APRProof:
node_refutations=node_refutations,
prior_loops_cache=prior_loops_cache,
_exec_time=exec_time,
variable_names_mapping=variable_names_mapping,
)

def write_proof_data(self) -> None:
Expand Down Expand Up @@ -636,6 +641,8 @@ def write_proof_data(self) -> None:

dct['loops_cache'] = self.prior_loops_cache

dct['variable_names_mapping'] = self.variable_names_mapping

proof_json.write_text(json.dumps(dct))
_LOGGER.info(f'Wrote proof data for {self.id}: {proof_json}')
self.kcfg.write_cfg_data()
Expand Down Expand Up @@ -971,7 +978,12 @@ def from_proof(
for var, term in model_subst.to_dict().items():
term_kast = KInner.from_dict(term)
term_pretty = kcfg_explore.pretty_print(term_kast)
model.append((var, term_pretty))
var_name = (
proof.variable_names_mapping.get(var, var)
if proof.variable_names_mapping is not None
else var
)
model.append((var_name, term_pretty))
models[node.id] = model
return APRFailureInfo(
failing_nodes=failing_nodes,
Expand Down
Loading