diff --git a/autoprecompiles/src/bitwise_lookup_optimizer.rs b/autoprecompiles/src/bitwise_lookup_optimizer.rs index 827b56c9f..0978c0bf9 100644 --- a/autoprecompiles/src/bitwise_lookup_optimizer.rs +++ b/autoprecompiles/src/bitwise_lookup_optimizer.rs @@ -108,7 +108,9 @@ pub fn optimize_bitwise_lookup( // does not increase. assert!(assignments.iter().all(|(_, expr)| expr.is_affine())); constraint_system.apply_substitutions(assignments); + + // Now try to replace bus interaction fields that the solver knows to be constant + let mut bus_interactions = vec![]; + let mut new_algebraic_constraints = vec![]; + // We remove all bus interactions because we do not want to change the order. + constraint_system.retain_bus_interactions(|bus_interaction| { + let mut modified = false; + let replacement = bus_interaction + .fields() + .map(|field| { + if let Some(n) = try_replace_by_number(field, solver) { + modified = true; + new_algebraic_constraints.push(&n - field); + n + } else { + field.clone() + } + }) + .collect(); + if modified { + log::trace!("Replacing bus interaction {bus_interaction} with {replacement}"); + } + bus_interactions.push(replacement); + false + }); + constraint_system.add_bus_interactions(bus_interactions); + constraint_system.add_algebraic_constraints(new_algebraic_constraints); Ok(constraint_system) } +/// Tries to find a number that is equivalent to the expression and returns it +/// as a GroupedExpression. +/// Returns None if it was unsuccessful or if the expression already is a number. +fn try_replace_by_number( + expr: &GroupedExpression, + solver: &impl Solver, +) -> Option> { + if expr.try_to_number().is_some() { + return None; + } + Some(GroupedExpression::from_number( + solver + .range_constraint_for_expression(expr) + .try_to_single_value()?, + )) +} + /// Removes free variables from the constraint system, under some conditions. /// /// Motivation: Suppose there is a constraint `2 * foo = bar` and `foo` only appears in this constraint. diff --git a/autoprecompiles/src/low_degree_bus_interaction_optimizer.rs b/autoprecompiles/src/low_degree_bus_interaction_optimizer.rs index 9ced8e996..11f594dfc 100644 --- a/autoprecompiles/src/low_degree_bus_interaction_optimizer.rs +++ b/autoprecompiles/src/low_degree_bus_interaction_optimizer.rs @@ -1,4 +1,5 @@ use itertools::Itertools; +use num_traits::Zero; use powdr_constraint_solver::constraint_system::{ BusInteraction, BusInteractionHandler, ConstraintSystem, }; @@ -51,10 +52,13 @@ impl< if let Some((replacement, range_constraints)) = self.try_replace_bus_interaction(&bus_int) { - // If we found a replacement, add the polynomial constraints and replace - // the bus interaction with interactions implementing the range constraints. + // If we found a replacement, add the polynomial constraints (unless it is + // trivially zero) and replace the bus interaction with interactions implementing + // the range constraints. // Note that many of these may be optimized away by the range constraint optimizer. - new_constraints.push(replacement); + if !replacement.is_zero() { + new_constraints.push(replacement); + } self.bus_interaction_handler .batch_make_range_constraints(range_constraints) diff --git a/autoprecompiles/src/optimizer.rs b/autoprecompiles/src/optimizer.rs index 60d384f75..a86f88e41 100644 --- a/autoprecompiles/src/optimizer.rs +++ b/autoprecompiles/src/optimizer.rs @@ -3,19 +3,14 @@ use std::hash::Hash; use std::{collections::BTreeMap, fmt::Display}; use itertools::Itertools; -use num_traits::Zero; use powdr_constraint_solver::constraint_system::BusInteractionHandler; -use powdr_constraint_solver::indexed_constraint_system::{ - apply_substitutions, IndexedConstraintSystem, -}; +use powdr_constraint_solver::indexed_constraint_system::IndexedConstraintSystem; use powdr_constraint_solver::inliner::inline_everything_below_degree_bound; -use powdr_constraint_solver::runtime_constant::RuntimeConstant; use powdr_constraint_solver::solver::{new_solver, Solver}; use powdr_constraint_solver::{ constraint_system::{BusInteraction, ConstraintSystem}, grouped_expression::GroupedExpression, journaling_constraint_system::JournalingConstraintSystem, - runtime_constant::VarTransformable, }; use powdr_number::FieldElement; @@ -49,22 +44,6 @@ pub fn optimize( } let constraint_system = symbolic_machine_to_constraint_system(machine); - let constraint_system = introduce_bus_interaction_variables(constraint_system); - - // Run the optimizer while avoiding inlining bus interaction field variables - let constraint_system = - run_optimization_loop_until_no_change::<_, _, _, A::MemoryBusInteraction<_>>( - constraint_system, - bus_interaction_handler.clone(), - only_inline_degree_one_and_no_bus_field_vars, - &mut stats_logger, - bus_map, - degree_bound, - )?; - - // Now remove the bus interaction field variables and run the optimizer, - // allowing all inlining below the degree bound. - let constraint_system = remove_bus_interaction_variables(constraint_system); let constraint_system = run_optimization_loop_until_no_change::<_, _, _, A::MemoryBusInteraction<_>>( constraint_system, @@ -117,24 +96,6 @@ pub fn optimize( Ok(constraint_system_to_symbolic_machine(constraint_system)) } -/// Inlining discriminator that prevents the inliner from inlining -/// bus interaction field variables (unless they are replaced -/// by a single other variable) and variables defined via bus interaction -/// field variables. All other variables are inlined if the expression has degree at most one. -fn only_inline_degree_one_and_no_bus_field_vars( - var: &Variable, - expr: &GroupedExpression>, - _constraint_system: &IndexedConstraintSystem>, -) -> bool { - let is_about_bus_field_var = (matches!(var, Variable::BusInteractionField(_, _)) - && expr.try_to_simple_unknown().is_none()) - || expr - .referenced_unknown_variables() - .any(|v| matches!(v, Variable::BusInteractionField(_, _))); - // and only inline if the degree is at most 1. - !is_about_bus_field_var && expr.degree() <= 1 -} - fn run_optimization_loop_until_no_change< P: FieldElement, V: Ord + Clone + Eq + Hash + Debug + Display, @@ -395,112 +356,3 @@ impl Display for Variable { } } } - -/// Transform the variable type of a constraint system by introducing -/// new variables for bus interaction fields. -fn introduce_bus_interaction_variables( - constraint_system: ConstraintSystem, -) -> ConstraintSystem> { - let mut new_constraints = Vec::new(); - let mut bus_interaction_vars = BTreeMap::new(); - let bus_interactions = constraint_system - .bus_interactions - .iter() - .enumerate() - .map(|(bus_interaction_index, bus_interaction)| { - BusInteraction::from_iter(bus_interaction.fields().enumerate().map( - |(field_index, expr)| { - let transformed_expr = - expr.transform_var_type(&mut |v| Variable::Variable(v.clone())); - if transformed_expr.is_affine() - && transformed_expr.referenced_unknown_variables().count() <= 1 - { - transformed_expr - } else { - let v = Variable::BusInteractionField(bus_interaction_index, field_index); - new_constraints.push( - transformed_expr - GroupedExpression::from_unknown_variable(v.clone()), - ); - bus_interaction_vars.insert(v.clone(), expr.clone()); - GroupedExpression::from_unknown_variable(v) - } - }, - )) - }) - .collect(); - ConstraintSystem { - algebraic_constraints: constraint_system - .algebraic_constraints - .iter() - .map(|expr| expr.transform_var_type(&mut |v| Variable::Variable(v.clone()))) - .chain(new_constraints) - .collect(), - bus_interactions, - } -} - -/// Reverses the effect of `introduce_bus_interaction_variables`, by inlining bus interaction -/// field variables. This might fail in some cases. -fn remove_bus_interaction_variables( - constraint_system: ConstraintSystem>, -) -> ConstraintSystem { - let bus_interaction_var_definitions = constraint_system - .algebraic_constraints - .iter() - .flat_map(|expr| try_solve_for_single_bus_interaction_variable(expr)) - .into_grouping_map() - .min_by_key(|_, expr| expr.degree()); - let substituted_system = apply_substitutions( - constraint_system, - bus_interaction_var_definitions - .into_iter() - .sorted_by_key(|(var, _)| var.clone()), - ); - ConstraintSystem { - algebraic_constraints: substituted_system - .algebraic_constraints - .into_iter() - .map(|expr| expr.transform_var_type(&mut transform_to_original_variable)) - .filter(|expr| expr != &Zero::zero()) - .collect(), - bus_interactions: substituted_system - .bus_interactions - .into_iter() - .map(|bi| { - BusInteraction::from_iter( - bi.fields() - .map(|expr| expr.transform_var_type(&mut transform_to_original_variable)), - ) - }) - .collect(), - } -} - -fn transform_to_original_variable(v: &Variable) -> V { - match v { - Variable::Variable(v) => v.clone(), - Variable::BusInteractionField(_, _) => { - panic!("Unexpected bus interaction field in transformation to original variable") - } - } -} - -/// Returns `Some(var, expr)` if `constraint` is equivalent to `var = expr` -/// and `var` is the only bus interaction variable in `constraint`. -#[allow(clippy::type_complexity)] -fn try_solve_for_single_bus_interaction_variable< - T: FieldElement, - V: Clone + Ord + Hash + Eq + Display, ->( - constraint: &GroupedExpression>, -) -> Option<(Variable, GroupedExpression>)> { - let var = constraint - .referenced_unknown_variables() - .filter(|var| matches!(var, Variable::BusInteractionField(_, _))) - .unique() - .exactly_one() - .ok()? - .clone(); - let solution = constraint.try_solve_for(&var)?; - Some((var, solution)) -} diff --git a/constraint-solver/src/indexed_constraint_system.rs b/constraint-solver/src/indexed_constraint_system.rs index f9e5bab84..dc026b632 100644 --- a/constraint-solver/src/indexed_constraint_system.rs +++ b/constraint-solver/src/indexed_constraint_system.rs @@ -217,7 +217,7 @@ fn retain( occurrences.retain(|_, occurrences| !occurrences.is_empty()); } -impl IndexedConstraintSystem { +impl IndexedConstraintSystem { /// Adds new algebraic constraints to the system. pub fn add_algebraic_constraints( &mut self, diff --git a/constraint-solver/src/journaling_constraint_system.rs b/constraint-solver/src/journaling_constraint_system.rs index ce0d60edc..1551bdeb0 100644 --- a/constraint-solver/src/journaling_constraint_system.rs +++ b/constraint-solver/src/journaling_constraint_system.rs @@ -68,6 +68,24 @@ impl, V: Ord + Clone + Eq + Hash + Display } } +impl JournalingConstraintSystem { + /// Adds new algebraic constraints to the system. + pub fn add_algebraic_constraints( + &mut self, + constraints: impl IntoIterator>, + ) { + self.system.add_algebraic_constraints(constraints); + } + + /// Adds new bus interactions to the system. + pub fn add_bus_interactions( + &mut self, + bus_interactions: impl IntoIterator>>, + ) { + self.system.add_bus_interactions(bus_interactions); + } +} + impl JournalingConstraintSystem { /// Removes all algebraic constraints that do not fulfill the predicate. pub fn retain_algebraic_constraints( diff --git a/constraint-solver/src/solver/base.rs b/constraint-solver/src/solver/base.rs index 4020dc5fb..4875c1591 100644 --- a/constraint-solver/src/solver/base.rs +++ b/constraint-solver/src/solver/base.rs @@ -1,4 +1,5 @@ use itertools::Itertools; +use num_traits::Zero; use powdr_number::{ExpressionConvertible, FieldElement}; use crate::constraint_system::{BusInteraction, BusInteractionHandler, ConstraintRef}; @@ -84,7 +85,7 @@ where ) { self.equivalent_expressions_cache.clear(); self.constraint_system - .add_algebraic_constraints(constraints); + .add_algebraic_constraints(constraints.into_iter().filter(|c| !c.is_zero())); } fn add_bus_interactions( diff --git a/openvm/src/lib.rs b/openvm/src/lib.rs index c12f0a30b..a560b5d0d 100644 --- a/openvm/src/lib.rs +++ b/openvm/src/lib.rs @@ -1670,7 +1670,7 @@ mod tests { main: 16416, log_up: 26292, }, - constraints: 9752, + constraints: 9132, bus_interactions: 11135, } "#]], diff --git a/openvm/tests/apc_builder_outputs/single_storeb.txt b/openvm/tests/apc_builder_outputs/single_storeb.txt index 85e1a023a..8550e4ef4 100644 --- a/openvm/tests/apc_builder_outputs/single_storeb.txt +++ b/openvm/tests/apc_builder_outputs/single_storeb.txt @@ -74,5 +74,5 @@ flags__3_0 * ((flags__3_0 - 1) * (flags__3_0 - 2)) = 0 (30720 * mem_ptr_limbs__0_0 - (30720 * rs1_data__0_0 + 7864320 * rs1_data__1_0 + 92160 * is_valid)) * (30720 * mem_ptr_limbs__0_0 - (30720 * rs1_data__0_0 + 7864320 * rs1_data__1_0 + 92161)) = 0 (943718400 * rs1_data__0_0 + 30720 * mem_ptr_limbs__1_0 + 817889279 * is_valid - (120 * rs1_data__1_0 + 30720 * rs1_data__2_0 + 7864320 * rs1_data__3_0 + 943718400 * mem_ptr_limbs__0_0)) * (943718400 * rs1_data__0_0 + 30720 * mem_ptr_limbs__1_0 + 817889278 - (120 * rs1_data__1_0 + 30720 * rs1_data__2_0 + 7864320 * rs1_data__3_0 + 943718400 * mem_ptr_limbs__0_0)) = 0 flags__1_0 * (flags__1_0 - 1) + flags__2_0 * (flags__2_0 - 1) + 4 * flags__0_0 * flags__1_0 + 4 * flags__0_0 * flags__2_0 + 5 * flags__0_0 * flags__3_0 + 5 * flags__1_0 * flags__2_0 + 5 * flags__1_0 * flags__3_0 + 5 * flags__2_0 * flags__3_0 - (1006632960 * flags__3_0 * (flags__3_0 - 1) + flags__0_0 * (flags__0_0 + flags__1_0 + flags__2_0 + flags__3_0 - 2) + flags__1_0 * (flags__0_0 + flags__1_0 + flags__2_0 + flags__3_0 - 2) + flags__2_0 * (flags__0_0 + flags__1_0 + flags__2_0 + flags__3_0 - 2) + 3 * flags__3_0 * (flags__0_0 + flags__1_0 + flags__2_0 + flags__3_0 - 2) + 5 * is_valid) = 0 -flags__0_0 * (flags__0_0 + flags__1_0 + flags__2_0 + flags__3_0 - 2) + 2 * flags__1_0 * (flags__0_0 + flags__1_0 + flags__2_0 + flags__3_0 - 2) + 3 * flags__2_0 * (flags__0_0 + flags__1_0 + flags__2_0 + flags__3_0 - 2) - flags__2_0 * (flags__2_0 - 1) = 0 +flags__2_0 * (flags__2_0 - 1) - (flags__0_0 * (flags__0_0 + flags__1_0 + flags__2_0 + flags__3_0 - 2) + 2 * flags__1_0 * (flags__0_0 + flags__1_0 + flags__2_0 + flags__3_0 - 2) + 3 * flags__2_0 * (flags__0_0 + flags__1_0 + flags__2_0 + flags__3_0 - 2)) = 0 is_valid * (is_valid - 1) = 0 \ No newline at end of file diff --git a/openvm/tests/apc_builder_outputs/single_storeh.txt b/openvm/tests/apc_builder_outputs/single_storeh.txt index 3b899ee25..081bad1be 100644 --- a/openvm/tests/apc_builder_outputs/single_storeh.txt +++ b/openvm/tests/apc_builder_outputs/single_storeh.txt @@ -70,5 +70,5 @@ write_data__3_0 - (flags__2_0 * read_data__1_0 + (flags__1_0 * flags__2_0 + flag (30720 * mem_ptr_limbs__0_0 - (30720 * rs1_data__0_0 + 7864320 * rs1_data__1_0 + 184320 * is_valid)) * (30720 * mem_ptr_limbs__0_0 - (30720 * rs1_data__0_0 + 7864320 * rs1_data__1_0 + 184321)) = 0 (943718400 * rs1_data__0_0 + 30720 * mem_ptr_limbs__1_0 - (120 * rs1_data__1_0 + 30720 * rs1_data__2_0 + 7864320 * rs1_data__3_0 + 943718400 * mem_ptr_limbs__0_0 + 377456642 * is_valid)) * (943718400 * rs1_data__0_0 + 30720 * mem_ptr_limbs__1_0 - (120 * rs1_data__1_0 + 30720 * rs1_data__2_0 + 7864320 * rs1_data__3_0 + 943718400 * mem_ptr_limbs__0_0 + 377456643)) = 0 flags__1_0 * (flags__1_0 - 1) + flags__2_0 * (flags__2_0 - 1) + 5 * flags__1_0 * flags__2_0 + 3 * flags__1_0 + 3 * flags__2_0 - (flags__1_0 * (flags__1_0 + flags__2_0 - 1) + flags__2_0 * (flags__1_0 + flags__2_0 - 1) + 3 * is_valid) = 0 -2 * flags__1_0 * (flags__1_0 + flags__2_0 - 1) + 3 * flags__2_0 * (flags__1_0 + flags__2_0 - 1) + flags__1_0 + flags__2_0 - (flags__2_0 * (flags__2_0 - 1) + 1 * is_valid) = 0 +flags__2_0 * (flags__2_0 - 1) + 1 * is_valid - (2 * flags__1_0 * (flags__1_0 + flags__2_0 - 1) + 3 * flags__2_0 * (flags__1_0 + flags__2_0 - 1) + flags__1_0 + flags__2_0) = 0 is_valid * (is_valid - 1) = 0 \ No newline at end of file