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 `and` terms can thus save some computation; roughly
speaking, the smaller the

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 `pand` call returns `pand`, we
can in principle attain a speedup factor greater than the number of available
cores.

The concept of early termination also applies to `por`, except that
early termination occurs when an argument evaluates to non-