Enum ProofStep 

pub enum ProofStep {
    Input {
        index: u32,
        clause: Vec<Lit>,
    },
    Resolution {
        index: u32,
        left: u32,
        right: u32,
        pivot: Var,
        clause: Vec<Lit>,
    },
    TheoryLemma {
        index: u32,
        theory: String,
        clause: Vec<Lit>,
        explanation: Vec<TermId>,
    },
}

Proof step for resolution-based proofs

Variants

Input

Input clause (from the original formula)

Fields

index: u32

Clause index

clause: Vec<Lit>

The clause (as a disjunction of literals)

Resolution

Resolution step

Fields

index: u32

Index of this proof step

left: u32

Left parent clause index

right: u32

Right parent clause index

pivot: Var

Pivot variable (the variable resolved on)

clause: Vec<Lit>

Resulting clause

TheoryLemma

Theory lemma (from a theory solver)

Fields

index: u32

Index of this proof step

theory: String

The theory that produced this lemma

clause: Vec<Lit>

The lemma clause

explanation: Vec<TermId>

Explanation terms

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.