Module varisat::proof

Proof generation.

Modules

drat
map_step	Maps literals and hashes of clause steps between the solver and the checker.

Structs

Proof

Proof generation.

Enums

ProofFormat

Proof formats that can be generated during solving.

Functions

add_clause	Call when adding an external clause.
add_step	Add a step to the proof.
clause_count_delta	Number of added or removed clauses.
close_proof	Stop writing proof steps.
flush_proof	Flush buffers used for writing proof steps.
handle_io_errors	Handle io errors during proof writing.
handle_self_check_result	Handle results of on the fly checking.
solve_finished	Called before solve returns to flush buffers and to trigger delayed unit conflict processing.
write_varisat_step	Write a step using our native format