%% Copyright (C) 2011 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('TRACE_SEARCH_QCSP', [trace_search_qcsp/3]).
:- use_module(library(lists)).
:- use_module(library(clpfd)).

% symboles de predicat
%  trace_search_qcsp  : Liste(_) x Clp x Base_Litterale
%  insatisfiable : Base_Litterale

% bltop, blbottom : Bl
% bl : Liste(Vlva) -> Bl
% vlva : Var x Liste(Va) -> Vlva
% va : Val x Arbre_Etiquete -> Va
% (_,_) : Val x Arbre_Etiquete
% top, bottom : Arbre_Etiquete 
 
%% trace_search_qcsp : Liste(Quant)  x Csp x Liste(Commandes)
trace_search_qcsp(Quant, Contraintes, Commandes) :-
	trace_search_qcsp_init(Quant, Quant, Contraintes, Commandes).

%% trace_search_qcsp_init : Liste(Quant) x Liste(Quant)  x Csp x Liste(Commandes)

trace_search_qcsp_init([],[], Contraintes, [succes]) :-
	call(Contraintes), !.

trace_search_qcsp_init([e(Xinit, _) | VariablesInit], [e(X,D_X) | Variables], Contraintes, Commandes) :-
	\+(\+(call(Contraintes))),
	!,
	e_map_trace_search_qcsp_exist(Xinit, D_X,X, VariablesInit, Variables, Contraintes, Commandes).

trace_search_qcsp_init([a(Xinit, _) | VariablesInit], [a(X,D_X) | Variables], Contraintes, Commandes) :-
	\+(\+(call(Contraintes))),
	!,
	a_map_trace_search_qcsp(Xinit, D_X,X, VariablesInit, Variables, Contraintes, Commandes_, Resultat),
	(
	  Resultat = succes
	->
	  append(Commandes_, [succes_global], Commandes)
	;
	  append(Commandes_, [echec_global], Commandes)
	).

trace_search_qcsp_init(_, _, _Contraintes, [echec]).

%% On franchit les premieres existentielles jusqu'à la première universelle (si elle existe).
e_map_trace_search_qcsp_exist(Xinit, D_X, X, VariablesInit, Variables, Contraintes, Commandes):-
	(Variables = [a(_,_) | _] ; Variables = []),
	!,
	e_map_trace_search_qcsp_last_exist(Xinit, D_X, X, VariablesInit, Variables, Contraintes, Commandes).

e_map_trace_search_qcsp_exist(_Xinit, [], _X, _VariablesInit, _Variables, _Contraintes, []).
e_map_trace_search_qcsp_exist(Xinit, [Val | D_X], X, VariablesInit, Variables, Contraintes, [branch(Xinit, Val) | Commandes_Out]):-
	copy_term((Variables, X, Contraintes), (Variables_Val, Val, Contraintes_Val)),
	trace_search_qcsp_exist(VariablesInit, Variables_Val, Contraintes_Val, Commandes_Val),
	e_map_trace_search_qcsp_exist(Xinit, D_X, X, VariablesInit, Variables, Contraintes, Commandes),
	append(Commandes_Val, Commandes, Commandes_Out).

trace_search_qcsp_exist([],[], Contraintes, [succes]) :-
	call(Contraintes), !.

trace_search_qcsp_exist([e(Xinit, _) | VariablesInit], [e(X,D_X) | Variables], Contraintes, Commandes) :-
	\+(\+(call(Contraintes))),
	!,
	e_map_trace_search_qcsp_exist(Xinit, D_X,X, VariablesInit, Variables, Contraintes, Commandes).

trace_search_qcsp_exist(_, _, _Contraintes, [echec]).

