Any bit-blasting tool has capacity limitations. However, you may also run into cases where GL is performing poorly due to preventable issues. When GL seems to be running forever, it can be helpful to trace the symbolic interpreter to see which functions are causing the problem. To trace the symbolic interpreter, run
(gl::trace-gl-interp :show-values t)
Here, at each call of the symbolic interpreter, the term being interpreted
and the variable bindings are shown, but since symbolic objects may be too
large to print, any bindings that are not concrete are hidden. You can also
get a trace with no variable bindings using
In many cases, performance problems are due to BDDs growing too large. This
is likely the case if the interpreter appears to get stuck (not printing any
more trace output) and the backtrace contains a lot of functions with names
There is one kind of BDD performance problem with a special solution.
Suppose GL is asked to prove
Another possible problem is that the symbolic interpreter never gets stuck, but keeps opening up more and more functions. These problems might be due to redundant-recursion, which may be avoided by providing a more efficient preferred-definitions.