-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.SMT.SMT
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Abstraction of SMT solvers
-----------------------------------------------------------------------------

{-# LANGUAGE DefaultSignatures          #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NamedFieldPuns             #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE Rank2Types                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE ViewPatterns               #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.SMT.SMT (
       -- * Model extraction
         Modelable(..)
       , SatModel(..), genParse
       , extractModels, getModelValues
       , getModelDictionaries, getModelUninterpretedValues
       , displayModels, showModel, shCV, showModelDictionary

       -- * Standard prover engine
       , standardEngine

       -- * Results of various tasks
       , ThmResult(..)
       , SatResult(..)
       , AllSatResult(..)
       , SafeResult(..)
       , OptimizeResult(..)
       )
       where

import qualified Control.Exception as C

import Control.Concurrent (newEmptyMVar, takeMVar, putMVar, forkIO)
import Control.DeepSeq    (NFData(..))
import Control.Monad      (zipWithM)
import Data.Char          (isSpace)
import Data.Maybe         (fromMaybe, isJust)
import Data.Int           (Int8, Int16, Int32, Int64)
import Data.List          (intercalate, isPrefixOf, transpose, isInfixOf)
import Data.Word          (Word8, Word16, Word32, Word64)

import GHC.TypeLits
import Data.Proxy

import Data.IORef (readIORef, writeIORef)

import Data.Time          (getZonedTime, defaultTimeLocale, formatTime, diffUTCTime, getCurrentTime)

import Data.Either(rights)

import System.Directory   (findExecutable)
import System.Environment (getEnv)
import System.Exit        (ExitCode(..))
import System.IO          (hClose, hFlush, hPutStrLn, hGetContents, hGetLine)
import System.Process     (runInteractiveProcess, waitForProcess, terminateProcess)

import qualified Data.Map.Strict as M
import qualified Data.Text       as T

import Data.SBV.Core.AlgReals
import Data.SBV.Core.Data
import Data.SBV.Core.Symbolic (SMTEngine, State(..))
import Data.SBV.Core.Concrete (showCV)
import Data.SBV.Core.Kind     (showBaseKind, intOfProxy)

import Data.SBV.Core.SizedFloats(FloatingPoint(..))

import Data.SBV.SMT.Utils     (showTimeoutValue, alignPlain, debug, mergeSExpr, SBVException(..))

import Data.SBV.Utils.PrettyNum
import Data.SBV.Utils.Lib       (joinArgs, splitArgs)
import Data.SBV.Utils.SExpr     (parenDeficit)
import Data.SBV.Utils.TDiff     (Timing(..), showTDiff)

import qualified System.Timeout as Timeout (timeout)

import Numeric

import qualified Data.SBV.Utils.CrackNum as CN

-- | Extract the final configuration from a result
resultConfig :: SMTResult -> SMTConfig
resultConfig :: SMTResult -> SMTConfig
resultConfig (Unsatisfiable SMTConfig
c Maybe [[Char]]
_  ) = SMTConfig
c
resultConfig (Satisfiable   SMTConfig
c SMTModel
_  ) = SMTConfig
c
resultConfig (DeltaSat      SMTConfig
c Maybe [Char]
_ SMTModel
_) = SMTConfig
c
resultConfig (SatExtField   SMTConfig
c SMTModel
_  ) = SMTConfig
c
resultConfig (Unknown       SMTConfig
c SMTReasonUnknown
_  ) = SMTConfig
c
resultConfig (ProofError    SMTConfig
c [[Char]]
_ Maybe SMTResult
_) = SMTConfig
c

-- | A 'Data.SBV.prove' call results in a 'ThmResult'
newtype ThmResult = ThmResult SMTResult
                  deriving ThmResult -> ()
forall a. (a -> ()) -> NFData a
rnf :: ThmResult -> ()
$crnf :: ThmResult -> ()
NFData

-- | A 'Data.SBV.sat' call results in a 'SatResult'
-- The reason for having a separate 'SatResult' is to have a more meaningful 'Show' instance.
newtype SatResult = SatResult SMTResult
                  deriving SatResult -> ()
forall a. (a -> ()) -> NFData a
rnf :: SatResult -> ()
$crnf :: SatResult -> ()
NFData

-- | An 'Data.SBV.allSat' call results in a 'AllSatResult'
data AllSatResult = AllSatResult { AllSatResult -> Bool
allSatMaxModelCountReached  :: Bool          -- ^ Did we reach the user given model count limit?
                                 , AllSatResult -> Bool
allSatHasPrefixExistentials :: Bool          -- ^ Were there quantifiers in the problem (unique upto prefix existentials)
                                 , AllSatResult -> Bool
allSatSolverReturnedUnknown :: Bool          -- ^ Did the solver report unknown at the end?
                                 , AllSatResult -> Bool
allSatSolverReturnedDSat    :: Bool          -- ^ Did the solver report delta-satisfiable at the end?
                                 , AllSatResult -> [SMTResult]
allSatResults               :: [SMTResult]   -- ^ All satisfying models
                                 }

-- | A 'Data.SBV.safe' call results in a 'SafeResult'
newtype SafeResult   = SafeResult   (Maybe String, String, SMTResult)

-- | An 'Data.SBV.optimize' call results in a 'OptimizeResult'. In the 'ParetoResult' case, the boolean is 'True'
-- if we reached pareto-query limit and so there might be more unqueried results remaining. If 'False',
-- it means that we have all the pareto fronts returned. See the 'Pareto' 'OptimizeStyle' for details.
data OptimizeResult = LexicographicResult SMTResult
                    | ParetoResult        (Bool, [SMTResult])
                    | IndependentResult   [(String, SMTResult)]

-- | What's the precision of a delta-sat query?
getPrecision :: SMTResult -> Maybe String -> String
getPrecision :: SMTResult -> Maybe [Char] -> [Char]
getPrecision SMTResult
r Maybe [Char]
queriedPrecision = case (Maybe [Char]
queriedPrecision, SMTConfig -> Maybe Double
dsatPrecision (SMTResult -> SMTConfig
resultConfig SMTResult
r)) of
                                   (Just [Char]
s, Maybe Double
_     ) -> [Char]
s
                                   (Maybe [Char]
_,      Just Double
d) -> forall a. RealFloat a => Maybe Int -> a -> ShowS
showFFloat forall a. Maybe a
Nothing Double
d [Char]
""
                                   (Maybe [Char], Maybe Double)
_                -> [Char]
"tool default"

-- User friendly way of printing theorem results
instance Show ThmResult where
  show :: ThmResult -> [Char]
show (ThmResult SMTResult
r) = [Char]
-> [Char]
-> [Char]
-> [Char]
-> (Maybe [Char] -> [Char])
-> [Char]
-> SMTResult
-> [Char]
showSMTResult [Char]
"Q.E.D."
                                     [Char]
"Unknown"
                                     [Char]
"Falsifiable"
                                     [Char]
"Falsifiable. Counter-example:\n"
                                     (\Maybe [Char]
mbP -> [Char]
"Delta falsifiable, precision: " forall a. [a] -> [a] -> [a]
++ SMTResult -> Maybe [Char] -> [Char]
getPrecision SMTResult
r Maybe [Char]
mbP forall a. [a] -> [a] -> [a]
++ [Char]
". Counter-example:\n")
                                     [Char]
"Falsifiable in an extension field:\n"
                                     SMTResult
r

-- User friendly way of printing satisfiablity results
instance Show SatResult where
  show :: SatResult -> [Char]
show (SatResult SMTResult
r) = [Char]
-> [Char]
-> [Char]
-> [Char]
-> (Maybe [Char] -> [Char])
-> [Char]
-> SMTResult
-> [Char]
showSMTResult [Char]
"Unsatisfiable"
                                     [Char]
"Unknown"
                                     [Char]
"Satisfiable"
                                     [Char]
"Satisfiable. Model:\n"
                                     (\Maybe [Char]
mbP -> [Char]
"Delta satisfiable, precision: " forall a. [a] -> [a] -> [a]
++ SMTResult -> Maybe [Char] -> [Char]
getPrecision SMTResult
r Maybe [Char]
mbP forall a. [a] -> [a] -> [a]
++ [Char]
". Model:\n")
                                     [Char]
"Satisfiable in an extension field. Model:\n"
                                     SMTResult
r

-- User friendly way of printing safety results
instance Show SafeResult where
   show :: SafeResult -> [Char]
show (SafeResult (Maybe [Char]
mbLoc, [Char]
msg, SMTResult
r)) = [Char]
-> [Char]
-> [Char]
-> [Char]
-> (Maybe [Char] -> [Char])
-> [Char]
-> SMTResult
-> [Char]
showSMTResult (ShowS
tag [Char]
"No violations detected")
                                                     (ShowS
tag [Char]
"Unknown")
                                                     (ShowS
tag [Char]
"Violated")
                                                     (ShowS
tag [Char]
"Violated. Model:\n")
                                                     (\Maybe [Char]
mbP -> ShowS
tag [Char]
"Violated in a delta-satisfiable context, precision: " forall a. [a] -> [a] -> [a]
++ SMTResult -> Maybe [Char] -> [Char]
getPrecision SMTResult
r Maybe [Char]
mbP forall a. [a] -> [a] -> [a]
++ [Char]
". Model:\n")
                                                     (ShowS
tag [Char]
"Violated in an extension field:\n")
                                                     SMTResult
r
        where loc :: [Char]
loc   = forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Char]
"" (forall a. [a] -> [a] -> [a]
++ [Char]
": ") Maybe [Char]
mbLoc
              tag :: ShowS
tag [Char]
s = [Char]
loc forall a. [a] -> [a] -> [a]
++ [Char]
msg forall a. [a] -> [a] -> [a]
++ [Char]
": " forall a. [a] -> [a] -> [a]
++ [Char]
s

-- The Show instance of AllSatResults.
instance Show AllSatResult where
  show :: AllSatResult -> [Char]
show AllSatResult { allSatMaxModelCountReached :: AllSatResult -> Bool
allSatMaxModelCountReached  = Bool
l
                    , allSatHasPrefixExistentials :: AllSatResult -> Bool
allSatHasPrefixExistentials = Bool
e
                    , allSatSolverReturnedUnknown :: AllSatResult -> Bool
allSatSolverReturnedUnknown = Bool
u
                    , allSatSolverReturnedDSat :: AllSatResult -> Bool
allSatSolverReturnedDSat    = Bool
d
                    , allSatResults :: AllSatResult -> [SMTResult]
allSatResults               = [SMTResult]
xs
                    } = forall {a}. (Eq a, Num a, Show a) => a -> [SMTResult] -> [Char]
go (Int
0::Int) [SMTResult]
xs
    where warnings :: [Char]
warnings = case (Bool
e, Bool
u) of
                       (Bool
False, Bool
False) -> [Char]
""
                       (Bool
False, Bool
True)  -> [Char]
" (Search stopped since solver has returned unknown.)"
                       (Bool
True,  Bool
False) -> [Char]
" (Unique up to prefix existentials.)"
                       (Bool
True,  Bool
True)  -> [Char]
" (Search stopped because solver has returned unknown, only prefix existentials were considered.)"

          go :: a -> [SMTResult] -> [Char]
go a
c (SMTResult
s:[SMTResult]
ss) = let c' :: a
c'      = a
cforall a. Num a => a -> a -> a
+a
1
                            (Bool
ok, [Char]
o) = forall {a}. Show a => a -> SMTResult -> (Bool, [Char])
sh a
c' SMTResult
s
                        in a
c' seq :: forall a b. a -> b -> b
`seq` if Bool
ok then [Char]
o forall a. [a] -> [a] -> [a]
++ [Char]
"\n" forall a. [a] -> [a] -> [a]
++ a -> [SMTResult] -> [Char]
go a
c' [SMTResult]
ss else [Char]
o
          go a
c []     = case (Bool
l, Bool
d, a
c) of
                          (Bool
True,  Bool
_   , a
_) -> [Char]
"Search stopped since model count request was reached."  forall a. [a] -> [a] -> [a]
++ [Char]
warnings
                          (Bool
_   ,  Bool
True, a
_) -> [Char]
"Search stopped since the result was delta-satisfiable." forall a. [a] -> [a] -> [a]
++ [Char]
warnings
                          (Bool
False, Bool
_   , a
0) -> [Char]
"No solutions found."
                          (Bool
False, Bool
_   , a
1) -> [Char]
"This is the only solution." forall a. [a] -> [a] -> [a]
++ [Char]
warnings
                          (Bool
False, Bool
_   , a
_) -> [Char]
"Found " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
c forall a. [a] -> [a] -> [a]
++ [Char]
" different solutions." forall a. [a] -> [a] -> [a]
++ [Char]
warnings

          sh :: a -> SMTResult -> (Bool, [Char])
