@@ -132,6 +132,12 @@ pub trait SolverDelegateEvalExt: SolverDelegate {
132
132
generate_proof_tree : GenerateProofTree ,
133
133
) -> ( Result < ( bool , Certainty ) , NoSolution > , Option < inspect:: GoalEvaluation < Self :: Interner > > ) ;
134
134
135
+ fn root_goal_may_hold_with_depth (
136
+ & self ,
137
+ root_depth : usize ,
138
+ goal : Goal < Self :: Interner , <Self :: Interner as Interner >:: Predicate > ,
139
+ ) -> bool ;
140
+
135
141
// FIXME: This is only exposed because we need to use it in `analyse.rs`
136
142
// which is not yet uplifted. Once that's done, we should remove this.
137
143
fn evaluate_root_goal_raw (
@@ -159,11 +165,25 @@ where
159
165
goal : Goal < I , I :: Predicate > ,
160
166
generate_proof_tree : GenerateProofTree ,
161
167
) -> ( Result < ( bool , Certainty ) , NoSolution > , Option < inspect:: GoalEvaluation < I > > ) {
162
- EvalCtxt :: enter_root ( self , generate_proof_tree, |ecx| {
168
+ EvalCtxt :: enter_root ( self , self . cx ( ) . recursion_limit ( ) , generate_proof_tree, |ecx| {
163
169
ecx. evaluate_goal ( GoalEvaluationKind :: Root , GoalSource :: Misc , goal)
164
170
} )
165
171
}
166
172
173
+ fn root_goal_may_hold_with_depth (
174
+ & self ,
175
+ root_depth : usize ,
176
+ goal : Goal < Self :: Interner , <Self :: Interner as Interner >:: Predicate > ,
177
+ ) -> bool {
178
+ self . probe ( || {
179
+ EvalCtxt :: enter_root ( self , root_depth, GenerateProofTree :: No , |ecx| {
180
+ ecx. evaluate_goal ( GoalEvaluationKind :: Root , GoalSource :: Misc , goal)
181
+ } )
182
+ . 0
183
+ } )
184
+ . is_ok ( )
185
+ }
186
+
167
187
#[ instrument( level = "debug" , skip( self ) ) ]
168
188
fn evaluate_root_goal_raw (
169
189
& self ,
@@ -173,7 +193,7 @@ where
173
193
Result < ( NestedNormalizationGoals < I > , bool , Certainty ) , NoSolution > ,
174
194
Option < inspect:: GoalEvaluation < I > > ,
175
195
) {
176
- EvalCtxt :: enter_root ( self , generate_proof_tree, |ecx| {
196
+ EvalCtxt :: enter_root ( self , self . cx ( ) . recursion_limit ( ) , generate_proof_tree, |ecx| {
177
197
ecx. evaluate_goal_raw ( GoalEvaluationKind :: Root , GoalSource :: Misc , goal)
178
198
} )
179
199
}
@@ -197,10 +217,11 @@ where
197
217
/// over using this manually (such as [`SolverDelegateEvalExt::evaluate_root_goal`]).
198
218
pub ( super ) fn enter_root < R > (
199
219
delegate : & D ,
220
+ root_depth : usize ,
200
221
generate_proof_tree : GenerateProofTree ,
201
222
f : impl FnOnce ( & mut EvalCtxt < ' _ , D > ) -> R ,
202
223
) -> ( R , Option < inspect:: GoalEvaluation < I > > ) {
203
- let mut search_graph = SearchGraph :: new ( delegate. solver_mode ( ) ) ;
224
+ let mut search_graph = SearchGraph :: new ( delegate. solver_mode ( ) , root_depth ) ;
204
225
205
226
let mut ecx = EvalCtxt {
206
227
delegate,
0 commit comments