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

;;; A dumb version.  Assumes all classes are XOR.
;;; Note that this returns a set of environments for every interpretation.  This is
;;; because the assumptions need not be independent.
(defun solutions (&aux interpretations new-interpretations new-interp start-time)
  (setq start-time (get-internal-run-time))
  (setq interpretations (list (list *empty-env*)))
  (dolist (class *classes*)
    (when (class-nodes class)
      (dolist (node (class-nodes class))
	(dolist (old-e interpretations)
	  (setq new-interp (union-envss (n-a-envs node) old-e))
	  (if new-interp (push new-interp new-interpretations))))
      (setq interpretations new-interpretations
	    new-interpretations nil)
      (unless interpretations
	(format T "~%Couldn't add class ~A=*t*" class) (setq *t* class)
	(return nil))))
  (format T "~% Solution construction time is:~D seconds" (time-taken start-time))
  interpretations)

(defvar *interp-trace* nil)

(defun env-interpretations () (convert-interpretations (interpretations)))

;;; Use interp-group on result of this function to identify isomorphic interpretations.
;;; Can be called with a starting seed.
(defun interpretations (&optional dont-minimize (start *empty-env*)
			&aux l start-time nl ne 
			actives universals universal xors 
			unconstrained-xors nuniversals)
  nuniversals
  ;; **** under cosntruction.
  dont-minimize
  universal
  unconstrained-xors
  xors
  ne
  nl

  (setq start-time (get-internal-run-time))
  (setq l (list start))
  (dolist (a *assumptions*)
    (if (eq (assumption-gc-status a) 'DONT) (setf (assumption-gc-status a) 'DO)))
  (setq actives (active-assumptions start))
; Important to do someday for efficiency.  Any assumption which appears in no nogoods
; of any form, make it universal.
;  (dolist (a actives)
;    (unless (dependent-assumption? a) (push a nuniversals)))
  (if *interp-trace* (format T "~%Universals:"))
  (dolist (u universals)
    (if *interp-trace* (format T "~% True assumption: ~A" (string-assumption u))))
  ;; ******* The ATMS can figure out variables itself.  They are xors whose
  ;; assumptions occur in only one disjunct!!!!!!! That is much better than this crock.
  ;; *variables* is a list of one-of classes. node-assumption pairs (fix someday).
  ;; ******** make sure somewhere that satisfied disjuncts are marked in some way.
  (setq l (variable-interpretations))
  ;; Process the rest of the disjunctive array, in order, but only those
  ;; not associated with a variable.
  ;; ******* xors interacts with actives ****** this feature is not used.
  ;; Walk through the XOR's, this is easy.
  ;; Open xor's are treated as defaults.

  ;; Process all class-xors first.********** these are all there are right now.
  ;; Assuming these are class-xors*******
  (comment ****** now obsolete I think although much more work is required.
  (dolist (xor *xors*)
    (setq active-count 0 unconstrained-count 0 count 0)
    (when (cddr xor)
      (dolist (a (cdr xor))
	(incf count)
	(unless (dependent-assumption? a) (incf unconstrained-count))
	(if (memq a actives) (incf active-count)))
      (print-xor xor)
      (if *interp-trace* (format T "~% Count = ~D, unconstrained = ~D, actives = ~D"
				 count unconstrained-count active-count))
      (cond ((and (= count unconstrained-count) (= active-count 0))
	     (push xor unconstrained-and-useless-xors))
	    ((= count unconstrained-count) (push xor unconstrained-xors))
;	    ((or (> unconstrained-count 0) (< active-count count))
;	     (print-xor xor)
;	     (break "unimplemented"))
	    (t (push (cons (- count unconstrained-count) (cdr xor)) xors)))))
  (when unconstrained-and-useless-xors
    (if *interp-trace*
	(format T "~% The following oneof disjunctions are unconstrained and uninteresting"))
    (mapc 'print-xor unconstrained-and-useless-xors))
  (when unconstrained-xors
    (if *interp-trace*
	(format T "~% The following oneof disjunctions are unconstrained but interesting"))
    (mapc 'print-xor unconstrained-xors))
  ;;***************** postprocess to add them?
  (setq xors (sort xors #'(lambda (x y) (< (car x) (car y)))))
  (dolist (xor xors)
    (if *interp-trace* (format T "~%~D interpretations" (length l)))
    (setq nl nil nuniversal nil)
    (dolist (a (cdr xor))
      (cond ((dependent-assumption? a)
	     (dolist (e l)
	       (setq ne (cons-env e a))
	       (unless (env-contradictory ne) (push ne nl))))
	    ((null nuniversal)
	     (setq nuniversal T)
	     (setq nl (append l nl)))))
    (setq l nl)
    (if (null l) (return)))
  ;;**************** nuniversals need to be stuck in in some way.*******
  (if *interp-trace*
      (format T "~% There are ~D possible interpretations after xors." (length l))))
  ;; Walk through the regular or's (unimplemented here).
  ;; Install back in some day soon.******** This works actually, I just didn't hack
  ;; it for generic-envs.  Also what are *ors* --- they should not contain the
  ;; variable discjunctions?

  (comment
  ;; Note that if *h4* were 1, and *h45* were T.  This should eliminate no interpretations.
    (do ((l l (cdr l)))
	((null l))
    (dotimes (count 99.)
      (when (dolist (or (aref *ors* count))
	      ;; I presume or-vector is properly updated.
	      (unless (vector-intersection? (disjunction-vector or) (env-vector (car l)))
		(describe or)
		(print-solution (car l))
		(if *interp-trace* (format T "~% Disjunction eliminates ~A" (car l)))
		(return T)))
	(rplaca l nil)
	(return))))
  (setq l (fdelqa nil l)))
  ;; Do the defaults.  At this point a default is any assumption, not appearing
  ;; in any variable, although that is too general.
  (setq l (extend-via-defaults l))
  ;; Walk through the defaults.
  ;; use ***** active/passive assumption trick!!!!!!! relative.
; Deleted 12:07 for KDF's example, put back when this is grocked.
;  (when l (setq l (interp-search l actives dont-minimize universal)))
  (format T "~% Interpretation construction time is:~D seconds"
	  (time-taken start-time))
  l)

(defvar *i-mode* :NEW-DEPTH3)			; Mode of finding variable interpretations.

;;; Warning this contains some dead code.
;;; Note that this code assumes that true or false assumptions will have already flushed
;;; the variable.  So this check does not have to be done during cons-env.
(defun variable-interpretations (&aux or variables)
  (dolist (s *assumption-symbols*)
    (cond ((true? (psymbol-pnode s)))
	  ((false? (psymbol-nnode s)))
	  (t (push (psymbol-or s) variables))))
  (dolist (var *variables*)
    (unless (class-closed var) (error "Malformed variable class"))
    (setq or (class-or var))
    (cond ((null or)
	   (format T "~% ~A has no disjunction." var))
	  ((disjunction-satisfied or) (format T "~% ~A has been satisfied." var))
	  (t (push or variables)
	     (format T "~% ~A of size ~D queued for interpretation construction."
		     var (disjunction-count (class-or var))))))
  ;; Induce missing variables from ors.
  (dotimes (i 99) ;;; *max-or-count*
    (dolist (or (aref *ors* i))
      (cond ((memq or variables))
	    ;; Assume we win.  A kludge!!*!*!*!*!!*! FIx.
	    ;; Our code won't work if assumption appears in two different disjunctions.
	    ;; Its over strong if not all pair-wise nogoods exist.  What if a->b and a or b.
	    (t (print or)
	       ;; If every variable in a disjunction is the negation of another, and this
	       ;; is not a negation disjunction, throw it away.***** Assumption-negation
	       ;; is overloaded here.
	       (cond ((or (assq 'NEGATE-ASSUMPTION (disjunction-informants or))
			  (dolist (a (disjunction-disjuncts or))
			    (or (assumption-negation a) (return T))))
		      (push or variables))
		     (T ;; **** This should only be installed once per disjunction, and
                        ;; then the disjunciton should be flushed.
		        (let ((nvars nil))
			  (dolist (a (disjunction-disjuncts or))
			    (push (assumption-negation a) nvars))
			  (contradiction (cons '(VARIABLE-INTERPRETATIONS) nvars)))
			
			(format T "~% Redundant disjunction")))))))

  ;; ***** insert the following xor optimizer we had before.
  ;; ***** instead of this crock.
  ;;******* does or-count really have number of remaining?
  (setq variables (sort variables #'(lambda (or1 or2) (< (disjunction-count or1) (disjunction-count or2)))))
  (selectq *i-mode*
    (:SIMPLE (simple-interpretations variables))
    (:BREADTH (variable-interpretations-breadth variables))
    (:DEPTH (variable-interpretations-depth variables))
    (:NEW-DEPTH3 (variable-interpretations-depth-stack variables))
    (:NEW-DEPTH2 (variable-interpretations-depth2 variables))
    (:NEW-DEPTH (forward-checking variables))))

;;; A depth-first version that doesn't cons at all.
(defvar *interpretations* nil)

;;; Arrays may simply be faster here!?*****
(defun forward-checking (variables &aux *interpretations* assumption-sets smallest next)
  (cond ((null variables) *empty-env-list*)
	(t (dolist (variable variables)
	     (setq next (cons (disjunction-count variable) (disjunction-disjuncts variable)))
	     (cond ((null smallest) (setq smallest next))
		   ((< (disjunction-count variable) (car smallest)) (push smallest assumption-sets) (setq smallest next))
		   (t (push next assumption-sets))))
	   ;; First iteration could be open-coded!?!?**
	   (dolist (a (cdr smallest))
	     (forward-checking-recurse *empty-env* a assumption-sets)))))

;;;******* its pretty clear its worth pruining all the subsumed nogoods off of assumption-nogoods.
(defun forward-checking-recurse (env assumption variables &aux smallest vector update-variable nenv)
  (cond ((null variables)
	 ;;******* Call a cons-env which we know doesn't have to do a consistency check as it is guaranteed to be.
	 (push (fast-cons-env env assumption nil) *interpretations*))
	(t ;;;******** again ths fast-cons-env need to no consistency checking!?!?!?!?*****
	   ;;;******** this does a useless backward check.
	   (setq nenv (fast-cons-env env assumption T))
	   (if (env-contradictory nenv) (error "Uh"))
	   ;; First we will update the vector of assumptions it is inconsistent with.  This could probably be
           ;; done in other parts of the ATMS as well.
	   ;; ALso note that the cache needs to be updated for this to work properly.
	   ;; ****** I haven't implemented this here because for my experiment, n-queens only has binary nogoods.
	   
	   ;; Go through all the remaining assumption sets and see if anybody gets removed.
	   ;;***** A reusable array would be more efficient here???
	   (setq variables (copy-tree variables)
		 vector (if (simple-envp nenv)
			    (simple-env-cons-env-cache nenv)
			    (car (env-cons-env-cache nenv))))
	   (dolist (variable variables)
	     (do ((assumptions (cdr variable) (cdr assumptions)))
		 ((null assumptions))
	       (when (vector-member (car assumptions) vector)
		 (setq update-variable T)
		 (rplaca assumptions nil)
		 (decf (car variable))))
	     ;;***** could do an intelligent backtrack here!?!?!!?!?!
	     (if (= (car variable) 0) (return))
	     (when update-variable
	       (rplacd variable (fdelqa nil (cdr variable)))
	       (setq update-variable nil))
	     (cond ((= (car variable) 1) (setq smallest variable))
		   ((null smallest) (setq smallest variable))
		   ((< (car variable) (car smallest)) (setq smallest variable))))
	   ;;******* We could do a prog here --- it would be faster.
	   ;;******* arrays, or more efficient about this consing.
	   (setq variables (fdelq1 smallest variables))
	   (dolist (a (cdr smallest))
	     (forward-checking-recurse nenv a variables))
	   )))
	   
(defvar *backtracks*)				; Number of useless descents.

(defvar *graph-deletions* 0)			; How many times constraint graph is updated.

;;; Note that many optimizations were put in the -stack version which aren't installed
;;; here.  So if this version is conceptually better, move the hacks.
;;; As so much computation is spent here, this looks ahead a lot.
;;;******* this is the only version of interpretation construction which counts backtracks.
(defun variable-interpretations-depth (variables &aux *interpretations* *backtracks*)
  (setq *backtracks* 0)
  (cond ((null variables) *empty-env-list*)
	(t (dolist (a (disjunction-disjuncts (car variables)))
	     (variable-interpretations-1 (assumption-env a) (cdr variables)))
	   (if *interp-trace*
	       (format T "~% Required ~D backtracks, ~D graph deletions"
		       *backtracks* *graph-deletions*))
	   *interpretations*)))

(defun variable-interpretations-1 (env variables &aux ne vector cache start)
  (setq start *interpretations*)
  (cond ((null variables) (push env *interpretations*))
	((simple-envp env)
	 (setq vector (simple-env-vector env)
	       cache (simple-env-cons-env-cache env))
	 (dolist (a (disjunction-disjuncts (car variables)))
	   (cond ((vector-member a cache))
		 ((vector-intersection? (assumption-binary-vector a) vector))
		 (t ;******* a crock.  The above tests will just be made again.
		  ;******* we could have a version of fast-cons-env which assumed total cache miss.
		  ;	(setq ne (cons-env env a))
		  (setq ne (fast-cons-vector2 env a (cdr variables) vector cache))
		  (or (null ne)
		      (and (not (simple-envp ne)) (env-contradictory ne))
		      (variable-interpretations-1 ne (cdr variables)))))))
	(t (setq vector (env-vector env)
		 cache (env-cons-env-cache env))
 	   (dolist (a (disjunction-disjuncts (car variables)))
	     (cond ((vector-member a (car cache)))
		   ((and (cdr cache) (setq ne (gethash a (cdr cache))))
		    (unless (env-contradictory ne)
		      (variable-interpretations-1 ne (cdr variables))))
		   ((vector-intersection? (assumption-binary-vector a) vector))
		   (t (setq ne (if (cdr variables)
				   (fast-cons-env2 env a vector cache)
				   (cons-env env a)))	; Rare event.
		      (or (null ne)
			  (and (not (simple-envp ne)) (env-contradictory ne))
			  (variable-interpretations-1 ne (cdr variables))))))))
  ;; Count number of times we never achieved anything.  This shouldn't happen
  ;; if we didn't have the complete graph.
  (if (eq start *interpretations*) (incf *backtracks*))
  )

;;; Used for gathering statistics, not for efficiency.
(defun simple-interpretations (variables &aux *backtracks* *interpretations*)
  (setq *backtracks* 0)
  (bt *empty-env* variables)
  (format T "~% Number of backtracks: ~D, Number of solutions: ~D"
	  *backtracks* (length *interpretations*))
  *interpretations*
  )

(defun bt (env variables &aux new-env flag)
  (if (null variables)
      (push env *interpretations*)
      (dolist (a (disjunction-disjuncts (car variables))
		 (unless flag
		   (incf *backtracks*)))
	(when (setq new-env (generic-cons-env env a))
	  (setq flag T)
	  (bt new-env (cdr variables))))))


(defun variable-interpretations-depth-stack (variables &aux alternatives)
  (dolist (v variables)
    (push (cons (disjunction-count v) (disjunction-disjuncts v)) alternatives))
  (variable-interpretations-depth-stack-2 *empty-env* alternatives))

;;; This assumes strong-focussing.  Is very simple minded just to experiment.
;;; This should be like candgenk probably and combined with variable-interpreations-depth-stack
;;; -2.
(defun variable-interpretations-depth-stack-sets-focus (seed-env choice-sets
							&aux alternatives choice-set
							interpretations start-time)
  (setq start-time (get-internal-run-time))
  (dolist (v choice-sets)
    (setq choice-set nil)
    (dolist (a v)
      (cond ((assumption-contradictory a))
	    ((eq *empty-env* (car (assumption-envs a)))
	     ;;*** I suspect that this can be done better.
	     (setq choice-set (list a))
	     (return nil))
	    (t (push a choice-set))))
    (push (cons (length choice-set) choice-set) alternatives))

  (setq alternatives (sort alternatives #'(lambda (a b) (< (car a) (car b)))))

  ;; Depth-first is the only thing that makes sense here.
  (setq interpretations (interpretations-focus seed-env alternatives))

  (if *interp-trace*
      (format T "~% ~D interpretations." (length interpretations)))

  (format T "~% Focus interpretation construction time is:~D seconds" (time-taken start-time))
;  (when *trace-file* (trace-v-i-d-s-s seed-env choice-sets interpretations))

;  (time (variable-interpretations-depth-stack-sets seed-env choice-sets))
  interpretations)

;;; This could pick the shortest first and not create environments.  But this is being
;;; used solely for functionality experiments for now.  Change-foci is bad, use
;;; add and retract assumption or DDB.

;;; Returns [envs , killer]
(defun interpretations-focus (env alternatives &aux interpretations new-env result killer)
  (cond ((null alternatives)
	 (setq env (simple-to-env env))
	 (change-foci (list env))
	 (run)
	 (cond ((env-contradictory env) (values nil (find-base-contradiction env)))
	       (t (cons env nil))))
	(t (dolist (a (cdar alternatives))
	     (unless (n-a-contradictory a)
;	       (if (generic-check-env? env) (error "Can't happen"))
	       (ensure-instantiated a)
	       (setq new-env (fast-cons-env env a t))
	       (unless (generic-env-contradictory new-env)
		 (multiple-value-setq (result killer)
		   (interpretations-focus new-env (cdr alternatives)))
		 (cond (result
			(setq interpretations (nconc result interpretations)))
		       ;; If there are no interpretations, the current env may
		       ;; have become inconsistent.
		       ;; If current assumption, wasn't the killer, env is inconsistent.
		       ((eq killer :CONSISTENT))
		       ((null killer)
			;;; ***** THIS NEVER HAPPENS ANYMORE.
;			(incf foo)
			(cond ((null (simple-envp env))
			       (return-from interpretations-focus
				 (values nil (find-base-contradiction env))))
			      ((setq killer (generic-check-env? env))
			       (return-from interpretations-focus (values nil killer)))))
		       ((if (listp killer)
			    (not (memq a killer))
			    (not (vector-member a (env-vector killer))))
			;; This means that env is inconsistent without further ado.
			(return-from interpretations-focus (values nil killer)))
		       ;; Of course, env may be inconsistent due to some other contradiction.
		       ((setq killer (generic-check-env-why? env))
			(return-from interpretations-focus (values nil killer)))
		       (t ;(incf bar)
			)
		       ))))
	   (values interpretations :CONSISTENT))))

;;; This version does not do consistency checking at every level.
(defun interpretations-focus (env alternatives &aux interpretations new-env result killer)
  (cond (alternatives
	 (dolist (a (cdar alternatives))
	   (unless (n-a-contradictory a)
	     (ensure-instantiated a)
	     (setq new-env (fast-cons-simple env a))
	     (multiple-value-setq (result killer)
	       (interpretations-focus new-env (cdr alternatives)))
	     (cond (result
		    (setq interpretations (nconc result interpretations)))
		   ;; If there are no interpretations, the current env may
		   ;; have become inconsistent.
		   ;; If current assumption, wasn't the killer, env is inconsistent.
		   ((eq killer :CONSISTENT))
		   ((null killer)
		    ;;; ***** THIS NEVER HAPPENS ANYMORE.
		    ;(incf foo)
		    (cond ((null (simple-envp env))
			   (return-from interpretations-focus
			     (values nil (find-base-contradiction env))))
			  ((setq killer (generic-check-env-why? env))
			   (return-from interpretations-focus (values nil killer)))))
		   ((if (listp killer)
			(not (memq a killer))
			(not (vector-member a (env-vector killer))))
		    ;; This means that env is inconsistent without further ado.
		    (return-from interpretations-focus (values nil killer)))
		   ;; Of course, env may be inconsistent due to some other contradiction.
		   ((progn ;(incf bar)
		      (generic-check-env-why? env))
		    ;;******* Return the killer in this case.
		    (return-from interpretations-focus nil))))))
	((setq killer (generic-check-env-why? env))
	 (if (eq killer T) (error "can't"))
	 (return-from interpretations-focus (values nil killer)))
	(t (setq env (simple-to-env env))
	   (change-foci (list env))
	   (run)
	   (cond ((env-contradictory env) (values nil (find-base-contradiction env)))
		 (t (cons env nil)))))
  (values interpretations :CONSISTENT))


;;; This probably makes the presupposition that the choice-sets all are of the same class.
;;; Related: the same choice better appear in only one choice-set
;;; ***** Make a better top-level function later.
;;;******* -focus is temporary.
(defun variable-interpretations-depth-stack-sets (seed-env choice-sets
							   &aux alternatives choice-set
							   interpretations)
  (dolist (v choice-sets)
    (setq choice-set nil)
    (dolist (a v)
      (cond ((assumption-contradictory a))
	    ((eq *empty-env* (car (assumption-envs a)))
	     ;;*** I suspect that this can be done better.
	     (setq choice-set (list a))
	     (return nil))
	    (t (push a choice-set))))
    (push (cons (length choice-set) choice-set) alternatives))
  (setq interpretations (variable-interpretations-depth-stack-2 seed-env alternatives))
  (if *interp-trace*
      (format T "~% ~D interpretations." (length interpretations)))
  (convert-interpretations interpretations)
  (when *trace-file* (trace-v-i-d-s-s seed-env choice-sets interpretations))
  interpretations)

;(defun variable-interpretations-depth-stack-sets-focus (seed-env choice-sets
;							   &aux alternatives choice-set
;							   interpretations)
;  ;; Repeat until no new nogoods are encountered.
;  (do nil
;      ((null (catch 'NEW-NOGOOD
;	       (dolist (v choice-sets)
;		 (setq choice-set nil)
;		 (dolist (a v)
;		   (cond ((assumption-contradictory a))
;			 ((eq *empty-env* (car (assumption-envs a)))
;			  ;;*** I suspect that this can be done better.
;			  (setq choice-set (list a))
;			  (return nil))
;			 (t (push a choice-set))))
;		 (push (cons (length choice-set) choice-set) alternatives))
;	       (setq interpretations
;		     (variable-interpretations-depth-stack-2 seed-env alternatives))
;	       (if *interp-trace*
;		   (format T "~% ~D interpretations." (length interpretations)))
;	       nil))))
;;  (convert-interpretations interpretations)
;;  (when *trace-file* (trace-v-i-d-s-s seed-env choice-sets interpretations))
;  interpretations)

(defun trace-v-i-d-s-s (seed-env choice-sets interpretations)    
  (dolist (e interpretations) (trace-env e))
;;; Don't, because this is skipped in check mode.
;;;  (trace-env seed-env) 
  (format *trace-file* "~% V-I-D-S-S2 (" (env-unique seed-env))
  (dolist (a (env-assumptions seed-env))
    (format *trace-file* " ~D" (assumption-unique a)))
  (format *trace-file* ") (")
  (mapc #'(lambda (choice-set)
	    (format *trace-file* "(")
	    (dolist (a choice-set) (format *trace-file* " ~D" (assumption-unique a)))
	    (format *trace-file* ")"))
	choice-sets)
  (format *trace-file* ")")
  ;; Put the answer in the file as well.
  (format *trace-file* "(")
  (let ((previous nil))
    (dolist (e interpretations)
      (zf previous
	  (format *trace-file* " ~D" (env-unique e))
	  (setq previous T)
	  (format *trace-file* " ~D" (env-unique e)))))
  (format *trace-file* ")")
  )

(defun convert-interpretations (interpretations)
  (mapl #'(lambda (interpretations &aux generic)
	    (setq generic (simple-to-env (car interpretations)))
	    (if (env-contradictory generic)
		(error "Generic env ~A was nogood ~A" (car interpretations) generic))
	    (rplaca interpretations generic)
	    )
	interpretations))

;;; This returns generic environments as of version 9
;;; If seed-env = *empty-env* we should do something smarter.
(defun variable-interpretations-depth-stack-2 (seed-env alternatives &aux
					       *interpretations* *backtracks* env-stack
					       nogoods 
					       alternative-stack alternative-entry
					       max-alternative (alternative-count 0))
  (setq *backtracks* 0 *graph-deletions* 0)
  (multiple-value-setq (alternatives seed-env nogoods)
    (setup-interp-construction alternatives seed-env))
  (if (eq seed-env *empty-env*) (format T "~% This case needs to be optimized."))
  (cond ((null alternatives) (push seed-env *interpretations*))
	((eq alternatives 'REFUTATION))
	(t
	 (dotimes (i (length alternatives))
	   (declare (ignore i))
	   (push (make-simple-env nil nil nil nil) env-stack))
	 (dolist (a alternatives)
	   (cond ((null max-alternative) (setq max-alternative (car a)))
		 ((> (car a) max-alternative) (setq max-alternative (car a))))
	   (incf alternative-count))
	 ;; This can be done with a lot less conses...but I'm lazy
	 (incf max-alternative)
	 (dotimes (i alternative-count)
	   (declare (ignore i))
	   (setq alternative-entry nil)
	   (dotimes (i alternative-count)
	     (declare (ignore i))
	     (push (make-list max-alternative) alternative-entry))
	   (push (cons 'A 'B) alternative-entry)
	   (push (cons 'C 'D) alternative-entry)
	   (push alternative-entry alternative-stack))
	 (variable-interpretations-1-stack
	   alternative-stack env-stack nogoods
	   seed-env alternatives)))
  (if *interp-trace*
      (format T "~% Required ~D backtracks, ~D graph deletions"
	      *backtracks* *graph-deletions*))
  *interpretations*)

;;; This cleans up the data structures for interpretation construction.  Sometimes
;;; this completes interpretation construction.  Some experimentatin is needed
;;; to determine whether this all is worth it.  I suspect on average, no time
;;; will be spent here.

;;; Need a test-cons-env? function.

(defun setup-interp-construction (alternatives seed-env &aux all-assumptions)
  (loop 
   (unless alternatives (return-from SETUP-INTERP-CONSTRUCTION (values nil seed-env)))
   (update-env-cache-vector seed-env)
   (multiple-value-setq (alternatives seed-env) (setup-alternatives alternatives seed-env))
   (if (eq alternatives 'REFUTATION) (return-from SETUP-INTERP-CONSTRUCTION 'REFUTATION))
   (if (null alternatives) (return-from SETUP-INTERP-CONSTRUCTION (values nil seed-env)))
   (cond ((= 1 (caar alternatives))
	  (setq seed-env (cons-env seed-env (cadar alternatives))
		alternatives (cdr alternatives)))
	 (t (setq all-assumptions (env-assumptions seed-env))
	    (dolist (alternative alternatives)
	      (setq all-assumptions (append (cdr alternative) all-assumptions)))
	    (return-from SETUP-INTERP-CONSTRUCTION
	      (values alternatives
		      seed-env
		      (nogoods-of-env seed-env (make-env-vector* all-assumptions))))))))

;;;**** tail recursive, can be done in a loop, but the loop above does this too???
;;; But doing the test here seems to help by a factor of 2.
(defun setup-alternatives (alternatives env &aux shortest new-alternative new-alternatives)
  (dolist (set alternatives)
    (setq new-alternative nil)
    (dolist (pa (cdr set))
      (unless (contradictory-cons-env? env pa)
	(push pa new-alternative)))
    (unless new-alternative (return-from SETUP-ALTERNATIVES 'REFUTATION))
    ;; If we luck out and get a singleton:
    (when (null (cdr new-alternative))
      (setq env (cons-env env (car new-alternative)))
      (if (env-contradictory env) (return-from SETUP-ALTERNATIVES 'REFUTATION))
      (if shortest (push shortest new-alternatives))
      (return-from SETUP-ALTERNATIVES
	(setup-alternatives
	  (append (cdr (memq set alternatives)) new-alternatives) env)))
    (push (length new-alternative) new-alternative)
    (cond ((null shortest) (setq shortest new-alternative))
	  ((< (car new-alternative) (car shortest))
	   (push shortest new-alternatives)
	   (setq shortest new-alternative))
	  (t (push new-alternative new-alternatives))))
  (values (if shortest (cons shortest new-alternatives)) env))

;;; This returns all the minimal nogoods which may be considered in this search.
;;; ***** This is a hack right now and needs a lot more data structure hacking sometime.
;;; Note that as this consults the cons-env-cache vector; that any assumptions
;;; appearing in that had better be flushed.
(defun nogoods-of-env (start-env max-vector &aux nogoods vector)
  (update-env-cache-vector start-env)
  (setq vector (car (env-cons-env-cache start-env)))
  (walk-contradictions 
    #'(lambda (contradiction)
	#+Symbolics
	(declare (sys:downward-function))
	(unless (or (vector-intersection? vector (env-vector contradiction))
		    (not (vector-subset (env-vector contradiction) max-vector)))
	  (push contradiction nogoods)))
    2)
  nogoods)

;;; This returns generic environments as of version 9
(defun variable-interpretations-depth-stack-1 (alternatives &aux
					     *interpretations* *backtracks* env-stack nogoods
					     new-alternatives alternative
					     alternative-stack alternative-entry
					     max-alternative alternative-count)
  (setq *backtracks* 0 *graph-deletions* 0)
  (cond ((null alternatives) *empty-env-list*)
	(t (multiple-value-setq (alternatives alternative)
	     (pick-shortest-alternative alternatives))
	   (dotimes (i (length alternatives))
	     (declare (ignore i))
	     (push (make-simple-env nil nil nil nil) env-stack))
	   (dolist (a (cdr alternative))
	     (setq nogoods nil)
	     ;;***** these may be in the disjunction data structure actually.
	     (dolist (nogood (assumption-nogoods a))
	       (unless (subsumed-nogood? nogood) (push nogood nogoods)))
	     (setq new-alternatives
		   (revise-alternatives alternatives (assumption-env a) a nogoods))
	     (unless (eq new-alternatives 'REFUTATION) 
	       (cond ((null new-alternatives) (push (assumption-env a) *interpretations*))
		     (t (setq alternative-count 0)
			(dolist (a new-alternatives)
			  (cond ((null max-alternative) (setq max-alternative (car a)))
				((> (car a) max-alternative) (setq max-alternative (car a))))
			  (incf alternative-count))
			;; This can be done with a lot less conses...but I'm lazy
			(incf max-alternative)
			(dotimes (i alternative-count)
			  (declare (ignore i))
			  (setq alternative-entry nil)
			  (dotimes (i alternative-count)
			    (declare (ignore i))
			    (push (make-list max-alternative) alternative-entry))
			  (push (cons 'A 'B) alternative-entry)
			  (push (cons 'C 'D) alternative-entry)
			  (push alternative-entry alternative-stack))
			(variable-interpretations-1-stack
			  alternative-stack env-stack nogoods
			  (assumption-env a) new-alternatives)))))
	   (if *interp-trace*
	       (format T "~% Required ~D backtracks, ~D graph deletions"
		       *backtracks* *graph-deletions*))
	   *interpretations*)))

(defvar *smashing-alternatives* T)		; A bit slower, but conses less.

;;; This constructs a new alternative set.  Makes sure the *first* alternative is the
;;; shortest one.
;;;****** This can be made more efficient.
;;; ********* the contradictory-cons can be far more stringent I think.
;;; This more or less assumes it is being called exactly once right now at
;;; the beginning with a real env; and efficiency is not an issue.
(defun revise-alternatives (alternatives env assumption-just-added nogoods
			    &aux shortest new-alternative new-alternatives)
  (unless alternatives (return-from REVISE-ALTERNATIVES nil))
  (incf *graph-deletions*)
  (dolist (set alternatives)
    (setq new-alternative nil)
    (dolist (pa (cdr set))
      (unless (or (if assumption-just-added
		      (vector-member pa (assumption-binary-vector assumption-just-added))
		      (or (vector-intersection? (assumption-binary-vector pa)
						(env-vector env))
			  (vector-member pa (generic-env-cons-env-cache env))))
		  (and nogoods (contradictory-cons?-stack-new pa
							      nogoods
							      env)))
	(push pa new-alternative)))
    (unless new-alternative (return-from REVISE-ALTERNATIVES 'REFUTATION))
    (push (length new-alternative) new-alternative)
    (cond ((null shortest) (setq shortest new-alternative))
	  ((< (car new-alternative) (car shortest))
	   (push shortest new-alternatives)
	   (setq shortest new-alternative))
	  (t (push new-alternative new-alternatives))))
  (cons shortest new-alternatives))

;;; Alternatives looks like ((n ... END*... ) ... (SKIP ...) (END ...)...)
(defun revise-alternatives-stack (result alternatives env assumption-just-added nogoods
				  smash-p &aux shortest next-free-result count cons1 cons2)
  (incf *graph-deletions*)
  (unless *smashing-alternatives*
    (return-from REVISE-ALTERNATIVES-STACK
      (revise-alternatives alternatives env assumption-just-added nogoods)))
  (setq cons1 (car result) cons2 (cadr result) result (cddr result))
  ;; Destructively copy over alternatives if possible.
  (cond (smash-p (setq result alternatives))
	(t (do ((alternatives alternatives (cdr alternatives))
		(result result))
	       ((null alternatives) (if result (rplaca (car result) 'END)))
	     (cond ((eq (caar alternatives) 'END)
		    (if result (rplaca (car result) 'END))
		    (return nil))	
		   ((eq (caar alternatives) 'SKIP))
		   (t (rplaca (car result) (caar alternatives))	
		      (do ((alternatives (cdar alternatives) (cdr alternatives))
			   (result (cdar result) (cdr result)))
			  ((null alternatives) (if result (rplaca result 'END)))
			(rplaca result (car alternatives)))
		      (setq result (cdr result)))))))
  ;; Given the assumption-just-added, flush all future variables which are now satisfied.
  ;; ***** this can be made much more efficient because each assumption points to the
  ;; other disjunctions in which it appears. So at a minimum we need only do this for
  ;; assumptions which appear in more than one disjunction.  Also, if this is taking a lot
  ;; of time, one of the stack slots could be the original disjunction so the iterated
  ;; vector member is not needed.
  (dolist (set result)
    (if (eq (car set) 'END) (return))
    (unless (eq (car set) 'SKIP)
      (if (memq assumption-just-added (cdr set))
	  (rplaca set 'SKIP))))

  (dolist (set result)
    (if (eq (car set) 'END) (return))
    (unless (eq (car set) 'SKIP)
      (setq next-free-result (cdr set) count 0)
      (dolist (pa (cdr set))
	(if (eq pa 'END) (return))
	(unless (or (vector-member pa (assumption-binary-vector assumption-just-added))
		    (and nogoods (contradictory-cons?-stack-new pa
								nogoods
								env)))
	  (incf count)
	  (rplaca next-free-result pa)
	  (setq next-free-result (cdr next-free-result))))
      (if next-free-result (rplaca next-free-result 'END))
      (unless (> count 0) (return-from REVISE-ALTERNATIVES-STACK 'REFUTATION))
      (rplaca set count)
      (cond ((null shortest) (setq shortest set))
	    ((< count (car shortest)) (setq shortest set)))))
  ;; If there is no shortest, i.e., every disjunction is satisfied.  We return nil.
  (unless shortest (return-from REVISE-ALTERNATIVES-STACK 'DONE))
  ;;; To avoid rewriting other code... (cdr alternatives) will be NIL if there
  ;;; there are no other alternatives.  This can all be saved by a multiple value call.
  (rplaca cons1 (cond ((eq shortest (car result)) (setq result (cdr result)) shortest)
		      (t (rplaca cons2 (car shortest))
			 (rplacd cons2 (cdr shortest))
			 (rplaca shortest 'SKIP)
			 cons2)))
  (rplacd cons1 (do ((result result (cdr result)))
		    ((null result) nil)
		  (cond ((eq (caar result) 'END) (return nil))
			((eq (caar result) 'SKIP))
			(t (return result)))))
  cons1)

;;; Picks the shortest alternative destructively.  Some of this should be checked
;;; sooner.
(defun pick-shortest-alternative (alternatives &aux before-shortest-ptr shortest)
  (when alternatives
    (do ((alternatives alternatives (cdr alternatives))
	 (previous-alternatives nil alternatives))
	((null alternatives))
      (if (= (caar alternatives) 0)
	  (return-from PICK-SHORTEST-ALTERNATIVE (values nil (car alternatives))))
      (cond ((null shortest)
	     (setq shortest (car alternatives)))
	    ((< (caar alternatives) (car shortest))
	     (setq shortest (car alternatives) before-shortest-ptr previous-alternatives))))
    (if before-shortest-ptr
	(rplacd before-shortest-ptr (cddr before-shortest-ptr))
	(setq alternatives (cdr alternatives)))
    (values alternatives shortest)))

;;; Part of the contract is that the shortest alternative is guaranteed to be the first one.
;;; Notice also that in this representation, alternatives is always guaranteed to be
;;; consistent with current env.
;;; *********** if the shortest alternative is 1 long. we don't have to recurse!!!!.
;;; *********** but make sure to keep backtrack counter properly updated.
;;; Also the cleverness about backtracking is not done at the first iteration.

(defun variable-interpretations-1-stack (alternative-stack env-stack nogoods env alternatives
					 &aux ne vector cache start new-nogoods alternative
					 new-alternatives smash-p count)
  (setq alternative (car alternatives) alternatives (cdr alternatives))
  (setq start *interpretations*)
  (if (null alternative)
      (new-interpretation env)
      (prog nil
	 loop
       (cond ((simple-envp env)
	      (setq count (car alternative)
		    vector (simple-env-vector env))
	      (dolist (a (cdr alternative))
		(if (eq a 'END) (return))
		(decf count)
		(setq smash-p (= count 0))
		;; Note that could return
		(setq ne (fast-cons-vector2-stack-new (car env-stack) env a vector))
		(cond ((null ne))
		      ((and (not (simple-envp ne)) (env-contradictory ne)))
		      ;; If current alternative is a variable, we should return immediately.
		      ((null alternatives) (new-interpretation ne))
		      (t (setq new-nogoods (prune-nogoods nogoods a))
			 (setq new-alternatives (revise-alternatives-stack
						  (car alternative-stack)
						  alternatives ne a nogoods smash-p))
			 (cond ((eq new-alternatives 'DONE)
				(new-interpretation ne))
			       ((eq new-alternatives 'REFUTATION))
			       ;; Do the tail recursion by hand, but keep proper count.
			       (smash-p (unless (= (car alternative) 1)
					  (if (eq start *interpretations*) (incf *backtracks*))
					  (setq start *interpretations*))
					(setq env ne
					      env-stack (cdr env-stack)
					      nogoods new-nogoods
					      alternative (car new-alternatives)
					      alternatives (cdr new-alternatives))
					(go loop))
			       (t (variable-interpretations-1-stack
				    (cdr alternative-stack)
				    (cdr env-stack) new-nogoods ne new-alternatives)))))))

	     (t (setq vector (env-vector env) cache (env-cons-env-cache env))
		(dolist (a (cdr alternative))
		  (cond ((eq a 'END) (return))
			((and (cdr cache) (setq ne (gethash a (cdr cache))))
			 ;; *** can't be inconsistent I think.
			 (cond ((env-contradictory ne))
			       ((null alternatives) (new-interpretation ne))
			       (t 
				  ;;; If we just chose a value which is inconsistent with a nogood
				  ;;; element.  That nogood will never be restricting.
  				  (setq new-nogoods (prune-nogoods nogoods a)
					new-alternatives
					(revise-alternatives-stack
					  (car alternative-stack) alternatives ne a nogoods nil))
				  (cond ((eq new-alternatives 'DONE) (new-interpretation ne))
					((eq new-alternatives 'REFUTATION))
					(t (variable-interpretations-1-stack
					     (cdr alternative-stack) env-stack new-nogoods ne new-alternatives))))))
			(t (setq ne (fast-cons-env2-stack-new (car env-stack) env a vector))
			   (cond ((null ne))
				 ((and (not (simple-envp ne)) (env-contradictory ne)))
				 ((null alternatives) (new-interpretation ne))
				 (t ;; If we just chose a value which is inconsistent with a nogood
				  ;; element.  That nogood will never be restricting.
				  (setq new-nogoods (prune-nogoods nogoods a)
				        new-alternatives
					(revise-alternatives-stack
					  (car alternative-stack) alternatives ne a nogoods nil))
				  (cond ((eq new-alternatives 'DONE) (new-interpretation ne))
					((eq new-alternatives 'REFUTATION))
					(t (variable-interpretations-1-stack
					     (cdr alternative-stack) (cdr env-stack) new-nogoods ne new-alternatives))))))))))))
  ;; Count number of times we never achieved anything.  This shouldn't happen
  ;; if we didn't have the complete graph.
  (if (eq start *interpretations*)
      (incf *backtracks*))
  )

;;; This updates the nogood data base assigned to this branch of the search.  It removes
;;; all nogoods containing a an assumption inconsistent with the assumption just added.
;;; **** it might be better to organize nogoods by number of uncommitted assumptions, or
;;; assumptions not yet in the current context.  Then constradictory-cons need only check
;;; those nogoods with exactly one assumption not in the current context.
(defun prune-nogoods (nogoods new-assumption &aux new-nogoods)
  (dolist (nogood nogoods)
    (unless (vector-intersection? (env-vector nogood)
				  (assumption-binary-vector new-assumption))
      (push nogood new-nogoods)))
  new-nogoods)

(defvar *interp-focus* nil)

;;;**** Under contstruction.
(defun new-interpretation (env)
  (if (simple-envp env) (setq env (copy-tree env)))
  (when *interp-focus*
    (setq env (simple-to-env env))
    ;;***** Use a flag:
    (if (memq env *interpretations*) (return-from new-interpretation nil))
    (if (env-contradictory env) (error "Should not get here"))
    (change-foci (list env))
    (run)
    ;;; ******* Great optimizations are possible here:
    (if (env-contradictory env) (throw 'NEW-NOGOOD T)))
  (push env *interpretations*))


(defun variable-interpretations-breadth (variables &aux l nl icount dcount ne)
  (setq l *empty-env-list*)
  (dolist (or variables)
    (if *interp-trace* (format T "~%~D Interpretations" (length l)))
    (setq nl nil)
    (if *interp-trace* (format T "~% Processing ~A" (disjunction-disjuncts or)))
    (setq icount 0 dcount (length (disjunction-disjuncts or)))
    (dolist (a (disjunction-disjuncts or))
      (dolist (e l)
	(setq ne (cons-env e a))
	(unless (env-contradictory ne)
	  (incf icount)
	  (push ne nl)
	  (if (and *interp-trace* (= (rem icount 1000.) 0))
	      (format T "~% ~D interpretations so far, ~D disjuncts to go" icount dcount))
	  ))
      (decf dcount))

    (setq l nl)
    (when (null l)
      (if *interp-trace* (format T "~% All interpretations are inconsistent"))
      (return)))
  (if *interp-trace*
      (format T "~%~D After emptying queue there are ~D interpretations" (length l)))
  l)

;;; This needs fixing as defaults is uncleanly defined.  This is very inefficient.
;;; And needs radical speedup some time, but it at least should be right.
;;; Snarf the one from GDE.
;;; **** this does not work right for T/F I think.****
;;; Some defaults can be pruned universally early if we want to try that.
(defun extend-via-defaults (roots &aux ne)
  (when roots
    (dolist (default (find-defaults))
      (when *interp-trace*
	(format T "~% Processing assumption ~A, ~D interpretations so far."
		default (length roots)))
      (dolist (e roots)
	(unless (memq default (generic-env-assumptions e))
	  (if (setq ne (generic-cons-env e default))
	      (push ne roots))))))
  (unsimplify-generic-envs roots))
  

;;; Simple minded right now.  Needs thought sometime.
;;; For now, assumptions which are totally true are ignored.****
;;; Note assumption-ors is not enough to make an assumption a non-default: a pure choose
;;; is an inclusive disjunction.
(defun find-defaults (&aux assumptions)
  (dolist (a *assumptions* assumptions)
    (cond ((i-true? a))
	  ((i-false? a))
	  ((and (assumption-variable a)
		(class-closed (assumption-variable a))))
	  ;; If an assumption symbol, its not a default.
	  ((and (assumption-symbol a) (psymbol-or (assumption-symbol a))))
	  (t (push a assumptions)))))

;;; Somewhat dead code.***
;;; This first separates out which assumptions are defaults, and don't occur in
;;; any disjunctions, xors, etc.**** This is probably done inconsistently in
;;; earlier code.
(defun interp-search (roots actives dont-minimize universal &aux pruned-actives)
  dont-minimize universal
  (dolist (a actives)
    (when (or (memq (assumption-value a) '(:IN NIL))
	      (and (null (assumption-xors a))
		   (null (class-closed (assumption-variable a)))))
      (push a pruned-actives)))
  (mapcan #'(lambda (root) (interp-search-1 root pruned-actives)) roots))

;;; This eval-when is only needed for InterLisp, but it doesn't bother ZL so I
;;; added it for all. -- Jeff 7/8/86
(eval-when (compile load eval) (defvar *interps*))

(defun interp-search-1 (root assumptions &aux *interps*)
  (interp-search-scan root assumptions)
  *interps*)

;;; This iteratively adds assumptions
(defun interp-search-scan (env assumptions-to-go
			       &aux actives passives new-assumptions-to-go status)
  (unless (dolist (e *interps*) (if (subset-env? e env) (return T)))
    (dolist (a assumptions-to-go)
      (cond ((env-contradictory (cons-env env a)))
	    (t (push a new-assumptions-to-go))))
    (setq assumptions-to-go new-assumptions-to-go new-assumptions-to-go nil)
    (cond ((null assumptions-to-go) (found-interp env "No more assumptions to go"))
	  (t
	   ;; Separate out the assumptions which at this point can actually add information.
	   (dolist (a assumptions-to-go)
	     (setq status nil)
	     (dolist (c (assumption-consequents a))
 	           ;; A consequence which already holds is not new information
	           ;; and is useless to any further scanning in this direction.
	       (cond ((true-in? (car c) env))
		     ((not (i-in? (car c))))
		     ;; This works only for linear problems***i.e., one assumption/just.
		     ((true-in? (car c) (cons-env env a)) (setq status 'ACTIVE) (return))
		     (t (setq status 'PASSIVE))))
	     (if (eq status 'ACTIVE) (push a actives) (push a passives)))
	   (cond ((null actives) (found-interp env "No actives"))
		 (t ;; Try to preserve original ordering.
		    ;; This could be more efficient.  If two assumptions are
		    ;; order insensitive, then...
		    ;; This is a crock.
   		    (setq actives (nreverse actives) passives (nreverse passives))
		    (dolist (a actives)
		      (interp-search-scan (cons-env env a)
					  (nconc (delete a actives) passives)))))))))

(defun found-interp (env reason &aux new)
  reason
  (if *interps* (do () ((not (subset-env? env (car *interps*))))
		  (setq *interps* (cdr *interps*) new T)))
  (do ((interps *interps* (cdr interps)))
      ((null (cdr interps)))
    (if (subset-env? env (cadr interps)) (rplacd interps (cddr interps))
	(setq interps (cdr interps) new T)))
  (cond (new (push env *interps*) (format T "~% How can this happen?"))
	((dolist (e *interps*) (if (subset-env? e env) (return T)))
	 (format T "~% How can this happen"))
	(t (push env *interps*)))
  (if *interp-trace*
      (format T "~% There are now ~D interpretations." (length *interps*))))

(defun old-new-interpretations (&optional dont-minimize (start *empty-env*)
			&aux l start-time nl ne 
			actives universals universal xors 
			unconstrained-xors nuniversals
			unconstrained-and-useless-xors nuniversal ors or)
  (setq start-time (get-internal-run-time))
  (setq l (list start))
  (dolist (a *assumptions*)
    (if (eq (assumption-gc-status a) 'DONT) (setf (assumption-gc-status a) 'DO)))
  (setq actives (active-assumptions start))
  (dolist (a actives)
    (unless (dependent-assumption? a) (push a nuniversals)))
  (format T "~%Universals:")
  (dolist (u universals)
    (format T "~% True assumption: ~A" (string-assumption u)))
  ;; ******* The ATMS can figure out variables itself.  They are xors whose
  ;; assumptions occur in only one disjunct!!!!!!! That is much better than this crock.
  ;; *variables* is a list of one-of classes. node-assumption pairs (fix someday).
  ;; ******** make sure somewhere that satisfied disjuncts are marked in some way.
  (dolist (var *variables*)
    (setq or (class-or var))
    (cond ((null or))
	  ((disjunction-satisfied or))
	  (t (push or ors))))
  ;; ***** insert the following xor optimizer we had before.
  (setq ors (sort ors #'(lambda (or1 or2) (< (disjunction-count or1) (disjunction-count or2)))))
  (dolist (or ors)
    (format T "~%~D Interpretations" (length l))
    (setq nl nil nuniversal nil)
    (dolist (a (disjunction-disjuncts or))
      (dolist (e l)
	(setq ne (cons-env e a))
	(unless (env-contradictory ne) (push ne nl))))
    (setq l nl)
    (if (null l) (return)))
  ;; Process the rest of the disjunctive array, in order, but only those
  ;; not associated with a variable.
  ;; ******* xors interacts with actives ****** this feature is not used.
  ;; Walk through the XOR's, this is easy.
  ;; Open xor's are treated as defaults.

  ;; Process all class-xors first.********** these are all there are right now.
  ;; Assuming these are class-xors*******
  (comment ****** now obsolete I think although much more work is required.
  (dolist (xor *xors*)
    (setq active-count 0 unconstrained-count 0 count 0)
    (when (cddr xor)
      (dolist (a (cdr xor))
	(incf count)
	(unless (dependent-assumption? a) (incf unconstrained-count))
	(if (memq a actives) (incf active-count)))
      (print-xor xor)
      (format T "~% Count = ~D, unconstrained = ~D, actives = ~D"
	      count unconstrained-count active-count)
      (cond ((and (= count unconstrained-count) (= active-count 0))
	     (push xor unconstrained-and-useless-xors))
	    ((= count unconstrained-count) (push xor unconstrained-xors))
;	    ((or (> unconstrained-count 0) (< active-count count))
;	     (print-xor xor)
;	     (break "unimplemented"))
	    (t (push (cons (- count unconstrained-count) (cdr xor)) xors))))))
  (when unconstrained-and-useless-xors
    (format T "~% The following oneof disjunctions are unconstrained and uninteresting")
    (mapc 'print-xor unconstrained-and-useless-xors))
  (when unconstrained-xors
    (format T "~% The following oneof disjunctions are unconstrained but interesting")
    (mapc 'print-xor unconstrained-xors))
  ;;***************** postprocess to add them?
  (setq xors (sort xors #'(lambda (x y) (< (car x) (car y)))))
  (dolist (xor xors)
    (format T "~%~D interpretations" (length l))
    (setq nl nil nuniversal nil)
    (dolist (a (cdr xor))
      (cond ((dependent-assumption? a)
	     (dolist (e l)
	       (setq ne (cons-env e a))
	       (unless (env-contradictory ne) (push ne nl))))
	    ((null nuniversal)
	     (setq nuniversal T)
	     (setq nl (append l nl)))))
    (setq l nl)
    (if (null l) (return)))
  ;;**************** nuniversals need to be stuck in in some way.*******
  (format T "~% There are ~D possible interpretations after xors." (length l))
  ;; Walk through the regular or's (unimplemented here).
  ;; Walk through the defaults.
  ;; use ***** active/passive assumption trick!!!!!!! relative.
  (when l
    (dolist (a actives)
      (when (or (memq (assumption-value a) '(:IN NIL))
		(and (null (assumption-xors a))
		     (null (class-closed (assumption-variable a)))))
	(format T "~% Processing assumption ~A, ~D interpretations so far."
		a (length l))
	(dolist (e l)
	  (unless (memq a (env-assumptions e))
	    ;; **** not worth doing unless the consequent node of the assumption is
	    ;; in eventually.******* Tremendous speed up possible here.****
	    (unless (env-contradictory (setq ne (cons-env e a)))
	      (push ne l)))))))
  (format T "~% There are ~D possible interpretations after defaults." (length l))
  ;; Keep the maximal ones.
  ;;****** not necessarily to simplify if no defaults.**************
  (setq l (unsimplify-envs l))
  (format T "~% There are ~D possible interpretations after picking maximals." (length l))
  (setq nl nil universal (find-or-make-env universals))
  (dolist (e l) (push (union-env e universal) nl))
  (setq l nl)
  (format T "~% About to remove useless assumptions")
  (unless dont-minimize
    (setq l (remove-useless l))
    (format T "~% There are ~D possible interpretations after removing useless." (length l))
    ;; Keep the minimal ones.
    (setq l (unsimplify-envs l));;***** think, is this right????
    (format T "~% There are ~D possible interpretations after simplifying." (length l)))
  (format T "~% Interpretation construction time is:~D seconds"
	  (time-taken start-time))
  l)

;;; Assumption is independent if it appears in nogoods.
;;; ******** this is not right because we don't care about nogoods it participates
;;; ******** have an assumption which is truely false or truely true.***********
;;; ******* binary vector isn't updated.
(defun dependent-assumption? (a) (or (assumption-nogoods a) (assumption-binary-vector a)))

(defun print-xor (xor)
  (format T "~%(XOR")
  (dolist (a (cdr xor)) (format T " ~A " (string-assumption a)))
  (format T ")"))

;;; This is much closer to the right thing, but without all the tricks of envis.
;;; **** inclusive disjunction is not done right here bunkie, see notes of 2/22/85.
;;; *** missing preferences.
(defun old-interpretations (&optional dont-minimize
			&aux (l (list *empty-env*)) start-time nl ne result
			actives)
  (setq start-time (get-internal-run-time))
  (dolist (a *assumptions*)
    (if (eq (assumption-gc-status a) 'DONT) (setf (assumption-gc-status a) 'DO)))
  ;; ******* only want active wrt to l********
  (setq actives (active-assumptions *empty-env*)) ; Hacked by Jeff to match new args.
  ;; ******* xors interacts with actives ****** this feature is not used.
  ;; Walk through the XOR's, this is easy.
  ;; Open xor's are treated as defaults.
  (dolist (class *classes*)
    (format T "~% Processing class ~A, ~D interpretations so far."
	    (class-datum class) (length l))
    (when (and (class-assumptions class) (class-closed class))
      (setq nl nil)
      (dolist (a (class-assumptions class))
	(format T "~% Processing assumption ~A" (string-assumption a))
	(dolist (e l)
	  (setq ne (cons-env e a))
	  (unless (env-contradictory ne) (push ne nl))))
      (setq l nl)
      (if (null l) (return nil))))
  (format T "~% There are ~D possible interpretations after xors." (length l))
  ;; Walk through the regular or's (unimplemented here).
  ;; Walk through the defaults.
  ;; use ***** active/passive assumption trick!!!!!!!
  (when l
    (dolist (a actives)
      (when (or (memq (assumption-value a) '(:IN NIL))
		(and (null (assumption-xors a))
		     (null (class-closed (assumption-variable a)))))
	(dolist (e l)
	  (unless (memq a (env-assumptions e))
	    ;; **** not worth doing unless the consequent node of the assumption is
	    ;; in eventually.******* Tremendous speed up possible here.****
	    (unless (env-contradictory (setq ne (cons-env e a)))
	      (push ne l)))))))
  (format T "~% There are ~D possible interpretations after defaults." (length l))
  ;; Keep the maximal ones.
  (setq l (unsimplify-envs l))
  (format T "~% There are ~D possible interpretations after picking maximals." (length l))
  ;; Now flush useless assumptions.
  (unless dont-minimize
    (setq l (remove-useless l))
    (format T "~% There are ~D possible interpretations after removing useless." (length l))
    ;; Keep the minimal ones.
    (setq l (unsimplify-envs l));;***** think, is this right????
    (format T "~% There are ~D possible interpretations after simplifying." (length l)))
  (setq result (interp-group l))
  (format T "~% Interpretation construction time is:~D seconds"
	  (time-taken start-time))
  result)

;;; Group interpretations into indistinguishables.
(defun interp-group (l &aux result nl in out)
  (setq l (list l) result nil)
  (dolist (n *nodes*)
    (cond ((i-out? n))
	  (t (setq nl nil)
	     (dolist (set l)
	       (setq in nil out nil)
	       (dolist (e set)
		 ;; Save consing ****
		 (if (true-in? n e) (push e in) (push e out)))
	       (cond ((cdr in) (push in nl))
		     (in (push in result)))
	       (cond ((cdr out) (push out nl))
		     (out (push out result))))
	     (setq l nl)
	     (unless nl (return nil)))))
  (nconc result nl))

(defvar *envs*)					; To put result.
(defvar *processed*)				; Envs processed already.

(defun remove-useless (l &aux *processed* *envs*)
  (dolist (e l) (remove0 e))
  *envs*)

;;; If a superset is on env, we're already there.
(defun remove0 (e &aux flag)
  (cond ((memq e *processed*))
	(t (push e *processed*)
	   (dolist (a (env-assumptions e))
	     (if (remove1 e a) (setq flag T)))
	   (unless flag (push e *envs*)))))

;;; Assumption is removable if it has no consequents at all.
(defun remove1 (e a &aux r consequents)
 (dolist (c (assumption-consequents a))
   (setq r (cnsqnt-result c))
   (and (true-in? r e) (not (memq r consequents)) (push r consequents)))
 (cond ((dolist (r consequents)
	  (or
	    ;; T=unnecessary assumption.
	    (dolist (env (n-a-envs r))
	      (and (subset-env? env e)
		   (not (memq a (env-assumptions env)))
		   (return T)))
	    (return T)))
	nil)
       (t (remove0 (uncons-env e a)) T)))

;;; *** This code must exist everywhere, maybe its worth pulling it out.
(defun simplify-envs (l)
  (setq l (sort l #'(lambda (e1 e2) (< (env-count e1) (env-count e2)))))
  (do ((l l (cdr l)))
      ((null l))
    (do ((l2 (cdr l) (cdr l2)))
	((null l2))
      (and (car l) (car l2) (subset-env? (car l) (car l2)) (rplaca l2 nil))))
  (setq l (fdelqa nil l)))

(defun unsimplify-envs (l)
  (setq l (sort l #'(lambda (e1 e2) (> (env-count e1) (env-count e2)))))
  (do ((l l (cdr l)))
      ((null l))
    (do ((l2 (cdr l) (cdr l2)))
	((null l2))
      (and (car l) (car l2) (subset-env? (car l2) (car l)) (rplaca l2 nil))))
  (setq l (fdelqa nil l)))

(defun unsimplify-generic-envs (l)
  (setq l (sort l #'(lambda (e1 e2) (> (generic-env-count e1) (generic-env-count e2)))))
  (do ((l l (cdr l)))
      ((null l))
    (do ((l2 (cdr l) (cdr l2)))
	((null l2))				
      (and (car l) (car l2) (generic-subset-env? (car l2) (car l)) (rplaca l2 nil))))
  (setq l (fdelqa nil l)))


;;; A probably better interpretation constructor.  This one has a higher startup
;;; overhead though.  If there were bit-vector opcodes this would go faster too.

;;; Returns a list of minimal candidates.
;;; ****** maybe it should just return lists of assumptions???????????
(defun minimal-candidates (&aux candidates array start-time)
  (setq start-time (get-internal-run-time))
  (multiple-value-setq (candidates array) (base-interpretations1))
  (format T "~% ~D candidates found." (length candidates))
  (prog1
    (mapcar #'(lambda (candidate)
		(find-or-make-env-force (vector-assumptions candidate array)))
	    candidates)
    (format T "~% Interpretation construction time is:~D seconds"
	    (time-taken start-time))))

(defun interpretations1 (&aux candidates array start-time universal envs)
  (setq start-time (get-internal-run-time))
  (multiple-value-setq (candidates array universal) (base-interpretations1))
  (setq envs (mapcar #'(lambda (candidate)
			 (find-or-make-env-safe
			   (assumptions-union (env-assumptions universal)
					      (nvector-assumptions candidate array))))
		     candidates))
  (if *interp-trace* (print-envs envs))
  (setq envs (remove-useless envs))
  (format T "~% There are ~D possible interpretations after removing useless." (length envs))
  (setq envs (simplify-envs envs));;***** think, is this right????
  (prog1 (interp-group envs)
	 (format T "~% Interpretation construction time is:~D seconds"
		 (time-taken start-time))))

(defvar *minimal-candidates*)

(defvar *disjunctions*)

;;; If assumptions aren't active, ignore them completely.
(defun base-interpretations1 (&aux (contra-count 0) offset bit word (active-count 0)
			 start assumptions *minimal-candidates* assumption-array
			 contradictions actives universals universal disjunctions
			 *disjunctions*)
  (dolist (a *assumptions*)
    (if (eq (assumption-gc-status a) 'DONT) (setf (assumption-gc-status a) 'DO)))
  ;; ******* only want active wrt to l********
  ;; Actives are all assumptions which play some role.  Rest can be assumed to not exist.
  ;; **** what to do with inactive disjuncts?
  ;; inclusive dijunsction not right.
  ;; Used to be active assumptions here.
  (setq actives (fast-active-assumptions))
  (dolist (c *assumptions*) (setf (assumption-vector c) nil (assumption-index c) nil))
  ;; Every nogood which we care about gets assigned a bit.
  (walk-contradictions
    #'(lambda (nogood)
	(unless (dolist (assumption (env-assumptions nogood))
		  (unless (memq assumption actives) (return T)))
	(push (env-assumptions nogood) contradictions)
	(incf contra-count))))
  ;; Assume every disjunction is exclusive ********************
  ;; Assume every class is closed ***********
  (dolist (class *classes*)
    (when (class-assumptions class)
      (unless (dolist (assumption (class-assumptions class))
		(unless (memq assumption actives) (return T)))
      (push (class-assumptions class) contradictions)
      (push (class-assumptions class) disjunctions))))
  (setq bit 0 offset 0)
  (dolist (set contradictions)
    (dolist (assumption set)
      (unless (assumption-vector assumption)
	(setf (assumption-vector assumption)
	      (make-bit-vector (1+ (// contra-count #.*word-size*)))))
      (setq word (nthcdr offset (assumption-vector assumption)))
      (rplaca word (set-bit (car word) bit)))
    (incf bit)
    (if ( bit #.*word-size*) (setq bit 0 offset (1+ offset))))
  ;; **** don't forget xors.
  (if (= bit 0) (setq offset (1- offset) bit #.*word-size*))
  (setf start (make-bit-vector (1+ (// contra-count #.*word-size*))))
  (unless (= bit #.*word-size*)
    (setq word (nthcdr offset start))
    ;;*** more elegant way, look in manual.
    (do ((bit bit (1+ bit)))
	(( bit #.*word-size*))
      (rplaca word (set-bit (car word) bit))))
  (dolist (assumption *assumptions*)
    (when (assumption-vector assumption)
      (push assumption assumptions)
      (setf (assumption-index assumption) active-count)
      (incf active-count)))
  (setq assumption-array (make-array active-count))
  (dolist (assumption *assumptions*)
    (if (assumption-index assumption)
	(setf (aref assumption-array (assumption-index assumption)) assumption)))
  (dolist (active actives) (unless (assumption-index active) (push active universals)))
  (dolist (disjunction disjunctions)
    (push (make-d-vector disjunction) *disjunctions*))
  (setq universal (find-or-make-env universals))
  (format T "~% Universal: ~A" universal)
  (interpretations1-1 nil assumptions start)
  (setq *minimal-candidates* (vector-simplify *minimal-candidates*))
  (values *minimal-candidates* assumption-array universal))

(defun make-d-vector (assumptions &aux max new-max vector count bit offset word)
  (do ((assumptions assumptions (cdr assumptions)))
      ((null assumptions) (setq max (or max 0)))
    (cond ((null max) (setq max (assumption-index (car assumptions))))
	  ((> (setq new-max (assumption-index (car assumptions))) max)
	   (setq max new-max))))
  (if assumptions
      (setq vector (make-bit-vector (1+ (// (or max (assumption-index (car assumptions)))
					    #.*word-size*)))))
  (dolist (assumption assumptions)
    (setq count (assumption-index assumption))
    (multiple-value-setq (offset bit) (floor count #.*word-size*))
    (setq word (nthcdr offset vector))
    (rplaca word (set-bit (car word) bit)))
  vector)

;;; A brief explanation of how this all works.
;;; A generic algorithm is as follows.
;;; This is a breadth-first search, eliminating duplicates, are subsumed guys.
;;; This finds all collections of assumptions which explain all conflicts.
;;; It processes the list of assumptions one-by-one.

;;; This can be bummed in both conses and subset checks.  Talk to KVL.
(comment
(defun interpretations1-1 (candidate assumptions-todo vector &aux l nl nvector ncandidate (i 0))
  (setq l (list (list candidate assumptions-todo vector)))
  (do nil (nil)
    (format T "~% At level ~D there are ~D solutions" i (length l))
    (incf i)
    (dolist (todo l)
      (setq candidate (first todo) assumptions-todo (second todo) vector (third todo))
      (do ((assumptions-todo assumptions-todo (cdr assumptions-todo)))
	  ((null assumptions-todo))
	(setq ncandidate (vector-cons (assumption-index (car assumptions-todo)) candidate))
	(cond ((dolist (d *disjunctions*) (if (vector-subset d ncandidate) (return T))))
	      ((dolist (word (setq nvector
				   (vector-union vector
						 (assumption-vector (car assumptions-todo)))))
		 (if (not= (lognot word) 0) (return T)))
	       ;;******** should go both ways.  With or without the assumption.
	       ;;**** or does it.
	       (if (cdr assumptions-todo)
		   (push (list ncandidate (cdr assumptions-todo) nvector) nl)))
	      ((dolist (c *minimal-candidates*) (if (vector-subset c ncandidate) (return t))))
	      (t (push ncandidate *minimal-candidates*)))))
    (setq l nl nl nil)
    (unless l (return nil)))))

(comment

;;; Crufty depth-first version.  Nees a final vector-simplify***
(defun old-interpretations1-1 (candidate assumptions-todo vector)
  (cond ((dolist (d *disjunctions*) (if (vector-subset d candidate) (return T))))
	((not (dolist (word vector) (if (not= (lognot word) 0) (return T))))
	 (push candidate *minimal-candidates*))
	(t (do ((assumptions-todo assumptions-todo (cdr assumptions-todo)))
	       ((null assumptions-todo))
	     (interpretations1-1 (vector-cons (assumption-index (car assumptions-todo)) candidate)
				 (cdr assumptions-todo)
				 (vector-union vector (assumption-vector (car assumptions-todo)))))))))