    {-|
    This module defines types and operations for parsing results from SMTLIB2.

    It does not depend on the rest of What4 so that it can be used
    directly by clients interested in generating SMTLIB without depending
    on the What4 formula interface.  All the type constructors are exposed
    so that clients can generate new values that are not exposed through
    this interface.
    -}
    {-# LANGUAGE CPP #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GeneralizedNewtypeDeriving #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE PatternSynonyms #-}
    {-# LANGUAGE TemplateHaskell #-}
    module What4.Protocol.SMTLib2.Parse
      ( -- * CheckSatResponse
        CheckSatResponse(..)
      , readCheckSatResponse
        -- * GetModelResponse
      , GetModelResponse
      , readGetModelResponse
      , ModelResponse(..)
      , DefineFun(..)
      , Symbol
        -- ** Sorts
      , Sort(..)
      , pattern Bool
      , pattern Int
      , pattern Real
      , pattern RoundingMode
      , pattern Array
        -- ** Terms
      , Term(..)
      ) where

    #if !MIN_VERSION_base(4,13,0)
    import Control.Monad.Fail( MonadFail )
    import qualified Control.Monad.Fail
    #endif

    import           Control.Monad (when)
    import           Control.Monad.Reader (ReaderT(..))
    import qualified Data.ByteString as BS
    import qualified Data.ByteString.UTF8 as UTF8
    import           Data.Char
    import           Data.HashSet (HashSet)
    import qualified Data.HashSet as HSet
    import           Data.Ratio
    import           Data.String
    import           Data.Word
    import           System.IO

    c2b :: Char -> Word8
    c2b :: Char -> Word8
    c2b = Int -> Word8
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int -> Word8) -> (Char -> Int) -> Char -> Word8
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Char -> Int
    forall a. Enum a => a -> Int
    fromEnum

    ------------------------------------------------------------------------
    -- Parser definitions

    -- | A parser monad that just reads from a handle.
    --
    -- We use our own parser rather than Attoparsec or some other library
    -- so that we can incrementally request characters.
    --
    -- We likely could replace this with Attoparsec by assuming that
    -- SMTLIB solvers always end their output responses with newlines, or
    -- feeding output one character at a time.
    newtype Parser a = Parser { forall a. Parser a -> ReaderT Handle IO a
    unParser :: ReaderT Handle IO a }
      deriving ((forall a b. (a -> b) -> Parser a -> Parser b)
    -> (forall a b. a -> Parser b -> Parser a) -> Functor Parser
    forall a b. a -> Parser b -> Parser a
    forall a b. (a -> b) -> Parser a -> Parser b
    forall (f :: Type -> Type).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> Parser a -> Parser b
    fmap :: forall a b. (a -> b) -> Parser a -> Parser b
    $c<$ :: forall a b. a -> Parser b -> Parser a
    <$ :: forall a b. a -> Parser b -> Parser a
    Functor, Functor Parser
    Functor Parser
    -> (forall a. a -> Parser a)
    -> (forall a b. Parser (a -> b) -> Parser a -> Parser b)
    -> (forall a b c.
        (a -> b -> c) -> Parser a -> Parser b -> Parser c)
    -> (forall a b. Parser a -> Parser b -> Parser b)
    -> (forall a b. Parser a -> Parser b -> Parser a)
    -> Applicative Parser
    forall a. a -> Parser a
    forall a b. Parser a -> Parser b -> Parser a
    forall a b. Parser a -> Parser b -> Parser b
    forall a b. Parser (a -> b) -> Parser a -> Parser b
    forall a b c. (a -> b -> c) -> Parser a -> Parser b -> Parser c
    forall (f :: Type -> Type).
    Functor f
    -> (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    $cpure :: forall a. a -> Parser a
    pure :: forall a. a -> Parser a
    $c<*> :: forall a b. Parser (a -> b) -> Parser a -> Parser b
    <*> :: forall a b. Parser (a -> b) -> Parser a -> Parser b
    $cliftA2 :: forall a b c. (a -> b -> c) -> Parser a -> Parser b -> Parser c
    liftA2 :: forall a b c. (a -> b -> c) -> Parser a -> Parser b -> Parser c
    $c*> :: forall a b. Parser a -> Parser b -> Parser b
    *> :: forall a b. Parser a -> Parser b -> Parser b
    $c<* :: forall a b. Parser a -> Parser b -> Parser a
    <* :: forall a b. Parser a -> Parser b -> Parser a
    Applicative)

    instance Monad Parser where
      Parser ReaderT Handle IO a
    m >>= :: forall a b. Parser a -> (a -> Parser b) -> Parser b
    >>= a -> Parser b
    h = ReaderT Handle IO b -> Parser b
    forall a. ReaderT Handle IO a -> Parser a
    Parser (ReaderT Handle IO b -> Parser b)
    -> ReaderT Handle IO b -> Parser b
    forall a b. (a -> b) -> a -> b
    $ ReaderT Handle IO a
    m ReaderT Handle IO a
    -> (a -> ReaderT Handle IO b) -> ReaderT Handle IO b
    forall a b.
    ReaderT Handle IO a
    -> (a -> ReaderT Handle IO b) -> ReaderT Handle IO b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Parser b -> ReaderT Handle IO b
    forall a. Parser a -> ReaderT Handle IO a
    unParser (Parser b -> ReaderT Handle IO b)
    -> (a -> Parser b) -> a -> ReaderT Handle IO b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Parser b
    h
    #if !MIN_VERSION_base(4,13,0)
      fail = Control.Monad.Fail.fail
    #endif

    instance MonadFail Parser where
      fail :: forall a. [Char] -> Parser a
    fail = [Char] -> Parser a
    forall a. HasCallStack => [Char] -> a
    error

    runParser :: Handle -> Parser a -> IO a
    runParser :: forall a. Handle -> Parser a -> IO a
    runParser Handle
    h (Parser ReaderT Handle IO a
    f) = ReaderT Handle IO a -> Handle -> IO a
    forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
    runReaderT ReaderT Handle IO a
    f Handle
    h

    parseChar :: Parser Char
    parseChar :: Parser Char
    parseChar = ReaderT Handle IO Char -> Parser Char
    forall a. ReaderT Handle IO a -> Parser a
    Parser (ReaderT Handle IO Char -> Parser Char)
    -> ReaderT Handle IO Char -> Parser Char
    forall a b. (a -> b) -> a -> b
    $ (Handle -> IO Char) -> ReaderT Handle IO Char
    forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
    ReaderT ((Handle -> IO Char) -> ReaderT Handle IO Char)
    -> (Handle -> IO Char) -> ReaderT Handle IO Char
    forall a b. (a -> b) -> a -> b
    $ Handle -> IO Char
    hGetChar

    -- | Peek ahead to get the next character.
    peekChar :: Parser Char
    peekChar :: Parser Char
    peekChar = ReaderT Handle IO Char -> Parser Char
    forall a. ReaderT Handle IO a -> Parser a
    Parser (ReaderT Handle IO Char -> Parser Char)
    -> ReaderT Handle IO Char -> Parser Char
    forall a b. (a -> b) -> a -> b
    $ (Handle -> IO Char) -> ReaderT Handle IO Char
    forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
    ReaderT ((Handle -> IO Char) -> ReaderT Handle IO Char)
    -> (Handle -> IO Char) -> ReaderT Handle IO Char
    forall a b. (a -> b) -> a -> b
    $ Handle -> IO Char
    hLookAhead

    dropChar :: Parser ()
    dropChar :: Parser ()
    dropChar = ReaderT Handle IO () -> Parser ()
    forall a. ReaderT Handle IO a -> Parser a
    Parser (ReaderT Handle IO () -> Parser ())
    -> ReaderT Handle IO () -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ (Handle -> IO ()) -> ReaderT Handle IO ()
    forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
    ReaderT ((Handle -> IO ()) -> ReaderT Handle IO ())
    -> (Handle -> IO ()) -> ReaderT Handle IO ()
    forall a b. (a -> b) -> a -> b
    $ \Handle
    h -> Handle -> IO Char
    hGetChar Handle
    h IO Char -> IO () -> IO ()
    forall a b. IO a -> IO b -> IO b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> () -> IO ()
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure ()

    -- | Drop characters until we get a non-whitespace character.
    dropWhitespace :: Parser ()
    dropWhitespace :: Parser ()
    dropWhitespace = do
      Char
    c <- Parser Char
    peekChar
      if Char -> Bool
    isSpace Char
    c then do
        Parser ()
    dropChar Parser () -> Parser () -> Parser ()
    forall a b. Parser a -> Parser b -> Parser b
    forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
    >> Parser ()
    dropWhitespace
       else
        () -> Parser ()
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure ()

    -- | Drop whitespace, and if next character matches expected return,
    -- otherwise fail.
    matchChar :: Char -> Parser ()
    matchChar :: Char -> Parser ()
    matchChar Char
    expected = do
      Char
    c <- Parser Char
    parseChar
      if Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    expected then
        () -> Parser ()
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure ()
       else if Char -> Bool
    isSpace Char
    c then
        Char -> Parser ()
    matchChar Char
    expected
       else
        [Char] -> Parser ()
    forall a. [Char] -> Parser a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail ([Char] -> Parser ()) -> [Char] -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Unexpected input char " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Char -> [Char]
    forall a. Show a => a -> [Char]
    show Char
    c [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "(expected " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Char -> [Char]
    forall a. Show a => a -> [Char]
    show Char
    expected [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ")"

    -- | Drop whitespace until we reach the given string.
    matchString :: BS.ByteString -> Parser ()
    matchString :: ByteString -> Parser ()
    matchString ByteString
    expected = do
      Parser ()
    dropWhitespace
      ByteString
    found <- ReaderT Handle IO ByteString -> Parser ByteString
    forall a. ReaderT Handle IO a -> Parser a
    Parser (ReaderT Handle IO ByteString -> Parser ByteString)
    -> ReaderT Handle IO ByteString -> Parser ByteString
    forall a b. (a -> b) -> a -> b
    $ (Handle -> IO ByteString) -> ReaderT Handle IO ByteString
    forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
    ReaderT ((Handle -> IO ByteString) -> ReaderT Handle IO ByteString)
    -> (Handle -> IO ByteString) -> ReaderT Handle IO ByteString
    forall a b. (a -> b) -> a -> b
    $ \Handle
    h -> Handle -> Int -> IO ByteString
    BS.hGet Handle
    h (ByteString -> Int
    BS.length ByteString
    expected)
      Bool -> Parser () -> Parser ()
    forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
    when (ByteString
    found ByteString -> ByteString -> Bool
    forall a. Eq a => a -> a -> Bool
    /= ByteString
    expected) (Parser () -> Parser ()) -> Parser () -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ do
        [Char] -> Parser ()
    forall a. [Char] -> Parser a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail ([Char] -> Parser ()) -> [Char] -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Unexpected string " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ByteString -> [Char]
    forall a. Show a => a -> [Char]
    show ByteString
    found [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "(expected " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ByteString -> [Char]
    forall a. Show a => a -> [Char]
    show ByteString
    expected [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ")"

    parseUntilCloseParen' :: [a] -> Parser a -> Parser [a]
    parseUntilCloseParen' :: forall a. [a] -> Parser a -> Parser [a]
    parseUntilCloseParen' [a]
    prev Parser a
    p = do
      Char
    c <- Parser Char
    peekChar
      if Char -> Bool
    isSpace Char
    c then
        Parser ()
    dropChar Parser () -> Parser [a] -> Parser [a]
    forall a b. Parser a -> Parser b -> Parser b
    forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
    >> [a] -> Parser a -> Parser [a]
    forall a. [a] -> Parser a -> Parser [a]
    parseUntilCloseParen' [a]
    prev Parser a
    p
       else if Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    ')' then
        Parser ()
    dropChar Parser () -> Parser [a] -> Parser [a]
    forall a b. Parser a -> Parser b -> Parser b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> [a] -> Parser [a]
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure ([a] -> [a]
    forall a. [a] -> [a]
    reverse [a]
    prev)
       else do
        Parser a
    p Parser a -> (a -> Parser [a]) -> Parser [a]
    forall a b. Parser a -> (a -> Parser b) -> Parser b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a
    n -> [a] -> Parser a -> Parser [a]
    forall a. [a] -> Parser a -> Parser [a]
    parseUntilCloseParen' (a
    na -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    prev) Parser a
    p

    -- | @parseUntilCloseParen p@ will drop whitespace characters, and
    -- run @p@
    parseUntilCloseParen :: Parser a -> Parser [a]
    parseUntilCloseParen :: forall a. Parser a -> Parser [a]
    parseUntilCloseParen = [a] -> Parser a -> Parser [a]
    forall a. [a] -> Parser a -> Parser [a]
    parseUntilCloseParen' []

    -- | @takeChars' p prev h@ prepends characters read from @h@ to @prev@
    -- until @p@ is false, and returns the resulting string.
    takeChars' :: (Char -> Bool) -> [Word8] -> Parser [Word8]
    takeChars' :: (Char -> Bool) -> [Word8] -> Parser [Word8]
    takeChars' Char -> Bool
    p [Word8]
    prev = do
      Char
    c <- Parser Char
    peekChar
      if Char -> Bool
    p Char
    c then do
        Char
    _ <- Parser Char
    parseChar
        (Char -> Bool) -> [Word8] -> Parser [Word8]
    takeChars' Char -> Bool
    p (Char -> Word8
    c2b Char
    cWord8 -> [Word8] -> [Word8]
    forall a. a -> [a] -> [a]
    :[Word8]
    prev)
       else do
        [Word8] -> Parser [Word8]
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure ([Word8] -> Parser [Word8]) -> [Word8] -> Parser [Word8]
    forall a b. (a -> b) -> a -> b
    $! [Word8]
    prev

    -- | @takeChars p@ returns the bytestring formed by reading
    -- characters until @p@ is false.
    takeChars :: (Char -> Bool) -> Parser BS.ByteString
    takeChars :: (Char -> Bool) -> Parser ByteString
    takeChars Char -> Bool
    p = do
      [Word8]
    l <- (Char -> Bool) -> [Word8] -> Parser [Word8]
    takeChars' Char -> Bool
    p []
      ByteString -> Parser ByteString
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (ByteString -> Parser ByteString)
    -> ByteString -> Parser ByteString
    forall a b. (a -> b) -> a -> b
    $! [Word8] -> ByteString
    BS.pack ([Word8] -> [Word8]
    forall a. [a] -> [a]
    reverse [Word8]
    l)

    instance IsString (Parser ()) where
      fromString :: [Char] -> Parser ()
    fromString = ByteString -> Parser ()
    matchString (ByteString -> Parser ())
    -> ([Char] -> ByteString) -> [Char] -> Parser ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> ByteString
    forall a. IsString a => [Char] -> a
    fromString

    -- | Parse a quoted string.
    parseQuotedString :: Parser String
    parseQuotedString :: Parser [Char]
    parseQuotedString = do
      Char -> Parser ()
    matchChar Char
    '"'
      ByteString
    l <- (Char -> Bool) -> Parser ByteString
    takeChars (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Char
    '"')
      Char -> Parser ()
    matchChar Char
    '"'
      [Char] -> Parser [Char]
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure ([Char] -> Parser [Char]) -> [Char] -> Parser [Char]
    forall a b. (a -> b) -> a -> b
    $ ByteString -> [Char]
    UTF8.toString ByteString
    l

    -- | Defines common operations for parsing SMTLIB results.
    class CanParse a where
      -- | Parser for values of this type.
      parse :: Parser a

      -- | Read from a handle.
      readFromHandle :: Handle -> IO a
      readFromHandle Handle
    h = Handle -> Parser a -> IO a
    forall a. Handle -> Parser a -> IO a
    runParser Handle
    h Parser a
    forall a. CanParse a => Parser a
    parse

    ------------------------------------------------------------------------
    -- Parse check-sat definitions

    -- | Result of check-sat and check-sat-assuming
    data CheckSatResponse
       = SatResponse
       | UnsatResponse
       | UnknownResponse
       | CheckSatUnsupported
       | CheckSatError !String

    instance CanParse CheckSatResponse where
      parse :: Parser CheckSatResponse
    parse = do
        Bool
    isParen <- Parser Bool
    checkParen
        if Bool
    isParen then do
          ByteString -> Parser ()
    matchString ByteString
    "error"
          Parser ()
    dropWhitespace
          [Char]
    msg <- Parser [Char]
    parseQuotedString
          Parser ()
    closeParen
          CheckSatResponse -> Parser CheckSatResponse
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure ([Char] -> CheckSatResponse
    CheckSatError [Char]
    msg)
         else
          [(ByteString, Parser CheckSatResponse)] -> Parser CheckSatResponse
    forall a. [(ByteString, Parser a)] -> Parser a
    matchApp [ (ByteString
    "sat",     CheckSatResponse -> Parser CheckSatResponse
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure CheckSatResponse
    SatResponse)
                   , (ByteString
    "unsat",   CheckSatResponse -> Parser CheckSatResponse
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure CheckSatResponse
    UnsatResponse)
                   , (ByteString
    "unknown", CheckSatResponse -> Parser CheckSatResponse
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure CheckSatResponse
    UnknownResponse)
                   , (ByteString
    "unsupported", CheckSatResponse -> Parser CheckSatResponse
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure CheckSatResponse
    CheckSatUnsupported)
                   ]

    -- | Read the results of a @(check-sat)@ request.
    readCheckSatResponse :: Handle -> IO CheckSatResponse
    readCheckSatResponse :: Handle -> IO CheckSatResponse
    readCheckSatResponse = Handle -> IO CheckSatResponse
    forall a. CanParse a => Handle -> IO a
    readFromHandle

    ------------------------------------------------------------------------
    -- Parse get-model definitions

    -- | An SMT symbol
    newtype Symbol = Symbol BS.ByteString
      deriving (Symbol -> Symbol -> Bool
    (Symbol -> Symbol -> Bool)
    -> (Symbol -> Symbol -> Bool) -> Eq Symbol
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Symbol -> Symbol -> Bool
    == :: Symbol -> Symbol -> Bool
    $c/= :: Symbol -> Symbol -> Bool
    /= :: Symbol -> Symbol -> Bool
    Eq)

    instance Show Symbol where
      show :: Symbol -> [Char]
    show (Symbol ByteString
    s) = ByteString -> [Char]
    forall a. Show a => a -> [Char]
    show ByteString
    s

    instance IsString Symbol where
      fromString :: [Char] -> Symbol
    fromString = ByteString -> Symbol
    Symbol (ByteString -> Symbol)
    -> ([Char] -> ByteString) -> [Char] -> Symbol
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> ByteString
    forall a. IsString a => [Char] -> a
    fromString

    symbolCharSet :: HashSet Char
    symbolCharSet :: HashSet Char
    symbolCharSet = [Char] -> HashSet Char
    forall a. (Eq a, Hashable a) => [a] -> HashSet a
    HSet.fromList
      ([Char] -> HashSet Char) -> [Char] -> HashSet Char
    forall a b. (a -> b) -> a -> b
    $  [Char
    'A'..Char
    'Z']
      [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char
    'a'..Char
    'z']
      [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char
    '0'..Char
    '9']
      [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char
    '~', Char
    '!', Char
    '@', Char
    '$', Char
    '%', Char
    '^', Char
    '&', Char
    '*', Char
    '_', Char
    '-', Char
    '+', Char
    '=', Char
    '<', Char
    '>', Char
    '.', Char
    '?', Char
    '/']

    initialSymbolCharSet :: HashSet Char
    initialSymbolCharSet :: HashSet Char
    initialSymbolCharSet = HashSet Char
    symbolCharSet HashSet Char -> HashSet Char -> HashSet Char
    forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
    `HSet.difference` ([Char] -> HashSet Char
    forall a. (Eq a, Hashable a) => [a] -> HashSet a
    HSet.fromList [Char
    '0'..Char
    '9'])

    generalReservedWords :: HashSet BS.ByteString
    generalReservedWords :: HashSet ByteString
    generalReservedWords = [ByteString] -> HashSet ByteString
    forall a. (Eq a, Hashable a) => [a] -> HashSet a
    HSet.fromList ([ByteString] -> HashSet ByteString)
    -> [ByteString] -> HashSet ByteString
    forall a b. (a -> b) -> a -> b
    $
      [ ByteString
    "!"
      , ByteString
    "_"
      , ByteString
    "as"
      , ByteString
    "BINARY"
      , ByteString
    "DECIMAL"
      , ByteString
    "exists"
      , ByteString
    "HEXADECIMAL"
      , ByteString
    "forall"
      , ByteString
    "let"
      , ByteString
    "match"
      , ByteString
    "NUMERAL"
      , ByteString
    "par"
      , ByteString
    "STRING"
      ]

    commandNames :: HashSet BS.ByteString
    commandNames :: HashSet ByteString
    commandNames = [ByteString] -> HashSet ByteString
    forall a. (Eq a, Hashable a) => [a] -> HashSet a
    HSet.fromList ([ByteString] -> HashSet ByteString)
    -> [ByteString] -> HashSet ByteString
    forall a b. (a -> b) -> a -> b
    $
      [ ByteString
    "assert"
      , ByteString
    "check-sat"
      , ByteString
    "check-sat-assuming"
      , ByteString
    "declare-const"
      , ByteString
    "declare-datatype"
      , ByteString
    "declare-datatypes"
      , ByteString
    "declare-fun"
      , ByteString
    "declare-sort"
      , ByteString
    "define-fun"
      , ByteString
    "define-fun-rec"
      , ByteString
    "define-sort"
      , ByteString
    "echo"
      , ByteString
    "exit"
      , ByteString
    "get-assertions"
      , ByteString
    "get-assignment"
      , ByteString
    "get-info"
      , ByteString
    "get-model"
      , ByteString
    "get-option"
      , ByteString
    "get-proof"
      , ByteString
    "get-unsat-assumptions"
      , ByteString
    "get-unsat-core"
      , ByteString
    "get-value"
      , ByteString
    "pop"
      , ByteString
    "push"
      , ByteString
    "reset"
      , ByteString
    "reset-assertions"
      , ByteString
    "set-info"
      , ByteString
    "set-logic"
      , ByteString
    "set-option"
      ]

    reservedWords :: HashSet BS.ByteString
    reservedWords :: HashSet ByteString
    reservedWords = HashSet ByteString -> HashSet ByteString -> HashSet ByteString
    forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
    HSet.union HashSet ByteString
    generalReservedWords HashSet ByteString
    commandNames

    instance CanParse Symbol where
      parse :: Parser Symbol
    parse = do
        Parser ()
    dropWhitespace
        Char
    c0 <- Parser Char
    peekChar
        if Char
    c0 Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '|' then do
          [Word8]
    r <- (Char -> Bool) -> [Word8] -> Parser [Word8]
    takeChars' (Char -> [Char] -> Bool
    forall (t :: Type -> Type) a.
    (Foldable t, Eq a) =>
    a -> t a -> Bool
    `notElem` [Char
    '|', Char
    '/']) [Char -> Word8
    c2b Char
    c0]
          Char
    ce <- Parser Char
    peekChar
          Bool -> Parser () -> Parser ()
    forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
    when (Char
    ce Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Char
    '|') (Parser () -> Parser ()) -> Parser () -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ do
            [Char] -> Parser ()
    forall a. [Char] -> Parser a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail ([Char] -> Parser ()) -> [Char] -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Unexpected character " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Char -> [Char]
    forall a. Show a => a -> [Char]
    show Char
    ce [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " inside symbol."
          Symbol -> Parser Symbol
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (Symbol -> Parser Symbol) -> Symbol -> Parser Symbol
    forall a b. (a -> b) -> a -> b
    $! ByteString -> Symbol
    Symbol ([Word8] -> ByteString
    BS.pack ([Word8] -> ByteString) -> [Word8] -> ByteString
    forall a b. (a -> b) -> a -> b
    $ [Word8] -> [Word8]
    forall a. [a] -> [a]
    reverse (Char -> Word8
    c2b Char
    ceWord8 -> [Word8] -> [Word8]
    forall a. a -> [a] -> [a]
    :[Word8]
    r))
         else if Char -> HashSet Char -> Bool
    forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
    HSet.member Char
    c0 HashSet Char
    initialSymbolCharSet then do
          ByteString
    r <- [Word8] -> ByteString
    BS.pack ([Word8] -> ByteString)
    -> ([Word8] -> [Word8]) -> [Word8] -> ByteString
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Word8] -> [Word8]
    forall a. [a] -> [a]
    reverse ([Word8] -> ByteString) -> Parser [Word8] -> Parser ByteString
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Char -> Bool) -> [Word8] -> Parser [Word8]
    takeChars' (Char -> HashSet Char -> Bool
    forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
    `HSet.member` HashSet Char
    symbolCharSet) [Char -> Word8
    c2b Char
    c0]
          Bool -> Parser () -> Parser ()
    forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
    when (ByteString -> HashSet ByteString -> Bool
    forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
    HSet.member ByteString
    r HashSet ByteString
    reservedWords) (Parser () -> Parser ()) -> Parser () -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ do
            [Char] -> Parser ()
    forall a. [Char] -> Parser a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail ([Char] -> Parser ()) -> [Char] -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Symbol cannot be reserved word " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ByteString -> [Char]
    forall a. Show a => a -> [Char]
    show ByteString
    r
          Symbol -> Parser Symbol
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (Symbol -> Parser Symbol) -> Symbol -> Parser Symbol
    forall a b. (a -> b) -> a -> b
    $! ByteString -> Symbol
    Symbol ByteString
    r
         else do
          [Char] -> Parser Symbol
    forall a. [Char] -> Parser a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail ([Char] -> Parser Symbol) -> [Char] -> Parser Symbol
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Unexpected character " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Char -> [Char]
    forall a. Show a => a -> [Char]
    show Char
    c0 [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " starting symbol."

    -- | This skips whitespace than reads in the next alphabetic or dash
    -- characters.
    matchApp :: [(BS.ByteString, Parser a)] -> Parser a
    matchApp :: forall a. [(ByteString, Parser a)] -> Parser a
    matchApp [(ByteString, Parser a)]
    actions = do
      Parser ()
    dropWhitespace
      let allowedChar :: Char -> Bool
    allowedChar Char
    c = Char
    'A' Char -> Char -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Char
    c Bool -> Bool -> Bool
    && Char
    c Char -> Char -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Char
    'Z' Bool -> Bool -> Bool
    || Char
    'a' Char -> Char -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Char
    c Bool -> Bool -> Bool
    && Char
    c Char -> Char -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Char
    'z' Bool -> Bool -> Bool
    || Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '-'
      ByteString
    w <- (Char -> Bool) -> Parser ByteString
    takeChars Char -> Bool
    allowedChar
      case ((ByteString, Parser a) -> Bool)
    -> [(ByteString, Parser a)] -> [(ByteString, Parser a)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (\(ByteString
    m,Parser a
    _p) -> ByteString
    m ByteString -> ByteString -> Bool
    forall a. Eq a => a -> a -> Bool
    == ByteString
    w) [(ByteString, Parser a)]
    actions of
        [] -> do
          ByteString
    w' <- (Char -> Bool) -> Parser ByteString
    takeChars (\Char
    c -> Char
    c Char -> [Char] -> Bool
    forall (t :: Type -> Type) a.
    (Foldable t, Eq a) =>
    a -> t a -> Bool
    `notElem` [Char
    '\r', Char
    '\n'])
          [Char] -> Parser a
    forall a. [Char] -> Parser a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail ([Char] -> Parser a) -> [Char] -> Parser a
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Unsupported keyword: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ByteString -> [Char]
    UTF8.toString (ByteString
    w ByteString -> ByteString -> ByteString
    forall a. Semigroup a => a -> a -> a
    <> ByteString
    w')
        [(ByteString
    _,Parser a
    p)] -> Parser a
    p
        (ByteString, Parser a)
    _:(ByteString, Parser a)
    _:[(ByteString, Parser a)]
    _ -> [Char] -> Parser a
    forall a. [Char] -> Parser a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail ([Char] -> Parser a) -> [Char] -> Parser a
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "internal error: Duplicate keywords " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ByteString -> [Char]
    forall a. Show a => a -> [Char]
    show ByteString
    w

    openParen :: Parser ()
    openParen :: Parser ()
    openParen = Char -> Parser ()
    matchChar Char
    '('

    closeParen :: Parser ()
    closeParen :: Parser ()
    closeParen = Char -> Parser ()
    matchChar Char
    ')'

    -- | Read in whitespace, and then if next character is a paren
    checkParen :: Parser Bool
    checkParen :: Parser Bool
    checkParen = do
      Char
    c <- Parser Char
    peekChar
      if Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '(' then
        Parser ()
    dropChar Parser () -> Parser Bool -> Parser Bool
    forall a b. Parser a -> Parser b -> Parser b
    forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
    >> Bool -> Parser Bool
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure Bool
    True
       else if Char -> Bool
    isSpace Char
    c then
        Parser Char
    parseChar Parser Char -> Parser Bool -> Parser Bool
    forall a b. Parser a -> Parser b -> Parser b
    forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
    >> Parser Bool
    checkParen
       else
        Bool -> Parser Bool
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure Bool
    False

    -- | An SMT sort.
    data Sort
      = Sort Symbol [Sort]
        -- ^ A named sort with the given arguments.
      | BitVec !Integer
        -- ^ A bitvector with the given width.
      | FloatingPoint !Integer !Integer
        -- ^ floating point with exponent bits followed by significand bit.

    pattern Bool :: Sort
    pattern $mBool :: forall {r}. Sort -> ((# #) -> r) -> ((# #) -> r) -> r
    $bBool :: Sort
    Bool = Sort "Bool" []

    pattern Int :: Sort
    pattern $mInt :: forall {r}. Sort -> ((# #) -> r) -> ((# #) -> r) -> r
    $bInt :: Sort
    Int = Sort "Int" []

    pattern Real :: Sort
    pattern $mReal :: forall {r}. Sort -> ((# #) -> r) -> ((# #) -> r) -> r
    $bReal :: Sort
    Real = Sort "Real" []

    pattern RoundingMode :: Sort
    pattern $mRoundingMode :: forall {r}. Sort -> ((# #) -> r) -> ((# #) -> r) -> r
    $bRoundingMode :: Sort
    RoundingMode = Sort "RoundingMode" []

    pattern Array :: Sort -> Sort -> Sort
    pattern $mArray :: forall {r}. Sort -> (Sort -> Sort -> r) -> ((# #) -> r) -> r
    $bArray :: Sort -> Sort -> Sort
    Array x y = Sort "Array" [x,y]

    parseDecimal' :: Integer -> Parser Integer
    parseDecimal' :: Integer -> Parser Integer
    parseDecimal' Integer
    cur = do
      Char
    c <- Parser Char
    peekChar
      if Char
    '0' Char -> Char -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Char
    c Bool -> Bool -> Bool
    && Char
    c Char -> Char -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Char
    '9' then do
        Parser ()
    dropChar
        Integer -> Parser Integer
    parseDecimal' (Integer -> Parser Integer) -> Integer -> Parser Integer
    forall a b. (a -> b) -> a -> b
    $! Integer
    10 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    cur Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (Char -> Int
    forall a. Enum a => a -> Int
    fromEnum Char
    c Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Char -> Int
    forall a. Enum a => a -> Int
    fromEnum Char
    '0')
       else
        Integer -> Parser Integer
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure Integer
    cur

    -- | Parse the next characters as a decimal number.
    --
    -- Note. No whitespace may proceed the number.
    parseDecimal ::Parser Integer
    parseDecimal :: Parser Integer
    parseDecimal = Integer -> Parser Integer
    parseDecimal' Integer
    0

    instance CanParse Integer where
      parse :: Parser Integer
    parse = Parser ()
    dropWhitespace Parser () -> Parser Integer -> Parser Integer
    forall a b. Parser a -> Parser b -> Parser b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> Parser Integer
    parseDecimal

    instance CanParse Sort where
      parse :: Parser Sort
    parse = do
        Bool
    isParen <- Parser Bool
    checkParen
        if Bool
    isParen then do
          Symbol
    sym <- Parser Symbol
    forall a. CanParse a => Parser a
    parse
          if Symbol
    sym Symbol -> Symbol -> Bool
    forall a. Eq a => a -> a -> Bool
    == Symbol
    "_" then do
            Sort
    r <- [(ByteString, Parser Sort)] -> Parser Sort
    forall a. [(ByteString, Parser a)] -> Parser a
    matchApp [ (,) ByteString
    "BitVec" (Integer -> Sort
    BitVec (Integer -> Sort) -> Parser Integer -> Parser Sort
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser Integer
    forall a. CanParse a => Parser a
    parse)
                          , (,) ByteString
    "FloatingPoint" (Integer -> Integer -> Sort
    FloatingPoint (Integer -> Integer -> Sort)
    -> Parser Integer -> Parser (Integer -> Sort)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser Integer
    forall a. CanParse a => Parser a
    parse Parser (Integer -> Sort) -> Parser Integer -> Parser Sort
    forall a b. Parser (a -> b) -> Parser a -> Parser b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> Parser Integer
    forall a. CanParse a => Parser a
    parse)
                          ]
            Parser ()
    closeParen
            Sort -> Parser Sort
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure Sort
    r
           else
            Symbol -> [Sort] -> Sort
    Sort Symbol
    sym ([Sort] -> Sort) -> Parser [Sort] -> Parser Sort
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser Sort -> Parser [Sort]
    forall a. Parser a -> Parser [a]
    parseUntilCloseParen Parser Sort
    forall a. CanParse a => Parser a
    parse
         else do
          Symbol
    sym <- Parser Symbol
    forall a. CanParse a => Parser a
    parse
          Sort -> Parser Sort
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (Sort -> Parser Sort) -> Sort -> Parser Sort
    forall a b. (a -> b) -> a -> b
    $! Symbol -> [Sort] -> Sort
    Sort Symbol
    sym []

    -- | This denotes an SMTLIB term over a fixed vocabulary.
    data Term
       = SymbolTerm !Symbol
       | AsConst !Sort !Term
       | BVTerm !Integer !Integer
       | IntTerm !Integer
         -- ^ @IntTerm v@ denotes the SMTLIB expression @v@ if @v >= 0@ and @(- `(negate v))
         -- otherwise.
       | RatTerm !Rational
         -- ^ @RatTerm r@ denotes the SMTLIB expression @(/ `(numerator r) `(denomator r))@.
       | StoreTerm !Term !Term !Term
         -- ^ @StoreTerm a i v@ denotes the SMTLIB expression @(store a i v)@.
       | IfEqTerm !Symbol !Term !Term !Term
         -- ^ @IfEqTerm v c t f@ denotes the SMTLIB expression @(ite (= v c) t f)@.

    parseIntegerTerm :: Parser Integer
    parseIntegerTerm :: Parser Integer
    parseIntegerTerm = do
      Bool
    isParen <- Parser Bool
    checkParen
      if Bool
    isParen then do
        ByteString -> Parser ()
    matchString ByteString
    "-"
        Integer
    r <- Parser Integer
    forall a. CanParse a => Parser a
    parse
        Parser ()
    closeParen
        Integer -> Parser Integer
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (Integer -> Parser Integer) -> Integer -> Parser Integer
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    r
       else do
        Parser Integer
    forall a. CanParse a => Parser a
    parse

    parseEq :: Parser (Symbol, Term)
    parseEq :: Parser (Symbol, Term)
    parseEq = do
      Parser ()
    openParen
      ByteString -> Parser ()
    matchString ByteString
    "="
      Symbol
    var <- Parser Symbol
    forall a. CanParse a => Parser a
    parse
      Term
    val <- Parser Term
    forall a. CanParse a => Parser a
    parse
      Parser ()
    closeParen
      (Symbol, Term) -> Parser (Symbol, Term)
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (Symbol
    var,Term
    val)

    parseTermApp :: Parser Term
    parseTermApp :: Parser Term
    parseTermApp = do
      Parser ()
    dropWhitespace
      -- Look for (as const tp) as argument
      Bool
    isParen <- Parser Bool
    checkParen
      if Bool
    isParen then do
        ByteString -> Parser ()
    matchString ByteString
    "as"
        ByteString -> Parser ()
    matchString ByteString
    "const"
        Term
    r <- Sort -> Term -> Term
    AsConst (Sort -> Term -> Term) -> Parser Sort -> Parser (Term -> Term)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser Sort
    forall a. CanParse a => Parser a
    parse Parser (Term -> Term) -> Parser Term -> Parser Term
    forall a b. Parser (a -> b) -> Parser a -> Parser b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> Parser Term
    forall a. CanParse a => Parser a
    parse
        Parser ()
    closeParen
        Term -> Parser Term
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (Term -> Parser Term) -> Term -> Parser Term
    forall a b. (a -> b) -> a -> b
    $! Term
    r
       else do
        Symbol
    op <- Parser Symbol
    forall a. CanParse a => Parser a
    parse :: Parser Symbol
        case Symbol
    op of
          Symbol
    "_" -> do
            ByteString -> Parser ()
    matchString ByteString
    "bv"
            Integer -> Integer -> Term
    BVTerm (Integer -> Integer -> Term)
    -> Parser Integer -> Parser (Integer -> Term)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser Integer
    parseDecimal Parser (Integer -> Term) -> Parser Integer -> Parser Term
    forall a b. Parser (a -> b) -> Parser a -> Parser b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> Parser Integer
    forall a. CanParse a => Parser a
    parse
          Symbol
    "/" -> do
            Integer
    num <- Parser Integer
    parseIntegerTerm
            Integer
    den <- Parser Integer
    forall a. CanParse a => Parser a
    parse
            Bool -> Parser () -> Parser ()
    forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
    when (Integer
    den Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0) (Parser () -> Parser ()) -> Parser () -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Parser ()
    forall a. [Char] -> Parser a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail ([Char] -> Parser ()) -> [Char] -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Model contains divide-by-zero"
            Term -> Parser Term
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (Term -> Parser Term) -> Term -> Parser Term
    forall a b. (a -> b) -> a -> b
    $ Rational -> Term
    RatTerm (Integer
    num Integer -> Integer -> Rational
    forall a. Integral a => a -> a -> Ratio a
    % Integer
    den)
          Symbol
    "-" -> do
            Integer -> Term
    IntTerm (Integer -> Term) -> (Integer -> Integer) -> Integer -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer
    forall a. Num a => a -> a
    negate (Integer -> Term) -> Parser Integer -> Parser Term
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser Integer
    forall a. CanParse a => Parser a
    parse
          Symbol
    "store" ->
            Term -> Term -> Term -> Term
    StoreTerm (Term -> Term -> Term -> Term)
    -> Parser Term -> Parser (Term -> Term -> Term)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser Term
    forall a. CanParse a => Parser a
    parse Parser (Term -> Term -> Term)
    -> Parser Term -> Parser (Term -> Term)
    forall a b. Parser (a -> b) -> Parser a -> Parser b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> Parser Term
    forall a. CanParse a => Parser a
    parse Parser (Term -> Term) -> Parser Term -> Parser Term
    forall a b. Parser (a -> b) -> Parser a -> Parser b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> Parser Term
    forall a. CanParse a => Parser a
    parse
          Symbol
    "ite" -> do
            (Symbol
    var,Term
    val) <- Parser (Symbol, Term)
    parseEq
            Term
    t <- Parser Term
    forall a. CanParse a => Parser a
    parse
            Term
    f <- Parser Term
    forall a. CanParse a => Parser a
    parse
            Term -> Parser Term
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (Term -> Parser Term) -> Term -> Parser Term
    forall a b. (a -> b) -> a -> b
    $ Symbol -> Term -> Term -> Term -> Term
    IfEqTerm Symbol
    var Term
    val Term
    t Term
    f
          Symbol
    _ -> do
            [Char] -> Parser Term
    forall a. [Char] -> Parser a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail ([Char] -> Parser Term) -> [Char] -> Parser Term
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Unsupported operator symbol " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Symbol -> [Char]
    forall a. Show a => a -> [Char]
    show Symbol
    op

    instance CanParse Term where
      parse :: Parser Term
    parse = do
        Parser ()
    dropWhitespace
        Char
    c <- Parser Char
    peekChar
        if Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '(' then do
          Term
    t <- Parser Term
    parseTermApp
          Parser ()
    closeParen
          Term -> Parser Term
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (Term -> Parser Term) -> Term -> Parser Term
    forall a b. (a -> b) -> a -> b
    $! Term
    t
         else if Char -> Bool
    isDigit Char
    c then
          Integer -> Term
    IntTerm (Integer -> Term) -> Parser Integer -> Parser Term
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser Integer
    parseDecimal
         else if Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '@' then
          Symbol -> Term
    SymbolTerm (Symbol -> Term) -> Parser Symbol -> Parser Term
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser Symbol
    forall a. CanParse a => Parser a
    parse
         else
          [Char] -> Parser Term
    forall a. [Char] -> Parser a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail ([Char] -> Parser Term) -> [Char] -> Parser Term
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Could not parse term"

    data DefineFun = DefineFun { DefineFun -> Symbol
    funSymbol :: !Symbol
                               , DefineFun -> [(Symbol, Sort)]
    funArgs :: ![(Symbol, Sort)]
                               , DefineFun -> Sort
    funResultSort :: !Sort
                               , DefineFun -> Term
    funDef :: !Term
                               }

    -- | A line in the model response
    data ModelResponse
       = DeclareSortResponse !Symbol !Integer
       | DefineFunResponse !DefineFun

    parseSortedVar :: Parser (Symbol, Sort)
    parseSortedVar :: Parser (Symbol, Sort)
    parseSortedVar = Parser ()
    openParen Parser () -> Parser (Symbol, Sort) -> Parser (Symbol, Sort)
    forall a b. Parser a -> Parser b -> Parser b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> ((,) (Symbol -> Sort -> (Symbol, Sort))
    -> Parser Symbol -> Parser (Sort -> (Symbol, Sort))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser Symbol
    forall a. CanParse a => Parser a
    parse Parser (Sort -> (Symbol, Sort))
    -> Parser Sort -> Parser (Symbol, Sort)
    forall a b. Parser (a -> b) -> Parser a -> Parser b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> Parser Sort
    forall a. CanParse a => Parser a
    parse) Parser (Symbol, Sort) -> Parser () -> Parser (Symbol, Sort)
    forall a b. Parser a -> Parser b -> Parser a
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f a
    <* Parser ()
    closeParen

    -- | Parses ⟨symbol⟩ ( ⟨sorted_var⟩* ) ⟨sort⟩ ⟨term⟩
    parseDefineFun :: Parser DefineFun
    parseDefineFun :: Parser DefineFun
    parseDefineFun = do
      Symbol
    sym <- Parser Symbol
    forall a. CanParse a => Parser a
    parse
      [(Symbol, Sort)]
    args <- Parser ()
    openParen Parser () -> Parser [(Symbol, Sort)] -> Parser [(Symbol, Sort)]
    forall a b. Parser a -> Parser b -> Parser b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> Parser (Symbol, Sort) -> Parser [(Symbol, Sort)]
    forall a. Parser a -> Parser [a]
    parseUntilCloseParen Parser (Symbol, Sort)
    parseSortedVar
      Sort
    res <- Parser Sort
    forall a. CanParse a => Parser a
    parse
      Term
    def <- Parser Term
    forall a. CanParse a => Parser a
    parse
      DefineFun -> Parser DefineFun
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (DefineFun -> Parser DefineFun) -> DefineFun -> Parser DefineFun
    forall a b. (a -> b) -> a -> b
    $! DefineFun { funSymbol :: Symbol
    funSymbol = Symbol
    sym
                        , funArgs :: [(Symbol, Sort)]
    funArgs = [(Symbol, Sort)]
    args
                        , funResultSort :: Sort
    funResultSort = Sort
    res
                        , funDef :: Term
    funDef = Term
    def
                        }

    instance CanParse ModelResponse where
      parse :: Parser ModelResponse
    parse = do
        Parser ()
    openParen
        ModelResponse
    r <- [(ByteString, Parser ModelResponse)] -> Parser ModelResponse
    forall a. [(ByteString, Parser a)] -> Parser a
    matchApp [ (,) ByteString
    "declare-sort"    (Parser ModelResponse -> (ByteString, Parser ModelResponse))
    -> Parser ModelResponse -> (ByteString, Parser ModelResponse)
    forall a b. (a -> b) -> a -> b
    $ Symbol -> Integer -> ModelResponse
    DeclareSortResponse (Symbol -> Integer -> ModelResponse)
    -> Parser Symbol -> Parser (Integer -> ModelResponse)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser Symbol
    forall a. CanParse a => Parser a
    parse Parser (Integer -> ModelResponse)
    -> Parser Integer -> Parser ModelResponse
    forall a b. Parser (a -> b) -> Parser a -> Parser b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> Parser Integer
    forall a. CanParse a => Parser a
    parse
                      , (,) ByteString
    "define-fun"      (Parser ModelResponse -> (ByteString, Parser ModelResponse))
    -> Parser ModelResponse -> (ByteString, Parser ModelResponse)
    forall a b. (a -> b) -> a -> b
    $ DefineFun -> ModelResponse
    DefineFunResponse (DefineFun -> ModelResponse)
    -> Parser DefineFun -> Parser ModelResponse
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser DefineFun
    parseDefineFun
                      , (,) ByteString
    "define-fun-rec"  (Parser ModelResponse -> (ByteString, Parser ModelResponse))
    -> Parser ModelResponse -> (ByteString, Parser ModelResponse)
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Parser ModelResponse
    forall a. [Char] -> Parser a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail [Char]
    "Do not yet support define-fun-rec"
                      , (,) ByteString
    "define-funs-rec" (Parser ModelResponse -> (ByteString, Parser ModelResponse))
    -> Parser ModelResponse -> (ByteString, Parser ModelResponse)
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Parser ModelResponse
    forall a. [Char] -> Parser a
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
    fail [Char]
    "Do not yet support define-funs-rec"
                      ]
        Parser ()
    closeParen
        ModelResponse -> Parser ModelResponse
    forall a. a -> Parser a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (ModelResponse -> Parser ModelResponse)
    -> ModelResponse -> Parser ModelResponse
    forall a b. (a -> b) -> a -> b
    $! ModelResponse
    r

    -- | The parsed declarations and definitions returned by "(get-model)"
    type GetModelResponse = [ModelResponse]

    -- | This reads the model response from a "(get-model)" request.
    readGetModelResponse :: Handle -> IO GetModelResponse
    readGetModelResponse :: Handle -> IO GetModelResponse
    readGetModelResponse Handle
    h =
      Handle -> Parser GetModelResponse -> IO GetModelResponse
    forall a. Handle -> Parser a -> IO a
    runParser Handle
    h (Parser GetModelResponse -> IO GetModelResponse)
    -> Parser GetModelResponse -> IO GetModelResponse
    forall a b. (a -> b) -> a -> b
    $
        Parser ()
    openParen Parser () -> Parser GetModelResponse -> Parser GetModelResponse
    forall a b. Parser a -> Parser b -> Parser b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> Parser ModelResponse -> Parser GetModelResponse
    forall a. Parser a -> Parser [a]
    parseUntilCloseParen Parser ModelResponse
    forall a. CanParse a => Parser a
    parse