Symbolic simulation in ACL2
Robert S. Boyer, Warren A. Hunt · 2009
We have created an experimental extension to ACL2 that provides a means to symbolically evaluate ACL2 expressions. This modified implementation can be used to compute the 'general' application of an ACL2 function to generalized data. In particular, we use uBDDs to represent functions from Boolean variables to finite sets of ACL2 objects, and for guard-checked ACL2 functions we can automatically create corresponding generalized functions to operate on such generalized data.