use {crate::types::DecisionLevel, std::path::PathBuf};
#[derive(Clone, Debug)]
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,
}
impl Default for Config {
fn default() -> Self {
Config {
c_cbt_thr: 100,
c_cls_lim: 0,
c_ip_int: 16384,
c_timeout: 5000.0,
splr_interface: false,
cnf_file: PathBuf::new(),
io_odir: PathBuf::from("."),
io_pfile: PathBuf::from("proof.out"),
io_rfile: PathBuf::new(),
no_color: false,
quiet_mode: false,
show_journal: false,
use_certification: false,
use_log: false,
crw_dcy_rat: 0.95,
elm_cls_lim: 18,
elm_grw_lim: 0,
elm_var_occ: 20000,
rst_step: 24,
rst_asg_len: 24,
rst_asg_slw: 8192,
rst_asg_thr: 0.75,
rst_lbd_len: 24,
rst_lbd_slw: 8192,
rst_lbd_thr: 1.10,
stg_rwd_dcy: 0.5,
stg_rwd_val: 1.0,
#[cfg(feature = "EVSIDS")]
vrw_dcy_rat: 0.98,
#[cfg(feature = "LR_rewarding")]
vrw_dcy_rat: 0.94,
#[cfg(feature = "EVSIDS")]
vrw_dcy_stp: 0.0001,
#[cfg(feature = "LR_rewarding")]
vrw_dcy_stp: 0.1,
}
}
}
impl Config {
pub fn inject_from_args(&mut self) {
let mut help = false;
let mut version = false;
if 1 < std::env::args().count() {
if let Some(ref cnf) = std::env::args().last() {
self.cnf_file = PathBuf::from(cnf.clone());
}
}
let args = std::env::args();
let mut iter = args.skip(1);
while let Some(arg) = iter.next() {
if let Some(stripped) = arg.strip_prefix("--") {
let flags = [
"no-color", "quiet", "certify", "journal", "log", "help", "version",
];
let options_u32 = ["cbt"];
let options_usize = [
"cl", "ii", "stat", "ecl", "evl", "evo", "rs", "ral", "ras", "rll", "rls",
];
let options_f64 = ["timeout", "cdr", "rat", "rlt", "srd", "srv", "vdr", "vds"];
let options_path = ["dir", "proof", "result"];
let seg: Vec<&str> = stripped.split('=').collect();
match seg.len() {
1 => {
let name = &arg[2..];
if flags.contains(&name) {
match name {
"no-color" => self.no_color = true,
"quiet" => self.quiet_mode = true,
"certify" => self.use_certification = true,
"journal" => self.show_journal = true,
"log" => self.use_log = true,
"help" => help = true,
"version" => version = true,
_ => panic!("invalid flag: {}", name),
}
} else if options_u32.contains(&name) {
if let Some(str) = iter.next() {
if let Ok(val) = str.parse::<u32>() {
match name {
"cbt" => self.c_cbt_thr = val,
_ => panic!("invalid option: {}", name),
}
} else {
panic!("invalid value {}", name);
}
} else {
panic!("no argument for {}", name);
}
} else if options_usize.contains(&name) {
if let Some(str) = iter.next() {
if let Ok(val) = str.parse::<usize>() {
match name {
"cl" => self.c_cls_lim = val,
"ii" => self.c_ip_int = val,
"ecl" => self.elm_cls_lim = val,
"evl" => self.elm_grw_lim = val,
"evo" => self.elm_var_occ = val,
"rs" => self.rst_step = val,
"ral" => self.rst_asg_len = val,
"ras" => self.rst_asg_slw = val,
"rll" => self.rst_lbd_len = val,
"rls" => self.rst_lbd_slw = val,
_ => panic!("invalid option: {}", name),
}
} else {
panic!("invalid value {}", name);
}
} else {
panic!("no argument for {}", name);
}
} else if options_f64.contains(&name) {
if let Some(str) = iter.next() {
if let Ok(val) = str.parse::<f64>() {
match name {
"timeout" => self.c_timeout = val,
"cdr" => self.crw_dcy_rat = val,
"rat" => self.rst_asg_thr = val,
"rlt" => self.rst_lbd_thr = val,
"srd" => self.stg_rwd_dcy = val,
"srv" => self.stg_rwd_val = val,
"vdr" => self.vrw_dcy_rat = val,
"vds" => self.vrw_dcy_stp = val,
_ => panic!("invalid option: {}", name),
}
} else {
panic!("invalid value {}", name);
}
} else {
panic!("no argument for {}", name);
}
} else if options_path.contains(&name) {
if let Some(val) = iter.next() {
match name {
"dir" => self.io_odir = PathBuf::from(val),
"proof" => self.io_pfile = PathBuf::from(val),
"result" => self.io_rfile = PathBuf::from(val),
_ => panic!("invalid option: {}", name),
}
} else {
panic!("invalid value {}", name);
}
} else {
panic!("unknown option name {}", name);
}
}
_ => {
println!("connected long arg: {:?} = {:?}", seg[0], seg[1]);
}
}
} else if let Some(name) = arg.strip_prefix('-') {
let flags = ["C", "q", "c", "j", "l", "h", "V"];
let options_path = ["o", "p", "r", "t"];
if flags.contains(&name) {
match name {
"C" => self.no_color = true,
"q" => self.quiet_mode = true,
"c" => self.use_certification = true,
"j" => self.show_journal = true,
"l" => self.use_log = true,
"h" => help = true,
"V" => version = true,
_ => panic!("invalid flag: {}", name),
}
} else if options_path.contains(&name) {
if let Some(val) = iter.next() {
match name {
"o" => self.io_odir = PathBuf::from(val),
"p" => self.io_pfile = PathBuf::from(val),
"r" => self.io_rfile = PathBuf::from(val),
"t" => {
self.c_timeout = val.parse::<f64>().expect("-t requires a number")
}
_ => panic!("invalid option: {}", name),
}
} else {
panic!("no argument for {}", name);
}
} else {
panic!("unknown option name {}", name);
}
} else if self.cnf_file.to_string_lossy() != arg {
panic!("invalid argument: {}", arg);
}
}
if help {
let featuers = [
#[cfg(feature = "best_phases_tracking")]
"best phase tracking",
#[cfg(feature = "clause_elimination")]
"clause elimination",
#[cfg(feature = "clause_reduction")]
"clause reduction",
#[cfg(feature = "clause_vivification")]
"clause vivification",
#[cfg(feature = "ema_calibration")]
"EMA calibration",
#[cfg(feature = "EVSIDS")]
"EVSIDS rewarding",
#[cfg(feature = "incremental_solver")]
"incremental solver",
#[cfg(feature = "just_used")]
"use_just_used_flag",
#[cfg(feature = "LR_rewarding")]
"Learning-Rate based rewarding",
#[cfg(feature = "Luby_restart")]
"Luby restart",
#[cfg(feature = "Luby_stabilization")]
"Luby stabilization",
#[cfg(feature = "reason_side_rewarding")]
"reason side rewarding",
#[cfg(feature = "strategy_adaptation")]
"strategy adaptation",
#[cfg(feature = "best_phases_reuse")]
"re-phasing",
#[cfg(feature = "var_staging")]
"stage-based var selection",
];
println!(
"{}\nActivated features: {}\n{}",
env!("CARGO_PKG_DESCRIPTION"),
featuers.join(", "),
help_string()
);
std::process::exit(0);
}
if version {
println!("{}", env!("CARGO_PKG_VERSION"));
std::process::exit(0);
}
if self.cnf_file.to_string_lossy().is_empty() {
println!("No target file specified. Run with '--help' to show help message.");
std::process::exit(0);
}
if !self.cnf_file.exists() {
println!("{} doesn't exist.", self.cnf_file.to_string_lossy());
std::process::exit(0);
}
}
}
fn help_string() -> String {
let config = Config::default();
format!(
"
USAGE:
splr [FLAGS] [OPTIONS] <cnf-file>
FLAGS:
-h, --help Prints help information
-C, --no-color Disable coloring
-q, --quiet Disable any progress message
-c, --certify Writes a DRAT UNSAT certification file
-j, --journal Shows sub-module logs
-l, --log Uses Glucose-like progress report
-V, --version Prints version information
OPTIONS (\x1B[000m\x1B[031mred options depend on features in Cargo.toml\x1B[000m):
--cbt <c-cbt-thr> Dec. lvl to use chronoBT {:>10}
--cdr <crw-dcy-rat> Clause reward decay rate {:>10.2}
--cl <c-cls-lim> Soft limit of #clauses (6MC/GB){:>10}
--ii <c-ip-int> #cls to start in-processor {:>10}
-t, --timeout <timeout> CPU time limit in sec. {:>10}
--ecl <elm-cls-lim> Max #lit for clause subsume {:>10}
--evl <elm-grw-lim> Grow limit of #cls in var elim.{:>10}
--evo <elm-var-occ> Max #cls for var elimination {:>10}
-o, --dir <io-outdir> Output directory {:>10}
-p, --proof <io-pfile> DRAT Cert. filename {:>10}
-r, --result <io-rfile> Result filename/stdout {:>10}
--ral <rst-asg-len> Length of assign. fast EMA {:>10}
--ras <rst-asg-slw> Length of assign. slow EMA {:>10}
--rat <rst-asg-thr> Blocking restart threshold {:>10.2}
--rll <rst-lbd-len> Length of LBD fast EMA {:>10}
--rls <rst-lbd-slw> Length of LBD slow EMA {:>10}
--rlt <rst-lbd-thr> Forcing restart threshold {:>10.2}
--rs <rst-step> #conflicts between restarts {:>10}
--srd <stg-rwd-dcy> Decay rate for staged var reward {:>10.2}
--srv <stg-rwd-val> Extra reward for staged vars {:>10.2}
--vdr <vrw-dcy-rat> Var reward decay rate {:>10.2}
--vds <vrw-dcy-stp> Var reward decay change step {:>10.2}
ARGS:
<cnf-file> DIMACS CNF file
",
config.c_cbt_thr,
config.crw_dcy_rat,
config.c_cls_lim,
config.c_ip_int,
config.c_timeout,
config.elm_cls_lim,
config.elm_grw_lim,
config.elm_var_occ,
config.io_odir.to_string_lossy(),
config.io_pfile.to_string_lossy(),
config.io_rfile.to_string_lossy(),
config.rst_asg_len,
config.rst_asg_slw,
config.rst_asg_thr,
config.rst_lbd_len,
config.rst_lbd_slw,
config.rst_lbd_thr,
config.rst_step,
config.stg_rwd_dcy,
config.stg_rwd_val,
config.vrw_dcy_rat,
config.vrw_dcy_stp,
)
}
impl<T> From<T> for Config
where
PathBuf: From<T>,
{
fn from(path: T) -> Config {
Config {
cnf_file: PathBuf::from(path),
..Config::default()
}
}
}
#[allow(unused_macros)]
macro_rules! dispatch {
($field: expr) => {
0 != $field
};
($field: expr, $default: expr) => {
match $field {
0 => $default,
x => 0 < x,
}
};
}
impl Config {
#[allow(unused_mut)]
pub fn override_args(mut self) -> Config {
self
}
}