sh a
i SMTResult
c = (Bool
ok, [Char]
-> [Char]
-> [Char]
-> [Char]
-> (Maybe [Char] -> [Char])
-> [Char]
-> SMTResult
-> [Char]
showSMTResult [Char]
"Unsatisfiable"
                                      [Char]
"Unknown"
                                      ([Char]
"Solution #" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
i forall a. [a] -> [a] -> [a]
++ [Char]
":\nSatisfiable") ([Char]
"Solution #" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
i forall a. [a] -> [a] -> [a]
++ [Char]
":\n")
                                      (\Maybe [Char]
mbP -> [Char]
"Solution $" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
i forall a. [a] -> [a] -> [a]
++ [Char]
" with delta-satisfiability, precision: " forall a. [a] -> [a] -> [a]
++ SMTResult -> Maybe [Char] -> [Char]
getPrecision SMTResult
c Maybe [Char]
mbP forall a. [a] -> [a] -> [a]
++ [Char]
":\n")
                                      ([Char]
"Solution $" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
i forall a. [a] -> [a] -> [a]
++ [Char]
" in an extension field:\n")
                                      SMTResult
c)
              where ok :: Bool
ok = case SMTResult
c of
                           Satisfiable{} -> Bool
True
                           SMTResult
_             -> Bool
False

-- Show instance for optimization results
instance Show OptimizeResult where
  show :: OptimizeResult -> [Char]
show OptimizeResult
res = case OptimizeResult
res of
               LexicographicResult SMTResult
r   -> forall {t}. IsString t => (t -> [Char]) -> SMTResult -> [Char]
sh forall a. a -> a
id SMTResult
r

               IndependentResult   [([Char], SMTResult)]
rs  -> [Char] -> [[Char]] -> [Char]
multi [Char]
"objectives" (forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall {a}. Show a => a -> SMTResult -> [Char]
shI) [([Char], SMTResult)]
rs)

               ParetoResult (Bool
False, [SMTResult
r]) -> forall {t}. IsString t => (t -> [Char]) -> SMTResult -> [Char]
sh ([Char]
"Unique pareto front: " forall a. [a] -> [a] -> [a]
++) SMTResult
r
               ParetoResult (Bool
False, [SMTResult]
rs)  -> [Char] -> [[Char]] -> [Char]
multi [Char]
"pareto optimal values" (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {a}. Show a => a -> SMTResult -> [Char]
shP [(Int
1::Int)..] [SMTResult]
rs)
               ParetoResult (Bool
True,  [SMTResult]
rs)  ->    [Char] -> [[Char]] -> [Char]
multi [Char]
"pareto optimal values" (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {a}. Show a => a -> SMTResult -> [Char]
shP [(Int
1::Int)..] [SMTResult]
rs)
                                           forall a. [a] -> [a] -> [a]
++ [Char]
"\n*** Note: Pareto-front extraction was terminated as requested by the user."
                                           forall a. [a] -> [a] -> [a]
++ [Char]
"\n***       There might be many other results!"

       where multi :: [Char] -> [[Char]] -> [Char]
multi [Char]
w [] = [Char]
"There are no " forall a. [a] -> [a] -> [a]
++ [Char]
w forall a. [a] -> [a] -> [a]
++ [Char]
" to display models for."
             multi [Char]
_ [[Char]]
xs = forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" [[Char]]
xs

             shI :: a -> SMTResult -> [Char]
shI a
n = forall {t}. IsString t => (t -> [Char]) -> SMTResult -> [Char]
sh (\[Char]
s -> [Char]
"Objective "     forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
n forall a. [a] -> [a] -> [a]
++ [Char]
": " forall a. [a] -> [a] -> [a]
++ [Char]
s)
             shP :: a -> SMTResult -> [Char]
shP a
i = forall {t}. IsString t => (t -> [Char]) -> SMTResult -> [Char]
sh (\[Char]
s -> [Char]
"Pareto front #" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
i forall a. [a] -> [a] -> [a]
++ [Char]
": " forall a. [a] -> [a] -> [a]
++ [Char]
s)

             sh :: (t -> [Char]) -> SMTResult -> [Char]
sh t -> [Char]
tag SMTResult
r = [Char]
-> [Char]
-> [Char]
-> [Char]
-> (Maybe [Char] -> [Char])
-> [Char]
-> SMTResult
-> [Char]
showSMTResult (t -> [Char]
tag t
"Unsatisfiable.")
                                      (t -> [Char]
tag t
"Unknown.")
                                      (t -> [Char]
tag t
"Optimal with no assignments.")
                                      (t -> [Char]
tag t
"Optimal model:" forall a. [a] -> [a] -> [a]
++ [Char]
"\n")
                                      (\Maybe [Char]
mbP -> t -> [Char]
tag t
"Optimal model with delta-satisfiability, precision: " forall a. [a] -> [a] -> [a]
++ SMTResult -> Maybe [Char] -> [Char]
getPrecision SMTResult
r Maybe [Char]
mbP forall a. [a] -> [a] -> [a]
++ [Char]
":" forall a. [a] -> [a] -> [a]
++ [Char]
"\n")
                                      (t -> [Char]
tag t
"Optimal in an extension field:" forall a. [a] -> [a] -> [a]
++ [Char]
"\n")
                                      SMTResult
r

-- | Instances of 'SatModel' can be automatically extracted from models returned by the
-- solvers. The idea is that the sbv infrastructure provides a stream of CV's (constant values)
-- coming from the solver, and the type @a@ is interpreted based on these constants. Many typical
-- instances are already provided, so new instances can be declared with relative ease.
--
-- Minimum complete definition: 'parseCVs'
class SatModel a where
  -- | Given a sequence of constant-words, extract one instance of the type @a@, returning
  -- the remaining elements untouched. If the next element is not what's expected for this
  -- type you should return 'Nothing'
  parseCVs  :: [CV] -> Maybe (a, [CV])
  -- | Given a parsed model instance, transform it using @f@, and return the result.
  -- The default definition for this method should be sufficient in most use cases.
  cvtModel  :: (a -> Maybe b) -> Maybe (a, [CV]) -> Maybe (b, [CV])
  cvtModel a -> Maybe b
f Maybe (a, [CV])
x = Maybe (a, [CV])
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(a
a, [CV]
r) -> a -> Maybe b
f a
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \b
b -> forall (m :: * -> *) a. Monad m => a -> m a
return (b
b, [CV]
r)

  default parseCVs :: Read a => [CV] -> Maybe (a, [CV])
  parseCVs (CV Kind
_ (CUserSort (Maybe Int
_, [Char]
s)) : [CV]
r) = forall a. a -> Maybe a
Just (forall a. Read a => [Char] -> a
read [Char]
s, [CV]
r)
  parseCVs [CV]
_                             = forall a. Maybe a
Nothing

-- | Parse a signed/sized value from a sequence of CVs
genParse :: Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse :: forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse Kind
k (x :: CV
x@(CV Kind
_ (CInteger Integer
i)):[CV]
r) | forall a. HasKind a => a -> Kind
kindOf CV
x forall a. Eq a => a -> a -> Bool
== Kind
k = forall a. a -> Maybe a
Just (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i, [CV]
r)
genParse Kind
_ [CV]
_                                         = forall a. Maybe a
Nothing

-- | Base case for 'SatModel' at unit type. Comes in handy if there are no real variables.
instance SatModel () where
  parseCVs :: [CV] -> Maybe ((), [CV])
parseCVs [CV]
xs = forall (m :: * -> *) a. Monad m => a -> m a
return ((), [CV]
xs)

-- | 'Bool' as extracted from a model
instance SatModel Bool where
  parseCVs :: [CV] -> Maybe (Bool, [CV])
parseCVs [CV]
xs = do (Integer
x, [CV]
r) <- forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse Kind
KBool [CV]
xs
                   forall (m :: * -> *) a. Monad m => a -> m a
return ((Integer
x :: Integer) forall a. Eq a => a -> a -> Bool
/= Integer
0, [CV]
r)

-- | 'Word8' as extracted from a model
instance SatModel Word8 where
  parseCVs :: [CV] -> Maybe (Word8, [CV])
parseCVs = forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (Bool -> Int -> Kind
KBounded Bool
False Int
8)

-- | 'Int8' as extracted from a model
instance SatModel Int8 where
  parseCVs :: [CV] -> Maybe (Int8, [CV])
parseCVs = forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (Bool -> Int -> Kind
KBounded Bool
True Int
8)

-- | 'Word16' as extracted from a model
instance SatModel Word16 where
  parseCVs :: [CV] -> Maybe (Word16, [CV])
parseCVs = forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (Bool -> Int -> Kind
KBounded Bool
False Int
16)

-- | 'Int16' as extracted from a model
instance SatModel Int16 where
  parseCVs :: [CV] -> Maybe (Int16, [CV])
parseCVs = forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (Bool -> Int -> Kind
KBounded Bool
True Int
16)

-- | 'Word32' as extracted from a model
instance SatModel Word32 where
  parseCVs :: [CV] -> Maybe (Word32, [CV])
parseCVs = forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (Bool -> Int -> Kind
KBounded Bool
False Int
32)

-- | 'Int32' as extracted from a model
instance SatModel Int32 where
  parseCVs :: [CV] -> Maybe (Int32, [CV])
parseCVs = forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (Bool -> Int -> Kind
KBounded Bool
True Int
32)

-- | 'Word64' as extracted from a model
instance SatModel Word64 where
  parseCVs :: [CV] -> Maybe (Word64, [CV])
parseCVs = forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (Bool -> Int -> Kind
KBounded Bool
False Int
64)

-- | 'Int64' as extracted from a model
instance SatModel Int64 where
  parseCVs :: [CV] -> Maybe (Int64, [CV])
parseCVs = forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (Bool -> Int -> Kind
KBounded Bool
True Int
64)

-- | 'Integer' as extracted from a model
instance SatModel Integer where
  parseCVs :: [CV] -> Maybe (Integer, [CV])
parseCVs = forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse Kind
KUnbounded

-- | 'AlgReal' as extracted from a model
instance SatModel AlgReal where
  parseCVs :: [CV] -> Maybe (AlgReal, [CV])
parseCVs (CV Kind
KReal (CAlgReal AlgReal
i) : [CV]
r) = forall a. a -> Maybe a
Just (AlgReal
i, [CV]
r)
  parseCVs [CV]
_                           = forall a. Maybe a
Nothing

-- | 'Float' as extracted from a model
instance SatModel Float where
  parseCVs :: [CV] -> Maybe (Float, [CV])
parseCVs (CV Kind
KFloat (CFloat Float
i) : [CV]
r) = forall a. a -> Maybe a
Just (Float
i, [CV]
r)
  parseCVs [CV]
_                          = forall a. Maybe a
Nothing

-- | 'Double' as extracted from a model
instance SatModel Double where
  parseCVs :: [CV] -> Maybe (Double, [CV])
parseCVs (CV Kind
KDouble (CDouble Double
i) : [CV]
r) = forall a. a -> Maybe a
Just (Double
i, [CV]
r)
  parseCVs [CV]
_                            = forall a. Maybe a
Nothing

-- | A general floating-point extracted from a model
instance (KnownNat eb, KnownNat sb) => SatModel (FloatingPoint eb sb) where
  parseCVs :: [CV] -> Maybe (FloatingPoint eb sb, [CV])
parseCVs (CV (KFP Int
ei Int
si) (CFP FP
fp) : [CV]
r)
    | forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @eb) forall a. Eq a => a -> a -> Bool
== Int
ei , forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @sb) forall a. Eq a => a -> a -> Bool
== Int
si = forall a. a -> Maybe a
Just (forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint FP
fp, [CV]
r)
  parseCVs [CV]
_                                                      = forall a. Maybe a
Nothing

-- | @CV@ as extracted from a model; trivial definition
instance SatModel CV where
  parseCVs :: [CV] -> Maybe (CV, [CV])
parseCVs (CV
cv : [CV]
r) = forall a. a -> Maybe a
Just (CV
cv, [CV]
r)
  parseCVs []       = forall a. Maybe a
Nothing

-- | A rounding mode, extracted from a model. (Default definition suffices)
instance SatModel RoundingMode

