/* ========================================================================== */
/*                              LEAR UTILITIES                                */
/*    Author  : Dominique Bouthinon (LIPN, Universite Paris13)                */
/*    History :                                                               */
/*   - an inconsistant extensional example is automatically discarded         */
/*     (there is no more check of a global consistance of the BK              */
/*     (5/06/13)                                                              */
/*   - add the possibility to number the negative examples by starting        */
/*     by numbers 1 (this option is to deal with old files)                   */
/*     (12/04/2013)                                                           */
/*            - every example is now represented by its sets of maximal and   */
/*			       minimal possibilities			                       */
/*              (8/02/2013)                                                   */
/*            - ajout vraies tete de clause                                   */
/*              (13/07/12)                                                    */
/*            - suppression de la notion de saturation (<=) dans build        */
/*              extensional examples +  suppressions irrelevant et non        */
/*              abducibles.                                                   */
/*              (14/10/11)                                                    */
/*            - ajouts atoms non pertinents (irrelevant)                      */
/*            - modifications of build extensional (improvments)              */
/*            - clausal format of examples  (16/01/10)                        */
/*            - each example has its own Herbrand base  (26-12-09)            */
/*            - read intentional examples and build extensional ones          */
/*              (22-12-09)                                                    */
/*            - split ambiguous examples into tables according to             */
/*              the arguments they contains (27-11-09).                       */
/*            - negation (neg) in background knowledge (8/06/2010)            */
/*            - general clauses : a(X) or b(Y) <- c(X) and d(Y)               */
/*            - add the possibility "X \= Y" in clauses (2/07/10)             */
/*            - neg(X) means X is false (but theoretically could be true      */
/*              while "<- X" means X is always false                          */
/*                                                                            */
/* ========================================================================== */

:- module(utilities_lear11,
           [
			build_all_models/5,
							% (LDomains, LClauses_bkg, LModes,
                 				%  LIrrelevant, LTables)
			build_all_tables/4,
						 	% (LParts, LClauses, LClauses_neg, LTables)

									% facts handling
			compute_known_unknown_facts/5,
			delete_non_facts/2,
			get_positive_facts/2,
			get_negative_facts/2,

			                     % learning examples handling
               build_extensional_examples/3,
			build_extensional_ex/7,
			compute_grounded_theory/9,

			discard_intentional_knowledge/0,
			discard_clauses_intentional2/1,
			simplify_clauses/2,
			instantiate_clauses/3,
			inserer_dans_base/1,
			delete_similar_elements/4,
			build_Herbrand_base/4,
			discard_similar_elements/3,
			lear_clauses_to_prolog/2,

	          numbers_negative_intentional_examples/3,
               write_examples/2,
               write_tabs/2,
               translate_clauses/2,

	          clausal_to_conjunctive/2,
	          conjunctive_to_clausal/2,
               simplify_tables/2,
               write_excel_results/5,
               write_results/17,
               get_learn_mode/1,
               set_learn_mode/1,
               retract_learn_mode/0,
               make_split_literals/2,
               split_literals/2,
                                                % display
            display_example/1,
            display_example_num/1,
            display_conjunction_quality/11,
            display_best_conjunction2/3,
            display_best_conjunction/1,
            display_best_conjunctions/3,
            display_conjunction/2,
            display_conjunction/6,
            fdisplay_rules/2,
            display_rules/1,
            display_fold/1,
            display_hyp/2,
            display_infos/3,
            display_results_file2/28,
            display_results_file/32,
            first_message/0
           ]).


:- dynamic intentional2:falsity/0.

        /* needed operators */

:- op(900, xfy, <=).           % saturation
:- op(900, xfy, <-).
:- op(900, fx, <-).
:- op(850, xfy, or).
:- op(850, xfy, and).


        /* needed modules */
:-
   getenv('LEAR_DIR', Lear),

   atom_concat(Lear, '/shell_commands.pl', Shell),
   use_module(Shell),

   atom_concat(Lear, '/list.pl', List),
   use_module(List),

   atom_concat(Lear, '/formated_writing.pl', Writing),
   use_module(Writing),

   atom_concat(Lear, '/cnf_dnf.pl', Cnf),
   use_module(Cnf),

   atom_concat(Lear, '/string.pl', String),
   use_module(String),

   atom_concat(Lear, '/term.pl', Term),
   use_module(Term),

   atom_concat(Lear, '/domains.pl', Domains),
   use_module(Domains),

   atom_concat(Lear, '/file.pl', File),
   use_module(File),

   atom_concat(Lear, '/clauses.pl', Clauses),
   use_module(Clauses),

   atom_concat(Lear, '/counter.pl', Counter),
   use_module(Counter),

   atom_concat(Lear, '/graph_examples2.pl', Graph),
   use_module(Graph),

   atom_concat(Lear, '/completion2.pl', Completion),
   use_module(Completion),

   atom_concat(Lear, '/miscellaneous.pl', Misc),
   use_module(Misc),

   atom_concat(Lear, '/intentional_data.pl', Int_data),
   use_module(Int_data).


        /* dynamic predicates */
:- dynamic intentional:background_knowledge/1.
:- dynamic intentional:herbrand_base/1.
:- dynamic intentional:positive_examples/1.
:- dynamic intentional:negative_examples/1.
:- dynamic intentional:mode/1.
:- dynamic intentional:types_under_oi/1.
:- dynamic intentional:types_instantiable/1.
:- dynamic intentional:abducible_predicates/1.


/* =================== build the maximal valid intepretations =============== */

maximal_valid_interpretations(
      LA,     % list of remaining attributes
      [LA]    % list of maximal valid interpretations
                              ) :-
     valid_interpretation(LA),   % LA containing uncertain attributes is maximal
                                % and satisfies all constraints
        !.

        /* there is no uncertain attribute so max interpreation is empty.
          no possibility to shrink it */
maximal_valid_interpretations([], []) :-
        !.

        /* current interpretation satisfies false constraints and
                can be extended by adding attributes */
maximal_valid_interpretations(
                               LA,      % available attributes
                               LMax     % maximal valid interpretations
                             ):-
        check_possible_and_maxima([], [LA], [], LMax).


check_possible_and_maxima(_Max_found, [], LMax, LMax) :-
        !.      % there is no more possible interpretations.

check_possible_and_maxima(_Max_found, [[]], LMax, LMax) :-
        !.      % one cannot reduce empty interpretation []

check_possible_and_maxima(Max_found, LPossible_N, LMax_N, LMax) :-
        build_maximal_interpretations(Max_found, LPossible_N, LMax_N1),
        append(LMax_N1, LMax_N, LMax).


build_maximal_interpretations(_Max_found, [], _LMax) :-
        !.

build_maximal_interpretations(
                               Max_found,
                               LPos_N  ,      % possible int. of length N
                               LMax           % maximal  int. of length N
                             ) :-

        dissociate_interpretations(LPos_N, LPos_N1A),
        discard_non_maximal_interpretations(LPos_N1A, Max_found, LPos_N1B),
        keep_possible_maxima(LPos_N1B, LPos_N1, LMax_N1),
        append(Max_found, LMax_N1, Max_found1),
        check_possible_and_maxima(Max_found1, LPos_N1, LMax_N1, LMax).


discard_non_maximal_interpretations([], _LMax, []) :-
        !.

discard_non_maximal_interpretations([IP|LIP], LMax, LPos) :-
        has_superset(IP, LMax),
        !,
        discard_non_maximal_interpretations(LIP, LMax, LPos).

discard_non_maximal_interpretations([IP|LIP], LMax, [IP|LPos]) :-
        discard_non_maximal_interpretations(LIP, LMax, LPos).


has_superset(L, [L1|_]) :-
        my_subset(L, L1),
        !.

has_superset(L, [_L1|LL]) :-
        has_superset(L, LL).

     /* built interpretations of lenght N-1 from interpretations of length N */
dissociate_interpretations([], []) :-
        !.

dissociate_interpretations([I|LI], LPos) :-
        dissociate_one_interpretation(I, LPos1),
        dissociate_interpretations(LI, LPos2),
        append(LPos1, LPos2, LPos3),
        sort(LPos3, LPos).


dissociate_one_interpretation(I, LI) :-
                findall(I1, select(_X, I, I1), LI).


keep_possible_maxima([], [], []) :-
        !.

keep_possible_maxima([I|LI], LPos, LMax) :-
        check_maximal_interpretation(I, Code),
        keep_possible_maxima(LI, LPos1, LMax1),
        place_maximal_interpretation(Code, I, LPos1, LMax1, LPos, LMax).


place_maximal_interpretation(ok_base, I, LPos, LMax, LPos, [I|LMax]) :-
        !.

place_maximal_interpretation(ok_or, I, LPos, LMax, [I|LPos], LMax) :-
        !.

place_maximal_interpretation(_, _, LPos, LMax, LPos, LMax).


/* ==================  build the minimal valid interpretations ============== */

minimal_valid_interpretations(
                   _LA,          % list of remaining attributes
                   [[]]          % list of minimal valid interpretations
                             ) :-
                   base_ok,      % empty interpretation is valid
        !.

        /* no available attribute : empty interpretation cannot be extended */
minimal_valid_interpretations([], []) :-
        !.

        /* empty interpretation satisfies false constraints and
                can be extended by adding attributes */
minimal_valid_interpretations(
        LA,     % available attributes
        LMin    % minimal valid interpretations
                              ):-
        minimal_interpretations_of_length1(LA, LPossible1, LMin1),
        check_possible_and_minima([], 1, LPossible1, LMin1, LMin).


check_possible_and_minima(_Min_found, _, [], LMin, LMin) :-
        !.

check_possible_and_minima(Min_found, N, LPossible_N1, LMin_N1, LMin) :-
        N1 is N+1,
        build_minimal_interpretations(Min_found, N1, LPossible_N1, LMin_N),
        append(LMin_N, LMin_N1, LMin).


build_minimal_interpretations(_, _, [], _LMin) :-
        !.

build_minimal_interpretations(
                                Min_found,
                                N,         % current length of interpretations
                                LP_N1,     % possible int. of length N-1
                                LMin       % minimal int. of length N
                             ) :-
        merge_all_interpretations(N, LP_N1, LP_NA),
        discard_non_minimal_interpretations(LP_NA, Min_found, LP_NB),
        keep_possible_minima(LP_NB, LP_N, LMin_N),
        append(Min_found, LMin_N, Min_found1),
        check_possible_and_minima(Min_found1, N, LP_N, LMin_N, LMin).


minimal_interpretations_of_length1([], [], []) :-
        !.

minimal_interpretations_of_length1([A|LA], LPossible, [[A]|LMinimal]) :-
        valid_interpretation([A]),
        !,
        minimal_interpretations_of_length1(LA, LPossible, LMinimal).

minimal_interpretations_of_length1([A|LA], [[A]|LPossible], LMinimal) :-
        interpretation_ok_for_false([A]),
        !,
        minimal_interpretations_of_length1(LA, LPossible, LMinimal).

minimal_interpretations_of_length1([_A|LA], LPossible, LMinimal) :-
        minimal_interpretations_of_length1(LA, LPossible, LMinimal).


discard_non_minimal_interpretations([], _LMin, []) :-
        !.

discard_non_minimal_interpretations([IP|LIP], LMin, LPos) :-
        has_subset(IP, LMin),
        !,
        discard_non_minimal_interpretations(LIP, LMin, LPos).

discard_non_minimal_interpretations([IP|LIP], LMin, [IP|LPos]) :-
        discard_non_minimal_interpretations(LIP, LMin, LPos).


has_subset(L, [L1|_]) :-
        my_subset(L1, L),
        !.

has_subset(L, [_L1|LL]) :-
        has_subset(L, LL).


merge_all_interpretations(_N, [], []) :-
        !.

merge_all_interpretations(N, [I|LI], LLI) :-
        merge_interpretations(N, I, LI, LLI1),
        merge_all_interpretations(N, LI, LLI2),
        append(LLI1, LLI2, LLI3),
        sort(LLI3, LLI).


merge_interpretations(_N, _I, [], []) :-
        !.

