Enum Formula

pub enum Formula {
    Lit(Lit),
    Paren(FormulaBox),
    Neg(FormulaBox),
    And(FormulaList),
    Or(FormulaList),
    Xor(FormulaList),
    Eq(FormulaList),
}

Represents the structure of formulas of .sat files.

Variants

Lit(Lit)

A single literal. This is the leaf node type of sat formulas.

Paren(FormulaBox)

Represents (f) if f is a valid formula.

Neg(FormulaBox)

Represents -(f) if f is a valid formula. This negates the result of the inner f.

And(FormulaList)

Represents *(f_1 .. f_k) if f_1, .., f_k are valid formulas. The effect is a logical and of its inner formulas.

Or(FormulaList)

Represents +(f_1 .. f_k) if f_1, .., f_k are valid formulas. The effect is a logical or of its inner formulas.

Xor(FormulaList)

Represents xor(f_1 .. f_k) if f_1, .., f_k are valid formulas. The effect is a logical xor of its inner formulas.

Eq(FormulaList)

Represents =(f_1 .. f_k) if f_1, .., f_k are valid formulas. The effect is a logical equals of its inner formulas.

Implementations

impl Formula

pub fn lit(lit: Lit) -> Formula

Creates a new literal leaf formula with the given literal.

pub fn paren(inner: Formula) -> Formula

Wraps the inner formula within parentheses.

pub fn neg(inner: Formula) -> Formula

Negates the inner formula.

pub fn and(params: Vec<Formula>) -> Formula

Creates a logical and formula of all given formulas in param.

pub fn or(params: Vec<Formula>) -> Formula

Creates a logical or formula of all given formulas in param.

pub fn xor(params: Vec<Formula>) -> Formula

Creates a logical xor formula of all given formulas in param.

pub fn eq(params: Vec<Formula>) -> Formula

Creates a logical equality formula of all given formulas in param.

Trait Implementations

impl Clone for Formula

fn clone(&self) -> Formula

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Formula

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

Formats the value using the given formatter.

impl PartialEq for Formula

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

impl StructuralPartialEq for Formula