Svar
A single variable in a symbolic vector expression.
This is a product type, introduced by defflexsum in support of svar.
Fields
- name
- The name of this variable. This can be any ACL2 object at all,
but our representation is optimized for stringp or symbolp names.
- delay — natp
- A natural valued index for this variable, used for instance
to support the encoding of, e.g., previous versus current
register values in FSMs. The default delay (which enjoys an
optimized representation) is 0. See below for some motivation
and explanation.
- nonblocking — booleanp
- A flag used in statement processing to indicate a reference
to a variable after nonblocking assignments have been done.
Not used in other contexts.
- override-test — booleanp
- override-val — booleanp
Each variable in an svex represents a 4vec.
In most s-expression formats, e.g., s-expressions in Lisp or in the ACL2::4v-sexprs used in esim, a variable is just a symbol, which
is generally treated as if it were an atomic name with no further
structure.
In contrast, in sv, our variables have both a name and also a natural
numbered index (called delay). This index is mainly an implementation
detail that allows us to cheaply (i.e., without intern$) construct new
variables.
In the semantics of expressions, e.g., in svex-lookup, variables are
distinct whenever they differ by name or by delay. That is, as far as
expression evaluation is concerned, the variable named "v" with delay 5 is
completely distinct from "v" with delay 4. Think of them as you would
indexed variables like v_5 versus v_4 in some mathematics.
Subtopics
- Svar-p
- Recognizer for svar structures.
- Svar-fix
- Fixing function for svar structures.
- Make-svar
- Basic constructor macro for svar structures.
- Svar-equiv
- Basic equivalence relation for svar structures.
- Svar->override-val
- Get the override-val field from a svar.
- Svar->override-test
- Get the override-test field from a svar.
- Svar->nonblocking
- Get the nonblocking field from a svar.
- Change-svar
- Modifying constructor for svar structures.
- Svar->delay
- Get the delay field from a svar.
- Svarlist
- A list of svar-p objects.
- Svar->name
- Get the name field from a svar.
- Svar-map
- An alist mapping svar-p to svar-p.
- Svar-alist
- An alist mapping svar-p to anything.
