@@ -908,41 +908,57 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
908
908
} ;
909
909
910
910
// We're rebasing an entry `e` over a head `p`. This head
911
- // has a number of own heads `h` it depends on. We need to
912
- // make sure that the path kind of all paths `hph` remain the
913
- // same after rebasing.
911
+ // has a number of own heads `h` it depends on.
914
912
//
915
- // After rebasing the cycles `hph` will go through `e`. We need
916
- // to make sure that forall possible paths `hep` and `heph`
917
- // is equal to `hph.`
918
- let ep = popped_head. paths_to_head ;
919
- for ( head_index, head) in stack_entry. heads . iter ( ) {
920
- let ph = head. paths_to_head ;
921
- let hp = Self :: cycle_path_kind (
922
- & self . stack ,
923
- stack_entry. step_kind_from_parent ,
924
- head_index,
925
- ) ;
926
-
927
- // We first validate that all cycles while computing `p` would stay
928
- // the same if we were to recompute it as a nested goal of `e`.
929
- let he = hp. extend ( * path_from_head) ;
930
- for ph in ph. iter_paths ( ) {
931
- let hph = hp. extend ( ph) ;
932
- for ep in ep. iter_paths ( ) {
933
- let hep = ep. extend ( he) ;
934
- let heph = hep. extend ( ph) ;
935
- if hph != heph {
936
- return false ;
913
+ // This causes our provisional result to depend on the lowest head
914
+ // of `p` to avoid moving any goal which uses this cache entry to
915
+ // the global cache.
916
+ if popped_head. usages . is_empty ( ) {
917
+ // The result of `e` does not depend on the value of `p`. This we can
918
+ // keep using the result of this provisional cache entry even if evaluating
919
+ // `p` as a nested goal of `e` would have a different result.
920
+ for ( head_index, _) in stack_entry. heads . iter ( ) {
921
+ heads. insert ( head_index, PathsToNested :: EMPTY , Usages :: default ( ) ) ;
922
+ }
923
+ } else {
924
+ // The entry `e` actually depends on the value of `p`. We need
925
+ // to make sure that the value of `p` wouldn't change even if we
926
+ // were to reevaluate it as a nested goal of `e` instead. For this
927
+ // we check that the path kind of all paths `hph` remain the
928
+ // same after rebasing.
929
+ //
930
+ // After rebasing the cycles `hph` will go through `e`. We need
931
+ // to make sure that forall possible paths `hep` and `heph`
932
+ // is equal to `hph.`
933
+ let ep = popped_head. paths_to_head ;
934
+ for ( head_index, head) in stack_entry. heads . iter ( ) {
935
+ let ph = head. paths_to_head ;
936
+ let hp = Self :: cycle_path_kind (
937
+ & self . stack ,
938
+ stack_entry. step_kind_from_parent ,
939
+ head_index,
940
+ ) ;
941
+
942
+ // We first validate that all cycles while computing `p` would stay
943
+ // the same if we were to recompute it as a nested goal of `e`.
944
+ let he = hp. extend ( * path_from_head) ;
945
+ for ph in ph. iter_paths ( ) {
946
+ let hph = hp. extend ( ph) ;
947
+ for ep in ep. iter_paths ( ) {
948
+ let hep = ep. extend ( he) ;
949
+ let heph = hep. extend ( ph) ;
950
+ if hph != heph {
951
+ return false ;
952
+ }
937
953
}
938
954
}
939
- }
940
955
941
- // If so, all paths reached while computing `p` have to get added
942
- // the heads of `e` to make sure that rebasing `e` again also considers
943
- // them.
944
- let eph = ep. extend_with_paths ( ph) ;
945
- heads. insert ( head_index, eph, head. usages . compressed ( ) ) ;
956
+ // If so, all paths reached while computing `p` have to get added
957
+ // the heads of `e` to make sure that rebasing `e` again also considers
958
+ // them.
959
+ let eph = ep. extend_with_paths ( ph) ;
960
+ heads. insert ( head_index, eph, head. usages . compressed ( ) ) ;
961
+ }
946
962
}
947
963
948
964
let Some ( head_index) = heads. opt_highest_cycle_head_index ( ) else {
0 commit comments