;;; -*- Mode: LISP; Syntax: Common-lisp; Package: CL-USER -*-

;;; Questions: Why is bond-1 faster than bond, I would have thought the reverse.
;;; (With delay-sat off in both cases.)

;;; Complete logic-based truth maintenance system, version 4 of 7/6/91

;;; Modified: forbus, on 4/27/95
;;; Got rid of annoying compiler warnings.

;;; Copyright (c) 1986, 1987, 1988, 1989, 1990 Kenneth D. Forbus, 
;;; University of Illinois, Johan de Kleer and Xerox Corporation.  
;;; All rights reserved.

;;; See the file legal.txt for a paragraph stating scope of permission
;;; and disclaimer of warranty.  The above copyright notice and that
;;; paragraph must be included in any separate copy of this file.

(in-package :cl-user)

(defun test-explain ()
  (setq *ltms* (create-ltms "Explain Example"))
  (tms-create-node *ltms* "x" :ASSUMPTIONP t)
  (compile-formula *ltms* `(:OR "x" "y"))
  (compile-formula *ltms* `(:OR (:NOT "y") "z"))
  (compile-formula *ltms* `(:OR (:NOT "z") "r"))	
  (enable-assumption (find-node *ltms* "x") :FALSE)
  (explain-node (find-node *ltms* "r")))

(defun test-formula (&optional complete)
	(declare (special r s tt u))
  (setq *ltms* (create-ltms "Formula" :complete complete)
	r (tms-create-node *ltms* "r")
	s (tms-create-node *ltms* "s")
	tt (tms-create-node *ltms* "t")
	u (tms-create-node *ltms* "u"))
  (compile-formula *ltms* `(:implies (:and ,r (:implies ,s ,tt)) ,u)))

(defun run-tests ()
  (test-ask)
  (test-avoid-all)
  (test-bug)
  (test-bug1)
  (test-tax 3)
  (test-tax1 3))

(defun test-ask ()
	(declare (special n1 n2))
  (setq *ltms* (create-ltms "Testing asking")
	n1 (tms-create-node *ltms* "N1" :assumptionp T)
	n2 (tms-create-node *ltms* "N2" :assumptionp T))
  (enable-assumption n1 :FALSE)
  (enable-assumption n2 :FALSE)
  (compile-formula *ltms* `(:or ,n1 ,n2))
  (why-nodes *ltms*))

(defun test-avoid-all ()
	(declare (special n1 n2))
  (setq *ltms* (create-ltms "Testing avoid all"
			    :contradiction-handler 'AVOID-ALL))
  (setq n1 (tms-create-node *ltms* "N1" :assumptionp T)
	n2 (tms-create-node *ltms* "N2" :assumptionp T))
  (enable-assumption n1 :FALSE)
  (enable-assumption n2 :FALSE)
  (compile-formula *ltms* `(:or ,n1 ,n2))
  (why-nodes *ltms*))

(defun test1 (&optional (complete T))
	(declare (special x y))
  (setq *ltms* (create-ltms "TEST1" :COMPLETE complete)
	x (tms-create-node *ltms* "x")
	y (tms-create-node *ltms* "y"))
  (add-formula *ltms* `(:or ,x ,y))
  (add-formula *ltms* `(:or ,x (:not ,y)))
  (complete-ltms *ltms*)
  (unless (true-node? x)
    (error "TEST1 failed")))

(defun test-bug ()
	(declare (special x y z))
  (setq *ltms* (create-ltms "BUG check"))
  (setq x (tms-create-node *ltms* "x" :assumptionp T)
	y (tms-create-node *ltms* "y" :assumptionp T)
	z (tms-create-node *ltms* "z"))
  (compile-formula *ltms* `(:or ,x ,z))
  (compile-formula *ltms* `(:or ,y ,z))
  (enable-assumption x :FALSE)
  (enable-assumption y :FALSE)
  (why-nodes *ltms*)
  (retract-assumption x)
  ;; The original LTMS used to not label z!?!?!?!
  (why-nodes *ltms*))

(defun test-bug1 (&optional (complete T))
	(declare (special x y z))
  (setq *ltms* (create-ltms "BUG check" :COMPLETE complete))
  (setq x (tms-create-node *ltms* "x" :assumptionp T)
	y (tms-create-node *ltms* "y" :assumptionp T)
	z (tms-create-node *ltms* "z"))
  (compile-formula *ltms* `(:or ,x ,z))
  (compile-formula *ltms* `(:or ,y ,z))
  (enable-assumption x :FALSE)
  (enable-assumption y :FALSE)
  (why-nodes *ltms*)
  (retract-assumption x)
  ;; The original LTMS used to not label z!?!?!?!
  (why-nodes *ltms*))

(defun test-tax (n &optional (complete T) &aux nodes)
  (setq *ltms* (create-ltms "taxing" :COMPLETE complete))
  (dotimes (i n) (push (tms-create-node *ltms* i) nodes))
  (add-formula *ltms* `(:taxonomy ,@nodes))
  (format T "~% ~D prime implicates" (ltms-clause-counter *ltms*)))

(defun test-tax1 (n &aux nodes)
  (setq *ltms* (create-ltms "taxing"))
  (dotimes (i n) (push (tms-create-node *ltms* i) nodes))
  (add-formula *ltms* `(:taxonomy ,@nodes))
  (format T "~% ~D prime implicates" (ltms-clause-counter *ltms*)))

(defun test-e (&optional (complete T))
	(declare (special a b c d e))
  (setq *ltms* (create-ltms "example" :complete complete :debugging T)	
	a (tms-create-node *ltms* "a" :assumptionp T)
	b (tms-create-node *ltms* "b" :assumptionp T)
	c (tms-create-node *ltms* "c" :assumptionp T)	
	d (tms-create-node *ltms* "d" :assumptionp T)
	e (tms-create-node *ltms* "e" :assumptionp T))
  (compile-formula *ltms* `(:or (:not ,a) ,b))
  (compile-formula *ltms* `(:or (:not ,c) ,d))
  (compile-formula *ltms* `(:or (:not ,c) ,e))
  (compile-formula *ltms* `(:or (:not ,b) (:not ,d) (:not ,e))))

(defun test-remove ()
	(declare (special a b c))
  (setq *ltms* (create-ltms "Delay" :complete T :debugging T)
	a (tms-create-node *ltms* "a" :assumptionp T)
	b (tms-create-node *ltms* "b" :assumptionp T)
	c (tms-create-node *ltms* "c" :assumptionp T))
  (compile-formula *ltms* `(:or ,a ,b ,c))
  (enable-assumption a :FALSE)
  (enable-assumption b :FALSE)
  (why-nodes *ltms*)
  (compile-formula *ltms* `(:or ,a ,b))
  (why-nodes *ltms*))

(defun test-delay ()
	(declare (special a b c))
  (setq *ltms* (create-ltms "Delay" :complete T :debugging T)
	a (tms-create-node *ltms* "a" :assumptionp T)
	b (tms-create-node *ltms* "b" :assumptionp T)
	c (tms-create-node *ltms* "c" :assumptionp T))
  (enable-assumption a :FALSE)
  (enable-assumption b :FALSE)

  (compile-formula *ltms* `(:or ,a (:not ,b)))
  (compile-formula *ltms* `(:or ,b ,c))
  (pretty-print-clauses *ltms*)

  (why-nodes *ltms*)
  (retract-assumption b)
  (pretty-print-clauses *ltms*)
  (why-nodes *ltms*))


