RFC: Arithmetics

[dcz-self]

I gave it a try and added some arithmetics that are going to be required by my use case.

Unlike the existing ones, those I added are all predicates. They all require full instantiation, apart from IsNeg, which will negate an integer if not out of bounds.

Initially I wanted to make the predicates fill in variables with matching values, but that quickly leads to i64-sized loops.

While I don't expect logru to support clp(fd), I think there's a continuum of ways to make arithmetics resolve to something useful. With one variable, the syntax could look like:

is(Var, and(condition, ...)).

where the resolver could look at all conditions to see if they are bounded before proceeding.

Does that sound like anything desireable?

---

Another thing is the lack of messages when there's a variable which is not instantiated enough. I epect that to be the main thing driving people away. I could give it a shot and change impl Resolver to return an error message, and pass it all the way to the user. Interested?

[fatho]

Initially I wanted to make the predicates fill in variables with matching values, but that quickly leads to i64-sized loops.

Yeah, I don't think that's feasible. For the core Arithmetic resolver, I'd like to stick to deterministic evaluation, just like is in prolog (if I remember that part correctly).

While I don't expect logru to support clp(fd), I think there's a continuum of ways to make arithmetics resolve to something useful. With one variable, the syntax could look like:

is(Var, and(condition, ...)).

where the resolver could look at all conditions to see if they are bounded before proceeding.

Does that sound like anything desireable?

That does sound interesting. So essentially you'd restrict the domain of a variable through various conditions, and then it allows iteration over the remaining values?
I'd probably have to see it to say if it's something I'd like to maintain in this library 😅 But in any case, I think it should be best implemented as its own resolver extending the basic Arithmetic one (and keeping that one limited to simple, deterministic operations).
And since the solver core is reasonably open, such more specialized extensions could also be published as a separate crate if needed.

Another thing is the lack of messages when there's a variable which is not instantiated enough. I epect that to be the main thing driving people away. I could give it a shot and change impl Resolver to return an error message, and pass it all the way to the user. Interested?

A better way of reporting errors than just failing a goal is definitely something that's on my roadmap. I'm not sure yet what the best way to do this is. If you have a concrete idea, feel free to put it in an issue to discuss, or make a PR (depending on how much work it is, though if it's invasive, first discussing the idea might be better before you sink to much work into it).

[dcz-self]

more specialized extensions could also be published as a separate crate if needed.

Agreed, I'll be doing testing in my own sandbox for now.

If you have a concrete idea,

I'd just go bottom-up by putting errors in the places where they are found and let the bubble up until they are visible to the user.