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    io::Write as _,
7    path::PathBuf,
8    process::exit,
9    sync::{Arc, RwLock},
10};
11
12use anyhow::anyhow;
13use clap::ValueHint;
14use conjure_cp::defaults::DEFAULT_RULE_SETS;
15use conjure_cp::instantiate::instantiate_model;
16use conjure_cp::{
17    Model,
18    context::Context,
19    rule_engine::{resolve_rule_sets, rewrite_morph, rewrite_naive},
20    settings::{
21        Rewriter, set_comprehension_expander, set_current_parser, set_current_rewriter,
22        set_current_solver_family, set_minion_discrete_threshold,
23    },
24    solver::Solver,
25};
26use conjure_cp::{
27    parse::conjure_json::model_from_json, rule_engine::get_rules, settings::SolverFamily,
28};
29use conjure_cp::{parse::tree_sitter::parse_essence_file_native, solver::adaptors::*};
30use conjure_cp_cli::find_conjure::conjure_executable;
31use conjure_cp_cli::utils::conjure::{get_solutions, solutions_to_json};
32use serde_json::to_string_pretty;
33
34use crate::cli::{GlobalArgs, LOGGING_HELP_HEADING};
35
36#[derive(Clone, Copy, Debug, PartialEq, Eq)]
37pub enum NumberOfSolutions {
38    All,
39    Limit(i32),
40}
41
42impl NumberOfSolutions {
43    fn as_solver_limit(self) -> i32 {
44        match self {
45            NumberOfSolutions::All => 0,
46            NumberOfSolutions::Limit(limit) => limit,
47        }
48    }
49}
50
51fn parse_number_of_solutions(input: &str) -> Result<NumberOfSolutions, String> {
52    if input.eq_ignore_ascii_case("all") {
53        return Ok(NumberOfSolutions::All);
54    }
55
56    let limit = input
57        .parse::<i32>()
58        .map_err(|_| "expected a positive integer or 'all'".to_string())?;
59
60    if limit <= 0 {
61        return Err("expected a positive integer or 'all'".to_string());
62    }
63
64    Ok(NumberOfSolutions::Limit(limit))
65}
66
67#[derive(Clone, Debug, clap::Args)]
68pub struct Args {
69    /// The input Essence problem file
70    #[arg(value_name = "INPUT_ESSENCE", value_hint = ValueHint::FilePath)]
71    pub essence_file: PathBuf,
72
73    /// The input Essence parameter file
74    #[arg(value_name = "PARAM_ESSENCE", value_hint = ValueHint::FilePath)]
75    pub param_file: Option<PathBuf>,
76
77    /// Save execution info as JSON to the given filepath.
78    #[arg(long ,value_hint=ValueHint::FilePath,help_heading=LOGGING_HELP_HEADING)]
79    pub info_json_path: Option<PathBuf>,
80
81    /// Do not run the solver.
82    ///
83    /// The rewritten model is printed to stdout in an Essence-style syntax
84    /// (but is not necessarily valid Essence).
85    #[arg(long, default_value_t = false)]
86    pub no_run_solver: bool,
87
88    /// Number of solutions to return. Use a positive integer, or `all`.
89    #[arg(
90        long,
91        short = 'n',
92        default_value = "1",
93        value_name = "N|all",
94        value_parser = parse_number_of_solutions
95    )]
96    pub number_of_solutions: NumberOfSolutions,
97
98    /// Save solutions to the given JSON file
99    #[arg(long, short = 'o', value_hint = ValueHint::FilePath,help_heading=LOGGING_HELP_HEADING)]
100    pub output: Option<PathBuf>,
101}
102
103pub fn run_solve_command(global_args: GlobalArgs, solve_args: Args) -> anyhow::Result<()> {
104    let essence_file = solve_args.essence_file.clone();
105    let param_file = solve_args.param_file.clone();
106
107    // each step is in its own method so that similar commands
108    // (e.g. testsolve) can reuse some of these steps.
109
110    let context = init_context(&global_args, essence_file, param_file)?;
111
112    let ctx_lock = context.read().unwrap();
113    let essence_file_name = ctx_lock
114        .essence_file_name
115        .as_ref()
116        .expect("context should contain the problem input file");
117    let param_file_name = ctx_lock.param_file_name.as_ref();
118
119    // parse models
120    let problem_model = parse(&global_args, Arc::clone(&context), essence_file_name)?;
121
122    // unify models
123    let unified_model = match param_file_name {
124        Some(param_file_name) => {
125            let param_model = parse(&global_args, Arc::clone(&context), param_file_name)?;
126            instantiate_model(problem_model, param_model)?
127        }
128        None => problem_model,
129    };
130    drop(ctx_lock);
131
132    let rewritten_model = rewrite(unified_model, &global_args, Arc::clone(&context))?;
133
134    let solver = init_solver(&global_args);
135
136    if solve_args.no_run_solver {
137        println!("{}", &rewritten_model);
138
139        if let Some(path) = global_args.save_solver_input_file {
140            let solver = solver.load_model(rewritten_model)?;
141            eprintln!("Writing solver input file to {}", path.display());
142            let mut file: Box<dyn std::io::Write> = Box::new(File::create(path)?);
143            solver.write_solver_input_file(&mut file)?;
144        }
145    } else {
146        run_solver(solver, &global_args, &solve_args, rewritten_model)?
147    }
148
149    // still do postamble even if we didn't run the solver
150    if let Some(ref path) = solve_args.info_json_path {
151        let context_obj = context.read().unwrap().clone();
152        let generated_json = &serde_json::to_value(context_obj)?;
153        let pretty_json = serde_json::to_string_pretty(&generated_json)?;
154        File::create(path)?.write_all(pretty_json.as_bytes())?;
155    }
156    Ok(())
157}
158
159/// Returns a new Context and Solver for solving.
160pub(crate) fn init_context(
161    global_args: &GlobalArgs,
162    essence_file: PathBuf,
163    param_file: Option<PathBuf>,
164) -> anyhow::Result<Arc<RwLock<Context<'static>>>> {
165    set_current_parser(global_args.parser);
166    set_current_rewriter(global_args.rewriter);
167    set_comprehension_expander(global_args.comprehension_expander);
168    set_current_solver_family(global_args.solver);
169    set_minion_discrete_threshold(global_args.minion_discrete_threshold);
170
171    let target_family = global_args.solver;
172    let mut extra_rule_sets: Vec<&str> = DEFAULT_RULE_SETS.to_vec();
173    for rs in &global_args.extra_rule_sets {
174        extra_rule_sets.push(rs.as_str());
175    }
176
177    if let SolverFamily::Sat(sat_encoding) = target_family {
178        extra_rule_sets.push(sat_encoding.as_rule_set());
179    }
180
181    let rule_sets = match resolve_rule_sets(target_family, &extra_rule_sets) {
182        Ok(rs) => rs,
183        Err(e) => {
184            tracing::error!("Error resolving rule sets: {}", e);
185            exit(1);
186        }
187    };
188
189    let pretty_rule_sets = rule_sets
190        .iter()
191        .map(|rule_set| rule_set.name)
192        .collect::<Vec<_>>()
193        .join(", ");
194
195    tracing::info!("Enabled rule sets: [{}]", pretty_rule_sets);
196    tracing::info!(
197        target: "file",
198        "Rule sets: {}",
199        pretty_rule_sets
200    );
201
202    let rules = get_rules(&rule_sets)?.into_iter().collect::<Vec<_>>();
203    tracing::info!(
204        target: "file",
205        "Rules: {}",
206        rules.iter().map(|rd| format!("{rd}")).collect::<Vec<_>>().join("\n")
207    );
208    let context = Context::new_ptr(
209        target_family,
210        extra_rule_sets.iter().map(|rs| rs.to_string()).collect(),
211        rules,
212        rule_sets.clone(),
213    );
214
215    context.write().unwrap().essence_file_name = Some(essence_file.to_str().expect("").into());
216    if let Some(param_file) = param_file {
217        context.write().unwrap().param_file_name = Some(param_file.to_str().expect("").into());
218    }
219
220    Ok(context)
221}
222
223pub(crate) fn init_solver(global_args: &GlobalArgs) -> Solver {
224    let family = global_args.solver;
225    let timeout_ms = global_args
226        .solver_timeout
227        .map(|dur| Duration::from(dur).as_millis())
228        .map(|timeout_ms| u64::try_from(timeout_ms).expect("Timeout too large"));
229
230    match family {
231        SolverFamily::Minion => Solver::new(Minion::default()),
232        SolverFamily::Sat(_) => Solver::new(Sat::default()),
233        SolverFamily::Smt(theory_cfg) => Solver::new(Smt::new(timeout_ms, theory_cfg)),
234    }
235}
236
237pub(crate) fn parse(
238    global_args: &GlobalArgs,
239    context: Arc<RwLock<Context<'static>>>,
240    file_path: &str,
241) -> anyhow::Result<Model> {
242    tracing::info!(target: "file", "Input file: {}", file_path);
243
244    match global_args.parser {
245        conjure_cp::settings::Parser::TreeSitter => {
246            parse_essence_file_native(file_path, context.clone()).map_err(|e| e.into())
247        }
248        conjure_cp::settings::Parser::ViaConjure => parse_with_conjure(file_path, context.clone()),
249    }
250}
251
252pub(crate) fn parse_with_conjure(
253    input_file: &str,
254    context: Arc<RwLock<Context<'static>>>,
255) -> anyhow::Result<Model> {
256    conjure_executable().map_err(|e| anyhow!("Could not find correct conjure executable: {e}"))?;
257
258    let mut cmd = std::process::Command::new("conjure");
259    let output = cmd
260        .arg("pretty")
261        .arg("--output-format=astjson")
262        .arg(input_file)
263        .output()?;
264
265    if !output.status.success() {
266        println!("Parsing error: {}", String::from_utf8(output.stderr)?);
267    }
268
269    let astjson = String::from_utf8(output.stdout)?;
270
271    if cfg!(feature = "extra-rule-checks") {
272        tracing::info!("extra-rule-checks: enabled");
273    } else {
274        tracing::info!("extra-rule-checks: disabled");
275    }
276
277    model_from_json(&astjson, context.clone()).map_err(|e| anyhow!(e))
278}
279
280pub(crate) fn rewrite(
281    model: Model,
282    global_args: &GlobalArgs,
283    context: Arc<RwLock<Context<'static>>>,
284) -> anyhow::Result<Model> {
285    tracing::info!("Initial model: \n{}\n", model);
286
287    set_current_rewriter(global_args.rewriter);
288
289    let comprehension_expander = global_args.comprehension_expander;
290    set_comprehension_expander(comprehension_expander);
291    tracing::info!("Comprehension expander: {}", comprehension_expander);
292
293    let rule_sets = context.read().unwrap().rule_sets.clone();
294
295    let new_model = match global_args.rewriter {
296        Rewriter::Morph => {
297            tracing::info!("Rewriting the model using the morph rewriter");
298            rewrite_morph(
299                model,
300                &rule_sets,
301                global_args.check_equally_applicable_rules,
302            )
303        }
304        Rewriter::Naive => {
305            tracing::info!("Rewriting the model using the default / naive rewriter");
306            rewrite_naive(
307                &model,
308                &rule_sets,
309                global_args.check_equally_applicable_rules,
310            )?
311        }
312    };
313
314    tracing::info!("Rewritten model: \n{}\n", new_model);
315    Ok(new_model)
316}
317
318fn run_solver(
319    solver: Solver,
320    global_args: &GlobalArgs,
321    cmd_args: &Args,
322    model: Model,
323) -> anyhow::Result<()> {
324    let out_file: Option<File> = match &cmd_args.output {
325        None => None,
326        Some(pth) => Some(
327            File::options()
328                .create(true)
329                .truncate(true)
330                .write(true)
331                .open(pth)?,
332        ),
333    };
334
335    let solutions = get_solutions(
336        solver,
337        model,
338        cmd_args.number_of_solutions.as_solver_limit(),
339        &global_args.save_solver_input_file,
340    )?;
341    tracing::info!(target: "file", "Solutions: {}", solutions_to_json(&solutions));
342
343    let solutions_json = solutions_to_json(&solutions);
344    let solutions_str = to_string_pretty(&solutions_json)?;
345    match out_file {
346        None => {
347            println!("Solutions:");
348            println!("{solutions_str}");
349        }
350        Some(mut outf) => {
351            outf.write_all(solutions_str.as_bytes())?;
352            println!(
353                "Solutions saved to {:?}",
354                &cmd_args.output.clone().unwrap().canonicalize()?
355            )
356        }
357    }
358    Ok(())
359}
conjure_oxide/solve.rs

conjure_oxide/
solve.rs
