[−][src]Trait splr::traits::VarDBIF

pub trait VarDBIF {
    fn new(n: usize) -> Self;

    fn len(&self) -> usize;

    fn is_empty(&self) -> bool;

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

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

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

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

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

    fn bump_activity(&mut self, vi: VarId);

    fn scale_activity(&mut self);
}

API for var DB like assigned, locked, compute_lbd and so on.

Required methods

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, c: &[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.

Loading content...

Implementors

impl VarDBIF for VarDB[src]

Loading content...