pub fn get_solutions(

    solver: Solver,

    model: Model,

    num_sols: i32,

    solver_input_file: &Option<PathBuf>,

) -> Result<Vec<BTreeMap<Name, Literal>>, anyhow::Error> {

    let adaptor_name = solver.get_name();

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

    let symbols_rc = Rc::clone(model.as_submodel().symbols_ptr_unchecked());

    let solver = solver.load_model(model)?;

    if let Some(solver_input_file) = solver_input_file {

        eprintln!(

            solver_input_file.display()

        let file = Box::new(std::fs::File::create(solver_input_file)?);

        solver.write_solver_input_file(&mut (file as Box<dyn std::io::Write>))?;

    }

    eprintln!("Running {adaptor_name}...");

    let all_solutions_ref = Arc::new(Mutex::<Vec<BTreeMap<Name, Literal>>>::new(vec![]));

    let all_solutions_ref_2 = all_solutions_ref.clone();

    let solver = if num_sols > 0 {

        let sols_left = Mutex::new(num_sols);

        solver

            .solve(Box::new(move |sols| {

                let mut all_solutions = (*all_solutions_ref_2).lock().unwrap();

                (*all_solutions).push(sols.into_iter().collect());

                let mut sols_left = sols_left.lock().unwrap();

                *sols_left -= 1;

                *sols_left != 0

            }))

            .unwrap()

        solver

            .solve(Box::new(move |sols| {

                let mut all_solutions = (*all_solutions_ref_2).lock().unwrap();

                (*all_solutions).push(sols.into_iter().collect());

                true

            }))

            .unwrap()

    solver.save_stats_to_context();

    let mut sols_guard = (*all_solutions_ref).lock().unwrap();

    let sols = &mut *sols_guard;

    let symbols = symbols_rc.borrow();

    let names = symbols.clone().into_iter().map(|x| x.0).collect_vec();

    let representations = names

        .into_iter()

        .filter_map(|x| symbols.representations_for(&x).map(|repr| (x, repr)))

        .filter_map(|(name, reprs)| {

            if reprs.is_empty() {

                return None;

            }

            assert!(

                reprs.len() <= 1,

            assert_eq!(

                reprs[0].len(),

            Some((name, reprs[0][0].clone()))

        })

        .collect_vec();

    for sol in sols.iter_mut() {

        for (name, representation) in representations.iter() {

            let value = representation.value_up(sol).unwrap();

            sol.insert(name.clone(), value);

        }

        *sol = sol

            .clone()

            .into_iter()

            .filter(|(name, _)| {

                !matches!(name, Name::Represented(_)) && !matches!(name, Name::Machine(_))

            })

            .collect();

    sols.retain(|x| !x.is_empty());

    Ok(sols.clone())

}

pub fn get_solutions_from_conjure(

    essence_file: &str,

    context: Arc<RwLock<Context<'static>>>,

) -> Result<Vec<BTreeMap<Name, Literal>>, anyhow::Error> {

    let tmp_dir = tempdir()?;

    let mut cmd = std::process::Command::new("conjure");

    let output = cmd

        .arg("solve")

        .arg("--number-of-solutions=all")

        .arg("--copy-solutions=no")

        .arg("-o")

        .arg(tmp_dir.path())

        .arg(essence_file)

        .output()?;

    if !output.status.success() {

        let stderr =

            String::from_utf8(output.stderr).unwrap_or_else(|e| e.utf8_error().to_string());

        return Err(anyhow::Error::msg(format!(

            "Error: `conjure solve` exited with code {}; stderr: {}",

            output.status, stderr

        )));

    }

    let solutions_files: Vec<_> =

        glob(&format!("{}/*.solution", tmp_dir.path().display()))?.collect();

    let solutions_set: Vec<_> = solutions_files

        .par_iter()

        .map(|solutions_file| {

            let solutions_file = solutions_file.as_ref().unwrap();

            let model = parse_essence_file(solutions_file.to_str().unwrap(), Arc::clone(&context))

                .expect("conjure solutions files to be parsable");

            let mut solutions = BTreeMap::new();

            for (name, decl) in model.as_submodel().symbols().clone().into_iter() {

                match &decl.kind() as &DeclarationKind {

                    conjure_cp::ast::DeclarationKind::ValueLetting(expression) => {

                        let literal = expression

                            .clone()

                            .into_literal()

                            .expect("lettings in a solution should only contain literals");

                        solutions.insert(name, literal);

                    }

            solutions

        })

        .collect();

    Ok(solutions_set

        .into_iter()

        .filter(|x| !x.is_empty())

        .collect())

}

pub fn solutions_to_json(solutions: &Vec<BTreeMap<Name, Literal>>) -> JsonValue {

    let mut json_solutions = Vec::new();

    for solution in solutions {

        let mut json_solution = Map::new();

        for (var_name, constant) in solution {

            let serialized_constant = serde_json::to_value(constant).unwrap();

            json_solution.insert(var_name.to_string(), serialized_constant);

        }

        json_solutions.push(JsonValue::Object(json_solution));

    let ans = JsonValue::Array(json_solutions);

    sort_json_object(&ans, true)

}