conjure_cp_cli/utils/

conjure.rs

use std::collections::{BTreeMap, HashMap};
use std::fmt::Write as _;
use std::fs;
use std::path::PathBuf;
use std::string::ToString;
use std::sync::{Arc, Mutex, RwLock};
use std::time::Instant;

use conjure_cp::ast::categories::{Category, CategoryOf};
use conjure_cp::ast::{Atom, DeclarationPtr, Expression, GroundDomain, Literal, Metadata, Name};
use conjure_cp::bug_assert;
use conjure_cp::context::Context;
use conjure_cp::settings::{configured_rule_trace_enabled, set_rule_trace_enabled};

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

use itertools::Itertools as _;
use tempfile::tempdir;

use crate::utils::json::sort_json_object;
use crate::utils::simplified_json::{
    domains_from_model, param_model_from_assignments, params_from_simplified_json_str,
    solutions_from_simplified_json_str,
};
use conjure_cp::Model;
use conjure_cp::instantiate::instantiate_model;
use conjure_cp::parse::tree_sitter::parse_essence_file_native;
use conjure_cp::representation::util::try_up;
use conjure_cp::solver::{SearchStatus, Solver};

use glob::glob;

use uniplate::Uniplate;

#[derive(Clone, Copy, Debug, Default)]
pub struct ConjureRunTimings {
    pub wall_clock_time_s: f64,
    pub translation_time_s: f64,
    pub conjure_translation_time_s: f64,
    pub savilerow_translation_time_s: f64,
    pub solve_time_s: f64,
}

#[derive(Debug)]
pub struct ConjureSolutions {
    pub solutions: Vec<BTreeMap<Name, Literal>>,
    pub timings: Option<ConjureRunTimings>,
}

/// Coerces a literal into the type expected by a reference domain when possible.
///
/// This is currently used to turn `0`/`1` solver outputs back into boolean
/// literals before substituting them into dominance expressions.
fn literal_for_reference_domain(
    reference_domain: Option<GroundDomain>,
    value: &Literal,
) -> Option<Literal> {
    if matches!(reference_domain, Some(GroundDomain::Bool)) {
        return match value {
            Literal::Bool(x) => Some(Literal::Bool(*x)),
            Literal::Int(1) => Some(Literal::Bool(true)),
            Literal::Int(0) => Some(Literal::Bool(false)),
            _ => None,
        };
    }

    Some(value.clone())
}

/// Replaces `fromSolution(x)` occurrences with the value of `x` from a previous solution.
fn substitute_from_solution(
    expr: &Expression,
    previous_solution: &BTreeMap<Name, Literal>,
) -> Option<Expression> {
    match expr {
        Expression::FromSolution(_, atom_expr) => {
            let Atom::Reference(reference) = atom_expr.as_ref() else {
                return Some(expr.clone());
            };

            let name = reference.name();
            let value = previous_solution.get(&name)?;
            let reference_domain = reference.resolved_domain().map(|x| x.as_ref().clone());
            let value = literal_for_reference_domain(reference_domain, value)?;
            Some(Expression::Atomic(Metadata::new(), Atom::Literal(value)))
        }
        _ => Some(expr.clone()),
    }
}

/// Replaces direct variable references with values from the candidate solution.
fn substitute_current_solution_refs(
    expr: &Expression,
    candidate_solution: &BTreeMap<Name, Literal>,
) -> Option<Expression> {
    match expr {
        Expression::Atomic(_, Atom::Reference(reference)) => {
            let name = reference.name();
            let value = candidate_solution.get(&name)?;
            let reference_domain = reference.resolved_domain().map(|x| x.as_ref().clone());
            let value = literal_for_reference_domain(reference_domain, value)?;
            Some(Expression::Atomic(Metadata::new(), Atom::Literal(value)))
        }
        _ => Some(expr.clone()),
    }
}

