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

(in-package 'tms)

"(c) Copyright 1986, 1987, 1988, 1989 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."

;;; This controls whether one environment is OK.
(defvar *strong-focussing* T)

;;; This file contains all the functions used to do label propagation.

;;; For many examples it pays incredibly to find to size 1 and size 2 contradictions first.
;;; In fact, more general the right order is for each increaseing n find the contradictions
;;; of size n, then the environments of size n, etc.  But I suspect that is all simply 
;;; to much book-keeping to be worth it.
(defun update-node1 (node new-envs complete-envs 
		     &aux start-time start-count contra-count
		     start-contra-counter)
  (when *update-trace*
    (setq start-time (get-internal-run-time)
	  start-count *env-counter*
	  contra-count 0
	  start-contra-counter *contra-counter*))
  (cond (*simple-hybrid* (update-node-hybrid node (car new-envs)))
	(*c012*
	 (update-node-c012 node new-envs nil)
	 (setq complete-envs (sanitize-envs complete-envs))
	 (if (setq new-envs (sanitize-envs new-envs))
	     (update-node node new-envs complete-envs)))
	(t (update-node node new-envs complete-envs)))

  (when *update-trace*
    (format T "~% Update time is:~D seconds" (time-taken start-time))
    (format T "~% ~D new minimal nogoods" (- *contra-counter* start-contra-counter))
    (if *going-nodes* (format T "~% ~D going nodes" (length *going-nodes*)))
    (format T "~% ~D new envs created" (- *env-counter* start-count))
    (do ((i (1+ start-count) (1+ i)))
	((> i *env-counter*))
      (if (e i) (incf contra-count)))
    (format T "~% Of which ~D are consistent." contra-count)))



;;; This needs to incrementally sanitize****Like above.********
;;;; THIS IS BUGGY I THINK COMPARE TO BELOW hybrid vrsion.
(defun propagate-clauses (node new-envs
			  &aux positives negatives flag open)
  (dolist (clause (n-a-nclauses node))
    ;; Make sure the clause is unit-open somewhere --- a big assumption.*****
    (setq negatives (first clause)
	  positives (second clause))
    ;; Check if the clause is active---perhaps this short be part of the clause
    ;; data structure.******

    ;; Test this check later.

    (setq open nil)
          
    (if positives (error "NOT IMPLEMENTED"))

    ;; If clause is satisfied, or has more than one open literal it is useless.
    (cond ;; Check whether the clause is useless right now.
	  ((or (dolist (n negatives)
		 (cond ((i-in? n))
		       ((i-false? n) (return T))
		       (open (return T))
		       (t (setq open n))))
	       (dolist (p positives)
		 (cond ((i-true? p) (return T))
		       ;;;???
		       (open (return T))
		       (t (setq open p))
		       ))))
	  
	  ((cdr positives))
	  ;;**how does open affect this?
	  (positives (update-node-envs (car positives) negatives node new-envs clause))
	  ;; If there is only one open, and everything is negative, its easy:
	  (open (update-node-envs (n-a-neg open) (remove open negatives) node new-envs clause))
	  (t (setq flag nil)
	     (dolist (n negatives)
	       (unless (or (eq n node) (i-true? n))
		 (if (n-a-neg n)
		     (update-node-envs (n-a-neg n) (remove n negatives) node new-envs clause)
		     ;;**** hybrid case this can be fixed moochly.***
;		     (error "~A has no negation" n)
		     (setq flag T))))
	     (if flag (update-node-envs *contra-node* negatives node new-envs clause))))))

;;; This now assumes all the labels are correct.  This positive and negative stuff
;;; sucks.  I think it will be cleaner in the future only to have negatives
;;; allowed in c aluse.



;;; This new version works with the *label-q*
;;; This assumes there are no positives.
;;; Don't bother queuing clauses whose consequent is currently known anyway.
(defun propagate-clauses-hybrid (node new-env &aux negatives open)
  ;; Special case optimization.
  (when *ltms*
    (dolist (clause (n-a-nclauses node))
      (cond ((= (clause-count clause) 1)
	     (dolist (n (clause-negatives clause))
	       (unless (hybrid-label n) (setq open n) (return nil)))
	     (when (and (n-a-neg open)
			(null (hybrid-label (n-a-neg open))))
	       (setf (clause-consequent clause) (n-a-neg open))
	       (queue-clause clause)))
	    ((> (clause-count clause) 1))
	    (t (setq *contradiction* (cons clause nil)))))
    (return-from propagate-clauses-hybrid nil))


  ;; There used to be a note here that this handled contradictions incorrectly
  ;; but I don't understand that.
  (dolist (clause (n-a-nclauses node))
    (cond ((null *ltms*)
	   (setq negatives (clause-negatives clause) open nil)
	   ;; If clause is satisfied, or has more than one open literal it is useless.
	   (cond ;; Check whether the clause is useless right now.
	     ((or (dolist (n negatives)
		    (cond ((i-in? n))
			  ((i-false? n) (return T))
			  (open (return T))
			  (t ;; If an assumption is not in focus, ignore this.  When the
			   ;; assumption ever comes in, it will be retriggered.
			   ;; Concievably we can have a node representing the negation
			   ;; of each node.
			   (if (tms::assumption? n) (return T))
			   (setq open n))))))
	     ;; If there is only one open, and everything is negative, its easy:
	     (open (if (n-a-neg open)
		       ;;;**** optimization to be introduced better.
		       ;;; ***** Perhaps keep a count of TRUE??
		       (progn (setf (clause-consequent clause) (n-a-neg open))
			      (queue-clause clause))
		       ;;***** THIS IS USUALL A G(H) which should be a cons-for-false.
		       ;;***** AND COULD BE OPTIMIZED ANYWAY.  THIS NEVER GETS CALLED ?
		       (weave-for-false (list new-env) negatives node)))
	     (t ;; Do this right away because this means focus is inconsistent.
	      (weave-for-false (list new-env) negatives node)
	      ;; Remember, this entire operation must be atomic.
	      (unless (env-contradictory new-env)
		(setf (clause-consequent clause) nil)
		(queue-clause clause))
	      )))
	  ((> (clause-count clause) 1))
	  ((= (clause-count clause) 1) (queue-clause clause))
	  (*rltms* (setq *contradiction* (list clause nil)))
	  (t (weave-for-false (list new-env) (clause-negatives clause) node)
	     (unless (env-contradictory new-env) (queue-clause clause))))))

;;; A consequent looks like (consequent-node . justification)
;;; New environments have been discovered for the antecedent node.
;;; *** why does this look at justifications only once. 

;;; This returns the possibly side-effected new-envs.

;;; ***** update-node1 => update-node here for efficiency******
(defun update-node-envs (node antecedent-nodes antecedent-node new-envs reason
			 &aux justifications)
  (setq justifications (n-a-justifications node))
  (cond ((n-a-contradictory node)
	 (unless (cdr antecedent-nodes)
	   (error "Contradiction should have been detected earlier"))
	 (weave-for-false new-envs antecedent-nodes antecedent-node reason)
	 new-envs)
	((i-true? node) new-envs)
	
	;Used to do this in above condition.
	;(contradictory-envs new-envs (list 'BASE 'LABEL-FOR-FALSE consequent)))
	
	;; If there are more than one antecedent nodes in this justification, just
        ;; recompute everything.  (Should be optimized more****.)
	((cdr antecedent-nodes)
	 (if *trace* (format T "~% Updating envs of ~A because of new antecedent envs ~A"
			     (node-string node) new-envs))
	 ;; This happens so often that its worth a pre-check.
	 (dolist (n antecedent-nodes)
	   (if (i-out? n) (return-from UPDATE-NODE-ENVS new-envs)))
	 
	 ;; This depends crucially on general-weave returning FRESH list structure
	 ;; **always**.  Because new-envs gets side-effected in this algorithm.
	 (multiple-value-bind (known-envs new-envs)
	     (general-weave (n-a-envs node) new-envs antecedent-nodes antecedent-node)
;	   (if new-envs (format T "+") (format T "-"))
	   (when new-envs
	     (update-node1 node new-envs known-envs)))
	 new-envs)
	;; If there is more than one justification, the envs of the consequent could
	;; already be updated.  Also, the new-envs could eliminate some environments
	;; of the label.  If the node is a member of some classes or has a negation
	;; its label can be affected by other mechanisms.
	((or (cdr justifications) (n-a-classes node) (n-a-neg node) (n-a-pclauses node))
	 (update-node-envs-simple node new-envs)
	 new-envs)
	;; If there is only one justification, and it has only one antecedent node, just
        ;; copy the update forward with doing any work.  But remember each node had
	;; better have a unique list structure for its label.  This is save ONLY if this
	;; this justification is the **only** way this node can be affected.
	(t (update-node1 node new-envs (fcopylist (n-a-envs antecedent-node))))))

;;; And new-envs to node, do all subsumptions.  This duplicates some of the work
;;; of change-node-envs.  Is this efficiency hack really worth it?
(defun update-node-envs-simple (node new-envs &aux node-envs new-new-envs)
  ;; This fcopylist is necessary, because envs gets rplaca'd.
  (setq node-envs (fcopylist (n-a-envs node)))
  (dolist (new-env new-envs)
    (unless (or (env-contradictory new-env)
		(do ((known-envs node-envs (cdr known-envs)))
		    ((null known-envs) nil)
		  (if (car known-envs)
		      (selectq (compare-env (car known-envs) new-env)
			(SUBSET21 (rplaca known-envs nil))
			((EQUAL SUBSET12) (return T))))))
      (push new-env new-new-envs)))
  (when new-new-envs
    (setq node-envs (fdelqa nil node-envs))
;    (setf (n-a-envs node) node-envs)
    ;; Really should do an fcopylist here to get a cdr-coded list.
    (update-node node new-new-envs (append new-new-envs node-envs))))

;;; Could be a macro if slow.
;;; Note that this should never be called if the node is an
;;; ****** the full test on assumption-nogoods hasn't perculated to c012.
;;; This assumes complete-envs is fresh data structure.
;;; Note this is the only place change-node-envs is called so change-node-envs
;;; should rely on new-envs too.
(defun update-node (node new-envs complete-envs &aux not-first consequent contra-counter neg)
  ;; A primitive focussing mechanism, could be much more efficient.  Could recycle
  ;; conses ****.
  (when *foci*
    (multiple-value-setq (new-envs complete-envs)
      (update-node-filter node new-envs complete-envs))
    (unless new-envs (return-from UPDATE-NODE nil)))
  (when (assumption? node)
    (multiple-value-setq (new-envs complete-envs)
      (update-assumption node new-envs complete-envs))
    (unless new-envs (return-from UPDATE-NODE nil)))
  (change-node-envs node complete-envs)
;;; Remember we are running depth first, so things can change right under us.  So
;;; for every consequent check that the new-envs set is really still new and not
;;; contradictory.  Note that update-node-consequents will clobber new-envs.
;;; New-envs better be new, or else this will infinite loop.  This algorithm will
;;; side-effectively remove any inconsistent environments on new-envs.  It returns
;;; the changed new-envs also.

;;; This code is based on the hypothesis that unless resolution happens underneath,
;;; a node-envs can never change underneath this algorithm.  This is clearly false
;;; if *h45* is on and resolutions are happening underneath.  The theorem holds because
;;; by necessity new-envs in recursive calls to update-node-consequents must grow
;;; monitonically.  It might be worth maintaining a stack of nodes whose environment
;;; we are updating and simply ignore circular updates.

  (if (n-a-contradictory node) (return-from UPDATE-NODE new-envs))

;;; This can be made much more efficient here because if the antecedent environments***
;;; don't change, we don't need to go breadth-first.******

  ;; In the new regime, justifications aren't constructed for negations, this code
  ;; ensures that negations are properly processed.
  (cond ((null (setq neg (n-a-neg node))))
	((null (n-a-envs neg)))
	(T (setq not-first T contra-counter *contra-counter*)
	   (dolist (e new-envs)
	     (unions-for-false e (n-a-envs neg)
			       (if *explain-flag*
				   `(CONSENSUS ,node ,neg ,e ,(n-a-envs neg))
				   '(CONSENSUS))))))
  ;; In the new regime, justifications aren't contructed for unique-value classes.
  ;; ***** This only assumes an exclusion class.
  (dolist (class (n-a-classes node))
    (when (class-exclusive class)
      (dolist (other (class-nodes class))
	(unless (or (eq other node) (i-false? other))
	  (unless not-first (setq not-first T contra-counter *contra-counter*))
	  (cond ((n-a-neg other)
		 (update-node-envs-simple (n-a-neg other) new-envs))
		(t (dolist (e new-envs)
		     (unless (env-contradictory e)
		       ;; Flush new-envs that become inconsistent.
		       (unions-for-false e (n-a-envs other)
					 `(EXCLUSION ,node ,other))))))))))
  ;; Look at the clauses in which it appears with opposite sign.
  (when (n-a-nclauses node)
    ;; Forget this optimization.
    (setq not-first T contra-counter *contra-counter*)
    (propagate-clauses node new-envs))
  ;; Process conventional justifications.
  (when (setq consequent (n-a-consequents node))
    (if *trace* (format T "~% Adjusting consequents of node ~S because of new found envs: ~A"
			node new-envs))
    (dolist (c consequent)
      (unless (i-true? (just-consequent c))
	(cond (not-first
	       ;; First check to see whether any of the new-envs became inconsistent.
	       ;; But only make this check if we have to.  
	       (unless (= contra-counter *contra-counter*)
		 (do ((new-env new-envs (cdr new-env)))
		     ((null new-env))
		   (when (env-contradictory (car new-env))
		     (rplaca new-env nil)))
		 (unless (setq new-envs (fdelqa nil new-envs))
		   (return-from UPDATE-NODE nil)))
	       (if *h45*
		   (setq new-envs (or (cleanup-for-h45 node new-envs)
				      (return-from UPDATE-NODE nil)))))
	      (t (setq not-first T)))
	;; *contra-counter* will increment if any envs become marked nogood.
	(setq contra-counter *contra-counter*)
	(unless (setq new-envs
		      (update-node-envs (just-consequent c) (just-antecedents c)
					node new-envs c))
	  (return-from UPDATE-NODE nil))))
    (if *trace* (format T "~% Finishing consequents of node ~A" (node-string node))))
  new-envs
  )

;;; Keep delayed minimal???? ***** is it worth it?  Probably not.  But think
;;; about it some day.
;;; This is only set up from removing new-envs, not old ones.****
;;; This is an experimental version which may become permanent which keeps the
;;; blocked label minimal (for strong focussing so far).

