% extract sets (together with flag if pos or neg)
set(ID,pos) :- pos(ID,X).
set(ID,neg) :- neg(ID,X).

% non-deterministically choose sets to satisfy
choose(ID) :- not n_choose(ID), set(ID,M).
n_choose(ID) :- not choose(ID), set(ID,M).

% non-deterministically guess attack structure
att(X,Y) :- not n_att(X,Y), arg(X), arg(Y).
n_att(X,Y) :- not att(X,Y), arg(X), arg(Y).

% check whether chosen sets are satisfied

% for negative examples: one 'global' constraint
:- not neg_ex_ok(ID), sem(ID,S), set(ID,neg), choose(ID).

% conflict-free: positive check
:- choose(ID), sem(ID,cf), pos(ID,X), pos(ID,Y), att(X,Y).
% negative check
n_cf(ID) :- choose(ID), neg(ID,X), neg(ID,Y), att(X,Y), sem(ID,cf).
neg_ex_ok(ID) :- choose(ID), n_cf(ID), sem(ID,cf), set(ID,neg).

% admissible: positive
sem(ID,cf) :- choose(ID), set(ID,pos), sem(ID,adm).
defeated(ID,X) :- choose(ID), pos(ID,Y), sem(ID,adm), att(Y,X).
:- choose(ID), att(Y,X), not defeated(ID,Y), sem(ID,adm), pos(ID,X).
% negative
sem(ID,cf) :- choose(ID), set(ID,neg), sem(ID,adm).
defeated(ID,X) :- choose(ID), neg(ID,Y), sem(ID,adm), att(Y,X).
not_defended(ID,X) :- choose(ID), att(Y,X), not defeated(ID,Y), sem(ID,adm), neg(ID,X).
neg_ex_ok(ID) :- choose(ID), not_defended(ID,X), sem(ID,adm), neg(ID,X).

% complete: positive
sem(ID,adm) :- choose(ID), set(ID,pos), sem(ID,com).
not_defended(ID,X) :- choose(ID), att(Y,X), not defeated(ID,Y), sem(ID,com), not pos(ID,X).
:- choose(ID), not pos(ID,X), arg(X), not not_defended(ID,X), sem(ID,com), set(ID,pos).
% negative
sem(ID,adm) :- choose(ID), set(ID,neg), sem(ID,com).
not_defended(ID,X) :- choose(ID), att(Y,X), not defeated(ID,Y), sem(ID,com), not neg(ID,X).
neg_ex_ok(ID) :- choose(ID), not neg(ID,X), arg(X), not not_defended(ID,X), sem(ID,com), set(ID,neg).

% stable: positive
sem(ID,cf) :- choose(ID), set(ID,pos), sem(ID,stb).
defeated(ID,Y) :- choose(ID), sem(ID,stb), pos(ID,X), att(X,Y). 
:- choose(ID), sem(ID,stb), set(ID,pos), arg(X), not pos(ID,X), not defeated(ID,X). 
% negative
sem(ID,cf) :- choose(ID), set(ID,neg), sem(ID,stb).
defeated(ID,Y) :- choose(ID), sem(ID,stb), neg(ID,X), att(X,Y). 
neg_ex_ok(ID) :- choose(ID), arg(X), not neg(ID,X), not defeated(ID,X), sem(ID,stb), set(ID,neg).

% preferred: positive
sem(ID,adm) :- choose(ID), set(ID,pos), sem(ID,prf).

out(ID,X) :- arg(X), not pos(ID,X), choose(ID), set(ID,pos), sem(ID,prf).
not_trivial(ID) :- arg(X), not pos(ID,X), choose(ID), set(ID,pos), sem(ID,prf).
ecl(ID,X) : out(ID,X) :- not_trivial(ID), choose(ID), set(ID,pos), sem(ID,prf).
spoil(ID) | ecl(ID,Z) : att(Z,Y) :- ecl(ID,X), att(Y,X), choose(ID), set(ID,pos), sem(ID,prf).
spoil(ID) :- ecl(ID,X), ecl(ID,Y), att(X,Y), choose(ID), set(ID,pos), sem(ID,prf).
spoil(ID) :- pos(ID,X), ecl(ID,Y), att(X,Y), choose(ID), set(ID,pos), sem(ID,prf).
ecl(ID,X) :- spoil(ID), arg(X), choose(ID), set(ID,pos), sem(ID,prf).
:- not spoil(ID), not_trivial(ID), choose(ID), set(ID,pos), sem(ID,prf).

