/* ========================================================================== */
/*                          HANDLE COMPATIBILITY RELATIONS                    */
/* ========================================================================== */
/* - better implementation of the subsumtion between clauses                  */
/*   (21/11/12)                                                               */
/* - new implementation of the compatibility+ relations                       */
/*   where positive examples are represented as graphs                        */
/*   (4/10/12)                                                                */
/* ========================================================================== */

:- module(
          compatibility5,
          [
            covered_pos/4,
            compatible_neg/5,
            compatible_pos/3,
            compatible_pos_rules/3,
            compatible_neg_rules/4
          ]
          ).

:-
   getenv('LEAR_DIR', Lear),
   atom_concat(Lear, '/list.pl', List),
   use_module(List),
   atom_concat(Lear, '/domains.pl', Domains),
   use_module(Domains),
   atom_concat(Lear, '/assumptions2.pl', Assumptions),
   use_module(Assumptions),
   atom_concat(Lear, '/manage_examples2.pl', Manage),
   use_module(Manage),
   atom_concat(Lear, '/miscellaneous.pl', Misc),
   use_module(Misc),
   atom_concat(Lear, '/term.pl', Term),
   use_module(Term).


/* ========================== Strict coverage =============================== */

	% chewk whether Hyp covers all possibilities
covered_pos(Hyp, Num, Head, LPossibilities) :-
   \+ compatible_neg(pos, Hyp, Num, Head, LPossibilities). 

/* =============== Compatibility with positive ambiguous examples =========== */

	/* check whether a set of rules is compatible+ with a positive
      ambiguous example. This means that at least a rule is compatible+ 
      with the example */
compatible_pos_rules([], _Graph, _Tab) :-
        !,
        fail.

compatible_pos_rules([
                       rule(
                             (
                               (_Id, [Hyp, _Hypa], _Seed), 
                               _Guidance, _Quality, _Errors, _PC
                             ), 
                             _Npos, _Nneg
                            )
                     |_LConjs], 
					(Num, Head, min_max(_,Graph)), 
					Tab) :-
        compatible_pos(Hyp, (Num, Head, Graph), Tab),
        !.

compatible_pos_rules([_Conj|LConjs], Graph, Tab) :-
        compatible_pos_rules(LConjs, Graph, Tab).


   /* check whether Hyp (a rule) is compatible+ with a positive ambiguous
      example. This means that the clause Hyp theta-subsumes one of the
      clauses of the example 
   */
compatible_pos(
               Hyp,                          % A clause Head :- Body
                                             % representing an hypothesis.
               (Num, Head_ex, Graph),
               (Num, Tab)                    % a positive ambiguous example
               ) :-
     get_domains(Num, pos, LDomains),        % get domains of types used in ex
     split_oi_domains(LDomains, _, LDomains_oi),
	 copy_term(Hyp, Hyp1),
     Hyp1 = (Head_hyp,Body_hyp),
     Conj = [Head_hyp|Body_hyp],
     update_values_domains(Conj, LDomains_oi, LDomains_oiA),
     convert_atoms_types(Conj, Hyp_types),
     bk:sets_vars_under_oi(LVars_oi),  
     get_sets_vars(oi, Conj, Hyp_types, LVars_oi, LTypes_vars),
			                % LTypes_vars contains the variables associated 
                         % with each oi type.
	 subsumes_head(Head_hyp, Head_ex, LTypes_vars, LDomains_oiA,
                   LTypes_vars1, LDomains_oi1),
     rank_atoms(Body_hyp, Body_hyp1),
     has_model(Body_hyp1, LTypes_vars1, LDomains_oi1, Graph, Tab).


    /* check if Conj has a model considering all the tables */
has_model([], _LTypes_vars, _LDomains_oi, _Graph, _Tab) :-                                               
   !.

has_model([Atom|LAtom], LTypes_vars, LDomains_oi, Graph, Tab) :-
   variabilize_atom(Atom, Atom1),             % to avoid instantiate Graph
   member((Atom1, LInstances), Graph),
   has_instance(Atom, LInstances, 
                Tab,  LTypes_vars,  LDomains_oi, 
                Tab1, LTypes_vars1, LDomains_oi1),    
   has_model(LAtom, LTypes_vars1, LDomains_oi1, Graph, Tab1).

 
	/* check whether Atom has a valid instance in LInstances */
