Prolog Test ist immer wahr var (Summe) Fehler

Question

Ich versuche, ein SWI-Prolog-Programm zu kompilieren, aber immer test is always true, var (sum) error on line 7. Ich kann nicht herausfinden, was das bedeutet. Kann mir bitte jemand helfen? Dies ist ein Programm, von dem ich hoffe, dass es lateinische Quadrate lösen wird. Vielen Dank.

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

Es ist eine Warnung, kein Fehler.

Ich habe einige Zeit erneut eine Anfrage auf SWI-Prolog Mailing-Liste für dieses Problem, da einige vorhandenen Code begonnen, diese Warnung nach einer Verfeinerung zu Nachrichten ausgelöst. Here ist die Antwort von Jan.

Ich denke, Sie können die Warnung ignorieren oder deaktivieren, aber das scheint nicht ratsam.

Answer 2

Wenn eine Zeile besteht aus drei ganzen Zahlen zwischen 1 und 3, und diese ganzen Zahlen müssen verschieden sein, dann ist die Summe einer solchen Zeile muss 6 (per Definition) sein. Die Angabe, dass die Summe einer solchen Zeile gleich 6 ist, ist daher eine Leerlaufbedingung. Die gleiche Überlegung gilt für die "Spalten", für die Sie ähnliche Disjointabhängigkeiten geltend machen.

Bearbeiten: Auch wenn die obige Argumentation richtig ist, ist dies nicht der Ursprung der Warnung. Carlo ist damit einverstanden, es hängt einfach davon ab, wie die Constraint-Bibliothek die Constraints neu schreibt.

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

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

test1/0 die Warnung gibt, tut test2/0 nicht. Dennoch fällt es mir schwer zu erkennen, warum die Warnung überhaupt gegeben wird, d. H. Was der Grund dafür ist. Zum Beispiel, hier ist die Erweiterung der test1/0 (meine Kommentare bemerken):

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