/*
solve(A,D,Overflow) :-
A has a proof tree of depth less than D and Overflow equals
no_overflow,or A has a branch in the computation tree longer
than D, and Overflow contains a list of its first D elements.
*/
solve(true,D,no_overflow) :- !.
solve(A,0,overflow([])).
solve((A,B),D,Overflow) :- !,
D > 0,
solve(A,D,OverflowA),
solve_conjunction(OverflowA,B,D,Overflow).
solve(A,D,Overflow) :-
D > 0,
clause(A,B),
D1 is D - 1,
solve(B,D1,OverflowB),
return_overflow(OverflowB,A,Overflow).
solve(A,D,no_overflow) :-
D > 0,
system(A), A.
solve_conjunction(overflow(S),B,D,overflow(S)).
solve_conjunction(no_overflow,B,D,Overflow) :-
solve(B,D,Overflow).
return_overflow(no_overflow,A,no_overflow).
return_overflow(overflow(S),A,overflow([A|S])).
% Program 17.11 :A meta-interpreter detecting a stack overflow