Struct splr::state::State

pub struct State {
    pub config: Config,
    pub stats: [usize; 4],
    pub target: CNFDescription,
    pub reflection_interval: usize,
    pub to_vivify: f64,
    pub vivify_thr: usize,
    pub b_lvl: Ema,
    pub c_lvl: Ema,
    pub conflicts: Vec<Lit>,
    pub last_asg: usize,
    pub new_learnt: Vec<Lit>,
    pub derive20: Vec<ClauseId>,
    pub progress_cnt: usize,
    pub record: ProgressRecord,
    pub start: Instant,
    pub time_limit: f64,
    // some fields omitted
}

Data storage for Solver.

Fields

config: Config

solver configuration

stats: [usize; 4]

collection of statistics data

target: CNFDescription

problem description

reflection_interval: usize

strategy adjustment interval in conflict

to_vivify: f64

time to execute vivification

vivify_thr: usize

loop limit of vivification loop

b_lvl: Ema

EMA of backjump levels

c_lvl: Ema

EMA of conflicting levels

conflicts: Vec<Lit>

hold conflicting literals for UNSAT problems

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

start: Instant

start clock for timeout handling

time_limit: f64

upper limit for timeout handling

Trait Implementations

impl Debug for State

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

Formats the value using the given formatter.

impl Default for State

pub fn default() -> State

Returns the "default value" for a type.

impl Display for State

pub 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.

pub 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.

pub 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.

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

Performs the indexing (container[index]) operation.

impl IndexMut<LogF64Id> for State

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

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

impl IndexMut<LogUsizeId> for State

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

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

impl IndexMut<Stat> for State

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

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

impl Instantiate for State

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

make and return an object from Config and CNFDescription.

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

update by a solver event.

impl StateIF for State

pub fn is_timeout(&self) -> bool

return true if it is timed out.

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

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

pub fn progress_header(&mut self)

write a header of stat data to stdio.

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

write a short message to stdout.

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

write a one-line message as log.

pub fn progress<'r, A, C, E, R>(
    &mut self,
    asg: &A,
    cdb: &C,
    elim: &E,
    rst: &'r R
) where
    A: AssignIF + VarSelectIF + Export<(usize, usize, usize, f64), ()>,
    C: Export<(usize, usize, usize, usize, usize, usize), bool>,
    E: Export<(usize, usize, f64), ()>,
    R: RestartIF + ExportBox<'r, RestarterEMAs<'r>>, 

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