% *** query with the goal with VisitedNodes

% the prove depth is a bit small;

/* This covering file has two parts: choosing and output the final.
To use this file -- cover(PosList,NegList,[],FinalT).
*/

set(evDepth,5).

/*********************Inconsistent Check ************************/
% T is discarded once cover one negative example
coverNeg(NegList):-
	member(NegEI,NegList),
	ex(NegEI,E,0), %%write('one Negative example'),%write(NegEI),
	set(evDepth,DepthLimit),
	depth_bound_call(user:E, DepthLimit).

checkIntegrityConstraint:-
	set(evDepth,DepthLimit),
	%DepthLimit=2,
	depth_bound_call(user:integrityConstraint, DepthLimit).

	

/*********************Integrity Constraint ************************/


/***************Count Coverage (RELATIVE) *********/
/*% only check those from check list
unCoverRecord([],[]).
unCoverRecord([Index|CheckList],NUnCoverList):-
	%write('%%%%% covering'),write(Index),
	
	ex(Index,concentration(MID,Change),PosNegSign),% ***


	%%write('%%%%% covering'),
	set(evDepth,DepthLimit),
	%%write('%%%%% covering'),

	(depth_bound_call(user:concentration(MID,Change,Time,[MID]), DepthLimit)->
		NUnCoverList=UnCoverList;
		NUnCoverList=[Index|UnCoverList]
	),

	%%write('%%%%% finish this example'),nl,
	unCoverRecord(CheckList,UnCoverList).
*/





unCoverRecord([],[]).
unCoverRecord([Index|CheckList],NUnCoverList):-
	write('%%%%% covering'),write(Index),
	ex(Index,E,PosNegSign),
	(integer(Index)->
		((set(etoB,yes))->
			retract(ex(Index,E,PosNegSign)); % *** you can't take ex(, since they doesn't exist
			Flag=0	% Flag is for later added
		);  % not necessarily positive -- used for count FalseNeg
		E=Index,Flag=0 % secondary examples
	),
	%%write(E),

	%%write('%%%%% covering'),
	set(evDepth,DepthLimit),
	%%write('%%%%% covering'),
	
	(queriedE(E,AugumentedE)->
		  QueriedE=AugumentedE; % do nothing
		  QueriedE=E),

	(depth_bound_call(user:QueriedE, DepthLimit)->
		NUnCoverList=UnCoverList;%write('succeed')
		NUnCoverList=[Index|UnCoverList]
	),
	(Flag==0 ->	
		Foo2=1;	% do nothing
		assert(ex(Index,E,PosNegSign)) % ***
	),
	write('%%%%% finish this example'),nl,
	unCoverRecord(CheckList,UnCoverList).





/***************SCORE ********************/
% Sequentially compute each T: add T, score it, remove T0

%score(TI,Coverage,Score):-
%	descriptionLength(TI,) % please note that you don't have ClaID to 


score(TI,Coverage,Score):-
	(set(specificScore,yes)->
		scoreSpecific(TI,Coverage,Score);
		score0(TI,Coverage,Score)
	).
	

score0(TI,Coverage,Score):-
	tCompScore0(TI,TComplex),
	Score is TComplex+Coverage.

tCompScore0([],0).
tCompScore0([ClaI|TI],NTScore):-
	tCompScore0(TI,TScore), 
	claInterpreter(ClaI,Cla),
	length(Cla,HL),
	NTScore is TScore+HL.


% score = TComplex+NumUnCover(Overall)
% {PreSocre,PreUnCover,T}	
% {Score,UnCover,NewTSoFar,T}

	
debug(X).

scoreTs(PosList,NegList,TSoFar,[],[]).
scoreTs(PosList,NegList,TSoFar,[T|Ts],NScoredTs):-

	scoreTs(PosList,NegList,TSoFar,Ts,ScoredTs),
	debug(1),
	%write('^^^Start scoring this T: Clause under inspection'), write(T),	nl,
	addTI(TSoFar,[],RefTSoFar),%write('TSoFar'),%write(TSoFar),%write('&&&'),
	addTI(T,RefTSoFar,RefAllT),%write('???Problem here'),%write(RefAllT),nl,
		
	debug(2),
	((coverNeg(NegList);once(checkIntegrityConstraint))->	% expensive to check redundancy, so remove as much as possible at this stage
		%write('---inconsistent---'),nl,
		removeRefT(RefAllT,UselessT),
		NScoredTs=ScoredTs;

		%write('----Fine'),nl,
		%write('$$$$Check Redundant'),
		RefAllT=NewRefAllT, %removeRedundant(RefAllT,NewRefAllT),
		%write('$$$$Finish'),nl,
		unCoverRecord(PosList,UnCover), %write('for this example'),%write(UnCover),nl,
		length(UnCover,K),

		removeRefT(NewRefAllT,NewAllT),

		score(NewAllT,K,Score),		
		

		NScoredTs=[{Score,UnCover,NewAllT,T}|ScoredTs], % T itself is useless in the next gene--but to debug increamental
		write('')%write('Finish this score'),%write({Score,UnCover,NewAllT,T}),nl
	).
	

/*************** START *******************/

cover([],_,FinalT,FinalT). % All Cover
%cover(EIs,_,FinalT,FinalT):-
%	length(EIs, RemainedNum),RemainedNum < 50,!. % only 100 remained

cover([EI|UnCover],NegList,TSoFar,FinalT):-
	%multiE(DepthLimit,EI,Ts),
	singleE(EI,Ts),
%%write('@@@@@@@Input for evaluation'), %write(UnCover),nl,%write(NegList),nl,nl,
write(EI),write('__________Start Scoring those for '),nl,
%evOneGen(Ts,TSoFar,UnCover,NegList,{NUnCover,NewTSoFar}),
	(Ts=[] ->
		  NUnCover=UnCover,NewTSoFar=TSoFar; %,nl,write('^&^&^&^& This example derives no Examples'),write(EI);
		  evOneGen(Ts,TSoFar,UnCover,NegList,{NUnCover,NewTSoFar})
	),
	cover(NUnCover,NegList,NewTSoFar,FinalT).



evOneGen(Ts,TSoFar,PosList,NegList,{UnCovered,NewTSoFar}):-
	scoreTs(PosList,NegList,TSoFar,Ts,ScoredTs),%write('^&^&^&^& finish scoring'),nl,

%sort(ScoredTs,[{Min,UnCovered,NewTSoFar,BestT}|RestTs]),
%%write('best for this examples is '),nl,%write({Min,UnCovered,NewTSoFar,BestT}),
%%write('?2'),
	sort(ScoredTs,SortedTs),print_list(SortedTs),
	
	(SortedTs==[] ->
		  write('nothing remains ');
		  Foo=0
	),

	%SortedTs=[{Score,UnCovered,NewTSoFar,ChosenT}|Rest],%write({Score,UnCovered,NewTSoFar,ChosenT}),nl,

	%minSets(SortedTs,MinSet),
	%first5(SortedTs,MinSet),
	%print_list(MinSet),
	%print_list([{Score,UnCovered,NewTSoFar,ChosenT}|Rest]),
	member({Score,UnCovered,NewTSoFar,ChosenT},SortedTs).

	%addT(NewTSoFar,TRef),
	%%print_list([{Min,UnCovered,NewTSoFar,BestT}|RestTs]),