:-op(130,fy,~).
:-op(130,fy,neg).
:-op(130,fy,not).
:-op(130,fy,nec).
:-op(130,fy,pos).
:-op(140,yfx,&).
:-op(150,yfx,v).
:-op(160,xfx,/=).
:-op(160,xfx,<->).

:-dynamic
	program/3,curprog/1.

:-dynamic
	verbose/0.
	
verbose.
	
/*** GENERAL OPERATIONS **********************************************/

atomize(undef,[]):-!.
atomize(true,[]):-!.
atomize(false,[]):-!.
atomize(0,[]):-!.
atomize([t,_],[]):-!.
atomize([f,_],[]):-!.
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).

included(A,B):- \+ (member(X,A), \+ member(X,B)).

passfilter(_P,[],[],[]):-!.
passfilter(P,[X|L],A,B):-
	passfilter(P,L,A0,B0),
	% construct term P(X)
	functor(PX,P,1),arg(1,PX,X),
	( call(PX),!,!,A=[X|A0],B=B0
	; A=A0, B=[X|B0]).

list_to_conjunction([F],F):-!.
list_to_conjunction(L,F):-l2c(L,true,F).
l2c([],F,F):-!.
l2c([F|Fs],true,H):-!,l2c(Fs,F,H).	
l2c([F|Fs],G,H):-!,l2c(Fs,G & F,H).	

/*** LOADING FILE ****************************************************/

loadfile(F):-
        write('Loading file '),write(F),nl,
 	(retractall(program(_,_,_)),retractall(curprog(_)),!
	 ; true),
	see(F), read_clauses, seen,
        findall(X,program(X,_Y,_Z),Xs),length(Xs,N),
        write(N),write(' programs loaded.'),nl.


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.

/*** INTERPRETATIONS *************************************************/

gen_subset([],[]):-!.
gen_subset([X|Xs],Zs):-
	gen_subset(Xs,Ys),
	(Zs=Ys;Zs=[X|Ys]).

gen_interp(ht2,Ps,[[HH,HT],[TH,TT]]):-
	  gen_subset(Ps,TT), gen_subset(TT,TH),
	  gen_subset(TT,HT), intersection(HT,TH,I), gen_subset(I,HH).

component([[HH,HT],[TH,TT]],W,C):-
	  W=hh,!,C=HH
	; W=ht,!,C=HT
	; W=th,!,C=TH
	; W=tt,!,C=TT
	; W=h,!,C=[HH,HT]
	; W=t,!,C=[TH,TT].
		
total([X,X]).	

world(hh).
world(ht).
world(th).
world(tt).

% transforms a world in the list of its components
% example: world(ht,X) returns X=[h,t]
world(W,[X,Y]):- 
	string_to_atom(S,W),
	string_to_list(S,[A,B]),
	string_to_atom([A],X),
	string_to_atom([B],Y).

access(h,t).
access(X,X):-member(X,[h,t]).

accessb(h,t).
accessb(t,h).

:-dynamic access2/2. % access2 predicate can be overwritten.


access1(W,W1):- world(W,[X,Y]), world(W1,[X1,Y1]),
		access(X,X1), access(Y,Y1).
access2(W,W1):- world(W,[X,Y]), world(W1,[X1,Y1]),
		access(X,X1), accessb(Y,Y1).

/* Replacing R2 (access2) by R1.R2 also captures WFS, but relations among modal operators do not vary w.r.t the original R */

%access12(W,W2):- world(W1), access1(W,W1), access2(W1,W2),!.
%access21(W,W2):- world(W1), access2(W,W1), access1(W1,W2),!.
%access121(W,W2):- world(W1), access12(W,W1), access1(W1,W2),!.
%access212(W,W2):- world(W1), access21(W,W1), access2(W1,W2),!.

access_star(W,W2):-world(W1),access2(W,W1),access1(W2,W1).
access_1_star(W1,W2):-world(W1),world(U),world(W2),
	access1(W1,U),access_star(U,W2).

