%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% dlv-Interpreter for preferred answer sets of propositional programs. 
% 
% 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).

% pbl - positive body literal; nbl - negative body literal 

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