%% 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
%% 
:- module('QBF_CNF', [parse/2, model_factors/4, model_factors/5]).
:- use_module(library(clpb),[]).
:- use_module(library(lists)).

% 'litteral_?' : _
% litteral : _ % Obsolete
litteral(Z) :- 'litteral_?'(Z).
'litteral_?'(Z) :-
	var(Z).
'litteral_?'(Z) :-
	Z = ~Y,
	var(Y).

% disjonct : Formule x Formule
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 : Formule x Formule
premiere_clause(Z,C,Cs) :- 
	compound(Z),
	Z = C * Cs,
	!.
premiere_clause(C,C,1).

% premier_litteral : Formule x _
premier_litteral(L,L,0) :-
	var(L),
	!.
premier_litteral((L+Ls),L,Ls).

% ajout_conjonction : _ x Formule x Formule
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 Formule x Formule
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 : Formule x Formule x Formule
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 Formule x Formule
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 : Liste(_) x Liste(Quantificateur) x Liste(Clause x Clause)

model_factors([], Clauses, [], Clauses).
model_factors([e(X)|VariablesQuantifiees], Clauses, [(C_nX,C_X)|Couples], Clauses_sans_X) :-
	model_factors(VariablesQuantifiees, 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([a(X)|VariablesQuantifiees], Clauses, [(1,1) | Couples], Clauses_sans_X) :-
	model_factors(VariablesQuantifiees, Clauses, Couples, Clauses_),
	elimine(X, Clauses_, Clauses_sans_X).


model_factors([], [], Clauses, [], Clauses).
model_factors([e | Quantifiees], [X|Variables], Clauses, [(C_X,C_nX)|Couples], Clauses_sans_X) :-
	model_factors(Quantifiees, Variables, 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([a | Quantifiees], [X|Variables], Clauses, Couples, Clauses_sans_X) :-
	model_factors(Quantifiees,Variables, 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 : Liste(Clauses) x Formule
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).

% Calcul la taille d'une formule clpb i.e. le nombre d'arcs dans la formule vue comme un arbre.
taille(F, N) :-
	nonvar(F),
	F = (A+B),
	!,
	taille(A, NA),
	taille(B, NB),
	N is NA + NB + 2.
taille(F, N) :-
	nonvar(F),
	F = (A*B),
	!,
	taille(A, NA),
	taille(B, NB),
	N is NA + NB + 2.
taille(_, 0).

% Calcul une formule clpb NNF pour le problème "odd parity"
odd_parity(1, [V], V).
odd_parity(N, Vars, Pos_Impair) :-
	N > 1,
	odd_parity(N, Vars, Pos_Impair, _Pos_Pair).
odd_parity(2, [V, V_], ((V * ~V_) + (~V * V_)), ((V * V_) + (~V * ~V_))).
odd_parity(N, [V | Vars], (Pos_Impair_ + Pos_Impair__), (Pos_Pair_ + Pos_Pair__)) :-
	N > 2,
	N1 is N - 1,
	odd_parity(N1, Vars, Pos_Impair, Pos_Pair),
	dist(Pos_Impair, ~V, Pos_Impair_),
	dist(Pos_Pair, ~V, Pos_Pair_),
	dist(Pos_Impair, V, Pos_Pair__),
	dist(Pos_Pair, V, Pos_Impair__).

dist(T, V, (V * T)) :-
	var(T),
	!.
dist(T, V, (V * T)) :-
	T = ~_,
	!.
dist(T, V, (V * T)) :-
	T = (_ * _),
	!.
dist((T + Ts), V, ((V * T) + Res)) :-
	dist(Ts, V, Res).