; The "tests" function tests EVERYTHING!
(defun tests ()
        (progn
        (princ "-----------------------------------------") (terpri)
        (easy-cnf)
        (hard-cnf)
        (easy-simplification)
        (hard-simplification)
        (combination)  )  )

; The "easy-cnf" function tests simple cases of conversion to CNF,
; where one conversion rule has to be applied once only.
(defun easy-cnf ()
        (progn
        (princ "Single-rule CNF tests:") (terpri) (terpri)
        (test-cnf '(implies p q))
        (test-cnf '(implies p (not q)))
        (test-cnf '(implies true false))
        (test-cnf '(not (and p q)))
        (test-cnf '(not (and p q r)))
        (test-cnf '(not (or p q)))
        (test-cnf '(not (or p q r)))
        (test-cnf '(not (and (not p) (not q))))
        (test-cnf '(not (or true) false))
        (test-cnf '(or p (and q r)))
        (test-cnf '(or (and p q) (and r s)))  )  )

; The "hard-cnf" function tests hard cases of conversion to CNF,
; where multiple conversion rules may be needed, in some order,
; and rules may be needed more than once.
(defun hard-cnf ()
        (progn
        (princ "Multiple-rule CNF tests:") (terpri) (terpri)
        (test-cnf '(and (implies a b) (implies c d)))
        (test-cnf '(implies p (implies q r)))
        (test-cnf '(not (and (or a b) (or c d))))
        (test-cnf '(not (or (and p q) (and r s))))
        (test-cnf '(or (and a b) (and c d)))
        (test-cnf '(and (and a b) (or c d)))
        (test-cnf '(or a (or b c)))  )  )

; The "easy-simplification" function tests easy cases of simplification,
; where one simplification rule has to be applied once only.
(defun easy-simplification ()
        (progn
        (princ "Single-step simplifications:") (terpri) (terpri)
        (test-simplify '(and p p))
        (test-simplify '(or p p))
        (test-simplify '(not (not p)))
        (test-simplify '(and false p))
        (test-simplify '(or true p))
        (test-simplify '(and true p))
        (test-simplify '(or false p))
        (test-simplify '(or p (not p)))
        (test-simplify '(or (not p) p))
        (test-simplify '(and p (not p)))
        (test-simplify '(and (not p) p))
        (test-simplify '(and (or p q) (not (or p q))))  )  )

; The "hard-simplification" function tests hard cases of function
; simplification, where multiple simplification rules may be needed,
; in some order, and rules may be needed more than once.
(defun hard-simplification ()
        (progn
        (princ "Multiple-step simplification:") (terpri) (terpri)
        (test-simplify '(and (or p p) (or p p)))
        (test-simplify '(and p (not (not p))))
        (test-simplify '(or (and true (not true)) (or false (not false))))
        (test-simplify '(or (and (not p) true) (and true p)))  )  )

; The "combination" function tests expressions that should be
; converted to CNF and also simplified.
(defun combination ()
        (progn
        (princ "Conversion to CNF and simplification:") (terpri) (terpri)
        (test-combination '(implies (not (and p q)) (or (not p) (not q))))
        (test-combination '(and (implies (and p (not q)) q) (not p)))
        (test-combination
            '(implies (and (implies p q) (implies q r)) (implies p r)) )
        (test-combination '(and (implies p q) (not (or (not p) q))))  )  )

; The "test-cnf" function prints out its argument, then (on a
; separate line) prints out the result of calling "to-cnf" with
; its argument, and finally prints a blank line. If your function
; for converting an expression to CNF form is named "to-cnf",
; you can use this function as is; otherwise, change the call
; in the fourth line to call your function rather than "to-cnf".
(defun test-cnf (expr)
        (progn
        (princ "input: ") (prin1 expr) (terpri)
        (princ "CNF:   ") (prin1 (to-cnf expr)) (terpri)
        (terpri)  )  )

; The "test-simplify" function prints out its argument, then (on a
; separate line) prints out the result of calling "simplify" with
; its argument, and finally prints a blank line. If your function
; for simplifying an expression is named "simplify",  you can use
; this function as is; otherwise, change the call in the fourth line
; to call your function rather than "simplify".
(defun test-simplify (expr)
        (progn
        (princ "input:   ") (prin1 expr) (terpri)
        (princ "simpler: ") (prin1 (simplify expr)) (terpri)
        (terpri)  )  )

; The "combination" function prints out its argument, then (on a
; separate line) prints out the result of calling "to-cnf" with
; its argument, then the result of calling "simplify" with the
; CNF expression, and finally prints a blank line. If your functions
; are named "to-cnf" and "simplify", you can use this function as is,
; otherwise chang the names of the functions that this one calls
(defun test-combination (expr)
        (progn
        (princ "input:   ") (prin1 expr) (terpri)
        (princ "CNF:     ") (prin1 (to-cnf expr)) (terpri)
        (princ "simpler: ") (prin1 (simplify (to-cnf expr))) (terpri)
        (terpri)  )  )

; This is the BEGINNING of a function to turn an arbitrary logical
; expression into a logical expression in Conjunctive Normal Form
; (CNF). At the moment, all it does is replace (IMPLIES P Q) with
; (OR (NOT P) Q).
(defun to-cnf (expr)
        (recursive-apply 'remove-implies expr)  )

; This is the BEGINNING of a function to simplify an arbitrary
; logical expression. At the moment, all it does is replace a
; contradiction such as (AND P (NOT P)) with FALSE.
(defun simplify (expr)
        (recursive-apply 'simplify-contradiction expr)  )

; If the argument to "remove-implies" is a list of the form
; (IMPLIES P Q), for arbitrarily complex P and Q, then the
; result is (OR (NOT P) Q). Any other argument is returned
; unchanged.
(defun remove-implies (expr)
        (cond
        ((atom expr) expr)
        ((eq (car expr) 'IMPLIES)
            (list 'OR (list 'NOT (cadr expr)) (caddr expr))  )
        (t expr)  )  )

; If the argument to "simplify-contradiction" is a list whose
; CAR is AND and whose CDR contains both P and (NOT P), for
; some P, then the result is FALSE, otherwise the result is
; the same as the input argument. Notice that this function
; compares the two P's for identity, not logical equivalence.
(defun simplify-contradiction (expr) 
        (cond
        ((null expr) ())
        ((eq (car expr) 'AND)
            (cond
            ((contains-both-x-and-not-x (cdr expr))  'FALSE)
            (t expr)  )  )
        (t expr)  )  )

; Test whether an S-expression occurs in a list. Like MEMBER, but
; the first argument can be anything, not just an atom.
(defun contains (x list)
        (cond
        ((null list) nil)
        ((equal x (car list)) t)
        (t (contains x (cdr list)))  )  )

; Test whether the given expression contains both X and (NOT X),
; for some (unknown) S-expression X.
(defun contains-both-x-and-not-x (expr)
        (cond
        ((null expr)  nil)
        (t (or
            ; Test for (P ... (NOT P) ...)
            (contains (list 'NOT (car expr)) (cdr expr))
            ; Test for ((NOT P) ... P ...)
            (and (not (atom (car expr)))
                 (equal (caar expr) 'NOT)
                 (contains (cadar expr) (cdr expr)) )
            ; Car is useless; test cdr
            (contains-both-x-and-not-x (cdr expr))  ))  )  )

; Recursively apply the function f to every top-level list element
; of expression x, then apply f to the result.
(defun recursive-apply (f x)
        (cond
        ((atom x) x)
        (t (apply f (list (cons (recursive-apply f (car x))
                                (recursive-apply f (cdr x))  ))))  )  )