-----------------------------------------------------------------------------
-- |
-- 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)
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
                       -> [(SV, CV)]                                    -- ^ constants
                       -> [((Int, Kind, Kind), [SV])]                   -- ^ auto-generated tables
                       -> [(Int, ArrayInfo)]                            -- ^ user specified arrays
                       -> [(String, SBVType)]                           -- ^ uninterpreted functions/constants
                       -> [(String, [String])]                          -- ^ user given axioms
                       -> 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
                          -> [(SV, CV)]                            -- ^ 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 []   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]

-- | Show a millisecond time-out value somewhat nicely
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"

-- | 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 "*** "

-- | 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 ""

-- | Align with some given prefix
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))

-- | Diagnostic message when verbose
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

-- | 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 (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 []             = []             -- Oh dear, line finished, but the string didn't. We're in trouble. Ignore!

       skipBar :: String -> String
skipBar ('|':cs :: String
cs) = String
cs
       skipBar (_:cs :: 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 = [ ""
                      , "*** 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]