-- | 'String' as extracted from a model
instance {-# OVERLAPS #-} SatModel [Char] where
  parseCVs :: [CV] -> Maybe ([Char], [CV])
parseCVs (CV Kind
_ (CString [Char]
c):[CV]
r) = forall a. a -> Maybe a
Just ([Char]
c, [CV]
r)
  parseCVs [CV]
_                    = forall a. Maybe a
Nothing

-- | 'Char' as extracted from a model
instance SatModel Char where
  parseCVs :: [CV] -> Maybe (Char, [CV])
parseCVs (CV Kind
_ (CChar Char
c):[CV]
r) = forall a. a -> Maybe a
Just (Char
c, [CV]
r)
  parseCVs [CV]
_                  = forall a. Maybe a
Nothing

-- | A list of values as extracted from a model. When reading a list, we
-- go as long as we can (maximal-munch). Note that this never fails, as
-- we can always return the empty list!
instance {-# OVERLAPPABLE #-} SatModel a => SatModel [a] where
  parseCVs :: [CV] -> Maybe ([a], [CV])
parseCVs [] = forall a. a -> Maybe a
Just ([], [])
  parseCVs [CV]
xs = case forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
xs of
                  Just (a
a, [CV]
ys) -> case forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
ys of
                                    Just ([a]
as, [CV]
zs) -> forall a. a -> Maybe a
Just (a
aforall a. a -> [a] -> [a]
:[a]
as, [CV]
zs)
                                    Maybe ([a], [CV])
Nothing       -> forall a. a -> Maybe a
Just ([], [CV]
ys)
                  Maybe (a, [CV])
Nothing     -> forall a. a -> Maybe a
Just ([], [CV]
xs)

-- | Tuples extracted from a model
instance (SatModel a, SatModel b) => SatModel (a, b) where
  parseCVs :: [CV] -> Maybe ((a, b), [CV])
parseCVs [CV]
as = do (a
a, [CV]
bs) <- forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
as
                   (b
b, [CV]
cs) <- forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
bs
                   forall (m :: * -> *) a. Monad m => a -> m a
return ((a
a, b
b), [CV]
cs)

-- | 3-Tuples extracted from a model
instance (SatModel a, SatModel b, SatModel c) => SatModel (a, b, c) where
  parseCVs :: [CV] -> Maybe ((a, b, c), [CV])
parseCVs [CV]
as = do (a
a,      [CV]
bs) <- forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
as
                   ((b
b, c
c), [CV]
ds) <- forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
bs
                   forall (m :: * -> *) a. Monad m => a -> m a
return ((a
a, b
b, c
c), [CV]
ds)

-- | 4-Tuples extracted from a model
instance (SatModel a, SatModel b, SatModel c, SatModel d) => SatModel (a, b, c, d) where
  parseCVs :: [CV] -> Maybe ((a, b, c, d), [CV])
parseCVs [CV]
as = do (a
a,         [CV]
bs) <- forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
as
                   ((b
b, c
c, d
d), [CV]
es) <- forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
bs
                   forall (m :: * -> *) a. Monad m => a -> m a
return ((a
a, b
b, c
c, d
d), [CV]
es)

-- | 5-Tuples extracted from a model
instance (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e) => SatModel (a, b, c, d, e) where
  parseCVs :: [CV] -> Maybe ((a, b, c, d, e), [CV])
parseCVs [CV]
as = do (a
a, [CV]
bs)            <- forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
as
                   ((b
b, c
c, d
d, e
e), [CV]
fs) <- forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
bs
                   forall (m :: * -> *) a. Monad m => a -> m a
return ((a
a, b
b, c
c, d
d, e
e), [CV]
fs)

-- | 6-Tuples extracted from a model
instance (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f) => SatModel (a, b, c, d, e, f) where
  parseCVs :: [CV] -> Maybe ((a, b, c, d, e, f), [CV])
parseCVs [CV]
as = do (a
a, [CV]
bs)               <- forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
as
                   ((b
b, c
c, d
d, e
e, f
f), [CV]
gs) <- forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
bs
                   forall (m :: * -> *) a. Monad m => a -> m a
return ((a
a, b
b, c
c, d
d, e
e, f
f), [CV]
gs)

-- | 7-Tuples extracted from a model
instance (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f, SatModel g) => SatModel (a, b, c, d, e, f, g) where
  parseCVs :: [CV] -> Maybe ((a, b, c, d, e, f, g), [CV])
parseCVs [CV]
as = do (a
a, [CV]
bs)                  <- forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
as
                   ((b
b, c
c, d
d, e
e, f
f, g
g), [CV]
hs) <- forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
bs
                   forall (m :: * -> *) a. Monad m => a -> m a
return ((a
a, b
b, c
c, d
d, e
e, f
f, g
g), [CV]
hs)

-- | Various SMT results that we can extract models out of.
class Modelable a where
  -- | Is there a model?
  modelExists :: a -> Bool

  -- | Extract assignments of a model, the result is a tuple where the first argument (if True)
  -- indicates whether the model was "probable". (i.e., if the solver returned unknown.)
  getModelAssignment :: SatModel b => a -> Either String (Bool, b)

  -- | Extract a model dictionary. Extract a dictionary mapping the variables to
  -- their respective values as returned by the SMT solver. Also see `getModelDictionaries`.
  getModelDictionary :: a -> M.Map String CV

  -- | Extract a model value for a given element. Also see `getModelValues`.
  getModelValue :: SymVal b => String -> a -> Maybe b
  getModelValue [Char]
v a
r = forall a. SymVal a => CV -> a
fromCV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` ([Char]
v forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` forall a. Modelable a => a -> Map [Char] CV
getModelDictionary a
r)

  -- | Extract a representative name for the model value of an uninterpreted kind.
  -- This is supposed to correspond to the value as computed internally by the
  -- SMT solver; and is unportable from solver to solver. Also see `getModelUninterpretedValues`.
  getModelUninterpretedValue :: String -> a -> Maybe String
  getModelUninterpretedValue [Char]
v a
r = case [Char]
v forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` forall a. Modelable a => a -> Map [Char] CV
getModelDictionary a
r of
                                     Just (CV Kind
_ (CUserSort (Maybe Int
_, [Char]
s))) -> forall a. a -> Maybe a
Just [Char]
s
                                     Maybe CV
_                              -> forall a. Maybe a
Nothing

  -- | A simpler variant of 'getModelAssignment' to get a model out without the fuss.
  extractModel :: SatModel b => a -> Maybe b
  extractModel a
a = case forall a b.
(Modelable a, SatModel b) =>
a -> Either [Char] (Bool, b)
getModelAssignment a
a of
                     Right (Bool
_, b
b) -> forall a. a -> Maybe a
Just b
b
                     Either [Char] (Bool, b)
_            -> forall a. Maybe a
Nothing

  -- | Extract model objective values, for all optimization goals.
  getModelObjectives :: a -> M.Map String GeneralizedCV

  -- | Extract the value of an objective
  getModelObjectiveValue :: String -> a -> Maybe GeneralizedCV
  getModelObjectiveValue [Char]
v a
r = [Char]
v forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` forall a. Modelable a => a -> Map [Char] GeneralizedCV
getModelObjectives a
r

  -- | Extract model uninterpreted-functions
  getModelUIFuns :: a -> M.Map String (SBVType, ([([CV], CV)], CV))

  -- | Extract the value of an uninterpreted-function as an association list
  getModelUIFunValue :: String -> a -> Maybe (SBVType, ([([CV], CV)], CV))
  getModelUIFunValue [Char]
v a
r = [Char]
v forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` forall a.
Modelable a =>
a -> Map [Char] (SBVType, ([([CV], CV)], CV))
getModelUIFuns a
r

-- | Return all the models from an 'Data.SBV.allSat' call, similar to 'extractModel' but
-- is suitable for the case of multiple results.
extractModels :: SatModel a => AllSatResult -> [a]
extractModels :: forall a. SatModel a => AllSatResult -> [a]
extractModels AllSatResult{allSatResults :: AllSatResult -> [SMTResult]
allSatResults = [SMTResult]
xs} = [a
ms | Right (Bool
_, a
ms) <- forall a b. (a -> b) -> [a] -> [b]
map forall a b.
(Modelable a, SatModel b) =>
a -> Either [Char] (Bool, b)
getModelAssignment [SMTResult]
xs]

-- | Get dictionaries from an all-sat call. Similar to `getModelDictionary`.
getModelDictionaries :: AllSatResult -> [M.Map String CV]
getModelDictionaries :: AllSatResult -> [Map [Char] CV]
getModelDictionaries AllSatResult{allSatResults :: AllSatResult -> [SMTResult]
allSatResults = [SMTResult]
xs} = forall a b. (a -> b) -> [a] -> [b]
map forall a. Modelable a => a -> Map [Char] CV
getModelDictionary [SMTResult]
xs

-- | Extract value of a variable from an all-sat call. Similar to `getModelValue`.
getModelValues :: SymVal b => String -> AllSatResult -> [Maybe b]
getModelValues :: forall b. SymVal b => [Char] -> AllSatResult -> [Maybe b]
getModelValues [Char]
s AllSatResult{allSatResults :: AllSatResult -> [SMTResult]
allSatResults = [SMTResult]
xs} =  forall a b. (a -> b) -> [a] -> [b]
map ([Char]
s forall a b. (Modelable a, SymVal b) => [Char] -> a -> Maybe b
`getModelValue`) [SMTResult]
xs

-- | Extract value of an uninterpreted variable from an all-sat call. Similar to `getModelUninterpretedValue`.
getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String]
getModelUninterpretedValues :: [Char] -> AllSatResult -> [Maybe [Char]]
getModelUninterpretedValues [Char]
s AllSatResult{allSatResults :: AllSatResult -> [SMTResult]
allSatResults = [SMTResult]
xs} =  forall a b. (a -> b) -> [a] -> [b]
map ([Char]
s forall a. Modelable a => [Char] -> a -> Maybe [Char]
`getModelUninterpretedValue`) [SMTResult]
xs

-- | 'ThmResult' as a generic model provider
instance Modelable ThmResult where
  getModelAssignment :: forall b. SatModel b => ThmResult -> Either [Char] (Bool, b)
getModelAssignment (ThmResult SMTResult
r) = forall a b.
(Modelable a, SatModel b) =>
a -> Either [Char] (Bool, b)
getModelAssignment SMTResult
r
  modelExists :: ThmResult -> Bool
modelExists        (ThmResult SMTResult
r) = forall a. Modelable a => a -> Bool
modelExists        SMTResult
r
  getModelDictionary :: ThmResult -> Map [Char] CV
getModelDictionary (ThmResult SMTResult
r) = forall a. Modelable a => a -> Map [Char] CV
getModelDictionary SMTResult
r
  getModelObjectives :: ThmResult -> Map [Char] GeneralizedCV
getModelObjectives (ThmResult SMTResult
r) = forall a. Modelable a => a -> Map [Char] GeneralizedCV
getModelObjectives SMTResult
r
  getModelUIFuns :: ThmResult -> Map [Char] (SBVType, ([([CV], CV)], CV))
getModelUIFuns     (ThmResult SMTResult
r) = forall a.
Modelable a =>
a -> Map [Char] (SBVType, ([([CV], CV)], CV))
getModelUIFuns     SMTResult
r

-- | 'SatResult' as a generic model provider
instance Modelable SatResult where
  getModelAssignment :: forall b. SatModel b => SatResult -> Either [Char] (Bool, b)
getModelAssignment (SatResult SMTResult
r) = forall a b.
(Modelable a, SatModel b) =>
a -> Either [Char] (Bool, b)
getModelAssignment SMTResult
r
  modelExists :: SatResult -> Bool
modelExists        (SatResult SMTResult
r) = forall a. Modelable a => a -> Bool
modelExists        SMTResult
r
  getModelDictionary :: SatResult -> Map [Char] CV
getModelDictionary (SatResult SMTResult
r) = forall a. Modelable a => a -> Map [Char] CV
getModelDictionary SMTResult
r
  getModelObjectives :: SatResult -> Map [Char] GeneralizedCV
getModelObjectives (SatResult SMTResult
r) = forall a. Modelable a => a -> Map [Char] GeneralizedCV
getModelObjectives SMTResult
r
  getModelUIFuns :: SatResult -> Map [Char] (SBVType, ([([CV], CV)], CV))
getModelUIFuns     (SatResult SMTResult
r) = forall a.
Modelable a =>
a -> Map [Char] (SBVType, ([([CV], CV)], CV))
getModelUIFuns     SMTResult
r

-- | 'SMTResult' as a generic model provider
instance Modelable SMTResult where
  getModelAssignment :: forall b. SatModel b => SMTResult -> Either [Char] (Bool, b)
getModelAssignment (Unsatisfiable SMTConfig
_ Maybe [[Char]]
_  ) = forall a b. a -> Either a b
Left [Char]
"SBV.getModelAssignment: Unsatisfiable result"
  getModelAssignment (Satisfiable   SMTConfig
_   SMTModel
m) = forall a b. b -> Either a b
Right (Bool
False, forall a. SatModel a => SMTModel -> a
parseModelOut SMTModel
m)
  getModelAssignment (DeltaSat      SMTConfig
_ Maybe [Char]
_ SMTModel
m) = forall a b. b -> Either a b
Right (Bool
False, forall a. SatModel a => SMTModel -> a
parseModelOut SMTModel
m)
  getModelAssignment (SatExtField   SMTConfig
_ SMTModel
_  ) = forall a b. a -> Either a b
Left [Char]
"SBV.getModelAssignment: The model is in an extension field"
  getModelAssignment (Unknown       SMTConfig
_ SMTReasonUnknown
m  ) = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ [Char]
"SBV.getModelAssignment: Solver state is unknown: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show SMTReasonUnknown
m
  getModelAssignment (ProofError    SMTConfig
_ [[Char]]
s Maybe SMTResult
_) = forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines forall a b. (a -> b) -> a -> b
$ [Char]
"SBV.getModelAssignment: Failed to produce a model: " forall a. a -> [a] -> [a]
: [[Char]]
s

  modelExists :: SMTResult -> Bool
modelExists Satisfiable{}   = Bool
True
  modelExists Unknown{}       = Bool
False -- don't risk it
  modelExists SMTResult
_               = Bool
False

  getModelDictionary :: SMTResult -> Map [Char] CV
getModelDictionary Unsatisfiable{}     = forall k a. Map k a
M.empty
  getModelDictionary (Satisfiable SMTConfig
_   SMTModel
m) = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (SMTModel -> [([Char], CV)]
modelAssocs SMTModel
m)
  getModelDictionary (DeltaSat    SMTConfig
_ Maybe [Char]
_ SMTModel
m) = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (SMTModel -> [([Char], CV)]
modelAssocs SMTModel
m)
  getModelDictionary SatExtField{}       = forall k a. Map k a
M.empty
  getModelDictionary Unknown{}           = forall k a. Map k a
M.empty
  getModelDictionary ProofError{}        = forall k a. Map k a
M.empty

  getModelObjectives :: SMTResult -> Map [Char] GeneralizedCV
getModelObjectives Unsatisfiable{}     = forall k a. Map k a
M.empty
  getModelObjectives (Satisfiable SMTConfig
_ SMTModel
m  ) = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (SMTModel -> [([Char], GeneralizedCV)]
modelObjectives SMTModel
m)
  getModelObjectives (DeltaSat    SMTConfig
_ Maybe [Char]
_ SMTModel
m) = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (SMTModel -> [([Char], GeneralizedCV)]
modelObjectives SMTModel
m)
  getModelObjectives (SatExtField SMTConfig
_ SMTModel
m  ) = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (SMTModel -> [([Char], GeneralizedCV)]
modelObjectives SMTModel
m)
  getModelObjectives Unknown{}           = forall k a. Map k a
M.empty
  getModelObjectives ProofError{}        = forall k a. Map k a
M.empty

  getModelUIFuns :: SMTResult -> Map [Char] (SBVType, ([([CV], CV)], CV))
getModelUIFuns Unsatisfiable{}     = forall k a. Map k a
M.empty
  getModelUIFuns (Satisfiable SMTConfig
_ SMTModel
m  ) = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (SMTModel -> [([Char], (SBVType, ([([CV], CV)], CV)))]
modelUIFuns SMTModel
m)
  getModelUIFuns (DeltaSat    SMTConfig
_ Maybe [Char]
_ SMTModel
m) = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (SMTModel -> [([Char], (SBVType, ([([CV], CV)], CV)))]
modelUIFuns SMTModel
m)
  getModelUIFuns (SatExtField SMTConfig
_ SMTModel
m  ) = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (SMTModel -> [([Char], (SBVType, ([([CV], CV)], CV)))]
modelUIFuns SMTModel
m)
  getModelUIFuns Unknown{}           = forall k a. Map k a
M.empty
  getModelUIFuns ProofError{}        = forall k a. Map k a
M.empty

-- | Extract a model out, will throw error if parsing is unsuccessful
parseModelOut :: SatModel a => SMTModel -> a
parseModelOut :: forall a. SatModel a => SMTModel -> a
parseModelOut SMTModel
m = case forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV
c | ([Char]
_, CV
c) <- SMTModel -> [([Char], CV)]
modelAssocs SMTModel
m] of
                   Just (a
x, []) -> a
x
                   Just (a
_, [CV]
ys) -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"SBV.parseModelOut: Partially constructed model; remaining elements: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [CV]
ys
                   Maybe (a, [CV])
Nothing      -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"SBV.parseModelOut: Cannot construct a model from: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show SMTModel
m

-- | Given an 'Data.SBV.allSat' call, we typically want to iterate over it and print the results in sequence. The
-- 'displayModels' function automates this task by calling @disp@ on each result, consecutively. The first
-- 'Int' argument to @disp@ 'is the current model number. The second argument is a tuple, where the first
-- element indicates whether the model is alleged (i.e., if the solver is not sure, returning Unknown).
-- The arrange argument can sort the results in any way you like, if necessary.
displayModels :: SatModel a => ([(Bool, a)] -> [(Bool, a)]) -> (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int
displayModels :: forall a.
SatModel a =>
([(Bool, a)] -> [(Bool, a)])
-> (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int
displayModels [(Bool, a)] -> [(Bool, a)]
arrange Int -> (Bool, a) -> IO ()
disp AllSatResult{allSatResults :: AllSatResult -> [SMTResult]
allSatResults = [SMTResult]
ms} = do
    let models :: [(Bool, a)]
models = forall a b. [Either a b] -> [b]
rights (forall a b. (a -> b) -> [a] -> [b]
map (forall a b.
(Modelable a, SatModel b) =>
a -> Either [Char] (Bool, b)
getModelAssignment forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMTResult -> SatResult
SatResult) [SMTResult]
ms)
    [Int]
inds <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Bool, a) -> Int -> IO Int
display ([(Bool, a)] -> [(Bool, a)]
arrange [(Bool, a)]
models) [(Int
1::Int)..]
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
last (Int
0forall a. a -> [a] -> [a]
:[Int]
inds)
  where display :: (Bool, a) -> Int -> IO Int
display (Bool, a)
r Int
i = Int -> (Bool, a) -> IO ()
disp Int
i (Bool, a)
r forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Int
i

-- | Show an SMTResult; generic version
showSMTResult :: String -> String -> String -> String -> (Maybe String -> String) -> String -> SMTResult -> String
showSMTResult :: [Char]
-> [Char]
-> [Char]
-> [Char]
-> (Maybe [Char] -> [Char])
-> [Char]
-> SMTResult
-> [Char]
showSMTResult [Char]
unsatMsg [Char]
unkMsg [Char]
satMsg [Char]
satMsgModel Maybe [Char] -> [Char]
dSatMsgModel [Char]
satExtMsg SMTResult
result = case SMTResult
result of
  Unsatisfiable SMTConfig
_ Maybe [[Char]]
uc                 -> [Char]
unsatMsg forall a. [a] -> [a] -> [a]
++ Maybe [[Char]] -> [Char]
showUnsatCore Maybe [[Char]]
uc
  Satisfiable SMTConfig
_ (SMTModel [([Char], GeneralizedCV)]
_ Maybe [((Quantifier, NamedSymVar), Maybe CV)]
_ [] []) -> [Char]
satMsg
  Satisfiable SMTConfig
_   SMTModel
m                  -> [Char]
satMsgModel    forall a. [a] -> [a] -> [a]
++ SMTConfig -> SMTModel -> [Char]
showModel SMTConfig
cfg SMTModel
m
  DeltaSat    SMTConfig
_ Maybe [Char]
p SMTModel
m                  -> Maybe [Char] -> [Char]
dSatMsgModel Maybe [Char]
p forall a. [a] -> [a] -> [a]
++ SMTConfig -> SMTModel -> [Char]
showModel SMTConfig
cfg SMTModel
m
  SatExtField SMTConfig
_ (SMTModel [([Char], GeneralizedCV)]
b Maybe [((Quantifier, NamedSymVar), Maybe CV)]
_ [([Char], CV)]
_ [([Char], (SBVType, ([([CV], CV)], CV)))]
_)   -> [Char]
satExtMsg   forall a. [a] -> [a] -> [a]
++ Bool -> Bool -> SMTConfig -> [([Char], GeneralizedCV)] -> [Char]
showModelDictionary Bool
True Bool
False SMTConfig
cfg [([Char], GeneralizedCV)]
b
  Unknown     SMTConfig
_ SMTReasonUnknown
r                    -> [Char]
unkMsg forall a. [a] -> [a] -> [a]
++ [Char]
".\n" forall a. [a] -> [a] -> [a]
++ [Char]
"  Reason: " [Char] -> ShowS
`alignPlain` forall a. Show a => a -> [Char]
show SMTReasonUnknown
r
  ProofError  SMTConfig
_ [] Maybe SMTResult
Nothing           -> [Char]
"*** An error occurred. No additional information available. Try running in verbose mode."
  ProofError  SMTConfig
_ [[Char]]
ls Maybe SMTResult
Nothing           -> [Char]
"*** An error occurred.\n" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" (forall a b. (a -> b) -> [a] -> [b]
map ([Char]
"***  " forall a. [a] -> [a] -> [a]
++) [[Char]]
ls)
  ProofError  SMTConfig
_ [[Char]]
ls (Just SMTResult
r)          -> forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" forall a b. (a -> b) -> a -> b
$  [ [Char]
"*** " forall a. [a] -> [a] -> [a]
++ [Char]
l | [Char]
l <- [[Char]]
ls]
                                                         forall a. [a] -> [a] -> [a]
++ [ [Char]
"***"
                                                            , [Char]
"*** Alleged model:"
                                                            , [Char]
"***"
                                                            ]
                                                         forall a. [a] -> [a] -> [a]
++ [[Char]
"*** "  forall a. [a] -> [a] -> [a]
++ [Char]
l | [Char]
l <- [Char] -> [[Char]]
lines ([Char]
-> [Char]
-> [Char]
-> [Char]
-> (Maybe [Char] -> [Char])
-> [Char]
-> SMTResult
-> [Char]
showSMTResult [Char]
unsatMsg [Char]
unkMsg [Char]
satMsg [Char]
satMsgModel Maybe [Char] -> [Char]
dSatMsgModel [Char]
satExtMsg SMTResult
r)]

 where cfg :: SMTConfig
cfg = SMTResult -> SMTConfig
resultConfig SMTResult
result
       showUnsatCore :: Maybe [[Char]] -> [Char]
showUnsatCore Maybe [[Char]]
Nothing   = [Char]
""
       showUnsatCore (Just [[Char]]
xs) = [Char]
". Unsat core:\n" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" [[Char]
"    " forall a. [a] -> [a] -> [a]
++ [Char]
x | [Char]
x <- [[Char]]
xs]

-- | Show a model in human readable form. Ignore bindings to those variables that start
-- with "__internal_sbv_" and also those marked as "nonModelVar" in the config; as these are only for internal purposes
showModel :: SMTConfig -> SMTModel -> String
showModel :: SMTConfig -> SMTModel -> [Char]
showModel SMTConfig
cfg SMTModel
model
   | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([Char], (SBVType, ([([CV], CV)], CV)))]
uiFuncs
   = [Char]
nonUIFuncs
   | Bool
True
   = ShowS
sep [Char]
nonUIFuncs forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n\n" (forall a b. (a -> b) -> [a] -> [b]
map (SMTConfig -> ([Char], (SBVType, ([([CV], CV)], CV))) -> [Char]
showModelUI SMTConfig
cfg) [([Char], (SBVType, ([([CV], CV)], CV)))]
uiFuncs)
   where nonUIFuncs :: [Char]
nonUIFuncs = Bool -> Bool -> SMTConfig -> [([Char], GeneralizedCV)] -> [Char]
showModelDictionary (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([Char], (SBVType, ([([CV], CV)], CV)))]
uiFuncs) Bool
False SMTConfig
cfg [([Char]
n, CV -> GeneralizedCV
RegularCV CV
c) | ([Char]
n, CV
c) <- SMTModel -> [([Char], CV)]
modelAssocs SMTModel
model]
         uiFuncs :: [([Char], (SBVType, ([([CV], CV)], CV)))]
uiFuncs    = SMTModel -> [([Char], (SBVType, ([([CV], CV)], CV)))]
modelUIFuns SMTModel
model
         sep :: ShowS
sep [Char]
""     = [Char]
""
         sep [Char]
x      = [Char]
x forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"

-- | Show bindings in a generalized model dictionary, tabulated
showModelDictionary :: Bool -> Bool -> SMTConfig -> [(String, GeneralizedCV)] -> String
showModelDictionary :: Bool -> Bool -> SMTConfig -> [([Char], GeneralizedCV)] -> [Char]
showModelDictionary Bool
warnEmpty Bool
includeEverything SMTConfig
cfg [([Char], GeneralizedCV)]
allVars
   | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([Char], GeneralizedCV)]
allVars
   = forall {p}. IsString p => p -> p
warn [Char]
"[There are no variables bound by the model.]"
   | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([Char], GeneralizedCV)]
relevantVars
   = forall {p}. IsString p => p -> p
warn [Char]
"[There are no model-variables bound by the model.]"
   | Bool
True
   = forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" forall b c a. (b -> c) -> (a -> b) -> a -> c
. [((Int, [Char]), (Int, [Char]))] -> [[Char]]
display forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall {t :: * -> *} {a}.
Foldable t =>
(t a, GeneralizedCV) -> ((Int, t a), (Int, [Char]))
shM forall a b. (a -> b) -> a -> b
$ [([Char], GeneralizedCV)]
relevantVars
  where warn :: p -> p
warn p
s = if Bool
warnEmpty then p
s else p
""

        relevantVars :: [([Char], GeneralizedCV)]
relevantVars  = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {b}. ([Char], b) -> Bool
ignore) [([Char], GeneralizedCV)]
allVars
        ignore :: ([Char], b) -> Bool
ignore ([Char] -> Text
T.pack -> Text
s, b
_)
          | Bool
includeEverything = Bool
False
          | Bool
True              = Text
"__internal_sbv_" Text -> Text -> Bool
`T.isPrefixOf` Text
s Bool -> Bool -> Bool
|| SMTConfig -> [Char] -> Bool
isNonModelVar SMTConfig
cfg (Text -> [Char]
T.unpack Text
s)

        shM :: (t a, GeneralizedCV) -> ((Int, t a), (Int, [Char]))
shM (t a
s, RegularCV CV
v) = let vs :: [Char]
vs = SMTConfig -> CV -> [Char]
shCV SMTConfig
cfg CV
v in ((forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
s, t a
s), ([Char] -> Int
vlength [Char]
vs, [Char]
vs))
        shM (t a
s, GeneralizedCV
other)       = let vs :: [Char]
vs = forall a. Show a => a -> [Char]
show GeneralizedCV
other in ((forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
s, t a
s), ([Char] -> Int
vlength [Char]
vs, [Char]
vs))

        display :: [((Int, [Char]), (Int, [Char]))] -> [[Char]]
display [((Int, [Char]), (Int, [Char]))]
svs   = forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a}. ((a, [Char]), (a, [Char])) -> [Char]
line [((Int, [Char]), (Int, [Char]))]
svs
           where line :: ((a, [Char]), (a, [Char])) -> [Char]
line ((a
_, [Char]
s), (a
_, [Char]
v)) = [Char]
"  " forall a. [a] -> [a] -> [a]
++ Int -> ShowS
right (Int
nameWidth forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
s) [Char]
s forall a. [a] -> [a] -> [a]
++ [Char]
" = " forall a. [a] -> [a] -> [a]
++ Int -> ShowS
left (Int
valWidth forall a. Num a => a -> a -> a
- [Char] -> Int
lTrimRight (ShowS
valPart [Char]
v)) [Char]
v
                 nameWidth :: Int
nameWidth             = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum forall a b. (a -> b) -> a -> b
$ Int
0 forall a. a -> [a] -> [a]
: [Int
l | ((Int
l, [Char]
_), (Int, [Char])
_) <- [((Int, [Char]), (Int, [Char]))]
svs]
                 valWidth :: Int
valWidth              = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum forall a b. (a -> b) -> a -> b
$ Int
0 forall a. a -> [a] -> [a]
: [Int
l | ((Int, [Char])
_, (Int
l, [Char]
_)) <- [((Int, [Char]), (Int, [Char]))]
svs]

        right :: Int -> ShowS
right Int
p [Char]
s = [Char]
s forall a. [a] -> [a] -> [a]
++ forall a. Int -> a -> [a]
replicate Int
p Char
' '
        left :: Int -> ShowS
left  Int
p [Char]
s = forall a. Int -> a -> [a]
replicate Int
p Char
' ' forall a. [a] -> [a] -> [a]
++ [Char]
s
        vlength :: [Char] -> Int
vlength [Char]
s = case forall a. (a -> Bool) -> [a] -> [a]
dropWhile (forall a. Eq a => a -> a -> Bool
/= Char
':') (forall a. [a] -> [a]
reverse (forall a. (a -> Bool) -> [a] -> [a]
takeWhile (forall a. Eq a => a -> a -> Bool
/= Char
'\n') [Char]
s)) of
                      (Char
':':Char
':':[Char]
r) -> forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace [Char]
r)
                      [Char]
_           -> forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
s -- conservative

        valPart :: ShowS
valPart [Char]
""          = [Char]
""
        valPart (Char
':':Char
':':[Char]
_) = [Char]
""
        valPart (Char
x:[Char]
xs)      = Char
x forall a. a -> [a] -> [a]
: ShowS
valPart [Char]
xs

        lTrimRight :: [Char] -> Int
lTrimRight = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse

-- | Show an uninterpreted function
showModelUI :: SMTConfig -> (String, (SBVType, ([([CV], CV)], CV))) -> String
showModelUI :: SMTConfig -> ([Char], (SBVType, ([([CV], CV)], CV))) -> [Char]
showModelUI SMTConfig
cfg ([Char]
nm, (SBVType [Kind]
ts, ([([CV], CV)]
defs, CV
dflt))) = forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" [[Char]
"  " forall a. [a] -> [a] -> [a]
++ [Char]
l | [Char]
l <- [Char]
sig forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map ([[Char]], [Char]) -> [Char]
align [([[Char]], [Char])]
body]
  where noOfArgs :: Int
noOfArgs = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
ts forall a. Num a => a -> a -> a
- Int
1

        sig :: [Char]
sig      = [Char]
nm forall a. [a] -> [a] -> [a]
++ [Char]
" :: " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate [Char]
" -> " (forall a b. (a -> b) -> [a] -> [b]
map Kind -> [Char]
showBaseKind [Kind]
ts)

        ls :: [([[Char]], [Char])]
ls       = forall a b. (a -> b) -> [a] -> [b]
map ([CV], CV) -> ([[Char]], [Char])
line [([CV], CV)]
defs
        defLine :: ([[Char]], [Char])
defLine  = ([Char]
nm forall a. a -> [a] -> [a]
: forall a. Int -> a -> [a]
replicate Int
noOfArgs [Char]
"_", CV -> [Char]
scv CV
dflt)

        body :: [([[Char]], [Char])]
body     = [([[Char]], [Char])]
ls forall a. [a] -> [a] -> [a]
++ [([[Char]], [Char])
defLine]

        colWidths :: [Int]
colWidths = [forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Char]]
col) | [[Char]]
col <- forall a. [[a]] -> [[a]]
transpose (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [([[Char]], [Char])]
body)]

        resWidth :: Int
resWidth  = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum  (Int
0 forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [([[Char]], [Char])]
body)

        align :: ([[Char]], [Char]) -> [Char]
align ([[Char]]
xs, [Char]
r) = [[Char]] -> [Char]
unwords forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> ShowS
left [Int]
colWidths [[Char]]
xs forall a. [a] -> [a] -> [a]
++ [[Char]
"=", Int -> ShowS
left Int
resWidth [Char]
r]
           where left :: Int -> ShowS
left Int
i [Char]
x = forall a. Int -> [a] -> [a]
take Int
i ([Char]
x forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat Char
' ')

        -- NB. We'll ignore crackNum here. Seems to be overkill while displaying an
        -- uninterpreted function.
        scv :: CV -> [Char]
scv = forall {a}. (Eq a, Num a) => a -> CV -> [Char]
sh (SMTConfig -> Int
printBase SMTConfig
cfg)
          where sh :: a -> CV -> [Char]
sh a
2  = forall a. PrettyNum a => a -> [Char]
binP
                sh a
10 = Bool -> CV -> [Char]
showCV Bool
False
                sh a
16 = forall a. PrettyNum a => a -> [Char]
hexP
                sh a
_  = forall a. Show a => a -> [Char]
show

        -- NB. If we have a float NaN/Infinity/+0/-0 etc. these will
        -- simply print as is, but will not be valid patterns. (We
        -- have the semi-goal of being able to paste these definitions
        -- in a Haskell file.) For the time being, punt on this, but
        -- we might want to do this properly later somehow. (Perhaps
        -- using some sort of a view pattern.)
        line :: ([CV], CV) -> ([String], String)
        line :: ([CV], CV) -> ([[Char]], [Char])
line ([CV]
args, CV
r) = ([Char]
nm forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (ShowS
paren forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> [Char]
scv) [CV]
args, CV -> [Char]
scv CV
r)
          where -- If negative, parenthesize. I think this is the only case
                -- we need to worry about. Hopefully!
                paren :: String -> String
                paren :: ShowS
paren x :: [Char]
x@(Char
'-':[Char]
_) = Char
'(' forall a. a -> [a] -> [a]
: [Char]
x forall a. [a] -> [a] -> [a]
++ [Char]
")"
                paren [Char]
x         = [Char]
x

-- | Show a constant value, in the user-specified base
shCV :: SMTConfig -> CV -> String
shCV :: SMTConfig -> CV -> [Char]
shCV SMTConfig{Int
printBase :: Int
printBase :: SMTConfig -> Int
printBase, Bool
crackNum :: SMTConfig -> Bool
crackNum :: Bool
crackNum} CV
cv = ShowS
cracked (forall {a} {a}.
(Eq a, Num a, PrettyNum a, Show a, Show a) =>
a -> a -> [Char]
sh Int
printBase CV
cv)
  where sh :: a -> a -> [Char]
sh a
2  = forall a. PrettyNum a => a -> [Char]
binS
        sh a
10 = forall a. Show a => a -> [Char]
show
        sh a
16 = forall a. PrettyNum a => a -> [Char]
hexS
        sh a
n  = \a
w -> forall a. Show a => a -> [Char]
show a
w forall a. [a] -> [a] -> [a]
++ [Char]
" -- Ignoring unsupported printBase " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
n forall a. [a] -> [a] -> [a]
++ [Char]
", use 2, 10, or 16."

        cracked :: ShowS
cracked [Char]
def
          | Bool -> Bool
not Bool
crackNum = [Char]
def
          | Bool
True         = case forall a. CrackNum a => a -> Maybe [Char]
CN.crackNum CV
cv of
                             Maybe [Char]
Nothing -> [Char]
def
                             Just [Char]
cs -> [Char]
def forall a. [a] -> [a] -> [a]
++ [Char]
"\n" forall a. [a] -> [a] -> [a]
++ [Char]
cs

-- | Helper function to spin off to an SMT solver.
pipeProcess :: SMTConfig -> State -> String -> [String] -> String -> (State -> IO a) -> IO a
pipeProcess :: forall a.
SMTConfig
-> State -> [Char] -> [[Char]] -> [Char] -> (State -> IO a) -> IO a
pipeProcess SMTConfig
cfg State
ctx [Char]
execName [[Char]]
opts [Char]
pgm State -> IO a
continuation = do
    Maybe [Char]
mbExecPath <- [Char] -> IO (Maybe [Char])
findExecutable [Char]
execName
    case Maybe [Char]
mbExecPath of
      Maybe [Char]
Nothing      -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [ [Char]
"Unable to locate executable for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (SMTSolver -> Solver
name (SMTConfig -> SMTSolver
solver SMTConfig
cfg))
                                      , [Char]
"Executable specified: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Char]
execName
                                      ]

      Just [Char]
execPath -> forall a.
SMTConfig
-> State -> [Char] -> [[Char]] -> [Char] -> (State -> IO a) -> IO a
runSolver SMTConfig
cfg State
ctx [Char]
execPath [[Char]]
opts [Char]
pgm State -> IO a
continuation
                       forall a. IO a -> [Handler a] -> IO a
`C.catches`
                        [ forall a e. Exception e => (e -> IO a) -> Handler a
C.Handler (\(SBVException
e :: SBVException)    -> forall e a. Exception e => e -> IO a
C.throwIO SBVException
e)
                        , forall a e. Exception e => (e -> IO a) -> Handler a
C.Handler (\(ErrorCall
e :: C.ErrorCall)     -> forall e a. Exception e => e -> IO a
C.throwIO ErrorCall
e)
                        , forall a e. Exception e => (e -> IO a) -> Handler a
C.Handler (\(SomeException
e :: C.SomeException) -> forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [ [Char]
"Failed to start the external solver:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show SomeException
e
                                                                                                , [Char]
"Make sure you can start " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Char]
execPath
                                                                                                , [Char]
"from the command line without issues."
                                                                                                ])
                        ]

-- | A standard engine interface. Most solvers follow-suit here in how we "chat" to them..
standardEngine :: String
               -> String
               -> SMTEngine
standardEngine :: [Char] -> [Char] -> SMTEngine
standardEngine [Char]
envName [Char]
envOptName SMTConfig
cfg State
ctx [Char]
pgm State -> IO res
continuation = do

    [Char]
execName <-                    [Char] -> IO [Char]
getEnv [Char]
envName     forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch` (\(SomeException
e :: C.SomeException) -> forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (forall (m :: * -> *) a. Monad m => a -> m a
return (SMTSolver -> [Char]
executable (SMTConfig -> SMTSolver
solver SMTConfig
cfg))))
    [[Char]]
execOpts <- ([Char] -> [[Char]]
splitArgs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap`  [Char] -> IO [Char]
getEnv [Char]
envOptName) forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch` (\(SomeException
e :: C.SomeException) -> forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (forall (m :: * -> *) a. Monad m => a -> m a
return (SMTSolver -> SMTConfig -> [[Char]]
options (SMTConfig -> SMTSolver
solver SMTConfig
cfg) SMTConfig
cfg)))

    let cfg' :: SMTConfig
cfg' = SMTConfig
cfg {solver :: SMTSolver
solver = (SMTConfig -> SMTSolver
solver SMTConfig
cfg) {executable :: [Char]
executable = [Char]
execName, options :: SMTConfig -> [[Char]]
options = forall a b. a -> b -> a
const [[Char]]
execOpts}}

    SMTEngine
standardSolver SMTConfig
cfg' State
ctx [Char]
pgm State -> IO res
continuation

-- | A standard solver interface. If the solver is SMT-Lib compliant, then this function should suffice in
-- communicating with it.
standardSolver :: SMTConfig       -- ^ The current configuration
               -> State           -- ^ Context in which we are running
               -> String          -- ^ The program
               -> (State -> IO a) -- ^ The continuation
               -> IO a
standardSolver :: SMTEngine
standardSolver SMTConfig
config State
ctx [Char]
pgm State -> IO a
continuation = do
    let msg :: [Char] -> m ()
msg [Char]
s    = forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
debug SMTConfig
config [[Char]
"** " forall a. [a] -> [a] -> [a]
++ [Char]
s]
        smtSolver :: SMTSolver
smtSolver= SMTConfig -> SMTSolver
solver SMTConfig
config
        exec :: [Char]
exec     = SMTSolver -> [Char]
executable SMTSolver
smtSolver
        opts :: [[Char]]
opts     = SMTSolver -> SMTConfig -> [[Char]]
options SMTSolver
smtSolver SMTConfig
config forall a. [a] -> [a] -> [a]
++ SMTConfig -> [[Char]]
extraArgs SMTConfig
config
    forall {m :: * -> *}. MonadIO m => [Char] -> m ()
msg forall a b. (a -> b) -> a -> b
$ [Char]
"Calling: "  forall a. [a] -> [a] -> [a]
++ ([Char]
exec forall a. [a] -> [a] -> [a]
++ (if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Char]]
opts then [Char]
"" else [Char]
" ") forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
joinArgs [[Char]]
opts)
    forall a. NFData a => a -> ()
