hyp-fix

(in-package "GL")

(include-book "bfr")

(include-book "bfr-param")

(include-book "bfr-reasoning")

(include-book "std/stobjs/absstobjs" :dir :system)

(include-book "std/stobjs/clone" :dir :system)

(include-book "std/lists/index-of" :dir :system)

(local (include-book "centaur/aig/aig-vars" :dir :system))

(local (in-theory (disable equal-of-booleans-rewrite
      consp-of-car-when-alistp
      double-containment
      aig-eval
      default-car
      default-cdr)))

(define calist-lookup
  (x calist)
  :inline t
  (let* ((res (cdr (hons-get x calist))))
    (and res (bfix res)))
  ///
  (defthm calist-lookup-of-cons
    (equal (calist-lookup k1 (cons pair calist))
      (if (or (atom pair) (not (equal k1 (car pair))))
        (calist-lookup k1 calist)
        (and (cdr pair) (bfix (cdr pair))))))
  (defthm calist-lookup-of-atom
    (implies (not (consp x))
      (equal (calist-lookup k x) nil))
    :rule-classes ((:rewrite :backchain-limit-lst 0))))

(define calist-remassocs
  (x seen)
  (if (atom x)
    nil
    (if (and (consp (car x))
        (not (ec-call (member-equal (caar x) seen))))
      (cons (car x)
        (calist-remassocs (cdr x) seen))
      (calist-remassocs (cdr x) seen)))
  ///
  (defthm lookup-in-calist-remassocs
    (equal (calist-lookup k
        (calist-remassocs x seen))
      (and (not (member k seen))
        (calist-lookup k x))))
  (defthm len-of-calist-remassocs
    (<= (len (calist-remassocs x seen))
      (len x))
    :rule-classes :linear)
  (defthm calist-remassocs-compose
    (equal (calist-remassocs (calist-remassocs x seen1)
        seen2)
      (calist-remassocs x (append seen1 seen2))))
  (defcong set-equiv
    equal
    (calist-remassocs x seen)
    2
    :package :legacy))

(define shrink-constraint-alist-aux
  (x seen)
  (if (atom x)
    (prog2$ (fast-alist-free seen) nil)
    (if (and (consp (car x))
        (not (hons-get (caar x) seen)))
      (if (cdar x)
        (hons-acons (caar x)
          (bfix (cdar x))
          (shrink-constraint-alist-aux (cdr x)
            (hons-acons (caar x) t seen)))
        (shrink-constraint-alist-aux (cdr x)
          (hons-acons (caar x) t seen)))
      (shrink-constraint-alist-aux (cdr x) seen)))
  ///
  (local (defun ind
      (x seen)
      (declare (xargs :measure (len x)))
      (if (atom x)
        seen
        (list (ind (cdr x)
            (hons-acons (caar x) t seen))
          (ind (cdr x) (hons-acons (caar x) t nil))
          (ind (cdr x) seen)))))
  (local (defthm calist-remassocs-compose-strong
      (implies (equal y (calist-remassocs x seen1))
        (equal (calist-remassocs y seen2)
          (calist-remassocs x (append seen1 seen2))))))
  (local (defthm set-equiv-of-cons-redundant
      (implies (member k x)
        (set-equiv (cons k x) x))))
  (defthm shrink-constraint-alist-aux-of-seen
    (implies (syntaxp (not (equal seen ''nil)))
      (equal (shrink-constraint-alist-aux x seen)
        (calist-remassocs (shrink-constraint-alist-aux x nil)
          (alist-keys seen))))
    :hints (("Goal" :in-theory (enable calist-remassocs alist-keys)
       :expand ((shrink-constraint-alist-aux x nil))
       :induct (ind x seen)))))

(define shrink-constraint-alist
  (x)
  :measure (len x)
  :verify-guards nil
  (mbe :logic (if (atom x)
      nil
      (if (consp (car x))
        (let ((rest (calist-remassocs (shrink-constraint-alist (cdr x))
               (list (caar x)))))
          (if (cdar x)
            (hons-acons (caar x) (bfix (cdar x)) rest)
            rest))
        (shrink-constraint-alist (cdr x))))
    :exec (shrink-constraint-alist-aux x nil))
  ///
  (defthm shrink-constraint-alist-aux-redef
    (equal (shrink-constraint-alist-aux x nil)
      (shrink-constraint-alist x))
    :hints (("Goal" :in-theory (enable shrink-constraint-alist-aux
         calist-remassocs))))
  (verify-guards shrink-constraint-alist)
  (defthm lookup-in-shrink-constraint-alist
    (equal (calist-lookup k
        (shrink-constraint-alist x))
      (calist-lookup k x)))
  (local (defthm set-equiv-of-cons-redundant
      (implies (member k seen)
        (set-equiv (cons k seen) seen))))
  (local (defthm set-equiv-of-append-to-cons
      (set-equiv (append seen (list k))
        (cons k seen))))
  (defthm shrink-constraint-alist-of-calist-remassocs
    (equal (shrink-constraint-alist (calist-remassocs x seen))
      (calist-remassocs (shrink-constraint-alist x)
        seen))
    :hints (("goal" :induct (shrink-constraint-alist x)
       :expand ((calist-remassocs x seen) (calist-remassocs nil seen)
         (:free (a b)
           (calist-remassocs (cons a b) seen))))))
  (defthm shrink-constraint-alist-idempotent
    (equal (shrink-constraint-alist (shrink-constraint-alist x))
      (shrink-constraint-alist x))
    :hints (("goal" :induct (shrink-constraint-alist x)
       :expand ((:free (a b)
          (shrink-constraint-alist (cons a b))))))))

(define eval-constraint-alist-aux
  (x seen env)
  (if (atom x)
    (prog2$ (fast-alist-free seen) t)
    (if (or (atom (car x)) (hons-get (caar x) seen))
      (eval-constraint-alist-aux (cdr x) seen env)
      (if (cdar x)
        (and (iff (aig-eval (caar x) env)
            (eql (cdar x) 1))
          (eval-constraint-alist-aux (cdr x)
            (hons-acons (caar x) t seen)
            env))
        (eval-constraint-alist-aux (cdr x)
          (hons-acons (caar x) t seen)
          env))))
  ///
  (local (defun ind
      (x seen)
      (declare (xargs :measure (len x)))
      (if (atom x)
        seen
        (list (ind (cdr x) seen)
          (ind (cdr x)
            (hons-acons (caar x) t seen))
          (ind (calist-remassocs (cdr x) (alist-keys seen))
            (hons-acons (caar x) t nil))))))
  (local (defthm set-equiv-of-append-to-cons
      (set-equiv (append seen (list k))
        (cons k seen))))
  (defthm eval-constraint-alist-aux-of-seen
    (implies (syntaxp (not (equal seen ''nil)))
      (equal (eval-constraint-alist-aux x seen env)
        (eval-constraint-alist-aux (calist-remassocs x (alist-keys seen))
          nil
          env)))
    :hints (("Goal" :in-theory (e/d (calist-remassocs))
       :induct (ind x seen)))))

(define eval-constraint-alist
  (x env)
  :measure (len x)
  :verify-guards nil
  (mbe :logic (if (atom x)
      t
      (if (consp (car x))
        (let ((rest (eval-constraint-alist (calist-remassocs (cdr x) (list (caar x)))
               env)))
          (if (cdar x)
            (and (iff (aig-eval (caar x) env)
                (eql (cdar x) 1))
              rest)
            rest))
        (eval-constraint-alist (cdr x) env)))
    :exec (eval-constraint-alist-aux x nil env))
  ///
  (local (defthm set-equiv-of-cons-redundant
      (implies (member k x)
        (set-equiv (cons k x) x))))
  (defthm eval-constraint-alist-aux-redef
    (equal (eval-constraint-alist-aux x nil env)
      (eval-constraint-alist x env))
    :hints (("Goal" :in-theory (enable eval-constraint-alist-aux
         calist-remassocs))))
  (verify-guards eval-constraint-alist)
  (defthm eval-constraint-alist-of-shrink-constraint-alist
    (equal (eval-constraint-alist (shrink-constraint-alist x)
        env)
      (eval-constraint-alist x env))
    :hints (("Goal" :in-theory (enable shrink-constraint-alist)
       :induct (eval-constraint-alist x env)
       :expand ((:free (a b)
          (eval-constraint-alist (cons a b) env))))))
  (defthm equal-1-of-lookup-when-eval-constraint-alist
    (implies (eval-constraint-alist calist env)
      (equal (equal 1 (calist-lookup x calist))
        (and (calist-lookup x calist)
          (aig-eval x env))))))

