		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

A4vec/svex-env-eval

Signature
(a4vec/svex-env-eval x env svexes svars boolmasks) → 4vecs
Arguments: x — Guard (a4veclist-p x).; env — Guard (svex-env-p env).; svexes — Guard (svexlist-p svexes).; svars — Guard (svarlist-p svars).; boolmasks — Guard (svar-boolmasks-p boolmasks).
Returns: 4vecs — Type (4veclist-p 4vecs).

Definitions and Theorems

Function: a4vec/svex-env-eval

(defun a4vec/svex-env-eval (x env svexes svars boolmasks)
 (declare (xargs :guard (and (a4veclist-p x)
                             (svex-env-p env)
                             (svexlist-p svexes)
                             (svarlist-p svars)
                             (svar-boolmasks-p boolmasks))))
 (declare
  (xargs
      :guard (svex-maskbits-ok svars (svexlist-mask-alist svexes))))
 (let ((__function__ 'a4vec/svex-env-eval))
   (declare (ignorable __function__))
   (b* ((env (make-fast-alist env))
        ((mv ?err aig-env)
         (svexlist->a4vec-aig-env-for-varlist
              svexes svars boolmasks env))
        (?ign (fast-alist-free env))
        (aig-env (make-fast-alist aig-env))
        (ans (a4veclist-eval x aig-env)))
     (fast-alist-free aig-env)
     ans)))

Theorem: 4veclist-p-of-a4vec/svex-env-eval

(defthm 4veclist-p-of-a4vec/svex-env-eval
  (b* ((4vecs (a4vec/svex-env-eval x env svexes svars boolmasks)))
    (4veclist-p 4vecs))
  :rule-classes :rewrite)

Theorem: svexlist-full-masks-p-when-subset

(defthm svexlist-full-masks-p-when-subset
  (implies (and (subsetp-equal some-svexes svexes)
                (svexlist-full-masks-p svexes masks))
           (svexlist-full-masks-p some-svexes masks)))

Theorem: a4vec/svex-env-eval-correct

(defthm a4vec/svex-env-eval-correct
 (b* ((masks (svexlist-mask-alist svexes))
      ((mv ?err a4env)
       (svex-varmasks->a4env svars masks boolmasks1))
      (x (svexlist->a4vec some-svexes a4env masks))
      (?4vecs (a4vec/svex-env-eval x env svexes svars boolmasks)))
  (implies
   (and
       (svex-maskbits-ok svars masks)
       (subsetp some-svexes svexes)
       (equal boolmasks
              (svar-boolmasks-fix boolmasks1))
       (svex-env-boolmasks-ok env boolmasks)
       (subsetp (intersection-equal (svexlist-vars some-svexes)
                                    (alist-keys (svex-env-fix env)))
                (svarlist-fix svars)))
   (equal 4vecs
          (svexlist-eval some-svexes env)))))

Theorem: a4vec/svex-env-eval-of-a4veclist-fix-x

(defthm a4vec/svex-env-eval-of-a4veclist-fix-x
  (equal (a4vec/svex-env-eval (a4veclist-fix x)
                              env svexes svars boolmasks)
         (a4vec/svex-env-eval x env svexes svars boolmasks)))

Theorem: a4vec/svex-env-eval-a4veclist-equiv-congruence-on-x

(defthm a4vec/svex-env-eval-a4veclist-equiv-congruence-on-x
 (implies
   (a4veclist-equiv x x-equiv)
   (equal (a4vec/svex-env-eval x env svexes svars boolmasks)
          (a4vec/svex-env-eval x-equiv env svexes svars boolmasks)))
 :rule-classes :congruence)

Theorem: a4vec/svex-env-eval-of-svexlist-fix-svexes

(defthm a4vec/svex-env-eval-of-svexlist-fix-svexes
  (equal (a4vec/svex-env-eval x env (svexlist-fix svexes)
                              svars boolmasks)
         (a4vec/svex-env-eval x env svexes svars boolmasks)))

Theorem: a4vec/svex-env-eval-svexlist-equiv-congruence-on-svexes

(defthm a4vec/svex-env-eval-svexlist-equiv-congruence-on-svexes
 (implies
   (svexlist-equiv svexes svexes-equiv)
   (equal (a4vec/svex-env-eval x env svexes svars boolmasks)
          (a4vec/svex-env-eval x env svexes-equiv svars boolmasks)))
 :rule-classes :congruence)

Theorem: a4vec/svex-env-eval-of-svarlist-fix-svars

(defthm a4vec/svex-env-eval-of-svarlist-fix-svars
  (equal (a4vec/svex-env-eval x env svexes (svarlist-fix svars)
                              boolmasks)
         (a4vec/svex-env-eval x env svexes svars boolmasks)))

Theorem: a4vec/svex-env-eval-svarlist-equiv-congruence-on-svars

(defthm a4vec/svex-env-eval-svarlist-equiv-congruence-on-svars
 (implies
   (svarlist-equiv svars svars-equiv)
   (equal (a4vec/svex-env-eval x env svexes svars boolmasks)
          (a4vec/svex-env-eval x env svexes svars-equiv boolmasks)))
 :rule-classes :congruence)