1 % splitting a formula into its subformulas
   2 subformula2(X,F) :- ac(X,F),statement(X).
   3 subformula2(X,F) :- subformula2(X,and(F,_)).
   4 subformula2(X,F) :- subformula2(X,and(_,F)).
   5 subformula2(X,F) :- subformula2(X,or(_,F)).
   6 subformula2(X,F) :- subformula2(X,or(F,_)).
   7 subformula2(X,F) :- subformula2(X,neg(F)).
   8 subformula2(X,F) :- subformula2(X,xor(F,_)).
   9 subformula2(X,F) :- subformula2(X,xor(_,F)).
  10 subformula2(X,F) :- subformula2(X,imp(F,_)).
  11 subformula2(X,F) :- subformula2(X,imp(_,F)).
  12 subformula2(X,F) :- subformula2(X,iff(F,_)).
  13 subformula2(X,F) :- subformula2(X,iff(_,F)).
  14 subformula(F) :- subformula2(_,F).
  15 
  16 % decide whether a subformula is an atom or not
  17 noatom(F) :- subformula(F), subformula(F1), subformula(F2), F=and(F1,F2).
  18 noatom(F) :- subformula(F), subformula(F1), subformula(F2), F=or(F1,F2).
  19 noatom(F) :- subformula(F), subformula(F1), F=neg(F1).
  20 noatom(F) :- subformula(F), subformula(F1), subformula(F2), F=xor(F1,F2).
  21 noatom(F) :- subformula(F), subformula(F1), subformula(F2), F=imp(F1,F2).
  22 noatom(F) :- subformula(F), subformula(F1), subformula(F2), F=iff(F1,F2).
  23 
  24 atom(X) :- subformula(X), not noatom(X).
  25 atom(X) :- subformula(X), X=c(v).
  26 atom(X) :- subformula(X), X=c(f).
  27 
  28 % check whether an interpretation is a model or not at a specific iteration
  29 ismodel(X,I) :- atom(X), in(X,I).
  30 ismodel(X,I) :- atom(X), X=c(v), iteration(I).
  31 ismodel(F,I) :- subformula(F), subformula(F1), F=neg(F1), nomodel(F1,I).
  32 ismodel(F,I) :- subformula(F), F=and(F1,F2), ismodel(F1,I), ismodel(F2,I).
  33 ismodel(F,I) :- subformula(F), subformula(F1), subformula(F2), F=or(F1,F2), ismodel(F1,I).
  34 ismodel(F,I) :- subformula(F), subformula(F1), subformula(F2), F=or(F1,F2), ismodel(F2,I).
  35 ismodel(F,I) :- subformula(F), F=xor(F1,F2), ismodel(F1,I), nomodel(F2,I).
  36 ismodel(F,I) :- subformula(F), F=xor(F1,F2), ismodel(F2,I), nomodel(F1,I).
  37 ismodel(F,I) :- subformula(F), subformula(F1), subformula(F2), F=imp(F1,F2), nomodel(F1,I).
  38 ismodel(F,I) :- subformula(F), F=imp(F1,F2), ismodel(F1,I), ismodel(F2,I).
  39 ismodel(F,I) :- subformula(F), F=iff(F1,F2), ismodel(F1,I), ismodel(F2,I).
  40 ismodel(F,I) :- subformula(F), F=iff(F1,F2), nomodel(F1,I), nomodel(F2,I).
  41 
  42 nomodel(X,I) :- atom(X), out(X,I).
  43 nomodel(X,I) :- atom(X), X=c(f), iteration(I).
  44 nomodel(F,I) :- subformula(F), subformula(F1), F=neg(F1), ismodel(F1,I).
  45 nomodel(F,I) :- subformula(F), subformula(F1), subformula(F2), F=and(F1,F2), nomodel(F1,I).
  46 nomodel(F,I) :- subformula(F), subformula(F1), subformula(F2), F=and(F1,F2), nomodel(F2,I).
  47 nomodel(F,I) :- subformula(F), F=or(F1,F2), nomodel(F1,I), nomodel(F2,I).
  48 nomodel(F,I) :- subformula(F), F=xor(F1,F2), ismodel(F1,I), ismodel(F2,I).
  49 nomodel(F,I) :- subformula(F), F=xor(F1,F2), nomodel(F1,I), nomodel(F2,I).
  50 nomodel(F,I) :- subformula(F), F=imp(F1,F2), ismodel(F1,I), nomodel(F2,I).
  51 nomodel(F,I) :- subformula(F), F=iff(F1,F2), nomodel(F1,I), ismodel(F2,I).
  52 nomodel(F,I) :- subformula(F), F=iff(F1,F2), nomodel(F2,I), ismodel(F1,I).
  53 
  54 % get the number of statements and create an ordering
  55 snum(I) :- I = #count{Y : statement(Y)}.
  56 iteration(I) :- snum(J), I=J-1.
  57 iteration(I) :- iteration(J), I=J-1, I>=0.
  58 
  59 % create undecided set of variables at the starting point of the function
  60 undec(X,I) :- snum(I), statement(X).
  61 
  62 % iterate the function one step further, and guess an additional element for A or R
  63 inA(X,I) :- inA(X,J), J=I+1, iteration(I).
  64 inR(X,I) :- inR(X,J), J=I+1, iteration(I).
  65 select(X,I) :- not deselect(X,I), statement(X), iteration(I), undec(X,J), J=I+1.
  66 deselect(X,I) :- not select(X,I), statement(X), iteration(I), undec(X,J), J=I+1.
  67 :- A=#count { I : select(_,I)}, iteration(I), A>1.
  68 undec(X,I) :- iteration(I), undec(X,J), J=I+1, deselect(X,I).
  69 % check whether the selected element is in A or not.
  70 in(X,I) | out(X,I) :- undec(X,J), J=I+1, iteration(I).
  71 in(X,I) :- iteration(I), J=I+1, inA(X,J).
  72 out(X,I) :- iteration(I), J=I+1, inR(X,J).
  73 
  74 okA(I) :- select(X,I), ac(X,F), ismodel(F,I).
  75 okA(I) :- A= #count{I : select(_,I)}, iteration(I), A=0.
  76 inA(X,I) :- okA(I), select(X,I).
  77 
  78 in(X,I) :- okA(I), undec(X,J), J=I+1, iteration(I).
  79 out(X,I) :- okA(I), undec(X,J), J=I+1, iteration(I).
  80 
  81 
  82 % check whether the selected element is in R or not.
  83 okR(I) :- select(X,I), ac(X,F), nomodel(F,I), not okA(I).
  84 in(X,I) :- okR(I), undec(X,J), J=I+1, iteration(I).
  85 out(X,I) :- okR(I), undec(X,J), J=I+1, iteration(I).
  86 inR(X,I) :- okR(I), select(X,I).
  87 
  88 ok(I) :- okA(I).
  89 ok(I) :- okR(I).
  90 
  91 :- not ok(I), iteration(I).
  92 
  93 accept(X) :- inA(X,0).
  94 reject(X) :- inR(X,0).
  95 
  96 :~ statement(X), not accept(X). [X@2]
  97 :~ statement(X), not reject(X). [X@1]
  98 %#maximize [accept(X)@2].
  99 %#maximize [reject(X)@1].