[−][src]Trait varisat::ExtendFormula
Extend a formula with new variables and clauses.
Required methods
fn add_clause(&mut self, literals: &[Lit])
Appends a clause to the formula.
literals
can be an IntoIterator<Item = Lit>
or IntoIterator<Item = &Lit>
.
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, Var>
Iterator over multiple new variables.
ⓘImportant traits for NewVarIter<'a, F, V>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>,
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()
.
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, Var>
[src]
ⓘImportant traits for NewVarIter<'a, F, V>fn new_lit_iter(&mut self, count: usize) -> NewVarIter<Self, Lit>
[src]
fn new_vars<Vars>(&mut self) -> Vars where
Vars: UniformTuple<Var>,
[src]
Vars: UniformTuple<Var>,
fn new_lits<Lits>(&mut self) -> Lits where
Lits: UniformTuple<Lit>,
[src]
Lits: UniformTuple<Lit>,
impl<'a> ExtendFormula for Solver<'a>
[src]
fn add_clause(&mut self, clause: &[Lit])
[src]
Add a clause to the solver.
fn new_var(&mut self) -> Var
[src]
Add a new variable to the solver.
fn new_lit(&mut self) -> Lit
[src]
ⓘImportant traits for NewVarIter<'a, F, V>fn new_var_iter(&mut self, count: usize) -> NewVarIter<Self, Var>
[src]
ⓘImportant traits for NewVarIter<'a, F, V>fn new_lit_iter(&mut self, count: usize) -> NewVarIter<Self, Lit>
[src]
fn new_vars<Vars>(&mut self) -> Vars where
Vars: UniformTuple<Var>,
[src]
Vars: UniformTuple<Var>,
fn new_lits<Lits>(&mut self) -> Lits where
Lits: UniformTuple<Lit>,
[src]
Lits: UniformTuple<Lit>,