conjure_oxide/
solve.rs

1//! conjure_oxide solve sub-command
2#![allow(clippy::unwrap_used)]
3use std::time::Duration;
4use std::{
5    fs::File,
6    path::{Path, PathBuf},
7    process::exit,
8    sync::{Arc, RwLock},
9};
10
11use anyhow::anyhow;
12use clap::ValueHint;
13use conjure_cp::instantiate::{instantiate_model, validate_instantiation_conditions};
14use conjure_cp::{
15    Model,
16    context::Context,
17    defaults::DEFAULT_RULE_SETS,
18    rule_engine::{resolve_rule_sets, rewrite_model},
19    settings::{
20        Rewriter, set_channelling, set_comprehension_expander, set_current_parser,
21        set_current_rewriter, set_current_solver_family, set_default_rule_trace_enabled,
22        set_heuristic, set_heuristic_responses, set_heuristic_seed, set_minion_discrete_threshold,
23        set_rule_attempt_trace_enabled, set_rule_trace_aggregates_enabled, set_rule_trace_enabled,
24    },
25    solver::Solver,
26};
27use conjure_cp::{
28    parse::conjure_json::model_from_json, rule_engine::get_rules, settings::SolverFamily,
29};
30use conjure_cp::{parse::tree_sitter::parse_essence_file_native, solver::adaptors::*};
31use conjure_cp_cli::find_conjure::conjure_executable;
32use conjure_cp_cli::utils::conjure::{get_solutions, solutions_to_essence, solutions_to_json};
33use conjure_cp_cli::utils::simplified_json::{
34    domains_from_model, param_model_from_assignments, params_from_simplified_json_str,
35    solution_to_simplified_json, solutions_to_simplified_json_string,
36};
37
38use crate::cli::{GlobalArgs, LOGGING_HELP_HEADING};
39
40#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, clap::ValueEnum)]
41pub enum OutputFormat {
42    /// Conjure-compatible Essence multi-solution / per-solution files
43    #[default]
44    Essence,
45    /// Conjure `--output-format=json` simplified JSON
46    Json,
47}
48
49#[derive(Clone, Copy, Debug, PartialEq, Eq)]
50pub enum NumberOfSolutions {
51    All,
52    Limit(i32),
53}
54
55impl NumberOfSolutions {
56    fn as_solver_limit(self) -> i32 {
57        match self {
58            NumberOfSolutions::All => 0,
59            NumberOfSolutions::Limit(limit) => limit,
60        }
61    }
62}
63
64fn parse_number_of_solutions(input: &str) -> Result<NumberOfSolutions, String> {
65    if input.eq_ignore_ascii_case("all") {
66        return Ok(NumberOfSolutions::All);
67    }
68
69    let limit = input
70        .parse::<i32>()
71        .map_err(|_| "expected a positive integer or 'all'".to_string())?;
72
73    if limit <= 0 {
74        return Err("expected a positive integer or 'all'".to_string());
75    }
76
77    Ok(NumberOfSolutions::Limit(limit))
78}
79
80#[derive(Clone, Debug, clap::Args)]
81pub struct Args {
82    /// The input Essence problem file
83    #[arg(value_name = "INPUT_ESSENCE", value_hint = ValueHint::FilePath)]
84    pub essence_file: PathBuf,
85
86    /// The input Essence parameter file
87    #[arg(value_name = "PARAM_ESSENCE", value_hint = ValueHint::FilePath)]
88    pub param_file: Option<PathBuf>,
89
90    /// Save execution info as JSON to the given filepath.
91    #[arg(long ,value_hint=ValueHint::FilePath,help_heading=LOGGING_HELP_HEADING)]
92    pub info_json_path: Option<PathBuf>,
93
94    /// Do not run the solver.
95    ///
96    /// The rewritten model is printed to stdout in an Essence-style syntax
97    /// (but is not necessarily valid Essence).
98    #[arg(long, default_value_t = false)]
99    pub no_run_solver: bool,
100
101    /// Number of solutions to return. Use a positive integer, or `all`.
102    #[arg(
103        long,
104        short = 'n',
105        default_value = "1",
106        value_name = "N|all",
107        value_parser = parse_number_of_solutions
108    )]
109    pub number_of_solutions: NumberOfSolutions,
110
111    /// Format for printed / saved solutions
112    #[arg(long, value_enum, default_value_t = OutputFormat::Essence, help_heading=LOGGING_HELP_HEADING)]
113    pub output_format: OutputFormat,
114
115    /// Write all solutions into a single file (default: true).
116    ///
117    /// Pass `--solutions-in-one-file=false` to emit one file (or stdout record) per solution.
118    #[arg(
119        long,
120        default_value_t = true,
121        action = clap::ArgAction::Set,
122        value_name = "BOOL",
123        help_heading = LOGGING_HELP_HEADING
124    )]
125    pub solutions_in_one_file: bool,
126
127    /// Save solutions to the given path (Essence `.solutions` / JSON `.solutions.json`, or a
128    /// filename stem when `--solutions-in-one-file=false`)
129    #[arg(long, short = 'o', value_hint = ValueHint::FilePath,help_heading=LOGGING_HELP_HEADING)]
130    pub output: Option<PathBuf>,
131
132    /// When optimising, retain every improving solution Minion reports instead of only the last
133    /// one.
134    #[arg(long, default_value_t = false)]
135    pub keep_intermediate_solutions: bool,
136}
137
138pub fn run_solve_command(global_args: GlobalArgs, solve_args: Args) -> anyhow::Result<()> {
139    let essence_file = solve_args.essence_file.clone();
140    let param_file = solve_args.param_file.clone();
141
142    // each step is in its own method so that similar commands
143    // (e.g. testsolve) can reuse some of these steps.
144
145    let context = init_context(&global_args, essence_file, param_file)?;
146
147    let ctx_lock = context.read().unwrap();
148    let essence_file_name = ctx_lock
149        .essence_file_name
150        .as_ref()
151        .expect("context should contain the problem input file");
152    let param_file_name = ctx_lock.param_file_name.as_ref();
153
154    // parse models
155    let problem_model = parse(&global_args, Arc::clone(&context), essence_file_name)?;
156
157    // unify models
158    let unified_model = match param_file_name {
159        Some(param_file_name) => {
160            let param_model = parse_param(
161                &global_args,
162                Arc::clone(&context),
163                param_file_name,
164                &problem_model,
165            )?;
166            instantiate_model(problem_model, param_model)?
167        }
168        None => {
169            let mut problem_model = problem_model;
170            validate_instantiation_conditions(&mut problem_model)?;
171            problem_model
172        }
173    };
174    drop(ctx_lock);
175
176    let rewritten_model = rewrite(unified_model, &global_args, Arc::clone(&context))?;
177
178    let solver = init_solver(&global_args);
179
180    if solve_args.no_run_solver {
181        println!("{}", rewritten_model);
182
183        if let Some(path) = global_args.save_solver_input_file {
184            let solver = solver.load_model(rewritten_model)?;
185            tracing::info!(
186                target: "conjure::stage",
187                path = %path.display(),
188                "writing solver input file"
189            );
190            let mut file: Box<dyn std::io::Write> = Box::new(File::create(path)?);
191            solver.write_solver_input_file(&mut file)?;
192        }
193    } else {
194        run_solver(solver, &global_args, &solve_args, rewritten_model)?
195    }
196
197    // still do postamble even if we didn't run the solver
198    if let Some(ref path) = solve_args.info_json_path {
199        let context_obj = context.read().unwrap().clone();
200        let generated_json = &serde_json::to_value(context_obj)?;
201        let pretty_json = serde_json::to_string_pretty(&generated_json)?;
202        std::fs::write(path, format!("{pretty_json}\n"))?;
203    }
204    Ok(())
205}
206
207/// Returns a new Context and Solver for solving.
208pub(crate) fn init_context(
209    global_args: &GlobalArgs,
210    essence_file: PathBuf,
211    param_file: Option<PathBuf>,
212) -> anyhow::Result<Arc<RwLock<Context<'static>>>> {
213    let default_rule_trace_enabled = global_args.rule_trace.is_some();
214    let rule_attempt_trace_enabled = global_args.rule_attempt_trace.is_some();
215    let rule_trace_aggregates_enabled = global_args.rule_trace_aggregates.is_some();
216    let rule_trace_enabled =
217        default_rule_trace_enabled || rule_attempt_trace_enabled || rule_trace_aggregates_enabled;
218
219    set_current_parser(global_args.parser);
220    set_current_rewriter(global_args.rewriter);
221    set_comprehension_expander(global_args.comprehension_expander);
222    set_current_solver_family(global_args.solver);
223    set_minion_discrete_threshold(global_args.minion_discrete_threshold);
224    set_rule_trace_enabled(rule_trace_enabled);
225    set_default_rule_trace_enabled(default_rule_trace_enabled);
226    set_rule_attempt_trace_enabled(rule_attempt_trace_enabled);
227    set_rule_trace_aggregates_enabled(rule_trace_aggregates_enabled);
228
229    let target_family = global_args.solver;
230    let mut extra_rule_sets: Vec<&str> = DEFAULT_RULE_SETS.to_vec();
231    for rs in &global_args.extra_rule_sets {
232        extra_rule_sets.push(rs.as_str());
233    }
234
235    let rule_sets = match resolve_rule_sets(target_family, &extra_rule_sets) {
236        Ok(rs) => rs,
237        Err(e) => {
238            tracing::error!("Error resolving rule sets: {}", e);
239            exit(1);
240        }
241    };
242
243    tracing::info!(
244        target: "conjure::stage",
245        count = rule_sets.len(),
246        "resolved rule sets"
247    );
248    tracing::debug!(
249        rule_sets = %rule_sets
250            .iter()
251            .map(|rule_set| rule_set.name)
252            .collect::<Vec<_>>()
253            .join(", "),
254        "enabled rule sets"
255    );
256
257    let rules = get_rules(&rule_sets)?.into_iter().collect::<Vec<_>>();
258    tracing::debug!(
259        "Rules: {}",
260        rules
261            .iter()
262            .map(|rd| format!("{rd}"))
263            .collect::<Vec<_>>()
264            .join("\n")
265    );
266    let context = Context::new_ptr(
267        target_family,
268        extra_rule_sets.iter().map(|rs| rs.to_string()).collect(),
269        rules,
270        rule_sets.clone(),
271    );
272
273    context.write().unwrap().essence_file_name = Some(essence_file.to_str().expect("").into());
274    if let Some(param_file) = param_file {
275        context.write().unwrap().param_file_name = Some(param_file.to_str().expect("").into());
276    }
277
278    Ok(context)
279}
280
281pub(crate) fn init_solver(global_args: &GlobalArgs) -> Solver {
282    let family = global_args.solver;
283    let timeout = global_args.solver_timeout.map(Duration::from);
284
285    match family {
286        SolverFamily::Minion => Solver::new(
287            Minion::with_search_orders(global_args.minion_varorder, global_args.minion_valorder)
288                .with_solver_seed(global_args.solver_seed)
289                .with_timeout(timeout),
290        ),
291        SolverFamily::Sat => Solver::new(
292            Sat::default()
293                .with_solver_seed(global_args.solver_seed)
294                .with_timeout(timeout),
295        ),
296        SolverFamily::Z3 => {
297            Solver::new(Smt::new(timeout).with_solver_seed(global_args.solver_seed))
298        }
299    }
300}
301
302pub(crate) fn parse(
303    global_args: &GlobalArgs,
304    context: Arc<RwLock<Context<'static>>>,
305    file_path: &str,
306) -> anyhow::Result<Model> {
307    tracing::info!(target: "conjure::stage", path = %file_path, "parsing input model");
308
309    match global_args.parser {
310        conjure_cp::settings::Parser::TreeSitter => {
311            parse_essence_file_native(file_path, context.clone()).map_err(|e| e.into())
312        }
313        conjure_cp::settings::Parser::ViaConjure => parse_with_conjure(file_path, context.clone()),
314    }
315}
316
317/// Parse an Essence or simplified-JSON parameter file.
318pub(crate) fn parse_param(
319    global_args: &GlobalArgs,
320    context: Arc<RwLock<Context<'static>>>,
321    file_path: &str,
322    problem_model: &Model,
323) -> anyhow::Result<Model> {
324    if file_path.ends_with(".json") {
325        tracing::info!(target: "conjure::stage", path = %file_path, "parsing parameter file");
326        let text = std::fs::read_to_string(file_path)?;
327        let given_domains = domains_from_model(problem_model);
328        let params = params_from_simplified_json_str(&text, &given_domains)?;
329        return Ok(param_model_from_assignments(
330            params,
331            &given_domains,
332            context,
333        ));
334    }
335    parse(global_args, context, file_path)
336}
337
338pub(crate) fn parse_with_conjure(
339    input_file: &str,
340    context: Arc<RwLock<Context<'static>>>,
341) -> anyhow::Result<Model> {
342    conjure_executable().map_err(|e| anyhow!("Could not find correct conjure executable: {e}"))?;
343
344    let mut cmd = std::process::Command::new("conjure");
345    let output = cmd
346        .arg("pretty")
347        .arg("--output-format=astjson")
348        .arg(input_file)
349        .output()?;
350
351    if !output.status.success() {
352        println!("Parsing error: {}", String::from_utf8(output.stderr)?);
353    }
354
355    let astjson = String::from_utf8(output.stdout)?;
356
357    if cfg!(feature = "extra-rule-checks") {
358        tracing::debug!("extra-rule-checks: enabled");
359    } else {
360        tracing::debug!("extra-rule-checks: disabled");
361    }
362
363    model_from_json(&astjson, context.clone()).map_err(|e| anyhow!(e))
364}
365
366pub(crate) fn rewrite(
367    model: Model,
368    global_args: &GlobalArgs,
369    context: Arc<RwLock<Context<'static>>>,
370) -> anyhow::Result<Model> {
371    tracing::debug!(model = %model, "initial model");
372
373    let rewriter = global_args.rewriter;
374    set_current_rewriter(rewriter);
375
376    let comprehension_expander = global_args.comprehension_expander;
377    set_comprehension_expander(comprehension_expander);
378    tracing::debug!(%comprehension_expander, "configured comprehension expander");
379
380    set_heuristic(global_args.heuristic);
381    set_heuristic_seed(global_args.seed);
382    set_heuristic_responses(global_args.responses.clone());
383    set_channelling(global_args.channelling);
384    tracing::debug!(
385        "Heuristic: {}, seed: {}, responses: {:?}, channelling: {}, solver seed: {}",
386        global_args.heuristic,
387        global_args.seed,
388        global_args.responses,
389        global_args.channelling,
390        global_args.solver_seed
391    );
392
393    let rule_sets = context.read().unwrap().rule_sets.clone();
394
395    let Rewriter::Rewrite(config) = rewriter;
396    tracing::info!(target: "conjure::stage", %config, "rewriting model");
397    let new_model = rewrite_model(&model, &rule_sets, config)?;
398
399    tracing::debug!(model = %new_model, "rewritten model");
400    Ok(new_model)
401}
402
403fn run_solver(
404    solver: Solver,
405    global_args: &GlobalArgs,
406    cmd_args: &Args,
407    model: Model,
408) -> anyhow::Result<()> {
409    let domains = domains_from_model(&model);
410    let solutions = get_solutions(
411        solver,
412        model,
413        cmd_args.number_of_solutions.as_solver_limit(),
414        cmd_args.keep_intermediate_solutions,
415        &global_args.save_solver_input_file,
416        global_args.rule_trace_cdp,
417    )?;
418    tracing::debug!(solutions = %solutions_to_json(&solutions), "solver solutions");
419
420    let solutions = coerce_bools_in_solutions(&solutions, &domains);
421    write_solutions(&solutions, cmd_args)?;
422    Ok(())
423}
424
425/// Turn solver `0`/`1` assignments back into booleans when the find domain is bool, so JSON/Essence
426/// output matches Conjure's simplified JSON (`true`/`false`).
427fn coerce_bools_in_solutions(
428    solutions: &[std::collections::BTreeMap<conjure_cp::ast::Name, conjure_cp::ast::Literal>],
429    domains: &std::collections::BTreeMap<conjure_cp::ast::Name, conjure_cp::ast::DomainPtr>,
430) -> Vec<std::collections::BTreeMap<conjure_cp::ast::Name, conjure_cp::ast::Literal>> {
431    use conjure_cp::ast::{GroundDomain, Literal, Name};
432    solutions
433        .iter()
434        .map(|solution| {
435            solution
436                .iter()
437                .map(|(name, value)| {
438                    let value = match domains.get(name).and_then(|domain| domain.as_ground()) {
439                        Some(GroundDomain::Bool) => match value {
440                            Literal::Int(1) => Literal::Bool(true),
441                            Literal::Int(0) => Literal::Bool(false),
442                            other => other.clone(),
443                        },
444                        _ => value.clone(),
445                    };
446                    (name.clone(), value)
447                })
448                .collect::<std::collections::BTreeMap<Name, Literal>>()
449        })
450        .collect()
451}
452
453fn write_solutions(
454    solutions: &[std::collections::BTreeMap<conjure_cp::ast::Name, conjure_cp::ast::Literal>],
455    cmd_args: &Args,
456) -> anyhow::Result<()> {
457    if cmd_args.solutions_in_one_file {
458        let body = match cmd_args.output_format {
459            OutputFormat::Essence => solutions_to_essence(solutions),
460            OutputFormat::Json => solutions_to_simplified_json_string(solutions)?,
461        };
462        match &cmd_args.output {
463            None => print!("{body}"),
464            Some(path) => {
465                std::fs::write(path, body.as_bytes())?;
466                println!("Solutions saved to {:?}", path.canonicalize()?);
467            }
468        }
469        return Ok(());
470    }
471
472    // One file / record per solution.
473    for (index, solution) in solutions.iter().enumerate() {
474        let body = match cmd_args.output_format {
475            OutputFormat::Essence => solutions_to_essence(std::slice::from_ref(solution)),
476            OutputFormat::Json => {
477                let value = solution_to_simplified_json(solution)?;
478                format!("{}\n", serde_json::to_string_pretty(&value)?)
479            }
480        };
481        match &cmd_args.output {
482            None => print!("{body}"),
483            Some(path) => {
484                let file_path = per_solution_output_path(path, index + 1, cmd_args.output_format);
485                std::fs::write(&file_path, body.as_bytes())?;
486                println!("Solution saved to {:?}", file_path.canonicalize()?);
487            }
488        }
489    }
490    Ok(())
491}
492
493fn per_solution_output_path(base: &Path, index: usize, format: OutputFormat) -> PathBuf {
494    let stem = base
495        .file_stem()
496        .and_then(|s| s.to_str())
497        .unwrap_or("solution");
498    let parent = base.parent().unwrap_or_else(|| std::path::Path::new("."));
499    let extension = match format {
500        OutputFormat::Essence => "solution",
501        OutputFormat::Json => "solution.json",
502    };
503    parent.join(format!("{stem}-{index:06}.{extension}"))
504}
conjure_oxide/solve.rs

conjure_oxide/
solve.rs
