;;; EXAMPLE AT END OF FILE!
;;;
;;; Use the FOLProblem structure to construct your logic problem. Then,
;;; pass it to translate-FOL-CNF to construct a CNF version of the problem.
;;; This version will be ready to use as the CNF part of a SAT problem.
;;;
;;; Construct the FOL statement using the following rules:
;;;
;;; <statement> => NIL | <clause>
;;;   NOTE: the NIL statement is trivially TRUE
;;; <clause> => <connector-clause> | <implies-clause> | <quantified-clause> | 
;;;             <not-clause> | <term>
;;;
;;; <connector-clause> => '(' <connector> <clause>* ')'
;;; <connector> => ':OR' | ':AND'
;;;    NOTE: an empty :OR is equivalent to FALSE, an empty :AND to TRUE
;;;
;;; <implies-clause> => '(' ':IMPLIES' <clause> <clause> ')'
;;;
;;; <not-clause> => '(' ':NOT' <clause> ')'
;;;
;;; Note that quantified clauses' variable list look a lot like a
;;; let statements declaration list.
;;; <quantified-clause> => '(' <quantifier> <var-list> <clause> ')'
;;; <quantifier> => ':FORALL' | ':EXISTS'
;;; <var-list> => '(' <var-pair>* ')'
;;; <var-pair> => '(' <var> <type> ')'
;;; <var> => valid variable name (a '?' followed by a string of characters)
;;; <type> => valid type name (member of the type list in this problem)
;;;
;;; <term> => '(' <pred> <arg>* ')'
;;; <pred> => valid predicate name (member of the predicates list in this problem)
;;; <arg> => valid object in the appropriate place in this predicate (member of the
;;;             object list of the type of this place of the predicate)
;;;
;;;
;;; Predicate lists should be of the form:
;;;
;;; '(' <pred-desc>* ')'
;;;
;;; <pred-desc> => '(' <pred> <type>* ')'
;;; 
;;; Where the <pred> is the name of the predicate and the <type> fields are the
;;; types of the predicate's arguments. N.B.: DO NOT declare the eq predicate. It
;;; is automatically declared and defined for you! (Note: currently there is no 
;;; type checking, so use caution with your predicates!)
;;;
;;; Type lists should be of the form:
;;;
;;; '(' <type-desc>* ')'
;;;
;;; <type-desc> => '(' <type> <obj>* ')'
;;; <obj> => an object of the type described
;;;
;;; Where each type descriptor specifies first the type name and then the members
;;; of that type.
;;;
;;; See also the example at the end of this file.

;; Some helper functions

;; returns T iff token passed in is a keyword
(defun keyword? (sym)
  (or (eq sym :AND)
      (eq sym :OR)
      (eq sym :IMPLIES)
      (eq sym :NOT)
      (eq sym :FORALL)
      (eq sym :EXISTS)))

