← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2013/hardin-hardin/support/APSP.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/workshops/2013/hardin-hardin/support/APSP.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
; Added by Matt K.: This book has taken only a couple of minutes on a decent
 
4
; Linux system in 2013.  However, ACL2 built on GCL 2.6.8 and Mac OS 10.6
 
5
; cannot complete the certification without running exhausting STRING storage,
 
6
; probably because it contains a large stobj.  So we certify it only in
 
7
; "everything" regressions.
 
8
 
 
9
;;
 
10
;;  This data structure and algorithm implementation is based on
 
11
;;  "Accelerating Large Graph Algorithms on the GPU using CUDA" by
 
12
;;  Parwan Harish and P.J. Narayanan (2007); and 
 
13
;;  "Parallelizing Dijkstra's Single-Source Shortest-Path Algorithm" by 
 
14
;;  Dan Ginsburg (2011).
 
15
;;
 
16
;;  Implements All-Pairs Shortest Path (APSP) for Weighted Graphs
 
17
;;
 
18
 
 
19
(local (include-book "integer-listp-theorems"))
 
20
 
 
21
(defconst *MAX_VERTICES* 1000000)
 
22
(defconst *MAX_EDGES_PER_VERTEX* 10)
 
23
(defconst *MAX_EDGES* (* *MAX_VERTICES* *MAX_EDGES_PER_VERTEX*))
 
24
 
 
25
(defconst *MAX_SOURCES* 10)
 
26
 
 
27
(defconst *MAX_RESULTS* (* *MAX_VERTICES* *MAX_SOURCES*))
 
28
 
 
29
(defstobj GraphData
 
30
  ;; Vertex count
 
31
  (vertexCount :type (integer 0 1000000) :initially 1000000)
 
32
  (edgeCount :type (integer 0 10000000) :initially 10000000)
 
33
 
 
34
  ;; (V) This contains a pointer to the edge list for each vertex
 
35
  ;;  (vertexArray :type (array (integer 0 (1- *MAX_EDGES*)) (*MAX_VERTICES*)) 
 
36
  ;;               :initially 0)
 
37
  (vertexArray :type (array (integer 0 9999999) (*MAX_VERTICES*)) :initially 0)
 
38
 
 
39
  ;; (E) This contains pointers to the vertices that each edge is attached to
 
40
  ;;  (edgeArray :type (array (integer 0 (1- *MAX_VERTICES*)) (*MAX_EDGES*)) 
 
41
  ;;             :initially 0)
 
42
  (edgeArray :type (array (integer 0 999999) (*MAX_EDGES*)) :initially 0)
 
43
 
 
44
  ;; (W) Weight array
 
45
  (weightArray :type (array (integer 0 *) (*MAX_EDGES*)) :initially 0)
 
46
 
 
47
  ;; (M) Mask array
 
48
  (maskArray :type (array (integer 0 1) (*MAX_VERTICES*)) :initially 0)
 
49
 
 
50
  ;; (C) Cost array
 
51
  (costArray :type (array (integer 0 *) (*MAX_VERTICES*)) :initially 0)
 
52
 
 
53
  ;; (U) Updating cost array
 
54
  (updatingCostArray :type (array (integer 0 *) (*MAX_VERTICES*)) :initially 0)
 
55
 
 
56
  ;; (S) Source Vertices
 
57
  ;; (SourceVertexArray :type (array (integer 0 (1- *MAX_SOURCES*)) (*MAX_SOURCES*))
 
58
  ;;                    :initially 0)
 
59
  (SourceVertexArray :type (array (integer 0 9) (*MAX_SOURCES*)) :initially 0)
 
60
 
 
61
  ;; (R) Results
 
62
  (ResultArray :type (array (integer 0 *) (*MAX_RESULTS*)) :initially 0)
 
63
 
 
64
:inline t)
 
65
 
 
66
;; J Moore's let-inserter -- makes stobj-based code more readable
 
