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

:- use_module(library(lists)).
:- use_module(operators).
:- use_module(helpers).
:- use_module(min).
:- use_module(library(random)).
:- use_module(library(timeout)).

generateTBox(0,_,_,[]):-!.
generateTBox(Size,Depth,Concepts,[F|Tail]):-
  random(1,3,Type),
  generateConcept(Concepts,Depth,C),
  generateConcept(Concepts,Depth,D),
  generateInclusion(Type,C,D,F),  
  Size1 is Size-1,
  generateTBox(Size1,Depth,Concepts,Tail).

generateInclusion(1,C,D,C inc D):-!.
generateInclusion(2,C,D,ti C inc D):-!.

generateConcept(Atoms,Depth,Concept):-
  random(0,7,Type),
  buildConcept(Atoms,Depth,Type,Concept).

buildConcept(Atoms,_,0,P):-!,
  length(Atoms,L),
  random(1,L,Who),
  nth(Who,Atoms,P).
buildConcept(Atoms,0,_,P):-!,
  length(Atoms,L),
  random(1,L,Who),
  nth(Who,Atoms,P).
buildConcept(Atoms,Depth,1,C and D):-!,
  Depth1 is Depth-1,
  generateConcept(Atoms,Depth1,C),
  generateConcept(Atoms,Depth1,D).
buildConcept(Atoms,Depth,2,C or D):-!,
  Depth1 is Depth-1,
  generateConcept(Atoms,Depth1,C),
  generateConcept(Atoms,Depth1,D).
buildConcept(Atoms,Depth,3,neg C):-!,
  Depth1 is Depth-1,
  generateConcept(Atoms,Depth1,C).
buildConcept(_,_,4,top):-!.
buildConcept(Atoms,Depth,5,ex r in C):-!,
  Depth1 is Depth-1,
  generateConcept(Atoms,Depth1,C).
buildConcept(Atoms,Depth,6,fe r in C):-!,
  Depth1 is Depth-1,
  generateConcept(Atoms,Depth1,C).


  
nth(1,[H|_],H):-!.
nth(N,[_|Tail],Element):-N1 is N-1,nth(N1,Tail,Element).

generateABox(0,_,_,_,[]):-!.
generateABox(Size,Depth,Labels,Concepts,[[[x+N,N],C]|Tail]):-!,
  generateConcept(Concepts,Depth,C),
  random(1,Labels,N),
  Size1 is Size-1,
  generateABox(Size1,Depth,Labels,Concepts,Tail).


test(NumberOfTests,TimeOut,SizeAbox,SizeTBox,NumberOfAtoms,Depth,NamedIndividuals):-
  retractall(successi(_)),
  retractall(fallimenti(_)),
  retractall(to(_)),
  asserta(successi(0)),
  asserta(fallimenti(0)),
  asserta(to(0)),
  genAtomicConcepts(NumberOfAtoms,AtomicConcepts),!,
  generateABox(SizeAbox,Depth,NamedIndividuals,AtomicConcepts,ABox),!,
  generateTBox(SizeTBox,Depth,AtomicConcepts,TBox),!,
  testOnQuery(NumberOfTests,ABox,TBox,TimeOut,AtomicConcepts,Depth,NamedIndividuals),!,
  printresults.

testOnQuery(0,_,_,_,_,_,_):-!.
testOnQuery(NumberOfTests,ABox,TBox,TimeOut,AtomicConcepts,Depth,NamedIndividuals):-
  buildUSet(TBox,U),
  randomQuery(AtomicConcepts,Depth,NamedIndividuals,Query),
  attempt(TimeOut,ABox,U,Query),
  ToDo is NumberOfTests-1,
  testOnQuery(ToDo,ABox,TBox,TimeOut,AtomicConcepts,Depth,NamedIndividuals).

randomQuery(AtomicConcepts,Depth,NamedIndividuals,Query):-
  random(1,3,Type),!,
  auxRandQuery(AtomicConcepts,Depth,NamedIndividuals,Query,Type),!.

auxRandQuery(AtomicConcepts,Depth,_,Query,1):-
  % Type 1: query=inclusion C inc D
  random(1,3,Type),
  generateConcept(AtomicConcepts,Depth,C),!,
  generateConcept(AtomicConcepts,Depth,D),!,
  generateInclusion(Type,C,D,Query).  
auxRandQuery(AtomicConcepts,Depth,NamedIndividuals,[[x+Who,Who],C],2):-
  % Type 2: query=ABox assertion C(a)
  generateConcept(AtomicConcepts,Depth,C),!,
  random(1,NamedIndividuals,Who).

genAtomicConcepts(0,[]):-!.
genAtomicConcepts(N,[c+N|Tail]):-N1 is N-1,genAtomicConcepts(N1,Tail).

buildUSet([],[]):-!.
buildUSet([C inc D|Tail],[[[C inc D],[]]|ResTail]):-!,buildUSet(Tail,ResTail).

attempt(TimeOut,ABox,U,Query):-
  time_out(prove(ABox,U,Query,_),TimeOut,Res),!,
  manipulate(Res).
attempt(_,_,_,_):-!,
  fallimenti(N),
  N1 is N+1,
  retractall(fallimenti(_)),
  asserta(fallimenti(N1)).

manipulate(success):-!,
  successi(N),
  N1 is N+1,
  retractall(successi(_)),
  asserta(successi(N1)).
manipulate(time_out):-!,
  to(N),
  N1 is N+1,
  retractall(to(_)),
  asserta(to(N1)).

printresults:-
  successi(S),fallimenti(F),to(TO),
  write('\n ********* RISULTATI *****************\n'),
  write('YES: '),write(S),write('\n'),
  write('NO: '),write(F),write('\n'),
  write('Time outs: '),write(TO),write('\n********************************\n'),!.