;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; simplify test data

;;; the calls below should evaluate to the following:
;;;
;;;   x
;;;   (not (and (or x (not y)) (not (or x y))))
;;;   (and x z)
;;;   (or x y)
;;;   #t
;;;   #f
;;;   (or x y)
;;;   (and x z)
;;;   (not (and (or x (not y)) (not (or x y))))
;;;  
;;;   x
;;;   y
;;;   z
;;;   e
;;;   f
;;;   g
;;;   h
;;;   #f
;;;   #t
;;;   #f


;;; from the handout
(simplify '(and x x))
(simplify '(not (and (or x (not y)) (not (and (not #f) (or x y))))))
(simplify '(and (and (or #f (and x x)) (and z (or z x))) (or (not w) w)))
(simplify '(or (and (or #t x) (or x x)) (not (or (and (not y) x) (not y)))))
(simplify '(or (not #t) (or (not x) x)))
(simplify '(or (and #f x) (and (not z) z)))
(simplify '(or (and (or #t x) (or x x)) (not (or (and (not y) x) (not y)))))
(simplify '(and (and (or #f (and x x)) (and z (or z x))) (or (not w) w)))
(simplify '(not (and (or x (not y)) (not (and (not #f) (or x y))))))


;;; further testing 
(simplify `
(and (and (and (and (and (and (and x x) (and x x)) (and (and x x) (and x x))) (and (and (and x x) (and x x)) (and (and x x) (and x x)))) (and (and (and (and x x) (and x x)) (and (and x x) (and x x))) (and (and (and x x) (and x x)) (and (and x x) (and x x))))) (and (and (and (and (and x x) (and x x)) (and (and x x) (and x x))) (and (and (and x x) (and x x)) (and (and x x) (and x x)))) (and (and (and (and x x) (and x x)) (and (and x x) (and x x))) (and (and (and x x) (and x x)) (and (and x x) (and x x)))))) (and (and (and (and (and (and x x) (and x x)) (and (and x x) (and x x))) (and (and (and x x) (and x x)) (and (and x x) (and x x)))) (and (and (and (and x x) (and x x)) (and (and x x) (and x x))) (and (and (and x x) (and x x)) (and (and x x) (and x x))))) (and (and (and (and (and x x) (and x x)) (and (and x x) (and x x))) (and (and (and x x) (and x x)) (and (and x x) (and x x)))) (and (and (and (and x x) (and x x)) (and (and x x) (and x x))) (and (and (and x x) (and x x)) (and (and x x) (and x x)))))))
)

(simplify `
(or (or (or (or (or (or (or y y) (or y y)) (or (or y y) (or y y))) (or (or (or y y) (or y y)) (or (or y y) (or y y)))) (or (or (or (or y y) (or y y)) (or (or y y) (or y y))) (or (or (or y y) (or y y)) (or (or y y) (or y y))))) (or (or (or (or (or y y) (or y y)) (or (or y y) (or y y))) (or (or (or y y) (or y y)) (or (or y y) (or y y)))) (or (or (or (or y y) (or y y)) (or (or y y) (or y y))) (or (or (or y y) (or y y)) (or (or y y) (or y y)))))) (or (or (or (or (or (or y y) (or y y)) (or (or y y) (or y y))) (or (or (or y y) (or y y)) (or (or y y) (or y y)))) (or (or (or (or y y) (or y y)) (or (or y y) (or y y))) (or (or (or y y) (or y y)) (or (or y y) (or y y))))) (or (or (or (or (or y y) (or y y)) (or (or y y) (or y y))) (or (or (or y y) (or y y)) (or (or y y) (or y y)))) (or (or (or (or y y) (or y y)) (or (or y y) (or y y))) (or (or (or y y) (or y y)) (or (or y y) (or y y)))))))
)

(simplify '(not (not (not (not (not (not (not (not (not (not (not (not (not (not (not (not (not (not (not (not (not (not (not (not (not (not z)))))))))))))))))))))))))))

(simplify '(and e (or e2 e)))
(simplify '(and f (or f e2)))
(simplify '(or g (and e2 g)))
(simplify '(or h (and h e2)))

(simplify (quote 
(and (and (and (and bar (not (and foo #f))) bar) (not bar)) (or (and (and (and bar (not (and foo #f))) bar) (not bar)) blah))
))

(simplify (quote 
(or (or bar (or (not (or foo #t)) bar)) (not (or bar (and bar blah))))
))

(simplify (quote 
(not (not (and (and (and (and bar (not (and foo #f))) bar) (not bar)) (or (and (and (and bar (not (and foo #f))) bar) (not bar)) blah))) (not (or (or bar (or (not (or foo #t)) bar)) (not (or bar (and bar blah))))))
))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; normalize test data

;;; the calls below should evaluate to the following:
;;;
;;;  (or (and x (not x) y)
;;; 	 (and x (not x) z)
;;; 	 (and x z y)
;;; 	 (and x z z)
;;; 	 (and y (not x) y)
;;; 	 (and y (not x) z)
;;; 	 (and y z y)
;;; 	 (and y z z))
;;;  (or (and a a a)
;;; 	 (and a a (not c))
;;; 	 (and a a (not d))
;;; 	 (and a (not b) a)
;;; 	 (and a (not b) (not c))
;;; 	 (and a (not b) (not d))
;;; 	 (and (not b) a a)
;;; 	 (and (not b) a (not c))
;;; 	 (and (not b) a (not d))
;;; 	 (and (not b) (not b) a)
;;; 	 (and (not b) (not b) (not c))
;;; 	 (and (not b) (not b) (not d))
;;; 	 (and c a a)
;;; 	 (and c a (not c))
;;; 	 (and c a (not d))
;;; 	 (and c (not b) a)
;;; 	 (and c (not b) (not c))
;;; 	 (and c (not b) (not d)))
;;;  (or (and x y z q z)
;;; 	 (and x y z (not w))
;;; 	 (and (not y) (not x) q z)
;;; 	 (and (not y) (not x) (not w))
;;; 	 (and (not y) (not z) q z)
;;; 	 (and (not y) (not z) (not w))
;;; 	 (and (not z) (not x) q z)
;;; 	 (and (not z) (not x) (not w))
;;; 	 (and (not z) (not z) q z)
;;; 	 (and (not z) (not z) (not w)))
;;;  (or (and (not x) w (not a) (not x) (not w))
;;; 	 (and (not x) w (not b) (not c) (not x) (not w))
;;; 	 (and (not x) w (not c) (not x) (not w))
;;; 	 (and (not q) (not w) (not a) (not x) (not w))
;;; 	 (and (not q) (not w) (not b) (not c) (not x) (not w))
;;; 	 (and (not q) (not w) (not c) (not x) (not w)))
;;;
;;; (or (and e1 e3) (and e2 e3))
;;; (or (and e1 e3) (and (not e2) e3))
;;; (and e3 (not e1) (not e2))
;;; (or a b c d e)
;;; (or b c (and a b) (and a c))


;;; from the handout
(normalize '(and (or x y) (or (not x) z) (or y z)))
(normalize '(and (or a (not b) c) (or a (not b)) (or a (not c) (not d))))
(normalize '(and (or (and x y z) (not (or (and y z) (and (or x) z)))) (or (and q z) (not w))))
(normalize '(not (or (or (and (or (and x) (not w)) (or q w))  (and a (or b c) c)) (or x w))))


(normalize '(and (or e1 e2) e3))
(normalize '(and (or e1 (not e2)) e3))
(normalize '(and e3 (not (or e1 e2))))
(normalize '(or a b c d e))
(normalize '(and (or #t a) (or b c)))