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

%
%  prenex(+Formula, -PrenexFormula)
%    B is logically equivalent to A and in prenex form
%
prenex(Formula, PrenexFormula) :-
	eliminate_equiv_xor(Formula, Formula1),
	rename_variables(Formula1, Formula2),
	prenex1(Formula2, PrenexFormula).

%
%  prenex1(+Formula, -PrenexFormula)
%
prenex1(exists X sep A, exists X sep A1) :- !,
	prenex1(A, A1).
prenex1(forall X sep A, forall X sep A1) :- !,
	prenex1(A, A1).
prenex1(neg exists X sep A, forall X sep C) :-
	prenex1(neg A, C).
prenex1(neg forall X sep A, exists X sep C) :-
	prenex1(neg A, C).
prenex1(exists X sep A or B, exists X sep C) :- !,
	prenex1(A or B, C).
prenex1(forall X sep A or B, forall X sep C) :- !,
	prenex1(A or B, C).
prenex1(exists X sep A and B, exists X sep C) :- !,
	prenex1(A and B, C).
prenex1(forall X sep A and B, forall X sep C) :- !,
	prenex1(A and B, C).
prenex1(exists X sep A imp B, forall X sep C) :- !,
	prenex1(A imp B, C).
prenex1(forall X sep A imp B, exists X sep C) :- !,
	prenex1(A imp B, C).
prenex1(A or exists X sep B, exists X sep C) :- !,
	prenex1(A or B, C).
prenex1(A or forall X sep B, forall X sep C) :- !,
	prenex1(A or B, C).
prenex1(A and exists X sep B, exists X sep C) :- !,
	prenex1(A and B, C).
prenex1(A and forall X sep B, forall X sep C) :- !,
	prenex1(A and B, C).
prenex1(A imp exists X sep B, exists X sep C) :- !,
	prenex1(A imp B, C).
prenex1(A imp forall X sep B, forall X sep C) :- !,
	prenex1(A imp B, C).
prenex1(neg A, C) :-
        (   contains_quantifiers(A), !,
	    prenex1(A, A1),
	    prenex1(neg A1, C)
	;   C = neg A
	).
prenex1(A or B, C) :-
        (   contains_quantifiers(A), !,
	    prenex1(A, A1),
	    prenex1(A1 or B, C)
        ;   contains_quantifiers(B), !,
	    prenex1(B, B1),
	    prenex1(A or B1, C)
	;   C = A or B
	).
prenex1(A and B, C) :-
        (   contains_quantifiers(A), !,
	    prenex1(A, A1),
	    prenex1(A1 and B, C)
        ;   contains_quantifiers(B), !,
	    prenex1(B, B1),
	    prenex1(A and B1, C)
	;   C = A and B
	).
prenex1(A imp B, C) :-
        (   contains_quantifiers(A), !,
	    prenex1(A, A1),
	    prenex1(A1 imp B, C)
        ;   contains_quantifiers(B), !,
	    prenex1(B, B1),
	    prenex1(A imp B1, C)
	;   C = A imp B
	).
prenex1(A, A).