/// Evaluates whether `candidate_solution` dominates `previous_solution`.
///
/// The dominance expression is instantiated with values from both solutions and
/// then constant-folded to a boolean result.
fn does_solution_dominate(
    dominance_expression: &Expression,
    candidate_solution: &BTreeMap<Name, Literal>,
    previous_solution: &BTreeMap<Name, Literal>,
) -> bool {
    let expr = dominance_expression
        .rewrite(&|e| substitute_from_solution(&e, previous_solution))
        .rewrite(&|e| substitute_current_solution_refs(&e, candidate_solution));

    matches!(
        conjure_cp::ast::eval::eval_constant(&expr),
        Some(Literal::Bool(true))
    )
}

/// Removes solutions that are dominated by another solution in the result set.
fn retroactively_prune_dominated(
    solutions: Vec<BTreeMap<Name, Literal>>,
    dominance_expression: &Expression,
) -> Vec<BTreeMap<Name, Literal>> {
    solutions
        .iter()
        .enumerate()
        .filter_map(|(i, solution)| {
            let dominated = solutions.iter().enumerate().any(|(j, candidate)| {
                i != j && does_solution_dominate(dominance_expression, candidate, solution)
            });

            if dominated {
                None
            } else {
                Some(solution.clone())
            }
        })
        .collect()
}

fn validate_solution_collection_options(model: &Model, num_sols: i32) -> Result<(), anyhow::Error> {
    if model.objective.is_some() && num_sols != 1 {
        let got = if num_sols == 0 {
            "all".to_string()
        } else {
            num_sols.to_string()
        };
        return Err(anyhow::anyhow!(
            "optimisation problems require number-of-solutions=1 (got {got})"
        ));
    }
    Ok(())
}

/// Wall-clock phases of collecting solutions from a compiled model.
#[derive(Clone, Copy, Debug, Default)]
pub struct SolutionCollectionTimings {
    pub backend_time_s: f64,
    /// Time inside the solver call, including solution callbacks and solver-time rewrites.
    pub search_time_s: f64,
    pub solution_processing_time_s: f64,
}

/// Collect and reconstruct model solutions.
pub fn get_solutions(
    solver: Solver,
    model: Model,
    num_sols: i32,
    keep_intermediate_solutions: bool,
    solver_input_file: &Option<PathBuf>,
    rule_trace_cdp: bool,
) -> Result<Vec<BTreeMap<Name, Literal>>, anyhow::Error> {
    get_solutions_with_timings(
        solver,
        model,
        num_sols,
        keep_intermediate_solutions,
        solver_input_file,
        rule_trace_cdp,
    )
    .map(|(solutions, _)| solutions)
}

