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 StructRecur,
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 = "interleave", value_name = "HEURISTIC")]
29 pub heuristic: Heuristic,
30
31 #[arg(short, long, default_value_t = 10, value_name = "INT")]
32 pub verbosity: u8,
33
34 #[arg(long, default_value_t = true)]
35 pub dump_file: bool,
36
37 #[arg(long, default_value_t = true)]
38 pub debug_mode: bool,
39
40 #[arg(long, default_value_t = false)]
41 pub show_output: bool,
42
43 #[arg(long, default_value_t = true)]
44 pub show_stat: bool,
45
46 #[arg(long, default_value_t = false)]
47 pub show_prog: bool,
48
49 #[arg(long, default_value_t = false)]
50 pub warn_as_err: bool,
51}
52
53pub fn parse_cli_args() -> CliArgs {
54 CliArgs::parse()
55}
56
57pub fn get_test_cli_args(prog_name: PathBuf) -> CliArgs {
58 CliArgs {
59 input: prog_name,
60 solver: Solver::Z3,
61 heuristic: Heuristic::LookAhead,
62 verbosity: 10,
63 dump_file: false,
64 debug_mode: false,
65 show_output: false,
66 show_stat: false,
67 show_prog: false,
68 warn_as_err: true,
69 }
70}