Struct varisat::proof::Proof

pub struct Proof<'a> {
    format: Option<ProofFormat>,
    target: BufWriter<Box<dyn Write + 'a>>,
    checker: Option<Checker<'a>>,
    map_step: MapStep,
    hash_bits: u32,
    clause_count: isize,
}

Proof generation.

Fields

format: Option<ProofFormat>

target: BufWriter<Box<dyn Write + 'a>>

checker: Option<Checker<'a>>

map_step: MapStep

hash_bits: u32

How many bits are used for storing clause hashes.

clause_count: isize

How many clauses are currently in the db.

This is used to pick a good number of hash_bits

Methods

impl<'a> Proof<'a>

pub fn write_proof(&mut self, target: impl Write + 'a, format: ProofFormat)

Start writing proof steps to the given target with the given format.

pub fn begin_checking(&mut self)

Begin checking proof steps.

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

Add a ProofProcessor.

See also Checker::add_processor.

pub fn is_active(&self) -> bool

Whether proof generation is active.

pub fn native_format(&self) -> bool

Are we emitting or checking our native format.

pub fn clause_hashes_required(&self) -> bool

Whether clause hashes are required for steps that support them.

pub fn models_in_proof(&self) -> bool

Whether found models are included in the proof.

Trait Implementations

impl<'a> Default for Proof<'a>

fn default() -> Proof<'a>

Returns the "default value" for a type.