%% Thom Fruehwirth ECRC 1991-1993
%% 910528 started boolean,and,or constraints
%% 910904 added xor,neg constraints
%% 911120 added imp constraint
%% 931110 ported to new release
%% 931111 added card constraint 
%% 961107 Christian Holzbaur, SICStus mods

:- use_module(library(chr)).
:- use_module(library(lists)).
handler boole.

chr_option(debug_compile,on).

:-chr_constraint boolean/1, and/3, or/3, xor/3, neg/2, imp/2.

%% and/3 specification
%%and(0,0,0).
%%and(0,1,0).
%%and(1,0,0).
%%and(1,1,1).

and(0,X,Y) <=> Y=0.
and(X,0,Y) <=> Y=0.
and(1,X,Y) <=> Y=X.
and(X,1,Y) <=> Y=X.
and(X,Y,1) <=> X=1,Y=1.
and(X,X,Z) <=> X=Z.
and(X,Y,A) \ and(X,Y,B) <=> A=B.
and(X,Y,A) \ and(Y,X,B) <=> A=B.


%% or/3 specification
%%or(0,0,0).
%%or(0,1,1).
%%or(1,0,1).
%%or(1,1,1).

or(0,X,Y) <=> Y=X.
or(X,0,Y) <=> Y=X.
or(X,Y,0) <=> X=0,Y=0.
or(1,X,Y) <=> Y=1.
or(X,1,Y) <=> Y=1.
or(X,X,Z) <=> X=Z.
or(X,Y,A) \ or(X,Y,B) <=> A=B.
or(X,Y,A) \ or(Y,X,B) <=> A=B.



%% xor/3 specification
%%xor(0,0,0).
%%xor(0,1,1).
%%xor(1,0,1).
%%xor(1,1,0).

xor(0,X,Y) <=> X=Y.
xor(X,0,Y) <=> X=Y.
xor(X,Y,0) <=> X=Y.
xor(1,X,Y) <=> neg(X,Y).
xor(X,1,Y) <=> neg(X,Y).
xor(X,Y,1) <=> neg(X,Y).
xor(X,X,Y) <=> Y=0.
xor(X,Y,X) <=> Y=0.
xor(Y,X,X) <=> Y=0.
xor(X,Y,A) \ xor(X,Y,B) <=> A=B.
xor(X,Y,A) \ xor(Y,X,B) <=> A=B.



%% neg/2 specification
%%neg(0,1).
%%neg(1,0).

neg(0,X) <=> X=1.
neg(X,0) <=> X=1.
neg(1,X) <=> X=0.
neg(X,1) <=> X=0.
neg(X,X) <=> fail.
neg(X,Y) \ neg(Y,Z) <=> X=Z.	
neg(X,Y) \ neg(Z,Y) <=> X=Z.	
neg(Y,X) \ neg(Y,Z) <=> X=Z.	
%% Interaction with other boolean constraints
neg(X,Y) \ and(X,Y,Z) <=> Z=0.
neg(Y,X) \ and(X,Y,Z) <=> Z=0.
neg(X,Z) , and(X,Y,Z) <=> X=1,Y=0,Z=0.
neg(Z,X) , and(X,Y,Z) <=> X=1,Y=0,Z=0.
neg(Y,Z) , and(X,Y,Z) <=> X=0,Y=1,Z=0.
neg(Z,Y) , and(X,Y,Z) <=> X=0,Y=1,Z=0.
neg(X,Y) \ or(X,Y,Z) <=> Z=1.
neg(Y,X) \ or(X,Y,Z) <=> Z=1.
neg(X,Z) , or(X,Y,Z) <=> X=0,Y=1,Z=1.
neg(Z,X) , or(X,Y,Z) <=> X=0,Y=1,Z=1.
neg(Y,Z) , or(X,Y,Z) <=> X=1,Y=0,Z=1.
neg(Z,Y) , or(X,Y,Z) <=> X=1,Y=0,Z=1.
neg(X,Y) \ xor(X,Y,Z) <=> Z=1.
neg(Y,X) \ xor(X,Y,Z) <=> Z=1.
neg(X,Z) \ xor(X,Y,Z) <=> Y=1.
neg(Z,X) \ xor(X,Y,Z) <=> Y=1.
neg(Y,Z) \ xor(X,Y,Z) <=> X=1.
neg(Z,Y) \ xor(X,Y,Z) <=> X=1.
neg(X,Y) , imp(X,Y) <=> X=0,Y=1.
neg(Y,X) , imp(X,Y) <=> X=0,Y=1.



%% imp/2 specification (implication)
%%imp(0,0).
%%imp(0,1).
%%imp(1,1).

%% any pros by specifying imp/3 ???
%%imp(0,0,1).
%%imp(0,1,1).
%%imp(1,1,1).
%%imp(1,0,0).

