;;; -*- Syntax:Common-Lisp; Mode: LISP; Package: (TMS Lisp 1000.); Base: 10. -*-

(in-package 'tms)

"(c) Copyright 1986, 1987, 1988 Xerox Corporation.  All rights reserved.  Subject to
the following conditions, permission is granted to use and copy this
software and to prepare derivative works:  Such use, copying or
preparation of derivative works must be for non-commercial research or
educational purposes; each copy or derivative work must include this
copyright notice in full; a copy of each completed derivative work must
be returned to:  DEKLEER@XEROX.COM (Arpanet) or Johan de Kleer,
Xerox PARC, 3333 Coyote Hill Road, Palo Alto, CA 94304.  This software
is made available AS IS, and Xerox Corporation makes no warranty about
the software or its performance."

;;; Have a type of class which is unique --- it would make consumers much easier.

;;; Consumers should not be closures I think, just pairs (vars . f).

;;; Have three classes of assumptions: choose,default,disjunction.

;;; Save conses somewhere by having a *vector* cache?

;;; Copylist is not the best in places.  Make cons-env etc fster.

;;; Try to make parity run faster.

;;; reclaim node is very slow.

;;; Need a division functin that returns the result and its remainder.

;;; o with resolution contras are not removed when subsumed?

;;;****inclusive or does not work right, or for interpretation construction/resolution.
;;; Should assumption-envs be a singleton or not.  Depends on mapping on n-a-envs.

;;; o there should be a disjunction data base kept in simplest form, like nogoods.

;;; o A class should not have a disjunction property which lists its assumptions.

;;; o cons-env should explicitly check that the consed assumption is not contradictory
;;;   either.

;;; o the node propagator maybe should check this too.

;;; o when a node receives an empty environment maybe the contradictory propagator should
;;;   be reinvoked by checking whether the consequent is contradictory and if that is the
;;;   only antecedent...

;;; o is there any justification stored with a contradiction.  That might be useful for 
;;;   debugging.

;;; o run the assumption-gc before rehahashing and only if there is some gcable ones.

;;; ****something very broken about assumptions.

;;; This cries out for lexical closures. ("Oh for a SCHEME").


;;; I guess classes can be nodes too and we have reflection (eh eh).

;;; This is the new assumption-based TMS. Implemented badly to play with. 
;;; Contradictions can only be retracted with great pain in this version.

;;***** nogoods may interact with contras---think about this later.

;;; ***Perhaps we should use thread cells instead of lists? for *nodes*, *assumptions*.


;;; This class stuff will soon be obsolete.
(defun assume-symbol (p-node n-node class &aux p-assumption n-assumption
		                               (old-trace-file *trace-file*) *trace-file*)
  (when old-trace-file
    (format old-trace-file "~%ASY ~D ~D ~D"
	    (n-a-unique p-node) (n-a-unique n-node) (if class (class-unique class))))
  (multiple-value-setq (p-assumption n-assumption)
    (create-symbol nil nil T T))
  (contradictory-assumption-pair p-assumption n-assumption)
  (if (node-assumption p-node) (error "Already assumed"))
  (if (node-assumption n-node) (error "Already assumed"))
  (setf (node-assumption p-node) p-assumption)
  (setf (node-assumption n-node) n-assumption)
  (setf (assumption-node p-assumption) p-node)
  (setf (assumption-node n-assumption) n-node)
  ;; Point the assumptions for

  (setf (assumption-datum p-assumption) nil)
  (setf (assumption-datum n-assumption) nil)
  ;; ***** we could just do this by hand with update-node1
  (justify-node p-node (list 'ASSUME-NODE p-assumption))
  (justify-node n-node (list 'ASSUME-NODE n-assumption))
  (when class
    (setf (class-assumptions class) (list p-assumption n-assumption))
    ;; Stupid, resolution should know about negations.  This is a stupid
    ;; way to encode it.
    (close-variable-class class)))

;;; This probably should do something more intelligent if the number if only
;;; two assumptions are introduced.

(defun assume-oneof (nodes datum
		     &aux (old-trace-file *trace-file*) 
		     class *trace-file* assumption-class assumption)
  datum						; Unused right now.
  (when old-trace-file
    (format old-trace-file "~%C-X-C-F-N2 (")
    (mapc #'(lambda (n-a) (trace-node n-a old-trace-file)) nodes)
    (format old-trace-file ")"))
  ;; This is now just an error check.
  (dolist (c (n-a-classes (car nodes)))
    (unless (dolist (node (cdr nodes))
	      (or (memq c (n-a-classes node)) (return T)))
      ;; Not quite right because false nodes are removed.
      ;;****** Bug caused by ex-cl trace need ATOM test here.
      ;;******* In efficient fix.
      (cond ((and (listp (class-datum c))
		  (eq 'ONEOF (car (class-datum c)))
		  (same-setp nodes (class-nodes c)))
	     (setq class c)
	     (return nil)))
      (error "I thought this couldn't happen")
      (return nil)))
  ;; First do a regular oneof.
  (setq class (oneof nodes class))
  ;; If one of the nodes is determined, we're done.
  (unless class (return-from ASSUME-ONEOF t))
  ;; Now put an assumption under each one which isn't true or false, and
  ;; create another oneof for those --- its unclear whether ultimately this
  ;; will be worth it or not.
  (setq assumption-class (create-class (cons 'ASSUME-ONEOF nodes) T T))
  (dolist (node (class-nodes class))
    (if (node-assumption node) (error "Node has already been assumed"))
    (setq assumption (basic-make-assumption class node nil))
    (setf (node-assumption node) assumption)
    (setf (assumption-node assumption) node)
    (dolist (a (class-nodes assumption-class)) (contradictory-assumption-pair assumption a))
    (add-class-to-node assumption assumption-class)
    (justify-node node (list 'ASSUME-NODE assumption))
    ;; This cannot cause anymore propagations now.
    (setf (n-a-neg assumption) (n-a-neg node))
    (push assumption (class-assumptions class)))
  (close-variable-class class)
  )

(defun create-xor-node (datum class &aux node)
  (setq node (create-node datum))
  (justify-node node (list 'ASSUME (make-a-assumption class datum)))
  (add-class-to-node node class)
  node)

(defun assumed-node? (node) (node-assumption node))

;;; This could be done better ...
(defun create-xor-assumption-set (values &aux class)
  (setq class (create-class values))
  (prog1 (mapcar #'(lambda (value) (make-a-assumption class value)) values)
	 (close-variable-class class)))

;;; This is not right ******** The disjunction is missing.
(defun create-ior-assumption-set (values) (mapcar #'create-assumption values))


;;; A set of assumptions form an inclusive disjunction.  This should **only** be called
;;; from top-level.
(defun choose (assumptions informant &aux nassumptions or vector count)
  (setq or (make-disjunction :ODISJUNCTS assumptions :INFORMANTS (list informant)))	;**** delay creation.
  (dolist (a assumptions) (or (i-false? a)
			      (memq a nassumptions)
			      (push a nassumptions)))
  ;********* throw contradiction.
  (cond ((null nassumptions) (error "There are no assumptions left of this choose."))
	((null (cdr nassumptions))
	 (true-assumption (car nassumptions) (cons 'RESOLVE or))
	 (if *luser-warning* (format T "~% Disjunction is a singleton."))
	 nil)
	;; First go see if it is already present.  Hash table may be used here eventually.
	((progn (setq vector (make-env-vector* nassumptions) count (length nassumptions))
		(dolist (d (aref *ors* count))
		  (when (vector-equal vector (disjunction-vector d)) 
		    (format T "~% Disjunction is already present")
		    (return d)))))
	;; If subsumed, ignore it as well.
	((do ((i 2 (1+ i))) ((= i count) nil)
	   (if (dolist (d (aref *ors* i)) (if (vector-subset (disjunction-vector d) vector)
					      (return T)))
	       (return T)))
	 (format T "~% Disjunction is subsumed.")
	 nil)
	;; Else its a new disjunction that needs to be analyzed.  
	(t (setf (disjunction-disjuncts or) nassumptions
		 (disjunction-count or) count
		 (disjunction-vector or) vector)
	   (if (or *resolve-by-labeling* *resolve-by-ordered-labeling*)
	       (contradiction (cons '(CHOOSE)
				    (mapcar #'negate-assumption-to-node nassumptions))))
	   (add-or or)
	   (and *h4* (> count *h4*) (new-disjunction or))
	   ;; We always have to do this because the basic resolution rules: true-assumption,
	   ;; false-assumption, are always active and refer to this data structure.  Errors
	   ;; will result if this is not done.
	   (dolist (a nassumptions) (push or (assumption-ors a)))
	   or
	   )))

;;; This adds a disjunction back in which was just removed.  It is guaranteed to
;;; have 2 or more disjuncts and is not subsumed or already in the table.
;;;********* who makes the vector correct after a delete??????
;;;********* this is extremely ineficient.
(defun add-or (or &aux count vector vectors)
  (if (disjunction-satisfied or) (error "Why are you adding"))

  (setq count (disjunction-count or) vector (disjunction-vector or))
  (push or (aref *ors* count))
  ;; Remove any superior disjunctions.
  (do ((i (1+ count) (1+ i)))
      ((> i 99.)) ;;**** *max-ior-count*
    (setq vectors (aref *ors* i))
    (do ((previous nil)
	 (d vectors (cdr d)))
	((null d))
      ;**** propersubset of course????
      (cond ((vector-subset vector (disjunction-vector (car d)))
	     (excise-or (car d))
	     (if previous (rplacd previous (cdr d)) (setq vectors (cdr d))))
	    (t (setq previous d))))
    (setf (aref *ors* i) vectors))
  ;; The binary resolutions to produce justifications are very fast, easy, and
  ;; useful. This produces A->A justifications only.  This often loses actually,
  ;; I default it to false these days.  This will cause recursive calls under
  ;; resolution if we do this.  This may not be what we want.  So think hard
  ;; about ever set *h45* to T.
  (and *h45* (= count 2) (binary-disjunction or)))

;;; Use this if you are truely getting rid of a disjunction.
(defun excise-or (or)
  (remove-or or)
  (dolist (assumption (disjunction-disjuncts or))
    (setf (assumption-ors assumption)
	  (fdelq1 or (assumption-ors assumption)))))

#+(OR :CL-ZL :ZL :CADR)
(defun remove-or (or) (fdelq1 or (zl:aloc *ors* (disjunction-count or))))

#+(OR :IL :CL)
(defun remove-or (or &aux slot new-slot)
  (setq new-slot (fdelq1 or (setq slot (aref *ors* (disjunction-count or)))))
  (unless (eq new-slot slot)
    (setf (aref *ors* (disjunction-count or)) new-slot))
  (if (memq or (aref *ors* (disjunction-count or))) (error "Ho is this possible")))

;;; Binary disjunctions resolve with ANY nogood they intersect with but not subset.
;;; Call this on encountering a new binary disjunction.
(defun binary-disjunction (or &aux vector cassumptions dassumptions d1 d2 resolves)
  (incf *binary-resolution-count*)
  (setq vector (disjunction-vector or)
	dassumptions (disjunction-disjuncts or)
	d1 (car dassumptions)
	d2 (cadr dassumptions))
  ;;****** its probably smarter to scan through all the nogoods each assumption is part of!!!.
  ;;****** thats guaranteed to be a smaller data base, this ponders every base
  ;;****** contradiction.
  (walk-contradictions
    #'(lambda (c)
	#+Symbolics
	(declare (sys:downward-function))
	(cond ((vector-subset vector (env-vector c)))
	      ((not (vector-intersection? vector (env-vector c))))
	      (t (push c resolves))))
    1)
  ;; **** is it worth checking its not subsumed?
  (dolist (c resolves)
    (setq cassumptions (env-assumptions c))
    (cond ((memq d1 cassumptions)
	   (justify-node d2 (cons 'BINARY-RESOLUTION (remove d1 cassumptions :count 1))))
	  ((memq d2 cassumptions)
	   (justify-node d1 (cons 'BINARY-RESOLUTION (remove d2 cassumptions :count 1)))))))

;;; Only called if *h4* says so.
;;; We don't distinguish between old original or induced nogoods.  So we have
;;; to run this rule on all nogoods.  **** Actually we might be able to look at 
;;; the justifications.   But what if the nogood is already ****??????
(DEFUN new-disjunction (or &aux count envs nogoods)
  ;; First construct its nogoods data base.
  (dolist (a (disjunction-disjuncts or))
    (setq count 0 envs nil)
    (dolist (env (assumption-nogoods a))
      (cond ((subsumed-nogood? env))
	    ((if *k* (> (env-count env) *k*)))
	    ((vector-intersection2? (env-vector env) (disjunction-vector or) a))
	    (t (push (uncons-env env a) envs)
	       (if *explain-flag*
		   (push (list (cons a (car envs)) env (env-contradictory-info env))
			 (disjunction-nogood-explanations or)))
	       (incf count))))
    ;; A singleton assumption in a nogood slot means there really is a pair environment
    ;; there.
    (cond ((if *k* (< *k* 2)))
	  ((null (assumption-binary-vector a)))
	  ((vector-subset (assumption-binary-vector a) (disjunction-vector or)))
	  (t (map-assumptions (assumption (assumption-binary-vector a))
	       (unless (or (memq assumption (disjunction-disjuncts or)) (i-false? assumption))
		 ;; Notice that it can be hard to find the pair-wise environment
		 ;; which is nogood you will usually get contra-env back.
		 (if *explain-flag*
		     (push (list (cons a assumption) '<UNKNOWN> '<UNKNOWN>)
			   (disjunction-nogood-explanations or)))
		 (push assumption envs)
		 (incf count)))))
    (push (cons a (cons count envs)) nogoods))
  (sort nogoods #'(lambda (a1 a2) (< (cadr a1) (cadr a2))))
  (setf (disjunction-nogoods or) nogoods)
  (or1-recurse or nil *empty-env* nil))

;;; Call this whenever a new nogood is discovered.
(defun contradiction-binary-disjunction (env &aux vector resolves cassumptions d1 d2 binaries)
  (when (setq binaries (aref *ors* 2))
    (setq vector (env-vector env) cassumptions (env-assumptions env))
    (dolist (d binaries)
      (and (vector-intersection? vector (disjunction-vector d))
	   (not (vector-subset (disjunction-vector d) vector))
	   (push d resolves)))
    (dolist (d resolves)
      (incf *binary-resolution-count*)
      (setq d1 (car (disjunction-disjuncts d)) d2 (cadr (disjunction-disjuncts d)))
      (cond ((memq d1 cassumptions)
	     (justify-node d2 (cons 'BINARY-RESOLUTION
				    (remove d1 cassumptions :count 1))))
	    ((memq d2 cassumptions)
	     (justify-node d1 (cons 'BINARY-RESOLUTION
				    (remove d2 cassumptions :count 1))))))))
    

;;; This is the rule H4.  
;;; *H4* = NIL, does nothing.
;;; *H4* = 1, does everything.
;;; *H4* = 2, ignores binary disjunctions.

;;; Call this upon the discovery of any new nogood.
;;; Note that it is unnecessary to resolve new nogoods produced by the resolver
;;; itself.  Hence the *dont* flag.
;;;****** see my commments about the *dont* flag.  In many many cases we don't
;;; need to process a new nogood over again.
(defun new-nogood (env &aux count max)
  (when (or (and *h4* (or (null *k*) (<= (env-count env) *k*)))
	    *resolve-by-labeling* *resolve-by-ordered-labeling*) ;(null *dont*)))
    (setq count (env-count env))
    (cond (*h4-adaptive*
	   (dolist (a (env-assumptions env))
	     (cond ((null (assumption-addb-index a))
		    (unless (assumption-nogood-stack a)
		      (setf (assumption-nogood-stack a) (make-array 20)))
		    (push env (aref (assumption-nogood-stack a) count)))
		   ((null max) (setq max a))
		   ((> (assumption-addb-index a) (assumption-addb-index max)) (setq max a))))
	   (when max
	     (unless (assumption-nogood-stack max)
	       (setf (assumption-nogood-stack max) (make-array 20)))
	     (push env (aref (assumption-nogood-stack max) count))))
	  (t (push env (aref *nogood-stack* count))
	     (if (< count *nogood-count*) (setq *nogood-count* count))))))

;;; This function could be called as often as after every justify-node.
(defun process-queued-nogoods (&aux *going-nodes* start-time)
  start-time
;  (setq start-time (get-internal-run-time))
  (cond ((or *resolve-by-labeling* *resolve-by-ordered-labeling*) (new-process-queued-nogoods))
	(*h4-adaptive* (adaptive-nogoods))
	(*h4* (old-process-queued-nogoods)))
  (if *going-nodes* (process-changed-nodes))
;  (format T "~% Resolving time (processing queued nogoods) is:~D seconds"
;	  (time-taken start-time))
)

;;;**** reprocess-or probably doesn't honor ordering.
;;; Could have a version which just incrementally went down ors.
(defun adaptive-nogoods (&aux env flag)
  ;; Once an assumption is processed, it need never be considered again this invokation.
  ;; That's not right either, because of incrementalness.
  ;; all assumptions in the same choose have the same priority.*****
  ;;***** only by luck are assumptions in decreasing order right now.
  (dolist (a *assumptions*)
    (do nil ((null *or-queue*))
      (reprocess-or (pop *or-queue*)))
    (do nil (nil)
      (setq flag nil)				;***** should wait until a new nogood.
      (when (assumption-nogood-stack a)
	(dotimes  (i 15.)				;****** global var for this.
	  (when (aref (assumption-nogood-stack a) i)
	    (setq env (pop (aref (assumption-nogood-stack a) i)))
	    (cond ((= i 1))
		  ((subsumed-nogood? env))
		  (t (if (or (null *max-nogood-used-size*)
			     (> *nogood-count* *max-nogood-used-size*))
			 (setq *max-nogood-used-size* *nogood-count*))
		     (or1-assumption env a)
		     (setq flag T)
		     (return))))))
      (unless flag (return)))))

;;; This seems like very inefficient becauses it often causes a complete sweep
;;; through the nogoods.
(defun old-process-queued-nogoods (&aux env)
  (do nil (nil)
    (do nil ((null *or-queue*))
      (reprocess-or (pop *or-queue*)))
    (do nil ((or *or-queue* (= *nogood-count* 100.)))
      (cond ((aref *nogood-stack* *nogood-count*)
	     (setq env (pop (aref *nogood-stack* *nogood-count*)))
	     ;;***** first form is now obsolete. and doesn't work.
	     (cond ((= *nogood-count* 1))
		   ;; **** I'm sure this is obsolete now.
		   ((listp env)
		    (apply #'or2-recurse (car env) (cdr env))
		    (process-changed-nodes))
		   ((subsumed-nogood? env))
		   ;; Singleton environments were automatically processed earlier,
		   ;; when it ran on the current set of shorter or-nogoods.
		   ((= (env-count env) 1))
		   (t (if (or (null *max-nogood-used-size*)
			      (> *nogood-count* *max-nogood-used-size*))
			  (setq *max-nogood-used-size* *nogood-count*))
		      (or1 env))))
	    (t (incf *nogood-count*))))
    (unless *or-queue* (return nil))))


(defun reprocess-or (or) (or1-recurse or nil *empty-env* nil))

;;; This borders on the insane, use only for experimentation.  Essentially, all resolutions
;;; are turned into a labeling problem with the benifit of *k*.  This can be highly
;;; optimized.
;;; **** if assumption updates automagically updated the nogood data base we'd 
;;; not need to construct these justifications!.  Just call update-node!?
;;; **** but we need to construct the environments for the negation just this time
;;; via a weaver though***
(defvar *dont* nil)
;;;*dont* is a temporary kludge.

;;; If an assumption has no negation, this does nothing.
;;; So if a lot of time is spent in this function...
;;; Optimize because new nogoods can't be produced by this scheme.  Aref's not necessary***
(defun new-process-queued-nogoods (&aux assumptions env (*dont* t) max)
  (do nil ((= *nogood-count* 100.))
    (cond ((aref *nogood-stack* *nogood-count*)
	   (setq env (pop (aref *nogood-stack* *nogood-count*)))
	   (cond ((subsumed-nogood? env))
		 ;; To prevent incredible recursion depth, singletons are run now, instead
		 ;; of immediately.
		 ((= *nogood-count* 1)
		  ;; If there was no negation ever constructed for it.  And it is now is
		  ;; false.  It can't play any role in future disjunctions.
		  (setq assumptions (env-assumptions env))
		  ;;; **** Assumption-negation is pretty well obsolete.  Flush it soon.
		  (if (assumption-negation (car assumptions))
		      (update-node1 (assumption-negation (car assumptions))
				    *empty-env-list*
				    *empty-env-list*))
		  ;; This is much cleaner now:
		  (if (n-a-neg (car assumptions))
		      (update-node1 (n-a-neg (car assumptions))
				    *empty-env-list*
				    *empty-env-list*)))
		 ;;** probably obsolete now.
		 (*resolve-by-labeling*
		    ;; These negated nodes will never have justifications.  Their
		    ;; labels are always updated with his present mechanism.  This
		    ;; can be optimized to only copy if necesary***
		    ;; Note that its a theorem that new-env cannot be subsumed.
		    ;; This does singletons also --- they can be optimized though.
                    ;; This is essentially the resolution rule here.
		    (dolist (a (env-assumptions env))
		      (if (subsumed-nogood? env) (return))
		      (minimal-nogood a env)))
		 ;; Any assumption not in ADDB ordering gets resolved automatically,
		 ;; only the maximal ADDB one does.
		 (*resolve-by-ordered-labeling*
		  (setq max nil)
		  (dolist (a (env-assumptions env))
		    (if (subsumed-nogood? env) (return))
		    (cond ((null (assumption-addb-index a))
			   (minimal-nogood a env))
			  ((null max) (setq max a))
			  ((> (assumption-addb-index a) (assumption-addb-index max))
			   (setq max a))))
		  (if max (minimal-nogood max env)))))
	  (t (incf *nogood-count*)))))

(defun minimal-nogood (a nogood &aux node new-env known-envs)
  (incf *minimal-nogood-count*)
  (when (and (not (subsumed-nogood? nogood))
	     (setq node (n-a-neg a)))
    (setq new-env (uncons-env nogood a)
	  known-envs (n-a-envs node))
    (if (env-contradictory new-env) (error "Can't happen"))
    ;; The new-env could concievably be a support already because it provoked the contra.
    ;; If so we can infer nothing new.
    (if (memq new-env known-envs) (return-from minimal-nogood nil))
    ;; Else do a psuedo label update.
    (setq known-envs (fcopylist known-envs))
    (do ((known-envs known-envs (cdr known-envs)))
	((null known-envs))
      (if (proper-subset-env? new-env (car known-envs))
	  (rplaca known-envs nil)))
    (setq known-envs (cons new-env (fdelqa nil known-envs)))
;			(format T "~% Updating ~A with ~A" node (string-env new-env))

    (update-node1 node
		  (ncons new-env)
		  known-envs)))

;;; Do not create the binary disjunction or nogood.  Then we'll recurse forever.
;;; (Well, not really, but there is no point in doing that).
(defun negate-assumption-to-node (assumption)
  (or (assumption-negation assumption)
      (setf (assumption-negation assumption)
	    (create-node (cons 'NOT assumption)))))

;;;****** assumption-negation is overloaded.
(defun negate-assumption (assumption &aux negation)
  (cond ((assumption-negation assumption))
	(t (setq negation (create-assumption (cons 'NOT assumption)))
	   (setf (assumption-negation assumption) negation)
	   (setf (assumption-negation negation) assumption)
	   (choose (list assumption negation) '(NEGATE-ASSUMPTION))
	   negation)))

;		 (*resolve-by-ordered-labeling*
;		  (setq max nil)
;		  (dolist (a (env-assumptions env))
;		    (if (subsumed-nogood? env) (return))
;		    (cond ((null (assumption-addb-index a))
;			   (minimal-nogood a env))
;			  ((null max) (setq max a))
;			  ((> (assumption-addb-index a) (assumption-addb-index max))
;			   (setq max a))))
;		  (if max (minimal-nogood max env)))

(defun or1 (nogood &aux max)
  (dolist (a (env-assumptions nogood))
    (if (subsumed-nogood? nogood) (return-from OR1 nil))
    (cond ((null (assumption-addb-index a)) (or1-assumption nogood a))
	  ((null max) (setq max a))
	  ((> (assumption-addb-index a) (assumption-addb-index max)) (setq max a))))
  (if max (or1-assumption nogood max)))

(defun or1-assumption (env a &aux cvector uncons slot)
  (setq cvector (env-vector env))
  (setq uncons (uncons-env env a))
  (dolist (or (assumption-ors a))
    (when (and (or (> (disjunction-count or) *h4*))
	       (null (vector-intersection2? cvector (disjunction-vector or) a))
	       (null (memq env (setq slot (assq a (disjunction-nogoods or))))))
      (if *explain-flag*
	  (push (list (cons a uncons) env (env-contradictory-info env))
		(disjunction-nogood-explanations or)))
      ;; A slot looks like (assumption count uncons-nogoods ...)
      (cond (slot (rplacd (cdr slot) (cons uncons (cddr slot)))
		  (incf (cadr slot)))
	    (t (unless (memq a (disjunction-disjuncts or)) (error "Uh?"))
	       (push (cons a (cons 1 (ncons uncons))) (disjunction-nogoods or))))
      (or1-recurse or a uncons env)
      (if (subsumed-nogood? env) (return-from OR1-ASSUMPTION nil))
      (sort-nogoods (disjunction-nogoods or))))
  )

;;; For some reason sort is extremely expensive?
(defun sort-nogoods (nogoods &aux needed)
  (do ((nogoods nogoods (cdr nogoods)))
      ((null (cdr nogoods)) (if (= 0 (cadar nogoods)) (return-from SORT-NOGOODS nil)))
    (if (= 0 (cadar nogoods)) (return-from SORT-NOGOODS nil))
    (if (> (cadar nogoods) (cadadr nogoods)) (setq needed T)))
  (if needed (sort nogoods #'(lambda (a1 a2) (< (cadr a1) (cadr a2))))))

;;; Returns NIL if some disjunct appears in no nogoods.
;;; This uses a simple heuristic for now to avoid updating costs.  It saves
;;; enough to worth the trouble.
(defun update-nogoods (or &aux nogoods update count alist disjuncts)
  (setq nogoods (disjunction-nogoods or))
  (if (= *contra-counter* (disjunction-contra-counter or)) (return-from UPDATE-NOGOODS nogoods))
  (setf (disjunction-contra-counter or) *contra-counter*)
  (setq disjuncts (disjunction-disjuncts or))
  (dolist (a disjuncts)
    (setq alist (assq a nogoods))
    (if (null alist) (return-from UPDATE-NOGOODS nil))
    (if (= 0 (cadr alist)) (return-from UPDATE-NOGOODS nil)))
  ;; Cleanup up the nogood data structure.  
  (dolist (alist nogoods)
    (setq count 0)
    (do ((at (cdr alist)))
	((null (cdr at)))
      (cond ((assumption? (cadr at))
	     (cond ((i-false? (cadr at)) (incf count) (rplacd at (cddr at)))
		   ((i-true? (cadr at)) (return nil))
		   (t (setq at (cdr at)))))
	    ((env-contradictory (cadr at))
	     (incf count)
	     (rplacd at (cddr at)))
	    (t (setq at (cdr at)))))
    (when (> count 0)
      (setq count (- (cadr alist) count))
      (rplaca (cdr alist) count)
      (if (= count 0) (return-from UPDATE-NOGOODS nil))
      (setq update T)))
  (if update (sort-nogoods nogoods))
  nogoods)

;;; ******* the contradictory-env call here for efficiency should also
;;; install the justifications for false******* or maybe that is all it should do.
;;; **************
;;;***** how often is one of the alphas subsumed, or the disjunction itself????

(defvar *or*)

;;; Note that the argument new-nogood is only used to generate explanations.
(defun or1-recurse (or assumption-to-ignore alphas new-nogood &aux nogoods)
  new-nogood
  (if (setq nogoods (update-nogoods or))
      (let ((*or* or))
	(or2-recurse nogoods assumption-to-ignore alphas
		     (if (and assumption-to-ignore *explain-flag*)
			 (list (cons assumption-to-ignore alphas)))))))

;;; contradictory-vector has to check explicitly (horribly are pair nogoods). We could
;;; check this going in.
;;; This is a brute force resolution rule.  It may or may not be better.
;(defun or2-recurse1 (disjunction-vector nogoods assumption-to-ignore alphas neg-clauses)

;(defun or2-recurse1 (disjunction-vector nogoods assumption-to-ignore alphas-vector)
;  (cond ((null nogoods)
;	 (contradictory-vector (vector-andc2 alphas-vector or-vector) '(RESOLUTION)))
;	((eq assumption-to-ignore (caar nogoods))
;n	 (or2-recurse1 or-vector nogoods nil alphas-vector))
;	(t (dolist (c (cddar nogoods))
;	     (unless (subsumed-nogood? c)
;	       (or2-recurse1 or-vector
;			     (cdr nogoods)
;			     assumption-to-ignore
;			     (vector-union alphas-vector (env-vector c))))))))

;;; *** neg-clauses is only consed up for explanation sake.
;;; ***** the assumption? here might be bullshit? I dunno.
;;; This takes all the time.
;;; Assumes alphas is consistent at calling time.
;;; *k*=2 should be really be done completely differently --- this algorithm is a dog.
(defun or2-recurse (nogoods assumption-to-ignore alphas neg-clauses
		    &aux next-alphas alphas-vector)
  (cond ((null (if (eq assumption-to-ignore (caar nogoods))
		   (setq nogoods (cdr nogoods))
		   nogoods))
	 (incf *full-resolution-count*)
	 ;; ***** Should we install a justification for false here? as well?  Its
	 ;; probably more efficient too?
	 (contradictory-env alphas (list 'BASE 'RESOLUTION *or* neg-clauses))
	 ;; Save conses here.
	 ;;********* this just makes no sense to me what this line is dong???
;	 (contradictory-just (list (list 'RESOLUTION *or* neg-clauses) alphas))
	 )
	(t ;(setq alphas-cache-vector (car (env-cons-env-cache alphas)
	    (setq alphas-vector (env-vector alphas))
;	   (incf index)
	   (dolist (c (cddar nogoods))
;	     (print (list 'trying c))
	     (cond ((assumption? c)
		    ;;******* this could be optimized also.*************** as below.
		    ;; Also ******is the or-nogoods optimizer really capable of processing
		    ;; this?
		    (unless (or (i-true? c) (i-false? c))
		      (setq next-alphas (cons-env alphas c))
;		      (if (and (eq foo c) (= index 1)) (error "hi"))
		      (unless (or (env-contradictory next-alphas)
				  (if *k* (>= (env-count next-alphas) *k*)))
			(or2-recurse (cdr nogoods)
				     assumption-to-ignore
				     next-alphas
				     (if *explain-flag*
					 (cons (cons (caar nogoods) c) neg-clauses)))	
			(if (env-contradictory alphas) (return)))))
		   ((env-contradictory c))
		   ;; The next two conditions open code a bit of union-env.  This turns
		   ;; out to be worth it.
;		   ((vector-intersection? alphas-cache-vector (env-vector c)))
		   ((vector-intersection? alphas-vector (car (env-cons-env-cache c))))
;		   ((dolist (a (env-assumptions c))
;		      (if (vector-intersection? alphas-vector (assumption-binary-vector a))
;			  (return T))))
		   ((env-contradictory (setq next-alphas (k-union-env alphas c))))
		   (t (or2-recurse (cdr nogoods)
				   assumption-to-ignore
				   next-alphas
				   (if *explain-flag* (cons (cons (caar nogoods) c)
							    neg-clauses)))
		      (if (env-contradictory alphas) (return)))))
;	   (decf index)
	   )))

;;; Doing union-env lazily above is a total disaster of the first order.  The reason
;;; is that there are just too many nogoods.


;;; This uses a new faster hyperresolution strategy.
;;; ***** needs a seperate data base for these disjunctins.
;;; ***** to win on subsumption more/(disjunction subsumption).

;;; Declaring a set of assumptions to be an exhaustive xor.
;;; Due to implementation defficiency, this will only work of the xors are all about
;;; the same variable.  Otherwise it will be incomplete.  For example, suppose
;;; the xor is {A,B,C} and you have {D,A} and {D,B,C} the implementation will not
;;; deduce {D}.  This can be fixed rather easily in add-contra-2, but since it runs
;;; so slowly, I haven't bothered to install that patch.

;;; Assumes pairwise contradictions are trapped some other way.  So ior
;;; should be about the same.

;;; Brand new.
(defun nxor (assumptions)
  (choose assumptions '(NXOR)))


;;; Rule H5, very very very slow, could be made more efficient but it is never used.
;;; This version should be very transparent as it directly follows the paper.
(defvar *alphas*)

;;;***** only use if h4 is working.
(defun h5 (node &aux envs *alphas*)
  (setq envs (n-a-envs node))
  (do ((i 2 (1+ i)))
      ((> i 99.))				; *max-or-count*
    (dolist (or (aref *ors* i))
      (h5-recurse (disjunction-vector or) envs (disjunction-nogoods or) *empty-env*)))
  (and *alphas*
    (dolist (alphas *alphas*)
      (format T "~% H5 updates label!?")
      ;; This a little bit of a crock, but saves duplicating running consumers etc.
      (justify-node node (cons 'H5 (env-assumptions alphas)))
    )))

;;; Could flush any label env which picked two assumptions from the disjunction.
;;; Every nogood also selects at most one disjunct.
(defun h5-recurse (vector envs nogoods alphas &aux new-alphas uncons)
  (cond ((env-contradictory alphas))
	((null nogoods)
	 (unless (dolist (e envs) (if (subset-env? e alphas) (return T)))
	   (push alphas *alphas*)))
	(t (dolist (c (cddar nogoods))
	     (if (assumption? c)
		 (unless (or (i-true? c) (i-false? c))
		   (h5-recurse vector envs
			       (cdr nogoods)
			       (cons-env c alphas)))
		 (unless (subsumed-nogood? c)
		   (h5-recurse vector envs
			       (cdr nogoods)
			       (union-env alphas (uncons-env c (caar nogoods)))))))
	   (dolist (e envs)
	     (when (vector-memq (assumption-offset (caar nogoods))
				(assumption-bits (caar nogoods))
				(env-vector e))
	       (setq uncons (uncons-env e (caar nogoods)))
	       (cond ((vector-intersection? vector (env-vector uncons)))
		     ((env-contradictory (setq new-alphas (union-env uncons alphas))))
		     (t (h5-recurse vector envs (cdr nogoods) new-alphas))))))))





;;; Inefficient, but works.
(defun walk-nodes (function)
#+Symbolics
  (declare (sys:downward-funarg function))
  (dolist (node *nodes*) (unless (free-node? node) (funcall function node))))



(defun create-class (datum &optional exclusive oneof data &aux class)
  (setq class (make-class :NAME-SYMBOL 'CLASS
			  :DATUM datum
			  :UNIQUE (incf *class-counter*)
			  :EXCLUSIVE exclusive
			  :ONEOF oneof
			  :ALLOWABLE-DATA data))
  (push class *classes*)
  (if *trace-file* (format *trace-file* "~%C-C1 ~D ~A ~A" *class-counter* exclusive oneof))
  class)

;;;***** can be made more efficient if necessary.
(defun ensure-class-nodes-exist (class)
  (cond ((= (length (class-allowable-data class)) (length (class-nodes class))))
	(t (dolist (v (class-allowable-data class))
	     (find-variable-value class v)))))

;;; A handy hack --- not for code that wants to be efficient.
(defun find-class (datum)
  (dolist (class *classes*) (if (equal (class-datum class) datum) (return class))))

(defun FIND-OR-MAKE-CLASS (datum) (or (find-class datum) (create-class datum)))

;;; If there are assumptions associated with the class, it constructs a disjunction.
;;; **** Should probably check every node of the class is assumed****
(defun close-variable-class (class)
  (unless (class-closed class)
    (if *trace-file* (format *trace-file* "~%CLOSE-CLASS ~D" (class-unique class)))
    (setf (class-closed class) T)
    ;;; ******* This assumes that the class is xor.  Is that right?
    (push class *variables*)
    (if (class-assumptions class)
	(setf (class-or class)
	      (nxor (class-assumptions class))))))


;;; Take care if this is made a delayed function again.
(defun add-class-to-node (node class)
  (when *trace-file*
    (format *trace-file* "~%AC ~D " (class-unique class))
    (trace-node node))
  ;;; If one of the other nodes is true, this node is false.
  ;;; **** This should be cached with the class when one node becomes true ****
  (when (class-exclusive class)
    (dolist (other (class-nodes class))
      (when (i-true? other)
	(contradictory-node node '(EXCLUSION))
	(return-from ADD-CLASS-TO-NODE nil)))
    (when (i-true? node)
      (dolist (other (class-nodes class))
	(contradictory-node other '(EXCLUSION))))
    (when (n-a-envs node)
      (dolist (other (class-nodes class))
	(when (n-a-envs other)
	  (weave-for-false nil (list node other) nil)))))
  (push node (class-nodes class))
  (push class (n-a-classes node))
  (when (class-consumers class)
    (add-class-consumer-to-node (class-consumers class) node)
    (if (i-in? node) (enqueue-node node))))

(defun uses-variable (node variable me)
  (unless (dolist (env (n-a-envs node)) (or (env-assumption? variable env) (return T)))
    (push me (n-a-env-consumers node))
    T))

(defun env-assumption? (variable env)
  (dolist (assumption (env-assumptions env))
    (if (eq variable (assumption-variable assumption)) (return assumption))))

(defun oneof (nodes &optional class unknown-nodes *going-nodes*)
  (dolist (node nodes)
    (cond ((i-false? node))
	  ((i-true? node)
	   (dolist (other nodes)
	     (unless (eq other node)
	       (contradictory-node other '(ONEOF))))
	   (if *going-nodes* (process-changed-nodes))
	   (return-from ONEOF nil))
	  (t (push node unknown-nodes))))
  (cond ((null unknown-nodes) (error "Everything is inconsistent"))
	((null (cdr unknown-nodes))
	 (propagate-true (car unknown-nodes))
	 nil)
	(t (unless class
	     (setq class (create-class (cons 'ONEOF nodes) T T))
	     (dolist (node unknown-nodes)
	       (add-class-to-node node class))
	     (setf (class-closed class) T))
	   (dolist (node unknown-nodes)
	     (when (n-a-envs node)
	       (dolist (other unknown-nodes)
		 (unless (or (eq other node) (i-false? other))
		   (cond ((n-a-neg other)
			  (if *simple-hybrid*
			      (update-node-hybrid (n-a-neg other) (car (n-a-envs node)))
			      (update-node-envs-simple (n-a-neg other) (n-a-envs node))))
			 (t (dolist (e (n-a-envs node))
			      (unions-for-false e (n-a-envs other) '(ONEOF)))))))))
	   (if *clause-mode* (clause '(ONE-OF) nodes nil))
	   (if *going-nodes* (process-changed-nodes))
	   class)))

;;; A trivial constraint language.

;;; Create a variable which must have one of a certain set of values. Returns
;;; the class. Some values want to be call-by-need (implement both***)

;;; This should only be used if you truely expect the nodes to never receive a justification.
(defun create-variable (name values &optional priority &aux class)
  (setq class (create-class name))
  (dolist (value values) (create-xor-node value class))
  (close-variable-class class)
  (if priority
      (dolist (a (class-assumptions class)) (setf (assumption-addb-index a) priority)))
  class)

;;; Everyone of these nodes is instantiatable, but maybe not now.
;(defun create-lazy-variable (name data &aux class) 
;  (setq class (create-class T T))
;  (dolist (datum data)
;    (add-class-to-node (create-node datum) class))
;  class)
;(defun lazy-instantiate (node)
  
(defun create-lazy-variable (name values &aux class assumption)
  (setq class (create-class name T T))
  (dolist (value values)
    ;; Create the raw assumption without doing any work.
    (setq assumption (lazy-basic-make-assumption class value value))
; ***** Useless now right:!?
;    (push 'ADD-XOR-JUST (n-a-env-consumers assumption))
    (push assumption (class-nodes class))
    (push assumption (class-assumptions class)))
  (dolist (assumption (class-assumptions class))
    ;; This essential does add-class-to-node to hook up consumers.
    ;; But there are no consumers, so its easy.
    (setf (assumption-classes assumption) (list class)))
  (setf (class-nodes class) (class-assumptions class))
  (push class *variables*)
  class)

;;; Dumbest approach is create an assumption for every possible value.
;;; The one to use on 9/3/90.
(defun create-assumption-variable (name values &aux class start end unique assumption)
  (setq class (create-class name T T))
  ; We would do this, but its exponentially slow:
  ;(dolist (value values) (make-a-assumption class value nil)
  (setq start (1+ *assumption-counter*))
  (dolist (value values)
    ;; Create the raw assumption without doing any work.
    (setq assumption (basic-make-assumption class value value))
    ;;******* Isn't this obsolete.::::
;    (push 'ADD-XOR-JUST (n-a-env-consumers assumption))
    (push assumption (class-assumptions class)))
  (setq end *assumption-counter*)
  (dolist (assumption (class-assumptions class))
    ;; Now give every assumption an appropriate vector.
    (setq unique (assumption-unique assumption))
    (setf (assumption-binary-vector assumption)
	  (cond ((= unique start) (construct-vector-run (1+ start) (1+ end)))
		((= unique end) (construct-vector-run start end))
		(t (construct-vector-run start unique (1+ unique) (1+ end)))))
    ;; Update the cons-env-cache as we just created the variable.
    (setf (env-cons-env-cache (assumption-env assumption))
	  (ncons (assumption-binary-vector assumption)))
    ;; This essential does add-class-to-node to hook up consumers.
    ;; But there are no consumers, so its easy.
    (setf (assumption-classes assumption) (list class)))
  (setf (class-nodes class) (class-assumptions class))
  (close-variable-class class)
  class)

;;; Like create-assumption-variable, but creates justifications as needed.
(defun new-create-assumption-variable (name values &aux class start end unique assumption)
  (setq class (create-class name))
  ; We would do this, but its exponentially slow:
  ;(dolist (value values) (make-a-assumption class value nil)
  (setq start (1+ *assumption-counter*))
  (dolist (value values)
    ;; Create the raw assumption without doing any work.
    (setq assumption (basic-make-assumption class value value))
;    (push 'ADD-XOR-JUST (n-a-env-consumers assumption))
    (push assumption (class-assumptions class)))
  (setq end *assumption-counter*)
  (dolist (assumption (class-assumptions class))
    ;; Now give every assumption an appropriate vector.
    (setq unique (assumption-unique assumption))
    (setf (assumption-binary-vector assumption)
	  (cond ((= unique start) (construct-vector-run (1+ start) (1+ end)))
		((= unique end) (construct-vector-run start end))
		(t (construct-vector-run start unique (1+ unique) (1+ end)))))
    ;; Update the cons-env-cache as we just created the variable.
    (setf (env-cons-env-cache (assumption-env assumption))
	  (ncons (assumption-binary-vector assumption)))
    ;; This essential does add-class-to-node to hook up consumers.
    ;; But there are no consumers, so its easy.
    (setf (assumption-classes assumption) (list class)))
  (setf (class-nodes class) (class-assumptions class))
  (close-variable-class class)
  (do ((as (class-assumptions class) (cdr as)))
      ((null (cdr as)))
    (dolist (a (cdr as)) (inactive-justify-node *contra-node* (list 'ONE-OF (car as) a))))
  class)

(defun create-variable1 (name values &aux class)
  (setq class (create-class name))
  (dolist (value values) (create-xor-node value class))
  (close-variable-class class)
  (do ((nodes (class-nodes class) (cdr nodes)))
      ((null nodes))
    (dolist (node2 (cdr nodes))
      (justify-node *contra-node* (list 'CREATE-VARIABLE1 (car nodes) node2))))
  class)

;;; Maybe there should be a kind of varible or a flag which instead created consumers
;;; for the contradictions.
(defun good-create-variable (class values &aux node)
  (dolist (node (class-nodes class))
    (unless (memq (n-a-datum node) values)
      (contradictory-node node '(GOOD-CREATE-VARIABLE))))
  (dolist (value values) 
    (unless (find-assumption class value)
      (setq node (find-variable-value class value))
      (justify-node node (list 'CREATE-VARIABLE (make-a-assumption class value)))))
  (close-variable-class class)
  class)

(defun clobber (class datum just) (justify-node (find-variable-value class datum) just))

;;; Utilities needed by ENVISION.

;;; This just adds a value to a variable, but does not create an assumption for it.
;;; However, it invokes the constraint that a variable can have only one value.
;;; There was an obscure bug in this code as a consequence of searching down the
;;; class nodes for an old node.  After all, the old node may not have been
;;; justified, therefore not yet in because add-class-to-node was a delayed
;;; function.  Now add-class-to-node should not have been a delayed function
;;; anyway, so I changed that.  Take care.
;;; UNIQUE VALUE constraints are automatically ensured by class membership.
(defun find-variable-value (class datum &aux node)
  (cond ((dolist (node (class-nodes class))
	   (if (eq (n-a-datum node) datum) (return node))))
	(t (setq node (create-node datum))
	   (add-class-to-node node class)
	   node)))

;;; **** Maybe this should be redone with classes.
;(defun exclusive (nodes conditional)
;  (do ((nodes1 nodes (cdr nodes1)))
;      ((null nodes1))
;    (do ((nodes2 (cdr nodes1) (cdr nodes2)))
;	((null nodes2))
;      (justify-node *contra-node*
;		    (list 'UNIQUE-VALUE (car nodes1) (car nodes2) conditional)))))

;;; **** Maybe this should be redone with classes.
(defun exclusive (nodes conditional)
  (do ((sub-nodes nodes (cdr sub-nodes)))
      ((null sub-nodes))
    (dolist (node2 (cdr sub-nodes))
      (justify-node *contra-node*
		    `(conditionally-exclusive ,conditional ,(car sub-nodes) ,node2)))))
 
;;; Returns the first assumption env which is a member of the class.  Like all
;;; the old env-assume?/choice?
(defun env-assume? (class env)
  (dolist (a (env-assumptions env))
    (if (memq class (assumption-classes a)) (return a))))

;;; Due to a crock of history.
(defun env-choice? (class env)
  (dolist (a (env-assumptions env))
    (if (eq class (assumption-variable a)) (return a))))

;;; Returns the one node of the class which has a node in the class.
(defun env-lookup (env class)
  (dolist (node (class-nodes class))
    (if (dolist (nenv (n-a-envs node)) (if (subset-env? nenv env) (return T)))
	(return node))))


;;; A correct assumption-gc.
;;; No it isn't.						
(defun assumption-gc (&aux old new good dont true)
  (setq new 0 old 0 good 0 dont 0 true 0)
  (dolist (a *assumptions*)
    (cond ((i-true? a) (incf true))
	  ((eq (assumption-gc-status a) 'DONT) (incf dont))
	  (t)
	  ((null (assumption-envs a)) (incf old))
	  ((or (env-contradictory (car (assumption-envs a)))
	       (dolist (c (assumption-consequents a))
		 (if (n-a-contradictory (cnsqnt-result c)) (return T))
		 (if (i-true? (cnsqnt-result c)) (return T))))
	   (break "Debugging check ---- continue without damage")
	   (setf (assumption-envs a) nil (assumption-contradictory a) 'GC)
	   (incf new))
	  (t (incf good))))
  (format T
	  "~% ~D locked, ~D true, ~D good, ~D gc'ed previously, ~D gc'ed now."
	  dont true good old new))

(defun fast-active-assumptions (&aux assumptions)
  (assumption-gc)
  (dolist (a *assumptions*)
    (and (not (i-true? a))
	 (not (i-false? a))
	 (assumption-envs a)
	 (if (or (env-nodes (car (assumption-envs a)))
		 (dolist (c (assumption-consequents a))
		   (if (dolist (e (n-a-envs (car c)))
			 ;;**** bit vectors???
			 (if (memq a (env-assumptions e)) (return T)))
		       (return T))))
	     (push a assumptions))))
  assumptions)

;;; This returns a list of those assumptions that actually play some role.  Used in
;;; interpretation construction.  This is usually, but not always equivalent to
;;; GC'ing.  The difference occurs only if assumptions co-occur with other
;;; nodes in justifications.  
;;; This also assumes assumptions aren't justified.

;;; This ignores all assumptions that cannot concievably usefuly be added to the base.
(defun active-assumptions (base &aux assumptions extend)
  (assumption-gc)
  (dolist (a *assumptions*)
    (cond ((i-true? a))
	  ((i-false? a))
	  ((env-contradictory (setq extend (cons-env base a))))
	  ((null (dolist (env (assumption-envs a))
		   ;;**** makes no sense at all env is not even referenced.
		   (if (successfull-union? base extend) (return T)))))
;	  ((dolist (node (env-nodes (assumption-env a)))
;	     (if (consistent-in? node extend) (return T)))
;	   (push a assumptions))
	  ((dolist (c (assumption-consequents a))
	     (if (dolist (e (n-a-envs (car c)))
		   (if (and (memq a (env-assumptions e)) (successfull-union? e extend))
		       (return T)))
		 (return T)))
	   (push a assumptions))))
  (format T "~% ~D assumptions, ~D active" (length *assumptions*) (length assumptions))
  assumptions)

;;; This looks for all environments which contain a false or true assumption
;;; and just axes them.  'SUBSUMED environments could also
(defun env-gc ()
  nil
  )