conjure_oxide/
cli.rs

1use std::path::PathBuf;
2
3use clap::{Args, Parser, Subcommand};
4
5use clap_complete::Shell;
6use conjure_cp::settings::{Parser as InputParser, QuantifiedExpander, Rewriter, SolverFamily};
7
8use crate::{pretty, solve, test_solve};
9
10pub(crate) const DEBUG_HELP_HEADING: Option<&str> = Some("Debug");
11pub(crate) const LOGGING_HELP_HEADING: Option<&str> = Some("Logging & Output");
12pub(crate) const EXPERIMENTAL_HELP_HEADING: Option<&str> = Some("Experimental");
13pub(crate) const OPTIMISATIONS_HELP_HEADING: Option<&str> = Some("Optimisations");
14
15/// All subcommands of conjure-oxide
16#[derive(Clone, Debug, Subcommand)]
17pub enum Command {
18    /// Solve a model
19    Solve(solve::Args),
20    /// Print the JSON info file schema
21    PrintJsonSchema,
22    /// Tests whether the Essence model is solvable with Conjure Oxide, and whether it gets the
23    /// same solutions as Conjure.
24    ///
25    /// Return-code will be 0 if the solutions match, 1 if they don't, and >1 on crash.
26    TestSolve(test_solve::Args),
27    /// Generate a completion script for the shell provided
28    Completion(CompletionArgs),
29    Pretty(pretty::Args),
30    // Run the language server
31    ServerLSP,
32}
33
34/// Global command line arguments.
35#[derive(Clone, Debug, Parser)]
36#[command(
37    author,
38    about = "Conjure Oxide: Automated Constraints Modelling Toolkit",
39    before_help = "Full documentation can be found online at: https://conjure-cp.github.io/conjure-oxide"
40)]
41pub struct Cli {
42    #[command(subcommand)]
43    pub subcommand: Command,
44
45    #[command(flatten)]
46    pub global_args: GlobalArgs,
47
48    /// Print version
49    #[arg(long = "version", short = 'V')]
50    pub version: bool,
51}
52
53#[derive(Debug, Clone, Args)]
54pub struct GlobalArgs {
55    /// Extra rule sets to enable
56    #[arg(long, value_name = "EXTRA_RULE_SETS", global = true)]
57    pub extra_rule_sets: Vec<String>,
58
59    /// Log verbosely
60    #[arg(long, short = 'v', help = "Log verbosely to stderr", global = true, help_heading = LOGGING_HELP_HEADING)]
61    pub verbose: bool,
62
63    // --no-x flag disables --x flag : https://jwodder.github.io/kbits/posts/clap-bool-negate/
64    /// Check for multiple equally applicable rules, exiting if any are found.
65    ///
66    /// Only compatible with the default rewriter.
67    #[arg(
68        long,
69        overrides_with = "_no_check_equally_applicable_rules",
70        default_value_t = false,
71        global = true,
72        help_heading= DEBUG_HELP_HEADING
73    )]
74    pub check_equally_applicable_rules: bool,
75
76    /// Output file for the human readable rule trace.
77    #[arg(long, global = true, help_heading=LOGGING_HELP_HEADING)]
78    pub human_rule_trace: Option<PathBuf>,
79
80    /// Do not check for multiple equally applicable rules [default].
81    ///
82    /// Only compatible with the default rewriter.
83    #[arg(long, global = true, help_heading = DEBUG_HELP_HEADING)]
84    pub _no_check_equally_applicable_rules: bool,
85
86    /// Which parser to use.
87    ///
88    /// Possible values: `tree-sitter`, `via-conjure`.
89    #[arg(
90        long,
91        default_value_t = InputParser::TreeSitter,
92        value_parser = parse_parser,
93        global = true,
94        help_heading = EXPERIMENTAL_HELP_HEADING
95    )]
96    pub parser: InputParser,
97
98    /// Which rewriter to use.
99    ///
100    /// Possible values: `naive`, `morph`.
101    #[arg(long, default_value_t = Rewriter::Naive, value_parser = parse_rewriter, global = true, help_heading = EXPERIMENTAL_HELP_HEADING)]
102    pub rewriter: Rewriter,
103
104    /// Which strategy to use for expanding quantified variables in comprehensions.
105    ///
106    /// Possible values: `native`, `via-solver`, `via-solver-ac`.
107    #[arg(long, default_value_t = QuantifiedExpander::Native, value_parser = parse_quantified_expander, global = true, help_heading = OPTIMISATIONS_HELP_HEADING)]
108    pub quantified_expander: QuantifiedExpander,
109
110    /// Solver family to use.
111    ///
112    /// Possible values: `minion`, `sat`, `sat-log`, `sat-direct`, `sat-order`;
113    /// with `smt` feature: `smt` and `smt-<ints>-<matrices>[-nodiscrete]`
114    /// where `<ints>` is `lia` or `bv`, and `<matrices>` is `arrays` or `atomic`.
115    #[arg(
116        long,
117        value_name = "SOLVER",
118        value_parser = parse_solver_family,
119        default_value = "minion",
120        short = 's',
121        global = true
122    )]
123    pub solver: SolverFamily,
124
125    /// Save a solver input file to <filename>.
126    ///
127    /// This input file will be in a format compatible by the command-line
128    /// interface of the selected solver. For example, when the solver is Minion,
129    /// a valid .minion file will be output.
130    ///
131    /// This file is for informational purposes only; the results of running
132    /// this file cannot be used by Conjure Oxide in any way.
133    #[arg(long,global=true, value_names=["filename"], next_line_help=true, help_heading=LOGGING_HELP_HEADING)]
134    pub save_solver_input_file: Option<PathBuf>,
135
136    /// Exit after all comprehensions have been unrolled, printing the number of expressions at that point.
137    ///
138    /// This is only compatible with the default rewriter.
139    ///
140    /// This flag is useful to compare how comprehension optimisations, such as expand-ac, effect
141    /// rewriting.
142    #[arg(long, default_value_t = false, global = true, help_heading = DEBUG_HELP_HEADING)]
143    pub exit_after_unrolling: bool,
144
145    /// Stop the solver after the given timeout.
146    ///
147    /// Currently only SMT supports this feature.
148    #[arg(long, global = true, help_heading = OPTIMISATIONS_HELP_HEADING)]
149    pub solver_timeout: Option<humantime::Duration>,
150
151    /// Generate log files
152    #[arg(long, default_value_t = false, global = true, help_heading = LOGGING_HELP_HEADING)]
153    pub log: bool,
154
155    /// Output file for conjure-oxide's text logs
156    #[arg(long, value_name = "LOGFILE", global = true, help_heading = LOGGING_HELP_HEADING)]
157    pub logfile: Option<PathBuf>,
158
159    /// Output file for conjure-oxide's json logs
160    #[arg(long, value_name = "JSON LOGFILE", global = true, help_heading = LOGGING_HELP_HEADING)]
161    pub logfile_json: Option<PathBuf>,
162}
163
164#[derive(Debug, Clone, Args)]
165pub struct CompletionArgs {
166    /// Shell type for which to generate the completion script
167    #[arg(value_enum)]
168    pub shell: Shell,
169}
170
171#[derive(Debug, Clone, Copy, clap::ValueEnum)]
172pub enum ShellTypes {
173    Bash,
174    Zsh,
175    Fish,
176    PowerShell,
177    Elvish,
178}
179
180fn parse_quantified_expander(input: &str) -> Result<QuantifiedExpander, String> {
181    input.parse()
182}
183
184fn parse_rewriter(input: &str) -> Result<Rewriter, String> {
185    input.parse()
186}
187
188fn parse_solver_family(input: &str) -> Result<SolverFamily, String> {
189    input.parse()
190}
191
192fn parse_parser(input: &str) -> Result<InputParser, String> {
193    input.parse()
194}
conjure_oxide/cli.rs

conjure_oxide/
cli.rs
