-----------------------------------------------------------------------------
-- |
-- 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
        , witnessName
        , addAnnotations
        , showTimeoutValue
        , alignDiagnostic
        , alignPlain
        , debug
        , mergeSExpr
        , SBVException(..)
        , startTranscript
        , finalizeTranscript
        , recordTranscript
        , recordException
        , recordEndTime
        , TranscriptMsg(..)
       )
       where

import qualified Control.Exception as C

import Control.Monad (zipWithM_)
import Control.Monad.Trans (MonadIO, liftIO)

import Data.SBV.Core.Data
import Data.SBV.Core.Symbolic (QueryContext, CnstMap, SMTDef, ResultInp(..), ProgInfo(..), startTime)

import Data.SBV.Utils.Lib   (joinArgs)
import Data.SBV.Utils.TDiff (Timing(..), showTDiff)

import Data.IORef (writeIORef)
import Data.Time  (getZonedTime, defaultTimeLocale, formatTime, diffUTCTime, getCurrentTime)

import Data.Char  (isSpace)
import Data.Maybe (fromMaybe)
import Data.List  (intercalate)

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

import System.Directory (findExecutable)
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
                       -> [(String, (Bool, Maybe [String], SBVType))]    -- ^ uninterpreted functions/constants
                       -> [(SMTDef, SBVType)]                            -- ^ 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, Kind, Kind), [SV])]                 -- ^ newly created tables
                          -> [(String, (Bool, Maybe [String], SBVType))] -- ^ newly created uninterpreted functions/constants
                          -> SBVPgm                                      -- ^ assignments
                          -> S.Seq (Bool, [(String, String)], SV)        -- ^ extra constraints
                          -> SMTConfig                                   -- ^ configuration
                          -> a

