%%%%%Основните неща от езика:
?-sat([p,and,[n,q]]).
%Логически променливи
is_var_(X):-is_var_dpll(X).
is_var_(X):-is_var_2(X).
%is_var1(X) - съвместими с dpll частта
is_var_dpll(p).
is_var_dpll(q).
is_var_dpll(r).
is_var_dpll(u).
is_var_dpll(v).
is_var_dpll(w).
%is_var2(X) - могат да се използват само за другите алгоритми
is_var_2(p0).
is_var_2(p1).
is_var_2(p2).
is_var_2(p3).
is_var_2(q0).
is_var_2(q1).
is_var_2(q2).
is_var_2(q3).
is_var_2([var, X]):-nat(X).


%Истинни стойности (константи). Разпознавател и генератор.
hitme(0).
hitme(1).

%Двузначни логически съюзи. Разбира се, използваме 'and' за конюнкция, 'or' за
%дизюнкция, 'imp' за импликация и 'equ' за еквиваленция. Също използваме 'n' за
%отрицание, но това се използва директно във формулите.
logical_conj2(and).
logical_conj2(or).
logical_conj2(imp).
logical_conj2(equ).


%Формули - следваме стандартната индуктивна дефиниция за формула, с разликата,
%че константите 0 и 1 също са формули.
%Формулите се представят със списъци. Можем да използваме 'cut' за да ускорим
%малко нещата, поради еднозначното представяне на формулите.
is_formula(X):-hitme(X),!.
is_formula(X):-is_var_(X),!.
is_formula([n, F]):-is_formula(F),!.
is_formula([F1, OP, F2]):-
  logical_conj2(OP),
  is_formula(F1),
  is_formula(F2),!.
%%%%%


%%%%%Разни неща, които се използват по-късно:
%varset(F+, R-): помощен предикат, който по дадена формула връща множеството на
%променливите й (като списък). 
%Разбира се това множество се определя индуктивно:
varset(X, []):-hitme(X),!.
varset(X, [X]):-is_var_(X),!.
varset([n, F], R):-varset(F, R),!.
varset([F1, OP, F2], R):-
  logical_conj2(OP),
  varset(F1, R1),
  varset(F2, R2),
  union_(R1, R2, R),!.

%subformula_(F+, X-): при преудовлетворяване последователно в X всички подформули
%на F. 
%subformula_(F+, X+): Също и разпознавател! (...нали?)
subformula_(F, F):-hitme(F),!.
subformula_(F, F):-is_var_(F),!.
subformula_(F, F).
subformula_([n, F], X):-subformula_(F, X).
subformula_([F1, OP, _], X):-logical_conj2(OP), subformula_(F1, X).
subformula_([_, OP, F2], X):-logical_conj2(OP), subformula_(F2, X).

%subforulas(F+, S-) - връща множеството (без повторения) от всички подформули на F в S.
subformulas(X, [X]):-hitme(X),!.
subformulas(X, [X]):-is_var_(X),!.
subformulas([n, F], [[n,F]|S]):-subformulas(F, S),!.
subformulas([F1, OP, F2], S):-
  logical_conj2(OP),
  subformulas(F1, S1),
  subformulas(F2, S2),
  union_([[F1, OP, F2]| S1], S2, S3),   
  set_(S3, S),!.


%%%%%value
%value(F+, V-): по дадена формула с празно множество от променливи (например,
%формули, в които променливите са заменени от константи), връща стойността й.
%Отново, дефиницията е индуктивна.

%Константите:
value(X, X):-hitme(X),!.

%Отрицание:
value([n, F], V):-value(F, VF), V is 1-VF,!.

%Конюнкция:
value([F1, and, F2], 1):-
  value(F1, V1), value(F2, V2),
  V1 == 1, V2 == 1,!.
value([_, and, _], 0):-!.

%Дизюнкция:
value([F1, or, F2], 0):-
  value(F1, V1), value(F2, V2),
  V1 == 0, V2 == 0,!.
value([_, or, _], 1):-!.

%Импликация:
value([F1, imp, F2], 0):-
  value(F1, V1), value(F2, V2),
  V1 == 1, V2 == 0,!.
value([_, imp, _], 1):-!.

%Еквиваленция:
value([F1, equ, F2], 1):-
  value(F1, V1), value(F2, V2),
  V1 == V2,!.
value([_, equ, _], 0):-!.
%%%%%value


%replace(F+, S+, X+, R-): във формулата F, замества всички срещания на S като
%подформула със X. Връща резултата в R.
replace(F, V, _, F):-
  not(subformula_(F, V)),!.
