acvm/compiler/optimizers/common_subexpression/

csat.rs

use std::{
    cmp::Ordering,
    collections::{HashMap, HashSet},
};

use acir::{
    AcirField,
    native_types::{Expression, Witness},
};
use indexmap::IndexMap;

use crate::compiler::simulator::unresolved_witnesses;

/// Minimum width accepted by the `CSatTransformer`.
pub(crate) const MIN_EXPRESSION_WIDTH: usize = 3;

/// A transformer which slices [`Expression`]s towards the backend's preferred `width`, creating
/// intermediate variables to hold partial calculations and then combining them to recover the
/// original expression.
///
/// This is a sub-pass of the [`CommonSubexpressionOptimizer`](super); see the module documentation
/// for how the slices it produces become common-subexpression candidates.
///
/// `width` is a best-effort target, not a guarantee. ACIR places no upper bound on the width of an
/// opcode, so the transformer never splits an expression in a way that would harm solvability. In
/// particular, an emitted opcode may exceed `width` when it cannot be sliced further without becoming
/// unsolvable. The two cases are:
/// - The expression has more than one multiplication term whose operands are not all solvable: each
///   such term must stay in the opcode (an intermediate bound to it would be unsolvable), so several
///   may remain.
/// - The sole unknown of the expression sits inside a multiplication term (e.g. `w_known * y = a + b + c + d`,
///   solving for `y`). The term cannot be hoisted into an intermediate without leaving the opcode with two
///   unknowns, so the whole expression — multiplication term and all linear terms — is emitted as one opcode.
///
/// The property the transformer preserves is solvability (see [`CircuitSimulator`](crate::compiler::CircuitSimulator)),
/// not width.
///
/// Pre-Condition:
/// - General Optimizer must run before this pass
pub(crate) struct CSatTransformer<F: AcirField> {
    width: usize,
    /// Track the witness that can be solved
    solvable_witness: HashSet<Witness>,
    /// Cache of field-element inverses, used to normalize intermediate expressions.
    /// Coefficients repeat heavily across a circuit (e.g. constant matrices, powers of two),
    /// so memoizing avoids recomputing the same expensive modular inversion many times.
    inverse_cache: HashMap<F, F>,
}

impl<F: AcirField> CSatTransformer<F> {
    /// Create an optimizer with a given width.
    ///
    /// Panics if `width` is less than `MIN_EXPRESSION_WIDTH`.
    pub(crate) fn new(width: usize) -> CSatTransformer<F> {
        assert!(width >= MIN_EXPRESSION_WIDTH, "width has to be at least {MIN_EXPRESSION_WIDTH}");

        CSatTransformer { width, solvable_witness: HashSet::new(), inverse_cache: HashMap::new() }
    }

    /// Check if the equation 'expression=0' can be solved, and if yes, add the solved witness to set of solvable witness
    fn try_solve(&mut self, opcode: &Expression<F>) {
        if let Some(unresolved) = unresolved_witnesses(opcode, &self.solvable_witness)
            && unresolved.len() == 1
        {
            self.mark_solvable(*unresolved.iter().next().expect("len == 1"));
        }
    }

    /// Adds the witness to set of solvable witness
    pub(crate) fn mark_solvable(&mut self, witness: Witness) {
        self.solvable_witness.insert(witness);
    }

