:-op(100,fy,not).
:-op(110,yfx,&).
:-op(120,yfx,v).
:-op(1200,yfx,-->).

:-dynamic
	program/3,curprog/1,symbols/1,rules/1.

%%%%%%%%%%%%%%%%%
% LOADING FILES 
%%%%%%%%%%%%%%%%%

loadfile(F):-
	(retractall(program(_,_,_)),retractall(curprog(_)),!
	 ; true),
	see(F), read_clauses, seen.

read_clauses:-
	read(C),(
	   C=end_of_file,!
	 ; C=(:- program(P)),!,
	   set_curprog(P),
	   read_clauses	   	 
	   
	 ; atomize(C,As),
	   curprog(P), 
	   program(P,Cs,Ss),
	   retractall(program(P,_,_)),
	   merge_set(As,Ss,Ts),
	   assertz(program(P,[C|Cs],Ts)),
	   read_clauses
	).

set_curprog(P):-
        (retractall(curprog(_)),! ; true),
        assertz(curprog(P)),
        (program(P,_,_),!,writelist(['Program ',P,
	                            ' has been overwritten.']),nl,
	 retractall(program(P,_,_))
	; true),
        assertz(program(P,[],[])).

newprogram(P):-
	set_curprog(P),
	read_clauses, seen.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% HT-Satisfaction
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

component(h,(Ih,_It),Ih).
component(t,(_Ih,It),It).
accessible(h,h).
accessible(h,t).
accessible(t,t).

sat_ht(I,(F & G),W) 	:- !,sat_ht(I,(F,G),W).
sat_ht(I,(F v G),W) 	:- !,sat_ht(I,(F;G),W).
sat_ht(I,(F --> G),W) 	:- !,sat_ht(I,(G:-F),W).
sat_ht(I,not F,W)   	:- !,sat_ht(I,(false:-F),W).

sat_ht(_I,true,_W)	:- !.
sat_ht(_I,false,_W)	:- !,fail.
sat_ht(I,F,W)		:- atom(F),!,component(W,I,Iw),member(F,Iw).
sat_ht(I,(F , G),W) 	:- sat_ht(I,F,W), sat_ht(I,G,W).
sat_ht(I,(F ; G),W) 	:- sat_ht(I,F,W),!; sat_ht(I,G,W).
sat_ht(I,(G :- F),W) 	:- \+ (accessible(W,W1), \+ (sat_ht_implic(I,(G :- F),W1))).

sat_ht_implic(I,(G :- F),W) :- sat_ht(I,G,W), !; \+ sat_ht(I,F,W).

modelht(I,T) :- \+ (member(F,T), \+ sat_ht(I,F,h)).

get_models(Ss,T,Ms):-bagof(M,(geninterp(Ss,M),modelht(M,T)),Ms).

geninterp([],([],[])):-!.
geninterp([P|Ps],(Ip,Ic)):-
	geninterp(Ps,(Jp,Jc)),
	(Ip=Jp    ,Ic=Jc
	;Ip=Jp    ,Ic=[P|Jc]
	;Ip=[P|Jp],Ic=[P|Jc]).

get_difference(Ss,F,G):-
	geninterp(Ss,I),modelht(I,F,FV),modelht(I,G,GV),FV \= GV.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Auxiliary operations
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

write_classes([]):-!.
write_classes([(J,Is)|L]):-
	write(J),
	(Is=[],!,write(' stable'),nl,! ; write(' >> '), writeall(', ',Is),nl),
	write_classes(L).  

writefacts([]):-!.
writefacts([F|Fs]):-
	write(F),write('.'),nl,
	writefacts(Fs).
  
included(A,B):- \+ (member(X,A), \+ member(X,B)).

lower((Ip,Jn),(Jp,Jn)):-included(Ip,Jp).

getlower(_J,[],[],[]):-!.
getlower(J,[I|Is],LowerJ,Rest):-
	getlower(J,Is,LJ,R),
	(lower(I,J),!,I=(Ip,_In),LowerJ=[Ip|LJ],Rest=R
	;LowerJ=LJ,Rest=[I|R]).

get_totals([],[],[]):-!.
get_totals([(I,I)|Ms],[(I,I)|Ts],Rs):-
	!,get_totals(Ms,Ts,Rs).
get_totals([M|Ms],Ts,[M|Rs]):-
	!,get_totals(Ms,Ts,Rs).