/// Collect solutions together with measured backend, search and reconstruction times.
pub fn get_solutions_with_timings(
    solver: Solver,
    model: Model,
    num_sols: i32,
    keep_intermediate_solutions: bool,
    solver_input_file: &Option<PathBuf>,
    rule_trace_cdp: bool,
) -> Result<(Vec<BTreeMap<Name, Literal>>, SolutionCollectionTimings), anyhow::Error> {
    set_rule_trace_enabled(rule_trace_cdp && configured_rule_trace_enabled());

    validate_solution_collection_options(&model, num_sols)?;

    let is_optimisation = model.objective.is_some();

    let dominance_expression = model.dominance.as_ref().map(|expr| match expr {
        Expression::DominanceRelation(_, inner) => inner.as_ref().clone(),
        _ => expr.clone(),
    });

    let adaptor_name = solver.get_name();

    tracing::info!(target: "conjure::stage", adaptor = adaptor_name, "building solver model");

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

    let backend_started_at = Instant::now();
    let solver = solver.load_model(model)?;
    let backend_time_s = backend_started_at.elapsed().as_secs_f64();

    if let Some(solver_input_file) = solver_input_file {
        tracing::info!(target: "conjure::stage",
            "Writing solver input file to {}",
            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>))?;
    }

    tracing::info!(target: "conjure::stage", adaptor = adaptor_name, "running solver");

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

    let search_started_at = Instant::now();
    let solver = if is_optimisation {
        solver
            .solve(Box::new(move |sols| {
                let mut all_solutions = (*all_solutions_ref_2).lock().unwrap();
                let solution = sols.into_iter().collect();
                if keep_intermediate_solutions {
                    all_solutions.push(solution);
                } else {
                    all_solutions.clear();
                    all_solutions.push(solution);
                }
                true
            }))
            .map_err(|err| anyhow::anyhow!("solver failed while collecting solutions: {err}"))?
    } else if num_sols > 0 {
        // Get num_sols solutions
        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
            }))
            .map_err(|err| anyhow::anyhow!("solver failed while collecting solutions: {err}"))?
    } else {
        // Get all solutions
        solver
            .solve(Box::new(move |sols| {
                let mut all_solutions = (*all_solutions_ref_2).lock().unwrap();
                all_solutions.push(sols.into_iter().collect());
                true
            }))
            .map_err(|err| anyhow::anyhow!("solver failed while collecting solutions: {err}"))?
    };

    let search_time_s = search_started_at.elapsed().as_secs_f64();
    let processing_started_at = Instant::now();
    let search_status = solver.search_status();
    solver.save_stats_to_context();

    // Get the collections of solutions and model symbols
    #[allow(clippy::unwrap_used)]
    let mut sols_guard = (*all_solutions_ref).lock().unwrap();
    let sols = &mut *sols_guard;

    // Stopping after a requested finite number of satisfaction solutions is intentional. Every
    // other incomplete search -- notably a solver timeout or interrupt while proving UNSAT -- must
    // not be accepted as a complete (possibly empty) solution set.
    let requested_limit_reached = !is_optimisation
        && num_sols > 0
        && sols.len() >= usize::try_from(num_sols).unwrap_or(usize::MAX);
    if let SearchStatus::Incomplete(reason) = search_status
        && !requested_limit_reached
    {
        return Err(anyhow::anyhow!("solver search incomplete: {reason:?}"));
    }

    let symbols = symbols_ptr.read();

    // Get the representations for each variable by name, since some variables are
    // divided into multiple auxiliary variables(see crate::representation::Representation)
    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;
            }
            bug_assert!(
                reprs.len() <= 1,
                "multiple representations for a variable is not yet implemented"
            );

            assert_eq!(
                reprs[0].len(),
                1,
                "nested representations are not yet implemented"
            );
            Some((name, reprs[0][0].clone()))
        })
        .collect_vec();

    let structured_declarations: Vec<DeclarationPtr> = symbols
        .iter_local()
        .filter(|(name, declaration)| {
            // `category_of` follows a value letting into its body, and from there into every
            // letting that body names. Those declarations have no representations, so skip them
            // before walking the chain.
            matches!(name, Name::User(_))
                && !declaration.reprs().is_empty()
                && declaration.category_of() >= Category::Decision
        })
        .map(|(_, declaration)| declaration.clone())
        .collect();

    for sol in sols.iter_mut() {
        // Get the value of complex variables using their auxiliary variables
        for (name, representation) in representations.iter() {
            if sol.contains_key(name) {
                continue;
            }

            let value = representation.value_up(sol).map_err(|err| {
                anyhow::anyhow!(
                    "failed to reconstruct value for variable {name} from solver solution: {err}"
                )
            })?;
            sol.insert(name.clone(), value);
        }

        let raw_assignment: HashMap<Name, Literal> = sol.clone().into_iter().collect();
        for declaration in &structured_declarations {
            let value = try_up(declaration.clone(), &raw_assignment).map_err(|err| {
                anyhow::anyhow!(
                    "failed to reconstruct value for variable {}: {err}",
                    declaration.name()
                )
            })?;
            sol.insert(declaration.name().clone(), value);
        }

        // Remove auxiliary variables since we've found the value of the
        // variable they represent
        *sol = sol
            .clone()
            .into_iter()
            .filter(|(name, _)| {
                !matches!(name, Name::Represented(_)) && !matches!(name, Name::Machine(_))
            })
            .collect();
    }

    sols.retain(|x| !x.is_empty());
    if let Some(dominance_expression) = dominance_expression.as_ref() {
        let pre_prune_len = sols.len();
        let pruned = retroactively_prune_dominated(sols.clone(), dominance_expression);
        let post_prune_len = pruned.len();

        tracing::info!(
            target: "conjure::stage",
            retained = post_prune_len,
            considered = pre_prune_len,
            "pruned dominated solutions"
        );

        *sols = pruned;
    }

    let solutions = sols.clone();
    Ok((
        solutions,
        SolutionCollectionTimings {
            backend_time_s,
            search_time_s,
            solution_processing_time_s: processing_started_at.elapsed().as_secs_f64(),
        },
    ))
}

