Struct CSatTransformer

pub(crate) struct CSatTransformer<F: AcirField> {
    width: usize,
    solvable_witness: HashSet<Witness>,
    inverse_cache: HashMap<F, F>,
}

A transformer which slices Expressions 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; 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), not width.

Pre-Condition:

• General Optimizer must run before this pass

Fields

width: usize

solvable_witness: HashSet<Witness>

Track the witness that can be solved

inverse_cache: HashMap<F, F>

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.

Implementations

impl<F: AcirField> CSatTransformer<F>

pub(crate) fn new(width: usize) -> CSatTransformer<F>

Create an optimizer with a given width.

Panics if width is less than MIN_EXPRESSION_WIDTH.

fn try_solve(&mut self, opcode: &Expression<F>)

Check if the equation ‘expression=0’ can be solved, and if yes, add the solved witness to set of solvable witness

pub(crate) fn mark_solvable(&mut self, witness: Witness)

Adds the witness to set of solvable witness

pub(crate) fn transform( &mut self, opcode: Expression<F>, intermediate_variables: &mut IndexMap<Expression<F>, (F, Witness)>, num_witness: &mut u32, ) -> Expression<F>

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.

fn full_opcode_scan_optimization( &mut self, opcode: Expression<F>, intermediate_variables: &mut IndexMap<Expression<F>, (F, Witness)>, num_witness: &mut u32, ) -> Expression<F>

fn normalize(&mut self, expr: Expression<F>) -> (F, Expression<F>)

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 get_or_create_intermediate_var( &mut self, intermediate_variables: &mut IndexMap<Expression<F>, (F, Witness)>, expr: Expression<F>, num_witness: &mut u32, ) -> (F, Witness)

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 partial_opcode_scan_optimization( &mut self, opcode: Expression<F>, intermediate_variables: &mut IndexMap<Expression<F>, (F, Witness)>, num_witness: &mut u32, ) -> Expression<F>