|
|
|---|
|
|
|
|---|
Specifying alternative definitions to be used for symbolic execution.
Sometimes the definition of some function is ill-suited for
automatic methods of symbolic execution. For example,
(integerp (* x (/ 2)))
and because currently multiplication by a non-integer is not supported in GL, this yields a G-APPLY form in most cases.
In this case and several others, one may instead provide an alternate definition for the function in question and use that as the basis for GL symbolic execution.
In the case of EVENP, the following theorem works as an alternate definition:
(defthm evenp-is-logbitp (equal (evenp x) (or (not (acl2-numberp x)) (and (integerp x) (equal (logbitp 0 x) nil)))) :rule-classes nil)
After proving this theorem, the following form sets this alternate definition as the one GL will use when symbolically interpreting EVENP:
(gl::set-preferred-def evenp evenp-is-logbitp)
This form produces one or more table events.