Resolver trait

[dcz-self]

I've been trying to create a resolver for arithmetics and I found the interface of the trait to be somewhat confusing.

Here's the trait for reference:

pub trait Resolver {
    type Choice: fmt::Debug;

    fn resolve(
        &mut self,
        goal_id: term_arena::TermId,
        goal_term: term_arena::AppTerm,
        context: &mut ResolveContext,
    ) -> Option<Resolved<Self::Choice>>;

    /// Returns true if there's another resolution pending.
    fn resume(
        &mut self,
        choice: &mut Self::Choice,
        goal_id: term_arena::TermId,
        context: &mut ResolveContext,
    ) -> bool;
}

As far as I undestand it, the resolver exists to return a chain of results. Every result can either just match, which means "the statement is true", or instantiate a variable to some concrete value, and let the resolution process continue elsewhere. The first lack of match breaks the chain.
Did I get that right?

If yes, then Resolver::Choice reminds me of an Iterator a lot. Without getting into how all this works, I'd imagine returning an Iterator that yields which variable should take which value or stop, something along the lines of:

enum Choice {
 Substitute(Var, Term),
 Match,
}

pub trait Resolver {
    fn resolve(
        &mut self,
        goal_id: term_arena::TermId,
        goal_term: term_arena::AppTerm,
        context: &mut ResolveContext,
    ) -> impl Iterator<Item=Choice>;
}

If that doesn't make sense, I'm seeing a couple of less invasive rough edges with this API.

One simple thing is that ::resume returns a bool where it could return another choice:

/// Returning None means nothing more can be resolved.
fn resume(
        &mut self,
        choice: Self::Choice,
        goal_id: term_arena::TermId,
        context: &mut ResolveContext,
    ) -> Option<Self::Choice>;

Another thing is that Resolver::resolve duplicates ::resume when it returns the first result (e.g. in RuleResolver). I think this could be avoided by calling ::resume first thing after each ::resolve.
When I tried it, it becomes clear that while the normal place to fail and stop resolution is ::resume, sometimes ::resolve already wants to fail immediately, so that would lead to some weird overlap of function.
I decided not to make a pull request from what I have without confirming that it's even desireable.

---

This all ultimately comes from the need to have a CLP/FD approximation :P Scryer Prolog has some downsides compared to Logru.

[fatho]

That trait has grown organically, so there might indeed be a better representation.

Regarding your questions:

If yes, then Resolver::Choice reminds me of an Iterator a lot. Without getting into how all this works, I'd imagine returning an Iterator that yields which variable should take which value or stop, something along the lines of:

You're right, essentially, it's iterator-like: after the initial call to resolve, we have a suspended computation (represented through Self::Choice) which we can resume later to get yet another solution.

We cannot actually return an iterator however, because we need that mutable access to ResolveContext which we cannot capture in the iterator, because then the search engine would not be able to actually suspend the computation. (Since we don't consume the iterator all at once, but we need to be able to come back to it after proceeding with the search from whatever it yielded).

The reason the state changes are done through a mutable reference (rather than e.g. just returning a list of (variable, value) pairs) is performance. Making this search go fast was (and still is) my main priority, so any interface changes shouldn't compromise performance.

Another complication with an actual iterator is the OrElse combinator, which sees if the first resolver can resolve, and if so, commits to that choice (so if it fails to resume later, it does not go to the second one). Only if the initial resolve fails, it then tries and commits to the second resolver.

One simple thing is that ::resume returns a bool where it could return another choice:

The bool is indeed a bit uninformative. The downside with your proposed interface is that you then need to move out the Choice from the state in the search engine, only to put it back later. That's something to benchmark, but in similar situations (i.e. taking something out an Option, and putting it back later) in a different context had a small but consistent performance impact, compared to checking whether it's Some, and then taking a mutable ref.

Another thing is that Resolver::resolve duplicates ::resume when it returns the first result (e.g. in RuleResolver). I think this could be avoided by calling ::resume first thing after each ::resolve.

This might have been a choice I made in the name of performance too (but I don't quite remember anymore), as a fast path for singleton predicates that don't have additional choices. This would be something to benchmark.

But I think this would also be problematic again for the OrElse combinator, where you would want to know immediately whether

---

I decided not to make a pull request from what I have without confirming that it's even desireable.

My stance would be that any API improvements that do not make performance worse are desirable. Any API improvements that manage to improve performance as well would be extra desirable :)
But even if performance suffers, if there's a good reason (like unlocking new features or use-cases) and it seems worth taking the it, I'm also open to that.

This all ultimately comes from the need to have a CLP/FD approximation

I'm not very intimately familiar with those features of Prolog. Do you have a concrete example of what you want to do, maybe I can point you to where I think that would fit in the engine.

Scryer Prolog has some downsides compared to Logru.

I don't think I can nor should I want to compete with that :D

[dcz-self]

Can you give me a quick introduction to how you benchmark things? AFAIK cargo bench is just a nightly thing, so it's probably something else.

Do you have a concrete example of what you want to do, maybe I can point you to where I think that would fit in the engine.

I have a tree full of constraints, like:

level1(Width, Height) :-
  Width #< 4096, Width #> 4, Height #% 8 == 0
level2(Width, Height) :- Width #= 2*Height

they all need to combine and give the ultimate Width, Height constraints.
A nice resolver API would be good for experimentation.

My current open question is whether this is fast enough. A statement like 0 <= Width < 4096 creates 4096 integers in the resolver. Adding another 0 <= Width < 4096 is 4096*4096 due to both resolvers. Whereas in a CLP/FD system, the constraints are treated analytically.
I think this needs another basic data type with a special behaviour when another constraint is added. I could follow the way you added integers.

The output from Scryer does seem to support having an extra type:

?- X in 0..2, Y in 0..2.
   clpz:(X in 0..2), clpz:(Y in 0..2).

[fatho]

Can you give me a quick introduction to how you benchmark things? AFAIK cargo bench is just a nightly thing, so it's probably something else.

What's nightly is the built-in benchmark harness with #[bench] attributes. It's indeed just cargo bench, but it's running through criterion. It also allows you to compare two runs, so it's fairly straightforward to use.

---

Regarding the problem at hand, I think enumerating all possible values is likely not going to cut it, so working with constraints in a smarter way sounds like the way to go.

While reading up on CLP, I came across "attributed variables" which seems to be the foundation on which this can be built.

In the context of logru, perhaps something like this would work where resolvers can annotate variables, and then get called in a hook when a variable is actually unified to check those constraints. And for explicit enumeration, we could probably just have a special predicate of the resolver that knows how to solve the constraints and just assigns all possible values that remain after that.

So for example, if we have

foo(X) :- X #>= 4, X #<= 10

then the query foo(X), X = 3 would be executed in a way where foo(X) just annotates X with the constraints, and the assignment X = 3 then triggers the hook, which is allowed to fail the assignment (which it will in this case because the constraints are not fulfilled).

And then we could have a predicate enum(X) that for a constrained variable X enumerates all the values it can possibly have that are left. So foo(X), enum(X) would give 4, 5, .., 10 as solutions.

That's all just a very rough idea though, but hopefully enough to get started with.