#[derive(Clone, Debug, Default)]
pub struct ConjureSolveCaptureOptions {
    /// When set, `conjure solve -o` writes models and Minion files here instead of a temp dir.
    pub artifact_dir: Option<PathBuf>,
    /// Passed to `conjure solve --savilerow-options` (e.g. `-O0`).
    pub savilerow_options: Option<String>,
}

#[allow(clippy::unwrap_used)]
pub fn get_solutions_from_conjure(
    essence_file: &str,
    param_file: Option<&str>,
    context: Arc<RwLock<Context<'static>>>,
) -> Result<Vec<BTreeMap<Name, Literal>>, anyhow::Error> {
    Ok(get_solutions_from_conjure_with_stats(
        essence_file,
        param_file,
        context,
        0,
        ConjureSolveCaptureOptions::default(),
    )?
    .solutions)
}

#[allow(clippy::unwrap_used)]
pub fn get_solutions_from_conjure_with_stats(
    essence_file: &str,
    param_file: Option<&str>,
    context: Arc<RwLock<Context<'static>>>,
    number_of_solutions: i32,
    capture_options: ConjureSolveCaptureOptions,
) -> Result<ConjureSolutions, anyhow::Error> {
    enum ConjureOutputDir {
        Temp(tempfile::TempDir),
        Fixed(PathBuf),
    }

    impl ConjureOutputDir {
        fn path(&self) -> &std::path::Path {
            match self {
                Self::Temp(dir) => dir.path(),
                Self::Fixed(path) => path,
            }
        }
    }

    let output_dir = match &capture_options.artifact_dir {
        Some(path) => {
            // A failed run leaves its diagnostics behind. Conjure may reuse files in an existing
            // output directory, and the glob below would also read stale solution files, so each
            // invocation must start with an empty artifact directory.
            if path.exists() {
                fs::remove_dir_all(path)?;
            }
            fs::create_dir_all(path)?;
            ConjureOutputDir::Fixed(path.clone())
        }
        None => ConjureOutputDir::Temp(tempdir()?),
    };

    let mut cmd = std::process::Command::new("conjure");
    let number_of_solutions_arg = if number_of_solutions == 0 {
        "all".to_string()
    } else {
        number_of_solutions.to_string()
    };

    cmd.arg("solve")
        .arg(format!("--number-of-solutions={number_of_solutions_arg}"))
        .arg("--copy-solutions=no")
        .arg("--solutions-in-one-file")
        .arg("--output-format=json")
        .arg("-o")
        .arg(output_dir.path());

    if let Some(options) = &capture_options.savilerow_options {
        cmd.arg(format!("--savilerow-options={options}"));
    }

    cmd.arg(essence_file);

    if let Some(file) = param_file {
        cmd.arg(file);
    }

    let conjure_solve_start = Instant::now();
    let output = cmd.output()?;
    let conjure_solve_wall_time_s = conjure_solve_start.elapsed().as_secs_f64();

    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 domains = domains_for_conjure_solutions(essence_file, param_file, Arc::clone(&context))?;

    let solutions_files: Vec<_> =
        glob(&format!("{}/*.solutions.json", output_dir.path().display()))?.collect();
    if solutions_files.is_empty() {
        // Unsatisfiable / no solutions: Conjure may omit the solutions file.
        let timings = read_conjure_timings(output_dir.path(), conjure_solve_wall_time_s)?;
        return Ok(ConjureSolutions {
            solutions: Vec::new(),
            timings,
        });
    }

    let mut solutions_set = Vec::new();
    for solutions_file in solutions_files {
        let solutions_file = solutions_file?;
        let text = fs::read_to_string(&solutions_file)?;
        solutions_set.extend(solutions_from_simplified_json_str(&text, &domains)?);
    }

    let timings = read_conjure_timings(output_dir.path(), conjure_solve_wall_time_s)?;

    Ok(ConjureSolutions {
        solutions: solutions_set
            .into_iter()
            .filter(|x| !x.is_empty())
            .collect(),
        timings,
    })
}

