Struct CSatTransformer

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

A transformer which processes any Expressions to break them up such that they fit within the backend’s width.

This transformer is only used when targeting the Bounded configuration.

This is done by creating intermediate variables to hold partial calculations and then combining them to calculate the original expression.

Pre-Condition:

• General Optimizer must run before this pass

Fields

width: usize

solvable_witness: HashSet<Witness>

Track the witness that can be solved

Implementations

impl CSatTransformer

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

Create an optimizer with a given width.

Panics if width is less than MIN_EXPRESSION_WIDTH.

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

Transform the input arithmetic expression into a new one having the correct ‘width’ by creating intermediate variables as needed. Having the correct width means:

• it has at most one multiplicative term
• it uses at most ‘width-1’ witness linear combination terms, to account for the new intermediate variable

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

fn normalize<F: AcirField>(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. The function panic if the input expression is constant

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