Il test Prolog è sempre true var (sum) error

Question

Sto provando a compilare un programma SWI-Prolog ma continuo a ricevere test is always true, var (sum) error on line 7. Non riesco a capire cosa significhi. Qualcuno può aiutarmi per favore? Questo è un programma che spero risolverà alla fine i quadrati latini. Grazie.

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

E 'un avvertimento, non un errore.

Ho inviato qualche volta di nuovo una richiesta sulla mailing list SWI-Prolog per questo problema, dal momento che alcuni codici esistenti hanno iniziato a sollevare questo avviso dopo un perfezionamento dei messaggi. Here è la risposta da gennaio

Penso che si possa ignorare l'avviso o disattivarlo, ma questo non sembra consigliabile.

Answer 2

Se una riga è costituita da tre numeri interi compresi tra 1 e 3, e questi numeri interi deve essere distinto, allora la somma di tale riga deve essere 6 (per definizione). Affermando che la somma di una riga di questo tipo è uguale a 6 è quindi un vincolo di inattività. Lo stesso ragionamento si applica alle "colonne" per le quali si asseriscono vincoli di disgiunzione simili.

Modifica: Anche se il ragionamento sopra riportato è corretto, questa non è l'origine dell'avviso. Carlo ha ragione su questo, dipende semplicemente dal modo in cui la libreria dei vincoli riscrive i vincoli.

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

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

test1/0 dà l'avvertimento, test2/0 non lo fa. Tuttavia, trovo difficile capire perché l'avvertimento è dato in primo luogo, cioè quale sia la ragione dietro a ciò. Ad esempio, qui è l'espansione della test1/0 (notare i miei commenti):

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