[−][src]Trait varisat_formula::cnf::ExtendFormula

pub trait ExtendFormula: Sized {
    fn add_clause(&mut self, literals: &[Lit]);

    fn new_var(&mut self) -> Var;

    fn new_lit(&mut self) -> Lit { ... }

    fn new_var_iter(&mut self, count: usize) -> NewVarIter<'_, Self>ⓘ
Notable 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>ⓘ
Notable 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_vars<Vars: UniformTuple<Var>>(&mut self) -> Vars { ... }

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

Extend a formula with new variables and clauses.

Required methods

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

Appends a clause to the formula.

fn new_var(&mut self) -> Var

Add a new variable to the formula and return it.

Loading content...

Provided methods

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>ⓘ

Notable 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;

Iterator over multiple new variables.

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

Notable 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;

Iterator over multiple new literals.

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

Add multiple new variables and return them.

Returns a uniform tuple of variables. The number of variables is inferred, so it can be used like let (x, y, z) = formula.new_vars().

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

Add multiple new variables and return them as positive literals.

Returns a uniform tuple of variables. The number of variables is inferred, so it can be used like let (x, y, z) = formula.new_lits().

Loading content...

Implementors

impl ExtendFormula for CnfFormula[src]

Loading content...