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.