/*** HT² SATISFACTION OF FORMULAS ****************************************/

  % Logical syntax
  (I,W) /= (F -> G)	:- !,(I,W) /= (G :- F).
  (I,W) /= (F & G)	:- !,(I,W) /= (F , G).
  (I,W) /= (F v G)	:- !,(I,W) /= (F ; G).
  
  % Some derived operators
  (I,W) /= (F <-> G)	:- !,(I,W) /= (F -> G) & (G -> F).
  (I,W) /= (- F)	:- !,(I,W) /= (F -> false).
  (I,W) /= (neg F)	:- !,(I,W) /= (F -> false).
             % warning: intuitionistic negation -F doesn't work as explicit negation
             % (see example p27)

  % Satisfaction of formulae using LP syntax
  (_I,W) /= undef	:- !,member(W,[ht,tt]).
     _M /= true 	:- !.
     _M /= false 	:- !,fail.
  (I,W) /= A		:- (atom(A),!; A= ~B,atom(B)),!,
                           component(I,W,IW),member(A,IW).
      M /= (F , G)	:- M /= F, M /= G.
      M /= (F ; G)	:- M /= F,!; M /= G.
  (I,W) /= not F	:- \+ (world(W1),access2(W,W1),(I,W1) /= F).
  (I,W) /= (F :- G)	:- \+ (world(W1),access1(W,W1),(I,W1) /= G,
                             \+ ((I,W1) /= F)).			       

%  (I,W) /= nec F :- \+ (world(W1),access1(W,W1),world(W2),access2(W1,W2),
%                               \+ (I, W2) /= F
%			).
   
%  (I,W) /= pos F :- \+ (world(W1),access1(W,W1), \+ someaccess2(I,W1,F)).
/* Relation R1.R2 (acces12) doesn't work: modal operators are not hereditary.
       (I,W) /= nec F :- \+ (world(W1),access12(W,W1),\+ (I, W1) /= F).
       (I,W) /= pos F :- world(W1),access12(W,W1), (I,W1) /= F.
*/

% someaccess2(I,W1,F):- 
%	world(W2),access2(W1,W2),(I,W2) /= F,!.
	

/*** COMPUTING PROGRAM MODELS **********************************************/

model(ht2,M,T) :- \+ (member(F,T),\+ (M /= F)).

models(ht2,Ss,T,Ms):-
	bagof(I,(gen_interp(ht2,Ss,I), model(ht2,(I,hh),T)),Ms).

is_minimal(h,[H,T],Ms):- \+ (member([H2,T],Ms), \+ subset(H,H2)).
is_minimal(t,[H,T],Ms):- \+ (member([H,T2],Ms), \+ subset(T,T2)).

write_info([],_):-!.
write_info([M|R],Ms):-
	write(M),
	(is_minimal(h,M,Ms),!,write(' H-minimal ');true),
	(is_minimal(t,M,Ms),!,write(' T-minimal ');true),
	nl,
	write_info(R,Ms).	

compute(P,Sem,Ss):-
  program(P,Clauses,_Symbols),
  models(Sem,Ss,Clauses,Models),
  length(Models,N1),
  write(N1), write(' models'),nl,
  ( Sem=l3,!,
    write_info(Models,Models)
  
  ; passfilter(total,Models,Totals0,Ns),
    sort(Totals0,Totals),
    partition(Totals,TotalsExt,Ns,Rest),
    length(Totals,N2),
    write(N2), write(' total models:'),nl,
    writepairs(1,TotalsExt),nl,
    length(Rest,N3),
    write(N3), write(' models that are not subtotal: '),nl,
    write_models(Rest)
  ).

strictly_lower([H,H1],[T,T1]):-
	  member(X,T), \+ member(X,H), !
	; member(X,T1), \+ member(X,H1).

not_in_equilibrium(T,T1,Clauses):-
    % get a smaller model
    gen_subset(T1,H1),intersection(H1,T,I),gen_subset(I,H),
    strictly_lower([H,H1],[T,T1]),
    model(ht2,([[H,H1],[T,T1]],hh),Clauses),!.

pemodels(P) :-
  program(P,Clauses,Symbols),
  repeat,(
    % get a total interpr. ((T,T1),(T,T1))
    gen_subset(Symbols,T1), gen_subset(T1,T), 
    % check if it is a total model
    model(ht2,([[T,T1],[T,T1]],hh),Clauses), 
    \+ not_in_equilibrium(T,T1,Clauses),
    write_belief_set([T,T1]),nl,fail
    
    ; true
  ),!.

