		Search-engine friendly clone of the ACL2 documentation.

Expressions

Bit-blasting

We implement an efficient translation from svex expressions into ACL2::aigs, to support symbolic simulation with gl.

Subtopics

Svex-focused-equivalence-checking: Tools for equivalence checking the evaluations of two sets of svex expressions under different environments.
A4vec-operations: Symbolic versions of the SV functions that operate on a4vecs instead of 4vecs.
Svexlist-eval-gl: Equivalent of svexlist-eval intended to work well under GL symbolic execution.
Aig-symbolic-arithmetic: A more or less complete set of functions for doing arithmetic on a symbolic bitvector representation consisting of lists of AIGs.
Svex-varmasks/env->aig-env-rec
Svex-varmasks->a4env-rec
Svexlist/env-list-eval-gl: Equivalent of svexlist/env-list-eval intended to work well under GL symbolic execution.
4vmask-to-a4vec-rec-env
4vmask-to-a4vec-rec
Svexlist->a4vecs-for-varlist: 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.
Svex-varmasks/env->aig-env-stats-rec
Svexlist->a4vec-nrev
A4veclist/svex-env-list-eval
A4vec: A symbolic 4vec, with lists of AIGs for the upper and lower bits.
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-maskbits-ok
Svex-envlist-check-boolmasks
Svex-env-check-boolmasks
Nat-bool-list-upper-boundp
Nat-bool-a4vec-lower-boundp
Maybe-svexlist-rewrite-fixpoint
4vmask-to-a4vec-varcount
A4vec-eval: Semantics of a4vecs.
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: Evaluate a list of a4vecs.
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: An alist mapping svex-p to a4vec-p.
Svex-a4vec-env: An alist mapping svar-p to a4vec-p.
A4veclistlist: A list of a4veclist-p objects.
A4veclist: A list of a4vec-p objects.
Symbolic-params-x-out-cond