Enum dimacs::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.

Methods

impl Formula

fn lit(lit: Lit) -> Formula

Creates a new literal leaf formula with the given literal.

fn paren(inner: Formula) -> Formula

Wraps the inner formula within parentheses.

fn neg(inner: Formula) -> Formula

Negates the inner formula.

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

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

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

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

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

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

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

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

Trait Implementations

impl Debug for Formula

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

Formats the value using the given formatter.

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 PartialEq for Formula

fn eq(&self, __arg_0: &Formula) -> bool

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

fn ne(&self, __arg_0: &Formula) -> bool

This method tests for !=.

impl Eq for Formula