% 6.a

:- op(200, fy, -). % NOT
:- op(210, yfx, *). % AND
:- op(220, yfx, +). % OR
:- op(230, xfy, ->). % IMPLIKACE
:- op(240, xfx, <->). % EKVIVALENCE
:- op(260, xfy, :). 

vyhodnot(true,_,true).
vyhodnot(false,_,false).
vyhodnot(X,S,H):-prvek(X:H,S).
vyhodnot(-F,S,H):-vyhodnot(F,S,HF),not(HF,H).
vyhodnot(F*G,S,H):-vyhodnot(F,S,HF),vyhodnot(G,S,HG),and(HF,HG,H).
vyhodnot(F+G,S,H):-vyhodnot(F,S,HF),vyhodnot(G,S,HG),or(HF,HG,H).
vyhodnot(F->G,S,H):-vyhodnot(F,S,HF),vyhodnot(G,S,HG),imp(HF,HG,H).
vyhodnot(F<->G,S,H):-vyhodnot(F,S,HF),vyhodnot(G,S,HG),equiv(HF,HG,H).

prvek(X,[X|_]).
prvek(X,[_|L]):-prvek(X,L).

not(true,false).
not(false,true).

and(true,true,true).
and(false,_,false).
and(_,false,false).

or(true,_,true).
or(_,true,true).
or(false,false,false).

imp(true,true,true).
imp(false,_,true).
imp(true,false,false).

equiv(true,true,true).
equiv(false,false,true).
equiv(true,false,false).
equiv(false,true,false).



% 6.b

splnitelna(F):-sp(F,S),!,ohodnot(S,SH),vyhodnot(F,SH,true),!.

sp(true,[]).
sp(false,[]).
sp(X,[X]):-atomic(X).
sp(-F,S):-sp(F,S).
sp(F*G,S):-sp(F,SF),sp(G,SG),merge(SF,SG,S).
sp(F+G,S):-sp(F,SF),sp(G,SG),merge(SF,SG,S).
sp(F->G,S):-sp(F,SF),sp(G,SG),merge(SF,SG,S).
sp(F<->G,S):-sp(F,SF),sp(G,SG),merge(SF,SG,S).


conc([],S,S).
conc([Y|S],T,[Y|U]):-conc(S,T,U).

%merge(X,[],X):- !.
merge([],X,X):- !.
merge([H|T],X,Z):-prvek(H,X),!,merge(T,X,Z).
merge([H|T],X,[H|Z]):-merge(T,X,Z).

ohodnot([],[]).
ohodnot([X],[X:true]).
ohodnot([X],[X:false]).
ohodnot([X|Xs],[X:true|Zb]):-ohodnot(Xs,Zb).
ohodnot([X|Xs],[X:false|Zb]):-ohodnot(Xs,Zb).

% 6.c

:- op(210, yfx, *).
:- op(220, yfx, +).
:- op(230, yfx, -).
:- op(230, yfx, .).
:- op(240, yfx, ^).
:- op(260, xfy, :). 


mnozina(S,_,S):-je_seznam(S).
mnozina(X,Tp,S):-prvek(X:S,Tp).
mnozina(A+B,Tp,S):-mnozina(A,Tp,As),mnozina(B,Tp,Bs),merge(As,Bs,S).
mnozina(A*B,Tp,S):-mnozina(A,Tp,As),mnozina(B,Tp,Bs),kart(As,Bs,S).
mnozina(A.B,Tp,S):-mnozina(A,Tp,As),mnozina(B,Tp,Bs),intersect(As,Bs,S).
mnozina(A-B,Tp,S):-mnozina(A,Tp,As),mnozina(B,Tp,Bs),sub(As,Bs,S).
mnozina(A^B,Tp,S):-mnozina(A,Tp,As),mnozina(B,Tp,Bs),merge(As,Bs,U),intersect(As,Bs,I),sub(U,I,S).

je_seznam([]).
je_seznam([_|T]):-je_seznam(T).

intersect([],_,[]).
intersect([H|T],X,[H|V]):-prvek(H,X),!,intersect(T,X,V).
intersect([H|T],X,V):-intersect(T,X,V).

kart([],_,[]).
kart([A|As],B,V):-k2(A,B,V1),kart(As,B,V2),conc(V1,V2,V),!.

k2(_,[],[]).
k2(A,[B|Bs],V):-k2(A,Bs,V1),conc([[A,B]],V1,V).

smaz_vse(X,[X|Zb],V):-smaz_vse(X,Zb,V).
smaz_vse(X,[Y|Zb],[Y|V]):-smaz_vse(X,Zb,V).
smaz_vse(_,[],[]).

sub(A,[],A).
sub(A,[B|Bs],V):-sub(A,Bs,V1),smaz_vse(B,V1,V),!.