/* Résolution propositionnelle J-F. Perrot 20-03-09 */

/* (1) Exemples */

winst([[[],[p]], [[],[u]],[[p],[q]], [[q],[r]], [[r],[s]],[[u,s],[]]]).
myst([[[p],[q]], [[q],[r]], [[r],[s]], [[u,s],[]], [[],[p]], [[],[u]]]).
hunt([ [[],[q]], [[],[p,r]], [[p],[s]], [[r],[s]], [[p,q,s],[]],
	[[q,r,s],[]] ]).
lovld([ [[],[a]], [[a],[b]], [[],[b,d]], [[],[c,d]], [[d],[c]],
	[[c],[e]], [[c,e],[]] ]).
nonex([ [[],[a,b,c]], [[],[e]], [[e],[b]], [[],[r,s]] ]).
nyst([[[p],[q]], [[q],[r]], [[s],[r]], [[u,s],[]], [[],[p]], [[],[u]]]).

/* Predicats pour essais commodes : appel par "essd(myst)" p.ex. */
/* essD comme essai de resolution Directe */
essd(Nom) :- T =..[Nom, X], call(T), normalise(X, Y), resolution(Y).
/* essL comme essai de resolution Lineaire */
essl(Nom) :- T =..[Nom, X], call(T), normalise(X, Y), reslineaire(Y).

/*(2) Gestion des ensembles (listes) de clauses
     ------------------------------------------ */
/* concat([], X, X).
concat([A|S], X, [A|Y]) :- concat(S, X, Y).
remplacé par append */

/* normalise(DonneeBrute, ResultatNormal) */

normalise([], []).
normalise([[N, P]|S], [[NN, NP]|NS]) :- sort(N, NN), sort(P, NP),
					normalise(S,NS).

/* adjonction SANS DUPLICATION d'une liste d'objets L1 (clauses ou
 atomes) a` une autre liste d'objets L2 : add(L1, L2, Resultat) */

add([], X, X).
add([A|S], X, Y) :- present(A, X), !, add(S, X, Y).
add([A|S], X, [A|Y]) :-  add(S, X, Y).

present(A, [B|S]):- A=B, !. /* on teste l'egalite, pas l'identite' */
present(A, [_|S]):- present(A, S).

reduire(X, Y, NX, NY) :- append(AX, [U|DX], X), append(AY, [U|DY], Y),
			append(AX, DX, NX), append(AY, DY, NY).

resolvante([NA, PA], [NB, PB], [NR, PR]) :-
		reduire(NA, PB, NNA, NPB), !,
		add(NNA, NB, NS), add(NPB, PA, PS),
		sort(NS, NR), sort(PS, PR).

resolvante([NA, PA], [NB, PB], [NR, PR]) :-
		reduire(PA, NB, NPA, NNB), !,
		add(NNB, NA, NS), add(NPA, PB, PS),
		sort(NS, NR), sort(PS, PR).

robinson(LCl, LR) :- resoudre(LCl, LCl, LR).

resolution(LCl) :- present([[],[]], LCl), !, write(oui).
resolution(LCl) :- robinson(LCl, LR), sresolution(LCl, LR).

sresolution(LCl, []) :- !, write(non). /* LCl fermee par resolution */
sresolution(LCl, LR) :- append(LR, LCl, L), resolution(L).

/* resoudre(Ref, LCl, Res), calcule Res la liste des resolvantes
de la liste LCl avec elle-meme qui ne sont pas dans Ref.
 */

resoudre(Ref, [], []).
resoudre(Ref, [Cl | SCl], Res):- resol(Ref, Cl, SCl, U), 
			resoudre(Ref, SCl, S), add(U, S, Res).
resol(Ref, Cl, [], []).
resol(Ref, Cl, [A|S], T) :- resolvante(Cl, A, R), !, 
				sresol(Ref, R, Cl, S, T).
resol(Ref, Cl, [_|S], U) :- resol(Ref, Cl, S, U).

sresol(Ref, Res, Cl, LCl, R) :- present(Res, Ref), !, 
				resol(Ref, Cl, LCl, R).
sresol(Ref, Res, Cl, LCl, [Res|R]) :- resol(Ref, Cl, LCl, R).

/* Ouf ! C'est tout.. Ca marche, mais quel effort....*/

rresoudre(LCl) :- normalise(LCl, X), resolution(X).


/*(5) La resolution propositionnelle lineaire 
      --------------------------------------- */
      
resolin(Ref, Cl, [A|S]) :- resolvante(Cl, A, R), 
				sresolin(Ref, R, Cl, S).
resolin(Ref, Cl, [_|S]) :- resolin(Ref, Cl, S).


sresolin(Ref, [[], []], Cl, S):- !. /* Resolvante vide, on a reussi */
sresolin(Ref, R, Cl, S) :- present(R, Ref), !, resolin(Ref, Cl, S).
 		   /* Resolvante deja connue, on relance sur le CDR */
sresolin(Ref, R, Cl, S) :- resolin([R|Ref], R, Ref).
		/* Appel recursif essentiel de la resolution lineaire */

tresolin(Ref, [A|S]) :- resolin(Ref, A, S), !. /* le backtrack */
tresolin(Ref, [A|S]) :- tresolin(Ref, S).

reslineaire(LCl) :- tresolin(LCl, LCl).

rreslineaire(LCl) :- normalise(LCl, X), reslineaire(X).

/* Bases de règles */

lregcl([], []).
lregcl([[T|Q]|R], [[Q,[T]]|C]) :- lregcl(R,C).

lfaitcl([], []).
lfaitcl([F|SF], [[[], [F]]|C]) :- lfaitcl(SF, C).

clauses(SCl) :- bagof(R, regle(R), BR), lregcl(BR, RCl),
        bagof(F, fait(F), BF), lfaitcl(BF, FCl),
        append(RCl,FCl, SCl).

regp(LButs) :- clauses(SCl), normalise([[LButs, []]|SCl], LC),
        resolution(LC).
regl(LButs) :- clauses(SCl), normalise([[LButs, []]|SCl], LC), reslineaire(LC).

