;;;
;;; Wang Algorithm
;;; programmed by Stuart C. Shapiro [shapiro@cs.buffalo.edu]
;;;               July 8, 1994
;;; predicate-wang added August 29, 1995
;;;
;;; Use and redistribution is unlimited
;;; as long as these comments are retained.
;;;
;;;  <logical connectives>:  -  &  or  =>  <=>
;;;  <quantifiers>: all exists
;;;  <variables>: determined by use in quantifier clause
;;;
;;; External functions: (wang TrueWffs FalseWffs)
;;;                     (predicate-wang TrueWffs FalseWffs Terms)
;;;
;;; Syntax of wffs:
;;;
;;; wff ::= atomic-wff |
;;;         (~ wff) |
;;;         (wff & wff)
;;;         (wff or wff)
;;;         (wff => wff)
;;;         (wff <=> wff)
;;;         (all variable wff)
;;;         (exists variable wff)
;;; atomic-wff ::= any Lisp form not of any of the above formats
;;; variable ::= any Lisp symbol not also used for another purpose
;;; term ::= any Lisp symbol
;;;
(defpackage wang
  (:shadow common-lisp:variable)
  (:export wang predicate-wang addwff))

(in-package wang)

(defun unary-operator (wff)
  (first wff))

(defun operator (wff)
  (second wff))

(defun unary-operand (wff)
  (second wff))

(defun first-operand (wff)
  (first wff))

(defun second-operand (wff)
  (third wff))

(defun quantifier (wff)
  (first wff))

(defun variable (wff)
  (second wff))

(defun scope (wff)
  (third wff))

(defun has-symbol-name (symbol name)
  (and (symbolp symbol)
       (string-equal (symbol-name symbol) name)))

(defun negation (wff)
  (has-symbol-name (unary-operator wff) "~"))

(defun conjunction (wff)
  (has-symbol-name (operator wff) "&"))

(defun disjunction (wff)
  (has-symbol-name (operator wff) "or"))

(defun implication (wff)
  (has-symbol-name (operator wff) "=>"))

(defun biconditional (wff)
  (has-symbol-name (operator wff) "<=>"))

(defun u-quantified-wff (wff)
  (has-symbol-name (quantifier wff) "all"))

(defun e-quantified-wff (wff)
  (has-symbol-name (quantifier wff) "exists"))

(defun unary-opd (wff)
  (negation wff))

(defun binary-opd (wff)
  (or (conjunction wff) (disjunction wff)
      (implication wff) (biconditional wff)))

(defun quantified (wff)
  (or (u-quantified-wff wff) (e-quantified-wff wff)))

(defun atomic (wff)
  (or (atom wff)
      (not (or (unary-opd wff) (binary-opd wff) (quantified wff)))))

(defun addwff (wff wfflist)
  (adjoin wff wfflist :test #'equal))

(defun predicate-wang (TrueWffs FalseWffs Terms) 
  "Returns True if no way to make consistent truth value assignments.
   Calls wang after expanding all universally quantified wffs into
   conjunctions of all ground instances, and expanding all existentially
   quantified wffs into disjunctions of all ground instances."
  (wang (mapcar #'(lambda (wff) (expand wff Terms)) TrueWffs)
	(mapcar #'(lambda (wff) (expand wff Terms)) FalseWffs)))

(defun expand (wff Terms)
  "Expands all quantified subformulas of wff into conjunctions or
   disjunctions of all ground instances."
  (cond ((atom wff) wff)
	((unary-opd wff)
	 (list (unary-operator wff)
	       (expand (unary-operand wff) Terms)))
	((binary-opd wff)
	 (list (expand (first-operand wff) Terms)
	       (operator wff)
	       (expand (second-operand wff) Terms)))
	((quantified wff)
	 (make-ground-wffs (expand (scope wff) Terms)
			   (variable wff)
			   Terms
			   (if (u-quantified-wff wff) '& 'or)))
	(t (mapcar #'(lambda (wff) (expand wff Terms)) wff))))

(defun make-ground-wffs (wff variable Terms con-or-dis-junction)
  "Returns a conjunction or disjunction, using con-or-dis-junction,
   of all ground instances of the open wff."
  (let ((result (subst (first Terms) variable wff)))
    (dolist (term (rest Terms) result)
      (setf result (list (subst term variable wff)
			 con-or-dis-junction
			 result)))))

(defun wang (TrueWffs FalseWffs)
  "Returns True if no way to make consistent truth value assignments."
  (if (intersection TrueWffs FalseWffs :test #'equal) t
    (let (wff)
      (cond ((setf wff (find-if-not #'atomic TrueWffs))
	     (cond ((negation wff)
		    (wang (remove wff TrueWffs)
			  (addwff (unary-operand wff) FalseWffs)))
		   ((conjunction wff)
		    (wang (addwff (first-operand wff)
				  (addwff (second-operand wff)
					  (remove wff TrueWffs)))
			  FalseWffs))
		   ((disjunction wff)
		    (and (wang (addwff (first-operand wff)
				       (remove wff TrueWffs))
			       FalseWffs)
			 (wang (addwff (second-operand wff)
				       (remove wff TrueWffs))
			       FalseWffs)))
		   ((implication wff)
		    (and (wang (addwff (second-operand wff)
				       (remove wff TrueWffs))
			       FalseWffs)
			 (wang (remove wff TrueWffs)
			       (addwff (first-operand wff) FalseWffs))))
		   ((biconditional wff)
		    (and (wang (addwff (first-operand wff)
				       (addwff (second-operand wff)
					       (remove wff TrueWffs)))
			       FalseWffs)
			 (wang (remove wff TrueWffs)
			       (addwff (first-operand wff)
				       (addwff (second-operand wff)
					       (remove wff FalseWffs))))))
		   ))
	    ((setf wff (find-if-not #'atomic FalseWffs))
	     (cond ((negation wff)
		    (wang (addwff (unary-operand wff) TrueWffs)
			  (remove wff FalseWffs)))
		   ((conjunction wff)
		    (and (wang Truewffs (addwff (first-operand wff)
						(remove wff Falsewffs)))
			 (wang Truewffs (addwff (second-operand wff)
						(remove wff Falsewffs)))))
		   ((disjunction wff)
		    (wang TrueWffs
			  (addwff (first-operand wff)
				  (addwff (second-operand wff)
					  (remove wff FalseWffs)))))
		   ((implication wff)
		    (wang (addwff (first-operand wff) TrueWffs)
			  (addwff (second-operand wff)
				  (remove wff FalseWffs))))
		   ((biconditional wff)
		    (and (wang (addwff (first-operand wff) TrueWffs)
			       (addwff (second-operand wff)
				       (remove wff FalseWffs)))
			 (wang (addwff (second-operand wff) TrueWffs)
			       (addwff (first-operand wff)
				       (remove wff FalseWffs)))))))
	    (t nil)))))