Early termination for pand and por.
This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism.
The evaluation of
If the above call of and is replaced by its parallel version,
pand, then there can be even more opportunity for skipping work. The
arguments to pand can be evaluated in parallel, in which case the
first such evaluation that returns with a value of
Consider the following functions that compute whether a tree is valid (see granularity for a discussion of the granularity form).
(defun valid-tip (x) (declare (xargs :guard t)) (or (eq x 'A) (eq x 'T) (eq x 'C) (eq x 'G))) (defun pvalid-tree (x depth) (declare (xargs :guard (natp depth))) (if (atom x) (valid-tip x) (pand (declare (granularity (< depth 10))) (pvalid-tree (car x) (1+ depth)) (pvalid-tree (cdr x) (1+ depth)))))
We would like to stop execution as soon as any tip is found to be invalid.
So, when computing the conjunction of terms by using pand, once one of
those terms evaluates to
The concept of early termination also applies to por, except that
early termination occurs when an argument evaluates to non-