1/* trill predicates
    2
    3This module performs reasoning over probabilistic description logic knowledge bases.
    4It reads probabilistic knowledge bases in RDF format or in Prolog format, a functional-like
    5sintax based on definitions of Thea library, and answers queries by finding the set 
    6of explanations or computing the probability.
    7
    8[1] http://vangelisv.github.io/thea/
    9
   10See https://github.com/rzese/trill/blob/master/doc/manual.pdf or
   11http://ds.ing.unife.it/~rzese/software/trill/manual.html for
   12details.
   13
   14@author Riccardo Zese
   15@license Artistic License 2.0
   16@copyright Riccardo Zese
   17*/
   18
   19/********************************
   20  SETTINGS
   21*********************************/
   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  %foreach(setting_trill_default(DefaultSetting,DefaultVal),assert(M:setting_trill(DefaultSetting,DefaultVal))).
   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
   39/***********
   40  Utilities for queries
   41 ***********/
   42
   43% findall
   44find_n_explanations(M,QueryType,QueryArgs,Expls,all,Opt):-
   45  !, % CUT so that no other calls to find_explanation can be ran (to avoid running that with variable N)
   46  findall(Expl,find_single_explanation(M,QueryType,QueryArgs,Expl,Opt),Expls).
   47
   48% find one in backtracking
   49find_n_explanations(M,QueryType,QueryArgs,Expl,bt,Opt):-
   50  !, % CUT so that no other calls to find_explanation can be ran (to avoid running that with variable N)
   51  find_single_explanation(M,QueryType,QueryArgs,Expl,Opt).
   52
   53% find_n_sol
   54find_n_explanations(M,QueryType,QueryArgs,Expls,N,Opt):-
   55  (number(N) -> % CUT so that no other calls to find_explanation can be ran
   56    (findnsols(N,Expl,find_single_explanation(M,QueryType,QueryArgs,Expl,Opt),Expls),!) % CUT otherwise findnsols would backtracks to look for another N sols
   57    ;
   58    (print_message(warning,wrong_number_max_expl),!,false)
   59  ).
   60
   61
   62% to find all axplanations for probabilistic queries
   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
   83% checks the explanation
   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
   95% checks if an explanations was already found
   96find_expls(M,[],Q,E):-
   97  %findall(Exp-CPs,M:exp_found([C,I,CPs],Exp),Expl),
   98  %dif(Expl,[]),
   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
  115% checks if an explanations was already found (instance_of version)
  116find_expls(M,[Tab|_T],Q0,E):- %gtrace,  % QueryArgs
  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  % this predicate checks if there are inconsistencies in the KB, i.e., explanations without query placeholder qp
  124  % if it is so, the explanation is labelled as inconsistent kb via Q
  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), %remove cpp from CPs1 so the qp remains inside choice points list
  130    update_choice_point_list(M,ID,Choice,E,CPs),
  131    fail
  132    )
  133    ;
  134    (%findall(Exp,M:exp_found([C,I],Exp),Expl),
  135    %not_already_found(M,Expl,[C,I],E),
  136    assert(M:exp_found(Q,E)), % QueryArgs
  137    fail
  138    )
  139  ).
  140
  141find_expls(M,[_Tab|T],Query,Expl):-
  142  %\+ length(T,0),
  143  find_expls(M,T,Query,Expl).
  144
  145
  146combine_expls_from_nondet_rules(M,Q0,cp(_,_,_,_,_,Expl),E):-%gtrace,
  147  check_non_empty_choice(Expl,ExplList),
  148  and_all_f(M,ExplList,ExplanationsList),
  149  %check_presence_of_other_choices(ExplanationsList,Explanations,Choices),
  150  member(E0-Choices0,ExplanationsList),
  151  sort(E0,E),
  152  sort(Choices0,Choices1),
  153  % this predicate checks if there are inconsistencies in the KB, i.e., explanations without query placeholder qp
  154  % if it is so, the explanation is labelled as inconsistent kb via Q
  155  consistency_check(Choices1,Choices,Q0,Q),
  156  (
  157    dif(Choices,[]) ->
  158    (
  159      %TODO gestione altri cp
  160      get_latest_choice(Choices,ID,Choice),
  161      subtract(Choices0,[cpp(ID,Choice)],CPs), %remove cpp from Choices1 so the qp remains inside choice points list
  162      update_choice_point_list(M,ID,Choice,E,CPs),
  163      fail % to force recursion
  164    ) ;
  165    (
  166      %findall(Exp,M:exp_found([C,I],Exp),ExplFound),
  167      %not_already_found(M,ExplFound,[C,I],E),
  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
  265% this predicate checks if there are inconsistencies in the KB, i.e., explanations with query placeholder qp
  266% if it is so, the explanation is labelled as inconsistent kb
  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
  273/****************************/
  274
  275/****************************
  276  TABLEAU ALGORITHM
  277****************************/
  278
  279% --------------
  280findClassAssertion4OWLNothing(_M,ABox,Expl):-
  281  findClassAssertion('http://www.w3.org/2002/07/owl#Nothing',_Ind,Expl,ABox).
  282
  283
  284%-------------
  285% clash managing
  286
  287%------------
  288:- multifile clash/4.  289
  290clash(M,maxCardinality(N,S,C)-Ind,Tab,Expl):-
  291  get_abox(Tab,ABox),
  292  %write('clash 9'),nl,
  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  %write('clash 10'),nl,
  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  %write('clash 9'),nl,
  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  %write('clash 10'),nl,
  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  %write('clash 9'),nl,
  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  %write('clash 10'),nl,
  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  %write('clash 9'),nl,
  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  %write('clash 10'),nl,
  356  s_neighbours(M,Ind,S,Tab,SN),
  357  length(SN,LSS),
  358  dif(LSS,N),!.
  359
  360% --------------
  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).
  368% --------------
  369
  370
  371/***********
  372  rules
  373************/
  374
  375/*
  376  unfold_rule
  377  ===========
  378*/
  379
  380% ----------------
  381% unionOf, intersectionOf, subClassOf, negation, allValuesFrom, someValuesFrom, exactCardinality(min and max), maxCardinality, minCardinality
  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
  394%-----------------
  395:- multifile find_sub_sup_class/4.  396
  397%role for concepts exactCardinality
  398find_sub_sup_class(M,exactCardinality(N,R),exactCardinality(N,S),subPropertyOf(R,S)):-
  399  M:subPropertyOf(R,S).
  400
  401%concept for concepts exactCardinality
  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
  406%role for concepts exactCardinality
  407find_sub_sup_class(M,exactCardinality(N,R,C),exactCardinality(N,S,C),subPropertyOf(R,S)):-
  408  M:subPropertyOf(R,S).
  409
  410%role for concepts maxCardinality
  411find_sub_sup_class(M,maxCardinality(N,R),maxCardinality(N,S),subPropertyOf(R,S)):-
  412  M:subPropertyOf(R,S).
  413
  414%concept for concepts maxCardinality
  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
  419%role for concepts maxCardinality
  420find_sub_sup_class(M,maxCardinality(N,R,C),maxCardinality(N,S,C),subPropertyOf(R,S)):-
  421  M:subPropertyOf(R,S).
  422
  423%role for concepts minCardinality
  424find_sub_sup_class(M,minCardinality(N,R),minCardinality(N,S),subPropertyOf(R,S)):-
  425  M:subPropertyOf(R,S).
  426
  427%concept for concepts minCardinality
  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
  432%role for concepts minCardinality
  433find_sub_sup_class(M,minCardinality(N,R,C),minCardinality(N,S,C),subPropertyOf(R,S)):-
  434  M:subPropertyOf(R,S).
  435
  436/* ************* */
  437
  438/***********
  439  update abox
  440  utility for tableau
  441************/
  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
  508/* ************* */
  509
  510% -------------------
  511notDifferentIndividuals(M,X,Y,ABox):-
  512  \+ inAssertDifferentIndividuals(M,X,Y),
  513  \+ inABoxDifferentIndividuals(X,Y,ABox).
  514
  515% --------------
  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
  544% ------------------
  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
  573% --------------------
  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
  585% ---------------
  586
  587findExplForClassOf(LC,LI,ABox0,Expl):-
  588  member(C,LC),
  589  member(I,LI),
  590  findClassAssertion(C,I,Expl,ABox0).
  591%  member((classAssertion(C,I),Expl),ABox0).
  592
  593/* ************ */
  594
  595
  596/*  absent
  597  =========
  598*/
  599absent(Expl0,Expl1,Expl):- % Expl0 already present expls, Expl1 new expls to add, Expl the combination of two lists
  600  absent0(Expl0,Expl1,Expl),!.
  601
  602%------------------
  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
  623/* **************** */
  624
  625/*
  626  build_abox
  627  ===============
  628*/
  629
  630/*build_abox(M,ABox):-
  631  findall((classAssertion(Class,Individual),[classAssertion(Class,Individual)]),classAssertion(Class,Individual),LCA),
  632  findall((propertyAssertion(Property,Subject, Object),[propertyAssertion(Property,Subject, Object)]),propertyAssertion(Property,Subject, Object),LPA),
  633  findall((propertyAssertion(Property,Subject,Object),[subPropertyOf(SubProperty,Property,Subject,Object),propertyAssertion(SubProperty,Subject,Object)]),subPropertyOf(SubProperty,Property),LSPA),
  634  new_abox(ABox0),
  635  add_all_to_tableau(LCA,ABox0,ABox1),
  636  add_all_to_tableau(LPA,ABox1,ABox2),
  637  add_all_to_tableau(LSPA,ABox2,ABox).
  638*/
  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      % findall((propertyAssertion(Property,Subject,Object),[subPropertyOf(SubProperty,Property),propertyAssertion(SubProperty,Subject,Object)]),subProp(M,SubProperty,Property,Subject,Object),LSPA),
  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    ; % all the individuals
  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      % findall((propertyAssertion(Property,Subject,Object),[subPropertyOf(SubProperty,Property),propertyAssertion(SubProperty,Subject,Object)]),subProp(M,SubProperty,Property,Subject,Object),LSPA),
  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
  674/* ********** */
  675
  676/**********************
  677
  678  Explanation Management
  679
  680***********************/
  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
  731/**********************
  732
  733Choice Points Management
  734
  735***********************/
  736
  737/*
  738  Initializes delta/2 containing the list of choice points and the number of choice points created.
  739  Every choice point is modeled by the predicate cp/5 containing the ID of the choice point,
  740  the individual and the class that triggered the creation of the choice point,
  741  the rule that created the cp:
  742  - or: or_rule
  743  - mr: max_rule
  744  Also it contains the list of possible choices and the explanations for each choice.
  745*/
  746init_delta(M):-
  747  retractall(M:delta(_,_)),
  748  assert(M:delta([],0)).
  749
  750get_choice_point_id(M,ID):-
  751  M:delta(_,ID).
  752
  753% Creates a new choice point and adds it to the delta/2 set of choice points.
  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
  774% cpp/2 is the choice point pointer. It contains the CP's ID (from the list of choice points delta/2)
  775% and the pointer of the choice maide at the choice point
  776add_choice_point(_,_,[],[]). 
  777
  778add_choice_point(_,CPP,[Expl-CP0|T0],[Expl-CP|T]):- %CPP=cpp(CPID,N)
  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
  795extract_choice_point_list(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  ( % if the set of explanations for the choice is empty it simply adds the new explanation -> union i.e., append([E-CPs],ExplToUpdate,ExplUpdated)
  805    % otherwise it adds only new explanations dropping those that are already present or those that are supersets of 
  806    % already present explanations -> absent(ExplToUpdate,[E-CPs],ExplUpdated)
  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  % It should never arrive here.
  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
  833/**********************
  834
  835 TRILL Probability Computation
  836
  837***********************/
  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)