1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
|
; Arithmetic-5 Library
; Written by Robert Krug
; Copyright/License:
; See the LICENSE file at the top level of the arithmetic-5 library.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; default-hint.lisp
;;;
;;; This book contains the definition of several default hints we will
;;; be using to control nonlinear arithmetic.
;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package "ACL2")
(include-book "dynamic-e-d")
; Matt K. mod, Jan. 2019: The following is needed for the #+acl2-devel build,
; since nonlinearp-default-hint defined below is a :logic mode function that
; calls observation-cw.
(include-book "system/observation1-cw" :dir :system)
(table acl2-defaults-table :state-ok t)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; When things have stabilized under simplification, enable non-linear
;;; arithmetic for one round (goal being simplified) only.
(defun nonlinearp-default-hint (stable-under-simplificationp hist pspv)
; Guard change for tau after ACL2 Version 5.0 by J Moore:
; The hideous guard below is just the expected guard for
; (access rewrite-constant
; (access prove-spec-var pspv :rewrite-constant)
; :nonlinearp)
; where, by ``expected,'' we mean to exclude the pathological cases allowing
; car and cdr to be applied to nil. Unfortuantely, the guard must be changed
; every time the locations of the two fields change in their respective
; defrecs. To get it, translate the access expression above and then write a
; consp of every subterm but the top-most. In addition, you must also change
; the guard on the definition of this function where it is found -- twice! --
; in books/hints/basic-tests.lisp.
(declare
(xargs
:guard
(and (consp pspv)
(consp (car pspv))
(consp (car (car pspv)))
(consp (cdr (car (car pspv))))
(consp (cdr (cdr (car (car pspv)))))
(consp (cdr (cdr (cdr (car (car pspv))))))
(consp (cdr (cdr (cdr (cdr (car (car pspv)))))))
(consp (cdr (cdr (cdr (cdr (cdr (car (car pspv))))))))
(consp (cdr (cdr (cdr (cdr (cdr (cdr (car (car pspv)))))))))
(consp (car (cdr (cdr (cdr (cdr (cdr (cdr (car (car pspv)))))))))))))
(cond (stable-under-simplificationp
(if (not (access rewrite-constant
(access prove-spec-var pspv :rewrite-constant)
:nonlinearp))
(prog2$
(observation-cw
'nonlinearp-default-hint
"We now enable non-linear arithmetic.")
'(:computed-hint-replacement t
:nonlinearp t))
nil))
((access rewrite-constant
(access prove-spec-var pspv :rewrite-constant)
:nonlinearp)
(if (and (consp hist)
(consp (car hist))
;; Without this, we would loop forever. But
;; whenever I try to write an explanation, I get
;; confused about why it works. I stumbled across
;; this by trial and error and observing the output
;; of tracing. Some day I should figure out what I
;; am doing.
(not (equal (caar hist) 'SETTLED-DOWN-CLAUSE)))
(prog2$
(observation-cw
'nonlinearp-default-hint
"We now disable non-linear arithmetic.")
'(:computed-hint-replacement t
:nonlinearp nil))
nil))
(t
nil)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; I should document this better.
;;; Note: Consider leaving prefer-positive-exponents enabled.
;;; But, how do I ensure that this is not undone by some user-given
;;; :in-theory hint?
(defun arithmetic-default-hint (stable-under-simplificationp hist last-hint-used)
; (declare (xargs :guard (and (consp pspv)
; (consp (car pspv))
; (consp (caar pspv))
; (consp (cdaar pspv))
; (consp (car (cdaar pspv)))
; (consp (caar (cdaar pspv)))
; (consp (cdaar (cdaar pspv)))
; (alistp (cddaar (cdaar pspv))))))
(declare (xargs :mode :program))
(cond (stable-under-simplificationp
(cond ((equal last-hint-used nil)
(prog2$
(observation-cw
'arithmetic-default-hint
"We now enable prefer-positive-exponents.")
(let ((e/d '(((:REWRITE prefer-positive-exponents-scatter-exponents-equal)
(:REWRITE prefer-positive-exponents-scatter-exponents-<)
(:rewrite PREFER-POSITIVE-EXPONENTS-SCATTER-EXPONENTS-<-2)
(:REWRITE |(expt x (+ m n))|)
(:REWRITE |(expt x (+ m n)) non-zero (+ m n)|)
(:REWRITE |(expt x (+ m n)) non-zero x|)
;;(:REWRITE |(expt x (+ m n)) non-pos m and n|)
;;(:REWRITE |(expt x (+ m n))) non-neg m and n|)
(:REWRITE normalize-factors-scatter-exponents)
(:REWRITE simplify-products-scatter-exponents-equal)
(:REWRITE simplify-products-scatter-exponents-<))
((:REWRITE normalize-factors-gather-exponents)
(:REWRITE simplify-products-gather-exponents-equal)
(:REWRITE simplify-products-gather-exponents-<)))))
`(:computed-hint-replacement ((arithmetic-default-hint
stable-under-simplificationp
hist
'prefer-positive-addends))
;; I am surprised that a quote
;; is not needed here, i.e.,
;; :dynamic-e/d ',e/d
:dynamic-e/d ,e/d
:nonlinearp nil))))
((equal last-hint-used 'prefer-positive-addends)
(prog2$
(observation-cw
'arithmetic-default-hint
"We now enable non-linear arithmetic.")
`(:computed-hint-replacement ((arithmetic-default-hint
stable-under-simplificationp
hist 'non-linear-arithmetic))
:nonlinearp t)))
(t
nil)))
((and (equal last-hint-used 'non-linear-arithmetic)
(consp hist)
(consp (car hist))
(not (equal (caar hist) 'SETTLED-DOWN-CLAUSE)))
(prog2$
(observation-cw
'arithmetic-default-hint
"We now disable non-linear arithmetic and return to the earlier ~
enabled theory.")
(let ((e/d '(((:REWRITE normalize-factors-gather-exponents)
(:REWRITE simplify-products-gather-exponents-equal)
(:REWRITE simplify-products-gather-exponents-<))
((:REWRITE prefer-positive-exponents-scatter-exponents-equal)
(:REWRITE prefer-positive-exponents-scatter-exponents-<)
(:rewrite PREFER-POSITIVE-EXPONENTS-SCATTER-EXPONENTS-<-2)
(:REWRITE |(expt x (+ m n))|)
(:REWRITE |(expt x (+ m n)) non-zero (+ m n)|)
(:REWRITE |(expt x (+ m n)) non-zero x|)
;;(:REWRITE |(expt x (+ m n)) non-pos m and n|)
;;(:REWRITE |(expt x (+ m n))) non-neg m and n|)
(:REWRITE normalize-factors-scatter-exponents)
(:REWRITE simplify-products-scatter-exponents-equal)
(:REWRITE simplify-products-scatter-exponents-<)))))
`(:computed-hint-replacement ((arithmetic-default-hint
stable-under-simplificationp
hist nil))
;; I am surprised that a quote
;; is not needed here, i.e.,
;; :dynamic-e/d ',e/d
:dynamic-e/d ,e/d
:nonlinearp nil))))
(t
nil)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; I would like to experiment with :or hints. But I cannot use
;;; :computed-hint-replacement within an :or hint, so I need to use
;;; the same replacement on both branches. Therefore, I need to keep
;;; track of where I am some other way than passing around extra
;;; flags. Luckily, the goal spec gives it away.
(defun first-inductive-subgoal-p (id)
(declare (xargs :guard (and (consp id)
(consp (cdr id)))))
(and (< 1 (len (car id))) ; We are inducting
(equal 1 (len (cadr id))) ; No splits
(equal 0 (cddr id))))
(defun branch-taken1 (x ans)
(declare (xargs :guard (true-listp x)))
(cond ((endp x)
ans)
((equal (car x) 'D1)
(branch-taken1 (cdr x) 1))
((equal (car x) 'D2)
(branch-taken1 (cdr x) 2))
(t
(branch-taken1 (cdr x) ans))))
(defun branch-taken (id)
(declare (xargs :guard (and (consp id)
(consp (cdr id))
(true-listp (cadr id)))))
(branch-taken1 (cadr id) nil))
(defun nonlinearp-default-hint++ (id stable-under-simplificationp hist last-hint-used)
; (declare (xargs :guard (and (consp id)
; (consp (cdr id))
; (true-listp (cadr id))
; (consp pspv)
; (consp (car pspv))
; (consp (caar pspv))
; (consp (cdaar pspv))
; (consp (car (cdaar pspv)))
; (consp (caar (cdaar pspv)))
; (consp (cdaar (cdaar pspv)))
; (alistp (cddaar (cdaar pspv))))))
(declare (xargs :mode :program))
(cond ;;(first-inductive-subgoal-p id)
;;...)
(stable-under-simplificationp
(cond ((equal last-hint-used nil)
(prog2$
(observation-cw
'nonlinearp-default-hint++
"Branch.")
(let ((e/d '(((:REWRITE prefer-positive-exponents-scatter-exponents-equal)
(:REWRITE prefer-positive-exponents-scatter-exponents-<)
(:rewrite PREFER-POSITIVE-EXPONENTS-SCATTER-EXPONENTS-<-2)
(:REWRITE |(expt x (+ m n))|)
(:REWRITE |(expt x (+ m n)) non-zero (+ m n)|)
(:REWRITE |(expt x (+ m n)) non-zero x|)
;;(:REWRITE |(expt x (+ m n)) non-pos m and n|)
;;(:REWRITE |(expt x (+ m n))) non-neg m and n|)
(:REWRITE normalize-factors-scatter-exponents)
(:REWRITE simplify-products-scatter-exponents-equal)
(:REWRITE simplify-products-scatter-exponents-<))
((:REWRITE normalize-factors-gather-exponents)
(:REWRITE simplify-products-gather-exponents-equal)
(:REWRITE simplify-products-gather-exponents-<)))))
`(:computed-hint-replacement ((nonlinearp-default-hint++ id
stable-under-simplificationp
hist 'check-branch-taken))
;; I am surprised that a quote
;; is not needed here, i.e.,
;; :dynamic-e/d ',e/d
:or ((:dynamic-e/d ,e/d
:nonlinearp nil)
(:nonlinearp t))))))
((equal last-hint-used 'prefer-positive-exponents)
(prog2$
(observation-cw
'nonlinearp-default-hint++
"Prefer-positive-exponents.")
`(:computed-hint-replacement ((nonlinearp-default-hint++ id
stable-under-simplificationp
hist 'non-linear-arithmetic))
:nonlinearp t)))
((equal last-hint-used 'recycle)
(prog2$
(observation-cw
'nonlinearp-default-hint++
"Recycle.")
`(:computed-hint-replacement ((nonlinearp-default-hint++ id
stable-under-simplificationp
hist 'non-linear-arithmetic))
:nonlinearp t)))
(t
nil)))
((equal last-hint-used 'check-branch-taken)
(let ((branch-taken (branch-taken id)))
(cond ((equal branch-taken 2)
(prog2$
(observation-cw
'nonlinearp-default-hint++
"Check-branch-taken prefer-positive-exponents.")
`(:computed-hint-replacement ((nonlinearp-default-hint++ id
stable-under-simplificationp
hist 'prefer-positive-exponents))
:no-op t)))
((equal branch-taken 1)
(prog2$
(observation-cw
'nonlinearp-default-hint++
"Check-branch-taken non-linear-arithmetic.")
`(:computed-hint-replacement ((nonlinearp-default-hint++ id
stable-under-simplificationp
hist 'recycle))
:nonlinearp nil)))
(t
(cw "~%~%~ [Note: Computed hint error --- seemingly impossible ~
case reached in nonlinearp-default-hint++. Perhaps there ~
are two or more :OR hints interacting in unexpected ways. ~
We do not know what to do here, and so are defaulting to ~
doing nothing.~%~%")))))
((and (equal last-hint-used 'non-linear-arithmetic)
(consp hist)
(consp (car hist))
(not (equal (caar hist) 'SETTLED-DOWN-CLAUSE)))
(prog2$
(observation-cw
'nonlinearp-default-hint++
"Non-linear-arithmetic.")
`(:computed-hint-replacement ((nonlinearp-default-hint++ id
stable-under-simplificationp
hist 'recycle))
:nonlinearp nil)))
(t
nil)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; The rest of this file is not used at the present. I leave it here
;;; so I will not have to duplicate the work later, in case I ever decide
;;; to implement the strategies hinted at below.
#|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Pieces of code for implementing a computed hint to rewrite equalities
;;; between boolean expressions to iff, e.g.,
;;; (equal (pred-1 ... ...)
;;; (pred-2 ...))
;;; ==>
;;; (iff (pred-1 ... ...)
;;; (pred-2 ...))
(defun boolean-fn-p (fn ens wrld)
(declare (xargs :mode :program))
(ts-booleanp (fcons-term fn (formals fn wrld)) ens wrld))
(defun equality-between-booleans-present-in-term (term ens wrld)
(declare (xargs :mode :program))
(and (equal (fn-symb term) 'EQUAL)
(boolean-fn-p (car (cadr term)) ens wrld)
(boolean-fn-p (car (caddr term)) ens wrld)))
(defun equality-between-booleans-present-in-goal-1 (goal ens wrld)
(declare (xargs :mode :program))
(if (endp goal)
nil
(or (equality-between-booleans-present-in-term (car goal) ens wrld)
(equality-between-booleans-present-in-goal-1 (cdr goal) ens wrld))))
(defun equality-between-booleans-present-in-goal (goal pspv wrld)
(declare (xargs :mode :program))
(equality-between-booleans-present-in-goal-1 goal
(access rewrite-constant
(access prove-spec-var
pspv
:rewrite-constant)
:current-enabled-structure)
wrld))
|#
;; Put it up to eleven
|
