Once we have a representation for symbolic objects, we can perform symbolic
executions on those objects. For instance, recall the symbolic number
p = (:g-integer true false A & B false)
We might symbolically add 1 to
q = (:g-integer false true A & B false)
which represents either 2 or 6. Suppose
r = (:g-integer A false true false)
which represents either 4 or 5. We might add
s = (:g-integer A true ~(A & B) (A & B) false)
whose value can be 6, 7, or 11.
The underlying algorithm GL uses for symbolic additions is just a ripple-carry addition on the Boolean expressions making up the bits of the two numbers. Performing a symbolic addition, then, means constructing new ubdds or aigs, depending on which mode is being used.
GL has built-in support for symbolically executing most ACL2 primitives.
Generally, this is done by cases on the types of the symbolic objects being
passed in as arguments. For instance, if we want to symbolically execute consp on
Beyond these primitives, GL provides what is essentially a McCarthy-style interpreter for symbolically executing terms. By default, it expands function definitions until it reaches primitives, with some special handling for if. For better performance, its interpretation scheme can be customized with more efficient definitions and other optimizations.