-----------------------------------------------------------------------------
-- |
-- 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      #-}
{-# LANGUAGE OverloadedStrings   #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.SMT.Utils (
          SMTLibConverter
        , SMTLibIncConverter
        , 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 qualified Data.Text as T
import           Data.Text (Text)

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
                       -> [(String, (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

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

-- | Show a millisecond time-out value somewhat nicely
showTimeoutValue :: Int -> String
showTimeoutValue :: Int -> [Char]
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 -> [Char] -> [Char]
forall a. Show a => a -> [Char] -> [Char]
shows Int
s                              [Char]
"s"
                       ((Int, Int)
_, (Int
hs, Int
0)) -> Float -> [Char] -> [Char]
forall a. Show a => a -> [Char] -> [Char]
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)) [Char]
"s"
                       ((Int, Int), (Int, Int))
_            -> Int -> [Char] -> [Char]
forall a. Show a => a -> [Char] -> [Char]
shows Int
i [Char]
"ms"

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

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

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

-- | Diagnostic message when verbose
debug :: MonadIO m => SMTConfig -> [String] -> m ()
debug :: forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
debug SMTConfig
cfg
  | Bool -> Bool
not (SMTConfig -> Bool
verbose SMTConfig
cfg)             = m () -> [[Char]] -> m ()
forall a b. a -> b -> a
const (() -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
  | Just [Char]
f <- SMTConfig -> Maybe [Char]
redirectVerbose SMTConfig
cfg = IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> ([[Char]] -> IO ()) -> [[Char]] -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> IO ()) -> [[Char]] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Char] -> [Char] -> IO ()
appendFile [Char]
f ([Char] -> IO ()) -> ([Char] -> [Char]) -> [Char] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"))
  | Bool
True                          = IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> ([[Char]] -> IO ()) -> [[Char]] -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> IO ()) -> [[Char]] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [Char] -> 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 :: [[Char]] -> [[Char]]
mergeSExpr []       = []
mergeSExpr ([Char]
x:[[Char]]
xs)
 | Int
d Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = [Char]
x [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: [[Char]] -> [[Char]]
mergeSExpr [[Char]]
xs
 | Bool
True   = let ([[Char]]
f, [[Char]]
r) = Int -> [[Char]] -> ([[Char]], [[Char]])
grab Int
d [[Char]]
xs in [[Char]] -> [Char]
unlines ([Char]
x[Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
:[[Char]]
f) [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: [[Char]] -> [[Char]]
mergeSExpr [[Char]]
r
 where d :: Int
d = [Char] -> Int
parenDiff [Char]
x

       parenDiff :: String -> Int
       parenDiff :: [Char] -> Int
parenDiff = Int -> [Char] -> Int
forall {a}. Num a => a -> [Char] -> a
go Int
0
         where go :: a -> [Char] -> a
go a
i [Char]
""       = a
i
               go a
i (Char
'(':[Char]
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 -> [Char] -> a
go a
i' [Char]
cs
               go a
i (Char
')':[Char]
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 -> [Char] -> a
go a
i' [Char]
cs
               go a
i (Char
'"':[Char]
cs) = a -> [Char] -> a
go a
i ([Char] -> [Char]
skipString [Char]
cs)
               go a
i (Char
'|':[Char]
cs) = a -> [Char] -> a
go a
i ([Char] -> [Char]
skipBar [Char]
cs)
               go a
i (Char
';':[Char]
cs) = a -> [Char] -> a
go a
i (Int -> [Char] -> [Char]
forall a. Int -> [a] -> [a]
drop Int
1 ((Char -> Bool) -> [Char] -> [Char]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'\n') [Char]
cs))
               go a
i (Char
_  :[Char]
cs) = a -> [Char] -> a
go a
i [Char]
cs

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

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

       skipBar :: [Char] -> [Char]
skipBar (Char
'|':[Char]
cs) = [Char]
cs
       skipBar (Char
_:[Char]
cs)   = [Char] -> [Char]
skipBar [Char]
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 -> [Char]
sbvExceptionDescription :: String
                        , SBVException -> Maybe [Char]
sbvExceptionSent        :: Maybe String
                        , SBVException -> Maybe [Char]
sbvExceptionExpected    :: Maybe String
                        , SBVException -> Maybe [Char]
sbvExceptionReceived    :: Maybe String
                        , SBVException -> Maybe [Char]
sbvExceptionStdOut      :: Maybe String
                        , SBVException -> Maybe [Char]
sbvExceptionStdErr      :: Maybe String
                        , SBVException -> Maybe ExitCode
sbvExceptionExitCode    :: Maybe ExitCode
                        , SBVException -> SMTConfig
sbvExceptionConfig      :: SMTConfig
                        , SBVException -> Maybe [[Char]]
sbvExceptionReason      :: Maybe [String]
                        , SBVException -> Maybe [[Char]]
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 -> [Char]
show SBVException { [Char]
sbvExceptionDescription :: SBVException -> [Char]
sbvExceptionDescription :: [Char]
sbvExceptionDescription
                   , Maybe [Char]
sbvExceptionSent :: SBVException -> Maybe [Char]
sbvExceptionSent :: Maybe [Char]
sbvExceptionSent
                   , Maybe [Char]
sbvExceptionExpected :: SBVException -> Maybe [Char]
sbvExceptionExpected :: Maybe [Char]
sbvExceptionExpected
                   , Maybe [Char]
sbvExceptionReceived :: SBVException -> Maybe [Char]
sbvExceptionReceived :: Maybe [Char]
sbvExceptionReceived
                   , Maybe [Char]
sbvExceptionStdOut :: SBVException -> Maybe [Char]
sbvExceptionStdOut :: Maybe [Char]
sbvExceptionStdOut
                   , Maybe [Char]
sbvExceptionStdErr :: SBVException -> Maybe [Char]
sbvExceptionStdErr :: Maybe [Char]
sbvExceptionStdErr
                   , Maybe ExitCode
sbvExceptionExitCode :: SBVException -> Maybe ExitCode
sbvExceptionExitCode :: Maybe ExitCode
sbvExceptionExitCode
                   , SMTConfig
sbvExceptionConfig :: SBVException -> SMTConfig
sbvExceptionConfig :: SMTConfig
sbvExceptionConfig
                   , Maybe [[Char]]
sbvExceptionReason :: SBVException -> Maybe [[Char]]
sbvExceptionReason :: Maybe [[Char]]
sbvExceptionReason
                   , Maybe [[Char]]
sbvExceptionHint :: SBVException -> Maybe [[Char]]
sbvExceptionHint :: Maybe [[Char]]
sbvExceptionHint
                   }

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

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

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

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

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

          in [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [[[Char]]] -> [[Char]]
forall {a}. IsString a => [[a]] -> [a]
join [[[Char]]
grp1, [[Char]]
grp2, [[Char]]
grp3, [[Char]]
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 NominalDiffTime
e <- IO NominalDiffTime
elapsed
                                                                 [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"*** SBV: Elapsed time: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ NominalDiffTime -> [Char]
showTDiff NominalDiffTime
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 [Char] -> SMTConfig -> IO ()
startTranscript Maybe [Char]
Nothing  SMTConfig
_   = () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
startTranscript (Just [Char]
f) SMTConfig
cfg = do [Char]
ts <- ZonedTime -> [Char]
forall a. Show a => a -> [Char]
show (ZonedTime -> [Char]) -> IO ZonedTime -> IO [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO ZonedTime
getZonedTime
                                  Maybe [Char]
mbExecPath <- [Char] -> IO (Maybe [Char])
findExecutable (SMTSolver -> [Char]
executable (SMTConfig -> SMTSolver
solver SMTConfig
cfg))
                                  [Char] -> [Char] -> IO ()
writeFile [Char]
f ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Maybe [Char] -> [Char]
start [Char]
ts Maybe [Char]
mbExecPath
  where SMTSolver{Solver
name :: Solver
name :: SMTSolver -> Solver
name, SMTConfig -> [[Char]]
options :: SMTSolver -> SMTConfig -> [[Char]]
options :: SMTConfig -> [[Char]]
options} = SMTConfig -> SMTSolver
solver SMTConfig
cfg
        start :: [Char] -> Maybe [Char] -> [Char]
start [Char]
ts Maybe [Char]
mbPath = [[Char]] -> [Char]
unlines [ [Char]
";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                                  , [Char]
";;; SBV: Starting at " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
ts
                                  , [Char]
";;;"
                                  , [Char]
";;;           Solver    : " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Solver -> [Char]
forall a. Show a => a -> [Char]
show Solver
name
                                  , [Char]
";;;           Executable: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> Maybe [Char] -> [Char]
forall a. a -> Maybe a -> a
fromMaybe [Char]
"Unable to locate the executable" Maybe [Char]
mbPath
                                  , [Char]
";;;           Options   : " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
unwords (SMTConfig -> [[Char]]
options SMTConfig
cfg [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ SMTConfig -> [[Char]]
extraArgs SMTConfig
cfg)
                                  , [Char]
";;;"
                                  , [Char]
";;; This file is an auto-generated loadable SMT-Lib file."
                                  , [Char]
";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                                  , [Char]
""
                                  ]

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

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

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