;;; -*- 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)
  (setq *mark* (list nil)
	envs (n-a-envs node))
  (cond ((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")))
  (check-explanation node))

(defun explanation-for-nogood (nogood &aux *mark*)
;  (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))
  (explanation-for-nogood-1 nogood)
;  (format T "~% Explanation construction for time ~A is:~D seconds"
;	  nogood
;	  (time-taken start-time))
	)
  

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

  (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 (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))
	       (error "Why am I here")

	       (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))
		     (error "Bad explanation"))
		   (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"))))
    (T (error "Explanation for type ~A is incorrectly implemented" (car reason))))
  result)

(defun explanation-for-justification (just &optional (nogood *contra-env*) &aux *mark*)
  (setq *mark* (list nil))
  (explanation-for-justification-1 just nogood))

(defun explanation-for-justification-1 (just nogood &aux result)
  (setq result (explanation-for-false (just-consequent just)))
  (when (or (null result) (eq result :CIRCULAR))
    (error "Cannot construct explanation for ~A" (just-consequent just)))
  (setq result (explanation-for-just just nogood))
  (when (or (null result) (eq result :CIRCULAR))
    (error "Cannot construct explanation for ~A" just))
  `(JUSTIFY-CONTRADICTION ,just ,(just-consequent just) . ,(just-antecedents just)))

;;; 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)
  (cond ((and (n-a-contradictory node) (not (env-contradictory env))) nil)
	((eq *mark* (n-a-mark node))
	 (cond ((eq :FAIL (n-a-support node)) nil)
	       ((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-support node) nil)
	   ;; 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
	       (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.
	     ;; It cannot fail.
	     (when (i-false? neg)
	       (or (setq result (explanation-for-false neg))
		   (error "Can't find explanation for ~A" result))
	       (if (eq result :CIRCULAR)
		   (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 
			 ;; Do not re-install this.  It will kill explanations
			 ;; you need.  Something like it is needed for efficiency.
			 ;; But not today.  See v24 traces for counterexamples.
			 ;; The problem is that contradicted assumptions introduce
			 ;; non-monotonicity in the propagation.
			 ; (setf (n-a-support node) :FAIL)
			 (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"))
		 )
	   )))

;;; 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 antecedents result)
  (when (eq *mark* (n-a-mark node))
    (return-from explanation-for-false
      (cond ((eq :FAIL (n-a-support node)) nil)
	    (t :CIRCULAR))))
  (setf (n-a-mark node) *mark*)
  (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 ((typep (cdr reason) 'JUST)
	     (explanation-for-false (just-consequent (cdr reason)))

	     (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*)
	     (setq reason (explanation-for-true (n-a-neg node)))
	     (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)
	    (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.
    (BASE (setq result (explanation-for-nogood-1 (assumption-env node)))
	  (if (eq result :CIRCULAR) (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.
(defun explanation-for-class (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)))))))
  (cond (non-circ nil)
	(circ :CIRCULAR)))
	
;;**** is this still right?:::::::
(defun explanation-for-just (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)

;;; The synteax of explanation.
;;; A list of either:
;;; (1) (NEGATION <node1> <node2>). These nodes are negations of each other.
;;; (2) (JUSTIFY-CONTRADICTION just consequent antecedents). Installing this justification.

(defvar *node-count* 0)

;;; This is a tad inefficient as it explores some things multiple times.
(defun check-nogood-explanation (description &aux (*node-count* 0))
  (if (eq (car description) 'JUSTIFY-CONTRADICTION)
      (setq description (cdr description)))
  (dolist (n (cdr description)) (check-explanation n))
;  (format T "~% Nogood explanation contains ~D nodes" *node-count*)
  )

(defun check-explanation (node)
  (incf *node-count*)
  (cond ((null (n-a-support node))
	 (error "Bad explanation --- ~A is not explained." node))
	((eq (n-a-support node) :ASSUMPTION))
	((eq (n-a-support node) :USER))
	((listp (n-a-support node))
	 (dolist (n (cdr (n-a-support node)))
	   (check-explanation n)))
	(t (dolist (n (just-antecedents (n-a-support node)))
	     (check-explanation n)))))

#+Symbolics
(defun show-nogood-dependency (description)
  (if (eq (car description) 'JUSTIFY-CONTRADICTION)
      (setq description (cdr description)))
  (fresh-line)
  (scl:format-graph-from-root description
			      #'(lambda (node stream)
				  #+Symbolics
				  (declare (sys:downward-function))
				  (format stream "~A" 
					  (if (listp node) (car node) (node-string node))))
			      #'(lambda (node)
				  #+Symbolics
				  (declare (sys:downward-function))
				  (cond ((listp node) (cdr node))
					((eq (n-a-support node) :ASSUMPTION) nil)
					((eq (n-a-support node) :USER) nil)
					((listp (n-a-support node)) (cdr (n-a-support node)))
					((just-antecedents (n-a-support node)))))
			      :dont-draw-duplicates t))

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

(defun print-nogood-dependency (description &aux *explained* (*line* 1))
  (format T "~%~A" description)
  (if (eq (car description) 'JUSTIFY-CONTRADICTION)
      (setq description (cdr description)))
  (dolist (child (cdr description))
    (print-nogood-dependency-1 child 1)))

(defun print-nogood-dependency-1 (node indent &aux where name)
  ;; *** There is Format idiom for this I forgot.
  (format T "~%~D:" *line*)
  (dotimes (i indent) (declare (ignore i)) (format T " "))
  (setq name (if (listp node) (car node) node))
  (unless (setq where (assq name *explained*))
    (push (cons name *line*) *explained*))
  (incf *line*)
  (incf indent)
  (format T "~A" name)
  (cond ((i-true? name) (format T "(T)"))
	((i-false? name) (format T "(F)")))
  (cond ((listp node)
	 (if where
	     (format T " explained at line ~D." (cdr where))
	     (dolist (child (cdr node)) (print-nogood-dependency-1 child indent))))
	((eq (n-a-support node) :ASSUMPTION)
	 (format T " :ASSUMPTION."))
	((eq (n-a-support node) :USER)
	 (format T " :USER."))
	((listp (n-a-support node))
	 (cond ((and (listp (car (n-a-support node)))
		     (eq (caar (n-a-support node)) :INVERT))
		(format T " by inverting the just: ")
		(simple-just (cdar (n-a-support node)))
		)
	       (t (format T " via ~A:" (car (n-a-support node)))))
	 (if where
	     (format T " explained at line ~D." (cdr where))
	     (dolist (child (cdr (n-a-support node)))
	       (print-nogood-dependency-1 child indent))))
	(t
	 (format T " via ")
	 (simple-just (n-a-support node))
	 (if where
	     (format T " explained at line ~D." (cdr where))
	     (dolist (child (just-antecedents (n-a-support node)))
	       (print-nogood-dependency-1 child 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))
			   (check-nogood-explanation explanation)
			   (selectq display
			     (:graph (show-nogood-dependency explanation))
			     (:print (print-nogood-dependency 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))))))