merge_interpretations(N, I, [I1|LI], [IMerged|LIMerged]) :-
        merge_two_interpretations(N, I, I1, IMerged),
        !,
        merge_interpretations(N, I, LI, LIMerged).


merge_interpretations(N, I, [_I1|LI], LIMerged) :-
        merge_interpretations(N, I, LI, LIMerged).


merge_two_interpretations(N, I1, I2, IMerged) :-
        append(I1, I2, I3),
        sort(I3, IMerged),
        length(IMerged, N).


keep_possible_minima([], [], []) :-
        !.

keep_possible_minima([I|LI], LPos, LMin) :-
        check_minimal_interpretation(I, Code),
        keep_possible_minima(LI, LPos1, LMin1),
        place_minimal_interpretation(Code, I, LPos1, LMin1, LPos, LMin).


place_minimal_interpretation(ok_base, I, LPos, LMin, LPos, [I|LMin]) :-
        !.

place_minimal_interpretation(ok_false, I, LPos, LMin, [I|LPos], LMin) :-
        !.

place_minimal_interpretation(_, _, LPos, LMin, LPos, LMin).


/* ========================================================================== */
/*                                 DISPLAY                                    */
/* ========================================================================== */

display_best_conjunction(((_,Best, Seed), G, Q, E, PC)):-
        nl,
        display_hyp(Best, Seed),
        print('covered pos ex  : '),
        println(PC),
        print('quality         : '),
        println(Q),
        print('errors          : '),
        println(E),
        print('guidance        : '),
        format('~2f',[G]),
        nl.


display_best_conjunction2(((_Id, Hyp, Seed),
                           Guidance, Quality, Errors, Comp_pos, Cov_pos),
                            Nb_pos, Nb_neg ):-
        nl,
        display_hyp(Hyp, Seed),
        learn:verbosity(Verbose),
       (
        Verbose >= 3
        ->
           write('# compatible+ ex    : '),
           write(Comp_pos),
           write('/'),
           write(Nb_pos),
           write('   ('),
           Percent_pos is  (100.0 * Comp_pos) / Nb_pos,
           format('~2f', [Percent_pos]),
           writeln(' %)'),


           write('# covered+ examples : '),
           write(Cov_pos),
	   write('/'),
           write(Nb_pos),
           write('   ('),
           Percent_cov is  (100.0 * Cov_pos) / Nb_pos,
           format('~2f', [Percent_cov]),
           writeln(' %)'),


           write('# compatible- ex    : '),
           Comp_neg is Nb_neg - Errors,
           write(Comp_neg),
           write('/'),
           write(Nb_neg),
           write('   ('),
           Percent_neg is  (100.0 * Comp_neg) / Nb_neg,
           format('~2f', [Percent_neg]),
           writeln(' %)'),

           write('# errors (on ex-)   : '),
           write(Errors),
           write('/'),
           write(Nb_neg),
           Percent_error is  (100.0 * Errors) / Nb_neg,
           write('   ('),
           format('~2f', [Percent_error]),
           writeln(' %)')
         ;
           true
        ),

       (
         Verbose >= 2
           ->
           display_term('Guidance            : '),
           format('~2f', [Guidance]),
           nl,
           display_term('Quality             : '),
           display_ln(Quality)
           ;
           true
        ).


display_best_conjunctions([], _Npos, _Nneg) :-
   !.

display_best_conjunctions([Conj|LConj], Npos, Nneg) :-
   display_best_conjunction2(Conj, Npos, Nneg),
   display_best_conjunctions(LConj, Npos, Nneg).


fdisplay_rules(Rules, Stream) :-
   current_output(Output),
   set_output(Stream),
   display_rules(Rules),
   set_output(Output).


display_rules([]) :-
        !.


display_rules([rule(Conj, Npos, Nneg)|LRules]) :-
        display_best_conjunction2(Conj, Npos, Nneg),
        display_rules(LRules).


display_conjunction(Hyp, Seed) :-
        display_hyp(Hyp, Seed).

display_conjunction(Hyp, Seed, NR, PC, Guidage, Qualite) :-
        display_hyp(Hyp, Seed),
        display_term('rejected neg ex : '),
        display_ln(NR),
        display_term('covered pos ex  : '),
        display_ln(PC),
        display_term('Guidance        : '),
        format('~2f', [Guidage]),
        nl,
        display_term('Quality         : '),
        display_ln(Qualite),
        nl.


display_conjunction_quality(
                            Hyp, Seed, Nb_pos, Nb_neg,
                            Nb_comp_pos, Nb_comp_neg,
                            Guidance_pos, Guidance_neg,
                            Guidance, Quality, Errors

                           ) :-
        display_hyp(Hyp, Seed),
        write('# compatible+ ex   : '),
        write(Nb_comp_pos),
        write('/'),
        write(Nb_pos),
        write('   ('),
        format('~2f', [Guidance_pos]),
        writeln(' %)'),

        write('# compatible- ex   : '),
        write(Nb_comp_neg),
        write('/'),
        write(Nb_neg),
        write('   ('),
        format('~2f', [Guidance_neg]),
        writeln(' %)'),

        write('# errors (on ex-)  : '),
        write(Errors),
        write('/'),
        write(Nb_neg),
        Percent_error is  (100.0 * Errors) / Nb_neg,
        write('   ('),
        format('~2f', [Percent_error]),
        writeln(' %)'),


        display_term('Guidance           : '),
        format('~2f', [Guidance]),
        nl,
        display_term('Quality            : '),
        display_ln(Quality).


	/* display one example with its number */
display_example_num(Ex) :-
   copy_term(Ex, Ex1),
   my_numbervars(Ex1),
   Ex1 = (Num, Head, Body),
   write('example number '),
   write(Num),
   writeln(' :'),
   write(Head),
   writeln(' :- '),
   display_tables(Body),
   writeln('.').


display_example(Ex) :-
   copy_term(Ex, Ex1),
   my_numbervars(Ex1),
   Ex1 = (Head, Body),
   write(Head),
   writeln(' :- '),
   display_tables(Body),
   writeln('.').

display_tables([]) :-
   !.

display_tables([T]) :-
   write('   '),
   write(T),
   !.

display_tables([T|L]) :-
    write('   '),
    write(T),
    writeln(' x '),
    display_tables(L).


        /* display a hypothesis */
display_hyp(Hyp,Seed) :-
   display_hypothesis(Hyp),
   learn:verbosity(Verbose),
        (
          Verbose >= 4
             ->
           (
               write('seed            : '),
               display_ln(Seed)
           ) ;
           true
         ).


display_hypothesis([Hyp,_Hypa]) :-
   display_clause(Hyp).


check_and(and) :-
   !,
   write(', ').

check_and(_).


display_fold(Fold_number) :-
        nl,
        write(' ========================= FOLD '),
        write(Fold_number),
        writeln(' ==========================='),
        nl.

display_infos(Duration, Precision, Standard_deviation) :-
   nl,
   writeln('Duration;Precision;Standard_deviation:'),
   write(Duration),
   write(';'),
   write(Precision),
   write(';'),
   writeln(Standard_deviation),
   nl.



	/* add results of one "learn and test" on a file for excel format */
write_excel_results(
             '',
               _N_true_pos, _N_false_pos,
               _N_true_neg, _N_false_neg
               ) :-
   !.

write_excel_results(
                    File,
                    N_true_pos, N_false_pos,
                    N_true_neg, N_false_neg
               ) :-

        atom_concat(File, '.csv', File_res),
        open(File_res, append, Stream),

        write(Stream, N_true_pos),
        write(Stream, ';'),

        write(Stream, N_false_neg),
        write(Stream, ';'),

        write(Stream, N_true_neg),
        write(Stream, ';'),

        write(Stream, N_false_pos),
        write(Stream, ';'),

        nl(Stream),
        close(Stream).


	/* write results of one "learn and test" on a file */
write_results(
 			File_train, 			% train file
               File_bkg,			     % background file
               File_test,			% test file
               Duration,			     % duration of learning
			   K,			     % beam widh
               N_pos_train, N_neg_train,
               N_pos_test, Precision_pos,  Recall_pos, Fmeasure_pos,
               N_neg_test, Precision_neg,  Recall_neg, Fmeasure_neg,
               Precision,			% global precision
               Rules               	% found set of rules
               ) :-

        atom_concat(File_train, '.res', File_res),
        open(File_res, write, Stream),

        write(Stream,'Files train                 : '),
        write(Stream, File_train),
        fwriteln(Stream, '.pl'),
        write(Stream,'# positive train examples   : '),
        fwriteln(Stream, N_pos_train),
        write(Stream,'# negative train examples   : '),
        fwriteln(Stream, N_neg_train),

        nl(Stream),

        write(Stream,'File test                   : '),
        write(Stream, File_test),
        fwriteln(Stream, '.pl'),
        write(Stream,'# positive test examples    : '),
        fwriteln(Stream, N_pos_test),
        write(Stream,'# negative test examples    : '),
        fwriteln(Stream, N_neg_test),

        nl(Stream),

        write(Stream,'File bkg                    : '),
        write(Stream, File_bkg),
        fwriteln(Stream, '.bkg'),

        nl(Stream),

	     write(Stream,'width of beam               : '),
        fwriteln(Stream, K),

        write(Stream,'learning duration           : '),
        fdisplay_duration(Stream, Duration),

        nl(Stream),

        write(Stream,'precision (pos)             : '),
        fwriteln(Stream, Precision_pos),

        write(Stream,'accuracy/recall (pos)       : '),
        fwriteln(Stream, Recall_pos),

        write(Stream,'Fmeasure (pos)              : '),
        fwriteln(Stream, Fmeasure_pos),

	     nl(Stream),

        write(Stream,'precision (neg)             : '),
        fwriteln(Stream, Precision_neg),

        write(Stream,'accuracy/recall (neg)       : '),
        fwriteln(Stream, Recall_neg),

        write(Stream,'Fmeasure (neg)              : '),
        fwriteln(Stream, Fmeasure_neg),

        nl(Stream),

        write(Stream,'Accuracy                    : '),
        fwriteln(Stream, Precision),

        nl(Stream),

        write(Stream,'set of rules                : '),
        nl(Stream),

        fdisplay_rules(Rules, Stream),

        close(Stream).


