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;

        let Some(new_constraints_for_exists) =

            rewrite_exists_comprehension_to_constraints(&comprehension, &mut new_symbols)

        new_constraints.extend(new_constraints_for_exists);

        changed = true;

    if changed {

        Ok(Reduction::with_symbols(

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

            new_symbols,

        ))

        Err(RuleNotApplicable)

}

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

    if comprehension_expander() != QuantifiedExpander::Native {

        return Err(RuleNotApplicable);

    }

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

        return Err(RuleNotApplicable);

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

    let mut symbols = symbols.clone();

    let results = expand_native(comprehension, &mut symbols)

    Ok(Reduction::with_symbols(into_matrix_expr!(results), symbols))

}

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

    if !matches!(

        comprehension_expander(),

        return Err(RuleNotApplicable);

    }

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

        return Err(RuleNotApplicable);

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

    let results = expand_via_solver(comprehension)

    Ok(Reduction::with_symbols(

        into_matrix_expr!(results),

        symbols.clone(),

    ))

}

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

    if comprehension_expander() != QuantifiedExpander::ViaSolverAc {

        return Err(RuleNotApplicable);

    }

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

    debug_assert_eq!(

        expr.children().len(),

    let comprehension = as_single_comprehension(&expr.children()[0]).ok_or(RuleNotApplicable)?;

    let results =

        expand_via_solver_ac(comprehension, ac_operator_kind).or(Err(RuleNotApplicable))?;

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

    Ok(Reduction::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 exprs = expr.clone().unwrap_list()?;

    let [Expr::Comprehension(_, comprehension)] = exprs.as_slice() 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 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()?;

        let rewritten_domain =

            replace_declaration_ptrs_in_domain(domain, &replacements_by_id, &replacements_by_name);

        let fresh_decl = symbols.gensym(&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))

        .collect()

}

fn replace_declaration_ptrs_in_expr(

    expr: Expr,

    replacements_by_id: &HashMap<ObjId, DeclarationPtr>,

    replacements_by_name: &HashMap<Name, DeclarationPtr>,

) -> Expr {

    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)

    })

}

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

        .transform_bi(&|expr: Expr| {

        .transform_bi(&|reference: Reference| {

    rewrite_int_ranges_in_domain_ptr(&mut rewritten, replacements_by_id, replacements_by_name);

    rewritten

}

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 {

        UnresolvedDomain::Int(ranges) => {

            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 {

        Range::Bounded(lower, upper) => {

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

) {

    if let IntVal::Expr(expr) = int_val {

        let rewritten = replace_declaration_ptrs_in_expr(

            (**expr).clone(),

            replacements_by_id,

            replacements_by_name,

        );

        *expr = Moo::new(rewritten);

    }

}