set(evDepth,10).

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

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):-
	(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.



scoreTs(PosList,NegList,TSoFar,[],[]):-!.
scoreTs(PosList,NegList,TSoFar,[HI|HIs],NScoredTs):-
	scoreTs(PosList,NegList,TSoFar,HIs,ScoredTs),!,
	hIndex(HI,T),
	addTI(TSoFar,[],RefTSoFar),
	addTI(T,RefTSoFar,RefAllT),
	((coverNeg(NegList);once(checkIntegrityConstraint))->	
		removeRefT(RefAllT,UselessT),
		NScoredTs=ScoredTs;
		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}-HI|ScoredTs]
	).

debug(X).

%set(shorterDistance_on_backtracking,no).

evOneIteration(HIs,TSoFar,PosList,NegList,NewHIs,{UnCovered,NewTSoFar}):-
	scoreTs(PosList,NegList,TSoFar,HIs,ScoredTs),
	sort(ScoredTs,SortedTs),%print_list(SortedTs),
(set(shorterDistance_on_backtracking,no)->
	append(PreScoredHIs,[{Score,UnCovered,NewTSoFar}-ChoosenHI|PostScoredHIs],SortedTs),
	append(PreScoredHIs,PostScoredHIs,RemainingScoredHIs);
	SortedTs=[{MinScore,MinUnCovered,MinNewTSoFar}-MinChoosenHI|Rest],
	getThresholdScore([MinScore],Rest,Threshold),
	top_member(Threshold,SortedTs,{Score,UnCovered,NewTSoFar}-ChoosenHI,RemainingScoredHIs)
),
	%write(ChoosenHI-{Score,UnCovered,NewTSoFar}),nl,
	updateNewHIs(UnCovered,RemainingScoredHIs,NewHIs).






top_member(Threshold,[Member_chosen|RestMembers],Member_chosen,RestMembers):-
	Member_chosen={Score,UnCovered,NewTSoFar}-ChoosenHI,
	Score=<Threshold.
top_member(Threshold,[OneMember|Members],Member_chosen,[OneMember|RestMembers]):-
	top_member(Threshold,Members,Member_chosen,RestMembers).

% restriction on the length of minScore
getThresholdScore([NewMinScore|MinScores],[],NewMinScore):- !.
getThresholdScore([NewMinScore|MinScores],[{Score,UnCovered,NewTSoFar}-ChoosenHI|Rest],NewMinScore):- length(MinScores,3),!.
getThresholdScore([MinScore|MinScores],[{MinScore,UnCovered,NewTSoFar}-ChoosenHI|Rest],Threshold):-
	!,getThresholdScore([MinScore|MinScores],Rest,Threshold).
getThresholdScore(MinScores,[{Score,UnCovered,NewTSoFar}-ChoosenHI|Rest],Threshold):-
	getThresholdScore([Score|MinScores],Rest,Threshold).

/*get2ndMinScore(MinScore,[{Score,UnCovered,NewTSoFar}-ChoosenHI|Rest],Score):- Score\==MinScore,!.
get2ndMinScore(MinScore,[{MinScore,UnCovered,NewTSoFar}-ChoosenHI|Rest],SecondMinScore):-
	get2ndMinScore(MinScore,Rest,SecondMinScore).*/

updateNewHIs(UnCovered,[],[]).
updateNewHIs(UnCovered,[{Score,UnCover,NewAllT}-HI|RemainingScoredHIs],NewHIs):-
	updateNewHIs(UnCovered,RemainingScoredHIs,HIs),
	(ord_subset(UnCovered,UnCover)->
		NewHIs=HIs;
		NewHIs=[HI|HIs]
	).
	
/*	maplist(updateNewHIs(UnCovered),RemainingScoredHIs,NewHIs0),
	flatten(NewHIs0,NewHIs).
updateNewHIs(UnCoveredEIs,{Score,UnCover,NewAllT}-HI,[]):-
	ord_subset(UnCoveredEIs,UnCover),!.
updateNewHIs(UnCoveredEIs,{Score,UnCover,NewAllT}-HI,HI).*/


global_covering([],_,HIs,FinalT,FinalT).
global_covering(UnCover,NegList,HIs,TSoFar,FinalT):-
	evOneIteration(HIs,TSoFar,UnCover,NegList,NewHIs,{NUnCover,NewTSoFar}),
	global_covering(NUnCover,NegList,NewHIs,NewTSoFar,FinalT).