← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/centaur/misc/seed-random.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/centaur/misc/seed-random.lisp
29
29
; Original author: Jared Davis <jared@centtech.com>
30
30
 
31
31
(in-package "ACL2")
 
32
(include-book "xdoc/top" :dir :system)
 
33
(include-book "tools/include-raw" :dir :system)
 
34
 
 
35
(defxdoc seed-random$
 
36
  :parents (random$)
 
37
  :short "Influence the random numbers produced by @(see random$)."
 
38
  :long "<p>General form:</p>
 
39
 
 
40
@({
 
41
     (include-book \"centaur/misc/seed-random\" :dir :system)
 
42
     (seed-random name
 
43
                  [:freshp t/nil]  ;; default t
 
44
                  )
 
45
})
 
46
 
 
47
<p>Hypothetical example:</p>
 
48
 
 
49
@({
 
50
   (seed-random 'foo) ;; randomly seed the generator, name this seed 'foo
 
51
   (random$ 50 state) --> (mv 31 state)
 
52
   (random$ 50 state) --> (mv 49 state)
 
53
   (random$ 50 state) --> (mv 2 state)
 
54
   (random$ 50 state) --> (mv 23 state)
 
55
   (random$ 50 state) --> (mv 15 state)
 
56
 
 
57
   (seed-random 'foo) ;; return to the seed named 'foo
 
58
   (random$ 50 state) --> (mv 31 state)
 
59
   (random$ 50 state) --> (mv 49 state)
 
60
   (random$ 50 state) --> (mv 2 state)
 
61
 
 
62
   (seed-random 'bar :freshp nil) ;; copy current seed, name it 'bar
 
63
   (random$ 50 state) --> (mv 23 state)
 
64
   (random$ 50 state) --> (mv 15 state)
 
65
 
 
66
   (seed-random 'foo) ;; return to 'foo
 
67
   (random$ 50 state) --> (mv 31 state)
 
68
 
 
69
   (seed-random 'bar) ;; return to 'bar
 
70
   (random$ 50 state) --> (mv 23 state)
 
71
   (random$ 50 state) --> (mv 15 state)
 
72
})
 
73
 
 
74
<p>Logically, @('seed-random$') ignores its arguments and just returns
 
75
@('nil').  We leave it enabled and would think it odd to ever prove a theorem
 
76
about it.</p>
 
77
 
 
78
<p>Under the hood, @('seed-random$') influences the behavior of @(see random$).
 
79
Note that in its implementation, the ACL2 function @('(random$ limit state)')
 
80
basically just calls @('(random limit)') to produce its result.  To understand
 
81
@('seed-random$'), it is useful to recall some features of Common Lisp:</p>
 
82
 
 
83
<ul>
 
84
 
 
85
<li>A @('random-state') is an implementation-defined data type that is used by
 
86
the @('random') function to produce random numbers.</li>
 
87
 
 
88
<li>In particular, @('(random limit &optional random-state)') can use some
 
89
particular @('random-state') or, by default, uses whatever @('random-state') is
 
90
currently bound to the special variable @('*random-state*').</li>
 
91
 
 
92
<li>A fresh, \"randomly initialized\" @('random-state') can be produced with
 
93
@('(make-random-state t)').</li>
 
94
 
 
95
<li>The current @('*random-state*') can be copied with @('(make-random-state
 
96
nil)').</li>
 
97
 
 
98
</ul>
 
99
 
 
100
<p>So, what does @('seed-random$') do?</p>
 
101
 
 
102
<p>We maintain a hidden association list that maps names to random-states.
 
103
These names can be any ACL2 objects, but we typically use symbols.</p>
 
104
 
 
105
<p>When @('seed-random$') is called with a name that is already bound to some
 
106
state, we just restore @('*random-state*') to this state.  This effectively
 
107
resets the random number generator so that it produces the same random numbers
 
108
as before.</p>
 
109
 
 
110
<p>When @('seed-random$') is called with a name that has not been bound yet,
 
111
its behavior depends on the optional @('freshp') keyword-argument.</p>
 
112
 
 
113
<p>When @('freshp') is @('t') (the default), we construct a \"randomly
 
114
initialized\" @('random-state'), bind @('name') to it, and install it as
 
115
@('*random-state*').  In other words, when @('foo') has never been used as a
 
116
name before, @('(seed-random$ 'foo)') effectively initializes the random number
 
117
generator to a truly random state.</p>
 
118
 
 
119
<p>On the other hand, when @('freshp') is @('nil') we simply copy and name the
 
120
current @('*random-state*').  It appears that, at least on CCL, the
 
121
@('*random-state*') starts the same upon every invocation of ACL2.  Hence, if
 
122
you launch ACL2 and then immediately invoke</p>
 
123
 
 
124
@({
 
125
    (seed-random 'seed :freshp nil)
 
126
})
 
127
 
 
128
<p>you can obtain a sequence of random numbers that you can return to even
 
129
after restarting ACL2, and which can be returned to at any time during the
 
130
session by just calling @('(seed-random 'seed)').</p>")
32
131
 
33
132
(defun seed-random$-fn (name freshp)
34
133
  (declare (xargs :guard t)
36
135
  nil)
37
136
 
38
137
(defmacro seed-random$ (name &key (freshp 't))
39
 
  ":Doc-Section random$
40
 
Influence the random numbers produced by ~ilc[random$]~/
41
 
 
42
 
General form:
43
 
~bv[]
44
 
 (seed-random name
45
 
              [:freshp t/nil]  ;; default t
46
 
              )
47
 
~ev[]
48
 
 
49
 
Hypothetical example:
50
 
~bv[]
51
 
  (seed-random 'foo) ;; randomly seed the generator, name this seed 'foo
52
 
  (random$ 50 state) --> (mv 31 state)
53
 
  (random$ 50 state) --> (mv 49 state)
54
 
  (random$ 50 state) --> (mv 2 state)
55
 
  (random$ 50 state) --> (mv 23 state)
56
 
  (random$ 50 state) --> (mv 15 state)
57
 
 
58
 
  (seed-random 'foo) ;; return to the seed named 'foo
59
 
  (random$ 50 state) --> (mv 31 state)
60
 
  (random$ 50 state) --> (mv 49 state)
61
 
  (random$ 50 state) --> (mv 2 state)
62
 
 
63
 
  (seed-random 'bar :freshp nil) ;; copy current seed, name it 'bar
64
 
  (random$ 50 state) --> (mv 23 state)
65
 
  (random$ 50 state) --> (mv 15 state)
66
 
 
67
 
  (seed-random 'foo) ;; return to 'foo
68
 
  (random$ 50 state) --> (mv 31 state)
69
 
 
70
 
  (seed-random 'bar) ;; return to 'bar
71
 
  (random$ 50 state) --> (mv 23 state)
72
 
  (random$ 50 state) --> (mv 15 state)
73
 
~ev[]
74
 
 
75
 
Logically, ~c[seed-random$] ignores its arguments and just returns ~c[nil]; we
76
 
leave it enabled and would think it odd to ever prove a theorem about it.
77
 
 
78
 
Under the hood, ~c[seed-random$] influences the behavior of ~ilc[random$].
79
 
Note that in its implementation, the ACL2 function ~c[(random$ limit state)]
80
 
basically just calls ~c[(random limit)] to produce its result.
81
 
 
82
 
To understand ~c[seed-random$], it is useful to recall some features of Common
83
 
Lisp:
84
 
 
85
 
 - A ~c[random-state] is an implementation-defined data type that is used by
86
 
   the ~c[random] function to produce random numbers.
87
 
 
88
 
 - In particular, ~c[(random limit &optional random-state)] can use some
89
 
   particular ~c[random-state] or, by default, uses whatever ~c[random-state]
90
 
   is currently bound to the special variable ~c[*random-state*].
91
 
 
92
 
 - A fresh, \"randomly initialized\" ~c[random-state] can be produced with
93
 
   ~c[(make-random-state t)].
94
 
 
95
 
 - The current ~c[*random-state*] can be copied with
96
 
   ~c[(make-random-state nil)].
97
 
 
98
 
So, what does ~c[seed-random$] do?
99
 
 
100
 
We maintain a hidden association list that maps names to random-states.  These
101
 
names can be any ACL2 objects, but we typically use symbols.
102
 
 
103
 
When ~c[seed-random$] is called with a name that is already bound to some
104
 
state, we just restore ~c[*random-state*] to this state.  This effectively
105
 
resets the random number generator so that it produces the same random numbers
106
 
as before.
107
 
 
108
 
When ~c[seed-random$] is called with a name that has not been bound yet, its
109
 
behavior depends on the optional ~c[freshp] keyword-argument.
110
 
 
111
 
When ~c[freshp] is ~c[t] (the default), we construct a \"randomly initialized\"
112
 
~c[random-state], bind ~c[name] to it, and install it as ~c[*random-state*].
113
 
In other words, when ~c[foo] has never been used as a name before,
114
 
~c[(seed-random$ 'foo)] effectively initializes the random number generator to
115
 
a truly random state.
116
 
 
117
 
On the other hand, when ~c[freshp] is ~c[nil] we simply copy and name the
118
 
current ~c[*random-state*].  It appears that, at least on CCL, the
119
 
~c[*random-state*] starts the same upon every invocation of ACL2.  Hence, if
120
 
you launch ACL2 and then immediately invoke
121
 
~bv[]
122
 
 (seed-random 'seed :freshp nil)
123
 
~ev[]
124
 
you can obtain a sequence of random numbers that you can return to even
125
 
after restarting ACL2, and which can be returned to at any time during the
126
 
session by just calling ~c[(seed-random 'seed)].~/~/"
127
 
 
128
138
  `(seed-random$-fn ,name ,freshp))
129
139
 
130
140
(defttag seed-random$)
131
141
 
132
 
(progn!
133
 
 (set-raw-mode t)
134
 
 
135
 
 (defparameter *random-seeds* nil)
136
 
 
137
 
 (defun seed-random$-fn (name freshp)
138
 
   (let ((look (assoc-equal name *random-seeds*)))
139
 
     (cond (look
140
 
            ;(format t "Restoring *random-state* to ~a.~%" (cdr look))
141
 
            (setq *random-state* (make-random-state (cdr look))))
142
 
           (freshp
143
 
            (let* ((new-st (make-random-state t)))
144
 
              ;(format t "Fresh seed ~a: ~a.~%" name new-st)
145
 
              (setq *random-seeds* (acons name new-st *random-seeds*))
146
 
              (setq *random-state* (make-random-state new-st))))
147
 
           (t
148
 
            (let ((new-st (make-random-state nil)))
149
 
              ;(format t "Copy seed to ~a: ~a.~%" name new-st)
150
 
              (setq *random-seeds* (acons name new-st *random-seeds*))))))
151
 
   nil))
 
142
(include-raw "seed-random-raw.lsp")
152
143
 
153
144
 
154
145
;; Basic tests to make sure it works