1/*
2	LPAD and CP-Logic reasoning suite
3	File lpadsld.pl
4	Goal oriented interpreter for LPADs based on SLDNF
5	Copyright (c) 2007, Fabrizio Riguzzi
6*/
7%:- set_prolog_flag(debug,on).
8%:- set_prolog_flag(discontiguous_warnings,on).
9%:- set_prolog_flag(single_var_warnings,on).
10%:- source.
11:-dynamic rule/5,rule_by_num/8,rule_uniform/8,def_rule/2,setting/2.
12
13:-use_module(library(lists)).
14:-use_module(library(ugraphs)).
15
16:-load_foreign_files(['cplint'],[],init_my_predicates).
17
18/* start of list of parameters that can be set by the user with
19set(Parameter,Value) */
20setting(epsilon_parsing,0.00001).
21setting(save_dot,false).
22setting(ground_body,true).
23/* available values: true, false
24if true, both the head and the body of each clause will be grounded, otherwise
25only the head is grounded. In the case in which the body contains variables
26not appearing in the head, the body represents an existential event */
27setting(min_error,0.01).
28setting(initial_depth_bound,4).
29setting(depth_bound,4).
30setting(prob_threshold,0.00001).
31setting(prob_bound,0.01).
32
33/* end of list of parameters */
34
35/* s(GoalsLIst,Prob) compute the probability of a list of goals
36GoalsLis can have variables, s returns in backtracking all the solutions with their
37corresponding probability */
38s(GoalsList,Prob):-
39	solve(GoalsList,Prob).
40
41
42solve(GoalsList,Prob):-
43	setof(Deriv,find_deriv(GoalsList,Deriv),LDup),
44	rem_dup_lists(LDup,[],L),
45	build_formula(L,Formula,[],Var),
46	var2numbers(Var,0,NewVar),
47	(setting(save_dot,true)->
48		format("Variables: ~p~n",[Var]),
49		compute_prob(NewVar,Formula,Prob,1)
50	;
51		compute_prob(NewVar,Formula,Prob,0)
52	).
53
54solve(GoalsList,0.0):-
55	\+ find_deriv(GoalsList,_Deriv).
56
57/* s(GoalsList,Prob,CPUTime1,CPUTime2,WallTime1,WallTime2) compute the probability of a list of goals
58GoalsLis can have variables, s returns in backtracking all the solutions with
59their corresponding probability
60CPUTime1 is the cpu time for performing resolution
61CPUTime2 is the cpu time for elaborating the BDD
62WallTime1 is the wall time for performing resolution
63WallTime2 is the wall time for elaborating the BDD */
64
65
66s(GoalsList,Prob,CPUTime1,CPUTime2,WallTime1,WallTime2):-
67	solve(GoalsList,Prob,CPUTime1,CPUTime2,WallTime1,WallTime2).
68
69
70solve(GoalsList,Prob,CPUTime1,CPUTime2,WallTime1,WallTime2):-
71	statistics(cputime,[_,_]),
72	statistics(walltime,[_,_]),
73	(setof(Deriv,find_deriv(GoalsList,Deriv),LDup)->
74		rem_dup_lists(LDup,[],L),
75		statistics(cputime,[_,CT1]),
76		CPUTime1 is CT1/1000,
77		statistics(walltime,[_,WT1]),
78		WallTime1 is WT1/1000,
79		%print_mem,
80		build_formula(L,Formula,[],Var,0,Conj),
81		length(L,ND),
82		length(Var,NV),
83		format(user_error,"Disjunctions :~d~nConjunctions: ~d~nVariables ~d~n",[ND,Conj,NV]),
84		var2numbers(Var,0,NewVar),
85		(setting(save_dot,true)->
86			format("Variables: ~p~n",[Var]),
87			compute_prob(NewVar,Formula,Prob,1)
88		;
89			compute_prob(NewVar,Formula,Prob,0)
90		),
91		statistics(cputime,[_,CT2]),
92		CPUTime2 is CT2/1000,
93		statistics(walltime,[_,WT2]),
94		WallTime2 is WT2/1000
95	;
96		%print_mem,
97		Prob=0.0,
98		statistics(cputime,[_,CT1]),
99		CPUTime1 is CT1/1000,
100		statistics(walltime,[_,WT1]),
101		WallTime1 is WT1/1000,
102		CPUTime2 =0.0,
103		statistics(walltime,[_,WT2]),
104		WallTime2 =0.0
105	),!.
106	/*,
107	format(user_error,"~nMemory after inference~n",[]),
108	print_mem.*/
109
110/* iterative deepening, depth bounded
111for negative goals, if their derivation is cut, then they are
112added to the head of the list of goals to be resolved at the next depth bound*/
113si(GoalsList,ProbL,ProbU,CPUTime):-
114        statistics(cputime,[_,_]),
115	setting(initial_depth_bound,D),
116        solve_i([(GoalsList,[])],[],D,ProbL,ProbU),
117	statistics(cputime,[_,CT]),
118	CPUTime is CT/1000.
119
120
121/* solve_i(L0,Succ,D,ProbL0,ProbU0): L0 is a list of couples (G,Der) where
122G is a list of goals to be resolved and Der is an explanation, D is the
123current depth, ProbL0 is the lower bound of the prob and ProbU0 is the upper
124bound
125*/
126solve_i(L0,Succ,D,ProbL0,ProbU0):-
127	findall((G1,Deriv),(member((G0,C0),L0),solvei(G0,D,C0,Deriv,G1)),L),
128	%	print_mem,
129	separate_ulbi(L,[],LL0,[],LU,[],Incomplete),
130	append(Succ,LL0,LL),
131	compute_prob_deriv(LL,ProbL),
132	append(Succ,LU,LU1),
133	compute_prob_deriv(LU1,ProbU),
134	Err is ProbU-ProbL,
135	setting(min_error,ME),
136	(Err<ME->
137		ProbU0=ProbU,
138		ProbL0=ProbL
139	;
140		setting(depth_bound,DB),
141		D1 is D+DB,
142		solve_i(Incomplete,LL,D1,ProbL0,ProbU0)
143	).
144
145/* iterative deepening, problog style: each time
146the derivation is restarted from the original goal */
147sir(GoalsList,ProbL,ProbU,CPUTime):-
148        statistics(cputime,[_,_]),
149	setting(depth_bound,D),
150        solveir(GoalsList,D,ProbL,ProbU),
151	statistics(cputime,[_,CT]),
152	CPUTime is CT/1000.
153
154
155/* solveir(GoalsList,D,ProbL0,ProbU0) GoalsLIst is the list
156of goals to be derived, D is the depth bound, ProbL0,ProbU0 are the lower
157and upper bound. If for a certain depth bound the error is not smaller
158than the threshold, the depth bound is increased and the derivation is
159restarted from the beginning */
160solveir(GoalsList,D,ProbL0,ProbU0):-
161	(setof(Deriv,find_derivr(GoalsList,D,Deriv),LDup)->
162		rem_dup_lists(LDup,[],L),
163	%	print_mem,
164		separate_ulb(L,[],LL,[],LU),
165		compute_prob_deriv(LL,ProbL),
166		compute_prob_deriv(LU,ProbU),
167		Err is ProbU-ProbL,
168		setting(min_error,ME),
169		(Err<ME->
170			ProbU0=ProbU,
171			ProbL0=ProbL
172		;
173			setting(depth_bound,DB),
174			D1 is D+DB,
175			solveir(GoalsList,D1,ProbL0,ProbU0)
176		)
177	;
178	%	print_mem,
179		ProbL0=0.0,
180		ProbU0=0.0
181	).
182
183/* approximate algorithm cilog2 style: the explanations with a prob below the
184threshold are cut  */
185sic(GoalsList,ProbL,ProbU,CPUTime):-
186        statistics(cputime,[_,_]),
187	setting(depth_bound,D),
188        solveic(GoalsList,D,ProbL,ProbU),
189	statistics(cputime,[_,CT]),
190	CPUTime is CT/1000.
191
192solveic(GoalsList,D,ProbL0,ProbU0):-
193	(setof((Deriv,P,Pruned),solvec(GoalsList,D,[],Deriv,1.0,P,Pruned),L)->
194	%	print_mem,
195		separate_ulbc(L,[],LL,0,Err),
196		compute_prob_deriv(LL,ProbL0),
197		ProbU0 is ProbL0+Err
198		/*(ProbU>1.0->
199			ProbU0=1.0
200		;
201			ProbU0=ProbU
202		)*/
203	;
204	%	print_mem,
205		ProbL0=0.0,
206		ProbU0=0.0
207	).
208
209compute_prob_deriv(LL,ProbL):-
210	build_formula(LL,FormulaL,[],VarL,0,_ConjL),
211	%length(LL,NDL),
212	%length(VarL,NVL),
213	%format(user_error,"Disjunctions :~d~nConjunctions: ~d~nVariables ~d~n",[NDL,ConjL,NVL]),
214	var2numbers(VarL,0,NewVarL),
215	(FormulaL=[]->
216		ProbL=0.0
217	;
218		(FormulaL=[[]|_]->
219			ProbL=1.0
220		;
221			(setting(save_dot,true)->
222			%	format("Variables: ~p~n",[VarL]),
223				compute_prob(NewVarL,FormulaL,ProbL,1)
224			;
225				compute_prob(NewVarL,FormulaL,ProbL,0)
226			)
227		)
228	).
229
230print_mem:-
231	statistics(global_stack,[GS,GSF]),
232	statistics(local_stack,[LS,LSF]),
233	statistics(heap,[HP,HPF]),
234	statistics(trail,[TU,TF]),
235	format(user_error,"~nGloabal stack used ~d execution stack free: ~d~n",[GS,GSF]),
236	format(user_error,"Local stack used ~d execution stack free: ~d~n",[LS,LSF]),
237	format(user_error,"Heap used ~d heap free: ~d~n",[HP,HPF]),
238	format(user_error,"Trail used ~d Trail free: ~d~n",[TU,TF]).
239
240find_deriv(GoalsList,Deriv):-
241	solve(GoalsList,[],DerivDup),
242	remove_duplicates(DerivDup,Deriv).
243
244find_derivr(GoalsList,DB,Deriv):-
245        solver(GoalsList,DB,[],DerivDup),
246	remove_duplicates(DerivDup,Deriv).
247
248
249/* duplicate can appear in the C set because two different unistantiated clauses may become the
250same clause when instantiated */
251
252/* sc(Goals,Evidence,Prob) compute the conditional probability of the list of goals
253Goals given the list of goals Evidence
254Goals and Evidence can have variables, sc returns in backtracking all the solutions with their
255corresponding probability
256*/
257sc(Goals,Evidence,Prob):-
258	solve_cond(Goals,Evidence,Prob).
259
260solve_cond(Goals,Evidence,Prob):-
261	(setof(DerivE,find_deriv(Evidence,DerivE),LDupE)->
262		rem_dup_lists(LDupE,[],LE),
263		(setof(DerivGE,find_deriv_GE(LE,Goals,DerivGE),LDupGE)->
264			%print_mem,
265			rem_dup_lists(LDupGE,[],LGE),
266			build_formula(LE,FormulaE,[],VarE),
267			var2numbers(VarE,0,NewVarE),
268			build_formula(LGE,FormulaGE,[],VarGE),
269			var2numbers(VarGE,0,NewVarGE),
270			compute_prob(NewVarE,FormulaE,ProbE,0),
271			call_compute_prob(NewVarGE,FormulaGE,ProbGE),
272			Prob is ProbGE/ProbE
273		;
274			%print_mem,
275			Prob=0.0
276		)
277	;
278		%print_mem,
279		Prob=undefined
280	).
281	/*,
282	format(user_error,"~nMemory after inference~n",[]),
283	print_mem. */
284
285sci(Goals,Evidence,ProbL,ProbU,CPUTime):-
286	statistics(cputime,[_,_]),
287	setting(depth_bound,D),
288	append(Goals,Evidence,GE),
289        solve_condi([(GE,[])],[(Evidence,[])],[],[],D,ProbL,ProbU),
290	statistics(cputime,[_,CT]),
291	CPUTime is CT/1000.
292
293solve_condi(LGoals,LEvidence,SuccGE,SuccE,D,ProbL0,ProbU0):-
294	findall((GE1,DerivE),
295		(member((GE,CE),LEvidence),solvei(GE,D,CE,DerivE,GE1)),
296		LE),
297	findall((GE1,DerivE),
298		(member((GE,CE),LGoals),solvei(GE,D,CE,DerivE,GE1)),
299		LGE),
300	separate_ulbi(LE,[],LLE0,[],LUE0,[],IncE),
301	append(SuccE,LUE0,LUE),
302	compute_prob_deriv(LUE,ProbUE),
303	(ProbUE\==0.0->
304		separate_ulbi(LGE,[],LLGE0,[],LUGE0,[],IncGE),
305		append(SuccGE,LLGE0,LLGE),
306		compute_prob_deriv(LLGE,ProbLGE),
307		ProbL is ProbLGE/ProbUE,
308		append(SuccE,LLE0,LLE),
309		compute_prob_deriv(LLE,ProbLE),
310		(ProbLE\==0.0->
311			append(SuccGE,LUGE0,LUGE),
312			compute_prob_deriv(LUGE,ProbUGE),
313			ProbU1 is ProbUGE/ProbLE
314		;
315			ProbU1=1.0
316		),
317		(ProbU1>1.0->
318			ProbU=1.0
319		;
320			ProbU=ProbU1
321		),
322		Err is ProbU-ProbL,
323		setting(min_error,ME),
324		(Err<ME->
325			ProbU0=ProbU,
326			ProbL0=ProbL
327		;
328			setting(depth_bound,DB),
329			D1 is D+DB,
330			solve_condi(IncGE,IncE,LLGE,LLE,D1,ProbL0,ProbU0)
331		)
332	;
333		ProbL0=undefined,
334		ProbU0=undefined
335	).
336
337/* iterative deepening, problog style */
338scir(Goals,Evidence,ProbL,ProbU,CPUTime):-
339	statistics(cputime,[_,_]),
340	setting(depth_bound,D),
341        solve_condir(Goals,Evidence,D,ProbL,ProbU),
342	statistics(cputime,[_,CT]),
343	CPUTime is CT/1000.
344
345solve_condir(Goals,Evidence,D,ProbL0,ProbU0):-
346	(call_residue(setof(DerivE,find_derivr(Evidence,D,DerivE),LDupE),_R0)->
347		rem_dup_lists(LDupE,[],LE),
348		append(Evidence,Goals,EG),
349		(call_residue(setof(DerivGE,find_derivr(EG,D,DerivGE),LDupGE),_R1)->
350			rem_dup_lists(LDupGE,[],LGE),
351			separate_ulb(LGE,[],LLGE,[],LUGE),
352			compute_prob_deriv(LLGE,ProbLGE),
353			compute_prob_deriv(LUGE,ProbUGE),
354			separate_ulb(LE,[],LLE,[],LUE),
355			compute_prob_deriv(LLE,ProbLE),
356			compute_prob_deriv(LUE,ProbUE),
357			ProbL is ProbLGE/ProbUE,
358			(ProbLE=0.0->
359				ProbU1=1.0
360			;
361				ProbU1 is ProbUGE/ProbLE
362			),
363			(ProbU1>1.0->
364				ProbU=1.0
365			;
366				ProbU=ProbU1
367			),
368			Err is ProbU-ProbL,
369			setting(min_error,ME),
370			(Err<ME->
371				ProbU0=ProbU,
372				ProbL0=ProbL
373			;
374				setting(depth_bound,DB),
375				D1 is D+DB,
376				solve_condir(Goals,Evidence,D1,ProbL0,ProbU0)
377			)
378		;
379			ProbL0=0.0,
380			ProbU0=0.0
381		)
382	;
383		ProbL0=undefined,
384		ProbU0=undefined
385	).
386
387/* approximate algorithm cilog2 style */
388scic(Goals,Evidence,ProbL,ProbU,CPUTime):-
389	statistics(cputime,[_,_]),
390	setting(depth_bound,D),
391        solve_condic(Goals,Evidence,D,ProbL,ProbU),
392	statistics(cputime,[_,CT]),
393	CPUTime is CT/1000.
394
395solve_condic(Goals,Evidence,D,ProbL0,ProbU0):-
396	(call_residue(setof((DerivE,P,Pruned),solvec(Evidence,D,[],DerivE,1.0,P,Pruned),LE),_R0)->
397		append(Evidence,Goals,EG),
398		(call_residue(setof((DerivGE,P,Pruned),solvec(EG,D,[],DerivGE,1.0,P,Pruned),LGE),_R1)->
399			separate_ulbc(LGE,[],LLGE,0.0,ErrGE),
400			compute_prob_deriv(LLGE,ProbLGE),
401			separate_ulbc(LE,[],LLE,0.0,ErrE),
402			compute_prob_deriv(LLE,ProbLE),
403			ProbUGE0 is ProbLGE+ErrGE,
404			(ProbUGE0>1.0->
405				ProbUGE=1.0
406			;
407				ProbUGE=ProbUGE0
408			),
409			ProbUE0 is ProbLE+ErrE,
410			(ProbUE0>1.0->
411				ProbUE=1.0
412			;
413				ProbUE=ProbUE0
414			),
415			ProbL0 is ProbLGE/ProbUE,
416			(ProbLE=0.0->
417				ProbU1=1.0
418			;
419				ProbU1 is ProbUGE/ProbLE
420			),
421			(ProbU1>1.0->
422				ProbU0=1.0
423			;
424				ProbU0=ProbU1
425			)
426		;
427			ProbL0=0.0,
428			ProbU0=0.0
429		)
430	;
431		ProbL0=undefined,
432		ProbU0=undefined
433	).
434
435/* sc(Goals,Evidence,Prob,Time1,Time2) compute the conditional probability of the list of goals
436Goals given the list of goals Evidence
437Goals and Evidence can have variables, sc returns in backtracking all the solutions with their
438corresponding probability
439Time1 is the time for performing resolution
440Time2 is the time for elaborating the two BDDs
441*/
442sc(Goals,Evidence,Prob,CPUTime1,CPUTime2,WallTime1,WallTime2):-
443	solve_cond(Goals,Evidence,Prob,CPUTime1,CPUTime2,WallTime1,WallTime2).
444
445solve_cond(Goals,Evidence,Prob,CPUTime1,CPUTime2,WallTime1,WallTime2):-
446	statistics(cputime,[_,_]),
447	statistics(walltime,[_,_]),
448	(setof(DerivE,find_deriv(Evidence,DerivE),LDupE)->
449		rem_dup_lists(LDupE,[],LE),
450		(setof(DerivGE,find_deriv_GE(LE,Goals,DerivGE),LDupGE)->
451			rem_dup_lists(LDupGE,[],LGE),
452			statistics(cputime,[_,CT1]),
453			CPUTime1 is CT1/1000,
454			statistics(walltime,[_,WT1]),
455			WallTime1 is WT1/1000,
456			build_formula(LE,FormulaE,[],VarE),
457			var2numbers(VarE,0,NewVarE),
458			build_formula(LGE,FormulaGE,[],VarGE),
459			var2numbers(VarGE,0,NewVarGE),
460			compute_prob(NewVarE,FormulaE,ProbE,0),
461			call_compute_prob(NewVarGE,FormulaGE,ProbGE),
462			Prob is ProbGE/ProbE,
463			statistics(cputime,[_,CT2]),
464			CPUTime2 is CT2/1000,
465			statistics(walltime,[_,WT2]),
466			WallTime2 is WT2/1000
467		;
468			Prob=0.0,
469			statistics(cputime,[_,CT1]),
470			CPUTime1 is CT1/1000,
471			statistics(walltime,[_,WT1]),
472			WallTime1 is WT1/1000,
473			CPUTime2=0.0,
474			WallTime2=0.0
475		)
476	;
477		Prob=undefined,
478			statistics(cputime,[_,CT1]),
479			CPUTime1 is CT1/1000,
480			statistics(walltime,[_,WT1]),
481			WallTime1 is WT1/1000,
482			CPUTime2=0.0,
483			WallTime2=0.0
484	).
485
486solve_cond_goals(Goals,LE,0,Time1,0):-
487	statistics(runtime,[_,_]),
488	\+ find_deriv_GE(LE,Goals,_DerivGE),
489	statistics(runtime,[_,T1]),
490	Time1 is T1/1000.
491
492call_compute_prob(NewVarGE,FormulaGE,ProbGE):-
493	(FormulaGE=[]->
494		ProbGE=0.0
495	;
496		(FormulaGE=[[]|_]->
497                	ProbGE=1.0
498		;
499			(setting(save_dot,true)->
500				format("Variables: ~p~n",[NewVarGE]),
501				compute_prob(NewVarGE,FormulaGE,ProbGE,1)
502			;
503				compute_prob(NewVarGE,FormulaGE,ProbGE,0)
504			)
505		)
506	).
507
508find_deriv_GE(LD,GoalsList,Deriv):-
509	member(D,LD),
510	solve(GoalsList,D,DerivDup),
511	remove_duplicates(DerivDup,Deriv).
512
513find_deriv_GE(LD,GoalsList,DB,Deriv):-
514        member(D,LD),
515	solve(GoalsList,DB,D,DerivDup),
516	remove_duplicates(DerivDup,Deriv).
517
518/* solve(GoalsList,CIn,COut) takes a list of goals and an input C set
519and returns an output C set
520The C set is a list of triple (N,R,S) where
521- N is the index of the head atom used, starting from 0
522- R is the index of the non ground rule used, starting from 1
523- S is the substitution of rule R, in the form of a list whose elements
524	are of the form 'VarName'=value
525*/
526solve([],C,C):-!.
527
528solve([bagof(V,EV^G,L)|T],CIn,COut):-!,
529	list2and(GL,G),
530	bagof((V,C),EV^solve(GL,CIn,C),LD),
531	length(LD,N),
532	build_initial_graph(N,GrIn),
533	build_graph(LD,0,GrIn,Gr),
534	clique(Gr,Clique),
535	build_Cset(LD,Clique,L,[],C1),
536	remove_duplicates_eq(C1,C2),
537	solve(T,C2,COut).
538
539solve([bagof(V,G,L)|T],CIn,COut):-!,
540	list2and(GL,G),
541	bagof((V,C),solve(GL,CIn,C),LD),
542	length(LD,N),
543	build_initial_graph(N,GrIn),
544	build_graph(LD,0,GrIn,Gr),
545	clique(Gr,Clique),
546	build_Cset(LD,Clique,L,[],C1),
547	remove_duplicates_eq(C1,C2),
548	solve(T,C2,COut).
549
550
551solve([setof(V,EV^G,L)|T],CIn,COut):-!,
552	list2and(GL,G),
553	setof((V,C),EV^solve(GL,CIn,C),LD),
554	length(LD,N),
555	build_initial_graph(N,GrIn),
556	build_graph(LD,0,GrIn,Gr),
557	clique(Gr,Clique),
558	build_Cset(LD,Clique,L1,[],C1),
559	remove_duplicates(L1,L),
560	solve(T,C1,COut).
561
562solve([setof(V,G,L)|T],CIn,COut):-!,
563	list2and(GL,G),
564	setof((V,C),solve(GL,CIn,C),LD),
565	length(LD,N),
566	build_initial_graph(N,GrIn),
567	build_graph(LD,0,GrIn,Gr),
568	clique(Gr,Clique),
569	build_Cset(LD,Clique,L1,[],C1),
570	remove_duplicates(L1,L),
571	solve(T,C1,COut).
572
573solve([\+ H |T],CIn,COut):-!,
574	list2and(HL,H),
575	(setof(D,find_deriv(HL,D),LDup)->
576		rem_dup_lists(LDup,[],L),
577		choose_clauses(CIn,L,C1),
578		solve(T,C1,COut)
579	;
580		solve(T,CIn,COut)
581	).
582
583solve([H|T],CIn,COut):-
584	builtin(H),!,
585	call(H),
586	solve(T,CIn,COut).
587
588solve([H|T],CIn,COut):-
589	def_rule(H,B),
590	append(B,T,NG),
591	solve(NG,CIn,COut).
592
593solve([H|T],CIn,COut):-
594	find_rule(H,(R,S,N),B,CIn),
595	solve_pres(R,S,N,B,T,CIn,COut).
596
597
598solvei([],_DB,C,C,[]):-!.
599
600solvei(G,0,C,C,G):-!.
601
602solvei([\+ H |T],DB,CIn,COut,G):-!,
603        list2and(HL,H),
604	(findall((GH,D),solvei(HL,DB,CIn,D,GH),L)->
605		separate_ulbi(L,[],LB,[],_UB,[],I),
606		(I\=[]->
607			C1=CIn,
608			G=[\+ H|G1]
609		;
610			choose_clauses(CIn,LB,C1),
611			G=G1
612		),
613		solvei(T,DB,C1,COut,G1)
614	;
615		solvei(T,DB,CIn,COut,G1)
616	).
617solvei([H|T],DB,CIn,COut,G):-
618	builtin(H),!,
619	call(H),
620	solvei(T,DB,CIn,COut,G).
621
622solvei([H|T],DB,CIn,COut,G):-
623	def_rule(H,B),
624	append(B,T,NG),
625	DB1 is DB-1,
626	solvei(NG,DB1,CIn,COut,G).
627
628solvei([H|T],DB,CIn,COut,G):-
629	find_rule(H,(R,S,N),B,CIn),
630	DB1 is DB-1,
631	solve_presi(R,S,N,B,T,DB1,CIn,COut,G).
632
633solver([],_DB,C,C):-!.
634
635solver(_G,0,C,[(_,pruned,_)|C]):-!.
636
637solver([\+ H |T],DB,CIn,COut):-!,
638        list2and(HL,H),
639	(setof(D,find_derivr(HL,DB,D),LDup)->
640		rem_dup_lists(LDup,[],L),
641		separate_ulb(L,[],LB,[],UB),
642		(\+ LB=UB->
643
644			choose_clauses(CIn,LB,C0),
645			C1=[(_,pruned,_)|C0]
646		;
647			choose_clauses(CIn,L,C1)
648		),
649		solver(T,DB,C1,COut)
650	;
651		solver(T,DB,CIn,COut)
652	).
653solver([H|T],DB,CIn,COut):-
654	builtin(H),!,
655	call(H),
656	solver(T,DB,CIn,COut).
657
658solver([H|T],DB,CIn,COut):-
659	def_rule(H,B),
660	append(B,T,NG),
661	DB1 is DB-1,
662	solver(NG,DB1,CIn,COut).
663
664solver([H|T],DB,CIn,COut):-
665	find_rule(H,(R,S,N),B,CIn),
666	DB1 is DB-1,
667	solve_presr(R,S,N,B,T,DB1,CIn,COut).
668
669
670solvec([],_DB,C,C,P,P,false):-!.
671
672solvec(_G,0,C,C,P,P,true):-!.
673
674solvec(_G,_DB,C,C,P,P,true):-
675	setting(prob_threshold,T),
676	P=<T,!.
677
678solvec([\+ H |T],DB,CIn,COut,P0,P1,Pruned):-!,
679        list2and(HL,H),
680	(setof((D,P,Pr),solvec(HL,DB,[],D,1,P,Pr),L)->
681		separate_ulbc(L,[],LB,0.0,PP),
682		(PP=\=0.0->
683
684			choose_clausesc(CIn,LB,C1,P0,P2),
685			Pruned=true,
686			solvec(T,DB,C1,COut,P2,P1,_)
687
688		;
689			choose_clausesc(CIn,LB,C1,P0,P2),
690			solvec(T,DB,C1,COut,P2,P1,Pruned)
691		)
692	;
693		solve(T,DB,CIn,COut,P0,P1,Pruned)
694	).
695
696solvec([H|T],DB,CIn,COut,P0,P1,Pruned):-
697	builtin(H),!,
698	call(H),
699	solvec(T,DB,CIn,COut,P0,P1,Pruned).
700
701solvec([H|T],DB,CIn,COut,P0,P1,Pruned):-
702	def_rule(H,B),
703	append(B,T,NG),
704	DB1 is DB-1,
705	solvec(NG,DB1,CIn,COut,P0,P1,Pruned).
706
707solvec([H|T],DB,CIn,COut,P0,P1,Pruned):-
708	find_rulec(H,(R,S,N),B,CIn,P),
709	DB1 is DB-1,
710	solve_presc(R,S,N,B,T,DB1,CIn,COut,P,P0,P1,Pruned).
711
712
713solve_pres(R,S,N,B,T,CIn,COut):-
714	member_eq((N,R,S),CIn),!,
715	append(B,T,NG),
716	solve(NG,CIn,COut).
717
718solve_pres(R,S,N,B,T,CIn,COut):-
719	append(CIn,[(N,R,S)],C1),
720	append(B,T,NG),
721	solve(NG,C1,COut).
722
723solve_presi(R,S,N,B,T,DB,CIn,COut,G):-
724        member_eq((N,R,S),CIn),!,
725	append(B,T,NG),
726	solvei(NG,DB,CIn,COut,G).
727
728solve_presi(R,S,N,B,T,DB,CIn,COut,G):-
729	append(CIn,[(N,R,S)],C1),
730	append(B,T,NG),
731	solvei(NG,DB,C1,COut,G).
732
733
734solve_presr(R,S,N,B,T,DB,CIn,COut):-
735        member_eq((N,R,S),CIn),!,
736	append(B,T,NG),
737	solver(NG,DB,CIn,COut).
738
739solve_presr(R,S,N,B,T,DB,CIn,COut):-
740	append(CIn,[(N,R,S)],C1),
741	append(B,T,NG),
742	solver(NG,DB,C1,COut).
743
744
745solve_presc(R,S,N,B,T,DB,CIn,COut,_,P0,P1,Pruned):-
746        member_eq((N,R,S),CIn),!,
747	append(B,T,NG),
748	solvec(NG,DB,CIn,COut,P0,P1,Pruned).
749
750solve_presc(R,S,N,B,T,DB,CIn,COut,P,P0,P1,Pruned):-
751	append(CIn,[(N,R,S)],C1),
752	append(B,T,NG),
753	P2 is P0*P,
754	solvec(NG,DB,C1,COut,P2,P1,Pruned).
755
756
757build_initial_graph(N,G):-
758	listN(0,N,Vert),
759	add_vertices([],Vert,G).
760
761
762build_graph([],_N,G,G).
763
764build_graph([(_V,C)|T],N,GIn,GOut):-
765	N1 is N+1,
766	compatible(C,T,N,N1,GIn,G1),
767	build_graph(T,N1,G1,GOut).
768
769compatible(_C,[],_N,_N1,G,G).
770
771compatible(C,[(_V,H)|T],N,N1,GIn,GOut):-
772	(compatible(C,H)->
773		add_edges(GIn,[N-N1,N1-N],G1)
774	;
775		G1=GIn
776	),
777	N2 is N1 +1,
778	compatible(C,T,N,N2,G1,GOut).
779
780compatible([],_C).
781
782compatible([(N,R,S)|T],C):-
783	not_present_with_a_different_head(N,R,S,C),
784	compatible(T,C).
785
786not_present_with_a_different_head(_N,_R,_S,[]).
787
788not_present_with_a_different_head(N,R,S,[(N,R,S)|T]):-!,
789	not_present_with_a_different_head(N,R,S,T).
790
791not_present_with_a_different_head(N,R,S,[(_N1,R,S1)|T]):-
792	S\=S1,!,
793	not_present_with_a_different_head(N,R,S,T).
794
795not_present_with_a_different_head(N,R,S,[(_N1,R1,_S1)|T]):-
796	R\=R1,
797	not_present_with_a_different_head(N,R,S,T).
798
799
800
801build_Cset(_LD,[],[],C,C).
802
803build_Cset(LD,[H|T],[V|L],CIn,COut):-
804	nth0(H,LD,(V,C)),
805	append(C,CIn,C1),
806	build_Cset(LD,T,L,C1,COut).
807
808
809/* find_rule(G,(R,S,N),Body,C) takes a goal G and the current C set and
810returns the index R of a disjunctive rule resolving with G together with
811the index N of the resolving head, the substitution S and the Body of the
812rule */
813find_rule(H,(R,S,N),Body,C):-
814	rule(H,_P,N,R,S,_,Head,Body),
815	member_head(H,Head,0,N),
816	not_already_present_with_a_different_head(N,R,S,C).
817
818find_rule(H,(R,S,Number),Body,C):-
819	rule_uniform(H,R,S,_,1/_Num,_L,Number,Body),
820	not_already_present_with_a_different_head(Number,R,S,C).
821
822find_rulec(H,(R,S,N),Body,C,P):-
823	rule(H,_P,N,R,S,_,Head,Body),
824	member_headc(H,Head,0,N,P),
825	not_already_present_with_a_different_head(N,R,S,C).
826
827
828not_already_present_with_a_different_head(_N,_R,_S,[]).
829
830
831not_already_present_with_a_different_head(N,R,S,[(N1,R,S1)|T]):-
832	not_different(N,N1,S,S1),!,
833	not_already_present_with_a_different_head(N,R,S,T).
834
835not_already_present_with_a_different_head(N,R,S,[(_N1,R1,_S1)|T]):-
836	R\==R1,
837	not_already_present_with_a_different_head(N,R,S,T).
838
839
840not_different(_N,_N1,S,S1):-
841	S\=S1,!.
842
843not_different(N,N1,S,S1):-
844	N\=N1,!,
845	dif(S,S1).
846
847not_different(N,N,S,S).
848
849
850member_head(H,[(H:_P)|_T],N,N).
851
852member_head(H,[(_H:_P)|T],NIn,NOut):-
853	N1 is NIn+1,
854	member_head(H,T,N1,NOut).
855
856member_headc(H,[(H:P)|_T],N,N,P).
857
858member_headc(H,[(_H:_P)|T],NIn,NOut,P):-
859	N1 is NIn+1,
860	member_headc(H,T,N1,NOut,P).
861
862
863/* choose_clauses(CIn,LC,COut) takes as input the current C set and
864the set of C sets for a negative goal and returns a new C set that
865excludes all the derivations for the negative goals */
866choose_clauses(C,[],C).
867
868choose_clauses(CIn,[D|T],COut):-
869	member((N,R,S),D),
870	already_present_with_a_different_head(N,R,S,CIn),!,
871	choose_a_head(N,R,S,CIn,C1),
872	choose_clauses(C1,T,COut).
873
874
875choose_clauses(CIn,[D|T],COut):-
876	member((N,R,S),D),
877	new_head(N,R,S,N1),
878	\+ already_present(N1,R,S,CIn),
879	impose_dif_cons(R,S,CIn),
880	choose_clauses([(N1,R,S)|CIn],T,COut).
881
882choose_clausesc(C,[],C,P,P).
883
884choose_clausesc(CIn,[D|T],COut,P0,P1):-
885	member((N,R,S),D),
886	already_present_with_a_different_head(N,R,S,CIn),!,
887	choose_a_headc(N,R,S,CIn,C1,P0,P2),
888	choose_clausesc(C1,T,COut,P2,P1).
889
890
891choose_clausesc(CIn,[D|T],COut,P0,P1):-
892	member((N,R,S),D),
893	new_head(N,R,S,N1),
894	\+ already_present(N1,R,S,CIn),
895	impose_dif_cons(R,S,CIn),
896	rule_by_num(R,S,_Numbers,Head,_Body),
897	nth0(N1, Head, (_H:P), _Rest),
898	P2 is P0*P,
899	choose_clausesc([(N1,R,S)|CIn],T,COut,P2,P1).
900
901
902choose_clauses_DB(C,[],C).
903
904choose_clauses_DB(CIn,[D|T],COut):-
905        member((N,R,S),D),
906	ground((N,R,S)),
907	already_present_with_a_different_head(N,R,S,CIn),!,
908	choose_a_head(N,R,S,CIn,C1),
909	choose_clauses_DB(C1,T,COut).
910
911choose_clauses_DB(CIn,[D|T],COut):-
912        member((N,R,S),D),
913	ground((N,R,S)),!,
914	new_head(N,R,S,N1),
915	\+ already_present(N1,R,S,CIn),
916	impose_dif_cons(R,S,CIn),
917	choose_clauses_DB([(N1,R,S)|CIn],T,COut).
918
919
920impose_dif_cons(_R,_S,[]):-!.
921
922impose_dif_cons(R,S,[(_NH,R,SH)|T]):-!,
923	dif(S,SH),
924	impose_dif_cons(R,S,T).
925
926impose_dif_cons(R,S,[_H|T]):-
927	impose_dif_cons(R,S,T).
928
929/* instantiation_present_with_the_same_head(N,R,S,C)
930takes rule R with substitution S and selected head N and a C set
931and asserts dif constraints for all the clauses in C of which RS
932is an instantitation and have the same head selected */
933instantiation_present_with_the_same_head(_N,_R,_S,[]).
934
935instantiation_present_with_the_same_head(N,R,S,[(NH,R,SH)|T]):-
936	\+ \+ S=SH,!,
937	dif_head_or_subs(N,R,S,NH,SH,T).
938
939instantiation_present_with_the_same_head(N,R,S,[_H|T]):-
940	instantiation_present_with_the_same_head(N,R,S,T).
941
942dif_head_or_subs(N,R,S,NH,_SH,T):-
943	dif(N,NH),
944	instantiation_present_with_the_same_head(N,R,S,T).
945
946dif_head_or_subs(N,R,S,N,SH,T):-
947	dif(S,SH),
948	instantiation_present_with_the_same_head(N,R,S,T).
949
950/* case 1 of Select: a more general rule is present in C with
951a different head, instantiate it */
952choose_a_headc(N,R,S,[(NH,R,SH)|T],[(NH,R,SH)|T],P,P):-
953	S=SH,
954	dif(N,NH).
955
956/* case 2 of Select: a more general rule is present in C with
957a different head, ensure that they do not generate the same
958ground clause */
959choose_a_headc(N,R,S,[(NH,R,SH)|T],[(NH,R,S),(NH,R,SH)|T],P0,P1):-
960	\+ \+ S=SH, S\==SH,
961	dif(N,NH),
962	dif(S,SH),
963	rule_by_num(R,S,_Numbers,Head,_Body),
964	nth0(NH, Head, (_H:P), _Rest),
965	P1 is P0*P.
966
967choose_a_headc(N,R,S,[H|T],[H|T1],P0,P1):-
968	choose_a_headc(N,R,S,T,T1,P0,P1).
969
970/* case 1 of Select: a more general rule is present in C with
971a different head, instantiate it */
972choose_a_head(N,R,S,[(NH,R,SH)|T],[(NH,R,SH)|T]):-
973	S=SH,
974	dif(N,NH).
975
976/* case 2 of Select: a more general rule is present in C with
977a different head, ensure that they do not generate the same
978ground clause */
979choose_a_head(N,R,S,[(NH,R,SH)|T],[(NH,R,S),(NH,R,SH)|T]):-
980	\+ \+ S=SH, S\==SH,
981	dif(N,NH),
982	dif(S,SH).
983
984choose_a_head(N,R,S,[H|T],[H|T1]):-
985	choose_a_head(N,R,S,T,T1).
986
987
988/* select a head different from N for rule R with
989substitution S, return it in N1 */
990new_head(N,R,S,N1):-
991	rule_by_num(R,S,Numbers,Head,_Body),
992	Head\=uniform(_,_,_),!,
993	nth0(N, Numbers, _Elem, Rest),
994	member(N1,Rest).
995
996new_head(N,R,S,N1):-
997	rule_by_num(R,S,Numbers,uniform(_A:1/Tot,_L,_Number),_Body),
998	listN(0,Tot,Numbers),
999	nth0(N, Numbers, _Elem, Rest),
1000	member(N1,Rest).
1001
1002already_present_with_a_different_head(N,R,S,[(NH,R,SH)|_T]):-
1003	\+ \+ S=SH,NH \= N.
1004
1005already_present_with_a_different_head(N,R,S,[_H|T]):-
1006	already_present_with_a_different_head(N,R,S,T).
1007
1008
1009/* checks that a rule R with head N and selection S is already
1010present in C (or a generalization of it is in C) */
1011already_present(N,R,S,[(N,R,SH)|_T]):-
1012	S=SH.
1013
1014already_present(N,R,S,[_H|T]):-
1015	already_present(N,R,S,T).
1016
1017/* rem_dup_lists removes the C sets that are a superset of
1018another C sets further on in the list of C sets */
1019/* rem_dup_lists removes the C sets that are a superset of
1020another C sets further on in the list of C sets */
1021rem_dup_lists([],L,L).
1022
1023rem_dup_lists([H|T],L0,L):-
1024	(member_subset(H,T);member_subset(H,L0)),!,
1025	rem_dup_lists(T,L0,L).
1026
1027rem_dup_lists([H|T],L0,L):-
1028	rem_dup_lists(T,[H|L0],L).
1029
1030member_subset(E,[H|_T]):-
1031	subset_my(H,E),!.
1032
1033member_subset(E,[_H|T]):-
1034	member_subset(E,T).
1035
1036separate_ulbi([],L,L,U,U,I,I):-!.
1037
1038separate_ulbi([([],H)|T],L0,[H|L1],U0,[H|U1],I0,I1):-
1039	!,
1040	separate_ulbi(T,L0,L1,U0,U1,I0,I1).
1041
1042separate_ulbi([(G,H)|T],L0,L1,U0,[H1|U1],I0,[(G,H)|I1]):-
1043        get_ground(H,H1),
1044	separate_ulbi(T,L0,L1,U0,U1,I0,I1).
1045
1046
1047separate_ulb([],L,L,U,U):-!.
1048
1049separate_ulb([H|T],L0,[H|L1],U0,[H|U1]):-
1050	ground(H),!,
1051	separate_ulb(T,L0,L1,U0,U1).
1052
1053separate_ulb([H|T],L0,L1,U0,[H1|U1]):-
1054        get_ground(H,H1),
1055	separate_ulb(T,L0,L1,U0,U1).
1056
1057
1058separate_ulbc([],L,L,P,P):-!.
1059
1060separate_ulbc([(_H,P,true)|T],L0,L1,P0,P1):-!,
1061	P2 is P0+P,
1062	separate_ulbc(T,L0,L1,P2,P1).
1063
1064separate_ulbc([(H,_P,false)|T],L0,[H|L1],P0,P1):-
1065	separate_ulbc(T,L0,L1,P0,P1).
1066
1067get_ground([],[]):-!.
1068
1069get_ground([H|T],[H|T1]):-
1070	ground(H),!,
1071	get_ground(T,T1).
1072
1073get_ground([_H|T],T1):-
1074	get_ground(T,T1).
1075
1076
1077/* predicates for building the formula to be converted into a BDD */
1078
1079/* build_formula(LC,Formula,VarIn,VarOut) takes as input a set of C sets
1080LC and a list of Variables VarIn and returns the formula and a new list
1081of variables VarOut
1082Formula is of the form [Term1,...,Termn]
1083Termi is of the form [Factor1,...,Factorm]
1084Factorj is of the form (Var,Value) where Var is the index of
1085the multivalued variable Var and Value is the index of the value
1086*/
1087build_formula([],[],Var,Var,C,C).
1088
1089build_formula([D|TD],[F|TF],VarIn,VarOut,C0,C1):-
1090	length(D,NC),
1091	C2 is C0+NC,
1092	build_term(D,F,VarIn,Var1),
1093	build_formula(TD,TF,Var1,VarOut,C2,C1).
1094
1095build_formula([],[],Var,Var).
1096
1097build_formula([D|TD],[F|TF],VarIn,VarOut):-
1098	build_term(D,F,VarIn,Var1),
1099	build_formula(TD,TF,Var1,VarOut).
1100
1101
1102build_term([],[],Var,Var).
1103
1104build_term([(_,pruned,_)|TC],TF,VarIn,VarOut):-!,
1105	build_term(TC,TF,VarIn,VarOut).
1106
1107build_term([(N,R,S)|TC],[[NVar,N]|TF],VarIn,VarOut):-
1108	(nth0_eq(0,NVar,VarIn,(R,S))->
1109		Var1=VarIn
1110	;
1111		append(VarIn,[(R,S)],Var1),
1112		length(VarIn,NVar)
1113	),
1114	build_term(TC,TF,Var1,VarOut).
1115
1116/* nth0_eq(PosIn,PosOut,List,El) takes as input a List,
1117an element El and an initial position PosIn and returns in PosOut
1118the position in the List that contains an element exactly equal to El
1119*/
1120nth0_eq(N,N,[H|_T],El):-
1121	H==El,!.
1122
1123nth0_eq(NIn,NOut,[_H|T],El):-
1124	N1 is NIn+1,
1125	nth0_eq(N1,NOut,T,El).
1126
1127/* var2numbers converts a list of couples (Rule,Substitution) into a list
1128of triples (N,NumberOfHeadsAtoms,ListOfProbabilities), where N is an integer
1129starting from 0 */
1130var2numbers([],_N,[]).
1131
1132var2numbers([(R,S)|T],N,[[N,ValNumber,Probs]|TNV]):-
1133	find_probs(R,S,Probs),
1134	length(Probs,ValNumber),
1135	N1 is N+1,
1136	var2numbers(T,N1,TNV).
1137
1138find_probs(R,S,Probs):-
1139	rule_by_num(R,S,_N,Head,_Body),
1140	get_probs(Head,Probs).
1141
1142get_probs(uniform(_A:1/Num,_P,_Number),ListP):-
1143	Prob is 1/Num,
1144	list_el(Num,Prob,ListP).
1145
1146get_probs([],[]).
1147
1148get_probs([_H:P|T],[P1|T1]):-
1149	P1 is P,
1150	get_probs(T,T1).
1151
1152list_el(0,_P,[]):-!.
1153
1154list_el(N,P,[P|T]):-
1155	N1 is N-1,
1156	list_el(N1,P,T).
1157
1158/* end of predicates for building the formula to be converted into a BDD */list_el(0,_P,[]):-!.
1159
1160
1161/* start of predicates for parsing an input file containing a program */
1162
1163/* p(File) parses the file File.cpl. It can be called more than once without
1164exiting yap */
1165p(File):-
1166	parse(File).
1167
1168parse(File):-
1169	atom_concat(File,'.cpl',FilePl),
1170	open(FilePl,read,S),
1171	read_clauses(S,C),
1172	close(S),
1173        retractall(rule_by_num(_,_,_,_,_)),
1174        retractall(rule(_,_,_,_,_,_,_,_)),
1175        retractall(def_rule(_,_)),
1176	retractall(rule_uniform(_,_,_,_,_,_,_,_)),
1177	process_clauses(C,1).
1178
1179process_clauses([(end_of_file,[])],_N):-!.
1180
1181process_clauses([((H:-B),V)|T],N):-
1182	H=uniform(A,P,L),!,
1183	list2and(BL,B),
1184	process_body(BL,V,V1),
1185	remove_vars([P],V1,V2),
1186	append(BL,[length(L,Tot),nth0(Number,L,P)],BL1),
1187	append(V2,['Tot'=Tot],V3),
1188	assertz(rule_by_num(N,V3,_NH,uniform(A:1/Tot,L,Number),BL1)),
1189	assertz(rule_uniform(A,N,V3,_NH,1/Tot,L,Number,BL1)),
1190	N1 is N+1,
1191	process_clauses(T,N1).
1192
1193process_clauses([((H:-B),V)|T],N):-
1194	H=(_;_),!,
1195	list2or(HL1,H),
1196	process_head(HL1,HL),
1197	list2and(BL,B),
1198	process_body(BL,V,V1),
1199	length(HL,LH),
1200	listN(0,LH,NH),
1201	assert_rules(HL,0,HL,BL,NH,N,V1),
1202	assertz(rule_by_num(N,V1,NH,HL,BL)),
1203	N1 is N+1,
1204	process_clauses(T,N1).
1205
1206process_clauses([((H:-B),V)|T],N):-
1207	H=(_:_),!,
1208	list2or(HL1,H),
1209	process_head(HL1,HL),
1210	list2and(BL,B),
1211	process_body(BL,V,V1),
1212	length(HL,LH),
1213	listN(0,LH,NH),
1214	assert_rules(HL,0,HL,BL,NH,N,V1),
1215	assertz(rule_by_num(N,V1,NH,HL,BL)),
1216	N1 is N+1,
1217	process_clauses(T,N1).
1218
1219process_clauses([((H:-B),_V)|T],N):-!,
1220	list2and(BL,B),
1221	assert(def_rule(H,BL)),
1222	process_clauses(T,N).
1223
1224process_clauses([(H,V)|T],N):-
1225	H=(_;_),!,
1226	list2or(HL1,H),
1227	process_head(HL1,HL),
1228	length(HL,LH),
1229	listN(0,LH,NH),
1230	assert_rules(HL,0,HL,[],NH,N,V),
1231	assertz(rule_by_num(N,V,NH,HL,[])),
1232	N1 is N+1,
1233	process_clauses(T,N1).
1234
1235process_clauses([(H,V)|T],N):-
1236	H=(_:_),!,
1237	list2or(HL1,H),
1238	process_head(HL1,HL),
1239	length(HL,LH),
1240	listN(0,LH,NH),
1241	assert_rules(HL,0,HL,[],NH,N,V),
1242	assertz(rule_by_num(N,V,NH,HL,[])),
1243	N1 is N+1,
1244	process_clauses(T,N1).
1245
1246process_clauses([(H,_V)|T],N):-
1247	assert(def_rule(H,[])),
1248	process_clauses(T,N).
1249
1250assert_rules([],_Pos,_HL,_BL,_Nh,_N,_V1):-!.
1251
1252assert_rules(['':_P],_Pos,_HL,_BL,_Nh,_N,_V1):-!.
1253
1254assert_rules([H:P|T],Pos,HL,BL,NH,N,V1):-
1255	assertz(rule(H,P,Pos,N,V1,NH,HL,BL)),
1256	Pos1 is Pos+1,
1257	assert_rules(T,Pos1,HL,BL,NH,N,V1).
1258
1259
1260/* if the annotation in the head are not ground, the null atom is not added
1261and the eventual formulas are not evaluated */
1262
1263process_head(HL,NHL):-
1264	(ground_prob(HL)->
1265		process_head_ground(HL,0,NHL)
1266	;
1267		NHL=HL
1268	).
1269
1270ground_prob([]).
1271
1272ground_prob([_H:PH|T]):-
1273	ground(PH),
1274	ground_prob(T).
1275
1276process_head_ground([H:PH],P,[H:PH1|Null]):-
1277	PH1 is PH,
1278	PNull is 1-P-PH1,
1279	setting(epsilon_parsing,Eps),
1280	EpsNeg is - Eps,
1281	PNull > EpsNeg,
1282	(PNull>Eps->
1283		Null=['':PNull]
1284	;
1285		Null=[]
1286	).
1287
1288process_head_ground([H:PH|T],P,[H:PH1|NT]):-
1289	PH1 is PH,
1290	P1 is P+PH1,
1291	process_head_ground(T,P1,NT).
1292
1293/* setof must have a goal of the form B^G where B is a term containing the existential variables */
1294process_body([],V,V).
1295
1296process_body([setof(A,B^_G,_L)|T],VIn,VOut):-!,
1297	get_var(A,VA),
1298	get_var(B,VB),
1299	remove_vars(VA,VIn,V1),
1300	remove_vars(VB,V1,V2),
1301	process_body(T,V2,VOut).
1302
1303process_body([setof(A,_G,_L)|T],VIn,VOut):-!,
1304	get_var(A,VA),
1305	remove_vars(VA,VIn,V1),
1306	process_body(T,V1,VOut).
1307
1308process_body([bagof(A,B^_G,_L)|T],VIn,VOut):-!,
1309	get_var(A,VA),
1310	get_var(B,VB),
1311	remove_vars(VA,VIn,V1),
1312	remove_vars(VB,V1,V2),
1313	process_body(T,V2,VOut).
1314
1315process_body([bagof(A,_G,_L)|T],VIn,VOut):-!,
1316	get_var(A,VA),
1317	remove_vars(VA,VIn,V1),
1318	process_body(T,V1,VOut).
1319
1320process_body([_H|T],VIn,VOut):-!,
1321	process_body(T,VIn,VOut).
1322
1323get_var_list([],[]).
1324
1325get_var_list([H|T],[H|T1]):-
1326	var(H),!,
1327	get_var_list(T,T1).
1328
1329get_var_list([H|T],VarOut):-!,
1330	get_var(H,Var),
1331	append(Var,T1,VarOut),
1332	get_var_list(T,T1).
1333
1334get_var(A,[A]):-
1335	var(A),!.
1336
1337get_var(A,V):-
1338	A=..[_F|Args],
1339	get_var_list(Args,V).
1340
1341remove_vars([],V,V).
1342
1343remove_vars([H|T],VIn,VOut):-
1344	delete_var(H,VIn,V1),
1345	remove_vars(T,V1,VOut).
1346
1347delete_var(_H,[],[]).
1348
1349delete_var(V,[VN=Var|T],[VN=Var|T1]):-
1350	V\==Var,!,
1351	delete_var(V,T,T1).
1352
1353delete_var(_V,[_H|T],T).
1354
1355/* predicates for reading in the program clauses */
1356read_clauses(S,Clauses):-
1357	(setting(ground_body,true)->
1358		read_clauses_ground_body(S,Clauses)
1359	;
1360		read_clauses_exist_body(S,Clauses)
1361	).
1362
1363
1364read_clauses_ground_body(S,[(Cl,V)|Out]):-
1365	read_term(S,Cl,[variable_names(V)]),
1366	(Cl=end_of_file->
1367		Out=[]
1368	;
1369		read_clauses_ground_body(S,Out)
1370	).
1371
1372
1373read_clauses_exist_body(S,[(Cl,V)|Out]):-
1374	read_term(S,Cl,[variable_names(VN)]),
1375	extract_vars_cl(Cl,VN,V),
1376	(Cl=end_of_file->
1377		Out=[]
1378	;
1379		read_clauses_exist_body(S,Out)
1380	).
1381
1382
1383extract_vars_cl(end_of_file,[]).
1384
1385extract_vars_cl(Cl,VN,Couples):-
1386	(Cl=(H:-_B)->
1387		true
1388	;
1389		H=Cl
1390	),
1391	extract_vars(H,[],V),
1392	pair(VN,V,Couples).
1393
1394
1395pair(_VN,[],[]).
1396
1397pair([VN= _V|TVN],[V|TV],[VN=V|T]):-
1398	pair(TVN,TV,T).
1399
1400
1401extract_vars(Var,V0,V):-
1402	var(Var),!,
1403	(member_eq(Var,V0)->
1404		V=V0
1405	;
1406		append(V0,[Var],V)
1407	).
1408
1409extract_vars(Term,V0,V):-
1410	Term=..[_F|Args],
1411	extract_vars_list(Args,V0,V).
1412
1413
1414extract_vars_list([],V,V).
1415
1416extract_vars_list([Term|T],V0,V):-
1417	extract_vars(Term,V0,V1),
1418	extract_vars_list(T,V1,V).
1419
1420
1421listN(N,N,[]):-!.
1422
1423listN(NIn,N,[NIn|T]):-
1424	N1 is NIn+1,
1425	listN(N1,N,T).
1426/* end of predicates for parsing an input file containing a program */
1427
1428/* start of utility predicates */
1429list2or([X],X):-
1430	X\=;(_,_),!.
1431
1432list2or([H|T],(H ; Ta)):-!,
1433	list2or(T,Ta).
1434
1435list2and([X],X):-
1436	X\=(_,_),!.
1437
1438list2and([H|T],(H,Ta)):-!,
1439	list2and(T,Ta).
1440
1441member_eq(A,[H|_T]):-
1442	A==H,!.
1443
1444member_eq(A,[_H|T]):-
1445	member_eq(A,T).
1446
1447subset_my([],_).
1448
1449subset_my([H|T],L):-
1450	member_eq(H,L),
1451	subset_my(T,L).
1452
1453remove_duplicates_eq([],[]).
1454
1455remove_duplicates_eq([H|T],T1):-
1456	member_eq(H,T),!,
1457	remove_duplicates_eq(T,T1).
1458
1459remove_duplicates_eq([H|T],[H|T1]):-
1460	remove_duplicates_eq(T,T1).
1461
1462builtin(_A is _B).
1463builtin(_A > _B).
1464builtin(_A < _B).
1465builtin(_A >= _B).
1466builtin(_A =< _B).
1467builtin(_A =:= _B).
1468builtin(_A =\= _B).
1469builtin(true).
1470builtin(false).
1471builtin(_A = _B).
1472builtin(_A==_B).
1473builtin(_A\=_B).
1474builtin(_A\==_B).
1475builtin(length(_L,_N)).
1476builtin(member(_El,_L)).
1477builtin(average(_L,_Av)).
1478builtin(max_list(_L,_Max)).
1479builtin(min_list(_L,_Max)).
1480builtin(nth0(_,_,_)).
1481builtin(nth(_,_,_)).
1482average(L,Av):-
1483	sum_list(L,Sum),
1484	length(L,N),
1485	Av is Sum/N.
1486
1487clique(Graph,Clique):-
1488	vertices(Graph,Candidates),
1489	extend_cycle(Graph,Candidates,[],[],Clique).
1490
1491extend_cycle(G,[H|T],Not,CS,CSOut):-
1492	neighbours(H, G, Neigh),
1493	intersection(Neigh,T,NewCand),
1494	intersection(Neigh,Not,NewNot),
1495	extend(G,NewCand,NewNot,[H|CS],CSOut).
1496
1497extend_cycle(G,[H|T],Not,CS,CSOut):-
1498	extend_cycle(G,T,[H|Not],CS,CSOut).
1499
1500extend(_G,[],[],CompSub,CompSub):-!.
1501
1502extend(G,Cand,Not,CS,CSOut):-
1503	extend_cycle(G,Cand,Not,CS,CSOut).
1504
1505/* set(Par,Value) can be used to set the value of a parameter */
1506set(Parameter,Value):-
1507	retract(setting(Parameter,_)),
1508	assert(setting(Parameter,Value)).
1509
1510/* end of utility predicates */
1511