-----------------------------------------------------------------------------
-- |
-- 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 FlexibleContexts #-}
{-# LANGUAGE NamedFieldPuns   #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Client.BaseIO where

import Data.SBV.Core.Data      (Kind, Outputtable, Penalty,
                                SymVal, SBool, SBV, SChar, SDouble, SFloat, SWord, SInt,
                                SFPHalf, SFPBFloat, SFPSingle, SFPDouble, SFPQuad, SFloatingPoint,
                                SInt8, SInt16, SInt32, SInt64, SInteger, SList,
                                SReal, SString, SV, SWord8, SWord16, SWord32,
                                SWord64, SEither, SRational, SMaybe, SSet, SArray, constrain, (.==))
import Data.SBV.Core.Kind      (BVIsNonZero, ValidFloat)
import Data.SBV.Core.Model     (Metric(..), SymTuple)
import Data.SBV.Core.Symbolic  (Objective, OptimizeStyle, Result, VarContext, Symbolic, SBVRunMode, SMTConfig,
                                SVal, symbolicEnv, rPartitionVars, State(..))
import Data.SBV.Control.Types  (SMTOption)
import Data.SBV.Provers.Prover (Provable, Satisfiable, SExecutable, ThmResult)
import Data.SBV.SMT.SMT        (AllSatResult, SafeResult, SatResult, OptimizeResult)

import GHC.TypeLits (KnownNat)

import Data.IORef(readIORef, writeIORef)

import qualified Data.SBV.Core.Data      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

import Control.Monad.Trans (liftIO)

-- | 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 :: forall a. Provable a => a -> IO ThmResult
prove = a -> IO ThmResult
forall (m :: * -> *) a. ProvableM 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 :: forall a. Provable a => SMTConfig -> a -> IO ThmResult
proveWith = SMTConfig -> a -> IO ThmResult
forall (m :: * -> *) a.
ProvableM m a =>
SMTConfig -> a -> m ThmResult
Trans.proveWith

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

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

-- | 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 :: Satisfiable a => a -> IO SatResult
sat :: forall a. Satisfiable a => a -> IO SatResult
sat = a -> IO SatResult
forall (m :: * -> *) a. SatisfiableM 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 :: Satisfiable a => SMTConfig -> a -> IO SatResult
satWith :: forall a. Satisfiable a => SMTConfig -> a -> IO SatResult
satWith = SMTConfig -> a -> IO SatResult
forall (m :: * -> *) a.
SatisfiableM m a =>
SMTConfig -> a -> m SatResult
Trans.satWith

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

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

-- | 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 :: Satisfiable a => a -> IO AllSatResult
allSat :: forall a. Satisfiable a => a -> IO AllSatResult
allSat = a -> IO AllSatResult
forall (m :: * -> *) a. SatisfiableM 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 :: Satisfiable a => SMTConfig -> a -> IO AllSatResult
allSatWith :: forall a. Satisfiable a => SMTConfig -> a -> IO AllSatResult
allSatWith = SMTConfig -> a -> IO AllSatResult
forall (m :: * -> *) a.
SatisfiableM 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 :: Satisfiable a => OptimizeStyle -> a -> IO OptimizeResult
optimize :: forall a. Satisfiable a => OptimizeStyle -> a -> IO OptimizeResult
optimize = OptimizeStyle -> a -> IO OptimizeResult
forall (m :: * -> *) a.
SatisfiableM 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 :: Satisfiable a => SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult
optimizeWith :: forall a.
Satisfiable a =>
SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult
optimizeWith = SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult
forall (m :: * -> *) a.
SatisfiableM m a =>
SMTConfig -> OptimizeStyle -> a -> m OptimizeResult
Trans.optimizeWith

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

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

-- | 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 :: forall a. Provable a => a -> IO Bool
isTheorem = a -> IO Bool
forall (m :: * -> *) a. ProvableM 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 :: forall a. Provable a => SMTConfig -> a -> IO Bool
isTheoremWith = SMTConfig -> a -> IO Bool
forall (m :: * -> *) a. ProvableM 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 :: Satisfiable a => a -> IO Bool
isSatisfiable :: forall a. Satisfiable a => a -> IO Bool
isSatisfiable = a -> IO Bool
forall (m :: * -> *) a. SatisfiableM 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 :: Satisfiable a => SMTConfig -> a -> IO Bool
isSatisfiableWith :: forall a. Satisfiable a => SMTConfig -> a -> IO Bool
isSatisfiableWith = SMTConfig -> a -> IO Bool
forall (m :: * -> *) a.
SatisfiableM 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 :: forall a. Symbolic a -> IO a
runSMT = SymbolicT IO 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 :: forall a. SMTConfig -> Symbolic a -> IO a
runSMTWith = SMTConfig -> SymbolicT IO a -> IO a
forall (m :: * -> *) a.
MonadIO m =>
SMTConfig -> SymbolicT m a -> m a
Trans.runSMTWith

-- | Create an argument for a name used in a safety-checking call.
--
-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sName_'
sName :: SExecutable IO a => a -> Symbolic ()
sName :: forall a. SExecutable IO a => a -> Symbolic ()
sName = a -> Symbolic ()
forall (m :: * -> *) a. SExecutable m a => 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 :: forall a. SExecutable IO a => 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 :: forall a. SExecutable IO a => 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 :: VarContext -> Kind -> Maybe String -> Symbolic (SBV a)
mkSymSBV :: forall a. VarContext -> Kind -> Maybe String -> Symbolic (SBV a)
mkSymSBV = VarContext -> Kind -> Maybe String -> SymbolicT IO (SBV a)
forall a (m :: * -> *).
MonadSymbolic m =>
VarContext -> 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 :: forall a. 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 :: forall a. Outputtable a => a -> Symbolic a
output = a -> SymbolicT IO a
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
forall (m :: * -> *). MonadSymbolic m => a -> m a
Trans.output

-- | Create a partitioning constraint, for all-sat calls.
allSatPartition :: SymVal a => String -> SBV a -> Symbolic ()
allSatPartition :: forall a. SymVal a => String -> SBV a -> Symbolic ()
allSatPartition String
nm SBV a
term = do
   State{IORef [String]
rPartitionVars :: State -> IORef [String]
rPartitionVars :: IORef [String]
rPartitionVars} <- SymbolicT IO State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv

   -- Generate a unique variable with the prefix nm if necessary and
   -- add it to partitions
   String
fresh <- IO String -> SymbolicT IO String
forall a. IO a -> SymbolicT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO String -> SymbolicT IO String)
-> IO String -> SymbolicT IO String
forall a b. (a -> b) -> a -> b
$ do [String]
olds <- IORef [String] -> IO [String]
forall a. IORef a -> IO a
readIORef IORef [String]
rPartitionVars
                        let new :: String