display_results_file2(
                   File_train,
                   File_bkg,
                   File_test,
                   Duration,
                   N, K,
                   LPrecision_pos, LRecall_pos, LFmeasure_pos,
                   LPrecision_neg, LRecall_neg, LFmeasure_neg,
                   LPrecision, LRules,
                   Average_precision_pos, Deviation_precision_pos,
         		    Average_recall_pos, Deviation_recall_pos,
                   Average_fmeasure_pos, Deviation_fmeasure_pos,
                   Average_precision_neg, Deviation_precision_neg,
                   Average_recall_neg, Deviation_recall_neg,
                   Average_fmeasure_neg, Deviation_fmeasure_neg,
                   Average_precision, Deviation_precision
               ) :-

        atom_concat(File_train, '.res', File_res),
        open(File_res, write, Stream),

        nl,
        nl,
        write('writing of the results on file '),
        writeln(File_res),


        write(Stream, '************************  RESULTS ************************'),
        nl(Stream),
        nl(Stream),

        write(Stream,'Files train                 : '),
        write(Stream, File_train),
        fwriteln(Stream, '.pl'),

        write(Stream,'File bkg                    : '),
        write(Stream, File_bkg),
        fwriteln(Stream, '.bkg'),

        write(Stream,'File test                   : '),
        write(Stream, File_test),
        fwriteln(Stream, '.pl'),
        nl(Stream),

        write(Stream,'# folds                     : '),
        fwriteln(Stream, N),

        write(Stream,'width of beam               : '),
        fwriteln(Stream, K),

        write(Stream,'elapsed time                : '),
        fdisplay_duration(Stream, Duration),


        display_folds_results(1,
                   Stream,
                   LPrecision_pos, LRecall_pos, LFmeasure_pos,
                   LPrecision_neg, LRecall_neg, LFmeasure_neg,
                   LPrecision, LRules),
        nl(Stream),
        nl(Stream),
        fwriteln(Stream,'==================================================='),
        format(Stream, 'Average global accuracy  : ~t~2f~35| %~n', Average_precision),
        format(Stream, 'Standard deviation       : ~t~2f~35|', Deviation_precision),
        nl(Stream),
        fwriteln(Stream,'==================================================='),
        nl(Stream),
        fwriteln(Stream, '----- Averages and standards deviation (+) -----'),
        nl(Stream),
        format(Stream, 'Average precision+       : ~t~2f~35| %~n', Average_precision_pos),
        format(Stream, 'Deviation precision+     : ~t~2f~35| ~n', Deviation_precision_pos),
        nl(Stream),
        format(Stream, 'Average accuracy+        : ~t~2f~35| %~n', Average_recall_pos),
        format(Stream, 'Deviation accuracy+      : ~t~2f~35| ~n', Deviation_recall_pos),
        nl(Stream),
        format(Stream, 'Average fmeasure+        : ~t~2f~35| ~n', Average_fmeasure_pos),
        format(Stream, 'Deviation fmeasure+      : ~t~2f~35| ~n', Deviation_fmeasure_pos),

        nl(Stream),
        fwriteln(Stream, '----- Averages and standards deviation (-) -----'),
        nl(Stream),
        format(Stream, 'Average precision-       : ~t~2f~35| %~n', Average_precision_neg),
        format(Stream, 'Deviation precision-     : ~t~2f~35| ~n', Deviation_precision_neg),
        nl(Stream),
        format(Stream, 'Average accuracy-        : ~t~2f~35| %~n', Average_recall_neg),
        format(Stream, 'Deviation accuracty-     : ~t~2f~35| ~n', Deviation_recall_neg),
        nl(Stream),
        format(Stream, 'Average fmeasure-        : ~t~2f~35| ~n', Average_fmeasure_neg),
        format(Stream, 'Deviation fmeasure-      : ~t~2f~35| ~n', Deviation_fmeasure_neg),
        nl(Stream),
        fwriteln(Stream, '*********************************************************************'),

        close(Stream).


display_results_file(
                   File_train,
                   File_bkg,
                   File_test,
                   Duration,
                   N_pos, N_neg, Length_pos, Length_neg, N, K,
                   LPrecision_pos, LRecall_pos, LFmeasure_pos,
                   LPrecision_neg, LRecall_neg, LFmeasure_neg,
                   LPrecision, LRules,
                   Average_precision_pos, Deviation_precision_pos,
         		    Average_recall_pos, Deviation_recall_pos,
                   Average_fmeasure_pos, Deviation_fmeasure_pos,
                   Average_precision_neg, Deviation_precision_neg,
                   Average_recall_neg, Deviation_recall_neg,
                   Average_fmeasure_neg, Deviation_fmeasure_neg,
                   Average_precision, Deviation_precision
               ) :-

        atom_concat(File_train, '.res', File_res),
        open(File_res, write, Stream),

        nl,
        nl,
        write('writing of the results on file '),
        writeln(File_res),


        write(Stream, '************************  RESULTS ************************'),
        nl(Stream),
        nl(Stream),

        write(Stream,'File train                  : '),
        write(Stream, File_train),
        fwriteln(Stream, '.pl'),

        write(Stream,'File bkg                    : '),
        write(Stream, File_bkg),
        fwriteln(Stream, '.bkg'),

        write(Stream,'File test                   : '),
        write(Stream, File_test),
        fwriteln(Stream, '.tst'),
        nl(Stream),


        write(Stream,'# whole positive examples   : '),
        fwriteln(Stream, N_pos),

        write(Stream,'# whole negative examples   : '),
        fwriteln(Stream, N_neg),

        write(Stream,'# folds                     : '),
        fwriteln(Stream, N),

        nl(Stream),

        write(Stream,'# positive examples by fold : '),
        fwriteln(Stream, Length_pos),

        write(Stream,'# negative examples by fold : '),
        fwriteln(Stream, Length_neg),
        nl(Stream),

        write(Stream,'width of beam               : '),
        fwriteln(Stream, K),

        write(Stream,'elapsed time                : '),
        fdisplay_duration(Stream, Duration),


        display_folds_results(1,
                   Stream,
                   LPrecision_pos, LRecall_pos, LFmeasure_pos,
                   LPrecision_neg, LRecall_neg, LFmeasure_neg,
                   LPrecision, LRules),
        nl(Stream),
        nl(Stream),
        fwriteln(Stream,'==================================================='),
        format(Stream, 'Average global accuracy  : ~t~2f~35| %~n', Average_precision),
        format(Stream, 'Standard deviation       : ~t~2f~35|', Deviation_precision),
        nl(Stream),
        fwriteln(Stream,'==================================================='),
        nl(Stream),
        fwriteln(Stream, '----- Averages and standards deviation (+) -----'),
        nl(Stream),
        format(Stream, 'Average precision+       : ~t~2f~35| %~n', Average_precision_pos),
        format(Stream, 'Deviation precision+     : ~t~2f~35| ~n', Deviation_precision_pos),
        nl(Stream),
        format(Stream, 'Average accuracy+        : ~t~2f~35| %~n', Average_recall_pos),
        format(Stream, 'Deviation accuracy+      : ~t~2f~35| ~n', Deviation_recall_pos),
        nl(Stream),
        format(Stream, 'Average fmeasure+        : ~t~2f~35| ~n', Average_fmeasure_pos),
        format(Stream, 'Deviation fmeasure+      : ~t~2f~35| ~n', Deviation_fmeasure_pos),

        nl(Stream),
        fwriteln(Stream, '----- Averages and standards deviation (-) -----'),
        nl(Stream),
        format(Stream, 'Average precision-       : ~t~2f~35| %~n', Average_precision_neg),
        format(Stream, 'Deviation precision-     : ~t~2f~35| ~n', Deviation_precision_neg),
        nl(Stream),
        format(Stream, 'Average accurracy-       : ~t~2f~35| %~n', Average_recall_neg),
        format(Stream, 'Deviation accuracy-      : ~t~2f~35| ~n', Deviation_recall_neg),
        nl(Stream),
        format(Stream, 'Average fmeasure-        : ~t~2f~35| ~n', Average_fmeasure_neg),
        format(Stream, 'Deviation fmeasure-      : ~t~2f~35| ~n', Deviation_fmeasure_neg),
        nl(Stream),
        fwriteln(Stream, '*******************************************************************'),

        close(Stream).


display_folds_results(_, _, [], [], [], [], [], [], [], []) :-
        !.

display_folds_results(N,
                      Stream,
                      [Precision_pos|LPrecision_pos],
                      [Recall_pos|LRecall_pos], [Fmeasure_pos|LFmeasure_pos],
                      [Precision_neg|LPrecision_neg],
                      [Recall_neg|LRecall_neg], [Fmeasure_neg|LFmeasure_neg],
                      [Precision|LPrecision], [Rules|LRules]) :-
        nl(Stream),
        format(Stream, '~`.t ~50|', []),
        nl(Stream),

        format(
                Stream,
                'fold ~t~d~7| : ~t~2f%~16| ~n~@',
                [N, Precision, display_rules(Rules)]
              ),
        nl(Stream),
        format(Stream, 'precision+ : ~1|~t~2f %~10|,   accuracy+ : ~20|~t~2f %~30|,   fmeasure+ : ~40|~t~2f~50|',
                [Precision_pos, Recall_pos, Fmeasure_pos]
              ),
        nl(Stream),
        format(
                Stream,
                'precision- : ~1|~t~2f %~10|,   accuracy- : ~20|~t~2f %~30|,   fmeasure- : ~40|~t~2f~50|',
                [Precision_neg, Recall_neg, Fmeasure_neg]
              ),
        nl(Stream),
        N1 is N+1,
        display_folds_results(N1,
                              Stream,
                              LPrecision_pos, LRecall_pos, LFmeasure_pos,
                              LPrecision_neg, LRecall_neg, LFmeasure_neg,
                              LPrecision, LRules).

first_message :-
        nl,
        nl,
        nl,
        nl,
        println('******************** LEARNING *****************************'),
        println('***********************************************************').



/* ========================================================================== */
/*                              KNOWLEDGE BASE HANDLING                       */
/* ========================================================================== */

introduire_faits([]) :-
        !.

introduire_faits([Fait|L]) :-
        (clause(Fait,true)
                -> true
                ;  intentional2:asserta(Fait)
        ),
        introduire_faits(L).


retirer_faits([]) :-
        !.

retirer_faits([Fait|L]) :-
        (clause(Fait,true)
                -> intentional2:retract(Fait)
                ;  true
        ),
        retirer_faits(L).


inserer_dans_base([]) :-
                !.

inserer_dans_base([Clause|LClause]):-
        intentional2:asserta(Clause),
        inserer_dans_base(LClause).

enlever_de_base([]) :-
                !.

enlever_de_base([Clause|LClause]):-
        intentional2:retract(Clause),
        enlever_de_base(LClause).

inserer_exemple(Exp, Faits_incertains):-
        inserer_dans_base(Exp),
        construire_nouveaux_faits(Nouveaux_faits_vrais, Faits_incertains),
        inserer_dans_base(Nouveaux_faits_vrais),
        intentional2:asserta(nouveaux_faits_vrais(Nouveaux_faits_vrais)).

enlever_exemple(Exp):-
        enlever_de_base(Exp),
        intentional2:retract(nouveaux_faits_vrais(Nouveaux_faits_vrais)),
        enlever_de_base(Nouveaux_faits_vrais).


/* =========================== NUMBERS intentional EXAMPLES ================= */

	/* starts the number of the negative examples at 1 */
numbers_negative_intentional_examples(File_int, File_int_bkg, File_int_out) :-

        % copy the File_int_bkg into a new file with the same name than
        % File_out
   atom_concat(File_int_bkg,'.int_bkg', File_bkg),
   atom_concat(File_int_out, '.int_bkg', File_bkg_out),

   shell_copy_file(File_bkg, File_bkg_out),

   get_data_old(File_int, LPos_int, LNeg_int),

   atom_concat(File_int_out, '.int', File_int_out2),
   open(File_int_out2, write, Stream),

   write(Stream, ':- style_check(-discontiguous).'),
   nl(Stream),
   nl(Stream),

   write_intentional_examples_domains_targets(1, LPos_int, pos, Stream),
   nl(Stream),
   nl(Stream),

   write_intentional_examples_domains_targets(1, LNeg_int, neg, Stream),

   close(Stream),

   discard_intentional_knowledge,
   intentional2:retractall(:-dynamic).


/* ========================================================================== */
/*             CONVERT intentional EXAMPLES INTO EXTENSIONAL ONES             */
/* ========================================================================== */

