Por
Parallel, Boolean version of or
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:
(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 >= 0 and each argi and expr are arbitrary terms.
Por evaluates its arguments in parallel. It returns a Boolean result:
t if any argument evaluates to non-nil, else nil. Note that
while or returns the first non-nil value from evaluating its
arguments left-to-right (if any such value is not nil) por always
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 por and 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
property of pand. In particular, guards generated from calls of
por may not assume for an argument that the preceding arguments evaluated
to nil.
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.