(local (in-theory (disable (:t calist-lookup$inline))))

(define eval-constraint-alist-witness
  (x env)
  :measure (len x)
  (if (atom x)
    t
    (if (consp (car x))
      (let ((rest (eval-constraint-alist-witness (calist-remassocs (cdr x) (list (caar x)))
             env)))
        (if (cdar x)
          (if (xor (aig-eval (caar x) env)
              (eql (cdar x) 1))
            (caar x)
            rest)
          rest))
      (eval-constraint-alist-witness (cdr x) env)))
  ///
  (defthm eval-constraint-alist-in-terms-of-witness
    (implies (rewriting-positive-literal `(eval-constraint-alist ,GL::X ,GL::ENV))
      (equal (eval-constraint-alist x env)
        (b* ((k (eval-constraint-alist-witness x env)))
          (or (not (calist-lookup k x))
            (iff (aig-eval k env)
              (equal (calist-lookup k x) 1))))))
    :hints (("Goal" :induct (eval-constraint-alist-witness x env)
       :expand ((eval-constraint-alist x env) (eval-constraint-alist-witness x env))
       :in-theory (disable (:d eval-constraint-alist-witness))))))

(define constraint-alist->aig-aux
  (x seen)
  (if (atom x)
    (prog2$ (fast-alist-free seen) t)
    (if (and (consp (car x))
        (not (hons-get (caar x) seen)))
      (if (cdar x)
        (aig-and (aig-iff (caar x) (equal (cdar x) 1))
          (constraint-alist->aig-aux (cdr x)
            (hons-acons (caar x) t seen)))
        (constraint-alist->aig-aux (cdr x)
          (hons-acons (caar x) t seen)))
      (constraint-alist->aig-aux (cdr x) seen)))
  ///
  (local (defun ind
      (x seen)
      (declare (xargs :measure (len x)))
      (if (atom x)
        seen
        (list (ind (cdr x) seen)
          (ind (cdr x)
            (hons-acons (caar x) t seen))
          (ind (calist-remassocs (cdr x) (alist-keys seen))
            (hons-acons (caar x) t nil))))))
  (local (defthm set-equiv-of-append-to-cons
      (set-equiv (append seen (list k))
        (cons k seen))))
  (defthm constraint-alist->aig-aux-of-seen
    (implies (syntaxp (not (equal seen ''nil)))
      (equal (constraint-alist->aig-aux x seen)
        (constraint-alist->aig-aux (calist-remassocs x (alist-keys seen))
          nil)))
    :hints (("goal" :in-theory (e/d (calist-remassocs))
       :induct (ind x seen)))))

(define constraint-alist->aig
  (x)
  :measure (len x)
  :verify-guards nil
  (mbe :logic (if (atom x)
      t
      (if (consp (car x))
        (let ((rest (constraint-alist->aig (calist-remassocs (cdr x) (list (caar x))))))
          (if (cdar x)
            (aig-and (aig-iff (caar x) (eql (cdar x) 1)) rest)
            rest))
        (constraint-alist->aig (cdr x))))
    :exec (constraint-alist->aig-aux x nil))
  ///
  (defthm constraint-alist->aig-aux-redef
    (equal (constraint-alist->aig-aux x nil)
      (constraint-alist->aig x))
    :hints (("Goal" :in-theory (enable constraint-alist->aig-aux))))
  (verify-guards constraint-alist->aig)
  (local (defthm set-equiv-of-cons-redundant
      (implies (member k x)
        (set-equiv (cons k x) x))))
  (defthm constraint-alist->aig-of-shrink-constraint-alist
    (equal (constraint-alist->aig (shrink-constraint-alist x))
      (constraint-alist->aig x))
    :hints (("Goal" :in-theory (enable shrink-constraint-alist)
       :induct (constraint-alist->aig x)
       :expand ((:free (a b)
          (constraint-alist->aig (cons a b)))))))
  (defthm eval-of-constraint-alist->aig
    (equal (aig-eval (constraint-alist->aig x) env)
      (eval-constraint-alist x env))
    :hints (("Goal" :in-theory (e/d (eval-constraint-alist aig-eval)
         (eval-constraint-alist-in-terms-of-witness)))))
  (defthm sets-in-aig-vars-of-aig-iff
    (implies (and (not (in v (aig-vars a)))
        (not (in v (aig-vars b))))
      (not (in v (aig-vars (aig-iff a b)))))
    :hints (("Goal" :in-theory (enable aig-iff aig-or))))
  (defthm constraint-alist->aig-of-remove-none
    (equal (constraint-alist->aig (calist-remassocs x nil))
      (constraint-alist->aig x))
    :hints (("Goal" :in-theory (enable calist-remassocs)))))

(define constr-alist-depends-on
  (v x)
  :measure (len x)
  :verify-guards nil
  (if (atom x)
    nil
    (if (consp (car x))
      (if (cdar x)
        (or (in (aig-var-fix v) (aig-vars (caar x)))
          (constr-alist-depends-on v
            (calist-remassocs (cdr x) (list (caar x)))))
        (constr-alist-depends-on v
          (calist-remassocs (cdr x) (list (caar x)))))
      (constr-alist-depends-on v (cdr x))))
  ///
  (defcong aig-var-equiv
    equal
    (constr-alist-depends-on v x)
    1
    :package :legacy)
  (local (defthm set-equiv-of-cons-redundant
      (implies (member k x)
        (set-equiv (cons k x) x))))
  (defthm constr-alist-depends-on-of-shrink-constraint-alist
    (equal (constr-alist-depends-on v
        (shrink-constraint-alist x))
      (constr-alist-depends-on v x))
    :hints (("Goal" :in-theory (enable shrink-constraint-alist)
       :induct (constr-alist-depends-on v x)
       :expand ((:free (a b)
          (constr-alist-depends-on v (cons a b)))))))
  (local (defthm aig-eval-of-acons-when-var-not-present
      (implies (not (in v (aig-vars x)))
        (equal (aig-eval x (cons (cons v y) env))
          (aig-eval x env)))
      :hints (("Goal" :in-theory (enable aig-eval aig-vars)))))
  (defthm constr-alist-depends-on-correct
    (implies (and (not (constr-alist-depends-on (double-rewrite v)
            x))
        (aig-var-p v))
      (equal (eval-constraint-alist x
          (cons (cons v val) env))
        (eval-constraint-alist x env)))
    :hints (("Goal" :in-theory (enable eval-constraint-alist))))
  (local (defthm in-aig-vars-of-aig-iff
      (implies (and (not (in v (aig-vars a)))
          (not (in v (aig-vars b))))
        (not (in v (aig-vars (aig-iff a b)))))
      :hints (("Goal" :in-theory (enable aig-iff aig-or)))))
  (defthm dependencies-of-constraint-alist->aig
    (implies (and (not (constr-alist-depends-on (double-rewrite v)
            x))
        (aig-var-p v))
      (not (in v (aig-vars (constraint-alist->aig x)))))
    :hints (("Goal" :in-theory (enable constraint-alist->aig))))
  (defthm constr-alist-depends-on-of-remassocs
    (implies (not (constr-alist-depends-on k x))
      (not (constr-alist-depends-on k
          (calist-remassocs x seen))))
    :hints (("Goal" :in-theory (enable calist-remassocs)))))

(define aig-under-constraint-alist
  (x calist)
  (b* (((when (booleanp x)) x) ((mv negp xabs) (if (and (not (aig-atom-p x)) (eq (cdr x) nil))
          (mv t (car x))
          (mv nil x)))
      (look (calist-lookup xabs calist))
      ((when look) (xor (eql 1 look) negp))
      ((when (aig-atom-p xabs)) x)
      ((when negp) x)
      (car (aig-under-constraint-alist (car xabs) calist))
      ((when (eq car nil)) nil)
      (cdr (aig-under-constraint-alist (cdr xabs) calist))
      (newx (aig-and-dumb car cdr))
      (look (calist-lookup newx calist))
      ((when look) (eql 1 look)))
    newx)
  ///
  (defthm aig-under-constraint-alist-of-shrink-constraint-alist
    (equal (aig-under-constraint-alist x
        (shrink-constraint-alist calist))
      (aig-under-constraint-alist x calist)))
  (defthm aig-under-constraint-alist-correct
    (implies (eval-constraint-alist calist env)
      (equal (aig-eval (aig-under-constraint-alist x calist)
          env)
        (aig-eval x env)))
    :hints (("Goal" :in-theory (enable aig-under-constraint-alist aig-eval))))
  (defthm aig-under-constraint-alist-bfr-depends
    (implies (and (bfr-mode) (not (bfr-depends-on k x)))
      (not (bfr-depends-on k
          (aig-under-constraint-alist x calist))))
    :hints (("Goal" :in-theory (enable bfr-depends-on))))
  (defthm aig-under-constraint-alist-pbfr-depends
    (implies (and (bfr-mode)
        (not (pbfr-depends-on k p x)))
      (not (pbfr-depends-on k
          p
          (aig-under-constraint-alist x calist))))
    :hints (("Goal" :in-theory (enable pbfr-depends-on bfr-from-param-space))))
  (defthm aig-under-constraint-alist-idempotent
    (equal (aig-under-constraint-alist (aig-under-constraint-alist x calist)
        calist)
      (aig-under-constraint-alist x calist))
    :hints (("goal" :induct (aig-under-constraint-alist x calist)) (and stable-under-simplificationp
        '(:in-theory (enable aig-and-dumb)))))
  (defthm aig-under-constraint-alist-of-t-and-nil
    (and (equal (aig-under-constraint-alist t calist) t)
      (equal (aig-under-constraint-alist nil calist) nil))))

(define constraint-alist-delete-keys
  (keys calist)
  (if (atom keys)
    calist
    (hons-acons (car keys)
      nil
      (constraint-alist-delete-keys (cdr keys) calist)))
  ///
  (local (defthm remassocs-of-shrink-when-no-keys
      (implies (not (consp keys))
        (equal (calist-remassocs (shrink-constraint-alist x)
            keys)
          (shrink-constraint-alist x)))
      :hints (("Goal" :in-theory (enable calist-remassocs
           shrink-constraint-alist)))))
  (local (defthm calist-remassocs-compose-strong
      (implies (equal y (calist-remassocs x seen1))
        (equal (calist-remassocs y seen2)
          (calist-remassocs x (append seen1 seen2))))))
  (defthm shrink-of-constraint-alist-delete-keys
    (equal (shrink-constraint-alist (constraint-alist-delete-keys keys calist))
      (calist-remassocs (shrink-constraint-alist calist)
        keys))
    :hints (("Goal" :in-theory (enable shrink-constraint-alist
         calist-remassocs
         pairlis$)
       :expand ((shrink-constraint-alist calist) (:free (seen)
           (calist-remassocs calist seen))))))
  (defthm lookup-of-constraint-alist-delete-keys
    (equal (calist-lookup k
        (constraint-alist-delete-keys keys calist))
      (and (not (member k keys))
        (calist-lookup k calist))))
  (defthm constraint-alist-delete-nil
    (equal (constraint-alist-delete-keys nil calist)
      calist)))

(define constraint-alist-assume-aig
  (x calist keys-acc)
  :returns (mv contradictionp calist num-aconses)
  (b* (((when (booleanp x)) (mv (not x) calist keys-acc)) ((mv negp xabs) (if (and (not (aig-atom-p x)) (eq (cdr x) nil))
          (mv t (car x))
          (mv nil x)))
      (look (calist-lookup xabs calist))
      ((when look) (if (xor (eql 1 look) negp)
          (mv nil calist keys-acc)
          (mv t calist keys-acc)))
      ((when (aig-atom-p xabs)) (mv nil
          (hons-acons xabs
            (if negp
              0
              1)
            calist)
          (cons xabs keys-acc)))
      ((when negp) (mv nil
          (hons-acons xabs 0 calist)
          (cons xabs keys-acc)))
      ((mv contradictionp1 calist keys-acc) (constraint-alist-assume-aig (car xabs)
          calist
          keys-acc))
      ((mv contradictionp2 calist keys-acc) (constraint-alist-assume-aig (cdr xabs)
          calist
          keys-acc)))
    (mv (or contradictionp1 contradictionp2)
      calist
      keys-acc))
  ///
  (local (defun shrink-ind
      (x calist keys-acc)
      (b* (((when (booleanp x)) keys-acc) ((mv negp xabs) (if (and (not (aig-atom-p x)) (eq (cdr x) nil))
              (mv t (car x))
              (mv nil x)))
          (look (calist-lookup xabs calist))
          ((when look) keys-acc)
          ((when (aig-atom-p xabs)) keys-acc)
          ((when negp) keys-acc)
          (?ign (shrink-ind (car xabs) calist keys-acc))
          ((mv ?contradictionp1 scalist skeys-acc) (constraint-alist-assume-aig (car xabs)
              (shrink-constraint-alist calist)
              keys-acc))
          ((mv ?contradictionp1 calist keys-acc) (constraint-alist-assume-aig (car xabs)
              calist
              keys-acc))
          (?ign (shrink-ind (cdr xabs) calist keys-acc)))
        (shrink-ind (cdr xabs) scalist skeys-acc))))
  (local (defthm set-equiv-switch
      (set-equiv (cons b (cons a lst))
        (cons a (cons b lst)))
      :hints (("Goal" :in-theory (enable set-unequal-witness-rw)))))
  (defthm constraint-alist-assume-aig-of-shrink
    (b* (((mv scontra snew-calist skeys) (constraint-alist-assume-aig x
           (shrink-constraint-alist calist)
           keys-acc)) ((mv contra new-calist keys) (constraint-alist-assume-aig x
            calist
            keys-acc)))
      (and (equal scontra contra)
        (equal (shrink-constraint-alist snew-calist)
          (shrink-constraint-alist new-calist))
        (equal skeys keys)))
    :hints (("goal" :induct (shrink-ind x calist keys-acc)
       :expand ((:free (a b)
          (shrink-constraint-alist (cons a b)))))))
  (local (defthm eval-of-calist-remassocs-when-not-present
      (implies (not (calist-lookup k calist))
        (equal (eval-constraint-alist (calist-remassocs calist (list k))
            env)
          (eval-constraint-alist calist env)))
      :hints (("Goal" :in-theory (enable eval-constraint-alist calist-remassocs)
         :expand ((:free (a b)
            (eval-constraint-alist (cons a b) env)))))))
  (defthm constraint-alist-assume-aig-remains-false
    (b* (((mv ?contradictionp ?new-calist ?keys-out) (constraint-alist-assume-aig x
           calist
           keys-in)))
      (implies (not (eval-constraint-alist calist env))
        (not (eval-constraint-alist new-calist env))))
    :hints (("Goal" :in-theory (e/d (eval-constraint-alist)
         (eval-constraint-alist-in-terms-of-witness))
       :expand ((:free (a b)
          (eval-constraint-alist (cons a b) env)))
       :induct (constraint-alist-assume-aig x
         calist
         keys-in))))
  (defthm constraint-alist-assume-aig-correct
    (b* (((mv ?contradictionp ?new-calist ?keys-out) (constraint-alist-assume-aig x
           calist
           keys-in)))
      (implies (and (eval-constraint-alist calist env)
          (not contradictionp))
        (equal (eval-constraint-alist new-calist env)
          (aig-eval x env))))
    :hints (("Goal" :in-theory (e/d (eval-constraint-alist aig-eval)
         (eval-constraint-alist-in-terms-of-witness))
       :expand ((:free (a b)
          (eval-constraint-alist (cons a b) env)))
       :induct (constraint-alist-assume-aig x
         calist
         keys-in))))
  (defthm constraint-alist-assume-aig-contradictionp
    (b* (((mv ?contradictionp ?new-calist ?keys-out) (constraint-alist-assume-aig x
           calist
           keys-in)))
      (implies (and (eval-constraint-alist calist env)
          (aig-eval x env))
        (not contradictionp)))
    :hints (("goal" :in-theory (enable aig-eval)
       :induct (constraint-alist-assume-aig x
         calist
         keys-in))))
  (local (defun ind
      (calist lst)
      (if (atom calist)
        lst
        (list (ind (cdr calist) lst)
          (ind (cdr calist) (cons (caar calist) lst))))))
  (local (defthm set-equiv-of-cons-redundant
      (implies (member k x)
        (set-equiv (cons k x) x))))
  (defthm remassocs-of-shrink-when-not-present
    (implies (not (calist-lookup k calist))
      (equal (calist-remassocs (shrink-constraint-alist calist)
          (cons k lst))
        (calist-remassocs (shrink-constraint-alist calist)
          lst)))
    :hints (("Goal" :expand ((shrink-constraint-alist calist) (:free (a b lst)
           (calist-remassocs (cons a b) lst))
         (:free (lst) (calist-remassocs nil lst)))
       :induct (ind calist lst))))
  (defthm constraint-alist-delete-keys-of-assume-aig
    (b* (((mv ?contradictionp ?new-calist ?keys-out) (constraint-alist-assume-aig x
           calist
           keys-in)))
      (equal (calist-remassocs (shrink-constraint-alist new-calist)
          keys-out)
        (calist-remassocs (shrink-constraint-alist calist)
          keys-in)))
    :hints (("Goal" :in-theory (enable shrink-constraint-alist)
       :expand ((:free (a b lst)
          (calist-remassocs (cons a b) lst)))
       :induct (constraint-alist-assume-aig x
         calist
         keys-in))))
  (defthm dependencies-of-constraint-alist-assume-aig
    (b* (((mv ?contradictionp ?new-calist ?keys-out) (constraint-alist-assume-aig x
           calist
           keys-in)))
      (implies (and (not (in (aig-var-fix k) (aig-vars x)))
          (not (constr-alist-depends-on k calist)))
        (not (constr-alist-depends-on k new-calist))))
    :hints (("Goal" :in-theory (e/d nil
         ((:d constraint-alist-assume-aig) subsetp-car-member
           aig-vars
           in
           subset
           union))
       :induct (constraint-alist-assume-aig x
         calist
         keys-in)
       :expand ((:free (a b)
          (constr-alist-depends-on k (cons a b))) (aig-vars x)
         (constraint-alist-assume-aig x
           calist
           keys-in))))))

(define calist-equiv
  (x y)
  :enabled t
  (equal (shrink-constraint-alist x)
    (shrink-constraint-alist y))
  ///
  (defequiv calist-equiv)
  (defmacro def-calist-equiv-cong
    (resequiv call)
    (let ((argnum (index-of 'x call)))
      `(encapsulate nil
        (local (defthm calist-cong-lemma
            (,GL::RESEQUIV ,(GL::UPDATE-NTH GL::ARGNUM `(GL::SHRINK-CONSTRAINT-ALIST GL::X) GL::CALL)
              ,GL::CALL)
            :rule-classes nil))
        (local (in-theory '(calist-equiv)))
        (defcong calist-equiv
          ,GL::RESEQUIV
          ,GL::CALL
          ,GL::ARGNUM
          :package :legacy :hints (("goal" :use ((:instance calist-cong-lemma) (:instance calist-cong-lemma (x x-equiv)))))))))
  (def-calist-equiv-cong equal
    (calist-lookup k x))
  (def-calist-equiv-cong equal
    (shrink-constraint-alist x))
  (def-calist-equiv-cong calist-equiv
    (calist-remassocs x keys))
  (def-calist-equiv-cong equal
    (eval-constraint-alist x env))
  (def-calist-equiv-cong equal
    (constraint-alist->aig x))
  (def-calist-equiv-cong equal
    (aig-under-constraint-alist a x))
  (def-calist-equiv-cong calist-equiv
    (constraint-alist-delete-keys keys x)))

(defstobj hyp$c
  (hyp-calist :type t)
  (calist-len :type (integer 0 *) :initially 0)
  (calist-nkeys :type (integer 0 *) :initially 0)
  (hyp-bfr-mode :type t)
  :renaming ((calist-len calist-len1) (calist-nkeys calist-nkeys1)))

(define calist-len
  (hyp$c)
  :enabled t
  (lnfix (calist-len1 hyp$c)))

(define calist-nkeys
  (hyp$c)
  :enabled t
  (lnfix (calist-nkeys1 hyp$c)))

(define maybe-shrink-hyp$c
  (hyp$c)
  (if (< (* 2 (calist-nkeys hyp$c))
      (calist-len hyp$c))
    (b* ((hyp$c (update-hyp-calist (shrink-constraint-alist (hyp-calist hyp$c))
           hyp$c)))
      (update-calist-len (calist-nkeys hyp$c)
        hyp$c))
    hyp$c)
  ///
  (defthm maybe-shrink-hyp$c-preserves-calist-equiv
    (calist-equiv (nth 0 (maybe-shrink-hyp$c hyp$c))
      (nth 0 hyp$c))))

(define bfr-hyp-mode-equiv
  (hyp1 hyp2)
  :verify-guards nil
  (bfr-case :bdd (equal hyp1 hyp2)
    :aig (calist-equiv hyp1 hyp2))
  ///
  (defequiv bfr-hyp-mode-equiv))

(define bfr-hyp-mode-fix
  (hyp)
  (bfr-case :bdd hyp
    :aig (shrink-constraint-alist hyp))
  ///
  (defcong bfr-hyp-mode-equiv
    equal
    (bfr-hyp-mode-fix hyp)
    1
    :package :legacy :hints (("Goal" :in-theory (enable bfr-hyp-mode-equiv))))
  (defthm bfr-hyp-mode-equiv-of-bfr-hyp-mode-fix
    (bfr-hyp-mode-equiv (bfr-hyp-mode-fix hyp)
      hyp)
    :hints (("Goal" :in-theory (enable bfr-hyp-mode-equiv))))
  (defthmd bfr-hyp-mode-equiv-in-terms-of-bfr-hyp-mode-fix
    (equal (bfr-hyp-mode-equiv hyp1 hyp2)
      (equal (bfr-hyp-mode-fix hyp1)
        (bfr-hyp-mode-fix hyp2)))
    :hints (("Goal" :in-theory (enable bfr-hyp-mode-equiv))))
  (defthm bfr-hyp-mode-fix-idempotent
    (equal (bfr-hyp-mode-fix (bfr-hyp-mode-fix x))
      (bfr-hyp-mode-fix x))))

(define bfr-hyp-mode-eval
  (hyp env)
  (bfr-case :bdd (bfr-eval hyp env)
    :aig (eval-constraint-alist hyp env))
  ///
  (defthm bfr-hyp-mode-eval-of-bfr-hyp-mode-fix
    (equal (bfr-hyp-mode-eval (bfr-hyp-mode-fix hyp)
        env)
      (bfr-hyp-mode-eval hyp env))
    :hints (("Goal" :in-theory (enable bfr-hyp-mode-fix))))
  (defcong bfr-hyp-mode-equiv
    equal
    (bfr-hyp-mode-eval hyp env)
    1
    :hints (("Goal" :in-theory (e/d (bfr-hyp-mode-equiv-in-terms-of-bfr-hyp-mode-fix)
         (bfr-hyp-mode-eval-of-bfr-hyp-mode-fix))
       :use ((:instance bfr-hyp-mode-eval-of-bfr-hyp-mode-fix) (:instance bfr-hyp-mode-eval-of-bfr-hyp-mode-fix
           (hyp hyp-equiv)))))))

(define bfr-hyp-init$c
  (hyp$c)
  (bfr-case :bdd (b* ((hyp$c (update-hyp-bfr-mode nil hyp$c)))
      (update-hyp-calist t hyp$c))
    :aig (b* ((hyp$c (update-hyp-bfr-mode t hyp$c)) (hyp$c (update-hyp-calist nil hyp$c))
        (hyp$c (update-calist-len 0 hyp$c)))
      (update-calist-nkeys 0 hyp$c))))

(define maybe-bfr-hyp-init$c
  (hyp$c)
  (bfr-case :bdd (if (hyp-bfr-mode hyp$c)
      (bfr-hyp-init$c hyp$c)
      hyp$c)
    :aig (if (hyp-bfr-mode hyp$c)
      hyp$c
      (bfr-hyp-init$c hyp$c))))

(define bfr-constr-init
  nil
  (bfr-case :bdd t :aig nil)
  ///
  (in-theory (disable (bfr-constr-init)))
  (defthm eval-of-bfr-constr-init
    (equal (bfr-hyp-mode-eval (bfr-constr-init) env)
      t)
    :hints (("Goal" :in-theory (enable bfr-hyp-mode-eval)))))

(defaggregate hyppair
  ((bfr-mode) (hyp))
  :layout :list)

(define bfr-hyp-fix
  ((h hyppair-p))
  :returns (new-hyp hyppair-p :hyp :guard)
  (b* (((hyppair h)))
    (hyppair (and (bfr-mode) t)
      (bfr-case :bdd (if h.bfr-mode
          t
          h.hyp)
        :aig (if h.bfr-mode
          (shrink-constraint-alist h.hyp)
          nil))))
  ///
  (defthm bfr-hyp-fix-idempotent
    (equal (bfr-hyp-fix (bfr-hyp-fix x))
      (bfr-hyp-fix x))))

(define bfr-hyp-equiv
  ((h1 hyppair-p) (h2 hyppair-p))
  (equal (bfr-hyp-fix h1) (bfr-hyp-fix h2))
  ///
  (defequiv bfr-hyp-equiv)
  (defcong bfr-hyp-equiv
    equal
    (bfr-hyp-fix h)
    1)
  (defthm bfr-hyp-fix-under-bfr-hyp-equiv
    (bfr-hyp-equiv (bfr-hyp-fix h) h)))

(defun hyp-congruences-fn
  (fn hints
    pres-hints
    hyp-fix-hints
    retval
    curr-pkg
    world)
  (declare (xargs :mode :program))
  (b* ((formals (formals fn world)) (stobjs-out (stobjs-out fn world))
      (preserves-thm (intern-in-package-of-symbol (concatenate 'string (symbol-name fn) "-PRESERVES-HYP")
          fn))
      (hyp-fix-thm (intern-in-package-of-symbol (concatenate 'string (symbol-name fn) "-OF-BFR-HYP-FIX")
          fn))
      (hyp-var (cond ((member 'hyp formals) 'hyp)
          ((member 'pathcond formals) 'pathcond)
          ((member 'hyp$a formals) 'hyp$a)
          ((member 'constr formals) 'constr)
          ((member 'h formals) 'h)
          (t (er hard?
              'hyp-congruences
              "~x0 does not appear to take a hyp as an argument~%"
              fn))))
      (hyp-var-equiv (gen-sym-sym (list hyp-var '-equiv)
          (pkg-witness curr-pkg)))
      (out-idx (or retval (index-of hyp-var stobjs-out))))
    `(progn ,@(AND GL::OUT-IDX
       `((GL::DEFTHM ,GL::PRESERVES-THM
          (EQUAL (GL::MV-NTH ,GL::OUT-IDX (,GL::FN . ,GL::FORMALS))
                 (GL::BFR-HYP-FIX ,GL::HYP-VAR))
          :HINTS ,(OR GL::PRES-HINTS GL::HINTS))))
      (defthm ,GL::HYP-FIX-THM
        (equal (,GL::FN . ,(SUBST `(GL::BFR-HYP-FIX ,GL::HYP-VAR) GL::HYP-VAR GL::FORMALS))
          (,GL::FN . ,GL::FORMALS))
        :hints ,(OR GL::HYP-FIX-HINTS GL::HINTS))
      (defcong bfr-hyp-equiv
        equal
        (,GL::FN . ,GL::FORMALS)
        ,(+ 1 (INDEX-OF GL::HYP-VAR GL::FORMALS))
        :hints (("goal" :in-theory '(bfr-hyp-equiv)
           :use ((:instance ,GL::HYP-FIX-THM) (:instance ,GL::HYP-FIX-THM
               (,GL::HYP-VAR ,GL::HYP-VAR-EQUIV)))))))))

(defmacro def-hyp-congruence
  (fn &key
    hints
    pres-hints
    hyp-fix-hints
    retval)
  `(make-event (hyp-congruences-fn ',GL::FN
      ',GL::HINTS
      ',GL::PRES-HINTS
      ',GL::HYP-FIX-HINTS
      ',GL::RETVAL
      (current-package state)
      (w state))))

(define bfr-hyp-eval
  ((h hyppair-p) env)
  (b* (((hyppair h)))
    (bfr-case :bdd (if h.bfr-mode
        t
        (bfr-eval h.hyp env))
      :aig (if h.bfr-mode
        (eval-constraint-alist h.hyp env)
        t)))
  ///
  (def-hyp-congruence bfr-hyp-eval
    :hints (("Goal" :in-theory (enable bfr-hyp-fix))))
  (defthm bfr-hyp-eval-in-terms-of-bfr-hyp-mode-eval
    (implies (iff (bfr-mode) (hyppair->bfr-mode h))
      (equal (bfr-hyp-eval h env)
        (bfr-hyp-mode-eval (hyppair->hyp h) env)))
    :hints (("Goal" :in-theory (enable bfr-hyp-mode-eval))))
  (defthm bfr-hyp-eval-when-bad-mode
    (implies (xor (bfr-mode) (hyppair->bfr-mode h))
      (equal (bfr-hyp-eval h env) t))
    :hints (("Goal" :in-theory (enable bfr-hyp-mode-eval))))
  (defthm bfr-hyp-eval-of-bfr-hyp-fix
    (equal (bfr-hyp-eval (bfr-hyp-fix h) env)
      (bfr-hyp-eval h env))
    :hints ((and stable-under-simplificationp
       '(:in-theory (enable bfr-hyp-eval
           bfr-hyp-mode-eval
           bfr-hyp-fix)))))
  (defcong bfr-hyp-equiv
    equal
    (bfr-hyp-eval h env)
    1
    :hints (("Goal" :in-theory (e/d (bfr-hyp-equiv)
         (bfr-hyp-eval bfr-hyp-eval-of-bfr-hyp-fix))
       :use ((:instance bfr-hyp-eval-of-bfr-hyp-fix (h h)) (:instance bfr-hyp-eval-of-bfr-hyp-fix
           (h h-equiv))))))
  (defthm bfr-hyp-mode-eval-of-bfr-hyp-fix
    (equal (bfr-hyp-mode-eval (hyppair->hyp (bfr-hyp-fix h))
        env)
      (bfr-hyp-eval h env))
    :hints ((and stable-under-simplificationp
       '(:in-theory (e/d (bfr-hyp-eval bfr-hyp-mode-eval
             bfr-hyp-fix
             eval-constraint-alist)
           (eval-constraint-alist-in-terms-of-witness)))))))

(define bfr-hyp-init$a
  (hyp$a)
  (declare (ignore hyp$a))
  :returns (new-hyp hyppair-p)
  (bfr-case :bdd (hyppair nil t)
    :aig (hyppair t (shrink-constraint-alist nil)))
  ///
  (def-hyp-congruence bfr-hyp-init$a
    :hints (("Goal" :in-theory (enable bfr-hyp-fix))))
  (defthm bfr-hyp-init-norm
    (implies (syntaxp (not (equal hyp$a ''nil)))
      (equal (bfr-hyp-init$a hyp$a)
        (bfr-hyp-init$a nil))))
  (defthm eval-of-bfr-hyp-init$a
    (equal (bfr-hyp-eval (bfr-hyp-init$a hyp$a) env)
      t)
    :hints (("Goal" :in-theory (enable bfr-hyp-mode-eval bfr-hyp-eval))))
  (defthm bfr-hyp-mode-fix-of-bfr-hyp-init$a
    (equal (bfr-hyp-fix (bfr-hyp-init$a hyp$a))
      (bfr-hyp-init$a hyp$a))
    :hints (("Goal" :in-theory (e/d (bfr-hyp-fix) ((bfr-hyp-fix)))))))

(define hyp$ap
  (hyp$a)
  :enabled t
  (hyppair-p hyp$a))

(define bfr-assume$c
  (x hyp$c)
  :returns (mv contradictionp new-hyp undo-info)
  (b* ((hyp$c (maybe-bfr-hyp-init$c hyp$c)))
    (bfr-case :bdd (b* ((orig (hyp-calist hyp$c)) (and (q-and x orig))
          (hyp$c (update-hyp-calist and hyp$c)))
        (mv (not and) hyp$c orig))
      :aig (b* (((mv contra hyp keys) (constraint-alist-assume-aig x
             (hyp-calist hyp$c)
             nil)) (hyp$c (update-hyp-calist hyp hyp$c))
          (nkeys (len keys))
          (hyp$c (update-calist-len (+ nkeys (calist-len hyp$c))
              hyp$c))
          (hyp$c (update-calist-nkeys (+ nkeys (calist-nkeys hyp$c))
              hyp$c))
          (hyp$c (maybe-shrink-hyp$c hyp$c)))
        (mv contra hyp$c keys)))))

(define bfr-constr-assume
  (x constr)
  :guard-hints (("goal" :in-theory (enable bfr-binary-and)))
  (bfr-case :bdd (b* ((and (mbe :logic (bfr-and x constr)
           :exec (q-and x constr))))
      (mv (not and) and constr))
    :aig (b* (((mv contra constr keys) (constraint-alist-assume-aig x constr nil)))
      (mv contra constr keys)))
  ///
  (defthm bfr-constr-assume-correct
    (b* (((mv ?contradictionp ?new-hyp ?undo-info) (bfr-constr-assume x hyp)))
      (implies (and (rewriting-negative-literal `(mv-nth '0 (bfr-constr-assume ,GL::X ,GL::HYP)))
          (bfr-hyp-mode-eval hyp env))
        (iff contradictionp
          (and (not (bfr-eval x env))
            (hide contradictionp)))))
    :hints (("Goal" :in-theory (enable bfr-hyp-mode-eval
         bfr-eval
         bfr-binary-and)) (and stable-under-simplificationp
        '(:use ((:instance eval-bdd-of-q-and
             (x hyp)
             (y x)
             (values env)))
          :expand ((:free (x) (hide x)))
          :in-theory (disable eval-bdd-of-q-and)))))
  (defthm bfr-constr-assume->hyp-correct
    (b* (((mv ?contradictionp ?new-hyp ?undo-info) (bfr-constr-assume x hyp)))
      (implies (and (bfr-hyp-mode-eval hyp env)
          (not contradictionp))
        (equal (bfr-hyp-mode-eval new-hyp env)
          (bfr-eval x env))))
    :hints (("Goal" :in-theory (enable bfr-hyp-mode-eval bfr-eval))))
  (defthm bfr-constr-assume-false
    (b* (((mv ?contradictionp ?new-hyp ?undo-info) (bfr-constr-assume x hyp)))
      (implies (and (rewriting-positive-literal `(bfr-hyp-mode-eval (mv-nth '1 (bfr-constr-assume ,GL::X ,GL::HYP))
              ,GL::ENV))
          (bfr-hyp-mode-eval hyp env))
        (equal (bfr-hyp-mode-eval new-hyp env)
          (or (bfr-eval x env)
            (hide (bfr-hyp-mode-eval new-hyp env))))))
    :hints (("goal" :expand ((:free (x) (hide x)))
       :in-theory (disable bfr-constr-assume)) (and stable-under-simplificationp
        '(:expand nil
          :cases ((mv-nth 0 (bfr-constr-assume x hyp))))))))

(define bfr-assume$a
  (x hyp$a)
  :guard (hyp$ap hyp$a)
  (b* ((hyp$a (bfr-hyp-fix hyp$a)) ((hyppair hyp$a))
      ((mv contra constr undo) (bfr-constr-assume x hyp$a.hyp)))
    (mv contra
      (hyppair (and (bfr-mode) t)
        (bfr-hyp-mode-fix constr))
      undo))
  ///
  (def-hyp-congruence bfr-assume$a
    :hints (("Goal" :in-theory (enable bfr-hyp-fix))))
  (local (defthm bfr-constr-assume-correct-bind
      (b* (((mv ?contradictionp ?new-hyp ?undo-info) (bfr-constr-assume x hyp)))
        (implies (and (rewriting-negative-literal `(mv-nth '0 (bfr-constr-assume ,GL::X ,GL::HYP)))
            (bind-free '((env . env)) (env))
            (bfr-hyp-mode-eval hyp env))
          (iff contradictionp
            (and (not (bfr-eval x env))
              (hide contradictionp)))))
      :hints (("goal" :use bfr-constr-assume-correct
         :expand ((:free (x) (hide x)))))))
  (defthm bfr-assume-correct
    (b* (((mv ?contradictionp ?new-hyp ?undo-info) (bfr-assume$a x hyp)))
      (implies (and (rewriting-negative-literal `(mv-nth '0 (bfr-assume$a ,GL::X ,GL::HYP)))
          (bfr-hyp-eval hyp env))
        (iff contradictionp
          (and (not (bfr-eval x env))
            (hide contradictionp)))))
    :hints (("goal" :expand ((:free (x) (hide x))))))
  (defthm bfr-assume->hyp-correct
    (b* (((mv ?contradictionp ?new-hyp ?undo-info) (bfr-assume$a x hyp)))
      (implies (and (bfr-hyp-eval hyp env)
          (not contradictionp))
        (equal (bfr-hyp-eval new-hyp env)
          (bfr-eval x env)))))
  (defthm bfr-assume-false
    (b* (((mv ?contradictionp ?new-hyp ?undo-info) (bfr-assume$a x hyp)))
      (implies (and (rewriting-positive-literal `(bfr-hyp-eval (mv-nth '1 (bfr-assume$a ,GL::X ,GL::HYP))
              ,GL::ENV))
          (bfr-hyp-eval hyp env))
        (equal (bfr-hyp-eval new-hyp env)
          (or (bfr-eval x env)
            (hide (bfr-hyp-eval new-hyp env))))))
    :hints (("goal" :expand ((:free (x) (hide x)))))))

(define bfr-unassume$c
  (hyp$c undo-info)
  (b* ((hyp$c (maybe-bfr-hyp-init$c hyp$c)))
    (bfr-case :bdd (update-hyp-calist undo-info hyp$c)
      :aig (b* ((hyp (hyp-calist hyp$c)) (new-hyp (constraint-alist-delete-keys undo-info hyp))
          (hyp$c (update-hyp-calist new-hyp hyp$c))
          (nkeys (len undo-info))
          (hyp$c (update-calist-len (+ nkeys (calist-len hyp$c))
              hyp$c))
          (hyp$c (update-calist-nkeys (max 0 (- (calist-nkeys hyp$c) nkeys))
              hyp$c)))
        (maybe-shrink-hyp$c hyp$c)))))

(define bfr-unassume$a
  (hyp$a undo-info)
  :guard (hyp$ap hyp$a)
  (b* ((hyp$a (bfr-hyp-fix hyp$a)))
    (bfr-case :bdd (hyppair nil undo-info)
      :aig (hyppair t
        (shrink-constraint-alist (constraint-alist-delete-keys undo-info
            (hyppair->hyp hyp$a))))))
  ///
  (def-hyp-congruence bfr-unassume$a
    :hints (("Goal" :in-theory (enable bfr-hyp-fix))))
  (local (defthm calist-remassocs-nil-of-true-list
      (implies (alistp x)
        (equal (calist-remassocs x nil) x))
      :hints (("Goal" :in-theory (enable calist-remassocs)))))
  (local (defthm alistp-of-calist-remassocs
      (implies (alistp x)
        (alistp (calist-remassocs x seen)))
      :hints (("Goal" :in-theory (enable calist-remassocs)))))
  (local (defthm alistp-of-shrink-constraint-alist
      (alistp (shrink-constraint-alist x))
      :hints (("Goal" :in-theory (enable shrink-constraint-alist)))))
  (defthm bfr-unassume-of-assume
    (b* (((mv ?contradictionp ?new-hyp ?undo-info) (bfr-assume$a x hyp)))
      (equal (bfr-unassume$a new-hyp undo-info)
        (bfr-hyp-fix hyp)))
    :hints (("Goal" :in-theory (enable bfr-assume$a
         bfr-constr-assume
         bfr-hyp-fix
         bfr-hyp-mode-fix)))))

(define hyp-calist-corrected$c
  (hyp$c)
  (bfr-case :bdd (if (hyp-bfr-mode hyp$c)
      t
      (hyp-calist hyp$c))
    :aig (if (hyp-bfr-mode hyp$c)
      (hyp-calist hyp$c)
      nil)))

(define hyp-fix$c
  (x hyp$c)
  (b* ((calist (hyp-calist-corrected$c hyp$c)))
    (bfr-case :bdd (if (not calist)
        (and x t)
        (let ((and (q-and x calist)))
          (if and
            (if (hqual and calist)
              t
              x)
            nil)))
      :aig (aig-under-constraint-alist x calist))))

(define bfr-constr-mode-fix
  (x h)
  (bfr-case :bdd (if (not h)
      (and x t)
      (let ((and (q-and x h)))
        (if and
          (if (hqual and h)
            t
            x)
          nil)))
    :aig (aig-under-constraint-alist x h))
  ///
  (defthm bfr-constr-mode-fix-correct
    (implies (bfr-hyp-mode-eval hyp env)
      (equal (bfr-eval (bfr-constr-mode-fix x hyp)
          env)
        (bfr-eval x env)))
    :hints (("Goal" :in-theory (enable bfr-hyp-mode-fix
         bfr-hyp-mode-eval
         bfr-eval)
       :expand ((eval-constraint-alist nil env))) (and stable-under-simplificationp
        '(:use ((:instance eval-bdd-of-q-and
             (x (bfr-hyp-mode-fix hyp))
             (y x)
             (values env)))
          :in-theory (e/d (bfr-hyp-mode-fix) (eval-bdd-of-q-and))))))
  (defthm bfr-depends-on-of-bfr-constr-mode-fix
    (implies (not (bfr-depends-on k x))
      (not (bfr-depends-on k
          (bfr-constr-mode-fix x hyp$a)))))
  (defthm pbfr-depends-on-of-bfr-constr-mode-fix
    (implies (not (pbfr-depends-on k p x))
      (not (pbfr-depends-on k
          p
          (bfr-constr-mode-fix x hyp$a)))))
  (defthm bfr-constr-mode-fix-idempotent
    (equal (bfr-constr-mode-fix (bfr-constr-mode-fix x hyp)
        hyp)
      (bfr-constr-mode-fix x hyp)))
  (defthm bfr-constr-mode-fix-of-t-and-nil
    (and (equal (bfr-constr-mode-fix t hyp) t)
      (equal (bfr-constr-mode-fix nil hyp) nil))))

