pvar(p). % definition of propositional variables
pvar(q).
pvar(r).
literal(n(L)) :- pvar(L), !. % definition of literals
literal(L) :- pvar(L).

clause(U) :- literal(U). %unit clause, has only one literal
clause(o(C1, C2)) :-
	  clause(C1)
	, clause(C2).


formula(C) :- clause(C). %unit formula, has only one clause
formula(a(F1, F2)) :-
	  formula(F1)
	, formula(F2).


nnf(X, X) :- literal(X). % NNF of literal is itself

nnf(n(n(X)), NNF) :- nnf(X, NNF). % double negation

nnf(a(A, B), a(Na, Nb)) :-
	  nnf(A, Na)
	, nnf(B, Nb). % and: (A === Na && B === Nb) -> ((A && B) === (Na && Nb))
nnf(n(a(A, B)), o(NnA, NnB)) :-
	  nnf(n(A), NnA)
	, nnf(n(B), NnB). % nand: (!A === NnA && !B === NnB) -> !(A && B) === (NnA || NnB)
nnf(o(A, B), o(Na, Nb)) :-
	  nnf(A, Na)
	, nnf(B, Nb). % or: (A === Na && B === Nb) -> (A || B === Na || Nb)
nnf(n(o(A, B)), a(NnA, NnB)) :-
	  nnf(n(A), NnA)
	, nnf(n(B), NnB). % nor: (!A === NnA && !B === NnB) -> (!(A || B) === NnA && NnB)
nnf(i(A, B), o(Na, Nb)) :-
	  nnf(n(A), Na)
	, nnf(B, Nb). % implication: (!A === Na && B === Nb) -> (A->B === Na || Nb)
nnf(n(i(A, B)), a(Na, NnB)) :-
	  nnf(A, Na)
	, nnf(n(B), NnB). % nimplication: (A === Na && !B === NnB) -> (!(A->B) === Na && NnB)
nnf(e(A, B), o(a(NA, NB), a(NnA, NnB))) :-
	  nnf(A, NA)
	, nnf(n(A), NnA)
	, nnf(B, NB)
	, nnf(n(B), NnB). % equivalence: (A === NA && !A === NnA && B === NB && !B === NnB) -> (A <-> B) === (NA && NB) || (NnA && NnB)
nnf(n(e(A, B)), o(a(NA, NnB), a(NnA, NB))) :-
	  nnf(A, NA)
	, nnf(n(A), NnA)
	, nnf(B, NB)
	, nnf(n(B), NnB). % nequivalence: (A === NA && !A === NnA && B === NB && !B === NnB) -> !(A <-> B) === (NA && NnB) || (NnA && NB)


% cnf(F, X): takes a propositional formula F as input and converts F into an
% equivalent formula X in CNF

nnf2cnf(CNF, CNF) :- formula(CNF), !.

nnf2cnf(NNF, CNF) :-
	  NNF = a(NNF_1, NNF_2)
	, nnf2cnf(NNF_1, CNF_1)
	, nnf2cnf(NNF_2, CNF_2)
	, CNF = a(CNF_1, CNF_2)
	, !.

nnf2cnf(NNF, CNF) :-
	  NNF = o(NNF_1, NNF_2)
	, nnf2cnf(NNF_1, CNF_1)
	, nnf2cnf(NNF_2, CNF_2)
	, (
		(clause(CNF_1), clause(CNF_2)) ->
			CNF = o(CNF_1, CNF_2)
		;
			(
			  (CNF_1 = a(C_n_1, CNF_n_1), CNF_m = CNF_2)
			; (CNF_2 = a(C_n_1, CNF_n_1), CNF_m = CNF_1)
	  		)
	  		, NNF_1_prime = o(C_n_1, CNF_m)
	  		, NNF_2_prime = o(CNF_n_1, CNF_m)
	  		, nnf2cnf(NNF_1_prime, CNF_1_prime)
	  		, nnf2cnf(NNF_2_prime, CNF_2_prime)
	  		, CNF = a(CNF_1_prime, CNF_2_prime)

	  )
	, !.

cnf(F, CNF) :-
	  nnf(F, NNF)
	, nnf2cnf(NNF, CNF).

%%a(a(p,q),a(o(n(p),a(p,n(q))),o(q,a(p,n(q)))))
%% a(p,q) && (n(p) || (p && n(q)) && (q || a(p,n(q))))
%% ? - nnf2cnf(a(a(p,q),o(a(p,n(q)),a(n(p),q))))
%% p && q && o(a(p,n(q)),a(n(p),q))

%% % ? - cnf(n(o(n(a(p,q)),e(p,q))), X).
% X = a(a(p,q),a(o(p,q),o(n(p),n(q))))
% X = {p,q,{p,q},{-p,-q}}