rnf [Char]
pgm seq :: forall a b. a -> b -> b
`seq` forall a.
SMTConfig
-> State -> [Char] -> [[Char]] -> [Char] -> (State -> IO a) -> IO a
pipeProcess SMTConfig
config State
ctx [Char]
exec [[Char]]
opts [Char]
pgm State -> IO a
continuation

-- | An internal type to track of solver interactions
data SolverLine = SolverRegular   String  -- ^ All is well
                | SolverTimeout   String  -- ^ Timeout expired
                | SolverException String  -- ^ Something else went wrong

-- | A variant of @readProcessWithExitCode@; except it deals with SBV continuations
runSolver :: SMTConfig -> State -> FilePath -> [String] -> String -> (State -> IO a) -> IO a
runSolver :: forall a.
SMTConfig
-> State -> [Char] -> [[Char]] -> [Char] -> (State -> IO a) -> IO a
runSolver SMTConfig
cfg State
ctx [Char]
execPath [[Char]]
opts [Char]
pgm State -> IO a
continuation
 = do let nm :: [Char]
nm  = forall a. Show a => a -> [Char]
show (SMTSolver -> Solver
name (SMTConfig -> SMTSolver
solver SMTConfig
cfg))
          msg :: [[Char]] -> IO ()
msg = forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
debug SMTConfig
cfg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map ([Char]
"*** " forall a. [a] -> [a] -> [a]
++)

          clean :: ShowS
