/*
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/>.
*/

/* module declaration, commented for the moment */
:-module(ph2,[phase2/8,toplevelphase2/8,optimize/5]).

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

/* Top level predicate, performing optimizations in unfolding */
toplevelphase2(S,U,K,Lt,Boxs,Db,KFisso,Tree) :-
  optimize(S,U,Db,NewS,NewU),!,
  prove_phase2(NewS,NewU,K,Lt,Boxs,Db,KFisso,Tree).
  
/* Predicates for optimizing unfolding */
optimize(S,[],_,S,[]):-!.
optimize(S,[[[C inc D],_]|Tail],Db,SNew,[[[C inc D],UsedLabels]|NewU]):-
  foreachlabel(S,C inc D,Db,STemp,UsedLabels),!,
  optimize(STemp,Tail,Db,SNew,NewU).
foreachlabel(S,_,[],S,[]):-!.
foreachlabel(S,C inc D,[X|Tail],SNew,[X|TailLabels]):-
  member([X,C],S),!,
  foreachlabel([[X,D]|S],C inc D,Tail,SNew,TailLabels).
foreachlabel(S,C inc D,[X|Tail],SNew,[X|TailLabels]):-
  member([X,neg C],S),!,
  foreachlabel(S,C inc D,Tail,SNew,TailLabels).
foreachlabel(S,C inc D,[X|Tail],SNew,[X|TailLabels]):-
  member([X,D],S),!,
  foreachlabel(S,C inc D,Tail,SNew,TailLabels).
foreachlabel(S,ti C inc D,[X|Tail],SNew,[X|TailLabels]):-
  member([X,C],S),member([X,box neg C],S),!,
  foreachlabel([[X,D]|S],C inc D,Tail,SNew,TailLabels).
foreachlabel(S,ti C inc D,[X|Tail],SNew,[X|TailLabels]):-
  member([X,neg C],S),!,
  foreachlabel(S,ti C inc D,Tail,SNew,TailLabels).
foreachlabel(S,ti C inc D,[X|Tail],SNew,[X|TailLabels]):-
  member([X,D],S),!,
  foreachlabel(S,ti C inc D,Tail,SNew,TailLabels).
foreachlabel(S,ti C inc D,[X|Tail],SNew,[X|TailLabels]):-
  member([X,neg box neg C],S),!,
  foreachlabel(S,ti C inc D,Tail,SNew,TailLabels).
foreachlabel(S,C inc D,[_|Tail],SNew,UsedLabels):-!,
  foreachlabel(S,C inc D,Tail,SNew,UsedLabels).

/* clash */
prove_phase2(S,U,_,_,_,_,_,Tree) :- member([X,C],S), member([X,neg C],S),buildTree('ph2','clash',S,U,[],Tree),!.
prove_phase2(S,U,_,_,_,_,_,Tree) :- member([X,R,_],S), member([X,neg ex R in top],S),buildTree('ph2','clash',S,U,[],Tree),!.
prove_phase2(S,U,_,_,_,_,_,Tree) :- member([_,R,X],S), member([X,neg ex R inv in top],S), write('clash3 ph2\n'),buildTree('ph2','clash',S,U,[],Tree),!.
prove_phase2(S,U,[],_,_,_,_,Tree) :- buildTree('ph2','clash',S,U,[],Tree),!.
prove_phase2(S,U,_,_,_,_,KFisso,Tree) :- member([X,neg box neg C],S), \+member([X,neg box neg C],KFisso),buildTree('ph2','clash',S,U,[],Tree),!.

/* T+ */
prove_phase2(S,U,K,Lt,Boxs,Db,KFisso,Tree) :- select([X,ti C],S,S1),!,
                prove_phase2([[X,C]|[[X,box neg C]|S1]],U,K,Lt,Boxs,Db,KFisso,Tree1),!,
                buildTree('ph2','T+',S,U,[Tree1],Tree),!.


/* T- */
prove_phase2(S,U,K,Lt,Boxs,Db,KFisso,Tree) :- select([X,neg ti C],S,S1),!,
                prove_phase2([[X,neg C]|S1],U,K,Lt,Boxs,Db,KFisso,Tree1),
                prove_phase2([[X,neg box neg C]|S1],U,K,Lt,Boxs,Db,KFisso,Tree2),!,
                buildTree('ph2','T-',S,U,[Tree1,Tree2],Tree),!.


/* or+ */
prove_phase2(S,U,K,Lt,Boxs,Db,KFisso,Tree) :- select([X,C or D],S,S1),!,
                        prove_phase2([[X,C]|S1],U,K,Lt,Boxs,Db,KFisso,Tree1),
                        prove_phase2([[X,D]|S1],U,K,Lt,Boxs,Db,KFisso,Tree2),!,
                        buildTree('ph2','or+',S,U,[Tree1,Tree2],Tree),!.