    /// Transform the input arithmetic expression by slicing it towards `self.width` via intermediate
    /// variables, marking the witness it solves for so later opcodes can reuse it.
    ///
    /// The intended shape of the returned opcode is:
    /// - at most one multiplication term, and
    /// - a fan-in whose [`Expression::width`] is at most `self.width`.
    ///
    /// This is best-effort, not guaranteed: when an unsolvable multiplication term cannot be hoisted
    /// into an intermediate variable, it (and the linear terms it sits alongside) remain in the opcode,
    /// which may then have more than one multiplication term and/or a width exceeding `self.width`. This
    /// is intentional — slicing such a term out would make the circuit unsolvable, and ACIR imposes no
    /// hard width limit. See the [`CSatTransformer`] documentation for details.
    ///
    /// The `width - 1` budget mentioned in the helper functions refers to each *intermediate* opcode:
    /// an intermediate reserves one wire for the variable it defines, so it can absorb at most `width - 1`
    /// source terms. The final opcode itself targets the full `self.width`.
    pub(crate) fn transform(
        &mut self,
        opcode: Expression<F>,
        intermediate_variables: &mut IndexMap<Expression<F>, (F, Witness)>,
        num_witness: &mut u32,
    ) -> Expression<F> {
        // Here we create intermediate variables and constrain them to be equal to any subset of the polynomial that can be represented as a full opcode
        let opcode =
            self.full_opcode_scan_optimization(opcode, intermediate_variables, num_witness);
        // The last optimization to do is to create intermediate variables in order to flatten the fan-in and the amount of mul terms
        // If a opcode has more than one mul term. We may need an intermediate variable for each one. Since not every variable will need to link to
        // the mul term, we could possibly do it that way.
        // We wil call this a partial opcode scan optimization which will result in the opcodes being able to fit into the correct width
        let mut opcode =
            self.partial_opcode_scan_optimization(opcode, intermediate_variables, num_witness);
        opcode.sort();
        self.try_solve(&opcode);
        opcode
    }