clean = SMTSolver -> ShowS
preprocess (SMTConfig -> SMTSolver
solver SMTConfig
cfg)

      (Maybe Int -> [Char] -> IO ()
send, Maybe Int -> [Char] -> IO [Char]
ask, Maybe [Char] -> Maybe Int -> IO [Char]
getResponseFromSolver, IO ([Char], [Char], ExitCode)
terminateSolver, IO ()
cleanUp, ProcessHandle
pid) <- do
                (Handle
inh, Handle
outh, Handle
errh, ProcessHandle
pid) <- [Char]
-> [[Char]]
-> Maybe [Char]
-> Maybe [([Char], [Char])]
-> IO (Handle, Handle, Handle, ProcessHandle)
runInteractiveProcess [Char]
execPath [[Char]]
opts forall a. Maybe a
Nothing forall a. Maybe a
Nothing

                let send :: Maybe Int -> String -> IO ()
                    send :: Maybe Int -> [Char] -> IO ()
send Maybe Int
mbTimeOut [Char]
command = do Handle -> [Char] -> IO ()
hPutStrLn Handle
inh (ShowS
clean [Char]
command)
                                                Handle -> IO ()
hFlush Handle
inh
                                                Maybe [Char] -> Either ([Char], Maybe Int) [Char] -> IO ()