% classify(Totals,Classes,StableModels,Ms,Ns)
classify([],[],[],Ms,Ms):-!.
classify([(J,J)|Js],[(J,BelowJs)|Rest],SMs,Ms0,Ms):-
	getlower((J,J),Ms0,BelowJs0,Ms1),
	sort(BelowJs0,BelowJs),
	classify(Js,Rest,SMs0,Ms1,Ms),
	( BelowJs=[],!,
	  merge_set([J],SMs0,SMs)
	; SMs=SMs0).

get_subtotals(Ms,Totals,Classes,SMs,Rest):-
	get_totals(Ms,Totals0,Rest0),
	sort(Totals0,Totals),
	classify(Totals,Classes,SMs,Rest0,Rest).
	
write_program(P):-
	write('------ PROGRAM '),write(P),nl,
	program(P,Cs,_),
	repeat,(member(C,Cs),write(C),nl,fail; true),!.
  	
difference([],_,[]):-!.
difference(Xs,[],Xs):-!.
difference([X|Xs],[Y|Ys],D):-
	  X@<Y,!,difference(Xs,[Y|Ys],D0),D=[X|D0]
	; Y@<X,!,difference([X|Xs],Ys,D)
	; difference(Xs,Ys,D).

write_rules(J,K):-
	(K=[],! ; writefacts(K),nl),
	difference(J,K,D),
	repeat,
	  (
	    member(X,D),member(Y,D),\+ X=Y,
	    write(X),write(':-'),write(Y),write('.'),nl,fail
	  ; true
	  ),!.

subt(P,Classes):-
	program(P,Cs,Ss),
	get_models(Ss,Cs,Ms),
	get_subtotals(Ms,_Totals,Classes,_SMs,_Rest).

models(P,Ss):-
	write_program(P),
	program(P,Cs,Ss0),
	( Ss=Ss0,! 
	; included(Ss0,Ss),!
	; write('Signature should include at least symbols: '),
	  writeall(', ',Ss0),nl,
	  fail
	),
	(retractall(symbols(_)),! ; true),
	asserta(symbols(Ss)),
	get_models(Ss,Cs,Ms),
	get_subtotals(Ms,Totals,Classes,SMs,_Rest),
	nl,write('------ MODELS'),nl,
	write_classes(Classes),nl,
	length(Ms,Nm),write(Nm),write(' models: '),
	length(Totals,Nt),write(Nt),write(' total,'),
	length(SMs,Ns),write(Ns),write(' stable'),nl.

models(P):-
	program(P,_Cs,Ss),
	models(P,Ss).

conjunction([],true):-!.
conjunction([F],F):-!.
conjunction([F|Fs],F & G):-conjunction(Fs,G).

equiv(P1,P2):-
	program(P1,Cs1,Ss1),
	program(P2,Cs2,Ss2),
	merge_set(Ss1,Ss2,Ss),
	(retractall(symbols(_)),! ; true),
	asserta(symbols(Ss)),
	get_models(Ss,Cs1,Ms1),
	get_subtotals(Ms1,_Totals1,Classes1,SMs1,_Rest1),
	get_models(Ss,Cs2,Ms2),
	get_subtotals(Ms2,_Totals2,Classes2,SMs2,_Rest2),
	( \+ (SMs1 = SMs2),!, 
	  write('Not strongly equivalent. Different stable models.')
	; \+ (Totals1 = Totals2),!,
	  member(J,Totals1),\+ member(J,Totals2),!,
	  write('Not strongly equivalent. Add the program:'),nl,
	  writefacts(J)
	; \+ (Classes1 = Classes2),!,
	  write('Not strongly equivalent. Add the program:'),nl,
	  member((J,LJ1),Classes1), % take a difference for some total J
	  member((J,LJ2),Classes2),
	  \+ LJ1=LJ2, !, % now take some K in the difference
	  ( member(K,LJ1), \+ member(K,LJ2),!
	  ; member(K,LJ2), \+ member(K,LJ1)
	  ),
	  write_rules(J,K),
	  fail

	; write('Strongly equivalent.')
	).
	
tautology(T):-
	atomize(T,Ss),
	(geninterp(Ss,M),\+ modelht(M,T),!,
	 write('Countermodel: '),write(M),nl,fail
	; true).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% help
%%%%%%%%%%%%%%%%%%%%%%%%%%%%

