558 add general proof api #583
Conversation
…oof`, `ProofRule`.
…objects in `BasicProverEnvironment` and multiple classes that implement said interface: `BasicProverEnvironmentWithAssumptionsWrapper`, `DebuggingBasicProverEnvironment`, `LoggingBasicProverEnvironment`, `StatisticsBasicProverEnvironment`, `SynchronizedBasicProverEnvironment`, `SynchronizedBasicProverEnvironmentWithContext`.
…objects in abstract class `AbstractProver` as well as flag `generateProofs` and method `checkGenerateProofs`.
…oof objects from the solvers into `Proof` objects.
…common `Proof`s from the solver.
…mpl` handles transformation from the solver's native proof into the common `Proof`.
…ing common `Proof`s from solvers. Conditions include: different theories, trivial proofs, simple proofs, not enabling proof production, etc.
baierd
left a comment
baierd
left a comment
There was a problem hiding this comment.
Partial review. I will continue tomorrow.
| * | ||
| * @param <T> The type of the proof object. | ||
| */ | ||
| public abstract class ProofFrame<T> { |
There was a problem hiding this comment.
Do i see it correctly that this class is only needed to generate the proof?
There was a problem hiding this comment.
Yes, this is wrapper that helps process the proofs, I did not want to repeat code over all solvers so I put the class in this directory.
There was a problem hiding this comment.
I moved this class inside AbstractProof I think this better fits the structure of the project. I was thinking of taking the proof interfaces out of the proofs package into the api one for the same reason.
| import org.sosy_lab.java_smt.api.Formula; | ||
|
|
||
| /** A proof node in the proof DAG of a proof. */ | ||
| public interface Proof { |
There was a problem hiding this comment.
It seems like the name of this class should be ProofNode.
There was a problem hiding this comment.
Note: this was named ProofNode in the past and was changed due to me requesting it.
In general: the Proof interface/object should hold all proofs themselves, and provide API to access them (similar to the model). The problem with this being called Proof can be seen in the API, e.g. ImmutableSet<Proof> getChildren();. If getChildren() returns a Proof, it is clear that there is a problem, as the Proof should only exist as one central element. Hence i was wrong in wanting to rename this interface to Proof, and it should be called ProofNode as @gcarpio21 named it correctly initially!
We should then add a new interface Proof, that has the API to return the root (and only ever the root) of the proof DAG (and potentially more in the future).
| // protected abstract Proof generateProof(); | ||
| // } | ||
|
|
||
| private final Set<Proof> children = new LinkedHashSet<>(); |
There was a problem hiding this comment.
Please try using immutable data-structures as far as possible.
You can find a good guide as to why and when to use mutable and immutable data-structures in CPAcheckers style-guide here.
… Deleted out-commented code. Deleted resolved TODO.
…bleSet`. Deleted out-commented code. Deleted resolved TODO." This reverts commit ed64164.
…e of `getChildren` to `ImmutableSet`.
…ed to `ImmutableSet`.
…Proof` to comply with the Style & Coding Guide.
… with the Style & Coding Guide.
…the Style & Coding Guide, deleted unnecessary comments.
| import org.sosy_lab.java_smt.api.Formula; | ||
|
|
||
| /** A proof node in the proof DAG of a proof. */ | ||
| public interface Proof { |
There was a problem hiding this comment.
Note: this was named ProofNode in the past and was changed due to me requesting it.
In general: the Proof interface/object should hold all proofs themselves, and provide API to access them (similar to the model). The problem with this being called Proof can be seen in the API, e.g. ImmutableSet<Proof> getChildren();. If getChildren() returns a Proof, it is clear that there is a problem, as the Proof should only exist as one central element. Hence i was wrong in wanting to rename this interface to Proof, and it should be called ProofNode as @gcarpio21 named it correctly initially!
We should then add a new interface Proof, that has the API to return the root (and only ever the root) of the proof DAG (and potentially more in the future).
| /** A proof rule from a given proof format. */ | ||
| public interface ProofRule { | ||
|
|
||
| /** Get the name of the proof rule. */ |
There was a problem hiding this comment.
An example would be helpful for users to understand. Especially since distinct solvers can return distinct rules.
| */ | ||
| GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS, | ||
|
|
||
| /** Whether the solver should generate proofs for unsatisfiable formulas. */ |
There was a problem hiding this comment.
Could you add a note about Z3 here please? The Z3 proof situation might be confusing for users.
There was a problem hiding this comment.
You mean about it needing proof generation enabled on the context object?
I was thinking to leave that out for this, as the only solver with proof generation should be CVC5 for now. Once it is turn for Z3 then I would add the corresponding note.
| } | ||
| } | ||
|
|
||
| // Traverses a proof and asserts that certain values are not null, instances, etc. |
There was a problem hiding this comment.
Looks like the name could be improved into something like varifyProofObjectValidity. (checkProof might be misunderstood such that the proof itself is checked for validity, but you are only checking the objects inside.) Also JavaDoc with more information would be helpful here.
2 participants
Objective
This PR aims to extend support for retrieving proofs of unsatisfiability from the CVC5 solver according to a general proof interface that would be used to do the same for other capable solvers. It is a step in closing the issue #558 .
Key Changes
Proof, andProofRuleas the main components for handling proofs.It is now possible to enable proof generating capabilities from CVC5 by passing
ProverOptions.GENERATE_PROOFSwhen creating a newProverEnvironmentinstance. Then when a query returns UNSAT one can callgetProof()to retrieve the proof of unsatisfiability.