What4.Protocol.SMTLib2.Response

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.

Documentation

data SMTResponse

Constructors

AckSuccess

AckUnsupported

AckError Text

AckSat

AckUnsat

AckUnknown

RspName Text

RspVersion Text

RspErrBehavior Text

RspOutOfMemory

RspRsnIncomplete

RspUnkReason SExp

AckSuccessSExp SExp

AckSkipped Text SMTResponse

Instances

Eq SMTResponse

Defined in What4.Protocol.SMTLib2.Response

Methods

(==) :: SMTResponse -> SMTResponse -> Bool

(/=) :: SMTResponse -> SMTResponse -> Bool

Show SMTResponse

Defined in What4.Protocol.SMTLib2.Response

Methods

showsPrec :: Int -> SMTResponse -> ShowS

show :: SMTResponse -> String

showList :: [SMTResponse] -> ShowS

data SMTLib2Exception

Constructors

SMTLib2Unsupported Command

SMTLib2Error Command Text

SMTLib2ParseError SMTLib2Intent [Command] Text

SMTLib2ResponseUnrecognized Command Text

SMTLib2InvalidResponse Command SMTLib2Intent SMTResponse

Instances

Show SMTLib2Exception

Defined in What4.Protocol.SMTLib2.Response

Methods

showsPrec :: Int -> SMTLib2Exception -> ShowS

show :: SMTLib2Exception -> String

showList :: [SMTLib2Exception] -> ShowS

Exception SMTLib2Exception

Defined in What4.Protocol.SMTLib2.Response

Methods

toException :: SMTLib2Exception -> SomeException

fromException :: SomeException -> Maybe SMTLib2Exception

displayException :: SMTLib2Exception -> String

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

Called to get a response from the SMT connection.

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

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]

strictSMTParsing :: ConfigOption BaseBoolType

strictSMTParseOpt :: ConfigDesc