Struct splr::config::Config

pub struct Config {
    pub clause_limit: usize,
    pub elim_grow_limit: usize,
    pub elim_lit_limit: usize,
    pub restart_asg_len: usize,
    pub restart_lbd_len: usize,
    pub restart_threshold: f64,
    pub restart_blocking: f64,
    pub restart_step: usize,
    pub cnf_filename: PathBuf,
    pub output_dirname: PathBuf,
    pub result_filename: PathBuf,
    pub proof_filename: PathBuf,
    pub use_log: bool,
    pub without_elim: bool,
    pub without_adaptive_restart: bool,
    pub without_adaptive_strategy: bool,
    pub without_deep_search: bool,
    pub use_certification: bool,
    pub timeout: f64,
    pub dump_interval: usize,
}

Configuration built from command line options

Fields

clause_limit: usize

soft limit of #clauses (24MC~4GB)

elim_grow_limit: usize

grow limit of #clauses by v-elim

elim_lit_limit: usize

#literals in a clause by v-elim

restart_asg_len: usize

length for assignment average

restart_lbd_len: usize

length for LBD average

restart_threshold: f64

forcing restart threshold

restart_blocking: f64

blocking restart threshold

restart_step: usize

#conflicts between restarts

cnf_filename: PathBuf

a DIMACS format CNF file

output_dirname: PathBuf

output directory

result_filename: PathBuf

result filename/stdout

proof_filename: PathBuf

filename for DRAT cert.

use_log: bool

Uses Glucose-like progress report

without_elim: bool

Disables exhaustive simplification

without_adaptive_restart: bool

Disables dynamic restart adaptation

without_adaptive_strategy: bool

Disables dynamic strategy adaptation

without_deep_search: bool

Disables deep search mode

use_certification: bool

Writes a DRAT UNSAT certification file

timeout: f64

CPU time limit in sec.

dump_interval: usize

interval for dumpping stat data

Trait Implementations

impl Default for Config

fn default() -> Config

Returns the "default value" for a type.

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<T> From<T> for Config where
    PathBuf: From<T>, 

fn from(path: T) -> Config

Performs the conversion.

impl Debug for Config

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

Formats the value using the given formatter.

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.