:- discontiguous sIdx/2.
:- discontiguous sCov/2.
:- discontiguous aCov/2.

not_min_choice(R1) :- 
	sCov(R1,_), rule(R1,I1), sCov(R2,_), rule(R2,I2), I2<I1.
sChoice(R) :- sIdx(R,_), sCov(R,_), \+ not_min_choice(R), !.

sIdx(r0,0).
sCov(r0,(Top, Next)) :- 
	incomplete(_,Top), clear(Top), goal(Next,Top), clear(Next).
aCov(move(next,top), move(Next,Top)) :- sChoice(r0), sCov(r0, (Top, Next)).
													 
sIdx(r1,1).
sCov(r1,(Basis,Top,BadTop)) :- 
	incomplete(Basis,Top), \+ clear(Top), 
	above(BadTop,Top), clear(BadTop).
aCov(move(badTop,table),move(BadTop,table)) :- 
	sChoice(r1), sCov(r1,(_,_,BadTop)).
aCov(move(badTop,other),move(BadTop, Other)) :- 
	sChoice(r1), sCov(r1,(_,_,BadTop)), 
	clear(Other), \+ Other=BadTop, \+ Other=table.

sIdx(r2,2).
sCov(r2,(Top,BadTop)) :- 
	incomplete(_,Top), clear(Top), goal(Next,Top), 
	\+ clear(Next), above(BadTop,Next), clear(BadTop).
aCov(move(badTop,table),move(BadTop,table)) :- 
	sChoice(r2), sCov(r2,(_,BadTop)).
aCov(move(badTop,other),move(BadTop,Other)) :- 
	sChoice(r2), sCov(r2,(Top,BadTop)), 
	clear(Other), \+ Other=Top, \+ Other=BadTop, \+ Other=table.

sIdx(r3,3).
sCov(r3,(BadTop)) :- 
	\+ finalBasis(_), goal(_,Basis), \+ goal(Basis,_), 
	\+ clear(Basis), above(BadTop,Basis), clear(BadTop).
aCov(move(badTop,table),move(BadTop,table)) :- 
	sChoice(r3), sCov(r3,(BadTop)).
aCov(move(badTop,other),move(BadTop,Other)) :- 
	sChoice(r3), sCov(r3,(BadTop)), clear(Other), 
	\+ Other=BadTop, \+ Other=table.

sIdx(r4,4).
sCov(r4,(Basis)) :- 
	\+ finalBasis(_), goal(_, Basis), 
	\+ goal(Basis,_), clear(Basis).
aCov(move(basis,table),move(Basis,table)) :- 
	sChoice(r4), sCov(r4,(Basis)).

sIdx(true,1.0Inf).	
sCov(true,[]).

aCov(others,move(X,Y)) :- 
	clear(X), clear(Y), \+ aCov(move(_,_),move(X,Y)), 
	\+ on(X,Y), \+ X=Y, \+ X=table.