%
%  Transform a formula to CNF
%

:- module(cnf,
    [cnf/2, cnf_to_clausal/2,
     demorgan/2,
     subst_var/3, member_term/2]).

user:file_search_path(common,'../common').
:- ensure_loaded(common(ops)).
:- ensure_loaded(common(def)).

%
%  cnf(A, B)
%    B is A in conjunctive normal form.
%
cnf(A, A5) :-
  rename(A, A1),           % Needed only for predicate formulas
  eliminate(A1, A2), 
  demorgan(A2, A3),
  extract(A3, A4),         % Needed only for predicate formulas
  distribute(A4, A5).

%
%  rename(A, B)
%  rename(A, List, Num, B)
%    B is A with bound variables renamed.
%    List is a list of pairs (X, Y),
%      where the Xs are all the variables,
%      and Y is X for the first occurrence of X
%      or a new variable for subsequent occurrences.
%    List1 is List appended with new substitutions created.
%
rename(A, B) :- rename(A, [], _, B).

rename(all(X, A), List, List1, all(Y, A1)) :-
  member_var((X, _), List), !,       % The variable was already encountered.
  copy_term(X, Y),                   % Create a new variable.
  rename(A, [(X, Y) | List], List1, A1).

rename(all(X, A), List, List1, all(X, A1)) :- !,
  rename(A, [(X, X) | List], List1, A1).
                                     % First occurrence "replaced" by itself.
rename(ex(X, A), List, List1, ex(Y, A1)) :-
  member_var((X, _), List), !,
  copy_term(X, Y),
  rename(A, [(X, Y) | List], List1, A1).
rename(ex(X, A), List, List1, ex(X, A1)) :- !, 
  rename(A, [(X, X) | List], List1, A1).
                                     % Similarly for ex quantifier.
rename(A, List, List2, B) :-
  A =.. [Opr, A1, A2],
  symbol_opr(_, Opr), !,
  rename(A1, List, List1, B1),
  rename(A2, List1, List2, B2),
  B =.. [Opr, B1, B2].

rename(neg A, List, List1, neg B) :- !,
  rename(A, List, List1, B).
rename(A, List, List, B) :-
  A =.. [F | Vars],
  subst_var(Vars, Vars1, List),
  B =.. [F | Vars1].

%
%  member_var((X,Y), List)
%    Finds the first pair (X,Y) in List.
%    Called with X bound to a variable and Y not bound.
%
member_var((A,Y), [(B,Y) | _]) :- A == B, !.
member_var(A, [_ | C]) :- member_var(A, C).

%
%  subst_var(V1List, V2List, List)
%    V1List is a list of variables, and List is a list of variable pairs.
%    For X in V1List, the corresponding element in V2List is Y,
%      if (X,Y) is in List, otherwise, it is X.
%  (The third clause is used in skolem, not in cnf.)
%
subst_var([], [], _).
subst_var([V | Tail], [V1 | Tail1], List) :-
  member_var((V, V1), List), !,
  subst_var(Tail, Tail1, List).
subst_var([V | Tail], [V | Tail1], List) :-
  subst_var(Tail, Tail1, List).

%
%  extract(A, B)
%    B is A with quantifiers extracted to prefix.
%
extract(all(X, A) or B,  all(X, C)) :- !, extract(A or B,  C).
extract(ex(X,  A) or B,  ex(X,  C)) :- !, extract(A or B,  C).
extract(all(X, A) and B, all(X, C)) :- !, extract(A and B, C).
extract(ex(X,  A) and B, ex(X,  C)) :- !, extract(A and B, C).

extract(A or  all(X, B), all(X, C)) :- !, extract(A or B,  C).
extract(A or  ex(X,  B), ex(X,  C)) :- !, extract(A or B,  C).
extract(A and all(X, B), all(X, C)) :- !, extract(A and B, C).
extract(A and ex(X,  B), ex(X,  C)) :- !, extract(A and B, C).

extract(A or B, C) :- !,
  extract(A, A1),
  extract(B, B1),
  (is_quantified(A1, B1) -> extract(A1 or B1, C) ; (C = A or B) ).

extract(A and B, C) :- !,
  extract(A, A1),
  extract(B, B1),
  (is_quantified(A1, B1) -> extract(A1 and B1, C) ; (C = A and B) ).

extract(A, A).

is_quantified(ex(_,_),  _).
is_quantified(all(_,_), _).
is_quantified(_, ex(_,_)).
is_quantified(_, all(_,_)).

%
%  eliminate(A, B)
%    B is A without eqv, xor and imp.
%
eliminate(A eqv B,
          (A1 and B1) or ((neg A1) and (neg B1)) ) :- !,
  eliminate(A, A1),
  eliminate(B, B1).