replace(F, F, X, X):-!.
replace([n, F], V, X, [n, R]):-replace(F, V, X, R),!.
replace([F1, OP, F2], V, X, [R1, OP, R2]):-
  logical_conj2(OP),
  replace(F1, V, X, R1),
  replace(F2, V, X, R2),!.
%%%%%



%%%%%Това вероятно няма да се използва:
%gen_values(F+, R-): при преудовлетворяване генерира във R всички възможни
%формули получени при заместването на променливите на F с константите 0 и 1
%(внимание: това са 2**n формули, където n е броя (различни) променливи в F).
%По-подходящо име?
gen_values(F, F):-varset(F, []),!.
gen_values(F, R):-
  varset(F, [V|_]),
  hitme(X),
  replace(F, V, X, R1),
  gen_values(R1, R).


%Накрая проверката за тавтология може да стане лесно (но бавно...):
not_tautology_lazy(F):-gen_values(F,R), value(R, X), X == 0.
is_tautology_lazy(F):-not(not_tautology_lazy(F)).

%Както и проверката за противоречие:
not_contradiction_lazy(F):-gen_values(F,R), value(R, X), X == 1.
is_contradiction_lazy(F):-not(not_contradiction_lazy(F)).



%%%%%Еквивалентни преобразования
%По-подходящи имена?
%replace_equ(F+, R-): замества формулите от вида (A <=> B) с еквивалентното
%(n(A) or B) and (A or n(B))
replace_equ(F,R):-subformula_(F, [A, equ, B]),!, 
  replace(F, [A, equ, B],   [ [[n,A], or, B], and, [A, or, [n, B]] ], R1),
  replace_equ(R1, R).
replace_equ(F,F):-!.  %тук стига само когато subformula_ не успее

%replace_imp(F+, R-): замества формулите от вида (A => B) с еквивалентното (n(A) or B)
replace_imp(F,R):-subformula_(F, [A, imp, B]),!, 
  replace(F, [A, imp, B], [[n,A], or, B], R1),
  replace_imp(R1, R).
replace_imp(F,F):-!.

%replace_dn(F+, R-): премахва двойните отрицания
replace_dn(F, R):-subformula_(F, [n, [n, A]]),!,
  replace(F, [n, [n, A]], A, R1),
  replace_dn(R1,R).
replace_dn(F,F):-!.

%replace_dm1(F+, R-): преобразува F по единия закон на Де Морган -- замества
%n(A and B)   с   (n(A) or n(B))
replace_dm1(F,R):-subformula_(F, [n, [A, and, B]]),!,
  replace(F, [n, [A, and, B]], [[n,A], or, [n,B]], R1),
  replace_dm1(R1, R).
replace_dm1(F,F):-!.

%replace_dm2(F+, R-): преобразува F по другия закон на Де Морган -- замества
%n(A or B)   с   (n(A) and n(B))
replace_dm2(F,R):-subformula_(F, [n, [A, or, B]]),!,
  replace(F, [n, [A, or, B]], [[n,A], and, [n,B]], R1),
  replace_dm2(R1, R).
replace_dm2(F,F):-!.

%replace_dist1(F+, R-): преобразува F по единия дистрибутивен закон -- замества
%C and (A or B)   с   (C and A) or (C and B)   и
%(A or B) and C   със същото.
%FIX: Не съм сигурен, че това работи коректно!
replace_dist1(F, R):-subformula_(F, [C, or, [A, and, B]]),!,
  replace(F, [C, or, [A, and, B]], [[C, or, A], and, [C, or, B]], R1),
  replace_dist1(R1,R).
replace_dist1(F, R):-subformula_(F, [[A, and, B], or, C]),!,
  replace(F, [[A, and, B], or, C], [[C, or, A], and, [C, or, B]], R1),
  replace_dist1(R1,R).
replace_dist1(F,F):-!.

%replace_dist2(F+, R-): засега не трябва
%%%%%



%%%%%Форми на формулите
%is_nnf(F+) - успява, ако F е в негативна нормална форма --- ако в F няма => и <=>, няма двойни
%отрицания и всички отрицания са пред променливи (в случая може и пред константи)
is_nnf(F):-not(not_nnf(F)).
not_nnf(F):-subformula_(F, [_, imp, _]),!.
not_nnf(F):-subformula_(F, [_, equ, _]),!.  %може да се оптимизира, subformula_ е бавно
not_nnf(F):-subformula_(F, [n, X]), not(is_var_(X)), not(hitme(X)),!.

