;-*- Mode:  LISP; Syntax: Common-lisp -*-

;;;; Assumption-based Truth Maintenance System
;;
;; Copyright (C) 1987, Kenneth D. Forbus, All rights reserved.
;; Please see attached conditions of use.
;;
;; Very simple version of de Kleer's ATMS. There are literally dozens of
;; optimizations that can be made to this code.  The virtues of this version
;; is (a) it is much smaller than de Kleer's "industrial grade" version and
;; (b) it runs in Gold Hill's GClispLM on IBM AT's as well as Symbolics machines.

(defstruct (tms-node :named
	    (:print-function (lambda (n st ignore)
		(format st "<TMS node ~D>" (tms-node-index n)))))
	   (index 0)        ; Unique name
	   (datum nil)      ; Pointer to PS data structures
	   (status ':OUT)   ; :IN if non-empty label, :OUT otherwise
	   (label nil)      ; minimal environments this node is believed in
	   (justifications nil) (consequences nil)
	   (rules nil)	     ; Will be run when there is a non-empty label.
	   (plist nil))     ; For markers and other things
			   
(defstruct (justification :named (:print-function
	      (lambda (j st ignore)
		(format st "<~A ~D>" (justification-type j)
			(justification-index j)))))
	   (index 0) (type nil)
	   (consequence nil)
	   (antecedents nil))

(defstruct (assumption :named
            (:print-function (lambda (a st ignore)
		(format st "A-~D" (assumption-index a))))
	    (:predicate assumption?))
	   (index 0) (datum nil)
	   (environments nil))

(defstruct (environment :named
	    (:print-function (lambda (e st ignore)
		(format st "E-~D" (environment-index e)))))
	   (index 0) (n-assumptions 0)
	   (assumptions nil)
	   (nodes nil)
	   (contradictory? nil))

;;;; Globals and initialization

(proclaim '(special *debug-tms* *node-counter* *justification-counter*
		    *assumption-counter* *environment-counter* *node*
		    *contra-node* *justification* *assumption*
		    *envirionment* *env-table* *nogood-table* *node-queue*
		    *empty-env* *tms-node-printer*))

(defvar *debug* nil) ;; system-level information
(defvar *debug-tms* nil) ;; tms details
(defvar *node-counter* 0) ;; Some counters
(defvar *justification-counter* 0)
(defvar *assumption-counter* 0)
(defvar *environment-counter* 0)
(defvar *node* nil) ;;Index variables
(defvar *justification* nil)
(defvar *assumption* nil)
(defvar *environment* nil)
(defvar *env-table* nil)
(defvar *nogood-table* nil)
(defvar *node-queue* nil)

