:- op(300,xfx,[and,or]).
:- op(200,fy,[not]).

gerador_de_tabelas( Expressao ):- nl,
   isole_variaveis( Expressao, Vars ), % Vars é o conjunto de variáveis em Expressão.
   length( Vars, N ), % número de variaveis em Vars.
   gerador_binario( N, ValoresBinarios ), % gera todas as combinacoes binarias possiveis para as N variaveis binarias   
   avalie_expr( ValoresBinarios, Vars, Expressao, Tabela ),
   imprima_tabela( Expressao, Vars, Tabela ).

isole_variaveis(Expr1 or Expr2,Vars):- !,
    isole_variaveis(Expr1,Vars1),
    isole_variaveis(Expr2,Vars2),
    uniao(Vars1,Vars2,Vars).  
isole_variaveis(Expr1 and Expr2,Vars):- !,
    isole_variaveis(Expr1,Vars1),
    isole_variaveis(Expr2,Vars2),
    uniao(Vars1,Vars2,Vars).
isole_variaveis(not Expr,Vars):- !,
    isole_variaveis(Expr,Vars).
isole_variaveis(X,[X]).   
   
imprima_tabela(Expr, Vars, Tabela):-
   write(Vars),  tab(7),  write(Expr),nl,
   write('---------------------------------------------'),nl,
   imprime_tab(Tabela).
   
imprime_tab([(V,R)|Tab]):-
   write(V),tab(15),write(R),nl,
   !,
   imprime_tab(Tab).
imprime_tab([]):- 
   write('---------------------------------------------'),nl.
  
gerador_binario(N,[Zeros|Vs]):-
   vetor(N,0,Zeros), % gera uma lista com N zeros 
   gera(N,Zeros,Vs).


avalie_expr([V|Vs],Vars,Expressao,[(V,R)|Tab]):-
   associe(V,Vars,Expressao,Expressao1), % associa os valores binarios em V as variaveis Vars em Expr
   tabela_verdade(Expressao1,R), % usa a tabela verdade para determinar o valor da expressao Expr1
   !,
   avalie_expr(Vs,Vars,Expressao,Tab).
avalie_expr([],_,_,[]).

associe([V|Vs],[Var|Vars],Expr1,Expr):-
   substituir(Var,V,Expr1,Expr2),
   !,
   associe(Vs,Vars,Expr2,Expr).
associe([],[],Expr,Expr).

tabela_verdade(1 or _Expr,1):- !.
tabela_verdade(0 or Expr,R):- !,
   tabela_verdade(Expr,R).
tabela_verdade(Expr1 or Expr2,R):-
   tabela_verdade(Expr1,R1),
   tabela_verdade(Expr2,R2),
   !,
   tabela_verdade(R1 or R2,R).
tabela_verdade(0 and _Expr,0):- !.
tabela_verdade(1 and Expr,R):- !,
   tabela_verdade(Expr,R).
tabela_verdade(Expr1 and Expr2,R):-
   tabela_verdade(Expr1,R1),
   tabela_verdade(Expr2,R2),
   !,
   tabela_verdade(R1 and R2,R).   
tabela_verdade(not Expr,R):-
   tabela_verdade(Expr,R1),
   !,
   nao(R1,R).
tabela_verdade(X,X).

nao(0,1).
nao(1,0).

substituir(Var, V, Expr1 or Expr2, Expr1_s or Expr2_s ):-
    substituir(Var, V, Expr1, Expr1_s),
    substituir(Var, V, Expr2, Expr2_s),
	!.	
substituir(Var, V, Expr1 and Expr2, Expr1_s and Expr2_s ):-
    substituir(Var, V, Expr1, Expr1_s),
    substituir(Var, V, Expr2, Expr2_s),
	!.	
substituir(Var,V,not Expr,not Expr_s):- !,
    substituir(Var,V,Expr,Expr_s).
substituir(Var,V,Var,V).
substituir(_,_,Var,Var).


gera(N,Anterior,[]):-
   vetor(N,1,Anterior). % Anterior é uma lista com N 1's.
gera(N,Anterior,[Atual|Proximos]):-
   sucessor(Anterior,Atual),
   !,
   gera(N,Atual,Proximos).
   

vetor(1,X,[X]).
vetor(N,X,[X|Zs]):-
  N > 1, !,
  N1 is N - 1,
  vetor(N1,X,Zs).

sucessor(Xs,Ys):-
  inverte(Xs,Sx), % inverte uma lista
  soma_1(Sx,Sx1),
  inverte(Sx1,Ys).

soma_1([0|Xs],[1|Xs]).
soma_1([1|Xs],[0|Ys]):-
  soma_1(Xs,Ys).
  

inverte(Xs,Sx):-
  inverte(Xs,[],Sx).

inverte([X|Xs],Ac,Sx):- !,
  inverte(Xs,[X|Ac],Sx).
inverte([],Ac,Ac).

uniao([X|Xs],Y,[X|Zs]):-
   not (member(X,Y)), !,
   uniao(Xs,Y,Zs).
uniao([X|Xs],Y,Zs):-
   member(X,Y), !,
   uniao(Xs,Y,Zs).
uniao([],Y,Y).

member(X,[X|_]):- !.
member(X,[_|Y]):- 
   member(X,Y).

concatena([X|Xs],Ys,[X|Zs]):- !,
   concatena(Xs,Ys,Zs).
concatena([],Ys,Ys).

%%%   Dados de Teste

%     O predicado abaixo foi feito para medir algumas caracteristiscas deste 
% programa em tempo de execucao
estatisticas(N):- 
   time(teste(N)),
   statistics(atoms,A),
   statistics(functors,F),   
   statistics(predicates,P),
   statistics(codes,C),
   write('Numero total de definicoes de atomos = '),write(A),nl,
   write('Numero total de pares nome/aridade definidos = '),write(F),nl,
   write('Numero total de definicoes de predicados = '),write(P),nl,
   write('Numero total de byte codes em todas as clausulas '),write(C),nl.

teste(N):-
 expressao(N,Expr),gerador_de_tabelas(Expr).

expressao(1,x or (not y and z)).
expressao(2,not x and y).
expressao(3,x or not x).
expressao(4,x and not y).
expressao(5, (x and y) and not(not x or not y)). % lei de De Morgan
expressao(6, (x and (y or z)) and ((x and y) or (x and z))). % distributiva