Skip to content

Allow limiting search time using fuel #227

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 1 commit into from
Closed

Allow limiting search time using fuel #227

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 12 additions & 1 deletion chalk-engine/src/forest.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -85,6 +86,7 @@ impl<C: Context> Forest<C> {
context,
table,
answer,
fuel,
}
}

Expand All @@ -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
Expand Down Expand Up @@ -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>
Expand All @@ -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;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think if we're going to have fuel, then the return type of this function needs to change to something like Result<Option<..>, OutOfFuel>, so we can return Err(OutOfFuel) here. Returning None will (incorrectly) cause the system to conclude that there are no more possible answers, which will (I believe..) affect caching and future answers. That's not really what we want.

That said, I'm not yet 100% sold on the concept of fuel -- we may want it eventually, but I think I'd prefer to push on addressing the slowdown issues in other ways to start.

Although I suppose that, in the end, the system is turing complete, and it's possible for users to put us in a computationally expensive position no matter what. The current system guarantees termination but only by bounding the maximum size of types we can create and other such tricks, which means that recursion may wind up taking quite a bit of time and wasting quite a bit of resources before ultimately terminating.

Actually, I think that I'd prefer not to add a fuel parameter here in any case, but instead to make this function return a Result and then propagate back the QuantumExceeded failures (instead of looping). Then we can move the loop further out, which seems fine. (The more we can push fuel out from the "inner loop", I think, the better.)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Then we can move the loop further out, which seems fine. (The more we can push fuel out from the "inner loop", I think, the better.)

A related thing we've discussed is that we might want to enable cancellation of chalk queries. That might also benefit from pushing logic for "stop/continue" to the outer loop.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll get back to this after I'm done with rust-lang/rust-analyzer#1408. I also think moving the outer loop further out might be a good idea because it'll allow us to add cancellation checks as well.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've tried a bit to find a good way to push the outer loop to rust-analyzer, but haven't had success so far. The problem is that constructing an answer requires searching until we've found one, and then continuing until it's clear whether there's a second answer, so something needs to keep that state...

}
*fuel -= 1;
}
match self
.forest
.ensure_root_answer(self.context, self.table, self.answer)
Expand Down
32 changes: 30 additions & 2 deletions chalk-solve/src/solve.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down