Creates a symbolic bit-level representation for x, assuming that vars are the only vars relevant to x and that the bits of vars given in boolmasks are Boolean-valued.
(svexlist->a4vecs-for-varlist-with-subexprs x vars boolmasks) → (mv err x-a4vecs subexp-a4vecs)
Steps: First creates a symbolic environment mapping the variables
to a4vec structures, each bit of which is a free variable. (For bits
constrained to be Boolean by boolmasks, the same variable is shared for
upper/lower.) Then uses
Function:
(defun svexlist->a4vecs-for-varlist-with-subexprs (x vars boolmasks) (declare (xargs :guard (and (svexlist-p x) (svarlist-p vars) (svar-boolmasks-p boolmasks)))) (let ((__function__ 'svexlist->a4vecs-for-varlist-with-subexprs)) (declare (ignorable __function__)) (b* (((mv masks toposort) (svexlist-mask-alist/toposort-memo x)) ((mv err a4env) (svex-varmasks->a4env vars masks boolmasks)) ((when err) (mv err nil nil)) (a4env (make-fast-alist a4env)) ((mv x-res sub-res) (svexlists->a4vec-top x toposort a4env masks)) (?ign (fast-alist-free a4env))) (mv nil x-res sub-res))))
Theorem:
(defthm return-type-of-svexlist->a4vecs-for-varlist-with-subexprs.err (b* (((mv ?err ?x-a4vecs ?subexp-a4vecs) (svexlist->a4vecs-for-varlist-with-subexprs x vars boolmasks))) (iff err (not (svex-maskbits-ok vars (svexlist-mask-alist x))))) :rule-classes :rewrite)
Theorem:
(defthm a4veclist-p-of-svexlist->a4vecs-for-varlist-with-subexprs.x-a4vecs (b* (((mv ?err ?x-a4vecs ?subexp-a4vecs) (svexlist->a4vecs-for-varlist-with-subexprs x vars boolmasks))) (a4veclist-p x-a4vecs)) :rule-classes :rewrite)
Theorem:
(defthm a4veclist-p-of-svexlist->a4vecs-for-varlist-with-subexprs.subexp-a4vecs (b* (((mv ?err ?x-a4vecs ?subexp-a4vecs) (svexlist->a4vecs-for-varlist-with-subexprs x vars boolmasks))) (a4veclist-p subexp-a4vecs)) :rule-classes :rewrite)
Theorem:
(defthm svexlist->a4vecs-for-varlist-with-subexprs-equals-svexlist->a4vecs-for-varlist (b* (((mv ?err ?x-a4vecs ?subexp-a4vecs) (svexlist->a4vecs-for-varlist-with-subexprs x vars boolmasks))) (b* (((mv err-spec a4vec-spec) (svexlist->a4vecs-for-varlist x vars boolmasks))) (and (equal err err-spec) (equal x-a4vecs a4vec-spec)))))