    // This optimization will search for combinations of terms which can be represented in a single assert-zero opcode
    // Case 1 : qM * wL * wR + qL * wL + qR * wR + qO * wO + qC
    // This polynomial does not require any further optimizations, it can be safely represented in one opcode
    // ie a polynomial with 1 mul(bi-variate) term and 3 (univariate) terms where 2 of those terms match the bivariate term
    // wL and wR, we can represent it in one opcode
    // GENERALIZED for WIDTH: instead of the number 3, we use `WIDTH`
    //
    //
    // Case 2: qM * wL * wR + qL * wL + qR * wR + qO * wO + qC + qM2 * wL2 * wR2 + qL * wL2 + qR * wR2 + qO * wO2 + qC2
    // This polynomial cannot be represented using one assert-zero opcode.
    //
    // This algorithm will first extract the first full opcode(if possible):
    // t = qM * wL * wR + qL * wL + qR * wR + qO * wO + qC
    //
    // The polynomial now looks like so t + qM2 * wL2 * wR2 + qL * wL2 + qR * wR2 + qO * wO2 + qC2
    // This polynomial cannot be represented using one assert-zero opcode.
    //
    // This algorithm will then extract the second full opcode(if possible):
    // t2 = qM2 * wL2 * wR2 + qL * wL2 + qR * wR2 + qO * wO2 + qC2
    //
    // The polynomial now looks like so t + t2
    // We can no longer extract another full opcode, hence the algorithm terminates. Creating two intermediate variables t and t2.
    // This stage of preprocessing does not guarantee that all polynomials can fit into a opcode. It only guarantees that all full opcodes have been extracted from each polynomial
    fn full_opcode_scan_optimization(
        &mut self,
        mut opcode: Expression<F>,
        intermediate_variables: &mut IndexMap<Expression<F>, (F, Witness)>,
        num_witness: &mut u32,
    ) -> Expression<F> {
        // We pass around this intermediate variable IndexMap, so that we do not create intermediate variables that we have created before
        // One instance where this might happen is t1 = wL * wR and t2 = wR * wL

        // First check that this is not a simple opcode which does not need optimization
        //
        // If the opcode only has one mul term, then this algorithm cannot optimize it any further
        // Either it can be represented in a single arithmetic equation or its fan-in is too large and we need intermediate variables for those
        // Large-fan-in optimization is not this algorithm's purpose.
        // If the opcode has 0 mul terms, then it is an add opcode and similarly it can either fit into a single assert-zero opcode or it has a large fan-in
        if opcode.mul_terms.len() <= 1 {
            return opcode;
        }

        // We now know that this opcode has multiple mul terms and can possibly be simplified into multiple full opcodes
        // We need to create a (w_l, w_r) IndexMap and then check the simplified fan-in to verify if we have terms both with w_l and w_r
        // In general, we can then push more terms into the opcode until we are at width-1 then the last variable will be the intermediate variable
        //

        // This will be our new opcode which will be equal to `self` except we will have intermediate variables that will be constrained to any
        // subset of the terms that can be represented as full opcodes
        let mut new_opcode = Expression::default();
        let mut remaining_mul_terms = Vec::with_capacity(opcode.mul_terms.len());
        for (scale, w_l, w_r) in opcode.mul_terms {
            // We want to layout solvable intermediate variables, if we cannot solve one of the witnesses
            // that means the intermediate opcode will not be immediately solvable
            if !self.solvable_witness.contains(&w_l) || !self.solvable_witness.contains(&w_r) {
                remaining_mul_terms.push((scale, w_l, w_r));
                continue;
            }

            // Check if this (scale, w_l, w_r) triple is present in the simplified fan-in
            // We are assuming that the fan-in/fan-out has been simplified.
            // Note this function is not public, and can only be called within the optimize method, so this guarantee will always hold
            let index_wl =
                opcode.linear_combinations.iter().position(|(_scale, witness)| *witness == w_l);
            let index_wr =
                opcode.linear_combinations.iter().position(|(_scale, witness)| *witness == w_r);

            match (index_wl, index_wr) {
                (None, _) | (_, None) => {
                    // This means that the polynomial does not contain both terms
                    // Just push the Qm term as it cannot form a full opcode
                    new_opcode.mul_terms.push((scale, w_l, w_r));
                }
                (Some(x), Some(y)) => {
                    // This means that we can form a full opcode with this Qm term

                    // First fetch the left and right wires which match the mul term
                    let left_wire_term = opcode.linear_combinations[x];
                    let right_wire_term = opcode.linear_combinations[y];

                    // Lets create an intermediate opcode to store this full opcode
                    //
                    let mut intermediate_opcode = Expression::default();
                    intermediate_opcode.mul_terms.push((scale, w_l, w_r));

                    // Add the left and right wires
                    intermediate_opcode.linear_combinations.push(left_wire_term);
                    intermediate_opcode.linear_combinations.push(right_wire_term);
                    // Remove the left and right wires so we do not re-add them
                    match x.cmp(&y) {
                        Ordering::Greater => {
                            opcode.linear_combinations.remove(x);
                            opcode.linear_combinations.remove(y);
                        }
                        Ordering::Less => {
                            opcode.linear_combinations.remove(y);
                            opcode.linear_combinations.remove(x);
                        }
                        Ordering::Equal => {
                            opcode.linear_combinations.remove(x);
                            intermediate_opcode.linear_combinations.pop();
                        }
                    }

                    let used_space = intermediate_opcode.linear_combinations.len();
                    assert!(used_space < self.width);

                    // Now we have used up "used_space" spaces in our assert-zero opcode. The width now dictates how many more we can add
                    let mut remaining_space = self.width - used_space - 1; // We minus 1 because we need an extra space to contain the intermediate variable
                    // Keep adding terms until we have no more left, or we reach the width
                    let mut remaining_linear_terms =
                        Vec::with_capacity(opcode.linear_combinations.len());
                    while remaining_space > 0 {
                        if let Some(wire_term) = opcode.linear_combinations.pop() {
                            // Add this element into the new opcode
                            if self.solvable_witness.contains(&wire_term.1) {
                                intermediate_opcode.linear_combinations.push(wire_term);
                                remaining_space -= 1;
                            } else {
                                remaining_linear_terms.push(wire_term);
                            }
                        } else {
                            // No more usable elements left in the old opcode
                            break;
                        }
                    }
                    opcode.linear_combinations.extend(remaining_linear_terms);

                    // Constrain this intermediate_opcode to be equal to the temp variable by adding it into the IndexMap
                    // We need a unique name for our intermediate variable
                    // TODO(https://github.com/noir-lang/noir/issues/10192): Another optimization, which could be applied in another algorithm
                    // If two opcodes have a large fan-in/out and they share a few common terms, then we should create intermediate variables for them
                    // Do some sort of subset matching algorithm for this on the terms of the polynomial
                    let intermediate_var = self.get_or_create_intermediate_var(
                        intermediate_variables,
                        intermediate_opcode,
                        num_witness,
                    );

                    // Add intermediate variable to the new opcode instead of the full opcode
                    self.mark_solvable(intermediate_var.1);
                    new_opcode.linear_combinations.push(intermediate_var);
                }
            }
        }

        // Add the rest of the elements back into the new_opcode
        new_opcode.mul_terms.extend(remaining_mul_terms);
        new_opcode.linear_combinations.extend(opcode.linear_combinations);
        new_opcode.q_c = opcode.q_c;
        new_opcode.sort();
        new_opcode
    }

