[−][src]Struct splr::config::Config
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_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 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
rst_stb_scl: f64
Stabilizer scaling
viv_thr: usize
#reduction for next vivification
stg_rwd_dcy: f64
Decay rate for Extra reward for vars on stage
stg_rwd_val: f64
Initial value for the extra reward for vars on stage
vrw_dcy_rat: f64
vrw_occ_cmp: f64
Occurrence compression rate in LR rewarding
Implementations
impl Config
[src]
pub fn inject_from_args(&mut self)
[src]
impl Config
[src]
pub fn override_args(mut self: Self) -> Config
[src]
pub fn use_elim(&self) -> bool
[src]
pub fn use_luby(&self) -> bool
[src]
pub fn use_reduce(&self) -> bool
[src]
pub fn use_rephase(&self) -> bool
[src]
pub fn use_vivify(&self) -> bool
[src]
pub fn use_reason_side_rewarding(&self) -> bool
[src]
pub fn use_stabilize(&self) -> bool
[src]
pub fn use_stage(&self) -> bool
[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]
PathBuf: From<T>,
Auto Trait Implementations
impl RefUnwindSafe for Config
[src]
impl Send for Config
[src]
impl Sync for Config
[src]
impl Unpin for Config
[src]
impl UnwindSafe for Config
[src]
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
pub fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
pub fn to_owned(&self) -> T
[src]
pub fn clone_into(&self, target: &mut T)
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
pub fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,