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


% Part 1: Guess a consistent set S.

  lit(L) :- head(L,_).  lit(L) :- pbl(L,_).  lit(L) :- nbl(L,_).

  in_S(L) v notin_S(L) :- lit(L).
  :- compl(X,Y), in_S(X), in_S(Y).


% Part 2: Handle preferences.

% Transitively close pr.

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

% Check irreflexivity.

  :- pr(X,X).


% Part 3: Stage IDs.

% 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.  Note that stage IDs range from 0 to n, while there are
% only n rule-IDs available, so stage 0 is represented by special predicates.

  stage(S) :- rule(S).


% Part 4: Evaluate positive bodies.

% Falsity of the positive body of a rule w.r.t. S.

  pos_body_false_S(R) :- rule(R), pbl(X,R), not in_S(X).

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

  pos_body_false_Si(R,Si) :- pbl(L,R), stage(Si), not in_Si(L,Si).

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

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


% Part 5: Evaluate negative bodies.

% Falsity of the negative body of a rule w.r.t. S.

  neg_body_false_S(R) :- rule(R), nbl(X,R), in_S(X).

% Falsity of the negative body of a rule in a set Si represented by in_Si/2.

  neg_body_false_Si(R,Si) :- nbl(L,R), in_Si(L,Si).


% Part 6: Determine active rules.

% Active rules w.r.t. (Si,S) where S is the set to be checked and Si a set
% represented by in_Si/2.

  active(R,Si) :- rule(R), stage(Si),
                  not pos_body_false_Si(R,Si), not neg_body_false_S(R).

% Active rules w.r.t. (S,Si) where S is the set to be checked and Si a set
% represented by in_Si/2.

  active_Si(R,Si) :- rule(R), stage(Si), not pos_body_false_S(R),
                     not neg_body_false_Si(R,Si).

% Initialisation: S0 = \emptyset
% Active rules w.r.t. (\emptyset,S) where S is the set to be checked.

  active_S0(R) :- rule(R), not pos_body_false_S0(R), not neg_body_false_S(R).


% Part 7: Check for preferred generating rules.

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

  head_not_in_Si(R,Si) :- stage(Si), head(H,R), not in_Si(H,Si).

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

  preferred_generating_rule_exists(R,Si) :- pr(R1,R), active_Si(R1,Si),
                                            head_not_in_Si(R1,Si).

% Initialisation: Check whether a rule, which is preferred to R, 
% exists such that it is active w.r.t. (S,\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_exists_S0(R) :- pr(R1,R), not pos_body_false_S(R1).


% Part 8: Compute Si.

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

  in_Si(H,Si) :- head(H,R), active(R,Sj), stage(Sj), stage(Si), Si > Sj,
                 not preferred_generating_rule_exists(R,Sj).

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

  in_Si(H,Si) :- head(H,R), active_S0(R), stage(Si),
                 not preferred_generating_rule_exists_S0(R).


% Part 9: Verify "stability".

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

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

% "Stability"

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