:-op(200,fy,not).
:-op(210,xfy,&).
:-op(220,xfy,x).
:-op(230,xfy,v).

:- consult('backend.pl').

:- dynamic numprefs/1, auxatom/1, debug/0, maxdegree/1.

numprefs(0).

prefcode(X) :- numprefs(X), retractall(numprefs(X)), X1 is X+1, asserta(numprefs(X1)).

lpod(F,Ordering) :-
	loadfile(F,P),
	(retractall(numprefs(_)),!;true),asserta(numprefs(0)),
	(retractall(auxatom(_)),!;true),
	(retractall(maxdegree(_)),!;true),asserta(maxdegree(1)),
	signature(P,S),
	gen_program(P,Gen),
	answersets(Gen,1,Ys),Ys=[M0],
	(debug,!,write('Found model '),write(M0),nl; true),
	improve(S,Gen,Ordering,M0,M),!,
	( debug,!,write('Optimal model:'),write(M),nl
	; findall(A,(member(A,M), \+ A=r(_,_)),As), write(As),nl
	).
	
improve(S,Gen,Ordering,M0,M):-
	% Test optimality
	findall(aux_o(R,I),member(r(R,I),M0),Os),
	maxdegree(MD),get_numbers(MD,DDs),findall(aux_degree(Z),member(Z,DDs),Zs),
	numprefs(NP),get_numbers(NP,PPs),findall(aux_rule(W),member(W,PPs),Ws),Ws1=[aux_rule(0)|Ws],
	append_all([Gen,Os,Zs,Ws1],P),
	concat_atom(['tester',Ordering,'.pl'],Tester),
	answersets(P,[Tester],1,Xs),
	% write_lines(P),nl,
	( Xs=[], !, M=M0  % optimal model found
	; Xs=[X],        % we found a better model
	  (debug,!,write('Found model '),write(X),nl; true),
	  findall(not A, (member(A,S), \+ member(A,M0)), NOTS),
	  append(NOTS,M0,M1),
	  binop(',',M1,Body), % add a constraint forbidding model M0
	  append(Gen,[( :- Body)],Gen1),
	  improve(S,Gen1,Ordering,X,M)
	).
	
gen_program(P,Rs):-
	classify_rules(P,Prefs,Rules),
	translate_prefs(Prefs,Rules1),
	findall((NA :- not A),(auxatom(A),get_auxatom(A,NA)),Rules2),
	append_all([Rules,Rules1,Rules2],Rs).
		
% Separate preference rules Ps from ordinary rules Os
classify_rules([],[],[]):-!.
classify_rules([R|Rs],[(Code,R)|Ps],Os) :-	(R = (_ x _), !; R=((_ x _) :- _) ),!, prefcode(Code), classify_rules(Rs,Ps,Os).
classify_rules([R|Rs],Ps,[R|Os]) :- classify_rules(Rs,Ps,Os).

translate_prefs([],[]):-!.
translate_prefs([P|Ps],Rs):-translate_pref(P,Rs0), translate_prefs(Ps,Rs1), append(Rs0,Rs1,Rs).

% Translate a preference rule (Code,R) into a set of rules Rs
translate_pref( (Code, R), [R0, (r(Code,1) :- not aux_body(Code)) |Rs]):-
	( R=(H :- B),!, R0=(aux_body(Code) :- B), B1=[aux_body(Code)]
	; H=R, R0=aux_body(Code), B1=[]
	),
	bin_to_list('x',H,H1),update_maxdegree(H1),
	t_pref(1,Code,H1,B1,Rs).

update_maxdegree(L) :- length(L,D), maxdegree(M), (D>M,!,retractall(maxdegree(_)), asserta(maxdegree(D)); true).

get_numbers(1,[1]):-!.
get_numbers(N,[N|L]):-N1 is N-1, get_numbers(N1,L).

t_pref(_W,_Code,[],B,[R]) :- !, body_list_to_rule( ( :- B), R ).
t_pref(W,Code,[A|As],B,[R1,R2|Rs]) :-
	!,
	get_auxatom(A,NA),
	Body=[not NA|B],
	body_list_to_rule( (A :- Body), R1),
	body_list_to_rule( (r(Code,W) :- Body), R2),
	W1 is W+1,
	t_pref(W1,Code,As,[not A|B],Rs).

get_auxatom(-A,NA):- !,concat_atom(['aux_neg_',A],NA), (auxatom(-A),!; assertz(auxatom(A))).
get_auxatom(A,NA):- concat_atom(['aux_',A],NA), (auxatom(A),!; assertz(auxatom(A))).

body_list_to_rule((H :- []), H):-!.
body_list_to_rule((H :- B), (H :- B1)):-!,binop(',',B,B1).
body_list_to_rule(( :- B), ( :- B1)):-!,binop(',',B,B1).

signature([],[]):-!.
signature([R|Rs],S):-!,signature(R,S0), signature(Rs,S1), merge_set(S0,S1,S).
signature(G,S):- G =.. [F,A,B],	member(F,[':-','x',',']),!,
	signature(A,SA), signature(B,SB), merge_set(SA,SB,S).
signature(not G,S):-!,signature(G,S).
signature(P,[P]).

%%% Auxiliary predicates

% binop(F,L,T) - constructs a term T by successive applications 
% of binary functor F to all elements in (nonempty) list L
binop(_F,[X],X):-!.
binop(F,[X|L],T):-binop(F,L,T0),T =.. [F,X,T0].

bin_to_list(F,Term,L) :- Term =.. [F,A,B], !,bin_to_list(F,A,LA),bin_to_list(F,B,LB),append(LA,LB,L).
bin_to_list(_F,A,[A]).

append_all([],[]):-!.
append_all([L|Ls],N):-append_all(Ls,M), append(L,M,N).