[−][src]Trait splr::traits::StateIF

pub trait StateIF {
    fn new(config: &Config, cnf: CNFDescription) -> State;

    fn num_unsolved_vars(&self) -> usize;

    fn is_timeout(&self) -> bool;

    fn adapt_strategy(&mut self, cdb: &mut ClauseDB, vdb: &mut VarDB);

    fn progress_header(&self);

    fn progress(&mut self, cdb: &ClauseDB, vars: &VarDB, mes: Option<&str>);

    fn flush(&self, mes: &str);
}

API for state/statistics management, providing progress.

Required methods

fn new(config: &Config, cnf: CNFDescription) -> State

return an initialized state based on solver configuration and data about a CNF file.

fn num_unsolved_vars(&self) -> usize

return the number of unsolved vars.

fn is_timeout(&self) -> bool

return true if it is timed out.

fn adapt_strategy(&mut self, cdb: &mut ClauseDB, vdb: &mut VarDB)

change heuristics based on stat data.

fn progress_header(&self)

write a header of stat data to stdio.

fn progress(&mut self, cdb: &ClauseDB, vars: &VarDB, mes: Option<&str>)

write stat data to stdio.

fn flush(&self, mes: &str)

write a short message to stdout.

Loading content...

Implementors

impl StateIF for State[src]

fn progress(&mut self, cdb: &ClauseDB, vars: &VarDB, mes: Option<&str>)[src]

mes should be shorter than or equal to 9, or 8 + a delimiter.

Loading content...