    {-# LANGUAGE Safe #-}
    {-# LANGUAGE RecordWildCards #-}
    {-# LANGUAGE PatternGuards #-}
    -- | A module for interacting with an SMT solver, using SmtLib-2 format.
    module SimpleSMT
      (
        -- * Basic Solver Interface
        Solver(..)
      , newSolver
      , newSolverNotify
      , ackCommand
      , simpleCommand
      , simpleCommandMaybe
      , loadFile
      , loadString

        -- ** S-Expressions
      , SExpr(..)
      , showsSExpr, ppSExpr, readSExpr

        -- ** Logging and Debugging
      , Logger(..)
      , newLogger
      , withLogLevel
      , logMessageAt
      , logIndented

        -- * Common SmtLib-2 Commands
      , setLogic, setLogicMaybe
      , setOption, setOptionMaybe
      , produceUnsatCores
      , named
      , push, pushMany
      , pop, popMany
      , inNewScope
      , declare
      , declareFun
      , declareDatatype
      , define
      , defineFun
      , defineFunRec
      , defineFunsRec
      , assert
      , check
      , Result(..)
      , getExprs, getExpr
      , getConsts, getConst
      , getUnsatCore
      , Value(..)
      , sexprToVal

        -- * Convenience Functions for SmtLib-2 Expressions
      , fam
      , fun
      , const
      , app

        -- * Convenience Functions for SmtLib-2 identifiers
      , quoteSymbol
      , symbol
      , keyword
      , as

        -- ** Types
      , tInt
      , tBool
      , tReal
      , tArray
      , tBits

        -- ** Literals
      , int
      , real
      , bool
      , bvBin
      , bvHex
      , value

        -- ** Connectives
      , not
      , and
      , andMany
      , or
      , orMany
      , xor
      , implies

        -- ** If-then-else
      , ite

        -- ** Relational Predicates
      , eq
      , distinct
      , gt
      , lt
      , geq
      , leq
      , bvULt
      , bvULeq
      , bvSLt
      , bvSLeq

        -- ** Arithmetic
      , add
      , addMany
      , sub
      , neg
      , mul
      , abs
      , div
      , mod
      , divisible
      , realDiv
      , toInt
      , toReal

        -- ** Bit Vectors
      , concat
      , extract
      , bvNot
      , bvNeg
      , bvAnd
      , bvXOr
      , bvOr
      , bvAdd
      , bvSub
      , bvMul
      , bvUDiv
      , bvURem
      , bvSDiv
      , bvSRem
      , bvShl
      , bvLShr
      , bvAShr
      , signExtend
      , zeroExtend

        -- ** Arrays
      , select
      , store
      ) where

    import Prelude hiding (not, and, or, abs, div, mod, concat, const)
    import qualified Prelude as P
    import Data.Char(isSpace, isDigit)
    import Data.List(unfoldr,intersperse)
    import Data.Bits(testBit)
    import Data.IORef(newIORef, atomicModifyIORef, modifyIORef', readIORef,
                      writeIORef)
    import System.Process(runInteractiveProcess, waitForProcess)
    import System.IO (hFlush, hGetLine, hGetContents, hPutStrLn, stdout, hClose)
    import System.Exit(ExitCode)
    import qualified Control.Exception as X
    import Control.Concurrent(forkIO)
    import Control.Monad(forever,when,void)
    import Text.Read(readMaybe)
    import Data.Ratio((%), numerator, denominator)
    import Numeric(showHex, readHex, showFFloat)

    -- | Results of checking for satisfiability.
    data Result = Sat         -- ^ The assertions are satisfiable
                | Unsat       -- ^ The assertions are unsatisfiable
                | Unknown     -- ^ The result is inconclusive
                  deriving (Result -> Result -> Bool
    (Result -> Result -> Bool)
    -> (Result -> Result -> Bool) -> Eq Result
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Result -> Result -> Bool
    == :: Result -> Result -> Bool
    $c/= :: Result -> Result -> Bool
    /= :: Result -> Result -> Bool
    Eq,Int -> Result -> ShowS
    [Result] -> ShowS
    Result -> String
    (Int -> Result -> ShowS)
    -> (Result -> String) -> ([Result] -> ShowS) -> Show Result
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Result -> ShowS
    showsPrec :: Int -> Result -> ShowS
    $cshow :: Result -> String
    show :: Result -> String
    $cshowList :: [Result] -> ShowS
    showList :: [Result] -> ShowS
    Show)

    -- | Common values returned by SMT solvers.
    data Value =  Bool  !Bool           -- ^ Boolean value
                | Int   !Integer        -- ^ Integral value
                | Real  !Rational       -- ^ Rational value
                | Bits  !Int !Integer   -- ^ Bit vector: width, value
                | Other !SExpr          -- ^ Some other value
                  deriving (Value -> Value -> Bool
    (Value -> Value -> Bool) -> (Value -> Value -> Bool) -> Eq Value
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Value -> Value -> Bool
    == :: Value -> Value -> Bool
    $c/= :: Value -> Value -> Bool
    /= :: Value -> Value -> Bool
    Eq,Int -> Value -> ShowS
    [Value] -> ShowS
    Value -> String
    (Int -> Value -> ShowS)
    -> (Value -> String) -> ([Value] -> ShowS) -> Show Value
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Value -> ShowS
    showsPrec :: Int -> Value -> ShowS
    $cshow :: Value -> String
    show :: Value -> String
    $cshowList :: [Value] -> ShowS
    showList :: [Value] -> ShowS
    Show)

    -- | S-expressions. These are the basic format for SmtLib-2.
    data SExpr  = Atom String
                | List [SExpr]
                  deriving (SExpr -> SExpr -> Bool
    (SExpr -> SExpr -> Bool) -> (SExpr -> SExpr -> Bool) -> Eq SExpr
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: SExpr -> SExpr -> Bool
    == :: SExpr -> SExpr -> Bool
    $c/= :: SExpr -> SExpr -> Bool
    /= :: SExpr -> SExpr -> Bool
    Eq, Eq SExpr
    Eq SExpr =>
    (SExpr -> SExpr -> Ordering)
    -> (SExpr -> SExpr -> Bool)
    -> (SExpr -> SExpr -> Bool)
    -> (SExpr -> SExpr -> Bool)
    -> (SExpr -> SExpr -> Bool)
    -> (SExpr -> SExpr -> SExpr)
    -> (SExpr -> SExpr -> SExpr)
    -> Ord SExpr
    SExpr -> SExpr -> Bool
    SExpr -> SExpr -> Ordering
    SExpr -> SExpr -> SExpr
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: SExpr -> SExpr -> Ordering
    compare :: SExpr -> SExpr -> Ordering
    $c< :: SExpr -> SExpr -> Bool
    < :: SExpr -> SExpr -> Bool
    $c<= :: SExpr -> SExpr -> Bool
    <= :: SExpr -> SExpr -> Bool
    $c> :: SExpr -> SExpr -> Bool
    > :: SExpr -> SExpr -> Bool
    $c>= :: SExpr -> SExpr -> Bool
    >= :: SExpr -> SExpr -> Bool
    $cmax :: SExpr -> SExpr -> SExpr
    max :: SExpr -> SExpr -> SExpr
    $cmin :: SExpr -> SExpr -> SExpr
    min :: SExpr -> SExpr -> SExpr
    Ord, Int -> SExpr -> ShowS
    [SExpr] -> ShowS
    SExpr -> String
    (Int -> SExpr -> ShowS)
    -> (SExpr -> String) -> ([SExpr] -> ShowS) -> Show SExpr
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> SExpr -> ShowS
    showsPrec :: Int -> SExpr -> ShowS
    $cshow :: SExpr -> String
    show :: SExpr -> String
    $cshowList :: [SExpr] -> ShowS
    showList :: [SExpr] -> ShowS
    Show)

    -- | Show an s-expression.
    showsSExpr :: SExpr -> ShowS
    showsSExpr :: SExpr -> ShowS
    showsSExpr SExpr
    ex =
      case SExpr
    ex of
        Atom String
    x  -> String -> ShowS
    showString String
    x
        List [SExpr]
    es -> Char -> ShowS
    showChar Char
    '(' ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                    (SExpr -> ShowS -> ShowS) -> ShowS -> [SExpr] -> ShowS
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\SExpr
    e ShowS
    m -> SExpr -> ShowS
    showsSExpr SExpr
    e ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Char -> ShowS
    showChar Char
    ' ' ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ShowS
    m)
                    (Char -> ShowS
    showChar Char
    ')') [SExpr]
    es

    -- | Show an S-expression in a somewhat readbale fashion.
    ppSExpr :: SExpr -> ShowS
    ppSExpr :: SExpr -> ShowS
    ppSExpr = Int -> SExpr -> ShowS
    go Int
    0
      where
      tab :: Int -> ShowS
    tab Int
    n = String -> ShowS
    showString (Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate Int
    n Char
    ' ')
      many :: [b -> b] -> b -> b
    many  = ((b -> b) -> (b -> b) -> b -> b) -> (b -> b) -> [b -> b] -> b -> b
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (b -> b) -> (b -> b) -> b -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    (.) b -> b
    forall a. a -> a
    id

      new :: Int -> SExpr -> ShowS
    new Int
    n SExpr
    e = Char -> ShowS
    showChar Char
    '\n' ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> ShowS
    tab Int
    n ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> SExpr -> ShowS
    go Int
    n SExpr
    e

      small :: t -> [SExpr] -> Maybe [ShowS]
    small t
    n [SExpr]
    es =
        case [SExpr]
    es of
          [] -> [ShowS] -> Maybe [ShowS]
    forall a. a -> Maybe a
    Just []
          SExpr
    e : [SExpr]
    more
            | t
    n t -> t -> Bool
    forall a. Ord a => a -> a -> Bool
    <= t
    0 -> Maybe [ShowS]
    forall a. Maybe a
    Nothing
            | Bool
    otherwise -> case SExpr
    e of
                             Atom String
    x -> (String -> ShowS
    showString String
    x ShowS -> [ShowS] -> [ShowS]
    forall a. a -> [a] -> [a]
    :) ([ShowS] -> [ShowS]) -> Maybe [ShowS] -> Maybe [ShowS]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> t -> [SExpr] -> Maybe [ShowS]
    small (t
    nt -> t -> t
    forall a. Num a => a -> a -> a
    -t
    1) [SExpr]
    more
                             SExpr
    _      -> Maybe [ShowS]
    forall a. Maybe a
    Nothing

      go :: Int -> SExpr -> ShowS
      go :: Int -> SExpr -> ShowS
    go Int
    n SExpr
    ex =
        case SExpr
    ex of
          Atom String
    x        -> String -> ShowS
    showString String
    x
          List [SExpr]
    es
            | Just [ShowS]
    fs <- Integer -> [SExpr] -> Maybe [ShowS]
    forall {t}. (Ord t, Num t) => t -> [SExpr] -> Maybe [ShowS]
    small Integer
    5 [SExpr]
    es ->
              Char -> ShowS
    showChar Char
    '(' ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [ShowS] -> ShowS
    forall {b}. [b -> b] -> b -> b
    many (ShowS -> [ShowS] -> [ShowS]
    forall a. a -> [a] -> [a]
    intersperse (Char -> ShowS
    showChar Char
    ' ') [ShowS]
    fs) ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Char -> ShowS
    showChar Char
    ')'

          List (Atom String
    x : [SExpr]
    es) -> String -> ShowS
    showString String
    "(" ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> ShowS
    showString String
    x ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                                    [ShowS] -> ShowS
    forall {b}. [b -> b] -> b -> b
    many ((SExpr -> ShowS) -> [SExpr] -> [ShowS]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> SExpr -> ShowS
    new (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    3)) [SExpr]
    es) ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> ShowS
    showString String
    ")"

          List [SExpr]
    es -> String -> ShowS
    showString String
    "(" ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [ShowS] -> ShowS
    forall {b}. [b -> b] -> b -> b
    many ((SExpr -> ShowS) -> [SExpr] -> [ShowS]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> SExpr -> ShowS
    new (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    2)) [SExpr]
    es) ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> ShowS
    showString String
    ")"

    -- | Parse an s-expression.
    readSExpr :: String -> Maybe (SExpr, String)
    readSExpr :: String -> Maybe (SExpr, String)
    readSExpr (Char
    c : String
    more) | Char -> Bool
    isSpace Char
    c = String -> Maybe (SExpr, String)
    readSExpr String
    more
    readSExpr (Char
    ';' : String
    more) = String -> Maybe (SExpr, String)
    readSExpr (String -> Maybe (SExpr, String))
    -> String -> Maybe (SExpr, String)
    forall a b. (a -> b) -> a -> b
    $ Int -> ShowS
    forall a. Int -> [a] -> [a]
    drop Int
    1 ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ (Char -> Bool) -> ShowS
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Char
    '\n') String
    more
    readSExpr (Char
    '|' : String
    more) = do (sym, '|' : rest) <- (String, String) -> Maybe (String, String)
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ((Char -> Bool) -> String -> (String, String)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    span (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    (/=) Char
    '|') String
    more)
                                Just (Atom ('|' : sym ++ ['|']), rest)
    readSExpr (Char
    '(' : String
    more) = do (xs,more1) <- String -> Maybe ([SExpr], String)
    list String
    more
                                return (List xs, more1)
      where
      list :: String -> Maybe ([SExpr], String)
    list (Char
    c : String
    txt) | Char -> Bool
    isSpace Char
    c = String -> Maybe ([SExpr], String)
    list String
    txt
      list (Char
    ')' : String
    txt) = ([SExpr], String) -> Maybe ([SExpr], String)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([], String
    txt)
      list String
    txt         = do (v,txt1) <- String -> Maybe (SExpr, String)
    readSExpr String
    txt
                            (vs,txt2) <- list txt1
                            return (v:vs, txt2)
    readSExpr String
    txt     = case (Char -> Bool) -> String -> (String, String)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    break Char -> Bool
    end String
    txt of
                           (String
    as,String
    bs) | Bool -> Bool
    P.not (String -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null String
    as) -> (SExpr, String) -> Maybe (SExpr, String)
    forall a. a -> Maybe a
    Just (String -> SExpr
    Atom String
    as, String
    bs)
                           (String, String)
    _ -> Maybe (SExpr, String)
    forall a. Maybe a
    Nothing
      where end :: Char -> Bool
    end Char
    x = Char
    x Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    ')' Bool -> Bool -> Bool
    || Char -> Bool
    isSpace Char
    x

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

    -- | An interactive solver process.
    data Solver = Solver
      { Solver -> SExpr -> IO SExpr
    command   :: SExpr -> IO SExpr
        -- ^ Send a command to the solver.

      , Solver -> IO ExitCode
    stop :: IO ExitCode
        -- ^ Terminate the solver.
      }

    -- | Start a new solver process.
    newSolver :: String       {- ^ Executable -}            ->
                 [String]     {- ^ Arguments -}             ->
                 Maybe Logger {- ^ Optional logging here -} ->
                 IO Solver
    newSolver :: String -> [String] -> Maybe Logger -> IO Solver
    newSolver String
    n [String]
    xs Maybe Logger
    l = String
    -> [String]
    -> Maybe Logger
    -> Maybe (ExitCode -> IO ())
    -> IO Solver
    newSolverNotify String
    n [String]
    xs Maybe Logger
    l Maybe (ExitCode -> IO ())
    forall a. Maybe a
    Nothing

    newSolverNotify ::
      String        {- ^ Executable -}            ->
      [String]      {- ^ Arguments -}             ->
      Maybe Logger  {- ^ Optional logging here -} ->
      Maybe (ExitCode -> IO ()) {- ^ Do this when the solver exits -} ->
      IO Solver
    newSolverNotify :: String
    -> [String]
    -> Maybe Logger
    -> Maybe (ExitCode -> IO ())
    -> IO Solver
    newSolverNotify String
    exe [String]
    opts Maybe Logger
    mbLog Maybe (ExitCode -> IO ())
    mbOnExit =
      do (hIn, hOut, hErr, h) <- String
    -> [String]
    -> Maybe String
    -> Maybe [(String, String)]
    -> IO (Handle, Handle, Handle, ProcessHandle)
    runInteractiveProcess String
    exe [String]
    opts Maybe String
    forall a. Maybe a
    Nothing Maybe [(String, String)]
    forall a. Maybe a
    Nothing

         let info String
    a = case Maybe Logger
    mbLog of
                        Maybe Logger
    Nothing -> () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                        Just Logger
    l  -> Logger -> String -> IO ()
    logMessage Logger
    l String
    a

         _ <- forkIO $ forever (do errs <- hGetLine hErr
                                   info ("[stderr] " ++ errs))
                        `X.catch` \X.SomeException {} -> () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

         case mbOnExit of
           Maybe (ExitCode -> IO ())
    Nothing -> () -> IO ()
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
           Just ExitCode -> IO ()
    this -> IO ThreadId -> IO ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (IO () -> IO ThreadId
    forkIO (ExitCode -> IO ()
    this (ExitCode -> IO ()) -> IO ExitCode -> IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ProcessHandle -> IO ExitCode
    waitForProcess ProcessHandle
    h))

         getResponse <-
           do txt <- hGetContents hOut                  -- Read *all* output
              ref <- newIORef (unfoldr readSExpr txt)  -- Parse, and store result
              return $ atomicModifyIORef ref $ \[SExpr]
    xs ->
                          case [SExpr]
    xs of
                            []     -> ([SExpr]
    xs, Maybe SExpr
    forall a. Maybe a
    Nothing)
                            SExpr
    y : [SExpr]
    ys -> ([SExpr]
    ys, SExpr -> Maybe SExpr
    forall a. a -> Maybe a
    Just SExpr
    y)

         let cmd SExpr
    c = do let txt :: String
    txt = SExpr -> ShowS
    showsSExpr SExpr
    c String
    ""
                        String -> IO ()
    info (String
    "[send->] " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    txt)
                        Handle -> String -> IO ()
    hPutStrLn Handle
    hIn String
    txt
                        Handle -> IO ()
    hFlush Handle
    hIn

             command SExpr
    c =
               do SExpr -> IO ()
    cmd SExpr
    c
                  mb <- IO (Maybe SExpr)
    getResponse
                  case mb of
                    Just SExpr
    res -> do String -> IO ()
    info (String
    "[<-recv] " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> ShowS
    showsSExpr SExpr
    res String
    "")
                                   SExpr -> IO SExpr
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SExpr
    res
                    Maybe SExpr
    Nothing  -> String -> IO SExpr
    forall a. String -> IO a
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail String
    "Missing response from solver"

             stop =
               do SExpr -> IO ()
    cmd ([SExpr] -> SExpr
    List [String -> SExpr
    Atom String
    "exit"])
                    IO () -> (SomeException -> IO ()) -> IO ()
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `X.catch` (\X.SomeException{} -> () -> IO ()
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ())
                  ec <- ProcessHandle -> IO ExitCode
    waitForProcess ProcessHandle
    h
                  X.catch (do hClose hIn
                              hClose hOut
                              hClose hErr)
                          (\IOException
    ex -> String -> IO ()
    info (IOException -> String
    forall a. Show a => a -> String
    show (IOException
    ex::X.IOException)))
                  return ec

             solver = Solver { IO ExitCode
    SExpr -> IO SExpr
    command :: SExpr -> IO SExpr
    stop :: IO ExitCode
    command :: SExpr -> IO SExpr
    stop :: IO ExitCode
    .. }

         setOption solver ":print-success" "true"
         setOption solver ":produce-models" "true"

         return solver

    -- | Load the contents of a file.
    loadFile :: Solver -> FilePath -> IO ()
    loadFile :: Solver -> String -> IO ()
    loadFile Solver
    s String
    file = Solver -> String -> IO ()
    loadString Solver
    s (String -> IO ()) -> IO String -> IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< String -> IO String
    readFile String
    file

    -- | Load a raw SMT string.
    loadString :: Solver -> String -> IO ()
    loadString :: Solver -> String -> IO ()
    loadString Solver
    s String
    str = String -> IO ()
    go (ShowS
    dropComments String
    str)
      where
      go :: String -> IO ()
    go String
    txt
        | (Char -> Bool) -> String -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Char -> Bool
    isSpace String
    txt = () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        | Bool
    otherwise =
          case String -> Maybe (SExpr, String)
    readSExpr String
    txt of
            Just (SExpr
    e,String
    rest) -> Solver -> SExpr -> IO SExpr
    command Solver
    s SExpr
    e IO SExpr -> IO () -> IO ()
    forall a b. IO a -> IO b -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> String -> IO ()
    go String
    rest
            Maybe (SExpr, String)
    Nothing       -> String -> IO ()
    forall a. String -> IO a
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    "Failed to parse SMT file."
                                            , String
    txt
                                            ]

      dropComments :: ShowS
    dropComments = [String] -> String
    unlines ([String] -> String) -> (String -> [String]) -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ShowS -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map ShowS
    dropComment ([String] -> [String])
    -> (String -> [String]) -> String -> [String]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> [String]
    lines
      dropComment :: ShowS
    dropComment String
    xs = case (Char -> Bool) -> String -> (String, String)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    break (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    ';') String
    xs of
                         (String
    as,Char
    _:String
    _) -> String
    as
                         (String, String)
    _ -> String
    xs

    -- | A command with no interesting result.
    ackCommand :: Solver -> SExpr -> IO ()
    ackCommand :: Solver -> SExpr -> IO ()
    ackCommand Solver
    proc SExpr
    c =
      do res <- Solver -> SExpr -> IO SExpr
    command Solver
    proc SExpr
    c
         case res of
           Atom String
    "success" -> () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
           SExpr
    _  -> String -> IO ()
    forall a. String -> IO a
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines
                          [ String
    "Unexpected result from the SMT solver:"
                          , String
    "  Expected: success"
                          , String
    "  Result: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> ShowS
    showsSExpr SExpr
    res String
    ""
                          ]

    -- | A command entirely made out of atoms, with no interesting result.
    simpleCommand :: Solver -> [String] -> IO ()
    simpleCommand :: Solver -> [String] -> IO ()
    simpleCommand Solver
    proc = Solver -> SExpr -> IO ()
    ackCommand Solver
    proc (SExpr -> IO ()) -> ([String] -> SExpr) -> [String] -> IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [SExpr] -> SExpr
    List ([SExpr] -> SExpr) -> ([String] -> [SExpr]) -> [String] -> SExpr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String -> SExpr) -> [String] -> [SExpr]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> SExpr
    Atom

    -- | Run a command and return True if successful, and False if unsupported.
    -- This is useful for setting options that unsupported by some solvers, but used
    -- by others.
    simpleCommandMaybe :: Solver -> [String] -> IO Bool
    simpleCommandMaybe :: Solver -> [String] -> IO Bool
    simpleCommandMaybe Solver
    proc [String]
    c =
      do res <- Solver -> SExpr -> IO SExpr
    command Solver
    proc ([SExpr] -> SExpr
    List ((String -> SExpr) -> [String] -> [SExpr]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> SExpr
    Atom [String]
    c))
         case res of
           Atom String
    "success"     -> Bool -> IO Bool
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
           Atom String
    "unsupported" -> Bool -> IO Bool
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
           SExpr
    _                  -> String -> IO Bool
    forall a. String -> IO a
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail (String -> IO Bool) -> String -> IO Bool
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines
                                          [ String
    "Unexpected result from the SMT solver:"
                                          , String
    "  Expected: success or unsupported"
                                          , String
    "  Result: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> ShowS
    showsSExpr SExpr
    res String
    ""
                                          ]

    -- | Set a solver option.
    setOption :: Solver -> String -> String -> IO ()
    setOption :: Solver -> String -> String -> IO ()
    setOption Solver
    s String
    x String
    y = Solver -> [String] -> IO ()
    simpleCommand Solver
    s [ String
    "set-option", String
    x, String
    y ]

    -- | Set a solver option, returning False if the option is unsupported.
    setOptionMaybe :: Solver -> String -> String -> IO Bool
    setOptionMaybe :: Solver -> String -> String -> IO Bool
    setOptionMaybe Solver
    s String
    x String
    y = Solver -> [String] -> IO Bool
    simpleCommandMaybe Solver
    s [ String
    "set-option", String
    x, String
    y ]

    -- | Set the solver's logic.  Usually, this should be done first.
    setLogic :: Solver -> String -> IO ()
    setLogic :: Solver -> String -> IO ()
    setLogic Solver
    s String
    x = Solver -> [String] -> IO ()
    simpleCommand Solver
    s [ String
    "set-logic", String
    x ]

    -- | Set the solver's logic, returning False if the logic is unsupported.
    setLogicMaybe :: Solver -> String -> IO Bool
    setLogicMaybe :: Solver -> String -> IO Bool
    setLogicMaybe Solver
    s String
    x = Solver -> [String] -> IO Bool
    simpleCommandMaybe Solver
    s [ String
    "set-logic", String
    x ]

    -- | Request unsat cores.  Returns if the solver supports them.
    produceUnsatCores :: Solver -> IO Bool
    produceUnsatCores :: Solver -> IO Bool
    produceUnsatCores Solver
    s = Solver -> String -> String -> IO Bool
    setOptionMaybe Solver
    s String
    ":produce-unsat-cores" String
    "true"

    -- | Checkpoint state.  A special case of 'pushMany'.
    push :: Solver -> IO ()
    push :: Solver -> IO ()
    push Solver
    proc = Solver -> Integer -> IO ()
    pushMany Solver
    proc Integer
    1

    -- | Restore to last check-point.  A special case of 'popMany'.
    pop :: Solver -> IO ()
    pop :: Solver -> IO ()
    pop Solver
    proc = Solver -> Integer -> IO ()
    popMany Solver
    proc Integer
    1

    -- | Push multiple scopes.
    pushMany :: Solver -> Integer -> IO ()
    pushMany :: Solver -> Integer -> IO ()
    pushMany Solver
    proc Integer
    n = Solver -> [String] -> IO ()
    simpleCommand Solver
    proc [ String
    "push", Integer -> String
    forall a. Show a => a -> String
    show Integer
    n ]

    -- | Pop multiple scopes.
    popMany :: Solver -> Integer -> IO ()
    popMany :: Solver -> Integer -> IO ()
    popMany Solver
    proc Integer
    n = Solver -> [String] -> IO ()
    simpleCommand Solver
    proc [ String
    "pop", Integer -> String
    forall a. Show a => a -> String
    show Integer
    n ]

    -- | Execute the IO action in a new solver scope (push before, pop after)
    inNewScope :: Solver -> IO a -> IO a
    inNewScope :: forall a. Solver -> IO a -> IO a
    inNewScope Solver
    s IO a
    m =
      do Solver -> IO ()
    push Solver
    s
         IO a
    m IO a -> IO () -> IO a
    forall a b. IO a -> IO b -> IO a
    `X.finally` Solver -> IO ()
    pop Solver
    s

    -- | Declare a constant.  A common abbreviation for 'declareFun'.
    -- For convenience, returns an the declared name as a constant expression.
    declare :: Solver -> String -> SExpr -> IO SExpr
    declare :: Solver -> String -> SExpr -> IO SExpr
    declare Solver
    proc String
    f SExpr
    t = Solver -> String -> [SExpr] -> SExpr -> IO SExpr
    declareFun Solver
    proc String
    f [] SExpr
    t

    -- | Declare a function or a constant.
    -- For convenience, returns an the declared name as a constant expression.
    declareFun :: Solver -> String -> [SExpr] -> SExpr -> IO SExpr
    declareFun :: Solver -> String -> [SExpr] -> SExpr -> IO SExpr
    declareFun Solver
    proc String
    f [SExpr]
    as SExpr
    r =
      do Solver -> SExpr -> IO ()
    ackCommand Solver
    proc (SExpr -> IO ()) -> SExpr -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> [SExpr] -> SExpr
    fun String
    "declare-fun" [ String -> SExpr
    Atom String
    f, [SExpr] -> SExpr
    List [SExpr]
    as, SExpr
    r ]
         SExpr -> IO SExpr
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> SExpr
    const String
    f)

    -- | Declare an ADT using the format introduced in SmtLib 2.6.
    declareDatatype ::
      Solver ->
      String {- ^ datatype name -} ->
      [String] {- ^ sort parameters -} ->
      [(String, [(String, SExpr)])] {- ^ constructors -} ->
      IO ()
    declareDatatype :: Solver
    -> String -> [String] -> [(String, [(String, SExpr)])] -> IO ()
    declareDatatype Solver
    proc String
    t [] [(String, [(String, SExpr)])]
    cs =
      Solver -> SExpr -> IO ()
    ackCommand Solver
    proc (SExpr -> IO ()) -> SExpr -> IO ()
    forall a b. (a -> b) -> a -> b
    $
        String -> [SExpr] -> SExpr
    fun String
    "declare-datatype" ([SExpr] -> SExpr) -> [SExpr] -> SExpr
    forall a b. (a -> b) -> a -> b
    $
          [ String -> SExpr
    Atom String
    t
          , [SExpr] -> SExpr
    List [ [SExpr] -> SExpr
    List (String -> SExpr
    Atom String
    c SExpr -> [SExpr] -> [SExpr]
    forall a. a -> [a] -> [a]
    : [ [SExpr] -> SExpr
    List [String -> SExpr
    Atom String
    s, SExpr
    argTy] | (String
    s, SExpr
    argTy) <- [(String, SExpr)]
    args]) | (String
    c, [(String, SExpr)]
    args) <- [(String, [(String, SExpr)])]
    cs ]
          ]
    declareDatatype Solver
    proc String
    t [String]
    ps [(String, [(String, SExpr)])]
    cs =
      Solver -> SExpr -> IO ()
    ackCommand Solver
    proc (SExpr -> IO ()) -> SExpr -> IO ()
    forall a b. (a -> b) -> a -> b
    $
        String -> [SExpr] -> SExpr
    fun String
    "declare-datatype" ([SExpr] -> SExpr) -> [SExpr] -> SExpr
    forall a b. (a -> b) -> a -> b
    $
          [ String -> SExpr
    Atom String
    t
          , String -> [SExpr] -> SExpr
    fun String
    "par" ([SExpr] -> SExpr) -> [SExpr] -> SExpr
    forall a b. (a -> b) -> a -> b
    $
              [ [SExpr] -> SExpr
    List ((String -> SExpr) -> [String] -> [SExpr]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> SExpr
    Atom [String]
    ps)
              , [SExpr] -> SExpr
    List [ [SExpr] -> SExpr
    List (String -> SExpr
    Atom String
    c SExpr -> [SExpr] -> [SExpr]
    forall a. a -> [a] -> [a]
    : [ [SExpr] -> SExpr
    List [String -> SExpr
    Atom String
    s, SExpr
    argTy] | (String
    s, SExpr
    argTy) <- [(String, SExpr)]
    args]) | (String
    c, [(String, SExpr)]
    args) <- [(String, [(String, SExpr)])]
    cs ]
              ]
          ]

    -- | Declare a constant.  A common abbreviation for 'declareFun'.
    -- For convenience, returns the defined name as a constant expression.
    define :: Solver ->
              String {- ^ New symbol -} ->
              SExpr  {- ^ Symbol type -} ->
              SExpr  {- ^ Symbol definition -} ->
              IO SExpr
    define :: Solver -> String -> SExpr -> SExpr -> IO SExpr
    define Solver
    proc String
    f SExpr
    t SExpr
    e = Solver -> String -> [(String, SExpr)] -> SExpr -> SExpr -> IO SExpr
    defineFun Solver
    proc String
    f [] SExpr
    t SExpr
    e

    -- | Define a function or a constant.
    -- For convenience, returns an the defined name as a constant expression.
    defineFun :: Solver ->
                 String           {- ^ New symbol -} ->
                 [(String,SExpr)] {- ^ Parameters, with types -} ->
                 SExpr            {- ^ Type of result -} ->
                 SExpr            {- ^ Definition -} ->
                 IO SExpr
    defineFun :: Solver -> String -> [(String, SExpr)] -> SExpr -> SExpr -> IO SExpr
    defineFun Solver
    proc String
    f [(String, SExpr)]
    as SExpr
    t SExpr
    e =
      do Solver -> SExpr -> IO ()
    ackCommand Solver
    proc (SExpr -> IO ()) -> SExpr -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> [SExpr] -> SExpr
    fun String
    "define-fun"
                         ([SExpr] -> SExpr) -> [SExpr] -> SExpr
    forall a b. (a -> b) -> a -> b
    $ [ String -> SExpr
    Atom String
    f, [SExpr] -> SExpr
    List [ [SExpr] -> SExpr
    List [String -> SExpr
    const String
    x,SExpr
    a] | (String
    x,SExpr
    a) <- [(String, SExpr)]
    as ], SExpr
    t, SExpr
    e]
         SExpr -> IO SExpr
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> SExpr
    const String
    f)

    -- | Define a recursive function or a constant.  For convenience,
    -- returns an the defined name as a constant expression.  This body
    -- takes the function name as an argument.
    defineFunRec :: Solver ->
                    String           {- ^ New symbol -} ->
                    [(String,SExpr)] {- ^ Parameters, with types -} ->
                    SExpr            {- ^ Type of result -} ->
                    (SExpr -> SExpr) {- ^ Definition -} ->
                    IO SExpr
    defineFunRec :: Solver
    -> String
    -> [(String, SExpr)]
    -> SExpr
    -> (SExpr -> SExpr)
    -> IO SExpr
    defineFunRec Solver
    proc String
    f [(String, SExpr)]
    as SExpr
    t SExpr -> SExpr
    e =
      do let fs :: SExpr
    fs = String -> SExpr
    const String
    f
         Solver -> SExpr -> IO ()
    ackCommand Solver
    proc (SExpr -> IO ()) -> SExpr -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> [SExpr] -> SExpr
    fun String
    "define-fun-rec"
                         ([SExpr] -> SExpr) -> [SExpr] -> SExpr
    forall a b. (a -> b) -> a -> b
    $ [ String -> SExpr
    Atom String
    f, [SExpr] -> SExpr
    List [ [SExpr] -> SExpr
    List [String -> SExpr
    const String
    x,SExpr
    a] | (String
    x,SExpr
    a) <- [(String, SExpr)]
    as ], SExpr
    t, SExpr -> SExpr
    e SExpr
    fs]
         SExpr -> IO SExpr
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SExpr
    fs

    -- | Define a recursive function or a constant.  For convenience,
    -- returns an the defined name as a constant expression.  This body
    -- takes the function name as an argument.
    defineFunsRec :: Solver ->
                     [(String, [(String,SExpr)], SExpr, SExpr)] ->
                     IO ()
    defineFunsRec :: Solver -> [(String, [(String, SExpr)], SExpr, SExpr)] -> IO ()
    defineFunsRec Solver
    proc [(String, [(String, SExpr)], SExpr, SExpr)]
    ds = Solver -> SExpr -> IO ()
    ackCommand Solver
    proc (SExpr -> IO ()) -> SExpr -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> [SExpr] -> SExpr
    fun String
    "define-funs-rec" [ SExpr
    decls, SExpr
    bodies ]
      where
        oneArg :: (String, [(String, SExpr)], SExpr, d) -> SExpr
    oneArg (String
    f, [(String, SExpr)]
    args, SExpr
    t, d
    _) = [SExpr] -> SExpr
    List [ String -> SExpr
    Atom String
    f, [SExpr] -> SExpr
    List [ [SExpr] -> SExpr
    List [String -> SExpr
    const String
    x,SExpr
    a] | (String
    x,SExpr
    a) <- [(String, SExpr)]
    args ], SExpr
    t]
        decls :: SExpr
    decls  = [SExpr] -> SExpr
    List (((String, [(String, SExpr)], SExpr, SExpr) -> SExpr)
    -> [(String, [(String, SExpr)], SExpr, SExpr)] -> [SExpr]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, [(String, SExpr)], SExpr, SExpr) -> SExpr
    forall {d}. (String, [(String, SExpr)], SExpr, d) -> SExpr
    oneArg [(String, [(String, SExpr)], SExpr, SExpr)]
    ds)
        bodies :: SExpr
    bodies = [SExpr] -> SExpr
    List (((String, [(String, SExpr)], SExpr, SExpr) -> SExpr)
    -> [(String, [(String, SExpr)], SExpr, SExpr)] -> [SExpr]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(String
    _, [(String, SExpr)]
    _, SExpr
    _, SExpr
    body) -> SExpr
    body) [(String, [(String, SExpr)], SExpr, SExpr)]
    ds)

    -- | Assume a fact.
    assert :: Solver -> SExpr -> IO ()
    assert :: Solver -> SExpr -> IO ()
    assert Solver
    proc SExpr
    e = Solver -> SExpr -> IO ()
    ackCommand Solver
    proc (SExpr -> IO ()) -> SExpr -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> [SExpr] -> SExpr
    fun String
    "assert" [SExpr
    e]

    -- | Check if the current set of assertion is consistent.
    check :: Solver -> IO Result
    check :: Solver -> IO Result
    check Solver
    proc =
      do res <- Solver -> SExpr -> IO SExpr
    command Solver
    proc ([SExpr] -> SExpr
    List [ String -> SExpr
    Atom String
    "check-sat" ])
         case res of
           Atom String
    "unsat"   -> Result -> IO Result
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    Unsat
           Atom String
    "unknown" -> Result -> IO Result
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    Unknown
           Atom String
    "sat"     -> Result -> IO Result
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    Sat
           SExpr
    _ -> String -> IO Result
    forall a. String -> IO a
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail (String -> IO Result) -> String -> IO Result
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines
                  [ String
    "Unexpected result from the SMT solver:"
                  , String
    "  Expected: unsat, unknown, or sat"
                  , String
    "  Result: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> ShowS
    showsSExpr SExpr
    res String
    ""
                  ]

    -- | Convert an s-expression to a value.
    sexprToVal :: SExpr -> Value
    sexprToVal :: SExpr -> Value
    sexprToVal SExpr
    expr =
      case SExpr
    expr of
        Atom String
    "true"                    -> Bool -> Value
    Bool Bool
    True
        Atom String
    "false"                   -> Bool -> Value
    Bool Bool
    False
        Atom (Char
    '#' : Char
    'b' : String
    ds)
          | Just Integer
    n <- String -> Maybe Integer
    binLit String
    ds         -> Int -> Integer -> Value
    Bits (String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    ds) Integer
    n
        Atom (Char
    '#' : Char
    'x' : String
    ds)
          | [(Integer
    n,[])] <- ReadS Integer
    forall a. (Eq a, Num a) => ReadS a
    readHex String
    ds      -> Int -> Integer -> Value
    Bits (Int
    4 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    * String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    ds) Integer
    n
        Atom String
    txt
          | Just Integer
    n <- String -> Maybe Integer
    forall a. Read a => String -> Maybe a
    readMaybe String
    txt     -> Integer -> Value
    Int Integer
    n
        List [ Atom String
    "-", SExpr
    x ]
          | Int Integer
    a <- SExpr -> Value
    sexprToVal SExpr
    x    -> Integer -> Value
    Int (Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    a)
        List [ Atom String
    "/", SExpr
    x, SExpr
    y ]
          | Int Integer
    a <- SExpr -> Value
    sexprToVal SExpr
    x
          , Int Integer
    b <- SExpr -> Value
    sexprToVal SExpr
    y    -> Rational -> Value
    Real (Integer
    a Integer -> Integer -> Rational
    forall a. Integral a => a -> a -> Ratio a
    % Integer
    b)
        SExpr
    _ -> SExpr -> Value
    Other SExpr
    expr

      where
      binLit :: String -> Maybe Integer
    binLit String
    cs = do ds <- (Char -> Maybe Integer) -> String -> Maybe [Integer]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Char -> Maybe Integer
    forall {a}. Num a => Char -> Maybe a
    binDigit String
    cs
                     return $ sum $ zipWith (*) (reverse ds) powers2
      powers2 :: [Integer]
    powers2   = Integer
    1 Integer -> [Integer] -> [Integer]
    forall a. a -> [a] -> [a]
    : (Integer -> Integer) -> [Integer] -> [Integer]
    forall a b. (a -> b) -> [a] -> [b]
    map (Integer
    2 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *) [Integer]
    powers2
      binDigit :: Char -> Maybe a
    binDigit Char
    '0' = a -> Maybe a
    forall a. a -> Maybe a
    Just a
    0
      binDigit Char
    '1' = a -> Maybe a
    forall a. a -> Maybe a
    Just a
    1
      binDigit Char
    _   = Maybe a
    forall a. Maybe a
    Nothing

    -- | Get the values of some s-expressions.
    -- Only valid after a 'Sat' result.
    getExprs :: Solver -> [SExpr] -> IO [(SExpr, Value)]
    getExprs :: Solver -> [SExpr] -> IO [(SExpr, Value)]
    getExprs Solver
    proc [SExpr]
    vals =
      do res <- Solver -> SExpr -> IO SExpr
    command Solver
    proc (SExpr -> IO SExpr) -> SExpr -> IO SExpr
    forall a b. (a -> b) -> a -> b
    $ [SExpr] -> SExpr
    List [ String -> SExpr
    Atom String
    "get-value", [SExpr] -> SExpr
    List [SExpr]
    vals ]
         case res of
           List [SExpr]
    xs -> (SExpr -> IO (SExpr, Value)) -> [SExpr] -> IO [(SExpr, Value)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM SExpr -> IO (SExpr, Value)
    forall {m :: * -> *}. MonadFail m => SExpr -> m (SExpr, Value)
    getAns [SExpr]
    xs
           SExpr
    _ -> String -> IO [(SExpr, Value)]
    forall a. String -> IO a
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail (String -> IO [(SExpr, Value)]) -> String -> IO [(SExpr, Value)]
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines
                     [ String
    "Unexpected response from the SMT solver:"
                     , String
    "  Exptected: a list"
                     , String
    "  Result: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> ShowS
    showsSExpr SExpr
    res String
    ""
                     ]
      where
      getAns :: SExpr -> m (SExpr, Value)
    getAns SExpr
    expr =
        case SExpr
    expr of
          List [ SExpr
    e, SExpr
    v ] -> (SExpr, Value) -> m (SExpr, Value)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr
    e, SExpr -> Value
    sexprToVal SExpr
    v)
          SExpr
    _             -> String -> m (SExpr, Value)
    forall a. String -> m a
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail (String -> m (SExpr, Value)) -> String -> m (SExpr, Value)
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines
                                [ String
    "Unexpected response from the SMT solver:"
                                , String
    "  Expected: (expr val)"
                                , String
    "  Result: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> ShowS
    showsSExpr SExpr
    expr String
    ""
                                ]

    -- | Get the values of some constants in the current model.
    -- A special case of 'getExprs'.
    -- Only valid after a 'Sat' result.
    getConsts :: Solver -> [String] -> IO [(String, Value)]
    getConsts :: Solver -> [String] -> IO [(String, Value)]
    getConsts Solver
    proc [String]
    xs =
      do ans <- Solver -> [SExpr] -> IO [(SExpr, Value)]
    getExprs Solver
    proc ((String -> SExpr) -> [String] -> [SExpr]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> SExpr
    Atom [String]
    xs)
         return [ (x,e) | (Atom x, e) <- ans ]

    -- | Get the value of a single expression.
    getExpr :: Solver -> SExpr -> IO Value
    getExpr :: Solver -> SExpr -> IO Value
    getExpr Solver
    proc SExpr
    x =
      do [ (_,v) ] <- Solver -> [SExpr] -> IO [(SExpr, Value)]
    getExprs Solver
    proc [SExpr
    x]
         return v

    -- | Get the value of a single constant.
    getConst :: Solver -> String -> IO Value
    getConst :: Solver -> String -> IO Value
    getConst Solver
    proc String
    x = Solver -> SExpr -> IO Value
    getExpr Solver
    proc (String -> SExpr
    Atom String
    x)

    -- | Returns the names of the (named) formulas involved in a contradiction.
    getUnsatCore :: Solver -> IO [String]
    getUnsatCore :: Solver -> IO [String]
    getUnsatCore Solver
    s =
      do res <- Solver -> SExpr -> IO SExpr
    command Solver
    s (SExpr -> IO SExpr) -> SExpr -> IO SExpr
    forall a b. (a -> b) -> a -> b
    $ [SExpr] -> SExpr
    List [ String -> SExpr
    Atom String
    "get-unsat-core" ]
         case res of
           List [SExpr]
    xs -> (SExpr -> IO String) -> [SExpr] -> IO [String]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM SExpr -> IO String
    forall {m :: * -> *}. MonadFail m => SExpr -> m String
    fromAtom [SExpr]
    xs
           SExpr
    _       -> String -> SExpr -> IO [String]
    forall {m :: * -> *} {a}. MonadFail m => String -> SExpr -> m a
    unexpected String
    "a list of atoms" SExpr
    res
      where
      fromAtom :: SExpr -> m String
    fromAtom SExpr
    x =
        case SExpr
    x of
          Atom String
    a -> String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    a
          SExpr
    _      -> String -> SExpr -> m String
    forall {m :: * -> *} {a}. MonadFail m => String -> SExpr -> m a
    unexpected String
    "an atom" SExpr
    x

      unexpected :: String -> SExpr -> m a
    unexpected String
    x SExpr
    e =
        String -> m a
    forall a. String -> m a
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail (String -> m a) -> String -> m a
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    "Unexpected response from the SMT Solver:"
                       , String
    "  Expected: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    x
                       , String
    "  Result: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> ShowS
    showsSExpr SExpr
    e String
    ""
                       ]

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

    -- | A constant, corresponding to a family indexed by some integers.
    fam :: String -> [Integer] -> SExpr
    fam :: String -> [Integer] -> SExpr
    fam String
    f [Integer]
    is = [SExpr] -> SExpr
    List (String -> SExpr
    Atom String
    "_" SExpr -> [SExpr] -> [SExpr]
    forall a. a -> [a] -> [a]
    : String -> SExpr
    Atom String
    f SExpr -> [SExpr] -> [SExpr]
    forall a. a -> [a] -> [a]
    : (Integer -> SExpr) -> [Integer] -> [SExpr]
    forall a b. (a -> b) -> [a] -> [b]
    map (String -> SExpr
    Atom (String -> SExpr) -> (Integer -> String) -> Integer -> SExpr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> String
    forall a. Show a => a -> String
    show) [Integer]
    is)

    -- | An SMT function.
    fun :: String -> [SExpr] -> SExpr
    fun :: String -> [SExpr] -> SExpr
    fun String
    f [] = String -> SExpr
    Atom String
    f
    fun String
    f [SExpr]
    as = [SExpr] -> SExpr
    List (String -> SExpr
    Atom String
    f SExpr -> [SExpr] -> [SExpr]
    forall a. a -> [a] -> [a]
    : [SExpr]
    as)

    -- | An SMT constant.  A special case of 'fun'.
    const :: String -> SExpr
    const :: String -> SExpr
    const String
    f = String -> [SExpr] -> SExpr
    fun String
    f []

    app :: SExpr -> [SExpr] -> SExpr
    app :: SExpr -> [SExpr] -> SExpr
    app SExpr
    f [SExpr]
    xs = [SExpr] -> SExpr
    List (SExpr
    f SExpr -> [SExpr] -> [SExpr]
    forall a. a -> [a] -> [a]
    : [SExpr]
    xs)

    -- Identifiers -----------------------------------------------------------------------

    -- | Symbols are either simple or quoted (c.f. SMTLIB v2.6 S3.1).
    -- This predicate indicates whether a character is allowed in a simple
    -- symbol.  Note that only ASCII letters are allowed.
    allowedSimpleChar :: Char -> Bool
    allowedSimpleChar :: Char -> Bool
    allowedSimpleChar Char
    c =
      Char -> Bool
    isDigit Char
    c Bool -> Bool -> Bool
    || Char
    c Char -> String -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` ([Char
    'a' .. Char
    'z'] String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char
    'A' .. Char
    'Z'] String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "~!@$%^&*_-+=<>.?/")

    isSimpleSymbol :: String -> Bool
    isSimpleSymbol :: String -> Bool
    isSimpleSymbol s :: String
    s@(Char
    c : String
    _) = Bool -> Bool
    P.not (Char -> Bool
    isDigit Char
    c) Bool -> Bool -> Bool
    && (Char -> Bool) -> String -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Char -> Bool
    allowedSimpleChar String
    s
    isSimpleSymbol String
    _         = Bool
    False

    quoteSymbol :: String -> String
    quoteSymbol :: ShowS
    quoteSymbol String
    s
      | String -> Bool
    isSimpleSymbol String
    s = String
    s
      | Bool
    otherwise        = Char
    '|' Char -> ShowS
    forall a. a -> [a] -> [a]
    : String
    s String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "|"

    symbol :: String -> SExpr
    symbol :: String -> SExpr
    symbol = String -> SExpr
    Atom (String -> SExpr) -> ShowS -> String -> SExpr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ShowS
    quoteSymbol

    keyword :: String -> SExpr
    keyword :: String -> SExpr
    keyword String
    s = String -> SExpr
    Atom (Char
    ':' Char -> ShowS
    forall a. a -> [a] -> [a]
    : String
    s)

    -- | Generate a type annotation for a symbol
    as :: SExpr -> SExpr -> SExpr
    as :: SExpr -> SExpr -> SExpr
    as SExpr
    s SExpr
    t = String -> [SExpr] -> SExpr
    fun String
    "as" [SExpr
    s, SExpr
    t]

    -- Types -----------------------------------------------------------------------

    -- | The type of integers.
    tInt :: SExpr
    tInt :: SExpr
    tInt = String -> SExpr
    const String
    "Int"

    -- | The type of booleans.
    tBool :: SExpr
    tBool :: SExpr
    tBool = String -> SExpr
    const String
    "Bool"

    -- | The type of reals.
    tReal :: SExpr
    tReal :: SExpr
    tReal = String -> SExpr
    const String
    "Real"

    -- | The type of arrays.
    tArray :: SExpr {- ^ Type of indexes  -} ->
              SExpr {- ^ Type of elements -} ->
              SExpr
    tArray :: SExpr -> SExpr -> SExpr
    tArray SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "Array" [SExpr
    x,SExpr
    y]

    -- | The type of bit vectors.
    tBits :: Integer {- ^ Number of bits -} ->
             SExpr
    tBits :: Integer -> SExpr
    tBits Integer
    w = String -> [Integer] -> SExpr
    fam String
    "BitVec" [Integer
    w]

    -- Literals --------------------------------------------------------------------

    -- | Boolean literals.
    bool :: Bool -> SExpr
    bool :: Bool -> SExpr
    bool Bool
    b = String -> SExpr
    const (if Bool
    b then String
    "true" else String
    "false")

    -- | Integer literals.
    int :: Integer -> SExpr
    int :: Integer -> SExpr
    int Integer
    x | Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    0     = SExpr -> SExpr
    neg (Integer -> SExpr
    int (Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    x))
          | Bool
    otherwise = String -> SExpr
    Atom (Integer -> String
    forall a. Show a => a -> String
    show Integer
    x)

    -- | Real (well, rational) literals.
    real :: Rational -> SExpr
    real :: Rational -> SExpr
    real Rational
    x
      | Double -> Rational
    forall a. Real a => a -> Rational
    toRational Double
    y Rational -> Rational -> Bool
    forall a. Eq a => a -> a -> Bool
    == Rational
    x = String -> SExpr
    Atom (Maybe Int -> Double -> ShowS
    forall a. RealFloat a => Maybe Int -> a -> ShowS
    showFFloat Maybe Int
    forall a. Maybe a
    Nothing Double
    y String
    "")
      | Bool
    otherwise = SExpr -> SExpr -> SExpr
    realDiv (Integer -> SExpr
    int (Rational -> Integer
    forall a. Ratio a -> a
    numerator Rational
    x)) (Integer -> SExpr
    int (Rational -> Integer
    forall a. Ratio a -> a
    denominator Rational
    x))
      where y :: Double
    y = Rational -> Double
    forall a. Fractional a => Rational -> a
    fromRational Rational
    x :: Double

    -- | A bit vector represented in binary.
    --
    --     * If the value does not fit in the bits, then the bits will be increased.
    --     * The width should be strictly positive.
    bvBin :: Int {- ^ Width, in bits -} -> Integer {- ^ Value -} -> SExpr
    bvBin :: Int -> Integer -> SExpr
    bvBin Int
    w Integer
    v = String -> SExpr
    const (String
    "#b" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    bits)
      where
      bits :: String
    bits = ShowS
    forall a. [a] -> [a]
    reverse [ if Integer -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    testBit Integer
    v Int
    n then Char
    '1' else Char
    '0' | Int
    n <- [ Int
    0 .. Int
    w Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1 ] ]

    -- | A bit vector represented in hex.
    --
    --    * If the value does not fit in the bits, the bits will be increased to
    --      the next multiple of 4 that will fit the value.
    --    * If the width is not a multiple of 4, it will be rounded
    --      up so that it is.
    --    * The width should be strictly positive.
    bvHex :: Int {- ^ Width, in bits -} -> Integer {- ^ Value -} -> SExpr
    bvHex :: Int -> Integer -> SExpr
    bvHex Int
    w Integer
    v
      | Integer
    v Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    0    = String -> SExpr
    const (String
    "#x" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    padding String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    hex)
      | Bool
    otherwise = Int -> Integer -> SExpr
    bvHex Int
    w (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Int
    w Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    v)
      where
      hex :: String
    hex     = Integer -> ShowS
    forall a. Integral a => a -> ShowS
    showHex Integer
    v String
    ""
      padding :: String
    padding = Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate (Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    P.div (Int
    w Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    3) Int
    4 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    hex) Char
    '0'

    -- | Render a value as an expression.  Bit-vectors are rendered in hex,
    -- if their width is a multiple of 4, and in binary otherwise.
    value :: Value -> SExpr
    value :: Value -> SExpr
    value Value
    val =
      case Value
    val of
        Bool Bool
    b    -> Bool -> SExpr
    bool Bool
    b
        Int Integer
    n     -> Integer -> SExpr
    int Integer
    n
        Real Rational
    r    -> Rational -> SExpr
    real Rational
    r
        Bits Int
    w Integer
    v | Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    P.mod Int
    w Int
    4 Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 -> Int -> Integer -> SExpr
    bvHex Int
    w Integer
    v
                 | Bool
    otherwise      -> Int -> Integer -> SExpr
    bvBin Int
    w Integer
    v
        Other SExpr
    o   -> SExpr
    o

    -- Connectives -----------------------------------------------------------------

    -- | Logical negation.
    not :: SExpr -> SExpr
    not :: SExpr -> SExpr
    not SExpr
    p = String -> [SExpr] -> SExpr
    fun String
    "not" [SExpr
    p]

    -- | Conjunction.
    and :: SExpr -> SExpr -> SExpr
    and :: SExpr -> SExpr -> SExpr
    and SExpr
    p SExpr
    q = String -> [SExpr] -> SExpr
    fun String
    "and" [SExpr
    p,SExpr
    q]

    andMany :: [SExpr] -> SExpr
    andMany :: [SExpr] -> SExpr
    andMany [SExpr]
    xs = if [SExpr] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SExpr]
    xs then Bool -> SExpr
    bool Bool
    True else String -> [SExpr] -> SExpr
    fun String
    "and" [SExpr]
    xs

    -- | Disjunction.
    or :: SExpr -> SExpr -> SExpr
    or :: SExpr -> SExpr -> SExpr
    or SExpr
    p SExpr
    q = String -> [SExpr] -> SExpr
    fun String
    "or" [SExpr
    p,SExpr
    q]

    orMany :: [SExpr] -> SExpr
    orMany :: [SExpr] -> SExpr
    orMany [SExpr]
    xs = if [SExpr] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SExpr]
    xs then Bool -> SExpr
    bool Bool
    False else String -> [SExpr] -> SExpr
    fun String
    "or" [SExpr]
    xs

    -- | Exclusive-or.
    xor :: SExpr -> SExpr -> SExpr
    xor :: SExpr -> SExpr -> SExpr
    xor SExpr
    p SExpr
    q = String -> [SExpr] -> SExpr
    fun String
    "xor" [SExpr
    p,SExpr
    q]

    -- | Implication.
    implies :: SExpr -> SExpr -> SExpr
    implies :: SExpr -> SExpr -> SExpr
    implies SExpr
    p SExpr
    q = String -> [SExpr] -> SExpr
    fun String
    "=>" [SExpr
    p,SExpr
    q]

    -- If-then-else ----------------------------------------------------------------

    -- | If-then-else.  This is polymorphic and can be used to construct any term.
    ite :: SExpr -> SExpr -> SExpr -> SExpr
    ite :: SExpr -> SExpr -> SExpr -> SExpr
    ite SExpr
    x SExpr
    y SExpr
    z = String -> [SExpr] -> SExpr
    fun String
    "ite" [SExpr
    x,SExpr
    y,SExpr
    z]

    -- Relations -------------------------------------------------------------------

    -- | Equality.
    eq :: SExpr -> SExpr -> SExpr
    eq :: SExpr -> SExpr -> SExpr
    eq SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "=" [SExpr
    x,SExpr
    y]

    distinct :: [SExpr] -> SExpr
    distinct :: [SExpr] -> SExpr
    distinct [SExpr]
    xs = if [SExpr] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SExpr]
    xs then Bool -> SExpr
    bool Bool
    True else String -> [SExpr] -> SExpr
    fun String
    "distinct" [SExpr]
    xs

    -- | Greater-then
    gt :: SExpr -> SExpr -> SExpr
    gt :: SExpr -> SExpr -> SExpr
    gt SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    ">" [SExpr
    x,SExpr
    y]

    -- | Less-then.
    lt :: SExpr -> SExpr -> SExpr
    lt :: SExpr -> SExpr -> SExpr
    lt SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "<" [SExpr
    x,SExpr
    y]

    -- | Greater-than-or-equal-to.
    geq :: SExpr -> SExpr -> SExpr
    geq :: SExpr -> SExpr -> SExpr
    geq SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    ">=" [SExpr
    x,SExpr
    y]

    -- | Less-than-or-equal-to.
    leq :: SExpr -> SExpr -> SExpr
    leq :: SExpr -> SExpr -> SExpr
    leq SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "<=" [SExpr
    x,SExpr
    y]

    -- | Unsigned less-than on bit-vectors.
    bvULt :: SExpr -> SExpr -> SExpr
    bvULt :: SExpr -> SExpr -> SExpr
    bvULt SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "bvult" [SExpr
    x,SExpr
    y]

    -- | Unsigned less-than-or-equal on bit-vectors.
    bvULeq :: SExpr -> SExpr -> SExpr
    bvULeq :: SExpr -> SExpr -> SExpr
    bvULeq SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "bvule" [SExpr
    x,SExpr
    y]

    -- | Signed less-than on bit-vectors.
    bvSLt :: SExpr -> SExpr -> SExpr
    bvSLt :: SExpr -> SExpr -> SExpr
    bvSLt SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "bvslt" [SExpr
    x,SExpr
    y]

    -- | Signed less-than-or-equal on bit-vectors.
    bvSLeq :: SExpr -> SExpr -> SExpr
    bvSLeq :: SExpr -> SExpr -> SExpr
    bvSLeq SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "bvsle" [SExpr
    x,SExpr
    y]

    -- | Addition.
    -- See also 'bvAdd'
    add :: SExpr -> SExpr -> SExpr
    add :: SExpr -> SExpr -> SExpr
    add SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "+" [SExpr
    x,SExpr
    y]

    addMany :: [SExpr] -> SExpr
    addMany :: [SExpr] -> SExpr
    addMany [SExpr]
    xs = if [SExpr] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SExpr]
    xs then Integer -> SExpr
    int Integer
    0 else String -> [SExpr] -> SExpr
    fun String
    "+" [SExpr]
    xs

    -- | Subtraction.
    sub :: SExpr -> SExpr -> SExpr
    sub :: SExpr -> SExpr -> SExpr
    sub SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "-" [SExpr
    x,SExpr
    y]

    -- | Arithmetic negation for integers and reals.
    -- See also 'bvNeg'.
    neg :: SExpr -> SExpr
    neg :: SExpr -> SExpr
    neg SExpr
    x = String -> [SExpr] -> SExpr
    fun String
    "-" [SExpr
    x]

    -- | Multiplication.
    mul :: SExpr -> SExpr -> SExpr
    mul :: SExpr -> SExpr -> SExpr
    mul SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "*" [SExpr
    x,SExpr
    y]

    -- | Absolute value.
    abs :: SExpr -> SExpr
    abs :: SExpr -> SExpr
    abs SExpr
    x = String -> [SExpr] -> SExpr
    fun String
    "abs" [SExpr
    x]

    -- | Integer division.
    div :: SExpr -> SExpr -> SExpr
    div :: SExpr -> SExpr -> SExpr
    div SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "div" [SExpr
    x,SExpr
    y]

    -- | Modulus.
    mod :: SExpr -> SExpr -> SExpr
    mod :: SExpr -> SExpr -> SExpr
    mod SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "mod" [SExpr
    x,SExpr
    y]

    -- | Is the number divisible by the given constant.
    divisible :: SExpr -> Integer -> SExpr
    divisible :: SExpr -> Integer -> SExpr
    divisible SExpr
    x Integer
    n = [SExpr] -> SExpr
    List [ String -> [Integer] -> SExpr
    fam String
    "divisible" [Integer
    n], SExpr
    x ]

    -- | Division of real numbers.
    realDiv :: SExpr -> SExpr -> SExpr
    realDiv :: SExpr -> SExpr -> SExpr
    realDiv SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "/" [SExpr
    x,SExpr
    y]

    -- | Bit vector concatenation.
    concat :: SExpr -> SExpr -> SExpr
    concat :: SExpr -> SExpr -> SExpr
    concat SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "concat" [SExpr
    x,SExpr
    y]

    -- | Extend to the signed equivalent bitvector by @i@ bits
    signExtend :: Integer -> SExpr -> SExpr
    signExtend :: Integer -> SExpr -> SExpr
    signExtend Integer
    i SExpr
    x = [SExpr] -> SExpr
    List [ String -> [Integer] -> SExpr
    fam String
    "sign_extend" [Integer
    i], SExpr
    x ]

    -- | Extend with zeros to the unsigned equivalent bitvector
    -- by @i@ bits
    zeroExtend :: Integer -> SExpr -> SExpr
    zeroExtend :: Integer -> SExpr -> SExpr
    zeroExtend Integer
    i SExpr
    x = [SExpr] -> SExpr
    List [ String -> [Integer] -> SExpr
    fam String
    "zero_extend" [Integer
    i], SExpr
    x ]

    -- | Satisfies @toInt x <= x@ (i.e., this is like Haskell's 'floor')
    toInt :: SExpr -> SExpr
    toInt :: SExpr -> SExpr
    toInt SExpr
    e = String -> [SExpr] -> SExpr
    fun String
    "to_int" [SExpr
    e]

    -- | Promote an integer to a real
    toReal :: SExpr -> SExpr
    toReal :: SExpr -> SExpr
    toReal SExpr
    e = String -> [SExpr] -> SExpr
    fun String
    "to_real" [SExpr
    e]

    -- | Extract a sub-sequence of a bit vector.
    extract :: SExpr -> Integer -> Integer -> SExpr
    extract :: SExpr -> Integer -> Integer -> SExpr
    extract SExpr
    x Integer
    y Integer
    z = [SExpr] -> SExpr
    List [ String -> [Integer] -> SExpr
    fam String
    "extract" [Integer
    y,Integer
    z], SExpr
    x ]

    -- | Bitwise negation.
    bvNot :: SExpr -> SExpr
    bvNot :: SExpr -> SExpr
    bvNot SExpr
    x = String -> [SExpr] -> SExpr
    fun String
    "bvnot" [SExpr
    x]

    -- | Bitwise conjuction.
    bvAnd :: SExpr -> SExpr -> SExpr
    bvAnd :: SExpr -> SExpr -> SExpr
    bvAnd SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "bvand" [SExpr
    x,SExpr
    y]

    -- | Bitwise disjunction.
    bvOr :: SExpr -> SExpr -> SExpr
    bvOr :: SExpr -> SExpr -> SExpr
    bvOr SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "bvor" [SExpr
    x,SExpr
    y]

    -- | Bitwise exclusive or.
    bvXOr :: SExpr -> SExpr -> SExpr
    bvXOr :: SExpr -> SExpr -> SExpr
    bvXOr SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "bvxor" [SExpr
    x,SExpr
    y]

    -- | Bit vector arithmetic negation.
    bvNeg :: SExpr -> SExpr
    bvNeg :: SExpr -> SExpr
    bvNeg SExpr
    x = String -> [SExpr] -> SExpr
    fun String
    "bvneg" [SExpr
    x]

    -- | Addition of bit vectors.
    bvAdd :: SExpr -> SExpr -> SExpr
    bvAdd :: SExpr -> SExpr -> SExpr
    bvAdd SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "bvadd" [SExpr
    x,SExpr
    y]

    -- | Subtraction of bit vectors.
    bvSub :: SExpr -> SExpr -> SExpr
    bvSub :: SExpr -> SExpr -> SExpr
    bvSub SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "bvsub" [SExpr
    x,SExpr
    y]

    -- | Multiplication of bit vectors.
    bvMul :: SExpr -> SExpr -> SExpr
    bvMul :: SExpr -> SExpr -> SExpr
    bvMul SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "bvmul" [SExpr
    x,SExpr
    y]

    -- | Bit vector unsigned division.
    bvUDiv :: SExpr -> SExpr -> SExpr
    bvUDiv :: SExpr -> SExpr -> SExpr
    bvUDiv SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "bvudiv" [SExpr
    x,SExpr
    y]

    -- | Bit vector unsigned reminder.
    bvURem :: SExpr -> SExpr -> SExpr
    bvURem :: SExpr -> SExpr -> SExpr
    bvURem SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "bvurem" [SExpr
    x,SExpr
    y]

    -- | Bit vector signed division.
    bvSDiv :: SExpr -> SExpr -> SExpr
    bvSDiv :: SExpr -> SExpr -> SExpr
    bvSDiv SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "bvsdiv" [SExpr
    x,SExpr
    y]

    -- | Bit vector signed reminder.
    bvSRem :: SExpr -> SExpr -> SExpr
    bvSRem :: SExpr -> SExpr -> SExpr
    bvSRem SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "bvsrem" [SExpr
    x,SExpr
    y]

    -- | Shift left.
    bvShl :: SExpr {- ^ value -} -> SExpr {- ^ shift amount -} -> SExpr
    bvShl :: SExpr -> SExpr -> SExpr
    bvShl SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "bvshl" [SExpr
    x,SExpr
    y]

    -- | Logical shift right.
    bvLShr :: SExpr {- ^ value -} -> SExpr {- ^ shift amount -} -> SExpr
    bvLShr :: SExpr -> SExpr -> SExpr
    bvLShr SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "bvlshr" [SExpr
    x,SExpr
    y]

    -- | Arithemti shift right (copies most significant bit).
    bvAShr :: SExpr {- ^ value -} -> SExpr {- ^ shift amount -} -> SExpr
    bvAShr :: SExpr -> SExpr -> SExpr
    bvAShr SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "bvashr" [SExpr
    x,SExpr
    y]

    -- | Get an elemeent of an array.
    select :: SExpr {- ^ array -} -> SExpr {- ^ index -} -> SExpr
    select :: SExpr -> SExpr -> SExpr
    select SExpr
    x SExpr
    y = String -> [SExpr] -> SExpr
    fun String
    "select" [SExpr
    x,SExpr
    y]

    -- | Update an array
    store :: SExpr {- ^ array -}     ->
             SExpr {- ^ index -}     ->
             SExpr {- ^ new value -} ->
             SExpr
    store :: SExpr -> SExpr -> SExpr -> SExpr
    store SExpr
    x SExpr
    y SExpr
    z = String -> [SExpr] -> SExpr
    fun String
    "store" [SExpr
    x,SExpr
    y,SExpr
    z]

    --------------------------------------------------------------------------------
    -- Attributes

    named :: String -> SExpr -> SExpr
    named :: String -> SExpr -> SExpr
    named String
    x SExpr
    e = String -> [SExpr] -> SExpr
    fun String
    "!" [SExpr
    e, String -> SExpr
    Atom String
    ":named", String -> SExpr
    Atom String
    x ]

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

    -- | Log messages with minimal formatting. Mostly for debugging.
    data Logger = Logger
      { Logger -> String -> IO ()
    logMessage :: String -> IO ()
        -- ^ Log a message.

      , Logger -> IO Int
    logLevel   :: IO Int

      , Logger -> Int -> IO ()
    logSetLevel:: Int -> IO ()

      , Logger -> IO ()
    logTab     :: IO ()
        -- ^ Increase indentation.

      , Logger -> IO ()
    logUntab   :: IO ()
        -- ^ Decrease indentation.
      }

    -- | Run an IO action with the logger set to a specific level, restoring it when
    -- done.
    withLogLevel :: Logger -> Int -> IO a -> IO a
    withLogLevel :: forall a. Logger -> Int -> IO a -> IO a
    withLogLevel Logger { IO Int
    IO ()
    Int -> IO ()
    String -> IO ()
    logMessage :: Logger -> String -> IO ()
    logLevel :: Logger -> IO Int
    logSetLevel :: Logger -> Int -> IO ()
    logTab :: Logger -> IO ()
    logUntab :: Logger -> IO ()
    logMessage :: String -> IO ()
    logLevel :: IO Int
    logSetLevel :: Int -> IO ()
    logTab :: IO ()
    logUntab :: IO ()
    .. } Int
    l IO a
    m =
      do l0 <- IO Int
    logLevel
         X.bracket_ (logSetLevel l) (logSetLevel l0) m

    logIndented :: Logger -> IO a -> IO a
    logIndented :: forall a. Logger -> IO a -> IO a
    logIndented Logger { IO Int
    IO ()
    Int -> IO ()
    String -> IO ()
    logMessage :: Logger -> String -> IO ()
    logLevel :: Logger -> IO Int
    logSetLevel :: Logger -> Int -> IO ()
    logTab :: Logger -> IO ()
    logUntab :: Logger -> IO ()
    logMessage :: String -> IO ()
    logLevel :: IO Int
    logSetLevel :: Int -> IO ()
    logTab :: IO ()
    logUntab :: IO ()
    .. } = IO () -> IO () -> IO a -> IO a
    forall a b c. IO a -> IO b -> IO c -> IO c
    X.bracket_ IO ()
    logTab IO ()
    logUntab

    -- | Log a message at a specific log level.
    logMessageAt :: Logger -> Int -> String -> IO ()
    logMessageAt :: Logger -> Int -> String -> IO ()
    logMessageAt Logger
    logger Int
    l String
    msg = Logger -> Int -> IO () -> IO ()
    forall a. Logger -> Int -> IO a -> IO a
    withLogLevel Logger
    logger Int
    l (Logger -> String -> IO ()
    logMessage Logger
    logger String
    msg)

    -- | A simple stdout logger.  Shows only messages logged at a level that is
    -- greater than or equal to the passed level.
    newLogger :: Int -> IO Logger
    newLogger :: Int -> IO Logger
    newLogger Int
    l =
      do tab <- Int -> IO (IORef Int)
    forall a. a -> IO (IORef a)
    newIORef Int
    0
         lev <- newIORef 0
         let logLevel    = IORef Int -> IO Int
    forall a. IORef a -> IO a
    readIORef IORef Int
    lev
             logSetLevel = IORef Int -> Int -> IO ()
    forall a. IORef a -> a -> IO ()
    writeIORef IORef Int
    lev

             shouldLog IO ()
    m =
               do cl <- IO Int
    logLevel
                  when (cl >= l) m

             logMessage String
    x = IO () -> IO ()
    shouldLog (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $
               do let ls :: [String]
    ls = String -> [String]
    lines String
    x
                  t <- IORef Int -> IO Int
    forall a. IORef a -> IO a
    readIORef IORef Int
    tab
                  putStr $ unlines [ replicate t ' ' ++ l | l <- ls ]
                  hFlush stdout

             logTab   = IO () -> IO ()
    shouldLog (IORef Int -> (Int -> Int) -> IO ()
    forall a. IORef a -> (a -> a) -> IO ()
    modifyIORef' IORef Int
    tab (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    2))
             logUntab = IO () -> IO ()
    shouldLog (IORef Int -> (Int -> Int) -> IO ()
    forall a. IORef a -> (a -> a) -> IO ()
    modifyIORef' IORef Int
    tab (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    subtract Int
    2))
         return Logger { .. }