;;; -*- 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."

;;; Simple debugging functions.
(defun print-nodes ()
  (format T "~% Nodes:")
  (dolist (node *nodes*)
    (print (list node
		 (string-envs (n-a-envs node))
		 (n-a-enqueued? node)
		 (n-a-consumers node)
		 ))))

;;; This summarizes all the ATMS inputs.
(defun print-inputs ()
  (format T "~%ATMS input forms:")
  (dolist (node *nodes*)
    (dolist (j (n-a-justifications node)) (print-justification node j)))
  (dotimes (i 99.) (dolist (or (aref *ors* i)) (print-or or)))
  )

(defun print-or (or)
;  (format T "~%choose {")
  (do ((disjuncts (disjunction-disjuncts or) (cdr disjuncts)))
      ((null disjuncts))
    (princ (assumption-string (car disjuncts)))
    (if (cdr disjuncts) (princ ",")))
;  (princ "}")
  )

;;; Prints out in format of papers, uses node-datums, uses [] to indicate an assumption.
(defun print-justification (node just)
  (terpri)
  (do ((a (cdr just) (cdr a)))
      ((null a))
    (princ (n-a-string (car a)))
    (if (cdr a) (format T ",")))
  (princ "=>")
  (princ (n-a-string node))
  (princ "      from ")
  (princ (car just)))

(defun n-a-string (n-a)
  (cond ((eq n-a *contra-node*) "FALSE")
	((assumption? n-a) (format nil "[~A]" (n-a-datum n-a)))
	(T (format nil "~A" (n-a-datum n-a)))))

(defun print-contradictions (&aux (count 0))
  (walk-contradictions 
    #'(lambda (env)
	#+Symbolics
	(declare (sys:downward-function))
	(incf count)
	(format T "~&~A:~A (count: ~D)~%   (~A)"
		env (string-env env) (env-count env) (env-contradictory-info env))))
  (format T "~% ~D contradictions total." count))

(defun print-contradictions-fast (&optional (stream t))
  (walk-contradictions 
    #'(lambda (env)
	#+Symbolics
	(declare (sys:downward-function))
	(format stream "~%(")
	(dolist (a (env-assumptions env))
	  (format stream "~D " (assumption-unique a)))
	(format stream ")"))))

(defun check-contradictions ()
  (walk-contradictions #'(lambda (nogood)
			   #+Symbolics
			   (declare (sys:downward-function))
			   (if (subsumed-nogood? nogood)
			       (error "Contradiction error")))))

(defun print-ors ()
  (dotimes (i 100.) (mapc #'print-or (aref *ors* i))))

(defun test-general-weave (known-envs new-partial-envs consequent
		       &optional (node-to-ignore 'IGNORE) &aux k1 k2 n1 n2)
  (multiple-value-setq (k1 n1)
    (ogeneral-weave known-envs new-partial-envs consequent node-to-ignore))
  (multiple-value-setq (k2 n2)
    (user-general-weave known-envs new-partial-envs consequent node-to-ignore))
  (or (= (length k1) (length k2)) (error "Known mismatch"))
  (or (= (length n1) (length n2)) (error "New mismatch."))
  (values k2 n2))

(defvar *node-to-ignore* nil)			; Node to ignore in weaving.
(defvar *known-envs*)
(defvar *new-envs*)

(defun ogeneral-weave (*known-envs* new-partial-envs consequent
		      &optional (*node-to-ignore* 'IGNORE)
		      &aux *new-envs*)
  (unless (dolist (n-a consequent) (if (i-false? n-a) (return T)))
    (dolist (new-partial-env new-partial-envs) (oweave consequent new-partial-env))
    (when *new-envs*
      (setq *known-envs* (fcopylist *known-envs*))
      (dolist (new-env *new-envs*)
	(mapl #'(lambda (known-env)
		  (and (car known-env)
		       (subset-env? new-env (car known-env))
		       (rplaca known-env nil)))
	     *known-envs*))
      (setq *known-envs* (nconc (fdelqa nil *known-envs*) *new-envs*))))
  (values *known-envs* *new-envs*))


;;; This is slow but right.
(defun oweave (nodes-to-process partial-env &aux new-env n-a)
  (setq n-a (car nodes-to-process))
  (cond ((or (eq n-a *node-to-ignore*) (if n-a (i-true? n-a)))
	 (oweave (cdr nodes-to-process) partial-env))
	((dolist (known-env *known-envs*)
	   (if (subset-env? known-env partial-env) (return T))))
	((dolist (new-env *new-envs*)
	   (if (subset-env? new-env partial-env) (return T))))
	((null nodes-to-process)
	 (mapl #'(lambda (new-env)
		   (when (subset-env? partial-env (car new-env))
		     (rplaca new-env nil)))
	       *new-envs*)
						;*** too many delqs'
	 (setq *new-envs* (cons partial-env (fdelqa nil *new-envs*))))
	((node? n-a)
	 (dolist (env (n-a-envs n-a))
	   (unless (env-contradictory (setq new-env (union-env partial-env env)))
	     (oweave (cdr nodes-to-process) new-env))))
	(t (unless (env-contradictory (setq new-env (cons-env partial-env n-a)))
	     (oweave (cdr nodes-to-process) new-env)))))



;;; This deletes any supersets of set2 in set1 preserving as much list structure as possible.
;;; Is hackery really worth it?
;(defun safely-delete-subsets (set1 set2 &aux new-set2)
;  (when set2
;    (setq new-set2 (safely-delete-subsets set1 (cdr set2)))
;    (cond ((dolist (item1 set1) (if (subset-env? item1 (car set2)) (return T))) new-set2)
;	  ((eq (cdr set2) new-set2) set2)
;	  (t (cons (car set2) new-set2)))))




(defun print-statistics (solutions &aux count)
  (format T "~% Number of solutions: ~D" (length solutions))
  (format T "~% Number of consumers invoked ~D" *consumer-invokations*)
  (format T "~% Number of TMS nodes: ~D" (1- *node-counter*))
  (format T "~% Number of TMS classes: ~D" (length *classes*))
  (format T "~% Number of contradictions: ~D" (1- *contra-counter*))
  (format T "~% Number of assumptions: ~D" (1- *assumption-counter*))
  (format T "~% Number of environments: ~D" (1- *env-counter*))
  (format T "~% Number of large union calculations: ~D" *big-union-count*)
  (format T "~% Number of full resolution steps: ~D" *full-resolution-count*)
  (format T "~% Minimal nogood resolutions ~D" *minimal-nogood-count*)
  (format T "~% Number of failed full resolution steps: ~D" *full-resolution-fail-count*)
  (format T "~% Number of justifications: ~D" *justification-count*)
  (format T "~% Number of binary resolutions: ~D" *binary-resolution-count*)
  (format T "~% Number of exhaustions: ~D" *exhaustions*)
  (format T "~% Number of edges in ADDB search tree: ~D" *addb-check-count*)
  (format T "~% Size of maximum nogood constructed: ~D" *max-contra-count*)
  (format T "~% Size of maximum nogood resolved with: ~D" *max-nogood-used-size*)
  (dotimes (i (1+ *max-contra-count*))
    (setq count (count-nogoods i))
    (when (> count 0)
      (format T "~% There are ~D base contradictions of size ~D" count i)))
  (dotimes (i (array-length *environments*))
    (when (aref *environments* i)
      (format T "~% There are ~D base environments of size ~D"
	      (length (aref *environments* i)) i)))
  (justification-statistics)
  solutions)

;;; If this is called a lot, this can be optimized by keeping counts explicitly.
(defun count-nogoods (size)
  (let ((count 0))
    (if *single-nogood-tree*
	(walk-extended-tree #'(lambda (env)
				#+Symbolics
				(declare (sys:downward-function))
				(if (= (env-count env) size) (incf count)))
			    *nogood-tree*)
	(walk-tree #'(lambda (ignore)
		       #+Symbolics
		       (declare (sys:downward-function))
		       (incf count))
		   (aref *nogood-trees* size)))
    count))

(defun env-total ()
  (let ((count 0))
    (dolist (n *nodes*)
      (if *simple-hybrid*
	  (incf count (length (n-a-blocked n)))
	  (incf count (length (n-a-envs n)))))
    (dolist (n *assumptions*)
      (if *simple-hybrid*
	  (incf count (length (n-a-blocked n)))
	  (incf count (length (n-a-envs n)))))
    count))

(defun smallest-nogood (&aux (min 100000000.))
  (if *single-nogood-tree*
      (walk-extended-tree #'(lambda (e)
			      #+Symbolics
			      (declare (sys:downward-function))
			      (if (< (env-count e) min) (setq min (env-count e))))
			    *nogood-tree*)
	)
  min)

(defun total-nogoods (&optional print)
  (let ((count 0)
	(length 0)
	(max 0))
    (if *single-nogood-tree*
	(walk-extended-tree #'(lambda (e)
			        #+Symbolics
				(declare (sys:downward-function))
				(incf count)
				(incf length (env-count e))
				(if (> (env-count e) max) (setq max (env-count e))))
			    *nogood-tree*)
	)
    (when print
      (format T "~% Total (minimal nogoods): ~D, Maximum size: ~D, Average size: ~D"
	      count max (/ (float length) count)))
    (values count (unless (= count 0) (/ (float length) count) max))))

