1:- module(sphere,[
    2  prob_meta/2,
    3  prob/2,
    4  query/1,
    5  bdd_dot_file/3,
    6  bdd_dot_string/3,
    7  % get_bdd/4,
    8  set_sphere/2,setting_sphere/2,
    9  get_var_n/6,
   10  load/1,load_file/1,
   11  % op(600,fx,'?'),
   12  op(600,xfy,'::')
   13    ]).

sphere

This module performs reasoning over Probabilistic Hybrid Knowledge Bases. It reads probabilistic HKB and computes the probability of queries.

Reexports cplint_util and bddem

author
- Riccardo Zese, Fabrizio Riguzzi
copyright
- Riccardo Zese, Fabrizio Riguzzi */
license
- Artistic License 2.0 https://opensource.org/licenses/Artistic-2.0
   25:- reexport(library(cplint_util)).   26:- reexport(library(bddem)).   27
   28% :- prolog_debug(chk_secure).
   29
   30:-meta_predicate query(:).   31:-meta_predicate prob(:,-).   32:-meta_predicate prob_meta(:,-).   33:-meta_predicate bdd_dot_file(:,+,-).   34:-meta_predicate bdd_dot_string(:,-,-).   35:-meta_predicate get_p(:,+,-).   36:-meta_predicate get_node(:,+,-).   37:-meta_predicate set_sphere(:,+).   38:-meta_predicate setting_sphere(:,-).   39:-meta_predicate set_sw(:,+).   40
   41% :- dynamic utility/2.
   42
   43:-use_module(library(lists)).   44:-use_module(library(apply)).   45:-use_module(library(assoc)).   46
   47:- use_module('./utility/trillo.pl').   48
   49:- style_check(-discontiguous).   50
   51:- thread_local rule_n/1,goal_n/1,sphere_input_mod/1,local_sphere_setting/2,lp_axioms_for_oracle/2.   52
   53:- table oracle_call(_,_,_,_,lattice(orc/3)), oracle_call(_,_,_,_,_,lattice(orc/3)), sphere_not(_,_,_,_,_,lattice(orc/3)),sphere_neg_H(_,_,_,_,_,lattice(orc/3)),sphere_not_dl(_,_,_,_,lattice(orc/3)),sphere_not_lp(_,_,_,_,lattice(orc/3)).%, sphere_check_inconsistency/4.
   54
   55prolog:message(inconsistenthkb) -->
   56  [ 'Inconsistent HKB' ].
   57
   58
   59default_setting_sphere(epsilon_parsing, 1e-5).
   60/* on, off */
   61
   62%default_setting_sphere(bagof,false).
   63/* values: false, intermediate, all, extra */
   64
   65%default_setting_sphere(compiling,off).
   66
   67:-set_prolog_flag(unknown,warning).   68
   69default_setting_sphere(depth_bound,false).  %if true, it limits the derivation of the example to the value of 'depth'
   70default_setting_sphere(depth,5).
   71default_setting_sphere(single_var,false). %false:1 variable for every grounding of a rule; true: 1 variable for rule (even if a rule has more groundings),simpler.
   72
   73default_setting_sphere(check_incons,false). %false the check is not performed.
   74
   75default_setting_sphere(tabling,auto).
   76/* values:
   77  auto
   78  explicit
   79*/
 load(++File:atom) is det
Loads File.phkb if it exists, otherwise loads File.cpl if it exists. /
   86load(File):-
   87  must_be(atom,File),
   88  atomic_concat(File,'.phkb',FileLPAD),
   89  (exists_file(FileLPAD)->
   90    load_file(FileLPAD)
   91  ;
   92    atomic_concat(File,'.cpl',FileCPL),
   93    (exists_file(FileCPL)->
   94      load_file(FileCPL)
   95    )
   96  ).
 load_file(++FileWithExtension:atom) is det
Loads FileWithExtension. /
  106load_file(File):-
  107  must_be(atom,File),
  108  begin_lpad_pred,
  109  user:consult(File),
  110  end_lpad_pred.
 prob_meta(:Query:conjunction_of_literals, -Probability:float) is nondet
