Benchmarks/wfs.chr

   1 :- module(wfs,[main/0, main/1]).
   2
   3 :- use_module(library(lists)).
   4
   5 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   6 %
   7 % Schrijf het programma waarvan je de wellfounded semantics wil bepalen
   8 % hieronder onder de vorm van prog/1 feiten. Let erop dat je een conjunctie
   9 % in de body tussen haakjes zet zodat prog/1 geparsed wordt, ipv prog/n.
  10
  11 /*
  12
  13 prog(p :- p).
  14
  15 prog(p :- \+ p).
  16
  17
  18 prog(p :- (q, \+ r)).
  19 prog(q :- (r, \+ p)).
  20 prog(r :- (p, \+ q)).
  21
  22 prog(p :- r).
  23 prog(r :- q).
  24 prog(q :- \+ q).
  25
  26 prog(p :- r).
  27 prog(r).
  28
  29 prog(p :- p).
  30 prog(s :- \+ p).
  31 prog(y :- (s, \+ x)).
  32 prog(x :- y).
  33 */
  34 prog(a :- a).
  35 prog(b :- b).
  36 prog(b :- \+ a).
  37 prog(c :- \+ b).
  38 prog(c :- c).
  39 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  40
  41
  42 :- constraints true/1, false/1, undefined/1, aclause/2, pos/2, neg/2, nbulit/2, nbplit/2, nbucl/2, phase2/0, true2/1, undefined2/1, aclause2/2, pos2/2, nbplit2/2, phase1/0, witness1/0, witness2/0.
  43
  44 true(At), aclause(Cl,At) \ pos(_,Cl) <=> true.
  45
  46 true(At), aclause(Cl,At) \ neg(_,Cl) <=> true.
  47
  48 false(At), aclause(Cl,At) \ pos(_,Cl) <=> true.
  49
  50 false(At), aclause(Cl,At) \ neg(_,Cl) <=> true.
  51
  52 true(At) \ nbucl(At,_) <=> true.
  53
  54 true(At) \ aclause(Cl,At), nbulit(Cl,_), nbplit(Cl,_) <=> true.
  55
  56 false(At) \ nbucl(At,_) <=> true.
  57
  58 nbucl(At,0) <=> false(At).
  59
  60 aclause(Cl,At), nbulit(Cl,0), nbplit(Cl,0) <=> true(At).
  61
  62 true(At) \ pos(At,Cl), nbulit(Cl,NU), nbplit(Cl,NP)
  63         <=>
  64                 NU1 is NU - 1, nbulit(Cl,NU1),
  65                 NP1 is NP - 1, nbplit(Cl,NP1).
  66
  67 false(At) \ neg(At,Cl), nbulit(Cl,NU)
  68         <=>
  69                 NU1 is NU - 1, nbulit(Cl,NU1).
  70
  71 true(At) \ neg(At,Cl), aclause(Cl,OAt), nbulit(Cl,_), nbplit(Cl,_), nbucl(OAt,N)
  72         <=>
  73                 N1 is N - 1, nbucl(OAt,N1).
  74
  75 false(At) \ pos(At,Cl), aclause(Cl,OAt), nbulit(Cl,_), nbplit(Cl,_), nbucl(OAt,N)
  76         <=>
  77                 N1 is N - 1, nbucl(OAt,N1).
  78
  79 witness2 \ witness2 <=> true.
  80 phase2, nbucl(At,_)  ==> witness2, undefined2(At).
  81 phase2, pos(At,Cl)   ==> pos2(At,Cl).
  82 phase2, aclause(Cl,At)    ==> aclause2(Cl,At).
  83 phase2, nbplit(Cl,N) ==> nbplit2(Cl,N).
  84 phase2, witness2 # ID <=> phase1 pragma passive(ID).
  85 phase2 \ nbplit2(_,_) # ID <=> true pragma passive(ID).
  86 phase2 \ aclause2(_,_) # ID <=> true pragma passive(ID).
  87 phase2 <=> true.
  88
  89
  90 true2(At), aclause2(Cl,At) \ pos2(_,Cl) <=> true.
  91 true2(At) \ undefined2(At) <=> true.
  92 aclause2(Cl,At), nbplit2(Cl,0) <=> true2(At).
  93 true2(At) \ pos2(At,Cl), nbplit2(Cl,NP)
  94         <=>
  95                 NP1 is NP - 1, nbplit2(Cl,NP1).
  96
  97 witness1 \ witness1 <=> true.
  98 phase1, undefined2(At) # ID1 , aclause(Cl,At) # ID2 \ pos(_,Cl) # ID3 <=> true pragma passive(ID1), passive(ID2), passive(ID3).
  99 phase1, undefined2(At) # ID1 , aclause(Cl,At) # ID2 \ neg(_,Cl) # ID3 <=> true pragma passive(ID1), passive(ID2), passive(ID3).
 100 phase1, undefined2(At) # ID1 \ aclause(Cl,At) # ID2 , nbulit(Cl,_) # ID3, nbplit(Cl,_) # ID4 <=> true pragma passive(ID1), passive(ID2), passive(ID3), passive(ID4).
 101 phase1 \ undefined2(At) # ID <=> witness1, false(At) pragma passive(ID).
 102 phase1 \ true2(_) # ID <=> true pragma passive(ID).
 103 phase1 \ aclause2(_,_) <=> true.
 104 phase1 \ pos2(_,_) # ID <=> true pragma passive(ID).
 105 phase1 \ nbplit2(_,_) # ID <=> true pragma passive(ID).
 106 phase1, witness1 # ID  <=> phase2 pragma passive(ID).
 107 phase1 \ nbucl(At,_) # ID <=> undefined(At) pragma passive(ID).
 108 phase1 \ pos(_,_) # ID <=> true.
 109 phase1 \ neg(_,_) # ID <=> true pragma passive(ID).
 110 phase1 \ aclause(_,_) # ID <=>  true pragma passive(ID).
 111 phase1 \ nbulit(_,_) # ID <=> true pragma passive(ID).
 112 phase1 \ nbplit(_,_) # ID <=> true pragma passive(ID).
 113 phase1 <=> true.
 114
 115 /*
 116         p :- r.
 117         r.
 118 */
 119 program1 :-
 120         nbucl(p,1),             % aantal undefined clauses voor p
 121         pos(r,cl1),             % positief voorkomen van r in clause cl1
 122         aclause(cl1,p),         % clause cl1 defineert p
 123         nbulit(cl1,1),          % aantal undefined literals in cl1
 124         nbplit(cl1,1),          % aantal positieve undefined literals in cl1
 125         nbucl(r,1),
 126         aclause(cl2,r),
 127         nbulit(cl2,0),
 128         nbplit(cl2,0).
 129
 130 /*
 131         p :- not r.
 132         r.
 133 */
 134 program2 :-
 135         nbucl(p,1),
 136         neg(r,cl1),
 137         aclause(cl1,p),
 138         nbulit(cl1,1),
 139         nbplit(cl1,1),
 140         nbucl(r,1),
 141         aclause(cl2,r),
 142         nbulit(cl2,0),
 143         nbplit(cl2,0).
 144
 145 /*
 146         p :- p.
 147 */
 148 program3 :-
 149         nbucl(p,1),
 150         pos(p,cl1),
 151         aclause(cl1,p),
 152         nbulit(cl1,1),
 153         nbplit(cl1,1).
 154
 155 /*
 156         p :- not p.
 157 */
 158 program4 :-
 159         nbucl(p,1),
 160         neg(p,cl1),
 161         aclause(cl1,p),
 162         nbulit(cl1,1),
 163         nbplit(cl1,0).
 164
 165 /*
 166         p :- q, not r.
 167         q :- r, not p.
 168         r :- p, not q.
 169 */
 170
 171 program5 :-
 172         nbucl(p,1),
 173         pos(p,cl3),
 174         neg(p,cl2),
 175         aclause(cl1,p),
 176         nbulit(cl1,2),
 177         nbplit(cl1,1),
 178         nbucl(q,1),
 179         pos(q,cl1),
 180         neg(q,cl3),
 181         aclause(cl2,q),
 182         nbulit(cl2,2),
 183         nbplit(cl2,1),
 184         nbucl(r,1),
 185         pos(r,cl2),
 186         neg(r,cl1),
 187         aclause(cl3,r),
 188         nbulit(cl3,2),
 189         nbplit(cl3,1).
 190
 191
 192 main :-
 193         main(1000).
 194
 195 main(N) :-
 196         cputime(T1),
 197         loop(N),
 198         cputime(T2),
 199         T is T2 - T1,
 200         write(bench(wfs ,N , T,0,hprolog)),write('.'),nl.
 201
 202 loop(N) :-
 203         ( N =< 0 ->
 204                 true
 205         ;
 206                 ( prog, fail ; true),
 207                 M is N - 1,
 208                 loop(M)
 209         ).
 210
 211 prog :-
 212         findall(Clause,wfs:prog(Clause),Clauses),
 213         process(Clauses,1),
 214         setof(At,B^(wfs:prog(At :- B) ; wfs:prog(At), atom(At)),Ats),
 215         process_atoms(Ats),
 216         phase2.
 217
 218 process([],_).
 219 process([C|Cs],N) :-
 220         ( C = (HAt :- B) ->
 221                 aclause(N,HAt),
 222                 conj2list(B,Literals,[]),
 223                 process_literals(Literals,N,NbULit,NbPLit),
 224                 nbulit(N,NbULit),
 225                 nbplit(N,NbPLit)
 226         ;
 227                 C = HAt,
 228                 aclause(N,HAt),
 229                 nbulit(N,0),
 230                 nbplit(N,0)
 231         ),
 232         N1 is N + 1,
 233         process(Cs,N1).
 234
 235 conj2list(G,L,T) :-
 236         ( G = (G1,G2) ->
 237                 conj2list(G1,L,T1),
 238                 conj2list(G2,T1,T)
 239         ;
 240                 L = [G|T]
 241         ).
 242
 243 process_literals([],_,0,0).
 244 process_literals([L|R],Cl,U,P) :-
 245         process_literals(R,Cl,U1,P1),
 246         ( L = (\+ At) ->
 247                 neg(At,Cl),
 248                 P = P1,
 249                 U is U1 + 1
 250         ;
 251                 pos(L,Cl),
 252                 P is P1 + 1,
 253                 U is U1 + 1
 254         ).
 255
 256 process_atoms([]).
 257 process_atoms([A|As]) :-
 258         findall(A,wfs:prog(A :- _),L),
 259         length(L,N),
 260         nbucl(A,N),
 261         process_atoms(As).