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

conjure_oxide/utils/
conjure.rs
