;; -*- Mode: Lisp; -*-

;;;; Inequality reasoning module for TGIZMO
;;;; File name: ineqs.lsp
;;;;  modified: Thursday, February 14, 2008 at 17:53:42 by forbus

;;; Copyright (c) 1991-1993, Kenneth D. Forbus, Northwestern University,
;;; and Johan de Kleer, the Xerox Corporation.
;;; All rights reserved.

;;; See the file legal.txt for a paragraph stating scope of permission
;;; and disclaimer of warranty.  The above copyright notice and that
;;; paragraph must be included in any separate copy of this file.


(in-package :cl-user)

(proclaim '(special *tgizmo*))

(defun num-order (n1 n2) (string< (format nil "~A" n1) (format nil "~A" n2)))

(defun individual-of (q-or-n) ;; Presumes single owner
    (cond ((not (listp q-or-n)) nil)
	  ((or (eq (car q-or-n) 'a)
	       (eq (car q-or-n) 'd)) (individual-of (cadr q-or-n)))
	  (t (cadr q-or-n))))

(defun quantity-of (q-or-n)
  (cond ((null q-or-n) (error "Bad format for quantity: ~A" q-or-n))
	((not (listp q-or-n)) nil)
	((or (eq (car q-or-n) 'a) (eq (car q-or-n) 'd)) (cadr q-or-n))
	((or (null (cdr q-or-n)) (cddr q-or-n))
	 (error "Bad format for quantity: ~A" q-or-n))
	(t q-or-n)))

(defun install-comparison-constraints-if-needed (n1 n2 &aux cycles)
  (when (equal n1 n2) (error "Can't do self-comparisons: ~A." n1))
  (if (num-order n2 n1) (psetq n1 n2 n2 n1))
  (unless (member (cons n1 n2) (tgizmo-comparisons *tgizmo*) :test #'equal)
	  (install-comparison-constraints n1 n2)
	  ;; Preprocess connectivity for transitivity inferences
	  (setq cycles (find-comparison-cycles-for n1 n2))
	  (when cycles
		(debugging-tgizmo :comp
				  "~%  ..Found new comparison cycles:~%~A" cycles)
		(setf (tgizmo-update-ineqs? *tgizmo*) t)
		(setf (tgizmo-comp-cycles *tgizmo*)
		      (nconc cycles
			     (tgizmo-comp-cycles *tgizmo*))))
	  ;; Finaly, record the comparison as potentially interesting.
	  (push (cons n1 n2) (tgizmo-comparisons *tgizmo*))))

;;;; Internal consistency and updating for comparisons

(defun install-comparison-constraints (n1 n2)
  ;; When one of them is not a quantity, perhaps because
  ;;  the individual in question does not exist,
  ;; the comparison is irrelevant
  (let ((q1 (quantity-of n1))
	(q2 (quantity-of n2))
	(node nil))
    (unless (or q1 q2) (error "Can't compare constants: ~A, ~A" q1 q2))
    (assert! `(:iff ,(if q1
			 (if q2 `(:or (:not (quantity ,q1))
				      (:not (quantity ,q2)))
			   `(:not (quantity ,q1)))
		       `(:not (quantity ,q2)))
		    (:and (:not (,n1 <= ,n2))
			  (:not (,n2 <= ,n1))))
	     :existence-constraint)
    ;; Ensure transitivity checked whenever new information
    ;; arrives.
    (setq node (get-tms-node `(,n1 <= ,n2)))
    (push `(update-ineqs-as-needed ,node :true)
	  (tms-node-true-rules node))
    (push `(update-ineqs-as-needed ,node :false)
	  (tms-node-false-rules node))
    (setq node (get-tms-node `(,n2 <= ,n1)))
    (push `(update-ineqs-as-needed ,node :true)
	  (tms-node-true-rules node))
    (push `(update-ineqs-as-needed ,node :false)
	  (tms-node-false-rules node)) 
    node))

(defun update-ineqs-as-needed (node label)
  (setf (tgizmo-update-ineqs? *tgizmo*) t)
  (case label
	(:true (push `(update-ineqs-as-needed ,node ,label)
		     (tms-node-true-rules node)))
	(:false (push `(update-ineqs-as-needed ,node ,label)
		      (tms-node-false-rules node)))
	(t (error "Inappropriate label ~A in update-ineqs-as-needed: ~A."
		  label node))))

;;;; Test predicates

(defun greater-than? (n1 n2)
  (and (true? `(,n2 <= ,n1)) (false? `(,n1 <= ,n2))))

(defun less-than? (n1 n2)
  (and (true? `(,n1 <= ,n2)) (false? `(,n2 <= ,n1))))

(defun equal-to? (n1 n2)
  (and (true? `(,n2 <= ,n1)) (true? `(,n1 <= ,n2)))) 

(defun rel-value (n1 n2)
  (let ((le `(,n1 <= ,n2))
	(ge `(,n2 <= ,n1)))
    (cond ((true? le)
	   (cond ((true? ge) :=)
		 ((false? ge) :<)
		 (t :<=)))
	  ((false? le)
	   (cond ((true? ge) :>)
		 ((false? ge) :bt)
		 (t :>=)))
	  ((true? ge) :>=)
	  (t :??))))

(defun rel-value-clause (n1 n2 rel)
  (case rel
	(:<= `(,n1 <= ,n2))
	(:>= `(,n2 <= ,n1))
	(:= `(:and (,n1 <= ,n2) (,n2 <= ,n1)))
	(:< `(:and (,n1 <= ,n2) (:not (,n2 <= ,n1))))
	(:> `(:and (:not (,n1 <= ,n2)) (,n2 <= ,n1)))))

(defun comparison? (n1 n2 &optional (*tgizmo* *tgizmo*))
  (install-comparison-constraints-if-needed n1 n2)
  (use-transitivity)
  (rel-value n1 n2))

;;;; Helpers for asserting inequalities

(defun greater-than! (n1 n2 &optional (reason :user))
  (assume! `(:not (,n1 <= ,n2)) reason)
  (assume! `(,n2 <= ,n1) reason))

(defun less-than! (n1 n2 &optional (reason :user))
  (assume! `(,n1 <= ,n2) reason)
  (assume! `(:not (,n2 <= ,n1)) reason))

(defun equal-to! (n1 n2 &optional (reason :user))
  (assume! `(,n1 <= ,n2) reason)
  (assume! `(,n2 <= ,n1) reason))

;;; The next three procedures are used in code which 
;;; produces justifications.

(defun lt-forms (n1 n2)
  `((,n1 <= ,n2) (:not (,n2 <= ,n1))))

(defun eq-forms (n1 n2)
  `((,n1 <= ,n2) (,n2 <= ,n1)))

(defun gt-forms (n1 n2)
  `((:not (,n1 <= ,n2)) (,n2 <= ,n1))) 

(defun lte-forms (n1 n2) `((,n1 <= ,n2)))

(defun gte-forms (n1 n2) `((,n2 <= ,n1)))

;;;; Transitivity computations

(defun use-transitivity (&optional (*tgizmo* *tgizmo*))
  (do () ((not (tgizmo-update-ineqs? *tgizmo*)))
      (setf (tgizmo-update-ineqs? *tgizmo*) nil)
      (dolist (cycle (tgizmo-comp-cycles *tgizmo*))
	      (check-comp-cycle cycle))
      (tg-run-rules)))

(defun find-comparison-cycles-for (n1 n2 &aux start)
  ;; Queue entries need to be (<n3> <n1>)
  (do ((queue (mapcar #'(lambda (n) (list n n1))
		      (find-comparison-set n1 n2))
	      (nconc (cdr queue) new-entries))
       (new-entries nil nil)
       (candidates nil)
       (cycles nil))
      ((null queue) (mapcar #'make-comp-cycle cycles))
      (cond ((equal (caar queue) n2) ;; Got one
	     (push  (car queue) cycles))
	    (t (dolist (new-num
			(find-comparison-set (caar queue)
					     (cadar queue)))
		       (unless (member new-num
				       (car queue) :test #'equal)
			       (push (cons new-num (car queue))
				     new-entries)))))))

(defun make-comp-cycle (number-list)
  (do ((nums number-list (cdr nums))
       (cycle nil))
      ((null (cdr nums))
       (nreverse (cons (cons (car nums) (car number-list))
		       cycle)))
      (push (cons (car nums) (cadr nums)) cycle)))

(defun find-comparison-set (n1 &optional (skip nil)
			       &aux others)
  (dolist (other (tg-fetch `(,n1 <= ?other)) others)
	  (unless (and skip (equal (third other) skip))
		  (push (third other) others))))
(defun check-comp-cycle (cycle &aux lts gts eqs leqs geqs bts unks)
  ;; Squeezes out any inferences that can be made via transitivity
  ;; Recall cycle is a list of pairs ((n1 . n2) ... (ni . n1)), 
  ;; where comparisons link each of the numbers.
  ;; What to do with a cycle can be defined by analogy with
  ;; BCP on clauses.  That is, some labellings are inconsistent,
  ;; while some partial labellings can lead to others being labelled.  
  (dolist (pair cycle)
     (case (rel-value (car pair) (cdr pair))
        (:= (push pair eqs))
        (:< (push pair lts))
        (:> (push pair gts))
        (:<= (push pair leqs))
        (:>= (push pair geqs))
        (:bt (push pair bts))
        (:?? (push pair unks))))
   (cond ((or (cdr unks) bts)) ;; Too many unknowns, or moot
         ((null unks) ;; Look for violations, hardening
          (cond ((and (null leqs) (null geqs)) ;; All hard
                 (cond ((or (and eqs (null gts) (null lts)) 
                            (and gts lts))) ;; Okay, all = or mixed
                       (t (contradiction ;; Net > or net <, impossible
                             (find-cycle-support cycle)
                             (tgizmo-ltre *tgizmo*)))))
                ((and leqs geqs)) ;; Mixed leqs & geqs => no conclusion
                ((null leqs) ;; must be geqs
                 (cond (lts ;; Only one case where hardening can occur:
                        ;; a single geq and a single lts, i.e.,
                        ;; A >= B = C = D < E = A
                        (when (and (null (cdr geqs))
                                   (null (cdr lts)))
                           (assert! `(:implies
                                      (:and ,@ (find-cycle-support cycle))
                                      (:and ,(rel-value-clause (caar geqs)
                                              (cdar geqs) :>)))
                              :hardening->=-<-case)))
                       (gts ;; Contradiction, net effect must be >
                        (contradiction (find-cycle-support cycle)
                           (tgizmo-ltre *tgizmo*)))
                       (t ;; geq's -> eq's
		       (assert! `(:implies
				  (:and ,@ (find-cycle-support cycle))
				  (:and ,@ (mapcar #'(lambda (pair)
						       (rel-value-clause (car pair) (cdr pair)
									 :=))
						   geqs)))
				:hardening->=))))
                (t ;; must be leqs
                   (cond (gts ;; One special case of hardening,
                          ;; A > B <= C = D = A
                          (when (and (null (cdr leqs))
                                     (null (cdr gts))
                                     eqs)
                             (assert! `(:implies (:and ,@ (find-cycle-support cycle))
                                        (:and ,(rel-value-clause (caar leqs) (cdar leqs)
                                                :<)))
                                :hardening->-<=-case)))
		      (lts ;; Contradiction, net effect must be <
		       (contradiction (find-cycle-support cycle)
				      (tgizmo-ltre *tgizmo*)))
		      (t ;; leq's -> eq's
		       (assert! `(:implies
				  (:and ,@ (find-cycle-support cycle))
				  (:and ,@ (mapcar #'(lambda (pair)
						       (rel-value-clause (car pair) (cdr pair)
									 :=))
						   leqs)))
				:hardening-<=))))))
         (t ;; Can last one be concluded?
            (cond ((and lts gts)) ;; no constraint
                  ((and geqs leqs)) ;; No constraint
                  ((and lts (null geqs)) ;; Last must be gt.
                   (assert! `(:implies
                              (:and ,@ (find-cycle-support cycle))
                              ,(rel-value-clause (caar unks) (cdar unks) :>))
                      :>-via-trans))
                  ((and gts (null leqs)) ;; Last must be lt.
                   (assert! `(:implies
                              (:and ,@ (find-cycle-support cycle))
                              ,(rel-value-clause (caar unks) (cdar unks) :<))
                      :<-via-trans))
                  ((and eqs (null geqs) (null leqs) 
                        (null lts) (null gts))           
                   (assert! `(:implies ;; last must be =.
                              (:and ,@ (find-cycle-support cycle))
                              ,(rel-value-clause (caar unks) (cdar unks) :=))
                      :=-via-trans))
                  ((and leqs (null geqs) (null lts) (null gts))
                   ;; All leq's plus unknown.  Must be geq.
                   (assert! `(:implies (:and ,@ (find-cycle-support cycle))
                              ,(rel-value-clause (caar unks) (cdar unks) :>=))
                      :geq-via-trans))
                  ((and geqs (null leqs) (null lts) (null gts))
                   ;; All geq's plus unknown.  Must be leq.
                   (assert! `(:implies (:and ,@ (find-cycle-support cycle))
                              ,(rel-value-clause (caar unks) (cdar unks) :<=))
                      :leq-via-trans))
                  (t (error "Bad length cycle: ~A" cycle))))))

;;; Support code

(defun find-cycle-support (cycle &aux support form)
  (dolist (pair cycle support)
   (when (setq form (signed-form `(,(car pair) <= ,(cdr pair))))
	 (push form support))
   (when (setq form (signed-form `(,(cdr pair) <= ,(car pair))))
	 (push form support))))

(defun signed-form (form)
  (case (label-of form)
	(:true form)
	(:false (list :not form))
	(t nil)))

(defun show-comp-cycles (&optional (*tgizmo* *tgizmo*) &aux (counter 0))
  (dolist (cycle (tgizmo-comp-cycles *tgizmo*))
	  (format t "~%~D: " counter)
	  (dolist (pair cycle) (format t "~A " (number-string (car pair))))
	  (incf counter))
  counter)

(defun show-ineqs (&optional (*tgizmo* *tgizmo*))
  (dolist (comp (tgizmo-comparisons *tgizmo*))
	  (format t "~%  ~A ~A ~A" (number-string (car comp))
		  (rel-value (car comp) (cdr comp))
		  (number-string (cdr comp)))))

;;; Test cases

(setq *ineq-test1* '((> (a (t i1)) (a (t i2)))
		       (= (a (t i2)) (a (t i3)))
		       (> (a (t i3)) (a (t i4)))
		       (< (a (t i4)) (a (t i1)))
		       (> (a (t i3)) (a (t i1))))) ;; Should be 3 cycles

(setq *ineq-test2* '((> (a (t fred)) (a (t george)))
		     (> (a (t george)) (a (t mable)))
		     (= (a (t mable)) (a (t anabelle)))
		     (> (a (t anabelle)) (a (t pat)))))