Struct splr::cdb::Clause

pub struct Clause {
    pub rank: u16,
    pub search_from: usize,
    // some fields omitted
}

A representation of ‘clause’

Fields

rank: u16

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

search_from: usize

the index from which propagate starts searching an un-falsified literal.

Implementations

impl Clause

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

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<A>(&self, asg: &A) -> bool where
    A: AssignIF, 

check clause satisfiability

fn len(&self) -> usize

return the number of literals.

fn timestamp(&self) -> usize

return timestamp

fn to_vivify(&self, initial_stage: bool) -> Option<f64>

return true if the clause should try vivification

fn vivified(&mut self)

clear flags about vivification

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

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

return true if the flag in on.

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

set the flag.

fn turn_off(&mut self, flag: Flag)

toggle the flag off.

fn turn_on(&mut self, flag: Flag)

toggle the flag on.

impl From<&'_ Clause> for Vec<i32>

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

Performs the conversion.

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<Clause> 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: &Clause) -> bool

This method tests for !=.

impl PartialOrd<Clause> 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 StructuralPartialEq for Clause