Redundant-recursion
Here is a way to write a list-filtering function.
(defun filter1 (x)
(cond ((atom x)
nil)
((element-okp (car x)) ;; keep it
(cons (car x) (filter1 (cdr x))))
(t ;; skip it
(filter1 (cdr x)))))
This definition can be inefficient for symbolic execution. Suppose we are
symbolically executing filter1, and the element-okp check has
produced a symbolic object that can take both nil and non-nil values.
Then, we proceed by symbolically executing both the keep- and skip-branches,
and construct a :g-ite form for the result. Since we have to evaluate the
recursive call twice, this execution becomes exponential in the length of
x.
We can avoid this blow-up by consolidating the recursive calls, as
follows.
(defun filter2 (x)
(if (atom x)
nil
(let ((rest (filter2 (cdr x))))
(if (element-okp (car x))
(cons (car x) rest)
rest))))
Of course, filter1 is probably slightly better for concrete execution
since it has a tail call in at least some cases. If we do not want to change
the definition of filter1, we can simply tell GL to use the filter2
definition instead, as described in the next section.
