How to optimize GL's symbolic simulations for faster or larger-scale proofs.

- Using different modes to solve the problem. Some modes vastly outperform others on particular problems and it is very easy to switch modes, so this is often a good first thing to try when you run into a performance problem.
- Decomposing difficult problems into easier subgoals. GL provides some support for case-splitting hard proofs, and in some cases this kind of decomposition can tremendously boost performance.
- Using other optimization techniques to make GL's symbolic execution strategy more efficient.

The scope of theorems GL can handle is directly impacted by its symbolic execution performance. It is actually quite easy to customize the way certain terms are interpreted, and this can sometimes provide important speedups.

GL's symbolic interpreter operates much like a basic Lisp interpreter. To symbolically interpret a function call, GL first eagerly interprets its arguments to obtain symbolic objects for the actuals. Then GL symbolically executes the function in one of three ways:

- As a special case, if the actuals evaluate to concrete objects, then GL may be able to stop symbolically executing and just call the actual ACL2 function on these arguments.
- For primitive ACL2 functions like +, consp, equal, and
for some defined functions like logand and ash where performance
is important, GL uses hand-written functions called
**symbolic counterparts**that can operate on symbolic objects. The advanced GL user can write new custom-symbolic-counterparts to speed up symbolic execution. - Otherwise, GL looks up the definition of the function, and recursively interprets its body in a new environment binding the formals to the symbolic actuals. The way a function is written can impact its symbolic execution performance; see redundant-recursion. It is easy to instruct GL to use more efficient, preferred-definitions for particular functions.

GL symbolically executes functions strictly according to the ACL2 logic and
does not consider guards. An important consequence is that when mbe is
used, GL's interpreter follows the

In the event that one is performing a very large decomposition proof (e.g.,
the theorem

- Term-level-reasoning
- GL's term-level proof support
- Def-gl-param-thm
- Prove a theorem using GL symbolic simulation with parametrized case-splitting.
- Case-splitting
- Modes
- GL modes allow you to control major aspects of how GL carries out its symbolic simulation and how it should solve Boolean formulas that arise during proofs.
- Memory-management
- Preferred-definitions
- Custom-symbolic-counterparts
- Redundant-recursion
- Alternate-definitions
- Specifying alternative definitions to be used for symbolic execution.
- Gl-param-thm
- Prove a theorem using GL symbolic simulation with parametrized case-splitting, without storing the theorem.