Struct splr::solver::Restarter

pub struct Restarter { /* fields omitted */ }

Restarter provides restart API and holds data about restart conditions.

Trait Implementations

impl Debug for Restarter

pub fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for Restarter

pub fn default() -> Restarter

Returns the "default value" for a type.

impl Export<(usize, usize, usize, usize, usize), (RestartMode, usize)> for Restarter

pub fn exports(&self) -> (usize, usize, usize, usize, usize)

exports:

1. the number of blocking in non-stabilization
2. the number of forcing restart non-stabilization
3. the index of span of stabilization phase
4. the number of stabilization cycle shifts
5. the maximum length of stabilization span so far

 use crate::splr::{config::Config, solver::Restarter, types::*};
 let rst = Restarter::instantiate(&Config::default(), &CNFDescription::default());
 let (num_blk_non, num_stb_non, num_blk_stb, num_rst_stb, num_rst_lng) = rst.exports();
 let (rst_mode, num_stb) = rst.mode();

pub fn mode(&self) -> (RestartMode, usize)

impl<'a> ExportBox<'a, (&'a Ema2, &'a Ema2)> for Restarter

pub fn exports_box(&'a self) -> Box<RestarterEMAs<'a>>

impl Instantiate for Restarter

pub fn instantiate(config: &Config, cnf: &CNFDescription) -> Self

make and return an object from Config and CNFDescription.

pub fn handle(&mut self, e: SolverEvent)

update by a solver event.

impl RestartIF for Restarter

type Exports = (usize, usize, usize, usize, usize)

pub fn restart(&mut self) -> Option<RestartDecision>

check blocking and forcing restart condition.

pub fn stabilize(&mut self, now: usize) -> Option<(bool, bool)>

check stabilization mode and return:

pub fn update(&mut self, kind: ProgressUpdate)

update specific sub-module