%% 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
%% 
:- use_module(library(clpb),[sat/1,taut/2,'*'/2,'+'/2,'~'/1]).
:- use_module(library(lists)).
:- use_module(sat).

litteral(Z) :-
	var(Z).
litteral(Z) :-
	Z = ~Y,
	var(Y).
disjonct(X,Y) :-
	litteral(Y),
	!,
	X=Y.
disjonct(X,Z) :-
	compound(Z),
	Z = X + _.
disjonct(X,Z) :-
	compound(Z),
	Z = _ + Y,
	disjonct(X,Y).

member_var(X,Y) :-
	X == Y,
	!.
member_var(X,Y+_C) :-
	X == Y,
	!.
member_var(X,Z) :-
	compound(Z),
	Z = _ + C,
	member_var(X,C).

selection_var(X,Y,0) :-
	X == Y,
	!.
selection_var(X,Y+C,C) :-
	X == Y,
	!.
selection_var(X,Z,C__) :-
	compound(Z),
	Z = Y+C,
	selection_var(X,C,C_),
	ajout_litteral(Y,C_,C__).

selection_litteral(L,C,C_) :-
	selection_var(L,C,C_).


member_non_var(X,~Y) :-
	X == Y,
	!.
member_non_var(X,~Y+_) :-
	X == Y,
	!.
member_non_var(X,Z) :-
	compound(Z),
	Z = _+C,
	member_non_var(X,C).


selection_non_var(X,~Y,0) :-
	X == Y,
	!.
selection_non_var(X,~Y+C,C) :-
	X == Y,
	!.
selection_non_var(X,Z,C__) :-
	nonvar(Z),
	Z = Y+C,
	selection_non_var(X,C,C_),
	ajout_litteral(Y,C_,C__).

selection_non_litteral(L,C,C_) :-
	selection_non_var(L,C,C_).

premiere_clause(Z,C,Cs) :- 
	compound(Z),
	Z = C * Cs,
	!.
premiere_clause(C,C,1).

premier_litteral(L,L,0) :-
	var(L),
	!.
premier_litteral((L+Ls),L,Ls).

ajout_conjonction(X, Y, 1)  :-  
	atomic(X),atomic(Y), X=1,Y=1,!.
ajout_conjonction(X, Y, 0) :-  
	atomic(X),atomic(Y), X=1,Y=0,!.
ajout_conjonction(X, Y, 0) :-  
	atomic(X), atomic(Y), X=0,Y=1,!.
ajout_conjonction(X, Y, 0) :-  
	atomic(X), atomic(Y), X=0,Y=0,!.
ajout_conjonction(X, Cs, Cs) :-  
	atomic(X), X=1, !.
ajout_conjonction(Cs, Y, Cs) :-  
	atomic(Y),Y=1,!.
ajout_conjonction(X, _Cs, 0) :-   
	atomic(X), X=0, !.
ajout_conjonction(_Cs, Y, 0) :-   
	atomic(Y), Y=0,!.
ajout_conjonction(Cs,Cs_,C*Cs_et_Cs_) :- 
	compound(Cs),
	Cs = C*Cs__,
	!,
	ajout_conjonction(Cs__,Cs_,Cs_et_Cs_).
ajout_conjonction(C,Cs,C*Cs).


ajout_litteral(X,C,C) :- 
	atomic(X), X = 0, !.
ajout_litteral(X,_,1) :- 
	atomic(X), X = 1, !.
ajout_litteral(~X,C,C) :- 
	atomic(X), X = 1, !.
ajout_litteral(~X,_,1) :- 
	atomic(X), X = 0, !.
ajout_litteral(X,Z,X) :-
	atomic(Z),
	Z = 0,
	!.
ajout_litteral(_,Z,1) :-
	atomic(Z),
	Z = 1,
	!.
ajout_litteral(X,C,1) :-
	(var(X), member_non_var(X,C) ; X = ~Y, var(Y), member_var(Y,C)),
	!.
ajout_litteral(X,C,C) :-
	(var(X), member_var(X,C) ; X = ~Y, var(Y), member_non_var(Y,C)),
	!.
ajout_litteral(X,C,X+C) :-
	(var(X), \+member_var(X,C) ; X = ~Y, var(Y), \+member_non_var(Y,C)).


conjonction_v_conjonction(X,_,1) :-
	atomic(X), 
	X = 1, 
	!.
conjonction_v_conjonction(Cs, Cs2, C_v_Cs2_x_Cs__v_Cs2) :-
	premiere_clause(Cs,C,Cs_),
	conjonction_v_clause(Cs2,C,C_v_Cs2),
	conjonction_v_conjonction(Cs_,Cs2,Cs__v_Cs2),
	ajout_conjonction(C_v_Cs2,Cs__v_Cs2,C_v_Cs2_x_Cs__v_Cs2).

conjonction_v_clause(X,_C,1) :-
	atomic(X),
	X = 1,
	!.
