Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Gl
Esim
Vl2014
Sv
Svex-stvs
Svex-decomposition-methodology
Sv-versus-esim
Svex-decomp
Svex-compose-dfs
Svex-compilation
Moddb
Svmods
Svstmt
Sv-tutorial
Expressions
Rewriting
Svex
Bit-blasting
A4vec-operations
Svexlist-eval-gl
Aig-symbolic-arithmetic
Svex-varmasks/env->aig-env-rec
Svex-varmasks->a4env-rec
Svexlist/env-list-eval-gl
4vmask-to-a4vec-rec-env
4vmask-to-a4vec-rec
Svexlist->a4vecs-for-varlist
Svex-varmasks/env->aig-env-stats-rec
Svexlist->a4vec-nrev
A4veclist/svex-env-list-eval
A4vec
Svexlist-x-out-unused-vars
Svex->a4vec-memotable-correctp
A4vec/svex-env-eval
Svex-varmasks->a4env
Svex-varmasks/env->aig-env-rec-log
4vmask-to-a4vec-env
4veclist-from-bitlist-log-rec
Svex-apply-aig
Svexlist-vars-for-symbolic-eval
Nat-bool-a4env-upper-boundp
4vmask-to-a4vec
Svexlist/env-list-vars-for-symbolic-eval
Svex-maskbits-for-vars
Svexlist->a4vec-aig-env-for-varlist
4vec-from-bitlist
Svexlist-full-masks-p
Svex-varmasks/env->aig-env-stats
Svex-varmasks/env->aig-env
Svexlistlist->a4vec
Svex-const-concat-args
Svex-mask-alist-extract-vars
Svexlist->a4vec-top
Nat-bool-a4vec-upper-boundp
Nat-bool-a4env-lower-boundp
Maybe-a3vec-fix
Svex-envlist-check-boolmasks
Svex-env-check-boolmasks
Nat-bool-list-upper-boundp
Nat-bool-a4vec-lower-boundp
Svex-maskbits-ok
Maybe-svexlist-rewrite-fixpoint
4vmask-to-a4vec-varcount
A4vec-eval
Svexlist-nth
A4veclist-nth
Nat-bool-list-lower-boundp
4veclist-from-bitlist
V2i-first-n
A4veclist-eval-gl
Svex-envlist-keyset
Svex-a4vec-env-eval
A4veclist/env-list-eval
Svexlist-variable-mask-alist
Sparseint-nfix
A4veclist-length
A4veclist-eval
4vec-boolmaskp
Nat-bool-list-nats
Nat-bool-a4env-p
Nat-bool-listp
A4veclist->aiglist
Svexlist-rewrite-fixpoint-memo
Nat-bool-a4vec-p
A4vec->aiglist
Svex-is-const-concat
Nat-bool-a4env-vars
Svexlist-mask-alist-memo
Nat-bool-a4vec-vars
Svexlist-vars-memo
A4vec-constantp
Svex-aig-memotable
Svex-a4vec-env
Svex-a4vec-env-p
Svex-a4vec-env-fix
Svex-a4vec-env-equiv
A4veclistlist
A4veclist
Symbolic-params-x-out-cond
Functions
4vmask
Why-infinite-width
Svex-vars
Evaluation
Values
Symbolic-test-vector
Vl-to-svex
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Bit-blasting
Svex-a4vec-env
An alist mapping
svar-p
to
a4vec-p
.
This is an ordinary
defalist
.
Subtopics
Svex-a4vec-env-p
Recognizer for
svex-a4vec-env
.
Svex-a4vec-env-fix
(svex-a4vec-env-fix x)
is an
fty
alist fixing function that follows the fix-keys strategy.
Svex-a4vec-env-equiv
Basic equivalence relation for
svex-a4vec-env
structures.