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

(in-package 'tms)

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

;;; This runs on two many different types of machines that the #+/#- macros
;;; got completely screwed up.  To simplify matters, there are five possible modes
;;; only one of which should be on in the features.  Be warned that at any given
;;; time not all modes work.  I don't debug all possible options all of the time.

;;; **** at the moment the only options that work are :IL and :CL.

;;; #+IL     Running in Interlisp.
;;; #+ZL     Running in pure ZetaLisp release 6.1 or better on a 3600. (doesn't work now).
;;; #+CADR   Running on a CADR or a TI machine. (doesn't work now)
;;; #+CL     Running in pure Common Lisp. (works).
;;; #+CL-ZL  Running a "pure" Common Lisp on a ZetaLisp release 6.1 or better on a 3600.(?)

;;; If mode is unspecified at compile time, set it to :CL
(eval-when (compile load eval)
  (let ((compile-time #.(or (car (intersection '(:IL :ZL :CADR :CL :CL-ZL) *features*)) :CL))
	(load-time (or (car (intersection '(:IL :ZL :CADR :CL :CL-ZL) *features*)) :CL)))
    (if (eq compile-time load-time)
	(pushnew compile-time *features*)
	(error "This file (defs.lisp) was compiled in mode ~S but loaded in mode ~S."
	       compile-time load-time))))

;;;
;;; This gets called at the top of each file.
;;; In case of problem call JonL.
;;; 
(defmacro validate-mode ()
  (let ((compile-time (validate-mode-1)))
    `(eval-when (load)
       (unless (equal ',compile-time (validate-mode-1))
	 (error "When this file was compiled the mode was: ~S, it is now ~S."
		',compile-time (validate-mode-1))))))

(defun validate-mode-1 (&aux old-f)
  (dolist (f '(:IL :ZL :CADR :CL :CL-ZL) old-f)
    (cond ((null (member f *features*)))
	  (old-f (error "There cannot be two ATMS modes: ~A and ~A" old-f f))
	  (t (setq old-f f)))))


;;; This makes sure the file was compiled and loaded in the same mode.  Otherwise
;;; all sorts of bugs appear.

(shadow '(class find-class))

(export '(*assumption-counter* *classes* *contra-counter*
          *contra-node* *empty-env* *env-counter*
	  *max-contra-count* *node-counter* *node-string*
	  add-class-to-node assume-node assume-xor-node assumption-datum
	  assumption-unique assumption-value assumption-variable assumptions-union
	  careful-node? class-datum class-nodes close-variable-class compare-env
	  cons-env consistent-in? create-class create-consumer
	  create-implied-by-consumer create-in-implied-consumer create-node
	  defconsumer e env-assumptions env-contradictory
	  env-datum env-nodes
	  env-unique env-vector find-assumption-for find-or-make-env
	  find-variable-value get-assumption-prop get-env-prop in in? init-tms
	  justify-node make-a-assumption node-assumption node-classes
	  node-consequents node-datum node-envs node-justifications node-status
	  node? nodes out out? possible-status-of-node
	  put-assumption-prop put-env-prop run status-of-node string-env
	  subset-env? subset12 subset21 subsumed-envs?
	  true-in? union-env union-envss vector-subset vector-union))

;;; CommonLisp If doesn't necessarily handle multiple else forms.
#-Symbolics
(defmacro zf (condition true &rest false) `(cond (,condition ,true) (t . ,false)))

#+Symbolics
(defmacro zf (condition true &rest false) `(if ,condition ,true . ,false))

;;; A CommonLisp ONCE-ONLY courtesy of Gregor Kiczales
;;; ONCE-ONLY does the same thing as it does in zetalisp.  I should have just lifted
;;; it from there but I am honest.  Not only that but this one is written in Common
;;; Lisp.  I feel a lot like bootstrapping, or maybe more like rebuilding Rome.
;;; The eval-when is here as a consession to an Allegro CommonLisp bug.  It shouldn't
;;; be needed in a proper CommonLisp.
(eval-when (compile load eval)
(defmacro once-only (vars &body body)
  (let ((gensym-var (gensym))
        (run-time-vars (gensym))
        (run-time-vals (gensym))
        (expand-time-val-forms ()))
    (dolist (var vars)
      (push `(if (or (symbolp ,var)
                     (numberp ,var)
                     (and (listp ,var) (member (car ,var) '(quote function))))
                 ,var
                 (let ((,gensym-var (gensym)))
                   (push ,gensym-var ,run-time-vars)
                   (push ,var ,run-time-vals)
                   ,gensym-var))
            expand-time-val-forms))    
    `(let* (,run-time-vars
            ,run-time-vals
            (wrapped-body
              ((lambda ,vars . ,body) . ,(reverse expand-time-val-forms))))
       `((lambda ,(nreverse ,run-time-vars)  ,wrapped-body)
         . ,(nreverse ,run-time-vals))))))

(proclaim '(declaration values))

(defun extract-declarations (body)
  (declare (values documentation declares body))
  (let (documentation declares)
    (when (stringp (car body)) (setq documentation (pop body)))
    (do ((form (car body) (car body)))
        ((or (null body)
             (not (and (listp form) (eq (car form) 'declare))))
         (values documentation declares body))
      (push (pop body) declares))))

#+(and :CL (not :il))
(defmacro selectq (test-object &body clauses) `(case ,test-object ,@clauses))

;;; The *big* "KKKKKKKK"ludge for this unecessary hack for Xerox Common Luse's
;;; need to shadow InterLuse's SELECTQ.

#+:il
(defmacro cl:selectq (test-object &body clauses) `(case ,test-object ,@clauses))

#+:CL 
(defmacro // (x y) `(values (floor ,x ,y)))

(defmacro array-length (x)
  #+:CL `(length ,x)
  #+(OR :ZL :CADR :CL-ZL) `(array-length ,x)
  )

;;; Fix :CL-ZL someday and not have this explicit kludgery *** hard to debug cl this way.
#+(AND :CL (NOT :SYMBOLICS))
(defmacro assq (x y) `(assoc ,x ,y :test #'eq))

;;; The Symbolics compiler compiles the above into an order of magnitude slower than
;;; it should. A test of #'eql is at least faster.  This is fastest.
#+(AND :CL :SYMBOLICS (NOT :IMACH))
(defmacro assq (x y) `(zl:assq ,x ,y))

#+(AND :CL :IMACH)
(defmacro assq (x y) `(assoc ,x ,y))

;;; This screw is due to all the character set conversions.
;;;  means end of file for Gold Hill
;;; /= means = in ZL.
;;; So we have no choice but to use our own symbol.

(defmacro not= (x y) `(not (= ,x ,y)))

#+(and :CL (not :TI))
(defmacro  (x y) `(<= ,x ,y))
#+:TI
(shadowing-import 'zlc:)
 
#+(and :CL (not :TI))
(defmacro  (x y) `(>= ,x ,y))
#+:TI
(shadowing-import 'zlc:)

;;;******* look at gregors >gregor>pcl>macros
#+(and :CL (not (or :TI :Imach)))
(defmacro memq (x y) `(member ,x ,y :test #'eq))
#+:TI
(shadowing-import 'zlc:memq)
#+Imach
(defmacro memq (x y) `(member ,x ,y))

#+(and :CL (not :TI))
(defmacro neq (x y) `(not (eq ,x ,y)))
#+:TI
(shadowing-import 'ticl:neq)

#+(and :CL (not :TI))
(defmacro comment (&rest x) (declare (ignore x)) ())
#+:TI
(shadowing-import 'ticl:comment)

#+Genera
(defmacro make-tms-hash-table (&rest args)
  (setq args (copy-list args))
  (remf args :size)
  `(make-hash-table :locking nil . ,args))

#-Genera
(defmacro make-tms-hash-table (&rest args)
  `(make-hash-table . ,args))

(defvar *version* 25)				; ATMS version.

;;; Purely performance flags:
(defvar *c012* nil)				; Look of 0, 1, 2 contradictions first.

(defvar *clause-mode* nil)			; Use clauses.

(defvar *contradict-solutions* T)		; Contradict solutions in backtracking.

(defvar *resolve-by-labeling* nil)		; Don't try this unless you are Johan

(defvar *resolve-by-ordered-labeling* nil)	; Only if ADDB is active.

(defvar *addb-count*)				; Used by ADDB to order assumptions.

(defvar *union-check* T)			; Consult cons-env-cache on union.
						; Don't create env if inconsistent.
;;; Must be T for new interpretation constructor to work.

(defvar *explain-flag* nil)			; If T, explanations are more retrievable.

(defvar *simple-hybrid* nil)			; One env per label max.

(defvar *ltms* nil)				; Doesn't bother updating blocked labels completely.

(defvar *sltms* nil)				; Strict LTMS, with above set.

(defvar *rltms* nil)				; Real LTMS.

(defvar *ltms-mark-env*)			; In label when *rltms* is used.

(defvar *critical* nil)				; Critical Reasoning.

(defvar *clauses* nil)				; T if there are any clauses at all.

;;; Non performance flags.

(defvar *h4* nil)				; Use of rule *h4*
						; NIL = nothing.
						; 1 = Resolve everything.
						; 2 = Resolve binary.

(defvar *h4-adaptive* nil)			; Analog to Pearl/Dechter adaptive consistency

(defvar *k* nil)				; Freuder's k-consistency.
						; *k* > 1 is always presumed.
						; NIL means full *k*.
						; *k* = 1, Mackworth's node-consistency.
						; *k* = 2, Mackworth's arc-consistency.
						; *k* = 3, Mackworth's path-consistency.

(defvar *max-nogood-size* nil)			; Size of maximum nogood created.

(defvar *max-nogood-used-size* nil)		; Used in resolution.

(defvar *h4-trace* nil)

(defvar *luser-warning* T)			; Prints msg if ATMS gets brain-dead calls.

(defvar *h45* nil)				; Resolve binary disjunctions.
						; This is much like h4 and h5 for those.
						;  **** this is mostly broken right now.

(defvar *report-focussing* T)			; Report focus timings.

(defvar *atms* nil)

;;; Ultimately all the data structures should be here.
(defstruct (atms)
  (nogood-handler nil)				; The nogood handler for this ATMS.
  (string-assumption nil)			; Converts assumption into string.
  (node-string nil)				; Converts node into string.
  )

;;; These are all the definitions that are necessary so that the rest of the TMS
;;; package can load and compile in any order and any external system that
;;; uses TMS has a component system, only has to depend on this file (hopefully).

;;; fast-xxx array operations
;;; On the lispm, these are just 1-d arrays that we allow ourselves to %p-contents-offset
;;; and %p-store-contents-offset into.
;;; In Interlisp we just allocate block of storage and \getbaseptr \rplptr into them.

#+(OR :ZL :CADR :CL-ZL)
(defmacro fast-make-array (length &optional area) `(make-array ,length ':AREA ,area))

#+(OR :ZL :CADR :CL-ZL)
(defmacro fast-aref (base offset) `(%p-contents-offset ,base ,offset))

#+(OR :ZL :CADR :CL-ZL)
(defmacro fast-aset (value base offset) `(%p-store-contents-offset ,value ,base ,offset))

#+:CL
(defmacro fast-make-array (length &optional area) area `(make-array ,length))

#+:CL
(defmacro fast-aref (base offset) `(aref ,base ,offset))

#+:CL 
(defmacro fast-aset (value base offset) `(setf (aref ,base ,offset) ,value))

;;; Hash-Slots are basically just offsets into fast arrays.  There are almost completely
;;; implemented in terms of the fast-xxx array operations.

#+(and :SYMBOLICS (not :CL))
(defmacro hash-slot-value (slot) `(car ,slot))	

#+:CL
(defmacro hash-slot-value (slot) (once-only (slot) `(unless (integerp ,slot) ,slot)))

#+:CL
(defmacro hash-slot-set (slot value hash-table)
  `(setf (aref (hash-array-loc ,hash-table) ,slot) ,value))

#+(OR :CADR :ZL :CL-ZL)
(defmacro hash-slot-set (slot value) `(rplaca ,slot ,value))

#+:CADR
(defmacro make-art-q-list (count) `(make-array ,count ':TYPE ':ART-Q-LIST))

#+:ZL
(defmacro make-art-q-list (count) `(make-array ,count :TYPE ART-Q-LIST))

;;; Assumes 2s complement.
;;; *word-size* is the number of useful bits that can be used in a fixnum (including sign).
;;; *sign-bit* is a fixnum with the sign bit on, and the rest zero.
;;; *word-size* is a string of ones's, with a zero sign bit.
#+:CL
(eval-when (load eval compile)
(defconstant *word-size*
	     (1+ (min (integer-length most-positive-fixnum)
		      (integer-length most-negative-fixnum)))))

#+:CL
(eval-when (load eval compile)
(defconstant *word-value* (1- (expt 2. (1- *word-size*)))))
#+:CL
(defconstant *sign-bit* (- -1 *word-value*))

#+:ZL
(defconst *word-size* 32.)
#+:ZL
(defconst *word-value* #o17777777777)
#+:ZL
(defconst *sign-bit* (- -1 *word-value*))

#+:CADR
(defconst *word-size* 24.)
#+:CADR
(defconst *word-value* #o37777777)
#+:CADR
(defconst *sign-bit* (- -1 *word-value*))

;;; This creates a bit vector of length n.
(defmacro make-bit-vector (length) `(simple-make-list ,length 0))

;;; I am confused what the following was trying to achieve.
;;; Don't use MAPL anywhere::: Symbolics code for MAPL sucks.  Don't use it.
;#+(AND (NOT :XS) (OR :CADR :3600)) (defmacro mapl (f &rest lists) `(map ,f ,@lists))

;;; Common Lisp does not have areas.
(defmacro simple-make-list (length initial-value &optional area)
  area						
  #+(OR :CADR :ZL :CL-ZL) `(si:%make-list ,initial-value ,area ,length)	;**much more efficient on Symbolics machines.
  #+:CL `(make-list ,length :initial-element ,initial-value)	
  )
;;; A faster version of the usual copylist.  Don't use MAPL here its a dog.
(defun fcopylist (list &optional area &aux result)
  area
  (if (atom list)
      list
      (do ((l1 (setq result (simple-make-list (length list) 0 area)) (cdr l1))
	   (list list (cdr list)))
	  ((null l1) result)
	(rplaca l1 (car list)))))

(defun fcopylist1 (list length &aux result)
  (do ((l1 (setq result (simple-make-list length nil area)) (cdr l1))
       (list list (cdr list)))
      ((null l1) result)
    (rplaca l1 (car list))))

;;; Length is guaranteed.
(defun copyconc (list length cdr &aux result)
  (setq result (simple-make-list #+Symbolics (1+ length) #-Symbolics length nil))
  (do ((last-result nil result)
       (result result (cdr result))
       (list list (cdr list)))
      ((null list) 
       #-Symbolics (rplacd last-result cdr)
       #+Symbolics (rplaca (cdr last-result) cdr)
       ;; This magic turns the last element into an nconc.
       #+Symbolics  (sys:%p-dpb sys:cdr-normal sys:%%q-cdr-code last-result))
    (rplaca result (car list)))
  (values result (+ length (length cdr))))

;;; Warning ---- not quite the same as delq, but faster on average.

;;; Delete all occurances fast.
(defun fdelqa (item list &aux last-ptr last-last-ptr)
  (when
    ;; Flush the leading ones.
    (do nil (nil) (cond ((null list) (return nil))
			((neq item (car list)) (return t)))
	(setq list (cdr list)))
    ;; Find the next one.
    (setq last-last-ptr list last-ptr (memq item list))
    (do () ((null last-ptr))
      (do ((ptr (cdr last-ptr) (cdr ptr)))
	  ((null ptr) (do ((p1 last-last-ptr p2)
			   (p2 (cdr last-last-ptr) (cdr p2)))
			  ((eq (car p2) item) (rplacd p1 nil)))
	   (setq last-ptr nil))
	(unless (eq (car ptr) item)
	  (rplaca last-ptr (car ptr))
	  (rplacd last-ptr (cdr ptr))
	  (setq last-last-ptr last-ptr
		last-ptr (memq item (cdr last-ptr)))
	  (return))))
    list))

;;; Delete first occurrance fast.
(defun fdelq1 (item list &aux ptr)
  (setq ptr (memq item list))
  (cond ((null ptr) list)
	((cdr ptr) (rplaca ptr (cadr ptr)) (rplacd ptr (cddr ptr)) list)
	((eq item (car list)) (cdr list))
	(t (do ((p1 list p2)
		(p2 (cdr list) p3)
		(p3 (cddr list) (cdr p3)))
	       ((null p3) (rplacd p1 nil)))
	   list)))

#-(OR :CL-ZL :ZL)
(defmacro ncons (x) `(cons ,x nil))

#+:CL-ZL
(defmacro ncons (x) `(zl:ncons ,x))

;;; On the Symbolics 3600 (boole BOOLE-ANDC2 ...) is incredibly slow.

#+(or :ZL :CADR)
(defsubst not-subset-bits (x y) (not (zerop (logand x (lognot y)))))

#+:CL-ZL
(defsubst not-subset-bits (x y) (not (zerop (logand x (lognot y)))))

#+:CL
(defmacro not-subset-bits (x y) `(not (zerop (logand ,x (lognot ,y)))))

#+(OR :ZL :CADR :CL-ZL)
(defmacro set-bit (word bit) `(zl:%logdpb (car word) (byte 1 bit) 1))

;;; If this is called often, we might check of the many ways to compute this, which
;;; is more efficient.
#+(OR :CL :IL)
(defmacro set-bit (word bit)
  (once-only (bit)
    `(logior ,word (if (< ,bit (1- *word-size*)) (ash 1 ,bit) *sign-bit*))))

;;; We can't do the obvious thing and redefine apply in zl, cadr.
#+(OR :CL :CL-ZL)
(defmacro cl-apply (f &rest args) `(apply ,f ,@args))

#+(OR :ZL :CADR)
(defmacro cl-apply (f &rest args) `(lexpr-funcall ,f ,@args))

#+:CL 
(defmacro let-closed (bindings &body body) `(let ,bindings ,@body))

(defvar *temp-node-datum* "Temporary node")	; TMS will GC a node with this label.

(defvar *full-resolution-count*)		; Number of full resolutions performed.

(defvar *addb-check-count*)			; How many edges in search tree.

(defvar *minimal-nogood-count*)

(defvar *full-resolution-fail-count*)		; Number of immediately useless full
						; resolutions.

(defvar *big-union-count*)			; Number of unions, both envs are > 1.

(defvar *justification-count*)			; Number of justifications.

(defvar *exhaustions*)				; Number of ADDB exhaustians.

(defvar *binary-resolution-count*)		; Number of binary resolutions.

(defvar *assumption-counter*)			; Last assumption created.

(defvar *empty-env*)				; The empty assumption set.

(defvar *nodes*)				; List of all nodes.

(defvar *unfocussed-nodes*)			; Nodes with pending consumers.

(defvar *assumption-symbols* nil "Both positive and negative literals are assumptions.")

(defvar *empty-env-list*)			; A singleton of *empty-env*

(defvar *contra-node*)				; A node which is always a contradiction.

(defvar *going-nodes*)				; Nodes that are changing their status.

(defvar *changed-hybrid-nodes*)

(defvar *nodes-to-check* nil)			; LTMS nodes looking for alternative support.

(defvar *clauses-to-check* nil)			; Replaces above.

(defvar *env-counter*)				; Unique id for envs.

(defvar *update-counter* 0)

(defvar *contra-counter*)			; Unique id for contras.

(defvar *max-contra-count*)			; Maxinum number of assumptions in a contra.

(defvar *nogood-trees*)				; minimal nogoods represented as a tree.
						; Size 1, and 2 minimal nogoods are in the
						; tree, but not for any significant reason

(defvar *nogood-tree*)				; Alternative representation:
                                                ; all nogoods in one tree.

(defvar *single-nogood-tree* T)			; Which representation should be used.

(defvar *ors*)					; Disjunction/size array.

(defvar *environments*)				; Env/size array.
						; Only contains consistent environments.


(defvar *indexed-envs*)

(defvar *incomplete-assumption* nil)

(defvar *incomplete-assumptions* nil)		; Assumptions that have neither been
						; completed added or retracted.

(defvar *trace-write-hash* nil)

(defvar *trace-read-hash* nil)

(defvar *hashes*)				; T if hash table contains entries of length i

(defvar *max-env-count*)			; Max number of assumptions seen in an env.

(defvar *current-size*)				; Current size of table.  Must b <= than above

(defvar *consumer-invokations*)			; Number of consumers executed.

(defvar *consumers-exist* nil)			; There are consumers.

(defvar *contra-env*)				; The contradictory environment.

(defvar *env-hash-table* nil)			; Hash table for environments.

(defvar *assumption-array*)			; Unique is index.

(defvar *assumptions*)				; List of all assumptions.

(defvar *or-queue*)

(defvar *variables*)				; List of all oneof variables.
						; Of necessity each such variable-value
						; assumption must occur in exactly one class.

(defvar *randoms* nil)				; For use in brain damaged hash.

;(foo)

(defvar *dump* nil)

(defvar *nogood-stack*)				; Array of nogoods sorted by length
						; waiting to be resolved.
(defvar *nogood-count*)				; Nogood size currently being worked on.

(defvar *classes*)

(defvar *class-counter* 1)

(defvar *symbol-counter* 1)

(defvar *contradiction* nil)

(defvar *foci* nil)				; If non-nil, labeling is restricted to thse.
						; NIL means everything is in focus.
						; :EMPTY means nothing is in focus.

(defvar *agenda*)

(defvar *control-stack* nil "stack of disjunction-assumptions/current-assumption pairs")

(defvar *t* nil "Temporary node used to store bug result")

(defvar *current-context* nil "a generic environment")	; I never promised you a rose garden.

(defvar *current-nogoods* nil)

(defvar *breadth-q* nil)			; (cost . env).

(defvar *label-q* nil)				; (cost . justs|clauses)

(defvar *label-q-array* nil)			; Replaces *label-q*
(defvar *label-q-best* 0)
(defvar *label-q-worst* 0)

;;; ****** Needs to grow dynmically in the future.
;(defvar *env-counters* (make-array 32000  :element-type '(unsigned-byte 16)
;				          :initial-element #o177777))

;(defvar *env-counters* (zl:make-array 32000 :type 'sys:art-16b))

						
;(defvar *env-array* (make-array 32000))

(defvar *last-assumption-enabled* nil)

(defvar *total-assumption-counter*)

(defvar *fast-assumptions-size* 0)

(defvar *fast-assumptions-conses* nil)

(defvar *blits-to-assumptions-conses* nil)

;;; User settable flag.

;;; Flags used for experimentation by Johan.  No one should change these unless
;;; they are doing research on TMS's.

(defvar *contra-trace* nil)

(defvar *cache-union-flag* nil "Cache all non-trivial unions")

(defvar *trace* nil)

(defvar *update-trace* nil)

(eval-when (compile load eval)
(defmacro deffield (word-accessor field-accessor test-accessor size position)
  `(progn
     (defmacro ,field-accessor (object)
       `(ldb (byte ,,size ,,position) (,',word-accessor ,object)))
     (defmacro ,test-accessor (object)
       `(ldb-test (byte ,,size ,,position) (,',word-accessor ,object)))
     (defsetf ,field-accessor (object) (new-value)
       `(setf (,',word-accessor ,object)
	      (dpb ,new-value (byte ,,size ,,position) (,',word-accessor ,object)))))))

(eval-when (compile load eval) ; Needed because these get included in others.

;;; There is a fairly hairy mess of defstructs going down here.  NAME-SYMBOL is 
;;; included in all others in order to provide a fast way of telling if the structure
;;; is of a particular type or not.  The NAME-SYMBOL slot is set at construction-time
;;; by the node and assumption creation fns.  Sometimes, NAME-SYMBOL is inhereted
;;; through N-A, instead of being directly included.  This is because you can't do
;;; multiple :includes.  In most cases (e.g., in the case
;;; of CLASS and ENV structs) the NAME-SYMBOL slot is nil and isn't set by anyone.  Perhaps
;;; this should be changed so that they are set by the structure's MAKE- fn by using
;;; :INCLUDE-time defaults.  It doesn't matter for now.  These are actually
;;; only needed for things that are possibly going to be interpreted by the NODE? and
;;; ASSUMTION? function.  Things like OR and ^ don't get them.

(defstruct name-symbol name-symbol)

(defstruct (n-a 
              #+(and :cl (not :cl-zl))
                (:include name-symbol)		; Used to determine structure type fast.
           )
  (datum nil)					; What the problem solver sees.
  (consequents nil)				; Nodes that directly depend on this.
  (unique nil)
  (envs nil)					; The label.
  (contradictory nil)				; Node is false.
  (justifications nil)
;; The following are not used in the basic ATMS.
  (enqueued? nil)
  (justification-consumers nil)
  (env-consumers nil)
  (consumers nil)				; List of lists.
;; *** It's unclear whether assumptions need these.
  (status nil)					; IN/OUT/GOING-IN/GOING-OUT/STAYING-IN/
						; STAYING-OUT
  (classes nil)					; Classes of node.
  ;;**** reclaim node doesn't clear all these?
  (neg nil)					; The negation of this node, if any.
  ;; Soon this will be cleaned up.
  ;; Notice this slot is duplicated if neg exists.
  (pclauses nil)				; Clauses in which this appears +
  (nclauses nil)				; Clauses in which this appears -
  (symbol nil)
  (probability nil)
  (blocked nil)					
  (focus nil)					; This n-a- is correct for this focus.
  (support nil)					; Used for ltms.
  (nbits 0)						
  (mark nil)					; Used for search.  *** Could have a bit.
						; Which is cleared.
  )

) ; closes eval-when for included structures.

;(defmacro n-a-ltms-support (n-a) `(n-a-blocked ,n-a))	; Used only if *ltms* is T.

(defmacro n-a-contra-envs (n-a) `(n-a-focus ,n-a))

(defvar *trace-file* nil)

(deffield n-a-nbits n-a-has-consumers n-a-has-consumers? 1 0)

;(defmacro n-a-enqueued? (n-a) `(ldb-test (byte 1 0) (n-a-bits ,n-a)))


;;; Essentially, every node is part of its own class.
;;; This is an :INCLUDE, but ZL version sucks.
(defstruct (node (:include n-a) (:print-function print-node)
		 #+Symbolics (:size-symbol *node-size*)
		 )
  (assumption nil)				; Assumption associated with this node.
						; *********** Unconditional!!!!!
  (negation nil)				; Soon to be obsolete.*****
  (unique-conditional nil)
  )

;;;***** temporary.
(defmacro node-thread (node) `(node-negation ,node))

(defun print-node (node stream depth)
  depth						; What am I supposed to do with this?
  (format stream "#<NODE-~D: ~A>#" (n-a-unique node) (node-string node)))

(defstruct (informant) (family nil))		; The family of consumers to which it belongs.

;;; A propositional symbol.
(defstruct (psymbol #+(and :cl (not :cl-zl))
		    (:include name-symbol))
  (datum nil)					; The problem-solvers representation.
  (pnode nil)					; Positive node.
  (nnode nil)					; Negative node.
  (pclauses nil)				; Clauses in which it appears positively.
  (nclauses nil)				; Clauses in which it appears negatively.
  (unique nil)					; Unique id.
  (truth nil)					; TRUE|FALSE|NIL
  (or nil)					; Kludge: P or not P
  )						

;;; Notice that env can be packed and reduced in size in various ways if that
;;; becomes important.
(defstruct (env
	     (:print-function print-env))
  (cons-env-cache nil)				; (bit-vector (a . env) ...)
						; bit-vector indicates inconsistent a's.
  (assumptions nil)				; Sorted list of assumptions
  (q nil)					; 
						; Used for interpretation construction.

  (nodes nil)					; The nodes whose envs refer to it.
  (consumer-nodes nil)
  (count nil)					; Number of assumptions.
  (vector nil)					; Bit vector of assumptions.
  (uncons-cache nil)				; Uncons-env cache.  As this is
						; primarily heavily used for contra envs.
						; This could overlap with nodes slot.
                                                ; ******** do above!!!!***********
  (datum nil)					; For user.
  (bits 0)
  )

(deffield env-bits env-hybrid env-hybrid? 1 0)

(defmacro set-env-hybrid (env val) `(setf (env-hybrid ,env) ,val))

(deffield env-bits env-indexed env-indexed? 1 1)

(deffield env-bits env-toindex env-toindex? 1 2)

(deffield env-bits env-contradictory-bit env-contradictory 1 3)

(deffield env-bits env-has-string-bit env-has-string? 1 4)

;;; Allows for 500,000 environments
(deffield env-bits env-unique env-unique? 19 5)

;;; env-cons-env-cache is guaranteed to be empty if env is contradictory.
(defmacro env-contradictory-info (env) `(env-cons-env-cache ,env))

(defvar *env-string-table*)

;;; Change this to env-string next time you boot.***********
(defmacro cached-env-string (env) `(gethash (env-unique ,env) *env-string-table*))

(defstruct (just (:print-function print-just))
  (consequent nil)
  (informant nil)
  (antecedents nil)
  (cost nil)
  (thread nil)
  (count nil)
  (unused nil)
  (out-thread nil)				; Thread used in propagate outness.
  )

(defun print-just (just stream depth)
  depth						; What am I supposed to do with this?
  (format stream "#<JUST: ~A => ~A>#" (just-antecedents just) (just-consequent just)))

;;; Keep just and clause in sync, as both are accessed without regard to type.
(defstruct (clause (:print-function print-clause))
  (consequent nil)				; This changes.
  (informant nil)
  (positives nil)				; Always NIL.  Used to distinguish.
  (cost nil)
  (thread nil)
  (count nil)
  (negatives nil)
  (out-thread nil))

(defun print-clause (cl stream depth)
  depth
  (format stream "#<CLAUSE:")
  (dolist (n (clause-positives cl))
    (format stream "[+~A]" n))
  (dolist (n (clause-negatives cl))
    (format stream "[-~A]" n))
  (if (clause-consequent cl)
      (format stream " ==> ~A" (clause-consequent cl)))

  (format stream ">"))

(defmacro clause? (clause-or-just) `(null (clause-positives ,clause-or-just)))

;(defmacro env-waiting (x)
;  `(ldb (byte 15 0) (aref *env-counters* (env-unique ,x))))

;(defmacro env-waitingp (env) `(not (= #o77777 (env-waiting ,env))))

(defmacro env-waiting (x) `(env-q ,x))

(defmacro env-waitingp (env) `(env-waiting ,env))

;;; This is used for intermediate constructions to avoid needless creation and caching.
;;; By definition all simple-envs are consistent.  By definition simple-envs are not empty.
;;; By definition a simple-env does not appear in the hash table.
(defstruct (simple-env #+symbolics :tree
		       #+symbolics (:constructor nil)
		       #-symbolics (:type list)
		       #-symbolics
		       (:constructor make-simple-env
			(count cons-env-cache assumptions vector)))
  count						; Number of assumptions in simple-env.
  cons-env-cache				; As in env, result is only good for nogood.
  assumptions					; Unsorted shared list of assumptions.
						; (Sometimes sorted now).
  vector					; Vector of assumptions.
  )

(defmacro simple-envp (env) `(consp ,env))

;;; The SMBX Commonlisp compilers are so stupid they can't optimize their default constructor.
;;; So I have to do this gross hack.  I use a :TREE because creating lists is usually very
;;; slow.  On non-Symbolics machines the above declarations just create a list.  That
;;; may or may not be a good idea.
#+Symbolics
(defmacro make-simple-env (count cons-env-cache assumptions vector)
  `(cons (cons ,count ,cons-env-cache) (cons ,assumptions ,vector)))

(defmacro generic-env-assumptions (generic-env)
  (once-only (generic-env)
    `(if (simple-envp ,generic-env)
	 (simple-env-assumptions ,generic-env)
	 (env-assumptions ,generic-env))))

;;; This gives you the bit-vector.
(defmacro generic-env-cons-env-cache (generic-env)
  (once-only (generic-env)
    `(if (simple-envp ,generic-env)
	 (simple-env-cons-env-cache ,generic-env)
	 (car (env-cons-env-cache ,generic-env)))))

(defmacro generic-env-vector (generic-env)
  (once-only (generic-env)
    `(if (simple-envp ,generic-env)
	 (simple-env-vector ,generic-env)
	 (env-vector ,generic-env))))

(defmacro generic-env-count (generic-env)
  (once-only (generic-env)
    `(if (simple-envp ,generic-env)
	 (simple-env-count ,generic-env)
	 (env-count ,generic-env))))

(defun print-env (env stream depth) depth (format stream "ENV-~A" (env-unique env)))

(defmacro node? (node)
  `(eq #+(not :cl-zl) (name-symbol-name-symbol ,node)
       #+(or :zl :cl-zl) (aref ,node 0)
       'NODE))

;;; **** lots of problems here if neither :cl nor :cl-zl are set.
(defmacro careful-node? (node)
  #+(not :cl-zl) `(typep ,node 'NODE)
  #+:cl-zl
  (once-only (node) `(if (arrayp ,node) (node? ,node))))
  
(defmacro subsumed-nogood? (env) `(eq 'SUBSUMED (car (env-contradictory-info ,env))))

(defmacro cnsqnt-result (cnsqnt) `(car ,cnsqnt))

(defmacro cnsqnt-informant (cnsqnt) `(cadr ,cnsqnt))

(defmacro cnsqnt-ant (cnsqnt) `(cdr ,cnsqnt))

(defmacro cnsqnt-supporters (cnsqnt) `(cddr ,cnsqnt))

(defmacro i-in? (node) `(n-a-envs ,node))

(defmacro i-out? (n-a) `(null (n-a-envs ,n-a)))

;;; Note that the ATMS is usually incomplete.  Hence, true? may return NIL even
;;; though n-a is logically deducible.  The idea here is that true? should be a free
;;; test.  If you really want to know whether n-a is true, I have to write another function.

(defmacro i-true? (n-a)
  `(eq *empty-env*
       (if (atom (n-a-envs ,n-a))
	   (n-a-envs ,n-a)
	   (car (n-a-envs ,n-a)))))

(defmacro i-false? (n-a) `(n-a-contradictory ,n-a))
    
;;; For most problem solving applications, we have the notion of classes. i.e.,
;;; (foo 1) is an instance of (foo ?x).  This builds this into a TMS.

(defstruct (class
              #+(and :cl (not :cl-zl))
                (:include name-symbol)		; Used to determine structure type fast.
	     (:print-function print-class))
  (consumers nil)				; All consumers for this class.
  (nodes nil)					; All nodes of this class.
  (last-consumer nil)				; Last consumer.
  (datum nil)					; For poor user.
  (assumptions nil)				; For assumption classes only.
  (closed nil)					; Class is closed.
  (or nil)					; Disjunctive assumptions associated with it.
  (unique nil)
  (non-simple-assumptions nil)			; Assumptions which received new envs.
  (exclusive nil)				; T if label propagation should treat it
						; as an exclusion class.
  (oneof nil)					; T if a oneof class. (Only used if closed.)
  (allowable-data nil)				; Allowable data for nodes in class.
  )

(defun print-class (class stream depth)
  depth
  (format stream "#<class: ~A>" (class-datum class)))

;;; The way to distinguish between assumptions and nodes without an extra
;;; slot is to compare lengths.  But I have not tweaked that.
(defstruct (assumption (:include n-a) (:print-function print-assumption))
  (variable nil)				; Abstract variable assigned.
  (value nil)					; Its value.
  (string nil)					; For io.
  (node nil)					; The non-a node it supports.
  (xors nil)					; Xor assumption sets
  (gc-status nil)				; NEVER, DONT, DO, or DONE.
  (disjunctions nil)				; Control disjunctions it is in.
  (vector nil)					; Used for interpretation construction.
  (index nil)					; Used for interpretation construction.
  (nogoods nil)					; Nogoods > 2 it is part of for resolution.
  (offset nil)					; Offset in bit vector.
  (bits nil)					; Word in bit vector.
  (mask nil)					; Mask in bit vector
  (binary-vector nil)				; Of assumptions it is inconsistent with.
  (cons-cache nil)				; Cons-env cache
  (addb-index nil)				; Used for ordered addb resolution.
  (ignorep nil)					; T if assumption is ignored.
  (ors nil)					; Inclusive ors it is part of.
  (negation nil)				; Its negation.***** should be in n-a.
						;**** soon to be obsolete.
  (env nil)					; This is the singleton environment of itself.
  (blocked-nodes nil)				; Consumers waiting for this assumption.
  (nogood-stack nil)				; Used for ordered H4 resolution.
  (dirty nil)					; T if has appeared any any nogood
						; except class-exclusions.  If classes
						; are added after a nogood ... to bad.
  (in-envs nil)					; Environments in which it appears.
						; Experimental.
  (count nil)					; Length of in-envs.
  (in-focus nil)				; T iff in current focus.
  (indexed-to nil)
  (envs-to-index nil)
  )

(defmacro assumption-single (a) `(assumption-count ,a))

(defmacro in-current-focus? (env) `(or *ltms* (= (env-waiting ,env) 0)))

(defun print-assumption (assumption stream depth)
  depth
  (format stream "#<A-~D: ~A>" (assumption-unique assumption) (string-assumption assumption)))

(defmacro assumption? (assumption)
  `(eq #+(and :cl (not :cl-zl)) (name-symbol-name-symbol ,assumption)
       #+(and :cl :cl-zl) (aref ,assumption 0)
       'ASSUMPTION))

(defmacro careful-assumption? (assumption)
  #+(not :cl-zl) `(typep ,assumption 'ASSUMPTION)
  #+:cl-zl
  (once-only (assumption) `(if (arrayp ,assumption) (node? ,assumption))))

(defvar *free-nodes*)				; Reclaimed nodes.

(defvar *free-assumptions* nil)			; Free assumptions.

(defvar *node-counter* 1)

(defmacro assumption-orderp (e1 e2) `(> (assumption-unique ,e1) (assumption-unique ,e2)))

;;; Remember, subset-env? is called incredibly often, so this is worth it.
;;; The two eq tests may actually not be worth it?
(defmacro subset-env? (oe1 oe2)
  `((lambda (e1 e2)
      (cond ((eq e1 e2))
	    ((eq e1 *empty-env*))
	    (( (env-count e1) (env-count e2)) nil)
	    ((vector-subset (env-vector e1) (env-vector e2)))))
    ,oe1 ,oe2))

;;; Might need more work.
(defun generic-subset-env? (e1 e2 &aux c1 c2 v1 v2)
  (cond ((eq e1 e2) (return-from GENERIC-SUBSET-ENV? T))
	((eq e1 *empty-env*) (return-from GENERIC-SUBSET-ENV? T))
	((eq e2 *empty-env*) (return-from GENERIC-SUBSET-ENV? nil)))
  (setq c1 (generic-env-count e1)
	c2 (generic-env-count e2))
  (if (> c1 c2) (return-from GENERIC-SUBSET-ENV? nil))
  (setq v1 (generic-env-vector e1)
	v2 (generic-env-vector e2))
  (if (< c1 c2) (return-from GENERIC-SUBSET-ENV? (vector-subset v1 v2)))
  (vector-equal v1 v2))


;(bar)

;;; This is optimizes for the case where oe2 cannot be a subset oe1.
(defmacro proper-subset-env? (oe1 oe2)
  `((lambda (e1 e2)
      (cond ((eq e1 *empty-env*) (neq e2 *empty-env*))
	    (( (env-count e1) (env-count e2)) nil)
	    ((vector-subset (env-vector e1) (env-vector e2)))))
    ,oe1 ,oe2))

;;; Does the environment e contain the assumption a.  Does not work for all
;;; contradictory environments.

(defmacro has-assumption? (a e)
  `(vector-member ,a (env-vector ,e)))

;;; Not referentially transparent.
(defmacro map-assumptions (form &body body)
  `(let ((.offset. 0) ,(car form))
     (dolist (.word. ,(cadr form))
       (unless (= .word. 0)
	 (dotimes (.bit. #.*word-size*)
	   (unless (zerop (logand .word. 1))
	     (setq ,(car form) (aref *assumption-array* (+ .offset. .bit.)))
	     ,@body)
	   (setq .word. (ash .word. -1))))
       (incf .offset. #.*word-size*))))

(defmacro hybrid-label (node) `(n-a-envs ,node))

;;; This solves the structure forwarding problem.
(defstruct (hash (:type vector) :named)
  (p1 nil)					; Small prime.
  (p2 nil)					; Size of table --- a prime.
  (primes nil)					; Remaining good primes.
  (free nil)					; Number of free slots.
  (thresh nil)					; free > thresh or rehash.
  (array nil)					; hash array.
  (array-loc nil)					; (aloc array 0)
  (area nil)
  )

(defvar *reclaim-flag* T)			; Depends on problem whether worth it.
						; n-queens it has no effect.
						; speeds up inequal by a factor of 3.

(defvar *debug* nil "TMS is does extra checking to make sure everything is kosher")

;;; Infinite hair, just to handle a ^ a.
(defstruct ^
  (consumer nil)
  (nodes nil))					; (class . processed-nodes).



(defvar *sets*)

(defstruct constraint
  (consumer nil)
  (informant nil)				; To prevent reflections.
  (test nil)
  (condition nil)
  (classes nil)				; Each entry is (class . nodes).
  )

(defstruct (disjunction (:print-function print-or-defstruct))
  (disjuncts nil)				; Remaining neither true nor false.
  (odisjuncts nil)				; Originally supplied disjuncts.
  (informants nil)				; Originally supplied informants.
  (satisfied nil)				; T if one original disjunct is true.
  (vector nil)					; Vector of remaining.
;;; Crockery needed to account for COUNT special term in Xerox CML.
#+:il (il:count nil)					; Number remaining
#-:il (count nil)					; Number remaining
  (nogoods nil)					; Alist of (assumption . nogoods)
  (contra-counter -1)				; Last contra-counter for update.
  (nogood-explanations nil)
  )

(defun print-or-defstruct (or *standard-output* depth)
  depth
  (princ "#<or ")
  (print-or or)
  (princ ">"))

;;; Returns time in seconds as a floating point number.
(defun time-taken (start-time)
   (/ (float (- (get-internal-run-time) start-time)) internal-time-units-per-second))

(defun real-time-taken (start-time)
   (/ (float (- (get-internal-real-time) start-time)) internal-time-units-per-second))

;;;***** CLean this up some day.
(defmacro insert-in-tree (e tree)
  `(let ((.it. ,tree))
     (if .it. (insert-tree ,e .it.) (setf ,tree (insert-tree ,e .it.)))))

(defmacro insert-in-tree-4 (e tree as)
  `(let ((.it. ,tree))
     (if .it. (insert-tree-4 ,e .it. ,as) (setf ,tree (insert-tree-4 ,e .it. ,as)))))

(defmacro remove-from-tree (e tree)
  `(let ((.it. ,tree)) (if (remove-tree ,e .it.) (setf ,tree nil))))

(defmacro subsumed-from-tree (function misses as tree)		
  `(let ((.it. ,tree)) (if (subsumed-tree ,function ,misses ,as .it.) (setf ,tree nil))))

(defmacro subsumed-from-tree-4 (function as tree)		
  `(let ((.it. ,tree)) (if (subsumed-tree-4 ,function ,as .it.) (setf ,tree nil))))

;;; Must occur after env is defined.
;;; Remove all contradictory and nil envs.  If takes time, experiment with better
;;; impelementations.
(defun sanitize-envs (envs &aux flag)
  (do ((envs envs (cdr envs)))
      ((null envs))
    (cond ((null (car envs)) (setq flag T))
	  ((env-contradictory (car envs)) (rplaca envs nil) (setq flag T))))
  (if flag (fdelqa nil envs) envs))

(defmacro cons-unsafe (a b)
  `(let ((result (pop conses)))
     (rplaca result ,a)
     (rplacd result ,b)
     result))

(defmacro push-unsafe (a b)
  `(let ((result (pop conses)))
     (rplaca result ,a)
     (rplacd result ,b)
     (setq ,b result)))