[−][src]Trait batsat::callbacks::Callbacks

pub trait Callbacks: Sized {
    pub fn on_start(&mut self) { ... }

    pub fn on_simplify(&mut self) { ... }

    pub fn on_restart(&mut self) { ... }

    pub fn on_gc(&mut self, _old_size: usize, _new_size: usize) { ... }

    pub fn on_new_clause(&mut self, _c: &[Lit], _src: Kind) { ... }

    pub fn on_delete_clause(&mut self, _c: &[Lit]) { ... }

    pub fn on_progress<F>(&mut self, _f: F)
    where
        F: FnOnce() -> ProgressStatus,
    { ... }

    pub fn on_result(&mut self, _s: lbool) { ... }

    pub fn stop(&self) -> bool { ... }
}

Basic callbacks to the solver

Typically intended for printing/statistics

Provided methods

pub fn on_start(&mut self)[src]

Called before starting to solve

pub fn on_simplify(&mut self)[src]

Called whenever the solver simplifies its set of clauses

pub fn on_restart(&mut self)[src]

Called whenever the SAT solver restarts

pub fn on_gc(&mut self, _old_size: usize, _new_size: usize)[src]

Called after a clause GC

pub fn on_new_clause(&mut self, _c: &[Lit], _src: Kind)[src]

Called whenever a new clause is learnt.

Params

  • c: list of literals of the clause
  • src: specifies where the clause comes from

pub fn on_delete_clause(&mut self, _c: &[Lit])[src]

Called when a clause is deleted.

pub fn on_progress<F>(&mut self, _f: F) where
    F: FnOnce() -> ProgressStatus, [src]

called regularly to indicate progress

pub fn on_result(&mut self, _s: lbool)[src]

Called when a result is computed

pub fn stop(&self) -> bool[src]

Should we stop? called regularly for asynchronous interrupts and such

Loading content...

Implementors

impl Callbacks for Basic[src]

impl Callbacks for Stats[src]

Loading content...