Skip to content

Commit faafc66

Browse files
borsbors
committed
Auto merge of #647 - flodiebold:recursive-max-size, r=jackh726
Make max goal size for recursive solver configurable
2 parents 65daa08 + 4d203b6 commit faafc66

File tree

12 files changed

+58
-28
lines changed

12 files changed

+58
-28
lines changed

‎chalk-integration/src/lib.rs

Lines changed: 18 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,7 @@ pub enum SolverChoice {
5555
Recursive {
5656
overflow_depth: usize,
5757
caching_enabled: bool,
58+
max_size: usize,
5859
},
5960
}
6061

@@ -73,10 +74,20 @@ impl SolverChoice {
7374
}
7475

7576
/// Returns the default recursive solver setup.
76-
pub fn recursive() -> Self {
77+
pub fn recursive_default() -> Self {
7778
SolverChoice::Recursive {
7879
overflow_depth: 100,
7980
caching_enabled: true,
81+
max_size: 30,
82+
}
83+
}
84+
85+
/// Returns a recursive solver with specific parameters.
86+
pub fn recursive(max_size: usize, overflow_depth: usize) -> Self {
87+
SolverChoice::Recursive {
88+
overflow_depth,
89+
caching_enabled: true,
90+
max_size,
8091
}
8192
}
8293

@@ -89,7 +100,12 @@ impl SolverChoice {
89100
SolverChoice::Recursive {
90101
overflow_depth,
91102
caching_enabled,
92-
} => Box::new(RecursiveSolver::new(overflow_depth, caching_enabled)),
103+
max_size,
104+
} => Box::new(RecursiveSolver::new(
105+
overflow_depth,
106+
max_size,
107+
caching_enabled,
108+
)),
93109
}
94110
}
95111
}

