Struct 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 with_capacity(capacity: usize) -> Self

Creates a new empty clause with at least the specified capacity.

Uses Vec::with_capacity internally.

pub fn reserve(&mut self, additional: usize)

Reserves capacity for at least additional more literals.

Uses Vec::reserve internally.

pub fn reserve_exact(&mut self, additional: usize)

Reserves the minimum capacity for at least additional more literals.

Uses Vec::reserve_exact internally.

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

Tries to reserve capacity for at least additional more literals.

Uses Vec::try_reserve internally.

Errors

If the capacity overflows, or the allocator reports a failure, then an error is returned.

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

Tries to reserve the minimum capacity for at least additional more literals.

Uses Vec::try_reserve_exact internally.

Errors

If the capacity overflows, or the allocator reports a failure, then an error is returned.

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

Methods from Deref<Target = Cl>

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 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 evaluate(&self, assignment: &Assignment) -> TernaryVal

Evaluates a clause under a given assignment

pub fn is_tautology(&self) -> bool

Checks whether the clause is tautological

pub fn sort(&mut self)

Performs slice::sort_unstable on the 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

Trait Implementations

impl AsMut<[Lit]> for Clause

fn as_mut(&mut self) -> &mut [Lit]

Converts this type into a mutable reference of the (usually inferred) input type.

impl AsMut<Cl> for Clause

fn as_mut(&mut self) -> &mut Cl

Converts this type into a mutable reference of the (usually inferred) input type.

impl AsRef<[Lit]> for Clause

fn as_ref(&self) -> &[Lit]

Converts this type into a shared reference of the (usually inferred) input type.

impl AsRef<Cl> for Clause

fn as_ref(&self) -> &Cl

Converts this type into a shared reference of the (usually inferred) input type.

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 ConstraintLike<Var> for Clause

Available on crate feature proof-logging only.

fn rhs(&self) -> isize

Gets the operator and right hand side of the constraint

fn sum_iter(&self) -> impl Iterator<Item = (isize, Axiom<Var>)>

Gets an iterator over the coefficient literal pairs in the constraint

impl Debug for Clause

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 Deref for Clause

type Target = Cl

The resulting type after dereferencing.

fn deref(&self) -> &Self::Target

Dereferences the value.

impl DerefMut for Clause

fn deref_mut(&mut self) -> &mut Self::Target

Mutably dereferences the value.

impl<'de> Deserialize<'de> for Clause

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Display for Clause

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

Formats the value using the given formatter.

impl<'a> Extend<&'a Clause> for Solver

fn extend<T: IntoIterator<Item = &'a Clause>>(&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 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<Clause> for Solver

fn extend<T: IntoIterator<Item = Clause>>(&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 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 From<Clause> for CardConstraint

fn from(value: Clause) -> Self

Converts to this type from the input type.

impl From<Clause> for PbConstraint

fn from(value: Clause) -> 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 Instance<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<'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,

Restrict a value to a certain interval.

impl PartialEq for Clause

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

Tests for self and other values to be equal, and is used by ==.

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

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

Tests less than (for self and other) and is used by the < operator.

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

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

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

Tests greater than (for self and other) and is used by the > operator.

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

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

impl Serialize for Clause

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Eq for Clause

impl StructuralPartialEq for Clause