conjonction_v_clause(Cs,C,Cs__v_C_x_C__v_C)  :-
	premiere_clause(Cs,C_,Cs_),
	conjonction_v_clause(Cs_,C,Cs__v_C),
	clause_v_clause(C_,C,C__v_C),
	ajout_conjonction(C__v_C,Cs__v_C,Cs__v_C_x_C__v_C).

clause_v_clause(X,C,C) :-
	atomic(X),
	X = 0,
	!.
clause_v_clause(X,_C,1) :-
	atomic(X),
	X = 1,
	!.
clause_v_clause(C,X,C) :-
	atomic(X),
	X = 0,
	!.
clause_v_clause(_C,X,1) :-
	atomic(X),
	X = 1,
	!.
clause_v_clause(C, C_, 1) :-
	(disjonct(X,C),	var(X), member_non_var(X,C_);
	 disjonct(~X,C), var(X), member_var(X,C_)),
	 !.
clause_v_clause(C,C_,C_v_C_) :- clause_v_clause_(C,C_,C_v_C_).
clause_v_clause_(Y, C, C_) :- 
	litteral(Y),
	!,
	ajout_litteral(Y,C,C_).
clause_v_clause_(C,C_,C_v_C_) :-
	premier_litteral(C,L,C__),
	clause_v_clause_(C__,C_,C___v_C_),
	ajout_litteral(L,C___v_C_,C_v_C_).

extrait(_X,Y,1,1,1) :- 
	atomic(Y),
	Y = 1,
	!.
extrait(X,Cs,C_C_X,C_nX,C_sX) :-
	premiere_clause(Cs,C,Cs_),
	selection_litteral(X,C,C_),
	!,
	extrait(X,Cs_,C_X,C_nX,C_sX),
	ajout_conjonction(C_,C_X,C_C_X).
extrait(X,Cs,C_X,C_C_nX,C_sX) :-
	premiere_clause(Cs,C,Cs_),
	selection_non_litteral(X,C,C_),
	!,
	extrait(X,Cs_,C_X,C_nX,C_sX),
	ajout_conjonction(C_,C_nX,C_C_nX).
extrait(X,Cs,C_X,C_nX,C_C_sX) :-
	premiere_clause(Cs,C,Cs_),
	!,
	extrait(X,Cs_,C_X,C_nX,C_sX),
	ajout_conjonction(C,C_sX,C_C_sX).

elimine(_,Y,1) :- 
	atomic(Y),
	Y = 1,
	!.
elimine(X,Cs,Clauses_sans_X) :-
	premiere_clause(Cs,C,Clauses),
	selection_litteral(X,C,C_),
	!,
	elimine(X,Clauses,Clauses_sans_X_),
	ajout_conjonction(C_,Clauses_sans_X_,Clauses_sans_X).
elimine(X,Cs,Clauses_sans_X) :-
	premiere_clause(Cs,C,Clauses),
	selection_non_litteral(X,C,C_),
	!,
	elimine(X,Clauses,Clauses_sans_X_),
	ajout_conjonction(C_,Clauses_sans_X_,Clauses_sans_X).
elimine(X,Cs,Clauses_sans_X) :-
	premiere_clause(Cs,C,Clauses),
	!,
	elimine(X,Clauses,Clauses_sans_X_),
	ajout_conjonction(C,Clauses_sans_X_,Clauses_sans_X).

% Calcul des model factors

model_factors([],[],Clauses,[],Clauses).
model_factors([X|L],[e|Q],Clauses,[(C_X,C_nX)|Couples],Clauses_sans_X) :-
	model_factors(L,Q,Clauses,Couples,Clauses_),
	extrait(X,Clauses_,C_X,C_nX,Clauses_sX_),
	conjonction_v_conjonction(C_X,C_nX,C_XCn_X),
	ajout_conjonction(C_XCn_X, Clauses_sX_,Clauses_sans_X).
model_factors([X|L],[a|Q],Clauses,Couples,Clauses_sans_X) :-
	model_factors(L,Q,Clauses,Couples,Clauses_),
	elimine(X,Clauses_,Clauses_sans_X).


% Le parseur de liste de listes de littéraux en une forme pour la librairie sat de Sicstus

parse([],1).
parse([C|Cs],F) :-
	parse_(C,FC),!,
	parse(Cs,FCs),
	ajout_conjonction(FC,FCs,F).

parse_([],0).
parse_([L|C],F) :-
	atomic(L),
	!,
	parse_(C,FC),
	ajout_litteral(L,FC,F).
parse_([L|C],F) :-
	compound(L),
	L= ~L_,
	atomic(L_),
	!,
	parse_(C,FC),
	ajout_litteral(L,FC,F).
parse_([L|C],F) :-
	litteral(L),
	!,
	parse_(C,FC),
	ajout_litteral(L,FC,F).
parse_([~(~L)|C],F) :-
	parse_(C,FC),
	ajout_litteral(L,FC,F).