‎chalk-recursive/src/fulfill.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -234,7 +234,7 @@ impl<'s, I: Interner, Solver: SolveDatabase<I>, Infer: RecursiveInferenceTable<I
234234
Obligation::Prove(goal) => {
235235
if self
236236
.infer
237-
.needs_truncation(self.solver.interner(), 30, goal)
237+
.needs_truncation(self.solver.interner(), self.solver.max_size(), goal)
238238
{
239239
// the goal is too big. Record that we should return Ambiguous
240240
self.cannot_prove = true;
@@ -244,7 +244,7 @@ impl<'s, I: Interner, Solver: SolveDatabase<I>, Infer: RecursiveInferenceTable<I
244244
Obligation::Refute(goal) => {
245245
if self
246246
.infer
247-
.needs_truncation(self.solver.interner(), 30, goal)
247+
.needs_truncation(self.solver.interner(), self.solver.max_size(), goal)
248248
{
249249
// the goal is too big. Record that we should return Ambiguous
250250
self.cannot_prove = true;

‎chalk-recursive/src/recursive.rs

Lines changed: 15 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,9 @@ struct RecursiveContext<I: Interner> {
2424
/// result.
2525
cache: FxHashMap<UCanonicalGoal<I>, Fallible<Solution<I>>>,
2626

27+
/// The maximum size for goals.
28+
max_size: usize,
29+
2730
caching_enabled: bool,
2831
}
2932

@@ -42,9 +45,13 @@ pub struct RecursiveSolver<I: Interner> {
4245
}
4346

4447
impl<I: Interner> RecursiveSolver<I> {
45-
pub fn new(overflow_depth: usize, caching_enabled: bool) -> Self {
48+
pub fn new(overflow_depth: usize, max_size: usize, caching_enabled: bool) -> Self {
4649
Self {
47-
ctx: Box::new(RecursiveContext::new(overflow_depth, caching_enabled)),
50+
ctx: Box::new(RecursiveContext::new(
51+
overflow_depth,
52+
max_size,
53+
caching_enabled,
54+
)),
4855
}
4956
}
5057
}
@@ -76,11 +83,12 @@ impl<T> MergeWith<T> for Fallible<T> {
7683
}
7784

7885
impl<I: Interner> RecursiveContext<I> {
79-
pub fn new(overflow_depth: usize, caching_enabled: bool) -> Self {
86+
pub fn new(overflow_depth: usize, max_size: usize, caching_enabled: bool) -> Self {
8087
RecursiveContext {
8188
stack: Stack::new(overflow_depth),
8289
search_graph: SearchGraph::new(),
8390
cache: FxHashMap::default(),
91+
max_size,
8492
caching_enabled,
8593
}
8694
}
@@ -291,6 +299,10 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
291299
fn db(&self) -> &dyn RustIrDatabase<I> {
292300
self.program
293301
}
302+
303+
fn max_size(&self) -> usize {
304+
self.context.max_size
305+
}
294306
}
295307

296308
impl<I: Interner> chalk_solve::Solver<I> for RecursiveSolver<I> {

‎chalk-recursive/src/solve.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,8 @@ pub(super) trait SolveDatabase<I: Interner>: Sized {
2424
minimums: &mut Minimums,
2525
) -> Fallible<Solution<I>>;
2626

27+
fn max_size(&self) -> usize;
28+
2729
fn interner(&self) -> &I;
2830

2931
fn db(&self) -> &dyn RustIrDatabase<I>;

‎tests/test/coinduction.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -219,7 +219,7 @@ fn coinductive_unsound1() {
219219

220220
goal {
221221
forall<X> { X: C1orC2 }
222-
} yields[SolverChoice::recursive()] {
222+
} yields[SolverChoice::recursive_default()] {
223223
// FIXME(chalk#399) recursive solver doesn't handle coinduction correctly
224224
"Unique; substitution [], lifetime constraints []"
225225
}
@@ -455,7 +455,7 @@ fn coinductive_multicycle4() {
455455

456456
goal {
457457
forall<X> { X: Any }
458-
} yields[SolverChoice::recursive()] {
458+
} yields[SolverChoice::recursive_default()] {
459459
// FIXME(chalk#399) recursive solver doesn't handle coinduction correctly
460460
"Unique; substitution [], lifetime constraints []"
461461
}

‎tests/test/cycle.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -165,7 +165,7 @@ fn overflow() {
165165
S<Z>: Q
166166
} yields[SolverChoice::slg(10, None)] {
167167
"Ambiguous; no inference guidance"
168-
} yields[SolverChoice::recursive()] {
168+
} yields[SolverChoice::recursive_default()] {
169169
"Ambiguous; no inference guidance"
170170
}
171171
}

‎tests/test/existential_types.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -413,7 +413,7 @@ fn dyn_associated_type_binding() {
413413
<dyn FnOnce<(), Output = i32> + 's as FnOnce<()>>::Output = T
414414
}
415415
}
416-
} yields[SolverChoice::recursive()] {
416+
} yields[SolverChoice::recursive_default()] {
417417
"Unique; substitution [?0 := Int(I32)], lifetime constraints []"
418418
} yields[SolverChoice::slg_default()] {
419419
// #234

‎tests/test/misc.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -130,7 +130,7 @@ fn only_draw_so_many() {
130130
exists<T> { T: Sized }
131131
} yields[SolverChoice::slg(10, Some(2))] {
132132
"Ambiguous; no inference guidance"
133-
} yields[SolverChoice::recursive()] {
133+
} yields[SolverChoice::recursive_default()] {
134134
"Ambiguous; no inference guidance"
135135
}
136136
}
@@ -158,7 +158,7 @@ fn only_draw_so_many_blow_up() {
158158
exists<T> { T: Foo }
159159
} yields[SolverChoice::slg(10, Some(2))] {
160160
"Ambiguous; definite substitution for<?U0> { [?0 := Vec<^0.0>] }"
161-
} yields[SolverChoice::recursive()] {
161+
} yields[SolverChoice::recursive_default()] {
162162
"Ambiguous; definite substitution for<?U0> { [?0 := Vec<^0.0>] }"
163163
}
164164
}
@@ -696,7 +696,7 @@ fn not_really_ambig() {
696696
exists<T> { Vec<T>: A }
697697
} yields[SolverChoice::slg_default()] {
698698
"Unique; substitution [?0 := Uint(U32)], lifetime constraints []"
699-
} yields[SolverChoice::recursive()] {
699+
} yields[SolverChoice::recursive_default()] {
700700
"Ambiguous; no inference guidance"
701701
}
702702
}
@@ -754,7 +754,7 @@ fn empty_definite_guidance() {
754754
// recursive solver infinite loop.
755755
} yields[SolverChoice::slg_default()] {
756756
"Unique"
757-
} yields[SolverChoice::recursive()] {
757+
} yields[SolverChoice::recursive_default()] {
758758
"Ambiguous"
759759
}
760760
}

‎tests/test/mod.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ macro_rules! parse_test_data {
7777
@parsed_goals[
7878
$($parsed_goals)*
7979
(stringify!($goal), SolverChoice::slg_default(), TestGoal::Aggregated($expected))
80-
(stringify!($goal), SolverChoice::recursive(), TestGoal::Aggregated($expected))
80+
(stringify!($goal), SolverChoice::recursive_default(), TestGoal::Aggregated($expected))
8181
]
8282
@unparsed_goals[$($unparsed_goals)*])
8383
};

‎tests/test/opaque_types.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -166,7 +166,7 @@ fn opaque_generics() {
166166
}
167167
} yields[SolverChoice::slg_default()] {
168168
"Ambiguous" // #234
169-
} yields[SolverChoice::recursive()] {
169+
} yields[SolverChoice::recursive_default()] {
170170
"Unique; substitution [?0 := Bar], lifetime constraints []"
171171
}
172172
}