    /// Normalize an expression by dividing it by its first coefficient
    /// The first coefficient here means coefficient of the first linear term, or of the first quadratic term if no linear terms exist.
    /// This function panics if the input expression is constant or if the first coefficient's inverse is `F::zero()`
    fn normalize(&mut self, mut expr: Expression<F>) -> (F, Expression<F>) {
        expr.sort();
        let a = if !expr.linear_combinations.is_empty() {
            expr.linear_combinations[0].0
        } else {
            expr.mul_terms[0].0
        };
        // The expression is already normalized when its leading coefficient is 1,
        // so we can skip the field inversion and the scaled copy entirely.
        if a == F::one() {
            return (a, expr);
        }
        // A leading coefficient of -1 normalizes to a plain negation.
        if a == -F::one() {
            return (a, -expr);
        }
        // Coefficients repeat heavily, so memoize the inverse to avoid recomputing it.
        let a_inverse = *self.inverse_cache.entry(a).or_insert_with(|| a.inverse());
        assert!(a_inverse != F::zero(), "normalize: the first coefficient is non-invertible");
        (a, expr * a_inverse)
    }

    /// Get or generate a scaled intermediate witness which is equal to the provided expression
    /// The sets of previously generated witness and their (normalized) expression is cached in the `intermediate_variables` map
    /// If there is no cache hit, we generate a new witness (and add the expression to the cache)
    /// else, we return the cached witness along with the scaling factor so it is equal to the provided expression
    fn get_or_create_intermediate_var(
        &mut self,
        intermediate_variables: &mut IndexMap<Expression<F>, (F, Witness)>,
        expr: Expression<F>,
        num_witness: &mut u32,
    ) -> (F, Witness) {
        let (k, normalized_expr) = self.normalize(expr);

        if intermediate_variables.contains_key(&normalized_expr) {
            let (l, iv) = intermediate_variables[&normalized_expr];
            assert!(
                l != F::zero(),
                "get_or_create_intermediate_var: attempting to divide l by F::zero()"
            );
            (k / l, iv)
        } else {
            let inter_var = Witness::new(*num_witness);
            *num_witness += 1;
            // Add intermediate opcode and variable to map
            intermediate_variables.insert(normalized_expr, (k, inter_var));
            (F::one(), inter_var)
        }
    }

