Struct varisat_formula::cnf::CnfFormula

pub struct CnfFormula {
    var_count: usize,
    literals: Vec<Lit>,
    clause_ranges: Vec<Range<usize>>,
}

A formula in conjunctive normal form (CNF).

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

Fields

var_count: usize

literals: Vec<Lit>

clause_ranges: Vec<Range<usize>>

Methods

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 iter(&self) -> impl Iterator<Item = &[Lit]>

Iterator over all clauses.

Trait Implementations

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.

Important traits for NewVarIter<'a, F, V>

impl<'a, F, V> Iterator for NewVarIter<'a, F, V> where
    F: ExtendFormula,
    V: From<Var>,  type Item = V;

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

Iterator over multiple new variables.

Important traits for NewVarIter<'a, F, V>

impl<'a, F, V> Iterator for NewVarIter<'a, F, V> where
    F: ExtendFormula,
    V: From<Var>,  type Item = V;

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

Iterator over multiple new literals.

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

Add multiple new variables and return them.

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

Add multiple new variables and return them as positive literals.

impl Eq for CnfFormula

fn assert_receiver_is_total_eq(&self)

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 !=.

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 Default for CnfFormula

fn default() -> CnfFormula

Returns the "default value" for a type.

impl Debug for CnfFormula

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

Formats the value using the given formatter.