bdd

(defun bdd-constructors
  (wrld)
  (declare (xargs :guard (and (plist-worldp wrld)
        (alistp (table-alist 'acl2-defaults-table wrld)))))
  (let ((pair (assoc-eq :bdd-constructors (table-alist 'acl2-defaults-table wrld))))
    (if pair
      (cdr pair)
      '(cons))))

(defun make-leaf-cst
  (unique-id trm boolp)
  (if boolp
    (list* unique-id trm '(t))
    (list* unique-id trm '(nil))))

(defun evg-fn-symb (x) (cond ((consp x) 'cons) (t nil)))

(defun bdd-constructor-trm-p
  (trm bdd-constructors)
  (and (consp trm)
    (if (fquotep trm)
      (member-eq (evg-fn-symb (cadr trm)) bdd-constructors)
      (member-eq (car trm) bdd-constructors))))

(defun evg-type
  (x)
  (cond ((consp x) 'consp)
    ((symbolp x) 'symbol)
    ((integerp x) 'integer)
    ((rationalp x) 'rational)
    ((complex-rationalp x) 'complex-rational)
    ((stringp x) 'string)
    ((characterp x) 'character)
    (t (er hard 'fn-symb "Unexpected object, ~x0." x))))

(defun make-if-cst
  (unique-id tst tbr fbr bdd-constructors)
  (let* ((boolp (and (cst-boolp tbr) (cst-boolp fbr))) (new-cst (list* unique-id tst boolp tbr fbr)))
    (cond ((or (and (leafp tbr)
           (bdd-constructor-trm-p (trm tbr) bdd-constructors))
         (and (leafp fbr)
           (bdd-constructor-trm-p (trm fbr) bdd-constructors))) (mv (msg "Attempted to create IF node during BDD processing with ~@0, ~
                which would produce a non-BDD term (as defined in :DOC ~
                bdd-algorithm).  See :DOC show-bdd."
            (let ((true-fn (trm tbr)) (false-fn (trm fbr)))
              (cond ((and (leafp tbr)
                   (bdd-constructor-trm-p (trm tbr) bdd-constructors)) (cond ((and (leafp fbr)
                       (bdd-constructor-trm-p (trm fbr) bdd-constructors)) (msg "true branch with ~#0~[function symbol ~x1~/explicit ~
                         value of type ~x2~] and false branch with ~
                         ~#3~[function symbol ~x4~/explicit value  of type ~
                         ~x5~]"
                        (if (eq (car true-fn) 'quote)
                          1
                          0)
                        (car true-fn)
                        (and (eq (car true-fn) 'quote) (evg-type (cadr true-fn)))
                        (if (eq (car false-fn) 'quote)
                          1
                          0)
                        (car false-fn)
                        (and (eq (car false-fn) 'quote) (evg-type (cadr false-fn)))))
                    (t (msg "true branch with ~#0~[function symbol ~x1~/explicit ~
                           value of type ~x2~]"
                        (if (eq (car true-fn) 'quote)
                          1
                          0)
                        (car true-fn)
                        (and (eq (car true-fn) 'quote) (evg-type (cadr true-fn)))))))
                (t (msg "false branch with ~#0~[function symbol ~x1~/explicit ~
                           value of type ~x2~]"
                    (if (eq (car false-fn) 'quote)
                      1
                      0)
                    (car false-fn)
                    (and (eq (car false-fn) 'quote) (evg-type (cadr false-fn))))))))
          new-cst))
      (t (mv nil new-cst)))))

(defun cst-nonnilp
  (cst)
  (and (leafp cst)
    (if (quotep (trm cst))
      (not (cst-nilp cst))
      (ffn-symb-p (trm cst) 'cons))))

(defun bool-mask1
  (formals vars rune)
  (cond ((endp formals) rune)
    ((member-eq (car formals) vars) (cons t (bool-mask1 (cdr formals) vars rune)))
    (t (cons nil (bool-mask1 (cdr formals) vars rune)))))

(defun boolean-term-var
  (x)
  (and (not (variablep x))
    (not (fquotep x))
    (cond ((and (eq (ffn-symb x) 'booleanp) (variablep (fargn x 1))) (fargn x 1))
      ((eq (ffn-symb x) 'if) (let ((test (fargn x 1)) (tbr (fargn x 2)) (fbr (fargn x 3)))
          (and (ffn-symb-p test 'equal)
            (let ((v (fargn test 1)))
              (and (variablep v)
                (let ((b (fargn test 2)))
                  (and (or (equal b *t*) (equal b *nil*))
                    (let ((c (if (equal b *t*)
                           *nil*
                           *t*)))
                      (if (and (equal test tbr) (equal fbr (fcons-term* 'equal v c)))
                        v
                        nil)))))))))
      (t nil))))

(defun boolean-hyps-vars
  (hyps)
  (if (endp hyps)
    nil
    (let ((rst (boolean-hyps-vars (cdr hyps))))
      (if (eq rst t)
        t
        (let ((v (boolean-term-var (car hyps))))
          (if v
            (cons v rst)
            t))))))

(defun first-boolean-type-prescription
  (type-prescription-list ens formals)
  (cond ((endp type-prescription-list) (mv nil nil))
    ((and (enabled-numep (access type-prescription
           (car type-prescription-list)
           :nume)
         ens)
       (ts-subsetp (access type-prescription
           (car type-prescription-list)
           :basic-ts)
         *ts-boolean*)) (let* ((tp (car type-prescription-list)) (hyps (access type-prescription tp :hyps))
          (vars (access type-prescription tp :vars)))
        (if hyps
          (let ((more-vars (boolean-hyps-vars hyps)))
            (if (or (eq more-vars t) (not (subsetp-eq more-vars formals)))
              (first-boolean-type-prescription (cdr type-prescription-list)
                ens
                formals)
              (mv (access type-prescription tp :rune)
                (union-eq vars more-vars))))
          (mv (access type-prescription tp :rune) vars))))
    (t (first-boolean-type-prescription (cdr type-prescription-list)
        ens
        formals))))

(defun recognizer-rune
  (recognizer-alist wrld ens)
  (cond ((endp recognizer-alist) nil)
    ((enabled-runep (access recognizer-tuple (car recognizer-alist) :rune)
       ens
       wrld) (access recognizer-tuple (car recognizer-alist) :rune))
    (t (recognizer-rune (cdr recognizer-alist) wrld ens))))

(defun bool-mask
  (fn wrld ens)
  (cond ((or (eq fn 'equal) (eq fn '<)) (list* nil nil *fake-rune-for-type-set*))
    ((eq fn 'not) (list* nil *fake-rune-for-type-set*))
    (t (let ((rune (recognizer-rune (getpropc fn 'recognizer-alist nil wrld)
             wrld
             ens)) (formals (formals fn wrld)))
        (if rune
          (bool-mask1 formals nil rune)
          (mv-let (rune vars)
            (first-boolean-type-prescription (getpropc fn 'type-prescriptions nil wrld)
              ens
              formals)
            (and rune (bool-mask1 formals vars rune))))))))

(defun commutative-p1
  (fn lemmas ens)
  (cond ((endp lemmas) nil)
    (t (if (and (member-eq (access rewrite-rule (car lemmas) :subclass)
            '(backchain abbreviation))
          (equal (access rewrite-rule (car lemmas) :equiv) 'equal)
          (enabled-numep (access rewrite-rule (car lemmas) :nume) ens)
          (null (access rewrite-rule (car lemmas) :hyps))
          (let ((lhs (access rewrite-rule (car lemmas) :lhs)) (rhs (access rewrite-rule (car lemmas) :rhs)))
            (and (or (eq (ffn-symb lhs) fn)
                (er hard
                  'commutative-p1
                  "We had thought we had a rewrite rule with :lhs ~
                               being a call of ~x0, but the :lhs is ~x1."
                  fn
                  lhs))
              (ffn-symb-p rhs fn)
              (variablep (fargn lhs 1))
              (variablep (fargn lhs 2))
              (not (eq (fargn lhs 1) (fargn lhs 2)))
              (equal (fargn lhs 1) (fargn rhs 2))
              (equal (fargn lhs 2) (fargn rhs 1)))))
        (access rewrite-rule (car lemmas) :rune)
        (commutative-p1 fn (cdr lemmas) ens)))))

(defun find-equivalence-rune
  (fn rules)
  (cond ((endp rules) nil)
    ((eq (access congruence-rule (car rules) :equiv) fn) (let ((rune (access congruence-rule (car rules) :rune)))
        (if (eq (car rune) :equivalence)
          rune
          (find-equivalence-rune fn (cdr rules)))))
    (t (find-equivalence-rune fn (cdr rules)))))

(defun equivalence-rune1
  (fn congruences)
  (cond ((endp congruences) (er hard
        'equivalence-rune
        "Failed to find an equivalence rune for function symbol ~x0."
        fn))
    (t (let ((x (car congruences)))
        (case-match x
          (('equal rules1 rules2) (let ((rune (find-equivalence-rune fn rules1)))
              (if (and rune (equal rune (find-equivalence-rune fn rules2)))
                rune
                (equivalence-rune1 fn (cdr congruences)))))
          (& (equivalence-rune1 fn (cdr congruences))))))))

(defun equivalence-rune
  (fn wrld)
  (declare (xargs :guard (equivalence-relationp fn wrld)))
  (cond ((eq fn 'equal) (fn-rune-nume 'equal nil nil wrld))
    (t (equivalence-rune1 fn
        (getpropc fn
          'congruences
          '(:error "See equivalence-rune.")
          wrld)))))

(defun commutative-p
  (fn ens wrld)
  (and (= (arity fn wrld) 2)
    (if (equivalence-relationp fn wrld)
      (equivalence-rune fn wrld)
      (commutative-p1 fn (getpropc fn 'lemmas nil wrld) ens))))

(defun op-alist
  (fns acc i ens wrld)
  (cond ((endp fns) acc)
    ((> i (mx-id-bound)) (er hard
        'bdd
        "We are very surprised to see that, apparently, your problem for bdd ~
         processing involves ~x0 function symbols!  We cannot handle this many ~
         function symbols."
        (/ i 3)))
    (t (op-alist (cdr fns)
        (cons (list* (car fns)
            i
            (commutative-p (car fns) ens wrld)
            (and (not (getpropc (car fns) 'constrainedp nil wrld))
              (enabled-xfnp (car fns) ens wrld)
              (fn-rune-nume (car fns) nil t wrld))
            (bool-mask (car fns) wrld ens))
          acc)
        (+ 3 i)
        ens
        wrld))))

(defun op-alist-info
  (fn op-alist)
  (cond ((endp op-alist) (mv (er hard 'op-alist-info "Function not found:  ~x0" fn)
        nil
        nil
        nil))
    ((eq fn (caar op-alist)) (let ((info (cdar op-alist)))
        (mv (car info) (cadr info) (caddr info) (cdddr info))))
    (t (op-alist-info fn (cdr op-alist)))))

(defun op-hash-index1
  (args i acc)
  (declare (type (signed-byte 61) i acc)
    (xargs :measure (acl2-count args)))
  (the-fixnum (cond ((endp args) (if (< acc 0)
          (- acc)
          acc))
      ((or (= (the-fixnum i) 18) (= (the-fixnum i) -1)) (if (> acc 0)
          (op-hash-index1 args -17 acc)
          (op-hash-index1 args 2 acc)))
      (t (op-hash-index1 (cdr args)
          (1+f i)
          (+f acc (*f i (unique-id (car args)))))))))

(defun if-search-bucket
  (x y z lst)
  (cond ((null lst) nil)
    ((and (cst= x (tst (car lst)))
       (cst= y (tbr (car lst)))
       (cst= z (fbr (car lst)))) (car lst))
    (t (if-search-bucket x y z (cdr lst)))))

(defun cst=-lst
  (x y)
  (cond ((endp x) t)
    (t (and (cst= (car x) (car y)) (cst=-lst (cdr x) (cdr y))))))

(defun op-search-bucket
  (op args lst)
  (cond ((null lst) nil)
    ((and (eq-op op (cadr (car lst)))
       (cst=-lst args (cddr (car lst)))) (car (car lst)))
    (t (op-search-bucket op args (cdr lst)))))

(defun op-search-bucket-2
  (op arg1 arg2 lst)
  (cond ((null lst) nil)
    ((and (eq-op op (cadr (car lst)))
       (let ((args (cddr (car lst))))
         (and (cst= arg1 (car args)) (cst= arg2 (cadr args))))) (car (car lst)))
    (t (op-search-bucket-2 op arg1 arg2 (cdr lst)))))

(defun op-search-bucket-if
  (arg1 arg2 arg3 lst)
  (cond ((null lst) nil)
    ((and (eq-op 'if (cadr (car lst)))
       (let ((args (cddr (car lst))))
         (and (cst= arg1 (car args))
           (cst= arg2 (cadr args))
           (cst= arg3 (caddr args))))) (car (car lst)))
    (t (op-search-bucket-if arg1 arg2 arg3 (cdr lst)))))

(defun chk-memo
  (op-code op args op-ht)
  (declare (type (signed-byte 61) op-code))
  (the-mv 2
    (signed-byte 61)
    (let ((n (op-hash-index op-code args)))
      (declare (type (signed-byte 61) n))
      (let ((ans (op-search-bucket op args (aref1 'op-ht op-ht n))))
        (cond (ans (mvf 0 ans)) (t (mvf n nil)))))))

(defun chk-memo-2
  (op-code op arg1 arg2 op-ht)
  (declare (type (signed-byte 61) op-code))
  (the-mv 2
    (signed-byte 61)
    (let ((n (op-hash-index-2 op-code arg1 arg2)))
      (declare (type (signed-byte 61) n))
      (let ((ans (op-search-bucket-2 op arg1 arg2 (aref1 'op-ht op-ht n))))
        (cond (ans (mvf 0 ans)) (t (mvf n nil)))))))

(defun chk-memo-if
  (arg1 arg2 arg3 op-ht)
  (the-mv 2
    (signed-byte 61)
    (let ((n (op-hash-index-if arg1 arg2 arg3)))
      (declare (type (signed-byte 61) n))
      (let ((ans (op-search-bucket-if arg1 arg2 arg3 (aref1 'op-ht op-ht n))))
        (cond (ans (mvf 0 ans)) (t (mvf n nil)))))))

(defun op-hash-index-string
  (index acc string)
  (declare (type (signed-byte 61) index acc))
  (the-fixnum (cond ((= index 0) acc)
      (t (let ((index (1- (the-fixnum index))))
          (declare (type (signed-byte 61) index))
          (op-hash-index-string index
            (logandf (hash-size)
              (+f acc (char-code (char string index))))
            string))))))

(defun op-hash-index-evg
  (evg)
  (the-fixnum (cond ((integerp evg) (logandf (hash-size) evg))
      ((rationalp evg) (logandf (hash-size)
          (+ (numerator evg) (* 17 (denominator evg)))))
      ((acl2-numberp evg) (logandf (hash-size)
          (+f (op-hash-index-evg (realpart evg))
            (op-hash-index-evg (imagpart evg)))))
      ((characterp evg) (+f (fourth-hash-size) (char-code evg)))
      ((symbolp evg) (logandf (hash-size)
          (*f 19 (op-hash-index-evg (symbol-name evg)))))
      ((stringp evg) (the-fixnum (op-hash-index-string (the-fixnum! (length evg) 'bdd)
            (half-hash-size)
            evg)))
      (t (logandf (hash-size)
          (+f (op-hash-index-evg (car evg))
            (*f 2 (op-hash-index-evg (cdr evg)))))))))

(defun op-search-bucket-quote
  (evg bucket)
  (cond ((null bucket) nil)
    ((and (eq-op 'quote (cadr (car bucket)))
       (equal evg (caddr (car bucket)))) (car (car bucket)))
    (t (op-search-bucket-quote evg (cdr bucket)))))

(defun chk-memo-quotep
  (term op-ht)
  (the-mv 2
    (signed-byte 61)
    (let ((n (op-hash-index-evg (cadr term))))
      (declare (type (signed-byte 61) n))
      (let ((ans (op-search-bucket-quote (cadr term) (aref1 'op-ht op-ht n))))
        (cond (ans (mvf 0 ans)) (t (mvf n nil)))))))

(defun bdd-quotep
  (term op-ht mx-id)
  (declare (type (signed-byte 61) mx-id))
  (the-mv 3
    (signed-byte 61)
    (cond ((equal term *t*) (mvf mx-id *cst-t* op-ht))
      ((equal term *nil*) (mvf mx-id *cst-nil* op-ht))
      (t (mv-let (hash-index ans)
          (chk-memo-quotep term op-ht)
          (declare (type (signed-byte 61) hash-index))
          (cond (ans (mvf mx-id ans op-ht))
            (t (let ((new-mx-id (1+mx-id mx-id)))
                (declare (type (signed-byte 61) new-mx-id))
                (let ((new-cst (make-leaf-cst new-mx-id term nil)))
                  (mvf new-mx-id
                    new-cst
                    (aset1-trusted 'op-ht
                      op-ht
                      hash-index
                      (cons (cons new-cst term) (aref1 'op-ht op-ht hash-index)))))))))))))

(defun rewrite-rule-to-bdd-rule
  (lemma)
  (make bdd-rule
    :lhs (access rewrite-rule lemma :lhs)
    :rhs (access rewrite-rule lemma :rhs)
    :rune (access rewrite-rule lemma :rune)))

(defun bdd-rules-alist1
  (recp lemmas ens all-fns nondef-rules def-rules new-fns)
  (cond ((endp lemmas) (mv new-fns nondef-rules def-rules))
    (t (let ((subclass (access rewrite-rule (car lemmas) :subclass)))
        (cond ((and (eq (access rewrite-rule (car lemmas) :equiv) 'equal)
             (enabled-numep (access rewrite-rule (car lemmas) :nume) ens)
             (case subclass
               (definition (and (null recp)
                   (null (access rewrite-rule (car lemmas) :hyps))
                   (subsetp-eq (all-vars (access rewrite-rule (car lemmas) :rhs))
                     (all-vars (access rewrite-rule (car lemmas) :lhs)))))
               (abbreviation (subsetp-eq (all-vars (access rewrite-rule (car lemmas) :rhs))
                   (all-vars (access rewrite-rule (car lemmas) :lhs))))
               (backchain (and (null (access rewrite-rule (car lemmas) :hyps))
                   (null (access rewrite-rule (car lemmas) :heuristic-info))
                   (subsetp-eq (all-vars (access rewrite-rule (car lemmas) :rhs))
                     (all-vars (access rewrite-rule (car lemmas) :lhs)))))
               (otherwise nil))) (bdd-rules-alist1 recp
              (cdr lemmas)
              ens
              all-fns
              (if (eq subclass 'definition)
                nondef-rules
                (cons (rewrite-rule-to-bdd-rule (car lemmas)) nondef-rules))
              (if (eq subclass 'definition)
                (cons (rewrite-rule-to-bdd-rule (car lemmas)) def-rules)
                def-rules)
              (union-eq (set-difference-eq (all-fnnames (access rewrite-rule (car lemmas) :rhs))
                  all-fns)
                new-fns)))
          (t (bdd-rules-alist1 recp
              (cdr lemmas)
              ens
              all-fns
              nondef-rules
              def-rules
              new-fns)))))))

(defun extra-rules-for-bdds
  (fn wrld)
  (cond ((eq fn 'equal) (list (make rewrite-rule
          :nume nil
          :hyps nil
          :equiv 'equal
          :subclass 'backchain
          :heuristic-info nil
          :backchain-limit-lst *initial-default-backchain-limit*
          :rune *fake-rune-for-anonymous-enabled-rule*
          :lhs (fcons-term* 'equal *nil* 'x)
          :var-info t
          :rhs (fcons-term* 'if 'x *nil* *t*))
        (make rewrite-rule
          :nume nil
          :hyps nil
          :equiv 'equal
          :subclass 'backchain
          :heuristic-info nil
          :backchain-limit-lst *initial-default-backchain-limit*
          :rune *fake-rune-for-anonymous-enabled-rule*
          :lhs (fcons-term* 'equal 'x *nil*)
          :var-info t
          :rhs (fcons-term* 'if 'x *nil* *t*))))
    ((eq fn 'consp) (list (make rewrite-rule
          :nume nil
          :hyps nil
          :equiv 'equal
          :subclass 'backchain
          :heuristic-info nil
          :backchain-limit-lst *initial-default-backchain-limit*
          :rune *fake-rune-for-anonymous-enabled-rule*
          :lhs (fcons-term* 'consp (fcons-term* 'cons 'x 'y))
          :var-info t
          :rhs *t*)))
    ((equivalence-relationp fn wrld) (list (make rewrite-rule
          :nume nil
          :hyps nil
          :equiv 'equal
          :subclass 'abbreviation
          :heuristic-info nil
          :backchain-limit-lst *initial-default-backchain-limit*
          :rune (equivalence-rune fn wrld)
          :lhs (fcons-term* fn 'x 'x)
          :var-info t
          :rhs *t*)))
    ((eq fn 'mv-nth) (list (make rewrite-rule
          :nume nil
          :hyps nil
          :equiv 'equal
          :subclass 'backchain
          :heuristic-info nil
          :backchain-limit-lst *initial-default-backchain-limit*
          :rune (fn-rune-nume 'mv-nth nil nil wrld)
          :lhs (fcons-term* 'mv-nth 'n (fcons-term* 'cons 'x 'y))
          :var-info t
          :rhs (fcons-term* 'if
            (fcons-term* 'zp 'n)
            'x
            (fcons-term* 'mv-nth
              (fcons-term* 'binary-+ 'n (kwote -1))
              'y)))))
    (t nil)))

(defun bdd-rules-alist
  (fns all-fns bdd-rules-alist ens wrld)
  (cond ((endp fns) (mv all-fns bdd-rules-alist))
    (t (mv-let (new-fns nondef-rules def-rules)
        (bdd-rules-alist1 (recursivep (car fns) t wrld)
          (append (getpropc (car fns) 'lemmas nil wrld)
            (extra-rules-for-bdds (car fns) wrld))
          ens
          (cons (car fns) all-fns)
          nil
          nil
          nil)
        (cond ((or def-rules nondef-rules) (bdd-rules-alist (append new-fns (cdr fns))
              (append new-fns all-fns)
              (cons (cons (car fns)
                  (cons (reverse nondef-rules) (reverse def-rules)))
                bdd-rules-alist)
              ens
              wrld))
          (t (bdd-rules-alist (cdr fns) all-fns bdd-rules-alist ens wrld)))))))

(defun some-one-way-unify-cst-lst
  (cst-lst rules op-ht mx-id ttree)
  (declare (type (signed-byte 61) mx-id))
  (the-mv 6
    (signed-byte 61)
    (cond ((endp rules) (mvf mx-id nil nil nil op-ht ttree))
      (t (mv-let (mx-id ans alist op-ht)
          (one-way-unify1-cst-lst mx-id
            (fargs (access bdd-rule (car rules) :lhs))
            cst-lst
            nil
            op-ht)
          (declare (type (signed-byte 61) mx-id))
          (cond (ans (mvf mx-id
                t
                (access bdd-rule (car rules) :rhs)
                alist
                op-ht
                (push-lemma (access bdd-rule (car rules) :rune) ttree)))
            (t (some-one-way-unify-cst-lst cst-lst
                (cdr rules)
                op-ht
                mx-id
                ttree))))))))

(defun leaf-cst-list
  (lst bool-vars acc mx-id)
  (cond ((endp lst) (mv mx-id acc))
    (t (mv-let (mx-id acc)
        (cond ((assoc-eq (car lst) acc) (mv mx-id acc))
          (t (let ((new-mx-id (1+mx-id mx-id)))
              (mv new-mx-id
                (cons (make-leaf-cst new-mx-id
                    (car lst)
                    (member-eq (car lst) bool-vars))
                  acc)))))
        (leaf-cst-list (cdr lst) bool-vars acc mx-id)))))

(defun decode-cst-alist1
  (alist cst-array)
  (cond ((endp alist) (mv nil cst-array))
    (t (mv-let (term cst-array)
        (decode-cst (cdar alist) cst-array)
        (mv-let (rest cst-array)
          (decode-cst-alist1 (cdr alist) cst-array)
          (mv (cons (list (caar alist) term) rest) cst-array))))))

(defun decode-cst-alist
  (cst-alist cst-array)
  (mv-let (alist cst-array)
    (decode-cst-alist1 cst-alist cst-array)
    (declare (ignore cst-array))
    alist))

(defun leaf-cst-list-array
  (mx-id)
  (let ((dim (1+ mx-id)))
    (compress1 'cst-array
      `((:header :dimensions (,DIM)
         :maximum-length ,(+ 10 DIM)
         :default nil)))))

(defun falsifying-assignment1
  (cst acc cst-array)
  (cond ((cst-nilp cst) (mv acc cst-array))
    ((quotep (trm cst)) (mv (er hard
          'falsifying-assignment1
          "Tried to falsify ~x0!"
          (trm cst))
        cst-array))
    ((leafp cst) (mv-let (term cst-array)
        (decode-cst cst cst-array)
        (mv (cons (list term nil) acc) cst-array)))
    ((cst-nonnilp (tbr cst)) (mv-let (term cst-array)
        (decode-cst (tst cst) cst-array)
        (falsifying-assignment1 (fbr cst)
          (cons (list term nil) acc)
          cst-array)))
    (t (mv-let (term cst-array)
        (decode-cst (tst cst) cst-array)
        (falsifying-assignment1 (tbr cst)
          (cons (list term
              (if (cst-boolp (tst cst))
                t
                *some-non-nil-value*))
            acc)
          cst-array)))))

(defun falsifying-assignment
  (cst mx-id)
  (mv-let (asst cst-array)
    (falsifying-assignment1 cst nil (leaf-cst-list-array mx-id))
    (declare (ignore cst-array))
    (reverse asst)))

(defun make-if
  (mx-id n op args x y z op-ht if-ht bdd-constructors)
  (declare (type (signed-byte 61) n mx-id))
  (the-mv 4
    (signed-byte 61)
    (cond ((cst= y z) (mvf mx-id
          y
          (aset1-trusted 'op-ht
            op-ht
            n
            (cons (list* y op args) (aref1 'op-ht op-ht n)))
          if-ht))
      (t (let ((m (if-hash-index x y z)))
          (declare (type (signed-byte 61) m))
          (let* ((bucket (aref1 'if-ht if-ht m)) (old-if (if-search-bucket x y z bucket)))
            (cond (old-if (mvf mx-id
                  old-if
                  (aset1-trusted 'op-ht
                    op-ht
                    n
                    (cons (list* old-if op args) (aref1 'op-ht op-ht n)))
                  if-ht))
              ((and (cst-tp y) (cst-nilp z) (cst-boolp x)) (mvf mx-id
                  x
                  (aset1-trusted 'op-ht
                    op-ht
                    n
                    (cons (list* x op args) (aref1 'op-ht op-ht n)))
                  if-ht))
              (t (let ((mx-id (1+mx-id mx-id)))
                  (declare (type (signed-byte 61) mx-id))
                  (mv-let (erp new-if)
                    (make-if-cst mx-id x y z bdd-constructors)
                    (cond (erp (mvf mx-id (car erp) (cdr erp) new-if))
                      (t (mvf mx-id
                          new-if
                          (aset1-trusted 'op-ht
                            op-ht
                            n
                            (cons (list* new-if op args) (aref1 'op-ht op-ht n)))
                          (aset1-trusted 'if-ht if-ht m (cons new-if bucket)))))))))))))))

(defun make-if-no-memo
  (mx-id x y z op-ht if-ht bdd-constructors)
  (declare (type (signed-byte 61) mx-id))
  (the-mv 4
    (signed-byte 61)
    (let ((m (if-hash-index x y z)))
      (declare (type (signed-byte 61) m))
      (let* ((bucket (aref1 'if-ht if-ht m)) (old-if (if-search-bucket x y z bucket)))
        (cond (old-if (mvf mx-id old-if op-ht if-ht))
          ((and (cst-tp y) (cst-nilp z) (cst-boolp x)) (mvf mx-id x op-ht if-ht))
          (t (let ((mx-id (1+mx-id mx-id)))
              (declare (type (signed-byte 61) mx-id))
              (mv-let (erp new-if)
                (make-if-cst mx-id x y z bdd-constructors)
                (cond (erp (mvf mx-id (car erp) (cdr erp) new-if))
                  (t (mvf mx-id
                      new-if
                      op-ht
                      (aset1-trusted 'if-ht if-ht m (cons new-if bucket)))))))))))))

(defun min-var
  (acc args)
  (declare (xargs :measure (acl2-count args)))
  (if (endp args)
    acc
    (let ((var (split-var (car args))))
      (if (null var)
        (min-var acc (cdr args))
        (min-var (cond ((null acc) var)
            ((< (unique-id var) (unique-id acc)) var)
            (t acc))
          (cdr args))))))

(defun combine-op-csts1
  (var-id args)
  (declare (type (signed-byte 61) var-id))
  (if (endp args)
    (mv nil nil)
    (mv-let (x y)
      (combine-op-csts1 var-id (cdr args))
      (cond ((leafp (car args)) (if (and (= (the-fixnum var-id) (unique-id (car args)))
              (cst-boolp (car args)))
            (mv (cons *cst-t* x) (cons *cst-nil* y))
            (mv (cons (car args) x) (cons (car args) y))))
        (t (if (= (the-fixnum var-id) (unique-id (tst (car args))))
            (mv (cons (tbr (car args)) x) (cons (fbr (car args)) y))
            (mv (cons (car args) x) (cons (car args) y))))))))

(defun bool-flg
  (args mask)
  (cond ((endp args) mask)
    ((car mask) (and (cst-boolp (car args))
        (bool-flg (cdr args) (cdr mask))))
    (t (bool-flg (cdr args) (cdr mask)))))

(defun some-bdd-constructorp
  (args bdd-constructors)
  (cond ((endp args) nil)
    (t (or (and (leafp (car args))
          (bdd-constructor-trm-p (trm (car args)) bdd-constructors))
        (some-bdd-constructorp (cdr args) bdd-constructors)))))

(defun combine-op-csts-simple
  (hash-index op
    mask
    args
    op-ht
    if-ht
    mx-id
    bdd-constructors
    ttree)
  (declare (type (signed-byte 61) hash-index mx-id))
  (the-mv 5
    (signed-byte 61)
    (let ((new-mx-id (1+mx-id mx-id)) (rune (and mask (bool-flg args mask))))
      (declare (type (signed-byte 61) new-mx-id))
      (let ((new-cst (make-leaf-cst new-mx-id (cons op args) rune)))
        (cond ((and bdd-constructors
             (some-bdd-constructorp args bdd-constructors)) (bdd-error new-mx-id
              "Attempted to create ~x0 node during BDD processing with an argument ~
           that is a call of ~#1~[a bdd-constructor~/CONS~], which would ~
           produce a non-BDD term (as defined in :DOC bdd-algorithm).  See ~
           :DOC show-bdd."
              (list (cons #\0 op)
                (cons #\1
                  (if (equal bdd-constructors '(cons))
                    1
                    0)))
              new-cst
              ttree))
          (t (mvf new-mx-id
              new-cst
              (aset1-trusted 'op-ht
                op-ht
                hash-index
                (cons (list* new-cst op args)
                  (aref1 'op-ht op-ht hash-index)))
              if-ht
              (if rune
                (push-lemma rune ttree)
                ttree))))))))

(defun combine-if-csts1
  (var-id args)
  (declare (type (signed-byte 61) var-id))
  (mv-let (x y)
    (combine-op-csts1 var-id (cdr args))
    (cond ((leafp (car args)) (if (= (the-fixnum var-id) (unique-id (car args)))
          (mv (cons *cst-t* x) (cons *cst-nil* y))
          (mv (cons (car args) x) (cons (car args) y))))
      (t (if (= (the-fixnum var-id) (unique-id (tst (car args))))
          (mv (cons (tbr (car args)) x) (cons (fbr (car args)) y))
          (mv (cons (car args) x) (cons (car args) y)))))))

(defun combine-if-csts
  (test-cst true-cst
    false-cst
    op-ht
    if-ht
    mx-id
    bdd-constructors)
  (declare (type (signed-byte 61) mx-id))
  (the-mv 4
    (signed-byte 61)
    (cond ((cst= true-cst false-cst) (mvf mx-id true-cst op-ht if-ht))
      ((cst= test-cst false-cst) (combine-if-csts test-cst
          true-cst
          *cst-nil*
          op-ht
          if-ht
          mx-id
          bdd-constructors))
      ((and (cst= test-cst true-cst) (cst-boolp true-cst)) (combine-if-csts test-cst
          *cst-t*
          false-cst
          op-ht
          if-ht
          mx-id
          bdd-constructors))
      ((and (cst-nilp false-cst)
         (if (cst-tp true-cst)
           (cst-boolp test-cst)
           (cst= test-cst true-cst))) (mvf mx-id test-cst op-ht if-ht))
      (t (let ((true-var (split-var true-cst)) (false-var (split-var false-cst)))
          (cond ((and (leafp test-cst)
               (or (null true-var)
                 (< (unique-id test-cst) (unique-id true-var)))
               (or (null false-var)
                 (< (unique-id test-cst) (unique-id false-var)))) (make-if-no-memo mx-id
                test-cst
                true-cst
                false-cst
                op-ht
                if-ht
                bdd-constructors))
            (t (mv-let (hash-index ans)
                (chk-memo-if test-cst true-cst false-cst op-ht)
                (declare (type (signed-byte 61) hash-index))
                (cond (ans (mvf mx-id ans op-ht if-ht))
                  (t (let* ((args (list test-cst true-cst false-cst)) (min-var (min-var nil args)))
                      (mv-let (args1 args2)
                        (combine-if-csts1 (unique-id min-var) args)
                        (bdd-mv-let (mx-id cst1 op-ht if-ht)
                          (combine-if-csts+ (car args1)
                            (cadr args1)
                            (caddr args1)
                            op-ht
                            if-ht
                            mx-id
                            bdd-constructors)
                          (bdd-mv-let (mx-id cst2 op-ht if-ht)
                            (combine-if-csts+ (car args2)
                              (cadr args2)
                              (caddr args2)
                              op-ht
                              if-ht
                              mx-id
                              bdd-constructors)
                            (make-if mx-id
                              hash-index
                              'if
                              args
                              min-var
                              cst1
                              cst2
                              op-ht
                              if-ht
                              bdd-constructors)))))))))))))))

(defun cst-list-to-evg-list
  (cst-lst)
  (cond ((endp cst-lst) nil)
    (t (cons (cadr (trm (car cst-lst)))
        (cst-list-to-evg-list (cdr cst-lst))))))

(defun cst-quote-listp
  (cst-lst)
  (cond ((endp cst-lst) t)
    ((and (leafp (car cst-lst)) (quotep (trm (car cst-lst)))) (cst-quote-listp (cdr cst-lst)))
    (t nil)))

(defun bdd-ev-fncall
  (mx-id hash-index
    op
    mask
    args
    op-ht
    if-ht
    bdd-constructors
    rune
    ttree
    state)
  (declare (type (signed-byte 61) hash-index mx-id))
  (the-mv 5
    (signed-byte 61)
    (mv-let (erp val latches)
      (ev-fncall op
        (cst-list-to-evg-list args)
        nil
        state
        nil
        nil
        nil)
      (declare (ignore latches))
      (cond (erp (combine-op-csts-simple hash-index
            op
            mask
            args
            op-ht
            if-ht
            mx-id
            (and (not (member-eq op bdd-constructors)) bdd-constructors)
            ttree))
        (t (bdd-quotep+ (list 'quote val)
            op-ht
            if-ht
            mx-id
            (push-lemma rune ttree)))))))

(defun make-if-for-op
  (mx-id hash-index
    op
    args
    test-cst
    true-cst
    false-cst
    op-ht
    if-ht
    bdd-constructors)
  (declare (type (signed-byte 61) hash-index mx-id))
  (the-mv 4
    (signed-byte 61)
    (cond ((cst= true-cst false-cst) (mvf mx-id
          true-cst
          (aset1-trusted 'op-ht
            op-ht
            hash-index
            (cons (list* true-cst op args)
              (aref1 'op-ht op-ht hash-index)))
          if-ht))
      ((let ((true-split-var (split-var true-cst)) (false-split-var (split-var false-cst))
           (test-id (unique-id test-cst)))
         (declare (type (signed-byte 61) test-id))
         (and (or (null true-split-var)
             (< test-id (unique-id true-split-var)))
           (or (null false-split-var)
             (< test-id (unique-id false-split-var))))) (make-if mx-id
          hash-index
          op
          args
          test-cst
          true-cst
          false-cst
          op-ht
          if-ht
          bdd-constructors))
      (t (bdd-mv-let (mx-id cst op-ht if-ht)
          (combine-if-csts+ test-cst
            true-cst
            false-cst
            op-ht
            if-ht
            mx-id
            bdd-constructors)
          (mvf mx-id
            cst
            (aset1-trusted 'op-ht
              op-ht
              hash-index
              (cons (list* cst op args) (aref1 'op-ht op-ht hash-index)))
            if-ht))))))

(defun if-ht-max-length
  (state)
  (if (f-boundp-global 'if-ht-max-length state)
    (f-get-global 'if-ht-max-length state)
    (+ 100000 (hash-size))))

(defun op-ht-max-length
  (state)
  (if (f-boundp-global 'op-ht-max-length state)
    (f-get-global 'op-ht-max-length state)
    (+ 100000 (hash-size))))

(defun leaf-cst-list-to-alist
  (leaf-cst-list)
  (cond ((endp leaf-cst-list) nil)
    (t (cons (cons (trm (car leaf-cst-list)) (car leaf-cst-list))
        (leaf-cst-list-to-alist (cdr leaf-cst-list))))))

(defun bdd-top
  (term input-vars bool-vars bdd-constructors cl-id ens state)
  (let* ((fns (all-fnnames term)) (wrld (w state)))
    (mv-let (fns bdd-rules-alist)
      (bdd-rules-alist (remove1-eq 'if fns)
        (add-to-set-eq 'if fns)
        nil
        ens
        wrld)
      (let ((op-alist (op-alist fns nil 6 ens wrld)) (if-ht (compress1 'if-ht
              `((:header :dimensions (,(1+ (HASH-SIZE)))
                 :maximum-length ,(IF-HT-MAX-LENGTH STATE)
                 :default nil))))
          (op-ht (compress1 'op-ht
              `((:header :dimensions (,(1+ (HASH-SIZE)))
                 :maximum-length ,(OP-HT-MAX-LENGTH STATE)
                 :default nil))))
          (all-vars (let ((term-vars (reverse (all-vars term))))
              (cond ((not (symbol-listp input-vars)) (er hard
                    'bdd-top
                    "The second argument of BDD-TOP must ~
                                          be a list of variables, but ~x0 is ~
                                          not."
                    input-vars))
                ((subsetp-eq term-vars input-vars) input-vars)
                (t (er hard
                    'bdd-top
                    "The following variables are free ~
                                            in the input term, ~x0, but not do ~
                                            not occur in the specified input ~
                                            variables, ~x1:  ~x2."
                    term
                    input-vars
                    (set-difference-eq term-vars input-vars)))))))
        (mv-let (mx-id leaf-cst-list)
          (leaf-cst-list all-vars
            bool-vars
            nil
            (max (unique-id *cst-nil*) (unique-id *cst-t*)))
          (mv-let (mx-id cst op-ht if-ht ttree)
            (bdd term
              (leaf-cst-list-to-alist leaf-cst-list)
              op-ht
              if-ht
              mx-id
              nil
              (make bddspv
                :op-alist op-alist
                :bdd-rules-alist bdd-rules-alist
                :bdd-constructors bdd-constructors)
              state)
            (cond ((stringp cst) (make bddnote
                  :cl-id cl-id
                  :goal-term term
                  :mx-id mx-id
                  :err-string cst
                  :fmt-alist (car op-ht)
                  :cst (cdr op-ht)
                  :term nil
                  :bdd-call-stack if-ht
                  :ttree ttree))
              (t (make bddnote
                  :cl-id cl-id
                  :goal-term term
                  :mx-id mx-id
                  :err-string nil
                  :fmt-alist nil
                  :cst cst
                  :term nil
                  :bdd-call-stack nil
                  :ttree ttree)))))))))

(defun get-bool-vars
  (vars type-alist ttree acc)
  (cond ((endp vars) (mv acc ttree))
    (t (let ((entry (assoc-eq (car vars) type-alist)))
        (cond ((and entry (ts-subsetp (cadr entry) *ts-boolean*)) (get-bool-vars (cdr vars)
              type-alist
              (cons-tag-trees (cddr entry) ttree)
              (cons (car vars) acc)))
          (t (get-bool-vars (cdr vars) type-alist ttree acc)))))))

(defun bdd-clause1
  (hint-alist type-alist
    cl
    position
    ttree0
    cl-id
    ens
    wrld
    state)
  (let* ((term (case position
         (:conc (mcons-term* 'if (car (last cl)) *t* *nil*))
         (:all (mcons-term* 'if (disjoin cl) *t* *nil*))
         (otherwise (let ((lit (nth position cl)))
             (case-match lit
               (('not x) (mcons-term* 'if x *t* *nil*))
               (& (mcons-term* 'not lit))))))) (all-vars (all-vars term))
      (vars-hint (cdr (assoc-eq :vars hint-alist)))
      (prove-hint (if (assoc-eq :prove hint-alist)
          (cdr (assoc-eq :prove hint-alist))
          t))
      (bdd-constructors-hint (if (assoc-eq :bdd-constructors hint-alist)
          (cdr (assoc-eq :bdd-constructors hint-alist))
          (bdd-constructors wrld))))
    (mv-let (bool-vars ttree1)
      (get-bool-vars all-vars type-alist ttree0 nil)
      (cond ((not (subsetp-eq (if (eq vars-hint t)
               all-vars
               vars-hint)
             bool-vars)) (let ((bad-vars (set-difference-eq (if (eq vars-hint t)
                   all-vars
                   vars-hint)
                 bool-vars)))
            (mv 'error
              (msg "The following variable~#0~[ is~/s are~] not known to be ~
                   Boolean by trivial (type set) reasoning:  ~&0.  Perhaps you ~
                   need to add hypotheses to that effect.  Alternatively, you ~
                   may want to prove :type-prescription rules (see :DOC ~
                   type-prescription) or :forward-chaining (see :DOC ~
                   forward-chaining) rules to help with the situation, or ~
                   perhaps to start with the hint ~x1."
                bad-vars
                (list :cases (if (consp (cdr bad-vars))
                    (list (cons 'and
                        (pairlis$ (make-list (length bad-vars) :initial-element 'booleanp)
                          (pairlis$ bad-vars nil))))
                    `((booleanp ,(CAR BAD-VARS))))))
              nil)))
        (t (let* ((real-vars-hint (if (eq vars-hint t)
                 nil
                 vars-hint)) (bddnote (bdd-top term
                  (append real-vars-hint
                    (set-difference-eq (reverse all-vars) real-vars-hint))
                  bool-vars
                  bdd-constructors-hint
                  cl-id
                  ens
                  state))
              (cst (access bddnote bddnote :cst))
              (err-string (access bddnote bddnote :err-string))
              (ttree (access bddnote bddnote :ttree)))
            (cond (err-string (if prove-hint
                  (mv 'error
                    (cons (access bddnote bddnote :err-string)
                      (access bddnote bddnote :fmt-alist))
                    bddnote)
                  (mv 'miss nil bddnote)))
              ((cst-tp cst) (mv 'hit
                  nil
                  (add-to-tag-tree 'bddnote
                    bddnote
                    (cons-tag-trees ttree ttree1))))
              (prove-hint (mv 'error
                  (list "The :BDD hint for the current goal has ~
                      successfully simplified this goal, but has ~
                      failed to prove it.  Consider using (SHOW-BDD) ~
                      to suggest a counterexample; see :DOC show-bdd.")
                  bddnote))
              (t (mv-let (new-term cst-array)
                  (decode-cst cst
                    (leaf-cst-list-array (access bddnote bddnote :mx-id)))
                  (declare (ignore cst-array))
                  (let* ((bddnote (change bddnote bddnote :term new-term)) (ttree (add-to-tag-tree 'bddnote
                          bddnote
                          (cons-tag-trees ttree ttree1))))
                    (cond ((eq position :conc) (mv 'hit
                          (list (add-literal new-term (butlast cl 1) t))
                          ttree))
                      ((eq position :all) (mv 'hit (list (add-literal new-term nil nil)) ttree))
                      (t (mv 'hit
                          (list (subst-for-nth-arg (dumb-negate-lit new-term) position cl))
                          ttree)))))))))))))

(defun expand-and-or-simple
  (term bool fns-to-be-ignored-by-rewrite wrld ttree)
  (cond ((variablep term) (mv nil nil ttree))
    ((fquotep term) (cond ((equal term *nil*) (if bool
            (mv t nil ttree)
            (mv nil nil ttree)))
        ((equal term *t*) (if bool
            (mv nil nil ttree)
            (mv t nil ttree)))
        (t (if bool
            (mv t (list *t*) ttree)
            (mv t nil ttree)))))
    ((member-equal (ffn-symb term) fns-to-be-ignored-by-rewrite) (mv nil nil ttree))
    ((flambda-applicationp term) (mv-let (hitp lst ttree0)
        (expand-and-or-simple (lambda-body (ffn-symb term))
          bool
          fns-to-be-ignored-by-rewrite
          wrld
          ttree)
        (cond (hitp (mv hitp
              (subcor-var-lst (lambda-formals (ffn-symb term))
                (fargs term)
                lst)
              ttree0))
          (t (mv nil nil ttree)))))
    ((eq (ffn-symb term) 'not) (mv-let (hitp lst ttree0)
        (expand-and-or-simple (fargn term 1)
          (not bool)
          fns-to-be-ignored-by-rewrite
          wrld
          ttree)
        (cond (hitp (mv hitp
              (dumb-negate-lit-lst lst)
              (push-lemma (fn-rune-nume 'not nil nil wrld) ttree0)))
          (t (mv nil nil ttree)))))
    ((and (eq (ffn-symb term) 'implies) bool) (expand-and-or-simple (subcor-var (formals 'implies wrld)
          (fargs term)
          (bbody 'implies))
        bool
        fns-to-be-ignored-by-rewrite
        wrld
        (push-lemma (fn-rune-nume 'implies nil nil wrld) ttree)))
    ((eq (ffn-symb term) 'if) (let ((t1 (fargn term 1)) (t2 (fargn term 2))
          (t3 (fargn term 3)))
        (cond ((or (equal t1 *nil*) (equal t2 t3)) (expand-and-or-simple+ t3
              bool
              fns-to-be-ignored-by-rewrite
              wrld
              ttree))
          ((quotep t1) (expand-and-or-simple+ t2
              bool
              fns-to-be-ignored-by-rewrite
              wrld
              ttree))
          ((and (quotep t2) (quotep t3)) (cond ((equal t2 *nil*) (mv-let (hitp lst ttree)
                  (expand-and-or-simple t1
                    (not bool)
                    fns-to-be-ignored-by-rewrite
                    wrld
                    ttree)
                  (mv t
                    (if hitp
                      (dumb-negate-lit-lst lst)
                      (list (dumb-negate-lit t1)))
                    ttree)))
              ((equal t3 *nil*) (expand-and-or-simple+ t1
                  bool
                  fns-to-be-ignored-by-rewrite
                  wrld
                  ttree))
              (t (expand-and-or-simple *t*
                  bool
                  fns-to-be-ignored-by-rewrite
                  wrld
                  ttree))))
          ((and (quotep t3) (eq (not bool) (equal t3 *nil*))) (mv-let (hitp lst1 ttree)
              (expand-and-or-simple+ t1
                nil
                fns-to-be-ignored-by-rewrite
                wrld
                ttree)
              (declare (ignore hitp))
              (mv-let (hitp lst2 ttree)
                (expand-and-or-simple+ t2
                  bool
                  fns-to-be-ignored-by-rewrite
                  wrld
                  ttree)
                (declare (ignore hitp))
                (if bool
                  (mv t (union-equal (dumb-negate-lit-lst lst1) lst2) ttree)
                  (mv t (union-equal lst1 lst2) ttree)))))
          ((and (quotep t2) (eq (not bool) (equal t2 *nil*))) (mv-let (hitp lst1 ttree)
              (expand-and-or-simple+ t1
                t
                fns-to-be-ignored-by-rewrite
                wrld
                ttree)
              (declare (ignore hitp))
              (mv-let (hitp lst2 ttree)
                (expand-and-or-simple+ t3
                  bool
                  fns-to-be-ignored-by-rewrite
                  wrld
                  ttree)
                (declare (ignore hitp))
                (if bool
                  (mv t (union-equal lst1 lst2) ttree)
                  (mv t (union-equal (dumb-negate-lit-lst lst1) lst2) ttree)))))
          (t (mv nil nil ttree)))))
    (t (mv nil nil ttree))))

(defun expand-clause
  (cl fns-to-be-ignored-by-rewrite wrld ttree acc)
  (cond ((endp cl) (mv acc ttree))
    (t (mv-let (hitp lst ttree)
        (expand-and-or-simple+ (car cl)
          t
          fns-to-be-ignored-by-rewrite
          wrld
          ttree)
        (declare (ignore hitp))
        (expand-clause (cdr cl)
          fns-to-be-ignored-by-rewrite
          wrld
          ttree
          (union-equal lst acc))))))

(defun bdd-clause
  (bdd-hint cl-id top-clause pspv wrld state)
  (let ((rcnst (access prove-spec-var pspv :rewrite-constant)) (literal-hint (or (cdr (assoc-eq :literal bdd-hint)) :all)))
    (cond ((and (integerp literal-hint)
         (not (< literal-hint (1- (length top-clause))))) (mv 'error
          (msg "There ~#0~[are no hypotheses~/is only one hypothesis~/are only ~
                ~n0 hypotheses~] in this goal, but your :BDD hint suggested ~
                that there would be at least ~x1 ~
                ~#1~[~/hypothesis~/hypotheses]."
            (1- (length top-clause))
            (1+ literal-hint))
          nil
          pspv))
      (t (mv-let (hitp current-clause
            current-clause-pts
            remove-trivial-equivalences-ttree)
          (remove-trivial-equivalences top-clause
            (enumerate-elements top-clause 0)
            t
            (access rewrite-constant rcnst :current-enabled-structure)
            wrld
            state
            nil)
          (declare (ignore hitp))
          (let ((position (cond ((integerp literal-hint) (position literal-hint current-clause-pts))
                 (t literal-hint))))
            (cond ((or (null position)
                 (and (eq literal-hint :conc)
                   (not (member (1- (length top-clause)) current-clause-pts)))) (mv 'error
                  (msg "The attempt to use a :BDD hint for the goal named ~
                            "~@0" has failed.  The problem is that the hint ~
                            specified that BDD processing was to be used on ~
                            the ~#1~[~n2 hypothesis~/conclusion~], which has ~
                            somehow disappeared.  One possibility is that this ~
                            literal is an equivalence that has disappeared ~
                            after being used for substitution into the rest of ~
                            the goal.  Another possibility is that this ~
                            literal has merged with another.  We suspect, ~
                            therefore, that you would benefit by reconsidering ~
                            this :BDD hint, possibly attaching it to a ~
                            subsequent goal instead."
                    (tilde-@-clause-id-phrase cl-id)
                    (if (null position)
                      0
                      1)
                    (if (null position)
                      (1+ literal-hint)
                      0))
                  nil
                  pspv))
              (t (let ((ens (access rewrite-constant rcnst :current-enabled-structure)))
                  (mv-let (expanded-clause ttree)
                    (expand-clause current-clause
                      (access rewrite-constant
                        rcnst
                        :fns-to-be-ignored-by-rewrite)
                      wrld
                      remove-trivial-equivalences-ttree
                      nil)
                    (mv-let (contradictionp type-alist fc-pair-lst)
                      (forward-chain-top 'bdd-clause
                        expanded-clause
                        nil
                        nil
                        t
                        wrld
                        ens
                        (match-free-override wrld)
                        state)
                      (cond (contradictionp (mv 'hit nil (cons-tag-trees ttree fc-pair-lst) pspv))
                        (t (mv-let (changedp clauses ttree)
                            (bdd-clause1 bdd-hint
                              type-alist
                              current-clause
                              position
                              ttree
                              cl-id
                              ens
                              wrld
                              state)
                            (mv changedp clauses ttree pspv)))))))))))))))