Remove proof field from Prover #4250
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Porting runtimeverification/pyk#960 to K repo.
APRProver.step_proof
currently assumes the proof being passed in theAPRProofStep
it takes as argument is the same asself.proof
, i.e. when it callsself.nonzero_depth
,self._check_subsume
, andself._checked_for_bounded
assumes the proof being passed in is always the same for a singleAPRProver
instance.This is a problem in itself, but changing this should also move us closer an implementation that can run
step_proof
on different nodes in parallel, by reducing its dependency on external data. A next step could be initializing a new KCFGExplore everystep_proof
instead of usingself.kcfg_explore
to access theKoreClient
.proof
field fromProver
andAPRProver
.self.prover
take a prover argumentinit_proof
at the beginning ofadvance_proof
rather than in theProver
constructor._checked_for_terminal
and_checked_for_bounded
intoAPRProof
, as they refer to nodes of a specific proof.