has_instance(Atom, LInstances, 
             Tab,  LTypes_vars,  LDomains_oi, 
             Tab1, LTypes_vars1, LDomains_oi1) :-
   member((Atom, Num_tab, LPossibilities), LInstances), 
   check_possibilities(Num_tab, LPossibilities, Tab, Tab1),
   check_oi(Atom, LTypes_vars, LDomains_oi, LTypes_vars1, LDomains_oi1).


check_possibilities(Num_tab,   LPossibilities, Tab, 
                    [(Num_tab, LPossibilities_tab1)|Tab1]) :-
   select((Num_tab, LPossibilities_tab), Tab, Tab1),
   intersection(LPossibilities, LPossibilities_tab, LPossibilities_tab1),
   LPossibilities_tab1 \== [].
   

/* =============== compatibility with negative ambiguous examples =========== */

	/* check whether the current hypothesis is compatible with a negative
        ambiguous example */
compatible_neg_rules([], _Num, _Head_exp, _LAssumptions) :-
        !.

compatible_neg_rules([rule(
                             (
                               (_Id, [Hyp, _Hypa], _Seed), 
                               _Guidance, _Quality, _Errors, _PC
                             ), 
                             _Npos, _Nneg
                            )
                     |Rules], Num, 
                     Head_exp, LAssumptions) :-
        compatible_neg(neg, Hyp, Num, Head_exp, LAssumptions),
        update_negative_one_example(Num, Hyp, Head_exp, LAssumptions),
        compatible_neg_rules(Rules, Num, Head_exp, LAssumptions).


	/* check whether Hyp is compatible- with the negative example represented
      by Head_neg and LAssumptions. This means that there exists an 
      interpretation I in LAssumptions such that 
      Head_hyp <- Body_hyp does not theta subsume Head_neg <- I */ 
compatible_neg(Signe, Hyp, Num, Head_neg, LAssumptions) :-

     get_domains(Num, Signe, LDomains),    % get domains of types used in ex
     split_oi_domains(LDomains, _LDomains_not_oi, LDomains_oi),

     copy_term(Hyp, Hyp1),
     Hyp1 = (Head_hyp,Body_hyp),
     Conj = [Head_hyp|Body_hyp],

     update_values_domains(Conj, LDomains_oi, LDomains_oi1),
     convert_atoms_types(Conj, Hyp_types),
     bk:sets_vars_under_oi(LVars_oi),  
     get_sets_vars(oi, Conj, Hyp_types, LVars_oi, LTypes_vars_oi),
			                % LTypes_vars contains the variables associated 
                               % with each oi type.
     subsumes_head(Head_hyp, Head_neg, LTypes_vars_oi,  LDomains_oi1,
                                       LTypes_vars_oi2, LDomains_oi2),
     !,
     split_ground_atoms(Body_hyp, Body_hyp_ground, Body_hyp_no_ground),
     no_subsumption(LAssumptions, Body_hyp_ground, Body_hyp_no_ground, 
                    LTypes_vars_oi2, LDomains_oi2).

	% Head_hyp does not subsume Head_neg, so there is compatibility-
compatible_neg(_Signe, _Hyp, _Num, _Head_neg, _LAssumptions).


	/* check whether there exists an interpretation I in LAssumptions 
      such that Body_hyp does not theta subsume I */ 

   % each interpretation in LAssumptions is theta subsumed 
   % by the body of the hypothesis 
   % (or the current negative example has no longer valid assumption,
   %  due to noise)
no_subsumption([], _Body_hyp_ground, _Body_hyp_no_ground, 
            _LTypes_vars, _LDomains_oi) :-
   !,
   fail.
	
	% the ground atoms of Hyp do not subsume I => no subsumption ok
no_subsumption([I|_LAssumptions], Body_hyp_ground, _Body_hyp_no_ground, 
               _LTypes_vars, _LDomains_oi) :-
     \+ subsume_ground_atoms(Body_hyp_ground, I),
     !.

	% the ground atoms of Hyp subsume I. We check the subsumption of the 
     % non ground atoms of Hyp
no_subsumption([I|_LAssumptions], _Body_hyp_ground, Body_hyp_no_ground, 
               LTypes_vars_oi, LDomains_oi) :-
     rank_atoms(Body_hyp_no_ground, Body_hyp_no_ground1),
     \+ subsumes_body(Body_hyp_no_ground1, I, LTypes_vars_oi, LDomains_oi),     
     !.

	% One tries another possibility of the example
