| Copyright | (c) Galois Inc 2015-2020 |
|---|---|
| License | BSD3 |
| Maintainer | jhendrix@galois.com |
| Safe Haskell | None |
| Language | Haskell2010 |
What4.Symbol
Description
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 [ as long as the
result is not an SMTLIB or Yices keyword.a-z A-Z '0-9' '_']
Synopsis
Documentation
data SolverSymbol Source #
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.
Instances
| Eq SolverSymbol Source # | |
Defined in What4.Symbol | |
| Ord SolverSymbol Source # | |
Defined in What4.Symbol Methods compare :: SolverSymbol -> SolverSymbol -> Ordering # (<) :: SolverSymbol -> SolverSymbol -> Bool # (<=) :: SolverSymbol -> SolverSymbol -> Bool # (>) :: SolverSymbol -> SolverSymbol -> Bool # (>=) :: SolverSymbol -> SolverSymbol -> Bool # max :: SolverSymbol -> SolverSymbol -> SolverSymbol # min :: SolverSymbol -> SolverSymbol -> SolverSymbol # | |
| Show SolverSymbol Source # | |
Defined in What4.Symbol Methods showsPrec :: Int -> SolverSymbol -> ShowS # show :: SolverSymbol -> String # showList :: [SolverSymbol] -> ShowS # | |
| Hashable SolverSymbol Source # | |
Defined in What4.Symbol | |
data SolverSymbolError Source #
This describes why a given text value was not a valid solver symbol.
Instances
| Show SolverSymbolError Source # | |
Defined in What4.Symbol Methods showsPrec :: Int -> SolverSymbolError -> ShowS # show :: SolverSymbolError -> String # showList :: [SolverSymbolError] -> ShowS # | |
emptySymbol :: SolverSymbol Source #
Return the empty symbol.
userSymbol :: String -> Either SolverSymbolError SolverSymbol Source #
This returns either a user symbol or the empty symbol if the string is empty.
systemSymbol :: String -> SolverSymbol Source #
safeSymbol :: String -> SolverSymbol Source #
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!".