Enum libprop_sat_solver::tableaux_solver::ExpansionKind

pub enum ExpansionKind {
    Alpha(Box<PropositionalFormula>, Option<Box<PropositionalFormula>>),
    Beta(Box<PropositionalFormula>, Box<PropositionalFormula>),
}

Result of expansion using various rules.

Variants

Alpha(Box<PropositionalFormula>, Option<Box<PropositionalFormula>>)

The alpha (α) rule is applicable to the forms:

Form	α1	α2
(A^B)	A	B
(A<->B)	(A->B)	(B->A)
(-(A|B))	(-A)	(-B)
(-(A->B))	A	(-B)
(-(-A))	A	-

Beta(Box<PropositionalFormula>, Box<PropositionalFormula>)

The beta (β) rule is applicable to the forms:

Form	β1	β2
(A|B)	A	B
(-(A^B))	(-A)	(-B)
(A->B)	(-A)	B
-(A<->B)	(A^(-B))	(B^(-A))

Trait Implementations

impl Clone for ExpansionKind

fn clone(&self) -> ExpansionKind

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for ExpansionKind

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

Formats the value using the given formatter.

impl Eq for ExpansionKind

impl PartialEq<ExpansionKind> for ExpansionKind

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

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

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

This method tests for !=.

impl StructuralEq for ExpansionKind

impl StructuralPartialEq for ExpansionKind