Pand
Parallel, Boolean version of and
This documentation topic relates to the experimental
extension of ACL2 supporting parallel execution and proof; see parallelism, and see parallel-programming, which has a disclaimer.
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 >= 0 and each argi and expr are arbitrary terms.
Pand evaluates its arguments in parallel. It returns a Boolean
result: nil if any argument evaluates to nil, else t. Note
that pand always returns a Boolean result, even though and can
return a non-nil value other than t, namely the value of its last
argument. (A moment's reflection will make it clear that in order for por to parallelize efficiently, it needs to return a Boolean value; so
pand returns a Boolean value for consistency with por.)
Another difference between pand and 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 pand can execute
in parallel, causing ``hello world'' to be printed to the terminal. If
we had used and rather than pand, then since (equal (make-list
100000) nil) evaluates to nil, the above call of cw would 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 execution is enabled (see set-parallel-execution).
Note that unlike the case for and, the definition of pand does
not provide (consp x) as a guard to (car x) in the call of
pand below:
(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 pand were 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.
