The advanced GL user can write custom symbolic counterparts to get better performance.
This is somewhat involved. Generally, such a function operates by cases on
what kinds of symbolic objects it has been given. Most of these cases are
easy; for instance, the symbolic counterpart for consp just returns
Once the counterpart has been defined, it must be proven sound with respect to the semantics of ACL2 and the symbolic object format. This is an ordinary ACL2 proof effort that requires some understanding of GL's implementation.
An example of a more sophisticated symbolic counterpart is an aig to