%% Copyright (C) 2012 Igor Stéphan
%% 
%% This program is free software; you can redistribute it and/or
%% modify it under the terms of the GNU General Public License
%% as published by the Free Software Foundation; either version 2
%% of the License, or (at your option) any later version.
%% 
%% This program is distributed in the hope that it will be useful,
%% but WITHOUT ANY WARRANTY; without even the implied warranty of
%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
%% GNU General Public License for more details.
%% 
%% You should have received a copy of the GNU General Public License
%% along with this program; if not, write to the Free Software
%% Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
%% http:%%www.gnu.org/copyleft/gpl.html
%%
%% igor.stephan@univ-angers.fr
%% 
:- module('QCSP_BASE', [combine_e/4, combine_a/3, equivalente_qcsp_base/2]).
:- use_module(library(lists)).
:- use_module(library(clpfd)).

% bltop, blbottom : Bl
% bl : Liste(Vlva) -> Bl
% vlva : Var x Liste(Val) x Liste(Va) -> Vlva
% va : Val x Arbre_Etiquete -> Va
% (_,_) : Val x Arbre_Etiquete
% top, bottom : Arbre_Etiquete 
 

%% combine_e : ?Var x +Liste(Val) x +Liste(Bl) x -Bl
combine_e(X, D, Liste_Bases, Base) :-
	(
	  all_bltop_or_blbottom(Liste_Bases)
	->
	  combine_e_cas_de_base(Liste_Bases, Facteurs_Base_X),
	  (
	    Facteurs_Base_X = []
	  ->
	    Base = blbottom
	  ;
	    Base = bl([vlva(X, D, Facteurs_Base_X)])
	  )
	;
	  extract_premiere(Liste_Bases, Facteurs_Base_X),
	  combine(Liste_Bases, X, Elements_Base),
	  Base = bl([vlva(X, D, Facteurs_Base_X) | Elements_Base])
	).

%% combine_e_cas_de_base : +Liste(Val) x +Liste(Bl) x -Liste(Va)
combine_e_cas_de_base([], []).
combine_e_cas_de_base([(Val, bltop) | Bases], [va(Val) | Facteurs]) :-
	combine_e_cas_de_base(Bases, Facteurs).

combine_a(_X, Liste_Bases, bltop) :-
	all_bltop(Liste_Bases), !.
combine_a(X, Liste_Bases, bl(Base)) :-
	combine(Liste_Bases, X, Base).

% Le prédicat extract_premiere extrait la liste des couples Valeur-Arbre_De_Contraintes, pour chaque élément du Domaine, des Sous_Bases pour la nouvelle variable introduite dans la base
%% extract_premiere : +Liste(Val) x +Liste(Bl) x -Liste(Va)
extract_premiere([], []).
extract_premiere([(Valeur, bl(_)) | Bases], [va(Valeur) | Liste_Couple_Valeur_Arbre_De_Contraintes]) :-
	extract_premiere(Bases, Liste_Couple_Valeur_Arbre_De_Contraintes).


% Le prédicat combine construit une nouvelle base à partir de la combinaison d'une liste de bases.
%% combine : +Liste(Bl) x +Liste(Val) x ?Var x -Bl

combine([], _X, []).
combine(Liste_Bases, X, [vlva(Y, D_Y, Liste_Va_Y) | Reste_Base]) :-
	Liste_Bases = [(_, bl([vlva(Y, D_Y, _) | _])) | _],
	decompose_liste_bl_selon_premiere_variable(Y, Liste_Bases, Liste_Va, Liste_Sous_Bases),
	construit_liste_couples_valeur_arbre_de_contraintes(Liste_Va, X, Liste_Va_Y),
	combine(Liste_Sous_Bases, X, Reste_Base).


