Trait splr::assign::ClauseManipulateIF

pub trait ClauseManipulateIF {
    pub fn satisfies(&self, c: &[Lit]) -> bool;
    pub fn locked(&self, c: &Clause, cid: ClauseId) -> bool;
}

API for var manipulation

Required methods

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

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

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

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

Loading content...

Implementors

impl ClauseManipulateIF for AssignStack

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

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

Loading content...