Struct rustsat::types::constraints::Clause

pub struct Clause { /* private fields */ }

Type representing a clause. Wrapper around a std collection to allow for changing the data structure. Optional clauses as sets will be included in the future.

Implementations

impl Clause

pub fn new() -> Self

Creates a new empty clause

pub fn lits(&self) -> &[Lit]

Gets the clause as a slice of literals

pub fn len(&self) -> usize

Gets the length of the clause

pub fn is_empty(&self) -> bool

Checks if the clause is empty

pub fn evaluate(&self, assignment: &Assignment) -> TernaryVal

Evaluates a clause under a given assignment

pub fn iter(&self) -> impl Iterator<Item = &Lit>

Gets an iterator over the clause

pub fn iter_mut(&mut self) -> impl Iterator<Item = &mut Lit>

Gets a mutable iterator over the clause

pub fn drain<R: RangeBounds<usize>>(&mut self, range: R) -> Drain<'_, Lit>

Like Vec::drain

pub fn normalize(self) -> Option<Self>

Normalizes the clause. This includes sorting the literals, removing duplicates and removing the entire clause if it is a tautology. Comparing two normalized clauses checks their logical equivalence.

pub fn sanitize(self) -> Option<Self>

Sanitizes the clause. This includes removing duplicates and removing the entire clause if it is a tautology. This preserves the order of the literals in the clause.

pub fn is_sat(&self, assign: &Assignment) -> bool

impl Clause

pub fn is_unit(&self) -> bool

Checks if the clause is a unit clause

pub fn is_binary(&self) -> bool

Checks if the clause is binary

pub fn add(&mut self, lit: Lit)

Adds a literal to the clause

pub fn remove(&mut self, lit: &Lit) -> bool

Removes the first occurrence of a literal from the clause Returns true if an occurrence was found

pub fn remove_thorough(&mut self, lit: &Lit) -> bool

Removes all occurrences of a literal from the clause

Trait Implementations

impl Clone for Clause

fn clone(&self) -> Clause

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Clause

Clauses can be printed with the Debug trait

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

Formats the value using the given formatter.

impl Default for Clause

fn default() -> Clause

Returns the “default value” for a type.

impl Display for Clause

Clauses can be printed with the Display trait

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

Formats the value using the given formatter.

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 Extend<Lit> for Clause

fn extend<T: IntoIterator<Item = Lit>>(&mut self, iter: T)

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 From<&[Lit]> for Clause

fn from(value: &[Lit]) -> Self

Converts to this type from the input type.

impl<const N: usize> From<[Lit; N]> for Clause

fn from(value: [Lit; N]) -> Self

Converts to this type from the input type.

impl FromIterator<Clause> for Cnf

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

Creates a value from an iterator.

impl<VM: ManageVars + Default> FromIterator<Clause> for SatInstance<VM>

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

Creates a value from an iterator.

impl FromIterator<Lit> for Clause

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

Creates a value from an iterator.

impl Hash for Clause

fn hash<H: Hasher>(&self, state: &mut H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl Index<usize> for Clause

type Output = Lit

The returned type after indexing.

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

Performs the indexing (container[index]) operation.

impl IndexMut<usize> for Clause

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

Performs the mutable indexing (container[index]) operation.

impl<'a> IntoIterator for &'a Clause

type Item = &'a Lit

The type of the elements being iterated over.

type IntoIter = Iter<'a, Lit>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.

impl<'a> IntoIterator for &'a mut Clause

type Item = &'a mut Lit

The type of the elements being iterated over.

type IntoIter = IterMut<'a, Lit>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.

impl IntoIterator for Clause

type Item = Lit

The type of the elements being iterated over.

type IntoIter = IntoIter<Lit>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.

impl Ord for Clause

fn cmp(&self, other: &Clause) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized + PartialOrd,

Restrict a value to a certain interval.

impl PartialEq for Clause

fn eq(&self, other: &Self) -> 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 PartialOrd for Clause

fn partial_cmp(&self, other: &Clause) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

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

This method tests less than (for self and other) and is used by the < operator.

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

This method tests less than or equal to (for self and other) and is used by the <= operator.

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

This method tests greater than (for self and other) and is used by the > operator.

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

This method tests greater than or equal to (for self and other) and is used by the >= operator.

impl Eq for Clause

impl StructuralEq for Clause