Crate varisat_internal_proof

Crate varisat_internal_proof 

Source
Expand description

Internal proof format for the Varisat SAT solver.

Modules§

binary_format
Binary format for varisat proofs.

Enums§

DeleteClauseProof
Justifications for a simple clause deletion.
ProofStep
A single proof step.

Functions§

clause_hash
A fast hash function for clauses (or other sets of literals).
lit_code_hash
Hash a single literal from a code.
lit_hash
Hash a single literal.

Type Aliases§

ClauseHash