Symbol package:what4
This defines a datatype for representing identifiers that can be used
with Crucible. These must start with an ASCII letter and can consist
of any characters in the set
[a-z
A-Z '0-9' '_'] as long as the result is
not an SMTLIB or Yices keyword.
This describes what a given SolverSymbol is associated with. Parameter
t is a phantom type brand used to track nonces.
A bijective map between vars and their canonical name for printing
purposes. Parameter t is a phantom type brand used to track
nonces.
Get current variable bindings.
This class is provides functions needed to implement the symbolic
array intrinsic functions
This represents a name known to the solver.
We have three types of symbols:
- The empty symbol
- A user symbol
- A system symbol
A user symbol should consist of a letter followed by any combination
of letters, digits, and underscore characters. It also cannot be a
reserved word in Yices or SMTLIB.
A system symbol should start with a letter followed by any number of
letter, digit, underscore or an exclamation mark characters. It must
contain at least one exclamation mark to distinguish itself from user
symbols.
Attempts to create a user symbol from the given string. If this fails
for some reason, the string is Z-encoded into a system symbol instead
with the prefix "zenc!".
This returns either a user symbol or the empty symbol if the string is
empty.
Indicates whether the problem uses symbolic arrays.
This describes why a given text value was not a valid solver symbol.
A symbolic
SymBV, including its lower and upper bounds as a
Domain.