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

(in-package 'tms)

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

;;; This is the basic ATMS. (Section 2 of the ATMS paper.)

;;; However, it contains necessary hooks for the other sections.
   
;;; This works for CADRs, 3600s, and Explorers.

;;; Basic entry points are (be careful using functions other than those listed because
;;; they often don't do what you think they do (e.g., contradictory-just).

;;; (init flag).
;;;  Create a new ATMS.  flag indicates whether old structures should be reused.
;;;  Note only one ATMS can exist at a time right now (easily fixed --- just never
;;;  had a need for it.

;;; (create-node datum)
;;;  Returns a new node for datum with an empty label and no justifications.

;;; (justify-node node justification).
;;;  Adds justification to node.  Justification looks like (<informant> . <antecedents>).

;;; *contra-node* is false.

;;; Important external calls:
;;; (out-node node)
;;;  Notifies that the node is being forced out.

;;; Convenient auxilliary entry points.
;;; (assume-datum datum).
;;;  Returns a new node for datum with a singleton label and an assumption justification.

;;; (assume-node node).
;;;  Unless the node has already been assumed, it is given an assumption justification.

;;; (contradiction justification).
;;;  A justification for false.

;;; (contradictory antecedents)
;;;  The set of nodes/assumptions imply false.

;;; (contradictory-node node reason)
;;;  This node is itself contradictory.

;;; (true-in? node env)
;;;  Is node in the context of env.

;;; (consistent-in? node env)
;;;  Is node in the context of env or any of its supersets?

;;; (in? node)
;;;  Is node in any context at all.

;;; (true? node)
;;;  Does the node necessarily hold in every (conceivable) context.

;;; (false? node)
;;;  Is the node necessarily absent in from every (coneivable) context.

;;; (out? node)
;;;  Is the node in no context at all.

;;; (status-of-node node)
;;;  Equivalent to above, returns :TRUE,:IN,:OUT,:FALSE.

;;; (in-antecedent? node justification)
;;;  Is the justification for node doing any work?

;;; (implies a c) *** why not ?
;;;  Does the presence of a in a context imply the presence of c.

(defun create-node (datum)
  (prog1 (internal-create-node datum)
	 (if *trace-file* (format *trace-file* "~%C-N ~D" *node-counter*))))


;;; Create a node associated with the datum and assume it.
(defun assume-datum (datum &aux node)
  (setq node (create-node datum))
  (justify-node node (list 'ASSUME (make-a-assumption node ':IN)))
  node)
			      
;;; This makes a conventional node an assumed node, and not xor with any other.
(defun assume-node (node)
  (cond ((node-assumption node))
	(t (let* ((asn (make-a-assumption node :IN))
		  (env (assumption-env asn)))
	     ;; We have the convention that the n-a-blocked always contains everything.
	     (setf (n-a-blocked asn) (list env))
	     (if *simple-hybrid* (error "This does not honor simple-hybrid flag index-early"))
	     (index-env env (env-assumptions env))

	     (unless (in-focus? asn)
	       (setf (n-a-envs asn) nil))
	     (setf (assumption-node asn) node)
	     (justify-node node (list 'ASSUME asn))
	     asn))))

;;; This makes node an xor assumption under given class.
(defun assume-xor-node (node class &optional new &aux assumption)
  (setq assumption (node-assumption node))
  (cond (assumption
	 (if (neq (assumption-variable assumption) class)
	     (error "Not implemented --- it would be too slow."))
	 node)
	((not (memq class (n-a-classes node)))
	 (error "Can't assumething part of a class its not in"))
	(t (setq assumption (basic-make-assumption class node nil))
	   (setf (node-assumption node) assumption)
	   (add-xor-assumption-to-class assumption class new)
	   (justify-node node (list 'ASSUME-XOR-NODE assumption))
	   node)))

;;; Basic problem solving operation is to justify one node in terms of others.
;;; It does not return a useful value.

;;; This algorithm could stand a lot more thought if the functionality is right.
;;; Loops are ok because they have to die out.
;;; Note that the same node may be reexamined many times.
;;; Maybe there should be a breadth-first queue.

;;; A justification looks like (user-supplied-informant . antecedent-nodes).
(defun justify-node (node justification &optional dont-remove-duplicates
		     &aux *going-nodes* just j-consumers out clean n ptr (count 0))
  (incf *justification-count*)
  (when *trace-file*
      (format *trace-file* "~%J-N ")
      (trace-node node)
      (format *trace-file* "(")
      (mapc #'(lambda (n-a) (trace-node n-a)) (cdr justification))
      (format *trace-file* ")"))
  ;; If the consequent is true, chuck the justification.
  (if (i-true? node) (return-from JUSTIFY-NODE nil))

  ;; This immediately throws away justifications one of whose antecedents is false, or
  ;; which contain duplicate antecedent nodes.

  (do ((antecedents (cdr justification) (cdr antecedents)))
      ((null antecedents)
       (if clean (rplacd justification (fdelqa nil (cdr justification)))))
    (when (setq n (car antecedents))
      (if (i-false? n) (return-from JUSTIFY-NODE nil))
      (unless (n-a-envs n)
	(setq out T)
	(incf count))
      ;; Rare, so this optimizes the case where there are no duplicates.
      (or out dont-remove-duplicates
	  (when (setq ptr (memq n (cdr antecedents)))
	    (do nil (nil)
	      (unless (n-a-envs n) (decf count))
	      (rplaca ptr nil)
	      (unless (setq ptr (memq n (cdr ptr))) (setq clean T) (return nil)))))))

  ;;***** When focussing much of below is unecessary.
  (setq just (make-just :CONSEQUENT node
			:INFORMANT (car justification)
			:ANTECEDENTS (cdr justification)
			:COUNT count))

  (push just (n-a-justifications node))

  (dolist (antecedent (cdr justification)) (push just (n-a-consequents antecedent)))
  (cond ((n-a-contradictory node)
	 (contradictory-just just)
	 (weave-for-false nil (cdr justification) nil
			  (if *explain-flag* (cons 'JUSTIFY-NODE just)
			      '(JUSTIFY-NODE))))
	;; Because there might be justification consumers, don't exit here.
	(out)
	((and *foci* *simple-hybrid* (cdr justification))
	 (hybrid-justification just))
	(t (multiple-value-bind (known-envs new-envs)
	       (general-weave (n-a-envs node) *empty-env-list* (cdr justification))
	     (when new-envs (update-node1 node new-envs known-envs)))))
  (if *going-nodes* (process-changed-nodes))
  (when (setq j-consumers (n-a-justification-consumers node))
    (dolist (c j-consumers) (add-node-consumer-to-node c node))
    (setf (n-a-justification-consumers node) nil))
  )



;;; Really designed for external invocation.
;;; Like justify-node, but doesn't record anything.  Internal function only.
(defun user-simple-justify-node (node antecedents &optional reason)
  (error "how-could-this happen")

  (if *explain-flag* (push (list 'user-simple-justify-node node antecedents) reason))
  (dolist (n-a antecedents) (if (i-out? n-a) (return-from USER-SIMPLE-JUSTIFY-NODE nil)))
  (cond ((n-a-contradictory node)
	 ;; This will now get an error as contradictory-just-1 takes a justification
	 (contradictory-just-1 antecedents)
	 (weave-for-false nil antecedents nil reason))
	((i-true? node))
	(t (multiple-value-bind (known-envs new-envs)
	       (general-weave (n-a-envs node) *empty-env-list* antecedents)
	     (when new-envs (update-node1 node new-envs known-envs))))))

;;; Use if you know the justification is currently inactive.
(defun inactive-justify-node (node justification &aux *going-nodes* consequent clean ptr n)
  (incf *justification-count*)
  (when *trace-file*
      (format *trace-file* "~%IJ-N ")
      (trace-node node)
      (format *trace-file* "(")
      (mapc #'(lambda (n-a) (trace-node n-a)) (cdr justification))
      (format *trace-file* ")"))

  (if (i-true? node) (return-from INACTIVE-JUSTIFY-NODE nil))

  (do ((antecedents (cdr justification) (cdr antecedents)))
      ((null antecedents)
       (if clean (rplacd justification (fdelqa nil (cdr justification)))))
    (when (setq n (car antecedents))
      (if (i-false? n) (return-from INACTIVE-JUSTIFY-NODE nil))
      ;; Rare, so this optimizes the case where there are no duplicates.
      (when (setq ptr (memq n (cdr antecedents)))
	(do nil (nil)
	  (rplaca ptr nil)
	  (unless (setq ptr (memq n (cdr ptr))) (setq clean T) (return nil))))))
  (push justification (n-a-justifications node))
  (setq consequent (cons node justification))
  (dolist (antecedent (cdr justification))
    (push consequent (n-a-consequents antecedent)))
  (if (n-a-contradictory node) (contradictory-just-1 justification))
  ;; *** if this pans out, do it more efficiently.
  (dolist (c (n-a-justification-consumers node))
    (add-node-consumer-to-node c node))
  (setf (n-a-justification-consumers node) nil))

(defun contradictory (set) (contradiction (cons 'CONTRADICTORY set)))

(defun contradiction (just) (justify-node *contra-node* just))

;;; Designed for used by user.
(defun add-envs (node envs &aux *going-nodes*)
  (if (i-true? node) (return-from ADD-ENVS nil))
  (cond ((n-a-contradictory node)
	 (contradictory-envs envs '(ADD-ENVS)))
	(t (multiple-value-bind (known-envs new-envs)
	       (general-weave (n-a-envs node) envs nil)
	     (when new-envs (update-node1 node new-envs known-envs)))))
  (if *going-nodes* (process-changed-nodes))
  )

;;; Never bother dequeuing as run will dequeue out things automatically.
(defun process-changed-nodes (&aux node)
  (do () (nil)
    (if (setq node (pop *going-nodes*))
	(setf (n-a-status node)
	      (case (n-a-status node)
		(STAYING-IN 'IN)
		(STAYING-OUT 'OUT)
		(GOING-IN (enqueue-node node) 'IN)
		(GOING-OUT 'OUT)
		((IN OUT) (error "Impossible combination"))
		(T (error "Impossible status"))))
	(return 'DONE))))

(defun print-consequent (consequent)
       (print `(,(n-a-datum (car consequent))  .,(mapcar #'(lambda (n) (n-a-datum n)) 
							   (cdr consequent)))))

(proclaim '(special *node-string*))		; Forbus DEFVAR's it.

;;; Only for KCL:
(defvar *node-string*)

;;; ******* kludge, why not construct this on demand instead of creating all these
;;; absurd names.
;;; All these calls to string are necessary because the string returned might
;;; be a zetalisp string.  We don't know what type of function funcall is calling.
(defun node-string (node)
  (cond ((eq (n-a-datum node) *temp-node-datum*)
	 (cl-apply #'concatenate
		   'STRING
		   "Temp-^"
		   (mapcar #'node-string (cdar (n-a-justifications node)))))
	;;
	((atms-node-string *atms*)
	 (string (funcall (atms-node-string *atms*) node)))
	;; For Dr. Forbus (soon to be obsolete).
	((and (boundp '*node-string*) *node-string*)
	 (string (funcall *node-string* node)))
;	((and (n-a-classes node) (null (cdr (n-a-classes node))))
;	 (format nil "~A=~A" (car (n-a-classes node)) (n-a-datum node)))
	(t (format nil " ~A" (n-a-datum node)))))


;;; As this sometimes gets called an awful lot, this is a bit open-coded.  This can
;;; use ideas from the single version to optimize***.
(defun known-in-all-envs? (n-a envs)
  (dolist (e (n-a-envs n-a) T)
    (if e
	(unless (dolist (e2 envs) (if (subset-env? e2 e) (return T)))
	  (return nil)))))

;;; Equivalent to above, but much more optimized.  I just open code subset-env? and
;;; optimized like a serious compiler should but doesn't.
;;; Both arguments are guaranteed non-empty.
(defun known-in-all-envs-single? (n-a envs &aux e count vector)
  (setq e (car (n-a-envs n-a)))
  (if (eq e *empty-env*) (return-from KNOWN-IN-ALL-ENVS-SINGLE? T))
  (setq count (env-count e) vector (env-vector e))
  (dolist (e2 envs)
    (if (or (eq e e2)
	    (and (< (env-count e2) count) (vector-subset (env-vector e2) vector)))
	(return-from KNOWN-IN-ALL-ENVS-SINGLE? T))))

;;; Mark a set of envs contradictory.  Guarantee is that envs are not now contradictory,
;;; and the set is minimal.  This is organized to page less if possible.
(defun contradictory-envs (envs reason) (if envs (contradictory-envs1 envs reason)))

(defun find-base-contradiction (env &aux reason)
  (loop (setq reason (env-contradictory-info env))
	(selectq (car reason)
	  (BASE (return env))
	  (SUBSUMED (setq env (cdr reason)))
	  (T (error "Bad data structure")))))

;;; Note that envs had better not be the label of some node or else this will die.  Because
;;; contradicting the environment, will remove the env from this very same list.  So envs
;;; would magically evaporate while looking at it.
(defun contradictory-envs1 (envs reason &aux max-count)
  ;; If so, remove them, but I think there should not be.
  (dolist (env envs) (if (env-contradictory env) (error "Illegal call"))
	             (if (eq *empty-env* env) (throw 'CONTRADICTION 'FAIL)))
  (and (atms-nogood-handler *atms*)
       (funcall (atms-nogood-handler *atms*) envs reason)
       (return-from CONTRADICTORY-ENVS1 T))

  (if *simple-hybrid* (dolist (e envs) (focus-is-inconsistent? e)))

  (setq envs (sort envs #'(lambda (e1 e2) (< (env-count e1) (env-count e2))))
	max-count (env-count (car (last envs))))
  (unless ( max-count *max-contra-count*)
    (setq *max-contra-count* max-count)
    (unless (or *single-nogood-tree* (< max-count (array-length *nogood-trees*)))
      (setq *nogood-trees*
	    (adjust-array *nogood-trees*
			  (floor (* 1.5 (array-length *nogood-trees*)))))))
  (dolist (env envs)
    ;;;**** this could be done more efficiently by grouping.  If this turns out to
    ;;; be an inefficiency do it.
    (setf (aref *environments* (env-count env))
	  (fdelq1 env (aref *environments* (env-count env))))
    (setf (env-contradictory-info env) reason)
    (setf (env-contradictory-bit env) 1)
    (update-env-string env)
    (if *contra-trace*
	(format T "~% ~A is contradicting1 because ~A" env reason))
    (incf *contra-counter*)

    (dolist (node (env-nodes env))
      (remove-env-from-label env node))
    (setf (env-nodes env) nil))

  ;; **** This can be made much more efficient by integrating with below.
  ;; Remove any redundant contradictions.
  ;; **** This can be made much more efficient by integrating the ideas from contradictory-env
  ;; **** This should skip singletons.
  (sweep-contradictions-envs envs)
  ;; Put new contradictions into contradiction array.  Skip singletons.
  (insert-contradictions envs)
  (sweep-environment-envs envs)
  ;; Get rid the singleton nogoods right away.  Their presence any longer will confuse
  ;; the weaver if it is ever called again.
  (dolist (env envs)
    (when (= (env-count env) 1)
      (contradictory-assumption-a (car (env-assumptions env)) env reason)))
  ;; Now do simple resolutions on singletons.  This may cause everything to recurse.
  ;; which may be a problem --- I don't know.
  (dolist (env envs)
    (when (= (env-count env) 1)
      (contradictory-assumption-b (car (env-assumptions env)))))
  (if (or *h4* *resolve-by-labeling* *resolve-by-ordered-labeling*)
      (dolist (env envs) (new-nogood env)))
  (dolist (env envs)
    (cond ((= (env-count env) 1))
	  ((= (env-count env) 2) (contradictory-binary-env env)
	                         (if *h45* (contradiction-binary-disjunction env)))
	  (t (if *h45* (contradiction-binary-disjunction env))
	     (dolist (assumption (env-assumptions env))
	       (setf (assumption-dirty assumption) T)
	       (push env (assumption-nogoods assumption))))))
  ;; Probably contradictory assumptions should be handled by a different
  ;; test.  Much faster***SUBSET FOR EXAMPLE IS TOO SLOW. NEED A VECTOR-MEMQ.
  ;; Do this as the very last thing.
  (dolist (env envs) (signal-nogood env))
  )

(defun insert-contradictions (new-nogoods)
  (if *single-nogood-tree*
      (dolist (new-nogood new-nogoods)
	(insert-in-tree-4 new-nogood *nogood-tree* unbound))
      (dolist (new-nogood new-nogoods)
	(insert-in-tree new-nogood (aref *nogood-trees* (env-count new-nogood))))))

(defun contradictory-binary-env (env &aux as)
  (setq as (env-assumptions env))
  (contradictory-assumption-pair (car as) (cadr as)))

;;;******* what about more complex label assumptions? --- Something to think about.
;;;We could mark a bunch of cons-env's contradictory, but would we miss some inconsistent
;;;environments?  We'd explicitly have to search the data base for them?
(defun contradictory-assumption-pair (a1 a2 &aux vector cache e1 e2)
  (setf (assumption-dirty a1) T)
  (setf (assumption-dirty a2) T)
  (setq vector (vector-cons3 a2 (assumption-binary-vector a1)))
  (setf (assumption-binary-vector a1) vector)
  (setq e1 (assumption-env a1) cache (env-cons-env-cache e1))
  (if cache (rplaca cache vector) (setf (env-cons-env-cache e1) (ncons vector)))
  ;; Now update the label if any (for justified assumptions).
;  (dolist (env (assumption-envs a1))
;    (unless (eq env e1)
;      (setq cache (env-cons-env-cache env)
;	    vector (vector-cons3 a2 (car cache)))
      

  (setq vector (vector-cons3 a1 (assumption-binary-vector a2)))
  (setf (assumption-binary-vector a2) vector)
  (setq e2 (assumption-env a2) cache (env-cons-env-cache e2))
  (if cache (rplaca cache vector) (setf (env-cons-env-cache e2) (list vector)))
  ;;

  ;; **** These should probably be justification consumers because
  ;; **** unless the user installs a justification on an assumption, these
  ;; **** are irrelevant.  
  ;; Don't do an inactive, because there may be other justifications.
  ;; ******* optimize better someday: call inactive only if neither have any non-assumption
  ;; justiciationa.
;  (justify-node *contra-node* (list 'PAIR a1 a2))
  )

(defun c (l1 l2 &aux i1 i2 p1 p2)
  (do nil (nil)
    (do nil (nil)
      (setq p1 i1)
      (setq i1 (pop l1))
      (unless (atom i1) (return nil)))
    (do nil (nil)
      (setq p2 i2)
      (setq i2 (pop l2))
      (unless (atom i2) (return nil)))
    (unless (equal (cadr i1) (cadr i2))
      (print (list p1 p2))
      (print (list i1 i2))
      (do ((l1 l1 (cdr l1))
	   (l2 l2 (cdr l2)))
	  (nil)
	(print (list (car l1) (car l2))))
      (break 'foo))))

;;; All the environment routines.   Remember that now *environments* contains only
;;; consistent environments and non SUBSUMED contradictory.  Perhaps the non subsumed
;;; contradictory environments should go elsewhere. [They do now.]
(defun contradictory-env (env reason &optional (sweep T) (sweep-envs T) &aux count assumptions)
;  (if (= (env-unique env) 90.) (error "Contradictoryin"))

;  (if *rltms* (error "Should not happen anymore"))
;  But we want to only insert it.
  (cond ((eq *empty-env* env) (throw 'CONTRADICTION 'FAIL))
	((env-contradictory env))
	(t ;; Must do this first because in the hybrid scheme, env may not be indexed yet.**
	   ;; **** neither are foci******* which is a potential bug is it not?
	   ;; This order is very very sensitive.  All sorts of bugs will crop up if you
	   ;; change this around.

	   (setf (env-contradictory-info env) reason)
	   (setf (env-contradictory-bit env) 1)
	   ;; The focus must be marked inconsistent, before remove-env-from-label is called.
	   ;; Otherwise, it will report an error.
	   (if *simple-hybrid* (focus-is-inconsistent? env))
	   (unless *sltms*
	     (dolist (node (env-nodes env))
	       (remove-env-from-label env node))
	     (setf (env-nodes env) nil))
	   (update-env-string env)
	   (if *contra-trace*
	       (format T "~% ~A is contradicting because ~A" (string-env env) reason))
	   (incf *contra-counter*)
	   (when sweep
	     ;; We don't want to call this recursively.
	     (when (and (atms-nogood-handler *atms*)
			(funcall (atms-nogood-handler *atms*) env reason))
	       (return-from CONTRADICTORY-ENV nil))
	     (setq count (env-count env))
	     (unless ( count *max-contra-count*)
	       (setq *max-contra-count* count)
	       (unless (or *single-nogood-tree* (< count (array-length *nogood-trees*)))
		 (setq *nogood-trees*
		       (adjust-array *nogood-trees*
				     (floor (* 1.5 (array-length *nogood-trees*)))))))
	    (setq assumptions (env-assumptions-delay env))
	    (sweep-contradictions env assumptions)
	    (if *single-nogood-tree*
		(insert-in-tree-4 env *nogood-tree* assumptions)
		(insert-in-tree env (aref *nogood-trees* count)))
	     ;;******* singleton contradictions can go much faster.  Scanning
	     ;;******* environments may not be worth it.
	     (setf (aref *environments* count) (fdelq1 env (aref *environments* count)))
	     ;; Now update environments constructed thus far.
	     (if sweep-envs (sweep-environments env))
	     (if (or *h4* *resolve-by-labeling* *resolve-by-ordered-labeling*)
		 (new-nogood env))
	     ;; **** eventually binary contradictions won't be in contradicotory array
	     ;; **** and binary envs won't have to be looked up*****
	     (cond ((= count 1) (contradictory-assumption (car assumptions) env reason))
		   ((= count 2) (contradictory-binary-env env)
		                (if *h45* (contradiction-binary-disjunction env)))
		   (t (if *h45* (contradiction-binary-disjunction env))
		      (dolist (assumption assumptions)
			(setf (assumption-dirty assumption) T)
			(push env (assumption-nogoods assumption)))))
	     ;; Probably contradictory assumptions should be handled by a different
	     ;; test.  Much faster***SUBSET FOR EXAMPLE IS TOO SLOW. NEED A VECTOR-MEMQ.
	     ;;; Do the signal as the very last thing.
	     (signal-nogood env)

	     ))))

;;; When an inconsistency occurs while focussing, we should immediately mark the foci
;;; inconsistent.  Why is this done at all?  I've forgotten.**** It now just seems a source
;;; of bugs?
;;; Notice that with functions like new-candidate-early a contradiction out of the
;;; focus can occur because it calls cons-for-false directly.  
(defun focus-is-inconsistent? (env &aux focus count)
  (cond ((null *foci*))
	((eq *foci* :EMPTY))
	((env-contradictory (setq focus (car *foci*))))
	;; See comments on update-... on a few occasions the contradiciton may be
	;; outside the focus.
	((not (subset-env? env focus)))

	(t (setq count (env-count focus))
	   (setf (aref *environments* count) (fdelq1 env (aref *environments* count)))
	   (contradictory-env focus (cons 'SUBSUMED env)
			      nil nil)
	   (setq *foci* :EMPTY)
	   )))

;;; The focussing case can be made more efficient.******
;;; This now assumes hybrid if focussing.
(defun remove-env-from-label (env node)
  (cond ((null (n-a-blocked node))
	 (if *explain-flag* (push env (n-a-contra-envs node)))
	 (unless (setf (n-a-envs node) (fdelq1 env (n-a-envs node))) (out-node node)))
	((eq env (car (n-a-envs node)))
	 (set-hybrid-label node nil 'remove-env-from-label)
	 (out-node node)
	 ;;**** label is sorted by size now.
	 (setf (n-a-blocked node) (fdelq1 env (n-a-blocked node)))
	 ;; This may or may not be wasted work.  But the label for the node is
	 ;; may no longer hybrid-correct now.  Either the next refocus should be global,
	 ;; or we can update here which may be futile.  I choose that on average,
	 ;; updating here would be best.  We also could have a list of nodes
	 ;; that require updating at the next change foci.
	 (setf (n-a-focus node) nil)
	 ;; Use *good-foci* here, because there is the only place we find contradictions.
	 (cond ((env-contradictory *good-foci*)
;		(or (eq *foci* :EMPTY) (and *foci* (env-contradictory (car *foci*))))
		(unless *ltms* (push node *changed-hybrid-nodes*)))
	       (t ;; I believe this can't happen anymore for the simple reason that
		  ;; the only contradictions which should happen are inside the focus,
		  ;; making the focus inconsistent!
		  
;;; ****** KDF: Here's where the barf was
;		  (error "Contradiction outside of focus")
		  
		  (cleanup-single-node-simple-hybrid node))))
	(t (setf (n-a-blocked node) (fdelq1 env (n-a-blocked node))))))

(defun sweep-contradictions (new-nogood as)
  (let ((reason (cons 'SUBSUMED new-nogood)))
    (cond (*single-nogood-tree*
	   (subsumed-from-tree-4 #'(lambda (nogood)
				     #+Symbolics
				     (declare (sys:downward-function))
				     (redundant-contradiction nogood reason))
				 as
				 *nogood-tree*))
	  (t ;; Find them.
	   (do ((i (1+ (env-count new-nogood)) (1+ i))
		(misses 1 (1+ misses)))
	       ((> i *max-contra-count*))
	     (subsumed-from-tree #'(lambda (nogood)
				     #+Symbolics
				     (declare (sys:downward-function))
				     (redundant-contradiction nogood reason))
				 misses as (aref *nogood-trees* i)))))))

(defun sweep-contradictions-envs (new-nogoods)
  (dolist (new-nogood new-nogoods) (sweep-contradictions new-nogood)))

;;; Given a new-nogood, this updates all cached environments.  This is heuristic and
;;; probably should be tuned.
(defvar *fast-sweep* nil)				; Experiment.

;;; I don't think *fast-sweep* should work because envs in foci etc and intermediates
;;; want to find out their are false too.  So don't use it.

(defun sweep-environments (new-nogood &aux start-size nogood-vector reason
			   in-focusp)
;  (if *sltms* (return-from sweep-environments nil))
  (if *debug* (check-env-waiting))
  (setq reason (cons 'SUBSUMED new-nogood)
	start-size (1+ (env-count new-nogood))
	nogood-vector (env-vector new-nogood))
;  (when (and *fast-sweep* (setq start-length (length (aref *environments* start-size))))
;    (dolist (a (env-assumptions new-nogood))
;      (when (< (assumption-count a) start-length)
;	(dolist (env (assumption-in-envs a))
;	  (if (subset-env? new-nogood env) (contradictory-env env reason nil nil)))
;	(return-from SWEEP-ENVIRONMENTS nil))))
  ;;******** cache env-waiting as its slow to get at
  (and *simple-hybrid* (env-waiting new-nogood) (not *ltms*)
       (setq in-focusp (- (env-count new-nogood) (env-waiting new-nogood))))
  (do ((i start-size (1+ i)))
      ((> i *max-env-count*))
    (do ((e (aref *environments* i) (cdr e))
	 (previous nil))
	((null e))
      (cond ((and in-focusp
		  (env-waitingp (car e))
		  (> in-focusp (- (env-count (car e)) (env-waiting (car e)))))
	     (setq previous e))
	    ((vector-subset nogood-vector (env-vector (car e)))
	     (if previous (rplacd previous (cdr e))
		 (setf (aref *environments* i) (cdr e)))
	     (contradictory-env (car e) reason nil nil))
	    (t (setq previous e))))))

;;; Could rplacd the list?
(defun sweep-environments-list (new-nogood envs)
  (dolist (env envs)
    (when (tms::subset-env? new-nogood env)
      (contradictory-env env (cons 'SUBSUMED new-nogood) nil nil))))

;;; Same as sweep-environments but with a sequence of envs: Smallest nogood first.
(defun sweep-environment-envs (nogoods &aux env-reason)
  (do ((i (1+ (env-count (car nogoods))) (1+ i)))
      ((> i *max-env-count*))
    (do ((e (aref *environments* i) (cdr e))
	 (previous nil))
	((null e))
      ;;*** propersubsetenv is ok I think.
      (cond ((dolist (env nogoods) (unless (< (env-count env) i) (return nil))
		     (when (subset-env? env (car e)) (setq env-reason env) (return T)))
	     (if previous (rplacd previous (cdr e)) (setf (aref *environments* i) (cdr e)))
	     (contradictory-env (car e) (cons 'SUBSUMED env-reason) nil))
	    (t (setq previous e))))))

;;; *****NOGOODS CAN BE PRUNED MORE EFFICIENTLY TOO BECAUSE WE KNOW 
;;; WHICH ONES WE HAVE TO REMOVE.  Mark them 'SUBSUMED and prune.
;;; Note, this presumes the environments have already been pruned
(defun contradictory-assumption (assumption env reason)
  (contradictory-assumption-a assumption env reason)
  (contradictory-assumption-b assumption)
  )

;;; Note that every environment except itself should be gone already because
;;; of the env-nodes data structure.
(defun contradictory-assumption-a (assumption env reason)
  (if *simple-hybrid* (set-hybrid-label assumption nil 'CONTRADICTORY-ASSUMPTION-A))	
  (setf (assumption-dirty assumption) T
	(n-a-blocked assumption) nil
	(assumption-nogoods assumption) nil)
  ;; This line is needed.
  (propagate-false assumption reason)
  ;;**** does this affect contras.
  (setf (assumption-contradictory assumption) (cons 'BASE env)))

;;; This does the propagation through the disjunction database, once an assumption
;;; has been discovered to be false.  Remember this function can be recursively
;;; entered.
  ;;; Xors are the same as iors.
(defun contradictory-assumption-b (assumption &aux ors)
  ;; ***** I've convinced myself that the following only works when an assumption
  ;; ***** occurs in only one disjunction.
  (setq ors (assumption-ors assumption))
  (dolist (or ors)
    (when *h4-trace*
      (format T "~% Eliminating disjunct ~A from" assumption)
      (print-or or))
    (remove-or or)
    (decf (disjunction-count or))
    (setf (disjunction-disjuncts or) (fdelq1 assumption (disjunction-disjuncts or))))
  ;; First flush assumptions and see what happens.
  (dolist (or ors)
    (when (= (disjunction-count or) 1)
      (if *h4-trace* (format T "~% Disjunction excised"))
      (true-assumption (car (disjunction-disjuncts or)) 'CONTRADICTORY-ASSUMPTION)))
  ;; Now do some work putting the ors back.
  ;;******** there is wierdness here that needs to be thought about.
  ;;******** what really really happens when you re-insert, how many of the old
  ;;******** nogoods can you really save.  Think about this*****
  ;;******** Also we should really do a db lookup insertiion/deltion again.
  ;;******** It could, in fact, now be subsumed.
  (dolist (or ors)
    (cond ((< (disjunction-count or) 2))
	  ((disjunction-satisfied or))
	  (t ;;; Could do this with an xor, or anti vector-cons.
 	   (setf (disjunction-vector or) (make-env-vector* (disjunction-disjuncts or)))
	   (setf (disjunction-nogoods or)
		 (delete-if #'(lambda (slot) (eq (car slot) assumption))
			    (disjunction-nogoods or)
			    :count 1))
	   (add-or or)
	   (push or *or-queue*)
;	   (and *h4* (> (disjunction-count or) *h4*) (new-disjunction or))
	   ))))

(defvar *subsume-trace* nil "Trace every subsumption of a nogood.")

(defun redundant-contradiction (e reason)
  (if *subsume-trace*
      (format T "~% Nogood ~A is being subsumed because ~A" e reason))
  ;; Nodes is now unused, so store old contradiction reason here.
  (if *explain-flag* (push (env-contradictory-info e) (env-nodes e)))
  (setf (env-contradictory-bit e) 1)
  (setf (env-contradictory-info e) reason))





;;; A version of Union-envss which tries very very had not to call union-env if it at all
;;; can be avoided.  This could be smarter, but that may not be worth it.  We know the
;;; intersection is minimal so many subset tests can be avoided.  Also, we might want
;;; to do a compare-env on every pair.   That would save more union-env calls.

;; Could always call generic-union-envss.
(defun union-envss (envs1 envs2 &aux envs new-e)	
  (dolist (e1 envs1) (if (memq e1 envs2) (push e1 envs)))
  (dolist (e1 envs1)
    (unless (memq e1 envs)
      (dolist (e2 envs2)
	(unless (memq e2 envs)
	  (setq new-e (union-env3 envs e1 e2))
	  (unless (env-contradictory new-e)
	    (do ((old-e envs (cdr old-e)))
		((null old-e))
	      (if (and (car old-e) (subset-env? new-e (car old-e)))
		  (rplaca old-e nil)))
	    (push new-e envs))))))
  (fdelqa nil envs))

(defun generic-env-contradictory (env-or-nil)
  (cond ((null env-or-nil) t)
	((tms::simple-envp env-or-nil) nil)
	(t (tms::env-contradictory env-or-nil))))

(defun generic-union-envss (envs1 envs2 &aux envs new-e)	
  (dolist (e1 envs1) (if (generic-env-member e1 envs2) (push e1 envs)))
  (dolist (e1 envs1)
    (unless (generic-env-member e1 envs)
      (dolist (e2 envs2)
	(unless (generic-env-member e2 envs)
	  (when (setq new-e (generic-union-env3 envs e1 e2))
	    (do ((old-e envs (cdr old-e)))
		((null old-e))
	      (if (and (car old-e) (generic-subset-env? new-e (car old-e)))
		  (rplaca old-e nil)))
	    (push new-e envs))))))
  (fdelqa nil envs))

;;; Based on the assumption that no simple-env will ever be equal to a regular env.
;;; This is true only for simple-env's created by certain functions.
(defun generic-env-member (e envs &aux vector)
  (cond ((not (simple-envp e)) (memq e envs))
	(t (setq vector (simple-env-vector e))
	   (dolist (e envs)
	     (and (simple-envp e) (vector-equal vector (simple-env-vector e)) (return T))))))

;;; ***** cons-env should test before consing.
;;; ***** contradiction can do a min at end.

;;; For almost all applications, on average, its always worth checking whether the
;;; combination is illegal.

;;; Do the union only if the result will be of size 2 or smaller.
(defun 2-union-env (e1 e2 &aux c1 c2)
  (cond ((eq e1 e2) e1)
	((eq e1 *empty-env*) e2)
	((eq e2 *empty-env*) e1)
	((> (setq c1 (env-count e1)) 2.) *contra-env*)
	((> (setq c2 (env-count e2)) 2.) *contra-env*)
	((= c1 1) (cond ((= c2 1)
			 (double (car (env-assumptions e1)) (car (env-assumptions e2))))
			((memq (car (env-assumptions e1)) (env-assumptions e2)) e2)
			(t *contra-env*)))
	((= c2 2) *contra-env*)
	((memq (car (env-assumptions e2)) (env-assumptions e1)) e1)
	(t *contra-env*)))

;;; This is exactly like union-env, except this delays constructing an
;;; environment as late as possible and still be optimal.  It returns a
;;; contradictory environment, if the result will be a superset of envs.
(defun union-env3 (envs e1 e2 &aux result count1 count2)	
  (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))))
       (return-from UNION-ENV3 *contra-env*))
  (setq result
	(cond ((eq e1 e2) e1)
	      ((env-contradictory e1) (return-from UNION-ENV3 *contra-env*))
	      ((env-contradictory e2) (return-from UNION-ENV3 *contra-env*))
	      ((eq e1 *empty-env*) e2)
	      ((eq e2 *empty-env*) e1)
	      ((= (setq count1 (env-count e1)) 1)  (cons-env e2 (car (env-assumptions e1))))
	      ((= (setq count2 (env-count e2)) 1)  (cons-env e1 (car (env-assumptions e2))))
	      ;; 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))
		       (progn e2))
		   (if (< count2 count1)
		       (if (vector-subset (env-vector e2) (env-vector e1))
			   (progn  e1)))))
	      ;; *** if union-check is enabled this maybe should cache.  But it never returns
	      ;; T why?
	      ((not (compatible-env? e1 e2)) (return-from UNION-ENV3 *contra-env*))
	      (t (return-from UNION-ENV3 (union-env1-3 envs e1 e2)))))
  (if (or (env-contradictory result)
	  (dolist (e envs) (and e (subset-env? e result) (return *contra-env*))))
      *contra-env*
      result))

;;; Returns NIL if result is nogood.
(defun generic-union-env3 (envs e1 e2 &aux result count1 count2)
  (setq result
	(cond ((and *union-check*
		    (or (vector-intersection? (generic-env-vector e1)
					      (generic-env-cons-env-cache e2))
			(vector-intersection? (generic-env-vector e2)
					      (generic-env-cons-env-cache e1))))
	       nil)
	      ((eq e1 e2) e1)
	      ((and (not (simple-envp e1)) (env-contradictory e1)) nil)
	      ((and (not (simple-envp e2)) (env-contradictory e2)) nil)
	      ((eq e1 *empty-env*) e2)
	      ((eq e2 *empty-env*) e1)
	      ((= (setq count1 (generic-env-count e1)) 1)
	       (generic-cons-env e2 (car (generic-env-assumptions e1))))
	      ((= (setq count2 (generic-env-count e2)) 1)
	       (generic-cons-env e1 (car (generic-env-assumptions e2))))
	      ;; We could optimize cons-env now****
	      ;; If complete only one of these tests should be sufficient.

	      ((if (< count1 count2)
		   (if (vector-subset (generic-env-vector e1) (generic-env-vector e2))
		       (progn e2))
		   (if (< count2 count1)
		       (if (vector-subset (generic-env-vector e2) (generic-env-vector e1))
			   (progn  e1)))))
	      ;; *** if union-check is enabled this maybe should cache.  But it never returns
	      ;; T why?
	      ((not (generic-compatible-env? e1 e2)) nil)
	      (t (return-from GENERIC-UNION-ENV3 (generic-union-env1-3 envs e1 e2)))))
  (and result
       (if (simple-envp result) T (not (env-contradictory result)))
       (not (dolist (e envs) (and e (generic-subset-env? e result) (return T))))
      result))

;;; This is the analog to union-env1.  It tries to avoid creating the environment
;;; if it doesn't need to.
(defun union-env1-3 (envs e1 e2 &aux v env ptr assumptions count)
  (incf *big-union-count*)
  (setq v (vector-union (env-vector e1) (env-vector e2))
	ptr (nget-or-puthash-env v *env-hash-table* T))
  (cond ((setq env (hash-slot-value ptr))
	 (if (env-contradictory env) (return-from UNION-ENV1-3 *contra-env*))
	 (dolist (e envs) (and e (subset-env? e env) (return-from UNION-ENV1-3 *contra-env*)))
	 env)
	((dolist (e envs) (and e (vector-subset (env-vector e) v) (return *contra-env*))))
	((progn (if *delay-assumptions*
		    (multiple-value-setq (assumptions count)
		      (blits-to-assumptions v))
		    (multiple-value-setq (assumptions count)
		      (fast-assumptions-union e1 e2)))
		(new-contradictory-env-assumptions? assumptions count))
	 (hash-slot-set ptr v *env-hash-table*)
	 (setf (aref *hashes* count) T)
	 (hash-allocate *env-hash-table*)
	 *contra-env*)
	(T (setq env (make-an-env-2 count
				    (if *delay-assumptions* :DELAY (fcopylist assumptions))
				    (fcopylist v)))
	   ;; The following is optional, I have never seen it do any harm, and
	   ;; I have never seen it do any good.
	   (setf (env-cons-env-cache env)
		 (ncons (vector-union-new (car (env-cons-env-cache e1))
					  (car (env-cons-env-cache e2)))))
	   (hash-slot-set ptr env *env-hash-table*)
	   (setf (aref *hashes* count) T)
	   (hash-allocate *env-hash-table*)
	   env)))

;;; We are guaranteed none of the antecedents are NIL or hold in *empty-env* and
;;; there are more than 1 antecedents.
;;; Returns NIL if environment is contradictory.***
;;; Wide-union cannot return contradictory, because every env is supposed to be part
;;; of the current focus.

;;; For most problems *large* T offers an improvement.
(defvar *large* T)

(defun wide-union (known-env knowns antecedents &aux v ptr env count)

  (if *rltms* (error "Don't call wide-union"))

  (setq v (parallel-vector-union antecedents))

  (setq count (blits-size v))

  ;; The following order was developed by experiment.
  ;; This is the most common case, so it's optimized.
  (when known-env

    (and *sltms* (not *critical*) (>= count (env-count known-env)) (return-from wide-union nil))

    ;;***** it strikes me that this entire function can be optimized in the sltms case.

    (when (or (vector-equal (env-vector known-env) v)
	      (vector-subset (env-vector known-env) v))
      (return-from WIDE-UNION nil))
    (when *critical*
      ;;****** can have a side-effecting remove!!!!
      (unless (vector-subset v (env-vector known-env))
	(dolist (a (blits-to-assumptions v))
	  (unless (vector-member a (env-vector known-env))
;	    (format T "~% Critical is doing something")
	    ;;****** can have a side-effecting remove!!!!
	    (decf count)
	    (setq v (remove-assumption-blits-unsafe v a)))))))
  (dolist (e knowns)
    (if (> (env-count e) count) (return nil))
    (and (neq e known-env)
	 (in-current-focus? e)
	 (= count (env-count e))
	 (vector-equal (env-vector e) v)
	 (return-from WIDE-UNION (values nil e))))	;Second arg used by *ltms*.

  ;;*** optimize.  This assumes it won't get any empty-env's at all here.
  ;;**** HOw can the following ever happen?  it does the right thing though.??
  (cond ((= count 1) (return-from WIDE-UNION (hybrid-label (car antecedents))))
	;;**** horribly slow:
	((= count 2)
	 (let ((assumptions (blits-to-assumptions v)))
	   (setq env (double (car assumptions) (cadr assumptions)))
	   (and (not *index-early*)
		*foci* (neq (car *foci*) :EMPTY) (setf (env-waiting env) 0))
	   (return-from WIDE-UNION env))))

  ;; We could check here whether the result is a superset of a known.  But
  ;; this event is extremely rare.  So we're not using it right now.

  ;; Find the slot in the hash table where this assumption occurs.
  (setq ptr (nget-or-puthash-env v *env-hash-table* T)
	env (hash-slot-value ptr))

  (cond ((null env))
	((env-contradictory env) (return-from WIDE-UNION nil))
	(t (return-from WIDE-UNION env)))

  ;;****** delete in unsafe versoin.
  (setq v (fcopylist v))

  ;; Now check to see whether any binary nogoods are violated.
;  (setq assumptions (env-assumptions (car antecedents)))
;  (dolist (a (cdr antecedents))
;    (setq assumptions (assumptions-union assumptions (env-assumptions a))))

;  (setq count (length assumptions))
;  (multiple-value-bind (new-assumptions new-length)

;    (unless (= count new-length) (error "Length error"))
;    (unless (equal assumptions new-assumptions) (error "Assumptions error")))



;  (multiple-value-setq (assumptions count) (parallel-assumptions-union antecedents))
;  (multiple-value-setq (assumptions count) (blits-to-assumptions v))
;  (setq assumptions (fcopylist1 assumptions count))

  ;; Now check to see whether any binary nogoods are violated.
;  (when (and *debug*
;	     (or (not (compatible-assumptions? assumptions v))
;		 (new-contradictory-env-assumptions? assumptions count)))
;    (error "Debugging check: Wide-union produces contradictory result"))
  (setq env (make-an-env-2 count (if *delay-assumptions*
				     :DELAY
				     (fcopylist1 (blits-to-assumptions v) count))
			   v))
  (and (not *index-early*)
       *foci* (neq (car *foci*) :EMPTY) (setf (env-waiting env) 0))
  
  (hash-slot-set ptr env *env-hash-table*)
  (hash-allocate *env-hash-table*)
  (setf (aref *hashes* count) T)
  env)

;;; This is an experimental version right now.
;;;***** notice that this can still be greatly optimzed.***
;;; Notice that this now allows *empty-env*.  Its unclear whether its worth
;;; optimizing this case.
(defun parallel-vector-union (antecedents &aux v conses)
  (setq conses *fast-assumptions-conses*)
  (multiple-value-setq (v conses) (vector-union-unsafe-blits
				    (env-vector (hybrid-label (car antecedents)))
				    (env-vector (hybrid-label (cadr antecedents)))
				    conses))
  (dolist (a (cddr antecedents))
     (multiple-value-setq (v conses)
       (vector-union-unsafe-blits v (env-vector (hybrid-label a)) conses)))
  v)

(defun parallel-vector-union-old (antecedents &aux v)
  (setq v (vector-union (env-vector (car antecedents)) (env-vector (cadr antecedents))))
  (dolist (a (cddr antecedents))
    ;;******** Could save conses here.******* Or have a parallel vector-union*****
    (setq v (vector-union v (env-vector a))))
  v)

;;; This is the analog to union-env1.  It tries to avoid creating the environment
;;; if it doesn't need to.
(defun generic-union-env1-3 (envs e1 e2 &aux v env assumptions count)
  (incf *big-union-count*)
  (setq v (vector-union (generic-env-vector e1) (generic-env-vector e2)))
  (cond ((setq env (gethash-env v *env-hash-table*))
	 (if (env-contradictory env) (return-from GENERIC-UNION-ENV1-3 nil))
	 (dolist (e envs) (and e
			       (generic-subset-env? e env)
			       (return-from GENERIC-UNION-ENV1-3 nil)))
	 env)
	((dolist (e envs)
	   (and e (vector-subset (generic-env-vector e) v) (return nil))))
	((progn (if *delay-assumptions*
		    (multiple-value-setq (assumptions count)
		      (blits-to-assumptions v))
		    (setq assumptions (assumptions-union (generic-env-assumptions e1)
							 (generic-env-assumptions e2))
			  count (length assumptions)))
		(new-contradictory-env-assumptions? assumptions count))
	 nil)
	(T (make-simple-env (length assumptions)
			    (vector-union-new (generic-env-cons-env-cache e1)
					      (generic-env-cons-env-cache e2))
			    assumptions
			    v))))

;;; Someday experiment with the order of these initial tests.
(defun union-env (e1 e2 &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)))))
	 *contra-env*)
	((eq e1 e2)  e1)
	((env-contradictory e1) *contra-env*)
	((env-contradictory e2) *contra-env*)
	((eq e1 *empty-env*)  e2)
	((eq e2 *empty-env*)  e1)
	((= (setq count1 (env-count e1)) 1)  (cons-env e2 (car (env-assumptions e1))))
	((= (setq count2 (env-count e2)) 1)  (cons-env e1 (car (env-assumptions e2))))
	;; 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))
		 (progn e2))
	     (if (< count2 count1)
		 (if (vector-subset (env-vector e2) (env-vector e1))
		     (progn  e1)))))
	;; *** if union-check is enabled this maybe should cache.  But it never returns
	;; T why?
	((not (compatible-env? e1 e2)) *contra-env*)
	((union-env1 e1 e2))))

(defun generic-union-env (e1 e2 &aux count1 count2)
  (cond ((and *union-check*
	      (or (vector-intersection? (generic-env-vector e1)
					(generic-env-cons-env-cache e2))
		  (vector-intersection? (generic-env-vector e2)
					(generic-env-cons-env-cache e1))))
	 nil)
	((eq e1 e2) e1)
	((and (not (simple-envp e1)) (env-contradictory e1)) nil)
	((and (not (simple-envp e2)) (env-contradictory e2)) nil)
	((eq e1 *empty-env*) e2)
	((eq e2 *empty-env*) e1)
	((= (setq count1 (generic-env-count e1)) 1)
	 (generic-cons-env e2 (car (generic-env-assumptions e1))))
	((= (setq count2 (generic-env-count e2)) 1)
	 (generic-cons-env e1 (car (generic-env-assumptions e2))))
	;; We could optimize cons-env now****
	;; If complete only one of these tests should be sufficient.
	((if (< count1 count2)
	     (if (vector-subset (generic-env-vector e1) (generic-env-vector e2))
		 (progn e2))
	     (if (< count2 count1)
		 (if (vector-subset (generic-env-vector e2) (generic-env-vector e1))
		     e1))))
	((not (generic-compatible-env? e1 e2)) nil)
	(t (generic-union-env1 e1 e2))))

;;; *can be improved a lot more.
(defun generic-union-env1 (e1 e2 &aux v env assumptions count)
  (incf *big-union-count*)
  (setq v (vector-union (generic-env-vector e1) (generic-env-vector e2)))
  (cond ((setq env (gethash-env v *env-hash-table*))
	 (and (not (env-contradictory env)) env))
	((progn (if *delay-assumptions*
		    (multiple-value-setq (assumptions count)
		      (blits-to-assumptions v))
		    (setq assumptions
			  (assumptions-union (generic-env-assumptions e1)
					     (generic-env-assumptions e2))
			  count (length assumptions)))
		(new-contradictory-env-assumptions? assumptions count))
	 nil)
	(T (make-simple-env count
			    (vector-union-new (generic-env-cons-env-cache e1)
					      (generic-env-cons-env-cache e2))
			    (if *delay-assumptions* :DELAY assumptions)
			    v))))

;;; A whole set of envs are to be unioned.  Return T if env becomes contradictory.
;;; This generates the singleton and double contradictions first.  For many applications
;;; 50% of the CPU cycles are spent here
(defun unions-for-false (env envs reason &aux count1 count2 vector1 cache1 vector2 cache2)
  (unless envs (return-from UNIONS-FOR-FALSE nil))
  (setq count1 (env-count env) vector1 (env-vector env))
  (cond ((memq env envs) (contradictory-env env `(BASE UNIONS-FOR-FALSE ,reason)) T)
	((eq *empty-env* env)
	 (error "This should be optimized out --- removing this line is ok")
	 (dolist (e envs) (contradictory-env e `(BASE UNIONS-FOR-FALSE ,reason)))
	 nil)
	((eq (car envs) *empty-env*)
	 (error "This should be optimized out --- removing this line is ok")
	 (contradictory-env env `(BASE UNIONS-FOR-FALSE ,reason))
	 T)
	((dolist (e envs)
	   (when (and (< (env-count e) count1) (vector-subset (env-vector e) vector1))
	     (contradictory-env env `(BASE UNIONS-FOR-FALSE ,reason))
	     (return T))))
	((= count1 1)
	 (dolist (e envs)
	   (when (= (env-count e) 1)
	     (double-for-false (car (env-assumptions e)) (car (env-assumptions env)) reason)
	     (if (env-contradictory env) (return-from UNIONS-FOR-FALSE T))))
	 (dolist (e envs)
	   (unless (= (env-count e) 1)
	     (cons-for-false e (car (env-assumptions env)) reason)
	     (if (env-contradictory env) (return T)))))
	;; We know no element of envs is a subset of env.
	;; We know *empty-env* is not on envs.
	;; We know that env has at least 2 assumptions.
	;; We know env is not contradictory.
	;; We know env is not on envs.
	;; The following open-codes union-for-false under those assumptions.
	(t (setq cache1 (car (env-cons-env-cache env)))
	   (dolist (e envs)
	     (setq vector2 (env-vector e)
		   cache2 (car (env-cons-env-cache e))
		   count2 (env-count e))
	     (cond ((env-contradictory e))
		   ((= count2 1) (cons-for-false env (car (env-assumptions e)) reason))
		   ((and cache1 (vector-intersection? vector2 cache1)))
		   ((and cache2 (vector-intersection? vector1 cache2)))
		   ((and (< count1 count2) (vector-subset vector1 vector2))
		    (contradictory-env e `(BASE UNIONS-FOR-FALSE ,reason)))
		   ((not (compatible-env? e env)))	
		   ((union-for-false1 e env reason)
		    (if (env-contradictory env) (return T))))))))

(defun k-union-env (e1 e2 &aux c1 c2 vector new-a)
  (cond ((eq e1 e2) e1)
	((or (null *k*) (> *k* 3))
	 (setq c1 (env-count e1) c2 (env-count e2))
	 (if (< c1 c2) (psetq e1 e2 e2 e1 c1 c2))
	 (setq vector (env-vector e1))
	 (dolist (a (env-assumptions e2))
	   (unless (vector-member a vector)
	     (incf c1)
	     (if (and *k* (>= c1 *k*)) (return-from K-UNION-ENV *contra-env*))
	     (setq new-a (if new-a 'LOSE a))))
	 (cond ((null new-a) e1)
	       ((eq new-a 'LOSE) (union-env e1 e2))
	       (t (cons-env e1 new-a))))
	((= *k* 1) (if (eq e1 *empty-env*) *empty-env* *contra-env*))
	((= *k* 2) (if (eq e1 *empty-env*) e2 (if (eq e2 *empty-env*) e1 *contra-env*)))
	;; k must be 3 or more.
	(t (2-union-env e1 e2))))

;(defun fast-k-union-env (env generic-env &aux size new-a generic-vector)
;  (cond ((eq e1 e2) e1)
;	((env-contradictory env) *contra-env*)
;	;; Succeeding tests depend on this.
;	((and (simple-envp generic-env) (vector-equal (env-vector env) (generic-env-vector generic-env)))
;	 env)
;	((equal *k* 1) (if (eq env *empty-env*) *empty-env* *contra-env*))
;	((equal *k* 2) (if (eq env *empty-env*)
;			   generic-env
;			   (if (eq generic-env *empty-env*)
;			       env
;			       *contra-env*)))
;	(t (setq size (generic-env-count generic-env)
;		 generic-vector (generic-env-vector generic-env))
;	   (dolist (a (env-assumptions env))
;	     (unless (vector-member a generic-vector)	
;	       (incf size)			
;	       (and *k* (>= size *k*) (return-from FAST-K-UNION-ENV *contra-env*))
;	       e
;	       (setq new-a (if new-a 'LOSE a))))
;	   (unless (eq new-a 'LOSE)
;	     ;;**** fast-cons-env probably too out of date.
;	     (return-from FAST-K-UNION-ENV (fast-cons-env generic-env new-a T)))
;	   
;	   
;
;  (cond ((eq e1 e2) e1)
;	((or (null *k*) (> *k* 3))
;	 (setq c1 (env-count e1) c2 (env-count e2))
;	 (if (< c1 c2) (psetq e1 e2 e2 e1 c1 c2))
;	 (setq vector (env-vector e1))
;	 (dolist (a (env-assumptions e2))
;	   (unless (vector-member a vector)
;	     (incf c1)
;	     (if (and *k* (>= c1 *k*)) (return-from FAST-K-UNION-ENV *contra-env*))))
;	 (fast-union-env e1 e2))
;	((= *k* 1) (if (eq e1 *empty-env*) *empty-env* *contra-env*))
;	((= *k* 2) (if (eq e1 *empty-env*) e2 (if (eq e2 *empty-env*) e1 *contra-env*)))
;	;; k must be 3 or more.
;	(t (2-union-env e1 e2))))

;;; This function is to be used if you want to avoid creating an environment.
;;; Remember by definiton all simple-envs are consistent. (If not, we'll find out
;;; later).
;;; The first argument is presumed to be a regular env.
;(defun fast-union-env (env generic-env &aux count1 count2 a v1 v2)
;  (cond ((eq env *empty-env*) generic-env)
;	((equal (env-vector env) (generic-env-vector generic-env)) env)
;	((env-contradictory env) *contra-env*)
;	((vector-intersection? (setq v1 (env-vector env))
;			       (car (generic-cons-env-cache generic-env)))
;	 *contra-env*)
;	((vector-intersection? (setq v2 (generic-env-vector generic-env))
;			       (car (cons-env-cache generic-env)))
;	 *contra-env*)
;	;;***** well, we could use cons-env if exactly one assumption added would do it.
;	((= (setq count1 (env-count e1)) 1) (fast-cons-env e2 (car (env-assumptions e1)) T))
;	((= (setq count2 (env-count e2)) 1) (fast-cons-env e1 (car (env-assumptions e2)) T))
;	((and (< (setq count1 (env-count env)) (setq count2 (generic-env-count generic-env)))
;	      (vector-subset v1 v2))
;	 generic-env)
;	((and (< count2 count1) (vector-subset v2 v1)) env)
;	((dolist (a (env-assumptions env))
;	   (if (vector-intersection? (assumption-binary-vector a) vector) (return T)))
;	 *contra-env*)

;;; Note that union-env1 can only be called if the result of the union operation
;;; is 3 or greater assumptions.
(defun union-env1 (e1 e2 &aux v env ptr assumptions count)
  (incf *big-union-count*)
  (setq v (vector-union-unsafe (env-vector e1) (env-vector e2) *fast-assumptions-conses*)
	ptr (nget-or-puthash-env v *env-hash-table*))
  (cond ((hash-slot-value ptr))
	(*simple-hybrid*
	 (setq count (blits-size v))
	 (cond ((or (and (eq (env-waiting e1) 0)
			 (eq (env-waiting e2) 0)
			 (not (env-contradictory *good-foci*)))
		    (not (new-contradictory-env-assumptions? (blits-to-assumptions v)
							     count)))
		(set-env-cache env (car (env-cons-env-cache e1)) (car (env-cons-env-cache e2)))
		(setq env (make-an-env-2 count :DELAY (fcopylist v) t))
		(hash-slot-set ptr env *env-hash-table*)
		(setf (aref *hashes* count) T)
		env)
	       (t (hash-slot-set ptr v *env-hash-table*)
		  (setf (aref *hashes* count) T)
		  *contra-env*)))
	((progn (setq v (fcopylist v))
		(multiple-value-setq (assumptions count)
		  (fast-assumptions-union e1 e2))
		(new-contradictory-env-assumptions? assumptions count))
	 (hash-slot-set ptr v *env-hash-table*)
	 (setf (aref *hashes* count) T)
	 *contra-env*)
	(T (setq env (make-an-env-2 count (fcopylist assumptions) v))
	   ;; The following is optional, I have never seen it do any harm, and
	   ;; I have never seen it do any good.
	   (set-env-cache env (car (env-cons-env-cache e1)) (car (env-cons-env-cache e2)))
	   (hash-slot-set ptr env *env-hash-table*)
	   (setf (aref *hashes* count) T)
	   env)))

;;; A specialization of union-env1.  Again this insists on putting envs in the hash table,
;;; that may be pointless?
;;; Note that the envs generated are 3 or more assumptions long.
(defun union-for-false1 (e1 e2 reason &aux v env ptr assumptions count)
  (incf *big-union-count*)
  (setq v (vector-union-unsafe (env-vector e1) (env-vector e2) *fast-assumptions-conses*)
	ptr (nget-or-puthash-env v *env-hash-table*))
  (cond ((setq env (hash-slot-value ptr))
	 (contradictory-env env `(BASE UNION-FOR-FALSE1 ,reason)))
	(*simple-hybrid*
	 (setq count (blits-size v))
	 (cond ((or (and (eq (env-waiting e1) 0)
			 (eq (env-waiting e2) 0)
			 (not (env-contradictory *good-foci*)))
		    (not (new-contradictory-env-assumptions? (blits-to-assumptions v)
							     count)))
		(setq env (make-an-env-2 count :DELAY (fcopylist v) t))
		(hash-slot-set ptr env *env-hash-table*)
		(setf (aref *hashes* count) T)
		(contradictory-env env `(BASE UNION-FOR-FALSE1 ,reason))
		env)
	       (t (hash-slot-set ptr (fcopylist v) *env-hash-table*)
		  (setf (aref *hashes* count) T)
		  *contra-env*)))
	((progn (setq v (fcopylist v))
		(if *delay-assumptions*
		    (multiple-value-setq (assumptions count)
		      (blits-to-assumptions v))
		    (multiple-value-setq (assumptions count)
		      (fast-assumptions-union e1 e2)))
		(new-contradictory-env-assumptions? assumptions count))
	 (hash-slot-set ptr v *env-hash-table*)
	 (setf (aref *hashes* count) T)
	 *contra-env*)
	(T (setq env (make-an-env-2 count (fcopylist assumptions) v t))
	   (hash-slot-set ptr env *env-hash-table*)
	   (setf (aref *hashes* count) T)
	   (contradictory-env env `(BASE UNION-FOR-FALSE1 ,reason))
	   env)))

;;; Successfull-union? checks whether the union between e1 and e2 will succeed without
;;; creating the environment.  Might be worth optimizing.
(defun successfull-union? (e1 e2) (not (env-contradictory (union-env e1 e2))))

;;; This returns T if the two environments have a non-empty intersection.  Note that
;;; this function is supposed to work on contradictory environments as well.
(defun intersection-env? (e1 e2) (vector-intersection? (env-vector e1) (env-vector e2)))


;;; Creation and data-base for assumptions.
;;; ***** this used to be called create-assumption bunkies.
(defun find-or-make-assumption (variable value)
  (or (find-assumption variable value) (make-a-assumption variable value)))

;;; Convention is NODES only have ':INs, otherwise CLASS.

(defun make-a-assumption (variable value &aux assumption)
  (setq assumption (basic-make-assumption variable value nil))
  (cond ((eq value ':IN) (setf (node-assumption variable) assumption))
	(t (add-xor-assumption-to-class assumption variable)))
  assumption)

(defun add-xor-assumption-to-class (assumption class &optional new)
  (if *trace-file*
      (format *trace-file* "~%ADD-XOR-ASSUMPTION-TO-CLASS ~D ~D"
	      (assumption-unique assumption)
	      (class-unique class)))
  (dolist (a (class-assumptions class))
    ;; If assumptions were guaranteed to be unjustified, we could now call.
    ;; (contradictory-assumption-pair assumption a))
    ;; Unfortunately, they can.
    ;; However, it makes things much more efficient if we help the ATMS up front:
    (contradictory-assumption-pair assumption a)
    (if *clause-mode*
	(tms::clause 'ADD-XOR-ASSUMPTION-TO-CLASS nil (list a assumption))))

    ;; It tends to be very expensive to create these pairwise justifications when
    ;; they are really not needed.  This is a simple approach.  Probably
    ;; we could be even smarter and make a conjunction consumer on itself twice.  But this
    ;; simple approach should almost always work.
  ;; This assumes the assumption was just created.***
  ;; ****There is an argument that the assumptions should just be part of their own class.
  ;; ****Then add-xor-just need never be installed.
  (unless (or new *clause-mode*)
    (push 'ADD-XOR-JUST (n-a-env-consumers assumption)))
  (push assumption (class-assumptions class)))

;;; It seems cretinous to install consumers at such a low level, but this speeds
;;; but cases where assumptions are justified enormously.  
(defun add-xor-just (.consumer. assumption)
  .consumer.
  (dolist (non-simple-assumption
	    (class-non-simple-assumptions (assumption-variable assumption)))
    (justify-node *contra-node* (list 'XOR-ASSUMPTION assumption non-simple-assumption)))
  (push assumption (class-non-simple-assumptions (assumption-variable assumption))))

;;; Don't call this function externally.
(defun basic-make-assumption (variable value datum &aux assumption count env)
  (setq count (incf *assumption-counter*))
  (setq assumption (basic-make-assumption-internal count variable value datum))
  (setf (aref *assumption-array* count) assumption)
  (setq env (make-an-env (list assumption)))
  (setf (assumption-env assumption) env
	(assumption-justifications assumption)
	(list (make-just :CONSEQUENT assumption
			 :INFORMANT 'ASSUMING-MYSELF
			 :ANTECEDENTS (list assumption)
			 :COUNT 1)))
			 
  (cond (*simple-hybrid*
	 (setf (n-a-blocked assumption) (list env))
;	 ;;***** in-focus? check here seems stupid, must be a faster way.
;	 ;; **** how could it possibly be in-focus?
;	 (when (in-focus? env)
;	   (setf (assumption-envs assumption) (list env))
;	   )
	 (setf (env-waiting env) 1)
	 (unless *index-early* (index-env env (env-assumptions env)))
	 )
	(t (setf (assumption-envs assumption) (list env))))
  (if *trace-file*
      (format *trace-file* "~%BASIC-MAKE-ASSUMPTION ~D ~D"
	      count
	      (if (typep variable 'CLASS) (class-unique variable))))
  assumption)

;;; Doesn't allocate a position
;;; ***** not intrace file.
(defun lazy-basic-make-assumption (variable value datum &aux assumption)
  ;;******** this assumes -bits.
  (setq assumption
	(internal-make-assumption 'DELAY
				  variable
				  value
				  datum
				  'OUT
				  'DONT))
  (setf (assumption-justifications assumption)
	(list (make-just :CONSEQUENT assumption
			 :INFORMANT 'ASSUMING-MYSELF
			 :ANTECEDENTS (list assumption)
			 :COUNT 1
			 )))
  assumption)

(defun ensure-instantiated (assumption &aux flag)
  (when (eq (assumption-unique assumption) 'DELAY)
    (let ((count (incf *assumption-counter*))
	  (class (car (assumption-classes assumption)))
	  (offset nil) (bit nil) (env nil))
      (multiple-value-setq (offset bit) (floor count #.*word-size*))
      (setf (assumption-unique assumption) count)
      (setf (assumption-offset assumption) offset)
      (setf (assumption-bits assumption) (set-bit 0 bit))
      (setf (assumption-mask assumption) (byte 1 bit))
      (setf (aref *assumption-array* count) assumption)
      (setq env (make-an-env (list assumption)))
      (setf (assumption-env assumption) env)
      ;;; This assumes the assumption comes from a variable.
      (dolist (other (class-assumptions class))
	(cond ((eq other assumption))
	      ((eq (assumption-unique other) 'DELAY) (setq flag T))
	      (t (setf (assumption-binary-vector other)
		       (vector-cons3 assumption (assumption-binary-vector other)))
		 (setf (assumption-binary-vector assumption)
		       (vector-cons3 other (assumption-binary-vector assumption))))))
      ;; We could upate the envs caches for these singleton environments too.
      ;; This next is a bit of a klude.
      (let ((*going-nodes* nil))
	(cond (*simple-hybrid*
	       (cond ((null *foci*)
		      (if *index-early* (setf (env-waiting env) 1))
		      (update-node-real-hybrid assumption env))
		     ((and (neq *foci* :EMPTY)
			   (vector-member assumption (env-vector *good-foci*)))
		      (if *index-early* (setf (env-waiting env) 0)))
		     (t (setf (env-waiting env) 1)
			(setf (n-a-blocked assumption) (list env))
;;; Never index these.
			(unless *index-early* (index-env env (env-assumptions env)))
			(push assumption (env-nodes env)))))
	      (t (update-node1 assumption (list env) (list env))))
	(process-changed-nodes))
      ;; Close the class only if told to.
      (if (class-closed class)
	  (unless (or flag (class-or class))
	    (setf (class-or class)
		  (nxor (class-assumptions class))))))))

;;; This simply creates an assumption, thats all.
(defun create-assumption (datum) (basic-make-assumption nil nil datum))

(defun find-assumption (variable value)
  (if (eq value ':IN)
      (node-assumption variable)
      (dolist (assumption (class-assumptions variable))
	(if (eq value (assumption-value assumption)) (return assumption)))))

(defun compare-env (e1 e2 &aux count1 count2)
  (cond ((eq e1 e2) 'EQUAL)
	((eq e1 *empty-env*) 'SUBSET12)
	((eq e2 *empty-env*) 'SUBSET21)
	(t (setq count1 (env-count e1) count2 (env-count e2))
	   (cond ((< count1 count2) 
		  (if (vector-subset (env-vector e1) (env-vector e2)) 'SUBSET12))
		 ((> count1 count2) (if (vector-subset (env-vector e2) (env-vector e1))
		      'SUBSET21))))))

;;; Assumptions handling.
;;; Call fast-assumptions-union if possible.
(defun assumptions-union (e1 e2)
  (do ((entries nil))
      (nil)
    (cond ((null e1) (return (nreconc entries e2)))
	  ((null e2) (return (nreconc entries e1)))
	  ((eq (car e1) (car e2))
	   (push (car e1) entries)
	   (setq e1 (cdr e1))
	   (setq e2 (cdr e2)))
	 ((> (assumption-unique (car e1)) (assumption-unique (car e2)))
	   (push (car e1) entries)
	   (setq e1 (cdr e1)))
	  (t (push (car e2) entries)
	     (setq e2 (cdr e2))))))

;;; This is destructive right now.  This could be slightly sped up.
(defun assumptions-merge (l1 l2 &aux result tail)
  (do nil (nil)
    (cond ((null l1)
	   (cond ((null tail) (return l2))
		 (t (rplacd tail l2) (return result))))
	  ((null l2)
	   (cond ((null tail) (return l1))
		 (t (rplacd tail l1) (return result))))
	  ((eq (car l1) (car l2))
	   (if (null tail) (setq result l1) (rplacd tail l1))
	   (setq tail l1 l1 (cdr l1) l2 (cdr l2)))
	  ((> (assumption-unique (car l1)) (assumption-unique (car l2)))
	   (if (null tail) (setq result l1) (rplacd tail l1))
	   (setq tail l1 l1 (cdr l1)))
	  (t (if (null tail) (setq result l2) (rplacd tail l2))
	     (setq tail l2 l2 (cdr l2))))))


;;;******* in init-tms sometie.
(dotimes (i 3000.) (push (ncons nil) *fast-assumptions-conses*))

(defmacro push-cons (item list free-list)
  `(let ((.cons-cell. (pop ,free-list)))
     (rplaca .cons-cell. ,item)
     (rplacd .cons-cell. ,list)
     (setf ,list .cons-cell.)))

;;; The most commonly used idiom.  Called with two envs.  Returns ordered assumptions plus
;;; length.
(defun fast-assumptions-union (e1 e2 &aux as1 as2 conses length)
  (setq conses *fast-assumptions-conses*
	as1 (env-assumptions e1)
	as2 (env-assumptions e2)
	length (+ (env-count e1) (env-count e2)))
  (do ((entries nil))
      (nil)
    (cond ((null as1) (return (values (nreconc entries as2) length)))
	  ((null as2) (return (values (nreconc entries as1) length)))
	  ((eq (car as1) (car as2))
	   (decf length)
	   (push-cons (car as1) entries conses)
	   (setq as1 (cdr as1))
	   (setq as2 (cdr as2)))
	 ((> (assumption-unique (car as1)) (assumption-unique (car as2)))
	   (push-cons (car as1) entries conses)
	   (setq as1 (cdr as1)))
	 (t (push-cons (car as2) entries conses)
	    (setq as2 (cdr as2))))))

;;; With much experimentation, this has been determined to cons the least.
(defun parallel-assumptions-union (sets &aux result end best (length 0) conses cons count)
  (cond ((null sets) (values nil 0))
	((null (cdr sets)) (values (env-assumptions (car sets)) (env-count (car sets))))
;	((null (cddr sets))
;	 (multiple-value-setq (result length) (fast-assumptions-union (car sets) (cadr sets)))
;	 (values (fcopylist result) length))
			      
	(t (setq conses *fast-assumptions-conses* count (length sets))
	   (do ((sets sets (cdr sets)))
	       ((null sets))
	     (rplaca sets (env-assumptions (car sets))))
	   (do nil (nil)
	     ;; This recycles the fragment of the old assumptions list.
	     (cond ((= count 0) (return nil))
		   ((= count 1) (if end (rplacd end nil))
				(dolist (set sets)
				  (when set
				    (return-from parallel-assumptions-union
				      (copyconc result length set))))))

	     (setq best nil)
	     (dolist (set sets)
	       (cond ((null set))
		     ((null best) (setq best (car set)))
		     ((eq best (car set)))
		     ((assumption-orderp best (car set)))
		     (t (setq best (car set)))))
	     (unless best (return nil))
	     ;; This constructs the result in the correct order.
	     (setq cons (car conses) conses (cdr conses))
	     (cond (end (rplacd end cons)
			(rplaca cons best)
			(setq end cons))
		   (t (rplaca cons best)
		      (setq result cons end cons)))
	     (incf length)
	     (do ((sets sets (cdr sets)))
		 ((null sets))
	       (cond ((null (car sets)))
		     ((eq best (caar sets))
		      (rplaca sets (cdar sets))
		      (if (null (car sets)) (decf count))
		      )
		     ))
	     )
	   (if end (rplacd end nil))
	   (values (fcopylist1 result length) length))))

;;; Returns T if env has become contradictory.
;;; Remember to handle a case where the env is not in the hash table but a subsequent
;;; env is created and inserted in the hash table.
(defun generic-check-env? (env &aux assumptions)
  (cond ((simple-envp env)
	 (setq assumptions (tms::generic-env-assumptions-delay env))
	 (or (dolist (a assumptions) (if (assumption-contradictory a) (return a)))
	     (not (compatible-assumptions? assumptions (simple-env-vector env)))
	     (new-contradictory-env-assumptions? assumptions (simple-env-count env) T)))
	(t (env-contradictory env))))

(defun generic-check-env-why? (env &aux assumptions)
  (cond ((simple-envp env)
	 (setq assumptions (tms::generic-env-assumptions-delay env))
	 (or (dolist (a assumptions) (if (assumption-contradictory a) (return a)))
	     (incompatible-assumptions? assumptions (simple-env-vector env))
	     (new-contradictory-env-assumptions? assumptions (simple-env-count env) T)))
	(t (env-contradictory env))))

;;; Assumption is env has already been looked up.
(defun contradictory-env-assumptions? (env &aux reason assumptions)
  (setq assumptions (env-assumptions-delay env))
  (or (dolist (a assumptions)
	(if (setq reason (assumption-contradictory a)) (return reason)))
      (new-contradictory-env-assumptions? assumptions
					  (env-count env))))

;;; Saves a lot of conses.
(defvar *conses* (simple-make-list 100. nil))

;;; If lookup is nil then the vector is not in the hash table, otherwise this
;;; might find it.  This assumes that assumption sets of length 0, 1 and 2 have
;;; been processed earlier.  In addition this assumes that all contradictions of
;;; length 0, 1 and 2 have been checked for earlier.  This only consults nogoods of
;;; size 3 and larger.
(defun new-contradictory-env-assumptions? (assumptions count &optional lookup &aux end)
  (unless (< count 3)
    (if (> count *current-size*) (adjust-sizes count))
    ;;***** catch is usless now too.
    (catch 'SUBSUMED 
      ;; Turn assumptions into a list of integers terminated by nil with no consing.
      ;; Ignore any assumptions not appearing in any nogoods at all.
      (let ((conses *conses*))
	(dolist (a assumptions)
	  (cond ((assumption-nogoods a)
		 (rplaca conses (assumption-unique a))
		 (setq conses (cdr conses)))
		((< count 4) (return-from NEW-CONTRADICTORY-ENV-ASSUMPTIONS? nil))
		(t (decf count)
		   (setq lookup T))))
	(rplaca conses nil))
      (cond (*single-nogood-tree*
	     (subsumed-by-tree-4 count nil *conses* *nogood-tree*))
	    (t (setq end (min (if lookup count (1- count)) *max-contra-count*))
	       (do ((i 3 (1+ i)))
		   ((> i end) nil)
		 (subsumed-by-tree-1 (- count i) 
				     *conses*
				     (aref *nogood-trees* i))))))))
;
;(defun comp ()
;  (dotimes (i (1+ *max-env-count*))
;    (dolist (e (aref *environments* i))
;      (new-contradictory-env-assumptions? (env-assumptions e) (env-count e) T))))
;
;(defun new-contradictory-env-assumptionst? (assumptions count &optional lookup &aux r1 r2 start)
;  (setq start (time:fixnum-microsecond-time)
;	r1 (new-contradictory-env-assumptions1? assumptions count lookup))
;  (incf foo1 (time:time-difference (time:fixnum-microsecond-time) start))
;  (setq start (time:fixnum-microsecond-time)
;	r2 (new-contradictory-env-assumptions2? assumptions count lookup))
;  (incf foo2 (time:time-difference (time:fixnum-microsecond-time) start))
;  (unless (eq r1 r2) (error "Results are different"))
;  (push (list (fcopylist assumptions) count lookup) foo)
;  r1)
;
;(defun comp1 ()
;  (dolist (c foo)
;    (new-contradictory-env-assumptions1? (car c) (cadr c) (caddr c))))
;
;(defun comp2 ()
;  (dolist (c foo)
;    (new-contradictory-env-assumptions2? (car c) (cadr c) (caddr c))))
;
;(defun new-contradictory-env-assumptions2? (assumptions count &optional lookup &aux end)
;  (unless (or (< count 3)
;	      (dolist (a assumptions T) (if (assumption-nogoods a) (return nil))))
;    (if (> count *current-size*) (adjust-sizes count))
;    (catch 'SUBSUMED 
;      (setq end (min (if lookup count (1- count)) *max-contra-count*))
;      ;; Turn assumptions into a list of integers terminated by nil with no consing.
;      (do ((conses *conses* (cdr conses))
;	   (assumptions assumptions (cdr assumptions)))
;	  ((null assumptions) (rplaca conses nil))
;	(rplaca conses (assumption-unique (car assumptions))))
;      (do ((i 3 (1+ i)))
;	  ((> i end) nil)
;	(subsumed-by-tree-1 (- count i) 
;			    *conses*
;			    (aref *nogood-trees* i))))))


;;; Note that if assumption-nogoods are NIL assumptions can be skipped in subsumed-by-tree-2.
;;; Perhaps we should have a version like above.
(defun contradictory-env-assumptions3? (assumption assumptions count &aux end result tree)
  (cond ((< count 3) nil)
	((null (assumption-nogoods assumption)) nil)
	(*single-nogood-tree*
	 ;;***** if a lot of time is spent here, this can be fixed to call subsumed-tree-5
	 ;; and not to check on assumptions which aren't in any nogoods.
	 (subsumed-by-tree-5 count (assumption-unique assumption) assumptions *nogood-tree*))
	(t (setq end (min (1- count) *max-contra-count*))
	   (do ((i 3 (1+ i)))
	       ((> i end) nil)
	     (and (setq tree (aref *nogood-trees* i))
		  (setq result (subsumed-by-tree-2 (- count i) 
						   (assumption-unique assumption)
						   assumptions
						   tree))
		  (return result))))))

;;; **** the sort can be sped up.

;;; This checks whether the cons would be contradictory.  It only looks
;;; at nogoods 3 or greater.
;;; This function assumes:
;;;  [1] assumption is not part of assumptions.
;;;  [2] assumptions is consistent
;;;  [3] assumption is 2-consistent with assumptions
;;;  [4] assumption union assumptions is itself not a minimal nogood.
;;;  [5] count is the length of the resulting environment.

;;; Emperically********* it turns out to be much faster to use cons-assumption
;;; to build the simple envs and not do the sort.  But this code is probably obsolete any
;;; way now.
;;; ****** SMM does the sort which is really bad.

;;; ***** This should not really be called anymore --- this is too inefficient.
;;; 5/31/88 Note that this function assumes that a hash table lookup has already
;;; been done, so it kind find itself on the nogoods list.

;;; Warning this is an obvious kludge which can easily be fixed if needed....
(defun contradictory-cons? (assumption new-vector count)
  (cond ((or (< *max-contra-count* 3) (< count 4)) nil)
	(t (contradictory-env-assumptions3?
			      assumption
			      (blits-to-assumptions new-vector)
			      count))))

;;; This answers the question: Will adding assumption to env violate
;;; any nogoods.  This assumes nogoods of size less than 3 are checked elsewhere.
;;; Notice we could do stronger pruning of nogoods now in interpretation construction.
;;; ***** the commented out code does not seem to work.

;;; 5/31/88 Note that this assumes that the resulting environment has not been looked up.
;;; Therefore this could be a minimal nogood.  Hence one of the nogoods could be exactly
;;; the length of consed environment.
(defun contradictory-cons?-stack-new (assumption nogoods env &aux count vector)
;  (contradictory-env-assumptions3? assumption
;				   (generic-env-assumptions env)
;				   (1+ (generic-env-count env))))

  (cond ((null nogoods) nil)
	;; If all nogoods are singletons or doubles --- don't do anything.
	((< *max-contra-count* 3) nil)
	;; If the resultant environment is less than 3 (*** but why are we called then), then
	;; it presumed to have been checked elsewhere.
	((< (setq count (1+ (generic-env-count env))) 3) nil)
	;; If the result environment is exactly of size 3, then it is nogood only
	;; it itself is a minimal nogood which can be checked in various ways.
	;; For now now we just drop through to the general case, but the
	;; case of size 3 can clearly be optimized.
	(t (setq vector (generic-env-vector env))
	   (dolist (nogood nogoods)
	     (and (eq (car (env-contradictory-info nogood)) 'BASE)
		  (<= (env-count nogood) count)
		  (vector-subset2 (env-vector nogood) vector assumption)
		  (return T))))))

;;; This is now more general, and checks for any binary contradiction.  This
;;; could be integrated into union-env.
;;;***** Note that if cons-caches were complete, this would never fail.
;;; Should be called incompatibl-env? really.

;;; Note that any attempt to cache (cf. the commented out code, only slows things down.
;;; Why I don't really know.

;;; As an experiment this now updates the caches in question such that compatible-env?
;;; will never get called again.

(defun compatible-env? (e1 e2 &aux vector cache)
  (if *ltms* (return-from compatible-env? t))
  (and *simple-hybrid*
       (eq (env-waiting e1) 0)
       (eq (env-waiting e2) 0)
       (return-from compatible-env? T))
  (if ( (env-count e2) (env-count e1)) (psetq e1 e2 e2 e1))
  (setq vector (env-vector e2))
  (not (dolist (a (env-assumptions-delay e1))
	 (when (vector-intersection? (assumption-binary-vector a) vector)
	   (if (setq cache (env-cons-env-cache e1))
	       (rplaca cache (vector-union-old (car cache) (assumption-binary-vector a)))
	       (setf (env-cons-env-cache e1) (ncons (fcopylist (assumption-binary-vector a)))))
	   (if (setq cache (env-cons-env-cache e2))
	       (rplaca cache (vector-cons4 a (car cache)))
	       (setf (env-cons-env-cache e2) (ncons (vector-cons4 a nil))))
;	   (update-env-cache-vector e1)
;	   (update-env-cache-vector e2)
	   (return T)))))

(defun generic-compatible-env? (e1 e2 &aux vector cache)
  (if ( (generic-env-count e2) (generic-env-count e1)) (psetq e1 e2 e2 e1))
  (setq vector (generic-env-vector e2))
  (not (dolist (a (generic-env-assumptions-delay e1))
	 (when (vector-intersection? (assumption-binary-vector a) vector)
	   (if (simple-envp e1)
	       (if (setq cache (simple-env-cons-env-cache e1))
		   (setf (simple-env-cons-env-cache e1)
			 (vector-union-old cache (assumption-binary-vector a)))
		   (setf (simple-env-cons-env-cache e1)
			 (fcopylist (assumption-binary-vector a))))
	       (if (setq cache (env-cons-env-cache e1))
		   (rplaca cache (vector-union-old (car cache)
						   (assumption-binary-vector a)))
		   (setf (env-cons-env-cache e1)
			 (ncons (fcopylist (assumption-binary-vector a))))))
	   (if (simple-envp e2)
	       (if (setq cache (simple-env-cons-env-cache e2))
		   (setf (simple-env-cons-env-cache e2) (vector-cons4 a cache))
		   (setf (simple-env-cons-env-cache e2) (vector-cons4 a nil)))
	       (if (setq cache (env-cons-env-cache e2))
		   (rplaca cache (vector-cons4 a (car cache)))
		   (setf (env-cons-env-cache e2) (ncons (vector-cons4 a nil)))))
;	   (update-env-cache-vector e1)
;	   (update-env-cache-vector e2)
	   (return T)))))

(defun compatible-assumptions? (assumptions vector &aux abv)
  (not (dolist (a assumptions)
	 ;; First test avoids the function call, which seems to yield a slight improvement.
	 (and (setq abv (assumption-binary-vector a))
	      (vector-intersection? abv vector)
	      (return T)))))

;;; This returns the pair of inconsistent assumptions.
;;; ***** can be more efficient.
(defun incompatible-assumptions? (assumptions vector &aux abv)
  (dolist (a assumptions)
    ;; First test avoids the function call, which seems to yield a slight improvement.
    (and (setq abv (assumption-binary-vector a))
	 (vector-intersection? abv vector)
	 (dolist (b assumptions)
	   (cond ((eq a b))
		 ((vector-member a (assumption-binary-vector b))
		  (return-from incompatible-assumptions? (list a b))))))))

(defmacro search-assumption-nogoods (count env assumption v)
  `(progn (setq ,count (1+ (env-count ,env)))
	  (do ((nogoods (assumption-nogoods ,assumption))
	       (nogood nil)
	       (previous nil))
	      ((null nogoods) nil)
	    (setq nogood (car nogoods))
	    (cond ((neq (car (env-contradictory-info nogood)) 'BASE)
		   (setq nogoods (cdr nogoods))
		   (cond (previous (rplacd previous (cdr previous)))
			 (t (setf (assumption-nogoods assumption) nogoods))))
		  ((and (< (env-count nogood) count) (vector-subset (env-vector nogood) ,v))
		   (return T))
		  (t (setq previous nogoods nogoods (cdr nogoods)))))))

;;; These are the same except for count.
(defmacro generic-search-assumption-nogoods (count env assumption v)
  `(progn (setq ,count (1+ (generic-env-count ,env)))
	  (do ((nogoods (assumption-nogoods ,assumption))
	       (nogood nil)
	       (previous nil))
	      ((null nogoods) nil)
	    (setq nogood (car nogoods))
	    (cond ((neq (car (env-contradictory-info nogood)) 'BASE)
		   (setq nogoods (cdr nogoods))
		   (cond (previous (rplacd previous (cdr previous)))
			 (t (setf (assumption-nogoods assumption) nogoods))))
		  ((and (< (env-count nogood) count) (vector-subset (env-vector nogood) ,v))
		   (return T))
		  (t (setq previous nogoods nogoods (cdr nogoods)))))))

;		 ((progn (setq count (1+ (env-count env)))
;			 (dolist (nogood (assumption-nogoods assumption))
;			   (and (eq (car (env-contradictory-info nogood)) 'BASE)
;				(< (env-count nogood) count)
;				(vector-subset (env-vector nogood) v)
;				(return T))))



;;; For speed-time tradeoff this maintains a cache.  This cache can be flushed
;;; at any time to get more space.
;;; ****** when a contradiction is found, the relevant caches are not updated ********
;;; ****** this would be one way to gain space.
;;; ****** I'm pretty convinced that justifying assumptions won't work because
;;; cons-env for example assumptions assumptions have singleton envs slots etc.
(defun cons-env (env assumption &aux ptr v ov count cache nenv)
  ;; **** notice that we represent binary inconssitencies twice.  Once in the
  ;; in the cache, another in the vector-intersecton?
  (cond	((= (env-count env) 1) (double assumption (car (env-assumptions env))))
	((env-contradictory env) env)
	((i-true? assumption) env)
	((assumption-contradictory assumption) *contra-env*)
	((vector-member assumption (setq ov (env-vector env))) env)
	((eq *empty-env* env) (assumption-env assumption))
	((and (setq cache (env-cons-env-cache env))
	      (cond ((vector-member assumption (car cache))
		     (return-from CONS-ENV *contra-env*))
		    ;;****** this test maybe should be integrated into the fast versions.
		    ((vector-intersection? (assumption-binary-vector assumption) ov)
		     (rplaca cache (vector-cons3 assumption (car cache)))
		     (return-from CONS-ENV *contra-env*))
		    ((or (null (cdr cache))
			 (null (setq nenv (gethash assumption (cdr cache)))))
		     nil)
		    ((env-contradictory nenv)	
		     (rplaca cache (vector-cons3 assumption (car cache)))
		     (if (cdr cache) (remhash assumption (cdr cache)))
		     (return-from CONS-ENV nenv))
		    (T (return-from CONS-ENV nenv)))))
	;;**** fsat versions haven't got this either.
	((and (null cache) (vector-intersection? (assumption-binary-vector assumption) ov))
	 (setf (env-cons-env-cache env) (ncons (vector-cons3 assumption nil)))
	 *contra-env*)

	(t (unless cache (setf (env-cons-env-cache env) (setq cache (ncons nil))))
	   ;; *** Fast version has a spurious clause here which is better above.
	   (cond ((setq nenv
			(hash-slot-value (setq ptr
					       (nget-or-puthash-env
						 (setq v (vector-cons4 assumption ov))
						 *env-hash-table*))))
		  (if (env-contradictory nenv)
		      ;; Singleton environment's use the assumption-binary-vector.
		      (unless (< (env-count env) 2)
			(rplaca cache (vector-cons3 assumption (car cache))))
		      (progn (unless (cdr cache)
			       (rplacd cache (make-tms-hash-table :size 5.)))
			     (setf (gethash assumption (cdr cache)) nenv)))
		  nenv)
		 ;;*** for big problems we just have to prune this from subsumptions.
		 ;;*** the other solution is to prune upon deletion.
		 ((search-assumption-nogoods count env assumption v)
		  (hash-slot-set ptr v *env-hash-table*)
		  (setf (aref *hashes* count) T)
		  ;; Note that we could never get here unless count is at least 3, so
		  ;; we will never windup updating the cache of a singleton.
		  (rplaca cache (vector-cons3 assumption (car cache)))
		  *contra-env*)
		 (t (setq nenv (make-an-env-2 count
					      (if *delay-assumptions*
						  :DELAY
						  (cons-assumption (env-assumptions env)
								   assumption))
					     v))
		    (hash-slot-set ptr nenv *env-hash-table*)
		    (setf (aref *hashes* count) T)
		    (progn (unless (cdr cache)
			     (rplacd cache (make-tms-hash-table :size 10)))
			   (setf (gethash assumption (cdr cache)) nenv))
		    ;; **** we could update the old cache first?
		    (set-env-cache nenv (car cache) (assumption-binary-vector assumption))
		    (when *index-early*
		      (setf (env-waiting nenv) (env-waiting env))
		      (unless (assumption-in-focus assumption)
			(decf (env-waiting nenv))))
		    nenv)))))

(defvar *delay-assumptions* T)

(defun scan-delay ()
  (dotimes (i (array-length *environments*))
    (dolist (e (aref *environments* i))
      (cond ((env-contradictory e))
	    ((<= (env-count e) 2))
	    ((eq (env-assumptions e) :DELAY))
	    (t (format t "~%~A has assumptions, should be delayed" e))))))

;;; This checks to see whether an cons-env will be inconsistent, without actually
;;; constructing it.
(defun contradictory-cons-env? (env assumption &aux v ov count cache nenv)
  ;; **** notice that we represent binary inconssitencies twice.  Once in the
  ;; in the cache, another in the vector-intersecton?
  (cond	((env-contradictory env))
	((= (env-count env) 1)
	 (env-contradictory (double assumption (car (env-assumptions env)))))
	((i-true? assumption) nil)
	((assumption-contradictory assumption) T)
	((vector-member assumption (setq ov (env-vector env))) nil)
	((eq *empty-env* env) nil)
	((and (setq cache (env-cons-env-cache env))
	      (cond ((vector-member assumption (car cache)) T)
		    ;;****** this test maybe should be integrated into the fast versions.
		    ((vector-intersection? (assumption-binary-vector assumption) ov)
		     (rplaca cache (vector-cons3 assumption (car cache)))
		     T)
		    ((or (null (cdr cache))
			 (null (setq nenv (gethash assumption (cdr cache)))))
		     nil)
		    ((env-contradictory nenv)	
		     (rplaca cache (vector-cons3 assumption (car cache)))
		     (if (cdr cache) (remhash assumption (cdr cache)))
		     T)
		    (t (return-from CONTRADICTORY-CONS-ENV? nil)))))
	;;**** fsat versions haven't got this either.
	((and (null cache) (vector-intersection? (assumption-binary-vector assumption) ov))
	 (setf (env-cons-env-cache env) (ncons (vector-cons3 assumption nil)))
	 T)

	(t (unless cache (setf (env-cons-env-cache env) (setq cache (ncons nil))))
	   ;; *** Fast version has a spurious clause here which is better above.
	   (cond ((setq nenv (gethash-env (setq v (vector-cons4 assumption ov))
					  *env-hash-table*))
		  (if (env-contradictory nenv)
		      ;; Singleton environment's use the assumption-binary-vector.
		      (unless (< (env-count env) 2)
			(rplaca cache (vector-cons3 assumption (car cache))))
		      (progn (unless (cdr cache)
			       (rplacd cache (make-tms-hash-table :size 5.)))
			     (setf (gethash assumption (cdr cache)) nenv)))
		  (env-contradictory nenv))
		 ;;*** for big problems we just have to prune this from subsumptions.
		 ;;*** the other solution is to prune upon deletion.
		 ((search-assumption-nogoods count env assumption v)
		  (rplaca cache (vector-cons3 assumption (car cache)))
		  T)))))


;;; A specialization of cons-env for false.  Changes in cons-env should perculate here.
;;; I think this makes no assumptions at all about the input.
(defun cons-for-false (env assumption reason &optional (swp T)
		       &aux ptr v ov count cache nenv)
  (cond ((= (env-count env) 1)
	 (double-for-false assumption (car (env-assumptions env)) reason swp))
	((env-contradictory env) env)
	((i-true? assumption)
	 (contradictory-env env `(BASE CONS-FOR-FALSE ,reason) t swp))
	((assumption-contradictory assumption) *contra-env*)
	((eq *empty-env* env)
	 (contradictory-env (assumption-env assumption) `(BASE CONS-FOR-FALSE ,reason) t swp))
	((vector-member assumption (setq ov (env-vector env)))
	 (contradictory-env env `(BASE CONS-FOR-FALSE ,reason) t swp))
	((and (setq cache (env-cons-env-cache env))
	      (cond ((vector-member assumption (car cache)) *contra-env*)
		    ((vector-intersection? (assumption-binary-vector assumption) ov)
		     (rplaca cache (vector-cons3 assumption (car cache)))
		     *contra-env*)
		    ((or (null (cdr cache))
			 (null (setq nenv (gethash assumption (cdr cache)))))
		     nil)
		    ((env-contradictory nenv)
		     (rplaca cache (vector-cons3 assumption (car cache)))
		     (if (cdr cache) (remhash assumption (cdr cache)))
		     nenv)
		    (t ;(error "HI")
		       (contradictory-env nenv `(BASE CONS-FOR-FALSE ,reason) t swp) nenv))))
	((and (null cache) (vector-intersection? (assumption-binary-vector assumption) ov))
	 (setf (env-cons-env-cache env) (ncons (vector-cons3 assumption nil)))
	 *contra-env*)
	;;; This sticks the contra-env in the hash table, which may not be worth it?
	;;; This actually creates the env, which may be futile???
	(t (unless cache (setf (env-cons-env-cache env) (setq cache (ncons nil))))

	   (cond ((setq nenv
			(hash-slot-value (setq ptr
					       (nget-or-puthash-env
						 (setq v (vector-cons4 assumption ov))
						 *env-hash-table*))))
		  (unless (< (env-count env) 2)
		    (rplaca cache (vector-cons3 assumption (car cache))))
		  (unless (env-contradictory nenv)
		    ;(error "HI")

		    (contradictory-env nenv `(BASE CONS-FOR-FALSE ,reason) t swp))
		  nenv)
		 ;; This table gets extremely big.  And is probably a bad idea.
		 ;;***** make this a macro and use it everywhere.
		 ((search-assumption-nogoods count env assumption v)
		  (hash-slot-set ptr v *env-hash-table*)
		  (setf (aref *hashes* count) T)
		  ;; Note that we could never get here unless count is at least 3, so
		  ;; we will never windup updating the cache of a singleton.
		  (rplaca cache (vector-cons3 assumption (car cache)))
		  *contra-env*)
		 ;; Does this make sense, actually stuffing the env in the hash table?
		 ;; This does not make that much sense.  We could skip this easily if
		 ;; we allowed lists in the descrimination net too.
		 (t (setq nenv (make-an-env-2 count
					      (if *delay-assumptions*
						  (blits-to-assumptions v)
						  (cons-assumption (env-assumptions env)
								   assumption))
					     v
					     t))
		    (hash-slot-set ptr nenv *env-hash-table*)
		    (setf (aref *hashes* count) T)
		    (when (and *simple-hybrid* *index-early*)
		      (setf (env-waiting nenv)
			    (if (assumption-in-focus assumption)
				(env-waiting env)
				(1+ (env-waiting env)))))
		      
		    (contradictory-env nenv `(BASE CONS-FOR-FALSE ,reason) t swp)
		    (rplaca cache (vector-cons3 assumption (car cache)))
		    nenv)))))

;;; Double-for-false assumes nothing about the incoming assumptions.
(defun double-for-false (a b reason &optional (swp T) &aux env cache nenv v)
  (cond ((eq a b)
	 (contradictory-env (assumption-env a) `(BASE DOUBLE-FOR-FALSE ,reason) t swp))
	((i-false? a))
	((i-false? b))
	((i-true? a)
	 (contradictory-env (assumption-env b) `(BASE DOUBLE-FOR-FALSE ,reason) t swp))
	((i-true? b)
	 (contradictory-env (assumption-env a) `(BASE DOUBLE-FOR-FALSE ,reason) t swp))
	((vector-member a (assumption-binary-vector b)))
	(t (if (> (assumption-unique a) (assumption-unique b)) (psetq a b b a))
	   ;;**vector-cons4 is overkill here.  In fact this list structure could
	   ;;be recycled.  i.e., it could be a stack-list**
	   (setq env (assumption-env a))
	   (cond ((and (setq cache (env-cons-env-cache env))
		       (cdr cache)
		       (setq nenv (gethash b (cdr cache))))
		  ;; *should we also update the cache?????? removing the nenv
		  ;; *and updating the cons vector?
		  (contradictory-assumption-pair a b)
		  (contradictory-env nenv `(BASE DOUBLE-FOR-FALSE ,reason) t swp))
		 (t (setq v (vector-cons4 a (env-vector (assumption-env b)))
			  nenv (make-an-env-2 2 (list b a) v T))
		    ;; If we want explanations, then stick it in the hash table
		    ;; because thats the only place we'll be able to get the nogood from.
		    (when *explain-flag*
		      (unless cache
			(setq cache (ncons nil))
			(setf (env-cons-env-cache (assumption-env a)) cache))
		      (unless (cdr cache) 
			(rplacd cache (make-tms-hash-table :size 5.)))
		      (setf (gethash b (cdr cache)) nenv))

		    ;; *** does contradictory-env automatically update the cache
		    ;; *** or should we do that here?
		    ;; *** if resolution wasn't on, it wouldn't be worth creating the env
		    ;; *** is it worth having the vector?
		    (contradictory-assumption-pair a b)
		    (contradictory-env nenv `(BASE DOUBLE-FOR-FALSE ,reason) t swp))))))

;;; It might be worth pruning the caches of singleton environments of contradictory envs.

;;; This combines two assumptions into a double environment.  It assumes:
;;; Note that the cache's for singleton environments are thus a little different
;;; than for other environments, the lower environment points to the higher one, but
;;; not the other way around.
;;; Note that double environments will no longer appear in the hash table.
(defun double (a1 a2 &aux v cache nenv env)
        ;; First check the trivial cases, this assumes nothing about the incoming assumptions.
  (cond ((i-false? a1) *contra-env*)
	((i-false? a2) *contra-env*)
	((i-true? a1) (if (i-true? a2) *empty-env* (assumption-env a2)))
	((i-true? a2) (assumption-env a1))
	((eq a1 a2) (assumption-env a1))
	;; Binary vectors are stored duplicately, so we need to test this only one way.	
	((vector-member a1 (assumption-binary-vector a2)) *contra-env*)
	(t (if (> (assumption-unique a1) (assumption-unique a2)) (psetq a1 a2 a2 a1))
	   (setq env (assumption-env a1))
	   (cond ((and (setq cache (env-cons-env-cache env))
		       (cdr cache)
		       (gethash a2 (cdr cache))))
		 (t (unless cache (setf (env-cons-env-cache env) (setq cache (ncons nil))))
		    (setq v (vector-cons4 a2 (env-vector env)))
		    (setq nenv (make-an-env-2 2 (list a2 a1) v))
		    (when (and *simple-hybrid* *index-early*)
		      (setf (env-waiting nenv)
			    (if (assumption-in-focus a1)
				(if (assumption-in-focus a2) 0 1)
				(if (assumption-in-focus a2) 1 2))))
		    (unless (cdr cache) (rplacd cache (make-tms-hash-table :size 10)))
		    (setf (gethash a2 (cdr cache)) nenv)
		    (set-env-cache nenv (assumption-binary-vector a1)
				        (assumption-binary-vector a2))
			    
		    nenv)))))

;;; This is just for efficiency.
(defun set-env-cache (env v1 v2)
  (if v1
      (setf (env-cons-env-cache env)
	    (ncons (if v2
		       (vector-union-new v1 v2)
		       (fcopylist v1)
		       )))
      (if v2 (setf (env-cons-env-cache env) (ncons (fcopylist v2))))))

(defun get-env-cache (v1 v2)
  (if v1
       (if v2
	   (vector-union-new v1 v2)
	   (fcopylist v1)
	   )
      (if v2 (fcopylist v2))))

;;; Finds the double environment, even if we don't want it.
;;; ****** this assumes the hashes never get cleared out.  Is that a valid assumption tomake?
(defun double-if-exists (a1 a2 &aux env cache)
  (if (> (assumption-unique a1) (assumption-unique a2)) (psetq a1 a2 a2 a1))
  (setq env (assumption-env a1))
  (and (setq cache (env-cons-env-cache env)) (cdr cache) (gethash a2 (cdr cache))))

;;; Try this some time.
(defun make-generic-env (assumptions &aux env v cache)
  (cond ((null assumptions) *empty-env*)
	((null (cdr assumptions))
	 (setq env (assumption-env (car assumptions)))
	 (unless (env-contradictory env) env))
	((null (cddr assumptions)) (double (car assumptions) (cadr assumptions)))
	((setq env (gethash-env (setq v (make-env-vector* assumptions)) *env-hash-table*))
	 (unless (env-contradictory env) env))
	((not (compatible-assumptions? assumptions v)) nil)
	((new-contradictory-env-assumptions? assumptions (length assumptions)) nil)
	;; This does not create cache.
	(t (setq cache (fcopylist (assumption-binary-vector (car assumptions))))
	   (dolist (a (cdr assumptions))
	     (setq cache (vector-union-old cache (assumption-binary-vector a))))
	   (make-simple-env (length assumptions)
			    nil
			    assumptions
			    v))))

;;;***** fix this.
;(defun make-generic-env (assumptions &aux result) 
;  (setq result *empty-env*)
;  (dolist (asn assumptions result)
;    (setq result (generic-cons-env result asn))
;    (unless result (return-from make-generic-env nil))))

;;; This accepts and will return simple-envs. It is used
;;; experimentally in interpretation construction.  Simple-envs are lists.

(defun generic-cons-env (env assumption &aux v ov count cache nenv)
  ;; **** notice that we represent binary inconssitencies twice.  Once in the
  ;; in the cache, another in the vector-intersecton?
  (cond	((= (generic-env-count env) 1)
	 (setq env (double assumption (car (generic-env-assumptions env))))
	 (if (not (env-contradictory env)) env))
	((and (not (simple-envp env)) (env-contradictory env)) nil)
	((i-true? assumption) env)
	((assumption-contradictory assumption) nil)
	((vector-member assumption (setq ov (generic-env-vector env))) env)
	((eq *empty-env* env) (assumption-env assumption))
	((if (simple-envp env)
	     (and (setq cache (simple-env-cons-env-cache env))
		  (cond ((vector-member assumption cache)
			 (return-from GENERIC-CONS-ENV nil))
			((vector-intersection? (assumption-binary-vector assumption) ov)
			 (setf (simple-env-cons-env-cache env)
			       (vector-cons3 assumption cache))
			 (return-from GENERIC-CONS-ENV nil))))
	     (and (setq cache (env-cons-env-cache env))
		  (cond ((vector-member assumption (car cache))
			 (return-from GENERIC-CONS-ENV nil))
			;;****** this test maybe should be integrated into the fast versions.
			((vector-intersection? (assumption-binary-vector assumption) ov)
			 (rplaca cache (vector-cons3 assumption (car cache)))
			 (return-from GENERIC-CONS-ENV nil))
			((or (null (cdr cache))
			     (null (setq nenv (gethash assumption (cdr cache)))))
			 nil)
			((env-contradictory nenv)	
			 (rplaca cache (vector-cons3 assumption (car cache)))
			 (if (cdr cache) (remhash assumption (cdr cache)))
			 nil)
			(nenv)))))
	((and (null cache) (vector-intersection? (assumption-binary-vector assumption) ov))
	 (if (simple-envp env)
	     (setf (simple-env-cons-env-cache env) (vector-cons3 assumption nil))
	     (setf (env-cons-env-cache env) (ncons (vector-cons3 assumption nil))))
	 nil)
	(t (or cache
	       (simple-envp env)
	       (setf (env-cons-env-cache env) (setq cache (ncons nil))))
	   ;; *** Fast version has a spurious clause here which is better above.
	   (cond ((setq nenv (gethash-env (setq v (vector-cons4 assumption ov))
					  *env-hash-table*))
		  (cond ((env-contradictory nenv)
			 ;; Singleton environment's use the assumption-binary-vector.
			 (unless (< (generic-env-count env) 2)
			   (if (simple-envp env)
			       (setf (simple-env-cons-env-cache env)
				     (vector-cons3 assumption cache))
			       (rplaca cache (vector-cons3 assumption (car cache)))))
			 nil)
			(nenv)))
		 ((generic-search-assumption-nogoods count env assumption v)
		  (if (simple-envp env)
		      (setf (simple-env-cons-env-cache env) (vector-cons3 assumption cache))
		      (rplaca cache (vector-cons3 assumption (car cache))))
		  nil)
		 (t (make-simple-env count
				     (vector-union-new (if (simple-envp env) cache (car cache))
						       (assumption-binary-vector assumption))
				     (cons-assumption (generic-env-assumptions env)
						      assumption)
				     v))))))

;;; Use this when you are relatively sure you don't care about the env.  This exploits
;;; all the ATMS caches, but doesn't update them.  This assumes
;;; [1] Incoming environment is consistent.
;;; [2] Assumption is not true or false.
;;; [3] Assumption is not part of env.
;;; If ignore-hash is T, then if simple-result-ok is not T, then this will not look the
;;; new environment up in the hash table to see if by coincidence it is there.  For
;;; some purposes this is very important.  For others this can cause a bug.
;;; I no longer understand what ignore-hash is for.  The way I originally wrote it is
;;; buggy.  Remember if the simple environment we just create is a nogood.
(defun fast-cons-env (env assumption simple-result-ok &optional ignore-hash)
  (setq ignore-hash nil)
  (cond ((simple-envp env) (fast-cons-vector3 env assumption simple-result-ok ignore-hash))
	(simple-result-ok (fast-cons-env1 env assumption))
	;; We could call just an uncaching version of cons-env, but thats probably
	;; not worth the effort...?????
	(t (cons-env env assumption))))





;;; A faster lookup.  This could be optimized.  Many lookup's during interpretation 
;;; construction will be for non-existant sizes.
;;;***** Note *hashes* might be useful for many things.  At the moment
;;; Length is called far to often to set it.  Look at every setf.
;;; Note that this assumes new-count and new-vector have to be set in any case.
;;; Leave the comparison with *max-env-count* in because count may be beyond length.
(defmacro lookup-cons-vector (assumption new-vector old-vector new-count old-count)
  `(progn (setq ,new-vector (vector-cons4 ,assumption ,old-vector)
		,new-count (1+ ,old-count))
	  (and ( ,new-count *max-env-count*)
	       (aref *hashes* ,new-count)
	       (gethash-env ,new-vector *env-hash-table*))))

(defmacro lookup-cons-vector? (assumption new-vector old-vector new-count old-count)
  `(progn (setq ,new-vector (vector-cons4 ,assumption ,old-vector)
		,new-count (1+ ,old-count))
	  (and (not ignore-hash)
	       ( ,new-count *max-env-count*)
	       (aref *hashes* ,new-count)
	       (gethash-env ,new-vector *env-hash-table*))))

;;; This fast-cons takes an env as input and may output a simple env.
;;; *** This could be slightly optimized so that doubling created simple environments.
(defun fast-cons-env1 (env assumption &aux v ov count cache nenv)
  (cond ((= (env-count env) 1)
	 (double assumption (car (env-assumptions-delay env))))
	((eq *empty-env* env) (assumption-env assumption))
	((and (setq cache (env-cons-env-cache env))
	      (cond ((vector-member assumption (car cache)) *contra-env*)
		    ((or (null (cdr cache))
			 (null (setq nenv (gethash assumption (cdr cache)))))
		     nil)
		    ;;**** this test seems pointless.
		    ((env-contradictory nenv) nenv)
		    (t nenv))))
	((vector-intersection? (assumption-binary-vector assumption)
			       (setq ov (env-vector env)))
	 *contra-env*)
	((lookup-cons-vector assumption v ov count (env-count env)))
	;;*** The following call is ridiculous as it does stupid things.  Conses
	;; too much and doesn't need a sort.
	((contradictory-cons? assumption v count) *contra-env*)
	(t ;(update-env-cache cache)
	 
	 (make-simple-env count
			  (get-env-cache (car cache) (assumption-binary-vector assumption))
			  (if *delay-assumptions*
			      :DELAY
			      (cons-assumption (env-assumptions env) assumption))
			  v))))

(defun simple-to-env (simple-env &aux v nenv ptr assumptions delay)
  (unless (simple-envp simple-env) (return-from simple-to-env simple-env))
  (setq assumptions (simple-env-assumptions simple-env))
  (when (eq assumptions :DELAY)
    (setq delay t)
    (setq assumptions (blits-to-assumptions (setq v (simple-env-vector simple-env)))))
  (cond ((null assumptions) *empty-env*)
	((null (cdr assumptions)) (assumption-env (car assumptions)))
	((null (cddr assumptions)) (double (car assumptions) (cadr assumptions)))
	((hash-slot-value (setq ptr (nget-or-puthash-env
				      (or v (setq v (simple-env-vector simple-env)))
				      *env-hash-table*))))
	(t ;;;**** this is stupid.  When this is debugged, we don't need to check
	   ;;; for consistency anymore.  
	   (setq nenv (make-an-env-3 (simple-env-count simple-env)
				     (if delay (fcopylist assumptions) assumptions)
				     v))
	   (hash-slot-set ptr nenv *env-hash-table*)
	   (setf (aref *hashes* (simple-env-count simple-env)) T)
	   (setf (env-cons-env-cache nenv) (ncons (simple-env-cons-env-cache simple-env)))
	   nenv)))

;;; This is a fast-cons-env2 which assumes the hard case.
;;; *** This could be slightly optimized so that doubling created simple environments.
(defun fast-cons-env2 (env assumption ov cache &aux v count)
  (cond ((= (env-count env) 1)
	 (double assumption (car (env-assumptions env))))
	((lookup-cons-vector assumption v ov count (env-count env)))
		;;*** could keep sorted if *tree-flag-on*?
	((contradictory-cons? assumption v count) *contra-env*)
	(t ;(update-env-cache cache)
	 (make-simple-env count
			  (vector-union-new (car cache)
					    (assumption-binary-vector assumption))
			  (cons assumption (env-assumptions env))
			  v))))

;;; Like fast-cons-env2-stack, however, the result is guaranteed consistent because
;;; of forward checking.  Doesn't check gethash --- the environment wanted is
;;; hardly ever there.
(defun fast-cons-env2-stack-new (result env assumption ov)
  (cond ((= (env-count env) 1)
	 (double assumption (car (env-assumptions env))))
	(t (setf (simple-env-count result) (1+ (env-count env))
		 (simple-env-cons-env-cache result) nil
		 (simple-env-assumptions result)
		 (if *delay-assumptions* :delay
		     (cons-assumption (env-assumptions env) assumption))
		 (simple-env-vector result) (vector-cons4 assumption ov))
	   result)))

;;; Like fast-cons-vector2-stack, however, the result is guaranteed consistent because
;;; of forward checking.  Doesn't check gethash --- the environment wanted is
;;; hardly ever there.
(defun fast-cons-vector2-stack-new (result simple-env assumption ov)
  (cond ((= (simple-env-count simple-env) 1)
	 (double assumption (car (simple-env-assumptions simple-env))))
	(t (setf (simple-env-count result) (1+ (simple-env-count simple-env))
		 (simple-env-cons-env-cache result) nil
		 (simple-env-assumptions result)
		 (if *delay-assumptions* :delay
		     (cons-assumption (simple-env-assumptions simple-env) assumption))
		 (simple-env-vector result) (vector-cons4 assumption ov))
	   result)))

;;; All statistics previous to 1/20/88 are suspect because cons-env-cache-vector
;;; had a serious bug in it.  I don't know how it ever worked right before then.
(defun update-env-cache-vector (e &aux cache as)
  (setq cache (env-cons-env-cache e) as (env-assumptions e))
  (unless (or cache (null as))
    (setq cache (ncons (fcopylist (assumption-binary-vector (pop as)))))
    (setf (env-cons-env-cache e) cache))
  (dolist (a as)
    (rplaca cache (vector-union-old (car cache) (assumption-binary-vector a)))))

;;; I think this is worth it, but its unclear.  Maybe every cache should have a checkpoint
;;; when it should be updated.  This could be used in all the variations of cons-env.
(defun update-env-cache (cache)
  (error "I don't think this is implemented for hash caches")
  (do ((previous cache) (next (cdr cache)))
      ((null next))
    (cond ((env-contradictory (cdr next))
	   (rplaca cache (vector-cons3 (car next) (car cache)))
	   (rplacd previous (cdr next))
	   (setq next (cdr next)))
	  (t (setq previous next next (cdr next))))))

;;; *** This could be slightly optimized so that doubling created simple environments.
(defun fast-cons-vector (simple-env assumption simple-result-ok &aux ov v count cache
				    ptr nenv) 
  (cond ((= (simple-env-count simple-env) 1)
	 (double assumption (car (simple-env-assumptions simple-env))))
	((vector-member assumption
			(setq cache (simple-env-cons-env-cache simple-env)))
	 *contra-env*)
	((vector-intersection? (assumption-binary-vector assumption)
			       (setq ov (simple-env-vector simple-env)))
	 *contra-env*)
	((null simple-result-ok)
	 (cond ((hash-slot-value (setq ptr (nget-or-puthash-env
					     (setq v (vector-cons4 assumption ov))
					     *env-hash-table*))))
	       ((contradictory-cons? assumption v
				     (setq count (1+ (simple-env-count simple-env))))
		(hash-slot-set ptr v *env-hash-table*)
		(setf (aref *hashes* count) T)
		*contra-env*)
	       (t (setq nenv
			(make-an-env-3 count
				       (cons assumption
					     (simple-env-assumptions simple-env))
				       v))
		  (hash-slot-set ptr nenv *env-hash-table*)
		  (setf (aref *hashes* count) T)
		  (setf (env-cons-env-cache nenv)
			(ncons (vector-union-new cache
						 (assumption-binary-vector assumption))))
		  nenv)))
	((lookup-cons-vector assumption v ov count (simple-env-count simple-env)))
	((contradictory-cons? assumption v count)
	 *contra-env*)
	((make-simple-env
	   count
	   (vector-union-new cache (assumption-binary-vector assumption))
	   (cons assumption (simple-env-assumptions simple-env))
	   v))))

;;;***** THIS IS NOT THAT FAST ANY MORE AT ALL?
(defun fast-contradictory-cons? (env assumption)
  (format T "~% fast-contradictory-cons? is now very slow")
  (cond ((eq *empty-env* env) (tms::assumption-contradictory assumption))
	((vector-member assumption (generic-env-cons-env-cache env)))
	((vector-intersection? (assumption-binary-vector assumption)
			       (generic-env-vector env)))
	;;*** avoid the cons-assumption?
	((contradictory-env-assumptions3? assumption
					  (cons-assumption (generic-env-assumptions env)
							   assumption)
					  (1+ (generic-env-count env))))))

;;; Just a faster version of fast-cons-vector for experiments.
;;; It keeps simple env assumptions sorted as that appears to be worth it.
(defun fast-cons-vector3 (simple-env assumption simple-result-ok &optional ignore-hash
								 &aux ov v count cache
				    ptr nenv assumptions)
  (setq ov (simple-env-vector simple-env))
  (cond ((= (simple-env-count simple-env) 1)
	 (double assumption (car (env-assumptions simple-env))))
	((or (vector-member assumption
			    (setq cache (simple-env-cons-env-cache simple-env)))
	     (vector-intersection? (assumption-binary-vector assumption) ov))
	 *contra-env*)
	((null simple-result-ok)
	 (cond ((hash-slot-value (setq ptr (nget-or-puthash-env
					     (setq v (vector-cons4 assumption ov))
					     *env-hash-table*))))
	       ((contradictory-env-assumptions3?
		  assumption (if *delay-assumptions*
				 (blits-to-assumptions v)
				 (setq assumptions
				       (cons-assumption
					 (simple-env-assumptions simple-env)
					 assumption)))
		  (setq count (1+ (simple-env-count simple-env))))
		(hash-slot-set ptr v *env-hash-table*)
		(setf (aref *hashes* count) T)
		*contra-env*)
	       ;;******** could simple-envs are sorted now remember.
	       ;;******** already sorted now.
	       (t (setq nenv
			(make-an-env-3 count (or assumptions :DELAY) v))
		  (hash-slot-set ptr nenv *env-hash-table*)
		  (setf (aref *hashes* count) T)
		  (set-env-cache nenv cache (assumption-binary-vector assumption))
		  nenv)))
; This is not quite right and doesn't speed up things anyway.  Its not right in that
; without a lookup generic-search-assumptions needs to do an <= check on count	
;	((progn (setq v (vector-cons4 assumption ov))
;		(generic-search-assumption-nogoods count
;						   simple-env assumption
;						   v))
;	 *contra-env*)
;; This sets ov again but so what I guess.
	((lookup-cons-vector? assumption v ov count (simple-env-count simple-env)))
	((and (assumption-nogoods assumption)
	      (contradictory-env-assumptions3? assumption
					       (if *delay-assumptions*
						   (blits-to-assumptions v)
						   (setq assumptions
							 (cons-assumption
							   (generic-env-assumptions-delay simple-env)
							   assumption)))
						   count))
	 *contra-env*)
	((make-simple-env
	   count
	   (get-env-cache cache (assumption-binary-vector assumption))
	   (if *delay-assumptions*
	       :DELAY
	       (or assumptions (cons-assumption (simple-env-assumptions simple-env) assumption)))
	   v))))

;;; Always assumes everything is simple.  Assumes delay.  Does not check compatibility even.
(defun fast-cons-simple (simple-env assumption &aux ov (count 0))
  ;;***** temporary:
  (unless (simple-envp simple-env)
    (setq simple-env
	  (make-simple-env (env-count simple-env) nil :DELAY (env-vector simple-env))))

  (if simple-env
      (setq count (simple-env-count simple-env)
	    ov (simple-env-vector simple-env)))
  (cond ((vector-member assumption ov) simple-env)
	;; Check for compatibility.
	((make-simple-env (1+ count)
			  nil
			  :DELAY
			  (vector-cons4 assumption ov)))))

;;; Like fast-cons-vector, but assumes the hard case.
;;; *** This could be slightly optimized so that doubling created simple environments.
(defun fast-cons-vector2 (simple-env assumption simple-result-ok ov cache &aux v count 
				    ptr nenv) 
  (cond ((= (simple-env-count simple-env) 1)
	 (double assumption (car (simple-env-assumptions simple-env))))
	((null simple-result-ok)
	 (cond ((hash-slot-value (setq ptr (nget-or-puthash-env
					     (setq v (vector-cons4 assumption ov))
					     *env-hash-table*))))
	       ((contradictory-cons? assumption v
				    (setq count (1+ (simple-env-count simple-env))))
		(hash-slot-set ptr v *env-hash-table*)
		(setf (aref *hashes* count) T)
		*contra-env*)
	       (t (setq nenv
			(make-an-env-3 count
				       (cons assumption
					     (simple-env-assumptions simple-env))
				       v))
		  (hash-slot-set ptr nenv *env-hash-table*)
		  (setf (aref *hashes* count) T)
		  (setf (env-cons-env-cache nenv)
			(ncons (vector-union-new cache
						 (assumption-binary-vector assumption))))
		  nenv)))
	((lookup-cons-vector assumption v ov count (simple-env-count simple-env)))
	((contradictory-cons? assumption v count)
	 *contra-env*)
	((make-simple-env
	   count
	   (vector-union-new cache (assumption-binary-vector assumption))
	   (cons assumption (simple-env-assumptions simple-env))
	   v))))

;;; This has two important properties. (1) it will create the env, no matter what,
;;; and (2) it does not do the nogood check.???
(defun force-cons-env (env assumption)
  ;; **** this works only by concidence, it doesn't suppress nogoods.
  (find-or-make-env (cons-assumption (env-assumptions-delay env) assumption)))

;;; This returns the environment obtained by removing assumption from env.  Note that
;;; the environment might be contradictory.  
(defun uncons-env (env assumption &aux result count as vector ptr assumptions)
  (if (eq env *contra-env*) (error "Can't uncons from THE contradictory environment"))
  (setq count (env-count env))
  (cond ((= count 1)
	 (if (eq assumption (car (env-assumptions-delay env)))
	     *empty-env*
	     (error "Unconsing a nonexistant assumption")))
	((= count 2)
	 (setq as (env-assumptions-delay env))
	 (cond ((eq (car as) assumption) (assumption-env (cadr as)))
	       ((eq (cadr as) assumption) (assumption-env (car as)))
	       (t (error "Unconsing a nonexistant assumption"))))
	((cdr (assq assumption (env-uncons-cache env))))
	;; Remember environments of size 2 are stored differently.
	((= count 3)
	 (setq as (env-assumptions-delay env))
	 (setq result (cond ((eq assumption (first as)) (double (second as) (third as)))
			    ((eq assumption (second as)) (double (first as) (third as)))
			    ((eq assumption (third as)) (double (first as) (second as)))
			    (t (error "Unconsing non-existant assumption"))))
	 (push (cons assumption result) (env-uncons-cache env))
	 result)

	;; If this is inefficient, write a function to do a single bit.
	(t (setq result
		 (hash-slot-value
		   (setq ptr (nget-or-puthash-env
			       (setq vector (remove-assumption (env-vector env)
							       assumption))
			       *env-hash-table*))))
	   (unless result
	     (if *simple-hybrid*
		 (setq assumptions (blits-to-assumptions vector))
		 (setq assumptions (uncons-assumption (env-assumptions env) assumption)))
	     (cond ((and (subsumed-nogood? env)
			 (or (not (compatible-assumptions? assumptions vector))
			     (dolist (a assumptions) (if (assumption-contradictory a) (return T)))
			     (new-contradictory-env-assumptions? assumptions (1- count))))
		    (hash-slot-set ptr vector *env-hash-table*)
		    (setf (aref *hashes* count) T)
		    (setq result *contra-env*))
		   (t (setq result (make-an-env-2 (1- count)
						  (if *simple-hybrid*
						      :DELAY
						      assumptions)
						  vector))
		      (when (and *simple-hybrid* *index-early*)
			(setf (env-waiting result) (env-waiting env))
			(unless (assumption-in-focus assumption)
			  (decf (env-waiting result))))
		      (setf (aref *hashes* count) T)
		      (hash-slot-set ptr result *env-hash-table*))))
	   (push (cons assumption result) (env-uncons-cache env))
	   result)))

(defun uncons-assumption (assumptions assumption &aux nassumptions)
  (do ((assumptions assumptions (cdr assumptions)))
      ((null assumptions) (error "Unconsing a nonexistant assumption"))
    (if (eq (car assumptions) assumption)
	(return (nreconc nassumptions (cdr assumptions)))
	(push (car assumptions) nassumptions))))

(defun find-or-make-env-vector (vector &aux count new-assumptions result ptr)
  ;;***** presumes simple-hybrid, compatibility, etc. Wrong assumptions probably.
  (setq ptr (nget-or-puthash-env vector *env-hash-table* t)
	result (hash-slot-value ptr))
  (if (eq result *contra-env*) (error "Unimplemented"))
  (if result (return-from find-or-make-env-vector result))
  (multiple-value-setq (new-assumptions count) (blits-to-assumptions vector))
  (when (= count 1)
    (return-from find-or-make-env-vector (assumption-env (car new-assumptions))))
  (when (= count 2)
    (return-from find-or-make-env-vector
      (double (car new-assumptions) (cadr new-assumptions))))
  (setq result (make-an-env-2 count :DELAY vector))
  (setf (aref *hashes* count) T)
  (hash-slot-set ptr result *env-hash-table*)
  (when (and new-assumptions
	     (or (eq new-assumptions :CONTRADICTION)
		 (new-contradictory-env-assumptions? new-assumptions count)))
    (setf (env-contradictory-bit result) 1)
    (setf (env-contradictory-info result) '(BASE UNIMPLEMENTED)))
  result)

;;; Inefficient, cleanup if happens very often.
;;; Remove every assumption of env2 from env1.
(defun env-difference-old (env1 env2 &aux vector)
  (setq vector (env-vector env1))
  (dolist (a (env-assumptions env2))
    (if (vector-member a vector) (setq env1 (uncons-env env1 a))))
  env1)

;;; The above env-difference doesn't work for nogoods.  This works as long as the result
;;; is not nogood.  This can be optimzed a lot.
(defun env-difference (start subtract)
  (if *delay-assumptions*
      (multiple-uncons-env start (fcopylist (env-assumptions-delay subtract)))
      (multiple-uncons-env start (env-assumptions subtract))))

;;;***** THIS SHOULD ALWAYS CREATE OR MAKE AN ENV.  NEVER RETURN *CONTRA-ENV*
(defun change-env (env adds retracts &aux vector count new-assumptions result ptr)
  ;;***** could be made more efficient here.  Save lots of conses.
  ;;***** presumes simple-hybrid, compatibility, etc.
  (setq vector (env-vector env))
  (dolist (r retracts) (setq vector (remove-assumption vector r)))
  (dolist (a adds) (setq vector (vector-cons4 a vector)))
  (setq count (blits-size vector))
  (cond ((= count 1)
	 (return-from change-env
	   (assumption-env (car (blits-to-assumptions vector)))))
	((= count 2)
	 (let ((assumptions (blits-to-assumptions vector)))
	   (return-from change-env
	     ;;**** does double always return an env.
	     (double (car assumptions) (cadr assumptions))))))

  (setq ptr (nget-or-puthash-env vector *env-hash-table* t)
	result (hash-slot-value ptr))
  (if (eq result *contra-env*) (error "Unimplemented --- result is contradictory"))
  (if result (return-from change-env result))
  (cond ;; In many cases, this first test is unecessary.
        ((dolist (a adds) (if (vector-intersection? (assumption-binary-vector a) vector)
			      (return T)))
	 (setq new-assumptions :CONTRADICTION))
	((and (not (env-contradictory env))
	      (not (dolist (a adds) (if (assumption-dirty a) (return T))))))
	;; An heuristic which can be optimized:
	((and (not (env-contradictory env)) (null (cdddr adds)))
	 (setq count (blits-size vector))
	 (dolist (a adds)
	   (when (dolist (nogood (assumption-nogoods a))
		   (and (eq (car (env-contradictory-info nogood)) 'BASE)
			(<= (env-count nogood) count)
			(vector-subset (env-vector nogood) vector)
			(return T)))
	     (setq new-assumptions :CONTRADICTION))))
	((and (env-contradictory env) (null retracts))
	 (setq new-assumptions :CONTRADICTION))
	((and (env-contradictory env)
	      (let ((base (env-vector (find-base-contradiction env))))
		(not (dolist (r retracts)
		       (if (vector-member r base) (return T))))))
;	 (ERROR "EXAMPLE OF FAILING RETRACT")
	 (setq new-assumptions :CONTRADICTION))

	(t ;(error "Why")
	   (multiple-value-setq (new-assumptions count) (blits-to-assumptions vector))))
  (if (< count 3) (error "Unimplemented --- count < 3"))
  (setq result (make-an-env-2 count :DELAY vector))
  (setf (aref *hashes* count) T)
  (hash-slot-set ptr result *env-hash-table*)
  (when (and new-assumptions
	     (or (eq new-assumptions :CONTRADICTION)
		 (new-contradictory-env-assumptions? new-assumptions count)))
    (setf (env-contradictory-bit result) 1)
    (setf (env-contradictory-info result) '(BASE UNIMPLEMENTED)))
  result)

(defun multiple-uncons-env (env assumptions &aux vector ptr new-assumptions result count)
  (cond ((null assumptions) env)
	((null (cdr assumptions)) (uncons-env env (car assumptions)))
	(t (setq vector (env-vector env))
	   ;; **** this is really inefficient...**** need unsafe version****. and copy.
	   (dolist (a assumptions)
	     (setq vector (remove-assumption vector a)))
	   (setq ptr (nget-or-puthash-env vector *env-hash-table* t)
		 result (hash-slot-value ptr))
	   (if result (return-from multiple-uncons-env result))
	   (multiple-value-setq (new-assumptions count)
	     (if *delay-assumptions*
		 (blits-to-assumptions vector)
		 (assumptions-difference (env-assumptions env) assumptions)))

	   ;; These special cases could be handled earlier.****
	   (cond ((= count 0) *empty-env*)
		 ((= count 1) (assumption-env (car new-assumptions)))
		 ((= count 2) (double (car new-assumptions) (cadr new-assumptions)))
		 ((and (subsumed-nogood? env)
		       (or (not (compatible-assumptions? new-assumptions vector))
			   (dolist (a new-assumptions) (if (assumption-contradictory a)
							   (return T)))
			   (new-contradictory-env-assumptions? new-assumptions
							       count)))
		    (hash-slot-set ptr vector *env-hash-table*)
		    (hash-allocate *env-hash-table*)
		    (setf (aref *hashes* count) T)
		    *contra-env*)
		   (t (setq result (make-an-env-2 count
						  (if *delay-assumptions*
						      :DELAY
						      new-assumptions)
						  vector))
		      (setf (aref *hashes* count) T)
		      (hash-slot-set ptr result *env-hash-table*)
		      (hash-allocate *env-hash-table*)
		      (when (and *simple-hybrid* *index-early*)
			(setf (env-waiting result) (env-waiting env))
			(dolist (a assumptions)
			  (unless (assumption-in-focus a)
			    (decf (env-waiting result)))))
		      result)))))

;;; Note that this assumes both lists are sorted.  This can be made more efficient.
(defun assumptions-difference (assumptions subtract &aux result end new (length 0))
  (do () ((or (null assumptions) (null subtract))
	  (values (cond (result (rplacd end assumptions) result)
			(t assumptions))
		  (+ length (length assumptions))))
    (cond ((assumption-orderp (car assumptions) (car subtract))
	   (incf length)
	   (setq new (cons (car assumptions) nil))
	   (if result (rplacd end new) (setq result new))
	   (setq end new
		 assumptions (cdr assumptions)))
	  ((eq (car assumptions) (car subtract))
	   (setq assumptions (cdr assumptions)
		 subtract (cdr subtract)))
	  (t (setq assumptions (cdr assumptions))))))

(defun cons-assumption (assumptions assumption &aux new-assumptions)
  (do ((assumptions assumptions (cdr assumptions)))
      ;;****** doesn't list assumption create a cdr code?
      ((null assumptions) (nreconc new-assumptions (list assumption)))
    (if (assumption-orderp assumption (car assumptions))
	(return (nreconc new-assumptions (cons assumption assumptions)))
	(push (car assumptions) new-assumptions))))






;;; Create an env, but don't put it into the hash table.  Used to create empty
;;; and singleton environments. *** replace every occureance of make-an-env
;;; with make-an-env-1 nil nil.
(defun make-an-env (assumptions) (make-an-env-1 assumptions nil nil))

(defvar *index-early* nil)

(defvar *lazy* t)				; An experiment.

;;; This PRESUMES there is no contradiction.  Call ONLY if you know what you are doing.
;;; PRESUMES hash table lookup has failed. PRESUMES assumptions are sorted.
(defun make-an-env-2 (count assumptions vector &optional dont-index &aux env)
  (setq env (make-env :ASSUMPTIONS assumptions
		      :COUNT count
		      :VECTOR vector))
  (setf (env-unique env) (incf *env-counter*))
;  (setf (aref *env-array* *env-counter*) env)
;  (set-env-hybrid env 1)

;  (unless (equal (make-env-vector-blits assumptions) vector)
;    (error "NOt possible"))

;  (error "for now")
;  (if (= *env-counter* 104.) (error "Found it"))

  (unless dont-index 
    (if *index-early* (index-env env assumptions))
    (assure-env-size count)
    (push env (aref *environments* count)))
  env)

(defvar *lazy-index* nil)

(defun cleanup-assumption (a &aux indexed-to envs)
  (if *ltms* (return-from cleanup-assumption nil))
  ;;****** when using for the first time??
  (setq indexed-to (assumption-indexed-to a)
	envs (assumption-in-envs a))
  (dolist (e *indexed-envs*)
    (if (eq e indexed-to) (return nil))
    (if (vector-member a (env-vector e))
	(push e envs)))
  (setf (assumption-indexed-to a) (car *indexed-envs*))
  (setf (assumption-in-envs a) envs))

;;; This seems to improve locality of reference a bit.
;;; No, flush it.
(defvar *batch-index* nil)

(defun index-env (env assumptions)
;  (if (= (env-unique env) 389.) (print 'indexing-389))

  ;; LTMS doesn't care about keeping the indexes straight.
  (if *ltms* (return-from index-env nil))

  (unless *index-early*
    ;;********** optimize.
    (if (or (env-indexed? env)
	    (env-toindex? env))
	(return-from index-env nil))
    (setf (env-toindex env) 1))

  (when (and *lazy-index* (cddr assumptions))
    (push env *indexed-envs*) 
    (return-from index-env nil))

  (when (and *batch-index* (cddr assumptions))
    (push env *indexed-envs*)
    (return-from index-env))

  (when (and *last-assumption-enabled*
	     ;;***** ALmost always true: Can probably be guaranteed in most
	     ;;circumstances.
	     (vector-member *last-assumption-enabled* (env-vector env)))
;    (format T "~% Delaying ~A on ~A" env *last-assumption-enabled*)
    (push env (assumption-envs-to-index *last-assumption-enabled*))
    (return-from index-env nil))

  (when (and *last-assumption-enabled*
	     *change-foci-trace*
	     (> (env-count env) 1))
;    (format T "~% INDEX-ENV: Indexing ~A because its not on last enabled assumption ~A"
;      	    env *last-assumption-enabled*)
;    (error "here we are")
    )

  (setf (env-indexed env) 1)
  

;***** which is faster:
;  (dolist (a (env-assumptions-delay env))
;    (push env (assumption-in-envs a)))
  (do-assumptions-blits (env-vector env)
			#'(lambda (a)
			    #+Symbolics
			    (declare (sys:downward-function))
			    (push env (assumption-in-envs a)))))

(defun correctly-indexed? (env &aux slot flag)
  (dolist (assumption (env-assumptions-delay env))
    (unless (setq slot (memq env (assumption-in-envs assumption)))
      (setq flag T)
      (format T "~%~A is not indexed on ~A" env assumption))
    (when (memq env (cdr slot))
      (setq flag T)
      (format T "~%~A is indexed twice on ~A")))
  (not flag))

(defun env-assumptions-delay (env &aux assumptions)
  (setq assumptions (env-assumptions env))
  (if (eq assumptions :DELAY)
      (blits-to-assumptions (env-vector env))
      assumptions))

(defun generic-env-assumptions-delay (env &aux assumptions)
  (setq assumptions (tms::generic-env-assumptions env))
  (if (eq assumptions :DELAY)
      (blits-to-assumptions (generic-env-vector env))
      assumptions))


(defun do-batched-indexes ()
  (dolist (e *indexed-envs*)
    (cond ((env-nodes e)
	   (dolist (a (env-assumptions e))
	     (push e (assumption-in-envs a))))
	  (t (setf (env-toindex e) 0)
	     (setf (env-indexed e) 0))))
  (setq *indexed-envs* nil))

;;; This also keeps the maximum environment count updated.
(defun assure-env-size (count)
  (unless ( count *max-env-count*)
    (setq *max-env-count* count)
    (adjust-sizes *max-env-count*)))

;;; This creates fresh list structure when expanding in the hope that the
;;; memory might be allocated locally.
(defun assure-assumption-size ()
  (when (> (incf *total-assumption-counter*) *fast-assumptions-size*)
    (setq *fast-assumptions-size* (* 2 (+ *fast-assumptions-size* 100.))
	  *fast-assumptions-conses* nil
	  *blits-to-assumptions-conses* nil)
    (setq *fast-assumptions-conses* (simple-make-list *fast-assumptions-size* nil)
	  *blits-to-assumptions-conses* (simple-make-list *fast-assumptions-size* nil))
    (do ((l *fast-assumptions-conses* (cdr l)))
	((null l))
      (rplaca l (cons nil nil)))
    (do ((l *blits-to-assumptions-conses* (cdr l)))
	((null l))
      (rplaca l (cons nil nil)))))

;;; This makes sure environment array is big enough.
(defun adjust-sizes (to-size &aux new-size)
  (unless (< to-size (array-length *environments*))
    (setq new-size (floor (* 1.5 to-size)))
    (setq *environments* (adjust-array *environments* new-size)
	  *hashes* (adjust-array *hashes* new-size)
	  *conses* (simple-make-list new-size nil)
	  *current-size* new-size)))

;;; Exactly like make-an-env-2 except it may contain a contradiction.  PRESUMES
;;; that compatibility and single contradictions have been checked already.
;;; You probably don't want to call this, why bother even creating the assumptins
;;; if the env may be contradictory.
(defun make-an-env-3 (count assumptions vector &aux env)
  (cond ((new-contradictory-env-assumptions? assumptions count) *contra-env*)
	(t (setq env (make-env :ASSUMPTIONS assumptions
			       :COUNT count
			       :VECTOR vector))
	   (setf (env-unique env) (incf *env-counter*))
;	   (if (= *env-counter* 152.) (error "here"))
;	   (setf (aref *env-array* *env-counter*) env)
;+++	   (set-env-hybrid env 1)
	   (if *index-early* (index-env env assumptions))
	   (assure-env-size count)
	   (push env (aref *environments* count))
	   env)))

;;; Assumptions are presumed sorted.
;;; Compat should throw out non-exclsuve compats*******
;;; Why bother creatng the env f it is known contradictory do that first***???
;;; This forces a creation ---- so don't call this function in general.
(defun make-an-env-1 (assumptions vector no-contra-check &aux env count reason)
  (setq count (length assumptions)
	env (make-env :ASSUMPTIONS assumptions
		      :COUNT count
		      :VECTOR (or vector (make-env-vector assumptions))))
  (setf (env-unique env) (incf *env-counter*))
;  (setf (aref *env-array* *env-counter*) env)
;+++   (set-env-hybrid env 1)
;  (if (= *env-counter* 389.) (error "here"))
  (unless no-contra-check (setq reason (contradictory-env-assumptions? env)))
  (cond (reason (setf (env-contradictory-bit env) 1)
		(setf (env-contradictory-info env) (cons 'SUBSUMED reason))
	 )
	(t (if *index-early* (index-env env assumptions))
	   (assure-env-size count)
	   (push env (aref *environments* count))))
  env)

;;; Makes no assumptions about whether assumptions are sorted, compatible, or contradictory.
;;; Not optimized.
;;; Where are singleton contra assumptions checked???*****true/false assumptions
;;; **** this is probably bogus for that reason.
;;; I'm confused about what is expected for this function for inactive assumptions?
;;; This function is not very optimized.  It might well be worth fixing.
;;; This does the force the creation of the env.
(defun find-or-make-env (assumptions &aux env ptr v count)
  (cond ((null assumptions) *empty-env*)
	((null (cdr assumptions)) (assumption-env (car assumptions)))
	((null (cddr assumptions)) (double (car assumptions) (cadr assumptions)))
	((dolist (a assumptions) (if (i-false? a) (return *contra-env*))))
	((hash-slot-value (setq ptr (nget-or-puthash-env
				      (setq v (make-env-vector* assumptions))
				      *env-hash-table*))))
	((progn (setq count (length assumptions))
		(and (compatible-assumptions? assumptions v)
		     (not (new-contradictory-env-assumptions? 
			    (setq assumptions (sort (fcopylist assumptions)
						    #'(lambda (x y)
							(assumption-orderp x y))))
			    count))))
	 ;; Remember contradictions can't be directly in table, in current representation.
	 (setq env (make-an-env-2 count assumptions v))
	 (hash-slot-set ptr env *env-hash-table*)
	 (setf (aref *hashes* count) T)
	 env)
	(t 
	   (hash-slot-set ptr v *env-hash-table*)		;**** why cache, flush?
	   (setf (aref *hashes* count) T)
	   *contra-env*)))

;;; This doesn't bother constructing a cache as in most cases it probably isn't worth it.
(defun find-or-make-generic-env (assumptions &optional dont-lookup &aux v count)
  (cond ((null assumptions) *empty-env*)
	((null (cdr assumptions)) (assumption-env (car assumptions)))
	((null (cddr assumptions)) (double (car assumptions) (cadr assumptions)))
	((unless dont-lookup
	   (gethash-env (setq v (make-env-vector* assumptions))
			*env-hash-table*)))
	((progn (setq count (length assumptions))
		(and (compatible-assumptions? assumptions
					      (or v (setq v (make-env-vector* assumptions))))
		     (not (new-contradictory-env-assumptions? 
			    (setq assumptions (sort (fcopylist assumptions)
						    #'(lambda (x y)
							(assumption-orderp x y))))
			    count))))
	 (make-simple-env count nil assumptions (or v (make-env-vector* assumptions))))
	(t *contra-env*)))

;;; Presumes assumptions are sorted, compatible, and no singleton contradiction.
(defun find-or-make-env-safe1 (assumptions &aux env ptr v)
  (cond ((null assumptions) *empty-env*)
	((null (cdr assumptions)) (assumption-env (car assumptions)))
	((null (cddr assumptions)) (double (car assumptions) (cadr assumptions)))
	((hash-slot-value (setq ptr (nget-or-puthash-env
				      (setq v (make-env-vector assumptions))
				      *env-hash-table*))))
	(t (setq env (make-an-env-3 (length assumptions) assumptions v))
	   (hash-slot-set ptr env *env-hash-table*)
	   (setf (aref *hashes* (length assumptions)) T)
	   env)))

;;; Assumes assumptions are sorted and guaranteed non contradictory!
(defun find-or-make-env-safe (assumptions &optional v &aux env ptr)
  (cond ((null assumptions) *empty-env*)
	((null (cdr assumptions)) (assumption-env (car assumptions)))
	((null (cddr assumptions)) (double (car assumptions) (cadr assumptions)))
	((hash-slot-value (setq ptr (nget-or-puthash-env
				      (or v (setq v (make-env-vector assumptions)))
				      *env-hash-table*))))
	(t (setq env (make-an-env-2 (length assumptions)
				    (if *delay-assumptions*
					:DELAY
					assumptions)
				    v))
	   (setf (aref *hashes* (length assumptions)) T)
	   (hash-slot-set ptr env *env-hash-table*)
	   (if (and *simple-hybrid* *index-early*) (set-env-waiting env))
	   env)))

;;;; Would do-assumption-blits be faster?****
(defun set-env-waiting (env &aux (count 0))
  (if *ltms* (return-from set-env-waiting nil))
  (dolist (a (env-assumptions-delay env))
    (unless (assumption-in-focus a) (incf count)))
  (setf (env-waiting env) count))
  
;;; Do not use env-assumptions-delay.  Or! use a different blits cons area for debugging.
(defun compute-env-waiting (env &aux (count 0))
  (do-assumptions-blits (env-vector env)
			#'(lambda (a)
			    #+Symbolics
			    (declare (sys:downward-function))
			    (unless (assumption-in-focus a) (incf count))))
  count)

(defun compute-missing (env &aux missing)
  (dolist (a (env-assumptions-delay env))
    (unless (assumption-in-focus a) (push a missing)))
  missing)

(defun where-indexed (env &aux slot (count 0))
  (dolist (a (env-assumptions-delay env))
    (when (setq slot (memq env (assumption-envs-to-index a)))
      (incf count)
      (format T "~% ~A is waiting on ~A" env a)
      (if (memq env (cdr slot))
	  (format T "~% But it appears twice!"))))
  (if (> count 1) (format T "~% Indexed too often")))

(defun check-env (env &optional msg)
  msg
  (when (and env (env-waitingp env))
    (and (not (= (env-waiting env) (compute-env-waiting env)))
	 (error "Mismatch at ~A" env))))

(defun check-just-counts (&optional msg)
  msg
  (dolist (n *nodes*)
    (dolist (j (n-a-justifications n))
      (check-just-count j))))

(defun check-just-count (j &aux (count 0) missing)
  (dolist (a (just-antecedents j))
    (unless (hybrid-label a) (incf count) (push a missing)))
  (unless (= count (just-count j))
    (format T "~%Justification has count ~D instead of the correct ~D is missing ~A"
	    (just-count j) count missing)
    (if (dolist (a (just-antecedents j))
	  (unless (memq j (n-a-consequents a)) (return T)))
	(format T "~% Which is not suprising as its not wired up to all its antecedents"))
    (error "Should not happen")

    ))

;;;***** buggy, doesn't account for some counts which will be incorrect.
(defun check-env-waiting (&optional msg &aux smallest compute)
  (if *ltms* (return-from check-env-waiting nil))
  msg
  (do ((i 1 (1+ i)))
      ((> i *max-env-count*))
    (do ((e (aref *environments* i) (cdr e)))
	((null e))
      (unless (env-waitingp (car e))
	(if (env-indexed? (car e))
	    (error "~A is indexed but has no count" (car e))))

      (when (env-waitingp (car e))
	(setq compute (compute-env-waiting (car e)))
	(cond ((env-indexed? (car e))
	       (and (not (= (env-waiting (car e)) compute))
		    (or (null smallest) (< (env-unique (car e)) (env-unique smallest)))
		    (setq smallest (car e))))
	      ((> compute 0) (unless (> (env-waiting (car e)) 0)
			       (error "Both not greater than 0")))
	      ((= compute 0) (unless (= (env-waiting (car e)) 0)
			       (error "Both not 0")))))))
  (when smallest
    (error "Bad env count for ~A: stored: ~D correct: ~D"
	   smallest (env-waiting smallest)
	   (compute-env-waiting smallest))))


;;; This demands that the set be created.  This presumes nothing about
;;; the assumption set.  Caveat emptor.

;;;; ********** this is horribly broken.
;;; It does not leave around the explanation for why the environment is subsumed.
(comment
(defun find-or-make-env-force (assumptions &aux env ptr v count)
  (cond ((null assumptions) *empty-env*)
	((dolist (a assumptions) (if (eq (assumption-contradictory a) 'GCED) (return T)))
	 ;; If its GC'ed, its not accessible in the cache any more.
	 (setq assumptions (sort assumptions #'assumption-orderp)
	       count (length assumptions)
	       v (make-env-vector assumptions)
	       env (make-an-env-4 count assumptions v))
	 (rplaca ptr env)
	 env)
	(t (setq assumptions (sort assumptions #'assumption-orderp)
		 count (length assumptions)
		 env (make-an-env-2 count assumptions v))
	   (cond ((car ptr) (setf (env-contradictory-bit env) 1)
			    (setf (env-contradictory-info env) '(SUBSUMED . SAFE)))
		 ((compatible-assumptions? assumptions v)
		  (setf (env-contradictory-info env) '(SUBSUMED . INCOMPATIBLE)))
		 ;;*** bogus now:
		 ((contradictory-env-assumptions1? v count)
		  (setf (env-contradictory-bit env) 1)
		  (setf (env-contradictory-info env) '(SUBSUMED . SAFE))))
	   (rplaca ptr env)
	   env))))

(defun find-or-make-env-bits (vector &aux env ptr assumptions)
  (error "Won't work for singleton/double environments")
  (setq vector (sanitize-vector vector))
  (cond ((null vector) *empty-env*)
	((hash-slot-value (setq ptr (nget-or-puthash-env vector *env-hash-table*))))
	;; ****** this is all to be fixed in next version. i.e., vector-assumptions.
        ;; THis is horrible, isn't it.  ???
	((compatible-assumptions? (setq assumptions
					(vector-assumptions vector *assumption-array*))
				  vector)


	 (setq env (make-an-env-1 assumptions vector nil))
	 (hash-slot-set ptr env *env-hash-table*)
	 (setf (aref *hashes* (length assumptions)) T)
	 env)
	(t (setf (aref *hashes* (length assumptions)) T)
	   (hash-slot-set ptr vector *env-hash-table*)
	   *contra-env*)))

;;; If the environment is *contra-env*, then a real environment is put in that
;;; slot instead.  Remember this clutters up the hash table, if you are using this
;;; function a lot you are doing something wrong.  This probably should be changed
;;; to return a generic env.
;;; This is used by CANDGEN right now.
(defun find-or-make-env-bits-force (vector &aux env ptr v assumptions)
  (cond ((null vector) *empty-env*)
	((setq env (hash-slot-value (setq ptr (nget-or-puthash-env vector *env-hash-table*))))
	 (cond ((neq *contra-env* env) env)
	       (t (setq env (make-an-env-1 (vector-assumptions vector *assumption-array*)
					   v nil))
		  (hash-slot-set ptr env *env-hash-table*)
		  (setf (aref *hashes* (length (env-assumptions env))) T)
		  env)))
	;; If there are more than two assumptions, just stick it in hash table.
	((cddr (setq assumptions (vector-assumptions vector *assumption-array*)))
	 (setq env (make-an-env-1 assumptions v nil))
	 (hash-slot-set ptr env *env-hash-table*)
	 (setf (aref *hashes* (length assumptions)) T)
	 (unless (compatible-assumptions? assumptions v)
	   (setf (env-contradictory-bit env) 1)
	   (setf (env-contradictory-info env) '(SUBSUMED . INCOMPATIBLE)))
	 env)
	((cdr assumptions) (double (car assumptions) (cadr assumptions)))
	(t (assumption-env (car assumptions)))))
	
	


;;; Note that an environment can become contradictory AFTER its string is cached.
(defun update-env-string (env &aux string)
  (when (env-has-string? env)
    #+(OR :ZL :CADR) (array-push (cached-env-string env) 42)	; #/* can't be read in CL!?!?!
    #+(OR :CL :CL-ZL) (cond ((stringp (cached-env-string env)) (vector-push #\* (cached-env-string env)))
			    ((setq string (cdr (assq ':A (cached-env-string env))))
			     (vector-push #\* string)))))

(defun princ-assumption (assumption &optional (stream T))
  (princ (string-assumption assumption) stream))


;;;;*** needs to be rethough.
;;; This is shit because want to make sure assumption-datum really does not
;;; have a non-cl string in it.
(defun string-assumption (assumption &aux variable value type handler)
  (or (assumption-string assumption)
      (setf (assumption-string assumption)
	    (cond ((atms-string-assumption *atms*)
		   (funcall (atms-string-assumption *atms*) assumption))
		  ((careful-node? (assumption-variable assumption))
		   (node-string (assumption-variable assumption)))
		  ((and (assumption-variable assumption)
			(setq variable
			      (if (node? (assumption-variable assumption))
				  (n-a-datum (assumption-variable assumption))
				  (class-datum (assumption-variable assumption)))
			      type (type-of variable)
			      value (assumption-value assumption)
			      handler (get type :TMS-STRING)
			      ))
		   (string (funcall handler assumption type variable value)))
		  ((and (null variable) (null value))
		   (format nil " ~A " (assumption-datum assumption)))
		  (t (format nil "(~A=~A)" variable value)
		     )))))

;;; There are three styles of environment strings:
;;; A: {...} or {...}*
;;; B: {...} or <...>
;;; C: [...]
;;; If string-env is a string, its of type A.  Otherwise there is an alist.
;;; This can be made a lot more efficient if need be.

;;; This could be optimized a lot more because all types have essentially the same
;;; contents, so reconstructing the innards every time is a real waste.

;;; Commonlisp (move to defs) if take 2 or 3 arguments, no more.
(defun string-env (env &optional (type :A) &aux slot)
  (cond ((simple-envp env) (compute-env-string env type))
	((stringp (setq slot (cached-env-string env)))
	 (if (eq type :A) slot
	     (progn (setf (cached-env-string env) (list (cons :A slot)))
		    (setf (env-has-string-bit env) 1)
		    (string-env env type))))
	((and (eq type :A) (null slot))
	 (setf (env-has-string-bit env) 1)
	 (setf (cached-env-string env) (compute-env-string env type)))
	((cdr (assq type slot)))
	(t (setq slot (compute-env-string env type))
	   (setf (env-has-string-bit env) 1)
	   (push (cons type slot) (cached-env-string env))
	   slot)))

(defun compute-env-string (env type &aux (ptr 1) (length 0) result strings contra)
  (if (eq env *contra-env*) (case type (:A "{}*") (:B "<>") (:C "[]"))
      (progn (unless (simple-envp env) (setq contra (env-contradictory env)))
	     (dolist (assumption (generic-env-assumptions-delay env))
	       (push (string-assumption assumption) strings))
	     (setq strings (sort strings #'string-lessp))
	     (dolist (string strings) (incf length (length string)))
	     (setq result
		   (cond ((or (eq type ':B) (eq type ':C))
			  (make-array (+ length 2) :ELEMENT-TYPE 'STRING-CHAR))
			 (contra
			  (make-array (+ length 3) :ELEMENT-TYPE 'STRING-CHAR))
			 (t (make-array (+ length 3)
					:ELEMENT-TYPE 'STRING-CHAR
					:FILL-POINTER (+ length 2)))))
	     (dolist (string strings)
	       (replace result string :START1 ptr)
	       (incf ptr (length string)))
	     (case type
	       (:A (setf (char result 0) #\{)
		(setf (char result ptr) #\})
		(if contra (setf (char result (1+ ptr)) #\*)))
	       (:B (cond ((env-contradictory env)
			  (setf (char result 0) #\<)
			  (setf (char result ptr)#\>))
			 (t (setf (char result 0) #\{)
			    (setf (char result ptr) #\}))))
	       (:C (setf (char result 0) #\[)
		(setf (char result ptr) #\])))
	     result)))

(defun string-envs (envs) (mapcar #'string-env envs))

(defun print-envs (envs)
  (dolist (e envs) (format T "~% ~A" (string-env e))))

(defun princ-envs (envs)
  (dolist (e envs) (format T " ~A" (string-env e))))

(defun print-envss (envss)
  (dolist (envs envss) (terpri) (dolist (e envs) (print (string-env e)))))

(defvar *active-control-stack*)
 
(defvar *pending-control-stack*)

(defvar *node-prototype*)

(defvar *nogood-contras*)			; Queued redundancies.

(defun init-tms (&optional (reuse T) &key nogood-handler string-assumption node-string
		                          (min-hash-size 30000.))
  (when *trace-file*
    (and *dump* (> *node-counter* 2) (dump))
    (format *trace-file* "~%INIT-TMS"))
  (unless *randoms*
    (dotimes (i 100.)
      (declare (ignore i))
      (push (random *word-value*) *randoms*))
    (setq *randoms* (fcopylist *randoms*)))

  ;; Put in problem-sovler
  (setq *agenda* nil)
  

  ;; Clear it.
  (setq *atms* (make-atms :nogood-handler nogood-handler
			  :string-assumption string-assumption
			  :node-string node-string)
	*ltms-mark-env* nil
	*pending-adds* nil
	*pending-retracts* nil
	*indexed-envs* nil
	*nodes-to-check* :END
	*clauses-to-check* :END
	*changed-hybrid-nodes* nil
	*incomplete-assumption* nil
	*incomplete-assumptions* nil
	*label-q* nil				
	*label-q-worst* 0
	*label-q-best* 0
	*breadth-q* nil				
	*or-queue* nil
	*variables* nil
	*free-nodes* nil
	*minimal-nogood-count* 0
	*addb-count* 0
	*update-counter* 0
	*env-counter* 1
	*contra-counter* 1
	*symbol-counter* 1
	*class-counter* 0
	*node-counter* 1
	*assumption-counter* -1
	*total-assumption-counter* -1
	*big-union-count* 0
	*consumer-invokations* 0
	*addb-check-count* 0
	*binary-resolution-count* 0
	*consumers-exist* nil
	*justification-count* 0
	*full-resolution-count* 0
	*full-resolution-fail-count* 0
	*exhaustions* 0
	*assumption-symbols* nil
	*nodes* nil
	*last-assumption-enabled* nil
	*classes* nil
	*empty-env* nil
	*max-env-count* 0
	*max-contra-count* 0
	*t* nil
	*nogood-count* 100.
	*nogood-contras* nil
	*control-stack* nil
	*current-focus* nil
	*current-context* nil
	*current-nogoods* nil
	*unfocussed-nodes* nil
	*nogood-tree* nil
	*foci* nil
	*current-size* 100.
	*max-nogood-size* nil
	*max-nogood-used-size* nil)
  (cond ((and reuse *env-hash-table* *environments* *assumption-array* *ors*)
	 (clrhash *trace-write-hash*)
	 (clrhash *trace-read-hash*)
	 (clrhash *env-string-table*)
	 (fill *label-q-array* nil)
	 (fill *hashes* nil)
	 (fill *nogood-trees* nil)
	 (fill *nogood-stack* nil)
	 (fill *assumption-array* nil)
	 (fill *environments* nil)
	 (fill *ors* nil)
;	 (fill *env-array* nil)
;	 (fill *env-counters* #o177777)
	 (if (> (hash-p1 *env-hash-table*) min-hash-size)
	     (reset-hash-table-env *env-hash-table*)
	     (setq *env-hash-table* (make-hash-table-env min-hash-size nil)))
	 (when *reclaim-flag*
	   (dolist (a (prog1 *assumptions* (setq *assumptions* nil))) (nuke-assumption a)))
	 (setq *assumptions* nil)
	   
	 )
	(t (setq *fast-assumptions-size* 0.
		 *fast-assumptions-conses* nil
		 *blits-to-assumptions-conses* nil
		 *assumptions* nil
		 *free-assumptions* nil
		 *env-string-table* (make-tms-hash-table)
		 *trace-write-hash* (make-tms-hash-table)
		 *trace-read-hash* (make-tms-hash-table)
		 *label-q-array* (make-array 5000)
		 *environments* (make-array *current-size* #+:CL :ADJUSTABLE #+:CL T)
		 *hashes* (make-array *current-size* #+:CL :ADJUSTABLE #+:CL T)
		 *nogood-trees* (make-array 100.)
		 *nogood-stack* (make-array 100.)
		 *assumption-array* (make-array 5000)	;*** ungrowable, fix sometime.
		 *ors* (make-array 1000 #+:CL :ADJUSTABLE #+:CL T)
		 *env-hash-table*
		 (make-hash-table-env 33000 nil))))
  ;; Initializing it.
  (setq *node-prototype* (make-node #-(or :zl :cl-zl) :NAME-SYMBOL
				    #-(or :zl :cl-zl) 'NODE)
	*empty-env* (make-an-env nil)
	*empty-env-list* (list *empty-env*)
	*contra-env* (make-an-env-1 nil nil nil))
  (setf (env-waiting *empty-env*) 0)
  (setf (env-indexed *empty-env*) 1)
  (setq *good-foci* *empty-env*)
  (setf (env-contradictory-bit *contra-env*) 1)
  (setf (env-contradictory-info *contra-env*) '(BASE . ROOT-CONTRADICTION))
  (setq *contra-node* (internal-create-node "A contradiction"))
  (contradictory-node *contra-node* 'ROOT-OF-ALL-EVIL)
  *atms*)


;;; Useful auxiallary functions provided purely for the user.

;;; Returns T if some the union of some env of node with env is non-contradictory.
(defun consistent-in? (node env)
  (dolist (nenv (n-a-envs node))
    (unless (env-contradictory (union-env nenv env)) (return T))))

(defun consistent-in-blocked? (node env)
  (dolist (nenv (n-a-blocked node))
    (unless (env-contradictory (union-env nenv env)) (return T))))

;;; An extremely conservative compare-envs.  Each of one set has
;;; to imply all of the other.
(defun compare-envs (set1 set2 &aux (result 'EQUAL))
  (dolist (e1 set1)
    (dolist (e2 set2)
      (selectq (compare-env e1 e2)
	(EQUAL)
	(SUBSET12 (when (eq result 'SUBSET21) (setq result nil) (return))
		  (setq result 'SUBSET12))
	(SUBSET21 (when (eq result 'SUBSET12) (setq result nil) (return))
		  (setq result 'SUBSET21))
	(T (setq result nil) (return))))
    (unless result (return)))
  result)

;;; For external use.
(defun antecedent-envs (justification)
  (user-general-weave nil *empty-env-list* (just-antecedents justification)))

(defun true-in? (node env &aux label)
  (setq label (n-a-envs node))
  (cond ((null label) nil)
	((atom label) (if (subset-env? label env) label))
	(t (dolist (nenv (n-a-envs node)) (if (subset-env? nenv env) (return nenv))))))

;;; It makes a hair difference that the current-env is usually the subsuming env.
(defun true-in-blocked? (node env &aux current-env)
  (cond (*simple-hybrid*
	 (setq current-env (hybrid-label node))
	 (cond ((null current-env)
		(dolist (nenv (n-a-blocked node)) (if (subset-env? nenv env) (return nenv))))
	       ((subset-env? current-env env) current-env)
	       (t (dolist (nenv (n-a-blocked node))
		    (and (neq nenv current-env) (subset-env? nenv env) (return nenv))))))
	(t (dolist (nenv (n-a-envs node)) (if (subset-env? nenv env) (return nenv))))))

;;;****** this should not take env as an argument.
(defun true-in-focus? (node env &aux current-env)
  (setq current-env (car (n-a-envs node)))
  (cond ((null current-env)
	 (dolist (nenv (n-a-blocked node)) (if (smart-in-focus? nenv env) (return nenv))))
	((smart-in-focus? current-env env) current-env)
	(t (dolist (nenv (n-a-blocked node))
	     (and (neq nenv current-env) (smart-in-focus? nenv env) (return nenv))))))

(defun generic-true-in? (node env)  ;; Turns out I needed this -- KDF.
  (dolist (nenv (n-a-envs node)) (if (generic-subset-env? nenv env) (return nenv))))

(defun generic-true-in-blocked? (node env) ;; Just added this 7/22/92 -- KDF
  (if *simple-hybrid* 
      (dolist (nenv (n-a-blocked node)) (if (generic-subset-env? nenv env) (return nenv)))
      (generic-true-in? node env)))

;;; Supporting-antecedents is what most users want to call.  It could be made much much 
;;; much faster by weaving for the first.
(defun supporting-antecedents (node env &aux justs)
  (cond ((i-out? node) nil)
	(t (dolist (j (n-a-justifications node))
	     (if (dolist (aenv (antecedent-envs j)) (if (subset-env? aenv env) (return T)))
		 (push j justs)))
	   justs)))

;;; This finds all justifications for node which hold in env.  Env can be a non-subsumed
;;; contradiction.  So this is good for finding justifications for particular contradictions.
;;; This is inefficient.
(defun in-antecedents (node env &aux justs)
  (dolist (j (n-a-justifications node))
    (unless (dolist (n-a (cdr j))
	      (cond ((i-out? n-a))
		    ((dolist (senv (n-a-envs n-a)) (if (subset-env? senv env) (return T))))
		    (t (return T))))
      (push j justs)))
  justs)

;;; If this is used much, it may be useful to cache things.  This determines whether
;;; the given antecedent is a supporter for the current in-antecedent? Notice that
;;; if another justification exists which is simpler, this antecedent will be rejected
;;; even though it could support it.  Caveat emptor.
(defun in-antecedent? (node justification)
  (cond ((i-out? node) nil)
	((dolist (antecedent (cdr justification)) (if (i-out? antecedent) (return T)))
	 nil)
	(t (dolist (env (n-a-envs node))
	     (if (in-antecedent-1? env (cdr justification)) (return T))))))

(defun in-antecedent-1? (env antecedents)
  (or (null antecedents)
      (if (node? (car antecedents))
	  (dolist (senv (n-a-envs (car antecedents)))
	    (when (subset-env? senv env)
	      (if (in-antecedent-1? env (cdr antecedents)) (return T))))
	  (and (memq (car antecedents) (env-assumptions env))
	       (in-antecedent-1? env (cdr antecedents))))))

(defun implies (a c)
  (not
    (dolist (c-env (n-a-envs c))
      (unless (dolist (a-env (n-a-envs a))
		(if (subset-env? a-env c-env) (return T)))
	(return T)))))

(defun known-true? (class)
  (dolist (node (class-nodes class)) (if (i-true? node) (return node))))

(defun known? (class env)
  (dolist (node (class-nodes class)) (if (true-in? node env) (return node))))

(defun known-blocked? (class env)
  (dolist (node (class-nodes class))
    (if (true-in-blocked? node env) (return node))))