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 = "look-ahead", 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 = false, action = clap::ArgAction::SetTrue)]
35 pub dump_file: bool,
36
37 #[arg(long, default_value_t = false, action = clap::ArgAction::SetTrue)]
38 pub debug_mode: bool,
39
40 #[arg(long, default_value_t = true, action = clap::ArgAction::Set)]
41 pub show_output: bool,
42
43 #[arg(long, default_value_t = false, action = clap::ArgAction::Set)]
44 pub show_stat: bool,
45
46 #[arg(long, default_value_t = false, action = clap::ArgAction::Set)]
47 pub show_prog: bool,
48
49 #[arg(long, default_value_t = true, action = clap::ArgAction::Set)]
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: true,
66 show_stat: true,
67 show_prog: false,
68 warn_as_err: true,
69 }
70}