equiv(P,Q) :-
  program(P,P1,Ss),
  program(Q,Q1,Ss1),
  merge_set(Ss,Ss1,Ss2),
  gen_interp(ht2,Ss2,I), 
  ( model(ht2,(I,hh),P1), \+ model(ht2,(I,hh),Q1),!,
    write_model(I),
    write(' model of '),write(P),write(' but not of '),write(Q),nl,fail
  ; model(ht2,(I,hh),Q1), \+ model(ht2,(I,hh),P1),!,
    write_model(I),
    write(' model of '),write(Q),write(' but not of '),write(P),nl,fail
  ).
  
equiv(_,_).
  
  
compute(P):- compute(P,ht2).

compute(P,Sem) :-
  program(P,_Cs,Ss),
  compute(P,Sem,Ss).
  
lower([[HH1,HT1],T],[[HH2,HT2],T]):-
	included(HH1,HH2),
	included(HT1,HT2).

partition([],[],Ps,Ps):-!.
partition([Q|Qs],[(Q,LowerQ)|Pairs],Ps0,PsN):-
	getlower(Q,Ps0,LowerQa,Ps1),
	sort(LowerQa,LowerQ),
	partition(Qs,Pairs,Ps1,PsN).

getlower(_Q,[],[],[]):-!.
getlower(Q,[P|Ps],LowerQ,Rest):-
	getlower(Q,Ps,LQ,R),
	(lower(P,Q),!,LowerQ=[P|LQ],Rest=R
	;LowerQ=LQ,Rest=[P|R]).

/*** COMPARING FORMULAS **********************************************/

getht2model(As, F, (I,W)):- 
	gen_interp(ht2,As,I), world(W), model(ht2,(I,W),[F]).

equivalent(F1,F2):-
	% get common signature
	atomize(F1,As1),
	atomize(F2,As2),
	merge_set(As1,As2,As),
	( getht2model(As,F1,M),
	  \+ model(ht2,M,[F2]),!,A=F1,B=F2
	  
	; getht2model(As,F2,M),
	  \+ model(ht2,M,[F1]),!,A=F2,B=F1
	),
	write(M),nl,
	write(' model of ('),write(A),
	write(') but countermodel of ('),write(B),write(')'),nl,
	fail.
	
equivalent(_F1,_F2).
	
entails(F1,F2):-
	% get common signature
	atomize(F1,As1),
	atomize(F2,As2),
	merge_set(As1,As2,As),
	getht2model(As,F1,M), \+ model(ht2,M,[F2]),!,
	write(M),nl,
	write(' model of ('),write(F1),
	write(') but countermodel of ('),write(F2),write(')'),nl,
	fail.
	
entails(_F1,_F2).	

tautology(F) :-
	atomize(F,As),
	gen_interp(ht2,As,I),world(W),\+ model(ht2,(I,W),[F]),!,
	verbose,write('Countermodel: '),write((I,W)),nl,fail.
tautology(_F).
	
/*** PRINT 6-VALUED TABLES *******************************************/

convert('00',' 0').
convert('01',' 1').
convert('11',' 2').
convert('02',' 3').
convert('12',' 4').
convert('22',' 5').

get_value(I,F,V):-
	(  (I,hh) /= F, !, V1=2,V2=2
	 ; \+ ((I,tt) /= F),!,V1=0,V2=0
	 ; ((I,ht) /= F,!,V1=1; V1=0),
	   ((I,th) /= F,!,V2=2; V2=1)
	 ),concat_atom([V1,V2],V).

join_components([H1,T1],[H2,T2],[H3,T3]):-
	merge_set(H1,H2,H3),merge_set(T1,T2,T3).
join_interps([H1,T1],[H2,T2],[H3,T3]):-
	join_components(H1,H2,H3),
	join_components(T1,T2,T3).


print_table_unary(P,F):-
	findall(I,gen_interp(ht2,[P],I),IPs),
	write('    | '),nl,
	write('----+----'),nl,
	repeat,
	  (
	    member(Ip,IPs), 
	    get_value(Ip,P,Vp),
	    write(' '),write(Vp),write(' | '),
	    get_value(Ip,F,VF), write(VF), nl, fail
	  ; true
	  ),!.

print_row(P,F,Ip,IQs):-
	get_value(Ip,P,Vp),
	write(' '),write(Vp),write(' | '),
	repeat,
	  (
	    member(Iq,IQs),
	    join_interps(Iq,Ip,I),
	    get_value(I,F,VF),
	    write(VF),write(' '),
	    fail
	  ; true
	  ),!.