;; returns T iff token passed in is a (possibly invalid) variable
(defun var? (sym)
  (and (symbolp sym)
       (char= (char (symbol-name sym) 0) #\?)))

;; returns T iff token passed in is a valid predicate
(defun pred? (prob sym)
  (when (not (FOLProblem-p prob))
    (error "Attempt to use pred? with a non-FOLProblem first arg"))
  (or
   (eq sym 'eq)
   (member sym (FOLProblem-preds prob) :key #'first))
  )

;; returns T iff token passed in is a valid type
(defun type? (prob sym)
  (when (not (FOLProblem-p prob))
    (error "Attempt to use type? with a non-FOLProblem first arg"))
  (member sym (FOLProblem-types prob) :key #'first)
  )

;; returns T iff token passed in is a valid symbol of the given type
;; in the given FOLProblem
(defun object? (prob type sym)
  (when (not (FOLProblem-p prob))
    (error "Attempt to use pred? with a non-FOLProblem first arg"))
  (when (not (type? prob type))
    (error "Attempt to use object? with a nonexistant type"))
  (let ((type-objs (rest (find type (FOLProblem-types prob) :key #'first))))
    (member sym type-objs)))


;; The primary structure, representing a first order logic problem.
(defstruct FOLProblem
  (preds NIL)				; a list of the predicates in this 
					; problem of the form:
					; ( (pred1 typea1 typeb1 typec1 ...)
					;   (pred2 typea2 typeb2 typec2 ...)
					;   ...)
					; Note that equality is built in!
  (types NIL)				; a list of the types in this problem 
					; along with their objects of the
					; form:
					; ( (typea objecta1 objecta2 ...)
					;   (typeb objectb1 objectb2 ...)
					;   ...)
  (statement NIL)			; the statements of this problem in 
					; the form described at the start
					; of this file.
  )

;; This function takes an FOLProblem and returns a CNF problem. 
(defun translate-FOL-CNF (prob)
  (when (not (FOLProblem-p prob))
    (error "Attempt to use translate-FOL-CNF with non-FOLProblem argument"))
  (tr-FOL-CNF prob (FOLProblem-statement prob) NIL))

;; Internal function for translating FOL to CNF
(defun tr-FOL-CNF (prob FOL-clause negated-p)
  (if (null FOL-clause)
      NIL
    (cond

     ;; Recur on the syntactic construct described by the first
     ;; element of FOL-clause
     ((keyword? (first FOL-clause)) 
      (tr-FOL-CNF-key prob FOL-clause negated-p))
            
     ;; Make a literal out of the element using the supplied make-lit
     ;; function from sat.lsp
     ((pred? prob (first FOL-clause)) 
      ;; Handle equality immediately
      (if (eq (first FOL-clause) 'eq)
	  (tr-FOL-CNF-eq prob FOL-clause negated-p)
	(list (list (make-lit FOL-clause (not negated-p))))))
	    
     ;; An error has occurred; only valid predicates and keywords start
     ;; clauses:
     (T 
      (error "Some clause starts with an invalid token (not a keyword or a predicate): ~S"
	     FOL-clause)))))

;; Internal function for translating an equality statement into
;; TRUE == (:AND ) or FALSE == (:OR )
(defun tr-FOL-CNF-eq (prob eq-clause negated-p)
  (assert (eq (first eq-clause) 'eq))
  (assert (= (length eq-clause) 3))
  (if (equal (second eq-clause) (third eq-clause))
      (tr-FOL-CNF prob '(:AND) negated-p)
    (tr-FOL-CNF prob '(:OR) negated-p)))

;; Internal function for translating FOL to CNF given a clause
;; controlled by the keyword at the start of FOL-clause. ASSUMES A
;; KEYWORD AT START OF FOL-clause!
(defun tr-FOL-CNF-key (prob FOL-clause negated-p)
  (assert (keyword? (first FOL-clause)))
  (case (first FOL-clause)
	;; NOT clauses simply negate the negated status
	(:NOT
	 (assert (= (length FOL-clause) 2))
	 (tr-FOL-CNF prob (second FOL-clause) (not negated-p)))
      
	;; IMPLIES resolves to (:OR (:NOT arg1) arg2)
	(:IMPLIES
	 (assert (= (length FOL-clause) 3))
	 (tr-FOL-CNF prob (list :OR (list :NOT (second FOL-clause))
				(third FOL-clause)) negated-p))
	;; FORALL and EXISTS are handled by a separate function, but reverse
	;; their senses here if they are negated; also, separate into
	;; quantifier, variable list, and clause:
	((:FORALL :EXISTS)
	 (assert (= (length FOL-clause) 3))
	 (tr-FOL-CNF-quant prob
			   (if negated-p
			       (if (eq (first FOL-clause) :FORALL)
				   :EXISTS
				 :FORALL)
			     (first FOL-clause))
			   (second FOL-clause)
			   (third FOL-clause)
			   negated-p))

	;; AND and OR are also handled by a separate function, but, again,
	;; reverse their senses here if they are negated.
	((:AND :OR)
	 (tr-FOL-CNF-connect prob
			     (if negated-p
				 (if (eq (first FOL-clause) :AND) :OR :AND)
			       (first FOL-clause))
			     (rest FOL-clause) negated-p))

	;; No other cases; indicate error
	(error "Unknown keyword: ~S" FOL-clause)))
			   
;; Internal function for translating quantified clauses to CNF
(defun tr-FOL-CNF-quant (prob quantifier vars clause negated-p)
  ;; Get a list of clauses which represents the clause instantiated under
  ;; all combinations of the given variables
  (let ((inst-clauses (instantiate prob vars (list clause)))
	(connector (case quantifier
			 (:FORALL :AND)
			 (:EXISTS :OR)
			 (OTHERWISE 
			  (error "Illegal quantifier: ~S" quantifier)))))
    (tr-FOL-CNF prob (cons connector inst-clauses) negated-p)))

;; Internal function for instantiating a set of clauses with a given
;; variable list
(defun instantiate (prob vars clauses)
  (if (null vars)
      clauses
    (instantiate prob (rest vars) 
		 (instantiate-var prob 
				  (first (first vars)) 
				  (second (first vars))
				  clauses))))

;; Internal function for instantiating a set of clauses with the given
;; variable/type pair
(defun instantiate-var (prob var type clauses)
  (assert (type? prob type))
  (assert (var? var))
  (instantiate-var-with-list 
   prob 
   var
 
   ;; objects of this type
   (rest (find type (folproblem-types prob) :key #'first)) 

   clauses))

;; Internal function for instantiating a set of clauses with the given
;; variable/values pair
(defun instantiate-var-with-list (prob var values clauses &optional (new-clauses NIL))
  (if (null values)
      new-clauses
    (instantiate-var-with-list prob var (rest values) clauses
			       (append
				(nsubst (first values) var (copy-tree clauses))
				new-clauses))))

;; Internal function for translating connectors into CNF
(defun tr-FOL-CNF-connect (prob connector clauses negated-p)
  ;; Form a list of the CNF versions of the clauses
  (let ((CNF-list (mapcar #'(lambda (clause)
			      (tr-FOL-CNF prob clause negated-p))
			  clauses)))
    ;; Very different procedure for :AND and :OR
    (case connector
	  ;; For :AND just glom the lists together (ands of ands = one
	  ;; big and).
	  (:AND 
	   (apply #'append CNF-list))
	  ;; For :OR need to use distributivity over clauses
	  (:OR 
	   (distribute CNF-list))
	  (OTHERWISE (error "Illegal connector: ~S" connector)))))

;; CNF-list is a disjunction of conjunctions of disjunctions.
;; returns a conjunction of disjunctions
;; (CNF-list is a list of lists of clauses)
;;
;; Note that this may share structure. To stop that, copy
;; CNF-list each time.
(defun distribute (CNF-list)
  (if (null CNF-list)
      '(())  ; FALSE
    (let ((result (distribute (rest CNF-list))))
      (apply #'append
	     (mapcar #'(lambda (CNF-clause)
			 (mapcar #'(lambda (other-CNF-clause)
				     (append CNF-clause other-CNF-clause))
				 result)) (first CNF-list))))))


;;; Example problem
;;
;; This example is drawn from the example problem at
;; http://www.cs.washington.edu/education/courses/cse473/99wi/assign/ps2ex.html
;;


(defvar *ps2ex-fol*)
(setf *ps2ex-fol*
      (make-folproblem 
         :preds '((plays prof prof week))
         :types '((prof A B C D E F) (week one two three four five))
         :statement '(:AND
                      ;; No prof plays herself
                      (:FORALL ((?x prof) (?z week)) (:NOT (plays ?x ?x ?z)))
                      
                      ;; If x plays y in week z, then y also plays x in week z
                      (:FORALL ((?x prof) (?y prof) (?z week))
                       (:IMPLIES (plays ?x ?y ?z) (plays ?y ?x ?z)))
                      
                      ;; Each prof plays at most once per week
                      (:FORALL ((?w prof) (?x prof) (?y prof) (?z week))
                       (:IMPLIES (:NOT (eq ?y ?w))
                        (:IMPLIES (plays ?x ?y ?z) (:NOT (plays ?x ?w ?z)))))
                      
                      ;; Each prof plays at least once per week
                      (:FORALL ((?x prof) (?z week))
                       (:EXISTS ((?y prof)) (plays ?x ?y ?z)))
                      
                      ;; Each prof plays each other prof at least once
                      (:FORALL ((?x prof) (?y prof))
                       (:EXISTS ((?z week))
                        (:IMPLIES (:NOT (eq ?x ?y)) (plays ?x ?y ?z))))
                      
                      ;; Each prof plays each other prof at most once
                      (:FORALL ((?w week) (?x prof) (?y prof) (?z week))
                       (:IMPLIES (:NOT (eq ?z ?w))
                        (:IMPLIES (plays ?x ?y ?z) (:NOT (plays ?x ?y ?w)))))
                      
                      ;; Problem constraints
                      (plays A D one)
                      (plays A F two)
                      (plays B E one)
                      (plays B C three)
                      (plays C F one))))

;;; Use of example
;;
;; To use this example, I recommend a DFS style search engine like the one below
;;
;; (defun dfs (states goal-p get-next)
;;    (cond ((null states) NIL)
;;          ((funcall goal-p (first states)) (first states))
;;          (T
;;             (dfs (append (funcall get-next (first states))
;;                     (rest states)) goal-p get-next))))
;;
;; Then, execute the following code:
;;
;; ;; Translate to CNF
;; (defvar *ps2ex-cnf*)
;; (setf *ps2ex-cnf* (translate-fol-cnf *ps2ex-fol*))
;;
;; ;; Set the problem
;; (set-problem *ps2ex-cnf*)
;; 
;; ;; Run the search
;; (setf soln (dfs (list (get-initial)) #'goal-p #'get-next))
;;
;; ;; Get the solution assignments:
;; (setf soln-assg (get-solution soln))
;;
;; ;; Now, just look through the solution assignments for the ones
;; ;; you are interested in. If you're only interested in satisfiability,
;; ;; you just need to know if the soln came back NIL or not.
;; ;;
;; ;; I looked through with the following code:
;;
;; ;; Do an equal comparison except that * matches any single element
;; (defun compare-with-wildcard (a b)
;;    (cond ((null a) (null b))
;;          ((null b) NIL)
;;          ((listp a) (and (listp b)
;;                          (compare-with-wildcard (car a) (car b))
;;                          (compare-with-wildcard (cdr a) (cdr b))))
;;          ((listp b) NIL)
;;          ((or (eq a '*) (eq b '*)) T)
;;          (T (equal a b))))
;;
;; (find '((plays B * two) . T) soln-assg :test #'compare-with-wildcard)
;;                                                   
;;
;; End code

;; Note that the engines I provide are not necessarily fast or efficient.
;; If you want them faster, feel free to modify them yourselves.
;;
;;   Steve Wolfman