1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
use std::path::PathBuf;
use structopt::StructOpt;
pub const VERSION: &str = "0.1.4";
pub const ACTIVITY_MAX: f64 = 1e308;
#[derive(Clone, Debug, StructOpt)]
#[structopt(name = "splr", about, author)]
pub struct Config {
#[structopt(long = "cl", default_value = "0")]
pub clause_limit: usize,
#[structopt(long = "eg", default_value = "4")]
pub elim_grow_limit: usize,
#[structopt(long = "el", default_value = "64")]
pub elim_lit_limit: usize,
#[structopt(long = "ra", default_value = "3500")]
pub restart_asg_len: usize,
#[structopt(long = "rl", default_value = "50")]
pub restart_lbd_len: usize,
#[structopt(long = "rt", default_value = "0.70")]
pub restart_threshold: f64,
#[structopt(long = "rb", default_value = "1.40")]
pub restart_blocking: f64,
#[structopt(long = "rs", default_value = "50")]
pub restart_step: usize,
#[structopt(parse(from_os_str))]
pub cnf_filename: PathBuf,
#[structopt(long = "dir", short = "o", default_value = ".", parse(from_os_str))]
pub output_dirname: PathBuf,
#[structopt(long = "result", short = "r", default_value = "", parse(from_os_str))]
pub result_filename: PathBuf,
#[structopt(
long = "proof",
default_value = "proof.out",
short = "p",
parse(from_os_str)
)]
pub proof_filename: PathBuf,
#[structopt(long = "log", short = "l")]
pub use_log: bool,
#[structopt(long = "without-elim", short = "E")]
pub without_elim: bool,
#[structopt(long = "without-adaptive-restart", short = "R")]
pub without_adaptive_restart: bool,
#[structopt(long = "without-adaptive-strategy", short = "S")]
pub without_adaptive_strategy: bool,
#[structopt(long = "without-deep-search", short = "D")]
pub without_deep_search: bool,
#[structopt(long = "certify", short = "c")]
pub use_certification: bool,
#[structopt(long = "to", default_value = "0")]
pub timeout: f64,
#[structopt(long = "stat", default_value = "0")]
pub dump_interval: usize,
}
impl Default for Config {
fn default() -> Config {
Config {
clause_limit: 18_000_000,
elim_grow_limit: 4,
elim_lit_limit: 100,
restart_asg_len: 3500,
restart_lbd_len: 50,
restart_threshold: 0.60,
restart_blocking: 1.40,
restart_step: 50,
cnf_filename: PathBuf::new(),
output_dirname: PathBuf::from("."),
result_filename: PathBuf::new(),
proof_filename: PathBuf::from("proof.out"),
use_log: false,
without_elim: false,
without_adaptive_restart: false,
without_adaptive_strategy: false,
without_deep_search: true,
use_certification: false,
timeout: 0.0,
dump_interval: 0,
}
}
}
impl<T> From<T> for Config
where
PathBuf: From<T>,
{
fn from(path: T) -> Config {
let mut config = Config::default();
config.cnf_filename = PathBuf::from(path);
config
}
}