%% 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('BASE_LITTERALE', [interpretation/2, oubases/3, oubases_it/3, opbases/4, etbases/3, insatisfiable/1, cofacteurs/2, variables_bl/2, mapconj_bl/3]). % etend % :- ['LISTE']. :- use_module(library(clpb), []). :- use_module('SAT',[forme_normale_disjonctive/2, '==='/2]). :- use_module(library(lists), [append/3]). % sorte : Base_Litterale % symbole de fonction % bl : Liste(_) x Liste(Clpb x Clpb) -> Base_Litterale % symbole de predicat % interpretation : Base_Litterale x Clpb % interpretation : Liste(_) x Liste(Clpb x Clpb) x Clpb % mapconj_bl : Liste(_) x Liste({0|1}) x Liste(Base_Litterale) % conj_bl : Liste(_) x Liste({0|1}) x Base % conj_bl : Liste({0|1}) x Base % oubases : Base_Litterale x Base_Litterale x Base_Litterale % oubases : Liste(_) x Liste(Clpb x Clpb) x Liste(Clpb x Clpb) x Liste(Clpb x Clpb) % combine : Liste(_) x Liste(Clpb x Clpb) x Clpb x Liste(Clpb x Clpb) x Clpb x Liste(Clpb x Clpb) x Liste(Clpb x Clpb) % oubases_it : Base_Litterale x Base_Litterale x Base_Litterale % oubases_it : Liste(_) x Liste(Clpb x Clpb) x Liste(Clpb x Clpb) x Liste(Clpb x Clpb) % definitions interpretation(bl(VB, B), I) :- interpretation(VB, B, I). interpretation([], [], 1). interpretation([V | Variables], [(P, N) | L], I) :- (var(V) -> V = X ; (V = e(X) ; V = a(X))), interpretation(Variables, L, I_), % forme_normale_disjonctive(((X + P) * (~X + N)) * I_, I). forme_normale_disjonctive(((~X + P) * (X + N)) * I_, I). oubases(bl(VB, B), bl(VB_, B_), bl(VB__, B__)) :- VB == VB_, VB__ = VB, oubases(VB, B, B_, B__). oubases([], B, B_, B__) :- simplification(B+B_, B__). oubases([_Variable], [(P, N)], [(P_, N_)], [(Resultat_P, Resultat_N)]) :- !, forme_normale_disjonctive(P + P_, Resultat_P), forme_normale_disjonctive(N + N_, Resultat_N). oubases([V | Variables], [(Pn, Nn) | B], [(Pn_, Nn_) | B_], [(Resultat_P, Resultat_N) | B__]) :- (var(V) -> V = X ; (V = e(X) ; V = a(X))), Variables = [_ | _], oubases(Variables, B, B_, B___), simplification_Xn(X, Pn, Nn, Xn), simplification_Xn(X, Pn_, Nn_, Xn_), combine(Variables, B___, Xn, B, Xn_, B_, B__), forme_normale_disjonctive(Pn + Pn_, Resultat_P), forme_normale_disjonctive(Nn + Nn_, Resultat_N). oubases_it(bl(S, Gardes), bl(S_, Gardes_), bl(S__, Gardes__)) :- S == S_, S__ = S, oubases_it(S, Gardes, Gardes_, Gardes__). oubases_it([], Gardes, Gardes_, Gardes__) :- simplification(Gardes+Gardes_, Gardes__). oubases_it(Symboles, Gardes, Gardes_, Gardes__) :- Symboles = [_ | _], oubases_it_((Symboles, []), (Gardes, []), (Gardes_, []), Gardes__). oubases_it_(([], _), ([],_), ([],_), []). oubases_it_(([Xi | Symboles_i_plus_1_a_n], Symboles_1_a_i_moins_1), ([(Pi, Ni) | Gardesi_plus_1_a_n], Gardes1_a_i_moins_1), ([(Pi_, Ni_) | Gardes_i_plus_1_a_n], Gardes_1_a_i_moins_1), [((Pi + Pi_)* (Pi + Combination_) * (Pi_ + Combination), (Ni + Ni_)* (Ni + Combination_) * (Ni_ + Combination)) | Gardes__]) :- append(Gardes1_a_i_moins_1, [(Pi, Ni)], Gardes1_a_i), append(Gardes_1_a_i_moins_1, [(Pi_, Ni_)], Gardes_1_a_i), append(Symboles_1_a_i_moins_1, [Xi], Symboles_1_a_i), oubases_it_((Symboles_i_plus_1_a_n, Symboles_1_a_i), (Gardesi_plus_1_a_n, Gardes1_a_i), (Gardes_i_plus_1_a_n, Gardes_1_a_i), Gardes__), combine_it(Symboles_1_a_i_moins_1, Gardes1_a_i_moins_1, Combination), combine_it(Symboles_1_a_i_moins_1, Gardes_1_a_i_moins_1, Combination_). combine_it([], [], 1). combine_it([X | Symboles], [(P, N) | Gardes], ((~X + P) * (X + N)) * Combinaison) :- combine_it(Symboles, Gardes, Combinaison). etbases(bl(Variables, B), bl(Variables, B_), bl(Variables, B__)) :- etbases(Variables, B, B_, B__). etbases([], B, B_, B__) :- simplification(B*B_, B__). etbases([_Variable], [(P, N)], [(P_, N_)], [(Resultat_P, Resultat_N)]) :- !, forme_normale_disjonctive(P * P_, Resultat_P), forme_normale_disjonctive(N * N_, Resultat_N). etbases([V | Variables], [(Pn, Nn) | B], [(Pn_, Nn_) | B_], [(Resultat_P, Resultat_N) | B__]) :- (var(V) -> V = X ; (V = e(X) ; V = a(X))), etbases(Variables, B, B_, B__), forme_normale_disjonctive(Pn * Pn_, Resultat_P), forme_normale_disjonctive(Nn * Nn_, Resultat_N). simplification_Xn(X, Pn, Nn, Xn) :- ( Nn == 1, !, ( Pn == 1, !, Xn = 1 ; Pn == 0, !, Xn = ~X ; Xn = (~X + Pn) ) ; Nn == 0, !, ( Pn == 1, !, Xn = X ; Pn == 0, !, Xn = 0 ; Xn = (X + Nn) ) ; Xn = ((~X + Pn) * (X + Nn)) ). %simplification_Xn(X, Pn, Nn, Xn) :- % ( % Pn == 1, !, % ( % Nn == 1, !, % Xn = 1 % ; % Nn == 0, !, % Xn = ~X % ; % Xn = (~X + Nn) % ) % ; % Pn == 0, !, % ( % Nn == 1, !, % Xn = X % ; % Nn == 0, !, % Xn = 0 % ; % Xn = (X + Pn) % = (X * (~X + Pn)) ???? % ) % ; % Xn = ((X + Pn) * (~X + Nn)) % ). combine([], [],_Xn, [], _Xn_, [], []). combine([_Xk | Variables], [(PXk, NXk) | B___], Xn, [(Pk, Nk) | B], Xn_, [(Pk_, Nk_) | B_], [(Resultat_Pk, Resultat_Nk) | B__]) :- combine(Variables, B___, Xn, B, Xn_, B_, B__), forme_normale_disjonctive((PXk * (Pk_ + Xn) * (Pk + Xn_)), Resultat_Pk), forme_normale_disjonctive((NXk * (Nk_ + Xn) * (Nk + Xn_)), Resultat_Nk). mapconj_bl(_, [],[]). mapconj_bl(Variables, [Modele | Modeles], [Base | Bases]) :- conj_bl(Variables, Modele, Base), mapconj_bl(Variables, Modeles, Bases). conj_bl(Variables, Modele, bl(Variables, Base)) :- conj_bl(Modele, Base). conj_bl([], []). % conj_bl([1 | Modele], [(0, 1) | Base]) :- conj_bl([1 | Modele], [(1, 0) | Base]) :- conj_bl(Modele, Base). % nj_bl([0 | Modele], [(1, 0) | Base]) :- conj_bl([0 | Modele], [(0, 1) | Base]) :- conj_bl(Modele, Base). insatisfiable(0). insatisfiable(bl([_ | Variables], [(Pi, Ni) | Cofacteurs])) :- ( Pi === 0, Ni === 0, ! ; insatisfiable(bl(Variables, Cofacteurs)) ). cofacteurs(bl(_, Cofacteurs), Cofacteurs). variables_bl(bl(Variables, _), Variables). opbases(X, bl(Variables, Cofacteurs_Top), bl(Variables, Cofacteurs_Bottom), bl([a(X) | Variables], [(1,1) | Cofacteurs])) :- opbases_(X, Variables, Cofacteurs_Top, Cofacteurs_Bottom, Cofacteurs). opbases_(_X, [], [],[],[]). opbases_(X, [e(_) | Variables], [(P, N) | Cofacteurs_Top], [(P_, N_) | Cofacteurs_Bottom], [(FND_P, FND_N) | Cofacteurs]) :- forme_normale_disjonctive((~X + P) * (X + P_), FND_P), forme_normale_disjonctive((~X + N) * (X + N_), FND_N), opbases_(X, Variables, Cofacteurs_Top, Cofacteurs_Bottom, Cofacteurs). opbases_(X, [a(_) | Variables], [(1, 1) | Cofacteurs_Top], [(1, 1) | Cofacteurs_Bottom], [(1, 1) | Cofacteurs]) :- opbases_(X, Variables, Cofacteurs_Top, Cofacteurs_Bottom, Cofacteurs).