recordTranscript (SMTConfig -> Maybe [Char]
transcript SMTConfig
cfg) forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left ([Char]
command, Maybe Int
mbTimeOut)

                    -- Send a line, get a whole s-expr. We ignore the pathetic case that there might be a string with an unbalanced parentheses in it in a response.
                    ask :: Maybe Int -> String -> IO String
                    ask :: Maybe Int -> [Char] -> IO [Char]
ask Maybe Int
mbTimeOut [Char]
command =
                                  -- solvers don't respond to empty lines or comments; we just pass back
                                  -- success in these cases to keep the illusion of everything has a response
                                  let cmd :: [Char]
cmd = forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace [Char]
command
                                  in if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
cmd Bool -> Bool -> Bool
|| [Char]
";" forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [Char]
cmd
                                     then forall (m :: * -> *) a. Monad m => a -> m a
return [Char]
"success"
                                     else do Maybe Int -> [Char] -> IO ()
send Maybe Int
mbTimeOut [Char]
command
                                             Maybe [Char] -> Maybe Int -> IO [Char]
getResponseFromSolver (forall a. a -> Maybe a
Just [Char]
command) Maybe Int
mbTimeOut

                    -- Get a response from the solver, with an optional time-out on how long
                    -- to wait. Note that there's *always* a time-out of 5 seconds once we get the
                    -- first line of response, as while the solver might take it's time to respond,
                    -- once it starts responding successive lines should come quickly.
                    getResponseFromSolver :: Maybe String -> Maybe Int -> IO String
                    getResponseFromSolver :: Maybe [Char] -> Maybe Int -> IO [Char]
getResponseFromSolver Maybe [Char]
mbCommand Maybe Int
mbTimeOut = do
                                [[Char]]
response <- Bool -> Int -> [[Char]] -> IO [[Char]]
go Bool
True Int
0 []
                                let collated :: [Char]
collated = forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse [[Char]]
response
                                Maybe [Char] -> Either ([Char], Maybe Int) [Char] -> IO ()
recordTranscript (SMTConfig -> Maybe [Char]
transcript SMTConfig
cfg) forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right [Char]
collated
                                forall (m :: * -> *) a. Monad m => a -> m a
return [Char]
collated

                      where safeGetLine :: Bool -> Handle -> IO SolverLine
safeGetLine Bool
isFirst Handle
h =
                                         let timeOutToUse :: Maybe Int
timeOutToUse | Bool
isFirst = Maybe Int
mbTimeOut
                                                          | Bool
True    = forall a. a -> Maybe a
Just Int
5000000
                                             timeOutMsg :: Int -> [Char]
timeOutMsg Int
t | Bool
isFirst = [Char]
"User specified timeout of " forall a. [a] -> [a] -> [a]
++ Int -> [Char]
showTimeoutValue Int
t forall a. [a] -> [a] -> [a]
++ [Char]
" exceeded"
                                                          | Bool
True    = [Char]
"A multiline complete response wasn't received before " forall a. [a] -> [a] -> [a]
++ Int -> [Char]
showTimeoutValue Int
t forall a. [a] -> [a] -> [a]
++ [Char]
" exceeded"

                                             -- Like hGetLine, except it keeps getting lines if inside a string.
                                             getFullLine :: IO String
                                             getFullLine :: IO [Char]
getFullLine = forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> [[Char]] -> IO [[Char]]
collect Bool
False []
                                                where collect :: Bool -> [[Char]] -> IO [[Char]]
collect Bool
inString [[Char]]
sofar = do [Char]
ln <- Handle -> IO [Char]
hGetLine Handle
h

                                                                                  let walk :: Bool -> [Char] -> Bool
walk Bool
inside []           = Bool
inside
                                                                                      walk Bool
inside (Char
'"':[Char]
cs)     = Bool -> [Char] -> Bool
walk (Bool -> Bool
not Bool
inside) [Char]
cs
                                                                                      walk Bool
inside (Char
_:[Char]
cs)       = Bool -> [Char] -> Bool
walk Bool
inside       [Char]
cs

                                                                                      stillInside :: Bool
stillInside = Bool -> [Char] -> Bool
walk Bool
inString [Char]
ln

                                                                                      sofar' :: [[Char]]
sofar' = [Char]
ln forall a. a -> [a] -> [a]
: [[Char]]
sofar

                                                                                  if Bool
stillInside
                                                                                     then Bool -> [[Char]] -> IO [[Char]]
collect Bool
True [[Char]]
sofar'
                                                                                     else forall (m :: * -> *) a. Monad m => a -> m a
return [[Char]]
sofar'

                                         in case Maybe Int
timeOutToUse of
                                              Maybe Int
Nothing -> [Char] -> SolverLine
SolverRegular forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO [Char]
getFullLine
                                              Just Int
t  -> do Maybe [Char]
r <- forall a. Int -> IO a -> IO (Maybe a)
Timeout.timeout Int
t IO [Char]
getFullLine
                                                            case Maybe [Char]
r of
                                                              Just [Char]
l  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Char] -> SolverLine
SolverRegular [Char]
l
                                                              Maybe [Char]
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Char] -> SolverLine
SolverTimeout forall a b. (a -> b) -> a -> b
$ Int -> [Char]
timeOutMsg Int
t


                            go :: Bool -> Int -> [[Char]] -> IO [[Char]]
go Bool
isFirst Int
i [[Char]]
sofar = do
                                            SolverLine
errln <- Bool -> Handle -> IO SolverLine
safeGetLine Bool
isFirst Handle
outh forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch` (\(SomeException
e :: C.SomeException) -> forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> SolverLine
SolverException (forall a. Show a => a -> [Char]
show SomeException
e))))
                                            case SolverLine
errln of
                                              SolverRegular [Char]
ln -> let need :: Int
need  = Int
i forall a. Num a => a -> a -> a
+ [Char] -> Int
parenDeficit [Char]
ln
                                                                      -- make sure we get *something*
                                                                      empty :: Bool
empty = case forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace [Char]
ln of
                                                                                []      -> Bool
True
                                                                                (Char
';':[Char]
_) -> Bool
True   -- yes this does happen! I've seen z3 print out comments on stderr.
                                                                                [Char]
_       -> Bool
False
                                                                  in case (Bool
empty, Int
need forall a. Ord a => a -> a -> Bool
<= Int
0) of
                                                                        (Bool
True, Bool
_)      -> do forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
debug SMTConfig
cfg [[Char]
"[SKIP] " [Char] -> ShowS
`alignPlain` [Char]
ln]
                                                                                             Bool -> Int -> [[Char]] -> IO [[Char]]
go Bool
isFirst Int
need [[Char]]
sofar
                                                                        (Bool
False, Bool
False) -> Bool -> Int -> [[Char]] -> IO [[Char]]
go Bool
False   Int
need ([Char]
lnforall a. a -> [a] -> [a]
:[[Char]]
sofar)
                                                                        (Bool
False, Bool
True)  -> forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
lnforall a. a -> [a] -> [a]
:[[Char]]
sofar)

                                              SolverException [Char]
e -> do ProcessHandle -> IO ()
terminateProcess ProcessHandle
pid
                                                                      forall e a. Exception e => e -> IO a
C.throwIO SBVException { sbvExceptionDescription :: [Char]
sbvExceptionDescription = [Char]
e
                                                                                             , sbvExceptionSent :: Maybe [Char]
sbvExceptionSent        = Maybe [Char]
mbCommand
                                                                                             , sbvExceptionExpected :: Maybe [Char]
sbvExceptionExpected    = forall a. Maybe a
Nothing
                                                                                             , sbvExceptionReceived :: Maybe [Char]
sbvExceptionReceived    = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines (forall a. [a] -> [a]
reverse [[Char]]
sofar)
                                                                                             , sbvExceptionStdOut :: Maybe [Char]
sbvExceptionStdOut      = forall a. Maybe a
Nothing
                                                                                             , sbvExceptionStdErr :: Maybe [Char]
sbvExceptionStdErr      = forall a. Maybe a
Nothing
                                                                                             , sbvExceptionExitCode :: Maybe ExitCode
sbvExceptionExitCode    = forall a. Maybe a
Nothing
                                                                                             , sbvExceptionConfig :: SMTConfig
sbvExceptionConfig      = SMTConfig
cfg { solver :: SMTSolver
solver = (SMTConfig -> SMTSolver
solver SMTConfig
cfg) { executable :: [Char]
executable = [Char]
execPath } }
                                                                                             , sbvExceptionReason :: Maybe [[Char]]
sbvExceptionReason      = forall a. Maybe a
Nothing
                                                                                             , sbvExceptionHint :: Maybe [[Char]]
sbvExceptionHint        = if [Char]
"hGetLine: end of file" forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` [Char]
e
                                                                                                                         then forall a. a -> Maybe a
Just [ [Char]
"Solver process prematurely ended communication."
                                                                                                                                   , [Char]
""
                                                                                                                                   , [Char]
"It is likely it was terminated because of a seg-fault."
                                                                                                                                   , [Char]
"Run with 'transcript=Just \"bad.smt2\"' option, and feed"
                                                                                                                                   , [Char]
"the generated \"bad.smt2\" file directly to the solver"
                                                                                                                                   , [Char]
"outside of SBV for further information."
                                                                                                                                   ]
                                                                                                                         else forall a. Maybe a
Nothing
                                                                                             }

                                              SolverTimeout [Char]
e -> do ProcessHandle -> IO ()
terminateProcess ProcessHandle
pid -- NB. Do not *wait* for the process, just quit.
                                                                    forall e a. Exception e => e -> IO a
