Prolog 测试始终为真 var(sum) 错误

Question

我正在尝试编译一个 SWI-Prolog 程序，但不断收到 test is always true, var (sum) error on line 7。我无法弄清楚这意味着什么。有人可以帮忙吗？这是一个我希望最终能解决拉丁方格的程序。谢谢。

:- 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

这是一个警告，而不是错误。

我再次在 SWI-Prolog 邮件列表上发布了针对此问题的请求，因为一些现有代码在对消息进行改进后开始引发此警告。 Here 是一月的回答。

我认为您可以忽略该警告，或禁用它，但这似乎不可取。

Answer 2

如果一行由1 和3 之间的三个整数组成，并且这些整数必须是不同的，那么这样一行的总和必须是6（根据定义）。因此，声明这样一行的总和等于6 是一个空闲约束。相同的推理适用于您断言类似不相交约束的“列”。

编辑：尽管上述推理是正确的，但这并不是警告的来源。 Carlo 在这一点上是对的，它只是取决于约束库重写约束的方式。

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

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

test1/0 给出警告，test2/0 没有。尽管如此，我还是很难理解为什么首先给出警告，即它背后的原因是什么。比如这里是test1/0的扩展（注意我的cmets）：

:- 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)
  ).