    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Core.Data
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Internal data-structures for the sbv library
    -----------------------------------------------------------------------------

    {-# LANGUAGE CPP                   #-}
    {-# LANGUAGE DefaultSignatures     #-}
    {-# LANGUAGE DeriveAnyClass        #-}
    {-# LANGUAGE DeriveGeneric         #-}
    {-# LANGUAGE FlexibleContexts      #-}
    {-# LANGUAGE FlexibleInstances     #-}
    {-# LANGUAGE InstanceSigs          #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE PatternGuards         #-}
    {-# LANGUAGE ScopedTypeVariables   #-}
    {-# LANGUAGE TypeApplications      #-}
    {-# LANGUAGE TypeFamilies          #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Core.Data
     ( SBool, SWord8, SWord16, SWord32, SWord64
     , SInt8, SInt16, SInt32, SInt64, SInteger, SReal, SFloat, SDouble, SChar, SString, SList
     , SEither, SMaybe
     , STuple, STuple2, STuple3, STuple4, STuple5, STuple6, STuple7, STuple8
     , RCSet(..), SSet
     , nan, infinity, sNaN, sInfinity, RoundingMode(..), SRoundingMode
     , sRoundNearestTiesToEven, sRoundNearestTiesToAway, sRoundTowardPositive, sRoundTowardNegative, sRoundTowardZero
     , sRNE, sRNA, sRTP, sRTN, sRTZ
     , SymVal(..)
     , CV(..), CVal(..), AlgReal(..), AlgRealPoly(..), ExtCV(..), GeneralizedCV(..), isRegularCV, cvSameType, cvToBool
     , mkConstCV ,liftCV2, mapCV, mapCV2
     , SV(..), trueSV, falseSV, trueCV, falseCV, normCV
     , SVal(..)
     , sTrue, sFalse, sNot, (.&&), (.||), (.<+>), (.~&), (.~|), (.=>), (.<=>), sAnd, sOr, sAny, sAll, fromBool
     , SBV(..), NodeId(..), mkSymSBV
     , ArrayContext(..), ArrayInfo, SymArray(..), SFunArray(..), SArray(..)
     , sbvToSV, sbvToSymSV, forceSVArg
     , SBVExpr(..), newExpr
     , cache, Cached, uncache, uncacheAI, HasKind(..)
     , Op(..), PBOp(..), FPOp(..), StrOp(..), SeqOp(..), RegExp(..), NamedSymVar, getTableIndex
     , SBVPgm(..), Symbolic, runSymbolic, State, getPathCondition, extendPathCondition
     , inSMTMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..)
     , SolverContext(..), internalVariable, internalConstraint, isCodeGenMode
     , SBVType(..), newUninterpreted
     , Quantifier(..), needsExistentials
     , SMTLibPgm(..), SMTLibVersion(..), smtLibVersionExtension, smtLibReservedNames
     , SolverCapabilities(..)
     , extractSymbolicSimulationState
     , SMTScript(..), Solver(..), SMTSolver(..), SMTResult(..), SMTModel(..), SMTConfig(..)
     , OptimizeStyle(..), Penalty(..), Objective(..)
     , QueryState(..), QueryT(..), SMTProblem(..)
     ) where

    import GHC.Generics (Generic)
    import GHC.Exts     (IsList(..))

    import Control.DeepSeq        (NFData(..))
    import Control.Monad.Trans    (liftIO)
    import Data.Int               (Int8, Int16, Int32, Int64)
    import Data.Word              (Word8, Word16, Word32, Word64)
    import Data.List              (elemIndex)
    import Data.Maybe             (fromMaybe)

    import Data.Proxy
    import Data.Typeable          (Typeable)

    import qualified Data.Generics as G    (Data(..))

    import System.Random

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

    import Data.SBV.Control.Types

    import Data.SBV.SMT.SMTLibNames

    import Data.SBV.Utils.Lib

    -- | Get the current path condition
    getPathCondition :: State -> SBool
    getPathCondition :: State -> SBool
    getPathCondition st :: State
    st = SVal -> SBool
    forall a. SVal -> SBV a
    SBV (State -> SVal
    getSValPathCondition State
    st)

    -- | Extend the path condition with the given test value.
    extendPathCondition :: State -> (SBool -> SBool) -> State
    extendPathCondition :: State -> (SBool -> SBool) -> State
    extendPathCondition st :: State
    st f :: SBool -> SBool
    f = State -> (SVal -> SVal) -> State
    extendSValPathCondition State
    st (SBool -> SVal
    forall a. SBV a -> SVal
    unSBV (SBool -> SVal) -> (SVal -> SBool) -> SVal -> SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBool -> SBool
    f (SBool -> SBool) -> (SVal -> SBool) -> SVal -> SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SVal -> SBool
    forall a. SVal -> SBV a
    SBV)

    -- | The "Symbolic" value. The parameter @a@ is phantom, but is
    -- extremely important in keeping the user interface strongly typed.
    newtype SBV a = SBV { SBV a -> SVal
    unSBV :: SVal }
                  deriving ((forall x. SBV a -> Rep (SBV a) x)
    -> (forall x. Rep (SBV a) x -> SBV a) -> Generic (SBV a)
    forall x. Rep (SBV a) x -> SBV a
    forall x. SBV a -> Rep (SBV a) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall a x. Rep (SBV a) x -> SBV a
    forall a x. SBV a -> Rep (SBV a) x
    $cto :: forall a x. Rep (SBV a) x -> SBV a
    $cfrom :: forall a x. SBV a -> Rep (SBV a) x
    Generic, SBV a -> ()
    (SBV a -> ()) -> NFData (SBV a)
    forall a. SBV a -> ()
    forall a. (a -> ()) -> NFData a
    rnf :: SBV a -> ()
    $crnf :: forall a. SBV a -> ()
    NFData)

    -- | A symbolic boolean/bit
    type SBool   = SBV Bool

    -- | 8-bit unsigned symbolic value
    type SWord8  = SBV Word8

    -- | 16-bit unsigned symbolic value
    type SWord16 = SBV Word16

    -- | 32-bit unsigned symbolic value
    type SWord32 = SBV Word32

    -- | 64-bit unsigned symbolic value
    type SWord64 = SBV Word64

    -- | 8-bit signed symbolic value, 2's complement representation
    type SInt8   = SBV Int8

    -- | 16-bit signed symbolic value, 2's complement representation
    type SInt16  = SBV Int16

    -- | 32-bit signed symbolic value, 2's complement representation
    type SInt32  = SBV Int32

    -- | 64-bit signed symbolic value, 2's complement representation
    type SInt64  = SBV Int64

    -- | Infinite precision signed symbolic value
    type SInteger = SBV Integer

    -- | Infinite precision symbolic algebraic real value
    type SReal = SBV AlgReal

    -- | IEEE-754 single-precision floating point numbers
    type SFloat = SBV Float

    -- | IEEE-754 double-precision floating point numbers
    type SDouble = SBV Double

    -- | A symbolic character. Note that, as far as SBV's symbolic strings are concerned, a character
    -- is currently an 8-bit unsigned value, corresponding to the ISO-8859-1 (Latin-1) character
    -- set: <http://en.wikipedia.org/wiki/ISO/IEC_8859-1>. A Haskell 'Char', on the other hand, is based
    -- on unicode. Therefore, there isn't a 1-1 correspondence between a Haskell character and an SBV
    -- character for the time being. This limitation is due to the SMT-solvers only supporting this
    -- particular subset. However, there is a pending proposal to add support for unicode, and SBV
    -- will track these changes to have full unicode support as solvers become available. For
    -- details, see: <http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml>
    type SChar = SBV Char

    -- | A symbolic string. Note that a symbolic string is /not/ a list of symbolic characters,
    -- that is, it is not the case that @SString = [SChar]@, unlike what one might expect following
    -- Haskell strings. An 'SString' is a symbolic value of its own, of possibly arbitrary but finite length,
    -- and internally processed as one unit as opposed to a fixed-length list of characters.
    type SString = SBV String

    -- | A symbolic list of items. Note that a symbolic list is /not/ a list of symbolic items,
    -- that is, it is not the case that @SList a = [a]@, unlike what one might expect following
    -- haskell lists\/sequences. An 'SList' is a symbolic value of its own, of possibly arbitrary but finite
    -- length, and internally processed as one unit as opposed to a fixed-length list of items.
    -- Note that lists can be nested, i.e., we do allow lists of lists of ... items.
    type SList a = SBV [a]

    -- | Symbolic 'Either'
    type SEither a b = SBV (Either a b)

    -- | Symbolic 'Maybe'
    type SMaybe a = SBV (Maybe a)

    -- | Symbolic 'Data.Set'. Note that we use 'RCSet', which supports
    -- both regular sets and complements, i.e., those obtained from the
    -- universal set (of the right type) by removing elements.
    type SSet a = SBV (RCSet a)

    -- | Symbolic 2-tuple. NB. 'STuple' and 'STuple2' are equivalent.
    type STuple a b = SBV (a, b)

    -- | Symbolic 2-tuple. NB. 'STuple' and 'STuple2' are equivalent.
    type STuple2 a b = SBV (a, b)

    -- | Symbolic 3-tuple.
    type STuple3 a b c = SBV (a, b, c)

    -- | Symbolic 4-tuple.
    type STuple4 a b c d = SBV (a, b, c, d)

    -- | Symbolic 5-tuple.
    type STuple5 a b c d e = SBV (a, b, c, d, e)

    -- | Symbolic 6-tuple.
    type STuple6 a b c d e f = SBV (a, b, c, d, e, f)

    -- | Symbolic 7-tuple.
    type STuple7 a b c d e f g = SBV (a, b, c, d, e, f, g)

    -- | Symbolic 8-tuple.
    type STuple8 a b c d e f g h = SBV (a, b, c, d, e, f, g, h)

    -- | IsList instance allows list literals to be written compactly.
    instance SymVal [a] => IsList (SList a) where
      type Item (SList a) = a
      fromList :: [Item (SList a)] -> SList a
    fromList = [Item (SList a)] -> SList a
    forall a. SymVal a => a -> SBV a
    literal
      toList :: SList a -> [Item (SList a)]
    toList x :: SList a
    x = [a] -> Maybe [a] -> [a]
    forall a. a -> Maybe a -> a
    fromMaybe ([Char] -> [a]
    forall a. HasCallStack => [Char] -> a
    error "IsList.toList used in a symbolic context!") (SList a -> Maybe [a]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SList a
    x)

    -- | Not-A-Number for 'Double' and 'Float'. Surprisingly, Haskell
    -- Prelude doesn't have this value defined, so we provide it here.
    nan :: Floating a => a
    nan :: a
    nan = 0a -> a -> a
    forall a. Fractional a => a -> a -> a
    /0

    -- | Infinity for 'Double' and 'Float'. Surprisingly, Haskell
    -- Prelude doesn't have this value defined, so we provide it here.
    infinity :: Floating a => a
    infinity :: a
    infinity = 1a -> a -> a
    forall a. Fractional a => a -> a -> a
    /0

    -- | Symbolic variant of Not-A-Number. This value will inhabit both
    -- 'SDouble' and 'SFloat'.
    sNaN :: (Floating a, SymVal a) => SBV a
    sNaN :: SBV a
    sNaN = a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal a
    forall a. Floating a => a
    nan

    -- | Symbolic variant of infinity. This value will inhabit both
    -- 'SDouble' and 'SFloat'.
    sInfinity :: (Floating a, SymVal a) => SBV a
    sInfinity :: SBV a
    sInfinity = a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal a
    forall a. Floating a => a
    infinity

    -- | Internal representation of a symbolic simulation result
    newtype SMTProblem = SMTProblem {SMTProblem -> SMTConfig -> SMTLibPgm
    smtLibPgm :: SMTConfig -> SMTLibPgm} -- ^ SMTLib representation, given the config

    -- | Symbolic 'True'
    sTrue :: SBool
    sTrue :: SBool
    sTrue = SVal -> SBool
    forall a. SVal -> SBV a
    SBV (Bool -> SVal
    svBool Bool
    True)

    -- | Symbolic 'False'
    sFalse :: SBool
    sFalse :: SBool
    sFalse = SVal -> SBool
    forall a. SVal -> SBV a
    SBV (Bool -> SVal
    svBool Bool
    False)

    -- | Symbolic boolean negation
    sNot :: SBool -> SBool
    sNot :: SBool -> SBool
    sNot (SBV b :: SVal
    b) = SVal -> SBool
    forall a. SVal -> SBV a
    SBV (SVal -> SVal
    svNot SVal
    b)

    -- | Symbolic conjunction
    infixr 3 .&&
    (.&&) :: SBool -> SBool -> SBool
    SBV x :: SVal
    x .&& :: SBool -> SBool -> SBool
    .&& SBV y :: SVal
    y = SVal -> SBool
    forall a. SVal -> SBV a
    SBV (SVal
    x SVal -> SVal -> SVal
    `svAnd` SVal
    y)

    -- | Symbolic disjunction
    infixr 2 .||
    (.||) :: SBool -> SBool -> SBool
    SBV x :: SVal
    x .|| :: SBool -> SBool -> SBool
    .|| SBV y :: SVal
    y = SVal -> SBool
    forall a. SVal -> SBV a
    SBV (SVal
    x SVal -> SVal -> SVal
    `svOr` SVal
    y)

    -- | Symbolic logical xor
    infixl 6 .<+>
    (.<+>) :: SBool -> SBool -> SBool
    SBV x :: SVal
    x .<+> :: SBool -> SBool -> SBool
    .<+> SBV y :: SVal
    y = SVal -> SBool
    forall a. SVal -> SBV a
    SBV (SVal
    x SVal -> SVal -> SVal
    `svXOr` SVal
    y)

    -- | Symbolic nand
    infixr 3 .~&
    (.~&) :: SBool -> SBool -> SBool
    x :: SBool
    x .~& :: SBool -> SBool -> SBool
    .~& y :: SBool
    y = SBool -> SBool
    sNot (SBool
    x SBool -> SBool -> SBool
    .&& SBool
    y)

    -- | Symbolic nor
    infixr 2 .~|
    (.~|) :: SBool -> SBool -> SBool
    x :: SBool
    x .~| :: SBool -> SBool -> SBool
    .~| y :: SBool
    y = SBool -> SBool
    sNot (SBool
    x SBool -> SBool -> SBool
    .|| SBool
    y)

    -- | Symbolic implication
    infixr 1 .=>
    (.=>) :: SBool -> SBool -> SBool
    x :: SBool
    x .=> :: SBool -> SBool -> SBool
    .=> y :: SBool
    y = SBool -> SBool
    sNot SBool
    x SBool -> SBool -> SBool
    .|| SBool
    y
    -- NB. Do *not* try to optimize @x .=> x = True@ here! If constants go through, it'll get simplified.
    -- The case "x .=> x" can hit is extremely rare, and the getAllSatResult function relies on this
    -- trick to generate constraints in the unlucky case of ui-function models.

    -- | Symbolic boolean equivalence
    infixr 1 .<=>
    (.<=>) :: SBool -> SBool -> SBool
    x :: SBool
    x .<=> :: SBool -> SBool -> SBool
    .<=> y :: SBool
    y = (SBool
    x SBool -> SBool -> SBool
    .&& SBool
    y) SBool -> SBool -> SBool
    .|| (SBool -> SBool
    sNot SBool
    x SBool -> SBool -> SBool
    .&& SBool -> SBool
    sNot SBool
    y)

    -- | Conversion from 'Bool' to 'SBool'
    fromBool :: Bool -> SBool
    fromBool :: Bool -> SBool
    fromBool True  = SBool
    sTrue
    fromBool False = SBool
    sFalse

    -- | Generalization of 'and'
    sAnd :: [SBool] -> SBool
    sAnd :: [SBool] -> SBool
    sAnd = (SBool -> SBool -> SBool) -> SBool -> [SBool] -> SBool
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr SBool -> SBool -> SBool
    (.&&) SBool
    sTrue

    -- | Generalization of 'or'
    sOr :: [SBool] -> SBool
    sOr :: [SBool] -> SBool
    sOr  = (SBool -> SBool -> SBool) -> SBool -> [SBool] -> SBool
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr SBool -> SBool -> SBool
    (.||) SBool
    sFalse

    -- | Generalization of 'any'
    sAny :: (a -> SBool) -> [a] -> SBool
    sAny :: (a -> SBool) -> [a] -> SBool
    sAny f :: a -> SBool
    f = [SBool] -> SBool
    sOr  ([SBool] -> SBool) -> ([a] -> [SBool]) -> [a] -> SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> SBool) -> [a] -> [SBool]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> SBool
    f

    -- | Generalization of 'all'
    sAll :: (a -> SBool) -> [a] -> SBool
    sAll :: (a -> SBool) -> [a] -> SBool
    sAll f :: a -> SBool
    f = [SBool] -> SBool
    sAnd ([SBool] -> SBool) -> ([a] -> [SBool]) -> [a] -> SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> SBool) -> [a] -> [SBool]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> SBool
    f

    -- | 'RoundingMode' can be used symbolically
    instance SymVal RoundingMode

    -- | The symbolic variant of 'RoundingMode'
    type SRoundingMode = SBV RoundingMode

    -- | Symbolic variant of 'RoundNearestTiesToEven'
    sRoundNearestTiesToEven :: SRoundingMode
    sRoundNearestTiesToEven :: SBV RoundingMode
    sRoundNearestTiesToEven = RoundingMode -> SBV RoundingMode
    forall a. SymVal a => a -> SBV a
    literal RoundingMode
    RoundNearestTiesToEven

    -- | Symbolic variant of 'RoundNearestTiesToAway'
    sRoundNearestTiesToAway :: SRoundingMode
    sRoundNearestTiesToAway :: SBV RoundingMode
    sRoundNearestTiesToAway = RoundingMode -> SBV RoundingMode
    forall a. SymVal a => a -> SBV a
    literal RoundingMode
    RoundNearestTiesToAway

    -- | Symbolic variant of 'RoundTowardPositive'
    sRoundTowardPositive :: SRoundingMode
    sRoundTowardPositive :: SBV RoundingMode
    sRoundTowardPositive = RoundingMode -> SBV RoundingMode
    forall a. SymVal a => a -> SBV a
    literal RoundingMode
    RoundTowardPositive

    -- | Symbolic variant of 'RoundTowardNegative'
    sRoundTowardNegative :: SRoundingMode
    sRoundTowardNegative :: SBV RoundingMode
    sRoundTowardNegative = RoundingMode -> SBV RoundingMode
    forall a. SymVal a => a -> SBV a
    literal RoundingMode
    RoundTowardNegative

    -- | Symbolic variant of 'RoundTowardZero'
    sRoundTowardZero :: SRoundingMode
    sRoundTowardZero :: SBV RoundingMode
    sRoundTowardZero = RoundingMode -> SBV RoundingMode
    forall a. SymVal a => a -> SBV a
    literal RoundingMode
    RoundTowardZero

    -- | Alias for 'sRoundNearestTiesToEven'
    sRNE :: SRoundingMode
    sRNE :: SBV RoundingMode
    sRNE = SBV RoundingMode
    sRoundNearestTiesToEven

    -- | Alias for 'sRoundNearestTiesToAway'
    sRNA :: SRoundingMode
    sRNA :: SBV RoundingMode
    sRNA = SBV RoundingMode
    sRoundNearestTiesToAway

    -- | Alias for 'sRoundTowardPositive'
    sRTP :: SRoundingMode
    sRTP :: SBV RoundingMode
    sRTP = SBV RoundingMode
    sRoundTowardPositive

    -- | Alias for 'sRoundTowardNegative'
    sRTN :: SRoundingMode
    sRTN :: SBV RoundingMode
    sRTN = SBV RoundingMode
    sRoundTowardNegative

    -- | Alias for 'sRoundTowardZero'
    sRTZ :: SRoundingMode
    sRTZ :: SBV RoundingMode
    sRTZ = SBV RoundingMode
    sRoundTowardZero

    -- | A 'Show' instance is not particularly "desirable," when the value is symbolic,
    -- but we do need this instance as otherwise we cannot simply evaluate Haskell functions
    -- that return symbolic values and have their constant values printed easily!
    instance Show (SBV a) where
      show :: SBV a -> [Char]
    show (SBV sv :: SVal
    sv) = SVal -> [Char]
    forall a. Show a => a -> [Char]
    show SVal
    sv

    -- | This instance is only defined so that we can define an instance for
    -- 'Data.Bits.Bits'. '==' and '/=' simply throw an error. Use
    -- 'Data.SBV.EqSymbolic' instead.
    instance Eq (SBV a) where
      SBV a :: SVal
    a == :: SBV a -> SBV a -> Bool
    == SBV b :: SVal
    b = SVal
    a SVal -> SVal -> Bool
    forall a. Eq a => a -> a -> Bool
    == SVal
    b
      SBV a :: SVal
    a /= :: SBV a -> SBV a -> Bool
    /= SBV b :: SVal
    b = SVal
    a SVal -> SVal -> Bool
    forall a. Eq a => a -> a -> Bool
    /= SVal
    b

    instance HasKind a => HasKind (SBV a) where
      kindOf :: SBV a -> Kind
    kindOf _ = Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a)

    -- | Convert a symbolic value to a symbolic-word
    sbvToSV :: State -> SBV a -> IO SV
    sbvToSV :: State -> SBV a -> IO SV
    sbvToSV st :: State
    st (SBV s :: SVal
    s) = State -> SVal -> IO SV
    svToSV State
    st SVal
    s

    -------------------------------------------------------------------------
    -- * Symbolic Computations
    -------------------------------------------------------------------------

    -- | Generalization of 'Data.SBV.mkSymSBV'
    mkSymSBV :: forall a m. MonadSymbolic m => Maybe Quantifier -> Kind -> Maybe String -> m (SBV a)
    mkSymSBV :: Maybe Quantifier -> Kind -> Maybe [Char] -> m (SBV a)
    mkSymSBV mbQ :: Maybe Quantifier
    mbQ k :: Kind
    k mbNm :: Maybe [Char]
    mbNm = SVal -> SBV a
    forall a. SVal -> SBV a
    SBV (SVal -> SBV a) -> m SVal -> m (SBV a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (m State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv m State -> (State -> m SVal) -> m SVal
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO SVal -> m SVal
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SVal -> m SVal) -> (State -> IO SVal) -> State -> m SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Quantifier -> Kind -> Maybe [Char] -> State -> IO SVal
    svMkSymVar Maybe Quantifier
    mbQ Kind
    k Maybe [Char]
    mbNm)

    -- | Generalization of 'Data.SBV.sbvToSymSW'
    sbvToSymSV :: MonadSymbolic m => SBV a -> m SV
    sbvToSymSV :: SBV a -> m SV
    sbvToSymSV sbv :: SBV a
    sbv = do
            State
    st <- m State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv
            IO SV -> m SV
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SV -> m SV) -> IO SV -> m SV
    forall a b. (a -> b) -> a -> b
    $ State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    sbv

    -- | Actions we can do in a context: Either at problem description
    -- time or while we are dynamically querying. 'Symbolic' and 'Query' are
    -- two instances of this class. Note that we use this mechanism
    -- internally and do not export it from SBV.
    class SolverContext m where
       -- | Add a constraint, any satisfying instance must satisfy this condition.
       constrain :: SBool -> m ()
       -- | Add a soft constraint. The solver will try to satisfy this condition if possible, but won't if it cannot.
       softConstrain :: SBool -> m ()
       -- | Add a named constraint. The name is used in unsat-core extraction.
       namedConstraint :: String -> SBool -> m ()
       -- | Add a constraint, with arbitrary attributes.
       constrainWithAttribute :: [(String, String)] -> SBool -> m ()
       -- | Set info. Example: @setInfo ":status" ["unsat"]@.
       setInfo :: String -> [String] -> m ()
       -- | Set an option.
       setOption :: SMTOption -> m ()
       -- | Set the logic.
       setLogic :: Logic -> m ()
       -- | Add a user specified axiom to the generated SMT-Lib file. The first argument is a mere
       -- string, use for commenting purposes. The second argument is intended to hold the multiple-lines
       -- of the axiom text as expressed in SMT-Lib notation. Note that we perform no checks on the axiom
       -- itself, to see whether it's actually well-formed or is sensical by any means.
       -- A separate formalization of SMT-Lib would be very useful here.
       addAxiom :: String -> [String] -> m ()
       -- | Set a solver time-out value, in milli-seconds. This function
       -- essentially translates to the SMTLib call @(set-info :timeout val)@,
       -- and your backend solver may or may not support it! The amount given
       -- is in milliseconds. Also see the function 'Data.SBV.Control.timeOut' for finer level
       -- control of time-outs, directly from SBV.
       setTimeOut :: Integer -> m ()
       -- | Get the state associated with this context
       contextState :: m State

       {-# MINIMAL constrain, softConstrain, namedConstraint, constrainWithAttribute, setOption, addAxiom, contextState #-}

       -- time-out, logic, and info are  simply options in our implementation, so default implementation suffices
       setTimeOut t :: Integer
    t = SMTOption -> m ()
    forall (m :: * -> *). SolverContext m => SMTOption -> m ()
    setOption (SMTOption -> m ()) -> SMTOption -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [[Char]] -> SMTOption
    OptionKeyword ":timeout" [Integer -> [Char]
    forall a. Show a => a -> [Char]
    show Integer
    t]
       setLogic     = SMTOption -> m ()
    forall (m :: * -> *). SolverContext m => SMTOption -> m ()
    setOption (SMTOption -> m ()) -> (Logic -> SMTOption) -> Logic -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Logic -> SMTOption
    SetLogic
       setInfo    k :: [Char]
    k = SMTOption -> m ()
    forall (m :: * -> *). SolverContext m => SMTOption -> m ()
    setOption (SMTOption -> m ()) -> ([[Char]] -> SMTOption) -> [[Char]] -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> [[Char]] -> SMTOption
    SetInfo [Char]
    k

    -- | A class representing what can be returned from a symbolic computation.
    class Outputtable a where
      -- | Generalization of 'Data.SBV.output'
      output :: MonadSymbolic m => a -> m a

    instance Outputtable (SBV a) where
      output :: SBV a -> m (SBV a)
    output i :: SBV a
    i = do
              SVal -> m ()
    forall (m :: * -> *). MonadSymbolic m => SVal -> m ()
    outputSVal (SBV a -> SVal
    forall a. SBV a -> SVal
    unSBV SBV a
    i)
              SBV a -> m (SBV a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return SBV a
    i

    instance Outputtable a => Outputtable [a] where
      output :: [a] -> m [a]
    output = (a -> m a) -> [a] -> m [a]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM a -> m a
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output

    instance Outputtable () where
      output :: () -> m ()
    output = () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return

    instance (Outputtable a, Outputtable b) => Outputtable (a, b) where
      output :: (a, b) -> m (a, b)
    output = (a -> b -> (a, b))
    -> (a -> m a) -> (b -> m b) -> (a, b) -> m (a, b)
    forall (m :: * -> *) a' b' r a b.
    Monad m =>
    (a' -> b' -> r) -> (a -> m a') -> (b -> m b') -> (a, b) -> m r
    mlift2 (,) a -> m a
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output b -> m b
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output

    instance (Outputtable a, Outputtable b, Outputtable c) => Outputtable (a, b, c) where
      output :: (a, b, c) -> m (a, b, c)
    output = (a -> b -> c -> (a, b, c))
    -> (a -> m a)
    -> (b -> m b)
    -> (c -> m c)
    -> (a, b, c)
    -> m (a, b, c)
    forall (m :: * -> *) a' b' c' r a b c.
    Monad m =>
    (a' -> b' -> c' -> r)
    -> (a -> m a') -> (b -> m b') -> (c -> m c') -> (a, b, c) -> m r
    mlift3 (,,) a -> m a
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output b -> m b
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output c -> m c
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output

    instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d) => Outputtable (a, b, c, d) where
      output :: (a, b, c, d) -> m (a, b, c, d)
    output = (a -> b -> c -> d -> (a, b, c, d))
    -> (a -> m a)
    -> (b -> m b)
    -> (c -> m c)
    -> (d -> m d)
    -> (a, b, c, d)
    -> m (a, b, c, d)
    forall (m :: * -> *) a' b' c' d' r a b c d.
    Monad m =>
    (a' -> b' -> c' -> d' -> r)
    -> (a -> m a')
    -> (b -> m b')
    -> (c -> m c')
    -> (d -> m d')
    -> (a, b, c, d)
    -> m r
    mlift4 (,,,) a -> m a
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output b -> m b
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output c -> m c
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output d -> m d
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output

    instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e) => Outputtable (a, b, c, d, e) where
      output :: (a, b, c, d, e) -> m (a, b, c, d, e)
    output = (a -> b -> c -> d -> e -> (a, b, c, d, e))
    -> (a -> m a)
    -> (b -> m b)
    -> (c -> m c)
    -> (d -> m d)
    -> (e -> m e)
    -> (a, b, c, d, e)
    -> m (a, b, c, d, e)
    forall (m :: * -> *) a' b' c' d' e' r a b c d e.
    Monad m =>
    (a' -> b' -> c' -> d' -> e' -> r)
    -> (a -> m a')
    -> (b -> m b')
    -> (c -> m c')
    -> (d -> m d')
    -> (e -> m e')
    -> (a, b, c, d, e)
    -> m r
    mlift5 (,,,,) a -> m a
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output b -> m b
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output c -> m c
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output d -> m d
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output e -> m e
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output

    instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f) => Outputtable (a, b, c, d, e, f) where
      output :: (a, b, c, d, e, f) -> m (a, b, c, d, e, f)
    output = (a -> b -> c -> d -> e -> f -> (a, b, c, d, e, f))
    -> (a -> m a)
    -> (b -> m b)
    -> (c -> m c)
    -> (d -> m d)
    -> (e -> m e)
    -> (f -> m f)
    -> (a, b, c, d, e, f)
    -> m (a, b, c, d, e, f)
    forall (m :: * -> *) a' b' c' d' e' f' r a b c d e f.
    Monad m =>
    (a' -> b' -> c' -> d' -> e' -> f' -> r)
    -> (a -> m a')
    -> (b -> m b')
    -> (c -> m c')
    -> (d -> m d')
    -> (e -> m e')
    -> (f -> m f')
    -> (a, b, c, d, e, f)
    -> m r
    mlift6 (,,,,,) a -> m a
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output b -> m b
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output c -> m c
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output d -> m d
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output e -> m e
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output f -> m f
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output

    instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f, Outputtable g) => Outputtable (a, b, c, d, e, f, g) where
      output :: (a, b, c, d, e, f, g) -> m (a, b, c, d, e, f, g)
    output = (a -> b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
    -> (a -> m a)
    -> (b -> m b)
    -> (c -> m c)
    -> (d -> m d)
    -> (e -> m e)
    -> (f -> m f)
    -> (g -> m g)
    -> (a, b, c, d, e, f, g)
    -> m (a, b, c, d, e, f, g)
    forall (m :: * -> *) a' b' c' d' e' f' g' r a b c d e f g.
    Monad m =>
    (a' -> b' -> c' -> d' -> e' -> f' -> g' -> r)
    -> (a -> m a')
    -> (b -> m b')
    -> (c -> m c')
    -> (d -> m d')
    -> (e -> m e')
    -> (f -> m f')
    -> (g -> m g')
    -> (a, b, c, d, e, f, g)
    -> m r
    mlift7 (,,,,,,) a -> m a
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output b -> m b
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output c -> m c
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output d -> m d
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output e -> m e
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output f -> m f
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output g -> m g
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output

    instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f, Outputtable g, Outputtable h) => Outputtable (a, b, c, d, e, f, g, h) where
      output :: (a, b, c, d, e, f, g, h) -> m (a, b, c, d, e, f, g, h)
    output = (a -> b -> c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
    -> (a -> m a)
    -> (b -> m b)
    -> (c -> m c)
    -> (d -> m d)
    -> (e -> m e)
    -> (f -> m f)
    -> (g -> m g)
    -> (h -> m h)
    -> (a, b, c, d, e, f, g, h)
    -> m (a, b, c, d, e, f, g, h)
    forall (m :: * -> *) a' b' c' d' e' f' g' h' r a b c d e f g h.
    Monad m =>
    (a' -> b' -> c' -> d' -> e' -> f' -> g' -> h' -> r)
    -> (a -> m a')
    -> (b -> m b')
    -> (c -> m c')
    -> (d -> m d')
    -> (e -> m e')
    -> (f -> m f')
    -> (g -> m g')
    -> (h -> m h')
    -> (a, b, c, d, e, f, g, h)
    -> m r
    mlift8 (,,,,,,,) a -> m a
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output b -> m b
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output c -> m c
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output d -> m d
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output e -> m e
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output f -> m f
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output g -> m g
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output h -> m h
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output

    -------------------------------------------------------------------------------
    -- * Symbolic Values
    -------------------------------------------------------------------------------
    -- | A 'SymVal' is a potential symbolic value that can be created instances of to be fed to a symbolic program.
    class (HasKind a, Typeable a) => SymVal a where
      -- | Generalization of 'Data.SBV.mkSymVal'
      mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV a)
      -- | Turn a literal constant to symbolic
      literal :: a -> SBV a
      -- | Extract a literal, from a CV representation
      fromCV :: CV -> a
      -- | Does it concretely satisfy the given predicate?
      isConcretely :: SBV a -> (a -> Bool) -> Bool

      -- minimal complete definition: Nothing.
      -- Giving no instances is okay when defining an uninterpreted/enumerated sort, but otherwise you really
      -- want to define: literal, fromCV, mkSymVal

      default mkSymVal :: (MonadSymbolic m, Read a, G.Data a) => Maybe Quantifier -> Maybe String -> m (SBV a)
      mkSymVal mbQ :: Maybe Quantifier
    mbQ mbNm :: Maybe [Char]
    mbNm = SVal -> SBV a
    forall a. SVal -> SBV a
    SBV (SVal -> SBV a) -> m SVal -> m (SBV a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (m State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv m State -> (State -> m SVal) -> m SVal
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO SVal -> m SVal
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SVal -> m SVal) -> (State -> IO SVal) -> State -> m SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Quantifier -> Kind -> Maybe [Char] -> State -> IO SVal
    svMkSymVar Maybe Quantifier
    mbQ Kind
    k Maybe [Char]
    mbNm)
        where -- NB.A call of the form
              --      constructUKind (Proxy @a)
              -- would be wrong here, as it would uninterpret the Proxy datatype!
              -- So, we have to use the dreaded undefined value in this case.
              k :: Kind
    k = a -> Kind
    forall a. (Read a, Data a) => a -> Kind
    constructUKind (a
    forall a. HasCallStack => a
    undefined :: a)

      default literal :: Show a => a -> SBV a
      literal x :: a
    x = let k :: Kind
    k@(KUninterpreted  _ conts :: Either [Char] [[Char]]
    conts) = a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    x
                      sx :: [Char]
    sx                          = a -> [Char]
    forall a. Show a => a -> [Char]
    show a
    x
                      mbIdx :: Maybe Int
    mbIdx = case Either [Char] [[Char]]
    conts of
                                Right xs :: [[Char]]
    xs -> [Char]
    sx [Char] -> [[Char]] -> Maybe Int
    forall a. Eq a => a -> [a] -> Maybe Int
    `elemIndex` [[Char]]
    xs
                                _        -> Maybe Int
    forall a. Maybe a
    Nothing
                  in SVal -> SBV a
    forall a. SVal -> SBV a
    SBV (SVal -> SBV a) -> SVal -> SBV a
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left (Kind -> CVal -> CV
    CV Kind
    k ((Maybe Int, [Char]) -> CVal
    CUserSort (Maybe Int
    mbIdx, [Char]
    sx))))

      default fromCV :: Read a => CV -> a
      fromCV (CV _ (CUserSort (_, s :: [Char]
    s))) = [Char] -> a
    forall a. Read a => [Char] -> a
    read [Char]
    s
      fromCV cv :: CV
    cv                        = [Char] -> a
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> a) -> [Char] -> a
    forall a b. (a -> b) -> a -> b
    $ "Cannot convert CV " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ CV -> [Char]
    forall a. Show a => a -> [Char]
    show CV
    cv [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " to kind " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> [Char]
    forall a. Show a => a -> [Char]
    show (Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a))

      isConcretely s :: SBV a
    s p :: a -> Bool
    p
        | Just i :: a
    i <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    s = a -> Bool
    p a
    i
        | Bool
    True                  = Bool
    False

      -- | Generalization of 'Data.SBV.forall'
      forall :: MonadSymbolic m => String -> m (SBV a)
      forall = Maybe Quantifier -> Maybe [Char] -> m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    Maybe Quantifier -> Maybe [Char] -> m (SBV a)
    mkSymVal (Quantifier -> Maybe Quantifier
    forall a. a -> Maybe a
    Just Quantifier
    ALL) (Maybe [Char] -> m (SBV a))
    -> ([Char] -> Maybe [Char]) -> [Char] -> m (SBV a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just

      -- | Generalization of 'Data.SBV.forall_'
      forall_ :: MonadSymbolic m => m (SBV a)
      forall_ = Maybe Quantifier -> Maybe [Char] -> m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    Maybe Quantifier -> Maybe [Char] -> m (SBV a)
    mkSymVal (Quantifier -> Maybe Quantifier
    forall a. a -> Maybe a
    Just Quantifier
    ALL) Maybe [Char]
    forall a. Maybe a
    Nothing

      -- | Generalization of 'Data.SBV.mkForallVars'
      mkForallVars :: MonadSymbolic m => Int -> m [SBV a]
      mkForallVars n :: Int
    n = (Int -> m (SBV a)) -> [Int] -> m [SBV a]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (m (SBV a) -> Int -> m (SBV a)
    forall a b. a -> b -> a
    const m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    forall_) [1 .. Int
    n]

      -- | Generalization of 'Data.SBV.exists'
      exists :: MonadSymbolic m => String -> m (SBV a)
      exists = Maybe Quantifier -> Maybe [Char] -> m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    Maybe Quantifier -> Maybe [Char] -> m (SBV a)
    mkSymVal (Quantifier -> Maybe Quantifier
    forall a. a -> Maybe a
    Just Quantifier
    EX) (Maybe [Char] -> m (SBV a))
    -> ([Char] -> Maybe [Char]) -> [Char] -> m (SBV a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just

      -- | Generalization of 'Data.SBV.exists_'
      exists_ :: MonadSymbolic m => m (SBV a)
      exists_ = Maybe Quantifier -> Maybe [Char] -> m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    Maybe Quantifier -> Maybe [Char] -> m (SBV a)
    mkSymVal (Quantifier -> Maybe Quantifier
    forall a. a -> Maybe a
    Just Quantifier
    EX) Maybe [Char]
    forall a. Maybe a
    Nothing

      -- | Generalization of 'Data.SBV.mkExistVars'
      mkExistVars :: MonadSymbolic m => Int -> m [SBV a]
      mkExistVars n :: Int
    n = (Int -> m (SBV a)) -> [Int] -> m [SBV a]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (m (SBV a) -> Int -> m (SBV a)
    forall a b. a -> b -> a
    const m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    exists_) [1 .. Int
    n]

      -- | Generalization of 'Data.SBV.free'
      free :: MonadSymbolic m => String -> m (SBV a)
      free = Maybe Quantifier -> Maybe [Char] -> m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    Maybe Quantifier -> Maybe [Char] -> m (SBV a)
    mkSymVal Maybe Quantifier
    forall a. Maybe a
    Nothing (Maybe [Char] -> m (SBV a))
    -> ([Char] -> Maybe [Char]) -> [Char] -> m (SBV a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just

      -- | Generalization of 'Data.SBV.free_'
      free_ :: MonadSymbolic m => m (SBV a)
      free_ = Maybe Quantifier -> Maybe [Char] -> m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    Maybe Quantifier -> Maybe [Char] -> m (SBV a)
    mkSymVal Maybe Quantifier
    forall a. Maybe a
    Nothing Maybe [Char]
    forall a. Maybe a
    Nothing

      -- | Generalization of 'Data.SBV.mkFreeVars'
      mkFreeVars :: MonadSymbolic m => Int -> m [SBV a]
      mkFreeVars n :: Int
    n = (Int -> m (SBV a)) -> [Int] -> m [SBV a]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (m (SBV a) -> Int -> m (SBV a)
    forall a b. a -> b -> a
    const m (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    free_) [1 .. Int
    n]

      -- | Generalization of 'Data.SBV.symbolic'
      symbolic :: MonadSymbolic m => String -> m (SBV a)
      symbolic = [Char] -> m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    [Char] -> m (SBV a)
    free

      -- | Generalization of 'Data.SBV.symbolics'
      symbolics :: MonadSymbolic m => [String] -> m [SBV a]
      symbolics = ([Char] -> m (SBV a)) -> [[Char]] -> m [SBV a]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM [Char] -> m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    [Char] -> m (SBV a)
    symbolic

      -- | Extract a literal, if the value is concrete
      unliteral :: SBV a -> Maybe a
      unliteral (SBV (SVal _ (Left c :: CV
    c))) = a -> Maybe a
    forall a. a -> Maybe a
    Just (a -> Maybe a) -> a -> Maybe a
    forall a b. (a -> b) -> a -> b
    $ CV -> a
    forall a. SymVal a => CV -> a
    fromCV CV
    c
      unliteral _                       = Maybe a
    forall a. Maybe a
    Nothing

      -- | Is the symbolic word concrete?
      isConcrete :: SBV a -> Bool
      isConcrete (SBV (SVal _ (Left _))) = Bool
    True
      isConcrete _                       = Bool
    False

      -- | Is the symbolic word really symbolic?
      isSymbolic :: SBV a -> Bool
      isSymbolic = Bool -> Bool
    not (Bool -> Bool) -> (SBV a -> Bool) -> SBV a -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBV a -> Bool
    forall a. SymVal a => SBV a -> Bool
    isConcrete

    instance (Random a, SymVal a) => Random (SBV a) where
      randomR :: (SBV a, SBV a) -> g -> (SBV a, g)
    randomR (l :: SBV a
    l, h :: SBV a
    h) g :: g
    g = case (SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    l, SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    h) of
                           (Just lb :: a
    lb, Just hb :: a
    hb) -> let (v :: a
    v, g' :: g
    g') = (a, a) -> g -> (a, g)
    forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
    randomR (a
    lb, a
    hb) g
    g in (a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal (a
    v :: a), g
    g')
                           _                  -> [Char] -> (SBV a, g)
    forall a. HasCallStack => [Char] -> a
    error "SBV.Random: Cannot generate random values with symbolic bounds"
      random :: g -> (SBV a, g)
    random         g :: g
    g = let (v :: a
    v, g' :: g
    g') = g -> (a, g)
    forall a g. (Random a, RandomGen g) => g -> (a, g)
    random g
    g in (a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal (a
    v :: a) , g
    g')

    ---------------------------------------------------------------------------------
    -- * Symbolic Arrays
    ---------------------------------------------------------------------------------

    -- | Flat arrays of symbolic values
    -- An @array a b@ is an array indexed by the type @'SBV' a@, with elements of type @'SBV' b@.
    --
    -- If a default value is supplied, then all the array elements will be initialized to this value.
    -- Otherwise, they will be left unspecified, i.e., a read from an unwritten location will produce
    -- an uninterpreted constant.
    --
    -- While it's certainly possible for user to create instances of 'SymArray', the
    -- 'SArray' and 'SFunArray' instances already provided should cover most use cases
    -- in practice. Note that there are a few differences between these two models in
    -- terms of use models:
    --
    --    * 'SArray' produces SMTLib arrays, and requires a solver that understands the
    --      array theory. 'SFunArray' is internally handled, and thus can be used with
    --      any solver. (Note that all solvers except 'Data.SBV.abc' support arrays, so this isn't
    --      a big decision factor.)
    --
    --    * For both arrays, if a default value is supplied, then reading from uninitialized
    --      cell will return that value. If the default is not given, then reading from
    --      uninitialized cells is still OK for both arrays, and will produce an uninterpreted
    --      constant in both cases.
    --
    --    * Only 'SArray' supports checking equality of arrays. (That is, checking if an entire
    --      array is equivalent to another.) 'SFunArray's cannot be checked for equality. In general,
    --      checking wholesale equality of arrays is a difficult decision problem and should be
    --      avoided if possible.
    --
    --    * Only 'SFunArray' supports compilation to C. Programs using 'SArray' will not be
    --      accepted by the C-code generator.
    --
    --    * You cannot use quickcheck on programs that contain these arrays. (Neither 'SArray'
    --      nor 'SFunArray'.)
    --
    --    * With 'SArray', SBV transfers all array-processing to the SMT-solver. So, it can generate
    --      programs more quickly, but they might end up being too hard for the solver to handle. With
    --      'SFunArray', SBV only generates code for individual elements and the array itself never
    --      shows up in the resulting SMTLib program. This puts more onus on the SBV side and might
    --      have some performance impacts, but it might generate problems that are easier for the SMT
    --      solvers to handle.
    --
    -- As a rule of thumb, try 'SArray' first. These should generate compact code. However, if
    -- the backend solver has hard time solving the generated problems, switch to
    -- 'SFunArray'. If you still have issues, please report so we can see what the problem might be!
    class SymArray array where
      -- | Generalization of 'Data.SBV.newArray_'
      newArray_      :: (MonadSymbolic m, HasKind a, HasKind b) => Maybe (SBV b) -> m (array a b)
      -- | Generalization of 'Data.SBV.newArray'
      newArray       :: (MonadSymbolic m, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (array a b)
      -- | Read the array element at @a@
      readArray      :: array a b -> SBV a -> SBV b
      -- | Update the element at @a@ to be @b@
      writeArray     :: SymVal b => array a b -> SBV a -> SBV b -> array a b
      -- | Merge two given arrays on the symbolic condition
      -- Intuitively: @mergeArrays cond a b = if cond then a else b@.
      -- Merging pushes the if-then-else choice down on to elements
      mergeArrays    :: SymVal b => SBV Bool -> array a b -> array a b -> array a b
      -- | Internal function, not exported to the user
      newArrayInState :: (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (array a b)

      {-# MINIMAL readArray, writeArray, mergeArrays, ((newArray_, newArray) | newArrayInState) #-}
      newArray_   mbVal :: Maybe (SBV b)
    mbVal = m State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv m State -> (State -> m (array a b)) -> m (array a b)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO (array a b) -> m (array a b)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (array a b) -> m (array a b))
    -> (State -> IO (array a b)) -> State -> m (array a b)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe [Char] -> Maybe (SBV b) -> State -> IO (array a b)
    forall (array :: * -> * -> *) a b.
    (SymArray array, HasKind a, HasKind b) =>
    Maybe [Char] -> Maybe (SBV b) -> State -> IO (array a b)
    newArrayInState Maybe [Char]
    forall a. Maybe a
    Nothing   Maybe (SBV b)
    mbVal
      newArray nm :: [Char]
    nm mbVal :: Maybe (SBV b)
    mbVal = m State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv m State -> (State -> m (array a b)) -> m (array a b)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO (array a b) -> m (array a b)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (array a b) -> m (array a b))
    -> (State -> IO (array a b)) -> State -> m (array a b)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe [Char] -> Maybe (SBV b) -> State -> IO (array a b)
    forall (array :: * -> * -> *) a b.
    (SymArray array, HasKind a, HasKind b) =>
    Maybe [Char] -> Maybe (SBV b) -> State -> IO (array a b)
    newArrayInState ([Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    nm) Maybe (SBV b)
    mbVal

      -- Despite our MINIMAL pragma and default implementations for newArray_ and
      -- newArray, we must provide a dummy implementation for newArrayInState:
      newArrayInState = [Char] -> Maybe [Char] -> Maybe (SBV b) -> State -> IO (array a b)
    forall a. HasCallStack => [Char] -> a
    error "undefined: newArrayInState"

    -- | Arrays implemented in terms of SMT-arrays: <http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml>
    --
    --   * Maps directly to SMT-lib arrays
    --
    --   * Reading from an unintialized value is OK. If the default value is given in 'newArray', it will
    --     be the result. Otherwise, the read yields an uninterpreted constant.
    --
    --   * Can check for equality of these arrays
    --
    --   * Cannot be used in code-generation (i.e., compilation to C)
    --
    --   * Cannot quick-check theorems using @SArray@ values
    --
    --   * Typically slower as it heavily relies on SMT-solving for the array theory
    newtype SArray a b = SArray { SArray a b -> SArr
    unSArray :: SArr }

    instance (HasKind a, HasKind b) => Show (SArray a b) where
      show :: SArray a b -> [Char]
    show SArray{} = "SArray<" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Proxy a -> [Char]
    forall a. HasKind a => a -> [Char]
    showType (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a) [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ":" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Proxy b -> [Char]
    forall a. HasKind a => a -> [Char]
    showType (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b) [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ">"

    instance SymArray SArray where
      readArray :: SArray a b -> SBV a -> SBV b
    readArray   (SArray arr :: SArr
    arr) (SBV a :: SVal
    a)               = SVal -> SBV b
    forall a. SVal -> SBV a
    SBV (SArr -> SVal -> SVal
    readSArr SArr
    arr SVal
    a)
      writeArray :: SArray a b -> SBV a -> SBV b -> SArray a b
    writeArray  (SArray arr :: SArr
    arr) (SBV a :: SVal
    a)    (SBV b :: SVal
    b)    = SArr -> SArray a b
    forall a b. SArr -> SArray a b
    SArray (SArr -> SVal -> SVal -> SArr
    writeSArr SArr
    arr SVal
    a SVal
    b)
      mergeArrays :: SBool -> SArray a b -> SArray a b -> SArray a b
    mergeArrays (SBV t :: SVal
    t)      (SArray a :: SArr
    a) (SArray b :: SArr
    b) = SArr -> SArray a b
    forall a b. SArr -> SArray a b
    SArray (SVal -> SArr -> SArr -> SArr
    mergeSArr SVal
    t SArr
    a SArr
    b)

      newArrayInState :: forall a b. (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (SArray a b)
      newArrayInState :: Maybe [Char] -> Maybe (SBV b) -> State -> IO (SArray a b)
    newArrayInState mbNm :: Maybe [Char]
    mbNm mbVal :: Maybe (SBV b)
    mbVal st :: State
    st = do (Kind -> IO ()) -> [Kind] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (State -> Kind -> IO ()
    registerKind State
    st) [Kind
    aknd, Kind
    bknd]
                                         SArr -> SArray a b
    forall a b. SArr -> SArray a b
    SArray (SArr -> SArray a b) -> IO SArr -> IO (SArray a b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> State -> (Kind, Kind) -> (Int -> [Char]) -> Maybe SVal -> IO SArr
    newSArr State
    st (Kind
    aknd, Kind
    bknd) (Maybe [Char] -> Int -> [Char]
    forall a. Show a => Maybe [Char] -> a -> [Char]
    mkNm Maybe [Char]
    mbNm) (SBV b -> SVal
    forall a. SBV a -> SVal
    unSBV (SBV b -> SVal) -> Maybe (SBV b) -> Maybe SVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (SBV b)
    mbVal)
         where mkNm :: Maybe [Char] -> a -> [Char]
    mkNm Nothing   t :: a
    t = "array_" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> [Char]
    forall a. Show a => a -> [Char]
    show a
    t
               mkNm (Just nm :: [Char]
    nm) _ = [Char]
    nm
               aknd :: Kind
    aknd = Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a)
               bknd :: Kind
    bknd = Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b)

    -- | Arrays implemented internally, without translating to SMT-Lib functions:
    --
    --   * Internally handled by the library and not mapped to SMT-Lib, hence can
    --     be used with solvers that don't support arrays. (Such as abc.)
    --
    --   * Reading from an unintialized value is OK. If the default value is given in 'newArray', it will
    --     be the result. Otherwise, the read yields an uninterpreted constant.
    --
    --   * Cannot check for equality of arrays.
    --
    --   * Can be used in code-generation (i.e., compilation to C).
    --
    --   * Can not quick-check theorems using @SFunArray@ values
    --
    --   * Typically faster as it gets compiled away during translation.
    newtype SFunArray a b = SFunArray { SFunArray a b -> SFunArr
    unSFunArray :: SFunArr }

    instance (HasKind a, HasKind b) => Show (SFunArray a b) where
      show :: SFunArray a b -> [Char]
    show SFunArray{} = "SFunArray<" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Proxy a -> [Char]
    forall a. HasKind a => a -> [Char]
    showType (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a) [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ":" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Proxy b -> [Char]
    forall a. HasKind a => a -> [Char]
    showType (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b) [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ">"

    instance SymArray SFunArray where
      readArray :: SFunArray a b -> SBV a -> SBV b
    readArray   (SFunArray arr :: SFunArr
    arr) (SBV a :: SVal
    a)             = SVal -> SBV b
    forall a. SVal -> SBV a
    SBV (SFunArr -> SVal -> SVal
    readSFunArr SFunArr
    arr SVal
    a)
      writeArray :: SFunArray a b -> SBV a -> SBV b -> SFunArray a b
    writeArray  (SFunArray arr :: SFunArr
    arr) (SBV a :: SVal
    a) (SBV b :: SVal
    b)     = SFunArr -> SFunArray a b
    forall a b. SFunArr -> SFunArray a b
    SFunArray (SFunArr -> SVal -> SVal -> SFunArr
    writeSFunArr SFunArr
    arr SVal
    a SVal
    b)
      mergeArrays :: SBool -> SFunArray a b -> SFunArray a b -> SFunArray a b
    mergeArrays (SBV t :: SVal
    t) (SFunArray a :: SFunArr
    a) (SFunArray b :: SFunArr
    b) = SFunArr -> SFunArray a b
    forall a b. SFunArr -> SFunArray a b
    SFunArray (SVal -> SFunArr -> SFunArr -> SFunArr
    mergeSFunArr SVal
    t SFunArr
    a SFunArr
    b)

      newArrayInState :: forall a b. (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (SFunArray a b)
      newArrayInState :: Maybe [Char] -> Maybe (SBV b) -> State -> IO (SFunArray a b)
    newArrayInState mbNm :: Maybe [Char]
    mbNm mbVal :: Maybe (SBV b)
    mbVal st :: State
    st = do (Kind -> IO ()) -> [Kind] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (State -> Kind -> IO ()
    registerKind State
    st) [Kind
    aknd, Kind
    bknd]
                                         SFunArr -> SFunArray a b
    forall a b. SFunArr -> SFunArray a b
    SFunArray (SFunArr -> SFunArray a b) -> IO SFunArr -> IO (SFunArray a b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> State
    -> (Kind, Kind) -> (Int -> [Char]) -> Maybe SVal -> IO SFunArr
    newSFunArr State
    st (Kind
    aknd, Kind
    bknd) (Maybe [Char] -> Int -> [Char]
    forall a. Show a => Maybe [Char] -> a -> [Char]
    mkNm Maybe [Char]
    mbNm) (SBV b -> SVal
    forall a. SBV a -> SVal
    unSBV (SBV b -> SVal) -> Maybe (SBV b) -> Maybe SVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (SBV b)
    mbVal)
        where mkNm :: Maybe [Char] -> a -> [Char]
    mkNm Nothing t :: a
    t   = "funArray_" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> [Char]
    forall a. Show a => a -> [Char]
    show a
    t
              mkNm (Just nm :: [Char]
    nm) _ = [Char]
    nm
              aknd :: Kind
    aknd = Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a)
              bknd :: Kind
    bknd = Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b)