;;; -*- Mode: LISP; Syntax: Common-lisp; -*-

;;;; Sample constraints for TCON interpreter.
;; Last edited 1/29/93, by KDF

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

(in-package :COMMON-LISP-USER)

(constraint adder ((a1 cell) (a2 cell) (sum cell))
	    (formulae (sum (a1 a2) (+ a1 a2))
		      (a1 (sum a2) (- sum a2))
		      (a2 (sum a1) (- sum a1))))

(constraint multiplier ((m1 cell) (m2 cell) (product cell))
 (formulae (product (m1) (if (nearly-zero? m1) 0.0 :DISMISS))
	   (product (m2) (if (nearly-zero? m2) 0.0 :DISMISS))
	   (product (m1 m2) (cond ((or (nearly-zero? m1)
				       (nearly-zero? m2))
				   :DISMISS)
				  (t (* m1 m2))))
	   (m1 (product m2) (if (nearly-zero? m2)
				(if (nearly-zero? product)
				    :DISMISS
				  :LOSE)
			      (/ product m2)))
	   (m2 (product m1) (if (nearly-zero? m1)
				(if (nearly-zero? product)
				    :DISMISS
				  :LOSE)
			      (/ product m1)))))

(constraint sign ((in cell) (out cell))
	    (formulae (out (in) (if (nearly-zero? in) 0.0
				    (signum in)))
		      (in (out) (if (= 0.0 out) 0.0 :DISMISS))))

(constraint magnitude ((in cell) (out cell))
	    (formulae (out (in) (if (nearly-zero? in) 0.0
				    (abs in)))
		      (in (out) (if (= 0.0 out)
				    0.0 :DISMISS))))

(constraint sign-magnitude ((number cell) (sign cell)
			    (magnitude cell)
			    (s sign) (m magnitude)
			    (prod multiplier))
	    (== (>> sign) (>> out s))
	    (== (>> magnitude) (>> out m))
	    (== (>> number) (>> in s))
	    (== (>> number) (>> in m))
	    ;Use multiplier constraint
	    (== (>> number) (>> product prod))
	    (== (>> sign) (>> m1 prod))
	    (== (>> magnitude) (>> m2 prod)))

;;;; Temperature conversion and other classics

(constraint F-to-C ((degF cell) (degC cell)
		    (sum adder)(m multiplier))
	    (== (>> degF) (>> sum sum))
	    (Constant (>> a1 sum) 32)
	    (== (>> a2 sum) (>> product m))
	    (== (>> degC) (>> m1 m))
	    (Constant (>> m2 m) (float (/ 9 5))))
;; Primitive boolean constraints.

(constraint implication ((antecedent cell) (consequent cell))
 (formulae (consequent (antecedent)
		       (cond (antecedent 'T) (t  :DISMISS)))
	   (antecedent (consequent)
		       (cond (consequent :DISMISS) (t 'NIL)))))

(constraint or-gate ((in1 cell) (in2 cell) (out cell))
      (formulae (out (in1 in2) (or in1 in2))
		(out (in1) (cond (in1 t) (t :DISMISS)))
		(out (in2) (cond (in2 t) (t :DISMISS)))
		(in1 (out in2) (cond ((not in2) out)
				     (t :DISMISS)))
		(in2 (out in1) (cond ((not in1) out)
				     (t :DISMISS)))))

(constraint and-gate ((in1 cell) (in2 cell) (out cell))
	    (formulae (out (in1 in2) (and in1 in2))
		      (out (in1) (cond (in1 :DISMISS)
				       (t nil)))
		      (out (in2) (cond (in2 :DISMISS)
				       (t nil)))
		      (in1 (out in2) (cond (in2 out)
					   (T :DISMISS)))
		      (in2 (out in1) (cond (in1 out)
					   (t :DISMISS)))))

(constraint relay ((in1 cell) (in2 cell) (out cell)
		   (control cell))
  (formulae (in1 (out control) (cond (control out)
				     (t :DISMISS)))
	    (in2 (out control) (cond (control :DISMISS)
				     (t out)))
	    (out (in1 control) (cond (control in1)
				     (t :DISMISS)))
	    (out (in2 control (cond (control :DISMISS)
				    (t in2))))))

;;; Constraints for GDE examples

(constraint node ((value cell)))

(constraint adder-component ((a1 cell) (a2 cell) (sum cell)
			     (ok assumption))
	    (formulae (sum (a1 a2 ok) (+ a1 a2))
		      (a1 (sum a2 ok) (- sum a2))
		      (a2 (sum a1 ok) (- sum a1))))

(constraint multiplier-component ((m1 cell) (m2 cell) (product cell)
				  (ok assumption))
 (formulae (product (m1) (if (nearly-zero? m1) 0.0 :DISMISS))
	   (product (m2) (if (nearly-zero? m2) 0.0 :DISMISS))
	   (product (m1 m2 ok) (cond ((or (nearly-zero? m1)
					  (nearly-zero? m2))
				      :DISMISS)
				     (t (* m1 m2))))
	   (m1 (product m2 ok) (if (nearly-zero? m2) :DISMISS
				   (/ product m2)))
	   (m2 (product m1 ok) (if (nearly-zero? m1) :DISMISS
				   (/ product m1)))))

(constraint or-component ((in1 cell) (in2 cell) (out cell)
			  (ok assumption))
      (formulae (out (in1 in2 ok)
		     (if (and (= in1 0) (in2 0)) 0 :DISMISS))
		(out (in1 ok) (if (= in1 1) 1 :DISMISS))
		(out (in2 ok) (if (= in2 1) 1 :DISMISS))
		(in1 (out in2 ok)
		     (if (and (= out 1) (= in2 0)) 1 :DISMISS))
		(in2 (out in1 ok)
		     (if (and (= out 1) (= in1 0)) 1 :DISMISS))
		(in1 (out ok) (if (= out 0) 0 :DISMISS))
		(in2 (out ok) (if (= out 0) 0 :DISMISS))))

(constraint inverter-component ((in cell) (out cell) (ok assumption))
      (formulae (in (out ok) (if (= out 0) 1 0))
		(out (in ok) (if (= in 0) 1 0))))

(assume-constraint and-component ((in1 cell) (in2 cell) (out cell))
	    (formulae (out (in1 in2) (and in1 in2))
		      (out (in1) (cond (in1 :DISMISS)
				       (t nil)))
		      (out (in2) (cond (in2 :DISMISS)
				       (t nil)))
		      (in1 (out in2) (cond (in2 out)
					   (t :DISMISS)))	
		      (in2 (out in1) (cond (in1 out)
					   (t :DISMISS)))))

(defun nearly-zero? (x) (nearly-equal? x 0))