    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Provers.Prover
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Provable abstraction and the connection to SMT solvers
    -----------------------------------------------------------------------------

    {-# LANGUAGE CPP                   #-}
    {-# LANGUAGE ConstraintKinds       #-}
    {-# LANGUAGE FlexibleContexts      #-}
    {-# LANGUAGE FlexibleInstances     #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE NamedFieldPuns        #-}
    {-# LANGUAGE ScopedTypeVariables   #-}
    {-# LANGUAGE TupleSections         #-}
    {-# LANGUAGE UndecidableInstances  #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Provers.Prover (
             SMTSolver(..), SMTConfig(..), Predicate
           , ProvableM(..), Provable, SatisfiableM(..), Satisfiable
           , generateSMTBenchmarkSat, generateSMTBenchmarkProof, ConstraintSet
           , ThmResult(..), SatResult(..), AllSatResult(..), SafeResult(..), OptimizeResult(..), SMTResult(..)
           , SExecutable(..), isSafe
           , runSMT, runSMTWith
           , SatModel(..), Modelable(..), displayModels, extractModels
           , getModelDictionaries, getModelValues, getModelUninterpretedValues
           , abc, boolector, bitwuzla, cvc4, cvc5, dReal, mathSAT, yices, z3, defaultSMTCfg, defaultDeltaSMTCfg
           , proveWithAny, proveWithAll, proveConcurrentWithAny, proveConcurrentWithAll
           , satWithAny,   satWithAll,   satConcurrentWithAny,   satConcurrentWithAll
           ) where

    import Control.Monad          (when, unless)
    import Control.Monad.IO.Class (MonadIO, liftIO)
    import Control.DeepSeq        (rnf, NFData(..))

    import Control.Concurrent.Async (async, waitAny, asyncThreadId, Async, mapConcurrently)
    import Control.Exception (finally, throwTo)
    import System.Exit (ExitCode(ExitSuccess))

    import System.IO.Unsafe (unsafeInterleaveIO)             -- only used safely!

    import System.Directory  (getCurrentDirectory)
    import Data.Time (getZonedTime, NominalDiffTime, UTCTime, getCurrentTime, diffUTCTime)
    import Data.List (intercalate, isPrefixOf)

    import Data.Maybe (mapMaybe, listToMaybe)

    import qualified Data.Foldable   as S (toList)
    import qualified Data.Text       as T

    import Data.SBV.Core.Data
    import Data.SBV.Core.Symbolic
    import Data.SBV.SMT.SMT
    import Data.SBV.SMT.Utils (debug, alignPlain)
    import Data.SBV.Utils.ExtractIO
    import Data.SBV.Utils.TDiff

    import qualified Data.SBV.Trans.Control as Control
    import qualified Data.SBV.Control.Query as Control
    import qualified Data.SBV.Control.Utils as Control

    import GHC.Stack

    import qualified Data.SBV.Provers.ABC       as ABC
    import qualified Data.SBV.Provers.Boolector as Boolector
    import qualified Data.SBV.Provers.Bitwuzla  as Bitwuzla
    import qualified Data.SBV.Provers.CVC4      as CVC4
    import qualified Data.SBV.Provers.CVC5      as CVC5
    import qualified Data.SBV.Provers.DReal     as DReal
    import qualified Data.SBV.Provers.MathSAT   as MathSAT
    import qualified Data.SBV.Provers.Yices     as Yices
    import qualified Data.SBV.Provers.Z3        as Z3

    import GHC.TypeLits

    mkConfig :: SMTSolver -> SMTLibVersion -> [Control.SMTOption] -> SMTConfig
    mkConfig :: SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
    mkConfig SMTSolver
    s SMTLibVersion
    smtVersion [SMTOption]
    startOpts = SMTConfig { verbose :: Bool
    verbose                     = Bool
    False
                                                , timing :: Timing
    timing                      = Timing
    NoTiming
                                                , printBase :: Int
    printBase                   = Int
    10
                                                , printRealPrec :: Int
    printRealPrec               = Int
    16
                                                , crackNum :: Bool
    crackNum                    = Bool
    False
                                                , transcript :: Maybe String
    transcript                  = Maybe String
    forall a. Maybe a
    Nothing
                                                , solver :: SMTSolver
    solver                      = SMTSolver
    s
                                                , smtLibVersion :: SMTLibVersion
    smtLibVersion               = SMTLibVersion
    smtVersion
                                                , dsatPrecision :: Maybe Double
    dsatPrecision               = Maybe Double
    forall a. Maybe a
    Nothing
                                                , extraArgs :: [String]
    extraArgs                   = []
                                                , satCmd :: String
    satCmd                      = String
    "(check-sat)"
                                                , allSatTrackUFs :: Bool
    allSatTrackUFs              = Bool
    True                   -- i.e., yes, do extract UI function values
                                                , allSatMaxModelCount :: Maybe Int
    allSatMaxModelCount         = Maybe Int
    forall a. Maybe a
    Nothing                -- i.e., return all satisfying models
                                                , allSatPrintAlong :: Bool
    allSatPrintAlong            = Bool
    False                  -- i.e., do not print models as they are found
                                                , isNonModelVar :: String -> Bool
    isNonModelVar               = Bool -> String -> Bool
    forall a b. a -> b -> a
    const Bool
    False            -- i.e., everything is a model-variable by default
                                                , validateModel :: Bool
    validateModel               = Bool
    False
                                                , optimizeValidateConstraints :: Bool
    optimizeValidateConstraints = Bool
    False
                                                , roundingMode :: RoundingMode
    roundingMode                = RoundingMode
    RoundNearestTiesToEven
                                                , solverSetOptions :: [SMTOption]
    solverSetOptions            = [SMTOption]
    startOpts
                                                , ignoreExitCode :: Bool
    ignoreExitCode              = Bool
    False
                                                , redirectVerbose :: Maybe String
    redirectVerbose             = Maybe String
    forall a. Maybe a
    Nothing
                                                }

    -- | If supported, this makes all output go to stdout, which works better with SBV
    -- Alas, not all solvers support it..
    allOnStdOut :: Control.SMTOption
    allOnStdOut :: SMTOption
    allOnStdOut = String -> SMTOption
    Control.DiagnosticOutputChannel String
    "stdout"

    -- | Default configuration for the ABC synthesis and verification tool.
    abc :: SMTConfig
    abc :: SMTConfig
    abc = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
    mkConfig SMTSolver
    ABC.abc SMTLibVersion
    SMTLib2 [SMTOption
    allOnStdOut]

    -- | Default configuration for the Boolector SMT solver
    boolector :: SMTConfig
    boolector :: SMTConfig
    boolector = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
    mkConfig SMTSolver
    Boolector.boolector SMTLibVersion
    SMTLib2 []

    -- | Default configuration for the Bitwuzla SMT solver
    bitwuzla :: SMTConfig
    bitwuzla :: SMTConfig
    bitwuzla = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
    mkConfig SMTSolver
    Bitwuzla.bitwuzla SMTLibVersion
    SMTLib2 []

    -- | Default configuration for the CVC4 SMT Solver.
    cvc4 :: SMTConfig
    cvc4 :: SMTConfig
    cvc4 = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
    mkConfig SMTSolver
    CVC4.cvc4 SMTLibVersion
    SMTLib2 [SMTOption
    allOnStdOut]

    -- | Default configuration for the CVC5 SMT Solver.
    cvc5 :: SMTConfig
    cvc5 :: SMTConfig
    cvc5 = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
    mkConfig SMTSolver
    CVC5.cvc5 SMTLibVersion
    SMTLib2 [SMTOption
    allOnStdOut]

    -- | Default configuration for the Yices SMT Solver.
    dReal :: SMTConfig
    dReal :: SMTConfig
    dReal = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
    mkConfig SMTSolver
    DReal.dReal SMTLibVersion
    SMTLib2 [ String -> [String] -> SMTOption
    Control.OptionKeyword String
    ":smtlib2_compliant" [String
    "true"]
                                         ]

    -- | Default configuration for the MathSAT SMT solver
    mathSAT :: SMTConfig
    mathSAT :: SMTConfig
    mathSAT = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
    mkConfig SMTSolver
    MathSAT.mathSAT SMTLibVersion
    SMTLib2 [SMTOption
    allOnStdOut]

    -- | Default configuration for the Yices SMT Solver.
    yices :: SMTConfig
    yices :: SMTConfig
    yices = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
    mkConfig SMTSolver
    Yices.yices SMTLibVersion
    SMTLib2 []

    -- | Default configuration for the Z3 SMT solver
    z3 :: SMTConfig
    z3 :: SMTConfig
    z3 = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
    mkConfig SMTSolver
    Z3.z3 SMTLibVersion
    SMTLib2 [ String -> [String] -> SMTOption
    Control.OptionKeyword String
    ":smtlib2_compliant" [String
    "true"]
                                , SMTOption
    allOnStdOut
                                ]

    -- | The default solver used by SBV. This is currently set to z3.
    defaultSMTCfg :: SMTConfig
    defaultSMTCfg :: SMTConfig
    defaultSMTCfg = SMTConfig
    z3

    -- | The default solver used by SBV for delta-satisfiability problems. This is currently set to dReal,
    -- which is also the only solver that supports delta-satisfiability.
    defaultDeltaSMTCfg :: SMTConfig
    defaultDeltaSMTCfg :: SMTConfig
    defaultDeltaSMTCfg = SMTConfig
    dReal

    -- | A predicate is a symbolic program that returns a (symbolic) boolean value. For all intents and
    -- purposes, it can be treated as an n-ary function from symbolic-values to a boolean. The 'Symbolic'
    -- monad captures the underlying representation, and can/should be ignored by the users of the library,
    -- unless you are building further utilities on top of SBV itself. Instead, simply use the 'Predicate'
    -- type when necessary.
    type Predicate = Symbolic SBool

    -- | A constraint set is a symbolic program that returns no values. The idea is that the constraints/min-max
    -- goals will serve as the collection of constraints that will be used for sat/optimize calls.
    type ConstraintSet = Symbolic ()

    -- | `Provable` is specialization of `ProvableM` to the `IO` monad. Unless you are using
    -- transformers explicitly, this is the type you should prefer.
    type Provable = ProvableM IO

    -- | `Data.SBV.Provers.Satisfiable` is specialization of `SatisfiableM` to the `IO` monad. Unless you are using
    -- transformers explicitly, this is the type you should prefer.
    type Satisfiable = SatisfiableM IO

    -- | A type @a@ is satisfiable if it has constraints, potentially returning a boolean. This class
    -- captures essentially sat and optimize calls.
    class ExtractIO m => SatisfiableM m a where
      -- | Reduce an arg, for sat purposes.
      satArgReduce :: a -> SymbolicT m SBool

      -- | Generalization of 'Data.SBV.sat'
      sat :: a -> m SatResult
      sat = SMTConfig -> a -> m SatResult
    forall (m :: * -> *) a.
    SatisfiableM m a =>
    SMTConfig -> a -> m SatResult
    satWith SMTConfig
    defaultSMTCfg

      -- | Generalization of 'Data.SBV.satWith'
      satWith :: SMTConfig -> a -> m SatResult
      satWith SMTConfig
    cfg a
    a = do SMTResult
    r <- (a -> SymbolicT m SBool)
    -> Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
    forall (m :: * -> *) a b.
    ExtractIO m =>
    (a -> SymbolicT m SBool)
    -> Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery a -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce Bool
    True (QueryT m ()
    forall (m :: * -> *). MonadIO m => QueryT m ()
    checkNoOptimizations QueryT m () -> QueryT m SMTResult -> QueryT m SMTResult
    forall a b. QueryT m a -> QueryT m b -> QueryT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> QueryT m SMTResult
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
    Control.getSMTResult) SMTConfig
    cfg a
    a
                         SMTResult -> SatResult
    SatResult (SMTResult -> SatResult) -> m SMTResult -> m SatResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> if SMTConfig -> Bool
    validationRequested SMTConfig
    cfg
                                       then (a -> SymbolicT m SBool)
    -> Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    forall (m :: * -> *) a.
    MonadIO m =>
    (a -> SymbolicT m SBool)
    -> Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    validate a -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce Bool
    True SMTConfig
    cfg a
    a SMTResult
    r
                                       else SMTResult -> m SMTResult
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTResult
    r

      -- | Generalization of 'Data.SBV.sat'
      dsat :: a -> m SatResult
      dsat = SMTConfig -> a -> m SatResult
    forall (m :: * -> *) a.
    SatisfiableM m a =>
    SMTConfig -> a -> m SatResult
    dsatWith SMTConfig
    defaultDeltaSMTCfg

      -- | Generalization of 'Data.SBV.satWith'
      dsatWith :: SMTConfig -> a -> m SatResult
      dsatWith SMTConfig
    cfg a
    a = do SMTResult
    r <- (a -> SymbolicT m SBool)
    -> Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
    forall (m :: * -> *) a b.
    ExtractIO m =>
    (a -> SymbolicT m SBool)
    -> Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery a -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce Bool
    True (QueryT m ()
    forall (m :: * -> *). MonadIO m => QueryT m ()
    checkNoOptimizations QueryT m () -> QueryT m SMTResult -> QueryT m SMTResult
    forall a b. QueryT m a -> QueryT m b -> QueryT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> QueryT m SMTResult
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
    Control.getSMTResult) SMTConfig
    cfg a
    a
                          SMTResult -> SatResult
    SatResult (SMTResult -> SatResult) -> m SMTResult -> m SatResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> if SMTConfig -> Bool
    validationRequested SMTConfig
    cfg
                                        then (a -> SymbolicT m SBool)
    -> Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    forall (m :: * -> *) a.
    MonadIO m =>
    (a -> SymbolicT m SBool)
    -> Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    validate a -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce Bool
    True SMTConfig
    cfg a
    a SMTResult
    r
                                        else SMTResult -> m SMTResult
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTResult
    r

      -- | Generalization of 'Data.SBV.allSat'
      allSat :: a -> m AllSatResult
      allSat = SMTConfig -> a -> m AllSatResult
    forall (m :: * -> *) a.
    SatisfiableM m a =>
    SMTConfig -> a -> m AllSatResult
    allSatWith SMTConfig
    defaultSMTCfg

      -- | Generalization of 'Data.SBV.allSatWith'
      allSatWith :: SMTConfig -> a -> m AllSatResult
      allSatWith SMTConfig
    cfg a
    a = do AllSatResult
    asr <- (a -> SymbolicT m SBool)
    -> Bool
    -> QueryT m AllSatResult
    -> SMTConfig
    -> a
    -> m AllSatResult
    forall (m :: * -> *) a b.
    ExtractIO m =>
    (a -> SymbolicT m SBool)
    -> Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery a -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce Bool
    True (QueryT m ()
    forall (m :: * -> *). MonadIO m => QueryT m ()
    checkNoOptimizations QueryT m () -> QueryT m AllSatResult -> QueryT m AllSatResult
    forall a b. QueryT m a -> QueryT m b -> QueryT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> QueryT m AllSatResult
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m, SolverContext m) =>
    m AllSatResult
    Control.getAllSatResult) SMTConfig
    cfg a
    a
                            if SMTConfig -> Bool
    validationRequested SMTConfig
    cfg
                               then do [SMTResult]
    rs' <- (SMTResult -> m SMTResult) -> [SMTResult] -> m [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 ((a -> SymbolicT m SBool)
    -> Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    forall (m :: * -> *) a.
    MonadIO m =>
    (a -> SymbolicT m SBool)
    -> Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    validate a -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce Bool
    True SMTConfig
    cfg a
    a) (AllSatResult -> [SMTResult]
    allSatResults AllSatResult
    asr)
                                       AllSatResult -> m AllSatResult
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return AllSatResult
    asr{allSatResults :: [SMTResult]
    allSatResults = [SMTResult]
    rs'}
                               else AllSatResult -> m AllSatResult
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return AllSatResult
    asr

      -- | Generalization of 'Data.SBV.isSatisfiable'
      isSatisfiable :: a -> m Bool
      isSatisfiable = SMTConfig -> a -> m Bool
    forall (m :: * -> *) a.
    SatisfiableM m a =>
    SMTConfig -> a -> m Bool
    isSatisfiableWith SMTConfig
    defaultSMTCfg

      -- | Generalization of 'Data.SBV.isSatisfiableWith'
      isSatisfiableWith :: SMTConfig -> a -> m Bool
      isSatisfiableWith SMTConfig
    cfg a
    p = do SatResult
    r <- SMTConfig -> a -> m SatResult
    forall (m :: * -> *) a.
    SatisfiableM m a =>
    SMTConfig -> a -> m SatResult
    satWith SMTConfig
    cfg a
    p
                                   case SatResult
    r of
                                     SatResult Satisfiable{}   -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
                                     SatResult Unsatisfiable{} -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
                                     SatResult
    _                         -> String -> m Bool
    forall a. HasCallStack => String -> a
    error (String -> m Bool) -> String -> m Bool
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.isSatisfiable: Received: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SatResult -> String
    forall a. Show a => a -> String
    show SatResult
    r

      -- | Generalization of 'Data.SBV.optimize'
      optimize :: OptimizeStyle -> a -> m OptimizeResult
      optimize = SMTConfig -> OptimizeStyle -> a -> m OptimizeResult
    forall (m :: * -> *) a.
    SatisfiableM m a =>
    SMTConfig -> OptimizeStyle -> a -> m OptimizeResult
    optimizeWith SMTConfig
    defaultSMTCfg

      -- | Generalization of 'Data.SBV.optimizeWith'
      optimizeWith :: SMTConfig -> OptimizeStyle -> a -> m OptimizeResult
      optimizeWith SMTConfig
    config OptimizeStyle
    style a
    optGoal = do
                       OptimizeResult
    res <- (a -> SymbolicT m SBool)
    -> Bool
    -> QueryT m OptimizeResult
    -> SMTConfig
    -> a
    -> m OptimizeResult
    forall (m :: * -> *) a b.
    ExtractIO m =>
    (a -> SymbolicT m SBool)
    -> Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery a -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce Bool
    True QueryT m OptimizeResult
    opt SMTConfig
    config a
    optGoal
                       if Bool -> Bool
    not (SMTConfig -> Bool
    optimizeValidateConstraints SMTConfig
    config)
                          then OptimizeResult -> m OptimizeResult
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return OptimizeResult
    res
                          else let v :: SMTResult -> m SMTResult
                                   v :: SMTResult -> m SMTResult
    v = (a -> SymbolicT m SBool)
    -> Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    forall (m :: * -> *) a.
    MonadIO m =>
    (a -> SymbolicT m SBool)
    -> Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    validate a -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce Bool
    True SMTConfig
    config a
    optGoal
                               in case OptimizeResult
    res of
                                    LexicographicResult SMTResult
    m -> SMTResult -> OptimizeResult
    LexicographicResult (SMTResult -> OptimizeResult) -> m SMTResult -> m OptimizeResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SMTResult -> m SMTResult
    v SMTResult
    m
                                    IndependentResult [(String, SMTResult)]
    xs  -> let w :: [(a, SMTResult)] -> [(a, SMTResult)] -> m [(a, SMTResult)]
    w []            [(a, SMTResult)]
    sofar = [(a, SMTResult)] -> m [(a, SMTResult)]
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(a, SMTResult)] -> [(a, SMTResult)]
    forall a. [a] -> [a]
    reverse [(a, SMTResult)]
    sofar)
                                                                 w ((a
    n, SMTResult
    m):[(a, SMTResult)]
    rest) [(a, SMTResult)]
    sofar = SMTResult -> m SMTResult
    v SMTResult
    m m SMTResult
    -> (SMTResult -> m [(a, SMTResult)]) -> m [(a, SMTResult)]
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SMTResult
    m' -> [(a, SMTResult)] -> [(a, SMTResult)] -> m [(a, SMTResult)]
    w [(a, SMTResult)]
    rest ((a
    n, SMTResult
    m') (a, SMTResult) -> [(a, SMTResult)] -> [(a, SMTResult)]
    forall a. a -> [a] -> [a]
    : [(a, SMTResult)]
    sofar)
                                                             in [(String, SMTResult)] -> OptimizeResult
    IndependentResult ([(String, SMTResult)] -> OptimizeResult)
    -> m [(String, SMTResult)] -> m OptimizeResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(String, SMTResult)]
    -> [(String, SMTResult)] -> m [(String, SMTResult)]
    forall {a}.
    [(a, SMTResult)] -> [(a, SMTResult)] -> m [(a, SMTResult)]
    w [(String, SMTResult)]
    xs []
                                    ParetoResult (Bool
    b, [SMTResult]
    rs)  -> (Bool, [SMTResult]) -> OptimizeResult
    ParetoResult ((Bool, [SMTResult]) -> OptimizeResult)
    -> ([SMTResult] -> (Bool, [SMTResult]))
    -> [SMTResult]
    -> OptimizeResult
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Bool
    b, ) ([SMTResult] -> OptimizeResult)
    -> m [SMTResult] -> m OptimizeResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (SMTResult -> m SMTResult) -> [SMTResult] -> m [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 SMTResult -> m SMTResult
    v [SMTResult]
    rs

        where opt :: QueryT m OptimizeResult
    opt = do [Objective (SV, SV)]
    objectives <- QueryT m [Objective (SV, SV)]
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m [Objective (SV, SV)]
    Control.getObjectives

                       Bool -> QueryT m () -> QueryT m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when ([Objective (SV, SV)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Objective (SV, SV)]
    objectives) (QueryT m () -> QueryT m ()) -> QueryT m () -> QueryT m ()
    forall a b. (a -> b) -> a -> b
    $
                              String -> QueryT m ()
    forall a. HasCallStack => String -> a
    error (String -> QueryT m ()) -> String -> QueryT m ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    ""
                                              , String
    "*** Data.SBV: Unsupported call to optimize when no objectives are present."
                                              , String
    "*** Use \"sat\" for plain satisfaction"
                                              ]

                       Bool -> QueryT m () -> QueryT m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (SolverCapabilities -> Bool
    supportsOptimization (SMTSolver -> SolverCapabilities
    capabilities (SMTConfig -> SMTSolver
    solver SMTConfig
    config))) (QueryT m () -> QueryT m ()) -> QueryT m () -> QueryT m ()
    forall a b. (a -> b) -> a -> b
    $
                              String -> QueryT m ()
    forall a. HasCallStack => String -> a
    error (String -> QueryT m ()) -> String -> QueryT m ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    ""
                                              , String
    "*** Data.SBV: The backend solver " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Solver -> String
    forall a. Show a => a -> String
    show (SMTSolver -> Solver
    name (SMTConfig -> SMTSolver
    solver SMTConfig
    config)) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "does not support optimization goals."
                                              , String
    "*** Please use a solver that has support, such as z3"
                                              ]

                       Bool -> QueryT m () -> QueryT m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (SMTConfig -> Bool
    validateModel SMTConfig
    config Bool -> Bool -> Bool
    && Bool -> Bool
    not (SMTConfig -> Bool
    optimizeValidateConstraints SMTConfig
    config)) (QueryT m () -> QueryT m ()) -> QueryT m () -> QueryT m ()
    forall a b. (a -> b) -> a -> b
    $
                              String -> QueryT m ()
    forall a. HasCallStack => String -> a
    error (String -> QueryT m ()) -> String -> QueryT m ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    ""
                                              , String
    "*** Data.SBV: Model validation is not supported in optimization calls."
                                              , String
    "***"
                                              , String
    "*** Instead, use `cfg{optimizeValidateConstraints = True}`"
                                              , String
    "***"
                                              , String
    "*** which checks that the results satisfy the constraints but does"
                                              , String
    "*** NOT ensure that they are optimal."
                                              ]

                       let optimizerDirectives :: [String]
    optimizerDirectives = (Objective (SV, SV) -> [String])
    -> [Objective (SV, SV)] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Objective (SV, SV) -> [String]
    forall {a} {a}. (Show a, Show a) => Objective (a, a) -> [String]
    minmax [Objective (SV, SV)]
    objectives [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ OptimizeStyle -> [String]
    priority OptimizeStyle
    style
                             where mkEq :: (a, a) -> String
    mkEq (a
    x, a
    y) = String
    "(assert (= " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    y String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "))"

                                   minmax :: Objective (a, a) -> [String]
    minmax (Minimize          String
    _  xy :: (a, a)
    xy@(a
    _, a
    v))     = [(a, a) -> String
    forall {a} {a}. (Show a, Show a) => (a, a) -> String
    mkEq (a, a)
    xy, String
    "(minimize "    String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    v                 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"]
                                   minmax (Maximize          String
    _  xy :: (a, a)
    xy@(a
    _, a
    v))     = [(a, a) -> String
    forall {a} {a}. (Show a, Show a) => (a, a) -> String
    mkEq (a, a)
    xy, String
    "(maximize "    String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    v                 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"]
                                   minmax (AssertWithPenalty String
    nm xy :: (a, a)
    xy@(a
    _, a
    v) Penalty
    mbp) = [(a, a) -> String
    forall {a} {a}. (Show a, Show a) => (a, a) -> String
    mkEq (a, a)
    xy, String
    "(assert-soft " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    v String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Penalty -> String
    penalize Penalty
    mbp String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"]
                                     where penalize :: Penalty -> String
    penalize Penalty
    DefaultPenalty    = String
    ""
                                           penalize (Penalty Rational
    w Maybe String
    mbGrp)
                                              | Rational
    w Rational -> Rational -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Rational
    0         = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    "SBV.AssertWithPenalty: Goal " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " is assigned a non-positive penalty: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    shw
                                                                                 , String
    "All soft goals must have > 0 penalties associated."
                                                                                 ]
                                              | Bool
    True           = String
    " :weight " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    shw String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> (String -> String) -> Maybe String -> String
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe String
    "" String -> String
    group Maybe String
    mbGrp
                                              where shw :: String
    shw = Double -> String
    forall a. Show a => a -> String
    show (Rational -> Double
    forall a. Fractional a => Rational -> a
    fromRational Rational
    w :: Double)

                                           group :: String -> String
    group String
    g = String
    " :id " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    g

                                   priority :: OptimizeStyle -> [String]
    priority OptimizeStyle
    Lexicographic = [] -- default, no option needed
                                   priority OptimizeStyle
    Independent   = [String
    "(set-option :opt.priority box)"]
                                   priority (Pareto Maybe Int
    _)    = [String
    "(set-option :opt.priority pareto)"]

                       (String -> QueryT m ()) -> [String] -> QueryT m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Bool -> String -> QueryT m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> String -> m ()
    Control.send Bool
    True) [String]
    optimizerDirectives

                       case OptimizeStyle
    style of
                         OptimizeStyle
    Lexicographic -> SMTResult -> OptimizeResult
    LexicographicResult (SMTResult -> OptimizeResult)
    -> QueryT m SMTResult -> QueryT m OptimizeResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QueryT m SMTResult
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
    Control.getLexicographicOptResults
                         OptimizeStyle
    Independent   -> [(String, SMTResult)] -> OptimizeResult
    IndependentResult   ([(String, SMTResult)] -> OptimizeResult)
    -> QueryT m [(String, SMTResult)] -> QueryT m OptimizeResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [String] -> QueryT m [(String, SMTResult)]
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    [String] -> m [(String, SMTResult)]
    Control.getIndependentOptResults ((Objective (SV, SV) -> String) -> [Objective (SV, SV)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Objective (SV, SV) -> String
    forall a. Objective a -> String
    objectiveName [Objective (SV, SV)]
    objectives)
                         Pareto Maybe Int
    mbN    -> (Bool, [SMTResult]) -> OptimizeResult
    ParetoResult        ((Bool, [SMTResult]) -> OptimizeResult)
    -> QueryT m (Bool, [SMTResult]) -> QueryT m OptimizeResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe Int -> QueryT m (Bool, [SMTResult])
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Maybe Int -> m (Bool, [SMTResult])
    Control.getParetoOptResults Maybe Int
    mbN

    -- | Find a satisfying assignment to a property with multiple solvers, running them in separate threads. The
    -- results will be returned in the order produced.
    satWithAll :: Satisfiable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
    satWithAll :: forall a.
    Satisfiable a =>
    [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
    satWithAll = ([SMTConfig]
    -> (SMTConfig -> a -> IO SatResult)
    -> a
    -> IO [(Solver, NominalDiffTime, SatResult)]
    forall b a.
    NFData b =>
    [SMTConfig]
    -> (SMTConfig -> a -> IO b)
    -> a
    -> IO [(Solver, NominalDiffTime, b)]
    `sbvWithAll` SMTConfig -> a -> IO SatResult
    forall (m :: * -> *) a.
    SatisfiableM m a =>
    SMTConfig -> a -> m SatResult
    satWith)

    -- | Find a satisfying assignment to a property with multiple solvers, running them in separate threads. Only
    -- the result of the first one to finish will be returned, remaining threads will be killed.
    -- Note that we send an exception to the losing processes, but we do *not* actually wait for them
    -- to finish. In rare cases this can lead to zombie processes. In previous experiments, we found
    -- that some processes take their time to terminate. So, this solution favors quick turnaround.
    satWithAny :: Satisfiable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, SatResult)
    satWithAny :: forall a.
    Satisfiable a =>
    [SMTConfig] -> a -> IO (Solver, NominalDiffTime, SatResult)
    satWithAny = ([SMTConfig]
    -> (SMTConfig -> a -> IO SatResult)
    -> a
    -> IO (Solver, NominalDiffTime, SatResult)
    forall b a.
    NFData b =>
    [SMTConfig]
    -> (SMTConfig -> a -> IO b) -> a -> IO (Solver, NominalDiffTime, b)
    `sbvWithAny` SMTConfig -> a -> IO SatResult
    forall (m :: * -> *) a.
    SatisfiableM m a =>
    SMTConfig -> a -> m SatResult
    satWith)

    -- | Find a satisfying assignment to a property using a single solver, but
    -- providing several query problems of interest, with each query running in a
    -- separate thread and return the first one that returns. This can be useful to
    -- use symbolic mode to drive to a location in the search space of the solver
    -- and then refine the problem in query mode. If the computation is very hard to
    -- solve for the solver than running in concurrent mode may provide a large
    -- performance benefit.
    satConcurrentWithAny :: Satisfiable a => SMTConfig -> [Query b] -> a -> IO (Solver, NominalDiffTime, SatResult)
    satConcurrentWithAny :: forall a b.
    Satisfiable a =>
    SMTConfig
    -> [Query b] -> a -> IO (Solver, NominalDiffTime, SatResult)
    satConcurrentWithAny SMTConfig
    solver [Query b]
    qs a
    a = do (Solver
    slvr,NominalDiffTime
    time,SMTResult
    result) <- SMTConfig
    -> (SMTConfig -> a -> Query b -> IO SMTResult)
    -> [Query b]
    -> a
    -> IO (Solver, NominalDiffTime, SMTResult)
    forall c a (m :: * -> *) b.
    NFData c =>
    SMTConfig
    -> (SMTConfig -> a -> QueryT m b -> IO c)
    -> [QueryT m b]
    -> a
    -> IO (Solver, NominalDiffTime, c)
    sbvConcurrentWithAny SMTConfig
    solver SMTConfig -> a -> Query b -> IO SMTResult
    forall {m :: * -> *} {a} {a}.
    SatisfiableM m a =>
    SMTConfig -> a -> QueryT m a -> m SMTResult
    go [Query b]
    qs a
    a
                                          (Solver, NominalDiffTime, SatResult)
    -> IO (Solver, NominalDiffTime, SatResult)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Solver
    slvr, NominalDiffTime
    time, SMTResult -> SatResult
    SatResult SMTResult
    result)
      where go :: SMTConfig -> a -> QueryT m a -> m SMTResult
    go SMTConfig
    cfg a
    a' QueryT m a
    q = (a -> SymbolicT m SBool)
    -> Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
    forall (m :: * -> *) a b.
    ExtractIO m =>
    (a -> SymbolicT m SBool)
    -> Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery a -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce Bool
    True (do a
    _ <- QueryT m a
    q; QueryT m ()
    forall (m :: * -> *). MonadIO m => QueryT m ()
    checkNoOptimizations QueryT m () -> QueryT m SMTResult -> QueryT m SMTResult
    forall a b. QueryT m a -> QueryT m b -> QueryT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> QueryT m SMTResult
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
    Control.getSMTResult) SMTConfig
    cfg a
    a'

    -- | Find a satisfying assignment to a property using a single solver, but run
    -- each query problem in a separate isolated thread and wait for each thread to
    -- finish. See 'satConcurrentWithAny' for more details.
    satConcurrentWithAll :: Satisfiable a => SMTConfig -> [Query b] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
    satConcurrentWithAll :: forall a b.
    Satisfiable a =>
    SMTConfig
    -> [Query b] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
    satConcurrentWithAll SMTConfig
    solver [Query b]
    qs a
    a = do [(Solver, NominalDiffTime, SMTResult)]
    results <- SMTConfig
    -> (SMTConfig -> a -> Query b -> IO SMTResult)
    -> [Query b]
    -> a
    -> IO [(Solver, NominalDiffTime, SMTResult)]
    forall c a (m :: * -> *) b.
    NFData c =>
    SMTConfig
    -> (SMTConfig -> a -> QueryT m b -> IO c)
    -> [QueryT m b]
    -> a
    -> IO [(Solver, NominalDiffTime, c)]
    sbvConcurrentWithAll SMTConfig
    solver SMTConfig -> a -> Query b -> IO SMTResult
    forall {m :: * -> *} {a} {a}.
    SatisfiableM m a =>
    SMTConfig -> a -> QueryT m a -> m SMTResult
    go [Query b]
    qs a
    a
                                          [(Solver, NominalDiffTime, SatResult)]
    -> IO [(Solver, NominalDiffTime, SatResult)]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(Solver, NominalDiffTime, SatResult)]
     -> IO [(Solver, NominalDiffTime, SatResult)])
    -> [(Solver, NominalDiffTime, SatResult)]
    -> IO [(Solver, NominalDiffTime, SatResult)]
    forall a b. (a -> b) -> a -> b
    $ (\(Solver
    a',NominalDiffTime
    b,SMTResult
    c) -> (Solver
    a',NominalDiffTime
    b,SMTResult -> SatResult
    SatResult SMTResult
    c)) ((Solver, NominalDiffTime, SMTResult)
     -> (Solver, NominalDiffTime, SatResult))
    -> [(Solver, NominalDiffTime, SMTResult)]
    -> [(Solver, NominalDiffTime, SatResult)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(Solver, NominalDiffTime, SMTResult)]
    results
      where go :: SMTConfig -> a -> QueryT m a -> m SMTResult
    go SMTConfig
    cfg a
    a' QueryT m a
    q = (a -> SymbolicT m SBool)
    -> Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
    forall (m :: * -> *) a b.
    ExtractIO m =>
    (a -> SymbolicT m SBool)
    -> Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery a -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce Bool
    True (do a
    _ <- QueryT m a
    q; QueryT m ()
    forall (m :: * -> *). MonadIO m => QueryT m ()
    checkNoOptimizations QueryT m () -> QueryT m SMTResult -> QueryT m SMTResult
    forall a b. QueryT m a -> QueryT m b -> QueryT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> QueryT m SMTResult
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
    Control.getSMTResult) SMTConfig
    cfg a
    a'

    -- | A type @a@ is provable if we can turn it into a predicate, i.e., it has to return a boolean.
    -- This class captures essentially prove calls.
    class ExtractIO m => ProvableM m a where
      -- | Reduce an arg, for proof purposes.
      proofArgReduce :: a -> SymbolicT m SBool

      -- | Generalization of 'Data.SBV.prove'
      prove :: a -> m ThmResult
      prove = SMTConfig -> a -> m ThmResult
    forall (m :: * -> *) a.
    ProvableM m a =>
    SMTConfig -> a -> m ThmResult
    proveWith SMTConfig
    defaultSMTCfg

      -- | Generalization of 'Data.SBV.proveWith'
      proveWith :: SMTConfig -> a -> m ThmResult
      proveWith SMTConfig
    cfg a
    a = do SMTResult
    r <- (a -> SymbolicT m SBool)
    -> Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
    forall (m :: * -> *) a b.
    ExtractIO m =>
    (a -> SymbolicT m SBool)
    -> Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery a -> SymbolicT m SBool
    forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
    proofArgReduce Bool
    False (QueryT m ()
    forall (m :: * -> *). MonadIO m => QueryT m ()
    checkNoOptimizations QueryT m () -> QueryT m SMTResult -> QueryT m SMTResult
    forall a b. QueryT m a -> QueryT m b -> QueryT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> QueryT m SMTResult
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
    Control.getSMTResult) SMTConfig
    cfg a
    a
                           SMTResult -> ThmResult
    ThmResult (SMTResult -> ThmResult) -> m SMTResult -> m ThmResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> if SMTConfig -> Bool
    validationRequested SMTConfig
    cfg
                                         then (a -> SymbolicT m SBool)
    -> Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    forall (m :: * -> *) a.
    MonadIO m =>
    (a -> SymbolicT m SBool)
    -> Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    validate a -> SymbolicT m SBool
    forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
    proofArgReduce Bool
    False SMTConfig
    cfg a
    a SMTResult
    r
                                         else SMTResult -> m SMTResult
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTResult
    r

      -- | Generalization of 'Data.SBV.dprove'
      dprove :: a -> m ThmResult
      dprove = SMTConfig -> a -> m ThmResult
    forall (m :: * -> *) a.
    ProvableM m a =>
    SMTConfig -> a -> m ThmResult
    dproveWith SMTConfig
    defaultDeltaSMTCfg

      -- | Generalization of 'Data.SBV.dproveWith'
      dproveWith :: SMTConfig -> a -> m ThmResult
      dproveWith SMTConfig
    cfg a
    a = do SMTResult
    r <- (a -> SymbolicT m SBool)
    -> Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
    forall (m :: * -> *) a b.
    ExtractIO m =>
    (a -> SymbolicT m SBool)
    -> Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery a -> SymbolicT m SBool
    forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
    proofArgReduce Bool
    False (QueryT m ()
    forall (m :: * -> *). MonadIO m => QueryT m ()
    checkNoOptimizations QueryT m () -> QueryT m SMTResult -> QueryT m SMTResult
    forall a b. QueryT m a -> QueryT m b -> QueryT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> QueryT m SMTResult
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
    Control.getSMTResult) SMTConfig
    cfg a
    a
                            SMTResult -> ThmResult
    ThmResult (SMTResult -> ThmResult) -> m SMTResult -> m ThmResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> if SMTConfig -> Bool
    validationRequested SMTConfig
    cfg
                                          then (a -> SymbolicT m SBool)
    -> Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    forall (m :: * -> *) a.
    MonadIO m =>
    (a -> SymbolicT m SBool)
    -> Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    validate a -> SymbolicT m SBool
    forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
    proofArgReduce Bool
    False SMTConfig
    cfg a
    a SMTResult
    r
                                          else SMTResult -> m SMTResult
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTResult
    r

      -- | Generalization of 'Data.SBV.isVacuousProof'
      isVacuousProof :: a -> m Bool
      isVacuousProof = SMTConfig -> a -> m Bool
    forall (m :: * -> *) a. ProvableM m a => SMTConfig -> a -> m Bool
    isVacuousProofWith SMTConfig
    defaultSMTCfg

      -- | Generalization of 'Data.SBV.isVacuousProofWith'
      isVacuousProofWith :: SMTConfig -> a -> m Bool
      isVacuousProofWith SMTConfig
    cfg a
    a = -- NB. Can't call runWithQuery since last constraint would become the implication!
           (Bool, Result) -> Bool
    forall a b. (a, b) -> a
    fst ((Bool, Result) -> Bool) -> m (Bool, Result) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SMTConfig -> SBVRunMode -> SymbolicT m Bool -> m (Bool, Result)
    forall (m :: * -> *) a.
    MonadIO m =>
    SMTConfig -> SBVRunMode -> SymbolicT m a -> m (a, Result)
    runSymbolic SMTConfig
    cfg (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
    SMTMode QueryContext
    QueryInternal IStage
    ISetup Bool
    True SMTConfig
    cfg) (a -> SymbolicT m SBool
    forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
    proofArgReduce a
    a SymbolicT m SBool -> SymbolicT m Bool -> SymbolicT m Bool
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> QueryContext -> QueryT m Bool -> SymbolicT m Bool
    forall (m :: * -> *) a.
    ExtractIO m =>
    QueryContext -> QueryT m a -> SymbolicT m a
    Control.executeQuery QueryContext
    QueryInternal QueryT m Bool
    check)
         where
           check :: QueryT m Bool
    check = do CheckSatResult
    cs <- QueryT m CheckSatResult
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
    Control.checkSat
                      case CheckSatResult
    cs of
                        CheckSatResult
    Control.Unsat  -> Bool -> QueryT m Bool
    forall a. a -> QueryT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
                        CheckSatResult
    Control.Sat    -> Bool -> QueryT m Bool
    forall a. a -> QueryT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
                        Control.DSat{} -> Bool -> QueryT m Bool
    forall a. a -> QueryT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
                        CheckSatResult
    Control.Unk    -> String -> QueryT m Bool
    forall a. HasCallStack => String -> a
    error String
    "SBV: isVacuous: Solver returned unknown!"

      -- | Generalization of 'Data.SBV.isTheorem'
      isTheorem :: a -> m Bool
      isTheorem = SMTConfig -> a -> m Bool
    forall (m :: * -> *) a. ProvableM m a => SMTConfig -> a -> m Bool
    isTheoremWith SMTConfig
    defaultSMTCfg

      -- | Generalization of 'Data.SBV.isTheoremWith'
      isTheoremWith :: SMTConfig -> a -> m Bool
      isTheoremWith SMTConfig
    cfg a
    p = do ThmResult
    r <- SMTConfig -> a -> m ThmResult
    forall (m :: * -> *) a.
    ProvableM m a =>
    SMTConfig -> a -> m ThmResult
    proveWith SMTConfig
    cfg a
    p
                               let bad :: a
    bad = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.isTheorem: Received:\n" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ThmResult -> String
    forall a. Show a => a -> String
    show ThmResult
    r
                               case ThmResult
    r of
                                 ThmResult Unsatisfiable{} -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
                                 ThmResult Satisfiable{}   -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
                                 ThmResult DeltaSat{}      -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
                                 ThmResult SatExtField{}   -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
                                 ThmResult Unknown{}       -> m Bool
    forall {a}. a
    bad
                                 ThmResult ProofError{}    -> m Bool
    forall {a}. a
    bad

    -- | Prove a property with multiple solvers, running them in separate threads. Only
    -- the result of the first one to finish will be returned, remaining threads will be killed.
    -- Note that we send an exception to the losing processes, but we do *not* actually wait for them
    -- to finish. In rare cases this can lead to zombie processes. In previous experiments, we found
    -- that some processes take their time to terminate. So, this solution favors quick turnaround.
    proveWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, ThmResult)
    proveWithAny :: forall a.
    Provable a =>
    [SMTConfig] -> a -> IO (Solver, NominalDiffTime, ThmResult)
    proveWithAny  = ([SMTConfig]
    -> (SMTConfig -> a -> IO ThmResult)
    -> a
    -> IO (Solver, NominalDiffTime, ThmResult)
    forall b a.
    NFData b =>
    [SMTConfig]
    -> (SMTConfig -> a -> IO b) -> a -> IO (Solver, NominalDiffTime, b)
    `sbvWithAny` SMTConfig -> a -> IO ThmResult
    forall (m :: * -> *) a.
    ProvableM m a =>
    SMTConfig -> a -> m ThmResult
    proveWith)

    -- | Prove a property with multiple solvers, running them in separate threads. The
    -- results will be returned in the order produced.
    proveWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
    proveWithAll :: forall a.
    Provable a =>
    [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
    proveWithAll  = ([SMTConfig]
    -> (SMTConfig -> a -> IO ThmResult)
    -> a
    -> IO [(Solver, NominalDiffTime, ThmResult)]
    forall b a.
    NFData b =>
    [SMTConfig]
    -> (SMTConfig -> a -> IO b)
    -> a
    -> IO [(Solver, NominalDiffTime, b)]
    `sbvWithAll` SMTConfig -> a -> IO ThmResult
    forall (m :: * -> *) a.
    ProvableM m a =>
    SMTConfig -> a -> m ThmResult
    proveWith)

    -- | Prove a property by running many queries each isolated to their own thread
    -- concurrently and return the first that finishes, killing the others
    proveConcurrentWithAny :: Provable a => SMTConfig -> [Query b] -> a -> IO (Solver, NominalDiffTime, ThmResult)
    proveConcurrentWithAny :: forall a b.
    Provable a =>
    SMTConfig
    -> [Query b] -> a -> IO (Solver, NominalDiffTime, ThmResult)
    proveConcurrentWithAny SMTConfig
    solver [Query b]
    qs a
    a = do (Solver
    slvr,NominalDiffTime
    time,SMTResult
    result) <- SMTConfig
    -> (SMTConfig -> a -> Query b -> IO SMTResult)
    -> [Query b]
    -> a
    -> IO (Solver, NominalDiffTime, SMTResult)
    forall c a (m :: * -> *) b.
    NFData c =>
    SMTConfig
    -> (SMTConfig -> a -> QueryT m b -> IO c)
    -> [QueryT m b]
    -> a
    -> IO (Solver, NominalDiffTime, c)
    sbvConcurrentWithAny SMTConfig
    solver SMTConfig -> a -> Query b -> IO SMTResult
    forall {m :: * -> *} {a} {a}.
    ProvableM m a =>
    SMTConfig -> a -> QueryT m a -> m SMTResult
    go [Query b]
    qs a
    a
                                            (Solver, NominalDiffTime, ThmResult)
    -> IO (Solver, NominalDiffTime, ThmResult)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Solver
    slvr, NominalDiffTime
    time, SMTResult -> ThmResult
    ThmResult SMTResult
    result)
      where go :: SMTConfig -> a -> QueryT m a -> m SMTResult
    go SMTConfig
    cfg a
    a' QueryT m a
    q = (a -> SymbolicT m SBool)
    -> Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
    forall (m :: * -> *) a b.
    ExtractIO m =>
    (a -> SymbolicT m SBool)
    -> Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery a -> SymbolicT m SBool
    forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
    proofArgReduce Bool
    False (do a
    _ <- QueryT m a
    q;  QueryT m ()
    forall (m :: * -> *). MonadIO m => QueryT m ()
    checkNoOptimizations QueryT m () -> QueryT m SMTResult -> QueryT m SMTResult
    forall a b. QueryT m a -> QueryT m b -> QueryT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> QueryT m SMTResult
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
    Control.getSMTResult) SMTConfig
    cfg a
    a'

    -- | Prove a property by running many queries each isolated to their own thread
    -- concurrently and wait for each to finish returning all results
    proveConcurrentWithAll :: Provable a => SMTConfig -> [Query b] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
    proveConcurrentWithAll :: forall a b.
    Provable a =>
    SMTConfig
    -> [Query b] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
    proveConcurrentWithAll SMTConfig
    solver [Query b]
    qs a
    a = do [(Solver, NominalDiffTime, SMTResult)]
    results <- SMTConfig
    -> (SMTConfig -> a -> Query b -> IO SMTResult)
    -> [Query b]
    -> a
    -> IO [(Solver, NominalDiffTime, SMTResult)]
    forall c a (m :: * -> *) b.
    NFData c =>
    SMTConfig
    -> (SMTConfig -> a -> QueryT m b -> IO c)
    -> [QueryT m b]
    -> a
    -> IO [(Solver, NominalDiffTime, c)]
    sbvConcurrentWithAll SMTConfig
    solver SMTConfig -> a -> Query b -> IO SMTResult
    forall {m :: * -> *} {a} {a}.
    ProvableM m a =>
    SMTConfig -> a -> QueryT m a -> m SMTResult
    go [Query b]
    qs a
    a
                                            [(Solver, NominalDiffTime, ThmResult)]
    -> IO [(Solver, NominalDiffTime, ThmResult)]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(Solver, NominalDiffTime, ThmResult)]
     -> IO [(Solver, NominalDiffTime, ThmResult)])
    -> [(Solver, NominalDiffTime, ThmResult)]
    -> IO [(Solver, NominalDiffTime, ThmResult)]
    forall a b. (a -> b) -> a -> b
    $ (\(Solver
    a',NominalDiffTime
    b,SMTResult
    c) -> (Solver
    a',NominalDiffTime
    b,SMTResult -> ThmResult
    ThmResult SMTResult
    c)) ((Solver, NominalDiffTime, SMTResult)
     -> (Solver, NominalDiffTime, ThmResult))
    -> [(Solver, NominalDiffTime, SMTResult)]
    -> [(Solver, NominalDiffTime, ThmResult)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(Solver, NominalDiffTime, SMTResult)]
    results
      where go :: SMTConfig -> a -> QueryT m a -> m SMTResult
    go SMTConfig
    cfg a
    a' QueryT m a
    q = (a -> SymbolicT m SBool)
    -> Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
    forall (m :: * -> *) a b.
    ExtractIO m =>
    (a -> SymbolicT m SBool)
    -> Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery a -> SymbolicT m SBool
    forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
    proofArgReduce Bool
    False (do a
    _ <- QueryT m a
    q; QueryT m ()
    forall (m :: * -> *). MonadIO m => QueryT m ()
    checkNoOptimizations QueryT m () -> QueryT m SMTResult -> QueryT m SMTResult
    forall a b. QueryT m a -> QueryT m b -> QueryT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> QueryT m SMTResult
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
    Control.getSMTResult) SMTConfig
    cfg a
    a'

    -- | Validate a model obtained from the solver
    validate :: MonadIO m => (a -> SymbolicT m SBool) -> Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    validate :: forall (m :: * -> *) a.
    MonadIO m =>
    (a -> SymbolicT m SBool)
    -> Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    validate a -> SymbolicT m SBool
    reducer Bool
    isSAT SMTConfig
    cfg a
    p SMTResult
    res =
         case SMTResult
    res of
           Unsatisfiable{} -> SMTResult -> m SMTResult
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTResult
    res
           Satisfiable SMTConfig
    _ SMTModel
    m -> case SMTModel -> Maybe [(NamedSymVar, CV)]
    modelBindings SMTModel
    m of
                                Maybe [(NamedSymVar, CV)]
    Nothing  -> String -> m SMTResult
    forall a. HasCallStack => String -> a
    error String
    "Data.SBV.validate: Impossible happened; no bindings generated during model validation."
                                Just [(NamedSymVar, CV)]
    env -> [(NamedSymVar, CV)] -> m SMTResult
    check [(NamedSymVar, CV)]
    env

           DeltaSat {}     -> [String] -> m SMTResult
    forall {m :: * -> *}. Monad m => [String] -> m SMTResult
    cant [ String
    "The model is delta-satisfiable."
                                   , String
    "Cannot validate delta-satisfiable models."
                                   ]

           SatExtField{}   -> [String] -> m SMTResult
    forall {m :: * -> *}. Monad m => [String] -> m SMTResult
    cant [ String
    "The model requires an extension field value."
                                   , String
    "Cannot validate models with infinities/epsilons produced during optimization."
                                   , String
    ""
                                   , String
    "To turn validation off, use `cfg{optimizeValidateConstraints = False}`"
                                   ]

           Unknown{}       -> SMTResult -> m SMTResult
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTResult
    res
           ProofError{}    -> SMTResult -> m SMTResult
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTResult
    res

      where cant :: [String] -> m SMTResult
    cant [String]
    msg = SMTResult -> m SMTResult
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SMTResult -> m SMTResult) -> SMTResult -> m SMTResult
    forall a b. (a -> b) -> a -> b
    $ SMTConfig -> [String] -> Maybe SMTResult -> SMTResult
    ProofError SMTConfig
    cfg ([String]
    msg [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    ""
                                                       , String
    "Unable to validate the produced model."
                                                       ]) (SMTResult -> Maybe SMTResult
    forall a. a -> Maybe a
    Just SMTResult
    res)

            check :: [(NamedSymVar, CV)] -> m SMTResult
    check [(NamedSymVar, CV)]
    env = do let envShown :: String
    envShown = Bool -> Bool -> SMTConfig -> [(String, GeneralizedCV)] -> String
    showModelDictionary Bool
    True Bool
    True SMTConfig
    cfg [(String, GeneralizedCV)]
    modelBinds
                                  where modelBinds :: [(String, GeneralizedCV)]
    modelBinds = [(Text -> String
    T.unpack Text
    n, CV -> GeneralizedCV
    RegularCV CV
    v) | (NamedSymVar SV
    _ Text
    n, CV
    v) <- [(NamedSymVar, CV)]
    env]

                               notify :: String -> m ()
    notify String
    s
                                 | Bool -> Bool
    not (SMTConfig -> Bool
    verbose SMTConfig
    cfg) = () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                                 | Bool
    True              = SMTConfig -> [String] -> m ()
    forall (m :: * -> *). MonadIO m => SMTConfig -> [String] -> m ()
    debug SMTConfig
    cfg [String
    "[VALIDATE] " String -> String -> String
    `alignPlain` String
    s]

                           String -> m ()
    forall {m :: * -> *}. MonadIO m => String -> m ()
    notify (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Validating the model. " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ if [(NamedSymVar, CV)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(NamedSymVar, CV)]
    env then String
    "There are no assignments." else String
    "Assignment:"
                           (String -> m ()) -> [String] -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ String -> m ()
    forall {m :: * -> *}. MonadIO m => String -> m ()
    notify [String
    "    " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    l | String
    l <- String -> [String]
    lines String
    envShown]

                           Result
    result <- (SBool, Result) -> Result
    forall a b. (a, b) -> b
    snd ((SBool, Result) -> Result) -> m (SBool, Result) -> m Result
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SMTConfig -> SBVRunMode -> SymbolicT m SBool -> m (SBool, Result)
    forall (m :: * -> *) a.
    MonadIO m =>
    SMTConfig -> SBVRunMode -> SymbolicT m a -> m (a, Result)
    runSymbolic SMTConfig
    cfg (Maybe (Bool, [(NamedSymVar, CV)]) -> SBVRunMode
    Concrete ((Bool, [(NamedSymVar, CV)]) -> Maybe (Bool, [(NamedSymVar, CV)])
    forall a. a -> Maybe a
    Just (Bool
    isSAT, [(NamedSymVar, CV)]
    env))) (a -> SymbolicT m SBool
    reducer a
    p SymbolicT m SBool
    -> (SBool -> SymbolicT m SBool) -> SymbolicT m SBool
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= SBool -> SymbolicT m SBool
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBool -> m SBool
    output)

                           let explain :: [String]
    explain  = [ String
    ""
                                          , String
    "Assignment:"  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ if [(NamedSymVar, CV)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(NamedSymVar, CV)]
    env then String
    " <none>" else String
    ""
                                          ]
                                       [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    ""          | Bool -> Bool
    not ([(NamedSymVar, CV)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(NamedSymVar, CV)]
    env)]
                                       [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "    " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    l | String
    l <- String -> [String]
    lines String
    envShown]
                                       [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "" ]

                               wrap :: String -> [String] -> m SMTResult
    wrap String
    tag [String]
    extras = SMTResult -> m SMTResult
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SMTResult -> m SMTResult) -> SMTResult -> m SMTResult
    forall a b. (a -> b) -> a -> b
    $ SMTConfig -> [String] -> Maybe SMTResult -> SMTResult
    ProofError SMTConfig
    cfg (String
    tag String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    explain [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    extras) (SMTResult -> Maybe SMTResult
    forall a. a -> Maybe a
    Just SMTResult
    res)

                               giveUp :: String -> m SMTResult
    giveUp   String
    s     = String -> [String] -> m SMTResult
    forall {m :: * -> *}. Monad m => String -> [String] -> m SMTResult
    wrap (String
    "Data.SBV: Cannot validate the model: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s)
                                                     [ String
    "SBV's model validator is incomplete, and cannot handle this particular case."
                                                     , String
    "Please report this as a feature request or possibly a bug!"
                                                     ]

                               badModel :: String -> m SMTResult
    badModel String
    s     = String -> [String] -> m SMTResult
    forall {m :: * -> *}. Monad m => String -> [String] -> m SMTResult
    wrap (String
    "Data.SBV: Model validation failure: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s)
                                                     [ String
    "Backend solver returned a model that does not satisfy the constraints."
                                                     , String
    "This could indicate a bug in the backend solver, or SBV itself. Please report."
                                                     ]

                               notConcrete :: SV -> m SMTResult
    notConcrete SV
    sv = String -> [String] -> m SMTResult
    forall {m :: * -> *}. Monad m => String -> [String] -> m SMTResult
    wrap (String
    "Data.SBV: Cannot validate the model, since " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    sv String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " is not concretely computable.")
                                                     (  Maybe String -> [String]
    perhaps (SV -> Maybe String
    why SV
    sv)
                                                     [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "SBV's model validator is incomplete, and cannot handle this particular case."
                                                        , String
    "Please report this as a feature request or possibly a bug!"
                                                        ]
                                                     )
                                    where perhaps :: Maybe String -> [String]
    perhaps Maybe String
    Nothing  = []
                                          perhaps (Just String
    x) = [String
    x, String
    ""]

                                          -- This is incomplete, but should capture the most common cases
                                          why :: SV -> Maybe String
    why SV
    s = case SV
    s SV -> [(SV, SBVExpr)] -> Maybe SBVExpr
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    `lookup` Seq (SV, SBVExpr) -> [(SV, SBVExpr)]
    forall a. Seq a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    S.toList (SBVPgm -> Seq (SV, SBVExpr)
    pgmAssignments (Result -> SBVPgm
    resAsgns Result
    result)) of
                                                    Maybe SBVExpr
    Nothing            -> Maybe String
    forall a. Maybe a
    Nothing
                                                    Just (SBVApp Op
    o [SV]
    as) -> case Op
    o of
                                                                            Uninterpreted String
    v  -> String -> Maybe String
    forall a. a -> Maybe a
    Just (String -> Maybe String) -> String -> Maybe String
    forall a b. (a -> b) -> a -> b
    $ String
    "The value depends on the uninterpreted constant " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    v String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "."
                                                                            QuantifiedBool String
    _ -> String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "The value depends on a quantified variable."
                                                                            IEEEFP FPOp
    FP_FMA    -> String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "Floating point FMA operation is not supported concretely."
                                                                            IEEEFP FPOp
    _         -> String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "Not all floating point operations are supported concretely."
                                                                            OverflowOp OvOp
    _     -> String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "Overflow-checking is not done concretely."
                                                                            Op
    _                -> [String] -> Maybe String
    forall a. [a] -> Maybe a
    listToMaybe ([String] -> Maybe String) -> [String] -> Maybe String
    forall a b. (a -> b) -> a -> b
    $ (SV -> Maybe String) -> [SV] -> [String]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe SV -> Maybe String
    why [SV]
    as

                               cstrs :: [(Bool, [(String, String)], SV)]
    cstrs = Seq (Bool, [(String, String)], SV)
    -> [(Bool, [(String, String)], SV)]
    forall a. Seq a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    S.toList (Seq (Bool, [(String, String)], SV)
     -> [(Bool, [(String, String)], SV)])
    -> Seq (Bool, [(String, String)], SV)
    -> [(Bool, [(String, String)], SV)]
    forall a b. (a -> b) -> a -> b
    $ Result -> Seq (Bool, [(String, String)], SV)
    resConstraints Result
    result

                               walkConstraints :: [(Bool, [(String, a)], SV)] -> m SMTResult -> m SMTResult
    walkConstraints [] m SMTResult
    cont = do
                                  Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([(Bool, [(String, String)], SV)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(Bool, [(String, String)], SV)]
    cstrs) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ String -> m ()
    forall {m :: * -> *}. MonadIO m => String -> m ()
    notify String
    "Validated all constraints."
                                  m SMTResult
    cont
                               walkConstraints ((Bool
    isSoft, [(String, a)]
    attrs, SV
    sv) : [(Bool, [(String, a)], SV)]
    rest) m SMTResult
    cont
                                  | SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SV
    sv Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Kind
    KBool
                                  = String -> m SMTResult
    forall {m :: * -> *}. Monad m => String -> m SMTResult
    giveUp (String -> m SMTResult) -> String -> m SMTResult
    forall a b. (a -> b) -> a -> b
    $ String
    "Constraint tied to " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    sv String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " is non-boolean."
                                  | Bool
    isSoft Bool -> Bool -> Bool
    || SV
    sv SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV
                                  = [(Bool, [(String, a)], SV)] -> m SMTResult -> m SMTResult
    walkConstraints [(Bool, [(String, a)], SV)]
    rest m SMTResult
    cont
                                  | SV
    sv SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV
                                  = case Maybe a
    mbName of
                                      Just a
    nm -> String -> m SMTResult
    forall {m :: * -> *}. Monad m => String -> m SMTResult
    badModel (String -> m SMTResult) -> String -> m SMTResult
    forall a b. (a -> b) -> a -> b
    $ String
    "Named constraint " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " evaluated to False."
                                      Maybe a
    Nothing -> String -> m SMTResult
    forall {m :: * -> *}. Monad m => String -> m SMTResult
    badModel String
    "A constraint was violated."
                                  | Bool
    True
                                  = SV -> m SMTResult
    forall {m :: * -> *}. Monad m => SV -> m SMTResult
    notConcrete SV
    sv
                                  where mbName :: Maybe a
    mbName = [a] -> Maybe a
    forall a. [a] -> Maybe a
    listToMaybe [a
    n | (String
    ":named", a
    n) <- [(String, a)]
    attrs]

                               -- SAT: All outputs must be true
                               satLoop :: [SV] -> m SMTResult
    satLoop []
                                 = do String -> m ()
    forall {m :: * -> *}. MonadIO m => String -> m ()
    notify String
    "All outputs are satisfied. Validation complete."
                                      SMTResult -> m SMTResult
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTResult
    res
                               satLoop (SV
    sv:[SV]
    svs)
                                 | SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SV
    sv Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Kind
    KBool
                                 = String -> m SMTResult
    forall {m :: * -> *}. Monad m => String -> m SMTResult
    giveUp (String -> m SMTResult) -> String -> m SMTResult
    forall a b. (a -> b) -> a -> b
    $ String
    "Output tied to " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    sv String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " is non-boolean."
                                 | SV
    sv SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV
                                 = [SV] -> m SMTResult
    satLoop [SV]
    svs
                                 | SV
    sv SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV
                                 = String -> m SMTResult
    forall {m :: * -> *}. Monad m => String -> m SMTResult
    badModel String
    "Final output evaluated to False."
                                 | Bool
    True
                                 = SV -> m SMTResult
    forall {m :: * -> *}. Monad m => SV -> m SMTResult
    notConcrete SV
    sv

                               -- Proof: At least one output must be false
                               proveLoop :: [SV] -> Bool -> m SMTResult
    proveLoop [] Bool
    somethingFailed
                                 | Bool
    somethingFailed = do String -> m ()
    forall {m :: * -> *}. MonadIO m => String -> m ()
    notify String
    "Counterexample is validated."
                                                        SMTResult -> m SMTResult
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTResult
    res
                                 | Bool
    True            = do String -> m ()
    forall {m :: * -> *}. MonadIO m => String -> m ()
    notify String
    "Counterexample violates none of the outputs."
                                                        String -> m SMTResult
    forall {m :: * -> *}. Monad m => String -> m SMTResult
    badModel String
    "Counter-example violates no constraints."
                               proveLoop (SV
    sv:[SV]
    svs) Bool
    somethingFailed
                                 | SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SV
    sv Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Kind
    KBool
                                 = String -> m SMTResult
    forall {m :: * -> *}. Monad m => String -> m SMTResult
    giveUp (String -> m SMTResult) -> String -> m SMTResult
    forall a b. (a -> b) -> a -> b
    $ String
    "Output tied to " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    sv String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " is non-boolean."
                                 | SV
    sv SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV
                                 = [SV] -> Bool -> m SMTResult
    proveLoop [SV]
    svs Bool
    somethingFailed
                                 | SV
    sv SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV
                                 = [SV] -> Bool -> m SMTResult
    proveLoop [SV]
    svs Bool
    True
                                 | Bool
    True
                                 = SV -> m SMTResult
    forall {m :: * -> *}. Monad m => SV -> m SMTResult
    notConcrete SV
    sv

                               -- Output checking is tricky, since we behave differently for different modes
                               checkOutputs :: [SV] -> m SMTResult
    checkOutputs []
                                 | [(Bool, [(String, String)], SV)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(Bool, [(String, String)], SV)]
    cstrs
                                 = String -> m SMTResult
    forall {m :: * -> *}. Monad m => String -> m SMTResult
    giveUp String
    "Impossible happened: There are no outputs nor any constraints to check."
                               checkOutputs [SV]
    os
                                 = do String -> m ()
    forall {m :: * -> *}. MonadIO m => String -> m ()
    notify String
    "Validating outputs."
                                      if Bool
    isSAT then [SV] -> m SMTResult
    forall {m :: * -> *}. MonadIO m => [SV] -> m SMTResult
    satLoop   [SV]
    os
                                               else [SV] -> Bool -> m SMTResult
    forall {m :: * -> *}. MonadIO m => [SV] -> Bool -> m SMTResult
    proveLoop [SV]
    os Bool
    False

                           String -> m ()
    forall {m :: * -> *}. MonadIO m => String -> m ()
    notify (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ if [(Bool, [(String, String)], SV)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(Bool, [(String, String)], SV)]
    cstrs
                                    then String
    "There are no constraints to check."
                                    else String
    "Validating " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show ([(Bool, [(String, String)], SV)] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [(Bool, [(String, String)], SV)]
    cstrs) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " constraint(s)."

                           [(Bool, [(String, String)], SV)] -> m SMTResult -> m SMTResult
    forall {m :: * -> *} {a}.
    (MonadIO m, Show a) =>
    [(Bool, [(String, a)], SV)] -> m SMTResult -> m SMTResult
    walkConstraints [(Bool, [(String, String)], SV)]
    cstrs ([SV] -> m SMTResult
    forall {m :: * -> *}. MonadIO m => [SV] -> m SMTResult
    checkOutputs (Result -> [SV]
    resOutputs Result
    result))

    -- | Create an SMT-Lib2 benchmark, for a SAT query.
    generateSMTBenchmarkSat :: SatisfiableM m a => a -> m String
    generateSMTBenchmarkSat :: forall (m :: * -> *) a. SatisfiableM m a => a -> m String
    generateSMTBenchmarkSat = Bool -> (a -> SymbolicT m SBool) -> a -> m String
    forall (m :: * -> *) a.
    MonadIO m =>
    Bool -> (a -> SymbolicT m SBool) -> a -> m String
    generateSMTBenchMarkGen Bool
    True a -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce

    -- | Create an SMT-Lib2 benchmark, for a Proof query.
    generateSMTBenchmarkProof :: ProvableM m a => a -> m String
    generateSMTBenchmarkProof :: forall (m :: * -> *) a. ProvableM m a => a -> m String
    generateSMTBenchmarkProof = Bool -> (a -> SymbolicT m SBool) -> a -> m String
    forall (m :: * -> *) a.
    MonadIO m =>
    Bool -> (a -> SymbolicT m SBool) -> a -> m String
    generateSMTBenchMarkGen Bool
    False a -> SymbolicT m SBool
    forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
    proofArgReduce

    -- | Generic benchmark creator
    generateSMTBenchMarkGen :: MonadIO m => Bool -> (a -> SymbolicT m SBool) -> a -> m String
    generateSMTBenchMarkGen :: forall (m :: * -> *) a.
    MonadIO m =>
    Bool -> (a -> SymbolicT m SBool) -> a -> m String
    generateSMTBenchMarkGen Bool
    isSat a -> SymbolicT m SBool
    reduce a
    a = do
          ZonedTime
    t <- IO ZonedTime -> m ZonedTime
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO ZonedTime
    getZonedTime

          let comments :: [String]
    comments = [String
    "Automatically created by SBV on " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ZonedTime -> String
    forall a. Show a => a -> String
    show ZonedTime
    t]
              cfg :: SMTConfig
    cfg      = SMTConfig
    defaultSMTCfg { smtLibVersion :: SMTLibVersion
    smtLibVersion = SMTLibVersion
    SMTLib2 }

          (SBool
    _, Result
    res) <- SMTConfig -> SBVRunMode -> SymbolicT m SBool -> m (SBool, Result)
    forall (m :: * -> *) a.
    MonadIO m =>
    SMTConfig -> SBVRunMode -> SymbolicT m a -> m (a, Result)
    runSymbolic SMTConfig
    cfg (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
    SMTMode QueryContext
    QueryInternal IStage
    ISetup Bool
    isSat SMTConfig
    cfg) (SymbolicT m SBool -> m (SBool, Result))
    -> SymbolicT m SBool -> m (SBool, Result)
    forall a b. (a -> b) -> a -> b
    $ a -> SymbolicT m SBool
    reduce a
    a SymbolicT m SBool
    -> (SBool -> SymbolicT m SBool) -> SymbolicT m SBool
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= SBool -> SymbolicT m SBool
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBool -> m SBool
    output

          let SMTProblem{SMTConfig -> SMTLibPgm
    smtLibPgm :: SMTConfig -> SMTLibPgm
    smtLibPgm :: SMTProblem -> SMTConfig -> SMTLibPgm
    smtLibPgm} = SBVRunMode -> QueryContext -> [String] -> Result -> SMTProblem
    Control.runProofOn (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
    SMTMode QueryContext
    QueryInternal IStage
    IRun Bool
    isSat SMTConfig
    cfg) QueryContext
    QueryInternal [String]
    comments Result
    res
              out :: String
    out                   = SMTLibPgm -> String
    forall a. Show a => a -> String
    show (SMTConfig -> SMTLibPgm
    smtLibPgm SMTConfig
    cfg)

          String -> m String
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> m String) -> String -> m String
    forall a b. (a -> b) -> a -> b
    $ String
    out String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "\n(check-sat)\n"

    checkNoOptimizations :: MonadIO m => QueryT m ()
    checkNoOptimizations :: forall (m :: * -> *). MonadIO m => QueryT m ()
    checkNoOptimizations = do [Objective (SV, SV)]
    objectives <- QueryT m [Objective (SV, SV)]
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m [Objective (SV, SV)]
    Control.getObjectives

                              Bool -> QueryT m () -> QueryT m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([Objective (SV, SV)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Objective (SV, SV)]
    objectives) (QueryT m () -> QueryT m ()) -> QueryT m () -> QueryT m ()
    forall a b. (a -> b) -> a -> b
    $
                                    String -> QueryT m ()
    forall a. HasCallStack => String -> a
    error (String -> QueryT m ()) -> String -> QueryT m ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    ""
                                                    , String
    "*** Data.SBV: Unsupported call sat/prove when optimization objectives are present."
                                                    , String
    "*** Use \"optimize\"/\"optimizeWith\" to calculate optimal satisfaction!"
                                                    ]

    instance ExtractIO m => SatisfiableM m (SymbolicT m ()) where satArgReduce :: SymbolicT m () -> SymbolicT m SBool
    satArgReduce SymbolicT m ()
    a = SymbolicT m SBool -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce ((SymbolicT m ()
    a SymbolicT m () -> SymbolicT m SBool -> SymbolicT m SBool
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBool -> SymbolicT m SBool
    forall a. a -> SymbolicT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SBool
    sTrue) :: SymbolicT m SBool)
    -- instance ExtractIO m => ProvableM m (SymbolicT m ())  -- NO INSTANCE ON PURPOSE; don't want to prove goals

    instance ExtractIO m => SatisfiableM m (SymbolicT m SBool) where satArgReduce :: SymbolicT m SBool -> SymbolicT m SBool
    satArgReduce   = SymbolicT m SBool -> SymbolicT m SBool
    forall a. a -> a
    id
    instance ExtractIO m => ProvableM    m (SymbolicT m SBool) where proofArgReduce :: SymbolicT m SBool -> SymbolicT m SBool
    proofArgReduce = SymbolicT m SBool -> SymbolicT m SBool
    forall a. a -> a
    id

    instance ExtractIO m => SatisfiableM m SBool where satArgReduce :: SBool -> SymbolicT m SBool
    satArgReduce   = SBool -> SymbolicT m SBool
    forall a. a -> SymbolicT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
    instance ExtractIO m => ProvableM    m SBool where proofArgReduce :: SBool -> SymbolicT m SBool
    proofArgReduce = SBool -> SymbolicT m SBool
    forall a. a -> SymbolicT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return

    instance (ExtractIO m, SymVal a, Constraint Symbolic r, SatisfiableM m r) => SatisfiableM m (Forall nm a -> r) where
      satArgReduce :: (Forall nm a -> r) -> SymbolicT m SBool
    satArgReduce = SBool -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce (SBool -> SymbolicT m SBool)
    -> ((Forall nm a -> r) -> SBool)
    -> (Forall nm a -> r)
    -> SymbolicT m SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Forall nm a -> r) -> SBool
    forall a. QuantifiedBool a => a -> SBool
    quantifiedBool

    instance (ExtractIO m, SymVal a, Constraint Symbolic r, ProvableM m r) => ProvableM m (Forall nm a -> r) where
      proofArgReduce :: (Forall nm a -> r) -> SymbolicT m SBool
    proofArgReduce = SBool -> SymbolicT m SBool
    forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
    proofArgReduce (SBool -> SymbolicT m SBool)
    -> ((Forall nm a -> r) -> SBool)
    -> (Forall nm a -> r)
    -> SymbolicT m SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Forall nm a -> r) -> SBool
    forall a. QuantifiedBool a => a -> SBool
    quantifiedBool

    instance (ExtractIO m, SymVal a, Constraint Symbolic r, SatisfiableM m r) => SatisfiableM m (Exists nm a -> r) where
      satArgReduce :: (Exists nm a -> r) -> SymbolicT m SBool
    satArgReduce = SBool -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce (SBool -> SymbolicT m SBool)
    -> ((Exists nm a -> r) -> SBool)
    -> (Exists nm a -> r)
    -> SymbolicT m SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Exists nm a -> r) -> SBool
    forall a. QuantifiedBool a => a -> SBool
    quantifiedBool

    instance (ExtractIO m, SymVal a, Constraint Symbolic r, SatisfiableM m r, EqSymbolic (SBV a)) => SatisfiableM m (ExistsUnique nm a -> r) where
      satArgReduce :: (ExistsUnique nm a -> r) -> SymbolicT m SBool
    satArgReduce = SBool -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce (SBool -> SymbolicT m SBool)
    -> ((ExistsUnique nm a -> r) -> SBool)
    -> (ExistsUnique nm a -> r)
    -> SymbolicT m SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ExistsUnique nm a -> r) -> SBool
    forall a. QuantifiedBool a => a -> SBool
    quantifiedBool

    instance (KnownNat n, ExtractIO m, SymVal a, Constraint Symbolic r, ProvableM m r) => ProvableM m (ForallN n nm a -> r) where
      proofArgReduce :: (ForallN n nm a -> r) -> SymbolicT m SBool
    proofArgReduce = SBool -> SymbolicT m SBool
    forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
    proofArgReduce (SBool -> SymbolicT m SBool)
    -> ((ForallN n nm a -> r) -> SBool)
    -> (ForallN n nm a -> r)
    -> SymbolicT m SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ForallN n nm a -> r) -> SBool
    forall a. QuantifiedBool a => a -> SBool
    quantifiedBool

    instance (KnownNat n, ExtractIO m, SymVal a, Constraint Symbolic r, SatisfiableM m r) => SatisfiableM m (ExistsN n nm a -> r) where
      satArgReduce :: (ExistsN n nm a -> r) -> SymbolicT m SBool
    satArgReduce = SBool -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce (SBool -> SymbolicT m SBool)
    -> ((ExistsN n nm a -> r) -> SBool)
    -> (ExistsN n nm a -> r)
    -> SymbolicT m SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ExistsN n nm a -> r) -> SBool
    forall a. QuantifiedBool a => a -> SBool
    quantifiedBool

    instance (ExtractIO m, SymVal a, Constraint Symbolic r, ProvableM m r) => ProvableM m (Exists nm a -> r) where
      proofArgReduce :: (Exists nm a -> r) -> SymbolicT m SBool
    proofArgReduce = SBool -> SymbolicT m SBool
    forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
    proofArgReduce (SBool -> SymbolicT m SBool)
    -> ((Exists nm a -> r) -> SBool)
    -> (Exists nm a -> r)
    -> SymbolicT m SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Exists nm a -> r) -> SBool
    forall a. QuantifiedBool a => a -> SBool
    quantifiedBool

    instance (ExtractIO m, SymVal a, Constraint Symbolic r, ProvableM m r, EqSymbolic (SBV a)) => ProvableM m (ExistsUnique nm a -> r) where
      proofArgReduce :: (ExistsUnique nm a -> r) -> SymbolicT m SBool
    proofArgReduce = SBool -> SymbolicT m SBool
    forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
    proofArgReduce (SBool -> SymbolicT m SBool)
    -> ((ExistsUnique nm a -> r) -> SBool)
    -> (ExistsUnique nm a -> r)
    -> SymbolicT m SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ExistsUnique nm a -> r) -> SBool
    forall a. QuantifiedBool a => a -> SBool
    quantifiedBool

    instance (KnownNat n, ExtractIO m, SymVal a, Constraint Symbolic r, SatisfiableM m r) => SatisfiableM m (ForallN n nm a -> r) where
      satArgReduce :: (ForallN n nm a -> r) -> SymbolicT m SBool
    satArgReduce = SBool -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce (SBool -> SymbolicT m SBool)
    -> ((ForallN n nm a -> r) -> SBool)
    -> (ForallN n nm a -> r)
    -> SymbolicT m SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ForallN n nm a -> r) -> SBool
    forall a. QuantifiedBool a => a -> SBool
    quantifiedBool

    instance (KnownNat n, ExtractIO m, SymVal a, Constraint Symbolic r, ProvableM m r) => ProvableM m (ExistsN n nm a -> r) where
      proofArgReduce :: (ExistsN n nm a -> r) -> SymbolicT m SBool
    proofArgReduce = SBool -> SymbolicT m SBool
    forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
    proofArgReduce (SBool -> SymbolicT m SBool)
    -> ((ExistsN n nm a -> r) -> SBool)
    -> (ExistsN n nm a -> r)
    -> SymbolicT m SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ExistsN n nm a -> r) -> SBool
    forall a. QuantifiedBool a => a -> SBool
    quantifiedBool

    {-
    -- The following is a possible definition, but it lets us write properties that
    -- are not useful.. Such as: prove $ \x y -> (x::SInt8) == y
    -- Running that will throw an exception since Haskell's equality is not be supported by symbolic things. (Needs .==).
    -- So, we avoid these insteances.
    instance ExtractIO m => ProvableM m Bool where
      proofArgReduce x  = proofArgReduce (if x then sTrue else sFalse :: SBool)

    instance ExtractIO m => SatisfiableM m Bool where
      satArgReduce x  = satArgReduce (if x then sTrue else sFalse :: SBool)
    -}

    -- | Create an argument
    mkArg :: (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg :: forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg = VarContext -> Maybe String -> m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    VarContext -> Maybe String -> m (SBV a)
    forall (m :: * -> *).
    MonadSymbolic m =>
    VarContext -> Maybe String -> m (SBV a)
    mkSymVal (Maybe Quantifier -> VarContext
    NonQueryVar Maybe Quantifier
    forall a. Maybe a
    Nothing) Maybe String
    forall a. Maybe a
    Nothing

    -- Functions
    instance (SymVal a, SatisfiableM m p) => SatisfiableM m (SBV a -> p) where
      satArgReduce :: (SBV a -> p) -> SymbolicT m SBool
    satArgReduce SBV a -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SBV a
    a -> p -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ SBV a -> p
    k SBV a
    a

    instance (SymVal a, ProvableM m p) => ProvableM m (SBV a -> p) where
      proofArgReduce :: (SBV a -> p) -> SymbolicT m SBool
    proofArgReduce SBV a -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SBV a
    a -> p -> SymbolicT m SBool
    forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
    proofArgReduce (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ SBV a -> p
    k SBV a
    a

    -- Arrays
    instance (HasKind a, HasKind b, SatisfiableM m p) => SatisfiableM m (SArray a b -> p) where
      satArgReduce :: (SArray a b -> p) -> SymbolicT m SBool
    satArgReduce SArray a b -> p
    k = Maybe (SBV b) -> SymbolicT m (SArray a b)
    forall (m :: * -> *) a b.
    (MonadSymbolic m, HasKind a, HasKind b) =>
    Maybe (SBV b) -> m (SArray a b)
    forall (array :: * -> * -> *) (m :: * -> *) a b.
    (SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
    Maybe (SBV b) -> m (array a b)
    newArray_ Maybe (SBV b)
    forall a. Maybe a
    Nothing SymbolicT m (SArray a b)
    -> (SArray a b -> SymbolicT m SBool) -> SymbolicT m SBool
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SArray a b
    a -> p -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ SArray a b -> p
    k SArray a b
    a

    instance (HasKind a, HasKind b, ProvableM m p) => ProvableM m (SArray a b -> p) where
      proofArgReduce :: (SArray a b -> p) -> SymbolicT m SBool
    proofArgReduce SArray a b -> p
    k = Maybe (SBV b) -> SymbolicT m (SArray a b)
    forall (m :: * -> *) a b.
    (MonadSymbolic m, HasKind a, HasKind b) =>
    Maybe (SBV b) -> m (SArray a b)
    forall (array :: * -> * -> *) (m :: * -> *) a b.
    (SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
    Maybe (SBV b) -> m (array a b)
    newArray_ Maybe (SBV b)
    forall a. Maybe a
    Nothing SymbolicT m (SArray a b)
    -> (SArray a b -> SymbolicT m SBool) -> SymbolicT m SBool
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SArray a b
    a -> p -> SymbolicT m SBool
    forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
    proofArgReduce (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ SArray a b -> p
    k SArray a b
    a

    -- 2 Tuple
    instance (SymVal a, SymVal b, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b) -> p) where
      satArgReduce :: ((SBV a, SBV b) -> p) -> SymbolicT m SBool
    satArgReduce (SBV a, SBV b) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SBV a
    a -> (SBV b -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce ((SBV b -> p) -> SymbolicT m SBool)
    -> (SBV b -> p) -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ \SBV b
    b -> (SBV a, SBV b) -> p
    k (SBV a
    a, SBV b
    b)

    instance (SymVal a, SymVal b, ProvableM m p) => ProvableM m ((SBV a, SBV b) -> p) where
      proofArgReduce :: ((SBV a, SBV b) -> p) -> SymbolicT m SBool
    proofArgReduce (SBV a, SBV b) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SBV a
    a -> (SBV b -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
    proofArgReduce ((SBV b -> p) -> SymbolicT m SBool)
    -> (SBV b -> p) -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ \SBV b
    b -> (SBV a, SBV b) -> p
    k (SBV a
    a, SBV b
    b)

    -- 3 Tuple
    instance (SymVal a, SymVal b, SymVal c, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c) -> p) where
      satArgReduce :: ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
    satArgReduce (SBV a, SBV b, SBV c) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SBV a
    a -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce ((SBV b -> SBV c -> p) -> SymbolicT m SBool)
    -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ \SBV b
    b SBV c
    c -> (SBV a, SBV b, SBV c) -> p
    k (SBV a
    a, SBV b
    b, SBV c
    c)

    instance (SymVal a, SymVal b, SymVal c, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c) -> p) where
      proofArgReduce :: ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
    proofArgReduce (SBV a, SBV b, SBV c) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SBV a
    a -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
    proofArgReduce ((SBV b -> SBV c -> p) -> SymbolicT m SBool)
    -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ \SBV b
    b SBV c
    c -> (SBV a, SBV b, SBV c) -> p
    k (SBV a
    a, SBV b
    b, SBV c
    c)

    -- 4 Tuple
    instance (SymVal a, SymVal b, SymVal c, SymVal d, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d) -> p) where
      satArgReduce :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
    satArgReduce (SBV a, SBV b, SBV c, SBV d) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg  SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SBV a
    a -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce ((SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool)
    -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ \SBV b
    b SBV c
    c SBV d
    d -> (SBV a, SBV b, SBV c, SBV d) -> p
    k (SBV a
    a, SBV b
    b, SBV c
    c, SBV d
    d)

    instance (SymVal a, SymVal b, SymVal c, SymVal d, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d) -> p) where
      proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
    proofArgReduce (SBV a, SBV b, SBV c, SBV d) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg  SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SBV a
    a -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
    proofArgReduce ((SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool)
    -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ \SBV b
    b SBV c
    c SBV d
    d -> (SBV a, SBV b, SBV c, SBV d) -> p
    k (SBV a
    a, SBV b
    b, SBV c
    c, SBV d
    d)

    -- 5 Tuple
    instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) where
      satArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
    satArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SBV a
    a -> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce ((SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool)
    -> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ \SBV b
    b SBV c
    c SBV d
    d SBV e
    e -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
    k (SBV a
    a, SBV b
    b, SBV c
    c, SBV d
    d, SBV e
    e)

    instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) where
      proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
    proofArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SBV a
    a -> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
    proofArgReduce ((SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool)
    -> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ \SBV b
    b SBV c
    c SBV d
    d SBV e
    e -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
    k (SBV a
    a, SBV b
    b, SBV c
    c, SBV d
    d, SBV e
    e)

    -- 6 Tuple
    instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) where
      satArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
    -> SymbolicT m SBool
    satArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SBV a
    a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
    -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
     -> SymbolicT m SBool)
    -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
    -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ \SBV b
    b SBV c
    c SBV d
    d SBV e
    e SBV f
    f -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
    k (SBV a
    a, SBV b
    b, SBV c
    c, SBV d
    d, SBV e
    e, SBV f
    f)

    instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) where
      proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
    -> SymbolicT m SBool
    proofArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SBV a
    a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
    -> SymbolicT m SBool
    forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
    proofArgReduce ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
     -> SymbolicT m SBool)
    -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
    -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ \SBV b
    b SBV c
    c SBV d
    d SBV e
    e SBV f
    f -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
    k (SBV a
    a, SBV b
    b, SBV c
    c, SBV d
    d, SBV e
    e, SBV f
    f)

    -- 7 Tuple
    instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) where
      satArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
    -> SymbolicT m SBool
    satArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SBV a
    a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
    -> SymbolicT m SBool
    forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
    satArgReduce ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
     -> SymbolicT m SBool)
    -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
    -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ \SBV b
    b SBV c
    c SBV d
    d SBV e
    e SBV f
    f SBV g
    g -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
    k (SBV a
    a, SBV b
    b, SBV c
    c, SBV d
    d, SBV e
    e, SBV f
    f, SBV g
    g)

    instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) where
      proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
    -> SymbolicT m SBool
    proofArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SBV a
    a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
    -> SymbolicT m SBool
    forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
    proofArgReduce ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
     -> SymbolicT m SBool)
    -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
    -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ \SBV b
    b SBV c
    c SBV d
    d SBV e
    e SBV f
    f SBV g
    g -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
    k (SBV a
    a, SBV b
    b, SBV c
    c, SBV d
    d, SBV e
    e, SBV f
    f, SBV g
    g)

    -- | Generalization of 'Data.SBV.runSMT'
    runSMT :: MonadIO m => SymbolicT m a -> m a
    runSMT :: forall (m :: * -> *) a. MonadIO m => SymbolicT m a -> m a
    runSMT = SMTConfig -> SymbolicT m a -> m a
    forall (m :: * -> *) a.
    MonadIO m =>
    SMTConfig -> SymbolicT m a -> m a
    runSMTWith SMTConfig
    defaultSMTCfg

    -- | Generalization of 'Data.SBV.runSMTWith'
    runSMTWith :: MonadIO m => SMTConfig -> SymbolicT m a -> m a
    runSMTWith :: forall (m :: * -> *) a.
    MonadIO m =>
    SMTConfig -> SymbolicT m a -> m a
    runSMTWith SMTConfig
    cfg SymbolicT m a
    a = (a, Result) -> a
    forall a b. (a, b) -> a
    fst ((a, Result) -> a) -> m (a, Result) -> m a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SMTConfig -> SBVRunMode -> SymbolicT m a -> m (a, Result)
    forall (m :: * -> *) a.
    MonadIO m =>
    SMTConfig -> SBVRunMode -> SymbolicT m a -> m (a, Result)
    runSymbolic SMTConfig
    cfg (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
    SMTMode QueryContext
    QueryExternal IStage
    ISetup Bool
    True SMTConfig
    cfg) SymbolicT m a
    a

    -- | Runs with a query.
    runWithQuery :: ExtractIO m => (a -> SymbolicT m SBool) -> Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery :: forall (m :: * -> *) a b.
    ExtractIO m =>
    (a -> SymbolicT m SBool)
    -> Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery a -> SymbolicT m SBool
    reducer Bool
    isSAT QueryT m b
    q SMTConfig
    cfg a
    a = (b, Result) -> b
    forall a b. (a, b) -> a
    fst ((b, Result) -> b) -> m (b, Result) -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SMTConfig -> SBVRunMode -> SymbolicT m b -> m (b, Result)
    forall (m :: * -> *) a.
    MonadIO m =>
    SMTConfig -> SBVRunMode -> SymbolicT m a -> m (a, Result)
    runSymbolic SMTConfig
    cfg (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
    SMTMode QueryContext
    QueryInternal IStage
    ISetup Bool
    isSAT SMTConfig
    cfg) SymbolicT m b
    comp
      where comp :: SymbolicT m b
    comp =  do SBool
    _ <- a -> SymbolicT m SBool
    reducer a
    a SymbolicT m SBool
    -> (SBool -> SymbolicT m SBool) -> SymbolicT m SBool
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= SBool -> SymbolicT m SBool
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBool -> m SBool
    output
                       QueryContext -> QueryT m b -> SymbolicT m b
    forall (m :: * -> *) a.
    ExtractIO m =>
    QueryContext -> QueryT m a -> SymbolicT m a
    Control.executeQuery QueryContext
    QueryInternal QueryT m b
    q

    -- | Check if a safe-call was safe or not, turning a 'SafeResult' to a Bool.
    isSafe :: SafeResult -> Bool
    isSafe :: SafeResult -> Bool
    isSafe (SafeResult (Maybe String
    _, String
    _, SMTResult
    result)) = case SMTResult
    result of
                                           Unsatisfiable{} -> Bool
    True
                                           Satisfiable{}   -> Bool
    False
                                           DeltaSat{}      -> Bool
    False   -- conservative
                                           SatExtField{}   -> Bool
    False   -- conservative
                                           Unknown{}       -> Bool
    False   -- conservative
                                           ProofError{}    -> Bool
    False   -- conservative

    -- | Perform an action asynchronously, returning results together with diff-time.
    runInThread :: NFData b => UTCTime -> (SMTConfig -> IO b) -> SMTConfig -> IO (Async (Solver, NominalDiffTime, b))
    runInThread :: forall b.
    NFData b =>
    UTCTime
    -> (SMTConfig -> IO b)
    -> SMTConfig
    -> IO (Async (Solver, NominalDiffTime, b))
    runInThread UTCTime
    beginTime SMTConfig -> IO b
    action SMTConfig
    config = IO (Solver, NominalDiffTime, b)
    -> IO (Async (Solver, NominalDiffTime, b))
    forall a. IO a -> IO (Async a)
    async (IO (Solver, NominalDiffTime, b)
     -> IO (Async (Solver, NominalDiffTime, b)))
    -> IO (Solver, NominalDiffTime, b)
    -> IO (Async (Solver, NominalDiffTime, b))
    forall a b. (a -> b) -> a -> b
    $ do
                    b
    result  <- SMTConfig -> IO b
    action SMTConfig
    config
                    UTCTime
    endTime <- b -> ()
    forall a. NFData a => a -> ()
    rnf b
    result () -> IO UTCTime -> IO UTCTime
    forall a b. a -> b -> b
    `seq` IO UTCTime
    getCurrentTime
                    (Solver, NominalDiffTime, b) -> IO (Solver, NominalDiffTime, b)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SMTSolver -> Solver
    name (SMTConfig -> SMTSolver
    solver SMTConfig
    config), UTCTime
    endTime UTCTime -> UTCTime -> NominalDiffTime
    `diffUTCTime` UTCTime
    beginTime, b
    result)

    -- | Perform action for all given configs, return the first one that wins. Note that we do
    -- not wait for the other asyncs to terminate; hopefully they'll do so quickly.
    sbvWithAny :: NFData b => [SMTConfig] -> (SMTConfig -> a -> IO b) -> a -> IO (Solver, NominalDiffTime, b)
    sbvWithAny :: forall b a.
    NFData b =>
    [SMTConfig]
    -> (SMTConfig -> a -> IO b) -> a -> IO (Solver, NominalDiffTime, b)
    sbvWithAny []      SMTConfig -> a -> IO b
    _    a
    _ = String -> IO (Solver, NominalDiffTime, b)
    forall a. HasCallStack => String -> a
    error String
    "SBV.withAny: No solvers given!"
    sbvWithAny [SMTConfig]
    solvers SMTConfig -> a -> IO b
    what a
    a = do UTCTime
    beginTime <- IO UTCTime
    getCurrentTime
                                   (Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b))
    -> (Solver, NominalDiffTime, b)
    forall a b. (a, b) -> b
    snd ((Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b))
     -> (Solver, NominalDiffTime, b))
    -> IO
         (Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b))
    -> IO (Solver, NominalDiffTime, b)
    forall a b. (a -> b) -> IO a -> IO b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` ((SMTConfig -> IO (Async (Solver, NominalDiffTime, b)))
    -> [SMTConfig] -> IO [Async (Solver, NominalDiffTime, b)]
    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 (UTCTime
    -> (SMTConfig -> IO b)
    -> SMTConfig
    -> IO (Async (Solver, NominalDiffTime, b))
    forall b.
    NFData b =>
    UTCTime
    -> (SMTConfig -> IO b)
    -> SMTConfig
    -> IO (Async (Solver, NominalDiffTime, b))
    runInThread UTCTime
    beginTime (SMTConfig -> a -> IO b
    `what` a
    a)) [SMTConfig]
    solvers IO [Async (Solver, NominalDiffTime, b)]
    -> ([Async (Solver, NominalDiffTime, b)]
        -> IO
             (Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b)))
    -> IO
         (Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b))
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= [Async (Solver, NominalDiffTime, b)]
    -> IO
         (Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b))
    forall {a}. [Async a] -> IO (Async a, a)
    waitAnyFastCancel)
       where -- Async's `waitAnyCancel` nicely blocks; so we use this variant to ignore the
             -- wait part for killed threads.
             waitAnyFastCancel :: [Async a] -> IO (Async a, a)
    waitAnyFastCancel [Async a]
    asyncs = [Async a] -> IO (Async a, a)
    forall {a}. [Async a] -> IO (Async a, a)
    waitAny [Async a]
    asyncs IO (Async a, a) -> IO () -> IO (Async a, a)
    forall a b. IO a -> IO b -> IO a
    `finally` (Async a -> IO ()) -> [Async a] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Async a -> IO ()
    forall {a}. Async a -> IO ()
    cancelFast [Async a]
    asyncs
             cancelFast :: Async a -> IO ()
    cancelFast Async a
    other = ThreadId -> ExitCode -> IO ()
    forall e. Exception e => ThreadId -> e -> IO ()
    throwTo (Async a -> ThreadId
    forall a. Async a -> ThreadId
    asyncThreadId Async a
    other) ExitCode
    ExitSuccess

    sbvConcurrentWithAny :: NFData c => SMTConfig -> (SMTConfig -> a -> QueryT m b -> IO c) -> [QueryT m b] -> a -> IO (Solver, NominalDiffTime, c)
    sbvConcurrentWithAny :: forall c a (m :: * -> *) b.
    NFData c =>
    SMTConfig
    -> (SMTConfig -> a -> QueryT m b -> IO c)
    -> [QueryT m b]
    -> a
    -> IO (Solver, NominalDiffTime, c)
    sbvConcurrentWithAny SMTConfig
    solver SMTConfig -> a -> QueryT m b -> IO c
    what [QueryT m b]
    queries a
    a = (Async (Solver, NominalDiffTime, c), (Solver, NominalDiffTime, c))
    -> (Solver, NominalDiffTime, c)
    forall a b. (a, b) -> b
    snd ((Async (Solver, NominalDiffTime, c), (Solver, NominalDiffTime, c))
     -> (Solver, NominalDiffTime, c))
    -> IO
         (Async (Solver, NominalDiffTime, c), (Solver, NominalDiffTime, c))
    -> IO (Solver, NominalDiffTime, c)
    forall a b. (a -> b) -> IO a -> IO b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` ((QueryT m b -> IO (Async (Solver, NominalDiffTime, c)))
    -> [QueryT m b] -> IO [Async (Solver, NominalDiffTime, c)]
    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 QueryT m b -> IO (Async (Solver, NominalDiffTime, c))
    runQueryInThread [QueryT m b]
    queries IO [Async (Solver, NominalDiffTime, c)]
    -> ([Async (Solver, NominalDiffTime, c)]
        -> IO
             (Async (Solver, NominalDiffTime, c), (Solver, NominalDiffTime, c)))
    -> IO
         (Async (Solver, NominalDiffTime, c), (Solver, NominalDiffTime, c))
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= [Async (Solver, NominalDiffTime, c)]
    -> IO
         (Async (Solver, NominalDiffTime, c), (Solver, NominalDiffTime, c))
    forall {a}. [Async a] -> IO (Async a, a)
    waitAnyFastCancel)
      where  -- Async's `waitAnyCancel` nicely blocks; so we use this variant to ignore the
             -- wait part for killed threads.
             waitAnyFastCancel :: [Async a] -> IO (Async a, a)
    waitAnyFastCancel [Async a]
    asyncs = [Async a] -> IO (Async a, a)
    forall {a}. [Async a] -> IO (Async a, a)
    waitAny [Async a]
    asyncs IO (Async a, a) -> IO () -> IO (Async a, a)
    forall a b. IO a -> IO b -> IO a
    `finally` (Async a -> IO ()) -> [Async a] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Async a -> IO ()
    forall {a}. Async a -> IO ()
    cancelFast [Async a]
    asyncs
             cancelFast :: Async a -> IO ()
    cancelFast Async a
    other = ThreadId -> ExitCode -> IO ()
    forall e. Exception e => ThreadId -> e -> IO ()
    throwTo (Async a -> ThreadId
    forall a. Async a -> ThreadId
    asyncThreadId Async a
    other) ExitCode
    ExitSuccess
             runQueryInThread :: QueryT m b -> IO (Async (Solver, NominalDiffTime, c))
    runQueryInThread QueryT m b
    q = do UTCTime
    beginTime <- IO UTCTime
    getCurrentTime
                                     UTCTime
    -> (SMTConfig -> IO c)
    -> SMTConfig
    -> IO (Async (Solver, NominalDiffTime, c))
    forall b.
    NFData b =>
    UTCTime
    -> (SMTConfig -> IO b)
    -> SMTConfig
    -> IO (Async (Solver, NominalDiffTime, b))
    runInThread UTCTime
    beginTime (\SMTConfig
    cfg -> SMTConfig -> a -> QueryT m b -> IO c
    what SMTConfig
    cfg a
    a QueryT m b
    q) SMTConfig
    solver

    sbvConcurrentWithAll :: NFData c => SMTConfig -> (SMTConfig -> a -> QueryT m b -> IO c) -> [QueryT m b] -> a -> IO [(Solver, NominalDiffTime, c)]
    sbvConcurrentWithAll :: forall c a (m :: * -> *) b.
    NFData c =>
    SMTConfig
    -> (SMTConfig -> a -> QueryT m b -> IO c)
    -> [QueryT m b]
    -> a
    -> IO [(Solver, NominalDiffTime, c)]
    sbvConcurrentWithAll SMTConfig
    solver SMTConfig -> a -> QueryT m b -> IO c
    what [QueryT m b]
    queries a
    a = (QueryT m b -> IO (Async (Solver, NominalDiffTime, c)))
    -> [QueryT m b] -> IO [Async (Solver, NominalDiffTime, c)]
    forall (t :: * -> *) a b.
    Traversable t =>
    (a -> IO b) -> t a -> IO (t b)
    mapConcurrently QueryT m b -> IO (Async (Solver, NominalDiffTime, c))
    runQueryInThread [QueryT m b]
    queries  IO [Async (Solver, NominalDiffTime, c)]
    -> ([Async (Solver, NominalDiffTime, c)]
        -> IO [(Solver, NominalDiffTime, c)])
    -> IO [(Solver, NominalDiffTime, c)]
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO [(Solver, NominalDiffTime, c)]
    -> IO [(Solver, NominalDiffTime, c)]
    forall a. IO a -> IO a
    unsafeInterleaveIO (IO [(Solver, NominalDiffTime, c)]
     -> IO [(Solver, NominalDiffTime, c)])
    -> ([Async (Solver, NominalDiffTime, c)]
        -> IO [(Solver, NominalDiffTime, c)])
    -> [Async (Solver, NominalDiffTime, c)]
    -> IO [(Solver, NominalDiffTime, c)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Async (Solver, NominalDiffTime, c)]
    -> IO [(Solver, NominalDiffTime, c)]
    forall {a}. [Async a] -> IO [a]
    go
      where  runQueryInThread :: QueryT m b -> IO (Async (Solver, NominalDiffTime, c))
    runQueryInThread QueryT m b
    q = do UTCTime
    beginTime <- IO UTCTime
    getCurrentTime
                                     UTCTime
    -> (SMTConfig -> IO c)
    -> SMTConfig
    -> IO (Async (Solver, NominalDiffTime, c))
    forall b.
    NFData b =>
    UTCTime
    -> (SMTConfig -> IO b)
    -> SMTConfig
    -> IO (Async (Solver, NominalDiffTime, b))
    runInThread UTCTime
    beginTime (\SMTConfig
    cfg -> SMTConfig -> a -> QueryT m b -> IO c
    what SMTConfig
    cfg a
    a QueryT m b
    q) SMTConfig
    solver

             go :: [Async a] -> IO [a]
    go []  = [a] -> IO [a]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
             go [Async a]
    as  = do (Async a
    d, a
    r) <- [Async a] -> IO (Async a, a)
    forall {a}. [Async a] -> IO (Async a, a)
    waitAny [Async a]
    as
                         -- The following filter works because the Eq instance on Async
                         -- checks the thread-id; so we know that we're removing the
                         -- correct solver from the list. This also allows for
                         -- running the same-solver (with different options), since
                         -- they will get different thread-ids.
                         [a]
    rs <- IO [a] -> IO [a]
    forall a. IO a -> IO a
    unsafeInterleaveIO (IO [a] -> IO [a]) -> IO [a] -> IO [a]
    forall a b. (a -> b) -> a -> b
    $ [Async a] -> IO [a]
    go ((Async a -> Bool) -> [Async a] -> [Async a]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Async a -> Async a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Async a
    d) [Async a]
    as)
                         [a] -> IO [a]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a
    r a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a]
    rs)

    -- | Perform action for all given configs, return all the results.
    sbvWithAll :: NFData b => [SMTConfig] -> (SMTConfig -> a -> IO b) -> a -> IO [(Solver, NominalDiffTime, b)]
    sbvWithAll :: forall b a.
    NFData b =>
    [SMTConfig]
    -> (SMTConfig -> a -> IO b)
    -> a
    -> IO [(Solver, NominalDiffTime, b)]
    sbvWithAll [SMTConfig]
    solvers SMTConfig -> a -> IO b
    what a
    a = do UTCTime
    beginTime <- IO UTCTime
    getCurrentTime
                                   (SMTConfig -> IO (Async (Solver, NominalDiffTime, b)))
    -> [SMTConfig] -> IO [Async (Solver, NominalDiffTime, b)]
    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 (UTCTime
    -> (SMTConfig -> IO b)
    -> SMTConfig
    -> IO (Async (Solver, NominalDiffTime, b))
    forall b.
    NFData b =>
    UTCTime
    -> (SMTConfig -> IO b)
    -> SMTConfig
    -> IO (Async (Solver, NominalDiffTime, b))
    runInThread UTCTime
    beginTime (SMTConfig -> a -> IO b
    `what` a
    a)) [SMTConfig]
    solvers IO [Async (Solver, NominalDiffTime, b)]
    -> ([Async (Solver, NominalDiffTime, b)]
        -> IO [(Solver, NominalDiffTime, b)])
    -> IO [(Solver, NominalDiffTime, b)]
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= (IO [(Solver, NominalDiffTime, b)]
    -> IO [(Solver, NominalDiffTime, b)]
    forall a. IO a -> IO a
    unsafeInterleaveIO (IO [(Solver, NominalDiffTime, b)]
     -> IO [(Solver, NominalDiffTime, b)])
    -> ([Async (Solver, NominalDiffTime, b)]
        -> IO [(Solver, NominalDiffTime, b)])
    -> [Async (Solver, NominalDiffTime, b)]
    -> IO [(Solver, NominalDiffTime, b)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Async (Solver, NominalDiffTime, b)]
    -> IO [(Solver, NominalDiffTime, b)]
    forall {a}. [Async a] -> IO [a]
    go)
       where go :: [Async a] -> IO [a]
    go []  = [a] -> IO [a]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
             go [Async a]
    as  = do (Async a
    d, a
    r) <- [Async a] -> IO (Async a, a)
    forall {a}. [Async a] -> IO (Async a, a)
    waitAny [Async a]
    as
                         -- The following filter works because the Eq instance on Async
                         -- checks the thread-id; so we know that we're removing the
                         -- correct solver from the list. This also allows for
                         -- running the same-solver (with different options), since
                         -- they will get different thread-ids.
                         [a]
    rs <- IO [a] -> IO [a]
    forall a. IO a -> IO a
    unsafeInterleaveIO (IO [a] -> IO [a]) -> IO [a] -> IO [a]
    forall a b. (a -> b) -> a -> b
    $ [Async a] -> IO [a]
    go ((Async a -> Bool) -> [Async a] -> [Async a]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Async a -> Async a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Async a
    d) [Async a]
    as)
                         [a] -> IO [a]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a
    r a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a]
    rs)

    -- | Symbolically executable program fragments. This class is mainly used for 'safe' calls, and is sufficiently populated internally to cover most use
    -- cases. Users can extend it as they wish to allow 'safe' checks for SBV programs that return/take types that are user-defined.
    class ExtractIO m => SExecutable m a where
       -- | Generalization of 'Data.SBV.sName'
       sName :: a -> SymbolicT m ()

       -- | Generalization of 'Data.SBV.safe'
       safe :: a -> m [SafeResult]
       safe = SMTConfig -> a -> m [SafeResult]
    forall (m :: * -> *) a.
    SExecutable m a =>
    SMTConfig -> a -> m [SafeResult]
    safeWith SMTConfig
    defaultSMTCfg

       -- | Generalization of 'Data.SBV.safeWith'
       safeWith :: SMTConfig -> a -> m [SafeResult]
       safeWith SMTConfig
    cfg a
    a = do String
    cwd <- (String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "/") (String -> String) -> m String -> m String
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO String -> m String
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO String
    getCurrentDirectory
                           let mkRelative :: String -> String
    mkRelative String
    path
                                  | String
    cwd String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isPrefixOf` String
    path = Int -> String -> String
    forall a. Int -> [a] -> [a]
    drop (String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    cwd) String
    path
                                  | Bool
    True                  = String
    path
                           ([SafeResult], Result) -> [SafeResult]
    forall a b. (a, b) -> a
    fst (([SafeResult], Result) -> [SafeResult])
    -> m ([SafeResult], Result) -> m [SafeResult]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SMTConfig
    -> SBVRunMode
    -> SymbolicT m [SafeResult]
    -> m ([SafeResult], Result)
    forall (m :: * -> *) a.
    MonadIO m =>
    SMTConfig -> SBVRunMode -> SymbolicT m a -> m (a, Result)
    runSymbolic SMTConfig
    cfg (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
    SMTMode QueryContext
    QueryInternal IStage
    ISafe Bool
    True SMTConfig
    cfg) (a -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName a
    a SymbolicT m ()
    -> SymbolicT m [SafeResult] -> SymbolicT m [SafeResult]
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> (String -> String) -> SymbolicT m [SafeResult]
    check String -> String
    mkRelative)
         where check :: (FilePath -> FilePath) -> SymbolicT m [SafeResult]
               check :: (String -> String) -> SymbolicT m [SafeResult]
    check String -> String
    mkRelative = QueryContext -> QueryT m [SafeResult] -> SymbolicT m [SafeResult]
    forall (m :: * -> *) a.
    ExtractIO m =>
    QueryContext -> QueryT m a -> SymbolicT m a
    Control.executeQuery QueryContext
    QueryInternal (QueryT m [SafeResult] -> SymbolicT m [SafeResult])
    -> QueryT m [SafeResult] -> SymbolicT m [SafeResult]
    forall a b. (a -> b) -> a -> b
    $ QueryT m [(String, Maybe CallStack, SV)]
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m [(String, Maybe CallStack, SV)]
    Control.getSBVAssertions QueryT m [(String, Maybe CallStack, SV)]
    -> ([(String, Maybe CallStack, SV)] -> QueryT m [SafeResult])
    -> QueryT m [SafeResult]
    forall a b. QueryT m a -> (a -> QueryT m b) -> QueryT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= ((String, Maybe CallStack, SV) -> QueryT m SafeResult)
    -> [(String, Maybe CallStack, SV)] -> QueryT m [SafeResult]
    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 ((String -> String)
    -> (String, Maybe CallStack, SV) -> QueryT m SafeResult
    verify String -> String
    mkRelative)

               -- check that the cond is unsatisfiable. If satisfiable, that would
               -- indicate the assignment under which the 'Data.SBV.sAssert' would fail
               verify :: (FilePath -> FilePath) -> (String, Maybe CallStack, SV) -> QueryT m SafeResult
               verify :: (String -> String)
    -> (String, Maybe CallStack, SV) -> QueryT m SafeResult
    verify String -> String
    mkRelative (String
    msg, Maybe CallStack
    cs, SV
    cond) = do
                       let locInfo :: [(String, SrcLoc)] -> String
    locInfo [(String, SrcLoc)]
    ps = let loc :: (String, SrcLoc) -> String
    loc (String
    f, SrcLoc
    sl) = [String] -> String
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [String -> String
    mkRelative (SrcLoc -> String
    srcLocFile SrcLoc
    sl), String
    ":", Int -> String
    forall a. Show a => a -> String
    show (SrcLoc -> Int
    srcLocStartLine SrcLoc
    sl), String
    ":", Int -> String
    forall a. Show a => a -> String
    show (SrcLoc -> Int
    srcLocStartCol SrcLoc
    sl), String
    ":", String
    f]
                                        in String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ",\n " (((String, SrcLoc) -> String) -> [(String, SrcLoc)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, SrcLoc) -> String
    loc [(String, SrcLoc)]
    ps)
                           location :: Maybe String
    location   = ([(String, SrcLoc)] -> String
    locInfo ([(String, SrcLoc)] -> String)
    -> (CallStack -> [(String, SrcLoc)]) -> CallStack -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallStack -> [(String, SrcLoc)]
    getCallStack) (CallStack -> String) -> Maybe CallStack -> Maybe String
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` Maybe CallStack
    cs

                       SMTResult
    result <- do Int -> QueryT m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
    Control.push Int
    1
                                    Bool -> String -> QueryT m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> String -> m ()
    Control.send Bool
    True (String -> QueryT m ()) -> String -> QueryT m ()
    forall a b. (a -> b) -> a -> b
    $ String
    "(assert " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    cond String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                                    SMTResult
    r <- QueryT m SMTResult
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
    Control.getSMTResult
                                    Int -> QueryT m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
    Control.pop Int
    1
                                    SMTResult -> QueryT m SMTResult
    forall a. a -> QueryT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTResult
    r

                       SafeResult -> QueryT m SafeResult
    forall a. a -> QueryT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SafeResult -> QueryT m SafeResult)
    -> SafeResult -> QueryT m SafeResult
    forall a b. (a -> b) -> a -> b
    $ (Maybe String, String, SMTResult) -> SafeResult
    SafeResult (Maybe String
    location, String
    msg, SMTResult
    result)

    instance (ExtractIO m, NFData a) => SExecutable m (SymbolicT m a) where
       sName :: SymbolicT m a -> SymbolicT m ()
    sName SymbolicT m a
    a = SymbolicT m a
    a SymbolicT m a -> (a -> SymbolicT m ()) -> SymbolicT m ()
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a
    r -> a -> ()
    forall a. NFData a => a -> ()
    rnf a
    r () -> SymbolicT m () -> SymbolicT m ()
    forall a b. a -> b -> b
    `seq` () -> SymbolicT m ()
    forall a. a -> SymbolicT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    instance ExtractIO m => SExecutable m (SBV a) where
       sName :: SBV a -> SymbolicT m ()
    sName SBV a
    v = SymbolicT m (SBV a) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName (SBV a -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV a -> m (SBV a)
    output SBV a
    v :: SymbolicT m (SBV a))

    -- Unit output
    instance ExtractIO m => SExecutable m () where
       sName :: () -> SymbolicT m ()
    sName () = SymbolicT m () -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName (() -> SymbolicT m ()
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => () -> m ()
    output () :: SymbolicT m ())

    -- List output
    instance ExtractIO m => SExecutable m [SBV a] where
       sName :: [SBV a] -> SymbolicT m ()
    sName [SBV a]
    vs = SymbolicT m [SBV a] -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName ([SBV a] -> SymbolicT m [SBV a]
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => [SBV a] -> m [SBV a]
    output [SBV a]
    vs :: SymbolicT m [SBV a])

    -- 2 Tuple output
    instance (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b) => SExecutable m (SBV a, SBV b) where
      sName :: (SBV a, SBV b) -> SymbolicT m ()
    sName (SBV a
    a, SBV b
    b) = SymbolicT m (SBV b) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName (SBV a -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV a -> m (SBV a)
    output SBV a
    a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV b)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV b -> SymbolicT m (SBV b)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV b -> m (SBV b)
    output SBV b
    b :: SymbolicT m (SBV b))

    -- 3 Tuple output
    instance (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b, NFData c, SymVal c) => SExecutable m (SBV a, SBV b, SBV c) where
      sName :: (SBV a, SBV b, SBV c) -> SymbolicT m ()
    sName (SBV a
    a, SBV b
    b, SBV c
    c) = SymbolicT m (SBV c) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName (SBV a -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV a -> m (SBV a)
    output SBV a
    a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV b)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV b -> SymbolicT m (SBV b)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV b -> m (SBV b)
    output SBV b
    b SymbolicT m (SBV b) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV c -> SymbolicT m (SBV c)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV c -> m (SBV c)
    output SBV c
    c :: SymbolicT m (SBV c))

    -- 4 Tuple output
    instance (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b, NFData c, SymVal c, NFData d, SymVal d) => SExecutable m (SBV a, SBV b, SBV c, SBV d) where
      sName :: (SBV a, SBV b, SBV c, SBV d) -> SymbolicT m ()
    sName (SBV a
    a, SBV b
    b, SBV c
    c, SBV d
    d) = SymbolicT m (SBV d) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName (SBV a -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV a -> m (SBV a)
    output SBV a
    a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV b)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV b -> SymbolicT m (SBV b)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV b -> m (SBV b)
    output SBV b
    b SymbolicT m (SBV b) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV c -> SymbolicT m (SBV c)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV c -> m (SBV c)
    output SBV c
    c SymbolicT m (SBV c) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV c -> SymbolicT m (SBV c)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV c -> m (SBV c)
    output SBV c
    c SymbolicT m (SBV c) -> SymbolicT m (SBV d) -> SymbolicT m (SBV d)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV d -> SymbolicT m (SBV d)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV d -> m (SBV d)
    output SBV d
    d :: SymbolicT m (SBV d))

    -- 5 Tuple output
    instance (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b, NFData c, SymVal c, NFData d, SymVal d, NFData e, SymVal e) => SExecutable m (SBV a, SBV b, SBV c, SBV d, SBV e) where
      sName :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> SymbolicT m ()
    sName (SBV a
    a, SBV b
    b, SBV c
    c, SBV d
    d, SBV e
    e) = SymbolicT m (SBV e) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName (SBV a -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV a -> m (SBV a)
    output SBV a
    a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV b)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV b -> SymbolicT m (SBV b)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV b -> m (SBV b)
    output SBV b
    b SymbolicT m (SBV b) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV c -> SymbolicT m (SBV c)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV c -> m (SBV c)
    output SBV c
    c SymbolicT m (SBV c) -> SymbolicT m (SBV d) -> SymbolicT m (SBV d)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV d -> SymbolicT m (SBV d)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV d -> m (SBV d)
    output SBV d
    d SymbolicT m (SBV d) -> SymbolicT m (SBV e) -> SymbolicT m (SBV e)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV e -> SymbolicT m (SBV e)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV e -> m (SBV e)
    output SBV e
    e :: SymbolicT m (SBV e))

    -- 6 Tuple output
    instance (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b, NFData c, SymVal c, NFData d, SymVal d, NFData e, SymVal e, NFData f, SymVal f) => SExecutable m (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) where
      sName :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> SymbolicT m ()
    sName (SBV a
    a, SBV b
    b, SBV c
    c, SBV d
    d, SBV e
    e, SBV f
    f) = SymbolicT m (SBV f) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName (SBV a -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV a -> m (SBV a)
    output SBV a
    a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV b)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV b -> SymbolicT m (SBV b)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV b -> m (SBV b)
    output SBV b
    b SymbolicT m (SBV b) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV c -> SymbolicT m (SBV c)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV c -> m (SBV c)
    output SBV c
    c SymbolicT m (SBV c) -> SymbolicT m (SBV d) -> SymbolicT m (SBV d)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV d -> SymbolicT m (SBV d)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV d -> m (SBV d)
    output SBV d
    d SymbolicT m (SBV d) -> SymbolicT m (SBV e) -> SymbolicT m (SBV e)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV e -> SymbolicT m (SBV e)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV e -> m (SBV e)
    output SBV e
    e SymbolicT m (SBV e) -> SymbolicT m (SBV f) -> SymbolicT m (SBV f)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV f -> SymbolicT m (SBV f)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV f -> m (SBV f)
    output SBV f
    f :: SymbolicT m (SBV f))

    -- 7 Tuple output
    instance (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b, NFData c, SymVal c, NFData d, SymVal d, NFData e, SymVal e, NFData f, SymVal f, NFData g, SymVal g) => SExecutable m (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) where
      sName :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> SymbolicT m ()
    sName (SBV a
    a, SBV b
    b, SBV c
    c, SBV d
    d, SBV e
    e, SBV f
    f, SBV g
    g) = SymbolicT m (SBV g) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName (SBV a -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV a -> m (SBV a)
    output SBV a
    a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV b)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV b -> SymbolicT m (SBV b)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV b -> m (SBV b)
    output SBV b
    b SymbolicT m (SBV b) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV c -> SymbolicT m (SBV c)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV c -> m (SBV c)
    output SBV c
    c SymbolicT m (SBV c) -> SymbolicT m (SBV d) -> SymbolicT m (SBV d)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV d -> SymbolicT m (SBV d)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV d -> m (SBV d)
    output SBV d
    d SymbolicT m (SBV d) -> SymbolicT m (SBV e) -> SymbolicT m (SBV e)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV e -> SymbolicT m (SBV e)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV e -> m (SBV e)
    output SBV e
    e SymbolicT m (SBV e) -> SymbolicT m (SBV f) -> SymbolicT m (SBV f)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV f -> SymbolicT m (SBV f)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV f -> m (SBV f)
    output SBV f
    f SymbolicT m (SBV f) -> SymbolicT m (SBV g) -> SymbolicT m (SBV g)
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBV g -> SymbolicT m (SBV g)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV g -> m (SBV g)
    output SBV g
    g :: SymbolicT m (SBV g))

    -- Functions
    instance (SymVal a, SExecutable m p) => SExecutable m (SBV a -> p) where
       sName :: (SBV a -> p) -> SymbolicT m ()
    sName SBV a -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SBV a
    a -> p -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName (p -> SymbolicT m ()) -> p -> SymbolicT m ()
    forall a b. (a -> b) -> a -> b
    $ SBV a -> p
    k SBV a
    a

    -- 2 Tuple input
    instance (SymVal a, SymVal b, SExecutable m p) => SExecutable m ((SBV a, SBV b) -> p) where
      sName :: ((SBV a, SBV b) -> p) -> SymbolicT m ()
    sName (SBV a, SBV b) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SBV a
    a -> (SBV b -> p) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName ((SBV b -> p) -> SymbolicT m ()) -> (SBV b -> p) -> SymbolicT m ()
    forall a b. (a -> b) -> a -> b
    $ \SBV b
    b -> (SBV a, SBV b) -> p
    k (SBV a
    a, SBV b
    b)

    -- 3 Tuple input
    instance (SymVal a, SymVal b, SymVal c, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c) -> p) where
      sName :: ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m ()
    sName (SBV a, SBV b, SBV c) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SBV a
    a -> (SBV b -> SBV c -> p) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName ((SBV b -> SBV c -> p) -> SymbolicT m ())
    -> (SBV b -> SBV c -> p) -> SymbolicT m ()
    forall a b. (a -> b) -> a -> b
    $ \SBV b
    b SBV c
    c -> (SBV a, SBV b, SBV c) -> p
    k (SBV a
    a, SBV b
    b, SBV c
    c)

    -- 4 Tuple input
    instance (SymVal a, SymVal b, SymVal c, SymVal d, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c, SBV d) -> p) where
      sName :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m ()
    sName (SBV a, SBV b, SBV c, SBV d) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SBV a
    a -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName ((SBV b -> SBV c -> SBV d -> p) -> SymbolicT m ())
    -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m ()
    forall a b. (a -> b) -> a -> b
    $ \SBV b
    b SBV c
    c SBV d
    d -> (SBV a, SBV b, SBV c, SBV d) -> p
    k (SBV a
    a, SBV b
    b, SBV c
    c, SBV d
    d)

    -- 5 Tuple input
    instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) where
      sName :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m ()
    sName (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SBV a
    a -> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName ((SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m ())
    -> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m ()
    forall a b. (a -> b) -> a -> b
    $ \SBV b
    b SBV c
    c SBV d
    d SBV e
    e -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
    k (SBV a
    a, SBV b
    b, SBV c
    c, SBV d
    d, SBV e
    e)

    -- 6 Tuple input
    instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) where
      sName :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> SymbolicT m ()
    sName (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SBV a
    a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
     -> SymbolicT m ())
    -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
    -> SymbolicT m ()
    forall a b. (a -> b) -> a -> b
    $ \SBV b
    b SBV c
    c SBV d
    d SBV e
    e SBV f
    f -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
    k (SBV a
    a, SBV b
    b, SBV c
    c, SBV d
    d, SBV e
    e, SBV f
    f)

    -- 7 Tuple input
    instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) where
      sName :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
    -> SymbolicT m ()
    sName (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    mkArg SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SBV a
    a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
    -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
     -> SymbolicT m ())
    -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
    -> SymbolicT m ()
    forall a b. (a -> b) -> a -> b
    $ \SBV b
    b SBV c
    c SBV d
    d SBV e
    e SBV f
    f SBV g
    g -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
    k (SBV a
    a, SBV b
    b, SBV c
    c, SBV d
    d, SBV e
    e, SBV f
    f, SBV g
    g)

    {- HLint ignore module "Reduce duplication" -}