Enum NnfFormula 

pub enum NnfFormula {
    Atom(usize),
    NegAtom(usize),
    And(Box<NnfFormula>, Box<NnfFormula>),
    Or(Box<NnfFormula>, Box<NnfFormula>),
    Top,
    Bot,
}

A propositional formula in NNF (Negation Normal Form).

In NNF, negations appear only at atoms (literals). This simplifies many proof-theoretic manipulations.

Variants

Atom(usize)

A positive atom (propositional variable index).

NegAtom(usize)

A negated atom.

And(Box<NnfFormula>, Box<NnfFormula>)

Conjunction.

Or(Box<NnfFormula>, Box<NnfFormula>)

Disjunction.

Top

The constant True.

Bot

The constant False.

Implementations

impl NnfFormula

pub fn is_literal(&self) -> bool

Check if the formula is a literal (atom or negated atom).

pub fn atom_count(&self) -> usize

Count the number of atoms in the formula.

pub fn connective_count(&self) -> usize

Count the number of connectives in the formula.

pub fn variables(&self) -> Vec<usize>

Collect all variable indices appearing in the formula.

pub fn eval(&self, assignment: &[bool]) -> bool

Evaluate the formula under a truth assignment (variable index → bool).

pub fn simplify(self) -> NnfFormula

Simplify by eliminating Top/Bot.

Trait Implementations

impl Clone for NnfFormula

fn clone(&self) -> NnfFormula

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for NnfFormula

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

Formats the value using the given formatter.

impl PartialEq for NnfFormula

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

impl StructuralPartialEq for NnfFormula