[−][src]Struct varisat_formula::cnf::CnfFormula
A formula in conjunctive normal form (CNF).
Equivalent to Vec<Vec
Implementations
impl CnfFormula
[src]
pub fn new() -> CnfFormula
[src]
Create an empty CNF formula.
pub fn var_count(&self) -> usize
[src]
Number of variables in the formula.
This also counts missing variables if a variable with a higher index is present. A vector of this length can be indexed with the variable indices present.
pub fn set_var_count(&mut self, count: usize)
[src]
Increase the number of variables in the formula.
If the parameter is less than the current variable count do nothing.
pub fn len(&self) -> usize
[src]
Number of clauses in the formula.
pub fn is_empty(&self) -> bool
[src]
Whether the set of clauses is empty.
pub fn iter(&self) -> impl Iterator<Item = &[Lit]>
[src]
Iterator over all clauses.
Trait Implementations
impl Debug for CnfFormula
[src]
impl Default for CnfFormula
[src]
fn default() -> CnfFormula
[src]
impl Eq for CnfFormula
[src]
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]
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;
[src]
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;
[src]
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
[src]
fn new_lits<Lits: UniformTuple<Lit>>(&mut self) -> Lits
[src]
impl<Clauses, Item> From<Clauses> for CnfFormula where
Clauses: IntoIterator<Item = Item>,
Item: Borrow<[Lit]>,
[src]
Clauses: IntoIterator<Item = Item>,
Item: Borrow<[Lit]>,
Convert an iterable of Lit
slices into a CnfFormula
fn from(clauses: Clauses) -> CnfFormula
[src]
impl PartialEq<CnfFormula> for CnfFormula
[src]
impl StructuralEq for CnfFormula
[src]
Auto Trait Implementations
impl RefUnwindSafe for CnfFormula
impl Send for CnfFormula
impl Sync for CnfFormula
impl Unpin for CnfFormula
impl UnwindSafe for CnfFormula
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,