    -- |
    -- Module      :  Cryptol.Symbolic.SBV
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE CPP #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE ImplicitParams #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE RecordWildCards #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TupleSections #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE ViewPatterns #-}

    module Cryptol.Symbolic.SBV
     ( SBVProverConfig
     , defaultProver
     , proverNames
     , setupProver
     , satProve
     , satProveOffline
     , SBVPortfolioException(..)
     ) where

    import Control.Applicative
    import Control.Concurrent.Async
    import Control.Concurrent.MVar
    import Control.Monad.IO.Class
    import Control.Monad (when, foldM, forM_)
    import Data.Maybe (fromMaybe)
    import qualified Data.Map as Map
    import qualified Control.Exception as X
    import System.Exit (ExitCode(ExitSuccess))

    import LibBF(bfNaN)

    import qualified Data.SBV as SBV (sObserve, symbolicEnv)
    import qualified Data.SBV.Internals as SBV (SBV(..))
    import qualified Data.SBV.Dynamic as SBV
    import           Data.SBV (Timing(SaveTiming))

    import qualified Cryptol.ModuleSystem as M hiding (getPrimMap)
    import qualified Cryptol.ModuleSystem.Env as M
    import qualified Cryptol.ModuleSystem.Base as M
    import qualified Cryptol.ModuleSystem.Monad as M
    import qualified Cryptol.ModuleSystem.Name as M

    import           Cryptol.Backend.SBV
    import qualified Cryptol.Backend.FloatHelpers as FH

    import qualified Cryptol.Eval as Eval
    import qualified Cryptol.Eval.Concrete as Concrete
    import qualified Cryptol.Eval.Value as Eval
    import           Cryptol.Eval.SBV
    import           Cryptol.Parser.Position (emptyRange)
    import           Cryptol.Symbolic
    import           Cryptol.TypeCheck.AST
    import           Cryptol.Utils.Ident (preludeReferenceName, prelPrim, identText)
    import           Cryptol.Utils.Panic(panic)
    import           Cryptol.Utils.Logger(logPutStrLn)
    import           Cryptol.Utils.RecordMap

    import Prelude ()
    import Prelude.Compat

    doSBVEval :: MonadIO m => SBVEval a -> m (SBV.SVal, a)
    doSBVEval :: forall (m :: * -> *) a. MonadIO m => SBVEval a -> m (SVal, a)
    doSBVEval SBVEval a
    m =
      (IO (SBVResult a) -> m (SBVResult a)
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SBVResult a) -> m (SBVResult a))
    -> IO (SBVResult a) -> m (SBVResult a)
    forall a b. (a -> b) -> a -> b
    $ CallStack -> Eval (SBVResult a) -> IO (SBVResult a)
    forall a. CallStack -> Eval a -> IO a
    Eval.runEval CallStack
    forall a. Monoid a => a
    mempty (SBVEval a -> Eval (SBVResult a)
    forall a. SBVEval a -> Eval (SBVResult a)
    sbvEval SBVEval a
    m)) m (SBVResult a) -> (SBVResult a -> m (SVal, a)) -> m (SVal, a)
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        SBVError EvalErrorEx
    err -> IO (SVal, a) -> m (SVal, a)
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (EvalErrorEx -> IO (SVal, a)
    forall e a. Exception e => e -> IO a
    X.throwIO EvalErrorEx
    err)
        SBVResult SVal
    p a
    x -> (SVal, a) -> m (SVal, a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal
    p, a
    x)

    -- External interface ----------------------------------------------------------

    proverConfigs :: [(String, SBV.SMTConfig)]
    proverConfigs :: [(String, SMTConfig)]
    proverConfigs =
      [ (String
    "cvc4"     , SMTConfig
    SBV.cvc4     )
      , (String
    "cvc5"     , SMTConfig
    SBV.cvc5     )
      , (String
    "yices"    , SMTConfig
    SBV.yices    )
      , (String
    "z3"       , SMTConfig
    SBV.z3       )
      , (String
    "boolector", SMTConfig
    SBV.boolector)
      , (String
    "mathsat"  , SMTConfig
    SBV.mathSAT  )
      , (String
    "abc"      , SMTConfig
    SBV.abc      )
      , (String
    "offline"  , SMTConfig
    SBV.defaultSMTCfg )
      , (String
    "any"      , SMTConfig
    SBV.defaultSMTCfg )

      , (String
    "sbv-cvc4"     , SMTConfig
    SBV.cvc4     )
      , (String
    "sbv-cvc5"     , SMTConfig
    SBV.cvc5     )
      , (String
    "sbv-yices"    , SMTConfig
    SBV.yices    )
      , (String
    "sbv-z3"       , SMTConfig
    SBV.z3       )
      , (String
    "sbv-boolector", SMTConfig
    SBV.boolector)
      , (String
    "sbv-mathsat"  , SMTConfig
    SBV.mathSAT  )
      , (String
    "sbv-abc"      , SMTConfig
    SBV.abc      )
      , (String
    "sbv-offline"  , SMTConfig
    SBV.defaultSMTCfg )
      , (String
    "sbv-any"      , SMTConfig
    SBV.defaultSMTCfg )
      ]

    newtype SBVPortfolioException
      = SBVPortfolioException [Either X.SomeException (Maybe String,String)]

    instance Show SBVPortfolioException where
      show :: SBVPortfolioException -> String
    show (SBVPortfolioException [Either SomeException (Maybe String, String)]
    exs) =
           [String] -> String
    unlines (String
    "All solvers in the portfolio failed!" String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : (Either SomeException (Maybe String, String) -> String)
    -> [Either SomeException (Maybe String, String)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Either SomeException (Maybe String, String) -> String
    forall {e}.
    Exception e =>
    Either e (Maybe String, String) -> String
    f [Either SomeException (Maybe String, String)]
    exs)
        where
        f :: Either e (Maybe String, String) -> String
    f (Left e
    e) = e -> String
    forall e. Exception e => e -> String
    X.displayException e
    e
        f (Right (Maybe String
    Nothing, String
    msg)) = String
    msg
        f (Right (Just String
    nm, String
    msg)) = String
    nm String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ": " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    msg

    instance X.Exception SBVPortfolioException

    data SBVProverConfig
      = SBVPortfolio [SBV.SMTConfig]
      | SBVProverConfig SBV.SMTConfig

    defaultProver :: SBVProverConfig
    defaultProver :: SBVProverConfig
    defaultProver = SMTConfig -> SBVProverConfig
    SBVProverConfig SMTConfig
    SBV.z3

    -- | The names of all the solvers supported by SBV
    proverNames :: [String]
    proverNames :: [String]
    proverNames = ((String, SMTConfig) -> String)
    -> [(String, SMTConfig)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, SMTConfig) -> String
    forall a b. (a, b) -> a
    fst [(String, SMTConfig)]
    proverConfigs

    setupProver :: String -> IO (Either String ([String], SBVProverConfig))
    setupProver :: String -> IO (Either String ([String], SBVProverConfig))
    setupProver String
    nm
      | String
    nm String -> [String] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [String
    "any",String
    "sbv-any"] =
    #if MIN_VERSION_sbv(8,9,0)
        do [SMTConfig]
    ps <- IO [SMTConfig]
    SBV.getAvailableSolvers
    #else
        do ps <- SBV.sbvAvailableSolvers
    #endif
           case [SMTConfig]
    ps of
             [] -> Either String ([String], SBVProverConfig)
    -> IO (Either String ([String], SBVProverConfig))
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (String -> Either String ([String], SBVProverConfig)
    forall a b. a -> Either a b
    Left String
    "SBV could not find any provers")
             [SMTConfig]
    _ ->  let msg :: String
    msg = String
    "SBV found the following solvers: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Solver] -> String
    forall a. Show a => a -> String
    show ((SMTConfig -> Solver) -> [SMTConfig] -> [Solver]
    forall a b. (a -> b) -> [a] -> [b]
    map (SMTSolver -> Solver
    SBV.name (SMTSolver -> Solver)
    -> (SMTConfig -> SMTSolver) -> SMTConfig -> Solver
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SMTConfig -> SMTSolver
    SBV.solver) [SMTConfig]
    ps) in
                   Either String ([String], SBVProverConfig)
    -> IO (Either String ([String], SBVProverConfig))
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (([String], SBVProverConfig)
    -> Either String ([String], SBVProverConfig)
    forall a b. b -> Either a b
    Right ([String
    msg], [SMTConfig] -> SBVProverConfig
    SBVPortfolio [SMTConfig]
    ps))

        -- special case, we search for two different yices binaries
      | String
    nm String -> [String] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [String
    "yices",String
    "sbv-yices"] = SMTConfig
    -> [String] -> IO (Either String ([String], SBVProverConfig))
    forall {a}.
    SMTConfig -> [String] -> IO (Either a ([String], SBVProverConfig))
    tryCfgs SMTConfig
    SBV.yices [String
    "yices-smt2", String
    "yices_smt2"]

      | Bool
    otherwise =
        case String -> [(String, SMTConfig)] -> Maybe SMTConfig
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup String
    nm [(String, SMTConfig)]
    proverConfigs of
          Just SMTConfig
    cfg -> SMTConfig
    -> [String] -> IO (Either String ([String], SBVProverConfig))
    forall {a}.
    SMTConfig -> [String] -> IO (Either a ([String], SBVProverConfig))
    tryCfgs SMTConfig
    cfg []
          Maybe SMTConfig
    Nothing  -> Either String ([String], SBVProverConfig)
    -> IO (Either String ([String], SBVProverConfig))
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (String -> Either String ([String], SBVProverConfig)
    forall a b. a -> Either a b
    Left (String
    "unknown solver name: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    nm))

      where
      tryCfgs :: SMTConfig -> [String] -> IO (Either a ([String], SBVProverConfig))
    tryCfgs SMTConfig
    cfg (String
    e:[String]
    es) =
        do let cfg' :: SMTConfig
    cfg' = SMTConfig
    cfg{ solver :: SMTSolver
    SBV.solver = (SMTConfig -> SMTSolver
    SBV.solver SMTConfig
    cfg){ executable :: String
    SBV.executable = String
    e } }
           Bool
    ok <- SMTConfig -> IO Bool
    SBV.sbvCheckSolverInstallation SMTConfig
    cfg'
           if Bool
    ok then Either a ([String], SBVProverConfig)
    -> IO (Either a ([String], SBVProverConfig))
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (([String], SBVProverConfig) -> Either a ([String], SBVProverConfig)
    forall a b. b -> Either a b
    Right ([], SMTConfig -> SBVProverConfig
    SBVProverConfig SMTConfig
    cfg')) else SMTConfig -> [String] -> IO (Either a ([String], SBVProverConfig))
    tryCfgs SMTConfig
    cfg [String]
    es

      tryCfgs SMTConfig
    cfg [] =
        do Bool
    ok <- SMTConfig -> IO Bool
    SBV.sbvCheckSolverInstallation SMTConfig
    cfg
           Either a ([String], SBVProverConfig)
    -> IO (Either a ([String], SBVProverConfig))
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (([String], SBVProverConfig) -> Either a ([String], SBVProverConfig)
    forall a b. b -> Either a b
    Right (Bool -> [String]
    ws Bool
    ok, SMTConfig -> SBVProverConfig
    SBVProverConfig SMTConfig
    cfg))

      ws :: Bool -> [String]
    ws Bool
    ok = if Bool
    ok then [] else [String]
    notFound
      notFound :: [String]
    notFound = [String
    "Warning: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " installation not found"]

    satSMTResults :: SBV.SatResult -> [SBV.SMTResult]
    satSMTResults :: SatResult -> [SMTResult]
    satSMTResults (SBV.SatResult SMTResult
    r) = [SMTResult
    r]

    allSatSMTResults :: SBV.AllSatResult -> [SBV.SMTResult]
    #if MIN_VERSION_sbv(8,8,0)
    allSatSMTResults :: AllSatResult -> [SMTResult]
    allSatSMTResults (SBV.AllSatResult {allSatResults :: AllSatResult -> [SMTResult]
    allSatResults = [SMTResult]
    rs}) = [SMTResult]
    rs
    #else
    allSatSMTResults (SBV.AllSatResult (_, _, _, rs)) = rs
    #endif

    thmSMTResults :: SBV.ThmResult -> [SBV.SMTResult]
    thmSMTResults :: ThmResult -> [SMTResult]
    thmSMTResults (SBV.ThmResult SMTResult
    r) = [SMTResult
    r]

    proverError :: String -> M.ModuleCmd (Maybe String, ProverResult)
    proverError :: String -> ModuleCmd (Maybe String, ProverResult)
    proverError String
    msg ModuleInput IO
    minp =
      ModuleRes (Maybe String, ProverResult)
    -> IO (ModuleRes (Maybe String, ProverResult))
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (((Maybe String, ProverResult), ModuleEnv)
    -> Either ModuleError ((Maybe String, ProverResult), ModuleEnv)
    forall a b. b -> Either a b
    Right ((Maybe String
    forall a. Maybe a
    Nothing, String -> ProverResult
    ProverError String
    msg), ModuleInput IO -> ModuleEnv
    forall (m :: * -> *). ModuleInput m -> ModuleEnv
    M.minpModuleEnv ModuleInput IO
    minp), [])

    isFailedResult :: [SBV.SMTResult] -> Maybe String
    isFailedResult :: [SMTResult] -> Maybe String
    isFailedResult [] = String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "Solver returned no results!"
    isFailedResult (SMTResult
    r:[SMTResult]
    _) =
      case SMTResult
    r of
        SBV.Unknown SMTConfig
    _cfg SMTReasonUnknown
    rsn  -> String -> Maybe String
    forall a. a -> Maybe a
    Just (String
    "Solver returned UNKNOWN " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SMTReasonUnknown -> String
    forall a. Show a => a -> String
    show SMTReasonUnknown
    rsn)
        SBV.ProofError SMTConfig
    _ [String]
    ms Maybe SMTResult
    _ -> String -> Maybe String
    forall a. a -> Maybe a
    Just ([String] -> String
    unlines (String
    "Solver error" String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    ms))
        SMTResult
    _ -> Maybe String
    forall a. Maybe a
    Nothing

    runSingleProver ::
      ProverCommand ->
      (String -> IO ()) ->
      SBV.SMTConfig ->
      (SBV.SMTConfig -> SBV.Symbolic SBV.SVal -> IO res) ->
      (res -> [SBV.SMTResult]) ->
      SBV.Symbolic SBV.SVal ->
      IO (Maybe String, [SBV.SMTResult])
    runSingleProver :: forall res.
    ProverCommand
    -> (String -> IO ())
    -> SMTConfig
    -> (SMTConfig -> Symbolic SVal -> IO res)
    -> (res -> [SMTResult])
    -> Symbolic SVal
    -> IO (Maybe String, [SMTResult])
    runSingleProver ProverCommand{Bool
    String
    [DeclGroup]
    Maybe String
    IORef ProverStats
    Schema
    Expr
    QueryType
    pcQueryType :: QueryType
    pcProverName :: String
    pcVerbose :: Bool
    pcValidate :: Bool
    pcProverStats :: IORef ProverStats
    pcExtraDecls :: [DeclGroup]
    pcSmtFile :: Maybe String
    pcExpr :: Expr
    pcSchema :: Schema
    pcIgnoreSafety :: Bool
    pcQueryType :: ProverCommand -> QueryType
    pcProverName :: ProverCommand -> String
    pcVerbose :: ProverCommand -> Bool
    pcValidate :: ProverCommand -> Bool
    pcProverStats :: ProverCommand -> IORef ProverStats
    pcExtraDecls :: ProverCommand -> [DeclGroup]
    pcSmtFile :: ProverCommand -> Maybe String
    pcExpr :: ProverCommand -> Expr
    pcSchema :: ProverCommand -> Schema
    pcIgnoreSafety :: ProverCommand -> Bool
    ..} String -> IO ()
    lPutStrLn SMTConfig
    prover SMTConfig -> Symbolic SVal -> IO res
    callSolver res -> [SMTResult]
    processResult Symbolic SVal
    e = do
       Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    pcVerbose (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $
         String -> IO ()
    lPutStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Trying proof with " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++
                                   Solver -> String
    forall a. Show a => a -> String
    show (SMTSolver -> Solver
    SBV.name (SMTConfig -> SMTSolver
    SBV.solver SMTConfig
    prover))
       res
    res <- SMTConfig -> Symbolic SVal -> IO res
    callSolver SMTConfig
    prover Symbolic SVal
    e

       Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    pcVerbose (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $
         String -> IO ()
    lPutStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Got result from " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++
                                   Solver -> String
    forall a. Show a => a -> String
    show (SMTSolver -> Solver
    SBV.name (SMTConfig -> SMTSolver
    SBV.solver SMTConfig
    prover))
       (Maybe String, [SMTResult]) -> IO (Maybe String, [SMTResult])
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> Maybe String
    forall a. a -> Maybe a
    Just (Solver -> String
    forall a. Show a => a -> String
    show (SMTSolver -> Solver
    SBV.name (SMTConfig -> SMTSolver
    SBV.solver SMTConfig
    prover))), res -> [SMTResult]
    processResult res
    res)

    runMultiProvers ::
      ProverCommand ->
      (String -> IO ()) ->
      [SBV.SMTConfig] ->
      (SBV.SMTConfig -> SBV.Symbolic SBV.SVal -> IO res) ->
      (res -> [SBV.SMTResult]) ->
      SBV.Symbolic SBV.SVal ->
      IO (Maybe String, [SBV.SMTResult])
    runMultiProvers :: forall res.
    ProverCommand
    -> (String -> IO ())
    -> [SMTConfig]
    -> (SMTConfig -> Symbolic SVal -> IO res)
    -> (res -> [SMTResult])
    -> Symbolic SVal
    -> IO (Maybe String, [SMTResult])
    runMultiProvers ProverCommand
    pc String -> IO ()
    lPutStrLn [SMTConfig]
    provers SMTConfig -> Symbolic SVal -> IO res
    callSolver res -> [SMTResult]
    processResult Symbolic SVal
    e = do
      [Async (Maybe String, [SMTResult])]
    as <- (IO (Maybe String, [SMTResult])
     -> IO (Async (Maybe String, [SMTResult])))
    -> [IO (Maybe String, [SMTResult])]
    -> IO [Async (Maybe String, [SMTResult])]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM IO (Maybe String, [SMTResult])
    -> IO (Async (Maybe String, [SMTResult]))
    forall a. IO a -> IO (Async a)
    async [ ProverCommand
    -> (String -> IO ())
    -> SMTConfig
    -> (SMTConfig -> Symbolic SVal -> IO res)
    -> (res -> [SMTResult])
    -> Symbolic SVal
    -> IO (Maybe String, [SMTResult])
    forall res.
    ProverCommand
    -> (String -> IO ())
    -> SMTConfig
    -> (SMTConfig -> Symbolic SVal -> IO res)
    -> (res -> [SMTResult])
    -> Symbolic SVal
    -> IO (Maybe String, [SMTResult])
    runSingleProver ProverCommand
    pc String -> IO ()
    lPutStrLn SMTConfig
    p SMTConfig -> Symbolic SVal -> IO res
    callSolver res -> [SMTResult]
    processResult Symbolic SVal
    e
                       | SMTConfig
    p <- [SMTConfig]
    provers
                       ]
      [Either SomeException (Maybe String, String)]
    -> [Async (Maybe String, [SMTResult])]
    -> IO (Maybe String, [SMTResult])
    waitForResults [] [Async (Maybe String, [SMTResult])]
    as

     where
     waitForResults :: [Either SomeException (Maybe String, String)]
    -> [Async (Maybe String, [SMTResult])]
    -> IO (Maybe String, [SMTResult])
    waitForResults [Either SomeException (Maybe String, String)]
    exs [] = SBVPortfolioException -> IO (Maybe String, [SMTResult])
    forall a e. Exception e => e -> a
    X.throw ([Either SomeException (Maybe String, String)]
    -> SBVPortfolioException
    SBVPortfolioException [Either SomeException (Maybe String, String)]
    exs)
     waitForResults [Either SomeException (Maybe String, String)]
    exs [Async (Maybe String, [SMTResult])]
    as =
       do (Async (Maybe String, [SMTResult])
    winner, Either SomeException (Maybe String, [SMTResult])
    result) <- [Async (Maybe String, [SMTResult])]
    -> IO
         (Async (Maybe String, [SMTResult]),
          Either SomeException (Maybe String, [SMTResult]))
    forall a. [Async a] -> IO (Async a, Either SomeException a)
    waitAnyCatch [Async (Maybe String, [SMTResult])]
    as
          let others :: [Async (Maybe String, [SMTResult])]
    others = (Async (Maybe String, [SMTResult]) -> Bool)
    -> [Async (Maybe String, [SMTResult])]
    -> [Async (Maybe String, [SMTResult])]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Async (Maybe String, [SMTResult])
    -> Async (Maybe String, [SMTResult]) -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Async (Maybe String, [SMTResult])
    winner) [Async (Maybe String, [SMTResult])]
    as
          case Either SomeException (Maybe String, [SMTResult])
    result of
            Left SomeException
    ex ->
              [Either SomeException (Maybe String, String)]
    -> [Async (Maybe String, [SMTResult])]
    -> IO (Maybe String, [SMTResult])
    waitForResults (SomeException -> Either SomeException (Maybe String, String)
    forall a b. a -> Either a b
    Left SomeException
    exEither SomeException (Maybe String, String)
    -> [Either SomeException (Maybe String, String)]
    -> [Either SomeException (Maybe String, String)]
    forall a. a -> [a] -> [a]
    :[Either SomeException (Maybe String, String)]
    exs) [Async (Maybe String, [SMTResult])]
    others
            Right r :: (Maybe String, [SMTResult])
    r@(Maybe String
    nm, [SMTResult]
    rs)
              | Just String
    msg <- [SMTResult] -> Maybe String
    isFailedResult [SMTResult]
    rs ->
                  [Either SomeException (Maybe String, String)]
    -> [Async (Maybe String, [SMTResult])]
    -> IO (Maybe String, [SMTResult])
    waitForResults ((Maybe String, String)
    -> Either SomeException (Maybe String, String)
    forall a b. b -> Either a b
    Right (Maybe String
    nm, String
    msg) Either SomeException (Maybe String, String)
    -> [Either SomeException (Maybe String, String)]
    -> [Either SomeException (Maybe String, String)]
    forall a. a -> [a] -> [a]
    : [Either SomeException (Maybe String, String)]
    exs) [Async (Maybe String, [SMTResult])]
    others
              | Bool
    otherwise ->
                  do [Async (Maybe String, [SMTResult])]
    -> (Async (Maybe String, [SMTResult]) -> IO ()) -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [Async (Maybe String, [SMTResult])]
    others (\Async (Maybe String, [SMTResult])
    a -> ThreadId -> ExitCode -> IO ()
    forall e. Exception e => ThreadId -> e -> IO ()
    X.throwTo (Async (Maybe String, [SMTResult]) -> ThreadId
    forall a. Async a -> ThreadId
    asyncThreadId Async (Maybe String, [SMTResult])
    a) ExitCode
    ExitSuccess)
                     (Maybe String, [SMTResult]) -> IO (Maybe String, [SMTResult])
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe String, [SMTResult])
    r

    -- | Select the appropriate solver or solvers from the given prover command,
    --   and invoke those solvers on the given symbolic value.
    runProver ::
      SBVProverConfig ->
      ProverCommand ->
      (String -> IO ()) ->
      SBV.Symbolic SBV.SVal ->
      IO (Maybe String, [SBV.SMTResult])
    runProver :: SBVProverConfig
    -> ProverCommand
    -> (String -> IO ())
    -> Symbolic SVal
    -> IO (Maybe String, [SMTResult])
    runProver SBVProverConfig
    proverConfig pc :: ProverCommand
    pc@ProverCommand{Bool
    String
    [DeclGroup]
    Maybe String
    IORef ProverStats
    Schema
    Expr
    QueryType
    pcQueryType :: ProverCommand -> QueryType
    pcProverName :: ProverCommand -> String
    pcVerbose :: ProverCommand -> Bool
    pcValidate :: ProverCommand -> Bool
    pcProverStats :: ProverCommand -> IORef ProverStats
    pcExtraDecls :: ProverCommand -> [DeclGroup]
    pcSmtFile :: ProverCommand -> Maybe String
    pcExpr :: ProverCommand -> Expr
    pcSchema :: ProverCommand -> Schema
    pcIgnoreSafety :: ProverCommand -> Bool
    pcQueryType :: QueryType
    pcProverName :: String
    pcVerbose :: Bool
    pcValidate :: Bool
    pcProverStats :: IORef ProverStats
    pcExtraDecls :: [DeclGroup]
    pcSmtFile :: Maybe String
    pcExpr :: Expr
    pcSchema :: Schema
    pcIgnoreSafety :: Bool
    ..} String -> IO ()
    lPutStrLn Symbolic SVal
    x =
      do let mSatNum :: Maybe Int
    mSatNum = case QueryType
    pcQueryType of
                         SatQuery (SomeSat Int
    n) -> Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    n
                         SatQuery SatNum
    AllSat -> Maybe Int
    forall a. Maybe a
    Nothing
                         QueryType
    ProveQuery -> Maybe Int
    forall a. Maybe a
    Nothing
                         QueryType
    SafetyQuery -> Maybe Int
    forall a. Maybe a
    Nothing

         case SBVProverConfig
    proverConfig of
           SBVPortfolio [SMTConfig]
    ps ->
             let ps' :: [SMTConfig]
    ps' = [ SMTConfig
    p { transcript :: Maybe String
    SBV.transcript = Maybe String
    pcSmtFile
                           , timing :: Timing
    SBV.timing = IORef ProverStats -> Timing
    SaveTiming IORef ProverStats
    pcProverStats
                           , verbose :: Bool
    SBV.verbose = Bool
    pcVerbose
                           , validateModel :: Bool
    SBV.validateModel = Bool
    pcValidate
                           }
                       | SMTConfig
    p <- [SMTConfig]
    ps
                       ] in

              case QueryType
    pcQueryType of
                QueryType
    ProveQuery  -> ProverCommand
    -> (String -> IO ())
    -> [SMTConfig]
    -> (SMTConfig -> Symbolic SVal -> IO ThmResult)
    -> (ThmResult -> [SMTResult])
    -> Symbolic SVal
    -> IO (Maybe String, [SMTResult])
    forall res.
    ProverCommand
    -> (String -> IO ())
    -> [SMTConfig]
    -> (SMTConfig -> Symbolic SVal -> IO res)
    -> (res -> [SMTResult])
    -> Symbolic SVal
    -> IO (Maybe String, [SMTResult])
    runMultiProvers ProverCommand
    pc String -> IO ()
    lPutStrLn [SMTConfig]
    ps' SMTConfig -> Symbolic SVal -> IO ThmResult
    SBV.proveWith ThmResult -> [SMTResult]
    thmSMTResults Symbolic SVal
    x
                QueryType
    SafetyQuery -> ProverCommand
    -> (String -> IO ())
    -> [SMTConfig]
    -> (SMTConfig -> Symbolic SVal -> IO ThmResult)
    -> (ThmResult -> [SMTResult])
    -> Symbolic SVal
    -> IO (Maybe String, [SMTResult])
    forall res.
    ProverCommand
    -> (String -> IO ())
    -> [SMTConfig]
    -> (SMTConfig -> Symbolic SVal -> IO res)
    -> (res -> [SMTResult])
    -> Symbolic SVal
    -> IO (Maybe String, [SMTResult])
    runMultiProvers ProverCommand
    pc String -> IO ()
    lPutStrLn [SMTConfig]
    ps' SMTConfig -> Symbolic SVal -> IO ThmResult
    SBV.proveWith ThmResult -> [SMTResult]
    thmSMTResults Symbolic SVal
    x
                SatQuery (SomeSat Int
    1) -> ProverCommand
    -> (String -> IO ())
    -> [SMTConfig]
    -> (SMTConfig -> Symbolic SVal -> IO SatResult)
    -> (SatResult -> [SMTResult])
    -> Symbolic SVal
    -> IO (Maybe String, [SMTResult])
    forall res.
    ProverCommand
    -> (String -> IO ())
    -> [SMTConfig]
    -> (SMTConfig -> Symbolic SVal -> IO res)
    -> (res -> [SMTResult])
    -> Symbolic SVal
    -> IO (Maybe String, [SMTResult])
    runMultiProvers ProverCommand
    pc String -> IO ()
    lPutStrLn [SMTConfig]
    ps' SMTConfig -> Symbolic SVal -> IO SatResult
    SBV.satWith SatResult -> [SMTResult]
    satSMTResults Symbolic SVal
    x
                QueryType
    _ -> (Maybe String, [SMTResult]) -> IO (Maybe String, [SMTResult])
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe String
    forall a. Maybe a
    Nothing,
                       [SMTConfig -> [String] -> Maybe SMTResult -> SMTResult
    SBV.ProofError SMTConfig
    p
                         [String
    ":sat with option prover=any requires option satNum=1"]
                         Maybe SMTResult
    forall a. Maybe a
    Nothing
                       | SMTConfig
    p <- [SMTConfig]
    ps])

           SBVProverConfig SMTConfig
    p ->
             let p' :: SMTConfig
    p' = SMTConfig
    p { transcript :: Maybe String
    SBV.transcript = Maybe String
    pcSmtFile
                        , allSatMaxModelCount :: Maybe Int
    SBV.allSatMaxModelCount = Maybe Int
    mSatNum
                        , timing :: Timing
    SBV.timing = IORef ProverStats -> Timing
    SaveTiming IORef ProverStats
    pcProverStats
                        , verbose :: Bool
    SBV.verbose = Bool
    pcVerbose
                        , validateModel :: Bool
    SBV.validateModel = Bool
    pcValidate
                        } in
              case QueryType
    pcQueryType of
                QueryType
    ProveQuery  -> ProverCommand
    -> (String -> IO ())
    -> SMTConfig
    -> (SMTConfig -> Symbolic SVal -> IO ThmResult)
    -> (ThmResult -> [SMTResult])
    -> Symbolic SVal
    -> IO (Maybe String, [SMTResult])
    forall res.
    ProverCommand
    -> (String -> IO ())
    -> SMTConfig
    -> (SMTConfig -> Symbolic SVal -> IO res)
    -> (res -> [SMTResult])
    -> Symbolic SVal
    -> IO (Maybe String, [SMTResult])
    runSingleProver ProverCommand
    pc String -> IO ()
    lPutStrLn SMTConfig
    p' SMTConfig -> Symbolic SVal -> IO ThmResult
    SBV.proveWith ThmResult -> [SMTResult]
    thmSMTResults Symbolic SVal
    x
                QueryType
    SafetyQuery -> ProverCommand
    -> (String -> IO ())
    -> SMTConfig
    -> (SMTConfig -> Symbolic SVal -> IO ThmResult)
    -> (ThmResult -> [SMTResult])
    -> Symbolic SVal
    -> IO (Maybe String, [SMTResult])
    forall res.
    ProverCommand
    -> (String -> IO ())
    -> SMTConfig
    -> (SMTConfig -> Symbolic SVal -> IO res)
    -> (res -> [SMTResult])
    -> Symbolic SVal
    -> IO (Maybe String, [SMTResult])
    runSingleProver ProverCommand
    pc String -> IO ()
    lPutStrLn SMTConfig
    p' SMTConfig -> Symbolic SVal -> IO ThmResult
    SBV.proveWith ThmResult -> [SMTResult]
    thmSMTResults Symbolic SVal
    x
                SatQuery (SomeSat Int
    1) -> ProverCommand
    -> (String -> IO ())
    -> SMTConfig
    -> (SMTConfig -> Symbolic SVal -> IO SatResult)
    -> (SatResult -> [SMTResult])
    -> Symbolic SVal
    -> IO (Maybe String, [SMTResult])
    forall res.
    ProverCommand
    -> (String -> IO ())
    -> SMTConfig
    -> (SMTConfig -> Symbolic SVal -> IO res)
    -> (res -> [SMTResult])
    -> Symbolic SVal
    -> IO (Maybe String, [SMTResult])
    runSingleProver ProverCommand
    pc String -> IO ()
    lPutStrLn SMTConfig
    p' SMTConfig -> Symbolic SVal -> IO SatResult
    SBV.satWith SatResult -> [SMTResult]
    satSMTResults Symbolic SVal
    x
                SatQuery SatNum
    _           -> ProverCommand
    -> (String -> IO ())
    -> SMTConfig
    -> (SMTConfig -> Symbolic SVal -> IO AllSatResult)
    -> (AllSatResult -> [SMTResult])
    -> Symbolic SVal
    -> IO (Maybe String, [SMTResult])
    forall res.
    ProverCommand
    -> (String -> IO ())
    -> SMTConfig
    -> (SMTConfig -> Symbolic SVal -> IO res)
    -> (res -> [SMTResult])
    -> Symbolic SVal
    -> IO (Maybe String, [SMTResult])
    runSingleProver ProverCommand
    pc String -> IO ()
    lPutStrLn SMTConfig
    p' SMTConfig -> Symbolic SVal -> IO AllSatResult
    SBV.allSatWith AllSatResult -> [SMTResult]
    allSatSMTResults Symbolic SVal
    x

    -- | Prepare a symbolic query by symbolically simulating the expression found in
    --   the @ProverQuery@.  The result will either be an error or a list of the types
    --   of the symbolic inputs and the symbolic value to supply to the solver.
    --
    --   Note that the difference between sat and prove queries is reflected later
    --   in `runProver` where we call different SBV methods depending on the mode,
    --   so we do _not_ negate the goal here.  Moreover, assumptions are added
    --   using conjunction for sat queries and implication for prove queries.
    --
    --   For safety properties, we want to add them as an additional goal
    --   when we do prove queries, and an additional assumption when we do
    --   sat queries.  In both cases, the safety property is combined with
    --   the main goal via a conjunction.
    prepareQuery ::
      Eval.EvalOpts ->
      ProverCommand ->
      M.ModuleT IO (Either String ([FinType], SBV.Symbolic SBV.SVal))
    prepareQuery :: EvalOpts
    -> ProverCommand
    -> ModuleT IO (Either String ([FinType], Symbolic SVal))
    prepareQuery EvalOpts
    evo ProverCommand{Bool
    String
    [DeclGroup]
    Maybe String
    IORef ProverStats
    Schema
    Expr
    QueryType
    pcQueryType :: ProverCommand -> QueryType
    pcProverName :: ProverCommand -> String
    pcVerbose :: ProverCommand -> Bool
    pcValidate :: ProverCommand -> Bool
    pcProverStats :: ProverCommand -> IORef ProverStats
    pcExtraDecls :: ProverCommand -> [DeclGroup]
    pcSmtFile :: ProverCommand -> Maybe String
    pcExpr :: ProverCommand -> Expr
    pcSchema :: ProverCommand -> Schema
    pcIgnoreSafety :: ProverCommand -> Bool
    pcQueryType :: QueryType
    pcProverName :: String
    pcVerbose :: Bool
    pcValidate :: Bool
    pcProverStats :: IORef ProverStats
    pcExtraDecls :: [DeclGroup]
    pcSmtFile :: Maybe String
    pcExpr :: Expr
    pcSchema :: Schema
    pcIgnoreSafety :: Bool
    ..} =
      do Map PrimIdent Expr
    ds <- do (ModulePath
    _mp, TCTopEntity
    ent) <- Bool -> ImportSource -> ModuleM (ModulePath, TCTopEntity)
    M.loadModuleFrom Bool
    True (ModName -> ImportSource
    M.FromModule ModName
    preludeReferenceName)
                  let m :: Module
    m = TCTopEntity -> Module
    tcTopEntityToModule TCTopEntity
    ent

                  let decls :: [DeclGroup]
    decls = Module -> [DeclGroup]
    forall mname. ModuleG mname -> [DeclGroup]
    mDecls Module
    m
                  let nms :: [Name]
    nms = (Name, IfaceDecl) -> Name
    forall a b. (a, b) -> a
    fst ((Name, IfaceDecl) -> Name) -> [(Name, IfaceDecl)] -> [Name]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Map Name IfaceDecl -> [(Name, IfaceDecl)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (IfaceDecls -> Map Name IfaceDecl
    M.ifDecls (IfaceG ModName -> IfaceDecls
    forall name. IfaceG name -> IfaceDecls
    M.ifDefines (Module -> IfaceG ModName
    forall name. ModuleG name -> IfaceG name
    M.genIface Module
    m)))
                  let ds :: Map PrimIdent Expr
    ds = [(PrimIdent, Expr)] -> Map PrimIdent Expr
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [ (Text -> PrimIdent
    prelPrim (Ident -> Text
    identText (Name -> Ident
    M.nameIdent Name
    nm)), Expr -> [DeclGroup] -> Expr
    EWhere (Name -> Expr
    EVar Name
    nm) [DeclGroup]
    decls) | Name
    nm <- [Name]
    nms ]
                  Map PrimIdent Expr -> ModuleT IO (Map PrimIdent Expr)
    forall a. a -> ModuleT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Map PrimIdent Expr
    ds

         ModuleEnv
    modEnv <- ModuleT IO ModuleEnv
    forall (m :: * -> *). Monad m => ModuleT m ModuleEnv
    M.getModuleEnv
         let extDgs :: [DeclGroup]
    extDgs = ModuleEnv -> [DeclGroup]
    M.allDeclGroups ModuleEnv
    modEnv [DeclGroup] -> [DeclGroup] -> [DeclGroup]
    forall a. [a] -> [a] -> [a]
    ++ [DeclGroup]
    pcExtraDecls

         Bool
    callStacks <- ModuleT IO Bool
    forall (m :: * -> *). Monad m => ModuleT m Bool
    M.getCallStacks
         let ?callStacks = ?callStacks::Bool
    Bool
    callStacks

         IO EvalOpts
    getEOpts <- ModuleM (IO EvalOpts)
    M.getEvalOptsAction

         Map Name Newtype
    ntEnv <- ModuleM (Map Name Newtype)
    M.getNewtypes

         -- The `addAsm` function is used to combine assumptions that
         -- arise from the types of symbolic variables (e.g. Z n values
         -- are assumed to be integers in the range `0 <= x < n`) with
         -- the main content of the query.  We use conjunction or implication
         -- depending on the type of query.
         let addAsm :: SVal -> SVal -> SVal
    addAsm = case QueryType
    pcQueryType of
               QueryType
    ProveQuery  -> \SVal
    x SVal
    y -> SVal -> SVal -> SVal
    SBV.svOr (SVal -> SVal
    SBV.svNot SVal
    x) SVal
    y
               QueryType
    SafetyQuery -> \SVal
    x SVal
    y -> SVal -> SVal -> SVal
    SBV.svOr (SVal -> SVal
    SBV.svNot SVal
    x) SVal
    y
               SatQuery SatNum
    _ -> \SVal
    x SVal
    y -> SVal -> SVal -> SVal
    SBV.svAnd SVal
    x SVal
    y

         case QueryType -> Schema -> Either String [FinType]
    predArgTypes QueryType
    pcQueryType Schema
    pcSchema of
           Left String
    msg -> Either String ([FinType], Symbolic SVal)
    -> ModuleT IO (Either String ([FinType], Symbolic SVal))
    forall a. a -> ModuleT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> Either String ([FinType], Symbolic SVal)
    forall a b. a -> Either a b
    Left String
    msg)
           Right [FinType]
    ts -> IO (Either String ([FinType], Symbolic SVal))
    -> ModuleT IO (Either String ([FinType], Symbolic SVal))
    forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
    M.io (IO (Either String ([FinType], Symbolic SVal))
     -> ModuleT IO (Either String ([FinType], Symbolic SVal)))
    -> IO (Either String ([FinType], Symbolic SVal))
    -> ModuleT IO (Either String ([FinType], Symbolic SVal))
    forall a b. (a -> b) -> a -> b
    $
             do Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    pcVerbose (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Logger -> String -> IO ()
    logPutStrLn (EvalOpts -> Logger
    Eval.evalLogger EvalOpts
    evo) String
    "Simulating..."
                Either String ([FinType], Symbolic SVal)
    -> IO (Either String ([FinType], Symbolic SVal))
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Either String ([FinType], Symbolic SVal)
     -> IO (Either String ([FinType], Symbolic SVal)))
    -> Either String ([FinType], Symbolic SVal)
    -> IO (Either String ([FinType], Symbolic SVal))
    forall a b. (a -> b) -> a -> b
    $ ([FinType], Symbolic SVal)
    -> Either String ([FinType], Symbolic SVal)
    forall a b. b -> Either a b
    Right (([FinType], Symbolic SVal)
     -> Either String ([FinType], Symbolic SVal))
    -> ([FinType], Symbolic SVal)
    -> Either String ([FinType], Symbolic SVal)
    forall a b. (a -> b) -> a -> b
    $ ([FinType]
    ts,
                  do State
    sbvState <- SymbolicT IO State
    forall (m :: * -> *). MonadSymbolic m => m State
    SBV.symbolicEnv
                     MVar State
    stateMVar <- IO (MVar State) -> SymbolicT IO (MVar State)
    forall a. IO a -> SymbolicT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (State -> IO (MVar State)
    forall a. a -> IO (MVar a)
    newMVar State
    sbvState)
                     MVar SVal
    defRelsVar <- IO (MVar SVal) -> SymbolicT IO (MVar SVal)
    forall a. IO a -> SymbolicT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (SVal -> IO (MVar SVal)
    forall a. a -> IO (MVar a)
    newMVar SVal
    SBV.svTrue)
                     let sym :: SBV
    sym = MVar State -> MVar SVal -> SBV
    SBV MVar State
    stateMVar MVar SVal
    defRelsVar
                     let tbl :: Map PrimIdent (Prim SBV)
    tbl = SBV -> IO EvalOpts -> Map PrimIdent (Prim SBV)
    primTable SBV
    sym IO EvalOpts
    getEOpts
                     let ?evalPrim = \PrimIdent
    i -> (Prim SBV -> Either Expr (Prim SBV)
    forall a b. b -> Either a b
    Right (Prim SBV -> Either Expr (Prim SBV))
    -> Maybe (Prim SBV) -> Maybe (Either Expr (Prim SBV))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PrimIdent -> Map PrimIdent (Prim SBV) -> Maybe (Prim SBV)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup PrimIdent
    i Map PrimIdent (Prim SBV)
    tbl) Maybe (Either Expr (Prim SBV))
    -> Maybe (Either Expr (Prim SBV)) -> Maybe (Either Expr (Prim SBV))
    forall a. Maybe a -> Maybe a -> Maybe a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|>
                                           (Expr -> Either Expr (Prim SBV)
    forall a b. a -> Either a b
    Left (Expr -> Either Expr (Prim SBV))
    -> Maybe Expr -> Maybe (Either Expr (Prim SBV))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PrimIdent -> Map PrimIdent Expr -> Maybe Expr
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup PrimIdent
    i Map PrimIdent Expr
    ds)
                     let ?range = ?range::Range
    Range
    emptyRange

                     -- Compute the symbolic inputs, and any domain constraints needed
                     -- according to their types.
                     [SBVEval (GenValue SBV)]
    args <- (VarShape SBV -> SBVEval (GenValue SBV))
    -> [VarShape SBV] -> [SBVEval (GenValue SBV)]
    forall a b. (a -> b) -> [a] -> [b]
    map (GenValue SBV -> SBVEval (GenValue SBV)
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (GenValue SBV -> SBVEval (GenValue SBV))
    -> (VarShape SBV -> GenValue SBV)
    -> VarShape SBV
    -> SBVEval (GenValue SBV)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBV -> VarShape SBV -> GenValue SBV
    forall sym. Backend sym => sym -> VarShape sym -> GenValue sym
    varShapeToValue SBV
    sym) ([VarShape SBV] -> [SBVEval (GenValue SBV)])
    -> SymbolicT IO [VarShape SBV]
    -> SymbolicT IO [SBVEval (GenValue SBV)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                         IO [VarShape SBV] -> SymbolicT IO [VarShape SBV]
    forall a. IO a -> SymbolicT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO ((FinType -> IO (VarShape SBV)) -> [FinType] -> IO [VarShape SBV]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (FreshVarFns SBV -> FinType -> IO (VarShape SBV)
    forall sym.
    Backend sym =>
    FreshVarFns sym -> FinType -> IO (VarShape sym)
    freshVar (SBV -> FreshVarFns SBV
    sbvFreshFns SBV
    sym)) [FinType]
    ts)
                     -- Run the main symbolic computation.  First we populate the
                     -- evaluation environment, then we compute the value, finally
                     -- we apply it to the symbolic inputs.
                     (SVal
    safety,SVal
    b) <- SBVEval SVal -> SymbolicT IO (SVal, SVal)
    forall (m :: * -> *) a. MonadIO m => SBVEval a -> m (SVal, a)
    doSBVEval (SBVEval SVal -> SymbolicT IO (SVal, SVal))
    -> SBVEval SVal -> SymbolicT IO (SVal, SVal)
    forall a b. (a -> b) -> a -> b
    $
                         do GenEvalEnv SBV
    env <- SBV -> [DeclGroup] -> GenEvalEnv SBV -> SEval SBV (GenEvalEnv SBV)
    forall sym.
    EvalPrims sym =>
    sym -> [DeclGroup] -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
    Eval.evalDecls SBV
    sym [DeclGroup]
    extDgs (GenEvalEnv SBV -> SBVEval (GenEvalEnv SBV))
    -> SBVEval (GenEvalEnv SBV) -> SBVEval (GenEvalEnv SBV)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
                                     SBV
    -> Map Name Newtype -> GenEvalEnv SBV -> SEval SBV (GenEvalEnv SBV)
    forall sym.
    EvalPrims sym =>
    sym
    -> Map Name Newtype -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
    Eval.evalNewtypeDecls SBV
    sym Map Name Newtype
    ntEnv GenEvalEnv SBV
    forall a. Monoid a => a
    mempty
                            GenValue SBV
    v <- SBV -> GenEvalEnv SBV -> Expr -> SEval SBV (GenValue SBV)
    forall sym.
    (?range::Range, EvalPrims sym) =>
    sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    Eval.evalExpr SBV
    sym GenEvalEnv SBV
    env Expr
    pcExpr
                            GenValue SBV
    appliedVal <- (GenValue SBV -> SBVEval (GenValue SBV) -> SBVEval (GenValue SBV))
    -> GenValue SBV
    -> [SBVEval (GenValue SBV)]
    -> SBVEval (GenValue SBV)
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM (SBV
    -> GenValue SBV
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (GenValue SBV)
    forall sym.
    Backend sym =>
    sym
    -> GenValue sym
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    Eval.fromVFun SBV
    sym) GenValue SBV
    v [SBVEval (GenValue SBV)]
    args
                            case QueryType
    pcQueryType of
                              QueryType
    SafetyQuery ->
                                do GenValue SBV -> SEval SBV ()
    forall sym. Backend sym => GenValue sym -> SEval sym ()
    Eval.forceValue GenValue SBV
    appliedVal
                                   SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SVal
    SBV.svTrue
                              QueryType
    _ -> SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (GenValue SBV -> SBit SBV
    forall sym. GenValue sym -> SBit sym
    Eval.fromVBit GenValue SBV
    appliedVal)

                     -- Ignore the safety condition if the flag is set and we are not
                     -- doing a safety query
                     let safety' :: SVal
    safety' = case QueryType
    pcQueryType of
                                     QueryType
    SafetyQuery -> SVal
    safety
                                     QueryType
    _ | Bool
    pcIgnoreSafety -> SVal
    SBV.svTrue
                                       | Bool
    otherwise -> SVal
    safety

                     -- "observe" the value of the safety predicate.  This makes its value
                     -- avaliable in the resulting model.
                     String -> SBV Bool -> Symbolic ()
    forall a. SymVal a => String -> SBV a -> Symbolic ()
    SBV.sObserve String
    "safety" (SVal -> SBV Bool
    forall a. SVal -> SBV a
    SBV.SBV SVal
    safety' :: SBV.SBV Bool)

                     -- read any definitional relations that were asserted
                     SVal
    defRels <- IO SVal -> Symbolic SVal
    forall a. IO a -> SymbolicT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (MVar SVal -> IO SVal
    forall a. MVar a -> IO a
    readMVar MVar SVal
    defRelsVar)

                     SVal -> Symbolic SVal
    forall a. a -> SymbolicT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SVal -> SVal -> SVal
    addAsm SVal
    defRels (SVal -> SVal -> SVal
    SBV.svAnd SVal
    safety' SVal
    b)))

    -- | Turn the SMT results from SBV into a @ProverResult@ that is ready for the Cryptol REPL.
    --   There may be more than one result if we made a multi-sat query.
    processResults ::
      ProverCommand ->
      [FinType] {- ^ Types of the symbolic inputs -} ->
      [SBV.SMTResult] {- ^ Results from the solver -} ->
      M.ModuleT IO ProverResult
    processResults :: ProverCommand
    -> [FinType] -> [SMTResult] -> ModuleT IO ProverResult
    processResults ProverCommand{Bool
    String
    [DeclGroup]
    Maybe String
    IORef ProverStats
    Schema
    Expr
    QueryType
    pcQueryType :: ProverCommand -> QueryType
    pcProverName :: ProverCommand -> String
    pcVerbose :: ProverCommand -> Bool
    pcValidate :: ProverCommand -> Bool
    pcProverStats :: ProverCommand -> IORef ProverStats
    pcExtraDecls :: ProverCommand -> [DeclGroup]
    pcSmtFile :: ProverCommand -> Maybe String
    pcExpr :: ProverCommand -> Expr
    pcSchema :: ProverCommand -> Schema
    pcIgnoreSafety :: ProverCommand -> Bool
    pcQueryType :: QueryType
    pcProverName :: String
    pcVerbose :: Bool
    pcValidate :: Bool
    pcProverStats :: IORef ProverStats
    pcExtraDecls :: [DeclGroup]
    pcSmtFile :: Maybe String
    pcExpr :: Expr
    pcSchema :: Schema
    pcIgnoreSafety :: Bool
    ..} [FinType]
    ts [SMTResult]
    results =
     do let isSat :: Bool
    isSat = case QueryType
    pcQueryType of
              QueryType
    ProveQuery -> Bool
    False
              QueryType
    SafetyQuery -> Bool
    False
              SatQuery SatNum
    _ -> Bool
    True

        PrimMap
    prims <- ModuleM PrimMap
    M.getPrimMap

        case [SMTResult]
    results of
           -- allSat can return more than one as long as
           -- they're satisfiable
           (SBV.Satisfiable {} : [SMTResult]
    _) | Bool
    isSat -> do
             [[(TValue, Expr, Value)]]
    tevss <- ((Bool, [(TValue, Expr, Value)]) -> [(TValue, Expr, Value)])
    -> [(Bool, [(TValue, Expr, Value)])] -> [[(TValue, Expr, Value)]]
    forall a b. (a -> b) -> [a] -> [b]
    map (Bool, [(TValue, Expr, Value)]) -> [(TValue, Expr, Value)]
    forall a b. (a, b) -> b
    snd ([(Bool, [(TValue, Expr, Value)])] -> [[(TValue, Expr, Value)]])
    -> ModuleT IO [(Bool, [(TValue, Expr, Value)])]
    -> ModuleT IO [[(TValue, Expr, Value)]]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (SMTResult -> ModuleT IO (Bool, [(TValue, Expr, Value)]))
    -> [SMTResult] -> ModuleT IO [(Bool, [(TValue, Expr, Value)])]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (PrimMap -> SMTResult -> ModuleT IO (Bool, [(TValue, Expr, Value)])
    forall {m :: * -> *}.
    Monad m =>
    PrimMap -> SMTResult -> m (Bool, [(TValue, Expr, Value)])
    mkTevs PrimMap
    prims) [SMTResult]
    results
             ProverResult -> ModuleT IO ProverResult
    forall a. a -> ModuleT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ProverResult -> ModuleT IO ProverResult)
    -> ProverResult -> ModuleT IO ProverResult
    forall a b. (a -> b) -> a -> b
    $ [[(TValue, Expr, Value)]] -> ProverResult
    AllSatResult [[(TValue, Expr, Value)]]
    tevss

           -- prove should only have one counterexample
           [r :: SMTResult
    r@SBV.Satisfiable{}] -> do
             (Bool
    safety, [(TValue, Expr, Value)]
    res) <- PrimMap -> SMTResult -> ModuleT IO (Bool, [(TValue, Expr, Value)])
    forall {m :: * -> *}.
    Monad m =>
    PrimMap -> SMTResult -> m (Bool, [(TValue, Expr, Value)])
    mkTevs PrimMap
    prims SMTResult
    r
             let cexType :: CounterExampleType
    cexType = if Bool
    safety then CounterExampleType
    PredicateFalsified else CounterExampleType
    SafetyViolation
             ProverResult -> ModuleT IO ProverResult
    forall a. a -> ModuleT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ProverResult -> ModuleT IO ProverResult)
    -> ProverResult -> ModuleT IO ProverResult
    forall a b. (a -> b) -> a -> b
    $ CounterExampleType -> [(TValue, Expr, Value)] -> ProverResult
    CounterExample CounterExampleType
    cexType [(TValue, Expr, Value)]
    res

           -- prove returns only one
           [SBV.Unsatisfiable {}] ->
             ProverResult -> ModuleT IO ProverResult
    forall a. a -> ModuleT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ProverResult -> ModuleT IO ProverResult)
    -> ProverResult -> ModuleT IO ProverResult
    forall a b. (a -> b) -> a -> b
    $ [TValue] -> ProverResult
    ThmResult (FinType -> TValue
    unFinType (FinType -> TValue) -> [FinType] -> [TValue]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [FinType]
    ts)

           -- unsat returns empty
           [] -> ProverResult -> ModuleT IO ProverResult
    forall a. a -> ModuleT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ProverResult -> ModuleT IO ProverResult)
    -> ProverResult -> ModuleT IO ProverResult
    forall a b. (a -> b) -> a -> b
    $ [TValue] -> ProverResult
    ThmResult (FinType -> TValue
    unFinType (FinType -> TValue) -> [FinType] -> [TValue]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [FinType]
    ts)

           -- otherwise something is wrong
           [SMTResult]
    _ -> ProverResult -> ModuleT IO ProverResult
    forall a. a -> ModuleT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ProverResult -> ModuleT IO ProverResult)
    -> ProverResult -> ModuleT IO ProverResult
    forall a b. (a -> b) -> a -> b
    $ String -> ProverResult
    ProverError ([SMTResult] -> String
    rshow [SMTResult]
    results)
    #if MIN_VERSION_sbv(10,0,0)
                  where rshow :: [SMTResult] -> String
    rshow | Bool
    isSat = AllSatResult -> String
    forall a. Show a => a -> String
    show (AllSatResult -> String)
    -> ([SMTResult] -> AllSatResult) -> [SMTResult] -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Bool -> Bool -> Bool -> [SMTResult] -> AllSatResult
    SBV.AllSatResult Bool
    False Bool
    False Bool
    False)
                        -- sbv-10.0.0 removes the `allSatHasPrefixExistentials` field
    #elif MIN_VERSION_sbv(8,8,0)
                  where rshow | isSat = show . (SBV.AllSatResult False False False False)
    #else
                  where rshow | isSat = show .  SBV.AllSatResult . (False,False,False,)
    #endif
                              | Bool
    otherwise = ThmResult -> String
    forall a. Show a => a -> String
    show (ThmResult -> String)
    -> ([SMTResult] -> ThmResult) -> [SMTResult] -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SMTResult -> ThmResult
    SBV.ThmResult (SMTResult -> ThmResult)
    -> ([SMTResult] -> SMTResult) -> [SMTResult] -> ThmResult
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [SMTResult] -> SMTResult
    forall a. HasCallStack => [a] -> a
    head

      where
      mkTevs :: PrimMap -> SMTResult -> m (Bool, [(TValue, Expr, Value)])
    mkTevs PrimMap
    prims SMTResult
    result = do
        -- It's a bit fragile, but the value of the safety predicate seems
        -- to always be the first value in the model assignment list.
        let (CV
    safetyCV, [CV]
    cvs) =
              case SMTResult -> Either String (Bool, [CV])
    SBV.getModelAssignment SMTResult
    result of
                Right (Bool
    _, (CV
    safetyCV' : [CV]
    cvs')) -> (CV
    safetyCV', [CV]
    cvs')
                Either String (Bool, [CV])
    _ -> String -> (CV, [CV])
    forall a. HasCallStack => String -> a
    error String
    "processResults: SBV.getModelAssignment failure"
            safety :: Bool
    safety = CV -> Bool
    SBV.cvToBool CV
    safetyCV
            ([VarShape Concrete]
    vs, [CV]
    _) = [FinType] -> [CV] -> ([VarShape Concrete], [CV])
    parseValues [FinType]
    ts [CV]
    cvs
            mdl :: [(TValue, Expr, Value)]
    mdl = PrimMap
    -> [FinType] -> [VarShape Concrete] -> [(TValue, Expr, Value)]
    computeModel PrimMap
    prims [FinType]
    ts [VarShape Concrete]
    vs
        (Bool, [(TValue, Expr, Value)])
    -> m (Bool, [(TValue, Expr, Value)])
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    safety, [(TValue, Expr, Value)]
    mdl)

    -- | Execute a symbolic ':prove' or ':sat' command.
    --
    --   This command returns a pair: the first element is the name of the
    --   solver that completes the given query (if any) along with the result
    --   of executing the query.
    satProve :: SBVProverConfig -> ProverCommand -> M.ModuleCmd (Maybe String, ProverResult)
    satProve :: SBVProverConfig
    -> ProverCommand -> ModuleCmd (Maybe String, ProverResult)
    satProve SBVProverConfig
    proverCfg ProverCommand
    pc =
      (String -> ModuleCmd (Maybe String, ProverResult))
    -> ModuleCmd (Maybe String, ProverResult)
    -> ModuleCmd (Maybe String, ProverResult)
    forall a. (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
    protectStack String -> ModuleCmd (Maybe String, ProverResult)
    proverError (ModuleCmd (Maybe String, ProverResult)
     -> ModuleCmd (Maybe String, ProverResult))
    -> ModuleCmd (Maybe String, ProverResult)
    -> ModuleCmd (Maybe String, ProverResult)
    forall a b. (a -> b) -> a -> b
    $ \ModuleInput IO
    minp ->
      ModuleInput IO
    -> ModuleM (Maybe String, ProverResult)
    -> IO (ModuleRes (Maybe String, ProverResult))
    forall a.
    ModuleInput IO
    -> ModuleM a
    -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
    M.runModuleM ModuleInput IO
    minp (ModuleM (Maybe String, ProverResult)
     -> IO (ModuleRes (Maybe String, ProverResult)))
    -> ModuleM (Maybe String, ProverResult)
    -> IO (ModuleRes (Maybe String, ProverResult))
    forall a b. (a -> b) -> a -> b
    $ do
      EvalOpts
    evo <- IO EvalOpts -> ModuleT IO EvalOpts
    forall a. IO a -> ModuleT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (ModuleInput IO -> IO EvalOpts
    forall (m :: * -> *). ModuleInput m -> m EvalOpts
    M.minpEvalOpts ModuleInput IO
    minp)

      let lPutStrLn :: String -> IO ()
    lPutStrLn = Logger -> String -> IO ()
    logPutStrLn (EvalOpts -> Logger
    Eval.evalLogger EvalOpts
    evo)

      EvalOpts
    -> ProverCommand
    -> ModuleT IO (Either String ([FinType], Symbolic SVal))
    prepareQuery EvalOpts
    evo ProverCommand
    pc ModuleT IO (Either String ([FinType], Symbolic SVal))
    -> (Either String ([FinType], Symbolic SVal)
        -> ModuleM (Maybe String, ProverResult))
    -> ModuleM (Maybe String, ProverResult)
    forall a b. ModuleT IO a -> (a -> ModuleT IO b) -> ModuleT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Left String
    msg -> (Maybe String, ProverResult)
    -> ModuleM (Maybe String, ProverResult)
    forall a. a -> ModuleT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe String
    forall a. Maybe a
    Nothing, String -> ProverResult
    ProverError String
    msg)
        Right ([FinType]
    ts, Symbolic SVal
    q) ->
          do (Maybe String
    firstProver, [SMTResult]
    results) <- IO (Maybe String, [SMTResult])
    -> ModuleT IO (Maybe String, [SMTResult])
    forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
    M.io (SBVProverConfig
    -> ProverCommand
    -> (String -> IO ())
    -> Symbolic SVal
    -> IO (Maybe String, [SMTResult])
    runProver SBVProverConfig
    proverCfg ProverCommand
    pc String -> IO ()
    lPutStrLn Symbolic SVal
    q)
             ProverResult
    esatexprs <- ProverCommand
    -> [FinType] -> [SMTResult] -> ModuleT IO ProverResult
    processResults ProverCommand
    pc [FinType]
    ts [SMTResult]
    results
             (Maybe String, ProverResult)
    -> ModuleM (Maybe String, ProverResult)
    forall a. a -> ModuleT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe String
    firstProver, ProverResult
    esatexprs)

    -- | Execute a symbolic ':prove' or ':sat' command when the prover is
    --   set to offline.  This only prepares the SMT input file for the
    --   solver and does not actually invoke the solver.
    --
    --   This method returns either an error message or the text of
    --   the SMT input file corresponding to the given prover command.
    satProveOffline :: SBVProverConfig -> ProverCommand -> M.ModuleCmd (Either String String)
    satProveOffline :: SBVProverConfig
    -> ProverCommand -> ModuleCmd (Either String String)
    satProveOffline SBVProverConfig
    _proverCfg pc :: ProverCommand
    pc@ProverCommand {Bool
    String
    [DeclGroup]
    Maybe String
    IORef ProverStats
    Schema
    Expr
    QueryType
    pcQueryType :: ProverCommand -> QueryType
    pcProverName :: ProverCommand -> String
    pcVerbose :: ProverCommand -> Bool
    pcValidate :: ProverCommand -> Bool
    pcProverStats :: ProverCommand -> IORef ProverStats
    pcExtraDecls :: ProverCommand -> [DeclGroup]
    pcSmtFile :: ProverCommand -> Maybe String
    pcExpr :: ProverCommand -> Expr
    pcSchema :: ProverCommand -> Schema
    pcIgnoreSafety :: ProverCommand -> Bool
    pcQueryType :: QueryType
    pcProverName :: String
    pcVerbose :: Bool
    pcValidate :: Bool
    pcProverStats :: IORef ProverStats
    pcExtraDecls :: [DeclGroup]
    pcSmtFile :: Maybe String
    pcExpr :: Expr
    pcSchema :: Schema
    pcIgnoreSafety :: Bool
    ..} =
      (String -> ModuleCmd (Either String String))
    -> ModuleCmd (Either String String)
    -> ModuleCmd (Either String String)
    forall a. (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
    protectStack (\String
    msg ModuleInput IO
    minp -> ModuleRes (Either String String)
    -> IO (ModuleRes (Either String String))
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Either String String, ModuleEnv)
    -> Either ModuleError (Either String String, ModuleEnv)
    forall a b. b -> Either a b
    Right (String -> Either String String
    forall a b. a -> Either a b
    Left String
    msg, ModuleInput IO -> ModuleEnv
    forall (m :: * -> *). ModuleInput m -> ModuleEnv
    M.minpModuleEnv ModuleInput IO
    minp), [])) (ModuleCmd (Either String String)
     -> ModuleCmd (Either String String))
    -> ModuleCmd (Either String String)
    -> ModuleCmd (Either String String)
    forall a b. (a -> b) -> a -> b
    $
      \ModuleInput IO
    minp -> ModuleInput IO
    -> ModuleM (Either String String)
    -> IO (ModuleRes (Either String String))
    forall a.
    ModuleInput IO
    -> ModuleM a
    -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
    M.runModuleM ModuleInput IO
    minp (ModuleM (Either String String)
     -> IO (ModuleRes (Either String String)))
    -> ModuleM (Either String String)
    -> IO (ModuleRes (Either String String))
    forall a b. (a -> b) -> a -> b
    $
         do let isSat :: Bool
    isSat = case QueryType
    pcQueryType of
                  QueryType
    ProveQuery -> Bool
    False
                  QueryType
    SafetyQuery -> Bool
    False
                  SatQuery SatNum
    _ -> Bool
    True

    #if MIN_VERSION_sbv(10,0,0)
                generateSMTBenchmark :: Symbolic SVal -> IO String
    generateSMTBenchmark
                  | Bool
    isSat     = Symbolic SVal -> IO String
    SBV.generateSMTBenchmarkSat
                  | Bool
    otherwise = Symbolic SVal -> IO String
    SBV.generateSMTBenchmarkProof
    #else
                generateSMTBenchmark = SBV.generateSMTBenchmark isSat
    #endif
            EvalOpts
    evo <- IO EvalOpts -> ModuleT IO EvalOpts
    forall a. IO a -> ModuleT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (ModuleInput IO -> IO EvalOpts
    forall (m :: * -> *). ModuleInput m -> m EvalOpts
    M.minpEvalOpts ModuleInput IO
    minp)

            EvalOpts
    -> ProverCommand
    -> ModuleT IO (Either String ([FinType], Symbolic SVal))
    prepareQuery EvalOpts
    evo ProverCommand
    pc ModuleT IO (Either String ([FinType], Symbolic SVal))
    -> (Either String ([FinType], Symbolic SVal)
        -> ModuleM (Either String String))
    -> ModuleM (Either String String)
    forall a b. ModuleT IO a -> (a -> ModuleT IO b) -> ModuleT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
              Left String
    msg -> Either String String -> ModuleM (Either String String)
    forall a. a -> ModuleT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> Either String String
    forall a b. a -> Either a b
    Left String
    msg)
              Right ([FinType]
    _ts, Symbolic SVal
    q) -> String -> Either String String
    forall a b. b -> Either a b
    Right (String -> Either String String)
    -> ModuleT IO String -> ModuleM (Either String String)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO String -> ModuleT IO String
    forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
    M.io (Symbolic SVal -> IO String
    generateSMTBenchmark Symbolic SVal
    q)

    protectStack :: (String -> M.ModuleCmd a)
                 -> M.ModuleCmd a
                 -> M.ModuleCmd a
    protectStack :: forall a. (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
    protectStack String -> ModuleCmd a
    mkErr ModuleCmd a
    cmd ModuleInput IO
    modEnv =
      (AsyncException -> Maybe ())
    -> IO (ModuleRes a) -> (() -> IO (ModuleRes a)) -> IO (ModuleRes a)
    forall e b a.
    Exception e =>
    (e -> Maybe b) -> IO a -> (b -> IO a) -> IO a
    X.catchJust AsyncException -> Maybe ()
    isOverflow (ModuleCmd a
    cmd ModuleInput IO
    modEnv) () -> IO (ModuleRes a)
    handler
      where isOverflow :: AsyncException -> Maybe ()
    isOverflow AsyncException
    X.StackOverflow = () -> Maybe ()
    forall a. a -> Maybe a
    Just ()
            isOverflow AsyncException
    _               = Maybe ()
    forall a. Maybe a
    Nothing
            msg :: String
    msg = String
    "Symbolic evaluation failed to terminate."
            handler :: () -> IO (ModuleRes a)
    handler () = String -> ModuleCmd a
    mkErr String
    msg ModuleInput IO
    modEnv

    -- | Given concrete values from the solver and a collection of finite types,
    --   reconstruct Cryptol concrete values, and return any unused solver
    --   values.
    parseValues :: [FinType] -> [SBV.CV] -> ([VarShape Concrete.Concrete], [SBV.CV])
    parseValues :: [FinType] -> [CV] -> ([VarShape Concrete], [CV])
    parseValues [] [CV]
    cvs = ([], [CV]
    cvs)
    parseValues (FinType
    t : [FinType]
    ts) [CV]
    cvs = (VarShape Concrete
    v VarShape Concrete -> [VarShape Concrete] -> [VarShape Concrete]
    forall a. a -> [a] -> [a]
    : [VarShape Concrete]
    vs, [CV]
    cvs'')
      where (VarShape Concrete
    v, [CV]
    cvs') = FinType -> [CV] -> (VarShape Concrete, [CV])
    parseValue FinType
    t [CV]
    cvs
            ([VarShape Concrete]
    vs, [CV]
    cvs'') = [FinType] -> [CV] -> ([VarShape Concrete], [CV])
    parseValues [FinType]
    ts [CV]
    cvs'

    -- | Parse a single value of a finite type by consuming some number of
    --   solver values.  The parsed Cryptol values is returned along with
    --   any solver values not consumed.
    parseValue :: FinType -> [SBV.CV] -> (VarShape Concrete.Concrete, [SBV.CV])
    parseValue :: FinType -> [CV] -> (VarShape Concrete, [CV])
    parseValue FinType
    FTBit [] = String -> [String] -> (VarShape Concrete, [CV])
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Cryptol.Symbolic.parseValue" [ String
    "empty FTBit" ]
    parseValue FinType
    FTBit (CV
    cv : [CV]
    cvs) = (SBit Concrete -> VarShape Concrete
    forall sym. SBit sym -> VarShape sym
    VarBit (CV -> Bool
    SBV.cvToBool CV
    cv), [CV]
    cvs)
    parseValue FinType
    FTInteger [CV]
    cvs =
      case Kind -> [CV] -> Maybe (Integer, [CV])
    forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
    SBV.genParse Kind
    SBV.KUnbounded [CV]
    cvs of
        Just (Integer
    x, [CV]
    cvs') -> (SInteger Concrete -> VarShape Concrete
    forall sym. SInteger sym -> VarShape sym
    VarInteger Integer
    SInteger Concrete
    x, [CV]
    cvs')
        Maybe (Integer, [CV])
    Nothing        -> String -> [String] -> (VarShape Concrete, [CV])
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Cryptol.Symbolic.parseValue" [ String
    "no integer" ]
    parseValue (FTIntMod Integer
    _) [CV]
    cvs = FinType -> [CV] -> (VarShape Concrete, [CV])
    parseValue FinType
    FTInteger [CV]
    cvs
    parseValue FinType
    FTRational [CV]
    cvs =
      (VarShape Concrete, [CV])
    -> Maybe (VarShape Concrete, [CV]) -> (VarShape Concrete, [CV])
    forall a. a -> Maybe a -> a
    fromMaybe (String -> [String] -> (VarShape Concrete, [CV])
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Cryptol.Symbolic.parseValue" [String
    "no rational"]) (Maybe (VarShape Concrete, [CV]) -> (VarShape Concrete, [CV]))
    -> Maybe (VarShape Concrete, [CV]) -> (VarShape Concrete, [CV])
    forall a b. (a -> b) -> a -> b
    $
      do (Integer
    n,[CV]
    cvs')  <- Kind -> [CV] -> Maybe (Integer, [CV])
    forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
    SBV.genParse Kind
    SBV.KUnbounded [CV]
    cvs
         (Integer
    d,[CV]
    cvs'') <- Kind -> [CV] -> Maybe (Integer, [CV])
    forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
    SBV.genParse Kind
    SBV.KUnbounded [CV]
    cvs'
         (VarShape Concrete, [CV]) -> Maybe (VarShape Concrete, [CV])
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SInteger Concrete -> SInteger Concrete -> VarShape Concrete
    forall sym. SInteger sym -> SInteger sym -> VarShape sym
    VarRational Integer
    SInteger Concrete
    n Integer
    SInteger Concrete
    d, [CV]
    cvs'')
    parseValue (FTSeq Integer
    0 FinType
    FTBit) [CV]
    cvs = (SWord Concrete -> VarShape Concrete
    forall sym. SWord sym -> VarShape sym
    VarWord (Integer -> Integer -> BV
    Concrete.mkBv Integer
    0 Integer
    0), [CV]
    cvs)
    parseValue (FTSeq Integer
    n FinType
    FTBit) [CV]
    cvs =
      case Kind -> [CV] -> Maybe (Integer, [CV])
    forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
    SBV.genParse (Bool -> Int -> Kind
    SBV.KBounded Bool
    False (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    n)) [CV]
    cvs of
        Just (Integer
    x, [CV]
    cvs') -> (SWord Concrete -> VarShape Concrete
    forall sym. SWord sym -> VarShape sym
    VarWord (Integer -> Integer -> BV
    Concrete.mkBv (Integer -> Integer
    forall a. Integral a => a -> Integer
    toInteger Integer
    n) Integer
    x), [CV]
    cvs')
        Maybe (Integer, [CV])
    Nothing -> String -> [String] -> (VarShape Concrete, [CV])
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Cryptol.Symbolic.parseValue" [String
    "no bitvector"]
    parseValue (FTSeq Integer
    n FinType
    t) [CV]
    cvs = (Integer -> [VarShape Concrete] -> VarShape Concrete
    forall sym. Integer -> [VarShape sym] -> VarShape sym
    VarFinSeq (Integer -> Integer
    forall a. Integral a => a -> Integer
    toInteger Integer
    n) [VarShape Concrete]
    vs, [CV]
    cvs')
      where ([VarShape Concrete]
    vs, [CV]
    cvs') = [FinType] -> [CV] -> ([VarShape Concrete], [CV])
    parseValues (Int -> FinType -> [FinType]
    forall a. Int -> a -> [a]
    replicate (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    n) FinType
    t) [CV]
    cvs
    parseValue (FTTuple [FinType]
    ts) [CV]
    cvs = ([VarShape Concrete] -> VarShape Concrete
    forall sym. [VarShape sym] -> VarShape sym
    VarTuple [VarShape Concrete]
    vs, [CV]
    cvs')
      where ([VarShape Concrete]
    vs, [CV]
    cvs') = [FinType] -> [CV] -> ([VarShape Concrete], [CV])
    parseValues [FinType]
    ts [CV]
    cvs
    parseValue (FTRecord RecordMap Ident FinType
    r) [CV]
    cvs = (RecordMap Ident (VarShape Concrete) -> VarShape Concrete
    forall sym. RecordMap Ident (VarShape sym) -> VarShape sym
    VarRecord RecordMap Ident (VarShape Concrete)
    r', [CV]
    cvs')
      where ([Ident]
    ns, [FinType]
    ts)   = [(Ident, FinType)] -> ([Ident], [FinType])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ([(Ident, FinType)] -> ([Ident], [FinType]))
    -> [(Ident, FinType)] -> ([Ident], [FinType])
    forall a b. (a -> b) -> a -> b
    $ RecordMap Ident FinType -> [(Ident, FinType)]
    forall a b. RecordMap a b -> [(a, b)]
    canonicalFields RecordMap Ident FinType
    r
            ([VarShape Concrete]
    vs, [CV]
    cvs') = [FinType] -> [CV] -> ([VarShape Concrete], [CV])
    parseValues [FinType]
    ts [CV]
    cvs
            fs :: [(Ident, VarShape Concrete)]
    fs         = [Ident] -> [VarShape Concrete] -> [(Ident, VarShape Concrete)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Ident]
    ns [VarShape Concrete]
    vs
            r' :: RecordMap Ident (VarShape Concrete)
    r'         = [Ident]
    -> [(Ident, VarShape Concrete)]
    -> RecordMap Ident (VarShape Concrete)
    forall a b. (Show a, Ord a) => [a] -> [(a, b)] -> RecordMap a b
    recordFromFieldsWithDisplay (RecordMap Ident FinType -> [Ident]
    forall a b. RecordMap a b -> [a]
    displayOrder RecordMap Ident FinType
    r) [(Ident, VarShape Concrete)]
    fs

    parseValue (FTNewtype Newtype
    _ [Either Nat' TValue]
    _ RecordMap Ident FinType
    r) [CV]
    cvs = FinType -> [CV] -> (VarShape Concrete, [CV])
    parseValue (RecordMap Ident FinType -> FinType
    FTRecord RecordMap Ident FinType
    r) [CV]
    cvs

    parseValue (FTFloat Integer
    e Integer
    p) [CV]
    cvs =
       (SFloat Concrete -> VarShape Concrete
    forall sym. SFloat sym -> VarShape sym
    VarFloat FH.BF { bfValue :: BigFloat
    FH.bfValue = BigFloat
    bfNaN
                       , bfExpWidth :: Integer
    FH.bfExpWidth = Integer
    e
                       , bfPrecWidth :: Integer
    FH.bfPrecWidth = Integer
    p
                       }
       , [CV]
    cvs
       )
       -- XXX: NOT IMPLEMENTED

    freshBoundedInt :: SBV -> Maybe Integer -> Maybe Integer -> IO SBV.SVal
    freshBoundedInt :: SBV -> Maybe Integer -> Maybe Integer -> IO SVal
    freshBoundedInt SBV
    sym Maybe Integer
    lo Maybe Integer
    hi =
      do SVal
    x <- SBV -> IO (SInteger SBV)
    freshSInteger_ SBV
    sym
         case Maybe Integer
    lo of
           Just Integer
    l  -> SBV -> SVal -> IO ()
    addDefEqn SBV
    sym (SVal -> SVal -> SVal
    SBV.svLessEq (Kind -> Integer -> SVal
    SBV.svInteger Kind
    SBV.KUnbounded Integer
    l) SVal
    x)
           Maybe Integer
    Nothing -> () -> IO ()
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
         case Maybe Integer
    hi of
           Just Integer
    h  -> SBV -> SVal -> IO ()
    addDefEqn SBV
    sym (SVal -> SVal -> SVal
    SBV.svLessEq SVal
    x (Kind -> Integer -> SVal
    SBV.svInteger Kind
    SBV.KUnbounded Integer
    h))
           Maybe Integer
    Nothing -> () -> IO ()
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
         SVal -> IO SVal
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SVal
    x

    freshBitvector :: SBV -> Integer -> IO SBV.SVal
    freshBitvector :: SBV -> Integer -> IO SVal
    freshBitvector SBV
    sym Integer
    w
      | Integer
    w Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0 = SVal -> IO SVal
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Kind -> Integer -> SVal
    SBV.svInteger (Bool -> Int -> Kind
    SBV.KBounded Bool
    False Int
    0) Integer
    0)
      | Bool
    otherwise = SBV -> Int -> IO (SWord SBV)
    freshBV_ SBV
    sym (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    w)

    sbvFreshFns :: SBV -> FreshVarFns SBV
    sbvFreshFns :: SBV -> FreshVarFns SBV
    sbvFreshFns SBV
    sym =
      FreshVarFns
      { freshBitVar :: IO (SBit SBV)
    freshBitVar     = SBV -> IO (SBit SBV)
    freshSBool_ SBV
    sym
      , freshWordVar :: Integer -> IO (SWord SBV)
    freshWordVar    = SBV -> Integer -> IO SVal
    freshBitvector SBV
    sym
      , freshIntegerVar :: Maybe Integer -> Maybe Integer -> IO (SInteger SBV)
    freshIntegerVar = SBV -> Maybe Integer -> Maybe Integer -> IO SVal
    freshBoundedInt SBV
    sym
      , freshFloatVar :: Integer -> Integer -> IO (SFloat SBV)
    freshFloatVar   = \Integer
    _ Integer
    _ -> () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return () -- TODO
      }