[−][src]Trait varisat::ExtendFormula

pub trait ExtendFormula {
    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, Var> { ... }

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

    fn new_vars<Vars>(&mut self) -> Vars
    where
        Vars: UniformTuple<Var>,
    { ... }

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

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.

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

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

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]

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]

fn new_lits<Lits>(&mut self) -> Lits where
    Lits: UniformTuple<Lit>, [src]

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]

fn new_lits<Lits>(&mut self) -> Lits where
    Lits: UniformTuple<Lit>, [src]

Loading content...