/* abdpp.pl, Abductive proof procedure */
/* version lpkr97:
	no inconsistency procedure is used
*/

/* version k
	corrected a bug of version i:
		the literal to be adbuced is skolemized only if it is positive
		skolem((not(Goal),..) did not work
*/

/* version j
	corrected a bug of the inconsistency procedure:
		even if no cosntraint was violated, the inc suceedeed
		becuase at_least_one_violated with [] succeeded
*/

/* version i
        treatment of non ground abducibles: every free variable is skolemized
		when the consistency is entered
		restriction: only constraint of the type
			<-a(X),... (type2)
		and not of the type 
			<-not(a(X)).... (type1)
		type1 ic could provide instantiations for X, so they should
		be tried first
		
*/

/* version h:
	ensured that non abducibles are resolved before abucibles in the 
		abductive derivation
*/

/* version g
        negation as failure literals for non abducible predicates are
        treated differently: they are not included in the set of abducibles
        the negation of non abd pred has not to be specified among abd nor
        the ic a,not(a) have to be specified for non abd

        but the negation of abd and the relative constraint have to be spec

	added the message when the depth limit is reached in the consistency
*/

/* version f
	inconsistency checking using only rules, not 
		abduced literals
	corrected the loop problem of inconsistency checking
	select_literal_in_1st_ic added in order to simplify the code
*/

/* version e
	literals that must be true according to ics are not abduced:
		inconsistency checking added
	from setof to findall for abducibles non ground
	selection rule in ics: 
		reduce first non abducibles, without choice point
		then abducibles, keeping a choice point, when the ic contains
			only non abd
		assumption: the rules and ic contain first non abd and then
			abd in their bodies
*/

/* Version d: limit on the depth of derivations added */

/* Version c: merge of version b and a

	version for Sicstus #2.1

	1) uniform treatment of user defined abducibles and default abducibles:
	besides the user defined abd and their constraints, the user must  
	include in the abducibles all the default literals not(a) plus all the
	constraints
	<-a,not(a). (version c) Example of input:

	rule(p,[q]).

	abducibles([not(p),q,not(q)]).

	ic([p,not(p)]).
	ic([q,not(q)]).
	
	2) the algorithm is able to find all the alternative explanations
	(version b) */

/* Version b: differences with version a1:
	the selection of the literal to be proved false in the 
	consistency phase is now done by a select predicate which leaves
	other choices open for backtracking
	In this way this algorithm finds all the minimal models !*/

/* Version a1: differences with version a
	no 3): negation of abducibles has not to appear in the list of
	abd.*/
	

/* Version a: differences with version 0
	1) treatment of negation as abduction for predicates
	not abducibile: not(p) and <-p,not(p) have to be included
	2) abducible can appear in the head of clauses
	3) negation of abducibles have to appear in the list of
	abducibles

*/

/* Version 0:
(negation of abducible is dealt implicitly by the
algorithm, therefore the ics expressing <-abd,not(abd) dont have
to be expressed)
falso, devono essere espressi altrimenti quando si fa la query
	not(abd)
viene subito abdotto not(abd) senza passare alla consistency per
abd*/

:-use_module(library(lists)).

abducible(A):-
	abducibles(AbdSet),
	memberchk(A,AbdSet),!.


/* Abductive derivation:
solve_abd(Goal,AbdIn,AbdOut,Depth) */

/* normal resolution steps */
solve_abd([],Abd,Abd,_Depth):-!.

/* depth limit reached */
solve_abd(Goal,_,_,0):-!,
	format("Depth limit reached, goal ~p~N",[Goal]),
        fail.

solve_abd([A|B],AbdIn,AbdOut,Depth):-
	rule(A,Body),
	Depth1 is Depth - 1,
	insert_nabd_1st(Body,B,B1),
	solve_abd(B1,AbdIn,AbdOut,Depth1).

/* NAF goal: not(A) where A is not abd */
solve_abd([not(A)|B],AbdIn,AbdOut,Depth):-
        not(abducible(A)),!,
        solve_con2([[A]],[not(A)|AbdIn],AbdOut1,Depth),
        delete(AbdOut1,not(A),AbdOut2),
	solve_abd(B,AbdOut2,AbdOut,Depth).

/* end of normal resolution steps */

/* (1) A has already been abduced */
solve_abd([A|B],AbdIn,AbdOut,Depth):-
	abducible(A),
	memberchk(A,AbdIn),!,
	solve_abd(B,AbdIn,AbdOut,Depth).


