conjure_oxide/utils/
conjure.rs

1use std::collections::BTreeMap;
2use std::path::PathBuf;
3use std::rc::Rc;
4use std::string::ToString;
5use std::sync::{Arc, Mutex, RwLock};
6
7use conjure_cp_core::ast::{DeclarationKind, Literal, Name};
8use conjure_cp_core::bug;
9use conjure_cp_core::context::Context;
10
11use conjure_cp_core::solver::adaptors::Sat;
12use serde_json::{Map, Value as JsonValue};
13
14use itertools::Itertools as _;
15use tempfile::tempdir;
16
17use crate::EssenceParseError;
18use crate::Model;
19use crate::parse_essence_file;
20use crate::solver::Solver;
21use crate::solver::adaptors::Minion;
22use crate::utils::json::sort_json_object;
23
24use glob::glob;
25
26use rayon::iter::{IntoParallelRefIterator, ParallelIterator};
27
28pub fn get_minion_solutions(
29    model: Model,
30    num_sols: i32,
31    solver_input_file: &Option<PathBuf>,
32) -> Result<Vec<BTreeMap<Name, Literal>>, anyhow::Error> {
33    let solver = Solver::new(Minion::new());
34    eprintln!("Building Minion model...");
35
36    // for later...
37    let symbols_rc = Rc::clone(model.as_submodel().symbols_ptr_unchecked());
38
39    let solver = solver.load_model(model)?;
40
41    if let Some(solver_input_file) = solver_input_file {
42        eprintln!(
43            "Writing solver input file to {}",
44            solver_input_file.display()
45        );
46        let mut file = std::fs::File::create(solver_input_file)?;
47        solver.write_solver_input_file(&mut file)?;
48    }
49
50    eprintln!("Running Minion...");
51
52    let all_solutions_ref = Arc::new(Mutex::<Vec<BTreeMap<Name, Literal>>>::new(vec![]));
53    let all_solutions_ref_2 = all_solutions_ref.clone();
54    let solver = if num_sols > 0 {
55        let sols_left = Mutex::new(num_sols);
56
57        #[allow(clippy::unwrap_used)]
58        solver
59            .solve(Box::new(move |sols| {
60                let mut all_solutions = (*all_solutions_ref_2).lock().unwrap();
61                (*all_solutions).push(sols.into_iter().collect());
62                let mut sols_left = sols_left.lock().unwrap();
63                *sols_left -= 1;
64
65                *sols_left != 0
66            }))
67            .unwrap()
68    } else {
69        #[allow(clippy::unwrap_used)]
70        solver
71            .solve(Box::new(move |sols| {
72                let mut all_solutions = (*all_solutions_ref_2).lock().unwrap();
73                (*all_solutions).push(sols.into_iter().collect());
74                true
75            }))
76            .unwrap()
77    };
78
79    solver.save_stats_to_context();
80
81    #[allow(clippy::unwrap_used)]
82    let mut sols_guard = (*all_solutions_ref).lock().unwrap();
83    let sols = &mut *sols_guard;
84    let symbols = symbols_rc.borrow();
85
86    let names = symbols.clone().into_iter().map(|x| x.0).collect_vec();
87    let representations = names
88        .into_iter()
89        .filter_map(|x| symbols.representations_for(&x).map(|repr| (x, repr)))
90        .filter_map(|(name, reprs)| {
91            if reprs.is_empty() {
92                return None;
93            }
94            assert!(
95                reprs.len() <= 1,
96                "multiple representations for a variable is not yet implemented"
97            );
98
99            assert_eq!(
100                reprs[0].len(),
101                1,
102                "nested representations are not yet implemented"
103            );
104            Some((name, reprs[0][0].clone()))
105        })
106        .collect_vec();
107
108    for sol in sols.iter_mut() {
109        for (name, representation) in representations.iter() {
110            let value = representation.value_up(sol).unwrap();
111            sol.insert(name.clone(), value);
112        }
113
114        // remove represented variables
115        *sol = sol
116            .clone()
117            .into_iter()
118            .filter(|(name, _)| !matches!(name, Name::Represented(_)))
119            .collect();
120    }
121
122    Ok(sols.clone().into_iter().filter(|x| !x.is_empty()).collect())
123}
124
125pub fn get_sat_solutions(
126    model: Model,
127    num_sols: i32,
128    solver_input_file: &Option<PathBuf>,
129) -> Result<Vec<BTreeMap<Name, Literal>>, anyhow::Error> {
130    let solver = Solver::new(Sat::default());
131    eprintln!("Building SAT model...");
132    let solver = solver.load_model(model)?;
133
134    if let Some(solver_input_file) = solver_input_file {
135        eprintln!(
136            "Writing solver input file to {}",
137            solver_input_file.display()
138        );
139        let mut file = std::fs::File::create(solver_input_file)?;
140        solver.write_solver_input_file(&mut file)?;
141    }
142
143    eprintln!("Running SAT...");
144
145    let all_solutions_ref = Arc::new(Mutex::<Vec<BTreeMap<Name, Literal>>>::new(vec![]));
146    let all_solutions_ref_2 = all_solutions_ref.clone();
147    let solver = if num_sols > 0 {
148        let sols_left = Mutex::new(num_sols);
149
150        #[allow(clippy::unwrap_used)]
151        solver
152            .solve(Box::new(move |sols| {
153                let mut all_solutions = (*all_solutions_ref_2).lock().unwrap();
154                (*all_solutions).push(sols.into_iter().collect());
155                let mut sols_left = sols_left.lock().unwrap();
156                *sols_left -= 1;
157
158                *sols_left != 0
159            }))
160            .unwrap()
161    } else {
162        #[allow(clippy::unwrap_used)]
163        solver
164            .solve(Box::new(move |sols| {
165                let mut all_solutions = (*all_solutions_ref_2).lock().unwrap();
166                (*all_solutions).push(sols.into_iter().collect());
167                true
168            }))
169            .unwrap()
170    };
171
172    solver.save_stats_to_context();
173
174    #[allow(clippy::unwrap_used)]
175    let sols = (*all_solutions_ref).lock().unwrap();
176
177    Ok((*sols).clone())
178}
179
180#[allow(clippy::unwrap_used)]
181pub fn get_solutions_from_conjure(
182    essence_file: &str,
183    context: Arc<RwLock<Context<'static>>>,
184) -> Result<Vec<BTreeMap<Name, Literal>>, EssenceParseError> {
185    let tmp_dir = tempdir().unwrap();
186
187    let mut cmd = std::process::Command::new("conjure");
188    let output = cmd
189        .arg("solve")
190        .arg("--number-of-solutions=all")
191        .arg("--copy-solutions=no")
192        .arg("-o")
193        .arg(tmp_dir.path())
194        .arg(essence_file)
195        .output()
196        .map_err(|e| EssenceParseError::ConjureSolveError(e.to_string()))?;
197
198    if !output.status.success() {
199        return Err(EssenceParseError::ConjureSolveError(format!(
200            "conjure solve exited with failure: {}",
201            String::from_utf8(output.stderr).unwrap()
202        )));
203    }
204
205    let solutions_files: Vec<_> = glob(&format!("{}/*.solution", tmp_dir.path().display()))
206        .unwrap()
207        .collect();
208
209    let solutions_set: Vec<_> = solutions_files
210        .par_iter()
211        .map(|solutions_file| {
212            let solutions_file = solutions_file.as_ref().unwrap();
213            let model = parse_essence_file(solutions_file.to_str().unwrap(), Arc::clone(&context))
214                .expect("conjure solutions files to be parsable");
215
216            let mut solutions = BTreeMap::new();
217            for (name, decl) in model.as_submodel().symbols().clone().into_iter() {
218                match &decl.kind() as &DeclarationKind {
219                    conjure_cp_core::ast::DeclarationKind::ValueLetting(expression) => {
220                        let literal = expression
221                            .clone()
222                            .into_literal()
223                            .expect("lettings in a solution should only contain literals");
224                        solutions.insert(name, literal);
225                    }
226                    _ => {
227                        bug!("only expect value letting declarations in solutions")
228                    }
229                }
230            }
231            solutions
232        })
233        .collect();
234
235    Ok(solutions_set
236        .into_iter()
237        .filter(|x| !x.is_empty())
238        .collect())
239}
240
241pub fn solutions_to_json(solutions: &Vec<BTreeMap<Name, Literal>>) -> JsonValue {
242    let mut json_solutions = Vec::new();
243    for solution in solutions {
244        let mut json_solution = Map::new();
245        for (var_name, constant) in solution {
246            let serialized_constant = serde_json::to_value(constant).unwrap();
247            json_solution.insert(var_name.to_string(), serialized_constant);
248        }
249        json_solutions.push(JsonValue::Object(json_solution));
250    }
251    let ans = JsonValue::Array(json_solutions);
252    sort_json_object(&ans, true)
253}
conjure_oxide/utils/conjure.rs

conjure_oxide/utils/
conjure.rs
