;;;; -*-  Mode: LISP; Syntax: Common-Lisp; Base: 10                          -*-
;;;; ---------------------------------------------------------------------------
;;;; File name: canonicalize.lsp
;;;;    System: FIRE
;;;;   Version: 1.0
;;;;    Author: Ken Forbus
;;;;   Created: September 15, 2001 14:13:10
;;;;   Purpose: Canonicalize axioms for backchaining
;;;; ---------------------------------------------------------------------------
;;;;  Modified: Friday, May 28, 2004 at 10:45:39 by Kenneth Forbus
;;;; ---------------------------------------------------------------------------

(in-package :fire)

;;;; Canonicalization of axioms for backchaining

;;; Canonicalization converts non-ground axioms into clauses,
;;; so that they can be used for backchaining.  As in the LTMS,
;;; we convert axioms to Conjunctive Normal Form (a conjunction of
;;; disjunctive clauses.)
;;;
;;; Since this canonicalizer is run off-line, we make it as flexible
;;; as possible by using CLOS to allow it to be extended to new
;;; connectives by adding new methods

;;; ***** Quantifiers aren't currently handled.

(defun ground-term? (axiom)
  (cond ((null axiom) t)
        ((variable? axiom) nil)
        ((not (consp axiom)) t)
        (t (and (ground-term? (car axiom))
                (ground-term? (cdr axiom))))))

(defun extract-vars (axiom &optional (vars nil))
  (cond ((null axiom) vars)
        ((variable? axiom) 
         (if (member axiom vars) vars
           (cons axiom vars)))
        ((not (listp axiom)) vars)
        (t (extract-vars (car axiom)
                         (extract-vars (cdr axiom)
                                       vars)))))

(defun canonicalize-axiom (axiom)
  (cond ((not (listp axiom)) nil)
        ((not (logical-connective? (car axiom)))
         (if (ground-term? axiom) ;; Just a fact, no axioms here
           (list (make-clause (list axiom) nil))
           (list (make-clause (list axiom) nil))))
        ((ground-term? axiom) nil) ;; Just a more complex fact
        (t (canonicalize-it (car axiom) (cdr axiom) nil))))


;; Sort terms, replaces variable names by canonical names, 
;; e.g. ?0, ?1, ?2, sublis into clause and returns the list 
;; of positive and negative terms and the list of variables. 

