558 add general proof api#583

Open

gcarpio21 wants to merge 46 commits intomasterfrom

558-add-general-proof-api

Commits on Dec 20, 2025

Added interfaces for handling general proofs of unsatisfiability: `Proof`, `ProofRule`.
gcarpio21
committed
Added abstract class implementing the proof interface `AbstractProof`.
gcarpio21
committed
Added the implementation of method `getProof` for retrieving `Proof` objects in `BasicProverEnvironment` and multiple classes that implement said interface: `BasicProverEnvironmentWithAssumptionsWr…
gcarpio21
committed
Added the implementation of method `getProof` for retrieving `Proof` objects in abstract class `AbstractProver` as well as flag `generateProofs` and method `checkGenerateProofs`.
gcarpio21
committed
Added the abstract class `ProofFrame` for transformation of native proof objects from the solvers into `Proof` objects.
gcarpio21
committed
Added `GENERATE_PROOFS` to `ProverOptions` in `SolverContext`.
gcarpio21
committed
Implemented method `getProof` in `CVC5AbstractProver` for retrieving common `Proof`s from the solver.
gcarpio21
committed
Added enum `CVC5ProofRule` for the different proof rules used by CVC5.
gcarpio21
committed
Added class `CV5Proof` which extends `AbstractProof`. `generateProofImpl` handles transformation from the solver's native proof into the common `Proof`.
gcarpio21
committed
Added method `requireProofGeneration` to `SolverBasedTest0`.
gcarpio21
committed
In `ProverEnvironmentTest` added multiple methods for testing retrieving common `Proof`s from solvers. Conditions include: different theories, trivial proofs, simple proofs, not enabling proof prod…
gcarpio21
committed

Commits on Jan 16, 2026

Removed unnecessary method from the `ProofRule` interface.
gcarpio21
committed

Commits on Jan 19, 2026

Merge branch 'master' into 558-add-general-proof-api
gcarpio21
authored

Commits on Jan 20, 2026

Commits on Jan 21, 2026

Proofs: Field `children` of `AbstractProof` now is an `ImmutableSet`.
gcarpio21
committed

Commits on Jan 22, 2026

Commits on Jan 26, 2026

Commits on Jan 27, 2026

Merge branch 'master' into 558-add-general-proof-api
gcarpio21
committed

Commits on Jan 28, 2026

Commits on Jan 30, 2026

Commits on Feb 17, 2026