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 detach_symbols(model: &mut Model) {

    let detached = model.symbols_ptr_unchecked_mut().detach();

    *model.symbols_ptr_unchecked_mut() = detached;

}

pub(super) fn rewrite_model_with_configured_rewriter<'a>(

    model: Model,

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

    configured_rewriter: Rewriter,

) -> Model {

    with_solver_family(SolverFamily::Minion, || {

        with_compact_heuristic(|| {

            rewrite_model_with_configured_rewriter_core(model, rule_sets, configured_rewriter)

                .unwrap()

        })

    })

}

pub(super) fn split_symbolic_guards(

    comprehension: &Comprehension,

) -> (Comprehension, Vec<Expression>) {

    let mut symbolic_guards = vec![];

    let mut qualifiers = vec![];

    for qualifier in &comprehension.qualifiers {

        match qualifier {

            qualifier => qualifiers.push(qualifier.clone()),

    let mut stripped = comprehension.clone();

    stripped.qualifiers = qualifiers;

    (stripped, symbolic_guards)

}

pub(super) fn min_max_skip_value(

    return_expression: &Expression,

    want_max: bool,

) -> Result<Literal, SolverError> {

    let ranges = return_expression

        .domain_of()

        .and_then(|domain| domain.as_ground().cloned())

        .and_then(|ground| match ground {

            GroundDomain::Int(ranges, _) => Some(ranges),

        })

        .ok_or_else(not_supported)?;

    let spanning = Range::spanning(&ranges);

    let bound = if want_max {

        spanning.high()

        spanning.low()

    Ok(Literal::Int(*bound.ok_or_else(not_supported)?))

}

pub(super) fn instantiate_return_expressions_from_values(

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

    return_expression_model: &Model,

    quantified_vars: &[Name],

    symbolic_guards: &[Expression],

    skip_operator: Option<ACOperatorKind>,

) -> Result<Vec<Expression>, SolverError> {

    let mut return_expressions = vec![];

    let min_max_skip_value = match skip_operator {

        _ => None,

    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))

        let mut binding_targets = Vec::with_capacity(symbolic_guards.len() + 1);

        binding_targets.push(return_expression.clone());

        binding_targets.extend(symbolic_guards.iter().cloned());

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

        let Some(guards) = instantiate_symbolic_guards(symbolic_guards)? else {

        return_expression = concretise_resolved_reference_atoms(return_expression);

        return_expression = expand_nested_comprehensions(return_expression)?;

        let Some(mut return_expression) = strip_guarded_safe_index_conditions(return_expression)

        return_expression = simplify_expression(return_expression);

        for guard in guards {

        return_expressions.push(return_expression);

    Ok(return_expressions)

}

fn expand_nested_comprehensions(expr: Expression) -> Result<Expression, SolverError> {

    let children = expr

        .children()

        .into_iter()

        .map(expand_nested_comprehensions)

        .collect::<Result<_, _>>()?;

    let expr = expr.with_children(children);

    let Expression::Comprehension(_, comprehension) = &expr else {

        return Ok(expr);

    let comprehension = comprehension.as_ref().clone();

    let has_expression_generator = comprehension.qualifiers.iter().any(|qualifier| {

        matches!(

            qualifier,

    });

    let (_, symbolic_guards) = split_symbolic_guards(&comprehension);

    if has_expression_generator

        || (comprehension.skip_operator.is_none() && !symbolic_guards.is_empty())

    }

    Ok(into_matrix_expr!(expand_via_solver(comprehension)?))

}

fn instantiate_symbolic_guards(

    symbolic_guards: &[Expression],

) -> Result<Option<Vec<Expression>>, SolverError> {

    let mut remaining = vec![];

    for guard in symbolic_guards {

    Ok(Some(remaining))

}

pub(super) fn retain_quantified_solution_values(

    values: HashMap<Name, Literal>,

    quantified_vars: &[Name],

    symbols: &SymbolTable,

) -> HashMap<Name, Literal> {

    let mut quantified_values = HashMap::new();

    for name in quantified_vars {

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

        let Ok(value) = try_up(decl, &values) else {

        quantified_values.insert(name.clone(), value);

    quantified_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 Some(lowered) = try_lower_const_unsafe_index_matrix_components(&subexpr) {

                return lowered;

            }

            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);

    }

        conjuncts.into_iter().partition(is_indomain_guard);

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

        return Some(expr);

}

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().into_list()

        for child in children {

            collect_top_level_and_terms(child, out);

        out.push(expr);

}

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

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

}

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.iter_local() {

        if matches!(

            &decl.kind() as &DeclarationKind,

        }

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

            continue;

        }

        let id = decl.id();

        let new_decl = parent_symtab.gen_find_auxiliary(&decl.domain().unwrap());

        machine_name_translations.insert(id, new_decl);

    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,

    exprs: &[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 exprs

        .iter()

        .flat_map(uniplate::Biplate::<DeclarationPtr>::universe_bi)

        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, reprs) in self.originals.drain(..) {

            let _ = decl.replace_kind(kind);

            *decl.reprs_mut() = reprs;

    }

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 old_reprs = decl.reprs().clone();

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

        let _ = decl.replace_kind(new_kind);

        originals.push((decl, old_kind, old_reprs));

    TempQuantifiedFindGuard { originals }

}