;;;
;;; Test Cases for Assignment 3
;;;
;;; Capture the output of the following test cases using "dribble".
;;; Hand in the output along with properly documented code.
;;;

;;
;; Test cases for SKOLEMIZE:
;;

(defparameter *skolem-1*
  '(forall ?x 
	   (exists ?u 
		   (forall ?y 
			   (exists ?v 
				   (forall ?z 
					   (and (not (p ?x ?u))
						(q (f ?y ?v ?z)))))))))

(defun skolemize-test-1 ()
  "Test case #1 for SKOLEMIZE."
  (print (skolemize *skolem-1*))
  nil)

(defparameter *skolem-2*
  '(exists ?x 
	   (forall ?u
		   (exists ?y
			   (forall ?v
				   (exists ?z
					   (or (not (p ?x ?u))
					       (q (f ?y ?v ?z)))))))))

(defun skolemize-test-2 ()
  "Test case #2 for SKOLEMIZE."
  (print (skolemize *skolem-2*))
  nil)

;;
;; Test cases for PREPROCESS:
;;

(defparameter *preprocess-1*
  '(forall ?x (and (p ?x ?x)
		   (exists ?y (=> (forall ?x (p ?x ?y))
				  (p ?y ?x))))))

(defun preprocess-test-1 ()
  "Test case #1 for PREPROCESS."
  (print (preprocess *preprocess-1*))
  nil)

(defparameter *preprocess-2*
  '(and (exists ?x (p ?x))
	(forall ?x (=> (p ?x) 
		       (exists ?y (and (> ?x ?y)
				       (p ?y)))))))

(defun preprocess-test-2 ()
  "Test case #2 for PREPROCESS."
  (print (preprocess *preprocess-2*))
  nil)
 
;;
;; Test cases for COMPOSE-SUBSTITUTIONS:
;;

(defparameter *sub-1* '((a ?x) ((f ?u (g ?v)) ?y) ((g ?v) ?z))
  "Substitution for testing COMPOSE-SUBSTITUTIONS.")

(defparameter *sub-2* '((b ?u) ((f ?x ?z) ?v) ((g ?y) ?z))
  "Substitution for testing COMPOSE-SUBSTITUTIONS.")

(defun compose-substitutions-test-1 ()
  "Test case #1 for COMPOSE-SUBSTITUTIONS."
  (compose-substitutions *sub-1* *sub-2*))

(defun compose-substitutions-test-2 ()
  "Test case #2 for COMPOSE-SUBSTITUTIONS."
  (compose-substitutions *sub-2* *sub-1*))

;;
;; Test cases for UNIFY
;;

