Struct batsat::callbacks::Stats

pub struct Stats {
    pub n_restarts: usize,
    pub n_clauses: u64,
    pub n_theory: u64,
    pub n_learnt: u64,
    pub n_gc: usize,
    // some fields omitted
}

Basic set of callbacks, maintaining some statistics and a "stop" predicate.

Fields

n_restarts: usize

n_clauses: u64

n_theory: u64

n_learnt: u64

n_gc: usize

Methods

impl Stats

pub fn new() -> Self

Allocate a new set of callbacks.

pub fn basic_mut(&mut self) -> &mut Basic

Cast the statistics CB into a basic CB.

Trait Implementations

impl Callbacks for Stats

fn stop(&self) -> bool

Should we stop? called regularly for asynchronous interrupts and such

fn on_restart(&mut self)

Called whenever the SAT solver restarts

fn on_gc(&mut self, _: usize, _: usize)

Called after a clause GC

fn on_new_clause(&mut self, _: &[Lit], k: ClauseKind)

Called whenever a new clause is learnt.

fn on_start(&mut self)

Called before starting to solve

fn on_simplify(&mut self)

Called whenever the solver simplifies its set of clauses

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

Called when a clause is deleted.

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

called regularly to indicate progress

fn on_result(&mut self, _s: lbool)

Called when a result is computed

impl Default for Stats

fn default() -> Self

Returns the "default value" for a type.

impl Display for Stats

fn fmt(&self, out: &mut Formatter) -> Result

Formats the value using the given formatter.