[−][src]Trait splr::cdb::LBDIF

pub trait LBDIF {
    pub fn compute_lbd<A>(&mut self, asg: &A, vec: &[Lit]) -> usize
    where
        A: AssignIF;

    pub fn compute_lbd_of<A>(&mut self, asg: &A, cid: ClauseId) -> usize
    where
        A: AssignIF;

    pub fn reset_lbd<A>(&mut self, asg: &A, all: bool)
    where
        A: AssignIF;
}

API to calculate LBD.

Required methods

pub fn compute_lbd<A>(&mut self, asg: &A, vec: &[Lit]) -> usize where
    A: AssignIF, [src]

return the LBD value for a set of literals.

pub fn compute_lbd_of<A>(&mut self, asg: &A, cid: ClauseId) -> usize where
    A: AssignIF, [src]

return the LBD value of clause cid.

pub fn reset_lbd<A>(&mut self, asg: &A, all: bool) where
    A: AssignIF, [src]

re-calculate the LBD values of all (learnt) clauses.

Loading content...

Implementors

impl LBDIF for ClauseDB[src]

Loading content...