/*
check_ic1: modified to handle is and =\= predicates

fitness: F/N F is the number of false derivations (satisfied constraints), N is the total
number of derivations
*/

:-use_module(library(lists)).

:-op(900,fx,not).

:-dynamic not/1.

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

not(_X).


check_ics_single_agent(AG,AbdIn,F,N):-
        get_all_ic(AG,Ics),!,
        length(Ics,N),
                                /* V b: modified */
        check_ics(Ics,AbdIn,0,F).
                                /* V b: modified */

get_all_ic(AG,List_of_ic):-
        findall((Ic,t),ic(Ic,AG),List_of_ic).


check_ics(AbdIn,F,N):-
        get_all_ic(Ics),!,
        length(Ics,N),
                                /* V b: modified */
        check_ics(Ics,AbdIn,0,F).
                                /* V b: modified */

get_all_ic(List_of_ic):-
        findall((Ic,t),ic(Ic,_AG),List_of_ic).

/* end */
check_ics([],_Abd,F,F):-!.


check_ics([H|T],Abd,FIn,FOut):-
        check_ic(H,Abd,V),
        F1 is FIn + V,
        check_ics(T,Abd,F1,FOut).

%/* one of the Ic is undefined */
%check_ic(([],u),_Abd,0.5):-!.

/* one of the Ic has been violated */
check_ic(([],t),_Abd,0):-!.

check_ic(([true|Rest_l],T),Abd,V):-!,
        check_ic((Rest_l,T),Abd,V).


/* (4) L1 has already been abduced */
check_ic(([L1|Rest_l],T),Abd,V):-
        memberchk(L1,Abd),!,
        check_ic((Rest_l,T),Abd,V).


/* (5) not(L1) has been abduced */
check_ic(([not L1| _Rest_l],_T) ,Abd,1):-
        memberchk(L1,Abd),!.

check_ic( ([L1|_Rest_l],_T) ,Abd,1):-
        memberchk(not L1,Abd),!.

%/* if L1 is a revisable of unknown truth value
%it is considered false */
%check_ic( ([not L1| Rest_l],T) ,Abd,V):-
%        revisable(L1),!,
%        check_ic((Rest_l,T),Abd,V).
%
%check_ic(([L1| Rest_l],_T) ,Abd,1):-
%        revisable(L1),!.

%/* if L1 is a revisable of unknown truth value
% the ic is assigned the truth value u */
%check_ic( ([not L1| Rest_l],_T) ,Abd,V):-
%        revisable(L1),!,
%        check_ic((Rest_l,u),Abd,V).
%
%check_ic(([L1| Rest_l],_T) ,Abd,V):-
%        revisable(L1),!,
%        check_ic((Rest_l,u),Abd,V).

check_ic(([true|Rest_l],T) ,Abd,V):-!,
        check_ic((Rest_l,T),Abd,V).


check_ic(([A is B|Rest_l],T) ,Abd,V):-!,
        (A is B->
                check_ic((Rest_l,T),Abd,V)
        ;
                V=1
        ).

check_ic(([ A=\=B|Rest_l],T) ,Abd,V):-!,
        (A=\=B->
                check_ic((Rest_l,T),Abd,V)
        ;
                V=1
        ).

check_ic(([ A>B|Rest_l],T) ,Abd,V):-!,
        (A>B->
                check_ic((Rest_l,T),Abd,V)
        ;
                V=1
        ).

check_ic( ([L1|Rest_l],T),Abd,V):-
% naf for non revisable is not admitted
        (L1=(not _L)->
                V=1
        ;
                findall((NewIc,T),(
                        clause(L1,BodyAnd),
                        and2list(BodyAnd,Body),
                        append(Body,Rest_l,NewIc)
                        ),
                        NewListIc),
                length(NewListIc,L),
                (L\==0->
                        check_ics(NewListIc,Abd,0,N),
                        (N==L->
                                V is 1
                        ;
                                V is 0
                        )
                ;
                        V=1
                )
        ).


and2list(A,[A]):-
        \+(A=(_B,_C)).