%nnf(F+, R-) - връща в R негативна нормална форма на F. Работи по следния начин:
%Първо заменя => и <=> с еквивалентни формули над {and, or, n}. След това, докато
%формулата не е в негативна нормална форма прави преобразувания по законите на Де Морган
%и премахва двойните отрицания. Винаги след краен брой такива преобразувания формулата 
%се свежда до ННФ (?).
nnf(F,R):-replace_equ(F,R1),
  replace_imp(R1, R2),
  nnf_help(R2, R).
nnf_help(F, F):-is_nnf(F),!.
nnf_help(F, R):-replace_dm1(F,R1), 
  replace_dm2(R1, R2),
  replace_dn(R2,R3),
  nnf_help(R3, R),!.


%is_cnf(F+): конюнктивна нормална форма
is_cnf(F):-not(not_cnf(F)).
not_cnf(F):-not(is_nnf(F)),!.
not_cnf(F):-subformula_(F, [ [A, and, B], or, C ]),!.  %дизюнкциите трябва да са елементарни
not_cnf(F):-subformula_(F, [ C, or, [A, and, B] ]),!.

%cnf(F+,R-)
cnf(F,R):-nnf(F, FN), cnf_help(FN, R).
cnf_help(F, F):-is_cnf(F),!.
cnf_help(F, R):-replace_dist1(F, R1),
  replace_dn(R1, R2), 
  cnf_help(R2, R),!.

%cnf_to_list(F+, R-): по дадена F в КНФ връща в R списъка с елементарните дизюнкции на F
cnf_to_list(F, R):-subformula_(F, [D1, and, D2]),
  cnf_to_list(D1, R1),
  cnf_to_list(D2, R2),
  union_(R1, R2, R),!.
cnf_to_list(F, [F]):-!.   %когато няма подформула конюнкция

%is_taut_ed(F+): успява ако елементарната дизюнкция F е тавтология. Това е
%изпълнено, точно когато една променлива и нейното отрицание участват в F, или,
%понеже позволихме участието на константи във формулата, когато 1 участва.
is_taut_ed(F):-subformula_(F, 1),!.
%FIX: грозно ;)
is_taut_ed(F):-subformula_(F, [n, V]), replace(F, [n, V], whatever, R), subformula_(R, V),!.

%is_taut_cnf(L+): успява, когато всяка елементарна дизюнкция от списъка L е тавтология
is_taut_cnf([]):-!.
is_taut_cnf([H|T]):-is_taut_ed(H),is_taut_cnf(T).

%is_tautology(F+): успява, ако F е тавтология. За целта привежда F в КНФ. Тя е
%тавтология, точно когато всяка елементарна дизюнкция е тавтология.
is_tautology(F):-cnf(F, FC),
  cnf_to_list(FC, FL),
  is_taut_cnf(FL).

%is_contradiction(F+): успява, ако F е противоречие. F е противоречие точно
%когато n(F) е тавтология.
is_contradiction(F):-is_tautology([n, F]).


%list_to_dpll(L+, R-): преобразува списък от елементарни дизюнкции във формата,
%използван от dpll частта. 
list_to_dpll([], []):-!.
list_to_dpll([H|T], [H2| T2]):-is_list(H),flatten(H, H1),
  deleteall(or, H1, H2),
  list_to_dpll(T, T2),!.
list_to_dpll([H|T], [ [H] | T2]):-list_to_dpll(T,T2),!.


%Разни (скучни) помощни неща:
value1(F,V):-replace1(F,R),value(R,V).
replace1(X, X):-hitme(X),!.
replace1(X, 1):-is_var_(X),!.
replace1([n, X], [n, R]):-replace1(X, R).
replace1([F1, OP, F2], [R1, OP, R2]):-logical_conj2(OP),
  replace1(F1, R1),
  replace1(F2, R2),!.


nat(0).
nat(N):-N>=0,nat(M), N is M+1.

%Връща множеството от елементи на даден списък (маха повторенията):
set_([], []):-!.
set_([H|T], S):-member_(H,T), set_(T, S),!.
set_([H|T], [H|S]):-set_(T,S),!.

member_(X, [X|_]).
member_(X, [_|T]):-member(X,T).

union_([], L, L) :- !.
union_([H|T], L, R) :-
	member(H, L), !, 
	union_(T, L, R).
union_([H|T], L, [H|R]) :-
	union_(T, L, R).

%pretty write
pwrite([H|T]):-write(H), nl, pwrite(T).
pwrite(_):-nl,nl.

%При дадена формула генерира възможните стойности на променливите и изписва
%получената формула и нейната стойност.
write_values(F):-gen_values(F,R), value(R,V), write(R), nl, write(V), nl,nl.