%% Copyright (C) 2005 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
%% 

% topbase, bottombase : Base
% base : Liste(Vlva) -> Base
% 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(Base) x -Base
combine_e(X, D, Liste_Bases, Base) :-
	(
	  all_topbase_or_bottombase(Liste_Bases)
	->
	  combine_e_cas_de_base(Liste_Bases, Facteurs_Base_X),
	  (
	    Facteurs_Base_X = []
	  ->
	    Base = bottombase
	  ;
	    Base = base([vlva(X, D, Facteurs_Base_X)])
	  )
	;
	  extract_premiere(Liste_Bases, Facteurs_Base_X),
	  combine(Liste_Bases, X, Elements_Base),
	  Base = base([vlva(X, D, Facteurs_Base_X) | Elements_Base])
	).

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

combine_a(_X, Liste_Bases, topbase) :-
	all_topbase(Liste_Bases), !.
combine_a(X, Liste_Bases, base(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(Base) x -Liste(Va)
extract_premiere([], []).

extract_premiere([(Valeur, base(_)) | 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(Base) x +Liste(Val) x ?Var x -Base

combine([], _X, []).
combine(Liste_Bases, X, [vlva(Y, D_Y, Liste_Va_Y) | Reste_Base]) :-
	Liste_Bases = [(_, base([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).

%% croise_arbre_de_contraintes : +Liste(Base) x Liste(Val) x ?Var x ?Var x -Liste(Base) x Liste(Va)

% 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(Base) x -Liste(Liste(Va)) x -Liste(Base)
decompose_liste_bl_selon_premiere_variable(_, [], [], []).

decompose_liste_bl_selon_premiere_variable(Var, [(Val, base([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, base(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_topbase([]).
all_topbase([topbase | All_Topbase]) :- all_topbase(All_Topbase).


all_topbase_or_bottombase([]).
all_topbase_or_bottombase([Base | All_topbase_or_bottombase]) :-
	(Base = (_, topbase) ; Base = (_, bottombase)),
	all_topbase_or_bottombase(All_topbase_or_bottombase).


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_base(base(Facteurs_A), base(Facteurs_B)) :-
	equivalente_base(Facteurs_A, Facteurs_B).

equivalente_base([], []).
equivalente_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_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_).