(defun qop (op x y)
  (case op
    (+ (case x
	 (+ (if (or (eq y '+) (eq y '0)) '+))
	 (0 y)
	 (- (if (or (eq y '-) (eq y '0)) '-))))
    (- (case x
	 (+ (if (or (eq y '-) (eq y '0)) '+))
	 (0 (case y (0 '0) (- '+) (+ '-)))
	 (- (if (or (eq y '+) (eq y '0)) '-))))))


(defun confluence (confluence) (confluence1 (car confluence) 0 nil (cdr confluence)))

(defun confluence1 (variables base support rhs &aux op name qvar result)
  (cond ((null variables)
	 (unless (or (equal base rhs) (if (listp rhs) (member base rhs)))
	   (add-clause nil support '(CONFLUENCE))))
	(t (cond ((atom (car variables)) (setq op '+ name (car variables)))
		 (t (setq op (caar variables)) (setq name (cdar variables))))
	   (setq qvar (lookup-qvar name))
	   (dolist (value (cdr qvar))
	     (setq result (qop op base (cdr (tms-node-datum value))))
	     (if result (confluence1 (cdr variables) result (cons value support) rhs))))))

(defvar *qvars* nil)

(defun find-ltre-class (name) 
  (dolist (qvar *qvars*) (if (eq name (car qvar)) (return qvar))))

(defun lookup-qnode (name value)
  (dolist (symbol (cdr (find-ltre-class name)))
    (if (eq value (cdr (tms-node-datum symbol))) (return symbol))))

(defun lookup-qvar (name &aux qvar symbol symbols)
  (setq qvar (find-ltre-class name))
  (if qvar (return-from lookup-qvar qvar))
  (dolist (value '(- 0 +))
    (setq symbol (tms-create-node *ltms* (cons name value) :ASSUMPTIONP T))
    (push symbol symbols))
  (add-formula *ltms* `(:taxonomy ,@symbols) '(QVAR DEFINITION))
  (setq qvar (cons name symbols))
  (push qvar *qvars*)
  qvar)

(defun encode-confluences (confluences)
  (dolist (confluence confluences) (confluence confluence)))

(proclaim (special *qvars*))

(defun qp (confluences)
  (setq *ltms* (create-ltms "QP" :COMPLETE :DELAY)
	*qvars* nil)
  (encode-confluences confluences)
  (format T "~% Performing resolutions on ~D clauses" (length (collect *ltms*)))
  (pretty-print-clauses *ltms*)
  (time (complete-ltms *ltms*))
;  (pretty-print-clauses *ltms*)
  (format T "~% There now are ~D clauses" (length (collect *ltms*)))
  )

(defun easy ()
  (qp `(((dpa (- . dpb) (- . dqab)) . 0))))

(defun two ()
  (qp `(((dpa (- . dpb) (- . dqab)) . 0)
	((dpb (- . dpc) (- .dqbc)) . 0)
	((dqab (- . dqbc)) . 0))))

(defun old-twos ()
  (qp `(((dpa (- . dpb) (- . dqab)) . 0)
	((dpb (- . dpc) (- . x)) . 0)
	((dqab (- . dqbc)) . 0)
	)))

(defun twos ()
  (qp `(((dpa (- . dpb) (- . dqab)) . 0)
	((dpb (- . dpc) (- . dqbc)) . 0)
	((dqab (- . dqbc)) . 0)
	)))

(defun two-pipes ()
  (setq *ltms* (create-ltms "QP" :COMPLETE :DELAY)
	*qvars* nil)
  (encode-confluences `(((dpa (- . dpb) (- . dqab)) . 0)	; Model of pipe ab
			((dpb (- . dpc) (- . dqbc)) . 0)	; Model of pipe bc
			((dqab (- . dqbc)) . 0)	                ; Flows are equal.
 			))
  (format T "~% Initially there are ~D clauses" (length (collect *ltms*)))
  (enable-assumption (lookup-qnode 'dpc 0) :TRUE)	; Right end is held down.
  (enable-assumption (lookup-qnode 'dpa '+) :TRUE)      ; Left end is rising.
  (pretty-print-clauses *ltms*)
  (time (complete-ltms *ltms*))
  (format T "~% There now are ~D clauses" (length (collect *ltms*)))
  (explain-node (lookup-qnode 'dpb '+)))
  

(defun twos1 ()
  (setq *ltms* (create-ltms "QP" :COMPLETE :DELAY)
	*qvars* nil)
  (encode-confluences `(((dpa (- . dpb) (- . dqab)) . 0)
			((dpb (- . dpc) (- . dqbc)) . 0)
			((dqab (- . dqbc)) . 0)
			))

  (enable-assumption (lookup-qnode 'dpa '+) :TRUE)
  (time (complete-ltms *ltms*))
  (format T "~% There now are ~D clauses" (length (collect *ltms*)))
  (retract-assumption (lookup-qnode 'dpa '+))
  (print (ltms-queue *ltms*))
  (dirty-clauses? *ltms*)
  (time (complete-ltms *ltms*))
  (format T "~% There now are ~D clauses" (length (collect *ltms*)))
  (unless (= 638. (length (collect *ltms*))) (error "Can't happen"))


  (format T "~% There should now be no dirty clauses")
  (dirty-clauses? *ltms*)

  ;;; Just repeat for safety.
  (time (complete-ltms *ltms*))
  (format T "~% There now are ~D clauses" (length (collect *ltms*)))
  (format T "~% There should now be no dirty clauses")
  (dirty-clauses? *ltms*)
  (print (ltms-queue *ltms*))
  (enable-assumption (lookup-qnode 'dpa '+) :TRUE)
  (print (ltms-queue *ltms*))
  (dirty-clauses? *ltms*)
  (time (complete-ltms *ltms*))
  (dirty-clauses? *ltms*)
  (format T "~% There now are ~D clauses" (length (collect *ltms*)))
  (retract-assumption (lookup-qnode 'dpa '+))
  (dirty-clauses? *ltms*)
  (time (complete-ltms *ltms*))
  (format T "~% There now are ~D clauses" (length (collect *ltms*)))
  )

(defun dirty-clauses? (ltms &aux (count 0))
  (walk-clauses #'(lambda (cl) (if (clause-dirty cl) (incf count)))
	     (ltms-clauses ltms))
  (format T "~% There are now ~D dirty clauses." count))

(defun ex1 ()
  (qp '(((x y) . 0))))

(defun ex2 ()
  (qp '(((x y) . 0)
	(((- . x) z) . 0))))

;;; Pressure regulator
(defun ex3 ()
  (qp '(
	((p1 (- . p2) (- . q)) . 0)
	((p2 (- . p3) (- . q) a) . 0)
	((p3 (- . p4) (- . q)) . 0)
	((p4 (- . p5) (- . q)) . 0)
	((p4 a) . 0))))

(defun ex4 ()
  (qp `((((- . a) (- . p1) (- . p5)) . 0))))


(defun test-and ()
  (setq *ltms* (create-ltms "LTMS")
	ok (tms-create-node *ltms* "ok" :assumptionp t)
	z (tms-create-node *ltms* "z" :assumptionp t)
	x (tms-create-node *ltms* "x" :assumptionp t)
	y (tms-create-node *ltms* "y" :assumptionp t))
  (add-formula *ltms* `(:implies ,ok (:iff ,z (:and ,x ,y))))
  (pretty-print-clauses *ltms*))

(defun test-andc ()
  (setq *ltms* (create-ltms "LTMS" :complete T)
	ok (tms-create-node *ltms* "ok" :assumptionp t)
	z (tms-create-node *ltms* "z" :assumptionp t)
	x (tms-create-node *ltms* "x" :assumptionp t)
	y (tms-create-node *ltms* "y" :assumptionp t))
  (add-formula *ltms* `(:implies ,ok (:iff ,z (:and ,x ,y))))
  (pretty-print-clauses *ltms*))

(defun test-and1 ()
  (setq *ltms* (create-ltms "LTMS")
	ok (tms-create-node *ltms* "ok" :assumptionp t)
	z=1 (tms-create-node *ltms* "z=1" :assumptionp t)
	z=0 (tms-create-node *ltms* "z=0" :assumptionp t)
	x=1 (tms-create-node *ltms* "x=1" :assumptionp t)
	x=0 (tms-create-node *ltms* "x=0" :assumptionp t)
	y=1 (tms-create-node *ltms* "y=1" :assumptionp t)
	y=0 (tms-create-node *ltms* "y=0" :assumptionp t)
	)
  (add-formula *ltms* `(:taxonomy ,z=1 ,z=0))
  (add-formula *ltms* `(:taxonomy ,x=1 ,x=0))
  (add-formula *ltms* `(:taxonomy ,y=1 ,y=0))
  
;  (add-formula *ltms* `(:implies ,ok (:iff ,z=1 (:and ,x=1 ,y=1))))
  (add-formula *ltms* `(:iff ,z=1 (:and ,x=1 ,y=1)))

  (pretty-print-clauses *ltms*))

(defun test-and1c ()
  (setq *ltms* (create-ltms "LTMS" :complete T)
	ok (tms-create-node *ltms* "ok" :assumptionp t)
	z=1 (tms-create-node *ltms* "z=1" :assumptionp t)
	z=0 (tms-create-node *ltms* "z=0" :assumptionp t)
	x=1 (tms-create-node *ltms* "x=1" :assumptionp t)
	x=0 (tms-create-node *ltms* "x=0" :assumptionp t)
	y=1 (tms-create-node *ltms* "y=1" :assumptionp t)
	y=0 (tms-create-node *ltms* "y=0" :assumptionp t)
	)
  (add-formula *ltms* `(:taxonomy ,z=1 ,z=0))
  (add-formula *ltms* `(:taxonomy ,x=1 ,x=0))
  (add-formula *ltms* `(:taxonomy ,y=1 ,y=0))
  
;  (add-formula *ltms* `(:implies ,ok (:iff ,z=1 (:and ,x=1 ,y=1))))
  (add-formula *ltms* `(:iff ,z=1 (:and ,x=1 ,y=1)))
  (pretty-print-clauses *ltms*))

(defun test-xor (complete)
  (setq *ltms* (create-ltms "LTMS" :complete complete)
	ok (tms-create-node *ltms* "ok" :assumptionp t)
	z=1 (tms-create-node *ltms* "z=1" :assumptionp t)
	z=0 (tms-create-node *ltms* "z=0" :assumptionp t)
	x=1 (tms-create-node *ltms* "x=1" :assumptionp t)
	x=0 (tms-create-node *ltms* "x=0" :assumptionp t)
	y=1 (tms-create-node *ltms* "y=1" :assumptionp t)
	y=0 (tms-create-node *ltms* "y=0" :assumptionp t)
	)
  (add-formula *ltms* `(:taxonomy ,z=1 ,z=0))
  (add-formula *ltms* `(:taxonomy ,x=1 ,x=0))
  (add-formula *ltms* `(:taxonomy ,y=1 ,y=0))
  
;  (add-formula *ltms* `(:implies ,ok (:iff ,z=1 (:and ,x=1 ,y=1))))
;  (add-formula *ltms* `(:iff ,z=1 (:taxonomy ,x=1 ,y=1)))


  (pretty-print-clauses *ltms*))

(defun build-xor (complete)
  (setq *ltms* (create-ltms "LTMS" :complete complete)
	x (tms-create-node *ltms* "x" :assumptionp t)
	y (tms-create-node *ltms* "y" :assumptionp t)
	z (tms-create-node *ltms* "z" :assumptionp t)
	a (tms-create-node *ltms* "a" :assumptionp t)
	b (tms-create-node *ltms* "b" :assumptionp t)
	c (tms-create-node *ltms* "c" :assumptionp t))
  (install-nand x y a)
  (install-nand x a b)
  (install-nand b c z)
  (install-nand a y c)
  (pretty-print-clauses *ltms*))

(defun install-nand (i1 i2 o)
  (add-formula *ltms* `(:iff (:not ,o) (:and ,i1 ,i2))))

(defun history-ex (&aux db)
  (setq *ltms* (create-ltms "History Example" :complete :delay))
  (setq db '((:OR (:NOT x1) x4 a p1)    
	     (:OR (:NOT x1) x4 a p2)    
	     (:OR (:NOT x1) x4 a p3)    
	     (:OR (:NOT x1) x4 a p4)    
	     (:OR (:NOT x1) x4 a p5)    
	     (:OR (:NOT x2) a c)         
	     (:OR (:NOT x3) b1)           
	     (:OR (:NOT x3) b2)           
	     (:OR (:NOT x3) b3)           
	     (:OR (:NOT x3) b4)           
	     (:OR (:NOT x3) b5)           
	     (:OR (:NOT x4) x1 a1)       
	     (:OR (:NOT x4) x1 a2)       
	     (:OR (:NOT x4) x1 a3)       
	     (:OR (:NOT x4) x1 a4)       
	     (:OR (:NOT x4) x1 a5)))
  (dolist (f db)
    (add-formula *ltms* f))
  (complete-ltms *ltms*)
  (format T "~% There now are ~D clauses" (length (collect *ltms*)))
  (print subsumed)
  (add-formula *ltms* '(:OR x1 x2 x3 x4))
  (complete-ltms *ltms*)
  (format T "~% There now are ~D clauses" (length (collect *ltms*)))
  (print subsumed)
  )

(defun kean-adder ()
  (setq *ltms* (create-ltms "Kean Adder" :complete :delay))
  (setq db
        `((:or (:not k=0) (:not l=0) (:not n=0) (:not ab(x1)) )
	  (:or (:not n=0) (:not m=0) (:not r=0) (:not ab(x2)) )
	  (:or (:not k=0) (:not l=1) (:not n=1) (:not ab(x1)) )
	  (:or (:not n=0) (:not m=1) (:not r=1) (:not ab(x2)) )
	  (:or (:not k=1) (:not l=0) (:not n=1) (:not ab(x1)) )
	  (:or (:not n=1) (:not m=0) (:not r=1) (:not ab(x2)) )
	  (:or (:not k=1) (:not l=1) (:not n=0) (:not ab(x1)) )
	  (:or (:not n=1) (:not m=1) (:not r=0) (:not ab(x2)) )
	  (:or (:not k=1) (:not l=1) (:not q=1) (:not ab(a1)) )
	  (:or (:not m=1) (:not n=1) (:not p=1) (:not ab(a2)) )
	  (:or (:not k=0) (:not q=0) (:not ab(a1)) )
	  (:or (:not m=0) (:not p=0) (:not ab(a2)) )
	  (:or (:not l=0) (:not q=0) (:not ab(a1)) )
	  (:or (:not n=0) (:not p=0) (:not ab(a2)) )
	  (:or (:not p=0) (:not q=0) (:not s=0) (:not ab(o1)) )
	  (:or (:not p=1) (:not s=1) (:not ab(o1)) )
	  (:or (:not q=1) (:not s=1) (:not ab(o1)) )
	  (:or (:not k=0) (:not l=0) (:not n=1) ab(x1) )
	  (:or (:not n=0) (:not m=0) (:not r=1) ab(x2) )
	  (:or (:not k=0) (:not l=1) (:not n=0) ab(x1) )
	  (:or (:not n=0) (:not m=1) (:not r=0) ab(x2) )
	  (:or (:not k=1) (:not l=0) (:not n=0) ab(x1) )
	  (:or (:not n=1) (:not m=0) (:not r=0) ab(x2) )
	  (:or (:not k=1) (:not l=1) (:not n=1) ab(x1) )
	  (:or (:not n=1) (:not m=1) (:not r=1) ab(x2) )
	  (:or (:not k=1) (:not l=1) (:not q=0) ab(a1) )
	  (:or (:not m=1) (:not n=1) (:not p=0) ab(a2) )
	  (:or (:not k=0) (:not q=1) ab(a1) )
	  (:or (:not m=0) (:not p=1) ab(a2) )
	  (:or (:not l=0) (:not q=1) ab(a1) )
	  (:or (:not n=0) (:not p=1) ab(a2) )
	  (:or (:not p=0) (:not q=0) (:not s=1) ab(o1) )
	  (:or (:not p=1) (:not s=0) ab(o1) )
	  (:or (:not q=1) (:not s=0) ab(o1) )
	  (:or (:not k=0) (:not k=1) )
	  (:or k=0 k=1 )
	  (:or (:not l=0) (:not l=1) )
	  (:or l=0 l=1 )
	  (:or (:not m=0) (:not m=1) )
	  (:or m=0 m=1 )
	  (:or (:not n=0) (:not n=1) )
	  (:or n=0 n=1 )
	  (:or (:not p=0) (:not p=1) )
	  (:or p=0 p=1 )
	  (:or (:not q=0) (:not q=1) )
	  (:or q=0 q=1 )
	  (:or (:not r=0) (:not r=1) )
	  (:or r=0 r=1 )
	  (:or (:not s=0) (:not s=1) )
	  (:or s=0 s=1 )))
  (dolist (f db)
    (add-formula *ltms* f))
  (format T "~% There now are ~D clauses" (length (collect *ltms*)))
  (time (complete-ltms *ltms*))
  (format T "~% There now are ~D clauses" (length (collect *ltms*))))

(defun selenoid ()
  (setq *ltms* (create-ltms "Selenoid" :complete :delay))
  (add-formula *ltms* '(:taxonomy (= ?a ok) (= ?a stuck_out) (= ?a stuck_in)))
  (add-formula *ltms* '(:taxonomy (= ?b dc_com) (= ?b v24dc) (= ?b float)))
  (add-formula *ltms* '(:taxonomy (= ?c v24dc) (= ?c dc_com) (= ?c float)))
  (add-formula *ltms* '(:taxonomy (= ?d in) (= ?d out)))

  
  (add-formula *ltms* '(:or
		   (:and (= ?a ok) (= ?b dc_com) (= ?c v24dc) (= ?d in) )
		   (:and (= ?a ok) (= ?b dc_com) (= ?c dc_com) (= ?d out) )
		   (:and (= ?a ok) (= ?b dc_com) (= ?c float) (= ?d out) )
		   (:and (= ?a ok) (= ?b v24dc) (= ?c v24dc) (= ?d out) )
		   (:and (= ?a ok) (= ?b v24dc) (= ?c dc_com) (= ?d out) )
		   (:and (= ?a ok) (= ?b v24dc) (= ?c float) (= ?d out) )
		   (:and (= ?a ok) (= ?b float) (= ?c v24dc) (= ?d out) )
		   (:and (= ?a ok) (= ?b float) (= ?c dc_com) (= ?d out) )
		   (:and (= ?a ok) (= ?b float) (= ?c float) (= ?d out) )
		   (:and (= ?a stuck_out) (= ?d out) )
		   (:and (= ?a stuck_in) (= ?d in) )
		   ))
  (format T "~% There now are ~D clauses" (length (collect *ltms*)))
  (time (complete-ltms *ltms*))
  (format T "~% There now are ~D clauses" (length (collect *ltms*))))

(defun valve ()
  (setq *ltms* (create-ltms "Valve" :complete :delay))
  (add-formula *ltms* '(:and
		  (:taxonomy (= ?a ok) (= ?a stuck_open) (= ?a stuck_closed))
		  (:taxonomy (= ?b in) (= ?b out))
		  (:taxonomy (= ?c low) (= ?c normal) (= ?c high) (= ?c none))
		  (:taxonomy (= ?d none) (= ?d low) (= ?d normal) (= ?d high))
		  (:or
		    (:and (= ?a ok) (= ?b in) (= ?c low) (= ?d low) )
		    (:and (= ?a ok) (= ?b in) (= ?c normal) (= ?d normal) )
		    (:and (= ?a ok) (= ?b in) (= ?c high) (= ?d high) )
		    (:and (= ?a ok) (= ?b out) (= ?c low) (= ?d low) )
		    (:and (= ?a ok) (= ?b out) (= ?c normal) (= ?d low) )
		    (:and (= ?a ok) (= ?b out) (= ?c high) (= ?d low) )
		    (:and (= ?c none) (= ?d none) )
		    (:and (= ?a stuck_open) (= ?c low) (= ?d low) )
		    (:and (= ?a stuck_open) (= ?c normal) (= ?d normal) )
		    (:and (= ?a stuck_open) (= ?c high) (= ?d high) )
		    (:and (= ?a stuck_closed) (= ?c low) (= ?d low) )
		    (:and (= ?a stuck_closed) (= ?c normal) (= ?d low) )
		    (:and (= ?a stuck_closed) (= ?c high) (= ?d low) )
		    )))
  (format T "~% There now are ~D clauses" (length (collect *ltms*)))
  (pretty-print-clauses *ltms*)
  (time (complete-ltms *ltms*))
  (format T "~% There now are ~D clauses" (length (collect *ltms*))))

(defun print-horn-clauses ()
  (walk-clauses *ltms*
		#'(lambda (l)
		    (when (definite? l)
		      (format T "~% ")
		      (pretty-string-clause l)))))

(defun print-new-rules ()
  (walk-clauses *ltms*
		#'(lambda (l)
		 (when (and (horn? l)
			    (not (member (car (clause-informant l)) '(:IMPLIED-BY ))))
		   (format T "~% ")
		   (pretty-string-rule l)))))

(defun pretty-string-rule (clause &aux pos)
  (dolist (lit (clause-literals clause))
    (if (eq (cdr lit) :FALSE)
	(format T "~A " (node-string (car lit)))
	(setq pos (car lit))))
  (format T "==>> ~A" (if pos (node-string pos) "CONTRADICTION")))

(defun horn? (cl &aux pos)
  (dolist (lit (clause-literals cl) T)
    (cond ((eq (cdr lit) :FALSE))
	  (pos (return nil))
	  (t (setq pos t)))))

(defun keanp (m k &aux as)
  (setq *ltms* (create-ltms "Kean Problem" :complete :delay :delay-sat t))
  (setq as (kean-setup m k))
;  (complete-ltms *ltms*)
  (format T "~% There now are ~D clauses" (length (collect *ltms*)))
  (add-formula *ltms* as)
  (pretty-print-clauses *ltms*)
  (time (complete-ltms *ltms*))
  (format T "~% There now are ~D clauses" (length (collect *ltms*)))
  )

(defun kean-setup (m k &aux as)
  (do ((i 1 (1+ i)))
      ((> i k) (cons :or as))
    (push `(:not (a ,i)) as)
    (do ((j 1 (1+ j)))
	((> j m))
      (add-formula *ltms* `(:or (a ,i) (:not (s ,i ,j)))))))

(defun teow (n &aux f1 f2)
  (setq *ltms* (create-ltms "Teow Problem" :complete :delay))
  (push `(:AND (A 1) (A 2)) f2)
  (do ((i 3 (+ i 2)))
      ((> i n))
    (push `(:IMPLIES (A ,i) (A 1)) f1)
    (push `(:IMPLIES (A ,(1+ i)) (A 2)) f1)
    (push `(:AND (A ,i) (A ,(1+ i))) f2))
  (add-formula *ltms*
	       `(:AND ,@(nreverse f1) (:OR .,(nreverse f2))))
  ;; Of course this does nothing:
  (time (complete-ltms *ltms*))
  (format T "~% There now are ~D clauses" (length (collect *ltms*)))
  )

(defun teow-bug-1 ()
  (setq *ltms* (create-ltms "Teow bug 1" :complete :delay))
  (add-formula *ltms* `(:and (:or x) (:or (:not x)))))

;;; On 9/11/91 this generated 3241 "PIs"(BCP conditioned) in 676 seconds.  Why did
;;; this take so long?
(defun bond ()
  (setq *ltms* (create-ltms "Bond bug" :complete :delay :delay-sat nil)
	x 
	'((:OR k) (:OR (:NOT l)) (:OR m) (:OR (:NOT r)) (:OR s) (:OR k  l  (:NOT n)  ek  el  en) (:OR k  n  (:NOT l)  ek  el  en)
    (:OR l  n  (:NOT k)  ek  el  en) (:OR (:NOT n)  (:NOT l)  (:NOT k)  ek  el  en)
    (:OR (:NOT k)  (:NOT l)  n  (:NOT ek)  en) (:OR (:NOT k)  l  (:NOT n)  (:NOT ek)  en)
    (:OR k  (:NOT l)  (:NOT n)  (:NOT ek)  en) (:OR k  l  n  (:NOT ek)  en)
    (:OR (:NOT k)  (:NOT l)  n  (:NOT el)  en) (:OR (:NOT k)  l  (:NOT n)  (:NOT el)  en)
    (:OR k  (:NOT l)  (:NOT n)  (:NOT el)  en) (:OR k  l  n  (:NOT el)  en) (:OR (:NOT k)  (:NOT l)  n  (:NOT exa))
    (:OR (:NOT k)  l  (:NOT n)  (:NOT exa)) (:OR k  (:NOT l)  (:NOT n)  (:NOT exa)) (:OR k  l  n  (:NOT exa))
    (:OR k  l  (:NOT n)  exa) (:OR k  n  (:NOT l)  exa) (:OR l  n  (:NOT k)  exa)
    (:OR (:NOT n)  (:NOT l)  (:NOT k)  exa) (:OR (:NOT k)  (:NOT l)  n  (:NOT en)  ek  el  ma)
    (:OR (:NOT k)  l  (:NOT n)  (:NOT en)  ek  el  ma) (:OR k  (:NOT l)  (:NOT n)  (:NOT en)  ek  el  ma)
    (:OR k  l  n  (:NOT en)  ek  el  ma) (:OR k  l  (:NOT n)  (:NOT ma)) (:OR k  n  (:NOT l)  (:NOT ma))
    (:OR l  n  (:NOT k)  (:NOT ma)) (:OR (:NOT n)  (:NOT l)  (:NOT k)  (:NOT ma)) (:OR en  (:NOT ma)) (:OR (:NOT ek)  (:NOT ma))
    (:OR (:NOT el)  (:NOT ma)) (:OR n  m  (:NOT r)  en  em  er) (:OR n  r  (:NOT m)  en  em  er)
    (:OR m  r  (:NOT n)  en  em  er) (:OR (:NOT r)  (:NOT m)  (:NOT n)  en  em  er)
    (:OR (:NOT n)  (:NOT m)  r  (:NOT en)  er) (:OR (:NOT n)  m  (:NOT r)  (:NOT en)  er) (:OR n  (:NOT m)  (:NOT r)  (:NOT en)  er)
    (:OR n  m  r  (:NOT en)  er) (:OR (:NOT n)  (:NOT m)  r  (:NOT em)  er) (:OR (:NOT n)  m  (:NOT r)  (:NOT em)  er)
    (:OR n  (:NOT m)  (:NOT r)  (:NOT em)  er) (:OR n  m  r  (:NOT em)  er) (:OR (:NOT n)  (:NOT m)  r  (:NOT exb))
    (:OR (:NOT n)  m  (:NOT r)  (:NOT exb)) (:OR n  (:NOT m)  (:NOT r)  (:NOT exb)) (:OR n  m  r  (:NOT exb))
    (:OR n  m  (:NOT r)  exb) (:OR n  r  (:NOT m)  exb) (:OR m  r  (:NOT n)  exb)
    (:OR (:NOT r)  (:NOT m)  (:NOT n)  exb) (:OR (:NOT n)  (:NOT m)  r  (:NOT er)  en  em  mb)
    (:OR (:NOT n)  m  (:NOT r)  (:NOT er)  en  em  mb) (:OR n  (:NOT m)  (:NOT r)  (:NOT er)  en  em  mb)
    (:OR n  m  r  (:NOT er)  en  em  mb) (:OR n  m  (:NOT r)  (:NOT mb)) (:OR n  r  (:NOT m)  (:NOT mb))
    (:OR m  r  (:NOT n)  (:NOT mb)) (:OR (:NOT r)  (:NOT m)  (:NOT n)  (:NOT mb)) (:OR er  (:NOT mb)) (:OR (:NOT en)  (:NOT mb))
    (:OR (:NOT em)  (:NOT mb)) (:OR k  (:NOT q)  ek  el  eq) (:OR l  (:NOT q)  ek  el  eq) (:OR q  (:NOT l)  (:NOT k)  ek  el  eq)
    (:OR (:NOT k)  (:NOT l)  (:NOT q)  (:NOT ek)  eq) (:OR (:NOT k)  l  q  (:NOT ek)  eq) (:OR k  (:NOT l)  q  (:NOT ek)  eq)
    (:OR k  l  q  (:NOT ek)  eq) (:OR (:NOT k)  (:NOT l)  (:NOT q)  (:NOT el)  eq) (:OR (:NOT k)  l  q  (:NOT el)  eq)
    (:OR k  (:NOT l)  q  (:NOT el)  eq) (:OR k  l  q  (:NOT el)  eq) (:OR (:NOT k)  (:NOT l)  (:NOT q)  (:NOT exc))
    (:OR (:NOT k)  l  q  (:NOT exc)) (:OR k  (:NOT l)  q  (:NOT exc)) (:OR k  l  q  (:NOT exc))
    (:OR k  (:NOT q)  exc) (:OR l  (:NOT q)  exc) (:OR q  (:NOT l)  (:NOT k)  exc)
    (:OR (:NOT k)  (:NOT l)  (:NOT q)  (:NOT eq)  ek  el  mc) (:OR (:NOT k)  l  q  (:NOT eq)  ek  el  mc)
    (:OR k  (:NOT l)  q  (:NOT eq)  ek  el  mc)  (:OR k  l  q  (:NOT eq)  ek  el  mc)
    (:OR k  (:NOT q)  (:NOT mc)) (:OR l  (:NOT q)  (:NOT mc)) (:OR q  (:NOT l)  (:NOT k)  (:NOT mc)) (:OR eq  (:NOT mc))
    (:OR (:NOT ek)  (:NOT mc)) (:OR (:NOT el)  (:NOT mc)) (:OR m  (:NOT p)  em  en  ep) (:OR n  (:NOT p)  em  en  ep)
    (:OR p  (:NOT n)  (:NOT m)  em  en  ep) (:OR (:NOT m)  (:NOT n)  (:NOT p)  (:NOT em)  ep) (:OR (:NOT m)  n  p  (:NOT em)  ep)
    (:OR m  (:NOT n)  p  (:NOT em)  ep) (:OR m  n  p  (:NOT em)  ep) (:OR (:NOT m)  (:NOT n)  (:NOT p)  (:NOT en)  ep)
    (:OR (:NOT m)  n  p  (:NOT en)  ep) (:OR m  (:NOT n)  p  (:NOT en)  ep) (:OR m  n  p  (:NOT en)  ep)
    (:OR (:NOT m)  (:NOT n)  (:NOT p)  (:NOT exd)) (:OR (:NOT m)  n  p  (:NOT exd)) (:OR m  (:NOT n)  p  (:NOT exd))
    (:OR m  n  p  (:NOT exd)) (:OR m  (:NOT p)  exd) (:OR n  (:NOT p)  exd)
    (:OR p  (:NOT n)  (:NOT m)  exd) (:OR (:NOT m)  (:NOT n)  (:NOT p)  (:NOT ep)  em  en  md)
    (:OR (:NOT m)  n  p  (:NOT ep)  em  en  md) (:OR m  (:NOT n)  p  (:NOT ep)  em  en  md)
    (:OR m  n  p  (:NOT ep)  em  en  md) (:OR m  (:NOT p)  (:NOT md)) (:OR n  (:NOT p)  (:NOT md))
    (:OR p  (:NOT n)  (:NOT m)  (:NOT md)) (:OR ep  (:NOT md)) (:OR (:NOT em)  (:NOT md)) (:OR (:NOT en)  (:NOT md))
    (:OR p  q  (:NOT s)  ep  eq  es) (:OR s  (:NOT p)  ep  eq  es) (:OR s  (:NOT q)  ep  eq  es)
    (:OR (:NOT p)  (:NOT q)  (:NOT s)  (:NOT ep)  es) (:OR (:NOT p)  q  (:NOT s)  (:NOT ep)  es) (:OR p  (:NOT q)  (:NOT s)  (:NOT ep)  es)
    (:OR p  q  s  (:NOT ep)  es) (:OR (:NOT p)  (:NOT q)  (:NOT s)  (:NOT eq)  es) (:OR (:NOT p)  q  (:NOT s)  (:NOT eq)  es)
    (:OR p  (:NOT q)  (:NOT s)  (:NOT eq)  es) (:OR p  q  s  (:NOT eq)  es) (:OR (:NOT p)  (:NOT q)  (:NOT s)  (:NOT exf))
    (:OR (:NOT p)  q  (:NOT s)  (:NOT exf)) (:OR p  (:NOT q)  (:NOT s)  (:NOT exf)) (:OR p  q  s  (:NOT exf)) (:OR p  q  (:NOT s)  exf)
    (:OR s  (:NOT p)  exf) (:OR s  (:NOT q)  exf) (:OR (:NOT p)  (:NOT q)  (:NOT s)  (:NOT es)  ep  eq  mf)
    (:OR (:NOT p)  q  (:NOT s)  (:NOT es)  ep  eq  mf) (:OR p  (:NOT q)  (:NOT s)  (:NOT es)  ep  eq  mf)
    (:OR p  q  s  (:NOT es)  ep  eq  mf) (:OR p  q  (:NOT s) (:NOT mf)) (:OR s  (:NOT p)  (:NOT mf)) (:OR s  (:NOT q)  (:NOT mf))
    (:OR es  (:NOT mf)) (:OR (:NOT ep)  (:NOT mf)) (:OR (:NOT eq)  (:NOT mf))))

  (dolist (c x) (add-formula *ltms* c))

  (time (complete-ltms *ltms*))
  (format T "~% There now are ~D clauses" (length (collect *ltms*))))

;;; On 9/11/91 this generated 3241 PIs in 218 seconds.
(defun bond-1 ()
  (setq *ltms* (create-ltms "Bond bug" :complete :delay :delay-sat nil)
	x 
	'((:OR k) (:OR (:NOT l)) (:OR m) (:OR (:NOT r)) (:OR s) (:OR k  l  (:NOT n)  ek  el  en) (:OR k  n  (:NOT l)  ek  el  en)
    (:OR l  n  (:NOT k)  ek  el  en) (:OR (:NOT n)  (:NOT l)  (:NOT k)  ek  el  en)
    (:OR (:NOT k)  (:NOT l)  n  (:NOT ek)  en) (:OR (:NOT k)  l  (:NOT n)  (:NOT ek)  en)
    (:OR k  (:NOT l)  (:NOT n)  (:NOT ek)  en) (:OR k  l  n  (:NOT ek)  en)
    (:OR (:NOT k)  (:NOT l)  n  (:NOT el)  en) (:OR (:NOT k)  l  (:NOT n)  (:NOT el)  en)
    (:OR k  (:NOT l)  (:NOT n)  (:NOT el)  en) (:OR k  l  n  (:NOT el)  en) (:OR (:NOT k)  (:NOT l)  n  (:NOT exa))
    (:OR (:NOT k)  l  (:NOT n)  (:NOT exa)) (:OR k  (:NOT l)  (:NOT n)  (:NOT exa)) (:OR k  l  n  (:NOT exa))
    (:OR k  l  (:NOT n)  exa) (:OR k  n  (:NOT l)  exa) (:OR l  n  (:NOT k)  exa)
    (:OR (:NOT n)  (:NOT l)  (:NOT k)  exa) (:OR (:NOT k)  (:NOT l)  n  (:NOT en)  ek  el  ma)
    (:OR (:NOT k)  l  (:NOT n)  (:NOT en)  ek  el  ma) (:OR k  (:NOT l)  (:NOT n)  (:NOT en)  ek  el  ma)
    (:OR k  l  n  (:NOT en)  ek  el  ma) (:OR k  l  (:NOT n)  (:NOT ma)) (:OR k  n  (:NOT l)  (:NOT ma))
    (:OR l  n  (:NOT k)  (:NOT ma)) (:OR (:NOT n)  (:NOT l)  (:NOT k)  (:NOT ma)) (:OR en  (:NOT ma)) (:OR (:NOT ek)  (:NOT ma))
    (:OR (:NOT el)  (:NOT ma)) (:OR n  m  (:NOT r)  en  em  er) (:OR n  r  (:NOT m)  en  em  er)
    (:OR m  r  (:NOT n)  en  em  er) (:OR (:NOT r)  (:NOT m)  (:NOT n)  en  em  er)
    (:OR (:NOT n)  (:NOT m)  r  (:NOT en)  er) (:OR (:NOT n)  m  (:NOT r)  (:NOT en)  er) (:OR n  (:NOT m)  (:NOT r)  (:NOT en)  er)
    (:OR n  m  r  (:NOT en)  er) (:OR (:NOT n)  (:NOT m)  r  (:NOT em)  er) (:OR (:NOT n)  m  (:NOT r)  (:NOT em)  er)
    (:OR n  (:NOT m)  (:NOT r)  (:NOT em)  er) (:OR n  m  r  (:NOT em)  er) (:OR (:NOT n)  (:NOT m)  r  (:NOT exb))
    (:OR (:NOT n)  m  (:NOT r)  (:NOT exb)) (:OR n  (:NOT m)  (:NOT r)  (:NOT exb)) (:OR n  m  r  (:NOT exb))
    (:OR n  m  (:NOT r)  exb) (:OR n  r  (:NOT m)  exb) (:OR m  r  (:NOT n)  exb)
    (:OR (:NOT r)  (:NOT m)  (:NOT n)  exb) (:OR (:NOT n)  (:NOT m)  r  (:NOT er)  en  em  mb)
    (:OR (:NOT n)  m  (:NOT r)  (:NOT er)  en  em  mb) (:OR n  (:NOT m)  (:NOT r)  (:NOT er)  en  em  mb)
    (:OR n  m  r  (:NOT er)  en  em  mb) (:OR n  m  (:NOT r)  (:NOT mb)) (:OR n  r  (:NOT m)  (:NOT mb))
    (:OR m  r  (:NOT n)  (:NOT mb)) (:OR (:NOT r)  (:NOT m)  (:NOT n)  (:NOT mb)) (:OR er  (:NOT mb)) (:OR (:NOT en)  (:NOT mb))
    (:OR (:NOT em)  (:NOT mb)) (:OR k  (:NOT q)  ek  el  eq) (:OR l  (:NOT q)  ek  el  eq) (:OR q  (:NOT l)  (:NOT k)  ek  el  eq)
    (:OR (:NOT k)  (:NOT l)  (:NOT q)  (:NOT ek)  eq) (:OR (:NOT k)  l  q  (:NOT ek)  eq) (:OR k  (:NOT l)  q  (:NOT ek)  eq)
    (:OR k  l  q  (:NOT ek)  eq) (:OR (:NOT k)  (:NOT l)  (:NOT q)  (:NOT el)  eq) (:OR (:NOT k)  l  q  (:NOT el)  eq)
    (:OR k  (:NOT l)  q  (:NOT el)  eq) (:OR k  l  q  (:NOT el)  eq) (:OR (:NOT k)  (:NOT l)  (:NOT q)  (:NOT exc))
    (:OR (:NOT k)  l  q  (:NOT exc)) (:OR k  (:NOT l)  q  (:NOT exc)) (:OR k  l  q  (:NOT exc))
    (:OR k  (:NOT q)  exc) (:OR l  (:NOT q)  exc) (:OR q  (:NOT l)  (:NOT k)  exc)
    (:OR (:NOT k)  (:NOT l)  (:NOT q)  (:NOT eq)  ek  el  mc) (:OR (:NOT k)  l  q  (:NOT eq)  ek  el  mc)
    (:OR k  (:NOT l)  q  (:NOT eq)  ek  el  mc)  (:OR k  l  q  (:NOT eq)  ek  el  mc)
    (:OR k  (:NOT q)  (:NOT mc)) (:OR l  (:NOT q)  (:NOT mc)) (:OR q  (:NOT l)  (:NOT k)  (:NOT mc)) (:OR eq  (:NOT mc))
    (:OR (:NOT ek)  (:NOT mc)) (:OR (:NOT el)  (:NOT mc)) (:OR m  (:NOT p)  em  en  ep) (:OR n  (:NOT p)  em  en  ep)
    (:OR p  (:NOT n)  (:NOT m)  em  en  ep) (:OR (:NOT m)  (:NOT n)  (:NOT p)  (:NOT em)  ep) (:OR (:NOT m)  n  p  (:NOT em)  ep)
    (:OR m  (:NOT n)  p  (:NOT em)  ep) (:OR m  n  p  (:NOT em)  ep) (:OR (:NOT m)  (:NOT n)  (:NOT p)  (:NOT en)  ep)
    (:OR (:NOT m)  n  p  (:NOT en)  ep) (:OR m  (:NOT n)  p  (:NOT en)  ep) (:OR m  n  p  (:NOT en)  ep)
    (:OR (:NOT m)  (:NOT n)  (:NOT p)  (:NOT exd)) (:OR (:NOT m)  n  p  (:NOT exd)) (:OR m  (:NOT n)  p  (:NOT exd))
    (:OR m  n  p  (:NOT exd)) (:OR m  (:NOT p)  exd) (:OR n  (:NOT p)  exd)
    (:OR p  (:NOT n)  (:NOT m)  exd) (:OR (:NOT m)  (:NOT n)  (:NOT p)  (:NOT ep)  em  en  md)
    (:OR (:NOT m)  n  p  (:NOT ep)  em  en  md) (:OR m  (:NOT n)  p  (:NOT ep)  em  en  md)
    (:OR m  n  p  (:NOT ep)  em  en  md) (:OR m  (:NOT p)  (:NOT md)) (:OR n  (:NOT p)  (:NOT md))
    (:OR p  (:NOT n)  (:NOT m)  (:NOT md)) (:OR ep  (:NOT md)) (:OR (:NOT em)  (:NOT md)) (:OR (:NOT en)  (:NOT md))
    (:OR p  q  (:NOT s)  ep  eq  es) (:OR s  (:NOT p)  ep  eq  es) (:OR s  (:NOT q)  ep  eq  es)
    (:OR (:NOT p)  (:NOT q)  (:NOT s)  (:NOT ep)  es) (:OR (:NOT p)  q  (:NOT s)  (:NOT ep)  es) (:OR p  (:NOT q)  (:NOT s)  (:NOT ep)  es)
    (:OR p  q  s  (:NOT ep)  es) (:OR (:NOT p)  (:NOT q)  (:NOT s)  (:NOT eq)  es) (:OR (:NOT p)  q  (:NOT s)  (:NOT eq)  es)
    (:OR p  (:NOT q)  (:NOT s)  (:NOT eq)  es) (:OR p  q  s  (:NOT eq)  es) (:OR (:NOT p)  (:NOT q)  (:NOT s)  (:NOT exf))
    (:OR (:NOT p)  q  (:NOT s)  (:NOT exf)) (:OR p  (:NOT q)  (:NOT s)  (:NOT exf)) (:OR p  q  s  (:NOT exf)) (:OR p  q  (:NOT s)  exf)
    (:OR s  (:NOT p)  exf) (:OR s  (:NOT q)  exf) (:OR (:NOT p)  (:NOT q)  (:NOT s)  (:NOT es)  ep  eq  mf)
    (:OR (:NOT p)  q  (:NOT s)  (:NOT es)  ep  eq  mf) (:OR p  (:NOT q)  (:NOT s)  (:NOT es)  ep  eq  mf)
    (:OR p  q  s  (:NOT es)  ep  eq  mf) (:OR p  q  (:NOT s) (:NOT mf)) (:OR s  (:NOT p)  (:NOT mf)) (:OR s  (:NOT q)  (:NOT mf))
    (:OR es  (:NOT mf)) (:OR (:NOT ep)  (:NOT mf)) (:OR (:NOT eq)  (:NOT mf))))

  (add-formula *ltms* `(:AND .,x) 'BOND-1)

  (complete-ltms *ltms*)
  (format T "~% There now are ~D clauses" (length (collect *ltms*))))

(defun bond-2 ()
  (pi '(:AND (:OR k) (:OR (:NOT l)) (:OR m) (:OR (:NOT r)) (:OR s) (:OR k  l  (:NOT n)  ek  el  en) (:OR k  n  (:NOT l)  ek  el  en)
    (:OR l  n  (:NOT k)  ek  el  en) (:OR (:NOT n)  (:NOT l)  (:NOT k)  ek  el  en)
    (:OR (:NOT k)  (:NOT l)  n  (:NOT ek)  en) (:OR (:NOT k)  l  (:NOT n)  (:NOT ek)  en)
    (:OR k  (:NOT l)  (:NOT n)  (:NOT ek)  en) (:OR k  l  n  (:NOT ek)  en)
    (:OR (:NOT k)  (:NOT l)  n  (:NOT el)  en) (:OR (:NOT k)  l  (:NOT n)  (:NOT el)  en)
    (:OR k  (:NOT l)  (:NOT n)  (:NOT el)  en) (:OR k  l  n  (:NOT el)  en) (:OR (:NOT k)  (:NOT l)  n  (:NOT exa))
    (:OR (:NOT k)  l  (:NOT n)  (:NOT exa)) (:OR k  (:NOT l)  (:NOT n)  (:NOT exa)) (:OR k  l  n  (:NOT exa))
    (:OR k  l  (:NOT n)  exa) (:OR k  n  (:NOT l)  exa) (:OR l  n  (:NOT k)  exa)
    (:OR (:NOT n)  (:NOT l)  (:NOT k)  exa) (:OR (:NOT k)  (:NOT l)  n  (:NOT en)  ek  el  ma)
    (:OR (:NOT k)  l  (:NOT n)  (:NOT en)  ek  el  ma) (:OR k  (:NOT l)  (:NOT n)  (:NOT en)  ek  el  ma)
    (:OR k  l  n  (:NOT en)  ek  el  ma) (:OR k  l  (:NOT n)  (:NOT ma)) (:OR k  n  (:NOT l)  (:NOT ma))
    (:OR l  n  (:NOT k)  (:NOT ma)) (:OR (:NOT n)  (:NOT l)  (:NOT k)  (:NOT ma)) (:OR en  (:NOT ma)) (:OR (:NOT ek)  (:NOT ma))
    (:OR (:NOT el)  (:NOT ma)) (:OR n  m  (:NOT r)  en  em  er) (:OR n  r  (:NOT m)  en  em  er)
    (:OR m  r  (:NOT n)  en  em  er) (:OR (:NOT r)  (:NOT m)  (:NOT n)  en  em  er)
    (:OR (:NOT n)  (:NOT m)  r  (:NOT en)  er) (:OR (:NOT n)  m  (:NOT r)  (:NOT en)  er) (:OR n  (:NOT m)  (:NOT r)  (:NOT en)  er)
    (:OR n  m  r  (:NOT en)  er) (:OR (:NOT n)  (:NOT m)  r  (:NOT em)  er) (:OR (:NOT n)  m  (:NOT r)  (:NOT em)  er)
    (:OR n  (:NOT m)  (:NOT r)  (:NOT em)  er) (:OR n  m  r  (:NOT em)  er) (:OR (:NOT n)  (:NOT m)  r  (:NOT exb))
    (:OR (:NOT n)  m  (:NOT r)  (:NOT exb)) (:OR n  (:NOT m)  (:NOT r)  (:NOT exb)) (:OR n  m  r  (:NOT exb))
    (:OR n  m  (:NOT r)  exb) (:OR n  r  (:NOT m)  exb) (:OR m  r  (:NOT n)  exb)
    (:OR (:NOT r)  (:NOT m)  (:NOT n)  exb) (:OR (:NOT n)  (:NOT m)  r  (:NOT er)  en  em  mb)
    (:OR (:NOT n)  m  (:NOT r)  (:NOT er)  en  em  mb) (:OR n  (:NOT m)  (:NOT r)  (:NOT er)  en  em  mb)
    (:OR n  m  r  (:NOT er)  en  em  mb) (:OR n  m  (:NOT r)  (:NOT mb)) (:OR n  r  (:NOT m)  (:NOT mb))
    (:OR m  r  (:NOT n)  (:NOT mb)) (:OR (:NOT r)  (:NOT m)  (:NOT n)  (:NOT mb)) (:OR er  (:NOT mb)) (:OR (:NOT en)  (:NOT mb))
    (:OR (:NOT em)  (:NOT mb)) (:OR k  (:NOT q)  ek  el  eq) (:OR l  (:NOT q)  ek  el  eq) (:OR q  (:NOT l)  (:NOT k)  ek  el  eq)
    (:OR (:NOT k)  (:NOT l)  (:NOT q)  (:NOT ek)  eq) (:OR (:NOT k)  l  q  (:NOT ek)  eq) (:OR k  (:NOT l)  q  (:NOT ek)  eq)
    (:OR k  l  q  (:NOT ek)  eq) (:OR (:NOT k)  (:NOT l)  (:NOT q)  (:NOT el)  eq) (:OR (:NOT k)  l  q  (:NOT el)  eq)
    (:OR k  (:NOT l)  q  (:NOT el)  eq) (:OR k  l  q  (:NOT el)  eq) (:OR (:NOT k)  (:NOT l)  (:NOT q)  (:NOT exc))
    (:OR (:NOT k)  l  q  (:NOT exc)) (:OR k  (:NOT l)  q  (:NOT exc)) (:OR k  l  q  (:NOT exc))
    (:OR k  (:NOT q)  exc) (:OR l  (:NOT q)  exc) (:OR q  (:NOT l)  (:NOT k)  exc)
    (:OR (:NOT k)  (:NOT l)  (:NOT q)  (:NOT eq)  ek  el  mc) (:OR (:NOT k)  l  q  (:NOT eq)  ek  el  mc)
    (:OR k  (:NOT l)  q  (:NOT eq)  ek  el  mc)  (:OR k  l  q  (:NOT eq)  ek  el  mc)
    (:OR k  (:NOT q)  (:NOT mc)) (:OR l  (:NOT q)  (:NOT mc)) (:OR q  (:NOT l)  (:NOT k)  (:NOT mc)) (:OR eq  (:NOT mc))
    (:OR (:NOT ek)  (:NOT mc)) (:OR (:NOT el)  (:NOT mc)) (:OR m  (:NOT p)  em  en  ep) (:OR n  (:NOT p)  em  en  ep)
    (:OR p  (:NOT n)  (:NOT m)  em  en  ep) (:OR (:NOT m)  (:NOT n)  (:NOT p)  (:NOT em)  ep) (:OR (:NOT m)  n  p  (:NOT em)  ep)
    (:OR m  (:NOT n)  p  (:NOT em)  ep) (:OR m  n  p  (:NOT em)  ep) (:OR (:NOT m)  (:NOT n)  (:NOT p)  (:NOT en)  ep)
    (:OR (:NOT m)  n  p  (:NOT en)  ep) (:OR m  (:NOT n)  p  (:NOT en)  ep) (:OR m  n  p  (:NOT en)  ep)
    (:OR (:NOT m)  (:NOT n)  (:NOT p)  (:NOT exd)) (:OR (:NOT m)  n  p  (:NOT exd)) (:OR m  (:NOT n)  p  (:NOT exd))
    (:OR m  n  p  (:NOT exd)) (:OR m  (:NOT p)  exd) (:OR n  (:NOT p)  exd)
    (:OR p  (:NOT n)  (:NOT m)  exd) (:OR (:NOT m)  (:NOT n)  (:NOT p)  (:NOT ep)  em  en  md)
    (:OR (:NOT m)  n  p  (:NOT ep)  em  en  md) (:OR m  (:NOT n)  p  (:NOT ep)  em  en  md)
    (:OR m  n  p  (:NOT ep)  em  en  md) (:OR m  (:NOT p)  (:NOT md)) (:OR n  (:NOT p)  (:NOT md))
    (:OR p  (:NOT n)  (:NOT m)  (:NOT md)) (:OR ep  (:NOT md)) (:OR (:NOT em)  (:NOT md)) (:OR (:NOT en)  (:NOT md))
    (:OR p  q  (:NOT s)  ep  eq  es) (:OR s  (:NOT p)  ep  eq  es) (:OR s  (:NOT q)  ep  eq  es)
    (:OR (:NOT p)  (:NOT q)  (:NOT s)  (:NOT ep)  es) (:OR (:NOT p)  q  (:NOT s)  (:NOT ep)  es) (:OR p  (:NOT q)  (:NOT s)  (:NOT ep)  es)
    (:OR p  q  s  (:NOT ep)  es) (:OR (:NOT p)  (:NOT q)  (:NOT s)  (:NOT eq)  es) (:OR (:NOT p)  q  (:NOT s)  (:NOT eq)  es)
    (:OR p  (:NOT q)  (:NOT s)  (:NOT eq)  es) (:OR p  q  s  (:NOT eq)  es) (:OR (:NOT p)  (:NOT q)  (:NOT s)  (:NOT exf))
    (:OR (:NOT p)  q  (:NOT s)  (:NOT exf)) (:OR p  (:NOT q)  (:NOT s)  (:NOT exf)) (:OR p  q  s  (:NOT exf)) (:OR p  q  (:NOT s)  exf)
    (:OR s  (:NOT p)  exf) (:OR s  (:NOT q)  exf) (:OR (:NOT p)  (:NOT q)  (:NOT s)  (:NOT es)  ep  eq  mf)
    (:OR (:NOT p)  q  (:NOT s)  (:NOT es)  ep  eq  mf) (:OR p  (:NOT q)  (:NOT s)  (:NOT es)  ep  eq  mf)
    (:OR p  q  s  (:NOT es)  ep  eq  mf) (:OR p  q  (:NOT s) (:NOT mf)) (:OR s  (:NOT p)  (:NOT mf)) (:OR s  (:NOT q)  (:NOT mf))
    (:OR es  (:NOT mf)) (:OR (:NOT ep)  (:NOT mf)) (:OR (:NOT eq)  (:NOT mf)))))

(defun check (ltms)
  (walk-clauses ltms
		#'(lambda (cl) (unless (find-tree cl ltms) (error "Can't find ~A" cl)))))

(defun check-tree (tree &aux (last 0))
  (unless (atom tree)
    (dolist (entry tree) (unless (<= last (setq last (tms-node-index (caar entry))))
			   (error "Tree out of order"))
	    (check-tree (cddr entry))
	    )))


;;; Temporary.
(defun find-tree (cl ltms)
  (find-tree-1 (clause-literals cl) (clause-length cl) (ltms-clauses ltms)))

;;;***** length is not sued here.
(defun find-tree-1 (lits length tree)
  (cond ((null lits) (if (atom tree) tree))
	((atom tree) nil)
	(t (dolist (subtree tree)
	     (if (eq (car lits) (car subtree))
		 (return (find-tree-1 (cdr lits) length (cdr subtree))))))))


;;; Temporary diagnostics? Needed for printing?

(defun find-clause (literals &aux cl)
  (setq literals (simplify-clause literals)
	cl (subsumed? literals (ltms-clauses *ltms*)))
  cl)


(defun print-envs (ltms)
  (maphash #'(lambda (ignore node)
	       (format T "~% ~A has label ~A" node (tms-env node :TRUE))
	       (format T "~% (:NOT ~A) has label ~A" node (tms-env node :FALSE))	       )
	   (ltms-nodes ltms)))

(defun justify-node (informant consequent antecedents)
  (add-clause (list consequent) antecedents informant))

(defun nogood-nodes (informant nodes)
  (add-clause nil nodes informant))

(defun step-1 ()
  (setq *ltms* (create-ltms "Step-1" :complete T :block? nil)
	a (tms-create-node *ltms* "A" :assumptionp t)
	b (tms-create-node *ltms* "B" :assumptionp t)
	c (tms-create-node *ltms* "C" :assumptionp t)
	x=1 (tms-create-node *ltms* "x=1")
	y=x (tms-create-node *ltms* "y=x")
	x=z (tms-create-node *ltms* "x=z")
	y=1 (tms-create-node *ltms* "y=1")
	z=1 (tms-create-node *ltms* "z=1") )
  (justify-node 'j1 x=1 (list a))
  (justify-node 'j2 y=x (list b))
  (justify-node 'j3 x=z (list c))
  (why-nodes *ltms*)
  (print-envs *ltms*)

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

  (format t "~2%x=1, y=x => y=1")
  (justify-node 'j4 y=1 (list x=1 y=x))
  (why-nodes *ltms*)
  (print-envs *ltms*)

  (format t "~2%We have a premise z=1")
  (justify-node 'Premise z=1 nil)
  (why-nodes *ltms*)
  (print-envs *ltms*)

  (format t "~2%z=1, x=z => x=1")
  (justify-node 'j5 x=1 (list z=1 x=z))
  (why-nodes *ltms*)
  (print-envs *ltms*) )

(defun print-statistics (&optional (ltms *ltms*) &aux lengths)
  (setq lengths (make-array 100. :initial-element 0))
  (format T "~% There are ~D propositional symbols" (ltms-node-counter ltms))
  (walk-clauses ltms
		#'(lambda (cl)
		    (incf (aref lengths (clause-length cl)))))
  (dotimes (i 100)
    (unless (= (aref lengths i) 0)
      (format T "~% There are ~D prime implicates of size ~D"
	      (aref lengths i)
	      i)))
  )