(defun scan-nodes (&aux (total 0) count fcount bcount (btotal 0) (ftotal 0))
  (dolist (n *nodes*)
    (when (n-a-envs n)
      (setq count (length (n-a-envs n))
	    fcount 0
	    bcount (length (n-a-blocked n)))
      (incf btotal bcount)

      (dolist (e (n-a-envs n))
	(if (dolist (f *foci*) (if (subset-env? e f) (return T)))
	    (incf fcount)))
      (format T "~% ~A has ~D environments, ~D in focus, ~D blocked"
	      n count fcount bcount)
      (incf ftotal fcount)
      (incf total count)))
  (dolist (n *assumptions*)
    (when (n-a-envs n)
      (setq count (length (n-a-envs n))
	    fcount 0
	    bcount (length (n-a-blocked n)))
      (incf btotal bcount)

      (dolist (e (n-a-envs n))
	(if (dolist (f *foci*) (if (subset-env? e f) (return T)))
	    (incf fcount)))
      (format T "~% ~A has ~D environments, ~D in focus, ~D blocked"
	      n count fcount bcount)
      (incf ftotal fcount)
      (incf total count)))
  (format T "~% Total non-blocked encountered: ~D (should be ~D) blocked ~D"
	  total ftotal btotal))

;;; This gives info about free nodes too --- needs more work.
(defun justification-statistics (&aux j-array c-array too-big size
				 (true 0) (false 0) (nothing 0))
  (setq j-array (make-array 1000. :ELEMENT-TYPE '(INTEGER 0 65536) :INITIAL-ELEMENT 0)
	c-array (make-array 1000. :ELEMENT-TYPE '(INTEGER 0 65536) :INITIAL-ELEMENT 0))
  (dolist (n *nodes*)
    (if (i-true? n)
	(incf true)
	(if (i-false? n) (incf false) (unless (n-a-envs n) (incf nothing))))
    (setq size (length (n-a-justifications n)))
    (if (> size 1000.)
	(push n too-big)
	(incf (aref j-array size)))
    (setq size (length (n-a-consequents n)))
    (if (> size 1000.)
	(push n too-big)
	(incf (aref c-array size))))
  ;; Right now *assumptions* are on a different list: A mistake!
(dolist (n *assumptions*)
    (if (i-true? n)
	(incf true)
	(if (i-false? n) (incf false) (unless (n-a-envs n) (incf nothing))))
    (setq size (length (n-a-justifications n)))
    (if (> size 1000.)
	(push n too-big)
	(incf (aref j-array size)))
    (setq size (length (n-a-consequents n)))
    (if (> size 1000.)
	(push n too-big)
	(incf (aref c-array size))))

  (format T "~% ~D true nodes; ~D false nodes; ~D empty labels" true false nothing)
  (format T "~% ~D nodes had too many justifications/consequents" (length too-big))
  (format T "~% Number of justifications per node:")
  (dotimes (i 1000.)
    (setq size (aref j-array i))
    (unless (= size 0)
      (format T "~%  ~D nodes with ~D justifications" size i)))
  (format T "~% Number of consequences per node:")
  (dotimes (i 1000.)
    (setq size (aref c-array i))
    (unless (= size 0)
      (format T "~%  ~D nodes with ~D consequences" size i))))

(defun check-order (as &optional msg)
  (do ((as as (cdr as)))
      ((null (cdr as)))
    (unless (assumption-orderp (car as) (cadr as)) (error "Illegal order: ~A" msg))))

(defun check-env-array ()
  (dotimes (i (array-length *environments*))
    (dolist (e (aref *environments* i))
      (if (env-contradictory e)
	  (format T "~% Contradictory env ~A found in slot ~D" e i)))))

(defun test-cons-env (l) (dolist (r l) (cons-env (car r) (cadr r))))

(defun clear-cons-env-cache ()
  (dotimes (i (array-length *environments*))
    (dolist (e (aref *environments* i))
      (setf (env-cons-env-cache e) nil))))

(defun clear-cons-env-cache1 ()
  (dotimes (i (array-length *environments*))
    (dolist (e (aref *environments* i))
      (if (env-cons-env-cache e)
	  (rplacd (env-cons-env-cache e) nil)))))

(defun lookat-caches ()
  (dotimes (i (array-length *environments*))
    (dolist (e (aref *environments* i))
      (when (cdr (env-cons-env-cache e))
	(format T "~% ~A ~A" e (cdr (env-cons-env-cache e)))))))

;;; ******** need a list of environments somehwerew********** *environments* is not it.
(defun check-env-cache (&aux cache count acount)
  (dotimes (i (array-length *environments*))
    (dolist (e (aref *environments* i))
      (when (setq cache (env-cons-env-cache e))
	(setq count 0 acount 0)
	(dolist (c (cdr cache)) (if (assumption-contradictory (car c)) (incf acount))
				(if (env-contradictory (cdr c)) (incf count)))
	(if (> count 0) (format T "~% ~A has ~D contradictions in cache" e count))
	(if (> acount 0) (format T "~% ~A has ~D bad assumptions in cache" e acount))))))

(defun clear-string-cache () (clrhash *env-string-table*))
						
(defun clean-blocked-labels ()
  (dolist (n-a *nodes*)
    (setf (n-a-blocked n-a) (fcopylist (n-a-blocked n-a)))))

;;; This finds how many environments are in the hash table and how many
;;; are contradictory.
(defun scan-envs (&aux goods vectors contras slot)
  (setq goods 0 vectors 0 contras 0)
  (let ((ptr (hash-array *env-hash-table*)))
    #+Symbolics (declare (sys:array-register ptr ))
    (dotimes (p3 (hash-p2 *env-hash-table*))
      (setq slot (aref ptr p3))
      (cond ((null slot))
	    ((listp slot) (incf vectors))
	    ((env-contradictory slot) (incf contras))
	    (t (incf goods)))))
  (format T "~% Of ~D possible, ~D are good, ~D are vectors, ~D are contradictory"
	  (hash-p2 *env-hash-table*) goods vectors contras))

(defun check-hash-vectors-blits (&aux slot)
  (let ((ptr (hash-array *env-hash-table*)))
    #+Symbolics (declare (sys:array-register ptr ))
    (dotimes (p3 (hash-p2 *env-hash-table*))
      (setq slot (aref ptr p3))
      (cond ((null slot))
	    ((listp slot) (check-blit-vector slot))
	    (t (check-blit-vector (env-vector slot)))))))

(defun check-blit-vector (vector)
  (dolist (n vector)
    (cond ((integerp n))
	  ((> (car n) 1))
	  ((< (car n) -1))
	  (t (error "Badly formatted vector: ~A" vector))
	  )))

;;; This is only partially right, because it ignores earlier nogoods (if there are
;;; more than three nodes).
(defun consistent-nodes? (the-nodes)
  (do ((envs (tms::node-envs (car the-nodes))
	     (tms::union-envss (tms::node-envs (car nodes)) envs))	;
       (nodes (cdr the-nodes) (cdr nodes))
       (last-envs nil)
       (last-node (car the-nodes)))
      ((or (null envs) (null nodes))
       (cond ((null envs)
	      (values nil (find-env-union-killer (tms::node-envs last-node)
							     last-envs)))
	     ((null (cdr nodes)) ;out of them
	      envs)))
    (setq last-envs envs last-node (car nodes))))

(defun consistent-nodes-blocked? (the-nodes)
  (do ((envs (tms::n-a-blocked (car the-nodes))
	     (tms::union-envss (tms::node-envs (car nodes)) envs))	;
       (nodes (cdr the-nodes) (cdr nodes))
       (last-envs nil)
       (last-node (car the-nodes)))
      ((or (null envs) (null nodes))
       (cond ((null envs)
	      (values nil (find-env-union-killer (tms::node-envs last-node)
							     last-envs)))
	     ((null (cdr nodes)) ;out of them
	      envs)))
    (setq last-envs envs last-node (car nodes))))

;;; This is only partially right, because it only returns the first nogood.
(defun find-env-union-killer (e1s e2s &aux result)
  (dolist (e1 e1s)
    (dolist (e2 e2s)
      (setq result (tms::find-nogood-for-assumptions
		     (tms::assumptions-union (tms::env-assumptions e1)
					     (tms::env-assumptions e2))
		     nil))
      (if result (return-from FIND-ENV-UNION-KILLER result)))))

; Obsolete.
;(defun print-union-stats (&aux total max count contras l bige)
;  (setq total 0 contras 0 count 0)
;  (do ((i 1 (1+ i)))
;      ((> i *max-env-count*))
;    (dolist (e (aref *environments* i))
;      (incf count)
;      (setq l (or (car (env-unions e)) 0))
;      (incf total l)
;      (when (or (null max) (< max l)) (setq max l bige e))
;      (dolist (p (cdr (env-unions e)))
;	(if (eq (cdr p) *contra-env*) (incf contras)))))
;  (format T "~% ~D environments, longest cache= ~D(~A), average cache=~D, % contra=~D"
;	  count max bige (// total count) (// (* contras 100.) total)))

(defun print-hs ()
  (selectq *h4*
    (NIL (format T "~% Rule *h4* is disabled."))
    (1 (format T "~% Rule *h4* is enabled."))
    (2 (format T "~% Rule *h4* applies to other than binary disjunctions."))
    (T (format T "~% Illegal value for *h4*: ~A" *h4*)))
  (if *h45* (format T "~% Rule *h45* is enabled.") (format T "~% Rule *h45* is disabled.")))

(defun why-nogood (n-a-e)
  (cond ((assumption? n-a-e)
	 (why-nogood-assumption n-a-e))))

(defun why-nogood-assumption (a)
  (selectq (car (assumption-contradictory a))
    (BASE (format T "~% Assumption ~A is false because its singleton environment is.")
	  (why-nogood-env (cdr (assumption-contradictory a))))
    (T (error "Uninimplemented"))))

;;; Returns a justification/resolution for false killing the nogood.
(defun why-nogood-env (env &aux reason)
  (unless (env-contradictory env) (error "Environment is consistent."))
  (if (eq env *contra-env*)
      (error "Environment is non-unique --- try why-nogood-assumptions."))
  (setq env (find-base-contradiction env))
  (setq reason (cdr (env-contradictory-info env)))
  (if (eq (car reason) 'DOUBLE-FOR-FALSE) (setq reason (cadr reason)))
  (selectq (car reason)
    (BACK-PROPAGATE (cadr reason))
    (LABEL-FOR-FALSE2 (fourth reason))
    (LABEL-FOR-FALSE (cddr reason))
    (RESOLUTION (cdr reason))
    (WEAVING-FOR-FALSE (cdr reason))
    (T (error "Unknown contradiction reason: ~A" (car reason)))))

;;; Finds the env killing the assumptions, or in a few cases a justification
;;; which is killing it (i.e., the env itself was never created).
(defun find-nogood-for-assumptions (assumptions &optional (is-nogood T) &aux env v)
  (dolist (a assumptions)
    (if (i-false? a) (return-from FIND-NOGOOD-FOR-ASSUMPTIONS (assumption-env a))))
  (setq env (find-or-make-env assumptions))
  (cond ((eq env *contra-env*)
	 (cond ((not (compatible-assumptions? assumptions
					      (setq v (make-env-vector* assumptions))))
		(do ((as assumptions (cdr as)))
		    ((null as))
		  (dolist (a (cdr as))
		    (when (vector-member (car as) (assumption-binary-vector a))
		      (return-from FIND-NOGOOD-FOR-ASSUMPTIONS
			(or (double-if-exists (car as) a)
			    (list *contra-node* '<UNKNOWN-INFORMANT> (car as) a))))))
		(format T "~% ATMS data base contains an error.")
		(dolist (a assumptions)
		  (if (vector-intersection? (assumption-binary-vector a) v)
		      (error " Problem is around ~A" a))))
	       ((new-contradictory-env-assumptions? assumptions
						    (length assumptions)))
	       (t (error "Can't find the nogood killing the assumptions, but something is"))))
	((env-contradictory env) (find-base-contradiction env))
	(is-nogood (error "The assumptions are consistent"))))

;;; Returns a justification for false killing the assumption set.  This
;;; finds only one, and for the moment, doesn't necessarily return the
;;; informant.
;;; This should now call find-nogood-for-assumptions.  Who still calls why-nogood-assumptions?
;;; *****
(defun why-nogood-assumptions (assumptions &optional dont-lookup &aux env)
  (setq env (if dont-lookup *contra-env* (find-or-make-env assumptions)))
;  (unless (env-contradictory env) (error "Assumptions are consistent!?"))
  (cond ((not (eq env *contra-env*)) (why-nogood-env env))
	((not (compatible-assumptions? assumptions (make-env-vector* assumptions)))
	 (do ((as assumptions (cdr as)))
	     ((null as) (error "Can't happen"))
	   (dolist (a (cdr as))
	     (when (vector-member (car as) (assumption-binary-vector a))
	       (return-from why-nogood-assumptions
		 (list '<UNKNOWN-INFORMANT> (car as) a))))))
	((setq env (new-contradictory-env-assumptions? assumptions (length assumptions)))
	 (why-nogood-env env))
;	(t (error "Uh --- I can't find a reason why the assumptions are inconsistent"))
	))

;;; Checks all known nodes to make sure they their label is right.
(defun check-node-labels ()
  (dolist (node *nodes*) (check-node-label node)))

(defun ltms-nodes-check ()
  (if *ltms-mark-env*
      (dolist (node *nodes*)
	(if (eq (car (n-a-envs node)) *ltms-mark-env*)
	    (format T "~% ~A has LTMS mark" node)))))

;;; Inefficient but straight forward.  This checks only for missing envs right now.
(defun check-node-label (node &aux old-envs envs)
  (setq old-envs (append (n-a-envs node) nil))	;**** want non-cdr coded copy.
  (dolist (j (n-a-justifications node))
    (setq envs (user-general-weave nil *empty-env-list* (cdr j)))
    (dolist (env envs)
      (cond ((memq env old-envs))
	    ((dolist (old-env old-envs) (if (subset-env? old-env env) (return T))))
	    (t (error "Missing env ~A" env))))))

;;; Checks all known nodes have no nils in their label.

(defun check-nodes () (dolist (node *nodes*) (check-node-envs node)))

(defun check-node-envs (node)
  (if (memq nil (n-a-envs node)) (error "Node ~A has nil in its label" node)))

(defun check-env-table ()
  (dotimes (i (1+ *max-env-count*))
    (dolist (e (aref *environments* i))
      (check-an-env e))))

(defun check-contra-table () (walk-contradictions #'check-an-env))
      
(defun walk-contradictions (function &optional (>i 0))
  #+Symbolics
  (declare (sys:downward-funarg function))
  (cond ((null *single-nogood-tree*)
	 (dotimes (i (1+ *max-contra-count*))
	   (unless (<= i >i)
	     (walk-tree function (aref *nogood-trees* i)))))
	(*nogood-tree* (walk-tree-4 function *nogood-tree*))))

;;; This misses binary nogoods.
(defun check-an-env (e &aux contra assumptions)
  (setq assumptions (env-assumptions e))
  (do ((assumptions assumptions next)
       (next (cdr assumptions) (cdr next)))
      ((null next))
    (unless (> (assumption-unique (car assumptions)) (assumption-unique (cadr assumptions)))
      (format T "~% ~A has its assumptions in bad order" e)))
  (setq contra (new-contradictory-env-assumptions? (env-assumptions e)
						   (env-count e)))
  (cond ((null contra)
	 (if (and (env-contradictory e) (subsumed-nogood? e))
	     (format T "~% ~A is marked contradictory when it shouldn't be" e)))
	((null (env-contradictory e))
	 (format T "~% ~A is not marked contradictory when it contains the nogood ~A"
		 e contra)
	 (print e)
	 (print contra)
	 )
	((subsumed-nogood? e)
	 (if (eq e contra)
	     (format T "~% ~A is marked subsumed, but isn't" e)))
	((eq e contra))
	(t (format T "~% ~A is subsumed by ~A but not marked as such" e contra))))

;;; This makes sure a label is good.
(defun check-envs (envs)
  (do ((envs envs (cdr envs)))
      ((null envs))
    (do ((tail (cdr envs) (cdr tail)))
	((null tail))
      (if (memq (compare-env (car envs) (car tail)) '(SUBSET12 SUBSET21 EQUAL))
	  (error "Lossage")))))

(defun check-just-node-labels ()
  (dolist (node *nodes*)
    (if (n-a-blocked node) (check-envs (n-a-blocked node)) (check-envs (n-a-envs node)))))

;;; This checks for DOWNING's bug which has a screwed up cache on singleton envs.  This
;;; is inefficient but works.
(defun check-doubles (&aux env cache)
  (dolist (assumption *assumptions*)
    (setq env (assumption-env assumption)
	  cache (cdr (env-cons-env-cache env)))
    (if cache
	(maphash #'(lambda (other-assumption double-env)
		     (unless (and (memq other-assumption (env-assumptions double-env))
				  (memq assumption (env-assumptions double-env))
				  (> (assumption-unique other-assumption)
				     (assumption-unique assumption)))
		       (error "Screwed up cache")))
		 cache))))

;;; 
(defun check-assumptions ()
  (do ((as *assumptions* (cdr as)))
      ((null as))
    (dolist (e (assumption-envs (car as)))
      (cond ((> (env-count e) 1))
	    ((eq (car (env-assumptions e)) (car as)))
	    ((memq (assumption-env (car as)) (assumption-envs (car (env-assumptions e))))
	     (format T "~% Assumptions ~A and ~A are equivalent"
		     (car as) (car (env-assumptions e))))
	    (t (format T "~% Assumption ~A depends on assumption ~B"
		       (car as) (car (env-assumptions e))))))))

(defun ensure-monitoring ()
  #+Symbolics
  (unless meter:*pc-monitor-array*
    (format T "~% PC array does not exist---I'm creating one")
    (meter:make-pc-array (* sys:page-size 64.))
    (meter:monitor-all-functions)))

(defun nogood-distribution ()
  (if *single-nogood-tree*
      (nogood-distribution-tree)
      (nogood-distribution-trees)))

(defun nogood-distribution-trees (&aux (total 0) count result)
  (dotimes (i (1+ *max-contra-count*))
    (setq count (count-tree (aref *nogood-trees* i)))
    (unless (= count 0)
      (incf total count)
      (push (cons i count) result)))
  (values result total))

;;; If this gets called a lot this can be made much faster.
(defun nogood-distribution-tree (&aux distribution (total 0))
  (walk-extended-tree #'(lambda (env &aux count slot)
			  #+Symbolics
			  (declare (sys:downward-function))
			  (incf total)
			  (setq count (env-count env)
				slot (assoc count distribution :test #'=))
			  (if slot
			      (incf (cdr slot))
			      (setq distribution (cons (cons count 1) distribution))))
		      *nogood-tree*)
  (values distribution total))

;;; This overcounts binary nogoods if there are singleton nogoods.*****
;;;***** why are there singletons in the tree?****
(defun print-nogood-distribution (&aux distribution total (ones 0) (twos 0))
  (dolist (a *assumptions*)
    (cond ((or (i-false? a) (i-true? a)) (incf ones))
	  (t (incf twos (count-bits-blots (assumption-binary-vector a))))))
  (format T "~% ~D nogoods of size ~D" ones 1)
  (format T "~% ~D nogoods of size ~D" twos 2)
  
  (multiple-value-setq (distribution total)
    (nogood-distribution))

  total

  (setq distribution (sort distribution #'(lambda (x y) (< (car x) (car y)))))
  (if (equal (caar distribution) 1) (pop distribution))
  (if (equal (caar distribution) 2) (pop distribution))
  (push (cons 2 ones) distribution)
  (push (cons 1 ones) distribution)
  (dolist (bucket distribution)
    (format T "~% ~D nogoods of size ~D" (cdr bucket) (car bucket))))

;;;For ADB.
(defun nogoods-between (lower upper)
  (if (>= upper *max-contra-count*) (setq upper *max-contra-count*))
  (if *single-nogood-tree*
      (nogoods-between-tree lower upper)
      (nogoods-between-trees lower upper)))

(defun nogoods-between-trees (lower upper &aux result)
  (unless (<= upper lower)
     (do ((i lower (1+ i)))
	 ((> i upper))
       (setq result (append (collect-minimal-nogoods i) result))))
  result)

;;; Returns all minimal nogoods of size i.
(defun collect-minimal-nogoods (i)
  (if *single-nogood-tree* (error "Unimplemented"))
  (collect-tree (aref *nogood-trees* i)))

(defun nogoods-between-tree (lower upper &aux result)
  (walk-extended-tree #'(lambda (env &aux count)
			  #+Symbolics
			  (declare (sys:downward-function))
			  (setq count (env-count env))
			  (and (>= count lower)
			       (<= count upper)
			       (push env result)))
		      *nogood-tree*)
  result)

;;; Acceptance tests of a new ATMS.  We should add a lot more here after time.

;;; bits/break *c012*:T/NIL *k*=2,3,4.

(defun accept ()
  (setq *c012* nil) (install-bits)
  (basic-accept)
  (install-break)
  (basic-accept)
  (setq *c012* T)
  (basic-accept)
  (install-bits)
  (basic-accept))

(defun basic-accept ()
  (setq *h4* nil *k* nil)
  (unless (= (length (freuder-1)) 2)
    (error "(freuder-1) generated wrong number of solutions"))
  (setq *h4* 1 *k* nil)
  (unless (= (length (freuder-1)) 2)
    (error "(freuder-1) generated wrong number of solutions"))
  (unless (= (length (freuder-2)) 6)
    (error "(freuder-2) generated wrong number of solutions"))
  (setq *h4* nil *k* nil)
  (unless (null (freuder-3))
    (error "(freuder-3) generated wrong number of solutions"))
  (setq *h4* 1 *k* 3)
  (unless (null (freuder-3))
    (error "(freuder-3) generated wrong number of solutions"))
  (setq *h4* nil *k* nil)
  (basic-basic-accept)
  (setq *h4* 1 *k* 2)
  (basic-basic-accept)
  (setq *k* 3)
  (basic-basic-accept)
  (setq *k* nil)
  (basic-basic-accept))

(defun basic-basic-accept ()

  (unless (= (length (n-queens 8)) 92.)
    (error "(n-queens 8) generated wrong number of solutions"))

  (unless (= (length (ib-1)) 1176.)
    (error "(ib-1) generated wrong number of solutions"))

  (unless (= (length (tn-queens 7)) 28.)
    (error "(tn-queens 7) generated wrong number of solutions"))

  (init-tms) (parity 9)
  
  (replay-all-trace-files))

(defun replay-all-trace-files ()
  (dolist (file '(">atms>trace>new-bug.trace"
		  ">atms>trace>ptest3-ir.trace"
		  ">atms>trace>ptest3-level.trace"
		  ">atms>trace>qpe-bug.txt"
		  ">atms>trace>trace.lisp"
		  ">atms>trace>v2-tms-tracea.txt"
		  ">atms>trace>v2-tms-traceb.txt"
		  ">atms>trace>v2-tms-tracec.txt"
		  ">atms>trace>gordon.lisp"
		  ))
    (replay file nil)))

;;; This runs short ATMS tests.
(defun short-test ()
  (dolist (file '(">atms>trace>ex1.trace"
		  ">atms>trace>ex2.trace"
		  ">atms>trace>ex3.trace"
		  ">atms>trace>ex4.trace"		  
		  ">atms>trace>ex5.trace"))
    (format T "~% Replaying file ~A" file)
    (replay file nil nil t)
    (profile-replay))
  (n-queens 8)
  (n-queens 9)
  (n-queens 10))

(defun benchmark ()
  (benchmark-files 3 '(">atms>trace>ex1.trace"
		       ">atms>trace>ex2.trace"
		       ">atms>trace>ex4.trace"
		       ">atms>trace>ex5.trace"))
  (benchmark-files 1 '(">atms>trace>ex3.trace"
		       ">atms>trace>ex7.trace"))
  (bench-queens)

  )

#+Symbolics
(defun benchmark-files (repeats files &aux (output zl:terminal-io))
  (let ((*standard-output* #'si:null-stream))
    (dolist (file files)
      (replay file nil nil T)
      (format output "~% ~D runs of ~A with gc-off but preemption allowed" repeats file)
      (si:gc-off)
      (dotimes (i repeats)
	(declare (ignore i))
	(time (profile-replay nil nil)))
      (format output "~% ~D runs of ~A with gc-off preemption disallowed" repeats file)
      (dotimes (i repeats) 
	(declare (ignore i))
	(time (process:without-preemption (profile-replay nil nil))))
      (si:gc-on))))

#+Symbolics
(defun bench-queens ()
  (let ((*standard-output* #'si:null-stream))
    (si:gc-off)
    (dotimes (i 3)
      (declare (ignore i))
      (time (n-queens 8)))
    (dotimes (i 3)
      (declare (ignore i))
      (time (process:without-preemption (n-queens 8))))
    (dotimes (i 3)
      (declare (ignore i))
      (time (dn-queens 8 t)))
    (dotimes (i 3)
      (declare (ignore i))
      (time (process:without-preemption (n-queens 8 t))))))


(defun node (u)
  (dolist (n *nodes*) (if (eq (n-a-unique n) u) (return n))))

;;; So you can get a particular env.
(defun e (n)
  (catch 'E
    (dotimes (i (1+ *max-env-count*))
      (dolist (e (aref *environments* i)) (if (= (env-unique e) n) (throw 'E e)))
      (walk-contradictions #'(lambda (e)
			       #+Symbolics
			       (declare (sys:downward-function))
			       (if (= (env-unique e) n) (throw 'E e)))))))

;;; Explanation facilities.

;;; This I suspect misses a few types of justifications for false for which the
;;; nogoods have to be consed.  So a little more work is required...
;;; This is pretty slow.
;;; The consensus explanation can be compressed. n-a-neg is redundant.***

(defvar *mark* nil)

(defun explanation-for-node (node &optional env &aux *mark* envs result)
  (setq *mark* (list nil)
	envs (n-a-envs node))
  (setq result
	(cond ;; This line must go first?
	  (env (explanation-for-node-1 node env))
	  ((n-a-contradictory node) (explanation-for-false node))
	  ((i-true? node) (explanation-for-true node))
	  (env (explanation-for-node-1 node env))
	  ((null envs) (error "Nothing to explain"))
	  ((null (cdr envs)) (explanation-for-node-1 node (car envs)))
	  (t (error "Which env is to be explained"))))
  result)

(defun explanation-for-nogood (nogood &aux *mark* result)
;  (setq start-time (get-internal-run-time))
  (unless *explain-flag* (format T "~% *explain-flag* is not set to T, you will lose."))
  (setq *mark* (list nil))
  (setq result (explanation-for-nogood-1 nogood))
  (if (eq result :CIRCULAR)
      (error "Impossible circular result"))
  result
;  (format T "~% Explanation construction for time ~A is:~D seconds"
;	  nogood
;	  (time-taken start-time))
	)
  

;;;***** exdplanations for nogood may be constructed too many times.
(defun explanation-for-nogood-1 (nogood &optional reason &aux result1 result2 result)
  (or reason
      (setq nogood (find-base-contradiction nogood)
	    reason (cdr (env-contradictory-info nogood))))
  (do nil (nil)
    ;;***** optimize so justify-node needs not be constructed.
    (cond ((typep reason 'just) (setq reason (cons 'JUSTIFY-NODE reason)) (return nil)))
    (cond ((memq (car reason) '(DOUBLE-FOR-FALSE CONS-FOR-FALSE UNIONS-FOR-FALSE
						 UNION-FOR-FALSE1))
	   (setq reason (cadr reason)))
	  ((eq (car reason) 'WEAVING-FOR-FALSE)
	   (setq reason (car (last reason))))
	  ((eq (car reason) 'WEAVE-FOR-FALSE)
	   (setq reason (cdr reason)))
	  (t (return nil))))
  (selectq (car reason)
    ;; Newly installed justification to a false node.
    (JUSTIFY-NODE (setq result (explanation-for-justification-1 (cdr reason) nogood)))
    (CONSENSUS (setq result1 (explanation-for-node-1 (second reason) (fourth reason)))
	       (when (or (null result1) (eq result1 :CIRCULAR))
		 (return-from explanation-for-nogood-1 result1))
	       ;; Do the easy case.
	       (dolist (env (fifth reason))
		 (when (subset-env? env nogood)
		   (unless (setq result2 (explanation-for-node-1 (third reason) env))
		     (return-from explanation-for-nogood-1 nil))
		   (when (eq result2 :CIRCULAR)
		     (return-from explanation-for-nogood-1 :CIRCULAR))
		   (return-from explanation-for-nogood-1
		     (list nogood :CONSENSUS (third reason) result1 result2))))
	       (error "Unimplemented 6")
	       (unless (setq result (explanation-for-node-1 (third reason) nogood))
		 (error "Bad Explanation"))
	       (when (eq result :CIRCULAR)
		 (return-from explanation-for-nogood-1 :CIRCULAR))
	       (setq result
		     (list 'NEGATION (second reason) (third reason)))
	       (unless result (error "Something fishy")))
    ;; Env is contradictory because the node is false.
    (SET-NODES (setq result (n-a-contradictory (cadr reason)))
	       (cond ((and (eq (car result) 'PROPAGATE-FALSE-1)
			   (typep (cdr result) 'JUST))
		      ;; This could be more efficient, as we know the just.
		      (setq result (explanation-for-false (cadr reason)))
		      (if (or (eq result :CIRCULAR) (null result))
			  (return-from explanation-for-nogood-1 result))
		      (return-from explanation-for-nogood-1
			(list nogood :SUPPORTS-CONTRADICTION :UNUSED result)))
		     (t (error "Unimplemented SET-NODES reason"))))
	       
    (REMOVED-TRUE-ASSUMPTION2
      (setq result1 (explanation-for-nogood-1 (fourth reason) (cdr (sixth reason))))
      (if (or (null result1) (eq result1 :CIRCULAR))
	  (return-from explanation-for-nogood-1 result1))
      (setq result2 (explanation-for-true (second reason)))
      (if (or (null result2) (eq result2 :CIRCULAR))
	  (return-from explanation-for-nogood-1 result2))
      (return-from explanation-for-nogood-1
	(list nogood :UNIT-RESOLUTION (third reason) result2 result1)))
    (T (error "Explanation for type ~A is incorrectly implemented" (car reason))))
  result)

(defun explanation-for-justification (just &optional (nogood *contra-env*) &aux *mark*)
  (error "What is this ever called for")
  (setq *mark* (list nil))
  (explanation-for-justification-1 just nogood))

;;; The consequent is false, and the antecedents contribute the nogood.
(defun explanation-for-justification-1 (just nogood &aux result1 result2)
  (setq result1 (explanation-for-false (just-consequent just)))
  (when (or (null result1) (eq result1 :CIRCULAR))
    (error "Cannot construct explanation for ~A" (just-consequent just)))
  (setq result2 (explanation-for-just just nogood))
  (when (or (null result2) (eq result2 :CIRCULAR))
    (error "Cannot construct explanation for ~A" just))
  `(,nogood :JUSTIFY-CONTRADICTION ,just ,result1 . ,(cdr result2)))

;;; Reason looks like (BASE RESOLUTION OR (a . nogood-1) ...)
(defun explain-resolution-result (env reason &aux result table)
  env
  (setq table (or-nogood-explanations (second reason)))
  (dolist (pair (fourth reason)) (push (cadr (or (assoc pair table :test #'EQUAL)
						 (error "not found")))
				       result))
  result)

;  (explain-resolution-result-1 env (or-disjuncts (caddr reason)) (or-nogoods (caddr reason))))

(defun explain-resolution-result-1 (env disjuncts nogoods &aux result)
  (if (null disjuncts)
      T
      (dolist (nogood-1 (cddr (assq (car disjuncts) nogoods)))
	(cond ((env-contradictory nogood-1))
	      ((null (setq result (explain-resolution-result-1 env (cdr disjuncts) nogoods))))
	      (t (return (cons (find-nogood-for-assumptions (cons (car disjuncts)
								  (env-assumptions nogood-1)))
			       (unless (eq result T) result))))))))

;;; Results:
;;;   NIL = failed to find any explanation.
;;;   List = the list of justifications needed.

;;; Mark=*mark*
;;; Support=Just 

;;; This still searches too much.*****


;;; If env is consistent, it should always succeed or an error is signalled.
;;; If env is nogood, then a NIL means it couldn't construct an explanation.
;;; The circular flag is for my debugging, it has no functional purpose.

;;; Returns two values.  Ultimately NIL=FAIL with second argument the circular
;;; responsibilities.


(defun explanation-for-node-1 (node env &aux result neg circ non-circ open-result)
  (unless (eq *mark* (n-a-mark node))
    (setf (n-a-mark node) *mark*)
    (setf (n-a-support node) nil))

  (and (n-a-contradictory node)
       (not (env-contradictory env))
       (return-from explanation-for-node-1 nil))

  ;; Check whether an existing derivation for this node exists.  Return it.
  ;; This requires very very very carefull thinking before you change it sir.
  (unless open-result
    (dolist (old-support (n-a-support node))
      (cond ((eq :FALSE (car old-support)))
	    ((not (subset-env? (car old-support) env)))
	    ((null (cdr old-support)))
	    ((eq (cdr old-support) :ON-STACK)
	     (if (eq (car old-support) env)
	     (return-from explanation-for-node-1 :CIRCULAR)))
	    (t (return-from explanation-for-node-1 old-support)))))

  (setq open-result (assq env (n-a-support node)))

  (cond ((and (assumption? node) (memq node (env-assumptions-delay env)))
	 (cond ((eq (assumption-env node) (car open-result))
		(rplacd open-result (list node :ASSUMPTION)))
	       (t (setq open-result (list (assumption-env node) node :ASSUMPTION))
		  ;;***** At this point can't the larger env be thrown away???????*****
		  (push open-result (n-a-support node))))
	 open-result)
	(t (unless open-result
	     (setq open-result (cons env nil))
	     (push open-result (n-a-support node)))
	   (rplacd open-result :ON-STACK)
	   ;; The primary source of environments is the justifications.
	   (dolist (j (n-a-justifications node))
	     (setq result (explanation-for-just j env))
	     (if (null result) (setq non-circ T))
	     (if (eq result :CIRCULAR) (setq circ T result nil))
	     (when result
	       (rplacd open-result (cons node result))
	       (return-from EXPLANATION-FOR-NODE-1 open-result)))
	   ;; Another source is the class its negation is part of.
	   (when (setq neg (n-a-neg node))
	     (dolist (class (n-a-classes neg))
	       (setq result (explanation-for-class node class env))
	       (cond ((eq result :CIRCULAR) (setq result nil))
		     ;;**** should explanation-for-class do this?
		     (result (setq result (cons env (cons class result)))
			     (rplacd open-result result)
			     (return-from EXPLANATION-FOR-NODE-1 result))))
	     ;; This is an ordering problem in propagate-false-1.
	     (when (and (not (assumption? neg))
			(node-assumption neg)
			(i-false? (node-assumption neg)))
	       (setq result (explanation-for-false (node-assumption neg)))
	       (cond ((eq result :CIRCULAR) (setq result nil))
		     ;;***** not right?
		     (t (rplaca open-result *empty-env*)
			(rplacd open-result
				`(,node :NEGATION-IS-FALSE ,result))
			(return-from explanation-for-node-1 open-result))))
	     
	     ;; Another source is false propagation on the node's negation.
	     (when (i-false? neg)
	       (setq result (explanation-for-false neg))
	       (when (or (null result) (eq result :CIRCULAR))
		 (rplacd open-result nil)
		 (return-from explanation-for-node-1 result))
	       (rplacd open-result
		       `(,node :NEGATION-IS-FALSE ,result))
	       (return-from EXPLANATION-FOR-NODE-1 open-result))
	     )
	   ;;**** Only constrcut circularities on contra-envs, not worth it for the rest.
	   (cond ((env-contradictory env) 
		  (rplacd open-result nil)
		  (if circ :CIRCULAR))
		 (circ (rplacd open-result nil) :CIRCULAR)
		 (non-circ (setf (n-a-mark node) nil);***
			   (error "Should not fail"))
		 )
	   )))

;;; Node is contradictory.  Build an explanation for it.
;;; Currently cannot fail.  If can fail mark needs to be reset to nil.
(defun explanation-for-false (node &aux reason result collect open-result)
  (unless (eq *mark* (n-a-mark node))
    (setf (n-a-mark node) *mark*)
    (setf (n-a-support node) nil))

  ;; Check whether an existing derivation for this node exists.  Return it.
  (dolist (old-support (n-a-support node))
    (cond ((neq (car old-support) :FALSE))
	  ((null (cdr old-support)) (setq open-result old-support) (return nil))
	  ((eq (cdr old-support) :ON-STACK) (return-from explanation-for-false :CIRCULAR))
	  (t (return-from explanation-for-false old-support))))

  (when (eq node *contra-node*)
    (setq result '(:FALSE :USER))
    (return-from explanation-for-false result))

  (unless open-result
    (setq open-result (cons :FALSE nil))
    (push open-result (n-a-support node)))

  (setq reason (n-a-contradictory node))
  ;;;******* SEARCH FOR ALL POSSIBLE CAUSES.
  (selectq (car reason)
    (PROPAGATE-FALSE-1
            ;; If the type is a justification. This is forced by antecedents.
      (cond ((typep (cdr reason) 'JUST)
	     (let ((subresult (explanation-for-false (just-consequent (cdr reason)))))
	       (when (or (null subresult) (eq subresult :CIRCULAR))
		 (rplacd open-result nil)
		 (return-from explanation-for-false subresult))
	       (push subresult collect))
	     (dolist (a (just-antecedents (cdr reason)))
	       (unless (eq a node)
		 (setq result (explanation-for-true a))
		 (cond ((null result) (return-from explanation-for-false nil))
		       ((eq :CIRCULAR result) (return-from explanation-for-false :CIRCULAR))
		       (t (push result collect)))))
	     (rplacd open-result (cons node (cons (cdr reason) collect)))
	     open-result)
	    ((typep (cdr reason) 'CLASS)
	     ;; The class is exclusive and some other node is true.
	     (dolist (other (class-nodes (cdr reason)))
	       (cond ((eq other node))
		     ((i-true? other)
		      (setq result (explanation-for-true other))
		      (unless (or (eq result :CIRCULAR) (null result))
			(return-from EXPLANATION-FOR-FALSE
			  `(:FALSE ,node ,(cdr reason) ,result)))))))
	    ((typep (cdr reason) 'CLAUSE)
	     (error "Unimplemented 11"))
	    ((eq (cdr reason) 'NEGATION-IS-TRUE)
	     (setq result (explanation-for-true (n-a-neg node)))
	     (when (or (null result) (eq result :CIRCULAR))
	       (rplacd open-result nil)
	       (return-from explanation-for-false result))
	     (rplacd open-result (list node :NEGATION-IS-TRUE result))
	     open-result)
	    ;; This means the n-a is we are looking at a contradictory assumption.
	    ((eq (cadr reason) 'BASE)
	     (setq result (explanation-for-nogood-1 (assumption-env node)))
	     (cond ((or (null result) (eq result :CIRCULAR))
		    (rplacd open-result nil)
		    (return-from explanation-for-false result))
		   (t (rplacd open-result `(,node :NOGOOD ,result))
		      (return-from explanation-for-false open-result))))
	    (T ;; Not an error, just here for debugging.
	       (error "~% External contradiction>?: ~A" reason)
	       T)))
    ;; This means the n-a is we are looking at a contradictory assumption.
    ;;***** is this code still reachable?  WHy two places?
    (BASE (error "Unimplemneted 13")
	  (setq result (explanation-for-nogood-1 (assumption-env node)))
	  (when (eq result :CIRCULAR)
	    (setf (n-a-mark node) nil);****
	    (return-from explanation-for-false :CIRCULAR))

	  (setf (n-a-support node) result)
	  T)
	  
    (T (error "~A is an unknown contradiction reason" (car reason)))))

;;; Inefficient way out.
(defun explanation-for-true (node)
  (explanation-for-node-1 node *empty-env*))

;;; Result=othernode if success.
;;; ****
;;; 8/4/93---the semantics of :CIRCULAR are still not consistent.
;;; [1] :CIRCULAR return means that no explanation was found, but one explanation
;;; path was not pursued because of a circularity.  **** Probably if an explanation
;;; was not found and it wasn't because of a circularity we should mark that node 
;;; as failed.  We do not do that consistently right now here.
;;; [2] :CIRCULAR means all paths are circular.  This could is written with the semantics
;;; that :CIRCULAR means all paths are circular.  This means a NIL could be returned
;;; even though some path is circular.  Someday it might be worth rewriting this so that 
;;; the returned values are (a) :ALL-CIRCULAR (b) :NON-CIRCULAR (c) success.  :SOME-CIRCULAR?

(defun explanation-for-class (node class env &aux aenv neg result circ non-circ collect)
  (setq neg (n-a-neg node))
  (when (class-exclusive class)
    (dolist (other-node (class-nodes class))
      (unless (eq other-node neg)
	(cond ((setq aenv (or (true-in? other-node env)
			      (and (not (n-a-contradictory other-node))
				   (memq other-node *set-nodes*)
				   *empty-env*)))
	       (setq result (explanation-for-node-1 other-node aenv))
	       (cond ((null result) (setq non-circ T) nil)
		     ((eq result :CIRCULAR) (setq result nil circ T) nil)
		     (result (return-from EXPLANATION-FOR-CLASS (list other-node result)))))
	      ((env-contradictory env)
	       (setq result (explanation-for-node-1 other-node env))
	       (cond ((null result) (setq non-circ T) nil)
		     ((eq result :CIRCULAR) (setq result nil circ T) nil)
		     (result
		      (return-from EXPLANATION-FOR-CLASS (list other-node result)))))))))
  ;; Special case for propagation of TRUE/FALSE.
  ;; This is a oneof class and all the other nodes are false.
  ;;**** the following makes no sense.
;  (when (and (class-oneof class)
;	     (i-true? node)
;	     (null (dolist (other-node (class-nodes class))
;		     (unless (eq other-node node)
;		       (unless (i-false? other-node) (return T))))))
;    (dolist (other-node (class-nodes class))
;      (unless (eq other-node node)
;	(setq result (explanation-for-false other-node))
;	(cond ((eq result :CIRCULAR) (setq result nil circ T) (return nil))
;	      ((null result) (setq non-circ T) (return nil))
;	      (t (push result collect)))))
;    (return-from EXPLANATION-FOR-CLASS `(:ONEOF ., collect)))

  ;; Remember :CIRCULAR means :ALL-CIRCULAR.
  (cond (non-circ nil)
	(circ :CIRCULAR)))
	
(defun explanation-for-just (j env &aux aenv result circ non-circ collect)
  ;;***** this check may make no difference either?
  ;; **** This check may just slow things done, check some day.??
;  (dolist (n (just-antecedents j))
;    (if (n-a-contradictory n) (return-from explanation-for-just nil)))

  (zf (env-contradictory env)
      ;;******* Opaque code:
      (dolist (n (just-antecedents j))

	(setq result nil)

	(when (setq aenv (true-in? n env))
	  (setq result (explanation-for-node-1 n aenv))
	  (cond ((null result) (setq non-circ T))
		((eq result :CIRCULAR) (setq result nil circ T))
		(t (push result collect))))
	(when (and (null result) (memq env (n-a-contra-envs n)))
	  (setq result (explanation-for-node-1 n env))
	  (cond ((null result) (setq non-circ T))
		((eq result :CIRCULAR) (setq result nil circ T))
		(t (push result collect))))
	;;*** :CIRCULAR here means always circular.  This is wierd.

	(unless result
	  (return-from EXPLANATION-FOR-JUST
	    (cond (non-circ nil)
		  (circ :CIRCULAR)))))

      (dolist (n (just-antecedents j)) (if (i-out? n) (return-from EXPLANATION-FOR-JUST nil)))
      ;; Be very carefull, circularities can trip us up here all over.
      (unless (dolist (aenv (antecedent-envs j))
		(and (subset-env? aenv env)
		     (null (dolist (n (just-antecedents j))
			     (setq result (explanation-for-node-1 n aenv))
			     (cond ((null result) (setq non-circ T) (return T))
				   ((eq result :CIRCULAR) (setq result nil circ T)
				    (return T))
				   (t (push result collect)))))
		     (return T)))
	(return-from EXPLANATION-FOR-JUST (cond (non-circ nil) (circ :CIRCULAR)))))
  (cons j collect))

#+Symbolics
(defun show-explanation (explanation)
  (fresh-line)
  (scl:format-graph-from-root explanation
			      #'(lambda (entry stream)
				  (declare (sys:downward-function))
				  (print-node-name entry stream))
			      #'entry-supporters
			      :dont-draw-duplicates t))

(defun entry-supporters (entry)
  (cond ((typep (car entry) 'ENV)
	 (cdddr entry))
	((eq (car entry) :FALSE)
	 (cond ((eq (third entry) :NOGOOD)
		(cdddr entry))
	       ((eq (cadr entry) :USER) nil)
	       ((eq (third entry) :NEGATION-IS-TRUE)
		(cdddr entry))
	       ((typep (third entry) 'JUST)
		(cdddr entry))
	       ((typep (third entry) 'CLASS)
		(cdddr entry))
	       (t (error "Unhandled :FALSE"))))
	(t (error "unhandled entry type"))))


(defun print-node-name (entry stream)
  (cond ((or (memq (cadr entry)
		   '(:CONSENSUS :SUPPORTS-CONTRADICTION :USER
				:JUSTIFY-CONTRADICTION :UNIT-RESOLUTION))
	     (typep (cadr entry) 'class))
	 (format stream "~A" (car entry)))
	((assumption? (cadr entry))
	 (format stream "A~D" (assumption-unique (cadr entry))))
	(t (format stream "N~D" (n-a-unique (cadr entry))))))


(defvar *explained* nil)
(defvar *line* 0)

(defun print-explanation (explanation &aux *explained* (*line* 1))
  (print-explanation-1 explanation 1))

(defun print-explanation-1 (entry indent &aux where)
  ;; *** There is Format idiom for this I forgot.
  (format T "~%~D:" *line*)
  (dotimes (i indent) (declare (ignore i)) (format T " "))
  (unless (setq where (assq entry *explained*))
    (push (cons entry *line*) *explained*))
  (incf *line*)
  (incf indent)
  (print-node-name entry t)
  (cond ((eq (car entry) *empty-env*) (format T "(T)"))
	((eq (car entry) :FALSE) (format T "(F)")))
  (cond (where (format T " explained at line ~D." (cdr where))
	       (return-from print-explanation-1 nil))
	((typep (third entry) 'just)
	 (format T " via ")
	 (simple-just (third entry)))
	((eq (third entry) :NEGATION-IS-FALSE)
	 (format T " Because its negation is false."))
	((eq (third entry) :ASSUMPTION)
	 (format T " is assumed."))
	((eq (second entry) :CONSENSUS)
	 (format T " is nogood because N~D and its negation N~D are derivable."
		 (n-a-unique (third entry))
		 (n-a-unique (n-a-neg (third entry)))))
	((eq (third entry) :NOGOOD)
	 (format T " Because singleton environment ~A became nogood."
		 (assumption-env (second entry))))
	((eq (third entry) :NEGATION-IS-TRUE)
	 (format T " Because its negation is true."))
	((eq (second entry) :SUPPORTS-CONTRADICTION)
	 (format T " Because justification for false:")
	 (simple-just (third entry)))
	((and (eq (first entry) :FALSE)
	      (typep (third entry) 'JUST))
	 (format T " by inverting the just: ")
	 (simple-just (third entry)))
	((eq (second entry) :JUSTIFY-CONTRADICTION)
	 (format T " Because justification for false*:"
		 (simple-just (third entry))))
	((eq (second entry) :UNIT-RESOLUTION)
	 (format T " Because assumption has become true in ~A."
		 (third entry)))
	((eq (third entry) :ONEOF)
	 (format T " oneof from class ~D" (class-unique (second entry))))
	((typep (second entry) 'CLASS)
	 (format T " via class ~D" (class-unique (second entry))))
	(t (error "Unimplemented")))
  (dolist (supporter (entry-supporters entry)) (print-explanation-1 supporter indent)))

(defun simple-just (just &aux previous)
  (dolist (a (just-antecedents just))
    (if previous (format T ","))
    (setq previous a)
    (format T "~D" (n-a-unique a)))
  (format T "->")
  (format T "~D" (n-a-unique (just-consequent just))))

;;; This skips the singleton and binary nogoods which isn't right.
(defun explain-all-nogoods (&optional (display #+:Symbolics :graph #-:Symbolics :print))
  (walk-contradictions #'(lambda (nogood &aux explanation)
			   #+Symbolics
			   (declare (sys:downward-function))
			   (setq explanation (explanation-for-nogood nogood))
			   (selectq display
			     (:graph (show-explanation explanation))
			     (:print (print-explanation explanation))))))

(defun explain-all-nodes (&aux explanation)
  (dolist (n *nodes*)
    (cond ((n-a-contradictory n)
	   (setq explanation (explanation-for-node n))
	   (if (or (null explanation) (eq explanation :CIRCULAR)) (error "Explanation bug"))

;	   (show-explanation explanation)
	   )
	  (t (dolist (env (n-a-envs n))
	       (setq explanation (explanation-for-node n env))
	       (if (or (null explanation) (eq explanation :CIRCULAR))
		   (error "Explanation bug"))

;	       (show-explanation explanation)
	       )))))

(defun explain-all-assumptions (&aux explanation)
  (dolist (n *assumptions*)
    (cond ((n-a-contradictory n)
	   (setq explanation (explanation-for-node n))
	   (if (or (null explanation) (eq explanation :CIRCULAR)) (error "Explanation bug"))

;	   (show-explanation explanation)
	   )
	  (t (dolist (env (n-a-envs n))
	       (setq explanation (explanation-for-node n env))
	       (if (or (null explanation) (eq explanation :CIRCULAR))
		   (error "Explanation bug"))

;	       (show-explanation explanation)
	       )))))

;;; Tests for union-envs.

(defun test-u (l) (dolist (p l) (union-envss (car p) (cadr p))))

(defun test-us (l &aux r1 r2)
  (dolist (p l) (setq r1 (union-envss1 (car p) (cadr p))
		      r2 (union-envss2 (car p) (cadr p)))
	  (unless (same-setp r1 r2) (error "Bug in some union-envs"))))

(defun same-setp (s1 s2)
  (cond ((equal s1 s2))
	((not= (length s1) (length s2)) nil)
	(t (dolist (e1 s1 T) (unless (memq e1 s2) (return-from SAME-SETP nil))))))

;;; Returns retracts, adds.  Inefficient, but who cares.
(defun compare-sets (set1 adds &aux retracts)
  (cond ((null adds) set1)
	(t (setq adds (fcopylist adds))
	   (dolist (e set1)
	     (cond ((memq e adds) (setq adds (fdelq1 e adds)))
		   (t (push e retracts))))
	   (values retracts adds))))

(defun check-c ()
  (dolist (n *nodes*)
    (and (in-focus? n)
	 (n-a-has-consumers? n)
	 (print n))))

(defun look-at-all ()
  (dolist (a *assumptions*) (look-at-assumption-envs a)))

(defun look-at-assumption-envs (a &aux (contras 0) (total 0) (has-nodes 0))
  (dolist (env (assumption-in-envs a))
    (incf total)
    (cond ((env-contradictory env) (incf contras))
	  ((env-nodes env) (incf has-nodes))))

  (if (> total 0)
      (format T "~% ~A Total: ~D, Contras: ~D, Have nodes: ~D"
	      a total contras has-nodes))

  )

;;; For timing creation.
(defun time-creation (n)
  (dotimes (i n)
    (declare (ignore i))
    (basic-make-assumption 'a 'b 'c)))

;;; Checks whether all ltms supports are correct.
(defun check-ltms-supports () (dolist (n *nodes*) (check-ltms-support n)))

(defun check-ltms-support (n &aux support env)
  (setq support (n-a-support n)
	env (n-a-envs n))

  (cond ((null env) (if support (format T "~% Node ~A has empty label but support?" n)))
	((null support) (error "Node ~A has support but no label" n))
	((eq support :ASSUMPTION))
	((null (clause-positives support))
	 (dolist (ante (just-antecedents support))
	   (unless (n-a-envs ante)
	     (error "Invalid supporting justification ~A, missing label for antecedent ~A"
		    support ante))))
	((neq n (clause-consequent support))
	 (error "Consequent of clause ~A is ~A, should be ~A"
		support (clause-consequent support) n))
	(t (dolist (ante (clause-negatives support))
	     (unless (or (eq ante (n-a-neg (clause-consequent support)))
			 (n-a-envs ante))
	       (error "Invalid support clause ~A, missing label for antecedent ~A"
		      support ante))))))

;;;; From old monotonic versions.

;;**** is this still right?:::::::
(defun explanation-for-just-old (j env &aux aenv result circ non-circ)
  ;;***** this check may make no difference either?

  (if (eq (just-thread j) *mark*) (return-from explanation-for-just nil))

  ;; **** This check may just slow things done, check some day.??
;  (dolist (n (just-antecedents j))
;    (if (n-a-contradictory n) (return-from explanation-for-just nil)))

  (zf (env-contradictory env)
      ;;******* Opaque code:
      (dolist (n (just-antecedents j))
	(unless
	  (cond ((setq aenv (true-in? n env))
		 (setq result (explanation-for-node-1 n aenv))
		 (if (null result) (setq non-circ T))
		 (if (eq result :CIRCULAR) (setq result nil circ T))
		 result)
		((memq env (n-a-contra-envs n))
		 (setq result (explanation-for-node-1 n env))
		 (if (null result) (setq non-circ T))
		 (if (eq result :CIRCULAR) (setq result nil circ T))
		 result))
	  (return-from EXPLANATION-FOR-JUST
	    (cond (non-circ (setf (just-thread j) *mark*) nil)
		  (circ :CIRCULAR)))))
      (dolist (n (just-antecedents j)) (if (i-out? n) (return-from EXPLANATION-FOR-JUST nil)))
      ;; Be very carefull, circularities can trip us up here all over.
      (unless (dolist (aenv (antecedent-envs j))
		(and (subset-env? aenv env)
		     (null (dolist (n (just-antecedents j))
			     (setq result (explanation-for-node-1 n aenv))
			     (if (null result) (setq non-circ T))
			     (if (eq result :CIRCULAR) (setq result nil circ T))
			     (unless result
			       (return T))))
		     (return T)))
	(return-from EXPLANATION-FOR-JUST (cond (non-circ nil) (circ :CIRCULAR)))))
  T)

(defun explanation-for-node-1-old (node env &aux result neg circ non-circ)
;  (if (memq (n-a-unique node) '(5646 5641 5778 5772 5591))
;      (print (list 'explanation-for-node-1 node env)))

;  (cond ((= (n-a-unique node) 5591.)
;	 (print (list 'see node env (eq *mark* (n-a-mark node))))
;	 (if (eq *mark* (n-a-mark node)) (error "Can't"))
;
;	 ))
  (cond ((and (n-a-contradictory node) (not (env-contradictory env))) nil)
	((eq *mark* (n-a-mark node))
	 (cond ((n-a-support node) T)
	       (t :CIRCULAR)))
	((and (assumption? node) (memq node (env-assumptions-delay env)))
	 (setf (n-a-mark node) *mark*)
	 (setf (n-a-support node) :ASSUMPTION)
	 T)
	(t (setf (n-a-mark node) *mark*)
	   (setf (n-a-blocked node) 'EXPLANATION-FOR-NODE-1)
	   (setf (n-a-support node) nil)
	   ;; The primary source of environments is the justifications.
	   (dolist (j (n-a-justifications node))
	     (if (memq (n-a-unique node) '(5641 5546 5778))
		 (print (list 'processing j)))

	     (setq result (explanation-for-just j env))
	     (if (memq (n-a-unique node) '(5641 5546 5778))
		 (print (list 'processing-result result)))


	     (if (null result) (setq non-circ T))
	     (if (eq result :CIRCULAR) (setq circ T result nil))
	     (when result
	       (setf (n-a-support node) j)
	       (return-from EXPLANATION-FOR-NODE-1 T)))
	   ;; Another source is the class its negation is part of.
	   (when (setq neg (n-a-neg node))
	     (dolist (class (n-a-classes neg))
	       (setq result (explanation-for-class node class env))
	       (if (eq result :CIRCULAR) (setq result nil))
	       (when result
		 (setf (n-a-support node) (list class result))
		 (return-from EXPLANATION-FOR-NODE-1 T)))
	     ;; This is an ordering problem in propagate-false-1.
	     (when (and (not (assumption? neg))
			(node-assumption neg)
			(i-false? (node-assumption neg)))
	       (setq result (explanation-for-false (node-assumption neg)))
	       (if (eq result :CIRCULAR) (setq result nil))
	       (when result
		 ;; This is a funny negation.
		 (setf (n-a-support node) (list :NEGATION-IS-FALSE (node-assumption neg)))
		 (return-from EXPLANATION-FOR-NODE-1 T)))

	     ;; Another source is false propagation on the node's negation.
	     (when (i-false? neg)
	       (setq result (explanation-for-false neg))
	       (unless result
		 (setf (n-a-mark node) nil)
		 (return-from explanation-for-node-1 nil))
	       (when (eq result :CIRCULAR)
		 (setf (n-a-mark node) nil)
		 (return-from EXPLANATION-FOR-NODE-1 result))
	       (setf (n-a-support node) (list :NEGATION-IS-FALSE neg))
	       (return-from EXPLANATION-FOR-NODE-1 T)))
	   ;;**** Only constrcut circularities on contra-envs, not worth it for the rest.
	   (cond ((env-contradictory env) 
		  (cond (circ (setf (n-a-mark node) nil) :CIRCULAR)
			(t (setf (n-a-mark node) nil)
			   nil)))
		 (circ (setf (n-a-mark node) nil) :CIRCULAR )
		 (non-circ (setf (n-a-mark node) nil) (error "Should not fail"))
		 )
	   )))

(defun explanation-for-class-old (node class env &aux aenv neg result circ non-circ)
  (setq neg (n-a-neg node))
  (when (class-exclusive class)
    (dolist (other-node (class-nodes class))
      (unless (eq other-node neg)
	(cond ((setq aenv (or (true-in? other-node env)
			      (and (not (n-a-contradictory other-node))
				   (memq other-node *set-nodes*)
				   *empty-env*)))
	       (setq result (explanation-for-node-1 other-node aenv))
	       (if (null result) (setq non-circ T))
	       (if (eq result :CIRCULAR) (setq result nil circ T))
	       (if result (return-from EXPLANATION-FOR-CLASS other-node)))
	      ((env-contradictory env)
	       (setq result (explanation-for-node-1 other-node env))
	       (if (null result) (setq non-circ T))
	       ;;**** cleanup soon.
	       (if (eq result :CIRCULAR) (setq result nil circ T))
	       (if result (return-from EXPLANATION-FOR-CLASS other-node)))))))
  ;; Special case for propagation of TRUE/FALSE.
  (when (and (class-oneof class)
	     (i-true? node)
	     (null (dolist (other-node (class-nodes class))
		     (unless (eq other-node node)
		       (unless (i-false? other-node) (return T))))))
    (dolist (other-node (class-nodes class))
      (unless (eq other-node node)
	(setq result (explanation-for-false other-node))
	(cond ((eq result :CIRCULAR) (setq result nil circ T) (return nil))
	      ((null result) (setq non-circ T) (return nil))))))
  ;; Remember :CIRCULAR means :ALL-CIRCULAR.
  (cond (non-circ nil)
	(circ :CIRCULAR)))

(defun explanation-for-false-old (node &aux reason antecedents result)
  (cond ((or (= (n-a-unique node) 5885.) (= (n-a-unique node) 5851.))
	 (print (list 'see node))))

  (when (eq *mark* (n-a-mark node))
    (return-from explanation-for-false
      (cond ((n-a-support node) T)
	    (t :CIRCULAR))))
  (setf (n-a-mark node) *mark*)
  (setf (n-a-blocked node) 'EXPLANATION-FOR-FALSE)
  (when (eq node *contra-node*)
    (setf (n-a-support node) :USER)
    (return-from explanation-for-false T))
  (setf (n-a-support node) nil)
  (setq reason (n-a-contradictory node))
  ;;;******* SEARCH FOR ALL POSSIBLE CAUSES.
  (selectq (car reason)
    (PROPAGATE-FALSE-1
            ;; If the type is a justification. This is forced by antecedents.
      
      (cond ((or (= (n-a-unique node) 5885.) (= (n-a-unique node) 5851.))
	     (print (list 'seehere node))))


      (cond ((typep (cdr reason) 'JUST)
	     (let ((subresult (explanation-for-false (just-consequent (cdr reason)))))
	       (when (neq T subresult)
		 (setf (n-a-mark node) nil)
		 (return-from explanation-for-false subresult)))
	     (dolist (a (just-antecedents (cdr reason)))
	       (unless (eq a node)
		 (explanation-for-true a)
		 (push a antecedents)))
	     (push (just-consequent (cdr reason)) antecedents)
	     (setf (n-a-support node) (cons (cons :INVERT (cdr reason)) antecedents))
	     T)
	    ((typep (cdr reason) 'CLASS)
	     (error "Unimplemented"))
	    ((typep (cdr reason) 'CLAUSE)
	     (error "Unimplemented"))
	    ((eq (cdr reason) 'NEGATION-IS-TRUE)
	     (setf (n-a-mark node) *mark*)
	     (setf (n-a-blocked node) 'explanation-for-false)
	     (setq reason (explanation-for-true (n-a-neg node)))
	     (setf (n-a-mark node) nil)
	     (unless reason (return-from explanation-for-false nil))
	     (if (eq reason :CIRCULAR) (return-from explanation-for-false :CIRCULAR))
	     (setf (n-a-support node) (list :NEGATION-IS-TRUE (n-a-neg node)))
	     T)
	    ;; This means the n-a is we are looking at a contradictory assumption.
	    ((eq (cadr reason) 'BASE)
	     (setq result (explanation-for-nogood-1 (assumption-env node)))
	     (when (eq result :CIRCULAR)
	       (setf (n-a-mark node) nil)
	       (return-from explanation-for-false :CIRCULAR))
	     (setf (n-a-support node) result)
	     T)
	    (T ;; Not an error, just here for debugging.
	       (error "~% External contradiction>?: ~A" reason)
	       T)))
    ;; This means the n-a is we are looking at a contradictory assumption.
    ;;***** is this code still reachable?  WHy two places?
    (BASE (setq result (explanation-for-nogood-1 (assumption-env node)))
	  (when (eq result :CIRCULAR)
	    (setf (n-a-mark node) nil)
	    (return-from explanation-for-false :CIRCULAR))

	  (setf (n-a-support node) result)
	  T)
	  
    (T (error "~A is an unknown contradiction reason" (car reason))))
  (setf (n-a-mark node) nil))


(defun explanation-for-nogood-1-old (nogood &optional reason &aux result)

  (or reason
      (setq nogood (find-base-contradiction nogood)
	    reason (cdr (env-contradictory-info nogood))))
;  (format T "~%Tree for ~A:~A" nogood (env-assumptions-delay nogood))
  (do nil (nil)
    ;;***** optimize so justify-node needs not be constructed.
    (cond ((typep reason 'just) (setq reason (cons 'JUSTIFY-NODE reason)) (return nil)))
    (cond ((memq (car reason) '(DOUBLE-FOR-FALSE CONS-FOR-FALSE UNIONS-FOR-FALSE
						 UNION-FOR-FALSE1))
	   (setq reason (cadr reason)))
	  ((eq (car reason) 'WEAVING-FOR-FALSE)
	   (setq reason (car (last reason))))
	  ((eq (car reason) 'WEAVE-FOR-FALSE)
	   (setq reason (cdr reason)))
	  (t (return nil))))
  (selectq (car reason)
    ;; Newly installed justification to a false node.
    (JUSTIFY-NODE (setq result (explanation-for-justification-1 (cdr reason) nogood)))
    (CONSENSUS (print 'lookinghere)
	       
	       (setq result (explanation-for-node-1 (second reason) (fourth reason)))
	       (unless result
		 (error "No explanation found for ~A" (second reason)))
;	       (if (eq result :CIRCULAR)
;		   (return-from explanation-for-nogood-1 :CIRCULAR))
	       (print (list 'env-circ))
	       (setq result nil)
	       ;; Do the easy case.
	       (dolist (env (fifth reason))
		 (when (subset-env? env nogood)
		   (unless (setq result (explanation-for-node-1 (third reason) env))
		     (return-from explanation-for-nogood-1 nil))
		   (when (eq result :CIRCULAR)
		     (return-from explanation-for-nogood-1 :CIRCULAR))
		   (setq result
			 (list 'NEGATION (second reason) (third reason)))
		   (return nil)))
	       (unless result
		 (unless (setq result (explanation-for-node-1 (third reason) nogood))
		   (error "Bad Explanation"))
		 (when (eq result :CIRCULAR)
		   (return-from explanation-for-nogood-1 :CIRCULAR))
		 (setq result
		       (list 'NEGATION (second reason) (third reason)))
		 (unless result (error "Something fishy"))))
    ;; Env is contradictory because the node is false.
    ;; *** set-nodes might be flushable as a reason.  Use justify-contradiction.
    (SET-NODES (setq result (n-a-contradictory (cadr reason)))
	       (cond ((and (eq (car result) 'PROPAGATE-FALSE-1)
			   (typep (cdr result) 'JUST))
		      (let ((subresult (explanation-for-false (cadr reason))))
			(if (or (eq subresult :CIRCULAR) (null subresult))
			    (return-from explanation-for-nogood-1 subresult)))

		      (setq result `(JUSTIFY-CONTRADICTION ,(cdr result)
							   ,(just-consequent (cdr result))
							   .,(just-antecedents (cdr result)))))
		     (t (error "Unimplemented SET-NODES reason"))))
	       
    (REMOVED-TRUE-ASSUMPTION2
      (setq result (explanation-for-nogood-1 (fourth reason) (cdr (sixth reason))))
      (if (eq result :CIRCULAR) (return-from explanation-for-nogood-1 :CIRCULAR))
      (explanation-for-true (second reason))
      T)
    (T (error "Explanation for type ~A is incorrectly implemented" (car reason))))
  result)

(defun explain-all-nogoods-old (&optional (display #+:Symbolics :graph #-:Symbolics :print))
  (walk-contradictions #'(lambda (nogood &aux explanation)
			   #+Symbolics
			   (declare (sys:downward-function))
			   (setq explanation (explanation-for-nogood nogood))
			   (check-nogood-explanation explanation)
			   (selectq display
			     (:graph (show-nogood-dependency explanation))
			     (:print (print-nogood-dependency explanation))))))