print_table_binary(P,Q,F):-
	findall(I,gen_interp(ht2,[P],I),IPs),
	findall(J,gen_interp(ht2,[Q],J),IQs),
	write('    | '),
	repeat,
	  (
	    member(Iq,IQs), get_value(Iq,Q,Vq), write(Vq),write(' '), fail
	  ; true
	  ),!,
	nl,
	write('----+------------------'),nl,
	repeat,
	  (
	    member(Ip,IPs), print_row(P,F,Ip,IQs), nl, fail
	  ; true
	  ),!.

print_table(F):-
	atomize(F,As),
	(As=[P],!,print_table_unary(P,F)
	;As=[P,Q],!,print_table_binary(P,Q,F)
	; As=[],!,
	  write('The formula must depend on at least 1 variable.'),nl,fail
	; write('The formula must depend on at most 2 variables,'),nl,
	  write('Current variables: '),writelist(As),nl,
	  fail
	).

/*** BACK AND FORTH **************************************************/

reduct([],_I,[]):- !.
reduct([F|Fs],I,[FI|FsI]):- !,reduct(F,I,FI), reduct(Fs,I,FsI).

reduct(not P,I,false) :- member(P,I),!.
reduct(not _P,_I,true) :- !.
reduct(P,I,PI):-
	P =.. [F|Args],
	reduct(Args,I,Args1),
	PI=.. [F|Args1].

sat(_I,[]):-!.
sat(I,[F|Fs]):-!, sat(I,F),sat(I,Fs).

sat(I,F -> G) :- !, sat(I, (neg F ; G)).
sat(I, (G :- F)) :- sat(I, (neg F ; G)).
sat(I,F & G) :- !, sat(I, (F,G)).
sat(I,F v G) :- !, sat(I, (F;G)).
sat(I,F <-> G) :- !, sat(I, (F -> G) & (G -> F)).
sat(I,(- F)) :- !, sat(I, (neg F)).

sat(_I,true) :- !.
sat(_I,false) :- !, fail.
sat(I,A) :- atom(A),!,member(A,I).
sat(I,(F , G))	:- sat(I,F), sat(I,G).
sat(I,(F ; G))	:- sat(I,F),!; sat(I,G).
sat(I,(neg F))	:- \+ sat(I,F).

minmodel(I,P):-
  sat(I,P), 
  \+ (gen_subset(I,J), J \= I, sat(J,P)).
  
back_and_forth(Pnum):-
  program(Pnum,P,Symbols),
  repeat,
    (
      gen_subset(Symbols,T),
      gen_subset(T,H),  %       nl, write((H,T)),nl,
      reduct(P,T,PT),
      minmodel(H,PT),  % write(PT),nl,
      reduct(P,H,PH),
      minmodel(T,PH),  % write(PH),nl,
      write([H,T]),nl,fail
    ; true),!.

/*** WFSX ************************************************************/

opposite(~A,A):-!.
opposite(A,~A).
seminormal([],[]):-!.
seminormal([R|Rs],[G|Gs]):-!,seminormal(R,G),seminormal(Rs,Gs).
seminormal((H :- B),(H :- not NH,B)):- !,opposite(H,NH).
seminormal(H,(H :- not NH)):- !,opposite(H,NH).

tp([],_I,[]):-!.
tp([(H :- B)|Cs],I,K):-!,tp(Cs,I,J),( sat(I,B),!,merge_set([H],J,K) ; K=J ).
tp([ H      |Cs],I,K):-!,tp(Cs,I,J),merge_set([H],J,K).
iterate_tp(P,I,K):-tp(P,I,J),( J=I,!,K=I ; iterate_tp(P,J,K) ).

iterate_wfsx(P,Psemi,I,W):-
	reduct(Psemi,I,PsI),
	iterate_tp(PsI,[],J),	
	reduct(P,J,PJ),
	iterate_tp(PJ,[],K),
	( K=I,!,W=(K,J) ; iterate_wfsx(P,Psemi,K,W)).
	
wfsx(PNum):-
	program(PNum,P,_),
	seminormal(P,Psemi),
	iterate_wfsx(P,Psemi,[],W),
	write(W),nl.

/*** PARTIAL STABLE MODELS *******************************************/

