Gl-concretize
During GL symbolic execution, try to reduce a symbolic object to a
concrete one.
- Signature
(gl-concretize x) → *
(gl-concretize x), logically speaking, just returns x.
However, during symbolic simulation (in AIG mode), it tries to reduce x to
a concrete object by finding one object it could represent and trying to prove
that it is always equal to that object.
Definitions and Theorems
Function: gl-concretize$inline
(defun gl-concretize$inline (x)
(declare (xargs :guard t))
(let ((__function__ 'gl-concretize))
(declare (ignorable __function__))
x))