no_subsumption([_|LAssumptions], Body_hyp_ground, Body_hyp_no_ground, 
               LTypes_vars_oi, LDomains_oi) :-
   no_subsumption(LAssumptions, Body_hyp_ground, Body_hyp_no_ground, 
                  LTypes_vars_oi, LDomains_oi).


/* ============================= SUBSUMPTION ================================ */

	/* check if Head_hyp theta-subsumes Head_ex */
subsumes_head(
			Head_hyp, 
			Head_ex, 
			LTypes_vars_oi, 
			LDomains_oi,
               LTypes_vars_oi1, 
			LDomains_oi1
             ) :-

   Head_hyp = Head_ex,         % we instantiate Head_hyp from Head_neg
                               % some vars of LTypes_vars have been instantiated

   check_oi(Head_hyp, LTypes_vars_oi, LDomains_oi,
                      LTypes_vars_oi1, LDomains_oi1).


	/* check if Body_hyp theta-subsume Body_exp */
	/* check if Head_hyp theta-subsume Head_ex */

subsumes_body(Body_hyp, Body_ex, _LTypes_vars_oi, _LDomains_oi) :-
   \+ my_subset(Body_hyp, Body_ex),            % Body_hyp cannot subsumes Body_ex
   !,
   fail.

subsumes_body(Body_hyp, Body_ex, LTypes_vars_oi, LDomains_oi) :-
   subsumes_the_body(Body_hyp, Body_ex, LTypes_vars_oi, LDomains_oi).


subsumes_the_body([], _Body_exp, _LTypes_vars_oi, _LDomains_oi) :-
   !.

subsumes_the_body(
			[Atom|Body_hyp], 
			Body_ex,
			LTypes_vars_oi, 	 % [type1(LVariables1), ...]
			LDomains_oi          % [type1(LValeurs1), ..]
             ) :-

   copy_term(Atom, Atom1),     % keep trace of original atom
   member(Atom, Body_ex),      % Atom unifies with an element of Body_ex
   check_oi(Atom, LTypes_vars_oi, LDomains_oi,
                  LTypes_vars_oi1, LDomains_oi1),  
   check_rank_atoms(Atom1, Atom, Body_hyp, Body_hyp1), 
   subsumes_the_body(Body_hyp1, Body_ex, LTypes_vars_oi1, LDomains_oi1).  


	/* check if the ground body part is a subset of Body ex */
subsume_ground_atoms(Body_ground, Body_ex) :-
   sort(Body_ground, Body_ground1),            % do discard doublets
   sort(Body_ex, Body_ex1),                    % to reorder atoms in order to
                                               % gain efficiency
   my_subset(Body_ground1, Body_ex1).                          
 

/* =========================== CHECK CONSTRAINT OI ========================== */

   	/* check whether instantiations have respected OI constraints */

check_oi(Atom, LTypes_vars, LDomains_oi, LTypes_vars1, LDomains_oi1) :-
   convert_atoms_types([Atom], [Atom_types]),
   Atom_types=..[_Functor|LTypes], 
   sort(LTypes, LTypes1),
   check_oi_instantiations(LTypes1, LTypes_vars,  LDomains_oi,
                                    LTypes_vars1, LDomains_oi1).

  
	/* check whether the instantiated variables meet OI constraints */
check_oi_instantiations([], LTypes_vars, LDomains_oi, 
                            LTypes_vars, LDomains_oi) :-
   !.

check_oi_instantiations(
                        [Type|LTypes], 
                        LTypes_vars, 
                        LDomains_oi, 
                        [Type_vars1|LTypes_vars1], 
                        [Type_values1|LDomains_oi1]
                       ) :-

   functor(Type_vars, Type, 1),        
  
   select(Type_vars, LTypes_vars, 
                     LTypes_vars2),    % example has variables of type Type
   !,   

   arg(1, Type_vars, LVars),	         % LVars contains the variables
                                       % (some be unified with constants) 
                                       % associated with the type Type                              
     
   delete_vars(LVars, LVars2),
   is_set(LVars2),                     % unified variables meet OI constraints

   functor(Type_values, Type, 1),
   select(Type_values, LDomains_oi,
                       LDomains_oi2),  
   !,
   arg(1, Type_values, LValues),	    % LValues contains the authorized
                                       % values for the type Type
   my_subset(LVars2, LValues),         % unified variables are in the 
							    % set of authorized values
   
   delete_constants(LVars, LVars1),
   Type_vars1 =..[Type|[LVars1]],      % update list of vars associated with
                                       % the type Type
   
   subtract(LValues, LVars2, LValues1),
   Type_values1 =..[Type|[LValues1]],      
                                       % update list of authorized values 
                                       % associated with the type Type
   	       
   check_oi_instantiations(LTypes, LTypes_vars2, LDomains_oi2,
                                   LTypes_vars1, LDomains_oi1).

							   % Type is not involved
