%% 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('ITERATIVE_CONSTRUCTION', [empty_bl/2,insert_bl_from_stock/3]).
:- use_module(library(lists)).
:- use_module(library(clpfd)).


% Le mode elimination ote du stock les branches qui correspondent à des varaibles n'appartenant pas au premier bloc d'existentielles.
% Le mode non_elimination conserve dans le stock les branches qui correspondent à des variables appartenant au premier bloc d'existentielles.


empty_bl([], []).
empty_bl([e(X, D_X) | Quant], [vlva(X, D_X, []) | Vlva]) :-
	empty_bl(Quant, Vlva).
empty_bl([a(_X, _D_X) | Quant], Vlva) :-
	empty_bl(Quant, Vlva).


insert_bl_from_stock([], Facteurs, Facteurs).
insert_bl_from_stock([Branche | Stock], Facteurs_In, Facteurs_Out) :-
	reverse(Branche, Branche_),
	insere_dans_chaque_vlva(Branche_, [], Facteurs_In, Facteurs),
	insert_bl_from_stock(Stock, Facteurs, Facteurs_Out).

insere_dans_chaque_vlva([], _, Facteurs, Facteurs).
% X est une existentielle
insere_dans_chaque_vlva([(X, Val_X) | Branche], Insert, [vlva(Z, D_X, Liste_Va_In) | Facteurs_In], [vlva(X, D_X, Liste_Va_Out) | Facteurs_Out]) :-
	X == Z,!,
	insere_val_branches(Val_X, Insert, Liste_Va_In, Liste_Va_Out),
	append(Insert, [(X, Val_X)], Insert_),
	insere_dans_chaque_vlva(Branche, Insert_, Facteurs_In, Facteurs_Out).
% X est une universelle
insere_dans_chaque_vlva([(X, Val_X) | Branche], Insert, Facteurs_In, Facteurs_Out) :-
	append(Insert, [(X, Val_X)], Insert_),
	insere_dans_chaque_vlva(Branche, Insert_, Facteurs_In, Facteurs_Out).



insere_val_branches(Val, [], Liste_Va_In, Liste_Va_Out) :-
	insere_liste_va_branche_vide(Val, Liste_Va_In, Liste_Va_Out).
insere_val_branches(Val, Branche, Liste_Va_In, Liste_Va_Out) :-
	Branche = [_ | _],
	insere_liste_va_branche(Val, Branche, Liste_Va_In, Liste_Va_Out).

insere_liste_va_branche_vide(Val, [], [va(Val)]).
insere_liste_va_branche_vide(Val, [va(Val) | Liste_Va], [va(Val) | Liste_Va]) :-
	!.
insere_liste_va_branche_vide(Val, [va(Val_) | Liste_Va], [va(Val_) | Liste_Va_]) :-
	insere_liste_va_branche_vide(Val, Liste_Va, Liste_Va_).

insere_liste_va_branche(Val, Branche, [], [va(Val, Arbre)]) :-
	insere_branche(Branche, abvide, Arbre).
insere_liste_va_branche(Val, Branche, [va(Val, Arbre_In) | Liste_Va], [va(Val, Arbre_Out) | Liste_Va]) :-
	!,
	insere_branche(Branche, Arbre_In, Arbre_Out).
insere_liste_va_branche(Val, Branche, [va(Val_, Arbre_) | Liste_Va_In], [va(Val_, Arbre_) | Liste_Va_Out]) :-
	insere_liste_va_branche(Val, Branche, Liste_Va_In, Liste_Va_Out).

insere_branche([(X, Val)], Arbre, Arbre_) :-
	Arbre =.. [ab, Y | Feuilles],
	X == Y,
	(
	  member(Val, Feuilles)
	->
	  Arbre_ = Arbre
	;
	  Arbre_ =.. [ab, X, Val | Feuilles]
	).
insere_branche([(X, Val) | Branche], Arbre_In, Arbre_Out) :-
	Arbre_In =.. [ab, Y | Sous_Arbres],
	X == Y,
	selectionne_sous_arbre(Val, Sous_Arbres, Sous_Arbres_Sans_Val, Sous_Arbre_Avec_Val),
	insere_branche(Branche, Sous_Arbre_Avec_Val, Sous_Arbre),
	Arbre_Out =.. [ab, Y | [(Val, Sous_Arbre) | Sous_Arbres_Sans_Val]].

insere_branche([(X, Val)], abvide, ab(X, Val)) :-
	!.
insere_branche([(X, Val) | Branche], abvide, ab(X, (Val, Sous_Arbre))) :-
	insere_branche(Branche, abvide, Sous_Arbre).



selectionne_sous_arbre(_Val, [], [], abvide).
selectionne_sous_arbre(Val, [(Val, Sous_Arbre) | Sous_Arbres], Sous_Arbres, Sous_Arbre) :-
	!.
selectionne_sous_arbre(Val, [VA | Sous_Arbres], [VA | Sous_Arbres_], Sous_Arbre) :-
	selectionne_sous_arbre(Val, Sous_Arbres, Sous_Arbres_, Sous_Arbre).

stocke(X, Val, Branche, [stock(Y, Branches_X) | Stock], [stock(X, [vb(Val, Branche) | Branches_X]) | Stock]) :-
	X == Y,
	!.
stocke(X, Val, Branche, [stock(Y, Branches_Y) | Stock_In], [stock(Y, Branches_Y) | Stock_Out]) :-
	stocke(X, Val, Branche, Stock_In, Stock_Out).

destocke(X, Val, Branche, [stock(Y, [vb(Val, Branche) | Branches_X]) | Stock], [stock(X, Branches_X) | Stock]) :-
	X == Y,
	!.
destocke(X, Val, Branche, [stock(Y, Branches_Y) | Stock_In], [stock(Y, Branches_Y) | Stock_Out]) :-
	destocke(X, Val, Branche, Stock_In, Stock_Out).


backtrack_echec(_, [], _Branche, _QuantPred, [], _Flot_Stock, flot(Facteurs, Facteurs)).
% Le point de choix été retrouvé
backtrack_echec(U, Trace, [(X, _Val_X) | Branche], QuantPred, QuantSuiv, Flot_Stock, Flot_Facteurs) :-
	Trace = [branch(Z, _Val_Z) | _Trace_],
	(
	  Q = e(Y, _D_X)
	;
	  Q = a(Y, _D_X)
	),
	append(QuantPred_, [Q], QuantPred),
	X == Y, Y == Z,!,
	descente(U, Trace, Branche, QuantPred_, [Q | QuantSuiv], Flot_Stock, Flot_Facteurs).
% Le point de choix est recherché
backtrack_echec(U, Trace, [(X, _Val_X) | Branche], QuantPred, QuantSuiv, Flot_Stock, Flot_Facteurs) :-
	Trace = [branch(_Z, _Val_Z) | _Trace_],
	(
	  Q = e(Y, _D_X)
	;
	  Q = a(Y, _D_X)
	),
	append(QuantPred_, [Q], QuantPred),
	X == Y, !,
	backtrack_echec(U,Trace, Branche, QuantPred_, [Q | QuantSuiv], Flot_Stock, Flot_Facteurs).