Struct varisat::checker::Checker

pub struct Checker<'a> where
    'a: 'a,  {
    ctx: Box<Context<'a>>,
}

A checker for unsatisfiability proofs in the native varisat format.

Fields

ctx: Box<Context<'a>>

Methods

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<impl io::Read>(
    &mut self,
    input: impl io::Read
) -> Result<(), Error> where
    impl io::Read: Read, 

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 + 'a))

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 + 'a)
)

Add a ProofTranscriptProcessor.

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

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

Checks a proof in the native Varisat format.

Trait Implementations

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>

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

fn default() -> Checker<'a>

Returns the "default value" for a type.