Struct splr::state::State

pub struct State {
    pub root_level: usize,
    pub num_vars: usize,
    pub num_solved_vars: usize,
    pub num_eliminated_vars: usize,
    pub config: Config,
    pub rst: RestartExecutor,
    pub stats: [usize; 19],
    pub strategy: SearchStrategy,
    pub target: CNFDescription,
    pub use_chan_seok: bool,
    pub ok: bool,
    pub b_lvl: Ema,
    pub c_lvl: Ema,
    pub model: Vec<Lbool>,
    pub conflicts: Vec<Lit>,
    pub new_learnt: Vec<Lit>,
    pub an_seen: Vec<bool>,
    pub last_asg: usize,
    pub last_dl: Vec<Lit>,
    pub lbd_temp: Vec<usize>,
    pub slack_duration: isize,
    pub stagnated: bool,
    pub start: SystemTime,
    pub time_limit: f64,
    pub record: ProgressRecord,
    pub use_progress: bool,
    pub progress_cnt: usize,
    pub progress_log: bool,
    pub development: Vec<(usize, f64, f64, f64, f64, f64)>,
}

Data storage for Solver

Fields

root_level: usize

num_vars: usize

num_solved_vars: usize

num_eliminated_vars: usize

config: Config

rst: RestartExecutor

stats: [usize; 19]

strategy: SearchStrategy

target: CNFDescription

use_chan_seok: bool

ok: bool

MISC

b_lvl: Ema

c_lvl: Ema

model: Vec<Lbool>

conflicts: Vec<Lit>

new_learnt: Vec<Lit>

an_seen: Vec<bool>

last_asg: usize

last_dl: Vec<Lit>

lbd_temp: Vec<usize>

slack_duration: isize

stagnated: bool

start: SystemTime

time_limit: f64

record: ProgressRecord

use_progress: bool

progress_cnt: usize

progress_log: bool

development: Vec<(usize, f64, f64, f64, f64, f64)>

Trait Implementations

impl StateIF for State

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 flush(&self, mes: &str)

write a short message to stdout.

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

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

impl Default for State

fn default() -> State

Returns the "default value" for a type.

impl Debug for State

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

Formats the value using the given formatter.

impl Display for State

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

Formats the value using the given formatter.