Enum DeleteClauseProof

pub enum DeleteClauseProof {
    Redundant,
    Simplified,
    Satisfied,
}

Justifications for a simple clause deletion.

Variants

Redundant

The clause is known to be redundant.

Simplified

The clause is irred and subsumed by the clause added in the previous step.

Satisfied

The clause contains a true literal.

Also used to justify deletion of tautological clauses.

Trait Implementations

impl Clone for DeleteClauseProof

fn clone(&self) -> DeleteClauseProof

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for DeleteClauseProof

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

Formats the value using the given formatter.

impl PartialEq for DeleteClauseProof

fn eq(&self, other: &DeleteClauseProof) -> 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 Copy for DeleteClauseProof

impl Eq for DeleteClauseProof

impl StructuralPartialEq for DeleteClauseProof