POR

parallel, Boolean version of or
Major Section:  PARALLELISM

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