build_extensional_examples(
                            File_ex,  % file containing intentional examples,
                            File_bkg, % file containing intentional background
                            Negation  % true if negation by failure (else false)
                          ) :-

       writeln('building extensional examples...'),

					% get elements of the background knowledge
	  consult_background_knowledge(intentional, File_bkg),
	  get_clauses_background(intentional, LClauses_bkg),
	  get_modes(intentional, LModes),
       discard_plus_minus(LModes, LModes1),
	  get_modes_atoms(intentional, The_modes),
	  get_irrelevant(intentional, LIrrelevant),

					% get the examples

   	  read_intentional_examples(ex_data, File_ex, LPos_int, LNeg_int),

       reset_count(nb_examples),
	  writeln('positive examples...'),

					% build positive examples
        build_extensional_ex(
                             LPos_int,
                             LClauses_bkg,
                             LModes1,
                             Negation,
                             LIrrelevant,
                             LPos_int1,
                             LPos_ext
                            ),


        build_graph_examples(LPos_ext, LPos_ext_graph),
        build_interpretations(LPos_ext_graph, LPos_inter_graph),

        get_kth_arguments_tuples(LPos_int1, 3, LPos_target),

        deal_with_targets(LPos_target, LPos_inter_graph, LPos_inter_graph1),
        numbers_elements(1, LPos_inter_graph1, LPos_inter_graph2),

        deal_with_targets(LPos_target, LPos_ext, LPos_ext1),
        numbers_elements(1, LPos_ext1, LPos_ext2),

	   create_tables_possibilities(LPos_ext2, LPos_tp),

        reset_count(nb_examples),
        writeln('negative examples...'),

					  % build negative examples
        build_extensional_ex(
                             LNeg_int,
                             LClauses_bkg,
                             LModes1,
                             Negation,
                             LIrrelevant,
                             LNeg_int1,
                             LNeg_ext
                            ),


        build_graph_examples(LNeg_ext, LNeg_ext_graph),
        build_interpretations(LNeg_ext_graph, LNeg_inter_graph),

        get_kth_arguments_tuples(LNeg_int1, 3, LNeg_target),

        deal_with_targets(LNeg_target, LNeg_inter_graph, LNeg_inter_graph1),
        numbers_elements(1, LNeg_inter_graph1, LNeg_inter_graph2),

        deal_with_targets(LNeg_target, LNeg_ext, LNeg_ext1),
        numbers_elements(1, LNeg_ext1, LNeg_ext2),

	   create_tables_possibilities(LNeg_ext2, LNeg_tp),

        get_targets_domains(LPos_int1, pos, LTarget_pos, LDomain_pos),
        numbers_elements(1, LTarget_pos, LTarget_pos1),
	   numbers_elements(1, LDomain_pos, LDomain_pos1),

        get_targets_domains(LNeg_int1, neg, LTarget_neg, LDomain_neg),
	   numbers_elements(1, LTarget_neg, LTarget_neg1),
	   numbers_elements(1, LDomain_neg, LDomain_neg1),


					% create files
        create_extensional_examples_file(File_ex,
                                         LTarget_pos1, LDomain_pos1,
                                         LPos_inter_graph2, LPos_tp,
                                         LTarget_neg1, LDomain_neg1,
                                         LNeg_inter_graph2, LNeg_tp),


        create_extensional_background_file(File_ex, The_modes),

        create_intentional_remaining_file(File_ex, LPos_int1, LNeg_int1),

        discard_intentional_knowledge,

        intentional2:retractall(:-dynamic),
        writeln('finished.').


build_extensional_ex([], _LClauses, _LModes, _Negation,
                     _LIrrelevant, [], []) :-
   !.

build_extensional_ex(
                      [(LClauses_ex, LDomains, LTarget)|LEx_int],
                      LClauses_bkg,     % background knowledge(without neg)
                      LModes,           % declared modes
                      Negation,         % true if negation by failure
                      LIrrelevant,      % non relevant atoms
                      [(LClauses_ex, LDomains, LTarget)|LEx_int1],
                      [min_max(Ex_min, Ex_max)|LEx_ext]  % extensional examples
                    ) :-

 % get_count(nb_examples, N),

  compute_grounded_theory(LClauses_ex, LDomains, LClauses_bkg, LModes,
                          Negation, LIrrelevant, LClauses_negB, HB, LHead2),

  clauses_negative_literals_to_positive_ones(LClauses_negB, LClauses_pos),
   			% attention ne pas faire sort de LClauses_pos
   			% LClauses_pos et LClauses_neg doivent
            % avoir le meme nombre d'elements et etre dans le même ordre


  get_non_used_atoms(HB, LClauses_pos, LNon_used_atoms),


  build_partition(LClauses_pos, [], LParts),
  build_tables(LParts, LClauses_pos, LClauses_negB, LTables_min, LTables_max1),
				% necessaire uniquement pour les max
				% (tables avec 1 possibilite vide pour chaque table min)
  compute_tables_non_used_atoms(LNon_used_atoms, LTables_max2),
  append(LTables_max1, LTables_max2, LTables_max3),
  simplify_tables(LTables_min, Ex_min),
  simplify_tables(LTables_max3, Ex_max),

  discard_clauses_intentional2(LHead2),

  !,
  build_extensional_ex(
  				       LEx_int,
                       LClauses_bkg, LModes, Negation, LIrrelevant,
                       LEx_int1, LEx_ext).

	% the current example was not consistant
build_extensional_ex(
                      [(_Ex, _Domains, Target)|LEx_int],
                      LClauses_bkg,     % background knowledge(without neg)
                      LModes,           % declared modes
                      Negation,         % true if negation by failure
                      LIrrelevant,      % non relevant atoms
                      LEx_int1,
                      LEx_ext           % extensional examples
                    ) :-
     writeln('!!! the current treated example is not consistant !!!'),
     writeln(Target),
	 build_extensional_ex(
  				           LEx_int,
                           LClauses_bkg, LModes, Negation, LIrrelevant,
                           LEx_int1, LEx_ext
                          ).


get_targets_domains([], _Signe, [], []) :-
   !.

get_targets_domains([(_, Domain, Target)|LInt], Signe,
                    [(Signe,Target)|LTargets], [(Signe, Domain)|LDomains]) :-
   get_targets_domains(LInt, Signe, LTargets, LDomains).

	/* compute the grounded clausal theory representing the intentional
        ambiguous examples */
compute_grounded_theory(
                        LClauses_ex,
                        LDomains,
                        LClauses_bkg,
                        LModes,
                        Negation,
                        LIrrelevant,
                        LClauses_negB,
                        HB,
                        LHead2
                       ) :-

   append(LClauses_ex, LClauses_bkg, LClauses_ex_bkg),

   lear_clauses_to_prolog(LClauses_ex_bkg, LHead),
   discard_similar_elements(LHead, LHead1, structurally),

   build_Herbrand_base(LIrrelevant, LModes, LDomains, HB),

  % delete_similar_elements([], LHead1, LTrue1, strictly), % sans doute plus
														  % necessaire

   compute_grounded_theory_according_negation(Negation, HB,
                                              LClauses_ex_bkg,
                                              [], LTrue1, LClauses_neg),

   append(LHead1, LTrue1, LHead2),
   simplify_clauses(LClauses_neg, LClauses_negA),
   discard_similar_elements(LClauses_negA, LClauses_negA1, structurally),
   sort(LClauses_negA1, LClauses_negB).



	/* two ways for building the grounded theory */
	% negation by failure : negative facts is HB - LTrue1
compute_grounded_theory_according_negation(
                                           true,          % negation by failure
                                           HB,            % Herbrand basis
                                           _LClauses_ex_bkg,
                                           LTrue,         % list of known true facts
                                           _LTrue1,       % list of new true p.
                                           LClauses_neg   % grounded theory
                                          ) :-
   subtract(HB, LTrue, Lfalse),
   add_neg(Lfalse, Lfalse_neg),
   append(LTrue, Lfalse_neg, LClauses),
   translate_clauses(LClauses, LClauses_neg).


compute_grounded_theory_according_negation(
                                       false,         % not negation by failure
                                       HB,            % Herbrand basis
                                       LClauses_ex_bkg,
                                       _LTrue,        % list of known true facts
                                       LTrue1,        % list of new true predi.
                                       LClauses_neg   % grounded theory
                                          ) :-
   inserer_dans_base(LTrue1),
   append(LClauses_ex_bkg, LTrue1, LClauses),

   translate_clauses(LClauses, LClauses_int),
  						  % builds instantiated clauses according to HB
   instantiate_clauses(LClauses_int, HB, LClauses_neg).


	/* build a negative atom from each atom */
add_neg([], []) :-
   !.

add_neg([Atom|LAtom], [neg(Atom)|LAtom_neg]) :-
   add_neg(LAtom, LAtom_neg).


   /* get all false atoms */
get_false_atoms([], []) :-
   !.

get_false_atoms([[neg(Atom)]|LClauses], [Atom|LAtoms]) :-
   ground(Atom),
   !,
   get_false_atoms(LClauses, LAtoms).


get_false_atoms([_Clause|LClauses], LAtoms) :-
   get_false_atoms(LClauses, LAtoms).



   /* discard of HB all atoms that are not true of false
      and that are not in the LAbducibles predicates */

discard_non_abducibles_atoms([], _Lnon_abducibles, _LDetermined, []) :-
   !.

discard_non_abducibles_atoms([Atom|LAtoms], Lnon_abducibles, LDetermined,
                             [Atom|LAtoms1]) :-
   member(Atom, LDetermined),     % keep Atom because it is determined,
                                  % (abducible or not)
   !,
   discard_non_abducibles_atoms(LAtoms, Lnon_abducibles, LDetermined, LAtoms1).


discard_non_abducibles_atoms([Atom|LAtoms], Lnon_abducibles, LDetermined,
                             [Atom|LAtoms1]) :-
   functor(Atom, Predicate, _Arity),
   \+ member(Predicate, Lnon_abducibles),   % keep Atom because it is abducible
   !,
   discard_non_abducibles_atoms(LAtoms, Lnon_abducibles, LDetermined, LAtoms1).

discard_non_abducibles_atoms([_Atom|LAtoms], Lnon_abducibles, LDetermined,
                             LAtoms1) :-
                                       % don't keep atom :
                                       % it is undetermined and non abducible
   discard_non_abducibles_atoms(LAtoms, Lnon_abducibles, LDetermined, LAtoms1).



/* discard non valid atoms from the Herbrand base HB */

discard_non_valid_atoms([], []) :-
   !.

discard_non_valid_atoms([Atom|LAtoms], [Atom|LAtoms_out]) :-
   valid_atom(Atom),
   !,
   discard_non_valid_atoms(LAtoms, LAtoms_out).

discard_non_valid_atoms([_Atom|LAtoms], LAtoms_out) :-
   discard_non_valid_atoms(LAtoms, LAtoms_out).


 /* saturate the knowledge base according to the clauses
     of the form Atom <= Body.
     We insert Atom for all possibilities of Body */
saturate([], []) :-					   % nothing to saturate
   !,
   retract_no_change.

saturate(_, []) :-                    % previous saturation has made no change
   retract(intentional2:no_change),
   !.

saturate(LSaturation, LHead) :-
   assert(intentional2:no_change),
   saturation(LSaturation, LSaturation1, LHead1),
   saturate(LSaturation1, LHead2),
   append(LHead1, LHead2, LHead).


	/* achieve the saturation */
saturation([], [], []) :-
   !.

saturation(
            [Atom <= Body |LSaturation],    % saturation clauses
            LSaturation1,                   % saturation clauses not used
            LHead                           % facts created by saturation
          ) :-
   enumeration_to_commas(Body, Body1),
   findall(Atom, intentional2:Body1, LAtoms),
   \+ empty(LAtoms),
   !,
   retract_no_change,
   assert_terms(LAtoms),
   saturation(LSaturation, LSaturation1, LHead1),
   append(LAtoms, LHead1, LHead).

 saturation([Clause|LSaturation],
            [Clause| LSaturation1],
            LHead) :-
    saturation(LSaturation, LSaturation1, LHead).


/* transforms saturation clause into ordinary clauses */
saturation_to_clauses([]) :-
   !.

saturation_to_clauses([A <= B|LClauses_sat]) :-
   enumeration_to_commas(B, B1),
   Body = ','(B1, \+A),
   intentional2:asserta(falsity :- Body),
   saturation_to_clauses(LClauses_sat).


/*  get all clauses of saturation */
get_saturation_clauses([], [], []) :-
   !.

get_saturation_clauses(
                       [(A <= B)| LClauses],
                       LClauses_no_sat,
                       [A <= B|LClauses_sat]
                       ) :-
    !,
   get_saturation_clauses(LClauses, LClauses_no_sat, LClauses_sat).

get_saturation_clauses(
                       [Clause| LClauses],
                       [Clause|LClauses_no_sat],
                       LClauses_sat
                       ) :-
   get_saturation_clauses(LClauses, LClauses_no_sat, LClauses_sat).


/* assert all terms of the list in the module intentional2 */
assert_terms([]) :-
   !.

assert_terms([Term|LTerm]) :-
  intentional2:asserta(Term),
  assert_terms(LTerm).

retract_no_change :-
   retract(intentional2:no_change),
   !.

retract_no_change.


   /* discard all neutral tables */
simplify_tables(LTables, LTables_out) :-
   delete(LTables, [[]], LTables1),
   check_tables(LTables1, LTables_out).


	/* if no more table one add the neutral table */