fn domains_for_conjure_solutions(
    essence_file: &str,
    param_file: Option<&str>,
    context: Arc<RwLock<Context<'static>>>,
) -> Result<BTreeMap<Name, conjure_cp::ast::DomainPtr>, anyhow::Error> {
    let problem = parse_essence_file_native(essence_file, Arc::clone(&context))?;
    let unified = match param_file {
        Some(param_path) if param_path.ends_with(".json") => {
            let given_domains = domains_from_model(&problem);
            let params =
                params_from_simplified_json_str(&fs::read_to_string(param_path)?, &given_domains)?;
            let param_model =
                param_model_from_assignments(params, &given_domains, Arc::clone(&context));
            instantiate_model(problem, param_model)?
        }
        Some(param_path) => {
            let param_model = parse_essence_file_native(param_path, Arc::clone(&context))?;
            instantiate_model(problem, param_model)?
        }
        None => problem,
    };
    Ok(domains_from_model(&unified))
}

fn read_conjure_timings(
    path: &std::path::Path,
    conjure_solve_wall_time_s: f64,
) -> Result<Option<ConjureRunTimings>, anyhow::Error> {
    let stats_files: Vec<_> = glob(&format!("{}/*.stats.json", path.display()))?.collect();
    if stats_files.is_empty() {
        return Ok(None);
    }

    let mut timings = ConjureRunTimings {
        wall_clock_time_s: conjure_solve_wall_time_s,
        ..Default::default()
    };
    for stats_file in stats_files {
        let stats_file = stats_file?;
        let stats: JsonValue = serde_json::from_str(&fs::read_to_string(&stats_file)?)?;
        let savilerow_total_time = stats
            .pointer("/savilerowInfo/SavileRowTotalTime")
            .and_then(JsonValue::as_str)
            .and_then(|value| value.parse::<f64>().ok())
            .unwrap_or_default();
        let solve_time = stats
            .pointer("/savilerowInfo/SolverTotalTime")
            .and_then(JsonValue::as_str)
            .and_then(|value| value.parse::<f64>().ok())
            .or_else(|| {
                stats
                    .pointer("/savilerowInfo/SolverSolveTime")
                    .and_then(JsonValue::as_str)
                    .and_then(|value| value.parse::<f64>().ok())
            })
            .unwrap_or_default();

        timings.savilerow_translation_time_s += savilerow_total_time;
        timings.solve_time_s += solve_time;
    }

    timings.conjure_translation_time_s =
        (conjure_solve_wall_time_s - timings.savilerow_translation_time_s - timings.solve_time_s)
            .max(0.0);
    timings.translation_time_s =
        timings.conjure_translation_time_s + timings.savilerow_translation_time_s;

    Ok(Some(timings))
}

pub fn solutions_to_json(solutions: &[BTreeMap<Name, Literal>]) -> JsonValue {
    let json_solutions = solutions.iter().map(solution_to_json).collect();
    let ans = JsonValue::Array(json_solutions);
    sort_json_object(&ans, true)
}

