:- ensure_loaded(to_cnf).
:- use_module('../Basis/translations.pl').
:- ensure_loaded('../Basis/internal_operators.pl').

%
%  clauses(+Formula, -Clauses)
%    Clauses is a set of clauses that is logically equivalent to Formula
%
clauses(Formula, Clauses) :-
	cnf(Formula, CNFFormula),
        cnf_to_clausal(CNFFormula, Clauses).

%
%  cnf_to_clausal(+CNFFormula, -Clauses)
%
cnf_to_clausal(Disjuncts and ConjunctsOfDisjuncts, Clauses) :- !,
	cnf_to_clausal(Disjuncts, FirstClause),
	cnf_to_clausal(ConjunctsOfDisjuncts, OtherClauses),
	append(FirstClause, OtherClauses, Clauses).
cnf_to_clausal(Disjuncts, Clause) :-
	disjunction_to_list(Disjuncts, List), 
	sort(List, Set),	             % Remove duplicates and sort
	(   member(Atom, Set),	             % Replace clause containing
	    member(neg Atom, Set), !,        % an atom and its negation 
	    Clause = []                      % by the empty clause
	;   Clause = [Set]
	).

%
%  disjunction_to_list(+Disjuncts, -Clause)
%
disjunction_to_list(Atom or Disjuncts, [Atom| Atoms]) :- !,
	disjunction_to_list(Disjuncts, Atoms).
disjunction_to_list(Atom, [Atom]).

%
%  write_clauses(+Clauses)
%
write_clauses([]) :- !,
	write([]).
write_clauses(Clauses) :-
	write_clauses1(Clauses).

%
%  write_clauses1(+Clauses)
%
write_clauses1([H|T]) :-
	maplist(from_internal_to_printable, H, H1),
	write(H1), write('  '),
	write_clauses1(T).
write_clauses1([]).