		Search-engine friendly clone of the ACL2 documentation.

Debugging

Performance-problems

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 :show-values nil. It may also be helpful to simply interrupt the computation and look at the Lisp backtrace, after executing

(set-debugger-enable t)

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 beginning in q-, which is the convention for BDD operators. In some cases, these performance problems may be solved by choosing a more efficient BDD order. But note that certain operations like multiplication are exponentially hard. If you run into these limits, you may need to refactor or decompose your problem into simpler sub-problems, e.g., with def-gl-param-thm.

There is one kind of BDD performance problem with a special solution. Suppose GL is asked to prove (equal spec impl) when this does not actually hold. Sometimes the symbolic objects for spec and impl can be created, but the BDD representing their equality is too large to fit in memory. The goal may then be restated with ACL2::always-equal instead of equal as the final comparison. Logically, always-equal is just equal. But always-equal has a custom symbolic counterpart that returns t when its arguments are equivalent, or else produces a symbolic object that captures just one counterexample and is indeterminate in all other cases.

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.