[−][src]Struct varisat::CnfFormula
A formula in conjunctive normal form (CNF).
Equivalent to Vec<Vec
Methods
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 iter(&self) -> impl Iterator<Item = &[Lit]>
[src]
Iterator over all clauses.
Trait Implementations
impl Debug for CnfFormula
[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]
fn eq(&self, other: &CnfFormula) -> bool
[src]
#[must_use]
fn ne(&self, other: &Rhs) -> bool
1.0.0[src]
This method tests for !=
.
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]
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>
[src]
Iterator over multiple new variables.
ⓘImportant traits for NewVarIter<'a, F, V>fn new_lit_iter(&mut self, count: usize) -> NewVarIter<Self, Lit>
[src]
Iterator over multiple new literals.
fn new_vars<Vars>(&mut self) -> Vars where
Vars: UniformTuple<Var>,
[src]
Vars: UniformTuple<Var>,
Add multiple new variables and return them. Read more
fn new_lits<Lits>(&mut self) -> Lits where
Lits: UniformTuple<Lit>,
[src]
Lits: UniformTuple<Lit>,
Add multiple new variables and return them as positive literals. Read more
impl Default for CnfFormula
[src]
fn default() -> CnfFormula
[src]
Auto Trait Implementations
impl Send for CnfFormula
impl Sync for CnfFormula
Blanket Implementations
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>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<Reference, Outer, OuterFieldType, Inner> HasPart<Nested<Outer, Inner>> for Reference where
Inner: Part,
Outer: Part<PartType = Field<OuterFieldType>>,
OuterFieldType: HasPart<Inner, RawTarget = OuterFieldType> + PartialRefTarget + ?Sized,
Reference: HasPart<Outer> + ?Sized,
[src]
Inner: Part,
Outer: Part<PartType = Field<OuterFieldType>>,
OuterFieldType: HasPart<Inner, RawTarget = OuterFieldType> + PartialRefTarget + ?Sized,
Reference: HasPart<Outer> + ?Sized,