    -----------------------------------------------------------------------------
    -- |
    -- 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 DataKinds             #-}
    {-# LANGUAGE DefaultSignatures     #-}
    {-# LANGUAGE DeriveAnyClass        #-}
    {-# LANGUAGE DeriveGeneric         #-}
    {-# LANGUAGE FlexibleContexts      #-}
    {-# LANGUAGE FlexibleInstances     #-}
    {-# LANGUAGE InstanceSigs          #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE PatternGuards         #-}
    {-# LANGUAGE ScopedTypeVariables   #-}
    {-# LANGUAGE TypeApplications      #-}
    {-# LANGUAGE TypeOperators         #-}
    {-# LANGUAGE TypeFamilies          #-}
    {-# LANGUAGE UndecidableInstances  #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Core.Data
     ( SBool, SWord8, SWord16, SWord32, SWord64
     , SInt8, SInt16, SInt32, SInt64, SInteger, SReal, SFloat, SDouble
     , SFloatingPoint, SFPHalf, SFPBFloat, SFPSingle, SFPDouble, SFPQuad
     , SRational
     , 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(..), SArray(..)
     , sbvToSV, sbvToSymSV, forceSVArg
     , SBVExpr(..), newExpr
     , cache, Cached, uncache, uncacheAI, HasKind(..)
     , Op(..), PBOp(..), FPOp(..), StrOp(..), RegExOp(..), SeqOp(..), RegExp(..), NamedSymVar(..), OvOp(..), 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(..), Constraint(..), Lambda(..), Forall(..), Exists(..), ExistsUnique(..), ForallN(..), ExistsN(..)
     , QuantifiedBool(..), EqSymbolic(..), QNot(..), Skolemize(skolemize, taggedSkolemize)
     ) where

    import GHC.TypeLits (KnownNat, Nat, Symbol, KnownSymbol, symbolVal, AppendSymbol)

    import GHC.Exts     (IsList(..))

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

    import Data.Kind (Type)
    import Data.Proxy
    import Data.Typeable          (Typeable)

    import GHC.Generics (Generic, U1(..), M1(..), (:*:)(..), K1(..), (:+:)(..))
    import qualified GHC.Generics  as G
    import qualified Data.Generics as G (Data(..))

    import qualified Data.IORef         as R    (readIORef)
    import qualified Data.IntMap.Strict as IMap (size, insert)

    import System.Random

    import Data.SBV.Core.AlgReals
    import Data.SBV.Core.SizedFloats
    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 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 State
    st 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 { forall a. 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
    $cfrom :: forall a x. SBV a -> Rep (SBV a) x
    from :: forall x. SBV a -> Rep (SBV a) x
    $cto :: forall a x. Rep (SBV a) x -> SBV a
    to :: forall x. Rep (SBV a) x -> SBV a
    Generic, SBV a -> ()
    (SBV a -> ()) -> NFData (SBV a)
    forall a. SBV a -> ()
    forall a. (a -> ()) -> NFData a
    $crnf :: forall a. SBV a -> ()
    rnf :: 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 arbitrary precision floating point value
    type SFloatingPoint (eb :: Nat) (sb :: Nat) = SBV (FloatingPoint eb sb)

    -- | A symbolic half-precision float
    type SFPHalf = SBV FPHalf

    -- | A symbolic brain-float precision float
    type SFPBFloat = SBV FPBFloat

    -- | A symbolic single-precision float
    type SFPSingle = SBV FPSingle

    -- | A symbolic double-precision float
    type SFPDouble = SBV FPDouble

    -- | A symbolic quad-precision float
    type SFPQuad = SBV FPQuad

    -- | A symbolic character. Note that this is the full unicode character set.
    -- see: <http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml>
    -- for details.
    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 rational value.
    type SRational = SBV Rational

    -- | 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 = [a] -> SList a
    [Item (SList a)] -> SList a
    forall a. SymVal a => a -> SBV a
    literal
      toList :: SList a -> [Item (SList a)]
    toList SList a
    x = [a] -> Maybe [a] -> [a]
    forall a. a -> Maybe a -> a
    fromMaybe ([Char] -> [a]
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "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 :: forall a. Floating a => a
    nan = a
    0a -> a -> a
    forall a. Fractional a => 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 :: forall a. Floating a => a
    infinity = a
    1a -> a -> a
    forall a. Fractional a => a -> a -> a
    /a
    0

    -- | Symbolic variant of Not-A-Number. This value will inhabit
    -- 'SFloat', 'SDouble' and 'SFloatingPoint'. types.
    sNaN :: (Floating a, SymVal a) => SBV a
    sNaN :: forall a. (Floating a, SymVal a) => 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
    -- 'SFloat', 'SDouble' and 'SFloatingPoint'. types.
    sInfinity :: (Floating a, SymVal a) => SBV a
    sInfinity :: forall a. (Floating a, SymVal a) => 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 SVal
    b) = SVal -> SBool
    forall a. SVal -> SBV a
    SBV (SVal -> SVal
    svNot SVal
    b)

    -- | Symbolic conjunction
    infixr 3 .&&
    (.&&) :: SBool -> SBool -> SBool
    SBV SVal
    x .&& :: SBool -> SBool -> SBool
    .&& SBV 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 SVal
    x .|| :: SBool -> SBool -> SBool
    .|| SBV 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 SVal
    x .<+> :: SBool -> SBool -> SBool
    .<+> SBV 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
    SBool
    x .~& :: SBool -> SBool -> SBool
    .~& SBool
    y = SBool -> SBool
    sNot (SBool
    x SBool -> SBool -> SBool
    .&& SBool
    y)

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

    -- | Symbolic implication
    infixr 1 .=>
    (.=>) :: SBool -> SBool -> SBool
    SBV SVal
    x .=> :: SBool -> SBool -> SBool
    .=> SBV SVal
    y = SVal -> SBool
    forall a. SVal -> SBV a
    SBV (SVal
    x SVal -> SVal -> SVal
    `svImplies` SVal
    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
    SBV SVal
    x .<=> :: SBool -> SBool -> SBool
    .<=> SBV SVal
    y = SVal -> SBool
    forall a. SVal -> SBV a
    SBV (SVal
    x SVal -> SVal -> SVal
    `svEqual` SVal
    y)

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

    -- | Generalization of 'and'
    sAnd :: [SBool] -> SBool
    sAnd :: [SBool] -> SBool
    sAnd = (SBool -> SBool -> SBool) -> SBool -> [SBool] -> SBool
    forall a b. (a -> b -> b) -> b -> [a] -> b
    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 a b. (a -> b -> b) -> b -> [a] -> b
    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 :: forall a. (a -> SBool) -> [a] -> SBool
    sAny 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 :: forall a. (a -> SBool) -> [a] -> SBool
    sAll 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 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 SVal
    a == :: SBV a -> SBV a -> Bool
    == SBV SVal
    b = SVal
    a SVal -> SVal -> Bool
    forall a. Eq a => a -> a -> Bool
    == SVal
    b
      SBV SVal
    a /= :: SBV a -> SBV a -> Bool
    /= SBV 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 SBV a
    _ = Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a)

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

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

    -- | Generalization of 'Data.SBV.mkSymSBV'
    mkSymSBV :: forall a m. MonadSymbolic m => VarContext -> Kind -> Maybe String -> m (SBV a)
    mkSymSBV :: forall a (m :: * -> *).
    MonadSymbolic m =>
    VarContext -> Kind -> Maybe [Char] -> m (SBV a)
    mkSymSBV VarContext
    vc Kind
    k 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 a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO SVal -> m SVal
    forall a. IO a -> m a
    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
    . VarContext -> Kind -> Maybe [Char] -> State -> IO SVal
    svMkSymVar VarContext
    vc Kind
    k Maybe [Char]
    mbNm)

    -- | Generalization of 'Data.SBV.sbvToSymSW'
    sbvToSymSV :: MonadSymbolic m => SBV a -> m SV
    sbvToSymSV :: forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
    sbvToSymSV SBV a
    sbv = do
            State
    st <- m State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv
            IO SV -> m SV
    forall a. IO a -> m a
    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

    -- | Values that we can turn into a constraint
    class MonadSymbolic m => Constraint m a where
      mkConstraint :: State -> a -> m ()

    -- | Base case: simple booleans
    instance MonadSymbolic m => Constraint m SBool where
      mkConstraint :: State -> SBool -> m ()
    mkConstraint State
    _ SBool
    out = m SBool -> m ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (m SBool -> m ()) -> m SBool -> m ()
    forall a b. (a -> b) -> a -> b
    $ SBool -> m SBool
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBool -> m SBool
    output SBool
    out

    -- | An existential symbolic variable, used in building quantified constraints. The name
    -- attached via the symbol is used during skolemization to create a skolem-function name
    -- when this variable is eliminated.
    newtype Exists (nm :: Symbol) a = Exists (SBV a)

    -- | An existential unique symbolic variable, used in building quantified constraints. The name
    -- attached via the symbol is used during skolemization. It's split into two extra names, suffixed
    -- @_eu1@ and @_eu2@, to name the universals in the equivalent formula:
    -- \(\exists! x\,P(x)\Leftrightarrow \exists x\,P(x) \land \forall x_{eu1} \forall x_{eu2} (P(x_{eu1}) \land P(x_{eu2}) \Rightarrow x_{eu1} = x_{eu2}) \)
    newtype ExistsUnique (nm :: Symbol) a = ExistsUnique (SBV a)

    -- | A universal symbolic variable, used in building quantified constraints. The name attached via the symbol is used
    -- during skolemization. It names the corresponding argument to the skolem-functions within the scope of this quantifier.
    newtype Forall (nm :: Symbol) a = Forall (SBV a)

    -- | Exactly @n@ existential symbolic variables, used in building quantified constraints. The name attached
    -- will be prefixed in front of @_1@, @_2@, ..., @_n@ to form the names of the variables.
    newtype ExistsN (n :: Nat) (nm :: Symbol) a = ExistsN [SBV a]

    -- | Exactly @n@ universal symbolic variables, used in in building quantified constraints. The name attached
    -- will be prefixed in front of @_1@, @_2@, ..., @_n@ to form the names of the variables.
    newtype ForallN (n :: Nat) (nm :: Symbol) a = ForallN [SBV a]

    -- | make a quantifier argument in the given state
    mkQArg :: forall m a. (HasKind a, MonadIO m) => State -> Quantifier -> m (SBV a)
    mkQArg :: forall (m :: * -> *) a.
    (HasKind a, MonadIO m) =>
    State -> Quantifier -> m (SBV a)
    mkQArg State
    st Quantifier
    q = do let k :: Kind
    k = Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a)
                     SV
    sv <- IO SV -> m SV
    forall a. IO a -> m a
    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
    $ Quantifier -> State -> Kind -> IO SV
    quantVar Quantifier
    q State
    st Kind
    k
                     SBV a -> m (SBV a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SBV a -> m (SBV a)) -> SBV a -> m (SBV a)
    forall a b. (a -> b) -> a -> b
    $ 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 (Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right ((State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache (IO SV -> State -> IO SV
    forall a b. a -> b -> a
    const (SV -> IO SV
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SV
    sv))))

    -- | Functions of a single existential
    instance (SymVal a, Constraint m r) => Constraint m (Exists nm a -> r) where
      mkConstraint :: State -> (Exists nm a -> r) -> m ()
    mkConstraint State
    st Exists nm a -> r
    fn = State -> Quantifier -> m (SBV a)
    forall (m :: * -> *) a.
    (HasKind a, MonadIO m) =>
    State -> Quantifier -> m (SBV a)
    mkQArg State
    st Quantifier
    EX m (SBV a) -> (SBV a -> m ()) -> m ()
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= State -> r -> m ()
    forall (m :: * -> *) a. Constraint m a => State -> a -> m ()
    mkConstraint State
    st (r -> m ()) -> (SBV a -> r) -> SBV a -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Exists nm a -> r
    fn (Exists nm a -> r) -> (SBV a -> Exists nm a) -> SBV a -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBV a -> Exists nm a
    forall (nm :: Symbol) a. SBV a -> Exists nm a
    Exists

    -- | Functions of a unique single existential
    instance (SymVal a, Constraint m r, EqSymbolic (SBV a), QuantifiedBool r) => Constraint m (ExistsUnique nm a -> r) where
      mkConstraint :: State -> (ExistsUnique nm a -> r) -> m ()
    mkConstraint State
    st = State
    -> (Exists nm a
        -> Forall (AppendSymbol nm "_eu1") a
        -> Forall (AppendSymbol nm "_eu2") a
        -> SBool)
    -> m ()
    forall (m :: * -> *) a. Constraint m a => State -> a -> m ()
    mkConstraint State
    st ((Exists nm a
      -> Forall (AppendSymbol nm "_eu1") a
      -> Forall (AppendSymbol nm "_eu2") a
      -> SBool)
     -> m ())
    -> ((ExistsUnique nm a -> r)
        -> Exists nm a
        -> Forall (AppendSymbol nm "_eu1") a
        -> Forall (AppendSymbol nm "_eu2") a
        -> SBool)
    -> (ExistsUnique nm a -> r)
    -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ExistsUnique nm a -> r)
    -> Exists nm a
    -> Forall (AppendSymbol nm "_eu1") a
    -> Forall (AppendSymbol nm "_eu2") a
    -> SBool
    forall b a (nm :: Symbol).
    (QuantifiedBool b, EqSymbolic (SBV a)) =>
    (ExistsUnique nm a -> b)
    -> Exists nm a
    -> Forall (AppendSymbol nm "_eu1") a
    -> Forall (AppendSymbol nm "_eu2") a
    -> SBool
    rewriteExistsUnique

    -- | Functions of a number of existentials
    instance (KnownNat n, SymVal a, Constraint m r) => Constraint m (ExistsN n nm a -> r) where
      mkConstraint :: State -> (ExistsN n nm a -> r) -> m ()
    mkConstraint State
    st ExistsN n nm a -> r
    fn = Int -> m (SBV a) -> m [SBV a]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM (Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n)) (State -> Quantifier -> m (SBV a)
    forall (m :: * -> *) a.
    (HasKind a, MonadIO m) =>
    State -> Quantifier -> m (SBV a)
    mkQArg State
    st Quantifier
    EX) m [SBV a] -> ([SBV a] -> m ()) -> m ()
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= State -> r -> m ()
    forall (m :: * -> *) a. Constraint m a => State -> a -> m ()
    mkConstraint State
    st (r -> m ()) -> ([SBV a] -> r) -> [SBV a] -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ExistsN n nm a -> r
    fn (ExistsN n nm a -> r)
    -> ([SBV a] -> ExistsN n nm a) -> [SBV a] -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [SBV a] -> ExistsN n nm a
    forall (n :: Nat) (nm :: Symbol) a. [SBV a] -> ExistsN n nm a
    ExistsN

    -- | Functions of a single universal
    instance (SymVal a, Constraint m r) => Constraint m (Forall nm a -> r) where
      mkConstraint :: State -> (Forall nm a -> r) -> m ()
    mkConstraint State
    st Forall nm a -> r
    fn = State -> Quantifier -> m (SBV a)
    forall (m :: * -> *) a.
    (HasKind a, MonadIO m) =>
    State -> Quantifier -> m (SBV a)
    mkQArg State
    st Quantifier
    ALL m (SBV a) -> (SBV a -> m ()) -> m ()
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= State -> r -> m ()
    forall (m :: * -> *) a. Constraint m a => State -> a -> m ()
    mkConstraint State
    st (r -> m ()) -> (SBV a -> r) -> SBV a -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Forall nm a -> r
    fn (Forall nm a -> r) -> (SBV a -> Forall nm a) -> SBV a -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBV a -> Forall nm a
    forall (nm :: Symbol) a. SBV a -> Forall nm a
    Forall

    -- | Functions of a number of universals
    instance (KnownNat n, SymVal a, Constraint m r) => Constraint m (ForallN n nm a -> r) where
      mkConstraint :: State -> (ForallN n nm a -> r) -> m ()
    mkConstraint State
    st ForallN n nm a -> r
    fn = Int -> m (SBV a) -> m [SBV a]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM (Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n)) (State -> Quantifier -> m (SBV a)
    forall (m :: * -> *) a.
    (HasKind a, MonadIO m) =>
    State -> Quantifier -> m (SBV a)
    mkQArg State
    st Quantifier
    ALL) m [SBV a] -> ([SBV a] -> m ()) -> m ()
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= State -> r -> m ()
    forall (m :: * -> *) a. Constraint m a => State -> a -> m ()
    mkConstraint State
    st (r -> m ()) -> ([SBV a] -> r) -> [SBV a] -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ForallN n nm a -> r
    fn (ForallN n nm a -> r)
    -> ([SBV a] -> ForallN n nm a) -> [SBV a] -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [SBV a] -> ForallN n nm a
    forall (n :: Nat) (nm :: Symbol) a. [SBV a] -> ForallN n nm a
    ForallN

    -- | Values that we can turn into a lambda abstraction
    class MonadSymbolic m => Lambda m a where
      mkLambda :: State -> a -> m ()

    -- | Base case, simple values
    instance MonadSymbolic m => Lambda m (SBV a) where
      mkLambda :: State -> SBV a -> m ()
    mkLambda State
    _ SBV a
    out = m (SBV a) -> m ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (m (SBV a) -> m ()) -> m (SBV a) -> m ()
    forall a b. (a -> b) -> a -> b
    $ SBV a -> m (SBV a)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV a -> m (SBV a)
    output SBV a
    out

    -- | Functions
    instance (SymVal a, Lambda m r) => Lambda m (SBV a -> r) where
      mkLambda :: State -> (SBV a -> r) -> m ()
    mkLambda State
    st SBV a -> r
    fn = m (SBV a)
    mkArg m (SBV a) -> (SBV a -> m ()) -> m ()
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= State -> r -> m ()
    forall (m :: * -> *) a. Lambda m a => State -> a -> m ()
    mkLambda State
    st (r -> m ()) -> (SBV a -> r) -> SBV a -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBV a -> r
    fn
        where mkArg :: m (SBV a)
    mkArg = do let k :: Kind
    k = Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a)
                         SV
    sv <- IO SV -> m SV
    forall a. IO a -> m a
    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 -> Kind -> IO SV
    lambdaVar State
    st Kind
    k
                         SBV a -> m (SBV a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SBV a -> m (SBV a)) -> SBV a -> m (SBV a)
    forall a b. (a -> b) -> a -> b
    $ 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 (Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right ((State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache (IO SV -> State -> IO SV
    forall a b. a -> b -> a
    const (SV -> IO SV
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SV
    sv))))

    -- | A value that can be used as a quantified boolean
    class QuantifiedBool a where
      -- | Turn a quantified boolean into a regular boolean. That is, this function turns an exists/forall quantified
      -- formula to a simple boolean that can be used as a regular boolean value. An example is:
      --
      -- @
      --   quantifiedBool $ \\(Forall x) (Exists y) -> y .> (x :: SInteger)
      -- @
      --
      -- is equivalent to `sTrue`. You can think of this function as performing quantifier-elimination: It takes
      -- a quantified formula, and reduces it to a simple boolean that is equivalent to it, but has no quantifiers.
      quantifiedBool :: a -> SBool

    -- | Base case of quantification, simple booleans
    instance {-# OVERLAPPING #-} QuantifiedBool SBool where
      quantifiedBool :: SBool -> SBool
    quantifiedBool = SBool -> SBool
    forall a. a -> a
    id

    -- | 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 :: QuantifiedBool a => a -> m ()

       -- | Add a soft constraint. The solver will try to satisfy this condition if possible, but won't if it cannot.
       softConstrain :: QuantifiedBool a => a -> m ()

       -- | Add a named constraint. The name is used in unsat-core extraction.
       namedConstraint :: QuantifiedBool a => String -> a -> m ()

       -- | Add a constraint, with arbitrary attributes.
       constrainWithAttribute :: QuantifiedBool a => [(String, String)] -> a -> m ()

       -- | Set info. Example: @setInfo ":status" ["unsat"]@.
       setInfo :: String -> [String] -> m ()

       -- | Set an option.
       setOption :: SMTOption -> m ()

       -- | Set the logic.
       setLogic :: Logic -> 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, contextState #-}

       -- time-out, logic, and info are  simply options in our implementation, so default implementation suffices
       setTimeOut 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 [Char]
    ":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    [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 :: forall (m :: * -> *). MonadSymbolic m => SBV a -> m (SBV a)
    output 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 a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SBV a
    i

    instance Outputtable a => Outputtable [a] where
      output :: forall (m :: * -> *). MonadSymbolic m => [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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM a -> m a
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => a -> m a
    output

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

    instance (Outputtable a, Outputtable b) => Outputtable (a, b) where
      output :: forall (m :: * -> *). MonadSymbolic m => (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
    forall (m :: * -> *). MonadSymbolic m => a -> m a
    output b -> m b
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => b -> m b
    output

    instance (Outputtable a, Outputtable b, Outputtable c) => Outputtable (a, b, c) where
      output :: forall (m :: * -> *). MonadSymbolic m => (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
    forall (m :: * -> *). MonadSymbolic m => a -> m a
    output b -> m b
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => b -> m b
    output c -> m c
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => c -> m c
    output

    instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d) => Outputtable (a, b, c, d) where
      output :: forall (m :: * -> *).
    MonadSymbolic m =>
    (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
    forall (m :: * -> *). MonadSymbolic m => a -> m a
    output b -> m b
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => b -> m b
    output c -> m c
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => c -> m c
    output d -> m d
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => d -> m d
    output

    instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e) => Outputtable (a, b, c, d, e) where
      output :: forall (m :: * -> *).
    MonadSymbolic m =>
    (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
    forall (m :: * -> *). MonadSymbolic m => a -> m a
    output b -> m b
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => b -> m b
    output c -> m c
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => c -> m c
    output d -> m d
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => d -> m d
    output e -> m e
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => e -> m e
    output

    instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f) => Outputtable (a, b, c, d, e, f) where
      output :: forall (m :: * -> *).
    MonadSymbolic m =>
    (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
    forall (m :: * -> *). MonadSymbolic m => a -> m a
    output b -> m b
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => b -> m b
    output c -> m c
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => c -> m c
    output d -> m d
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => d -> m d
    output e -> m e
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => e -> m e
    output f -> m f
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => f -> m f
    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 :: forall (m :: * -> *).
    MonadSymbolic m =>
    (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
    forall (m :: * -> *). MonadSymbolic m => a -> m a
    output b -> m b
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => b -> m b
    output c -> m c
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => c -> m c
    output d -> m d
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => d -> m d
    output e -> m e
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => e -> m e
    output f -> m f
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => f -> m f
    output g -> m g
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => g -> m g
    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 :: forall (m :: * -> *).
    MonadSymbolic m =>
    (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
    forall (m :: * -> *). MonadSymbolic m => a -> m a
    output b -> m b
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => b -> m b
    output c -> m c
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => c -> m c
    output d -> m d
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => d -> m d
    output e -> m e
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => e -> m e
    output f -> m f
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => f -> m f
    output g -> m g
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => g -> m g
    output h -> m h
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => h -> m h
    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 => VarContext -> 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) => VarContext -> Maybe String -> m (SBV a)
      mkSymVal VarContext
    vc 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 a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO SVal -> m SVal
    forall a. IO a -> m a
    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
    . VarContext -> Kind -> Maybe [Char] -> State -> IO SVal
    svMkSymVar VarContext
    vc 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 a
    x = let k :: Kind
    k  = 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
                      conts :: Maybe [[Char]]
    conts = case Kind
    k of
                               KUserSort [Char]
    _ Maybe [[Char]]
    cts -> Maybe [[Char]]
    cts
                               Kind
    _               -> Maybe [[Char]]
    forall a. Maybe a
    Nothing
                      mbIdx :: Maybe Int
    mbIdx = case Maybe [[Char]]
    conts of
                                Just [[Char]]
    xs -> [Char]
    sx [Char] -> [[Char]] -> Maybe Int
    forall a. Eq a => a -> [a] -> Maybe Int
    `elemIndex` [[Char]]
    xs
                                Maybe [[Char]]
    Nothing -> 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 Kind
    _ (CUserSort (Maybe Int
    _, [Char]
    s))) = [Char] -> a
    forall a. Read a => [Char] -> a
    read [Char]
    s
      fromCV CV
    cv                        = [Char] -> a
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> a) -> [Char] -> a
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "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]
    ++ [Char]
    " 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 (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a))

      isConcretely SBV a
    s a -> Bool
    p
        | Just 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.free'
      free :: MonadSymbolic m => String -> m (SBV a)
      free = VarContext -> Maybe [Char] -> m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    VarContext -> Maybe [Char] -> m (SBV a)
    forall (m :: * -> *).
    MonadSymbolic m =>
    VarContext -> Maybe [Char] -> m (SBV a)
    mkSymVal (Maybe Quantifier -> VarContext
    NonQueryVar 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_ = VarContext -> Maybe [Char] -> m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    VarContext -> Maybe [Char] -> m (SBV a)
    forall (m :: * -> *).
    MonadSymbolic m =>
    VarContext -> Maybe [Char] -> m (SBV a)
    mkSymVal (Maybe Quantifier -> VarContext
    NonQueryVar 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 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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 (m :: * -> *). MonadSymbolic m => m (SBV a)
    free_) [Int
    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)
    forall (m :: * -> *). 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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM [Char] -> m (SBV a)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    [Char] -> m (SBV a)
    forall (m :: * -> *). MonadSymbolic m => [Char] -> m (SBV a)
    symbolic

      -- | Extract a literal, if the value is concrete
      unliteral :: SBV a -> Maybe a
      unliteral (SBV (SVal Kind
    _ (Left 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 SBV a
    _                       = Maybe a
    forall a. Maybe a
    Nothing

      -- | Is the symbolic word concrete?
      isConcrete :: SBV a -> Bool
      isConcrete (SBV (SVal Kind
    _ (Left CV
    _))) = Bool
    True
      isConcrete SBV a
    _                       = 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 :: forall g. RandomGen g => (SBV a, SBV a) -> g -> (SBV a, g)
    randomR (SBV a
    l, SBV a
    h) 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 a
    lb, Just a
    hb) -> let (a
    v, g
    g') = (a, a) -> g -> (a, g)
    forall g. RandomGen 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')
                           (Maybe a, Maybe a)
    _                  -> [Char] -> (SBV a, g)
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "SBV.Random: Cannot generate random values with symbolic bounds"
      random :: forall g. RandomGen g => g -> (SBV a, g)
    random         g
    g = let (a
    v, g
    g') = g -> (a, g)
    forall g. RandomGen 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
    ---------------------------------------------------------------------------------

    -- | 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.
    --
    -- The reason for this class is rather historic. In the past, SBV provided two different kinds of
    -- arrays: an `SArray` abstraction that mapped directly to SMTLib arrays  (which is still available
    -- today), and a functional notion of arrays that used internal caching, called @SFunArray@. The latter
    -- has been removed as the code turned out to be rather tricky and hard to maintain; so we only
    -- have one instance of this class. But end users can add their own instances, if needed.
    --
    -- NB. 'sListArray' insists on a concrete initializer, because not having one would break
    -- referential transparency. See https://github.com/LeventErkok/sbv/issues/553 for details.
    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)

      -- | Create a literal array
      sListArray :: (HasKind a, SymVal b) => b -> [(SBV a, SBV b)] -> 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 -> Either (Maybe (SBV b)) String -> State -> IO (array a b)

      {-# MINIMAL readArray, writeArray, mergeArrays, ((newArray_, newArray) | newArrayInState), sListArray #-}
      newArray_   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 a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO (array a b) -> m (array a b)
    forall a. IO a -> m a
    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]
    -> Either (Maybe (SBV b)) [Char] -> State -> IO (array a b)
    forall a b.
    (HasKind a, HasKind b) =>
    Maybe [Char]
    -> Either (Maybe (SBV b)) [Char] -> State -> IO (array a b)
    forall (array :: * -> * -> *) a b.
    (SymArray array, HasKind a, HasKind b) =>
    Maybe [Char]
    -> Either (Maybe (SBV b)) [Char] -> State -> IO (array a b)
    newArrayInState Maybe [Char]
    forall a. Maybe a
    Nothing   (Maybe (SBV b) -> Either (Maybe (SBV b)) [Char]
    forall a b. a -> Either a b
    Left Maybe (SBV b)
    mbVal)
      newArray [Char]
    nm 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 a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO (array a b) -> m (array a b)
    forall a. IO a -> m a
    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]
    -> Either (Maybe (SBV b)) [Char] -> State -> IO (array a b)
    forall a b.
    (HasKind a, HasKind b) =>
    Maybe [Char]
    -> Either (Maybe (SBV b)) [Char] -> State -> IO (array a b)
    forall (array :: * -> * -> *) a b.
    (SymArray array, HasKind a, HasKind b) =>
    Maybe [Char]
    -> Either (Maybe (SBV b)) [Char] -> State -> IO (array a b)
    newArrayInState ([Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    nm) (Maybe (SBV b) -> Either (Maybe (SBV b)) [Char]
    forall a b. a -> Either a b
    Left 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]
    -> Either (Maybe (SBV b)) [Char]
    -> State
    -> IO (array a b)
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "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 uninitialized 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
    newtype SArray a b = SArray { forall a b. SArray a b -> SArr
    unSArray :: SArr }

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

    instance SymArray SArray where
      readArray :: forall a b. SArray a b -> SBV a -> SBV b
    readArray   (SArray SArr
    arr) (SBV SVal
    a)               = SVal -> SBV b
    forall a. SVal -> SBV a
    SBV (SArr -> SVal -> SVal
    readSArr SArr
    arr SVal
    a)
      writeArray :: forall b a. SymVal b => SArray a b -> SBV a -> SBV b -> SArray a b
    writeArray  (SArray SArr
    arr) (SBV SVal
    a)    (SBV 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 :: forall b a.
    SymVal b =>
    SBool -> SArray a b -> SArray a b -> SArray a b
    mergeArrays (SBV SVal
    t)      (SArray SArr
    a) (SArray 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)

      sListArray :: forall a b. (HasKind a, SymVal b) => b -> [(SBV a, SBV b)] -> SArray a b
      sListArray :: forall a b.
    (HasKind a, SymVal b) =>
    b -> [(SBV a, SBV b)] -> SArray a b
    sListArray b
    initializer = (SArray a b -> (SBV a, SBV b) -> SArray a b)
    -> SArray a b -> [(SBV a, SBV b)] -> SArray a b
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl ((SBV a -> SBV b -> SArray a b) -> (SBV a, SBV b) -> SArray a b
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry ((SBV a -> SBV b -> SArray a b) -> (SBV a, SBV b) -> SArray a b)
    -> (SArray a b -> SBV a -> SBV b -> SArray a b)
    -> SArray a b
    -> (SBV a, SBV b)
    -> SArray a b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SArray a b -> SBV a -> SBV b -> SArray a b
    forall b a. SymVal b => SArray a b -> SBV a -> SBV b -> SArray a b
    forall (array :: * -> * -> *) b a.
    (SymArray array, SymVal b) =>
    array a b -> SBV a -> SBV b -> array a b
    writeArray) SArray a b
    arr
        where arr :: SArray a b
    arr = SArr -> SArray a b
    forall a b. SArr -> SArray a b
    SArray (SArr -> SArray a b) -> SArr -> SArray a b
    forall a b. (a -> b) -> a -> b
    $ (Kind, Kind) -> Cached ArrayIndex -> SArr
    SArr (Kind, Kind)
    ks (Cached ArrayIndex -> SArr) -> Cached ArrayIndex -> SArr
    forall a b. (a -> b) -> a -> b
    $ (State -> IO ArrayIndex) -> Cached ArrayIndex
    forall a. (State -> IO a) -> Cached a
    cache State -> IO ArrayIndex
    r
               where ks :: (Kind, Kind)
    ks   = (Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @b))
                     r :: State -> IO ArrayIndex
    r State
    st = do ArrayMap
    amap <- IORef ArrayMap -> IO ArrayMap
    forall a. IORef a -> IO a
    R.readIORef (State -> IORef ArrayMap
    rArrayMap State
    st)

                               let k :: ArrayIndex
    k    = Int -> ArrayIndex
    ArrayIndex (Int -> ArrayIndex) -> Int -> ArrayIndex
    forall a b. (a -> b) -> a -> b
    $ ArrayMap -> Int
    forall a. IntMap a -> Int
    IMap.size ArrayMap
    amap
                                   iVal :: SBV b
    iVal = b -> SBV b
    forall a. SymVal a => a -> SBV a
    literal b
    initializer

                               SV
    iSV <- State -> SBV b -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV b
    iVal

                               let upd :: ArrayMap -> ArrayMap
    upd  = Int -> ([Char], (Kind, Kind), ArrayContext) -> ArrayMap -> ArrayMap
    forall a. Int -> a -> IntMap a -> IntMap a
    IMap.insert (ArrayIndex -> Int
    unArrayIndex ArrayIndex
    k) ([Char]
    "array_" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ArrayIndex -> [Char]
    forall a. Show a => a -> [Char]
    show ArrayIndex
    k, (Kind, Kind)
    ks, Either (Maybe SV) [Char] -> ArrayContext
    ArrayFree (Maybe SV -> Either (Maybe SV) [Char]
    forall a b. a -> Either a b
    Left (SV -> Maybe SV
    forall a. a -> Maybe a
    Just SV
    iSV)))

                               ArrayIndex
    k ArrayIndex -> IO () -> IO ()
    forall a b. a -> b -> b
    `seq` State
    -> (State -> IORef ArrayMap)
    -> (ArrayMap -> ArrayMap)
    -> IO ()
    -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef ArrayMap
    rArrayMap ArrayMap -> ArrayMap
    upd (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ State
    -> (IncState -> IORef ArrayMap) -> (ArrayMap -> ArrayMap) -> IO ()
    forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
    modifyIncState State
    st IncState -> IORef ArrayMap
    rNewArrs ArrayMap -> ArrayMap
    upd
                               ArrayIndex -> IO ArrayIndex
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ArrayIndex
    k

      newArrayInState :: forall a b. (HasKind a, HasKind b) => Maybe String -> Either (Maybe (SBV b)) String -> State -> IO (SArray a b)
      newArrayInState :: forall a b.
    (HasKind a, HasKind b) =>
    Maybe [Char]
    -> Either (Maybe (SBV b)) [Char] -> State -> IO (SArray a b)
    newArrayInState Maybe [Char]
    mbNm Either (Maybe (SBV b)) [Char]
    eiVal 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])
    -> Either (Maybe SVal) [Char]
    -> 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) ((Maybe (SBV b) -> Either (Maybe SVal) [Char])
    -> ([Char] -> Either (Maybe SVal) [Char])
    -> Either (Maybe (SBV b)) [Char]
    -> Either (Maybe SVal) [Char]
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either (Maybe SVal -> Either (Maybe SVal) [Char]
    forall a b. a -> Either a b
    Left (Maybe SVal -> Either (Maybe SVal) [Char])
    -> (Maybe (SBV b) -> Maybe SVal)
    -> Maybe (SBV b)
    -> Either (Maybe SVal) [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (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
    <$>)) [Char] -> Either (Maybe SVal) [Char]
    forall a b. b -> Either a b
    Right Either (Maybe (SBV b)) [Char]
    eiVal)
         where mkNm :: Maybe [Char] -> a -> [Char]
    mkNm Maybe [Char]
    Nothing   a
    t = [Char]
    "array_" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> [Char]
    forall a. Show a => a -> [Char]
    show a
    t
               mkNm (Just [Char]
    nm) a
    _ = [Char]
    nm
               aknd :: Kind
    aknd = Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a)
               bknd :: Kind
    bknd = Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @b)

    -- | Symbolic Equality. Note that we can't use Haskell's 'Eq' class since Haskell insists on returning Bool
    -- Comparing symbolic values will necessarily return a symbolic value.
    --
    -- Minimal complete definition: None, if the type is instance of @Generic@. Otherwise '(.==)'.
    infix 4 .==, ./=, .===, ./==
    class EqSymbolic a where
      -- | Symbolic equality.
      (.==) :: a -> a -> SBool
      -- | Symbolic inequality.
      (./=) :: a -> a -> SBool
      -- | Strong equality. On floats ('SFloat'/'SDouble'), strong equality is object equality; that
      -- is @NaN == NaN@ holds, but @+0 == -0@ doesn't. On other types, (.===) is simply (.==).
      -- Note that (.==) is the /right/ notion of equality for floats per IEEE754 specs, since by
      -- definition @+0 == -0@ and @NaN@ equals no other value including itself. But occasionally
      -- we want to be stronger and state @NaN@ equals @NaN@ and @+0@ and @-0@ are different from
      -- each other. In a context where your type is concrete, simply use `Data.SBV.fpIsEqualObject`. But in
      -- a polymorphic context, use the strong equality instead.
      --
      -- NB. If you do not care about or work with floats, simply use (.==) and (./=).
      (.===) :: a -> a -> SBool
      -- | Negation of strong equality. Equaivalent to negation of (.===) on all types.
      (./==) :: a -> a -> SBool

      -- | Returns (symbolic) 'sTrue' if all the elements of the given list are different.
      distinct :: [a] -> SBool

      -- | Returns (symbolic) `sTrue` if all the elements of the given list are different. The second
      -- list contains exceptions, i.e., if an element belongs to that set, it will be considered
      -- distinct regardless of repetition.
      distinctExcept :: [a] -> [a] -> SBool

      -- | Returns (symbolic) 'sTrue' if all the elements of the given list are the same.
      allEqual :: [a] -> SBool

      -- | Symbolic membership test.
      sElem    :: a -> [a] -> SBool

      -- | Symbolic negated membership test.
      sNotElem :: a -> [a] -> SBool

      a
    x ./=  a
    y = SBool -> SBool
    sNot (a
    x a -> a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .==  a
    y)
      a
    x .=== a
    y = a
    x a -> a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== a
    y
      a
    x ./== a
    y = SBool -> SBool
    sNot (a
    x a -> a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .=== a
    y)

      allEqual []     = SBool
    sTrue
      allEqual (a
    x:[a]
    xs) = (a -> SBool) -> [a] -> SBool
    forall a. (a -> SBool) -> [a] -> SBool
    sAll (a
    x a -> a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .==) [a]
    xs

      -- Default implementation of 'distinct'. Note that we override
      -- this method for the base types to generate better code.
      distinct []     = SBool
    sTrue
      distinct (a
    x:[a]
    xs) = (a -> SBool) -> [a] -> SBool
    forall a. (a -> SBool) -> [a] -> SBool
    sAll (a
    x a -> a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./=) [a]
    xs SBool -> SBool -> SBool
    .&& [a] -> SBool
    forall a. EqSymbolic a => [a] -> SBool
    distinct [a]
    xs

      -- Default implementation of 'distinctExcept'. Note that we override
      -- this method for the base types to generate better code.
      distinctExcept [a]
    es [a]
    ignored = [a] -> SBool
    go [a]
    es
        where isIgnored :: a -> SBool
    isIgnored = (a -> [a] -> SBool
    forall a. EqSymbolic a => a -> [a] -> SBool
    `sElem` [a]
    ignored)

              go :: [a] -> SBool
    go []     = SBool
    sTrue
              go (a
    x:[a]
    xs) = let xOK :: SBool
    xOK  = a -> SBool
    isIgnored a
    x SBool -> SBool -> SBool
    .|| (a -> SBool) -> [a] -> SBool
    forall a. (a -> SBool) -> [a] -> SBool
    sAll (\a
    y -> a -> SBool
    isIgnored a
    y SBool -> SBool -> SBool
    .|| a
    x a -> a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./= a
    y) [a]
    xs
                          in SBool
    xOK SBool -> SBool -> SBool
    .&& [a] -> SBool
    go [a]
    xs

      a
    x `sElem`    [a]
    xs = (a -> SBool) -> [a] -> SBool
    forall a. (a -> SBool) -> [a] -> SBool
    sAny (a -> a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== a
    x) [a]
    xs
      a
    x `sNotElem` [a]
    xs = SBool -> SBool
    sNot (a
    x a -> [a] -> SBool
    forall a. EqSymbolic a => a -> [a] -> SBool
    `sElem` [a]
    xs)

      -- Default implementation for '(.==)' if the type is 'Generic'
      default (.==) :: (G.Generic a, GEqSymbolic (G.Rep a)) => a -> a -> SBool
      (.==) = a -> a -> SBool
    forall a. (Generic a, GEqSymbolic (Rep a)) => a -> a -> SBool
    symbolicEqDefault

    -- | Default implementation of symbolic equality, when the underlying type is generic
    -- Not exported, used with automatic deriving.
    symbolicEqDefault :: (G.Generic a, GEqSymbolic (G.Rep a)) => a -> a -> SBool
    symbolicEqDefault :: forall a. (Generic a, GEqSymbolic (Rep a)) => a -> a -> SBool
    symbolicEqDefault a
    x a
    y = Rep a Any -> Rep a Any -> SBool
    forall a. Rep a a -> Rep a a -> SBool
    forall (f :: * -> *) a. GEqSymbolic f => f a -> f a -> SBool
    symbolicEq (a -> Rep a Any
    forall x. a -> Rep a x
    forall a x. Generic a => a -> Rep a x
    G.from a
    x) (a -> Rep a Any
    forall x. a -> Rep a x
    forall a x. Generic a => a -> Rep a x
    G.from a
    y)

    -- | Not exported, used for implementing generic equality.
    class GEqSymbolic f where
      symbolicEq :: f a -> f a -> SBool

    {-
     - N.B. A V1 instance like the below would be wrong!
     - Why? Because in SBV, we use empty data to mean "uninterpreted" sort; not
     - something that has no constructors. Perhaps that was a bad design
     - decision. So, do not allow equality checking of such values.
    instance GEqSymbolic V1 where
      symbolicEq _ _ = sTrue
    -}

    instance GEqSymbolic U1 where
      symbolicEq :: forall a. U1 a -> U1 a -> SBool
    symbolicEq U1 a
    _ U1 a
    _ = SBool
    sTrue

    instance (EqSymbolic c) => GEqSymbolic (K1 i c) where
      symbolicEq :: forall a. K1 i c a -> K1 i c a -> SBool
    symbolicEq (K1 c
    x) (K1 c
    y) = c
    x c -> c -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== c
    y

    instance (GEqSymbolic f) => GEqSymbolic (M1 i c f) where
      symbolicEq :: forall a. M1 i c f a -> M1 i c f a -> SBool
    symbolicEq (M1 f a
    x) (M1 f a
    y) = f a -> f a -> SBool
    forall a. f a -> f a -> SBool
    forall (f :: * -> *) a. GEqSymbolic f => f a -> f a -> SBool
    symbolicEq f a
    x f a
    y

    instance (GEqSymbolic f, GEqSymbolic g) => GEqSymbolic (f :*: g) where
      symbolicEq :: forall a. (:*:) f g a -> (:*:) f g a -> SBool
    symbolicEq (f a
    x1 :*: g a
    y1) (f a
    x2 :*: g a
    y2) = f a -> f a -> SBool
    forall a. f a -> f a -> SBool
    forall (f :: * -> *) a. GEqSymbolic f => f a -> f a -> SBool
    symbolicEq f a
    x1 f a
    x2 SBool -> SBool -> SBool
    .&& g a -> g a -> SBool
    forall a. g a -> g a -> SBool
    forall (f :: * -> *) a. GEqSymbolic f => f a -> f a -> SBool
    symbolicEq g a
    y1 g a
    y2

    instance (GEqSymbolic f, GEqSymbolic g) => GEqSymbolic (f :+: g) where
      symbolicEq :: forall a. (:+:) f g a -> (:+:) f g a -> SBool
    symbolicEq (L1 f a
    l) (L1 f a
    r) = f a -> f a -> SBool
    forall a. f a -> f a -> SBool
    forall (f :: * -> *) a. GEqSymbolic f => f a -> f a -> SBool
    symbolicEq f a
    l f a
    r
      symbolicEq (R1 g a
    l) (R1 g a
    r) = g a -> g a -> SBool
    forall a. g a -> g a -> SBool
    forall (f :: * -> *) a. GEqSymbolic f => f a -> f a -> SBool
    symbolicEq g a
    l g a
    r
      symbolicEq (L1 f a
    _) (R1 g a
    _) = SBool
    sFalse
      symbolicEq (R1 g a
    _) (L1 f a
    _) = SBool
    sFalse

    -- | A class of values that can be skolemized. Note that we don't export this class. Use
    -- the 'skolemize' function instead.
    class Skolemize a where
      type SkolemsTo a :: Type
      skolem :: String -> [(SVal, String)] -> a -> SkolemsTo a

      -- | Skolemization. For any formula, skolemization gives back an equisatisfiable formula that
      -- has no existential quantifiers in it. You have to provide enough names for all the
      -- existentials in the argument. (Extras OK, so you can pass an infinite list if you like.)
      -- The names should be distinct, and also different from any other uninterpreted name
      -- you might have elsewhere.
      skolemize :: (Constraint Symbolic (SkolemsTo a), Skolemize a) => a -> SkolemsTo a
      skolemize = [Char] -> [(SVal, [Char])] -> a -> SkolemsTo a
    forall a.
    Skolemize a =>
    [Char] -> [(SVal, [Char])] -> a -> SkolemsTo a
    skolem [Char]
    "" []

      -- | If you use the same names for skolemized arguments in different functions, they will
      -- collide; which is undesirable. Unfortunately there's no easy way for SBV to detect this.
      -- In such cases, use 'taggedSkolemize' to add a scope to the skolem-function names generated.
      taggedSkolemize :: (Constraint Symbolic (SkolemsTo a), Skolemize a) => String -> a -> SkolemsTo a
      taggedSkolemize [Char]
    scope = [Char] -> [(SVal, [Char])] -> a -> SkolemsTo a
    forall a.
    Skolemize a =>
    [Char] -> [(SVal, [Char])] -> a -> SkolemsTo a
    skolem ([Char]
    scope [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "_") []

    -- | Base case; pure symbolic values
    instance Skolemize (SBV a) where
      type SkolemsTo (SBV a) = SBV a
      skolem :: [Char] -> [(SVal, [Char])] -> SBV a -> SkolemsTo (SBV a)
    skolem [Char]
    _ [(SVal, [Char])]
    _ = SBV a -> SkolemsTo (SBV a)
    SBV a -> SBV a
    forall a. a -> a
    id

    -- | Skolemize over a universal quantifier
    instance (KnownSymbol nm, Skolemize r) => Skolemize (Forall nm a -> r) where
      type SkolemsTo (Forall nm a -> r) = Forall nm a -> SkolemsTo r
      skolem :: [Char]
    -> [(SVal, [Char])]
    -> (Forall nm a -> r)
    -> SkolemsTo (Forall nm a -> r)
    skolem [Char]
    scope [(SVal, [Char])]
    args Forall nm a -> r
    f arg :: Forall nm a
    arg@(Forall SBV a
    a) = [Char] -> [(SVal, [Char])] -> r -> SkolemsTo r
    forall a.
    Skolemize a =>
    [Char] -> [(SVal, [Char])] -> a -> SkolemsTo a
    skolem [Char]
    scope ([(SVal, [Char])]
    args [(SVal, [Char])] -> [(SVal, [Char])] -> [(SVal, [Char])]
    forall a. [a] -> [a] -> [a]
    ++ [(SBV a -> SVal
    forall a. SBV a -> SVal
    unSBV SBV a
    a, Proxy nm -> [Char]
    forall (n :: Symbol) (proxy :: Symbol -> *).
    KnownSymbol n =>
    proxy n -> [Char]
    symbolVal (forall {k} (t :: k). Proxy t
    forall (t :: Symbol). Proxy t
    Proxy @nm))]) (Forall nm a -> r
    f Forall nm a
    arg)

    -- | Skolemize over a number of universal quantifiers
    instance (KnownSymbol nm, Skolemize r) => Skolemize (ForallN n nm a -> r) where
      type SkolemsTo (ForallN n nm a -> r) = ForallN n nm a -> SkolemsTo r
      skolem :: [Char]
    -> [(SVal, [Char])]
    -> (ForallN n nm a -> r)
    -> SkolemsTo (ForallN n nm a -> r)
    skolem [Char]
    scope [(SVal, [Char])]
    args ForallN n nm a -> r
    f arg :: ForallN n nm a
    arg@(ForallN [SBV a]
    xs) = [Char] -> [(SVal, [Char])] -> r -> SkolemsTo r
    forall a.
    Skolemize a =>
    [Char] -> [(SVal, [Char])] -> a -> SkolemsTo a
    skolem [Char]
    scope ([(SVal, [Char])]
    args [(SVal, [Char])] -> [(SVal, [Char])] -> [(SVal, [Char])]
    forall a. [a] -> [a] -> [a]
    ++ (SBV a -> Int -> (SVal, [Char]))
    -> [SBV a] -> [Int] -> [(SVal, [Char])]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith SBV a -> Int -> (SVal, [Char])
    grab [SBV a]
    xs [(Int
    1::Int)..]) (ForallN n nm a -> r
    f ForallN n nm a
    arg)
        where pre :: [Char]
    pre = Proxy nm -> [Char]
    forall (n :: Symbol) (proxy :: Symbol -> *).
    KnownSymbol n =>
    proxy n -> [Char]
    symbolVal (forall {k} (t :: k). Proxy t
    forall (t :: Symbol). Proxy t
    Proxy @nm)
              grab :: SBV a -> Int -> (SVal, [Char])
    grab SBV a
    x Int
    i = (SBV a -> SVal
    forall a. SBV a -> SVal
    unSBV SBV a
    x, [Char]
    pre [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "_" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    i)

    -- | Skolemize over an existential quantifier
    instance (HasKind a, KnownSymbol nm, Skolemize r) => Skolemize (Exists nm a -> r) where
      type SkolemsTo (Exists nm a -> r) = SkolemsTo r
      skolem :: [Char]
    -> [(SVal, [Char])]
    -> (Exists nm a -> r)
    -> SkolemsTo (Exists nm a -> r)
    skolem [Char]
    scope [(SVal, [Char])]
    args Exists nm a -> r
    f = [Char] -> [(SVal, [Char])] -> r -> SkolemsTo r
    forall a.
    Skolemize a =>
    [Char] -> [(SVal, [Char])] -> a -> SkolemsTo a
    skolem [Char]
    scope [(SVal, [Char])]
    args (Exists nm a -> r
    f (SBV a -> Exists nm a
    forall (nm :: Symbol) a. SBV a -> Exists nm a
    Exists SBV a
    skolemized))
        where skolemized :: SBV a
    skolemized = SVal -> SBV a
    forall a. SVal -> SBV a
    SBV (SVal -> SBV a) -> SVal -> SBV a
    forall a b. (a -> b) -> a -> b
    $ Kind -> [Char] -> UICodeKind -> [(SVal, [Char])] -> SVal
    svUninterpretedNamedArgs (Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a)) ([Char]
    scope [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Proxy nm -> [Char]
    forall (n :: Symbol) (proxy :: Symbol -> *).
    KnownSymbol n =>
    proxy n -> [Char]
    symbolVal (forall {k} (t :: k). Proxy t
    forall (t :: Symbol). Proxy t
    Proxy @nm)) UICodeKind
    UINone [(SVal, [Char])]
    args

    -- | Skolemize over a number of existential quantifiers
    instance (HasKind a, KnownNat n, KnownSymbol nm, Skolemize r) => Skolemize (ExistsN n nm a -> r) where
      type SkolemsTo (ExistsN n nm a -> r) = SkolemsTo r
      skolem :: [Char]
    -> [(SVal, [Char])]
    -> (ExistsN n nm a -> r)
    -> SkolemsTo (ExistsN n nm a -> r)
    skolem [Char]
    scope [(SVal, [Char])]
    args ExistsN n nm a -> r
    f = [Char] -> [(SVal, [Char])] -> r -> SkolemsTo r
    forall a.
    Skolemize a =>
    [Char] -> [(SVal, [Char])] -> a -> SkolemsTo a
    skolem [Char]
    scope [(SVal, [Char])]
    args (ExistsN n nm a -> r
    f ([SBV a] -> ExistsN n nm a
    forall (n :: Nat) (nm :: Symbol) a. [SBV a] -> ExistsN n nm a
    ExistsN [SBV a]
    skolemized))
        where need :: Int
    need   = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n)
              prefix :: [Char]
    prefix = Proxy nm -> [Char]
    forall (n :: Symbol) (proxy :: Symbol -> *).
    KnownSymbol n =>
    proxy n -> [Char]
    symbolVal (forall {k} (t :: k). Proxy t
    forall (t :: Symbol). Proxy t
    Proxy @nm)
              fs :: [[Char]]
    fs     = [[Char]
    prefix [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "_" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    i | Int
    i <- [Int
    1 .. Int
    need]]
              skolemized :: [SBV a]
    skolemized = [SVal -> SBV a
    forall a. SVal -> SBV a
    SBV (SVal -> SBV a) -> SVal -> SBV a
    forall a b. (a -> b) -> a -> b
    $ Kind -> [Char] -> UICodeKind -> [(SVal, [Char])] -> SVal
    svUninterpretedNamedArgs (Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a)) ([Char]
    scope [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    n) UICodeKind
    UINone [(SVal, [Char])]
    args | [Char]
    n <- [[Char]]
    fs]

    -- | Skolemize over a unique existential quantifier
    instance (  HasKind a
              , EqSymbolic (SBV a)
              , KnownSymbol nm
              , QuantifiedBool r
              , Skolemize (Forall (AppendSymbol nm "_eu1") a -> Forall (AppendSymbol nm "_eu2") a -> SBool)
             ) => Skolemize (ExistsUnique nm a -> r) where
      type SkolemsTo (ExistsUnique nm a -> r) =  Forall (AppendSymbol nm "_eu1") a
                                              -> Forall (AppendSymbol nm "_eu2") a
                                              -> SBool
      skolem :: [Char]
    -> [(SVal, [Char])]
    -> (ExistsUnique nm a -> r)
    -> SkolemsTo (ExistsUnique nm a -> r)
    skolem [Char]
    scope [(SVal, [Char])]
    args ExistsUnique nm a -> r
    f = [Char]
    -> [(SVal, [Char])]
    -> (Forall (AppendSymbol nm "_eu1") a
        -> Forall (AppendSymbol nm "_eu2") a -> SBool)
    -> SkolemsTo
         (Forall (AppendSymbol nm "_eu1") a
          -> Forall (AppendSymbol nm "_eu2") a -> SBool)
    forall a.
    Skolemize a =>
    [Char] -> [(SVal, [Char])] -> a -> SkolemsTo a
    skolem [Char]
    scope [(SVal, [Char])]
    args ((ExistsUnique nm a -> r)
    -> Exists nm a
    -> Forall (AppendSymbol nm "_eu1") a
    -> Forall (AppendSymbol nm "_eu2") a
    -> SBool
    forall b a (nm :: Symbol).
    (QuantifiedBool b, EqSymbolic (SBV a)) =>
    (ExistsUnique nm a -> b)
    -> Exists nm a
    -> Forall (AppendSymbol nm "_eu1") a
    -> Forall (AppendSymbol nm "_eu2") a
    -> SBool
    rewriteExistsUnique ExistsUnique nm a -> r
    f (SBV a -> Exists nm a
    forall (nm :: Symbol) a. SBV a -> Exists nm a
    Exists SBV a
    skolemized))
        where skolemized :: SBV a
    skolemized = SVal -> SBV a
    forall a. SVal -> SBV a
    SBV (SVal -> SBV a) -> SVal -> SBV a
    forall a b. (a -> b) -> a -> b
    $ Kind -> [Char] -> UICodeKind -> [(SVal, [Char])] -> SVal
    svUninterpretedNamedArgs (Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a)) ([Char]
    scope [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Proxy nm -> [Char]
    forall (n :: Symbol) (proxy :: Symbol -> *).
    KnownSymbol n =>
    proxy n -> [Char]
    symbolVal (forall {k} (t :: k). Proxy t
    forall (t :: Symbol). Proxy t
    Proxy @nm)) UICodeKind
    UINone [(SVal, [Char])]
    args

    -- | Class of things that we can logically negate
    class QNot a where
      type NegatesTo a :: Type
      -- | Negation of a quantified formula. This operation essentially lifts 'sNot' to quantified formulae.
      -- Note that you can achieve the same using @'sNot' . 'quantifiedBool'@, but that will hide the
      -- quantifiers, so prefer this version if you want to keep them around.
      qNot :: a -> NegatesTo a

    -- | Base case; pure symbolic boolean
    instance QNot SBool where
      type NegatesTo SBool = SBool
      qNot :: SBool -> NegatesTo SBool
    qNot = SBool -> NegatesTo SBool
    SBool -> SBool
    sNot

    -- | Negate over a universal quantifier. Switches to existential.
    instance QNot r => QNot (Forall nm a -> r) where
      type NegatesTo (Forall nm a -> r) = Exists nm a -> NegatesTo r
      qNot :: (Forall nm a -> r) -> NegatesTo (Forall nm a -> r)
    qNot Forall nm a -> r
    f (Exists SBV a
    a) = r -> NegatesTo r
    forall a. QNot a => a -> NegatesTo a
    qNot (Forall nm a -> r
    f (SBV a -> Forall nm a
    forall (nm :: Symbol) a. SBV a -> Forall nm a
    Forall SBV a
    a))

    -- | Negate over a number of universal quantifiers
    instance QNot r => QNot (ForallN nm n a -> r) where
      type NegatesTo (ForallN nm n a -> r) = ExistsN nm n a -> NegatesTo r
      qNot :: (ForallN nm n a -> r) -> NegatesTo (ForallN nm n a -> r)
    qNot ForallN nm n a -> r
    f (ExistsN [SBV a]
    xs) = r -> NegatesTo r
    forall a. QNot a => a -> NegatesTo a
    qNot (ForallN nm n a -> r
    f ([SBV a] -> ForallN nm n a
    forall (n :: Nat) (nm :: Symbol) a. [SBV a] -> ForallN n nm a
    ForallN [SBV a]
    xs))

    -- | Negate over an existential quantifier. Switches to universal.
    instance QNot r => QNot (Exists nm a -> r) where
      type NegatesTo (Exists nm a -> r) = Forall nm a -> NegatesTo r
      qNot :: (Exists nm a -> r) -> NegatesTo (Exists nm a -> r)
    qNot Exists nm a -> r
    f (Forall SBV a
    a) = r -> NegatesTo r
    forall a. QNot a => a -> NegatesTo a
    qNot (Exists nm a -> r
    f (SBV a -> Exists nm a
    forall (nm :: Symbol) a. SBV a -> Exists nm a
    Exists SBV a
    a))

    -- | Negate over a number of existential quantifiers
    instance QNot r => QNot (ExistsN nm n a -> r) where
      type NegatesTo (ExistsN nm n a -> r) = ForallN nm n a -> NegatesTo r
      qNot :: (ExistsN nm n a -> r) -> NegatesTo (ExistsN nm n a -> r)
    qNot ExistsN nm n a -> r
    f (ForallN [SBV a]
    xs) = r -> NegatesTo r
    forall a. QNot a => a -> NegatesTo a
    qNot (ExistsN nm n a -> r
    f ([SBV a] -> ExistsN nm n a
    forall (n :: Nat) (nm :: Symbol) a. [SBV a] -> ExistsN n nm a
    ExistsN [SBV a]
    xs))

    -- | Negate over an unique existential quantifier
    instance (QNot r, QuantifiedBool r, EqSymbolic (SBV a)) => QNot (ExistsUnique nm a -> r) where
      type NegatesTo (ExistsUnique nm a -> r) =  Forall nm a
                                              -> Exists (AppendSymbol nm "_eu1") a
                                              -> Exists (AppendSymbol nm "_eu2") a
                                              -> SBool
      qNot :: (ExistsUnique nm a -> r) -> NegatesTo (ExistsUnique nm a -> r)
    qNot = (Exists nm a
     -> Forall (AppendSymbol nm "_eu1") a
     -> Forall (AppendSymbol nm "_eu2") a
     -> SBool)
    -> NegatesTo
         (Exists nm a
          -> Forall (AppendSymbol nm "_eu1") a
          -> Forall (AppendSymbol nm "_eu2") a
          -> SBool)
    (Exists nm a
     -> Forall (AppendSymbol nm "_eu1") a
     -> Forall (AppendSymbol nm "_eu2") a
     -> SBool)
    -> Forall nm a
    -> Exists (AppendSymbol nm "_eu1") a
    -> Exists (AppendSymbol nm "_eu2") a
    -> SBool
    forall a. QNot a => a -> NegatesTo a
    qNot ((Exists nm a
      -> Forall (AppendSymbol nm "_eu1") a
      -> Forall (AppendSymbol nm "_eu2") a
      -> SBool)
     -> Forall nm a
     -> Exists (AppendSymbol nm "_eu1") a
     -> Exists (AppendSymbol nm "_eu2") a
     -> SBool)
    -> ((ExistsUnique nm a -> r)
        -> Exists nm a
        -> Forall (AppendSymbol nm "_eu1") a
        -> Forall (AppendSymbol nm "_eu2") a
        -> SBool)
    -> (ExistsUnique nm a -> r)
    -> Forall nm a
    -> Exists (AppendSymbol nm "_eu1") a
    -> Exists (AppendSymbol nm "_eu2") a
    -> SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ExistsUnique nm a -> r)
    -> Exists nm a
    -> Forall (AppendSymbol nm "_eu1") a
    -> Forall (AppendSymbol nm "_eu2") a
    -> SBool
    forall b a (nm :: Symbol).
    (QuantifiedBool b, EqSymbolic (SBV a)) =>
    (ExistsUnique nm a -> b)
    -> Exists nm a
    -> Forall (AppendSymbol nm "_eu1") a
    -> Forall (AppendSymbol nm "_eu2") a
    -> SBool
    rewriteExistsUnique

    -- | Get rid of exists unique.
    rewriteExistsUnique :: ( QuantifiedBool b                 -- If b can be turned into a boolean
                           , EqSymbolic (SBV a)               -- If we can do equality on symbolic a's
                           )                                  -- THEN
                        => (ExistsUnique nm a -> b)           -- Given an unique-existential, we can
                        -> Exists nm a                        -- Turn it into an existential
                        -> Forall (AppendSymbol nm "_eu1") a  -- A universal
                        -> Forall (AppendSymbol nm "_eu2") a  -- Another universal
                        -> SBool                                  -- Making sure given holds, and if both univers hold, they're the same
    rewriteExistsUnique :: forall b a (nm :: Symbol).
    (QuantifiedBool b, EqSymbolic (SBV a)) =>
    (ExistsUnique nm a -> b)
    -> Exists nm a
    -> Forall (AppendSymbol nm "_eu1") a
    -> Forall (AppendSymbol nm "_eu2") a
    -> SBool
    rewriteExistsUnique ExistsUnique nm a -> b
    f (Exists SBV a
    x) (Forall SBV a
    x1) (Forall SBV a
    x2) = SBool
    fx SBool -> SBool -> SBool
    .&& SBool
    unique
      where fx :: SBool
    fx    = b -> SBool
    forall a. QuantifiedBool a => a -> SBool
    quantifiedBool (b -> SBool) -> b -> SBool
    forall a b. (a -> b) -> a -> b
    $ ExistsUnique nm a -> b
    f (SBV a -> ExistsUnique nm a
    forall (nm :: Symbol) a. SBV a -> ExistsUnique nm a
    ExistsUnique SBV a
    x)
            fx1 :: b
    fx1   = ExistsUnique nm a -> b
    f (SBV a -> ExistsUnique nm a
    forall (nm :: Symbol) a. SBV a -> ExistsUnique nm a
    ExistsUnique SBV a
    x1)
            fx2 :: b
    fx2   = ExistsUnique nm a -> b
    f (SBV a -> ExistsUnique nm a
    forall (nm :: Symbol) a. SBV a -> ExistsUnique nm a
    ExistsUnique SBV a
    x2)

            bothHolds :: SBool
    bothHolds  = b -> SBool
    forall a. QuantifiedBool a => a -> SBool
    quantifiedBool b
    fx1 SBool -> SBool -> SBool
    .&& b -> SBool
    forall a. QuantifiedBool a => a -> SBool
    quantifiedBool b
    fx2
            mustEqual :: SBool
    mustEqual  = SBV a
    x1 SBV a -> SBV a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SBV a
    x2
            unique :: SBool
    unique     = SBool
    bothHolds SBool -> SBool -> SBool
    .=> SBool
    mustEqual