and2list((A,R),[A|T]):-
        and2list(R,T).




find_sol([],S,S):-!.

find_sol([H|T],SI,SO):-
        member(L,H),
        complement(L,L1),
        insert(L1,SI,SI1),
        find_sol(T,SI1,SO).

insert(L,[],[L]):-!.

insert(not L,[L|_T],_T):-!,fail.

insert(L,[not L|_T],_T):-!,fail.

insert(L,[L|T],[L|T]):-!.

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

solution(AG,C,NewC,Acc):-
        lamarck(AG,C,SS,Acc),
        find_sol(SS,[],S),
        update(S,C,NewC).

update([],C,C):-!.

update([H|T],Cin,Cout):-
        modify(H,Cin,C1),
        update(T,C1,Cout).

modify(H,C,C):-
        member(H,C),!.

modify(H,C,NC):-
        complement(H,NH),
        substitute(NH,C,H,NC).

lamarck(AG,AbdIn,SS,Acc):-
        get_all_ic(AG,Ics),!,
                                /* V b: modified */
        verify_ics(Ics,AbdIn,[],[],SS,[],Acc).

                                /* V b: modified */

/* end */
verify_ics([],_Abd,_S,SS,SS,Acc,Acc):-!.


verify_ics([H|T],Abd,S,SSIn,SSOut,AccIn,AccOut):-
        verify_ic(H,Abd,S,SSIn,SS1,AccIn,Acc1),
        verify_ics(T,Abd,S,SS1,SSOut,Acc1,AccOut).

%/* one of the Ic is undefined */
%verify_ic(([],u),_Abd,0.5,Acc,Acc):-!.

/* one of the Ic has been violated */
verify_ic(([],t),_Abd,S,SSI,[S|SSI],Acc,Acc):-!.

verify_ic(([true|Rest_l],T),Abd,S,SSI,SSO,AccI,AccO):-!,
        verify_ic((Rest_l,T),Abd,S,SSI,SSO,AccI,AccO).


verify_ic(([A is B|Rest_l],T),Abd,S,SSI,SSO,AccI,AccO):-!,
        (A is B->
                verify_ic((Rest_l,T),Abd,S,SSI,SSO,AccI,AccO)
        ;
                %the ic is satisfied
                AccO=AccI,
                SSO=SSI
        ).

verify_ic(([A=\=B|Rest_l],T),Abd,S,SSI,SSO,AccI,AccO):-!,
        (A=\=B->
                verify_ic((Rest_l,T),Abd,S,SSI,SSO,AccI,AccO)
        ;
                %the ic is satisfied
                AccO=AccI,
                SSO=SSI
        ).

verify_ic(([A>B|Rest_l],T),Abd,S,SSI,SSO,AccI,AccO):-!,
        (A>B->
                verify_ic((Rest_l,T),Abd,S,SSI,SSO,AccI,AccO)
        ;
                %the ic is satisfied
                AccO=AccI,
                SSO=SSI
        ).

%/* (5) not(L1) has been abduced */
%verify_ic(([not L1| Rest_l],T),Abd,S,SSI,SSO):-
%        revisable(L1),!,
%        verify_ic((Rest_l,T),Abd,[not L1|S],SSI,SSO).
%
%
%verify_ic( ([L1|Rest_l],T),Abd,S,SSI,SSO):-
%        revisable(L1),!,
%        verify_ic((Rest_l,T),Abd,[L1|S],SSI,SSO).


/* (4) L1 has already been abduced */
verify_ic(([L1|Rest_l],T),Abd,S,SSI,SSO,AccI,AccO):-
        memberchk(L1,Abd),!,
        verify_ic((Rest_l,T),Abd,[L1|S],SSI,SSO,[L1|AccI],AccO).

/* (5) not(L1) has been abduced */
verify_ic(([not L1| _Rest_l],_T),Abd,_S,SS,SS,Acc,[L1|Acc]):-
        memberchk(L1,Abd),!.