    // A partial opcode scan optimization aim to create intermediate variables in order to compress the polynomial
    // So that it fits within the given width
    // Note that this opcode follows the full opcode scan optimization.
    // We define the partial width as equal to the full width - 2.
    // This is because two of our variables cannot be used as they are linked to the multiplication terms
    // Example: qM1 * wL1 * wR2 + qL1 * wL3 + qR1 * wR4+ qR2 * wR5 + qO1 * wO5 + qC
    // One thing to note is that the multiplication wires do not match any of the fan-in/out wires. This is guaranteed as we have
    // just completed the full opcode optimization algorithm.
    //
    // Actually we can optimize in two ways here: We can create an intermediate variable which is equal to the fan-in terms
    // t = qL1 * wL3 + qR1 * wR4 -> width = 3
    // This `t` value can only use width - 1 terms
    // The opcode now looks like: qM1 * wL1 * wR2 + t + qR2 * wR5+ qO1 * wO5 + qC
    // But this is still not acceptable since wR5 is not wR2, so we need another intermediate variable
    // t2 = t + qR2 * wR5
    //
    // The opcode now looks like: qM1 * wL1 * wR2 + t2 + qO1 * wO5 + qC
    // This is still not good, so we do it one more time:
    // t3 = t2 + qO1 * wO5
    // The opcode now looks like: qM1 * wL1 * wR2 + t3 + qC
    //
    // Another strategy is to create a temporary variable for the multiplier term and then we can see it as a term in the fan-in
    //
    // Same Example: qM1 * wL1 * wR2 + qL1 * wL3 + qR1 * wR4+ qR2 * wR5 + qO1 * wO5 + qC
    // t = qM1 * wL1 * wR2
    // The opcode now looks like: t + qL1 * wL3 + qR1 * wR4+ qR2 * wR5 + qO1 * wO5 + qC
    // Still assuming width-3, we still need to use width-1 terms for the intermediate variables, however we can stop at an earlier stage because
    // the opcode does not need the multiplier term to match with any of the fan-in terms
    // t2 = t + qL1 * wL3
    // The opcode now looks like: t2 + qR1 * wR4+ qR2 * wR5 + qO1 * wO5 + qC
    // t3 = t2 + qR1 * wR4
    // The opcode now looks like: t3 + qR2 * wR5 + qO1 * wO5 + qC
    // This took the same amount of opcodes, but which one is better when the width increases? Compute this and maybe do both optimizations
    // naming : partial_opcode_mul_first_opt and partial_opcode_fan_first_opt
    // Also remember that since we did full opcode scan, there is no way we can have a non-zero mul term along with the wL and wR terms being non-zero
    //
    // Cases, a lot of mul terms, a lot of fan-in terms, 50/50
    fn partial_opcode_scan_optimization(
        &mut self,
        mut opcode: Expression<F>,
        intermediate_variables: &mut IndexMap<Expression<F>, (F, Witness)>,
        num_witness: &mut u32,
    ) -> Expression<F> {
        // We will go for the easiest route, which is to convert all multiplications into additions using intermediate variables
        // Then use intermediate variables again to squash the fan-in, so that it can fit into the appropriate width

        // First check if this polynomial actually needs a partial opcode optimization
        // There is the chance that it fits perfectly within the assert-zero opcode
        if fits_in_one_identity(&opcode, self.width) {
            return opcode;
        }

        // Replace each multiplication term with an intermediate variable, so it becomes a single linear
        // term in the fan-in. We can only do this for terms whose operands are both solvable: an intermediate
        // bound to an unsolvable multiplication term would itself be unsolvable. Unsolvable terms are kept in
        // the opcode unchanged.
        let mut remaining_mul_terms = Vec::with_capacity(opcode.mul_terms.len());
        for (scale, w_l, w_r) in opcode.mul_terms {
            if self.solvable_witness.contains(&w_l) && self.solvable_witness.contains(&w_r) {
                let mut intermediate_opcode = Expression::default();

                // Push mul term into the opcode
                intermediate_opcode.mul_terms.push((scale, w_l, w_r));
                // Get an intermediate variable which squashes the multiplication term
                let intermediate_var = self.get_or_create_intermediate_var(
                    intermediate_variables,
                    intermediate_opcode,
                    num_witness,
                );

                // Add intermediate variable as a part of the fan-in for the original opcode
                opcode.linear_combinations.push(intermediate_var);
                self.mark_solvable(intermediate_var.1);
            } else {
                remaining_mul_terms.push((scale, w_l, w_r));
            }
        }

        // Any multiplication terms left here are unsolvable and could not be hoisted into intermediates.
        opcode.mul_terms = remaining_mul_terms;

        // The remaining work is to squash the linear fan-in down to `self.width` terms. We can only stop once
        // the linear fan-in fits; any residual unsolvable multiplication terms stay where they are, so the
        // final opcode's `width()` may still exceed `self.width`. That is acceptable (ACIR has no width limit)
        // and unavoidable — slicing those terms out would make the circuit unsolvable.
        if opcode.linear_combinations.len() <= self.width {
            return opcode;
        }

        // Stores the intermediate variables that are used to
        // reduce the fan in.
        let mut added_vars = Vec::new();

        while opcode.linear_combinations.len() > self.width {
            // Collect as many terms up to the given width-1 and constrain them to an intermediate variable
            let mut intermediate_opcode = Expression::default();

            let mut remaining_linear_terms = Vec::with_capacity(opcode.linear_combinations.len());

            for term in opcode.linear_combinations {
                if self.solvable_witness.contains(&term.1)
                    && intermediate_opcode.linear_combinations.len() < self.width - 1
                {
                    intermediate_opcode.linear_combinations.push(term);
                } else {
                    remaining_linear_terms.push(term);
                }
            }
            opcode.linear_combinations = remaining_linear_terms;
            let not_full = intermediate_opcode.linear_combinations.len() < self.width - 1;
            if intermediate_opcode.linear_combinations.len() > 1 {
                let intermediate_var = self.get_or_create_intermediate_var(
                    intermediate_variables,
                    intermediate_opcode,
                    num_witness,
                );
                self.mark_solvable(intermediate_var.1);
                added_vars.push(intermediate_var);
            } else {
                // Put back the single term that couldn't form an intermediate variable
                opcode.linear_combinations.extend(intermediate_opcode.linear_combinations);
            }
            // The intermediate opcode is not full, but the opcode still has too many terms
            if not_full && opcode.linear_combinations.len() > self.width {
                unreachable!("Could not reduce the expression");
            }
        }

        // Add back the intermediate variables to
        // keep consistency with the original equation.
        opcode.linear_combinations.extend(added_vars);
        self.partial_opcode_scan_optimization(opcode, intermediate_variables, num_witness)
    }
}