% Le prédicat construit_liste_couples_valeur_arbre_de_contraintes pour chaque Valeur du Domaine croise les  
%% construit_liste_couples_valeur_arbre_de_contraintes:
% Liste_couples_valeur_arbre_de_contraintes:+Liste(Liste(Va)) x Domaine:+Liste(Val) x ?Var x -Liste(Va)
construit_liste_couples_valeur_arbre_de_contraintes(Liste_Couples_Valeur_Arbre_De_Contraintes, _, []) :-
	construction_terminee(Liste_Couples_Valeur_Arbre_De_Contraintes), !.
construit_liste_couples_valeur_arbre_de_contraintes(Liste_Couples_Valeur_Arbre_De_Contraintes, X, [va(Val, Arbre) | Liste_Va]) :-
	extrait_pour_Val_les_arbres_de_contraintes(Liste_Couples_Valeur_Arbre_De_Contraintes, Premiere_Liste_Arbre, Autres_Listes_Va, Val),
	Arbre =.. [ab, X | Premiere_Liste_Arbre],
	construit_liste_couples_valeur_arbre_de_contraintes(Autres_Listes_Va, X, Liste_Va).

%% Le prédicat extrait_pour_Val_les_arbres_de_contraintes extrait de la liste de liste des couples valeur-arbre de contraintes les arbres de contraintes pour la valeur Val 
%% extrait_pour_Val_les_arbres_de_contraintes : +Liste(Val) x +Liste(Liste(Va)) x -Liste(Arbre_De_Contraintes) x -Liste(Liste(Va)) x -Val
extrait_pour_Val_les_arbres_de_contraintes([], [], [], _Val). 

extrait_pour_Val_les_arbres_de_contraintes([(Val_Croisement, Liste_Va_In) | Liste_Liste_Va_In], [(Val_Croisement, A) | Liste_Arbre_De_Contraintes], [(Val_Croisement, Liste_Va_Out) | Liste_Liste_Va_Out], Val) :-
	selectionne(Liste_Va_In, va(Val, A), Liste_Va_Out),
	!,
	extrait_pour_Val_les_arbres_de_contraintes(Liste_Liste_Va_In, Liste_Arbre_De_Contraintes, Liste_Liste_Va_Out, Val).


extrait_pour_Val_les_arbres_de_contraintes([(Val_Croisement, Liste_Va_In) | Liste_Liste_Va_In], [Val_Croisement | Liste_Arbre_De_Contraintes], [(Val_Croisement, Liste_Va_Out) | Liste_Liste_Va_Out], Val) :-
	selectionne(Liste_Va_In, va(Val), Liste_Va_Out),
	!,
	extrait_pour_Val_les_arbres_de_contraintes(Liste_Liste_Va_In, Liste_Arbre_De_Contraintes, Liste_Liste_Va_Out, Val).

extrait_pour_Val_les_arbres_de_contraintes([Liste_Va_In | Liste_Liste_Va_In], Liste_Arbre_De_Contraintes, [Liste_Va_In | Liste_Liste_Va_Out], Val) :-
	extrait_pour_Val_les_arbres_de_contraintes(Liste_Liste_Va_In, Liste_Arbre_De_Contraintes, Liste_Liste_Va_Out, Val).


%% decompose_liste_bl_selon_premiere_variable : ?Var x +Liste(Bl) x -Liste(Liste(Va)) x -Liste(Bl)
decompose_liste_bl_selon_premiere_variable(_, [], [], []).
decompose_liste_bl_selon_premiere_variable(Var, [(Val, bl([vlva(Var_, _D, Liste_Va) | Sous_Base])) | Liste_Bases], [(Val,Liste_Va) | Liste_Val_Liste_Va], Liste_Sous_Bases) :-
	Var == Var_, % Simple vérification : le paramètre Var est inutile
	decompose_liste_bl_selon_premiere_variable(Var, Liste_Bases, Liste_Val_Liste_Va, Liste_Sous_Bases_),
	(
	  Sous_Base = []
	->
	  Liste_Sous_Bases =  Liste_Sous_Bases_
	;
	  Liste_Sous_Bases =  [(Val, bl(Sous_Base)) | Liste_Sous_Bases_]
	).
	  