To be used in place of prob/2 for meta calls (doesn't abolish tables) /
  118prob_meta(M:Goal,P):-
  119  must_be(nonvar,Goal),
  120  must_be(var,P),
  121  term_variables(Goal,VG),
  122  get_next_goal_number(M,GN),
  123  atomic_concat('$goal',GN,NewGoal),
  124  Goal1=..[NewGoal|VG],
  125  list2and(GoalL,Goal),
  126  ( M:local_sphere_setting(depth_bound,true) *->
  127      ( process_body_db(GoalL,BDD,BDDAnd,DB,[],_Vars,BodyList2,Env,M),
  128        add_bdd_arg_db(Goal1,Env,BDDAnd,DB,M,Head1),
  129        dyn_goals(M,GoalL),
  130        BodyOracle = (sphere:oracle_call(Goal,M,Env,0,DB,BDDAnd))
  131      )
  132    ;
  133      ( process_body(GoalL,BDD,BDDAnd,[],_Vars,BodyList2,Env,M),
  134        add_bdd_arg(Goal1,Env,BDDAnd,M,Head1),
  135        dyn_goals(M,GoalL),
  136        BodyOracle = (sphere:oracle_call(Goal,M,Env,0,BDDAnd))
  137      )
  138  ),
  139  append([onec(Env,BDD)],BodyList2,BodyList3),
  140  list2and(BodyList3,Body2),
  141  M:(asserta((Head1 :- BodyOracle),RefOC)),
  142  M:(asserta((Head1 :- Body2),RefSC)),
  143  init(Env),
  144  check_inconsistency_activation(M),
  145  %build_and_expand(M),
  146  findall((Goal,P),get_p(M:Goal1,Env,P),L),
  147  end(Env),
  148  erase(RefOC),
  149  erase(RefSC),
  150  member((Goal,P),L).
 query_meta(:Query:atom) is nondet
To be used in place of query/1 for meta calls (doesn't abolish tables) /
  157query_meta(M:Goal):-
  158  must_be(nonvar,Goal),
  159  term_variables(Goal,VG),
  160  get_next_goal_number(M,GN),
  161  atomic_concat('$goal',GN,NewGoal),
  162  Goal1=..[NewGoal|VG],
  163  list2and(GoalL,Goal),
  164  ( M:local_sphere_setting(depth_bound,true) *->
  165      ( process_body_db(GoalL,BDD,BDDAnd,DB,[],_Vars,BodyList2,Env,M),
  166        add_bdd_arg_db(Goal1,Env,BDDAnd,DB,M,Head1),
  167        dyn_goals(M,GoalL),
  168        BodyOracle = (sphere:oracle_call(Goal,M,Env,0,DB,BDDAnd))
  169      )
  170    ;
  171      ( process_body(GoalL,BDD,BDDAnd,[],_Vars,BodyList2,Env,M),
  172        add_bdd_arg(Goal1,Env,BDDAnd,M,Head1),
  173        dyn_goals(M,GoalL),
  174        BodyOracle = (sphere:oracle_call(Goal,M,Env,0,BDDAnd))
  175      )
  176  ),
  177  append([onec(Env,BDD)],BodyList2,BodyList3),
  178  list2and(BodyList3,Body2),
  179  M:(asserta((Head1 :- BodyOracle),RefOC)),
  180  M:(asserta((Head1 :- Body2),RefSC)),
  181  init(Env),
  182  check_inconsistency_activation(M),
  183  %build_and_expand(M),
  184  get_query_truth(M:Goal1,Env),!,
  185  end(Env),
  186  erase(RefOC),
  187  erase(RefSC).
 bdd_dot_file(:Query:atom, +FileName:string, -LV:list) is det
The predicate builds the BDD for Query and writes its dot representation to file FileName and a list in LV with the association of variables to rules. LV is a list of list, each sublist has three elements: the multivalued variable number, the rule number and the grounding substitution. /
  200bdd_dot_file(M:Goal,File,LV):-
  201  must_be(nonvar,Goal),
  202  must_be(string,File),
  203  must_be(var,LV),
  204  abolish_all_tables,
  205  init(Env),
  206  get_node(M:Goal,Env,Out),
  207  Out=(_,BDD),!,
  208  findall([V,R,S],M:v(R,S,V),LV),
  209  create_dot(Env,BDD,File),
  210  end(Env).
 bdd_dot_string(:Query:atom, -DotString:string, -LV:list) is det
The predicate builds the BDD for Query and returns its dot representation in DotString and a list in LV with the association of variables to rules. LV is a list of list, each sublist has three elements: the multivalued variable number, the rule number and the grounding substitution. /
  221bdd_dot_string(M:Goal,DotString,LV):-
  222  must_be(nonvar,Goal),
  223  must_be(var,DotString),
  224  must_be(var,LV),
  225  DotString=dot(Dot),
  226  abolish_all_tables,
  227  init(Env),
  228  get_node(M:Goal,Env,Out),
  229  Out=(_,BDD),!,
  230  findall([V,R,S],M:v(R,S,V),LV),
  231  create_dot_string(Env,BDD,Dot),
  232  end(Env).
 prob(:Query:atom, -Probability:float) is nondet
The predicate computes the probability of Query If Query is not ground, it returns in backtracking all ground instantiations of Query together with their probabilities /
  245prob(M:Goal,P):-
  246  must_be(nonvar,Goal),
  247  abolish_all_tables,
  248  init_oracle(M),
  249  prob_meta(M:Goal,P).
  250
  251
  252query(M:Goal):-
  253  must_be(nonvar,Goal),
  254  abolish_all_tables,
  255  init_oracle(M),
  256  query_meta(M:Goal).
  257
  258get_p(M:Goal,Env,P):-
  259  get_node(M:Goal,Env,BDD),
  260  ret_probc(Env,BDD,P).
  261
  262get_query_truth(M:Goal,Env):-
  263    M:local_sphere_setting(depth_bound,true),!,
  264    M:local_sphere_setting(depth,DB),
  265    retractall(M:v(_,_,_)),
  266    retractall(M:av(_,_,_)),
  267    %retractall(M:dec(_,_,_)),
  268    add_bdd_arg_db(Goal,Env,BDD,DB,M,Goal1),%DB=depth bound
  269    (bagof(BDD,M:Goal1,L)*->
  270      or_listc(L,Env,B)
  271    ;
  272      zeroc(Env,B)
  273    ),
  274    \+ zeroc(Env,B).
  275  
  276get_query_truth(M:Goal,Env):- %with DB=false
  277  retractall(M:v(_,_,_)),
  278  retractall(M:av(_,_,_)),
  279  %retractall(M:dec(_,_,_)),
  280  add_bdd_arg(Goal,Env,BDD,M,Goal1),
  281  (bagof(BDD,M:Goal1,L)*->
  282    or_listc(L,Env,B)
  283  ;
  284    zeroc(Env,B)
  285    % format("-------------------------Failed goal: ~w ~n",[M:Goal])
  286  ),
  287  \+ zeroc(Env,B).
  288
  289get_node(M:Goal,Env,BDD):-
  290  M:local_sphere_setting(depth_bound,true),!,
  291  M:local_sphere_setting(depth,DB),
  292  retractall(M:v(_,_,_)),
  293  retractall(M:av(_,_,_)),
  294  %retractall(M:dec(_,_,_)),
  295  add_bdd_arg_db(Goal,Env,BDD,DB,M,Goal1),%DB=depth bound
  296  (bagof(BDD,M:Goal1,L)*->
  297    or_listc(L,Env,BDD)
  298  ;
  299    zeroc(Env,BDD)
  300  ).
  301
  302get_node(M:Goal,Env,BDD):- %with DB=false
  303  retractall(M:v(_,_,_)),
  304  retractall(M:av(_,_,_)),
  305  %retractall(M:dec(_,_,_)),
  306  add_bdd_arg(Goal,Env,BDD,M,Goal1),
  307  (bagof(BDD,M:Goal1,L)*->
  308    or_listc(L,Env,BDD)
  309  ;
  310    zeroc(Env,BDD)
  311    % format("-------------------------Failed goal: ~w ~n",[M:Goal])
  312  ).
  313
  314
  315
  316
  317
  318
  319
  320
  321get_next_goal_number(PName,R):-
  322  retract(PName:goal_n(R)),
  323  R1 is R+1,
  324  assert(PName:goal_n(R1)).
  325
  326
  327get_next_rule_number(PName,R):-
  328  retract(PName:rule_n(R)),
  329  R1 is R+1,
  330  assert(PName:rule_n(R1)).
  331
  332
  333assert_all([],_M,[]).
  334
  335assert_all([H|T],M,[HRef|TRef]):-
  336  assertz(M:H,HRef),
  337  assert_all(T,M,TRef).
  338
  339
  340retract_all([]):-!.
  341
  342retract_all([H|T]):-
  343  erase(H),
  344  retract_all(T).
 get_var_n(++M:atomic, ++Environment:int, ++Rule:int, ++Substitution:term, ++Probabilities:list, -Variable:int) is det
Returns the index Variable of the random variable associated to rule with index Rule, grounding substitution Substitution and head distribution Probabilities in environment Environment. /
  353get_var_n(M,Env,R,S,Probs0,V):-
  354  M:query_rule(R,_H,_B,_S),!,
  355  (ground(Probs0)->
  356    maplist(is,Probs,Probs0),
  357    (M:v(R,S,V)->
  358      true
  359    ;
  360      add_query_var(Env,Probs,R,V),
  361      assert(M:v(R,S,V))
  362    )
  363  ;
  364    throw(error('Non ground probabilities not instantiated by the body'))
  365  ).
  366
  367get_var_n(M,Env,R,S,Probs0,V):-
  368  (ground(Probs0)->
  369    maplist(is,Probs,Probs0),
  370    (M:v(R,S,V)->
  371      true
  372    ;
  373      % format("P: ~w ~w ~n",[Probs,R]),
  374      add_var(Env,Probs,R,V),
  375      assert(M:v(R,S,V))
  376    )
  377  ;
  378    throw(error('Non ground probabilities not instantiated by the body'))
  379  ).
  380
  381
  382add_bdd_arg(M:A,Env,BDD,M:A1):-
  383  A=..[P|Args],
  384  append(Args,[Env,BDD],Args1),
  385  A1=..[P|Args1].
  386
  387
  388add_bdd_arg_db(M:A,Env,BDD,DB,M:A1):-
  389  A=..[P|Args],
  390  append(Args,[Env,DB,BDD],Args1),
  391  A1=..[P|Args1].
  392
  393
  394add_bdd_arg(A,Env,BDD,_Module,A1):-
  395  A=..[P|Args],
  396  append(Args,[Env,BDD],Args1),
  397  A1=..[P|Args1].
  398
  399
  400add_bdd_arg_db(A,Env,BDD,DB,_Module,A1):-
  401  A=..[P|Args],
  402  append(Args,[Env,DB,BDD],Args1),
  403  A1=..[P|Args1].
  404
  405  
  406
  407dyn_goals(M,L):-
  408  M:lp_axioms_for_oracle(LPList0,_LBody0),
  409  sort(LPList0,LPList1),
  410  clean_lplist(LPList1,LPList),
  411  dyn_goals(M,L,LPList).
  412  %retractall(M:lp_axioms_for_oracle(_,_)).
  413
  414dyn_goals(_,[],_):-!.
  415
  416dyn_goals(M,[H|T],LPList):-
  417  functor(H,P,A),
  418  \+ member((P/A),LPList),!,
  419  (M:local_sphere_setting(depth_bound,true)->
  420    AD is A + 3
  421  ;
  422    AD is A + 2
  423  ),
  424  M:(dynamic P/AD),
  425  dyn_goals(M,T,LPList).
  426
  427dyn_goals(M,[_H|T],LPList):-
  428  dyn_goals(M,T,LPList).
  429
  430
  431generate_rules_fact([],_Env,_VC,_R,_Probs,_N,[],_Module,_Doubled).
  432
  433generate_rules_fact([Head:_P1,'':_P2],Env,VC,R,Probs,N,[Clause],Module,Doubled):-!,
  434  add_bdd_arg(Head,Env,BDD,Module,Head1),
  435  ( Doubled=true ->
  436      Clause=(Head1:-(get_var_n(Module,Env,R,VC,Probs,V),equalityc(Env,V,N,BDDAnd),sphere:sphere_neg_H(Module,_H1,Head,Env,BDDAnd,BDDN),andc(Env,BDDAnd,BDDN,BDD),sphere:sphere_check_inconsistency(Module,Head,Env,BDD)))
  437    ;
  438      Clause=(Head1:-(get_var_n(Module,Env,R,VC,Probs,V),equalityc(Env,V,N,BDD),sphere:sphere_check_inconsistency(Module,Head,Env,BDD)))
  439  ).
  440
  441generate_rules_fact([Head:_P|T],Env,VC,R,Probs,N,[Clause|Clauses],Module,Doubled):-
  442  add_bdd_arg(Head,Env,BDD,Module,Head1),
  443  ( Doubled=true ->
  444      Clause=(Head1:-(get_var_n(Module,Env,R,VC,Probs,V),equalityc(Env,V,N,BDDAnd),sphere:sphere_neg_H(Module,_H1,Head,Env,BDDAnd,BDDN),andc(Env,BDDAnd,BDDN,BDD),sphere:sphere_check_inconsistency(Module,Head,Env,BDD)))
  445    ;
  446      Clause=(Head1:-(get_var_n(Module,Env,R,VC,Probs,V),equalityc(Env,V,N,BDD),sphere:sphere_check_inconsistency(Module,Head,Env,BDD)))
  447  ),
  448  N1 is N+1,
  449  generate_rules_fact(T,Env,VC,R,Probs,N1,Clauses,Module,Doubled).
  450
  451
  452generate_rules_fact_db([],_Env,_VC,_R,_Probs,_N,[],_Module,_Doubled).
  453
  454generate_rules_fact_db([Head:_P1,'':_P2],Env,VC,R,Probs,N,[Clause],Module,Doubled):-
  455  add_bdd_arg_db(Head,Env,BDD,_DB,Module,Head1),
  456  ( Doubled=true ->
  457      Clause=(Head1:-(get_var_n(Module,Env,R,VC,Probs,V),equalityc(Env,V,N,BDDAnd),sphere:sphere_neg_H(Module,_H1,Head,Env,BDDAnd,BDDN),andc(Env,BDDAnd,BDDN,BDD),sphere:sphere_check_inconsistency(Module,Head,Env,BDD)))
  458    ;
  459      Clause=(Head1:-(get_var_n(Module,Env,R,VC,Probs,V),equalityc(Env,V,N,BDD),sphere:sphere_check_inconsistency(Module,Head,Env,BDD)))
  460  ).
  461
  462generate_rules_fact_db([Head:_P|T],Env,VC,R,Probs,N,[Clause|Clauses],Module,Doubled):-
  463  add_bdd_arg_db(Head,Env,BDD,_DB,Module,Head1),
  464  ( Doubled=true ->
  465      Clause=(Head1:-(get_var_n(Module,Env,R,VC,Probs,V),equalityc(Env,V,N,BDDAnd),sphere:sphere_neg_H(Module,_H1,Head,Env,BDDAnd,BDDN),andc(Env,BDDAnd,BDDN,BDD),sphere:sphere_check_inconsistency(Module,Head,Env,BDD)))
  466    ;
  467      Clause=(Head1:-(get_var_n(Module,Env,R,VC,Probs,V),equalityc(Env,V,N,BDD),sphere:sphere_check_inconsistency(Module,Head,Env,BDD)))
  468  ),
  469  N1 is N+1,
  470  generate_rules_fact_db(T,Env,VC,R,Probs,N1,Clauses,Module,Doubled).
  471
  472
  473generate_clause(Head,Env,Body,VC,R,Probs,BDDAnd,N,Clause,Module):-
  474  add_bdd_arg(Head,Env,BDD,Module,Head1),
  475  Clause=(Head1:-(Body,get_var_n(Module,Env,R,VC,Probs,V),equalityc(Env,V,N,B),andc(Env,BDDAnd,B,BDD))).
  476
  477
  478generate_clause_db(Head,Env,Body,VC,R,Probs,DB,BDDAnd,N,Clause,Module):-
  479  add_bdd_arg_db(Head,Env,BDD,DBH,Module,Head1),
  480  Clause=(Head1:-(DBH>=1,DB is DBH-1,Body,get_var_n(Module,Env,R,VC,Probs,V),equalityc(Env,V,N,B),andc(Env,BDDAnd,B,BDD))).
  481
  482
  483generate_rules([],_Env,_Body,_VC,_R,_Probs,_BDDAnd,_N,[],_Module).
  484
  485generate_rules([Head:_P1,'':_P2],Env,Body,VC,R,Probs,BDDAnd,N,[Clause],Module):-!,
  486  generate_clause(Head,Env,Body,VC,R,Probs,BDDAnd,N,Clause,Module).
  487
  488generate_rules([Head:_P|T],Env,Body,VC,R,Probs,BDDAnd,N,[Clause|Clauses],Module):-
  489  generate_clause(Head,Env,Body,VC,R,Probs,BDDAnd,N,Clause,Module),
  490  N1 is N+1,
  491  generate_rules(T,Env,Body,VC,R,Probs,BDDAnd,N1,Clauses,Module).
  492
  493
  494generate_rules_db([],_Env,_Body,_VC,_R,_Probs,_DB,_BDDAnd,_N,[],_Module):-!.
  495
  496generate_rules_db([Head:_P1,'':_P2],Env,Body,VC,R,Probs,DB,BDDAnd,N,[Clause],Module):-!,
  497  generate_clause_db(Head,Env,Body,VC,R,Probs,DB,BDDAnd,N,Clause,Module).
  498
  499generate_rules_db([Head:_P|T],Env,Body,VC,R,Probs,DB,BDDAnd,N,[Clause|Clauses],Module):-
  500  generate_clause_db(Head,Env,Body,VC,R,Probs,DB,BDDAnd,N,Clause,Module),!,%agg.cut
  501  N1 is N+1,
  502  generate_rules_db(T,Env,Body,VC,R,Probs,DB,BDDAnd,N1,Clauses,Module).
  503
  504
  505process_body([],BDD,BDD,Vars,Vars,[],_Env,_Module).
  506
  507process_body([\+ H|T],BDD,BDD1,Vars,Vars1,[\+ H|Rest],Env,Module):-
  508  builtin(H),!,
  509  process_body(T,BDD,BDD1,Vars,Vars1,Rest,Env,Module).
  510
  511process_body([\+ db(H)|T],BDD,BDD1,Vars,Vars1,[\+ H|Rest],Env,Module):-
  512  !,
  513  process_body(T,BDD,BDD1,Vars,Vars1,Rest,Env,Module).
  514
  515process_body([\+ H|T],BDD,BDD1,Vars,[BDDH,BDDN,BDD2|Vars1],
  516[(sphere:sphere_not(Module,H1,Pred,Doubled,Env,BDDH,BDDN)), %H1,(sphere:sphere_not(Module,H1,Pred,Doubled,Env,BDDH,BDDN)),
  517  andc(Env,BDD,BDDN,BDD2)|Rest],Env,Module):-!,
  518  add_bdd_arg(H,Env,BDDH,Module,H1),
  519  assert_body_pred(Module,H),
  520  ( name_value(H,Pred)-> Doubled=true ; (Pred=H,Doubled=false) ),
  521  process_body(T,BDD2,BDD1,Vars,Vars1,Rest,Env,Module).
  522
  523process_body([H|T],BDD,BDD1,Vars,Vars1,[H1|Rest],Env,Module):-
  524  transform(H,H1),!,
  525  process_body(T,BDD,BDD1,Vars,Vars1,Rest,Env,Module).
  526
  527process_body([H|T],BDD,BDD1,Vars,Vars1,[H|Rest],Env,Module):-
  528  builtin(H),!,
  529  process_body(T,BDD,BDD1,Vars,Vars1,Rest,Env,Module).
  530
  531process_body([db(H)|T],BDD,BDD1,Vars,Vars1,[H|Rest],Env,Module):-
  532  !,
  533  process_body(T,BDD,BDD1,Vars,Vars1,Rest,Env,Module).
  534
  535process_body([H|T],BDD,BDD1,Vars,[BDDH,BDD2|Vars1],
  536[H1,andc(Env,BDD,BDDH,BDD2)|Rest],Env,Module):-
  537  add_bdd_arg(H,Env,BDDH,Module,H1),
  538  assert_body_pred(Module,H),
  539  process_body(T,BDD2,BDD1,Vars,Vars1,Rest,Env,Module).
  540
  541process_body_db([],BDD,BDD,_DB,Vars,Vars,[],_Env,_Module):-!.
  542
  543process_body_db([\+ H|T],BDD,BDD1,DB,Vars,Vars1,[\+ H|Rest],Env,Module):-
  544  builtin(H),!,
  545  process_body_db(T,BDD,BDD1,DB,Vars,Vars1,Rest,Env,Module).
  546
  547process_body_db([\+ db(H)|T],BDD,BDD1,DB,Vars,Vars1,[\+ H|Rest],Env,Module):-
  548  !,
  549  process_body_db(T,BDD,BDD1,DB,Vars,Vars1,Rest,Env,Module).
  550
  551process_body_db([\+ H|T],BDD,BDD1,DB,Vars,[BDDH,BDDN,BDD2|Vars1],
  552[(sphere:sphere_not(Module,H1,Pred,Doubled,Env,BDDH,BDDN)), %H1,(sphere:sphere_not(Module,H1,Pred,Doubled,Env,BDDH,BDDN)),
  553  andc(Env,BDD,BDDN,BDD2)|Rest],Env,Module):-!,
  554  add_bdd_arg_db(H,Env,BDDH,DB,Module,H1),
  555  assert_body_pred(Module,H),
  556  ( name_value(H,Pred)-> Doubled=true ; (Pred=H,Doubled=false) ),
  557  process_body_db(T,BDD2,BDD1,DB,Vars,Vars1,Rest,Env,Module).
  558
  559process_body_db([H|T],BDD,BDD1,DB,Vars,Vars1,[H1|Rest],Env,Module):-
  560  transform(H,H1),!,
  561  process_body_db(T,BDD,BDD1,DB,Vars,Vars1,Rest,Env,Module).
  562
  563process_body_db([H|T],BDD,BDD1,DB,Vars,Vars1,[H|Rest],Env,Module):-
  564  builtin(H),!,
  565  process_body_db(T,BDD,BDD1,DB,Vars,Vars1,Rest,Env,Module).
  566
  567process_body_db([db(H)|T],BDD,BDD1,DB,Vars,Vars1,[H|Rest],Env,Module):-
  568  !,
  569  process_body_db(T,BDD,BDD1,DB,Vars,Vars1,Rest,Env,Module).
  570
  571process_body_db([H|T],BDD,BDD1,DB,Vars,[BDDH,BDD2|Vars1],
  572[H1,andc(Env,BDD,BDDH,BDD2)|Rest],Env,Module):-!, %agg. cut
  573  add_bdd_arg_db(H,Env,BDDH,DB,Module,H1),
  574  assert_body_pred(Module,H),
  575  process_body_db(T,BDD2,BDD1,DB,Vars,Vars1,Rest,Env,Module).
  576
  577
  578process_head(HeadList, GroundHeadList1) :-
  579  ground_prob(HeadList), !,
  580  process_head_ground(HeadList, 0.0, GroundHeadList),
  581  ( GroundHeadList = [V:P] -> 
  582      P1 is 1.0 - P, 
  583      GroundHeadList1 = [V:P,'':P1] ; 
  584      GroundHeadList1 = GroundHeadList
  585  ).
  586
  587process_head(HeadList0, HeadList):-
  588  get_probs(HeadList0,PL),
  589  foldl(minus,PL,1.0,PNull),
  590  append(HeadList0,['':PNull],HeadList).
  591
  592minus(A,B,B-A).
  593
  594prob_ann(_:P0,P):-!, to_float(P0,P).
  595prob_ann(P0::_,P):- to_float(P0, P).
  596
  597to_float(P0, P) :-
  598  ground(P0), !,
  599  P is float(P0).
  600to_float(P, P).
  601
  602gen_head(H,P,VH,V,V1,H1:P):-copy_term((H,VH,V),(H1,VH,V1)).
  603gen_head_disc(H,VH,V,V1:P,H1:P1):-copy_term((H,VH,V),(H1,VH,V1)),P1 is float(P).
  604
  605assert_head_pred(M,H):-
  606  (sphere_input_mod(M) ->
  607   (functor(H,Pred0,Arity),
  608    ((Arity==1;Arity==2) ->
  609      ( H=..[Pred0|Args],
  610        ( name_value(Pred0,Pred)-> true ; Pred=Pred0 ),
  611        M:lp_axioms_for_oracle(LT,LB),
  612        retractall(M:lp_axioms_for_oracle(_,_)),
  613        (dif(Args,[]) -> ADD=[Pred/Arity-Args] ; ADD=[Pred/Arity]),
  614        append(LT,ADD,L),
  615        M:assert(lp_axioms_for_oracle(L,LB))
  616      )
  617     ;
  618      true
  619    )
  620   )
  621   ;
  622    true
  623  ).
  624
  625assert_body_pred(M,B):-
  626  (sphere_input_mod(M) ->
  627   (functor(B,Pred0,Arity),
  628    ((Arity==1;Arity==2) ->
  629      ( ( name_value(Pred0,Pred)-> true ; Pred=Pred0 ),
  630        M:lp_axioms_for_oracle(LT,LB),
  631        retractall(M:lp_axioms_for_oracle(_,_)),
  632        M:assert(lp_axioms_for_oracle(LT,[Pred/Arity|LB]))
  633      )
  634     ;
  635      true
  636    )
  637   )
  638   ;
  639    true
  640  ).
  641
  642/* process_head_ground([Head:ProbHead], Prob, [Head:ProbHead|Null])
  643 * ----------------------------------------------------------------
  644 */
  645process_head_ground([H], Prob, [Head:ProbHead1|Null]) :-
  646  (H=Head:ProbHead;H=ProbHead::Head),!,
  647  ProbHead1 is float(ProbHead),
  648  ProbLast is 1.0 - Prob - ProbHead1,
  649  prolog_load_context(module, M),sphere_input_mod(M),
  650  M:local_sphere_setting(epsilon_parsing, Eps),
  651  EpsNeg is - Eps,
  652  ProbLast > EpsNeg,
  653  (ProbLast > Eps ->
  654    Null = ['':ProbLast]
  655  ;
  656    Null = []
  657  ),
  658  assert_head_pred(M,Head).
  659
  660process_head_ground([H|Tail], Prob, [Head:ProbHead1|Next]) :-
  661  (H=Head:ProbHead;H=ProbHead::Head),
  662  ProbHead1 is float(ProbHead),
  663  ProbNext is Prob + ProbHead1,
  664  prolog_load_context(module, M),sphere_input_mod(M),
  665  assert_head_pred(M,Head),
  666  process_head_ground(Tail, ProbNext, Next).
  667
  668
  669ground_prob([]).
  670
  671ground_prob([_Head:ProbHead|Tail]) :-!,
  672  ground(ProbHead), % Succeeds if there are no free variables in the term ProbHead.
  673  ground_prob(Tail).
  674
  675ground_prob([ProbHead::_Head|Tail]) :-
  676  ground(ProbHead), % Succeeds if there are no free variables in the term ProbHead.
  677  ground_prob(Tail).
  678
  679
  680get_probs(Head, PL):-
  681  maplist(prob_ann,Head,PL).
  682
  683/*get_probs([], []).
  684
  685get_probs([_H:P|T], [P1|T1]) :-
  686  P1 is P,
  687  get_probs(T, T1).
  688*/
  689
  690is_lp_assertion(lpClassAssertion(_,_)).
  691is_lp_assertion(lpPropertyAssertion(_,_,_)).
  692
  693
  694lp_assertion_to_atom(lpClassAssertion(Class,Individual),Atom):-
  695                Atom=..[Class,Individual].
  696lp_assertion_to_atom(lpPropertyAssertion(Role,Individual1, Individual2),Atom):-
  697                Atom=..[Role,Individual1,Individual2].
  698
  699lp_assertion_to_doubledatom(lpClassAssertion(Class,Individual),Atom):-
  700				atomic_concat(Class,'spheredoubled',ClassD),
  701                Atom=..[ClassD,Individual].
  702lp_assertion_to_doubledatom(lpPropertyAssertion(Role,Individual1, Individual2),Atom):-
  703                atomic_concat(Role,'spheredoubled',RoleD),
  704                Atom=..[RoleD,Individual1,Individual2].
  705
  706
  707get_bdd(_M,Env,[],BDDX):- !,
  708  onec(Env,BDDX).
  709
  710get_bdd(M,Env,[HA|T],BDDAnd):-
  711  get_prob_ax_mt(M,HA,AxN,H,Sub,Probs),!,
  712  get_var_n(M,Env,AxN,Sub,Probs,VH), 
  713  equalityc(Env,VH,H,BDDH),
  714  get_bdd(M,Env,T,BDDT),
  715  andc(Env,BDDH,BDDT,BDDAnd).
  716
  717get_bdd(M,Env,[_H|T],BDDAnd):- !,
  718  onec(Env,BDDH),
  719  get_bdd(M,Env,T,BDDT),
  720  andc(Env,BDDH,BDDT,BDDAnd).
  721
  722get_prob_ax_mt(M,Ax,N,0,[],[Prob,ProbN]):-
  723  Ax \= (_,_,_),
  724  compute_prob_ax(M,Ax,Prob),
  725  ProbN is 1-Prob,
  726  (M:na(Ax,N)-> 
  727    true
  728   ;
  729    (get_next_rule_number(M,N),
  730    assert(M:na(Ax,N)))
  731  ).
  732
  733compute_prob_ax(M,Ax,Prob):-
  734  findall(ProbA,(trillo:disponte_iri(DisponteIri),M:annotationAssertion(DisponteIri,Ax,literal(ProbAT)),atom_number(ProbAT,ProbA)),Probs),
  735  compute_prob_ax1(Probs,Prob).
  736
  737
  738compute_prob_ax1([Prob],Prob):-!.
  739
  740compute_prob_ax1([Prob1,Prob2],Prob):-!,
  741  Prob is Prob1+Prob2-(Prob1*Prob2).
  742
  743compute_prob_ax1([Prob1 | T],Prob):-
  744  compute_prob_ax1(T,Prob0),
  745  Prob is Prob1 + Prob0 - (Prob1*Prob0).
  746
  747
  748sphere_not(Module,H1,_H,_Doubled,Env,BDDH,BDDN):-
  749  sphere_not_lp(Module,H1,Env,BDDH,BDDN).
  750
  751sphere_not(Module,_H1,H,Doubled,Env,_BDDH,BDDN):-
  752  sphere_not_dl(Module,H,Doubled,Env,BDDN).
  753
  754sphere_check_inconsistency(Module,H,Env,BDDIn):-  % TODO: check whether H is a Dl-atom
  755  Module:local_sphere_setting(check_incons,true),
  756  %sphere_not_dl(Module,H,0,Env,BDDH),
  757  H=..[Class,Individual],
  758  instanceOf_meta(complementOf(Class),Individual,Explanation0,Module,Env,BDDT),!,
  759  include(is_lp_assertion,Explanation0,LPAssertions),
  760  maplist(lp_assertion_to_atom,LPAssertions,Atoms),
  761  solve_all(Module,Atoms,Env,BDDA),
  762  andc(Env,BDDT,BDDA,BDDH),
  763  andc_inc(Env,BDDIn,BDDH,Zero),
  764  ( zeroc(Env,Zero) -> true ; warn_about_inconsistency(Module)).
  765
  766sphere_check_inconsistency(_Module,_H,_Env,_BDDIn) :- !.
  767
  768check_inconsistency_activation(M):-
  769  M:inconsistency_warning, !,
  770  retractall(M:inconsistency_warning),
  771  set_sphere(M:check_incons,true).
  772
  773check_inconsistency_activation(_M).
  774
  775warn_about_inconsistency(M) :-
  776  ( M:inconsistency_warning ->
  777      true
  778    ;
  779      ( print_message(warning,inconsistenthkb),
  780        assert(M:inconsistency_warning),
  781        set_sphere(M:check_incons,false)
  782      )
  783  ).
  784
  785sphere_neg_H(Module,_H1,H,Env,_BDDIn,BDDN):-  % TODO: check whether H is a Dl-atom
  786  sphere_not_dl(Module,H,0,Env,BDDH),
  787  bdd_notc(Env,BDDH,BDDN).
  788
  789
  790sphere_not_lp(Module,H1,Env,BDDH,BDDN):-
  791  call(Module:H1),
  792  bdd_notc(Env,BDDH,BDDN).
  793
  794
  795
  796sphere_not_dl(M,H,Doubled,Env,BDDN):-
  797  H=..[Class,Individual],
  798  instanceOf_meta(complementOf(Class),Individual,Explanation0,M,Env,BDDT),
  799  include(is_lp_assertion,Explanation0,LPAssertions),
  800  (Doubled=0 -> 
  801     maplist(lp_assertion_to_atom,LPAssertions,Atoms)
  802    ;
  803     maplist(lp_assertion_to_doubledatom,LPAssertions,Atoms)
  804  ),
  805  solve_all(M,Atoms,Env,BDDA),
  806  andc(Env,BDDT,BDDA,BDDN).
  807
  808sphere_not_dl(_M,H,_Doubled,Env,BDDN):-
  809  H=..[_|Args],
  810  maplist(nonvar,Args),
  811  zeroc(Env,BDDN).
  812
  813oracle_call(Head,M,Env,Doubled,BDD):-
  814  Head=..[Class,Individual],
  815  instanceOf_meta(Class,Individual,Explanation0,M,Env,BDDT),
  816  include(is_lp_assertion,Explanation0,LPAssertions),
  817  (Doubled=0 -> 
  818     maplist(lp_assertion_to_atom,LPAssertions,Atoms)
  819    ;
  820     maplist(lp_assertion_to_doubledatom,LPAssertions,Atoms)
  821  ),
  822  solve_all(M,Atoms,Env,BDDA),
  823  andc(Env,BDDT,BDDA,BDD).
  824
  825/*
  826oracle_call(Head,M,Env,BDD):-
  827  Head=..[Class,Individual],
  828  instanceOf_meta(complementOf(Class),Individual,Explanation0),
  829  get_bdd(Env,Explanation0,BDDT),
  830  include(is_lp_assertion,Explanation0,LPAssertions),
  831  maplist(lp_assertion_to_atom,LPAssertions,Atoms),
  832  solve_all(Atoms,Env,BDDA),
  833  andc(Env,BDDT,BDDA,BDD0),
  834  bdd_notc(Env,BDD0,BDD).
  835*/
  836
  837oracle_call(Head,M,Env,Doubled,BDD):-
  838  Head=..[Role,Individual1,Individual2],
  839  property_value_meta(Role,Individual1,Individual2,Explanation0,M,Env,BDDT),
  840  include(is_lp_assertion,Explanation0,LPAssertions),
  841  (Doubled=0 -> 
  842     maplist(lp_assertion_to_atom,LPAssertions,Atoms)
  843    ;
  844     maplist(lp_assertion_to_doubledatom,LPAssertions,Atoms)
  845  ),
  846   solve_all(M,Atoms,Env,BDDA),
  847  andc(Env,BDDT,BDDA,BDD).
  848
  849/*
  850oracle_call(Head,_M,Env,_Doubled,BDD):-
  851  Head=..[_|Args],
  852  maplist(nonvar,Args),
  853  zeroc(Env,BDD).
  854*/
  855
  856oracle_call(Head,M,Env,Doubled,DB,BDD):-
  857  Head=..[Class,Individual],
  858  instanceOf_meta(Class,Individual,Explanation0,M,Env,BDDT),
  859  include(is_lp_assertion,Explanation0,LPAssertions),
  860  (Doubled=0 -> 
  861     maplist(lp_assertion_to_atom,LPAssertions,Atoms)
  862    ;
  863     maplist(lp_assertion_to_doubledatom,LPAssertions,Atoms)
  864  ),
  865  solve_all(M,Atoms,Env,DB,BDDA),
  866  andc(Env,BDDT,BDDA,BDD).
  867
  868/*
  869oracle_call(Head,M,Env,BDD):-
  870  Head=..[Class,Individual],
  871  instanceOf_meta(complementOf(Class),Individual,Explanation0),
  872  get_bdd(Env,Explanation0,BDDT),
  873  include(is_lp_assertion,Explanation0,LPAssertions),
  874  maplist(lp_assertion_to_atom,LPAssertions,Atoms),
  875  solve_all(Atoms,Env,BDDA),
  876  andc(Env,BDDT,BDDA,BDD0),
  877  bdd_notc(Env,BDD0,BDD).
  878*/
  879
  880oracle_call(Head,M,Env,Doubled,DB,BDD):-
  881  Head=..[Role,Individual1,Individual2],
  882  property_value_meta(Role,Individual1,Individual2,Explanation0,M,Env,BDDT),
  883  include(is_lp_assertion,Explanation0,LPAssertions),
  884  (Doubled=0 -> 
  885     maplist(lp_assertion_to_atom,LPAssertions,Atoms)
  886    ;
  887     maplist(lp_assertion_to_doubledatom,LPAssertions,Atoms)
  888  ),
  889  solve_all(M,Atoms,Env,DB,BDDA),
  890  andc(Env,BDDT,BDDA,BDD).
  891  
  892oracle_call(Head,_M,Env,_Doubled,_DB,BDD):-
  893  Head=..[_|Args],
  894  maplist(nonvar,Args),
  895  zeroc(Env,BDD).
  896
  897solve_all(_M,[],Env,BDDOne):- !,
  898  onec(Env,BDDOne).
  899
  900solve_all(M,[H|T],Env,BDD):-
  901  call(M:H,Env,BDDH),
  902  solve_all(M,T,Env,BDDT),
  903  andc(Env,BDDT,BDDH,BDD).
  904
  905solve_all(_M,[],Env,_DBH,BDDOne):- !,
  906  onec(Env,BDDOne).
  907
  908solve_all(M,[H|T],Env,DBH,BDD):-
  909  call(M:H,Env,DBH,BDDH),
  910  solve_all(M,T,Env,DBH,BDDT),
  911  andc(Env,BDDT,BDDH,BDD).
 set_sphere(:Parameter:atom, +Value:term) is det
The predicate sets the value of a parameter For a list of parameters see https://friguzzi.github.io/cplint/

/

  922set_sphere(M:Parameter,Value):-
  923  must_be(atom,Parameter),
  924  must_be(nonvar,Value),
  925  retract(M:local_sphere_setting(Parameter,_)),
  926  assert(M:local_sphere_setting(Parameter,Value)).
 setting_sphere(:Parameter:atom, ?Value:term) is det
The predicate returns the value of a parameter For a list of parameters see https://friguzzi.github.io/cplint/ /
  935setting_sphere(M:P,V):-
  936  must_be(atom,P),
  937  M:local_sphere_setting(P,V).
  938
  939/*
  940delete_equal([],_,[]).
  941
  942delete_equal([H|T],E,T):-
  943  H == E,!.
  944
  945delete_equal([H|T],E,[H|T1]):-
  946  delete_equal(T,E,T1).
  947*/
  948
  949set_sw(M:A,B):-
  950  get_next_rule_number(M,R),
  951  assert(M:sw(R,A,B)).
  952
  953/*
  954act(M,A/B):-
  955  (M:local_sphere_setting(depth_bound,true)->
  956    B1 is B + 3
  957  ;
  958    B1 is B + 2
  959  ),
  960  M:(dynamic A/B1).
  961*/
  962
  963tab(M,A/B,P):-
  964  length(Args0,B),
  965  (M:local_sphere_setting(depth_bound,true)->
  966    ExtraArgs=[_,_,lattice(orc/3)]
  967  ;
  968    ExtraArgs=[_,lattice(orc/3)]
  969  ),
  970  append(Args0,ExtraArgs,Args),
  971  P=..[A|Args],
  972  PT=..[A|Args0],
  973  assert(M:tabled(PT)).
  974
  975zero_clause(M,A/B,(H:-maplist(nonvar,Args0),zeroc(Env,BDD))):-
  976  length(Args0,B),
  977  (M:local_sphere_setting(depth_bound,true)->
  978    ExtraArgs=[Env,_,BDD]
  979  ;
  980    ExtraArgs=[Env,BDD]
  981  ),
  982  append(Args0,ExtraArgs,Args),
  983  H=..[A|Args].
  984
  985assert_lp_axioms(M,L):-
  986  assert_lp_axioms(M,L,I),
  987  (dif(I,[]) -> (sort(I,Inds),trillo_utility_translation:create_and_assert_axioms(M,lpIndividuals(Inds)));
  988    true).
  989
  990assert_lp_axioms(_,[],[]).
  991
  992assert_lp_axioms(M,[P/1|T],I):- !,
  993  trillo_utility_translation:create_and_assert_axioms(M,lpClassAssertion(P)),
  994  assert_lp_axioms(M,T,I).
  995
  996assert_lp_axioms(M,[P/2|T],I):- !,
  997  trillo_utility_translation:create_and_assert_axioms(M,lpPropertyAssertion,[P]),
  998  assert_lp_axioms(M,T,I).
  999
 1000assert_lp_axioms(M,[P/1-[A]|T],I):-!, 
 1001  extract_ground([A],L1),
 1002  trillo_utility_translation:create_and_assert_axioms(M,lpClassAssertion(P)),
 1003  assert_lp_axioms(M,T,I0),
 1004  append(L1,I0,I).
 1005
 1006assert_lp_axioms(M,[P/2-L|T],I):- !,
 1007  extract_ground(L,L1),
 1008  trillo_utility_translation:create_and_assert_axioms(M,lpPropertyAssertion(P)),
 1009  assert_lp_axioms(M,T,I0),
 1010  append(L1,I0,I).
 1011
 1012assert_lp_axioms(M,[_P/_A-L|T],I):-
 1013  extract_ground(L,L1),
 1014  assert_lp_axioms(M,T,I0),
 1015  append(L1,I0,I).
 1016
 1017extract_ground([],[]).
 1018extract_ground([H|T],[H|T1]):-
 1019  ground(H),!,
 1020  extract_ground(T,T1).
 1021extract_ground([_H|T],T1):-
 1022  extract_ground(T,T1).
 1023
 1024
 1025clean_lplist([],[]).
 1026
 1027clean_lplist([P/A|T0],[P/A|T]):-
 1028  clean_lplist(T0,T).
 1029
 1030clean_lplist([P/A-_|T0],[P/A|T]):-
 1031  clean_lplist(T0,T).
 1032
 1033create_ocrules_db([],[],_).
 1034
 1035create_ocrules_db([P/A|T0],[(H:-(DBH>=1,DB is DBH-1,sphere:oracle_call(OCQ,M,Env,0,DB,BDD))),(HD:-(DBH>=1,DB is DBH-1,sphere:oracle_call(OCQ,M,Env,1,DB,BDD)))|T],M):-
 1036  length(Args,A),
 1037  atomic_concat(P,'spheredoubled',PD),
 1038  append([P|Args],[Env,DBH,BDD],H0),
 1039  append([PD|Args],[Env,DBH,BDD],H0D),
 1040  H=..H0,
 1041  HD=..H0D,
 1042  OCQ=..[P|Args],
 1043  create_ocrules_db(T0,T,M).
 1044
 1045create_ocrules([],[],_).
 1046
 1047create_ocrules([P/A|T0],[(H:-(sphere:oracle_call(OCQ,M,Env,0,BDD))),(HD:-(sphere:oracle_call(OCQ,M,Env,1,BDD)))|T],M):-
 1048  length(Args,A),
 1049  atomic_concat(P,'spheredoubled',PD),
 1050  append([P|Args],[Env,BDD],H0),
 1051  append([PD|Args],[Env,BDD],H0D),
 1052  H=..H0,
 1053  HD=..H0D,
 1054  OCQ=..[P|Args],
 1055  create_ocrules(T0,T,M).
 1056
 1057create_oracle_calls(M,LPList,LBody,OCRules):-
 1058  M:local_sphere_setting(depth_bound,true),!,
 1059  clean_lplist(LPList,LPListCleaned),
 1060  append(LPListCleaned,LBody,OCList0),
 1061  sort(OCList0,OCList),
 1062  create_ocrules_db(OCList,OCRules,M).
 1063
 1064create_oracle_calls(M,LPList,LBody,OCRules):-
 1065  clean_lplist(LPList,LPListCleaned),
 1066  append(LPListCleaned,LBody,OCList0),
 1067  sort(OCList0,OCList),
 1068  create_ocrules(OCList,OCRules,M).
 1069
 1070to_table(M,Heads,[],Heads):-
 1071  M:local_sphere_setting(tabling,explicit),!.
 1072
 1073to_table(M,Heads,ProcTabDir,Heads1):-
 1074  maplist(tab_dir(M),Heads,TabDirList,Heads1L),
 1075  append(TabDirList,TabDir),
 1076  maplist(system:term_expansion,TabDir,ProcTabDirL),
 1077  append(ProcTabDirL,ProcTabDir),
 1078  append(Heads1L,Heads1).
 1079
 1080tab_dir(_M,'':_,[],[]):-!.
 1081
 1082tab_dir(M,H:P,[],[H:P]):-
 1083  M:tabled(H),!.
 1084
 1085tab_dir(M,Head,[(:- table HT)],[H1:P]):-
 1086  (Head=H:P;Head=P::H),!,
 1087  functor(H,F,A0),
 1088  functor(PT,F,A0),
 1089  PT=..[F|Args0],
 1090  (M:local_sphere_setting(depth_bound,true)->
 1091    ExtraArgs=[_,_,lattice(orc/3)]
 1092  ;
 1093    ExtraArgs=[_,lattice(orc/3)]
 1094  ),
 1095  append(Args0,ExtraArgs,Args),
 1096  HT=..[F|Args],
 1097  H=..[_|ArgsH],
 1098  H1=..[F|ArgsH],
 1099  assert(M:tabled(PT)),
 1100  zero_clause(M,F/A0,LZ),
 1101  assert(M:zero_clauses(LZ)).
 1102
 1103
 1104% ================================================================================
 1105
 1106double_head([],[]).
 1107
 1108double_head([H:P|T],[HD:P|TD]):-!,
 1109  H=..[HP|Args],
 1110  atomic_concat(HP,'spheredoubled',HPD),
 1111  HD=..[HPD|Args],
 1112  double_head(T,TD).
 1113
 1114double_head([H|T],[HD|TD]):-
 1115  H\=(_:_),H\=(_::_),
 1116  H=..[HP|Args],
 1117  atomic_concat(HP,'spheredoubled',HPD),
 1118  HD=..[HPD|Args],
 1119  double_head(T,TD).
 1120
 1121double_body([],[],[]).
 1122
 1123double_body([\+H|T],[\+HD|TD1],[\+H|TD2]):-!,
 1124  H=..[HP|Args],
 1125  atomic_concat(HP,'spheredoubled',HPD),
 1126  HD=..[HPD|Args],
 1127  double_body(T,TD1,TD2).
 1128
 1129double_body([H|T],[H|TD1],[HD|TD2]):-
 1130  H=..[HP|Args],
 1131  atomic_concat(HP,'spheredoubled',HPD),
 1132  HD=..[HPD|Args],
 1133  double_body(T,TD1,TD2).
 1134
 1135
 1136create_doubled_rules_1_db(HeadList,BodyD1,R,Probs,DB,M,[rule_by_num(R,HeadList,BodyD1,VC1)|Clauses]):-
 1137  process_body_db(BodyD1,BDD,BDDAnd,DB,[],_Vars,BodyList1,Env,M),%aggiunge bdd pred
 1138  append([onec(Env,BDD)],BodyList1,BodyList2),
 1139  list2and(BodyList2,Body1),
 1140  append(HeadList,BodyD1,List),
 1141  term_variables(List,VC), % extracts variables from head and body
 1142  (M:local_sphere_setting(single_var,true)->
 1143    VC1 = []
 1144  ;
 1145    VC1 = VC
 1146  ),
 1147  to_table(M,HeadList,TabDir,HeadList1), % adds table
 1148  ( M:local_sphere_setting(check_incons,true) -> 
 1149      generate_rules_d_1_db(HeadList1,HeadList,Env,Body1,VC1,R,Probs,DB,BDDAnd,0,Clauses0,M) %genera regoles
 1150    ;
 1151      generate_rules_db(HeadList1,Env,Body1,VC1,R,Probs,DB,BDDAnd,0,Clauses0,M) %genera regoles
 1152  ),
 1153  append(TabDir,Clauses0,Clauses).
 1154
 1155create_doubled_rules_1(HeadList,BodyD1,R,Probs,M,[rule_by_num(R,HeadList,BodyD1,VC1)|Clauses]):-
 1156  process_body(BodyD1,BDD,BDDAnd,[],_Vars,BodyList1,Env,M),%aggiunge bdd pred
 1157  append([onec(Env,BDD)],BodyList1,BodyList2),
 1158  list2and(BodyList2,Body1),
 1159  append(HeadList,BodyD1,List),
 1160  term_variables(List,VC), % extracts variables from head and body
 1161  (M:local_sphere_setting(single_var,true)->
 1162    VC1 = []
 1163  ;
 1164    VC1 = VC
 1165  ),
 1166  to_table(M,HeadList,TabDir,HeadList1), % adds table
 1167  ( M:local_sphere_setting(check_incons,true) -> 
 1168      generate_rules_d_1(HeadList1,HeadList,Env,Body1,VC1,R,Probs,BDDAnd,0,Clauses0,M) % generates rules
 1169    ;
 1170      generate_rules(HeadList1,Env,Body1,VC1,R,Probs,BDDAnd,0,Clauses0,M) % generates rules
 1171  ),
 1172  append(TabDir,Clauses0,Clauses).
 1173
 1174create_doubled_rules_2_db(HeadList,BodyD1,R,Probs,DB,M,[rule_by_num(R,HeadList,BodyD1,VC1)|Clauses]):-
 1175  process_body_db(BodyD1,BDD,BDDAnd,DB,[],_Vars,BodyList1,Env,M),% adds bdd pred
 1176  append([onec(Env,BDD)],BodyList1,BodyList2),
 1177  list2and(BodyList2,Body1),
 1178  append(HeadList,BodyD1,List),
 1179  term_variables(List,VC), % extracts variables from head and body
 1180  (M:local_sphere_setting(single_var,true)->
 1181    VC1 = []
 1182  ;
 1183    VC1 = VC
 1184  ),
 1185  to_table(M,HeadList,TabDir,HeadList1), % adds table
 1186  generate_rules_d_2_db(HeadList1,Env,Body1,VC1,R,Probs,DB,BDDAnd,0,Clauses0,M), % generates rules
 1187  append(TabDir,Clauses0,Clauses).
 1188
 1189create_doubled_rules_2(HeadList,BodyD1,R,Probs,M,[rule_by_num(R,HeadList,BodyD1,VC1)|Clauses]):-
 1190  process_body(BodyD1,BDD,BDDAnd,[],_Vars,BodyList1,Env,M),%aggiunge bdd pred
 1191  append([onec(Env,BDD)],BodyList1,BodyList2),
 1192  list2and(BodyList2,Body1),
 1193  append(HeadList,BodyD1,List),
 1194  term_variables(List,VC), % extracts variables from head and body
 1195  (M:local_sphere_setting(single_var,true)->
 1196    VC1 = []
 1197  ;
 1198    VC1 = VC
 1199  ),
 1200  to_table(M,HeadList,TabDir,HeadList1), % adds table
 1201  generate_rules_d_2(HeadList1,Env,Body1,VC1,R,Probs,BDDAnd,0,Clauses0,M), % generates rules
 1202  append(TabDir,Clauses0,Clauses).
 1203
 1204generate_rules_d_1_db([],_,_Env,_Body,_VC,_R,_Probs,_DB,_BDDAnd,_N,[],_Module).
 1205
 1206generate_rules_d_1_db([Head:_P1,'':_P2],[HeadNT:_P1NT,'':_P2NT],Env,Body,VC,R,Probs,DB,BDDAnd,N,[Clause],Module):-!,
 1207  list2and(BodyList,Body),
 1208  append(BodyList,[sphere:sphere_check_inconsistency(Module,HeadNT,Env,BDDAnd)],BodyListD),
 1209  list2and(BodyListD,BodyD),
 1210  generate_clause_db(Head,Env,BodyD,VC,R,Probs,DB,BDDAnd,N,Clause,Module).
 1211
 1212generate_rules_d_1_db([Head:_P|T],[HeadNT:_PNT|TNT],Env,Body,VC,R,Probs,DB,BDDAnd,N,[Clause|Clauses],Module):-
 1214  list2and(BodyList,Body),
 1215  append(BodyList,[sphere:sphere_check_inconsistency(Module,HeadNT,Env,BDDAnd)],BodyListD),
 1216  list2and(BodyListD,BodyD),
 1217  generate_clause_db(Head,Env,BodyD,VC,R,Probs,DB,BDDAnd,N,Clause,Module),
 1218  N1 is N+1,
 1219  generate_rules_d_1_db(T,TNT,Env,Body,VC,R,Probs,DB,BDDAnd,N1,Clauses,Module)
 1219.
 1220
 1221generate_rules_d_1([],_,_Env,_Body,_VC,_R,_Probs,_BDDAnd,_N,[],_Module).
 1222
 1223generate_rules_d_1([Head:_P1,'':_P2],[HeadNT:_P1NT,'':_P2NT],Env,Body,VC,R,Probs,BDDAnd,N,[Clause],Module):-!,
 1224  list2and(BodyList,Body),
 1225  append(BodyList,[sphere:sphere_check_inconsistency(Module,HeadNT,Env,BDDAnd)],BodyListD),
 1226  list2and(BodyListD,BodyD),
 1227  generate_clause(Head,Env,BodyD,VC,R,Probs,BDDAnd,N,Clause,Module).
 1228
 1229generate_rules_d_1([Head:_P|T],[HeadNT:_PNT|TNT],Env,Body,VC,R,Probs,BDDAnd,N,[Clause|Clauses],Module):-
 1230  list2and(BodyList,Body),
 1231  append(BodyList,[sphere:sphere_check_inconsistency(Module,HeadNT,Env,BDDAnd)],BodyListD),
 1232  list2and(BodyListD,BodyD),
 1233  generate_clause(Head,Env,BodyD,VC,R,Probs,BDDAnd,N,Clause,Module),
 1234  N1 is N+1,
 1235  generate_rules_d_1(T,TNT,Env,Body,VC,R,Probs,BDDAnd,N1,Clauses,Module).
 1236
 1237generate_rules_d_2_db([],_Env,_Body,_VC,_R,_Probs,_DB,_BDDAnd,_N,[],_Module).
 1238
 1239generate_rules_d_2_db([Head:_P1,'':_P2],Env,Body,VC,R,Probs,DB,BDDAnd,N,[Clause],Module):-!,
 1240  list2and(BodyList,Body),name_value(Head,HeadNegH),
 1241  append(BodyList,[sphere:sphere_neg_H(Module,_H1,HeadNegH,Env,BDDAnd,BDDN),andc(Env,BDDAnd,BDDN,BDDAndD),sphere:sphere_check_inconsistency(Module,HeadNegH,Env,BDDAndD)],BodyListD),
 1242  list2and(BodyListD,BodyD),
 1243  generate_clause_2_db(Head,Env,BodyD,VC,R,Probs,DB,BDDAndD,N,Clause,Module).
 1244
 1245generate_rules_d_2_db([Head:_P|T],Env,Body,VC,R,Probs,DB,BDDAnd,N,[Clause|Clauses],Module):-
 1246  list2and(BodyList,Body),name_value(Head,HeadNegH),
 1247  append(BodyList,[sphere:sphere_neg_H(Module,_H1,HeadNegH,Env,BDDAnd,BDDN),andc(Env,BDDAnd,BDDN,BDDAndD),sphere:sphere_check_inconsistency(Module,HeadNegH,Env,BDDAndD)],BodyListD),
 1248  list2and(BodyListD,BodyD),
 1249  generate_clause_db(Head,Env,BodyD,VC,R,Probs,DB,BDDAndD,N,Clause,Module),
 1250  N1 is N+1,
 1251  generate_rules_d_2_db(T,Env,Body,VC,R,Probs,DB,BDDAnd,N1,Clauses,Module).
 1252
 1253generate_rules_d_2([],_Env,_Body,_VC,_R,_Probs,_BDDAnd,_N,[],_Module).
 1254
 1255generate_rules_d_2([Head:_P1,'':_P2],Env,Body,VC,R,Probs,BDDAnd,N,[Clause],Module):-!,
 1256  list2and(BodyList,Body),name_value(Head,HeadNegH),
 1257  append(BodyList,[sphere:sphere_neg_H(Module,_H1,HeadNegH,Env,BDDAnd,BDDN),andc(Env,BDDAnd,BDDN,BDDAndD),sphere:sphere_check_inconsistency(Module,HeadNegH,Env,BDDAndD)],BodyListD),
 1258  list2and(BodyListD,BodyD),
 1259  generate_clause(Head,Env,BodyD,VC,R,Probs,BDDAndD,N,Clause,Module).
 1260
 1261generate_rules_d_2([Head:_P|T],Env,Body,VC,R,Probs,BDDAnd,N,[Clause|Clauses],Module):-
 1262  list2and(BodyList,Body),name_value(Head,HeadNegH),
 1263  append(BodyList,[sphere:sphere_neg_H(Module,_H1,HeadNegH,Env,BDDAnd,BDDN),andc(Env,BDDAnd,BDDN,BDDAndD),sphere:sphere_check_inconsistency(Module,HeadNegH,Env,BDDAndD)],BodyListD),
 1264  list2and(BodyListD,BodyD),
 1265  generate_clause(Head,Env,BodyD,VC,R,Probs,BDDAndD,N,Clause,Module),
 1266  N1 is N+1,
 1267  generate_rules_d_2(T,Env,Body,VC,R,Probs,BDDAnd,N1,Clauses,Module).
 1268
 1269name_value(H, H1) :-
 1270 H=..[String|Args],
 1271 sub_string(String, Before, _, _, "spheredoubled"), !,
 1272 sub_string(String, 0, Before, _, NameString),
 1273 atom_string(Name,NameString),
 1274 H1=..[Name|Args].
 1275
 1276%name_value(H,H).
 1277
 1278% ================================================================================
 1279%
 1280%   TERM EXPANSION
 1281%
 1282% ================================================================================
 1283sphere_expansion(begin_of_file,_):-
 1284  !,
 1285  fail.
 1286
 1287sphere_expansion((:- begin_phkb), []) :-
 1288  prolog_load_context(module, M),
 1289  sphere_input_mod(M),!,
 1290  assert(M:sphere_on).
 1291
 1292sphere_expansion((:- end_phkb), OCRules) :- 
 1293  prolog_load_context(module, M),
 1294  sphere_input_mod(M),!,
 1295  M:lp_axioms_for_oracle(LPList0,LBody0),
 1296  sort(LPList0,LPList),
 1297  sort(LBody0,LBody),
 1298  assert_lp_axioms(M,LPList),
 1299  create_oracle_calls(M,LPList,LBody,OCRules),
 1300  %retractall(M:lp_axioms_for_oracle(_,_)),
 1301  retractall(M:sphere_on).
 1302
 1303sphere_expansion(values(A,B), values(A,B)) :-
 1304  prolog_load_context(module, M),
 1305  sphere_input_mod(M),M:sphere_on,!.
 1306
 1307sphere_expansion(kb_prefix(A,B), []) :-
 1308  trillo:add_kb_prefix(A,B),!.
 1309
 1310sphere_expansion(owl_rdf(A), []) :-
 1311  trillo_utility_translation:parse_rdf_from_owl_rdf_pred(A),!.
 1312
 1313sphere_expansion((Head :- Body),Clauses):-
 1314  prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1315  M:local_sphere_setting(depth_bound,true),
 1316% disjunctive clause with more than one head atom and depth_bound
 1317  Head = (_;_), !,
 1318  list2or(HeadListOr, Head),
 1319  double_head(HeadListOr,HeadListOrD),
 1320  process_head(HeadListOr, HeadList),
 1321  process_head(HeadListOrD, HeadListD),
 1322  list2and(BodyList, Body),
 1323  double_body(BodyList,BodyListD1,BodyListD2),
 1324  get_next_rule_number(M,R),
 1325  get_probs(HeadList,Probs),
 1326  create_doubled_rules_1_db(HeadList,BodyListD1,R,Probs,DB,M,ClausesD1),
 1327  create_doubled_rules_2_db(HeadListD,BodyListD2,R,Probs,DB,M,ClausesD2),
 1328  append(ClausesD1,ClausesD2,Clauses).
 1329
 1330
 1331sphere_expansion((Head :- Body),Clauses):-
 1332	  %trace,
 1333    ((Head:- Body) \= ((sphere_expansion(_,_)) :- _ )),
 1334  prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1335% disjunctive clause with more than one head atom without depth_bound
 1336  Head = (_;_), !,
 1337  list2or(HeadListOr, Head),
 1338  double_head(HeadListOr,HeadListOrD),
 1339  process_head(HeadListOr, HeadList),
 1340  process_head(HeadListOrD, HeadListD),
 1341  list2and(BodyList, Body),
 1342  double_body(BodyList,BodyListD1,BodyListD2),
 1343  get_next_rule_number(M,R),
 1344  get_probs(HeadList,Probs), % gets the probs list
 1345  create_doubled_rules_1(HeadList,BodyListD1,R,Probs,M,ClausesD1),
 1346  create_doubled_rules_2(HeadListD,BodyListD2,R,Probs,M,ClausesD2),
 1347  append(ClausesD1,ClausesD2,Clauses).
 1348
 1349sphere_expansion((Head :- Body), []) :-
 1350% disjunctive clause with a single head atom with prob. 0 without depth_bound --> the rule is not loaded in the theory and not counted by NR
 1351  prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1352  ((Head:-Body) \= ((sphere_expansion(_,_) ):- _ )),
 1353  (Head = (_:P);Head=(P::_)),
 1354  ground(P),
 1355  P=:=0.0, !.
 1356
 1357sphere_expansion((Head :- Body), Clauses) :-
 1358% disjunctive clause with a single head atom and depth_bound
 1359  prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1360  M:local_sphere_setting(depth_bound,true),
 1361  ((Head:-Body) \= ((sphere_expansion(_,_) ):- _ )),
 1362  list2or(HeadListOr, Head),
 1363  double_head(HeadListOr,HeadListOrD),
 1364  process_head(HeadListOr, HeadList),
 1365  process_head(HeadListOrD, HeadListD),
 1366  HeadList=[_H:_],!,
 1367  list2and(BodyList, Body),
 1368  double_body(BodyList,BodyListD1,BodyListD2),
 1369  process_body_db(BodyListD1,BDD,BDDAnd,DB,[],_Vars,BodyListD11,Env,M),
 1370  process_body_db(BodyListD2,BDD,BDDAnd,DB,[],_VarsD,BodyListD21,Env,M),
 1371  append([onec(Env,BDD)],BodyListD11,BodyListD12),
 1372  append([onec(Env,BDD)],BodyListD21,BodyListD22),
 1373  append(BodyListD12,[sphere:sphere_check_inconsistency(M,H,Env,BDDAnd)],BodyListD13),
 1374  append(BodyListD22,[sphere:sphere_neg_H(M,_H12,H,Env,BDDAnd,BDDN),andc(Env,BDDAnd,BDDN,BDDAndD),sphere:sphere_check_inconsistency(M,H,Env,BDDAndD)],BodyListD23),
 1375  list2and([DBH>=1,DB is DBH -1|BodyListD13],Body1),
 1376  list2and([DBH>=1,DB is DBH -1|BodyListD23],BodyD1),
 1377  to_table(M,HeadList,TabDirD1,[H1:_]),
 1378  to_table(M,HeadListD,TabDirD2,[HD1:_]),
 1379  add_bdd_arg_db(H1,Env,BDDAnd,DBH,M,Head1),
 1380  add_bdd_arg_db(HD1,Env,BDDAndD,DBH,M,HeadD1),
 1381  append(TabDirD1,[(Head1 :- Body1)],ClausesD1),
 1382  append(TabDirD2,[(HeadD1 :- BodyD1)],ClausesD2),
 1383  append(ClausesD1,ClausesD2,Clauses).
 1384
 1385sphere_expansion((Head :- Body), Clauses) :-
 1386% disjunctive clause with a single head atom without depth_bound with prob =1
 1387  prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1388  ((Head:-Body) \= ((sphere_expansion(_,_) ):- _ )),
 1389  list2or(HeadListOr, Head),
 1390  double_head(HeadListOr,HeadListOrD),
 1391  process_head(HeadListOr, HeadList),
 1392  process_head(HeadListOrD, HeadListD),
 1393  HeadList=[_H:_],!,
 1394  list2and(BodyList, Body),
 1395  double_body(BodyList,BodyListD1,BodyListD2),
 1396  process_body(BodyListD1,BDD,BDDAnd,[],_Vars,BodyListD11,Env,M),
 1397  process_body(BodyListD2,BDD,BDDAnd,[],_VarsD,BodyListD21,Env,M),
 1398  append([onec(Env,BDD)],BodyListD11,BodyListD12),
 1399  append([onec(Env,BDD)],BodyListD21,BodyListD22),
 1400  append(BodyListD12,[sphere:sphere_check_inconsistency(M,H,Env,BDDAnd)],BodyListD13),
 1401  append(BodyListD22,[sphere:sphere_neg_H(M,_H12,H,Env,BDDAnd,BDDN),andc(Env,BDDAnd,BDDN,BDDAndD),sphere:sphere_check_inconsistency(M,H,Env,BDDAndD)],BodyListD23),
 1402  list2and(BodyListD13,Body1),
 1403  list2and(BodyListD23,BodyD1),
 1404  to_table(M,HeadList,TabDirD1,[H1:_]),
 1405  to_table(M,HeadListD,TabDirD2,[HD1:_]),
 1406  add_bdd_arg(H1,Env,BDDAnd,M,Head1),
 1407  add_bdd_arg(HD1,Env,BDDAndD,M,HeadD1),
 1408  append(TabDirD1,[(Head1 :- Body1)],ClausesD1),
 1409  append(TabDirD2,[(HeadD1 :- BodyD1)],ClausesD2),
 1410  append(ClausesD1,ClausesD2,Clauses).
 1411
 1412/*
 1413sphere_expansion((Head :- Body), Clauses) :-
 1414% disjunctive clause with a single head atom and DB, with prob \= 1
 1415  prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1416  M:local_sphere_setting(depth_bound,true),
 1417  ((Head:-Body) \= ((sphere_expansion(_,_) ):- _ )),
 1418  (Head = (_H:_);Head=(_::_H)), !,
 1419  list2or(HeadListOr, Head),
 1420  double_head(HeadListOr,HeadListOrD),
 1421  process_head(HeadListOr, HeadList),% adds null if needed
 1422  process_head(HeadListOrD, HeadListD),
 1423  list2and(BodyList, Body),
 1424  double_body(BodyList,BodyListD1,BodyListD2),
 1425  process_body_db(BodyListD1,BDD,BDDAnd, DB,[],_Vars,BodyListD11,Env,M),
 1426  process_body_db(BodyListD2,BDD,BDDAnd, DB,[],_VarsD,BodyListD21,Env,M),
 1427  append([onec(Env,BDD)],BodyListD11,BodyListD12),
 1428  append([onec(Env,BDD)],BodyListD21,BodyListD22),
 1429  append(BodyListD12,[sphere:sphere_check_inconsistency(M,H,Env,BDDAnd)],BodyListD13),
 1430  append(BodyListD22,[sphere:sphere_neg_H(M,_H12,H,Env,BDDAnd,BDDN),andc(Env,BDDAnd,BDDN,BDDAndD),sphere:sphere_check_inconsistency(M,H,Env,BDDAndD)],BodyListD23),
 1431  list2and(BodyListD13,Body1),
 1432  list2and(BodyListD23,BodyD1),
 1433  append(HeadList,BodyListD1,ListD1),
 1434  append(HeadListD,BodyListD2,ListD2),
 1435  term_variables(ListD1,VC1),
 1436  term_variables(ListD2,VC2),
 1437  get_next_rule_number(M,R),
 1438  get_probs(HeadList,Probs),%***test single_var
 1439  (M:local_sphere_setting(single_var,true)->
 1440    VC11 = [],VC12 = []
 1441  ;
 1442    VC11 = VC1,VC12 = VC2
 1443  ),
 1444  to_table(M,HeadList,TabDir,[H1:_]),
 1445  to_table(M,HeadListD,TabDir,[HD1:_]),
 1446  generate_doubled_clause_1_db(H1,Env,Body1,VC11,R,Probs,DB,BDDAnd,0,Clauses0,M),
 1447  generate_doubled_clause_2_db(HD1,Env,BodyD1,VC12,R,Probs,DB,BDDAnd,0,Clauses1,M),
 1448  append(TabDir,[Clauses0,Clauses1],Clauses).
 1449
 1450sphere_expansion((Head :- Body), [rule_by_num(R,HeadList,BodyListD13,VC11),rule_by_num(R,HeadListD,BodyListD23,VC12)|Clauses]) :-
 1451% disjunctive clause with a single head atom without DB, with prob \= 1
 1452  prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1453  ((Head:-Body) \= ((sphere_expansion(_,_) ):- _ )),
 1454  (Head = (_H:_);Head = (_::_H)), !,
 1455  list2or(HeadListOr, Head),
 1456  double_head(HeadListOr,HeadListOrD),
 1457  process_head(HeadListOr, HeadList),% adds null if needed
 1458  process_head(HeadListOrD, HeadListD),
 1459  list2and(BodyList, Body),
 1460  double_body(BodyList,BodyListD1,BodyListD2),
 1461  process_body(BodyListD1,BDD,BDDAnd, [],_Vars,BodyListD11,Env,M),
 1462  process_body(BodyListD2,BDD,BDDAnd, [],_VarsD,BodyListD21,Env,M),
 1463  append([onec(Env,BDD)],BodyListD11,BodyListD12),
 1464  append([onec(Env,BDD)],BodyListD21,BodyListD22),
 1465  append(BodyListD12,[sphere:sphere_check_inconsistency(M,H,Env,BDDAnd)],BodyListD13),
 1466  append(BodyListD22,[sphere:sphere_neg_H(M,_H12,H,Env,BDDAnd,BDDN),andc(Env,BDDAnd,BDDN,BDDAndD),sphere:sphere_check_inconsistency(M,H,Env,BDDAndD)],BodyListD23),
 1467  list2and(BodyListD13,Body1),
 1468  list2and(BodyListD23,BodyD1),
 1469  append(HeadList,BodyListD1,ListD1),
 1470  append(HeadListD,BodyListD2,ListD2),
 1471  term_variables(ListD1,VC1),
 1472  term_variables(ListD2,VC2),
 1473  get_next_rule_number(M,R),
 1474  get_probs(HeadList,Probs),%***test single_vars
 1475  (M:local_sphere_setting(single_var,true)->
 1476    VC11 = [],VC12 = []
 1477  ;
 1478    VC11 = VC1,VC12 = VC2
 1479  ),
 1480  to_table(M,HeadList,TabDir,[H1:_]),
 1481  to_table(M,HeadListD,TabDir,[HD1:_]),
 1482  generate_doubled_clause_1(H1,Env,Body1,VC11,R,Probs,BDDAnd,0,Clauses0,M),
 1483  generate_doubled_clause_2(HD1,Env,BodyD1,VC12,R,Probs,BDDAnd,0,Clauses1,M),
 1484  append(TabDir,[Clauses0,Clauses1],Clauses).
 1485*/
 1486sphere_expansion((Head :- Body), Clauses) :-
 1487  % disjunctive clause with a single head atom and DB, with prob \= 1
 1488    prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1489    M:local_sphere_setting(depth_bound,true),
 1490    ((Head:-Body) \= ((sphere_expansion(_,_) ):- _ )),
 1491    (Head = (_H:_);Head=(_::_H)), !,
 1492    list2or(HeadListOr, Head),
 1493    double_head(HeadListOr,HeadListOrD),
 1494    process_head(HeadListOr, HeadList),% adds null if needed
 1495    process_head(HeadListOrD, HeadListD),
 1496    list2and(BodyList, Body),
 1497    double_body(BodyList,BodyListD1,BodyListD2),
 1498    get_next_rule_number(M,R),
 1499    get_probs(HeadList,Probs),%***test single_var
 1500    create_doubled_rules_1_db(HeadList,BodyListD1,R,Probs,DB,M,ClausesD1),
 1501    create_doubled_rules_2_db(HeadListD,BodyListD2,R,Probs,DB,M,ClausesD2),
 1502    append(ClausesD1,ClausesD2,Clauses).
 1503  
 1504  sphere_expansion((Head :- Body), Clauses) :-
 1505  % disjunctive clause with a single head atom without DB, with prob \= 1
 1506    prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1507    ((Head:-Body) \= ((sphere_expansion(_,_) ):- _ )),
 1508    (Head = (_H:_);Head = (_::_H)), !,
 1509    list2or(HeadListOr, Head),
 1510    double_head(HeadListOr,HeadListOrD),
 1511    process_head(HeadListOr, HeadList),% adds null if needed
 1512    process_head(HeadListOrD, HeadListD),
 1513    list2and(BodyList, Body),
 1514    double_body(BodyList,BodyListD1,BodyListD2),
 1515    get_next_rule_number(M,R),
 1516    get_probs(HeadList,Probs),%***test single_vars
 1517    create_doubled_rules_1(HeadList,BodyListD1,R,Probs,M,ClausesD1),
 1518    create_doubled_rules_2(HeadListD,BodyListD2,R,Probs,M,ClausesD2),
 1519    append(ClausesD1,ClausesD2,Clauses).
 1520
 1521
 1522/*sphere_expansion((Head :- Body),Clauses) :-
 1523% definite clause for db facts
 1524  prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1525  ((Head:-Body) \= ((sphere_expansion(_,_)) :- _ )),
 1526  Head=db(Head1),!,
 1527  Clauses=(Head1 :- Body).
 1528*/
 1529sphere_expansion((Head :- Body),Clauses) :-
 1530% definite clause with depth_bound
 1531  prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1532  M:local_sphere_setting(depth_bound,true),
 1533  ((Head:-Body) \= ((sphere_expansion(_,_)) :- _ )),!,
 1534  double_head([Head],[HeadD]),
 1535  list2and(BodyList, Body),
 1536  double_body(BodyList,BodyListD1,BodyListD2),
 1537  process_body_db(BodyListD1,BDD,BDDAnd,DB,[],_Vars,BodyListD12,Env,M),
 1538  process_body_db(BodyListD2,BDD,BDDAnd,DB,[],_VarsD,BodyListD22,Env,M),
 1539  append([onec(Env,BDD)],BodyListD12,BodyListD13),
 1540  append([onec(Env,BDD)],BodyListD22,BodyListD23),
 1541  append(BodyListD13,[sphere:sphere_check_inconsistency(M,Head,Env,BDDAnd)],BodyListD14),
 1542  append(BodyListD23,[sphere:sphere_neg_H(M,_H12,Head,Env,BDDAnd,BDDN),andc(Env,BDDAnd,BDDN,BDDAndD),sphere:sphere_check_inconsistency(M,Head,Env,BDDAndD)],BodyListD24),
 1543  list2and([DBH>=1,DB is DBH-1|BodyListD14],BodyD12),
 1544  list2and([DBH>=1,DB is DBH-1|BodyListD24],BodyD22),
 1545  to_table(M,[Head:_],TabDirD1,[Head1:_]),
 1546  to_table(M,[HeadD:_],TabDirD2,[HeadD1:_]),
 1547  add_bdd_arg_db(Head1,Env,BDDAnd,DBH,M,Head2),
 1548  add_bdd_arg_db(HeadD1,Env,BDDAndD,DBH,M,HeadD2),
 1549  assert_head_pred(M,Head),
 1550  append(TabDirD1,[(Head2 :- BodyD12)],ClausesD1),
 1551  append(TabDirD2,[(HeadD2 :- BodyD22)],ClausesD2),
 1552  append(ClausesD1,ClausesD2,Clauses).
 1553
 1554sphere_expansion((Head :- Body),Clauses) :-
 1555%  writeln((Head:-Body)),
 1556 % trace,
 1557% definite clause without DB
 1558  prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1559  ((Head:-Body) \= ((sphere_expansion(_,_)) :- _ )),!,
 1560  double_head([Head],[HeadD]),
 1561  list2and(BodyList, Body),
 1562  double_body(BodyList,BodyListD1,BodyListD2),
 1563  process_body(BodyListD1,BDD,BDDAnd,[],_Vars,BodyListD12,Env,M),
 1564  process_body(BodyListD2,BDD,BDDAnd,[],_VarsD,BodyListD22,Env,M),
 1565  append([onec(Env,BDD)],BodyListD12,BodyListD13),
 1566  append([onec(Env,BDD)],BodyListD22,BodyListD23),
 1567  append(BodyListD13,[sphere:sphere_check_inconsistency(M,Head,Env,BDDAnd)],BodyListD14),
 1568  append(BodyListD23,[sphere:sphere_neg_H(M,_H12,Head,Env,BDDAnd,BDDN),andc(Env,BDDAnd,BDDN,BDDAndD),sphere:sphere_check_inconsistency(M,Head,Env,BDDAndD)],BodyListD24),
 1569  list2and(BodyListD14,BodyD12),
 1570  list2and(BodyListD24,BodyD22),
 1571  to_table(M,[Head:_],TabDirD1,[Head1:_]),
 1572  to_table(M,[HeadD:_],TabDirD2,[HeadD1:_]),
 1573  add_bdd_arg(Head1,Env,BDDAnd,M,Head2),
 1574  add_bdd_arg(HeadD1,Env,BDDAndD,M,HeadD2),
 1575  assert_head_pred(M,Head),
 1576  append(TabDirD1,[(Head2 :- BodyD12)],ClausesD1),
 1577  append(TabDirD2,[(HeadD2 :- BodyD22)],ClausesD2),
 1578  append(ClausesD1,ClausesD2,Clauses).
 1579
 1580sphere_expansion(Axiom,[]):-
 1581  prolog_load_context(module, M),
 1582  trillo_utility_translation:is_axiom(Axiom),
 1583  trillo_utility_translation:create_and_assert_axioms(M,Axiom).
 1584
 1585sphere_expansion(Head,
 1586  [rule_by_num(R,HeadListD1,[],VC1),rule_by_num(R,HeadListD2,[],VC1)|Clauses]) :-
 1587  prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1588  M:local_sphere_setting(depth_bound,true),
 1589% disjunctive FACT with more than one head atom e db
 1590  Head=(_;_), !,
 1591  list2or(HeadListOr, Head),
 1592  double_head(HeadListOr,HeadListOrD),
 1593  process_head(HeadListOr, HeadListD1),
 1594  process_head(HeadListOrD, HeadListD2),
 1595  term_variables(HeadListD1,VC),
 1596  get_next_rule_number(M,R),
 1597  get_probs(HeadListD1,Probs),
 1598  (M:local_sphere_setting(single_var,true)->
 1599    VC1 = []
 1600  ;
 1601    VC1 = VC
 1602  ),
 1603  to_table(M,HeadListD1,TabDirD1,HeadListD11),
 1604  to_table(M,HeadListD2,TabDirD2,HeadListD21),
 1605  generate_rules_fact_db(HeadListD11,_Env,VC1,R,Probs,0,ClausesD10,M,false),
 1606  generate_rules_fact_db(HeadListD21,_EnvD1,VC1,R,Probs,0,ClausesD20,M,true),
 1607  append(TabDirD1,ClausesD10,ClausesD1),
 1608  append(TabDirD2,ClausesD20,ClausesD2),
 1609  append(ClausesD1,ClausesD2,Clauses).
 1610
 1611sphere_expansion(Head,[rule_by_num(R,HeadListD1,[],VC1),rule_by_num(R,HeadListD2,[],VC1)|Clauses]) :-
 1612  prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1613% disjunctive fact with more than one head atom senza db
 1614  Head=(_;_), !,
 1615  list2or(HeadListOr, Head),
 1616  double_head(HeadListOr,HeadListOrD),
 1617  process_head(HeadListOr, HeadListD1),
 1618  process_head(HeadListOrD, HeadListD2),
 1619  term_variables(HeadListD1,VC),
 1620  get_next_rule_number(M,R),
 1621  get_probs(HeadListD1,Probs), %**** test single_var
 1622  (M:local_sphere_setting(single_var,true)->
 1623    VC1 = []
 1624  ;
 1625    VC1 = VC
 1626  ),
 1627  to_table(M,HeadListD1,TabDirD1,HeadListD11),
 1628  to_table(M,HeadListD2,TabDirD2,HeadListD21),
 1629  generate_rules_fact(HeadListD11,_Env,VC1,R,Probs,0,ClausesD10,M,false),
 1630  generate_rules_fact(HeadListD21,_EnvD1,VC1,R,Probs,0,ClausesD20,M,true),
 1631  append(TabDirD1,ClausesD10,ClausesD1),
 1632  append(TabDirD2,ClausesD20,ClausesD2),
 1633  append(ClausesD1,ClausesD2,Clauses).
 1634
 1635sphere_expansion(Head,[]) :-
 1636  prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1637% disjunctive fact with a single head atom with prob. 0
 1638  (Head \= ((sphere_expansion(_,_)) :- _ )),
 1639  (Head = (_:P); Head = (P::_)),
 1640  ground(P),
 1641  P=:=0.0, !.
 1642
 1643sphere_expansion(Head,Clauses) :-
 1644  prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1645  M:local_sphere_setting(depth_bound,true),
 1646% disjunctive fact with a single head atom with prob = 1 and depth bound
 1647  (Head \= ((sphere_expansion(_,_)) :- _ )),
 1648  (Head = (H:P); Head = (P::H)),
 1649  ground(P),
 1650  P=:=1.0, !,
 1651  double_head([Head],[HeadD]),
 1652  list2and([onec(Env,BDD),sphere:sphere_check_inconsistency(M,H,Env,BDD)],Body1),
 1653  list2and([onec(Env,BDDOne),sphere:sphere_neg_H(M,_HD11,H,Env,BDDOne,BDDN),andc(Env,BDDOne,BDDN,BDD),sphere:sphere_check_inconsistency(M,H,Env,BDD)],BodyD1),
 1654  to_table(M,[Head:_],TabDirD1,[H1:_]),
 1655  to_table(M,[HeadD:_],TabDirD2,[HD1:_]),
 1656  add_bdd_arg_db(H1,Env,BDD,_DB,M,Head1),
 1657  add_bdd_arg_db(HD1,Env,BDD,_DBD,M,HeadD1),
 1658  assert_head_pred(M,H),
 1659  append(TabDirD1,[(Head1 :- Body1)],ClausesD1),
 1660  append(TabDirD2,[(HeadD1 :- BodyD1)],ClausesD2),
 1661  append(ClausesD1,ClausesD2,Clauses).
 1662
 1663sphere_expansion(Head,Clauses) :-
 1664  prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1665% disjunctive fact with a single head atom with prob = 1 without depth bound
 1666  (Head \= ((sphere_expansion(_,_)) :- _ )),
 1667  (Head = (H:P);Head =(P::H)),
 1668  ground(P),
 1669  P=:=1.0, !,
 1670  double_head([Head],[HeadD]),
 1671  list2and([onec(Env,BDD),sphere:sphere_check_inconsistency(M,H,Env,BDD)],Body1),
 1672  list2and([onec(Env,BDDOne),sphere:sphere_neg_H(M,_HD11,H,Env,BDDOne,BDDN),andc(Env,BDDOne,BDDN,BDD),sphere:sphere_check_inconsistency(M,H,Env,BDD)],BodyD1),
 1673  to_table(M,[Head:_],TabDirD1,[H1:_]),
 1674  to_table(M,[HeadD:_],TabDirD2,[HD1:_]),
 1675  add_bdd_arg(H1,Env,BDD,M,Head1),
 1676  add_bdd_arg(HD1,Env,BDD,M,HeadD1),
 1677  assert_head_pred(M,H),
 1678  append(TabDirD1,[(Head1 :- Body1)],ClausesD1),
 1679  append(TabDirD2,[(HeadD1 :- BodyD1)],ClausesD2),
 1680  append(ClausesD1,ClausesD2,Clauses).
 1681
 1682sphere_expansion(Head,[rule_by_num(R,HeadList,[],VC1)|Clauses]) :-
 1683  prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1684  M:local_sphere_setting(depth_bound,true),
 1685% disjunctive fact with a single head atom and generic prob with depth bound
 1686  (Head \= ((sphere_expansion(_,_)) :- _ )),
 1687  (Head=(H:_);Head=(_::H)), !,
 1688  list2or(HeadListOr, Head),
 1689  double_head(HeadListOr,HeadListOrD),
 1690  process_head(HeadListOr, HeadList),
 1691  process_head(HeadListOrD, HeadListD),
 1692  term_variables(HeadList,VC),
 1693  get_next_rule_number(M,R),
 1694  get_probs(HeadList,Probs),
 1695  to_table(M,HeadList,TabDirD1,[H1:_]),
 1696  to_table(M,HeadListD,TabDirD2,[HD1:_]),
 1697  add_bdd_arg_db(H1,Env,BDD,_DB,M,Head1),
 1698  add_bdd_arg_db(HD1,Env,BDD,_DBD,M,HeadD1),
 1699  (M:local_sphere_setting(single_var,true)->
 1700    VC1 = []
 1701  ;
 1702    VC1 = VC
 1703  ),
 1704  Clauses0=[(Head1:-(get_var_n(M,Env,R,VC1,Probs,V),equalityc(Env,V,0,BDD),sphere:sphere_check_inconsistency(M,H,Env,BDD)))],
 1705  ClausesD0=[(HeadD1:-(get_var_n(M,Env,R,VC1,Probs,V),equalityc(Env,V,0,BDDH),sphere:sphere_neg_H(M,_HD11,H,Env,BDDH,BDDN),andc(Env,BDDH,BDDN,BDD),sphere:sphere_check_inconsistency(M,H,Env,BDD)))],
 1706  append(TabDirD1,Clauses0,ClausesD1),
 1707  append(TabDirD2,ClausesD0,ClausesD2),
 1708  append(ClausesD1,ClausesD2,Clauses).
 1709
 1710sphere_expansion(Head,[rule_by_num(R,HeadList,[],VC1)|Clauses]) :-
 1711  prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1712% disjunctive fact with a single head atom and generic prob without depth bound
 1713  (Head \= ((sphere_expansion(_,_)) :- _ )),
 1714  (Head=(H:_);Head=(_::H)), !,
 1715  list2or(HeadListOr, Head),
 1716  double_head(HeadListOr,HeadListOrD),
 1717  process_head(HeadListOr, HeadList),
 1718  process_head(HeadListOrD, HeadListD),
 1719  term_variables(HeadList,VC),
 1720  get_next_rule_number(M,R),
 1721  get_probs(HeadList,Probs),
 1722  to_table(M,HeadList,TabDirD1,[H1:_]),
 1723  to_table(M,HeadListD,TabDirD2,[HD1:_]),
 1724  % write('headlist: '), writeln(HeadList),
 1725  % write('h1: '), writeln(H1),
 1726  add_bdd_arg(H1,Env,BDD,M,Head1),%***test single_var
 1727  add_bdd_arg(HD1,Env,BDD,M,HeadD1),%***test single_var
 1728  % write('head1: '), writeln(Head1),
 1729  % write('vc: '), writeln(VC),
 1730  (M:local_sphere_setting(single_var,true)->
 1731    VC1 = []
 1732  ;
 1733    VC1 = VC
 1734  ),
 1735  Clauses0=[(Head1:-(get_var_n(M,Env,R,VC1,Probs,V),equalityc(Env,V,0,BDD),sphere:sphere_check_inconsistency(M,H,Env,BDD)))],
 1736  ClausesD0=[(HeadD1:-(get_var_n(M,Env,R,VC1,Probs,V),equalityc(Env,V,0,BDDH),sphere:sphere_neg_H(M,_HD11,H,Env,BDDH,BDDN),andc(Env,BDDH,BDDN,BDD),sphere:sphere_check_inconsistency(M,H,Env,BDD)))],
 1737  append(TabDirD1,Clauses0,ClausesD1),
 1738  append(TabDirD2,ClausesD0,ClausesD2),
 1739  append(ClausesD1,ClausesD2,Clauses).
 1740
 1741sphere_expansion((:- set_sphere(P,V)), []) :-!,
 1742  prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1743  set_sphere(P,V).
 1744
 1745sphere_expansion((:- set_sw(A,B)), []) :-!,
 1746  prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1747  set_sw(M:A,B).
 1748
 1749
 1750sphere_expansion(Head, Clauses) :-
 1751  prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1752  M:local_sphere_setting(depth_bound,true),
 1753% definite fact with db
 1754  (Head \= ((sphere_expansion(_,_) ):- _ )),
 1755  (Head\= end_of_file),!,
 1756  double_head([Head],[HeadD]),
 1757  to_table(M,[Head:_],TabDirD1,[Head1:_]),
 1758  to_table(M,[HeadD:_],TabDirD2,[HeadD1:_]),
 1759  add_bdd_arg_db(Head1,Env,One,_DB,M,Head2),
 1760  add_bdd_arg_db(HeadD1,Env,One,_DBD,M,HeadD2),
 1761  assert_head_pred(M,Head),
 1762  append(TabDirD1,[(Head2:-(onec(Env,One),sphere:sphere_check_inconsistency(M,Head,Env,One)))],ClausesD1),
 1763  append(TabDirD2,[(HeadD2:-(onec(Env,BDDOne),sphere:sphere_neg_H(M,_HD11,Head,Env,BDDOne,BDDN),andc(Env,BDDOne,BDDN,One),sphere:sphere_check_inconsistency(M,Head,Env,One)))],ClausesD2),
 1764  append(ClausesD1,ClausesD2,Clauses).
 1765
 1766sphere_expansion(Head, Clauses) :-
 1767  prolog_load_context(module, M),sphere_input_mod(M),M:sphere_on,
 1768% definite fact without db
 1769  (Head \= ((sphere_expansion(_,_) ):- _ )),
 1770  (Head\= end_of_file),
 1771  double_head([Head],[HeadD]),
 1772  to_table(M,[Head:_],TabDirD1,[Head1:_]),
 1773  to_table(M,[HeadD:_],TabDirD2,[HeadD1:_]),
 1774  add_bdd_arg(Head1,Env,One,M,Head2),
 1775  add_bdd_arg(HeadD1,Env,One,M,HeadD2),
 1776  assert_head_pred(M,Head),
 1777  append(TabDirD1,[(Head2:-(onec(Env,One),sphere:sphere_check_inconsistency(M,Head,Env,One)))],ClausesD1),
 1778  append(TabDirD2,[(HeadD2:-(onec(Env,BDDOne),sphere:sphere_neg_H(M,_HD11,Head,Env,BDDOne,BDDN),andc(Env,BDDOne,BDDN,One),sphere:sphere_check_inconsistency(M,Head,Env,One)))],ClausesD2),
 1779  append(ClausesD1,ClausesD2,Clauses).
 begin_lpad_pred is det
Initializes LPAD loading. /
 1786begin_lpad_pred:-
 1787  assert(sphere_input_mod(user)),
 1788  assert(user:sphere_on).
 end_lpad_pred is det
Terminates the cplint inference module. /
 1795end_lpad_pred:-
 1796  retractall(sphere_input_mod(_)),
 1797  retractall(user:sphere_on).
 1798
 1799list2or([],true):-!.
 1800
 1801list2or([X],X):-
 1802    X\=;(_,_),!.
 1803
 1804list2or([H|T],(H ; Ta)):-!,
 1805    list2or(T,Ta).
 1806
 1807
 1808list2and([],true):-!.
 1809
 1810list2and([X],X):-
 1811    X\=(_,_),!.
 1812
 1813list2and([H|T],(H,Ta)):-!,
 1814    list2and(T,Ta).
 1815
 1816transform(H,H1):-
 1817  H=..[prob|Args],
 1818  H1=..[prob_meta|Args].
 1819
 1820builtin(average(_L,_Av)) :- !.
 1821builtin(G) :-
 1822  swi_builtin(G).
 1823
 1824
 1825:- multifile sandbox:safe_meta/2. 1826
 1827sandbox:safe_meta(sphere:prob(_,_), []).
 1828sandbox:safe_meta(sphere:prob_meta(_,_), []).
 1829sandbox:safe_meta(sphere:bdd_dot_file(_,_,_), []).
 1830sandbox:safe_meta(sphere:bdd_dot_string(_,_,_), []).
 1831sandbox:safe_meta(sphere:get_bdd(_,_,_,_), []).
 1832sandbox:safe_meta(sphere:set_sphere(_,_),[]).
 1833sandbox:safe_meta(sphere:setting_sphere(_,_),[]).
 1834
 1835
 1836
 1837
 1838:- license(artisticv2). 1839
 1840:- thread_local sphere_file/1. 1841
 1842user:term_expansion(:-sphere, Clauses) :-!, %look sphere_old
 1843  prolog_load_context(source, Source),
 1844  asserta(sphere_file(Source)),
 1845  prolog_load_context(module, M),
 1846  trillo:set_up(M),
 1847  trillo_utility_translation:set_up_kb_loading(M),
 1848  trillo:add_kb_prefixes(M:['disponte'='http://ml.unife.it/disponte#','owl'='http://www.w3.org/2002/07/owl#']),
 1849  retractall(M:local_sphere_setting(_,_)),
 1850  findall(local_sphere_setting(P,V),default_setting_sphere(P,V),L),
 1851  assert_all(L,M,_),
 1852  assert(sphere_input_mod(M)),
 1853  retractall(M:rule_n(_)),
 1854  retractall(M:goal_n(_)),
 1855  retractall(M:lp_axioms_for_oracle(_,_)),
 1856  assert(M:rule_n(0)),
 1857  assert(M:goal_n(0)),
 1858  assert(M:lp_axioms_for_oracle([],[])),
 1859  M:(dynamic na/2, v/3, av/3, query_rule/4, rule_by_num/4, dec/3,
 1860    zero_clauses/1, sphere_on/0, tabled/1, '$cons'/2, inconsistency_warning/0),
 1861  retractall(M:query_rule(_,_,_,_)),
 1862  retractall(M:na(_,_)),
 1863  style_check(-discontiguous),
 1864  process_body([\+ '$cons'],BDD,BDDAnd,[],_Vars,BodyList2,Env,M),
 1865  append([onec(Env,BDD)],BodyList2,BodyList3),
 1866  list2and(BodyList3,Body2),
 1867  to_table(M,['$constraints':_],TabDir,[Head1:_]),
 1868  to_table(M,['$cons':_],TabDirCons,_),
 1869  add_bdd_arg(Head1,Env,BDDAnd,M,Head2),
 1870  append([TabDir,TabDirCons,[(Head2 :- Body2)]],Clauses).
 1871
 1872user:term_expansion(end_of_file, C) :- 
 1873  sphere_file(Source),
 1874  prolog_load_context(source, Source),
 1875  retractall(sphere_file(Source)),
 1876  prolog_load_context(module, M),
 1877  sphere_input_mod(M),!,
 1878  retractall(sphere_input_mod(M)),
 1879  findall(LZ,M:zero_clauses(LZ),L),
 1880  %findall(LZ,M:zero_clauses(LZ),L0),
 1881  %append(L0,L),
 1882  retractall(M:zero_clauses(_)),
 1883  retractall(M:tabled(_)),
 1884  append(L,[(:- style_check(+discontiguous)),end_of_file],C).
 1885
 1886user:term_expansion(In, Out) :-
 1887   \+ current_prolog_flag(xref, true),
 1888   sphere_file(Source),
 1889   prolog_load_context(source, Source),
 1890   sphere_expansion(In, Out)