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

;;; Basic user functions.

(defun get-assumption-node (node) (assumption-node node))

(defun label (n-a)
  (when *trace-file*
    (dolist (e (n-a-envs n-a)) (trace-env e))
    (format *trace-file* "~%L ")
    (trace-node n-a)
    (format *trace-file* "(")
    (let ((previous nil))
      (dolist (e (n-a-envs n-a))
	(zf previous
	    (format *trace-file* " ~D" (env-unique e))
	    (setq previous T)
	    (format *trace-file* "~D" (env-unique e)))))
    (format *trace-file* ")"))
  (n-a-envs n-a))

(defun in? (node)
  (when *trace-file*
    (format *trace-file* "~%~:[OUT~;IN~] " (i-in? node))
    (trace-node node))
  (i-in? node))

(defun out? (node)  
  (when *trace-file*
    (format *trace-file* "~%~:[OUT~;IN~] " (i-in? node))
    (trace-node node))
  (i-out? node))

(defun true? (n-a)
  (when *trace-file*
    (format *trace-file* "~%~:[NT~;TR~] " (i-true? n-a))
    (trace-node n-a))
  (i-true? n-a))

(defun false? (n-a)
  (when *trace-file*
    (format *trace-file* "~%~:[NF~;F~] " (i-false? n-a))
    (trace-node n-a))
  (i-false? n-a))

