@@ -417,26 +417,23 @@ pub struct ExecutionStats {
417417 pub equivalence_classes_by_block : BTreeMap < u64 , Vec < Vec < ( usize , usize ) > > > ,
418418}
419419
420- pub fn build < A : Adapter > (
421- block : BasicBlock < A :: Instruction > ,
422- vm_config : AdapterVmConfig < A > ,
423- degree_bound : DegreeBound ,
424- apc_candidates_dir_path : Option < & Path > ,
420+ fn add_ai_constraints < A : Adapter > (
425421 execution_stats : & ExecutionStats ,
426- ) -> Result < AdapterApc < A > , crate :: constraint_optimizer:: Error > {
427- let start = std:: time:: Instant :: now ( ) ;
428-
429- let ( mut machine, column_allocator) = statements_to_symbolic_machine :: < A > (
430- & block,
431- vm_config. instruction_handler ,
432- & vm_config. bus_map ,
433- ) ;
422+ subs : & [ Vec < u64 > ] ,
423+ block : & BasicBlock < A :: Instruction > ,
424+ columns : impl Iterator < Item = AlgebraicReference > ,
425+ ) -> (
426+ Vec < SymbolicConstraint < A :: PowdrField > > ,
427+ Vec < SymbolicConstraint < A :: PowdrField > > ,
428+ ) {
434429 let range_constraints = & execution_stats. column_ranges_by_pc ;
435430 let equivalence_classes_by_block = & execution_stats. equivalence_classes_by_block ;
436431
432+ let mut range_analyzer_constraints = Vec :: new ( ) ;
433+ let mut equivalence_analyzer_constraints = Vec :: new ( ) ;
434+
437435 // Mapping (instruction index, column index) -> AlgebraicReference
438- let reverse_subs = column_allocator
439- . subs
436+ let reverse_subs = subs
440437 . iter ( )
441438 . enumerate ( )
442439 . flat_map ( |( instr_index, subs) | {
@@ -445,8 +442,7 @@ pub fn build<A: Adapter>(
445442 . map ( move |( col_index, & poly_id) | ( poly_id, ( instr_index, col_index) ) )
446443 } )
447444 . collect :: < BTreeMap < _ , _ > > ( ) ;
448- let algebraic_references = machine
449- . main_columns ( )
445+ let algebraic_references = columns
450446 . map ( |r| ( reverse_subs. get ( & r. id ) . unwrap ( ) . clone ( ) , r. clone ( ) ) )
451447 . collect :: < BTreeMap < _ , _ > > ( ) ;
452448
@@ -465,40 +461,60 @@ pub fn build<A: Adapter>(
465461 let constraint =
466462 AlgebraicExpression :: Reference ( reference) - AlgebraicExpression :: Number ( value) ;
467463
468- machine
469- . constraints
470- . push ( SymbolicConstraint { expr : constraint } ) ;
464+ range_analyzer_constraints. push ( SymbolicConstraint { expr : constraint } ) ;
465+ }
466+ }
467+ }
468+
469+ if let Some ( equivalence_classes) = equivalence_classes_by_block. get ( & block. start_pc ) {
470+ for equivalence_class in equivalence_classes {
471+ let first = equivalence_class. first ( ) . unwrap ( ) ;
472+ let Some ( first_ref) = algebraic_references. get ( first) . cloned ( ) else {
473+ println ! (
474+ "Missing reference for (i: {}, col_index: {})" ,
475+ first. 0 , first. 1
476+ ) ;
477+ continue ;
478+ } ;
479+ for other in equivalence_class. iter ( ) . skip ( 1 ) {
480+ let Some ( other_ref) = algebraic_references. get ( other) . cloned ( ) else {
481+ println ! (
482+ "Missing reference for (i: {}, col_index: {})" ,
483+ other. 0 , other. 1
484+ ) ;
485+ continue ;
486+ } ;
487+ let constraint = AlgebraicExpression :: Reference ( first_ref. clone ( ) )
488+ - AlgebraicExpression :: Reference ( other_ref. clone ( ) ) ;
489+ equivalence_analyzer_constraints. push ( SymbolicConstraint { expr : constraint } ) ;
471490 }
472491 }
473492 }
474493
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- // }
494+ ( range_analyzer_constraints, equivalence_analyzer_constraints)
495+ }
496+
497+ pub fn build < A : Adapter > (
498+ block : BasicBlock < A :: Instruction > ,
499+ vm_config : AdapterVmConfig < A > ,
500+ degree_bound : DegreeBound ,
501+ apc_candidates_dir_path : Option < & Path > ,
502+ execution_stats : & ExecutionStats ,
503+ ) -> Result < AdapterApc < A > , crate :: constraint_optimizer:: Error > {
504+ let start = std:: time:: Instant :: now ( ) ;
505+
506+ let ( mut machine, column_allocator) = statements_to_symbolic_machine :: < A > (
507+ & block,
508+ vm_config. instruction_handler ,
509+ & vm_config. bus_map ,
510+ ) ;
511+
512+ let ( range_analyzer_constraints, equivalence_analyzer_constraints) = add_ai_constraints :: < A > (
513+ execution_stats,
514+ & column_allocator. subs ,
515+ & block,
516+ machine. main_columns ( ) ,
517+ ) ;
502518
503519 let labels = [ ( "apc_start_pc" , block. start_pc . to_string ( ) ) ] ;
504520 metrics:: counter!( "before_opt_cols" , & labels)
0 commit comments