Struct varisat_checker::Checker

pub struct Checker<'a> { /* fields omitted */ }

A checker for unsatisfiability proofs in the native varisat format.

Implementations

impl<'a> Checker<'a>

pub fn new() -> Checker<'a>

Create a new checker.

pub fn add_clause(&mut self, clause: &[Lit]) -> Result<(), CheckerError>

Adds a clause to the checker.

pub fn add_formula(&mut self, formula: &CnfFormula) -> Result<(), CheckerError>

Add a formula to the checker.

pub fn add_dimacs_cnf(&mut self, input: impl Read) -> Result<(), Error>

Reads and adds a formula in DIMACS CNF format.

Using this avoids creating a temporary CnfFormula.

pub fn add_processor(&mut self, processor: &'a mut dyn ProofProcessor)

Add a ProofProcessor.

This has to be called before loading any clauses or checking any proofs.

pub fn add_transcript(
    &mut self,
    processor: &'a mut dyn ProofTranscriptProcessor
)

Add a ProofTranscriptProcessor.

This has to be called before loading any clauses or checking any proofs.

pub fn check_proof(&mut self, input: impl Read) -> Result<(), CheckerError>

Checks a proof in the native Varisat format.

Trait Implementations

impl<'a> Default for Checker<'a>

fn default() -> Checker<'a>

Returns the "default value" for a type.

impl<'a> SelfChecker for Checker<'a>

fn self_check_step(&mut self, step: ProofStep<'_>) -> Result<(), CheckerError>

fn self_check_delayed_steps(&mut self) -> Result<(), CheckerError>