(define bfr-constr-fix
  (x hyp$a)
  :guard (hyp$ap hyp$a)
  (b* ((h (hyppair->hyp (bfr-hyp-fix hyp$a))))
    (bfr-case :bdd (if (not h)
        (and x t)
        (let ((and (q-and x h)))
          (if and
            (if (hqual and h)
              t
              x)
            nil)))
      :aig (aig-under-constraint-alist x h)))
  ///
  (def-hyp-congruence bfr-constr-fix)
  (defthm bfr-constr-fix-correct
    (implies (bfr-hyp-eval hyp env)
      (equal (bfr-eval (bfr-constr-fix x hyp) env)
        (bfr-eval x env)))
    :hints (("Goal" :in-theory (enable bfr-hyp-fix bfr-hyp-eval bfr-eval)
       :expand ((eval-constraint-alist nil env))) (and stable-under-simplificationp
        '(:use ((:instance eval-bdd-of-q-and
             (x (hyppair->hyp (bfr-hyp-fix hyp)))
             (y x)
             (values env)))
          :in-theory (e/d (bfr-hyp-fix) (eval-bdd-of-q-and))))))
  (defthm bfr-depends-on-of-bfr-constr-fix
    (implies (not (bfr-depends-on k x))
      (not (bfr-depends-on k
          (bfr-constr-fix x hyp$a)))))
  (defthm pbfr-depends-on-of-bfr-constr-fix
    (implies (not (pbfr-depends-on k p x))
      (not (pbfr-depends-on k
          p
          (bfr-constr-fix x hyp$a)))))
  (defthm bfr-constr-fix-idempotent
    (equal (bfr-constr-fix (bfr-constr-fix x hyp)
        hyp)
      (bfr-constr-fix x hyp)))
  (defthm bfr-constr-fix-of-t-and-nil
    (and (equal (bfr-constr-fix t hyp) t)
      (equal (bfr-constr-fix nil hyp) nil))))

