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.
- bits — integerp
- An integer valued field used to record various bits of
information. Often used to rename a set of variables to
variables-prime, where we know the first set has certain bits
unset. Exact use varies over the phase of processing; e.g.,
this is used to record the nonblocking bit for VL statement
processing and used to record the override-test and
override-val bits for SVTV processing.
- props — svar-proplist
- An area to store any pieces of information that don't fit in
the bits. This can be any alist mapping symbols to arbitrary
values.
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->props
- Get the props field from a svar.
- Svar->delay
- Get the delay field from a svar.
- Svar->bits
- Get the bits field from a svar.
- Change-svar
- Modifying constructor for svar structures.
- 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.
