/* lap.pl: LAP: Learning Abductive Programs */


:-[abdpp].

der_depth(10).

induce:-
	der_depth(Der),
	format("LAP ver 1~NMax derivation depth=~d~N ~N",[Der]),
	eplus(Eplus),
	eminus(Eminus),
	covering_loop(Eplus,Eminus,[],L,[],Delta),
        format(" ~NEnd execution. Generated rules~N",[L]),
        print_list(L),
	format(" ~NAbduced literals: ~p~N",[Delta]).

print_list([]):-!.

print_list([H|T]):-
        print_list(T),
        format("~w~N",[H]).

/* covering loop */
/* no more positive examples to be covered: end */
covering_loop([],_Eminus,L,L,Delta,Delta):-!.

/* some positive examples left: generate a new clause, add it to the theory
and remove the examples covered by the clause */
covering_loop(Eplus,Eminus,Lin,Lout,Delta,Deltaout):-
	format("Current training set: ~NE+=~p~NE-=~p ~N",
		[Eplus,Eminus]),
	generate_cl(Eplus,Eminus,Epluscov,Cl,Delta,Delta1),!,
	deleteall(Delta1,Delta,NewDelta), 
        format("Generated clause: ~p~N\c
                Positive examples covered: ~p~N~NAbduced literals: ~p~N ~N",
                [Cl,Epluscov,NewDelta]),
	update(Eplus,Epluscov,Eplus1,Eminus,Eminus1,Delta1,Delta2),
	covering_loop(Eplus1,Eminus1,[Cl|Lin],Lout,Delta2,Deltaout).

/* if generate_cl fails, then return the current set of clauses L*/
covering_loop(_Eplus,_Eminus,L,L,Delta,Delta).

/* removes the covered positive examples from E+ and moves abduced literals of
target predicates from delta to the training set */
update(Eplusin,Epluscov,Eplusout,Eminusin,Eminusout,Delta,Deltaout):-
        deleteall(Eplusin,Epluscov,Eplus1),
        add_abd(Delta,[],Deltaout,Eplus1,Eplusout,Eminusin,Eminusout).

add_abd([],D,D,Eplus,Eplus,Eminus,Eminus):-!.

add_abd([not(A)|DeltaRest],Din,Dout,Eplusin,Eplusout,Eminusin,[A|Eminusout]):-
        bias(rule(A,_AllowedLiterals)),!,
        add_abd(DeltaRest,Din,Dout,Eplusin,Eplusout,Eminusin,Eminusout).

add_abd([A|DeltaRest],Din,Dout,Eplusin,[A|Eplusout],Eminusin,Eminusout):-
        bias(rule(A,_AllowedLiterals)),!,
        add_abd(DeltaRest,Din,Dout,Eplusin,Eplusout,Eminusin,Eminusout).

add_abd([A|DeltaRest],Din,[A|Dout],Eplusin,Eplusout,Eminusin,Eminusout):-
        add_abd(DeltaRest,Din,Dout,Eplusin,Eplusout,Eminusin,Eminusout).


deleteall(Eplus,[],Eplus):-!.

deleteall(Eplusin,[H|T],Eplusout):-
	delete(Eplusin,H,Eplusout1),
	deleteall(Eplusout1,T,Eplusout).

/* generate a clause that covers at least one positive example and no
negative one */
generate_cl(Eplus,Eminus,Epluscovered,Cl,Deltain,Deltaout):-
% pick a target predicate 
	bias(rule(H,AllowedLiterals)),
	functor(H,N,A),
% generates a head with new variables
	functor(H1,N,A), 
	memberchk(H1,Eplus), 
% verifies that there is at least one pos ex for H in the training set 
% start the specialization loop with the rule p(X):-.
	specialize(rule(H,[]),Cl,AllowedLiterals,
		Eplus,Epluscovered,Eminus,Deltain,Deltaout).

/* specialization loop */
specialize(Clin,Clout,AllowedLiterals,Eplus,Epluscovered,Eminus,Deltain,Deltaout):-
	asserta(Clin),
	Clin=rule(H,Body),
	epluscovered(H,Eplus,[],Epluscovered1,Deltain,Delta1),
	(Epluscovered1=[]->
		% the rule does not cover any positive example, therefore backtracking
		retract(Clin),
		fail
	;
		eminuscovered(Eminus,[],Eminuscovered,Delta1,Delta2),
		(Eminuscovered=[]->
			% consistent clause, end of the loop
			Clout=Clin,
			Epluscovered=Epluscovered1,
			Deltaout=Delta2
		;
			% inconsistent clause: new iteration of the loop			
			retract(Clin),
			% pick a literal from the bias
			select_literal_to_add(L,AllowedLiterals,AllLit1),
			append(Body,[L],Body1),
			specialize(rule(H,Body1),Clout,
				AllLit1,
				Eplus,Epluscovered,Eminuscovered,
				Delta2,Deltaout)
		)
	).




/* select a literal from the bias */
select_literal_to_add(L,AllLitin,AllLitout):-
			member(L,AllLitin),
			delete(AllLitin,L,AllLitout).

/* epluscovered: test the coverage of positive examples */
epluscovered(_Target,[],Epc,Epc,Delta,Delta):-!.

epluscovered(Target,[H|T],Epcin,Epcout,Deltain,Deltaout):-   
	functor(Target,F,A),
	functor(Target1,F,A),
	\+(Target1=H),!,
	epluscovered(Target,T,Epcin,Epcout,Deltain,Deltaout).  

epluscovered(Target,[H|T],Epcin,Epcout,Deltain,Deltaout):-
	der_depth(Depth),
	rule(H,B), % added to avoid the abduction of H
	(solve_abd(B,Deltain,Delta1,Depth)->
		% covered example 
		epluscovered(Target,T,[H|Epcin],Epcout,Delta1,Deltaout)
	;
		epluscovered(Target,T,Epcin,Epcout,Deltain,Deltaout)
	).

/* eminuscovered: test the coverage of negative examples */
eminuscovered([],Emc,Emc,Delta,Delta):-!.
	
eminuscovered([H|T],Emcin,Emcout,Deltain,Deltaout):-
	der_depth(Depth),
	(solve_abd(not(H),Deltain,Delta1,Depth)->
		% es non coperto (not(H) ha successo)
		delete(Delta1,not(H),Delta2),
		% elimino not(H) dagli abdotti
		eminuscovered(T,Emcin,Emcout,Delta2,Deltaout)
	;
		eminuscovered(T,[H|Emcin],Emcout,Deltain,Deltaout)
	).