/* (2) A is abducible but neither A nor not(A) have already been abduced */
solve_abd([not(A)|B],AbdIn,AbdOut,Depth):-
	abducible(not(A)),!,
	not(memberchk(A,AbdIn)),
	solve_con(not(A),[not(A)|AbdIn],AbdOut1,Depth),
	solve_abd(B,AbdOut1,AbdOut,Depth).


solve_abd([A|B],AbdIn,AbdOut,Depth):-
	abducible(A),!,
	not(memberchk(not(A),AbdIn)),
	solve_con(A,[A|AbdIn],AbdOut1,Depth),
	solve_abd(B,AbdOut1,AbdOut,Depth).

/* A not a list */
solve_abd(A,AbdIn,AbdOut,Depth):-
        not(is_list(A)),!,
        solve_abd([A],AbdIn,AbdOut,Depth).


/* Consistency derivation:
solve_con(Goal,AbdIn,AbdOut,Depth) */

solve_con(Goal,AbdIn,AbdOut,Depth):-
	skolem(Goal),
	get_all_ic(Goal,[First_ic | Rest_ics]),!,
				/* V b: modified */
	select_literal(First_ic,First_ic1),
				/* V b: added */
	solve_con2([First_ic1 | Rest_ics],AbdIn,AbdOut,Depth).
				/* V b: modified */

/* if there are no ics, then Goal can be abducted */
solve_con(_Goal,Abd,Abd,_Depth):-!.

/*v b: predicate that selects one literal from the ic
 	and puts it in the head of ic
the selection is done only if the ic contains only abducibles */

select_literal_in_1st_ic([],[]):-!.

select_literal_in_1st_ic([FirstIc|RestIc],[NewFirstIc|RestIc]):-
	select_literal(FirstIc,NewFirstIc).

select_literal([],[]):-!.

select_literal([Lit|RestIcIn],[L|IcOut]):-
	abducible(Lit),!,
	select(L,[Lit|RestIcIn],IcOut).

select_literal(Ic,Ic).

get_all_ic(Goal,List_of_ic):-
	findall(Ic,get_ic(Goal,Ic),List_of_ic).

get_ic(Goal,Ic):-
	ic(X),memberchk(Goal,X),delete(X,Goal,Ic).

/* all the ic are satisfied */
solve_con2([],Abd,Abd,_):-!. 

/* one of the Ic has been violated */
solve_con2([ [] |_],_,_,_):-!,fail.

/* depth limit reached */
solve_con2(Ics,_,_,0):-!,
	format("Depth limit reached, ics ~p~N",[Ics]),
        fail.

/* (3) first try to use resolution */
solve_con2([ [L1|Rest_l] |Rest_ic],AbdIn,AbdOut,Depth):-
	findall(NewIc,(rule(L1,Body),insert_nabd_1st(Body,Rest_l,NewIc)),
		NewListIc),
	(NewListIc=[]->
		fail
	;
		!
	),
	appendc(NewListIc,Rest_ic,[ Ic | Rest_ic1]),
	select_literal(Ic,Ic1),
	Depth1 is Depth - 1,
	solve_con2([Ic1 | Rest_ic1],AbdIn,AbdOut,Depth1).

/* (4) L1 has already been abduced */
solve_con2([ [L1|Rest_l] |Rest_ic],AbdIn,AbdOut,Depth):-
	memberchk(L1,AbdIn),!,
	select_literal(Rest_l,Rest_l1),
	solve_con2([Rest_l1|Rest_ic],AbdIn,AbdOut,Depth).


/* (5) not(L1) has been abduced */
solve_con2([ [not(L1)| _Rest_l] |Rest_ic],AbdIn,AbdOut,Depth):-
	memberchk(L1,AbdIn),!,
	select_literal_in_1st_ic(Rest_ic,Rest_ic1),
	solve_con2(Rest_ic1,AbdIn,AbdOut,Depth).

solve_con2([ [L1|_Rest_l] |Rest_ic],AbdIn,AbdOut,Depth):-
	memberchk(not(L1),AbdIn),!,
	select_literal_in_1st_ic(Rest_ic,Rest_ic1),
        solve_con2(Rest_ic1,AbdIn,AbdOut,Depth).

/* (6) L1 is abducible but neither L1 nor not(L1) have already been abduced */

