@@ -66,6 +66,7 @@ pub trait Delegate {
6666 type ProofTreeBuilder ;
6767 fn inspect_is_noop ( inspect : & mut Self :: ProofTreeBuilder ) -> bool ;
6868
69+ const DIVIDE_AVAILABLE_DEPTH_ON_OVERFLOW : usize ;
6970 fn recursion_limit ( cx : Self :: Cx ) -> usize ;
7071
7172 fn initial_provisional_result (
@@ -150,7 +151,7 @@ impl AvailableDepth {
150151 }
151152
152153 Some ( if last. encountered_overflow {
153- AvailableDepth ( last. available_depth . 0 / 2 )
154+ AvailableDepth ( last. available_depth . 0 / D :: DIVIDE_AVAILABLE_DEPTH_ON_OVERFLOW )
154155 } else {
155156 AvailableDepth ( last. available_depth . 0 - 1 )
156157 } )
@@ -306,7 +307,7 @@ struct StackEntry<X: Cx> {
306307/// goals still on the stack.
307308#[ derive_where( Debug ; X : Cx ) ]
308309struct ProvisionalCacheEntry < X : Cx > {
309- is_sus : bool ,
310+ encountered_overflow : bool ,
310311 heads : CycleHeads ,
311312 path_from_head : CycleKind ,
312313 nested_goals : NestedGoals < X > ,
@@ -421,7 +422,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
421422 self . provisional_cache . retain ( |& input, entries| {
422423 entries. retain_mut ( |entry| {
423424 let ProvisionalCacheEntry {
424- is_sus : _,
425+ encountered_overflow : _,
425426 heads,
426427 path_from_head,
427428 nested_goals,
@@ -544,10 +545,9 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
544545 debug_assert ! ( validate_cache. is_none( ) ) ;
545546 let entry = self . provisional_cache . entry ( input) . or_default ( ) ;
546547 let StackEntry { heads, nested_goals, encountered_overflow, .. } = final_entry;
547- let is_sus = encountered_overflow;
548548 let path_from_head = Self :: stack_path_kind ( cx, & self . stack , heads. highest_cycle_head ( ) ) ;
549549 entry. push ( ProvisionalCacheEntry {
550- is_sus ,
550+ encountered_overflow ,
551551 heads,
552552 path_from_head,
553553 nested_goals,
@@ -606,14 +606,18 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
606606 debug ! ( ?input, ?path_from_global_entry, ?entries, "candidate_is_applicable" ) ;
607607 // A provisional cache entry is applicable if the path to
608608 // its highest cycle head is equal to the expected path.
609- for ProvisionalCacheEntry {
610- is_sus : _ ,
611- heads,
609+ for & ProvisionalCacheEntry {
610+ encountered_overflow ,
611+ ref heads,
612612 path_from_head,
613613 nested_goals : _,
614614 result : _,
615- } in entries. iter ( ) . filter ( |e| !e . is_sus )
615+ } in entries. iter ( )
616616 {
617+ if encountered_overflow {
618+ continue ;
619+ }
620+
617621 let head = heads. highest_cycle_head ( ) ;
618622 let full_path = if Self :: stack_coinductive_from ( cx, stack, head) {
619623 path_from_global_entry
@@ -707,15 +711,15 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
707711
708712 let entries = self . provisional_cache . get ( & input) ?;
709713 for & ProvisionalCacheEntry {
710- is_sus ,
714+ encountered_overflow ,
711715 ref heads,
712716 path_from_head,
713717 ref nested_goals,
714718 result,
715719 } in entries
716720 {
717721 let head = heads. highest_cycle_head ( ) ;
718- if is_sus {
722+ if encountered_overflow {
719723 let last = self . stack . raw . last ( ) . unwrap ( ) ;
720724 if !last. heads . opt_lowest_cycle_head ( ) . is_some_and ( |lowest| lowest <= head) {
721725 continue ;
0 commit comments