%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%               DLV META-INTERPRETER
%
% for weakly preferred answer sets of prop. prioritized LP (P,<). 
%
% INPUT: Rules
%
%   r:  A <- B1,...,Bm, not C1,..., not Cn
%
% are represented by facts:
%
%  rule(r). head(A,r). pbl(B1,r). ... pbl(Bm,r).
%                      nbl(C1,r). ... nbl(Cn,r).
%
% Classical negation is represented by facts
%
%   compl(L,L').
%
% for complementary classical literals L and L'.
%
% Rule preferences r < r' are specified as facts
%
%   pr(r,r').
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Represent answer set:

  in_AS(X) :- head(X,R), pos_body_true(R), not neg_body_false(R).

  pos_body_exists(R) :- pbl(X,R).
  pos_body_true(R) :- rule(R), not pos_body_exists(R).

  pbl_inbetween(X,Y,R) :- pbl(X,R), pbl(Y,R), pbl(Z,R), X < Z, Z < Y.
  pbl_notlast(X,R) :- pbl(X,R), pbl(Y,R), X < Y.
  pbl_notfirst(X,R) :- pbl(X,R), pbl(Y,R), Y < X.

  pos_body_true_upto(R,X) :- pbl(X,R), not pbl_notfirst(X,R), in_AS(X).
  pos_body_true_upto(R,X) :- pos_body_true_upto(R,Y), pbl(X,R),
                             in_AS(X), Y < X, not pbl_inbetween(Y,X,R).
  pos_body_true(R) :- pos_body_true_upto(R,X), not pbl_notlast(X,R).

  neg_body_false(R) :- nbl(X,R), in_AS(X).

% Eliminate opposite literals (explicitly specified).

  :- compl(X,Y), in_AS(X), in_AS(Y).

% For full prioritization: refine pr to a total ordering.

 pr(X,Y) v pr(Y,X) :- rule(X),rule(Y), X != Y. 

 pr(X,Z) :- pr(X,Y), pr(Y,Z). 

         :- pr(X,X). 

% Weakly preferred answer sets: another total ordering,
% as close to pr as possible.

 pr1(X,Y) v pr1(Y,X) :- rule(X),rule(Y), X != Y. 

 pr1(X,Z) :- pr1(X,Y), pr1(Y,Z). 

         :- pr1(X,X). 

% weak constraint: minimize violations

 :~ rule(X), rule(Y), pr(X,Y), pr1(Y,X). [1:1]

% Check dual reduct: Build sets S_i, use rule ids as indices i.
%
% lit(X,r): the literal x occurs in the set S_r

   lit(X,Y) :- head(X,Y), pos_body_true(Y), 
               not defeat_local(Y), not in_AS(X). 

   lit(X,Y) :- head(X,Y), pos_body_true(Y), 
               not defeat_local(Y), not defeat_global(Y). 

   defeat_local(Y)  :- nbl(X,Y), lit(X,Y1), pr1(Y1,Y).  

   defeat_global(Y) :- nbl(X,Y), in_AS(X). 

% include literal into CP(.), which is a weakly preferred anser set

   in_WPAS(X) :- lit(X,Y).

   :- in_WPAS(X), not in_AS(X).