Enum Witness 

pub enum Witness {
    Assignment(Vec<Lit>),
    Substitution(Perm),
}

A redundancy witness for a ProofStep::Pr clause.

Variants

Assignment(Vec<Lit>)

An explicit partial assignment (the set of literals it sets true) — the classic PR witness.

Substitution(Perm)

A literal permutation / automorphism. Against the clause C it certifies, it denotes the assignment ω = { ¬σ(l) : l ∈ C }.

Trait Implementations

impl Clone for Witness

fn clone(&self) -> Witness

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Witness

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

Formats the value using the given formatter.

impl PartialEq for Witness

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for Witness

impl StructuralPartialEq for Witness