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

conjure_oxide/
cli.rs
