    -----------------------------------------------------------------------------
    -- |
    -- 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, mplus)
    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, hReady, hGetChar)
    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(..), mustIgnoreVar)
    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 -> ()
    (ThmResult -> ()) -> NFData ThmResult
    forall a. (a -> ()) -> NFData a
    $crnf :: ThmResult -> ()
    rnf :: 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 -> ()
    (SatResult -> ()) -> NFData SatResult
    forall a. (a -> ()) -> NFData a
    $crnf :: SatResult -> ()
    rnf :: 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
    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) -> Maybe Int -> Double -> ShowS
    forall a. RealFloat a => Maybe Int -> a -> ShowS
    showFFloat Maybe Int
    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: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SMTResult -> Maybe [Char] -> [Char]
    getPrecision SMTResult
    r Maybe [Char]
    mbP [Char] -> ShowS
    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: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SMTResult -> Maybe [Char] -> [Char]
    getPrecision SMTResult
    r Maybe [Char]
    mbP [Char] -> ShowS
    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: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SMTResult -> Maybe [Char] -> [Char]
    getPrecision SMTResult
    r Maybe [Char]
    mbP [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ". Model:\n")
                                                         (ShowS
    tag [Char]
    "Violated in an extension field:\n")
                                                         SMTResult
    r
            where loc :: [Char]
    loc   = [Char] -> ShowS -> Maybe [Char] -> [Char]
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe [Char]
    "" ([Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ": ") Maybe [Char]
    mbLoc
                  tag :: ShowS
    tag [Char]
    s = [Char]
    loc [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    msg [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ": " [Char] -> ShowS
    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
                        , allSatSolverReturnedUnknown :: AllSatResult -> Bool
    allSatSolverReturnedUnknown = Bool
    u
                        , allSatSolverReturnedDSat :: AllSatResult -> Bool
    allSatSolverReturnedDSat    = Bool
    d
                        , allSatResults :: AllSatResult -> [SMTResult]
    allSatResults               = [SMTResult]
    xs
                        } = Int -> [SMTResult] -> [Char]
    forall {a}. (Eq a, Num a, Show a) => a -> [SMTResult] -> [Char]
    go (Int
    0::Int) [SMTResult]
    xs
        where warnings :: [Char]
    warnings | Bool
    u    = [Char]
    " (Search stopped since solver has returned unknown.)"
                       | Bool
    True = [Char]
    ""

              go :: a -> [SMTResult] -> [Char]
    go a
    c (SMTResult
    s:[SMTResult]
    ss) = let c' :: a
    c'      = a
    ca -> a -> a
    forall a. Num a => a -> a -> a
    +a
    1
                                (Bool
    ok, [Char]
    o) = a -> SMTResult -> (Bool, [Char])
    forall {a}. Show a => a -> SMTResult -> (Bool, [Char])
    sh a
    c' SMTResult
    s
                            in a
    c' a -> ShowS
    forall a b. a -> b -> b
    `seq` if Bool
    ok then [Char]
    o [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\n" [Char] -> ShowS
    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."  [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    warnings
                              (Bool
    _   ,  Bool
    True, a
    _) -> [Char]
    "Search stopped since the result was delta-satisfiable." [Char] -> ShowS
    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." [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    warnings
                              (Bool
    False, Bool
    _   , a
    _) -> [Char]
    "Found " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> [Char]
    forall a. Show a => a -> [Char]
    show a
    c [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " different solutions." [Char] -> ShowS
    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 #" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> [Char]
    forall a. Show a => a -> [Char]
    show a
    i [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ":\nSatisfiable") ([Char]
    "Solution #" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> [Char]
    forall a. Show a => a -> [Char]
    show a
    i [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ":\n")
                                          (\Maybe [Char]
    mbP -> [Char]
    "Solution $" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> [Char]
    forall a. Show a => a -> [Char]
    show a
    i [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " with delta-satisfiability, precision: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SMTResult -> Maybe [Char] -> [Char]
    getPrecision SMTResult
    c Maybe [Char]
    mbP [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ":\n")
                                          ([Char]
    "Solution $" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> [Char]
    forall a. Show a => a -> [Char]
    show a
    i [Char] -> ShowS
    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   -> ShowS -> SMTResult -> [Char]
    forall {t}. IsString t => (t -> [Char]) -> SMTResult -> [Char]
    sh ShowS
    forall a. a -> a
    id SMTResult
    r

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

                   ParetoResult (Bool
    False, [SMTResult
    r]) -> ShowS -> SMTResult -> [Char]
    forall {t}. IsString t => (t -> [Char]) -> SMTResult -> [Char]
    sh ([Char]
    "Unique pareto front: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++) SMTResult
    r
                   ParetoResult (Bool
    False, [SMTResult]
    rs)  -> [Char] -> [[Char]] -> [Char]
    multi [Char]
    "pareto optimal values" ((Int -> SMTResult -> [Char]) -> [Int] -> [SMTResult] -> [[Char]]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Int -> SMTResult -> [Char]
    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" ((Int -> SMTResult -> [Char]) -> [Int] -> [SMTResult] -> [[Char]]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Int -> SMTResult -> [Char]
    forall {a}. Show a => a -> SMTResult -> [Char]
    shP [(Int
    1::Int)..] [SMTResult]
    rs)
                                               [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\n*** Note: Pareto-front extraction was terminated as requested by the user."
                                               [Char] -> ShowS
    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 " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    w [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " to display models for."
                 multi [Char]
    _ [[Char]]
    xs = [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    intercalate [Char]
    "\n" [[Char]]
    xs

                 shI :: a -> SMTResult -> [Char]
    shI a
    n = ShowS -> SMTResult -> [Char]
    forall {t}. IsString t => (t -> [Char]) -> SMTResult -> [Char]
    sh (\[Char]
    s -> [Char]
    "Objective "     [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> [Char]
    forall a. Show a => a -> [Char]
    show a
    n [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ": " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    s)
                 shP :: a -> SMTResult -> [Char]
    shP a
    i = ShowS -> SMTResult -> [Char]
    forall {t}. IsString t => (t -> [Char]) -> SMTResult -> [Char]
    sh (\[Char]
    s -> [Char]
    "Pareto front #" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> [Char]
    forall a. Show a => a -> [Char]
    show a
    i [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ": " [Char] -> ShowS
    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:" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\n")
                                          (\Maybe [Char]
    mbP -> t -> [Char]
    tag t
    "Optimal model with delta-satisfiability, precision: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SMTResult -> Maybe [Char] -> [Char]
    getPrecision SMTResult
    r Maybe [Char]
    mbP [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ":" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\n")
                                          (t -> [Char]
    tag t
    "Optimal in an extension field:" [Char] -> ShowS
    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 Maybe (a, [CV])
    -> ((a, [CV]) -> Maybe (b, [CV])) -> Maybe (b, [CV])
    forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \(a
    a, [CV]
    r) -> a -> Maybe b
    f a
    a Maybe b -> (b -> Maybe (b, [CV])) -> Maybe (b, [CV])
    forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \b
    b -> (b, [CV]) -> Maybe (b, [CV])
    forall a. a -> Maybe a
    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) = (a, [CV]) -> Maybe (a, [CV])
    forall a. a -> Maybe a
    Just ([Char] -> a
    forall a. Read a => [Char] -> a
    read [Char]
    s, [CV]
    r)
      parseCVs [CV]
    _                             = Maybe (a, [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) | CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    x Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    k = (a, [CV]) -> Maybe (a, [CV])
    forall a. a -> Maybe a
    Just (Integer -> a
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Integer
    i, [CV]
    r)
    genParse Kind
    _ [CV]
    _                                         = Maybe (a, [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 = ((), [CV]) -> Maybe ((), [CV])
    forall a. a -> Maybe a
    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) <- Kind -> [CV] -> Maybe (Integer, [CV])
    forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
    genParse Kind
    KBool [CV]
    xs
                       (Bool, [CV]) -> Maybe (Bool, [CV])
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Integer
    x :: Integer) Integer -> Integer -> Bool
    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 = Kind -> [CV] -> Maybe (Word8, [CV])
    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 = Kind -> [CV] -> Maybe (Int8, [CV])
    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 = Kind -> [CV] -> Maybe (Word16, [CV])
    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 = Kind -> [CV] -> Maybe (Int16, [CV])
    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 = Kind -> [CV] -> Maybe (Word32, [CV])
    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 = Kind -> [CV] -> Maybe (Int32, [CV])
    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 = Kind -> [CV] -> Maybe (Word64, [CV])
    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 = Kind -> [CV] -> Maybe (Int64, [CV])
    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 = Kind -> [CV] -> Maybe (Integer, [CV])
    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) = (AlgReal, [CV]) -> Maybe (AlgReal, [CV])
    forall a. a -> Maybe a
    Just (AlgReal
    i, [CV]
    r)
      parseCVs [CV]
    _                           = Maybe (AlgReal, [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) = (Float, [CV]) -> Maybe (Float, [CV])
    forall a. a -> Maybe a
    Just (Float
    i, [CV]
    r)
      parseCVs [CV]
    _                          = Maybe (Float, [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) = (Double, [CV]) -> Maybe (Double, [CV])
    forall a. a -> Maybe a
    Just (Double
    i, [CV]
    r)
      parseCVs [CV]
    _                            = Maybe (Double, [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)
        | Proxy eb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @eb) Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    ei , Proxy sb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @sb) Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    si = (FloatingPoint eb sb, [CV]) -> Maybe (FloatingPoint eb sb, [CV])
    forall a. a -> Maybe a
    Just (FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint FP
    fp, [CV]
    r)
      parseCVs [CV]
    _                                                      = Maybe (FloatingPoint eb sb, [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) = (CV, [CV]) -> Maybe (CV, [CV])
    forall a. a -> Maybe a
    Just (CV
    cv, [CV]
    r)
      parseCVs []       = Maybe (CV, [CV])
    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) = ([Char], [CV]) -> Maybe ([Char], [CV])
    forall a. a -> Maybe a
    Just ([Char]
    c, [CV]
    r)
      parseCVs [CV]
    _                    = Maybe ([Char], [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) = (Char, [CV]) -> Maybe (Char, [CV])
    forall a. a -> Maybe a
    Just (Char
    c, [CV]
    r)
      parseCVs [CV]
    _                  = Maybe (Char, [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 [] = ([a], [CV]) -> Maybe ([a], [CV])
    forall a. a -> Maybe a
    Just ([], [])
      parseCVs [CV]
    xs = case [CV] -> Maybe (a, [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV]
    xs of
                      Just (a
    a, [CV]
    ys) -> case [CV] -> Maybe ([a], [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV]
    ys of
                                        Just ([a]
    as, [CV]
    zs) -> ([a], [CV]) -> Maybe ([a], [CV])
    forall a. a -> Maybe a
    Just (a
    aa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    as, [CV]
    zs)
                                        Maybe ([a], [CV])
    Nothing       -> ([a], [CV]) -> Maybe ([a], [CV])
    forall a. a -> Maybe a
    Just ([], [CV]
    ys)
                      Maybe (a, [CV])
    Nothing     -> ([a], [CV]) -> Maybe ([a], [CV])
    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) <- [CV] -> Maybe (a, [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV]
    as
                       (b
    b, [CV]
    cs) <- [CV] -> Maybe (b, [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV]
    bs
                       ((a, b), [CV]) -> Maybe ((a, b), [CV])
    forall a. a -> Maybe a
    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) <- [CV] -> Maybe (a, [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV]
    as
                       ((b
    b, c
    c), [CV]
    ds) <- [CV] -> Maybe ((b, c), [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV]
    bs
                       ((a, b, c), [CV]) -> Maybe ((a, b, c), [CV])
    forall a. a -> Maybe a
    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) <- [CV] -> Maybe (a, [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV]
    as
                       ((b
    b, c
    c, d
    d), [CV]
    es) <- [CV] -> Maybe ((b, c, d), [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV]
    bs
                       ((a, b, c, d), [CV]) -> Maybe ((a, b, c, d), [CV])
    forall a. a -> Maybe a
    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)            <- [CV] -> Maybe (a, [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV]
    as
                       ((b
    b, c
    c, d
    d, e
    e), [CV]
    fs) <- [CV] -> Maybe ((b, c, d, e), [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV]
    bs
                       ((a, b, c, d, e), [CV]) -> Maybe ((a, b, c, d, e), [CV])
    forall a. a -> Maybe a
    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)               <- [CV] -> Maybe (a, [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV]
    as
                       ((b
    b, c
    c, d
    d, e
    e, f
    f), [CV]
    gs) <- [CV] -> Maybe ((b, c, d, e, f), [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV]
    bs
                       ((a, b, c, d, e, f), [CV]) -> Maybe ((a, b, c, d, e, f), [CV])
    forall a. a -> Maybe a
    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)                  <- [CV] -> Maybe (a, [CV])
    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) <- [CV] -> Maybe ((b, c, d, e, f, g), [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV]
    bs
                       ((a, b, c, d, e, f, g), [CV])
    -> Maybe ((a, b, c, d, e, f, g), [CV])
    forall a. a -> Maybe a
    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 = CV -> b
    forall a. SymVal a => CV -> a
    fromCV (CV -> b) -> Maybe CV -> Maybe b
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` ([Char]
    v [Char] -> Map [Char] CV -> Maybe CV
    forall k a. Ord k => k -> Map k a -> Maybe a
    `M.lookup` a -> Map [Char] CV
    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 [Char] -> Map [Char] CV -> Maybe CV
    forall k a. Ord k => k -> Map k a -> Maybe a
    `M.lookup` a -> Map [Char] CV
    forall a. Modelable a => a -> Map [Char] CV
    getModelDictionary a
    r of
                                         Just (CV Kind
    _ (CUserSort (Maybe Int
    _, [Char]
    s))) -> [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    s
                                         Maybe CV
    _                              -> Maybe [Char]
    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 a -> Either [Char] (Bool, b)
    forall a b.
    (Modelable a, SatModel b) =>
    a -> Either [Char] (Bool, b)
    forall b. SatModel b => a -> Either [Char] (Bool, b)
    getModelAssignment a
    a of
                         Right (Bool
    _, b
    b) -> b -> Maybe b
    forall a. a -> Maybe a
    Just b
    b
                         Either [Char] (Bool, b)
    _            -> Maybe 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 [Char] -> Map [Char] GeneralizedCV -> Maybe GeneralizedCV
    forall k a. Ord k => k -> Map k a -> Maybe a
    `M.lookup` a -> Map [Char] GeneralizedCV
    forall a. Modelable a => a -> Map [Char] GeneralizedCV
    getModelObjectives a
    r

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

      -- | Extract the value of an uninterpreted-function as an association list
      getModelUIFunValue :: String -> a -> Maybe (SBVType, Either String ([([CV], CV)], CV))
      getModelUIFunValue [Char]
    v a
    r = [Char]
    v [Char]
    -> Map [Char] (SBVType, Either [Char] ([([CV], CV)], CV))
    -> Maybe (SBVType, Either [Char] ([([CV], CV)], CV))
    forall k a. Ord k => k -> Map k a -> Maybe a
    `M.lookup` a -> Map [Char] (SBVType, Either [Char] ([([CV], CV)], CV))
    forall a.
    Modelable a =>
    a -> Map [Char] (SBVType, Either [Char] ([([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) <- (SMTResult -> Either [Char] (Bool, a))
    -> [SMTResult] -> [Either [Char] (Bool, a)]
    forall a b. (a -> b) -> [a] -> [b]
    map SMTResult -> Either [Char] (Bool, a)
    forall a b.
    (Modelable a, SatModel b) =>
    a -> Either [Char] (Bool, b)
    forall b. SatModel b => SMTResult -> 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} = (SMTResult -> Map [Char] CV) -> [SMTResult] -> [Map [Char] CV]
    forall a b. (a -> b) -> [a] -> [b]
    map SMTResult -> Map [Char] CV
    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} =  (SMTResult -> Maybe b) -> [SMTResult] -> [Maybe b]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char]
    s [Char] -> SMTResult -> Maybe b
    forall b. SymVal b => [Char] -> SMTResult -> Maybe b
    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} =  (SMTResult -> Maybe [Char]) -> [SMTResult] -> [Maybe [Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char]
    s [Char] -> SMTResult -> Maybe [Char]
    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) = SMTResult -> Either [Char] (Bool, b)
    forall a b.
    (Modelable a, SatModel b) =>
    a -> Either [Char] (Bool, b)
    forall b. SatModel b => SMTResult -> Either [Char] (Bool, b)
    getModelAssignment SMTResult
    r
      modelExists :: ThmResult -> Bool
    modelExists        (ThmResult SMTResult
    r) = SMTResult -> Bool
    forall a. Modelable a => a -> Bool
    modelExists        SMTResult
    r
      getModelDictionary :: ThmResult -> Map [Char] CV
    getModelDictionary (ThmResult SMTResult
    r) = SMTResult -> Map [Char] CV
    forall a. Modelable a => a -> Map [Char] CV
    getModelDictionary SMTResult
    r
      getModelObjectives :: ThmResult -> Map [Char] GeneralizedCV
    getModelObjectives (ThmResult SMTResult
    r) = SMTResult -> Map [Char] GeneralizedCV
    forall a. Modelable a => a -> Map [Char] GeneralizedCV
    getModelObjectives SMTResult
    r
      getModelUIFuns :: ThmResult -> Map [Char] (SBVType, Either [Char] ([([CV], CV)], CV))
    getModelUIFuns     (ThmResult SMTResult
    r) = SMTResult -> Map [Char] (SBVType, Either [Char] ([([CV], CV)], CV))
    forall a.
    Modelable a =>
    a -> Map [Char] (SBVType, Either [Char] ([([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) = SMTResult -> Either [Char] (Bool, b)
    forall a b.
    (Modelable a, SatModel b) =>
    a -> Either [Char] (Bool, b)
    forall b. SatModel b => SMTResult -> Either [Char] (Bool, b)
    getModelAssignment SMTResult
    r
      modelExists :: SatResult -> Bool
    modelExists        (SatResult SMTResult
    r) = SMTResult -> Bool
    forall a. Modelable a => a -> Bool
    modelExists        SMTResult
    r
      getModelDictionary :: SatResult -> Map [Char] CV
    getModelDictionary (SatResult SMTResult
    r) = SMTResult -> Map [Char] CV
    forall a. Modelable a => a -> Map [Char] CV
    getModelDictionary SMTResult
    r
      getModelObjectives :: SatResult -> Map [Char] GeneralizedCV
    getModelObjectives (SatResult SMTResult
    r) = SMTResult -> Map [Char] GeneralizedCV
    forall a. Modelable a => a -> Map [Char] GeneralizedCV
    getModelObjectives SMTResult
    r
      getModelUIFuns :: SatResult -> Map [Char] (SBVType, Either [Char] ([([CV], CV)], CV))
    getModelUIFuns     (SatResult SMTResult
    r) = SMTResult -> Map [Char] (SBVType, Either [Char] ([([CV], CV)], CV))
    forall a.
    Modelable a =>
    a -> Map [Char] (SBVType, Either [Char] ([([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]]
    _  ) = [Char] -> Either [Char] (Bool, b)
    forall a b. a -> Either a b
    Left [Char]
    "SBV.getModelAssignment: Unsatisfiable result"
      getModelAssignment (Satisfiable   SMTConfig
    _   SMTModel
    m) = (Bool, b) -> Either [Char] (Bool, b)
    forall a b. b -> Either a b
    Right (Bool
    False, SMTModel -> b
    forall a. SatModel a => SMTModel -> a
    parseModelOut SMTModel
    m)
      getModelAssignment (DeltaSat      SMTConfig
    _ Maybe [Char]
    _ SMTModel
    m) = (Bool, b) -> Either [Char] (Bool, b)
    forall a b. b -> Either a b
    Right (Bool
    False, SMTModel -> b
    forall a. SatModel a => SMTModel -> a
    parseModelOut SMTModel
    m)
      getModelAssignment (SatExtField   SMTConfig
    _ SMTModel
    _  ) = [Char] -> Either [Char] (Bool, b)
    forall a b. a -> Either a b
    Left [Char]
    "SBV.getModelAssignment: The model is in an extension field"
      getModelAssignment (Unknown       SMTConfig
    _ SMTReasonUnknown
    m  ) = [Char] -> Either [Char] (Bool, b)
    forall a b. a -> Either a b
    Left ([Char] -> Either [Char] (Bool, b))
    -> [Char] -> Either [Char] (Bool, b)
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "SBV.getModelAssignment: Solver state is unknown: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SMTReasonUnknown -> [Char]
    forall a. Show a => a -> [Char]
    show SMTReasonUnknown
    m
      getModelAssignment (ProofError    SMTConfig
    _ [[Char]]
    s Maybe SMTResult
    _) = [Char] -> Either [Char] (Bool, b)
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> Either [Char] (Bool, b))
    -> [Char] -> Either [Char] (Bool, b)
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "SBV.getModelAssignment: Failed to produce a model: " [Char] -> [[Char]] -> [[Char]]
    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{}     = Map [Char] CV
    forall k a. Map k a
    M.empty
      getModelDictionary (Satisfiable SMTConfig
    _   SMTModel
    m) = [([Char], CV)] -> Map [Char] CV
    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) = [([Char], CV)] -> Map [Char] CV
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList (SMTModel -> [([Char], CV)]
    modelAssocs SMTModel
    m)
      getModelDictionary SatExtField{}       = Map [Char] CV
    forall k a. Map k a
    M.empty
      getModelDictionary Unknown{}           = Map [Char] CV
    forall k a. Map k a
    M.empty
      getModelDictionary ProofError{}        = Map [Char] CV
    forall k a. Map k a
    M.empty

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

      getModelUIFuns :: SMTResult -> Map [Char] (SBVType, Either [Char] ([([CV], CV)], CV))
    getModelUIFuns Unsatisfiable{}     = Map [Char] (SBVType, Either [Char] ([([CV], CV)], CV))
    forall k a. Map k a
    M.empty
      getModelUIFuns (Satisfiable SMTConfig
    _ SMTModel
    m  ) = [([Char], (SBVType, Either [Char] ([([CV], CV)], CV)))]
    -> Map [Char] (SBVType, Either [Char] ([([CV], CV)], CV))
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList (SMTModel -> [([Char], (SBVType, Either [Char] ([([CV], CV)], CV)))]
    modelUIFuns SMTModel
    m)
      getModelUIFuns (DeltaSat    SMTConfig
    _ Maybe [Char]
    _ SMTModel
    m) = [([Char], (SBVType, Either [Char] ([([CV], CV)], CV)))]
    -> Map [Char] (SBVType, Either [Char] ([([CV], CV)], CV))
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList (SMTModel -> [([Char], (SBVType, Either [Char] ([([CV], CV)], CV)))]
    modelUIFuns SMTModel
    m)
      getModelUIFuns (SatExtField SMTConfig
    _ SMTModel
    m  ) = [([Char], (SBVType, Either [Char] ([([CV], CV)], CV)))]
    -> Map [Char] (SBVType, Either [Char] ([([CV], CV)], CV))
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList (SMTModel -> [([Char], (SBVType, Either [Char] ([([CV], CV)], CV)))]
    modelUIFuns SMTModel
    m)
      getModelUIFuns Unknown{}           = Map [Char] (SBVType, Either [Char] ([([CV], CV)], CV))
    forall k a. Map k a
    M.empty
      getModelUIFuns ProofError{}        = Map [Char] (SBVType, Either [Char] ([([CV], CV)], CV))
    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 [CV] -> Maybe (a, [CV])
    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) -> [Char] -> a
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> a) -> [Char] -> a
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "SBV.parseModelOut: Partially constructed model; remaining elements: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [CV] -> [Char]
    forall a. Show a => a -> [Char]
    show [CV]
    ys
                       Maybe (a, [CV])
    Nothing      -> [Char] -> a
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> a) -> [Char] -> a
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "SBV.parseModelOut: Cannot construct a model from: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SMTModel -> [Char]
    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 = [Either [Char] (Bool, a)] -> [(Bool, a)]
    forall a b. [Either a b] -> [b]
    rights ((SMTResult -> Either [Char] (Bool, a))
    -> [SMTResult] -> [Either [Char] (Bool, a)]
    forall a b. (a -> b) -> [a] -> [b]
    map (SatResult -> Either [Char] (Bool, a)
    forall a b.
    (Modelable a, SatModel b) =>
    a -> Either [Char] (Bool, b)
    forall b. SatModel b => SatResult -> Either [Char] (Bool, b)
    getModelAssignment (SatResult -> Either [Char] (Bool, a))
    -> (SMTResult -> SatResult) -> SMTResult -> Either [Char] (Bool, a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SMTResult -> SatResult
    SatResult) [SMTResult]
    ms)
        [Int]
    inds <- ((Bool, a) -> Int -> IO Int) -> [(Bool, a)] -> [Int] -> IO [Int]
    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)..]
        Int -> IO Int
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Int -> IO Int) -> Int -> IO Int
    forall a b. (a -> b) -> a -> b
    $ [Int] -> Int
    forall a. HasCallStack => [a] -> a
    last (Int
    0Int -> [Int] -> [Int]
    forall 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 IO () -> IO Int -> IO Int
    forall a b. IO a -> IO b -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Int -> IO Int
    forall a. a -> IO a
    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 [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Maybe [[Char]] -> [Char]
    showUnsatCore Maybe [[Char]]
    uc
      Satisfiable SMTConfig
    _ (SMTModel [([Char], GeneralizedCV)]
    _ Maybe [(NamedSymVar, CV)]
    _ [] []) -> [Char]
    satMsg
      Satisfiable SMTConfig
    _   SMTModel
    m                  -> [Char]
    satMsgModel    [Char] -> ShowS
    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 [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SMTConfig -> SMTModel -> [Char]
    showModel SMTConfig
    cfg SMTModel
    m
      SatExtField SMTConfig
    _ (SMTModel [([Char], GeneralizedCV)]
    b Maybe [(NamedSymVar, CV)]
    _ [([Char], CV)]
    _ [([Char], (SBVType, Either [Char] ([([CV], CV)], CV)))]
    _)   -> [Char]
    satExtMsg   [Char] -> ShowS
    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 [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ".\n" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "  Reason: " [Char] -> ShowS
    `alignPlain` SMTReasonUnknown -> [Char]
    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" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    intercalate [Char]
    "\n" (ShowS -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char]
    "***  " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++) [[Char]]
    ls)
      ProofError  SMTConfig
    _ [[Char]]
    ls (Just SMTResult
    r)          -> [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    intercalate [Char]
    "\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $  [ [Char]
    "*** " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    l | [Char]
    l <- [[Char]]
    ls]
                                                             [[Char]] -> [[Char]] -> [[Char]]
    forall a. [a] -> [a] -> [a]
    ++ [ [Char]
    "***"
                                                                , [Char]
    "*** Alleged model:"
                                                                , [Char]
    "***"
                                                                ]
                                                             [[Char]] -> [[Char]] -> [[Char]]
    forall a. [a] -> [a] -> [a]
    ++ [[Char]
    "*** "  [Char] -> ShowS
    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" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    intercalate [Char]
    "\n" [[Char]
    "    " [Char] -> ShowS
    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
       | [([Char], (SBVType, Either [Char] ([([CV], CV)], CV)))] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [([Char], (SBVType, Either [Char] ([([CV], CV)], CV)))]
    uiFuncs
       = [Char]
    nonUIFuncs
       | Bool
    True
       = ShowS
    sep [Char]
    nonUIFuncs [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    intercalate [Char]
    "\n\n" ((([Char], (SBVType, Either [Char] ([([CV], CV)], CV))) -> [Char])
    -> [([Char], (SBVType, Either [Char] ([([CV], CV)], CV)))]
    -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map (SMTConfig
    -> ([Char], (SBVType, Either [Char] ([([CV], CV)], CV))) -> [Char]
    showModelUI SMTConfig
    cfg) [([Char], (SBVType, Either [Char] ([([CV], CV)], CV)))]
    uiFuncs)
       where nonUIFuncs :: [Char]
    nonUIFuncs = Bool -> Bool -> SMTConfig -> [([Char], GeneralizedCV)] -> [Char]
    showModelDictionary ([([Char], (SBVType, Either [Char] ([([CV], CV)], CV)))] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [([Char], (SBVType, Either [Char] ([([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, Either [Char] ([([CV], CV)], CV)))]
    uiFuncs    = SMTModel -> [([Char], (SBVType, Either [Char] ([([CV], CV)], CV)))]
    modelUIFuns SMTModel
    model
             sep :: ShowS
    sep [Char]
    ""     = [Char]
    ""
             sep [Char]
    x      = [Char]
    x [Char] -> ShowS
    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
       | [([Char], GeneralizedCV)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [([Char], GeneralizedCV)]
    allVars
       = ShowS
    forall {p}. IsString p => p -> p
    warn [Char]
    "[There are no variables bound by the model.]"
       | [([Char], GeneralizedCV)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [([Char], GeneralizedCV)]
    relevantVars
       = ShowS
    forall {p}. IsString p => p -> p
    warn [Char]
    "[There are no model-variables bound by the model.]"
       | Bool
    True
       = [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    intercalate [Char]
    "\n" ([[Char]] -> [Char])
    -> ([([Char], GeneralizedCV)] -> [[Char]])
    -> [([Char], GeneralizedCV)]
    -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [((Int, [Char]), (Int, [Char]))] -> [[Char]]
    display ([((Int, [Char]), (Int, [Char]))] -> [[Char]])
    -> ([([Char], GeneralizedCV)] -> [((Int, [Char]), (Int, [Char]))])
    -> [([Char], GeneralizedCV)]
    -> [[Char]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (([Char], GeneralizedCV) -> ((Int, [Char]), (Int, [Char])))
    -> [([Char], GeneralizedCV)] -> [((Int, [Char]), (Int, [Char]))]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char], GeneralizedCV) -> ((Int, [Char]), (Int, [Char]))
    forall {t :: * -> *} {a}.
    Foldable t =>
    (t a, GeneralizedCV) -> ((Int, t a), (Int, [Char]))
    shM ([([Char], GeneralizedCV)] -> [Char])
    -> [([Char], GeneralizedCV)] -> [Char]
    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  = (([Char], GeneralizedCV) -> Bool)
    -> [([Char], GeneralizedCV)] -> [([Char], GeneralizedCV)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool)
    -> (([Char], GeneralizedCV) -> Bool)
    -> ([Char], GeneralizedCV)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Char], GeneralizedCV) -> Bool
    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              = SMTConfig -> [Char] -> Bool
    mustIgnoreVar 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 ((t a -> Int
    forall a. t a -> Int
    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 = GeneralizedCV -> [Char]
    forall a. Show a => a -> [Char]
    show GeneralizedCV
    other in ((t a -> Int
    forall a. t a -> Int
    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   = (((Int, [Char]), (Int, [Char])) -> [Char])
    -> [((Int, [Char]), (Int, [Char]))] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Int, [Char]), (Int, [Char])) -> [Char]
    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]
    "  " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> ShowS
    right (Int
    nameWidth Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - [Char] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Char]
    s) [Char]
    s [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " = " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> ShowS
    left (Int
    valWidth Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - [Char] -> Int
    lTrimRight (ShowS
    valPart [Char]
    v)) [Char]
    v
                     nameWidth :: Int
    nameWidth             = [Int] -> Int
    forall a. Ord a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum ([Int] -> Int) -> [Int] -> Int
    forall a b. (a -> b) -> a -> b
    $ Int
    0 Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    : [Int
    l | ((Int
    l, [Char]
    _), (Int, [Char])
    _) <- [((Int, [Char]), (Int, [Char]))]
    svs]
                     valWidth :: Int
    valWidth              = [Int] -> Int
    forall a. Ord a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum ([Int] -> Int) -> [Int] -> Int
    forall a b. (a -> b) -> a -> b
    $ Int
    0 Int -> [Int] -> [Int]
    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 [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> Char -> [Char]
    forall a. Int -> a -> [a]
    replicate Int
    p Char
    ' '
            left :: Int -> ShowS
    left  Int
    p [Char]
    s = Int -> Char -> [Char]
    forall a. Int -> a -> [a]
    replicate Int
    p Char
    ' ' [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    s
            vlength :: [Char] -> Int
    vlength [Char]
    s = case (Char -> Bool) -> ShowS
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Char
    ':') (ShowS
    forall a. [a] -> [a]
    reverse ((Char -> Bool) -> ShowS
    forall a. (a -> Bool) -> [a] -> [a]
    takeWhile (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Char
    '\n') [Char]
    s)) of
                          (Char
    ':':Char
    ':':[Char]
    r) -> [Char] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length ((Char -> Bool) -> ShowS
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile Char -> Bool
    isSpace [Char]
    r)
                          [Char]
    _           -> [Char] -> Int
    forall a. [a] -> Int
    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 Char -> ShowS
    forall a. a -> [a] -> [a]
    : ShowS
    valPart [Char]
    xs

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

    -- | Show an uninterpreted function
    showModelUI :: SMTConfig -> (String, (SBVType, Either String ([([CV], CV)], CV))) -> String
    showModelUI :: SMTConfig
    -> ([Char], (SBVType, Either [Char] ([([CV], CV)], CV))) -> [Char]
    showModelUI SMTConfig
    cfg ([Char]
    nm, (SBVType [Kind]
    ts, Either [Char] ([([CV], CV)], CV)
    interp))
      = [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    intercalate [Char]
    "\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ case Either [Char] ([([CV], CV)], CV)
    interp of
                             Left  [Char]
    e  -> [[Char]
    "  " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    l | [Char]
    l <- [[Char]
    sig,  [Char]
    e]]
                             Right ([([CV], CV)], CV)
    ds -> [[Char]
    "  " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    l | [Char]
    l <- [Char]
    sig [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    : ([([CV], CV)], CV) -> [[Char]]
    mkBody ([([CV], CV)], CV)
    ds]
      where noOfArgs :: Int
    noOfArgs = [Kind] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Kind]
    ts Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1

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

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

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

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

                    align :: ([[Char]], [Char]) -> [Char]
    align ([[Char]]
    xs, [Char]
    r) = [[Char]] -> [Char]
    unwords ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ (Int -> ShowS) -> [Int] -> [[Char]] -> [[Char]]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Int -> ShowS
    left [Int]
    colWidths [[Char]]
    xs [[Char]] -> [[Char]] -> [[Char]]
    forall a. [a] -> [a] -> [a]
    ++ [[Char]
    "=", Int -> ShowS
    left Int
    resWidth [Char]
    r]
                       where left :: Int -> ShowS
    left Int
    i [Char]
    x = Int -> ShowS
    forall a. Int -> [a] -> [a]
    take Int
    i ([Char]
    x [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Char -> [Char]
    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 = Int -> CV -> [Char]
    forall {a}. (Eq a, Num a) => a -> CV -> [Char]
    sh (SMTConfig -> Int
    printBase SMTConfig
    cfg)
              where sh :: a -> CV -> [Char]
    sh a
    2  = CV -> [Char]
    forall a. PrettyNum a => a -> [Char]
    binP
                    sh a
    10 = Bool -> CV -> [Char]
    showCV Bool
    False
                    sh a
    16 = CV -> [Char]
    forall a. PrettyNum a => a -> [Char]
    hexP
                    sh a
    _  = CV -> [Char]
    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 [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    : (CV -> [Char]) -> [CV] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map (ShowS
    paren ShowS -> (CV -> [Char]) -> CV -> [Char]
    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
    '(' Char -> ShowS
    forall a. a -> [a] -> [a]
    : [Char]
    x [Char] -> ShowS
    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 :: SMTConfig -> Int
    printBase :: Int
    printBase, Bool
    crackNum :: Bool
    crackNum :: SMTConfig -> Bool
    crackNum} CV
    cv = ShowS
    cracked (Int -> CV -> [Char]
    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  = a -> [Char]
    forall a. PrettyNum a => a -> [Char]
    binS
            sh a
    10 = a -> [Char]
    forall a. Show a => a -> [Char]
    show
            sh a
    16 = a -> [Char]
    forall a. PrettyNum a => a -> [Char]
    hexS
            sh a
    n  = \a
    w -> a -> [Char]
    forall a. Show a => a -> [Char]
    show a
    w [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " -- Ignoring unsupported printBase " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> [Char]
    forall a. Show a => a -> [Char]
    show a
    n [Char] -> ShowS
    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 CV -> Maybe [Char]
    forall a. CrackNum a => a -> Maybe [Char]
    CN.crackNum CV
    cv of
                                 Maybe [Char]
    Nothing -> [Char]
    def
                                 Just [Char]
    cs -> [Char]
    def [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\n" [Char] -> ShowS
    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      -> [Char] -> IO a
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> IO a) -> [Char] -> IO a
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines [ [Char]
    "Unable to locate executable for " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Solver -> [Char]
    forall a. Show a => a -> [Char]
    show (SMTSolver -> Solver
    name (SMTConfig -> SMTSolver
    solver SMTConfig
    cfg))
                                          , [Char]
    "Executable specified: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> [Char]
    show [Char]
    execName
                                          ]

          Just [Char]
    execPath -> SMTConfig
    -> State -> [Char] -> [[Char]] -> [Char] -> (State -> IO a) -> IO a
    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
                           IO a -> [Handler a] -> IO a
    forall a. IO a -> [Handler a] -> IO a
    `C.catches`
                            [ (SBVException -> IO a) -> Handler a
    forall a e. Exception e => (e -> IO a) -> Handler a
    C.Handler (\(SBVException
    e :: SBVException)    -> SBVException -> IO a
    forall e a. Exception e => e -> IO a
    C.throwIO SBVException
    e)
                            , (ErrorCall -> IO a) -> Handler a
    forall a e. Exception e => (e -> IO a) -> Handler a
    C.Handler (\(ErrorCall
    e :: C.ErrorCall)     -> ErrorCall -> IO a
    forall e a. Exception e => e -> IO a
    C.throwIO ErrorCall
    e)
                            , (SomeException -> IO a) -> Handler a
    forall a e. Exception e => (e -> IO a) -> Handler a
    C.Handler (\(SomeException
    e :: C.SomeException) -> SomeException -> IO a -> IO a
    forall a. SomeException -> IO a -> IO a
    handleAsync SomeException
    e (IO a -> IO a) -> IO a -> IO a
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO a
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> IO a) -> [Char] -> IO a
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines [ [Char]
    "Failed to start the external solver:\n" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SomeException -> [Char]
    forall a. Show a => a -> [Char]
    show SomeException
    e
                                                                                                    , [Char]
    "Make sure you can start " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    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     IO [Char] -> (SomeException -> IO [Char]) -> IO [Char]
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `C.catch` (\(SomeException
    e :: C.SomeException) -> SomeException -> IO [Char] -> IO [Char]
    forall a. SomeException -> IO a -> IO a
    handleAsync SomeException
    e ([Char] -> IO [Char]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SMTSolver -> [Char]
    executable (SMTConfig -> SMTSolver
    solver SMTConfig
    cfg))))
        [[Char]]
    execOpts <- ([Char] -> [[Char]]
    splitArgs ([Char] -> [[Char]]) -> IO [Char] -> IO [[Char]]
    forall a b. (a -> b) -> IO a -> IO b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap`  [Char] -> IO [Char]
    getEnv [Char]
    envOptName) IO [[Char]] -> (SomeException -> IO [[Char]]) -> IO [[Char]]
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `C.catch` (\(SomeException
    e :: C.SomeException) -> SomeException -> IO [[Char]] -> IO [[Char]]
    forall a. SomeException -> IO a -> IO a
    handleAsync SomeException
    e ([[Char]] -> IO [[Char]]
    forall a. a -> IO a
    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 = (solver cfg) {executable = execName, options = const execOpts}}

        SMTConfig -> State -> [Char] -> (State -> IO res) -> IO res
    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    = SMTConfig -> [[Char]] -> m ()
    forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
    debug SMTConfig
    config [[Char]
    "** " [Char] -> ShowS
    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 [[Char]] -> [[Char]] -> [[Char]]
    forall a. [a] -> [a] -> [a]
    ++ SMTConfig -> [[Char]]
    extraArgs SMTConfig
    config
        [Char] -> IO ()
    forall {m :: * -> *}. MonadIO m => [Char] -> m ()
    msg ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Calling: "  [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ([Char]
    exec [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (if [[Char]] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [[Char]]
    opts then [Char]
    "" else [Char]
    " ") [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [[Char]] -> [Char]
    joinArgs [[Char]]
    opts)
        [Char] -> ()
    forall a. NFData a => a -> ()
    rnf [Char]
    pgm () -> IO a -> IO a
    forall a b. a -> b -> b
    `seq` SMTConfig
    -> State -> [Char] -> [[Char]] -> [Char] -> (State -> IO a) -> IO a
    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  = Solver -> [Char]
    forall a. Show a => a -> [Char]
    show (SMTSolver -> Solver
    name (SMTConfig -> SMTSolver
    solver SMTConfig
    cfg))
              msg :: [[Char]] -> IO ()
    msg = SMTConfig -> [[Char]] -> IO ()
    forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
    debug SMTConfig
    cfg ([[Char]] -> IO ()) -> ([[Char]] -> [[Char]]) -> [[Char]] -> IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ShowS -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char]
    "*** " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++)

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

              -- the very first command we send
              heartbeat :: [Char]
    heartbeat = [Char]
    "(set-option :print-success true)"

          (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 Maybe [Char]
    forall a. Maybe a
    Nothing Maybe [([Char], [Char])]
    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) (Either ([Char], Maybe Int) [Char] -> IO ())
    -> Either ([Char], Maybe Int) [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ ([Char], Maybe Int) -> Either ([Char], Maybe Int) [Char]
    forall a b. a -> Either a b
    Left ([Char]
    command, Maybe Int
    mbTimeOut)

                        -- is this a set-command? Then we expect faster response; except for the heartbeat
                        isSetCommand :: Maybe [Char] -> Bool
    isSetCommand = Bool -> ([Char] -> Bool) -> Maybe [Char] -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    False [Char] -> Bool
    chk
                          where chk :: [Char] -> Bool
    chk [Char]
    cmd = [Char]
    cmd [Char] -> [Char] -> Bool
    forall a. Eq a => a -> a -> Bool
    /= [Char]
    heartbeat Bool -> Bool -> Bool
    && [Char]
    "(set-option :" [Char] -> [Char] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isPrefixOf` [Char]
    cmd

                        -- 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
    mbTimeOutGiven [Char]
    command =
                                      let -- If the command is a set-option call, make sure there's a timeout on it
                                          -- This ensures that if we try to set an option before diagnostic-output
                                          -- is redirected to stdout and the solver chokes, then we can catch it
                                          mbTimeOut :: Maybe Int
    mbTimeOut | Maybe [Char] -> Bool
    isSetCommand ([Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    command) = Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    1000000
                                                    | Bool
    True                        = Maybe Int
    mbTimeOutGiven

                                          -- 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
                                          cmd :: [Char]
    cmd = (Char -> Bool) -> ShowS
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile Char -> Bool
    isSpace [Char]
    command

                                      in if [Char] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Char]
    cmd Bool -> Bool -> Bool
    || [Char]
    ";" [Char] -> [Char] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isPrefixOf` [Char]
    cmd
                                         then [Char] -> IO [Char]
    forall a. a -> IO a
    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 ([Char] -> Maybe [Char]
    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 = [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    intercalate [Char]
    "\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [[Char]]
    forall a. [a] -> [a]
    reverse [[Char]]
    response
                                    Maybe [Char] -> Either ([Char], Maybe Int) [Char] -> IO ()
    recordTranscript (SMTConfig -> Maybe [Char]
    transcript SMTConfig
    cfg) (Either ([Char], Maybe Int) [Char] -> IO ())
    -> Either ([Char], Maybe Int) [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Either ([Char], Maybe Int) [Char]
    forall a b. b -> Either a b
    Right [Char]
    collated
                                    [Char] -> IO [Char]
    forall a. a -> IO a
    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 | Maybe [Char] -> Bool
    isSetCommand Maybe [Char]
    mbCommand = Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    1000000
                                                              | Bool
    isFirst                = Maybe Int
    mbTimeOut
                                                              | Bool
    True                   = Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    5000000
                                                 timeOutMsg :: Int -> [Char]
    timeOutMsg Int
    t | Bool
    isFirst = [Char]
    "User specified timeout of " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    showTimeoutValue Int
    t [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " exceeded"
                                                              | Bool
    True    = [Char]
    "A multiline complete response wasn't received before " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    showTimeoutValue Int
    t [Char] -> ShowS
    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 = [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    intercalate [Char]
    "\n" ([[Char]] -> [Char])
    -> ([[Char]] -> [[Char]]) -> [[Char]] -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [[Char]] -> [[Char]]
    forall a. [a] -> [a]
    reverse ([[Char]] -> [Char]) -> IO [[Char]] -> IO [Char]
    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 [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    : [[Char]]
    sofar

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

                                                 -- Carefully grab things as they are ready. But don't block!
                                                 collectH :: Handle -> IO [Char]
    collectH Handle
    handle = ShowS
    forall a. [a] -> [a]
    reverse ShowS -> IO [Char] -> IO [Char]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Char] -> IO [Char]
    coll [Char]
    ""
                                                   where coll :: [Char] -> IO [Char]
    coll [Char]
    sofar = do Bool
    b <- Handle -> IO Bool
    hReady Handle
    handle
                                                                         if Bool
    b
                                                                            then Handle -> IO Char
    hGetChar Handle
    handle IO Char -> (Char -> IO [Char]) -> IO [Char]
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \Char
    c -> [Char] -> IO [Char]
    coll (Char
    cChar -> ShowS
    forall a. a -> [a] -> [a]
    :[Char]
    sofar)
                                                                            else [Char] -> IO [Char]
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [Char]
    sofar

                                                 -- grab the contents of a handle, and return it trimmed if any
                                                 grab :: Handle -> IO (Maybe [Char])
    grab Handle
    handle = do Maybe [Char]
    mbCts <- ([Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just ([Char] -> Maybe [Char]) -> IO [Char] -> IO (Maybe [Char])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Handle -> IO [Char]
    collectH Handle
    handle) IO (Maybe [Char])
    -> (SomeException -> IO (Maybe [Char])) -> IO (Maybe [Char])
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `C.catch` (\(SomeException
    _ :: C.SomeException) -> Maybe [Char] -> IO (Maybe [Char])
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe [Char]
    forall a. Maybe a
    Nothing)
                                                                  Maybe [Char] -> IO (Maybe [Char])
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Maybe [Char] -> IO (Maybe [Char]))
    -> Maybe [Char] -> IO (Maybe [Char])
    forall a b. (a -> b) -> a -> b
    $ (Char -> Bool) -> ShowS
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile Char -> Bool
    isSpace ShowS -> Maybe [Char] -> Maybe [Char]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe [Char]
    mbCts

                                             in case Maybe Int
    timeOutToUse of
                                                  Maybe Int
    Nothing -> [Char] -> SolverLine
    SolverRegular ([Char] -> SolverLine) -> IO [Char] -> IO SolverLine
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO [Char]
    getFullLine
                                                  Just Int
    t  -> do Maybe [Char]
    r <- Int -> IO [Char] -> IO (Maybe [Char])
    forall a. Int -> IO a -> IO (Maybe a)
    Timeout.timeout Int
    t IO [Char]
    getFullLine
                                                                case Maybe [Char]
    r of
                                                                  Just [Char]
    l  -> SolverLine -> IO SolverLine
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SolverLine -> IO SolverLine) -> SolverLine -> IO SolverLine
    forall a b. (a -> b) -> a -> b
    $ [Char] -> SolverLine
    SolverRegular [Char]
    l
                                                                  Maybe [Char]
    Nothing -> do Maybe [Char]
    out <- Handle -> IO (Maybe [Char])
    grab Handle
    outh
                                                                                Maybe [Char]
    err <- Handle -> IO (Maybe [Char])
    grab Handle
    errh
                                                                                -- in this case, if we have something on out/err pass that back as regular
                                                                                case Maybe [Char]
    err Maybe [Char] -> Maybe [Char] -> Maybe [Char]
    forall a. Maybe a -> Maybe a -> Maybe a
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    `mplus` Maybe [Char]
    out of
                                                                                  Just [Char]
    x | Bool -> Bool
    not ([Char] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Char]
    x) -> SolverLine -> IO SolverLine
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SolverLine -> IO SolverLine) -> SolverLine -> IO SolverLine
    forall a b. (a -> b) -> a -> b
    $ [Char] -> SolverLine
    SolverRegular [Char]
    x
                                                                                  Maybe [Char]
    _                     -> SolverLine -> IO SolverLine
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SolverLine -> IO SolverLine) -> SolverLine -> IO SolverLine
    forall a b. (a -> b) -> a -> b
    $ [Char] -> SolverLine
    SolverTimeout (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 IO SolverLine -> (SomeException -> IO SolverLine) -> IO SolverLine
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `C.catch` (\(SomeException
    e :: C.SomeException) -> SomeException -> IO SolverLine -> IO SolverLine
    forall a. SomeException -> IO a -> IO a
    handleAsync SomeException
    e (SolverLine -> IO SolverLine
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Char] -> SolverLine
    SolverException (SomeException -> [Char]
    forall a. Show a => a -> [Char]
    show SomeException
    e))))
                                                case SolverLine
    errln of
                                                  SolverRegular [Char]
    ln -> let need :: Int
    need  = Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + [Char] -> Int
    parenDeficit [Char]
    ln
                                                                          -- make sure we get *something*
                                                                          empty :: Bool
    empty = case (Char -> Bool) -> ShowS
    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 Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    0) of
                                                                            (Bool
    True, Bool
    _)      -> do SMTConfig -> [[Char]] -> IO ()
    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]
    ln[Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    :[[Char]]
    sofar)
                                                                            (Bool
    False, Bool
    True)  -> [[Char]] -> IO [[Char]]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Char]
    ln[Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    :[[Char]]
    sofar)

                                                  SolverException [Char]
    e -> do ProcessHandle -> IO ()
    terminateProcess ProcessHandle
    pid
                                                                          SBVException -> IO [[Char]]
    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    = Maybe [Char]
    forall a. Maybe a
    Nothing
                                                                                                 , sbvExceptionReceived :: Maybe [Char]
    sbvExceptionReceived    = [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just ([Char] -> Maybe [Char]) -> [Char] -> Maybe [Char]
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines ([[Char]] -> [[Char]]
    forall a. [a] -> [a]
    reverse [[Char]]
    sofar)
                                                                                                 , sbvExceptionStdOut :: Maybe [Char]
    sbvExceptionStdOut      = Maybe [Char]
    forall a. Maybe a
    Nothing
                                                                                                 , sbvExceptionStdErr :: Maybe [Char]
    sbvExceptionStdErr      = Maybe [Char]
    forall a. Maybe a
    Nothing
                                                                                                 , sbvExceptionExitCode :: Maybe ExitCode
    sbvExceptionExitCode    = Maybe ExitCode
    forall a. Maybe a
    Nothing
                                                                                                 , sbvExceptionConfig :: SMTConfig
    sbvExceptionConfig      = SMTConfig
    cfg { solver = (solver cfg) { executable = execPath } }
                                                                                                 , sbvExceptionReason :: Maybe [[Char]]
    sbvExceptionReason      = Maybe [[Char]]
    forall a. Maybe a
    Nothing
                                                                                                 , sbvExceptionHint :: Maybe [[Char]]
    sbvExceptionHint        = if [Char]
    "hGetLine: end of file" [Char] -> [Char] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isInfixOf` [Char]
    e
                                                                                                                             then [[Char]] -> Maybe [[Char]]
    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 Maybe [[Char]]
    forall a. Maybe a
    Nothing
                                                                                                 }

                                                  SolverTimeout [Char]
    e -> do ProcessHandle -> IO ()
    terminateProcess ProcessHandle
    pid -- NB. Do not *wait* for the process, just quit.

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

                        terminateSolver :: IO ([Char], [Char], ExitCode)
    terminateSolver = do Handle -> IO ()
    hClose Handle
    inh
                                             MVar ()
    outMVar <- IO (MVar ())
    forall a. IO (MVar a)
    newEmptyMVar
                                             [Char]
    out <- Handle -> IO [Char]
    hGetContents Handle
    outh IO [Char] -> (SomeException -> IO [Char]) -> IO [Char]
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `C.catch`  (\(SomeException
    e :: C.SomeException) -> SomeException -> IO [Char] -> IO [Char]
    forall a. SomeException -> IO a -> IO a
    handleAsync SomeException
    e ([Char] -> IO [Char]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SomeException -> [Char]
    forall a. Show a => a -> [Char]
    show SomeException
    e)))
                                             ThreadId
    _ <- IO () -> IO ThreadId
    forkIO (IO () -> IO ThreadId) -> IO () -> IO ThreadId
    forall a b. (a -> b) -> a -> b
    $ Int -> IO Int
    forall a. a -> IO a
    C.evaluate ([Char] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Char]
    out) IO Int -> IO () -> IO ()
    forall a b. IO a -> IO b -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> MVar () -> () -> IO ()
    forall a. MVar a -> a -> IO ()
    putMVar MVar ()
    outMVar ()
                                             [Char]
    err <- Handle -> IO [Char]
    hGetContents Handle
    errh IO [Char] -> (SomeException -> IO [Char]) -> IO [Char]
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `C.catch`  (\(SomeException
    e :: C.SomeException) -> SomeException -> IO [Char] -> IO [Char]
    forall a. SomeException -> IO a -> IO a
    handleAsync SomeException
    e ([Char] -> IO [Char]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SomeException -> [Char]
    forall a. Show a => a -> [Char]
    show SomeException
    e)))
                                             ThreadId
    _ <- IO () -> IO ThreadId
    forkIO (IO () -> IO ThreadId) -> IO () -> IO ThreadId
    forall a b. (a -> b) -> a -> b
    $ Int -> IO Int
    forall a. a -> IO a
    C.evaluate ([Char] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Char]
    err) IO Int -> IO () -> IO ()
    forall a b. IO a -> IO b -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> MVar () -> () -> IO ()
    forall a. MVar a -> a -> IO ()
    putMVar MVar ()
    outMVar ()
                                             MVar () -> IO ()
    forall a. MVar a -> IO a
    takeMVar MVar ()
    outMVar
                                             MVar () -> IO ()
    forall a. MVar a -> IO a
    takeMVar MVar ()
    outMVar
                                             Handle -> IO ()
    hClose Handle
    outh IO () -> (SomeException -> IO ()) -> IO ()
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `C.catch`  (\(SomeException
    e :: C.SomeException) -> SomeException -> IO () -> IO ()
    forall a. SomeException -> IO a -> IO a
    handleAsync SomeException
    e (() -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()))
                                             Handle -> IO ()
    hClose Handle
    errh IO () -> (SomeException -> IO ()) -> IO ()
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `C.catch`  (\(SomeException
    e :: C.SomeException) -> SomeException -> IO () -> IO ()
    forall a. SomeException -> IO a -> IO a
    handleAsync SomeException
    e (() -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()))
                                             ExitCode
    ex <- ProcessHandle -> IO ExitCode
    waitForProcess ProcessHandle
    pid IO ExitCode -> (SomeException -> IO ExitCode) -> IO ExitCode
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `C.catch` (\(SomeException
    e :: C.SomeException) -> SomeException -> IO ExitCode -> IO ExitCode
    forall a. SomeException -> IO a -> IO a
    handleAsync SomeException
    e (ExitCode -> IO ExitCode
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Int -> ExitCode
    ExitFailure (-Int
    999))))
                                             ([Char], [Char], ExitCode) -> IO ([Char], [Char], ExitCode)
    forall a. a -> IO a
    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 ([[Char]] -> IO ()) -> [[Char]] -> IO ()
    forall a b. (a -> b) -> a -> b
    $   [ [Char]
    "Solver   : " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    nm
                                       , [Char]
    "Exit code: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ExitCode -> [Char]
    forall a. Show a => a -> [Char]
    show ExitCode
    ex
                                       ]
                                    [[Char]] -> [[Char]] -> [[Char]]
    forall a. [a] -> [a] -> [a]
    ++ [ [Char]
    "Std-out  : " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    intercalate [Char]
    "\n           " ([Char] -> [[Char]]
    lines [Char]
    out) | Bool -> Bool
    not ([Char] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Char]
    out)]
                                    [[Char]] -> [[Char]] -> [[Char]]
    forall a. [a] -> [a] -> [a]
    ++ [ [Char]
    "Std-err  : " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    intercalate [Char]
    "\n           " ([Char] -> [[Char]]
    lines [Char]
    err) | Bool -> Bool
    not ([Char] -> Bool
    forall a. [a] -> Bool
    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 -> () -> IO ()
    forall a. a -> IO a
    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 " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ExitCode -> [Char]
    forall a. Show a => a -> [Char]
    show ExitCode
    ex [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " per user request!"]
                                                   else SBVException -> IO ()
    forall e a. Exception e => e -> IO a
    C.throwIO SBVException { sbvExceptionDescription :: [Char]
    sbvExceptionDescription = [Char]
    "Failed to complete the call to " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    nm
                                                                               , sbvExceptionSent :: Maybe [Char]
    sbvExceptionSent        = Maybe [Char]
    forall a. Maybe a
    Nothing
                                                                               , sbvExceptionExpected :: Maybe [Char]
    sbvExceptionExpected    = Maybe [Char]
    forall a. Maybe a
    Nothing
                                                                               , sbvExceptionReceived :: Maybe [Char]
    sbvExceptionReceived    = Maybe [Char]
    forall a. Maybe a
    Nothing
                                                                               , sbvExceptionStdOut :: Maybe [Char]
    sbvExceptionStdOut      = [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    out
                                                                               , sbvExceptionStdErr :: Maybe [Char]
    sbvExceptionStdErr      = [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    err
                                                                               , sbvExceptionExitCode :: Maybe ExitCode
    sbvExceptionExitCode    = ExitCode -> Maybe ExitCode
    forall a. a -> Maybe a
    Just ExitCode
    ex
                                                                               , sbvExceptionConfig :: SMTConfig
    sbvExceptionConfig      = SMTConfig
    cfg { solver = (solver cfg) { executable = execPath } }
                                                                               , sbvExceptionReason :: Maybe [[Char]]
    sbvExceptionReason      = Maybe [[Char]]
    forall a. Maybe a
    Nothing
                                                                               , sbvExceptionHint :: Maybe [[Char]]
    sbvExceptionHint        = if Bool -> Bool
    not (SMTConfig -> Bool
    verbose SMTConfig
    cfg)
                                                                                                           then [[Char]] -> Maybe [[Char]]
    forall a. a -> Maybe a
    Just [[Char]
    "Run with 'verbose=True' for further information"]
                                                                                                           else Maybe [[Char]]
    forall a. Maybe a
    Nothing
                                                                               }

                    (Maybe Int -> [Char] -> IO (), Maybe Int -> [Char] -> IO [Char],
     Maybe [Char] -> Maybe Int -> IO [Char],
     IO ([Char], [Char], ExitCode), IO (), ProcessHandle)
    -> IO
         (Maybe Int -> [Char] -> IO (), Maybe Int -> [Char] -> IO [Char],
          Maybe [Char] -> Maybe Int -> IO [Char],
          IO ([Char], [Char], ExitCode), IO (), ProcessHandle)
    forall a. a -> IO a
    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
                                            SMTConfig -> [[Char]] -> IO ()
    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"] -> SMTConfig -> [[Char]] -> IO ()
    forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
    debug SMTConfig
    cfg [[Char]
    "[GOOD] " [Char] -> ShowS
    `alignPlain` [Char]
    l]
                                              [[Char]]
    _           -> do SMTConfig -> [[Char]] -> IO ()
    forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
    debug SMTConfig
    cfg [[Char]
    "[FAIL] " [Char] -> ShowS
    `alignPlain` [Char]
    l]

                                                                let isOption :: Bool
    isOption = [Char]
    "(set-option" [Char] -> [Char] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isPrefixOf` (Char -> Bool) -> ShowS
    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 <- ([Char] -> Either [Char] [Char]
    forall a b. b -> Either a b
    Right ([Char] -> Either [Char] [Char])
    -> IO [Char] -> IO (Either [Char] [Char])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe [Char] -> Maybe Int -> IO [Char]
    getResponseFromSolver Maybe [Char]
    forall a. Maybe a
    Nothing (Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    5000000))
                                                                            IO (Either [Char] [Char])
    -> (SomeException -> IO (Either [Char] [Char]))
    -> IO (Either [Char] [Char])
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `C.catch` (\(SomeException
    e :: C.SomeException) -> SomeException
    -> IO (Either [Char] [Char]) -> IO (Either [Char] [Char])
    forall a. SomeException -> IO a -> IO a
    handleAsync SomeException
    e (Either [Char] [Char] -> IO (Either [Char] [Char])
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Char] -> Either [Char] [Char]
    forall a b. a -> Either a b
    Left (SomeException -> [Char]
    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 = [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    intercalate [Char]
    "\n" ([[Char]] -> [Char]) -> ([Char] -> [[Char]]) -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> [[Char]]
    lines ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ [Char]
    outOrig
                                                                    err :: [Char]
    err = [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    intercalate [Char]
    "\n" ([[Char]] -> [Char]) -> ([Char] -> [[Char]]) -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> [[Char]]
    lines ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ [Char]
    errOrig

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

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

                                 -- Mark in the log, mostly.
                                 Maybe Int -> [Char] -> IO ()
    sendAndGetSuccess Maybe Int
    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 (SMTSolver -> Solver) -> SMTSolver -> Solver
    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 SMTConfig -> [[Char]] -> IO ()
    forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
    debug SMTConfig
    cfg [[Char]
    "** Skipping heart-beat for the solver " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Solver -> [Char]
    forall a. Show a => a -> [Char]
    show Solver
    backend]
                                    else do [Char]
    r <- Maybe Int -> [Char] -> IO [Char]
    ask (Int -> Maybe Int
    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"]     -> SMTConfig -> [[Char]] -> IO ()
    forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
    debug SMTConfig
    cfg [[Char]
    "[GOOD] " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    heartbeat]
                                              [[Char]
    "unsupported"] -> [Char] -> IO ()
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines [ [Char]
    ""
                                                                                 , [Char]
    "*** Backend solver (" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++  Solver -> [Char]
    forall a. Show a => a -> [Char]
    show Solver
    backend [Char] -> ShowS
    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]]
    _               -> [Char] -> IO ()
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines [ [Char]
    ""
                                                                                 , [Char]
    "*** Data.SBV: Failed to initiate contact with the solver!"
                                                                                 , [Char]
    "***"
                                                                                 , [Char]
    "***   Sent    : " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    heartbeat
                                                                                 , [Char]
    "***   Expected: success"
                                                                                 , [Char]
    "***   Received: " [Char] -> ShowS
    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 SMTConfig -> [[Char]] -> IO ()
    forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
    debug SMTConfig
    cfg [ [Char]
    "** Backend solver " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Solver -> [Char]
    forall a. Show a => a -> [Char]
    show Solver
    backend [Char] -> ShowS
    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 Maybe Int
    forall a. Maybe a
    Nothing [Char]
    "(set-option :global-declarations true)"

                                 -- Now dump the program!
                                 ([Char] -> IO ()) -> [[Char]] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Maybe Int -> [Char] -> IO ()
    sendAndGetSuccess Maybe Int
    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 Maybe [Char]
    forall a. Maybe a
    Nothing
                                                     , queryConfig :: SMTConfig
    queryConfig              = SMTConfig
    cfg
                                                     , queryTerminate :: IO ()
    queryTerminate           = IO ()
    cleanUp
                                                     , queryTimeOutValue :: Maybe Int
    queryTimeOutValue        = Maybe Int
    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 <- IORef (Maybe QueryState) -> IO (Maybe QueryState)
    forall a. IORef a -> IO a
    readIORef IORef (Maybe QueryState)
    qsp

                                 case Maybe QueryState
    mbQS of
                                   Maybe QueryState
    Nothing -> IORef (Maybe QueryState) -> Maybe QueryState -> IO ()
    forall a. IORef a -> a -> IO ()
    writeIORef IORef (Maybe QueryState)
    qsp (QueryState -> Maybe QueryState
    forall a. a -> Maybe a
    Just QueryState
    qs)
                                   Just QueryState
    _  -> [Char] -> IO ()
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> IO ()) -> [Char] -> IO ()
    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 IO a -> (SomeException -> IO a) -> IO a
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `C.catch` (\(SomeException
    e :: C.SomeException) -> SomeException -> IO a -> IO a
    forall a. SomeException -> IO a -> IO a
    handleAsync SomeException
    e (IO a -> IO a) -> IO a -> IO a
    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) (SomeException -> [Char]
    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
                                                                                SomeException -> IO a
    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 :: Timing
    timing :: SMTConfig -> Timing
    timing} State
    state = case Timing
    timing of
                                               Timing
    NoTiming        -> () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                                               Timing
    PrintTiming     -> do NominalDiffTime
    e <- IO NominalDiffTime
    elapsed
                                                                     [Char] -> IO ()
    putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "*** SBV: Elapsed time: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ NominalDiffTime -> [Char]
    showTDiff NominalDiffTime
    e
                                               SaveTiming IORef NominalDiffTime
    here -> IORef NominalDiffTime -> NominalDiffTime -> IO ()
    forall a. IORef a -> a -> IO ()
    writeIORef IORef NominalDiffTime
    here (NominalDiffTime -> IO ()) -> IO NominalDiffTime -> IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< IO NominalDiffTime
    elapsed
      where elapsed :: IO NominalDiffTime
    elapsed = IO UTCTime
    getCurrentTime IO UTCTime -> (UTCTime -> IO NominalDiffTime) -> IO NominalDiffTime
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \UTCTime
    end -> NominalDiffTime -> IO NominalDiffTime
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NominalDiffTime -> IO NominalDiffTime)
    -> NominalDiffTime -> IO NominalDiffTime
    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
    _   = () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    startTranscript (Just [Char]
    f) SMTConfig
    cfg = do [Char]
    ts <- ZonedTime -> [Char]
    forall a. Show a => a -> [Char]
    show (ZonedTime -> [Char]) -> IO ZonedTime -> IO [Char]
    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 ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Maybe [Char] -> [Char]
    start [Char]
    ts Maybe [Char]
    mbExecPath
      where SMTSolver{Solver
    name :: SMTSolver -> Solver
    name :: Solver
    name, SMTConfig -> [[Char]]
    options :: SMTSolver -> SMTConfig -> [[Char]]
    options :: 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 " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ts
                                      , [Char]
    ";;;"
                                      , [Char]
    ";;;           Solver    : " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Solver -> [Char]
    forall a. Show a => a -> [Char]
    show Solver
    name
                                      , [Char]
    ";;;           Executable: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> Maybe [Char] -> [Char]
    forall a. a -> Maybe a -> a
    fromMaybe [Char]
    "Unable to locate the executable" Maybe [Char]
    mbPath
                                      , [Char]
    ";;;           Options   : " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [[Char]] -> [Char]
    unwords (SMTConfig -> [[Char]]
    options SMTConfig
    cfg [[Char]] -> [[Char]] -> [[Char]]
    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
    _  = () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    finalizeTranscript (Just [Char]
    f) ExitCode
    ec = do [Char]
    ts <- ZonedTime -> [Char]
    forall a. Show a => a -> [Char]
    show (ZonedTime -> [Char]) -> IO ZonedTime -> IO [Char]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO ZonedTime
    getZonedTime
                                        [Char] -> [Char] -> IO ()
    appendFile [Char]
    f ([Char] -> IO ()) -> [Char] -> IO ()
    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 " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ts
                             , [Char]
    ";;;"
                             , [Char]
    ";;; Exit code: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ExitCode -> [Char]
    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]
    _ = () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    recordTranscript (Just [Char]
    f) Either ([Char], Maybe Int) [Char]
    m = do [Char]
    tsPre <- TimeLocale -> [Char] -> ZonedTime -> [Char]
    forall t. FormatTime t => TimeLocale -> [Char] -> t -> [Char]
    formatTime TimeLocale
    defaultTimeLocale [Char]
    "; [%T%Q" (ZonedTime -> [Char]) -> IO ZonedTime -> IO [Char]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO ZonedTime
    getZonedTime
                                     let ts :: [Char]
    ts = Int -> ShowS
    forall a. Int -> [a] -> [a]
    take Int
    15 ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ [Char]
    tsPre [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Char -> [Char]
    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 ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ ([Char]
    ts [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "] " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Maybe Int -> [Char]
    to Maybe Int
    mbTimeOut [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "Sending:") [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    : [Char] -> [[Char]]
    lines [Char]
    sent
                                       Right [Char]
    recv              -> [Char] -> [Char] -> IO ()
    appendFile [Char]
    f ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ case [Char] -> [[Char]]
    lines ((Char -> Bool) -> ShowS
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile Char -> Bool
    isSpace [Char]
    recv) of
                                                                                            []  -> [[Char]
    ts [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "] Received: <NO RESPONSE>"]  -- can't really happen.
                                                                                            [[Char]
    x] -> [[Char]
    ts [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "] Received: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    x]
                                                                                            [[Char]]
    xs  -> ([Char]
    ts [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "] Received: ") [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    : ShowS -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char]
    ";   " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++) [[Char]]
    xs
            where to :: Maybe Int -> [Char]
    to Maybe Int
    Nothing  = [Char]
    ""
                  to (Just Int
    i) = [Char]
    "[Timeout: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    showTimeoutValue Int
    i [Char] -> ShowS
    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]
    _ = () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    recordException (Just [Char]
    f) [Char]
    m = do [Char]
    ts <- ZonedTime -> [Char]
    forall a. Show a => a -> [Char]
    show (ZonedTime -> [Char]) -> IO ZonedTime -> IO [Char]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO ZonedTime
    getZonedTime
                                    [Char] -> [Char] -> IO ()
    appendFile [Char]
    f ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ ShowS
    exc [Char]
    ts
      where exc :: ShowS
    exc [Char]
    ts = [[Char]] -> [Char]
    unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ [ [Char]
    ""
                               , [Char]
    ";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                               , [Char]
    ";;;"
                               , [Char]
    ";;; SBV: Caught an exception at " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ts
                               , [Char]
    ";;;"
                               ]
                            [[Char]] -> [[Char]] -> [[Char]]
    forall a. [a] -> [a] -> [a]
    ++ [ [Char]
    ";;;   " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    l | [Char]
    l <- ([Char] -> Bool) -> [[Char]] -> [[Char]]
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile [Char] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null ([Char] -> [[Char]]
    lines [Char]
    m) ]
                            [[Char]] -> [[Char]] -> [[Char]]
    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 = SomeException -> IO a
    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 = Maybe AsyncException -> Bool
    forall a. Maybe a -> Bool
    isJust (SomeException -> Maybe AsyncException
    forall e. Exception e => SomeException -> Maybe e
    C.fromException SomeException
    e :: Maybe C.AsyncException) Bool -> Bool -> Bool
    || Maybe SomeAsyncException -> Bool
    forall a. Maybe a -> Bool
    isJust (SomeException -> Maybe SomeAsyncException
    forall e. Exception e => SomeException -> Maybe e
    C.fromException SomeException
    e :: Maybe C.SomeAsyncException)