Why do I need to run clpfd:label/1 for my query to terminate?

3
votes

Here's a prolog session:

?- use_module(library(clpfd)).
true.

?- Large #>= Small, Small #> 0, length([1, 2], Large).
Large = 2,
Small in 1..2.

?- Large #>= Small, Small #> 0, length([1, 2], Large), length(List, Small).
Large = 2,
Small = 1,
List = [_5770] ;
Large = Small, Small = 2,
List = [_5770, _5776] ;
^CAction (h for help) ? abort
% Execution Aborted
?- Large #>= Small, Small #> 0, length([1, 2], Large), label([Small]), length(List, Small).
Large = 2,
Small = 1,
List = [_4464] ;
Large = Small, Small = 2,
List = [_4478, _4484].

?-

The first query works just fine. The second query loops forever once it's enumerates all the solutions. The third query works, but I don't know why.

Is this just the way clpfd works, I always need to call label before I try to use the constrained variables?

1
prologclpfd
Extremely related, here's another question which discusses non-termination when using clpfd and length/2: stackoverflow.com/questions/32478193/… – num1

1 Answers

2
votes

In a sense, this occurs because you are using "too little" clpfd: In current Prolog systems, length/2 does not take pending constraints into account!

I leave it as a challenge to implement a variant of length/2 that does. Ideally though, it should also work with CLP(B), CLP(Q) etc.! The way to make solvers cooperate with such predicates in general is not yet clear.