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

Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.Protocol.SMTLib2.Parse

Contents

- CheckSatResponse
- GetModelResponse
  - Sorts
  - Terms

Description

This module defines types and operations for parsing results from SMTLIB2.

It does not depend on the rest of What4 so that it can be used directly by clients interested in generating SMTLIB without depending on the What4 formula interface. All the type constructors are exposed so that clients can generate new values that are not exposed through this interface.

Synopsis

- data CheckSatResponse
  - = SatResponse
  - | UnsatResponse
  - | UnknownResponse
  - | CheckSatUnsupported
  - | CheckSatError !String
- readCheckSatResponse :: Handle -> IO CheckSatResponse
- type GetModelResponse = [ModelResponse]
- readGetModelResponse :: Handle -> IO GetModelResponse
- data ModelResponse
  - = DeclareSortResponse !Symbol !Integer
  - | DefineFunResponse !DefineFun
- data DefineFun = DefineFun {
  - funSymbol :: !Symbol
  - funArgs :: ![(Symbol, Sort)]
  - funResultSort :: !Sort
  - funDef :: !Term
  }
- data Symbol
- data Sort
  - = Sort Symbol [Sort]
  - | BitVec !Integer
  - | FloatingPoint !Integer !Integer
- pattern Bool :: Sort
- pattern Int :: Sort
- pattern Real :: Sort
- pattern RoundingMode :: Sort
- pattern Array :: Sort -> Sort -> Sort
- data Term
  - = SymbolTerm !Symbol
  - | AsConst !Sort !Term
  - | BVTerm !Integer !Integer
  - | IntTerm !Integer
  - | RatTerm !Rational
  - | StoreTerm !Term !Term !Term
  - | IfEqTerm !Symbol !Term !Term !Term

# CheckSatResponse

data CheckSatResponse Source #

Result of check-sat and check-sat-assuming

Constructors

SatResponse |
UnsatResponse |
UnknownResponse |
CheckSatUnsupported |
CheckSatError !String |

readCheckSatResponse :: Handle -> IO CheckSatResponse Source #

Read the results of a `(check-sat)` request.

# GetModelResponse

type GetModelResponse = [ModelResponse] Source #

The parsed declarations and definitions returned by "(get-model)"

readGetModelResponse :: Handle -> IO GetModelResponse Source #

This reads the model response from a "(get-model)" request.

data ModelResponse Source #

A line in the model response

Constructors

DeclareSortResponse !Symbol !Integer |
DefineFunResponse !DefineFun |

data DefineFun Source #

Constructors

DefineFun |

Fields

- funSymbol :: !Symbol
- funArgs :: ![(Symbol, Sort)]
- funResultSort :: !Sort
- funDef :: !Term

data Symbol Source #

An SMT symbol

#### Instances

Instances details

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

## Sorts

data Sort Source #

An SMT sort.

Constructors

Sort Symbol [Sort] | A named sort with the given arguments.
BitVec !Integer | A bitvector with the given width.
FloatingPoint !Integer !Integer | floating point with exponent bits followed by significand bit.

pattern Bool :: Sort Source #

pattern Int :: Sort Source #

pattern Real :: Sort Source #

pattern RoundingMode :: Sort Source #

pattern Array :: Sort -> Sort -> Sort Source #

## Terms

data Term Source #

This denotes an SMTLIB term over a fixed vocabulary.

Constructors

SymbolTerm !Symbol |
AsConst !Sort !Term |
BVTerm !Integer !Integer |
IntTerm !Integer | `IntTerm v` denotes the SMTLIB expression `v` if `v >= 0` and @(- `(negate v)) otherwise.
RatTerm !Rational | `RatTerm r` denotes the SMTLIB expression `(/ `(numerator r) `(denomator r))`.
StoreTerm !Term !Term !Term | `StoreTerm a i v` denotes the SMTLIB expression `(store a i v)`.
IfEqTerm !Symbol !Term !Term !Term | `IfEqTerm v c t f` denotes the SMTLIB expression `(ite (= v c) t f)`.