val3(_I,true,2) :- !.
val3(_I,false,0) :- !.
val3(_I,undef,1) :- !.
val3(_I,2,2) :- !.
val3(_I,0,0) :- !.
val3(_I,1,1) :- !.

val3((H,T),A,V) :- atom(A),!,
	( member(A,H),!,V=2
	; member(A,T),!,V=1
	; V=0).

val3(I, (G :- F), V) :- !, val3(I, (F -> G), V).
val3(I, (F,G), V) :- !, val3(I, (F & G), V).
val3(I, (F;G), V) :- !, val3(I, (F v G), V).
val3(I,(F <-> G),V) :- !, val3(I, ((F -> G) & (G -> F)), V).

val3(I,(F -> G), V) :- !, val3(I,F,VF),val3(I,G,VG),(VG >= VF,!,V=2; V=0).
val3(I,(F & G), V) :- !, val3(I,F,VF),val3(I,G,VG),orderval(VF,VG,V,_).
val3(I,(F v G), V) :- !, val3(I,F,VF),val3(I,G,VG),orderval(VF,VG,_,V).
val3(I,(not F), V) :- !,val3(I,F,VF),V is 2-VF.

orderval(X,Y,X,Y):- Y>=X,!.  
orderval(X,Y,Y,X).  

reduct3([],_I,[]):- !.
reduct3([F|Fs],I,[FI|FsI]):- !,reduct3(F,I,FI), reduct3(Fs,I,FsI).

reduct3(not P,I,V) :- !,val3(I,(not P),V).
reduct3(P,I,PI):-
	P =.. [F|Args],
	reduct3(Args,I,Args1),
	PI=.. [F|Args1].
	
sat3(_I,[]):-!.
sat3(I,[F|Fs]):-!, sat3(I,F),sat3(I,Fs).
sat3(I,F):-val3(I,F,V),V=2.

gen_strictly_lower((T,T1),(H,H1)):-
	gen_subset(T1,H1),
	intersection(T,H1,A),
	gen_subset(A,H),
	(H,H1) \= (T,T1).

is_minimal(I,P):- \+ (gen_strictly_lower(I,J),sat3(J,P)).

psmodels(Pnum):-
  program(Pnum,P,Symbols),
  repeat,
    (
      gen_subset(Symbols,T1),
      gen_subset(T1,T),         % nl, write((T,T1)),nl,
      reduct3(P,(T,T1),PT),     % write(PT),nl,nl,nl,
      sat3((T,T1),PT),
      is_minimal((T,T1),PT),
      write([T,T1]),nl,fail
    ; true),!.


/*** INFINITE VALUED SEMANTICS  **************************************/

:- dynamic range/3, maxlen/0.


initialize_ranges(Maxlen,Ps) :-
  (retractall(maxlen(_)),!;true),assertz(maxlen(Maxlen)),
  (retractall(range(_,_,_)),!;true),
  Max is 2*(Maxlen+1),
  repeat,
    ( member(P,Ps), assertz(range(P,0,Max)), fail
    ; true),!.

update_ranges(T) :-
  repeat,(member(F,T), update_range(F), fail ; true),!.

update_range( (A :- Val) ) :-
  atom(A),val2int(Val,V),!,range(A,Min,Max),
  (Min>=V,!; retractall(range(A,Min,Max)), assertz(range(A,V,Max))).
update_range( (Val :- A) ) :-
  atom(A),val2int(Val,V),!,range(A,Min,Max),
  (V>=Max,!; retractall(range(A,Min,Max)), assertz(range(A,Min,V))).


val2int([f,N],N):-!.
val2int(0,I):-!, maxlen(Maxlen),I is Maxlen+1.
val2int([t,N],I):-!, maxlen(Maxlen), I is 2*(Maxlen+1)-N.
int2val(I,[f,I]):- maxlen(Maxlen), Maxlen>=I,!.
int2val(I,0):- maxlen(Maxlen), I is Maxlen+1,!.
int2val(I,[t,N]):- maxlen(Maxlen), N is 2*(Maxlen+1)-I.
	
gen_ivinterp([],[]) :- !.
gen_ivinterp([P|Ps],[[P,V]|Is]) :-
	range(P,Min,Max),
	numlist(Min,Max,Values),
	member(I,Values),
	int2val(I,V),
	gen_ivinterp(Ps,Is).

