{-# 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)
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(..))
type SMTLibConverter a = QueryContext
-> Set.Set Kind
-> Bool
-> [String]
-> ([(Quantifier, NamedSymVar)], [NamedSymVar])
-> [Either SV (SV, [SV])]
-> [(SV, CV)]
-> [((Int, Kind, Kind), [SV])]
-> [(Int, ArrayInfo)]
-> [(String, SBVType)]
-> [(String, [String])]
-> SBVPgm
-> S.Seq (Bool, [(String, String)], SV)
-> SV
-> SMTConfig
-> a
type SMTLibIncConverter a = [NamedSymVar]
-> Set.Set Kind
-> [(SV, CV)]
-> [(Int, ArrayInfo)]
-> [((Int, Kind, Kind), [SV])]
-> [(String, SBVType)]
-> SBVPgm
-> S.Seq (Bool, [(String, String)], SV)
-> SMTConfig
-> a
addAnnotations :: [(String, String)] -> String -> String
addAnnotations :: [(String, String)] -> String -> String
addAnnotations [] x :: String
x = String
x
addAnnotations atts :: [(String, String)]
atts x :: String
x = "(! " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " 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]
++ ")"
where mkAttr :: (String, t Char) -> String
mkAttr (a :: String
a, v :: t Char
v) = String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ " |" 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]
++ "|"
sanitize :: Char -> String
sanitize '|' = "_bar_"
sanitize '\\' = "_backslash_"
sanitize c :: Char
c = [Char
c]
showTimeoutValue :: Int -> String
showTimeoutValue :: Int -> String
showTimeoutValue i :: Int
i = case (Int
i Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
`quotRem` 1000000, Int
i Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
`quotRem` 500000) of
((s :: Int
s, 0), _) -> Int -> String -> String
forall a. Show a => a -> String -> String
shows Int
s "s"
(_, (hs :: Int
hs, 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
/ (2::Float)) "s"
_ -> Int -> String -> String
forall a. Show a => a -> String -> String
shows Int
i "ms"
alignDiagnostic :: String -> String -> String
alignDiagnostic :: String -> String -> String
alignDiagnostic = String -> String -> String -> String
alignWithPrefix "*** "
alignPlain :: String -> String -> String
alignPlain :: String -> String -> String
alignPlain = String -> String -> String -> String
alignWithPrefix ""
alignWithPrefix :: String -> String -> String -> String
alignWithPrefix :: String -> String -> String -> String
alignWithPrefix pre :: String
pre tag :: String
tag multi :: String
multi = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\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 (t :: * -> *) a. Foldable t => t a -> Int
length String
tag Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
pre) ' ')) ((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 (t :: * -> *) a. Foldable t => t a -> Bool
null) (String -> [String]
lines String
multi))
debug :: MonadIO m => SMTConfig -> [String] -> m ()
debug :: SMTConfig -> [String] -> m ()
debug cfg :: SMTConfig
cfg
| Bool -> Bool
not (SMTConfig -> Bool
verbose SMTConfig
cfg) = m () -> [String] -> m ()
forall a b. a -> b -> a
const (() -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
| Just f :: String
f <- SMTConfig -> Maybe String
redirectVerbose SMTConfig
cfg = IO () -> m ()
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]
++ "\n"))
| Bool
True = IO () -> m ()
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
mergeSExpr :: [String] -> [String]
mergeSExpr :: [String] -> [String]
mergeSExpr [] = []
mergeSExpr (x :: String
x:xs :: [String]
xs)
| Int
d Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = String
x String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String] -> [String]
mergeSExpr [String]
xs
| Bool
True = let (f :: [String]
f, r :: [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 t. Num t => t -> String -> t
go 0
where go :: t -> String -> t
go i :: t
i "" = t
i
go i :: t
i ('(':cs :: String
cs) = let i' :: t
i'= t
it -> t -> t
forall a. Num a => a -> a -> a
+1 in t
i' t -> t -> t
forall a b. a -> b -> b
`seq` t -> String -> t
go t
i' String
cs
go i :: t
i (')':cs :: String
cs) = let i' :: t
i'= t
it -> t -> t
forall a. Num a => a -> a -> a
-1 in t
i' t -> t -> t
forall a b. a -> b -> b
`seq` t -> String -> t
go t
i' String
cs
go i :: t
i ('"':cs :: String
cs) = t -> String -> t
go t
i (String -> String
skipString String
cs)
go i :: t
i ('|':cs :: String
cs) = t -> String -> t
go t
i (String -> String
skipBar String
cs)
go i :: t
i (_ :cs :: String
cs) = t -> String -> t
go t
i String
cs
grab :: Int -> [String] -> ([String], [String])
grab i :: Int
i ls :: [String]
ls
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 0 = ([], [String]
ls)
grab _ [] = ([], [])
grab i :: Int
i (l :: String
l:ls :: [String]
ls) = let (a :: [String]
a, b :: [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 ('"':'"':cs :: String
cs) = String -> String
skipString String
cs
skipString ('"':cs :: String
cs) = String
cs
skipString (_:cs :: String
cs) = String -> String
skipString String
cs
skipString [] = []
skipBar :: String -> String
skipBar ('|':cs :: String
cs) = String
cs
skipBar (_:cs :: String
cs) = String -> String
skipBar String
cs
skipBar [] = []
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]
}
instance C.Exception SBVException
instance Show SBVException where
show :: SBVException -> String
show SBVException { String
sbvExceptionDescription :: String
sbvExceptionDescription :: SBVException -> String
sbvExceptionDescription
, Maybe String
sbvExceptionSent :: Maybe String
sbvExceptionSent :: SBVException -> Maybe String
sbvExceptionSent
, Maybe String
sbvExceptionExpected :: Maybe String
sbvExceptionExpected :: SBVException -> Maybe String
sbvExceptionExpected
, Maybe String
sbvExceptionReceived :: Maybe String
sbvExceptionReceived :: SBVException -> Maybe String
sbvExceptionReceived
, Maybe String
sbvExceptionStdOut :: Maybe String
sbvExceptionStdOut :: SBVException -> Maybe String
sbvExceptionStdOut
, Maybe String
sbvExceptionStdErr :: Maybe String
sbvExceptionStdErr :: SBVException -> Maybe String
sbvExceptionStdErr
, Maybe ExitCode
sbvExceptionExitCode :: Maybe ExitCode
sbvExceptionExitCode :: SBVException -> Maybe ExitCode
sbvExceptionExitCode
, SMTConfig
sbvExceptionConfig :: SMTConfig
sbvExceptionConfig :: SBVException -> SMTConfig
sbvExceptionConfig
, Maybe [String]
sbvExceptionReason :: Maybe [String]
sbvExceptionReason :: SBVException -> Maybe [String]
sbvExceptionReason
, Maybe [String]
sbvExceptionHint :: Maybe [String]
sbvExceptionHint :: SBVException -> Maybe [String]
sbvExceptionHint
}
= let grp1 :: [String]
grp1 = [ ""
, "*** Data.SBV: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sbvExceptionDescription String -> String -> String
forall a. [a] -> [a] -> [a]
++ ":"
]
grp2 :: [String]
grp2 = ["*** Sent : " String -> String -> String
`alignDiagnostic` String
snt | Just snt :: String
snt <- [Maybe String
sbvExceptionSent], Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
snt ]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["*** Expected : " String -> String -> String
`alignDiagnostic` String
excp | Just excp :: String
excp <- [Maybe String
sbvExceptionExpected], Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
excp]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["*** Received : " String -> String -> String
`alignDiagnostic` String
rcvd | Just rcvd :: String
rcvd <- [Maybe String
sbvExceptionReceived], Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
rcvd]
grp3 :: [String]
grp3 = ["*** Stdout : " String -> String -> String
`alignDiagnostic` String
out | Just out :: String
out <- [Maybe String
sbvExceptionStdOut], Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
out ]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["*** Stderr : " String -> String -> String
`alignDiagnostic` String
err | Just err :: String
err <- [Maybe String
sbvExceptionStdErr], Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
err ]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["*** Exit code : " String -> String -> String
`alignDiagnostic` ExitCode -> String
forall a. Show a => a -> String
show ExitCode
ec | Just ec :: ExitCode
ec <- [Maybe ExitCode
sbvExceptionExitCode] ]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["*** Executable: " String -> String -> String
`alignDiagnostic` SMTSolver -> String
executable (SMTConfig -> SMTSolver
solver SMTConfig
sbvExceptionConfig) ]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["*** Options : " String -> String -> String
`alignDiagnostic` [String] -> String
joinArgs (SMTSolver -> SMTConfig -> [String]
options (SMTConfig -> SMTSolver
solver SMTConfig
sbvExceptionConfig) SMTConfig
sbvExceptionConfig) ]
grp4 :: [String]
grp4 = ["*** Reason : " String -> String -> String
`alignDiagnostic` [String] -> String
unlines [String]
rsn | Just rsn :: [String]
rsn <- [Maybe [String]
sbvExceptionReason]]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["*** Hint : " String -> String -> String
`alignDiagnostic` [String] -> String
unlines [String]
hnt | Just hnt :: [String]
hnt <- [Maybe [String]
sbvExceptionHint ]]
join :: [[String]] -> [String]
join [] = []
join [x :: [String]
x] = [String]
x
join (g :: [String]
g:gs :: [[String]]
gs) = case [[String]] -> [String]
join [[String]]
gs of
[] -> [String]
g
rest :: [String]
rest -> [String]
g [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["***"] [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]