rate_common::clausedatabase

Trait ClauseStorage

Source 
pub trait ClauseStorage {
    // Required methods
    fn open_clause(&mut self) -> Clause;
    fn push_literal(&mut self, literal: Literal, verbose: bool);
}

Required Methods§

Source

fn open_clause(&mut self) -> Clause

Initialze a new clause.

This must be called before adding literals with push_literal().

Source

fn push_literal(&mut self, literal: Literal, verbose: bool)

Add a literal to the current clause.

If passed literal 0, the clause will be finished and open_clause() must be called before adding literals to the next clause.

Implementors§