pub fn instantiate_model(problem_model: Model, param_model: Model) -> anyhow::Result<Model> {

    let symbol_table = problem_model.symbols_ptr_unchecked().write();

    let param_table = param_model.symbols_ptr_unchecked().write();

    let mut pending_givens = symbol_table

        .iter_local()

        .filter_map(|(name, decl)| decl.as_given().map(|_| name.clone()))

        .collect::<Vec<_>>();

    while !pending_givens.is_empty() {

        let mut next_pending = Vec::new();

        let mut made_progress = false;

        for name in pending_givens {

            let mut decl = symbol_table

                .lookup_local(&name)

                .ok_or_else(|| anyhow!("Given declaration `{name}` not found in problem model"))?;

            let Some(domain) = decl.as_given() else {

            let param_decl = param_table.lookup(&name);

            let expr = param_decl

                .as_ref()

                .and_then(DeclarationPtr::as_value_letting)

                .ok_or_else(|| {

                    anyhow!(

                })?;

            let expr_value = eval_constant(&expr)

                .ok_or_else(|| anyhow!("Letting expression `{expr}` cannot be evaluated"))?;

            let Ok(ground_domain) = domain.resolve() else {

            if !ground_domain.contains(&expr_value)? {

                return Err(anyhow!(

                    "Domain of given statement `{name}` does not contain letting value"

                ));

            }

            let new_decl = Declaration::new(

                name.clone(),

                DeclarationKind::ValueLetting(expr.clone(), Some(domain.clone())),

            drop(domain);

            decl.replace(new_decl);

            made_progress = true;

            tracing::info!("Replaced {name} given with letting.");

        if next_pending.is_empty() {

            break;

    drop(symbol_table);

    Ok(problem_model)

}