:- module(utility, [eliminate_equiv_xor/2,
		    eliminate_equiv_xor_imp/2,
		    de_morgan/2,
		    distribute_or_over_and/2,
		    distribute_and_over_or/2,
		    instance/4,
                    instances/4,
		    rename_variables/2,
		    contains_quantifiers/1,
		    has_no_occurrence_in/2,
		    has_no_free_occurrence_in/2]).

:- ensure_loaded(internal_operators).

%
%  eliminate_equiv_xor(+A, -B)
%    A is a formula built from all available logical operators;
%    B is logically equivalent to A and contains neither equivalence
%    nor exclusive or
%
eliminate_equiv_xor(A eqv B, (A1 imp B1) and (B1 imp A1)) :- !,
	eliminate_equiv_xor(A, A1),
	eliminate_equiv_xor(B, B1).
eliminate_equiv_xor(A xor B, (A1 and neg B1) or (neg A1 and B1)) :- !,
	eliminate_equiv_xor(A, A1),
	eliminate_equiv_xor(B, B1).
eliminate_equiv_xor(neg A, neg A1) :- !,
	eliminate_equiv_xor(A, A1).
eliminate_equiv_xor(A or B, A1 or B1) :- !,
	eliminate_equiv_xor(A, A1),
	eliminate_equiv_xor(B, B1).
eliminate_equiv_xor(A and B, A1 and B1) :- !,
	eliminate_equiv_xor(A, A1),
	eliminate_equiv_xor(B, B1).
eliminate_equiv_xor(exists X sep A, exists X sep A1) :- !,
	eliminate_equiv_xor(A, A1).
eliminate_equiv_xor(forall X sep A, forall X sep A1) :- !,
	eliminate_equiv_xor(A, A1).
eliminate_equiv_xor(A, A).

%
%  eliminate_equiv_xor_imp(+A, -B)
%    A is a formula built from all available logical operators;
%    B is logically equivalent to A and contains neither equivalence
%    nor exclusive or nor implication
%
eliminate_equiv_xor_imp(A eqv B, (A1 and B1) or (neg A1 and neg B1)) :- !,
	eliminate_equiv_xor_imp(A, A1),
	eliminate_equiv_xor_imp(B, B1).
eliminate_equiv_xor_imp(A xor B, (A1 and neg B1) or (neg A1 and B1)) :- !,
	eliminate_equiv_xor_imp(A, A1),
	eliminate_equiv_xor_imp(B, B1).
eliminate_equiv_xor_imp(A imp B, neg A1 or B1) :- !,
	eliminate_equiv_xor_imp(A, A1),
	eliminate_equiv_xor_imp(B, B1).
eliminate_equiv_xor_imp(neg A, neg A1) :- !,
	eliminate_equiv_xor_imp(A, A1).
eliminate_equiv_xor_imp(A or B, A1 or B1) :- !,
	eliminate_equiv_xor_imp(A, A1),
	eliminate_equiv_xor_imp(B, B1).
eliminate_equiv_xor_imp(A and B, A1 and B1) :- !,
	eliminate_equiv_xor_imp(A, A1),
	eliminate_equiv_xor_imp(B, B1).
eliminate_equiv_xor_imp(exists X sep A, exists X sep A1) :- !,
	eliminate_equiv_xor_imp(A, A1).
eliminate_equiv_xor_imp(forall X sep A, forall X sep A1) :- !,
	eliminate_equiv_xor_imp(A, A1).
eliminate_equiv_xor_imp(A, A).

%
%  de_morgan(+A, -B)
%    A is a formula built from atoms using negation,
%    disjunction and conjunction only;
%    B is logically equivalent to A and in negation normal form
%    (negations are pushed inwards and double negations are reduced,
%    so that negations are only applied to atoms)
%
de_morgan(neg neg A, A1) :- !,
	de_morgan(A, A1).
de_morgan(neg (A or B), A1 and B1) :- !,
	de_morgan(neg A, A1),
	de_morgan(neg B, B1).
de_morgan(neg (A and B), A1 or B1) :- !,
	de_morgan(neg A, A1),
	de_morgan(neg B, B1).
de_morgan(A or B, A1 or B1) :- !,
	de_morgan(A, A1),
	de_morgan(B, B1).
de_morgan(A and B, A1 and B1) :- !,
	de_morgan(A, A1),
	de_morgan(B, B1).
de_morgan(A, A).

%
%  distribute_or_over_and(+A, -B)
%    A is a formula in negation normal form;
%    B is logically equivalent to A,
%    with disjunction distributed over conjunction
%
distribute_or_over_and(A and B, A1 and B1) :- !, 
	distribute_or_over_and(A, A1),
	distribute_or_over_and(B, B1).
distribute_or_over_and(A or B and C, ABC) :- !, 
	distribute_or_over_and(A or B, AB),
	distribute_or_over_and(A or C, AC),
	distribute_or_over_and(AB and AC, ABC).
distribute_or_over_and(A and B or C, ABC) :- !,
	distribute_or_over_and(A or C, AC),
	distribute_or_over_and(B or C, BC),
	distribute_or_over_and(AC and BC, ABC).
distribute_or_over_and(A or B, C) :- !,
	(   contains_and(A or B), !,
	    distribute_or_over_and(A, A1),
	    distribute_or_over_and(B, B1),
	    distribute_or_over_and(A1 or B1, C)
	;   C = A or B
	).
distribute_or_over_and(A, A).

%
%  contains_and(+A)
%
contains_and(_ and _).
contains_and(A or B) :-
	(   contains_and(A)
	;   contains_and(B)
	).

%
%  distribute_and_over_or(+A, -B)
%    A is a formula in negation normal form;
%    B is logically equivalent to A,
%    with conjunction distributed over disjunction
%
distribute_and_over_or(A or B, A1 or B1) :- !, 
	distribute_and_over_or(A, A1),
	distribute_and_over_or(B, B1).
