conjure_oxide/
cli.rs

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

conjure_oxide/
cli.rs
