Enum ProofStep 

pub enum ProofStep {
    Rup(Vec<Lit>),
    Pr {
        clause: Vec<Lit>,
        witness: Witness,
    },
    Delete(Vec<Lit>),
}

One step of a refutation: add a clause with the justification a checker replays, or delete a clause from the working database (the DRAT deletion that inprocessing — vivification, BVE — relies on; deletions are unchecked, only additions carry a redundancy obligation).

Variants

Rup(Vec<Lit>)

Add a clause that is RUP w.r.t. the current database.

Pr

Add a clause that is propagation-redundant w.r.t. the current database, certified by witness. May remove models; preserves satisfiability.

Fields

clause: Vec<Lit>

witness: Witness

Delete(Vec<Lit>)

Remove a clause from the working database (a sound DRAT deletion).

Implementations

impl ProofStep

pub fn clause(&self) -> &[Lit]

The clause this step adds or deletes.

Trait Implementations

impl Clone for ProofStep

fn clone(&self) -> ProofStep

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ProofStep

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Eq for ProofStep

impl PartialEq for ProofStep

fn eq(&self, other: &ProofStep) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for ProofStep