;;;
;;; Solution for A3 question #3
;;;
;;; By Philip W. L. Fong
;;;


(defun generate-subsets (S)
  "Generate a list of all subsets of members of list S."
  (if (null S)
      (list nil)
    (let ((S1 (generate-subsets (rest S))))
      (append S1
	      (mapcar #'(lambda (L) (cons (first S) L))
		      S1)))))

(defun generate-non-empty-subsets (S)
  "Generate a list of all non-empty subsets of members of list S."
  (remove nil (generate-subsets S)))

(defun unify-literal-list (L)
  "Given a non-empty set L of literals, return their MGU the literals
are unifiable, and 'failure otherwise."
  (if (null (rest L))
      nil
    (unify (mapcar #'make-equation (butlast L) (rest L)))))

(defun make-annotated-factor (C L)
  "Create an annotated factor containing a clause C and a literal L."
  (list C L))

(defun annotated-factor-clause (F)
  "Select the clause in an annotated factor F."
  (first F))

(defun annotated-factor-literal (F)
  "Select the literal in an annotated factor F."
  (second F))

(defun annotated-factor (C LL)
  "Given a clause C and a non-empty list LL of literals from C, return
the annotated factor of C with respect to LL if the literals in LL are 
unifiable, and return 'failure otherwise."
  (let ((mgu (unify-literal-list LL)))
    (if (eq mgu 'failure)
	mgu
      (make-annotated-factor 
       (remove-duplicates (apply-substitution mgu C) :test #'equal)
       (apply-substitution mgu (first LL))))))

(defun generate-annotated-factors (C)
  "Generate a list of all annotated factors of clause C."
  (let ((subsets (generate-non-empty-subsets C))
	(annotated-factors nil))
    (dolist (LL subsets annotated-factors)
	    (let ((F (annotated-factor C LL)))
	      (if (not (eq F 'failure))
		  (push F annotated-factors))))))

(defparameter C0 '((p ?x) (p (f ?y)) (p (g ?y)) (p (f (f ?z))) (q ?x ?y)))

(defun binary-resolvent (C1 C2 L1 L2)
  "Given a positive literal L1 and a negative literal L2 from clauses C1 
and C2 respectively, compute the binary resolvent of C1 and C2 by resolving 
upon L1 and L2.  If resolution fails then return 'failure."
  (let ((mgu (unify (list (make-equation L1 (negation-wff L2))))))
    (if (eq mgu 'failure)
	'failure
      (let ((R1 (remove L1 C1 :test #'equal))
	    (R2 (remove L2 C2 :test #'equal)))
	(remove-duplicates (append (apply-substitution mgu R1)
				   (apply-substitution mgu R2))
			   :test #'equal)))))

(defun resolve-annotated-factors (F1 F2)
  "Given a annotated factors F1 (positive) and F2 (negative), compute
their binary resolvent, or return if no such binary resolvent is defined."
  (binary-resolvent (annotated-factor-clause F1)
		    (annotated-factor-clause F2)
		    (annotated-factor-literal F1)
		    (annotated-factor-literal F2)))

(defun extract-positive-annotated-factors (FL)
  "Given a list FL of annotated factors, return a list of all annotated
factors in FL that contains a positive literal."
  (remove-if #'(lambda (F) (negation-p (annotated-factor-literal F))) 
	     FL))

(defun extract-negative-annotated-factors (FL)
  "Given a list FL of annotated factors, return a list of all annotated
factors in FL that contains a negative literal."
  (remove-if #'(lambda (F) (not (negation-p (annotated-factor-literal F)))) 
	     FL))

(defun generate-resolvents (C1 C2)
  "Generate the list of all resolvents of clauses C1 and C2."
  (let ((factors-1 (generate-annotated-factors C1))
	(factors-2 (generate-annotated-factors C2)))
    (let ((positive-1 (extract-positive-annotated-factors factors-1))
	  (negative-1 (extract-negative-annotated-factors factors-1))
	  (positive-2 (extract-positive-annotated-factors factors-2))
	  (negative-2 (extract-negative-annotated-factors factors-2))
	  (resolvents nil))
      (dolist (F1 positive-1)
	      (dolist (F2 negative-2)
		      (let ((R (resolve-annotated-factors F1 F2)))
			(if (not (eq R 'failure))
			    (push R resolvents)))))
      (dolist (F1 negative-1)
	      (dolist (F2 positive-2)
		      (let ((R (resolve-annotated-factors F2 F1)))
			(if (not (eq R 'failure))
			    (push R resolvents)))))
      resolvents)))


(defparameter C1 '((p ?x) (p (f ?y)) (q ?y)))
(defparameter C2 '((not (p (f a))) (not (q ?z))))