This repository has been archived on 2023-08-20. You can view files and clone it, but cannot push or open issues or pull requests.
yap-6.3/packages/chr/Benchmarks/wfs.chr

263 lines
5.6 KiB
Plaintext
Raw Normal View History

2015-10-13 08:17:51 +01:00
:- module(wfs,[main/0, main/1]).
:- use_module(library(chr)).
:- use_module(library(lists)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Schrijf het programma waarvan je de wellfounded semantics wil bepalen
% hieronder onder de vorm van prog/1 feiten. Let erop dat je een conjunctie
% in de body tussen haakjes zet zodat prog/1 geparsed wordt, ipv prog/n.
/*
prog(p :- p).
prog(p :- \+ p).
prog(p :- (q, \+ r)).
prog(q :- (r, \+ p)).
prog(r :- (p, \+ q)).
prog(p :- r).
prog(r :- q).
prog(q :- \+ q).
prog(p :- r).
prog(r).
prog(p :- p).
prog(s :- \+ p).
prog(y :- (s, \+ x)).
prog(x :- y).
*/
prog(a :- a).
prog(b :- b).
prog(b :- \+ a).
prog(c :- \+ b).
prog(c :- c).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- chr_constraint 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.
true(At), aclause(Cl,At) \ pos(_,Cl) <=> true.
true(At), aclause(Cl,At) \ neg(_,Cl) <=> true.
false(At), aclause(Cl,At) \ pos(_,Cl) <=> true.
false(At), aclause(Cl,At) \ neg(_,Cl) <=> true.
true(At) \ nbucl(At,_) <=> true.
true(At) \ aclause(Cl,At), nbulit(Cl,_), nbplit(Cl,_) <=> true.
false(At) \ nbucl(At,_) <=> true.
nbucl(At,0) <=> false(At).
aclause(Cl,At), nbulit(Cl,0), nbplit(Cl,0) <=> true(At).
true(At) \ pos(At,Cl), nbulit(Cl,NU), nbplit(Cl,NP)
<=>
NU1 is NU - 1, nbulit(Cl,NU1),
NP1 is NP - 1, nbplit(Cl,NP1).
false(At) \ neg(At,Cl), nbulit(Cl,NU)
<=>
NU1 is NU - 1, nbulit(Cl,NU1).
true(At) \ neg(At,Cl), aclause(Cl,OAt), nbulit(Cl,_), nbplit(Cl,_), nbucl(OAt,N)
<=>
N1 is N - 1, nbucl(OAt,N1).
false(At) \ pos(At,Cl), aclause(Cl,OAt), nbulit(Cl,_), nbplit(Cl,_), nbucl(OAt,N)
<=>
N1 is N - 1, nbucl(OAt,N1).
witness2 \ witness2 <=> true.
phase2, nbucl(At,_) ==> witness2, undefined2(At).
phase2, pos(At,Cl) ==> pos2(At,Cl).
phase2, aclause(Cl,At) ==> aclause2(Cl,At).
phase2, nbplit(Cl,N) ==> nbplit2(Cl,N).
phase2, witness2 # ID <=> phase1 pragma passive(ID).
phase2 \ nbplit2(_,_) # ID <=> true pragma passive(ID).
phase2 \ aclause2(_,_) # ID <=> true pragma passive(ID).
phase2 <=> true.
true2(At), aclause2(Cl,At) \ pos2(_,Cl) <=> true.
true2(At) \ undefined2(At) <=> true.
aclause2(Cl,At), nbplit2(Cl,0) <=> true2(At).
true2(At) \ pos2(At,Cl), nbplit2(Cl,NP)
<=>
NP1 is NP - 1, nbplit2(Cl,NP1).
witness1 \ witness1 <=> true.
phase1, undefined2(At) # ID1 , aclause(Cl,At) # ID2 \ pos(_,Cl) # ID3 <=> true pragma passive(ID1), passive(ID2), passive(ID3).
phase1, undefined2(At) # ID1 , aclause(Cl,At) # ID2 \ neg(_,Cl) # ID3 <=> true pragma passive(ID1), passive(ID2), passive(ID3).
phase1, undefined2(At) # ID1 \ aclause(Cl,At) # ID2 , nbulit(Cl,_) # ID3, nbplit(Cl,_) # ID4 <=> true pragma passive(ID1), passive(ID2), passive(ID3), passive(ID4).
phase1 \ undefined2(At) # ID <=> witness1, false(At) pragma passive(ID).
phase1 \ true2(_) # ID <=> true pragma passive(ID).
phase1 \ aclause2(_,_) <=> true.
phase1 \ pos2(_,_) # ID <=> true pragma passive(ID).
phase1 \ nbplit2(_,_) # ID <=> true pragma passive(ID).
phase1, witness1 # ID <=> phase2 pragma passive(ID).
phase1 \ nbucl(At,_) # ID <=> undefined(At) pragma passive(ID).
phase1 \ pos(_,_) # ID <=> true.
phase1 \ neg(_,_) # ID <=> true pragma passive(ID).
phase1 \ aclause(_,_) # ID <=> true pragma passive(ID).
phase1 \ nbulit(_,_) # ID <=> true pragma passive(ID).
phase1 \ nbplit(_,_) # ID <=> true pragma passive(ID).
phase1 <=> true.
/*
p :- r.
r.
*/
program1 :-
nbucl(p,1), % aantal undefined clauses voor p
pos(r,cl1), % positief voorkomen van r in clause cl1
aclause(cl1,p), % clause cl1 defineert p
nbulit(cl1,1), % aantal undefined literals in cl1
nbplit(cl1,1), % aantal positieve undefined literals in cl1
nbucl(r,1),
aclause(cl2,r),
nbulit(cl2,0),
nbplit(cl2,0).
/*
p :- not r.
r.
*/
program2 :-
nbucl(p,1),
neg(r,cl1),
aclause(cl1,p),
nbulit(cl1,1),
nbplit(cl1,1),
nbucl(r,1),
aclause(cl2,r),
nbulit(cl2,0),
nbplit(cl2,0).
/*
p :- p.
*/
program3 :-
nbucl(p,1),
pos(p,cl1),
aclause(cl1,p),
nbulit(cl1,1),
nbplit(cl1,1).
/*
p :- not p.
*/
program4 :-
nbucl(p,1),
neg(p,cl1),
aclause(cl1,p),
nbulit(cl1,1),
nbplit(cl1,0).
/*
p :- q, not r.
q :- r, not p.
r :- p, not q.
*/
program5 :-
nbucl(p,1),
pos(p,cl3),
neg(p,cl2),
aclause(cl1,p),
nbulit(cl1,2),
nbplit(cl1,1),
nbucl(q,1),
pos(q,cl1),
neg(q,cl3),
aclause(cl2,q),
nbulit(cl2,2),
nbplit(cl2,1),
nbucl(r,1),
pos(r,cl2),
neg(r,cl1),
aclause(cl3,r),
nbulit(cl3,2),
nbplit(cl3,1).
main :-
main(1000).
main(N) :-
cputime(T1),
loop(N),
cputime(T2),
T is T2 - T1,
write(bench(wfs ,N , T,0,hprolog)),write('.'),nl.
loop(N) :-
( N =< 0 ->
true
;
( prog, fail ; true),
M is N - 1,
loop(M)
).
prog :-
findall(Clause,wfs:prog(Clause),Clauses),
process(Clauses,1),
setof(At,B^(wfs:prog(At :- B) ; wfs:prog(At), atom(At)),Ats),
process_atoms(Ats),
phase2.
process([],_).
process([C|Cs],N) :-
( C = (HAt :- B) ->
aclause(N,HAt),
conj2list(B,Literals,[]),
process_literals(Literals,N,NbULit,NbPLit),
nbulit(N,NbULit),
nbplit(N,NbPLit)
;
C = HAt,
aclause(N,HAt),
nbulit(N,0),
nbplit(N,0)
),
N1 is N + 1,
process(Cs,N1).
conj2list(G,L,T) :-
( G = (G1,G2) ->
conj2list(G1,L,T1),
conj2list(G2,T1,T)
;
L = [G|T]
).
process_literals([],_,0,0).
process_literals([L|R],Cl,U,P) :-
process_literals(R,Cl,U1,P1),
( L = (\+ At) ->
neg(At,Cl),
P = P1,
U is U1 + 1
;
pos(L,Cl),
P is P1 + 1,
U is U1 + 1
).
process_atoms([]).
process_atoms([A|As]) :-
findall(A,wfs:prog(A :- _),L),
length(L,N),
nbucl(A,N),
process_atoms(As).