Develop a common proof format and export proofs

[gcarpio21]

Objective

This PR aims to expose proofs produced by supported solvers through the API, primarily via a getProof() method.

Key Changes

• Introduced ProofNode, ProofDag, and ProofRule as the main components for handling proofs.
• Implemented proof retrieval for the Z3 solver.
• Explored a standardized format for proofs across different solvers.

Proof Format Conversion

To unify proof representation, this PR investigates converting solver-specific proofs into a common format, with RESOLUTE (used by SMTInterpol) as a candidate.

• The proposed approach models proof rules in CNF and transforms them into resolution steps.
• The Z3ToResoluteProofConverter provides an example of this transformation.

Task List

• [x] Implement getProof() for Z3.

• [x] Introduce ProofNode, ProofDag, and ProofRule.

• [ ] Implement getProof() for other solvers.

  • [x] Z3
  • [x] MathSAT5
  • [x] CVC5
  • [x] SMTInterpol
  • [ ] Princess
  • [ ] Opensmt

• [x] Test getProof more robustly.

Next Steps

• More flexibility while handling proofs could be provided through the ProofDag interface.

[baierd]

@leventeBajczi could you spare a look at this PR and maybe give us some feedback on the current proof interface?

[leventeBajczi]

@leventeBajczi could you spare a look at this PR and maybe give us some feedback on the current proof interface?

Definitely!

So far, I really like the relatively clean API for accessing the proofs, and I'm especially happy to see that the Z3 proofs are transformed to a 'simple' proof tree/DAG -- however, I'm uncertain how complete that transformation is based on the code, I think some information about that is missing (maybe as a comment?) to state how well Z3 proofs can be transformed into the common format.

Other than that, great work! I'm looking forward to integrating this with Theta. I'm really surprised at the number of solvers supporting proof generation, I only knew about MathSAT and Z3 beforehand. They will definitely be handy for us.

Have you maybe done some performance impact tests with the solvers when proof generation is enabled? I'd be interested to see how much performance is lost when it's active.

[gcarpio21]

@leventeBajczi could you spare a look at this PR and maybe give us some feedback on the current proof interface?

Definitely!

So far, I really like the relatively clean API for accessing the proofs, and I'm especially happy to see that the Z3 proofs are transformed to a 'simple' proof tree/DAG -- however, I'm uncertain how complete that transformation is based on the code, I think some information about that is missing (maybe as a comment?) to state how well Z3 proofs can be transformed into the common format.

Other than that, great work! I'm looking forward to integrating this with Theta. I'm really surprised at the number of solvers supporting proof generation, I only knew about MathSAT and Z3 beforehand. They will definitely be handy for us.

Have you maybe done some performance impact tests with the solvers when proof generation is enabled? I'd be interested to see how much performance is lost when it's active.

Right now, the Z3ToResoluteProofConverter class is still a work in progress. The goal is to transform Z3 proofs into a format similar to SMTInterpol’s (RESOLUTE), following the same proof rules.

Currently, the main functionality is to make Z3 proofs accessible through JavaSMT by simplifying Z3’s proof structures and implementing the ProofNode interface, which should capture all relevant proof information.

I haven’t run any performance tests yet. From what I know, enabling proof generation in a solver itself is usually quite costly. Hopefully, retrieving proofs through JavaSMT won’t introduce significant additional overhead.

I’ve also added more documentation in the code to clarify some of these points.

[gcarpio21]

Good work in cleaning up the classes!

I added a MathSAT5 native test for the proof generation option and it seems that there is no problem with it. Do other solvers need to option when creating the context?

Z3 needs the proof generation set when creating context

[baierd]

Good work in cleaning up the classes! I added a MathSAT5 native test for the proof generation option and it seems that there is no problem with it. Do other solvers need to option when creating the context?

Z3 needs the proof generation set when creating context

You can try to simply enable it per default currently in this branch. We can measure the performance impact and decide if we want this or not later.