;;; -*- Mode: LISP; Package: (PRIMORDIAL :USE CL :COLON-MODE :EXTERNAL); Base: 10; Syntax: Ansi-common-lisp -*-

;;; LaHaShem HaAretz U'Mloah

;;; This file contains a set of functions for testing Screamer prior to
;;; release. Run the function (PRIME-ORDEAL). If it returns T and doesn't
;;; produce any error messages then Screamer is probably OK.

#||#(in-package :cl-user)

(screamer:define-screamer-package :primordial (:use :iterate))

(in-package :primordial)

(defun attacks (qi qj distance)
 (or (= qi qj) (= qi (+ qj distance)) (= qi (- qj distance))))

(defun check-queens (queen queens &optional (distance 1))
 (unless (null queens)
  (if (attacks queen (first queens) distance) (fail))
  (check-queens queen (rest queens) (1+ distance))))

(defun n-queens (n &optional queens)
 (if (= (length queens) n)
     queens
     (let ((queen (an-integer-between 1 n)))
      (check-queens queen queens)
      (n-queens n (cons queen queens)))))

(defun test1 () (= (length (all-values (n-queens 4))) 2))

(defun test2 () (= (length (all-values (n-queens 8))) 92))

(defun a-bit () (either 0 1))

;;; note: DOLIST and DOTIMES work nondeterministically because PUSH doesn't
;;;       destructively modify the list that is being collected so each list
;;;       returned as a nondeterministic value is available after backtracking.

