Struct splr::var::VarDB

pub struct VarDB {
    pub lbd_temp: Vec<usize>,
    pub activity_inc: f64,
    pub activity_decay: f64,
    pub activity_decay_max: f64,
    // some fields omitted
}

Structure for variables.

Fields

lbd_temp: Vec<usize>

activity_inc: f64

activity_decay: f64

activity_decay_max: f64

Trait Implementations

impl VarDBIF for VarDB

fn new(n: usize) -> Self

return a new instance.

fn len(&self) -> usize

return the length of vars.

fn is_empty(&self) -> bool

return true if it's empty.

fn assigned(&self, l: Lit) -> Lbool

return the 'value' of a given literal.

fn locked(&self, c: &Clause, cid: ClauseId) -> bool

return true is the clause is the reason of the assignment.

fn satisfies(&self, vec: &[Lit]) -> bool

return true if the set of literals is satisfiable under the current assignment.

fn update_stat(&mut self, state: &State)

copy some stat data from State.

fn compute_lbd(&self, vec: &[Lit], keys: &mut [usize]) -> usize

return a LBD value for the set of literals.

fn bump_activity(&mut self, vi: VarId)

update the variable's activity.

fn scale_activity(&mut self)

increment activity step.

impl Default for VarDB

fn default() -> VarDB

Returns the "default value" for a type.

impl Index<usize> for VarDB

type Output = Var

The returned type after indexing.

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

Performs the indexing (container[index]) operation.

impl Index<Range<usize>> for VarDB

type Output = [Var]

The returned type after indexing.

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

Performs the indexing (container[index]) operation.

impl Index<RangeFrom<usize>> for VarDB

type Output = [Var]

The returned type after indexing.

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

Performs the indexing (container[index]) operation.

impl IndexMut<usize> for VarDB

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

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

impl IndexMut<Range<usize>> for VarDB

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

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

impl IndexMut<RangeFrom<usize>> for VarDB

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

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

impl Debug for VarDB

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

Formats the value using the given formatter.