%% 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
%% 
% programme ELIMINATION_BL_QBF_CNF
:- module('ELIMINATION_BL_QBF_CNF', [elimination_bl_qbf_cnf/3,certificate_bottom_up_cnf/3]).
% etend
% :- ['QBF'].
:- use_module('QBF_CNF',[parse/2, model_factors/4, model_factors/5]).
:- use_module(library(lists)).
% sorte : Binder, Certificate
% symbole de fonction
%  certificate : Binder x Liste(Formule x Formule) -> Certificate
% symboles de predicat
%  elimination_bl_qbf_cnf : Binder x Liste(Clauses) x Certificate

% CNF
elimination_bl_qbf_cnf(Binder,Clauses,bl(Binder,Couples)) :-
	Clauses = [_ | _],!,
	parse(Clauses,Formula),
	model_factors(Binder, Formula, Couples, 1),
	!.



certificate_bottom_up_cnf(Binder,Clauses, Cert) :-
	Clauses = [_ | _],!,
	parse(Clauses,Formula),
	Binder = binder(Quant, Variables),
	(model_factors(Quant, Variables, Formula, Couples, 1) ->
	Cert = certificate(Binder,Couples) ; Cert = non_valid),
	!.

separe([], [], []).
separe([e(X) | Binder], [e | Quant], [X | Vars]) :-
	separe(Binder, Quant, Vars).
separe([a(X) | Binder], [a | Quant], [X | Vars]) :-
	separe(Binder, Quant, Vars).