%% 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(sat, ['|='/2, '|='/1, sat/1, contingent/1, contingent/2, '==='/3, '==='/2, simplification/2, forme_normale_disjonctive/2, modeles_vers_FND/2, formule_clpb/1, expression_clpb/1]).
:- use_module(library(clpb),[sat/1,taut/2, labeling/1]).
:- use_module('/home/stephan/MES_LIVRES/PROGRAMMATION_LOGIQUE/PROGRAMMES/VARIABLES',[variables/2]).
% :- use_module(library(clpb),['*'/2,'+'/2,'>'/2,'<'/2,'~'/1]).
:- op(800, xfx, '|='). % cf http://www.sics.se/sicstus/docs/latest3/html/sicstus.html/Standard-Operators.html#Standard-Operators
:- op(800, xfx, '==='). % cf http://www.sics.se/sicstus/docs/latest3/html/sicstus.html/Standard-Operators.html#Standard-Operators

'SAT':sat(F) :-
       \+(\+(sat(F))).

'|='(M,F) :-
	\+(\+((sat(M),taut(F,1)))).

'|='(F) :-
	\+(\+(taut(F,1))).

contingent(F) :-
	\+(taut(F,1)),
	\+(taut(~F,1)).
contingent(M,F) :-
	\+((sat(M),taut(F,1))),
	\+((sat(M),taut(~F,1))).

'==='(M,X,Y) :-
	\+(\+((sat(M),taut((X >= Y) * (X =< Y),1)))).
'==='(X,Y) :-
	\+(\+(taut((X >= Y) * (X =< Y),1))).

simplification(X,X) :-
	(
	  var(X)
	;
	  atomic(X)
	),
	!.

simplification(~X,Z) :-
	simplification(X,X_),
	(
	  (compound(X_), X_ = ~Z) ->
	  true
	;
	  Z = ~X_
	).
simplification(X*Y,Z) :-
	simplification(X,X_),
	simplification(Y,Y_),
	(
	    atomic(X_),
	    X_ = 0,
	    !,
	    Z = 0
	;
	    atomic(Y_),
	    Y_ = 0,
	    !,
	    Z = 0
	;
	    atomic(X_),
	    X_ = 1,
	    !,
	    Z = Y_
	;    
	    atomic(Y_),
	    Y_ = 1,
	    !,
	    Z = X_
	;
	    compound(X_),
	    X_ = ~U,
	    U == Y_,
	    !,
	    Z = 0
	;
	    compound(Y_),
	    Y_ = ~U,
	    U == X_,
	    !,
	    Z = 0
	;
	    X_ == Y_,
	    !,
	    Z = X_
	;
	    Z = X_ * Y_
	).
simplification(X+Y,Z) :-
	simplification(X,X_),
	simplification(Y,Y_),
	(
	    atomic(X_),
	    X_ = 1,
	    !,
	    Z = 1
	;
	    atomic(Y_),
	    Y_ = 1,
	    !,
	    Z = 1
	;
	    atomic(X_),
	    X_ = 0,
	    !,
	    Z = Y_
	;    
	    atomic(Y_),
	    Y_ = 0,
	    !,
	    Z = X_
	;
	    compound(X_),
	    X_ = ~U,
	    U == Y_,
	    !,
	    Z = 1
	;
	    compound(Y_),
	    Y_ = ~U,
	    U == X_,
	    !,
	    Z = 1
	;
	    X_ == Y_,
	    !,
	    Z = X_
	;
	    Z = X_ + Y_
	).


forme_normale_disjonctive(F, FND) :-
	'VARIABLES':variables(F, Variables),
	forme_normale_disjonctive(Variables, F, FND).

forme_normale_disjonctive([], F, 1) :-
	sat(F),
	!.
forme_normale_disjonctive([], F, 0) :-
	\+(sat(F)),
	!.
forme_normale_disjonctive(Variables, F, FND) :-
	bagof(Variables, (sat(F), labeling(Variables)), Modeles),
	!,
	modeles_vers_FND(Variables, Modeles, FND).
forme_normale_disjonctive(_Variables, F, 0) :-
	\+(sat(F)).

modeles_vers_FND(_Variables, [], 0).
modeles_vers_FND(Variables, [Modele | Modeles], (Une_FND + FND)) :-
	modele_vers_FND(Variables, Modele, Une_FND),
	modeles_vers_FND(Variables, Modeles, FND).

modele_vers_FND([], [], 1).
modele_vers_FND([X | Variables], [1 | Modeles], (X * FND)) :-
	modele_vers_FND(Variables, Modeles, FND).
modele_vers_FND([X | Variables], [0 | Modeles], (~X * FND)) :-
	modele_vers_FND(Variables, Modeles, FND).
	

formule_clpb(T) :-
	var(T), !.
formule_clpb(T) :-
	atomic(T), !.
formule_clpb(T) :-
	compound(T),
	T = ~T_, !,
	formule_clpb(T_).
formule_clpb(T) :-
	compound(T),
	(T = (G + D) ; T = (G * D)),
	formule_clpb(G),
	formule_clpb(D).


expression_clpb(T) :-
	atomic(T).
expression_clpb(T) :-
	compound(T),
	T = ~T_, !,
	expression_clpb(T_).
expression_clpb(T) :-
	compound(T),
	(T = (G + D) ; T = (G * D)),
	expression_clpb(G),
	expression_clpb(D).