(defun atms-init ()
  (setq *env-table* nil *nogood-table* nil *node-queue* nil)
  (setq *node-counter* 0 *justification-counter* 0
	*assumption-counter* 0 *environment-counter* 0)
  (setq *node* nil
	*justification* nil
	*environment* nil
	*assumption* nil)
  (setq *tms-node-printer* #'(lambda (n) (tms-node-datum n)))
  (setq *contra-node* (build-tms-node "The Contradiction")
	*empty-env* (build-environment nil)))

(defun assumption-order (a1 a2)
  (< (assumption-index a1) (assumption-index a2)))

(defun env-order (e1 e2)
  (< (environment-index e1) (environment-index e2)))

;;;; Constructors
;; None of these functions should be called by the user, only
;; by other ATMS programs.  The user-interface hooks are at the
;; end of the file.

(defun build-assumption (datum &aux a)
  (setq a (make-assumption :datum datum :index (incf *assumption-counter*)))
  (setf (getf (tms-node-plist datum) ':Assumption) a)
  (push a *assumption*)
  a)

(defun build-environment (assumptions &aux e)
  (setq e (make-environment :index (incf *environment-counter*)
			    :assumptions assumptions
		            :n-assumptions (length assumptions)))
  (dolist (a assumptions) (push e (assumption-environments a))) 
  (insert-env-in-table e) (push e *environment*)
  e)

(defun build-tms-node (datum &aux n)
  (setq n (make-tms-node :index (incf *node-counter*) :datum datum))
  (push n *node*)
  n)

(defun build-justification (type consequent antecedents &aux j)
  (if *debug-tms* (format t "~%Justifying ~A in terms of ~A on ~A"
			  (funcall *tms-node-printer* consequent) type antecedents))
  (setq j (make-justification :index (incf *node-counter*) :type type
			      :consequence consequent
			      :antecedents antecedents))
  (push j (tms-node-justifications consequent))
  (dolist (ante antecedents)
    (unless (assumption? ante)
      (push j (tms-node-consequences ante)))) 
  (push j *justification*)
  (cond ((eq consequent *contra-node*) (update-nogood j))
	(t (update-node consequent)))
  j)

(defmacro ordered-push (item list test)
  `(setq ,list (ordered-insert ,item ,list ,test)))

(defun ordered-insert (item list test)
  (cond ((null list) (list item))
	((funcall test item (car list)) (cons item list))
	((eq item (car list)) list) 
	(t (cons (car list) (ordered-insert item (cdr list) test)))))

;;;; Updating labels
;; This occurs whenever a justification is added.  If the node being
;; justified has new environments as a consequence, propagation must occur.

(defun update-node (the-node)
  (declare (special *node-queue*))
  (do ((queue (cond (the-node (cons the-node *node-queue*)) (t *node-queue*))
	      (append (cdr queue) *node-queue*))
       (node nil) (new-envs? nil nil)
       (*node-queue* nil nil)
       (counter 0 (1+ counter))) ; for debugging
      ((null queue) counter)
    (setq node (car queue) new-envs? (update-label node))
    (when new-envs?
      (dolist (j (tms-node-consequences node))
	(cond ((eq (justification-consequence j) *contra-node*) (update-nogood j))
	      (t (push (justification-consequence j) *node-queue*)))))))

(defun update-label (node &aux new-envs)
  ;; Simple version -- recompute the label from scratch, and
  ;; compare it against the old label.  Return T if different.
  (if *debug-tms* (format t "~%   Updating label of ~A.."
			  (funcall *tms-node-printer* node)))
  (unless (and (null (cdr (tms-node-label node))) ;skip premises
		(eq (car (tms-node-label node)) *empty-env*))
  (dolist (just (tms-node-justifications node))
    (dolist (penv (compute-justification-envs just))
    (cond ((some #'(lambda (e) (env-subsumed? penv e)) new-envs))
	  ((env-contradictory? penv))
	  (t (dolist (oenv new-envs)
	       (if (env-subsumed? oenv penv) ;subsumes a known one?
		   (setq new-envs (remove oenv new-envs))))
	     (ordered-push penv new-envs #'env-order)))))
    (cond ((equal (tms-node-label node) new-envs) nil)
	  (t (dolist (oenv (tms-node-label node))
	       (unless (member oenv new-envs)
		 (setf (environment-nodes oenv)
		       (delete node (environment-nodes oenv)))))
	     (dolist (nenv new-envs)
	       (unless (member nenv (tms-node-label node))
		 (push node (environment-nodes nenv))))
	     (setf (tms-node-label node) new-envs)
	     (cond (new-envs 
		    (setf (tms-node-status node) ':IN)
		    (dolist (rule (tms-node-rules node))
		      (enqueue rule)))
		   (t (setf (tms-node-status node) ':OUT)))
	     t))))

;;;; Computing environments for a justification
;;

(defun compute-justification-envs (just &aux input-assumptions
					     input-envs
					      base-env)
  ;; Figures out the environments for the consequence of a justification
  ;; by combining the environments of the antecedents.
  (dolist (ante (justification-antecedents just))
    (cond ((assumption? ante) (push ante input-assumptions))
	  (t (push (tms-node-label ante) input-envs))))
  (unless (and input-assumptions
	       (null (setq base-env (make-env-from-assumptions
				      input-assumptions))))
    (generate-env-cross-product (if base-env base-env *empty-env*)
				      input-envs)))

(defun generate-env-cross-product (base-env env-choices)
  (let ((*env-product* nil))
    (labels ((generate-env-cross-product1 (base-env env-choices &aux nenv)
	      (cond ((null env-choices)
		     (unless (or (some #'(lambda (e)
					   (env-subsumed? base-env e))
				       *env-product*)
				 (env-contradictory? base-env))
		       (dolist (e *env-product*)
			 (if (env-subsumed? e base-env)
			     (setq *env-product* (delete e *env-product*))))
		       (pushnew base-env *env-product*)))
		    (t (dolist (env (car env-choices))
			 (setq nenv (append-envs env base-env))
			 (when nenv
			   (generate-env-cross-product1 nenv
				(cdr env-choices))))))))
    (generate-env-cross-product1 base-env env-choices)
    *env-product*)))

;;; Constructing new envs from assumptions and old envs
;;
;; All of these functions return NIL if the env that is created
;; is contradictory.

(defun make-env-from-assumptions (assumptions
				   &optional (base-env *empty-env*)
				   &aux nenv)
  (setq nenv base-env)
  (dolist (assume assumptions)
    (setq nenv (cons-env assume nenv))
    (if (null nenv) (return nil)))
  nenv)

(defun append-envs (e1 e2)
  (when (> (environment-n-assumptions e1) (environment-n-assumptions e2))
    (psetq e1 e2 e2 e1))
  (make-env-from-assumptions (environment-assumptions e1) e2))

(defun cons-env (assumption env &aux nassumes oenv)
  (setq nassumes (ordered-insert assumption
				       (environment-assumptions env)
				       #'assumption-order))
  (setq oenv (lookup-env nassumes))
  (cond (oenv (unless (environment-contradictory? oenv) oenv))
	(t (setq oenv (build-environment nassumes))
	   (unless (env-contradictory? oenv) oenv))))

;;;; Indexing envs
;; Keep them in tables sorted by length to simplify global searches.
;; These happen in two places: If a new nogood is being added, must test
;; smaller nogoods to see if subsumed.  If the new nogood is okay, must
;; test all environments larger than it to see if they subsume it, and
;; hence should be wiped out.

(defun insert-env-in-table (env &aux index entry)
  (setq index (environment-n-assumptions env)
	entry (assoc index *env-table* :test #'=))
  (cond (entry (setf (cdr entry) (cons env (cdr entry))))
	(t (ordered-push (list index env) *env-table*
			       #'(lambda (entry1 entry2)
				   (< (car entry1) (car entry2)))))))

(defun lookup-env (assumes &aux index entry)
  (setq index (length assumes)
	entry (assoc index *env-table* :test #'=))
  (dolist (env (cdr entry) nil)
    (if (equal (environment-assumptions env) assumes)
	(return env))))

;;;; Determining subsumption
;;This would be faster with bit vectors, but for simplicity
;; we take advantage of the sorted order of the assumptions.

(defun env-subsumed? (e1 e2)
  (cond ((eq e1 e2) t)
	((< (environment-n-assumptions e1)
	    (environment-n-assumptions e2)) nil)
	(t
	  (do ((a1 (environment-assumptions e1))
	       (a2 (environment-assumptions e2))
	       (subsumed? nil)
	       (lost? nil))
	      ((or subsumed? lost?) subsumed?)
	    (cond ((null a1) (if (null a2) (setq subsumed? t)
				 (setq lost? t)))
		  ((null a2) (setq subsumed? t))
		  ((< (assumption-index (car a1))
		      (assumption-index (car a2)))
		   (setq a1 (cdr a1)))
		  ((> (assumption-index (car a1))
		      (assumption-index (car a2)))
		   (setq lost? t))
		  (t (setq a1 (cdr a1) a2 (cdr a2))))))))

;;;; Processing nogoods

(defun update-nogood (just &aux index)
  (dolist (cenv (compute-justification-envs just))
    ;; Clear out subsumed nogoods.
    (if *debug-tms* (format t "~%  ~A new minimal nogood." cenv))
    (setf (environment-contradictory? cenv) just)
    (remove-env-from-labels cenv)
    (insert-nogood-in-table cenv)
    (setq index (environment-n-assumptions cenv))
    (dolist (entry *nogood-table*)
      (when (> (car entry) index)
	(dolist (old (cdr entry))
	  (if (env-subsumed? old cenv)
	      (setf (cdr entry) (delete old (cdr entry)))))))
    (dolist (entry *env-table*)
      (when (> (car entry) index)
	(dolist (old (cdr entry))
	  (when (and (not (environment-contradictory? old))
		     (env-subsumed? old cenv))
	    (setf (environment-contradictory? old) cenv)
	    (remove-env-from-labels old)))))))

(defun insert-nogood-in-table (env &aux index entry)
  (setq index (environment-n-assumptions env)
	entry (assoc index *nogood-table* :test #'=))
  (cond (entry (setf (cdr entry) (cons env (cdr entry))))
	(t (ordered-push (list index env) *nogood-table*
			 #'(lambda (e1 e2) (< (car e1) (car e2)))))))

(defun env-contradictory? (env &aux index)
;; Detects if an environment is contradictory
;; by attempting to find a nogood that subsumes it.
  (cond ((environment-contradictory? env) t)
	(t (setq index (environment-n-assumptions env))
	   (dolist (entry *nogood-table*)
	     (cond ((> (car entry) index) (return nil))
		   (t (dolist (cenv (cdr entry))
			(when (env-subsumed? env cenv)
			  (setf (environment-contradictory? env) cenv)
			  (return t)))))))))

(defun remove-env-from-labels (env)
  (dolist (node (environment-nodes env))
    (setf (tms-node-label node) (delete env (tms-node-label node)))
    (unless (tms-node-label node) (setf (tms-node-status node) ':OUT))
    (push node *node-queue*)))

;;;; User interface

(defun get-node-assumption (node)
  (getf (tms-node-plist node) ':Assumption))

(defun assume-node (node &optional (type 'Assume-node))
  (unless (get-node-assumption node) ;; Don't assume something twice
    (build-justification type node (list (build-assumption node)))))

(defun premise-node! (node)
  ;; The label simply becomes the empty environment,
  ;; meaning that it is true under any set of assumptions.
  (setf (tms-node-label node) (list *empty-env*))
  (setf (tms-node-status node) ':IN)
  (update-node node))

(defun nogood-nodes (nodes &optional (just 'Nogood))
  (build-justification just *contra-node* nodes))

(defun node-implied-by? (n env)
  (some #'(lambda (le) (env-subsumed? env le)) (tms-node-label n)))

(defun node-consistent-with? (n env)
  (some #'(lambda (le) (let ((nenv (append-envs le env)))
			 (and nenv (not (environment-contradictory? nenv)))))
	(tms-node-label n)))				    

;;;; Printing
(defvar *tms-node-printer* #'(lambda (n) (tms-node-datum n)))

(defun why-node (node &optional (stream t) (prefix ""))
  (cond ((eq (tms-node-status node) ':OUT)
	 (format stream "~%~A~A is out."
		 prefix (funcall *tms-node-printer* node)))
	(t (format stream "~%~A~A is in, under ~A"
		   prefix (funcall *tms-node-printer* node)
		   (tms-node-label node)))))

(defun why-nodes (&optional (stream t))
  (dolist (n (reverse *node*)) (why-node n stream)))

(defun node-justifications (node &optional (stream t))
  (format t "~% For ~A:" (funcall *tms-node-printer* node))
  (dolist (j (tms-node-justifications node)) (print-justification j stream)))

(defun print-justification (j &optional (stream t))
  (format stream "~%  ~A, " (justification-type j))
  (dolist (a (justification-antecedents j)) (why-node a stream "     ")))

(defun e (n) (dolist (env *environment*)
	       (if (= (environment-index env) n) (return env)))) 

;;; Yet more printing
(defun print-env (e &optional (stream t))
  (labels ((print-comma-list (elements)
	    (cond ((null elements) nil)
		  ((null (cdr elements))
		   (format stream "~A"
			   (funcall *tms-node-printer*
				    (assumption-datum (car elements)))))
		  (t (format stream "~A, "
			     (funcall *tms-node-printer*
				      (assumption-datum (car elements))))
		     (print-comma-list (cdr elements))))))
	  (format stream "~%~A:~A" e
		  (if (environment-contradictory? e) "* " " "))
	  (format stream "{") (print-comma-list (environment-assumptions e))
	  (format stream "}") e))

(defun print-envs (&optional (stream t))
  (dolist (e (reverse *environment*)) (print-env e stream)))

(defun print-atms-statistics ()
  (format t "~% For environment table:")
  (dolist (entry *env-table*)
    (format t "~%   Length ~D, ~D" (car entry) (length (cdr entry))))
  (format t "~% For nogood table:")
  (dolist (entry *nogood-table*)
    (format t "~%   Length ~D, ~D" (car entry) (length (cdr entry)))))

;;;; Interpretation construction

(defun get-solutions (alternative-sets &aux solutions
					     new-solutions
					     new-interp
					    counter)
  (if *debug* (format t "~% Constructing interpretations..."))
  (setq counter 0
	solutions (list (list *empty-env*)))
  (dolist (alternatives alternative-sets solutions)
    (incf counter)
    (dolist (alternative alternatives)
      (dolist (old-e solutions)
	(setq new-interp (generate-env-cross-product
			   *empty-env* (list old-e
                                             (tms-node-label alternative))))
	(if new-interp (push new-interp new-solutions))))
    (setq solutions new-solutions
	  new-solutions nil)
    ;(print solutions)
    (if *debug* (format t "~%  Round ~D, ~D solutions."
			    counter (length solutions)))))

;;;; Depth-first Interpretation construction

(proclaim '(special *solutions*))

(defun get-depth-solutions (alternative-sets)

  (if *debug* (format t "~% Constructing interpretations depth-first..."))
  (let ((*solutions* nil)
	;these are initially nodes, must first strip them down to lists of envs.
	(choice-sets (mapcar #'(lambda (alt-set)
				 (mapcan #'(lambda (alt)
					     (tms-node-label alt)) alt-set))
			     alternative-sets)))

    (dolist (choice (car choice-sets))
      (get-depth-solutions1 choice (cdr choice-sets)))
    *solutions*))

(defun get-depth-solutions1 (solution choice-sets &aux new-solution)
  (cond ((null choice-sets) (push solution *solutions*))
	((environment-contradictory? solution)) ;something died.
	(t (dolist (choice (car choice-sets))
	     (setq new-solution (append-envs solution choice))
	     (when (and new-solution  ;; bulletproofing
			(not (environment-contradictory? new-solution)))
	       (get-depth-solutions1 new-solution (cdr choice-sets)))))))

;;;; Test code

(proclaim '(special a b c d e f))

(defun atms-test1 ()
  (setq a (build-tms-node "A")
	b (build-tms-node "B")
	c (build-tms-node "C")
	d (build-tms-node "D")
	e (build-tms-node "E")
	f (build-tms-node "F"))
  (assume-node a)
  (assume-node b)
  (assume-node c)
  (build-justification 'J1 d (list a b))
  (build-justification 'J2 e (list b c))
  (build-justification 'J3 f (list d e))
  (why-nodes)
  (print-envs))

(defun atms-test2 ()
  (build-justification 'simpler d (list a))
  (why-nodes)
  (print-envs))

(defun atms-test3 ()
  (nogood-nodes (list a b))
  (why-nodes)
  (print-envs))



;;; an example from de Kleer's paper by Gitchang

(proclaim '(special a b c x=1 y=x x=z y=1 z=1))

(defun step-1 ()
  (setq a (build-tms-node "A")
	b (build-tms-node "B")
	c (build-tms-node "C")
	x=1 (build-tms-node "x=1")
	y=x (build-tms-node "y=x")
	x=z (build-tms-node "x=z")
	y=1 (build-tms-node "y=1")
	z=1 (build-tms-node "z=1") )
  (assume-node a)
  (assume-node b)
  (assume-node c)
  (build-justification 'j1 x=1 (list a))
  (build-justification 'j2 y=x (list b))
  (build-justification 'j3 x=z (list c))
  (why-nodes)
  (print-envs)

  (format t "~2%Now register nogood{A,B}")
  (nogood-nodes (list a b))
  (why-nodes)
  (print-envs)

  (format t "~2%x=1, y=x => y=1")
  (build-justification 'j4 y=1 (list x=1 y=x))
  (why-nodes)
  (print-envs)

  (format t "~2%We have a premise z=1")
  (premise-node! z=1)
  (why-nodes)
  (print-envs)

  (format t "~2%z=1, x=z => x=1")
  (build-justification 'j5 x=1 (list z=1 x=z))
  (why-nodes)
  (print-envs) )


#| The result of the above program.

The Contradiction is out.
A is in, under (E-2)
B is in, under (E-3)
C is in, under (E-4)
x=1 is in, under (E-2)
y=x is in, under (E-3)
x=z is in, under (E-4)
y=1 is out.
z=1 is out.
E-1: {}
E-2: {A}
E-3: {B}
E-4: {C}

Now register nogood{A,B}
The Contradiction is out.
A is in, under (E-2)
B is in, under (E-3)
C is in, under (E-4)
x=1 is in, under (E-2)
y=x is in, under (E-3)
x=z is in, under (E-4)
y=1 is out.
z=1 is out.
E-1: {}
E-2: {A}
E-3: {B}
E-4: {C}
E-5:* {A, B}

x=1, y=x => y=1
The Contradiction is out.
A is in, under (E-2)
B is in, under (E-3)
C is in, under (E-4)
x=1 is in, under (E-2)
y=x is in, under (E-3)
x=z is in, under (E-4)
y=1 is out.
z=1 is out.
E-1: {}
E-2: {A}
E-3: {B}
E-4: {C}
E-5:* {A, B}

We have a premise z=1
The Contradiction is out.
A is in, under (E-2)
B is in, under (E-3)
C is in, under (E-4)
x=1 is in, under (E-2)
y=x is in, under (E-3)
x=z is in, under (E-4)
y=1 is out.
z=1 is in, under (E-1)
E-1: {}
E-2: {A}
E-3: {B}
E-4: {C}
E-5:* {A, B}

z=1, x=z => x=1
The Contradiction is out.
A is in, under (E-2)
B is in, under (E-3)
C is in, under (E-4)
x=1 is in, under (E-2 E-4)
y=x is in, under (E-3)
x=z is in, under (E-4)
y=1 is in, under (E-6)
z=1 is in, under (E-1)
E-1: {}
E-2: {A}
E-3: {B}
E-4: {C}
E-5:* {A, B}
E-6: {B, C}

|#