/*
Copyright 2013 Laura Giordano, Valentina Gliozzi, Adam Jalal, Nicola Olivetti, Gian Luca Pozzato

    This file is part of PreDeLo 1.0.

    PreDeLo 1.0 is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    PreDeLo 1.0 is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with PreDeLo 1.0.  If not, see <http://www.gnu.org/licenses/>.
*/

/* imports */
:- use_module(library(lists)).
:- use_module(operators).
:- use_module(helpers).
:- use_module(ph2).


/* top level */
prove(S,U,[X,F],Tree) :- append(S,[[X,neg F]],S1),
                getTypicals(S1,LtABox),!,
                getTypicals(U,LtTBox),!,
                append(LtABox,LtTBox,Lt),!,
                initLabels(S1,Labels),!,
                prove(S1,U,Lt,Labels,S,[],Tree),!.

/* clash */
prove(S,U,_,_,_,_,Tree) :- member([X,C],S), member([X, neg C],S),buildTree('ph1','clash',S,U,[],Tree),!.
prove(S,U,_,_,_,_,Tree) :- member([X,R,_],S), member([X,neg ex R in top],S),buildTree('ph1','clash',S,U,[],Tree),!.
prove(S,U,_,_,_,_,Tree) :- member([_,R,X],S), member([X,neg ex R inv in top],S),buildTree('ph1','clash',S,U,[],Tree),!.


/* T+ */
prove(S,U,Lt,Labels,Abox,Boxs,Tree) :- select([X,ti C],S,S1),!,
                prove([[X,C]|[[X,box neg C]|S1]],U,Lt,Labels,Abox,Boxs,Tree1),!,
                buildTree('ph1','T+',S,U,[Tree1],Tree),!.


/* pre-unfolds (optimization) */
prove(S,U,Lt,Labels,Abox,Boxs,Tree):-
    select([[C inc D],L1],U,UNew),
    member(X,Labels),
    \+(member(X,L1)),
    member([X,C],S),!,
    prove([[X,D]|S],[[[C inc D],[X|L1]]|UNew],Lt,Labels,Abox,Boxs,Tree).
prove(S,U,Lt,Labels,Abox,Boxs,Tree):-
    select([[ti C inc D],L1],U,UNew),
    member(X,Labels),
    \+(member(X,L1)),
    member([X,C],S),
    member([X,box neg C],S),!,
    prove([[X,D]|S],[[[ti C inc D],[X|L1]]|UNew],Lt,Labels,Abox,Boxs,Tree).
prove(S,U,Lt,Labels,Abox,Boxs,Tree):-
    select([[C inc D],L1],U,UNew),
    member(X,Labels),
    \+(member(X,L1)),
    member([X,neg C],S),!,
    prove(S,[[[C inc D],[X|L1]]|UNew],Lt,Labels,Abox,Boxs,Tree).
prove(S,U,Lt,Labels,Abox,Boxs,Tree):-
    select([[C inc D],L1],U,UNew),
    member(X,Labels),
    \+(member(X,L1)),
    member([X,D],S),!,
    prove(S,[[[C inc D],[X|L1]]|UNew],Lt,Labels,Abox,Boxs,Tree).
prove(S,U,Lt,Labels,Abox,Boxs,Tree):-
    select([[ti C inc D],L1],U,UNew),
    member(X,Labels),
    \+(member(X,L1)),
    member([X,neg C],S),!,
    prove(S,[[[ti C inc D],[X|L1]]|UNew],Lt,Labels,Abox,Boxs,Tree).
prove(S,U,Lt,Labels,Abox,Boxs,Tree):-
    select([[ti C inc D],L1],U,UNew),
    member(X,Labels),
    \+(member(X,L1)),
    member([X,neg box neg C],S),!,
    prove(S,[[[ti C inc D],[X|L1]]|UNew],Lt,Labels,Abox,Boxs,Tree).


/* unfold */
prove(S,U,Lt,Labels,Abox,Boxs,Tree) :- member([X,_],S),
                select([[C inc D],L1],U,U1),
                \+(member(X,L1)),!,
                prove([[X, D or (neg C)]|S],[[[C inc D],[X|L1]]|U1],Lt,Labels,Abox,Boxs,Tree1),!,
                buildTree('ph1','Unfold',S,U,[Tree1],Tree),!.


/* T- */
prove(S,U,Lt,Labels,Abox,Boxs,Tree) :- select([X,neg ti C],S,S1),!,
                prove([[X,neg C]|S1],U,Lt,Labels,Abox,Boxs,Tree1),
                prove([[X,neg box neg C]|S1],U,Lt,Labels,Abox,Boxs,Tree2),
                buildTree('ph1','T-',S,U,[Tree1,Tree2],Tree),!.


/* or+ */
prove(S,U,Lt,Labels,Abox,Boxs,Tree) :- select([X,C or D],S,S1),!,
                        prove([[X,C]|S1],U,Lt,Labels,Abox,Boxs,Tree1),
                        prove([[X,D]|S1],U,Lt,Labels,Abox,Boxs,Tree2),
                        buildTree('ph1','or+',S,U,[Tree1,Tree2],Tree),!.

/* cut */
prove(S,U,Lt,Labels,Abox,Boxs,Tree) :- member(C,Lt),
                member(X,Labels),
                \+(member([X,box neg C],S)),
                \+(member([X,neg box neg C],S)),!,
                prove([[X,box neg C]|S],U,Lt,Labels,Abox,Boxs,Tree1),!,
                prove([[X,neg box neg C]|S],U,Lt,Labels,Abox,Boxs,Tree2),!,
                buildTree('ph1','cut',S,U,[Tree1,Tree2],Tree),!.


