    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Client.BaseIO
    -- Copyright : (c) Brian Schroeder
    --                 Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Monomorphized versions of functions for simplified client use via
    -- @Data.SBV@, where we restrict the underlying monad to be IO.
    -----------------------------------------------------------------------------

    {-# LANGUAGE DataKinds            #-}
    {-# LANGUAGE DefaultSignatures    #-}
    {-# LANGUAGE FlexibleContexts     #-}
    {-# LANGUAGE FlexibleInstances    #-}
    {-# LANGUAGE TypeFamilies         #-}
    {-# LANGUAGE TypeOperators        #-}
    {-# LANGUAGE UndecidableInstances #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Client.BaseIO where

    import Data.SBV.Core.Data      (HasKind, Kind, Outputtable, Penalty, SymArray,
                                    SymVal, SBool, SBV, SChar, SDouble, SFloat,
                                    SInt8, SInt16, SInt32, SInt64, SInteger, SList,
                                    SReal, SString, SV, SWord8, SWord16, SWord32,
                                    SWord64, SEither, SMaybe, SSet)
    import Data.SBV.Core.Sized     (SInt, SWord, IntN, WordN, IsNonZero)
    import Data.SBV.Core.Model     (Metric(..), SymTuple)
    import Data.SBV.Core.Symbolic  (Objective, OptimizeStyle, Quantifier, Result,
                                    Symbolic, SBVRunMode, SMTConfig, SVal)
    import Data.SBV.Control.Types  (SMTOption)
    import Data.SBV.Provers.Prover (Provable, SExecutable, ThmResult)
    import Data.SBV.SMT.SMT        (AllSatResult, SafeResult, SatResult,
                                    OptimizeResult)

    import GHC.TypeLits
    import Data.Kind

    import Data.Int
    import Data.Word

    import qualified Data.SBV.Core.Data      as Trans
    import qualified Data.SBV.Core.Sized     as Trans
    import qualified Data.SBV.Core.Model     as Trans
    import qualified Data.SBV.Core.Symbolic  as Trans
    import qualified Data.SBV.Provers.Prover as Trans

    -- Data.SBV.Provers.Prover:

    -- | Turns a value into a universally quantified predicate, internally naming the inputs.
    -- In this case the sbv library will use names of the form @s1, s2@, etc. to name these variables
    -- Example:
    --
    -- >  forAll_ $ \(x::SWord8) y -> x `shiftL` 2 .== y
    --
    -- is a predicate with two arguments, captured using an ordinary Haskell function. Internally,
    -- @x@ will be named @s0@ and @y@ will be named @s1@.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.forAll_'
    forAll_ :: Provable a => a -> Symbolic SBool
    forAll_ :: a -> Symbolic SBool
    forAll_ = a -> Symbolic SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    Trans.forAll_

    -- | Turns a value into a predicate, allowing users to provide names for the inputs.
    -- If the user does not provide enough number of names for the variables, the remaining ones
    -- will be internally generated. Note that the names are only used for printing models and has no
    -- other significance; in particular, we do not check that they are unique. Example:
    --
    -- >  forAll ["x", "y"] $ \(x::SWord8) y -> x `shiftL` 2 .== y
    --
    -- This is the same as above, except the variables will be named @x@ and @y@ respectively,
    -- simplifying the counter-examples when they are printed.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.forAll'
    forAll :: Provable a => [String] -> a -> Symbolic SBool
    forAll :: [String] -> a -> Symbolic SBool
    forAll = [String] -> a -> Symbolic SBool
    forall (m :: * -> *) a.
    MProvable m a =>
    [String] -> a -> SymbolicT m SBool
    Trans.forAll

    -- | Turns a value into an existentially quantified predicate. (Indeed, 'exists' would have been
    -- a better choice here for the name, but alas it's already taken.)
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.forSome_'
    forSome_ :: Provable a => a -> Symbolic SBool
    forSome_ :: a -> Symbolic SBool
    forSome_ = a -> Symbolic SBool
    forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
    Trans.forSome_

    -- | Version of 'forSome' that allows user defined names.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.forSome'
    forSome :: Provable a => [String] -> a -> Symbolic SBool
    forSome :: [String] -> a -> Symbolic SBool
    forSome = [String] -> a -> Symbolic SBool
    forall (m :: * -> *) a.
    MProvable m a =>
    [String] -> a -> SymbolicT m SBool
    Trans.forSome

    -- | Prove a predicate, using the default solver.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.prove'
    prove :: Provable a => a -> IO ThmResult
    prove :: a -> IO ThmResult
    prove = a -> IO ThmResult
    forall (m :: * -> *) a. MProvable m a => a -> m ThmResult
    Trans.prove

    -- | Prove the predicate using the given SMT-solver.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.proveWith'
    proveWith :: Provable a => SMTConfig -> a -> IO ThmResult
    proveWith :: SMTConfig -> a -> IO ThmResult
    proveWith = SMTConfig -> a -> IO ThmResult
    forall (m :: * -> *) a.
    MProvable m a =>
    SMTConfig -> a -> m ThmResult
    Trans.proveWith

    -- | Find a satisfying assignment for a predicate, using the default solver.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sat'
    sat :: Provable a => a -> IO SatResult
    sat :: a -> IO SatResult
    sat = a -> IO SatResult
    forall (m :: * -> *) a. MProvable m a => a -> m SatResult
    Trans.sat

    -- | Find a satisfying assignment using the given SMT-solver.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.satWith'
    satWith :: Provable a => SMTConfig -> a -> IO SatResult
    satWith :: SMTConfig -> a -> IO SatResult
    satWith = SMTConfig -> a -> IO SatResult
    forall (m :: * -> *) a.
    MProvable m a =>
    SMTConfig -> a -> m SatResult
    Trans.satWith

    -- | Find all satisfying assignments, using the default solver.
    -- Equivalent to @'allSatWith' 'Data.SBV.defaultSMTCfg'@. See 'allSatWith' for details.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.allSat'
    allSat :: Provable a => a -> IO AllSatResult
    allSat :: a -> IO AllSatResult
    allSat = a -> IO AllSatResult
    forall (m :: * -> *) a. MProvable m a => a -> m AllSatResult
    Trans.allSat

    -- | Return all satisfying assignments for a predicate.
    -- Note that this call will block until all satisfying assignments are found. If you have a problem
    -- with infinitely many satisfying models (consider 'SInteger') or a very large number of them, you
    -- might have to wait for a long time. To avoid such cases, use the 'Data.SBV.Core.Symbolic.allSatMaxModelCount'
    -- parameter in the configuration.
    --
    -- NB. Uninterpreted constant/function values and counter-examples for array values are ignored for
    -- the purposes of 'allSat'. That is, only the satisfying assignments modulo uninterpreted functions and
    -- array inputs will be returned. This is due to the limitation of not having a robust means of getting a
    -- function counter-example back from the SMT solver.
    --  Find all satisfying assignments using the given SMT-solver
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.allSatWith'
    allSatWith :: Provable a => SMTConfig -> a -> IO AllSatResult
    allSatWith :: SMTConfig -> a -> IO AllSatResult
    allSatWith = SMTConfig -> a -> IO AllSatResult
    forall (m :: * -> *) a.
    MProvable m a =>
    SMTConfig -> a -> m AllSatResult
    Trans.allSatWith

    -- | Optimize a given collection of `Objective`s.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.optimize'
    optimize :: Provable a => OptimizeStyle -> a -> IO OptimizeResult
    optimize :: OptimizeStyle -> a -> IO OptimizeResult
    optimize = OptimizeStyle -> a -> IO OptimizeResult
    forall (m :: * -> *) a.
    MProvable m a =>
    OptimizeStyle -> a -> m OptimizeResult
    Trans.optimize

    -- | Optimizes the objectives using the given SMT-solver.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.optimizeWith'
    optimizeWith :: Provable a => SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult
    optimizeWith :: SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult
    optimizeWith = SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult
    forall (m :: * -> *) a.
    MProvable m a =>
    SMTConfig -> OptimizeStyle -> a -> m OptimizeResult
    Trans.optimizeWith

    -- | Check if the constraints given are consistent, using the default solver.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.isVacuous'
    isVacuous :: Provable a => a -> IO Bool
    isVacuous :: a -> IO Bool
    isVacuous = a -> IO Bool
    forall (m :: * -> *) a. MProvable m a => a -> m Bool
    Trans.isVacuous

    -- | Determine if the constraints are vacuous using the given SMT-solver.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.isVacuousWith'
    isVacuousWith :: Provable a => SMTConfig -> a -> IO Bool
    isVacuousWith :: SMTConfig -> a -> IO Bool
    isVacuousWith = SMTConfig -> a -> IO Bool
    forall (m :: * -> *) a. MProvable m a => SMTConfig -> a -> m Bool
    Trans.isVacuousWith

    -- | Checks theoremhood using the default solver.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.isTheorem'
    isTheorem :: Provable a => a -> IO Bool
    isTheorem :: a -> IO Bool
    isTheorem = a -> IO Bool
    forall (m :: * -> *) a. MProvable m a => a -> m Bool
    Trans.isTheorem

    -- | Check whether a given property is a theorem.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.isTheoremWith'
    isTheoremWith :: Provable a => SMTConfig -> a -> IO Bool
    isTheoremWith :: SMTConfig -> a -> IO Bool
    isTheoremWith = SMTConfig -> a -> IO Bool
    forall (m :: * -> *) a. MProvable m a => SMTConfig -> a -> m Bool
    Trans.isTheoremWith

    -- | Checks satisfiability using the default solver.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.isSatisfiable'
    isSatisfiable :: Provable a => a -> IO Bool
    isSatisfiable :: a -> IO Bool
    isSatisfiable = a -> IO Bool
    forall (m :: * -> *) a. MProvable m a => a -> m Bool
    Trans.isSatisfiable

    -- | Check whether a given property is satisfiable.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.isSatisfiableWith'
    isSatisfiableWith :: Provable a => SMTConfig -> a -> IO Bool
    isSatisfiableWith :: SMTConfig -> a -> IO Bool
    isSatisfiableWith = SMTConfig -> a -> IO Bool
    forall (m :: * -> *) a. MProvable m a => SMTConfig -> a -> m Bool
    Trans.isSatisfiableWith

    -- | Run an arbitrary symbolic computation, equivalent to @'runSMTWith' 'Data.SBV.defaultSMTCfg'@
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.runSMT'
    runSMT :: Symbolic a -> IO a
    runSMT :: Symbolic a -> IO a
    runSMT = Symbolic a -> IO a
    forall (m :: * -> *) a. MonadIO m => SymbolicT m a -> m a
    Trans.runSMT

    -- | Runs an arbitrary symbolic computation, exposed to the user in SAT mode
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.runSMTWith'
    runSMTWith :: SMTConfig -> Symbolic a -> IO a
    runSMTWith :: SMTConfig -> Symbolic a -> IO a
    runSMTWith = SMTConfig -> Symbolic a -> IO a
    forall (m :: * -> *) a.
    MonadIO m =>
    SMTConfig -> SymbolicT m a -> m a
    Trans.runSMTWith

    -- | NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sName_'
    sName_ :: SExecutable IO a => a -> Symbolic ()
    sName_ :: a -> Symbolic ()
    sName_ = a -> Symbolic ()
    forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
    Trans.sName_

    -- | NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sName'
    sName :: SExecutable IO a => [String] -> a -> Symbolic ()
    sName :: [String] -> a -> Symbolic ()
    sName = [String] -> a -> Symbolic ()
    forall (m :: * -> *) a.
    SExecutable m a =>
    [String] -> a -> SymbolicT m ()
    Trans.sName

    -- | Check safety using the default solver.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.safe'
    safe :: SExecutable IO a => a -> IO [SafeResult]
    safe :: a -> IO [SafeResult]
    safe = a -> IO [SafeResult]
    forall (m :: * -> *) a. SExecutable m a => a -> m [SafeResult]
    Trans.safe

    -- | Check if any of the 'Data.SBV.sAssert' calls can be violated.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.safeWith'
    safeWith :: SExecutable IO a => SMTConfig -> a -> IO [SafeResult]
    safeWith :: SMTConfig -> a -> IO [SafeResult]
    safeWith = SMTConfig -> a -> IO [SafeResult]
    forall (m :: * -> *) a.
    SExecutable m a =>
    SMTConfig -> a -> m [SafeResult]
    Trans.safeWith

    -- Data.SBV.Core.Data:

    -- | Create a symbolic variable.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.mkSymSBV'
    mkSymSBV :: Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a)
    mkSymSBV :: Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a)
    mkSymSBV = Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a)
    forall a (m :: * -> *).
    MonadSymbolic m =>
    Maybe Quantifier -> Kind -> Maybe String -> m (SBV a)
    Trans.mkSymSBV

    -- | Convert a symbolic value to an SV, inside the Symbolic monad
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sbvToSymSV'
    sbvToSymSV :: SBV a -> Symbolic SV
    sbvToSymSV :: SBV a -> Symbolic SV
    sbvToSymSV = SBV a -> Symbolic SV
    forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
    Trans.sbvToSymSV

    -- | Mark an interim result as an output. Useful when constructing Symbolic programs
    -- that return multiple values, or when the result is programmatically computed.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.output'
    output :: Outputtable a => a -> Symbolic a
    output :: a -> Symbolic a
    output = a -> Symbolic a
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    Trans.output

    -- | Create a user named input (universal)
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.forall'
    forall :: SymVal a => String -> Symbolic (SBV a)
    forall :: String -> Symbolic (SBV a)
    forall = String -> Symbolic (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    Trans.forall

    -- | Create an automatically named input
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.forall_'
    forall_ :: SymVal a => Symbolic (SBV a)
    forall_ :: Symbolic (SBV a)
    forall_ = Symbolic (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    Trans.forall_

    -- | Get a bunch of new words
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.mkForallVars'
    mkForallVars :: SymVal a => Int -> Symbolic [SBV a]
    mkForallVars :: Int -> Symbolic [SBV a]
    mkForallVars = Int -> Symbolic [SBV a]
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    Int -> m [SBV a]
    Trans.mkForallVars

    -- | Create an existential variable
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.exists'
    exists :: SymVal a => String -> Symbolic (SBV a)
    exists :: String -> Symbolic (SBV a)
    exists = String -> Symbolic (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    Trans.exists

    -- | Create an automatically named existential variable
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.exists_'
    exists_ :: SymVal a => Symbolic (SBV a)
    exists_ :: Symbolic (SBV a)
    exists_ = Symbolic (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    Trans.exists_

    -- | Create a bunch of existentials
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.mkExistVars'
    mkExistVars :: SymVal a => Int -> Symbolic [SBV a]
    mkExistVars :: Int -> Symbolic [SBV a]
    mkExistVars = Int -> Symbolic [SBV a]
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    Int -> m [SBV a]
    Trans.mkExistVars

    -- | Create a free variable, universal in a proof, existential in sat
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.free'
    free :: SymVal a => String -> Symbolic (SBV a)
    free :: String -> Symbolic (SBV a)
    free = String -> Symbolic (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    Trans.free

    -- | Create an unnamed free variable, universal in proof, existential in sat
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.free_'
    free_ :: SymVal a => Symbolic (SBV a)
    free_ :: Symbolic (SBV a)
    free_ = Symbolic (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    Trans.free_

    -- | Create a bunch of free vars
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.mkFreeVars'
    mkFreeVars :: SymVal a => Int -> Symbolic [SBV a]
    mkFreeVars :: Int -> Symbolic [SBV a]
    mkFreeVars = Int -> Symbolic [SBV a]
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    Int -> m [SBV a]
    Trans.mkFreeVars

    -- | Similar to free; Just a more convenient name
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.symbolic'
    symbolic :: SymVal a => String -> Symbolic (SBV a)
    symbolic :: String -> Symbolic (SBV a)
    symbolic = String -> Symbolic (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    Trans.symbolic

    -- | Similar to mkFreeVars; but automatically gives names based on the strings
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.symbolics'
    symbolics :: SymVal a => [String] -> Symbolic [SBV a]
    symbolics :: [String] -> Symbolic [SBV a]
    symbolics = [String] -> Symbolic [SBV a]
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    [String] -> m [SBV a]
    Trans.symbolics

    -- | One stop allocator
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.mkSymVal'
    mkSymVal :: SymVal a => Maybe Quantifier -> Maybe String -> Symbolic (SBV a)
    mkSymVal :: Maybe Quantifier -> Maybe String -> Symbolic (SBV a)
    mkSymVal = Maybe Quantifier -> Maybe String -> Symbolic (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    Maybe Quantifier -> Maybe String -> m (SBV a)
    Trans.mkSymVal

    -- | Create a new anonymous array, possibly with a default initial value.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.newArray_'
    newArray_ :: (SymArray array, HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (array a b)
    newArray_ :: Maybe (SBV b) -> Symbolic (array a b)
    newArray_ = Maybe (SBV b) -> Symbolic (array a b)
    forall (array :: * -> * -> *) (m :: * -> *) a b.
    (SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
    Maybe (SBV b) -> m (array a b)
    Trans.newArray_

    -- | Create a named new array, possibly with a default initial value.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.newArray'
    newArray :: (SymArray array, HasKind a, HasKind b) => String -> Maybe (SBV b) -> Symbolic (array a b)
    newArray :: String -> Maybe (SBV b) -> Symbolic (array a b)
    newArray = String -> Maybe (SBV b) -> Symbolic (array a b)
    forall (array :: * -> * -> *) (m :: * -> *) a b.
    (SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
    String -> Maybe (SBV b) -> m (array a b)
    Trans.newArray

    -- Data.SBV.Core.Model:

    -- | Generically make a symbolic var
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.genMkSymVar'
    genMkSymVar :: Kind -> Maybe Quantifier -> Maybe String -> Symbolic (SBV a)
    genMkSymVar :: Kind -> Maybe Quantifier -> Maybe String -> Symbolic (SBV a)
    genMkSymVar = Kind -> Maybe Quantifier -> Maybe String -> Symbolic (SBV a)
    forall (m :: * -> *) a.
    MonadSymbolic m =>
    Kind -> Maybe Quantifier -> Maybe String -> m (SBV a)
    Trans.genMkSymVar

    -- | Declare a named 'SBool'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sBool'
    sBool :: String -> Symbolic SBool
    sBool :: String -> Symbolic SBool
    sBool = String -> Symbolic SBool
    forall (m :: * -> *). MonadSymbolic m => String -> m SBool
    Trans.sBool

    -- | Declare an unnamed 'SBool'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sBool_'
    sBool_ :: Symbolic SBool
    sBool_ :: Symbolic SBool
    sBool_ = Symbolic SBool
    forall (m :: * -> *). MonadSymbolic m => m SBool
    Trans.sBool_

    -- | Declare a list of 'SBool's
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sBools'
    sBools :: [String] -> Symbolic [SBool]
    sBools :: [String] -> Symbolic [SBool]
    sBools = [String] -> Symbolic [SBool]
    forall (m :: * -> *). MonadSymbolic m => [String] -> m [SBool]
    Trans.sBools

    -- | Declare a named 'SWord8'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sWord8'
    sWord8 :: String -> Symbolic SWord8
    sWord8 :: String -> Symbolic SWord8
    sWord8 = String -> Symbolic SWord8
    forall (m :: * -> *). MonadSymbolic m => String -> m SWord8
    Trans.sWord8

    -- | Declare an unnamed 'SWord8'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sWord8_'
    sWord8_ :: Symbolic SWord8
    sWord8_ :: Symbolic SWord8
    sWord8_ = Symbolic SWord8
    forall (m :: * -> *). MonadSymbolic m => m SWord8
    Trans.sWord8_

    -- | Declare a list of 'SWord8's
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sWord8s'
    sWord8s :: [String] -> Symbolic [SWord8]
    sWord8s :: [String] -> Symbolic [SWord8]
    sWord8s = [String] -> Symbolic [SWord8]
    forall (m :: * -> *). MonadSymbolic m => [String] -> m [SWord8]
    Trans.sWord8s

    -- | Declare a named 'SWord16'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sWord16'
    sWord16 :: String -> Symbolic SWord16
    sWord16 :: String -> Symbolic SWord16
    sWord16 = String -> Symbolic SWord16
    forall (m :: * -> *). MonadSymbolic m => String -> m SWord16
    Trans.sWord16

    -- | Declare an unnamed 'SWord16'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sWord16_'
    sWord16_ :: Symbolic SWord16
    sWord16_ :: Symbolic SWord16
    sWord16_ = Symbolic SWord16
    forall (m :: * -> *). MonadSymbolic m => m SWord16
    Trans.sWord16_

    -- | Declare a list of 'SWord16's
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sWord16s'
    sWord16s :: [String] -> Symbolic [SWord16]
    sWord16s :: [String] -> Symbolic [SWord16]
    sWord16s = [String] -> Symbolic [SWord16]
    forall (m :: * -> *). MonadSymbolic m => [String] -> m [SWord16]
    Trans.sWord16s

    -- | Declare a named 'SWord32'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sWord32'
    sWord32 :: String -> Symbolic SWord32
    sWord32 :: String -> Symbolic SWord32
    sWord32 = String -> Symbolic SWord32
    forall (m :: * -> *). MonadSymbolic m => String -> m SWord32
    Trans.sWord32

    -- | Declare an unamed 'SWord32'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sWord32_'
    sWord32_ :: Symbolic SWord32
    sWord32_ :: Symbolic SWord32
    sWord32_ = Symbolic SWord32
    forall (m :: * -> *). MonadSymbolic m => m SWord32
    Trans.sWord32_

    -- | Declare a list of 'SWord32's
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sWord32s'
    sWord32s :: [String] -> Symbolic [SWord32]
    sWord32s :: [String] -> Symbolic [SWord32]
    sWord32s = [String] -> Symbolic [SWord32]
    forall (m :: * -> *). MonadSymbolic m => [String] -> m [SWord32]
    Trans.sWord32s

    -- | Declare a named 'SWord64'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sWord64'
    sWord64 :: String -> Symbolic SWord64
    sWord64 :: String -> Symbolic SWord64
    sWord64 = String -> Symbolic SWord64
    forall (m :: * -> *). MonadSymbolic m => String -> m SWord64
    Trans.sWord64

    -- | Declare an unnamed 'SWord64'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sWord64_'
    sWord64_ :: Symbolic SWord64
    sWord64_ :: Symbolic SWord64
    sWord64_ = Symbolic SWord64
    forall (m :: * -> *). MonadSymbolic m => m SWord64
    Trans.sWord64_

    -- | Declare a list of 'SWord64's
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sWord64s'
    sWord64s :: [String] -> Symbolic [SWord64]
    sWord64s :: [String] -> Symbolic [SWord64]
    sWord64s = [String] -> Symbolic [SWord64]
    forall (m :: * -> *). MonadSymbolic m => [String] -> m [SWord64]
    Trans.sWord64s

    -- | Declare a named 'SWord'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sWord'
    sWord :: (KnownNat n, IsNonZero n) => String -> Symbolic (SWord n)
    sWord :: String -> Symbolic (SWord n)
    sWord = String -> Symbolic (SWord n)
    forall (n :: Nat) (m :: * -> *).
    (KnownNat n, IsNonZero n, MonadSymbolic m) =>
    String -> m (SWord n)
    Trans.sWord

    -- | Declare an unnamed 'SWord'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sWord_'
    sWord_ :: (KnownNat n, IsNonZero n) => Symbolic (SWord n)
    sWord_ :: Symbolic (SWord n)
    sWord_ = Symbolic (SWord n)
    forall (n :: Nat) (m :: * -> *).
    (KnownNat n, IsNonZero n, MonadSymbolic m) =>
    m (SWord n)
    Trans.sWord_

    -- | Declare a list of 'SWord8's
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sWords'
    sWords :: (KnownNat n, IsNonZero n) => [String] -> Symbolic [SWord n]
    sWords :: [String] -> Symbolic [SWord n]
    sWords = [String] -> Symbolic [SWord n]
    forall (n :: Nat) (m :: * -> *).
    (KnownNat n, IsNonZero n, MonadSymbolic m) =>
    [String] -> m [SWord n]
    Trans.sWords

    -- | Declare a named 'SInt8'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sInt8'
    sInt8 :: String -> Symbolic SInt8
    sInt8 :: String -> Symbolic SInt8
    sInt8 = String -> Symbolic SInt8
    forall (m :: * -> *). MonadSymbolic m => String -> m SInt8
    Trans.sInt8

    -- | Declare an unnamed 'SInt8'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sInt8_'
    sInt8_ :: Symbolic SInt8
    sInt8_ :: Symbolic SInt8
    sInt8_ = Symbolic SInt8
    forall (m :: * -> *). MonadSymbolic m => m SInt8
    Trans.sInt8_

    -- | Declare a list of 'SInt8's
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sInt8s'
    sInt8s :: [String] -> Symbolic [SInt8]
    sInt8s :: [String] -> Symbolic [SInt8]
    sInt8s = [String] -> Symbolic [SInt8]
    forall (m :: * -> *). MonadSymbolic m => [String] -> m [SInt8]
    Trans.sInt8s

    -- | Declare a named 'SInt16'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sInt16'
    sInt16 :: String -> Symbolic SInt16
    sInt16 :: String -> Symbolic SInt16
    sInt16 = String -> Symbolic SInt16
    forall (m :: * -> *). MonadSymbolic m => String -> m SInt16
    Trans.sInt16

    -- | Declare an unnamed 'SInt16'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sInt16_'
    sInt16_ :: Symbolic SInt16
    sInt16_ :: Symbolic SInt16
    sInt16_ = Symbolic SInt16
    forall (m :: * -> *). MonadSymbolic m => m SInt16
    Trans.sInt16_

    -- | Declare a list of 'SInt16's
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sInt16s'
    sInt16s :: [String] -> Symbolic [SInt16]
    sInt16s :: [String] -> Symbolic [SInt16]
    sInt16s = [String] -> Symbolic [SInt16]
    forall (m :: * -> *). MonadSymbolic m => [String] -> m [SInt16]
    Trans.sInt16s

    -- | Declare a named 'SInt32'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sInt32'
    sInt32 :: String -> Symbolic SInt32
    sInt32 :: String -> Symbolic SInt32
    sInt32 = String -> Symbolic SInt32
    forall (m :: * -> *). MonadSymbolic m => String -> m SInt32
    Trans.sInt32

    -- | Declare an unnamed 'SInt32'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sInt32_'
    sInt32_ :: Symbolic SInt32
    sInt32_ :: Symbolic SInt32
    sInt32_ = Symbolic SInt32
    forall (m :: * -> *). MonadSymbolic m => m SInt32
    Trans.sInt32_

    -- | Declare a list of 'SInt32's
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sInt32s'
    sInt32s :: [String] -> Symbolic [SInt32]
    sInt32s :: [String] -> Symbolic [SInt32]
    sInt32s = [String] -> Symbolic [SInt32]
    forall (m :: * -> *). MonadSymbolic m => [String] -> m [SInt32]
    Trans.sInt32s

    -- | Declare a named 'SInt64'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sInt64'
    sInt64 :: String -> Symbolic SInt64
    sInt64 :: String -> Symbolic SInt64
    sInt64 = String -> Symbolic SInt64
    forall (m :: * -> *). MonadSymbolic m => String -> m SInt64
    Trans.sInt64

    -- | Declare an unnamed 'SInt64'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sInt64_'
    sInt64_ :: Symbolic SInt64
    sInt64_ :: Symbolic SInt64
    sInt64_ = Symbolic SInt64
    forall (m :: * -> *). MonadSymbolic m => m SInt64
    Trans.sInt64_

    -- | Declare a list of 'SInt64's
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sInt64s'
    sInt64s :: [String] -> Symbolic [SInt64]
    sInt64s :: [String] -> Symbolic [SInt64]
    sInt64s = [String] -> Symbolic [SInt64]
    forall (m :: * -> *). MonadSymbolic m => [String] -> m [SInt64]
    Trans.sInt64s

    -- | Declare a named 'SInt'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sInt'
    sInt :: (KnownNat n, IsNonZero n) => String -> Symbolic (SInt n)
    sInt :: String -> Symbolic (SInt n)
    sInt = String -> Symbolic (SInt n)
    forall (n :: Nat) (m :: * -> *).
    (KnownNat n, IsNonZero n, MonadSymbolic m) =>
    String -> m (SInt n)
    Trans.sInt

    -- | Declare an unnamed 'SInt'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sInt_'
    sInt_ :: (KnownNat n, IsNonZero n) => Symbolic (SInt n)
    sInt_ :: Symbolic (SInt n)
    sInt_ = Symbolic (SInt n)
    forall (n :: Nat) (m :: * -> *).
    (KnownNat n, IsNonZero n, MonadSymbolic m) =>
    m (SInt n)
    Trans.sInt_

    -- | Declare a list of 'SInt's
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sInts'
    sInts :: (KnownNat n, IsNonZero n) => [String] -> Symbolic [SInt n]
    sInts :: [String] -> Symbolic [SInt n]
    sInts = [String] -> Symbolic [SInt n]
    forall (n :: Nat) (m :: * -> *).
    (KnownNat n, IsNonZero n, MonadSymbolic m) =>
    [String] -> m [SInt n]
    Trans.sInts

    -- | Declare a named 'SInteger'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sInteger'
    sInteger :: String -> Symbolic SInteger
    sInteger :: String -> Symbolic SInteger
    sInteger = String -> Symbolic SInteger
    forall (m :: * -> *). MonadSymbolic m => String -> m SInteger
    Trans.sInteger

    -- | Declare an unnamed 'SInteger'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sInteger_'
    sInteger_ :: Symbolic SInteger
    sInteger_ :: Symbolic SInteger
    sInteger_ = Symbolic SInteger
    forall (m :: * -> *). MonadSymbolic m => m SInteger
    Trans.sInteger_

    -- | Declare a list of 'SInteger's
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sIntegers'
    sIntegers :: [String] -> Symbolic [SInteger]
    sIntegers :: [String] -> Symbolic [SInteger]
    sIntegers = [String] -> Symbolic [SInteger]
    forall (m :: * -> *). MonadSymbolic m => [String] -> m [SInteger]
    Trans.sIntegers

    -- | Declare a named 'SReal'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sReal'
    sReal :: String -> Symbolic SReal
    sReal :: String -> Symbolic SReal
    sReal = String -> Symbolic SReal
    forall (m :: * -> *). MonadSymbolic m => String -> m SReal
    Trans.sReal

    -- | Declare an unnamed 'SReal'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sReal_'
    sReal_ :: Symbolic SReal
    sReal_ :: Symbolic SReal
    sReal_ = Symbolic SReal
    forall (m :: * -> *). MonadSymbolic m => m SReal
    Trans.sReal_

    -- | Declare a list of 'SReal's
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sReals'
    sReals :: [String] -> Symbolic [SReal]
    sReals :: [String] -> Symbolic [SReal]
    sReals = [String] -> Symbolic [SReal]
    forall (m :: * -> *). MonadSymbolic m => [String] -> m [SReal]
    Trans.sReals

    -- | Declare a named 'SFloat'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFloat'
    sFloat :: String -> Symbolic SFloat
    sFloat :: String -> Symbolic SFloat
    sFloat = String -> Symbolic SFloat
    forall (m :: * -> *). MonadSymbolic m => String -> m SFloat
    Trans.sFloat

    -- | Declare an unnamed 'SFloat'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFloat_'
    sFloat_ :: Symbolic SFloat
    sFloat_ :: Symbolic SFloat
    sFloat_ = Symbolic SFloat
    forall (m :: * -> *). MonadSymbolic m => m SFloat
    Trans.sFloat_

    -- | Declare a list of 'SFloat's
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFloats'
    sFloats :: [String] -> Symbolic [SFloat]
    sFloats :: [String] -> Symbolic [SFloat]
    sFloats = [String] -> Symbolic [SFloat]
    forall (m :: * -> *). MonadSymbolic m => [String] -> m [SFloat]
    Trans.sFloats

    -- | Declare a named 'SDouble'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sDouble'
    sDouble :: String -> Symbolic SDouble
    sDouble :: String -> Symbolic SDouble
    sDouble = String -> Symbolic SDouble
    forall (m :: * -> *). MonadSymbolic m => String -> m SDouble
    Trans.sDouble

    -- | Declare an unnamed 'SDouble'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sDouble_'
    sDouble_ :: Symbolic SDouble
    sDouble_ :: Symbolic SDouble
    sDouble_ = Symbolic SDouble
    forall (m :: * -> *). MonadSymbolic m => m SDouble
    Trans.sDouble_

    -- | Declare a list of 'SDouble's
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sDoubles'
    sDoubles :: [String] -> Symbolic [SDouble]
    sDoubles :: [String] -> Symbolic [SDouble]
    sDoubles = [String] -> Symbolic [SDouble]
    forall (m :: * -> *). MonadSymbolic m => [String] -> m [SDouble]
    Trans.sDoubles

    -- | Declare a named 'SChar'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sChar'
    sChar :: String -> Symbolic SChar
    sChar :: String -> Symbolic SChar
    sChar = String -> Symbolic SChar
    forall (m :: * -> *). MonadSymbolic m => String -> m SChar
    Trans.sChar

    -- | Declare an unnamed 'SChar'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sChar_'
    sChar_ :: Symbolic SChar
    sChar_ :: Symbolic SChar
    sChar_ = Symbolic SChar
    forall (m :: * -> *). MonadSymbolic m => m SChar
    Trans.sChar_

    -- | Declare a list of 'SChar's
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sChars'
    sChars :: [String] -> Symbolic [SChar]
    sChars :: [String] -> Symbolic [SChar]
    sChars = [String] -> Symbolic [SChar]
    forall (m :: * -> *). MonadSymbolic m => [String] -> m [SChar]
    Trans.sChars

    -- | Declare a named 'SString'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sString'
    sString :: String -> Symbolic SString
    sString :: String -> Symbolic SString
    sString = String -> Symbolic SString
    forall (m :: * -> *). MonadSymbolic m => String -> m SString
    Trans.sString

    -- | Declare an unnamed 'SString'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sString_'
    sString_ :: Symbolic SString
    sString_ :: Symbolic SString
    sString_ = Symbolic SString
    forall (m :: * -> *). MonadSymbolic m => m SString
    Trans.sString_

    -- | Declare a list of 'SString's
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sStrings'
    sStrings :: [String] -> Symbolic [SString]
    sStrings :: [String] -> Symbolic [SString]
    sStrings = [String] -> Symbolic [SString]
    forall (m :: * -> *). MonadSymbolic m => [String] -> m [SString]
    Trans.sStrings

    -- | Declare a named 'SList'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sList'
    sList :: SymVal a => String -> Symbolic (SList a)
    sList :: String -> Symbolic (SList a)
    sList = String -> Symbolic (SList a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SList a)
    Trans.sList

    -- | Declare an unnamed 'SList'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sList_'
    sList_ :: SymVal a => Symbolic (SList a)
    sList_ :: Symbolic (SList a)
    sList_ = Symbolic (SList a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SList a)
    Trans.sList_

    -- | Declare a list of 'SList's
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sLists'
    sLists :: SymVal a => [String] -> Symbolic [SList a]
    sLists :: [String] -> Symbolic [SList a]
    sLists = [String] -> Symbolic [SList a]
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    [String] -> m [SList a]
    Trans.sLists

    -- | Declare a named tuple.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sTuple'
    sTuple :: (SymTuple tup, SymVal tup) => String -> Symbolic (SBV tup)
    sTuple :: String -> Symbolic (SBV tup)
    sTuple = String -> Symbolic (SBV tup)
    forall tup (m :: * -> *).
    (SymTuple tup, SymVal tup, MonadSymbolic m) =>
    String -> m (SBV tup)
    Trans.sTuple

    -- | Declare an unnamed tuple.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sTuple_'
    sTuple_ :: (SymTuple tup, SymVal tup) => Symbolic (SBV tup)
    sTuple_ :: Symbolic (SBV tup)
    sTuple_ = Symbolic (SBV tup)
    forall tup (m :: * -> *).
    (SymTuple tup, SymVal tup, MonadSymbolic m) =>
    m (SBV tup)
    Trans.sTuple_

    -- | Declare a list of tuples.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sTuples'
    sTuples :: (SymTuple tup, SymVal tup) => [String] -> Symbolic [SBV tup]
    sTuples :: [String] -> Symbolic [SBV tup]
    sTuples = [String] -> Symbolic [SBV tup]
    forall tup (m :: * -> *).
    (SymTuple tup, SymVal tup, MonadSymbolic m) =>
    [String] -> m [SBV tup]
    Trans.sTuples

    -- | Declare a named 'Data.SBV.SEither'.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sEither'
    sEither :: (SymVal a, SymVal b) => String -> Symbolic (SEither a b)
    sEither :: String -> Symbolic (SEither a b)
    sEither = String -> Symbolic (SEither a b)
    forall a b (m :: * -> *).
    (SymVal a, SymVal b, MonadSymbolic m) =>
    String -> m (SEither a b)
    Trans.sEither

    -- | Declare an unnamed 'Data.SBV.SEither'.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sEither_'
    sEither_ :: (SymVal a, SymVal b) => Symbolic (SEither a b)
    sEither_ :: Symbolic (SEither a b)
    sEither_ = Symbolic (SEither a b)
    forall a b (m :: * -> *).
    (SymVal a, SymVal b, MonadSymbolic m) =>
    m (SEither a b)
    Trans.sEither_

    -- | Declare a list of 'Data.SBV.SEither' values.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sEithers'
    sEithers :: (SymVal a, SymVal b) => [String] -> Symbolic [SEither a b]
    sEithers :: [String] -> Symbolic [SEither a b]
    sEithers = [String] -> Symbolic [SEither a b]
    forall a b (m :: * -> *).
    (SymVal a, SymVal b, MonadSymbolic m) =>
    [String] -> m [SEither a b]
    Trans.sEithers

    -- | Declare a named 'Data.SBV.SMaybe'.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sMaybe'
    sMaybe :: SymVal a => String -> Symbolic (SMaybe a)
    sMaybe :: String -> Symbolic (SMaybe a)
    sMaybe = String -> Symbolic (SMaybe a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SMaybe a)
    Trans.sMaybe

    -- | Declare an unnamed 'Data.SBV.SMaybe'.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sMaybe_'
    sMaybe_ :: SymVal a => Symbolic (SMaybe a)
    sMaybe_ :: Symbolic (SMaybe a)
    sMaybe_ = Symbolic (SMaybe a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SMaybe a)
    Trans.sMaybe_

    -- | Declare a list of 'Data.SBV.SMaybe' values.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sMaybes'
    sMaybes :: SymVal a => [String] -> Symbolic [SMaybe a]
    sMaybes :: [String] -> Symbolic [SMaybe a]
    sMaybes = [String] -> Symbolic [SMaybe a]
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    [String] -> m [SMaybe a]
    Trans.sMaybes

    -- | Declare a named 'Data.SBV.SSet'.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sSet'
    sSet :: (Ord a, SymVal a) => String -> Symbolic (SSet a)
    sSet :: String -> Symbolic (SSet a)
    sSet = String -> Symbolic (SSet a)
    forall a (m :: * -> *).
    (Ord a, SymVal a, MonadSymbolic m) =>
    String -> m (SSet a)
    Trans.sSet

    -- | Declare an unnamed 'Data.SBV.SSet'.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sSet_'
    sSet_ :: (Ord a, SymVal a) => Symbolic (SSet a)
    sSet_ :: Symbolic (SSet a)
    sSet_ = Symbolic (SSet a)
    forall a (m :: * -> *).
    (Ord a, SymVal a, MonadSymbolic m) =>
    m (SSet a)
    Trans.sSet_

    -- | Declare a list of 'Data.SBV.SSet' values.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sSets'
    sSets :: (Ord a, SymVal a) => [String] -> Symbolic [SSet a]
    sSets :: [String] -> Symbolic [SSet a]
    sSets = [String] -> Symbolic [SSet a]
    forall a (m :: * -> *).
    (Ord a, SymVal a, MonadSymbolic m) =>
    [String] -> m [SSet a]
    Trans.sSets

    -- | Form the symbolic conjunction of a given list of boolean conditions. Useful in expressing
    -- problems with constraints, like the following:
    --
    -- @
    --   sat $ do [x, y, z] <- sIntegers [\"x\", \"y\", \"z\"]
    --            solve [x .> 5, y + z .< x]
    -- @
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.solve'
    solve :: [SBool] -> Symbolic SBool
    solve :: [SBool] -> Symbolic SBool
    solve = [SBool] -> Symbolic SBool
    forall (m :: * -> *). MonadSymbolic m => [SBool] -> m SBool
    Trans.solve

    -- | Introduce a soft assertion, with an optional penalty
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.assertWithPenalty'
    assertWithPenalty :: String -> SBool -> Penalty -> Symbolic ()
    assertWithPenalty :: String -> SBool -> Penalty -> Symbolic ()
    assertWithPenalty = String -> SBool -> Penalty -> Symbolic ()
    forall (m :: * -> *).
    MonadSymbolic m =>
    String -> SBool -> Penalty -> m ()
    Trans.assertWithPenalty

    -- | Minimize a named metric
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.minimize'
    minimize :: Metric a => String -> SBV a -> Symbolic ()
    minimize :: String -> SBV a -> Symbolic ()
    minimize = String -> SBV a -> Symbolic ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    Trans.minimize

    -- | Maximize a named metric
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.maximize'
    maximize :: Metric a => String -> SBV a -> Symbolic ()
    maximize :: String -> SBV a -> Symbolic ()
    maximize = String -> SBV a -> Symbolic ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    Trans.maximize

    -- Data.SBV.Core.Symbolic:

    -- | Convert a symbolic value to an SV, inside the Symbolic monad
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.svToSymSV'
    svToSymSV :: SVal -> Symbolic SV
    svToSymSV :: SVal -> Symbolic SV
    svToSymSV = SVal -> Symbolic SV
    forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
    Trans.svToSymSV

    -- | Run a symbolic computation, and return a extra value paired up with the 'Result'
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.runSymbolic'
    runSymbolic :: SBVRunMode -> Symbolic a -> IO (a, Result)
    runSymbolic :: SBVRunMode -> Symbolic a -> IO (a, Result)
    runSymbolic = SBVRunMode -> Symbolic a -> IO (a, Result)
    forall (m :: * -> *) a.
    MonadIO m =>
    SBVRunMode -> SymbolicT m a -> m (a, Result)
    Trans.runSymbolic

    -- | Add a new option
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.addNewSMTOption'
    addNewSMTOption :: SMTOption -> Symbolic ()
    addNewSMTOption :: SMTOption -> Symbolic ()
    addNewSMTOption = SMTOption -> Symbolic ()
    forall (m :: * -> *). MonadSymbolic m => SMTOption -> m ()
    Trans.addNewSMTOption

    -- | Handling constraints
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.imposeConstraint'
    imposeConstraint :: Bool -> [(String, String)] -> SVal -> Symbolic ()
    imposeConstraint :: Bool -> [(String, String)] -> SVal -> Symbolic ()
    imposeConstraint = Bool -> [(String, String)] -> SVal -> Symbolic ()
    forall (m :: * -> *).
    MonadSymbolic m =>
    Bool -> [(String, String)] -> SVal -> m ()
    Trans.imposeConstraint

    -- | Add an optimization goal
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.addSValOptGoal'
    addSValOptGoal :: Objective SVal -> Symbolic ()
    addSValOptGoal :: Objective SVal -> Symbolic ()
    addSValOptGoal = Objective SVal -> Symbolic ()
    forall (m :: * -> *). MonadSymbolic m => Objective SVal -> m ()
    Trans.addSValOptGoal

    -- | Mark an interim result as an output. Useful when constructing Symbolic programs
    -- that return multiple values, or when the result is programmatically computed.
    --
    -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.outputSVal'
    outputSVal :: SVal -> Symbolic ()
    outputSVal :: SVal -> Symbolic ()
    outputSVal = SVal -> Symbolic ()
    forall (m :: * -> *). MonadSymbolic m => SVal -> m ()
    Trans.outputSVal

    -- | Capturing non-matching instances for better error messages, conversions from sized
    type FromSizedErr (arg :: Type) =     'Text "fromSized: Cannot convert from type: " ':<>: 'ShowType arg
                                    ':$$: 'Text "           Source type must be one of SInt N, SWord N, IntN N, WordN N"
                                    ':$$: 'Text "           where N is 8, 16, 32, or 64."

    -- | Capturing non-matching instances for better error messages, conversions to sized
    type ToSizedErr (arg :: Type) =      'Text "toSized: Cannot convert from type: " ':<>: 'ShowType arg
                                  ':$$: 'Text "          Source type must be one of Int8/16/32/64"
                                  ':$$: 'Text "                                  OR Word8/16/32/64"
                                  ':$$: 'Text "                                  OR their symbolic variants."

    -- | Capture the correspondence between sized and fixed-sized BVs
    type family FromSized (t :: Type) :: Type where
       FromSized (WordN  8) = Word8
       FromSized (WordN 16) = Word16
       FromSized (WordN 32) = Word32
       FromSized (WordN 64) = Word64
       FromSized (IntN   8) = Int8
       FromSized (IntN  16) = Int16
       FromSized (IntN  32) = Int32
       FromSized (IntN  64) = Int64
       FromSized (SWord  8) = SWord8
       FromSized (SWord 16) = SWord16
       FromSized (SWord 32) = SWord32
       FromSized (SWord 64) = SWord64
       FromSized (SInt   8) = SInt8
       FromSized (SInt  16) = SInt16
       FromSized (SInt  32) = SInt32
       FromSized (SInt  64) = SInt64

    type family FromSizedCstr (t :: Type) :: Constraint where
       FromSizedCstr (WordN  8) = ()
       FromSizedCstr (WordN 16) = ()
       FromSizedCstr (WordN 32) = ()
       FromSizedCstr (WordN 64) = ()
       FromSizedCstr (IntN   8) = ()
       FromSizedCstr (IntN  16) = ()
       FromSizedCstr (IntN  32) = ()
       FromSizedCstr (IntN  64) = ()
       FromSizedCstr (SWord  8) = ()
       FromSizedCstr (SWord 16) = ()
       FromSizedCstr (SWord 32) = ()
       FromSizedCstr (SWord 64) = ()
       FromSizedCstr (SInt   8) = ()
       FromSizedCstr (SInt  16) = ()
       FromSizedCstr (SInt  32) = ()
       FromSizedCstr (SInt  64) = ()
       FromSizedCstr arg        = TypeError (FromSizedErr arg)

    -- | Conversion from a sized BV to a fixed-sized bit-vector.
    class FromSizedBV a where
       -- | Convert a sized bit-vector to the corresponding fixed-sized bit-vector,
       -- for instance 'SWord 16' to 'SWord16'. See also 'toSized'.
       fromSized :: a -> FromSized a

       default fromSized :: (Num (FromSized a), Integral a) => a -> FromSized a
       fromSized = a -> FromSized a
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral

    instance {-# OVERLAPPING  #-} FromSizedBV (WordN   8)
    instance {-# OVERLAPPING  #-} FromSizedBV (WordN  16)
    instance {-# OVERLAPPING  #-} FromSizedBV (WordN  32)
    instance {-# OVERLAPPING  #-} FromSizedBV (WordN  64)
    instance {-# OVERLAPPING  #-} FromSizedBV (IntN    8)
    instance {-# OVERLAPPING  #-} FromSizedBV (IntN   16)
    instance {-# OVERLAPPING  #-} FromSizedBV (IntN   32)
    instance {-# OVERLAPPING  #-} FromSizedBV (IntN   64)
    instance {-# OVERLAPPING  #-} FromSizedBV (SWord   8) where fromSized :: SWord 8 -> FromSized (SWord 8)
    fromSized = SWord 8 -> FromSized (SWord 8)
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    Trans.sFromIntegral
    instance {-# OVERLAPPING  #-} FromSizedBV (SWord  16) where fromSized :: SWord 16 -> FromSized (SWord 16)
    fromSized = SWord 16 -> FromSized (SWord 16)
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    Trans.sFromIntegral
    instance {-# OVERLAPPING  #-} FromSizedBV (SWord  32) where fromSized :: SWord 32 -> FromSized (SWord 32)
    fromSized = SWord 32 -> FromSized (SWord 32)
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    Trans.sFromIntegral
    instance {-# OVERLAPPING  #-} FromSizedBV (SWord  64) where fromSized :: SWord 64 -> FromSized (SWord 64)
    fromSized = SWord 64 -> FromSized (SWord 64)
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    Trans.sFromIntegral
    instance {-# OVERLAPPING  #-} FromSizedBV (SInt    8) where fromSized :: SInt 8 -> FromSized (SInt 8)
    fromSized = SInt 8 -> FromSized (SInt 8)
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    Trans.sFromIntegral
    instance {-# OVERLAPPING  #-} FromSizedBV (SInt   16) where fromSized :: SInt 16 -> FromSized (SInt 16)
    fromSized = SInt 16 -> FromSized (SInt 16)
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    Trans.sFromIntegral
    instance {-# OVERLAPPING  #-} FromSizedBV (SInt   32) where fromSized :: SInt 32 -> FromSized (SInt 32)
    fromSized = SInt 32 -> FromSized (SInt 32)
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    Trans.sFromIntegral
    instance {-# OVERLAPPING  #-} FromSizedBV (SInt   64) where fromSized :: SInt 64 -> FromSized (SInt 64)
    fromSized = SInt 64 -> FromSized (SInt 64)
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    Trans.sFromIntegral
    instance {-# OVERLAPPABLE #-} FromSizedCstr arg => FromSizedBV arg where fromSized :: arg -> FromSized arg
    fromSized = String -> arg -> FromSized arg
    forall a. HasCallStack => String -> a
    error "unreachable"

    -- | Capture the correspondence between fixed-sized and sized BVs
    type family ToSized (t :: Type) :: Type where
       ToSized Word8   = WordN  8
       ToSized Word16  = WordN 16
       ToSized Word32  = WordN 32
       ToSized Word64  = WordN 64
       ToSized Int8    = IntN   8
       ToSized Int16   = IntN  16
       ToSized Int32   = IntN  32
       ToSized Int64   = IntN  64
       ToSized SWord8  = SWord  8
       ToSized SWord16 = SWord 16
       ToSized SWord32 = SWord 32
       ToSized SWord64 = SWord 64
       ToSized SInt8   = SInt   8
       ToSized SInt16  = SInt  16
       ToSized SInt32  = SInt  32
       ToSized SInt64  = SInt  64

    type family ToSizedCstr (t :: Type) :: Constraint where
       ToSizedCstr Word8   = ()
       ToSizedCstr Word16  = ()
       ToSizedCstr Word32  = ()
       ToSizedCstr Word64  = ()
       ToSizedCstr Int8    = ()
       ToSizedCstr Int16   = ()
       ToSizedCstr Int32   = ()
       ToSizedCstr Int64   = ()
       ToSizedCstr SWord8  = ()
       ToSizedCstr SWord16 = ()
       ToSizedCstr SWord32 = ()
       ToSizedCstr SWord64 = ()
       ToSizedCstr SInt8   = ()
       ToSizedCstr SInt16  = ()
       ToSizedCstr SInt32  = ()
       ToSizedCstr SInt64  = ()
       ToSizedCstr arg     = TypeError (ToSizedErr arg)

    -- | Conversion from a fixed-sized BV to a sized bit-vector.
    class ToSizedBV a where
       -- | Convert a fixed-sized bit-vector to the corresponding sized bit-vector,
       -- for instance 'SWord16' to 'SWord 16'. See also 'fromSized'.
       toSized :: a -> ToSized a

       default toSized :: (Num (ToSized a), Integral a) => (a -> ToSized a)
       toSized = a -> ToSized a
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral

    instance {-# OVERLAPPING  #-} ToSizedBV Word8
    instance {-# OVERLAPPING  #-} ToSizedBV Word16
    instance {-# OVERLAPPING  #-} ToSizedBV Word32
    instance {-# OVERLAPPING  #-} ToSizedBV Word64
    instance {-# OVERLAPPING  #-} ToSizedBV Int8
    instance {-# OVERLAPPING  #-} ToSizedBV Int16
    instance {-# OVERLAPPING  #-} ToSizedBV Int32
    instance {-# OVERLAPPING  #-} ToSizedBV Int64
    instance {-# OVERLAPPING  #-} ToSizedBV SWord8  where toSized :: SWord8 -> ToSized SWord8
    toSized = SWord8 -> ToSized SWord8
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    Trans.sFromIntegral
    instance {-# OVERLAPPING  #-} ToSizedBV SWord16 where toSized :: SWord16 -> ToSized SWord16
    toSized = SWord16 -> ToSized SWord16
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    Trans.sFromIntegral
    instance {-# OVERLAPPING  #-} ToSizedBV SWord32 where toSized :: SWord32 -> ToSized SWord32
    toSized = SWord32 -> ToSized SWord32
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    Trans.sFromIntegral
    instance {-# OVERLAPPING  #-} ToSizedBV SWord64 where toSized :: SWord64 -> ToSized SWord64
    toSized = SWord64 -> ToSized SWord64
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    Trans.sFromIntegral
    instance {-# OVERLAPPING  #-} ToSizedBV SInt8   where toSized :: SInt8 -> ToSized SInt8
    toSized = SInt8 -> ToSized SInt8
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    Trans.sFromIntegral
    instance {-# OVERLAPPING  #-} ToSizedBV SInt16  where toSized :: SInt16 -> ToSized SInt16
    toSized = SInt16 -> ToSized SInt16
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    Trans.sFromIntegral
    instance {-# OVERLAPPING  #-} ToSizedBV SInt32  where toSized :: SInt32 -> ToSized SInt32
    toSized = SInt32 -> ToSized SInt32
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    Trans.sFromIntegral
    instance {-# OVERLAPPING  #-} ToSizedBV SInt64  where toSized :: SInt64 -> ToSized SInt64
    toSized = SInt64 -> ToSized SInt64
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    Trans.sFromIntegral
    instance {-# OVERLAPPABLE #-} ToSizedCstr arg => ToSizedBV arg where toSized :: arg -> ToSized arg
    toSized = String -> arg -> ToSized arg
    forall a. HasCallStack => String -> a
    error "unreachable"