@@ -97,8 +97,9 @@ pub(super) fn validate_predicate_is_splittable(
9797}
9898
9999/// Split a predicate into a chain if it exceeds statement limit. Callers
100- /// splitting many predicates under one `Params` (module lowering) share one
101- /// cache so same-shape predicates search only once.
100+ /// splitting many predicates under one `Params` share one cache so same-shape
101+ /// predicates search only once; whole-module callers should prefer
102+ /// [`split_predicates_if_needed`], which also parallelizes the searches.
102103pub fn split_predicate_if_needed (
103104 pred : CustomPredicateDef ,
104105 params : & Params ,
@@ -124,6 +125,73 @@ pub fn split_predicate_if_needed(
124125 } )
125126}
126127
128+ /// Split a whole module's predicates. The link assignment is a pure function
129+ /// of a predicate's statement/wildcard shape, so each distinct shape is
130+ /// searched once and the searches run in parallel across shapes.
131+ pub fn split_predicates_if_needed (
132+ predicates : Vec < CustomPredicateDef > ,
133+ params : & Params ,
134+ ) -> Result < Vec < SplitResult > , SplittingError > {
135+ use rayon:: prelude:: * ;
136+
137+ for pred in & predicates {
138+ validate_predicate_is_splittable ( pred) ?;
139+ }
140+
141+ // Predicates over the statement cap get a prepared split input; the rest
142+ // pass through whole.
143+ let inputs: Vec < Option < SplitInput > > = predicates
144+ . iter ( )
145+ . map ( |pred| {
146+ ( pred. statements . len ( ) > Params :: max_custom_predicate_arity ( ) )
147+ . then ( || prepare_split_input ( pred) )
148+ } )
149+ . collect ( ) ;
150+
151+ // One representative per distinct shape, in first-encounter order so a
152+ // search failure surfaces the same predicate the sequential loop would
153+ // have blamed.
154+ let mut seen_shapes: HashSet < & SplitShape > = HashSet :: new ( ) ;
155+ let mut representatives: Vec < ( & str , & SplitInput ) > = Vec :: new ( ) ;
156+ for ( pred, input) in predicates. iter ( ) . zip ( & inputs) {
157+ if let Some ( input) = input {
158+ if seen_shapes. insert ( & input. shape ) {
159+ representatives. push ( ( pred. name . name . as_str ( ) , input) ) ;
160+ }
161+ }
162+ }
163+
164+ let searched: Vec < Result < LinkAssignment , SplittingError > > = representatives
165+ . par_iter ( )
166+ . map ( |( name, input) | search_link_assignment ( name, input, params) )
167+ . collect ( ) ;
168+ let mut assignment_of_shape: HashMap < & SplitShape , LinkAssignment > = HashMap :: new ( ) ;
169+ for ( ( _, input) , result) in representatives. iter ( ) . zip ( searched) {
170+ assignment_of_shape. insert ( & input. shape , result?) ;
171+ }
172+
173+ let results: Vec < Result < SplitResult , SplittingError > > = predicates
174+ . into_par_iter ( )
175+ . zip ( & inputs)
176+ . map ( |( pred, input) | match input {
177+ None => Ok ( SplitResult {
178+ predicates : vec ! [ pred] ,
179+ chain_info : None ,
180+ } ) ,
181+ Some ( input) => {
182+ let assignment = assignment_of_shape[ & input. shape ] . clone ( ) ;
183+ let ( chain_predicates, chain_info) =
184+ build_chain_from_assignment ( & pred, input, assignment, params) ?;
185+ Ok ( SplitResult {
186+ predicates : chain_predicates,
187+ chain_info : Some ( chain_info) ,
188+ } )
189+ }
190+ } )
191+ . collect ( ) ;
192+ results. into_iter ( ) . collect ( )
193+ }
194+
127195fn collect_wildcards_from_statement ( stmt : & StatementTmpl ) -> HashSet < String > {
128196 stmt. wildcard_names ( ) . map ( str:: to_string) . collect ( )
129197}
@@ -852,6 +920,7 @@ enum CandidateSearch {
852920fn candidate_orderings ( input : & SplitInput , params : & Params ) -> CandidateSearch {
853921 use rand:: { seq:: SliceRandom , SeedableRng } ;
854922 use rand_chacha:: ChaCha20Rng ;
923+ use rayon:: prelude:: * ;
855924
856925 let num_statements = input. shape . num_statements ;
857926 let max_args = Params :: max_statement_args ( ) ;
@@ -882,26 +951,29 @@ fn candidate_orderings(input: &SplitInput, params: &Params) -> CandidateSearch {
882951 refinement_seeds. push ( shuffled) ;
883952 }
884953
885- let mut refined: Vec < ( Vec < usize > , usize ) > = Vec :: new ( ) ;
886- let mut shortcut_attempted = false ;
887- for seed in refinement_seeds {
888- let result = refine_ordering (
889- seed,
890- & input. shape . statements_using ,
891- & input. shape . is_original_public ,
892- max_args,
893- REFINE_ITERATIONS ,
894- ) ;
895- let result_cost = input. excess_cost ( & result) ;
896- if result_cost == 0 && !shortcut_attempted {
897- shortcut_attempted = true ;
898- if let Some ( assignment) = input. partition_at_lower_bound ( & result, params) {
899- return CandidateSearch :: Found ( assignment) ;
900- }
901- // A cost-0 ordering that still needs extra links: refine the
902- // remaining seeds and let the full partition loop decide.
954+ // Each refinement depends only on its seed, so the seeds run in parallel.
955+ let mut refined: Vec < ( Vec < usize > , usize ) > = refinement_seeds
956+ . into_par_iter ( )
957+ . map ( |seed| {
958+ let result = refine_ordering (
959+ seed,
960+ & input. shape . statements_using ,
961+ & input. shape . is_original_public ,
962+ max_args,
963+ REFINE_ITERATIONS ,
964+ ) ;
965+ let result_cost = input. excess_cost ( & result) ;
966+ ( result, result_cost)
967+ } )
968+ . collect ( ) ;
969+ // The first cost-0 refinement in seed order gets one shortcut attempt: the
970+ // stable sort below keeps seed order among ties, so it is the ordering the
971+ // partition loop would try first anyway. A cost-0 ordering that still
972+ // needs extra links falls through to the full partition loop.
973+ if let Some ( ( zero_cost_ordering, _) ) = refined. iter ( ) . find ( |( _, cost) | * cost == 0 ) {
974+ if let Some ( assignment) = input. partition_at_lower_bound ( zero_cost_ordering, params) {
975+ return CandidateSearch :: Found ( assignment) ;
903976 }
904- refined. push ( ( result, result_cost) ) ;
905977 }
906978 refined. sort_by_key ( |( _, refined_cost) | * refined_cost) ;
907979
@@ -931,12 +1003,7 @@ fn split_into_chain(
9311003 params : & Params ,
9321004 search_cache : & mut SplitSearchCache ,
9331005) -> Result < ( Vec < CustomPredicateDef > , SplitChainInfo ) , SplittingError > {
934- let original_name = pred. name . name . clone ( ) ;
935- let conjunction = pred. conjunction_type ;
936- let real_statement_count = pred. statements . len ( ) ;
937-
9381006 let input = prepare_split_input ( pred) ;
939- let num_statements = input. shape . num_statements ;
9401007
9411008 // The link assignment depends only on the statement/wildcard usage shape
9421009 // (plus `params`, fixed for the cache's lifetime), and modules routinely
@@ -945,13 +1012,30 @@ fn split_into_chain(
9451012 let assignment = if let Some ( assignment) = search_cache. assignments . get ( & input. shape ) {
9461013 assignment. clone ( )
9471014 } else {
948- let assignment = search_link_assignment ( & original_name , & input, params) ?;
1015+ let assignment = search_link_assignment ( & pred . name . name , & input, params) ?;
9491016 search_cache
9501017 . assignments
9511018 . insert ( input. shape . clone ( ) , assignment. clone ( ) ) ;
9521019 assignment
9531020 } ;
9541021
1022+ build_chain_from_assignment ( pred, & input, assignment, params)
1023+ }
1024+
1025+ /// Everything downstream of the ordering search: reorder the statements per
1026+ /// the assignment, derive each link's argument lists, and emit the chain's
1027+ /// predicate definitions plus [`SplitChainInfo`].
1028+ fn build_chain_from_assignment (
1029+ pred : & CustomPredicateDef ,
1030+ input : & SplitInput ,
1031+ assignment : LinkAssignment ,
1032+ params : & Params ,
1033+ ) -> Result < ( Vec < CustomPredicateDef > , SplitChainInfo ) , SplittingError > {
1034+ let original_name = pred. name . name . clone ( ) ;
1035+ let conjunction = pred. conjunction_type ;
1036+ let real_statement_count = pred. statements . len ( ) ;
1037+ let num_statements = input. shape . num_statements ;
1038+
9551039 // Reorder map: original index -> position in flattened chain.
9561040 let mut reorder_map = vec ! [ 0usize ; num_statements] ;
9571041 {
0 commit comments