Enum varisat_internal_proof::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 Eq for DeleteClauseProof

fn assert_receiver_is_total_eq(&self)

impl PartialEq<DeleteClauseProof> for DeleteClauseProof

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

This method tests for self and other values to be equal, and is used by ==.

#[must_use]

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

This method tests for !=.

impl Copy for DeleteClauseProof

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.