check_tables([], [[[]]]) :-
   !.

check_tables(LTables, LTables).


        /* discard all data in the module intentional */
discard_intentional_knowledge :-
   retractall(intentional:background_knowledge(_)),
   retractall(intentional:herbrand_base(_)),
   retractall(intentional:positive_examples(_)),
   retractall(intentional:negative_examples(_)),
   retractall(intentional:mode(_)),
   retractall(intentional:types_under_oi(_)),
   retractall(intentional:types_instantiable(_)),
   retractall(intentional:abducible_predicates(_)).


        /* discard all data in the module intentional2 */
discard_clauses_intentional2([]) :-
   !.

discard_clauses_intentional2([Head|LHeads]) :-
   intentional2:retractall(Head),
   discard_clauses_intentional2(LHeads).


	/* create a file containing not discarded intentional examples */
create_intentional_remaining_file(File_int, LPos_int, LNeg_int) :-

   atom_concat(File_int, '_remaining.int', File_int1),
   open(File_int1, write, Stream),

   write(Stream, ':- style_check(-discontiguous).'),
   nl(Stream),
   nl(Stream),

   write_intentional_examples_domains_targets(1, LPos_int, pos, Stream),
   nl(Stream),
   nl(Stream),

   write_intentional_examples_domains_targets(1, LNeg_int, neg, Stream),

   close(Stream).


        /* create the extensional files from extensional examples */
create_extensional_examples_file(
                                 File,
                                 LTarget_pos,
                                 LDomain_pos,
                                 LPos_inter_graph,
                                 LPos_tp,
                                 LTarget_neg,
                                 LDomain_neg,
                                 LNeg_inter_graph,
                                 LNeg_tp
                                 ) :-

           % write the file
   atom_concat(File, '.pl', File_out),
   open(File_out, write, Out),

   fwriteln_point(Out, loaded_examples),
   nl(Out),
   fwriteln_point(Out,':-style_check(-discontiguous)'),
   nl(Out),

   fwriteln(Out, 'examplesP('),
   fwriteln(Out, '['),
   write_examples(LPos_inter_graph, Out),
   fwriteln(Out,']'),
   fwriteln(Out,').'),

   nl(Out),
   nl(Out),

   fwriteln(Out, 'tabs(pos,'),
   fwriteln(Out, '['),
   write_tabs(LPos_tp, Out),
   fwriteln(Out,']'),
   fwriteln(Out,').'),

   nl(Out),
   nl(Out),

   fwriteln(Out, 'examplesN('),
   fwriteln(Out, '['),
   write_examples(LNeg_inter_graph, Out),
   fwriteln(Out, ']'),
   fwriteln(Out,').'),


   fwriteln(Out, 'tabs(neg,'),
   fwriteln(Out, '['),
   write_tabs(LNeg_tp, Out),
   fwriteln(Out,']'),
   fwriteln(Out,').'),

   nl(Out),
   nl(Out),

   write_targets(LTarget_pos, Out),
   write_targets(LTarget_neg, Out),

   nl(Out),
   nl(Out),

   write_domains(LDomain_pos, Out),
   write_domains(LDomain_neg, Out),

   close(Out).


write_tables_possibilities([],  _Out) :-
   !.

write_tables_possibilities([TP|LTP], Out) :-
   fwrite(Out, '('),
   fwrite(Out, TP),
   fwriteln(Out,').'),
   write_tables_possibilities(LTP, Out).



  /* write the examples */
write_tabs([], _Out) :-
   !.

write_tabs([Ex], Out) :-
   write_one_tab(Ex, Out),
   nl(Out),
   !.

write_tabs([Ex|LEx],  Out) :-
   write_one_tab(Ex, Out),
   fwriteln(Out,','),
   write_tabs(LEx, Out).


	/* write one tab on the file Out */
write_one_tab((Num, Exp_max), Out) :-
   fwrite(Out, '('),
   fwrite(Out, Num),
   fwrite(Out, ','),
   nl(Out),
   fwrite_list(Out, Exp_max),
   nl(Out),
   fwrite(Out,')').


   /* write the examples */

write_examples([], _) :-
   !.

write_examples([Ex], Out) :-
   write_one_example(Ex, Out),
   nl(Out),
   !.

write_examples([Ex|LEx],  Out) :-
   write_one_example(Ex, Out),
   fwriteln(Out,','),
   write_examples(LEx, Out).


	/* write one example on the file Out */
write_one_example((Num, Head, min_max(Exp_min, Exp_max)), Out) :-
   fwrite(Out, '('),
   fwrite(Out, Num),
   fwrite(Out, ','),
   fwrite(Out, Head),
   fwrite(Out, ','),
   nl(Out),
   fwrite(Out, 'min_max('),
   nl(Out),
   fwrite_list(Out, Exp_min),
   fwrite(Out, ','),
   nl(Out),
   \+ \+ (
          numbervars(Exp_max, 0, _, [singletons(true)]),
          fwrite_list(Out, Exp_max)
         ),
   fwrite(Out, ')'),
   fwrite(Out,')').


  /* write the targets on file */
write_targets([], _) :-
   !.

write_targets([(Num, Label, T)|LL], Out) :-
   fwrite(Out, 'target('),
   fwrite(Out, Num),
   fwrite(Out, ','),
   fwrite(Out, Label),
   fwrite(Out,','),
   fwrite(Out, T),
   fwriteln(Out,').'),
   write_targets(LL, Out).


  /* write the domains on file */
write_domains([], _) :-
   !.

write_domains([(Num, Label, L)|LL], Out) :-
   fwrite(Out, 'domains('),
   fwrite(Out, Num),
   fwriteln(Out,','),
   fwrite(Out, Label),
   fwrite(Out,','),
   fwrite_list(Out, L),
   fwriteln(Out,').'),
   write_domains(LL, Out).




create_extensional_background_file(File, LModes) :-
   atom_concat(File, '.bkg', File_out),
   open(File_out, write, Out),
   fwriteln_point(Out, loaded_background),
   nl(Out),

   add_relational_target(Out),
   intentional:target_mode(Mode),
   fwriteln_point(Out, mode(Mode)),

   treat_modes_plus(LModes, Out),
   treat_arg_plus(LModes, Out),

   intentional:types_instantiable(LTypes_instantiable),
   fwriteln_point(Out, types_instantiable(LTypes_instantiable)),
   intentional:types_under_oi(LTypes_oi),
   fwriteln_point(Out, types_under_oi(LTypes_oi)),
   close(Out).


treat_modes_plus([], _Out) :-
   !.

treat_modes_plus([mode(Mode)|LModes], Out) :-
    Mode=..[Pred|LArgs],
    discard_plus_minus_args(LArgs, LArgs1),
    Mode1=..[Pred|LArgs1],
    fwriteln_point(Out, mode(Mode1)),
    treat_modes_plus(LModes, Out).

treat_arg_plus([], _Out) :-
   !.

treat_arg_plus([mode(Mode)|LModes], Out) :-
    Mode=..[Pred|LArgs],
    discard_args_plus(LArgs, LArgs1),
    Mode1=..[Pred|LArgs1],
    fwriteln_point(Out, mode_arguments(Mode1)),
    treat_arg_plus(LModes, Out).


        /* add the flag 'clausal' to the file if examples are clauses */
add_relational_target(Out) :-
   intentional:target_relation(R),
   !,
   fwriteln_point(Out, target_relation(R)).


add_relational_target(_Out).


/* ========================================================================== */
/*                          BUILDING PARTITION AND TABLES                     */
/* ========================================================================== */


	/* add all possible tables representing the non used atoms of HB */
compute_all_tables_non_used_atoms([], []) :-
   !.

compute_all_tables_non_used_atoms([Atom|LAtoms], [[[], [Atom]]|LTables_max]) :-
   compute_all_tables_non_used_atoms(LAtoms, LTables_max).


	/* add the tables representing the non used atoms of HB */
compute_tables_non_used_atoms([], []) :-
   !.

compute_tables_non_used_atoms([Atom|LAtoms], [[[Atom]]|LTables_max]) :-
   compute_tables_non_used_atoms(LAtoms, LTables_max).


/* get the atoms of HB non used in the clauses of LClauses */
get_non_used_atoms([], _LClauses, []) :-
   !.

get_non_used_atoms([Atom|LAtoms], LClauses, LNon_used_atoms) :-
   used_in_clauses(Atom, LClauses),
   !,
   get_non_used_atoms(LAtoms, LClauses, LNon_used_atoms).

get_non_used_atoms([Atom|LAtoms], LClauses, [Atom|LNon_used_atoms]) :-
   get_non_used_atoms(LAtoms, LClauses, LNon_used_atoms).


/* check whether Atom is used in a clause of LClauses */
used_in_clauses(_Atom, []) :-
   !,
   fail.

used_in_clauses(Atom, [Clause|_LClauses]) :-
   member(Atom, Clause),
   !.

used_in_clauses(Atom, [_Clause|LClauses]) :-
   used_in_clauses(Atom, LClauses).

/* check whether Atom is used in Clause (reprented as a list of atoms */


        /* get all constants of the grounded atoms in LAtoms */
get_arguments([], []) :-
   !.

get_arguments([Atom|LAtoms], LArgs_out) :-
   Atom=..[_|LArgs],
   get_arguments(LAtoms, LArgs1),
   append(LArgs, LArgs1, LArgs_out).


/* build the product of tables representing all the models of a
		clausal theory */
build_all_models(LDomains, LClauses_bkg, LModes, LIrrelevant, LTables) :-

	compute_grounded_theory([], LDomains, LClauses_bkg, LModes,
                             false, LIrrelevant, LClauses_negB, HB, _LHead2),

     clauses_negative_literals_to_positive_ones(LClauses_negB, LClauses_pos),
   			% attention ne pas faire sort de LClauses_pos
   			% LClauses_pos et LClauses_neg doivent
               % avoir le meme nombre d'elements et etre dans le même ordre



	build_partition(LClauses_pos, [], LParts),
  	build_all_tables(LParts, LClauses_pos, LClauses_negB, LTables1),

	get_non_used_atoms(HB, LClauses_pos, LNon_used_atoms),
  	compute_all_tables_non_used_atoms(LNon_used_atoms, LTables2),

  	append(LTables1, LTables2, LTables3),
  	simplify_tables(LTables3, LTables).


		/* build the set of all the models of the clausal thoery LClauses_neg
            in a tables format given by LTables */
build_all_tables(LParts, LClauses, LClauses_neg, LTables) :-
	  	associate_CNFs_with_partition(LParts, LClauses, LClauses_neg, LCNFs),
          translate_all_CNFs_to_tables(LCNFs, LTables1),
		factorize_tables(LTables1, LTables).


build_tables(LParts, LClauses, LClauses_neg, LTables_min, LTables_max) :-
        associate_CNFs_with_partition(LParts, LClauses, LClauses_neg, LCNFs),
        translate_CNFs_to_tables(LCNFs, LTables_min1, LTables_max1),
	   factorize_tables(LTables_min1, LTables_min),
	   factorize_tables(LTables_max1, LTables_max).


factorize_tables([], []) :-
   !.

factorize_tables([Table|LTables],LTables_factorized) :-
	factorize_one_table(Table, Table_factorized),
						% Table_factorized is a list of two or one table
	factorize_tables(LTables, LTables_factorized1),
	append(Table_factorized, LTables_factorized1, LTables_factorized).


	/* gather the grounded atoms that are in each possibility of
	   the Table into anoter table */

						% one single possibility in the table
factorize_one_table([Possibility], [[Possibility]]) :-
   !.

factorize_one_table(Table, Tables_factorized) :-
	Table = [Possibility|LPossibilities],
						% Possibility contains all possible shared atoms
						% it must be refined
	get_shared_atoms(LPossibilities, Possibility, LShared_atoms),
	discard_shared_atoms(Table, LShared_atoms, Table1),
	build_factorized_tables(LShared_atoms, Table1, Tables_factorized).

						% no shared atoms
build_factorized_tables([], Table, [Table]) :-
   !.

