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

    {-# LANGUAGE DefaultSignatures          #-}
    {-# LANGUAGE GeneralizedNewtypeDeriving #-}
    {-# LANGUAGE NamedFieldPuns             #-}
    {-# LANGUAGE Rank2Types                 #-}
    {-# LANGUAGE ScopedTypeVariables        #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

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

           -- * Standard prover engine
           , standardEngine

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

    import qualified Control.Exception as C

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

    import Data.IORef (readIORef, writeIORef)

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

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

    import qualified Data.Map.Strict as M

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

    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)

    -- | Extract the final configuration from a result
    resultConfig :: SMTResult -> SMTConfig
    resultConfig :: SMTResult -> SMTConfig
    resultConfig (Unsatisfiable c :: SMTConfig
    c _  ) = SMTConfig
    c
    resultConfig (Satisfiable   c :: SMTConfig
    c _  ) = SMTConfig
    c
    resultConfig (SatExtField   c :: SMTConfig
    c _  ) = SMTConfig
    c
    resultConfig (Unknown       c :: SMTConfig
    c _  ) = SMTConfig
    c
    resultConfig (ProofError    c :: SMTConfig
    c _ _) = 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
    rnf :: ThmResult -> ()
    $crnf :: ThmResult -> ()
    NFData

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

    -- | An 'Data.SBV.allSat' call results in a 'AllSatResult'. The first boolean says whether we
    -- hit the max-model limit as we searched. The second boolean says whether
    -- there were prefix-existentials. The third boolean says whether we stopped because
    -- the solver returned 'Unknown'.
    newtype AllSatResult = AllSatResult (Bool, Bool, Bool, [SMTResult])

    -- | 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)]

    -- User friendly way of printing theorem results
    instance Show ThmResult where
      show :: ThmResult -> String
    show (ThmResult r :: SMTResult
    r) = String
    -> String -> String -> String -> String -> SMTResult -> String
    showSMTResult "Q.E.D."
                                         "Unknown"
                                         "Falsifiable" "Falsifiable. Counter-example:\n" "Falsifiable in an extension field:\n" SMTResult
    r

    -- User friendly way of printing satisfiablity results
    instance Show SatResult where
      show :: SatResult -> String
    show (SatResult r :: SMTResult
    r) = String
    -> String -> String -> String -> String -> SMTResult -> String
    showSMTResult "Unsatisfiable"
                                         "Unknown"
                                         "Satisfiable" "Satisfiable. Model:\n" "Satisfiable in an extension field. Model:\n" SMTResult
    r

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

    -- The Show instance of AllSatResults. Note that we have to be careful in being lazy enough
    -- as the typical use case is to pull results out as they become available.
    instance Show AllSatResult where
      show :: AllSatResult -> String
    show (AllSatResult (l :: Bool
    l, e :: Bool
    e, u :: Bool
    u, xs :: [SMTResult]
    xs)) = Int -> [SMTResult] -> String
    forall t. (Eq t, Num t, Show t) => t -> [SMTResult] -> String
    go (0::Int) [SMTResult]
    xs
        where warnings :: String
    warnings = case (Bool
    e, Bool
    u) of
                           (False, False) -> ""
                           (False, True)  -> " (Search stopped since solver has returned unknown.)"
                           (True,  False) -> " (Unique up to prefix existentials.)"
                           (True,  True)  -> " (Search stopped becase solver has returned unknown, only prefix existentials were considered.)"

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

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

    -- Show instance for optimization results
    instance Show OptimizeResult where
      show :: OptimizeResult -> String
    show res :: OptimizeResult
    res = case OptimizeResult
    res of
                   LexicographicResult r :: SMTResult
    r   -> ShowS -> SMTResult -> String
    sh ShowS
    forall a. a -> a
    id SMTResult
    r

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

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

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

                 shI :: a -> SMTResult -> String
    shI n :: a
    n = ShowS -> SMTResult -> String
    sh (\s :: String
    s -> "Objective "     String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    n String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ": " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    s)
                 shP :: a -> SMTResult -> String
    shP i :: a
    i = ShowS -> SMTResult -> String
    sh (\s :: String
    s -> "Pareto front #" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    i String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ": " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    s)

                 sh :: ShowS -> SMTResult -> String
    sh tag :: ShowS
    tag = String
    -> String -> String -> String -> String -> SMTResult -> String
    showSMTResult (ShowS
    tag "Unsatisfiable.")
                                        (ShowS
    tag "Unknown.")
                                        (ShowS
    tag "Optimal with no assignments.")
                                        (ShowS
    tag "Optimal model:" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "\n")
                                        (ShowS
    tag "Optimal in an extension field:" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "\n")

    -- | 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 f :: a -> Maybe b
    f x :: Maybe (a, [CV])
    x = Maybe (a, [CV])
    x Maybe (a, [CV])
    -> ((a, [CV]) -> Maybe (b, [CV])) -> Maybe (b, [CV])
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \(a :: a
    a, r :: [CV]
    r) -> a -> Maybe b
    f a
    a Maybe b -> (b -> Maybe (b, [CV])) -> Maybe (b, [CV])
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \b :: b
    b -> (b, [CV]) -> Maybe (b, [CV])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (b
    b, [CV]
    r)

      default parseCVs :: Read a => [CV] -> Maybe (a, [CV])
      parseCVs (CV _ (CUserSort (_, s :: String
    s)) : r :: [CV]
    r) = (a, [CV]) -> Maybe (a, [CV])
    forall a. a -> Maybe a
    Just (String -> a
    forall a. Read a => String -> a
    read String
    s, [CV]
    r)
      parseCVs _                             = 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 :: Kind -> [CV] -> Maybe (a, [CV])
    genParse k :: Kind
    k (x :: CV
    x@(CV _ (CInteger i :: Integer
    i)):r :: [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 _ _                                         = 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 xs :: [CV]
    xs = ((), [CV]) -> Maybe ((), [CV])
    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 xs :: [CV]
    xs = do (x :: Integer
    x, r :: [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 (m :: * -> *) a. Monad m => a -> m a
    return ((Integer
    x :: Integer) Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= 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 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 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 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 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 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 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 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 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 KReal (CAlgReal i :: AlgReal
    i) : r :: [CV]
    r) = (AlgReal, [CV]) -> Maybe (AlgReal, [CV])
    forall a. a -> Maybe a
    Just (AlgReal
    i, [CV]
    r)
      parseCVs _                           = 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 KFloat (CFloat i :: Float
    i) : r :: [CV]
    r) = (Float, [CV]) -> Maybe (Float, [CV])
    forall a. a -> Maybe a
    Just (Float
    i, [CV]
    r)
      parseCVs _                          = 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 KDouble (CDouble i :: Double
    i) : r :: [CV]
    r) = (Double, [CV]) -> Maybe (Double, [CV])
    forall a. a -> Maybe a
    Just (Double
    i, [CV]
    r)
      parseCVs _                            = Maybe (Double, [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]
    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

    -- | 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 SatModel a => SatModel [a] where
      parseCVs :: [CV] -> Maybe ([a], [CV])
    parseCVs [] = ([a], [CV]) -> Maybe ([a], [CV])
    forall a. a -> Maybe a
    Just ([], [])
      parseCVs xs :: [CV]
    xs = case [CV] -> Maybe (a, [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV]
    xs of
                      Just (a :: a
    a, ys :: [CV]
    ys) -> case [CV] -> Maybe ([a], [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV]
    ys of
                                        Just (as :: [a]
    as, zs :: [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)
                                        Nothing       -> ([a], [CV]) -> Maybe ([a], [CV])
    forall a. a -> Maybe a
    Just ([], [CV]
    ys)
                      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 as :: [CV]
    as = do (a :: a
    a, bs :: [CV]
    bs) <- [CV] -> Maybe (a, [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV]
    as
                       (b :: b
    b, cs :: [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 (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 as :: [CV]
    as = do (a :: a
    a,      bs :: [CV]
    bs) <- [CV] -> Maybe (a, [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV]
    as
                       ((b :: b
    b, c :: c
    c), ds :: [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 (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 as :: [CV]
    as = do (a :: a
    a,         bs :: [CV]
    bs) <- [CV] -> Maybe (a, [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV]
    as
                       ((b :: b
    b, c :: c
    c, d :: d
    d), es :: [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 (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 as :: [CV]
    as = do (a :: a
    a, bs :: [CV]
    bs)            <- [CV] -> Maybe (a, [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV]
    as
                       ((b :: b
    b, c :: c
    c, d :: d
    d, e :: e
    e), fs :: [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 (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 as :: [CV]
    as = do (a :: a
    a, bs :: [CV]
    bs)               <- [CV] -> Maybe (a, [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV]
    as
                       ((b :: b
    b, c :: c
    c, d :: d
    d, e :: e
    e, f :: f
    f), gs :: [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 (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 as :: [CV]
    as = do (a :: a
    a, bs :: [CV]
    bs)                  <- [CV] -> Maybe (a, [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV]
    as
                       ((b :: b
    b, c :: c
    c, d :: d
    d, e :: e
    e, f :: f
    f, g :: g
    g), hs :: [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 (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 v :: String
    v r :: a
    r = CV -> b
    forall a. SymVal a => CV -> a
    fromCV (CV -> b) -> Maybe CV -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` (String
    v String -> Map String CV -> Maybe CV
    forall k a. Ord k => k -> Map k a -> Maybe a
    `M.lookup` a -> Map String CV
    forall a. Modelable a => a -> Map String 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 v :: String
    v r :: a
    r = case String
    v String -> Map String CV -> Maybe CV
    forall k a. Ord k => k -> Map k a -> Maybe a
    `M.lookup` a -> Map String CV
    forall a. Modelable a => a -> Map String CV
    getModelDictionary a
    r of
                                         Just (CV _ (CUserSort (_, s :: String
    s))) -> String -> Maybe String
    forall a. a -> Maybe a
    Just String
    s
                                         _                              -> Maybe String
    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
    a = case a -> Either String (Bool, b)
    forall a b.
    (Modelable a, SatModel b) =>
    a -> Either String (Bool, b)
    getModelAssignment a
    a of
                         Right (_, b :: b
    b) -> b -> Maybe b
    forall a. a -> Maybe a
    Just b
    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 v :: String
    v r :: a
    r = String
    v String -> Map String GeneralizedCV -> Maybe GeneralizedCV
    forall k a. Ord k => k -> Map k a -> Maybe a
    `M.lookup` a -> Map String GeneralizedCV
    forall a. Modelable a => a -> Map String GeneralizedCV
    getModelObjectives a
    r

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

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

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

    -- | Get dictionaries from an all-sat call. Similar to `getModelDictionary`.
    getModelDictionaries :: AllSatResult -> [M.Map String CV]
    getModelDictionaries :: AllSatResult -> [Map String CV]
    getModelDictionaries (AllSatResult (_, _, _, xs :: [SMTResult]
    xs)) = (SMTResult -> Map String CV) -> [SMTResult] -> [Map String CV]
    forall a b. (a -> b) -> [a] -> [b]
    map SMTResult -> Map String CV
    forall a. Modelable a => a -> Map String 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 :: String -> AllSatResult -> [Maybe b]
    getModelValues s :: String
    s (AllSatResult (_, _, _, xs :: [SMTResult]
    xs)) =  (SMTResult -> Maybe b) -> [SMTResult] -> [Maybe b]
    forall a b. (a -> b) -> [a] -> [b]
    map (String
    s String -> SMTResult -> Maybe b
    forall a b. (Modelable a, SymVal b) => String -> 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 :: String -> AllSatResult -> [Maybe String]
    getModelUninterpretedValues s :: String
    s (AllSatResult (_, _, _, xs :: [SMTResult]
    xs)) =  (SMTResult -> Maybe String) -> [SMTResult] -> [Maybe String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String
    s String -> SMTResult -> Maybe String
    forall a. Modelable a => String -> a -> Maybe String
    `getModelUninterpretedValue`) [SMTResult]
    xs

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

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

    -- | 'SMTResult' as a generic model provider
    instance Modelable SMTResult where
      getModelAssignment :: SMTResult -> Either String (Bool, b)
    getModelAssignment (Unsatisfiable _ _  ) = String -> Either String (Bool, b)
    forall a b. a -> Either a b
    Left "SBV.getModelAssignment: Unsatisfiable result"
      getModelAssignment (Satisfiable   _ m :: SMTModel
    m  ) = (Bool, b) -> Either String (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   _ _  ) = String -> Either String (Bool, b)
    forall a b. a -> Either a b
    Left "SBV.getModelAssignment: The model is in an extension field"
      getModelAssignment (Unknown       _ m :: SMTReasonUnknown
    m  ) = String -> Either String (Bool, b)
    forall a b. a -> Either a b
    Left (String -> Either String (Bool, b))
    -> String -> Either String (Bool, b)
    forall a b. (a -> b) -> a -> b
    $ "SBV.getModelAssignment: Solver state is unknown: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SMTReasonUnknown -> String
    forall a. Show a => a -> String
    show SMTReasonUnknown
    m
      getModelAssignment (ProofError    _ s :: [String]
    s _) = String -> Either String (Bool, b)
    forall a. HasCallStack => String -> a
    error (String -> Either String (Bool, b))
    -> String -> Either String (Bool, b)
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.getModelAssignment: Failed to produce a model: " String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    s

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

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

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

      getModelUIFuns :: SMTResult -> Map String (SBVType, ([([CV], CV)], CV))
    getModelUIFuns Unsatisfiable{}   = Map String (SBVType, ([([CV], CV)], CV))
    forall k a. Map k a
    M.empty
      getModelUIFuns (Satisfiable _ m :: SMTModel
    m) = [(String, (SBVType, ([([CV], CV)], CV)))]
    -> Map String (SBVType, ([([CV], CV)], CV))
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList (SMTModel -> [(String, (SBVType, ([([CV], CV)], CV)))]
    modelUIFuns SMTModel
    m)
      getModelUIFuns (SatExtField _ m :: SMTModel
    m) = [(String, (SBVType, ([([CV], CV)], CV)))]
    -> Map String (SBVType, ([([CV], CV)], CV))
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList (SMTModel -> [(String, (SBVType, ([([CV], CV)], CV)))]
    modelUIFuns SMTModel
    m)
      getModelUIFuns Unknown{}         = Map String (SBVType, ([([CV], CV)], CV))
    forall k a. Map k a
    M.empty
      getModelUIFuns ProofError{}      = Map String (SBVType, ([([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 :: SMTModel -> a
    parseModelOut m :: SMTModel
    m = case [CV] -> Maybe (a, [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV
    c | (_, c :: CV
    c) <- SMTModel -> [(String, CV)]
    modelAssocs SMTModel
    m] of
                       Just (x :: a
    x, []) -> a
    x
                       Just (_, ys :: [CV]
    ys) -> String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ "SBV.parseModelOut: Partially constructed model; remaining elements: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [CV] -> String
    forall a. Show a => a -> String
    show [CV]
    ys
                       Nothing      -> String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ "SBV.parseModelOut: Cannot construct a model from: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SMTModel -> String
    forall a. Show a => a -> String
    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, returing 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 :: ([(Bool, a)] -> [(Bool, a)])
    -> (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int
    displayModels arrange :: [(Bool, a)] -> [(Bool, a)]
    arrange disp :: Int -> (Bool, a) -> IO ()
    disp (AllSatResult (_, _, _, ms :: [SMTResult]
    ms)) = do
        let models :: [(Bool, a)]
    models = [(Bool, a)
    a | Right a :: (Bool, a)
    a <- (SMTResult -> Either String (Bool, a))
    -> [SMTResult] -> [Either String (Bool, a)]
    forall a b. (a -> b) -> [a] -> [b]
    map (SatResult -> Either String (Bool, a)
    forall a b.
    (Modelable a, SatModel b) =>
    a -> Either String (Bool, b)
    getModelAssignment (SatResult -> Either String (Bool, a))
    -> (SMTResult -> SatResult) -> SMTResult -> Either String (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) [(1::Int)..]
        Int -> IO Int
    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. [a] -> a
    last (0Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    :[Int]
    inds)
      where display :: (Bool, a) -> Int -> IO Int
    display r :: (Bool, a)
    r i :: Int
    i = Int -> (Bool, a) -> IO ()
    disp Int
    i (Bool, a)
    r IO () -> IO Int -> IO Int
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Int -> IO Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    i

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

     where cfg :: SMTConfig
    cfg = SMTResult -> SMTConfig
    resultConfig SMTResult
    result
           showUnsatCore :: Maybe [String] -> String
    showUnsatCore Nothing   = ""
           showUnsatCore (Just xs :: [String]
    xs) = ". Unsat core:\n" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate "\n" ["    " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    x | String
    x <- [String]
    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 -> String
    showModel cfg :: SMTConfig
    cfg model :: SMTModel
    model
       | [(String, (SBVType, ([([CV], CV)], CV)))] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(String, (SBVType, ([([CV], CV)], CV)))]
    uiFuncs
       = String
    nonUIFuncs
       | Bool
    True
       = ShowS
    sep String
    nonUIFuncs String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate "\n\n" (((String, (SBVType, ([([CV], CV)], CV))) -> String)
    -> [(String, (SBVType, ([([CV], CV)], CV)))] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (SMTConfig -> (String, (SBVType, ([([CV], CV)], CV))) -> String
    showModelUI SMTConfig
    cfg) [(String, (SBVType, ([([CV], CV)], CV)))]
    uiFuncs)
       where nonUIFuncs :: String
    nonUIFuncs = Bool -> Bool -> SMTConfig -> [(String, GeneralizedCV)] -> String
    showModelDictionary ([(String, (SBVType, ([([CV], CV)], CV)))] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(String, (SBVType, ([([CV], CV)], CV)))]
    uiFuncs) Bool
    False SMTConfig
    cfg [(String
    n, CV -> GeneralizedCV
    RegularCV CV
    c) | (n :: String
    n, c :: CV
    c) <- SMTModel -> [(String, CV)]
    modelAssocs SMTModel
    model]
             uiFuncs :: [(String, (SBVType, ([([CV], CV)], CV)))]
    uiFuncs    = SMTModel -> [(String, (SBVType, ([([CV], CV)], CV)))]
    modelUIFuns SMTModel
    model
             sep :: ShowS
    sep ""     = ""
             sep x :: String
    x      = String
    x String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "\n\n"

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

            relevantVars :: [(String, GeneralizedCV)]
    relevantVars  = ((String, GeneralizedCV) -> Bool)
    -> [(String, GeneralizedCV)] -> [(String, GeneralizedCV)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool)
    -> ((String, GeneralizedCV) -> Bool)
    -> (String, GeneralizedCV)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String, GeneralizedCV) -> Bool
    forall b. (String, b) -> Bool
    ignore) [(String, GeneralizedCV)]
    allVars
            ignore :: (String, b) -> Bool
    ignore (s :: String
    s, _)
              | Bool
    includeEverything = Bool
    False
              | Bool
    True              = "__internal_sbv_" String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isPrefixOf` String
    s Bool -> Bool -> Bool
    || SMTConfig -> String -> Bool
    isNonModelVar SMTConfig
    cfg String
    s

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

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

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

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

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

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

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

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

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

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

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

            scv :: CV -> String
    scv = Int -> CV -> String
    forall a. (Eq a, Num a) => a -> CV -> String
    sh (SMTConfig -> Int
    printBase SMTConfig
    cfg)
              where sh :: a -> CV -> String
    sh 2  = CV -> String
    forall a. PrettyNum a => a -> String
    binP
                    sh 10 = Bool -> CV -> String
    showCV Bool
    False
                    sh 16 = CV -> String
    forall a. PrettyNum a => a -> String
    hexP
                    sh _  = CV -> String
    forall a. Show a => a -> String
    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) -> ([String], String)
    line (args :: [CV]
    args, r :: CV
    r) = (String
    nm String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : (CV -> String) -> [CV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (ShowS
    paren ShowS -> (CV -> String) -> CV -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CV -> String
    scv) [CV]
    args, CV -> String
    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 :: String
    x@('-':_) = '(' Char -> ShowS
    forall a. a -> [a] -> [a]
    : String
    x String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
                    paren x :: String
    x         = String
    x

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

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

          Just execPath :: String
    execPath -> SMTConfig
    -> State -> String -> [String] -> String -> (State -> IO a) -> IO a
    forall a.
    SMTConfig
    -> State -> String -> [String] -> String -> (State -> IO a) -> IO a
    runSolver SMTConfig
    cfg State
    ctx String
    execPath [String]
    opts String
    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
    $ String -> IO a
    forall a. HasCallStack => String -> a
    error (String -> IO a) -> String -> IO a
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ "Failed to start the external solver:\n" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SomeException -> String
    forall a. Show a => a -> String
    show SomeException
    e
                                                                                                    , "Make sure you can start " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    execPath
                                                                                                    , "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 :: String -> String -> SMTEngine
    standardEngine envName :: String
    envName envOptName :: String
    envOptName cfg :: SMTConfig
    cfg ctx :: State
    ctx pgm :: String
    pgm continuation :: State -> IO res
    continuation = do

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

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

        SMTConfig -> State -> String -> (State -> IO res) -> IO res
    SMTEngine
    standardSolver SMTConfig
    cfg' State
    ctx String
    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 currrent configuration
                   -> State           -- ^ Context in which we are running
                   -> String          -- ^ The program
                   -> (State -> IO a) -- ^ The continuation
                   -> IO a
    standardSolver :: SMTConfig -> State -> String -> (State -> IO a) -> IO a
    standardSolver config :: SMTConfig
    config ctx :: State
    ctx pgm :: String
    pgm continuation :: State -> IO a
    continuation = do
        let msg :: String -> m ()
    msg s :: String
    s    = SMTConfig -> [String] -> m ()
    forall (m :: * -> *). MonadIO m => SMTConfig -> [String] -> m ()
    debug SMTConfig
    config ["** " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    s]
            smtSolver :: SMTSolver
    smtSolver= SMTConfig -> SMTSolver
    solver SMTConfig
    config
            exec :: String
    exec     = SMTSolver -> String
    executable SMTSolver
    smtSolver
            opts :: [String]
    opts     = SMTSolver -> SMTConfig -> [String]
    options SMTSolver
    smtSolver SMTConfig
    config
        String -> IO ()
    forall (m :: * -> *). MonadIO m => String -> m ()
    msg (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ "Calling: "  String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (String
    exec String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (if [String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    opts then "" else " ") String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    joinArgs [String]
    opts)
        String -> ()
    forall a. NFData a => a -> ()
    rnf String
    pgm () -> IO a -> IO a
    forall a b. a -> b -> b
    `seq` SMTConfig
    -> State -> String -> [String] -> String -> (State -> IO a) -> IO a
    forall a.
    SMTConfig
    -> State -> String -> [String] -> String -> (State -> IO a) -> IO a
    pipeProcess SMTConfig
    config State
    ctx String
    exec [String]
    opts String
    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 :: SMTConfig
    -> State -> String -> [String] -> String -> (State -> IO a) -> IO a
    runSolver cfg :: SMTConfig
    cfg ctx :: State
    ctx execPath :: String
    execPath opts :: [String]
    opts pgm :: String
    pgm continuation :: State -> IO a
    continuation
     = do let nm :: String
    nm  = Solver -> String
    forall a. Show a => a -> String
    show (SMTSolver -> Solver
    name (SMTConfig -> SMTSolver
    solver SMTConfig
    cfg))
              msg :: [String] -> IO ()
    msg = SMTConfig -> [String] -> IO ()
    forall (m :: * -> *). MonadIO m => SMTConfig -> [String] -> m ()
    debug SMTConfig
    cfg ([String] -> IO ()) -> ([String] -> [String]) -> [String] -> IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ShowS -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map ("*** " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++)

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

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

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

                        -- Send a line, get a whole s-expr. We ignore the pathetic case that there might be a string with an unbalanced parentheses in it in a response.
                        ask :: Maybe Int -> String -> IO String
                        ask :: Maybe Int -> String -> IO String
    ask mbTimeOut :: Maybe Int
    mbTimeOut command :: String
    command =
                                      -- solvers don't respond to empty lines or comments; we just pass back
                                      -- success in these cases to keep the illusion of everything has a response
                                      let cmd :: String
    cmd = (Char -> Bool) -> ShowS
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile Char -> Bool
    isSpace String
    command
                                      in if String -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null String
    cmd Bool -> Bool -> Bool
    || ";" String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isPrefixOf` String
    cmd
                                         then String -> IO String
    forall (m :: * -> *) a. Monad m => a -> m a
    return "success"
                                         else do Maybe Int -> String -> IO ()
    send Maybe Int
    mbTimeOut String
    command
                                                 Maybe String -> Maybe Int -> IO String
    getResponseFromSolver (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    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 String -> Maybe Int -> IO String
    getResponseFromSolver mbCommand :: Maybe String
    mbCommand mbTimeOut :: Maybe Int
    mbTimeOut = do
                                    [String]
    response <- Bool -> Int -> [String] -> IO [String]
    go Bool
    True 0 []
                                    let collated :: String
    collated = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate "\n" ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ [String] -> [String]
    forall a. [a] -> [a]
    reverse [String]
    response
                                    Maybe String -> Either (String, Maybe Int) String -> IO ()
    recordTranscript (SMTConfig -> Maybe String
    transcript SMTConfig
    cfg) (Either (String, Maybe Int) String -> IO ())
    -> Either (String, Maybe Int) String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> Either (String, Maybe Int) String
    forall a b. b -> Either a b
    Right String
    collated
                                    String -> IO String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    collated

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

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

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

                                                                                          stillInside :: Bool
    stillInside = Bool -> String -> Bool
    walk Bool
    inString String
    ln

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

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

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

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

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

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

                        terminateSolver :: IO (String, String, ExitCode)
    terminateSolver = do Handle -> IO ()
    hClose Handle
    inh
                                             MVar ()
    outMVar <- IO (MVar ())
    forall a. IO (MVar a)
    newEmptyMVar
                                             String
    out <- Handle -> IO String
    hGetContents Handle
    outh IO String -> (SomeException -> IO String) -> IO String
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `C.catch`  (\(SomeException
    e :: C.SomeException) -> SomeException -> IO String -> IO String
    forall a. SomeException -> IO a -> IO a
    handleAsync SomeException
    e (String -> IO String
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SomeException -> String
    forall a. Show a => a -> String
    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 (String -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    out) IO Int -> IO () -> IO ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> MVar () -> () -> IO ()
    forall a. MVar a -> a -> IO ()
    putMVar MVar ()
    outMVar ()
                                             String
    err <- Handle -> IO String
    hGetContents Handle
    errh IO String -> (SomeException -> IO String) -> IO String
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `C.catch`  (\(SomeException
    e :: C.SomeException) -> SomeException -> IO String -> IO String
    forall a. SomeException -> IO a -> IO a
    handleAsync SomeException
    e (String -> IO String
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SomeException -> String
    forall a. Show a => a -> String
    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 (String -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    err) IO Int -> IO () -> IO ()
    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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
    return (Int -> ExitCode
    ExitFailure (-999))))
                                             (String, String, ExitCode) -> IO (String, String, ExitCode)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String
    out, String
    err, ExitCode
    ex)

                        cleanUp :: IO ()
    cleanUp
                          = do (out :: String
    out, err :: String
    err, ex :: ExitCode
    ex) <- IO (String, String, ExitCode)
    terminateSolver

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

                               Maybe String -> ExitCode -> IO ()
    finalizeTranscript (SMTConfig -> Maybe String
    transcript SMTConfig
    cfg) ExitCode
    ex
                               SMTConfig -> State -> IO ()
    recordEndTime SMTConfig
    cfg State
    ctx

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

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

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

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

                                                                    reason :: [String]
    reason | Bool
    isOption = [ "Backend solver reports it does not support this option."
                                                                                        , "Check the spelling, and if correct please report this as a"
                                                                                        , "bug/feature request with the solver!"
                                                                                        ]
                                                                           | Bool
    True     = [ "Check solver response for further information. If your code is correct,"
                                                                                        , "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 String String
    mbExtras <- (String -> Either String String
    forall a b. b -> Either a b
    Right (String -> Either String String)
    -> IO String -> IO (Either String String)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe String -> Maybe Int -> IO String
    getResponseFromSolver Maybe String
    forall a. Maybe a
    Nothing (Int -> Maybe Int
    forall a. a -> Maybe a
    Just 5000000))
                                                                            IO (Either String String)
    -> (SomeException -> IO (Either String String))
    -> IO (Either String String)
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `C.catch` (\(SomeException
    e :: C.SomeException) -> SomeException
    -> IO (Either String String) -> IO (Either String String)
    forall a. SomeException -> IO a -> IO a
    handleAsync SomeException
    e (Either String String -> IO (Either String String)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> Either String String
    forall a b. a -> Either a b
    Left (SomeException -> String
    forall a. Show a => a -> String
    show SomeException
    e))))

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

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

                                                                    exc :: SBVException
    exc = SBVException :: String
    -> Maybe String
    -> Maybe String
    -> Maybe String
    -> Maybe String
    -> Maybe String
    -> Maybe ExitCode
    -> SMTConfig
    -> Maybe [String]
    -> Maybe [String]
    -> SBVException
    SBVException { sbvExceptionDescription :: String
    sbvExceptionDescription = "Unexpected non-success response from " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    nm
                                                                                       , sbvExceptionSent :: Maybe String
    sbvExceptionSent        = String -> Maybe String
    forall a. a -> Maybe a
    Just String
    l
                                                                                       , sbvExceptionExpected :: Maybe String
    sbvExceptionExpected    = String -> Maybe String
    forall a. a -> Maybe a
    Just "success"
                                                                                       , sbvExceptionReceived :: Maybe String
    sbvExceptionReceived    = String -> Maybe String
    forall a. a -> Maybe a
    Just (String -> Maybe String) -> String -> Maybe String
    forall a b. (a -> b) -> a -> b
    $ String
    r String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "\n" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    extras
                                                                                       , sbvExceptionStdOut :: Maybe String
    sbvExceptionStdOut      = String -> Maybe String
    forall a. a -> Maybe a
    Just String
    out
                                                                                       , sbvExceptionStdErr :: Maybe String
    sbvExceptionStdErr      = String -> Maybe String
    forall a. a -> Maybe a
    Just String
    err
                                                                                       , sbvExceptionExitCode :: Maybe ExitCode
    sbvExceptionExitCode    = ExitCode -> Maybe ExitCode
    forall a. a -> Maybe a
    Just ExitCode
    ex
                                                                                       , sbvExceptionConfig :: SMTConfig
    sbvExceptionConfig      = SMTConfig
    cfg { solver :: SMTSolver
    solver = (SMTConfig -> SMTSolver
    solver SMTConfig
    cfg) {executable :: String
    executable = String
    execPath } }
                                                                                       , sbvExceptionReason :: Maybe [String]
    sbvExceptionReason      = [String] -> Maybe [String]
    forall a. a -> Maybe a
    Just [String]
    reason
                                                                                       , sbvExceptionHint :: Maybe [String]
    sbvExceptionHint        = Maybe [String]
    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 -> String -> IO ()
    sendAndGetSuccess Maybe Int
    forall a. Maybe a
    Nothing "; 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 -> [String] -> IO ()
    forall (m :: * -> *). MonadIO m => SMTConfig -> [String] -> m ()
    debug SMTConfig
    cfg ["** Skipping heart-beat for the solver " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Solver -> String
    forall a. Show a => a -> String
    show Solver
    backend]
                                    else do let heartbeat :: String
    heartbeat = "(set-option :print-success true)"
                                            String
    r <- Maybe Int -> String -> IO String
    ask (Int -> Maybe Int
    forall a. a -> Maybe a
    Just 5000000) String
    heartbeat  -- Give the solver 5s to respond, this should be plenty enough!
                                            case String -> [String]
    words String
    r of
                                              ["success"]     -> SMTConfig -> [String] -> IO ()
    forall (m :: * -> *). MonadIO m => SMTConfig -> [String] -> m ()
    debug SMTConfig
    cfg ["[GOOD] " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    heartbeat]
                                              ["unsupported"] -> String -> IO ()
    forall a. HasCallStack => String -> a
    error (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ ""
                                                                                 , "*** Backend solver (" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++  Solver -> String
    forall a. Show a => a -> String
    show Solver
    backend String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ") does not support the command:"
                                                                                 , "***"
                                                                                 , "***     (set-option :print-success true)"
                                                                                 , "***"
                                                                                 , "*** SBV relies on this feature to coordinate communication!"
                                                                                 , "*** Please request this as a feature!"
                                                                                 ]
                                              _               -> String -> IO ()
    forall a. HasCallStack => String -> a
    error (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ ""
                                                                                 , "*** Data.SBV: Failed to initiate contact with the solver!"
                                                                                 , "***"
                                                                                 , "***   Sent    : " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    heartbeat
                                                                                 , "***   Expected: success"
                                                                                 , "***   Received: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    r
                                                                                 , "***"
                                                                                 , "*** 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 -> [String] -> IO ()
    forall (m :: * -> *). MonadIO m => SMTConfig -> [String] -> m ()
    debug SMTConfig
    cfg [ "** Backend solver " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Solver -> String
    forall a. Show a => a -> String
    show Solver
    backend String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " does not support global decls."
                                                   , "** Some incremental calls, such as pop, will be limited."
                                                   ]
                                    else Maybe Int -> String -> IO ()
    sendAndGetSuccess Maybe Int
    forall a. Maybe a
    Nothing "(set-option :global-declarations true)"

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

                                 -- Prepare the query context and ship it off
                                 let qs :: QueryState
    qs = QueryState :: (Maybe Int -> String -> IO String)
    -> (Maybe Int -> String -> IO ())
    -> (Maybe Int -> IO String)
    -> SMTConfig
    -> IO ()
    -> Maybe Int
    -> Int
    -> QueryState
    QueryState { queryAsk :: Maybe Int -> String -> IO String
    queryAsk                 = Maybe Int -> String -> IO String
    ask
                                                     , querySend :: Maybe Int -> String -> IO ()
    querySend                = Maybe Int -> String -> IO ()
    send
                                                     , queryRetrieveResponse :: Maybe Int -> IO String
    queryRetrieveResponse    = Maybe String -> Maybe Int -> IO String
    getResponseFromSolver Maybe String
    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 = 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
                                   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 _  -> String -> IO ()
    forall a. HasCallStack => String -> a
    error (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ ""
                                                              , "Data.SBV: Impossible happened, query-state was already set."
                                                              , "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 String -> SMTConfig -> IO ()
    startTranscript (SMTConfig -> Maybe String
    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 String -> String -> IO ()
    recordException    (SMTConfig -> Maybe String
    transcript SMTConfig
    cfg) (SomeException -> String
    forall a. Show a => a -> String
    show SomeException
    e)
                                                                                Maybe String -> ExitCode -> IO ()
    finalizeTranscript (SMTConfig -> Maybe String
    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 :: SMTConfig -> Timing
    timing :: Timing
    timing} state :: State
    state = case Timing
    timing of
                                               NoTiming        -> () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                                               PrintTiming     -> do NominalDiffTime
    e <- IO NominalDiffTime
    elapsed
                                                                     String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ "*** SBV: Elapsed time: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ NominalDiffTime -> String
    showTDiff NominalDiffTime
    e
                                               SaveTiming here :: 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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \end :: UTCTime
    end -> NominalDiffTime -> IO NominalDiffTime
    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 String -> SMTConfig -> IO ()
    startTranscript Nothing  _   = () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    startTranscript (Just f :: String
    f) cfg :: SMTConfig
    cfg = do String
    ts <- ZonedTime -> String
    forall a. Show a => a -> String
    show (ZonedTime -> String) -> IO ZonedTime -> IO String
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO ZonedTime
    getZonedTime
                                      Maybe String
    mbExecPath <- String -> IO (Maybe String)
    findExecutable (SMTSolver -> String
    executable (SMTConfig -> SMTSolver
    solver SMTConfig
    cfg))
                                      String -> String -> IO ()
    writeFile String
    f (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String -> String
    start String
    ts Maybe String
    mbExecPath
      where SMTSolver{Solver
    name :: Solver
    name :: SMTSolver -> Solver
    name, SMTConfig -> [String]
    options :: SMTConfig -> [String]
    options :: SMTSolver -> SMTConfig -> [String]
    options} = SMTConfig -> SMTSolver
    solver SMTConfig
    cfg
            start :: String -> Maybe String -> String
    start ts :: String
    ts mbPath :: Maybe String
    mbPath = [String] -> String
    unlines [ ";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                                      , ";;; SBV: Starting at " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ts
                                      , ";;;"
                                      , ";;;           Solver    : " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Solver -> String
    forall a. Show a => a -> String
    show Solver
    name
                                      , ";;;           Executable: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String -> Maybe String -> String
    forall a. a -> Maybe a -> a
    fromMaybe "Unable to locate the executable" Maybe String
    mbPath
                                      , ";;;           Options   : " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords (SMTConfig -> [String]
    options SMTConfig
    cfg)
                                      , ";;;"
                                      , ";;; This file is an auto-generated loadable SMT-Lib file."
                                      , ";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                                      , ""
                                      ]

    -- | Finish up the transcript file.
    finalizeTranscript :: Maybe FilePath -> ExitCode -> IO ()
    finalizeTranscript :: Maybe String -> ExitCode -> IO ()
    finalizeTranscript Nothing  _  = () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    finalizeTranscript (Just f :: String
    f) ec :: ExitCode
    ec = do String
    ts <- ZonedTime -> String
    forall a. Show a => a -> String
    show (ZonedTime -> String) -> IO ZonedTime -> IO String
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO ZonedTime
    getZonedTime
                                        String -> String -> IO ()
    appendFile String
    f (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ ShowS
    end String
    ts
      where end :: ShowS
    end ts :: String
    ts = [String] -> String
    unlines [ ""
                             , ";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                             , ";;;"
                             , ";;; SBV: Finished at " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ts
                             , ";;;"
                             , ";;; Exit code: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ExitCode -> String
    forall a. Show a => a -> String
    show ExitCode
    ec
                             , ";;;"
                             , ";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                             ]

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

    -- Record the exception
    recordException :: Maybe FilePath -> String -> IO ()
    recordException :: Maybe String -> String -> IO ()
    recordException Nothing  _ = () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    recordException (Just f :: String
    f) m :: String
    m = do String
    ts <- ZonedTime -> String
    forall a. Show a => a -> String
    show (ZonedTime -> String) -> IO ZonedTime -> IO String
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO ZonedTime
    getZonedTime
                                    String -> String -> IO ()
    appendFile String
    f (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ ShowS
    exc String
    ts
      where exc :: ShowS
    exc ts :: String
    ts = [String] -> String
    unlines ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ [ ""
                               , ";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                               , ";;;"
                               , ";;; SBV: Caught an exception at " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ts
                               , ";;;"
                               ]
                            [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ ";;;   " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    l | String
    l <- (String -> Bool) -> [String] -> [String]
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile String -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (String -> [String]
    lines String
    m) ]
                            [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ ";;;"
                               , ";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                               ]

    -- We should not be catching/processing asynchronous exceptions.
    -- See http://github.com/LeventErkok/sbv/issues/410
    handleAsync :: C.SomeException -> IO a -> IO a
    handleAsync :: SomeException -> IO a -> IO a
    handleAsync e :: SomeException
    e cont :: 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)