C.throwIO SBVException { sbvExceptionDescription :: [Char]
sbvExceptionDescription = [Char]
"Timeout! " forall a. [a] -> [a] -> [a]
++ [Char]
e
                                                                                           , sbvExceptionSent :: Maybe [Char]
sbvExceptionSent        = Maybe [Char]
mbCommand
                                                                                           , sbvExceptionExpected :: Maybe [Char]
sbvExceptionExpected    = forall a. Maybe a
Nothing
                                                                                           , sbvExceptionReceived :: Maybe [Char]
sbvExceptionReceived    = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines (forall a. [a] -> [a]
reverse [[Char]]
sofar)
                                                                                           , sbvExceptionStdOut :: Maybe [Char]
sbvExceptionStdOut      = forall a. Maybe a
Nothing
                                                                                           , sbvExceptionStdErr :: Maybe [Char]
sbvExceptionStdErr      = forall a. Maybe a
Nothing
                                                                                           , sbvExceptionExitCode :: Maybe ExitCode
sbvExceptionExitCode    = forall a. Maybe a
Nothing
                                                                                           , sbvExceptionConfig :: SMTConfig
sbvExceptionConfig      = SMTConfig
cfg { solver :: SMTSolver
solver = (SMTConfig -> SMTSolver
solver SMTConfig
cfg) { executable :: [Char]
executable = [Char]
execPath } }
                                                                                           , sbvExceptionReason :: Maybe [[Char]]
sbvExceptionReason      = forall a. Maybe a
Nothing
                                                                                           , sbvExceptionHint :: Maybe [[Char]]
sbvExceptionHint        = if Bool -> Bool
not (SMTConfig -> Bool
verbose SMTConfig
cfg)
                                                                                                                       then forall a. a -> Maybe a
Just [[Char]
"Run with 'verbose=True' for further information"]
                                                                                                                       else forall a. Maybe a
Nothing
                                                                                           }

                    terminateSolver :: IO ([Char], [Char], ExitCode)
terminateSolver = do Handle -> IO ()
hClose Handle
inh
                                         MVar ()
outMVar <- forall a. IO (MVar a)
newEmptyMVar
                                         [Char]
out <- Handle -> IO [Char]
hGetContents Handle
outh forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch`  (\(SomeException
e :: C.SomeException) -> forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Show a => a -> [Char]
show SomeException
e)))
                                         ThreadId
_ <- IO () -> IO ThreadId
forkIO forall a b. (a -> b) -> a -> b
$ forall a. a -> IO a
C.evaluate (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
out) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a. MVar a -> a -> IO ()
putMVar MVar ()
outMVar ()
                                         [Char]
err <- Handle -> IO [Char]
hGetContents Handle
errh forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch`  (\(SomeException
e :: C.SomeException) -> forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Show a => a -> [Char]
show SomeException
e)))
                                         ThreadId
_ <- IO () -> IO ThreadId
forkIO forall a b. (a -> b) -> a -> b
$ forall a. a -> IO a
C.evaluate (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
err) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a. MVar a -> a -> IO ()
putMVar MVar ()
outMVar ()
                                         forall a. MVar a -> IO a
takeMVar MVar ()
outMVar
                                         forall a. MVar a -> IO a
takeMVar MVar ()
outMVar
                                         Handle -> IO ()
hClose Handle
outh forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch`  (\(SomeException
e :: C.SomeException) -> forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (forall (m :: * -> *) a. Monad m => a -> m a
return ()))
                                         Handle -> IO ()
hClose Handle
errh forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch`  (\(SomeException
e :: C.SomeException) -> forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (forall (m :: * -> *) a. Monad m => a -> m a
return ()))
                                         ExitCode
ex <- ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
pid forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch` (\(SomeException
e :: C.SomeException) -> forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> ExitCode
ExitFailure (-Int
999))))
                                         forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
out, [Char]
err, ExitCode
ex)

                    cleanUp :: IO ()
cleanUp
                      = do ([Char]
out, [Char]
err, ExitCode
ex) <- IO ([Char], [Char], ExitCode)
terminateSolver

                           [[Char]] -> IO ()
msg forall a b. (a -> b) -> a -> b
$   [ [Char]
"Solver   : " forall a. [a] -> [a] -> [a]
++ [Char]
nm
                                   , [Char]
"Exit code: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show ExitCode
ex
                                   ]
                                forall a. [a] -> [a] -> [a]
++ [ [Char]
"Std-out  : " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n           " ([Char] -> [[Char]]
lines [Char]
out) | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
out)]
                                forall a. [a] -> [a] -> [a]
++ [ [Char]
"Std-err  : " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n           " ([Char] -> [[Char]]
lines [Char]
err) | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
err)]

                           Maybe [Char] -> ExitCode -> IO ()
finalizeTranscript (SMTConfig -> Maybe [Char]
transcript SMTConfig
cfg) ExitCode
ex
                           SMTConfig -> State -> IO ()
recordEndTime SMTConfig
cfg State
ctx

                           case ExitCode
ex of
                             ExitCode
ExitSuccess -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
                             ExitCode
_           -> if SMTConfig -> Bool
ignoreExitCode SMTConfig
cfg
                                               then [[Char]] -> IO ()
msg [[Char]
"Ignoring non-zero exit code of " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show ExitCode
ex forall a. [a] -> [a] -> [a]
++ [Char]
" per user request!"]
                                               else forall e a. Exception e => e -> IO a
C.throwIO SBVException { sbvExceptionDescription :: [Char]
sbvExceptionDescription = [Char]
"Failed to complete the call to " forall a. [a] -> [a] -> [a]
++ [Char]
nm
                                                                           , sbvExceptionSent :: Maybe [Char]
sbvExceptionSent        = forall a. Maybe a
Nothing
                                                                           , sbvExceptionExpected :: Maybe [Char]
sbvExceptionExpected    = forall a. Maybe a
Nothing
                                                                           , sbvExceptionReceived :: Maybe [Char]
sbvExceptionReceived    = forall a. Maybe a
Nothing
                                                                           , sbvExceptionStdOut :: Maybe [Char]
sbvExceptionStdOut      = forall a. a -> Maybe a
Just [Char]
out
                                                                           , sbvExceptionStdErr :: Maybe [Char]
sbvExceptionStdErr      = forall a. a -> Maybe a
Just [Char]
err
                                                                           , sbvExceptionExitCode :: Maybe ExitCode
sbvExceptionExitCode    = forall a. a -> Maybe a
Just ExitCode
ex
                                                                           , sbvExceptionConfig :: SMTConfig
sbvExceptionConfig      = SMTConfig
cfg { solver :: SMTSolver
solver = (SMTConfig -> SMTSolver
solver SMTConfig
cfg) { executable :: [Char]
executable = [Char]
execPath } }
                                                                           , sbvExceptionReason :: Maybe [[Char]]
sbvExceptionReason      = forall a. Maybe a
Nothing
                                                                           , sbvExceptionHint :: Maybe [[Char]]
sbvExceptionHint        = if Bool -> Bool
not (SMTConfig -> Bool
verbose SMTConfig
cfg)
                                                                                                       then forall a. a -> Maybe a
Just [[Char]
"Run with 'verbose=True' for further information"]
                                                                                                       else forall a. Maybe a
Nothing
                                                                           }

                forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Int -> [Char] -> IO ()
send, Maybe Int -> [Char] -> IO [Char]
ask, Maybe [Char] -> Maybe Int -> IO [Char]
getResponseFromSolver, IO ([Char], [Char], ExitCode)
terminateSolver, IO ()
cleanUp, ProcessHandle
pid)

      let executeSolver :: IO a
executeSolver = do let sendAndGetSuccess :: Maybe Int -> String -> IO ()
                                 sendAndGetSuccess :: Maybe Int -> [Char] -> IO ()
sendAndGetSuccess Maybe Int
mbTimeOut [Char]
l
                                   -- The pathetic case when the solver doesn't support queries, so we pretend it responded "success"
                                   -- Currently ABC is the only such solver.
                                   | Bool -> Bool
not (SolverCapabilities -> Bool
supportsCustomQueries (SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)))
                                   = do Maybe Int -> [Char] -> IO ()
send Maybe Int
mbTimeOut [Char]
l
                                        forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
debug SMTConfig
cfg [[Char]
"[ISSUE] " [Char] -> ShowS
`alignPlain` [Char]
l]
                                   | Bool
True
                                   = do [Char]
r <- Maybe Int -> [Char] -> IO [Char]
ask Maybe Int
mbTimeOut [Char]
l
                                        case [Char] -> [[Char]]
words [Char]
r of
                                          [[Char]
"success"] -> forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
debug SMTConfig
cfg [[Char]
"[GOOD] " [Char] -> ShowS
`alignPlain` [Char]
l]
                                          [[Char]]
_           -> do forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
debug SMTConfig
cfg [[Char]
"[FAIL] " [Char] -> ShowS
`alignPlain` [Char]
l]

                                                            let isOption :: Bool
isOption = [Char]
"(set-option" forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace [Char]
l

                                                                reason :: [[Char]]
reason | Bool
isOption = [ [Char]
"Backend solver reports it does not support this option."
                                                                                    , [Char]
"Check the spelling, and if correct please report this as a"
                                                                                    , [Char]
"bug/feature request with the solver!"
                                                                                    ]
                                                                       | Bool
True     = [ [Char]
"Check solver response for further information. If your code is correct,"
                                                                                    , [Char]
"please report this as an issue either with SBV or the solver itself!"
                                                                                    ]

                                                            -- put a sync point here before we die so we consume everything
                                                            Either [Char] [Char]
mbExtras <- (forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [Char] -> Maybe Int -> IO [Char]
getResponseFromSolver forall a. Maybe a
Nothing (forall a. a -> Maybe a
Just Int
5000000))
                                                                        forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch` (\(SomeException
e :: C.SomeException) -> forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left (forall a. Show a => a -> [Char]
show SomeException
e))))

                                                            -- Ignore any exceptions from last sync, pointless.
                                                            let extras :: [Char]
extras = case Either [Char] [Char]
mbExtras of
                                                                           Left [Char]
_   -> []
                                                                           Right [Char]
xs -> [Char]
xs

                                                            ([Char]
outOrig, [Char]
errOrig, ExitCode
ex) <- IO ([Char], [Char], ExitCode)
terminateSolver
                                                            let out :: [Char]
out = forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [[Char]]
lines forall a b. (a -> b) -> a -> b
$ [Char]
outOrig
                                                                err :: [Char]
err = forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [[Char]]
lines forall a b. (a -> b) -> a -> b
$ [Char]
errOrig

                                                                exc :: SBVException
exc = SBVException { sbvExceptionDescription :: [Char]
sbvExceptionDescription = [Char]
"Unexpected non-success response from " forall a. [a] -> [a] -> [a]
++ [Char]
nm
                                                                                   , sbvExceptionSent :: Maybe [Char]
sbvExceptionSent        = forall a. a -> Maybe a
Just [Char]
l
                                                                                   , sbvExceptionExpected :: Maybe [Char]
sbvExceptionExpected    = forall a. a -> Maybe a
Just [Char]
"success"
                                                                                   , sbvExceptionReceived :: Maybe [Char]
sbvExceptionReceived    = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [Char]
r forall a. [a] -> [a] -> [a]
++ [Char]
"\n" forall a. [a] -> [a] -> [a]
++ [Char]
extras
                                                                                   , sbvExceptionStdOut :: Maybe [Char]
sbvExceptionStdOut      = forall a. a -> Maybe a
Just [Char]
out
                                                                                   , sbvExceptionStdErr :: Maybe [Char]
sbvExceptionStdErr      = forall a. a -> Maybe a
Just [Char]
err
                                                                                   , sbvExceptionExitCode :: Maybe ExitCode
sbvExceptionExitCode    = forall a. a -> Maybe a
Just ExitCode
ex
                                                                                   , sbvExceptionConfig :: SMTConfig
sbvExceptionConfig      = SMTConfig
cfg { solver :: SMTSolver
solver = (SMTConfig -> SMTSolver
solver SMTConfig
cfg) {executable :: [Char]
executable = [Char]
execPath } }
                                                                                   , sbvExceptionReason :: Maybe [[Char]]
sbvExceptionReason      = forall a. a -> Maybe a
Just [[Char]]
reason
                                                                                   , sbvExceptionHint :: Maybe [[Char]]
sbvExceptionHint        = forall a. Maybe a
Nothing
                                                                                   }

                                                            forall e a. Exception e => e -> IO a
C.throwIO SBVException
exc

                             -- Mark in the log, mostly.
                             Maybe Int -> [Char] -> IO ()
sendAndGetSuccess forall a. Maybe a
Nothing [Char]
"; Automatically generated by SBV. Do not edit."

                             -- First check that the solver supports :print-success
                             let backend :: Solver
backend = SMTSolver -> Solver
name forall a b. (a -> b) -> a -> b
$ SMTConfig -> SMTSolver
solver SMTConfig
cfg
                             if Bool -> Bool
not (SolverCapabilities -> Bool
supportsCustomQueries (SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)))
                                then forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
