% *** query with the goal with VisitedNodes

% main problem is ex0 where recognizable name is mapped to ID. those places signed with % ***
% 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,7).

/*********************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),
	(integer(Index)->
		ex(Index,concentration(MID,Change,Time),PosNegSign),ex0(Index,E0,PosNegSign),% *** query with E, while need to extract ex0(..)
		((set(etoB,yes),PosNegSign==1)->
			retract(ex0(Index,E0,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'),

	(depth_bound_call(user:concentration(MID,Change,Time,[MID]), DepthLimit)->
		NUnCoverList=UnCoverList;
		NUnCoverList=[Index|UnCoverList]
	),
	(Flag==0 ->	
		Foo2=1;	% do nothing
		assert(ex0(Index,E0,PosNegSign)) % ***
	),
	%%write('%%%%% finish this example'),nl,
	unCoverRecord(CheckList,UnCoverList).





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

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}
scoreTs(PosList,NegList,TSoFar,[],[]).
scoreTs(PosList,NegList,TSoFar,[T|Ts],NScoredTs):-

	scoreTs(PosList,NegList,TSoFar,Ts,ScoredTs),

(checklist(reactionStateContradictionCheck(TSoFar),T)-> % check consistence before scoring
	%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,
	%addTI_redundencyCheck(T,TSoFar,RefTSoFar,RefAllT),%write('???Problem here'),%write(RefAllT),nl,
	
	
	
	%nl,nl,%write(TSoFar), %write('ADDing '), %%print_list(T),nl,listing,
	
	
	((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'),
		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

	  )
	);
	nl,write('--------------------------haha, here is one postential inconsistent'), write(T),write(TSoFar),nl,
	NScoredTs=ScoredTs). % not consistence, so just remove that candidate T.
	

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

cover([],_,FinalT,FinalT). % All Cover
%cover(EIs,_,FinalT,FinalT):-
%	length(EIs, RemainedNum),RemainedNum < 50,!. % only 100 remained
cover([EI|UnCover],NegList,TSoFar,FinalT):-
	set(depthLimit,DepthLimit),
	%multiE(DepthLimit,EI,Ts),
	singleE(DepthLimit,EI,Ts),
%%write('@@@@@@@Input for evaluation'), %write(UnCover),nl,%write(NegList),nl,nl,
%%write('__________Start Scoring'),nl,
	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=[{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]),

	nl.



% Here is for beam search.
first5([A,B,C,D,E|R],[A,B,C,D,E]).

minSets([{Min,UnCovered,NewTSoFar,ChosenT}|Lists],[{Min,UnCovered,NewTSoFar,ChosenT}|Same]):-
	(once(append(Same,[{Score1,UnCovered1,NewTSoFar1,ChosenT1}|ListB],Lists),Score1\==Min),!;Same=[]). % find the first one that is not the same as Min