search

mthom / scryer-prolog

A modern Prolog implementation written mostly in Rust.
BSD 3-Clause "New" or "Revised" License
2.01k stars 117 forks source link

CLP(B): Slow projection of residual goals #2434

Open triska opened 3 months ago

triska commented 3 months ago

With the following libraries loaded:

:- use_module(library(clpb)).
:- use_module(library(lists)).
:- use_module(library(debug)).

We have:

?- length(Ls, 12), sat(+Ls), false.
   false.   % very fast termination

Yet, generalizing away false at the end, we have:

?- length(Ls, 12), sat(+Ls), * false.
% slow!

This means that the projection of residual goals in library(clpb) is slow in this situation and others like it!

I would greatly appreciate any help with improving this. For instance, starting from https://github.com/mthom/scryer-prolog/blob/d6ac03552d8484f8ad7c4307d1c9cfb5db46b16f/src/lib/clpb.pl#L1691 what exactly is so slow here, and which cases are affected?

Second, what do we actually want to guarantee in residual goals of library(clpb)? It would be great to have a set of sensible test cases, using copy_term/3 to reason about residual goals, and ideally systematically testing many cases, even exhaustively.

Third, can we improve the speed while retaining useful guarantees that residual goals satisfy?

@bakaq, @notoria: Since you have already made tremendous contributions involving residual goals and constraints, I hope this issue could likewise interest you particularly. I would greatly appreciate your help with this. Thank you a lot!

notoria commented 3 months ago

With copy_term/3:

?- length(Ls, 12), sat(+Ls), time(copy_term(Ls, _, _)), false.
% slow

The slow starts here: https://github.com/mthom/scryer-prolog/blob/d6ac03552d8484f8ad7c4307d1c9cfb5db46b16f/src/lib/clpb.pl#L1915

Generalizing from there and any goals that come after makes it faster.