Crate varisat_checker

Proof checker for Varisat proofs.

Modules

clauses	Clause storage (unit and non-unit clauses).
context	Central checker data structure.
hash	Computation of clause hashes.
internal	Varisat internal interface used for on-the-fly checking.
processing	Processing of checked proof steps.
rup	Reverse unit propagation redundancy checks.
sorted_lits	Utilities for slices of sorted literals.
state	Checker state and checking of proof steps.
tmp	Temporary data.
transcript	Proof transcripts.
variables	Variable metadata.

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.

Constants

_DERIVE_failure_Fail_FOR_CheckerError
_DERIVE_failure_core_fmt_Display_FOR_CheckerError

Traits

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