eliminate(A xor B,
          (A1 and (neg B1)) or ((neg A1) and B1) ) :- !,
  eliminate(A, A1),
  eliminate(B, B1).
eliminate(A imp B,
          (neg A1) or B1 )     :- !,
  eliminate(A, A1),
  eliminate(B, B1).
eliminate(A or B,  A1 or B1)   :- !,
  eliminate(A, A1),
  eliminate(B, B1).
eliminate(A and B,  A1 and B1) :- !,
  eliminate(A, A1),
  eliminate(B, B1).
eliminate(neg A, neg A1)       :- !,
  eliminate(A, A1).
eliminate(all(X,A), all(X,A1)) :- !,
  eliminate(A, A1).
eliminate(ex(X,A), ex(X,A1))   :- !,
  eliminate(A, A1).
eliminate(A, A).

%
%  demorgan(A, B)
%    B is A with negations pushed inwards and
%    reducing double negations.
%
demorgan(neg (A and B), A1 or B1) :- !,
  demorgan(neg A, A1),
  demorgan(neg B, B1).
demorgan(neg (A or B), A1 and B1) :- !,
  demorgan(neg A, A1),
  demorgan(neg B, B1).
demorgan((neg (neg A)),  A1)      :- !,
  demorgan(A, A1).
demorgan(neg all(X,A), ex(X,A1))  :- !,
  demorgan(neg A, A1).
demorgan(neg ex(X,A), all(X,A1))  :- !,
  demorgan(neg A, A1).

demorgan(neg always A, eventually A1)  :- !,
  demorgan(neg A, A1).
demorgan(neg eventually A, always A1)  :- !,
  demorgan(neg A, A1).


demorgan(all(X,A), all(X,A1))     :- !,
  demorgan(A, A1).
demorgan(ex(X,A),   ex(X,A1))     :- !,
  demorgan(A, A1).
demorgan(A and B,    A1 and B1)   :- !,
  demorgan(A, A1),
  demorgan(B, B1).
demorgan(A or B,    A1 or B1)     :- !,
  demorgan(A, A1),
  demorgan(B, B1).
demorgan(A, A).

%
%  distribute(A, B)
%    B is A with disjuntion distributed over conjunction
%
distribute(all(X,A), all(X,A1)) :- !, distribute(A, A1).
distribute(ex(X,A),  ex(X,A1))  :- !, distribute(A, A1).
distribute(A or (B and C), ABC) :- !, 
  distribute(A or B, AB),
  distribute(A or C, AC),
  distribute(AB and AC, ABC).
distribute((A and B) or C, ABC) :- !,
  distribute(A or C, AC),
  distribute(B or C, BC),
  distribute(AC and BC, ABC).
distribute(A or B, A1 or B1) :- !, 
  distribute(A, A1),
  distribute(B, B1).
distribute(A and B, A1 and B1) :- !, 
  distribute(A, A1),
  distribute(B, B1).
distribute(A, A).

%
%  cnf_to_clausal(A, B)
%    A is a CNF formula, B is the formula in clausal notation.
%
cnf_to_clausal(D1 and D2, S) :- !,
  cnf_to_clausal(D1, S1),
  cnf_to_clausal(D2, S2),
  append(S1, S2, S).
cnf_to_clausal(D, S) :-
  disjunction_to_set(D, S).

%
%  disjunction_to_set(D, S) -
%    D is a disjunction of literals and S is the disjunction as a set.
%    A disjunction containing clashing (identical)
%      literals is valid and may be discarded.
%
disjunction_to_set(D, []) :-
  disjunction_to_set1(D, List),
  member(L1, List),
  member(neg L2, List),
  L1 == L2, !.           % Identical, not unifiable.
disjunction_to_set(D, [S]) :-
  disjunction_to_set1(D, List),
  remove_dups(List, S).

%
%  disjunction_to_set1(D, S) -
%    The disjunction D is transformed into a list.
%
disjunction_to_set1(L1 or L2, S) :- !,
  disjunction_to_set1(L1, S1),
  disjunction_to_set1(L2, S2),
  append(S1, S2, S).
disjunction_to_set1(L, [L]).

%
%  remove_dups(List, Set) -
%    Make List a Set by removing duplicates, but DO NOT unify.
%
remove_dups([Head|Tail], NewTail) :-
  remove_dups(Tail, NewTail),
  member_term(Head, NewTail), !.
remove_dups([Head|Tail], [Head | NewTail]) :- !,
  remove_dups(Tail, NewTail).
remove_dups([], []).

%
%  member_term(T, List) - Like member, but do not unify.
%
member_term(L, [Head|_]) :-
  L == Head, !.
member_term(L, [_|Tail]) :- !,
  member_term(L, Tail).