D,#TD1PsT[Begin using 006 escapes](1 0 (NIL 0) (NIL :ITALIC NIL) "CPTFONTI");;;-*-Mode:LISP;Syntax:COMMON-LISP;Package:(DALG :use CL :COLON-MODE :EXTERNAL);Base:10-*-
;;; Created 10/29/90 22:12:46 by shirley

;;;
;;; The D-algorithm in Lisp
;;;

;;; Notes:
;;; o I'm leaving out the code for marking a subset of the network as 
;;;   potentially observable (i.e., when only a few outputs are observed.  We
;;;   could put it back in later.
;;; o I'm changing it to use PDCF's (Primitive D-Cubes of Failure).
;;; o I'm removing behavior cubes (they weren't used anyway).
;;; o Change for-relevant-cubes to consider all of the assignments, not just the one
;;;   mentioned.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;			 Globals and Basic Utilities                       ;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

0(defvar (2 0 (NIL 0) (NIL :BOLD NIL) "CPTFONTCB")*VERBOSE-D-ALGORITHM*0 'nil)
(defvar 2*ADD-RANDOM-INPUTS*0 'nil)
(defvar 2*FAULTY-COMPONENT*0)			1;Communication between d-algorithm and constraint-propagation

0(defvar 2*PRIMARY-BACKTRACK-MAXIMUM*0 5)
(defvar 2*INTERNAL-BACKTRACK-MAXIMUM*0 500000)	1;0500000
(defvar 2*PRIMARY-BACKTRACK-COUNT*0)
(defvar 2*INTERNAL-BACKTRACK-COUNT*0)
(defvar 2*PROPAGATE-CONSTRAINTS-ON-PRIMARY-INPUT-ASSIGNMENTS*0 'T)
(defvar 2*PROPAGATE-CONSTRAINTS-ON-INTERNAL-ASSIGNMENTS*0 'T)
(defvar 2*ERROR-MESSAGE-ON-DEAD-ENDS*0 'nil)

(defun 2SENSITIVE-VALUE?0 (value)
  (and (symbolp value)
       (or (eq value 'D)
	   (eq value 'DB))))

(defun 2TRACE-DALG0 ()
  (trace CHOOSE-PDCF LINE-JUSTIFY-SET LINE-JUSTIFY PATH-SENSITIZE-SET PATH-SENSITIZE 
	 collect-test-vector))

(defun 2TRACE-DALG-INTERFACE0 ()
  (trace port-to-node type-bidirectional-ports type-input-ports type-output-ports
	 node-drives node-driven-by node-potentially-observable? primary-output?
	 primary-input? component-type circuit-nodes))

(defmacro 2DOWNWARD-CLOSURE0 (args &body body)
  `#'(lambda ,args (declare (sys:downward-function)) ,@body))

1;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;			Interface to the Network Model                     ;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

0(defun 2PORT-TO-NODE0 (component port-name)
  (atpg::port-to-node component port-name))

(defun 2TYPE-BIDIRECTIONAL-PORTS0 (type)
  (atpg:type-bidirectional-ports type))

(defun 2TYPE-INPUT-PORTS0 (type)
  (atpg:type-input-ports type))

(defun 2TYPE-OUTPUT-PORTS0 (type)
  (atpg:type-output-ports type))

(defun 2NODE-DRIVES0 (node)
  (atpg:node-drives node))

(defun 2NODE-DRIVEN-BY0 (node)
  (atpg:node-driven-by node))

1;;; I now have an implementation for this.
;0(defun 2NODE-POTENTIALLY-OBSERVABLE?0 (ignore) 't)
  
(defun 2PRIMARY-OUTPUT?0 (node)
  (atpg:node-primary-output? node))

(defun 2PRIMARY-INPUT?0 (node)
  (atpg:node-primary-input? node))

(defun 2COMPONENT-TYPE0 (component)
  (atpg:component-type component))

(defun 2CIRCUIT-NODES0 (&optional circuit)
  (if circuit
      (atpg:network-circuit-nodes circuit)
      (atpg:network-circuit-nodes)))

(defmacro 2NODE-CONSTANT-VALUE0 (ignore) nil)	1;Not implementing this

0(defun 2COERCE-TO-NETWORK-OBJECT0 (node-reference)
  (atpg:coerce-to-network-object node-reference))

(defun 2CIRCUIT-PRIMARY-OUTPUTS0 (circuit)
  (atpg:circuit-primary-outputs circuit))

(defmacro 2NODE-D-ASSIGNMENT0 (node)
  `(get (atpg:coerce-to-network-object ,node) 'd-assignment))

(defmacro 2CIRCUIT-LOOKUP0 (name circuit)
  `(atpg:circuit-lookup ,name ,circuit))

(defmacro 2INTERNAL-POTENTIALLY-OBSERVABLE?0 (node)
  `(get ,node 'potentially-observable))

(defmacro 2INTERNAL-POTENTIALLY-SENSITIVE?0 (node)
  `(get ,node 'potentially-sensitive))

1;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;			       Cube Abstraction                            ;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; A cube looks like (<all-assignments> <inputs> <outputs>) where all of
;;; <all-assignments>, <inputs> and <outputs> look like: ((port-name
;;; assignment) ...).  The purpose of <all-assignments> is to allow quick
;;; filtering of relevant cubes.
;;;

0(defmacro 2MAKE-CUBE0 (assignments inputs outputs) `(list ,assignments ,inputs ,outputs))
(defmacro 2CUBE-ASSIGNMENTS0 (cube) `(first ,cube))
(defmacro 2CUBE-INPUTS0 (cube) `(second ,cube))
(defmacro 2CUBE-OUTPUTS0 (cube) `(third ,cube))

(defmacro 2CUBE-ASSIGNMENT-PORT0 (cube) `(first ,cube))
(defmacro 2CUBE-ASSIGNMENT-VALUE0 (cube) `(second ,cube))

(defmacro 2GENERATION-CUBES0 (component-type) `(get ,component-type 'generation-cubes))
(defmacro 2PROPAGATION-CUBES0 (component-type) `(get ,component-type 'propagation-cubes))

(defun 2COMPONENT-PDCFS0 (component mode)
  (let ((result (cdr (assoc mode (generation-cubes (component-type component))))))
    (or result
	(error "Couldn't find primitive cubes of failure for ~s in mode ~s" component mode))))

(defun 2CUBE-ASSIGNMENT-NODE0 (component cube-assignment)
  (port-to-node component (cube-assignment-port cube-assignment)))

(defun 2PORT-VALUE-IN-CUBE0 (port cube)
  (cube-assignment-value (assoc port (cube-assignments cube))))

(defun 2DEFINE-GENERATION-CUBES0 (component-type mode-cubes-alist)
  (setf (generation-cubes component-type)
	(loop for (mode . cubes) in mode-cubes-alist
		  collect (cons mode (format-cubes component-type cubes)))))

(defun 2DEFINE-PROPAGATION-CUBES0 (component-type cubes)
  (setf (propagation-cubes component-type) (format-cubes component-type cubes)))

(defun 2FORMAT-CUBES0 (component-type cubes)
  (let ((input-ports (type-input-ports component-type))
	(output-ports (type-output-ports component-type))
	(bidirectional-ports (type-bidirectional-ports component-type)))
    1;; Validate the cubes
0    (loop for cube in cubes
	  do (dolist (assignment cube)
	       (unless (and (consp assignment)
			    (atom (first assignment))
			    (consp (rest assignment))
			    (atom (second assignment))
			    (null (rest (rest assignment))))
		 (format t "~&Malformed assignment: ~S~%" assignment))
	       (let ((port-name (cube-assignment-port assignment)))
		 (unless (or (member port-name input-ports)
			     (member port-name output-ports)
			     (member port-name bidirectional-ports))
		   (format t "~&Unknown port: ~S~%" port-name))))
      1;; Divide into inputs and outputs
0	  collect
	    (loop with inputs = '()
		  and outputs = '()
		  for assignment in cube
		  for port-name = (cube-assignment-port assignment)
		  do (cond ((member port-name input-ports) (push assignment inputs))
			   ((member port-name output-ports) (push assignment outputs))
			   ((member port-name bidirectional-ports) (push assignment inputs) (push assignment outputs)))
		  finally (return (make-cube cube inputs outputs))))))

1;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;		D contexts (environments of node assignments)              ;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

0(defvar 2*D-TRAIL*0)
(defvar 2*RESOURCE-OF-D-TRAILS*0 '())

(defun 2NEW-D-TRAIL0 ()
  (if (null *resource-of-d-trails*)
      (make-array '(100) :initial-element nil :fill-pointer 0)
      (scl:without-interrupts (pop *resource-of-d-trails*))))

1;;; It's bogus that this indirects through node-d-assignment in the interface.
;;; Oh well, it keeps the interface in one place.
0(defmacro 2D-ASSIGNMENT0 (node)
  `(node-d-assignment ,node))

1;;; Assume no NIL assignments.
0(defmacro 2D-ASSIGNED?0 (node)
  `(node-d-assignment ,node))

(defmacro 2WITH-D-CONTEXT0 (&body body)
  (let ((temporary (gensym)))
    `(labels ((,temporary () (progn (clear-d-context) ,@body)))
       (if (boundp '*d-trail*)
	   (,temporary)
	   (let* ((*d-trail* (new-d-trail)))
	     (unwind-protect 
		 (,temporary)
	       (scl:without-interrupts
		 (push *d-trail* *resource-of-d-trails*))))))))

(defmacro 2WITH-D-TRAIL0 (&body body)
  `(let ((d-mark (fill-pointer *d-trail*)))
     (prog1					1;unwind-protect
0       (progn ,@body)
       (d-unwind d-mark))))

(defun 2D-ASSIGN!0 (node value)
  (vector-push-extend node *d-trail*)		1;Pushed first
0  (vector-push-extend (d-assignment node) *d-trail*)	1;pushed second
0  (setf (d-assignment node) value))

(defun 2D-UNWIND0 (d-mark)
  (loop while (> (fill-pointer *d-trail*) d-mark)
	for old-value = (vector-pop *d-trail*)
	for old-node  = (vector-pop *d-trail*)
	doing (setf (d-assignment old-node) old-value)))

1;;; Assume NIL assignments mean no assignments.
0(defun 2CLEAR-D-CONTEXT0 ()
  (loop for node in (circuit-nodes)
	do (setf (d-assignment (coerce-to-network-object node)) nil)))

1;;; Input-Vector is a pair list
0(defun 2INITIALIZE-D-CONTEXT0 (&optional input-vector)
  1;; Setup constants
0  (dolist (node (circuit-nodes))
    (setq node (coerce-to-network-object node))
    (when (node-constant-value node)
      (d-assign! node (node-constant-value node))
      (unless (propagate-forward-constraints-consistently node)
	(error "Propagation error during initialization: node=~S" node))))
  (labels ((check-constraints (node)
	     (let ((flag nil))
	       (propagate-forward-constraints node (downward-closure () (setq flag t)))
	       flag)))
    (loop for assignment in input-vector
	  for node = (coerce-to-network-object (first assignment))
	  when (second assignment)
	    do (d-assign! node (second assignment))
	       (unless (check-constraints node)
		 (error "Propagation error during initialization: node=~S" node)))
    (setf (fill-pointer *d-trail*) 0)))

1;;;
;;; Hash table implementation
;;;

0;(defvar 2*D-CONTEXT*0)
;(defvar 2*D-TRAIL*0)
;(defvar 2*RESOURCE-OF-D-CONTEXTS*0 '())
;(defvar 2*RESOURCE-OF-D-TRAILS*0 '())
;
;(defun 2NEW-D-CONTEXT0 ()
;  (if (null *resource-of-d-contexts*)
;      (make-hash-table :test 'equal :size 50)	1;Should be the size of the circuit
0;      (scl:without-interrupts (pop *resource-of-d-contexts*))))
;
;(defun 2NEW-D-TRAIL0 ()
;  (if (null *resource-of-d-trails*)
;      (make-array '(100) :initial-element nil :fill-pointer 0)
;      (scl:without-interrupts (pop *resource-of-d-trails*))))
;
;(defmacro 2d-assignment0 (node)
;  `(gethash ,node *d-context*))
;
;(defmacro 2d-assigned?0 (node)
;  `(multiple-value-bind (ignore found)
;       (d-assignment ,node)
;     found))
;
;(defmacro 2with-d-context0 (&body body)
;  (let ((temporary (gensym)))
;    `(labels ((,temporary () ,@body))
;       (if (boundp '*d-context*)
;	   (,temporary)
;	   (let* ((*d-context* (new-d-context))
;		  (*d-trail* (new-d-trail)))
;	     (unwind-protect 
;		 (,temporary)
;	       (scl:without-interrupts
;		 (push *d-context* *resource-of-d-contexts*)
;		 (push *d-trail* *resource-of-d-trails*))))))))
;
;(defmacro 2with-d-trail0 (&body body)
;  `(let ((d-mark (fill-pointer *d-trail*)))
;     (prog1					1;unwind-protect
0;       (progn ,@body)
;       (d-unwind d-mark))))
;
;(defun 2D-ASSIGN!0 (node value)
;  (vector-push-extend node *d-trail*)		1;Pushed first
0;  (vector-push-extend (d-assignment node) *d-trail*)	1;pushed second
0;  (setf (d-assignment node) value))
;
;(defun 2D-UNWIND0 (d-mark)
;  (loop while (> (fill-pointer *d-trail*) d-mark)
;	for old-value = (vector-pop *d-trail*)
;	for old-node  = (vector-pop *d-trail*)
;	doing (setf (d-assignment old-node) old-value)))
;
;1;;; Input-Vector is a pair list
0;(defun 2INITIALIZE-D-CONTEXT0 (&optional input-vector)
;  (clrhash *d-context*)
;  1;; Setup constants
0;  (dolist (node (circuit-nodes))
;    (setq node (coerce-to-network-object node))
;    (when (node-constant-value node)
;      (d-assign! node (node-constant-value node))
;      (unless (propagate-forward-constraints-consistently node)
;	(error "Propagation error during initialization: node=~S" node))))
;  (labels ((check-constraints (node)
;	     (let ((flag nil))
;	       (propagate-forward-constraints node #'(lambda () (setq flag t)))
;	       flag)))
;    (loop for assignment in input-vector
;	  for node = (coerce-to-network-object (first assignment))
;	  when (second assignment)
;	    do (d-assign! node (second assignment))
;	       (unless (check-constraints node)
;		 (error "Propagation error during initialization: node=~S" node)))
;    (setf (fill-pointer *d-trail*) 0)))
;
;(defun 2DESCRIBE-D-CONTEXT0 ()
;  (format t "~&D Context:~%")
;  (maphash #'(lambda (key value)
;	       (when (not (null value))
;		 (print (list key value))))
;	   *d-context*))

1;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;			       Backtrack Cutoff                            ;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;; Return values test-vector and backtrack-cutoff?
0(defmacro 2WITH-BACKTRACK-CUTOFF0 ((&key (primary '*primary-backtrack-maximum*) (internal '*internal-backtrack-maximum*))
				 &body body)
  `(let ((*primary-backtrack-count* 0)
	 (*primary-backtrack-maximum* ,primary)
	 (*internal-backtrack-count* 0)
	 (*internal-backtrack-maximum* ,internal))
     (catch 'BACKTRACK-CUTOFF ,@body)))

(defun 2HANDLE-PRIMARY-BACKTRACK-CUTOFF0 ()
  (when (> (incf *primary-backtrack-count*) *primary-backtrack-maximum*)
    (tv:beep)
    (format t "(2primary backtrack cutoff0 at ~d) " *primary-backtrack-maximum*)
    (throw 'BACKTRACK-CUTOFF nil)))

(defun 2HANDLE-INTERNAL-BACKTRACK-CUTOFF0 ()
  (when (> (incf *internal-backtrack-count*) *internal-backtrack-maximum*)
    (tv:beep)
    (format t "(2internal backtrack cutoff0 at ~d) " *internal-backtrack-maximum*)
    (throw 'BACKTRACK-CUTOFF 'backtrack-cutoff)))

1;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;		      Mark potentially observable nodes                    ;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; This is useful if only a subset of the network is actually observable.  It
;;; just walks backwards through the network marking nodes that that can
;;; possibly effect one of the outputs.
;;;

0(defvar 2*POTENTIALLY-OBSERVABLE-TIMESTAMP*0 0)

(defun 2MARK-POTENTIALLY-OBSERVABLE-NODES0 (circuit &optional (observable-outputs (circuit-primary-outputs circuit)))
  (unless (equal observable-outputs (circuit-lookup :potentially-observervable-node-spec circuit))
    (incf *potentially-observable-timestamp*)
    (format t "~&Marking the 2POTENTIALLY0 2OBSERVABLE0 2NODES0 ...")
    (labels ((internal (node)
	       (unless (eql *potentially-observable-timestamp* (internal-potentially-observable? node))
		 (setf (internal-potentially-observable? node) *potentially-observable-timestamp*)
		 (unless (primary-input? node)
		   (loop with component = (first (first (node-driven-by node)))
			 for input-port in (type-input-ports (component-type component))
			 for input-node = (port-to-node component input-port)
			 do (internal input-node))))))
      (dolist (output observable-outputs)
	(internal (coerce-to-network-object output))))
    (setf (circuit-lookup :potentially-observervable-node-spec circuit) observable-outputs)
    (format t "done~%")
    observable-outputs))

(defun 2NODE-POTENTIALLY-OBSERVABLE?0 (node)
  (unless (atpg:network-object? node)
    (error "node isn't a network object"))
  (eql *potentially-observable-timestamp* (internal-potentially-observable? node)))

1;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;		       Mark potentially sensitive nodes                    ;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; This is a kludge.  I should have done a Podem in the first place.  Anyway,
;;; There's a problem in choosing any D-Cube to use - sensitive values can
;;; easily get propagated back to primary inputs, where they are cut off
;;; there.  This code implements an earlier filter.  First it marks every node
;;; that is potentially driven by the component under test.  Then, only those
;;; are allowed to hold sensitive values.  The filter will appear in
;;; FOR-RELEVENT-CUBES.
;;;

0(defvar 2*POTENTIALLY-SENSITIVE-TIMESTAMP*0 0)

(defun 2MARK-POTENTIALLY-SENSITIVE-NODES0 (circuit component)
  (unless (equal component (circuit-lookup :potentially-sensitive-from-component circuit))
    (incf *potentially-sensitive-timestamp*)
    (format t "~&Marking the 2POTENTIALLY0 2SENSITIVE0 2NODES0 ...")
    (labels ((internal (node)
	       (unless (eql *potentially-sensitive-timestamp* (internal-potentially-sensitive? node))
		 (setf (internal-potentially-sensitive? node) *potentially-sensitive-timestamp*)
		 (unless (primary-output? node)
		   (loop for (component) in (node-drives node) do
		     (loop for output-port in (type-output-ports (component-type component))
			   for output-node = (port-to-node component output-port)
			   do (internal output-node)))))))
      (loop for output-port in (type-output-ports (component-type component))
	    for node = (port-to-node component output-port)
	    do (internal (coerce-to-network-object node))))
    (setf (circuit-lookup :potentially-sensitive-from-component circuit) component)
    (format t "done~%")))

(defun 2NODE-POTENTIALLY-SENSITIVE?0 (node)
  (unless (atpg:network-object? node)
    (error "node isn't a network object"))
  (eql *potentially-sensitive-timestamp* (internal-potentially-sensitive? node)))

1;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;				 Main Entries                              ;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;; Return 'BACKTRACK-CUTOFF if that's what happened
;;; Input-Vector is a pair list (and can contain assignments for internal nodes too).
0(defun 2D-ALGORITHM0 (circuit *faulty-component* faulty-mode &optional input-vector)
  (atpg:with-circuit circuit			1;Flush this.
0    (mark-potentially-observable-nodes circuit)
    (mark-potentially-sensitive-nodes circuit *faulty-component*)
    (with-d-context
      (initialize-d-context input-vector)
      (catch 'D-ALGORITHM
	(with-backtrack-cutoff ()
1;0	  (format t "~&internal=~s, primary=~s~%" *internal-backtrack-maximum* *primary-backtrack-maximum*)
	  (choose-pdcf
	    *faulty-component*
	    faulty-mode
	    (downward-closure ()
1;0	      (print (collect-test-vector))
	      (throw 'D-ALGORITHM (collect-test-vector))
1;0	      (incf *count*)
	      )))))))

(defun 2CHOOSE-PDCF0 (component faulty-mode cont)
  (declare (sys:downward-funarg cont))
  (dolist (cube (component-pdcfs component faulty-mode))
    (with-d-trail
      (line-justify-set
	component (cube-inputs cube)
	(downward-closure ()
	  (path-sensitize-set
	    component (cube-outputs cube)
	    cont))))))

1;;; Justify all from the set (this is different from PATH-SENSITIZE-SET)
0(defun 2LINE-JUSTIFY-SET0 (component assignments continuation)
  (declare (sys:downward-funarg continuation))
  (if (null assignments)
      (funcall continuation)
      (line-justify
	(cube-assignment-node component (first assignments))
	(cube-assignment-value (first assignments))
	(downward-closure ()
	  (line-justify-set component (rest assignments) continuation)))))

(defun 2LINE-JUSTIFY0 (node value continuation)
  (declare (sys:downward-funarg continuation))
  (cond ((equal-assignment? value (d-assignment node))
	 (funcall continuation))
	((new-assignment? value (d-assignment node))
	 (d-assign! node value)
	 (cond ((primary-input? node)
		(cond ((sensitive-value? value) nil)
		      (*propagate-constraints-on-primary-input-assignments*
		       (propagate-forward-constraints node continuation))
		      (t
		       (funcall continuation)
		       (handle-primary-backtrack-cutoff)
		       )))
	       ((null (node-driven-by node))
		(if (node-constant-value node)
		    (error "Shouldn't get here")
		    (when *error-message-on-dead-ends*
		      (error "~s isn't a primary input, but still isn't driven by anything" node))))
	       (t
		(labels ((continue (continuation)
			   (loop for (component driving-port) in (node-driven-by node) doing
			     (for-relevant-cubes
			       component driving-port value
			       (downward-closure (cube)
				 (line-justify-set component (cube-inputs cube) continuation))))))
		  (if *propagate-constraints-on-internal-assignments*
		      (propagate-forward-constraints node (downward-closure () (continue continuation)))
		      (continue continuation))))))
	(t (handle-internal-backtrack-cutoff))))

1;;; Sensitize one from the set (this is different from LINE-JUSTIFY-SET)
0(defun 2PATH-SENSITIZE-SET0 (component assignments continuation)
  (declare (sys:downward-funarg continuation))
  (if (null assignments)
      (funcall continuation)
      (dolist (assignment assignments)
	(let ((value (cube-assignment-value assignment)))
	  (when (sensitive-value? value)
	    (with-d-trail
	      (path-sensitize (cube-assignment-node component assignment) value continuation)))))))

(defun 2PATH-SENSITIZE0 (node value continuation)
  (cond ((not (node-potentially-observable? node)))
	((not (compatable-assignment? value (d-assignment node))))
	(t
	 (d-assign! node value)
	 (cond ((primary-output? node)
		(funcall continuation))
	       ((null (node-drives node))
		(when *error-message-on-dead-ends*
		  (error "~s isn't a primary output, but still doesn't drive anything" node))
		(handle-internal-backtrack-cutoff))
	       (t
		(loop for (component driven-port) in (node-drives node) doing
		  (for-relevant-cubes
		    component driven-port value
		    (downward-closure (cube)
			(line-justify-set
			  component (cube-inputs cube)
			  (downward-closure ()
			      (path-sensitize-set component (cube-outputs cube) continuation)))))))))))

(defun 2NEW-ASSIGNMENT?0 (ignore old)
  (null old))

(defun 2EQUAL-ASSIGNMENT?0 (new old)
  (eql new old))

(defun 2COMPATABLE-ASSIGNMENT?0 (new old)
  (or (null old) (null new) (eq new old)))

;(defun 2FOR-RELEVANT-CUBES0 (component port value continuation)
;  (declare (sys:downward-funarg continuation))
;  (let ((the-cubes (propagation-cubes (component-type component))))
;    (if (null the-cubes)
;	(error "no cubes for component ~s which is a ~s" component (component-type component))
;	(loop for cube in the-cubes
;	      when (equal-assignment? value (port-value-in-cube port cube))
;		do (with-d-trail
;		     (funcall continuation cube))))))

(defun 2FOR-RELEVANT-CUBES0 (component port value continuation)
  (declare (sys:downward-funarg continuation))
  (let ((the-cubes (propagation-cubes (component-type component))))
    (if (null the-cubes)
	(error "no cubes for component ~s which is a ~s" component (component-type component))
	(loop for cube in the-cubes do
	  (when (equal-assignment? value (port-value-in-cube port cube))
	    (if (and (compatible-cube cube component)
		     (check-sensitivities cube component))
		(with-d-trail
		  (funcall continuation cube))
		(handle-internal-backtrack-cutoff)))))))

(defun 2COMPATIBLE-CUBE0 (cube component)
  (loop for (port value) in (cube-assignments cube)
	for current-value = (d-assignment (port-to-node component port))
	always (compatable-assignment? value current-value)))

(defun 2CHECK-SENSITIVITIES0 (cube component)
  (loop for (port value) in (cube-assignments cube)
	always (or (not (sensitive-value? value))
		   (node-potentially-sensitive? (port-to-node component port)))))

1;;; Note: there was a COERCE-TO-NETWORK-OBJECT in here, which I think was unnecessary
0(defun 2COLLECT-TEST-VECTOR0 ()
  (loop for node in (circuit-nodes)
	for value = (cond ((primary-output? node)
			   (d-assignment node))
			  ((not (primary-input? node))
			   nil)
			  ((filter-sensitive-values (d-assignment node)))
			  (*add-random-inputs*
			   (random 2)))
	when value
	  collect (list node value)))

1;;; If a D or DB appears on a primary input (which happens when generating
;;; a test explicitly for an input), then convert it to the good boolean value.
0(defun 2FILTER-SENSITIVE-VALUES0 (value)
  (cond ((eql value 'D) 1)
	((eql value 'DB) 0)
	(t value)))

1;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;			    Constraint Propagation                         ;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;; Reducing consing
0(defvar 2*CONSTRAINT-PROPAGATION-QUEUE*0 (make-array '(100) :initial-element nil :fill-pointer 0))

1;;; Call the continuation if all of the propagation works out.  Don't want a 0with-d-trail1 here.  All assignments
;;; last longer than this function invocation and go away with the containing 0with-d-trail1.
0(defun 2PROPAGATE-FORWARD-CONSTRAINTS0 (node continuation)
  (declare (sys:downward-funarg continuation))
  (setf (fill-pointer *constraint-propagation-queue*) 0)
  (dolist (component (node-drives node)) (vector-push-extend component *constraint-propagation-queue*))
  (unless (loop named loop
		with trail = 0
		while (< trail (fill-pointer *constraint-propagation-queue*))
		for (component) = (prog1 (aref *constraint-propagation-queue* trail) (incf trail))
		for gate-output = (run-forward-propagation-rule component)
		when gate-output
		  do (let* ((output-node (port-to-node component (first (type-output-ports (component-type component)))))
			    (previous-value (d-assignment output-node)))
		       (cond ((null previous-value)
			      (d-assign! output-node gate-output)
			      (dolist (component (node-drives output-node))
				(vector-push-extend component *constraint-propagation-queue*)))
			     ((eql previous-value gate-output))
			     ((eql component *faulty-component*))	1;Do nothing
0			     (t (return-from loop 't)))))
    1;; Unless propagation turned up a contradiction, continue with test generation
0    (funcall continuation)))

(defun 2RUN-FORWARD-PROPAGATION-RULE0 (component)
  (let ((rule (get (component-type component) 'forward-propagation-rule)))
    (when rule (format t "~&Running forward rule for ~s~%" component))
    (when rule (funcall rule component))))

(defun 2ERASE-FORWARD-CONSTRAINTS0 (node)
  (setf (fill-pointer *constraint-propagation-queue*) 0)
  (dolist (component (node-drives node)) (vector-push-extend component *constraint-propagation-queue*))
  (unless (loop named loop
		with trail = 0
		while (< trail (fill-pointer *constraint-propagation-queue*))
		for (component) = (prog1 (aref *constraint-propagation-queue* trail) (incf trail))
		do (let ((output-node (port-to-node component (first (type-output-ports (component-type component))))))
		     (d-assign! output-node nil)
		     (dolist (component (node-drives output-node))
		       (vector-push-extend component *constraint-propagation-queue*))))))

1;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;		       D Cubes for Primitive Components                    ;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

0(defun 2CREATE-D-PROPAGATION-CUBES0 (input-names output-name func)
  (let ((rules '()))
  (labels ((printer (inputs)
	     (let ((good (apply func (mapcar #'coerce-good inputs)))
		   (bad (apply func (mapcar #'coerce-bad inputs))))
	       (push (nconc (loop for name in input-names
				  for val in inputs
				  collect (list name val))
			    (list (list output-name 
					(cond ((eql good bad) good)
					      ((eql good 1)   'D)
					      ((eql good 0)   'DB)
					      (t (error "shouldn't get here"))))))
		     rules)))
	   (iterator (n inputs)
	     (if (zerop n)
		 (printer inputs)
		 (dolist (i '(0 1 d db))
		   (iterator (- n 1) (cons i inputs))))))
    (iterator (length input-names) '())
    (nreverse rules))))

(defun 2COERCE-GOOD0 (val)
  (cond ((eql val 1) 1)
	((eql val 0) 0)
	((eql val 'D) 1)
	((eql val 'DB) 0)
	(t (error "shouldn't get here"))))

(defun 2COERCE-BAD0 (val)
  (cond ((eql val 1) 1)
	((eql val 0) 0)
	((eql val 'D) 0)
	((eql val 'DB) 1)
	(t (error "shouldn't get here"))))

1;;;
;;; Gate Definitions
;;;

0d-alg:
(dalg:define-propagation-cubes
2  'BUF
0  (dalg:create-d-propagation-cubes
    '(in)
    'out
    #'(lambda (in) in)))

d-alg:
(dalg:define-generation-cubes
  2'BUF
0  '((S0 ((in 1) (out dalg:d)))
    (S1 ((in 0) (out dalg:db)))))

d-alg:
(dalg:define-propagation-cubes
2  'NOT
0  (dalg:create-d-propagation-cubes
    '(in)
    'out
    #'(lambda (in) (- 1 in))))

d-alg:
(dalg:define-generation-cubes
  2'NOT
0  '((S0 ((in 0) (out dalg:d)))
    (S1 ((in 1) (out dalg:db)))))

d-alg:
(dalg:define-propagation-cubes
2  'AND2
0  (dalg:create-d-propagation-cubes
    '(in-1 in-2)
    'out
    #'(lambda (in-1 in-2)
	(cond ((eql in-1 0) 0)
	      ((eql in-2 0) 0)
	      ((eql in-1 1) in-2)
	      ((eql in-2 1) in-1)))))

d-alg:
(dalg:define-generation-cubes
  2'AND2
0  '((S0 ((in-1 1) (in-2 1) (out dalg:d)))
    (S1 ((in-1 0) (out dalg:db))
	((in-2 0) (out dalg:db)))))

d-alg:
(dalg:define-propagation-cubes
2  'NAND2
0  (dalg:create-d-propagation-cubes
    '(in-1 in-2)
    'out
    #'(lambda (in-1 in-2)
	(- 1 (cond ((eql in-1 0) 0)
		   ((eql in-2 0) 0)
		   ((eql in-1 1) in-2)
		   ((eql in-2 1) in-1))))))

d-alg:
(dalg:define-generation-cubes
  2'NAND2
0  '((S0 ((in-1 0) (out dalg:d))
	((in-2 0) (out dalg:d)))
    (S1 ((in-1 1) (in-2 1) (out dalg:db)))))

d-alg:
(dalg:define-propagation-cubes
2  'OR2
0  (dalg:create-d-propagation-cubes
    '(in-1 in-2)
    'out
    #'(lambda (in-1 in-2)
	(cond ((eql in-1 1) 1)
	      ((eql in-2 1) 1)
	      ((eql in-1 0) in-2)
	      ((eql in-2 0) in-1)))))

d-alg:
(dalg:define-generation-cubes
  2'OR2
0  '((S0 ((in-1 1) (out dalg:d))
	((in-2 1) (out dalg:d)))
    (S1 ((in-1 0) (in-2 0) (out dalg:db)))))

d-alg:
(dalg:define-propagation-cubes
2  'NOR2
0  (dalg:create-d-propagation-cubes
    '(in-1 in-2)
    'out
    #'(lambda (in-1 in-2)
	(- 1 (cond ((eql in-1 1) 1)
		   ((eql in-2 1) 1)
		   ((eql in-1 0) in-2)
		   ((eql in-2 0) in-1))))))

d-alg:
(dalg:define-generation-cubes
  2'NOR2
0  '((S0 ((in-1 0) (in-2 0) (out dalg:db)))
    (S1 ((in-1 1) (out dalg:d))
	((in-2 1) (out dalg:d)))))

d-alg:
(dalg:define-propagation-cubes
2  'XOR2
0  (dalg:create-d-propagation-cubes
    '(in-1 in-2)
    'out
    #'(lambda (in-1 in-2)
	(if (eql in-1 0)
	    in-2
	    (- 1 in-2)))))

d-alg:
(dalg:define-generation-cubes
  2'XOR2
0  '((S0 ((in-1 0) (in-2 1) (out dalg:d))
	((in-1 1) (in-2 0) (out dalg:d)))
    (S1 ((in-1 0) (in-2 0) (out dalg:db))
	((in-1 1) (in-2 1) (out dalg:db)))))