Struct splr::config::Config[−][src]

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 submodule logging report

use_certification: bool

Writes a DRAT UNSAT certification file

use_log: bool

Uses Glucose-like progress report

crw_dcy_rat: f64elm_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[src]

pub fn inject_from_args(&mut self)[src]

impl Config[src]

pub fn override_args(self) -> Config[src]

Trait Implementations

impl Clone for Config[src]

impl Debug for Config[src]

impl Default for Config[src]

impl<T> From<T> for Config where
    PathBuf: From<T>, [src]

Auto Trait Implementations

impl RefUnwindSafe for Config

impl Send for Config

impl Sync for Config

impl Unpin for Config

impl UnwindSafe for Config

Blanket Implementations

impl<T> Any for T where
    T: 'static + ?Sized, [src]

impl<T> Borrow<T> for T where
    T: ?Sized, [src]

impl<T> BorrowMut<T> for T where
    T: ?Sized, [src]

impl<T> From<T> for T[src]

impl<T, U> Into<U> for T where
    U: From<T>, [src]

impl<T> ToOwned for T where
    T: Clone, [src]

type Owned = T

The resulting type after obtaining ownership.

impl<T, U> TryFrom<U> for T where
    U: Into<T>, [src]

type Error = Infallible

The type returned in the event of a conversion error.

impl<T, U> TryInto<U> for T where
    U: TryFrom<T>, [src]

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.