verify_ic( ([L1|_Rest_l],_T),Abd,_S,SS,SS,Acc,[L1|Acc]):-
        memberchk(not L1,Abd),!.

%/* if L1 is a revisable of unknown truth value
%it is considered false */
%verify_ic( ([not L1| Rest_l],T) ,Abd,V):-
%        revisable(L1),!,
%        verify_ic((Rest_l,T),Abd,V).
%
%verify_ic(([L1| Rest_l],_T) ,Abd,1):-
%        revisable(L1),!.

%/* if L1 is a revisable of unknown truth value
% the ic is assigned the truth value u */
%verify_ic( ([not L1| Rest_l],_T) ,Abd,V):-
%        revisable(L1),!,
%        verify_ic((Rest_l,u),Abd,V).
%
%verify_ic(([L1| Rest_l],_T) ,Abd,V):-
%        revisable(L1),!,
%        verify_ic((Rest_l,u),Abd,V).


verify_ic( ([L1|Rest_l],T),Abd,S,SSI,SSO,AccI,AccO):-
% naf for non revisable is not admitted
        (L1=(not _L)->
                %the ic is satisfied
                AccO=AccI,
                SSO=SSI
        ;
                findall((NewIc,T),(
                        clause(L1,BodyAnd),
                        and2list(BodyAnd,Body),
                        append(Body,Rest_l,NewIc)
                        ),
                        NewListIc),
                verify_ics(NewListIc,Abd,S,SSI,SSO,AccI,AccO)
        ).

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





solution(S):-
        support_sets(SS),
        find_sol(SS,[],S).

support_sets(SS):-
        get_all_ic(Ics),!,
                                /* V b: modified */
        verify_ic_no_abd_s(Ics,[],[],[],SS).
                                /* V b: modified */

verify_ic_no_abd_s([],_Abd,_S,SS,SS):-!.


verify_ic_no_abd_s([H|T],Abd,S,SSIn,SSOut):-
        verify_ic_no_abd_(H,Abd,S,SSIn,SS1),
        verify_ic_no_abd_s(T,Abd,S,SS1,SSOut).

%/* one of the Ic is undefined */
%verify_ic_no_abd_(([],u),_Abd,0.5):-!.

/* one of the Ic has been violated */
verify_ic_no_abd_(([],t),_Abd,S,SSI,[S|SSI]):-!.

verify_ic_no_abd_(([true|Rest_l],T),Abd,S,SSI,SSO):-!,
        verify_ic_no_abd_((Rest_l,T),Abd,S,SSI,SSO).



/* (5) not(L1) has been abduced */
verify_ic_no_abd_(([not L1| Rest_l],T),Abd,S,SSI,SSO):-
        revisable(L1),!,
        verify_ic_no_abd_((Rest_l,T),Abd,[not L1|S],SSI,SSO).


verify_ic_no_abd_( ([L1|Rest_l],T),Abd,S,SSI,SSO):-
        revisable(L1),!,
        verify_ic_no_abd_((Rest_l,T),Abd,[L1|S],SSI,SSO).


%/* (4) L1 has already been abduced */
%verify_ic_no_abd_(([L1|Rest_l],T),Abd,S,SSI,SSO):-
%        memberchk(L1,Abd),!,
%        verify_ic_no_abd_((Rest_l,T),Abd,[L1|S],SSI,SSO).
%
%/* (5) not(L1) has been abduced */
%verify_ic_no_abd_(([not L1| _Rest_l],_T),Abd,_S,SS,SS):-
%        memberchk(L1,Abd),!.
%
%verify_ic_no_abd_( ([L1|_Rest_l],_T),Abd,_S,SS,SS):-
%        memberchk(not L1,Abd),!.




verify_ic_no_abd_( ([L1|Rest_l],T),Abd,S,SSI,SSO):-
        findall((NewIc,T),(
                clause(L1,BodyAnd),
                and2list(BodyAnd,Body),
                append(Body,Rest_l,NewIc)
                ),
                NewListIc),
        verify_ic_no_abd_s(NewListIc,Abd,S,SSI,SSO).