distribute_and_over_or(A and (B or C), ABC) :- !, 
	distribute_and_over_or(A and B, AB),
	distribute_and_over_or(A and C, AC),
	distribute_and_over_or(AB and AC, ABC).
distribute_and_over_or((A or B) and C, ABC) :- !,
	distribute_and_over_or(A and C, AC),
	distribute_and_over_or(B and C, BC),
	distribute_and_over_or(AC or BC, ABC).
distribute_and_over_or(A and B, C) :- !,
	(   contains_or(A and B), !,
	    distribute_and_over_or(A, A1),
	    distribute_and_over_or(B, B1),
	    distribute_and_over_or(A1 and B1, C)
	;   C = A and B
	).
distribute_and_over_or(A, A).

%
%  contains_or(+A)
%
contains_or(_ or _).
contains_or(A and B) :-
	(   contains_or(A)
	;   contains_or(B)
	).

%
%  instance(+Variable, +Term, +Expression, -Instance)
%    Instance is an instance of Expression obtained by substituting
%    Term for the free occurrences of Variable in Expression;
%    Variable can be denoted either by a lower case letter of by a term
%    of the form '$VAR'(i)
%
instance(Variable, Term, Variable, Term) :- !.
instance(X, _, exists X sep Form, exists X sep Form) :- !.
instance(X, Term, exists Y sep Form, exists Y sep Form1) :- !,
	instance(X, Term, Form, Form1).
instance(X, _, forall X sep Form, forall X sep Form) :- !.
instance(X, Term, forall Y sep Form, forall Y sep Form1) :- !,
	instance(X, Term, Form, Form1).
instance(X, Term, Expression, Instance) :-
	compound(Expression),
	Expression \= '$VAR'(_), !,
	Expression =..  [Oper| Args],
	maplist(instance(X, Term), Args, Args1),
	Instance =.. [Oper| Args1].
instance(_, _, Atom, Atom).

%
%  instances(+Variable, +Terms, +Formula, -Instances)
%    Instances is the list of instances of Formula
%    obtained by substituting a member of Terms
%    for the free occurrences of Variable in Formula
%
instances(X, [Term| Terms], Form, [Inst| Insts]) :-
	instance(X, Term, Form, Inst),
	instances(X, Terms, Form, Insts).
instances(_, [], _, []).

%
%  rename_variables(+Formula, -RenamedFormula)
%    RenamedFormula is Formula with bound variables renamed so that
%    distinct quantifers operate on distinct variables;
%    Formula should not contain any term of the form xi for some
%    nonnull natural number i, and all bound variables in RenamedFormula
%    will be of the form xi 
%
rename_variables(Formula, RenamedFormula) :-
	reset_gensym(x),
	rename_variables1(Formula, RenamedFormula).

%
%  rename_variables1(+Formula, -RenamedFormula)
%
rename_variables1(exists X sep FormX, exists V sep Form) :- !,
	gensym(x, V),
	instance(X, V, FormX, FormV),
	rename_variables1(FormV, Form).
rename_variables1(forall X sep FormX, forall V sep Form) :- !,
	gensym(x, V),
	instance(X, V, FormX, FormV),
	rename_variables1(FormV, Form).
rename_variables1(Expression, RenamedExpression) :-
	compound(Expression), !,
	Expression =.. [Oper| Args],
	maplist(rename_variables1, Args, Args1),
	RenamedExpression =.. [Oper| Args1].
rename_variables1(ConstantOrVariable, ConstantOrVariable).

%
%  contains_quantifiers(+Formula)
%
contains_quantifiers(_ sep _) :- !.
contains_quantifiers(neg A) :- !,
	contains_quantifiers(A).
contains_quantifiers(A or B) :- !,
	(   contains_quantifiers(A)
	;   contains_quantifiers(B)
	).
contains_quantifiers(A and B) :- !,
	(   contains_quantifiers(A)
	;   contains_quantifiers(B)
	).
contains_quantifiers(A imp B) :- !,
	(   contains_quantifiers(A)
	;   contains_quantifiers(B)
	).
contains_quantifiers(A eqv B) :- !,
	(   contains_quantifiers(A)
	;   contains_quantifiers(B)
	).
contains_quantifiers(A xor B) :-
	(   contains_quantifiers(A)
	;   contains_quantifiers(B)
	).

%
%  has_no_occurrence_in(+Variable, +Expression)
%    Variable can be denoted either by a lower case letter of by a term
%    of the form '$VAR'(i)
%
has_no_occurrence_in(Variable, Expression) :-
	compound(Expression),
	Expression \= '$VAR'(_), !,
	Expression =..  [_| Args],
	checklist(has_no_occurrence_in(Variable), Args).
has_no_occurrence_in(Variable, Expression) :-
	Variable \= Expression.

%
%  has_no_free_occurrence_in(+Variable, + Expression)
%    Variable can be denoted either by a lower case letter of by a term
%    of the form '$VAR'(i)
%
has_no_free_occurrence_in(X, exists X sep _) :- !.
has_no_free_occurrence_in(X, exists _ sep A) :- !,
	has_no_free_occurrence_in(X, A).
has_no_free_occurrence_in(X, forall X sep _) :- !.
has_no_free_occurrence_in(X, forall _ sep A) :- !,
	has_no_free_occurrence_in(X, A).
has_no_free_occurrence_in(X, Expression) :-
	compound(Expression),
	Expression \= '$VAR'(_), !,
	Expression =..  [_| Args],
	checklist(has_no_free_occurrence_in(X), Args).
has_no_free_occurrence_in(X, ConstantOrVariable) :-
	X \= ConstantOrVariable.