conjure_oxide/
solve.rs

1//! conjure_oxide solve sub-command
2#![allow(clippy::unwrap_used)]
3use std::{
4    fs::File,
5    io::Write as _,
6    path::PathBuf,
7    process::exit,
8    sync::{Arc, RwLock},
9};
10
11use anyhow::{anyhow, ensure};
12use clap::ValueHint;
13use conjure_cp::{
14    Model,
15    ast::comprehension::USE_OPTIMISED_REWRITER_FOR_COMPREHENSIONS,
16    context::Context,
17    rule_engine::{resolve_rule_sets, rewrite_morph, rewrite_naive},
18    solver::Solver,
19};
20use conjure_cp::{defaults::DEFAULT_RULE_SETS, solver::adaptors::smt::TheoryConfig};
21use conjure_cp::{
22    parse::conjure_json::model_from_json, rule_engine::get_rules, solver::SolverFamily,
23};
24use conjure_cp::{parse::tree_sitter::parse_essence_file_native, solver::adaptors::*};
25use conjure_cp_cli::find_conjure::conjure_executable;
26use conjure_cp_cli::utils::conjure::{get_solutions, solutions_to_json};
27use serde_json::to_string_pretty;
28
29use crate::cli::{GlobalArgs, LOGGING_HELP_HEADING};
30
31#[derive(Clone, Debug, clap::Args)]
32pub struct Args {
33    /// The input Essence file
34    #[arg(value_name = "INPUT_ESSENCE", value_hint = ValueHint::FilePath)]
35    pub input_file: PathBuf,
36
37    /// Save execution info as JSON to the given filepath.
38    #[arg(long ,value_hint=ValueHint::FilePath,help_heading=LOGGING_HELP_HEADING)]
39    pub info_json_path: Option<PathBuf>,
40
41    /// Do not run the solver.
42    ///
43    /// The rewritten model is printed to stdout in an Essence-style syntax
44    /// (but is not necessarily valid Essence).
45    #[arg(long, default_value_t = false)]
46    pub no_run_solver: bool,
47
48    /// Number of solutions to return. 0 returns all solutions
49    #[arg(long, default_value_t = 0, short = 'n')]
50    pub number_of_solutions: i32,
51
52    /// Save solutions to the given JSON file
53    #[arg(long, short = 'o', value_hint = ValueHint::FilePath,help_heading=LOGGING_HELP_HEADING)]
54    pub output: Option<PathBuf>,
55}
56
57pub fn run_solve_command(global_args: GlobalArgs, solve_args: Args) -> anyhow::Result<()> {
58    let input_file = solve_args.input_file.clone();
59
60    // each step is in its own method so that similar commands
61    // (e.g. testsolve) can reuse some of these steps.
62
63    let context = init_context(&global_args, input_file)?;
64    let model = parse(&global_args, Arc::clone(&context))?;
65    let rewritten_model = rewrite(model, &global_args, Arc::clone(&context))?;
66    let solver = init_solver(global_args.solver);
67
68    if solve_args.no_run_solver {
69        println!("{}", &rewritten_model);
70
71        if let Some(path) = global_args.save_solver_input_file {
72            let solver = solver.load_model(rewritten_model)?;
73            eprintln!("Writing solver input file to {}", path.display());
74            let mut file: Box<dyn std::io::Write> = Box::new(File::create(path)?);
75            solver.write_solver_input_file(&mut file)?;
76        }
77    } else {
78        run_solver(solver, &global_args, &solve_args, rewritten_model)?
79    }
80
81    // still do postamble even if we didn't run the solver
82    if let Some(ref path) = solve_args.info_json_path {
83        let context_obj = context.read().unwrap().clone();
84        let generated_json = &serde_json::to_value(context_obj)?;
85        let pretty_json = serde_json::to_string_pretty(&generated_json)?;
86        File::create(path)?.write_all(pretty_json.as_bytes())?;
87    }
88    Ok(())
89}
90
91/// Returns a new Context and Solver for solving.
92pub(crate) fn init_context(
93    global_args: &GlobalArgs,
94    input_file: PathBuf,
95) -> anyhow::Result<Arc<RwLock<Context<'static>>>> {
96    let target_family = global_args.solver;
97    let mut extra_rule_sets: Vec<&str> = DEFAULT_RULE_SETS.to_vec();
98    for rs in &global_args.extra_rule_sets {
99        extra_rule_sets.push(rs.as_str());
100    }
101
102    if global_args.no_use_expand_ac {
103        extra_rule_sets.pop_if(|x| x == &"Better_AC_Comprehension_Expansion");
104    }
105
106    let rule_sets = match resolve_rule_sets(target_family, &extra_rule_sets) {
107        Ok(rs) => rs,
108        Err(e) => {
109            tracing::error!("Error resolving rule sets: {}", e);
110            exit(1);
111        }
112    };
113
114    let pretty_rule_sets = rule_sets
115        .iter()
116        .map(|rule_set| rule_set.name)
117        .collect::<Vec<_>>()
118        .join(", ");
119
120    tracing::info!("Enabled rule sets: [{}]", pretty_rule_sets);
121    tracing::info!(
122        target: "file",
123        "Rule sets: {}",
124        pretty_rule_sets
125    );
126
127    let rules = get_rules(&rule_sets)?.into_iter().collect::<Vec<_>>();
128    tracing::info!(
129        target: "file",
130        "Rules: {}",
131        rules.iter().map(|rd| format!("{rd}")).collect::<Vec<_>>().join("\n")
132    );
133    let context = Context::new_ptr(
134        target_family,
135        extra_rule_sets.iter().map(|rs| rs.to_string()).collect(),
136        rules,
137        rule_sets.clone(),
138    );
139
140    context.write().unwrap().file_name = Some(input_file.to_str().expect("").into());
141
142    Ok(context)
143}
144
145pub(crate) fn init_solver(family: SolverFamily) -> Solver {
146    match family {
147        SolverFamily::Minion => Solver::new(Minion::default()),
148        SolverFamily::Sat => Solver::new(Sat::default()),
149        SolverFamily::Smt(TheoryConfig { ints, matrices }) => Solver::new(Smt::new(ints, matrices)),
150    }
151}
152
153pub(crate) fn parse(
154    global_args: &GlobalArgs,
155    context: Arc<RwLock<Context<'static>>>,
156) -> anyhow::Result<Model> {
157    let input_file: String = context
158        .read()
159        .unwrap()
160        .file_name
161        .clone()
162        .expect("context should contain the input file");
163
164    tracing::info!(target: "file", "Input file: {}", input_file);
165    if global_args.use_native_parser {
166        parse_essence_file_native(input_file.as_str(), context.clone()).map_err(|e| e.into())
167    } else {
168        conjure_executable()
169            .map_err(|e| anyhow!("Could not find correct conjure executable: {e}"))?;
170
171        let mut cmd = std::process::Command::new("conjure");
172        let output = cmd
173            .arg("pretty")
174            .arg("--output-format=astjson")
175            .arg(input_file)
176            .output()?;
177
178        let conjure_stderr = String::from_utf8(output.stderr)?;
179
180        ensure!(conjure_stderr.is_empty(), conjure_stderr);
181
182        let astjson = String::from_utf8(output.stdout)?;
183
184        if cfg!(feature = "extra-rule-checks") {
185            tracing::info!("extra-rule-checks: enabled");
186        } else {
187            tracing::info!("extra-rule-checks: disabled");
188        }
189
190        model_from_json(&astjson, context.clone()).map_err(|e| anyhow!(e))
191    }
192}
193
194pub(crate) fn rewrite(
195    model: Model,
196    global_args: &GlobalArgs,
197    context: Arc<RwLock<Context<'static>>>,
198) -> anyhow::Result<Model> {
199    tracing::info!("Initial model: \n{}\n", model);
200
201    let rule_sets = context.read().unwrap().rule_sets.clone();
202
203    let new_model = if global_args.use_optimised_rewriter {
204        USE_OPTIMISED_REWRITER_FOR_COMPREHENSIONS.store(true, std::sync::atomic::Ordering::Relaxed);
205        tracing::info!("Rewriting the model using the optimising rewriter");
206        rewrite_morph(
207            model,
208            &rule_sets,
209            global_args.check_equally_applicable_rules,
210        )
211    } else {
212        tracing::info!("Rewriting the model using the default / naive rewriter");
213        if global_args.exit_after_unrolling {
214            tracing::info!("Exiting after unrolling");
215        }
216        rewrite_naive(
217            &model,
218            &rule_sets,
219            global_args.check_equally_applicable_rules,
220            global_args.exit_after_unrolling,
221        )?
222    };
223
224    tracing::info!("Rewritten model: \n{}\n", new_model);
225    Ok(new_model)
226}
227
228fn run_solver(
229    solver: Solver,
230    global_args: &GlobalArgs,
231    cmd_args: &Args,
232    model: Model,
233) -> anyhow::Result<()> {
234    let out_file: Option<File> = match &cmd_args.output {
235        None => None,
236        Some(pth) => Some(
237            File::options()
238                .create(true)
239                .truncate(true)
240                .write(true)
241                .open(pth)?,
242        ),
243    };
244
245    let solutions = get_solutions(
246        solver,
247        model,
248        cmd_args.number_of_solutions,
249        &global_args.save_solver_input_file,
250    )?;
251    tracing::info!(target: "file", "Solutions: {}", solutions_to_json(&solutions));
252
253    let solutions_json = solutions_to_json(&solutions);
254    let solutions_str = to_string_pretty(&solutions_json)?;
255    match out_file {
256        None => {
257            println!("Solutions:");
258            println!("{solutions_str}");
259        }
260        Some(mut outf) => {
261            outf.write_all(solutions_str.as_bytes())?;
262            println!(
263                "Solutions saved to {:?}",
264                &cmd_args.output.clone().unwrap().canonicalize()?
265            )
266        }
267    }
268    Ok(())
269}
conjure_oxide/solve.rs

conjure_oxide/
solve.rs
