fn select_encoding<T: Copy>(

    pinned: Option<T>,

    algorithms: &[T],

    labels: &[&str],

    compact: impl FnOnce() -> usize,

) -> (T, SelectionProvenance) {

    if let Some(algorithm) = pinned {

        return (algorithm, SelectionProvenance::ExplicitConfiguration);

    }

    let index = if algorithms.len() == 1 {

        0

        match settings::heuristic() {

            Heuristic::First => 0,

            Heuristic::Compact => compact(),

            Heuristic::All => settings::next_heuristic_all_index(labels),

    (algorithms[index], SelectionProvenance::Heuristic)

}

pub(crate) fn resolve_encoding_choices(decisions: &mut [SatEncodingDecision]) {

    resolve_element_choices(decisions);

    resolve_table_choices(decisions);

    resolve_alldifferent_choices(decisions);

    resolve_pb_choices(decisions);

    resolve_cardinality_choices(decisions);

    resolve_amo_choices(decisions);

}

fn resolve_element_choices(decisions: &mut [SatEncodingDecision]) {

    let sizes = decisions

        .iter()

        .filter_map(|decision| match decision {

            } => Some(entries.len()),

            _ => None,

        })

    if sizes.is_empty() {

        return;

    }

    let algorithms = &ElementEncoding::ALL;

    let (algorithm, provenance) = select_encoding(

        settings::element_encoding(),

        algorithms,

        &ElementEncoding::LABELS,

        || usize::from(sizes.iter().any(|size| *size > 4)),

    for decision in decisions {

        if let SatEncodingDecision::Element { encoding, .. } = decision

            && encoding.is_none()

            *encoding = Some(EncodingSelection {

                algorithm,

                provenance,

            });

        }

}

fn resolve_table_choices(decisions: &mut [SatEncodingDecision]) {

    if settings::table_encoding().is_none() && settings::heuristic() == Heuristic::Compact {

        for decision in decisions {

            if let SatEncodingDecision::Table {

                rows,

                row_views,

                encoding,

                ..

            } = decision

                && encoding.is_none()

                let algorithm = compact_table_encoding(rows, row_views.as_ref().map(Vec::len));

                *encoding = Some(EncodingSelection {

                    algorithm,

                    provenance: SelectionProvenance::Heuristic,

                });

            }

        return;

    }

    let rows = decisions

        .iter()

        .filter_map(|decision| match decision {

            } => Some(rows.len()),

            _ => None,

        })

    if rows.is_empty() {

        return;

    }

    let binary = decisions.iter().all(|decision| match decision {

        } => inputs.len() == 2 && row_views.is_none(),

        _ => true,

    });

    let algorithms = &TableEncoding::ALL[..if binary { 3 } else { 2 }];

    let labels = &TableEncoding::LABELS[..algorithms.len()];

        select_encoding(settings::table_encoding(), algorithms, labels, || {

    for decision in decisions {

        if let SatEncodingDecision::Table { encoding, .. } = decision

            && encoding.is_none()

            *encoding = Some(EncodingSelection {

                algorithm,

                provenance,

            });

        }

}

fn compact_table_encoding(rows: &[Vec<i64>], variable_row_count: Option<usize>) -> TableEncoding {

    let count = variable_row_count

        .unwrap_or_else(|| rows.iter().collect::<std::collections::BTreeSet<_>>().len());

    if count > 4 {

        TableEncoding::Mdd

}

fn resolve_alldifferent_choices(decisions: &mut [SatEncodingDecision]) {

    let eligible: Vec<_> = decisions

        .iter()

        .filter_map(|decision| match decision {

            } => Some(comparisons.is_none() && inputs.iter().all(|input| input.choices.is_some())),

            _ => None,

        })

    if eligible.is_empty() {

        return;

    }

    let algorithms = if eligible.iter().all(|eligible| *eligible) {

        &AllDifferentEncoding::ALL[..]

        &AllDifferentEncoding::ALL[..1]

    let (algorithm, provenance) = select_encoding(

        settings::alldifferent_encoding(),

        algorithms,

        &AllDifferentEncoding::LABELS[..algorithms.len()],

    for decision in decisions {

        if let SatEncodingDecision::AllDifferent { encoding, .. } = decision

            && encoding.is_none()

            *encoding = Some(EncodingSelection {

                algorithm,

                provenance,

            });

        }

}

pub(crate) fn count_uses_amo(inputs: &[Expression], relation: IntegerRelation, bound: i64) -> bool {

        inputs

            .iter()

                (0i128, 0usize),

                |(constants, variables), input| match crate::ast::eval_constant(input) {

                    Some(crate::ast::Literal::Bool(true)) => (constants + 1, variables),

                    Some(crate::ast::Literal::Bool(false)) => (constants, variables),

                    _ => (constants, variables + 1),

                },

    if variables <= 1 {

        return false;

    }

    let bound = i128::from(bound) - constants;

    match relation {

        IntegerRelation::Less | IntegerRelation::GreaterEqual => bound - 1 == 1,

        IntegerRelation::LessEqual | IntegerRelation::Greater => bound == 1,

        IntegerRelation::Equal | IntegerRelation::NotEqual => bound == 1 || bound - 1 == 1,

}

fn resolve_amo_choices(decisions: &mut [SatEncodingDecision]) {

    let compact = settings::amo_encoding().is_none() && settings::heuristic() == Heuristic::Compact;

    let largest = decisions

        .iter()

        .filter_map(|decision| match decision {

            } => Some(inputs.len()),

            } if count_uses_amo(inputs, *relation, *bound) => Some(inputs.len()),

            } if selection.algorithm == AllDifferentEncoding::ValueAmo => Some(inputs.len()),

            _ => None,

        })

    let Some(largest) = largest else {

        return;

    let (algorithm, provenance) = select_encoding(

        settings::amo_encoding(),

        &AmoEncoding::ALL,

        &AmoEncoding::LABELS,

        || usize::from(largest > 5),

    for decision in decisions {

        let algorithm = if compact {

            let size = match &*decision {

                | SatEncodingDecision::CountRelation { inputs, .. } => inputs.len(),

                _ => 0,

            compact_amo_encoding(size)

            algorithm

        if let SatEncodingDecision::CountRelation {

            inputs,

            relation,

            bound,

            amo_encoding,

            ..

        } = decision

            && amo_encoding.is_none()

            && count_uses_amo(inputs, *relation, *bound)

            *amo_encoding = Some(EncodingSelection {

                algorithm,

                provenance,

            });

        }

        if let SatEncodingDecision::AtMostOne { encoding, .. }

        | SatEncodingDecision::AllDifferent {

            amo_encoding: encoding,

            encoding:

                Some(EncodingSelection {

                    algorithm: AllDifferentEncoding::ValueAmo,

                    ..

                }),

            ..

        } = decision

            && encoding.is_none()

            *encoding = Some(EncodingSelection {

                algorithm,

                provenance,

            });

        }

}

fn compact_amo_encoding(size: usize) -> AmoEncoding {

    if size <= 5 {

        AmoEncoding::Pairwise

        AmoEncoding::Ladder

}

fn resolve_cardinality_choices(decisions: &mut [SatEncodingDecision]) {

    if !decisions.iter().any(|decision| {

        matches!(

            decision,

    }) {

        return;

    }

    let (algorithm, provenance) = select_encoding(

        settings::cardinality_encoding(),

        &CardinalityEncoding::ALL,

        &CardinalityEncoding::LABELS,

    for decision in decisions {

        if let SatEncodingDecision::Cardinality { encoding, .. }

        | SatEncodingDecision::CountRelation { encoding, .. } = decision

            && encoding.is_none()

            *encoding = Some(EncodingSelection {

                algorithm,

                provenance,

            });

        }

}

fn resolve_pb_choices(decisions: &mut [SatEncodingDecision]) {

    let unresolved: Vec<_> = decisions

        .iter()

        .filter_map(|decision| match decision {

            } => Some(terms),

            } => Some(&value.terms),

            } => inputs

                .iter()

                .chain(except.iter())

                .max_by_key(|input| {

                    input

                        .terms

                        .iter()

                        .map(|(weight, _)| i128::from(*weight).abs())

                })

                .map(|input| &input.terms),

            } => inputs

                .iter()

                .chain(row_views.iter().flatten().flatten())

                .max_by_key(|input| {

                    input

                        .terms

                        .iter()

                        .map(|(weight, _)| i128::from(*weight).abs())

                })

                .map(|input| &input.terms),

            } => std::iter::once(index_view)

                .chain(std::iter::once(value))

                .chain(entries.iter().map(|(_, entry)| entry))

                .max_by_key(|view| {

                    view.terms

                        .iter()

                        .map(|(weight, _)| i128::from(*weight).abs())

                })

                .map(|view| &view.terms),

            _ => None,

        })

    if unresolved.is_empty() {

        return;

    }

    let (algorithm, provenance) = select_encoding(

        settings::pb_encoding(),

        &PbEncoding::ALL,

        &PbEncoding::LABELS,

        || {

            usize::from(unresolved.iter().any(|terms| {

                terms

                    .iter()

                    .map(|(weight, _)| i128::from(*weight).abs())

                    > 4096

            }))

        },

    for decision in decisions {

        if let SatEncodingDecision::PseudoBoolean { encoding, .. }

        | SatEncodingDecision::IntegerRelation { encoding, .. }

        | SatEncodingDecision::Objective { encoding, .. }

        | SatEncodingDecision::AllDifferent {

            pb_encoding: encoding,

            ..

        }

        | SatEncodingDecision::Table {

            pb_encoding: encoding,

            ..

        }

        | SatEncodingDecision::Element {

            pb_encoding: encoding,

            ..

        } = decision

            && encoding.is_none()

            *encoding = Some(EncodingSelection {

                algorithm,

                provenance,

            });

        }

}