Struct varisat::cnf::CnfFormula

pub struct CnfFormula { /* fields omitted */ }

A formula in conjunctive normal form (CNF).

Equivalent to Vec<Vec> but more efficient as it uses a single buffer for all literals.

Implementations

impl CnfFormula

pub fn new() -> CnfFormula

Create an empty CNF formula.

pub fn var_count(&self) -> usize

Number of variables in the formula.

This also counts missing variables if a variable with a higher index is present. A vector of this length can be indexed with the variable indices present.

pub fn set_var_count(&mut self, count: usize)

Increase the number of variables in the formula.

If the parameter is less than the current variable count do nothing.

pub fn len(&self) -> usize

Number of clauses in the formula.

pub fn is_empty(&self) -> bool

Whether the set of clauses is empty.

pub fn iter(&self) -> impl Iterator<Item = &[Lit]>

Iterator over all clauses.

Trait Implementations

impl Debug for CnfFormula

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

Formats the value using the given formatter.

impl Default for CnfFormula

fn default() -> CnfFormula

Returns the "default value" for a type.

impl Eq for CnfFormula

impl ExtendFormula for CnfFormula

fn add_clause(&mut self, clause: &[Lit])

Appends a clause to the formula.

fn new_var(&mut self) -> Var

Add a new variable to the formula and return it.

fn new_lit(&mut self) -> Lit

Add a new variable to the formula and return it as positive literal.

fn new_var_iter(&mut self, count: usize) -> NewVarIter<'_, Self, Var>

Iterator over multiple new variables.

fn new_lit_iter(&mut self, count: usize) -> NewVarIter<'_, Self, Lit>

Iterator over multiple new literals.

fn new_vars<Vars>(&mut self) -> Vars where
    Vars: UniformTuple<Var>, 

Add multiple new variables and return them.

fn new_lits<Lits>(&mut self) -> Lits where
    Lits: UniformTuple<Lit>, 

Add multiple new variables and return them as positive literals.

impl<Clauses, Item> From<Clauses> for CnfFormula where
    Clauses: IntoIterator<Item = Item>,
    Item: Borrow<[Lit]>, 

Convert an iterable of Lit slices into a CnfFormula

fn from(clauses: Clauses) -> CnfFormula

Performs the conversion.

impl PartialEq<CnfFormula> for CnfFormula

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

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

#[must_use]fn ne(&self, other: &Rhs) -> bool

This method tests for !=.