		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svexlist/env-list-eval-gl

Equivalent of svexlist/env-list-eval intended to work well under GL symbolic execution.

Signature
(svexlist/env-list-eval-gl x envs symbolic-params) → *
Arguments: x — Svex expressions to evaluate.
Guard (svexlistlist-p x).; envs — Bindings of variables to 4vec values.
Guard (svex-envlist-p envs).; symbolic-params — Alist giving symbolic execution parameters; see below.
Guard (alistp symbolic-params).

This function is provably equivalent to svexlist/env-list-eval, but is tailored to perform well under symbolic execution. For symbolic execution, we assume that the inputs to this function other than envs are fully concrete, and that each envs are symbolic only in its values, not its keys or its shape.

It is analogous to svexlist-eval-gl, but the individual lists of svexes within x are each evaluated with the corresponding element of envs. Symbolic execution is set up so that the svexes are all rendered into AIGs in a batch with memoization between all the lists.

The symbolic-params input behaves as it does in svexlist-eval-gl. However, the :boolmasks and :vars entries must be applicable to all environments in the list. That is, for each entry in the boolmasks, the corresponding key must be bound in every entry in the envs to a symbolic 4vec value that is (syntactically) Boolean-valued in the masked bits. Similarly, the :vars entry, if given, is unioned with the variables bound in all environments.

Definitions and Theorems

Function: svexlist/env-list-eval-gl

(defun svexlist/env-list-eval-gl (x envs symbolic-params)
 (declare (xargs :guard (and (svexlistlist-p x)
                             (svex-envlist-p envs)
                             (alistp symbolic-params))))
 (let ((__function__ 'svexlist/env-list-eval-gl))
  (declare (ignorable __function__))
  (b*
   ((envs (take (len x) envs))
    (x (svexlistlist-fix x))
    (svexes (append-lists x))
    (svars (svexlist/env-list-vars-for-symbolic-eval
                svexes envs symbolic-params))
    (svexes (svexlist-x-out-unused-vars
                 svexes svars
                 (symbolic-params-x-out-cond symbolic-params)))
    (svexes (maybe-svexlist-rewrite-fixpoint
                 svexes
                 (cdr (assoc :simplify symbolic-params))))
    (boolmasks
     (make-fast-alist
      (hons-copy
         (ec-call (svar-boolmasks-fix
                       (cdr (assoc :boolmasks symbolic-params)))))))
    ((unless (svex-envlist-check-boolmasks boolmasks envs))
     (b*
      ((?ign
           (cw "ERROR: some bits assumed to be Boolean were not~%"))
       (?ign (gl::gl-error 'boolcheck-failed)))
      (gl::gl-hide (svexlist/env-list-eval x envs))))
    ((mv err a4vecs)
     (time$ (svexlist->a4vecs-for-varlist svexes svars boolmasks)
            :msg "; svex->aigs: ~st sec, ~sa bytes.~%"))
    ((when err)
     (b* ((?ign (cw "ERROR gathering AIG bits for variables: ~@0~%"
                    err))
          (?ign (gl::gl-error 'a4env-failed)))
       (gl::gl-hide (svexlist/env-list-eval x envs))))
    (a4veclist-list (extract-lists x a4vecs)))
   (a4veclist/svex-env-list-eval a4veclist-list
                                 envs svexes svars boolmasks))))

Theorem: svexlist/env-list-eval-gl-correct

(defthm svexlist/env-list-eval-gl-correct
  (equal (svexlist/env-list-eval-gl x envs symbolic-params)
         (svexlist/env-list-eval x envs)))

Theorem: svexlist/env-list-eval-for-symbolic-redef

(defthm svexlist/env-list-eval-for-symbolic-redef
  (equal (svexlist/env-list-eval x envs)
         (svexlist/env-list-eval-gl x envs nil)))

Theorem: svexlist/env-list-eval-gl-of-svexlistlist-fix-x

(defthm svexlist/env-list-eval-gl-of-svexlistlist-fix-x
  (equal (svexlist/env-list-eval-gl (svexlistlist-fix x)
                                    envs symbolic-params)
         (svexlist/env-list-eval-gl x envs symbolic-params)))

Theorem: svexlist/env-list-eval-gl-svexlistlist-equiv-congruence-on-x

(defthm svexlist/env-list-eval-gl-svexlistlist-equiv-congruence-on-x
 (implies
   (svexlistlist-equiv x x-equiv)
   (equal (svexlist/env-list-eval-gl x envs symbolic-params)
          (svexlist/env-list-eval-gl x-equiv envs symbolic-params)))
 :rule-classes :congruence)

Theorem: svexlist/env-list-eval-gl-of-svex-envlist-fix-envs

(defthm svexlist/env-list-eval-gl-of-svex-envlist-fix-envs
  (equal (svexlist/env-list-eval-gl x (svex-envlist-fix envs)
                                    symbolic-params)
         (svexlist/env-list-eval-gl x envs symbolic-params)))

Theorem: svexlist/env-list-eval-gl-svex-envlist-equiv-congruence-on-envs

(defthm
    svexlist/env-list-eval-gl-svex-envlist-equiv-congruence-on-envs
 (implies
   (svex-envlist-equiv envs envs-equiv)
   (equal (svexlist/env-list-eval-gl x envs symbolic-params)
          (svexlist/env-list-eval-gl x envs-equiv symbolic-params)))
 :rule-classes :congruence)