1use super::*;
2use clap::{Parser, ValueEnum};
3
4#[derive(ValueEnum, Copy, Clone, Debug, PartialEq, Eq)]
5pub enum Solver {
6 Z3,
7 CVC5,
8 NoSmt,
9}
10
11#[derive(ValueEnum, Copy, Clone, Debug, PartialEq, Eq)]
12pub enum Heuristic {
13 LeftBiased,
14 Interleave,
15 SmallFirst,
16 LookAhead,
17 Random,
18}
19
20#[derive(Parser, Debug, Clone)]
21#[command(version, about, long_about = None)]
22pub struct CliArgs {
23 pub input: PathBuf,
24
25 #[arg(long, default_value = "no-smt", value_name = "SOLVER")]
26 pub solver: Solver,
27
28 #[arg(long, default_value = "small-first", value_name = "HEURISTIC")]
29 pub heuristic: Heuristic,
30
31 #[arg(long, default_value_t = 10, value_name = "INT")]
32 pub depth_step: usize,
33
34 #[arg(long, default_value_t = usize::MAX, value_name = "INT")]
35 pub depth_limit: usize,
36
37 #[arg(long, default_value_t = usize::MAX, value_name = "INT")]
38 pub answer_limit: usize,
39
40 #[arg(long, default_value_t = false, action = clap::ArgAction::SetTrue)]
41 pub answer_pause: bool,
42
43 #[arg(short, long, default_value_t = 10, value_name = "INT")]
44 pub verbosity: u8,
45
46 #[arg(long, default_value_t = false, action = clap::ArgAction::SetTrue)]
47 pub dump_file: bool,
48
49 #[arg(long, default_value_t = false, action = clap::ArgAction::SetTrue)]
50 pub debug_mode: bool,
51
52 #[arg(long, default_value_t = true, action = clap::ArgAction::Set)]
53 pub show_output: bool,
54
55 #[arg(long, default_value_t = false, action = clap::ArgAction::Set)]
56 pub show_stat: bool,
57
58 #[arg(long, default_value_t = false, action = clap::ArgAction::Set)]
59 pub show_prog: bool,
60
61 #[arg(long, default_value_t = true, action = clap::ArgAction::Set)]
62 pub warn_as_err: bool,
63}
64
65pub fn parse_cli_args() -> CliArgs {
66 CliArgs::parse()
67}
68
69pub fn get_test_cli_args(prog_name: PathBuf) -> CliArgs {
70 CliArgs {
71 input: prog_name,
72 solver: Solver::Z3,
73 heuristic: Heuristic::SmallFirst,
74 depth_step: 10,
75 depth_limit: usize::MAX,
76 answer_limit: usize::MAX,
77 answer_pause: false,
78 verbosity: 10,
79 dump_file: false,
80 debug_mode: false,
81 show_output: true,
82 show_stat: true,
83 show_prog: false,
84 warn_as_err: true,
85 }
86}
87
88pub fn get_bench_cli_args(prog_name: PathBuf, heuristic: Heuristic, depth_limit: usize) -> CliArgs {
89 CliArgs {
90 input: prog_name,
91 solver: Solver::Z3,
92 heuristic,
93 depth_step: 10,
94 depth_limit,
95 answer_limit: usize::MAX,
96 answer_pause: false,
97 verbosity: 10,
98 dump_file: false,
99 debug_mode: false,
100 show_output: false,
101 show_stat: false,
102 show_prog: false,
103 warn_as_err: true,
104 }
105}