use {crate::types::DecisionLevel, std::path::PathBuf};
pub const CERTIFICATION_DEFAULT_FILENAME: &str = "proof.drat";
#[derive(Clone, Debug)]
pub struct Config {
pub c_cbt_thr: DecisionLevel,
pub c_cls_lim: 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_cdb_heatmap: bool,
pub show_journal: bool,
pub use_certification: bool,
pub enable_eliminator: bool,
pub elm_cls_lim: usize,
pub elm_grw_lim: usize,
pub elm_var_occ: usize,
}
impl Default for Config {
fn default() -> Self {
Config {
c_cbt_thr: 32, c_cls_lim: 0,
c_timeout: 5000.0,
splr_interface: false,
cnf_file: PathBuf::new(),
io_odir: PathBuf::from("."),
io_pfile: PathBuf::from(CERTIFICATION_DEFAULT_FILENAME),
io_rfile: PathBuf::new(),
no_color: false,
quiet_mode: false,
show_cdb_heatmap: false,
show_journal: false,
use_certification: false,
enable_eliminator: cfg!(feature = "clause_elimination"),
elm_cls_lim: 64,
elm_grw_lim: 0,
elm_var_occ: 20000,
}
}
}
impl Config {
pub fn inject_from_args(&mut self) {
let mut help = false;
let mut version = false;
if 1 < std::env::args().count()
&& let Some(ref cnf) = std::env::args().next_back()
{
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", "heatmap", "journal", "help", "version",
];
let options_usize = ["cl", "stat", "ecl", "evl", "evo"];
let options_f64 = ["timeout"];
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,
"heatmap" => self.show_cdb_heatmap = true,
"journal" => self.show_journal = true,
"help" => help = true,
"version" => version = true,
_ => panic!("invalid flag: {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,
"ecl" => self.elm_cls_lim = val,
"evl" => self.elm_grw_lim = val,
"evo" => self.elm_var_occ = 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,
_ => 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}");
}
}
_ => {
panic!("connected long arg: {:?} = {:?}", seg[0], seg[1]);
}
}
} else if let Some(name) = arg.strip_prefix('-') {
let flags = ["C", "q", "c", "j", "H", "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,
"H" => self.show_cdb_heatmap = 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 features = [
#[cfg(feature = "chrono_BT")]
"chrono BT",
#[cfg(feature = "clause_elimination")]
"Luby-based clause elimination",
#[cfg(feature = "clause_vivification")]
"Luby-based clause vivification",
#[cfg(feature = "EMA_calibration")]
"EMA calibration",
#[cfg(feature = "reason_side_rewarding")]
"reason-side rewarding",
#[cfg(feature = "rephase")]
"Luby-based re-phasing",
#[cfg(feature = "trail_saving")]
"trail saving",
#[cfg(feature = "unsafe_access")]
"unsafe access",
];
println!(
"{}\nActivated features: {}\n{}",
env!("CARGO_PKG_DESCRIPTION"),
features.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 {
macro_rules! _OPTION {
($feature: expr, $var: expr, $line: expr) => {
if cfg!(feature = $feature) {
format!($line, $var)
} else {
"".to_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
-H, --heatmap Shows clause heatmap
-j, --journal Shows log about restart stages
-V, --version Prints version information
OPTIONS:
--cl <c-cls-lim> Soft limit of #clauses (6MC/GB){:>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}
-t, --timeout <timeout> CPU time limit in sec. {:>10}
ARGS:
<cnf-file> DIMACS CNF file
",
config.c_cls_lim,
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.c_timeout,
)
}
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
}
}