/*

	File: 		wfs.chr
	Author:		Tom Schrijvers
	E-mail:		Tom . Schrijvers @ cs . kuleuven . be
	Copyright:	2003 - 2004, K.U.Leuven

	Computes well-founded semantics of logic program
	
*/
:- module(wfs,[main/0, main/1]).

:- use_module(library(chr)).
:- use_module(library(lists)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Program
prog((a :- a)).
prog((b :- b)).
prog((b :- \+(a))).
prog((c :- \+(b))).
prog((c :- c)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

handler wfs.

constraints 
		 true/1,		% true(p)		p.inI^+
		 false/1,		% false(p)		p.inI^-
		 undefined/1,		% undefined(p)		p \not\in I \wedge \neg p \not\in I
		 aclause/2,		% aclause(r,p)		r.head = p
		 pos/2,			% pos(p,r)		p \in r.body^+
		 neg/2,			% neg(p,r)		p \in r.body^-
		 nbulit/2,		% nbulit(r,i)		r.literal = i
		 nbplit/2,		% nbplit(r,i)		
		 nbucl/2,		% nbucl(p,i)		p.headof = i
		 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. 

main :-
	main(1000).

main(N) :-
	statistics(runtime,[T1|_]),
	loop(N),
	statistics(runtime,[T2|_]),
	T is T2 - T1,
	write(bench(wfs,N,T,0,sicstus)), write('.'),nl.

loop(N) :-
	( N =< 0 ->
		true
	;
		( prog, fail ; true),
		M is N - 1,
		loop(M)
	).

prog :-
	findall(Clause,prog(Clause),Clauses),
	process(Clauses,1),
	setof(At,B^(prog((At :- B)) ; 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,prog((A :- _)),L),
	length(L,N),
	nbucl(A,N),
	process_atoms(As).