Struct rustsat::instances::Cnf

pub struct Cnf { /* private fields */ }

Simple type representing a CNF formula. Other than SatInstance<VM>, this type only supports clauses and does have an internal variable manager.

Implementations

impl Cnf

pub fn new() -> Cnf

Creates a new Cnf

pub fn with_capacity(capacity: usize) -> Cnf

Creates a new Cnf with a given capacity of clauses

pub fn try_reserve(&mut self, additional: usize) -> Result<(), TryReserveError>

Tries to reserve memory for at least additional new clauses

pub fn shrink_to_fit(&mut self)

Shrinks the allocated memory of the Cnf to fit the number of clauses

pub fn capacity(&self) -> usize

Gets the capacity of the Cnf

pub fn add_clause(&mut self, clause: Clause)

Adds a clause to the CNF

pub fn add_unit(&mut self, unit: Lit)

Adds a unit clause to the CNF

pub fn add_binary(&mut self, lit1: Lit, lit2: Lit)

Adds a binary clause to the CNF

pub fn add_ternary(&mut self, lit1: Lit, lit2: Lit, lit3: Lit)

Adds a ternary clause to the CNF

pub fn is_empty(&self) -> bool

Checks if the CNF is empty

pub fn len(&self) -> usize

Returns the number of clauses in the instance

pub fn add_lit_impl_lit(&mut self, a: Lit, b: Lit)

See atomics::lit_impl_lit

pub fn add_lit_impl_clause(&mut self, a: Lit, b: &[Lit])

See atomics::lit_impl_clause

pub fn add_lit_impl_cube(&mut self, a: Lit, b: &[Lit])

Adds an implication of form a -> (b1 & b2 & … & bm)

pub fn add_cube_impl_lit(&mut self, a: &[Lit], b: Lit)

See atomics::cube_impl_lit

pub fn add_clause_impl_lit(&mut self, a: &[Lit], b: Lit)

Adds an implication of form (a1 | a2 | … | an) -> b

pub fn add_cube_impl_clause(&mut self, a: &[Lit], b: &[Lit])

See atomics::cube_impl_clause

pub fn add_clause_impl_clause(&mut self, a: &[Lit], b: &[Lit])

Adds an implication of form (a1 | a2 | … | an) -> (b1 | b2 | … | bm)

pub fn add_clause_impl_cube(&mut self, a: &[Lit], b: &[Lit])

Adds an implication of form (a1 | a2 | … | an) -> (b1 & b2 & … & bm)

pub fn add_cube_impl_cube(&mut self, a: &[Lit], b: &[Lit])

Adds an implication of form (a1 & a2 & … & an) -> (b1 & b2 & … & bm)

pub fn join(self, other: Cnf) -> Cnf

Joins the current CNF with another one. Like Cnf::extend but consumes the object and returns a new object.

pub fn iter(&self) -> Iter<'_, Clause>

Returns an iterator over references to the clauses

pub fn iter_mut(&mut self) -> IterMut<'_, Clause>

Returns an iterator over mutable references to the clauses

pub fn normalize(self) -> Self

Normalizes the CNF. This includes normalizing and sorting the clauses, removing duplicates and tautologies. Comparing two normalized CNFs is equal to comparing sets of sets of literals.

pub fn sanitize(self) -> Self

Sanitizes the CNF by removing tautologies, removing redundant literals, etc.

Trait Implementations

impl Clone for Cnf

fn clone(&self) -> Cnf

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl CollectClauses for Cnf

fn n_clauses(&self) -> usize

Gets the number of clauses in the collection

impl Debug for Cnf

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for Cnf

fn default() -> Cnf

Returns the “default value” for a type.

impl Extend<Clause> for Cnf

fn extend<Iter: IntoIterator<Item = Clause>>(&mut self, iter: Iter)

Extends a collection with the contents of an iterator.

fn extend_one(&mut self, item: A)

🔬This is a nightly-only experimental API. (extend_one)

Extends a collection with exactly one element.

fn extend_reserve(&mut self, additional: usize)

🔬This is a nightly-only experimental API. (extend_one)

Reserves capacity in a collection for the given number of additional elements.

impl FromIterator<Clause> for Cnf

fn from_iter<T: IntoIterator<Item = Clause>>(iter: T) -> Self

Creates a value from an iterator.

impl Index<usize> for Cnf

type Output = Clause

The returned type after indexing.

fn index(&self, index: usize) -> &Self::Output

Performs the indexing (container[index]) operation.

impl IntoIterator for Cnf

type Item = Clause

The type of the elements being iterated over.

type IntoIter = IntoIter<Clause>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.

impl PartialEq for Cnf

fn eq(&self, other: &Cnf) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for Cnf

impl StructuralEq for Cnf

impl StructuralPartialEq for Cnf