(define bfr-hyp->bfr$c
  (hyp$c)
  (b* ((h (hyp-calist-corrected$c hyp$c)))
    (bfr-case :bdd h
      :aig (constraint-alist->aig h))))

(define bfr-constr-mode->bfr
  (h)
  (bfr-case :bdd h
    :aig (constraint-alist->aig h))
  ///
  (defthm bfr-eval-of-bfr-constr-mode->bfr
    (equal (bfr-eval (bfr-constr-mode->bfr hyp) env)
      (bfr-hyp-mode-eval hyp env))
    :hints ((and stable-under-simplificationp
       '(:in-theory (enable bfr-eval
           bfr-hyp-mode-eval
           bfr-hyp-mode-fix))))))

(define bfr-constr->bfr
  (hyp$a)
  :guard (hyp$ap hyp$a)
  (b* ((h (hyppair->hyp (bfr-hyp-fix hyp$a))))
    (bfr-case :bdd h
      :aig (constraint-alist->aig h)))
  ///
  (def-hyp-congruence bfr-constr->bfr)
  (defthm bfr-eval-of-bfr-constr->bfr
    (equal (bfr-eval (bfr-constr->bfr hyp) env)
      (bfr-hyp-eval hyp env))
    :hints ((and stable-under-simplificationp
       '(:in-theory (enable bfr-eval bfr-hyp-eval bfr-hyp-fix))))))

(define bfr-constr-mode-depends-on
  (k p h)
  :verify-guards nil
  (bfr-case :bdd (pbfr-depends-on k p h)
    :aig (constr-alist-depends-on k h))
  ///
  (defthm bfr-constr-mode-depends-on-correct
    (implies (and (not (bfr-constr-mode-depends-on k p x))
        (bfr-eval p env)
        (bfr-eval p (bfr-set-var k v env)))
      (equal (bfr-hyp-mode-eval x
          (bfr-param-env p
            (bfr-set-var k v env)))
        (bfr-hyp-mode-eval x
          (bfr-param-env p env))))
    :hints (("Goal" :in-theory (enable bfr-hyp-mode-eval bfr-hyp-mode-fix)) (and stable-under-simplificationp
        '(:in-theory (e/d (bfr-eval bfr-set-var
              bfr-param-env
              bfr-varname-fix
              bfr-hyp-mode-fix)
            (nfix))))))
  (defthm bfr-constr-mode-depends-on-of-bfr-constr-assume
    (implies (and (not (bfr-constr-mode-depends-on k p x))
        (not (pbfr-depends-on k p a)))
      (not (bfr-constr-mode-depends-on k
          p
          (mv-nth 1 (bfr-constr-assume a x)))))
    :hints (("Goal" :in-theory (enable bfr-constr-assume
         bfr-hyp-mode-fix
         bfr-constr-assume)) (and stable-under-simplificationp
        '(:in-theory (enable pbfr-depends-on
            bfr-depends-on
            bfr-from-param-space
            bfr-varname-fix)))))
  (defthm pbfr-depends-on-of-bfr-constr-mode->bfr
    (implies (not (bfr-constr-mode-depends-on k p x))
      (not (pbfr-depends-on k
          p
          (bfr-constr-mode->bfr x))))
    :hints (("Goal" :in-theory (enable bfr-constr-mode->bfr)) (and stable-under-simplificationp
        '(:in-theory (e/d (pbfr-depends-on bfr-depends-on
              bfr-from-param-space
              bfr-varname-fix)
            (nfix))))))
  (defthm bfr-constr-mode-depends-on-of-bfr-hyp-mode-fix
    (equal (bfr-constr-mode-depends-on k
        p
        (bfr-hyp-mode-fix x))
      (bfr-constr-mode-depends-on k p x))
    :hints (("Goal" :in-theory (enable bfr-hyp-mode-fix)))))

