%% 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(qbf_cnf,[parse/2, models_factors/5]).
:- use_module(sat, [simplification/2]).

simplification_certificate([],[],[],[],_).
simplification_certificate([X|L],[e|Q],[(C_X,_C_nX) | Certificate],[(0,1) | NCertificate], M) :-
	'M|=C'(M,~C_X),
	!,
	simplification_certificate(L,Q,Certificate, NCertificate,X*M).

simplification_certificate([X|L],[e|Q],[(_C_X,C_nX) | Certificate],[(1,0) | NCertificate], M) :-
	'M|=C'(M,~C_nX),
	!,
	simplification_certificate(L,Q,Certificate, NCertificate,~X*M).

simplification_certificate([_X|L],[e|Q],[(C_X,C_nX) | Certificate],[(C_X,C_nX) | NCertificate], M) :-
	simplification_certificate(L,Q,Certificate, NCertificate,M).

simplification_certificate([_X|L],[a|Q], Certificate,NCertificate,M) :-
	simplification_certificate(L,Q,Certificate, NCertificate,M).


certificate(binder(Q,L),Clauses,Certificate) :-
	parse(Clauses,Formule),
	(model_factors(L,Q,Formule,Couples,1) ->
	    Certificate = Couples;
	    Certificate = non_valide),!.