/// Checks if this expression can fit into one arithmetic identity
fn fits_in_one_identity<F: AcirField>(expr: &Expression<F>, width: usize) -> bool {
    // A Polynomial with more than one mul term cannot fit into one opcode
    if expr.mul_terms.len() > 1 {
        return false;
    }

    expr.width() <= width
}

#[cfg(test)]
mod tests {
    use super::*;
    use acir::FieldElement;

    #[test]
    fn simple_reduction_smoke_test() {
        let a = Witness(0);
        let b = Witness(1);
        let c = Witness(2);
        let d = Witness(3);

        // a = b + c + d;
        let opcode_a = Expression::from_str(&format!("{a} - {b} - {c} - {d}")).unwrap();

        let mut intermediate_variables: IndexMap<
            Expression<FieldElement>,
            (FieldElement, Witness),
        > = IndexMap::new();

        let mut num_witness = 4;

        let mut optimizer = CSatTransformer::new(MIN_EXPRESSION_WIDTH);
        optimizer.mark_solvable(b);
        optimizer.mark_solvable(c);
        optimizer.mark_solvable(d);
        let got_optimized_opcode_a =
            optimizer.transform(opcode_a, &mut intermediate_variables, &mut num_witness);

        // a = b + c + d => a - b - c - d = 0
        // For width3, the result becomes:
        // a - d + e = 0
        // - c - b  - e = 0
        //
        // a - b + e = 0
        let e = Witness(4);
        let expected_optimized_opcode_a =
            Expression::from_str(&format!("{a} - {d} + {e}")).unwrap();

        assert_eq!(expected_optimized_opcode_a, got_optimized_opcode_a);

        assert_eq!(intermediate_variables.len(), 1);

        // e = - c - b
        let expected_intermediate_opcode = Expression::from_str(&format!("-{c} - {b}")).unwrap();
        let (_, normalized_opcode) =
            CSatTransformer::new(MIN_EXPRESSION_WIDTH).normalize(expected_intermediate_opcode);
        assert!(intermediate_variables.contains_key(&normalized_opcode));
        assert_eq!(intermediate_variables[&normalized_opcode].1, e);
    }

