/* ========================================================================== */
/*                 PREDICATES  DEALING WITH CNFs AND DNFs                     */
/* ========================================================================== */


:- module(cnf_dnf,
          [
             cnf_to_dnf/2,
             dnf_to_cnf/2, 
             simplify_DNF/2,
             simplify_CNF/2
          ]
          ).
 
 
:-
   getenv('LEAR_DIR', Lear),
   writeln(Lear),
   atom_concat(Lear, '/list.pl', List),
   use_module(List).
          
/* ======================================================================== */
/*                           CNF to DNF                                     */
/* ======================================================================== */   
   
  
        /* kepp this order of the clauses (it has an important meaning 
           in the recursivity) ! */
cnf_to_dnf([Clause], DNF) :-
   !,
   distribute(Clause, [], DNF1),
   simplify_DNF(DNF1, DNF).
        
cnf_to_dnf(
           [],        % Empty CNF is true (each interpretation is a model of [])
           [[]]       % So the associated DNF contains the empty conjunction
                      % that is always true.
           ) :-   
   !.

cnf_to_dnf([Clause|LClauses], DNF) :-
   cnf_to_dnf(LClauses, DNF1),
   distribute(Clause, DNF1, DNF2),
   simplify_DNF(DNF2, DNF).   
   
   
        /* simplify a Disjunctive Normal Form (DNF) */ 
simplify_DNF(
             DNF,          % DNF to simplify
             DNF_out       % Simplified DNF
            ) :-
   simplify_conjunctions(DNF, DNF1),
   keep_minimal_lists(DNF1, DNF2),
   delete(DNF2, [false], DNF_out).    
    
    
    /* simplify a set of clauses */
simplify_conjunctions([], []) :-
   !.
   
simplify_conjunctions([Conj|LConj], [Conj_out|LConj_out]) :-
   sort(Conj, Conj1),                                   % discard duplicates
   simplify_one_conjunction(Conj1, Conj_out),
   simplify_conjunctions(LConj, LConj_out).
  
  
   /* simplify a grounded conjunction of atoms */
simplify_one_conjunction([], []) :-
   !.
   
simplify_one_conjunction([neg(Atom)|LAtoms], [false]) :-
   member(Atom, LAtoms),
   !.
   
simplify_one_conjunction([Atom|LAtoms], [false]) :-
   member(neg(Atom), LAtoms),
   !.   
   
simplify_one_conjunction(
                    [Atom|LAtoms],     % _Atom has been checked
                    Conj_out            % Simplified conjunction : 
                                        % either Conj or [false]
                   ) :-
   simplify_one_conjunction(LAtoms, Conj),
   check_conjunction(Atom, Conj, Conj_out).
   


check_conjunction(_Atom, [false], [false]) :-
   !.
   
check_conjunction(Atom, Conj, [Atom|Conj]).   
   
/* ======================================================================== */
/*                           DNF to CNF                                     */
/* ======================================================================== */   

        /* kepp this order of the clauses (it has an important meaning 
           in the recursivity) ! */
dnf_to_cnf([Conj], CNF) :-
   !,
   distribute(Conj, [], CNF1),
   simplify_CNF(CNF1, CNF).
        
dnf_to_cnf(
           [],    % Empty DNF is false (it has no model)
           [[]]   % So the associated CNF contains the empty clause
                  % that is false (has no model) 
           ) :-   
   !.

dnf_to_cnf([Conj|LConj], CNF) :-
   dnf_to_cnf(LConj, CNF1),
   distribute(Conj, CNF1, CNF2),
   simplify_CNF(CNF2, CNF).
   
  
        /* simplify a Conjunctive Normal Form */ 
simplify_CNF(
             CNF,                  % Conjonctive Normal Form to simplify
             CNF_out       % Simplified Conjonctive Normal Form
            ) :-
   simplify_clauses(CNF, CNF1),
   keep_minimal_lists(CNF1, CNF2),
   delete(CNF2, [true], CNF_out).
   
   
   /* simplify a set of clauses */
simplify_clauses([], []) :-
   !.
   
simplify_clauses([Clause|LClauses], [Clause_out|LClauses_out]) :-
   sort(Clause, Clause1),                                  % discard duplicates
   simplify_one_clause(Clause1, Clause_out),
   simplify_clauses(LClauses, LClauses_out).
  
  
   /* simplify a grounded clause (disjunction of atoms) */
simplify_one_clause([], []) :-
   !.
   
simplify_one_clause([neg(Atom)|LAtoms], [true]) :-
   member(Atom, LAtoms),
   !.
   
simplify_one_clause([Atom|LAtoms], [true]) :-
   member(neg(Atom), LAtoms),
   !.   
   
   
simplify_one_clause(
                    [Atom|LAtoms],     % _Atom has been checked
                    Clause_out          % simplified clause : 
                                        % either Clause or [true]
                   ) :-
   simplify_one_clause(LAtoms, Clause),
   check_clause(Atom, Clause, Clause_out).
   
check_clause(_Atom, [true], [true]) :-
   !.
   
check_clause(Atom, Clause, [Atom|Clause]).   
   
   
   
/* ======================================================================== */
/*                           OPERATIONS ON LITERALS                         */
/* ======================================================================== */    
   
        /* respect the order of the clauses ! */     
distribute([Literal], DNF, DNF_out) :-
   !,
   distribute_literal(Literal, DNF, DNF_out).   
        
distribute([], DNF, DNF) :-
   !.
   
distribute([Literal|LLiteral], DNF, DNF_out) :-
   distribute_literal(Literal, DNF, DNF2),
   distribute(LLiteral, DNF, DNF1),
   append(DNF2, DNF1, DNF_out).
   

        /* respect the order of the clauses ! */
distribute_literal(Literal, [Conjunction], [[Literal|Conjunction]]) :-
   !.
   
distribute_literal(Literal, [], [[Literal]]) :-
   !.
   
distribute_literal(Literal, [Conjunction|DNF], [[Literal|Conjunction]|DNF1]) :-
   distribute_literal(Literal, DNF, DNF1).
   
   
complete_DNF(DNF, DNF_out) :-
   flatten(DNF, DNF1),
   sort(DNF1,  DNF2),
   completing_DNF(DNF, DNF2, DNF_out).
   
   /* complete each Herbrand interpretation by adding negative litterals */
completing_DNF(
             [],         % list of conjunctions
             _HB,        % Herbrand basis
             []          % Completed DNF
            ).  
   
completing_DNF(
             [Conj|LConj],         % list of conjunctions
             HB,                   % Herbrand basis
             [Conj_out|LConj_out]  % Completed DNF
            ) :-      
   complete_one_conjunction(Conj, HB, Conj_out),
   completing_DNF(LConj, HB, LConj_out).
   
   
   /* complete a conjunction by adding negative litterals */
complete_one_conjunction(
                         LAtoms,            % list of atoms
                         HB,                % Herbrand basis
                         LAtoms_out         % final list of atoms
            ) :-  
   subtract(HB, LAtoms, LAtoms1),
   create_negative_litterals(LAtoms1, LAtoms_neg),
   append(LAtoms, LAtoms_neg, LAtoms_out).
   
        % create negative litterals from a set of atoms
create_negative_litterals([], []) :-
   !.
   
create_negative_litterals([Atom|LAtoms], [neg(Atom)|LAtoms_neg]) :-
   create_negative_litterals(LAtoms, LAtoms_neg).
                      
