;;; CSE 341, 99su
;;; Assignment 2:  Scheme/Boolean Formulas
;;; sample solutions for simplify and normalize
;;; original code by Trevor Olson, revised by Amir Michail


;;
;; simplify
;;


;; The "and" and "or" rules are similar so handle them together.
;; Argument "type" indicates whether this is an "and" or "or" expression.
(define (and-or x y type)
  (let ((temp (eq? type 'and)))
    (cond
     ((equal? x y) x)                      ; (and x x) => x, (or x x) => x
     ((equal? x temp) y)                   ; (and #t y) => y, (or #f y) => y
     ((equal? x (not temp)) (not temp))    ; (and #f y) => #f, (or #t y) => #t
     ((pair? y) (cond
		 ((equal? y (list 'not x))
		  (not temp))       ; (and x (not x)) => #f, (or x (not x)) => #t
		 ((and (equal? (car y) (if temp 'or 'and))
		       (or (equal? x (cadr y)) (equal? x (caddr y))))
		  x)                ; (and x (or x y)) => x, (or x (and x y)) => x
		 (else 'nosimp)))
     (else 'nosimp))))

;; This function tries out both argument orders for "and" and "or".
;; Argument "type" indicates whether this is an "and" or "or" expression.
(define (and-or-simp x y type)
  (let ((left-first (and-or x y type)))
     (if (not (eq? left-first 'nosimp)) left-first
	 (let ((right-first (and-or y x type)))
	   (if (not (eq? right-first 'nosimp)) right-first
	       (list type x y))))))


;; simplify "not" expression
(define (not-simp x)
  (cond 
   ((pair? x) (if (eq? 'not (car x)) 
		  (cadr x)           ; (not (not x)) => x
		  (list 'not x))) 
   ((eq? x #t) #f)                   ; (not #t) => #f
   ((eq? x #f) #t)                   ; (not #f) => #t
   (else (list 'not x))))

;; main simplify function
;; calls helper-functions depending on type of expression
;; (Observe how the arguments are simplified recursively before we attempt to
;;  simplify the top-level expression.)
(define (simplify x)
  (cond
   ((not (pair? x)) x)
   ((equal? 'and (car x)) (and-or-simp (simplify (cadr x)) (simplify (caddr x)) 'and))
   ((equal? 'or (car x)) (and-or-simp (simplify (cadr x)) (simplify (caddr x)) 'or))
   ((equal? 'not (car x)) (not-simp (simplify (cadr x))))
   (else x)))






;; BONUS
;; 
;;
;; normalize
;;

;;
;;
;; some helper functions
;;
;;

;; get operator in top-level expression 
(define (get-op f)
  (if (list? f) (car f) f))

;; get arguments for operator
(define (get-args f)
  (if (list? f) (cdr f) '()))

;; a literal is of the form "variable" or "(not variable)"
(define (literal-clause? f)
  (or (not (list? f)) 
      (and (list? f) (eq? (first f) 'not) (not (list? (second f))))))

;; get conjuncts
(define (conjuncts s)
  (cond ((eq? (get-op s) 'and) (get-args s))
	((eq? s #t) '())
	(else (list s))))

;; get disjuncts
(define (disjuncts s)
  (cond ((eq? (get-op s) 'or) (get-args s))
	((eq? s #f) '())
	(else (list s))))

;; form a (simplified) conjunction
(define (conjunction args)
  (if (= (length args) 0)
      #t
      (if (= (length args) 1)
	  (first args)
	  (cons 'and args))))

;; form a (simplified) disjunction
(define (disjunction args)
  (if (= (length args) 0)
      #f
      (if (= (length args) 1)
	  (first args)
	  (cons 'or args))))


;; move "not" inwards in the expression; uses DeMorgan
(define (move-not-inwards f)
  (let ((op (get-op f))
	(args (get-args f)))
    (cond ((eq? op #t)
	   #f)
	  ((eq? op #f)
	   #t)
	  ((eq? op 'not)
	   (first args))
	  ((eq? op 'and)
	   (disjunction (map move-not-inwards args)))
	  ((eq? op 'or)
	   (conjunction (map move-not-inwards args)))
	  (else (list 'not f)))))

;; helper functions

(define (iterate-e2 x e2)
  (if (null? e2) '()
      (append (list (conjunction (append (conjuncts x) (conjuncts (car e2))))) (iterate-e2 x (cdr e2)))))

(define (iterate-e1 e1 e2)
  (if (null? e1) '()
      (append (iterate-e2 (car e1) e2) (iterate-e1 (cdr e1) e2))))

;; return a DNF expression for the conjunction
;; example:  (merge-conjuncts '((or w x) (or y z))) 
;;              => (or (and w y) (and w y) (and x y) (and x z))
;; uses the distributive law
(define (merge-conjuncts conjuncts)
  (if (= (length conjuncts) 0) #t
      (if (= (length conjuncts) 1)
	  (first conjuncts)
	  (let ((e1 (disjuncts (car conjuncts)))
		(e2 (disjuncts (merge-conjuncts (cdr conjuncts)))))
	    ; for example, e1 = (w x), e2 = (y z)
	    (disjunction (iterate-e1 e1 e2))))))

;; top-level function
;;
;; recursively normalizes arguments 
;;
(define (normalize f)
  (let ((op (get-op f))
	(args (get-args f)))
    (cond ((eq? op 'not)
	   (let ((f2 (move-not-inwards (first args))))
	     (if (literal-clause? f2) f2 (normalize f2))))
	  ((eq? op 'or)
	   (disjunction (apply append (map (lambda (q) (disjuncts (normalize q))) args))))
	  ((eq? op 'and)
	   (merge-conjuncts (map normalize args)))
	  (else f))))