chalk_engine/
solve.rs

1use crate::context::{AnswerResult, AnswerStream};
2use crate::forest::Forest;
3use crate::slg::aggregate::AggregateOps;
4use crate::slg::SlgContextOps;
5use chalk_ir::interner::Interner;
6use chalk_ir::{Canonical, ConstrainedSubst, Goal, InEnvironment, UCanonical};
7use chalk_solve::{RustIrDatabase, Solution, Solver, SubstitutionResult};
8
9use std::fmt;
10
11pub struct SLGSolver<I: Interner> {
12    pub(crate) forest: Forest<I>,
13    pub(crate) max_size: usize,
14    pub(crate) expected_answers: Option<usize>,
15}
16
17impl<I: Interner> SLGSolver<I> {
18    pub fn new(max_size: usize, expected_answers: Option<usize>) -> Self {
19        Self {
20            forest: Forest::new(),
21            max_size,
22            expected_answers,
23        }
24    }
25}
26
27impl<I: Interner> fmt::Debug for SLGSolver<I> {
28    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
29        write!(fmt, "SLGSolver")
30    }
31}
32
33impl<I: Interner> Solver<I> for SLGSolver<I> {
34    fn solve(
35        &mut self,
36        program: &dyn RustIrDatabase<I>,
37        goal: &UCanonical<InEnvironment<Goal<I>>>,
38    ) -> Option<Solution<I>> {
39        let ops = SlgContextOps::new(program, self.max_size, self.expected_answers);
40        ops.make_solution(goal, self.forest.iter_answers(&ops, goal), || true)
41    }
42
43    fn solve_limited(
44        &mut self,
45        program: &dyn RustIrDatabase<I>,
46        goal: &UCanonical<InEnvironment<Goal<I>>>,
47        should_continue: &dyn std::ops::Fn() -> bool,
48    ) -> Option<Solution<I>> {
49        let ops = SlgContextOps::new(program, self.max_size, self.expected_answers);
50        ops.make_solution(goal, self.forest.iter_answers(&ops, goal), should_continue)
51    }
52
53    fn solve_multiple(
54        &mut self,
55        program: &dyn RustIrDatabase<I>,
56        goal: &UCanonical<InEnvironment<Goal<I>>>,
57        f: &mut dyn FnMut(SubstitutionResult<Canonical<ConstrainedSubst<I>>>, bool) -> bool,
58    ) -> bool {
59        let ops = SlgContextOps::new(program, self.max_size, self.expected_answers);
60        let mut answers = self.forest.iter_answers(&ops, goal);
61        loop {
62            let subst = match answers.next_answer(|| true) {
63                AnswerResult::Answer(answer) => {
64                    if !answer.ambiguous {
65                        SubstitutionResult::Definite(answer.subst)
66                    } else if answer
67                        .subst
68                        .value
69                        .subst
70                        .is_identity_subst(ops.program().interner())
71                    {
72                        SubstitutionResult::Floundered
73                    } else {
74                        SubstitutionResult::Ambiguous(answer.subst)
75                    }
76                }
77                AnswerResult::Floundered => SubstitutionResult::Floundered,
78                AnswerResult::NoMoreSolutions => {
79                    return true;
80                }
81                AnswerResult::QuantumExceeded => continue,
82            };
83
84            if !f(subst, !answers.peek_answer(|| true).is_no_more_solutions()) {
85                return false;
86            }
87        }
88    }
89}
chalk_engine/solve.rs

chalk_engine/
solve.rs