check_oi_instantiations([_Type|LTypes], LTypes_vars,  LDomains_oi, 
                                        LTypes_vars1, LDomains_oi1) :-
	check_oi_instantiations(LTypes, LTypes_vars, LDomains_oi, 
                                     LTypes_vars1, LDomains_oi1).
   
  
/* ============================== MISCELLEANEOUS ============================ */

	/* check whether Atom is an instance of Atom1 (it has less variables), 
       and in consequence rank atoms of Body_hyp */
check_rank_atoms(Atom1, Atom, Body_hyp, Body_hyp1) :-
     copy_term(Atom1, AtomA),
     numbervars(AtomA, 0, NumberA),
     copy_term(Atom, AtomB),
     numbervars(AtomB, 0, NumberB),
     NumberB < NumberA,              % Atom1 has been instantied in Atom
     !,
     rank_atoms(Body_hyp, Body_hyp1).

check_rank_atoms(_Atom1, _Atom, Body_hyp, Body_hyp).


	/* rank the atoms of LAtoms according to the number of their variables */
rank_atoms([], []) :-
   !.

rank_atoms(LAtoms, LAtoms_out) :-
   compute_nb_variables(LAtoms, LNumbers),
   rank_atoms_vars(LAtoms, LNumbers, [], [], LAtoms_out).

	/* rank the atoms of LAtoms according to their numbers of variables in
        LNumbers */
rank_atoms_vars([], [], LAtoms, _LNumbers, LAtoms) :-
   !.

rank_atoms_vars(
                [Atom|LAtoms], [Number|LNumbers], 
                LAtoms1, LNumbers1,
                LAtoms_out
               ) :-
   insert_atom_number(Atom, Number, LAtoms1, LNumbers1, LAtoms2, LNumbers2),
   rank_atoms_vars(LAtoms, LNumbers, LAtoms2, LNumbers2, 
                   LAtoms_out).

	/* insert Number in its right place ascending sorted list LNumbers,
        and Atom at the same place in LAtoms */

insert_atom_number(Atom, Number, [], [], [Atom], [Number]) :-
   !.

insert_atom_number(Atom, Number, [Atom1|LAtoms1], [Number1|LNumbers1], 
                  [Atom,Atom1|LAtoms1], [Number,Number1|LNumbers1]) :-
   Number =< Number1,
   !.

insert_atom_number(Atom, Number, [Atom1|LAtoms1], [Number1|LNumbers1], 
                  [Atom1|LAtoms2], [Number1|LNumbers2]) :-
   insert_atom_number(Atom, Number, LAtoms1, LNumbers1, LAtoms2, LNumbers2).
  
   
	/* compute the number of variables in each atom of LAtoms */
compute_nb_variables([], []) :-
   !.

compute_nb_variables([Atom|LAtoms], [Number|LNumbers]) :-
   copy_term(Atom, Atom1),
   numbervars(Atom1, 0, Number),
   compute_nb_variables(LAtoms, LNumbers).


	/* discard constants that have been in list of atoms LAtoms */
discard_constants_atoms([], []) :-
   !.

discard_constants_atoms([Atom|LAtoms], [Atom1|LAtoms1]) :-
   Atom=..[Functor|[L]],
   delete_constants(L, L1),   % keep only variables
   Atom1=..[Functor|[L1]],
   discard_constants_atoms(LAtoms, LAtoms1).  

	/* discard of Conj all ground terms that are in Possibility */
 discard_ground_terms([], _Possibility, []) :-
    !.

discard_ground_terms([Term|Conj], Possibility, Conj_out) :-
   ground(Term),
   member(Term, Possibility),
   !,
   discard_ground_terms(Conj, Possibility, Conj_out).


discard_ground_terms([Term|Conj], Possibility, [Term|Conj_out]) :-
   discard_ground_terms(Conj, Possibility, Conj_out).

/* =========================== END OF LISTING =============================== */
