Struct SimplificationConfig 

pub struct SimplificationConfig {
    pub apply_demorgan: bool,
    pub simplify_double_negation: bool,
    pub remove_identities: bool,
    pub combine_inferences: bool,
    pub simplify_tautologies: bool,
    pub max_passes: usize,
}

Configuration for proof simplification.

Fields

apply_demorgan: bool

Apply De Morgan’s laws to normalize negations

simplify_double_negation: bool

Simplify double negations (¬¬p → p)

remove_identities: bool

Remove identity operations (p ∧ true → p)

combine_inferences: bool

Combine consecutive inferences when possible

simplify_tautologies: bool

Simplify tautologies (p ∨ ¬p → true)

max_passes: usize

Maximum number of simplification passes

Implementations

impl SimplificationConfig

pub fn new() -> Self

Create a new configuration with all simplifications enabled.

pub fn without_demorgan(self) -> Self

Disable De Morgan’s law simplification.

pub fn with_max_passes(self, passes: usize) -> Self

Set maximum number of passes.

Trait Implementations

impl Clone for SimplificationConfig

fn clone(&self) -> SimplificationConfig

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SimplificationConfig

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

Formats the value using the given formatter.

impl Default for SimplificationConfig

fn default() -> Self

Returns the “default value” for a type.