fn selected_comprehension_expander(comprehension: &Comprehension) -> QuantifiedExpander {

    match comprehension_expander() {

        QuantifiedExpander::Auto => auto_comprehension_expander(comprehension),

        explicit => explicit,

}

fn auto_comprehension_expander(comprehension: &Comprehension) -> QuantifiedExpander {

    let Some(candidate_assignments) = estimated_candidate_assignments(comprehension) else {

        if has_dependent_generators_and_nested_return(comprehension) {

            return QuantifiedExpander::ViaSolverAc;

        }

        return QuantifiedExpander::Native;

    if candidate_assignments < AUTO_SOLVER_THRESHOLD {

        return QuantifiedExpander::Native;

    }

    let useful_guard = has_useful_quantified_guard(comprehension);

    let useful_ac_pruning = match comprehension.skip_operator {

        ) => has_cheap_ac_return_pruning(comprehension),

    if useful_guard || useful_ac_pruning {

        QuantifiedExpander::ViaSolverAc

        QuantifiedExpander::Native

}

fn estimated_candidate_assignments(comprehension: &Comprehension) -> Option<u64> {

    let mut assignments = 1u64;

    for qualifier in &comprehension.qualifiers {

        match qualifier {

                let domain = ptr.domain()?;

                let length = domain.resolve().ok()?.length().ok()?;

                assignments = assignments.saturating_mul(length);

            ComprehensionQualifier::Condition(_) => {}

    Some(assignments)

}

fn has_dependent_generators_and_nested_return(comprehension: &Comprehension) -> bool {

    if !matches!(

        comprehension.skip_operator,

        Some(

            ACOperatorKind::And

                | ACOperatorKind::Or

                | ACOperatorKind::Sum

                | ACOperatorKind::Product

        )

    ) {

    }

    let mut generator_count = 0;

    for qualifier in &comprehension.qualifiers {

        match qualifier {

            ComprehensionQualifier::Generator { ptr } if ptr.domain().is_some() => {

                generator_count += 1;

    generator_count >= 2

        && comprehension

            .return_expression

            .any_expression(|expression| matches!(expression, Expr::Comprehension(_, _)))

}

fn has_useful_quantified_guard(comprehension: &Comprehension) -> bool {

    let quantified_vars: BTreeSet<_> = comprehension.quantified_vars().into_iter().collect();

    comprehension.qualifiers.iter().any(|qualifier| {

        let ComprehensionQualifier::Condition(condition) = qualifier else {

            return false;

        comprehension.is_quantified_guard(condition)

            && Biplate::<Name>::universe_bi(condition)

                .iter()

                .any(|name| quantified_vars.contains(name))

    })

}

fn has_cheap_ac_return_pruning(comprehension: &Comprehension) -> bool {

    let quantified_vars: BTreeSet<_> = comprehension.quantified_vars().into_iter().collect();

    let return_expression = &comprehension.return_expression;

    if !comprehension_has_non_quantified_guards(comprehension)

        && expression_depends_only_on_quantified_decisions(

            comprehension,

            return_expression,

            &quantified_vars,

        )

    }

    has_quantified_conjunction_in_pruning_position(

        comprehension,

        return_expression,

        &quantified_vars,

    )

}

fn has_quantified_conjunction_in_pruning_position(

    comprehension: &Comprehension,

    expression: &Expr,

    quantified_vars: &BTreeSet<Name>,

) -> bool {

    match expression {

        Expr::Imply(_, antecedent, _) => antecedent.any_expression(|subexpression| {

            matches!(subexpression, Expr::And(_, _))

                && expression_depends_only_on_quantified_decisions(

                    comprehension,

                    subexpression,

                    quantified_vars,

                )

        }),

        _ => false,

}

fn expression_depends_only_on_quantified_decisions(

    comprehension: &Comprehension,

    expression: &Expr,

    quantified_vars: &BTreeSet<Name>,

) -> bool {

    let referenced_names = Biplate::<Name>::universe_bi(expression);

    referenced_names

        .iter()

        .any(|name| quantified_vars.contains(name))

        && comprehension.is_quantified_guard(expression)

}

fn simplify_expanded_ac_results(results: Vec<Expr>, ac_operator: ACOperatorKind) -> Vec<Expr> {

    let simplified = simplify_expression(ac_operator.as_expression(into_matrix_expr!(results)));

    match (&ac_operator, &simplified) {

        | (ACOperatorKind::Max, Expr::Max(_, matrix)) => matrix

            .unwrap_list_cow()

            .map(std::borrow::Cow::into_owned)

        _ => vec![simplified],

}

fn exists_quantified_to_finds(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

    let Expr::Root(metadata, constraints) = expr else {

        return Err(RuleNotApplicable);

    let mut new_symbols = symbols.clone();

    let mut new_constraints = Vec::with_capacity(constraints.len());

    let mut changed = false;

    for constraint in constraints {

        let Some(comprehension) = as_exists_comprehension(constraint) else {

            new_constraints.push(constraint.clone());

            continue;

            rewrite_exists_comprehension_to_constraints(&comprehension, &mut new_symbols)

        new_constraints.extend(new_constraints_for_exists);

        changed = true;

    if changed {

        Ok(RuleEffect::with_symbols(

            Expr::Root(metadata.clone(), new_constraints),

            new_symbols,

        ))

        Err(RuleNotApplicable)

}

fn expand_ac_comprehension_native(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

    let ac_operator_kind = expr.to_ac_operator_kind().ok_or(RuleNotApplicable)?;

    let children = expr.children();

    debug_assert_eq!(

        children.len(),

        1,

    let comprehension = children

        .front()

        .and_then(as_single_comprehension)

        .ok_or(RuleNotApplicable)?;

}

fn expand_comprehension_native(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

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

        return Err(RuleNotApplicable);

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

    if selected_comprehension_expander(&comprehension) != QuantifiedExpander::Native {

    }

    for qual in &comprehension.qualifiers {

        if let ComprehensionQualifier::ExpressionGenerator { .. } = qual {

        }

    let mut symbols = symbols.clone();

    let comprehension_domain = comprehension.domain_of();

    let skip_operator = comprehension.skip_operator;

    let results = expand_native(comprehension, &mut symbols).or(Err(RuleNotApplicable))?;

    let results = match skip_operator {

        Some(op) => simplify_expanded_ac_results(results, op),

        None => results,

    let expanded = into_matrix_expr!(results);

    let expanded = match comprehension_domain {

        Some(domain) if expanded.list_len() == Some(0) => {

        _ => expanded,

    Ok(RuleEffect::with_symbols(expanded, symbols))

}

fn expand_comprehension_via_solver(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

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

        return Err(RuleNotApplicable);

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

    if !matches!(

        selected_comprehension_expander(&comprehension),

        QuantifiedExpander::ViaSolver | QuantifiedExpander::ViaSolverAc

    ) {

        return Err(RuleNotApplicable);

}

fn expand_comprehension_via_solver_ac(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

    let ac_operator_kind = expr.to_ac_operator_kind().ok_or(RuleNotApplicable)?;

    let children = expr.children();

    debug_assert_eq!(

        children.len(),

        1,

    let comprehension = children

        .front()

        .and_then(as_single_comprehension)

        .ok_or(RuleNotApplicable)?;

    if selected_comprehension_expander(&comprehension) != QuantifiedExpander::ViaSolverAc {

        return Err(RuleNotApplicable);

    }

    for qual in &comprehension.qualifiers {

        if let ComprehensionQualifier::ExpressionGenerator { .. } = qual {

        }

    let results = match expand_via_solver_ac(comprehension.clone(), ac_operator_kind) {

        Ok(results) => results,

    let new_expr = ac_operator_kind.as_expression(into_matrix_expr!(results));

    Ok(RuleEffect::with_symbols(new_expr, symbols.clone()))

}

fn as_single_comprehension(expr: &Expr) -> Option<Comprehension> {

    if let Expr::Comprehension(_, comprehension) = expr {

        return Some(comprehension.as_ref().clone());

    }

    let [Expr::Comprehension(_, comprehension)] = expr.unwrap_list_ref()? else {

        return None;

}

fn as_exists_comprehension(expr: &Expr) -> Option<Comprehension> {

    let Expr::Or(_, or_child) = expr else {

        return None;

    as_single_comprehension(or_child.as_ref())

}

fn comprehension_has_non_quantified_guards(comprehension: &Comprehension) -> bool {

    comprehension.qualifiers.iter().any(|qualifier| {

        let ComprehensionQualifier::Condition(condition) = qualifier else {

            return false;

        !comprehension.is_quantified_guard(condition)

    })

}

fn rewrite_exists_comprehension_to_constraints(

    comprehension: &Comprehension,

    symbols: &mut SymbolTable,

) -> Option<Vec<Expr>> {

    let quantified_declarations = quantified_declarations(comprehension)?;

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

    let mut replacements_by_name: HashMap<Name, DeclarationPtr> = HashMap::new();

    for decl in quantified_declarations {

        let domain = decl.domain()?;

            replace_declaration_ptrs_in_domain(domain, &replacements_by_id, &replacements_by_name);

        let fresh_decl = symbols.gen_find_auxiliary(&rewritten_domain);

        replacements_by_id.insert(decl.id(), fresh_decl.clone());

        replacements_by_name.insert(decl.name().clone(), fresh_decl);

    let mut conjuncts = Vec::new();

    for qualifier in &comprehension.qualifiers {

        if let ComprehensionQualifier::Condition(condition) = qualifier {

        }

    conjuncts.push(replace_declaration_ptrs_in_expr(

        comprehension.return_expression.clone(),

        &replacements_by_id,

        &replacements_by_name,

    ));

    Some(conjuncts)

}

fn quantified_declarations(comprehension: &Comprehension) -> Option<Vec<DeclarationPtr>> {

    let quantified_names = comprehension.quantified_vars();

    let symbols = comprehension.symbols();

    quantified_names

        .into_iter()

        .map(|name| symbols.lookup_local(&name))

}

fn replace_declaration_ptrs_in_expr(

    expr: Expr,

    replacements_by_id: &HashMap<ObjId, DeclarationPtr>,

    replacements_by_name: &HashMap<Name, DeclarationPtr>,

) -> Expr {

    let rewritten = expr

        .transform_bi(&|decl: DeclarationPtr| {

            if let Some(replacement) = replacements_by_id.get(&decl.id()) {

                return replacement.clone();

            }

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

            replacements_by_name.get(&name).cloned().unwrap_or(decl)

        })

        .transform_bi(&|reference: Reference| {

            replace_reference(reference, replacements_by_id, replacements_by_name)

        });

    rewritten.transform_bi(&|mut comprehension: Comprehension| {

        let shadowed_names = comprehension.quantified_vars();

        let visible_replacements_by_name = replacements_by_name

            .iter()

            .filter(|(name, _)| !shadowed_names.contains(name))

            .map(|(name, declaration)| (name.clone(), declaration.clone()))

        comprehension.return_expression = replace_declaration_ptrs_in_expr(

            comprehension.return_expression,

            replacements_by_id,

            &visible_replacements_by_name,

        );

        for qualifier in &mut comprehension.qualifiers {

        comprehension

    })

}

fn replace_declaration_ptrs_in_domain(

    domain: DomainPtr,

    replacements_by_id: &HashMap<ObjId, DeclarationPtr>,

    replacements_by_name: &HashMap<Name, DeclarationPtr>,

) -> DomainPtr {

    let mut rewritten = domain

    rewrite_int_ranges_in_domain_ptr(&mut rewritten, replacements_by_id, replacements_by_name);

    rewritten

}

fn replace_reference(

    reference: Reference,

    replacements_by_id: &HashMap<ObjId, DeclarationPtr>,

    replacements_by_name: &HashMap<Name, DeclarationPtr>,

) -> Reference {

    let replacement = replacements_by_id

        .get(&reference.ptr().id())

        .cloned()

        .or_else(|| {

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

            replacements_by_name.get(&name).cloned()

        });

    replacement.map(Reference::new).unwrap_or(reference)

}

fn rewrite_int_ranges_in_domain_ptr(

    domain: &mut DomainPtr,

    replacements_by_id: &HashMap<ObjId, DeclarationPtr>,

    replacements_by_name: &HashMap<Name, DeclarationPtr>,

) {

    let mut rewritten = domain.as_ref().clone();

    rewrite_int_ranges_in_domain(&mut rewritten, replacements_by_id, replacements_by_name);

    *domain = Moo::new(rewritten);

}

fn rewrite_int_ranges_in_domain(

    domain: &mut Domain,

    replacements_by_id: &HashMap<ObjId, DeclarationPtr>,

    replacements_by_name: &HashMap<Name, DeclarationPtr>,

) {

    let Domain::Unresolved(unresolved) = domain else {

        return;

    rewrite_int_ranges_in_unresolved_domain(

        Moo::make_mut(unresolved),

        replacements_by_id,

        replacements_by_name,

    );

}

fn rewrite_int_ranges_in_unresolved_domain(

    unresolved: &mut UnresolvedDomain,

    replacements_by_id: &HashMap<ObjId, DeclarationPtr>,

    replacements_by_name: &HashMap<Name, DeclarationPtr>,

) {

    match unresolved {

            for range in ranges {

                rewrite_int_range(range, replacements_by_id, replacements_by_name);

}

fn rewrite_int_range(

    range: &mut Range<IntVal>,

    replacements_by_id: &HashMap<ObjId, DeclarationPtr>,

    replacements_by_name: &HashMap<Name, DeclarationPtr>,

) {

    match range {

            rewrite_int_value(lower, replacements_by_id, replacements_by_name);

            rewrite_int_value(upper, replacements_by_id, replacements_by_name);

}

fn rewrite_int_value(

    int_val: &mut IntVal,

    replacements_by_id: &HashMap<ObjId, DeclarationPtr>,

    replacements_by_name: &HashMap<Name, DeclarationPtr>,

) {

    match int_val {

            *reference =

                replace_reference(reference.clone(), replacements_by_id, replacements_by_name);

            let rewritten = replace_declaration_ptrs_in_expr(

                (**expr).clone(),

                replacements_by_id,

                replacements_by_name,

            );

            *expr = Moo::new(rewritten);

        IntVal::Const(_) => {}

}

    fn literal(literal: Literal) -> Expr {

        Expr::Atomic(Metadata::new(), Atom::Literal(literal))

    }

    fn reference(declaration: DeclarationPtr) -> Expr {

        Expr::Atomic(Metadata::new(), Atom::new_ref(declaration))

    }

    fn eq(lhs: Expr, rhs: Expr) -> Expr {

        Expr::Eq(Metadata::new(), Moo::new(lhs), Moo::new(rhs))

    }

    fn comprehension_with_int_generator(

        upper: i32,

        parent: SymbolTablePtr,

    ) -> (Comprehension, DeclarationPtr) {

        let declaration = DeclarationPtr::new_quantified(

            Name::user("i"),

            Domain::int(vec![Range::Bounded(1, upper)]),

        );

        let comprehension = ComprehensionBuilder::new(parent)

            .generator(declaration)

            .with_return_value(literal(Literal::Bool(true)));

        let ComprehensionQualifier::Generator { ptr } = &comprehension.qualifiers[0] else {

        (comprehension.clone(), ptr.clone())

    }

    fn auto_keeps_small_guarded_comprehensions_native() {

        let (mut comprehension, quantified) = comprehension_with_int_generator(

            AUTO_SOLVER_THRESHOLD as i32 - 1,

            SymbolTablePtr::new(),

        );

        comprehension

            .qualifiers

            .push(ComprehensionQualifier::Condition(eq(

                reference(quantified),

                literal(Literal::Int(1)),

            )));

        assert_eq!(

            auto_comprehension_expander(&comprehension),

            QuantifiedExpander::Native

    }

    fn auto_uses_solver_for_large_quantified_guards() {

        let parent = SymbolTablePtr::new();

        let outer = DeclarationPtr::new_find(Name::user("outer"), Domain::bool());

        parent.write().insert(outer.clone());

            comprehension_with_int_generator(AUTO_SOLVER_THRESHOLD as i32, parent);

        comprehension

            .qualifiers

            .push(ComprehensionQualifier::Condition(eq(

                reference(quantified),

                literal(Literal::Int(1)),

            )));

        comprehension.return_expression = reference(outer);

        comprehension.skip_operator = Some(ACOperatorKind::And);

        assert_eq!(

            auto_comprehension_expander(&comprehension),

            QuantifiedExpander::ViaSolverAc

    }

    fn auto_keeps_single_ac_comparison_with_outer_decision_native() {

        let parent = SymbolTablePtr::new();

        let outer = DeclarationPtr::new_find(Name::user("outer"), Domain::bool());

        parent.write().insert(outer.clone());

            comprehension_with_int_generator(AUTO_SOLVER_THRESHOLD as i32, parent);

        let quantified_filter = eq(reference(quantified), literal(Literal::Int(1)));

        comprehension.return_expression = Expr::Imply(

            Metadata::new(),

            Moo::new(quantified_filter),

            Moo::new(reference(outer)),

        );

        comprehension.skip_operator = Some(ACOperatorKind::And);

        assert_eq!(

            auto_comprehension_expander(&comprehension),

            QuantifiedExpander::Native

    }

    fn auto_uses_solver_for_quantified_conjunction_in_ac_return() {

        let parent = SymbolTablePtr::new();

        let outer = DeclarationPtr::new_find(Name::user("outer"), Domain::bool());

        parent.write().insert(outer.clone());

            comprehension_with_int_generator(AUTO_SOLVER_THRESHOLD as i32, parent);

        let filters = vec![

            eq(reference(quantified.clone()), literal(Literal::Int(1))),

            eq(reference(quantified), literal(Literal::Int(2))),

        let quantified_filter = Expr::And(Metadata::new(), Moo::new(into_matrix_expr!(filters)));

        comprehension.return_expression = Expr::Imply(

            Metadata::new(),

            Moo::new(quantified_filter),

            Moo::new(reference(outer)),

        );

        comprehension.skip_operator = Some(ACOperatorKind::And);

        assert_eq!(

            auto_comprehension_expander(&comprehension),

            QuantifiedExpander::ViaSolverAc

    }

    fn auto_ignores_quantified_conjunctions_in_implication_consequents() {

        let parent = SymbolTablePtr::new();

        let outer = DeclarationPtr::new_find(Name::user("outer"), Domain::bool());

        parent.write().insert(outer.clone());

            comprehension_with_int_generator(AUTO_SOLVER_THRESHOLD as i32, parent);

        let single_filter = eq(reference(quantified.clone()), literal(Literal::Int(1)));

        let quantified_conjunction = Expr::And(

            Metadata::new(),

            Moo::new(into_matrix_expr!(vec![

                eq(reference(quantified.clone()), literal(Literal::Int(1)),),

                eq(reference(quantified), literal(Literal::Int(2))),

            ])),

        );

        let consequent = Expr::And(

            Metadata::new(),

            Moo::new(into_matrix_expr!(vec![

                quantified_conjunction,

                reference(outer),

            ])),

        );

        comprehension.return_expression = Expr::Imply(

            Metadata::new(),

            Moo::new(single_filter),

            Moo::new(consequent),

        );

        comprehension.skip_operator = Some(ACOperatorKind::And);

        assert_eq!(

            auto_comprehension_expander(&comprehension),

            QuantifiedExpander::Native

    }

    fn auto_uses_solver_for_dependent_generators_with_nested_returns() {

        let parent = SymbolTablePtr::new();

            comprehension_with_int_generator(AUTO_SOLVER_THRESHOLD as i32, parent);

        let dependent_domain = Domain::int(vec![Range::Bounded(

            IntVal::Const(1),

            IntVal::Reference(Reference::new(outer)),

        )]);

        let inner_generator = DeclarationPtr::new_quantified(Name::user("j"), dependent_domain);

        comprehension

            .qualifiers

            .push(ComprehensionQualifier::Generator {

                ptr: inner_generator,

            });

        let nested = ComprehensionBuilder::new(SymbolTablePtr::new())

            .with_return_value(literal(Literal::Bool(true)));

        comprehension.return_expression = Expr::Comprehension(Metadata::new(), Moo::new(nested));

        comprehension.skip_operator = Some(ACOperatorKind::And);

        assert_eq!(

            auto_comprehension_expander(&comprehension),

            QuantifiedExpander::ViaSolverAc

    }

    fn auto_keeps_large_unprunable_comprehensions_native() {

        let parent = SymbolTablePtr::new();

        let outer = DeclarationPtr::new_find(Name::user("outer"), Domain::bool());

        parent.write().insert(outer.clone());

            comprehension_with_int_generator(AUTO_SOLVER_THRESHOLD as i32, parent);

        comprehension.return_expression = reference(outer);

        comprehension.skip_operator = Some(ACOperatorKind::And);

        assert_eq!(

            auto_comprehension_expander(&comprehension),

            QuantifiedExpander::Native

    }

    fn replaces_references_in_expressions() {

        let quantified = DeclarationPtr::new_quantified(Name::user("matrix_bools"), Domain::bool());

        let replacement = DeclarationPtr::new_find(Name::Machine(0), Domain::bool());

        let safe_index = Expr::SafeIndex(

            Metadata::new(),

            Moo::new(Expr::Atomic(

                Metadata::new(),

                Atom::new_ref(quantified.clone()),

            )),

            vec![Expr::Atomic(

                Metadata::new(),

                Atom::Literal(Literal::Int(1)),

            )],

        );

            ComprehensionBuilder::new(SymbolTablePtr::new()).with_return_value(safe_index);

        let expr = Expr::Comprehension(Metadata::new(), Moo::new(inner_comprehension));

        let replacements_by_id = HashMap::from([(quantified.id(), replacement.clone())]);

            HashMap::from([(quantified.name().clone(), replacement.clone())]);

            replace_declaration_ptrs_in_expr(expr, &replacements_by_id, &replacements_by_name);

        let Expr::Comprehension(_, comprehension) = rewritten else {

        let Expr::SafeIndex(_, subject, _) = &comprehension.return_expression else {

        let Expr::Atomic(_, Atom::Reference(reference)) = subject.as_ref() else {

        assert_eq!(reference.id(), replacement.id());

    }