-- | The name of a witness for a type. We should make sure this doesn't conflict any reserved names, but I think the chances of that is
-- pretty low anyhow.
witnessName :: String -> String
witnessName :: String -> String
witnessName = (String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_witness")

-- | 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 (Int -> String -> String
forall a. Int -> [a] -> [a]
drop Int
1 ((Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'\n') 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 t'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]

-- | Compute and report the end time
recordEndTime :: SMTConfig -> State -> IO ()
recordEndTime :: SMTConfig -> State -> IO ()
recordEndTime SMTConfig{Timing
timing :: Timing
timing :: SMTConfig -> Timing
timing} State
state = case Timing
timing of
                                           Timing
NoTiming        -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                           Timing
PrintTiming     -> do e <- IO NominalDiffTime
elapsed
                                                                 putStrLn $ "*** SBV: Elapsed time: " ++ showTDiff e
                                           SaveTiming IORef NominalDiffTime
here -> IORef NominalDiffTime -> NominalDiffTime -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef NominalDiffTime
here (NominalDiffTime -> IO ()) -> IO NominalDiffTime -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO NominalDiffTime
elapsed
  where elapsed :: IO NominalDiffTime
elapsed = IO UTCTime
getCurrentTime IO UTCTime -> (UTCTime -> IO NominalDiffTime) -> IO NominalDiffTime
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \UTCTime
end -> NominalDiffTime -> IO NominalDiffTime
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (NominalDiffTime -> IO NominalDiffTime)
-> NominalDiffTime -> IO NominalDiffTime
forall a b. (a -> b) -> a -> b
$ UTCTime -> UTCTime -> NominalDiffTime
diffUTCTime UTCTime
end (State -> UTCTime
startTime State
state)

-- | Start a transcript file, if requested.
startTranscript :: Maybe FilePath -> SMTConfig -> IO ()
startTranscript :: Maybe String -> SMTConfig -> IO ()
startTranscript Maybe String
Nothing  SMTConfig
_   = () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
startTranscript (Just String
f) SMTConfig
cfg = do ts <- ZonedTime -> String
forall a. Show a => a -> String
show (ZonedTime -> String) -> IO ZonedTime -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO ZonedTime
getZonedTime
                                  mbExecPath <- findExecutable (executable (solver cfg))
                                  writeFile f $ start ts mbExecPath
  where SMTSolver{Solver
name :: Solver
name :: SMTSolver -> Solver
name, SMTConfig -> [String]
options :: SMTSolver -> SMTConfig -> [String]
options :: SMTConfig -> [String]
options} = SMTConfig -> SMTSolver
solver SMTConfig
cfg
        start :: String -> Maybe String -> String
start String
ts Maybe String
mbPath = [String] -> String
unlines [ String
";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                                  , String
";;; SBV: Starting at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ts
                                  , String
";;;"
                                  , String
";;;           Solver    : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Solver -> String
forall a. Show a => a -> String
show Solver
name
                                  , String
";;;           Executable: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
"Unable to locate the executable" Maybe String
mbPath
                                  , String
";;;           Options   : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (SMTConfig -> [String]
options SMTConfig
cfg [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ SMTConfig -> [String]
extraArgs SMTConfig
cfg)
                                  , String
";;;"
                                  , String
";;; This file is an auto-generated loadable SMT-Lib file."
                                  , String
";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                                  , String
""
                                  ]

-- | Finish up the transcript file.
finalizeTranscript :: Maybe FilePath -> ExitCode -> IO ()
finalizeTranscript :: Maybe String -> ExitCode -> IO ()
finalizeTranscript Maybe String
Nothing  ExitCode
_  = () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
finalizeTranscript (Just String
f) ExitCode
ec = do ts <- ZonedTime -> String
forall a. Show a => a -> String
show (ZonedTime -> String) -> IO ZonedTime -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO ZonedTime
getZonedTime
                                    appendFile f $ end ts
  where end :: String -> String
end String
ts = [String] -> String
unlines [ String
""
                         , String
";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                         , String
";;;"
                         , String
";;; SBV: Finished at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ts
                         , String
";;;"
                         , String
";;; Exit code: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ExitCode -> String
forall a. Show a => a -> String
show ExitCode
ec
                         , String
";;;"
                         , String
";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                         ]

-- Kind of things we can record
data TranscriptMsg = SentMsg  String (Maybe Int) -- ^ Message sent, and time-out if any
                   | RecvMsg  String             -- ^ Message received
                   | DebugMsg String             -- ^ A debug message; neither sent nor received

-- If requested, record in the transcript file
recordTranscript :: Maybe FilePath -> TranscriptMsg -> IO ()
recordTranscript :: Maybe String -> TranscriptMsg -> IO ()
recordTranscript Maybe String
Nothing  TranscriptMsg
_ = () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
recordTranscript (Just String
f) TranscriptMsg
m = do tsPre <- TimeLocale -> String -> ZonedTime -> String
forall t. FormatTime t => TimeLocale -> String -> t -> String
formatTime TimeLocale
defaultTimeLocale String
"; [%T%Q" (ZonedTime -> String) -> IO ZonedTime -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO ZonedTime
getZonedTime
                                 let ts = Int -> String -> String
forall a. Int -> [a] -> [a]
take Int
15 (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
tsPre String -> String -> String
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. a -> [a]
repeat Char
'0'
                                 case m of
                                   SentMsg String
sent Maybe Int
mbTimeOut  -> String -> String -> IO ()
appendFile String
f (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (String
ts String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"] " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Maybe Int -> String
to Maybe Int
mbTimeOut String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Sending:") String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String -> [String]
lines String
sent
                                   RecvMsg String
recv            -> String -> String -> IO ()
appendFile String
f (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ case String -> [String]
lines ((Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace String
recv) of
                                                                                        []  -> [String
ts String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"] Received: <NO RESPONSE>"]  -- can't really happen.
                                                                                        [String
x] -> [String
ts String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"] Received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x]
                                                                                        [String]
xs  -> (String
ts String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"] Received: ") String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
";   " String -> String -> String
forall a. [a] -> [a] -> [a]
++) [String]
xs
                                   DebugMsg String
msg            -> let tag :: String
tag = String
ts String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"] "
                                                                  emp :: String
emp = Char
';' Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> String -> String
forall a. Int -> [a] -> [a]
drop Int
1 ((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map (Char -> Char -> Char
forall a b. a -> b -> a
const Char
' ') String
tag)
                                                              in (String -> String -> IO ()) -> [String] -> [String] -> IO ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (\String
t String
l -> String -> String -> IO ()
appendFile String
f (String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n")) (String
tag String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String -> [String]
forall a. a -> [a]
repeat String
emp) (String -> [String]
lines String
msg)
        where to :: Maybe Int -> String
to Maybe Int
Nothing  = String
""
              to (Just Int
i) = String
"[Timeout: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
showTimeoutValue Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"] "
{-# INLINE recordTranscript #-}

-- Record the exception
recordException :: Maybe FilePath -> String -> IO ()
recordException :: Maybe String -> String -> IO ()
recordException Maybe String
Nothing  String
_ = () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
recordException (Just String
f) String
m = do ts <- ZonedTime -> String
forall a. Show a => a -> String
show (ZonedTime -> String) -> IO ZonedTime -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO ZonedTime
getZonedTime
                                appendFile f $ exc ts
  where exc :: String -> String
exc String
ts = [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [ String
""
                           , String
";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                           , String
";;;"
                           , String
";;; SBV: Caught an exception at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ts
                           , String
";;;"
                           ]
                        [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
";;;   " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
l | String
l <- (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (String -> [String]
lines String
m) ]
                        [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
";;;"
                           , String
";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                           ]