(defun test3-internal (n)
 (local
  (let (collection)
   ;; note: MCL 2.0 mistakingly thinks that I is referenced.
   (dotimes (i n) #-mcl (declare (ignore i)) (push (either 0 1) collection))
   collection)))

(defun test3 ()
 (equal (all-values (test3-internal 2)) '((0 0) (1 0) (0 1) (1 1))))

(defun test4-internal (n)
 (local (let (collection)
         ;; note: MCL 2.0 mistakingly thinks that I is referenced.
	 (dotimes (i n) #-mcl (declare (ignore i)) (push (a-bit) collection))
	 collection)))

(defun test4 ()
 (equal (all-values (test3-internal 2)) '((0 0) (1 0) (0 1) (1 1))))

(defun test5-internal (list)
 (local (let (collection)
	 (dolist (e list) (push (either 0 1) collection))
	 collection)))

(defun test5 ()
 (equal (all-values (test3-internal 2)) '((0 0) (1 0) (0 1) (1 1))))

(defun test6-internal (list)
 (local (let (collection)
	 (dolist (e list) (push (a-bit) collection))
	 collection)))

(defun test6 ()
 (equal (all-values (test3-internal 2)) '((0 0) (1 0) (0 1) (1 1))))

;;; Problems with LOOP:
;;;  1. Symbolics implementation of LOOP expands directly into RPLACD without
;;;     going through SETF. This foils the LOCAL declaration.
;;;  2. Results disappear upon ALL-VALUES internal backtracking.
;;;  3. Lucid expands LOOP into a MULTIPLE-VALUE-CALL.

;;(defun test7-internal (n) (local (loop repeat n collect (either 0 1))))

;;(defun test7 ()
;; (equal (all-values (test7-internal 2)) '((1 1) (0 1) (1 0) (0 0))))

;;(defun test8-internal (n) (local (loop repeat n collect (a-bit))))

;;(defun test8 ()
;; (equal (all-values (test8-internal 2)) '((1 1) (0 1) (1 0) (0 0))))

;;; Problems with ITERATE:
;;;  1. Beta conversion of (let ((#:foo nil)) (setf foo 'bar)) is unsound.
;;;  2. Results disappear upon ALL-VALUES internal backtracking.

;;(defun test9-internal (n)
;; (local (iterate (repeat n) (collect (either 0 1)))))

;;(defun test9 ()
;; (equal (all-values (test9-internal 2)) '((1 1) (0 1) (1 0) (0 0))))

;;(defun test10-internal (n) (local (iterate (repeat n) (collect (a-bit)))))

;;(defun test10 ()
;; (equal (all-values (test10-internal 2)) '((1 1) (0 1) (1 0) (0 0))))

(defun bar (n)
 (local (LET* ((COUNT789)
	       (RESULT788)
	       (END-POINTER790)
	       (TEMP791))
	 (BLOCK NIL
	  (TAGBODY
	     (SETQ COUNT789 N)
           LOOP-TOP-NIL
	     (IF (<= COUNT789 0) (GO LOOP-END-NIL))
	     (PROGN
	      (SETQ TEMP791 (LIST (A-BIT)))
	      (IF TEMP791
		  (SETQ END-POINTER790
			(IF RESULT788
			    (SETF (CDR END-POINTER790) TEMP791)
			    (SETQ RESULT788 TEMP791))))
	      RESULT788)
           LOOP-STEP-NIL
	     (SETQ COUNT789 (1- COUNT789))
	     (GO LOOP-TOP-NIL)
           LOOP-END-NIL)
	  RESULT788))))

(defun test11 ()
 (let ((x (make-variable)))
  (assert! (numberpv x))
  (and (known? (numberpv x))
       (not (known? (notv (numberpv x))))
       (not (known? (realpv x)))
       (not (known? (notv (realpv x))))
       (not (known? (integerpv x)))
       (not (known? (notv (integerpv x)))))))

(defun test12 ()
 (let ((x (make-variable)))
  (assert! (notv (numberpv x)))
  (and (known? (andv (notv (numberpv x))
		     (notv (realpv x))
		     (notv (integerpv x))))
       (not (known? (numberpv x)))
       (not (known? (realpv x)))
       (not (known? (integerpv x))))))

(defun test13 ()
 (let ((x (make-variable)))
  (assert! (realpv x))
  (and (known? (andv (numberpv x) (realpv x)))
       (not (known? (notv (numberpv x))))
       (not (known? (notv (realpv x))))
       (not (known? (integerpv x)))
       (not (known? (notv (integerpv x)))))))

(defun test14 ()
 (let ((x (make-variable)))
  (assert! (notv (realpv x)))
  (and (known? (andv (notv (realpv x)) (notv (integerpv x))))
       (not (known? (numberpv x)))
       (not (known? (notv (numberpv x))))
       (not (known? (realpv x)))
       (not (known? (integerpv x))))))

(defun test15 ()
 (let ((x (make-variable)))
  (assert! (integerpv x))
  (and (known? (andv (integerpv x) (realpv x) (numberpv x)))
       (not (known? (notv (numberpv x))))
       (not (known? (notv (realpv x))))
       (not (known? (notv (integerpv x)))))))

(defun test16 ()
 (let ((x (make-variable)))
  (assert! (notv (integerpv x)))
  (and (known? (notv (integerpv x)))
       (not (known? (numberpv x)))
       (not (known? (realpv x)))
       (not (known? (notv (numberpv x))))
       (not (known? (notv (realpv x))))
       (not (known? (integerpv x))))))

(defun test17 ()
 (let ((x (make-variable)))
  (assert! (numberpv x))
  (assert! (notv (realpv x)))
  (and (known? (andv (numberpv x) (notv (realpv x)) (notv (integerpv x))))
       (not (known? (notv (numberpv x))))
       (not (known? (realpv x)))
       (not (known? (integerpv x))))))

(defun test18 ()
 (let ((x (make-variable)))
  (assert! (numberpv x))
  (assert! (notv (integerpv x)))
  (and (known? (andv (numberpv x) (notv (integerpv x))))
       (not (known? (notv (numberpv x))))
       (not (known? (realpv x)))
       (not (known? (notv (realpv x))))
       (not (known? (integerpv x))))))

(defun test19 ()
 (let ((x (make-variable)))
  (assert! (realpv x))
  (assert! (notv (integerpv x)))
  (and (known? (andv (numberpv x) (realpv x) (notv (integerpv x))))
       (not (known? (notv (numberpv x))))
       (not (known? (notv (realpv x))))
       (not (known? (integerpv x))))))

(defun test20 ()
 (let ((x (make-variable)))
  (null (all-values (assert! (numberpv x)) (assert! (notv (numberpv x)))))))

(defun test21 ()
 (let ((x (make-variable)))
  (null (all-values (assert! (realpv x)) (assert! (notv (realpv x)))))))

(defun test22 ()
 (let ((x (make-variable)))
  (null (all-values (assert! (integerpv x)) (assert! (notv (integerpv x)))))))

(defun test23 ()
 (let* ((x (make-variable))
	(p1 (numberpv x))
	(p2 (notv (numberpv x)))
	(p3 (realpv x))
	(p4 (notv (realpv x)))
	(p5 (integerpv x))
	(p6 (notv (integerpv x))))
  (assert! p1)
  (and (known? p1)
       (not (known? p2))
       (not (known? p3))
       (not (known? p4))
       (not (known? p5))
       (not (known? p6)))))

(defun test24 ()
 (let* ((x (make-variable))
	(p1 (numberpv x))
	(p2 (notv (numberpv x)))
	(p3 (realpv x))
	(p4 (notv (realpv x)))
	(p5 (integerpv x))
	(p6 (notv (integerpv x))))
  (assert! p2)
  (and (not (known? p1))
       (known? p2)
       (not (known? p3))
       (known? p4)
       (not (known? p5))
       (known? p6))))

(defun test25 ()
 (let* ((x (make-variable))
	(p1 (numberpv x))
	(p2 (notv (numberpv x)))
	(p3 (realpv x))
	(p4 (notv (realpv x)))
	(p5 (integerpv x))
	(p6 (notv (integerpv x))))
  (assert! p3)
  (and (known? p1)
       (not (known? p2))
       (known? p3)
       (not (known? p4))
       (not (known? p5))
       (not (known? p6)))))

(defun test26 ()
 (let* ((x (make-variable))
	(p1 (numberpv x))
	(p2 (notv (numberpv x)))
	(p3 (realpv x))
	(p4 (notv (realpv x)))
	(p5 (integerpv x))
	(p6 (notv (integerpv x))))
  (assert! p4)
  (and (not (known? p1))
       (not (known? p2))
       (not (known? p3))
       (known? p4)
       (not (known? p5))
       (known? p6))))

(defun test27 ()
 (let* ((x (make-variable))
	(p1 (numberpv x))
	(p2 (notv (numberpv x)))
	(p3 (realpv x))
	(p4 (notv (realpv x)))
	(p5 (integerpv x))
	(p6 (notv (integerpv x))))
  (assert! p5)
  (and (known? p1)
       (not (known? p2))
       (known? p3)
       (not (known? p4))
       (known? p5)
       (not (known? p6)))))

(defun test28 ()
 (let* ((x (make-variable))
	(p1 (numberpv x))
	(p2 (notv (numberpv x)))
	(p3 (realpv x))
	(p4 (notv (realpv x)))
	(p5 (integerpv x))
	(p6 (notv (integerpv x))))
  (assert! p6)
  (and (not (known? p1))
       (not (known? p2))
       (not (known? p3))
       (not (known? p4))
       (not (known? p5))
       (known? p6))))

(defun test29 ()
 (let* ((x (make-variable))
	(p1 (numberpv x))
	(p2 (notv (numberpv x))))
  (null (all-values (assert! p1) (assert! p2)))))

(defun test30 ()
 (let ((x (make-variable)))
  (null
   (all-values
    (assert!
     (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))))
    (assert!
     (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))))))))

(defun test31 ()
 (let ((x (make-variable)))
  (assert!
   (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))))
  (assert!
   (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))))
  (and (known? (andv (notv (numberpv x))
		     (notv (realpv x))
		     (notv (integerpv x))))
       (not (known? (numberpv x)))
       (not (known? (realpv x)))
       (not (known? (integerpv x))))))

(defun test32 ()
 (let ((x (make-variable)))
  (assert!
   (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))))
  (assert!
   (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))))
  (and (known? (andv (numberpv x) (realpv x) (integerpv x)))
       (not (known? (notv (numberpv x))))
       (not (known? (notv (realpv x))))
       (not (known? (notv (integerpv x)))))))

(defun test33 ()
 (let ((x (make-variable)))
  (assert!
   (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))))
  (assert!
   (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))))
  (and (known? (andv (numberpv x) (realpv x) (notv (integerpv x))))
       (not (known? (notv (numberpv x))))
       (not (known? (notv (realpv x))))
       (not (known? (integerpv x))))))

(defun test34 ()
 (let ((x (make-variable)))
  (assert!
   (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))))
  (assert!
   (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))))
  (and (known? (andv (numberpv x) (notv (realpv x)) (notv (integerpv x))))
       (not (known? (notv (numberpv x))))
       (not (known? (realpv x)))
       (not (known? (integerpv x))))))

(defun test35 ()
 (let ((x (make-variable)))
  (assert!
   (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))))
  (assert!
   (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))))
  (equal (all-values (solution x (static-ordering #'linear-force)))
	 '(b c 2 3 2.0 3.0 #c(2 0.0) #c(3 0.0)))))

(defun test36 ()
 (let ((x (make-variable)))
  (assert!
   (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))))
  (assert!
   (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))))
  (assert! (numberpv x))
  (equal (all-values (solution x (static-ordering #'linear-force)))
	 '(2 3 2.0 3.0 #c(2 0.0) #c(3 0.0)))))

(defun test37 ()
 (let ((x (make-variable)))
  (assert!
   (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))))
  (assert!
   (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))))
  (assert! (notv (numberpv x)))
  (equal (all-values (solution x (static-ordering #'linear-force))) '(b c))))

(defun test38 ()
 (let ((x (make-variable)))
  (assert!
   (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))))
  (assert!
   (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))))
  (assert! (realpv x))
  (equal (all-values (solution x (static-ordering #'linear-force)))
	 '(2 3 2.0 3.0))))

(defun test39 ()
 (let ((x (make-variable)))
  (assert!
   (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))))
  (assert!
   (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))))
  (assert! (notv (realpv x)))
  (equal (all-values (solution x (static-ordering #'linear-force)))
	 '(b c #c(2 0.0) #c(3 0.0)))))

(defun test40 ()
 (let ((x (make-variable)))
  (assert!
   (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))))
  (assert!
   (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))))
  (assert! (integerpv x))
  (equal (all-values (solution x (static-ordering #'linear-force))) '(2 3))))

(defun test41 ()
 (let ((x (make-variable)))
  (assert!
   (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))))
  (assert!
   (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))))
  (assert! (notv (integerpv x)))
  (equal (all-values (solution x (static-ordering #'linear-force)))
	 '(b c 2.0 3.0 #c(2 0.0) #c(3 0.0)))))

(defun test42 ()
 (let ((x (make-variable)))
  (assert!
   (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))))
  (assert!
   (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))))
  (assert! (numberpv x))
  (assert! (notv (integerpv x)))
  (equal (all-values (solution x (static-ordering #'linear-force)))
	 '(2.0 3.0 #c(2 0.0) #c(3 0.0)))))

(defun test43 ()
 (let ((x (make-variable)))
  (assert!
   (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))))
  (assert!
   (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))))
  (assert! (numberpv x))
  (assert! (notv (realpv x)))
  (equal (all-values (solution x (static-ordering #'linear-force)))
	 '(#c(2 0.0) #c(3 0.0)))))

(defun test44 ()
 (let ((x (make-variable)))
  (assert!
   (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))))
  (assert!
   (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))))
  (assert! (realpv x))
  (assert! (notv (integerpv x)))
  (equal (all-values (solution x (static-ordering #'linear-force)))
	 '(2.0 3.0))))

(defun test45 ()
 (let* ((x (make-variable))
	(p1
	 (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))))
	(p2
	 (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)))))
  (null (all-values (assert! p1) (assert! p2)))))

(defun test46 ()
 (let* ((x (make-variable))
	(p1
	 (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))))
	(p2
	 (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))))
	(p3 (numberpv x))
	(p4 (notv (numberpv x)))
	(p5 (realpv x))
	(p6 (notv (realpv x)))
	(p7 (integerpv x))
	(p8 (notv (integerpv x))))
  (assert! p1)
  (assert! p2)
  (and (not (known? p3))
       (known? p4)
       (not (known? p5))
       (known? p6)
       (not (known? p7))
       (known? p8))))

(defun test47 ()
 (let* ((x (make-variable))
	(p1
	 (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))))
	(p2
	 (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))))
	(p3 (numberpv x))
	(p4 (notv (numberpv x)))
	(p5 (realpv x))
	(p6 (notv (realpv x)))
	(p7 (integerpv x))
	(p8 (notv (integerpv x))))
  (assert! p1)
  (assert! p2)
  (and (known? p3)
       (not (known? p4))
       (known? p5)
       (not (known? p6))
       (known? p7)
       (not (known? p8)))))

(defun test48 ()
 (let* ((x (make-variable))
	(p1
	 (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))))
	(p2
	 (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))))
	(p3 (numberpv x))
	(p4 (notv (numberpv x)))
	(p5 (realpv x))
	(p6 (notv (realpv x)))
	(p7 (integerpv x))
	(p8 (notv (integerpv x))))
  (assert! p1)
  (assert! p2)
  (and (known? p3)
       (not (known? p4))
       (known? p5)
       (not (known? p6))
       (not (known? p7))
       (known? p8))))

(defun test49 ()
 (let* ((x (make-variable))
	(p1
	 (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))))
	(p2
	 (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))))
	(p3 (numberpv x))
	(p4 (notv (numberpv x)))
	(p5 (realpv x))
	(p6 (notv (realpv x)))
	(p7 (integerpv x))
	(p8 (notv (integerpv x))))
  (assert! p1)
  (assert! p2)
  (and (known? p3)
       (not (known? p4))
       (not (known? p5))
       (known? p6)
       (not (known? p7))
       (known? p8))))

(defun test50 ()
 (let* ((x (make-variable))
	(p1
	 (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))))
	(p2
	 (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))))
	(p3 (memberv x '(b c 2 3 2.0 3.0 #c(2 0.0) #c(3 0.0)))))
  (assert! p1)
  (assert! p2)
  (known? p3)))

(defun test51 ()
 (let* ((x (make-variable))
	(p1
	 (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))))
	(p2
	 (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))))
	(p3 (memberv x '(2 3 2.0 3.0 #c(2 0.0) #c(3 0.0))))
	(p4 (numberpv x)))
  (assert! p1)
  (assert! p2)
  (assert! p4)
  (known? p3)))

