Trait batsat::interface::Theory

pub trait Theory<S: TheoryArgument>: Debug {
    fn final_check(&mut self, _: &mut S, model: &[Lit]) -> FinalCheckRes;
    fn create_level(&mut self);
    fn pop_level(&mut self, n: u32);
    fn on_add_clause(&mut self, c: &S::Clause, learnt: bool);
}

Theory that parametrizes the solver and can react on events

Required Methods

fn final_check(&mut self, _: &mut S, model: &[Lit]) -> FinalCheckRes

Check the model candidate model thoroughly.

If the partial model isn’t satisfiable in the theory then this must return FinalCheckRes::Conflict and push a conflict clause.

fn create_level(&mut self)

Push a new backtracking level

fn pop_level(&mut self, n: u32)

Pop n levels from the stack

fn on_add_clause(&mut self, c: &S::Clause, learnt: bool)

Called whenever the solver gets a new clause

Implementors