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

    let mut encodings = HashSet::new();

    let mut has_indicator = false;

    let mut operands_ready = true;

    let table = matches!(expr, Expr::Table(..) | Expr::NegativeTable(..));

    let inputs = if table {

        expr.children()

            .into_iter()

            .flat_map(|child| {

                crate::shared::utils::table_operand(&child)

                    .universe()

                    .into_iter()

                    .filter(|input| matches!(input, Expr::SATInt(..)))

            })

        operands(expr).collect()

    for operand in inputs {

        let indicator = ready_indicator(&operand);

        has_indicator |= indicator;

        operands_ready &= indicator

            || matches!(

                operand,

        if let Expr::SATInt(_, encoding, _, _) = operand {

            encodings.insert(encoding);

        }

    let retains_views = matches!(

        expr,

    if retains_views && !encodings.iter().any(needs_actual_value_circuit) {

        return Err(RuleNotApplicable);

    }

    let has_indicator = !retains_views && has_indicator && operands_ready;

    if !has_indicator

        && encodings

            .iter()

            .all(|encoding| matches!(encoding, SATIntEncoding::Log))

        return Err(RuleNotApplicable);

    }

    let mut decisions = Vec::new();

    let mut new_symbols = symbols.clone();

    let mut convert = |input: Expr| {

        if (retains_views

            && !matches!(&input, Expr::SATInt(_, encoding, _, _) if needs_actual_value_circuit(encoding)))

            || (!has_indicator && ready_indicator(&input))

            input

            to_log(input, &mut decisions, &mut new_symbols)

    };

    let children: VecDeque<Expr> = expr

        .children()

        .into_iter()

        .map(|child| {

            if table {

                map_table_cells(crate::shared::utils::table_operand(&child), &mut convert)

                match matrix_child(&child) {

                        let converted: Vec<Expr> = elements.into_iter().map(&mut convert).collect();

                        rebuild_matrix_child(converted, index_domain)

                    None => convert(child),

        })

    let new_expression = expr.with_children(children);

    if new_expression == *expr && decisions.is_empty() {

    }

    Ok(RuleEffect::sat(new_expression, decisions, new_symbols))

}

fn needs_actual_value_circuit(encoding: &SATIntEncoding) -> bool {

    matches!(encoding, SATIntEncoding::Rank(ranges) if ranges.len() != 1)

}

fn map_table_cells(expression: Expr, convert: &mut impl FnMut(Expr) -> Expr) -> Expr {

    if matches!(expression, Expr::SATInt(..)) {

        return convert(expression);

    }

    let children = expression

        .children()

        .into_iter()

        .map(|child| map_table_cells(crate::shared::utils::table_operand(&child), convert))

    expression.with_children(children)

}

fn matrix_child(expr: &Expr) -> Option<(Vec<Expr>, DomainPtr)> {

    match expr {

            Some((elements.clone(), index_domain.clone()))

        _ => None,

}

fn rebuild_matrix_child(elements: Vec<Expr>, index_domain: DomainPtr) -> Expr {

    Expr::AbstractLiteral(

        Metadata::new(),

        AbstractLiteral::Matrix(elements, index_domain),

    )

}

fn operands(expr: &Expr) -> impl Iterator<Item = Expr> {

    expr.children()

        .into_iter()

        .flat_map(|child| match matrix_child(&child) {

            Some((elements, _)) => elements,

            None => vec![child],

        })

}

fn to_log(expr: Expr, decisions: &mut Vec<SatEncodingDecision>, symbols: &mut SymbolTable) -> Expr {

    if ready_indicator(&expr) {

        let Expr::ToInt(_, input) = expr else {

        return Expr::SATInt(

            Metadata::new(),

            SATIntEncoding::Log,

            Moo::new(into_matrix_expr!(vec![

                input.as_ref().clone(),

                false.into()

            ])),

            (0, 1),

        );

    }

    let Expr::SATInt(_, encoding, bits, bounds) = &expr else {

        return expr;

    if matches!(encoding, SATIntEncoding::Log) {

        return expr;

    }

    let Some(bits) = bits.as_ref().clone().into_list() else {

    let (low, high) = *bounds;

    let width = bit_magnitude(low).max(bit_magnitude(high));

    if matches!(encoding, SATIntEncoding::Offset | SATIntEncoding::Rank(_)) {

        let mut decoded = add_unsigned_constant(&bits, i64::from(low), width, decisions, symbols);

        if let SATIntEncoding::Rank(ranges) = encoding {

            let mut start = 0u64;

            for (index, &(range_low, range_high)) in ranges.iter().enumerate() {

                if index > 0 {

                    let selector = unsigned_at_least(&bits, start, decisions, symbols);

                    let candidate = add_unsigned_constant(

                        &bits,

                        i64::from(range_low) - start as i64,

                        width,

                        decisions,

                        symbols,

                    );

                    decoded = decoded

                        .into_iter()

                        .zip(candidate)

                        .map(|(old, new)| {

                            tseytin_mux(selector.clone(), old, new, decisions, symbols)

                        })

                }

                start += (i64::from(range_high) - i64::from(range_low) + 1) as u64;

        }

        return Expr::SATInt(

            Metadata::new(),

            SATIntEncoding::Log,

            Moo::new(into_matrix_expr!(decoded)),

            (low, high),

        );

    }

    if matches!(encoding, SATIntEncoding::SignMagnitude) {

        return Expr::SATInt(

            Metadata::new(),

            SATIntEncoding::Log,

            Moo::new(into_matrix_expr!(sign_magnitude_to_twos_complement(

                &bits, width, decisions, symbols

            ))),

            (low, high),

        );

    }

    let value_bits = match encoding {

        SATIntEncoding::Direct => bits,

        SATIntEncoding::Order => order_to_value_bits(&bits, decisions, symbols),

    let log_bits: Vec<Expr> = (0..width)

        .map(|index| {

            let terms: Vec<Expr> = value_bits

                .iter()

                .enumerate()

                .filter(|(offset, _)| ((low + *offset as i32) as u32) >> index & 1 == 1)

                .map(|(_, bit)| bit.clone())

            match terms.len() {

                0 => Expr::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(false))),

                1 => terms.into_iter().next().expect("just checked the length"),

                _ => tseytin_or(&terms, decisions, symbols),

        })

    Expr::SATInt(

        Metadata::new(),

        SATIntEncoding::Log,

        Moo::new(into_matrix_expr!(log_bits)),

        (low, high),

    )

}

fn ready_indicator(expr: &Expr) -> bool {

    matches!(expr, Expr::ToInt(_, input)

        if crate::shared::utils::is_literal(input)

            && input.domain_of().is_some_and(|domain| domain.is_bool()))

}

fn order_to_value_bits(

    thresholds: &[Expr],

    decisions: &mut Vec<SatEncodingDecision>,

    symbols: &mut SymbolTable,

) -> Vec<Expr> {

    thresholds

        .iter()

        .enumerate()

        .map(|(index, threshold)| match thresholds.get(index + 1) {

                let not_next = tseytin_not(next.clone(), decisions, symbols);

                tseytin_and(&[threshold.clone(), not_next], decisions, symbols)

            None => threshold.clone(),

        })

}

pub(super) fn sat_int_literal(encoding: &SATIntEncoding, value: i32) -> Expr {

    let bits = match encoding {

        SATIntEncoding::Log => log_literal_bits(value),

        SATIntEncoding::Offset | SATIntEncoding::Rank(_) => vec![false.into()],

        SATIntEncoding::SignMagnitude => sign_magnitude_literal_bits(value),

            vec![Expr::Atomic(

                Metadata::new(),

                Atom::Literal(Literal::Bool(true)),

            )]

        Metadata::new(),

        match encoding {

            SATIntEncoding::Rank(_) => SATIntEncoding::Rank(vec![(value, value)]),

            other => other.clone(),

        Moo::new(into_matrix_expr!(bits)),

        (value, value),

}

fn sign_magnitude_literal_bits(value: i32) -> Vec<Expr> {

    let magnitude = i64::from(value).unsigned_abs();

    let width = (64 - magnitude.leading_zeros()).max(1);

    let bit = |set: bool| Expr::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(set)));

    (0..width)

        .map(|index| bit((magnitude >> index) & 1 == 1))

        .chain(std::iter::once(bit(value < 0)))

}

fn sign_magnitude_to_twos_complement(

    bits: &[Expr],

    width: usize,

    decisions: &mut Vec<SatEncodingDecision>,

    symbols: &mut SymbolTable,

) -> Vec<Expr> {

    let (sign, magnitude) = bits.split_last().expect("a sign bit");

    let mut carry = sign.clone();

    let mut out = Vec::with_capacity(width);

    for index in 0..width {

        let flipped = match magnitude.get(index) {

            Some(bit) => tseytin_xor(bit.clone(), sign.clone(), decisions, symbols),

            None => sign.clone(),

        out.push(tseytin_xor(

            flipped.clone(),

            carry.clone(),

            decisions,

            symbols,

        ));

        carry = tseytin_and(&[flipped, carry], decisions, symbols);

    out

}

fn log_literal_bits(value: i32) -> Vec<Expr> {

    let mut remaining = value as u32;

    (0..bit_magnitude(value))

        .map(|_| {

            let bit = Expr::Atomic(

                Metadata::new(),

                Atom::Literal(Literal::Bool(remaining & 1 != 0)),

            );

            remaining >>= 1;

            bit

        })

}

fn encode_sat_int_literals(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

    let mut encoding = None;

    let mut has_literal = false;

    for operand in operands(expr) {

        match operand {

            Expr::SATInt(_, found, _, _) => encoding = encoding.or(Some(found)),

            Expr::Atomic(_, Atom::Literal(Literal::Int(_))) => has_literal = true,

            _ => {}

    let (Some(encoding), true) = (encoding, has_literal) else {

        return Err(RuleNotApplicable);

    let encode = |expr: Expr| match expr {

        Expr::Atomic(_, Atom::Literal(Literal::Int(value))) => sat_int_literal(&encoding, value),

        other => other,

    };

    let children: VecDeque<Expr> = expr

        .children()

        .into_iter()

        .map(|child| match matrix_child(&child) {

                rebuild_matrix_child(elements.into_iter().map(encode).collect(), index_domain)

            None => encode(child),

        })

    Ok(RuleEffect::pure(expr.with_children(children)))

}

fn add_unsigned_constant(

    bits: &[Expr],

    constant: i64,

    width: usize,

    decisions: &mut Vec<SatEncodingDecision>,

    symbols: &mut SymbolTable,

) -> Vec<Expr> {

    let mut carry: Expr = false.into();

    let mut out = Vec::with_capacity(width);

    for index in 0..width {

        let bit = bits.get(index).cloned().unwrap_or_else(|| false.into());

        let sum = tseytin_xor(bit.clone(), carry.clone(), decisions, symbols);

        if (constant as u32 >> index) & 1 == 1 {

            out.push(tseytin_not(sum, decisions, symbols));

            carry = tseytin_or(&[bit, carry], decisions, symbols);

            out.push(sum);

            carry = tseytin_and(&[bit, carry], decisions, symbols);

    out

}

fn unsigned_at_least(

    bits: &[Expr],

    minimum: u64,

    decisions: &mut Vec<SatEncodingDecision>,

    symbols: &mut SymbolTable,

) -> Expr {

    let maximum = minimum - 1;

    let mut leq: Expr = true.into();

    for (index, bit) in bits.iter().enumerate() {

        let not = tseytin_not(bit.clone(), decisions, symbols);

        leq = if (maximum >> index) & 1 == 1 {

            tseytin_or(&[not, leq], decisions, symbols)

            tseytin_and(&[not, leq], decisions, symbols)

    tseytin_not(leq, decisions, symbols)

}