    #[test]
    fn stepwise_reduction_test() {
        let a = Witness(0);
        let b = Witness(1);
        let c = Witness(2);
        let d = Witness(3);
        let e = Witness(4);

        // a = b + c + d + e;
        let opcode_a = Expression::from_str(&format!("-{a} + {b} + {c} + {d} + {e}")).unwrap();

        let mut intermediate_variables: IndexMap<
            Expression<FieldElement>,
            (FieldElement, Witness),
        > = IndexMap::new();

        let mut num_witness = 4;

        let mut optimizer = CSatTransformer::new(MIN_EXPRESSION_WIDTH);
        optimizer.mark_solvable(a);
        optimizer.mark_solvable(c);
        optimizer.mark_solvable(d);
        optimizer.mark_solvable(e);
        let got_optimized_opcode_a =
            optimizer.transform(opcode_a, &mut intermediate_variables, &mut num_witness);

        // Since b is not known, it cannot be put inside intermediate opcodes, so it must belong to the transformed opcode.
        let contains_b = got_optimized_opcode_a.linear_combinations.iter().any(|(_, w)| *w == b);
        assert!(contains_b);
    }

    #[test]
    fn recognize_expr_with_single_shared_witness_which_fits_in_single_identity() {
        // Regression test for an expression which Zac found which should have been preserved but
        // was being split into two expressions.
        let expr = Expression::from_str("-555*w8*w10 + w10 + w11 - w13").unwrap();
        assert!(fits_in_one_identity(&expr, 4));
    }

    #[test]
    #[should_panic(expected = "normalize: the first coefficient is non-invertible")]
    fn normalize_on_zero_linear_combination_panics() {
        let expr = Expression {
            mul_terms: vec![],
            linear_combinations: vec![(FieldElement::zero(), Witness(0))],
            q_c: FieldElement::zero(),
        };
        CSatTransformer::new(MIN_EXPRESSION_WIDTH).normalize(expr);
    }

    #[test]
    #[should_panic(expected = "normalize: the first coefficient is non-invertible")]
    fn normalize_on_zero_mul_term_scale_panics() {
        let expr = Expression {
            mul_terms: vec![(FieldElement::zero(), Witness(0), Witness(1))],
            linear_combinations: vec![],
            q_c: FieldElement::zero(),
        };
        CSatTransformer::new(MIN_EXPRESSION_WIDTH).normalize(expr);
    }

