Major Section: PARALLELISM
This documentation topic relates to the experimental extension of ACL2 supporting parallel evaluation and proof; see parallelism.
Example Forms: (pand (subsetp-equal x y) (subsetp-equal y x)) (pand (declare (granularity (and (> (length x) 500) (> (length y) 500)))) (subsetp-equal x y) (subsetp-equal y x))
General Form: (pand (declare (granularity expr)) ; optional granularity declaration arg1 ... argN)where
N >= 0and each
exprare arbitrary terms.
Pand evaluates its arguments in parallel. It returns a Boolean result:
nil if any argument evaluates to
t. Note that
pand always returns a Boolean result, even though
and can return a
nil value other than
t, namely the value of its last argument.
(A moment's reflection will make it clear that in order for
parallelize efficiently, it needs to return a Boolean value; so
returns a Boolean value for consistency with
Another difference between
and is that for a call of
pand, even if an argument evaluates to
nil, a subsequent argument
may be evaluated. Consider the following example (where
cw prints a
string; see cw).
(defun bar () (pand (equal (make-list 100000) nil) ; evaluates to nil (cw "hello world~%")))When
(bar)is evaluated, the above arguments of
pandcan execute in parallel, causing ``
hello world'' to be printed to the terminal. If we had used
pand, then since
(equal (make-list 100000) nil)evaluates to
nil, the above call of
cwwould be avoided and no such printing would take place. Even with
pand, such printing might not take place, depending on resources, timing of thread creation, and whether or not parallel evaluation is enabled (see set-parallel-evaluation).
Note that unlike the case for
and, the definition of
pand does not
(consp x) as a guard to
(car x) in the call of
(defun h (x) (declare (xargs :guard t)) (pand (consp x) (equal (car x) 'foo)))As a result, guard verification will fail for the above definition. If
pandwere replaced by
and, then guard verification would succeed.
See parallelism-tutorial for another example. Also
see parallelism-at-the-top-level for restrictions on evaluating parallelism
primitives from within the ACL2 top-level loop. Finally
see early-termination to read how
pand can offer more efficiency than
and by avoiding evaluation of some of its arguments.