Struct splr::config::Config

pub struct Config {

    pub c_cbt_thr: DecisionLevel,
    pub c_cls_lim: usize,
    pub c_ip_int: usize,
    pub c_timeout: f64,
    pub splr_interface: bool,
    pub cnf_file: PathBuf,
    pub io_odir: PathBuf,
    pub io_pfile: PathBuf,
    pub io_rfile: PathBuf,
    pub no_color: bool,
    pub quiet_mode: bool,
    pub show_journal: bool,
    pub use_certification: bool,
    pub use_log: bool,
    pub crw_dcy_rat: f64,
    pub elm_cls_lim: usize,
    pub elm_grw_lim: usize,
    pub elm_var_occ: usize,
    pub rst_step: usize,
    pub rst_asg_len: usize,
    pub rst_asg_slw: usize,
    pub rst_asg_thr: f64,
    pub rst_lbd_len: usize,
    pub rst_lbd_slw: usize,
    pub rst_lbd_thr: f64,
    pub stg_rwd_dcy: f64,
    pub stg_rwd_val: f64,
    pub vrw_dcy_rat: f64,
    pub vrw_dcy_stp: f64,
}

Configuration built from command line options

Fields

c_cbt_thr: DecisionLevel

Dec. lvl to use chronoBT

c_cls_lim: usize

Soft limit of #clauses (6MC/GB)

c_ip_int: usize

#cls to start in-processor

c_timeout: f64

CPU time limit in sec.

splr_interface: bool

Build Splr interface

cnf_file: PathBuf

DIMACS CNF file

io_odir: PathBuf

Output directory

io_pfile: PathBuf

DRAT Cert. filename

io_rfile: PathBuf

Result filename/stdout

no_color: bool

Disable coloring

quiet_mode: bool

Disable any progress message

show_journal: bool

Show sub-module logging report

use_certification: bool

Writes a DRAT UNSAT certification file

use_log: bool

Uses Glucose-like progress report

crw_dcy_rat: f64

elm_cls_lim: usize

Max #lit for clause subsume

elm_grw_lim: usize

Grow limit of #cls in var elimination

elm_var_occ: usize

Max #cls for var elimination

rst_step: usize

#conflicts between restarts

rst_asg_len: usize

Length of assign. fast EMA

rst_asg_slw: usize

Length of assign. slow EMA

rst_asg_thr: f64

Blocking restart threshold. Originally this was the Glucose’s R.

rst_lbd_len: usize

Length of LBD fast EMA

rst_lbd_slw: usize

Length of LBD slow EMA

rst_lbd_thr: f64

Forcing restart threshold

stg_rwd_dcy: f64

Decay rate of the extra reward for staged vars

stg_rwd_val: f64

Initial value of the extra reward for staged vars

vrw_dcy_rat: f64

Var Reward Decay Rate

vrw_dcy_stp: f64

Decay increment step.

Implementations

impl Config

pub fn inject_from_args(&mut self)

impl Config

pub fn override_args(self) -> Config

Trait Implementations

impl Clone for Config

fn clone(&self) -> Config

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Config

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

Formats the value using the given formatter.

impl Default for Config

fn default() -> Self

Returns the “default value” for a type.

impl<T> From<T> for Config where
    PathBuf: From<T>, 

fn from(path: T) -> Config

Performs the conversion.

impl PropertyDereference<Tf64, f64> for Config

fn derefer(&self, k: Tf64) -> f64