(define bfr-constr-depends-on
  (k p (hyp$a hyp$ap))
  :verify-guards nil
  (b* ((h (hyppair->hyp (bfr-hyp-fix hyp$a))))
    (bfr-case :bdd (pbfr-depends-on k p h)
      :aig (constr-alist-depends-on k h)))
  ///
  (def-hyp-congruence bfr-constr-depends-on)
  (defthm bfr-constr-depends-on-correct
    (implies (and (not (bfr-constr-depends-on k p x))
        (bfr-eval p env)
        (bfr-eval p (bfr-set-var k v env)))
      (equal (bfr-hyp-eval x
          (bfr-param-env p
            (bfr-set-var k v env)))
        (bfr-hyp-eval x (bfr-param-env p env))))
    :hints (("Goal" :in-theory (enable bfr-hyp-eval bfr-hyp-fix)) (and stable-under-simplificationp
        '(:in-theory (e/d (bfr-eval bfr-set-var
              bfr-param-env
              bfr-varname-fix
              bfr-hyp-fix)
            (nfix))))))
  (defthm bfr-constr-depends-on-of-bfr-constr-assume
    (implies (and (not (bfr-constr-depends-on k p x))
        (not (pbfr-depends-on k p a)))
      (not (bfr-constr-depends-on k
          p
          (mv-nth 1 (bfr-assume$a a x)))))
    :hints (("Goal" :in-theory (enable bfr-assume$a
         bfr-hyp-fix
         bfr-hyp-mode-fix
         bfr-constr-assume)) (and stable-under-simplificationp
        '(:in-theory (enable pbfr-depends-on
            bfr-depends-on
            bfr-from-param-space
            bfr-varname-fix)))))
  (defthm pbfr-depends-on-of-bfr-constr->bfr
    (implies (not (bfr-constr-depends-on k p x))
      (not (pbfr-depends-on k
          p
          (bfr-constr->bfr x))))
    :hints (("Goal" :in-theory (enable bfr-constr->bfr)) (and stable-under-simplificationp
        '(:in-theory (e/d (pbfr-depends-on bfr-depends-on
              bfr-from-param-space
              bfr-varname-fix)
            (nfix)))))))