ival(_I,true,[t,0]) :- !.
ival(_I,false,[f,0]) :- !.
ival(_I,[t,N],[t,N]) :- !.
ival(_I,[f,N],[f,N]) :- !.
ival(_I,0,0) :- !.

ival(I,A,V) :- atom(A),!,member([A,V],I).

ival(I, (G :- F), V) :- !, ival(I, (F -> G), V).
ival(I, (F,G), V) :- !, ival(I, (F & G), V).
ival(I, (F;G), V) :- !, ival(I, (F v G), V).
ival(I,(F <-> G),V) :- !, ival(I, ((F -> G) & (G -> F)), V).

ival(I,(F -> G), V) :- !, ival(I,F,VF),ival(I,G,VG),(geq(VG,VF),!,V=[t,0]; V=VG).
ival(I,(F & G), V) :- !, ival(I,F,VF),ival(I,G,VG),iorderval(VF,VG,V,_).
ival(I,(F v G), V) :- !, ival(I,F,VF),ival(I,G,VG),iorderval(VF,VG,_,V).
ival(I,(not F), V) :- !,ival(I,F,VF),
	( VF=[t,N],!,N1 is N+1, V=[f,N1]
	; VF=[f,N],!,N1 is N+1, V=[t,N1]
	; V=0).

geq(X,Y) :- val2int(X,X1),val2int(Y,Y1),X1>=Y1.

iorderval(X,Y,X,Y):- geq(Y,X),!.  
iorderval(X,Y,Y,X).  

infmodulo(_I,[],[]):-!.

ivmodel(I,T) :- \+ (member(F,T), ival(I,F,V), V\=[t,0]).

ivmodels(Pnum):-ivmodels(0,Pnum).

ivmodels(Maxlen,Pnum):-
  program(Pnum,P,Symbols),
  (Maxlen=0,!, length(Symbols,N), Maxlen1 is N-1; Maxlen1=Maxlen),
  initialize_ranges(Maxlen1,Symbols),
  /*update_ranges(P),*/
  findall(K,(gen_ivinterp(Symbols,K),ivmodel(K,P)), Is),
  repeat,
    (
      member(I,Is),
      \+ (member(J,Is), J \= I, ileq(0,Maxlen1,J,I) ),
      transform_values(I,I1),
      writelist(I1),nl,fail
    ; true),!.

ivmodulo([],_I,[]):-!.
ivmodulo([(H :- B) | P],I,[(H :- BI)|PI]):-!,ivmodulo(P,I,PI),ivmodulo(B,I,BI).
ivmodulo([H|P],I,[H|PI]):-!,ivmodulo(P,I,PI).
ivmodulo((A,B),I,(AI,BI)):-!,ivmodulo(A,I,AI),ivmodulo(B,I,BI).
ivmodulo(not A,I,V):-!,ival(I,not A,V).
ivmodulo(A,_I,A).

ivstable(Pnum):-
  program(Pnum,P,Symbols),
  length(Symbols,N), N1 is N-1,
  numlist(0,N1,Ns),
  repeat,
    (
      gen_ivinterp(Ns,Symbols,I),
      ivmodel(I,P),
      ivmodulo(P,I,PI),
      \+ (gen_ivinterp(Ns,Symbols,J),J \= I,ileq(0,N1,J,I),ivmodel(J,PI)),
      transform_values(I,I1),
      writelist(I1),nl,fail
     ; true),!.


test(Pnum):-
  program(Pnum,P,Symbols),
  length(Symbols,N), N1 is N-1,
  numlist(0,N1,Ns),
  findall(K,(gen_ivinterp(Ns,Symbols,K),ivmodel(K,P)), Is),
  repeat,
    (
      member(I,Is), % pick a model
      ivmodulo(P,I,PI),
      % get all the strictly smaller models
      findall(W,(gen_ivinterp(Ns,Symbols,W),W \= I,ileq(0,N1,W,I), ivmodel(W,PI)), Ws),
      Ws \= [], % check we have some, that is, I is not minimal for P^I
      write('-----'),nl,
      transform_values(I,I1),
      writelist(I1),write(' <---'),nl,
      
      member(Z,Ws),ivmodel(Z,P),
      transform_values(Z,Z1),
      writelist(Z1),nl,
      fail
    ; true),!.


