pub(super) fn with_temporary_model(model: Model, search_order: Option<Vec<Name>>) -> Model {

    let mut model = model;

    model.context = Arc::new(RwLock::new(Context::default()));

    model.search_order = search_order;

    model

}

pub(super) fn rewrite_model_with_configured_rewriter<'a>(

    model: Model,

    rule_sets: &Vec<&'a RuleSet<'a>>,

    configured_rewriter: Rewriter,

) -> Model {

    rewrite_model_with_configured_rewriter_core(model, rule_sets, configured_rewriter).unwrap()

}

pub(super) fn instantiate_return_expressions_from_values(

    values: Vec<HashMap<Name, Literal>>,

    return_expression_model: &Model,

    quantified_vars: &[Name],

) -> Vec<Expression> {

    let mut return_expressions = vec![];

    for value in values {

        let return_expression_model = return_expression_model.clone();

        let child_symtab = return_expression_model.symbols().clone();

        let mut return_expression = return_expression_model.into_single_expression();

        let value: HashMap<_, _> = value

            .into_iter()

            .filter(|(name, _)| quantified_vars.contains(name))

            .collect();

        let _temp_value_bindings =

            temporarily_bind_quantified_vars_to_values(&child_symtab, &return_expression, &value);

        return_expression = concretise_resolved_reference_atoms(return_expression);

        let Some(mut return_expression) = strip_guarded_safe_index_conditions(return_expression)

        return_expression = simplify_expression(return_expression);

        return_expressions.push(return_expression);

    return_expressions

}

pub(super) fn retain_quantified_solution_values(

    mut values: HashMap<Name, Literal>,

    quantified_vars: &[Name],

) -> HashMap<Name, Literal> {

    values.retain(|name, _| quantified_vars.contains(name));

    values

}

pub(super) fn simplify_expression(mut expr: Expression) -> Expression {

    for _ in 0..128 {

        let next = expr.clone().transform_bi(&|subexpr: Expression| {

            if let Some(lit) = eval_constant(&subexpr) {

                return Expression::Atomic(Metadata::new(), Atom::Literal(lit));

            }

            if let Ok(reduction) = run_partial_evaluator(&subexpr) {

                return reduction.new_expression;

            }

            subexpr

        });

        if next == expr {

            break;

        }

        expr = next;

    expr

}

pub(super) fn strip_guarded_safe_index_conditions(expr: Expression) -> Option<Expression> {

    let mut conjuncts = Vec::new();

    collect_top_level_and_terms(expr.clone(), &mut conjuncts);

    if conjuncts.len() == 1 && conjuncts[0] == expr {

        return Some(expr);

    }

    let (guards, mut non_guards): (Vec<_>, Vec<_>) =

        conjuncts.into_iter().partition(is_indomain_guard);

    if guards.is_empty() || non_guards.len() != 1 {

        return Some(expr);

    }

    let guarded_term = non_guards.pop().expect("length checked above");

    if !guards

        .iter()

        .all(|guard| guard_targets_safe_index_index(guard, &guarded_term))

    }

    for guard in &guards {

        let simplified_guard = simplify_expression(guard.clone());

        match eval_constant(&simplified_guard) {

            Some(Literal::Bool(true)) => {}

            Some(Literal::Bool(false)) => return None,

    Some(guarded_term)

}

fn collect_top_level_and_terms(expr: Expression, out: &mut Vec<Expression>) {

    if let Expression::And(_, ref children) = expr

        && let Some(children) = children.as_ref().clone().unwrap_list()

        for child in children {

            collect_top_level_and_terms(child, out);

        }

    } else {

        out.push(expr);

    }

}

fn is_indomain_guard(expr: &Expression) -> bool {

    matches!(expr, Expression::InDomain(_, _, _))

}

fn guard_targets_safe_index_index(guard: &Expression, expr: &Expression) -> bool {

    let Expression::InDomain(_, guarded_index, _) = guard else {

    expr.universe().into_iter().any(|subexpr| {

        let Expression::SafeIndex(_, _, indices) = subexpr else {

        indices.iter().any(|index| index == guarded_index.as_ref())

    })

}

fn concretise_resolved_reference_atoms(expr: Expression) -> Expression {

    expr.transform_bi(&|atom: Atom| match atom {

        Atom::Reference(reference) => reference

            .resolve_constant()

            .map_or_else(|| Atom::Reference(reference), Atom::Literal),

        other => other,

    })

}

pub(super) fn lift_machine_references_into_parent_scope(

    expr: Expression,

    child_symtab: &SymbolTable,

    parent_symtab: &mut SymbolTable,

) -> Expression {

    let mut machine_name_translations: HashMap<ObjId, DeclarationPtr> = HashMap::new();

    for (name, decl) in child_symtab.clone().into_iter_local() {

        if matches!(

            &decl.kind() as &DeclarationKind,

        }

        if !matches!(&name, Name::Machine(_)) {

            continue;

    expr.transform_bi(&|atom: Atom| {

        if let Atom::Reference(ref decl) = atom

            && let id = decl.id()

            && let Some(new_decl) = machine_name_translations.get(&id)

            atom

    })

}

    fn drop(&mut self) {

        for (mut decl, kind) in self.originals.drain(..) {

            let _ = decl.replace_kind(kind);

        }

    }

fn maybe_bind_temp_value_letting(

    originals: &mut Vec<(DeclarationPtr, DeclarationKind)>,

    decl: &DeclarationPtr,

    lit: &Literal,

) {

    if originals

        .iter()

        .any(|(existing, _)| existing.id() == decl.id())

        return;

    }

    let mut decl = decl.clone();

    let old_kind = decl.kind().clone();

    let temp_kind = DeclarationKind::TemporaryValueLetting(Expression::Atomic(

        Metadata::new(),

        Atom::Literal(lit.clone()),

    ));

    let _ = decl.replace_kind(temp_kind);

    originals.push((decl, old_kind));

}

fn temporarily_bind_quantified_vars_to_values(

    symbols: &SymbolTable,

    expr: &Expression,

    values: &HashMap<Name, Literal>,

) -> TempQuantifiedValueLettingGuard {

    let mut originals = Vec::new();

    for (name, lit) in values {

        let Some(decl) = symbols.lookup_local(name) else {

        maybe_bind_temp_value_letting(&mut originals, &decl, lit);

        let kind = decl.kind();

        if let DeclarationKind::Quantified(inner) = &*kind

        }

    for decl in uniplate::Biplate::<DeclarationPtr>::universe_bi(expr) {

        let name = decl.name().clone();

        let Some(lit) = values.get(&name) else {

            continue;

        maybe_bind_temp_value_letting(&mut originals, &decl, lit);

        let kind = decl.kind();

        if let DeclarationKind::Quantified(inner) = &*kind

        }

    TempQuantifiedValueLettingGuard { originals }

}

    fn drop(&mut self) {

        for (mut decl, kind) in self.originals.drain(..) {

            let _ = decl.replace_kind(kind);

        }

    }

pub(super) fn temporarily_materialise_quantified_vars_as_finds(

    model: &Model,

    quantified_vars: &[Name],

) -> TempQuantifiedFindGuard {

    let symbols = model.symbols().clone();

    let mut originals = Vec::new();

    for name in quantified_vars {

        let Some(mut decl) = symbols.lookup_local(name) else {

        let old_kind = decl.kind().clone();

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

        let new_kind = DeclarationKind::Find(DecisionVariable::new(domain));

        let _ = decl.replace_kind(new_kind);

        originals.push((decl, old_kind));

    TempQuantifiedFindGuard { originals }

}