(define hyp-norm$a
  ((hyp$a hyp$ap))
  :enabled t
  (bfr-hyp-fix hyp$a))

(define create-hyp$a
  nil
  :enabled t
  (hyppair nil nil))

(defun-nx hyp-corr
  (hyp$c hyp$a)
  (and (iff (hyp-bfr-mode hyp$c)
      (hyppair->bfr-mode hyp$a))
    (if (hyp-bfr-mode hyp$c)
      (equal (shrink-constraint-alist (hyp-calist hyp$c))
        (hyppair->hyp hyp$a))
      (equal (hyp-calist hyp$c)
        (hyppair->hyp hyp$a)))))

(encapsulate nil
  (local (in-theory (e/d (bfr-hyp-mode-fix bfr-hyp-init$c
          bfr-assume$c
          bfr-assume$a
          bfr-binary-and
          bfr-constr-assume
          bfr-unassume$c
          bfr-unassume$a
          hyp$ap
          hyp-fix$c
          bfr-hyp-init$a
          bfr-constr-fix
          bfr-hyp->bfr$c
          bfr-constr->bfr
          bfr-hyp-fix
          maybe-bfr-hyp-init$c
          maybe-shrink-hyp$c
          hyp-calist-corrected$c)
        ((bfr-hyp-mode-fix) nth update-nth))))
  (defabsstobj-events hyp
    :foundation hyp$c
    :recognizer (hyp-p :logic hyp$ap :exec hyp$cp)
    :creator (create-hyp :logic create-hyp$a
      :exec create-hyp$c)
    :corr-fn hyp-corr
    :corr-fn-exists t
    :exports ((bfr-hyp-init :logic bfr-hyp-init$a
       :exec bfr-hyp-init$c
       :protect t) (bfr-assume :logic bfr-assume$a
        :exec bfr-assume$c
        :protect t)
      (bfr-unassume :logic bfr-unassume$a
        :exec bfr-unassume$c
        :protect t)
      (hyp-fix :logic bfr-constr-fix :exec hyp-fix$c)
      (hyp-norm :logic hyp-norm$a
        :exec maybe-bfr-hyp-init$c
        :protect t)
      (bfr-hyp->bfr :logic bfr-constr->bfr
        :exec bfr-hyp->bfr$c))))

