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

Safe Haskell | None
Language | Haskell2010

What4.Protocol.SMTLib2.Response

Description

This module defines types and operations for parsing SMTLib2 solver responses.

These are high-level responses, as describe in `https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf`, page 47, Figure 3.9.

This parser is designed to be the top level handling for solver responses, and to be used in conjuction with What4.Protocol.SMTLib2.Parse and What4.Protocol.SExp with the latter handling detailed parsing of specific constructs returned in the body of the general response.

Synopsis

- data SMTResponse
  - = AckSuccess
  - | AckUnsupported
  - | AckError Text
  - | AckSat
  - | AckUnsat
  - | AckUnknown
  - | AckInfeasible
  - | AckFail
  - | RspName Text
  - | RspVersion Text
  - | RspErrBehavior Text
  - | RspOutOfMemory
  - | RspRsnIncomplete
  - | RspUnkReason SExp
  - | AckSuccessSExp SExp
  - | AckSkipped Text SMTResponse
- data SMTLib2Exception
  - = SMTLib2Unsupported Command
  - | SMTLib2Error Command Text
  - | SMTLib2ParseError SMTLib2Intent [Command] Text
  - | SMTLib2ResponseUnrecognized Command Text
  - | SMTLib2InvalidResponse Command SMTLib2Intent SMTResponse
- getSolverResponse :: WriterConn t h -> IO (Either SomeException SMTResponse)
- getLimitedSolverResponse :: String -> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
- smtParseOptions :: [ConfigDesc]
- strictSMTParsing :: ConfigOption BaseBoolType
- strictSMTParseOpt :: ConfigDesc

# Documentation

data SMTResponse Source #

Constructors

AckSuccess |
AckUnsupported |
AckError Text |
AckSat |
AckUnsat |
AckUnknown |
AckInfeasible |
AckFail |
RspName Text |
RspVersion Text |
RspErrBehavior Text |
RspOutOfMemory |
RspRsnIncomplete |
RspUnkReason SExp |
AckSuccessSExp SExp |
AckSkipped Text SMTResponse |

#### Instances

Instances details

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

data SMTLib2Exception Source #

Constructors

SMTLib2Unsupported Command |
SMTLib2Error Command Text |
SMTLib2ParseError SMTLib2Intent [Command] Text |
SMTLib2ResponseUnrecognized Command Text |
SMTLib2InvalidResponse Command SMTLib2Intent SMTResponse |

#### Instances

Instances details

Exception SMTLib2Exception Source # |
Instance details Defined in What4.Protocol.SMTLib2.Response Methods toException :: SMTLib2Exception -> SomeException Source # fromException :: SomeException -> Maybe SMTLib2Exception Source # displayException :: SMTLib2Exception -> String Source # backtraceDesired :: SMTLib2Exception -> Bool Source #
Show SMTLib2Exception Source # |
Instance details Defined in What4.Protocol.SMTLib2.Response Methods showsPrec :: Int -> SMTLib2Exception -> ShowS Source # show :: SMTLib2Exception -> String Source # showList :: [SMTLib2Exception] -> ShowS Source #

getSolverResponse :: WriterConn t h -> IO (Either SomeException SMTResponse) Source #

Called to get a response from the SMT connection.

getLimitedSolverResponse :: String -> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a Source #

Gets a limited set of responses, throwing an exception when a response is not matched by the filter. Also throws exceptions for standard error results. The passed command and intent arguments are only used for marking error messages.

Callers which do not want exceptions thrown for standard error conditions should feel free to use `getSolverResponse` and handle all response cases themselves.

smtParseOptions :: [ConfigDesc] Source #

strictSMTParsing :: ConfigOption BaseBoolType Source #

strictSMTParseOpt :: ConfigDesc Source #