(defun test52 ()
 (let* ((x (make-variable))
	(p1
	 (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))))
	(p2
	 (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))))
	(p3 (memberv x '(b c)))
	(p4 (notv (numberpv x))))
  (assert! p1)
  (assert! p2)
  (assert! p4)
  (known? p3)))

(defun test53 ()
 (let* ((x (make-variable))
	(p1
	 (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))))
	(p2
	 (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))))
	(p3 (memberv x '(2 3 2.0 3.0)))
	(p4 (realpv x)))
  (assert! p1)
  (assert! p2)
  (assert! p4)
  (known? p3)))

(defun test54 ()
 (let* ((x (make-variable))
	(p1
	 (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))))
	(p2
	 (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))))
	(p3 (memberv x '(b c #c(2 0.0) #c(3 0.0))))
	(p4 (notv (realpv x))))
  (assert! p1)
  (assert! p2)
  (assert! p4)
  (known? p3)))

(defun test55 ()
 (let* ((x (make-variable))
	(p1
	 (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))))
	(p2
	 (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))))
	(p3 (memberv x '(2 3)))
	(p4 (integerpv x)))
  (assert! p1)
  (assert! p2)
  (assert! p4)
  (known? p3)))

(defun test56 ()
 (let* ((x (make-variable))
	(p1
	 (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))))
	(p2
	 (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))))
	(p3 (memberv x '(b c 2.0 3.0 #c(2 0.0) #c(3 0.0))))
	(p4 (notv (integerpv x))))
  (assert! p1)
  (assert! p2)
  (assert! p4)
  (known? p3)))

