Availability:built-in

**call_with_depth_limit**(

`:Goal, +Limit, -Result`)

`Goal`can be proven without recursion deeper than

`Limit`levels, call_with_depth_limit/3 succeeds, binding

`Result`to the deepest recursion level used during the proof. Otherwise,

`Result`is unified with

`depth_limit_exceeded`

if the limit was exceeded during the proof, or the entire predicate
fails if `Goal`fails without exceeding

`Limit`.

The depth limit is guarded by the internal machinery. This may differ from the depth computed based on a theoretical model. For example, true/0 is translated into an inline virtual machine instruction. Also, repeat/0 is not implemented as below, but as a non-deterministic foreign predicate.

repeat. repeat :- repeat.

As a result, call_with_depth_limit/3 may still loop infinitely on programs that should theoretically finish in finite time. This problem can be cured by using Prolog equivalents to such built-in predicates.

This predicate may be used for theorem provers to realise techniques
like *iterative deepening*. See also call_with_inference_limit/3.
It was implemented after discussion with Steve Moyle
smoyle@ermine.ox.ac.uk.