@@ -434,15 +434,18 @@ pub fn build<A: Adapter>(
434434 let range_constraints = & execution_stats. column_ranges_by_pc ;
435435 let equivalence_classes_by_block = & execution_stats. equivalence_classes_by_block ;
436436
437- // Mapping (instruction index, column index) -> AlgebraicReference
437+ // Mapping (pc index, column index) -> AlgebraicReference
438438 let reverse_subs = column_allocator
439439 . subs
440440 . iter ( )
441441 . enumerate ( )
442442 . flat_map ( |( instr_index, subs) | {
443- subs. iter ( )
444- . enumerate ( )
445- . map ( move |( col_index, & poly_id) | ( poly_id, ( instr_index, col_index) ) )
443+ subs. iter ( ) . enumerate ( ) . map ( move |( col_index, & poly_id) | {
444+ (
445+ poly_id,
446+ ( block. start_pc as usize + ( instr_index * 4 ) , col_index) ,
447+ )
448+ } )
446449 } )
447450 . collect :: < BTreeMap < _ , _ > > ( ) ;
448451 let algebraic_references = machine
@@ -458,8 +461,12 @@ pub fn build<A: Adapter>(
458461 for ( col_index, range) in range_constraints. iter ( ) . enumerate ( ) {
459462 if range. 0 == range. 1 {
460463 let value = A :: PowdrField :: from ( range. 0 as u64 ) ;
461- let Some ( reference) = algebraic_references. get ( & ( i, col_index) ) . cloned ( ) else {
462- println ! ( "Missing reference for (i: {}, col_index: {})" , i, col_index) ;
464+ let Some ( reference) = algebraic_references. get ( & ( pc as usize , col_index) ) . cloned ( )
465+ else {
466+ println ! (
467+ "Missing reference for (pc: {}, col_index: {})" ,
468+ pc, col_index
469+ ) ;
463470 continue ;
464471 } ;
465472 let constraint =
@@ -472,33 +479,32 @@ pub fn build<A: Adapter>(
472479 }
473480 }
474481
475- // TODO: This can cause unsatisfiable constraints somehow.
476- // if let Some(equivalence_classes) = equivalence_classes_by_block.get(&block.start_pc) {
477- // for equivalence_class in equivalence_classes {
478- // let first = equivalence_class.first().unwrap();
479- // let Some(first_ref) = algebraic_references.get(first).cloned() else {
480- // println!(
481- // "Missing reference for (i: {}, col_index: {})",
482- // first.0, first.1
483- // );
484- // continue;
485- // };
486- // for other in equivalence_class.iter().skip(1) {
487- // let Some(other_ref) = algebraic_references.get(other).cloned() else {
488- // println!(
489- // "Missing reference for (i: {}, col_index: {})",
490- // other.0, other.1
491- // );
492- // continue;
493- // };
494- // let constraint = AlgebraicExpression::Reference(first_ref.clone())
495- // - AlgebraicExpression::Reference(other_ref.clone());
496- // machine
497- // .constraints
498- // .push(SymbolicConstraint { expr: constraint });
499- // }
500- // }
501- // }
482+ if let Some ( equivalence_classes) = equivalence_classes_by_block. get ( & block. start_pc ) {
483+ for equivalence_class in equivalence_classes {
484+ let first = equivalence_class. first ( ) . unwrap ( ) ;
485+ let Some ( first_ref) = algebraic_references. get ( first) . cloned ( ) else {
486+ println ! (
487+ "Missing reference for (i: {}, col_index: {})" ,
488+ first. 0 , first. 1
489+ ) ;
490+ continue ;
491+ } ;
492+ for other in equivalence_class. iter ( ) . skip ( 1 ) {
493+ let Some ( other_ref) = algebraic_references. get ( other) . cloned ( ) else {
494+ println ! (
495+ "Missing reference for (i: {}, col_index: {})" ,
496+ other. 0 , other. 1
497+ ) ;
498+ continue ;
499+ } ;
500+ let constraint = AlgebraicExpression :: Reference ( first_ref. clone ( ) )
501+ - AlgebraicExpression :: Reference ( other_ref. clone ( ) ) ;
502+ machine
503+ . constraints
504+ . push ( SymbolicConstraint { expr : constraint } ) ;
505+ }
506+ }
507+ }
502508
503509 let labels = [ ( "apc_start_pc" , block. start_pc . to_string ( ) ) ] ;
504510 metrics:: counter!( "before_opt_cols" , & labels)
0 commit comments