		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svexlist->a4vec-aig-env-for-varlist

Signature
(svexlist->a4vec-aig-env-for-varlist x vars boolmasks env) → (mv err aig-env)
Arguments: x — Guard (svexlist-p x).; vars — Guard (svarlist-p vars).; boolmasks — Guard (svar-boolmasks-p boolmasks).; env — Guard (svex-env-p env).
Returns: err — Type (iff err (not (svex-maskbits-ok vars (svexlist-mask-alist x)))).

Definitions and Theorems

Function: svexlist->a4vec-aig-env-for-varlist

(defun svexlist->a4vec-aig-env-for-varlist (x vars boolmasks env)
  (declare (xargs :guard (and (svexlist-p x)
                              (svarlist-p vars)
                              (svar-boolmasks-p boolmasks)
                              (svex-env-p env))))
  (let ((__function__ 'svexlist->a4vec-aig-env-for-varlist))
    (declare (ignorable __function__))
    (b* ((masks (svexlist-variable-mask-alist x)))
      (svex-varmasks/env->aig-env vars masks boolmasks env))))

Theorem: return-type-of-svexlist->a4vec-aig-env-for-varlist.err

(defthm return-type-of-svexlist->a4vec-aig-env-for-varlist.err
  (b* (((mv ?err ?aig-env)
        (svexlist->a4vec-aig-env-for-varlist x vars boolmasks env)))
    (iff err
         (not (svex-maskbits-ok vars (svexlist-mask-alist x)))))
  :rule-classes :rewrite)

Theorem: svexlist->a4vec-for-varlist-correct

(defthm svexlist->a4vec-for-varlist-correct
 (b* (((mv err a4vecs)
       (svexlist->a4vecs-for-varlist x vars boolmasks))
      ((mv ?err1 aig-env)
       (svexlist->a4vec-aig-env-for-varlist x vars boolmasks env)))
  (implies
   (and
       (not err)
       (svar-boolmasks-p boolmasks)
       (svex-env-boolmasks-ok env boolmasks)
       (subsetp (intersection-equal (svexlist-vars x)
                                    (alist-keys (svex-env-fix env)))
                (svarlist-fix vars)))
   (equal (a4veclist-eval a4vecs aig-env)
          (svexlist-eval x env)))))

Theorem: svexlist->a4vec-aig-env-for-varlist-of-svexlist-fix-x

(defthm svexlist->a4vec-aig-env-for-varlist-of-svexlist-fix-x
 (equal (svexlist->a4vec-aig-env-for-varlist (svexlist-fix x)
                                             vars boolmasks env)
        (svexlist->a4vec-aig-env-for-varlist x vars boolmasks env)))

Theorem: svexlist->a4vec-aig-env-for-varlist-svexlist-equiv-congruence-on-x

(defthm
 svexlist->a4vec-aig-env-for-varlist-svexlist-equiv-congruence-on-x
 (implies
   (svexlist-equiv x x-equiv)
   (equal (svexlist->a4vec-aig-env-for-varlist x vars boolmasks env)
          (svexlist->a4vec-aig-env-for-varlist
               x-equiv vars boolmasks env)))
 :rule-classes :congruence)

Theorem: svexlist->a4vec-aig-env-for-varlist-of-svarlist-fix-vars

(defthm svexlist->a4vec-aig-env-for-varlist-of-svarlist-fix-vars
 (equal (svexlist->a4vec-aig-env-for-varlist x (svarlist-fix vars)
                                             boolmasks env)
        (svexlist->a4vec-aig-env-for-varlist x vars boolmasks env)))

Theorem: svexlist->a4vec-aig-env-for-varlist-svarlist-equiv-congruence-on-vars

(defthm
 svexlist->a4vec-aig-env-for-varlist-svarlist-equiv-congruence-on-vars
 (implies
   (svarlist-equiv vars vars-equiv)
   (equal (svexlist->a4vec-aig-env-for-varlist x vars boolmasks env)
          (svexlist->a4vec-aig-env-for-varlist
               x vars-equiv boolmasks env)))
 :rule-classes :congruence)