conjure_oxide/
cli.rs

1use std::path::PathBuf;
2
3use clap::{ArgAction, Args, Parser, Subcommand, ValueEnum};
4
5use clap_complete::Shell;
6use conjure_cp::settings::{
7    Channelling, DEFAULT_HEURISTIC_SEED, Heuristic, Parser as InputParser, QuantifiedExpander,
8    Rewriter, SolverFamily,
9};
10use conjure_cp::solver::adaptors::{MinionValueOrder, MinionVariableOrder, SatBackend};
11use git_version::git_version;
12
13use crate::{pretty, solve, test_solve};
14
15pub(crate) const LOGGING_HELP_HEADING: Option<&str> = Some("Logging & Output");
16pub(crate) const CONFIGURATION_HELP_HEADING: Option<&str> = Some("Configuration");
17pub(crate) const MODELLING_HELP_HEADING: Option<&str> = Some("Modelling choices");
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    // Free `-h` for `--heuristic`; help remains available as `--help`.
45    disable_help_flag = true,
46    version = git_version!(),
47    disable_version_flag = true,
48    display_name = "conjure-oxide",
49    // clap's derive turns this on for a required subcommand; keep the concise
50    // "requires a subcommand" error instead of dumping the full help.
51    arg_required_else_help = false
52)]
53pub struct Cli {
54    #[command(subcommand)]
55    pub subcommand: Command,
56
57    #[command(flatten)]
58    pub global_args: GlobalArgs,
59
60    /// Print version
61    // `ArgAction::Version` is handled by clap while parsing, so `--version` works on its own,
62    // without the otherwise-required subcommand.
63    #[arg(long = "version", short = 'V', action = ArgAction::Version)]
64    pub version: (),
65}
66
67#[derive(Debug, Clone, Args)]
68pub struct GlobalArgs {
69    /// Print help
70    #[arg(long, action = clap::ArgAction::Help, global = true)]
71    pub help: (),
72
73    /// Extra rule sets to enable
74    #[arg(long, value_name = "EXTRA_RULE_SETS", global = true)]
75    pub extra_rule_sets: Vec<String>,
76
77    /// Increase stderr logging detail (-v: stages, -vv: rule applications, -vvv: rule attempts).
78    ///
79    /// Rule-attempt logging can be expensive and produce a very large amount of output.
80    #[arg(
81        long,
82        short = 'v',
83        action = ArgAction::Count,
84        global = true,
85        conflicts_with = "quiet",
86        help_heading = LOGGING_HELP_HEADING
87    )]
88    pub verbose: u8,
89
90    /// Disable warning and progress logs on stderr
91    #[arg(long, short = 'q', global = true, help_heading = LOGGING_HELP_HEADING)]
92    pub quiet: bool,
93
94    /// Output file for the default rule trace.
95    #[arg(long, global = true, help_heading=LOGGING_HELP_HEADING)]
96    pub rule_trace: Option<PathBuf>,
97
98    /// Output file for aggregated rule-application counts.
99    ///
100    /// Counts are kept in memory and written when the program exits, in the format:
101    /// `total_rule_applications: N`, followed by one line per rule.
102    #[arg(long, global = true, help_heading=LOGGING_HELP_HEADING)]
103    pub rule_trace_aggregates: Option<PathBuf>,
104
105    /// Continue rule trace generation during solver-time CDP rewrites.
106    ///
107    /// This is off by default, so follow-up dominance-blocking rewrites do not contribute to the
108    /// trace.
109    #[arg(long, default_value_t = false, global = true, help_heading=LOGGING_HELP_HEADING)]
110    pub rule_trace_cdp: bool,
111
112    /// Output file for the rule-attempt trace in CSV format.
113    ///
114    /// Each row includes: elapsed_s, rule_level, rule_name, rule_set, status, expression.
115    #[arg(
116        long = "rule-attempt-trace",
117        global = true,
118        help_heading=LOGGING_HELP_HEADING
119    )]
120    pub rule_attempt_trace: Option<PathBuf>,
121
122    /// Which parser to use.
123    ///
124    /// Possible values: `tree-sitter`, `via-conjure`.
125    #[arg(
126        long,
127        default_value_t = InputParser::default(),
128        value_parser = parse_parser,
129        global = true,
130        help_heading = CONFIGURATION_HELP_HEADING
131    )]
132    pub parser: InputParser,
133
134    /// Which rewriter to use.
135    ///
136    /// Possible values: `baseline`, `optimised`, `baseline+prefilter`, or `baseline+worklist`.
137    ///
138    /// Option meanings:
139    /// - `prefilter`: skip rules whose declared expression kinds cannot match; strong win vs
140    ///   baseline and part of `optimised`.
141    /// - `worklist`: drive rewriting from persistent dirty queues instead of repeated full scans;
142    ///   strong win vs baseline and part of `optimised`.
143    #[arg(long, default_value_t = Rewriter::default(), value_parser = parse_rewriter, global = true, help_heading = CONFIGURATION_HELP_HEADING)]
144    pub rewriter: Rewriter,
145
146    /// Which strategy to use for expanding quantified variables in comprehensions.
147    ///
148    /// Possible values: `auto`, `native`, `via-solver`, `via-solver-ac`. `auto` chooses
149    /// between native and solver-backed expansion from the comprehension's estimated size and
150    /// available pruning constraints.
151    #[arg(
152        long,
153        default_value_t = QuantifiedExpander::Auto,
154        value_parser = parse_comprehension_expander,
155        global = true,
156        help_heading = MODELLING_HELP_HEADING
157    )]
158    pub comprehension_expander: QuantifiedExpander,
159
160    /// Heuristic for selecting an answer when multiple modelling choices are applicable.
161    ///
162    /// Possible values: `f` (first), `r` (random), `c` (compact), `i` (interactive). Compact
163    /// estimates structural work for supported Minion representation choices, falling back to
164    /// representation-domain size elsewhere, and minimises resulting AST depth for equally-applicable
165    /// rewrite rules. Use -v to inspect representation costs. Interactive prompts on stderr, or uses
166    /// `--responses` when provided. `x` (all) is reserved for model generation and is not
167    /// supported by the CLI yet.
168    #[arg(
169        long,
170        short = 'h',
171        default_value_t = Heuristic::Compact,
172        value_parser = parse_cli_heuristic,
173        global = true,
174        help_heading = MODELLING_HELP_HEADING
175    )]
176    pub heuristic: Heuristic,
177
178    /// Comma-separated 1-based answers for the interactive heuristic (`-h i`).
179    ///
180    /// If provided, these are used as the answers during interactive model generation instead of
181    /// prompting the user.
182    #[arg(
183        long,
184        value_name = "INTS",
185        value_delimiter = ',',
186        global = true,
187        help_heading = MODELLING_HELP_HEADING
188    )]
189    pub responses: Vec<usize>,
190
191    /// Seed used by the random heuristic.
192    #[arg(
193        long,
194        default_value_t = DEFAULT_HEURISTIC_SEED,
195        global = true,
196        help_heading = MODELLING_HELP_HEADING
197    )]
198    pub seed: u64,
199
200    /// Seed used by the backend solver's random search behaviour.
201    #[arg(
202        long,
203        default_value_t = 0,
204        global = true,
205        help_heading = CONFIGURATION_HELP_HEADING
206    )]
207    pub solver_seed: u32,
208
209    /// Whether multiple representations of the same declaration may be channelled together.
210    ///
211    /// Possible values: `no`, `yes`, `uniform`. Channelling is disabled by default.
212    /// `uniform` uses one representation kind per type family throughout the model. Enable `yes` for
213    /// different representations of the same variable at different call sites, e.g.
214    /// `1 in (x :: set (representation packed) of int) /\ 2 in (x :: set (representation occurrence) of int)`.
215    #[arg(
216        long,
217        default_value_t = Channelling::No,
218        value_parser = parse_cli_channelling,
219        global = true,
220        help_heading = MODELLING_HELP_HEADING
221    )]
222    pub channelling: Channelling,
223
224    /// Pin the SAT element composition: implication or support.
225    #[arg(long = "sat-encoding-element", global = true, help_heading = MODELLING_HELP_HEADING)]
226    pub element_encoding: Option<conjure_cp::ast::sat_decision::ElementEncoding>,
227
228    /// Pin the SAT table composition: tuple, mdd or binary-support (constant two-column relations).
229    #[arg(long = "sat-encoding-table", global = true, help_heading = MODELLING_HELP_HEADING)]
230    pub table_encoding: Option<conjure_cp::ast::sat_decision::TableEncoding>,
231
232    /// Pin allDifferent: pairwise, or value-amo (requires Direct or Boolean value indicators).
233    #[arg(long = "sat-encoding-alldifferent", global = true, help_heading = MODELLING_HELP_HEADING)]
234    pub alldifferent_encoding: Option<conjure_cp::ast::sat_decision::AllDifferentEncoding>,
235
236    /// Pin the SAT AMO encoder: pairwise, ladder, bitwise, commander, bimander, two-product,
237    /// pindakaas-pairwise, pindakaas-ladder or pindakaas-bitwise.
238    /// If omitted, compact chooses per constraint; portfolio heuristics share one family choice.
239    #[arg(long = "sat-encoding-amo", global = true, help_heading = MODELLING_HELP_HEADING)]
240    pub amo_encoding: Option<conjure_cp::ast::sat_decision::AmoEncoding>,
241
242    /// Pin the SAT cardinality encoder: rustsat-totalizer or pindakaas-sorting-network.
243    #[arg(long = "sat-encoding-cardinality", global = true, help_heading = MODELLING_HELP_HEADING)]
244    pub cardinality_encoding: Option<conjure_cp::ast::sat_decision::CardinalityEncoding>,
245
246    /// Pin the SAT weighted encoder: rustsat-generalized-totalizer, rustsat-binary-adder, pindakaas-bdd, rustsat-dynamic-poly-watchdog, or pindakaas-swc.
247    #[arg(long = "sat-encoding-pb", global = true, help_heading = MODELLING_HELP_HEADING)]
248    pub pb_encoding: Option<conjure_cp::ast::sat_decision::PbEncoding>,
249
250    /// Solver to use.
251    ///
252    /// Possible values: `minion`, `sat`, `z3`.
253    ///
254    /// How a model is expressed for the chosen solver -- which SAT encoding an integer gets, or
255    /// which Z3 theory -- is a modelling choice made per declaration, not part of the solver name.
256    /// Use `--heuristic` to steer those choices and `--channelling` to allow more than one per
257    /// declaration.
258    #[arg(
259        long,
260        value_name = "SOLVER",
261        value_parser = parse_solver_family,
262        default_value = "minion",
263        short = 's',
264        global = true,
265        help_heading = CONFIGURATION_HELP_HEADING
266    )]
267    pub solver: SolverFamily,
268
269    /// SAT backend to use with --solver sat (only compiled backends are available).
270    #[arg(long, value_enum, default_value_t = SatBackend::default(), global = true,
271        help_heading = CONFIGURATION_HELP_HEADING)]
272    pub sat_backend: SatBackend,
273
274    /// Pin the int-domain span threshold for using Minion `DISCRETE` variables.
275    ///
276    /// If maximum - minimum + 1 <= this value, emit `DISCRETE`; otherwise `BOUND`.
277    /// Constraints requiring `DISCRETE` override this choice. If omitted, the heuristic chooses
278    /// between 10, zero (all `BOUND`), and unlimited (all `DISCRETE`). Compact chooses 10.
279    #[arg(
280        long,
281        global = true,
282        help_heading = MODELLING_HELP_HEADING
283    )]
284    pub minion_discrete_threshold: Option<usize>,
285
286    /// Override Minion variable ordering.
287    ///
288    /// Possible values: `static`, `sdf`, `srf`, `ldf`, `random`, `conflict`, `wdeg`,
289    /// `domoverwdeg`.
290    #[arg(
291        long,
292        value_name = "ORDER",
293        value_parser = parse_minion_variable_order,
294        global = true,
295        help_heading = CONFIGURATION_HELP_HEADING
296    )]
297    pub minion_varorder: Option<MinionVariableOrder>,
298
299    /// Override Minion value ordering.
300    ///
301    /// Possible values: `ascend`, `descend`, `random`.
302    #[arg(
303        long,
304        value_name = "ORDER",
305        value_parser = parse_minion_value_order,
306        global = true,
307        help_heading = CONFIGURATION_HELP_HEADING
308    )]
309    pub minion_valorder: Option<MinionValueOrder>,
310
311    /// Save a solver input file to <filename>.
312    ///
313    /// This input file will be in a format compatible by the command-line
314    /// interface of the selected solver. For example, when the solver is Minion,
315    /// a valid .minion file will be output.
316    ///
317    /// This file is for informational purposes only; the results of running
318    /// this file cannot be used by Conjure Oxide in any way.
319    #[arg(long,global=true, value_names=["filename"], next_line_help=true, help_heading=LOGGING_HELP_HEADING)]
320    pub save_solver_input_file: Option<PathBuf>,
321
322    /// Stop the solver after the given cumulative wall-clock timeout.
323    ///
324    /// Minion has one-second timeout resolution, so finer durations are rounded up.
325    #[arg(long, global = true, help_heading = CONFIGURATION_HELP_HEADING)]
326    pub solver_timeout: Option<humantime::Duration>,
327
328    /// Write general logs to this file
329    #[arg(long, value_name = "PATH", global = true, help_heading = LOGGING_HELP_HEADING)]
330    pub log_file: Option<PathBuf>,
331
332    /// Format used by --log-file [default: text]
333    #[arg(long, value_enum, requires = "log_file", global = true, help_heading = LOGGING_HELP_HEADING)]
334    pub log_format: Option<LogFormat>,
335
336    /// Detail written by --log-file [default: stages]
337    #[arg(long, value_enum, requires = "log_file", global = true, help_heading = LOGGING_HELP_HEADING)]
338    pub log_detail: Option<LogDetail>,
339}
340
341#[derive(Clone, Copy, Debug, Default, ValueEnum)]
342pub enum LogFormat {
343    #[default]
344    Text,
345    Json,
346}
347
348#[derive(Clone, Copy, Debug, Default, ValueEnum)]
349pub enum LogDetail {
350    #[default]
351    Stages,
352    Applications,
353    Attempts,
354}
355
356#[derive(Debug, Clone, Args)]
357pub struct CompletionArgs {
358    /// Shell type for which to generate the completion script
359    #[arg(value_enum)]
360    pub shell: Shell,
361}
362
363#[derive(Debug, Clone, Copy, clap::ValueEnum)]
364pub enum ShellTypes {
365    Bash,
366    Zsh,
367    Fish,
368    PowerShell,
369    Elvish,
370}
371
372fn parse_comprehension_expander(input: &str) -> Result<QuantifiedExpander, String> {
373    input.parse()
374}
375
376fn parse_cli_heuristic(input: &str) -> Result<Heuristic, String> {
377    match input.parse::<Heuristic>()? {
378        Heuristic::All => {
379            Err("heuristic 'x' (all) is not supported by the command line yet".to_string())
380        }
381        heuristic => Ok(heuristic),
382    }
383}
384
385fn parse_cli_channelling(input: &str) -> Result<Channelling, String> {
386    input.parse::<Channelling>()
387}
388
389fn parse_rewriter(input: &str) -> Result<Rewriter, String> {
390    input.parse::<Rewriter>()
391}
392
393fn parse_solver_family(input: &str) -> Result<SolverFamily, String> {
394    let family = input.parse()?;
395    if family == SolverFamily::Z3 && !cfg!(feature = "z3") {
396        return Err("Z3 solver support was not compiled in (enable the `z3` feature).".into());
397    }
398    Ok(family)
399}
400
401fn parse_parser(input: &str) -> Result<InputParser, String> {
402    input.parse()
403}
404
405fn parse_minion_value_order(input: &str) -> Result<MinionValueOrder, String> {
406    match input {
407        "ascend" => Ok(MinionValueOrder::Ascend),
408        "descend" => Ok(MinionValueOrder::Descend),
409        "random" => Ok(MinionValueOrder::Random),
410        other => Err(format!(
411            "unknown minion value order '{other}', expected one of: ascend, descend, random"
412        )),
413    }
414}
415
416fn parse_minion_variable_order(input: &str) -> Result<MinionVariableOrder, String> {
417    match input {
418        "static" => Ok(MinionVariableOrder::Static),
419        "sdf" => Ok(MinionVariableOrder::SmallestDomainFirst),
420        "srf" => Ok(MinionVariableOrder::SmallestRatioFirst),
421        "ldf" => Ok(MinionVariableOrder::LargestDomainFirst),
422        "random" => Ok(MinionVariableOrder::Random),
423        "conflict" => Ok(MinionVariableOrder::Conflict),
424        "wdeg" => Ok(MinionVariableOrder::WeightedDegree),
425        "domoverwdeg" => Ok(MinionVariableOrder::DomainOverWeightedDegree),
426        other => Err(format!(
427            "unknown minion variable order '{other}', expected one of: static, sdf, srf, ldf, \
428             random, conflict, wdeg, domoverwdeg"
429        )),
430    }
431}
432
433#[cfg(test)]
434mod tests {
435    use super::*;
436
437    #[test]
438    fn sat_backend_defaults_to_available_native_backend() {
439        let cli =
440            Cli::try_parse_from(["conjure-oxide", "solve", "model.essence", "--solver", "sat"])
441                .unwrap();
442        #[cfg(all(feature = "sat-cadical", not(target_family = "wasm")))]
443        assert_eq!(cli.global_args.sat_backend, SatBackend::Cadical);
444        #[cfg(not(all(feature = "sat-cadical", not(target_family = "wasm"))))]
445        assert_eq!(cli.global_args.sat_backend, SatBackend::Batsat);
446    }
447
448    #[test]
449    fn sat_backend_option_accepts_only_compiled_backends() {
450        for name in ["cadical", "batsat"] {
451            let result = Cli::try_parse_from([
452                "conjure-oxide",
453                "solve",
454                "model.essence",
455                "--solver",
456                "sat",
457                "--sat-backend",
458                name,
459            ]);
460            let available = SatBackend::value_variants()
461                .iter()
462                .find(|backend| backend.to_string() == name);
463            match available {
464                Some(backend) => assert_eq!(result.unwrap().global_args.sat_backend, *backend),
465                None => assert_eq!(
466                    result.unwrap_err().kind(),
467                    clap::error::ErrorKind::InvalidValue
468                ),
469            }
470        }
471    }
472
473    #[cfg(not(feature = "z3"))]
474    #[test]
475    fn selecting_z3_without_support_reports_the_missing_feature() {
476        let error =
477            Cli::try_parse_from(["conjure-oxide", "solve", "model.essence", "--solver", "z3"])
478                .unwrap_err();
479        assert_eq!(error.kind(), clap::error::ErrorKind::ValueValidation);
480        assert!(
481            error
482                .to_string()
483                .contains("Z3 solver support was not compiled in")
484        );
485    }
486
487    /// Regression test for #1631: `--version` used to fail as it requires a subcommand.
488    #[test]
489    fn version_flag_works_without_a_subcommand() {
490        for flag in ["--version", "-V"] {
491            let err = Cli::try_parse_from(["conjure-oxide", flag]).unwrap_err();
492            assert_eq!(err.kind(), clap::error::ErrorKind::DisplayVersion);
493            assert!(err.to_string().starts_with("conjure-oxide "));
494        }
495    }
496
497    #[test]
498    fn compact_is_the_default_cli_heuristic() {
499        let cli = Cli::try_parse_from(["conjure-oxide", "solve", "model.essence"]).unwrap();
500        assert_eq!(cli.global_args.heuristic, Heuristic::Compact);
501    }
502
503    #[test]
504    fn auto_is_the_default_comprehension_expander() {
505        let cli = Cli::try_parse_from(["conjure-oxide", "solve", "model.essence"]).unwrap();
506        assert_eq!(
507            cli.global_args.comprehension_expander,
508            QuantifiedExpander::Auto
509        );
510    }
511
512    #[test]
513    fn solver_seed_defaults_to_zero_and_can_be_overridden() {
514        let cli = Cli::try_parse_from(["conjure-oxide", "solve", "model.essence"]).unwrap();
515        assert_eq!(cli.global_args.solver_seed, 0);
516
517        let cli = Cli::try_parse_from([
518            "conjure-oxide",
519            "solve",
520            "model.essence",
521            "--solver-seed",
522            "42",
523        ])
524        .unwrap();
525        assert_eq!(cli.global_args.solver_seed, 42);
526    }
527
528    #[test]
529    fn parses_all_minion_variable_orders() {
530        let cases = [
531            ("static", MinionVariableOrder::Static),
532            ("sdf", MinionVariableOrder::SmallestDomainFirst),
533            ("srf", MinionVariableOrder::SmallestRatioFirst),
534            ("ldf", MinionVariableOrder::LargestDomainFirst),
535            ("random", MinionVariableOrder::Random),
536            ("conflict", MinionVariableOrder::Conflict),
537            ("wdeg", MinionVariableOrder::WeightedDegree),
538            ("domoverwdeg", MinionVariableOrder::DomainOverWeightedDegree),
539        ];
540
541        for (name, expected) in cases {
542            let cli = Cli::try_parse_from([
543                "conjure-oxide",
544                "solve",
545                "model.essence",
546                "--minion-varorder",
547                name,
548            ])
549            .unwrap();
550            assert_eq!(cli.global_args.minion_varorder, Some(expected));
551        }
552    }
553}
conjure_oxide/cli.rs

conjure_oxide/
cli.rs
