		Search-engine friendly clone of the ACL2 documentation.

Aig-random-sim

Init-random-state

Create a fast alist binding each variable to a random 60-bit natural.

Signature
(init-random-state vars state) → (mv fal state)

Definitions and Theorems

Function: init-random-state

(defun init-random-state (vars state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((__function__ 'init-random-state))
    (declare (ignorable __function__))
    (b* ((vars (list-fix vars))
         ((mv nums state)
          (n-random-60-bit-nats (length vars)
                                state)))
      (mv (make-fast-alist (pairlis$ vars nums))
          state))))

Theorem: state-p1-of-init-random-state

(defthm state-p1-of-init-random-state
  (implies (force (state-p1 state))
           (state-p1 (mv-nth 1 (init-random-state vars state)))))