‎tests/test/projection.rs

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -142,7 +142,7 @@ fn projection_equality() {
142142
} yields[SolverChoice::slg_default()] {
143143
// this is wrong, chalk#234
144144
"Ambiguous"
145-
} yields[SolverChoice::recursive()] {
145+
} yields[SolverChoice::recursive_default()] {
146146
"Unique; substitution [?0 := Uint(U32)]"
147147
}
148148

@@ -153,7 +153,7 @@ fn projection_equality() {
153153
} yields[SolverChoice::slg_default()] {
154154
// this is wrong, chalk#234
155155
"Ambiguous"
156-
} yields[SolverChoice::recursive()] {
156+
} yields[SolverChoice::recursive_default()] {
157157
"Unique; substitution [?0 := Uint(U32)]"
158158
}
159159
}
@@ -183,7 +183,7 @@ fn projection_equality_priority1() {
183183
} yields[SolverChoice::slg_default()] {
184184
// this is wrong, chalk#234
185185
"Ambiguous"
186-
} yields[SolverChoice::recursive()] {
186+
} yields[SolverChoice::recursive_default()] {
187187
// This is.. interesting, but not necessarily wrong.
188188
// It's certainly true that based on the impls we see
189189
// the only possible value for `U` is `u32`.
@@ -271,7 +271,7 @@ fn projection_equality_priority2() {
271271
// use the impl, but the SLG solver can't decide between
272272
// the placeholder and the normalized form.
273273
"Ambiguous; definite substitution for<?U1> { [?0 := S1, ?1 := ^0.0] }"
274-
} yields[SolverChoice::recursive()] {
274+
} yields[SolverChoice::recursive_default()] {
275275
// Constraining Out1 = S1 gives us only one choice, use the impl,
276276
// and the recursive solver prefers the normalized form.
277277
"Unique; substitution [?0 := S1, ?1 := Uint(U32)], lifetime constraints []"
@@ -298,7 +298,7 @@ fn projection_equality_from_env() {
298298
} yields[SolverChoice::slg_default()] {
299299
// this is wrong, chalk#234
300300
"Ambiguous"
301-
} yields[SolverChoice::recursive()] {
301+
} yields[SolverChoice::recursive_default()] {
302302
"Unique; substitution [?0 := Uint(U32)]"
303303
}
304304
}
@@ -326,7 +326,7 @@ fn projection_equality_nested() {
326326
} yields[SolverChoice::slg_default()] {
327327
// this is wrong, chalk#234
328328
"Ambiguous"
329-
} yields[SolverChoice::recursive()] {
329+
} yields[SolverChoice::recursive_default()] {
330330
"Unique; substitution [?0 := Uint(U32)]"
331331
}
332332
}
@@ -368,7 +368,7 @@ fn iterator_flatten() {
368368
} yields[SolverChoice::slg_default()] {
369369
// this is wrong, chalk#234
370370
"Ambiguous"
371-
} yields[SolverChoice::recursive()] {
371+
} yields[SolverChoice::recursive_default()] {
372372
"Unique; substitution [?0 := Uint(U32)]"
373373
}
374374
}
@@ -720,7 +720,7 @@ fn normalize_under_binder() {
720720
} yields[SolverChoice::slg_default()] {
721721
// chalk#234, I think
722722
"Ambiguous"
723-
} yields[SolverChoice::recursive()] {
723+
} yields[SolverChoice::recursive_default()] {
724724
"Unique; substitution [?0 := I32], lifetime constraints []"
725725
}
726726

@@ -743,7 +743,7 @@ fn normalize_under_binder() {
743743
} yields[SolverChoice::slg_default()] {
744744
// chalk#234, I think
745745
"Ambiguous"
746-
} yields[SolverChoice::recursive()] {
746+
} yields[SolverChoice::recursive_default()] {
747747
"Unique; substitution [?0 := Ref<'!1_0, I32>], lifetime constraints []"
748748
}
749749

@@ -1038,7 +1038,7 @@ fn guidance_for_projection_on_flounder() {
10381038
<Range<T> as Iterator>::Item = U
10391039
}
10401040
}
1041-
} yields[SolverChoice::recursive()] {
1041+
} yields[SolverChoice::recursive_default()] {
10421042
"Ambiguous; definite substitution for<?U0> { [?0 := ^0.0, ?1 := ^0.0] }"
10431043
}
10441044
}

‎tests/test/unify.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -166,7 +166,7 @@ fn unify_quantified_lifetimes() {
166166
InEnvironment { environment: Env([]), goal: '^0.0: '!1_0 }\
167167
] \
168168
}"
169-
} yields[SolverChoice::recursive()] {
169+
} yields[SolverChoice::recursive_default()] {
170170
// only difference is in the value of ?1, which is equivalent
171171
"Unique; for<?U0> { \
172172
substitution [?0 := '^0.0, ?1 := '^0.0], \

0 commit comments

Comments
 (0)