what4-1.2: Solver-agnostic symbolic values support for issuing queries
Safe HaskellNone
LanguageHaskell2010

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

Documentation

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.