		Search-engine friendly clone of the ACL2 documentation.

Svex-stvs

Svtv-versus-stv

A note on naming conventions

Svex STVs are modeled after esim ACL2::symbolic-test-vectors, and since they are intended to be a nearly drop-in replacement, we had to mangle the names of existing esim STV-related functions somehow. We settled on the following scheme:

Basically all Esim STV-related functions/utilities have names in the ACL2 package and containing "STV". So for an Esim function acl2::some-stv-tool, we name our Svex analogue acl2::some-svtv-tool and import that symbol into the SVEX package. We also add an alias sv::some-stv-tool (not in the ACL2 package). To summarize, you can refer to the Svex version of this function by any of the following:

acl2::some-svtv-tool
sv::some-svtv-tool, really the same symbol as above
sv::some-stv-tool, a macro alias for the above.

The modified name "SVTV" doesn't really stand for anything aside from perhaps "Svex symbolic test vector." In svex-related documentation, we refer to STVs and SVTVs more or less interchangeably, unless we are explicitly referring to Esim STVs (in which case we won't say SVTV). We usually refer to functions using the SVTV versions of the name, since that will be the same in either package.

Maybe we shouldn't pollute the ACL2 package with the SVTV symbols, and instead just use STV symbols in the SVEX package. We don't have much of an excuse other than sometimes we're working in the ACL2 package and want to just type an extra V rather than an extra SV::.