[−][src]Trait varisat::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.
fn new_var_iter(&mut self, count: usize) -> NewVarIter<'_, Self, Var>ⓘ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;
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;
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>(&mut self) -> Vars where
Vars: UniformTuple<Var>,
Vars: UniformTuple<Var>,
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>(&mut self) -> Lits where
Lits: UniformTuple<Lit>,
Lits: UniformTuple<Lit>,
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()
.