Allow limiting search time using fuel

To use Chalk in an IDE environment, we need to be able to prevent it from taking
too much time, even if that means getting a wrong or incomplete answer.
This is done by specifying an amount of 'fuel'; each iteration of the top-level
search loop takes one unit of fuel, and when it runs out, we return.

Author: flodiebold

chalk-engine/src/forest.rs

@@ -77,6 +77,7 @@ impl<C: Context> Forest<C> {
         &'f mut self,
         context: &'f impl ContextOps<C>,
         goal: &C::UCanonicalGoalInEnvironment,
+        fuel: Option<usize>,
     ) -> impl AnswerStream<C> + 'f {
         let table = self.get_or_create_table_for_ucanonical_goal(context, goal.clone());
         let answer = AnswerIndex::ZERO;
@@ -85,6 +86,7 @@ impl<C: Context> Forest<C> {
             context,
             table,
             answer,
+            fuel,
         }
     }
 
@@ -95,8 +97,9 @@ impl<C: Context> Forest<C> {
         &mut self,
         context: &impl ContextOps<C>,
         goal: &C::UCanonicalGoalInEnvironment,
+        fuel: Option<usize>,
     ) -> Option<C::Solution> {
-        context.make_solution(C::canonical(&goal), self.iter_answers(context, goal))
+        context.make_solution(C::canonical(&goal), self.iter_answers(context, goal, fuel))
     }
 
     /// True if all the tables on the stack starting from `depth` and
@@ -148,6 +151,7 @@ struct ForestSolver<'me, C: Context + 'me, CO: ContextOps<C> + 'me> {
     context: &'me CO,
     table: TableIndex,
     answer: AnswerIndex,
+    fuel: Option<usize>,
 }
 
 impl<'me, C, CO> AnswerStream<C> for ForestSolver<'me, C, CO>
@@ -157,6 +161,13 @@ where
 {
     fn peek_answer(&mut self) -> Option<SimplifiedAnswer<C>> {
         loop {
+            if let Some(fuel) = &mut self.fuel {
+                if *fuel == 0 {
+                    // TODO: would it be better to return an ambiguous answer?
+                    return None;
+                }
+                *fuel -= 1;
+            }
             match self
                 .forest
                 .ensure_root_answer(self.context, self.table, self.answer)

chalk-solve/src/solve.rs

@@ -113,19 +113,47 @@ impl Solver {
     ///     each time you invoke `solve`, as otherwise the cached data may be
     ///     invalid.
     /// - `goal` the goal to solve
+    /// - `fuel` if `Some`, this limits how much time the solver spends before giving up.
     ///
     /// # Returns
     ///
     /// - `None` is the goal cannot be proven.
     /// - `Some(solution)` if we succeeded in finding *some* answers,
     ///   although `solution` may reflect ambiguity and unknowns.
-    pub fn solve(
+    pub fn solve_with_fuel(
         &mut self,
         program: &dyn RustIrDatabase,
         goal: &UCanonical<InEnvironment<Goal>>,
+        fuel: Option<usize>,
     ) -> Option<Solution> {
         let ops = self.forest.context().ops(program);
-        self.forest.solve(&ops, goal)
+        self.forest.solve(&ops, goal, fuel)
+    }
+
+    /// Attempts to solve the given goal, which must be in canonical
+    /// form. Returns a unique solution (if one exists).  This will do
+    /// only as much work towards `goal` as it has to (and that work
+    /// is cached for future attempts).
+    ///
+    /// # Parameters
+    ///
+    /// - `program` -- defines the program clauses in scope.
+    ///   - **Important:** You must supply the same set of program clauses
+    ///     each time you invoke `solve`, as otherwise the cached data may be
+    ///     invalid.
+    /// - `goal` the goal to solve
+    ///
+    /// # Returns
+    ///
+    /// - `None` is the goal cannot be proven.
+    /// - `Some(solution)` if we succeeded in finding *some* answers,
+    ///   although `solution` may reflect ambiguity and unknowns.
+    pub fn solve(
+        &mut self,
+        program: &dyn RustIrDatabase,
+        goal: &UCanonical<InEnvironment<Goal>>,
+    ) -> Option<Solution> {
+        self.solve_with_fuel(program, goal, None)
     }
 
     pub fn into_test(self) -> TestSolver {