3

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?

num1
  • 4,825
  • 4
  • 31
  • 49
  • 2
    Extremely related, here's another question which discusses non-termination when using clpfd and length/2: https://stackoverflow.com/questions/32478193/using-a-constrained-variable-with-length-2 – num1 Jun 22 '18 at 17:04

1 Answers1

2

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.

mat
  • 40,498
  • 3
  • 51
  • 78
  • 1
    Thanks for the answer! I'm not sure this is right though. I made a version which uses constraings: clp_length([], 0). clp_length([_Head|Rest], Length) :- Length #= Length1 + 1, clp_length(Rest, Length1). Using it does not, as far as I can tell, change the behavior of the above queries. – num1 Jun 22 '18 at 16:10
  • 3
    You are *extremely* close though: Adding the single additional constraint `Length #> 0` makes this work. A small suggestion: `list_length/2` is a *much* better name, because it indicates what the arguments of the predicate are! – mat Jun 22 '18 at 16:20
  • 1
    Thank you, I appreciate the help! I discovered this about 5 minutes after you posted, wished I had checked here first! This leads me to my next question though, I have no idea why that helps, it feels like a constraint which a constraint propagator should be able to propagate. I opened a question here wondering why: https://stackoverflow.com/questions/50992433/why-doesnt-this-clpfd-query-terminate-until-i-add-a-redundant-constraint – num1 Jun 22 '18 at 16:51
  • 1
    That's perfectly fine: It is appropriate to discuss different aspects and follow-up questions separately. This is definitely well worth its own question, so let us continue there! Preferably with a better predicate name though. – mat Jun 22 '18 at 16:53