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

Copyright(c) Galois Inc 2015-2020
Safe HaskellNone



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.



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.

data SolverSymbolError Source #

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

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.

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