    #[test]
    #[should_panic(
        expected = "get_or_create_intermediate_var: attempting to divide l by F::zero()"
    )]
    fn get_or_create_intermediate_var_with_zero_panics() {
        let expr = Expression {
            mul_terms: vec![(FieldElement::one(), Witness(0), Witness(1))],
            linear_combinations: vec![],
            q_c: FieldElement::zero(),
        };

        let mut intermediate_variables = IndexMap::new();
        intermediate_variables.insert(expr.clone(), (FieldElement::zero(), Witness(0)));

        let mut num_witness = 2;

        let mut optimizer = CSatTransformer::new(MIN_EXPRESSION_WIDTH);
        optimizer.get_or_create_intermediate_var(
            &mut intermediate_variables,
            expr,
            &mut num_witness,
        );
    }

    #[test]
    fn full_opcode_scan_optimization_extracts_full_opcodes() {
        // Expression: x*x + a*b + x + a + b + c + d + e + f + g
        //
        // With width=3 and two mul terms, full_opcode_scan_optimization extracts each
        // mul term together with 2 linear terms into an intermediate variable:
        //   t0 = x*x + x + g      (Witness 8)
        //   t1 = a*b + a + b      (Witness 9)
        //
        // The remaining expression becomes: t0 + t1 + c + d + e + f
        let x = Witness(0);
        let a = Witness(1);
        let b = Witness(2);
        let c = Witness(3);
        let d = Witness(4);
        let e = Witness(5);
        let f = Witness(6);
        let g = Witness(7);

        let opcode = Expression {
            mul_terms: vec![(FieldElement::one(), x, x), (FieldElement::one(), a, b)],
            linear_combinations: vec![
                (FieldElement::one(), x),
                (FieldElement::one(), a),
                (FieldElement::one(), b),
                (FieldElement::one(), c),
                (FieldElement::one(), d),
                (FieldElement::one(), e),
                (FieldElement::one(), f),
                (FieldElement::one(), g),
            ],
            q_c: FieldElement::zero(),
        };

        let mut intermediate_variables: IndexMap<
            Expression<FieldElement>,
            (FieldElement, Witness),
        > = IndexMap::new();
        let mut num_witness = 8u32;

        let mut optimizer = CSatTransformer::new(MIN_EXPRESSION_WIDTH);
        for w in [x, a, b, c, d, e, f, g] {
            optimizer.mark_solvable(w);
        }

        let result = optimizer.full_opcode_scan_optimization(
            opcode,
            &mut intermediate_variables,
            &mut num_witness,
        );

        // Both mul terms were replaced by intermediate variables; no mul terms remain.
        assert!(result.mul_terms.is_empty(), "all mul terms should be absorbed");

        // Each intermediate variable is full: it has 2 linear terms.
        for intermediate in intermediate_variables.keys() {
            assert!(
                intermediate.mul_terms.len() == 1,
                "intermediate variables should be full opcodes"
            );
            assert!(
                intermediate.linear_combinations.len() == 2,
                "intermediate variables should be full opcodes"
            );
        }
        // Remaining linear terms: c, d, e, f+ t0, t1 (intermediate vars).
        assert_eq!(result.linear_combinations.len(), 6);
    }

    #[test]
    #[should_panic(expected = "Could not reduce the expression")]
    fn single_solvable_term_in_intermediate_opcode_is_preserved() {
        // Test the case when len() is 1 in the line: 'if intermediate_opcode.linear_combinations.len() > 1 {'
        // Setup: width is 3, 4 terms [a, b, c, d], only 'a' is solvable.
        //
        // Because only 'a' is solvable, the intermediate_opcode will be [a], so its len is 1.
        // In this case, 'a' should be added back to the opcode which makes it larger than the width and trigger the panic.

        let a = Witness(0); // solvable
        let b = Witness(1); // unsolvable
        let c = Witness(2); // unsolvable
        let d = Witness(3); // unsolvable

        let opcode = Expression {
            mul_terms: vec![],
            linear_combinations: vec![
                (FieldElement::one(), a),
                (FieldElement::one(), b),
                (FieldElement::one(), c),
                (FieldElement::one(), d),
            ],
            q_c: FieldElement::zero(),
        };

        let mut intermediate_variables: IndexMap<
            Expression<FieldElement>,
            (FieldElement, Witness),
        > = IndexMap::new();

        let mut num_witness = 4;

        let mut optimizer = CSatTransformer::new(MIN_EXPRESSION_WIDTH);
        optimizer.mark_solvable(a);

        let _ = optimizer.transform(opcode, &mut intermediate_variables, &mut num_witness);
    }
}