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

(defstruct (queen (:print-function print-queen)) column)
  
(defun print-queen (queen stream depth)
  depth
  (format stream "#<Q~D>" (queen-column queen)))

(setf (get 'QUEEN :TMS-STRING) 'print-queen-assumption)

(defun print-queen-assumption (assumption type variable value)
  type assumption
  (format nil "[Q~D=~D]" (queen-column variable) value))

(defconsumer n-queens (node1 node2 &aux diff1 diff2) ()
  (cond ((= (n-a-datum node1) (n-a-datum node2))
	 (consumer-contradiction 'COLUMNS))
	(t (setq diff1 (- (queen-column (class-datum (car (n-a-classes node1))))
			  (queen-column (class-datum (car (n-a-classes node2)))))
		 diff2 (- (n-a-datum node1) (n-a-datum node2)))
	   (if (or (= diff1 diff2) (= diff1 (- diff2)))
	       (consumer-contradiction 'DIAGONALS)
	       ))))

(defun n-queens-old (n &optional (priority nil) (process-nogoods T) (find-interpretations T)
		   &aux queens values answer start-time class node)
  (setq start-time (get-internal-run-time))
  (init-tms T)
  ;; A variable for each row, its value is the column.
  (setq queens (make-array n))
  (dotimes (i n) (push i values))
  (dotimes (i n)
    (setq class (create-assumption-variable (make-queen :COLUMN i) values))
    (setf (aref queens i) class)
    (dolist (a (class-nodes class))
      (if priority (setf (assumption-addb-index a) i))
      (when (or *resolve-by-labeling* *resolve-by-ordered-labeling*)
	(setq node (create-node a))
	(setf (n-a-neg a) node)
	(setf (n-a-neg node) a))))

  ;;;****** above is no good.  Because it doesn't install the justification for false.
  ;;; Look at the previous version of it.

  (dotimes (i (1- n))
    (do ((j (1+ i) (1+ j)))
	(( j n))
      (create-consumer N-QUEENS (list (aref queens j) (aref queens i)) nil)))
  (format T "~% Setting up time is:~D seconds" (time-taken start-time))
  (run)
;  (when *h4* (reset-meter T) (meter T (process-queued-nogoods)))
  (if (and (or *h4* *resolve-by-labeling*) process-nogoods) (process-queued-nogoods))
  (if find-interpretations 
      (meter T (setq answer (interpretations))))
  (print-statistics answer)
  ;; This has to return answer to get accept to work.
  answer)

(defun n-queens (n &optional (priority nil) (process-nogoods T) (find-interpretations T)
		   &aux queens values answer start-time)
  (setq start-time (get-internal-run-time))
  (init-tms T)
  ;; A variable for each row, its value is the column.
  (setq queens (make-array n))
  (dotimes (i n) (push i values))
  (dotimes (i n)
    (setf (aref queens i) (create-variable (make-queen :COLUMN i) values
					   (if priority i))))
  (dotimes (i (1- n))
    (do ((j (1+ i) (1+ j)))
	(( j n))
      (create-consumer N-QUEENS (list (aref queens j) (aref queens i)) nil)))
  (format T "~% Setting up time is:~D seconds" (time-taken start-time))
  (run)
;  (when *h4* (reset-meter T) (meter T (process-queued-nogoods)))
  (if (and (or *h4* *resolve-by-labeling*) process-nogoods) (process-queued-nogoods))
  (if find-interpretations 
      (meter T (setq answer (interpretations))))
  (print-statistics answer)
  nil)

(defun hn-queens (n &optional (process-nogoods T) (find-interpretations T)
		   &aux queens values answer start-time sets)
  (setq start-time (get-internal-run-time))
  (init-tms)
  (setq *simple-hybrid* T)
  ;; A variable for each row, its value is the column.
  (setq queens (make-array n))
  (dotimes (i n) (push i values))
  (dotimes (i n)
    (setf (aref queens i) (create-lazy-variable (make-queen :COLUMN i) values)))
  (dotimes (i (1- n))
    (do ((j (1+ i) (1+ j)))
	(( j n))
      (create-consumer N-QUEENS (list (aref queens j) (aref queens i)) nil)))
  (format T "~% Setting up time is:~D seconds" (time-taken start-time))
;  (when *h4* (reset-meter T) (meter T (process-queued-nogoods)))
  (if (and (or *h4* *resolve-by-labeling*) process-nogoods) (process-queued-nogoods))
  (dotimes (i n)
    (push (class-assumptions (aref queens i)) sets))

  (if find-interpretations 
      (meter T (setq answer
		     (variable-interpretations-depth-stack-sets-focus *empty-env* sets))))
  (print-statistics answer)
  nil)

;;; This runs n-queens for various k as an experiment.
(defun n-queens-expt (&optional (start 4) by-labeling)
  (if by-labeling (setq *resolve-by-labeling* t *h4* nil)
                  (setq *resolve-by-labeling* nil *h4* 1))

  (do ((n start (1+ n)))
      (nil)
    (format T "~% n = ~D" n)
    (do ((i 2. (1+ i))) ((> i n))
      (setq *k* i)
      (format T "~% *k* = ~D" *k*)
      (n-queens n))))

(defvar *n*)

(defconsumer tn-queens (node1 node2 &aux diff1 diff2) ()
  (cond ((= (n-a-datum node1) (n-a-datum node2))
	 (consumer-contradiction 'COLUMNS))
	(t (setq diff1 (- (queen-column (class-datum (car (n-a-classes node1))))
			  (queen-column (class-datum (car (n-a-classes node2)))))
		 diff2 (- (n-a-datum node1) (n-a-datum node2)))
	   (if (or (= (mod diff1 *n*) (mod diff2 *n*))
		   (= (mod diff1 *n*) (mod (- diff2) *n*)))
	       (consumer-contradiction 'DIAGONALS)))))

(defun tn-queens (*n* &aux queens values answer start-time)
  (setq start-time (get-internal-run-time))
  (init-tms T)
  ;; A variable for each row, its value is the column.
  (setq queens (make-array *n*))
  (dotimes (i *n*) (push i values))
  (dotimes (i *n*)
    (setf (aref queens i) (create-variable (make-queen :COLUMN i) values)))
  (dotimes (i (1- *n*))
    (do ((j (1+ i) (1+ j)))
	(( j *n*))
      (format T "Consumer made for ~a ~a ~%" j i)
      (create-consumer TN-QUEENS (list (aref queens j) (aref queens i)) nil)))
  (format T "~% Setting up time is:~D seconds" (time-taken start-time))
  (run)
  (if *h4* (process-queued-nogoods))
  (setq answer (interpretations))
  (print-statistics answer)
  ;; This returns the answer so that accept can check it.
  answer
  )



;;; This uses dependency directed backtracking.
(defun dn-queens (n &optional print &aux queens values answer start-time variable *count*)
  (setq *count* 0)
  (setq start-time (get-internal-run-time))
  (init-tms T)
  ;; A variable for each row, its value is the column.
  (setq queens (make-array n))
  (dotimes (i n) (push i values))
  (dotimes (i n)
    (setq variable (create-variable (make-queen :COLUMN i) values))
    (setf (aref queens i) variable)
    (assert-control-disjunction (class-assumptions variable)))
  (dotimes (i (1- n))
    (do ((j (1+ i) (1+ j)))
	(( j n))
      (create-consumer N-QUEENS (list (aref queens j) (aref queens i)) nil)))
  (format T "~% Setting up time is:~D seconds" (time-taken start-time))
  (catch 'CONTRADICTION
    (run)
    (backtrack print))
  (print-statistics answer)
  (format T "~% Queen checks: ~D" *count*)
  answer
  )

(defun queens (n) (/ (- (expt n 4) (expt n 3)) 2.))

;;; Paul Morris's n-queens formulation.
(defun pn-queens (n &aux queens values start-time last-positions next-positions)
  (setq start-time (get-internal-run-time))
  (init-tms)
  ;; A variable for each row, its value is the column.
  (setq queens (make-array n))
  (dotimes (i n) (push i values))
  (dotimes (i n)
    (setf (aref queens i) (create-variable (make-queen :COLUMN i) values)))
  (dotimes (i (1- n))
    (do ((j (1+ i) (1+ j)))
	(( j n))
      (create-consumer N-QUEENS (list (aref queens j) (aref queens i)) nil)))
  (format T "~% Setting up time is:~D seconds" (time-taken start-time))
  (run)
  ;; Thus far things are the same.
  (setq start-time (get-internal-run-time))
  (setq last-positions (create-node 'TRUE))
  (justify-node last-positions '(TRUE))
  (dotimes (i n)
    (setq next-positions (create-node (format nil "Position on row ~D" i)))
    (dolist (position (class-nodes (aref queens i)))
      (justify-node next-positions (list '(COMPOSE) last-positions position)))
    (format T "~% position ~D has ~D possibilities" i (length (n-a-envs next-positions)))
    (setq last-positions next-positions)
    )
  (format T "~% Justification time is:~D seconds" (time-taken start-time))
  (n-a-envs next-positions)
  )

(defun parity (n &aux odd even bits bit0 bit1 nodd neven start)
  (setq odd (create-node "ODD") even (create-node "EVEN"))
  (justify-node even (list 'TRUTH))
  (dotimes (i n)
    (format T "~% Adding bit ~D" i)
    (setq start (get-internal-run-time))
    (setq bits (create-variable (format nil "bit-~D" i) '(0 1))
	  bit0 (find-variable-value bits '0)
	  bit1 (find-variable-value bits '1)
	  nodd (create-node (format nil "bits-~D are odd" i))
	  neven (create-node (format nil "bits-~D are even" i)))
    (justify-node neven (list 'EVEN even bit0))
    (justify-node neven (list 'EVEN odd bit1))
    (justify-node nodd (list 'ODD even bit1))
    (justify-node nodd (list 'ODD odd bit0))
    (setq even neven odd nodd)
    (format T "~% Time is:~D seconds" (time-taken start)))
  (print-statistics nil)
  even)

;;; For metering only.
(defun mparity (n &aux odd even bits bit0 bit1 nodd neven)
  (setq odd (create-node "ODD") even (create-node "EVEN"))
  (justify-node even (list 'TRUTH))
  (dotimes (i n)
    (setq bits (create-variable (format nil "bit-~D" i) '(0 1))
	  bit0 (find-variable-value bits '0)
	  bit1 (find-variable-value bits '1)
	  nodd (create-node (format nil "bits-~D are odd" i))
	  neven (create-node (format nil "bits-~D are even" i)))
    (justify-node neven (list 'EVEN even bit0))
    (justify-node neven (list 'EVEN odd bit1))
    (justify-node nodd (list 'ODD even bit1))
    (justify-node nodd (list 'ODD odd bit0))
    (setq even neven odd nodd))
  even)

(defun good-parity (n &optional print
		      &aux odd even bits bit0 bit1 nodd neven start start-time)
  (init-tms T)
  (setq start-time (get-internal-run-time)
	odd (create-node "ODD") even (create-node "EVEN"))
  (justify-node even (list 'TRUTH))
  (dotimes (i n)
    (format T "~% Adding bit ~D" i)
    (setq start (get-internal-run-time)
	  bits (create-variable (format nil "bit-~D" i) '(0 1))
	  bit0 (find-variable-value bits '0)
	  bit1 (find-variable-value bits '1)
	  nodd (create-node (format nil "bits-~D are odd" i))
	  neven (create-node (format nil "bits-~D are even" i)))
    (assert-control-disjunction (class-assumptions bits))
    (justify-node-consumer neven (list 'EVEN even bit0))
    (justify-node-consumer neven (list 'EVEN odd bit1))
    (justify-node-consumer nodd (list 'ODD even bit1))
    (justify-node-consumer nodd (list 'ODD odd bit0))
    (setq even neven odd nodd)
    (run)
    (format T "~% Time is:~D seconds" (time-taken start)))
  (backtrack print)
  (format T "~% Running time is:~D seconds" (time-taken start-time))
  (print-statistics nil)
  (values odd even))


;;; None of these justify-nodes are right they are missing informants.

(defun unout-test1 ()
  (declare (special A A* A** B B* C C* D E AC))
  (init-tms t)
  (setq a (create-node "A")
	a* (assume-datum "A*")
	a** (assume-datum "A**")
	b (create-node "B")
	b* (assume-datum "B*")
	c (create-node "C")
	c* (assume-datum "C*")
	d (create-node "D")
	e (create-node "E"))
  (justify-node *contra-node* (list nil b* a**))
  (justify-node a (list nil a**))
  (justify-node b (list nil b*))
  (justify-node c (list nil c*))
  (justify-node d (list nil a b))
  (justify-node e (list nil a c))
  (print-nodes)
  ;; This should bring D in for the first time.
  (justify-node a (list nil a*))
  (print-nodes))

(defconsumer introduce (a b) (new)
  (justify-node (create-node new) (list 'JUST a b)))

;;; Macros to make examples easier to write.
(defmacro defnodes (&rest pairs)
  `(progn . ,(mapcar #'(lambda (pair)
			 (if (listp pair)
			     `(setq ,(first pair) (create-node ,(second pair)))
			     `(setq ,pair (create-node #+:IL ,pair
						       #-:IL ,(string-downcase pair)))))
		   pairs)))

(defmacro defassumptions (&rest pairs)
  `(progn . ,(mapcar #'(lambda (pair)
			 (if (listp pair)
			     `(setq ,(first pair) (create-assumption ,(second pair)))
			     `(setq ,pair (create-assumption #+:IL ,pair
							     #-:IL ,(string-upcase pair)))))
		   pairs)))

;;; Unouting test with node consumers.
(defun unout-test2 ()
  (declare (special A A* A** B B* C C* D E AC))
  (init-tms t)
  (defnodes a b c)
  (create-consumer introduce (list a b) nil :NEW "D")
  (create-consumer introduce (list a c) nil :NEW "E")
  (print-nodes)
  (defassumptions (b* "B*") (c* "C*") (a** "A**"))
  (justify-node *contra-node* (list 'JUST b* a**))
  (run)
  (justify-node b (list 'JUST b*))
  (justify-node a (list 'JUST a**))
  (justify-node c (list 'JUST c*))
  (print-nodes)
  (setq a* (assume-datum "A*"))
  (justify-node a (list 'JUST a*))
  (run)
  (print-nodes))

;;; Unouting test with class consumers. (Brain damaged thing to do, but it tests.)
;;; Why is the (let () ...) needed *****? Without it you'll get an error msg.
(defconsumer introduce-3 (a b) (name)
  (let ()
    (declare (special d))
    (justify-node (car (push (create-node name) d))
		  (list 'JUST a b))))

(defun unout-test3 (&aux bc cc)
  (declare (special A A* A** B B* C C* D E AC))
  (setq d nil e nil)
  (init-tms t)
  (setq ac (create-class "Ac")
	bc (create-class "Bc")
	cc (create-class "Cc"))
  (create-consumer introduce-3 (list ac bc) nil :NAME "Another D")
  (create-consumer introduce-3 (list ac cc) nil :NAME "Another E")
  (setq a (create-node "A"))
  (setq b (create-node "B"))
  (setq c (create-node "C"))
  (add-class-to-node a ac)
  (add-class-to-node b bc)
  (add-class-to-node c cc)
  (print-nodes)
  (setq b* (assume-datum "B*"))
  (setq a** (assume-datum "A**"))
  (justify-node *contra-node* (list 'JUST b* a**))
  (run)
  (justify-node b (list 'JUST b*))
  (justify-node a (list 'JUST a**))
  (setq c* (assume-datum "C*"))
  (justify-node c (list 'JUST c*))
  (run)
  (print-nodes)
  (setq a* (assume-datum "A*"))
  (justify-node a (list 'JUST a*))
  (run)
  (print-nodes))

;;;** self automatically special?
(defconsumer test1 (a) nil a (break "hifolks"))

(defun test1 ()
  (declare (special A A* A** B B* C C* D E AC))
  (init-tms t)
  (setq ac (create-class "Ac"))
  (run)
  (create-consumer test1 (list ac) nil)
  (run)
  (setq a (assume-datum "A"))
  (add-class-to-node a ac)
  (print-nodes))

;;; Example from paper.
(defun test2 (&aux a c b d e)
  (init-tms t)
  (setq a (create-assumption "A")
	b (create-node "b")
	c (create-assumption "C")
	d (create-node "d")
	e (create-node "e"))
  (justify-node b (list nil a))
  (justify-node d (list nil c))
  (justify-node e (list nil a c))
  (print-envss (env-interpretations))
  (justify-node *contra-node* (list nil b d))
  (print-envss (env-interpretations)))

(defun test3 (&aux a b)
  (init-tms t)
  (setq a (assume-datum "a")
	b (assume-datum "b"))
  (justify-node b (list nil a))
  (justify-node a (list nil b))
  (print-envss (env-interpretations)))
  
(defun test4 (&aux a b)
  (init-tms t)
  (setq a (assume-datum "a")
	b (assume-datum "b"))
  (justify-node b (list nil a))
  (print-envss (env-interpretations)))


(defvar *fact-count*)

(defun fact (n &aux (result 1))
  (incf *fact-count*)
  (do ((j 1 (1+ j)))
      ((> j n))
    (setq result (* result j)))
  result)

;;; The problem in Lisp.
(defun lpl (&aux a b c)
  (dotimes (x 2)
    (setq a (* x (fact (+ x 10.))))
    (format T "~% x=~D, a=~D" x a)
    (dotimes (y 2)
      (setq b (* y (fact (+ y 11.))))
      (format T "~% x=~D, y=~D b=~D" x y b)
      (dotimes (z 2)
	(setq c (* z (fact (+ z 12.))))
	(format T "~% x=~D, y=~D, z=~D, c=~D" x y z c)
	(and (not= a b)
	     (= (* z a) (* x c))
	     (format T "~% Solution: X=~D,Y=~D,Z=~D" x y z))))))


(defun lpl1 (&aux a b c (*fact-count* 0))
  (dotimes (x 2)
    (setq a (fact (+ x 10.)))
    (format T "~% x=~D, a=~D" x a)
    (dotimes (y 2)
      (setq b (fact (+ y 10.)))
      (format T "~% x=~D, y=~D b=~D" x y b)
      (dotimes (z 2)
	(setq c (fact (+ z 10.)))
	(format T "~% x=~D, y=~D, z=~D, c=~D" x y z c)
	(and (not= a b)
	     (= (* z a) (* x c))
	     (format T "~% Solution: X=~D,Y=~D,Z=~D" x y z)))))
  (format T "~% ~D factorials" *fact-count*))

(defun lpl2 (&aux a b c (*fact-count* 0))
  (dotimes (x 2)
    (setq a (fact (+ x 10.)))
    (format T "~% x=~D, a=~D" x a)
    (dotimes (y 2)
      (setq b (fact (+ y 10.)))
      (format T "~% x=~D, y=~D b=~D" x y b)
      (dotimes (z 2)
	(setq c (fact (+ z 10.)))
	(format T "~% x=~D, y=~D, z=~D, c=~D" x y z c)
	(and (not= a b)
	     (not= b c)
	     (format T "~% Solution: X=~D,Y=~D,Z=~D" x y z)))))
  (format T "~% ~D factorials" *fact-count*))

(defun lpl3 (&aux a b c (*fact-count* 0))
  (dotimes (x 2)
    (setq a (fact (+ x 10.)))
    (format T "~% x=~D, a=~D" x a)
    (dotimes (y 2)
      (setq b (fact (+ y 10.)))
      (format T "~% x=~D, y=~D b=~D" x y b)
      (and (not= a b)
	   (dotimes (z 2)
	     (setq c (fact (+ z 10.)))
	     (format T "~% x=~D, y=~D, z=~D, c=~D" x y z c)
	     (and 
	       (not= b c)
	       (format T "~% Solution: X=~D,Y=~D,Z=~D" x y z))))))
  (format T "~% ~D factorials" *fact-count*))


;;; Here are lots of examples from the papers.  They are numbered by paper and page number.
(defun egII6 (&aux ac)
  (init-tms)
  (setq *h4* 1 *h45* nil)
  (print-hs)
  (egII6a)
  (unless (n-a-contradictory ac) (error "Error nogood{C} not deduced with h4."))
  (init-tms)
  (setq *h4* nil *h45* T)
  (print-hs)
  (egII6a)
  (unless (n-a-contradictory ac) (error "Error nogood{C} not deduced h45.")))

(defun egII6a ()
  (declare (special aa ab a b c ac))
  (defnodes a b c)
  (defassumptions (aa "A") (ab "B") (ac "C"))
  (justify-node a (list 'EGII6 aa))
  (justify-node b (list 'EGII6 ab))
  (justify-node c (list 'EGII6 ac))
  (choose (list aa ab) 'EGII6)
  (justify-node *contra-node* (list 'EGII6 c a))
  (justify-node *contra-node* (list 'EGII6 c b))
  (print-inputs)
  (process-queued-nogoods)
  (print-nodes))

(defun egII7 ()
  (declare (special aa ab a b c))
  (init-tms)
  (defnodes a b c)
  (defassumptions (aa "A") (ab "B"))
  (justify-node a (list 'EG7 aa))
  (justify-node b (list 'EG7 ab))
  (justify-node c (list 'EG7 a))
  (justify-node c (list 'EG7 b))
  (choose (list aa ab) 'EG7)
  (print-inputs)
  (print-nodes)
  (h5 c)
  (print-nodes))

(defun egII8 ()
  (declare (special c))
  (setq *h4* nil *h45* T)
  (print-hs)
  (egII8a)
  (unless (i-true? c) (error "c not proven universally"))
  (setq *h45* nil)
  (print-hs)
  (egII8a)
  (h5 c)
  (print-nodes)
  (unless (i-true? c) (error "c not proven universally")))

(defun egII8a ()
  (declare (special aa ab a b c))
  (init-tms)
  (defnodes a b c)
  (defassumptions (aa "A") (ab "B"))
  (justify-node a (list 'EG7 aa))
  (justify-node b (list 'EG7 ab))
  (justify-node c (list 'EG7 a))
  (justify-node *contra-node* (list 'EG7 b))
  (choose (list aa ab) 'EG7)
  (print-inputs)
  (print-nodes))


(defun IIp17 ()
  (format T "~% Example of page 17 Extending the ATMS")
  (format T "~% Without resolution.")
  (setq *h4* 1 *h45* nil)
  (IIp17a)
  )

(defun IIp17a ()
  (declare (special ~b aa b c d))
  (init-tms)
  (print-hs)
  (defnodes b ~b c d)
  (defassumptions (aa "A"))
  (negation b ~b)
  (justify-node c (list 'EG aa ~b))
  (justify-node c (list 'EG b))
  (justify-node d (list 'EG c))
  (h5 d)
  (print-inputs)
  (print-nodes)
  )

(defun IIp18 ()
  (declare (special aa b c d))
  (format T "~% Example of page 18 Extending the ATMS")
  (init-tms)
  (setq *h4* 1)
  (print-hs)
  (defnodes b c d)
  (defassumptions (aa "A"))
  (encode-by-disjunction (list '=> (list aa) (list b c)))
  (justify-node c (list 'EG b))
  (justify-node d (list 'EG c))
  (print-inputs)
  (print-nodes))

(defun IIp19 ()
  (declare (special aa ee b c d e a))
  (format T "~% Example of page 18 Extending the ATMS")
  (init-tms)
  (setq *h4* 1)
  (print-hs)
  (defnodes b c d e)
  (defassumptions (aa "A") (ee "E"))
  (encode-by-buggy-simple-implication (list '=> (list aa) (list b c)))
  (encode-by-buggy-simple-implication (list '=> (list e) (list b c d)))
  (justify-node *contra-node* (list 'EG b))
  (justify-node *contra-node* (list 'EG c))
  (justify-node e (list 'EG ee))
  (justify-node a (list 'EG aa))
  (justify-node c (list 'EG b))
  (justify-node d (list 'EG c))
  (print-inputs)
  (print-nodes))

(defun IIp21 ()
  (declare (special aa ee b c d e a))
  (format T "~% Example of page 21 Extending the ATMS")
  (init-tms)
  (setq *h4* 1)
  (print-hs)
  (defnodes b c d e)
  (defassumptions (aa "A") (ee "E"))
  (encode-by-implication-a (list '=> (list aa) (list b c)))
  (encode-by-implication-a (list '=> (list e) (list b c d)))
  (justify-node *contra-node* (list 'EG b))
  (justify-node *contra-node* (list 'EG c))
  (justify-node e (list 'EG ee))
  (justify-node a (list 'EG aa))
  (justify-node c (list 'EG b))
  (justify-node d (list 'EG c))
  (print-inputs)
  (print-nodes))

(defun IIp24 ()
  (declare (special aa b c))
  (format T "~% Example of page 24 Extending the ATMS")
  (init-tms)
  (setq *h4* 1)
  (print-hs)
  (defnodes b c)
  (defassumptions (aa "A"))
  (nm-justify-node c (list aa) (list b) 'EG)
  (print-inputs)
  (print-nodes))

(defun IIp25a ()
  (declare (special aa b c))
  (format T "~% Example of page 25 Extending the ATMS")
  (init-tms)
  (setq *h4* 1)
  (print-hs)
  (defnodes b c)
  (defassumptions (aa "A"))
  (nm-justify-node c (list aa) (list b) 'EG)
  (justify-node *contra-node* (list 'EG c))
  (print-inputs)
  (print-nodes)
  (process-queued-nogoods)
  (h5 b)
  (print-nodes))

(defun IIp25b ()
  (declare (special aa b c d))
  (format T "~% Example of page 25 Extending the ATMS")
  (init-tms)
  (setq *h4* 1)
  (print-hs)
  (defnodes b c d)
  (defassumptions (aa "A"))
  (nm-justify-node c (list aa) (list b) 'EG)
  (justify-node d (list 'EG b))
  (justify-node d (list 'EG c))
  (print-inputs)
  (print-nodes)
  (format T "~% Hyperresolution...")
  (process-queued-nogoods)
  (h5 d)
  (print-nodes))


(defun IIp26 ()
  (declare (special n aa))
  (format T "~% Example of page 26 Extending the ATMS")
  (init-tms)
  (setq *h4* 1)
  (print-hs)
  (defnodes n)
  (defassumptions (aa "A"))
  (nm-justify-node n (list aa) (list n) 'EG)
  (print-inputs)
  (print-nodes)
  )

(defun greiner ()
  (declare (special a b q ~q))
  (defassumptions (a "A") (b "B") (q "Q") (~q "~Q"))
  (format T"~% Greiner's question.")
  (init-tms)
  (setq *h4* 1)
  (justify-node *contra-node* (list 'NEGATION q ~q))
  (choose (list q ~q) '(NEGATION))
  (justify-node b (list nil a))
  (justify-node q (list nil b)))



;;; ***** this causes interpetations to go into an inf loop.
(defun test-SANJAY-TEST ()
  (sanjay '((EQUIV (= (X P1) A) (= (X P1) D))
	    (EQUIV (= (Y P2) E) (= (X P2) C))
	    (EQUIV (= (X P1) D) (= (Y P1) A))
	    (EQUIV (= (Y P2) C) (= (X P2) E)))
   '((X ((= P1 A) (= P2 B)) ((= P1 A) (= P2 C)) ((= P1 D) (= P2 E)) ((= P1 D) (P2 F)))
     (Y ((= P1 A) (= P2 B)) ((= P1 A) (= P2 C)) ((= P1 D) (= P2 E)) ((= P1 D) (P2 F))))))

(defun SANJAY-TEST ()
  (sanjay '((EQUIV (= (X P1) A) (= (Y P1) D))
	    (EQUIV (= (Y P2) E) (= (X P2) C))
	    (EQUIV (= (X P1) D) (= (Y P1) A))
	    (EQUIV (= (Y P2) C) (= (X P2) E)))
   '((X ((= P1 A) (= P2 B)) ((= P1 A) (= P2 C)) ((= P1 D) (= P2 E)) ((= P1 D) (= P2 F)))
     (Y ((= P1 A) (= P2 B)) ((= P1 A) (= P2 C)) ((= P1 D) (= P2 E)) ((= P1 D) (= P2 F))))))

(defun sanjay (constraints parts &aux var defs dnf conjunct)
  (init-tms)
  (dolist (constraint constraints)
    (selectq (car constraint)
      (EQUIV (equiv (find-sanjay (second constraint))
		    (find-sanjay (third constraint))))
      (T (error "Unimplemented"))))
  (dolist (part parts)
    (setq var (car part) defs (cdr part) dnf nil)
    (dolist (def defs)
      (setq conjunct nil)
      (dolist (descriptor def)
	;; Assumes = crock***.
	(push (find-or-make-assumption (find-or-make-class (list var (second descriptor)))
				       (third descriptor))
	      conjunct))
      (push conjunct dnf))
    (dnf dnf))
  (dolist (class *classes*) (close-variable-class class))
  )

(defun find-sanjay (descriptor)
  (selectq (car descriptor)
    (= (find-or-make-assumption (find-or-make-class (second descriptor)) (third descriptor)))
    (T (error "Unimplemented"))))


;;; A crock.

(defun print-solution (interpretation &aux found)
  (terpri)
  (dolist (class (reverse *classes*))
    (setq found nil)
    (dolist (a (class-assumptions class))
      (when (true-in? a interpretation)
	(princ a)
	(when found (format T "~% But two possible values were found???")
	      (describe a)
	      (describe found))
	(setq found a))
      )
      (unless found (format T "~A=???" class))))



;;; Sanjay's roll place problem the dumb way as an experiment

(defconsumer x1 (position) ()
  (cond ((< (n-a-datum position) 75.) (consumer-contradiction 'X1-RANGE))
	((> (n-a-datum position) 135.) (consumer-contradiction 'X1-RANGE))))

(defconsumer x5 (position) ()
  (if (< (n-a-datum position) 800.) (consumer-contradiction 'X5-RANGE)))

;;; The positions can't be closer than 10, or further apart than 175.
(defconsumer OBSTACLE1 (pos &aux i) ()
  (setq i (n-a-datum pos))
  (cond ((< i 300))
	((> i 350))
	(t (consumer-contradiction 'OBSTACLE1))))

(defconsumer OBSTACLE2 (pos &aux i) ()
  (setq i (n-a-datum pos))
  (cond ((< i 650))
	((> i 700))
	(t (consumer-contradiction 'OBSTACLE2))))

(defconsumer IMMEDIATE-DIFFERENCE (pos1 pos2 &aux xi xj) ()
  (setq xi (n-a-datum pos1) xj (n-a-datum pos2))
  (cond ((<= xj xi) (consumer-contradiction 'AFTER))
	((< (- xj xi) 10) (consumer-contradiction 'TOO-CLOSE))
	((> (- xj xi) 175) (consumer-contradiction 'TOO-FAR))))

;;; Any two rolls must be equal to or more than 300 part.

(defconsumer DIFFERENCE (pos1 pos2 &aux xi xj) ()
  (setq xi (n-a-datum pos1) xj (n-a-datum pos2))
  (if (< (- xj xi) 300) (consumer-contradiction 'TWO-TOO-CLOSE)))


(defun simple-rolls3 (&aux x1 x2 x3 x4 x5 values l)
  (init-tms)
  (do ((i 900. (1- i)))
      ((= i 0))
    (push i values))
  (setq x1 (time (create-assumption-variable "X1" values))
	x2 (time (create-assumption-variable "X2" values))
	x3 (time (create-assumption-variable "X3" values))
	x4 (time (create-assumption-variable "X4" values))
	x5 (time (create-assumption-variable "X5" values)))
  (dolist (x1 (class-nodes x1))
    (when (or (< (n-a-datum x1) 75.)
	      (> (n-a-datum x1) 135.))
      (contradictory-node x1 '(X1))))
  (dolist (x5 (class-nodes x5))
    (when (< (n-a-datum x5) 800.)
      (contradictory-node x5 '(X5))))
  (create-consumer X5 (list x5) nil)
  (setq l (list x1 x2 x3 x4 x5))
  (dolist (x l)
    (create-consumer OBSTACLE1 (list x) nil)
    (create-consumer OBSTACLE2 (list x) nil))
  (do ((l l (cdr l)))
      ((null (cdr l)))
    (dolist (pos2 (cdr l))
      (create-consumer IMMEDIATE-DIFFERENCE (list (car l) pos2) nil))
    (dolist (pos2 (cddr l))
      (create-consumer DIFFERENCE (list (car l) pos2) nil)))
  )



  
;; Here is where we could use two-classes,
  ;; but we better not given the current consumer bugs.

;;; This circumvents the consumers.  Perhaps there should be some
;;; way of more cleverly compiling simple-rolls.

(defun simple-rolls2 (&aux x1 x2 x3 x4 x5 values l)
  (init-tms)
  (do ((i 900. (1- i)))
      ((= i 0))
    (push i values))
  (setq x1 (time (create-assumption-variable "X1" values))
	x2 (time (create-assumption-variable "X2" values))
	x3 (time (create-assumption-variable "X3" values))
	x4 (time (create-assumption-variable "X4" values))
	x5 (time (create-assumption-variable "X5" values)))
  (dolist (x1 (class-nodes x1))
    (when (or (< (n-a-datum x1) 75.)
	      (> (n-a-datum x1) 135.))
      (contradictory-node x1 '(X1))))
  (dolist (x5 (class-nodes x5))
    (when (< (n-a-datum x5) 800.)
      (contradictory-node x5 '(X5))))
  (create-consumer X5 (list x5) nil)
  (setq l (list x1 x2 x3 x4 x5))
  (dolist (x l)

    (create-consumer OBSTACLE1 (list x) nil)
    (create-consumer OBSTACLE2 (list x) nil))
  (do ((l l (cdr l)))
      ((null (cdr l)))
    (dolist (pos2 (cdr l))
      (create-consumer IMMEDIATE-DIFFERENCE (list (car l) pos2) nil))
    (dolist (pos2 (cddr l))
      (create-consumer DIFFERENCE (list (car l) pos2) nil)))
  ;; Here is where we could use two-classes,
  ;; but we better not given the current consumer bugs.
  )


(defmacro in-range (x)
  (once-only (x)
    `(or (< ,x 300.) (> ,x 700.) (and (> ,x 350) (< ,x 700.)))))

(defun simple-rolls5 (&aux x1 x2 x3 x4 x5 values l x1-values x5-values)
  (init-tms)
  (do ((i 900. (1- i)))
      ((= i 0))
    (if (in-range i) (push i values)))
  (do ((i 75. (1+ i)))
      ((> i 135.))
    (if (in-range i) (push i x1-values)))
  (do ((i 800. (1+ i)))
      ((> i 900.))
    (if (in-range i) (push i x5-values)))

  (setq x1 (time (create-assumption-variable "X1" x1-values))
	x2 (time (create-assumption-variable "X2" values))
	x3 (time (create-assumption-variable "X3" values))
	x4 (time (create-assumption-variable "X4" values))
	x5 (time (create-assumption-variable "X5" x5-values)))

  (setq l (list x1 x2 x3 x4 x5))
  (do ((l l (cdr l)))
      ((null (cdr l)))
    (dolist (xi (class-nodes (car l)))
      (dolist (xj (class-nodes (cadr l)))
	(cond ((<= (n-a-datum xj) (n-a-datum xi))
	       (contradictory-assumption-pair xi xj))
	      ((< (- (n-a-datum xj) (n-a-datum xi)) 10)
	       (contradictory-assumption-pair xi xj))
	      ((> (- (n-a-datum xj) (n-a-datum xi)) 175)
	       (contradictory-assumption-pair xi xj)))))
    (when (caddr l)
      (dolist (xi (class-nodes (car l)))
	(dolist (xj (class-nodes (caddr l)))
	  (if (< (- (n-a-datum xj) (n-a-datum xi)) 300)
	      (contradictory-assumption-pair xi xj))))))
;; Here is where we could use two-classes,
  ;; but we better not given the current consumer bugs.
  )

(defun simple-rolls1 (&aux x1 x2 x3 x4 x5 values l)
  (init-tms)
  (do ((i 900. (1- i)))
      ((= i 0))
    (push i values))
  (setq x1 (time (create-assumption-variable "X1" values))
	x2 (time (create-assumption-variable "X2" values))
	x3 (time (create-assumption-variable "X3" values))
	x4 (time (create-assumption-variable "X4" values))
	x5 (time (create-assumption-variable "X5" values)))
  (create-consumer X1 (list x1) nil)
  (create-consumer X5 (list x5) nil)
  (setq l (list x1 x2 x3 x4 x5))
  (dolist (x l)
    (create-consumer OBSTACLE1 (list x) nil)
    (create-consumer OBSTACLE2 (list x) nil))
  (do ((l l (cdr l)))
      ((null (cdr l)))
    (dolist (pos2 (cdr l))
      ;;; Can be much more efficient...
      (dolist (xi (class-nodes (car l)))
	(dolist (xj (class-nodes pos2))
	  (cond ((<= (n-a-datum xj) (n-a-datum xi))
		 (contradiction (list 'AFTER xi xj)))
		((< (- (n-a-datum xj) (n-a-datum xi)) 10)
		 (contradiction (list 'TOO-CLOSE xi xj)))

		((> (- (n-a-datum xj) (n-a-datum xi)) 175)
		 (contradiction (list 'TOO-FAR xi xj)))
		))))
    (dolist (pos2 (cddr l))
      (dolist (xi (class-nodes (car l)))
	(dolist (xj (class-nodes pos2))
	  (if (< (- (n-a-datum xj) (n-a-datum xi)) 300.)
	      (contradiction (list 'TWO-TOO-CLOSE xi xj)))))))
  ;; Here is where we could use two-classes,
  ;; but we better not given the current consumer bugs.
  )

(defun simple-rolls (&aux x1 x2 x3 x4 x5 values l)
  (init-tms)
  (do ((i 900. (1- i)))
      ((= i 0))
    (push i values))
  (setq x1 (time (create-assumption-variable "X1" values))
	x2 (time (create-assumption-variable "X2" values))
	x3 (time (create-assumption-variable "X3" values))
	x4 (time (create-assumption-variable "X4" values))
	x5 (time (create-assumption-variable "X5" values)))
  (create-consumer X1 (list x1) nil)
  (create-consumer X5 (list x5) nil)
  (setq l (list x1 x2 x3 x4 x5))
  (dolist (x l)
    (create-consumer OBSTACLE1 (list x) nil)
    (create-consumer OBSTACLE2 (list x) nil))
  (do ((l l (cdr l)))
      ((null (cdr l)))
    (dolist (pos2 (cdr l))
      (create-consumer IMMEDIATE-DIFFERENCE (list (car l) pos2) nil))
    (dolist (pos2 (cddr l))
      (create-consumer DIFFERENCE (list (car l) pos2) nil)))
  ;; Here is where we could use two-classes,
  ;; but we better not given the current consumer bugs.
  )

(defun freuder-1 ()
  (init-tms)
  (csp '((x1 a b)
	 (x2 e f)
	 (x3 c d g))
       '(((x1 x2) (b e) (b f))
	 ((x1 x3) (b c) (b d) (b g))
	 ((x2 x3) (e d) (f g))))
  ;; Need to repeat until done.
  (run)
  (process-queued-nogoods)
  (run)
  (mapc 'print-solution (env-interpretations))
  )

;;; This is the graph coloring problem from Freuder's paper.
(defun freuder-2 ()
  (init-tms)
  (csp '((n1 r g b)
	 (n2 r g b)
	 (n3 r g b))
       '(((n1 n2) (r g) (r b) (g r) (g b) (b r) (b g))
	 ((n2 n3) (r g) (r b) (g r) (g b) (b r) (b g))
	 ((n1 n3) (r g) (r b) (g r) (g b) (b r) (b g))))
  (run)
  (process-queued-nogoods)
  (run)
  (mapc 'print-solution (env-interpretations))
  )

;;; Four nodes, three colors
(defun freuder-3 ()
  (init-tms)
  (csp '((n1 r g b)
	 (n2 r g b)
	 (n3 r g b)
	 (n4 r g b))
       '(((n1 n2) (r g) (r b) (g r) (g b) (b r) (b g))
	 ((n2 n3) (r g) (r b) (g r) (g b) (b r) (b g))
	 ((n1 n3) (r g) (r b) (g r) (g b) (b r) (b g))
	 ((n1 n4) (r g) (r b) (g r) (g b) (b r) (b g))
	 ((n2 n4) (r g) (r b) (g r) (g b) (b r) (b g))
	 ((n3 n4) (r g) (r b) (g r) (g b) (b r) (b g))))
  (run)
  (process-queued-nogoods)
  (run)
  (mapc 'print-solution (env-interpretations))
  )

(defun csp-find-class (x) (or (find-class x) (error "Bad specification")))

;;; This is a brute force CSP converter.
(defun csp (variables constraints &aux cvars)
  (dolist (binding variables) (create-assumption-variable (car binding) (cdr binding)))
  (dolist (constraint constraints)
    (setq cvars nil)
    (dolist (var (car constraint)) (push (find-class var) cvars))
    (csp-recurse cvars nil nil (cdr constraint))))

(defun csp-recurse (cvars values nodes oks)
  (cond (cvars
	 (dolist (node (class-nodes (car cvars)))
	   (csp-recurse (cdr cvars) (cons (n-a-datum node) values) (cons node nodes) oks)))
	((member values oks :test #'equal))
	(t (justify-node *contra-node* (cons 'CONSTRAINT nodes)))))

(defconsumer next (node1 node2) ()
  (if (eq (n-a-datum node1) (n-a-datum node2)) (consumer-contradiction 'NEXT)))

;;; Counts start from 0.
(defun ib (colors topology &aux r (count 0))
  (init-tms)
  (dolist (next topology) (dolist (node next) (if (> node count) (setq count node))))
  (setq r (make-array count))
  (dotimes (i count) (setf (aref r i) (create-variable (format nil "R~D" i) colors)))
  (dolist (next topology)
    (create-consumer NEXT (list (aref r (1- (car next))) (aref r (1- (cadr next)))) nil))
  (run)		     
  (process-queued-nogoods)
  (print-statistics (interpretations))
  )

(defun ib-1 ()
  (ib '(b y r g)
      '((1 13) (1 2) (2 13) (2 4)
	(4 10) (6 10) (8 13) (6 13)
	(2 3) (3 4) (3 13) (3 5)
	(5 6) (5 13) (4 5) (5 10)
	(1 7) (7 13) (2 7) (4 7)
	(7 8) (4 9) (9 10) (8 9)
	(9 13) (6 11) (10 11) (11 13)
	(9 12) (11 12) (12 13))))


;;; A standard example.

(defvar *bad-color* nil)

;;; This stops at 212 arbitrarily.

;;; 3675, GC on, bits:
;;; 245 --- 572 seconds
;;; 212 --- 927 seconds

(defun test (&optional (end 212.) &aux start-time *going-nodes* last-time new)
  (unless *bad-color* (setq *bad-color* (generate-map-example)))
  (init-tms nil)
  (ensure-monitoring)
  (dolist (c *bad-color*) (encode-clause c) (run))
  (setq start-time (get-internal-run-time))
  (reset-meter T)
  (dolist (a *assumptions*)
    (setq last-time (get-internal-run-time))
    (print a)
    (setq new (assumption-env a))
    (meter T (update-node1 a (ncons new) (cons new (n-a-envs a))))
    (format T " Incremental time: ~D, Total time: ~D"
	    (time-taken last-time) (time-taken start-time))
;    (hash-statistics *env-hash-table*)
;    (maybe-rehash-env *env-hash-table*)
;    (hash-statistics *env-hash-table*)
    (if (= (assumption-unique a) end) (return))
    )
;  (meter-report T)
  (print-statistics nil))

;;; do (brain-dead1 (generate-map-example)) (brain-dead2)

;;; This does a brain-dead translation of a SAT problem into the ATMS.
;;; SAT problem is in standard RUP format.  There are many many other ways, but this
;;; works.
(defun brain-dead1 (l)
  (init-tms)
  (dolist (c l) (encode-clause c) (run))
;  (process-queued-nogoods)
  )

(defun brain-dead2  (&aux *going-nodes* new start-time last-time)
  (setq start-time (get-internal-run-time))
  (dolist (a *assumptions*)
    (setq last-time (get-internal-run-time))
    (print a)
    (setq new (assumption-env a))
    (update-node1 a (ncons new) (cons new (n-a-envs a)))
    (if (or *h4* *resolve-by-labeling*) (process-queued-nogoods))
    (format T " Incremental time: ~D, Total time: ~D"
	    (time-taken last-time) (time-taken start-time))
    )
  (print-statistics (interpretations)))

;;; This works only for some SAT problems.  It turns every positive
;;; clause into a one-of, the rest into justifications, if possible.  So
;;; this will fail on many SAT problems.  This encoding can be made more general
;;; but thats unecessary for Siskind's examples.
(defun encode-clause (c &aux true false antecedents)
  (dolist (lit c)
    (selectq (cdr lit)
      (:TRUE (push (car lit) true))
      (:FALSE (push (car lit) false))
      (t (error "Malformed clause"))))
  ;; Positive clauses become one-of disjunctions or we are dead.  Make sure they
  ;; don't yet exist.
  (cond ((null false)
	 (dolist (a true) (if (lookup-n-a a)
			      (error "Non unique literal in positive clause")))
	 (new-create-assumption-variable 'POSITIVE-CLAUSE true)
	 (dolist (a true) (setf (assumption-envs (lookup-n-a a)) nil)))
	((null true)
	 (dolist (f false) (push (or (lookup-n-a f) (create-node f)) antecedents))
	 (justify-node *contra-node* (cons 'NEGATIVE-CLAUSE antecedents)))
	((null (cdr true))
	 (dolist (f false) (push (or (lookup-n-a f) (create-node f)) antecedents))
	 (justify-node (or (lookup-n-a (car true)) (create-node (car true)))
		       (cons 'HORN-CLAUSE antecedents)))
	(t (error "Can't encode a clause with more than two positive literals"))))

;;; Inefficient.
(defun lookup-n-a (datum)
  (dolist (n *nodes*)
    (if (eq (n-a-datum n) datum) (return-from LOOKUP-N-A n)))
  (dolist (a *assumptions*)
    (if (eq (n-a-datum a) datum) (return-from LOOKUP-N-A a))))



;;; Here are three functions you can call to generate SAT problems
;;; for the three problems. Each returns a SAT problem which is
;;; a list of clauses (disjunctions). Each clause is a list of
;;; terms of the form (<foo> . :true) or (<foo> . :false) where
;;; the first means <foo> and the second means <foo> inverted.
;;; <foo> typically is a symbol whose print name is generated
;;; to have some reasonable meaning.
;;; To generate the SAT problem for the expensive map coloring
;;; problem, with complexity 12**31 use:
;;; (generate-map-example)
;;; To generate the SAT problem for the better map coloring
;;; problem with complexity 4**13 use:
;;; (generate-alternate-map-example)
;;; To generate the SAT problem for 8-queens use:
;;; (generate-n-queens-example 8)
;;; a generator for the map example

#+Symbolics
(defun generate-map-example ()
 (append
  (loop for i from 1 to 31
        collect
          (loop for j from 1 to 12
                collect (cons (intern (format nil "T-~D-~D" i j)) :true)))
  (loop for region in
            '(?r1 ?r2 ?r3 ?r4 ?r5 ?r6 ?r7 ?r8 ?r9 ?r10 ?r11 ?r12 ?r13)
        append (generate-map-example-sufur region))
  (generate-map-example-next  1 '?r1  '?r13)
  (generate-map-example-next  2 '?r1  '?r2)
  (generate-map-example-next  3 '?r2  '?r13)
  (generate-map-example-next  4 '?r2  '?r4)
  (generate-map-example-next  5 '?r4  '?r10)
  (generate-map-example-next  6 '?r6  '?r10)
  (generate-map-example-next  7 '?r8  '?r13)
  (generate-map-example-next  8 '?r6  '?r13)
  (generate-map-example-next  9 '?r2  '?r3)
  (generate-map-example-next 10 '?r3  '?r4)
  (generate-map-example-next 11 '?r3  '?r13)
  (generate-map-example-next 12 '?r3  '?r5)
  (generate-map-example-next 13 '?r5  '?r6)
  (generate-map-example-next 14 '?r5  '?r13)
  (generate-map-example-next 15 '?r4  '?r5)
  (generate-map-example-next 16 '?r5  '?r10)
  (generate-map-example-next 17 '?r1  '?r7)
  (generate-map-example-next 18 '?r7  '?r13)
  (generate-map-example-next 19 '?r2  '?r7)
  (generate-map-example-next 20 '?r4  '?r7)
  (generate-map-example-next 21 '?r7  '?r8)
  (generate-map-example-next 22 '?r4  '?r9)
  (generate-map-example-next 23 '?r9  '?r10)
  (generate-map-example-next 24 '?r8  '?r9)
  (generate-map-example-next 25 '?r9  '?r13)
  (generate-map-example-next 26 '?r6  '?r11)
  (generate-map-example-next 27 '?r10 '?r11)
  (generate-map-example-next 28 '?r11 '?r13)
  (generate-map-example-next 29 '?r9  '?r12)
  (generate-map-example-next 30 '?r11 '?r12)
  (generate-map-example-next 31 '?r12 '?r13)))

#+Symbolics
(defun generate-map-example-next (i region1 region2)
 (loop for j from 1
       for colors in '((blue yellow) (blue red)     (blue green)
                       (yellow blue) (yellow red)   (yellow green)
                       (red blue)    (red yellow)   (red green)
                       (green blue)  (green yellow) (green red))
       for color1 = (first colors)
       for color2 = (second colors)
       collect
         (list (cons (intern (format nil "T-~D-~D" i j)) :true)
               (cons (intern (format nil "~A=~A" region1 color1)) :false)
               (cons (intern (format nil "~A=~A" region2 color2)) :false))
       collect
         (list (cons (intern (format nil "T-~D-~D" i j)) :false)
               (cons (intern (format nil "~A=~A" region1 color1)) :true))
       collect
         (list (cons (intern (format nil "T-~D-~D" i j)) :false)
               (cons (intern (format nil "~A=~A" region2 color2)) :true))))

#+Symbolics
(defun generate-map-example-sufur (region)
 (loop for colors in '((blue yellow)
                       (blue red)
                       (blue green)
                       (yellow red)
                       (yellow green)
                       (red green))
       for color1 = (first colors)
       for color2 = (second colors)
       collect
         (list (cons (intern (format nil "~A=~A" region color1)) :false)
               (cons (intern (format nil "~A=~A" region color2)) :false))))

#+Symbolics
(defun generate-alternate-map-example-next (region1 region2)
 (loop for color in '(red blue yellow green)
       collect
         (list (cons (intern (format nil "~A=~A" region1 color)) :false)
               (cons (intern (format nil "~A=~A" region2 color)) :false))))

#+Symbolics
(defun generate-alternate-map-example-base (region)
 (loop for color in '(red blue yellow green)
       collect (cons (intern (format nil "~A=~A" region color)) :true)))

#+Symbolics
(defun generate-alternate-map-example ()
 (append
  (loop for region in
            '(?r1 ?r2 ?r3 ?r4 ?r5 ?r6 ?r7 ?r8 ?r9 ?r10 ?r11 ?r12 ?r13)
        collect (generate-alternate-map-example-base region))
  (loop for region in
            '(?r1 ?r2 ?r3 ?r4 ?r5 ?r6 ?r7 ?r8 ?r9 ?r10 ?r11 ?r12 ?r13)
        append (generate-map-example-sufur region))
  (generate-alternate-map-example-next '?r1  '?r13)
  (generate-alternate-map-example-next '?r1  '?r2)
  (generate-alternate-map-example-next '?r2  '?r13)
  (generate-alternate-map-example-next '?r2  '?r4)
  (generate-alternate-map-example-next '?r4  '?r10)
  (generate-alternate-map-example-next '?r6  '?r10)
  (generate-alternate-map-example-next '?r8  '?r13)
  (generate-alternate-map-example-next '?r6  '?r13)
  (generate-alternate-map-example-next '?r2  '?r3)
  (generate-alternate-map-example-next '?r3  '?r4)
  (generate-alternate-map-example-next '?r3  '?r13)
  (generate-alternate-map-example-next '?r3  '?r5)
  (generate-alternate-map-example-next '?r5  '?r6)
  (generate-alternate-map-example-next '?r5  '?r13)
  (generate-alternate-map-example-next '?r4  '?r5)
  (generate-alternate-map-example-next '?r5  '?r10)
  (generate-alternate-map-example-next '?r1  '?r7)
  (generate-alternate-map-example-next '?r7  '?r13)
  (generate-alternate-map-example-next '?r2  '?r7)
  (generate-alternate-map-example-next '?r4  '?r7)
  (generate-alternate-map-example-next '?r7  '?r8)
  (generate-alternate-map-example-next '?r4  '?r9)
  (generate-alternate-map-example-next '?r9  '?r10)
  (generate-alternate-map-example-next '?r8  '?r9)
  (generate-alternate-map-example-next '?r9  '?r13)
  (generate-alternate-map-example-next '?r6  '?r11)
  (generate-alternate-map-example-next '?r10 '?r11)
  (generate-alternate-map-example-next '?r11 '?r13)
  (generate-alternate-map-example-next '?r9  '?r12)
  (generate-alternate-map-example-next '?r11 '?r12)
  (generate-alternate-map-example-next '?r12 '?r13)))

;;; a generator for the n-queens example
;;; note: needs to have some redundant clauses removes

#+Symbolics
(defun generate-n-queens-example (n)
 (append
  (loop for i from 1 to n
        collect
          (loop for j from 1 to n
                collect (cons (intern (format nil "Q-~D-~D" i j)) :true)))
  (loop for i from 1 to n
        append
          (loop for j1 from 1 to n
                append
                  (loop for j2 from (+ j1 1) to n
                        collect
                          (list (cons (intern (format nil "Q-~D-~D" i j1))
                                      :false)
                                (cons (intern (format nil "Q-~D-~D" i j2))
                                      :false))
                        collect
                          (list (cons (intern (format nil "Q-~D-~D" j1 i))
                                      :false)
                                (cons (intern (format nil "Q-~D-~D" j2 i))
                                      :false))
                        when (<= j2 (- n i -1))
                          collect
                            (list
                             (cons
                              (intern (format nil "Q-~D-~D" (+ i j1 -1) j1))
                              :false)
                             (cons
                              (intern (format nil "Q-~D-~D" (+ i j2 -1) j2))
                              :false))
                        when (<= j2 (- n i -1))
                          collect
                            (list
                             (cons
                              (intern (format nil "Q-~D-~D" j1 (+ i j1 -1)))
                              :false)
                             (cons
                              (intern (format nil "Q-~D-~D" j2 (+ i j2 -1)))
                              :false))
                        when (<= j2 i)
                          collect
                            (list
                             (cons
                              (intern (format nil "Q-~D-~D" (- i j1 -1) j1))
                              :false)
                             (cons
                              (intern (format nil "Q-~D-~D" (- i j2 -1) j2))
                              :false))
                        when (<= j2 i)
                          collect
                            (list (cons (intern (format nil "Q-~D-~D"
                                                        (+ (- n i) j1)
                                                        (- n j1 -1)))
                                        :false)
                                  (cons (intern (format nil "Q-~D-~D"
                                                        (+ (- n i) j2)
                                                        (- n j2 -1)))
                                        :false)))))))


(defun natms-paper (&aux a b c)
  (setq *resolve-by-labeling* t)
  (init-tms)
  (setq a (create-assumption "A")
	b (create-assumption "B")
	c (create-assumption "C"))
  (choose (list a b) 'GIVEN)
  (justify-node *contra-node* (list 'GIVEN a c))
  (justify-node *contra-node* (list 'GIVEN b c))
  (run)
  (process-queued-nogoods)
  (print-envs (n-a-envs a))
  (print-envs (n-a-envs b))
  (print-envs (n-a-envs c)))