Random$
Obtain a random value
Example:
(random$ 10 state) ==> (mv 7 <state>)
(Random$ limit state), where limit is a positive integer, returns
a random non-negative integer together with a new state. Logically,
it simply returns the first element of a list that is a field of the ACL2
state, called the acl2-oracle (see read-ACL2-oracle),
together with the new state resulting from removing that element from that
list. (Except, if that element is not in range as specified above, then 0 is
returned.) However, random$ actually invokes a Common Lisp function to
choose the integer returned. Quoting from the Common Lisp HyperSpec(TM), http://www.lispworks.com/documentation/HyperSpec/Front:
``An approximately uniform choice distribution is used... each of the
possible results occurs with (approximate) probability 1/limit.''
Consider enabling rules natp-random$ and random$-linear if you
want to reason about random$.
Function: random$
(defun random$ (limit state)
(declare (type (integer 1 *) limit)
(xargs :stobjs state))
(mv-let (erp val state)
(read-acl2-oracle state)
(mv (cond ((and (null erp)
(natp val)
(< val limit))
val)
(t 0))
state)))Subtopics
- Seed-random$
- Influence the random numbers produced by random$.
- Random-list-aux
- Add random numbers onto an accumulator.
- Random$-lemmas
- Lemmas about random$ available in the system/random book.
- Random-list
- Generate a list of random numbers in [0, limit).