help(htcheck):- 
  write('models(P)       shows models of program P.'),nl,
  write('models(P,S)     idem as models(P) but using signature S (a list of atoms).'),nl,
  write('equiv(P1,P2)    decides strong eq. of programs P1, P2.'),nl,
  write('program(P,Rs,S) stored program with name P, rules Rs, signature S.'),nl,
  write('loadfile(F)     loads all programs stored in file F. Format like:'),nl,
  write('                :-program(p1).'),nl,
  write('                p :- q, not r.'),nl,
  write('                q :- not p.'),nl,
  write('                :-program(p2).'),nl,
  write('                a :- not b.'),nl,
  write('                ...'),nl,
  write('newprogram(P)   defines a new program entering rule by rule and'),nl,
  write('                ending with Ctrl-D in an empty line.'),nl.
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% To delete a given "subtotal" model (H,T) add the rule
%    not p1;p1; ...; not pn;pn :- q1, ...,qm, not r1, ..., not rk.
% where
%    H={q1, ...,qm}
%    T-H= {p1, ...,pm}
%    Sigma-T = {r1, ..., rk}
% When H=T, just add the rule
%   false :- q1,...,qm, not r1,..., not rk.

lit(0,X,X):-!.
lit(1,X,not X):-!.
build_clause(_Op,V,[X],L):-!, lit(V,X,L).
build_clause(',',V,[X|Xs], (L , C) ):-!, lit(V,X,L),build_clause(',',V,Xs,C).
build_clause(';',V,[X|Xs], (L ; C) ):-!, lit(V,X,L),build_clause(';',V,Xs,C).	

commas([X],X):-!.
commas([X|Xs],(X,Ys)):-commas(Xs,Ys).

semis([X],X):-!.
semis([X|Xs],(X;Ys)):-semis(Xs,Ys).

negs([],[]):-!.
negs([X|Xs],[not X|Ys]):-negs(Xs,Ys).
  
build_rule(HPs,HNs,BPs,BNs,R):-
	negs(HNs,HNs1),
	append(HPs,HNs1,Hs),
	( Hs=[],!,Head=false
	; semis(Hs,Head)
	),
	negs(BNs,BNs1),
	append(BPs,BNs1,Bs),
	( Bs=[],!,R=Head
	; commas(Bs,Body),
	  R=(Head :- Body)
	).

build_differences(I,Negs,Js):-
	repeat,
	(
	  get_subset(I,J), \+ I=J,
	  \+ member(J,Js),
	  difference(I,J,K),
	  build_rule(K,K,J,Negs,R),
	  add_rule(R),
	  fail
	; true),!.


build_class(Ss,I,Cs):-
	sort(I,I1),
	difference(Ss,I1,Negs),
	(
	  member((I,Js),Cs),!,
	  build_differences(I,Negs,Js)
	; build_rule([],[],I,Negs,R),
	  add_rule(R)
	).

add_rule(R):-
	rules(Rs),
	(retractall(rules(_)),! ; true),
	append(Rs,[R],Qs),
	asserta(rules(Qs)).
	  
construct(P):-
	models(P),
	nl,
	write('Generated strongly equivalent program'),nl,nl,
	program(P,_Cs,Ss),
	(retractall(symbols(_)),! ; true),
	asserta(symbols(Ss)),
	(retractall(rules(_)),! ; true),
	asserta(rules([])),
	subt(P,Classes),
	repeat,
	( get_subset(Ss,I),
	  build_class(Ss,I,Classes),fail
	; true
	),!,
	rules(Rs),
	repeat, (member(R,Rs),write(R),nl,fail;true),!.

get_subset([],[]):-!.

get_subset([X|Xs],S):-
	get_subset(Xs,R), 
	(S=R; S=[X|R]).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Display operations
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
writelist([]):-!.
writelist([A|As]):-write(A),writelist(As).

writeall(_Sep,[]):-!.
writeall(_Sep,[X]):-!, write(X).
writeall(Sep,[X|L]):-
  write(X),write(Sep),
  writeall(Sep,L).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Atomizing a expression
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

atomize(true,[]):-!.
atomize(false,[]):-!.
atomize(T,As):-
	T =.. [F|Args],
	(Args=[],!,As=[F] ;atomize_args(Args,As) ).
atomize_args([],[]):-!.
atomize_args([F|Fs],Cs):-
	atomize(F,As),atomize_args(Fs,Bs),merge_set(As,Bs,Cs).

:-nl,nl,write('For help on this program type help(htcheck)'), nl,nl.
:-loadfile('prog1.p').





