Skip to main content

prune_lang/cli/
args.rs

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}