1
use std::collections::BTreeMap;
2
use std::path::PathBuf;
3
use std::string::ToString;
4
use std::sync::{Arc, Mutex, RwLock};
5

            
6
use conjure_cp::ast::{DeclarationKind, Literal, Name};
7
use conjure_cp::bug;
8
use conjure_cp::context::Context;
9

            
10
use serde_json::{Map, Value as JsonValue};
11

            
12
use itertools::Itertools as _;
13
use tempfile::tempdir;
14

            
15
use crate::utils::json::sort_json_object;
16
use conjure_cp::Model;
17
use conjure_cp::parse::tree_sitter::parse_essence_file;
18
use conjure_cp::solver::Solver;
19

            
20
use glob::glob;
21

            
22
use rayon::iter::{IntoParallelRefIterator, ParallelIterator};
23

            
24
1126
pub fn get_solutions(
25
1126
    solver: Solver,
26
1126
    model: Model,
27
1126
    num_sols: i32,
28
1126
    solver_input_file: &Option<PathBuf>,
29
1126
) -> Result<Vec<BTreeMap<Name, Literal>>, anyhow::Error> {
30
1126
    let adaptor_name = solver.get_name();
31

            
32
1126
    eprintln!("Building {adaptor_name} model...");
33

            
34
    // Create for later since we consume the model when loading it
35
1126
    let symbols_ptr = model.as_submodel().symbols_ptr_unchecked().clone();
36

            
37
1126
    let solver = solver.load_model(model)?;
38

            
39
1126
    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 file = Box::new(std::fs::File::create(solver_input_file)?);
45
        solver.write_solver_input_file(&mut (file as Box<dyn std::io::Write>))?;
46
1126
    }
47

            
48
1126
    eprintln!("Running {adaptor_name}...");
49

            
50
    // Create two arcs, one to pass into the solver callback, one to get solutions out later
51
1126
    let all_solutions_ref = Arc::new(Mutex::<Vec<BTreeMap<Name, Literal>>>::new(vec![]));
52
1126
    let all_solutions_ref_2 = all_solutions_ref.clone();
53

            
54
1126
    let solver = if num_sols > 0 {
55
        // Get num_sols solutions
56
        let sols_left = Mutex::new(num_sols);
57

            
58
        #[allow(clippy::unwrap_used)]
59
        solver
60
            .solve(Box::new(move |sols| {
61
                let mut all_solutions = (*all_solutions_ref_2).lock().unwrap();
62
                (*all_solutions).push(sols.into_iter().collect());
63
                let mut sols_left = sols_left.lock().unwrap();
64
                *sols_left -= 1;
65

            
66
                *sols_left != 0
67
            }))
68
            .unwrap()
69
    } else {
70
        // Get all solutions
71
        #[allow(clippy::unwrap_used)]
72
1126
        solver
73
23412
            .solve(Box::new(move |sols| {
74
23412
                let mut all_solutions = (*all_solutions_ref_2).lock().unwrap();
75
23412
                (*all_solutions).push(sols.into_iter().collect());
76
23412
                true
77
23412
            }))
78
1126
            .unwrap()
79
    };
80

            
81
1126
    solver.save_stats_to_context();
82

            
83
    // Get the collections of solutions and model symbols
84
    #[allow(clippy::unwrap_used)]
85
1126
    let mut sols_guard = (*all_solutions_ref).lock().unwrap();
86
1126
    let sols = &mut *sols_guard;
87
1126
    let symbols = symbols_ptr.read();
88

            
89
    // Get the representations for each variable by name, since some variables are
90
    // divided into multiple auxiliary variables(see crate::representation::Representation)
91
1126
    let names = symbols.clone().into_iter().map(|x| x.0).collect_vec();
92
1126
    let representations = names
93
1126
        .into_iter()
94
3870
        .filter_map(|x| symbols.representations_for(&x).map(|repr| (x, repr)))
95
3494
        .filter_map(|(name, reprs)| {
96
3494
            if reprs.is_empty() {
97
3306
                return None;
98
188
            }
99
188
            assert!(
100
188
                reprs.len() <= 1,
101
                "multiple representations for a variable is not yet implemented"
102
            );
103

            
104
188
            assert_eq!(
105
188
                reprs[0].len(),
106
                1,
107
                "nested representations are not yet implemented"
108
            );
109
188
            Some((name, reprs[0][0].clone()))
110
3494
        })