ileq(N,MAX,_,_) :- N>MAX,!.	
ileq(N,MAX,I,J) :-
	findall([X,[V,N]],member([X,[V,N]],I),IN),
	findall([Y,[W,N]],member([Y,[W,N]],J),JN),
	( IN=JN,!, N1 is N+1, ileq(N1,MAX,I,J)
	; findall(X1,member([X1,[t,N]],IN),ItN),
	  findall(Y1,member([Y1,[t,N]],JN),JtN),
	  subset(ItN,JtN), 
	  findall(X2,member([X2,[f,N]],IN),IfN),
	  findall(Y2,member([Y2,[f,N]],JN),JfN),
	  subset(JfN,IfN)
	).


transform_values([],[]):-!.
transform_values([[X,V]|Ps],[W|Qs]):-
	( V=0,!,concat_atom(['(',X,',',0,')'],W)
	; V=[U,N],!,concat_atom(['(',X,',',U,N,')'],W)
	),transform_values(Ps,Qs).

	
/*** DISPLAY *********************************************************/

writelist([],_):-!.
writelist([X],_):-!,write(X).
writelist([X|L],Separator):-
  write(X),(Separator=nl,!,nl; write(Separator)),
  writelist(L,Separator).

writelist(L):-writelist(L,',').

write_belief_set([H,T]):- 
	write('({'),
	writelist(H,','),
	write('},{'),
	writelist(T,','),
	write('})').

write_model([Bh,Bt]):-
	write('   ( '),write_belief_set(Bh),write(' , '),write_belief_set(Bt), write(' )').

write_belief_sets([]):-!.
write_belief_sets([M|Ms]):-
	write_belief_set(M),nl,
	write_belief_sets(Ms).

write_models([]):-!.
write_models([M|Ms]):-
	write_model(M),nl,write_models(Ms).

writepairs(_,[]):-!.
writepairs(N,[(Q,Ps)|L]):-
/*	( Ps=[],!,Q=[_,Bt],write('Bh = Bt = '),write_belief_set(Bt),nl
	; true),
	writepairs(M,L).
*/
	write(N),write(') '),
	Q=[_,Bt],write('Bh = Bt = '),write_belief_set(Bt),
	( Ps=[],!,write('  *** Partial Stable Model'),! 
	; nl,  write_models(Ps)
	),nl,
	M is N + 1,
	writepairs(M,L).  

/*** INITIALIZATION ************************************************/

help:- 
  nl,
  write('--- Dealing with formulas -------'),nl,
  write('equivalent(F,G) decides whether formulas F and G are semantically equivalent.'),nl,
  write('entails(F,G)    decides whether F (semantically) entails G.'),nl,
  write('tautology(F)    decides whether F is a tautology.'),nl,
  write('print_table(F)  prints the corresponding 6-valued table for F.'),nl,
  write('                Note: F must depend either on 1 or 2 variables.'),nl,
  nl,
  write('--- Dealing with predefined programs -------'),nl,
  write('pemodels(P)       shows the partial eq. models of program P.'),nl,
  write('psmodels(P)       shows the partial stable models of program P.'),nl,
  write('back_and_forth(P) shows the Back&Forth models of program P.'),nl,
  write('ivmodels(P)       shows the infinite valued models of program P.'),nl,
  write('minivmodels(P)    shows the minimal infinite valued models of program P.'),nl,
  write('wfsx(P)           computes the WF model under WFSX (~ is strong neg.)'),nl,
write('equiv(P,Q)        Decides whether P and Q have the same models.'),nl,
  write('compute(P)        shows all models of program P classified by their
   "there" belief pair.'),nl,
  write('program(P,Rs,S)   retrieves stored program with name P, rules Rs, signature S.'),nl,
  write('loadfile(F)       loads all programs stored in file F (see example file prog1.p).'),nl,
  write('newprogram(P)     defines a new program entering rule by rule and'),nl,
  write('                  ending with Ctrl-D in an empty line.'),nl,
  nl,
  write('Operators       meaning'),nl,
  write('----------------------------------------'),nl,
  write(' ,    &         conjunction '),nl,
  write(' ;    v         disjunction '),nl,
  write(' not            WF negation'),nl,
  write(' neg  -         intuitionistic negation'),nl,
  write(' ->             implication'),nl,
  write(' :-             (reverse) implication'),nl,
  write(' <->            double implication'),nl.

  

:- write('Type "help." for a list of predicates and their use.'),nl.

:- loadfile('prog1.pl').