new = case (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
olds) (String
nm String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i | Int
i <- [(Int
1 :: Int) ..]]) of
                                    String
h:[String]
_ -> String
h
                                    []  -> String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"Impossible: Can't get a fresh variable from infinite list in partition." String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String, SBV a) -> String
forall a. Show a => a -> String
show (String
nm, SBV a
term)
                        IORef [String] -> [String] -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef [String]
rPartitionVars ([String]
olds [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
new])
                        String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
new

   -- declare and constrain
   SBV a
v <- String -> Symbolic (SBV a)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
fresh
   SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SBV a
v SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
term

-- | 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 :: forall a. SymVal a => String -> Symbolic (SBV a)
free = String -> SymbolicT IO (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
forall (m :: * -> *). 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_ :: forall a. SymVal a => Symbolic (SBV a)
free_ = SymbolicT IO (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
forall (m :: * -> *). 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 :: forall a. SymVal a => Int -> Symbolic [SBV a]
mkFreeVars = Int -> SymbolicT IO [SBV a]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
Int -> m [SBV a]
forall (m :: * -> *). 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 :: forall a. SymVal a => String -> Symbolic (SBV a)
symbolic = String -> SymbolicT IO (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
forall (m :: * -> *). 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 :: forall a. SymVal a => [String] -> Symbolic [SBV a]
symbolics = [String] -> SymbolicT IO [SBV a]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
forall (m :: * -> *). 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 => VarContext -> Maybe String -> Symbolic (SBV a)
mkSymVal :: forall a.
SymVal a =>
VarContext -> Maybe String -> Symbolic (SBV a)
mkSymVal = VarContext -> Maybe String -> SymbolicT IO (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
VarContext -> Maybe String -> m (SBV a)
forall (m :: * -> *).
MonadSymbolic m =>
VarContext -> Maybe String -> m (SBV a)
Trans.mkSymVal

-- 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 -> VarContext -> Maybe String -> Symbolic (SBV a)
genMkSymVar :: forall a. Kind -> VarContext -> Maybe String -> Symbolic (SBV a)
genMkSymVar = Kind -> VarContext -> Maybe String -> SymbolicT IO (SBV a)
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> 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 unnamed '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, BVIsNonZero n) => String -> Symbolic (SWord n)
sWord :: forall (n :: Nat).
(KnownNat n, BVIsNonZero n) =>
String -> Symbolic (SWord n)
sWord = String -> SymbolicT IO (SWord n)
forall (n :: Nat) (m :: * -> *).
(KnownNat n, BVIsNonZero 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, BVIsNonZero n) => Symbolic (SWord n)
sWord_ :: forall (n :: Nat).
(KnownNat n, BVIsNonZero n) =>
Symbolic (SWord n)
sWord_ = SymbolicT IO (SWord n)
forall (n :: Nat) (m :: * -> *).
(KnownNat n, BVIsNonZero 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, BVIsNonZero n) => [String] -> Symbolic [SWord n]
sWords :: forall (n :: Nat).
(KnownNat n, BVIsNonZero n) =>
[String] -> Symbolic [SWord n]
sWords = [String] -> SymbolicT IO [SWord n]
forall (n :: Nat) (m :: * -> *).
(KnownNat n, BVIsNonZero 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, BVIsNonZero n) => String -> Symbolic (SInt n)
sInt :: forall (n :: Nat).
(KnownNat n, BVIsNonZero n) =>
String -> Symbolic (SInt n)
sInt = String -> SymbolicT IO (SInt n)
forall (n :: Nat) (m :: * -> *).
(KnownNat n, BVIsNonZero 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, BVIsNonZero n) => Symbolic (SInt n)
sInt_ :: forall (n :: Nat). (KnownNat n, BVIsNonZero n) => Symbolic (SInt n)
sInt_ = SymbolicT IO (SInt n)
forall (n :: Nat) (m :: * -> *).
(KnownNat n, BVIsNonZero 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, BVIsNonZero n) => [String] -> Symbolic [SInt n]
sInts :: forall (n :: Nat).
(KnownNat n, BVIsNonZero n) =>
[String] -> Symbolic [SInt n]
sInts = [String] -> SymbolicT IO [SInt n]
forall (n :: Nat) (m :: * -> *).
(KnownNat n, BVIsNonZero 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 'SFloatingPoint eb sb'
--
-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFloatingPoint'
sFloatingPoint :: ValidFloat eb sb => String -> Symbolic (SFloatingPoint eb sb)
sFloatingPoint :: forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
String -> Symbolic (SFloatingPoint eb sb)
sFloatingPoint = String -> Symbolic (SFloatingPoint eb sb)
forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
String -> Symbolic (SFloatingPoint eb sb)
Trans.sFloatingPoint

-- | Declare an unnamed 'SFloatingPoint' @eb@ @sb@
--
-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFloatingPoint_'
sFloatingPoint_ :: ValidFloat eb sb => Symbolic (SFloatingPoint eb sb)
sFloatingPoint_ :: forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
Symbolic (SFloatingPoint eb sb)
sFloatingPoint_ = Symbolic (SFloatingPoint eb sb)
forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
Symbolic (SFloatingPoint eb sb)
Trans.sFloatingPoint_

-- | Declare a list of 'SFloatingPoint' @eb@ @sb@'s
--
-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFloatingPoints'
sFloatingPoints :: ValidFloat eb sb => [String] -> Symbolic [SFloatingPoint eb sb]
sFloatingPoints :: forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
[String] -> Symbolic [SFloatingPoint eb sb]
sFloatingPoints = [String] -> Symbolic [SFloatingPoint eb sb]
forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
[String] -> Symbolic [SFloatingPoint eb sb]
Trans.sFloatingPoints

-- | Declare a named 'SFPHalf'
--
-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPHalf'
sFPHalf :: String -> Symbolic SFPHalf
sFPHalf :: String -> Symbolic SFPHalf
sFPHalf = String -> Symbolic SFPHalf
Trans.sFPHalf

-- | Declare an unnamed 'SFPHalf'
--
-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPHalf_'
sFPHalf_ :: Symbolic SFPHalf
sFPHalf_ :: Symbolic SFPHalf
sFPHalf_ = Symbolic SFPHalf
Trans.sFPHalf_

-- | Declare a list of 'SFPHalf's
--
-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPHalfs'
sFPHalfs :: [String] -> Symbolic [SFPHalf]
sFPHalfs :: [String] -> Symbolic [SFPHalf]
sFPHalfs = [String] -> Symbolic [SFPHalf]
Trans.sFPHalfs

-- | Declare a named 'SFPBFloat'
--
-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.SFPBFloat'
sFPBFloat :: String -> Symbolic SFPBFloat
sFPBFloat :: String -> Symbolic SFPBFloat
sFPBFloat = String -> Symbolic SFPBFloat
Trans.sFPBFloat

-- | Declare an unnamed 'SFPBFloat'
--
-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.SFPBFloat'
sFPBFloat_ :: Symbolic SFPBFloat
sFPBFloat_ :: Symbolic SFPBFloat
sFPBFloat_ = Symbolic SFPBFloat
Trans.sFPBFloat_

-- | Declare a list of 'SFPQuad's
--
-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPBFloats'
sFPBFloats :: [String] -> Symbolic [SFPBFloat]
sFPBFloats :: [String] -> Symbolic [SFPBFloat]
sFPBFloats = [String] -> Symbolic [SFPBFloat]
Trans.sFPBFloats

-- | Declare a named 'SFPSingle'
--
-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPSingle'
sFPSingle :: String -> Symbolic SFPSingle
sFPSingle :: String -> Symbolic SFPSingle
sFPSingle = String -> Symbolic SFPSingle
Trans.sFPSingle

-- | Declare an unnamed 'SFPSingle'
--
-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPSingle_'
sFPSingle_ :: Symbolic SFPSingle
sFPSingle_ :: Symbolic SFPSingle
sFPSingle_ = Symbolic SFPSingle
Trans.sFPSingle_

-- | Declare a list of 'SFPSingle's
--
-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPSingles'
sFPSingles :: [String] -> Symbolic [SFPSingle]
sFPSingles :: [String] -> Symbolic [SFPSingle]
sFPSingles = [String] -> Symbolic [SFPSingle]
Trans.sFPSingles

-- | Declare a named 'SFPDouble'
--
-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPDouble'
sFPDouble :: String -> Symbolic SFPDouble
sFPDouble :: String -> Symbolic SFPDouble
sFPDouble = String -> Symbolic SFPDouble
Trans.sFPDouble

-- | Declare an unnamed 'SFPDouble'
--
-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPDouble_'
sFPDouble_ :: Symbolic SFPDouble
sFPDouble_ :: Symbolic SFPDouble
sFPDouble_ = Symbolic SFPDouble
Trans.sFPDouble_

-- | Declare a list of 'SFPDouble's
--
-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPDoubles'
sFPDoubles :: [String] -> Symbolic [SFPDouble]
sFPDoubles :: [String] -> Symbolic [SFPDouble]
sFPDoubles = [String] -> Symbolic [SFPDouble]
Trans.sFPDoubles

-- | Declare a named 'SFPQuad'
--
-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPQuad'
sFPQuad :: String -> Symbolic SFPQuad
sFPQuad :: String -> Symbolic SFPQuad
sFPQuad = String -> Symbolic SFPQuad
Trans.sFPQuad

-- | Declare an unnamed 'SFPQuad'
--
-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPQuad_'
sFPQuad_ :: Symbolic SFPQuad
sFPQuad_ :: Symbolic SFPQuad
sFPQuad_ = Symbolic SFPQuad
Trans.sFPQuad_

-- | Declare a list of 'SFPQuad's
--
-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPQuads'
sFPQuads :: [String] -> Symbolic [SFPQuad]
sFPQuads :: [String] -> Symbolic [SFPQuad]
sFPQuads = [String] -> Symbolic [SFPQuad]
Trans.sFPQuads

-- | 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 :: forall a. SymVal a => String -> Symbolic (SList a)
sList = String -> SymbolicT IO (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_ :: forall a. SymVal a => Symbolic (SList a)
sList_ = SymbolicT IO (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 :: forall a. SymVal a => [String] -> Symbolic [SList a]
sLists = [String] -> SymbolicT IO [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 :: forall tup.
(SymTuple tup, SymVal tup) =>
String -> Symbolic (SBV tup)
sTuple = String -> SymbolicT IO (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_ :: forall tup. (SymTuple tup, SymVal tup) => Symbolic (SBV tup)
sTuple_ = SymbolicT IO (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 :: forall tup.
(SymTuple tup, SymVal tup) =>
[String] -> Symbolic [SBV tup]
sTuples = [String] -> SymbolicT IO [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 :: forall a b.
(SymVal a, SymVal b) =>
String -> Symbolic (SEither a b)
sEither = String -> SymbolicT IO (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_ :: forall a b. (SymVal a, SymVal b) => Symbolic (SEither a b)
sEither_ = SymbolicT IO (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 :: forall a b.
(SymVal a, SymVal b) =>
[String] -> Symbolic [SEither a b]
sEithers = [String] -> SymbolicT IO [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.SRational'.
--
-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sRational'
sRational :: String -> Symbolic SRational
sRational :: String -> Symbolic SRational
sRational = String -> Symbolic SRational
forall (m :: * -> *). MonadSymbolic m => String -> m SRational
Trans.sRational

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

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

-- | 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 :: forall a. SymVal a => String -> Symbolic (SMaybe a)
sMaybe = String -> SymbolicT IO (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_ :: forall a. SymVal a => Symbolic (SMaybe a)
sMaybe_ = SymbolicT IO (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 :: forall a. SymVal a => [String] -> Symbolic [SMaybe a]
sMaybes = [String] -> SymbolicT IO [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 :: forall a. (Ord a, SymVal a) => String -> Symbolic (SSet a)
sSet = String -> SymbolicT IO (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_ :: forall a. (Ord a, SymVal a) => Symbolic (SSet a)
sSet_ = SymbolicT IO (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 :: forall a. (Ord a, SymVal a) => [String] -> Symbolic [SSet a]
sSets = [String] -> SymbolicT IO [SSet a]
forall a (m :: * -> *).
(Ord a, SymVal a, MonadSymbolic m) =>
[String] -> m [SSet a]
Trans.sSets

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

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

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

-- | 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 :: forall a. Metric a => 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 :: forall a. Metric a => 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 :: SMTConfig -> SBVRunMode -> Symbolic a -> IO (a, Result)
runSymbolic :: forall a. SMTConfig -> SBVRunMode -> Symbolic a -> IO (a, Result)
runSymbolic = SMTConfig -> SBVRunMode -> SymbolicT IO a -> IO (a, Result)
forall (m :: * -> *) a.
MonadIO m =>
SMTConfig -> 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

-- | A variant of observe that you can use at the top-level. This is useful with quick-check, for instance.
--
-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sObserve'
sObserve :: SymVal a => String -> SBV a -> Symbolic ()
sObserve :: forall a. SymVal a => String -> SBV a -> Symbolic ()
sObserve String
m SBV a
x = String -> SVal -> Symbolic ()
forall (m :: * -> *). MonadSymbolic m => String -> SVal -> m ()
Trans.sObserve String
m (SBV a -> SVal
forall a. SBV a -> SVal
Trans.unSBV SBV a
x)