build_factorized_tables(LShared_atoms, Table, [[LShared_atoms], Table]).


	/* get the atoms share by each possibility of the Table */

						% no possible shared atoms
get_shared_atoms(_Table, [], []) :-
   !.
						% no more possibility to explore
get_shared_atoms([], LShared_atoms, LShared_atoms) :-
   !.

get_shared_atoms([Possibility|LPossibilities],
				  LShared_atoms_seen, LShared_atoms) :-
	intersection(Possibility, LShared_atoms_seen, LShared_atoms_seen1),
	get_shared_atoms(LPossibilities, LShared_atoms_seen1, LShared_atoms).


	/* discard from each possibility of Table the atoms shared by all
       the possibility */

						% no shared atoms
discard_shared_atoms(Table, [], Table) :-
   !.
						% no more possibility to explore
discard_shared_atoms([], _Shared_atoms, []) :-
   !.

discard_shared_atoms([Possibility|LPossibilities], LShared_atoms,
					 [Possibility1|LPossibilities1]) :-
	subtract(Possibility, LShared_atoms, Possibility1),
	discard_shared_atoms(LPossibilities, LShared_atoms, LPossibilities1).


        /* each instantiated CNF is translated in an instantiated DNF (table),
		and all tables are gathered in a set of tables representing
          an ambiguous example */
translate_all_CNFs_to_tables([], []) :-
   !.

translate_all_CNFs_to_tables(
                             [(Part,CNF)|LCNFs],
					    [Table|LTables]
			               ) :-
    keep_minimal_lists(CNF, CNF1),
    cnf_to_dnf(CNF1, DNF),
    build_models_DNF(all, Part, DNF, Table1),
    sort(Table1, Table),
    translate_all_CNFs_to_tables(LCNFs, LTables).


        /* each instantiated CNF (corresponding to one table) is translated in
           an instantiated DNF (table), and all tables are gathered in
           a set of tables representing ambiguous examples */
translate_CNFs_to_tables([], [], []) :-
   !.

translate_CNFs_to_tables(
                          [(Part,CNF)|LCNFs],
                          [Table_min2|LTables_min],
					           [Table_max2|LTables_max]
			               ) :-
    keep_minimal_lists(CNF, CNF1),
    cnf_to_dnf(CNF1, DNF),
    build_models_DNF(negative, Part, DNF, Table_min),
    build_models_DNF(positive, Part, DNF, Table_max),
    sort(Table_min, Table_min1),
    sort(Table_max, Table_max1),
    keep_minimal_lists(Table_min1, Table_min2),
    keep_maximal_lists(Table_max1, Table_max2),
    translate_CNFs_to_tables(LCNFs, LTables_min, LTables_max).


        /* build all models of the instantiated DNF */
build_models_DNF(_Signe, _Part, [], []) :-
   !.

build_models_DNF(Signe, Part, [Conj|LConj], LModels_out) :-
   build_model_conjunction(Signe, Part, Conj, LModels_conj),
   build_models_DNF(Signe, Part, LConj, LModels),
   append(LModels, LModels_conj, LModels_out).


        /* build the maximal model of the conjunction Conj
		 Part is the set of considered atoms in this part,
           that is the sub Herbrand basis */
build_model_conjunction(positive, Part, Conj, [Model]) :-
   !,
   negative_literals_to_positive_ones(Conj, Conj1),
   subtract(Part, Conj1, Part1),    		 % atoms of Part not used in Conj
   delete_negative_literals_one_conj(Conj, Conj2),
   append(Conj2, Part1, Model).


        /* build the minimal model of conjunction Conj */
build_model_conjunction(negative, _Part, Conj, [Model]) :-
    !,
   delete_negative_literals_one_conj(Conj, Model).

       /* build all the models of the conjunction Conj */
build_model_conjunction(all, Part, Conj, LModels) :-
   negative_literals_to_positive_ones(Conj, Conj1),
   subtract(Part, Conj1, Part1),    		 % atoms of Part not used in Conj
   all_parts(Part1, LParts), 				 % all combinations with atoms
									 % not used in Conj
   delete_negative_literals_one_conj(Conj, Basis_model),
   append_list_to_lists(Basis_model, LParts, LModels).


delete_negative_literals([], []) :-
   !.

delete_negative_literals([Conj|LConj], [Conj_out|LConj_out]) :-
   delete_negative_literals_one_conj(Conj, Conj_out),
   delete_negative_literals(LConj, LConj_out).


delete_negative_literals_one_conj([], []) :-
   !.

delete_negative_literals_one_conj([neg(_)|LAtoms], LAtoms_out) :-
   !,
   delete_negative_literals_one_conj(LAtoms, LAtoms_out).


delete_negative_literals_one_conj([Atom|LAtoms], [Atom|LAtoms_out]) :-
   !,
   delete_negative_literals_one_conj(LAtoms, LAtoms_out).


        /* gather all clauses associated with a same part with this part */
associate_CNFs_with_partition([], _LClauses, _LClauses_neg, []) :-
   !.                                       % all tables have been treated

associate_CNFs_with_partition(_LPars, [], [], []) :-
   !.                                       % all clauses have been treated

associate_CNFs_with_partition(
                           [Part|LParts],
                           LClauses,
                           LClauses_neg,
                           [(Part,Part_clauses)|LParts_clauses]) :-
   associate_CNFs_with_one_part(Part, LClauses, LClauses_neg,
                                LClauses1, LClauses_neg1, Part_clauses),
   associate_CNFs_with_partition(LParts, LClauses1, LClauses_neg1,
                              LParts_clauses).

   /* gather all clauses associated with Part in Part_clauses */
associate_CNFs_with_one_part(_Table, [], [], [], [], []) :-
    !.

associate_CNFs_with_one_part(
                              Part,
                              [Clause|LClauses],           % list of atoms
                              [Clause_neg|LClauses_neg],   % clauses with not
                              LClauses_out,
                              LClauses_neg_out,
                              [Clause_neg|LClauses_part]
                              ) :-
   intersection(Part, Clause, I),
   \+ empty(I),                % current Clause depends on Table
   !,
   associate_CNFs_with_one_part(Part, LClauses, LClauses_neg,
                                 LClauses_out, LClauses_neg_out,
                                 LClauses_part).

   associate_CNFs_with_one_part(
                              Part,
                              [Clause|LClauses],
                              [Clause_neg|LClauses_neg],
                              [Clause|LClauses_out],
                              [Clause_neg|LClauses_neg_out],
                              LClauses_part
                              ) :-
                              % current Clause does not depends on table
   associate_CNFs_with_one_part(Part, LClauses, LClauses_neg,
                                 LClauses_out, LClauses_neg_out,
                                 LClauses_part).


   /* identify dependant atoms of a CNF and place them in a same table */
  build_partition([], LParts, LParts) :-
     !.

  build_partition(
                   [Clause|LClauses],    % Clauses to check
                   LParts,               % Tables already created
                   LParts_out            % Final tables
                  ) :-
     sort(Clause, Clause2),
     check_partition(Clause2, LParts, LParts_out1),
     build_partition(LClauses, LParts_out1, LParts_out).


     /* Update parts by checking atoms of Clauses and current parts */
  check_partition(Part, [], [Part_out]) :-
     !,                                 % Clause becomes a table
     sort(Part, Part_out).

  check_partition(
                   Part_built,            % current built part
                   [Part|LParts],         % explored parts
                   LParts_out             % Final parts
                  ) :-
     intersection(Part_built, Part, Inter),
     \+ empty(Inter),
     !,
     append(Part_built, Part, Part_built1),
     check_partition(Part_built1, LParts, LParts_out).

   check_partition(
                   Part_built,         % current built part
                   [Part|LParts],      % explored Parts
                   [Part|LPart_out]    % Final partition
                  ) :-
        check_partition(Part_built, LParts, LPart_out).

        /* transform negative literals in positive literals */
   clauses_negative_literals_to_positive_ones([], []) :-
      !.

   clauses_negative_literals_to_positive_ones([Clause|LClauses],[Clause1|LClauses1]) :-
      negative_literals_to_positive_ones(Clause, Clause1),
      clauses_negative_literals_to_positive_ones(LClauses, LClauses1).


      /* transform negative literals in positive literals */
   negative_literals_to_positive_ones([], []) :-
      !.

   negative_literals_to_positive_ones([neg(Atom)|LAtoms],[Atom|LAtoms_out]) :-
      !,
      negative_literals_to_positive_ones(LAtoms, LAtoms_out).

   negative_literals_to_positive_ones([Atom|LAtoms],[Atom|LAtoms_out]) :-
      negative_literals_to_positive_ones(LAtoms, LAtoms_out).


   /* instantiate a list of clauses by using facts */
instantiate_clauses([], _LFacts, []) :-
   !.

instantiate_clauses(
                     [Clause|LClauses],
                     LFacts,
                     LClauses_instantiated
                   ) :-
    findall(
             Instantiation,
             instantiate_one_clause(Clause, LFacts, Instantiation),
             LL1
           ),
    instantiate_clauses(LClauses, LFacts, LL2),
    append(LL1, LL2, LClauses_instantiated).


   /* instantiate a list of atoms by using facts */
instantiate_one_clause([], _LFacts, []) :-
   !.

	% if a clause contains X=Y and X=Y is true, the clause is a tautologie,
	% we can discard it,
    % if X=Y is false we keep the clause and discard X=Y
instantiate_one_clause(
                              [X=Y|LAtoms],
                              LFacts,
                              LAtoms_instantiated
                             ) :-
   X\=Y,
   instantiate_one_clause(LAtoms, LFacts, LAtoms_instantiated).

 % if a clause contains X\=Y and X\=Y is true, the clause is a tautologie,
	% we can discard it, otherwhise we keep the clause and discard X\=Y
instantiate_one_clause(
                              [X\=Y|LAtoms],
                              LFacts,
                              LAtoms_instantiated
                             ) :-
   X=Y,
   instantiate_one_clause(LAtoms, LFacts, LAtoms_instantiated).

instantiate_one_clause(
                              [neg(Atom)|LAtoms],
                              LFacts,
                              [neg(Atom)|LAtoms_instantiated]
                             ) :-
   member(Atom, LFacts),           % instantiate Atom
   instantiate_one_clause(LAtoms, LFacts, LAtoms_instantiated).

instantiate_one_clause(
                              [Atom|LAtoms],
                              LFacts,
                              [Atom|LAtoms_instantiated]
                             ) :-
   Atom \= neg(_X),
   member(Atom, LFacts),           % instantiate Atom
   instantiate_one_clause(LAtoms, LFacts, LAtoms_instantiated).



/* ========================================================================== */
/*                  MODELES DE HERBRAND DES EXEMPLES                          */
/* ========================================================================== */

        /* add dynamic declarations corresponding to predicates
           declared in the modes, into the module intentional2 */

call_dynamic_declarations(Module, []) :-
   Module:(dynamic neg/1),
   Module:(dynamic or/1),
   !.

call_dynamic_declarations(Module, [Mode|LModes]) :-
   Mode=..[Functor|LArgs],
   length(LArgs, N),
   Module:(dynamic Functor/N),
   call_dynamic_declarations(Module, LModes).


call_dynamic_declarations([]) :-
   intentional2:(dynamic neg/1),
   intentional2:(dynamic or/1),
   !.

call_dynamic_declarations([Mode|LModes]) :-
   Mode=..[Functor|LArgs],
   length(LArgs, N),
   intentional2:(dynamic Functor/N),
   call_dynamic_declarations(LModes).


        /* build the Herbrand base from the domains of types and the modes */
build_Herbrand_base(_LIrrelevant, [], _LDomains, []) :-
   !.                                             % no more mode to consider


build_Herbrand_base(
			     LIrrelevant,
			     [Mode|LModes],
                    LDomains,
                    HB
                   ) :-
   build_atoms(Mode, LDomains, HBA),
   discard_irrelevant_atoms(LIrrelevant, HBA, HB1),
   build_Herbrand_base(LIrrelevant, LModes, LDomains, HB2),
   append(HB1, HB2, HB).


	/* discard atoms that match with atoms of the irrelevant list */
