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

;;;; Rule for enforcing constraints on sets
;; 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.

;;; 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)

(rule ((:true (set ?name) :var ?f1))
  (rule ((:intern (?name members ?construal1) :var ?f2))
    (rule ((:intern (?name has-member ?new) :var ?f3
		    :test (not (member ?new ?construal1
				       :test #'equal))))
	  (rassert! (:implies (:and ?f1 ?f2) (:not ?f3))
		    :not-in-set))
    (rule ((:intern (?name members ?construal2) :var ?f3
	     :test (and (form< ?f2 ?f3) ;; avoid redundant nogoods
			(set-exclusive-or ?construal1
					  ?construal2
					  :test 'equal))))
	  (rassert! (:not (:and ?f1 ?f2 ?f3))
		    :construal-uniqueness))))

;;; It's important to avoid duplicate justifications, especially in
;;; large problems.  Do this by reifying justifications made by the
;;; CWA code in the LTRE database, using this rule to translate the
;;; statement into the appropriate clauses.  (These statements can
;;; safely be premises, because they are inviolate: only the
;;; statements which participate in them can be wrong.

(rule ((:intern (cwa-justification ?ante ?conse) :var ?cwaj))
  (rassert! (:implies ?cwaj
		      (:implies ?ante ?conse))
	    :cwa-justification))