/// Render solutions in the format produced by Conjure's `--solutions-in-one-file` option.
pub fn solutions_to_essence(solutions: &[BTreeMap<Name, Literal>]) -> String {
    let mut solutions = solutions.iter().collect::<Vec<_>>();
    solutions.sort_by(|lhs, rhs| solution_essence_cmp(lhs, rhs));

    let mut output = String::new();
    for (index, solution) in solutions.iter().enumerate() {
        writeln!(output, "$ Solution: {:06}", index + 1).unwrap();
        writeln!(output, "language Essence 1.3\n").unwrap();
        let mut unnamed_types = BTreeMap::new();
        for value in solution.values() {
            for literal in value.universe() {
                if let Literal::Unnamed(value) = literal {
                    unnamed_types.insert(value.ty.name.clone(), value.ty.size);
                }
            }
        }
        for (name, size) in unnamed_types {
            let members = (1..=size).map(|index| format!("{name}_{index}")).join(", ");
            writeln!(output, "letting {name} be new type enum {{{members}}}").unwrap();
        }
        for (name, value) in *solution {
            writeln!(output, "letting {name} be {value}").unwrap();
        }
        output.push_str("\n\n");
    }
    output
}

fn solution_essence_cmp(
    lhs: &BTreeMap<Name, Literal>,
    rhs: &BTreeMap<Name, Literal>,
) -> std::cmp::Ordering {
    lhs.iter()
        .zip(rhs)
        .find_map(|((lhs_name, lhs_value), (rhs_name, rhs_value))| {
            let ordering = lhs_name.cmp(rhs_name);
            (ordering != std::cmp::Ordering::Equal)
                .then_some(ordering)
                .or_else(|| {
                    let ordering = lhs_value.essence_cmp(rhs_value);
                    (ordering != std::cmp::Ordering::Equal).then_some(ordering)
                })
        })
        .unwrap_or_else(|| lhs.len().cmp(&rhs.len()))
}

fn solution_to_json(solution: &BTreeMap<Name, Literal>) -> JsonValue {
    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);
    }
    sort_json_object(&JsonValue::Object(json_solution), false)
}

#[cfg(test)]
mod tests {
    use super::*;
    use conjure_cp::ast::{DeclarationPtr, Domain, Moo, Reference};

    #[test]
    fn renders_conjure_multi_solution_essence_format() {
        let mut first = BTreeMap::new();
        first.insert(Name::User("b".into()), Literal::Bool(false));
        first.insert(Name::User("x".into()), Literal::Int(1));
        let mut second = BTreeMap::new();
        second.insert(Name::User("b".into()), Literal::Bool(true));
        second.insert(Name::User("x".into()), Literal::Int(2));

        assert_eq!(
            solutions_to_essence(&[first, second]),
            concat!(
                "$ Solution: 000001\n",
                "language Essence 1.3\n\n",
                "letting b be false\n",
                "letting x be 1\n\n\n",
                "$ Solution: 000002\n",
                "language Essence 1.3\n\n",
                "letting b be true\n",
                "letting x be 2\n\n\n",
            )
        );
    }

    #[test]
    fn retroactive_pruning_removes_dominated_prior_solution() {
        let x = Name::User("x".into());
        let x_ref = Expression::Atomic(
            Metadata::new(),
            Atom::Reference(Reference::new(DeclarationPtr::new_find(
                x.clone(),
                Domain::bool(),
            ))),
        );
        let dominance_expression = Expression::Imply(
            Metadata::new(),
            Moo::new(x_ref),
            Moo::new(Expression::FromSolution(
                Metadata::new(),
                Moo::new(Atom::Reference(Reference::new(DeclarationPtr::new_find(
                    x.clone(),
                    Domain::bool(),
                )))),
            )),
        );

        let mut sol_true = BTreeMap::new();
        sol_true.insert(x.clone(), Literal::Int(1));
        let mut sol_false = BTreeMap::new();
        sol_false.insert(x, Literal::Int(0));

        let pruned =
            retroactively_prune_dominated(vec![sol_true, sol_false.clone()], &dominance_expression);

        assert_eq!(pruned, vec![sol_false]);
    }
}