| Safe Haskell | Safe-Inferred |
|---|---|
| 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
- 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
Instances
| Show SMTResponse Source # | |
Defined in What4.Protocol.SMTLib2.Response Methods showsPrec :: Int -> SMTResponse -> ShowS # show :: SMTResponse -> String # showList :: [SMTResponse] -> ShowS # | |
| Eq SMTResponse Source # | |
Defined in What4.Protocol.SMTLib2.Response | |
data SMTLib2Exception Source #
Constructors
| SMTLib2Unsupported Command | |
| SMTLib2Error Command Text | |
| SMTLib2ParseError SMTLib2Intent [Command] Text | |
| SMTLib2ResponseUnrecognized Command Text | |
| SMTLib2InvalidResponse Command SMTLib2Intent SMTResponse |
Instances
| Exception SMTLib2Exception Source # | |
Defined in What4.Protocol.SMTLib2.Response Methods toException :: SMTLib2Exception -> SomeException # | |
| Show SMTLib2Exception Source # | |
Defined in What4.Protocol.SMTLib2.Response Methods showsPrec :: Int -> SMTLib2Exception -> ShowS # show :: SMTLib2Exception -> String # showList :: [SMTLib2Exception] -> ShowS # | |
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 #