conjure_oxide/utils/
conjure.rs

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

conjure_oxide/utils/
conjure.rs
