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

%% 031119 Marc: labeling, boolean cardinality removed for exercices
%%              complete handler see webCHR

:- use_module(library(chr)).

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

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

%% 20050118 taken from WebCHR
%% 20050118 minor errors corrected (A is *abs(...)*), compute rules introduced, card2nand, card2xor introduced (Marc)

%% Boolean cardinality operator
%% card(A,B,L,N) constrains list L of length N to have between A and B 1s

:-chr_constraint card/4, labeling/0.

card(A,B,L):- 
 	length(L,N), 
 	A=<B,0=<B,A=<N,				%0=<N 	
 	card(A,B,L,N).

%% card/4 specification
%%card(A,B,[],0):- A=<0,0=<B.
%%card(A,B,[0|L],N):-
%%		N1 is N-1,
%%		card(A,B,L,N1).
%%card(A,B,[1|L],N):-  
%%		A1 is A-1, B1 is B-1, N1 is N-1,
%%		card(A1,B1,L,N1).

debug    @ card(A,B,L,N) ==> write('* '), write(card(A,B,L,N)), nl.

compute1 @ card(A,B,L,N) <=> \+ number(A) | A1 is abs(A), card(A1,B,L,N).
compute2 @ card(A,B,L,N) <=> \+ number(B) | B1 is abs(B), card(A,B1,L,N).
compute3 @ card(A,B,L,N) <=> \+ number(N) | N1 is abs(N), card(A,B,L,N1).

triv_sat @ card(A,B,L,N) <=> A=<0,N=<B | true.     % trivial satisfaction
pos_sat  @ card(N,B,L,N) <=> set_to(L,1).	         % positive satisfaction
neg_sat  @ card(A,0,L,N) <=> set_to(L,0).          % negative satisfaction

pos_red  @ card(A,B,L,N) <=> remove(1,L,L1) | card(A-1,B-1,L1,N-1). %  positive reduction												 
neg_red  @ card(A,B,L,N) <=> remove(0,L,L1) | card(A,B,L1,N-1). % negative reduction
                             
labeling, card(A,B,L,N) <=> label_card(A,B,L,N), labeling.

label_card(A,B,[],0)    :- A=<0,0=<B.
label_card(A,B,[0|L],_) :- card(A,B,L).
label_card(A,B,[1|L],_) :- A1 is A-1, B1 is B-1, card(A1,B1,L).

%% auxiliary predicates
set_to([],_).
set_to([V|L],V) :- set_to(L,V).

remove( X, [X|L],  L).
remove( Y, [X|Xs], [X|Xt]) :- 	remove( Y, Xs, Xt).


% constraints and/3, neg/2, or/3, nand/3, xor/3.

%% special cases with two variables
card2and   @ card(0,1,[X,Y],2) <=> and(X,Y,0).		
card2neg   @ card(1,1,[X,Y],2) <=> neg(X,Y).		
card2or    @ card(1,2,[X,Y],2) <=> or(X,Y,1).

%% special cases with three variables X,Y,Z

card2xor   @ card(3,3,[X,Y,Z,Z],4) <=> xor(X,Y,1).
card2nand  @ card(2,3,[X,Y,Z,Z],4) <=> nand(X,Y,Z).

% andneg @ nand(X,Y,Z) <=> and(X,Y,W), neg(W,Z).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% Aufgabe 2 CET

:-chr_constraint eq/2, neq/2, one_neq/2.

:-op(700, xfx, [neq, eq]).

idempotency   @ X eq Y \ X eq Y  <=> true.

reflexivity   @ X eq X           <=> true.
symmetry      @ X eq Y           ==> Y eq X.

acyclicity    @ X eq T           ==> var(X), nonvar(T), T=..[F|A], in(X,A) |
                                     fail.

transitivity  @ X eq Y, Y eq Z   ==> X eq Z.

%% changed to simplification to remove terms T1 and T2
decompostion  @ T1 eq T2         ==> nonvar(T1), nonvar(T2),
                                     same_functor(T1,T2) |
																		 T1=..[F|A1], T2=..[F|A2],
																		 eq_list(A1,A2).
contradiction @ T1 eq T2         ==> nonvar(T1), nonvar(T2),
                                     \+ same_functor(T1,T2) |
																		 fail.

%% problem to implement compatibility directly, use substitution instead
%% easy solution: use build-in = for substitution
substitution  @ Y eq T2 \ X eq T1 <=> var(X), nonvar(T2),
                                      T2=..[F|A], in(X, A) |
																		  X=T1.

%% aux

in(X,[H|_]) :- nonvar(H), H=..[_|A], in(X,A).
in(X,[H|_]) :- X==H.
in(X,[_|T]) :- in(X,T).

eq_list([],[]).
eq_list([H1|T1], [H2|T2]) :- H1 eq H2, eq_list(T1,T2).

same_functor(X,Y) :- functor(X,F,N), functor(Y,F,N).


%% END cet

%% | ?- p(a,X,c,Y,Z) eq p(Y,X,c,a,W).
%% Y = a,
%% Z = W ? ;
%% no
%% | ?- p(Y,g(Y,f(Y)),g(X,a)) eq p(f(U),V,g(h(U,V,W),U)).
%% U = a,
%% V = g(f(a),f(f(a))),
%% X = h(a,g(f(a),f(f(a))),W),
%% Y = f(a) ? ;
%% no
%% | ?- p(g(X),h(a,X),h(Y,Y)) eq p(U,h(a,g(V)),h(V,g(U))).
%% no
%% | ?- p(h(f(X),a),X,h(f(f(X)),f(f(X)))) eq p(h(V,a),U,h(W,f(V))).
%% V = f(U),
%% W = f(f(U)),
%% X = U ? ;
%% no



%% BEGIN neq Aufgabe 3


irreflexivity @ X neq X           <=> fail.

orientation   @ X neq Y           <=> Y @< X | Y neq X.

difference    @ T1 neq T2         <=> nonvar(T1), nonvar(T2),
                                      \+ same_functor(T1,T2) |
																			true.

decompostion  @ T1 neq T2         <=> nonvar(T1), nonvar(T2),
                                      same_functor(T1,T2) |
 																	    T1=..[F|A1], T2=..[F|A2],
																			one_neq(A1,A2).

cyclicity     @ X neq T           <=> var(X), nonvar(T), T=..[F|A], in(X,A) |
                                      true.

one_neq([],[])            <=> fail.
one_neq([H1],[H2])        <=> H1 neq H2. % more efficient, no extra choicepoint
one_neq([H1|T1], [H2|T2]) <=> true | (H1 neq H2 ; one_neq(T1, T2)).

%% END neq

%% | ?- X neq f(X).
%% true ? ;
%% no
%% % source_info
%% | ?- f(a,X) neq f(X,Y).
%% X neq a ? ;
%% X neq Y ? ;
%% no
%% % source_info
%% | ?- f(g(X),a) neq f(Y,X).
%% Y neq g(X) ? ;
%% X neq a ? ;
%% no
%% % source_info