;;; Returns FALSE,OUT,IN,TRUE.  For external use only.
(defun status-of-node (node &aux envs result)
  (setq result
	(cond ((n-a-contradictory node) :FALSE)
	      ((null (setq envs (n-a-envs node))) ':OUT)
	      ((eq *empty-env* (car envs)) ':TRUE)
	      (T ':IN)))
  (when *trace-file*
    (format *trace-file* "~%S ~A " result)
    (trace-node node))
  result)

;;; Nothing is in a contradictory env. For external use only, and then for debugging.
;;;****** no needs to output env.
(defun possible-status-of-node (node env &aux envs result)
  (setq result 
	(cond ((env-contradictory env) ':OUT)
	      ((n-a-contradictory node) ':FALSE)
	      ((null (setq envs (n-a-envs node))) ':OUT)
	      ((eq *empty-env* (car envs)) ':TRUE)
	      ((dolist (e envs) (if (successfull-union? e env) (return ':IN))))
	      (T ':OUT)))
  (when *trace-file*
    (format *trace-file* "~% PS ~A " result)
    (trace-node node))
  result)

(defmacro without-focus (&body body) `(let ((*foci* nil)) (prog1 ,@body)))

(defun user-contradictory-env (env reason &aux *going-nodes*)
  (when *trace-file*
    (trace-env env)
    (format *trace-file* "~%UCE ~D" (env-unique env)))
  (if (neq (car reason) 'BASE) (error "Reason must look like (BASE . ...)"))
  (contradictory-env env reason)
  (when *going-nodes* (process-changed-nodes)))

(defun user-contradictory-envs (envs reason &aux *going-nodes*)
  (when *trace-file*
    (dolist (e envs) (trace-env e))
    (format *trace-file* "~%UCES ")
    (format *trace-file* "(")
    (let ((previous nil))
      (dolist (e envs)
	(zf previous
	    (format *trace-file* "~D" (env-unique e))
	    (setq previous T)
	    (format *trace-file* " ~D" (env-unique e)))))
    (format *trace-file* ")"))

  (if (neq (car reason) 'BASE) (error "Reason must look like (BASE . ...)"))
  (contradictory-envs1 envs reason)
  (when *going-nodes* (process-changed-nodes)))

;;; Returns two nodes.  Creates a class only for historical reasons****.  Soon obsolete.
(defun create-symbol (datum &optional class passumption nassumption
		      &aux node1 node2 symbol (old-trace-file *trace-file*) *trace-file*)
  class
;  This should be commented out some day, but adb::get-tms-node1 still needs it.
;  (unless class (setq class (create-class datum nil nil)))
  (setq node2 (if nassumption
		  (create-assumption (cons 'NOT datum))
		  (create-node (cons 'NOT datum)))
	node1 (if passumption
		  (create-assumption datum)
		  (create-node datum)))
  (setq symbol (make-psymbol :NAME-SYMBOL 'SYMBOL
			     :DATUM datum
			     :PNODE node1
			     :NNODE node2
			     :UNIQUE (incf *symbol-counter*)
			     :OR (make-disjunction :DISJUNCTS (list node1 node2)
						   :ODISJUNCTS (list node1 node2)
						   :COUNT 2)
			     ))
;  This should be commented out some day, but adb::get-tms-node1 still needs it.
;  (add-class-to-node node2 class)
;  This should be commented out some day, but adb::get-tms-node1 still needs it.
;  (add-class-to-node node1 class)
  (setf (n-a-neg node1) node2)
  (setf (n-a-neg node2) node1)
  (setf (n-a-symbol node1) symbol)
  (setf (n-a-symbol node2) symbol)
  (when (and nassumption passumption)
    (push symbol *assumption-symbols*)
    (contradictory-assumption-pair node1 node2))
  (when old-trace-file
    (format old-trace-file
	    "~%CS1 ~D " *symbol-counter*)
    (trace-node node1 old-trace-file)
    (format old-trace-file " ")
    (trace-node node2 old-trace-file))
  (values node1 node2))

;;; Interface to negation code.  Someday may be in its own file.
(defun class->symbol (class &aux nodes node1 node2 *going-nodes* flag)
  ;; Exclusion is handled by negation.
  (setf (class-exclusive class) nil)
  (setq nodes (class-nodes class)
	node1 (car nodes)
	node2 (cadr nodes))
  (unless (= (length nodes) 2) (error "Must be exactly two nodes in a negation"))
  (if (n-a-neg node1) (error "Node is already negated"))
  (if (n-a-neg node2) (error "Node is already negated"))
  (setf (n-a-neg node1) node2)
  (setf (n-a-neg node2) node1)
  ;; Now make sure we have the right clauses hooked up.
  (if (or (n-a-pclauses node1) (n-a-nclauses node1))
      (error "unimplemented"))
  (dolist (p (n-a-pclauses node1))
    (unless (member p (n-a-nclauses node2) :TEST #'EQUAL)
      (push p (n-a-nclauses node2))))
  (dolist (n (n-a-nclauses node1))
    (unless (member n (n-a-pclauses node2) :TEST #'EQUAL)
      (push n (n-a-pclauses node1))))
  (dolist (p (n-a-pclauses node2))
    (unless (member p (n-a-nclauses node1) :TEST #'EQUAL)
      ;; When each clause p was originally encoded, node2 which occurs positively
      ;; in it had no negative.
      ;; Clobber the clause into its preferred representation.
      (unless (memq node2 (second p)) (error "BUG"))
      (setf (second p) (fdelq1 node2 (second p)))
      (push node1 (first p))
      (cond ((cdr (second p)))
	    ((second p)
	     (user-simple-justify-node (car (second p)) (first p)))
	    (t (setq flag nil)
	       (dolist (n (cdr (first p)))
		 (when (n-a-neg n)
		   (user-simple-justify-node (n-a-neg n) (remove n (first p)))
		   (setq flag T)))
	       (if flag (user-simple-justify-node *contra-node* (first p)))
	       ))
      (if (member p (n-a-nclauses node1) :TEST #'EQUAL)
	  (error "Duplicate???"))
      (push p (n-a-nclauses node1))))
  (dolist (n (n-a-nclauses node2))
    (unless (member n (n-a-pclauses node1) :TEST #'EQUAL)
      ;;*** install the justifications we failed to install last time.
      ;;*** because node1 did not exist.
      ;; When each clause n was originally encoded, node2 which occurs negatively
      ;; in it, had no positive.  So the number of only-positives cannot have changed.
      (when (null (second n))
	(user-simple-justify-node node1 (remove node2 (first n))))
      (if (member n (n-a-pclauses node1) :TEST #'EQUAL)
	  (error "Duplicate-B???"))
      (push n (n-a-pclauses node1))))
  ;; Now that we know these two are negations of each other, do the inferences
  ;; we might not have been able to do earlier.
  (cond ((i-true? node1) (contradictory-node node2 '(CLASS->SYMBOL)))
	((i-true? node2) (contradictory-node node1 '(CLASS->SYMBOL)))
	((i-false? node1) (justify-node node2 '(CLASS->SYMBOL)))
	((i-false? node2) (justify-node node1 '(CLASS->SYMBOL))))
  (if *going-nodes* (process-changed-nodes))
  )

;;; Soon to be extremely updated.
;;; This removes duplicate literals.  This must be done, otherwise our BCP gets errors.
;;; This avoids copying in most cases.  Can be made slightly more efficient if necessary.
(defun clause (informant positives negatives
	       &aux remaining-positives remaining-negatives clause flag (count 0) copyp)
  (when *trace-file*
    (format *trace-file* "~%CL (")
    (dolist (positive positives) (trace-node positive))
    (format *trace-file* ") (")
    (dolist (negative negatives) (trace-node negative))
    (format *trace-file* ")"))
  (dolist (n negatives) (if (i-false? n) (return-from CLAUSE nil)))
  (dolist (p positives) (if (i-true? p) (return-from CLAUSE nil)))
  (cond ((null *clause-mode*)
 	 (cond ((null positives)
		(justify-node *contra-node* (cons informant negatives)))
	       ((null (cdr positives))
		(justify-node (car positives) (cons informant negatives)))
	       (T (error "You said no clauses bunky"))))
	(t (cond ((or (dolist (n negatives) (if (i-true? n) (return T)))
		      (do ((n negatives (cdr n)))
			  ((null n))
			(if (memq (car n) (cdr n)) (return T))))
		  (dolist (n negatives)
		    (unless (memq n remaining-negatives)
		      (push n remaining-negatives))))
		 (t (setq remaining-negatives negatives)))
	   ;; Try to canonicalize for debugging purposes.  Try to make the clause
	   ;; as negative as possible.  Could save conses here.
	   (do ((p positives (cdr p)))
	       ((null p))
	     (cond ((or (i-false? p) (n-a-neg p))
		    (cond (copyp (push p remaining-positives))
			  ((eq p (car positives)) (setq positives (cdr positives)))
			  (t (setq copyp t)
			     (dolist (positive positives)
			       (if (eq p positive) (return nil))
			       (push positive remaining-positives)))))))
	   (unless copyp (setq remaining-positives positives))

	 ;; If we are using the synthesis rule, we don't need to store clauses.
	 (and *resolve-by-labeling*
	      (null remaining-positives)
	      (dolist (neg remaining-negatives T)
		(unless (assumption? neg) (return nil)))
	      (progn (user-simple-justify-node *contra-node*
					       remaining-negatives
					       (if *explain-flag*
						   `(CLAUSE ,informant ,positives ,negatives)))
		     (return-from clause nil)))

	 ;; If there is only one literal, were done; don't go to the effort of encoding
	 ;; the clause.
	 (cond ((null remaining-positives)
		(cond ((null remaining-negatives) (throw 'CONTRADICTION 'FAIL))
		      ((cdr remaining-negatives))
		      (t (justify-node *contra-node* (cons informant remaining-negatives))
			 (return-from CLAUSE nil))))
	       ((cdr remaining-positives))
	       ((null remaining-negatives)
		(justify-node (car remaining-positives) (list informant))
		(return-from CLAUSE nil)))
	 (dolist (n remaining-negatives) (unless (n-a-envs n) (incf count)))
	 (setq positives remaining-positives
	       negatives remaining-negatives
	       ;; Fourth slot is cost cache.
	       clause (make-clause :negatives negatives
				   :positives (if positives (error "Should be nil"))
				   :informant informant
				   :count count))

	 (setq *clauses* t)

	 ;; As far as possible wire up the clauses.
	 ;; Remember, by construction a positive can't have a negative.
	 ;; ***THe following equal checks don't work obviously.
	 (dolist (p positives) (push clause (n-a-pclauses p)))
	 (dolist (n negatives) (push clause (n-a-nclauses n)))
	 ;; Now do the propagations we should have done if we hadn't seen this clause until
	 ;; now.  This isn't right in general.  Fix some day.
	 (when (< count 2)
	   (if *rltms* (error "needs work"))
	   (let (*going-nodes*)
	     (cond ((cdr positives))
		   (positives (user-simple-justify-node (car positives) negatives))
		   (t (setq flag nil)
		      (dolist (n negatives)
			(if (n-a-neg n)
			    (user-simple-justify-node (n-a-neg n) (remove n negatives))
			    (setq flag T)))
		      (if flag (user-simple-justify-node *contra-node* negatives))
		      ))
	     (if *going-nodes* (process-changed-nodes))))
	 )))

(defun cc ()
  (dolist (n *nodes*)
    (cnc n)))

(defun cnc (n)
  (do ((clauses (n-a-pclauses n) (cdr clauses)))
      ((null clauses))
    (dolist (other (cdr clauses))
      (and (equal (car clauses) other)
	   (format T "~% Duplicates ~A:::~A" (car clauses) other))))

    (do ((clauses (n-a-nclauses n) (cdr clauses)))
      ((null clauses))
    (dolist (other (cdr clauses))
      (and (equal (car clauses) other)
	   (format T "~% Duplicates ~A:::~A" (car clauses) other)))))

(defun cj (l &aux envs)
  (dolist (j l)
    (setq envs (n-a-envs (second j)))
    (justify-node (second j) (third j))
    (unless (equal (n-a-envs (second j)) envs)
      (error "J did something"))))