111
1126
        .collect_vec();
112

            
113
23412
    for sol in sols.iter_mut() {
114
        // Get the value of complex variables using their auxiliary variables
115
23412
        for (name, representation) in representations.iter() {
116
10120
            let value = representation.value_up(sol).unwrap();
117
10120
            sol.insert(name.clone(), value);
118
10120
        }
119

            
120
        // Remove auxiliary variables since we've found the value of the
121
        // variable they represent
122
23412
        *sol = sol
123
23412
            .clone()
124
23412
            .into_iter()
125
197912
            .filter(|(name, _)| {
126
197912
                !matches!(name, Name::Represented(_)) && !matches!(name, Name::Machine(_))
127
197912
            })
128
23412
            .collect();
129
    }
130

            
131
23412
    sols.retain(|x| !x.is_empty());
132
1126
    Ok(sols.clone())
133
1126
}
134

            
135
#[allow(clippy::unwrap_used)]
136
pub fn get_solutions_from_conjure(
137
    essence_file: &str,
138
    context: Arc<RwLock<Context<'static>>>,
139
) -> Result<Vec<BTreeMap<Name, Literal>>, anyhow::Error> {
140
    let tmp_dir = tempdir()?;
141

            
142
    let mut cmd = std::process::Command::new("conjure");
143
    let output = cmd
144
        .arg("solve")
145
        .arg("--number-of-solutions=all")
146
        .arg("--copy-solutions=no")
147
        .arg("-o")
148
        .arg(tmp_dir.path())
149
        .arg(essence_file)
150
        .output()?;
151

            
152
    if !output.status.success() {
153
        let stderr =
154
            String::from_utf8(output.stderr).unwrap_or_else(|e| e.utf8_error().to_string());
155
        return Err(anyhow::Error::msg(format!(
156
            "Error: `conjure solve` exited with code {}; stderr: {}",
157
            output.status, stderr
158
        )));
159
    }
160

            
161
    let solutions_files: Vec<_> =
162
        glob(&format!("{}/*.solution", tmp_dir.path().display()))?.collect();
163

            
164
    let solutions_set: Vec<_> = solutions_files
165
        .par_iter()
166
        .map(|solutions_file| {
167
            let solutions_file = solutions_file.as_ref().unwrap();
168
            let model = parse_essence_file(solutions_file.to_str().unwrap(), Arc::clone(&context))
169
                .expect("conjure solutions files to be parsable");
170

            
171
            let mut solutions = BTreeMap::new();
172
            for (name, decl) in model.as_submodel().symbols().clone().into_iter() {
173
                match &decl.kind() as &DeclarationKind {
174
                    conjure_cp::ast::DeclarationKind::ValueLetting(expression) => {
175
                        let literal = expression
176
                            .clone()
177
                            .into_literal()
178
                            .expect("lettings in a solution should only contain literals");
179
                        solutions.insert(name, literal);
180
                    }
181
                    _ => {
182
                        bug!("only expect value letting declarations in solutions")
183
                    }
184
                }
185
            }
186
            solutions
187
        })
188
        .collect();
189

            
190
    Ok(solutions_set
191
        .into_iter()
192
        .filter(|x| !x.is_empty())
193
        .collect())
194
}
195

            
196
2248
pub fn solutions_to_json(solutions: &Vec<BTreeMap<Name, Literal>>) -> JsonValue {
197
2248
    let mut json_solutions = Vec::new();
198
46816
    for solution in solutions {
199
46816
        let mut json_solution = Map::new();
200
189120
        for (var_name, constant) in solution {
201
189120
            let serialized_constant = serde_json::to_value(constant).unwrap();
202
189120
            json_solution.insert(var_name.to_string(), serialized_constant);
203
189120
        }
204
46816
        json_solutions.push(JsonValue::Object(json_solution));
205
    }
206
2248
    let ans = JsonValue::Array(json_solutions);
207
2248
    sort_json_object(&ans, true)
208
2248
}