;;; This is only set up from removing new-envs, not old ones.****
(defun update-node-filter (node new-envs complete-envs
			   &aux update change delayed shortest keep)
  (if *simple-hybrid* (error "Incompletely implemented"))

  (setq delayed (n-a-blocked node))
  ;; EMPTY means nothing should happen.
  (when (eq *foci* :EMPTY)
    (setq delayed (append new-envs delayed))
    (dolist (new-env new-envs) (push node (env-nodes new-env)))
    (setf (n-a-blocked node) delayed)
    (return-from UPDATE-NODE-FILTER nil))

  ;; Strong focussing means you let only a shortest environment through for each foci.
  ;; This focussing doesn't remove longer labels (yet******************).
  ;; This code does not update the blocked label to be minimal *****
  (cond (*strong-focussing*
	 ;; For each foci find one label environment which is shortest for each foci.
	 (dolist (f *foci*)
	   (setq shortest nil)
	   (dolist (c complete-envs)
	     (cond ((not (subset-env? c f)))
		   ((null shortest) (setq shortest c))
		   ((< (env-count c) (env-count shortest)) (setq shortest c))
		   ((not (= (env-count c) (env-count shortest))))

		   ;; Prefer old label.
		   ((memq c new-envs))
;		   ((not (memq c new-envs)) (setq shortest nil))
		   ((memq c keep) (setq shortest nil))
		   (t (setq shortest c))))
	   (if shortest (push shortest keep)))

	 (if keep (setq update T))
    
		 ;;***** FLUSH from env-nodes the spurious reference.
	 

	 ;; Now make sure we copy over only the one's we want.
	 (do ((new new-envs (cdr new)))
	     ((null new))
	   (unless (memq (car new) keep)
	     (setq change T)
	     (push (car new) delayed)
	     (push node (env-nodes (car new)))
	     (rplaca (memq (car new) complete-envs) nil)
	     (rplaca new nil)))
	 )
	(t ;;;**** buggy doesn't update env-nodes.
	   (do ((new new-envs (cdr new)))
	       ((null new))
	     (unless (dolist (f *foci*)
		       (when (subset-env? (car new) f)
			 (setq update T)
			 (return T)))
	       (setq change T)
	       (push (car new) delayed)			;****** cons could be recycled.
	       (rplaca (memq (car new) complete-envs) nil)
	       (rplaca new nil)))))
  (when change

    (if (memq (car delayed) (cdr delayed)) (error "Horrible"))

    (print node)
    (setf (n-a-blocked node) delayed)
    (check-node node))
  (unless update (return-from UPDATE-NODE-FILTER nil))
  (unless change (return-from UPDATE-NODE-FILTER (values new-envs complete-envs)))
  (values (fdelqa nil new-envs) (fdelqa nil complete-envs)))

;;; Tell the ATMS that foci changed.
;;; This can be made much more efficient if necessary.
;;; This **** does not save conses.
;;; Supersets of old foci are not new foci.

(defvar *foci-complete* nil)			; This per-ATMS flag indicates whether
						; the focussed labels are correct.

(defun change-foci (new-foci &optional (update T)
		    &aux really-new-foci start-time
		    *going-nodes* not-subset old-focus)
  ;;;***** could be more general.
  (if (equal new-foci *foci*) (return-from change-foci nil))

;  The following is needed in the old change-foci-simple-hybrid.
;  (setq *current-focus* (car new-foci))
  (unless *current-focus* (setq *current-focus* *empty-env*))

  (when *trace-file*
    (dolist (e new-foci) (trace-env e))
    (format *trace-file* "~%CF ")
    (format *trace-file* "(")
    (let ((previous nil))
      (dolist (e new-foci)
	(zf previous
	    (format *trace-file* " ~D" (env-unique e))
	    (setq previous T)
	    (format *trace-file* "~D" (env-unique e)))))
    (format *trace-file* ")"))

  (if *report-focussing* (setq start-time (get-internal-run-time)))
  (if (or (eq *foci* :EMPTY) (null *foci*))
      (setq really-new-foci new-foci)
      (dolist (f new-foci) (unless (memq f *foci*) (push f really-new-foci))))

  ;; If the new is a subset of the old, then this can be optimized later.
  (if (or (not *foci-complete*) (eq *foci* :EMPTY))
      (setq not-subset T)
      (dolist (n really-new-foci)
	(unless (dolist (o *foci*)
		  (and o (subset-env? n o) (return T)))
	  (setq not-subset T)
	  (return nil))))

  ;; Signal that the foci are not correct for new *foci* yet.
  (setq old-focus (if (eq *foci* :EMPTY) :EMPTY (car *foci*))
	*foci-complete* nil
	*foci* new-foci)
  (if (cdr *foci*) (error "Simple hybrid requires one foci"))
  (change-foci-simple-hybrid update (car really-new-foci) old-focus)
  
  ;;;****** Error check.
;  (dolist (a *assumptions*)
;    (and (assumption-in-focus a)
;	 (not (vector-member a (env-vector *good-foci*)))
;	 (progn (format T "~% Assumption ~A is labeled in focus, but not in *good-foci*: ~A"
;			a *good-foci*)
;	   (error "Illegal state"))))


  ;; This can be much more optimized.
  ;; Note that a node is put in the agenda under its shortest env, not its shortest foci env.
  (if not-subset (cleanup-unfocussed-nodes))

  ;;; ***** Could be much more efficient.****
  ;;; remove everything which is not in current foci.

  ;;; DO this only if there are new foci environments.
  ;;; ****** very inefficient.

  ;;;***** THIS SHOULD BE INVOKED ONLY IF THERE ARE OLD foci.

  ;;; ***** When *foci* becomes empty.


;  (if (env-contradictory (car *foci*)) (error "UH"))

  ;; Just to maintain consistency, even if the foci has become empty its probably
  ;; still important to update the queue.  
  (if *going-nodes* (process-changed-nodes))

  (setq *foci-complete* T)

  (if *report-focussing*
      (format T "~% Refocus time is:~D seconds"
	      (time-taken start-time))))


(defun change-foci-general (update really-new-foci)
  ;; First make sure there are no spurious environments in nodes to complicate things.
  ;; This removes all environments not in foci.
  ;;**** probably should do a pass through all the nodes.
  (when (and *strong-focussing* (neq *foci* :EMPTY))
    (cleanup-nodes-general *assumptions*)
    (cleanup-nodes-general *nodes*))

  (when really-new-foci

    ;;; If foci is inconsistent by now, punt this*****

    (if update (update-atms))))

(defvar *good-foci* nil)

(defvar *adds* nil)

