Crate varisat_checker

Proof checker for Varisat proofs.

Modules

internal

Varisat internal interface used for on-the-fly checking.

Structs

CheckedUserVar	Corresponding user variable for a proof variable.
Checker	A checker for unsatisfiability proofs in the native varisat format.
CheckerData	Checker data available to proof processors.
ResolutionPropagations	A list of clauses to resolve and propagations to show that the resolvent is an AT.

Enums

CheckedProofStep	A single step of a proof.
CheckedSamplingMode	Sampling mode of a user variable.
CheckerError	Possible errors while checking a varisat proof.
ProofTranscriptStep	Step of a proof transcript.

Traits

ProofProcessor	Implement to process proof steps.
ProofTranscriptProcessor	Implement to process transcript steps.