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

"(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."

(in-package 'tms)

;;; This makes sure the file was compiled and loaded in the same mode.  Otherwise
;;; all sorts of bugs appear.
;(check-compile-consistency #.*compile-mode*)

;;; A node is in from the perspective of the problem solver if it is in at least one
;;; non-ignored environment.
(defun ps-in? (node) (dolist (e (n-a-envs node)) (or (ignored-env? e) (return e))))

;;; If this is called often, it should be a slot on every env, or a bit.
(defun ignored-env? (e)
  (dolist (a (env-assumptions e)) (if (assumption-ignorep a) (return a))))
  
(defun nm-justify-node (node inlist outlist informant &aux initem outitem)
  (cond ((cdr inlist)
	 (setq initem (create-node "inlist for nmj"))
	 (justify-node initem (cons 'INLIST inlist)))
	(t (setq initem (car inlist))))
  (cond ((cdr outlist)
	 (setq outitem (create-node "outlist for nmj"))
	 (dolist (o outlist) (justify-node outitem (list 'OUTLIST o)))
	 (implied-disjunction1 outitem outlist))
	(t (setq outitem (car outlist))))
  (simple-nm-justify-node node initem outitem informant))

;;;****** delay until in is in.
(defun simple-nm-justify-node (node in out informant &aux ina outa)
  (setq ina (create-assumption (format nil "Assume-~A" (n-a-datum node))))
  (justify-node node (list "NMJ-1" in ina))
  (justify-node *contra-node* (list "NMJ-2" in out ina))
  (setq outa (create-assumption (format nil "Assume-~A" (n-a-datum out))))
  ;; The out assumption should be ignored.
  (setf (assumption-ignorep outa) T)
  (justify-node out (list "NMJ-3" in outa))
  (justify-node *contra-node* (list "NMJ-4" in node outa))
  ;; XOR or IOR is ok here.
  (choose (list ina outa) informant))

;;; This encodes o -> o1 or o2 or o3 ...
;;; This assumes unique assumptions are created for each.   Other modes are discussed.
;;; ****** If the node is already defaulted what then???????
;;; ****** If the node already is an assumption then what?????
;;; Creating the implied disjunction could really wait until o is in.****
(defun implied-disjunction1 (o os &aux as a)
  (cond ((null (cdr os)) (justify-node (car os) (list 'TRIVIAL-IMPLIED-DISJUNCTION o)))
	(t (dolist (oi os) (setq a (create-assumption oi))
		           (push a as)
      		           (justify-node oi (list 'IMPLIED-DISJUNCTION a o)))
	   (ior as))))

;;; Look elsewhere.
(defun ior (x) x (break "unimplemented"))

;;; imp looks like (=> lhs rhs), where all are nodes.

;;; This uses the scheme of section 6.4.4 of Extending the ATMS.
(defun encode-by-implication-a (imp &aux eqn lhs rhs disjunct disjunction)
  (setq lhs (second imp) rhs (third imp))
  (cond ((null rhs)
	 (justify-node *contra-node* (cons 'ENCODE-BY-IMPLICATION-A lhs)))
	((null (cdr rhs))
	 (justify-node (car rhs) (cons 'ENCODE-BY-IMPLICATION-A lhs)))
	(t (dolist (i rhs)
	     (setq disjunct (conditional-unique-default i))
	     (push disjunct disjunction)
	     (justify-node i (cons 'ENCODE-BY-IMPLICATION-A (cons disjunct lhs))))
	   (setq eqn (create-assumption imp))
	   (push eqn disjunction)
	   (setf (assumption-ignorep eqn) T)
	   (justify-node *contra-node* (cons 'ENCODE-BY-IMPLICATION-A (cons eqn lhs)))
	   (choose disjunction 'ENCODE-BY-IMPLICATION-A))))
	   
(defun encode-by-buggy-simple-implication (imp &aux disjunction disjunct)
  (dolist (i (third imp))
    (setq disjunct (buggy-conditional-unique-default-node i))
    (push disjunct disjunction)
    (justify-node i (cons 'BUGGY-ENCODE (cons disjunct (second imp)))))
  (choose disjunction 'BUGGY-ENCODE))

(defun encode-by-disjunction (imp &aux disjunction)
  (dolist (i (third imp)) (push (default-node i) disjunction))
  (dolist (i (second imp)) (push (default-node (negate-node i)) disjunction))
  (choose disjunction 'ENCODE-BY-DISJUNCTION))
  
(defun negate-node (n-a &aux n a1 a2)
  (cond ((assumption? n-a)
	 (cond ((assumption-negation n-a))
	       (t (setq n (create-assumption (format nil "NOT ~A" (n-a-datum n-a))))
		  (setf (assumption-negation n-a) n)
		  (setf (assumption-negation n) n-a)
		  (setf (assumption-ignorep n) T)
		  (justify-node *contra-node* (list 'NEGATE-NODE n n-a))
		  (choose (list n-a n) 'NEGATE-NODE)
		  n)))
	((node-negation n-a))
	(t (setq n (create-node (format nil "NOT ~A" (n-a-datum n-a))))
	   (setf (node-negation n-a) n)
	   (setf (node-negation n) n-a)
	   (justify-node *contra-node* (list 'NEGATE-NODE n-a n))
	   (setq a1 (default-node n-a) a2 (default-node n))
	   (when (assumption-negation a1) (error "What to do?"))
	   (setf (assumption-negation a1) a2)
	   (when (assumption-negation a2) (error "What to do?"))
	   (setf (assumption-negation a2) a1)
	   ;; Allow these assumptions to have multiple negations.???
	   (choose (list a1 a2) 'NEGATE-NODE)
	   n)))
	   
;;; For examples only.  Returns the default to use.
(defun conditional-unique-default (n-a &aux a)
  (cond ((assumption? n-a) n-a)
	((node-unique-conditional n-a))
	(t (setq a (create-assumption (n-a-datum n-a)))
	   (setf (assumption-ignorep a) T)
	   (setf (node-unique-conditional n-a) a)
	   a)))

;;; For examples only.  Returns the default to use.
(defun buggy-conditional-unique-default-node (n-a &aux a)
  (cond ((assumption? n-a) n-a)
	((node-assumption n-a))
	(t (setq a (create-assumption (n-a-datum n-a)))
	   (setf (assumption-ignorep a) T)
	   (setf (node-assumption n-a) a)
	   a)))

;;; This defaults a node unconditionally if it hasn't been defaulted already.  It returns
;;; an assumption.
(defun default-node (n-a &aux a)
  (cond ((assumption? n-a) n-a)
	((node-assumption n-a))
	(t (assume-node n-a)
	   (setq a (node-assumption n-a))
	   (setf (assumption-datum a) (n-a-datum n-a))
	   (setf (assumption-ignorep a) T)
	   a)))

;;;*******?????
;;; This defines a negation.  ***************** when n-a gets modified.
;;; Put negations in here??????? what if things already have negations??????????
(defun negation (x y &aux ax ay)
  (justify-node *contra-node* (list 'NEGATION x y))
  (cond ((assumption? x))
	((setq ax (node-assumption x)))
	(t (assume-node x)
	   (setq ax (node-assumption x))
	   (setf (assumption-datum ax) (n-a-datum x))
	   (setf (assumption-ignorep ax) T)))
  (cond ((assumption? y))
	((setq ay (node-assumption y)))
	(t (assume-node y)
	   (setq ay (node-assumption y))
	   (setf (assumption-datum ay) (n-a-datum y))
	   (setf (assumption-ignorep ay) T)))
  (choose (list ax ay) 'NEGATION))


;;; Encodes EQUIV A B without assumptions

(defun equiv (a b)
  (justify-node a (list 'EQUIV b))
  (justify-node b (list 'EQUIV a)))

;;; Assumes a set of conjuncts, conjuncts are atomic assumptions.
;;; Let the ior data-base do the subsumption (this is buggy right now I think***).
;;; We might have to do a pre-subsumption check when we generate these.
(defun dnf (conjuncts &aux disjuncts new-disjuncts)
  (format T "~% DNF converted ~D conjuncts" (length conjuncts))
  (dolist (conjunct conjuncts)
    (setq new-disjuncts nil)
    (dolist (assumption conjunct)
      (if disjuncts
	  (dolist (disjunct disjuncts)
	    (push (if (memq assumption disjunct)
		      disjunct
		      (cons assumption disjunct))
		  new-disjuncts))
	  (push (list assumption) new-disjuncts)))
    (setq disjuncts new-disjuncts))
  (format T "~% ~D disjunctions" (length disjuncts))

  (dolist (disjunct disjuncts)
    (choose disjunct '(DNF)))

  )