Skip to main content

conjure_cp_core/
instantiate.rs

1use crate::{
2    Model,
3    ast::{DeclarationKind, DeclarationPtr, declaration::Declaration, eval_constant},
4};
5use anyhow::anyhow;
6
7/// Instantiate a problem model with values from a parameter model.
8///
9/// For each `given` declaration in `problem_model`, this looks for a corresponding value `letting`
10/// in `param_model`, checks it is a constant and within the given domain, and replaces the `given`
11/// with a value-letting in the returned model.
12pub fn instantiate_model(problem_model: Model, param_model: Model) -> anyhow::Result<Model> {
13    let symbol_table = problem_model.symbols_ptr_unchecked().write();
14    let param_table = param_model.symbols_ptr_unchecked().write();
15    let mut pending_givens = symbol_table
16        .iter_local()
17        .filter_map(|(name, decl)| decl.as_given().map(|_| name.clone()))
18        .collect::<Vec<_>>();
19
20    while !pending_givens.is_empty() {
21        let mut next_pending = Vec::new();
22        let mut made_progress = false;
23
24        for name in pending_givens {
25            let mut decl = symbol_table
26                .lookup_local(&name)
27                .ok_or_else(|| anyhow!("Given declaration `{name}` not found in problem model"))?;
28
29            let Some(domain) = decl.as_given() else {
30                continue;
31            };
32
33            let param_decl = param_table.lookup(&name);
34            let expr = param_decl
35                .as_ref()
36                .and_then(DeclarationPtr::as_value_letting)
37                .ok_or_else(|| {
38                    anyhow!(
39                        "Given declaration `{name}` does not have corresponding letting in parameter file"
40                    )
41                })?;
42
43            let expr_value = eval_constant(&expr)
44                .ok_or_else(|| anyhow!("Letting expression `{expr}` cannot be evaluated"))?;
45
46            let Some(ground_domain) = domain.resolve() else {
47                next_pending.push(name);
48                continue;
49            };
50
51            if !ground_domain.contains(&expr_value).unwrap() {
52                return Err(anyhow!(
53                    "Domain of given statement `{name}` does not contain letting value"
54                ));
55            }
56
57            let new_decl = Declaration::new(
58                name.clone(),
59                DeclarationKind::ValueLetting(expr.clone(), Some(domain.clone())),
60            );
61            drop(domain);
62            decl.replace(new_decl);
63            made_progress = true;
64
65            tracing::info!("Replaced {name} given with letting.");
66        }
67
68        if next_pending.is_empty() {
69            break;
70        }
71
72        if !made_progress {
73            return Err(anyhow!(
74                "Domain of given statement `{}` cannot be resolved",
75                next_pending[0]
76            ));
77        }
78
79        pending_givens = next_pending;
80    }
81
82    drop(symbol_table);
83    Ok(problem_model)
84}