discard_irrelevant_atoms([], LAtom, LAtom) :-
   !.

discard_irrelevant_atoms([Clause|LClause], LAtom, LAtom_out) :-
   deal_with_irrelevant_clause(Clause, LAtom, LAtom1),
   discard_irrelevant_atoms(LClause, LAtom1, LAtom_out).


	/* discard atoms that are not relevant with respect to Clause */
deal_with_irrelevant_clause(Head <- Body, LAtom, LAtom_out) :-
  !,
  get_body(Body, LBody),
  deal_with_one_irrelevant_clause(Head, LBody, LAtom, LAtom_out).

deal_with_irrelevant_clause(Atom, LAtom, LAtom_out) :-
   delete_all(LAtom, Atom, LAtom_out).


	/* deal all irrelevant atoms according to LBody and Head */
deal_with_one_irrelevant_clause(Head, LBody, LAtom, LAtom_out) :-
  delete_one_irrelevant_atom(Head, LBody, LAtom, LAtom1),
  !,
  deal_with_one_irrelevant_clause(Head, LBody, LAtom1, LAtom_out).

deal_with_one_irrelevant_clause(_Head, _LBody, LAtom, LAtom).


delete_one_irrelevant_atom(Head, LBody, LAtom, LAtom1) :-
  copy_term((Head, LBody), (Head1, LBody1)),  % to not instantiate variable
  is_subset(LBody1, LAtom),
  select(Head1, LAtom, LAtom1).



	/* get the list of facts inside Body */
get_body(Atom and Body, [Atom|LBody]) :-
   !,
   get_body(Body, LBody).

get_body(Atom, [Atom]).


        /* build the grounded atoms associates to the current mode */
build_atoms(Mode, LDomains, LAtoms) :-
   Mode=..[Functor|LTypes],
   get_domains(LTypes, LDomains, List_domains),
   !,
   cross_product_arguments(List_domains, List_arguments),
   build_all_atoms(Functor, List_arguments, LAtoms).

build_atoms(_Mode, _LDomains, []).   % not relevent mode


        /* make the cross product of arguments included in List_domains */

cross_product_arguments([], []) :-       % no domain
   !.

cross_product_arguments(LDomains, []) :-
   member([], LDomains),      % no cross product if there is an empty list
   !.

cross_product_arguments(LDomains, LProduct) :-
   cross_product_lists(LDomains, LProduct).


/* the list of types becomes a list of domains */
get_domains([], _, []) :-
   !.

get_domains([Type|LTypes], LDomains, [Domain|List_domains]) :-
   functor(Atom, Type, 1),
   member(Atom, LDomains),
   arg(1, Atom, Domain),
   get_domains(LTypes, LDomains, List_domains).


        /* build all grounded atoms having the arguments that are
           in List_arguments */

build_all_atoms(Functor, [], [Functor]) :-      % propositionnal atom
   !.

build_all_atoms(Functor, LArguments, LAtoms) :-
   build_all_atoms2(Functor, LArguments, LAtoms).


build_all_atoms2(_, [], []) :-
   !.

build_all_atoms2(Functor, [LArgs|List_arguments], [Atom|LAtoms]) :-
   Atom=..[Functor|LArgs],
   % valid_atom(Atom),
   !,
   build_all_atoms2(Functor, List_arguments, LAtoms).

build_all_atoms2(Functor, [_LArgs|List_arguments], LAtoms) :-
   build_all_atoms2(Functor, List_arguments, LAtoms).


        /* Atom is valid whether it does not trigger the fact false */

valid_atom(Atom) :-       % Atom is already in the base which is consistent
   intentional2:Atom,
   !.

valid_atom(Atom) :-
   intentional2:asserta(Atom),
   intentional2:falsity,
   !,
   intentional2:retract(Atom),
   fail.

valid_atom(Atom) :-
   intentional2:retract(Atom).

        /* get all atoms appearing in the provided clauses */
get_atoms_of_clauses([], []) :-
   !.

get_atoms_of_clauses(
                     [Clause|LClauses],
                     LAtoms_out
                    ) :-
   get_atoms_clause(Clause, LAtoms_clause),
   get_atoms_of_clauses(LClauses, LAtoms),
   append(LAtoms_clause, LAtoms, LAtoms_out).

        /* get all grounded atoms of the current clause */
get_atoms_clause(Head <- Body, LAtoms) :-
      !,
        get_atoms_enumeration(Head, LAtoms_head),
        get_atoms_enumeration(Body, LAtoms_body),
        append(LAtoms_head, LAtoms_body, LAtoms).

get_atoms_clause(<- Body, LAtoms) :-
      !,
        get_atoms_enumeration(Body, LAtoms).

get_atoms_clause(Head, LAtoms) :-
        get_atoms_enumeration(Head, LAtoms).

        /* get all grounded atoms referenced in an enumeration of atoms
           separated with 'or' or 'and' */
get_atoms_enumeration(Enum, LAtoms) :-
   enumeration_to_list(Enum, LAtoms).


/* ========================================================================== */
/*                CONSTRUCTION DES FAITS DEDUCTIBLES                          */
/* ========================================================================== */

                        /* un fait est vrai s'il est deductible de la base */
                        /* de connaissances                                */
build_true_facts([], [], []) :-
        !.

build_true_facts(
                         [Atome|Faits], /* liste des faits vrais possible   */
                         Faits_pas_vrais,
                         [Atome|Faits_vrais]
                      ) :-
        intentional2:Atome,    /* Atome est vrai car deductible de la base */
        !,
        build_true_facts(Faits, Faits_pas_vrais, Faits_vrais).


build_true_facts(
                         [Atome|Faits],
                         [Atome|Faits_pas_vrais],
                         Faits_vrais
                       ) :-
        build_true_facts(Faits, Faits_pas_vrais, Faits_vrais).


                /* un fait est false si une contrainte est violee quand on */
                /* l ajoute a la base de connaissance                     */
build_false_facts([], [], []) :-
        !.

build_false_facts(
                             [Atome|Faits],     % liste des faits false possibles
                             [Atome|Faits_pas_false],
                             Faits_false
                             ) :-
        interpretation_ok_for_false([Atome]),
        !,
        build_false_facts(Faits, Faits_pas_false, Faits_false).


build_false_facts(
                              [Atome|Faits],
                              Faits_pas_false,
                              [Atome|Faits_false]
                             ) :-
        build_false_facts(Faits, Faits_pas_false, Faits_false).


construire_nouveaux_faits_false(Faits_pas_vrais, Faits_incertains,
                               Faits_false) :-
        build_false_facts(Faits_pas_vrais, Faits_incertains, Faits_false).


construire_nouveaux_faits(Faits_vrais, Faits_incertains) :-
        faits_incertains(FI),
        build_true_facts(FI, Faits_pas_vrais, Faits_vrais),
        construire_nouveaux_faits_false(Faits_pas_vrais, Faits_incertains, _).


/* ========================================================================== */
/*              VERIFIE L''INTEGRITE DE LA BASE DE CONNAISSANCES              */
/* ========================================================================== */

        /* check that considering Atom as true is compatible with
           the background knowledge */
is_true_ok(Atom) :-
        constraints_false_ok(Atom).

is_false_ok(Atom) :-
        \+ intentional2:Atom. % ok : Atom is not derived frome the background knowledge


        /* true si la base reste integre quand on ajoute atom */
constraints_false_ok(Atom) :-
        intentional2:assert(Atom),
        falsity,              % false success when a constrainst is not satisfied.
        !,
        intentional2:retract(Atom),
        fail.

constraints_false_ok(Atom) :-
        intentional2:retract(Atom). % la base est integre


check_minimal_interpretation(I, Code) :-
        inserer_dans_base(I),
        check_min(Code),
        enlever_de_base(I).

check_min(Code) :-
        base_ok_for_false ->
                (
                    base_ok_for_or ->
                        Code == ok_base
                        ;
                        Code == ok_false
                )
                ;
                Code == nok.


check_maximal_interpretation(I, Code) :-
        inserer_dans_base(I),
        check_max(Code),
        enlever_de_base(I).


check_max(Code) :-
        base_ok_for_or ->
                (
                    base_ok_for_false ->
                        Code == ok_base
                        ;
                        Code == ok_or
                )
                ;
                Code == nok.

base_ok:-
        base_ok_for_false,
        base_ok_for_or.

base_ok_for_false :-
        intentional2:falsity,
        gtrace,
        !,
        fail.

base_ok_for_false.

base_ok_for_or :-
                intentional2:findall(Clause_or, or(Clause_or), LClauses_or),
                list_or_ok(LClauses_or).


list_or_ok([]) :-
        !.

list_or_ok([Clause_or|LClauses_or]) :-
        member(Goal, Clause_or),
        call_goal(Goal),
        !,
        list_or_ok(LClauses_or).


call_goal(A) :-
        callable(A),
        !,
        intentional2:A.

call_goal([]) :-
        !.

call_goal([A|L]) :-
        intentional2:A,
        !,
        call_goal(L).

valid_interpretation(I) :-
        inserer_dans_base(I),
        base_ok,
        !,
        enlever_de_base(I).

valid_interpretation(I) :-
        enlever_de_base(I),
        fail.

interpretation_ok_for_false(I) :-
        inserer_dans_base(I),
        base_ok_for_false,
        !,
        enlever_de_base(I).

interpretation_ok_for_false(I) :-
        enlever_de_base(I),
        fail.

interpretation_ok_for_or(I) :-
        inserer_dans_base(I),
        base_ok_for_or,
        !,
        enlever_de_base(I).

interpretation_ok_for_or(I) :-
        enlever_de_base(I),
        fail.

/* ========================================================================== */
/*                                   HERBRAND BASE                            */
/* ========================================================================== */

creer_variables(0,[]):-
        !.

creer_variables(N,[_|Lv]):-
   N1 is N-1,
   creer_variables(N1,Lv).

creer_atome_libre(Atome):-
   predicates(LP),
   member((Predicat,Arite),LP),
   creer_variables(Arite,Lvariables),
   Atome=..[Predicat|Lvariables].

construire_atomes_libres(LAL):-
   findall(Atome, creer_atome_libre(Atome), LAL).

instancier_terme(A):-
      A=..[Pred|Larguments],
      instancier_liste(Larguments),
      A=..[Pred|Larguments].

instancier_liste([]).

instancier_liste([X|L]):-
      constants(LC),
      member(X,LC),
      instancier_liste(L).

atome_herbrand(A):-
          construire_atomes_libres(LA),
      member(A,LA),
      instancier_terme(A).

construire_base_Herbrand :-
      findall(A, atome_herbrand(A), LBH),
      asserta(base_Herbrand(LBH)).

/* ========================================================================== */
/*                                   MISCELLENAOUS                            */
/* ========================================================================== */

	/* convert each clausal hypothesis in a single conjunction */
clausal_to_conjunctive([], []) :-
   !.

clausal_to_conjunctive(
								[(Id, [(Head, Body), (Heada, Bodya)],Seed)|L],
								[(Id, [[Head|Body], [Heada|Bodya]], Seed)|L_out]
                      ) :-
   clausal_to_conjunctive(L, L_out).


	/* convert each conjunctive hypothesis in a clausal one */
conjunctive_to_clausal([], []) :-
   !.

conjunctive_to_clausal(
								[(Id, [[Head|Body], [Heada|Bodya]], Seed)|L],
								[(Id, [(Head,Body), (Heada,Bodya)], Seed)|L_out]
                      ) :-
   conjunctive_to_clausal(L, L_out).


        /* transforme clauses from lear syntax to prolog syntax
           and assert them into the intentional module */
lear_clauses_to_prolog([], []) :-
   !.

lear_clauses_to_prolog([Clause|LClauses], LHeads_out) :-
   one_lear_clause_to_prolog(Clause, LHead),
   lear_clauses_to_prolog(LClauses, LHeads),
   append(LHead, LHeads, LHeads_out).

one_lear_clause_to_prolog(<- Body, [falsity]) :-
   !,
   enumeration_to_commas(Body, Body1),
   intentional2:assert((falsity :- Body1)).


