-----------------------------------------------------------------------------
-- |
-- 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)
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?
                       -> Set.Set Kind                                  -- ^ Kinds used in the problem
                       -> Bool                                          -- ^ is this a sat problem?
                       -> [String]                                      -- ^ extra comments to place on top
                       -> ([(Quantifier, NamedSymVar)], [NamedSymVar])  -- ^ inputs and aliasing names and trackers
                       -> [Either SV (SV, [SV])]                        -- ^ skolemized inputs
                       -> (CnstMap, [(SV, CV)])                         -- ^ constants. The map, and as rendered in order
                       -> [((Int, Kind, Kind), [SV])]                   -- ^ auto-generated tables
                       -> [(Int, ArrayInfo)]                            -- ^ user specified arrays
                       -> [(String, SBVType)]                           -- ^ uninterpreted functions/constants
                       -> [(Bool, String, [String])]                    -- ^ 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 =  [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, 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 (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) 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 (t :: * -> *) a. Foldable t => t a -> Bool
null) (String -> [String]
lines String
multi))

-- | Diagnostic message when verbose
debug :: MonadIO m => SMTConfig -> [String] -> m ()
debug :: 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 (m :: * -> *) a. Monad m => a -> m a
return ())
  | Just 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]
++ String
"\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

-- | 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 t. Num t => t -> String -> t
go Int
0
         where go :: t -> String -> t
go t
i String
""       = t
i
               go t
i (Char
'(':String
cs) = let i' :: t
i'= t
it -> t -> t
forall a. Num a => a -> a -> a
+t
1 in t
i' t -> t -> t
`seq` t -> String -> t
go t
i' String
cs
               go t
i (Char
')':String
cs) = let i' :: t
i'= t
it -> t -> t
forall a. Num a => a -> a -> a
-t
1 in t
i' t -> t -> t
`seq` t -> String -> t
go t
i' String
cs
               go t
i (Char
'"':String
cs) = t -> String -> t
go t
i (String -> String
skipString String
cs)
               go t
i (Char
'|':String
cs) = t -> String -> t
go t
i (String -> String
skipBar String
cs)
               go t
i (Char
_  :String
cs) = t -> String -> t
go t
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 :: 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 = [ 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 (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 (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 (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 (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 (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]