/* LLPAD version 3 by Fabrizio Riguzzi differences with respect to version 2: * different bias: more than one head_bias and determination * learns ground clauses and then generalizes them differences with respect to version 1: * Aleph language bias * beam search of clauses */ :-use_module(library(lists)),use_module(library(clpr)). %:-set_prolog_flag(language,iso). :-unknown(_S,fail). :- op(560, xfy, or). :-consult(ref_op). i(File,Variables,Program):- generate_file_names(File,FileKB,FileOut,FileL), % title(File,user_output), statistics(runtime,[_,_]), load_models(FileKB,ModulesList), [FileL], assert(definite_rule_number(1)), assert(rule_number(1)), induce(ModulesList,Variables,Program), statistics(runtime,[_,T]), open(FileOut,write,Stream), % title(File,Stream), % title(File,user_output), T1 is T /1000, format(Stream,"Execution time ~f seconds. Generated rules~N",[T1]), format("Execution time ~f seconds. Generated rules~N",[T1]), findall(def_rule(N,Info,R),def_rule(N,Info,R),DefRules), print_list(DefRules,Stream), print_list(DefRules,user_output), findall(rule(N,Info,R),rule(N,Info,R),Rules), print_list(Rules,Stream), print_list(Rules,user_output), findall(rule(N1,R1),rule(N1,_Info,R1),Rules1), print_list(Rules1,Stream), nl(Stream), nl, print_list(Program,Stream), print_list(Program,user_output), close(Stream). induce(ModulesList,Variables,Program):- findall(ALH,head_bias(ALH),L), search_clauses(ModulesList,L), solve(ModulesList,Variables), generalize(ModulesList,Variables,Program). generalize(ModulesList,Variables,P1):- generate_program(Variables,1,[],P), generalize_program(ModulesList,P,P1). generalize_program(ML,P,P1):- gen_loop(ML,P,P1). gen_loop(ML,PIn,POut):- while1(ML,Found,C1,C2,LGG,PIn), (Found=true-> delete(PIn,C1,P), delete(P,C2,P1), append(P1,[LGG],P2), gen_loop(ML,P2,POut) ; POut=PIn ). while1(_ML,false,_C1,_C2,_LGG,[_C]):-!. while1(ML,Found,C1,C2,LGG,[C|Rest]):- (while2(ML,C,Rest,C21,LGG1)-> Found=true, C1=C, C2=C21, LGG=LGG1 ; while1(ML,Found,C1,C2,LGG,Rest) ). while2(ML,C1,[C2|Rest],C21,LGG):- (compute_lgg(ML,C1,C2,LGG1)-> LGG=LGG1, C21=C2 ; while2(ML,C1,Rest,C21,LGG) ). compute_lgg(ML,C1,C2,(H:-B)):- lgg_clauses(C1,C2,(H:-B)), process_example_list(ML,ExL,_), remove_prob_to_and(H,(A,Rest)), test_body(ExL,(A:-B),0,NBT,[],ETL), test_head(ETL,((A,Rest):-B),0,NBT,[],_ETHL). remove_prob_to_and(A:_P,A):-!. remove_prob_to_and(A:_P or Rest,(A,Rest1)):- remove_prob_to_and(Rest,Rest1). generate_program([],_N,P,P):-!. generate_program([H|T],N,PIn,[C|POut]):- H>0.9,!, rule(N,_I,C), N1 is N+1, generate_program(T,N1,PIn,POut). generate_program([_H|T],N,PIn,POut):- N1 is N+1, generate_program(T,N1,PIn,POut). search_clauses(_ModulesList,[]):-!. search_clauses(ModulesList,[ALH|Rest]):- search_definite_cl(ModulesList,ALH), ALH=[Head|_Rest], search_bodies(ModulesList,Head,ALH), search_clauses(ModulesList,Rest). search_definite_cl(_ExampleList,[]):-!. search_definite_cl(ExampleList,[Atom|T]):- search_definite(Atom,ExampleList), search_definite_cl(ExampleList,T). search_definite(Head,ExampleList):- process_example_list(ExampleList,ProcessedEL,Head), test_head(ProcessedEL,(Head:-true),0,NHT,[],ETHL), length(ExampleList,L), (L=NHT-> % clause is true in all examples % add the clause to the theory retract(definite_rule_number(N)), format("~p~N",[def_rule(N,[pos(NHT),ETHL],(Head:-true))]), assertz(def_rule(N,[pos(NHT),ETHL],(Head:-true))), N1 is N+1, assert(definite_rule_number(N1)) ; definite_cycle([((Head:-true),ProcessedEL,_)],1) ). process_example_list([],[],_Head):-!. process_example_list([(Ex,_LH)|RestEx],[(Ex,[Head])|RestProcessedEL],Head):- process_example_list(RestEx,RestProcessedEL,Head). definite_cycle([],_N):-!. definite_cycle(_Beam,N):- setting(nodes,Nodes), N>Nodes,!. definite_cycle([((Head:-Body),ExampleList,_)|RestBeam],I):- findall(C,auto_refine((Head:-Body),C),Refinements), process_refinements(Refinements,ExampleList,RestBeam,NewBeam), I1 is I+1, definite_cycle(NewBeam,I1). process_refinements([],_Ex,B,B):-!. process_refinements([(Head:-Body)|Rest],ExL,BIn,BOut):- test_body(ExL,(Head:-Body),0,NBT,[],ETL), (NBT>0-> % clause not trivially true test_head(ETL,(Head:-Body),0,NHT,[],ETHL), (NBT=NHT-> % clause is true in all the examples % add the clause to the theory retract(definite_rule_number(N)), format("~p~N",[def_rule(N,[pos(NHT),ETHL],(Head:-Body))]), assertz(def_rule(N,[pos(NHT),ETHL],(Head:-Body))), N1 is N+1, assert(definite_rule_number(N1)), B1=BIn ; % the clause is false in some interpretations, (NHT>0-> % the heads is true in at least one of the interpretations % where the body is true % add the clause to the beam setting(d,BeamSize), insert_in_order(((Head:-Body),ETL,NHT),BeamSize,BIn,B1) ; % do nothing true ) ) ; B1 = BIn ), process_refinements(Rest,ExL,B1,BOut). insert_in_order(C,BeamSize,[],[C]):- BeamSize>0,!. insert_in_order(_NewClauseItem,0,Beam,Beam):-!. insert_in_order((C,ETL,NHT),BeamSize, [(C1,ETL1,NHT1)|RestBeamIn], BeamOut):- NHT>NHT1,!, % bigger heuristic, insert here NewBeam=[ (C,ETL,NHT),(C1,ETL1,NHT1)|RestBeamIn], length(NewBeam,L), (L>BeamSize-> nth(L,NewBeam,_Last,BeamOut) ; BeamOut=NewBeam ). insert_in_order((C,ETL,NHT),BeamSize, [(C1,ETL1,NHT1)|RestBeamIn], [(C1,ETL1,NHT1)|RestBeamOut]):- BeamSize1 is BeamSize -1, insert_in_order((C,ETL,NHT),BeamSize1,RestBeamIn, RestBeamOut). search_bodies(ExampleList,Head,ALH):- process_example_list(ExampleList,ProcessedEL,Head), length(ProcessedEL,L), bodies_cycle([((Head:-true),ProcessedEL,L)],1,ALH). bodies_cycle([],_N,_ALH):-!. bodies_cycle(_Beam,N,_ALH):- setting(nodes,Nodes), N>Nodes,!. bodies_cycle([((Head:-Body),ExampleList,NBT)|RestBeam],I,ALH):- (ExampleList=[]-> I1 is I+1, bodies_cycle(RestBeam,I1,ALH) ; search_heads((Head:-Body),ExampleList,NBT,ALH), findall(C,auto_refine((Head:-Body),C),Refinements), process_body_refinements(Refinements,ExampleList,RestBeam,NewBeam), I1 is I+1, bodies_cycle(NewBeam,I1,ALH) ). process_body_refinements([],_Ex,B,B):-!. process_body_refinements([(Head:-Body)|Rest],ExL,BIn,BOut):- test_body(ExL,(Head:-Body),0,NBT,[],ETL), setting(d,BeamSize), insert_in_order(((Head:-Body),ETL,NBT),BeamSize,BIn,B1), process_body_refinements(Rest,ExL,B1,BOut). search_heads((_Head:-Body),ExampleList,NBT,AA):- heads_cycle([((AA,AA),Body,ExampleList,NBT)]). heads_cycle([]):-!. heads_cycle([((Head,HeadList),Body,ExampleList,NBT)|RestBeam]):- list2and(BodyList,Body), list2and(Head,HeadAnd), intersection1(Head,BodyList,Int), (Int=[]-> % not a tautology test_head(ExampleList,(HeadAnd:-Body),0,NHT,[],_ETL), (NHT=NBT-> % the clause is true in all interpretations (exclusive_disjuncts_no_empty((HeadAnd:-Body),ExampleList,ListListModHT)-> % solution found compute_probabilities((HeadAnd:-Body),NewClause,ListListModHT), retract(rule_number(N)), format("~p~N",[rule(N,[pos(NHT),ListListModHT],NewClause)]), assertz(rule(N,[pos(NHT),ListListModHT],NewClause)), N1 is N+1, assert(rule_number(N1)), NewBeam=RestBeam ; % refine heaad (remove disjuncts) length(Head,N), (N>2-> findall((NewState,Body,ExampleList,NBT), refine_head((Head,HeadList),NewState),Refinements), append(RestBeam,Refinements,NewBeam) ; NewBeam=RestBeam ) ) ; % the clause is false in some interpretations % do not consider heads with a subset of the disjuncts NewBeam=RestBeam ) ; % the clause is a tautology, it has to be refined length(Head,N), (N>2-> findall((NewState,Body,ExampleList,NBT), refine_head((Head,HeadList),NewState),Refinements), append(RestBeam,Refinements,NewBeam) ; NewBeam=RestBeam ) ), heads_cycle(NewBeam). solve(ModuleList,Variables):- findall(rule(N,Info,R),rule(N,Info,R),Rules), rule_number(N), N1 is N-1, length(Variables,N1), % domain(Variables,0,1), impose_unary_constraints(Variables), find_int_body_true(Rules,[],Ints,[],Heads), impose_mutual_exclusion_constraints(Variables,Ints,Heads,Rules), impose_interpretation_constraints(ModuleList,Variables,Rules), % bb_inf(Variables,1,ListSol). labelling(Variables). labelling([]):-!. labelling([H|T]):- {H=<0}, labelling(T). labelling([H|T]):- {H>=1}, labelling(T). find_int_body_true([],Interp,Interp,Heads,Heads):-!. find_int_body_true([rule(_Number,[_Pos,ML],(Head:-_Body))|RulesT], IntIn,[IntList|IntOut],HeadsIn,[HeadsList|HeadsOut]):- append_all(ML,[],IntList), ann_head_to_list(Head,HeadsList), find_int_body_true(RulesT,IntIn,IntOut,HeadsIn,HeadsOut). ann_head_to_list((H:_P),[H]):-!. ann_head_to_list((H:_P) or Rest,[H|RestHeads]):- ann_head_to_list(Rest,RestHeads). append_all([],L,L):-!. append_all([LIntH|IntT],IntIn,IntOut):- append(IntIn,LIntH,Int1), append_all(IntT,Int1,IntOut). impose_mutual_exclusion_constraints([],[],[],[]):-!. impose_mutual_exclusion_constraints([VH|VT],[IH|IT],[HH|HT],[RH|RT]):- mutual_exclusion(VH,VT,IH,IT,HH,HT,RH), impose_mutual_exclusion_constraints(VT,IT,HT,RT). mutual_exclusion(_V,[],_I,[],_H,[],_R):-!. mutual_exclusion(V,[VH|VT],I,[IH|IT],H,[HH|HT],R):- intersection1(H,HH,IntHead), (IntHead=[]-> % no common head true ; % one or more common heads (intersection(I,IH,[])-> % bodies mutually exclusive true ; % bodies non-mutually exclusive {V+VH=<1} ) ), mutual_exclusion(V,VT,I,IT,H,HT,R). impose_unary_constraints([]):-!. impose_unary_constraints([H|T]):- {H >=0}, {H=<1}, impose_unary_constraints(T). impose_interpretation_constraints([],_Variables,_Rules):-!. impose_interpretation_constraints([(H,_)|T],Variables,Rules):- H:prob(P), LogP is log(P), build_expression(LogP,H,Variables,Rules,Expr), {Expr = 1}, impose_interpretation_constraints(T,Variables,Rules). build_expression(_LogP,_Module,[],[],0):-!. build_expression(LogP,Module,[Variable|RestVar],[rule(_N,[_Pos,ML],(Head:-_Body))|RestRules], ExprOut):- (member_list_list((Module,HeadLit),ML)-> extract_head_prob(HeadLit,Head,ProbHead), LogProbHead is log(ProbHead)/LogP, ExprOut=Variable*LogProbHead + Expr ; ExprOut=Expr ), build_expression(LogP,Module,RestVar,RestRules,Expr). member_list_list((Module,HeadLit),[HML|_TML]):- member((Module,HeadLit),HML),!. member_list_list((Module,HeadLit),[_HML|TML]):- member_list_list((Module,HeadLit),TML). extract_head_prob(HeadLit,(HeadLit:ProbHead),ProbHead):-!. extract_head_prob(HeadLit,(HeadLit:ProbHead or _Rest) ,ProbHead):-!. extract_head_prob(HeadLit,(_HP or Rest),ProbHead):- extract_head_prob(HeadLit,Rest,ProbHead). compute_probabilities((Head:-Body),(NewHead:-Body),ListListModHT):- compute_prob(ListListModHT,[],ListProb,0,Total), insert_prob(Head,NewHead,ListProb,Total). compute_prob([],L,L,T,T):-!. compute_prob([H|T],LIn,[SubTot|LOut],TIn,TOut):- sum_prob(H,0,SubTot), Tot is TIn+SubTot, compute_prob(T,LIn,LOut,Tot,TOut). sum_prob([],T,T). sum_prob([(H,_)|T],SubTotIn,SubTotOut):- H:prob(P), SubTot is SubTotIn+P, sum_prob(T,SubTot,SubTotOut). insert_prob(Lit,Lit:PD,[P],Total):-!, PD is P/Total. insert_prob((Lit,Rest),(Lit:PD or Rest1),[P|T],Total):- PD is P/Total, insert_prob(Rest,Rest1,T,Total). exclusive_disjuncts_no_empty((H:-_Body),ML,MHL):- find_sets_of_modules(H,ML,MHL), no_intersections(MHL). find_sets_of_modules(H,ML,[MHT]):- H\=(_,_),!, test_disjunct(H,ML,MHT), MHT\=[]. find_sets_of_modules((H,Rest),ML,[MHT|MHL]):- test_disjunct(H,ML,MHT), MHT\=[], find_sets_of_modules(Rest,ML,MHL). no_intersections(MHL):- findall(Int, (delete1(MHL, Element, Rest), member(Element1,Rest),intersection(Element,Element1,Int),Int\=[]), []). test_disjunct(H,ML,MHT):- test_single_head(ML,(H:-true),0,_MHTN,[],MHT). test_single_head([],(_Head:-_Body),NHT,NHT,MLHT,MLHT):-!. test_single_head([(Module,LS)|RestM],(Head:-Body),NHTIn,NHTOut,MLHTIn,MLHTOut):- (test_head_subst(Module,LS,(Head:-Body))-> % clause is true NHT is NHTIn +1, MLHTOut=[(Module,Head)|MLHT], test_single_head(RestM,(Head:-Body),NHT,NHTOut,MLHTIn,MLHT) ; % clause is false test_single_head(RestM,(Head:-Body),NHTIn,NHTOut,MLHTIn,MLHTOut) ). test_head([],(_Head:-_Body),NHT,NHT,MLHT,MLHT):-!. test_head([(Module,LS)|RestM],(Head:-Body),NHTIn,NHTOut,MLHTIn,MLHTOut):- (test_head_subst(Module,LS,(Head:-Body))-> % clause is true NHT is NHTIn +1, MLHTOut=[Module|MLHT], test_head(RestM,(Head:-Body),NHT,NHTOut,MLHTIn,MLHT) ; % clause is false test_head(RestM,(Head:-Body),NHTIn,NHTOut,MLHTIn,MLHTOut) ). test_head_subst(_Module,[],(_Head:-_Body)):-!. test_head_subst(Module,[H1|Rest],(Head:-Body)):- copy_term((Head:-Body),(Head1:-_Body1)), list2and(Head1List,Head1), Head1List=[El|_Rest], El=..[_F1|Args], H1=..[_F2|Args], distribute_not(Head1,InstHeadNot), (call((Module:InstHeadNot))-> % head is false, the clause does not cover the example fail ; % head is true, the clause covers the example test_head_subst(Module,Rest,(Head:-Body)) ). distribute_not(L,\+ L):- L\=(_,_),!. distribute_not((L,RestL),(\+ L ,NewRestL)):- distribute_not(RestL,NewRestL). test_body([],_Cl,NBT,NBT,CM,CM). test_body([(Module,_H)|RestM],(Head:-Body),NBTIn,NBTOut,CMIn,CMOut):- copy_term((Head:-Body),(Head1:-Body1)), findall(Head1,call(Module:Body1),LS), (LS=[]-> NBT is NBTIn, CMOut=CM, test_body(RestM,(Head:-Body),NBT,NBTOut,CMIn,CM) ; NBT is NBTIn+1, CMOut=[(Module,LS)|CM], test_body(RestM,(Head:-Body),NBT,NBTOut,CMIn,CM) ). load_models(File,ModulesList):- open(File,read,Stream), read_models(Stream,ModulesList), close(Stream). read_models(Stream,[(Name,_)|Names]):- read(Stream,begin(model(Name))),!, read_all_atoms(Stream,Name), read_models(Stream,Names). read_models(_S,[]). read_all_atoms(Stream,Name):- read(Stream,Atom), Atom \=end(model(Name)),!, assertz(Name:Atom), read_all_atoms(Stream,Name). read_all_atoms(_S,_N). title(File,Stream):- max_spec_steps(Spec), der_depth(Der), beamsize(B), ver(V), verbosity(Ver), verapp(Vapp), min_cov(MC), format(Stream,"~N ~N/*~NACL1 ver ~a AbdProofProc. ver ~a~NFile name: ~a~N", [V,Vapp,File]), format(Stream,"Max spec steps=~d, Beamsize=~d,~NDerivation depth=~d, Verbosity=~d, Minimum coverage=~d~N*/~N", [Spec,B,Der,Ver,MC]). delete_a_literal(Conj,ListOfConj):- findall(RemConj,delete_literal(Conj,RemConj),ListOfConj). delete_literal((_H,R),R). delete_literal((H,R),(H,R1)):- delete_literal(R,R1). list2and([],true):-!. list2and([X],X):- \+(is_list(X)), X\=(_,_),!. list2and([H|T],(H,Ta)):-!, list2and(T,Ta). memberchk_eq(A, [A1|_]) :-A==A1, !. memberchk_eq(A, [_|B]) :- memberchk_eq(A, B). print_list([],_Stream):-!. print_list([Rule|Rest],Stream):- numbervars(Rule,0,_M), format(Stream,"~p.~N",[Rule]), print_list(Rest,Stream). generate_file_names(File,FileKB,FileOut,FileL):- name(File,FileString), append(FileString,".kb",FileStringKB), name(FileKB,FileStringKB), append(FileString,".l",FileStringL), name(FileL,FileStringL), append(FileString,".out",FileOutString), name(FileOut,FileOutString). % select a literal from a list and return the elements after the element selected delete1([H|T],H,T). delete1([_H|T],El,T1):- delete1(T,El,T1). intersection1([],_L,[]):-!. intersection1([H|T],Y,[H|Z]):- member(H,Y),!, intersection1(T,Y,Z). intersection1([_H|T],Y,Z):- intersection1(T,Y,Z). intersection([],_L,[]):-!. intersection([(H,_)|T],Y,[(H,_)|Z]):- member((H,_),Y),!, intersection(T,Y,Z). intersection([(H,_)|T],Y,Z):- \+member((H,_),Y), intersection(T,Y,Z). /* | ?- lgg_clauses((win(conf1):- occ(place1,x,conf1),occ(place2,o,conf1)), (win(conf2):- occ(place1,x, conf2),occ(place2,x, conf2)),LGG). LGG = win(_A):-occ(place1,x,_A),occ(_B,x,_A),occ(_C,_D,_A),occ(place2,_D,_A) ? yes | ?- lgg_clauses((win(conf1):- occ(place1,x,conf1),occ1(place2,o,conf1)), (win(conf2):- occ(place1,x, conf2),occ1(place2,x, conf2)),LGG). LGG = win(_A):-occ(place1,x,_A),occ1(place2,_B,_A) ? yes */ lgg_clauses((H1:-B1),(H2:-B2),(H3:-B3)):- list2or(H1L,H1), length(H1L,N), list2or(H2L,H2), length(H2L,N), lgg_head_list(H1L,H2L,[],H3L,[],Subst), list2or(H3L,H3), length(H3L,N), list2and(B1L,B1), list2and(B2L,B2), lgg_list(B1L,B2L,[],B3L,Subst,_Subst1), list2and(B3L,B3). lgg_head_list([],_L2,L3,L3,S,S):-!. lgg_head_list([H1 : Prob|T1],L2,L3In,L3Out,SIn,SOut):- lgg_head_list1(H1,Prob,L2,L3,SIn,S1), append(L3In,L3,L31), lgg_head_list(T1,L2,L31,L3Out,S1,SOut). lgg_head_list1(_H1,_Prob,[],[],S,S):-!. lgg_head_list1(H1,Prob,[H2 : Prob|T2],[H3 : Prob|T3],SIn,SOut):- lgg1([H1],[H2],[H3],SIn,S1), nonvar(H3), !, lgg_head_list1(H1,Prob,T2,T3,S1,SOut). lgg_head_list1(H1,Prob,[_H2|T2],T3,SIn,SOut):- lgg_head_list1(H1,Prob,T2,T3,SIn,SOut). lgg_list([],_L2,L3,L3,S,S):-!. lgg_list([H1|T1],L2,L3In,L3Out,SIn,SOut):- lgg_list1(H1,L2,L3,SIn,S1), append(L3In,L3,L31), lgg_list(T1,L2,L31,L3Out,S1,SOut). lgg_list1(_H1,[],[],S,S):-!. lgg_list1(H1,[H2|T2],[H3|T3],SIn,SOut):- lgg1([H1],[H2],[H3],SIn,S1), nonvar(H3), !, lgg_list1(H1,T2,T3,S1,SOut). lgg_list1(H1,[_H2|T2],T3,SIn,SOut):- lgg_list1(H1,T2,T3,SIn,SOut). lgg_lit(L1,L2,L3):- lgg(L1,L2,L3),nonvar(L3). lgg(Term1,Term2,Term3) :- lgg1([Term1],[Term2],[Term3],[],_Subst), !. lgg1([],[],[],Subst,Subst). lgg1([Head1|Tail1],[Head2|Tail2],[Head3|Tail3],Subst1,Subst3) :- nonvar(Head1), nonvar(Head2), Head1 =..[F|Tail11], Head2 =..[F|Tail22], lgg1(Tail11,Tail22,Tail33,Subst1,Subst2), Head3 =..[F|Tail33], lgg1(Tail1,Tail2,Tail3,Subst2,Subst3), !. lgg1([Head1|Tail1],[Head2|Tail2],[Head3|Tail3],Subst1,Subst2) :- subst_member((Head3/(Head1,Head2)),Subst1), lgg1(Tail1,Tail2,Tail3,Subst1,Subst2), !. lgg1([Head1|Tail1],[Head2|Tail2],[Head3|Tail3],Subst1,Subst2) :- lgg1(Tail1,Tail2,Tail3,[(Head3/(Head1,Head2))|Subst1],Subst2), !. subst_member((A/B),[(A/C)|_]) :- B == C, !. subst_member(A,[_|B]) :- subst_member(A,B), !. list2or([],true):-!. list2or([X],X):- X\=or(_,_),!. list2or([H|T],(H or Ta)):-!, list2or(T,Ta).