%% 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(qbf_cnf).

politique([],[],[],_,[]).

politique((X; P), [X|L], [e|Q], M, [(_C_X,C_nX)|C]) :-
	'|='(X*M,C_nX),
	politique(P,L,Q,X*M,C).
politique((~X; P), [X|L], [e|Q], M, [(C_X,_C_nX)|C]) :-
	'|='(~X*M,C_X),
	politique(P,L,Q,~X*M,C).

politique([(X -> P_X),((~X) -> P_nX)], [X|L],[a|Q], M, C) :-
	politique(P_X,L,Q,X*M,C),
	politique(P_nX,L,Q,~X*M,C).


models(binder(Q,L),Clauses,P) :-
	parse(Clauses,Formule),
	(model_factors(L,Q,Formule,Couples,1) ->
	    politique(P,L,Q,1,Couples);
	    P = non_valide).


% | ?- models(binder([a,e,a,e],[_a,_b,_c,_d]),[[~_a, ~_b, ~_c, _d],[~_a, ~_b,_c, ~_d],[~_a, _b,_c, ~_d],[~_a, _b,_c, _d],[_a, ~_b,~_c, _d],[_a, ~_b,_c, _d],[_a, _b,_c, ~_d],[_a, _b,_c, _d]],P).
%
% P = [(_a->(_b;[(_c->(_d;[])),(~_c->(~_d;[]))])),(~_a->(_b;[(_c->(_d;[])),(~_c->(_d;[]))]))] ? ;
%
% no

% | ?- models(binder([e,e,e,a,e,e,e,a,e,e],[_1,_2,_3,_4,_5,_6,_7,_8,_9,_10]),[[_1],[_4, ~_1, _5],[_4, ~_5, _1],[_4, ~_3, _6],[_4, ~_6, _3],[~_4, ~_3, _5],[~_4, ~_5, _3],[~_4, ~_2, _6],[~_4, ~_6, _2],[~_8, ~_5, _9],[~_8, ~_9, _5],[~_8, ~_7, _10],[~_8, ~_10, _7],[_8, ~_7, _9],[_8, ~_9, _7],[_8, ~_6, _10],[_8, ~_10, _6],[~_9, _10]],P).
%
% P = _1;_2;_3;[(_4->(_5;_6;_7;[(_8->(_9;_10;[])),(~_8->(_9;_10;[]))])),(~_4->(_5;_6;_7;[(_8->(_9;_10;[])),(~_8->(_9;_10;[]))]))] ? ;
% 
% no