1/* 2 LPAD and CP-Logic reasoning suite 3 File lpadclpbn.pl 4 Goal oriented interpreter for LPADs based on SLDNF 5 Copyright (c) 2008, Fabrizio Riguzzi 6 Inference is performed translating the portion of the LPAD related to the goal 7 into CLP(BN) 8*/ 9 10:- module(lpadclpbn, [p/1, 11 s/2,sc/3,s/6,sc/7,set/2,setting/2]). 12 13 14:-dynamic rule/4,def_rule/2,setting/2. 15 16:-use_module(library(lists)). 17:-use_module(library(ugraphs)). 18:-use_module(library(avl)). 19:-use_module(library(clpbn)). 20 21:-set_clpbn_flag(suppress_attribute_display,true). 22 23:-set_clpbn_flag(bnt_model,propositional). 24 25 26/* start of list of parameters that can be set by the user with 27set(Parameter,Value) */ 28setting(epsilon_parsing,0.00001). 29setting(save_dot,false). 30setting(ground_body,true). 31/* available values: true, false 32if true, both the head and the body of each clause will be grounded, otherwise 33only the head is grounded. In the case in which the body contains variables 34not appearing in the head, the body represents an existential event */ 35 36setting(cpt_zero,0.0001). 37 38/* end of list of parameters */ 39 40/* s(GoalsList,Prob) compute the probability of a list of goals 41GoalsLis can have variables, s returns in backtracking all the solutions with 42their corresponding probability */ 43s(GL,P):- 44 setof(Deriv,find_deriv(GL,Deriv),LDup),!, 45 append_all(LDup,[],L), 46 remove_head(L,L1), 47 remove_duplicates(L1,L2), 48 build_ground_lpad(L2,0,CL), 49 convert_to_clpbn(CL,GL,LV,P). 50 51s(_GL,0.0). 52/* sc(GoalsList,EvidenceList,Prob) compute the probability of a list of goals 53GoalsList given EvidenceList. Both lists can have variables, sc returns in 54backtracking all the solutions with their corresponding probability 55Time1 is the time for performing resolution 56Time2 is the time for performing bayesian inference */ 57sc(GL,GLC,P):- 58 (setof(Deriv,find_deriv(GLC,Deriv),LDupC)-> 59 (setof(Deriv,find_deriv(GL,Deriv),LDup)-> 60 append_all(LDup,[],L), 61 remove_head(L,L1), 62 append_all(LDupC,[],LC), 63 remove_head(LC,LC1), 64 append(L1,LC1,LD), 65 remove_duplicates(LD,LD1), 66 build_ground_lpad(LD1,0,CL), 67 convert_to_clpbn(CL,GL,LV,P,GLC) 68 ; 69 P=0.0 70 ) 71 ; 72 P=undef 73 ). 74 75 76 77/* s(GoalsList,Prob,Time1,Time2) compute the probability of a list of goals 78GoalsLis can have variables, s returns in backtracking all the solutions with 79their corresponding probability 80Time1 is the time for performing resolution 81Time2 is the time for performing bayesian inference */ 82s(GL,P,Time1,Time2):- 83 statistics(cputime,[_,_]), 84 statistics(walltime,[_,_]), 85 (setof(Deriv,find_deriv(GL,Deriv),LDup)-> 86 append_all(LDup,[],L), 87 remove_head(L,L1), 88 remove_duplicates(L1,L2), 89 build_ground_lpad(L2,0,CL), 90 convert_to_clpbn(CL,GL,LV,P), 91 statistics(cputime,[_,CT2]), 92 Time1 is CT2/1000, 93 statistics(walltime,[_,WT2]), 94 Time2 is WT2/1000 95 ; 96 P=0.0, 97 statistics(cputime,[_,CT1]), 98 Time1 is CT1/1000, 99 statistics(walltime,[_,WT1]), 100 Time2 is WT1/1000 101 ). 102 103s(GoalsList,Prob,CPUTime1,CPUTime2,WallTime1,WallTime2):- 104 solve(GoalsList,Prob,CPUTime1,CPUTime2,WallTime1,WallTime2). 105 106 107solve(GL,P,CPUTime1,CPUTime2,WallTime1,WallTime2):- 108 statistics(cputime,[_,_]), 109 statistics(walltime,[_,_]), 110 (setof(Deriv,find_deriv(GL,Deriv),LDup)-> 111 append_all(LDup,[],L), 112 remove_head(L,L1), 113 remove_duplicates(L1,L2), 114 statistics(cputime,[_,CT1]), 115 CPUTime1 is CT1/1000, 116 statistics(walltime,[_,WT1]), 117 WallTime1 is WT1/1000, 118 print_mem, 119 build_ground_lpad(L2,0,CL), 120 convert_to_clpbn(CL,GL,LV,P), 121 statistics(cputime,[_,CT2]), 122 CPUTime2 is CT2/1000, 123 statistics(walltime,[_,WT2]), 124 WallTime2 is WT2/1000 125 ; 126 print_mem, 127 P=0.0, 128 statistics(cputime,[_,CT1]), 129 CPUTime1 is CT1/1000, 130 statistics(walltime,[_,WT1]), 131 WallTime1 is WT1/1000, 132 CPUTime2 =0.0, 133 statistics(walltime,[_,WT2]), 134 WallTime2 =0.0 135 ),!, 136 format(user_error,"Memory after inference~n",[]), 137 print_mem. 138 139/* sc(GoalsList,EvidenceList,Prob) compute the probability of a list of goals 140GoalsList given EvidenceList. Both lists can have variables, sc returns in 141backtracking all the solutions with their corresponding probability */ 142 143sc(GL,GLC,P,CPUTime1,CPUTime2,WallTime1,WallTime2):- 144 statistics(cputime,[_,_]), 145 statistics(walltime,[_,_]), 146 (setof(Deriv,find_deriv(GLC,Deriv),LDupC)-> 147 (setof(Deriv,find_deriv(GL,Deriv),LDup)-> 148 append_all(LDup,[],L), 149 remove_head(L,L1), 150 append_all(LDupC,[],LC), 151 remove_head(LC,LC1), 152 append(L1,LC1,LD), 153 remove_duplicates(LD,LD1), 154 statistics(cputime,[_,CT1]), 155 CPUTime1 is CT1/1000, 156 statistics(walltime,[_,WT1]), 157 WallTime1 is WT1/1000, 158 print_mem, 159 build_ground_lpad(LD1,0,CL), 160 convert_to_clpbn(CL,GL,LV,P,GLC), 161 statistics(cputime,[_,CT2]), 162 CPUTime2 is CT2/1000, 163 statistics(walltime,[_,WT2]), 164 WallTime2 is WT2/1000 165 ; 166 P=0.0, 167 print_mem, 168 format(user_error,"Porb 0~n",[]), 169 statistics(cputime,[_,CT1]), 170 CPUTime1 is CT1/1000, 171 statistics(walltime,[_,WT1]), 172 WallTime1 is WT1/1000, 173 CPUTime2 =0.0, 174 WallTime2 =0.0 175 ) 176 ; 177 P=undef, 178 print_mem, 179 statistics(cputime,[_,CT1]), 180 CPUTime1 is CT1/1000, 181 statistics(walltime,[_,WT1]), 182 WallTime1 is WT1/1000, 183 CPUTime2 =0.0, 184 WallTime2 =0.0, 185 print_mem, 186 format(user_error,"Undef~n",[]) 187 ), 188 format(user_error,"Memory after inference~n",[]), 189 print_mem. 190 191remove_head([],[]). 192 193remove_head([(_N,R,S)|T],[(R,S)|T1]):- 194 remove_head(T,T1). 195 196append_all([],L,L):-!. 197 198append_all([LIntH|IntT],IntIn,IntOut):- 199 append(IntIn,LIntH,Int1), 200 append_all(IntT,Int1,IntOut). 201 202process_goals([],[],[]). 203 204process_goals([H|T],[HG|TG],[HV|TV]):- 205 H=..[F,HV|Rest], 206 HG=..[F|Rest], 207 process_goals(T,TG,TV). 208 209build_ground_lpad([],_N,[]). 210 211build_ground_lpad([(R,S)|T],N,[(N1,Head1,Body1)|T1]):- 212 rule(R,S,_,Head,Body), 213 N1 is N+1, 214 merge_identical(Head,Head1), 215 remove_built_ins(Body,Body1), 216 build_ground_lpad(T,N1,T1). 217 218remove_built_ins([],[]):-!. 219 220remove_built_ins([\+H|T],T1):- 221 builtin(H),!, 222 remove_built_ins(T,T1). 223 224remove_built_ins([H|T],T1):- 225 builtin(H),!, 226 remove_built_ins(T,T1). 227 228remove_built_ins([H|T],[H|T1]):- 229 remove_built_ins(T,T1). 230 231merge_identical([],[]):-!. 232 233merge_identical([A:P|T],[A:P1|Head]):- 234 find_identical(A,P,T,P1,T1), 235 merge_identical(T1,Head). 236 237find_identical(_A,P,[],P,[]):-!. 238 239find_identical(A,P0,[A:P|T],P1,T1):-!, 240 P2 is P0+P, 241 find_identical(A,P2,T,P1,T1). 242 243find_identical(A,P0,[H:P|T],P1,[H:P|T1]):- 244 find_identical(A,P0,T,P1,T1). 245 246convert_to_clpbn(CL,GL,LV,P,GLC):- 247 find_ground_atoms(CL,[],GAD), 248 remove_duplicates(GAD,GANull), 249 delete(GANull,'',GA), 250 atom_vars(GA,[],AV,AVL), 251 choice_vars(CL,[],CV,CVL), 252 add_rule_tables(CL,CVL,AV), 253 add_atoms_tables(AVL,GA,CL,CV,AV), 254 add_ev(GLC,AV), 255 get_prob(GL,AV,AVL,CVL,P). 256 257add_ev([],_AV). 258 259add_ev([\+ H|T],AV):-!, 260 avl_lookup(H,V,AV), 261 clpbn:put_atts(V,evidence(0)), 262 add_ev(T,AV). 263 264add_ev([H|T],AV):- 265 avl_lookup(H,V,AV), 266 clpbn:put_atts(V,evidence(1)), 267 add_ev(T,AV). 268 269convert_to_clpbn(CL,GL,LV,P):- 270 find_ground_atoms(CL,[],GAD), 271 remove_duplicates(GAD,GANull), 272 delete(GANull,'',GA), 273 atom_vars(GA,[],AV,AVL), 274 choice_vars(CL,[],CV,CVL), 275 add_rule_tables(CL,CVL,AV), 276 add_atoms_tables(AVL,GA,CL,CV,AV), 277 get_prob(GL,AV,AVL,CVL,P). 278 279get_prob(GL,AV,AVL,CVL,P):- 280 build_table_conj(GL,Table), 281 find_atoms_body(GL,Atoms), 282 lookup_gvars(GL,AV,Parents,[],_Signs), 283 {G=goal with p([f,t],Table, Parents)}, 284 append(AVL,CVL,Vars), 285 append(Vars,[G],Vars1), 286 clpbn:clpbn_run_solver([G], Vars1,_State), 287 clpbn_display:get_atts(G, [posterior(Vs,Vals,[_P0,P],AllDiffs)]). 288 289lookup_gvars([],_AV,[],S,S). 290 291lookup_gvars([\+ H|T],AV,[HV|T1],Sign0,Sign2):- !, 292 avl_lookup(H,HV,AV), 293 clpbn:get_atts(HV, [key(K)]), 294 avl_insert(K,f,Sign0,Sign1), 295 lookup_gvars(T,AV,T1,Sign1,Sign2). 296 297lookup_gvars([H|T],AV,[HV|T1],Sign0,Sign2):- 298 avl_lookup(H,HV,AV), 299 clpbn:get_atts(HV, [key(K)]), 300 avl_insert(K,t,Sign0,Sign1), 301 lookup_gvars(T,AV,T1,Sign1,Sign2). 302 303add_atoms_tables([],[],_CL,_CV,_AV). 304 305add_atoms_tables([H|T],[HA|TA],CL,CV,AV):- 306 find_rules_with_atom(HA,CL,R), 307 parents(R,CV,Par), 308 build_table_atoms(HA,R,Table), 309 {H = HA with p([f,t],Table,Par)}, 310 add_atoms_tables(T,TA,CL,CV,AV). 311 312build_table_conj(R,Table):- 313 build_col_conj(R,t,f,[],Row1), 314 build_col_conj(R,t,t,Row1,Table). 315 316build_col_conj([],Tr,Final,Row0,Row1):- 317 (Tr=Final-> 318 append(Row0,[1.0],Row1) 319 ; 320 setting(cpt_zero,Zero), 321 append(Row0,[Zero],Row1) 322 ). 323 324build_col_conj([\+H|RP],Tr,Final,Row0,Row2):-!, 325 build_col_conj(RP,Tr,Final,Row0,Row1), 326 build_col_conj(RP,f,Final,Row1,Row2). 327 328build_col_conj([H|RP],Tr,Final,Row0,Row2):- 329 build_col_conj(RP,f,Final,Row0,Row1), 330 build_col_conj(RP,Tr,Final,Row1,Row2). 331 332build_table_atoms(H,R,Table):- 333 build_col(H,R,f,f,[],Row1), 334 build_col(H,R,t,f,Row1,Table). 335 336build_col(A,[],Tr,Found,Row0,Row1):- 337 (Tr=Found-> 338 append(Row0,[1.0],Row1) 339 ; 340 setting(cpt_zero,Zero), 341 append(Row0,[Zero],Row1) 342 ). 343 344build_col(A,[(N,H)|RP],Tr,Found,Row0,Row1):- 345 build_col_cycle(A,H,RP,Tr,Found,Row0,Row1). 346 347build_col_cycle(_A,[],_RP,_Tr,_Found,Row,Row). 348 349build_col_cycle(A,[A:P|T],RP,Tr,Found,Row0,Row2):-!, 350 build_col(A,RP,Tr,t,Row0,Row1), 351 build_col_cycle(A,T,RP,Tr,Found,Row1,Row2). 352 353build_col_cycle(A,[_|T],RP,Tr,Found,Row0,Row2):- 354 build_col(A,RP,Tr,Found,Row0,Row1), 355 build_col_cycle(A,T,RP,Tr,Found,Row1,Row2). 356 357parents([],_CV,[]). 358 359parents([(N,_H)|T],CV,[V|T1]):- 360 avl_lookup(N,V,CV), 361 parents(T,CV,T1). 362 363find_rules_with_atom(_A,[],[]). 364 365find_rules_with_atom(A,[(N,Head,Body)|T],[(N,Head)|R]):- 366 member(A:P,Head),!, 367 find_rules_with_atom(A,T,R). 368 369find_rules_with_atom(A,[_H|T],R):- 370 find_rules_with_atom(A,T,R). 371 372add_rule_tables([],[],_AV). 373 374add_rule_tables([(N,Head,Body)|T],[CV|TCV],AV):- 375 find_atoms_head(Head,Atoms,Probs), 376 get_parents(Body,AV,Par), 377 build_table(Probs,Body,Table), 378 {CV=ch(N) with p(Atoms,Table,Par)}, 379 add_rule_tables(T,TCV,AV). 380 381build_table([P],L,Row):-!, 382 build_col(L,t,P,1.0,Row). 383 384build_table([HP|TP],L,Tab):- 385 setting(cpt_zero,Zero), 386 build_col(L,t,HP,Zero,Row), 387 append(Row,Row1,Tab), 388 build_table(TP,L,Row1). 389 390build_col([],t,HP,_PNull,[HP]):-!. 391 392build_col([],f,_HP,PNull,[PNull]):-!. 393 394 395build_col([\+ H|T],Truth,P,PNull,Row):-!, 396 build_col(T,Truth,P,PNull,Row1), 397 append(Row1,Row2,Row), 398 build_col(T,f,P,PNull,Row2). 399 400build_col([_H|T],Truth,P,PNull,Row):- 401 build_col(T,f,P,PNull,Row1), 402 append(Row1,Row2,Row), 403 build_col(T,Truth,P,PNull,Row2). 404 405get_parents([],_AV,[]). 406 407get_parents([\+ H|T],AV,[V|T1]):-!, 408 avl_lookup(H,V,AV), 409 get_parents(T,AV,T1). 410 411get_parents([H|T],AV,[V|T1]):-!, 412 avl_lookup(H,V,AV), 413 get_parents(T,AV,T1). 414 415choice_vars([],Tr,Tr,[]). 416 417choice_vars([(N,_H,_B)|T],Tr0,Tr1,[NV|T1]):- 418 avl_insert(N,NV,Tr0,Tr2), 419 choice_vars(T,Tr2,Tr1,T1). 420 421atom_vars([],Tr,Tr,[]). 422 423atom_vars([H|T],Tr0,Tr1,[VH|VT]):- 424 avl_insert(H,VH,Tr0,Tr2), 425 atom_vars(T,Tr2,Tr1,VT). 426 427find_ground_atoms([],GA,GA). 428 429find_ground_atoms([(_N,Head,Body)|T],GA0,GA1):- 430 find_atoms_head(Head,AtH,_P), 431 append(GA0,AtH,GA2), 432 find_atoms_body(Body,AtB), 433 append(GA2,AtB,GA3), 434 find_ground_atoms(T,GA3,GA1). 435 436find_atoms_body([],[]). 437 438find_atoms_body([\+H|T],[H|T1]):-!, 439 find_atoms_body(T,T1). 440 441find_atoms_body([H|T],[H|T1]):- 442 find_atoms_body(T,T1). 443 444 445find_atoms_head([],[],[]). 446 447find_atoms_head([H:P|T],[H|TA],[P|TP]):- 448 find_atoms_head(T,TA,TP). 449 450print_mem:- 451 statistics(global_stack,[GS,GSF]), 452 statistics(local_stack,[LS,LSF]), 453 statistics(heap,[HP,HPF]), 454 statistics(trail,[TU,TF]), 455 format(user_error,"~nGloabal stack used ~d execution stack free: ~d~n",[GS,GSF]), 456 format(user_error,"Local stack used ~d execution stack free: ~d~n",[LS,LSF]), 457 format(user_error,"Heap used ~d heap free: ~d~n",[HP,HPF]), 458 format(user_error,"Trail used ~d Trail free: ~d~n",[TU,TF]). 459 460find_deriv(GoalsList,Deriv):- 461 solve(GoalsList,[],DerivDup), 462 remove_duplicates(DerivDup,Deriv). 463/* duplicate can appear in the C set because two different unistantiated clauses may become the 464same clause when instantiated */ 465 466 467 468/* solve(GoalsList,CIn,COut) takes a list of goals and an input C set 469and returns an output C set 470The C set is a list of triple (N,R,S) where 471- N is the index of the head atom used, starting from 0 472- R is the index of the non ground rule used, starting from 1 473- S is the substitution of rule R, in the form of a list whose elements 474 are of the form 'VarName'=value 475*/ 476solve([],C,C):-!. 477 478solve([bagof(V,EV^G,L)|T],CIn,COut):-!, 479 list2and(GL,G), 480 bagof((V,C),EV^solve(GL,CIn,C),LD), 481 length(LD,N), 482 build_initial_graph(N,GrIn), 483 build_graph(LD,0,GrIn,Gr), 484 clique(Gr,Clique), 485 build_Cset(LD,Clique,L,[],C1), 486 remove_duplicates_eq(C1,C2), 487 solve(T,C2,COut). 488 489solve([bagof(V,G,L)|T],CIn,COut):-!, 490 list2and(GL,G), 491 bagof((V,C),solve(GL,CIn,C),LD), 492 length(LD,N), 493 build_initial_graph(N,GrIn), 494 build_graph(LD,0,GrIn,Gr), 495 clique(Gr,Clique), 496 build_Cset(LD,Clique,L,[],C1), 497 remove_duplicates_eq(C1,C2), 498 solve(T,C2,COut). 499 500 501solve([setof(V,EV^G,L)|T],CIn,COut):-!, 502 list2and(GL,G), 503 setof((V,C),EV^solve(GL,CIn,C),LD), 504 length(LD,N), 505 build_initial_graph(N,GrIn), 506 build_graph(LD,0,GrIn,Gr), 507 clique(Gr,Clique), 508 build_Cset(LD,Clique,L1,[],C1), 509 remove_duplicates(L1,L), 510 solve(T,C1,COut). 511 512solve([setof(V,G,L)|T],CIn,COut):-!, 513 list2and(GL,G), 514 setof((V,C),solve(GL,CIn,C),LD), 515 length(LD,N), 516 build_initial_graph(N,GrIn), 517 build_graph(LD,0,GrIn,Gr), 518 clique(Gr,Clique), 519 build_Cset(LD,Clique,L1,[],C1), 520 remove_duplicates(L1,L), 521 solve(T,C1,COut). 522 523solve([\+ H |T],CIn,COut):-!, 524 list2and(HL,H), 525 (setof(D,find_deriv(HL,D),LDup)-> 526 rem_dup_lists(LDup,[],L), 527 choose_clauses(CIn,L,C1), 528 solve(T,C1,COut) 529 ; 530 solve(T,CIn,COut) 531 ). 532 533solve([H|T],CIn,COut):- 534 builtin(H),!, 535 call(H), 536 solve(T,CIn,COut). 537 538solve([H|T],CIn,COut):- 539 def_rule(H,B), 540 append(B,T,NG), 541 solve(NG,CIn,COut). 542 543solve([H|T],CIn,COut):- 544 find_rule(H,(R,S,N),B,CIn), 545 solve_pres(R,S,N,B,T,CIn,COut). 546 547solve_pres(R,S,N,B,T,CIn,COut):- 548 member_eq((N,R,S),CIn),!, 549 append(B,T,NG), 550 solve(NG,CIn,COut). 551 552solve_pres(R,S,N,B,T,CIn,COut):- 553 append(CIn,[(N,R,S)],C1), 554 append(B,T,NG), 555 solve(NG,C1,COut). 556 557build_initial_graph(N,G):- 558 listN(0,N,Vert), 559 add_vertices([],Vert,G). 560 561 562build_graph([],_N,G,G). 563 564build_graph([(_V,C)|T],N,GIn,GOut):- 565 N1 is N+1, 566 compatible(C,T,N,N1,GIn,G1), 567 build_graph(T,N1,G1,GOut). 568 569compatible(_C,[],_N,_N1,G,G). 570 571compatible(C,[(_V,H)|T],N,N1,GIn,GOut):- 572 (compatible(C,H)-> 573 add_edges(GIn,[N-N1,N1-N],G1) 574 ; 575 G1=GIn 576 ), 577 N2 is N1 +1, 578 compatible(C,T,N,N2,G1,GOut). 579 580compatible([],_C). 581 582compatible([(N,R,S)|T],C):- 583 not_present_with_a_different_head(N,R,S,C), 584 compatible(T,C). 585 586not_present_with_a_different_head(_N,_R,_S,[]). 587 588not_present_with_a_different_head(N,R,S,[(N,R,S)|T]):-!, 589 not_present_with_a_different_head(N,R,S,T). 590 591not_present_with_a_different_head(N,R,S,[(_N1,R,S1)|T]):- 592 S\=S1,!, 593 not_present_with_a_different_head(N,R,S,T). 594 595not_present_with_a_different_head(N,R,S,[(_N1,R1,_S1)|T]):- 596 R\=R1, 597 not_present_with_a_different_head(N,R,S,T). 598 599 600 601build_Cset(_LD,[],[],C,C). 602 603build_Cset(LD,[H|T],[V|L],CIn,COut):- 604 nth0(H,LD,(V,C)), 605 append(C,CIn,C1), 606 build_Cset(LD,T,L,C1,COut). 607 608 609/* find_rule(G,(R,S,N),Body,C) takes a goal G and the current C set and 610returns the index R of a disjunctive rule resolving with G together with 611the index N of the resolving head, the substitution S and the Body of the 612rule */ 613find_rule(H,(R,S,N),Body,C):- 614 rule(R,S,_,Head,Body), 615 member_head(H,Head,0,N), 616 not_already_present_with_a_different_head(N,R,S,C). 617 618find_rule(H,(R,S,Number),Body,C):- 619 rule(R,S,_,uniform(H:1/_Num,_P,Number),Body), 620 not_already_present_with_a_different_head(Number,R,S,C). 621 622not_already_present_with_a_different_head(_N,_R,_S,[]). 623 624not_already_present_with_a_different_head(N,R,S,[(N1,R,S1)|T]):- 625 not_different(N,N1,S,S1),!, 626 not_already_present_with_a_different_head(N,R,S,T). 627 628not_already_present_with_a_different_head(N,R,S,[(_N1,R1,_S1)|T]):- 629 R\==R1, 630 not_already_present_with_a_different_head(N,R,S,T). 631 632not_different(_N,_N1,S,S1):- 633 S\=S1,!. 634 635not_different(N,N1,S,S1):- 636 N\=N1,!, 637 dif(S,S1). 638 639not_different(N,N,S,S). 640 641 642member_head(H,[(H:_P)|_T],N,N). 643 644member_head(H,[(_H:_P)|T],NIn,NOut):- 645 N1 is NIn+1, 646 member_head(H,T,N1,NOut). 647 648/* choose_clauses(CIn,LC,COut) takes as input the current C set and 649the set of C sets for a negative goal and returns a new C set that 650excludes all the derivations for the negative goals */ 651choose_clauses(C,[],C). 652 653choose_clauses(CIn,[D|T],COut):- 654 member((N,R,S),D), 655 already_present_with_a_different_head(N,R,S,CIn),!, 656 choose_a_head(N,R,S,CIn,C1), 657 choose_clauses(C1,T,COut). 658 659 660choose_clauses(CIn,[D|T],COut):- 661 member((N,R,S),D), 662 new_head(N,R,S,N1), 663 \+ already_present(N1,R,S,CIn), 664 impose_dif_cons(R,S,CIn), 665 choose_clauses([(N1,R,S)|CIn],T,COut). 666 667impose_dif_cons(_R,_S,[]):-!. 668 669impose_dif_cons(R,S,[(_NH,R,SH)|T]):-!, 670 dif(S,SH), 671 impose_dif_cons(R,S,T). 672 673impose_dif_cons(R,S,[_H|T]):- 674 impose_dif_cons(R,S,T). 675 676/* instantiation_present_with_the_same_head(N,R,S,C) 677takes rule R with substitution S and selected head N and a C set 678and asserts dif constraints for all the clauses in C of which RS 679is an instantitation and have the same head selected */ 680instantiation_present_with_the_same_head(_N,_R,_S,[]). 681 682instantiation_present_with_the_same_head(N,R,S,[(NH,R,SH)|T]):- 683 \+ \+ S=SH,!, 684 dif_head_or_subs(N,R,S,NH,SH,T). 685 686instantiation_present_with_the_same_head(N,R,S,[_H|T]):- 687 instantiation_present_with_the_same_head(N,R,S,T). 688 689dif_head_or_subs(N,R,S,NH,_SH,T):- 690 dif(N,NH), 691 instantiation_present_with_the_same_head(N,R,S,T). 692 693dif_head_or_subs(N,R,S,N,SH,T):- 694 dif(S,SH), 695 instantiation_present_with_the_same_head(N,R,S,T). 696 697/* case 1 of Select: a more general rule is present in C with 698a different head, instantiate it */ 699choose_a_head(N,R,S,[(NH,R,SH)|T],[(NH,R,SH)|T]):- 700 S=SH, 701 dif(N,NH). 702 703/* case 2 of Select: a more general rule is present in C with 704a different head, ensure that they do not generate the same 705ground clause */ 706choose_a_head(N,R,S,[(NH,R,SH)|T],[(NH,R,S),(NH,R,SH)|T]):- 707 \+ \+ S=SH, S\==SH, 708 dif(N,NH), 709 dif(S,SH). 710 711choose_a_head(N,R,S,[H|T],[H|T1]):- 712 choose_a_head(N,R,S,T,T1). 713 714/* select a head different from N for rule R with 715substitution S, return it in N1 */ 716new_head(N,R,S,N1):- 717 rule(R,S,Numbers,Head,_Body), 718 Head\=uniform(_,_,_),!, 719 nth0(N, Numbers, _Elem, Rest), 720 member(N1,Rest). 721 722new_head(N,R,S,N1):- 723 rule(R,S,Numbers,uniform(_A:1/Tot,_L,_Number),_Body), 724 listN(0,Tot,Numbers), 725 nth0(N, Numbers, _Elem, Rest), 726 member(N1,Rest). 727 728already_present_with_a_different_head(N,R,S,[(NH,R,SH)|_T]):- 729 \+ \+ S=SH,NH \= N. 730 731already_present_with_a_different_head(N,R,S,[_H|T]):- 732 already_present_with_a_different_head(N,R,S,T). 733 734 735/* checks that a rule R with head N and selection S is already 736present in C (or a generalization of it is in C) */ 737already_present(N,R,S,[(N,R,SH)|_T]):- 738 S=SH. 739 740already_present(N,R,S,[_H|T]):- 741 already_present(N,R,S,T). 742 743/* rem_dup_lists removes the C sets that are a superset of 744another C sets further on in the list of C sets */ 745/* rem_dup_lists removes the C sets that are a superset of 746another C sets further on in the list of C sets */ 747rem_dup_lists([],L,L). 748 749rem_dup_lists([H|T],L0,L):- 750 (member_subset(H,T);member_subset(H,L0)),!, 751 rem_dup_lists(T,L0,L). 752 753rem_dup_lists([H|T],L0,L):- 754 rem_dup_lists(T,[H|L0],L). 755 756member_subset(E,[H|_T]):- 757 subset_my(H,E),!. 758 759member_subset(E,[_H|T]):- 760 member_subset(E,T). 761 762 763 764/* predicates for building the formula to be converted into a BDD */ 765 766/* build_formula(LC,Formula,VarIn,VarOut) takes as input a set of C sets 767LC and a list of Variables VarIn and returns the formula and a new list 768of variables VarOut 769Formula is of the form [Term1,...,Termn] 770Termi is of the form [Factor1,...,Factorm] 771Factorj is of the form (Var,Value) where Var is the index of 772the multivalued variable Var and Value is the index of the value 773*/ 774build_formula([],[],Var,Var). 775 776build_formula([D|TD],[F|TF],VarIn,VarOut):- 777 build_term(D,F,VarIn,Var1), 778 build_formula(TD,TF,Var1,VarOut). 779 780build_term([],[],Var,Var). 781 782build_term([(N,R,S)|TC],[[NVar,N]|TF],VarIn,VarOut):- 783 (nth0_eq(0,NVar,VarIn,(R,S))-> 784 Var1=VarIn 785 ; 786 append(VarIn,[(R,S)],Var1), 787 length(VarIn,NVar) 788 ), 789 build_term(TC,TF,Var1,VarOut). 790 791/* nth0_eq(PosIn,PosOut,List,El) takes as input a List, 792an element El and an initial position PosIn and returns in PosOut 793the position in the List that contains an element exactly equal to El 794*/ 795nth0_eq(N,N,[H|_T],El):- 796 H==El,!. 797 798nth0_eq(NIn,NOut,[_H|T],El):- 799 N1 is NIn+1, 800 nth0_eq(N1,NOut,T,El). 801 802/* var2numbers converts a list of couples (Rule,Substitution) into a list 803of triples (N,NumberOfHeadsAtoms,ListOfProbabilities), where N is an integer 804starting from 0 */ 805var2numbers([],_N,[]). 806 807var2numbers([(R,S)|T],N,[[N,ValNumber,Probs]|TNV]):- 808 find_probs(R,S,Probs), 809 length(Probs,ValNumber), 810 N1 is N+1, 811 var2numbers(T,N1,TNV). 812 813find_probs(R,S,Probs):- 814 rule(R,S,_N,Head,_Body), 815 get_probs(Head,Probs). 816 817get_probs(uniform(_A:1/Num,_P,_Number),ListP):- 818 Prob is 1/Num, 819 list_el(Num,Prob,ListP). 820 821get_probs([],[]). 822 823get_probs([_H:P|T],[P1|T1]):- 824 P1 is P, 825 get_probs(T,T1). 826 827list_el(0,_P,[]):-!. 828 829list_el(N,P,[P|T]):- 830 N1 is N-1, 831 list_el(N1,P,T). 832 833/* end of predicates for building the formula to be converted into a BDD */list_el(0,_P,[]):-!. 834 835 836/* start of predicates for parsing an input file containing a program */ 837 838/* p(File) parses the file File.cpl. It can be called more than once without 839exiting yap */ 840p(File):- 841 parse(File). 842 843parse(File):- 844 atom_concat(File,'.cpl',FilePl), 845 open(FilePl,read,S), 846 read_clauses(S,C), 847 close(S), 848 retractall(rule(_,_,_,_,_)), 849 retractall(def_rule(_,_)), 850 process_clauses(C,1). 851 852process_clauses([(end_of_file,[])],_N). 853 854process_clauses([((H:-B),V)|T],N):- 855 H=uniform(A,P,L),!, 856 list2and(BL,B), 857 process_body(BL,V,V1), 858 remove_vars([P],V1,V2), 859 append(BL,[length(L,Tot),nth0(Number,L,P)],BL1), 860 append(V2,['Tot'=Tot],V3), 861 assertz(rule(N,V3,_NH,uniform(A:1/Tot,L,Number),BL1)), 862 N1 is N+1, 863 process_clauses(T,N1). 864 865process_clauses([((H:-B),V)|T],N):- 866 H=(_;_),!, 867 list2or(HL1,H), 868 process_head(HL1,HL), 869 list2and(BL,B), 870 process_body(BL,V,V1), 871 length(HL,LH), 872 listN(0,LH,NH), 873 assertz(rule(N,V1,NH,HL,BL)), 874 N1 is N+1, 875 process_clauses(T,N1). 876 877process_clauses([((H:-B),V)|T],N):- 878 H=(_:_),!, 879 list2or(HL1,H), 880 process_head(HL1,HL), 881 list2and(BL,B), 882 process_body(BL,V,V1), 883 length(HL,LH), 884 listN(0,LH,NH), 885 assertz(rule(N,V1,NH,HL,BL)), 886 N1 is N+1, 887 process_clauses(T,N1). 888 889process_clauses([((H:-B),V)|T],N):-!, 890 process_head([H:1.0],HL), 891 list2and(BL,B), 892 process_body(BL,V,V1), 893 length(HL,LH), 894 listN(0,LH,NH), 895 assertz(rule(N,V1,NH,HL,BL)), 896 N1 is N+1, 897 process_clauses(T,N1). 898 899process_clauses([(H,V)|T],N):- 900 H=(_;_),!, 901 list2or(HL1,H), 902 process_head(HL1,HL), 903 length(HL,LH), 904 listN(0,LH,NH), 905 assertz(rule(N,V,NH,HL,[])), 906 N1 is N+1, 907 process_clauses(T,N1). 908 909process_clauses([(H,V)|T],N):- 910 H=(_:_),!, 911 list2or(HL1,H), 912 process_head(HL1,HL), 913 length(HL,LH), 914 listN(0,LH,NH), 915 assertz(rule(N,V,NH,HL,[])), 916 N1 is N+1, 917 process_clauses(T,N1). 918 919process_clauses([(H,V)|T],N):- 920 process_head([H:1.0],HL), 921 length(HL,LH), 922 listN(0,LH,NH), 923 assertz(rule(N,V,NH,HL,[])), 924 N1 is N+1, 925 process_clauses(T,N1). 926 927/* if the annotation in the head are not ground, the null atom is not added 928and the eventual formulas are not evaluated */ 929 930process_head(HL,NHL):- 931 (ground_prob(HL)-> 932 process_head_ground(HL,0.0,NHL) 933 ; 934 NHL=HL 935 ). 936 937ground_prob([]). 938 939ground_prob([_H:PH|T]):- 940 ground(PH), 941 ground_prob(T). 942 943process_head_ground([H:PH],P,[H:PH1,'':PNull1]):-!, 944 PH1 is PH, 945 PNull is 1.0-P-PH1, 946 (PNull>=0.0-> 947 PNull1 =PNull 948 ; 949 PNull1=0.0 950 ). 951 952process_head_ground([H:PH|T],P,[H:PH1|NT]):- 953 PH1 is PH, 954 P1 is P+PH1, 955 process_head_ground(T,P1,NT). 956 957/* setof must have a goal of the form B^G where B is a term containing the existential variables */ 958process_body([],V,V). 959 960process_body([setof(A,B^_G,_L)|T],VIn,VOut):-!, 961 get_var(A,VA), 962 get_var(B,VB), 963 remove_vars(VA,VIn,V1), 964 remove_vars(VB,V1,V2), 965 process_body(T,V2,VOut). 966 967process_body([setof(A,_G,_L)|T],VIn,VOut):-!, 968 get_var(A,VA), 969 remove_vars(VA,VIn,V1), 970 process_body(T,V1,VOut). 971 972process_body([bagof(A,B^_G,_L)|T],VIn,VOut):-!, 973 get_var(A,VA), 974 get_var(B,VB), 975 remove_vars(VA,VIn,V1), 976 remove_vars(VB,V1,V2), 977 process_body(T,V2,VOut). 978 979process_body([bagof(A,_G,_L)|T],VIn,VOut):-!, 980 get_var(A,VA), 981 remove_vars(VA,VIn,V1), 982 process_body(T,V1,VOut). 983 984process_body([_H|T],VIn,VOut):-!, 985 process_body(T,VIn,VOut). 986 987get_var_list([],[]). 988 989get_var_list([H|T],[H|T1]):- 990 var(H),!, 991 get_var_list(T,T1). 992 993get_var_list([H|T],VarOut):-!, 994 get_var(H,Var), 995 append(Var,T1,VarOut), 996 get_var_list(T,T1). 997 998get_var(A,[A]):- 999 var(A),!. 1000 1001get_var(A,V):- 1002 A=..[_F|Args], 1003 get_var_list(Args,V). 1004 1005remove_vars([],V,V). 1006 1007remove_vars([H|T],VIn,VOut):- 1008 delete_var(H,VIn,V1), 1009 remove_vars(T,V1,VOut). 1010 1011delete_var(_H,[],[]). 1012 1013delete_var(V,[VN=Var|T],[VN=Var|T1]):- 1014 V\==Var,!, 1015 delete_var(V,T,T1). 1016 1017delete_var(_V,[_H|T],T). 1018 1019/* predicates for reading in the program clauses */ 1020read_clauses(S,Clauses):- 1021 (setting(ground_body,true)-> 1022 read_clauses_ground_body(S,Clauses) 1023 ; 1024 read_clauses_exist_body(S,Clauses) 1025 ). 1026 1027 1028read_clauses_ground_body(S,[(Cl,V)|Out]):- 1029 read_term(S,Cl,[variable_names(V)]), 1030 (Cl=end_of_file-> 1031 Out=[] 1032 ; 1033 read_clauses_ground_body(S,Out) 1034 ). 1035 1036 1037read_clauses_exist_body(S,[(Cl,V)|Out]):- 1038 read_term(S,Cl,[variable_names(VN)]), 1039 extract_vars_cl(Cl,VN,V), 1040 (Cl=end_of_file-> 1041 Out=[] 1042 ; 1043 read_clauses_exist_body(S,Out) 1044 ). 1045 1046 1047extract_vars_cl(end_of_file,[]). 1048 1049extract_vars_cl(Cl,VN,Couples):- 1050 (Cl=(H:-_B)-> 1051 true 1052 ; 1053 H=Cl 1054 ), 1055 extract_vars(H,[],V), 1056 pair(VN,V,Couples). 1057 1058 1059pair(_VN,[],[]). 1060 1061pair([VN= _V|TVN],[V|TV],[VN=V|T]):- 1062 pair(TVN,TV,T). 1063 1064 1065extract_vars(Var,V0,V):- 1066 var(Var),!, 1067 (member_eq(Var,V0)-> 1068 V=V0 1069 ; 1070 append(V0,[Var],V) 1071 ). 1072 1073extract_vars(Term,V0,V):- 1074 Term=..[_F|Args], 1075 extract_vars_list(Args,V0,V). 1076 1077 1078extract_vars_list([],V,V). 1079 1080extract_vars_list([Term|T],V0,V):- 1081 extract_vars(Term,V0,V1), 1082 extract_vars_list(T,V1,V). 1083 1084 1085listN(N,N,[]):-!. 1086 1087listN(NIn,N,[NIn|T]):- 1088 N1 is NIn+1, 1089 listN(N1,N,T). 1090/* end of predicates for parsing an input file containing a program */ 1091 1092/* start of utility predicates */ 1093list2or([X],X):- 1094 X\=;(_,_),!. 1095 1096list2or([H|T],(H ; Ta)):-!, 1097 list2or(T,Ta). 1098 1099list2and([X],X):- 1100 X\=(_,_),!. 1101 1102list2and([H|T],(H,Ta)):-!, 1103 list2and(T,Ta). 1104 1105member_eq(A,[H|_T]):- 1106 A==H,!. 1107 1108member_eq(A,[_H|T]):- 1109 member_eq(A,T). 1110 1111subset_my([],_). 1112 1113subset_my([H|T],L):- 1114 member_eq(H,L), 1115 subset_my(T,L). 1116 1117remove_duplicates_eq([],[]). 1118 1119remove_duplicates_eq([H|T],T1):- 1120 member_eq(H,T),!, 1121 remove_duplicates_eq(T,T1). 1122 1123remove_duplicates_eq([H|T],[H|T1]):- 1124 remove_duplicates_eq(T,T1). 1125 1126builtin(_A is _B). 1127builtin(_A > _B). 1128builtin(_A < _B). 1129builtin(_A >= _B). 1130builtin(_A =< _B). 1131builtin(_A =:= _B). 1132builtin(_A =\= _B). 1133builtin(true). 1134builtin(false). 1135builtin(_A = _B). 1136builtin(_A==_B). 1137builtin(_A\=_B). 1138builtin(_A\==_B). 1139builtin(length(_L,_N)). 1140builtin(member(_El,_L)). 1141builtin(average(_L,_Av)). 1142builtin(max_list(_L,_Max)). 1143builtin(min_list(_L,_Max)). 1144builtin(nth0(_,_,_)). 1145builtin(nth(_,_,_)). 1146average(L,Av):- 1147 sum_list(L,Sum), 1148 length(L,N), 1149 Av is Sum/N. 1150 1151clique(Graph,Clique):- 1152 vertices(Graph,Candidates), 1153 extend_cycle(Graph,Candidates,[],[],Clique). 1154 1155extend_cycle(G,[H|T],Not,CS,CSOut):- 1156 neighbours(H, G, Neigh), 1157 intersection(Neigh,T,NewCand), 1158 intersection(Neigh,Not,NewNot), 1159 extend(G,NewCand,NewNot,[H|CS],CSOut). 1160 1161extend_cycle(G,[H|T],Not,CS,CSOut):- 1162 extend_cycle(G,T,[H|Not],CS,CSOut). 1163 1164extend(_G,[],[],CompSub,CompSub):-!. 1165 1166extend(G,Cand,Not,CS,CSOut):- 1167 extend_cycle(G,Cand,Not,CS,CSOut). 1168 1169/* set(Par,Value) can be used to set the value of a parameter */ 1170set(Parameter,Value):- 1171 retract(setting(Parameter,_)), 1172 assert(setting(Parameter,Value)). 1173 1174/* end of utility predicates */ 1175