/* cut */
prove_phase2(S,U,K,Lt,Boxs,Db,KFisso,Tree) :- member(C,Lt),member(X,Db),
                \+(member([X,box neg C],S)),
                \+(member([X,neg box neg C],S)),!,
                prove_phase2([[X,box neg C]|S],U,K,Lt,Boxs,Db,KFisso,Tree1),!,
                prove_phase2([[X,neg box neg C]|S],U,K,Lt,Boxs,Db,KFisso,Tree2),!,
                buildTree('ph2','cut',S,U,[Tree1,Tree2],Tree),!.

/* unfold */
prove_phase2(S,U,K,Lt,Boxs,Db,KFisso,Tree) :- member(X,Db),
                select([[C inc D],L1],U,U1),
                \+(member(X,L1)),!,
                prove_phase2([[X,(neg C) or D]|S],[[[C inc D],[X|L1]]|U1],K,Lt,Boxs,Db,KFisso,Tree1),!,
                buildTree('ph2','Unfold',S,U,[Tree1],Tree),!.


/* exists+ r */
prove_phase2(S,U,K,Lt,Boxs,Db,KFisso,Tree) :- select([X,ex R in top],S,S2),
                        select(X,Db,RecDb),!,
                        phase2RecEx(S2,U,K,Lt,Boxs,Db,RecDb,X,R,KFisso,ChildList),!,
                        buildTree('ph2','ex ',S,U,ChildList,Tree),!.


/* exists+ r inv*/
prove_phase2(S,U,K,Lt,Boxs,Db,KFisso,Tree) :- select([X,ex R inv in top],S,S2),
                        select(X,Db,RecDb),!,
                        phase2RecExInv(S2,U,K,Lt,Boxs,Db,RecDb,X,R,KFisso,ChildList),!,
                        buildTree('ph2','ex inv',S,U,ChildList,Tree),!.


/* box- */
prove_phase2(S,U,K,Lt,Boxs,Db,KFisso,Tree) :- member([X,neg box neg _],S), \+member(X,Boxs),!,
                        append(Boxs,[X],Boxs2),
                        extractNegBoxNegC(X,S,Lc,S2),
                        compareWithK(X,Lc,K),
                        phase2RecBoxConc(S,U,K,Lt,Boxs2,Db,Lc,X,S2,KFisso,Tree).


/* recursion on concepts for box -*/
phase2RecBoxConc(_,_,_,_,_,_,[],_,_,_,[]):-!.
phase2RecBoxConc(S,U,K,Lt,Boxs,Db,[C|Lc],X,SOld,KFisso,ChildList) :-
                                phase2RecBoxLab(S,U,K,Lt,Boxs,Db,Db,X,C,SOld,KFisso,ChildList1),
                                phase2RecBoxConc(S,U,K,Lt,Boxs,Db,Lc,X,SOld,KFisso,ChildList2),
                                append(ChildList1,ChildList2,ChildList).


/* recursion on Boxs for box - */                                
phase2RecBoxLab(_,_,_,_,_,_,[],_,_,_,_,[]):-!.
phase2RecBoxLab(S,U,K,Lt,Boxs,Db,[X|RecDb],X,C,SOld,KFisso,ChildList) :- phase2RecBoxLab(S,U,K,Lt,Boxs,Db,RecDb,X,C,SOld,KFisso,ChildList).
phase2RecBoxLab(S,U,K,Lt,Boxs,Db,[Y|RecDb],X,C,SOld,KFisso,[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),
		  	         removeBoxes(K,X,KNew),
                                prove_phase2(S7,U,KNew,Lt,Boxs,Db,KFisso,Tree),
                                phase2RecBoxLab(S,U,K,Lt,Boxs,Db,RecDb,X,C,SOld,KFisso,ChildList),!.


/* recursion for exists r inv */
phase2RecEx(_,_,_,_,_,_,[],_,_,_,[]):-!.
phase2RecEx(S,U,K,Lt,Boxs,Db,[Y|L2],X,R,KFisso,[Tree1|ChildList]) :- append(S,[[X,R,Y]],S2),
                                        prove_phase2(S2,U,K,Lt,Boxs,Db,KFisso,Tree1),
                                        phase2RecEx(S,U,K,Lt,Boxs,Db,L2,X,R,KFisso,ChildList),!.


/* recursion for exists r inv */
phase2RecExInv(_,_,_,_,_,_,[],_,_,_,[]):-!.
phase2RecExInv(S,U,K,Lt,Boxs,Db,[Y|L2],X,R,KFisso,[Tree1|ChildList]) :- append(S,[[Y,R,X]],S2),
                                        prove_phase2(S2,U,K,Lt,Boxs,Db,KFisso,Tree1),
                                        phase2RecExInv(S,U,K,Lt,Boxs,Db,L2,X,R,KFisso,ChildList),!.