insere([], _Val, []).
insere([va(Val_, A) | Liste_Va], Val, [va(Val_, A, Val) | Liste_Va_Val]) :-
	insere(Liste_Va, Val, Liste_Va_Val).
insere([va(Val_) | Liste_Va], Val, [va(Val_, Val) | Liste_Va_Val]) :-
	insere(Liste_Va, Val, Liste_Va_Val).

all_bltop([]).
all_bltop([bltop | All_BlTop]) :- all_bltop(All_BlTop).


all_bltop_or_blbottom([]).
all_bltop_or_blbottom([Bl | All_bltop_or_blbottom]) :-
	(Bl = (_, bltop) ; Bl = (_, blbottom)),
	all_bltop_or_blbottom(All_bltop_or_blbottom).


in_all_va(D, Liste_Va) :-
	in_all_va(D, [], Liste_Va).

in_all_va([], [], []).
in_all_va([Val | D], Liste_Va_, [va(Val) | Liste_Va__]) :-
	!,
	append(Liste_Va_, Liste_Va__, Liste_Va),
	in_all_va(D, [], Liste_Va).
in_all_va([Val | D], Liste_Va_, [va(Val, _) | Liste_Va__]) :-
	!,
	append(Liste_Va_, Liste_Va__, Liste_Va),
	in_all_va(D, [], Liste_Va).
in_all_va(D, Liste_Va_, [Va | Liste_Va__]) :-
	in_all_va(D, [Va | Liste_Va_], Liste_Va__).


selectionne([X | L1], X, L1) :- !.
selectionne([X | L1], Y, [X | L2]) :-
	selectionne(L1, Y, L2).

construction_terminee([]).
construction_terminee([(_,[]) | L]) :-
	construction_terminee(L).

%%% Equivalence entre Base de Litteraux QCSP
equivalente_qcsp_base(bl(Facteurs_A), bl(Facteurs_B)) :-
	equivalente_qcsp_base(Facteurs_A, Facteurs_B).

equivalente_qcsp_base([], []).
equivalente_qcsp_base([vlva(X_A, D, LVa_A) | Facteurs_A], [vlva(X_B, D, LVa_B) | Facteurs_B]) :-
	X_A == X_B,
	equivalente_lva(LVa_A, LVa_B),
	equivalente_qcsp_base(Facteurs_A, Facteurs_B).

equivalente_lva([], []).
equivalente_lva([va(Val) | LVa_A], LVa_B) :-
	delete(LVa_B, va(Val), LVa_B_),
	equivalente_lva(LVa_A, LVa_B_).
equivalente_lva([va(Val, Arbre_A) | LVa_A], LVa_B) :-
	suppression(LVa_B, va(Val, Arbre_B), LVa_B_),
	equivalente_tree(Arbre_A, Arbre_B),
	equivalente_lva(LVa_A, LVa_B_).

suppression([X|L],X,L) :- !.
suppression([Y|L],X,[Y|L_]) :- 
   suppression(L,X,L_).

equivalente_tree(Feuille, Feuille) :-
	atomic(Feuille),
	!.
equivalente_tree(Arbre_A, Arbre_B) :-
	compound(Arbre_A),
	compound(Arbre_B),
	Arbre_A =.. [ab, V_A | Args_A],
	Arbre_B =.. [ab, V_B | Args_B],
	V_A == V_B,
	map_equivalente_tree(Args_A, Args_B).

map_equivalente_tree([], []).
map_equivalente_tree([Val | Vals_A], Vals_B) :-
	atomic(Val),
	suppression(Vals_B, Val, Vals_B_),
	map_equivalente_tree(Vals_A, Vals_B_).
map_equivalente_tree([(Val, Sous_Arbre_A) | Arbres_A], Arbres_B) :-
	suppression(Arbres_B, (Val, Sous_Arbre_B), Arbres_B_),
	equivalente_tree(Sous_Arbre_A, Sous_Arbre_B),
	map_equivalente_tree(Arbres_A, Arbres_B_).