%% On franchit la dernière existentielle du premier paquet
%% e_map_trace_search_qcsp_last_exist : Liste(Val) x Var x Liste(Quant) x Liste(Quant) x Csp x Liste(Commandes)
e_map_trace_search_qcsp_last_exist(_Xinit, [], _X, _VariablesInit, _Variables, _Contraintes, []).
e_map_trace_search_qcsp_last_exist(Xinit, [Val | D_X], X, VariablesInit, Variables, Contraintes, [branch(Xinit, Val) | Commandes_Out]):-
	copy_term((Variables, X, Contraintes), (Variables_Val, Val, Contraintes_Val)),
	trace_search_qcsp(VariablesInit, Variables_Val, Contraintes_Val, Commandes_Val, Resultat_Val),
	(
	  Resultat_Val = succes
	->
	  append(Commandes_Val, [succes_global], Commandes_Val_)
	;
	  Commandes_Val_ = Commandes_Val
	),
	e_map_trace_search_qcsp_last_exist(Xinit, D_X, X, VariablesInit, Variables, Contraintes, Commandes),
	append(Commandes_Val_, Commandes, Commandes_Out).


%% trace_search_qcsp : Liste(Quant) x Liste(Quant)  x Csp x Liste(Commandes)
trace_search_qcsp([],[], Contraintes, [succes], succes) :-
	call(Contraintes), !.

trace_search_qcsp([e(Xinit, _) | VariablesInit], [e(X,D_X) | Variables], Contraintes, Commandes, Resultat) :-
	\+(\+(call(Contraintes))),
	!,
	e_map_trace_search_qcsp(Xinit, D_X,X, VariablesInit, Variables, Contraintes, Commandes, Resultat).

trace_search_qcsp([a(Xinit, _) | VariablesInit], [a(X,D_X) | Variables], Contraintes, Commandes, Resultat) :-
	\+(\+(call(Contraintes))),
	!,
	a_map_trace_search_qcsp(Xinit, D_X,X, VariablesInit, Variables, Contraintes, Commandes, Resultat).

trace_search_qcsp(_, _, _Contraintes, [echec], echec).
	


%% e_map_trace_search_qcsp : Liste(Val) x Var x Liste(Quant) x Liste(Quant) x Csp x Liste(Bl)
e_map_trace_search_qcsp(_Xinit, [], _X, _VariablesInit, _Variables, _Contraintes, [], echec).
e_map_trace_search_qcsp(Xinit, [Val | D_X], X, VariablesInit, Variables, Contraintes, [branch(Xinit, Val) | Commandes_Out], Resultat):-
	copy_term((Variables, X, Contraintes), (Variables_Val, Val, Contraintes_Val)),
	trace_search_qcsp(VariablesInit, Variables_Val, Contraintes_Val, Commandes_Val, Resultat_Val),
	(Resultat_Val = succes -> Resultat = succes ; Resultat = Resultat_Rec),
	e_map_trace_search_qcsp(Xinit, D_X, X, VariablesInit, Variables, Contraintes, Commandes, Resultat_Rec),
	append(Commandes_Val, Commandes, Commandes_Out).

%% a_map_trace_search_qcsp : Liste(Val) x Var x Liste(Quant) x Liste(Quant) x Csp x Liste(Bl)
a_map_trace_search_qcsp(_Xinit, [], _X, _VariablesInit, _Variables, _Contraintes, [], succes).
a_map_trace_search_qcsp(Xinit, [Val | D_X], X, VariablesInit, Variables, Contraintes, [branch(Xinit, Val) | Commandes_Out], Resultat):-
	copy_term((Variables, X, Contraintes), (Variables_Val, Val, Contraintes_Val)),
	trace_search_qcsp(VariablesInit, Variables_Val, Contraintes_Val, Commandes_Val, Resultat_Val),
	(
	  Resultat_Val = echec
	->
	  append(Commandes_Val, [echec(Xinit, Val)], Commandes_Out),
	  Resultat = Resultat_Val
	;
	  a_map_trace_search_qcsp(Xinit, D_X, X, VariablesInit, Variables, Contraintes, Commandes, Resultat),
	  append(Commandes_Val, Commandes, Commandes_Out)
	).