1 ;;; -*- Mode: LISP; Package: (PRIMORDIAL :USE CL :COLON-MODE :EXTERNAL); Base: 10; Syntax: Ansi-common-lisp -*-
3 ;;; LaHaShem HaAretz U'Mloah
5 ;;; This file contains a set of functions for testing Screamer prior to
6 ;;; release. Run the function (PRIME-ORDEAL). If it returns T and doesn't
7 ;;; produce any error messages then Screamer is probably OK.
9 ;;; CMU CommonLisp has a bug with DEFPACKAGE.
11 #-
(or poplog akcl cmu
) (in-package :screamer-user
)
13 #-
(or poplog akcl cmu
)
14 (screamer:define-screamer-package
:primordial
(:use
:iterate
))
17 (defpackage :primordial
18 (:shadowing-import-from
:screamer
:defun
:multiple-value-bind
:y-or-n-p
)
19 (:use
:cl
:screamer
:iterate
))
21 (in-package :primordial
)
25 '(screamer::defun
screamer::multiple-value-bind screamer
::y-or-n-p
))
27 #+(or poplog akcl
) (use-package '(:cl
:screamer
:iterate
))
29 (defun equal-set?
(x y
)
30 (and (subsetp x y
:test
#'equal
) (subsetp y x
:test
#'equal
)))
32 (defun attacks (qi qj distance
)
33 (or (= qi qj
) (= qi
(+ qj distance
)) (= qi
(- qj distance
))))
35 (defun check-queens (queen queens
&optional
(distance 1))
37 (if (attacks queen
(first queens
) distance
) (fail))
38 (check-queens queen
(rest queens
) (1+ distance
))))
40 (defun n-queens (n &optional queens
)
41 (if (= (length queens
) n
)
43 (let ((queen (an-integer-between 1 n
)))
44 (check-queens queen queens
)
45 (n-queens n
(cons queen queens
)))))
47 (defun test1 () (= (length (all-values (n-queens 4))) 2))
49 (defun test2 () (= (length (all-values (n-queens 8))) 92))
51 (defun a-bit () (either 0 1))
53 ;;; note: DOLIST and DOTIMES work nondeterministically because PUSH doesn't
54 ;;; destructively modify the list that is being collected so each list
55 ;;; returned as a nondeterministic value is available after backtracking.
56 ;;; note: Tests 3 through 6 are commented out since they all contain
57 ;;; nondeterministc DOTIMES and DOLIST which don't work under CMU
58 ;;; Common Lisp and I don't have time to figure out why.
61 (defun test3-internal (n)
64 (dotimes (i n
) (push (either 0 1) collection
))
69 (equal-set?
(all-values (test3-internal 2)) '((0 0) (1 0) (0 1) (1 1))))
72 (defun test4-internal (n)
73 (local (let (collection)
74 (dotimes (i n
) (push (a-bit) collection
))
79 (equal-set?
(all-values (test3-internal 2)) '((0 0) (1 0) (0 1) (1 1))))
82 (defun test5-internal (list)
83 (local (let (collection)
84 (dolist (e list
) (push (either 0 1) collection
))
89 (equal-set?
(all-values (test3-internal 2)) '((0 0) (1 0) (0 1) (1 1))))
92 (defun test6-internal (list)
93 (local (let (collection)
94 (dolist (e list
) (push (a-bit) collection
))
99 (equal-set?
(all-values (test3-internal 2)) '((0 0) (1 0) (0 1) (1 1))))
101 ;;; Problems with LOOP:
102 ;;; 1. Symbolics implementation of LOOP expands directly into RPLACD without
103 ;;; going through SETF. This foils the LOCAL declaration.
104 ;;; 2. Results disappear upon ALL-VALUES internal backtracking.
105 ;;; 3. Lucid expands LOOP into a MULTIPLE-VALUE-CALL.
108 (defun test7-internal (n) (local (loop repeat n collect
(either 0 1))))
112 (equal-set?
(all-values (test7-internal 2)) '((1 1) (0 1) (1 0) (0 0))))
115 (defun test8-internal (n) (local (loop repeat n collect
(a-bit))))
119 (equal-set?
(all-values (test8-internal 2)) '((1 1) (0 1) (1 0) (0 0))))
121 ;;; Problems with ITERATE:
122 ;;; 1. Beta conversion of (let ((#:foo nil)) (setf foo 'bar)) is unsound.
123 ;;; 2. Results disappear upon ALL-VALUES internal backtracking.
126 (defun test9-internal (n)
127 (local (iterate (repeat n
) (collect (either 0 1)))))
131 (equal-set?
(all-values (test9-internal 2)) '((1 1) (0 1) (1 0) (0 0))))
134 (defun test10-internal (n) (local (iterate (repeat n
) (collect (a-bit)))))
138 (equal-set?
(all-values (test10-internal 2)) '((1 1) (0 1) (1 0) (0 0))))
142 (local (LET* ((COUNT789)
150 (IF (<= COUNT789
0) (GO LOOP-END-NIL
))
152 (SETQ TEMP791
(LIST (A-BIT)))
156 (SETF (CDR END-POINTER790
) TEMP791
)
157 (SETQ RESULT788 TEMP791
))))
160 (SETQ COUNT789
(1- COUNT789
))
166 (let ((x (make-variable)))
167 (assert! (numberpv x
))
168 (and (known?
(numberpv x
))
169 (not (known?
(notv (numberpv x
))))
170 (not (known?
(realpv x
)))
171 (not (known?
(notv (realpv x
))))
172 (not (known?
(integerpv x
)))
173 (not (known?
(notv (integerpv x
)))))))
176 (let ((x (make-variable)))
177 (assert! (notv (numberpv x
)))
178 (and (known?
(andv (notv (numberpv x
))
180 (notv (integerpv x
))))
181 (not (known?
(numberpv x
)))
182 (not (known?
(realpv x
)))
183 (not (known?
(integerpv x
))))))
186 (let ((x (make-variable)))
188 (and (known?
(andv (numberpv x
) (realpv x
)))
189 (not (known?
(notv (numberpv x
))))
190 (not (known?
(notv (realpv x
))))
191 (not (known?
(integerpv x
)))
192 (not (known?
(notv (integerpv x
)))))))
195 (let ((x (make-variable)))
196 (assert! (notv (realpv x
)))
197 (and (known?
(andv (notv (realpv x
)) (notv (integerpv x
))))
198 (not (known?
(numberpv x
)))
199 (not (known?
(notv (numberpv x
))))
200 (not (known?
(realpv x
)))
201 (not (known?
(integerpv x
))))))
204 (let ((x (make-variable)))
205 (assert! (integerpv x
))
206 (and (known?
(andv (integerpv x
) (realpv x
) (numberpv x
)))
207 (not (known?
(notv (numberpv x
))))
208 (not (known?
(notv (realpv x
))))
209 (not (known?
(notv (integerpv x
)))))))
212 (let ((x (make-variable)))
213 (assert! (notv (integerpv x
)))
214 (and (known?
(notv (integerpv x
)))
215 (not (known?
(numberpv x
)))
216 (not (known?
(realpv x
)))
217 (not (known?
(notv (numberpv x
))))
218 (not (known?
(notv (realpv x
))))
219 (not (known?
(integerpv x
))))))
222 (let ((x (make-variable)))
223 (assert! (numberpv x
))
224 (assert! (notv (realpv x
)))
225 (and (known?
(andv (numberpv x
) (notv (realpv x
)) (notv (integerpv x
))))
226 (not (known?
(notv (numberpv x
))))
227 (not (known?
(realpv x
)))
228 (not (known?
(integerpv x
))))))
231 (let ((x (make-variable)))
232 (assert! (numberpv x
))
233 (assert! (notv (integerpv x
)))
234 (and (known?
(andv (numberpv x
) (notv (integerpv x
))))
235 (not (known?
(notv (numberpv x
))))
236 (not (known?
(realpv x
)))
237 (not (known?
(notv (realpv x
))))
238 (not (known?
(integerpv x
))))))
241 (let ((x (make-variable)))
243 (assert! (notv (integerpv x
)))
244 (and (known?
(andv (numberpv x
) (realpv x
) (notv (integerpv x
))))
245 (not (known?
(notv (numberpv x
))))
246 (not (known?
(notv (realpv x
))))
247 (not (known?
(integerpv x
))))))
250 (let ((x (make-variable)))
251 (null (all-values (assert! (numberpv x
)) (assert! (notv (numberpv x
)))))))
254 (let ((x (make-variable)))
255 (null (all-values (assert! (realpv x
)) (assert! (notv (realpv x
)))))))
258 (let ((x (make-variable)))
259 (null (all-values (assert! (integerpv x
)) (assert! (notv (integerpv x
)))))))
262 (let* ((x (make-variable))
264 (p2 (notv (numberpv x
)))
266 (p4 (notv (realpv x
)))
268 (p6 (notv (integerpv x
))))
278 (let* ((x (make-variable))
280 (p2 (notv (numberpv x
)))
282 (p4 (notv (realpv x
)))
284 (p6 (notv (integerpv x
))))
286 (and (not (known? p1
))
294 (let* ((x (make-variable))
296 (p2 (notv (numberpv x
)))
298 (p4 (notv (realpv x
)))
300 (p6 (notv (integerpv x
))))
310 (let* ((x (make-variable))
312 (p2 (notv (numberpv x
)))
314 (p4 (notv (realpv x
)))
316 (p6 (notv (integerpv x
))))
318 (and (not (known? p1
))
326 (let* ((x (make-variable))
328 (p2 (notv (numberpv x
)))
330 (p4 (notv (realpv x
)))
332 (p6 (notv (integerpv x
))))
342 (let* ((x (make-variable))
344 (p2 (notv (numberpv x
)))
346 (p4 (notv (realpv x
)))
348 (p6 (notv (integerpv x
))))
350 (and (not (known? p1
))
358 (let* ((x (make-variable))
360 (p2 (notv (numberpv x
))))
361 (null (all-values (assert! p1
) (assert! p2
)))))
364 (let ((x (make-variable)))
368 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
370 (memberv x
'(d e f
4 5 6 4.0 5.0 6.0 #c
(4 0.0) #c
(5 0.0) #c
(6 0.0))))))))
373 (let ((x (make-variable)))
375 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
377 (memberv x
'(a b c
4 5 6 4.0 5.0 6.0 #c
(4 0.0) #c
(5 0.0) #c
(6 0.0))))
378 (and (known?
(andv (notv (numberpv x
))
380 (notv (integerpv x
))))
381 (not (known?
(numberpv x
)))
382 (not (known?
(realpv x
)))
383 (not (known?
(integerpv x
))))))
386 (let ((x (make-variable)))
388 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
390 (memberv x
'(d e f
1 2 3 4.0 5.0 6.0 #c
(4 0.0) #c
(5 0.0) #c
(6 0.0))))
391 (and (known?
(andv (numberpv x
) (realpv x
) (integerpv x
)))
392 (not (known?
(notv (numberpv x
))))
393 (not (known?
(notv (realpv x
))))
394 (not (known?
(notv (integerpv x
)))))))
397 (let ((x (make-variable)))
399 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
401 (memberv x
'(d e f
4 5 6 1.0 2.0 3.0 #c
(4 0.0) #c
(5 0.0) #c
(6 0.0))))
402 (and (known?
(andv (numberpv x
) (realpv x
) (notv (integerpv x
))))
403 (not (known?
(notv (numberpv x
))))
404 (not (known?
(notv (realpv x
))))
405 (not (known?
(integerpv x
))))))
408 (let ((x (make-variable)))
410 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
412 (memberv x
'(d e f
4 5 6 4.0 5.0 6.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
413 (and (known?
(andv (numberpv x
) (notv (realpv x
)) (notv (integerpv x
))))
414 (not (known?
(notv (numberpv x
))))
415 (not (known?
(realpv x
)))
416 (not (known?
(integerpv x
))))))
419 (let ((x (make-variable)))
421 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
423 (memberv x
'(b c d
2 3 4 2.0 3.0 4.0 #c
(2 0.0) #c
(3 0.0) #c
(4 0.0))))
424 (equal-set?
(all-values (solution x
(static-ordering #'linear-force
)))
425 '(b c
2 3 2.0 3.0 #c
(2 0.0) #c
(3 0.0)))))
428 (let ((x (make-variable)))
430 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
432 (memberv x
'(b c d
2 3 4 2.0 3.0 4.0 #c
(2 0.0) #c
(3 0.0) #c
(4 0.0))))
433 (assert! (numberpv x
))
434 (equal-set?
(all-values (solution x
(static-ordering #'linear-force
)))
435 '(2 3 2.0 3.0 #c
(2 0.0) #c
(3 0.0)))))
438 (let ((x (make-variable)))
440 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
442 (memberv x
'(b c d
2 3 4 2.0 3.0 4.0 #c
(2 0.0) #c
(3 0.0) #c
(4 0.0))))
443 (assert! (notv (numberpv x
)))
444 (equal-set?
(all-values (solution x
(static-ordering #'linear-force
)))
448 (let ((x (make-variable)))
450 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
452 (memberv x
'(b c d
2 3 4 2.0 3.0 4.0 #c
(2 0.0) #c
(3 0.0) #c
(4 0.0))))
454 (equal-set?
(all-values (solution x
(static-ordering #'linear-force
)))
458 (let ((x (make-variable)))
460 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
462 (memberv x
'(b c d
2 3 4 2.0 3.0 4.0 #c
(2 0.0) #c
(3 0.0) #c
(4 0.0))))
463 (assert! (notv (realpv x
)))
464 (equal-set?
(all-values (solution x
(static-ordering #'linear-force
)))
465 '(b c
#c
(2 0.0) #c
(3 0.0)))))
468 (let ((x (make-variable)))
470 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
472 (memberv x
'(b c d
2 3 4 2.0 3.0 4.0 #c
(2 0.0) #c
(3 0.0) #c
(4 0.0))))
473 (assert! (integerpv x
))
474 (equal-set?
(all-values (solution x
(static-ordering #'linear-force
)))
478 (let ((x (make-variable)))
480 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
482 (memberv x
'(b c d
2 3 4 2.0 3.0 4.0 #c
(2 0.0) #c
(3 0.0) #c
(4 0.0))))
483 (assert! (notv (integerpv x
)))
484 (equal-set?
(all-values (solution x
(static-ordering #'linear-force
)))
485 '(b c
2.0 3.0 #c
(2 0.0) #c
(3 0.0)))))
488 (let ((x (make-variable)))
490 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
492 (memberv x
'(b c d
2 3 4 2.0 3.0 4.0 #c
(2 0.0) #c
(3 0.0) #c
(4 0.0))))
493 (assert! (numberpv x
))
494 (assert! (notv (integerpv x
)))
495 (equal-set?
(all-values (solution x
(static-ordering #'linear-force
)))
496 '(2.0
3.0 #c
(2 0.0) #c
(3 0.0)))))
499 (let ((x (make-variable)))
501 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
503 (memberv x
'(b c d
2 3 4 2.0 3.0 4.0 #c
(2 0.0) #c
(3 0.0) #c
(4 0.0))))
504 (assert! (numberpv x
))
505 (assert! (notv (realpv x
)))
506 (equal-set?
(all-values (solution x
(static-ordering #'linear-force
)))
507 '(#c
(2 0.0) #c
(3 0.0)))))
510 (let ((x (make-variable)))
512 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
514 (memberv x
'(b c d
2 3 4 2.0 3.0 4.0 #c
(2 0.0) #c
(3 0.0) #c
(4 0.0))))
516 (assert! (notv (integerpv x
)))
517 (equal-set?
(all-values (solution x
(static-ordering #'linear-force
)))
521 (let* ((x (make-variable))
523 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
525 (memberv x
'(d e f
4 5 6 4.0 5.0 6.0 #c
(4 0.0) #c
(5 0.0) #c
(6 0.0)))))
526 (null (all-values (assert! p1
) (assert! p2
)))))
529 (let* ((x (make-variable))
531 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
533 (memberv x
'(a b c
4 5 6 4.0 5.0 6.0 #c
(4 0.0) #c
(5 0.0) #c
(6 0.0))))
535 (p4 (notv (numberpv x
)))
537 (p6 (notv (realpv x
)))
539 (p8 (notv (integerpv x
))))
542 (and (not (known? p3
))
550 (let* ((x (make-variable))
552 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
554 (memberv x
'(d e f
1 2 3 4.0 5.0 6.0 #c
(4 0.0) #c
(5 0.0) #c
(6 0.0))))
556 (p4 (notv (numberpv x
)))
558 (p6 (notv (realpv x
)))
560 (p8 (notv (integerpv x
))))
571 (let* ((x (make-variable))
573 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
575 (memberv x
'(d e f
4 5 6 1.0 2.0 3.0 #c
(4 0.0) #c
(5 0.0) #c
(6 0.0))))
577 (p4 (notv (numberpv x
)))
579 (p6 (notv (realpv x
)))
581 (p8 (notv (integerpv x
))))
592 (let* ((x (make-variable))
594 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
596 (memberv x
'(d e f
4 5 6 4.0 5.0 6.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
598 (p4 (notv (numberpv x
)))
600 (p6 (notv (realpv x
)))
602 (p8 (notv (integerpv x
))))
613 (let* ((x (make-variable))
615 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
617 (memberv x
'(b c d
2 3 4 2.0 3.0 4.0 #c
(2 0.0) #c
(3 0.0) #c
(4 0.0))))
618 (p3 (memberv x
'(b c
2 3 2.0 3.0 #c
(2 0.0) #c
(3 0.0)))))
624 (let* ((x (make-variable))
626 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
628 (memberv x
'(b c d
2 3 4 2.0 3.0 4.0 #c
(2 0.0) #c
(3 0.0) #c
(4 0.0))))
629 (p3 (memberv x
'(2 3 2.0 3.0 #c
(2 0.0) #c
(3 0.0))))
637 (let* ((x (make-variable))
639 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
641 (memberv x
'(b c d
2 3 4 2.0 3.0 4.0 #c
(2 0.0) #c
(3 0.0) #c
(4 0.0))))
642 (p3 (memberv x
'(b c
)))
643 (p4 (notv (numberpv x
))))
650 (let* ((x (make-variable))
652 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
654 (memberv x
'(b c d
2 3 4 2.0 3.0 4.0 #c
(2 0.0) #c
(3 0.0) #c
(4 0.0))))
655 (p3 (memberv x
'(2 3 2.0 3.0)))
663 (let* ((x (make-variable))
665 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
667 (memberv x
'(b c d
2 3 4 2.0 3.0 4.0 #c
(2 0.0) #c
(3 0.0) #c
(4 0.0))))
668 (p3 (memberv x
'(b c
#c
(2 0.0) #c
(3 0.0))))
669 (p4 (notv (realpv x
))))
676 (let* ((x (make-variable))
678 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
680 (memberv x
'(b c d
2 3 4 2.0 3.0 4.0 #c
(2 0.0) #c
(3 0.0) #c
(4 0.0))))
681 (p3 (memberv x
'(2 3)))
689 (let* ((x (make-variable))
691 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
693 (memberv x
'(b c d
2 3 4 2.0 3.0 4.0 #c
(2 0.0) #c
(3 0.0) #c
(4 0.0))))
694 (p3 (memberv x
'(b c
2.0 3.0 #c
(2 0.0) #c
(3 0.0))))
695 (p4 (notv (integerpv x
))))
702 (let* ((x (make-variable))
704 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
706 (memberv x
'(b c d
2 3 4 2.0 3.0 4.0 #c
(2 0.0) #c
(3 0.0) #c
(4 0.0))))
707 (p3 (memberv x
'(2.0
3.0 #c
(2 0.0) #c
(3 0.0))))
708 (p4 (andv (numberpv x
) (notv (integerpv x
)))))
715 (let* ((x (make-variable))
717 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
719 (memberv x
'(b c d
2 3 4 2.0 3.0 4.0 #c
(2 0.0) #c
(3 0.0) #c
(4 0.0))))
720 (p3 (memberv x
'(#c
(2 0.0) #c
(3 0.0))))
721 (p4 (andv (numberpv x
) (notv (realpv x
)))))
728 (let* ((x (make-variable))
730 (memberv x
'(a b c
1 2 3 1.0 2.0 3.0 #c
(1 0.0) #c
(2 0.0) #c
(3 0.0))))
732 (memberv x
'(b c d
2 3 4 2.0 3.0 4.0 #c
(2 0.0) #c
(3 0.0) #c
(4 0.0))))
733 (p3 (memberv x
'(2.0
3.0)))
734 (p4 (andv (realpv x
) (notv (integerpv x
)))))
741 (let* ((x (make-variable))
742 (p1 (notv (memberv x
'(a b c d
))))
743 (p2 (memberv x
'(c d e f g h
)))
744 (p3 (notv (memberv x
'(g h i j
))))
745 (p4 (andv (memberv x
'(e f
)) (notv (memberv x
'(a b c d g h i j z
))))))
752 (let* ((x (make-variable))
753 (p1 (notv (memberv x
'(a b c d
))))
754 (p2 (memberv x
'(c d g h
)))
755 (p3 (notv (memberv x
'(g h i j
)))))
756 (null (all-values (assert! p1
) (assert! p2
) (assert! p3
)))))
759 (let ((x (an-integer-betweenv 0 4))
760 (y (an-integer-betweenv 8 12))
761 (z (a-member-ofv '(-1 6 13))))
762 (assert! (<=v x z y
))
763 (known?
(memberv z
'(6)))))
766 (let* ((x (make-variable))
769 (p1 (andv (integerpv x
) (>=v x
0) (<=v x
4)))
770 (p2 (andv (integerpv y
) (>=v y
8) (<=v y
12)))
771 (p3 (memberv z
'(-1 6 13)))
773 (p5 (andv (memberv z
'(6)) (notv (memberv z
'(-1 13))))))
780 (defun test64-internal (n)
781 (let ((q (make-array (list n n
)))
783 (iterate (for i from
0 below n
)
784 (iterate (for j from
0 below n
)
785 (setf (aref q i j
) (make-variable))
786 (assert! (booleanpv (aref q i j
)))))
787 (iterate (for i from
0 below n
)
789 (iterate (for j from
0 below n
)
790 (setf row
(orv row
(aref q i j
))))
791 (setf top
(andv top row
)))
792 (iterate (for j from
0 below n
)
794 (iterate (for i from
0 below n
)
795 (setf column
(orv column
(aref q i j
))))
796 (setf top
(andv top column
)))
798 (for i from
0 below n
)
800 (for j from
0 below n
)
802 (for k from
0 below n
)
804 (setf top
(andv top
(notv (andv (aref q i j
) (aref q i k
))))))
806 (setf top
(andv top
(notv (andv (aref q i j
) (aref q k j
))))))
807 (if (and (/= k
0) (< (+ i k
) n
) (< (+ j k
) n
))
809 (andv top
(notv (andv (aref q i j
) (aref q
(+ i k
) (+ j k
)))))))
810 (if (and (/= k
0) (< (+ i k
) n
) (>= (- j k
) 0))
812 (andv top
(notv (andv (aref q i j
) (aref q
(+ i k
) (- j k
)))))))
813 (if (and (/= k
0) (>= (- i k
) 0) (< (+ j k
) n
))
815 (andv top
(notv (andv (aref q i j
) (aref q
(- i k
) (+ j k
)))))))
816 (if (and (/= k
0) (>= (- i k
) 0) (>= (- j k
) 0))
818 (andv top
(notv (andv (aref q i j
)
819 (aref q
(- i k
) (- j k
))))))))))
825 (for i from
0 below n
)
826 (iterate (for j from
0 below n
)
827 (in outer
(collect (aref q i j
)))))
828 (static-ordering #'linear-force
))))))
830 (defun test64 () (= (test64-internal 8) 92))
832 (defun test65-internal (n)
833 (let ((q (make-array (list n n
))))
834 (iterate (for i from
0 below n
)
835 (iterate (for j from
0 below n
)
836 (setf (aref q i j
) (make-variable))
837 (assert! (booleanpv (aref q i j
)))))
838 (iterate (for i from
0 below n
)
840 (iterate (for j from
0 below n
)
841 (setf row
(orv row
(aref q i j
))))
843 (iterate (for j from
0 below n
)
845 (iterate (for i from
0 below n
)
846 (setf column
(orv column
(aref q i j
))))
849 (for i from
0 below n
)
851 (for j from
0 below n
)
853 (for k from
0 below n
)
855 (assert! (notv (andv (aref q i j
) (aref q i k
)))))
857 (assert! (notv (andv (aref q i j
) (aref q k j
)))))
858 (if (and (/= k
0) (< (+ i k
) n
) (< (+ j k
) n
))
859 (assert! (notv (andv (aref q i j
) (aref q
(+ i k
) (+ j k
))))))
860 (if (and (/= k
0) (< (+ i k
) n
) (>= (- j k
) 0))
861 (assert! (notv (andv (aref q i j
) (aref q
(+ i k
) (- j k
))))))
862 (if (and (/= k
0) (>= (- i k
) 0) (< (+ j k
) n
))
863 (assert! (notv (andv (aref q i j
) (aref q
(- i k
) (+ j k
))))))
864 (if (and (/= k
0) (>= (- i k
) 0) (>= (- j k
) 0))
865 (assert! (notv (andv (aref q i j
) (aref q
(- i k
) (- j k
)))))))))
870 (for i from
0 below n
)
871 (iterate (for j from
0 below n
)
872 (in outer
(collect (aref q i j
)))))
873 (static-ordering #'linear-force
))))))
875 (defun test65 () (= (test65-internal 8) 92))
878 (let ((x (an-integer-betweenv 1 4))
879 (y (a-member-ofv '(5 7))))
880 (known?
(funcallv #'(lambda (x y z
) (< x y z
)) x y
10))))
883 (let ((x (an-integer-betweenv 1 4))
884 (y (a-member-ofv '(5 7))))
885 (known?
(notv (funcallv #'(lambda (x y z
) (> x y z
)) x y
10)))))
888 (let ((w (an-integer-betweenv 1 4))
889 (x (a-member-ofv '(5 7)))
890 (y (a-member-ofv '(8 10))))
891 (known?
(applyv #'(lambda (w x y z
) (< w x y z
)) w x
(list y
11)))))
894 (let ((w (an-integer-betweenv 1 4))
895 (x (a-member-ofv '(5 7)))
896 (y (a-member-ofv '(8 10))))
897 (known?
(notv (applyv #'(lambda (w x y z
) (> w x y z
)) w x
(list y
11))))))
899 (defun prime-ordeal ()
901 (unless (test1) (format t
"~% Test 1 failed") (setf bug? t
))
902 (unless (test2) (format t
"~% Test 2 failed") (setf bug? t
))
903 (unless (test11) (format t
"~% Test 11 failed") (setf bug? t
))
904 (unless (test12) (format t
"~% Test 12 failed") (setf bug? t
))
905 (unless (test13) (format t
"~% Test 13 failed") (setf bug? t
))
906 (unless (test14) (format t
"~% Test 14 failed") (setf bug? t
))
907 (unless (test15) (format t
"~% Test 15 failed") (setf bug? t
))
908 (unless (test16) (format t
"~% Test 16 failed") (setf bug? t
))
909 (unless (test17) (format t
"~% Test 17 failed") (setf bug? t
))
910 (unless (test18) (format t
"~% Test 18 failed") (setf bug? t
))
911 (unless (test19) (format t
"~% Test 19 failed") (setf bug? t
))
912 (unless (test20) (format t
"~% Test 20 failed") (setf bug? t
))
913 (unless (test21) (format t
"~% Test 21 failed") (setf bug? t
))
914 (unless (test22) (format t
"~% Test 22 failed") (setf bug? t
))
915 (unless (test23) (format t
"~% Test 23 failed") (setf bug? t
))
916 (unless (test24) (format t
"~% Test 24 failed") (setf bug? t
))
917 (unless (test25) (format t
"~% Test 25 failed") (setf bug? t
))
918 (unless (test26) (format t
"~% Test 26 failed") (setf bug? t
))
919 (unless (test27) (format t
"~% Test 27 failed") (setf bug? t
))
920 (unless (test28) (format t
"~% Test 28 failed") (setf bug? t
))
921 (unless (test29) (format t
"~% Test 29 failed") (setf bug? t
))
922 (unless (test30) (format t
"~% Test 30 failed") (setf bug? t
))
923 (unless (test31) (format t
"~% Test 31 failed") (setf bug? t
))
924 (unless (test32) (format t
"~% Test 32 failed") (setf bug? t
))
925 (unless (test33) (format t
"~% Test 33 failed") (setf bug? t
))
926 (unless (test34) (format t
"~% Test 34 failed") (setf bug? t
))
927 (unless (test35) (format t
"~% Test 35 failed") (setf bug? t
))
928 (unless (test36) (format t
"~% Test 36 failed") (setf bug? t
))
929 (unless (test37) (format t
"~% Test 37 failed") (setf bug? t
))
930 (unless (test38) (format t
"~% Test 38 failed") (setf bug? t
))
931 (unless (test39) (format t
"~% Test 39 failed") (setf bug? t
))
932 (unless (test40) (format t
"~% Test 40 failed") (setf bug? t
))
933 (unless (test41) (format t
"~% Test 41 failed") (setf bug? t
))
934 (unless (test42) (format t
"~% Test 42 failed") (setf bug? t
))
935 (unless (test43) (format t
"~% Test 43 failed") (setf bug? t
))
936 (unless (test44) (format t
"~% Test 44 failed") (setf bug? t
))
937 (unless (test45) (format t
"~% Test 45 failed") (setf bug? t
))
938 (unless (test46) (format t
"~% Test 46 failed") (setf bug? t
))
939 (unless (test47) (format t
"~% Test 47 failed") (setf bug? t
))
940 (unless (test48) (format t
"~% Test 48 failed") (setf bug? t
))
941 (unless (test49) (format t
"~% Test 49 failed") (setf bug? t
))
942 (unless (test50) (format t
"~% Test 50 failed") (setf bug? t
))
943 (unless (test51) (format t
"~% Test 51 failed") (setf bug? t
))
944 (unless (test52) (format t
"~% Test 52 failed") (setf bug? t
))
945 (unless (test53) (format t
"~% Test 53 failed") (setf bug? t
))
946 (unless (test54) (format t
"~% Test 54 failed") (setf bug? t
))
947 (unless (test55) (format t
"~% Test 55 failed") (setf bug? t
))
948 (unless (test56) (format t
"~% Test 56 failed") (setf bug? t
))
949 (unless (test57) (format t
"~% Test 57 failed") (setf bug? t
))
950 (unless (test58) (format t
"~% Test 58 failed") (setf bug? t
))
951 (unless (test59) (format t
"~% Test 59 failed") (setf bug? t
))
952 (unless (test60) (format t
"~% Test 60 failed") (setf bug? t
))
953 (unless (test61) (format t
"~% Test 61 failed") (setf bug? t
))
954 (unless (test62) (format t
"~% Test 62 failed") (setf bug? t
))
955 (unless (test63) (format t
"~% Test 63 failed") (setf bug? t
))
956 (unless (test64) (format t
"~% Test 64 failed") (setf bug? t
))
957 (unless (test65) (format t
"~% Test 65 failed") (setf bug? t
))
958 (unless (test66) (format t
"~% Test 66 failed") (setf bug? t
))
959 (unless (test67) (format t
"~% Test 67 failed") (setf bug? t
))
960 (unless (test68) (format t
"~% Test 68 failed") (setf bug? t
))
961 (unless (test69) (format t
"~% Test 69 failed") (setf bug? t
))
962 (if bug?
(error "Screamer has a bug")))
965 ;;; Tam V'Nishlam Shevah L'El Borei Olam