[−][src]Trait varisat_formula::cnf::ExtendFormula
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.
Provided methods
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>fn new_var_iter(&mut self, count: usize) -> NewVarIter<Self>
ⓘImportant traits for NewVarIter<'a, F, V>
Iterator over multiple new variables.
ⓘImportant traits for NewVarIter<'a, F, V>fn new_lit_iter(&mut self, count: usize) -> NewVarIter<Self, Lit>
ⓘImportant traits for NewVarIter<'a, F, 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()
.
Implementors
impl ExtendFormula for CnfFormula
[src]
fn add_clause(&mut self, clause: &[Lit])
[src]
fn new_var(&mut self) -> Var
[src]
fn new_lit(&mut self) -> Lit
[src]
ⓘImportant traits for NewVarIter<'a, F, V>fn new_var_iter(&mut self, count: usize) -> NewVarIter<Self>
[src]
ⓘImportant traits for NewVarIter<'a, F, V>
ⓘImportant traits for NewVarIter<'a, F, V>fn new_lit_iter(&mut self, count: usize) -> NewVarIter<Self, Lit>
[src]
ⓘImportant traits for NewVarIter<'a, F, V>