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 human readable rule trace.
80    #[arg(long, global = true, help_heading=LOGGING_HELP_HEADING)]
81    pub rule_trace: Option<PathBuf>,
82
83    /// Output file for verbose rule-attempt trace in CSV format.
84    ///
85    /// Each row includes: elapsed_s, rule_level, rule_name, rule_set, status, expression.
86    #[arg(long, global = true, help_heading=LOGGING_HELP_HEADING)]
87    pub rule_trace_verbose: Option<PathBuf>,
88
89    /// Do not check for multiple equally applicable rules [default].
90    ///
91    /// Only compatible with the default rewriter.
92    #[arg(long, global = true, help_heading = DEBUG_HELP_HEADING)]
93    pub _no_check_equally_applicable_rules: bool,
94
95    /// Which parser to use.
96    ///
97    /// Possible values: `tree-sitter`, `via-conjure`.
98    #[arg(
99        long,
100        default_value_t = InputParser::ViaConjure,
101        value_parser = parse_parser,
102        global = true,
103        help_heading = CONFIGURATION_HELP_HEADING
104    )]
105    pub parser: InputParser,
106
107    /// Which rewriter to use.
108    ///
109    /// Possible values: `naive`, `morph`.
110    #[arg(long, default_value_t = Rewriter::Naive, value_parser = parse_rewriter, global = true, help_heading = CONFIGURATION_HELP_HEADING)]
111    pub rewriter: Rewriter,
112
113    /// Which strategy to use for expanding quantified variables in comprehensions.
114    ///
115    /// Possible values: `native`, `via-solver`, `via-solver-ac`.
116    #[arg(
117        long,
118        default_value_t = QuantifiedExpander::Native,
119        value_parser = parse_comprehension_expander,
120        global = true,
121        help_heading = CONFIGURATION_HELP_HEADING
122    )]
123    pub comprehension_expander: QuantifiedExpander,
124
125    /// Solver family to use.
126    ///
127    /// Possible values: `minion`, `sat`, `sat-log`, `sat-direct`, `sat-order`,
128    /// `smt[-<ints>][-<matrices>][-nodiscrete]`
129    /// where `<ints>` is `lia` or `bv`, and `<matrices>` is `arrays` or `atomic`.
130    #[arg(
131        long,
132        value_name = "SOLVER",
133        value_parser = parse_solver_family,
134        default_value = "minion",
135        short = 's',
136        global = true,
137        help_heading = CONFIGURATION_HELP_HEADING
138    )]
139    pub solver: SolverFamily,
140
141    /// Int-domain size threshold for using Minion `DISCRETE` variables.
142    ///
143    /// If an int domain has size <= this value, Conjure Oxide emits `DISCRETE`; otherwise `BOUND`.
144    #[arg(
145        long,
146        default_value_t = DEFAULT_MINION_DISCRETE_THRESHOLD,
147        global = true,
148        help_heading = CONFIGURATION_HELP_HEADING
149    )]
150    pub minion_discrete_threshold: usize,
151
152    /// Save a solver input file to <filename>.
153    ///
154    /// This input file will be in a format compatible by the command-line
155    /// interface of the selected solver. For example, when the solver is Minion,
156    /// a valid .minion file will be output.
157    ///
158    /// This file is for informational purposes only; the results of running
159    /// this file cannot be used by Conjure Oxide in any way.
160    #[arg(long,global=true, value_names=["filename"], next_line_help=true, help_heading=LOGGING_HELP_HEADING)]
161    pub save_solver_input_file: Option<PathBuf>,
162
163    /// Stop the solver after the given timeout.
164    ///
165    /// Currently only SMT supports this feature.
166    #[arg(long, global = true, help_heading = OPTIMISATIONS_HELP_HEADING)]
167    pub solver_timeout: Option<humantime::Duration>,
168
169    /// Generate log files
170    #[arg(long, default_value_t = false, global = true, help_heading = LOGGING_HELP_HEADING)]
171    pub log: bool,
172
173    /// Output file for conjure-oxide's text logs
174    #[arg(long, value_name = "LOGFILE", global = true, help_heading = LOGGING_HELP_HEADING)]
175    pub logfile: Option<PathBuf>,
176
177    /// Output file for conjure-oxide's json logs
178    #[arg(long, value_name = "JSON LOGFILE", global = true, help_heading = LOGGING_HELP_HEADING)]
179    pub logfile_json: Option<PathBuf>,
180}
181
182#[derive(Debug, Clone, Args)]
183pub struct CompletionArgs {
184    /// Shell type for which to generate the completion script
185    #[arg(value_enum)]
186    pub shell: Shell,
187}
188
189#[derive(Debug, Clone, Copy, clap::ValueEnum)]
190pub enum ShellTypes {
191    Bash,
192    Zsh,
193    Fish,
194    PowerShell,
195    Elvish,
196}
197
198fn parse_comprehension_expander(input: &str) -> Result<QuantifiedExpander, String> {
199    input.parse()
200}
201
202fn parse_rewriter(input: &str) -> Result<Rewriter, String> {
203    input.parse()
204}
205
206fn parse_solver_family(input: &str) -> Result<SolverFamily, String> {
207    input.parse()
208}
209
210fn parse_parser(input: &str) -> Result<InputParser, String> {
211    input.parse()
212}
conjure_oxide/cli.rs

conjure_oxide/
cli.rs
