hons-tests

(in-package "ACL2")

(comp t)

(memoize 'fib)

(defn tree-depth
  (x)
  (if (atom x)
    0
    (1+ (max (tree-depth (car x)) (tree-depth (cdr x))))))

(memoize 'build-tree)

(memoize 'tree-depth)

(defn make-list-of-numbers
  (n)
  (declare (xargs :guard (natp n)))
  (if (zp n)
    (list n)
    (hons n (make-list-of-numbers (1- n)))))

(comp 'make-list-of-numbers)

(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)))

(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)
  (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))
          (t (qcons (q-ite (car x) (qcar y) (qcar z))
              (q-ite (cdr x) (qcdr y) (qcdr z)))))))))

(defn normp
  (x)
  (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))))))

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

(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)))

(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))))))

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

(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))))

(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))

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

(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))

(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)
  (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) (q-ite x y t))

(defn q-or-c2
  (x y)
  (if (atom y)
    (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) (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) (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)
  (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)))))

(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-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))))))

(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)
  (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)
  (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))))))

(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))))))

(defn q-reorder
  (x vars nvars)
  (declare (xargs :guard (and (eqlable-listp vars) (eqlable-listp nvars))
      :measure (acl2-count nvars)))
  (if (or (atom x) (atom nvars))
    x
    (if (eql (car vars) (car nvars))
      (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))))))

(defn q-reorder-down-one
  (x var vars)
  (declare (xargs :guard (eqlablep var)))
  (if (atom x)
    x
    (if (atom vars)
      x
      (if (eql (car vars) var)
        (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 q-exists-shrink
  (x e-vars 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)
  (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)
  (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)
  (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)))

(defn good-to-if-p
  (x)
  (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))))

(defn to-if-subst
  (new old term)
  (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))))))

(defn to-if
  (term)
  (declare (xargs :verify-guards nil))
  (cond ((atom term) (cond ((eqlablep term) term)
        (t (hist "Illegal argument to to-if ~a." term))))
    ((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))))
    ((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)))))))
    ((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)))))))
    ((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))))))))
    ((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))))

(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))))

(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)))))

(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)))))

(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))))

(verify-guards vars-help)

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

(defn qnorm1-guard
  (x)
  (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))))
        '(and (consp args) (normp (car args)) (null (cdr args)))
        (otherwise nil)))))

(defn qnorm1
  (term 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))))

(defn qnorm
  (term)
  (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))))

(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))

(defn common-tautologies
  nil
  "(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
  nil
  "(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)))))))

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

(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)))))

(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)))))

(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)))

(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))))))

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

(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)
  (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)
  (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)))))))))

(memoize 'q-ite
  :condition '(and (consp x) (or (consp y) (consp z))))

(memoize 'qnorm1)

(memoize 'qvar-n)

(defn lfoo
  (x)
  (if (atom x)
    0
    (+ 1 (lfoo (cdr x)))))

(memoize 'lfoo)

(defxdoc normp
  :parents (hons-and-memoization)
  :short "Recognizer of ubdds."
  :long "<p>
 (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).</p>

 ")

(defxdoc q-ite
  :parents (hons-and-memoization)
  :short "If-then-else for ubdds."
  :long "<p>
 (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.</p>

 ")

(defxdoc qnorm
  :parents (hons-and-memoization)
  :short "Creates ubdds."
  :long "<p>
 (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).</p>

 <p>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.</p>

 ")

(defxdoc qnorm1
  :parents (hons-and-memoization)
  :short "Creates ubdds."
  :long "<p>
 (QNORM1 term vars) returns the unique ubdd for TERM, an IF-expression, with
 respect to the variable ordering VARS.</p>

 ")

(defxdoc to-if
  :parents (hons-and-memoization)
  :short "Recognizer for the TO-IF langauge"
  :long "<p>
 (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.</p>

 <p>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.</p>

 <p>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.</p>

 <p>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!</p>

 <p>(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.</p>

 <p>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.</p>

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

 <p>Merelly for emphasis: The string "2" is not a TO-IF variable.</p>

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

 <p>(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.</p>

 <p>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.</p>

 <p>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.</p>

 <p>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.</p>

 ")