%lt(X,Y) :- arg(X),arg(Y), X<Y.
%nsucc(X,Z) :- lt(X,Y), lt(Y,Z).
%succ(X,Y) :- lt(X,Y), not nsucc(X,Y).
%ninf(X) :- lt(Y,X).
%nsup(X) :- lt(X,Y).
%inf(X) :- not ninf(X), arg(X).
%sup(X) :- not nsup(X), arg(X).
%inN(ID,X) :- pos(ID,X), sem(ID,prf), choose(ID).
%inN(ID,X) | outN(ID,X) :- not pos(ID,X), arg(X), sem(ID,prf), choose(ID), set(ID,pos).
%eq_upto(ID,Y) :- inf(Y), pos(ID,Y), sem(ID,prf), choose(ID), inN(ID,Y).
%eq_upto(ID,Y) :- inf(Y), not pos(ID,Y), sem(ID,prf), choose(ID), outN(ID,Y), set(ID,pos).
%eq_upto(ID,Y) :- succ(Z,Y), pos(ID,Y), sem(ID,prf), choose(ID), inN(ID,Y), eq_upto(ID,Z).
%eq_upto(ID,Y) :- succ(Z,Y), not pos(ID,Y), sem(ID,prf), choose(ID), outN(ID,Y), eq_upto(ID,Z), set(ID,pos).
%eq(ID) :- sup(Y), eq_upto(ID,Y). 
%undefeated_upto(ID,X,Y) :- inf(Y), outN(ID,X), outN(ID,Y).
%undefeated_upto(ID,X,Y) :- inf(Y), outN(ID,X),  not att(Y,X).
%undefeated_upto(ID,X,Y) :- succ(Z,Y), undefeated_upto(ID,X,Z), outN(ID,Y).
%undefeated_upto(ID,X,Y) :- succ(Z,Y), undefeated_upto(ID,X,Z), not att(Y,X).
%undefeated(ID,X) :- sup(Y), undefeated_upto(ID,X,Y).
%not_empty :- arg(X).
%spoil(ID) :- not not_empty, sem(ID,prf), choose(ID), set(ID,pos).
%spoil(ID) :- eq(ID).
%spoil(ID) :- inN(ID,X), inN(ID,Y), att(X,Y).
%spoil(ID) :- inN(ID,X), outN(ID,Y), att(Y,X), undefeated(ID,Y).
%inN(ID,X) :- spoil(ID), arg(X).
%outN(ID,X) :- spoil(ID), arg(X).
%:- not spoil(ID), sem(ID,prf), choose(ID), set(ID,pos).

% negative
sem(ID,adm) :- choose(ID), set(ID,neg), sem(ID,prf).
supIn(ID,X) :- choose(ID), neg(ID,X), sem(ID,prf).
supIn(ID,X) :- not supOut(ID,X), choose(ID), not neg(ID,X), sem(ID,prf), arg(X), set(ID,neg).
supOut(ID,X) :- not supIn(ID,X), choose(ID), not neg(ID,X), sem(ID,prf), arg(X), set(ID,neg).
conflictingPRF(ID) :- supIn(ID,X), supIn(ID,Y), att(X,Y), choose(ID), set(ID,neg), sem(ID,prf).
defeatedPRF(ID,X) :- supIn(ID,Y), att(Y,X), choose(ID), set(ID,neg), sem(ID,prf).
not_defendedPRF(ID,X) :- att(Y,X), not defeatedPRF(ID,Y), choose(ID), set(ID,neg), sem(ID,prf).
setNotDefendedPRF(ID) :- supIn(ID,X), not_defendedPRF(ID,X), choose(ID), set(ID,neg), sem(ID,prf).
admissibleSetPRF(ID) :- not conflictingPRF(ID), not setNotDefendedPRF(ID), choose(ID), set(ID,neg), sem(ID,prf).
neg_ex_ok(ID) :- supIn(ID,X), not neg(ID,X), admissibleSetPRF(ID), choose(ID), set(ID,neg), sem(ID,prf).

% weights
:~ n_choose(ID), weight(ID,W). [W,ID]

%show only attack structure
#show att/2.
%#show n_att/2.
#show n_choose/1.
#show choose/1.
%#show sem/2.
%#show set/2.
#show weight/2.