Add Proof Support to API #558
Description
JavaSMT is lacking a common API for proofs of unsatisfiablity. This is partially due to basically no two solvers using the same proof format.
@gcarpio21 already worked quite a lot on supporting proofs in the formats of the solvers in JavaSMT, but also started working on a common proof format based on SMTInterpols format.
Since this work is currently squashed into a single branch, we should split the core-framework for proofs with a well working solver implementation for proofs into a new branch and focus on merging it to master before continuing. @gcarpio21 please choose an appropriate SMT solver for this and commit your work to branch 558-add-general-proof-api.
Subsequently, we should add more solvers in their own branches.
To keep track of the progress:
- General proof API
- Test suite for proofs
Solvers with proof support that have been added to JavaSMT:
- Z3
- CVC5
- CVC4
- MathSAT5
- SMTInterpol
- Princess
- OpenSMT