/* (6a) see if not(L1) is implied by the constraints, i.e. L1 violates at least
		one constraint 
	proof of inconsistency for not(L1)  */
/* version lpkr97: no inconsistency
solve_con2([ [L1|_Rest_l] |Rest_ic],AbdIn,AbdOut,Depth):-
	abducible(not(L1)),
	inconsistency(L1,AbdIn,Depth),!,
	select_literal_in_1st_ic(Rest_ic,Rest_ic1),
        solve_con2(Rest_ic1,AbdIn,AbdOut,Depth).
*/

/* (6b) start an abductive derivation for not(L1) */
solve_con2([ [not(L1)|_Rest_l] |Rest_ic],AbdIn,AbdOut,Depth):-
	abducible(not(L1)),!,
	solve_abd(L1,AbdIn,AbdOut1,Depth),
	select_literal_in_1st_ic(Rest_ic,Rest_ic1),
        solve_con2(Rest_ic1,AbdOut1,AbdOut,Depth).

solve_con2([ [L1|_Rest_l] |Rest_ic],AbdIn,AbdOut,Depth):-
	abducible(L1),!,
	solve_abd(not(L1),AbdIn,AbdOut1,Depth),
	select_literal_in_1st_ic(Rest_ic,Rest_ic1),
        solve_con2(Rest_ic1,AbdOut1,AbdOut,Depth).


/* (7) L1 is not abducible and has no successful rule */
solve_con2([ [_L1|_Rest_l] |Rest_ic],AbdIn,AbdOut,Depth):-
	select_literal_in_1st_ic(Rest_ic,Rest_ic1),
        solve_con2(Rest_ic1,AbdIn,AbdOut,Depth).

inconsistency(Goal,Abd,Depth):-
	get_all_ic(Goal,ICs),!,
	at_least_one_violated(ICs,Abd,Depth).

at_least_one_violated([],_Abd,_Depth):-!,fail.

at_least_one_violated([Ic|_RestIc],Abd,Depth):-
	solve_nc(Ic,Abd,Depth),!.

at_least_one_violated([_Ic|RestIc],Abd,Depth):-
	at_least_one_violated(RestIc,Abd,Depth).
	
/* Abductive derivation without consistency
solve_nc(Goal,Abd,Depth) */

/* normal resolution steps */
solve_nc([],_Abd,_Depth):-!.

/* depth limit reached */
solve_nc(Goal,_,0):-!,
        format("Depth limit reached in inconsistency, goal ~p~N",[Goal]),
        fail.

solve_nc([A|B],Abd,Depth):-!,
        solve_nc(A,Abd,Depth),
        solve_nc(B,Abd,Depth).

solve_nc(A,Abd,Depth):-
        rule(A,Body),
        Depth1 is Depth - 1,
        solve_nc(Body,Abd,Depth1).
/* end of normal resolution steps */

/* (1) A has already been abduced */
solve_nc(A,Abd,_Depth):-
        abducible(A),
        memberchk(A,Abd),!.

/* insert_nabd_1st: assumption: in Body the non abd are before the abd */

insert_nabd_1st([],Cl,Cl):-!.

insert_nabd_1st([Nonabd|RestBody],RestIc,[Nonabd|NewRestIc]):-
	not(abducible(Nonabd)),!,
	insert_nabd_1st(RestBody,RestIc,NewRestIc).

insert_nabd_1st(RestBodyOfAbd,RestIc,NewIc):-
	appendc(RestIc,RestBodyOfAbd,NewIc).
/* when only abducible are lerft, they are added to the bottom of the ic */

appendc([],L,L):-!. % append redefined for optimization: ! added

appendc([H|T],L,[H|T1]):-
	appendc(T,L,T1).

skolem(not(Goal)):-!,
	Goal=..[_|Args],
        skolem1(Args).

skolem(Goal):-
	Goal=..[_|Args],
	skolem1(Args).

skolem1([]):-!.

skolem1([H|T]):-
	(var(H)->
		new_const(H)
	;
		true
	),
	skolem1(T).

new_const(H):-
	retract(new_const_number(N)),
	N1 is N + 1,
	assert(new_const_number(N1)),
	number_chars(N,Nstr),
	append("skolem",Nstr,Nconst),
	name(H,Nconst).

:-dynamic new_const_number/1.
	
new_const_number(0).

not(X):-X,!,fail.

not(_).