Major Section: PARALLEL-PROGRAMMING
This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism.
Example Forms: (por (subsetp-equal x y) (subsetp-equal y x)) (por (declare (granularity (and (> (length x) 500) (> (length y) 500)))) (subsetp-equal x y) (subsetp-equal y x))
General Form: (por (declare (granularity expr)) ; optional granularity declaration arg1 ... argN)where
N >= 0and each
exprare arbitrary terms.
Por evaluates its arguments in parallel. It returns a Boolean result:
t if any argument evaluates to non-
nil. Note that
or returns the first non-
nil value from evaluating its
arguments left-to-right (if any such value is not
returns a Boolean result, in support of efficiency (see early-termination)
in light of the nondeterministic order in which argument values are returned.
Another difference between
or is that for a call of
por, even if the an argument's value is not
nil, a subsequent
argument may be evaluated. See pand for a discussion of the analogous
pand. In particular, guards generated from calls of
por may not assume for an argument that the preceding arguments evaluated
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
por can offer more efficiency than
or by avoiding evaluation of some of its arguments.