(defparameter *wff-1* '(p (f ?x (g ?x))))
(defparameter *wff-2* '(p (f ?y ?z)))
(defparameter *wff-3* '(p (f ?z ?z)))
(defparameter *wff-4* '(p (f a (f a))))

(defun unify-test-1 ()
  "Test case #1 for UNIFY."
  (unify (list (make-equation *wff-1* *wff-2*))))

(defun unify-test-2 ()
  "Test case #2 for UNIFY."
  (unify (list (make-equation *wff-1* *wff-3*))))

(defun unify-test-3 ()
  "Test case #3 for UNIFY."
  (unify (list (make-equation *wff-1* *wff-4*))))

;;
;; Test cases for ANNOTATED-FACTOR
;;

(defparameter *af-1* '((p ?x) (p (f ?x)) (p (f ?y)) (q ?y ?z) (q ?x a)))

(defun annotated-factor-test-1 ()
  "Test case #1 for ANNOTATED-FACTOR."
  (annotated-factor *af-1* (list (first *af-1*) (third *af-1*))))

(defun annotated-factor-test-2 ()
  "Test case #2 for ANNOTATED-FACTOR."
  (annotated-factor *af-1* (list (first *af-1*) (second *af-1*))))

(defun annotated-factor-test-3 ()
  "Test case #3 for ANNOTATED-FACTOR."
  (annotated-factor *af-1* (list (first *af-1*) 
				 (second *af-1*) 
				 (third *af-1*))))

(defun annotated-factor-test-4 ()
  "Test case #4 for ANNOTATED-FACTOR."
  (annotated-factor *af-1* (list (fourth *af-1*))))

(defun annotated-factor-test-5 ()
  "Test case #5 for ANNOTATED-FACTOR."
  (annotated-factor *af-1* (list (fourth *af-1*) (fifth *af-1*))))

;;
;; Test cases for GENERATE-ANNOTATED-FACTORS
;;

(defun generate-annotated-factors-test-1 ()
  "Test case #1 for GENERATE-ANNOTATED-FACTORS."
  (print (generate-annotated-factors *af-1*))
  nil)

(defparameter *af-2*
  '((p ?u) (not (p (f ?v))) (not (p ?w)) (not (q ?u a)) (q (g ?w) ?w)))

(defun generate-annotated-factors-test-2 ()
  "Test case #2 for GENERATE-ANNOTATED-FACTORS."
  (print (generate-annotated-factors *af-2*))
  nil)

;;
;; Test cases for RESOLVE-ANNOTATED-FACTORS
;;

(defparameter *raf-1*
  '(((P ?X) (P (F ?X)) (P (F ?Y)) (Q ?Y ?Z) (Q ?X A)) 
    (Q ?X A)))

(defparameter *raf-2*
  '(((P ?U) (NOT (P (F ?V))) (NOT (P ?W)) (NOT (Q ?U A)) (Q (G ?W) ?W))
    (NOT (Q ?U A))))

(defparameter *raf-3*
  '(((P ?U) (NOT (P (F ?V))) (NOT (P ?W)) (NOT (Q ?U A)) (Q (G ?W) ?W))
    (NOT (P ?W))))

(defun resolve-annotated-factors-test-1 ()
  "Test case #1 for RESOLVE-ANNOTATED-FACTORS."
  (resolve-annotated-factors *raf-1* *raf-2*))

(defun resolve-annotated-factors-test-2 ()
  (resolve-annotated-factors *raf-1* *raf-3*))

;;
;; Test cases for GENERATE-RESOLVENTS
;;

(defun generate-resolvents-test-1 ()
  "Test case #1 for GENERATE-RESOLVENTS."
  (print (generate-resolvents *af-1* *af-2*))
  nil)

;;
;; Test cases for REFUTE
;;

(defparameter *rf-1* 
  '(((P) (Q) (R))
    ((not (Q)) (S))
    ((not (R)) (S))
    ((not (S)) (not (R)))
    ((not (S)) (not (Q)))
    ((not (P)))))

(defun refute-test-1 (depth-limit)
  "Test case #1 for REFUTE."
  (refute *rf-1* (make-dfs depth-limit nil)))

(defparameter *rf-2*
  '(((not (p ?x)) (not (p ?y)) (q ?x ?y))
    ((p a))
    ((not (q ?z ?z)))))

(defun refute-test-2 (depth-limit)
  "Test case #2 for REFUTE."
  (refute *rf-2* (make-dfs depth-limit nil)))

(defparameter *rf-3*
  '(((not (p ?x)) (p (f ?x)))
    ((p a))
    ((not (p ?x)) (not (p (f (f ?x)))))))

(defun refute-test-3 (depth-limit)
  "Test case #3 for REFUTE."
  (refute *rf-3* (make-dfs depth-limit nil)))

;;
;; Test cases for PROVE
;;

(defparameter *premises-1*
  '(and (even z)
	(and (forall ?x (=> (even ?x) (odd  (s ?x))))
	     (forall ?x (=> (odd  ?x) (even (s ?x)))))))

(defparameter *concl-1*
  '(odd (s (s (s z)))))

(defparameter *concl-2*
  '(forall ?x (=> (even ?x) (even (s (s ?x))))))

(defun prove-test-1 (depth-limit)
  "Test case #1 for PROVE."
  (prove *premises-1* *concl-1* (make-dfs depth-limit nil)))

(defun prove-test-2 (depth-limit)
  "Test case #2 for PROVE."
  (prove *premises-1* *concl-2* (make-dfs depth-limit nil)))