Struct splr::cdb::Clause

pub struct Clause {
    pub rank: u16,
    pub rank_old: u16,
    pub search_from: u16,
    /* private fields */
}

A representation of ‘clause’

Fields

rank: u16

A static clause evaluation criterion like LBD, NDD, or something.

rank_old: u16

A record of the rank at previos stage.

search_from: u16

the index from which propagate starts searching an un-falsified literal. Since it’s just a hint, we don’t need u32 or usize.

Implementations

impl Clause

pub fn update_lbd( &mut self, asg: &impl AssignIF, lbd_temp: &mut [usize] ) -> usize

update rank field with the present LBD.

Trait Implementations

impl ClauseIF for Clause

fn is_empty(&self) -> bool

return true if it contains no literals; a clause after unit propagation.

fn is_dead(&self) -> bool

return true if it contains no literals; a clause after unit propagation.

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

return an iterator over its literals.

fn lit0(&self) -> Lit

return 1st watch

fn lit1(&self) -> Lit

return 2nd watch

fn contains(&self, lit: Lit) -> bool

return true if the clause contains the literal

fn is_satisfied_under(&self, asg: &impl AssignIF) -> bool

check clause satisfiability

fn len(&self) -> usize

return the number of literals.

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

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

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

Formats the value using the given formatter.

impl FlagIF for Clause

type FlagType = FlagClause

fn is(&self, flag: Self::FlagType) -> bool

return true if the flag in on.

fn set(&mut self, f: Self::FlagType, b: bool)

set the flag.

fn turn_off(&mut self, flag: Self::FlagType)

toggle the flag off.

fn turn_on(&mut self, flag: Self::FlagType)

toggle the flag on.

fn toggle(&mut self, flag: Self::FlagType)

impl From<&Clause> for Vec<i32>

fn from(c: &Clause) -> Vec<i32>

Converts to this type from the input type.

impl Index<Range<usize>> for Clause

type Output = [Lit]

The returned type after indexing.

fn index(&self, r: Range<usize>) -> &[Lit]

Performs the indexing (container[index]) operation.

impl Index<RangeFrom<usize>> for Clause

type Output = [Lit]

The returned type after indexing.

fn index(&self, r: RangeFrom<usize>) -> &[Lit]

Performs the indexing (container[index]) operation.

impl Index<usize> for Clause

type Output = Lit

The returned type after indexing.

fn index(&self, i: usize) -> &Lit

Performs the indexing (container[index]) operation.

impl IndexMut<Range<usize>> for Clause

fn index_mut(&mut self, r: Range<usize>) -> &mut [Lit]

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

impl IndexMut<RangeFrom<usize>> for Clause

fn index_mut(&mut self, r: RangeFrom<usize>) -> &mut [Lit]

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

impl IndexMut<usize> for Clause

fn index_mut(&mut self, i: usize) -> &mut Lit

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

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