Struct splr::state::State

pub struct State {

    pub config: Config,
    pub cnf: CNFDescription,
    pub stats: [usize; 7],
    pub restart: RestartManager,
    pub stm: StageManager,
    pub target: CNFDescription,
    pub reflection_interval: usize,
    pub b_lvl: Ema,
    pub c_lvl: Ema,
    pub e_mode: Ema2,
    pub e_mode_threshold: f64,
    pub exploration_rate_ema: Ema,
    pub last_asg: usize,
    pub new_learnt: Vec<Lit>,
    pub derive20: Vec<ClauseId>,
    pub progress_cnt: usize,
    pub record: ProgressRecord,
    pub sls_index: usize,
    pub start: Instant,
    pub time_limit: f64,
    /* private fields */
}

Data storage for Solver.

Fields

config: Config

solver configuration

cnf: CNFDescription

the problem.

stats: [usize; 7]

collection of statistics data

restart: RestartManager

stm: StageManager

StageManager

target: CNFDescription

problem description

reflection_interval: usize

strategy adjustment interval in conflict

b_lvl: Ema

EMA of backjump levels

c_lvl: Ema

EMA of conflicting levels

e_mode: Ema2

EMA of c_lbd - b_lbd, or Exploration vs. Eploitation

e_mode_threshold: f64

exploration_rate_ema: Ema

last_asg: usize

hold the previous number of non-conflicting assignment

new_learnt: Vec<Lit>

working place to build learnt clauses

derive20: Vec<ClauseId>

working place to store given clauses’ ids which is used to derive a good learnt

progress_cnt: usize

progress invocation counter

record: ProgressRecord

keep the previous statistics values

sls_index: usize

progress of SLS

start: Instant

start clock for timeout handling

time_limit: f64

upper limit for timeout handling

Trait Implementations

impl Clone for State

fn clone(&self) -> State

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for State

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

Formats the value using the given formatter.

impl Default for State

fn default() -> State

Returns the “default value” for a type.

impl Display for State

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

Formats the value using the given formatter.

impl Index<LogF64Id> for State

type Output = f64

The returned type after indexing.

fn index(&self, i: LogF64Id) -> &Self::Output

Performs the indexing (container[index]) operation.

impl Index<LogUsizeId> for State

type Output = usize

The returned type after indexing.

fn index(&self, i: LogUsizeId) -> &Self::Output

Performs the indexing (container[index]) operation.

impl Index<Stat> for State

type Output = usize

The returned type after indexing.

fn index(&self, i: Stat) -> &usize

Performs the indexing (container[index]) operation.

impl IndexMut<LogF64Id> for State

fn index_mut(&mut self, i: LogF64Id) -> &mut Self::Output

Performs the mutable indexing (container[index]) operation.

impl IndexMut<LogUsizeId> for State

fn index_mut(&mut self, i: LogUsizeId) -> &mut Self::Output

Performs the mutable indexing (container[index]) operation.

impl IndexMut<Stat> for State

fn index_mut(&mut self, i: Stat) -> &mut usize

Performs the mutable indexing (container[index]) operation.

impl Instantiate for State

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

make and return an object from Config and CNFDescription.

fn handle(&mut self, e: SolverEvent)

update by a solver event.

impl PropertyDereference<Tusize, usize> for State

fn derefer(&self, k: Tusize) -> usize

impl PropertyReference<TEma, EmaView> for State

fn refer(&self, k: TEma) -> &EmaView

impl StateIF for State

fn progress<A, C>(&mut self, asg: &A, cdb: &C)

where A: PropertyDereference<Tusize, usize> + PropertyDereference<Tf64, f64> + PropertyReference<TEma, EmaView>, C: PropertyDereference<Tusize, usize> + PropertyDereference<Tf64, f64> + PropertyReference<TEma, EmaView>,

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

fn is_timeout(&self) -> bool

return true if it is timed out.

fn elapsed(&self) -> Option<f64>

return elapsed time as a fraction. return None if something is wrong.

fn progress_header(&mut self)

write a header of stat data to stdio.

fn flush<S: AsRef<str>>(&self, mes: S)

write a short message to stdout.

fn log<S: AsRef<str>>( &mut self, tick: Option<(Option<usize>, Option<usize>, usize)>, mes: S )

write a one-line message as log.