;  qi.lisp                                  Boyer & Hunt

(in-package "ACL2")
(include-book "hons-help2")

; ubdd operations.  ubdd-based set operations.  Reachability.

; ubdd stands for 'unlabeled bdd', and means a cons-tree in T and NIL
; without any subtree that is '(t . t) or '(nil . nil).

; By 'cons-tree in T and NIL' we mean the intersection of all sets S
; such that:
;
;    1.  T is a member of S,
;    2.  NIL is a member of S, and
;    3.  for all x and y, if x and y are in S, then (CONS x y) is in S.

; Legend:
;  A function whose name begins "q-"  returns an ubdd.
;  A function whose name beqins "qv-" returns a list of ubdds.
;  A function whose name begins "qs-" is a set operation on ubdds.

; If, especially in the name of a function, we write 'bdd', we mean
; 'ubdd'.

; This paragraph sucks because it refers to variables, which are
; nowhere in sight.  This file defines a number of ubdd-related
; operations.  ubdds generally have three characteristics: each path
; from the root to a tip encounters each variable at most once, every
; path encounters variables in pre-specified order, and no pair of
; outgoing edges point to the same node (reduced).  Our ubdd
; definition does not reduce internal nodes unless both outgoing edges
; of a ubdd node point to the same constant.  As a result, we do not
; need to store the variable name in the ubdd nodes.  We do reduce our
; ubdds in the sense that constant values terminate any path.

(defabbrev qcar (x) (if (consp x) (car x) x))

(defabbrev qcdr (x) (if (consp x) (cdr x) x))

(defabbrev qcons (x y)
  (if (if (eq x t)
          (eq y t)
        (and (eq x nil) (eq y nil)))
      x
    (hons x y)))

; The three abbreviations above along with the two functions below
; provide the complete definition of our ubdd system.  The order of
; the ubdd variables is implicit -- there are no names, just the depth
; from the root.  Thus, an ubdd with only one variable can be either
; the reduced values T or NIL, or it can be, (HONS T NIL), or (HONS
; NIL T); (HONS T T) and (HONS NIL NIL) are not permitted, but reduced
; to T and NIL, respectively (see the definition of NORMP below).

(defn q-not (x)
  (if (atom x)
      (if x nil t)
    (hons (q-not (car x))
          (q-not (cdr x)))))

(defn q-ite (x y z)

  ":Doc-section Hons-and-Memoization

  if-then-else for ubdds.~/

  (Q-ITE x y z) expects three ubdds, which are to be interpreted at
  the same level.  Informally speaking. Q-ITE returns a single ubdd,
  also at the same level, that is 'equivalent' to (IF x y z).  The two
  theorems Q-ITE-CORRECT and NORMP-Q-ITE express formally what Q-ITE
  returns.~/~/"

  (cond
   ((null x) z)
   ((atom x) y)
   (t (let ((y (if (hqual x y) t y))
            (z (if (hqual x z) nil z)))
        (cond ((hqual y z) y)
              ((and (eq y t) (eq z nil)) x)
              ((and (eq y nil) (eq z t)) (q-not x))
              ;; ((eq z nil) (q-and x y))
              ;; ((eq z t)   (q-implies x y))
              ;; ((eq y t)   (q-or x y))
              ;; ((eq y nil) (q-and-c1 x y))
              (t (qcons (q-ite (car x) (qcar y) (qcar z))
                        (q-ite (cdr x) (qcdr y) (qcdr z)))))))))

; For these definitions to serve as an effective ubdd system, we
; memoize the functions Q-NOT and Q-ITE.


(defn normp (x)

 ":Doc-section Hons-and-Memoization

  Recognizer of ubdds.~/
  (NORMP x) returns T or NIL according to whether X is a well-formed
  ubdd, i.e., a rooted, binary tree, in T and NIL, with no node equal
  to '(T . T) or '(NIL . NIL).~/~/"

  (mbe :logic
       (if (atom x)
           (booleanp x)
         (and (normp (car x))
              (normp (cdr x))
              (if (atom (car x))
                  (not (equal (car x) (cdr x)))
                t)))

       :exec
       (cond ((eq x t) t)
             ((eq x nil) t)
             ((atom x) nil)
             (t (let ((a (car x))
                      (d (cdr x)))
                  (cond ((eq a t)
                         (cond ((eq d nil) t)
                               ((eq d t) nil)
                               (t (normp d))))
                        ((eq a nil)
                         (cond ((eq d nil) nil)
                               ((eq d t) t)
                               (t (normp d))))
                        (t (and (normp a) (normp d)))))))))

(defn normp-list (x)
  (if (atom x) t (and (normp (car x)) (normp-list (cdr x)))))

(defn eval-bdd (x values)

  "(EVAL-bdd x values) is the 'value' of X with respect to VALUES.

   X is normally a CONS tree of Booleans and VALUES is normally a
   TRUE-LISTP of Booleans, i.e., Ts and NILs.  (Typically, X is T,
   NIL, or a 'HONSP' NORMP.)  Of course, since EVAL-BDD's guard is T,
   it can be given any two ACL2 objects as arguments.

   If X is an atom, then X is its own 'value'; otherwise, we use the
   CAR and CDR of VALUES, say A and D, to guide us further through X.
   (If VALUES is an atom, we use NIL for both A and D.)  If A is NIL
   the answer is the value of (CDR X) with respect to D; otherwise the
   answer is the value of (CAR X) with respect to D.

   One can think of the VALUES argument to EVAL-BDD as having its last
   atom replaced with an infinite list of NILs."

  (if (atom x)
      x
    (if (atom values)
        (eval-bdd (cdr x) nil)
      (if (car values)
          (eval-bdd (car x) (cdr values))
        (eval-bdd (cdr x) (cdr values))))))

(defthm normp-implies-eval-bdd-blp
  (implies (normp x)
           (booleanp (eval-bdd x vals))))

(defn eval-bdd-list (bdds values)
  (if (atom bdds)
      nil
    (hons (eval-bdd (car bdds) values)
          (eval-bdd-list (cdr bdds) values))))

; Assuming variable names are ordered by their location in a list,
; LOCN returns the location of a variable in a list.  (QVAR-N i)
; creates the ith ubdd variable.  Variable names are a mere
; convenience.  We have tried not to impose any unnecessary
; restriction on variables names; however, since we usually only use
; symbols and natural numbers for variable names we have sometimes
; used the EQLABLEP guard on variables.

(defn locn-acc (v vs acc)
  (declare (xargs :guard (integerp acc)))
  (cond ((atom vs) acc)
        ((equal v (car vs)) acc)
        (t (locn-acc v (cdr vs) (1+ acc)))))

(defn locn (v vs)
  (declare (xargs :guard t
                  :verify-guards nil))
  (mbe
   :logic
   (cond ((atom vs) 0)
         ((equal v (car vs)) 0)
         (t (1+ (locn v (cdr vs)))))
   :exec
   (locn-acc v vs 0)))

