11use crate :: adapter:: { Adapter , AdapterApc , AdapterVmConfig } ;
22use crate :: blocks:: BasicBlock ;
33use crate :: bus_map:: { BusMap , BusType } ;
4+ use crate :: data_driven_constraints:: { add_ai_constraints, DataDrivenConstraints } ;
45use crate :: evaluation:: AirStats ;
56use crate :: expression_conversion:: algebraic_to_grouped_expression;
67use crate :: symbolic_machine_generator:: convert_machine_field_type;
@@ -12,7 +13,7 @@ use powdr_expression::{
1213 visitors:: Children , AlgebraicBinaryOperation , AlgebraicBinaryOperator , AlgebraicUnaryOperation ,
1314} ;
1415use serde:: { Deserialize , Serialize } ;
15- use std:: collections:: { BTreeMap , BTreeSet } ;
16+ use std:: collections:: BTreeSet ;
1617use std:: fmt:: Display ;
1718use std:: io:: BufWriter ;
1819use std:: iter:: once;
@@ -26,6 +27,7 @@ pub mod adapter;
2627pub mod blocks;
2728pub mod bus_map;
2829pub mod constraint_optimizer;
30+ pub mod data_driven_constraints;
2931pub mod evaluation;
3032pub mod execution_profile;
3133pub mod expression;
@@ -416,111 +418,12 @@ impl ColumnAllocator {
416418 }
417419}
418420
419- #[ derive( Serialize , Deserialize ) ]
420- pub struct DebugInfo {
421- pub air_id_by_pc : BTreeMap < u32 , usize > ,
422- pub column_names_by_air_id : BTreeMap < usize , Vec < String > > ,
423- }
424-
425- #[ derive( Serialize , Deserialize , Clone ) ]
426- pub struct ExecutionStats {
427- pub column_ranges_by_pc : BTreeMap < u32 , Vec < ( u32 , u32 ) > > ,
428- pub equivalence_classes_by_block : BTreeMap < u64 , Vec < Vec < ( usize , usize ) > > > ,
429- }
430-
431- #[ derive( Serialize , Deserialize ) ]
432- pub struct ExecutionStatsJson {
433- pub execution_stats : ExecutionStats ,
434- pub debug_info : DebugInfo ,
435- }
436-
437- fn add_ai_constraints < A : Adapter > (
438- execution_stats : & ExecutionStats ,
439- subs : & [ Vec < u64 > ] ,
440- block : & BasicBlock < A :: Instruction > ,
441- columns : impl Iterator < Item = AlgebraicReference > ,
442- ) -> (
443- Vec < SymbolicConstraint < A :: PowdrField > > ,
444- Vec < SymbolicConstraint < A :: PowdrField > > ,
445- ) {
446- let range_constraints = & execution_stats. column_ranges_by_pc ;
447- let equivalence_classes_by_block = & execution_stats. equivalence_classes_by_block ;
448-
449- let mut range_analyzer_constraints = Vec :: new ( ) ;
450- let mut equivalence_analyzer_constraints = Vec :: new ( ) ;
451-
452- // Mapping (instruction index, column index) -> AlgebraicReference
453- let reverse_subs = subs
454- . iter ( )
455- . enumerate ( )
456- . flat_map ( |( instr_index, subs) | {
457- subs. iter ( )
458- . enumerate ( )
459- . map ( move |( col_index, & poly_id) | ( poly_id, ( instr_index, col_index) ) )
460- } )
461- . collect :: < BTreeMap < _ , _ > > ( ) ;
462- let algebraic_references = columns
463- . map ( |r| ( reverse_subs. get ( & r. id ) . unwrap ( ) . clone ( ) , r. clone ( ) ) )
464- . collect :: < BTreeMap < _ , _ > > ( ) ;
465-
466- for i in 0 ..block. statements . len ( ) {
467- let pc = ( block. start_pc + ( i * 4 ) as u64 ) as u32 ;
468- let Some ( range_constraints) = range_constraints. get ( & pc) else {
469- continue ;
470- } ;
471- for ( col_index, range) in range_constraints. iter ( ) . enumerate ( ) {
472- if range. 0 == range. 1 {
473- let value = A :: PowdrField :: from ( range. 0 as u64 ) ;
474- let Some ( reference) = algebraic_references. get ( & ( i, col_index) ) . cloned ( ) else {
475- panic ! (
476- "Missing reference for (i: {}, col_index: {}, block_id: {})" ,
477- i, col_index, block. start_pc
478- ) ;
479- } ;
480- let constraint =
481- AlgebraicExpression :: Reference ( reference) - AlgebraicExpression :: Number ( value) ;
482-
483- range_analyzer_constraints. push ( SymbolicConstraint { expr : constraint } ) ;
484- }
485- }
486- }
487-
488- if let Some ( equivalence_classes) = equivalence_classes_by_block. get ( & block. start_pc ) {
489- for equivalence_class in equivalence_classes {
490- let first = equivalence_class. first ( ) . unwrap ( ) ;
491- let Some ( first_ref) = algebraic_references. get ( first) . cloned ( ) else {
492- // TODO: This fails in some blocks. For now, just return no extra constraints.
493- println ! (
494- "Missing reference for (i: {}, col_index: {}, block_id: {})" ,
495- first. 0 , first. 1 , block. start_pc
496- ) ;
497- return ( range_analyzer_constraints, vec ! [ ] ) ;
498- } ;
499- for other in equivalence_class. iter ( ) . skip ( 1 ) {
500- let Some ( other_ref) = algebraic_references. get ( other) . cloned ( ) else {
501- // TODO: This fails in some blocks. For now, just return no extra constraints.
502- println ! (
503- "Missing reference for (i: {}, col_index: {}, block_id: {})" ,
504- other. 0 , other. 1 , block. start_pc
505- ) ;
506- return ( range_analyzer_constraints, vec ! [ ] ) ;
507- } ;
508- let constraint = AlgebraicExpression :: Reference ( first_ref. clone ( ) )
509- - AlgebraicExpression :: Reference ( other_ref. clone ( ) ) ;
510- equivalence_analyzer_constraints. push ( SymbolicConstraint { expr : constraint } ) ;
511- }
512- }
513- }
514-
515- ( range_analyzer_constraints, equivalence_analyzer_constraints)
516- }
517-
518421pub fn build < A : Adapter > (
519422 block : BasicBlock < A :: Instruction > ,
520423 vm_config : AdapterVmConfig < A > ,
521424 degree_bound : DegreeBound ,
522425 apc_candidates_dir_path : Option < & Path > ,
523- execution_stats : & ExecutionStats ,
426+ execution_stats : & DataDrivenConstraints ,
524427) -> Result < AdapterApc < A > , crate :: constraint_optimizer:: Error > {
525428 let start = std:: time:: Instant :: now ( ) ;
526429
0 commit comments