/*
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(alctm2,[prove_phase2/6,toplevelphase2/6]).

:- use_module(library(lists)).
:- use_module(operators).
:- use_module(helpers).


/* Top level predicate, performing optimizations in unfolding */
toplevelphase2(S,U,Lt,K,Bb,Db):-
  optimize(S,U,Db,NewS,NewU),!,
  prove_phase2(NewS,NewU,Lt,K,Bb,Db).
 
/* 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(_,_,_,[],_,_) :- !.
prove_phase2(S,_,_,_,Bb,_) :- member([X,neg box neg C],S), \+member([X,neg box neg C],Bb),!.
prove_phase2(S,_,_,_,_,_) :- member([X,C],S), member([X, neg C],S),!.
prove_phase2(S,_,_,_,_,_) :- member([_,neg top],S),!.
prove_phase2(S,_,_,_,_,_) :- member([_,bottom],S),!.

/* and + */
prove_phase2(S,U,Lt,K,Bb,Db) :- select([X,C and D],S,S1),!,
                prove_phase2([[X,C]|[[X,D]|S1]],U,Lt,K,Bb,Db),!.


/* or - */
prove_phase2(S,U,Lt,K,Bb,Db) :- select([X,neg (C or D)],S,S1),
                prove_phase2([[X,neg C]|[[X,neg D]|S1]],U,Lt,K,Bb,Db),!.


/* neg */
prove_phase2(S,U,Lt,K,Bb,Db) :- select([X, neg neg C],S,S1),
                prove_phase2([[X,C]|S1],U,Lt,K,Bb,Db),!.


/* T+ */
prove_phase2(S,U,Lt,K,Bb,Db) :- select([X,ti C],S,S1),
                prove_phase2([[X,C]|[[X,box neg C]|S1]],U,Lt,K,Bb,Db),!.


/* for each + */
prove_phase2(S,U,Lt,K,Bb,Db) :- member([X,fe R in C],S),
                member([X,R,Y],S),
                \+(member([Y,C],S)),!,
                prove_phase2([[Y,C]|S],U,Lt,K,Bb,Db),!.


/* exists - */
prove_phase2(S,U,Lt,K,Bb,Db) :- member([X,neg ex R in C],S),
                member([X,R,Y],S),
                \+(member([Y,neg C],S)),!,
                prove_phase2([[Y,neg C]|S],U,Lt,K,Bb,Db),!.


/* unfold */
prove_phase2(S,U,Lt,K,Bb,Db) :- 
                select([[C inc D],L],U,U1),
                member(X,Db),
                \+member(X,L),!,
                prove_phase2([[X,(neg C) or D]|S],[[C inc D],[X|L]]|U1],Lt,K,Bb,Db),!.


/* and - */
prove_phase2(S,U,Lt,K,Bb,Db) :- select([X, neg(C and D)],S,S1),
                prove_phase2([[X, neg C]|S1],U,Lt,K,Bb,Db),!,
                prove_phase2([[X, neg D]|S1],U,Lt,K,Bb,Db),!.


/* or + */
prove_phase2(S,U,Lt,K,Bb,Db) :- select([X,C or D],S,S1),
                prove_phase2([[X,C]|S1],U,Lt,K,Bb,Db),!,
                prove_phase2([[X,D]|S1],U,Lt,K,Bb,Db),!.


/* T- */
prove_phase2(S,U,Lt,K,Bb,Db) :- select([X,neg ti C],S,S1),
                prove_phase2([[X,neg C]|S1],U,Lt,K,Bb,Db),!,
                prove_phase2([[X,neg box neg C]|S1],U,Lt,K,Bb,Db),!.

/* cut */
prove_phase2(S,U,Lt,K,Bb,Db) :- member(X,Db),
                        member(C,Lt),
                        \+member([X,neg box neg C],S), 
			 \+member([X,box neg C],S),!,
                        prove_phase2([[X,box neg C]|S],U,Lt,K,Bb,Db),!,
                        prove_phase2([[X,neg box neg C]|S],U,Lt,K,Bb,Db),!.


/* exists + */
prove_phase2(S,U,Lt,K,Bb,Db) :- select([X,ex R in C],S,S1),
                        prove_phase2RecE(S1,U,Lt,K,Bb,Db,X,R,C,Db).


/* for each - */
prove_phase2(S,U,Lt,K,Bb,Db) :- select([X,neg fe R in C],S,S1),
                        prove_phase2RecF(S1,U,Lt,K,Bb,Db,X,R,C,Db).




/* box - */
prove_phase2(S,U,Lt,K,Bb,Db) :-member([X,neg box neg C],S),
			member([X,neg box neg C],Bb),
                        extractBox(X,S,Sm),
		        \+uncheckedSideCondition(X,S,C,Sm),!, 
			select([X,neg box neg C],K,K1),
                        extractBox(X,S,Sm),!,
                        prove_phase2RecB(S,U,Lt,K1,Bb,Db,X,C,Sm,Db),!.





/* recursive box- */
prove_phase2RecB(_,_,_,_,_,_,_,_,_,[]) :-!.
prove_phase2RecB(S,U,Lt,K,Bb,Db,X,C,Sm,[X|Tail]) :-!,
		        prove_phase2RecB(S,U,Lt,K,Bb,Db,X,C,Sm,Tail).
prove_phase2RecB(S,U,Lt,K,Bb,Db,X,C,Sm,[V|Tail]) :- 
                        genSmList(V,Sm,Smv),!,
                        append([[V,C]|[[V,box neg C]|S]],Smv,S3),!,
                        prove_phase2(S3,U,Lt,K,Bb,Db),!,
                        prove_phase2RecB(S,U,Lt,K,Bb,Db,X,C,Sm,Tail),!.

/* recursive ex+ */
prove_phase2RecE(_,_,_,_,_,_,_,_,_,[]) :-!.
prove_phase2RecE(S,U,Lt,K,Bb,Db,X,R,C,[X|Tail]) :-!,
							prove_phase2RecE(S,U,Lt,K,Bb,Db,X,R,C,Tail).
prove_phase2RecE(S,U,Lt,K,Bb,Db,X,R,C,[V|Tail]) :- 
                        prove_phase2([[X,R,V]|[[V,C]|S]],U,Lt,K,Bb,Db),!,
                        prove_phase2RecE(S,U,Lt,K,Bb,Db,X,R,C,Tail),!.

/* recursive fe- */
prove_phase2RecF(_,_,_,_,_,_,_,_,_,[]) :-!. 
prove_phase2RecF(S,U,Lt,K,Bb,Db,X,R,C,[X|Tail]) :-!,
						   prove_phase2RecF(S,U,Lt,K,Bb,Db,X,R,C,Tail).
prove_phase2RecF(S,U,Lt,K,Bb,Db,X,R,C,[V|Tail]) :- 
                        prove_phase2([[X,R,V]|[[V,neg C]|S]],U,Lt,K,Bb,Db),!,
                        prove_phase2RecF(S,U,Lt,K,Bb,Db,X,R,C,Tail),!.