Safe Haskell	None
Language	Haskell2010

What4.Protocol.SMTLib2.Parse

Contents

CheckSatResponse
GetModelResonse
- 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.

GetModelResonse

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

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

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)`.