%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% DLV-Interpreter for preferred answer sets of propositional programs
% under the semantics defined by Wang, Zhou and Lin 2000, using the
% definition in Schaub/Wang 2001.
% 
% Store rules
%  
%     r:  A <- B1,...,Bm, not C1,..., not Cn
%
% by facts: 
% 
%  rule(r). head(A,r). pbl(B1,r). ... pbl(Bm,r). nbl(C1,r). ... nbl(Cn,r).
%
% classical negation must be emulated, state facts compl(L,L') for
% opposite classical literals 
%
% Specify preference  r < r' through fact  pr(r,r'). 
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Apply rules of the program: 

  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).

% Transitively close pr.

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

% Check irreflexivity.

  :- pr(X,X).

% Rule-IDs are used as stage-IDs (the number of rules is an upper bound for
% the number of computation stages), and the built-in arbitrary order < over
% these IDs is used.

  stage(S) :- rule(S).

% Falsity of the positive body of a rule in a set Xi (which is
% represented by in_Xi: Xi = { L | in_Xi(L,Xi) }

  pos_body_false_Xi(R,Xi) :- pbl(L,R), stage(Xi), not in_Xi(L,Xi).

% Initialisation: X0 = \emptyset
% The positive body is false w.r.t. \emptyset if some positive body
% literal exists.

  pos_body_false0(R) :- pbl(L,R).

% Active rules w.r.t. (Xi,X) where X is an answer set and Xi a set
% represented by in_Xi/2.

  active(R,Xi) :- rule(R), stage(Xi),
                  not pos_body_false_Xi(R,Xi), not neg_body_false(R).

% Initialisation: X0 = \emptyset
% Active rules w.r.t. (\emptyset,X) where X is 

  active0(R) :- rule(R), not pos_body_false0(R), not neg_body_false(R).

% Falsity of the negative body of a rule in a set Xi represented by in_Xi/2.

  neg_body_false_Xi(R,Xi) :- nbl(L,R), in_Xi(L,Xi).

% Active rules w.r.t. (X,Xi) where X is an answer set and Xi a set
% represented by in_Xi/2.

  active_Xi(R,Xi) :- rule(R), stage(Xi), pos_body_true(R),
                     not neg_body_false_Xi(R,Xi).

% Check whether the head of a rule R is in a set Xi.

  head_not_in_Xi(R,Xi) :- stage(Xi), head(H,R), not in_Xi(H,Xi).

% Check whether a rule, which is preferred to R, exists such that it
% is active w.r.t. (X,Xi) and its head does not occur in X1.

  preferred_generating_rule_exists(R,Xi) :- pr(R1,R), active_Xi(R1,Xi),
                                            head_not_in_Xi(R1,Xi).

% Initialisation: Check whether a rule, which is preferred to R, 
% exists such that it is active w.r.t. (X,\emptyset) and its head does
% not occur in \emptyset. The latter condition is trivially true, the
% former boils down to checking whether the positive body is true (not
% false).

  preferred_generating_rule_exists0(R) :- pr(R1,R), pos_body_true(R1).


% Compute Xis.

% Initialisation: Include the head of all rules which are active
% w.r.t. (X,X) and and where no preferred rule exists s.t. it is active
% w.r.t. (X,\emptyset) and its head does not occur in \emptyset.
% Since Xi \subseteq Xj for all j>i, these head literals must be in all
% Xk (k>0).

  in_Xi(H,Xi) :- stage(Xi), active0(R), head(H,R),
                 not preferred_generating_rule_exists0(R).

% Step: Include the head of all rules which are active
% w.r.t. (X,X) and and where no preferred rule exists s.t. it is active
% w.r.t. (X,Xi) and its head does not occur in Xi.
% Since Xi \subseteq Xj for all j>i, these head literals must be in all
% such Xj.

  in_Xi(H,Xj) :- head(H,R), active(R,Xi), stage(Xi), stage(Xj), Xj > Xi,
                 not preferred_generating_rule_exists(R,Xi).

% The preferred answer set (PAS) is the union of all Xi.

  in_PAS(L) :- in_Xi(L,_).

% "Stability"

  :- in_PAS(L), not in_AS(L).
  :- in_AS(L), not in_PAS(L).