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

    let (matrix, except) = match expr {

        Expr::AllDiff(_, matrix) => (matrix, None),

            let value = super::pseudo_boolean::integer_view(except).ok_or(RuleNotApplicable)?;

            (matrix, Some(value))

        _ => return Err(RuleNotApplicable),

    let elements = super::counting::matrix_entries(matrix).ok_or(RuleNotApplicable)?;

    let inputs = elements

        .iter()

        .map(super::pseudo_boolean::integer_view)

        .collect::<Option<Vec<_>>>()

        .ok_or(RuleNotApplicable)?;

    let mut symbols = symbols.clone();

    let output = super::boolean::create_bool_aux(&mut symbols);

    Ok(RuleEffect::sat(

        output.clone(),

        vec![SatEncodingDecision::AllDifferent {

            output,

            inputs,

            comparisons: None,

            except,

            encoding: None,

            amo_encoding: None,

            pb_encoding: None,

        }],

        symbols,

    ))

}

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

    let (matrix, except) = match expr {

        Expr::AllDiff(_, matrix) => (matrix, None),

        Expr::AllDifferentExcept(_, matrix, except) => (matrix, Some(except)),

        _ => return Err(RuleNotApplicable),

    let inputs = super::counting::matrix_entries(matrix).ok_or(RuleNotApplicable)?;

    if inputs.is_empty()

        || inputs.iter().any(|input| {

            matches!(

                input.return_type(),

        })

        return Err(RuleNotApplicable);

    }

    let mut symbols = symbols.clone();

    let mut definitions = Vec::new();

    let mut conditions = Vec::new();

    for (index, left) in inputs.iter().enumerate() {

        let exempt = except.filter(|_| index + 1 < inputs.len()).map(|except| {

            let output = super::boolean::create_bool_aux(&mut symbols);

            definitions.push(Expr::Iff(

                Metadata::new(),

                Moo::new(output.clone()),

                Moo::new(Expr::Eq(

                    Metadata::new(),

                    Moo::new(left.clone()),

                    except.clone(),

                )),

            ));

            output

        });

        for right in &inputs[index + 1..] {

            let unequal = Expr::Neq(

                Metadata::new(),

                Moo::new(left.clone()),

                Moo::new(right.clone()),

            );

            conditions.push(if let Some(exempt) = &exempt {

                Expr::Or(

                    Metadata::new(),

                    Moo::new(conjure_cp::into_matrix_expr!(vec![unequal, exempt.clone()])),

                )

                unequal

    Ok(RuleEffect::new(

        Expr::SatAllDifferentComparisons(

            Metadata::new(),

            Moo::new(conjure_cp::into_matrix_expr!(conditions)),

        ),

        definitions,

        symbols,

    ))

}

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

    let Expr::SatAllDifferentComparisons(_, comparisons) = expr else {

        return Err(RuleNotApplicable);

    let comparisons = comparisons.unwrap_list_cow().ok_or(RuleNotApplicable)?;

    if !comparisons.iter().all(|condition| {

        condition.return_type() == ReturnType::Bool && crate::shared::utils::is_literal(condition)

    }) {

        return Err(RuleNotApplicable);

    }

    let mut symbols = symbols.clone();

    let output = super::boolean::create_bool_aux(&mut symbols);

    Ok(RuleEffect::sat(

        output.clone(),

        vec![SatEncodingDecision::AllDifferent {

            output,

            inputs: vec![],

            comparisons: Some(comparisons.into_owned()),

            except: None,

            encoding: None,

            amo_encoding: None,

            pb_encoding: None,

        }],

        symbols,

    ))

}