imp(0,X) <=> true.
imp(X,0) <=> X=0.
imp(1,X) <=> X=1.
imp(X,1) <=> true.
imp(X,X) <=> true.
imp(X,Y),imp(Y,X) <=> X=Y.	

%% END handler boole


%% Aufgabe 1 ************************************************************
%% equiv/3

%equiv(0,0,1).
%equiv(0,1,0).
%equiv(1,0,0).
%equiv(1,1,1).

:-chr_constraint equiv/3.

%% equiv/3 may be definied by other boolean constraints, e.g.
equiv(X,Y,Z) <=> xor(X,Y,W), neg(W,Z).

equiv1 @ equiv(X, Y, Z) <=> X=0 | neg(Y, Z).
equiv2 @ equiv(X, Y, Z) <=> Y=0 | neg(X, Z).
equiv3 @ equiv(X, Y, Z) <=> Z=0 | neg(X, Y).
equiv4 @ equiv(X, Y, Z) <=> X=1 | Z=Y.
equiv5 @ equiv(X, Y, Z) <=> Y=1 | Z=X.
equiv6 @ equiv(X, Y, Z) <=> Z=1 | X=Y.
equiv7 @ equiv(X, Y, Z) <=> X=Y | Z=1.
equiv8 @ equiv(X, Y, Z) <=> X=Z | Y=1.
equiv9 @ equiv(X, Y, Z) <=> Y=Z | X=1.

% %% interaction with neg/2 and equiv/3
neg(X,Y) \ equiv(X,Y,Z) <=> Z=0.
neg(X,Z) \ equiv(X,Y,Z) <=> Y=0.
neg(Y,Z) \ equiv(X,Y,Z) <=> X=0.
neg(Y,X) \ equiv(X,Y,Z) <=> Z=0.
neg(Z,X) \ equiv(X,Y,Z) <=> Y=0.
neg(Z,Y) \ equiv(X,Y,Z) <=> X=0.

%% Aufgabe 2 ************************************************************

:-chr_constraint enum/1.

enum([])    <=> true.
enum([H|T]) <=> true | (H=1 ; H=0), enum(T).

tellTruth(Lehmann,Mueller,Schulze) :-
	neg(Mueller,MuellerLies),
	equiv(Lehmann,MuellerLies, 1),

	neg(Schulze,SchulzeLies),
	equiv(Mueller,SchulzeLies, 1),

 	neg(Lehmann,LehmannLies),
 	and(LehmannLies,MuellerLies,BothLie),
 	equiv(Schulze,BothLie, 1).

% :- tellTruth(Lehmann,Mueller,Schulze).
% Lehmann = 0,
% Mueller = 1,
% Schulze = 0 ?


%% Aufgabe 3 ************************************************************

cross(X,Y,A,B) :-
	and(X,Y,I1),
	
	neg(X,NX),
	or(NX,I1,I2),
	
	neg(Y,NY),
	or(NY,I1,I3),

	neg(I2,NI2),
	or(NI2,I1,I4),

	neg(I3,NI3),
	or(NI3,I1,I5),

	or(I4,I5,I6),

	and(I2,I6,A),
	and(I3,I6,B).

% | ?- cross(1,0,A,B).
% A = 0,
% B = 1 ? ;
% no

% | ?- cross(1,Y,1,B).
% B = 1,
% Y = 1 ? ;
% no

% | ?- cross(0,Y,A,B).
% B = 0,
% Y = A,
% neg(A,_A) ? ;
% no


% | ?- cross(X,Y,X,Y).
% neg(X,_A),
% neg(Y,_B),
% neg(_C,_D),
% neg(_E,_F),
% and(X,Y,_G),
% or(_A,_G,_C),
% or(_B,_G,_E),
% or(_D,_G,_H),
% or(_F,_G,_I),
% or(_H,_I,_J),
% and(_C,_J,X),
% and(_E,_J,Y) ? ;
% no

% | ?- cross(Y,X,X,Y).
% neg(Y,_A),
% neg(X,_B),
% neg(_C,_D),
% neg(_E,_F),
% and(Y,X,_G),
% or(_A,_G,_C),
% or(_B,_G,_E),
% or(_D,_G,_H),
% or(_F,_G,_I),
% or(_H,_I,_J),
% and(_C,_J,X),
% and(_E,_J,Y) ? ;
% no

% | ?- cross(X,Y,A,B).
% neg(X,_A),
% neg(Y,_B),
% neg(_C,_D),
% neg(_E,_F),
% and(X,Y,_G),
% or(_A,_G,_C),
% or(_B,_G,_E),
% or(_D,_G,_H),
% or(_F,_G,_I),
% or(_H,_I,_J),
% and(_C,_J,A),
% and(_E,_J,B) ? ;
% no

% | ?- cross(X,Y,A,B), neg(X,Y).
% X = B,
% Y = A,
% neg(B,A) ? ;
% no