% upravene podla
%   Ivan Bratko: Prolog Programming for Artificial Intelligence (4th Edition)
%                Pearson Education Canada, 2011


:- op(100, fy, ~).
:- op(110, xfy, &).
:- op(120, xfy, v).
:- op(130, xfy, =>).
:- op(140, xfy, <=>).


uprav(X, Y) :-
    nl, print(X), nl,
    transform(X,Z),
    (X = Z, Y = Z;
     uprav(Z,Y)
    ), !.


literal(X) :- atom(X).
literal(~ X) :- atom(X).


transform(X <=> Y, (X => Y) & (Y => X)) :- tlac(X <=> Y, "eliminacia ekvivalencie").

transform(X => Y, ~X v Y) :- tlac(X => Y, "eliminacia implikacie").

transform(~ ( X v Y ), ~X & ~Y) :- tlac(~( X v Y ), "DeMorganov zakon").
transform(~ ( X & Y ), ~X v ~Y) :- tlac(~( X & Y ), "DeMorganov zakon").

transform(~ ( ~ X ), X) :- tlac(~ ( ~ X ), "dvojita negacia").

transform(X & Y v Z, (X v Z) & (Y v Z)) :-
    tlac(X & Y v Z, "distribucny zakon (or nad and)"). 
transform(X v Y & Z, (X v Y) & (X v Z)) :-
    tlac(X v Y & Z, "distribucny zakon (and over or)").

transform((X v Y) v Z, X v (Y v Z)) :- tlac((X v Y) v Z, "asociativny zakon").
transform((X & Y) & Z, X & (Y & Z)) :- tlac(X & (Y & Z), "asociativny zakon").

transform(~X v Y, true) :- obsahuje_or(X,Y), tlac(~X v X, "true").
transform(X v Y, true) :- obsahuje_or(~X,Y), tlac(X v ~X, "true").
transform(Y, true) :- obsahuje_or(true,Y), tlac(true v Y, "true").

transform(true & X, X) :- tlac(true & X, "pohltenie").
transform(X & true, X) :- tlac(X & true, "pohltenie").
transform(X & Y, Y) :- obsahuje_and(X,Y), tlac(X & Y, "pohltenie").

transform(X v Y, Y) :- literal(X), obsahuje_or(X,Y), tlac(X, "deduplikacia").

transform(X v Y, X1 v Y1) :- 
    tlac(X v Y, "kontrola kazdeho clena dizjunkcie"),
    (literal(X), X1 = X; transform(X, X1)),
    (literal(Y), Y1 = Y; transform(Y, Y1)).

transform(X & Y, X1 & Y1) :- 
    tlac(X & Y, "kontrola kazdeho clena konjunkcie"),
    (literal(X), X1 = X; transform(X, X1)),
    (literal(Y), Y1 = Y; transform(Y, Y1)).


obsahuje_or(X,X).
obsahuje_or(X,X v _).
obsahuje_or(X,_ v X).
obsahuje_or(X,_ v Z) :- obsahuje_or(X,Z).


obsahuje_and(X,Y) :- pohlcuje(Y,X).
obsahuje_and(X,Y & _) :- pohlcuje(Y,X).
obsahuje_and(X,_ & Y) :- pohlcuje(Y,X).
obsahuje_and(X,_ & Z) :-obsahuje_and(X,Z).


pohlcuje(X,Y) :- literal(X), obsahuje_or(X,Y).
pohlcuje(X v Y, Z) :- literal(X), obsahuje_or(X,Z), pohlcuje(Y,Z). 


%tlac(X,Y) :-
%  print(na), print(' '), print(X),
%  print(' '), print(aplikujem), print(' '), print(Y), nl.
tlac(_,_).


% Priklady
%
%  uprav( p <=> (x v y) & (~x v ~y), X).
%
%  uprav( ~( (~a v ~b) & (~a v ~c) & (~b v ~c)) , X).
%
%  uprav( ~( (~a v ~b) & (~a v ~c) & (~a v ~d) & (~b v ~c) & (~b v ~d) & (~c v ~d)) , X).