what4-1.6.3: Solver-agnostic symbolic values support for issuing queries

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 `[`a`-`z` `A`-`Z` '0`-`9' '_']` as long as the result is not an SMTLIB or Yices keyword.

Synopsis

- data SolverSymbol
- solverSymbolAsText :: SolverSymbol -> Text
- data SolverSymbolError
- emptySymbol :: SolverSymbol
- userSymbol :: String -> Either SolverSymbolError SolverSymbol
- systemSymbol :: String -> SolverSymbol
- safeSymbol :: String -> SolverSymbol
- ppSolverSymbolError :: SolverSymbolError -> String

# 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

Instances details

Show SolverSymbol Source # |
Instance details Defined in What4.Symbol Methods showsPrec :: Int -> SolverSymbol -> ShowS Source # show :: SolverSymbol -> String Source # showList :: [SolverSymbol] -> ShowS Source #
Eq SolverSymbol Source # |
Instance details Defined in What4.Symbol Methods (==) :: SolverSymbol -> SolverSymbol -> Bool Source # (/=) :: SolverSymbol -> SolverSymbol -> Bool Source #
Ord SolverSymbol Source # |

Instance details

Defined in What4.Symbol

Methods

compare :: SolverSymbol -> SolverSymbol -> Ordering Source #

(<) :: SolverSymbol -> SolverSymbol -> Bool Source #

(<=) :: SolverSymbol -> SolverSymbol -> Bool Source #

(>) :: SolverSymbol -> SolverSymbol -> Bool Source #

(>=) :: SolverSymbol -> SolverSymbol -> Bool Source #

max :: SolverSymbol -> SolverSymbol -> SolverSymbol Source #

min :: SolverSymbol -> SolverSymbol -> SolverSymbol Source #

Hashable SolverSymbol Source # |
Instance details Defined in What4.Symbol Methods hashWithSalt :: Int -> SolverSymbol -> Int Source # hash :: SolverSymbol -> Int Source #

solverSymbolAsText :: SolverSymbol -> Text Source #

data SolverSymbolError Source #

This describes why a given text value was not a valid solver symbol.

#### Instances

Instances details

Show SolverSymbolError Source # |
Instance details Defined in What4.Symbol Methods showsPrec :: Int -> SolverSymbolError -> ShowS Source # show :: SolverSymbolError -> String Source # showList :: [SolverSymbolError] -> ShowS Source #

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!".

ppSolverSymbolError :: SolverSymbolError -> String Source #