@@ -66,6 +66,7 @@ pub trait Delegate {
66
66
type ProofTreeBuilder ;
67
67
fn inspect_is_noop ( inspect : & mut Self :: ProofTreeBuilder ) -> bool ;
68
68
69
+ const DIVIDE_AVAILABLE_DEPTH_ON_OVERFLOW : usize ;
69
70
fn recursion_limit ( cx : Self :: Cx ) -> usize ;
70
71
71
72
fn initial_provisional_result (
@@ -150,7 +151,7 @@ impl AvailableDepth {
150
151
}
151
152
152
153
Some ( if last. encountered_overflow {
153
- AvailableDepth ( last. available_depth . 0 / 2 )
154
+ AvailableDepth ( last. available_depth . 0 / D :: DIVIDE_AVAILABLE_DEPTH_ON_OVERFLOW )
154
155
} else {
155
156
AvailableDepth ( last. available_depth . 0 - 1 )
156
157
} )
@@ -306,7 +307,7 @@ struct StackEntry<X: Cx> {
306
307
/// goals still on the stack.
307
308
#[ derive_where( Debug ; X : Cx ) ]
308
309
struct ProvisionalCacheEntry < X : Cx > {
309
- is_sus : bool ,
310
+ encountered_overflow : bool ,
310
311
heads : CycleHeads ,
311
312
path_from_head : CycleKind ,
312
313
nested_goals : NestedGoals < X > ,
@@ -421,7 +422,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
421
422
self . provisional_cache . retain ( |& input, entries| {
422
423
entries. retain_mut ( |entry| {
423
424
let ProvisionalCacheEntry {
424
- is_sus : _,
425
+ encountered_overflow : _,
425
426
heads,
426
427
path_from_head,
427
428
nested_goals,
@@ -544,10 +545,9 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
544
545
debug_assert ! ( validate_cache. is_none( ) ) ;
545
546
let entry = self . provisional_cache . entry ( input) . or_default ( ) ;
546
547
let StackEntry { heads, nested_goals, encountered_overflow, .. } = final_entry;
547
- let is_sus = encountered_overflow;
548
548
let path_from_head = Self :: stack_path_kind ( cx, & self . stack , heads. highest_cycle_head ( ) ) ;
549
549
entry. push ( ProvisionalCacheEntry {
550
- is_sus ,
550
+ encountered_overflow ,
551
551
heads,
552
552
path_from_head,
553
553
nested_goals,
@@ -606,14 +606,18 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
606
606
debug ! ( ?input, ?path_from_global_entry, ?entries, "candidate_is_applicable" ) ;
607
607
// A provisional cache entry is applicable if the path to
608
608
// 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,
612
612
path_from_head,
613
613
nested_goals : _,
614
614
result : _,
615
- } in entries. iter ( ) . filter ( |e| !e . is_sus )
615
+ } in entries. iter ( )
616
616
{
617
+ if encountered_overflow {
618
+ continue ;
619
+ }
620
+
617
621
let head = heads. highest_cycle_head ( ) ;
618
622
let full_path = if Self :: stack_coinductive_from ( cx, stack, head) {
619
623
path_from_global_entry
@@ -707,15 +711,15 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
707
711
708
712
let entries = self . provisional_cache . get ( & input) ?;
709
713
for & ProvisionalCacheEntry {
710
- is_sus ,
714
+ encountered_overflow ,
711
715
ref heads,
712
716
path_from_head,
713
717
ref nested_goals,
714
718
result,
715
719
} in entries
716
720
{
717
721
let head = heads. highest_cycle_head ( ) ;
718
- if is_sus {
722
+ if encountered_overflow {
719
723
let last = self . stack . raw . last ( ) . unwrap ( ) ;
720
724
if !last. heads . opt_lowest_cycle_head ( ) . is_some_and ( |lowest| lowest <= head) {
721
725
continue ;
0 commit comments