:- ensure_loaded('../Basis/internal_operators.pl').
:- ensure_loaded('../Basis/utilities.pl').

%
%  cnf(+A, -B)
%    A is a quantifier free formula;
%    B is logically equivalent to A and in conjunctive normal form
%
cnf(A, A4) :-
	eliminate_equiv_xor_imp(A, A1),
	de_morgan(A1, A2),
	distribute_or_over_and(A2, A3),
	right_associate(A3, A4).
%
%  right_associate(+A, -B)
%    A is a quantifier free formula in conjunctive normal form,
%    but possibly with conjunctions of groups of conjuncts
%    and with disjunctions of groups of disjuncts;
%    B is logically equivalent to A,
%    with conjunction applied from right to left
%    and with disjunction applied from right to left,
%    so that as few parentheses as possible are used for printing
%
right_associate((A and B) and C, F) :- !,
	right_associate(A and (B and C), F).
right_associate(A and B, A1 and B1) :- !,
	right_associate(A, A1),
	right_associate(B, B1).
right_associate((A or B) or C, F) :- !,
	right_associate(A or (B or C), F).
right_associate(A or B, A1 or B1) :- !,
	right_associate(A, A1),
	right_associate(B, B1).
right_associate(A, A).