;;;****** delete third argum
(defun change-foci-simple-hybrid-old (update new-focus ignore &aux
				  adds retracts old-good-foci node env)

  (if (env-contradictory new-focus)
      (error "Called change-foci-simple-hybrid with contradictory env"))

  (setq old-good-foci *good-foci*
	*good-foci* nil)

  (cond (old-good-foci
	 (multiple-value-setq (retracts adds) (compare-foci old-good-foci new-focus))
;	 (format T "~% Adds: ~A, Retracts: ~A" adds retracts)
	 ;; I once thought it might be clever to not do retract-assumptions and let
	 ;; these be caught lazily.  That doesn't work because it might be the case
	 ;; that the removal of the supporting environment might cause another supporting
	 ;; environment to the for which has not been propagated.

	 ;; Before doing anything, look ahead to see if loss is emminent and don't bother
	 ;; doing anything at all.
	 ;; This is very incomplete right now, but it helps a lot. Extend***

	 (dolist (a adds)
	   (when (setq node (assumption-node a))
	     ;; **presumes the class is oneof.

	     (dolist (n (tms::class-nodes (car (n-a-classes node))))


	       (when (setq env (true-in-blocked? n new-focus))
		 ;;***** In many cases the previous focus became inconsistent, and therefore
		 ;;***** this will fail for the same reason.  But we don't check that right yet
		 (cond ((eq node n)
;			(error "LOOK")
				    
				    (return nil))
		       (t (cons-for-false env a 'EXCLUSIVE)
			  (setq *good-foci* old-good-foci)
;			  (format T "~% Avoiding the shift")
			  (return-from CHANGE-FOCI-SIMPLE-HYBRID-old nil)))))))

	 ;; If look ahead doesn't tell us what's going on... try this.

	 (dolist (r retracts) (retract-assumption r))

	 (if (env-contradictory new-focus)
	     (error "Focus became inconsistent after retraction"))



	 (do ((a adds (cdr a)))
	     ((null a))
	   (enable-assumption (car a))

	   (when (env-contradictory new-focus)
	     ;; Foci is correct only up til this.
	     (setq *good-foci* new-focus)
	     (dolist (n (cdr a))
	       ;; I'm not convinced that this uncons-env should not some times absolutely
	       ;; fail if correct because *foci* is larger.*********
	       (setq *good-foci* (uncons-env *good-foci* n)))
	     
	     (return-from change-foci-simple-hybrid-old nil)))

	 (setq *good-foci* new-focus)

	 (do () ((null (setq node (pop *changed-hybrid-nodes*))))
	   (cleanup-single-node-simple-hybrid node)
	   (if (env-contradictory new-focus) (return-from change-foci-simple-hybrid-old nil)))

	 (update-atms)

	 (return-from change-foci-simple-hybrid-old nil)

	 ;;;***** this is here for diagnostic purposes.
;	 (dolist (n *nodes*) (hybrid-label n))

;; Next trhee are debugging.
;	 (if update (update-atms))
;	 (check-hybrid-labels-1 *nodes* 'A)
;	 (check-hybrid-labels-1 *assumptions* 'A)

	 )
	(t (format T "~% Forced to compute from scratch because old label set is incomplete ~A"
		   )
	   (change-foci-simple-hybrid-1 new-focus *assumptions*)
	   (change-foci-simple-hybrid-1 new-focus *nodes*)
	   ))
  (unless (env-contradictory new-focus)
    (setq *good-foci* new-focus)
    (if update (update-atms)))
  )

;;; This assumption has neither been completely integrated or retracted.
;;; ****** Can't there ever be more than one incomplete-assumptions.  If so fix this.

(defvar *change-foci-trace* nil)

;;; This is under a lot of construction.
(defun change-foci-simple-hybrid (update new-focus ignore &aux
				  adds retracts old-good-foci node env)

  (and *debug* (env-contradictory new-focus)
      (error "Called change-foci-simple-hybrid with contradictory env"))

  (setq old-good-foci *good-foci*
	*good-foci* nil)

  (cond (old-good-foci
	 (multiple-value-setq (retracts adds) (compare-foci old-good-foci new-focus))
	 (if *change-foci-trace* (format T "~% Adds: ~A, Retracts: ~A" adds retracts))
	 ;; I once thought it might be clever to not do retract-assumptions and let
	 ;; these be caught lazily.  That doesn't work because it might be the case
	 ;; that the removal of the supporting environment might cause another supporting
	 ;; environment to the for which has not been propagated.

	 ;; Before doing anything, look ahead to see if loss is emminent and don't bother
	 ;; doing anything at all.
	 ;; This is very incomplete right now, but it helps a lot. Extend***

	 (dolist (a adds) (setf (assumption-in-focus a) T))
	 (dolist (r retracts) (setf (assumption-in-focus r) nil))

	 (dolist (a adds)
	   (when (setq node (assumption-node a))
	     ;; **presumes the class is oneof.

;	     (unless (n-a-classes node) (error "Can't happen"))

	     (dolist (n (tms::class-nodes (car (n-a-classes node))))

	       (when (setq env (true-in-focus? n new-focus))
		 ;;***** In many cases the previous focus became inconsistent, and therefore
		 ;;***** this will fail for the same reason.  But we don't check that right yet
		 (cond ((eq node n)
;			(error "LOOK")
				    
				    (return nil))
		       (t (cons-for-false env a 'EXCLUSIVE)
			  (setq *good-foci* old-good-foci)
			  (cleanup-adds-subtracts adds subtracts)
			  (if *change-foci-trace* (format T "~% Avoiding the shift"))
			  (return-from CHANGE-FOCI-SIMPLE-HYBRID nil)))))))

	 ;; If look ahead doesn't tell us what's going on... try this.
	 
	 ;; In the current strategy, retracting an assumption can make the focus
	 ;; inconsistent because the retraction may install the best environment
	 ;; for the ultimate focus.

	 ;; All the incomplete assumptions, which are not added back now, should be
	 ;; retracted now.  If we perchance encounter a contradiction, we don't change
	 ;; the current good focus.
	 (when (and *incomplete-assumption*
		    (not (assumption-in-focus *incomplete-assumption*)))
	   (retract-assumption *incomplete-assumption*)
	   (when (env-contradictory new-focus)
	     (setq *good-foci* old-good-foci)
	     (cleanup-adds-subtracts adds subtracts)
	     (return-from change-foci-simple-hybrid nil))
	   (setq *incomplete-assumption* nil))

	 (dolist (r retracts)
	   (retract-assumption r)
	   ;; I'm not sure this is right, but everything is correct up to the current
	   ;; retraction.
	   ;; ***** there is something rather wrong here because the retract/add
	   ;; ***** has the bug that it doesn't complete if there is a contradiction
	   ;; ***** and those don't really get fixed up.
	   (when (env-contradictory new-focus)
	     (setq *incomplete-assumption* r
		   *good-foci* old-good-foci)
	     ;;;****** THIS UNCONS-ENV might sometimes not work I think.

	     ;; Get rid of all the adds.
	     (dolist (a adds) (setf (assumption-in-focus a) nil))

	     (do ((retracts retracts (cdr retracts)))
		 ((null retracts))
	       (setq *good-foci* (uncons-env *good-foci* (car retracts)))
	       (when (eq (car retracts) r)
		 (dolist (r retracts) (setf (assumption-in-focus r) T))
		 (return-from change-foci-simple-hybrid nil)))))

	 ;; We want to make sure the *incomplete-assumption* is the first add, so
	 ;; we won't suffer from the problem of two *incomplete-assumption*.
	 (when *incomplete-assumption*
	   (unless (eq (car adds) *incomplete-assumption*)
	     ;; **** could be more optimal.
	     (setq adds (cons *incomplete-assumption*
			      (fdelq1 *incomplete-assumption* adds))))
	   (setq *incomplete-assumption* nil))

	 (do ((a adds (cdr a)))
	     ((null a))
	   (update-atms)

	   (unless (env-contradictory new-focus)

	 (dolist (a a)
	   (when (setq node (assumption-node a))
	     ;; **presumes the class is oneof.

	     (dolist (n (tms::class-nodes (car (n-a-classes node))))


	       (when (setq env (true-in-blocked? n new-focus))
		 ;;***** In many cases the previous focus became inconsistent, and therefore
		 ;;***** this will fail for the same reason.  But we don't check that right yet
		 (cond ((eq node n)
;			(error "LOOK")
				    
				    (return nil))
		       (t (cons-for-false env a 'EXCLUSIVE)
			  (setq *good-foci* old-good-foci)
			  (cleanup-adds-subtracts adds subtracts)
			  (if *change-foci-trace* (format T "~% Really avoiding the shift"))
			  (return-from CHANGE-FOCI-SIMPLE-HYBRID nil)))))))

	   (enable-assumption (car a)))

	   ;;; This is a little bit kludgey, we may be able to make the next more efficient.

	   (when (env-contradictory new-focus)
	     (setq *incomplete-assumption* (car a))
	     ;; Foci is correct only up til this.
	     ;; ****
	     (setq *good-foci* new-focus)
	     (dolist (n (cdr a))
	       ;; I'm not convinced that this uncons-env should not some times absolutely
	       ;; fail if correct because *foci* is larger.*********
	       ;;; ****** THIS IS WIERD, THIS ASSUMPTION BOTH ISN'T COMPLETELY INSTALLED
	       ;;; ****** NOR IS IT DE-INSTALLED.

	       (setf (assumption-in-focus n) nil)
	       (setq *good-foci* (uncons-env *good-foci* n)))
	     
	     (return-from change-foci-simple-hybrid nil)))

	 (setq *good-foci* new-focus)

	 (do () ((null (setq node (pop *changed-hybrid-nodes*))))
	   (cleanup-single-node-simple-hybrid node)
	   (if (env-contradictory new-focus) (return-from change-foci-simple-hybrid nil)))

	 (update-atms)

	 ;; Note the focus could be inconsistent now.

	 (return-from change-foci-simple-hybrid nil)

	 ;;;***** this is here for diagnostic purposes.
;	 (dolist (n *nodes*) (hybrid-label n))

;; Next trhee are debugging.
;	 (if update (update-atms))
;	 (check-hybrid-labels-1 *nodes* 'A)
;	 (check-hybrid-labels-1 *assumptions* 'A)

	 )
	(t ;;******** THIS SHOULD BE AN ALMOST IMPOSSIBLE EVENT.
	   (dolist (a *assumptions*) (setf (assumption-in-focus a) nil))
	   (dolist (a (env-assumptions new-focus)) (setf (assumption-in-focus a) T))

	   (change-foci-simple-hybrid-1 new-focus *assumptions*)
	   (change-foci-simple-hybrid-1 new-focus *nodes*)
	   ))
  (unless (env-contradictory new-focus)
    (setq *good-foci* new-focus)
    (if update (update-atms)))
  )

;;; This is equivalent to change-foci-simple-hybrid consing the assumption.
;;; Returns T if the assumption add succeeded.
(defun enable-current-assumption (a &aux new-focus env node *going-nodes*)
  (setq new-focus (cons-env *good-foci* a))
  (unless *sltms*
    (change-foci-simple-hybrid T new-focus 'IGNORE)
    (return-from enable-current-assumption nil))
  (if *change-foci-trace* (format T "~% Add: ~A" a))
  (and (and (setq node (assumption-node a))
	    (n-a-classes node))
       (dolist (n (tms::class-nodes (car (n-a-classes node))))
	 (when (setq env (true-in-blocked? n new-focus))
	   (cond ((eq node n) (return nil))
		 (t (cons-for-false env a 'EXCLUSIVE)
		    (return-from ENABLE-CURRENT-ASSUMPTION nil))))))
  (setf (assumption-in-focus a) T)
  (when (and *incomplete-assumption* (not (assumption-in-focus *incomplete-assumption*)))
    (set-hybrid-label *incomplete-assumption* nil 'ENABLE-CURRENT-ASSUMPTION)
    (setq *incomplete-assumption* nil))
  (when *incomplete-assumption* (error "Not completely implemented"))
  (enable-assumption a)
  (when (env-contradictory new-focus)
    (setq *incomplete-assumption* a)
    (setf (assumption-in-focus a) nil)
    (return-from enable-current-assumption nil))
  (setq *good-foci* new-focus)
  (update-atms)
  (if (env-contradictory new-focus) (return-from enable-current-assumption nil))
  (setq *foci* (list new-focus))
  (if *going-nodes* (process-changed-nodes))
  (not (env-contradictory new-focus)))

;;; THIS IS THE VERSION CURRENTLY USED.
;;; This remains buggy.
;;; Remember in this paradigm we don't find all contradictions, so it can well be the
;;; the case that the state before the current change might still be inconsistent
;;; because, for example, it might contain multiple contradictions and we found only one.
(defun change-foci-simple-hybrid (update new-focus ignore &aux 
				  adds retracts old-good-foci node env start-time)
;  (check-env-waiting 'start)
  (if *debug* (check-env-waiting 'start))
  (setq start-time (get-internal-real-time))

;  (let ((n (tms:node 633.)))
;    (if n
;  (print (list 'start (n-a-envs n) (car *foci*) *good-foci*))))


  (and *debug* (env-contradictory new-focus)
      (error "Called change-foci-simple-hybrid with contradictory env"))

  (setq old-good-foci *good-foci*)

  (cond (old-good-foci
	 (multiple-value-setq (retracts adds) (compute-foci-change new-focus *good-foci*))
	 (if *change-foci-trace* (format T "~% Adds: ~A, Retracts: ~A" adds retracts))

	 ; ***** But enable calls change-foci right back.  Comment out the follwing 3 lines?

;	 (when (and (null retracts) (null (cdr adds)))
;	   (enable-current-assumption (car adds))
;	   (return-from change-foci-simple-hybrid nil))

	 ;; I once thought it might be clever to not do retract-assumptions and let
	 ;; these be caught lazily.  That doesn't work because it might be the case
	 ;; that the removal of the supporting environment might cause another supporting
	 ;; environment to the for which has not been propagated.

	 ;; Before doing anything, look ahead to see if loss is emminent and don't bother
	 ;; doing anything at all.
	 ;; This is very incomplete right now, but it helps a lot. Extend***

	 (dolist (a adds)
	   (when (and (setq node (assumption-node a))
		      (n-a-classes node))
	     ;; **presumes the class is oneof.
	     (dolist (n (tms::class-nodes (car (n-a-classes node))))

	       (when (setq env (true-in-blocked? n new-focus))
		 ;;***** In many cases the previous focus became inconsistent, and therefore
		 ;;***** this will fail for the same reason.  But we don't check that right yet
		 (cond ((eq node n)
;			(error "LOOK")
				    
				    (return nil))
		       (t (cons-for-false env a 'EXCLUSIVE)
			  (if *change-foci-trace*
			      (format T "--- Avoiding the shift after ~D seconds."
				      (real-time-taken start-time)))
			  (return-from CHANGE-FOCI-SIMPLE-HYBRID nil)))))))

	 ;; This only moves the labels to be correct with respect to the new focus.
	 (if *debug* (check-env-waiting 'd))
;	 (setq *good-foci* nil)

;	 (print (list 'last *last-assumption-enabled*))
	 (move-hybrid-labels adds retracts)

	 ;; This is not quite right, but close.  It doesn't correct for early contras exits.
	 (cond ((null *last-assumption-enabled*))
	       ((memq *last-assumption-enabled* retracts)
		(setq *last-assumption-enabled* nil))
	       ((null adds))
	       (t (if *change-foci-trace*
		      (format T "~% Cleaning up last assumption: ~A"
			      *last-assumption-enabled*))
		  (cleanup-last-assumption (car (last adds)))))

	 (if *debug* (check-env-waiting 'c))


	 ;; **** More generally we want to pick the assumption in the least
	 ;; number of envs probably!!!!!
	 (if adds (setq *last-assumption-enabled* (car (last adds))))

	 ;; If look ahead doesn't tell us what's going on... try this.
	 
	 ;; In the current strategy, retracting an assumption can make the focus
	 ;; inconsistent because the retraction may install the best environment
	 ;; for the ultimate focus.

	 ;; All the incomplete assumptions, which are not added back now, should be
	 ;; retracted now.  If we perchance encounter a contradiction, we don't change
	 ;; the current good focus.
	 (when (and *incomplete-assumption*
		    (not (assumption-in-focus *incomplete-assumption*)))
	   (retract-assumption *incomplete-assumption*)
	   (when (env-contradictory new-focus)
	     (cleanup-adds-retracts adds retracts old-good-foci)
	     ;; There is a problem that showed up in doing Forbus' more complex examples.
	     ;; Namely, the above retract-assumption can install new n-a-envs wrt to
	     ;; the assumptions just added.  We must retract those assumptions to make
	     ;; sure the label is correct.  **** A more general solution is to have
	     ;; multiple *incomplete-assumption*.
	     ;;****** temporary
	     (let ((*foci* (list *good-foci*)))
	       (dolist (a adds) (retract-assumption a)))

	     (if *change-foci-trace* (format T "--- Contradiction(1) after ~D seconds."
					     (real-time-taken start-time)))

;	     (error "FOO")

	     (return-from change-foci-simple-hybrid nil))
	   (setq *incomplete-assumption* nil))

	 (dolist (r retracts)
	   (retract-assumption r)
	   ;; I'm not sure this is right, but everything is correct up to the current
	   ;; retraction.
	   ;; ***** there is something rather wrong here because the retract/add
	   ;; ***** has the bug that it doesn't complete if there is a contradiction
	   ;; ***** and those don't really get fixed up.
	   (when (env-contradictory new-focus)
	     (setq *incomplete-assumption* r)
	     ;; The completed retracts have already been done.
	     (let ((done nil))
	       (dolist (done-r retracts)
		 (push done-r done)
		 (if (eq done-r r) (return)))
	       (setq old-good-foci (multiple-uncons-env old-good-foci done)))
	     (cleanup-adds-retracts adds retracts old-good-foci)
					     (real-time-taken start-time)
					     r
					     )
	     ;;***** this needs to be handled with *incomplete-assumptions*
	     (let ((*foci* (list *good-foci*)))
	       (dolist (a adds) (retract-assumption a)))
	     (return-from change-foci-simple-hybrid nil))

	 ;; We want to make sure the *incomplete-assumption* is the first add, so
	 ;; we won't suffer from the problem of two *incomplete-assumption*.
	 (when *incomplete-assumption*
	   (if *change-foci-trace*
	       (format T "~% Adding the incomplete ~A first" *incomplete-assumption*))
	   (unless (eq (car adds) *incomplete-assumption*)
	     ;; **** could be more optimal.
	     (setq adds (cons *incomplete-assumption*
			      (fdelq1 *incomplete-assumption* adds))))
	   (setq *incomplete-assumption* nil))

	 (if (env-contradictory new-focus)
	     (format T "~% Still inconsistent after retraction?"))

	 (do ((a adds (cdr a)))
	     ((null a))
	   (unless (env-contradictory new-focus)
	     (enable-assumption (car a)))

	   ;;; This is a little bit kludgey, we may be able to make the next more efficient.

	   (when (env-contradictory new-focus)
	     (setq *incomplete-assumption* (car a))
	     (if *change-foci-trace* (format T "~% Retractions: ~A (first is incomplete)" a))
	     (if *change-foci-trace* (format T "--- Contradiction(3) after ~D seconds."
					     (real-time-taken start-time)))
	     (cleanup-adds-retracts adds retracts
				    (multiple-uncons-env new-focus
							 (sort (fcopylist a)
							       #'(lambda (x y)
								   (assumption-orderp x y)))))
	     ;;;****** needed for KDF's example to work.
	     ;;; Because the labels will not be correct.  ***** All these assumptions are
	     ;;; incomplete.
	     (let ((*foci* (list *good-foci*)))
	       (dolist (a (cdr a)) (retract-assumption a)))

;	     (when (and (car a)
;			(= 10. (assumption-unique (car a))))
;		  (describe (tms:node 1011.))
;		  (describe *good-foci*))


	     (return-from change-foci-simple-hybrid nil)))

	 (setq *good-foci* new-focus)
	 (if (eq *contra-env* *good-foci*) (error "UH3"))

	 (and *ltms* *changed-hybrid-nodes* (error "Can't have changed hybrid nodes with LTMS"))

	 (do () ((null (setq node (pop *changed-hybrid-nodes*))))
	   (cleanup-single-node-simple-hybrid node)
	   (when (env-contradictory new-focus)
	     (if *change-foci-trace* (format T "--- Contradiction(4) after ~D seconds."
					     (real-time-taken start-time)))
	     (return-from change-foci-simple-hybrid nil)))
;	 (check-env-waiting 'B)
	 (if *debug* (check-env-waiting 'B))
;	 (check-hybrid-labels "before")
	 (update-atms)
;	 (check-hybrid-labels "after")

	 ;; Note the focus could be inconsistent now.
	 (if *change-foci-trace* (format T "--- Complete after ~D seconds."
					 (real-time-taken start-time)))

;	 (check-env-waiting 'A)
	 (if *debug* (check-env-waiting 'A))
	 (return-from change-foci-simple-hybrid nil)

	 ;;;***** this is here for diagnostic purposes.
;	 (dolist (n *nodes*) (hybrid-label n))

;; Next trhee are debugging.
;	 (if update (update-atms))
;	 (check-hybrid-labels-1 *nodes* 'A)
;	 (check-hybrid-labels-1 *assumptions* 'A)

	 )
	(t ;;******** THIS SHOULD BE AN ALMOST IMPOSSIBLE EVENT.
	 (error "This won't work anymore")
	 ;;*good-foci* not set among many other things.
	   (dolist (a *assumptions*) (setf (assumption-in-focus a) nil))
	   (dolist (a (env-assumptions new-focus)) (setf (assumption-in-focus a) T))

	   (change-foci-simple-hybrid-1 new-focus *assumptions*)
	   (change-foci-simple-hybrid-1 new-focus *nodes*)
	   ))
  (unless (env-contradictory new-focus)
    (setq *good-foci* new-focus)
    (if update (update-atms)))
  )

(defun change-foci-simple-hybrid (update new-focus ignore &aux adds retracts)
  (multiple-value-setq (retracts adds) (compute-foci-change new-focus *current-focus*))
  (change-assumptions adds retracts))

(defvar *pending-adds* nil)

(defvar *pending-retracts* nil)

(defvar *current-focus* nil)

;;; Returns T if consistent.
(defun change-assumptions (uadds uretracts &aux
			   node env start-time *going-nodes* new-focus adds retracts *contradiction*)
  (if *change-foci-trace*
      (format T "~% User: Adds: ~A, Retracts: ~A"
	      (if (< (length uadds) 5) uadds (length uadds))
	      (if (< (length uretracts) 5) uretracts (length uretracts))))

  ;; I commented this out.
;  (or *ltms* *sltms* (error "Won't work"))
  ;; Cleanup the adds/retracts of the user.
  (dolist (a uadds) (if (memq a uretracts) (error "Adding and retracting ~A" a))
    (unless (assumption-in-focus a) (push a adds)))
  (dolist (r uretracts)
    (if (assumption-in-focus r)
	(push r retracts)
	(format T "~% Retracting ~A is unnecessary as it is not in focus" r)))

  (move-hybrid-labels adds retracts)


;  (format T "~% P: ~A, ~A" *pending-adds* *pending-retracts*)

  (setq new-focus (change-env *current-focus* adds retracts))

  (if *change-foci-trace* (format T "~% Setting foci to ~A" new-focus))

  ;;; An error check.
;  (dolist (a *assumptions*)
;    (cond ((assumption-in-focus a)
;	   (unless (vector-member a (env-vector new-focus))
;	     (error "Assumption ~A labeled in focus but isn't" a)))
;	  ((vector-member a (env-vector new-focus))
;	   (error "Assumption ~A should be labeled in focus but isn't" a))))

;  (if (env-contradictory new-focus)
;      (error "Switching to inconsistent focus? --- this should be optimized away"))

  (setq *foci* (list new-focus)
	*current-focus* new-focus)

;  (check-current-focus)


  (dolist (a adds)
    (cond ((memq a *pending-adds*))
	  ((memq a *pending-retracts*)
	   (setq *pending-retracts* (fdelq1 a *pending-retracts*))
	   ;; This may never be invoked:
	   (push a *pending-adds*))
	  (t (push a *pending-adds*))))

  (dolist (r retracts)
    (cond ((memq r *pending-retracts*))
	  ((memq r *pending-adds*)
	   ;; Because of the way this algorithm works assumptions on *pending-adds*
	   ;; might be partially added.  Hence, they need retraction.
	   ;;****
	   (push r *pending-retracts*)
	   (setq *pending-adds* (fdelq1 r *pending-adds*)))
	  (t (push r *pending-retracts*))))

;  (format T "~% P: ~A, ~A" *pending-adds* *pending-retracts*)

  (when (env-contradictory new-focus)
    (if *going-nodes* (process-changed-nodes))
    (if *change-foci-trace* (format T "--- but new focus is a contradictory env already!"))
    (return-from change-assumptions nil))

;  (check-env-waiting 'start)
  (if *debug* (check-env-waiting 'start))
  (setq start-time (get-internal-real-time))

;  (let ((n (tms:node 633.)))
;    (if n
;  (print (list 'start (n-a-envs n) (car *foci*) *good-foci*))))


  (and *debug* (env-contradictory new-focus)
      (error "Called change-assumptions with contradictory env"))

  (if *change-foci-trace*
      (format T "~% Pending: Adds: ~A, Retracts: ~A"
	      *pending-adds*
	      *pending-retracts*))

  ;; I once thought it might be clever to not do retract-assumptions and let
  ;; these be caught lazily.  That doesn't work because it might be the case
  ;; that the removal of the supporting environment might cause another supporting
  ;; environment to the for which has not been propagated.

  ;; Before doing anything, look ahead to see if loss is emminent and don't bother
  ;; doing anything at all.
  ;; This is very incomplete right now, but it helps a lot. Extend***

  (dolist (a *pending-adds*)
    (when (and (setq node (assumption-node a))
	       (n-a-classes node))
      ;; **presumes the class is oneof.
      (dolist (n (tms::class-nodes (car (n-a-classes node))))
	
	(when (setq env (true-in-blocked? n new-focus))
	  ;;***** In many cases the previous focus became inconsistent, and therefore
	  ;;***** this will fail for the same reason.  But we don't check that right yet
	  (cond ((eq node n)
		 ;			(error "LOOK")
				    
		 (return nil))
		(*rltms* (if *going-nodes* (process-changed-nodes))
			 (if *change-foci-trace* (format T " --- Block label rules this out."))
			 (return-from CHANGE-ASSUMPTIONS 
			   (values nil (list a env))))

		(t (cons-for-false env a 'EXCLUSIVE)
		   (if *change-foci-trace*
		       (format T "--- Avoiding the shift after ~D seconds."
			       (real-time-taken start-time)))
		   (unless (eq *foci* :EMPTY)
		     (print (list env a))
		     (error "Can't happen --- Focus isn't empty!"))
		   (if *going-nodes* (process-changed-nodes))
		   (return-from CHANGE-ASSUMPTIONS nil)))))))


  ;; This only moves the labels to be correct with respect to the new focus.
  (if *debug* (check-env-waiting 'd))
;	 (setq *good-foci* nil)

;	 (print (list 'last *last-assumption-enabled*))


  (if (env-contradictory new-focus) (error "Focus is inconsistent 0"))

  ;; Remember an *incomplete-assumption* is now only an assumption we tried
  ;; to add, but wasn't completely added or removed.
  (when (and *incomplete-assumption*
	     (not (assumption-in-focus *incomplete-assumption*)))
    (retract-assumption *incomplete-assumption*)
  
    (when (env-contradictory new-focus)
      (if *change-foci-trace*
	  (format T "--- Retracting incomplete ~A causes contradiction"
		  *incomplete-assumption*))
      (if *going-nodes* (process-changed-nodes))
      (return-from change-assumptions nil)))

  ;; This assumption could not have been deleted from *pending-adds*
  (setq *incomplete-assumption* nil)

  ;; Retraction can never cause a contradiction in new scheme.  Why did I say that,
  ;; of course it can.
  (do ((a)) ((null *pending-retracts*))
    (setq a (car *pending-retracts*))
;    (format T "~% Retracting: ~A, Remaining: ~A" a *pending-retracts*)
    (retract-assumption a)
    (when (env-contradictory new-focus)
      (setq *incomplete-assumption* a)
      (if *change-foci-trace* (format T "--- Retracting ~A causes contradiction" a))
      (if *going-nodes* (process-changed-nodes))
      (return-from change-assumptions nil))
    (pop *pending-retracts*))

  (do ((a)) ((null *pending-adds*))
    (setq a (car *pending-adds*))
    (enable-assumption a)
    (when (or (env-contradictory new-focus) *contradiction*)
      (setq *incomplete-assumption* a)
      (if *change-foci-trace* (format T "~% Retractions: ~A (first is incomplete)" a))
      (if *change-foci-trace* (format T "--- Contradiction(3) after ~D seconds."
				      (real-time-taken start-time)))

      (if *going-nodes* (process-changed-nodes))
      (if *change-foci-trace*
	  (format T "--- enabling assumption immediately produces contra."))
      (if *contradiction* (return-from change-assumptions (values nil *contradiction*)))
      (return-from change-assumptions nil))
    (pop *pending-adds*))

  (setq *good-foci* new-focus)
  (if (eq *contra-env* *good-foci*) (error "UH3"))

  (update-atms)
  (if *going-nodes* (process-changed-nodes))
  ;;**** temporary kludge:
  (if *contradiction* (return-from change-assumptions (values nil *contradiction*)))
  (if *change-foci-trace* (format T "--- Complete after ~D seconds."
				  (real-time-taken start-time)))

  (null (env-contradictory *current-focus*))
  )


;;; There were many bugs in this routine when written above.  If this ever
;;; becomes inefficient, we can rewrite this more optimally taking advantage
;;; of what has been done already in the caller.  Remember, by default the
;;; caller has set all these variables already.
;;;
;;; This used to check that new-good-foci was consistent, but that would not be right because
;;; sometimes we have no alternative where the old and the new foci are inconsistent.  We don't
;;; want to go do ddb!
(defun cleanup-adds-retracts (adds retracts new-good-foci)
  (setq *good-foci* new-good-foci)
  (dolist (a adds)
    (unless (vector-member a (env-vector *good-foci*))
      (move-assumption-out a)
      (setf (assumption-in-focus a) nil)))
  (dolist (a retracts)
    (when (vector-member a (env-vector *good-foci*))
      (move-assumption-in a)
      (setf (assumption-in-focus a) T))))

;;; This is the difficult case whenever another assumption is pushed on the stack
;;; without retracting this one.  We could be more clever about computing
;;; the env-waiting any many cases.
(defun cleanup-last-assumption (new-assumption &aux (count 0) waiting)
  (if *ltms* (return-from cleanup-last-assumption nil))
  (dolist (env (assumption-envs-to-index *last-assumption-enabled*))
    (cond ((env-indexed? env))
	  ((env-contradictory env))
	  ((null (env-nodes env))
	   (setf (env-indexed env) 0)
	   (setf (env-toindex env) 0))
;	  ((vector-member new-assumption (env-vector env))
;	   (push env (assumption-envs-to-index new-assumption))
;	   (format T "~% Optimized: ~D ~D" (env-waiting env) (compute-env-waiting env))
;	   )

	  (t
	   (incf count)
	   (setf (env-indexed env) 1)
	   (setf (env-toindex env) 0)
	   (setq waiting 0)
;	   (format T "~% CLEANUP-LAST-ASSUMPTION: ~A" env)
	   (do-assumptions-blits (env-vector env)
				 #'(lambda (a)
				     #+Symbolics
				     (declare (sys:downward-function))
				     (unless (assumption-in-focus a) (incf waiting))
				     (push env (assumption-in-envs a))))
	   (setf (env-waiting env) waiting)
;	   (format T "~% CLEANUP-LAST-ASSUMPTION: ~A to ~D" env waiting)	
	   )
))
  (setf (assumption-envs-to-index *last-assumption-enabled*) nil)
  (if (and *change-foci-trace* (> count 0))
      (format T "~% Indexed ~D environments to cleanup ~A" count *last-assumption-enabled*))
  )

(defun cleanup-in-envs (assumption &aux (count 0) waiting)
  (if *ltms* (return-from cleanup-in-envs nil))
  (dolist (env (assumption-envs-to-index assumption))
    (cond ((env-indexed? env))
	  ((env-contradictory env))
	  ((null (env-nodes env))
	   (setf (env-indexed env) 0)
	   (setf (env-toindex env) 0))
	  (t
	   (incf count)
	   (setf (env-indexed env) 1)
	   (setf (env-toindex env) 0)
	   (setq waiting 0)
;	   (format T "~% CLEANUP-IN-ENVS: ~A" env)
	   (do-assumptions-blits (env-vector env)
				 #'(lambda (a)
				     #+Symbolics
				     (declare (sys:downward-function))
				     (unless (assumption-in-focus a) (incf waiting))
				     (push env (assumption-in-envs a))))
	   (setf (env-waiting env) waiting)
;	   (format T "~% CLEANUP-IN-ENVS: ~A to ~D" env waiting)	
	   )
))
  (setf (assumption-envs-to-index assumption) nil)
  (if (and *change-foci-trace* (> count 0))
      (format T "~% Indexed ~D environments to cleanup ~A" count assumption))
  )

(defun change-foci-simple-hybrid-1 (new-focus nodes)
  (dolist (n nodes)
    (cleanup-single-node-simple-hybrid n)
    (if (env-contradictory new-focus) (return)))
  )

(defun move-hybrid-labels (adds retracts)
  (dolist (a adds) (setf (assumption-in-focus a) T))
  (dolist (r retracts) (setf (assumption-in-focus r) nil))
  (if *ltms* (return-from move-hybrid-labels nil))
  (if *debug* (check-env-waiting))
  (dolist (r retracts) (move-assumption-out r))
  (dolist (a adds) (move-assumption-in a))
  ;; Further optimization is possible here, but for now all pending indexings are done
  ;; right now.
  (dolist (a adds) (cleanup-in-envs a)))
  

;;; This is a post test to make sure every label is what it is supposed to be.  For
;;; debugging.
(defun check-hybrid-labels-1 (nodes msg &aux focus)
  (unless (eq *foci* :EMPTY)
    (setq focus (car *foci*))
    (dolist (n nodes)
      (check-hybrid-label n focus msg))))

(defun check-envs-nodes ()
  (dolist (n *nodes*)
    (dolist (e (n-a-blocked n))
      (cond ((eq e *empty-env*))
	    ((memq n (env-nodes e)))
	    (t (error "Node ~A is missing from (env-nodes ~A)"
		      n e)))))
  (dotimes (i (1+ *max-env-count*))
    (dolist (e (aref *environments* i))
      (unless (env-contradictory e)
	(check-env-nodes e)
	(dolist (n (env-nodes e))
	  (unless (memq e (n-a-blocked n))
	    (error "Env ~A is missing from envs of ~A"
		   e n)))))))

(defun check-env-nodes (env)
  (if (env-contradictory env) (error "Can't happen"))
  (do ((nodes (env-nodes env) (cdr nodes)))
      ((null nodes))
    (if (memq (car nodes) (cdr nodes))
	(error "Node ~A occurs twice on env-nodes(~A)"
	       (car nodes) env))))

(defun check-node (n &optional msg)
  (check-hybrid-label n (car *foci*) msg))

(defun check-hybrid-label (n focus msg &aux env blocked shortest)

    (setq blocked (n-a-blocked n) env (car (n-a-envs n)) shortest nil)

    (if (cdr (n-a-envs n)) (error "~A: Label of ~A is greater than 1" msg n))

    (when env
      (unless (memq env blocked) (error "~A: Focus env is not in blocked env for ~A" msg n))
      (if (not (subset-env? env focus))
	  (error "~A: Env ~A not in focus in node ~A" msg env n)))
    
    (do ((blocked (cdr blocked) (cdr blocked)))
	((null blocked))
      (if (memq (car blocked) (cdr blocked))
	  (error "~A: Env occurs twice in blocked label" msg)))

    (dolist (e blocked)
      (cond ((not (subset-env? e focus)))
	    ((null shortest) (push e shortest))
	    ((< (env-count e) (env-count (car shortest)))
	     (setq shortest (list e)))
	    ((= (env-count e) (env-count (car shortest)))
	     (push e shortest))))

    (cond ((null shortest))
	  ((null env)
	   (error "~A: Focus label for ~A is empty while it should be one of ~A"
		  msg n shortest))
	  ((not (memq env shortest))
	   (error "~A: Focussed label is ~A but should be one of ~A"
		  msg env shortest))))

;;; This is a separate function simply because its easier to check in a single
;;; place any errors.
(defun set-hybrid-label (node env who &optional reason &aux old)
;  (check-just-counts)

;  (when (memq (n-a-unique node) '(138 125 146.))
;    (format T "~% ~A is setting node ~A to ~A within ~A was ~A blocked = ~A"
;	    who node env *foci* (hybrid-label node) (n-a-blocked node))
;    )						
  who
  (cond ((null env)
	 (cond ((null *ltms*))
	       ((null (setq old (hybrid-label node))))
	       ((eq who 'PROPAGATE-OUTNESS) (setf (n-a-support node) nil))
	       (t (setf (n-a-envs node) nil)
		  (setf (n-a-support node) nil)
		  ;; No need to propagate the contra env as that will have been done.
		  (cond ((and (not *sltms*) (env-contradictory old))
			 (dolist (c (n-a-nclauses node))
			   (incf (clause-count c))
			   )
			 (dolist (j (n-a-consequents node))
			   (incf (just-count j))))
			(t (propagate-outness node)))
		  ;; This makes sure an alternative label, if one exists will be
		  ;; searched for.
		  (dolist (c (n-a-pclauses node))
		    (cond ((clause-cost c))
			  ((> (clause-count c) 0))
			  (t (setf (clause-consequent c) nil)
			     (queue-clause c))))
		  (when (n-a-neg node)
		    (dolist (c (n-a-nclauses (n-a-neg node)))
		      (cond ((clause-cost c))
			    ((> (clause-count c) 0))
			    (t (setf (clause-consequent c) nil)
			       (queue-clause c)))))
		  (dolist (j (n-a-justifications node))
		    (cond ((just-cost j))
			  ((> (just-count j) 0))
			  (t (queue-justification j))))
		  (return-from set-hybrid-label nil)
		  ))
	 (setf (n-a-envs node) nil))
	((setq old (n-a-envs node))
	 (cond (*ltms* (and *debug* (null reason) (not (assumption? node))
			    (error "Must have supporting reason"))
;		       (check-support reason)
		       (unless (or (symbolp reason) (just-antecedents reason))
			 (setf (clause-consequent reason) node))

		       (setf (n-a-support node) reason))
	       (t (set-env-hybrid env 1)))
	 (rplaca old env))
	(t (cond (*ltms* (and *debug* (null reason) (not (assumption? node))
			      (error "Must have supporting reason"))
			 (unless (or (symbolp reason) (just-antecedents reason))
			   (setf (clause-consequent reason) node))
			 (setf (n-a-support node) reason)
			 (dolist (c (n-a-nclauses node))
			   (decf (clause-count c)))
			 (dolist (j (n-a-consequents node))
			   (decf (just-count j))))
		 (t (set-env-hybrid env 1)))
	   (setf (n-a-envs node) env))))

(defun check-support (reason &aux node subreason)
  (unless (eq reason :ASSUMPTION)
    (setq node (just-consequent reason))
    (dolist (a (just-antecedents reason))
      (setq subreason (n-a-support a))
      (unless (eq subreason :ASSUMPTION)
	(if (memq node (just-antecedents subreason))
	    (error "Circular support discovered"))))))

(defun check-hybrid-labels (&optional (msg "bad hybrid label") &aux env flag)
  (dolist (n *nodes*)
    (when (and (setq env (hybrid-label n))
	       (not (= 0 (env-waiting env))))
      (setq flag T)
      (format T "~% Node ~A has out of focus hybrid label ~A" n env)))
  (if flag (error msg)))

;;; Returns the current best label for this node.  This is obsolete because
;;; we precompute it correctly now.  But this can be useful for future experiments.
(defun hybrid-label-debug (node &aux focus good-env picked env blocked)
  (cond ((eq *foci* :EMPTY) nil)
	((eq (n-a-focus node) (setq focus (car *foci*))) (car (n-a-envs node)))
	(t (setq env (car (n-a-envs node)) blocked (n-a-blocked node))
	   (and env (if (subset-env? env focus) (setq good-env env)))
	   (setq picked nil)
	   (do ((e blocked (cdr e)))
	       ((null e)
		(cond ;; Case 1: Nothing useful found in blocked label.
		  ((null picked)
		   ;;;***** could have a flag if contradictions occured.
		   ;;; ***** in all three cases here.
		   (cond ((null env))
			 ((null good-env)
			  (error "Can't happen --- case 1")
			  ;; This is the only possibility which is now allowed.
			  (set-hybrid-label node nil 'hybrid-label)
			  (out-node node))))
		  ;; Case 2: Something useful was found and old label was empty.
		  ((null env)
		   (error "Can't happen yet - case 2")
		   (setq env (car picked))
		   (set-hybrid-label node env 'hybrid-label))
		  ;; Case 3: Something useful was found and old label was not empty.
		  (t (error "Can't happen yet - case 3")
		     (setq env (car picked))
		     (set-hybrid-label node env 'hybrid-label))))
	     (cond ((null (car e)))
		   ((eq (car e) env))
		   ;;**************** contradiction appears in label.
		   ((env-contradictory (car e)) (error "Why")
		    (rplaca e nil))
		   ((not (subset-env? (car e) focus)))
		   ((null picked)
		    (if (or (null good-env) (< (env-count (car e)) (env-count good-env)))
			(setq picked e)))
		   ((< (env-count (car e)) (env-count (car picked)))
		    (setq picked e))))
	   (setf (n-a-focus node) focus)
	   env)))

;;; If env is supplied as an argument, this means that we already know we
;;; want to get this env out of focussed label.
;;; This now exploits the fact that scores increase as you look through.
(defun cleanup-single-node-simple-hybrid (n &optional env
					  &aux picked new-env best-env
					  (best-score 1000000) score)
  (if *ltms* (error "Don't call cleanup-single-node-simple-hybrid in LTMS"))

;  (and (= (n-a-unique n) 1221.) (format T "~% Cleaning up ~A" n))

  ;; If the node is correct for the current focus (which can occur for various reasons),
  ;; do nothing.
  (cond (env)
	((or (eq *foci* :EMPTY)
	     (eq (n-a-focus n) (car *foci*)))
	 (return-from CLEANUP-SINGLE-NODE-SIMPLE-HYBRID nil))
	((setq env (car (n-a-envs n)))
	 (when (in-current-focus? env)
	   (setq best-env env best-score (env-count env)))))
;  (and (= (n-a-unique n) 1221.) (format T "~% Working on ~A" n))

  (dolist (blocked-env (n-a-blocked n))
    (cond ((eq blocked-env env))
	  ((not (in-current-focus? blocked-env)))
	  ((< (setq score (env-count blocked-env)) best-score)
	   (setq picked blocked-env best-score score)
	   ;; blocked envs are sorted by cost.
	   (return nil))))


  (cond ;; Case 1: Nothing useful found in blocked label.
        ((null picked)
	 ;;;***** could have a flag if contradictions occured.
	 ;;; ***** in all three cases here.
	 (cond ((null env))
	       ((null best-env)
		(set-hybrid-label n nil 'CLEANUP-SINGLE-NODE-SIMPLE-HYBRID)
		(out-node n))))
	; ; Case 2: Something useful was found and old label was empty.
	((null env)
	 ;; Then queue the new label for insertion!********* FEEX.
	 ;; This should be done on the spot for efficiency.****
	 ;;*** efficient.
	 (setq new-env picked)
	 (set-hybrid-label n new-env 'CLEANUP-SINGLE-NODE-SIMPLE-HYBRID)
	 ;;;*** need to feex update-node-real-hybrid.
	 (update-node-hybrid-common n new-env env)
	 )
	;; Case 3: Something useful was found and old label was not empty.
	(t (set-hybrid-label n picked 'CLEANUP-SINGLE-NODE-SIMPLE-HYBRID)
	   (update-node-hybrid-common n picked env)))
;  (and (= (n-a-unique n) 1221.)
;       (format T "~% Setting 1221's focus to ~A" *foci*))

  ;; Don't change this to *foci*: This is the focus we are heading towards.
  ;; Why is this comment above?  *foci* is the focus we are heading towards, and
  ;; this node is now correct for it.
  (unless (eq *foci* :EMPTY)
    (setf (n-a-focus n) (car *foci*))))

;;; Experimental.  Here in-env is being added.  We don't know much else.
;;; This cannot update the focus as it only checks the addition of in-env.
;;; We do know that in-env is in the focus.
;;; This presumes the new-focus is the current focus.
(defun cleanup-single-node-env (n in-env &aux env node-envs)
  (cond ((eq (n-a-focus n) (car *foci*)))
	((and (setq node-envs (n-a-envs n))
	      (<= (env-count (setq env (car node-envs))) (env-count in-env))
	      ;; The hybrid label can't be guaranteed correct, and this test is fast.
	      (in-current-focus? env)))
	;; Only try to update the node if really necessary:
	(t (cleanup-single-node-simple-hybrid n (car node-envs)))))


;	(t (set-hybrid-label n in-env 'CLEANUP-SINGLE-NODE-ENV)
;	   ;; This may queue for a second time, but often not?
;	   (update-node-hybrid-common n in-env env)

(defun cleanup-unfocussed-nodes ()
  (do ((n *unfocussed-nodes* (cdr n)))
      ((null n))
    (cond ((eq (n-a-enqueued? (car n)) :AGENDA))
	  ((or (i-out? (car n))
	       (null (n-a-has-consumers? (car n))))
	   (setf (n-a-enqueued? (car n)) nil)
	   (rplaca n nil))
	  ((in-focus? (car n))
	   (insert-in-agenda (car n))
	   (rplaca n nil))))
  (setq *unfocussed-nodes* (fdelqa nil *unfocussed-nodes*)))

;;; This throws environments out of the label which are no longer relevant
;;; to the new foci.  This is done first whenever foci is changed.  This
;;; is to make sure any subsequent ATMS operations don't stumble over irrelevant environments.
;;; A lot of cycles get eaten up here.  So this is worth optimizing.
;;; Isn't used in simple-hybrid.
(defun cleanup-nodes-general (nodes &aux env)
  (if *simple-hybrid* (error "Can't happen"))

  ;; As this gets called a lot. Optimizing this special case is worth it.
  (dolist (n nodes)
    (cond ((null (n-a-envs n)))
	  ;; Otherwise optimize the case where the label is a singleton.
	  ((null (cdr (n-a-envs n)))
	   (setq env (car (n-a-envs n)))
	   (unless (dolist (f *foci*) (if (subset-env? env f) (return T)))
	     (push env (n-a-blocked n))
	     (setf (n-a-envs n) nil)
	     (out-node n)))
	  (t (let ((new-label nil) best)
		(dolist (f *foci*)
		  (setq best nil)
		  (dolist (e (n-a-envs n))
		    (cond ((not (subset-env? e f)))
			  ((null best) (setq best e))
			  ((< (env-count e) (env-count best)) (setq best e))))
		  (and best (not (memq best new-label)) (push best new-label)))
		(dolist (e (n-a-envs n))
		  (unless (memq e new-label)
		    (push e (n-a-blocked n))))
		(setf (n-a-envs n) new-label)
		(unless new-label (out-node n))
		)))
    ))

(defun cleanup-foci ()
  (cond ((null *foci*))
	((eq *foci* :EMPTY))
	(t (do ((foci *foci* (cdr foci)))
	       ((null foci))
	     (if (env-contradictory (car foci))
		 (rplaca foci nil)))
	   (setq *foci* (fdelqa nil *foci*))
	   (unless *foci* (setq *foci* :EMPTY)))))

;;; Returns T if node is within current foci.
;;; Returns T if there are no foci.
(defun in-focus? (node)
  (cond ((eq *foci* :EMPTY) ;(format T "~% **** empty")

	  ;this does bad things 06/06/92.
	  ;This works better:
	 (n-a-envs node))

	(*simple-hybrid* (n-a-envs node))
	((null *foci*) T)
	(t (dolist (f *foci*) (if (true-in? node f) (return-from IN-FOCUS? T))))))

(defun check-current-focus ()
  (dolist (a *assumptions*)
    (cond ((eq (assumption-unique a) 'delay))
	  ((assumption-in-focus a)
	   (unless (vector-member a (env-vector *current-focus*))
	     (error "In focus but not in current focus ~A" a)))
	  ((vector-member a (env-vector *current-focus*))
	   (error "In current focus, but not in focus ~A" a)))))

;;; In general we can do far smart things.  This is a special-case optimization.
;;; For binary nogoods.  This can be made more efficient.  The fdelqa here is stupide.
;;; ***** The unconses here are really slow.
(defun update-assumption (node new-envs complete-envs &aux one-bad uncons)
  (if (n-a-contradictory node) (error "bogus --- remove if needed"))

  ;;; b, L => n; n,b is a nogood ===> We can deduce b,L is a nogood.

  (do ((env new-envs (cdr env)))
      ((null env))
    (when (vector-intersection? (assumption-binary-vector node) (env-vector (car env)))
      (explained-contradiction env node)
      (setq one-bad T)
      (rplaca env nil)))
  (when one-bad
    (setq new-envs (sanitize-envs new-envs))
    (unless new-envs (return-from UPDATE-ASSUMPTION nil))
    (setq complete-envs (sanitize-envs complete-envs)
	  one-bad nil))
  ;;; This resolution rule is always worth doing early.  If an assumption has become
  ;;; true.  Immediately reduce the nogoods.  This is an instance of the synthesis rule,
  ;;; but its always worth doing early.  
  (cond ((eq (car new-envs) *empty-env*) (setq one-bad (update-assumption-nogoods node)))
	;; If resolution is on, the following is totally redundant.
	;; It captures one half of resolution, the other half would be to do the dual
	;; upon the discovery of every nogood.
	(*resolve-by-labeling*)
	(*resolve-by-ordered-labeling*)
	(t (dolist (nogood (assumption-nogoods node))
	     (setq uncons nil)
	     (cond ((assumption? nogood))
		   ((subsumed-nogood? nogood))
		   (t (dolist (env new-envs)
			(cond ((and (null env) (env-contradictory env)))
			      (t (unless uncons (setq uncons (uncons-env nogood node)))
				 ;; ****Actually one-bad needs to be set only if we find a new nogood.
				 (setq one-bad T)
;				 (push (cons uncons env) foo)
				 (union-for-false uncons env 'NEEDS-WORK)
				 ))))))))
  (when one-bad
    (setq new-envs (sanitize-envs new-envs))
    (unless new-envs (return-from UPDATE-ASSUMPTION nil)))
  (when one-bad (setq complete-envs (sanitize-envs complete-envs)))
  (if *h45*
      (setq new-envs (or (cleanup-for-h45 node new-envs) (return-from UPDATE-ASSUMPTION nil))))
  (values new-envs complete-envs))

(defun update-assumption-nogoods (node &aux one-bad uncons)
  ;; The binary nogoods are stored as a bit vector.
  (dolist (a (vector-assumptions (assumption-binary-vector node) *assumption-array*))
    (unless (i-false? a)
      (contradictory-env (assumption-env a)
			 (if *explain-flag*
			     `(BASE REMOVED-TRUE-ASSUMPTION2
				    ,node
				    ,a
				    ., (let ((binary-nogood (double-if-exists node a)))
					 (if binary-nogood
					     (list binary-nogood
						   (env-contradictory binary-nogood)))))
			     '(BASE REMOVED-TRUE-ASSUMPTION2)))))
  (dolist (nogood (assumption-nogoods node))
    (cond ((assumption? nogood) (error "Should no longer happen"))
	  ((subsumed-nogood? nogood))
	  (t (setq uncons (uncons-env nogood node))
	     ;; Complete-envs may have changed:
	     (setq one-bad T)
	     (contradictory-env uncons
				(if *explain-flag*
				    `(BASE REMOVED-TRUE-ASSUMPTION
					   ,node ,nogood ,uncons)
				    '(BASE REMOVED-TRUE-ASSUMPTION))))))
  one-bad)


(defun explained-contradiction (env node)
  (contradictory-env (car env)
		     (if *explain-flag*
			 `(BASE ASSUMPTION-LABELING ,node
				. ,(dolist (a (env-assumptions (car env)))
				     (cond ((vector-member a
							   (assumption-binary-vector node))
					    (let ((binary-nogood (double-if-exists
								   node a)))
					      (if binary-nogood
						  (return (list a binary-nogood
								(env-contradictory
								  binary-nogood)))
						  (return (list a))))))))
			 '(BASE ASSUMPTION-LABELING))))

;;; This should be called after every call to contradictory-env on the current env
;;; set as that can cause arbitrary envs hacking.  *h45* is one such example.  
;;; Is resolution another???? Check.  Returns the updated new-envs.  Can be grossly
;;; optimized****

	     ;; Now remove all new-envs which have become subsumed for this node.
	     ;; **** this is totally stupid.  All you really have to check is to make
	     ;; sure each new-env is still on node-envs.  Thats absolutely all!!!!!!.
	     ;; Thus, for all cases this is inefficient code***************************
	     ;; And if h45 happens above, like process-queued-nogoods.  This can 
	     ;; never happen.

;;; This used to be a subset-env?, but thats not good enough.
(defun cleanup-for-h45 (node new-envs &aux node-envs)
  (setq node-envs (n-a-envs node))
  (do ((new-env new-envs (cdr new-env)))
      ((null new-env))
    (if (car new-env)
	(dolist (node-env node-envs)
	  (when (subset-env? node-env (car new-env))
	    (rplaca new-env nil)
	    (return)))))
  (setq new-envs (fdelqa nil new-envs)))

;;; This search is specifically organized to find contradictions of size 1 or size 2 first.
;;; It may fortuitously find other contradictions (may not be worth it?)
;;; but it will never actually
;;; create a contradictory environment, because that has shown in practice to be
;;; too expensive.

;;; Returns NIL if everything in new-envs has become contradictory or is to big.
;;;; ***** incompletely implemented: Returns T more often than necessary.
(defun update-node-c012 (node new-envs stack &aux continue)
  (if (memq node stack) (return-from UPDATE-NODE-C012 nil))
  ;; In general we can do smart things.  This is a special-case optimization.
  ;; For binary nogoods.  This can be made more efficient.  The fdelqa here is stupid.
  ;; *** this check may be thus removable from the normal update-node***
  (when (assumption? node)
    (do ((env new-envs (cdr env)))
	((null env))
      (cond ((null (car env)))
	    ((env-contradictory (car env)))
	    ((vector-intersection? (assumption-binary-vector node)
				   (env-vector (car env)))
	     (contradictory-env (car env) '(BASE ASSUMPTION-LABELING)))
	    ((< (env-count (car env)) 3.) (setq continue T))))
    (unless continue (return-from UPDATE-NODE-c012 nil)))
  (cond ((n-a-contradictory node)
	 (dolist (env new-envs)
	   (and env
		(not (env-contradictory env))
		(contradictory-env env '(BASE UPDATE-NODE-C012))))
	 T)
	(t (update-node-consequents-c012 node new-envs (cons node stack)) ;*** stack cons??
	   T)))

(defun update-node-consequents-c012 (node new-envs stack &aux consequent)
  (unless (null (setq consequent (n-a-consequents node)))
    (do () (nil)
      (unless (update-node-envs-c012 (car consequent) node new-envs stack)
	(return-from UPDATE-NODE-CONSEQUENTS-C012 nil))
      (unless (setq consequent (cdr consequent))
	(return-from UPDATE-NODE-CONSEQUENTS-C012 nil)))))

;;; This is only looking for nogoods of size 0, 1, 2 and those existing
;;; environments it fortuitously stumbles across.
;;; *** should it update labels???????????????***** this version does not!!!
;;; *** maybe it should update labels which don't cause cres??

;;; Returns NIL if new-envs is totally contradictory.  Not implemented enough.

(defun update-node-envs-c012 (consequent antecedent-node new-envs stack
			 &aux node antecedent-nodes)
  (setq node (first consequent) antecedent-nodes (cddr consequent))
  (cond ((n-a-contradictory node)
	 (unless (cdr antecedent-nodes)
	   (error "Contradiction should have been detected earlier"))
	 (weave-for-false-c012 new-envs (cdr consequent) antecedent-node)
	 T)
	((i-true? node))
	((cdr antecedent-nodes)
	 ;; This is probably faster than weaving.  Dunno.  The idea is we
	 ;; don't want to cons up all these stupid lists all the time.
	 ;; ** assumptions
	 (dolist (env new-envs)
	   (avoid-weaving consequent env antecedent-nodes antecedent-node stack))
	 T)
	(t (update-node-c012 node new-envs stack))))

(defun avoid-weaving (consequent env nodes antecedent-node stack &aux env1)
  ;; Punt if we can't do anything interesting.
  (if (or (env-contradictory env) (> (env-count env) 2)) (return-from AVOID-WEAVING nil))
  (prog ()
	start
	;; Skip to the first node which can tell us anything.
	(do nil ((null nodes)
		 ;; This test can be applied every union***********
		 ;; Can be highly optimized.***********************
		 ;; we can check This real easy.************
		 (dolist (known-env (n-a-envs (car consequent)))
		   (and (< (env-count known-env) 3)
			(subset-env? known-env env)
			(return-from AVOID-WEAVING nil)))
		 (update-node-c012 (car consequent) (list env) stack)
		 (return-from AVOID-WEAVING nil))
	  (cond ((i-true? (car nodes)))
		((eq (car nodes) antecedent-node) (setq antecedent-node nil))
		(t (return nil)))
	  (setq nodes (cdr nodes)))
	(when (eq env *empty-env*)
	  (setq env1 nil)
	  (dolist (env (n-a-envs (car nodes)))
	    (cond ((> (env-count env) 2))
		  ((null env1) (setq env1 env))
		  (T (avoid-weaving consequent env (cdr nodes) antecedent-node stack))))
	  (cond (env1 (setq env env1 nodes (cdr nodes)) (go start))
		(t (return nil))))
	;; *** we could have a version of union which took three arguments!.
	(setq env1 nil)
	(dolist (new-env (n-a-envs (car nodes)))
	  (cond ((> (env-count new-env) 2))
		;;*** could be optimized because are 1 or 2.
		((env-contradictory (setq new-env (2-union-env env new-env))))
		((null env1) (setq env1 new-env))
		(T (avoid-weaving consequent new-env (cdr nodes) antecedent-node stack))))
	(when env1 (setq env env1 nodes (cdr nodes)) (go start))))

;;; Env is new for antecedent-node, compute a new env(s) for consequent-node.
;;; I tries to avoid calling general-weave-c012 at all.
;;;****** is the first argument to update-node-c012 always redundant?***
;;;****** Make second argument always be a singleton.
;;;****** incorporate ideas of weaving-for-false, weaving-for-false-c012 here.
;;;****** this is a bit of a crock.  Weaving-for-false is the best example.
(defvar *justification* 'ILLEGAL-VALUE)		; Lucid demands a value.

;;; This only attempts to find contradictions of size 0, 1, 2.
(defun weave-for-false-c012 (envs *justification* node-to-ignore)
  (cond ;; If any antecedents are out, punt.
	((dolist (n-a (cdr *justification*))
	   (cond ((eq n-a node-to-ignore))
		 ((i-out? n-a) (return T)))))
	(node-to-ignore
	 (dolist (e envs)
	   (weaving-for-false-c012 (cdr *justification*) e node-to-ignore)))
	(t (weaving-for-false-c012 (cdr *justification*) *empty-env* nil))))

;;;****** The 2-union-env could be fixed here.  We could do this depth first after all.
;;; consing up the doubles is easy.
(defun weaving-for-false-c012 (nodes env node-to-ignore &aux envs)
  (prog ()
    loop
       (cond ((env-contradictory env))
	     ((null nodes)
	      (contradictory-env env
				 (cons 'BASE (cons 'WEAVING-FOR-FALSE *justification*))))
	     ((or (null (cdr nodes))
		  (and (null (cddr nodes)) (eq (cadr nodes) node-to-ignore)))
	      (if (unions-for-false-c012 env (n-a-envs (car nodes)) *justification*)
		  (return nil)))
	     ((eq (car nodes) node-to-ignore)
	      (setq nodes (cdr nodes) node-to-ignore nil)
	      (go loop))
	     ((cdr (setq envs (n-a-envs (car nodes))))
	      (dolist (e envs)
		(weaving-for-false-c012 (cdr nodes) (2-union-env env e) node-to-ignore)
		(if (env-contradictory env) (return nil))))
	     (t (setq env (2-union-env env (car envs))
		      nodes (cdr nodes))
		(go loop)))))

(defun unions-for-false-c012 (env envs reason)
  (cond ((env-contradictory env))
	((memq env envs) (contradictory-env env `(BASE UNIONS-FOR-FALSE-C012 ,reason)) T)
	((eq *empty-env* env)
	 (print "Should be optimized out earlier")
	 (dolist (e envs) (contradictory-env e `(BASE UNIONS-FOR-FALSE-C012 ,reason)))
	 nil)
	((eq (car envs) *empty-env*)
	 (print "Should be optimized out")
	 (contradictory-env env `(BASE UNIONS-FOR-FALSE-C012 ,reason))
	 T)
	((= (env-count env) 1)
	 (dolist (e envs)
	   (cond ((null e))
		 ((env-contradictory e))
		 ((= (env-count e) 1)
		  (double-for-false
		    (car (env-assumptions e)) (car (env-assumptions env)) reason)
		  (if (env-contradictory env) (return T)))
		 ((vector-member (car (env-assumptions env)) (env-vector e))
		  (contradictory-env env `(BASE UNIONS-FOR-FALSE-C012 ,reason))
		  (if (env-contradictory env) (return T))))))
	(t (dolist (e envs)
	     (cond ((null e))
		   ((env-contradictory e))
		   ((= (env-count e) 1)
		    (when (vector-member (car (env-assumptions e)) (env-vector env))
		      (contradictory-env env `(BASE UNIONS-FOR-FALSE-C012 ,reason))
		      (return T)))
		   ((vector-subset (env-vector env) (env-vector e))
		    (contradictory-env env `(BASE UNIONS-FOR-FALSE-C012 ,reason))))))))

;;; This weaver only bothers to return new 0, 1, 2 size environments.  
(defun general-weave-c012 (known-envs new-partial-envs consequent
			   &optional (node-to-ignore 'IGNORE) &aux new-new-partial-envs)
  (cond ((equal *empty-env-list* known-envs) nil)
	((dolist (n-a consequent)
	   (and (neq n-a node-to-ignore) (i-out? n-a) (return T)))
	 nil)
	(t (dolist (new-env new-partial-envs)
	     (cond ((null new-env))
		   ((env-contradictory new-env))
		   ((> (env-count new-env) 2.))
		   ((dolist (known known-envs)
		      (if (subset-env? known new-env) (return T))))
		   (t (push new-env new-new-partial-envs))))
	   (if new-new-partial-envs
	       (nweave-c012 consequent new-new-partial-envs node-to-ignore known-envs)))))

(defun nweave-c012 (nodes-to-process partial-envs node-to-ignore known-envs
		    &aux npartial-envs)
  ;; Try to handle the extremely simple common case where everything is a singleton,
  ;; and dispatch back to the general case if you lose.
  ;; *** we could have many difference versions of nweave-. for each case.
  ;; *** no need to return to the general general case.
  ;; *** if the general case reduces envs to one env, it could dispatch
  ;; *** to the easy case.
  (cond ((and (null known-envs) (null (cdr partial-envs)))
	 (nweave-simple-c012 nodes-to-process (car partial-envs) node-to-ignore))
	((equal partial-envs *empty-env-list*);;********** be much better.
	 (do ((nodes-to-process nodes-to-process (cdr nodes-to-process)))
	     ((null nodes-to-process) partial-envs)
	   (cond ((i-true? (car nodes-to-process)))
		 ((eq (car nodes-to-process) node-to-ignore))
		 (t (setq npartial-envs (fcopylist (n-a-envs (car nodes-to-process))))
		    (if npartial-envs
			(return (weave1-c012 (cdr nodes-to-process) npartial-envs
					node-to-ignore known-envs))
			(return nil))))))
	(t (weave1-c012 nodes-to-process partial-envs node-to-ignore known-envs))))

(defun nweave-simple-c012 (nodes-to-process env node-to-ignore
			   &aux node nenv env1 env2 envs comp last-nil oenvs)
  (do ((nodes-to-process nodes-to-process (cdr nodes-to-process)))
      ;; We could with crockery save this cons.
      ((null nodes-to-process) (list env))
    ;; If the node is to be ignored, ignore it.
    (unless (eq node-to-ignore (setq node (car nodes-to-process)))
      (setq nenv (car (n-a-envs node)))
      (cond ;; If the node is true, it contributes nothing.
	    ((eq nenv *empty-env*))
	    ;; If the next node has a simple label, its easy.
 	    ((null (cdr (n-a-envs node)))
	     (setq env (2-union-env env nenv))
	     (if (env-contradictory env) (return nil)))
	    ;; Here things get slightly dicey.  Lets hope that only one of the
	    ;; envs we have to construct survive.
	    (t (dolist (nenv (n-a-envs node))
		 (setq env1 (2-union-env env nenv))
		 (cond ;; If the result is contradictory we are in luck.
		       ((env-contradictory env1))
		       ;; If we haven't got any consistent envs yet, we are in luck.
		       ((null env2) (setq env2 env1))
		       ;; Things are not hopless yet, they might compare.
		       ((setq comp (compare-env env1 env2))
			(selectq comp
			  (EQUAL) ;;Damn Cl.
			  (SUBSET21)
			  (SUBSET12 (setq env2 env1))))
		       ;; The screw case, things are no longer simple.  We just have
		       ;; to byte the bullet and finish our work, and then trap
		       ;; out to the general case again.
		       ((null envs) (setq envs (list env1 env2)))
		       ;; We have to check for subsumption, in the usual way.
		       ;; Same old theorems apply.
		       (t (setq oenvs envs last-nil nil)
			  (do ((envs envs (cdr envs)))
			      ((null envs)
			       (if last-nil
				   (rplaca last-nil env1)
				   (push env1 oenvs)))
			    (cond ((null (car envs)) (setq last-nil envs))
				  (t (selectq (compare-env env1 (car envs))
				       ;; If the label is minimal, you could not have hacked
				       ;; envs at all yet.  This env does nothing.
				       (EQUAL (return))
				       (SUBSET12 (rplaca envs env1)
						 (do ((envs (cdr envs) (cdr envs)))
						     ((null envs))
						   ;; Can't find yourself if label was min.
						   (when (and (car envs)
						       (proper-subset-env? env1 (car envs)))
						     (rplaca envs nil)
						     (setq last-nil envs)))
						 (when last-nil
						   (fdelqa nil oenvs)
						   (unless (cdr oenvs)
						     (setq env2 (car oenvs) oenvs nil)
						   (return))))
				       (SUBSET21 (return))))))
			  (setq envs oenvs))))
	       ;; If envs is non-nil at this point, we have lost and can't use
	       ;; the simple approach any more: There is more than one env in the
	       ;; label so far.  Thus, we dispatch back to the general case.
	       (cond ((null envs) (if env2 (setq env env2 env2 nil) (return nil)))
		     ;; We don't have to do the general case if no nodes left.
		     ((or (null (cdr nodes-to-process))
			  (and (null (cddr nodes-to-process))
			       (eq (cadr nodes-to-process) node-to-ignore)))
		      (return envs))
		     (t (return
			  (nweave (cdr nodes-to-process) envs node-to-ignore nil)))))))))

;;; This can be incredibly optimized.  This is actually somewhat stupid.

(defun weave1-c012 (nodes-to-process partial-envs node-to-ignore known-envs
	       &aux new-env npartial-envs flag new)
  (dolist (node nodes-to-process)
    (setq npartial-envs nil)
    (cond ((eq node node-to-ignore))
	  ((i-true? node))
	  ;; If the label has exactly one environment, cross product is simpler.
	  ((null (cdr (n-a-envs node)))
	   (setq new nil)
	   ;; This loop updates the partial-envs list in place.  This works because the
	   ;; new partial-envs can't be any bigger than the original one.
	   ;;**** there will be so few, so why bother*** producing a copy?
	   (do ((penv partial-envs (cdr penv)))
	       ((null penv))
	     (cond ((null (car penv)))
		   ((or (env-contradictory (car penv)) (> (env-count (car penv)) 2.))
		    (rplaca penv nil))
		   ;; If the new union is inconsistent, delete it from the partial result.
		   ((env-contradictory
		      (setq new-env (2-union-env (car penv) (car (n-a-envs node)))))
		    (rplaca penv nil))
		   ;; If the new union is subsumed by what is already known, forget it.
		   ((dolist (known-env known-envs)
		      (if (subset-env? known-env new-env) (return T)))
		    (rplaca penv nil))
		   ;; Otherwise, scan the updated prefix of partial-envs.  When you
		   ;; find old self, replace it with your new self.
		   (t (setq flag nil)
		      (do ((penvs partial-envs (cdr penvs)))
			  ((eq penvs penv) (setq new T) (rplaca penvs new-env))
			(cond ((null (car penvs)))
			      ;; This is based on the theorem that if the prefix is
			      ;; always minimal, then if you have found an element prefix
			      ;; which you subsume, you cannot find yourself, nor any
			      ;; element which subsumes you.
			      (flag (if (subset-env? new-env (car penvs))
					(rplaca penvs nil)))
			      ;; Scan the prefix, to ensure that minimality is
			      ;; maintained.  If you ever find an element you subsume,
			      ;; then the much easier previous check is faster.
			      (t (selectq (compare-env new-env (car penvs))
				   ;; If you find yourself.  By minimality don't look
				   ;; further.  But get rid of the duplicate.  
				   ;; Note that new should have been set by now.
				   (EQUAL (rplaca penv nil) (return))
				   ;; If you find an earlier element which you 
				   ;; subsume, delete it.  
				   ;; By minimality you won't find yourself,
				   ;; or something that subsumes you.  
				   (SUBSET12 (rplaca penvs nil) (setq flag T))
				   ;; If you find something that subsumes you, forget about
				   ;; yourself.
				   (SUBSET21 (rplaca penv nil) (return)))))))))
	   ;; new is T, unless partial-envs is totally nil.
	   (unless new (setq partial-envs nil) (return)))
	  ;;***** does the following have the same bug as yourself?
	  ;; ******* 99% of the calls to union happen right here ******
	  (T (dolist (env (n-a-envs node))
	       (dolist (penv partial-envs)
		 (unless (or (null penv)
			     (env-contradictory (setq new-env (2-union-env penv env)))
			     (dolist (known-env known-envs)
			       (if (subset-env? known-env new-env) (return T))))
		   (setq flag nil)	
		   (do ((penvs npartial-envs (cdr penvs)))
		       ((null penvs) (unless flag (push new-env npartial-envs)))
		     (cond ((null (car penvs)))
			   (flag (if (subset-env? new-env (car penvs))
				     (rplaca penvs nil)))
			   (t (selectq (compare-env new-env (car penvs))
				(EQUAL (return))
				(SUBSET12 (rplaca penvs new-env) (setq flag T))
				(SUBSET21 (return)))))))))
	     (setq partial-envs npartial-envs)
	     (unless npartial-envs (return nil)))))
  (fdelqa nil partial-envs))

(defmacro union-reason (reason)
  `(if *explain-flag*
       `(BASE UNION-FOR-FALSE ,,reason)
       `(BASE UNION-FOR-FALSE)))

;;; A specialization of union, when the result is going to be marked inconsistent.
;;; Changes to union-env should perculate to here.
(defun union-for-false (e1 e2 reason &aux count1 count2)
  (cond	((and *union-check*
	      (or (vector-intersection? (env-vector e1) (car (env-cons-env-cache e2)))
		  (vector-intersection? (env-vector e2) (car (env-cons-env-cache e1))))))
	((env-contradictory e1))
	((env-contradictory e2))
	((eq e1 e2) (contradictory-env e1 (union-reason reason)))
	((eq e1 *empty-env*) (contradictory-env e2 (union-reason reason)))
	((eq e2 *empty-env*) (contradictory-env e1 (union-reason reason)))
	((= (setq count1 (env-count e1)) 1)
	 (cons-for-false e2 (car (env-assumptions e1)) reason))
	((= (setq count2 (env-count e2)) 1)
	 (cons-for-false e1 (car (env-assumptions e2)) reason))
	;; We could optimize cons-env now****
	;; If complete only one of these tests should be sufficient.

	((if (< count1 count2)
	     (if (vector-subset (env-vector e1) (env-vector e2))
		 (contradictory-env e2 (union-reason reason)))
	     (if (< count2 count1)
		 (if (vector-subset (env-vector e2) (env-vector e1))
		     (contradictory-env e1 (union-reason reason))))))
	;; *** if union-check is enabled this maybe should cache.  But it never returns
	;; T why?
	((not (compatible-env? e1 e2)))
	((union-for-false1 e1 e2 reason))))

;;; Designed really for external calls.
(defun user-general-weave (known-envs new-partial-envs antecedents
			   &optional (node-to-ignore 'IGNORE))
  (dolist (n-a antecedents)
    (cond ((eq n-a node-to-ignore))
	  ((i-out? n-a) (return-from USER-GENERAL-WEAVE known-envs))))
  (general-weave known-envs new-partial-envs antecedents))

;;; General-weave assumes it is not called with known-envs = *empty-env-list* because
;;; that should have been caught earlier.
;;; General weave assumes every antecedent is in, if not this should be trapped earlier.
(defun general-weave (known-envs new-partial-envs antecedents
		      &optional (node-to-ignore 'IGNORE) &aux new-envs flag)

  (cond ;; If any antecedent is known, punt.
	((and known-envs
	      (dolist (n-a antecedents)
		(cond ((eq n-a node-to-ignore))
		      ((known-in-all-envs? n-a known-envs) (return T)))))
	 known-envs)
			   
	;;; If we smash new-partial-envs what about cdr-coding.
	(t 
	   ;; Efficiency hack which may or may not help.  It saves an initial function
	   ;; call in many cases, and speeds up cases where antecedents are true.
	   ;; This strips off all leading true antecedents.
	   (do nil (nil)
	     (if (eq node-to-ignore (car antecedents)) (pop antecedents))
	     (cond ((and (eq (car new-partial-envs) *empty-env*) antecedents)
		    (setq new-partial-envs (n-a-envs (car antecedents)))
		    (pop antecedents))
		   (t (return nil))))

	   ;;****** We should optimize the case where antecedents are nil.

	   (setq new-partial-envs (fcopylist new-partial-envs))
	   ;; Remove the already known partial-envs.
	   (do ((env new-partial-envs (cdr env)))
	       ((null env))
	     (if (dolist (known known-envs) (if (subset-env? known (car env)) (return T)))
		 (rplaca env nil)
		 (setq flag T)))
	   (cond ((null flag) known-envs)
		 ((setq new-envs
			(nweave antecedents new-partial-envs node-to-ignore known-envs))
		  (setq known-envs (fcopylist known-envs))
		  (dolist (new-env new-envs)
		    (do ((known-env known-envs (cdr known-env)))
			((null known-env))
		      (and (car known-env)
			   (proper-subset-env? new-env (car known-env))
			   (rplaca known-env nil))))
		  (setq known-envs (nconc (fdelqa nil known-envs) new-envs))
		  (values known-envs new-envs))
		 (t known-envs)))))

;;; A version of general-weave specialized for weaving for false.  If this still
;;; takes a lot of time this can be optimized a lot more.
(defun weave-for-false (envs antecedents node-to-ignore &optional reason)
  (if *explain-flag* (push 'WEAVE-FOR-FALSE reason))
  (cond ;; If any antecedents are out, punt.
	((dolist (n-a antecedents)
	   (cond ((eq n-a node-to-ignore))
		 ((i-out? n-a) (return T)))))
	(node-to-ignore
	 (dolist (e envs)
	   (weaving-for-false antecedents e node-to-ignore reason)))
	(t (weaving-for-false antecedents *empty-env* nil reason))))

;;; It is a theorem that nodes has at least two elements initially.  This goes way out
;;; of its way to avoid calling union-env.  **** The changes here could perculate
;;; to the -c012 version.
;;;**** Changed added 6/23/88 which -c012 doesn't have either: a future node might
;;; become out, that wasn't checked for.  It happens in (dn-queens 4 t) with
;;; *resolve-by-ordered-labeling*.  Some day when optimizing, remove the out? check
;;; and see what actually is causing the problem.
;;; **** unfortunately the above doesn't happen anymore because I changed ADDB so there
;;; may be a bug lurking here.
(defun weaving-for-false (nodes env node-to-ignore reason &aux next-nodes flag envs)
  ;; Punt if we can't do anything interesting.
  (if (env-contradictory env) (return-from WEAVING-FOR-FALSE nil))
  (prog ()
	start
	;; Skip to the first node which can tell us anything.
	(do nil ((null nodes)
		 ;; This can happen. (justify-node F x T T T) for example.
		 (contradictory-env env `(BASE WEAVING-FOR-FALSE))
		 ;,*justification*))
		 (return-from WEAVING-FOR-FALSE nil))
	  (cond ((i-true? (car nodes)))
		((eq (car nodes) node-to-ignore) (setq node-to-ignore nil))
		;**?? Optimize this case somehow.
		((i-out? (car nodes)) (return-from WEAVING-FOR-FALSE nil))
		(t (return nil)))
	  (setq nodes (cdr nodes)))
	(cond ((neq env *empty-env*))
	      ((null (cdr (n-a-envs (car nodes))))
	       (setq env (car (n-a-envs (car nodes))) nodes (cdr nodes))
	       (go start))
	      (t ;;****** also on the last e, why don't we 
		 (dolist (e (n-a-envs (car nodes)))
		   ;;*** sound, but not optimal.  I added the following kludge, but
		   ;;needs to be thought about.  Really we should check whether e
                   ;; is still part of the label.  We could do a complex check to make
		   ;; sure e is still in the label.****** If a deletion happens
		   ;; **** is the envs updated?????*************
		   ;; **** occurs only with nogood resolution.
		   ;;*** in general after every call to weaving for false we need to
		   ;; to check the envs and nodes we have in or hands.
;		   (if (memq e (n-a-envs (car nodes)))
		       (weaving-for-false (cdr nodes) e node-to-ignore reason))
		 (return-from WEAVING-FOR-FALSE nil)))
	;; Now we have a non-empty env, and nodes starting with something interesting.
	(setq next-nodes (cdr nodes))
	loop
	(do nil ((null next-nodes)
		 (unions-for-false env (n-a-envs (car nodes))
				   (if *explain-flag*
				       `(WEAVING-FOR-FALSE
					  ,nodes ,env ,node-to-ignore ,reason)
				       '(WEAVING-FOR-FALSE)))
		 ;*justification*)
		 (return-from WEAVING-FOR-FALSE nil))
	  (cond ((i-true? (car next-nodes)))
		((eq (car next-nodes) node-to-ignore) (setq node-to-ignore nil))
		;;**** check this earlier.
		((i-out? (car next-nodes)) (return-from WEAVING-FOR-FALSE nil))
		(t (return nil)))
	  (setq next-nodes (cdr next-nodes)))
	;; Now we are in a situation where we have a non-empty env, and two interesing nodes.
	;; We will have no choice but to do a real union-env.  Lets hope next-nodes is a
	;; singleton.
	(when (null (cdr (n-a-envs (car next-nodes))))
	  (setq env (union-env env (car (n-a-envs (car next-nodes)))))
	  (if (env-contradictory env) (return-from WEAVING-FOR-FALSE nil))
	  (setq next-nodes (cdr next-nodes))
	  (go loop))
	;; env is not empty, neither nodes or next-envs is a singleton.  
	(setq flag nil envs nil)
	(dolist (e (n-a-envs (car nodes)))
	  (unless (or (env-contradictory (setq e (union-env env e)))
		      (and flag (eq e env))
		      (memq e envs))
	    (if (eq e env) (setq flag T) (push e envs))
	    (weaving-for-false next-nodes e node-to-ignore reason)
	    (if (env-contradictory env) (return-from WEAVING-FOR-FALSE nil))))))

;;; Try to be clever if everything is true.
;;; **** known-envs hack.

(defun nweave (nodes-to-process partial-envs node-to-ignore known-envs &aux npartial-envs)
  ;; Try to handle the extremely simple common case where everything is a singleton,
  ;; and dispatch back to the general case if you lose.
  ;; *** we could have many difference versions of nweave-. for each case.
  ;; *** no need to return to the general general case.
  ;; *** if the general case reduces envs to one env, it could dispatch
  ;; *** to the easy case.
  (cond ((and (null known-envs) (null (cdr partial-envs)))
	 (nweave-simple nodes-to-process (car partial-envs) node-to-ignore))
	((eq (car partial-envs) *empty-env*)
	 ;;****** This should be optimzed away, because this can now only ooccur
	 ;;****** If nodes-to-process is nil.
	 (do ((nodes-to-process nodes-to-process (cdr nodes-to-process)))
	     ((null nodes-to-process) partial-envs)
	   (cond ((i-true? (car nodes-to-process)))
		 ((eq (car nodes-to-process) node-to-ignore))
		 (t (setq npartial-envs (fcopylist (n-a-envs (car nodes-to-process))))
		    ;;*** remove subsets function.
		    (when known-envs
		      (do ((tenv npartial-envs (cdr tenv)))
			  ((null tenv))
			(if (dolist (known known-envs)
			      (if (subset-env? known (car tenv)) (return T)))
			    (rplaca tenv nil)))
		      (setq npartial-envs (fdelqa nil npartial-envs)))
		    (if npartial-envs
			(return (weave1 (cdr nodes-to-process) npartial-envs
					node-to-ignore known-envs))
			(return nil))))))
	(t (weave1 nodes-to-process partial-envs node-to-ignore known-envs))))

(defun weave1 (nodes-to-process partial-envs node-to-ignore known-envs
	       &aux new-env npartial-envs flag)
;  (push (cons (length partial-envs) (mapcar #'(lambda (n)
;  (declare (sys:downward-function))
;						(if (neq node-to-ignore n) (length (n-a-envs n))))
;					    nodes-to-process))
;	foo)

  (dolist (node nodes-to-process)
    (setq npartial-envs nil)
    (cond ((eq node node-to-ignore))
	  ((i-true? node))
	  ;; If the label has exactly one environment, cross product is simpler.
	  ((null (cdr (n-a-envs node)))
	   (setq partial-envs
		 (weave-single-env (car (n-a-envs node)) known-envs partial-envs))
	   (unless partial-envs (return nil)))
	  ((null (cdr partial-envs))
	   (setq partial-envs
		 (safe-weave-single-env (car partial-envs) known-envs (n-a-envs node)))
	   (unless partial-envs (return nil)))
	  ;;***** does the following have the same bug as yourself?
	  ;; ******* 99% of the calls to union happen right here ******
	  (T (dolist (env (n-a-envs node))
	       (dolist (penv partial-envs)
		 (unless (or (null penv)
			     (env-contradictory (setq new-env
						       (union-env3 known-envs penv env))))
		   (setq flag nil)	
		   (do ((penvs npartial-envs (cdr penvs)))
		       ((null penvs) (unless flag (push new-env npartial-envs)))
		     (cond ((null (car penvs)))
			   (flag (if (subset-env? new-env (car penvs))
				     (rplaca penvs nil)))
			   (t (selectq (compare-env new-env (car penvs))
				(EQUAL (return))
				(SUBSET12 (rplaca penvs new-env) (setq flag T))
				(SUBSET21 (return)))))))))
	     (setq partial-envs npartial-envs)
	     (unless npartial-envs (return nil)))))
  (fdelqa nil partial-envs))

;;; If much time is spent here, make a version of weave-single-env which wins here.
(defun safe-weave-single-env (env known-envs partial-envs &aux safe-partial-envs)
  (dolist (penv partial-envs)
    (unless (dolist (known known-envs) (if (subset-env? known penv) (return T)))
      (push penv safe-partial-envs)))
  (weave-single-env env known-envs safe-partial-envs))

;; This loop updates the partial-envs list in place.  This works because the
;; new partial-envs can't be any bigger than the original one.
(defun old-weave-single-env (env known-envs partial-envs &aux new-env flag new)
  (do ((penv partial-envs (cdr penv)))
      ((null penv))
    (cond ((null (car penv)))
	  ;; If the new union is inconsistent, delete it from the partial result.
	  ((env-contradictory
	     (setq new-env (union-env3 known-envs (car penv) env)))
	   (rplaca penv nil))
	  ;; Otherwise, scan the updated prefix of partial-envs.  When you
	  ;; find old self, replace it with your new self.
	  (t (setq flag nil)
	     (do ((penvs partial-envs (cdr penvs)))
		 ((eq penvs penv) (setq new T) (rplaca penvs new-env))
	       (cond ((null (car penvs)))
		     ;; This is based on the theorem that if the prefix is
		     ;; always minimal, then if you have found an element prefix
		     ;; which you subsume, you cannot find yourself, nor any
		     ;; element which subsumes you.
		     (flag (if (subset-env? new-env (car penvs))
			       (rplaca penvs nil)))
		     ;; Scan the prefix, to ensure that minimality is
		     ;; maintained.  If you ever find an element you subsume,
		     ;; then the much easier previous check is faster.
		     (t (selectq (compare-env new-env (car penvs))
			  ;; If you find yourself.  By minimality don't look
			  ;; further.  But get rid of the duplicate.  
			  ;; Note that new should have been set by now.
			  (EQUAL (rplaca penv nil) (return))
			  ;; If you find an earlier element which you 
			  ;; subsume, delete it.  
			  ;; By minimality you won't find yourself,
			  ;; or something that subsumes you.  
			  (SUBSET12 (rplaca penvs nil) (setq flag T))
			  ;; If you find something that subsumes you, forget about
			  ;; yourself.
			  (SUBSET21 (rplaca penv nil) (return)))))))))
  ;; new is T, unless partial-envs is totally nil.
  (unless new (setq partial-envs nil))
  partial-envs)

;;; ***** idea if union-env3 result here is a subset only check for eq?

(defun weave-single-env (env known-envs partial-envs)
  (dolist (penv partial-envs)
    (when (and penv (subset-env? penv env))
      (dolist (known known-envs)
	(if (subset-env? known env)
	    (return-from WEAVE-SINGLE-ENV nil)))
      (return-from WEAVE-SINGLE-ENV (list env))))
  (cond ((= (env-count env) 1)
	 (new-weave-assumption (car (env-assumptions env)) known-envs partial-envs))
	(t (old-weave-single-env env known-envs partial-envs))))

;;; Prefix always contained assumption.
(defun new-weave-assumption (assumption known-envs partial-envs &aux non new last-non new-env)
  (do ((penv partial-envs (cdr penv))
       (ppenv nil (if recycle ppenv penv))
       (recycle nil nil))
      ((null penv)
       (cond ((null new) nil)
	     (non (rplacd last-non partial-envs) non)
	     (t partial-envs)))
    (cond ((null (car penv)))
	  ((vector-member assumption (env-vector (car penv)))
	   (setq new T)
	   (do ((non non (cdr non)))
	       ((null non))
	     (and (car non)
		  (subset-env? (car non) (car penv))
		  (rplaca non nil))
	     (if (eq last-non non) (return nil))))
	  ((or (env-contradictory (setq new-env (cons-env (car penv) assumption)))
	       (dolist (known known-envs) (if (subset-env? known new-env) (return T))))
	   (rplaca penv nil))
	  ;; Now we have another non, its prime with respect to other nons, but
	  ;; it might be a superset of the prefix.
	  (t (do ((penvs partial-envs (cdr penvs)))
		 ((eq penvs penv)
		  (setq new T)
		  (cond (last-non (rplacd last-non penv)
				  (setq last-non penv))
			(t (setq non penv last-non penv)))
		  (setq recycle T)
		  (if ppenv (rplacd ppenv (cdr penv)) (setq partial-envs (cdr penv)))
		  (rplaca last-non new-env)
		  )
	       (when (and (car penvs) (subset-env? (car penvs) new-env))
		 (rplaca penv nil)
		 (return nil)))))))

;;; creates a set of environments by conjoining all the environments of the nodes-to-process
;;; along with the new-partial-environment and adds these to *new-envs*
;;; This tries to be efficient.***** be cleverer about partial-envs.

;;; This handles the simple case of weaving where there are no known-envs, and
;;; all the antecedents have singleton environments.  This happens very commonly
;;; in justifications for the *contra-node*.
(defun nweave-simple (nodes-to-process env node-to-ignore
				       &aux node nenv env1 env2 envs comp last-nil oenvs)
  (do ((nodes-to-process nodes-to-process (cdr nodes-to-process)))
      ;; We could with crockery save this cons.
      ((null nodes-to-process) (list env))
    ;; If the node is to be ignored, ignore it.
    (unless (eq node-to-ignore (setq node (car nodes-to-process)))
      (setq nenv (car (n-a-envs node)))
      (cond ;; If the node is true, it contributes nothing.
	    ((eq nenv *empty-env*))
	    ;; If the next node has a simple label, its easy.
 	    ((null (cdr (n-a-envs node)))
	     (setq env (union-env env nenv))
	     (if (env-contradictory env) (return nil)))
	    ;; Here things get slightly dicey.  Lets hope that only one of the
	    ;; envs we have to construct survive.
	    (t (dolist (nenv (n-a-envs node))
		 (setq env1 (union-env env nenv))
		 (cond ;; If the result is contradictory we are in luck.
		       ((env-contradictory env1))
		       ;; If we haven't got any consistent envs yet, we are in luck.
		       ((null env2) (setq env2 env1))
		       ;; Things are not hopless yet, they might compare.
		       ((and (null envs) (setq comp (compare-env env1 env2)))
			(selectq comp
			  (EQUAL) ;;Damn Cl.
			  (SUBSET21)
			  (SUBSET12 (setq env2 env1))))
		       ;; The screw case, things are no longer simple.  We just have
		       ;; to byte the bullet and finish our work, and then trap
		       ;; out to the general case again.
		       ((null envs) (setq envs (list env1 env2)))
		       ;; We have to check for subsumption, in the usual way.
		       ;; Same old theorems apply.
		       (t (setq oenvs envs last-nil nil)
			  (do ((envs envs (cdr envs)))
			      ((null envs)
			       (if last-nil
				   (rplaca last-nil env1)
				   (push env1 oenvs)))
			    (cond ((null (car envs)) (setq last-nil envs))
				  (t (selectq (compare-env env1 (car envs))
				       ;; If the label is minimal, you could not have hacked
				       ;; envs at all yet.  This env does nothing.
				       (EQUAL (return))
				       (SUBSET12 (rplaca envs env1)
						 (do ((envs (cdr envs) (cdr envs)))
						     ((null envs))
						   ;; Can't find yourself if label was min.
						   (when (and (car envs)
						       (proper-subset-env? env1 (car envs)))
						     (rplaca envs nil)
						     (setq last-nil envs)))
						 (when last-nil
						   (fdelqa nil oenvs)
						   (unless (cdr oenvs)
						     (setq env2 (car oenvs) oenvs nil)
						   (return))))
				       (SUBSET21 (return))))))
			  (setq envs oenvs))))
	       ;; If envs is non-nil at this point, we have lost and can't use
	       ;; the simple approach any more: There is more than one env in the
	       ;; label so far.  Thus, we dispatch back to the general case.
	       (cond ((null envs) (if env2 (setq env env2 env2 nil) (return nil)))
		     ;; We don't have to do the general case if no nodes left.
		     ((dolist (node (cdr nodes-to-process) T)
			(cond ((eq node node-to-ignore))
			      ((true? node))
			      (t (return nil))))
		      (return envs))
		     (t (return
			  (nweave (cdr nodes-to-process) envs node-to-ignore nil)))))))))

;;; Replace the nodes envs with a new set.  If the status changes, and we care, i.e., there
;;; are pending rules on the node, start building a pending queue.  Due to the
;;; large number of bugs, this makes sure that the changed envs are really useful.

;;; Returns T if santization is required....not anymore.

;;; The case of new-envs = empty-env could be optimized.****
(defun change-node-envs (node new-envs &aux old-envs out-informative in-informative)
  ;;**** why doesn't this first option return T if contradictory environments are discoverd?
  (cond ((n-a-contradictory node)
	 ;;*** we have to have a carefull flag or something to leave this behind.
	 (contradictory-envs new-envs
			     '(BASE LABEL-FOR-FALSE2)))
;			     (list 'BASE
;				   'LABEL-FOR-FALSE2
;				   node new-envs
;				   justification
;				   (mapcar #'(lambda (n-a) (fcopylist (n-a-envs n-a)))
;					   (cddr justification))))
	
	(t (setq old-envs (n-a-envs node))
	   (setf (n-a-envs node) new-envs)
	   ;; For debugging, remove sometime for efficiency reasons.
	   (and *simple-hybrid* (cdr new-envs) (error "Multiple label update!?"))

	   ;; If an env goes away, unwire the node.
	   (dolist (old-env old-envs)
	     (unless (or (memq old-env new-envs) (env-contradictory old-env))
	       (setq out-informative T)
	       (setf (env-nodes old-env) (fdelq1 node (env-nodes old-env)))))
	   ;; If a new-env comes in, wire the node.
	   (dolist (new-env new-envs)
	     (unless (memq new-env old-envs)
	       (setq in-informative T)
	       (incf *update-counter*)
	       ;; Don't bother keeping two-way pointers for envs.
	       (unless (eq new-env *empty-env*)
		 (push node (env-nodes new-env)))))
	   ;; **** make more efficient by just saving the cons.****
	   (unless (or in-informative out-informative (eq (car new-envs) *empty-env*))
	     (error "Uninformative node update"))
	   (when in-informative
	     ;; We may have to queue these at a higher level sometime, because some of the
	     ;; labeling algorithm may depend on labels not changing below it, and
	     ;; hence have a queue just like *going-nodes*.
	     (if (eq (car new-envs) *empty-env*) (new-true-node node))
	     (dolist (c (n-a-env-consumers node)) (add-node-consumer-to-node c node))
	     (setf (n-a-env-consumers node) nil))
	   (cond (old-envs (cond ((null new-envs) (out-node node))
				 ((and (n-a-enqueued? node) in-informative)
				  (enqueue-node node))
				 ))
		 (new-envs 
		  (setf (n-a-status node)
			(if (n-a-has-consumers? node)
			    (selectq (n-a-status node)
			      (GOING-OUT 'STAYING-IN)
			      (STAYING-OUT 'GOING-IN)
			      (OUT (push node *going-nodes*) 'GOING-IN)
			      ((IN GOING-IN STAYING-IN)
			       (error "Consumer node was already ~A?" (n-a-status node)))
			      (T (error "Impossible node status ~A"	
					(n-a-status node))))
			    'IN))))))

  nil)

;;; Tell the TMS that the given node is contradictory.
(defun contradictory-node (node reason &aux *going-nodes*)
  (unless (n-a-contradictory node)
    (propagate-false node reason)
    (if *going-nodes* (process-changed-nodes))))

;;; This propagates TRUE/FALSE through the entire network without doing any label
;;; updating in between at all.  Assuming this runs underneath *going-nodes*.
(defvar *set-nodes* nil)

(defun new-true-node (node)
  (let ((*set-nodes* nil))
    (propagate-true-2 node)
    (set-nodes)))

(defun propagate-true (node)
  (let ((*set-nodes* nil))
    (propagate-true-1 node)
    (set-nodes)))

(defun propagate-false (node reason)
  (let ((*set-nodes* nil))
    (propagate-false-1 node reason)
    (set-nodes)))

(defun contradictory-just (justification &aux *set-nodes*)
  (contradictory-just-1 justification)
  (set-nodes))

;;; Not optimized for assumptions being set at all.  This is very wierd and needs more thought,
;;; the envs data structure will be a bit inconsistent until set-nodes finishes.
;;; Also, *set-nodes* should be a set of symbols, and not nodes.
(defun set-nodes ()
  (dolist (n *set-nodes*)
    (when (n-a-contradictory n)
      (if *simple-hybrid*
	  ;; This is basically a judgement call decision.  After all shouldn't the contradictory
	  ;; envs be detected when the environment is made active?  In any case, if the node
	  ;; is an assumption you should *always* at least contradict the environment of the assumption.
	  (do nil ((null (n-a-blocked n)))
	    (contradictory-env (car (n-a-blocked n))
			       (if *explain-flag* `(BASE SET-NODES ,n)
				   '(BASE SET-NODES))))
	  (do nil ((null (n-a-envs n)))
	    (contradictory-env (car (n-a-envs n))
			       (if *explain-flag* `(BASE SET-NODES ,n)
				   '(BASE SET-NODES))))
	  )))
  (dolist (n *set-nodes*)
    (unless (n-a-contradictory n)
      ;;**** there is no direct way of making this work****.
      ;;**** the label update algorithm may have to look at the same *empty-env* multiple times.
      (if *simple-hybrid*
	  (update-node-real-hybrid-safe n *empty-env*)
	  (update-node1 n *empty-env-list* *empty-env-list*)))))

(defun propagate-true-1 (node)
  (if (n-a-contradictory node) (throw 'CONTRADICTION 'FAIL))
  (unless (i-true? node)
    (push node *set-nodes*)
    ;;;;******* THIS TOTALLY SCREWS UP (env-nodes ...****.
    (setf (n-a-envs node) *empty-env-list*)
    (if *simple-hybrid* (setf (n-a-blocked node) *empty-env-list*))
    (propagate-true-2 node)))

;;; This is called when a node gets an empty environment.  If the node participates in
;;; a justification for false, false might be back propagatable.  Again, I don't know
;;; whether this is worth it.

(defun propagate-true-2 (node)
  (when (n-a-neg node) (propagate-false-1 (n-a-neg node) 'NEGATION-IS-TRUE))
  (when (assumption? node)
    ;; Remove all assumption disjunctions mentioning it.
    (dolist (or (assumption-ors node))
      (excise-or or)
      ;;*** perhaps this should be thought about some more.  
      (setf (disjunction-satisfied or) T)))
  (dolist (class (n-a-classes node))
    (when (class-exclusive class)
      (dolist (other (class-nodes class))
	(unless (eq other node)
	  (propagate-false-1 other class)))))
  (dolist (c (n-a-consequents node))
    (if (n-a-contradictory (just-consequent c))
	(contradictory-just-1 c)))
  (dolist (c (n-a-nclauses node)) (propagate-clause node c)))

(defun propagate-false-1 (node reason &aux open)
  (if (i-true? node) (throw 'CONTRADICTION 'FAIL))
  (unless (n-a-contradictory node)
    (setf (n-a-contradictory node) (if *explain-flag* (cons 'PROPAGATE-FALSE-1 reason)
					'(PROPAGATE-FALSE-1)))
;;; The following code is (a) buggy (see pred-prey QPE example) because callers
;;; may hold node-justifications, (b) makes explanations hard.  if we
;;; ever want to re-install this for efficiency, rethink this.
;;; **** Did I remove the prechecks in the various weave procedures for contradictory
;;; nodes?
;;; Remove all useless justifications in which this node participates.
;;; Consequent looks like (node . justification)
;    (unless *ltms*
;      (dolist (cnsqnt (n-a-consequents node))
;	(setf (n-a-justifications (just-consequent cnsqnt))
;	      (fdelq1 cnsqnt (n-a-justifications (just-consequent cnsqnt))))
;	(dolist (antecedent (just-antecedents cnsqnt))
;	  (unless (eq node antecedent)
;	    (setf (n-a-consequents antecedent) (fdelq1 cnsqnt (n-a-consequents antecedent))))))
;      (setf (n-a-consequents node) nil))
    (push node *set-nodes*)
    (when (n-a-neg node) (propagate-true-1 (n-a-neg node)))
    (dolist (class (n-a-classes node))
      (when (class-oneof class)			; Redundant because clause is always there?
	(setq open nil)
	(dolist (node2 (class-nodes class) (if open (propagate-true-1 open)))
	  (cond ((i-false? node2))
		((i-true? node2))
		(open (return nil))
		(t (setq open node2))))))
    (dolist (j (n-a-justifications node)) (contradictory-just-1 j))
    (dolist (c (n-a-pclauses node)) (propagate-clause node c))
    (when (n-a-neg node)
      (dolist (c (n-a-nclauses (n-a-neg node))) (propagate-clause node c)))

    ))

;;; Given a justification for a contradictory node, this propagates it backwards.  This
;;; is incomplete as well, but it is an efficiency hack.  If the single antecedent is
;;; an assumption it should already be taken care of.
(defun contradictory-just-1 (just &aux only-supporter antecedents)
  (setq antecedents (just-antecedents just))
  (unless (dolist (supporter antecedents)
	    (cond ((i-true? supporter))
		  ((n-a-contradictory supporter) (return T))
		  (only-supporter (return T))
		  (t (setq only-supporter supporter))))
    (unless only-supporter
      (when *explain-flag*
	(format T "~% ~A => ~A, but consequent is false and antecedents true."
		antecedents
		(just-consequent just))
	(throw 'CONTRADICTION (explanation-for-justification just)))
      (throw 'CONTRADICTION 'FAIL))
    (propagate-false-1 only-supporter just)))

;;; This is incorrect if negatives don't exist.  WHICH THEY SOMETIMES DON'T FOR ASSUMPTIONS.
;;; ****
(defun propagate-clause (node clause &aux open)
  node
  ;; All negatives must be true, or nothing can be concluded.
  (dolist (n (first clause))
    (cond ((i-true? n))
	  (open (return-from PROPAGATE-CLAUSE nil))
	  (t (setq open n))))
  ;; We have an open negatively occuring literal.
  (dolist (p (second clause))
    (cond ((i-false? p))
	  (open (return-from PROPAGATE-CLAUSE nil))
	  (t (setq open p))))
  ;; We have an open literal, all other negatives are true, and all other positives are false,
  ;; so open MUST be true.
  (if (memq open (first clause))
      ;; Open literal occurs negatively, it must be false.
      (propagate-false-1 open clause)
      ;; Open literal occurs positively, it must be true.
      (propagate-true-1 open)))

;;; True-assumption is called when the ATMS discovers some disjunction of assumptons
;;; is reduced to a singleton.

;;; Peter Struss claims this is probably
;;; extremely inefficient.****************
;;; ******* rehasing should flush these from the table.
;;; ******** Also the justify-node will now detect the smaller nogoods.  In actual
;;; fact it may be possib
(defun true-assumption (assumption informant)
  ;; Make the assumption universally true.
  (justify-node assumption (list informant))
  ;; Mark its negation as false.
  ;; Soon to be obsolete I think.****
  (when (or *resolve-by-labeling* *resolve-by-ordered-labeling*)
    (if (assumption-negation assumption)
	(contradictory-node (assumption-negation assumption) '(TRUE-ASSUMPTION))))
  )