    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.SMT.Utils
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- A few internally used types/routines
    -----------------------------------------------------------------------------

    {-# LANGUAGE NamedFieldPuns #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.SMT.Utils (
              SMTLibConverter
            , SMTLibIncConverter
            , addAnnotations
            , showTimeoutValue
            , alignDiagnostic
            , alignPlain
            , debug
            , mergeSExpr
            , SBVException(..)
           )
           where

    import qualified Control.Exception as C

    import Control.Monad.Trans (MonadIO, liftIO)

    import Data.SBV.Core.Data
    import Data.SBV.Core.Symbolic (QueryContext, CnstMap, SMTDef, ResultInp(..), ProgInfo(..))
    import Data.SBV.Utils.Lib (joinArgs)

    import Data.List (intercalate)
    import qualified Data.Set      as Set (Set)
    import qualified Data.Sequence as S   (Seq)

    import System.Exit (ExitCode(..))

    -- | An instance of SMT-Lib converter; instantiated for SMT-Lib v1 and v2. (And potentially for newer versions in the future.)
    type SMTLibConverter a =  QueryContext                                  -- ^ Internal or external query?
                           -> ProgInfo                                      -- ^ Various program info
                           -> Set.Set Kind                                  -- ^ Kinds used in the problem
                           -> Bool                                          -- ^ is this a sat problem?
                           -> [String]                                      -- ^ extra comments to place on top
                           -> ResultInp                                     -- ^ inputs or params
                           -> (CnstMap, [(SV, CV)])                         -- ^ constants. The map, and as rendered in order
                           -> [((Int, Kind, Kind), [SV])]                   -- ^ auto-generated tables
                           -> [(Int, ArrayInfo)]                            -- ^ user specified arrays
                           -> [(String, (Maybe [String], SBVType))]         -- ^ uninterpreted functions/constants
                           -> [SMTDef]                                      -- ^ user given axioms/definitions
                           -> SBVPgm                                        -- ^ assignments
                           -> S.Seq (Bool, [(String, String)], SV)          -- ^ extra constraints
                           -> SV                                            -- ^ output variable
                           -> SMTConfig                                     -- ^ configuration
                           -> a

    -- | An instance of SMT-Lib converter; instantiated for SMT-Lib v1 and v2. (And potentially for newer versions in the future.)
    type SMTLibIncConverter a =  ProgInfo                              -- ^ Various prog info
                              -> [NamedSymVar]                         -- ^ inputs
                              -> Set.Set Kind                          -- ^ new kinds
                              -> (CnstMap, [(SV, CV)])                 -- ^ all constants sofar, and new constants
                              -> [(Int, ArrayInfo)]                    -- ^ newly created arrays
                              -> [((Int, Kind, Kind), [SV])]           -- ^ newly created tables
                              -> [(String, (Maybe [String], SBVType))] -- ^ newly created uninterpreted functions/constants
                              -> SBVPgm                                -- ^ assignments
                              -> S.Seq (Bool, [(String, String)], SV)  -- ^ extra constraints
                              -> SMTConfig                             -- ^ configuration
                              -> a

    -- | Create an annotated term
    addAnnotations :: [(String, String)] -> String -> String
    addAnnotations :: [(String, String)] -> String -> String
    addAnnotations []   String
    x = String
    x
    addAnnotations [(String, String)]
    atts String
    x = String
    "(! " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords (((String, String) -> String) -> [(String, String)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, String) -> String
    forall {t :: * -> *}. Foldable t => (String, t Char) -> String
    mkAttr [(String, String)]
    atts) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
      where mkAttr :: (String, t Char) -> String
    mkAttr (String
    a, t Char
    v) = String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " |" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Char -> String) -> t Char -> String
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Char -> String
    sanitize t Char
    v String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "|"
            sanitize :: Char -> String
    sanitize Char
    '|'  = String
    "_bar_"
            sanitize Char
    '\\' = String
    "_backslash_"
            sanitize Char
    c    = [Char
    c]

    -- | Show a millisecond time-out value somewhat nicely
    showTimeoutValue :: Int -> String
    showTimeoutValue :: Int -> String
    showTimeoutValue Int
    i = case (Int
    i Int -> Int -> (Int, Int)
    forall a. Integral a => a -> a -> (a, a)
    `quotRem` Int
    1000000, Int
    i Int -> Int -> (Int, Int)
    forall a. Integral a => a -> a -> (a, a)
    `quotRem` Int
    500000) of
                           ((Int
    s, Int
    0), (Int, Int)
    _)  -> Int -> String -> String
    forall a. Show a => a -> String -> String
    shows Int
    s                              String
    "s"
                           ((Int, Int)
    _, (Int
    hs, Int
    0)) -> Float -> String -> String
    forall a. Show a => a -> String -> String
    shows (Int -> Float
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    hs Float -> Float -> Float
    forall a. Fractional a => a -> a -> a
    / (Float
    2::Float)) String
    "s"
                           ((Int, Int), (Int, Int))
    _            -> Int -> String -> String
    forall a. Show a => a -> String -> String
    shows Int
    i String
    "ms"

    -- | Nicely align a potentially multi-line message with some tag, but prefix with three stars
    alignDiagnostic :: String -> String -> String
    alignDiagnostic :: String -> String -> String
    alignDiagnostic = String -> String -> String -> String
    alignWithPrefix String
    "*** "

    -- | Nicely align a potentially multi-line message with some tag, no prefix.
    alignPlain :: String -> String -> String
    alignPlain :: String -> String -> String
    alignPlain = String -> String -> String -> String
    alignWithPrefix String
    ""

    -- | Align with some given prefix
    alignWithPrefix :: String -> String -> String -> String
    alignWithPrefix :: String -> String -> String -> String
    alignWithPrefix String
    pre String
    tag String
    multi = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    "\n" ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ (String -> String -> String) -> [String] -> [String] -> [String]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith String -> String -> String
    forall a. [a] -> [a] -> [a]
    (++) (String
    tag String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : String -> [String]
    forall a. a -> [a]
    repeat (String
    pre String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate (String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    tag 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
    pre) Char
    ' ')) ((String -> Bool) -> [String] -> [String]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null) (String -> [String]
    lines String
    multi))

    -- | Diagnostic message when verbose
    debug :: MonadIO m => SMTConfig -> [String] -> m ()
    debug :: forall (m :: * -> *). MonadIO m => SMTConfig -> [String] -> m ()
    debug SMTConfig
    cfg
      | Bool -> Bool
    not (SMTConfig -> Bool
    verbose SMTConfig
    cfg)             = m () -> [String] -> m ()
    forall a b. a -> b -> a
    const (() -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())
      | Just String
    f <- SMTConfig -> Maybe String
    redirectVerbose SMTConfig
    cfg = IO () -> m ()
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> ([String] -> IO ()) -> [String] -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String -> IO ()) -> [String] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (String -> String -> IO ()
    appendFile String
    f (String -> IO ()) -> (String -> String) -> String -> IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "\n"))
      | Bool
    True                          = IO () -> m ()
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> ([String] -> IO ()) -> [String] -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String -> IO ()) -> [String] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ String -> IO ()
    putStrLn

    -- | In case the SMT-Lib solver returns a response over multiple lines, compress them so we have
    -- each S-Expression spanning only a single line.
    mergeSExpr :: [String] -> [String]
    mergeSExpr :: [String] -> [String]
    mergeSExpr []       = []
    mergeSExpr (String
    x:[String]
    xs)
     | Int
    d Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 = String
    x String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String] -> [String]
    mergeSExpr [String]
    xs
     | Bool
    True   = let ([String]
    f, [String]
    r) = Int -> [String] -> ([String], [String])
    grab Int
    d [String]
    xs in [String] -> String
    unlines (String
    xString -> [String] -> [String]
    forall a. a -> [a] -> [a]
    :[String]
    f) String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String] -> [String]
    mergeSExpr [String]
    r
     where d :: Int
    d = String -> Int
    parenDiff String
    x

           parenDiff :: String -> Int
           parenDiff :: String -> Int
    parenDiff = Int -> String -> Int
    forall {a}. Num a => a -> String -> a
    go Int
    0
             where go :: a -> String -> a
    go a
    i String
    ""       = a
    i
                   go a
    i (Char
    '(':String
    cs) = let i' :: a
    i'= a
    ia -> a -> a
    forall a. Num a => a -> a -> a
    +a
    1 in a
    i' a -> a -> a
    forall a b. a -> b -> b
    `seq` a -> String -> a
    go a
    i' String
    cs
                   go a
    i (Char
    ')':String
    cs) = let i' :: a
    i'= a
    ia -> a -> a
    forall a. Num a => a -> a -> a
    -a
    1 in a
    i' a -> a -> a
    forall a b. a -> b -> b
    `seq` a -> String -> a
    go a
    i' String
    cs
                   go a
    i (Char
    '"':String
    cs) = a -> String -> a
    go a
    i (String -> String
    skipString String
    cs)
                   go a
    i (Char
    '|':String
    cs) = a -> String -> a
    go a
    i (String -> String
    skipBar String
    cs)
                   go a
    i (Char
    _  :String
    cs) = a -> String -> a
    go a
    i String
    cs

           grab :: Int -> [String] -> ([String], [String])
    grab Int
    i [String]
    ls
             | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    0    = ([], [String]
    ls)
           grab Int
    _ []     = ([], [])
           grab Int
    i (String
    l:[String]
    ls) = let ([String]
    a, [String]
    b) = Int -> [String] -> ([String], [String])
    grab (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +String -> Int
    parenDiff String
    l) [String]
    ls in (String
    lString -> [String] -> [String]
    forall a. a -> [a] -> [a]
    :[String]
    a, [String]
    b)

           skipString :: String -> String
    skipString (Char
    '"':Char
    '"':String
    cs)   = String -> String
    skipString String
    cs
           skipString (Char
    '"':String
    cs)       = String
    cs
           skipString (Char
    _:String
    cs)         = String -> String
    skipString String
    cs
           skipString []             = []             -- Oh dear, line finished, but the string didn't. We're in trouble. Ignore!

           skipBar :: String -> String
    skipBar (Char
    '|':String
    cs) = String
    cs
           skipBar (Char
    _:String
    cs)   = String -> String
    skipBar String
    cs
           skipBar []       = []                     -- Oh dear, line finished, but the string didn't. We're in trouble. Ignore!

    -- | An exception thrown from SBV. If the solver ever responds with a non-success value for a command,
    -- SBV will throw an 'SBVException', it so the user can process it as required. The provided 'Show' instance
    -- will render the failure nicely. Note that if you ever catch this exception, the solver is no longer alive:
    -- You should either -- throw the exception up, or do other proper clean-up before continuing.
    data SBVException = SBVException {
                              SBVException -> String
    sbvExceptionDescription :: String
                            , SBVException -> Maybe String
    sbvExceptionSent        :: Maybe String
                            , SBVException -> Maybe String
    sbvExceptionExpected    :: Maybe String
                            , SBVException -> Maybe String
    sbvExceptionReceived    :: Maybe String
                            , SBVException -> Maybe String
    sbvExceptionStdOut      :: Maybe String
                            , SBVException -> Maybe String
    sbvExceptionStdErr      :: Maybe String
                            , SBVException -> Maybe ExitCode
    sbvExceptionExitCode    :: Maybe ExitCode
                            , SBVException -> SMTConfig
    sbvExceptionConfig      :: SMTConfig
                            , SBVException -> Maybe [String]
    sbvExceptionReason      :: Maybe [String]
                            , SBVException -> Maybe [String]
    sbvExceptionHint        :: Maybe [String]
                            }

    -- | SBVExceptions are throwable. A simple "show" will render this exception nicely
    -- though of course you can inspect the individual fields as necessary.
    instance C.Exception SBVException

    -- | A fairly nice rendering of the exception, for display purposes.
    instance Show SBVException where
     show :: SBVException -> String
    show SBVException { String
    sbvExceptionDescription :: SBVException -> String
    sbvExceptionDescription :: String
    sbvExceptionDescription
                       , Maybe String
    sbvExceptionSent :: SBVException -> Maybe String
    sbvExceptionSent :: Maybe String
    sbvExceptionSent
                       , Maybe String
    sbvExceptionExpected :: SBVException -> Maybe String
    sbvExceptionExpected :: Maybe String
    sbvExceptionExpected
                       , Maybe String
    sbvExceptionReceived :: SBVException -> Maybe String
    sbvExceptionReceived :: Maybe String
    sbvExceptionReceived
                       , Maybe String
    sbvExceptionStdOut :: SBVException -> Maybe String
    sbvExceptionStdOut :: Maybe String
    sbvExceptionStdOut
                       , Maybe String
    sbvExceptionStdErr :: SBVException -> Maybe String
    sbvExceptionStdErr :: Maybe String
    sbvExceptionStdErr
                       , Maybe ExitCode
    sbvExceptionExitCode :: SBVException -> Maybe ExitCode
    sbvExceptionExitCode :: Maybe ExitCode
    sbvExceptionExitCode
                       , SMTConfig
    sbvExceptionConfig :: SBVException -> SMTConfig
    sbvExceptionConfig :: SMTConfig
    sbvExceptionConfig
                       , Maybe [String]
    sbvExceptionReason :: SBVException -> Maybe [String]
    sbvExceptionReason :: Maybe [String]
    sbvExceptionReason
                       , Maybe [String]
    sbvExceptionHint :: SBVException -> Maybe [String]
    sbvExceptionHint :: Maybe [String]
    sbvExceptionHint
                       }

             = let grp1 :: [String]
    grp1 = [ String
    ""
                          , String
    "*** Data.SBV: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    sbvExceptionDescription String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ":"
                          ]

                   grp2 :: [String]
    grp2 =  [String
    "***    Sent      : " String -> String -> String
    `alignDiagnostic` String
    snt     | Just String
    snt  <- [Maybe String
    sbvExceptionSent],     Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ String -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null String
    snt ]
                        [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String
    "***    Expected  : " String -> String -> String
    `alignDiagnostic` String
    excp    | Just String
    excp <- [Maybe String
    sbvExceptionExpected], Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ String -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null String
    excp]
                        [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String
    "***    Received  : " String -> String -> String
    `alignDiagnostic` String
    rcvd    | Just String
    rcvd <- [Maybe String
    sbvExceptionReceived], Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ String -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null String
    rcvd]

                   grp3 :: [String]
    grp3 =  [String
    "***    Stdout    : " String -> String -> String
    `alignDiagnostic` String
    out     | Just String
    out  <- [Maybe String
    sbvExceptionStdOut],   Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ String -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null String
    out ]
                        [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String
    "***    Stderr    : " String -> String -> String
    `alignDiagnostic` String
    err     | Just String
    err  <- [Maybe String
    sbvExceptionStdErr],   Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ String -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null String
    err ]
                        [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String
    "***    Exit code : " String -> String -> String
    `alignDiagnostic` ExitCode -> String
    forall a. Show a => a -> String
    show ExitCode
    ec | Just ExitCode
    ec   <- [Maybe ExitCode
    sbvExceptionExitCode]                 ]
                        [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String
    "***    Executable: " String -> String -> String
    `alignDiagnostic` SMTSolver -> String
    executable (SMTConfig -> SMTSolver
    solver SMTConfig
    sbvExceptionConfig)                                   ]
                        [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String
    "***    Options   : " String -> String -> String
    `alignDiagnostic` [String] -> String
    joinArgs (SMTSolver -> SMTConfig -> [String]
    options (SMTConfig -> SMTSolver
    solver SMTConfig
    sbvExceptionConfig) SMTConfig
    sbvExceptionConfig)        ]

                   grp4 :: [String]
    grp4 =  [String
    "***    Reason    : " String -> String -> String
    `alignDiagnostic` [String] -> String
    unlines [String]
    rsn | Just [String]
    rsn <- [Maybe [String]
    sbvExceptionReason]]
                        [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String
    "***    Hint      : " String -> String -> String
    `alignDiagnostic` [String] -> String
    unlines [String]
    hnt | Just [String]
    hnt <- [Maybe [String]
    sbvExceptionHint  ]]

                   join :: [[String]] -> [String]
    join []     = []
                   join [[String]
    x]    = [String]
    x
                   join ([String]
    g:[[String]]
    gs) = case [[String]] -> [String]
    join [[String]]
    gs of
                                   []    -> [String]
    g
                                   [String]
    rest  -> [String]
    g [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String
    "***"] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    rest

              in [String] -> String
    unlines ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ [[String]] -> [String]
    join [[String]
    grp1, [String]
    grp2, [String]
    grp3, [String]
    grp4]