Prolog test is always true var(sum) error

Question

I am trying to compile a SWI-Prolog program but keep getting test is always true, var (sum) error on line 7. I cant figure out what this means. Can someone please help? This is a program I am hoping will eventually solve Latin squares. Thank you.

:- use_module(library(clpfd)).

magic_counter(Count) :-
    findall(a, magic_1(_Soln), As),
    length(As, Count).

magic_1(Soln) :-
    Row1 = [W1, W2, W3],
    Row2 = [X1, X2, X3],
    Row3 = [Y1, Y2, Y3],

    Row1 ins 1..3,
    Row2 ins 1..3,
    Row3 ins 1..3,

    Sum #= 6,

    all_different(Row1),
    all_different(Row2),
    all_different(Row3),

    all_different([W1,X1,Y1]),
    all_different([W2,X2,Y2]),
    all_different([W3,X3,Y3]),

    W1 + W2 + W3 #= Sum,
    X1 + X2 + X3 #= Sum,
    Y1 + Y2 + Y3 #= Sum,

    W1 + X1 + Y1 #= Sum,
    W2 + X2 + Y2 #= Sum,
    W3 + X3 + Y3 #= Sum,

    append(Row1,Row2,Row12),
    append(Row12,Row3,Soln),

    labeling([], Soln).

Answer 1

It's a warning, not an error.

I posted some time again a request on SWI-Prolog mailing list for this problem, since some existing code begun to raise this warning after a refinement to messages. Here is the answer from Jan.

I think you can ignore the warning, or disable it, but this seems not advisable.

Answer 2

If a row consists of three integers between 1 and 3, and these integers must be distinct, then the sum of such a row must be 6 (by definition). Stating that the sum of such a row equals 6 is therefore an idle constraint. The same reasoning applies to the 'columns' for which you assert similar disjointness constraints.

Edit: Even though the above reasoning is correct, this is not the origin of the warning. Carlo is right on this, it simply depends on the way in which the constraint library rewrites the constraints.

test1:-
  L = [X],
  L ins 1..2,
  Y #= 2,
  X #= Y.

test2:-
  L = [X],
  L ins 1..2,
  X #= 2.

test1/0 gives the warning, test2/0 does not. Still, I find it difficult to see why the warning is given in the first place, i.e. what the rational behind it is. For example, here is the expansion of test1/0 (notice my comments):

:- use_module(library(clpfd)).

test1:-
  A=[D],
  A ins 1..2,
  (
    integer(B)
  ->
    (
      var(2)
    ->
      2 is B
    ;
      true
    ->
      B=:=2
    ;
      C is B,
      clpfd:clpfd_equal(C, 2)
    )
  ;
    true
  ->
    (
      var(B) % This does not throw a warning.
    ->
      B is 2
    ;
      C is 2,
      clpfd:clpfd_equal(B, C)
    )
  ;
    clpfd:clpfd_equal(B, 2)
  ),
  (
    integer(D)
  ->
    (
      var(B) % This throws a "Test is always true" warning.
    ->
      B is D
    ;
      integer(B)
    ->
      D=:=B
    ;
      E is D,
      clpfd:clpfd_equal(E, B)
    )
  ;
    integer(B)
  ->
    (
      var(D)
    ->
      D is B
    ;
      E is B,
      clpfd:clpfd_equal(D, E)
    )
  ;
    clpfd:clpfd_equal(D, B)
  ).