    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Dynamic
    -- Copyright : (c) Brian Huffman
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Dynamically typed low-level API to the SBV library, for users who
    -- want to generate symbolic values at run-time. Note that with this
    -- API it is possible to create terms that are not type correct; use
    -- at your own risk!
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Dynamic
      (
      -- * Programming with symbolic values
      -- ** Symbolic types
      -- *** Abstract symbolic value type
        SVal
      , HasKind(..), Kind(..), CV(..), CVal(..), cvToBool
      -- *** SMT Arrays of symbolic values
      , SArr, readSArr, writeSArr, mergeSArr, newSArr, eqSArr
      -- *** Functional arrays of symbolic values
      , SFunArr, readSFunArr, writeSFunArr, mergeSFunArr, newSFunArr

      -- ** Creating a symbolic variable
      , Symbolic
      , Quantifier(..)
      , svMkSymVar
      , sWordN, sWordN_, sIntN, sIntN_
      -- ** Operations on symbolic values
      -- *** Boolean literals
      , svTrue, svFalse, svBool, svAsBool
      -- *** Integer literals
      , svInteger, svAsInteger
      -- *** Float literals
      , svFloat, svDouble
      -- *** Algebraic reals (only from rationals)
      , svReal, svNumerator, svDenominator
      -- *** Symbolic equality
      , svEqual, svNotEqual
      -- *** Constructing concrete lists
      , svEnumFromThenTo
      -- *** Symbolic ordering
      , svLessThan, svGreaterThan, svLessEq, svGreaterEq, svStructuralLessThan
      -- *** Arithmetic operations
      , svPlus, svTimes, svMinus, svUNeg, svAbs
      , svDivide, svQuot, svRem, svQuotRem, svExp
      , svAddConstant, svIncrement, svDecrement
      -- *** Logical operations
      , svAnd, svOr, svXOr, svNot
      , svShl, svShr, svRol, svRor
      -- *** Splitting, joining, and extending
      , svExtract, svJoin
      -- *** Sign-casting
      , svSign, svUnsign
      -- *** Numeric conversions
      , svFromIntegral
      -- *** Indexed lookups
      , svSelect
      -- *** Word-level operations
      , svToWord1, svFromWord1, svTestBit, svSetBit
      , svShiftLeft, svShiftRight
      , svRotateLeft, svRotateRight
      , svBarrelRotateLeft, svBarrelRotateRight
      , svWordFromBE, svWordFromLE
      , svBlastLE, svBlastBE
      -- ** Conditionals: Mergeable values
      , svIte, svLazyIte, svSymbolicMerge
      -- * Uninterpreted sorts, constants, and functions
      , svUninterpreted
      -- * Properties, proofs, and satisfiability
      -- ** Proving properties
      , proveWith
      -- ** Checking satisfiability
      , satWith, allSatWith
      -- ** Checking safety
      , safeWith
      -- * Proving properties using multiple solvers
      , proveWithAll, proveWithAny, satWithAll, satWithAny
      -- * Proving properties using multiple threads
      , proveConcurrentWithAll, proveConcurrentWithAny
      , satConcurrentWithAny, satConcurrentWithAll
      -- * Quick-check
      , svQuickCheck

      -- * Model extraction

      -- ** Inspecting proof results
      , ThmResult(..), SatResult(..), AllSatResult(..), SafeResult(..), OptimizeResult(..), SMTResult(..)

      -- ** Programmable model extraction
      , genParse, getModelAssignment, getModelDictionary
      -- * SMT Interface: Configurations and solvers
      , SMTConfig(..), SMTLibVersion(..), Solver(..), SMTSolver(..), boolector, cvc4, yices, z3, mathSAT, abc, defaultSolverConfig, defaultSMTCfg, sbvCheckSolverInstallation, sbvAvailableSolvers

      -- * Symbolic computations
      , outputSVal

      -- * Code generation from symbolic programs
      , SBVCodeGen

      -- ** Setting code-generation options
      , cgPerformRTCs, cgSetDriverValues, cgGenerateDriver, cgGenerateMakefile

      -- ** Designating inputs
      , svCgInput, svCgInputArr

      -- ** Designating outputs
      , svCgOutput, svCgOutputArr

      -- ** Designating return values
      , svCgReturn, svCgReturnArr

      -- ** Code generation with uninterpreted functions
      , cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert

      -- ** Code generation with 'Data.SBV.SInteger' and 'Data.SBV.SReal' types
      , cgIntegerSize, cgSRealType, CgSRealType(..)

      -- ** Compilation to C
      , compileToC, compileToCLib

      -- ** Compilation to SMTLib
      , generateSMTBenchmark
      ) where

    import Data.Map.Strict (Map)

    import Data.SBV.Core.Kind
    import Data.SBV.Core.Concrete
    import Data.SBV.Core.Symbolic
    import Data.SBV.Core.Operations

    import Data.SBV.Compilers.CodeGen ( SBVCodeGen
                                      , svCgInput, svCgInputArr
                                      , svCgOutput, svCgOutputArr
                                      , svCgReturn, svCgReturnArr
                                      , cgPerformRTCs, cgSetDriverValues, cgGenerateDriver, cgGenerateMakefile
                                      , cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert
                                      , cgIntegerSize, cgSRealType, CgSRealType(..)
                                      )
    import Data.SBV.Compilers.C       (compileToC, compileToCLib)

    import Data.SBV.Provers.Prover (boolector, cvc4, yices, z3, mathSAT, abc, defaultSMTCfg)
    import Data.SBV.SMT.SMT        (ThmResult(..), SatResult(..), SafeResult(..), OptimizeResult(..), AllSatResult(..), genParse)
    import Data.SBV                (sbvCheckSolverInstallation, defaultSolverConfig, sbvAvailableSolvers)

    import qualified Data.SBV                as SBV (SBool, proveWithAll, proveWithAny, satWithAll, satWithAny
                                                    , proveConcurrentWithAll, proveConcurrentWithAny
                                                    , satConcurrentWithAny, satConcurrentWithAll
                                                    )
    import qualified Data.SBV.Core.Data      as SBV (SBV(..))
    import qualified Data.SBV.Core.Model     as SBV (sbvQuickCheck)
    import qualified Data.SBV.Provers.Prover as SBV (proveWith, satWith, safeWith, allSatWith, generateSMTBenchmark)
    import qualified Data.SBV.SMT.SMT        as SBV (Modelable(getModelAssignment, getModelDictionary))

    import Data.Time (NominalDiffTime)

    -- | Dynamic variant of quick-check
    svQuickCheck :: Symbolic SVal -> IO Bool
    svQuickCheck :: Symbolic SVal -> IO Bool
    svQuickCheck = Symbolic SBool -> IO Bool
    SBV.sbvQuickCheck (Symbolic SBool -> IO Bool)
    -> (Symbolic SVal -> Symbolic SBool) -> Symbolic SVal -> IO Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap SVal -> SBool
    toSBool

    toSBool :: SVal -> SBV.SBool
    toSBool :: SVal -> SBool
    toSBool = SVal -> SBool
    forall a. SVal -> SBV a
    SBV.SBV

    -- | Create SMT-Lib benchmarks. The first argument is the basename of the file, we will automatically
    -- add ".smt2" per SMT-Lib2 convention. The 'Bool' argument controls whether this is a SAT instance, i.e.,
    -- translate the query directly, or a PROVE instance, i.e., translate the negated query.
    generateSMTBenchmark :: Bool -> Symbolic SVal -> IO String
    generateSMTBenchmark :: Bool -> Symbolic SVal -> IO String
    generateSMTBenchmark isSat :: Bool
    isSat s :: Symbolic SVal
    s = Bool -> Symbolic SBool -> IO String
    forall (m :: * -> *) a.
    (MonadIO m, MProvable m a) =>
    Bool -> a -> m String
    SBV.generateSMTBenchmark Bool
    isSat ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap SVal -> SBool
    toSBool Symbolic SVal
    s)

    -- | Proves the predicate using the given SMT-solver
    proveWith :: SMTConfig -> Symbolic SVal -> IO ThmResult
    proveWith :: SMTConfig -> Symbolic SVal -> IO ThmResult
    proveWith cfg :: SMTConfig
    cfg s :: Symbolic SVal
    s = SMTConfig -> Symbolic SBool -> IO ThmResult
    forall (m :: * -> *) a.
    MProvable m a =>
    SMTConfig -> a -> m ThmResult
    SBV.proveWith SMTConfig
    cfg ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap SVal -> SBool
    toSBool Symbolic SVal
    s)

    -- | Find a satisfying assignment using the given SMT-solver
    satWith :: SMTConfig -> Symbolic SVal -> IO SatResult
    satWith :: SMTConfig -> Symbolic SVal -> IO SatResult
    satWith cfg :: SMTConfig
    cfg s :: Symbolic SVal
    s = SMTConfig -> Symbolic SBool -> IO SatResult
    forall (m :: * -> *) a.
    MProvable m a =>
    SMTConfig -> a -> m SatResult
    SBV.satWith SMTConfig
    cfg ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap SVal -> SBool
    toSBool Symbolic SVal
    s)

    -- | Check safety using the given SMT-solver
    safeWith :: SMTConfig -> Symbolic SVal -> IO [SafeResult]
    safeWith :: SMTConfig -> Symbolic SVal -> IO [SafeResult]
    safeWith cfg :: SMTConfig
    cfg s :: Symbolic SVal
    s = SMTConfig -> Symbolic SBool -> IO [SafeResult]
    forall (m :: * -> *) a.
    SExecutable m a =>
    SMTConfig -> a -> m [SafeResult]
    SBV.safeWith SMTConfig
    cfg ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap SVal -> SBool
    toSBool Symbolic SVal
    s)

    -- | Find all satisfying assignments using the given SMT-solver
    allSatWith :: SMTConfig -> Symbolic SVal -> IO AllSatResult
    allSatWith :: SMTConfig -> Symbolic SVal -> IO AllSatResult
    allSatWith cfg :: SMTConfig
    cfg s :: Symbolic SVal
    s = SMTConfig -> Symbolic SBool -> IO AllSatResult
    forall (m :: * -> *) a.
    MProvable m a =>
    SMTConfig -> a -> m AllSatResult
    SBV.allSatWith SMTConfig
    cfg ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap SVal -> SBool
    toSBool Symbolic SVal
    s)

    -- | Prove a property with multiple solvers, running them in separate threads. The
    -- results will be returned in the order produced.
    proveWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, ThmResult)]
    proveWithAll :: [SMTConfig]
    -> Symbolic SVal -> IO [(Solver, NominalDiffTime, ThmResult)]
    proveWithAll cfgs :: [SMTConfig]
    cfgs s :: Symbolic SVal
    s = [SMTConfig]
    -> Symbolic SBool -> IO [(Solver, NominalDiffTime, ThmResult)]
    forall a.
    Provable a =>
    [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
    SBV.proveWithAll [SMTConfig]
    cfgs ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap SVal -> SBool
    toSBool Symbolic SVal
    s)

    -- | Prove a property with multiple solvers, running them in separate
    -- threads. Only the result of the first one to finish will be
    -- returned, remaining threads will be killed.
    proveWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, NominalDiffTime, ThmResult)
    proveWithAny :: [SMTConfig]
    -> Symbolic SVal -> IO (Solver, NominalDiffTime, ThmResult)
    proveWithAny cfgs :: [SMTConfig]
    cfgs s :: Symbolic SVal
    s = [SMTConfig]
    -> Symbolic SBool -> IO (Solver, NominalDiffTime, ThmResult)
    forall a.
    Provable a =>
    [SMTConfig] -> a -> IO (Solver, NominalDiffTime, ThmResult)
    SBV.proveWithAny [SMTConfig]
    cfgs ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap SVal -> SBool
    toSBool Symbolic SVal
    s)

    -- | Prove a property with query mode using multiple threads. Each query
    -- computation will spawn a thread and a unique instance of your solver to run
    -- asynchronously. The 'Symbolic' 'SVal' is duplicated for each thread. This
    -- function will block until all child threads return.
    proveConcurrentWithAll :: SMTConfig -> Symbolic SVal -> [Query SVal] -> IO [(Solver, NominalDiffTime, ThmResult)]
    proveConcurrentWithAll :: SMTConfig
    -> Symbolic SVal
    -> [Query SVal]
    -> IO [(Solver, NominalDiffTime, ThmResult)]
    proveConcurrentWithAll cfg :: SMTConfig
    cfg s :: Symbolic SVal
    s queries :: [Query SVal]
    queries = SMTConfig
    -> [Query SVal]
    -> Symbolic SBool
    -> IO [(Solver, NominalDiffTime, ThmResult)]
    forall a b.
    Provable a =>
    SMTConfig
    -> [Query b] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
    SBV.proveConcurrentWithAll SMTConfig
    cfg [Query SVal]
    queries ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap SVal -> SBool
    toSBool Symbolic SVal
    s)

    -- | Prove a property with query mode using multiple threads. Each query
    -- computation will spawn a thread and a unique instance of your solver to run
    -- asynchronously. The 'Symbolic' 'SVal' is duplicated for each thread. This
    -- function will return the first query computation that completes, killing the others.
    proveConcurrentWithAny :: SMTConfig -> Symbolic SVal -> [Query SVal] -> IO (Solver, NominalDiffTime, ThmResult)
    proveConcurrentWithAny :: SMTConfig
    -> Symbolic SVal
    -> [Query SVal]
    -> IO (Solver, NominalDiffTime, ThmResult)
    proveConcurrentWithAny cfg :: SMTConfig
    cfg s :: Symbolic SVal
    s queries :: [Query SVal]
    queries = SMTConfig
    -> [Query SVal]
    -> Symbolic SBool
    -> IO (Solver, NominalDiffTime, ThmResult)
    forall a b.
    Provable a =>
    SMTConfig
    -> [Query b] -> a -> IO (Solver, NominalDiffTime, ThmResult)
    SBV.proveConcurrentWithAny SMTConfig
    cfg [Query SVal]
    queries ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap SVal -> SBool
    toSBool Symbolic SVal
    s)

    -- | Find a satisfying assignment to a property with multiple solvers,
    -- running them in separate threads. The results will be returned in
    -- the order produced.
    satWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, SatResult)]
    satWithAll :: [SMTConfig]
    -> Symbolic SVal -> IO [(Solver, NominalDiffTime, SatResult)]
    satWithAll cfgs :: [SMTConfig]
    cfgs s :: Symbolic SVal
    s = [SMTConfig]
    -> Symbolic SBool -> IO [(Solver, NominalDiffTime, SatResult)]
    forall a.
    Provable a =>
    [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
    SBV.satWithAll [SMTConfig]
    cfgs ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap SVal -> SBool
    toSBool Symbolic SVal
    s)

    -- | Find a satisfying assignment to a property with multiple solvers,
    -- running them in separate threads. Only the result of the first one
    -- to finish will be returned, remaining threads will be killed.
    satWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult)
    satWithAny :: [SMTConfig]
    -> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult)
    satWithAny cfgs :: [SMTConfig]
    cfgs s :: Symbolic SVal
    s = [SMTConfig]
    -> Symbolic SBool -> IO (Solver, NominalDiffTime, SatResult)
    forall a.
    Provable a =>
    [SMTConfig] -> a -> IO (Solver, NominalDiffTime, SatResult)
    SBV.satWithAny [SMTConfig]
    cfgs ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap SVal -> SBool
    toSBool Symbolic SVal
    s)

    -- | Find a satisfying assignment to a property with multiple threads in query
    -- mode. The 'Symbolic' 'SVal' represents what is known to all child query threads.
    -- Each query thread will spawn a unique instance of the solver. Only the first
    -- one to finish will be returned and the other threads will be killed.
    satConcurrentWithAny :: SMTConfig -> [Query b] -> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult)
    satConcurrentWithAny :: SMTConfig
    -> [Query b]
    -> Symbolic SVal
    -> IO (Solver, NominalDiffTime, SatResult)
    satConcurrentWithAny cfg :: SMTConfig
    cfg qs :: [Query b]
    qs s :: Symbolic SVal
    s = SMTConfig
    -> [Query b]
    -> Symbolic SBool
    -> IO (Solver, NominalDiffTime, SatResult)
    forall a b.
    Provable a =>
    SMTConfig
    -> [Query b] -> a -> IO (Solver, NominalDiffTime, SatResult)
    SBV.satConcurrentWithAny SMTConfig
    cfg [Query b]
    qs ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap SVal -> SBool
    toSBool Symbolic SVal
    s)

    -- | Find a satisfying assignment to a property with multiple threads in query
    -- mode. The 'Symbolic' 'SVal' represents what is known to all child query threads.
    -- Each query thread will spawn a unique instance of the solver. This function
    -- will block until all child threads have completed.
    satConcurrentWithAll :: SMTConfig -> [Query b] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, SatResult)]
    satConcurrentWithAll :: SMTConfig
    -> [Query b]
    -> Symbolic SVal
    -> IO [(Solver, NominalDiffTime, SatResult)]
    satConcurrentWithAll cfg :: SMTConfig
    cfg qs :: [Query b]
    qs s :: Symbolic SVal
    s = SMTConfig
    -> [Query b]
    -> Symbolic SBool
    -> IO [(Solver, NominalDiffTime, SatResult)]
    forall a b.
    Provable a =>
    SMTConfig
    -> [Query b] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
    SBV.satConcurrentWithAll SMTConfig
    cfg [Query b]
    qs ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap SVal -> SBool
    toSBool Symbolic SVal
    s)

    -- | Extract a model, the result is a tuple where the first argument (if True)
    -- indicates whether the model was "probable". (i.e., if the solver returned unknown.)
    getModelAssignment :: SMTResult -> Either String (Bool, [CV])
    getModelAssignment :: SMTResult -> Either String (Bool, [CV])
    getModelAssignment = SMTResult -> Either String (Bool, [CV])
    forall a b.
    (Modelable a, SatModel b) =>
    a -> Either String (Bool, b)
    SBV.getModelAssignment

    -- | Extract a model dictionary. Extract a dictionary mapping the variables to
    -- their respective values as returned by the SMT solver. Also see `Data.SBV.SMT.getModelDictionaries`.
    getModelDictionary :: SMTResult -> Map String CV
    getModelDictionary :: SMTResult -> Map String CV
    getModelDictionary = SMTResult -> Map String CV
    forall a. Modelable a => a -> Map String CV
    SBV.getModelDictionary