(defun test57 ()
 (let* ((x (make-variable))
	(p1
	 (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))))
	(p2
	 (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))))
	(p3 (memberv x '(2.0 3.0 #c(2 0.0) #c(3 0.0))))
	(p4 (andv (numberpv x) (notv (integerpv x)))))
  (assert! p1)
  (assert! p2)
  (assert! p4)
  (known? p3)))

(defun test58 ()
 (let* ((x (make-variable))
	(p1
	 (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))))
	(p2
	 (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))))
	(p3 (memberv x '(#c(2 0.0) #c(3 0.0))))
	(p4 (andv (numberpv x) (notv (realpv x)))))
  (assert! p1)
  (assert! p2)
  (assert! p4)
  (known? p3)))

(defun test59 ()
 (let* ((x (make-variable))
	(p1
	 (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))))
	(p2
	 (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))))
	(p3 (memberv x '(2.0 3.0)))
	(p4 (andv (realpv x) (notv (integerpv x)))))
  (assert! p1)
  (assert! p2)
  (assert! p4)
  (known? p3)))

(defun test60 ()
 (let* ((x (make-variable))
	(p1 (notv (memberv x '(a b c d))))
	(p2 (memberv x '(c d e f g h)))
	(p3 (notv (memberv x '(g h i j))))
	(p4 (andv (memberv x '(e f)) (notv (memberv x '(a b c d g h i j z))))))
  (assert! p1)
  (assert! p2)
  (assert! p3)
  (known? p4)))

(defun test61 ()
 (let* ((x (make-variable))
	(p1 (notv (memberv x '(a b c d))))
	(p2 (memberv x '(c d g h)))
	(p3 (notv (memberv x '(g h i j)))))
  (null (all-values (assert! p1) (assert! p2) (assert! p3)))))

(defun test62 ()
 (let ((x (an-integer-betweenv 0 4))
       (y (an-integer-betweenv 8 12))
       (z (a-member-ofv '(-1 6 13))))
  (assert! (<=v x z y))
  (known? (memberv z '(6)))))

(defun test63 ()
 (let* ((x (make-variable))
	(y (make-variable))
	(z (make-variable))
	(p1 (andv (integerpv x) (>=v x 0) (<=v x 4)))
	(p2 (andv (integerpv y) (>=v y 8) (<=v y 12)))
	(p3 (memberv z '(-1 6 13)))
	(p4 (<=v x z y))
	(p5 (andv (memberv z '(6)) (notv (memberv z '(-1 13))))))
  (assert! p1)
  (assert! p2)
  (assert! p3)
  (assert! p4)
  (known? p5)))

(defun test64-internal (n)
 (let ((q (make-array (list n n)))
       (top t))
  (iterate (for i from 0 below n)
	   (iterate (for j from 0 below n)
		    (setf (aref q i j) (make-variable))
		    (assert! (booleanpv (aref q i j)))))
  (iterate (for i from 0 below n)
	   (for row = nil)
	   (iterate (for j from 0 below n)
		    (setf row (orv row (aref q i j))))
	   (setf top (andv top row)))
  (iterate (for j from 0 below n)
	   (for column = nil)
	   (iterate (for i from 0 below n)
		    (setf column (orv column (aref q i j))))
	   (setf top (andv top column)))
  (iterate
   (for i from 0 below n)
   (iterate
    (for j from 0 below n)
    (iterate
     (for k from 0 below n)
     (if (/= j k)
	 (setf top (andv top (notv (andv (aref q i j) (aref q i k))))))
     (if (/= i k)
	 (setf top (andv top (notv (andv (aref q i j) (aref q k j))))))
     (if (and (/= k 0) (< (+ i k) n) (< (+ j k) n))
	 (setf top
	       (andv top (notv (andv (aref q i j) (aref q (+ i k) (+ j k)))))))
     (if (and (/= k 0) (< (+ i k) n) (>= (- j k) 0))
	 (setf top
	       (andv top (notv (andv (aref q i j) (aref q (+ i k) (- j k)))))))
     (if (and (/= k 0) (>= (- i k) 0) (< (+ j k) n))
	 (setf top
	       (andv top (notv (andv (aref q i j) (aref q (- i k) (+ j k)))))))
     (if (and (/= k 0) (>= (- i k) 0) (>= (- j k) 0))
	 (setf top
	       (andv top (notv (andv (aref q i j)
				     (aref q (- i k) (- j k))))))))))
  (assert! top)
  (length
   (all-values
    (solution
     (iterate outer
	      (for i from 0 below n)
	      (iterate (for j from 0 below n)
		       (in outer (collect (aref q i j)))))
     (static-ordering #'linear-force))))))

(defun test64 () (= (test64-internal 8) 92))

(defun test65-internal (n)
 (let ((q (make-array (list n n))))
  (iterate (for i from 0 below n)
	   (iterate (for j from 0 below n)
		    (setf (aref q i j) (make-variable))
		    (assert! (booleanpv (aref q i j)))))
  (iterate (for i from 0 below n)
	   (for row = nil)
	   (iterate (for j from 0 below n)
		    (setf row (orv row (aref q i j))))
	   (assert! row))
  (iterate (for j from 0 below n)
	   (for column = nil)
	   (iterate (for i from 0 below n)
		    (setf column (orv column (aref q i j))))
	   (assert! column))
  (iterate
   (for i from 0 below n)
   (iterate
    (for j from 0 below n)
    (iterate
     (for k from 0 below n)
     (if (/= j k)
	 (assert! (notv (andv (aref q i j) (aref q i k)))))
     (if (/= i k)
	 (assert! (notv (andv (aref q i j) (aref q k j)))))
     (if (and (/= k 0) (< (+ i k) n) (< (+ j k) n))
	 (assert! (notv (andv (aref q i j) (aref q (+ i k) (+ j k))))))
     (if (and (/= k 0) (< (+ i k) n) (>= (- j k) 0))
	 (assert! (notv (andv (aref q i j) (aref q (+ i k) (- j k))))))
     (if (and (/= k 0) (>= (- i k) 0) (< (+ j k) n))
	 (assert! (notv (andv (aref q i j) (aref q (- i k) (+ j k))))))
     (if (and (/= k 0) (>= (- i k) 0) (>= (- j k) 0))
	 (assert! (notv (andv (aref q i j) (aref q (- i k) (- j k)))))))))
  (length
   (all-values
    (solution
     (iterate outer
	      (for i from 0 below n)
	      (iterate (for j from 0 below n)
		       (in outer (collect (aref q i j)))))
     (static-ordering #'linear-force))))))

(defun test65 () (= (test65-internal 8) 92))

(defun test66 ()
 (let ((x (an-integer-betweenv 1 4))
       (y (a-member-ofv '(5 7))))
  (known? (funcallv #'(lambda (x y z) (< x y z)) x y 10))))

(defun test67 ()
 (let ((x (an-integer-betweenv 1 4))
       (y (a-member-ofv '(5 7))))
  (known? (notv (funcallv #'(lambda (x y z) (> x y z)) x y 10)))))

(defun test68 ()
 (let ((w (an-integer-betweenv 1 4))
       (x (a-member-ofv '(5 7)))
       (y (a-member-ofv '(8 10))))
  (known? (applyv #'(lambda (w x y z) (< w x y z)) w x (list y 11)))))

(defun test69 ()
 (let ((w (an-integer-betweenv 1 4))
       (x (a-member-ofv '(5 7)))
       (y (a-member-ofv '(8 10))))
  (known? (notv (applyv #'(lambda (w x y z) (> w x y z)) w x (list y 11))))))

(defun prime-ordeal ()
 (unless (and (test1) (test2) (test3) (test4) (test5) (test6)
	      (test11) (test12) (test13) (test14) (test15) (test16) (test17)
	      (test18) (test19) (test20) (test21) (test22) (test23) (test24)
	      (test25) (test26) (test27) (test28) (test29) (test30) (test31)
	      (test32) (test33) (test34) (test35) (test36) (test37) (test38)
	      (test39) (test40) (test41) (test42) (test43) (test44) (test45)
	      (test46) (test47) (test48) (test49) (test50) (test51) (test52)
	      (test53) (test54) (test55) (test56) (test57) (test58) (test59)
	      (test60) (test61) (test62) (test63) (test64) (test65) (test66)
	      (test67) (test68) (test69))
  (error "Screamer has a bug"))
 t)

;;; Tam V'Nishlam Shevah L'El Borei Olam