(defmacro lbfr-hyp-fix
  (hyp)
  `(hyp-norm ,GL::HYP))

(define hyp-fixedp
  (x hyp)
  (hqual (hyp-fix x hyp) x)
  ///
  (defthm hyp-fixedp-of-hyp-fix
    (hyp-fixedp (bfr-constr-fix x hyp) hyp)
    :hints (("Goal" :in-theory (enable hyp-fix))))
  (defthm hyp-fix-of-hyp-fixedp
    (implies (hyp-fixedp x hyp)
      (equal (bfr-constr-fix x hyp) x))))

(define true-under-hyp
  (x hyp)
  (declare (ignorable hyp))
  (eq x t)
  ///
  (def-hyp-congruence true-under-hyp)
  (defthmd true-under-hyp-point
    (implies (and (true-under-hyp x hyp)
        (hyp-fixedp x hyp)
        (bfr-hyp-eval hyp v))
      (bfr-eval x v))))

(define false-under-hyp
  (x hyp)
  (declare (ignorable hyp))
  (eq x nil)
  ///
  (def-hyp-congruence false-under-hyp)
  (defthmd false-under-hyp-point
    (implies (and (false-under-hyp x hyp)
        (hyp-fixedp x hyp)
        (bfr-hyp-eval hyp v))
      (not (bfr-eval x v)))))

(defmacro hf (x) `(hyp-fix ,GL::X hyp))

(defmacro th
  (x)
  `(true-under-hyp ,GL::X hyp))

(defmacro fh
  (x)
  `(false-under-hyp ,GL::X hyp))

(add-untranslate-pattern (true-under-hyp ?x hyp)
  (th ?x))

(add-untranslate-pattern (false-under-hyp ?x hyp)
  (fh ?x))

(add-untranslate-pattern (hyp-fix ?x hyp)
  (hf ?x))

(defstobj-clone pathcond hyp :suffix "-PATHCOND")

(add-bfr-fn-pat bfr-constr-fix)