Struct TautologyElimination 

pub struct TautologyElimination;

Preprocessor for Tautology Elimination.

A tautological clause is a clause that contains both a literal and its negation (e.g. x V !x V y). Such clauses are always true and can be removed from a CNF formula without changing its satisfiability.

Trait Implementations

impl Clone for TautologyElimination

fn clone(&self) -> TautologyElimination

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TautologyElimination

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

Formats the value using the given formatter.

impl Default for TautologyElimination

fn default() -> TautologyElimination

Returns the “default value” for a type.

impl PartialEq for TautologyElimination

fn eq(&self, other: &TautologyElimination) -> 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<L: Literal, S: LiteralStorage<L>> Preprocessor<L, S> for TautologyElimination

fn preprocess(&self, cnf: &[Clause<L, S>]) -> Vec<Clause<L, S>>

Applies tautology elimination.

Filters out any clause c for which c.is_tautology() is true.

impl Copy for TautologyElimination

impl Eq for TautologyElimination

impl StructuralPartialEq for TautologyElimination