    -----------------------------------------------------------------------------
    -- |
    -- 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         #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Provers.Prover (
             SMTSolver(..), SMTConfig(..), Predicate
           , MProvable(..), Provable, proveWithAll, proveWithAny , satWithAll, satWithAny
           , satConcurrentWithAny, satConcurrentWithAll, proveConcurrentWithAny, proveConcurrentWithAll
           , generateSMTBenchmark
           , Goal
           , ThmResult(..), SatResult(..), AllSatResult(..), SafeResult(..), OptimizeResult(..), SMTResult(..)
           , SExecutable(..), isSafe
           , runSMT, runSMTWith
           , SatModel(..), Modelable(..), displayModels, extractModels
           , getModelDictionaries, getModelValues, getModelUninterpretedValues
           , boolector, cvc4, yices, z3, mathSAT, abc, defaultSMTCfg
           ) 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, nub)

    import Data.Maybe (mapMaybe, listToMaybe)

    import qualified Data.Map.Strict as M
    import qualified Data.Foldable   as S (toList)

    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.Boolector  as Boolector
    import qualified Data.SBV.Provers.CVC4       as CVC4
    import qualified Data.SBV.Provers.Yices      as Yices
    import qualified Data.SBV.Provers.Z3         as Z3
    import qualified Data.SBV.Provers.MathSAT    as MathSAT
    import qualified Data.SBV.Provers.ABC        as ABC

    mkConfig :: SMTSolver -> SMTLibVersion -> [Control.SMTOption] -> SMTConfig
    mkConfig :: SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
    mkConfig s :: SMTSolver
    s smtVersion :: SMTLibVersion
    smtVersion startOpts :: [SMTOption]
    startOpts = SMTConfig :: Bool
    -> Timing
    -> Int
    -> Int
    -> String
    -> Maybe Int
    -> Bool
    -> Bool
    -> (String -> Bool)
    -> Bool
    -> Bool
    -> Maybe String
    -> SMTLibVersion
    -> SMTSolver
    -> Bool
    -> RoundingMode
    -> [SMTOption]
    -> Bool
    -> Maybe String
    -> SMTConfig
    SMTConfig { verbose :: Bool
    verbose                     = Bool
    False
                                                , timing :: Timing
    timing                      = Timing
    NoTiming
                                                , printBase :: Int
    printBase                   = 10
                                                , printRealPrec :: Int
    printRealPrec               = 16
                                                , transcript :: Maybe String
    transcript                  = Maybe String
    forall a. Maybe a
    Nothing
                                                , solver :: SMTSolver
    solver                      = SMTSolver
    s
                                                , smtLibVersion :: SMTLibVersion
    smtLibVersion               = SMTLibVersion
    smtVersion
                                                , satCmd :: String
    satCmd                      = "(check-sat)"
                                                , satTrackUFs :: Bool
    satTrackUFs                 = 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
                                                , allowQuantifiedQueries :: Bool
    allowQuantifiedQueries      = 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 -> [String] -> SMTOption
    Control.OptionKeyword ":diagnostic-output-channel" [String -> String
    forall a. Show a => a -> String
    show "stdout"]

    -- | 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 CVC4 SMT Solver.
    cvc4 :: SMTConfig
    cvc4 :: SMTConfig
    cvc4 = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
    mkConfig SMTSolver
    CVC4.cvc4 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 ":smtlib2_compliant" ["true"]
                                , SMTOption
    allOnStdOut
                                ]

    -- | 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 ABC synthesis and verification tool.
    abc :: SMTConfig
    abc :: SMTConfig
    abc = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
    mkConfig SMTSolver
    ABC.abc SMTLibVersion
    SMTLib2 [SMTOption
    allOnStdOut]

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

    -- | 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 goal is a symbolic program that returns no values. The idea is that the constraints/min-max
    -- goals will serve as appropriate directives for sat/prove calls.
    type Goal = Symbolic ()

    -- | A type @a@ is provable if we can turn it into a predicate.
    -- Note that a predicate can be made from a curried function of arbitrary arity, where
    -- each element is either a symbolic type or up-to a 7-tuple of symbolic-types. So
    -- predicates can be constructed from almost arbitrary Haskell functions that have arbitrary
    -- shapes. (See the instance declarations below.)
    class ExtractIO m => MProvable m a where
      -- | Generalization of 'Data.SBV.forAll_'
      forAll_ :: a -> SymbolicT m SBool

      -- | Generalization of 'Data.SBV.forAll'
      forAll  :: [String] -> a -> SymbolicT m SBool

      -- | Generalization of 'Data.SBV.forSome_'
      forSome_ :: a -> SymbolicT m SBool

      -- | Generalization of 'Data.SBV.forSome'
      forSome :: [String] -> a -> SymbolicT m SBool

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

      -- | Generalization of 'Data.SBV.proveWith'
      proveWith :: SMTConfig -> a -> m ThmResult
      proveWith cfg :: SMTConfig
    cfg a :: a
    a = do SMTResult
    r <- Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
    forall (m :: * -> *) a b.
    MProvable m a =>
    Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery Bool
    False (QueryT m ()
    forall (m :: * -> *). MonadIO m => QueryT m ()
    checkNoOptimizations QueryT m () -> QueryT m SMTResult -> QueryT m SMTResult
    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 Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    forall (m :: * -> *) a.
    MProvable m a =>
    Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    validate Bool
    False SMTConfig
    cfg a
    a SMTResult
    r
                                         else SMTResult -> m SMTResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTResult
    r

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

      -- | Generalization of 'Data.SBV.satWith'
      satWith :: SMTConfig -> a -> m SatResult
      satWith cfg :: SMTConfig
    cfg a :: a
    a = do SMTResult
    r <- Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
    forall (m :: * -> *) a b.
    MProvable m a =>
    Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery Bool
    True (QueryT m ()
    forall (m :: * -> *). MonadIO m => QueryT m ()
    checkNoOptimizations QueryT m () -> QueryT m SMTResult -> QueryT m SMTResult
    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 Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    forall (m :: * -> *) a.
    MProvable m a =>
    Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    validate Bool
    True SMTConfig
    cfg a
    a SMTResult
    r
                                       else SMTResult -> m SMTResult
    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.
    MProvable m a =>
    SMTConfig -> a -> m AllSatResult
    allSatWith SMTConfig
    defaultSMTCfg

      -- | Generalization of 'Data.SBV.allSatWith'
      allSatWith :: SMTConfig -> a -> m AllSatResult
      allSatWith cfg :: SMTConfig
    cfg a :: a
    a = do f :: (Bool, Bool, Bool, [SMTResult])
    f@(mm :: Bool
    mm, pe :: Bool
    pe, un :: Bool
    un, rs :: [SMTResult]
    rs) <- Bool
    -> QueryT m (Bool, Bool, Bool, [SMTResult])
    -> SMTConfig
    -> a
    -> m (Bool, Bool, Bool, [SMTResult])
    forall (m :: * -> *) a b.
    MProvable m a =>
    Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery Bool
    True (QueryT m ()
    forall (m :: * -> *). MonadIO m => QueryT m ()
    checkNoOptimizations QueryT m ()
    -> QueryT m (Bool, Bool, Bool, [SMTResult])
    -> QueryT m (Bool, Bool, Bool, [SMTResult])
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> QueryT m (Bool, Bool, Bool, [SMTResult])
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m, SolverContext m) =>
    m (Bool, Bool, Bool, [SMTResult])
    Control.getAllSatResult) SMTConfig
    cfg a
    a
                            (Bool, Bool, Bool, [SMTResult]) -> AllSatResult
    AllSatResult ((Bool, Bool, Bool, [SMTResult]) -> AllSatResult)
    -> m (Bool, Bool, Bool, [SMTResult]) -> m AllSatResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> 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)
    mapM (Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    forall (m :: * -> *) a.
    MProvable m a =>
    Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    validate Bool
    True SMTConfig
    cfg a
    a) [SMTResult]
    rs
                                                     (Bool, Bool, Bool, [SMTResult])
    -> m (Bool, Bool, Bool, [SMTResult])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    mm, Bool
    pe, Bool
    un, [SMTResult]
    rs')
                                             else (Bool, Bool, Bool, [SMTResult])
    -> m (Bool, Bool, Bool, [SMTResult])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool, Bool, Bool, [SMTResult])
    f

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

      -- | Generalization of 'Data.SBV.optimizeWith'
      optimizeWith :: SMTConfig -> OptimizeStyle -> a -> m OptimizeResult
      optimizeWith config :: SMTConfig
    config style :: OptimizeStyle
    style optGoal :: a
    optGoal = do
                       OptimizeResult
    res <- Bool
    -> QueryT m OptimizeResult -> SMTConfig -> a -> m OptimizeResult
    forall (m :: * -> *) a b.
    MProvable m a =>
    Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery Bool
    True QueryT m OptimizeResult
    opt SMTConfig
    config a
    optGoal
                       if Bool -> Bool
    not (SMTConfig -> Bool
    optimizeValidateConstraints SMTConfig
    config)
                          then OptimizeResult -> m OptimizeResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return OptimizeResult
    res
                          else let v :: SMTResult -> m SMTResult
                                   v :: SMTResult -> m SMTResult
    v = Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    forall (m :: * -> *) a.
    MProvable m a =>
    Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
    validate Bool
    True SMTConfig
    config a
    optGoal
                               in case OptimizeResult
    res of
                                    LexicographicResult m :: 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 xs :: [(String, SMTResult)]
    xs  -> let w :: [(a, SMTResult)] -> [(a, SMTResult)] -> m [(a, SMTResult)]
    w []            sofar :: [(a, SMTResult)]
    sofar = [(a, SMTResult)] -> m [(a, SMTResult)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(a, SMTResult)] -> [(a, SMTResult)]
    forall a. [a] -> [a]
    reverse [(a, SMTResult)]
    sofar)
                                                                 w ((n :: a
    n, m :: SMTResult
    m):rest :: [(a, SMTResult)]
    rest) sofar :: [(a, SMTResult)]
    sofar = SMTResult -> m SMTResult
    v SMTResult
    m m SMTResult
    -> (SMTResult -> m [(a, SMTResult)]) -> m [(a, SMTResult)]
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \m' :: 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 (b :: Bool
    b, rs :: [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)
    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
                       [(Quantifier, NamedSymVar)]
    qinps      <- QueryT m [(Quantifier, NamedSymVar)]
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m [(Quantifier, NamedSymVar)]
    Control.getQuantifiedInputs
                       SBVPgm
    spgm       <- QueryT m SBVPgm
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SBVPgm
    Control.getSBVPgm

                       Bool -> QueryT m () -> QueryT m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when ([Objective (SV, SV)] -> 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 [ ""
                                              , "*** Data.SBV: Unsupported call to optimize when no objectives are present."
                                              , "*** 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 [ ""
                                              , "*** 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]
    ++ "does not support optimization goals."
                                              , "*** 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 [ ""
                                              , "*** Data.SBV: Model validation is not supported in optimization calls."
                                              , "***"
                                              , "*** Instead, use `cfg{optimizeValidateConstraints = True}`"
                                              , "***"
                                              , "*** which checks that the results satisfy the constraints but does"
                                              , "*** NOT ensure that they are optimal."
                                              ]

                       let universals :: [NamedSymVar]
    universals = [NamedSymVar
    s | (ALL, s :: NamedSymVar
    s) <- [(Quantifier, NamedSymVar)]
    qinps]

                           firstUniversal :: NodeId
    firstUniversal
                             | [NamedSymVar] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [NamedSymVar]
    universals = String -> NodeId
    forall a. HasCallStack => String -> a
    error "Data.SBV: Impossible happened! Universal optimization with no universals!"
                             | Bool
    True            = [NodeId] -> NodeId
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    minimum ((NamedSymVar -> NodeId) -> [NamedSymVar] -> [NodeId]
    forall a b. (a -> b) -> [a] -> [b]
    map (SV -> NodeId
    nodeId (SV -> NodeId) -> (NamedSymVar -> SV) -> NamedSymVar -> NodeId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedSymVar -> SV
    forall a b. (a, b) -> a
    fst) [NamedSymVar]
    universals)

                           nodeId :: SV -> NodeId
    nodeId (SV _ n :: NodeId
    n) = NodeId
    n

                           mappings :: M.Map SV SBVExpr
                           mappings :: Map SV SBVExpr
    mappings = [(SV, SBVExpr)] -> Map SV SBVExpr
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList (Seq (SV, SBVExpr) -> [(SV, SBVExpr)]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    S.toList (SBVPgm -> Seq (SV, SBVExpr)
    pgmAssignments SBVPgm
    spgm))

                           chaseUniversal :: SV -> [String]
    chaseUniversal entry :: SV
    entry = (NamedSymVar -> String) -> [NamedSymVar] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedSymVar -> String
    forall a b. (a, b) -> b
    snd ([NamedSymVar] -> [String]) -> [NamedSymVar] -> [String]
    forall a b. (a -> b) -> a -> b
    $ SV -> [NamedSymVar] -> [NamedSymVar]
    go SV
    entry []
                             where go :: SV -> [NamedSymVar] -> [NamedSymVar]
    go x :: SV
    x sofar :: [NamedSymVar]
    sofar
                                    | NodeId
    nx NodeId -> NodeId -> Bool
    forall a. Ord a => a -> a -> Bool
    >= NodeId
    firstUniversal
                                    = [NamedSymVar] -> [NamedSymVar]
    forall a. Eq a => [a] -> [a]
    nub ([NamedSymVar] -> [NamedSymVar]) -> [NamedSymVar] -> [NamedSymVar]
    forall a b. (a -> b) -> a -> b
    $ [NamedSymVar
    unm | unm :: NamedSymVar
    unm@(u :: SV
    u, _) <- [NamedSymVar]
    universals, NodeId
    nx NodeId -> NodeId -> Bool
    forall a. Ord a => a -> a -> Bool
    >= SV -> NodeId
    nodeId SV
    u] [NamedSymVar] -> [NamedSymVar] -> [NamedSymVar]
    forall a. [a] -> [a] -> [a]
    ++ [NamedSymVar]
    sofar
                                    | Bool
    True
                                    = let oVars :: Op -> [SV]
    oVars (LkUp _ a :: SV
    a b :: SV
    b)             = [SV
    a, SV
    b]
                                          oVars (IEEEFP (FP_Cast _ _ o :: SV
    o)) = [SV
    o]
                                          oVars _                        = []
                                          vars :: [SV]
    vars = case SV
    x SV -> Map SV SBVExpr -> Maybe SBVExpr
    forall k a. Ord k => k -> Map k a -> Maybe a
    `M.lookup` Map SV SBVExpr
    mappings of
                                                   Nothing            -> []
                                                   Just (SBVApp o :: Op
    o ss :: [SV]
    ss) -> [SV] -> [SV]
    forall a. Eq a => [a] -> [a]
    nub (Op -> [SV]
    oVars Op
    o [SV] -> [SV] -> [SV]
    forall a. [a] -> [a] -> [a]
    ++ [SV]
    ss)
                                      in (SV -> [NamedSymVar] -> [NamedSymVar])
    -> [NamedSymVar] -> [SV] -> [NamedSymVar]
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr SV -> [NamedSymVar] -> [NamedSymVar]
    go [NamedSymVar]
    sofar [SV]
    vars
                                    where nx :: NodeId
    nx = SV -> NodeId
    nodeId SV
    x

                       let needsUniversalOpt :: [(String, [String])]
    needsUniversalOpt = let tag :: a -> [a] -> Maybe (a, [a])
    tag _  [] = Maybe (a, [a])
    forall a. Maybe a
    Nothing
                                                   tag nm :: a
    nm xs :: [a]
    xs = (a, [a]) -> Maybe (a, [a])
    forall a. a -> Maybe a
    Just (a
    nm, [a]
    xs)
                                                   needsUniversal :: Objective (SV, b) -> Maybe (String, [String])
    needsUniversal (Maximize          nm :: String
    nm (x :: SV
    x, _))   = String -> [String] -> Maybe (String, [String])
    forall a a. a -> [a] -> Maybe (a, [a])
    tag String
    nm (SV -> [String]
    chaseUniversal SV
    x)
                                                   needsUniversal (Minimize          nm :: String
    nm (x :: SV
    x, _))   = String -> [String] -> Maybe (String, [String])
    forall a a. a -> [a] -> Maybe (a, [a])
    tag String
    nm (SV -> [String]
    chaseUniversal SV
    x)
                                                   needsUniversal (AssertWithPenalty nm :: String
    nm (x :: SV
    x, _) _) = String -> [String] -> Maybe (String, [String])
    forall a a. a -> [a] -> Maybe (a, [a])
    tag String
    nm (SV -> [String]
    chaseUniversal SV
    x)
                                               in (Objective (SV, SV) -> Maybe (String, [String]))
    -> [Objective (SV, SV)] -> [(String, [String])]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe Objective (SV, SV) -> Maybe (String, [String])
    forall b. Objective (SV, b) -> Maybe (String, [String])
    needsUniversal [Objective (SV, SV)]
    objectives

                       Bool -> QueryT m () -> QueryT m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([NamedSymVar] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [NamedSymVar]
    universals Bool -> Bool -> Bool
    || [(String, [String])] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(String, [String])]
    needsUniversalOpt) (QueryT m () -> QueryT m ()) -> QueryT m () -> QueryT m ()
    forall a b. (a -> b) -> a -> b
    $
                              let len :: Int
    len = [Int] -> Int
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum ([Int] -> Int) -> [Int] -> Int
    forall a b. (a -> b) -> a -> b
    $ 0 Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    : [String -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    nm | (nm :: String
    nm, _) <- [(String, [String])]
    needsUniversalOpt]
                                  pad :: String -> String
    pad n :: String
    n = String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate (Int
    len Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - String -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    n) ' '
                              in 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) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ [ ""
                                                   , "*** Data.SBV: Problem needs optimization of metric in the scope of universally quantified variable(s):"
                                                   , "***"
                                                   ]
                                               [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++  [ "***          " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++  String -> String
    pad String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " [Depends on: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", " [String]
    xs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "]"  | (s :: String
    s, xs :: [String]
    xs) <- [(String, [String])]
    needsUniversalOpt ]
                                               [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++  [ "***"
                                                   , "*** Optimization is only meaningful with existentially quantified metrics."
                                                   ]

                       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 (x :: a
    x, y :: a
    y) = "(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
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    y String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "))"

                                   minmax :: Objective (a, a) -> [String]
    minmax (Minimize          _  xy :: (a, a)
    xy@(_, v :: a
    v))     = [(a, a) -> String
    forall a a. (Show a, Show a) => (a, a) -> String
    mkEq (a, a)
    xy, "(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]
    ++ ")"]
                                   minmax (Maximize          _  xy :: (a, a)
    xy@(_, v :: a
    v))     = [(a, a) -> String
    forall a a. (Show a, Show a) => (a, a) -> String
    mkEq (a, a)
    xy, "(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]
    ++ ")"]
                                   minmax (AssertWithPenalty nm :: String
    nm xy :: (a, a)
    xy@(_, v :: a
    v) mbp :: Penalty
    mbp) = [(a, a) -> String
    forall a a. (Show a, Show a) => (a, a) -> String
    mkEq (a, a)
    xy, "(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]
    ++ ")"]
                                     where penalize :: Penalty -> String
    penalize DefaultPenalty    = ""
                                           penalize (Penalty w :: Rational
    w mbGrp :: Maybe String
    mbGrp)
                                              | Rational
    w Rational -> Rational -> Bool
    forall a. Ord a => a -> a -> Bool
    <= 0         = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ "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]
    ++ " is assigned a non-positive penalty: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    shw
                                                                                 , "All soft goals must have > 0 penalties associated."
                                                                                 ]
                                              | Bool
    True           = " :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
    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 g :: String
    g = " :id " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    g

                                   priority :: OptimizeStyle -> [String]
    priority Lexicographic = [] -- default, no option needed
                                   priority Independent   = ["(set-option :opt.priority box)"]
                                   priority (Pareto _)    = ["(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
                         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
                         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 mbN :: 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

      -- | Generalization of 'Data.SBV.isVacuous'
      isVacuous :: a -> m Bool
      isVacuous = SMTConfig -> a -> m Bool
    forall (m :: * -> *) a. MProvable m a => SMTConfig -> a -> m Bool
    isVacuousWith SMTConfig
    defaultSMTCfg

      -- | Generalization of 'Data.SBV.isVacuousWith'
      isVacuousWith :: SMTConfig -> a -> m Bool
      isVacuousWith cfg :: SMTConfig
    cfg a :: 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
    <$> SBVRunMode -> SymbolicT m Bool -> m (Bool, Result)
    forall (m :: * -> *) a.
    MonadIO m =>
    SBVRunMode -> SymbolicT m a -> m (a, Result)
    runSymbolic (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
    SMTMode QueryContext
    QueryInternal IStage
    ISetup Bool
    True SMTConfig
    cfg) (a -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forSome_ a
    a SymbolicT m SBool -> SymbolicT m Bool -> SymbolicT m Bool
    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 :: QueryT m Bool
    check = do CheckSatResult
    cs <- QueryT m CheckSatResult
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
    Control.checkSat
                      case CheckSatResult
    cs of
                        Control.Unsat -> Bool -> QueryT m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
                        Control.Sat   -> Bool -> QueryT m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
                        Control.Unk   -> String -> QueryT m Bool
    forall a. HasCallStack => String -> a
    error "SBV: isVacuous: Solver returned unknown!"

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

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

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

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

      -- | Validate a model obtained from the solver
      validate :: Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
      validate isSAT :: Bool
    isSAT cfg :: SMTConfig
    cfg p :: a
    p res :: SMTResult
    res = case SMTResult
    res of
                                   Unsatisfiable{} -> SMTResult -> m SMTResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTResult
    res
                                   Satisfiable _ m :: SMTModel
    m -> case SMTModel -> Maybe [((Quantifier, NamedSymVar), Maybe CV)]
    modelBindings SMTModel
    m of
                                                        Nothing  -> String -> m SMTResult
    forall a. HasCallStack => String -> a
    error "Data.SBV.validate: Impossible happaned; no bindings generated during model validation."
                                                        Just env :: [((Quantifier, NamedSymVar), Maybe CV)]
    env -> [((Quantifier, NamedSymVar), Maybe CV)] -> m SMTResult
    forall (m :: * -> *).
    MProvable m a =>
    [((Quantifier, NamedSymVar), Maybe CV)] -> m SMTResult
    check [((Quantifier, NamedSymVar), Maybe CV)]
    env
                                   SatExtField{}   -> SMTResult -> m SMTResult
    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 [ "The model requires an extension field value."
                                                                              , "Cannot validate models with infinities/epsilons produced during optimization."
                                                                              , ""
                                                                              , "To turn validation off, use `cfg{optimizeValidateConstraints = False}`"
                                                                              , ""
                                                                              , "Unable to validate the produced model."
                                                                              ]
                                                                              (SMTResult -> Maybe SMTResult
    forall a. a -> Maybe a
    Just SMTResult
    res)
                                   Unknown{}       -> SMTResult -> m SMTResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTResult
    res
                                   ProofError{}    -> SMTResult -> m SMTResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTResult
    res

        where check :: [((Quantifier, NamedSymVar), Maybe CV)] -> m SMTResult
    check env :: [((Quantifier, NamedSymVar), Maybe CV)]
    env = do let univs :: [String]
    univs    = [String
    n | ((ALL, (_, n :: String
    n)), _) <- [((Quantifier, NamedSymVar), Maybe CV)]
    env]
                                 envShown :: String
    envShown = Bool -> Bool -> SMTConfig -> [(String, GeneralizedCV)] -> String
    showModelDictionary Bool
    True Bool
    True SMTConfig
    cfg [(String, GeneralizedCV)]
    modelBinds
                                    where modelBinds :: [(String, GeneralizedCV)]
    modelBinds = [(String
    n, Quantifier -> SV -> Maybe CV -> GeneralizedCV
    forall a. HasKind a => Quantifier -> a -> Maybe CV -> GeneralizedCV
    fake Quantifier
    q SV
    s Maybe CV
    v) | ((q :: Quantifier
    q, (s :: SV
    s, n :: String
    n)), v :: Maybe CV
    v) <- [((Quantifier, NamedSymVar), Maybe CV)]
    env]
                                          fake :: Quantifier -> a -> Maybe CV -> GeneralizedCV
    fake q :: Quantifier
    q s :: a
    s Nothing
                                            | Quantifier
    q Quantifier -> Quantifier -> Bool
    forall a. Eq a => a -> a -> Bool
    == Quantifier
    ALL
                                            = CV -> GeneralizedCV
    RegularCV (CV -> GeneralizedCV) -> CV -> GeneralizedCV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    s) (CVal -> CV) -> CVal -> CV
    forall a b. (a -> b) -> a -> b
    $ (Maybe Int, String) -> CVal
    CUserSort (Maybe Int
    forall a. Maybe a
    Nothing, "<universally quantified>")
                                            | Bool
    True
                                            = CV -> GeneralizedCV
    RegularCV (CV -> GeneralizedCV) -> CV -> GeneralizedCV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    s) (CVal -> CV) -> CVal -> CV
    forall a b. (a -> b) -> a -> b
    $ (Maybe Int, String) -> CVal
    CUserSort (Maybe Int
    forall a. Maybe a
    Nothing, "<no binding found>")
                                          fake _ _ (Just v :: CV
    v) = CV -> GeneralizedCV
    RegularCV CV
    v

                                 notify :: String -> m ()
    notify s :: String
    s
                                   | Bool -> Bool
    not (SMTConfig -> Bool
    verbose SMTConfig
    cfg) = () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                                   | Bool
    True              = SMTConfig -> [String] -> m ()
    forall (m :: * -> *). MonadIO m => SMTConfig -> [String] -> m ()
    debug SMTConfig
    cfg ["[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
    $ "Validating the model. " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ if [((Quantifier, NamedSymVar), Maybe CV)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [((Quantifier, NamedSymVar), Maybe CV)]
    env then "There are no assignments." else "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
    forall a. [a] -> [a] -> [a]
    ++ String
    l | String
    l <- String -> [String]
    lines String
    envShown]

                             Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    univs) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
                                    String -> m ()
    forall (m :: * -> *). MonadIO m => String -> m ()
    notify (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ "NB. The following variable(s) are universally quantified: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", " [String]
    univs
                                    String -> m ()
    forall (m :: * -> *). MonadIO m => String -> m ()
    notify   "    We will assume that they are essentially zero for the purposes of validation."
                                    String -> m ()
    forall (m :: * -> *). MonadIO m => String -> m ()
    notify   "    Note that this is a gross simplification of the model validation with universals!"

                             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
    <$> SBVRunMode -> SymbolicT m SBool -> m (SBool, Result)
    forall (m :: * -> *) a.
    MonadIO m =>
    SBVRunMode -> SymbolicT m a -> m (a, Result)
    runSymbolic (Maybe (Bool, [((Quantifier, NamedSymVar), Maybe CV)]) -> SBVRunMode
    Concrete ((Bool, [((Quantifier, NamedSymVar), Maybe CV)])
    -> Maybe (Bool, [((Quantifier, NamedSymVar), Maybe CV)])
    forall a. a -> Maybe a
    Just (Bool
    isSAT, [((Quantifier, NamedSymVar), Maybe CV)]
    env))) ((if Bool
    isSAT then a -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forSome_ a
    p else a -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_ a
    p) SymbolicT m SBool
    -> (SBool -> SymbolicT m SBool) -> SymbolicT m SBool
    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
    output)

                             let explain :: [String]
    explain  = [ ""
                                            , "Assignment:"  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ if [((Quantifier, NamedSymVar), Maybe CV)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [((Quantifier, NamedSymVar), Maybe CV)]
    env then " <none>" else ""
                                            ]
                                         [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ ""          | Bool -> Bool
    not ([((Quantifier, NamedSymVar), Maybe CV)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [((Quantifier, NamedSymVar), Maybe CV)]
    env)]
                                         [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ "    " 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]
    ++ [ "" ]

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

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

                                 notConcrete :: SV -> m SMTResult
    notConcrete sv :: SV
    sv = String -> [String] -> m SMTResult
    forall (m :: * -> *). Monad m => String -> [String] -> m SMTResult
    wrap ("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]
    ++ " is not concretely computable.")
                                                       (  Maybe String -> [String]
    perhaps (SV -> Maybe String
    why SV
    sv)
                                                       [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ "SBV's model validator is incomplete, and cannot handle this particular case."
                                                          , "Please report this as a feature request or possibly a bug!"
                                                          ]
                                                       )
                                      where perhaps :: Maybe String -> [String]
    perhaps Nothing  = []
                                            perhaps (Just x :: String
    x) = [String
    x, ""]

                                            -- This is incomplete, but should capture the most common cases
                                            why :: SV -> Maybe String
    why s :: 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 (t :: * -> *) a. Foldable t => t a -> [a]
    S.toList (SBVPgm -> Seq (SV, SBVExpr)
    pgmAssignments (Result -> SBVPgm
    resAsgns Result
    result)) of
                                                      Nothing            -> Maybe String
    forall a. Maybe a
    Nothing
                                                      Just (SBVApp o :: Op
    o as :: [SV]
    as) -> case Op
    o of
                                                                              Uninterpreted v :: String
    v   -> String -> Maybe String
    forall a. a -> Maybe a
    Just (String -> Maybe String) -> String -> Maybe String
    forall a b. (a -> b) -> a -> b
    $ "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]
    ++ "."
                                                                              IEEEFP FP_FMA     -> String -> Maybe String
    forall a. a -> Maybe a
    Just "Floating point FMA operation is not supported concretely."
                                                                              IEEEFP _          -> String -> Maybe String
    forall a. a -> Maybe a
    Just "Not all floating point operations are supported concretely."
                                                                              OverflowOp _      -> String -> Maybe String
    forall a. a -> Maybe a
    Just "Overflow-checking is not done concretely."
                                                                              _                 -> [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 (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 [] cont :: m SMTResult
    cont = do
                                    Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([(Bool, [(String, String)], SV)] -> 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 "Validated all constraints."
                                    m SMTResult
    cont
                                 walkConstraints ((isSoft :: Bool
    isSoft, attrs :: [(String, a)]
    attrs, sv :: SV
    sv) : rest :: [(Bool, [(String, a)], SV)]
    rest) cont :: 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
    $ "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]
    ++ " 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 nm :: 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
    $ "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]
    ++ " evaluated to False."
                                        Nothing -> String -> m SMTResult
    forall (m :: * -> *). Monad m => String -> m SMTResult
    badModel "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 | (":named", n :: 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 "All outputs are satisfied. Validation complete."
                                        SMTResult -> m SMTResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTResult
    res
                                 satLoop (sv :: SV
    sv:svs :: [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
    $ "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]
    ++ " 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 "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 [] somethingFailed :: Bool
    somethingFailed
                                   | Bool
    somethingFailed = do String -> m ()
    forall (m :: * -> *). MonadIO m => String -> m ()
    notify "Counterexample is validated."
                                                          SMTResult -> m SMTResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTResult
    res
                                   | Bool
    True            = do String -> m ()
    forall (m :: * -> *). MonadIO m => String -> m ()
    notify "Counterexample violates none of the outputs."
                                                          String -> m SMTResult
    forall (m :: * -> *). Monad m => String -> m SMTResult
    badModel "Counter-example violates no constraints."
                                 proveLoop (sv :: SV
    sv:svs :: [SV]
    svs) somethingFailed :: 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
    $ "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]
    ++ " 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 (t :: * -> *) a. Foldable t => t a -> Bool
    null [(Bool, [(String, String)], SV)]
    cstrs
                                   = String -> m SMTResult
    forall (m :: * -> *). Monad m => String -> m SMTResult
    giveUp "Impossible happened: There are no outputs nor any constraints to check."
                                 checkOutputs os :: [SV]
    os
                                   = do String -> m ()
    forall (m :: * -> *). MonadIO m => String -> m ()
    notify "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 (t :: * -> *) a. Foldable t => t a -> Bool
    null [(Bool, [(String, String)], SV)]
    cstrs
                                      then "There are no constraints to check."
                                      else "Validating " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show ([(Bool, [(String, String)], SV)] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [(Bool, [(String, String)], SV)]
    cstrs) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " 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))

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

    -- | 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 :: [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.
    MProvable m a =>
    SMTConfig -> a -> m ThmResult
    proveWith)

    -- | 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 :: [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.
    MProvable m a =>
    SMTConfig -> a -> m ThmResult
    proveWith)

    -- | 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 :: Provable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
    satWithAll :: [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.
    MProvable 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 :: Provable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, SatResult)
    satWithAny :: [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.
    MProvable 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 :: Provable a => SMTConfig -> [Query b] -> a -> IO (Solver, NominalDiffTime, SatResult)
    satConcurrentWithAny :: SMTConfig
    -> [Query b] -> a -> IO (Solver, NominalDiffTime, SatResult)
    satConcurrentWithAny solver :: SMTConfig
    solver qs :: [Query b]
    qs a :: a
    a = do (slvr :: Solver
    slvr,time :: NominalDiffTime
    time,result :: 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.
    MProvable m a =>
    SMTConfig -> a -> QueryT m a -> m SMTResult
    go [Query b]
    qs a
    a
                                          (Solver, NominalDiffTime, SatResult)
    -> IO (Solver, NominalDiffTime, SatResult)
    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 cfg :: SMTConfig
    cfg a' :: a
    a' q :: QueryT m a
    q = Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
    forall (m :: * -> *) a b.
    MProvable m a =>
    Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery 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 (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 return the first that finishes, killing the others
    proveConcurrentWithAny :: Provable a => SMTConfig -> [Query b] -> a -> IO (Solver, NominalDiffTime, ThmResult)
    proveConcurrentWithAny :: SMTConfig
    -> [Query b] -> a -> IO (Solver, NominalDiffTime, ThmResult)
    proveConcurrentWithAny solver :: SMTConfig
    solver qs :: [Query b]
    qs a :: a
    a = do (slvr :: Solver
    slvr,time :: NominalDiffTime
    time,result :: 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.
    MProvable m a =>
    SMTConfig -> a -> QueryT m a -> m SMTResult
    go [Query b]
    qs a
    a
                                            (Solver, NominalDiffTime, ThmResult)
    -> IO (Solver, NominalDiffTime, ThmResult)
    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 cfg :: SMTConfig
    cfg a' :: a
    a' q :: QueryT m a
    q = Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
    forall (m :: * -> *) a b.
    MProvable m a =>
    Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery 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 (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 :: Provable a => SMTConfig -> [Query b] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
    satConcurrentWithAll :: SMTConfig
    -> [Query b] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
    satConcurrentWithAll solver :: SMTConfig
    solver qs :: [Query b]
    qs a :: 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.
    MProvable m a =>
    SMTConfig -> a -> QueryT m a -> m SMTResult
    go [Query b]
    qs a
    a
                                          [(Solver, NominalDiffTime, SatResult)]
    -> IO [(Solver, NominalDiffTime, SatResult)]
    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
    $ (\(a' :: Solver
    a',b :: NominalDiffTime
    b,c :: 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 cfg :: SMTConfig
    cfg a' :: a
    a' q :: QueryT m a
    q = Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
    forall (m :: * -> *) a b.
    MProvable m a =>
    Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery 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 (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 :: SMTConfig
    -> [Query b] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
    proveConcurrentWithAll solver :: SMTConfig
    solver qs :: [Query b]
    qs a :: 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.
    MProvable m a =>
    SMTConfig -> a -> QueryT m a -> m SMTResult
    go [Query b]
    qs a
    a
                                            [(Solver, NominalDiffTime, ThmResult)]
    -> IO [(Solver, NominalDiffTime, ThmResult)]
    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
    $ (\(a' :: Solver
    a',b :: NominalDiffTime
    b,c :: 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 cfg :: SMTConfig
    cfg a' :: a
    a' q :: QueryT m a
    q = Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
    forall (m :: * -> *) a b.
    MProvable m a =>
    Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery 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 (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'

    -- | Create an SMT-Lib2 benchmark. The 'Bool' argument controls whether this is a SAT instance, i.e.,
    -- translate the query directly, or a PROVE instance, i.e., translate the negated query.
    generateSMTBenchmark :: (MonadIO m, MProvable m a) => Bool -> a -> m String
    generateSMTBenchmark :: Bool -> a -> m String
    generateSMTBenchmark isSat :: Bool
    isSat a :: a
    a = do
          ZonedTime
    t <- IO ZonedTime -> m ZonedTime
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO ZonedTime
    getZonedTime

          let comments :: [String]
    comments = ["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 }

          (_, res :: Result
    res) <- SBVRunMode -> SymbolicT m SBool -> m (SBool, Result)
    forall (m :: * -> *) a.
    MonadIO m =>
    SBVRunMode -> SymbolicT m a -> m (a, Result)
    runSymbolic (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
    $ (if Bool
    isSat then a -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forSome_ else a -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_) a
    a SymbolicT m SBool
    -> (SBool -> SymbolicT m SBool) -> SymbolicT m SBool
    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
    output

          let SMTProblem{SMTConfig -> SMTLibPgm
    smtLibPgm :: SMTProblem -> SMTConfig -> SMTLibPgm
    smtLibPgm :: 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 (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]
    ++ "\n(check-sat)\n"

    checkNoOptimizations :: MonadIO m => QueryT m ()
    checkNoOptimizations :: 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 (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 [ ""
                                                    , "*** Data.SBV: Unsupported call sat/prove when optimization objectives are present."
                                                    , "*** Use \"optimize\"/\"optimizeWith\" to calculate optimal satisfaction!"
                                                    ]

    -- If we get a program producing nothing (i.e., Symbolic ()), pretend it simply returns True.
    -- This is useful since min/max calls and constraints will provide the context
    instance ExtractIO m => MProvable m (SymbolicT m ()) where
      forAll_ :: SymbolicT m () -> SymbolicT m SBool
    forAll_    a :: SymbolicT m ()
    a = SymbolicT m SBool -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_    ((SymbolicT m ()
    a SymbolicT m () -> SymbolicT m SBool -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBool -> SymbolicT m SBool
    forall (m :: * -> *) a. Monad m => a -> m a
    return SBool
    sTrue) :: SymbolicT m SBool)
      forAll :: [String] -> SymbolicT m () -> SymbolicT m SBool
    forAll ns :: [String]
    ns  a :: SymbolicT m ()
    a = [String] -> SymbolicT m SBool -> SymbolicT m SBool
    forall (m :: * -> *) a.
    MProvable m a =>
    [String] -> a -> SymbolicT m SBool
    forAll [String]
    ns  ((SymbolicT m ()
    a SymbolicT m () -> SymbolicT m SBool -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBool -> SymbolicT m SBool
    forall (m :: * -> *) a. Monad m => a -> m a
    return SBool
    sTrue) :: SymbolicT m SBool)
      forSome_ :: SymbolicT m () -> SymbolicT m SBool
    forSome_   a :: SymbolicT m ()
    a = SymbolicT m SBool -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forSome_   ((SymbolicT m ()
    a SymbolicT m () -> SymbolicT m SBool -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBool -> SymbolicT m SBool
    forall (m :: * -> *) a. Monad m => a -> m a
    return SBool
    sTrue) :: SymbolicT m SBool)
      forSome :: [String] -> SymbolicT m () -> SymbolicT m SBool
    forSome ns :: [String]
    ns a :: SymbolicT m ()
    a = [String] -> SymbolicT m SBool -> SymbolicT m SBool
    forall (m :: * -> *) a.
    MProvable m a =>
    [String] -> a -> SymbolicT m SBool
    forSome [String]
    ns ((SymbolicT m ()
    a SymbolicT m () -> SymbolicT m SBool -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> SBool -> SymbolicT m SBool
    forall (m :: * -> *) a. Monad m => a -> m a
    return SBool
    sTrue) :: SymbolicT m SBool)

    instance ExtractIO m => MProvable m (SymbolicT m SBool) where
      forAll_ :: SymbolicT m SBool -> SymbolicT m SBool
    forAll_    = SymbolicT m SBool -> SymbolicT m SBool
    forall a. a -> a
    id
      forAll :: [String] -> SymbolicT m SBool -> SymbolicT m SBool
    forAll []  = SymbolicT m SBool -> SymbolicT m SBool
    forall a. a -> a
    id
      forAll xs :: [String]
    xs  = String -> SymbolicT m SBool -> SymbolicT m SBool
    forall a. HasCallStack => String -> a
    error (String -> SymbolicT m SBool -> SymbolicT m SBool)
    -> String -> SymbolicT m SBool -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ "SBV.forAll: Extra unmapped name(s) in predicate construction: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", " [String]
    xs
      forSome_ :: SymbolicT m SBool -> SymbolicT m SBool
    forSome_   = SymbolicT m SBool -> SymbolicT m SBool
    forall a. a -> a
    id
      forSome :: [String] -> SymbolicT m SBool -> SymbolicT m SBool
    forSome [] = SymbolicT m SBool -> SymbolicT m SBool
    forall a. a -> a
    id
      forSome xs :: [String]
    xs = String -> SymbolicT m SBool -> SymbolicT m SBool
    forall a. HasCallStack => String -> a
    error (String -> SymbolicT m SBool -> SymbolicT m SBool)
    -> String -> SymbolicT m SBool -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ "SBV.forSome: Extra unmapped name(s) in predicate construction: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", " [String]
    xs

    instance ExtractIO m => MProvable m SBool where
      forAll_ :: SBool -> SymbolicT m SBool
    forAll_   = SBool -> SymbolicT m SBool
    forall (m :: * -> *) a. Monad m => a -> m a
    return
      forAll :: [String] -> SBool -> SymbolicT m SBool
    forAll _  = SBool -> SymbolicT m SBool
    forall (m :: * -> *) a. Monad m => a -> m a
    return
      forSome_ :: SBool -> SymbolicT m SBool
    forSome_  = SBool -> SymbolicT m SBool
    forall (m :: * -> *) a. Monad m => a -> m a
    return
      forSome :: [String] -> SBool -> SymbolicT m SBool
    forSome _ = SBool -> SymbolicT m SBool
    forall (m :: * -> *) a. Monad m => a -> m a
    return

    {-
    -- The following works, 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 .==).
    instance Provable Bool where
      forAll_  x  = forAll_   (if x then true else false :: SBool)
      forAll s x  = forAll s  (if x then true else false :: SBool)
      forSome_  x = forSome_  (if x then true else false :: SBool)
      forSome s x = forSome s (if x then true else false :: SBool)
    -}

    -- Functions
    instance (SymVal a, MProvable m p) => MProvable m (SBV a -> p) where
      forAll_ :: (SBV a -> p) -> SymbolicT m SBool
    forAll_        k :: SBV a -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    forall_   SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> p -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_   (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ SBV a -> p
    k SBV a
    a
      forAll :: [String] -> (SBV a -> p) -> SymbolicT m SBool
    forAll (s :: String
    s:ss :: [String]
    ss)  k :: SBV a -> p
    k = String -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    forall String
    s  SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> [String] -> p -> SymbolicT m SBool
    forall (m :: * -> *) a.
    MProvable m a =>
    [String] -> a -> SymbolicT m SBool
    forAll [String]
    ss (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ SBV a -> p
    k SBV a
    a
      forAll []      k :: SBV a -> p
    k = (SBV a -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_ SBV a -> p
    k
      forSome_ :: (SBV a -> p) -> SymbolicT m SBool
    forSome_       k :: SBV a -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    exists_  SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> p -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forSome_   (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ SBV a -> p
    k SBV a
    a
      forSome :: [String] -> (SBV a -> p) -> SymbolicT m SBool
    forSome (s :: String
    s:ss :: [String]
    ss) k :: SBV a -> p
    k = String -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    exists String
    s SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> [String] -> p -> SymbolicT m SBool
    forall (m :: * -> *) a.
    MProvable m a =>
    [String] -> a -> SymbolicT m SBool
    forSome [String]
    ss (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ SBV a -> p
    k SBV a
    a
      forSome []     k :: SBV a -> p
    k = (SBV a -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forSome_ SBV a -> p
    k

    -- SFunArrays (memory, functional representation), only supported universally for the time being
    instance (HasKind a, HasKind b, MProvable m p) => MProvable m (SArray a b -> p) where
      forAll_ :: (SArray a b -> p) -> SymbolicT m SBool
    forAll_       k :: SArray a b -> p
    k = Maybe (SBV b) -> SymbolicT 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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SArray a b
    a -> p -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_   (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ SArray a b -> p
    k SArray a b
    a
      forAll :: [String] -> (SArray a b -> p) -> SymbolicT m SBool
    forAll (s :: String
    s:ss :: [String]
    ss) k :: SArray a b -> p
    k = String -> Maybe (SBV b) -> SymbolicT m (SArray a b)
    forall (array :: * -> * -> *) (m :: * -> *) a b.
    (SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
    String -> Maybe (SBV b) -> m (array a b)
    newArray String
    s Maybe (SBV b)
    forall a. Maybe a
    Nothing SymbolicT m (SArray a b)
    -> (SArray a b -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SArray a b
    a -> [String] -> p -> SymbolicT m SBool
    forall (m :: * -> *) a.
    MProvable m a =>
    [String] -> a -> SymbolicT m SBool
    forAll [String]
    ss (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ SArray a b -> p
    k SArray a b
    a
      forAll []     k :: SArray a b -> p
    k = (SArray a b -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_ SArray a b -> p
    k
      forSome_ :: (SArray a b -> p) -> SymbolicT m SBool
    forSome_      _ = String -> SymbolicT m SBool
    forall a. HasCallStack => String -> a
    error "SBV.forSome.SFunArray: Existential arrays are not currently supported."
      forSome :: [String] -> (SArray a b -> p) -> SymbolicT m SBool
    forSome _     _ = String -> SymbolicT m SBool
    forall a. HasCallStack => String -> a
    error "SBV.forSome.SFunArray: Existential arrays are not currently supported."

    -- SArrays (memory, SMT-Lib notion of arrays), only supported universally for the time being
    instance (HasKind a, HasKind b, MProvable m p) => MProvable m (SFunArray a b -> p) where
      forAll_ :: (SFunArray a b -> p) -> SymbolicT m SBool
    forAll_       k :: SFunArray a b -> p
    k = Maybe (SBV b) -> SymbolicT m (SFunArray 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 (SFunArray a b)
    -> (SFunArray a b -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SFunArray a b
    a -> p -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_   (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ SFunArray a b -> p
    k SFunArray a b
    a
      forAll :: [String] -> (SFunArray a b -> p) -> SymbolicT m SBool
    forAll (s :: String
    s:ss :: [String]
    ss) k :: SFunArray a b -> p
    k = String -> Maybe (SBV b) -> SymbolicT m (SFunArray a b)
    forall (array :: * -> * -> *) (m :: * -> *) a b.
    (SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
    String -> Maybe (SBV b) -> m (array a b)
    newArray String
    s Maybe (SBV b)
    forall a. Maybe a
    Nothing SymbolicT m (SFunArray a b)
    -> (SFunArray a b -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SFunArray a b
    a -> [String] -> p -> SymbolicT m SBool
    forall (m :: * -> *) a.
    MProvable m a =>
    [String] -> a -> SymbolicT m SBool
    forAll [String]
    ss (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ SFunArray a b -> p
    k SFunArray a b
    a
      forAll []     k :: SFunArray a b -> p
    k = (SFunArray a b -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_ SFunArray a b -> p
    k
      forSome_ :: (SFunArray a b -> p) -> SymbolicT m SBool
    forSome_      _ = String -> SymbolicT m SBool
    forall a. HasCallStack => String -> a
    error "SBV.forSome.SArray: Existential arrays are not currently supported."
      forSome :: [String] -> (SFunArray a b -> p) -> SymbolicT m SBool
    forSome _     _ = String -> SymbolicT m SBool
    forall a. HasCallStack => String -> a
    error "SBV.forSome.SArray: Existential arrays are not currently supported."

    -- 2 Tuple
    instance (SymVal a, SymVal b, MProvable m p) => MProvable m ((SBV a, SBV b) -> p) where
      forAll_ :: ((SBV a, SBV b) -> p) -> SymbolicT m SBool
    forAll_        k :: (SBV a, SBV b) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    forall_  SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> (SBV b -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_   ((SBV b -> p) -> SymbolicT m SBool)
    -> (SBV b -> p) -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ \b :: SBV b
    b -> (SBV a, SBV b) -> p
    k (SBV a
    a, SBV b
    b)
      forAll :: [String] -> ((SBV a, SBV b) -> p) -> SymbolicT m SBool
    forAll (s :: String
    s:ss :: [String]
    ss)  k :: (SBV a, SBV b) -> p
    k = String -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    forall String
    s SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> [String] -> (SBV b -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a.
    MProvable m a =>
    [String] -> a -> SymbolicT m SBool
    forAll [String]
    ss ((SBV b -> p) -> SymbolicT m SBool)
    -> (SBV b -> p) -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ \b :: SBV b
    b -> (SBV a, SBV b) -> p
    k (SBV a
    a, SBV b
    b)
      forAll []      k :: (SBV a, SBV b) -> p
    k = ((SBV a, SBV b) -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_ (SBV a, SBV b) -> p
    k
      forSome_ :: ((SBV a, SBV b) -> p) -> SymbolicT m SBool
    forSome_       k :: (SBV a, SBV b) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    exists_  SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> (SBV b -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forSome_   ((SBV b -> p) -> SymbolicT m SBool)
    -> (SBV b -> p) -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ \b :: SBV b
    b -> (SBV a, SBV b) -> p
    k (SBV a
    a, SBV b
    b)
      forSome :: [String] -> ((SBV a, SBV b) -> p) -> SymbolicT m SBool
    forSome (s :: String
    s:ss :: [String]
    ss) k :: (SBV a, SBV b) -> p
    k = String -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    exists String
    s SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> [String] -> (SBV b -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a.
    MProvable m a =>
    [String] -> a -> SymbolicT m SBool
    forSome [String]
    ss ((SBV b -> p) -> SymbolicT m SBool)
    -> (SBV b -> p) -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ \b :: SBV b
    b -> (SBV a, SBV b) -> p
    k (SBV a
    a, SBV b
    b)
      forSome []     k :: (SBV a, SBV b) -> p
    k = ((SBV a, SBV b) -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forSome_ (SBV a, SBV b) -> p
    k

    -- 3 Tuple
    instance (SymVal a, SymVal b, SymVal c, MProvable m p) => MProvable m ((SBV a, SBV b, SBV c) -> p) where
      forAll_ :: ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
    forAll_       k :: (SBV a, SBV b, SBV c) -> p
    k  = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    forall_  SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_   ((SBV b -> SBV c -> p) -> SymbolicT m SBool)
    -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ \b :: SBV b
    b c :: SBV c
    c -> (SBV a, SBV b, SBV c) -> p
    k (SBV a
    a, SBV b
    b, SBV c
    c)
      forAll :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
    forAll (s :: String
    s:ss :: [String]
    ss) k :: (SBV a, SBV b, SBV c) -> p
    k  = String -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    forall String
    s SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> [String] -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a.
    MProvable m a =>
    [String] -> a -> SymbolicT m SBool
    forAll [String]
    ss ((SBV b -> SBV c -> p) -> SymbolicT m SBool)
    -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ \b :: SBV b
    b c :: SBV c
    c -> (SBV a, SBV b, SBV c) -> p
    k (SBV a
    a, SBV b
    b, SBV c
    c)
      forAll []     k :: (SBV a, SBV b, SBV c) -> p
    k  = ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_ (SBV a, SBV b, SBV c) -> p
    k
      forSome_ :: ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
    forSome_       k :: (SBV a, SBV b, SBV c) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    exists_  SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forSome_   ((SBV b -> SBV c -> p) -> SymbolicT m SBool)
    -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ \b :: SBV b
    b c :: SBV c
    c -> (SBV a, SBV b, SBV c) -> p
    k (SBV a
    a, SBV b
    b, SBV c
    c)
      forSome :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
    forSome (s :: String
    s:ss :: [String]
    ss) k :: (SBV a, SBV b, SBV c) -> p
    k = String -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    exists String
    s SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> [String] -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a.
    MProvable m a =>
    [String] -> a -> SymbolicT m SBool
    forSome [String]
    ss ((SBV b -> SBV c -> p) -> SymbolicT m SBool)
    -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
    forall a b. (a -> b) -> a -> b
    $ \b :: SBV b
    b c :: SBV c
    c -> (SBV a, SBV b, SBV c) -> p
    k (SBV a
    a, SBV b
    b, SBV c
    c)
      forSome []     k :: (SBV a, SBV b, SBV c) -> p
    k = ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forSome_ (SBV a, SBV b, SBV c) -> p
    k

    -- 4 Tuple
    instance (SymVal a, SymVal b, SymVal c, SymVal d, MProvable m p) => MProvable m ((SBV a, SBV b, SBV c, SBV d) -> p) where
      forAll_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
    forAll_        k :: (SBV a, SBV b, SBV c, SBV d) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    forall_  SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_   ((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
    $ \b :: SBV b
    b c :: SBV c
    c d :: 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)
      forAll :: [String]
    -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
    forAll (s :: String
    s:ss :: [String]
    ss)  k :: (SBV a, SBV b, SBV c, SBV d) -> p
    k = String -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    forall String
    s SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> [String] -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a.
    MProvable m a =>
    [String] -> a -> SymbolicT m SBool
    forAll [String]
    ss ((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
    $ \b :: SBV b
    b c :: SBV c
    c d :: 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)
      forAll []      k :: (SBV a, SBV b, SBV c, SBV d) -> p
    k = ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_ (SBV a, SBV b, SBV c, SBV d) -> p
    k
      forSome_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
    forSome_       k :: (SBV a, SBV b, SBV c, SBV d) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    exists_  SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forSome_   ((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
    $ \b :: SBV b
    b c :: SBV c
    c d :: 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)
      forSome :: [String]
    -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
    forSome (s :: String
    s:ss :: [String]
    ss) k :: (SBV a, SBV b, SBV c, SBV d) -> p
    k = String -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    exists String
    s SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> [String] -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a.
    MProvable m a =>
    [String] -> a -> SymbolicT m SBool
    forSome [String]
    ss ((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
    $ \b :: SBV b
    b c :: SBV c
    c d :: 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)
      forSome []     k :: (SBV a, SBV b, SBV c, SBV d) -> p
    k = ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forSome_ (SBV a, SBV b, SBV c, SBV d) -> p
    k

    -- 5 Tuple
    instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, MProvable m p) => MProvable m ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) where
      forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
    forAll_        k :: (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)
    forall_  SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_   ((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
    $ \b :: SBV b
    b c :: SBV c
    c d :: SBV d
    d e :: 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)
      forAll :: [String]
    -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
    forAll (s :: String
    s:ss :: [String]
    ss)  k :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
    k = String -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    forall String
    s SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> [String]
    -> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a.
    MProvable m a =>
    [String] -> a -> SymbolicT m SBool
    forAll [String]
    ss ((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
    $ \b :: SBV b
    b c :: SBV c
    c d :: SBV d
    d e :: 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)
      forAll []      k :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
    k = ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_ (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
    k
      forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
    forSome_       k :: (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)
    exists_  SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forSome_   ((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
    $ \b :: SBV b
    b c :: SBV c
    c d :: SBV d
    d e :: 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)
      forSome :: [String]
    -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
    forSome (s :: String
    s:ss :: [String]
    ss) k :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
    k = String -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    exists String
    s SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> [String]
    -> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a.
    MProvable m a =>
    [String] -> a -> SymbolicT m SBool
    forSome [String]
    ss ((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
    $ \b :: SBV b
    b c :: SBV c
    c d :: SBV d
    d e :: 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)
      forSome []     k :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
    k = ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forSome_ (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
    k

    -- 6 Tuple
    instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, MProvable m p) => MProvable m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) where
      forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
    -> SymbolicT m SBool
    forAll_        k :: (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)
    forall_  SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
    -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_   ((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
    $ \b :: SBV b
    b c :: SBV c
    c d :: SBV d
    d e :: SBV e
    e f :: 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)
      forAll :: [String]
    -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
    -> SymbolicT m SBool
    forAll (s :: String
    s:ss :: [String]
    ss)  k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
    k = String -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    forall String
    s SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> [String]
    -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
    -> SymbolicT m SBool
    forall (m :: * -> *) a.
    MProvable m a =>
    [String] -> a -> SymbolicT m SBool
    forAll [String]
    ss ((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
    $ \b :: SBV b
    b c :: SBV c
    c d :: SBV d
    d e :: SBV e
    e f :: 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)
      forAll []      k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
    k = ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
    -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_ (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
    k
      forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
    -> SymbolicT m SBool
    forSome_       k :: (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)
    exists_  SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
    -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forSome_   ((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
    $ \b :: SBV b
    b c :: SBV c
    c d :: SBV d
    d e :: SBV e
    e f :: 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)
      forSome :: [String]
    -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
    -> SymbolicT m SBool
    forSome (s :: String
    s:ss :: [String]
    ss) k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
    k = String -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    exists String
    s SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> [String]
    -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
    -> SymbolicT m SBool
    forall (m :: * -> *) a.
    MProvable m a =>
    [String] -> a -> SymbolicT m SBool
    forSome [String]
    ss ((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
    $ \b :: SBV b
    b c :: SBV c
    c d :: SBV d
    d e :: SBV e
    e f :: 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)
      forSome []     k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
    k = ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
    -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forSome_ (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
    k

    -- 7 Tuple
    instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, MProvable m p) => MProvable m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) where
      forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
    -> SymbolicT m SBool
    forAll_        k :: (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)
    forall_  SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
    -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_   ((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
    $ \b :: SBV b
    b c :: SBV c
    c d :: SBV d
    d e :: SBV e
    e f :: SBV f
    f g :: 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)
      forAll :: [String]
    -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
    -> SymbolicT m SBool
    forAll (s :: String
    s:ss :: [String]
    ss)  k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
    k = String -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    forall String
    s SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> [String]
    -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
    -> SymbolicT m SBool
    forall (m :: * -> *) a.
    MProvable m a =>
    [String] -> a -> SymbolicT m SBool
    forAll [String]
    ss ((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
    $ \b :: SBV b
    b c :: SBV c
    c d :: SBV d
    d e :: SBV e
    e f :: SBV f
    f g :: 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)
      forAll []      k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
    k = ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
    -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_ (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
    k
      forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
    -> SymbolicT m SBool
    forSome_       k :: (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)
    exists_  SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
    -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forSome_   ((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
    $ \b :: SBV b
    b c :: SBV c
    c d :: SBV d
    d e :: SBV e
    e f :: SBV f
    f g :: 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)
      forSome :: [String]
    -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
    -> SymbolicT m SBool
    forSome (s :: String
    s:ss :: [String]
    ss) k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
    k = String -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    exists String
    s SymbolicT m (SBV a)
    -> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> [String]
    -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
    -> SymbolicT m SBool
    forall (m :: * -> *) a.
    MProvable m a =>
    [String] -> a -> SymbolicT m SBool
    forSome [String]
    ss ((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
    $ \b :: SBV b
    b c :: SBV c
    c d :: SBV d
    d e :: SBV e
    e f :: SBV f
    f g :: 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)
      forSome []     k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
    k = ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
    -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forSome_ (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
    k

    -- | Generalization of 'Data.SBV.runSMT'
    runSMT :: MonadIO m => SymbolicT m a -> m a
    runSMT :: 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 :: SMTConfig -> SymbolicT m a -> m a
    runSMTWith cfg :: SMTConfig
    cfg a :: 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
    <$> SBVRunMode -> SymbolicT m a -> m (a, Result)
    forall (m :: * -> *) a.
    MonadIO m =>
    SBVRunMode -> SymbolicT m a -> m (a, Result)
    runSymbolic (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
    SMTMode QueryContext
    QueryExternal IStage
    ISetup Bool
    True SMTConfig
    cfg) SymbolicT m a
    a

    -- | Runs with a query.
    runWithQuery :: MProvable m a => Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery :: Bool -> QueryT m b -> SMTConfig -> a -> m b
    runWithQuery isSAT :: Bool
    isSAT q :: QueryT m b
    q cfg :: SMTConfig
    cfg a :: 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
    <$> SBVRunMode -> SymbolicT m b -> m (b, Result)
    forall (m :: * -> *) a.
    MonadIO m =>
    SBVRunMode -> SymbolicT m a -> m (a, Result)
    runSymbolic (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
    _ <- (if Bool
    isSAT then a -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forSome_ else a -> SymbolicT m SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    forAll_) a
    a SymbolicT m SBool
    -> (SBool -> SymbolicT m SBool) -> SymbolicT m SBool
    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
    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 (_, _, result :: SMTResult
    result)) = case SMTResult
    result of
                                           Unsatisfiable{} -> Bool
    True
                                           Satisfiable{}   -> Bool
    False
                                           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 :: UTCTime
    -> (SMTConfig -> IO b)
    -> SMTConfig
    -> IO (Async (Solver, NominalDiffTime, b))
    runInThread beginTime :: UTCTime
    beginTime action :: SMTConfig -> IO b
    action config :: 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 (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 :: [SMTConfig]
    -> (SMTConfig -> a -> IO b) -> a -> IO (Solver, NominalDiffTime, b)
    sbvWithAny []      _    _ = String -> IO (Solver, NominalDiffTime, b)
    forall a. HasCallStack => String -> a
    error "SBV.withAny: No solvers given!"
    sbvWithAny solvers :: [SMTConfig]
    solvers what :: SMTConfig -> a -> IO b
    what a :: 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 (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)
    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 (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 asyncs :: [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 other :: 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 :: SMTConfig
    -> (SMTConfig -> a -> QueryT m b -> IO c)
    -> [QueryT m b]
    -> a
    -> IO (Solver, NominalDiffTime, c)
    sbvConcurrentWithAny solver :: SMTConfig
    solver what :: SMTConfig -> a -> QueryT m b -> IO c
    what queries :: [QueryT m b]
    queries a :: 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 (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)
    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 (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 asyncs :: [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 other :: 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 q :: 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 (\cfg :: 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 :: SMTConfig
    -> (SMTConfig -> a -> QueryT m b -> IO c)
    -> [QueryT m b]
    -> a
    -> IO [(Solver, NominalDiffTime, c)]
    sbvConcurrentWithAll solver :: SMTConfig
    solver what :: SMTConfig -> a -> QueryT m b -> IO c
    what queries :: [QueryT m b]
    queries a :: 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 (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 q :: 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 (\cfg :: 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 (m :: * -> *) a. Monad m => a -> m a
    return []
             go as :: [Async a]
    as  = do (d :: Async a
    d, r :: 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 (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 :: [SMTConfig]
    -> (SMTConfig -> a -> IO b)
    -> a
    -> IO [(Solver, NominalDiffTime, b)]
    sbvWithAll solvers :: [SMTConfig]
    solvers what :: SMTConfig -> a -> IO b
    what a :: 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)
    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 (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 (m :: * -> *) a. Monad m => a -> m a
    return []
             go as :: [Async a]
    as  = do (d :: Async a
    d, r :: 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 (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 sufficently 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.sName'
       sName  :: [String] -> 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 cfg :: SMTConfig
    cfg a :: a
    a = do String
    cwd <- (String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "/") (String -> String) -> m String -> m String
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO String -> m String
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO String
    getCurrentDirectory
                           let mkRelative :: String -> String
    mkRelative path :: 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 (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
    <$> SBVRunMode -> SymbolicT m [SafeResult] -> m ([SafeResult], Result)
    forall (m :: * -> *) a.
    MonadIO m =>
    SBVRunMode -> SymbolicT m a -> m (a, Result)
    runSymbolic (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 (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 mkRelative :: 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 (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)
    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 mkRelative :: String -> String
    mkRelative (msg :: String
    msg, cs :: Maybe CallStack
    cs, cond :: SV
    cond) = do
                       let locInfo :: [(String, SrcLoc)] -> String
    locInfo ps :: [(String, SrcLoc)]
    ps = let loc :: (String, SrcLoc) -> String
    loc (f :: String
    f, sl :: SrcLoc
    sl) = [String] -> String
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [String -> String
    mkRelative (SrcLoc -> String
    srcLocFile SrcLoc
    sl), ":", Int -> String
    forall a. Show a => a -> String
    show (SrcLoc -> Int
    srcLocStartLine SrcLoc
    sl), ":", Int -> String
    forall a. Show a => a -> String
    show (SrcLoc -> Int
    srcLocStartCol SrcLoc
    sl), ":", String
    f]
                                        in String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ",\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 (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 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
    $ "(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]
    ++ ")"
                                    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 1
                                    SMTResult -> QueryT m SMTResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTResult
    r

                       SafeResult -> QueryT m SafeResult
    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_   a :: SymbolicT m a
    a = SymbolicT m a
    a SymbolicT m a -> (a -> SymbolicT m ()) -> SymbolicT m ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \r :: 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 (m :: * -> *) a. Monad m => a -> m a
    return ()
       sName :: [String] -> SymbolicT m a -> SymbolicT m ()
    sName []   = SymbolicT m a -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName_
       sName xs :: [String]
    xs   = String -> SymbolicT m a -> SymbolicT m ()
    forall a. HasCallStack => String -> a
    error (String -> SymbolicT m a -> SymbolicT m ())
    -> String -> SymbolicT m a -> SymbolicT m ()
    forall a b. (a -> b) -> a -> b
    $ "SBV.SExecutable.sName: Extra unmapped name(s): " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", " [String]
    xs

    instance ExtractIO m => SExecutable m (SBV a) where
       sName_ :: SBV a -> SymbolicT m ()
    sName_   v :: 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
    output SBV a
    v :: SymbolicT m (SBV a))
       sName :: [String] -> SBV a -> SymbolicT m ()
    sName xs :: [String]
    xs v :: SBV a
    v = [String] -> SymbolicT m (SBV a) -> SymbolicT m ()
    forall (m :: * -> *) a.
    SExecutable m a =>
    [String] -> a -> SymbolicT m ()
    sName [String]
    xs (SBV a -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m 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
    output () :: SymbolicT m ())
       sName :: [String] -> () -> SymbolicT m ()
    sName xs :: [String]
    xs () = [String] -> SymbolicT m () -> SymbolicT m ()
    forall (m :: * -> *) a.
    SExecutable m a =>
    [String] -> a -> SymbolicT m ()
    sName [String]
    xs (() -> SymbolicT m ()
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output () :: SymbolicT m ())

    -- List output
    instance ExtractIO m => SExecutable m [SBV a] where
       sName_ :: [SBV a] -> SymbolicT m ()
    sName_   vs :: [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
    output [SBV a]
    vs :: SymbolicT m [SBV a])
       sName :: [String] -> [SBV a] -> SymbolicT m ()
    sName xs :: [String]
    xs vs :: [SBV a]
    vs = [String] -> SymbolicT m [SBV a] -> SymbolicT m ()
    forall (m :: * -> *) a.
    SExecutable m a =>
    [String] -> a -> SymbolicT m ()
    sName [String]
    xs ([SBV a] -> SymbolicT m [SBV a]
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m 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_ (a :: SBV a
    a, b :: 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
    output SBV a
    a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV 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
    output SBV b
    b :: SymbolicT m (SBV b))
      sName :: [String] -> (SBV a, SBV b) -> SymbolicT m ()
    sName _       = (SBV a, SBV b) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName_

    -- 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_ (a :: SBV a
    a, b :: SBV b
    b, c :: 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
    output SBV a
    a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV 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
    output SBV b
    b SymbolicT m (SBV b) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
    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
    output SBV c
    c :: SymbolicT m (SBV c))
      sName :: [String] -> (SBV a, SBV b, SBV c) -> SymbolicT m ()
    sName _          = (SBV a, SBV b, SBV c) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName_

    -- 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_ (a :: SBV a
    a, b :: SBV b
    b, c :: SBV c
    c, d :: 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
    output SBV a
    a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV 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
    output SBV b
    b SymbolicT m (SBV b) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
    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
    output SBV c
    c SymbolicT m (SBV c) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
    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
    output SBV c
    c SymbolicT m (SBV c) -> SymbolicT m (SBV d) -> SymbolicT m (SBV d)
    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
    output SBV d
    d :: SymbolicT m (SBV d))
      sName :: [String] -> (SBV a, SBV b, SBV c, SBV d) -> SymbolicT m ()
    sName _             = (SBV a, SBV b, SBV c, SBV d) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName_

    -- 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_ (a :: SBV a
    a, b :: SBV b
    b, c :: SBV c
    c, d :: SBV d
    d, e :: 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
    output SBV a
    a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV 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
    output SBV b
    b SymbolicT m (SBV b) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
    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
    output SBV c
    c SymbolicT m (SBV c) -> SymbolicT m (SBV d) -> SymbolicT m (SBV d)
    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
    output SBV d
    d SymbolicT m (SBV d) -> SymbolicT m (SBV e) -> SymbolicT m (SBV e)
    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
    output SBV e
    e :: SymbolicT m (SBV e))
      sName :: [String] -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> SymbolicT m ()
    sName _                = (SBV a, SBV b, SBV c, SBV d, SBV e) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName_

    -- 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_ (a :: SBV a
    a, b :: SBV b
    b, c :: SBV c
    c, d :: SBV d
    d, e :: SBV e
    e, f :: 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
    output SBV a
    a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV 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
    output SBV b
    b SymbolicT m (SBV b) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
    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
    output SBV c
    c SymbolicT m (SBV c) -> SymbolicT m (SBV d) -> SymbolicT m (SBV d)
    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
    output SBV d
    d SymbolicT m (SBV d) -> SymbolicT m (SBV e) -> SymbolicT m (SBV e)
    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
    output SBV e
    e SymbolicT m (SBV e) -> SymbolicT m (SBV f) -> SymbolicT m (SBV f)
    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
    output SBV f
    f :: SymbolicT m (SBV f))
      sName :: [String]
    -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> SymbolicT m ()
    sName _                   = (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName_

    -- 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_ (a :: SBV a
    a, b :: SBV b
    b, c :: SBV c
    c, d :: SBV d
    d, e :: SBV e
    e, f :: SBV f
    f, g :: 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
    output SBV a
    a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV 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
    output SBV b
    b SymbolicT m (SBV b) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
    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
    output SBV c
    c SymbolicT m (SBV c) -> SymbolicT m (SBV d) -> SymbolicT m (SBV d)
    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
    output SBV d
    d SymbolicT m (SBV d) -> SymbolicT m (SBV e) -> SymbolicT m (SBV e)
    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
    output SBV e
    e SymbolicT m (SBV e) -> SymbolicT m (SBV f) -> SymbolicT m (SBV f)
    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
    output SBV f
    f SymbolicT m (SBV f) -> SymbolicT m (SBV g) -> SymbolicT m (SBV g)
    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
    output SBV g
    g :: SymbolicT m (SBV g))
      sName :: [String]
    -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g)
    -> SymbolicT m ()
    sName _                      = (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName_

    -- Functions
    instance (SymVal a, SExecutable m p) => SExecutable m (SBV a -> p) where
       sName_ :: (SBV a -> p) -> SymbolicT m ()
    sName_        k :: SBV a -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    exists_   SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: 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
       sName :: [String] -> (SBV a -> p) -> SymbolicT m ()
    sName (s :: String
    s:ss :: [String]
    ss)  k :: SBV a -> p
    k = String -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    exists String
    s  SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> [String] -> p -> SymbolicT m ()
    forall (m :: * -> *) a.
    SExecutable m a =>
    [String] -> a -> SymbolicT m ()
    sName [String]
    ss (p -> SymbolicT m ()) -> p -> SymbolicT m ()
    forall a b. (a -> b) -> a -> b
    $ SBV a -> p
    k SBV a
    a
       sName []      k :: SBV a -> p
    k = (SBV a -> p) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName_ SBV a -> p
    k

    -- 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_        k :: (SBV a, SBV b) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    exists_  SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: 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
    $ \b :: SBV b
    b -> (SBV a, SBV b) -> p
    k (SBV a
    a, SBV b
    b)
      sName :: [String] -> ((SBV a, SBV b) -> p) -> SymbolicT m ()
    sName (s :: String
    s:ss :: [String]
    ss)  k :: (SBV a, SBV b) -> p
    k = String -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    exists String
    s SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> [String] -> (SBV b -> p) -> SymbolicT m ()
    forall (m :: * -> *) a.
    SExecutable m a =>
    [String] -> a -> SymbolicT m ()
    sName [String]
    ss ((SBV b -> p) -> SymbolicT m ()) -> (SBV b -> p) -> SymbolicT m ()
    forall a b. (a -> b) -> a -> b
    $ \b :: SBV b
    b -> (SBV a, SBV b) -> p
    k (SBV a
    a, SBV b
    b)
      sName []      k :: (SBV a, SBV b) -> p
    k = ((SBV a, SBV b) -> p) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName_ (SBV a, SBV b) -> p
    k

    -- 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_       k :: (SBV a, SBV b, SBV c) -> p
    k  = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    exists_  SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: 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
    $ \b :: SBV b
    b c :: SBV c
    c -> (SBV a, SBV b, SBV c) -> p
    k (SBV a
    a, SBV b
    b, SBV c
    c)
      sName :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m ()
    sName (s :: String
    s:ss :: [String]
    ss) k :: (SBV a, SBV b, SBV c) -> p
    k  = String -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    exists String
    s SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> [String] -> (SBV b -> SBV c -> p) -> SymbolicT m ()
    forall (m :: * -> *) a.
    SExecutable m a =>
    [String] -> a -> SymbolicT m ()
    sName [String]
    ss ((SBV b -> SBV c -> p) -> SymbolicT m ())
    -> (SBV b -> SBV c -> p) -> SymbolicT m ()
    forall a b. (a -> b) -> a -> b
    $ \b :: SBV b
    b c :: SBV c
    c -> (SBV a, SBV b, SBV c) -> p
    k (SBV a
    a, SBV b
    b, SBV c
    c)
      sName []     k :: (SBV a, SBV b, SBV c) -> p
    k  = ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName_ (SBV a, SBV b, SBV c) -> p
    k

    -- 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_        k :: (SBV a, SBV b, SBV c, SBV d) -> p
    k = SymbolicT m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    exists_  SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: 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
    $ \b :: SBV b
    b c :: SBV c
    c d :: 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)
      sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m ()
    sName (s :: String
    s:ss :: [String]
    ss)  k :: (SBV a, SBV b, SBV c, SBV d) -> p
    k = String -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    exists String
    s SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> [String] -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m ()
    forall (m :: * -> *) a.
    SExecutable m a =>
    [String] -> a -> SymbolicT m ()
    sName [String]
    ss ((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
    $ \b :: SBV b
    b c :: SBV c
    c d :: 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)
      sName []      k :: (SBV a, SBV b, SBV c, SBV d) -> p
    k = ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName_ (SBV a, SBV b, SBV c, SBV d) -> p
    k

    -- 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_        k :: (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)
    exists_  SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: 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
    $ \b :: SBV b
    b c :: SBV c
    c d :: SBV d
    d e :: 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)
      sName :: [String]
    -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m ()
    sName (s :: String
    s:ss :: [String]
    ss)  k :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
    k = String -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    exists String
    s SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> [String]
    -> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m ()
    forall (m :: * -> *) a.
    SExecutable m a =>
    [String] -> a -> SymbolicT m ()
    sName [String]
    ss ((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
    $ \b :: SBV b
    b c :: SBV c
    c d :: SBV d
    d e :: 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)
      sName []      k :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
    k = ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    sName_ (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
    k

    -- 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_        k :: (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)
    exists_  SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: 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
    $ \b :: SBV b
    b c :: SBV c
    c d :: SBV d
    d e :: SBV e
    e f :: 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)
      sName :: [String]
    -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
    -> SymbolicT m ()
    sName (s :: String
    s:ss :: [String]
    ss)  k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
    k = String -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    exists String
    s SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> [String]
    -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
    -> SymbolicT m ()
    forall (m :: * -> *) a.
    SExecutable m a =>
    [String] -> a -> SymbolicT m ()
    sName [String]
    ss ((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
    $ \b :: SBV b
    b c :: SBV c
    c d :: SBV d
    d e :: SBV e
    e f :: 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)
      sName []      k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
    k = ((SBV 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 a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
    k

    -- 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_        k :: (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)
    exists_  SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: 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
    $ \b :: SBV b
    b c :: SBV c
    c d :: SBV d
    d e :: SBV e
    e f :: SBV f
    f g :: 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)
      sName :: [String]
    -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
    -> SymbolicT m ()
    sName (s :: String
    s:ss :: [String]
    ss)  k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
    k = String -> SymbolicT m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    exists String
    s SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a :: SBV a
    a -> [String]
    -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
    -> SymbolicT m ()
    forall (m :: * -> *) a.
    SExecutable m a =>
    [String] -> a -> SymbolicT m ()
    sName [String]
    ss ((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
    $ \b :: SBV b
    b c :: SBV c
    c d :: SBV d
    d e :: SBV e
    e f :: SBV f
    f g :: 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)
      sName []      k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
    k = ((SBV 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 a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
    k

    {-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}