/* exists+ r inv 1 */
prove(S,U,Lt,Labels,Abox,Boxs,Tree) :- select([X,ex R inv in top],S,S2),
                        \+member([_,_,_],S),!,
                        genLabel(Labels,_,NewLabels),
                        select(X,NewLabels,RecLabels),
                        proveRecExInv(S2,U,Lt,Abox,NewLabels,RecLabels,X,R,Boxs,ChildList),!,
                        buildTree('ph1','ex inv 1',S,U,ChildList,Tree),!.
                        

/* exists+ r inv 2 */
prove(S,U,Lt,Labels,Abox,Boxs,Tree) :- select([X,ex R in top],S,S2),
                        member([_,_,_],S),!,
                        select(X,Labels,RecLabels),
                        proveRecExInv(S2,U,Lt,Abox,Labels,RecLabels,X,R,Boxs,ChildList),!,
                        buildTree('ph1','ex inv 2',S,U,ChildList,Tree),!.


/* exists+ r1 */
prove(S,U,Lt,Labels,Abox,Boxs,Tree) :- select([X,ex R in top],S,S2),
                        \+member([_,_,_],S),!,
                        genLabel(Labels,_,NewLabels),
                        select(X,NewLabels,RecLabels),
                        proveRecEx(S2,U,Lt,Abox,NewLabels,RecLabels,X,R,Boxs,ChildList),!,
                        buildTree('ph1','ex 1',S,U,ChildList,Tree),!.


/* exists+ r2 */
prove(S,U,Lt,Labels,Abox,Boxs,Tree) :- select([X,ex R in top],S,S2),
                        member([_,_,_],S),!,
                        select(X,Labels,RecLabels),
                        proveRecEx(S2,U,Lt,Abox,Labels,RecLabels,X,R,Boxs,ChildList),!,
                        buildTree('ph1','ex 2',S,U,ChildList,Tree),!.



/* box- */
prove(S,U,Lt,Labels,Abox,Boxs,Tree) :- member([X,neg box neg _],S), \+member(X,Boxs),!,
                        append(Boxs,[X],Boxs2),
                        extractNegBoxNegC(X,S,Lc,_),
                        genLabel(Labels,_,NewLabels),
                        proveRecBoxConc(S,U,Lt,Abox,NewLabels,Lc,X,S,Boxs2,ChildList),
                        buildTree('ph1','box-',S,U,ChildList,Tree),!.

/* phase2 */
prove(S,U,Lt,Labels,Abox,_,[]) :-getK(S,Lt,K),
                                removeDup(K,K2),
                                clearSubsumptions(U,U1),
                                \+toplevelphase2(Abox,U1,K2,Lt,[],Labels,K2,_),!.

/* recursion on concepts for box -*/
proveRecBoxConc(_,_,_,_,_,[],_,_,_,[]):-!.
proveRecBoxConc(S,U,Lt,Abox,Labels,[C|Lc],X,SOld,Boxs,ChildList) :-
                                proveRecBoxLab(S,U,Lt,Abox,Labels,Labels,X,C,SOld,Boxs,ChildList1),
                                proveRecBoxConc(S,U,Lt,Abox,Labels,Lc,X,SOld,Boxs,ChildList2),
                                append(ChildList1,ChildList2,ChildList).

/* recursion on labels for box - */                                
proveRecBoxLab(_,_,_,_,_,[],_,_,_,_,[]):-!.
proveRecBoxLab(S,U,Lt,Abox,Labels,[X|RecLabels],X,C,SOld,Boxs,ChildList) :- proveRecBoxLab(S,U,Lt,Abox,Labels,RecLabels,X,C,SOld,Boxs,ChildList).
proveRecBoxLab(S,U,Lt,Abox,Labels,[Y|RecLabels],X,C,SOld,Boxs,[Tree|ChildList]) :- 
                                append(S,[[Y,C]],S2),
                                append(S2,[[Y,box neg C]],S3),
                                genSmList(X,Y,S,S4),
                                append(S3,S4,S5),
                                genSmCompList(X,Y,C,SOld,S6),
                                append(S5,S6,S7),
                                removeDup(S7,S8),
                                prove(S8,U,Lt,Labels,Abox,Boxs,Tree),
                                proveRecBoxLab(S,U,Lt,Abox,Labels,RecLabels,X,C,SOld,Boxs,ChildList),!.

/* recursion for exists r */
proveRecEx(_,_,_,_,_,[],_,_,_,[]):-!.
proveRecEx(S,U,Lt,Abox,Labels,[Y|L2],X,R,Boxs,[Tree1|ChildList]) :- append(S,[[X,R,Y]],S2),
                                        prove(S2,U,Lt,Labels,Abox,Boxs,Tree1),
                                        proveRecEx(S,U,Lt,Abox,Labels,L2,X,R,Boxs,ChildList),!.

/* recursion for exists inv r */
proveRecExInv(_,_,_,_,_,[],_,_,_,[]):-!.
proveRecExInv(S,U,Lt,Abox,Labels,[Y|L2],X,R,Boxs,[Tree1|ChildList]) :- append(S,[[Y,R,X]],S2),
                                        prove(S2,U,Lt,Labels,Abox,Boxs,Tree1),
                                        proveRecExInv(S,U,Lt,Abox,Labels,L2,X,R,Boxs,ChildList),!.