Struct splr::config::Config

pub struct Config {
    pub c_cbt_thr: DecisionLevel,
    pub c_cls_lim: usize,
    pub c_ip_int: usize,
    pub c_tout: f64,
    pub splr_interface: bool,
    pub cnf_file: PathBuf,
    pub io_dump: usize,
    pub io_odir: PathBuf,
    pub io_pfile: PathBuf,
    pub io_rfile: PathBuf,
    pub no_color: bool,
    pub quiet_mode: bool,
    pub use_certification: bool,
    pub use_log: bool,
    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_ccc_thr: f64,
    pub rst_lbd_len: usize,
    pub rst_lbd_slw: usize,
    pub rst_lbd_thr: f64,
    pub rst_mld_thr: f64,
    pub rst_stb_scl: f64,
    pub viv_beg: f64,
    pub viv_end: f64,
    pub viv_int: usize,
    pub viv_scale: f64,
    pub vrw_dcy_beg: f64,
    pub vrw_dcy_end: f64,
    // some fields omitted
}

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_tout: f64

CPU time limit in sec. .

splr_interface: bool

Build Splr interface .

cnf_file: PathBuf

DIMACS CNF file .

io_dump: usize

Interval for dumping stat data .

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

use_certification: bool

Writes a DRAT UNSAT certification file

use_log: bool

Uses Glucose-like progress report

elm_cls_lim: usize

Max #lit for clause subsume .

elm_grw_lim: usize

Grow limit of #cls in var elim. .

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 .

rst_ccc_thr: f64

Conflict Correlation threshold

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 .

rst_mld_thr: f64

Usability to restart .

rst_stb_scl: f64

Stabilizer scaling .

viv_beg: f64

Lower bound of vivif. loop .

viv_end: f64

Upper bound of vivif. loop .

viv_int: usize

Vivification interval .

viv_scale: f64

#reduction for next vivif. .

vrw_dcy_beg: f64

Initial var reward decay .

vrw_dcy_end: f64

Maximum var reward decay .

Implementations

impl Config

pub fn override_args(self) -> Config

pub fn use_reduce(&self) -> bool

pub fn use_elim(&self) -> bool

pub fn use_vivify(&self) -> bool

pub fn use_rephase(&self) -> bool

pub fn use_reason_side_rewarding(&self) -> bool

pub fn use_stabilize(&self) -> bool

pub fn use_adaptive(&self) -> bool

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 StructOpt for Config

fn clap<'a, 'b>() -> App<'a, 'b>

Returns the corresponding clap::App.

fn from_clap(matches: &ArgMatches<'_>) -> Self

Creates the struct from clap::ArgMatches. It cannot fail with a parameter generated by clap by construction.

fn from_args() -> Self

Gets the struct from the command line arguments. Print the error message and quit the program in case of failure.

fn from_iter<I>(iter: I) -> Self where
    I: IntoIterator,
    <I as IntoIterator>::Item: Into<OsString>,
    <I as IntoIterator>::Item: Clone, 

Gets the struct from any iterator such as a Vec of your making. Print the error message and quit the program in case of failure.

fn from_iter_safe<I>(iter: I) -> Result<Self, Error> where
    I: IntoIterator,
    <I as IntoIterator>::Item: Into<OsString>,
    <I as IntoIterator>::Item: Clone, 

Gets the struct from any iterator such as a Vec of your making.

impl StructOptInternal for Config

fn augment_clap<'a, 'b>(app: App<'a, 'b>) -> App<'a, 'b>

fn is_subcommand() -> bool

fn from_subcommand(_sub: (&'b str, Option<&'b ArgMatches<'a>>)) -> Option<Self>