    {-|
    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.
    -}

    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE OverloadedStrings #-}

    module What4.Protocol.SMTLib2.Response
      (
        SMTResponse(..)
      , SMTLib2Exception(..)
      , getSolverResponse
      , getLimitedSolverResponse
      , smtParseOptions
      , strictSMTParsing
      , strictSMTParseOpt
      )
    where

    import           Control.Applicative
    import           Control.Exception
    import qualified Data.Attoparsec.Text as AT
    import           Data.Maybe ( isJust )
    import           Data.Text ( Text )
    import qualified Data.Text as Text
    import qualified Data.Text.Lazy as Lazy
    import qualified Data.Text.Lazy.Builder as Builder
    import qualified Prettyprinter.Util as PPU
    import qualified System.IO.Streams as Streams
    import qualified System.IO.Streams.Attoparsec.Text as AStreams

    import qualified What4.BaseTypes as BT
    import qualified What4.Config as CFG
    import           What4.Protocol.SExp
    import qualified What4.Protocol.SMTLib2.Syntax as SMT2
    import qualified What4.Protocol.SMTWriter as SMTWriter
    import           What4.Utils.Process ( filterAsync )

    strictSMTParsing :: CFG.ConfigOption BT.BaseBoolType
    strictSMTParsing :: ConfigOption BaseBoolType
    strictSMTParsing = BaseTypeRepr BaseBoolType -> String -> ConfigOption BaseBoolType
    forall (tp :: BaseType).
    BaseTypeRepr tp -> String -> ConfigOption tp
    CFG.configOption BaseTypeRepr BaseBoolType
    BT.BaseBoolRepr String
    "solver.strict_parsing"

    strictSMTParseOpt :: CFG.ConfigDesc
    strictSMTParseOpt :: ConfigDesc
    strictSMTParseOpt =
      ConfigOption BaseBoolType
    -> OptionStyle BaseBoolType
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal BaseBoolType)
    -> ConfigDesc
    forall (tp :: BaseType).
    ConfigOption tp
    -> OptionStyle tp
    -> Maybe (Doc Void)
    -> Maybe (ConcreteVal tp)
    -> ConfigDesc
    CFG.mkOpt ConfigOption BaseBoolType
    strictSMTParsing OptionStyle BaseBoolType
    CFG.boolOptSty
      (Doc Void -> Maybe (Doc Void)
    forall a. a -> Maybe a
    Just (Doc Void -> Maybe (Doc Void)) -> Doc Void -> Maybe (Doc Void)
    forall a b. (a -> b) -> a -> b
    $ Text -> Doc Void
    forall ann. Text -> Doc ann
    PPU.reflow (Text -> Doc Void) -> Text -> Doc Void
    forall a b. (a -> b) -> a -> b
    $
       [Text] -> Text
    Text.concat [Text
    "Strictly parse SMT responses and fail on"
                   , Text
    "unrecognized data (the default)."
                   , Text
    "This might need to be disabled when running"
                   , Text
    "the SMT solver in verbose mode."
                   ])
      Maybe (ConcreteVal BaseBoolType)
    forall a. Maybe a
    Nothing

    smtParseOptions :: [CFG.ConfigDesc]
    smtParseOptions :: [ConfigDesc]
    smtParseOptions = [ ConfigDesc
    strictSMTParseOpt ]

    data SMTResponse = AckSuccess
                     | AckUnsupported
                     | AckError Text
                     | AckSat
                     | AckUnsat
                     | AckUnknown
                     | AckInfeasible -- SyGuS response
                     | AckFail -- SyGuS response
                     | RspName Text
                     | RspVersion Text
                     | RspErrBehavior Text
                     | RspOutOfMemory
                     | RspRsnIncomplete
                     | RspUnkReason SExp
                     | AckSuccessSExp SExp
                     | AckSkipped Text SMTResponse
                     deriving (SMTResponse -> SMTResponse -> Bool
    (SMTResponse -> SMTResponse -> Bool)
    -> (SMTResponse -> SMTResponse -> Bool) -> Eq SMTResponse
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: SMTResponse -> SMTResponse -> Bool
    == :: SMTResponse -> SMTResponse -> Bool
    $c/= :: SMTResponse -> SMTResponse -> Bool
    /= :: SMTResponse -> SMTResponse -> Bool
    Eq, Int -> SMTResponse -> ShowS
    [SMTResponse] -> ShowS
    SMTResponse -> String
    (Int -> SMTResponse -> ShowS)
    -> (SMTResponse -> String)
    -> ([SMTResponse] -> ShowS)
    -> Show SMTResponse
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> SMTResponse -> ShowS
    showsPrec :: Int -> SMTResponse -> ShowS
    $cshow :: SMTResponse -> String
    show :: SMTResponse -> String
    $cshowList :: [SMTResponse] -> ShowS
    showList :: [SMTResponse] -> ShowS
    Show)

    -- | Called to get a response from the SMT connection.

    getSolverResponse :: SMTWriter.WriterConn t h
                      -> IO (Either SomeException SMTResponse)
    getSolverResponse :: forall t h. WriterConn t h -> IO (Either SomeException SMTResponse)
    getSolverResponse WriterConn t h
    conn = do
      Either SomeException SMTResponse
    mb <- (SomeException -> Maybe SomeException)
    -> IO SMTResponse -> IO (Either SomeException SMTResponse)
    forall e b a.
    Exception e =>
    (e -> Maybe b) -> IO a -> IO (Either b a)
    tryJust SomeException -> Maybe SomeException
    filterAsync
            (Parser SMTResponse -> InputStream Text -> IO SMTResponse
    forall r. Parser r -> InputStream Text -> IO r
    AStreams.parseFromStream
              -- n.b. the parseFromStream with an attoparsec parser used
              -- here will throw
              -- System.IO.Streams.Attoparsec.ParseException on a parser
              -- failure; the rspParser throws some other parse errors
              (ResponseStrictness -> Parser SMTResponse
    rspParser (WriterConn t h -> ResponseStrictness
    forall t h. WriterConn t h -> ResponseStrictness
    SMTWriter.strictParsing WriterConn t h
    conn))
              (WriterConn t h -> InputStream Text
    forall t h. WriterConn t h -> InputStream Text
    SMTWriter.connInputHandle WriterConn t h
    conn))
      Either SomeException SMTResponse
    -> IO (Either SomeException SMTResponse)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Either SomeException SMTResponse
    mb

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

    getLimitedSolverResponse :: String
                             -> (SMTResponse -> Maybe a)
                             -> SMTWriter.WriterConn t h
                             -> SMT2.Command
                             -> IO a
    getLimitedSolverResponse :: forall a t h.
    String
    -> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
    getLimitedSolverResponse String
    intent SMTResponse -> Maybe a
    handleResponse WriterConn t h
    conn Command
    cmd =
      let validateResp :: SMTResponse -> m a
    validateResp SMTResponse
    rsp =
            case SMTResponse
    rsp of
              SMTResponse
    AckUnsupported -> SMTLib2Exception -> m a
    forall a e. Exception e => e -> a
    throw (Command -> SMTLib2Exception
    SMTLib2Unsupported Command
    cmd)
              (AckError Text
    msg) -> SMTLib2Exception -> m a
    forall a e. Exception e => e -> a
    throw (Command -> Text -> SMTLib2Exception
    SMTLib2Error Command
    cmd Text
    msg)
              (AckSkipped Text
    _line SMTResponse
    rest) -> SMTResponse -> m a
    validateResp SMTResponse
    rest
              SMTResponse
    _ -> case SMTResponse -> Maybe a
    handleResponse SMTResponse
    rsp of
                     Just a
    x -> a -> m a
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return a
    x
                     Maybe a
    Nothing -> SMTLib2Exception -> m a
    forall a e. Exception e => e -> a
    throw (SMTLib2Exception -> m a) -> SMTLib2Exception -> m a
    forall a b. (a -> b) -> a -> b
    $ Command -> String -> SMTResponse -> SMTLib2Exception
    SMTLib2InvalidResponse Command
    cmd String
    intent SMTResponse
    rsp
      in WriterConn t h -> IO (Either SomeException SMTResponse)
    forall t h. WriterConn t h -> IO (Either SomeException SMTResponse)
    getSolverResponse WriterConn t h
    conn IO (Either SomeException SMTResponse)
    -> (Either SomeException SMTResponse -> IO a) -> IO a
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Right SMTResponse
    rsp -> SMTResponse -> IO a
    forall {m :: Type -> Type}. Monad m => SMTResponse -> m a
    validateResp SMTResponse
    rsp
        Left se :: SomeException
    se@(SomeException e
    e)
          | Maybe SomeException -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe SomeException -> Bool) -> Maybe SomeException -> Bool
    forall a b. (a -> b) -> a -> b
    $ SomeException -> Maybe SomeException
    filterAsync SomeException
    se -> e -> IO a
    forall a e. Exception e => e -> a
    throw e
    e
          | Just (AStreams.ParseException String
    _) <- SomeException -> Maybe ParseException
    forall e. Exception e => SomeException -> Maybe e
    fromException SomeException
    se
            -> do -- Parser failed and left the unparseable input in the
                  -- stream; extract it to show the user
                  Maybe Text
    curInp <- InputStream Text -> IO (Maybe Text)
    forall a. InputStream a -> IO (Maybe a)
    Streams.read (WriterConn t h -> InputStream Text
    forall t h. WriterConn t h -> InputStream Text
    SMTWriter.connInputHandle WriterConn t h
    conn)
                  SMTLib2Exception -> IO a
    forall a e. Exception e => e -> a
    throw (SMTLib2Exception -> IO a) -> SMTLib2Exception -> IO a
    forall a b. (a -> b) -> a -> b
    $ String -> [Command] -> Text -> SMTLib2Exception
    SMTLib2ParseError String
    intent [Command
    cmd] (Text -> SMTLib2Exception) -> Text -> SMTLib2Exception
    forall a b. (a -> b) -> a -> b
    $ String -> Text
    Text.pack (String -> Text) -> String -> Text
    forall a b. (a -> b) -> a -> b
    $
                    [String] -> String
    unlines [ String
    "Solver response parsing failure."
                            , String
    "*** Exception: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ e -> String
    forall e. Exception e => e -> String
    displayException e
    e
                            , String
    "Attempting to parse input for " String -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> String
    intent String -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> String
    ":"
                            , Maybe Text -> String
    forall a. Show a => a -> String
    show Maybe Text
    curInp
                            ]
          | Bool
    otherwise -> e -> IO a
    forall a e. Exception e => e -> a
    throw e
    e

    rspParser :: SMTWriter.ResponseStrictness -> AT.Parser SMTResponse
    rspParser :: ResponseStrictness -> Parser SMTResponse
    rspParser ResponseStrictness
    strictness =
      let lexeme :: Parser Text b -> Parser Text b
    lexeme Parser Text b
    p = Parser ()
    skipSpaceOrNewline Parser () -> Parser Text b -> Parser Text b
    forall a b. Parser Text a -> Parser Text b -> Parser Text b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> Parser Text b
    p
          parens :: Parser Text a -> Parser Text a
    parens Parser Text a
    p = Char -> Parser Char
    AT.char Char
    '(' Parser Char -> Parser Text a -> Parser Text a
    forall a b. Parser Text a -> Parser Text b -> Parser Text b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> Parser Text a
    p Parser Text a -> Parser Char -> Parser Text a
    forall a b. Parser Text a -> Parser Text b -> Parser Text a
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f a
    <* Char -> Parser Char
    AT.char Char
    ')'
          errParser :: Parser SMTResponse
    errParser = Parser SMTResponse -> Parser SMTResponse
    forall {a}. Parser Text a -> Parser Text a
    parens (Parser SMTResponse -> Parser SMTResponse)
    -> Parser SMTResponse -> Parser SMTResponse
    forall a b. (a -> b) -> a -> b
    $ Parser Text Text -> Parser Text Text
    forall {a}. Parser Text a -> Parser Text a
    lexeme (Text -> Parser Text Text
    AT.string Text
    "error")
                      Parser Text Text -> Parser SMTResponse -> Parser SMTResponse
    forall a b. Parser Text a -> Parser Text b -> Parser Text b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> (Text -> SMTResponse
    AckError (Text -> SMTResponse) -> Parser Text Text -> Parser SMTResponse
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser Text Text -> Parser Text Text
    forall {a}. Parser Text a -> Parser Text a
    lexeme Parser Text Text
    parseSMTLib2String)
          specific_success_response :: Parser SMTResponse
    specific_success_response = Parser SMTResponse
    check_sat_response Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
    forall a. Parser Text a -> Parser Text a -> Parser Text a
    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
    <|> Parser SMTResponse
    check_synth_response Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
    forall a. Parser Text a -> Parser Text a -> Parser Text a
    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
    <|> Parser SMTResponse
    get_info_response
          check_sat_response :: Parser SMTResponse
    check_sat_response = (SMTResponse
    AckSat SMTResponse -> Parser Text Text -> Parser SMTResponse
    forall a b. a -> Parser Text b -> Parser Text a
    forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
    <$ Text -> Parser Text Text
    AT.string Text
    "sat")
                               Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
    forall a. Parser Text a -> Parser Text a -> Parser Text a
    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
    <|> (SMTResponse
    AckUnsat SMTResponse -> Parser Text Text -> Parser SMTResponse
    forall a b. a -> Parser Text b -> Parser Text a
    forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
    <$ Text -> Parser Text Text
    AT.string Text
    "unsat")
                               Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
    forall a. Parser Text a -> Parser Text a -> Parser Text a
    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
    <|> (SMTResponse
    AckUnknown SMTResponse -> Parser Text Text -> Parser SMTResponse
    forall a b. a -> Parser Text b -> Parser Text a
    forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
    <$ Text -> Parser Text Text
    AT.string Text
    "unknown")
          check_synth_response :: Parser SMTResponse
    check_synth_response = (SMTResponse
    AckInfeasible SMTResponse -> Parser Text Text -> Parser SMTResponse
    forall a b. a -> Parser Text b -> Parser Text a
    forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
    <$ Text -> Parser Text Text
    AT.string Text
    "infeasible")
                                 Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
    forall a. Parser Text a -> Parser Text a -> Parser Text a
    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
    <|> (SMTResponse
    AckFail SMTResponse -> Parser Text Text -> Parser SMTResponse
    forall a b. a -> Parser Text b -> Parser Text a
    forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
    <$ Text -> Parser Text Text
    AT.string Text
    "fail")
          get_info_response :: Parser SMTResponse
    get_info_response = Parser SMTResponse -> Parser SMTResponse
    forall {a}. Parser Text a -> Parser Text a
    parens Parser SMTResponse
    info_response
          info_response :: Parser SMTResponse
    info_response = Parser SMTResponse
    errBhvParser
                          Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
    forall a. Parser Text a -> Parser Text a -> Parser Text a
    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
    <|> Parser SMTResponse
    nameParser
                          Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
    forall a. Parser Text a -> Parser Text a -> Parser Text a
    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
    <|> Parser SMTResponse
    unkReasonParser
                          Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
    forall a. Parser Text a -> Parser Text a -> Parser Text a
    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
    <|> Parser SMTResponse
    versionParser
          nameParser :: Parser SMTResponse
    nameParser = Parser Text Text -> Parser Text Text
    forall {a}. Parser Text a -> Parser Text a
    lexeme (Text -> Parser Text Text
    AT.string Text
    ":name")
                       Parser Text Text -> Parser SMTResponse -> Parser SMTResponse
    forall a b. Parser Text a -> Parser Text b -> Parser Text b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> Parser SMTResponse -> Parser SMTResponse
    forall {a}. Parser Text a -> Parser Text a
    lexeme (Text -> SMTResponse
    RspName (Text -> SMTResponse) -> Parser Text Text -> Parser SMTResponse
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser Text Text
    parseSMTLib2String)
          versionParser :: Parser SMTResponse
    versionParser = Parser Text Text -> Parser Text Text
    forall {a}. Parser Text a -> Parser Text a
    lexeme (Text -> Parser Text Text
    AT.string Text
    ":version")
                          Parser Text Text -> Parser SMTResponse -> Parser SMTResponse
    forall a b. Parser Text a -> Parser Text b -> Parser Text b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> Parser SMTResponse -> Parser SMTResponse
    forall {a}. Parser Text a -> Parser Text a
    lexeme (Text -> SMTResponse
    RspVersion (Text -> SMTResponse) -> Parser Text Text -> Parser SMTResponse
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser Text Text
    parseSMTLib2String)
          errBhvParser :: Parser SMTResponse
    errBhvParser = Parser Text Text -> Parser Text Text
    forall {a}. Parser Text a -> Parser Text a
    lexeme (Text -> Parser Text Text
    AT.string Text
    ":error-behavior")
                         Parser Text Text -> Parser SMTResponse -> Parser SMTResponse
    forall a b. Parser Text a -> Parser Text b -> Parser Text b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> Parser SMTResponse -> Parser SMTResponse
    forall {a}. Parser Text a -> Parser Text a
    lexeme (Text -> SMTResponse
    RspErrBehavior (Text -> SMTResponse) -> Parser Text Text -> Parser SMTResponse
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                                    (Text -> Parser Text Text
    AT.string Text
    "continued-execution"
                                     Parser Text Text -> Parser Text Text -> Parser Text Text
    forall a. Parser Text a -> Parser Text a -> Parser Text a
    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
    <|> Text -> Parser Text Text
    AT.string Text
    "immediate-exit")
                                     -- Explicit error instead of generic
                                     -- fallback since :error-behavior was
                                     -- matched but behavior type was not.
                                     Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
    forall a. Parser Text a -> Parser Text a -> Parser Text a
    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
    <|> SMTLib2Exception -> Parser SMTResponse
    forall a e. Exception e => e -> a
    throw (Command -> Text -> SMTLib2Exception
    SMTLib2ResponseUnrecognized
                                                Command
    SMT2.getErrorBehavior
                                                Text
    "bad :error-behavior value")
                                   )
          unkReasonParser :: Parser SMTResponse
    unkReasonParser =
            Parser Text Text -> Parser Text Text
    forall {a}. Parser Text a -> Parser Text a
    lexeme (Text -> Parser Text Text
    AT.string Text
    ":reason-unknown")
            Parser Text Text -> Parser SMTResponse -> Parser SMTResponse
    forall a b. Parser Text a -> Parser Text b -> Parser Text b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> Parser SMTResponse -> Parser SMTResponse
    forall {a}. Parser Text a -> Parser Text a
    lexeme (SMTResponse
    RspOutOfMemory SMTResponse -> Parser Text Text -> Parser SMTResponse
    forall a b. a -> Parser Text b -> Parser Text a
    forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
    <$ Text -> Parser Text Text
    AT.string Text
    "memout"
                        Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
    forall a. Parser Text a -> Parser Text a -> Parser Text a
    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
    <|> SMTResponse
    RspRsnIncomplete SMTResponse -> Parser Text Text -> Parser SMTResponse
    forall a b. a -> Parser Text b -> Parser Text a
    forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
    <$ Text -> Parser Text Text
    AT.string Text
    "incomplete"
                        Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
    forall a. Parser Text a -> Parser Text a -> Parser Text a
    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
    <|> (Char -> Parser Char
    AT.char Char
    '(' Parser Char -> Parser SMTResponse -> Parser SMTResponse
    forall a b. Parser Text a -> Parser Text b -> Parser Text b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> (SExp -> SMTResponse
    RspUnkReason (SExp -> SMTResponse) -> Parser Text SExp -> Parser SMTResponse
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser Text Text -> Parser Text SExp
    parseSExpBody Parser Text Text
    parseSMTLib2String))
                        -- already matched :reason-unknown, so any other
                        -- arguments to that are errors.
                        Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
    forall a. Parser Text a -> Parser Text a -> Parser Text a
    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
    <|> SMTLib2Exception -> Parser SMTResponse
    forall a e. Exception e => e -> a
    throw (Command -> Text -> SMTLib2Exception
    SMTLib2ResponseUnrecognized
                                   (Builder -> Command
    SMT2.Cmd Builder
    "reason?")
                                   Text
    "bad :reason-unknown value")
                      )
      in Parser ()
    skipSpaceOrNewline Parser () -> Parser SMTResponse -> Parser SMTResponse
    forall a b. Parser Text a -> Parser Text b -> Parser Text b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *>
         ((SMTResponse
    AckSuccess SMTResponse -> Parser Text Text -> Parser SMTResponse
    forall a b. a -> Parser Text b -> Parser Text a
    forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
    <$ Text -> Parser Text Text
    AT.string Text
    "success")
          Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
    forall a. Parser Text a -> Parser Text a -> Parser Text a
    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
    <|> (SMTResponse
    AckUnsupported SMTResponse -> Parser Text Text -> Parser SMTResponse
    forall a b. a -> Parser Text b -> Parser Text a
    forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
    <$ Text -> Parser Text Text
    AT.string Text
    "unsupported")
          Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
    forall a. Parser Text a -> Parser Text a -> Parser Text a
    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
    <|> Parser SMTResponse
    specific_success_response
          Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
    forall a. Parser Text a -> Parser Text a -> Parser Text a
    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
    <|> Parser SMTResponse
    errParser
          Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
    forall a. Parser Text a -> Parser Text a -> Parser Text a
    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
    <|> (Char -> Parser Char
    AT.char Char
    '(' Parser Char -> Parser SMTResponse -> Parser SMTResponse
    forall a b. Parser Text a -> Parser Text b -> Parser Text b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> (SExp -> SMTResponse
    AckSuccessSExp (SExp -> SMTResponse) -> Parser Text SExp -> Parser SMTResponse
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser Text Text -> Parser Text SExp
    parseSExpBody Parser Text Text
    parseSMTLib2String))
          -- sometimes verbose output mode will generate interim text
          -- before the actual ack; the following skips lines of input
          -- that aren't recognized.
           Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
    forall a. Parser Text a -> Parser Text a -> Parser Text a
    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
    <|> (case ResponseStrictness
    strictness of
                  ResponseStrictness
    SMTWriter.Strict -> Parser SMTResponse
    forall a. Parser Text a
    forall (f :: Type -> Type) a. Alternative f => f a
    empty
                  ResponseStrictness
    SMTWriter.Lenient -> Text -> SMTResponse -> SMTResponse
    AckSkipped
                                       (Text -> SMTResponse -> SMTResponse)
    -> Parser Text Text -> Parser Text (SMTResponse -> SMTResponse)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Char -> Bool) -> Parser Text Text
    AT.takeWhile1 (Bool -> Bool
    not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Char -> Bool
    AT.isEndOfLine)
                                       Parser Text (SMTResponse -> SMTResponse)
    -> Parser SMTResponse -> Parser SMTResponse
    forall a b. Parser Text (a -> b) -> Parser Text a -> Parser Text b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> (ResponseStrictness -> Parser SMTResponse
    rspParser ResponseStrictness
    strictness))
         )

    parseSMTLib2String :: AT.Parser Text
    parseSMTLib2String :: Parser Text Text
    parseSMTLib2String = Char -> Parser Char
    AT.char Char
    '\"' Parser Char -> Parser Text Text -> Parser Text Text
    forall a b. Parser Text a -> Parser Text b -> Parser Text b
    forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
    >> Parser Text Text
    go
     where
     go :: AT.Parser Text
     go :: Parser Text Text
    go = do Text
    xs <- (Char -> Bool) -> Parser Text Text
    AT.takeWhile (Bool -> Bool
    not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    ==Char
    '\"'))
             Char
    _ <- Char -> Parser Char
    AT.char Char
    '\"'
             (do Char
    _ <- Char -> Parser Char
    AT.char Char
    '\"'
                 Text
    ys <- Parser Text Text
    go
                 Text -> Parser Text Text
    forall a. a -> Parser Text a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Text
    xs Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "\"" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    ys)
              ) Parser Text Text -> Parser Text Text -> Parser Text Text
    forall a. Parser Text a -> Parser Text a -> Parser Text a
    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
    <|> Text -> Parser Text Text
    forall a. a -> Parser Text a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Text
    xs

    ----------------------------------------------------------------------

    data SMTLib2Exception
      = SMTLib2Unsupported SMT2.Command
      | SMTLib2Error SMT2.Command Text
      | SMTLib2ParseError SMTLib2Intent [SMT2.Command] Text
      | SMTLib2ResponseUnrecognized SMT2.Command Text
      | SMTLib2InvalidResponse SMT2.Command SMTLib2Intent SMTResponse

    type SMTLib2Intent = String

    instance Show SMTLib2Exception where
      show :: SMTLib2Exception -> String
    show =
        let showCmd :: Command -> String
    showCmd (SMT2.Cmd Builder
    c) = Text -> String
    Lazy.unpack (Text -> String) -> Text -> String
    forall a b. (a -> b) -> a -> b
    $ Builder -> Text
    Builder.toLazyText Builder
    c
        in [String] -> String
    unlines ([String] -> String)
    -> (SMTLib2Exception -> [String]) -> SMTLib2Exception -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . \case
          (SMTLib2Unsupported Command
    cmd) ->
            [ String
    "unsupported command:"
            , String
    "  " String -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> Command -> String
    showCmd Command
    cmd
            ]
          (SMTLib2Error Command
    cmd Text
    msg) ->
            [ String
    "Solver reported an error:"
            , String
    "  " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Text -> String
    Text.unpack Text
    msg
            , String
    "in response to command:"
            , String
    "  " String -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> Command -> String
    showCmd Command
    cmd
            ]
          (SMTLib2ParseError String
    intent [Command]
    cmds Text
    msg) ->
            [ String
    "Could not parse solver response:"
            , String
    "  " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Text -> String
    Text.unpack Text
    msg
            , String
    "in response to commands for " String -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> String
    intent String -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> String
    ":"
            ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (Command -> String) -> [Command] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Command -> String
    showCmd [Command]
    cmds
          (SMTLib2ResponseUnrecognized Command
    cmd Text
    rsp) ->
            [ String
    "Unrecognized response from solver:"
            , String
    "  " String -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> Text -> String
    Text.unpack Text
    rsp
            , String
    "in response to command:"
            , String
    "  " String -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> Command -> String
    showCmd Command
    cmd
            ]
          (SMTLib2InvalidResponse Command
    cmd String
    intent SMTResponse
    rsp) ->
            [ String
    "Received parsed and understood but unexpected response from solver:"
            , String
    "  " String -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> SMTResponse -> String
    forall a. Show a => a -> String
    show SMTResponse
    rsp
            , String
    "in response to command for " String -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> String
    intent String -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> String
    ":"
            , String
    "  " String -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> Command -> String
    showCmd Command
    cmd
            ]

    instance Exception SMTLib2Exception