Lines
85.15 %
Functions
50.97 %
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(
candidate_solution: &BTreeMap<Name, Literal>,
Expression::Atomic(_, Atom::Reference(reference)) => {
let value = candidate_solution.get(&name)?;
/// 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,
) -> 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>>,
) -> 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()
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.
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(
) -> 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);
all_solutions.clear();
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);
all_solutions.push(sols.into_iter().collect());
let mut sols_left = sols_left.lock().unwrap();
*sols_left -= 1;
*sols_left != 0
// Get all solutions
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| {
"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()
.filter(|(name, _)| {
!matches!(name, Name::Represented(_)) && !matches!(name, Name::Machine(_))
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>,
pub fn get_solutions_from_conjure(
essence_file: &str,
param_file: Option<&str>,
context: Arc<RwLock<Context<'static>>>,
Ok(get_solutions_from_conjure_with_stats(
essence_file,
param_file,
context,
0,
ConjureSolveCaptureOptions::default(),
)?
.solutions)
pub fn get_solutions_from_conjure_with_stats(
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 {
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)?);
Ok(ConjureSolutions {
solutions: solutions_set
.filter(|x| !x.is_empty())
.collect(),
fn domains_for_conjure_solutions(
) -> 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))?;
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")
.or_else(|| {
stats
.pointer("/savilerowInfo/SolverSolveTime")
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)
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));
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",
"letting b be true\n",
"letting x be 2\n\n\n",
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(
Moo::new(x_ref),
Moo::new(Expression::FromSolution(
Moo::new(Atom::Reference(Reference::new(DeclarationPtr::new_find(
)))),
)),
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]);