(defun canonicalize-clause (clause)
  (let* ((clause (sort clause #'string< :key #'caar))
         (vars (extract-vars clause))
         (newvars nil))
    (dotimes (v (length vars))
      (push (intern (format nil "?~A" v)) newvars))
    (values (sublis (mapcar #'cons vars newvars) clause) newvars)))
              
;;; The internal method canonicalize-it does the real work. 
;;; We make it a method so that additional connectives and other
;;; special-cases can be added as needed.

(defmethod canonicalize-it ((connective t)(args t)(negate? t)) nil)
;;; ***** Should this be an error?  There is a possibility of a mismatch
;;; ***** between what the KB considers a logical connective and what FIRE
;;; ***** knows how to handle.  This implementation presumes that if the same
;;; ***** connective name is used, that the semantics is the same.

(defmethod canonicalize-it ((connective symbol)(args list)(negate? symbol))
  (if negate? (list (make-clause nil (list (cons connective args))))
    (list 
     (make-clause (list (cons connective args)) nil))))
  
(defmethod canonicalize-it ((connective (eql 'data::implies))
                            (args list) (negate? symbol))
  (let ((ante (car args))
        (conse (cadr args)))
    (if negate?
      (nconc (canonicalize-it (car ante) (cdr ante) nil)
             (canonicalize-it (car conse) (cdr conse) t))
      (disjoin-axioms (canonicalize-it (car ante) (cdr ante) t)
                      (canonicalize-it (car conse) (cdr conse) nil)))))

;; For some of the logical connectives the LTRE uses different names
;; how should we maintain these mappings? 
;; equiv = iff, xor = taxonomy

(defmethod canonicalize-it ((connective (eql 'data::equiv)) 
                            (args list) (negate? symbol))   
  (let ((ante (car args))
        (conse (cadr args)))
    (nconc (canonicalize-it 'data::implies (list ante conse) negate?)
           (canonicalize-it 'data::implies (list conse ante) negate?))))


(defmethod canonicalize-it ((connective (eql 'data::and)) 
                            (args list) (negate? symbol))
  (if negate? 
    (canonicalize-disjunction args t)
    (canonicalize-conjunction args nil)))
    
(defmethod canonicalize-it ((connective (eql 'data::or)) 
                            (args list) (negate? symbol))
  (if negate? 
    (canonicalize-conjunction args t)
    (canonicalize-disjunction args nil)))
    
(defun canonicalize-conjunction (args negate?)
  (mapcan #'(lambda (sub) (canonicalize-it (car sub) (cdr sub) negate?)) args))

(defun canonicalize-disjunction (args negate?)
  (unless args
    (return-from canonicalize-disjunction (list nil)))
  (setf args (reverse args))  ;; (TRH) retain order of terms to simplify debugging
  (do ((result (canonicalize-it (caar args) (cdar args) negate?))
       (rest (cdr args) (cdr rest)))
      ((null rest) result)
    (setq result (disjoin-axioms (canonicalize-it (caar rest) (cdar rest) negate?) result))))


(defmethod canonicalize-it ((connective (eql 'data::xor)) 
                            (args list) (negate? symbol))
  (canonicalize-it 
   'data::and 
   `((data::or ,@(copy-list args))
     ,@(do ((firsts args (cdr firsts))
            (rests (cdr args) (cdr rests))
            (result nil))
           ((null rests) result)
         (dolist (other rests)
           (push `(data::not (data::and ,(car firsts) ,other))
                 result))))
   negate?))

(defmethod canonicalize-it ((connective (eql 'data::not)) 
                            (args list) (negate? symbol))
  (canonicalize-it (caar args) (cdar args) (not negate?)))

(defmethod canonicalize-it ((connective (eql 'data::thereExists))
                            (args list) (negate? symbol))
  (let* ((form (cons connective args))
         (var (car args))
         (stmt (cadr args))
         (expansion (canonicalize-it (car stmt) (cdr stmt) negate?))
         (term (make-instance 'quantified-term :form form :expansion expansion :var var)))
    (if negate? 
      (list (make-clause nil (list term)))
      (list (make-clause (list term) nil)))
    ))

;;; Disprove a universally quantified axiom by finding a single counterexample
(defmethod canonicalize-it ((connective (eql 'data::forAll))
                            (args list) (negate? symbol))
  (let ((stmt (cadr args)))
    (canonicalize-it (car stmt) (cdr stmt) (not negate?))))
                                
;; Modeled after LTMS version
(defun disjoin-axioms (conj1 conj2)
  (unless (or conj1 conj2) (return-from disjoin-axioms nil))
  (mapcan #'(lambda (disj1)
              (mapcan #'(lambda (disj2)
                          (multiple-value-bind (duplicates? tautology?)
                              (clause-redundant? disj1 disj2)
                            (cond (tautology? nil)
                                  (duplicates?
                                   (list (append-unique disj1 disj2)))
                                  (t (list (append disj1 disj2))))))
                conj2))
    conj1))

(defun term-form (thing) (car thing))
(defun term-label (thing) (cdr thing))

(defun append-unique (l1 l2)
  (remove-duplicates (append l1 l2) :test 'equal))

;;; *** This is buggy. Thinks that the following is a tautology, for example. 
;;;(implies (and (isa dog ?x)
;;;              (mother ?x ?y))  
;;;         (isa dog ?y)))
;;; variable-bindings have to be subsituted. 
;;; It ends up throwing 5-10% of valide axioms because of this. 
;;; When we have literals that are not ground, for example ((isa dog ?x) . false) 
;;; and ((isa dog ?y) . true) we cant just say that they make a tautology 
;;; unless ?x and ?y bind to the same thing. So, my suggestion -- 
;;; 1. If there are variables whose bindings are not known, 
;;;    we use #'equal to check for duplicates/tautologies. 
;;; 2. If the bindings are known, we sublis them, and then #'equal.
;;;(defun clause-redundant? (c1 c2 &aux (duplicates? nil))
;;;  (dolist (term1 c1 (values duplicates? nil))
;;;    (dolist (term2 (find (term-form term1) c2 :test #'(lambda (x y)
;;;                                                        (not (eq (ltre::unify x y) :fail)))
;;;                         :key 'term-form))
;;;      (cond ((eq (term-label term1) (term-label term2))
;;;             (setq duplicates? t))
;;;            (t (return-from clause-redundant? (values duplicates? t)))))))
;;;
;;; Version below solves the above problem, but assumes that the variables 
;;; are canonicalized. The test is #'equal after substituting the bindings. 

(defun clause-redundant? (c1 c2 &aux (duplicates? nil))
  (dolist (term1 c1 (values duplicates? nil))
    (dolist (term2 (find (term-form term1) c2 :test #'(lambda (x y) (equal x y))
                         :key 'term-form))
      (cond ((eq (term-label term1) (term-label term2))
             (setq duplicates? t))
            (t (return-from clause-redundant? (values duplicates? t)))))))

(defun make-clause (pos-terms neg-terms)
  (setq pos-terms (remove-duplicates pos-terms :test 'equal))
  (setq neg-terms (remove-duplicates neg-terms :test 'equal))
  (when (intersection pos-terms neg-terms :test 'equal)
    (return-from make-clause (values nil)))
  (nconc (mapcar #'(lambda (term) (cons term :true)) pos-terms)
         (mapcar #'(lambda (term) (cons term :false)) neg-terms)))

;;;; ---------------------------------------------------------------------------
;;; END OF CODE