Self-contained proof steps for EqualityProver and APRProver

[nwatson22]

Refactor to advance_proof intended to split step_proof stages get_steps (figure out which steps are available), exec (standalone chunk of work which has all the information necessary to perform it contained in ProofStep, and commit, which modifies proof with the results of the proof steps. Intended to be an incremental step toward parallelizing individual proofs. Pulled largely from #727
Adds:

• ProofStep and subclasses APRProofStep and ImpliesProofStep
• StepResult and subclasses APRProofResult and ImpliesProofResult, for returning proof update information from ProofStep.exec
• subclasses of APRProofResult APRProofExtendResult for if the current node should be extended and APRProofSubsumeResult for if it should be subsumed into the target
• Change Proof.advance_proof to, instead of calling step in a loop, calls get_steps, and then calls exec and then commit on each of these steps.

Tested against kontrol test suite as well.

[ehildenb]

I don't like how KCFGExplore is a field of the *Step classes, because presumably we'll be passing the *Step between different processes, and the KCFGExplore has with it backend servers. So I guess I'd prefer if the KCFGExplore stayed in the *Prover classes, and somehow the actual proof step still happens in the *Prover classes. The *Step classes should just be the basic data necessary to mark what step is to be taken next, in teh case of APRProofStep that would just be the node id that is supposed to be expanded next, and in the case of ImpliesProofStep that would just be the empty data (since the expansion routine is always the same).

@tothtamas28 what do you think?

[ehildenb]

Let's make the following changes:

• get_steps() -> list[ProofStep] and commit(ProofStepResult) -> None, are now methods of the *Proof classes, not of the *Prover classes.
• The step_proof(ProofStep) -> list[ProofStepResult] method is part of the *Prover class.
• The ProofStep and ProofStepResult do not hold a KCFGExplore (that stays in *Prover classes), and only holds the minimum data for step_proof(...) to be able to operate.

[ehildenb]

With this design, we may be able to make it so that *Prover does not even hold a *Proof in its hands.

[palinatolmach]

@nwatson22 is anything blocking this PR? Is it still relevant?

[nwatson22]

Closing in favor of

• Remove proof field from Prover k#4250
• Add separate get proof steps and execute proof step phase k#4246
• Parallel proof exploration k#4256