Struct splr::cdb::ClauseId

pub struct ClauseId {
    pub ordinal: u32,
}

Clause identifier, or clause index, starting with one. Note: ids are re-used after 'garbage collection'.

Fields

ordinal: u32

a sequence number.

Implementations

impl ClauseId

pub fn is_none(&self) -> bool

Trait Implementations

impl ClauseIdIF for ClauseId

pub fn is_lifted_lit(self) -> bool

return true if the clause is generated from a literal by Eliminator.

impl Clone for ClauseId

pub fn clone(&self) -> ClauseId

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Copy for ClauseId

impl Debug for ClauseId

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

Formats the value using the given formatter.

impl Default for ClauseId

pub fn default() -> Self

return the default empty clause, used in a reason slot or no conflict path.

impl Display for ClauseId

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

Formats the value using the given formatter.

impl Eq for ClauseId

impl From<ClauseId> for Lit

pub fn from(cid: ClauseId) -> Self

Performs the conversion.

impl From<Lit> for ClauseId

pub fn from(l: Lit) -> ClauseId

Performs the conversion.

impl From<usize> for ClauseId

pub fn from(u: usize) -> ClauseId

Performs the conversion.

impl Index<&'_ ClauseId> for ClauseDB

type Output = Clause

The returned type after indexing.

pub fn index(&self, cid: &ClauseId) -> &Clause

Performs the indexing (container[index]) operation.

impl Index<ClauseId> for ClauseDB

type Output = Clause

The returned type after indexing.

pub fn index(&self, cid: ClauseId) -> &Clause

Performs the indexing (container[index]) operation.

impl IndexMut<&'_ ClauseId> for ClauseDB

pub fn index_mut(&mut self, cid: &ClauseId) -> &mut Clause

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

impl IndexMut<ClauseId> for ClauseDB

pub fn index_mut(&mut self, cid: ClauseId) -> &mut Clause

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

impl Ord for ClauseId

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

This method returns an Ordering between self and other.

#[must_use]pub fn max(self, other: Self) -> Self

Compares and returns the maximum of two values.

#[must_use]pub fn min(self, other: Self) -> Self

Compares and returns the minimum of two values.

#[must_use]pub fn clamp(self, min: Self, max: Self) -> Self

Restrict a value to a certain interval.

impl PartialEq<ClauseId> for ClauseId

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

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

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

This method tests for !=.

impl PartialOrd<ClauseId> for ClauseId

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

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

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

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

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

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

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

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

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

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

impl StructuralEq for ClauseId

impl StructuralPartialEq for ClauseId