		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svex-varmasks/env->aig-env

Signature
(svex-varmasks/env->aig-env vars masks boolmasks env) → (mv err env)
Arguments: vars — Guard (svarlist-p vars).; masks — Guard (svex-mask-alist-p masks).; boolmasks — Guard (svar-boolmasks-p boolmasks).; env — look up variables in env to get 4vecs to assign.
Guard (svex-env-p env).
Returns: err — some mask was negative.
Type (implies (svex-mask-alist-p masks) (iff err (not (svex-maskbits-ok vars masks)))) .; env — binds AIG vars to Boolean values.

Definitions and Theorems

Function: svex-varmasks/env->aig-env

(defun svex-varmasks/env->aig-env (vars masks boolmasks env)
 (declare (xargs :guard (and (svarlist-p vars)
                             (svex-mask-alist-p masks)
                             (svar-boolmasks-p boolmasks)
                             (svex-env-p env))))
 (let ((__function__ 'svex-varmasks/env->aig-env))
  (declare (ignorable __function__))
  (b*
   ((?stats (svex-varmasks/env->aig-env-stats vars masks boolmasks))
    ((mv err res &)
     (svex-varmasks/env->aig-env-rec
          vars masks boolmasks env 0 nil)))
   (mv err res))))

Theorem: return-type-of-svex-varmasks/env->aig-env.err

(defthm return-type-of-svex-varmasks/env->aig-env.err
  (b* (((mv ?err ?env)
        (svex-varmasks/env->aig-env vars masks boolmasks env)))
    (implies (svex-mask-alist-p masks)
             (iff err
                  (not (svex-maskbits-ok vars masks)))))
  :rule-classes :rewrite)

Theorem: eval-svex-varmasks->a4env-with-env

(defthm eval-svex-varmasks->a4env-with-env
 (b*
  (((mv err a4env)
    (svex-varmasks->a4env vars masks boolmasks1))
   ((mv ?err1 env)
    (svex-varmasks/env->aig-env vars
                                (svex-mask-alist-extract-vars masks)
                                boolmasks goalenv)))
  (implies (and (not err)
                (svex-mask-alist-p masks)
                (equal boolmasks
                       (svar-boolmasks-fix boolmasks1))
                (svex-env-boolmasks-ok goalenv boolmasks))
           (svex-envs-mask-equiv-on-vars
                vars
                masks (svex-a4vec-env-eval a4env env)
                goalenv))))

Theorem: svex-varmasks/env->aig-env-of-svarlist-fix-vars

(defthm svex-varmasks/env->aig-env-of-svarlist-fix-vars
  (equal (svex-varmasks/env->aig-env (svarlist-fix vars)
                                     masks boolmasks env)
         (svex-varmasks/env->aig-env vars masks boolmasks env)))

Theorem: svex-varmasks/env->aig-env-svarlist-equiv-congruence-on-vars

(defthm svex-varmasks/env->aig-env-svarlist-equiv-congruence-on-vars
 (implies
  (svarlist-equiv vars vars-equiv)
  (equal
       (svex-varmasks/env->aig-env vars masks boolmasks env)
       (svex-varmasks/env->aig-env vars-equiv masks boolmasks env)))
 :rule-classes :congruence)