Skip to content
This repository was archived by the owner on Apr 25, 2024. It is now read-only.

Self-contained proof steps for EqualityProver and APRProver #886

Closed
wants to merge 21 commits into from
Closed
Changes from 1 commit
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
61a3172
Separate logic for ImpliesProof and APRProof into self-contained step…
nwatson22 Feb 15, 2024
5412c5e
Merge 61a31724709329df06fefef5d2a42b2fe03451e9 into d7b05c1de94620720…
nwatson22 Feb 15, 2024
fbe0eb7
Set Version: 0.1.628
Feb 15, 2024
adea081
Fix nodes being checked for terminal before starting the next step
nwatson22 Feb 15, 2024
8621acc
Merge branch 'noah/atomic-steps' of https://github.com/runtimeverific…
nwatson22 Feb 15, 2024
481d271
Fix subst not being set
nwatson22 Feb 15, 2024
4f08787
Fix max_iteration and fail_fast only executing between step groups
nwatson22 Feb 16, 2024
ec0c7ae
Clean up
nwatson22 Feb 16, 2024
9626c12
Clean up
nwatson22 Feb 16, 2024
0f6258a
Clean up
nwatson22 Feb 16, 2024
adf59d2
Merge master into branch
nwatson22 Feb 16, 2024
13c15d8
Merge adf59d2000c24381604c467eac6e1c5fca35eb3e into 8bec235cf7356a844…
nwatson22 Feb 16, 2024
883fbc2
Set Version: 0.1.630
Feb 16, 2024
e445d45
Fix proof data not being writen and failure info not being saved at t…
nwatson22 Feb 16, 2024
f38ad6b
Merge branch 'noah/atomic-steps' of https://github.com/runtimeverific…
nwatson22 Feb 16, 2024
4325aad
Fix write_proof not being called at the correct time
nwatson22 Feb 16, 2024
97f3e4e
Merge master into branch
nwatson22 Feb 16, 2024
0772327
Merge 97f3e4ef108f6fb6c00da29ab9aeb8ec2b3edb48 into 02ec6eb1d39f12663…
nwatson22 Feb 16, 2024
4b74439
Set Version: 0.1.632
Feb 16, 2024
2b5ee73
Start moving commit and get_steps to proof
nwatson22 Feb 20, 2024
03737cc
Merge branch 'noah/atomic-steps' of https://github.com/runtimeverific…
nwatson22 Feb 20, 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
Prev Previous commit
Next Next commit
Clean up
nwatson22 committed Feb 16, 2024
commit ec0c7ae0b5bdaa721db081e5d1e2af73fd045bb2
14 changes: 0 additions & 14 deletions src/pyk/proof/reachability.py
Original file line number Diff line number Diff line change
@@ -739,7 +739,6 @@ def get_steps(self) -> Iterable[APRProofStep]:
terminal_rules=self.terminal_rules,
)
)
print(steps)
return steps

def commit(self, result: StepResult) -> None:
@@ -761,9 +760,6 @@ def commit(self, result: StepResult) -> None:
if self.proof.failed:
self.proof.failure_info = self.failure_info()

show = KCFGShow(self.kcfg_explore.kprint, node_printer=APRProofNodePrinter(self.proof, self.kcfg_explore.kprint, full_printer=True))
print('\n+'.join(show.pretty(self.proof.kcfg)))

self._check_all_terminals()

for node in self.proof.terminal:
@@ -775,12 +771,6 @@ def commit(self, result: StepResult) -> None:
self._checked_for_subsumption.add(node.id)
self._check_subsume(node)

print(f'pending: {self.proof.pending}')
print(f'can_progress: {self.proof.can_progress}')

show = KCFGShow(self.kcfg_explore.kprint, node_printer=APRProofNodePrinter(self.proof, self.kcfg_explore.kprint, full_printer=True))
print('\n-'.join(show.pretty(self.proof.kcfg)))

def failure_info(self) -> APRFailureInfo:
return APRFailureInfo.from_proof(self.proof, self.kcfg_explore, counterexample_info=self.counterexample_info)

@@ -838,12 +828,8 @@ def _check_subsume(self) -> CSubst | None:
return self.kcfg_explore.cterm_implies(self.cterm, self.target_cterm)

def exec(self) -> APRProofResult:
print(f'is_terminal: {self.is_terminal}')
print(f'target_is_terminal: {self.target_is_terminal}')
if self.is_terminal or not self.target_is_terminal:
print(f'always_check_subsumption: {self.always_check_subsumption}')
if self.always_check_subsumption:
print(f'checking subsumption {self.node_id}')
csubst = self._check_subsume()
if csubst is not None or self.is_terminal:
return APRProofSubsumeResult(csubst=csubst, node_id=self.node_id)