debug SMTConfig
cfg [[Char]
"** Skipping heart-beat for the solver " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Solver
backend]
                                else do let heartbeat :: [Char]
heartbeat = [Char]
"(set-option :print-success true)"
                                        [Char]
r <- Maybe Int -> [Char] -> IO [Char]
ask (forall a. a -> Maybe a
Just Int
5000000) [Char]
heartbeat  -- Give the solver 5s to respond, this should be plenty enough!
                                        case [Char] -> [[Char]]
words [Char]
r of
                                          [[Char]
"success"]     -> forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
debug SMTConfig
cfg [[Char]
"[GOOD] " forall a. [a] -> [a] -> [a]
++ [Char]
heartbeat]
                                          [[Char]
"unsupported"] -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [ [Char]
""
                                                                             , [Char]
"*** Backend solver (" forall a. [a] -> [a] -> [a]
++  forall a. Show a => a -> [Char]
show Solver
backend forall a. [a] -> [a] -> [a]
++ [Char]
") does not support the command:"
                                                                             , [Char]
"***"
                                                                             , [Char]
"***     (set-option :print-success true)"
                                                                             , [Char]
"***"
                                                                             , [Char]
"*** SBV relies on this feature to coordinate communication!"
                                                                             , [Char]
"*** Please request this as a feature!"
                                                                             ]
                                          [[Char]]
_               -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [ [Char]
""
                                                                             , [Char]
"*** Data.SBV: Failed to initiate contact with the solver!"
                                                                             , [Char]
"***"
                                                                             , [Char]
"***   Sent    : " forall a. [a] -> [a] -> [a]
++ [Char]
heartbeat
                                                                             , [Char]
"***   Expected: success"
                                                                             , [Char]
"***   Received: " forall a. [a] -> [a] -> [a]
++ [Char]
r
                                                                             , [Char]
"***"
                                                                             , [Char]
"*** Try running in debug mode for further information."
                                                                             ]

                             -- For push/pop support, we require :global-declarations to be true. But not all solvers
                             -- support this. Issue it if supported. (If not, we'll reject pop calls.)
                             if Bool -> Bool
not (SolverCapabilities -> Bool
supportsGlobalDecls (SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)))
                                then forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
debug SMTConfig
cfg [ [Char]
"** Backend solver " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Solver
backend forall a. [a] -> [a] -> [a]
++ [Char]
" does not support global decls."
                                               , [Char]
"** Some incremental calls, such as pop, will be limited."
                                               ]
                                else Maybe Int -> [Char] -> IO ()
sendAndGetSuccess forall a. Maybe a
Nothing [Char]
"(set-option :global-declarations true)"

                             -- Now dump the program!
                             forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Maybe Int -> [Char] -> IO ()
sendAndGetSuccess forall a. Maybe a
Nothing) ([[Char]] -> [[Char]]
mergeSExpr ([Char] -> [[Char]]
lines [Char]
pgm))

                             -- Prepare the query context and ship it off
                             let qs :: QueryState
qs = QueryState { queryAsk :: Maybe Int -> [Char] -> IO [Char]
queryAsk                 = Maybe Int -> [Char] -> IO [Char]
ask
                                                 , querySend :: Maybe Int -> [Char] -> IO ()
querySend                = Maybe Int -> [Char] -> IO ()
send
                                                 , queryRetrieveResponse :: Maybe Int -> IO [Char]
queryRetrieveResponse    = Maybe [Char] -> Maybe Int -> IO [Char]
getResponseFromSolver forall a. Maybe a
Nothing
                                                 , queryConfig :: SMTConfig
queryConfig              = SMTConfig
cfg
                                                 , queryTerminate :: IO ()
queryTerminate           = IO ()
cleanUp
                                                 , queryTimeOutValue :: Maybe Int
queryTimeOutValue        = forall a. Maybe a
Nothing
                                                 , queryAssertionStackDepth :: Int
queryAssertionStackDepth = Int
0
                                                 }
                                 qsp :: IORef (Maybe QueryState)
qsp = State -> IORef (Maybe QueryState)
rQueryState State
ctx

                             Maybe QueryState
mbQS <- forall a. IORef a -> IO a
readIORef IORef (Maybe QueryState)
qsp

                             case Maybe QueryState
mbQS of
                               Maybe QueryState
Nothing -> forall a. IORef a -> a -> IO ()
writeIORef IORef (Maybe QueryState)
qsp (forall a. a -> Maybe a
Just QueryState
qs)
                               Just QueryState
_  -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [ [Char]
""
                                                          , [Char]
"Data.SBV: Impossible happened, query-state was already set."
                                                          , [Char]
"Please report this as a bug!"
                                                          ]

                             -- off we go!
                             State -> IO a
continuation State
ctx

      -- NB. Don't use 'bracket' here, as it wouldn't have access to the exception.
      let launchSolver :: IO a
launchSolver = do Maybe [Char] -> SMTConfig -> IO ()
startTranscript (SMTConfig -> Maybe [Char]
transcript SMTConfig
cfg) SMTConfig
cfg
                            IO a
executeSolver

      IO a
launchSolver forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch` (\(SomeException
e :: C.SomeException) -> forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e forall a b. (a -> b) -> a -> b
$ do ProcessHandle -> IO ()
terminateProcess ProcessHandle
pid
                                                                            ExitCode
ec <- ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
pid
                                                                            Maybe [Char] -> [Char] -> IO ()
recordException    (SMTConfig -> Maybe [Char]
transcript SMTConfig
cfg) (forall a. Show a => a -> [Char]
show SomeException
e)
                                                                            Maybe [Char] -> ExitCode -> IO ()
finalizeTranscript (SMTConfig -> Maybe [Char]
transcript SMTConfig
cfg) ExitCode
ec
                                                                            SMTConfig -> State -> IO ()
recordEndTime SMTConfig
cfg State
ctx
                                                                            forall e a. Exception e => e -> IO a
C.throwIO SomeException
e)

-- | Compute and report the end time
recordEndTime :: SMTConfig -> State -> IO ()
recordEndTime :: SMTConfig -> State -> IO ()
recordEndTime SMTConfig{Timing
timing :: SMTConfig -> Timing
timing :: Timing
timing} State
state = case Timing
timing of
                                           Timing
NoTiming        -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                           Timing
PrintTiming     -> do NominalDiffTime
e <- IO NominalDiffTime
elapsed
                                                                 [Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ [Char]
"*** SBV: Elapsed time: " forall a. [a] -> [a] -> [a]
++ NominalDiffTime -> [Char]
showTDiff NominalDiffTime
e
                                           SaveTiming IORef NominalDiffTime
here -> forall a. IORef a -> a -> IO ()
writeIORef IORef NominalDiffTime
here forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO NominalDiffTime
elapsed
  where elapsed :: IO NominalDiffTime
elapsed = IO UTCTime
getCurrentTime forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \UTCTime
end -> forall (m :: * -> *) a. Monad m => a -> m a
return 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
_   = forall (m :: * -> *) a. Monad m => a -> m a
return ()
startTranscript (Just [Char]
f) SMTConfig
cfg = do [Char]
ts <- forall a. Show a => a -> [Char]
show 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 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 :: SMTConfig -> [[Char]]
options :: SMTSolver -> 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 " forall a. [a] -> [a] -> [a]
++ [Char]
ts
                                  , [Char]
";;;"
                                  , [Char]
";;;           Solver    : " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Solver
name
                                  , [Char]
";;;           Executable: " forall a. [a] -> [a] -> [a]
++ forall a. a -> Maybe a -> a
fromMaybe [Char]
"Unable to locate the executable" Maybe [Char]
mbPath
                                  , [Char]
";;;           Options   : " forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
unwords (SMTConfig -> [[Char]]
options SMTConfig
cfg 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
_  = forall (m :: * -> *) a. Monad m => a -> m a
return ()
finalizeTranscript (Just [Char]
f) ExitCode
ec = do [Char]
ts <- forall a. Show a => a -> [Char]
show forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO ZonedTime
getZonedTime
                                    [Char] -> [Char] -> IO ()
appendFile [Char]
f forall a b. (a -> b) -> a -> b
$ ShowS
end [Char]
ts
  where end :: ShowS
end [Char]
ts = [[Char]] -> [Char]
unlines [ [Char]
""
                         , [Char]
";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                         , [Char]
";;;"
                         , [Char]
";;; SBV: Finished at " forall a. [a] -> [a] -> [a]
++ [Char]
ts
                         , [Char]
";;;"
                         , [Char]
";;; Exit code: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show ExitCode
ec
                         , [Char]
";;;"
                         , [Char]
";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                         ]

-- If requested, record in the transcript file
recordTranscript :: Maybe FilePath -> Either (String, Maybe Int) String -> IO ()
recordTranscript :: Maybe [Char] -> Either ([Char], Maybe Int) [Char] -> IO ()
recordTranscript Maybe [Char]
Nothing  Either ([Char], Maybe Int) [Char]
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()
recordTranscript (Just [Char]
f) Either ([Char], Maybe Int) [Char]
m = do [Char]
tsPre <- forall t. FormatTime t => TimeLocale -> [Char] -> t -> [Char]
formatTime TimeLocale
defaultTimeLocale [Char]
"; [%T%Q" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO ZonedTime
getZonedTime
                                 let ts :: [Char]
ts = forall a. Int -> [a] -> [a]
take Int
15 forall a b. (a -> b) -> a -> b
$ [Char]
tsPre forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat Char
'0'
                                 case Either ([Char], Maybe Int) [Char]
m of
                                   Left  ([Char]
sent, Maybe Int
mbTimeOut) -> [Char] -> [Char] -> IO ()
appendFile [Char]
f forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines forall a b. (a -> b) -> a -> b
$ ([Char]
ts forall a. [a] -> [a] -> [a]
++ [Char]
"] " forall a. [a] -> [a] -> [a]
++ Maybe Int -> [Char]
to Maybe Int
mbTimeOut forall a. [a] -> [a] -> [a]
++ [Char]
"Sending:") forall a. a -> [a] -> [a]
: [Char] -> [[Char]]
lines [Char]
sent
                                   Right [Char]
recv              -> [Char] -> [Char] -> IO ()
appendFile [Char]
f forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines forall a b. (a -> b) -> a -> b
$ case [Char] -> [[Char]]
lines (forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace [Char]
recv) of
                                                                                        []  -> [[Char]
ts forall a. [a] -> [a] -> [a]
++ [Char]
"] Received: <NO RESPONSE>"]  -- can't really happen.
                                                                                        [[Char]
x] -> [[Char]
ts forall a. [a] -> [a] -> [a]
++ [Char]
"] Received: " forall a. [a] -> [a] -> [a]
++ [Char]
x]
                                                                                        [[Char]]
xs  -> ([Char]
ts forall a. [a] -> [a] -> [a]
++ [Char]
"] Received: ") forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map ([Char]
";   " forall a. [a] -> [a] -> [a]
++) [[Char]]
xs
        where to :: Maybe Int -> [Char]
to Maybe Int
Nothing  = [Char]
""
              to (Just Int
i) = [Char]
"[Timeout: " forall a. [a] -> [a] -> [a]
++ Int -> [Char]
showTimeoutValue Int
i 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]
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()
recordException (Just [Char]
f) [Char]
m = do [Char]
ts <- forall a. Show a => a -> [Char]
show forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO ZonedTime
getZonedTime
                                [Char] -> [Char] -> IO ()
appendFile [Char]
f forall a b. (a -> b) -> a -> b
$ ShowS
exc [Char]
ts
  where exc :: ShowS
exc [Char]
ts = [[Char]] -> [Char]
unlines forall a b. (a -> b) -> a -> b
$ [ [Char]
""
                           , [Char]
";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                           , [Char]
";;;"
                           , [Char]
";;; SBV: Caught an exception at " forall a. [a] -> [a] -> [a]
++ [Char]
ts
                           , [Char]
";;;"
                           ]
                        forall a. [a] -> [a] -> [a]
++ [ [Char]
";;;   " forall a. [a] -> [a] -> [a]
++ [Char]
l | [Char]
l <- forall a. (a -> Bool) -> [a] -> [a]
dropWhile forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Char] -> [[Char]]
lines [Char]
m) ]
                        forall a. [a] -> [a] -> [a]
++ [ [Char]
";;;"
                           , [Char]
";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                           ]

-- We should not be catching/processing asynchronous exceptions.
-- See http://github.com/LeventErkok/sbv/issues/410
handleAsync :: C.SomeException -> IO a -> IO a
handleAsync :: forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e IO a
cont
  | Bool
isAsynchronous = forall e a. Exception e => e -> IO a
C.throwIO SomeException
e
  | Bool
True           = IO a
cont
  where -- Stealing this definition from the asynchronous exceptions package to reduce dependencies
        isAsynchronous :: Bool
        isAsynchronous :: Bool
isAsynchronous = forall a. Maybe a -> Bool
isJust (forall e. Exception e => SomeException -> Maybe e
C.fromException SomeException
e :: Maybe C.AsyncException) Bool -> Bool -> Bool
|| forall a. Maybe a -> Bool
isJust (forall e. Exception e => SomeException -> Maybe e
C.fromException SomeException
e :: Maybe C.SomeAsyncException)