Trait splr::cdb::ClauseIF

pub trait ClauseIF {
    // Required methods
    fn is_empty(&self) -> bool;
    fn is_dead(&self) -> bool;
    fn lit0(&self) -> Lit;
    fn lit1(&self) -> Lit;
    fn contains(&self, lit: Lit) -> bool;
    fn is_satisfied_under(&self, asg: &impl AssignIF) -> bool;
    fn iter(&self) -> Iter<'_, Lit>;
    fn len(&self) -> usize;
}

API for Clause, providing literal accessors.

Required Methods

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

check clause satisfiability

fn iter(&self) -> Iter<'_, Lit>

return an iterator over its literals.

fn len(&self) -> usize

return the number of literals.

Object Safety

This trait is not object safe.

Implementors

impl ClauseIF for Clause