one_lear_clause_to_prolog(X or Head, [or(_)]) :-   % positive clause
             % positive clause : a1 or a2..
   !,
   enumeration_to_list(X or Head, LHead),
   intentional2:assert(or(LHead)).


one_lear_clause_to_prolog(X or Head <- Body, [falsity]) :-       % general clauses
   !,
   add_not(X or Head, LHead_not),
   enumeration_to_list(Body, LBody),
   append(LHead_not, LBody, LBody2),
   list_to_commas(LBody2, Body2),
   intentional2:assert(falsity :- Body2).

one_lear_clause_to_prolog(Atom <- Body, [Atom]) :-       % Horn clause
   !,
   enumeration_to_commas(Body, Body1),
   intentional2:assert(Atom :- Body1).

one_lear_clause_to_prolog(Atom, [Atom]) :-  % positive clause : a1 or a2..
   !,
   intentional2:assert(Atom).



   /* change the prolog formalism of a clause into the logical formalism */
translate_clauses([], []) :-
   !.

translate_clauses(
                  [Clause|LClauses],
                  [Clause_not|LClauses_not]
                 ) :-
   copy_term(Clause,Clause1),
   transform_one_clause(Clause1, Clause_not),
   translate_clauses(LClauses, LClauses_not).


transform_one_clause(Head <- Body, LClause) :-  % general clause
   !,
   enumeration_to_list(Head, LHead),
   add_not(Body, LBody),
   append(LHead, LBody, LClause).

transform_one_clause(<- Body, LBody) :-                   % negative clause
   !,
   add_not(Body, LBody).


transform_one_clause(Head, LHead) :-                      % positive clause
   enumeration_to_list(Head, LHead).


add_not(X=Y and Enum, [X\=Y|LEnum]) :-
   !,
   add_not(Enum, LEnum).

add_not(X=Y or Enum, [X\=Y|LEnum]) :-
   !,
   add_not(Enum, LEnum).


add_not(X\=Y and Enum, [X=Y|LEnum]) :-
   !,
   add_not(Enum, LEnum).

add_not(X\=Y or Enum, [X=Y|LEnum]) :-
   !,
   add_not(Enum, LEnum).


add_not(neg(X) and Enum, [X|LEnum]) :-
   !,
   add_not(Enum, LEnum).

add_not(X and Enum, [neg(X)|LEnum]) :-
   !,
   add_not(Enum, LEnum).

add_not(neg(X) or Enum, [X|LEnum]) :-
   !,
   add_not(Enum, LEnum).

add_not(X or Enum, [neg(X)|LEnum]) :-
   !,
   add_not(Enum, LEnum).

add_not(X\=Y, [X=Y]) :-
   !.

add_not(X=Y, [X\=Y]) :-
   !.

add_not(neg(X), [X]) :-
   !.

add_not(X, [neg(X)]).


enumerate_numbers(1, [1]) :-
   !.

enumerate_numbers(N, L) :-
   N1 is N - 1,
   enumerate_numbers(N1, L1),
   append(L1, [N], L).


/* ================================== SPLIT LITERALS ======================== */
/*     split one list of atoms in lists of atoms such that :
          - a variable is not in two or more lists
          - two variables of same type under oi are not in two or more lists
          - a variable and a constant of same type under oi are not in
            two or more lists
*/


make_split_literals([], []) :-
   !.

make_split_literals([Conj|LConj], [LParts_conj|LLParts_conj]) :-
   split_literals(Conj, LParts_conj),
   make_split_literals(LConj, LLParts_conj).



split_literals(L, LLout) :-
	create_sublists(L, LL),
	length(LL, N),
	merge_lists_sharing_arguments(N, LL, LLout).


	/* create a list with each element of the list L */
create_sublists([], []) :-
   !.

create_sublists([X|L], [[X]|LL]) :-
   create_sublists(L, LL).


   /* merge in a single lists all atoms in the lists of lists LL that share at
      least one argument */
merge_lists_sharing_arguments(1, LL, LL) :-
   !.

merge_lists_sharing_arguments(N, [L|LL], LLout) :-
   merge_two_lists(L, LL, LL1),
   N1 is N-1,
   merge_lists_sharing_arguments(N1, LL1, LLout).


   /* merge L with the first list of LL that contains atoms having arguments
      shared with atoms of L */
merge_two_lists(L, [], [L]) :-
      !.

merge_two_lists(L, [L1|LL], [L2|LL]) :-
  share_arguments(L, L1),
   !,
   append(L, L1, L2).

merge_two_lists(L, [L1|LL], [L1|LL2]) :-
   merge_two_lists(L, LL, LL2).


	/* check wether L1 and L2 have atoms that share arguments */
share_arguments(L1, L2) :-
	get_arguments_list_atoms(L1, LArgs1),
	get_arguments_list_atoms(L2, LArgs2),
     sort(LArgs1, LArgs_1),
     sort(LArgs2, LArgs_2),
	check_similar_arguments(LArgs_1, LArgs_2).


	/* get all arguments of atoms of the list L */
get_arguments_list_atoms([], []) :-
   !.

get_arguments_list_atoms([Atom|LAtoms], LArgs_types_out) :-
   Atom =..[Functor|LArgs],
   bk:pattern_types(Functor, LTypes),
   make_coples(LArgs, LTypes, LArgs_types),
   get_arguments_list_atoms(LAtoms, LArgs_types1),
   append(LArgs_types, LArgs_types1, LArgs_types_out).


   /* check whether L1 and L2 share argument of several natures */
check_similar_arguments(L1, L2) :-
   get_vars(L1, LVars1),
   get_vars(L2, LVars2),
   have_similar_element(LVars1, LVars2, strictly),
   !.

check_similar_arguments(L1, L2) :-
   have_common_type_oi(L1, L2).


   /* get the var in coples (Arg, Type) in L */
get_vars([], []) :-
   !.

get_vars([(Var,_Type)|LArgs], [Var|LVars]) :-
   var(Var),
   !,
   get_vars(LArgs, LVars).

get_vars([_|LArgs], LVars) :-
   get_vars(LArgs,LVars).


   /* check whether there is two args (Arg1, type_oi) in L1 and
      (Arg2, type_oi) in L2 wither at least Arg1 or Arg2 is a var */

have_common_type_oi([(Arg1, Type)|_], LArgs2) :-
   check_oi_mode(oi, Type),
   check_arg_type(Arg1, Type, LArgs2),
    !.

have_common_type_oi([_|LArgs1], LArgs2) :-
   have_common_type_oi(LArgs1, LArgs2).


   /* check whether there exist (Arg1, Type) in LArgs such that
      Arg or Arg1 is a variable */
check_arg_type(Arg, Type, [(Arg1, Type)|_]) :-
   one_var(Arg, Arg1),
   !.

check_arg_type(Arg, Type, [_|L]) :-
   check_arg_type(Arg, Type, L).


   /* return true whether Arg ou Arg1 is a variable */
one_var(Arg, _) :-
   var(Arg),
   !.

one_var(_, Arg) :-
   var(Arg).


/* ============================ FACTS HANDLING ============================== */

	/* compute the known and unknown facts of each intentional example */
compute_known_unknown_facts(_LIrrelevant, [], _LClauses_bkg, _LModes, []) :-
   !.

compute_known_unknown_facts(LIrrelevant, [(Ex_int, LDomains, Target)|LEx_int],
                            LClauses_bkg, LModes,
                      [ex(Known, Unknown, LDomains, Target)|LKnown_unknown]) :-
  compute_grounded_theory_complete(Ex_int, LDomains,
                                   LClauses_bkg, LModes, LIrrelevant,
                                   LClauses_negB, HB, LHead2),
  !,

  delete_non_facts(LClauses_negB, LFacts),
  get_positive_facts(LFacts, LPositive_facts),
  get_negative_facts(LFacts, LNegative_facts),

  append(LPositive_facts, LNegative_facts, Known),
  build_unknown_facts(HB, Known, Unknown),

  discard_clauses_intentional2(LHead2),
  compute_known_unknown_facts(LIrrelevant, LEx_int, LClauses_bkg,
                              LModes, LKnown_unknown).


compute_known_unknown_facts(LIrrelevant, [(Ex_int, LDomains, Target)|LEx_int],
                            LClauses_bkg, LModes, LKnown_unknown) :-
   writeln('!!! the following example is not consistent !!!'),
   writeln(Target),
   writeln(Ex_int),
   writeln(LDomains),
   compute_known_unknown_facts(LIrrelevant, LEx_int, LClauses_bkg,
                               LModes, LKnown_unknown).


	/* an atom a is unknow if neither a nor neg(a) is in Known */
build_unknown_facts([], _Known, []) :-
   !.

build_unknown_facts([Atom|LAtoms], Known, [Atom|Unknown]) :-
  \+ member(Atom, Known),
  \+ member(neg(Atom), Known),
  !,
  build_unknown_facts(LAtoms, Known, Unknown).

build_unknown_facts([_Atom|LAtoms], Known, Unknown) :-
  build_unknown_facts(LAtoms, Known, Unknown).


	/* filters the negative facts from a set of Facts */
get_negative_facts([], []) :-
   !.

get_negative_facts([Fact|LFacts], [Fact|LNegative_facts]) :-
   functor(Fact, neg, _),
   !,
   get_negative_facts(LFacts, LNegative_facts).

get_negative_facts([_Fact|LFacts], LNegative_facts) :-
   get_negative_facts(LFacts, LNegative_facts).


	/* filters the positive facts from a set of Facts) */
get_positive_facts([], []) :-
   !.

get_positive_facts([neg(_)|LFacts], LPositive_facts) :-
   !,
   get_positive_facts(LFacts, LPositive_facts).

get_positive_facts([Fact|LFacts], [Fact|LPositive_facts]) :-
   get_positive_facts(LFacts, LPositive_facts).


	/* delete clauses having more than one literal and gather
        remaining facts in a single list */
delete_non_facts([], []) :-
   !.

delete_non_facts([[Fact]|LClauses], [Fact|LClauses1]) :-
   !,
   delete_non_facts(LClauses, LClauses1).

delete_non_facts([_Clause|LClauses], LClauses1) :-
   delete_non_facts(LClauses, LClauses1).


/* ============================== MISCELLENAOUS ============================= */

        /* add an extra table containing the target concept to each
           extensional examples */
deal_with_targets([], LExp, LExp) :-    % examples are not clauses
   !.

deal_with_targets(LTarget, LExp, LExp_out) :-
   add_target(LTarget, LExp, LExp_out).


add_target([], [], []) :-
   !.

add_target([Target|LTarget], [Exp|LExp], [(Target, Exp)|LExp1]) :-
   add_target(LTarget, LExp, LExp1).


/* each example is represented as a pair min_max(Ex_min, Ex_max) where
  Ex_min is a set of interpretations and Ex_max is a graph).
  this predicate translate a set of tables in a set of interpretations */
build_interpretations([], []) :-
   writeln('termine !!!!!'),
   !.

build_interpretations(
                       [min_max(Tables_min, Graph_max)|LEx],
                       [min_max(Inter_min, Graph_max)|LEx1]
                      ) :-
   compute_interpretations(Tables_min, Inter_min),
   build_interpretations(LEx, LEx1).


	/* compute all interpretations of the ambiguous example Exp
           expressed as a cross-product of tables */
compute_interpretations(Exp, LInterpretations) :-
   cross_product_lists_of_lists(Exp, LInterpretations).


discard_args_plus([], []) :-
   !.

discard_args_plus([+_X|L], [plus|L1]) :-
   !,
   discard_args_plus(L, L1).

discard_args_plus([_X|L], [none|L1]) :-
   discard_args_plus(L, L1).


get_learn_mode(Mode) :-
   learn:learn_mode(Mode).

set_learn_mode(Mode) :-
   retract_learn_mode,
   learn:assert(learn_mode(Mode)).

retract_learn_mode :-
   learn:retract(learn_mode(_)),
   !.

retract_learn_mode.

/* ============================= FIN DU LISTING ============================= */

