		Search-engine friendly clone of the ACL2 documentation.

Expressions

Evaluation

The formal semantics of our expressions are defined by svex-eval, a simple McCarthy-style evaluator for interpreting an svex under an environment that gives values to its variables.

Subtopics

Svex-xeval: Cheaply detect always-constant bits in an svex by approximately evaluating it under the empty (i.e., all X) environment.
Svex-mono-eval: Evaluate an X-monotonic approximation of an svex
Svex-eval: Evaluate an svex in some environment.
Svex-apply: Apply an svex function to some 4vec arguments.
Svex-env: An alist mapping svars to 4vecs. Often used as an environment that gives variables their values in svex-eval.
Svex-alist-eval: Evaluate every expression in an svex-alist under the same environment.
Svar-boolmasks-lookup
Svex-s4eval: Evaluate an svex in some s4vec environment.
Svexlist-unquote
Svex-alist-eval-for-symbolic
Svexlist-eval: Evaluate each svex in a list under the same environment.
Svexlist-quotesp
Svar-boolmasks: An alist mapping svar-p to integerp.
Svexlist-s4eval: Evaluate each svex in a list under the same environment.
Svexlist-eval-for-symbolic