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.