67
(defmacro seq (stobj &rest rst)
 
68
  (cond ((endp rst) stobj)
 
69
        ((endp (cdr rst)) (car rst))
 
70
        (t `(let ((,stobj ,(car rst)))
 
71
              (seq ,stobj ,@(cdr rst))))))
 
72
 
 
73
 
 
74
(defthm integerp-forward-to-rationalp--thm
 
75
  (implies (integerp x)
 
76
           (rationalp x))
 
77
  :rule-classes ((:forward-chaining :trigger-terms ((integerp x))) :rewrite))
 
78
 
 
79
(defthm integerp-forward-to-acl2-numberp--thm
 
80
  (implies (integerp x)
 
81
           (acl2-numberp x))
 
82
  :rule-classes ((:forward-chaining :trigger-terms ((integerp x))) :rewrite))
 
83
 
 
84
 
 
85
(defthm vertexArray-is-integer-listp--thm
 
86
  (implies (vertexArrayp x) 
 
87
           (integer-listp x)) 
 
88
  :rule-classes ((:forward-chaining :trigger-terms ((vertexArrayp x))) :rewrite))
 
89
 
 
90
(defthm edgeArray-is-integer-listp--thm
 
91
  (implies (edgeArrayp x)
 
92
           (integer-listp x))
 
93
  :rule-classes ((:forward-chaining :trigger-terms ((edgeArrayp x))) :rewrite))
 
94
 
 
95
(defthm weightArray-is-integer-listp--thm
 
96
  (implies (weightArrayp x) 
 
97
           (integer-listp x)) 
 
98
  :rule-classes ((:forward-chaining :trigger-terms ((weightArrayp x))) :rewrite))
 
99
 
 
100
(defthm costArray-is-integer-listp--thm
 
101
  (implies (costArrayp x)
 
102
           (integer-listp x)) 
 
103
  :rule-classes ((:forward-chaining :trigger-terms ((costArrayp x))) :rewrite))
 
104
 
 
105
(defthm updatingCostArray-is-integer-listp--thm
 
106
  (implies (updatingCostArrayp x) 
 
107
           (integer-listp x)) 
 
108
:rule-classes ((:forward-chaining :trigger-terms ((updatingCostArrayp x))) 
 
109
               :rewrite))
 
110
 
 
111
(defthm maskArray-is-integer-listp--thm
 
112
  (implies (maskArrayp x) 
 
113
           (integer-listp x)) 
 
114
  :rule-classes ((:forward-chaining :trigger-terms ((maskArrayp x))) :rewrite))
 
115
 
 
116
(defthm sourceVertexArray-is-integer-listp--thm
 
117
  (implies (sourceVertexArrayp x) 
 
118
           (integer-listp x)) 
 
119
:rule-classes ((:forward-chaining :trigger-terms ((sourceVertexArrayp x))) 
 
120
               :rewrite))
 
121
 
 
122
(defthm resultArray-is-integer-listp--thm
 
123
  (implies (resultArrayp x) 
 
124
           (integer-listp x)) 
 
125
  :rule-classes ((:forward-chaining :trigger-terms ((resultArrayp x))) :rewrite))
 
126
 
 
127
(defthm weightArrayp-update-nth--thm
 
128
  (implies 
 
129
   (and (weightArrayp n)
 
130
        (>= x 0)
 
131
        (< x (len n))
 
132
        (integerp y)
 
133
        (<= 0 y))
 
134
   (weightArrayp (update-nth x y n)))
 
135
  :rule-classes ((:forward-chaining :trigger-terms ((update-nth x y n))) :rewrite))
 
136
 
 
137
(defthm maskArrayp-update-nth--thm
 
138
  (implies 
 
139
   (and (maskArrayp n)
 
140
        (>= x 0)
 
141
        (< x (len n))
 
142
        (or (= y 0) (= y 1)))
 
143
   (maskArrayp (update-nth x y n)))
 
144
  :rule-classes ((:forward-chaining :trigger-terms ((update-nth x y n))) :rewrite))
 
145
 
 
146
(defthm edgeArrayp-update-nth--thm
 
147
  (implies 
 
148
   (and (edgeArrayp n)
 
149
        (>= x 0)
 
150
        (< x (len n))
 
151
        (integerp y)
 
152
        (<= 0 y)
 
153
        (< y *MAX_VERTICES*))
 
154
   (edgeArrayp (update-nth x y n)))
 
155
  :rule-classes ((:forward-chaining :trigger-terms ((update-nth x y n))) :rewrite))
 
156
 
 
157
(defthm costArrayp-update-nth--thm
 
158
  (implies 
 
159
   (and (costArrayp n)
 
160
        (>= x 0)
 
161
        (< x (len n))
 
162
        (integerp y)
 
163
        (>= y 0))
 
164
   (costArrayp (update-nth x y n)))
 
165
  :rule-classes ((:forward-chaining :trigger-terms ((update-nth x y n))) :rewrite))
 
166
 
 
167
(defthm updatingCostArrayp-update-nth--thm
 
168
  (implies 
 
169
   (and (updatingCostArrayp n)
 
170
        (>= x 0)
 
171
        (< x (len n))
 
172
        (integerp y)
 
173
        (>= y 0))
 
174
   (updatingCostArrayp (update-nth x y n)))
 
175
  :rule-classes ((:forward-chaining :trigger-terms ((update-nth x y n))) :rewrite))
 
176
 
 
177
(defthm resultArrayp-update-nth--thm
 
178
  (implies 
 
179
   (and (resultArrayp n)
 
180
        (>= x 0)
 
181
        (< x (len n))
 
182
        (integerp y)
 
183
        (>= y 0))
 
184
   (resultArrayp (update-nth x y n)))
 
185
  :rule-classes ((:forward-chaining :trigger-terms ((update-nth x y n))) :rewrite))
 
186
 
 
187
(defthm sourceVertexArrayp-update-nth--thm
 
188
  (implies 
 
189
   (and (sourceVertexArrayp n)
 
190
        (>= x 0)
 
191
        (< x (len n))
 
192
        (integerp y)
 
193
        (>= y 0)
 
194
        (< y *MAX_SOURCES*))
 
195
   (sourceVertexArrayp (update-nth x y n)))
 
196
  :rule-classes ((:forward-chaining :trigger-terms ((update-nth x y n))) :rewrite))
 
197
 
 
198
(defthm costArray-ge-0--thm
 
199
  (implies 
 
200
   (and (costArrayp n)
 
201
        (>= x 0)
 
202
        (< x (len n)))
 
203
   (<= 0 (nth x n)))
 
204
  :rule-classes ((:forward-chaining :trigger-terms ((nth x n))) :rewrite))
 
205
 
 
206
(defthm updatingCostArray-ge-0--thm
 
207
  (implies 
 
208
   (and (updatingCostArrayp n)
 
209
        (>= x 0)
 
210
        (< x (len n)))
 
211
   (<= 0 (nth x n)))
 
212
  :rule-classes ((:forward-chaining :trigger-terms ((nth x n))) :rewrite))
 
213
 
 
214
(defthm nth-edgeArray-integerp--thm
 
215
  (implies 
 
216
   (and (edgeArrayp n)
 
217
        (>= x 0)
 
218
        (< x (len n)))
 
219
   (integerp (nth x n)))
 
220
  :rule-classes ((:forward-chaining :trigger-terms ((nth x n))) :rewrite))
 
221
 
 
222
(defthm nth-weightArray-integerp--thm
 
223
  (implies 
 
224
   (and (weightArrayp n)
 
225
        (>= x 0)
 
226
        (< x (len n)))
 
227
   (integerp (nth x n)))
 
228
  :rule-classes ((:forward-chaining :trigger-terms ((nth x n))) :rewrite))
 
229
 
 
230
(defthm nth-CostArray-integerp--thm
 
231
  (implies 
 
232
   (and (costArrayp n)
 
233
        (>= x 0)
 
234
        (< x (len n)))
 
235
   (integerp (nth x n)))
 
236
  :rule-classes ((:forward-chaining :trigger-terms ((nth x n))) :rewrite))
 
237
 
 
238
(defthm nth-updatingCostArray-integerp--thm
 
239
  (implies 
 
240
   (and (updatingCostArrayp n)
 
241
        (>= x 0)
 
242
        (< x (len n)))
 
243
   (integerp (nth x n)))
 
244
  :rule-classes ((:forward-chaining :trigger-terms ((nth x n))) :rewrite))
 
245
 
 
246
(defthm nth-maskArray-integerp--thm
 
247
  (implies 
 
248
   (and (maskArrayp n)
 
249
        (>= x 0)
 
250
        (< x (len n)))
 
251
   (integerp (nth x n)))
 
252
  :rule-classes ((:forward-chaining :trigger-terms ((nth x n))) :rewrite))
 
253
 
 
254
 
 
255
(defthm edgeArray-ge-0--thm
 
256
  (implies 
 
257
   (and (edgeArrayp n)
 
258
        (>= x 0)
 
259
        (< x (len n)))
 
260
   (<= 0 (nth x n)))
 
261
  :rule-classes ((:forward-chaining :trigger-terms ((nth x n))) :rewrite))
 
262
 
 
263
(defthm edgeArray-lt-max-vertex-count--thm
 
264
  (implies 
 
265
   (and (edgeArrayp n)
 
266
        (>= x 0)
 
267
        (< x (len n)))
 
268
   (< (nth x n) *MAX_VERTICES*))
 
269
  :rule-classes ((:forward-chaining :trigger-terms ((nth x n))) :rewrite))
 
270
 
 
271
 
 
272
(defthm vertexArray-lt-max-edge-count--thm
 
273
  (implies 
 
274
   (and (vertexArrayp n)
 
275
        (>= x 0)
 
276
        (< x (len n)))
 
277
   (< (nth x n) *MAX_EDGES*))
 
278
  :rule-classes ((:forward-chaining :trigger-terms ((nth x n))) :rewrite))
 
279
 
 
280
(defthm natp-max-edge-count-minus-vertexArrayi--thm
 
281
  (implies 
 
282
   (and (vertexArrayp n)
 
283
        (>= x 0)
 
284
        (< x (len n)))
 
285
   (natp (+ *MAX_EDGES* (- (nth x n)))))
 
286
  :rule-classes ((:forward-chaining :trigger-terms ((nth x n))) :rewrite))
 
287
 
 
288
 
 
289
(defthm sourceVertexArray-ge-0--thm
 
290
  (implies 
 
291
   (and (sourceVertexArrayp n)
 
292
        (>= x 0)
 
293
        (< x (len n)))
 
294
   (<= 0 (nth x n)))
 
295
  :rule-classes ((:forward-chaining :trigger-terms ((nth x n))) :rewrite))
 
296
 
 
297
(defthm weightArray-ge-0--thm
 
298
  (implies 
 
299
   (and (weightArrayp n)
 
300
        (>= x 0)
 
301
        (< x (len n)))
 
302
   (<= 0 (nth x n)))
 
303
  :rule-classes ((:forward-chaining :trigger-terms ((nth x n))) :rewrite))
 
304
 
 
305
(defthm vertexArray-ge-0--thm
 
306
  (implies 
 
307
   (and (vertexArrayp n)
 
308
        (>= x 0)
 
309
        (< x (len n)))
 
310
   (<= 0 (nth x n)))
 
311
  :rule-classes ((:forward-chaining :trigger-terms ((nth x n))) :rewrite))
 
312
 
 
313
 
 
314
(defun init-vertex-array (i GraphData)
 
315
  (declare (xargs :stobjs GraphData 
 
316
                  :guard (and (natp i) (<= i *MAX_VERTICES*))))
 
317
  (cond ((not (and (mbt (GraphDatap GraphData))
 
318
                   (mbt (natp i))
 
319
                   (mbt (<= i *MAX_VERTICES*)))) GraphData)
 
320
        ((mbe :logic (zp i)
 
321
              :exec (int= i 0)) GraphData)
 
322
        (t 
 
323
         (seq GraphData
 
324
              (update-vertexArrayi (1- i) (* (1- i) *MAX_EDGES_PER_VERTEX*) 
 
325
                                   GraphData)
 
326
              (init-vertex-array (1- i) GraphData)))))
 
327
 
 
328
;;(in-theory (enable natp-random$))
 
329
 
 
330
(defun init-edge-and-weight-arrays (ix GraphData state)
 
331
  (declare (xargs :stobjs (GraphData state)
 
332
                  :verify-guards nil
 
333
                  :guard (and (natp ix) (<= ix *MAX_EDGES*))))
 
334
  (cond ((not (GraphDatap GraphData)) (mv GraphData state))
 
335
        ((not (natp ix)) (mv GraphData state))
 
336
        ((> ix *MAX_EDGES*) (mv GraphData state))
 
337
        ((mbe :logic (zp ix)
 
338
              :exec (int= ix 0)) (mv GraphData state))
 
339
        (t 
 
340
         (mv-let (rnd1 state) (random$ *MAX_VERTICES* state)
 
341
                 (let ((GraphData (update-edgeArrayi (1- ix) rnd1 GraphData)))
 
342
                   (mv-let (rnd2 state) (random$ 100 state) 
 
343
                           (let ((GraphData (update-weightArrayi 
 
344
                                             (1- ix)
 
345
                                             (if (zp rnd2) 1 rnd2) GraphData)))
 
346
                             (init-edge-and-weight-arrays (1- ix) 
 
347
                                                          GraphData state))))))))
 
348
 
 
349
 
 
350
;;;
 
351
;;  Generate a random graph
 
352
;;
 
353
 
 
354
(defun generateRandomGraph (GraphData state)
 
355
  (declare (xargs :stobjs (GraphData state) 
 
356
                  :verify-guards nil))
 
357
  (seq GraphData
 
358
       (init-vertex-array *MAX_VERTICES* GraphData)
 
359
       (init-edge-and-weight-arrays *MAX_EDGES* GraphData state)))
 
360
 
 
361
;;
 
362
;; Check whether the mask array is empty.  This tells the algorithm whether
 
363
;; it needs to continue running or not.
 
364
;;
 
365
 
 
366
(defun maskArrayEmptyp (i GraphData)
 
367
  (declare (xargs :stobjs GraphData 
 
368
                  :guard (and (natp i) (<= i *MAX_VERTICES*))))
 
369
  (cond ((not (and (mbt (GraphDatap GraphData))
 
370
                   (mbt (natp i)) (mbt (<= i *MAX_VERTICES*)))) nil)
 
371
        ((mbe :logic (zp i)
 
372
              :exec (int= i 0)) t)
 
373
        ((= (maskArrayi (1- i) GraphData) 1) nil)
 
374
        (t (maskArrayEmptyp (1- i) GraphData))))
 
375
 
 
376
 
 
377
(defun init-mask-cost-updating-cost (v-down result-num GraphData)
 
378
  (declare (xargs :stobjs GraphData 
 
379
                  :guard (and (natp v-down) 
 
380
                              (<= v-down *MAX_VERTICES*)
 
381
                              (natp result-num) 
 
382
                              (< result-num *MAX_SOURCES*))))
 
383
  (cond ((not (and (mbt (GraphDatap GraphData))
 
384
                   (mbt (natp v-down))
 
385
                   (mbt (natp result-num))
 
386
                   (mbt (< result-num *MAX_SOURCES*))
 
387
                   (mbt (<= v-down *MAX_VERTICES*)))) GraphData)
 
388
        ((mbe :logic (zp v-down)
 
389
              :exec (int= v-down 0)) GraphData)
 
390
        (t (seq GraphData
 
391
                (if (= (- *MAX_VERTICES* v-down)
 
392
                       (sourceVertexArrayi result-num GraphData))
 
393
                    (seq GraphData
 
394
                         (update-maskArrayi (- *MAX_VERTICES* v-down) 1 GraphData)
 
395
                         (update-costArrayi (- *MAX_VERTICES* v-down) 0 GraphData)
 
396
                         (update-updatingCostArrayi (- *MAX_VERTICES* v-down) 0 
 
397
                                                    GraphData))
 
398
                  (seq GraphData
 
399
                       (update-maskArrayi (- *MAX_VERTICES* v-down) 0 GraphData)
 
400
                       (update-costArrayi (- *MAX_VERTICES* v-down) 
 
401
                                          #xffffffffffffffff GraphData)
 
402
                       (update-updatingCostArrayi (- *MAX_VERTICES* v-down) 
 
403
                                                  #xffffffffffffffff GraphData)))
 
404
                (init-mask-cost-updating-cost (1- v-down) result-num GraphData)))))
 
405
 
 
406
(defthm imcuc-preserves-true-listp--thm
 
407
  (IMPLIES (and (true-listp GraphData)
 
408
                (natp v-down)
 
409
                (<= v-down *MAX_VERTICES*)
 
410
                (natp result-num) 
 
411
                (< result-num *MAX_SOURCES*))
 
412
           (TRUE-LISTP (INIT-MASK-COST-UPDATING-COST v-down result-num GRAPHDATA))))
 
413
 
 
414
(defthm imcuc-preserves-len--thm
 
415
  (implies (true-listp GraphData)
 
416
           (= (len (init-mask-cost-updating-cost v-down result-num GraphData))
 
417
              (len GraphData))))
 
418
 
 
419
(defthm imcuc-preserves-costArrayp--thm
 
420
  (implies (COSTARRAYP (NTH *COSTARRAYI* GraphData))
 
421
           (COSTARRAYP
 
422
            (NTH *COSTARRAYI*
 
423
                 (init-mask-cost-updating-cost v-down result-num GraphData)))))
 
424
 
 
425
(defthm imcuc-edgeArray-unchanged--thm
 
426
  (= (nth *EDGEARRAYI* 
 
427
          (init-mask-cost-updating-cost v-down result-num GraphData))
 
428
     (nth *EDGEARRAYI* GraphData)))
 
429
 
 
430
(defthm imcuc-edgeCount-unchanged--thm
 
431
  (= (nth *EDGECOUNT* 
 
432
          (init-mask-cost-updating-cost v-down result-num GraphData))
 
433
     (nth *EDGECOUNT* GraphData)))
 
434
 
 
435
(defthm imcuc-preserves-maskArrayp--thm
 
436
  (implies (MASKARRAYP (NTH *MASKARRAYI* GraphData))
 
437
           (MASKARRAYP
 
438
            (NTH *MASKARRAYI*
 
439
                 (init-mask-cost-updating-cost v-down result-num GraphData)))))
 
440
 
 
441
(defthm imcuc-resultArray-unchanged--thm
 
442
  (= (nth *RESULTARRAYI* 
 
443
          (init-mask-cost-updating-cost v-down result-num GraphData))
 
444
     (nth *RESULTARRAYI* GraphData)))
 
445
 
 
446
(defthm imcuc-sourceVertexArray-unchanged--thm
 
447
  (= (nth *SOURCEVERTEXARRAYI* 
 
448
          (init-mask-cost-updating-cost v-down result-num GraphData))
 
449
     (nth *SOURCEVERTEXARRAYI* GraphData)))
 
450
 
 
451
(defthm imcuc-vertexArray-unchanged--thm
 
452
  (= (nth *VERTEXARRAYI*
 
453
          (init-mask-cost-updating-cost v-down result-num GraphData))
 
454
     (nth *VERTEXARRAYI* GraphData)))
 
455
 
 
456
(defthm imcuc-vertexCount-unchanged--thm
 
457
  (= (car (init-mask-cost-updating-cost v-down result-num GraphData))
 
458
     (car GraphData)))
 
459
 
 
460
(defthm imcuc-weightArray-unchanged--thm
 
461
  (= (nth *WEIGHTARRAYI* 
 
462
          (init-mask-cost-updating-cost v-down result-num GraphData))
 
463
     (nth *WEIGHTARRAYI* GraphData)))
 
464
 
 
465
(defthm imcuc-preserves-GraphDatap--thm
 
466
  (implies (GraphDatap GraphData)
 
467
           (GraphDatap (init-mask-cost-updating-cost v-down result-num GraphData))))
 
468
 
 
469
(in-theory (disable init-mask-cost-updating-cost))
 
470
 
 
471
(defthm plus-ge-0-if-addends-ge-0--thm
 
472
  (implies (and (>= x 0) (>= y 0)) 
 
473
           (<= 0 (+ x y))))
 
474
 
 
475
(defthm plus-is-integerp-if-addends-integerp--thm
 
476
  (implies (and (integerp x) (integerp y)) 
 
477
           (integerp (+ x y))))
 
478
 
 
479
;; Would like to use a more modern arithmetic book, but it interferes with 
 
480
;; Sol's defiteration macro, amongst other things.
 
481
(local (include-book "arithmetic/top-with-meta" :dir :system))
 
482
 
 
483
(defun dsk1-inner-loop (edge-down edge-max tid GraphData)
 
484
  (declare (xargs :stobjs GraphData 
 
485
                  :guard (and (natp edge-down)
 
486
                              (natp edge-max)
 
487
                              (natp tid)
 
488
                              (< tid *MAX_VERTICES*)
 
489
                              (<= edge-down edge-max)
 
490
                              (<= edge-max *MAX_EDGES*))))
 
491
  (cond ((not (and (mbt (GraphDatap GraphData))
 
492
                   (mbt (natp edge-down))
 
493
                   (mbt (natp edge-max))
 
494
                   (mbt (natp tid))
 
495
                   (mbt (< tid *MAX_VERTICES*))
 
496
                   (mbt (<= edge-down edge-max))
 
497
                   (mbt (<= edge-max *MAX_EDGES*)))) GraphData)
 
498
        ((mbe :logic (zp edge-down)
 
499
              :exec (int= edge-down 0)) GraphData)
 
500
        (t (let ((updating-index (edgeArrayi 
 
501
                                   (the (integer 0 *) (- edge-max edge-down)) 
 
502
                                   GraphData)))
 
503
             (seq GraphData 
 
504
                  (update-updatingCostArrayi 
 
505
                   updating-index 
 
506
                   (min (updatingCostArrayi updating-index GraphData) 
 
507
                        (+ (costArrayi tid GraphData)
 
508
                           (weightArrayi (- edge-max edge-down) GraphData))) 
 
509
                   GraphData)
 
510
                  (dsk1-inner-loop (1- edge-down) edge-max tid GraphData))))))
 
511
 
 
512
 
 
513
(defthm dsk1-il-preserves-true-listp--thm
 
514
  (implies (true-listp GraphData)
 
515
           (true-listp (dsk1-inner-loop edge-down edge-max tid GraphData))))
 
516
 
 
517
(defthm dsk1-il-preserves-len--thm
 
518
  (implies (true-listp GraphData)
 
519
           (= (len (dsk1-inner-loop edge-down edge-max tid GraphData))
 
520
              (len GraphData))))
 
521
 
 
522
(defthm dsk1-il-costArray-unchanged--thm
 
523
  (= (nth *COSTARRAYI* 
 
524
          (dsk1-inner-loop edge-down edge-max tid GraphData))
 
525
     (nth *COSTARRAYI* GraphData)))
 
526
 
 
527
(defthm dsk1-il-edgeArray-unchanged--thm
 
528
  (= (nth *EDGEARRAYI* 
 
529
          (dsk1-inner-loop edge-down edge-max tid GraphData))
 
530
     (nth *EDGEARRAYI* GraphData)))
 
531
 
 
532
(defthm dsk1-il-edgeCount-unchanged--thm
 
533
  (= (nth *EDGECOUNT* 
 
534
          (dsk1-inner-loop edge-down edge-max tid GraphData))
 
535
     (nth *EDGECOUNT* GraphData)))
 
536
 
 
537
(defthm dsk1-il-maskArray-unchanged--thm
 
538
  (= (nth *MASKARRAYI* 
 
539
          (dsk1-inner-loop edge-down edge-max tid GraphData))
 
540
     (nth *MASKARRAYI* GraphData)))
 
541
 
 
542
(defthm dsk1-il-resultArray-unchanged--thm
 
543
  (= (nth *RESULTARRAYI* 
 
544
          (dsk1-inner-loop edge-down edge-max tid GraphData))
 
545
     (nth *RESULTARRAYI* GraphData)))
 
546
 
 
547
(defthm dsk1-il-sourceVertexArray-unchanged--thm
 
548
  (= (nth *SOURCEVERTEXARRAYI* 
 
549
          (dsk1-inner-loop edge-down edge-max tid GraphData))
 
550
     (nth *SOURCEVERTEXARRAYI* GraphData)))
 
551
 
 
552
(defthm dsk1-il-vertexArray-unchanged--thm
 
553
  (= (nth *VERTEXARRAYI* 
 
554
          (dsk1-inner-loop edge-down edge-max tid GraphData))
 
555
     (nth *VERTEXARRAYI* GraphData)))
 
556
 
 
557
(defthm dsk1-il-vertexCount-unchanged--thm
 
558
  (= (car (dsk1-inner-loop edge-down edge-max tid GraphData))
 
559
     (car GraphData)))
 
560
 
 
561
(defthm dsk1-il-weightArray-unchanged--thm
 
562
  (= (nth *WEIGHTARRAYI* 
 
563
          (dsk1-inner-loop edge-down edge-max tid GraphData))
 
564
     (nth *WEIGHTARRAYI* GraphData)))
 
565
 
 
566
(defthm dsk1-il-preserves-updatingCostArrayp--thm
 
567
  (implies (UPDATINGCOSTARRAYP (NTH *UPDATINGCOSTARRAYI* GraphData))
 
568
           (UPDATINGCOSTARRAYP
 
569
            (NTH *UPDATINGCOSTARRAYI*
 
570
                 (DSK1-INNER-LOOP EDGE-DOWN EDGE-MAX TID GRAPHDATA)))))
 
571
 
 
572
(defthm dsk1-il-preserves-updatingCostArrayp-len--thm
 
573
  (= (LEN (NTH *UPDATINGCOSTARRAYI*
 
574
               (DSK1-INNER-LOOP EDGE-DOWN EDGE-MAX TID GRAPHDATA)))
 
575
     (LEN (NTH *UPDATINGCOSTARRAYI* GRAPHDATA))))
 
576
 
 
577
(defthm dsk1-il-preserves-GraphDatap--thm
 
578
  (implies (GraphDatap GraphData)
 
579
           (GraphDatap (dsk1-inner-loop edge-down edge-max tid GraphData))))
 
580
 
 
581
(in-theory (disable dsk1-inner-loop))
 
582
 
 
583
;; (defthm dsk1-il-GraphDatap-maskArray-update--thm
 
584
;; (implies (and (GraphDatap GraphData) 
 
585
;;               (or (= y 0) (= y 1)) (>= 0 x) (< x *MAX_VERTICES*)
 
586
;;               (Graphdatap (dsk1-inner-loop edge-down edge-max tid 
 
587
;;                                                               GraphData)))
 
588
;;   (Graphdatap (dsk1-inner-loop edge-down edge-max tid 
 
589
;;               (UPDATE-NTH *MASKARRAYI*
 
590
;;                            (UPDATE-NTH x y (NTH *MASKARRAYI* GRAPHDATA))
 
591
;;                            GRAPHDATA)))))
 
592
 
 
593
(defthm update-updatingCostArray-vertexArray-unchanged--thm
 
594
  (= (nth *VERTEXARRAYI* (UPDATE-NTH *UPDATINGCOSTARRAYI* j GRAPHDATA))
 
595
     (nth *VERTEXARRAYI* GraphData)))
 
596
 
 
597
 
 
598
;; An instance of Hardin's Bridge:
 
599
;;
 
600
;; array-based iterative loop --> tail-recursive stobj array fn == 
 
601
;; non-tail-recursive stobj arrary fn ==> (thm involving nthcdr or take) ==> 
 
602
;; primitive-recursive fn operating on a list
 
603
 
 
604
;; Load Sol's nice iterator stuff
 
605
;; Synthesizes tail-recursive and non-tail-recursive stobj array fns 
 
606
;; and proves them equal
 
607
(include-book "centaur/misc/iter" :dir :system)
 
608
 
 
609
;; Iteration macro for a "nondecreasing" predicate on vertex array
 
610
(defiteration nondec-arr (res GraphData)
 
611
  (declare (xargs :stobjs GraphData))
 
612
  (and (<= (vertexArrayi (1- (- *MAX_VERTICES* ix)) GraphData) 
 
613
           (vertexArrayi (- *MAX_VERTICES* ix) GraphData)) res)
 
614
   :returns res
 
615
   :index ix
 
616
   :last *MAX_VERTICES*
 
617
   :first 1
 
618
)
 
619
 
 
620
;; Output from defiteration:
 
621
 
 
622
;; We export NONDEC-ARR$INLINE, NONDEC-ARR-ITER, NONDEC-ARR-TAILREC and
 
623
;; NONDEC-ARR-STEP$INLINE.
 
624
 
 
625
;; (DEFUN NONDEC-ARR$INLINE (RES GRAPHDATA)
 
626
;;   (DECLARE (XARGS :STOBJS GRAPHDATA))
 
627
;;   (B* NIL
 
628
;;       (MBE :LOGIC (NONDEC-ARR-ITER *MAX_VERTICES* RES GRAPHDATA)
 
629
;;         :EXEC (NONDEC-ARR-TAILREC 1 RES GRAPHDATA))))
 
630
 
 
631
;; (DEFUN NONDEC-ARR-STEP$INLINE
 
632
;;   (IX RES GRAPHDATA)
 
633
;;   (DECLARE (TYPE (INTEGER 1 *) IX)
 
634
;;         (IGNORABLE IX RES GRAPHDATA)
 
635
;;         (XARGS :GUARD-HINTS NIL))
 
636
;;   (DECLARE (XARGS :STOBJS GRAPHDATA))
 
637
;;   (DECLARE (XARGS :GUARD (AND (<= 1 IX)
 
638
;;                            (< IX *MAX_VERTICES*)
 
639
;;                            T)))
 
640
;;   (AND (<= (VERTEXARRAYI (1- (- *MAX_VERTICES* IX))
 
641
;;                       GRAPHDATA)
 
642
;;         (VERTEXARRAYI (- *MAX_VERTICES* IX)
 
643
;;                       GRAPHDATA))
 
644
;;        RES))
 
645
 
 
646
;; (DEFUN NONDEC-ARR-ITER (IX RES GRAPHDATA)
 
647
;;   (DECLARE (TYPE (INTEGER 1 *) IX)
 
648
;;         (XARGS :MEASURE (NFIX (- (IFIX IX) (IFIX 1)))
 
649
;;                :VERIFY-GUARDS NIL))
 
650
;;   (DECLARE (XARGS :STOBJS GRAPHDATA))
 
651
;;   (DECLARE (XARGS :GUARD (AND (<= 1 IX)
 
652
;;                            (<= IX *MAX_VERTICES*)
 
653
;;                            T)))
 
654
;;   (B* (((WHEN (MBE :LOGIC (ZP (- (IFIX IX) (IFIX 1)))
 
655
;;                 :EXEC (INT= 1 IX)))
 
656
;;      RES)
 
657
;;        (IX (1- (LIFIX IX)))
 
658
;;        (RES (NONDEC-ARR-ITER IX RES GRAPHDATA)))
 
659
;;       (NONDEC-ARR-STEP IX RES GRAPHDATA)))
 
660
 
 
661
;; (DEFUN NONDEC-ARR-TAILREC (IX RES GRAPHDATA)
 
662
;;   (DECLARE
 
663
;;    (TYPE (INTEGER 1 *) IX)
 
664
;;    (XARGS :MEASURE (NFIX (- (IFIX *MAX_VERTICES*) (IFIX IX)))))
 
665
;;   (DECLARE (XARGS :STOBJS GRAPHDATA))
 
666
;;   (DECLARE (XARGS :GUARD (AND (<= 1 IX)
 
667
;;                            (<= IX *MAX_VERTICES*)
 
668
;;                            T)))
 
669
;;   (B*
 
670
;;    (((WHEN (MBE :LOGIC (ZP (- (IFIX *MAX_VERTICES*) (IFIX IX)))
 
671
;;              :EXEC (INT= *MAX_VERTICES* IX)))
 
672
;;      RES)
 
673
;;     (IX (LIFIX IX))
 
674
;;     (RES (NONDEC-ARR-STEP IX RES GRAPHDATA)))
 
675
;;    (NONDEC-ARR-TAILREC (1+ IX)
 
676
;;                     RES GRAPHDATA)))
 
677
 
 
678
 
 
679
;; Pretty wrapper for the tail-recursive fn
 
680
;; Needed for guard proof of dijkstra-sssp-kernel-1
 
681
(defun vertices-nondecreasing (GraphData)
 
682
  (declare (xargs :stobjs GraphData))
 
683
  (cond ((not (GraphDatap GraphData)) nil)
 
684
        (t (nondec-arr-tailrec 1 t GraphData))))
 
685
 
 
686
;; A primitive-recursive fn operating on a list
 
687
;; ACL2 likes these sort of fns
 
688
(defun nondec (res lst)
 
689
  (declare (xargs :guard (integer-listp lst)))
 
690
  (cond ((< (len lst) 2) res)
 
691
        (t (and (<= (car lst) (cadr lst))
 
692
                (nondec res (cdr lst))))))
 
693
 
 
694
;; Just a wrapper of the above
 
695
(defun nondecreasing (lst)
 
696
  (declare (xargs :guard (integer-listp lst)))
 
697
  (nondec t lst))
 
698
 
 
699
;; A theorem of the sort readily proven about the above fn
 
700
(defthm nondecreasing-nth--thm
 
701
  (implies (and (> i 0) (< i (len lst)) (nondecreasing lst))
 
702
           (<= (nth (1- i) lst) (nth i lst))))
 
703
 
 
704
 
 
705
(local (include-book "data-structures/list-defthms" :dir :system))
 
706
 
 
707
(local (include-book "nthcdr-theorems"))
 
708
 
 
709
(defthm nth-of-cdr--thm
 
710
  (implies (natp x)
 
711
           (= (nth x (cdr lst)) (nth (1+ x) lst))))
 
712
 
 
713
;; Theorem involving nthcdr -- needed for crossing the bridge
 
714
(defthm nondec-arr-iter-eq-nondec-nthcdr--thm
 
715
  (implies (and (GraphDatap GraphData) (integerp xx) (>= xx 0)
 
716
                (<= xx (len (nth *VERTEXARRAYI* GraphData))))
 
717
           (= (nondec-arr-iter xx res GraphData)
 
718
              (nondec res (nthcdr (- *MAX_VERTICES* xx) 
 
719
                      (nth *VERTEXARRAYI* GraphData)))))
 
720
:hints (("Goal" :in-theory (enable nondec-arr-iter)))
 
721
)
 
722
 
 
723
;; Non-tail-recursive stobj array fn = Primitive-recursive list fn 
 
724
(defthm nondec-arr-iter-*MAX_VERTICES*-eq-nondec--thm
 
725
  (implies (GraphDatap GraphData)
 
726
           (= (nondec-arr-iter *MAX_VERTICES* res GraphData)
 
727
              (nondec res (nth *VERTEXARRAYI* GraphData))))
 
728
:hints (("Goal" :use (:instance nondec-arr-iter-eq-nondec-nthcdr--thm 
 
729
                                  (xx *MAX_VERTICES*))))
 
730
)
 
731
 
 
732
;; Tail-recursive stobj array fn = Primitive-recursive list fn
 
733
(defthm nondec-arr-tail-1-eq-nondec--thm
 
734
  (implies (GraphDatap GraphData)
 
735
           (= (nondec-arr-tailrec 1 res GraphData)
 
736
              (nondec res (nth *VERTEXARRAYI* GraphData)))))
 
737
 
 
738
;; Pretty final result -- bridge crossed!
 
739
(defthm vertices-nondecreasing-is-nondecreasing--thm
 
740
  (implies (GraphDatap GraphData)
 
741
           (= (vertices-nondecreasing GraphData)
 
742
              (nondecreasing (nth *VERTEXARRAYI* GraphData)))))
 
743
 
 
744
 
 
745
;; Now it's easier to prove theorems about the tail-recursive stobj fn -- 
 
746
;; fails to prove without the bridge.
 
747
(defthm vertices-nondecreasing-nth--thm
 
748
  (implies (and (GraphDatap GraphData)
 
749
                (> ix 0) 
 
750
                (< ix (len (nth *VERTEXARRAYI* GraphData)))
 
751
                (vertices-nondecreasing GraphData))
 
752
           (<= (vertexArrayi (1- ix) GraphData)
 
753
               (vertexArrayi ix GraphData))))
 
754
 
 
755
(defthm nondecreasing-vertexArray-nth--thm
 
756
  (implies (and (GraphDatap GraphData) (> ix 0) 
 
757
                (< ix (len (nth *VERTEXARRAYI* GraphData)))
 
758
                (nondecreasing (nth *VERTEXARRAYI* GraphData)))
 
759
           (<= (vertexArrayi (1- ix) GraphData)
 
760
               (vertexArrayi ix GraphData))))
 
761
 
 
762
(defthm natp-le-plus-of-neg--thm
 
763
  (implies (and (integerp x) (integerp y) (<= x y))
 
764
           (natp (+ (- x) y))))
 
765
 
 
766
(defthm index-lt-len-means-index-minus-1-lt-len--thm
 
767
  (implies (and (> ix 0) (< ix (len y))) (< (1- ix) (len y)))
 
768
  :rule-classes ((:forward-chaining :trigger-terms ((< ix (len y)))) :rewrite))
 
769
 
 
770
;; Needed to complete the guard proof for dijkstra-sssp-kernel-1
 
771
(DEFTHM NONDECREASING-VERTEXARRAY-NATP-DIFF-ADJACENT--THM
 
772
  (IMPLIES (AND (integer-listp (NTH *VERTEXARRAYI* GRAPHDATA)) ;;(GRAPHDATAP GRAPHDATA)
 
773
                (> IX 0) (< (1- ix) (LEN (NTH *VERTEXARRAYI* GRAPHDATA)))
 
774
                (< IX (LEN (NTH *VERTEXARRAYI* GRAPHDATA)))
 
775
                (NONDECREASING (NTH *VERTEXARRAYI* GRAPHDATA)))
 
776
           (NATP (+ (- (VERTEXARRAYI (1- IX) GRAPHDATA))
 
777
                    (VERTEXARRAYI IX GRAPHDATA)))))
 
778
 
 
779
;; Sigh...
 
780
(defthmd lt-means-le--thm
 
781
  (implies (< x y)
 
782
           (<= x y)))
 
783
 
 
784
(defun dijkstra-sssp-kernel-1 (tid-down GraphData)
 
785
  (declare (xargs :stobjs GraphData 
 
786
                  :guard (and (natp tid-down) (<= tid-down *MAX_VERTICES*)
 
787
                              (vertices-nondecreasing GraphData))
 
788
                  :guard-hints (("Goal" :in-theory (enable lt-means-le--thm))
 
789
                                ("Subgoal 1.3" :USE (:INSTANCE 
 
790
                                 NONDECREASING-VERTEXARRAY-NATP-DIFF-ADJACENT--THM
 
791
                                   (IX (+ 1 *MAX_VERTICES* (- TID-DOWN))))))))
 
792
  (cond ((not (and (mbt (GraphDatap GraphData))
 
793
                   (mbt (natp tid-down))
 
794
                   (mbt (<= tid-down *MAX_VERTICES*)))) GraphData)
 
795
        ((mbe :logic (zp tid-down)
 
796
              :exec (int= tid-down 0)) GraphData)
 
797
        (t (if (= (maskArrayi (- *MAX_VERTICES* tid-down) GraphData) 1)
 
798
               (seq GraphData
 
799
                    (update-maskArrayi (- *MAX_VERTICES* tid-down) 0 GraphData)
 
800
                    (dsk1-inner-loop 
 
801
                     ;; edge-down = edge-end - edge-start
 
802
                     (- (if (< (1+ (- *MAX_VERTICES* tid-down)) 
 
803
                               *MAX_VERTICES*)
 
804
                            (vertexArrayi 
 
805
                             (1+ (- *MAX_VERTICES* tid-down))
 
806
                             GraphData)
 
807
                          *MAX_EDGES*)
 
808
                        (vertexArrayi (- *MAX_VERTICES* tid-down) GraphData))
 
809
                     ;; edge-end 
 
810
                     (if (< (1+ (- *MAX_VERTICES* tid-down))
 
811
                            *MAX_VERTICES*)
 
812
                         (vertexArrayi 
 
813
                          (1+ (- *MAX_VERTICES* tid-down))
 
814
                          GraphData)
 
815
                       *MAX_EDGES*)
 
816
                     ;; tid
 
817
                     (- *MAX_VERTICES* tid-down)
 
818
                     GraphData)
 
819
                    (dijkstra-sssp-kernel-1 (1- tid-down) GraphData))
 
820
             (dijkstra-sssp-kernel-1 (1- tid-down) GraphData)))))
 
821
 
 
822
 
 
823
(defthm dsk1-preserves-true-listp--thm
 
824
  (implies (true-listp GraphData)
 
825
           (true-listp (dijkstra-sssp-kernel-1 x GraphData))))
 
826
 
 
827
(defthm dsk1-preserves-len--thm
 
828
  (implies (true-listp GraphData)
 
829
           (= (len (dijkstra-sssp-kernel-1 x GraphData))
 
830
              (len GraphData))))
 
831
 
 
832
(defthm dsk1-costArray-unchanged--thm
 
833
  (= (nth *COSTARRAYI* 
 
834
          (dijkstra-sssp-kernel-1 x GraphData))
 
835
     (nth *COSTARRAYI* GraphData)))
 
836
 
 
837
(defthm dsk1-edgeArray-unchanged--thm
 
838
  (= (nth *EDGEARRAYI* 
 
839
          (dijkstra-sssp-kernel-1 x GraphData))
 
840
     (nth *EDGEARRAYI* GraphData)))
 
841
 
 
842
(defthm dsk1-edgeCount-unchanged--thm
 
843
  (= (nth *EDGECOUNT* 
 
844
          (dijkstra-sssp-kernel-1 x GraphData))
 
845
     (nth *EDGECOUNT* GraphData)))
 
846
 
 
847
(defthm dsk1-resultArray-unchanged--thm
 
848
  (= (nth *RESULTARRAYI* 
 
849
          (dijkstra-sssp-kernel-1 x GraphData))
 
850
     (nth *RESULTARRAYI* GraphData)))
 
851
 
 
852
(defthm dsk1-sourceVertexArray-unchanged--thm
 
853
  (= (nth *SOURCEVERTEXARRAYI* 
 
854
          (dijkstra-sssp-kernel-1 x GraphData))
 
855
     (nth *SOURCEVERTEXARRAYI* GraphData)))
 
856
 
 
857
(defthm dsk1-vertexArray-unchanged--thm
 
858
  (= (nth *VERTEXARRAYI* 
 
859
          (dijkstra-sssp-kernel-1 x GraphData))
 
860
     (nth *VERTEXARRAYI* GraphData)))
 
861
 
 
862
(defthm dsk1-vertexCount-unchanged--thm
 
863
  (= (car (dijkstra-sssp-kernel-1 x GraphData))
 
864
     (car GraphData)))
 
865
 
 
866
(defthm dsk1-weightArray-unchanged--thm
 
867
  (= (nth *WEIGHTARRAYI* 
 
868
          (dijkstra-sssp-kernel-1 x GraphData))
 
869
     (nth *WEIGHTARRAYI* GraphData)))
 
870
 
 
871
(defthm dsk1-preserves-maskArrayp--thm
 
872
  (implies (MASKARRAYP (NTH *MASKARRAYI* GraphData))
 
873
           (MASKARRAYP
 
874
            (NTH *MASKARRAYI*
 
875
                 (DIJKSTRA-SSSP-KERNEL-1 X GRAPHDATA)))))
 
876
 
 
877
(defthm dsk1-preserves-maskArrayp-len--thm
 
878
  (implies (MASKARRAYP (NTH *MASKARRAYI* GraphData))
 
879
           (= (LEN (NTH *MASKARRAYI*
 
880
                        (DIJKSTRA-SSSP-KERNEL-1 X GRAPHDATA)))
 
881
              (LEN (NTH *MASKARRAYI* GRAPHDATA)))))
 
882
 
 
883
 
 
884
(defthm dsk1-preserves-GraphDatap--thm
 
885
  (implies (GraphDatap GraphData)
 
886
           (GraphDatap (dijkstra-sssp-kernel-1 x GraphData))))
 
887
 
 
888
(in-theory (disable dijkstra-sssp-kernel-1))
 
889
 
 
890
;; Equivalent of OCL_SSSP_KERNEL2()
 
891
(defun dijkstra-sssp-kernel-2 (tid-down GraphData)
 
892
  (declare (xargs :stobjs GraphData 
 
893
                  :guard (and (natp tid-down) (<= tid-down *MAX_VERTICES*))))
 
894
  (cond ((not (and (mbt (GraphDatap GraphData))
 
895
                   (mbt (natp tid-down))
 
896
                   (mbt (<= tid-down *MAX_VERTICES*)))) GraphData)
 
897
        ((mbe :logic (zp tid-down)
 
898
              :exec (int= tid-down 0)) GraphData)
 
899
        (t (seq GraphData
 
900
                (if (> (costArrayi (- *MAX_VERTICES* tid-down) GraphData)
 
901
                       (updatingCostArrayi (- *MAX_VERTICES* tid-down) GraphData))
 
902
                    (seq GraphData
 
903
                         (update-costArrayi 
 
904
                          (- *MAX_VERTICES* tid-down) 
 
905
                          (updatingCostArrayi (- *MAX_VERTICES* tid-down) GraphData)
 
906
                          GraphData)
 
907
                         (update-maskArrayi (- *MAX_VERTICES* tid-down) 1 
 
908
                                            GraphData))
 
909
                  (update-updatingCostArrayi (- *MAX_VERTICES* tid-down)
 
910
                                             (costArrayi 
 
911
                                              (- *MAX_VERTICES* tid-down) 
 
912
                                              GraphData)
 
913
                                             GraphData))
 
914
                (dijkstra-sssp-kernel-2 (1- tid-down) GraphData)))))
 
915
 
 
916
(defthm dsk2-preserves-true-listp--thm
 
917
  (implies (true-listp GraphData)
 
918
           (true-listp (dijkstra-sssp-kernel-2 x GraphData))))
 
919
 
 
920
(defthm dsk2-preserves-len--thm
 
921
  (implies (true-listp GraphData)
 
922
           (= (len (dijkstra-sssp-kernel-2 x GraphData))
 
923
              (len GraphData))))
 
924
 
 
925
(defthm dsk2-edgeArray-unchanged--thm
 
926
  (= (nth *EDGEARRAYI* 
 
927
          (dijkstra-sssp-kernel-2 x GraphData))
 
928
     (nth *EDGEARRAYI* GraphData)))
 
929
 
 
930
(defthm dsk2-edgeCount-unchanged--thm
 
931
  (= (nth *EDGECOUNT* 
 
932
          (dijkstra-sssp-kernel-2 x GraphData))
 
933
     (nth *EDGECOUNT* GraphData)))
 
934
 
 
935
(defthm dsk2-resultArray-unchanged--thm
 
936
  (= (nth *RESULTARRAYI* 
 
937
          (dijkstra-sssp-kernel-2 x GraphData))
 
938
     (nth *RESULTARRAYI* GraphData)))
 
939
 
 
940
(defthm dsk2-sourceVertexArray-unchanged--thm
 
941
  (= (nth *SOURCEVERTEXARRAYI* 
 
942
          (dijkstra-sssp-kernel-2 x GraphData))
 
943
     (nth *SOURCEVERTEXARRAYI* GraphData)))
 
944
 
 
945
(defthm dsk2-vertexArray-unchanged--thm
 
946
  (= (nth *VERTEXARRAYI* 
 
947
          (dijkstra-sssp-kernel-2 x GraphData))
 
948
     (nth *VERTEXARRAYI* GraphData)))
 
949
 
 
950
(defthm dsk2-vertexCount-unchanged--thm
 
951
  (= (car (dijkstra-sssp-kernel-2 x GraphData))
 
952
     (car GraphData)))
 
953
 
 
954
(defthm dsk2-weightArray-unchanged--thm
 
955
  (= (nth *WEIGHTARRAYI* 
 
956
          (dijkstra-sssp-kernel-2 x GraphData))
 
957
     (nth *WEIGHTARRAYI* GraphData)))
 
958
 
 
959
(defthm dsk2-preserves-costArrayp--thm
 
960
  (implies (COSTARRAYP (NTH *COSTARRAYI* GraphData))
 
961
           (COSTARRAYP
 
962
            (NTH *COSTARRAYI*
 
963
             (DIJKSTRA-SSSP-KERNEL-2 X GRAPHDATA)))))
 
964
 
 
965
(defthm dsk2-preserves-costArrayp-len--thm
 
966
  (implies (COSTARRAYP (NTH *COSTARRAYI* GraphData))
 
967
           (= (LEN (NTH *COSTARRAYI*
 
968
                        (DIJKSTRA-SSSP-KERNEL-2 X GRAPHDATA)))
 
969
              (LEN (NTH *COSTARRAYI* GRAPHDATA)))))
 
970
 
 
971
(defthm dsk2-preserves-maskArrayp--thm
 
972
  (implies (MASKARRAYP (NTH *MASKARRAYI* GraphData))
 
973
           (MASKARRAYP
 
974
            (NTH
 
975
             *MASKARRAYI*
 
976
             (DIJKSTRA-SSSP-KERNEL-2 X GRAPHDATA)))))
 
977
 
 
978
(defthm dsk2-preserves-maskArrayp-len--thm
 
979
  (implies (MASKARRAYP (NTH *MASKARRAYI* GraphData))
 
980
           (= (LEN (NTH *MASKARRAYI*
 
981
                        (DIJKSTRA-SSSP-KERNEL-2 X GRAPHDATA)))
 
982
              (LEN (NTH *MASKARRAYI* GRAPHDATA)))))
 
983
 
 
984
(defthm dsk2-preserves-updatingCostArrayp--thm
 
985
  (implies (UPDATINGCOSTARRAYP (NTH *UPDATINGCOSTARRAYI* GraphData))
 
986
           (UPDATINGCOSTARRAYP
 
987
            (NTH
 
988
             *UPDATINGCOSTARRAYI*
 
989
             (DIJKSTRA-SSSP-KERNEL-2 X GRAPHDATA)))))
 
990
 
 
991
(defthm dsk2-preserves-updatingCostArrayp-len--thm
 
992
  (implies (UPDATINGCOSTARRAYP (NTH *UPDATINGCOSTARRAYI* GraphData))
 
993
           (= (LEN (NTH *UPDATINGCOSTARRAYI*
 
994
                        (DIJKSTRA-SSSP-KERNEL-2 X GRAPHDATA)))
 
995
              (LEN (NTH *UPDATINGCOSTARRAYI* GRAPHDATA)))))
 
996
 
 
997
(defthm dsk2-preserves-GraphDatap--thm
 
998
  (implies (GraphDatap GraphData)
 
999
           (GraphDatap (dijkstra-sssp-kernel-2 x GraphData))))
 
1000
 
 
1001
(in-theory (disable dijkstra-sssp-kernel-2))
 
1002
 
 
1003
 
 
1004
(defun mask-array-not-empty-processing (countdown GraphData)
 
1005
  (declare (xargs :stobjs GraphData
 
1006
                  :guard (and (natp countdown)
 
1007
                              (vertices-nondecreasing GraphData))))
 
1008
  (cond ((not (and (mbt (GraphDatap GraphData))
 
1009
                   (mbt (natp countdown))
 
1010
                   (mbt (vertices-nondecreasing GraphData)))) GraphData)
 
1011
        ((maskArrayEmptyp *MAX_VERTICES* GraphData) GraphData)
 
1012
        ((mbe :logic (zp countdown)
 
1013
              :exec (int= countdown 0)) GraphData)
 
1014
        (t (seq GraphData
 
1015
                (dijkstra-sssp-kernel-1 *MAX_VERTICES* GraphData)
 
1016
                (dijkstra-sssp-kernel-2 *MAX_VERTICES* GraphData)
 
1017
                (mask-array-not-empty-processing (1- countdown) GraphData)))))
 
1018
 
 
1019
(defthm manep-preserves-true-listp--thm
 
1020
  (IMPLIES (and (true-listp GraphData)
 
1021
                (>= countdown 0))
 
1022
           (TRUE-LISTP (mask-array-not-empty-processing countdown GraphData))))
 
1023
 
 
1024
(defthm manep-preserves-len--thm
 
1025
  (implies (true-listp GraphData)
 
1026
           (= (len (mask-array-not-empty-processing countdown GraphData))
 
1027
              (len GraphData))))
 
1028
 
 
1029
(defthm manep-preserves-costArrayp--thm
 
1030
  (implies (COSTARRAYP (NTH *COSTARRAYI* GraphData))
 
1031
           (COSTARRAYP
 
1032
            (NTH *COSTARRAYI*
 
1033
                 (mask-array-not-empty-processing countdown GraphData)))))
 
1034
 
 
1035
(defthm manep-edgeArray-unchanged--thm
 
1036
  (= (nth *EDGEARRAYI* 
 
1037
          (mask-array-not-empty-processing countdown GraphData))
 
1038
     (nth *EDGEARRAYI* GraphData)))
 
1039
 
 
1040
(defthm manep-edgeCount-unchanged--thm
 
1041
  (= (nth *EDGECOUNT* 
 
1042
          (mask-array-not-empty-processing countdown GraphData))
 
1043
     (nth *EDGECOUNT* GraphData)))
 
1044
 
 
1045
(defthm manep-preserves-maskArrayp--thm
 
1046
  (implies (MASKARRAYP (NTH *MASKARRAYI* GraphData))
 
1047
           (MASKARRAYP
 
1048
            (NTH *MASKARRAYI*
 
1049
                 (mask-array-not-empty-processing countdown GraphData)))))
 
1050
 
 
1051
(defthm manep-resultArray-unchanged--thm
 
1052
  (= (nth *RESULTARRAYI* 
 
1053
          (mask-array-not-empty-processing countdown GraphData))
 
1054
     (nth *RESULTARRAYI* GraphData)))
 
1055
 
 
1056
(defthm manep-sourceVertexArray-unchanged--thm
 
1057
  (= (nth *SOURCEVERTEXARRAYI* 
 
1058
          (mask-array-not-empty-processing countdown GraphData))
 
1059
     (nth *SOURCEVERTEXARRAYI* GraphData)))
 
1060
 
 
1061
(defthm manep-vertexArray-unchanged--thm
 
1062
  (= (nth *VERTEXARRAYI*
 
1063
          (mask-array-not-empty-processing countdown GraphData))
 
1064
     (nth *VERTEXARRAYI* GraphData)))
 
1065
 
 
1066
(defthm manep-vertexCount-unchanged--thm
 
1067
  (= (car (mask-array-not-empty-processing countdown GraphData))
 
1068
     (car GraphData)))
 
1069
 
 
1070
(defthm manep-weightArray-unchanged--thm
 
1071
  (= (nth *WEIGHTARRAYI* 
 
1072
          (mask-array-not-empty-processing countdown GraphData))
 
1073
     (nth *WEIGHTARRAYI* GraphData)))
 
1074
 
 
1075
(defthm manep-preserves-GraphDatap--thm
 
1076
  (implies (GraphDatap GraphData)
 
1077
           (GraphDatap (mask-array-not-empty-processing countdown GraphData))))
 
1078
 
 
1079
(in-theory (disable mask-array-not-empty-processing))
 
1080
 
 
1081
 
 
1082
(defun copy-out-results (index-down result-num GraphData)
 
1083
  (declare (xargs :stobjs GraphData
 
1084
                  :guard (and (natp index-down)
 
1085
                              (natp result-num)
 
1086
                              (<= index-down *MAX_VERTICES*)
 
1087
                              (< result-num *MAX_SOURCES*))))
 
1088
  (cond ((not (and (mbt (GraphDatap GraphData))
 
1089
                   (mbt (natp index-down))
 
1090
                   (mbt (natp result-num))
 
1091
                   (mbt (<= index-down *MAX_VERTICES*))
 
1092
                   (mbt (< result-num *MAX_SOURCES*)))) GraphData)
 
1093
        ((mbe :logic (zp index-down)
 
1094
              :exec (int= index-down 0)) GraphData)
 
1095
        (t (seq GraphData
 
1096
                ;; Copy the result back
 
1097
                (update-ResultArrayi 
 
1098
                  (+ (* result-num *MAX_VERTICES*) (1- index-down))
 
1099
                  (costArrayi (1- index-down) GraphData) GraphData)
 
1100
                (copy-out-results (1- index-down) result-num GraphData)))))
 
1101
 
 
1102
(defthm cor-preserves-true-listp--thm
 
1103
  (IMPLIES (true-listp GraphData)
 
1104
           (TRUE-LISTP (copy-out-results index-down result-num GraphData))))
 
1105
 
 
1106
(defthm cor-preserves-len--thm
 
1107
  (implies (true-listp GraphData)
 
1108
           (= (len (copy-out-results index-down result-num GraphData))
 
1109
              (len GraphData))))
 
1110
 
 
1111
(defthm cor-costArray-unchanged--thm
 
1112
  (= (nth *COSTARRAYI* 
 
1113
          (copy-out-results index-down result-num GraphData))
 
1114
     (nth *COSTARRAYI* GraphData)))
 
1115
 
 
1116
(defthm cor-edgeArray-unchanged--thm
 
1117
  (= (nth *EDGEARRAYI* 
 
1118
          (copy-out-results index-down result-num GraphData))
 
1119
     (nth *EDGEARRAYI* GraphData)))
 
1120
 
 
1121
(defthm cor-edgeCount-unchanged--thm
 
1122
  (= (nth *EDGECOUNT* 
 
1123
          (copy-out-results index-down result-num GraphData))
 
1124
     (nth *EDGECOUNT* GraphData)))
 
1125
 
 
1126
(defthm cor-maskArray-unchanged--thm
 
1127
  (= (nth *MASKARRAYI* 
 
1128
          (copy-out-results index-down result-num GraphData))
 
1129
     (nth *MASKARRAYI* GraphData)))
 
1130
 
 
1131
(defthm cor-preserves-resultArrayp--thm
 
1132
  (implies (RESULTARRAYP (NTH *RESULTARRAYI* GraphData))
 
1133
           (RESULTARRAYP
 
1134
            (NTH *RESULTARRAYI*
 
1135
                 (copy-out-results index-down result-num GraphData)))))
 
1136
 
 
1137
(defthm cor-sourceVertexArray-unchanged--thm
 
1138
  (= (nth *SOURCEVERTEXARRAYI* 
 
1139
          (copy-out-results index-down result-num GraphData))
 
1140
     (nth *SOURCEVERTEXARRAYI* GraphData)))
 
1141
 
 
1142
(defthm cor-updatingCostArray-unchanged--thm
 
1143
  (= (nth *UPDATINGCOSTARRAYI* 
 
1144
          (copy-out-results index-down result-num GraphData))
 
1145
     (nth *UPDATINGCOSTARRAYI* GraphData)))
 
1146
 
 
1147
(defthm cor-vertexArray-unchanged--thm
 
1148
  (= (nth *VERTEXARRAYI*
 
1149
          (copy-out-results index-down result-num GraphData))
 
1150
     (nth *VERTEXARRAYI* GraphData)))
 
1151
 
 
1152
(defthm cor-vertexCount-unchanged--thm
 
1153
  (= (car (copy-out-results index-down result-num GraphData))
 
1154
     (car GraphData)))
 
1155
 
 
1156
(defthm cor-weightArray-unchanged--thm
 
1157
  (= (nth *WEIGHTARRAYI* 
 
1158
          (copy-out-results index-down result-num GraphData))
 
1159
     (nth *WEIGHTARRAYI* GraphData)))
 
1160
 
 
1161
(defthm cor-preserves-GraphDatap--thm
 
1162
  (implies (GraphDatap GraphData)
 
1163
           (GraphDatap (copy-out-results index-down result-num GraphData))))
 
1164
 
 
1165
(in-theory (disable copy-out-results))
 
1166
 
 
1167
 
 
1168
(defun APSP-helper (result-num-down GraphData) 
 
1169
  (declare (xargs :stobjs GraphData 
 
1170
                  :guard (and (natp result-num-down)
 
1171
                              (<= result-num-down *MAX_SOURCES*)
 
1172
                              (vertices-nondecreasing GraphData))))
 
1173
  (cond ((not (and (mbt (GraphDatap GraphData))
 
1174
                   (mbt (natp result-num-down))
 
1175
                   (mbt (<= result-num-down *MAX_SOURCES*)))) GraphData)
 
1176
        ((mbe :logic (zp result-num-down)
 
1177
              :exec (int= result-num-down 0)) GraphData)
 
1178
        (t (seq GraphData
 
1179
                (init-mask-cost-updating-cost *MAX_VERTICES* 
 
1180
                                              (- *MAX_SOURCES* result-num-down) 
 
1181
                                              GraphData)
 
1182
                (mask-array-not-empty-processing #xffffffff GraphData)
 
1183
                (copy-out-results *MAX_VERTICES* 
 
1184
                                  (- *MAX_SOURCES* result-num-down) GraphData)
 
1185
                (APSP-helper (1- result-num-down) GraphData)))))
 
1186
 
 
1187
 
 
1188
(defun init-source-vertex-array (index-down numResults GraphData)
 
1189
  (declare (xargs :stobjs GraphData
 
1190
                  :guard (and (natp index-down) 
 
1191
                              (natp numResults)
 
1192
                              (<= index-down *MAX_SOURCES*)
 
1193
                              (<= numResults *MAX_SOURCES*))))
 
1194
  (cond ((not (and (mbt (GraphDatap GraphData))
 
1195
                   (mbt (natp index-down))
 
1196
                   (mbt (natp numResults))
 
1197
                   (mbt (<= index-down *MAX_SOURCES*))
 
1198
                   (mbt (<= numResults *MAX_SOURCES*)))) GraphData)
 
1199
        ((mbe :logic (zp numResults)
 
1200
              :exec (int= numResults 0)) GraphData)
 
1201
        ((mbe :logic (zp index-down)
 
1202
              :exec (int= index-down 0)) GraphData)
 
1203
        (t (seq GraphData
 
1204
                (if (<= index-down numResults) 
 
1205
                    (update-SourceVertexArrayi (1- index-down) (1- index-down) 
 
1206
                                               GraphData)
 
1207
                  (update-SourceVertexArrayi (1- index-down) 0 GraphData))
 
1208
                (init-source-vertex-array (1- index-down) numResults GraphData)))))
 
1209
 
 
1210
(defthm isva-0-0--thm
 
1211
  (implies (GraphDatap GraphData)
 
1212
           (= (INIT-SOURCE-VERTEX-ARRAY 0 1 GRAPHDATA) GraphData)))
 
1213
 
 
1214
(defthm isva-0-1--thm
 
1215
  (implies (GraphDatap GraphData)
 
1216
           (= (INIT-SOURCE-VERTEX-ARRAY 0 1 GRAPHDATA) GraphData)))
 
1217
 
 
1218
(defthm isva-index-1-0--thm
 
1219
  (implies (GraphDatap GraphData)
 
1220
           (= (INIT-SOURCE-VERTEX-ARRAY 1 0 GRAPHDATA) GraphData)))
 
1221
 
 
1222
(defthm isva-1-1--thm
 
1223
  (implies (GraphDatap GraphData)
 
1224
           (= (INIT-SOURCE-VERTEX-ARRAY 1 1 GRAPHDATA)
 
1225
              (update-SourceVertexArrayi 0 0 GraphData))))
 
1226
 
 
1227
 
 
1228
(defthm isva-preserves-true-listp--thm
 
1229
  (IMPLIES (true-listp GraphData)
 
1230
           (TRUE-LISTP (init-source-vertex-array index-down numResults GraphData))))
 
1231
 
 
1232
(defthm isva-preserves-len--thm
 
1233
  (implies (true-listp GraphData)
 
1234
           (= (len (init-source-vertex-array index-down numResults GraphData))
 
1235
              (len GraphData))))
 
1236
 
 
1237
(defthm isva-costArray-unchanged--thm
 
1238
  (= (nth *COSTARRAYI* 
 
1239
          (init-source-vertex-array index-down numResults GraphData))
 
1240
     (nth *COSTARRAYI* GraphData)))
 
1241
 
 
1242
(defthm isva-edgeArray-unchanged--thm
 
1243
  (= (nth *EDGEARRAYI* 
 
1244
          (init-source-vertex-array index-down numResults GraphData))
 
1245
     (nth *EDGEARRAYI* GraphData)))
 
1246
 
 
1247
(defthm isva-edgeCount-unchanged--thm
 
1248
  (= (nth *EDGECOUNT* 
 
1249
          (init-source-vertex-array index-down numResults GraphData))
 
1250
     (nth *EDGECOUNT* GraphData)))
 
1251
 
 
1252
(defthm isva-maskArray-unchanged--thm
 
1253
  (= (nth *MASKARRAYI* 
 
1254
          (init-source-vertex-array index-down numResults GraphData))
 
1255
     (nth *MASKARRAYI* GraphData)))
 
1256
 
 
1257
(defthm isva-resultArray-unchanged--thm
 
1258
  (= (nth *RESULTARRAYI* 
 
1259
          (init-source-vertex-array index-down numResults GraphData))
 
1260
     (nth *RESULTARRAYI* GraphData)))
 
1261
 
 
1262
(defthm isva-preserves-sourceVertexArrayp--thm
 
1263
  (implies (SOURCEVERTEXARRAYP (NTH *SOURCEVERTEXARRAYI* GraphData))
 
1264
           (SOURCEVERTEXARRAYP
 
1265
            (NTH *SOURCEVERTEXARRAYI*
 
1266
                 (init-source-vertex-array index-down numResults GraphData)))))
 
1267
 
 
1268
(defthm isva-updatingCostArray-unchanged--thm
 
1269
  (= (nth *UPDATINGCOSTARRAYI* 
 
1270
          (init-source-vertex-array index-down numResults GraphData))
 
1271
     (nth *UPDATINGCOSTARRAYI* GraphData)))
 
1272
 
 
1273
(defthm isva-vertexArray-unchanged--thm
 
1274
  (= (nth *VERTEXARRAYI*
 
1275
          (init-source-vertex-array index-down numResults GraphData))
 
1276
     (nth *VERTEXARRAYI* GraphData)))
 
1277
 
 
1278
(defthm isva-vertexCount-unchanged--thm
 
1279
  (= (car (init-source-vertex-array index-down numResults GraphData))
 
1280
     (car GraphData)))
 
1281
 
 
1282
(defthm isva-weightArray-unchanged--thm
 
1283
  (= (nth *WEIGHTARRAYI* 
 
1284
          (init-source-vertex-array index-down numResults GraphData))
 
1285
     (nth *WEIGHTARRAYI* GraphData)))
 
1286
 
 
1287
(defthm isva-preserves-GraphDatap--thm
 
1288
  (implies (GraphDatap GraphData)
 
1289
           (GraphDatap (init-source-vertex-array index-down numResults GraphData))))
 
1290
 
 
1291
(in-theory (disable init-source-vertex-array))
 
1292
 
 
1293
 
 
1294
(defun init-results (index-down GraphData)
 
1295
  (declare (xargs :stobjs GraphData
 
1296
                  :guard (and (natp index-down) 
 
1297
                              (<= index-down *MAX_RESULTS*))))
 
1298
  (cond ((not (and (mbt (GraphDatap GraphData))
 
1299
                   (mbt (natp index-down))
 
1300
                   (mbt (<= index-down *MAX_RESULTS*)))) GraphData)
 
1301
        ((mbe :logic (zp index-down)
 
1302
              :exec (int= index-down 0)) GraphData)
 
1303
        (t (seq GraphData
 
1304
                (update-ResultArrayi (1- index-down) 0 GraphData)
 
1305
                (init-results (1- index-down) GraphData)))))
 
1306
 
 
1307
 
 
1308
(defthm ir-preserves-true-listp--thm
 
1309
  (IMPLIES (true-listp GraphData)
 
1310
           (TRUE-LISTP (init-results index-down GraphData))))
 
1311
 
 
1312
(defthm ir-preserves-len--thm
 
1313
  (implies (true-listp GraphData)
 
1314
           (= (len (init-results index-down GraphData))
 
1315
              (len GraphData))))
 
1316
 
 
1317
(defthm ir-costArray-unchanged--thm
 
1318
  (= (nth *COSTARRAYI* 
 
1319
          (init-results index-down GraphData))
 
1320
     (nth *COSTARRAYI* GraphData)))
 
1321
 
 
1322
(defthm ir-preserves-costArrayp--thm
 
1323
  (implies (COSTARRAYP (NTH *COSTARRAYI* GraphData))
 
1324
           (COSTARRAYP
 
1325
            (NTH *COSTARRAYI*
 
1326
                 (init-results index-down GraphData)))))
 
1327
 
 
1328
(defthm ir-edgeArray-unchanged--thm
 
1329
  (= (nth *EDGEARRAYI* 
 
1330
          (init-results index-down GraphData))
 
1331
     (nth *EDGEARRAYI* GraphData)))
 
1332
 
 
1333
(defthm ir-edgeCount-unchanged--thm
 
1334
  (= (nth *EDGECOUNT* 
 
1335
          (init-results index-down GraphData))
 
1336
     (nth *EDGECOUNT* GraphData)))
 
1337
 
 
1338
(defthm ir-maskArray-unchanged--thm
 
1339
  (= (nth *MASKARRAYI* 
 
1340
          (init-results index-down GraphData))
 
1341
     (nth *MASKARRAYI* GraphData)))
 
1342
 
 
1343
(defthm ir-preserves-resultArrayp--thm
 
1344
  (implies (RESULTARRAYP (NTH *RESULTARRAYI* GraphData))
 
1345
           (RESULTARRAYP
 
1346
            (NTH *RESULTARRAYI*
 
1347
                 (init-results index-down GraphData)))))
 
1348
 
 
1349
(defthm ir-sourceVertexArray-unchanged--thm
 
1350
  (= (nth *SOURCEVERTEXARRAYI* 
 
1351
          (init-results index-down GraphData))
 
1352
     (nth *SOURCEVERTEXARRAYI* GraphData)))
 
1353
 
 
1354
(defthm ir-updatingCostArray-unchanged--thm
 
1355
  (= (nth *UPDATINGCOSTARRAYI* 
 
1356
          (init-results index-down GraphData))
 
1357
     (nth *UPDATINGCOSTARRAYI* GraphData)))
 
1358
 
 
1359
(defthm ir-vertexArray-unchanged--thm
 
1360
  (= (nth *VERTEXARRAYI*
 
1361
          (init-results index-down GraphData))
 
1362
     (nth *VERTEXARRAYI* GraphData)))
 
1363
 
 
1364
(defthm ir-vertexCount-unchanged--thm
 
1365
  (= (car (init-results index-down GraphData))
 
1366
     (car GraphData)))
 
1367
 
 
1368
(defthm ir-weightArray-unchanged--thm
 
1369
  (= (nth *WEIGHTARRAYI* 
 
1370
          (init-results index-down GraphData))
 
1371
     (nth *WEIGHTARRAYI* GraphData)))
 
1372
 
 
1373
(defthm ir-preserves-GraphDatap--thm
 
1374
  (implies (GraphDatap GraphData)
 
1375
           (GraphDatap (init-results index-down GraphData))))
 
1376
 
 
1377
(in-theory (disable init-results))
 
1378
 
 
1379
 
 
1380
;; Top-level function
 
1381
(defun APSP (numResults GraphData)
 
1382
  (declare (xargs :stobjs GraphData 
 
1383
                  :guard (and (natp numResults) 
 
1384
                              (<= numResults *MAX_SOURCES*)
 
1385
                              (vertices-nondecreasing GraphData))))
 
1386
  (cond ((not (and (mbt (GraphDatap GraphData))
 
1387
                   (mbt (natp numResults))
 
1388
                   (mbt (<= numResults *MAX_SOURCES*)))) GraphData)
 
1389
        (t (seq GraphData
 
1390
                (init-source-vertex-array *MAX_SOURCES* numResults GraphData)
 
1391
                (init-results *MAX_RESULTS* GraphData)
 
1392
                (APSP-helper numResults GraphData)))))
 
1393
 
 
1394
;;;;;;;; Testing regime
 
1395
;;
 
1396
;; (ld "APSP.lisp" :ld-pre-eval-print t)
 
1397
;; (generateRandomGraph GraphData state)
 
1398
;; (time$ (APSP *MAX_SOURCES* GraphData))
 
1399
;;
 
1400
;; In general:
 
1401
;; (APSP <numberofsources> GraphData)
 
1402
;;
 
1403
;;;;;;;;