PAND

parallel, Boolean version of and 
Major Section:  PARALLEL-PROGRAMMING

This documentation topic relates to the experimental extension of ACL2 supporting parallel execution 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 >= 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.