18
22:- multifile setting_trill_default/2. 23setting_trill_default(det_rules,[o_rule,and_rule,unfold_rule,add_exists_rule,forall_rule,forall_plus_rule,exists_rule,min_rule]).
24setting_trill_default(nondet_rules,[or_rule,max_rule,ch_rule]).
25
26set_up(M):-
27 utility_translation:set_up(M),
28 init_delta(M),
29 M:(dynamic exp_found/2, setting_trill/2),
30 retractall(M:setting_trill(_,_)).
31 32
33clean_up(M):-
34 utility_translation:clean_up(M),
35 M:(dynamic exp_found/2, setting_trill/2),
36 retractall(M:exp_found(_,_)),
37 retractall(M:setting_trill(_,_)).
38
42
44find_n_explanations(M,QueryType,QueryArgs,Expls,all,Opt):-
45 !, 46 findall(Expl,find_single_explanation(M,QueryType,QueryArgs,Expl,Opt),Expls).
47
49find_n_explanations(M,QueryType,QueryArgs,Expl,bt,Opt):-
50 !, 51 find_single_explanation(M,QueryType,QueryArgs,Expl,Opt).
52
54find_n_explanations(M,QueryType,QueryArgs,Expls,N,Opt):-
55 (number(N) -> 56 (findnsols(N,Expl,find_single_explanation(M,QueryType,QueryArgs,Expl,Opt),Expls),!) 57 ;
58 (print_message(warning,wrong_number_max_expl),!,false)
59 ).
60
61
63all_sub_class_int(M:ClassEx,SupClassEx,Exps):-
64 all_unsat_int(M:intersectionOf([ClassEx,complementOf(SupClassEx)]),Exps).
65
66all_instanceOf_int(M:ClassEx,IndEx,Exps):-
67 findall(Expl,instanceOf(M:ClassEx,IndEx,Expl),Exps).
68
69all_property_value_int(M:PropEx,Ind1Ex,Ind2Ex,Exps):-
70 findall(Expl,property_value(M:PropEx,Ind1Ex,Ind2Ex,Expl),Exps).
71
72all_unsat_int(M:ConceptEx,Exps):-
73 findall(Expl,unsat_internal(M:ConceptEx,Expl),Exps).
74
75
76all_inconsistent_theory_int(M:Exps):-
77 findall(Expl,inconsistent_theory(M:Expl),Exps).
78
79
80compute_prob_and_close(M,Exps,Prob):-
81 compute_prob(M,Exps,Prob),!.
82
84check_and_close(_,Expl0,Expl):-
85 dif(Expl0,[]),
86 sort(Expl0,Expl).
87
88is_expl(M,Expl):-
89 dif(Expl,[]),
90 dif(Expl,[[]]),
91 initial_expl(M,EExpl),
92 dif(Expl,EExpl).
93
94
96find_expls(M,[],Q,E):-
97 98 99 find_expls_from_choice_point_list(M,Q,E).
100
101find_expls(M,[],['inconsistent','kb'],E):-!,
102 findall(Exp,M:exp_found(['inconsistent','kb'],Exp),Expl0),
103 remove_supersets(Expl0,Expl),!,
104 member(E,Expl).
105
106find_expls(M,[],_Q,_):-
107 M:exp_found(['inconsistent','kb'],_),!,
108 print_message(warning,inconsistent),!,false.
109
110find_expls(M,[],Q,E):-
111 findall(Exp,M:exp_found(Q,Exp),Expl0),
112 remove_supersets(Expl0,Expl),!,
113 member(E,Expl).
114
116find_expls(M,[Tab|_T],Q0,E):- 117 get_clashes(Tab,Clashes),
118 member(Clash,Clashes),
119 clash(M,Clash,Tab,EL0),
120 member(E0-CPs0,EL0),
121 sort(CPs0,CPs1),
122 sort(E0,E),
123 124 125 consistency_check(CPs1,CPs2,Q0,Q),
126 (dif(CPs2,[]) ->
127 (
128 get_latest_choice(CPs2,ID,Choice),
129 subtract(CPs1,[cpp(ID,Choice)],CPs), 130 update_choice_point_list(M,ID,Choice,E,CPs),
131 fail
132 )
133 ;
134 ( 135 136 assert(M:exp_found(Q,E)), 137 fail
138 )
139 ).
140
141find_expls(M,[_Tab|T],Query,Expl):-
142 143 find_expls(M,T,Query,Expl).
144
145
146combine_expls_from_nondet_rules(M,Q0,cp(_,_,_,_,_,Expl),E):- 147 check_non_empty_choice(Expl,ExplList),
148 and_all_f(M,ExplList,ExplanationsList),
149 150 member(E0-Choices0,ExplanationsList),
151 sort(E0,E),
152 sort(Choices0,Choices1),
153 154 155 consistency_check(Choices1,Choices,Q0,Q),
156 (
157 dif(Choices,[]) ->
158 (
159 160 get_latest_choice(Choices,ID,Choice),
161 subtract(Choices0,[cpp(ID,Choice)],CPs), 162 update_choice_point_list(M,ID,Choice,E,CPs),
163 fail 164 ) ;
165 (
166 167 168 assert(M:exp_found(Q,E)),
169 fail
170 )
171 ).
172
173find_expls_from_choice_point_list(M,QI,E):-
174 extract_choice_point_list(M,CP),
175 (
176 combine_expls_from_nondet_rules(M,QI,CP,E) ;
177 find_expls_from_choice_point_list(M,QI,E)
178 ).
179
180
181check_non_empty_choice(Expl,ExplList):-
182 dict_pairs(Expl,_,PairsList),
183 findall(Ex,member(_-Ex,PairsList),ExplList),
184 \+ memberchk([],ExplList).
185
186
187check_presence_of_other_choices([],[],[]).
188
189check_presence_of_other_choices([E-[]|ExplanationsList],[E|Explanations],Choices):- !,
190 check_presence_of_other_choices(ExplanationsList,Explanations,Choices).
191
192check_presence_of_other_choices([E-CP|ExplanationsList],[E|Explanations],[CP|Choices]):-
193 check_presence_of_other_choices(ExplanationsList,Explanations,Choices).
194
195check_CP([],_).
196
197check_CP([cp(CP,N)|CPT],L):-
198 findall(cp,member(_-[cp(CP,N)|CPT],L),ExplPartsList),
199 length(ExplPartsList,N),
200 check_CP(CPT,L).
201
202
203not_already_found(_M,[],_Q,_E):-!.
204
205not_already_found(_M,[H|_T],_Q,E):-
206 subset(H,E),!,
207 fail.
208
209not_already_found(M,[H|_T],Q,E):-
210 subset(E,H),!,
211 retract(M:exp_found(Q,H)).
212
213not_already_found(M,[_H|T],Q,E):-
214 not_already_found(M,T,Q,E).
215
216
217get_latest_choice([],0,0).
218
219get_latest_choice(CPs,ID,Choice):-
220 get_latest_choice_point(CPs,0,ID),
221 get_latest_choice_of_cp(CPs,ID,0,Choice).
222
223get_latest_choice_point([],ID,ID).
224
225get_latest_choice_point([cpp(ID0,_)|T],ID1,ID):-
226 ID2 is max(ID1,ID0),
227 get_latest_choice_point(T,ID2,ID).
228
229
230get_latest_choice_of_cp([],_,C,C).
231
232get_latest_choice_of_cp([cpp(ID,C0)|T],ID,C1,C):- !,
233 C2 is max(C1,C0),
234 get_latest_choice_of_cp(T,ID,C2,C).
235
236get_latest_choice_of_cp([_|T],ID,C1,C):-
237 get_latest_choice_of_cp(T,ID,C1,C).
238
239
240remove_supersets([H|T],ExplanationsList):-
241 remove_supersets([H],T,ExplanationsList).
242
243remove_supersets(E,[],E).
244
245remove_supersets(E0,[H|T],ExplanationsList):-
246 remove_supersets_int(E0,H,E),
247 remove_supersets(E,T,ExplanationsList).
248
249remove_supersets_int(E0,H,E0):-
250 memberchk(H,E0),!.
251
252remove_supersets_int(E0,H,E0):-
253 member(H1,E0),
254 subset(H1,H),!.
255
256remove_supersets_int(E0,H,E):-
257 member(H1,E0),
258 subset(H,H1),!,
259 nth0(_,E0,H1,E1),
260 remove_supersets_int(E1,H,E).
261
262remove_supersets_int(E,H,[H|E]).
263
264
267consistency_check(CPs,CPs,['inconsistent','kb'],['inconsistent','kb']):- !.
268
269consistency_check(CPs0,CPs,Q0,Q):-
270 (nth0(_,CPs0,qp,CPs) -> (Q=Q0) ; (Q=['inconsistent','kb'],CPs=CPs0)).
271
272
274
278
280findClassAssertion4OWLNothing(_M,ABox,Expl):-
281 findClassAssertion('http://www.w3.org/2002/07/owl#Nothing',_Ind,Expl,ABox).
282
283
286
288:- multifile clash/4. 289
290clash(M,maxCardinality(N,S,C)-Ind,Tab,Expl):-
291 get_abox(Tab,ABox),
292 293 findClassAssertion(maxCardinality(N,S,C),Ind,Expl1,ABox),
294 s_neighbours(M,Ind,S,Tab,SN),
295 individual_class_C(SN,C,ABox,SNC),
296 length(SNC,LSS),
297 LSS @> N,
298 make_expl(M,Ind,S,SNC,Expl1,ABox,Expl).
299
300clash(M,maxCardinality(N,S)-Ind,Tab,Expl):-
301 get_abox(Tab,ABox),
302 303 findClassAssertion(maxCardinality(N,S),Ind,Expl1,ABox),
304 s_neighbours(M,Ind,S,Tab,SN),
305 length(SN,LSS),
306 LSS @> N,
307 make_expl(M,Ind,S,SN,Expl1,ABox,Expl).
308
309clash(M,exactCardinality(N,S,C)-Ind,Tab,Expl):-
310 get_abox(Tab,ABox),
311 312 findClassAssertion(exactCardinality(N,S,C),Ind,Expl1,ABox),
313 s_neighbours(M,Ind,S,Tab,SN),
314 individual_class_C(SN,C,ABox,SNC),
315 length(SNC,LSS),
316 dif(LSS,N),
317 make_expl(M,Ind,S,SNC,Expl1,ABox,Expl).
318
319clash(M,exactCardinality(N,S)-Ind,Tab,Expl):-
320 get_abox(Tab,ABox),
321 322 findClassAssertion(exactCardinality(N,S),Ind,Expl1,ABox),
323 s_neighbours(M,Ind,S,Tab,SN),
324 length(SN,LSS),
325 dif(LSS,N),
326 make_expl(M,Ind,S,SN,Expl1,ABox,Expl).
327
328
329
330:- multifile check_clash/3. 331
332check_clash(M,maxCardinality(N,S,C)-Ind,Tab):-
333 get_abox(Tab,ABox),
334 335 s_neighbours(M,Ind,S,Tab,SN),
336 individual_class_C(SN,C,ABox,SNC),
337 length(SNC,LSS),
338 LSS @> N,!.
339
340check_clash(M,maxCardinality(N,S)-Ind,Tab):-
341 342 s_neighbours(M,Ind,S,Tab,SN),
343 length(SN,LSS),
344 LSS @> N,!.
345
346check_clash(M,exactCardinality(N,S,C)-Ind,Tab):-
347 get_abox(Tab,ABox),
348 349 s_neighbours(M,Ind,S,Tab,SN),
350 individual_class_C(SN,C,ABox,SNC),
351 length(SNC,LSS),
352 dif(LSS,N),!.
353
354check_clash(M,exactCardinality(N,S)-Ind,Tab):-
355 356 s_neighbours(M,Ind,S,Tab,SN),
357 length(SN,LSS),
358 dif(LSS,N),!.
359
361
362make_expl(_,_,_,[],Expl,_,Expl).
363
364make_expl(M,Ind,S,[H|T],Expl0,ABox,Expl):-
365 findPropertyAssertion(S,Ind,H,Expl2,ABox),
366 and_f(M,Expl2,Expl0,Expl1),
367 make_expl(M,Ind,S,T,Expl1,ABox,Expl).
369
370
374
379
382:- multifile find_neg_class/2. 383
384find_neg_class(exactCardinality(N,R,C),unionOf([maxCardinality(NMax,R,C),minCardinality(NMin,R,C)])):-
385 NMax is N - 1,
386 NMin is N + 1.
387
388find_neg_class(minCardinality(N,R,C),maxCardinality(NMax,R,C)):-
389 NMax is N - 1.
390
391find_neg_class(maxCardinality(N,R,C),minCardinality(NMin,R,C)):-
392 NMin is N + 1.
393
395:- multifile find_sub_sup_class/4. 396
398find_sub_sup_class(M,exactCardinality(N,R),exactCardinality(N,S),subPropertyOf(R,S)):-
399 M:subPropertyOf(R,S).
400
402find_sub_sup_class(M,exactCardinality(N,R,C),exactCardinality(N,R,D),Ax):-
403 find_sub_sup_class(M,C,D,Ax),
404 atomic(D).
405
407find_sub_sup_class(M,exactCardinality(N,R,C),exactCardinality(N,S,C),subPropertyOf(R,S)):-
408 M:subPropertyOf(R,S).
409
411find_sub_sup_class(M,maxCardinality(N,R),maxCardinality(N,S),subPropertyOf(R,S)):-
412 M:subPropertyOf(R,S).
413
415find_sub_sup_class(M,maxCardinality(N,R,C),maxCardinality(N,R,D),Ax):-
416 find_sub_sup_class(M,C,D,Ax),
417 atomic(D).
418
420find_sub_sup_class(M,maxCardinality(N,R,C),maxCardinality(N,S,C),subPropertyOf(R,S)):-
421 M:subPropertyOf(R,S).
422
424find_sub_sup_class(M,minCardinality(N,R),minCardinality(N,S),subPropertyOf(R,S)):-
425 M:subPropertyOf(R,S).
426
428find_sub_sup_class(M,minCardinality(N,R,C),minCardinality(N,R,D),Ax):-
429 find_sub_sup_class(M,C,D,Ax),
430 atomic(D).
431
433find_sub_sup_class(M,minCardinality(N,R,C),minCardinality(N,S,C),subPropertyOf(R,S)):-
434 M:subPropertyOf(R,S).
435
437
442modify_ABox(_,Tab,sameIndividual(LF),_Expl1,Tab):-
443 length(LF,1),!.
444
445modify_ABox(M,Tab0,sameIndividual(LF),Expl1,Tab):-
446 get_abox(Tab0,ABox0),
447 ( find((sameIndividual(L),Expl0),ABox0) ->
448 ( sort(L,LS),
449 sort(LF,LFS),
450 LS = LFS,!,
451 absent(Expl0,Expl1,Expl),
452 remove_from_abox(ABox0,[(sameIndividual(L),Expl0)],ABox),
453 Tab1=Tab0
454 )
455 ;
456 (ABox = ABox0,Expl = Expl1,L = LF,
457 add_clash_to_tableau(M,Tab0,sameIndividual(LF),Tab1))
458 ),
459 set_abox(Tab1,[(sameIndividual(L),Expl)|ABox],Tab).
460
461modify_ABox(_,Tab,differentIndividuals(LF),_Expl1,Tab):-
462 length(LF,1),!.
463
464modify_ABox(M,Tab0,differentIndividuals(LF),Expl1,Tab):-
465 get_abox(Tab0,ABox0),
466 ( find((differentIndividuals(L),Expl0),ABox0) ->
467 ( sort(L,LS),
468 sort(LF,LFS),
469 LS = LFS,!,
470 absent(Expl0,Expl1,Expl),
471 remove_from_abox(ABox0,[(differentIndividuals(L),Expl0)],ABox),
472 Tab1=Tab0
473 )
474 ;
475 (ABox = ABox0,Expl = Expl1,L = LF,
476 add_clash_to_tableau(M,Tab0,differentIndividuals(LF),Tab1))
477 ),
478 set_abox(Tab1,[(differentIndividuals(L),Expl)|ABox],Tab).
479
480modify_ABox(M,Tab0,C,Ind,Expl1,Tab):-
481 get_abox(Tab0,ABox0),
482 ( find((classAssertion(C,Ind),Expl0),ABox0) ->
483 ( absent(Expl0,Expl1,Expl),
484 remove_from_abox(ABox0,(classAssertion(C,Ind),Expl0),ABox),
485 Tab1=Tab0
486 )
487 ;
488 (ABox = ABox0,Expl = Expl1,
489 add_clash_to_tableau(M,Tab0,C-Ind,Tab1))
490 ),
491 set_abox(Tab1,[(classAssertion(C,Ind),Expl)|ABox],Tab2),
492 update_expansion_queue_in_tableau(M,C,Ind,Tab2,Tab).
493
494modify_ABox(M,Tab0,P,Ind1,Ind2,Expl1,Tab):-
495 get_abox(Tab0,ABox0),
496 ( find((propertyAssertion(P,Ind1,Ind2),Expl0),ABox0) ->
497 ( absent(Expl0,Expl1,Expl),
498 remove_from_abox(ABox0,(propertyAssertion(P,Ind1,Ind2),Expl0),ABox),
499 Tab1=Tab0
500 )
501 ;
502 (ABox = ABox0,Expl = Expl1,
503 add_clash_to_tableau(M,Tab0,P-Ind1-Ind2,Tab1))
504 ),
505 set_abox(Tab1,[(propertyAssertion(P,Ind1,Ind2),Expl)|ABox],Tab2),
506 update_expansion_queue_in_tableau(M,P,Ind1,Ind2,Tab2,Tab).
507
509
511notDifferentIndividuals(M,X,Y,ABox):-
512 \+ inAssertDifferentIndividuals(M,X,Y),
513 \+ inABoxDifferentIndividuals(X,Y,ABox).
514
516
517inAssertDifferentIndividuals(M,differentIndividuals(X),differentIndividuals(Y)):-
518 !,
519 M:differentIndividuals(LI),
520 member(X0,X),
521 member(X0,LI),
522 member(Y0,Y),
523 member(Y0,LI).
524
525inAssertDifferentIndividuals(M,X,sameIndividual(Y)):-
526 !,
527 M:differentIndividuals(LI),
528 member(X,LI),
529 member(Y0,Y),
530 member(Y0,LI).
531
532inAssertDifferentIndividuals(M,sameIndividual(X),Y):-
533 !,
534 M:differentIndividuals(LI),
535 member(X0,X),
536 member(X0,LI),
537 member(Y,LI).
538
539inAssertDifferentIndividuals(M,X,Y):-
540 M:differentIndividuals(LI),
541 member(X,LI),
542 member(Y,LI).
543
545
546inABoxDifferentIndividuals(sameIndividual(X),sameIndividual(Y),ABox):-
547 !,
548 find((differentIndividuals(LI),_),ABox),
549 member(X0,X),
550 member(X0,LI),
551 member(Y0,Y),
552 member(Y0,LI).
553
554inABoxDifferentIndividuals(X,sameIndividual(Y),ABox):-
555 !,
556 find((differentIndividuals(LI),_),ABox),
557 member(X,LI),
558 member(Y0,Y),
559 member(Y0,LI).
560
561inABoxDifferentIndividuals(sameIndividual(X),Y,ABox):-
562 !,
563 find((differentIndividuals(LI),_),ABox),
564 member(X0,X),
565 member(X0,LI),
566 member(Y,LI).
567
568inABoxDifferentIndividuals(X,Y,ABox):-
569 find((differentIndividuals(LI),_),ABox),
570 member(X,LI),
571 member(Y,LI).
572
574
575listIntersection([],_,[]).
576
577listIntersection([HX|TX],LCY,TI):-
578 \+ member(HX,LCY),
579 listIntersection(TX,LCY,TI).
580
581listIntersection([HX|TX],LCY,[HX|TI]):-
582 member(HX,LCY),
583 listIntersection(TX,LCY,TI).
584
586
587findExplForClassOf(LC,LI,ABox0,Expl):-
588 member(C,LC),
589 member(I,LI),
590 findClassAssertion(C,I,Expl,ABox0).
592
594
595
599absent(Expl0,Expl1,Expl):- 600 absent0(Expl0,Expl1,Expl),!.
601
603absent0(Expl0,Expl1,Expl):-
604 absent1(Expl0,Expl1,Expl,Added),
605 dif(Added,0).
606
607absent1(Expl,[],Expl,0).
608
609absent1(Expl0,[H-CP|T],[H-CP|Expl],1):-
610 absent2(Expl0,H),!,
611 absent1(Expl0,T,Expl,_).
612
613absent1(Expl0,[_|T],Expl,Added):-
614 absent1(Expl0,T,Expl,Added).
615
616absent2([H-_],Expl):- !,
617 \+ subset(H,Expl).
618
619absent2([H-_|T],Expl):-
620 \+ subset(H,Expl),!,
621 absent2(T,Expl).
622
624
629
639
640
641build_abox(M,Tableau,QueryType,QueryArgs):-
642 retractall(M:final_abox(_)),
643 collect_individuals(M,QueryType,QueryArgs,ConnectedInds),
644 ( dif(ConnectedInds,[]) ->
645 ( findall((classAssertion(Class,Individual),[[classAssertion(Class,Individual)]-[]]),(member(Individual,ConnectedInds),M:classAssertion(Class,Individual)),LCA),
646 findall((propertyAssertion(Property,Subject, Object),[[propertyAssertion(Property,Subject, Object)]-[]]),(member(Subject,ConnectedInds),M:propertyAssertion(Property,Subject, Object),dif('http://www.w3.org/2000/01/rdf-schema#comment',Property)),LPA),
647 648 findall(nominal(NominalIndividual),(member(NominalIndividual,ConnectedInds),M:classAssertion(oneOf(_),NominalIndividual)),LNA),
649 findall((differentIndividuals(Ld),[[differentIndividuals(Ld)]-[]]),(M:differentIndividuals(Ld),intersect(Ld,ConnectedInds)),LDIA),
650 findall((sameIndividual(L),[[sameIndividual(L)]-[]]),(M:sameIndividual(L),intersect(L,ConnectedInds)),LSIA)
651 )
652 ; 653 ( findall((classAssertion(Class,Individual),[[classAssertion(Class,Individual)]-[]]),M:classAssertion(Class,Individual),LCA),
654 findall((propertyAssertion(Property,Subject, Object),[[propertyAssertion(Property,Subject, Object)]-[]]),(M:propertyAssertion(Property,Subject, Object),dif('http://www.w3.org/2000/01/rdf-schema#comment',Property)),LPA),
655 656 findall(nominal(NominalIndividual),M:classAssertion(oneOf(_),NominalIndividual),LNA),
657 findall((differentIndividuals(Ld),[[differentIndividuals(Ld)]-[]]),M:differentIndividuals(Ld),LDIA),
658 findall((sameIndividual(L),[[sameIndividual(L)]-[]]),M:sameIndividual(L),LSIA)
659 )
660 ),
661 new_abox(ABox0),
662 new_tabs(Tabs0),
663 init_expansion_queue(LCA,LPA,ExpansionQueue),
664 init_tableau(ABox0,Tabs0,ExpansionQueue,Tableau0),
665 append([LCA,LDIA,LPA],CreateTabsList),
666 create_tabs(CreateTabsList,Tableau0,Tableau1),
667 append([LCA,LPA,LNA,LDIA],AddAllList),
668 add_all_to_tableau(M,AddAllList,Tableau1,Tableau2),
669 merge_all_individuals(M,LSIA,Tableau2,Tableau3),
670 add_owlThing_list(M,Tableau3,Tableau),
671 !.
672
673
675
681
682and_all_f(M,ExplPartsList,E) :-
683 empty_expl(M,EmptyE),
684 and_all_f(M,ExplPartsList,EmptyE,E).
685
686and_all_f(_,[],E,E) :- !.
687
688and_all_f(M,[H|T],E0,E):-
689 and_f(M,E0,H,E1),
690 and_all_f(M,T,E1,E).
691
692initial_expl(_M,[[]-[]]):-!.
693
694empty_expl(_M,[[]-[]]):-!.
695
696and_f_ax(M,Axiom,F0,F):-
697 and_f(M,[[Axiom]-[]],F0,F).
698
699and_f(_M,[],[],[]):- !.
700
701and_f(_M,[],L,L):- !.
702
703and_f(_M,L,[],L):- !.
704
705and_f(_M,L1,L2,F):-
706 and_f1(L1,L2,[],F).
707
708and_f1([],_,L,L).
709
710and_f1([H1-CP1|T1],L2,L3,L):-
711 and_f2(H1,CP1,L2,L12),
712 append(L3,L12,L4),
713 and_f1(T1,L2,L4,L).
714
715and_f2(_,_,[],[]):- !.
716
717and_f2(L1,CP1,[H2-CP2|T2],[H-CP|T]):-
718 append(L1,H2,H),
719 append(CP1,CP2,CP),
720 and_f2(L1,CP1,T2,T).
721
722or_f([],E,E).
723
724or_f([E0|T],E1,E):-
725 memberchk(E0,E1),!,
726 or_f(T,E1,E).
727
728or_f([E0|T],E1,[E0|E]):-
729 or_f(T,E1,E).
730
736
746init_delta(M):-
747 retractall(M:delta(_,_)),
748 assert(M:delta([],0)).
749
750get_choice_point_id(M,ID):-
751 M:delta(_,ID).
752
754create_choice_point(M,Ind,Rule,Class,Choices,ID0):-
755 init_expl_per_choice(Choices,ExplPerChoice),
756 M:delta(CPList,ID0),
757 ID is ID0 + 1,
758 retractall(M:delta(_,_)),
759 assert(M:delta([cp(ID0,Ind,Rule,Class,Choices,ExplPerChoice)|CPList],ID)).
760
761
762init_expl_per_choice(Choices,ExplPerChoice):-
763 length(Choices,N),
764 init_expl_per_choice_int(0,N,epc{0:[]},ExplPerChoice).
765
766init_expl_per_choice_int(N,N,ExplPerChoice,ExplPerChoice).
767
768init_expl_per_choice_int(N0,N,ExplPerChoice0,ExplPerChoice):-
769 ExplPerChoice1 = ExplPerChoice0.put(N0,[]),
770 N1 is N0 + 1,
771 init_expl_per_choice_int(N1,N,ExplPerChoice1,ExplPerChoice).
772
773
776add_choice_point(_,_,[],[]).
777
778add_choice_point(_,CPP,[Expl-CP0|T0],[Expl-CP|T]):- 779 (
780 dif(CP0,[]) ->
781 (
782 append([CPP],CP0,CP)
783 )
784 ;
785 (
786 CP = [CPP]
787 )
788 ),
789 add_choice_point(_,CPP,T0,T).
790
791
792get_choice_point_list(M,CP):-
793 M:delta(CP,_).
794
(M,CP):-
796 M:delta([CP|CPList],ID),
797 retractall(M:delta(_,_)),
798 assert(M:delta(CPList,ID)).
799
800update_choice_point_list(M,ID,Choice,E,CPs):-
801 M:delta(CPList0,ID0),
802 memberchk(cp(ID,Ind,Rule,Class,Choices,ExplPerChoice0),CPList0),
803 ExplToUpdate = ExplPerChoice0.get(Choice),
804 ( 805 806 807 dif(ExplToUpdate,[]) ->
808 (
809 or_f(ExplToUpdate,[E-CPs],ExplUpdated)
810 ) ;
811 (
812 ExplUpdated=[E-CPs]
813 )
814 ),
815 ExplPerChoice = ExplPerChoice0.put(Choice,ExplUpdated),
816 update_choice_point_list_int(CPList0,cp(ID,Ind,Rule,Class,Choices,ExplPerChoice0),ExplPerChoice,CPList),
817 retractall(M:delta(_,_)),
818 assert(M:delta(CPList,ID0)).
819
820update_choice_point_list_int([],_,_,[]):-
821 writeln("Probably something wrong happened. Please report the problem opening an issue on github!").
822 823
824update_choice_point_list_int([cp(ID,Ind,Rule,Class,Choices,ExplPerChoice0)|T],
825 cp(ID,Ind,Rule,Class,Choices,ExplPerChoice0),ExplPerChoice,
826 [cp(ID,Ind,Rule,Class,Choices,ExplPerChoice)|T]) :- !.
827
828update_choice_point_list_int([H|T],
829 cp(ID,Ind,Rule,Class,Choices,ExplPerChoice0),ExplPerChoice,
830 [H|T1]):-
831 update_choice_point_list_int(T,cp(ID,Ind,Rule,Class,Choices,ExplPerChoice0),ExplPerChoice,T1).
832
838
839get_bdd_environment(_M,Env):-
840 init(Env).
841
842clean_environment(_M,Env):-
843 end(Env).
844
845
846build_bdd(M,Env,[X],BDD):- !,
847 bdd_and(M,Env,X,BDD).
848
849build_bdd(M,Env, [H|T],BDD):-
850 build_bdd(M,Env,T,BDDT),
851 bdd_and(M,Env,H,BDDH),
852 or(Env,BDDH,BDDT,BDD).
853
854build_bdd(_M,Env,[],BDD):- !,
855 zero(Env,BDD).
856
857
858bdd_and(M,Env,[X],BDDX):-
859 get_prob_ax(M,X,AxN,Prob),!,
860 ProbN is 1-Prob,
861 get_var_n(Env,AxN,[],[Prob,ProbN],VX),
862 equality(Env,VX,0,BDDX),!.
863
864bdd_and(_M,Env,[_X],BDDX):- !,
865 one(Env,BDDX).
866
867bdd_and(M,Env,[H|T],BDDAnd):-
868 get_prob_ax(M,H,AxN,Prob),!,
869 ProbN is 1-Prob,
870 get_var_n(Env,AxN,[],[Prob,ProbN],VH),
871 equality(Env,VH,0,BDDH),
872 bdd_and(M,Env,T,BDDT),
873 and(Env,BDDH,BDDT,BDDAnd).
874
875bdd_and(M,Env,[_H|T],BDDAnd):- !,
876 one(Env,BDDH),
877 bdd_and(M,Env,T,BDDT),
878 and(Env,BDDH,BDDT,BDDAnd)