sbv-8.4: Data/SBV/SMT/Utils.hs
-----------------------------------------------------------------------------
-- |
-- 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 [] x = x
addAnnotations atts x = "(! " ++ x ++ " " ++ unwords (map mkAttr atts) ++ ")"
where mkAttr (a, v) = a ++ " |" ++ concatMap sanitize v ++ "|"
sanitize '|' = "_bar_"
sanitize '\\' = "_backslash_"
sanitize c = [c]
-- | Show a millisecond time-out value somewhat nicely
showTimeoutValue :: Int -> String
showTimeoutValue i = case (i `quotRem` 1000000, i `quotRem` 500000) of
((s, 0), _) -> shows s "s"
(_, (hs, 0)) -> shows (fromIntegral hs / (2::Float)) "s"
_ -> shows i "ms"
-- | Nicely align a potentially multi-line message with some tag, but prefix with three stars
alignDiagnostic :: String -> String -> String
alignDiagnostic = alignWithPrefix "*** "
-- | Nicely align a potentially multi-line message with some tag, no prefix.
alignPlain :: String -> String -> String
alignPlain = alignWithPrefix ""
-- | Align with some given prefix
alignWithPrefix :: String -> String -> String -> String
alignWithPrefix pre tag multi = intercalate "\n" $ zipWith (++) (tag : repeat (pre ++ replicate (length tag - length pre) ' ')) (filter (not . null) (lines multi))
-- | Diagnostic message when verbose
debug :: MonadIO m => SMTConfig -> [String] -> m ()
debug cfg
| not (verbose cfg) = const (return ())
| Just f <- redirectVerbose cfg = liftIO . mapM_ (appendFile f . (++ "\n"))
| True = liftIO . mapM_ 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 [] = []
mergeSExpr (x:xs)
| d == 0 = x : mergeSExpr xs
| True = let (f, r) = grab d xs in unlines (x:f) : mergeSExpr r
where d = parenDiff x
parenDiff :: String -> Int
parenDiff = go 0
where go i "" = i
go i ('(':cs) = let i'= i+1 in i' `seq` go i' cs
go i (')':cs) = let i'= i-1 in i' `seq` go i' cs
go i ('"':cs) = go i (skipString cs)
go i ('|':cs) = go i (skipBar cs)
go i (_ :cs) = go i cs
grab i ls
| i <= 0 = ([], ls)
grab _ [] = ([], [])
grab i (l:ls) = let (a, b) = grab (i+parenDiff l) ls in (l:a, b)
skipString ('"':'"':cs) = skipString cs
skipString ('"':cs) = cs
skipString (_:cs) = skipString cs
skipString [] = [] -- Oh dear, line finished, but the string didn't. We're in trouble. Ignore!
skipBar ('|':cs) = cs
skipBar (_:cs) = skipBar 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 {
sbvExceptionDescription :: String
, sbvExceptionSent :: Maybe String
, sbvExceptionExpected :: Maybe String
, sbvExceptionReceived :: Maybe String
, sbvExceptionStdOut :: Maybe String
, sbvExceptionStdErr :: Maybe String
, sbvExceptionExitCode :: Maybe ExitCode
, sbvExceptionConfig :: SMTConfig
, sbvExceptionReason :: 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 { sbvExceptionDescription
, sbvExceptionSent
, sbvExceptionExpected
, sbvExceptionReceived
, sbvExceptionStdOut
, sbvExceptionStdErr
, sbvExceptionExitCode
, sbvExceptionConfig
, sbvExceptionReason
, sbvExceptionHint
}
= let grp1 = [ ""
, "*** Data.SBV: " ++ sbvExceptionDescription ++ ":"
]
grp2 = ["*** Sent : " `alignDiagnostic` snt | Just snt <- [sbvExceptionSent], not $ null snt ]
++ ["*** Expected : " `alignDiagnostic` excp | Just excp <- [sbvExceptionExpected], not $ null excp]
++ ["*** Received : " `alignDiagnostic` rcvd | Just rcvd <- [sbvExceptionReceived], not $ null rcvd]
grp3 = ["*** Stdout : " `alignDiagnostic` out | Just out <- [sbvExceptionStdOut], not $ null out ]
++ ["*** Stderr : " `alignDiagnostic` err | Just err <- [sbvExceptionStdErr], not $ null err ]
++ ["*** Exit code : " `alignDiagnostic` show ec | Just ec <- [sbvExceptionExitCode] ]
++ ["*** Executable: " `alignDiagnostic` executable (solver sbvExceptionConfig) ]
++ ["*** Options : " `alignDiagnostic` joinArgs (options (solver sbvExceptionConfig) sbvExceptionConfig) ]
grp4 = ["*** Reason : " `alignDiagnostic` unlines rsn | Just rsn <- [sbvExceptionReason]]
++ ["*** Hint : " `alignDiagnostic` unlines hnt | Just hnt <- [sbvExceptionHint ]]
join [] = []
join [x] = x
join (g:gs) = case join gs of
[] -> g
rest -> g ++ ["***"] ++ rest
in unlines $ join [grp1, grp2, grp3, grp4]