Trait ClauseIterator

pub trait ClauseIterator {
    // Required method
    fn clause(&mut self, clause: &[i32]) -> bool;
}

Allows to traverse all remaining irredundant clauses. Satisfied and eliminated clauses are not included, nor any derived units unless such a unit literal is frozen. Falsified literals are skipped. If the solver is inconsistent only the empty clause is traversed.

If ‘clause’ returns false traversal aborts early.

Required Methods

fn clause(&mut self, clause: &[i32]) -> bool

Implementors