(defthm locn-is-locn-acc
  (implies (natp acc)
           (equal (locn-acc v vars acc)
                  (+ acc (locn v vars)))))

(verify-guards locn)

(defn qvar-n (n)
  (declare (xargs :guard (natp n)))
  (mbe
   :logic
   (cond ((not (natp n)) nil)
         ((= n 0) (hons t nil))
         (t (let ((x (qvar-n (1- n))))
              (hons x x))))
   :exec
   (cond ((int= n 0) (hons t nil))
         (t (let ((x (qvar-n (1- n))))
              (hons x x))))))

(defthm consp-qvar-n
  (implies (and (integerp n)
                (<= 0 n))
           (consp (qvar-n n))))

(defthm normp-qvar-n
  (normp (qvar-n n)))

(in-theory (disable qvar-n))

(defn var-to-tree (var vars) (qvar-n (locn var vars)))

(defthm normp-var-to-tree
  (normp (var-to-tree var vars)))

(in-theory (disable var-to-tree))

(defn var-to-tree-list (variables vars)
  (if (atom variables) nil
    (hons (var-to-tree (car variables) vars)
          (var-to-tree-list (cdr variables) vars))))

;                      *B0* and *B1*

(defconst *b1* t

  "The constant *B1*, which has value T, plays at least four roles:

     (a) *B1* represents 'true'.

     (b) *B1* represents 'bit 1' in bit vectors.

     (c) *B1* represents 'negative' as an arithmetic sign in a general
         integer.

     (d) *B1* refers to the the CAR side of a CONSP NORMP.")

(defconst *b0* nil

  "The constant *B0*, which always has value NIL, represents 'false',
  'bit 0', 'positive as an arithmetic sign', 'CDR side', and, of
  course, the empty list.")

(defconst *list-b1* (hist *b1*))

(defconst *list-b0* (hist *b0*))

(defmacro is-b1 (x) `(eq ,x t))

(defmacro is-b0 (x) `(eq ,x nil))

(defmacro if-bbb (x y z)

  "(IF-BBB x y z) is equal to (Q-ITE x y z).  IF-BBB is a
  'short-circuit' or 'lazy' version of Q-ITE that avoids evaluating y
  if x evaluates to *B0* and avoids evaluating z if x evaluates to
  *B1*."

; A possible improvement to IF-BBB: macroexpansion of IF-BBB terms
; could result in less code.  The double appearances of y and z could
; be eliminated with an FLET of two functions.  But currently, ACL2
; does support not FLET unless all the free vars in the body are among
; the args.

  `(let ((if-bbb-x-do-not-use-elsewhere ,x))
     (cond
      ((is-b1 if-bbb-x-do-not-use-elsewhere) ,y)
      ((is-b0 if-bbb-x-do-not-use-elsewhere) ,z)
      (t (let* ((if-bbb-y-do-not-use-elsewhere ,y)
                (if-bbb-z-do-not-use-elsewhere ,z))
           (q-ite if-bbb-x-do-not-use-elsewhere
                  if-bbb-y-do-not-use-elsewhere
                  if-bbb-z-do-not-use-elsewhere))))))


(defmacro and-bb (x y) `(if-bbb ,x ,y *b0*))

(defn iff-bb (x y) (if-bbb x y (q-not y)))

(defn xor-bb (x y) (if-bbb x (q-not y) y))

(defn not-b (x) (q-not x))

(defmacro or-bb (x y) `(if-bbb ,x *b1* ,y))

(defabbrev maj-bbb (c a b) (if-bbb c (or-bb a b) (and-bb a b)))


; We define additional ubdd-operations that can sometime provide
; better efficiency than only using Q-ITE through the use of specific
; function memoization.

(defn q-not-ite (x)
  (q-ite x nil t))

(defn q-and (x y)
  (if (atom x)
      (if x y nil)
    (if (atom y)
        (if y x nil)
      (if (hqual x y)
          x
        (let ((l (q-and (car x) (car y)))
              (r (q-and (cdr x) (cdr y))))
          (qcons l r))))))

(defn q-and-ite (x y)
  (q-ite x y nil))

; It would be nice here to have:
;    (thm (equal (q-and x y) (q-and-ite x y))).

(defn q-or (x y)
  (if (atom x)
      (if x t y)
    (if (atom y)
        (if y t x)
      (if (hqual x y)
          x
        (let ((l (q-or (car x) (car y)))
              (r (q-or (cdr x) (cdr y))))
          (qcons l r))))))

(defn q-or-ite (x y)
  (q-ite x t y))

(defn q-implies (x y)
  ;; aka q-or-c1
  (if (atom x)
      (if x y t)
    (if (atom y)
        (if y t (q-not x))
      (if (hqual x y)
          t
        (let ((l (q-implies (car x) (car y)))
              (r (q-implies (cdr x) (cdr y))))
          (qcons l r))))))

(defn q-implies-ite (x y)
  ;; aka q-or-c1
  (q-ite x y t))

(defn q-or-c2 (x y)
  (if (atom y) ; y tested for to emulate q-or-c2-ite
      (if y x t)
    (if (atom x)
        (if x t (q-not y))
      (if (hqual x y)
          t
        (let ((l (q-or-c2 (car x) (car y)))
              (r (q-or-c2 (cdr x) (cdr y))))
          (qcons l r))))))

(defn q-or-c2-ite (x y)
  ;; aka y->x
  (q-ite y x t))

(defn q-and-c1 (x y)
  (if (atom x)
      (if x nil y)
    (if (atom y)
        (if y (q-not x) nil)
      (if (hqual x y)
          nil
        (let ((l (q-and-c1 (car x) (car y)))
              (r (q-and-c1 (cdr x) (cdr y))))
          (qcons l r))))))

(defn q-and-c1-ite (x y)
  (q-ite x nil y))

(defn q-and-c2 (x y)
  (if (atom x)
      (if x (q-not y) nil)
    (if (atom y)
        (if y nil x)
      (if (hqual x y)
          nil
        (let ((l (q-and-c2 (car x) (car y)))
              (r (q-and-c2 (cdr x) (cdr y))))
          (qcons l r))))))

(defn q-and-c2-ite (x y)
  (q-ite y nil x))

(defn q-iff (x y)
  (if (atom x)
      (if x y (q-not y))
    (if (atom y)
        (if y x (q-not x))
      (if (hqual x y)
          t
        (let ((l (q-iff (car x) (car y)))
              (r (q-iff (cdr x) (cdr y))))
          (qcons l r))))))

(defn q-iff-ite (x y)   ; why call q-not rather than q-ite?
  (if-bbb x y (q-not y)))
      
(defn q-nand (x y)
  (if (atom x)
      (if x (q-not y) t)
    (if (atom y)
        (if y (q-not x) t)
      (if (hqual x y)
          (q-not x)
        (let ((l (q-nand (car x) (car y)))
              (r (q-nand (cdr x) (cdr y))))
          (qcons l r))))))
      
(defn q-nand-ite (x y)
  (if-bbb x (q-not y) t))

(defn q-nor (x y)
  (if (atom x)
      (if x nil (q-not y))
    (if (atom y)
        (if y nil (q-not x))
      (if (hqual x y)
          (q-not x)
        (let ((l (q-nor (car x) (car y)))
              (r (q-nor (cdr x) (cdr y))))
          (qcons l r))))))

(defn q-nor-ite (x y)
  (if-bbb x nil (q-not y)))

(defn q-xor (x y)
  (if (atom x)
      (if x (q-not y) y)
    (if (atom y)
        (if y (q-not x) x)
      (if (hqual x y)
          nil
        (let ((l (q-xor (car x) (car y)))
              (r (q-xor (cdr x) (cdr y))))
          (qcons l r))))))

(defn q-xor-ite (x y)

; why call atom, q-not, and hqual rather than q-ite?

  (if (atom x)
      (if x (q-not y) y)
    (if (atom y)
        (if y (q-not x) x)
      (if (hqual x y)
          nil
        (if-bbb x (q-not y) y)))))

; End of the 10 q-functions of two arguments.


(defn q-buf (x)         x)

(defn q-or3   (w x y)   (q-or  w (q-or  x y)))

(defn q-and3  (w x y)   (q-and w (q-and x y)))

(defn q-or4   (w x y z) (q-or  w (q-or  x (q-or  y z))))

(defn q-and4  (w x y z) (q-and w (q-and x (q-and y z))))

(defn q-nor3  (w x y)   (q-not (q-or3  w x y)))

(defn q-nand3 (w x y)   (q-not (q-and3 w x y)))

(defn q-nor4  (w x y z) (q-not (q-or4  w x y z)))

(defn q-nand4 (w x y z) (q-not (q-and4 w x y z)))


; (defn qs-complement (x full-set) (q-and-c1 x full-set))

; Conjecture:  (qs-subset x y) is an efficient implementation of
; (eq t (q-implies x y)).

(defn qs-subset (x y)
  (cond ((atom x)
         (if x (eq y t) t))
        ((atom y) y)
        ((hqual x y) t)
        (t (and (qs-subset (car x) (car y))
                (qs-subset (cdr x) (cdr y))))))

;; Composes the Boolean function represented by ubdd X with those
;; represented by ubdds in the list L.

(defn q-compose (x l)
  (if (atom x)
      x
    (if (atom l)
        (q-compose (cdr x) nil)
      (if-bbb (car l)
              (q-compose (car x) (cdr l))
              (q-compose (cdr x) (cdr l))))))

(defn q-compose-list (xs l)
  (if (atom xs)
      nil
    (cons (q-compose (car xs) l)
          (q-compose-list (cdr xs) l))))

(defn q-restrict (x n v vars)
  
  ;; Needs to be memoized.  Q-RESTRICT takes an ubdd X, a value N (T
  ;; or NIL), a variable V, which is a member of the list of variables
  ;; VARS with respect to which X is an ubdd.  Q-RESTRICT returns the
  ;; ubdd corresponding to the formula that one obtains by simplifying
  ;; every internal node in X corresponding to variable V to N.  Thus,
  ;; if an ubdd with variables '(A B C) has variable B restricted to
  ;; NIL, then both outgoing edges from every internal node Y at
  ;; "level" B will point to the (CDR Y).

  ;; This like forming (LET ((V N)) X) and simplifying the resulting
  ;; expression.

  (declare (xargs :guard (and (eqlablep v)
                              (eqlable-listp vars))))
  (if (atom x)
      x
    (if (eql v (car vars))
        (if n
            (qcons (car x) (car x))
          (qcons (cdr x) (cdr x)))
      (qcons (q-restrict (car x) n v (cdr vars))
             (q-restrict (cdr x) n v (cdr vars))))))

(defn q-restrict-shrink (x n v vars)
  
  ;; Q-RESTRICT-SHRINK should to be memoized.  Q-RESTRICT-SHRINK takes
  ;; an ubdd X, a value N (t or nil), a variable V, which is a member
  ;; of the list of variables VARS with respect to which X is an ubdd.
  ;; q-RESTRICT-SHRINK returns the ubdd corresponding to the formula
  ;; that one obtains by substituting N for X in the formula to which
  ;; X corresponds.

  ;; Suttle point: the var V is eliminated.  Always know which VARS
  ;; list you are using!

  (declare (xargs :guard (and (eqlablep v)
                              (eqlable-listp vars))))
  (if (atom x)
      x
    (if (eql v (car vars))
        (if n (car x) (cdr x))
      (qcons (q-restrict-shrink (car x) n v (cdr vars))
             (q-restrict-shrink (cdr x) n v (cdr vars))))))

; Q-REORDER is an ubdd variable reorder function.  DELETE-HQL is
; defined to return a unique (HONSP) object.  For the memoization of
; Q-REORDER to work best, it should be called as (Q-REORDER x
; (HONS-COPY vars) (HONS-COPY nvars)) which will ensure that unique
; objects are supplied.

(defn delete-hql (x l)
  (declare (xargs :guard (eqlablep x)))
  (cond ((atom l) nil)
        ((eql x (car l))
         (cdr l))
        (t (hons (car l) (delete-hql x (cdr l))))))

(defthm symbol-listp-delete-hql
  (implies (eqlable-listp l)
           (eqlable-listp (delete-hql x l))))

(defn q-reorder (x vars nvars)
  
  ;; Needs to be memoized.  VARS and NVARS should be of the same
  ;; length.  X is an ubdd.  Q-REORDER returns the ubdd whose meaning
  ;; with respect to NVARS is equivalent to to the meaning of X with
  ;; respect to VARS.
  
  (declare (xargs :guard (and (eqlable-listp vars)
                              (eqlable-listp nvars))
                  :measure (acl2-count nvars)))
  (if (or (atom x)
          (atom nvars)) ;; could be eliminated
      x
    (if (eql (car vars) (car nvars))
        ;; It may be possible to simplify the QCONS function calls
        ;; here to HONS function calls.
        (qcons (q-reorder (car x) (cdr vars) (cdr nvars))
               (q-reorder (cdr x) (cdr vars) (cdr nvars)))
      (qcons (q-reorder (q-restrict-shrink x t (car nvars) vars)
                        (delete-hql (car nvars) vars)
                        (cdr nvars))
             (q-reorder (q-restrict-shrink x nil (car nvars) vars)
                        (delete-hql (car nvars) vars)
                        (cdr nvars))))))

(defun q-restrict-alist (x bindings vars)

  ;; See also Q-RESTRICT.

  ;; (Q-RESTRICT-ALIST x bindings vars) is somewhat similar to forming
  ;; (let bindings x) and simplifying the resulting expression.

  ;; Should this be re-written to use Q-ITE and obviate the need to
  ;; memoize this function?  Probably not.

  (declare (xargs :guard (eqlable-alistp bindings)))
  (if (atom x)
      x
    (if (atom vars)
        x
      (let ((pair (assoc (car vars) bindings)))
        (if pair
            (let ((x-below (q-restrict-alist
                            (if (cdr pair) (car x) (cdr x))
                            bindings (cdr vars))))
              (qcons x-below x-below))
          (qcons (q-restrict-alist (car x) bindings (cdr vars))
                 (q-restrict-alist (cdr x) bindings (cdr vars))))))))

(defun q-restrict-alist-list (x-lst bindings vars)
  (declare (xargs :guard (eqlable-alistp bindings)))
  (if (atom x-lst)
      nil
    (cons (q-restrict-alist (car x-lst) bindings vars)
          (q-restrict-alist-list (cdr x-lst) bindings vars))))


(defn q-reorder-down-one (x var vars)
  ;; This function "swaps" variable VAR with the variable just below
  ;; it in the variable order.
  (declare (xargs :guard (eqlablep var)))
  (if (atom x)
      x
    (if (atom vars)
        x
      (if (eql (car vars) var)
          ;; Perform the swap.
          (qcons (qcons (qcar (qcar x))
                        (qcar (qcdr x)))
                 (qcons (qcdr (qcar x))
                        (qcdr (qcdr x))))          
        (hons (q-reorder-down-one (car x) var (cdr vars))
              (q-reorder-down-one (cdr x) var (cdr vars)))))))


#||

(defn find-best-position-helper (bdd var max-var)
  (loop for 

(defn find-best-position (bdd var)
  (let ((max-var (max-depth bdd)))
    (if (< max-var var)
        bdd
      (find-best-position-helper bdd var max-var)

||#

(defn q-exists-shrink (x E-vars vars)

  ;; E-vars must be a subset of VARS and its variables must appear in
  ;; the same order as they do in VARS.  Q-EXISTS-SHRINK returns an
  ;; answer that has meaning with respect to the deletion of the
  ;; members of E-vars from VARS.

  (declare (xargs :guard (and (eqlable-listp E-vars)
                              (eqlable-listp vars))))
  (if (or (atom x)
          (atom E-vars))
      x
    (if (eql (car E-vars) (car vars))
        (q-or (q-exists-shrink (car x) (cdr E-vars) (cdr vars))
              (q-exists-shrink (cdr x) (cdr E-vars) (cdr vars)))
      (qcons (q-exists-shrink (car x) E-vars (cdr vars))
             (q-exists-shrink (cdr x) E-vars (cdr vars))))))

(defn q-exists (x E-vars vars)

  ;; E-vars must be a subset of VARS and its variables must appear in
  ;; the same order as they do in VARS.  Q-EXISTS returns an answer
  ;; that has meaning with respect to VARS.

  (declare (xargs :guard (and (eqlable-listp E-vars)
                              (eqlable-listp vars))))
  (if (or (atom x)
          (atom E-vars))
      x
    (if (eql (car E-vars) (car vars))
        (let ((below
               (q-or (q-exists (car x) (cdr E-vars) (cdr vars))
                     (q-exists (cdr x) (cdr E-vars) (cdr vars)))))
          (qcons below below))
      (qcons (q-exists (car x) E-vars (cdr vars))
             (q-exists (cdr x) E-vars (cdr vars))))))

(defn q-for-all-shrink (x E-vars vars)

  ;; E-vars must be a subset of VARS and its variables must appear in
  ;; the same order as they do in VARS.  Q-FOR-ALL-SHRINK returns an
  ;; answer that has meaning with respect to the deletion of the
  ;; members of E-vars from VARS.

  (declare (xargs :guard (and (eqlable-listp E-vars)
                              (eqlable-listp vars))))
  (if (or (atom x)
          (atom E-vars))
      x
    (if (eql (car E-vars) (car vars))
        (q-and (q-for-all-shrink (car x) (cdr E-vars) (cdr vars))
               (q-for-all-shrink (cdr x) (cdr E-vars) (cdr vars)))
      (qcons (q-for-all-shrink (car x) E-vars (cdr vars))
             (q-for-all-shrink (cdr x) E-vars (cdr vars))))))

(defn q-for-all (x E-vars vars)

  ;; E-vars must be a subset of VARS and its variables must appear in
  ;; the same order as they do in VARS.  Q-FOR-ALL returns an answer
  ;; that has meaning with respect to VARS.

  (declare (xargs :guard (and (eqlable-listp E-vars)
                              (eqlable-listp vars))))
  (if (or (atom x)
          (atom E-vars))
      x
    (if (eql (car E-vars) (car vars))
        (let ((below
               (q-and (q-for-all (car x) (cdr E-vars) (cdr vars))
                      (q-for-all (cdr x) (cdr E-vars) (cdr vars)))))
          (qcons below below))
      (qcons (q-for-all (car x) E-vars (cdr vars))
             (q-for-all (cdr x) E-vars (cdr vars))))))

(defn q-exists-one-var (x v vars)
  (declare (xargs :guard (and (eqlablep v)
                              (eqlable-listp vars))))
  (q-or (q-restrict x  t  v vars)
        (q-restrict x nil v vars)))

(defn q-for-all-one-var (x v vars)
  (declare (xargs :guard (and (eqlablep v)
                              (eqlable-listp vars))))
  (q-and (q-restrict x  t  v vars)
         (q-restrict x nil v vars)))

(defn q-exists-one-var-shrink (x v vars)
  (declare (xargs :guard (and (eqlablep v)
                              (eqlable-listp vars))))
  (q-or (q-restrict-shrink x  t  v vars)
        (q-restrict-shrink x nil v vars)))

(defn q-for-all-one-var-shrink (x v vars)
  (declare (xargs :guard (and (eqlablep v)
                              (eqlable-listp vars))))
  (q-and (q-restrict-shrink x  t  v vars)
         (q-restrict-shrink x nil v vars)))


; To ease the use of our ubdd system, we have defined some functions
; that let a user write expressions in a typical Lisp style.  Such
; expressions are then converted into IF-expressions, before they are
; converted into ubdds.

(defn good-to-if-p (x)
  ;; GOOD-TO-IF-P recognizes a well-formed IF-expression.
  (if (atom x)
      (eqlablep x)
    (let ((fn (car x))
          (args (cdr x)))
      (case fn
        (if (and (consp args)
                 (consp (cdr args))
                 (consp (cddr args))
                 (null (cdddr args))
                 (good-to-if-p (car args))
                 (good-to-if-p (cadr args))
                 (good-to-if-p (caddr args))))
        (otherwise nil)))))

(defn nmake-if (test true false)
  (declare (xargs :guard (and (good-to-if-p test)
                              (good-to-if-p true)
                              (good-to-if-p false))))
  (cond ((eq test t)
         true)
        ((eq test nil)
         false)
        ((and (consp test) (eq 'if (car test))
              (null (caddr test)) (eq t (cadddr test)))
         (nmake-if (cadr test) false true))
        (t (let* ((true (if (hqual test true) t true))
                  (true (if (and (consp true)
                                 (hqual test (cadr true)))
                            (caddr true)
                          true))
                  (false (if (hqual test false) nil false))
                  (false (if (and (consp false)
                                  (hqual test (cadr false)))
                             (cadddr false)
                           false)))
             (cond ((hqual true false) true)
                   ((and (eq true t) (eq false nil))
                    test)
                   (t (hist 'if test true false)))))))

(defn to-if-error-p (x)
  (and (consp x)
       (stringp (car x))))

(defthm good-to-if-nmake-if
  (implies (and (good-to-if-p x)
                (good-to-if-p y)
                (good-to-if-p z))
           (good-to-if-p (nmake-if x y z))))

(defthm eqlablep-of-nmake-if
  (implies (and (good-to-if-p x)
                (good-to-if-p y)
                (good-to-if-p z)
                (not (consp (nmake-if x y z))))
           (eqlablep (nmake-if x y z))))

(defthm consp-of-nmake-if
  (implies (and (good-to-if-p x)
                (good-to-if-p y)
                (good-to-if-p z)
                (not (eqlablep (nmake-if x y z))))
           (consp (nmake-if x y z))))

(in-theory (disable nmake-if))

(defn to-if-subst (new old term)
  ;; Substitute new for the atom, old, in term.  Note that if old is not an
  ;; atom then this function will return the given good-to-if-p term
  ;; unchanged.
  (declare (xargs :guard (good-to-if-p term)))
  (cond ((atom term)
         (cond ((eq term t) t)
               ((eq term nil) nil)
               ((eql term old) new)
               (t term)))
        (t (hist 'if
                 (to-if-subst new old (cadr term))
                 (to-if-subst new old (caddr term))
                 (to-if-subst new old (cadddr term))))))

(defthm good-to-if-p-to-if-subst
  (implies (and (good-to-if-p new)
                (good-to-if-p term))
           (good-to-if-p (to-if-subst new old term))))

(defthm atom-to-if-implies-eqlablep-to-if-subst
  (implies (and (not (consp (to-if-subst new old term)))
                (good-to-if-p new)
                (good-to-if-p term))
           (eqlablep (to-if-subst new old term))))

(defconst *and-synonyms*   '(and & *))
(defconst *or-synonyms*    '(or \| +))
(defconst *iff-synonyms*   '(iff eq eql equal eqv xnor =
                                 == equiv <-> <=>))
(defconst *if-synonyms*    '(if ite mux))
(defconst *not-synonyms*   '(not ~))
(defconst *xor-synonyms*   '(xor exor))
(defconst *nand-synonyms*  '(nand))
(defconst *nor-synonyms*   '(nor))
(defconst *andc1-synonyms* '(andc1))
(defconst *andc2-synonyms* '(andc2))
(defconst *orc1-synonyms*  '(orc1 implies -> =>))
(defconst *orc2-synonyms*  '(orc2))

(defn to-if (term)
  (declare (xargs :verify-guards nil))

  ":Doc-section Hons-and-Memoization

   Recognizer for the TO-IF langauge ~/

   (TO-IF x) is a recognizer for objects in the TO-IF language, which
   may be used for writing Boolean expressions.  The TO-IF language is
   a subset of the TO-IF2 language.

   If X is in the TO-IF language, then (TO-IF x) returns an equivalent
   member of the TO-IF language expressed in the limited vocabulary of
   IF, T, NIL, and variables.  The result returned is not in any
   particular normal form, but it is in the form expected by the
   function QNORM1.

   If X is not in the TO-IF language, then (TO-IF x) returns a CONS
   whose CAR is a string that may help explain in what sense X is not
   in the TO-IF language.

   Though similar to the language of ACL2, the TO-IF language is NOT
   the same as the ACL2 langauge or the TO-IF2 language, so watch out!

   (TERM-EVAL (TO-IF term) vars vals) gives the meaning of (TO-IF
   TERM) with respect to the binding of the variables in VARS to the
   Booleans in VALS.

   Informally, in the TO-IF language, T and NIL both are and denote
   the Boolean constants.  All eqlable ACL2 atoms (i.e., symbols,
   integers, rational, complex numbers, characters, but not strings)
   are variables in the TO-IF language.  The variables denote Boolean
   values, i.e., T and NIL.

   Merely for emphasis: The integer 2 is a variable in the TO-IF
   language, odd as that may seem at first.

   Merelly for emphasis:  The string \"2\" is not a TO-IF variable.

   (IF x y z) means what Y means if X means T and means what Z means
   if X means NIL.

   (TO-IF `(LET ,x ,y ,z)) is the result of simultaneously replacing
   in (TO-IF z) all the occurrences of the variable x with
   (TO-IF y).  Note that although in Lisp, one might write:
   (let ((x y)) z), the TO-IF 'LET' takes exactly three arguments.

   In a TO-IF expression one may also use the unary operator NOT and
   the binary operators AND, OR, IFF, IMPLIES, XOR, NAND, NOR, ANDC1,
   ORC1, and ORC2.

   TO-IF does not handle quantifiers such as FORALL nor FORSOME, nor
   does it permit operators to take a variable number of arguments.
   For such features, see TO-IF2.

   There are many synonyms for the many familar logical operators.
   Invoke (SAT-HELP) to see them all.  There is no facility
   for a user to extend these synonyms.
    ~/~/"

  (cond ((atom term)
         (cond ((eqlablep term) term)
               (t (hist "Illegal argument to to-if ~a." term))))
        ;; Zero Arguments
        ((to-if-error-p term) term)
        ((not (eqlablep (car term)))
         (hist "Illegal argument to to-if ~a." term))
        ((atom (cdr term))
         (cond ((not (null (cdr term)))
                (hist "Illegal argument to to-if ~a." term))
               ((member (car term) *and-synonyms*) t)
               ((member (car term) *or-synonyms*) nil)
               (t (hist "Illegal argument to to-if ~a." term))))
        ;; One Argument
        ((atom (cddr term))
         (cond ((not (null (cddr term)))
                (hist "Illegal argument to to-if ~a." term))
               (t (let ((arg1 (to-if (cadr term))))
                    (cond ((to-if-error-p arg1)
                           (hist "Illegal argument to to-if ~a."
                                 term))
                          ((member (car term) *not-synonyms*)
                           (nmake-if arg1 nil t))
                          ((or (member (car term) *and-synonyms*)
                               (member (car term) *or-synonyms*))
                           arg1)
                          (t (hist "Illegal arg to to-if ~a."
                                   term)))))))
        ;; Two Arguments
        ((atom (cdddr term))
         (cond ((not (null (cdddr term)))
                (hist "Illegal argument to to-if ~a." term))
               (t (let ((arg1 (to-if (cadr term)))
                        (arg2 (to-if (caddr term))))
                    (cond ((to-if-error-p arg1) arg1)
                          ((to-if-error-p arg2) arg2)
                          ((member (car term) *and-synonyms*)
                           (nmake-if arg1 arg2 nil))
                          ((member (car term) *or-synonyms*)
                           (nmake-if arg1 t arg2))
                          ((member (car term) *iff-synonyms*)
                           (nmake-if arg1 arg2 (nmake-if arg2 nil t)))
                          ((member (car term) *orc1-synonyms*)
                           (nmake-if arg1 arg2 t))
                          ((member (car term) *orc2-synonyms*)
                           (nmake-if arg1 (nmake-if arg2 nil t) t))
                          ((member (car term) *andc1-synonyms*)
                           (nmake-if arg2 (nmake-if arg1 nil t) nil))
                          ((member (car term) *andc2-synonyms*)
                           (nmake-if arg1 (nmake-if arg2 nil t) nil))
                          ((member (car term) *xor-synonyms*)
                           (nmake-if arg1 (nmake-if arg2 nil t) arg2))
                          ((member (car term) *nand-synonyms*)
                           (nmake-if arg1 (nmake-if arg2 nil t) t))
                          ((member (car term) *nor-synonyms*)
                           (nmake-if arg1 nil (nmake-if arg2 nil t)))
                          (t (hist "Illegal arg to to-if ~a."
                                   term)))))))
        ;; LET Expression
        ((and (null (cddddr term)) (eq (car term) 'let))
         (let ((var (cadr term))
               (val (caddr term))
               (body (cadddr term)))
           (cond ((or (not (symbolp var))
                      (eq var t)
                      (eq var nil))
                  (hist "Bad bound variable ~a." var))
                 (t (let ((valt (to-if val))
                          (bodyt (to-if body)))
                      (cond ((to-if-error-p valt) valt)
                            ((to-if-error-p bodyt) bodyt)
                            (t (to-if-subst valt var bodyt))))))))
        ;; IF Expression
        ((and (null (cddddr term)) (member (car term) *if-synonyms*))
         (let ((arg1 (to-if (cadr term)))
               (arg2 (to-if (caddr term)))
               (arg3 (to-if (cadddr term))))
           (cond ((to-if-error-p arg1) arg1)
                 ((to-if-error-p arg2) arg2)
                 ((to-if-error-p arg3) arg3)
                 (t (nmake-if arg1 arg2 arg3)))))
        (t (hist "Illegal argument to to-if ~a." term))))

(defthm good-to-if-p-to-if
  (implies (not (to-if-error-p (to-if term)))
           (good-to-if-p (to-if term))))

(verify-guards to-if)

(defn eql-var-lessp (v1 v2)
  (declare (xargs :guard (and (eqlablep v1)
                              (eqlablep v2))))
  (cond ((characterp v1)
         (if (characterp v2)
             (< (char-code v1)
                (char-code v2))
           t))
        ((symbolp v1)
         (if (characterp v2)
             nil
           (if (symbolp v2)
               (symbol-< v1 v2)
             t)))
        (t (if (acl2-numberp v2)
               (if (< (imagpart v1) (imagpart v2))
                   t
                   (if (eql (imagpart v1) (imagpart v2))
                       (< (realpart v1) (realpart v2))
                       nil))
             nil))))

(in-theory (disable eql-var-lessp))
           
(defn var-lessp (v1 v2 var-order)
  (declare (xargs :guard (and (eqlablep v1)
                              (eqlablep v2)
                              (eqlable-listp var-order))))
  (let ((l1 (member v1 var-order))
        (l2 (member v2 var-order)))
    (if l1
        (if l2
            (and (not (eql v1 v2))
                 (member v2 l1))
          t)
      (if l2
          nil
        (eql-var-lessp v1 v2)))))

(in-theory (disable var-lessp))

(defn nmerge (l1 l2 var-order)
  (declare (xargs :guard (and (eqlable-listp l1)
                              (eqlable-listp l2)
                              (eqlable-listp var-order))
                  :measure (+ (acl2-count l1)
                              (acl2-count l2))))
  (cond ((atom l1) l2)
        ((atom l2) l1)
        ((eql (car l1) (car l2))
         (hons (car l1) (nmerge (cdr l1) (cdr l2) var-order)))
        ((var-lessp (car l1) (car l2) var-order)
         (hons (car l1)
               (nmerge (cdr l1) l2 var-order)))
        (t (hons (car l2)
                 (nmerge l1 (cdr l2) var-order)))))

(defthm eqlable-listp-nmerge
  (implies (and (eqlable-listp l1)
                (eqlable-listp l2)
                (eqlable-listp var-order))
           (eqlable-listp (nmerge l1 l2 var-order))))

(defn vars-help (term var-order)
  (declare (xargs :guard (and (good-to-if-p term)
                              (eqlable-listp var-order))
                  :verify-guards nil))
  (cond ((atom term)
         (cond ((or (eq term t) (eq term nil)) nil)
               (t (hist term))))
        (t (nmerge (vars-help (cadr term) var-order)
                   (nmerge (vars-help (caddr term) var-order)
                           (vars-help (cadddr term) var-order)
                           var-order)
                   var-order))))

(defthm eqlable-listp-vars-help
  (implies (and (good-to-if-p term)
                (eqlable-listp var-order))
           (eqlable-listp (vars-help term var-order))))

(verify-guards vars-help)
(in-theory (disable vars-help))

; VARS was defined to allow the use of CONS for intermediate partially
; sorted lists of symbols, and here we finally then make the list
; unique.

(defn vars (term var-order)
  (declare (xargs :guard (and (good-to-if-p term)
                              (eqlable-listp var-order))))
  (hopy-list-r (vars-help term var-order)))

(defthm eqlable-listp-hons-copy-list-r
  (implies (eqlable-listp x)
           (eqlable-listp (hons-copy-list-r x))))

(defthm eqlable-listp-vars
  (implies (and (good-to-if-p term)
                (eqlable-listp var-order))
           (eqlable-listp (vars term var-order))))


(defn qnorm1-guard (x)
  ;; Recognizes acceptable terms for QNORM.
  (if (atom x)
      (eqlablep x)
    (let ((fn (car x))
          (args (cdr x)))
      (case fn
        (if (and (consp args)
                 (consp (cdr args))
                 (consp (cddr args))
                 (null (cdddr args))
                 (qnorm1-guard (car args))
                 (qnorm1-guard (cadr args))
                 (qnorm1-guard (caddr args))))
        (quote (and (consp args)
                    (normp (car args))
                    (null (cdr args))))
        (otherwise nil)))))

(defn qnorm1 (term vars)

  ":Doc-section Hons-and-Memoization

   Creates ubdds.   ~/

   (QNORM1 term vars) returns the unique ubdd for TERM, an
   IF-expression, with respect to the variable ordering VARS. ~/~/"

  (declare (xargs :measure (acl2-count term)
                  :guard (and (qnorm1-guard term)
                              (eqlable-listp vars))))
  (cond ((eq term t) t)
        ((eq term nil) nil)
        ((atom term) (var-to-tree term vars))
        ((eq (car term) 'if)
         (let ((test (qnorm1 (cadr term) vars)))
           (cond ((eq test t)
                  (qnorm1 (caddr term) vars))
                 ((eq test nil)
                  (qnorm1 (cadddr term) vars))
                 (t (q-ite
                     test
                     (qnorm1 (caddr term) vars)
                     (qnorm1 (cadddr term) vars))))))
        ((eq (car term) 'quote) (cadr term))
        (t (list "Bad arg to qnorm1 ~a." term))))

(defn qnorm1-guard-list (l)
  (if (atom l)
      t
    (and (qnorm1-guard (car l))
         (qnorm1-guard-list (cdr l)))))

(defn qnorm1-list (l vars)
  (declare (xargs :guard (and (qnorm1-guard-list l)
                              (eqlable-listp vars))))
  (if (atom l)
      nil
    (cons (qnorm1 (car l) vars)
          (qnorm1-list (cdr l) vars))))


(defthm good-to-if-p-implies-qnorm1-guard
  (implies (good-to-if-p term)
           (qnorm1-guard term)))

(defn qnorm (term)

  ":Doc-section Hons-and-Memoization

   Creates ubdds.   ~/

  (QNORM term) returns the unique ubdd for TERM, an expression in
  the TO-IF language, with respect to the variable ordering returned
  by (VARS (TO-IF TERM) NIL).

  If TERM is a tautology, then QNORM returns T.  If term is
  a contradiction, then QNORM returns NIL.  If term is satisfiable,
  then QNORM returns a CONSP ubdd.~/~/"

  (let ((term (to-if term)))
    (cond ((to-if-error-p term) term)
          (t (qnorm1 term (vars term nil))))))

(defn qnorm-list (l vars)
  (declare (xargs :guard (eqlable-listp vars)))
  (cond ((atom l) nil)
        (t (let* ((term (to-if (car l)))
                  (term (if (to-if-error-p term)
                            term
                          (qnorm1 term vars))))
           (hons term
                 (qnorm-list (cdr l) vars))))))

(defn qtaut (term)
  (let ((x (to-if term)))
    (cond ((to-if-error-p x) x)
          (t (let ((vars (vars x nil)))
               (eq 't
                   (qnorm1 x vars)))))))

(defn qsublis (alist term)
  (declare (xargs :guard (and (good-to-if-p term)
                              (eqlable-alistp alist))))
  (cond ((atom term)
         (let ((ans (assoc term alist)))
           (if ans (cdr ans) term)))
        (t (hist 'if
                 (qsublis alist (cadr term))
                 (qsublis alist (caddr term))
                 (qsublis alist (cadddr term))))))

(defn t-nil-tree (x)
  (if (atom x)
      (or (eq x t) (eq x nil))
    (and (t-nil-tree (car x))
         (t-nil-tree (cdr x)))))

(defn q-to-if (term vars)
  (declare (xargs :guard (and (t-nil-tree term)
                              (eqlable-listp vars))))
  (if (atom term)
      term
    (let ((l (q-to-if (car term) (cdr vars)))
          (r (q-to-if (cdr term) (cdr vars))))
      (nmake-if (car vars) l r))))

(defthm good-to-if-p-is-q-to-if
  (implies (and (t-nil-tree term)
                (eqlable-listp vars))
           (good-to-if-p (q-to-if term vars))))

(defn re-order (term oldvars newvars)
  (declare (xargs :guard (and (t-nil-tree term)
                              (eqlable-listp oldvars)
                              (eqlable-listp newvars))))
  (qnorm1 (q-to-if term oldvars) newvars))


; A small set of tests to check our (normalizer-based) tautology
; checker.

(defn common-tautologies ()

  "(COMMON-TAUTOLOGIES) is a list of terms in the TO-IF language each
  of which is a propositional truth, i.e., is a tautology, i.e., has
  value T under all bindings of its variables."

  '((iff a a)
    (implies (and a b) a)
    (implies a (or a b))
    (iff (implies a (implies b c))
         (implies (and a b) c))
    (iff (implies a b) (or (not a) b))
    (iff (iff a b) (and (implies a b) (implies b a)))
    (iff (iff a b) (or (and a b) (and (not a) (not b))))
    (iff (implies a b) (implies (not b) (not a)))
    (iff (not a) (implies a nil))
    (iff (and a t) a)
    (iff (and a nil) nil)
    (iff (not t) nil)
    (iff (not nil) t)
    (iff (or a t) t)
    (iff (or a nil) a)
    (iff (iff a t) a)
    (iff (iff a nil) (not a))
    (iff (and a b) (and b a))
    (iff (or a b) (or b a))
    (iff (or a a) a)
    (iff (not (not a)) a)
    (iff (and a a) a)
    (iff (iff a a) t)
    (iff (xor a a) nil)
    (iff (iff a b) (iff b a))
    (iff (iff a (iff b c)) (iff (iff a b) c))
    (iff (and (or p (or q r))
              (or (not p) q))
         (and (or q r)
              (or (not p) q)))
    (implies (implies (not c) c) c)
    (iff (or a (or b c)) (or (or a b) c))
    (iff (and a (and b c)) (and (and a b) c))
    (iff (and a (or b c)) (or (and a b) (and a c)))
    (iff (or a (and b c)) (and (or a b) (or a c)))
    (iff (not (and a b)) (or (not a) (not b)))
    (iff (not (or a b)) (and (not a) (not b)))
    (iff (xor a b) (not (iff a b)))
    (iff (nor a b) (not (or a b)))
    (iff (nand a b) (not (and a b)))
    (iff (or a (iff b c)) (iff (or a b) (or a c)))
    (iff (and a (xor b c)) (xor (and a b) (and a c)))
    (iff (xor a (xor b c)) (xor (xor a b) c))
    (iff (if a b c) (and (implies a b) (implies (not a) c)))
    (iff (if t b c) b)
    (iff (if nil b c) c)
    (iff (if a b nil) (and a b))
    (iff (if a t b) (or a b))
    (iff (if a b b) b)
    (iff (if a a nil) a)
    (iff (if c b a) (if a (if b t (if c nil t)) (if b c nil)))
    (iff (if b2 a b1) (if a (if b1 t b2) (if b1 (if b2 nil t) nil)))
    (iff (if b1 a b2) (if a (if b1 t b2) (if b1 nil b2)))
    (iff (xor
          k
          (xor
           j
           (xor
            i
            (xor
             h
             (xor g (xor e (xor d (xor c (xor b a)))))))))
         (xor a (xor b (xor
                        c
                        (xor
                         d
                         (xor
                          e
                          (xor g (xor h (xor i (xor j k))))))))))))

(defn common-non-tautologies ()

  "(COMMON-NON-TAUTOLOGIES) is a short list of terms in the TO-IF
  language, each of which is a NOT a tautology."

  '(a
    (xor a b)
    (iff a b)
    (not a)
    (implies a b)
    (implies (or a b) (and a b))
    (iff (implies a b) (implies b a))
    (iff (implies a (implies b c)) (implies (implies a b) c))
    (iff (iff a (or b c)) (or (iff a b) (iff a c)))
    (iff (xor a (and b c)) (and (xor a b) (xor a c)))))

(defn check-q-true (l)
  (if (atom l)
      t
    (let ((term (to-if (car l))))
      (if (to-if-error-p term)
          nil
        (and (eq t (qnorm1 term (vars term nil)))
             (check-q-true (cdr l)))))))

(defn check-q-not-true (l)
  (if (atom l)
      t
    (let ((term (to-if (car l))))
      (if (to-if-error-p term)
          nil
        (and (not (eq t (qnorm1 term (vars term nil))))
             (check-q-not-true (cdr l)))))))

; We disable the executable counterparts so this theorem is checked
; each time this file is loaded.

(in-theory (disable (:executable-counterpart common-tautologies)
                    (:executable-counterpart common-non-tautologies)))

(in-theory (disable common-tautologies common-non-tautologies))

(defn check-q ()
  (and (check-q-true (common-tautologies))
       (check-q-not-true (common-non-tautologies))))

; As a way to i

(defn set-bdd (bdd loc v)
  (cond
   ((atom loc) v)
   ((car loc) (qcons (set-bdd (qcar bdd) (cdr loc) v) (qcdr bdd)))
   (t (qcons (qcar bdd) (set-bdd (qcdr bdd) (cdr loc) v)))))

(defn set-bdd-list (bdds loc vs)
  (if (or (atom vs) (atom bdds))
      nil
    (hons (set-bdd      (car bdds) loc (car vs))
          (set-bdd-list (cdr bdds) loc (cdr vs)))))

(defn set-bdd-pair-list (bdd-pairs loc vs)
  (if (or (atom vs)
          (atom bdd-pairs)
          (atom (car vs))
          (atom (car bdd-pairs)))
      nil
    (hons (hons (set-bdd (caar bdd-pairs) loc (caar vs))
                (set-bdd (cdar bdd-pairs) loc (cdar vs)))
          (set-bdd-pair-list (cdr bdd-pairs) loc (cdr vs)))))

(defconst *2t* t)

(defconst *2f* nil)

(defconst *4x* (hons t t))

(defconst *4u* (hons nil nil))

(defconst *4t* (hons t nil))

(defconst *4f* (hons nil t))

(defn to (x)
  (cond ((or (null x) (eq x 'f))         *4f*)
        ((eq x t)                        *4t*)
        ((or (eq x 'floating) (eq x 'u)) *4u*)
        (t                               *4x*)))

(defn to-list (l)
  (if (atom l) nil
    (cons (to (car l)) (to-list (cdr l)))))

(defn b-fix-eval-bdd (x values)
  (if (eval-bdd x values) t nil))

(defn qv-ite (c a b)
  (if (or (atom a) (atom b))
      nil
    (cons (q-ite c (car a) (car b))
          (qv-ite c (cdr a) (cdr b)))))

(defthm true-listp-qv-ite-if
  (true-listp (qv-ite c a b)))


;!!!  I want to everywhere change Q-IFF-LIST to Q-PAND-IFF-LIST.

(defn q-iff-list (x y)
  (if (or (atom x) (atom y))
      t
    (q-and-ite (q-iff-ite (car x) (car y))
               (q-iff-list (cdr x) (cdr y)))))

(defn or-c2 (x y) (or x (not y)))

(defn and-c1 (x y) (and (not x) y))

(defn and-c2 (x y) (and x (not y)))

 
; Finds a satisfying assignment for an ubdd.

(defn q-sat (x)
  (if (atom x)
      nil
    (if (eq (cdr x) nil)
        (cons t (q-sat (car x)))
      (cons nil (q-sat (cdr x))))))

; Given a list of ubdds, finds an assignment that satisfies at least
; one of them.

(defn q-sat-any (a)
  (if (atom a)
      nil
    (if (eq (car a) nil)
        (q-sat-any (cdr a))
      (q-sat (car a)))))

; Finds an assignment of ubdd variables which makes the two given ubdd
; vectors unequal.

; (defn find-ctrexample (a b)
;   (let ((xorlst (q-bv-xor a b)))
;    (q-sat-any xorlst)))

(defn q-and-is-nil (x y)
  (cond ((eq x t) (eq y nil))
        ((atom x) t)
        ((eq y t) nil)
        ((atom y) t)
        (t (and (q-and-is-nil (qcar x) (qcar y))
                (q-and-is-nil (qcdr x) (qcdr y))))))

(defn q-and-is-nilc2 (x y)
  (cond ((eq x t) (eq y t))
        ((atom x) t)
        ((eq y t) t)
        ((atom y) nil)
        (t (and (q-and-is-nilc2 (qcar x) (qcar y))
                (q-and-is-nilc2 (qcdr x) (qcdr y))))))

(defn q-not-is-atomic (x)
; returns T, NIL, or NOT-ATOMIC
  (if (atom x)
      (not x)
    'not-atomic))

(defabbrev atom-fix (y)
  (if (atom y) y 'not-atomic))

(defn q-ite-is-atomic (x y z)
  ; returns T, NIL, or NOT-ATOMIC
  (cond
   ((null x) (atom-fix z))
   ((atom x) (atom-fix y))
   (t (let ((y (if (hqual x y) t y))
            (z (if (hqual x z) nil z)))
        (cond ((hqual y z) (atom-fix y))
              ((and (eq y t) (eq z nil)) (atom-fix x))
              ((and (eq y nil) (eq z t)) (q-not-is-atomic x))
              (t (let ((a (q-ite-is-atomic
                           (car x) (qcar y) (qcar z)))
                       (d (q-ite-is-atomic
                           (cdr x) (qcdr y) (qcdr z))))
                   (cond ((or (eq a 'not-atomic)
                              (eq d 'not-atomic))
                          'not-atomic)
                         ((equal a d) a)
                         (t 'not-atomic)))))))))