		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svex-varmasks/env->aig-env-rec-log

Signature
(svex-varmasks/env->aig-env-rec-log count vars masks boolmasks env nextvar acc) → (mv err new-acc new-nextvar rem-vars)
Arguments: count — Guard (natp count).; 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 -- symbolic.
Guard (svex-env-p env).; nextvar — Guard (natp nextvar).; acc — aig environment accumulator.
Returns: rem-vars — Type (equal rem-vars (nthcdr count vars)).

Definitions and Theorems

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

(defun svex-varmasks/env->aig-env-rec-log
       (count vars masks boolmasks env nextvar acc)
  (declare (xargs :guard (and (natp count)
                              (svarlist-p vars)
                              (svex-mask-alist-p masks)
                              (svar-boolmasks-p boolmasks)
                              (svex-env-p env)
                              (natp nextvar))))
  (declare (xargs :guard (<= count (len vars))))
  (let ((__function__ 'svex-varmasks/env->aig-env-rec-log))
    (declare (ignorable __function__))
    (b* (((when (zp count))
          (mv nil acc (lnfix nextvar) vars))
         (mask (svex-mask-lookup (svex-var (car vars))
                                 masks))
         ((when (sparseint-< mask 0))
          (mv (msg "Negative mask: ~x0~%"
                   (svar-fix (car vars)))
              acc (lnfix nextvar)
              (nthcdr count vars)))
         (boolmask (svar-boolmasks-lookup (car vars)
                                          boolmasks))
         (4vec (svex-env-lookup (svar-fix (car vars))
                                env))
         (env-part (4vmask-to-a4vec-env mask boolmask 4vec nextvar))
         (nextvar (+ (lnfix nextvar)
                     (4vmask-to-a4vec-varcount mask boolmask)))
         (acc (append env-part acc))
         (count (1- count))
         (half-count (logcdr count))
         ((mv err acc nextvar vars)
          (svex-varmasks/env->aig-env-rec-log
               half-count (cdr vars)
               masks boolmasks env nextvar acc))
         ((when err)
          (mv err acc nextvar
              (nthcdr (- count half-count) vars))))
      (svex-varmasks/env->aig-env-rec-log
           (- count half-count)
           vars masks boolmasks env nextvar acc))))

Theorem: return-type-of-svex-varmasks/env->aig-env-rec-log.rem-vars

(defthm return-type-of-svex-varmasks/env->aig-env-rec-log.rem-vars
  (b* (((mv ?err ?new-acc ?new-nextvar ?rem-vars)
        (svex-varmasks/env->aig-env-rec-log
             count
             vars masks boolmasks env nextvar acc)))
    (equal rem-vars (nthcdr count vars)))
  :rule-classes :rewrite)

Theorem: svex-varmasks/env->aig-env-rec-log-in-terms-of-svex-varmasks/env->aig-env-rec

(defthm
 svex-varmasks/env->aig-env-rec-log-in-terms-of-svex-varmasks/env->aig-env-rec
 (b* (((mv ?err ?new-acc ?new-nextvar ?rem-vars)
       (svex-varmasks/env->aig-env-rec-log
            count
            vars masks boolmasks env nextvar acc)))
   (implies (<= (nfix count) (len vars))
            (b* (((mv spec-err spec-acc spec-nextvar)
                  (svex-varmasks/env->aig-env-rec
                       (take count vars)
                       masks boolmasks env nextvar acc)))
              (and (equal err spec-err)
                   (equal new-acc spec-acc)
                   (equal new-nextvar spec-nextvar))))))

Theorem: svex-varmasks/env->aig-env-rec-in-terms-of-rec-log

(defthm svex-varmasks/env->aig-env-rec-in-terms-of-rec-log
  (equal (svex-varmasks/env->aig-env-rec
              vars masks boolmasks env nextvar acc)
         (b* (((mv err acc nextvar ?rest)
               (svex-varmasks/env->aig-env-rec-log
                    (len vars)
                    vars masks boolmasks env nextvar acc)))
           (mv err acc nextvar))))