(in-package :vag :use '(lisp util rules))

(export '(goto-context consider-expression assert contradiction? value-of
	  why print-justification just-assertion just-rule-name just-subjustifications))

;;This file is built on top of denoticer.
;;Information is passed in from vag.lisp through symbol properties.
;;The following information is input from vag.lisp

;; --- the definition property of constructor symbols.
;; --- the implementation property of constructor symbols.
;; --- the filter predicate property of function symbols.
;; --- the output sort of function symbols.
;; --- the filter predicate property of sort symbols.
;; --- the supersort of a sort symbol
;; --- the sort of a variable.

;;Here is where information is derived from the vag code.

(defextender consider-expression (exp)
  (assert-internal `(consider! ,(intern-node (vag-macro-expand-all exp))) 'context-premise))

(defextender assert (formula)
  (assert-internal `(has-value ,(intern-node formula) true) 'context-assumption))

(defnoticer consider!1 ((consider! ?x))
  ?justification
  (dolist (prod (assoc-value 'production (node-other-assertions ?x)))
    (when (eq (car prod) ?x)
      (let ((lex-prod prod))
	(propagate-consider! ?x prod
			     (justification 'consider-propagation
					    `(consider! ,?x)
					    `(production ,@lex-prod)))))))

(defun consider!2 (prod)
  (let ((x (first prod)))
    (when (member 'consider! (node-monadic-properties x))
      (propagate-consider! x prod (justification 'consider-propagation `(consider! ,x)
						 `(production ,@prod))))))

(pushnew 'consider!2 (noticers 'production))

(defmacro prod-fun (prod)
  `(second ,prod))

(defmacro prod-rhs (prod)
  `(cddr ,prod))

(defmacro prod-lhs (prod)
  `(car ,prod))

(defun propagate-consider! (x prod just)
  (declare (ignore x))
  (let ((fun (prod-fun prod))
	(args (prod-rhs prod)))
    (if (eq fun 'if)
	(assert-internal `(consider! ,(car args)) just)
	(progn
	  (dolist (arg args)
	    (assert-internal `(consider! ,arg) just))
	  (assert-predicate (filter-predicate fun) args just)
	  (let ((sort (output-sort-cache fun)))
	    (when (and sort (symbolp sort))
	      (assert-sort x sort just)))
	  (let ((def (vag-definition fun)))
	    (when def
	      (assert-internal `(= ,x ,(beta-reduction def args)) (create-justification 'beta-reduction (list just)))))))))

(defun beta-reduction (op args)
  (selectmatch op
    ((lambda ?argvars ?body)
     (let ((subst (mapcar 'cons ?argvars args)))
       (intern-node2 (apply-vag-subst subst ?body))))))

(defun assert-predicate (pred args just)
  (when pred
    (let ((formula (beta-reduction pred args))
	  (new-just (when just (rules::create-justification 'filter-predicate (list just)))))
      (assert-internal `(has-value ,formula true) new-just)
      (assert-internal `(consider! ,formula) new-just))))

(defnoticer notice-var1 ((production ?x :the-variable ?y)
			 (has-value ?y ?v))
  (notice-var ?x ?v ?justification))

(defnoticer notice-var2 ((has-value ?y ?v)
			 (production ?x :the-variable ?y))
  (notice-var ?x ?v ?justification))

(defun notice-var (?x ?v ?just)
    (when (symbolp ?v)
      (let ((sort (vag-var-sort ?v)))
	(when sort
	  (assert-sort ?x sort ?just)))))
	  
(defun assert-sort (x sort just)
  (assert-internal `(has-type ,x ,sort) just)
  (let ((next (parent-sort sort)))
    (when next
      (assert-sort x next (when just (rules::create-justification 'supersort (list just)))))))

(defnoticer type-noticer ((has-type ?x ?sort))
  (when (and ?sort (symbolp ?sort))
    (assert-predicate (sort-constraint ?sort) (list ?x) ?justification)))

(defun var-value (x)
  (car (assoc-value 'has-value (node-binaries-forward x))))

(defun propagate-value-prod (prod)
  (let ((imp (implementation (prod-fun prod))))
    (when imp
      (let ((argvals (mapcar #'(lambda (arg)
				 (let ((vals (assoc-value 'has-value (node-binaries-forward arg))))
				   (unless vals
				     (return-from propagate-value-prod nil))
				   (car vals)))
			     (prod-rhs prod))))
	(set-value (prod-lhs prod)
		   (apply imp argvals)
		   (create-justification 'implementation-application
					 (cons (gethash `(production ,@prod) *justification-table*)
					       (mapcar #'(lambda (arg val)
						     (gethash `(has-value ,arg ,val) *justification-table*))
						 (prod-rhs prod)
						 argvals))))))))

(pushnew 'propagate-value-prod (noticers 'production))

(defnoticer implementation-noticer ((has-value ?x ?v))
  ?justification
  (mapc 'propagate-value-prod (assoc-value 'production (node-other-assertions ?x))))



;========================================================================
;conditionals
;========================================================================

(defnoticer if-noticer1 ((production ?z if ?phi ?x ?y)
			 (has-value ?phi ?truth))
  (if (eq ?truth 'true)
      (equate-vars ?z ?x ?justification)
      (equate-vars ?z ?y ?justification)))

(defun equate-vars (x y just)
  (assert-internal `(= ,x ,y) just))

(defnoticer if-noticer2 ((has-value ?phi ?truth)
			 (production ?z if ?phi ?x ?y))
  (if (eq ?truth 'true)
      (equate-vars ?z ?x ?justification)
      (equate-vars ?z ?y ?justification)))


;========================================================================
;BCP
;========================================================================

(defnoticer not1 ((production ?y not ?x)
		  (has-value ?y ?val))
  (set-value ?x (negation ?val) ?justification))

(defun set-value (x y just)
  (assert-internal `(has-value ,x ,y) just))

(defnoticer not2 ((has-value ?y ?val)
		  (production ?y not ?x))
  (set-value ?x (negation ?val) ?justification))

(defnoticer and1 ((production ?z and ?x ?y))
  ?justification
  (check-and-consistency ?z ?x ?y))

(defnoticer and2 ((has-value ?z ?val)
		  (production ?z and ?x ?y))
  ?justification
  (check-and-consistency ?z ?x ?y))

(defnoticer and3 ((has-value ?y ?val)
		  (production ?z and ?x ?y))
  ?justification
  (check-and-consistency ?z ?x ?y))

(defnoticer and4 ((has-value ?x ?val)
		  (production ?z and ?x ?y))
  ?justification
  (check-and-consistency ?z ?x ?y))

(defun value-justification (rule-name node value)
  (create-justification rule-name (list (gethash `(has-value ,node ,value) *justification-table*))))

(defun value-justification2 (rule-name nodes values)
  (create-justification rule-name
			(mapcar #'(lambda (node value)
				    (gethash `(has-value ,node ,value) *justification-table*))
				nodes
				values)))

(defun check-and-consistency (z x y)
  (let ((zval (var-value z))
	(xval (var-value x))
	(yval (var-value y)))
    (cond ((eq zval 'true)
	   (let ((just (value-justification 'and-definition z 'true)))
	     (set-value x 'true just)
	     (set-value y 'true just)))
	  ((eq zval 'false)
	   (when (eq xval 'true)
	     (set-value y 'false (value-justification2 'and-definition (list z x) (list 'false 'true))))
	   (when (eq yval 'true)
	     (set-value x 'false (value-justification2 'and-definition (list z y) (list 'false 'true)))))
	  ((eq xval 'false)
	   (set-value z 'false (value-justification 'and-definition x 'false)))
	  ((eq yval 'false)
	   (set-value z 'false (value-justification 'and-definition y 'false)))
	  ((and (eq xval 'true)
		(eq yval 'true))
	   (set-value z 'true (value-justification2 'and-definition (list x y) (list 'true 'true)))))))

(defnoticer or1 ((production ?z or ?x ?y))
  ?justification
  (check-or-consistency ?z ?x ?y))

(defnoticer or2 ((has-value ?z ?val)
		  (production ?z or ?x ?y))
  ?justification
  (check-or-consistency ?z ?x ?y))

(defnoticer or3 ((has-value ?y ?val)
		  (production ?z or ?x ?y))
  ?justification
  (check-or-consistency ?z ?x ?y))

(defnoticer or4 ((has-value ?x ?val)
		  (production ?z or ?x ?y))
  ?justification
  (check-or-consistency ?z ?x ?y))

(defun check-or-consistency (z x y)
  (let ((zval (var-value z))
	(xval (var-value x))
	(yval (var-value y)))
    (cond ((eq zval 'false)
	   (let ((just (value-justification 'or-definition z 'false)))
	     (set-value x 'false just)
	     (set-value y 'false just)))
	  ((eq zval 'true)
	   (when (eq xval 'false)
	     (set-value y 'true (value-justification2 'and-definition (list z x) (list 'true 'false))))
	   (when (eq yval 'false)
	     (set-value x 'true (value-justification2 'and-definition (list z y) (list 'true 'false)))))
	  ((eq xval 'true)
	   (set-value z 'true (value-justification 'and-definition x 'true)))
	  ((eq yval 'true)
	   (set-value z 'true (value-justification 'and-definition y 'true)))
	  ((and (eq xval 'false)
		(eq yval 'fasle))
	   (set-value z 'false (value-justification2 'and-definition (list x y) (list 'false 'false)))))))


;========================================================================
;cons, car, cdr, and null?
;========================================================================


;There is a subtle bug motivating the use of consider! in the following rules.
;consider
;(define (numbers-between x y)
;  (if (> x y)
;      nil
;      (cons x (numbers-between (+ x 1) y))))
;
;and (consider! (numbers-between x y)) where x and y are variables.
;
;we get (consider! x) and we get that (cons x (numbers-between (+ x 1) y)) is interned.
;If we equate (car (cons x (numbers-between ...))) to x then we get (consider! (car (cons x ...)))
;which gives us (consider! (numbers-between (+ x 1) y)).  This gives an infinite loop.

(defnoticer cons1 ((production ?z cons ?x ?y)
		   (production ?w car ?z)
		   (consider! ?w))
  (equate-vars ?w ?x ?justification))

(defnoticer cons2 ((production ?w car ?z)
		   (consider! ?w)
		   (production ?z cons ?x ?y))
  (equate-vars ?w ?x ?justification))

(defnoticer cons3 ((consider! ?w)
		   (production ?w car ?z)
		   (production ?z cons ?x ?y))
  (equate-vars ?w ?x ?justification))

(defnoticer cons4 ((production ?z cons ?x ?y)
		   (production ?w cdr ?z)
		   (consider! ?w))
  (equate-vars ?w ?y ?justification))

(defnoticer cons5 ((production ?w cdr ?z)
		   (consider! ?w)
		   (production ?z cons ?x ?y))
  (equate-vars ?w ?y ?justification))

(defnoticer cons6 ((consider! ?w)
		   (production ?w cdr ?z)
		   (production ?z cons ?x ?y))
  (equate-vars ?w ?y ?justification))

(defnoticer null1 ((production ?z cons ?x ?y))
  (set-value (intern-node2 `(null? ,?z)) 'false ?justification))

(defnoticer null2 ((production ?y nil))
  (set-value (intern-node2 `(null? ,?y)) 'true ?justification))


;========================================================================
;member?, append, and map
;========================================================================

(setf (vag-definition 'member?)
      '(lambda (x y)
	(if (null? y)
	    (false)
	    (if (= x (car y))
		(true)
		(member? x (cdr y))))))

(setf (vag-definition 'append)
      '(lambda (x y)
	(if (null? x)
	    y
	    (cons (car x) (append (cdr x) y)))))

;map can not be handled with a definition because lambda expressions are
;not first class.

(defnoticer map1 ((production ?l2 map ?f ?l1)
		  (production ?l1 nil))
  (equate-vars ?l1 ?l2 ?justification))

(defnoticer map2 ((production ?l1 nil)
		  (production ?l2 map ?f ?l1))
  (equate-vars ?l1 ?l2 ?justification))

(defnoticer map3 ((production ?l1 cons ?x ?y)
		  (production ?l2 map ?f ?l1)
		  (has-value ?f ?fval))
  (equate-vars ?l2
	       (intern-node2 `(cons ,(beta-reduction ?fval (list ?x)) (map ,?f ,?y)))
	       ?justification))

(defnoticer map4 ((production ?l2 map ?f ?l1)
		  (production ?l1 cons ?x ?y)
		  (has-value ?f ?fval))
  (equate-vars ?l2
	       (intern-node2 `(cons ,(beta-reduction ?fval (list ?x)) (map ,?f ,?y)))
	       ?justification))

(defnoticer map5 ((has-value ?f ?fval)
		  (production ?l2 map ?f ?l1)
		  (production ?l1 cons ?x ?y))
  (equate-vars ?l2
	       (intern-node2 `(cons ,(beta-reduction ?fval (list ?x)) (map ,?f ,?y)))
	       ?justification))



;========================================================================
;bounds propagation
;========================================================================

(lisp:defvar *improv-req* .05)

(defun var-lower-bound (x)
  (let ((ans nil))
    (dolist (b (assoc-value 'lower-bound (node-binaries-forward x)))
      (when (or (null ans)
		(> b ans))
	(setq ans b)))
    ans))

(defun var-upper-bound (x)
  (let ((ans nil))
    (dolist (b (assoc-value 'upper-bound (node-binaries-forward x)))
      (when (or (null ans)
		(< b ans))
	(setq ans b)))
    ans))

(defun set-upper-bound (var bound just)
  (unless (dead? var)
    (let ((vlb (var-lower-bound var))
	  (vub (var-upper-bound var)))
      (if (and vlb (< bound (- vlb *infinitetesimal*)))
	  (assert-internal '(false) (create-justification 'conflicting-bounds
							  (list just
								(gethash `(lower-bound ,var ,vlb) *justification-table*))))
	  (let* ((delta (- (or vub *infinity*)
			   (or vlb *minus-infinity*))))
	    (when (and (> delta 0)
		       (> (- (or vub *infinity*) bound)
			  (* *improv-req* delta)))
	      (assert-internal `(upper-bound ,var ,bound) just)))))))

(defun set-lower-bound (var bound just)
  (unless (dead? var)
    (let ((vlb (var-lower-bound var))
	  (vub (var-upper-bound var)))
      (if (and vub (> bound (+ vub *infinitetesimal*)))
	  (assert-internal '(false) (create-justification 'conflicting-bounds
							  (list just
								(gethash `(upper-bound ,var ,vub) *justification-table*))))
	  (let* ((delta (- (or vub *infinity*)
			   (or vlb *minus-infinity*))))
	    (when (and (> delta 0)
		       (> (- bound (or vlb *minus-infinity*))
			  (* *improv-req* delta)))
	      (assert-internal `(lower-bound ,var ,bound) just)))))))

(defnoticer value-to-bound1 ((has-value ?var ?val)
			     (upper-bound ?var ?bound))
  (when (< ?bound ?val)
    (assert-internal '(false) ?justification)))

(defnoticer value-to-bound2 ((upper-bound ?var ?bound)
			     (has-value ?var ?val))
  (when (< ?bound ?val)
    (assert-internal '(false) ?justification)))

(defnoticer value-to-bound3 ((has-value ?var ?val)
			     (lower-bound ?var ?bound))
  (when (< ?val ?bound)
    (assert-internal '(false) ?justification)))

(defnoticer value-to-bound4 ((lower-bound ?var ?bound)
			     (has-value ?var ?val))
  (when (< ?val ?bound)
    (assert-internal '(false) ?justification)))

(defnoticer value-to-bound5 ((has-value ?var ?val))
  (when (numberp ?val)
    (set-lower-bound ?var ?val ?justification)
    (set-upper-bound ?var ?val ?justification)))

(defnoticer bound-to-value ((upper-bound ?x ?ub)
			    (lower-bound ?x ?lb))
  (when (< (abs (- ?ub ?lb)) (* 5 *infinitetesimal*))
    (set-value ?x (/ (+ ?ub ?lb) 2) ?justification)))

(defnoticer +noticer1
    ((production ?x + ?y ?z))
  ?justification
  (+-check ?x ?y ?z))

(defnoticer +noticer2
    ((lower-bound ?x ?xlb)
     (production ?x + ?y ?z))
  ?justification
  (+-check ?x ?y ?z))

(defnoticer +noticer3
    ((lower-bound ?y ?ylb)
     (production ?x + ?y ?z))
  ?justification
  (+-check ?x ?y ?z))

(defnoticer +noticer4
    ((lower-bound ?y ?ylb)
     (production ?x + ?z ?y))
  ?justification
  (+-check ?x ?y ?z))

(defnoticer +noticer5
    ((upper-bound ?x ?xub)
     (production ?x + ?y ?z))
  ?justification
  (+-check ?x ?y ?z))

(defnoticer +noticer6
    ((upper-bound ?y ?yub)
     (production ?x + ?y ?z))
  ?justification
  (+-check ?x ?y ?z))

(defnoticer +noticer7
    ((upper-bound ?y ?yub)
     (production ?x + ?z ?y))
  ?justification
  (+-check ?x ?y ?z))

(defun +-check (x y z) ;x=y+z.
  (let ((ylb (var-lower-bound y))
	(zlb (var-lower-bound z))
	(yub (var-upper-bound y))
	(zub (var-upper-bound z))
	(xlb (var-lower-bound x))
	(xub (var-upper-bound x)))
    (when (and ylb zlb)
      (set-lower-bound x (+ ylb zlb) (justification '+-bound-prop `(lower-bound ,y ,ylb) `(lower-bound ,z ,zlb))))
    (when (and yub zub)
      (set-upper-bound x (+ yub zub) (justification '+-bound-prop `(upper-bound ,y ,yub) `(upper-bound ,x ,zub))))
    (when (and xlb zub)
      (set-lower-bound y (- xlb zub) (justification '+-bound-prop `(lower-bound ,x ,xlb) `(upper-bound ,z ,zub))))
    (when (and xub zlb)
      (set-upper-bound y (- xub zlb) (justification '+-bound-prop `(upper-bound ,x ,xub) `(lower-bound ,z ,zlb))))
    (when (and xlb yub)
      (set-lower-bound z (- xlb yub) (justification '+-bound-prop `(lower-bound ,x ,xlb) `(upper-bound ,y ,yub))))
    (when (and xub ylb)
      (set-upper-bound z (- xub ylb) (justification '+-bound-prop `(upper-bound ,x ,xub) `(lower-bound ,y ,ylb))))))

(defnoticer -noticer1 ((production ?z - ?x ?y))
  (equate-vars ?x (intern-node2 `(+ ,?z ,?y)) ?justification))

(defnoticer *noticer1 ((production ?x * ?y ?z))
  ?justification
  (*-consistency-check ?x ?y ?z))

(defnoticer *noticer2 ((upper-bound ?x ?xub)
		       (production ?x * ?y ?z))
  ?justification
  (*-consistency-check ?x ?y ?z))

(defnoticer *noticer3 ((upper-bound ?y ?xub)
		       (production ?x * ?y ?z))
  ?justification
  (*-consistency-check ?x ?y ?z))

(defnoticer *noticer4 ((upper-bound ?z ?xub)
		       (production ?x * ?y ?z))
  ?justification
  (*-consistency-check ?x ?y ?z))

(defnoticer *noticer5 ((lower-bound ?x ?xub)
		       (production ?x * ?y ?z))
  ?justification
  (*-consistency-check ?x ?y ?z))

(defnoticer *noticer6 ((lower-bound ?y ?xub)
		       (production ?x * ?y ?z))
  ?justification
  (*-consistency-check ?x ?y ?z))

(defnoticer *noticer7 ((lower-bound ?z ?xub)
		       (production ?x * ?y ?z))
  ?justification
  (*-consistency-check ?x ?y ?z))

;in the following x = y*z

(defun *-consistency-check (x y z)
  (let ((xub (var-upper-bound x))
	(xlb (var-lower-bound x))
	(yub (var-upper-bound y))
	(ylb (var-lower-bound y))
	(zub (var-upper-bound z))
	(zlb (var-lower-bound z))
	(xubf nil)
	(xlbf nil))
    (when (and ylb (> ylb 0))
      (when zlb
	(setf xlbf t)
	(set-lower-bound x (* ylb zlb) (justification '*-prop `(lower-bound ,y ,ylb) `(lower-bound ,z ,zlb))))
      (when (and zub yub)
	(setf xubf t)
	(set-upper-bound x (* yub zub) (justification '*-prop
						     `(lower-bound ,y ,ylb)
						     `(upper-bound ,y ,yub)
						     `(upper-bound ,z ,zub))))
      (when xub
	(set-upper-bound z (/ xub ylb) (justification '*-prop `(lower-bound ,y ,ylb) `(upper-bound ,x ,xub))))
      (when (and yub xlb)
	(set-lower-bound z (/ xlb yub) (justification '*-prop
						      `(lower-bound ,y ,ylb)
						      `(lower-bound ,x ,xlb)
						      `(upper-bound ,y ,yub)))))
    (when (and yub (< yub 0))
      (when zub
	(setf xlbf t)
	(set-lower-bound x (* yub zub) (justification '*-prop `(upper-bound ,y ,yub) `(upper-bound ,z ,zub))))
      (when (and zlb ylb)
	(setf xubf t)
	(set-upper-bound x (* ylb zlb) (justification '*-prop
						     `(lower-bound ,y ,ylb)
						     `(upper-bound ,y ,yub)
						     `(upper-bound ,z ,zlb))))
      (when xlb
	(set-upper-bound z (/ xlb yub) (justification '*-prop `(upper-bound ,y ,yub) `(lower-bound ,x ,xlb))))
      (when (and ylb xub)
	(set-lower-bound z (/ xub ylb) (justification '*-prop
						      `(lower-bound ,y ,ylb)
						      `(upper-bound ,x ,xub)
						      `(upper-bound ,y ,yub)))))
    (when (and zlb (> zlb 0))
      (when (and ylb (not xlbf))
	(setf xlbf t)
	(set-lower-bound x (* ylb zlb) (justification '*-prop `(lower-bound ,y ,ylb) `(lower-bound ,z ,zlb))))
      (when (and zub yub (not xubf))
	(setf xubf t)
	(set-upper-bound x (* yub zub) (justification '*-prop
						     `(lower-bound ,z ,zlb)
						     `(upper-bound ,y ,yub)
						     `(upper-bound ,z ,zub))))
      (when xub
	(set-upper-bound y (/ xub zlb) (justification '*-prop `(lower-bound ,z ,zlb) `(upper-bound ,x ,xub))))
      (when (and zub xlb)
	(set-lower-bound y (/ xlb zub) (justification '*-prop
						      `(lower-bound ,z ,zlb)
						      `(lower-bound ,x ,zlb)
						      `(upper-bound ,z ,zub)))))
    (when (and zub (< zub 0))
      (when (and yub (not xlbf))
	(setf xlbf t)
	(set-lower-bound x (* yub zub) (justification '*-prop `(upper-bound ,y ,yub) `(upper-bound ,z ,zub))))
      (when (and ylb zlb (not xubf))
	(setf xubf t)
	(set-upper-bound x (* ylb zlb) (justification '*-prop
						     `(lower-bound ,y ,ylb)
						     `(upper-bound ,z ,zub)
						     `(upper-bound ,z ,zlb))))
      (when xub
	(set-upper-bound y (/ xub zlb) (justification '*-prop `(lower-bound ,z ,zlb) `(upper-bound ,x ,xub))))
      (when (and zub xlb)
	(set-lower-bound y (/ xlb zub) (justification '*-prop
						      `(lower-bound ,z ,zlb)
						      `(lower-bound ,x ,xlb)
						      `(upper-bound ,z ,zub)))))
    (when (and yub ylb zub zlb (or (not xubf) (not xlbf)))
      (let ((yz1 (* yub zub))
	    (yz2 (* yub zlb))
	    (yz3 (* ylb zub))
	    (yz4 (* ylb zlb))
	    (just (justification '*-prop
				 `(upper-bound ,y ,yub)
				 `(lower-bound ,y ,ylb)
				 `(upper-bound ,z ,zub)
				 `(lower-bound ,z ,zlb))))
	(unless xubf (set-upper-bound x (max yz1 yz2 yz3 yz4) just))
	(unless xlbf (set-lower-bound x (min yz1 yz2 yz3 yz4) just))))))

(defnoticer =noticer1 ((production ?phi = ?x ?y))
  ?justification
  (check-=-consistency ?phi ?x ?y))

(defnoticer =noticer2 ((has-value ?phi :anything)
		       (production ?phi = ?x ?y))
  ?justification
  (check-=-consistency ?phi ?x ?y))

(defnoticer =noticer3 ((upper-bound ?x :anything)
		       (production ?phi = ?x ?y))
  ?justification
  (check-=-consistency ?phi ?x ?y))

(defnoticer =noticer4 ((upper-bound ?y :anything)
		       (production ?phi = ?x ?y))
  ?justification
  (check-=-consistency ?phi ?x ?y))

(defnoticer =noticer5 ((lower-bound ?x :anything)
		       (production ?phi = ?x ?y))
  ?justification
  (check-=-consistency ?phi ?x ?y))

(defnoticer =noticer6 ((lower-bound ?y :anything)
		       (production ?phi = ?x ?y))
  ?justification
  (check-=-consistency ?phi ?x ?y))


(defun check-=-consistency (phi x y)
  (let ((ylb (var-lower-bound y))
	(yub (var-upper-bound y))
	(xlb (var-lower-bound x))
	(xub (var-upper-bound x)))
    (when (and xlb yub (> xlb (+ yub *infinitetesimal*)))
      (set-value phi 'false (justification 'bounds-inference
					   `(production ,phi = ,x ,y)
					   `(upper-bound ,y ,yub)
					   `(lower-bound ,x ,xlb))))
    (when (and ylb xub (> ylb (+ xub *infinitetesimal*)))
      (set-value phi 'false (justification 'bounds-inference
					   `(production ,phi = ,x ,y)
					   `(upper-bound ,x ,xub)
					   `(lower-bound ,y ,ylb))))))

(defnoticer /-noticer1 ((production ?z / ?x ?y))
  (equate-vars ?x (intern-node2 `(* ,?z ,?y)) ?justification))

(defnoticer >noticer1 ((production ?phi > ?x ?y))
  ?justification
  (check->-consistency ?phi ?x ?y))

(defnoticer >noticer2 ((has-value ?phi :anything)
		       (production ?phi > ?x ?y))
  ?justification
  (check->-consistency ?phi ?x ?y))

(defnoticer >noticer3 ((upper-bound ?x :anything)
		       (production ?phi > ?x ?y))
  ?justification
  (check->-consistency ?phi ?x ?y))

(defnoticer >noticer4 ((upper-bound ?y :anything)
		       (production ?phi > ?x ?y))
  ?justification
  (check->-consistency ?phi ?x ?y))

(defnoticer >noticer5 ((lower-bound ?x :anything)
		       (production ?phi > ?x ?y))
  ?justification
  (check->-consistency ?phi ?x ?y))

(defnoticer >noticer6 ((lower-bound ?y :anything)
		       (production ?phi > ?x ?y))
  ?justification
  (check->-consistency ?phi ?x ?y))

(defnoticer >noticer7 ((production ?phi > ?x ?x))
  (assert-internal `(has-value ,?phi false) ?justification))

(defun check->-consistency (phi x y)
  (let ((xlb (var-lower-bound x))
	(xub (var-upper-bound x))
	(ylb (var-lower-bound y))
	(yub (var-upper-bound y)))
    (when (and xlb yub (> xlb yub))
      (set-value phi 'true (justification 'bounds-inference
					  `(production ,phi > ,x ,y)
					  `(upper-bound ,y ,yub)
					  `(lower-bound ,x ,xlb))))
    (when (and ylb xub (> ylb xub))
      (set-value phi 'false (justification 'bounds-inference
					   `(production ,phi > ,x ,y)
					   `(upper-bound ,x ,xub)
					   `(lower-bound ,y ,ylb))))
    (when (eq (var-value phi) 'true)
      (when ylb
	(set-lower-bound x ylb (justification 'bounds-inference
					      `(production ,phi > ,x ,y)
					      `(has-value ,phi true)
					      `(lower-bound ,y ,ylb))))
      (when xub
	(set-upper-bound y xub (justification 'bounds-inference
					      `(production ,phi > ,x ,y)
					      `(has-value ,phi true)
					      `(upper-bound ,x ,xub)))))
    (when (eq (var-value phi) 'false)
      (when xlb
	(set-lower-bound y xlb  (justification 'bounds-inference
					       `(production ,phi > ,x ,y)
					       `(has-value ,phi false)
					       `(lower-bound ,x ,xlb))))
      (when yub
	(set-upper-bound x yub (justification 'bounds-inference
					      `(production ,phi > ,x ,y)
					      `(has-value ,phi false)
					      `(upper-bound ,y ,yub)))))))

;;the inference rules for >= are identical to those for >.

(defnoticer >=noticer1 ((production ?phi >= ?x ?y))
  ?justification
  (check->-consistency ?phi ?x ?y))

(defnoticer >=noticer2 ((has-value ?phi :anything)
		       (production ?phi >= ?x ?y))
  ?justification
  (check->-consistency ?phi ?x ?y))

(defnoticer >=noticer3 ((upper-bound ?x :anything)
		       (production ?phi >= ?x ?y))
  ?justification
  (check->-consistency ?phi ?x ?y))

(defnoticer >=noticer4 ((upper-bound ?y :anything)
		       (production ?phi >= ?x ?y))
  ?justification
  (check->-consistency ?phi ?x ?y))

(defnoticer >=noticer5 ((lower-bound ?x :anything)
		       (production ?phi >= ?x ?y))
  ?justification
  (check->-consistency ?phi ?x ?y))

(defnoticer >=noticer6 ((lower-bound ?y :anything)
			(production ?phi >= ?x ?y))
  ?justification
  (check->-consistency ?phi ?x ?y))

(defnoticer >=noticer7 ((production ?phi >= ?x ?x))
  (assert-internal `(has-value ,?phi true) ?justification))