    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Core.Symbolic
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Symbolic values
    -----------------------------------------------------------------------------

    {-# LANGUAGE CPP                        #-}
    {-# LANGUAGE DefaultSignatures          #-}
    {-# LANGUAGE DeriveDataTypeable         #-}
    {-# LANGUAGE DeriveFunctor              #-}
    {-# LANGUAGE FlexibleInstances          #-}
    {-# LANGUAGE FunctionalDependencies     #-}
    {-# LANGUAGE GADTs                      #-}
    {-# LANGUAGE GeneralizedNewtypeDeriving #-}
    {-# LANGUAGE NamedFieldPuns             #-}
    {-# LANGUAGE PatternGuards              #-}
    {-# LANGUAGE Rank2Types                 #-}
    {-# LANGUAGE ScopedTypeVariables        #-}
    {-# LANGUAGE TupleSections              #-}
    {-# LANGUAGE TypeOperators              #-}
    {-# LANGUAGE UndecidableInstances       #-} -- for undetermined s in MonadState

    {-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}

    module Data.SBV.Core.Symbolic
      ( NodeId(..)
      , SV(..), swKind, trueSV, falseSV
      , Op(..), PBOp(..), OvOp(..), FPOp(..), StrOp(..), SeqOp(..), SetOp(..), RegExp(..)
      , Quantifier(..), needsExistentials
      , RoundingMode(..)
      , SBVType(..), svUninterpreted, newUninterpreted
      , SVal(..)
      , svMkSymVar, sWordN, sWordN_, sIntN, sIntN_
      , ArrayContext(..), ArrayInfo
      , svToSV, svToSymSV, forceSVArg
      , SBVExpr(..), newExpr, isCodeGenMode, isSafetyCheckingIStage, isRunIStage, isSetupIStage
      , Cached, cache, uncache, modifyState, modifyIncState
      , ArrayIndex(..), FArrayIndex(..), uncacheAI, uncacheFAI
      , NamedSymVar
      , getSValPathCondition, extendSValPathCondition
      , getTableIndex
      , SBVPgm(..), MonadSymbolic(..), SymbolicT, Symbolic, runSymbolic, State(..), withNewIncState, IncState(..), incrementInternalCounter
      , inSMTMode, SBVRunMode(..), IStage(..), Result(..)
      , registerKind, registerLabel, recordObservable
      , addAssertion, addNewSMTOption, imposeConstraint, internalConstraint, internalVariable
      , SMTLibPgm(..), SMTLibVersion(..), smtLibVersionExtension
      , SolverCapabilities(..)
      , extractSymbolicSimulationState
      , OptimizeStyle(..), Objective(..), Penalty(..), objectiveName, addSValOptGoal
      , MonadQuery(..), QueryT(..), Query, Queriable(..), Fresh(..), QueryState(..), QueryContext(..)
      , SMTScript(..), Solver(..), SMTSolver(..), SMTResult(..), SMTModel(..), SMTConfig(..), SMTEngine
      , validationRequested, outputSVal
      ) where

    import Control.Arrow               (first, second, (***))
    import Control.DeepSeq             (NFData(..))
    import Control.Monad               (when)
    import Control.Monad.Except        (MonadError, ExceptT)
    import Control.Monad.Reader        (MonadReader(..), ReaderT, runReaderT,
                                        mapReaderT)
    import Control.Monad.State.Lazy    (MonadState)
    import Control.Monad.Trans         (MonadIO(liftIO), MonadTrans(lift))
    import Control.Monad.Trans.Maybe   (MaybeT)
    import Control.Monad.Writer.Strict (MonadWriter)
    import Data.Char                   (isAlpha, isAlphaNum, toLower)
    import Data.IORef                  (IORef, newIORef, readIORef)
    import Data.List                   (intercalate, sortBy)
    import Data.Maybe                  (isJust, fromJust, fromMaybe)
    import Data.String                 (IsString(fromString))

    import Data.Time (getCurrentTime, UTCTime)

    import GHC.Stack

    import qualified Control.Monad.State.Lazy    as LS
    import qualified Control.Monad.State.Strict  as SS
    import qualified Control.Monad.Writer.Lazy   as LW
    import qualified Control.Monad.Writer.Strict as SW
    import qualified Data.IORef                  as R    (modifyIORef')
    import qualified Data.Generics               as G    (Data(..))
    import qualified Data.IntMap.Strict          as IMap (IntMap, empty, toAscList, lookup, insertWith)
    import qualified Data.Map.Strict             as Map  (Map, empty, toList, lookup, insert, size)
    import qualified Data.Set                    as Set  (Set, empty, toList, insert, member)
    import qualified Data.Foldable               as F    (toList)
    import qualified Data.Sequence               as S    (Seq, empty, (|>))

    import System.Mem.StableName

    import Data.SBV.Core.Kind
    import Data.SBV.Core.Concrete
    import Data.SBV.SMT.SMTLibNames
    import Data.SBV.Utils.TDiff (Timing)
    import Data.SBV.Utils.Lib   (stringToQFS)

    import Data.SBV.Control.Types

    #if MIN_VERSION_base(4,11,0)
    import Control.Monad.Fail as Fail
    #endif

    -- | A symbolic node id
    newtype NodeId = NodeId Int deriving (NodeId -> NodeId -> Bool
    (NodeId -> NodeId -> Bool)
    -> (NodeId -> NodeId -> Bool) -> Eq NodeId
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: NodeId -> NodeId -> Bool
    $c/= :: NodeId -> NodeId -> Bool
    == :: NodeId -> NodeId -> Bool
    $c== :: NodeId -> NodeId -> Bool
    Eq, Eq NodeId
    Eq NodeId =>
    (NodeId -> NodeId -> Ordering)
    -> (NodeId -> NodeId -> Bool)
    -> (NodeId -> NodeId -> Bool)
    -> (NodeId -> NodeId -> Bool)
    -> (NodeId -> NodeId -> Bool)
    -> (NodeId -> NodeId -> NodeId)
    -> (NodeId -> NodeId -> NodeId)
    -> Ord NodeId
    NodeId -> NodeId -> Bool
    NodeId -> NodeId -> Ordering
    NodeId -> NodeId -> NodeId
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: NodeId -> NodeId -> NodeId
    $cmin :: NodeId -> NodeId -> NodeId
    max :: NodeId -> NodeId -> NodeId
    $cmax :: NodeId -> NodeId -> NodeId
    >= :: NodeId -> NodeId -> Bool
    $c>= :: NodeId -> NodeId -> Bool
    > :: NodeId -> NodeId -> Bool
    $c> :: NodeId -> NodeId -> Bool
    <= :: NodeId -> NodeId -> Bool
    $c<= :: NodeId -> NodeId -> Bool
    < :: NodeId -> NodeId -> Bool
    $c< :: NodeId -> NodeId -> Bool
    compare :: NodeId -> NodeId -> Ordering
    $ccompare :: NodeId -> NodeId -> Ordering
    $cp1Ord :: Eq NodeId
    Ord)

    -- | A symbolic word, tracking it's signedness and size.
    data SV = SV !Kind !NodeId

    -- | For equality, we merely use the node-id
    instance Eq SV where
      SV _ n1 :: NodeId
    n1 == :: SV -> SV -> Bool
    == SV _ n2 :: NodeId
    n2 = NodeId
    n1 NodeId -> NodeId -> Bool
    forall a. Eq a => a -> a -> Bool
    == NodeId
    n2

    -- | Again, simply use the node-id for ordering
    instance Ord SV where
      SV _ n1 :: NodeId
    n1 compare :: SV -> SV -> Ordering
    `compare` SV _ n2 :: NodeId
    n2 = NodeId
    n1 NodeId -> NodeId -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare` NodeId
    n2

    instance HasKind SV where
      kindOf :: SV -> Kind
    kindOf (SV k :: Kind
    k _) = Kind
    k

    instance Show SV where
      show :: SV -> String
    show (SV _ (NodeId n :: Int
    n)) = case Int
    n of
                                 -2 -> "false"
                                 -1 -> "true"
                                 _  -> 's' Char -> ShowS
    forall a. a -> [a] -> [a]
    : Int -> String
    forall a. Show a => a -> String
    show Int
    n

    -- | Kind of a symbolic word.
    swKind :: SV -> Kind
    swKind :: SV -> Kind
    swKind (SV k :: Kind
    k _) = Kind
    k

    -- | Forcing an argument; this is a necessary evil to make sure all the arguments
    -- to an uninterpreted function are evaluated before called; the semantics of uinterpreted
    -- functions is necessarily strict; deviating from Haskell's
    forceSVArg :: SV -> IO ()
    forceSVArg :: SV -> IO ()
    forceSVArg (SV k :: Kind
    k n :: NodeId
    n) = Kind
    k Kind -> IO () -> IO ()
    forall a b. a -> b -> b
    `seq` NodeId
    n NodeId -> IO () -> IO ()
    forall a b. a -> b -> b
    `seq` () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    -- | Constant False as an 'SV'. Note that this value always occupies slot -2.
    falseSV :: SV
    falseSV :: SV
    falseSV = Kind -> NodeId -> SV
    SV Kind
    KBool (NodeId -> SV) -> NodeId -> SV
    forall a b. (a -> b) -> a -> b
    $ Int -> NodeId
    NodeId (-2)

    -- | Constant True as an 'SV'. Note that this value always occupies slot -1.
    trueSV :: SV
    trueSV :: SV
    trueSV  = Kind -> NodeId -> SV
    SV Kind
    KBool (NodeId -> SV) -> NodeId -> SV
    forall a b. (a -> b) -> a -> b
    $ Int -> NodeId
    NodeId (-1)

    -- | Symbolic operations
    data Op = Plus
            | Times
            | Minus
            | UNeg
            | Abs
            | Quot
            | Rem
            | Equal
            | NotEqual
            | LessThan
            | GreaterThan
            | LessEq
            | GreaterEq
            | Ite
            | And
            | Or
            | XOr
            | Not
            | Shl
            | Shr
            | Rol Int
            | Ror Int
            | Extract Int Int                       -- Extract i j: extract bits i to j. Least significant bit is 0 (big-endian)
            | Join                                  -- Concat two words to form a bigger one, in the order given
            | LkUp (Int, Kind, Kind, Int) !SV !SV   -- (table-index, arg-type, res-type, length of the table) index out-of-bounds-value
            | ArrEq   ArrayIndex ArrayIndex         -- Array equality
            | ArrRead ArrayIndex
            | KindCast Kind Kind
            | Uninterpreted String
            | Label String                          -- Essentially no-op; useful for code generation to emit comments.
            | IEEEFP FPOp                           -- Floating-point ops, categorized separately
            | PseudoBoolean PBOp                    -- Pseudo-boolean ops, categorized separately
            | OverflowOp    OvOp                    -- Overflow-ops, categorized separately
            | StrOp StrOp                           -- String ops, categorized separately
            | SeqOp SeqOp                           -- Sequence ops, categorized separately
            | SetOp SetOp                           -- Set operations, categorized separately
            | TupleConstructor Int                  -- Construct an n-tuple
            | TupleAccess Int Int                   -- Access element i of an n-tuple; second argument is n
            | EitherConstructor Kind Kind Bool      -- Construct a sum; False: left, True: right
            | EitherIs Kind Kind Bool               -- Either branch tester; False: left, True: right
            | EitherAccess Bool                     -- Either branch access; False: left, True: right
            | MaybeConstructor Kind Bool            -- Construct a maybe value; False: Nothing, True: Just
            | MaybeIs Kind Bool                     -- Maybe tester; False: nothing, True: just
            | MaybeAccess                           -- Maybe branch access; grab the contents of the just
            deriving (Op -> Op -> Bool
    (Op -> Op -> Bool) -> (Op -> Op -> Bool) -> Eq Op
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Op -> Op -> Bool
    $c/= :: Op -> Op -> Bool
    == :: Op -> Op -> Bool
    $c== :: Op -> Op -> Bool
    Eq, Eq Op
    Eq Op =>
    (Op -> Op -> Ordering)
    -> (Op -> Op -> Bool)
    -> (Op -> Op -> Bool)
    -> (Op -> Op -> Bool)
    -> (Op -> Op -> Bool)
    -> (Op -> Op -> Op)
    -> (Op -> Op -> Op)
    -> Ord Op
    Op -> Op -> Bool
    Op -> Op -> Ordering
    Op -> Op -> Op
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Op -> Op -> Op
    $cmin :: Op -> Op -> Op
    max :: Op -> Op -> Op
    $cmax :: Op -> Op -> Op
    >= :: Op -> Op -> Bool
    $c>= :: Op -> Op -> Bool
    > :: Op -> Op -> Bool
    $c> :: Op -> Op -> Bool
    <= :: Op -> Op -> Bool
    $c<= :: Op -> Op -> Bool
    < :: Op -> Op -> Bool
    $c< :: Op -> Op -> Bool
    compare :: Op -> Op -> Ordering
    $ccompare :: Op -> Op -> Ordering
    $cp1Ord :: Eq Op
    Ord)

    -- | Floating point operations
    data FPOp = FP_Cast        Kind Kind SV   -- From-Kind, To-Kind, RoundingMode. This is "value" conversion
              | FP_Reinterpret Kind Kind      -- From-Kind, To-Kind. This is bit-reinterpretation using IEEE-754 interchange format
              | FP_Abs
              | FP_Neg
              | FP_Add
              | FP_Sub
              | FP_Mul
              | FP_Div
              | FP_FMA
              | FP_Sqrt
              | FP_Rem
              | FP_RoundToIntegral
              | FP_Min
              | FP_Max
              | FP_ObjEqual
              | FP_IsNormal
              | FP_IsSubnormal
              | FP_IsZero
              | FP_IsInfinite
              | FP_IsNaN
              | FP_IsNegative
              | FP_IsPositive
              deriving (FPOp -> FPOp -> Bool
    (FPOp -> FPOp -> Bool) -> (FPOp -> FPOp -> Bool) -> Eq FPOp
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: FPOp -> FPOp -> Bool
    $c/= :: FPOp -> FPOp -> Bool
    == :: FPOp -> FPOp -> Bool
    $c== :: FPOp -> FPOp -> Bool
    Eq, Eq FPOp
    Eq FPOp =>
    (FPOp -> FPOp -> Ordering)
    -> (FPOp -> FPOp -> Bool)
    -> (FPOp -> FPOp -> Bool)
    -> (FPOp -> FPOp -> Bool)
    -> (FPOp -> FPOp -> Bool)
    -> (FPOp -> FPOp -> FPOp)
    -> (FPOp -> FPOp -> FPOp)
    -> Ord FPOp
    FPOp -> FPOp -> Bool
    FPOp -> FPOp -> Ordering
    FPOp -> FPOp -> FPOp
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: FPOp -> FPOp -> FPOp
    $cmin :: FPOp -> FPOp -> FPOp
    max :: FPOp -> FPOp -> FPOp
    $cmax :: FPOp -> FPOp -> FPOp
    >= :: FPOp -> FPOp -> Bool
    $c>= :: FPOp -> FPOp -> Bool
    > :: FPOp -> FPOp -> Bool
    $c> :: FPOp -> FPOp -> Bool
    <= :: FPOp -> FPOp -> Bool
    $c<= :: FPOp -> FPOp -> Bool
    < :: FPOp -> FPOp -> Bool
    $c< :: FPOp -> FPOp -> Bool
    compare :: FPOp -> FPOp -> Ordering
    $ccompare :: FPOp -> FPOp -> Ordering
    $cp1Ord :: Eq FPOp
    Ord)

    -- Note that the show instance maps to the SMTLib names. We need to make sure
    -- this mapping stays correct through SMTLib changes. The only exception
    -- is FP_Cast; where we handle different source/origins explicitly later on.
    instance Show FPOp where
       show :: FPOp -> String
    show (FP_Cast f :: Kind
    f t :: Kind
    t r :: SV
    r)      = "(FP_Cast: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    f String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " -> " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    t String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ", using RM [" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    r String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "])"
       show (FP_Reinterpret f :: Kind
    f t :: Kind
    t) = case (Kind
    f, Kind
    t) of
                                      (KBounded False 32, KFloat)  -> "(_ to_fp 8 24)"
                                      (KBounded False 64, KDouble) -> "(_ to_fp 11 53)"
                                      _                            -> ShowS
    forall a. HasCallStack => String -> a
    error ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ "SBV.FP_Reinterpret: Unexpected conversion: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    f String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " to " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    t
       show FP_Abs               = "fp.abs"
       show FP_Neg               = "fp.neg"
       show FP_Add               = "fp.add"
       show FP_Sub               = "fp.sub"
       show FP_Mul               = "fp.mul"
       show FP_Div               = "fp.div"
       show FP_FMA               = "fp.fma"
       show FP_Sqrt              = "fp.sqrt"
       show FP_Rem               = "fp.rem"
       show FP_RoundToIntegral   = "fp.roundToIntegral"
       show FP_Min               = "fp.min"
       show FP_Max               = "fp.max"
       show FP_ObjEqual          = "="
       show FP_IsNormal          = "fp.isNormal"
       show FP_IsSubnormal       = "fp.isSubnormal"
       show FP_IsZero            = "fp.isZero"
       show FP_IsInfinite        = "fp.isInfinite"
       show FP_IsNaN             = "fp.isNaN"
       show FP_IsNegative        = "fp.isNegative"
       show FP_IsPositive        = "fp.isPositive"

    -- | Pseudo-boolean operations
    data PBOp = PB_AtMost  Int        -- ^ At most k
              | PB_AtLeast Int        -- ^ At least k
              | PB_Exactly Int        -- ^ Exactly k
              | PB_Le      [Int] Int  -- ^ At most k,  with coefficients given. Generalizes PB_AtMost
              | PB_Ge      [Int] Int  -- ^ At least k, with coefficients given. Generalizes PB_AtLeast
              | PB_Eq      [Int] Int  -- ^ Exactly k,  with coefficients given. Generalized PB_Exactly
              deriving (PBOp -> PBOp -> Bool
    (PBOp -> PBOp -> Bool) -> (PBOp -> PBOp -> Bool) -> Eq PBOp
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: PBOp -> PBOp -> Bool
    $c/= :: PBOp -> PBOp -> Bool
    == :: PBOp -> PBOp -> Bool
    $c== :: PBOp -> PBOp -> Bool
    Eq, Eq PBOp
    Eq PBOp =>
    (PBOp -> PBOp -> Ordering)
    -> (PBOp -> PBOp -> Bool)
    -> (PBOp -> PBOp -> Bool)
    -> (PBOp -> PBOp -> Bool)
    -> (PBOp -> PBOp -> Bool)
    -> (PBOp -> PBOp -> PBOp)
    -> (PBOp -> PBOp -> PBOp)
    -> Ord PBOp
    PBOp -> PBOp -> Bool
    PBOp -> PBOp -> Ordering
    PBOp -> PBOp -> PBOp
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: PBOp -> PBOp -> PBOp
    $cmin :: PBOp -> PBOp -> PBOp
    max :: PBOp -> PBOp -> PBOp
    $cmax :: PBOp -> PBOp -> PBOp
    >= :: PBOp -> PBOp -> Bool
    $c>= :: PBOp -> PBOp -> Bool
    > :: PBOp -> PBOp -> Bool
    $c> :: PBOp -> PBOp -> Bool
    <= :: PBOp -> PBOp -> Bool
    $c<= :: PBOp -> PBOp -> Bool
    < :: PBOp -> PBOp -> Bool
    $c< :: PBOp -> PBOp -> Bool
    compare :: PBOp -> PBOp -> Ordering
    $ccompare :: PBOp -> PBOp -> Ordering
    $cp1Ord :: Eq PBOp
    Ord, Int -> PBOp -> ShowS
    [PBOp] -> ShowS
    PBOp -> String
    (Int -> PBOp -> ShowS)
    -> (PBOp -> String) -> ([PBOp] -> ShowS) -> Show PBOp
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [PBOp] -> ShowS
    $cshowList :: [PBOp] -> ShowS
    show :: PBOp -> String
    $cshow :: PBOp -> String
    showsPrec :: Int -> PBOp -> ShowS
    $cshowsPrec :: Int -> PBOp -> ShowS
    Show)

    -- | Overflow operations
    data OvOp = Overflow_SMul_OVFL   -- ^ Signed multiplication overflow
              | Overflow_SMul_UDFL   -- ^ Signed multiplication underflow
              | Overflow_UMul_OVFL   -- ^ Unsigned multiplication overflow
              deriving (OvOp -> OvOp -> Bool
    (OvOp -> OvOp -> Bool) -> (OvOp -> OvOp -> Bool) -> Eq OvOp
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: OvOp -> OvOp -> Bool
    $c/= :: OvOp -> OvOp -> Bool
    == :: OvOp -> OvOp -> Bool
    $c== :: OvOp -> OvOp -> Bool
    Eq, Eq OvOp
    Eq OvOp =>
    (OvOp -> OvOp -> Ordering)
    -> (OvOp -> OvOp -> Bool)
    -> (OvOp -> OvOp -> Bool)
    -> (OvOp -> OvOp -> Bool)
    -> (OvOp -> OvOp -> Bool)
    -> (OvOp -> OvOp -> OvOp)
    -> (OvOp -> OvOp -> OvOp)
    -> Ord OvOp
    OvOp -> OvOp -> Bool
    OvOp -> OvOp -> Ordering
    OvOp -> OvOp -> OvOp
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: OvOp -> OvOp -> OvOp
    $cmin :: OvOp -> OvOp -> OvOp
    max :: OvOp -> OvOp -> OvOp
    $cmax :: OvOp -> OvOp -> OvOp
    >= :: OvOp -> OvOp -> Bool
    $c>= :: OvOp -> OvOp -> Bool
    > :: OvOp -> OvOp -> Bool
    $c> :: OvOp -> OvOp -> Bool
    <= :: OvOp -> OvOp -> Bool
    $c<= :: OvOp -> OvOp -> Bool
    < :: OvOp -> OvOp -> Bool
    $c< :: OvOp -> OvOp -> Bool
    compare :: OvOp -> OvOp -> Ordering
    $ccompare :: OvOp -> OvOp -> Ordering
    $cp1Ord :: Eq OvOp
    Ord)

    -- | Show instance. It's important that these follow the internal z3 names
    instance Show OvOp where
      show :: OvOp -> String
    show Overflow_SMul_OVFL = "bvsmul_noovfl"
      show Overflow_SMul_UDFL = "bvsmul_noudfl"
      show Overflow_UMul_OVFL = "bvumul_noovfl"

    -- | String operations. Note that we do not define @StrAt@ as it translates to 'StrSubstr' trivially.
    data StrOp = StrConcat       -- ^ Concatenation of one or more strings
               | StrLen          -- ^ String length
               | StrUnit         -- ^ Unit string
               | StrNth          -- ^ Nth element
               | StrSubstr       -- ^ Retrieves substring of @s@ at @offset@
               | StrIndexOf      -- ^ Retrieves first position of @sub@ in @s@, @-1@ if there are no occurrences
               | StrContains     -- ^ Does @s@ contain the substring @sub@?
               | StrPrefixOf     -- ^ Is @pre@ a prefix of @s@?
               | StrSuffixOf     -- ^ Is @suf@ a suffix of @s@?
               | StrReplace      -- ^ Replace the first occurrence of @src@ by @dst@ in @s@
               | StrStrToNat     -- ^ Retrieve integer encoded by string @s@ (ground rewriting only)
               | StrNatToStr     -- ^ Retrieve string encoded by integer @i@ (ground rewriting only)
               | StrInRe RegExp  -- ^ Check if string is in the regular expression
               deriving (StrOp -> StrOp -> Bool
    (StrOp -> StrOp -> Bool) -> (StrOp -> StrOp -> Bool) -> Eq StrOp
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: StrOp -> StrOp -> Bool
    $c/= :: StrOp -> StrOp -> Bool
    == :: StrOp -> StrOp -> Bool
    $c== :: StrOp -> StrOp -> Bool
    Eq, Eq StrOp
    Eq StrOp =>
    (StrOp -> StrOp -> Ordering)
    -> (StrOp -> StrOp -> Bool)
    -> (StrOp -> StrOp -> Bool)
    -> (StrOp -> StrOp -> Bool)
    -> (StrOp -> StrOp -> Bool)
    -> (StrOp -> StrOp -> StrOp)
    -> (StrOp -> StrOp -> StrOp)
    -> Ord StrOp
    StrOp -> StrOp -> Bool
    StrOp -> StrOp -> Ordering
    StrOp -> StrOp -> StrOp
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: StrOp -> StrOp -> StrOp
    $cmin :: StrOp -> StrOp -> StrOp
    max :: StrOp -> StrOp -> StrOp
    $cmax :: StrOp -> StrOp -> StrOp
    >= :: StrOp -> StrOp -> Bool
    $c>= :: StrOp -> StrOp -> Bool
    > :: StrOp -> StrOp -> Bool
    $c> :: StrOp -> StrOp -> Bool
    <= :: StrOp -> StrOp -> Bool
    $c<= :: StrOp -> StrOp -> Bool
    < :: StrOp -> StrOp -> Bool
    $c< :: StrOp -> StrOp -> Bool
    compare :: StrOp -> StrOp -> Ordering
    $ccompare :: StrOp -> StrOp -> Ordering
    $cp1Ord :: Eq StrOp
    Ord)

    -- | Regular expressions. Note that regular expressions themselves are
    -- concrete, but the 'Data.SBV.RegExp.match' function from the 'Data.SBV.RegExp.RegExpMatchable' class
    -- can check membership against a symbolic string/character. Also, we
    -- are preferring a datatype approach here, as opposed to coming up with
    -- some string-representation; there are way too many alternatives
    -- already so inventing one isn't a priority. Please get in touch if you
    -- would like a parser for this type as it might be easier to use.
    data RegExp = Literal String       -- ^ Precisely match the given string
                | All                  -- ^ Accept every string
                | None                 -- ^ Accept no strings
                | Range Char Char      -- ^ Accept range of characters
                | Conc  [RegExp]       -- ^ Concatenation
                | KStar RegExp         -- ^ Kleene Star: Zero or more
                | KPlus RegExp         -- ^ Kleene Plus: One or more
                | Opt   RegExp         -- ^ Zero or one
                | Loop  Int Int RegExp -- ^ From @n@ repetitions to @m@ repetitions
                | Union [RegExp]       -- ^ Union of regular expressions
                | Inter RegExp RegExp  -- ^ Intersection of regular expressions
                deriving (RegExp -> RegExp -> Bool
    (RegExp -> RegExp -> Bool)
    -> (RegExp -> RegExp -> Bool) -> Eq RegExp
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: RegExp -> RegExp -> Bool
    $c/= :: RegExp -> RegExp -> Bool
    == :: RegExp -> RegExp -> Bool
    $c== :: RegExp -> RegExp -> Bool
    Eq, Eq RegExp
    Eq RegExp =>
    (RegExp -> RegExp -> Ordering)
    -> (RegExp -> RegExp -> Bool)
    -> (RegExp -> RegExp -> Bool)
    -> (RegExp -> RegExp -> Bool)
    -> (RegExp -> RegExp -> Bool)
    -> (RegExp -> RegExp -> RegExp)
    -> (RegExp -> RegExp -> RegExp)
    -> Ord RegExp
    RegExp -> RegExp -> Bool
    RegExp -> RegExp -> Ordering
    RegExp -> RegExp -> RegExp
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: RegExp -> RegExp -> RegExp
    $cmin :: RegExp -> RegExp -> RegExp
    max :: RegExp -> RegExp -> RegExp
    $cmax :: RegExp -> RegExp -> RegExp
    >= :: RegExp -> RegExp -> Bool
    $c>= :: RegExp -> RegExp -> Bool
    > :: RegExp -> RegExp -> Bool
    $c> :: RegExp -> RegExp -> Bool
    <= :: RegExp -> RegExp -> Bool
    $c<= :: RegExp -> RegExp -> Bool
    < :: RegExp -> RegExp -> Bool
    $c< :: RegExp -> RegExp -> Bool
    compare :: RegExp -> RegExp -> Ordering
    $ccompare :: RegExp -> RegExp -> Ordering
    $cp1Ord :: Eq RegExp
    Ord)

    -- | With overloaded strings, we can have direct literal regular expressions.
    instance IsString RegExp where
      fromString :: String -> RegExp
    fromString = String -> RegExp
    Literal

    -- | Regular expressions as a 'Num' instance. Note that
    -- only `+` (union) and `*` (concatenation) make sense.
    instance Num RegExp where
      -- flatten the concats to make them simpler
      Conc xs :: [RegExp]
    xs * :: RegExp -> RegExp -> RegExp
    * y :: RegExp
    y = [RegExp] -> RegExp
    Conc ([RegExp]
    xs [RegExp] -> [RegExp] -> [RegExp]
    forall a. [a] -> [a] -> [a]
    ++ [RegExp
    y])
      x :: RegExp
    x * Conc ys :: [RegExp]
    ys = [RegExp] -> RegExp
    Conc (RegExp
    x  RegExp -> [RegExp] -> [RegExp]
    forall a. a -> [a] -> [a]
    :  [RegExp]
    ys)
      x :: RegExp
    x * y :: RegExp
    y       = [RegExp] -> RegExp
    Conc [RegExp
    x, RegExp
    y]

      -- flatten the unions to make them simpler
      Union xs :: [RegExp]
    xs + :: RegExp -> RegExp -> RegExp
    + y :: RegExp
    y = [RegExp] -> RegExp
    Union ([RegExp]
    xs [RegExp] -> [RegExp] -> [RegExp]
    forall a. [a] -> [a] -> [a]
    ++ [RegExp
    y])
      x :: RegExp
    x + Union ys :: [RegExp]
    ys = [RegExp] -> RegExp
    Union (RegExp
    x  RegExp -> [RegExp] -> [RegExp]
    forall a. a -> [a] -> [a]
    : [RegExp]
    ys)
      x :: RegExp
    x + y :: RegExp
    y        = [RegExp] -> RegExp
    Union [RegExp
    x, RegExp
    y]

      abs :: RegExp -> RegExp
    abs         = String -> RegExp -> RegExp
    forall a. HasCallStack => String -> a
    error "Num.RegExp: no abs method"
      signum :: RegExp -> RegExp
    signum      = String -> RegExp -> RegExp
    forall a. HasCallStack => String -> a
    error "Num.RegExp: no signum method"

      fromInteger :: Integer -> RegExp
    fromInteger x :: Integer
    x
        | Integer
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0    = RegExp
    None
        | Integer
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == 1    = String -> RegExp
    Literal ""   -- Unit for concatenation is the empty string
        | Bool
    True      = String -> RegExp
    forall a. HasCallStack => String -> a
    error (String -> RegExp) -> String -> RegExp
    forall a b. (a -> b) -> a -> b
    $ "Num.RegExp: Only 0 and 1 makes sense as a reg-exp, no meaning for: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show Integer
    x

      negate :: RegExp -> RegExp
    negate      = String -> RegExp -> RegExp
    forall a. HasCallStack => String -> a
    error "Num.RegExp: no negate method"

    -- | Show instance for `RegExp`. The mapping is done so the outcome matches the
    -- SMTLib string reg-exp operations
    instance Show RegExp where
      show :: RegExp -> String
    show (Literal s :: String
    s)       = "(str.to.re \"" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    stringToQFS String
    s String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "\")"
      show All               = "re.allchar"
      show None              = "re.nostr"
      show (Range ch1 :: Char
    ch1 ch2 :: Char
    ch2)   = "(re.range \"" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    stringToQFS [Char
    ch1] String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "\" \"" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    stringToQFS [Char
    ch2] String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "\")"
      show (Conc [])         = Integer -> String
    forall a. Show a => a -> String
    show (1 :: Integer)
      show (Conc [x :: RegExp
    x])        = RegExp -> String
    forall a. Show a => a -> String
    show RegExp
    x
      show (Conc xs :: [RegExp]
    xs)         = "(re.++ " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((RegExp -> String) -> [RegExp] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map RegExp -> String
    forall a. Show a => a -> String
    show [RegExp]
    xs) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
      show (KStar r :: RegExp
    r)         = "(re.* " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ RegExp -> String
    forall a. Show a => a -> String
    show RegExp
    r String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
      show (KPlus r :: RegExp
    r)         = "(re.+ " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ RegExp -> String
    forall a. Show a => a -> String
    show RegExp
    r String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
      show (Opt   r :: RegExp
    r)         = "(re.opt " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ RegExp -> String
    forall a. Show a => a -> String
    show RegExp
    r String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
      show (Loop  lo :: Int
    lo hi :: Int
    hi r :: RegExp
    r)
         | Int
    lo Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= 0, Int
    hi Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    lo = "((_ re.loop " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    lo String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    hi String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ") " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ RegExp -> String
    forall a. Show a => a -> String
    show RegExp
    r String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
         | Bool
    True              = ShowS
    forall a. HasCallStack => String -> a
    error ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ "Invalid regular-expression Loop with arguments: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Int, Int) -> String
    forall a. Show a => a -> String
    show (Int
    lo, Int
    hi)
      show (Inter r1 :: RegExp
    r1 r2 :: RegExp
    r2)     = "(re.inter " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ RegExp -> String
    forall a. Show a => a -> String
    show RegExp
    r1 String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ RegExp -> String
    forall a. Show a => a -> String
    show RegExp
    r2 String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
      show (Union [])        = "re.nostr"
      show (Union [x :: RegExp
    x])       = RegExp -> String
    forall a. Show a => a -> String
    show RegExp
    x
      show (Union xs :: [RegExp]
    xs)        = "(re.union " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((RegExp -> String) -> [RegExp] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map RegExp -> String
    forall a. Show a => a -> String
    show [RegExp]
    xs) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"

    -- | Show instance for @StrOp@. Note that the mapping here is
    -- important to match the SMTLib equivalents, see here: <http://rise4fun.com/z3/tutorialcontent/sequences>
    instance Show StrOp where
      show :: StrOp -> String
    show StrConcat   = "str.++"
      show StrLen      = "str.len"
      show StrUnit     = "seq.unit"      -- NB. The "seq" prefix is intentional; works uniformly.
      show StrNth      = "seq.nth"       -- NB. The "seq" prefix is intentional; works uniformly.
      show StrSubstr   = "str.substr"
      show StrIndexOf  = "str.indexof"
      show StrContains = "str.contains"
      show StrPrefixOf = "str.prefixof"
      show StrSuffixOf = "str.suffixof"
      show StrReplace  = "str.replace"
      show StrStrToNat = "str.to.int"    -- NB. SMTLib uses "int" here though only nats are supported
      show StrNatToStr = "int.to.str"    -- NB. SMTLib uses "int" here though only nats are supported
      -- Note the breakage here with respect to argument order. We fix this explicitly later.
      show (StrInRe s :: RegExp
    s) = "str.in.re " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ RegExp -> String
    forall a. Show a => a -> String
    show RegExp
    s

    -- | Sequence operations.
    data SeqOp = SeqConcat    -- ^ See StrConcat
               | SeqLen       -- ^ See StrLen
               | SeqUnit      -- ^ See StrUnit
               | SeqNth       -- ^ See StrNth
               | SeqSubseq    -- ^ See StrSubseq
               | SeqIndexOf   -- ^ See StrIndexOf
               | SeqContains  -- ^ See StrContains
               | SeqPrefixOf  -- ^ See StrPrefixOf
               | SeqSuffixOf  -- ^ See StrSuffixOf
               | SeqReplace   -- ^ See StrReplace
      deriving (SeqOp -> SeqOp -> Bool
    (SeqOp -> SeqOp -> Bool) -> (SeqOp -> SeqOp -> Bool) -> Eq SeqOp
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: SeqOp -> SeqOp -> Bool
    $c/= :: SeqOp -> SeqOp -> Bool
    == :: SeqOp -> SeqOp -> Bool
    $c== :: SeqOp -> SeqOp -> Bool
    Eq, Eq SeqOp
    Eq SeqOp =>
    (SeqOp -> SeqOp -> Ordering)
    -> (SeqOp -> SeqOp -> Bool)
    -> (SeqOp -> SeqOp -> Bool)
    -> (SeqOp -> SeqOp -> Bool)
    -> (SeqOp -> SeqOp -> Bool)
    -> (SeqOp -> SeqOp -> SeqOp)
    -> (SeqOp -> SeqOp -> SeqOp)
    -> Ord SeqOp
    SeqOp -> SeqOp -> Bool
    SeqOp -> SeqOp -> Ordering
    SeqOp -> SeqOp -> SeqOp
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: SeqOp -> SeqOp -> SeqOp
    $cmin :: SeqOp -> SeqOp -> SeqOp
    max :: SeqOp -> SeqOp -> SeqOp
    $cmax :: SeqOp -> SeqOp -> SeqOp
    >= :: SeqOp -> SeqOp -> Bool
    $c>= :: SeqOp -> SeqOp -> Bool
    > :: SeqOp -> SeqOp -> Bool
    $c> :: SeqOp -> SeqOp -> Bool
    <= :: SeqOp -> SeqOp -> Bool
    $c<= :: SeqOp -> SeqOp -> Bool
    < :: SeqOp -> SeqOp -> Bool
    $c< :: SeqOp -> SeqOp -> Bool
    compare :: SeqOp -> SeqOp -> Ordering
    $ccompare :: SeqOp -> SeqOp -> Ordering
    $cp1Ord :: Eq SeqOp
    Ord)

    -- | Show instance for SeqOp. Again, mapping is important.
    instance Show SeqOp where
      show :: SeqOp -> String
    show SeqConcat   = "seq.++"
      show SeqLen      = "seq.len"
      show SeqUnit     = "seq.unit"
      show SeqNth      = "seq.nth"
      show SeqSubseq   = "seq.extract"
      show SeqIndexOf  = "seq.indexof"
      show SeqContains = "seq.contains"
      show SeqPrefixOf = "seq.prefixof"
      show SeqSuffixOf = "seq.suffixof"
      show SeqReplace  = "seq.replace"

    -- | Set operations.
    data SetOp = SetEqual
               | SetMember
               | SetInsert
               | SetDelete
               | SetIntersect
               | SetUnion
               | SetSubset
               | SetDifference
               | SetComplement
               | SetHasSize
            deriving (SetOp -> SetOp -> Bool
    (SetOp -> SetOp -> Bool) -> (SetOp -> SetOp -> Bool) -> Eq SetOp
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: SetOp -> SetOp -> Bool
    $c/= :: SetOp -> SetOp -> Bool
    == :: SetOp -> SetOp -> Bool
    $c== :: SetOp -> SetOp -> Bool
    Eq, Eq SetOp
    Eq SetOp =>
    (SetOp -> SetOp -> Ordering)
    -> (SetOp -> SetOp -> Bool)
    -> (SetOp -> SetOp -> Bool)
    -> (SetOp -> SetOp -> Bool)
    -> (SetOp -> SetOp -> Bool)
    -> (SetOp -> SetOp -> SetOp)
    -> (SetOp -> SetOp -> SetOp)
    -> Ord SetOp
    SetOp -> SetOp -> Bool
    SetOp -> SetOp -> Ordering
    SetOp -> SetOp -> SetOp
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: SetOp -> SetOp -> SetOp
    $cmin :: SetOp -> SetOp -> SetOp
    max :: SetOp -> SetOp -> SetOp
    $cmax :: SetOp -> SetOp -> SetOp
    >= :: SetOp -> SetOp -> Bool
    $c>= :: SetOp -> SetOp -> Bool
    > :: SetOp -> SetOp -> Bool
    $c> :: SetOp -> SetOp -> Bool
    <= :: SetOp -> SetOp -> Bool
    $c<= :: SetOp -> SetOp -> Bool
    < :: SetOp -> SetOp -> Bool
    $c< :: SetOp -> SetOp -> Bool
    compare :: SetOp -> SetOp -> Ordering
    $ccompare :: SetOp -> SetOp -> Ordering
    $cp1Ord :: Eq SetOp
    Ord)

    -- The show instance for 'SetOp' is merely for debugging, we map them separately so
    -- the mapped strings are less important here.
    instance Show SetOp where
      show :: SetOp -> String
    show SetEqual      = "=="
      show SetMember     = "Set.member"
      show SetInsert     = "Set.insert"
      show SetDelete     = "Set.delete"
      show SetIntersect  = "Set.intersect"
      show SetUnion      = "Set.union"
      show SetSubset     = "Set.subset"
      show SetDifference = "Set.difference"
      show SetComplement = "Set.complement"
      show SetHasSize    = "Set.setHasSize"

    -- Show instance for 'Op'. Note that this is largely for debugging purposes, not used
    -- for being read by any tool.
    instance Show Op where
      show :: Op -> String
    show Shl    = "<<"
      show Shr    = ">>"

      show (Rol i :: Int
    i) = "<<<" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i
      show (Ror i :: Int
    i) = ">>>" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i

      show (Extract i :: Int
    i j :: Int
    j) = "choose [" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ":" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    j String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "]"

      show (LkUp (ti :: Int
    ti, at :: Kind
    at, rt :: Kind
    rt, l :: Int
    l) i :: SV
    i e :: SV
    e)
            = "lookup(" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    tinfo String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ", " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    i String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ", " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    e String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
            where tinfo :: String
    tinfo = "table" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    ti String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "(" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    at String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " -> " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    rt String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ", " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    l String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"

      show (ArrEq i :: ArrayIndex
    i j :: ArrayIndex
    j)          = "array_" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ArrayIndex -> String
    forall a. Show a => a -> String
    show ArrayIndex
    i String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " == array_" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ArrayIndex -> String
    forall a. Show a => a -> String
    show ArrayIndex
    j
      show (ArrRead i :: ArrayIndex
    i)          = "select array_" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ArrayIndex -> String
    forall a. Show a => a -> String
    show ArrayIndex
    i

      show (KindCast fr :: Kind
    fr to :: Kind
    to)     = "cast_" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    fr String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "_" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    to
      show (Uninterpreted i :: String
    i)    = "[uninterpreted] " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    i

      show (Label s :: String
    s)            = "[label] " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    s

      show (IEEEFP w :: FPOp
    w)           = FPOp -> String
    forall a. Show a => a -> String
    show FPOp
    w

      show (PseudoBoolean p :: PBOp
    p)    = PBOp -> String
    forall a. Show a => a -> String
    show PBOp
    p

      show (OverflowOp o :: OvOp
    o)       = OvOp -> String
    forall a. Show a => a -> String
    show OvOp
    o

      show (StrOp s :: StrOp
    s)            = StrOp -> String
    forall a. Show a => a -> String
    show StrOp
    s
      show (SeqOp s :: SeqOp
    s)            = SeqOp -> String
    forall a. Show a => a -> String
    show SeqOp
    s
      show (SetOp s :: SetOp
    s)            = SetOp -> String
    forall a. Show a => a -> String
    show SetOp
    s

      show (TupleConstructor   0) = "mkSBVTuple0"
      show (TupleConstructor   n :: Int
    n) = "mkSBVTuple" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n
      show (TupleAccess      i :: Int
    i n :: Int
    n) = "proj_" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "_SBVTuple" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n

      show (EitherConstructor k1 :: Kind
    k1 k2 :: Kind
    k2  False) = "(_ left_SBVEither "  String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show (Kind -> Kind -> Kind
    KEither Kind
    k1 Kind
    k2) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
      show (EitherConstructor k1 :: Kind
    k1 k2 :: Kind
    k2  True ) = "(_ right_SBVEither " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show (Kind -> Kind -> Kind
    KEither Kind
    k1 Kind
    k2) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
      show (EitherIs          k1 :: Kind
    k1 k2 :: Kind
    k2  False) = "(_ is (left_SBVEither ("  String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k1 String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ") " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show (Kind -> Kind -> Kind
    KEither Kind
    k1 Kind
    k2) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "))"
      show (EitherIs          k1 :: Kind
    k1 k2 :: Kind
    k2  True ) = "(_ is (right_SBVEither (" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k2 String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ") " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show (Kind -> Kind -> Kind
    KEither Kind
    k1 Kind
    k2) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "))"
      show (EitherAccess             False) = "get_left_SBVEither"
      show (EitherAccess             True ) = "get_right_SBVEither"

      show (MaybeConstructor k :: Kind
    k False) = "(_ nothing_SBVMaybe " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show (Kind -> Kind
    KMaybe Kind
    k) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
      show (MaybeConstructor k :: Kind
    k True)  = "(_ just_SBVMaybe "    String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show (Kind -> Kind
    KMaybe Kind
    k) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
      show (MaybeIs          k :: Kind
    k False) = "(_ is (nothing_SBVMaybe () "              String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show (Kind -> Kind
    KMaybe Kind
    k) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "))"
      show (MaybeIs          k :: Kind
    k True ) = "(_ is (just_SBVMaybe (" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ") " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show (Kind -> Kind
    KMaybe Kind
    k) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "))"
      show MaybeAccess               = "get_just_SBVMaybe"

      show op :: Op
    op
        | Just s :: String
    s <- Op
    op Op -> [(Op, String)] -> Maybe String
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    `lookup` [(Op, String)]
    syms = String
    s
        | Bool
    True                       = ShowS
    forall a. HasCallStack => String -> a
    error "impossible happened; can't find op!"
        where syms :: [(Op, String)]
    syms = [ (Op
    Plus, "+"), (Op
    Times, "*"), (Op
    Minus, "-"), (Op
    UNeg, "-"), (Op
    Abs, "abs")
                     , (Op
    Quot, "quot")
                     , (Op
    Rem,  "rem")
                     , (Op
    Equal, "=="), (Op
    NotEqual, "/=")
                     , (Op
    LessThan, "<"), (Op
    GreaterThan, ">"), (Op
    LessEq, "<="), (Op
    GreaterEq, ">=")
                     , (Op
    Ite, "if_then_else")
                     , (Op
    And, "&"), (Op
    Or, "|"), (Op
    XOr, "^"), (Op
    Not, "~")
                     , (Op
    Join, "#")
                     ]

    -- | Quantifiers: forall or exists. Note that we allow
    -- arbitrary nestings.
    data Quantifier = ALL | EX deriving Quantifier -> Quantifier -> Bool
    (Quantifier -> Quantifier -> Bool)
    -> (Quantifier -> Quantifier -> Bool) -> Eq Quantifier
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Quantifier -> Quantifier -> Bool
    $c/= :: Quantifier -> Quantifier -> Bool
    == :: Quantifier -> Quantifier -> Bool
    $c== :: Quantifier -> Quantifier -> Bool
    Eq

    -- | Show instance for 'Quantifier'
    instance Show Quantifier where
      show :: Quantifier -> String
    show ALL = "Forall"
      show EX  = "Exists"

    -- | Are there any existential quantifiers?
    needsExistentials :: [Quantifier] -> Bool
    needsExistentials :: [Quantifier] -> Bool
    needsExistentials = (Quantifier
    EX Quantifier -> [Quantifier] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem`)

    -- | A simple type for SBV computations, used mainly for uninterpreted constants.
    -- We keep track of the signedness/size of the arguments. A non-function will
    -- have just one entry in the list.
    newtype SBVType = SBVType [Kind]
                 deriving (SBVType -> SBVType -> Bool
    (SBVType -> SBVType -> Bool)
    -> (SBVType -> SBVType -> Bool) -> Eq SBVType
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: SBVType -> SBVType -> Bool
    $c/= :: SBVType -> SBVType -> Bool
    == :: SBVType -> SBVType -> Bool
    $c== :: SBVType -> SBVType -> Bool
    Eq, Eq SBVType
    Eq SBVType =>
    (SBVType -> SBVType -> Ordering)
    -> (SBVType -> SBVType -> Bool)
    -> (SBVType -> SBVType -> Bool)
    -> (SBVType -> SBVType -> Bool)
    -> (SBVType -> SBVType -> Bool)
    -> (SBVType -> SBVType -> SBVType)
    -> (SBVType -> SBVType -> SBVType)
    -> Ord SBVType
    SBVType -> SBVType -> Bool
    SBVType -> SBVType -> Ordering
    SBVType -> SBVType -> SBVType
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: SBVType -> SBVType -> SBVType
    $cmin :: SBVType -> SBVType -> SBVType
    max :: SBVType -> SBVType -> SBVType
    $cmax :: SBVType -> SBVType -> SBVType
    >= :: SBVType -> SBVType -> Bool
    $c>= :: SBVType -> SBVType -> Bool
    > :: SBVType -> SBVType -> Bool
    $c> :: SBVType -> SBVType -> Bool
    <= :: SBVType -> SBVType -> Bool
    $c<= :: SBVType -> SBVType -> Bool
    < :: SBVType -> SBVType -> Bool
    $c< :: SBVType -> SBVType -> Bool
    compare :: SBVType -> SBVType -> Ordering
    $ccompare :: SBVType -> SBVType -> Ordering
    $cp1Ord :: Eq SBVType
    Ord)

    instance Show SBVType where
      show :: SBVType -> String
    show (SBVType []) = ShowS
    forall a. HasCallStack => String -> a
    error "SBV: internal error, empty SBVType"
      show (SBVType xs :: [Kind]
    xs) = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate " -> " ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ (Kind -> String) -> [Kind] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Kind -> String
    forall a. Show a => a -> String
    show [Kind]
    xs

    -- | A symbolic expression
    data SBVExpr = SBVApp !Op ![SV]
                 deriving (SBVExpr -> SBVExpr -> Bool
    (SBVExpr -> SBVExpr -> Bool)
    -> (SBVExpr -> SBVExpr -> Bool) -> Eq SBVExpr
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: SBVExpr -> SBVExpr -> Bool
    $c/= :: SBVExpr -> SBVExpr -> Bool
    == :: SBVExpr -> SBVExpr -> Bool
    $c== :: SBVExpr -> SBVExpr -> Bool
    Eq, Eq SBVExpr
    Eq SBVExpr =>
    (SBVExpr -> SBVExpr -> Ordering)
    -> (SBVExpr -> SBVExpr -> Bool)
    -> (SBVExpr -> SBVExpr -> Bool)
    -> (SBVExpr -> SBVExpr -> Bool)
    -> (SBVExpr -> SBVExpr -> Bool)
    -> (SBVExpr -> SBVExpr -> SBVExpr)
    -> (SBVExpr -> SBVExpr -> SBVExpr)
    -> Ord SBVExpr
    SBVExpr -> SBVExpr -> Bool
    SBVExpr -> SBVExpr -> Ordering
    SBVExpr -> SBVExpr -> SBVExpr
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: SBVExpr -> SBVExpr -> SBVExpr
    $cmin :: SBVExpr -> SBVExpr -> SBVExpr
    max :: SBVExpr -> SBVExpr -> SBVExpr
    $cmax :: SBVExpr -> SBVExpr -> SBVExpr
    >= :: SBVExpr -> SBVExpr -> Bool
    $c>= :: SBVExpr -> SBVExpr -> Bool
    > :: SBVExpr -> SBVExpr -> Bool
    $c> :: SBVExpr -> SBVExpr -> Bool
    <= :: SBVExpr -> SBVExpr -> Bool
    $c<= :: SBVExpr -> SBVExpr -> Bool
    < :: SBVExpr -> SBVExpr -> Bool
    $c< :: SBVExpr -> SBVExpr -> Bool
    compare :: SBVExpr -> SBVExpr -> Ordering
    $ccompare :: SBVExpr -> SBVExpr -> Ordering
    $cp1Ord :: Eq SBVExpr
    Ord)

    -- | To improve hash-consing, take advantage of commutative operators by
    -- reordering their arguments.
    reorder :: SBVExpr -> SBVExpr
    reorder :: SBVExpr -> SBVExpr
    reorder s :: SBVExpr
    s = case SBVExpr
    s of
                  SBVApp op :: Op
    op [a :: SV
    a, b :: SV
    b] | Op -> Bool
    isCommutative Op
    op Bool -> Bool -> Bool
    && SV
    a SV -> SV -> Bool
    forall a. Ord a => a -> a -> Bool
    > SV
    b -> Op -> [SV] -> SBVExpr
    SBVApp Op
    op [SV
    b, SV
    a]
                  _ -> SBVExpr
    s
      where isCommutative :: Op -> Bool
            isCommutative :: Op -> Bool
    isCommutative o :: Op
    o = Op
    o Op -> [Op] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Op
    Plus, Op
    Times, Op
    Equal, Op
    NotEqual, Op
    And, Op
    Or, Op
    XOr]

    -- Show instance for 'SBVExpr'. Again, only for debugging purposes.
    instance Show SBVExpr where
      show :: SBVExpr -> String
    show (SBVApp Ite [t :: SV
    t, a :: SV
    a, b :: SV
    b])             = [String] -> String
    unwords ["if", SV -> String
    forall a. Show a => a -> String
    show SV
    t, "then", SV -> String
    forall a. Show a => a -> String
    show SV
    a, "else", SV -> String
    forall a. Show a => a -> String
    show SV
    b]
      show (SBVApp Shl     [a :: SV
    a, i :: SV
    i])            = [String] -> String
    unwords [SV -> String
    forall a. Show a => a -> String
    show SV
    a, "<<", SV -> String
    forall a. Show a => a -> String
    show SV
    i]
      show (SBVApp Shr     [a :: SV
    a, i :: SV
    i])            = [String] -> String
    unwords [SV -> String
    forall a. Show a => a -> String
    show SV
    a, ">>", SV -> String
    forall a. Show a => a -> String
    show SV
    i]
      show (SBVApp (Rol i :: Int
    i) [a :: SV
    a])               = [String] -> String
    unwords [SV -> String
    forall a. Show a => a -> String
    show SV
    a, "<<<", Int -> String
    forall a. Show a => a -> String
    show Int
    i]
      show (SBVApp (Ror i :: Int
    i) [a :: SV
    a])               = [String] -> String
    unwords [SV -> String
    forall a. Show a => a -> String
    show SV
    a, ">>>", Int -> String
    forall a. Show a => a -> String
    show Int
    i]
      show (SBVApp (PseudoBoolean pb :: PBOp
    pb) args :: [SV]
    args)   = [String] -> String
    unwords (PBOp -> String
    forall a. Show a => a -> String
    show PBOp
    pb String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : (SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    forall a. Show a => a -> String
    show [SV]
    args)
      show (SBVApp (OverflowOp op :: OvOp
    op)    args :: [SV]
    args)   = [String] -> String
    unwords (OvOp -> String
    forall a. Show a => a -> String
    show OvOp
    op String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : (SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    forall a. Show a => a -> String
    show [SV]
    args)
      show (SBVApp op :: Op
    op                 [a :: SV
    a, b :: SV
    b]) = [String] -> String
    unwords [SV -> String
    forall a. Show a => a -> String
    show SV
    a, Op -> String
    forall a. Show a => a -> String
    show Op
    op, SV -> String
    forall a. Show a => a -> String
    show SV
    b]
      show (SBVApp op :: Op
    op                 args :: [SV]
    args)   = [String] -> String
    unwords (Op -> String
    forall a. Show a => a -> String
    show Op
    op String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : (SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    forall a. Show a => a -> String
    show [SV]
    args)

    -- | A program is a sequence of assignments
    newtype SBVPgm = SBVPgm {SBVPgm -> Seq (SV, SBVExpr)
    pgmAssignments :: S.Seq (SV, SBVExpr)}

    -- | 'NamedSymVar' pairs symbolic values and user given/automatically generated names
    type NamedSymVar = (SV, String)

    -- | Style of optimization. Note that in the pareto case the user is allowed
    -- to specify a max number of fronts to query the solver for, since there might
    -- potentially be an infinite number of them and there is no way to know exactly
    -- how many ahead of time. If 'Nothing' is given, SBV will possibly loop forever
    -- if the number is really infinite.
    data OptimizeStyle = Lexicographic      -- ^ Objectives are optimized in the order given, earlier objectives have higher priority.
                       | Independent        -- ^ Each objective is optimized independently.
                       | Pareto (Maybe Int) -- ^ Objectives are optimized according to pareto front: That is, no objective can be made better without making some other worse.
                       deriving (OptimizeStyle -> OptimizeStyle -> Bool
    (OptimizeStyle -> OptimizeStyle -> Bool)
    -> (OptimizeStyle -> OptimizeStyle -> Bool) -> Eq OptimizeStyle
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: OptimizeStyle -> OptimizeStyle -> Bool
    $c/= :: OptimizeStyle -> OptimizeStyle -> Bool
    == :: OptimizeStyle -> OptimizeStyle -> Bool
    $c== :: OptimizeStyle -> OptimizeStyle -> Bool
    Eq, Int -> OptimizeStyle -> ShowS
    [OptimizeStyle] -> ShowS
    OptimizeStyle -> String
    (Int -> OptimizeStyle -> ShowS)
    -> (OptimizeStyle -> String)
    -> ([OptimizeStyle] -> ShowS)
    -> Show OptimizeStyle
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [OptimizeStyle] -> ShowS
    $cshowList :: [OptimizeStyle] -> ShowS
    show :: OptimizeStyle -> String
    $cshow :: OptimizeStyle -> String
    showsPrec :: Int -> OptimizeStyle -> ShowS
    $cshowsPrec :: Int -> OptimizeStyle -> ShowS
    Show)

    -- | Penalty for a soft-assertion. The default penalty is @1@, with all soft-assertions belonging
    -- to the same objective goal. A positive weight and an optional group can be provided by using
    -- the 'Penalty' constructor.
    data Penalty = DefaultPenalty                  -- ^ Default: Penalty of @1@ and no group attached
                 | Penalty Rational (Maybe String) -- ^ Penalty with a weight and an optional group
                 deriving Int -> Penalty -> ShowS
    [Penalty] -> ShowS
    Penalty -> String
    (Int -> Penalty -> ShowS)
    -> (Penalty -> String) -> ([Penalty] -> ShowS) -> Show Penalty
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Penalty] -> ShowS
    $cshowList :: [Penalty] -> ShowS
    show :: Penalty -> String
    $cshow :: Penalty -> String
    showsPrec :: Int -> Penalty -> ShowS
    $cshowsPrec :: Int -> Penalty -> ShowS
    Show

    -- | Objective of optimization. We can minimize, maximize, or give a soft assertion with a penalty
    -- for not satisfying it.
    data Objective a = Minimize          String a         -- ^ Minimize this metric
                     | Maximize          String a         -- ^ Maximize this metric
                     | AssertWithPenalty String a Penalty -- ^ A soft assertion, with an associated penalty
                     deriving (Int -> Objective a -> ShowS
    [Objective a] -> ShowS
    Objective a -> String
    (Int -> Objective a -> ShowS)
    -> (Objective a -> String)
    -> ([Objective a] -> ShowS)
    -> Show (Objective a)
    forall a. Show a => Int -> Objective a -> ShowS
    forall a. Show a => [Objective a] -> ShowS
    forall a. Show a => Objective a -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Objective a] -> ShowS
    $cshowList :: forall a. Show a => [Objective a] -> ShowS
    show :: Objective a -> String
    $cshow :: forall a. Show a => Objective a -> String
    showsPrec :: Int -> Objective a -> ShowS
    $cshowsPrec :: forall a. Show a => Int -> Objective a -> ShowS
    Show, a -> Objective b -> Objective a
    (a -> b) -> Objective a -> Objective b
    (forall a b. (a -> b) -> Objective a -> Objective b)
    -> (forall a b. a -> Objective b -> Objective a)
    -> Functor Objective
    forall a b. a -> Objective b -> Objective a
    forall a b. (a -> b) -> Objective a -> Objective b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: a -> Objective b -> Objective a
    $c<$ :: forall a b. a -> Objective b -> Objective a
    fmap :: (a -> b) -> Objective a -> Objective b
    $cfmap :: forall a b. (a -> b) -> Objective a -> Objective b
    Functor)

    -- | The name of the objective
    objectiveName :: Objective a -> String
    objectiveName :: Objective a -> String
    objectiveName (Minimize          s :: String
    s _)   = String
    s
    objectiveName (Maximize          s :: String
    s _)   = String
    s
    objectiveName (AssertWithPenalty s :: String
    s _ _) = String
    s

    -- | The state we keep track of as we interact with the solver
    data QueryState = QueryState { QueryState -> Maybe Int -> String -> IO String
    queryAsk                 :: Maybe Int -> String -> IO String
                                 , QueryState -> Maybe Int -> String -> IO ()
    querySend                :: Maybe Int -> String -> IO ()
                                 , QueryState -> Maybe Int -> IO String
    queryRetrieveResponse    :: Maybe Int -> IO String
                                 , QueryState -> SMTConfig
    queryConfig              :: SMTConfig
                                 , QueryState -> IO ()
    queryTerminate           :: IO ()
                                 , QueryState -> Maybe Int
    queryTimeOutValue        :: Maybe Int
                                 , QueryState -> Int
    queryAssertionStackDepth :: Int
                                 }

    -- | Computations which support query operations.
    class Monad m => MonadQuery m where
      queryState :: m State

      default queryState :: (MonadTrans t, MonadQuery m', m ~ t m') => m State
      queryState = m' State -> t m' State
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift m' State
    forall (m :: * -> *). MonadQuery m => m State
    queryState

    instance MonadQuery m             => MonadQuery (ExceptT e m)
    instance MonadQuery m             => MonadQuery (MaybeT m)
    instance MonadQuery m             => MonadQuery (ReaderT r m)
    instance MonadQuery m             => MonadQuery (SS.StateT s m)
    instance MonadQuery m             => MonadQuery (LS.StateT s m)
    instance (MonadQuery m, Monoid w) => MonadQuery (SW.WriterT w m)
    instance (MonadQuery m, Monoid w) => MonadQuery (LW.WriterT w m)

    -- | A query is a user-guided mechanism to directly communicate and extract
    -- results from the solver. A generalization of 'Data.SBV.Query'.
    newtype QueryT m a = QueryT { QueryT m a -> ReaderT State m a
    runQueryT :: ReaderT State m a }
        deriving (Functor (QueryT m)
    a -> QueryT m a
    Functor (QueryT m) =>
    (forall a. a -> QueryT m a)
    -> (forall a b. QueryT m (a -> b) -> QueryT m a -> QueryT m b)
    -> (forall a b c.
        (a -> b -> c) -> QueryT m a -> QueryT m b -> QueryT m c)
    -> (forall a b. QueryT m a -> QueryT m b -> QueryT m b)
    -> (forall a b. QueryT m a -> QueryT m b -> QueryT m a)
    -> Applicative (QueryT m)
    QueryT m a -> QueryT m b -> QueryT m b
    QueryT m a -> QueryT m b -> QueryT m a
    QueryT m (a -> b) -> QueryT m a -> QueryT m b
    (a -> b -> c) -> QueryT m a -> QueryT m b -> QueryT m c
    forall a. a -> QueryT m a
    forall a b. QueryT m a -> QueryT m b -> QueryT m a
    forall a b. QueryT m a -> QueryT m b -> QueryT m b
    forall a b. QueryT m (a -> b) -> QueryT m a -> QueryT m b
    forall a b c.
    (a -> b -> c) -> QueryT m a -> QueryT m b -> QueryT m c
    forall (f :: * -> *).
    Functor f =>
    (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    forall (m :: * -> *). Applicative m => Functor (QueryT m)
    forall (m :: * -> *) a. Applicative m => a -> QueryT m a
    forall (m :: * -> *) a b.
    Applicative m =>
    QueryT m a -> QueryT m b -> QueryT m a
    forall (m :: * -> *) a b.
    Applicative m =>
    QueryT m a -> QueryT m b -> QueryT m b
    forall (m :: * -> *) a b.
    Applicative m =>
    QueryT m (a -> b) -> QueryT m a -> QueryT m b
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> c) -> QueryT m a -> QueryT m b -> QueryT m c
    <* :: QueryT m a -> QueryT m b -> QueryT m a
    $c<* :: forall (m :: * -> *) a b.
    Applicative m =>
    QueryT m a -> QueryT m b -> QueryT m a
    *> :: QueryT m a -> QueryT m b -> QueryT m b
    $c*> :: forall (m :: * -> *) a b.
    Applicative m =>
    QueryT m a -> QueryT m b -> QueryT m b
    liftA2 :: (a -> b -> c) -> QueryT m a -> QueryT m b -> QueryT m c
    $cliftA2 :: forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> c) -> QueryT m a -> QueryT m b -> QueryT m c
    <*> :: QueryT m (a -> b) -> QueryT m a -> QueryT m b
    $c<*> :: forall (m :: * -> *) a b.
    Applicative m =>
    QueryT m (a -> b) -> QueryT m a -> QueryT m b
    pure :: a -> QueryT m a
    $cpure :: forall (m :: * -> *) a. Applicative m => a -> QueryT m a
    $cp1Applicative :: forall (m :: * -> *). Applicative m => Functor (QueryT m)
    Applicative, a -> QueryT m b -> QueryT m a
    (a -> b) -> QueryT m a -> QueryT m b
    (forall a b. (a -> b) -> QueryT m a -> QueryT m b)
    -> (forall a b. a -> QueryT m b -> QueryT m a)
    -> Functor (QueryT m)
    forall a b. a -> QueryT m b -> QueryT m a
    forall a b. (a -> b) -> QueryT m a -> QueryT m b
    forall (m :: * -> *) a b.
    Functor m =>
    a -> QueryT m b -> QueryT m a
    forall (m :: * -> *) a b.
    Functor m =>
    (a -> b) -> QueryT m a -> QueryT m b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: a -> QueryT m b -> QueryT m a
    $c<$ :: forall (m :: * -> *) a b.
    Functor m =>
    a -> QueryT m b -> QueryT m a
    fmap :: (a -> b) -> QueryT m a -> QueryT m b
    $cfmap :: forall (m :: * -> *) a b.
    Functor m =>
    (a -> b) -> QueryT m a -> QueryT m b
    Functor, Applicative (QueryT m)
    a -> QueryT m a
    Applicative (QueryT m) =>
    (forall a b. QueryT m a -> (a -> QueryT m b) -> QueryT m b)
    -> (forall a b. QueryT m a -> QueryT m b -> QueryT m b)
    -> (forall a. a -> QueryT m a)
    -> Monad (QueryT m)
    QueryT m a -> (a -> QueryT m b) -> QueryT m b
    QueryT m a -> QueryT m b -> QueryT m b
    forall a. a -> QueryT m a
    forall a b. QueryT m a -> QueryT m b -> QueryT m b
    forall a b. QueryT m a -> (a -> QueryT m b) -> QueryT m b
    forall (m :: * -> *). Monad m => Applicative (QueryT m)
    forall (m :: * -> *) a. Monad m => a -> QueryT m a
    forall (m :: * -> *) a b.
    Monad m =>
    QueryT m a -> QueryT m b -> QueryT m b
    forall (m :: * -> *) a b.
    Monad m =>
    QueryT m a -> (a -> QueryT m b) -> QueryT m b
    forall (m :: * -> *).
    Applicative m =>
    (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    return :: a -> QueryT m a
    $creturn :: forall (m :: * -> *) a. Monad m => a -> QueryT m a
    >> :: QueryT m a -> QueryT m b -> QueryT m b
    $c>> :: forall (m :: * -> *) a b.
    Monad m =>
    QueryT m a -> QueryT m b -> QueryT m b
    >>= :: QueryT m a -> (a -> QueryT m b) -> QueryT m b
    $c>>= :: forall (m :: * -> *) a b.
    Monad m =>
    QueryT m a -> (a -> QueryT m b) -> QueryT m b
    $cp1Monad :: forall (m :: * -> *). Monad m => Applicative (QueryT m)
    Monad, Monad (QueryT m)
    Monad (QueryT m) =>
    (forall a. IO a -> QueryT m a) -> MonadIO (QueryT m)
    IO a -> QueryT m a
    forall a. IO a -> QueryT m a
    forall (m :: * -> *).
    Monad m =>
    (forall a. IO a -> m a) -> MonadIO m
    forall (m :: * -> *). MonadIO m => Monad (QueryT m)
    forall (m :: * -> *) a. MonadIO m => IO a -> QueryT m a
    liftIO :: IO a -> QueryT m a
    $cliftIO :: forall (m :: * -> *) a. MonadIO m => IO a -> QueryT m a
    $cp1MonadIO :: forall (m :: * -> *). MonadIO m => Monad (QueryT m)
    MonadIO, m a -> QueryT m a
    (forall (m :: * -> *) a. Monad m => m a -> QueryT m a)
    -> MonadTrans QueryT
    forall (m :: * -> *) a. Monad m => m a -> QueryT m a
    forall (t :: (* -> *) -> * -> *).
    (forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
    lift :: m a -> QueryT m a
    $clift :: forall (m :: * -> *) a. Monad m => m a -> QueryT m a
    MonadTrans,
                  MonadError e, MonadState s, MonadWriter w)

    instance Monad m => MonadQuery (QueryT m) where
      queryState :: QueryT m State
    queryState = ReaderT State m State -> QueryT m State
    forall (m :: * -> *) a. ReaderT State m a -> QueryT m a
    QueryT ReaderT State m State
    forall r (m :: * -> *). MonadReader r m => m r
    ask

    mapQueryT :: (ReaderT State m a -> ReaderT State n b) -> QueryT m a -> QueryT n b
    mapQueryT :: (ReaderT State m a -> ReaderT State n b)
    -> QueryT m a -> QueryT n b
    mapQueryT f :: ReaderT State m a -> ReaderT State n b
    f = ReaderT State n b -> QueryT n b
    forall (m :: * -> *) a. ReaderT State m a -> QueryT m a
    QueryT (ReaderT State n b -> QueryT n b)
    -> (QueryT m a -> ReaderT State n b) -> QueryT m a -> QueryT n b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ReaderT State m a -> ReaderT State n b
    f (ReaderT State m a -> ReaderT State n b)
    -> (QueryT m a -> ReaderT State m a)
    -> QueryT m a
    -> ReaderT State n b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QueryT m a -> ReaderT State m a
    forall (m :: * -> *) a. QueryT m a -> ReaderT State m a
    runQueryT
    {-# INLINE mapQueryT #-}

    -- | Create a fresh variable of some type in the underlying query monad transformer.
    -- For further control on how these variables are projected and embedded, see the
    -- 'Queriable' class.
    class Fresh m a where
      fresh :: QueryT m a

    -- | An queriable value. This is a generalization of the 'Fresh' class, in case one needs
    -- to be more specific about how projections/embeddings are done.
    class Queriable m a b | a -> b where
      -- | ^ Create a new symbolic value of type @a@
      create  :: QueryT m a
      -- | ^ Extract the current value in a SAT context
      project :: a -> QueryT m b
      -- | ^ Create a literal value. Morally, 'embed' and 'project' are inverses of each other
      -- via the 'QueryT' monad transformer.
      embed   :: b -> QueryT m a

    -- Have to define this one by hand, because we use ReaderT in the implementation
    instance MonadReader r m => MonadReader r (QueryT m) where
      ask :: QueryT m r
    ask = m r -> QueryT m r
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift m r
    forall r (m :: * -> *). MonadReader r m => m r
    ask
      local :: (r -> r) -> QueryT m a -> QueryT m a
    local f :: r -> r
    f = (ReaderT State m a -> ReaderT State m a)
    -> QueryT m a -> QueryT m a
    forall (m :: * -> *) a (n :: * -> *) b.
    (ReaderT State m a -> ReaderT State n b)
    -> QueryT m a -> QueryT n b
    mapQueryT ((ReaderT State m a -> ReaderT State m a)
     -> QueryT m a -> QueryT m a)
    -> (ReaderT State m a -> ReaderT State m a)
    -> QueryT m a
    -> QueryT m a
    forall a b. (a -> b) -> a -> b
    $ (m a -> m a) -> ReaderT State m a -> ReaderT State m a
    forall (m :: * -> *) a (n :: * -> *) b r.
    (m a -> n b) -> ReaderT r m a -> ReaderT r n b
    mapReaderT ((m a -> m a) -> ReaderT State m a -> ReaderT State m a)
    -> (m a -> m a) -> ReaderT State m a -> ReaderT State m a
    forall a b. (a -> b) -> a -> b
    $ (r -> r) -> m a -> m a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local r -> r
    f

    -- | A query is a user-guided mechanism to directly communicate and extract
    -- results from the solver.
    type Query = QueryT IO

    instance MonadSymbolic Query where
       symbolicEnv :: Query State
    symbolicEnv = Query State
    forall (m :: * -> *). MonadQuery m => m State
    queryState

    instance NFData OptimizeStyle where
       rnf :: OptimizeStyle -> ()
    rnf x :: OptimizeStyle
    x = OptimizeStyle
    x OptimizeStyle -> () -> ()
    forall a b. a -> b -> b
    `seq` ()

    instance NFData Penalty where
       rnf :: Penalty -> ()
    rnf DefaultPenalty  = ()
       rnf (Penalty p :: Rational
    p mbs :: Maybe String
    mbs) = Rational -> ()
    forall a. NFData a => a -> ()
    rnf Rational
    p () -> () -> ()
    forall a b. a -> b -> b
    `seq` Maybe String -> ()
    forall a. NFData a => a -> ()
    rnf Maybe String
    mbs

    instance NFData a => NFData (Objective a) where
       rnf :: Objective a -> ()
    rnf (Minimize          s :: String
    s a :: a
    a)   = String -> ()
    forall a. NFData a => a -> ()
    rnf String
    s () -> () -> ()
    forall a b. a -> b -> b
    `seq` a -> ()
    forall a. NFData a => a -> ()
    rnf a
    a
       rnf (Maximize          s :: String
    s a :: a
    a)   = String -> ()
    forall a. NFData a => a -> ()
    rnf String
    s () -> () -> ()
    forall a b. a -> b -> b
    `seq` a -> ()
    forall a. NFData a => a -> ()
    rnf a
    a
       rnf (AssertWithPenalty s :: String
    s a :: a
    a p :: Penalty
    p) = String -> ()
    forall a. NFData a => a -> ()
    rnf String
    s () -> () -> ()
    forall a b. a -> b -> b
    `seq` a -> ()
    forall a. NFData a => a -> ()
    rnf a
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Penalty -> ()
    forall a. NFData a => a -> ()
    rnf Penalty
    p

    -- | Result of running a symbolic computation
    data Result = Result { Result -> Set Kind
    reskinds       :: Set.Set Kind                                 -- ^ kinds used in the program
                         , Result -> [(String, CV)]
    resTraces      :: [(String, CV)]                               -- ^ quick-check counter-example information (if any)
                         , Result -> [(String, CV -> Bool, SV)]
    resObservables :: [(String, CV -> Bool, SV)]                   -- ^ observable expressions (part of the model)
                         , Result -> [(String, [String])]
    resUISegs      :: [(String, [String])]                         -- ^ uninterpeted code segments
                         , Result -> ([(Quantifier, NamedSymVar)], [NamedSymVar])
    resInputs      :: ([(Quantifier, NamedSymVar)], [NamedSymVar]) -- ^ inputs (possibly existential) + tracker vars
                         , Result -> [(SV, CV)]
    resConsts      :: [(SV, CV)]                                   -- ^ constants
                         , Result -> [((Int, Kind, Kind), [SV])]
    resTables      :: [((Int, Kind, Kind), [SV])]                  -- ^ tables (automatically constructed) (tableno, index-type, result-type) elts
                         , Result -> [(Int, ArrayInfo)]
    resArrays      :: [(Int, ArrayInfo)]                           -- ^ arrays (user specified)
                         , Result -> [(String, SBVType)]
    resUIConsts    :: [(String, SBVType)]                          -- ^ uninterpreted constants
                         , Result -> [(String, [String])]
    resAxioms      :: [(String, [String])]                         -- ^ axioms
                         , Result -> SBVPgm
    resAsgns       :: SBVPgm                                       -- ^ assignments
                         , Result -> Seq (Bool, [(String, String)], SV)
    resConstraints :: S.Seq (Bool, [(String, String)], SV)         -- ^ additional constraints (boolean)
                         , Result -> [(String, Maybe CallStack, SV)]
    resAssertions  :: [(String, Maybe CallStack, SV)]              -- ^ assertions
                         , Result -> [SV]
    resOutputs     :: [SV]                                         -- ^ outputs
                         }

    -- Show instance for 'Result'. Only for debugging purposes.
    instance Show Result where
      -- If there's nothing interesting going on, just print the constant. Note that the
      -- definiton of interesting here is rather subjective; but essentially if we reduced
      -- the result to a single constant already, without any reference to anything.
      show :: Result -> String
    show Result{resConsts :: Result -> [(SV, CV)]
    resConsts=[(SV, CV)]
    cs, resOutputs :: Result -> [SV]
    resOutputs=[r :: SV
    r]}
        | Just c :: CV
    c <- SV
    r SV -> [(SV, CV)] -> Maybe CV
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    `lookup` [(SV, CV)]
    cs
        = CV -> String
    forall a. Show a => a -> String
    show CV
    c
      show (Result kinds :: Set Kind
    kinds _ _ cgs :: [(String, [String])]
    cgs is :: ([(Quantifier, NamedSymVar)], [NamedSymVar])
    is cs :: [(SV, CV)]
    cs ts :: [((Int, Kind, Kind), [SV])]
    ts as :: [(Int, ArrayInfo)]
    as uis :: [(String, SBVType)]
    uis axs :: [(String, [String])]
    axs xs :: SBVPgm
    xs cstrs :: Seq (Bool, [(String, String)], SV)
    cstrs asserts :: [(String, Maybe CallStack, SV)]
    asserts os :: [SV]
    os) = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate "\n" ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $
                       (if [String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    usorts then [] else "SORTS" String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : ShowS -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map ("  " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++) [String]
    usorts)
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ["INPUTS"]
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((Quantifier, NamedSymVar) -> String)
    -> [(Quantifier, NamedSymVar)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (Quantifier, NamedSymVar) -> String
    shn (([(Quantifier, NamedSymVar)], [NamedSymVar])
    -> [(Quantifier, NamedSymVar)]
    forall a b. (a, b) -> a
    fst ([(Quantifier, NamedSymVar)], [NamedSymVar])
    is)
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (if [NamedSymVar] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (([(Quantifier, NamedSymVar)], [NamedSymVar]) -> [NamedSymVar]
    forall a b. (a, b) -> b
    snd ([(Quantifier, NamedSymVar)], [NamedSymVar])
    is) then [] else "TRACKER VARS" String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : (NamedSymVar -> String) -> [NamedSymVar] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Quantifier, NamedSymVar) -> String
    shn ((Quantifier, NamedSymVar) -> String)
    -> (NamedSymVar -> (Quantifier, NamedSymVar))
    -> NamedSymVar
    -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Quantifier
    EX,)) (([(Quantifier, NamedSymVar)], [NamedSymVar]) -> [NamedSymVar]
    forall a b. (a, b) -> b
    snd ([(Quantifier, NamedSymVar)], [NamedSymVar])
    is))
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ["CONSTANTS"]
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((SV, CV) -> [String]) -> [(SV, CV)] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (SV, CV) -> [String]
    forall a. Show a => (SV, a) -> [String]
    shc [(SV, CV)]
    cs
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ["TABLES"]
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (((Int, Kind, Kind), [SV]) -> String)
    -> [((Int, Kind, Kind), [SV])] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Int, Kind, Kind), [SV]) -> String
    forall a a a a.
    (Show a, Show a, Show a, Show a) =>
    ((a, a, a), a) -> String
    sht [((Int, Kind, Kind), [SV])]
    ts
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ["ARRAYS"]
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((Int, ArrayInfo) -> String) -> [(Int, ArrayInfo)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int, ArrayInfo) -> String
    forall a a a a.
    (Show a, Show a, Show a, Show a) =>
    (a, (String, (a, a), a)) -> String
    sha [(Int, ArrayInfo)]
    as
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ["UNINTERPRETED CONSTANTS"]
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((String, SBVType) -> String) -> [(String, SBVType)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, SBVType) -> String
    forall a. Show a => (String, a) -> String
    shui [(String, SBVType)]
    uis
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ["USER GIVEN CODE SEGMENTS"]
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((String, [String]) -> [String])
    -> [(String, [String])] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (String, [String]) -> [String]
    shcg [(String, [String])]
    cgs
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ["AXIOMS"]
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((String, [String]) -> String) -> [(String, [String])] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, [String]) -> String
    shax [(String, [String])]
    axs
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ["DEFINE"]
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((SV, SBVExpr) -> String) -> [(SV, SBVExpr)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(s :: SV
    s, e :: SBVExpr
    e) -> "  " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    shs SV
    s String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " = " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SBVExpr -> String
    forall a. Show a => a -> String
    show SBVExpr
    e) (Seq (SV, SBVExpr) -> [(SV, SBVExpr)]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    F.toList (SBVPgm -> Seq (SV, SBVExpr)
    pgmAssignments SBVPgm
    xs))
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ["CONSTRAINTS"]
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((Bool, [(String, String)], SV) -> String)
    -> [(Bool, [(String, String)], SV)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (("  " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++) ShowS
    -> ((Bool, [(String, String)], SV) -> String)
    -> (Bool, [(String, String)], SV)
    -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Bool, [(String, String)], SV) -> String
    forall a. Show a => (Bool, [(String, String)], a) -> String
    shCstr) (Seq (Bool, [(String, String)], SV)
    -> [(Bool, [(String, String)], SV)]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    F.toList Seq (Bool, [(String, String)], SV)
    cstrs)
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ["ASSERTIONS"]
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((String, Maybe CallStack, SV) -> String)
    -> [(String, Maybe CallStack, SV)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (("  "String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++) ShowS
    -> ((String, Maybe CallStack, SV) -> String)
    -> (String, Maybe CallStack, SV)
    -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String, Maybe CallStack, SV) -> String
    forall a. Show a => (String, Maybe CallStack, a) -> String
    shAssert) [(String, Maybe CallStack, SV)]
    asserts
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ["OUTPUTS"]
                    [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [SV] -> [String]
    forall a. Show a => [a] -> [String]
    sh2 [SV]
    os
        where sh2 :: Show a => [a] -> [String]
              sh2 :: [a] -> [String]
    sh2 = (a -> String) -> [a] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (("  "String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++) ShowS -> (a -> String) -> a -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> String
    forall a. Show a => a -> String
    show)

              usorts :: [String]
    usorts = [String -> Either String [String] -> String
    forall a. String -> Either a [String] -> String
    sh String
    s Either String [String]
    t | KUninterpreted s :: String
    s t :: Either String [String]
    t <- Set Kind -> [Kind]
    forall a. Set a -> [a]
    Set.toList Set Kind
    kinds]
                       where sh :: String -> Either a [String] -> String
    sh s :: String
    s (Left   _) = String
    s
                             sh s :: String
    s (Right es :: [String]
    es) = String
    s String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " (" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", " [String]
    es String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"

              shs :: SV -> String
    shs sv :: SV
    sv = SV -> String
    forall a. Show a => a -> String
    show SV
    sv String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " :: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show (SV -> Kind
    swKind SV
    sv)

              sht :: ((a, a, a), a) -> String
    sht ((i :: a
    i, at :: a
    at, rt :: a
    rt), es :: a
    es)  = "  Table " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    i String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " : " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    at String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "->" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    rt String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " = " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    es

              shc :: (SV, a) -> [String]
    shc (sv :: SV
    sv, cv :: a
    cv)
                | SV
    sv SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV Bool -> Bool -> Bool
    || SV
    sv SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV
                = []
                | Bool
    True
                = ["  " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    sv String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " = " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    cv]

              shcg :: (String, [String]) -> [String]
    shcg (s :: String
    s, ss :: [String]
    ss) = ("Variable: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    s) String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : ShowS -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map ("  " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++) [String]
    ss

              shn :: (Quantifier, NamedSymVar) -> String
    shn (q :: Quantifier
    q, (sv :: SV
    sv, nm :: String
    nm)) = "  " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ni String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " :: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show (SV -> Kind
    swKind SV
    sv) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ex String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    alias
                where ni :: String
    ni = SV -> String
    forall a. Show a => a -> String
    show SV
    sv
                      ex :: String
    ex | Quantifier
    q Quantifier -> Quantifier -> Bool
    forall a. Eq a => a -> a -> Bool
    == Quantifier
    ALL = ""
                         | Bool
    True     = ", existential"
                      alias :: String
    alias | String
    ni String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    nm = ""
                            | Bool
    True     = ", aliasing " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    nm

              sha :: (a, (String, (a, a), a)) -> String
    sha (i :: a
    i, (nm :: String
    nm, (ai :: a
    ai, bi :: a
    bi), ctx :: a
    ctx)) = "  " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ni String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " :: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    ai String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " -> " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    bi String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    alias
                                           String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "\n     Context: "     String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    ctx
                where ni :: String
    ni = "array_" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    i
                      alias :: String
    alias | String
    ni String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    nm = ""
                            | Bool
    True     = ", aliasing " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    nm

              shui :: (String, a) -> String
    shui (nm :: String
    nm, t :: a
    t) = "  [uninterpreted] " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " :: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    t

              shax :: (String, [String]) -> String
    shax (nm :: String
    nm, ss :: [String]
    ss) = "  -- user defined axiom: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "\n  " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate "\n  " [String]
    ss

              shCstr :: (Bool, [(String, String)], a) -> String
    shCstr (isSoft :: Bool
    isSoft, [], c :: a
    c)               = Bool -> String
    soft Bool
    isSoft String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    c
              shCstr (isSoft :: Bool
    isSoft, [(":named", nm :: String
    nm)], c :: a
    c) = Bool -> String
    soft Bool
    isSoft String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ": " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    c
              shCstr (isSoft :: Bool
    isSoft, attrs :: [(String, String)]
    attrs, c :: a
    c)            = Bool -> String
    soft Bool
    isSoft String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    c String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " (attributes: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [(String, String)] -> String
    forall a. Show a => a -> String
    show [(String, String)]
    attrs String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"

              soft :: Bool -> String
    soft True  = "[SOFT] "
              soft False = ""

              shAssert :: (String, Maybe CallStack, a) -> String
    shAssert (nm :: String
    nm, stk :: Maybe CallStack
    stk, p :: a
    p) = "  -- assertion: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String -> (CallStack -> String) -> Maybe CallStack -> String
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe "[No location]"
    #if MIN_VERSION_base(4,9,0)
                    CallStack -> String
    prettyCallStack
    #else
                    showCallStack
    #endif
                    Maybe CallStack
    stk String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ": " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    p

    -- | The context of a symbolic array as created
    data ArrayContext = ArrayFree (Maybe SV)                   -- ^ A new array, the contents are initialized with the given value, if any
                      | ArrayMutate ArrayIndex SV SV           -- ^ An array created by mutating another array at a given cell
                      | ArrayMerge  SV ArrayIndex ArrayIndex   -- ^ An array created by symbolically merging two other arrays

    instance Show ArrayContext where
      show :: ArrayContext -> String
    show (ArrayFree Nothing)   = " initialized with random elements"
      show (ArrayFree (Just sv :: SV
    sv)) = " initialized with " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    sv
      show (ArrayMutate i :: ArrayIndex
    i a :: SV
    a b :: SV
    b)   = " cloned from array_" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ArrayIndex -> String
    forall a. Show a => a -> String
    show ArrayIndex
    i String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " with " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    a String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " :: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show (SV -> Kind
    swKind SV
    a) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " |-> " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    b String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " :: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show (SV -> Kind
    swKind SV
    b)
      show (ArrayMerge  s :: SV
    s i :: ArrayIndex
    i j :: ArrayIndex
    j)   = " merged arrays " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ArrayIndex -> String
    forall a. Show a => a -> String
    show ArrayIndex
    i String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " and " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ArrayIndex -> String
    forall a. Show a => a -> String
    show ArrayIndex
    j String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " on condition " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    s

    -- | Expression map, used for hash-consing
    type ExprMap = Map.Map SBVExpr SV

    -- | Constants are stored in a map, for hash-consing.
    type CnstMap = Map.Map CV SV

    -- | Kinds used in the program; used for determining the final SMT-Lib logic to pick
    type KindSet = Set.Set Kind

    -- | Tables generated during a symbolic run
    type TableMap = Map.Map (Kind, Kind, [SV]) Int

    -- | Representation for symbolic arrays
    type ArrayInfo = (String, (Kind, Kind), ArrayContext)

    -- | SMT Arrays generated during a symbolic run
    type ArrayMap  = IMap.IntMap ArrayInfo

    -- | Functional Arrays generated during a symbolic run
    type FArrayMap  = IMap.IntMap (SVal -> SVal, IORef (IMap.IntMap SV))

    -- | Uninterpreted-constants generated during a symbolic run
    type UIMap     = Map.Map String SBVType

    -- | Code-segments for Uninterpreted-constants, as given by the user
    type CgMap     = Map.Map String [String]

    -- | Cached values, implementing sharing
    type Cache a   = IMap.IntMap [(StableName (State -> IO a), a)]

    -- | Stage of an interactive run
    data IStage = ISetup        -- Before we initiate contact.
                | ISafe         -- In the context of a safe/safeWith call
                | IRun          -- After the contact is started

    -- | Are we cecking safety
    isSafetyCheckingIStage :: IStage -> Bool
    isSafetyCheckingIStage :: IStage -> Bool
    isSafetyCheckingIStage s :: IStage
    s = case IStage
    s of
                                 ISetup -> Bool
    False
                                 ISafe  -> Bool
    True
                                 IRun   -> Bool
    False

    -- | Are we in setup?
    isSetupIStage :: IStage -> Bool
    isSetupIStage :: IStage -> Bool
    isSetupIStage s :: IStage
    s = case IStage
    s of
                       ISetup -> Bool
    True
                       ISafe  -> Bool
    False
                       IRun   -> Bool
    True

    -- | Are we in a run?
    isRunIStage :: IStage -> Bool
    isRunIStage :: IStage -> Bool
    isRunIStage s :: IStage
    s = case IStage
    s of
                      ISetup -> Bool
    False
                      ISafe  -> Bool
    False
                      IRun   -> Bool
    True

    -- | Different means of running a symbolic piece of code
    data SBVRunMode = SMTMode QueryContext IStage Bool SMTConfig                        -- ^ In regular mode, with a stage. Bool is True if this is SAT.
                    | CodeGen                                                           -- ^ Code generation mode.
                    | Concrete (Maybe (Bool, [((Quantifier, NamedSymVar), Maybe CV)]))  -- ^ Concrete simulation mode, with given environment if any. If Nothing: Random.

    -- Show instance for SBVRunMode; debugging purposes only
    instance Show SBVRunMode where
       show :: SBVRunMode -> String
    show (SMTMode qc :: QueryContext
    qc ISetup True  _)  = "Satisfiability setup (" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ QueryContext -> String
    forall a. Show a => a -> String
    show QueryContext
    qc String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
       show (SMTMode qc :: QueryContext
    qc ISafe  True  _)  = "Safety setup (" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ QueryContext -> String
    forall a. Show a => a -> String
    show QueryContext
    qc String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
       show (SMTMode qc :: QueryContext
    qc IRun   True  _)  = "Satisfiability (" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ QueryContext -> String
    forall a. Show a => a -> String
    show QueryContext
    qc String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
       show (SMTMode qc :: QueryContext
    qc ISetup False _)  = "Proof setup (" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ QueryContext -> String
    forall a. Show a => a -> String
    show QueryContext
    qc String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
       show (SMTMode qc :: QueryContext
    qc ISafe  False _)  = ShowS
    forall a. HasCallStack => String -> a
    error ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ "ISafe-False is not an expected/supported combination for SBVRunMode! (" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ QueryContext -> String
    forall a. Show a => a -> String
    show QueryContext
    qc String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
       show (SMTMode qc :: QueryContext
    qc IRun   False _)  = "Proof (" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ QueryContext -> String
    forall a. Show a => a -> String
    show QueryContext
    qc String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
       show CodeGen                      = "Code generation"
       show (Concrete Nothing)           = "Concrete evaluation with random values"
       show (Concrete (Just (True, _)))  = "Concrete evaluation during model validation for sat"
       show (Concrete (Just (False, _))) = "Concrete evaluation during model validation for prove"

    -- | Is this a CodeGen run? (i.e., generating code)
    isCodeGenMode :: State -> IO Bool
    isCodeGenMode :: State -> IO Bool
    isCodeGenMode State{IORef SBVRunMode
    runMode :: State -> IORef SBVRunMode
    runMode :: IORef SBVRunMode
    runMode} = do SBVRunMode
    rm <- IORef SBVRunMode -> IO SBVRunMode
    forall a. IORef a -> IO a
    readIORef IORef SBVRunMode
    runMode
                                      Bool -> IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> IO Bool) -> Bool -> IO Bool
    forall a b. (a -> b) -> a -> b
    $ case SBVRunMode
    rm of
                                                 Concrete{} -> Bool
    False
                                                 SMTMode{}  -> Bool
    False
                                                 CodeGen    -> Bool
    True

    -- | The state in query mode, i.e., additional context
    data IncState = IncState { IncState -> IORef [NamedSymVar]
    rNewInps        :: IORef [NamedSymVar]   -- always existential!
                             , IncState -> IORef (Set Kind)
    rNewKinds       :: IORef KindSet
                             , IncState -> IORef CnstMap
    rNewConsts      :: IORef CnstMap
                             , IncState -> IORef ArrayMap
    rNewArrs        :: IORef ArrayMap
                             , IncState -> IORef TableMap
    rNewTbls        :: IORef TableMap
                             , IncState -> IORef UIMap
    rNewUIs         :: IORef UIMap
                             , IncState -> IORef SBVPgm
    rNewAsgns       :: IORef SBVPgm
                             , IncState -> IORef (Seq (Bool, [(String, String)], SV))
    rNewConstraints :: IORef (S.Seq (Bool, [(String, String)], SV))
                             }

    -- | Get a new IncState
    newIncState :: IO IncState
    newIncState :: IO IncState
    newIncState = do
            IORef [NamedSymVar]
    is    <- [NamedSymVar] -> IO (IORef [NamedSymVar])
    forall a. a -> IO (IORef a)
    newIORef []
            IORef (Set Kind)
    ks    <- Set Kind -> IO (IORef (Set Kind))
    forall a. a -> IO (IORef a)
    newIORef Set Kind
    forall a. Set a
    Set.empty
            IORef CnstMap
    nc    <- CnstMap -> IO (IORef CnstMap)
    forall a. a -> IO (IORef a)
    newIORef CnstMap
    forall k a. Map k a
    Map.empty
            IORef ArrayMap
    am    <- ArrayMap -> IO (IORef ArrayMap)
    forall a. a -> IO (IORef a)
    newIORef ArrayMap
    forall a. IntMap a
    IMap.empty
            IORef TableMap
    tm    <- TableMap -> IO (IORef TableMap)
    forall a. a -> IO (IORef a)
    newIORef TableMap
    forall k a. Map k a
    Map.empty
            IORef UIMap
    ui    <- UIMap -> IO (IORef UIMap)
    forall a. a -> IO (IORef a)
    newIORef UIMap
    forall k a. Map k a
    Map.empty
            IORef SBVPgm
    pgm   <- SBVPgm -> IO (IORef SBVPgm)
    forall a. a -> IO (IORef a)
    newIORef (Seq (SV, SBVExpr) -> SBVPgm
    SBVPgm Seq (SV, SBVExpr)
    forall a. Seq a
    S.empty)
            IORef (Seq (Bool, [(String, String)], SV))
    cstrs <- Seq (Bool, [(String, String)], SV)
    -> IO (IORef (Seq (Bool, [(String, String)], SV)))
    forall a. a -> IO (IORef a)
    newIORef Seq (Bool, [(String, String)], SV)
    forall a. Seq a
    S.empty
            IncState -> IO IncState
    forall (m :: * -> *) a. Monad m => a -> m a
    return IncState :: IORef [NamedSymVar]
    -> IORef (Set Kind)
    -> IORef CnstMap
    -> IORef ArrayMap
    -> IORef TableMap
    -> IORef UIMap
    -> IORef SBVPgm
    -> IORef (Seq (Bool, [(String, String)], SV))
    -> IncState
    IncState { rNewInps :: IORef [NamedSymVar]
    rNewInps        = IORef [NamedSymVar]
    is
                            , rNewKinds :: IORef (Set Kind)
    rNewKinds       = IORef (Set Kind)
    ks
                            , rNewConsts :: IORef CnstMap
    rNewConsts      = IORef CnstMap
    nc
                            , rNewArrs :: IORef ArrayMap
    rNewArrs        = IORef ArrayMap
    am
                            , rNewTbls :: IORef TableMap
    rNewTbls        = IORef TableMap
    tm
                            , rNewUIs :: IORef UIMap
    rNewUIs         = IORef UIMap
    ui
                            , rNewAsgns :: IORef SBVPgm
    rNewAsgns       = IORef SBVPgm
    pgm
                            , rNewConstraints :: IORef (Seq (Bool, [(String, String)], SV))
    rNewConstraints = IORef (Seq (Bool, [(String, String)], SV))
    cstrs
                            }

    -- | Get a new IncState
    withNewIncState :: State -> (State -> IO a) -> IO (IncState, a)
    withNewIncState :: State -> (State -> IO a) -> IO (IncState, a)
    withNewIncState st :: State
    st cont :: State -> IO a
    cont = do
            IncState
    is <- IO IncState
    newIncState
            IORef IncState -> (IncState -> IncState) -> IO ()
    forall a. IORef a -> (a -> a) -> IO ()
    R.modifyIORef' (State -> IORef IncState
    rIncState State
    st) (IncState -> IncState -> IncState
    forall a b. a -> b -> a
    const IncState
    is)
            a
    r  <- State -> IO a
    cont State
    st
            IncState
    finalIncState <- IORef IncState -> IO IncState
    forall a. IORef a -> IO a
    readIORef (State -> IORef IncState
    rIncState State
    st)
            (IncState, a) -> IO (IncState, a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (IncState
    finalIncState, a
    r)

    -- | The state of the symbolic interpreter
    data State  = State { State -> SVal
    pathCond     :: SVal                             -- ^ kind KBool
                        , State -> UTCTime
    startTime    :: UTCTime
                        , State -> IORef SBVRunMode
    runMode      :: IORef SBVRunMode
                        , State -> IORef IncState
    rIncState    :: IORef IncState
                        , State -> IORef [(String, CV)]
    rCInfo       :: IORef [(String, CV)]
                        , State -> IORef [(String, CV -> Bool, SV)]
    rObservables :: IORef [(String, CV -> Bool, SV)]
                        , State -> IORef Int
    rctr         :: IORef Int
                        , State -> IORef (Set Kind)
    rUsedKinds   :: IORef KindSet
                        , State -> IORef (Set String)
    rUsedLbls    :: IORef (Set.Set String)
                        , State
    -> IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    rinps        :: IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set.Set String) -- First : User defined, with proper quantifiers
                                                                                                               -- Second: Internally declared, always existential
                                                                                                               -- Third : Entire set of names, for faster lookup
                        , State -> IORef (Seq (Bool, [(String, String)], SV))
    rConstraints :: IORef (S.Seq (Bool, [(String, String)], SV))
                        , State -> IORef [SV]
    routs        :: IORef [SV]
                        , State -> IORef TableMap
    rtblMap      :: IORef TableMap
                        , State -> IORef SBVPgm
    spgm         :: IORef SBVPgm
                        , State -> IORef CnstMap
    rconstMap    :: IORef CnstMap
                        , State -> IORef ExprMap
    rexprMap     :: IORef ExprMap
                        , State -> IORef ArrayMap
    rArrayMap    :: IORef ArrayMap
                        , State -> IORef FArrayMap
    rFArrayMap   :: IORef FArrayMap
                        , State -> IORef UIMap
    rUIMap       :: IORef UIMap
                        , State -> IORef CgMap
    rCgMap       :: IORef CgMap
                        , State -> IORef [(String, [String])]
    raxioms      :: IORef [(String, [String])]
                        , State -> IORef [SMTOption]
    rSMTOptions  :: IORef [SMTOption]
                        , State -> IORef [Objective (SV, SV)]
    rOptGoals    :: IORef [Objective (SV, SV)]
                        , State -> IORef [(String, Maybe CallStack, SV)]
    rAsserts     :: IORef [(String, Maybe CallStack, SV)]
                        , State -> IORef (Cache SV)
    rSVCache     :: IORef (Cache SV)
                        , State -> IORef (Cache ArrayIndex)
    rAICache     :: IORef (Cache ArrayIndex)
                        , State -> IORef (Cache FArrayIndex)
    rFAICache    :: IORef (Cache FArrayIndex)
                        , State -> IORef (Maybe QueryState)
    rQueryState  :: IORef (Maybe QueryState)
                        }

    -- NFData is a bit of a lie, but it's sufficient, most of the content is iorefs that we don't want to touch
    instance NFData State where
       rnf :: State -> ()
    rnf State{} = ()

    -- | Get the current path condition
    getSValPathCondition :: State -> SVal
    getSValPathCondition :: State -> SVal
    getSValPathCondition = State -> SVal
    pathCond

    -- | Extend the path condition with the given test value.
    extendSValPathCondition :: State -> (SVal -> SVal) -> State
    extendSValPathCondition :: State -> (SVal -> SVal) -> State
    extendSValPathCondition st :: State
    st f :: SVal -> SVal
    f = State
    st{pathCond :: SVal
    pathCond = SVal -> SVal
    f (State -> SVal
    pathCond State
    st)}

    -- | Are we running in proof mode?
    inSMTMode :: State -> IO Bool
    inSMTMode :: State -> IO Bool
    inSMTMode State{IORef SBVRunMode
    runMode :: IORef SBVRunMode
    runMode :: State -> IORef SBVRunMode
    runMode} = do SBVRunMode
    rm <- IORef SBVRunMode -> IO SBVRunMode
    forall a. IORef a -> IO a
    readIORef IORef SBVRunMode
    runMode
                                  Bool -> IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> IO Bool) -> Bool -> IO Bool
    forall a b. (a -> b) -> a -> b
    $ case SBVRunMode
    rm of
                                             CodeGen    -> Bool
    False
                                             Concrete{} -> Bool
    False
                                             SMTMode{}  -> Bool
    True

    -- | The "Symbolic" value. Either a constant (@Left@) or a symbolic
    -- value (@Right Cached@). Note that caching is essential for making
    -- sure sharing is preserved.
    data SVal = SVal !Kind !(Either CV (Cached SV))

    instance HasKind SVal where
      kindOf :: SVal -> Kind
    kindOf (SVal k :: Kind
    k _) = Kind
    k

    -- Show instance for 'SVal'. Not particularly "desirable", but will do if needed
    -- NB. We do not show the type info on constant KBool values, since there's no
    -- implicit "fromBoolean" applied to Booleans in Haskell; and thus a statement
    -- of the form "True :: SBool" is just meaningless. (There should be a fromBoolean!)
    instance Show SVal where
      show :: SVal -> String
    show (SVal KBool (Left c :: CV
    c))  = Bool -> CV -> String
    showCV Bool
    False CV
    c
      show (SVal k :: Kind
    k     (Left c :: CV
    c))  = Bool -> CV -> String
    showCV Bool
    False CV
    c String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " :: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
      show (SVal k :: Kind
    k     (Right _)) =         "<symbolic> :: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k

    -- We really don't want an 'Eq' instance for 'SBV' or 'SVal'. As it really makes no sense.
    -- But since we do want the 'Bits' instance, we're forced to define equality. See
    -- <http://github.com/LeventErkok/sbv/issues/301>. We simply error out.
    -- | This instance is only defined so that we can define an instance for
    -- 'Data.Bits.Bits'. '==' and '/=' simply throw an error.
    instance Eq SVal where
      a :: SVal
    a == :: SVal -> SVal -> Bool
    == b :: SVal
    b = String -> String -> (String, String) -> Bool
    forall a. String -> String -> (String, String) -> a
    noEquals "==" ".==" (SVal -> String
    forall a. Show a => a -> String
    show SVal
    a, SVal -> String
    forall a. Show a => a -> String
    show SVal
    b)
      a :: SVal
    a /= :: SVal -> SVal -> Bool
    /= b :: SVal
    b = String -> String -> (String, String) -> Bool
    forall a. String -> String -> (String, String) -> a
    noEquals "/=" "./=" (SVal -> String
    forall a. Show a => a -> String
    show SVal
    a, SVal -> String
    forall a. Show a => a -> String
    show SVal
    b)

    -- Bail out nicely.
    noEquals :: String -> String -> (String, String) -> a
    noEquals :: String -> String -> (String, String) -> a
    noEquals o :: String
    o n :: String
    n (l :: String
    l, r :: String
    r) = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ ""
                                          , "*** Data.SBV: Comparing symbolic values using Haskell's Eq class!"
                                          , "***"
                                          , "*** Received:    " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    l String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "  " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    r
                                          , "*** Instead use: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    l String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " "  String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    n String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    r
                                          , "***"
                                          , "*** The Eq instance for symbolic values are necessiated only because"
                                          , "*** of the Bits class requirement. You must use symbolic equality"
                                          , "*** operators instead. (And complain to Haskell folks that they"
                                          , "*** remove the 'Eq' superclass from 'Bits'!.)"
                                          ]

    -- | Things we do not support in interactive mode, at least for now!
    noInteractive :: [String] -> a
    noInteractive :: [String] -> a
    noInteractive ss :: [String]
    ss = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $  ""
                                       String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    :  "*** Data.SBV: Unsupported interactive/query mode feature."
                                       String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    :  ShowS -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map ("***  " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++) [String]
    ss
                                       [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ["*** Data.SBV: Please report this as a feature request!"]

    -- | Modification of the state, but carefully handling the interactive tasks.
    -- Note that the state is always updated regardless of the mode, but we get
    -- to also perform extra operation in interactive mode. (Typically error out, but also simply
    -- ignore if it has no impact.)
    modifyState :: State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState :: State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState st :: State
    st@State{IORef SBVRunMode
    runMode :: IORef SBVRunMode
    runMode :: State -> IORef SBVRunMode
    runMode} field :: State -> IORef a
    field update :: a -> a
    update interactiveUpdate :: IO ()
    interactiveUpdate = do
            IORef a -> (a -> a) -> IO ()
    forall a. IORef a -> (a -> a) -> IO ()
    R.modifyIORef' (State -> IORef a
    field State
    st) a -> a
    update
            SBVRunMode
    rm <- IORef SBVRunMode -> IO SBVRunMode
    forall a. IORef a -> IO a
    readIORef IORef SBVRunMode
    runMode
            case SBVRunMode
    rm of
              SMTMode _ IRun _ _ -> IO ()
    interactiveUpdate
              _                  -> () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    -- | Modify the incremental state
    modifyIncState  :: State -> (IncState -> IORef a) -> (a -> a) -> IO ()
    modifyIncState :: State -> (IncState -> IORef a) -> (a -> a) -> IO ()
    modifyIncState State{IORef IncState
    rIncState :: IORef IncState
    rIncState :: State -> IORef IncState
    rIncState} field :: IncState -> IORef a
    field update :: a -> a
    update = do
            IncState
    incState <- IORef IncState -> IO IncState
    forall a. IORef a -> IO a
    readIORef IORef IncState
    rIncState
            IORef a -> (a -> a) -> IO ()
    forall a. IORef a -> (a -> a) -> IO ()
    R.modifyIORef' (IncState -> IORef a
    field IncState
    incState) a -> a
    update

    -- | Add an observable
    recordObservable :: State -> String -> (CV -> Bool) -> SV -> IO ()
    recordObservable :: State -> String -> (CV -> Bool) -> SV -> IO ()
    recordObservable st :: State
    st nm :: String
    nm chk :: CV -> Bool
    chk sv :: SV
    sv = State
    -> (State -> IORef [(String, CV -> Bool, SV)])
    -> ([(String, CV -> Bool, SV)] -> [(String, CV -> Bool, SV)])
    -> IO ()
    -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef [(String, CV -> Bool, SV)]
    rObservables ((String
    nm, CV -> Bool
    chk, SV
    sv)(String, CV -> Bool, SV)
    -> [(String, CV -> Bool, SV)] -> [(String, CV -> Bool, SV)]
    forall a. a -> [a] -> [a]
    :) (() -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())

    -- | Increment the variable counter
    incrementInternalCounter :: State -> IO Int
    incrementInternalCounter :: State -> IO Int
    incrementInternalCounter st :: State
    st = do Int
    ctr <- IORef Int -> IO Int
    forall a. IORef a -> IO a
    readIORef (State -> IORef Int
    rctr State
    st)
                                     State -> (State -> IORef Int) -> (Int -> Int) -> IO () -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef Int
    rctr (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +1) (() -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())
                                     Int -> IO Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    ctr

    -- | Uninterpreted constants and functions. An uninterpreted constant is
    -- a value that is indexed by its name. The only property the prover assumes
    -- about these values are that they are equivalent to themselves; i.e., (for
    -- functions) they return the same results when applied to same arguments.
    -- We support uninterpreted-functions as a general means of black-box'ing
    -- operations that are /irrelevant/ for the purposes of the proof; i.e., when
    -- the proofs can be performed without any knowledge about the function itself.
    svUninterpreted :: Kind -> String -> Maybe [String] -> [SVal] -> SVal
    svUninterpreted :: Kind -> String -> Maybe [String] -> [SVal] -> SVal
    svUninterpreted k :: Kind
    k nm :: String
    nm code :: Maybe [String]
    code args :: [SVal]
    args = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    result
      where result :: State -> IO SV
    result st :: State
    st = do let ty :: SBVType
    ty = [Kind] -> SBVType
    SBVType ((SVal -> Kind) -> [SVal] -> [Kind]
    forall a b. (a -> b) -> [a] -> [b]
    map SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf [SVal]
    args [Kind] -> [Kind] -> [Kind]
    forall a. [a] -> [a] -> [a]
    ++ [Kind
    k])
                           State -> String -> SBVType -> Maybe [String] -> IO ()
    newUninterpreted State
    st String
    nm SBVType
    ty Maybe [String]
    code
                           [SV]
    sws <- (SVal -> IO SV) -> [SVal] -> IO [SV]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (State -> SVal -> IO SV
    svToSV State
    st) [SVal]
    args
                           (SV -> IO ()) -> [SV] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ SV -> IO ()
    forceSVArg [SV]
    sws
                           State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    forall a b. (a -> b) -> a -> b
    $ Op -> [SV] -> SBVExpr
    SBVApp (String -> Op
    Uninterpreted String
    nm) [SV]
    sws

    -- | Create a new uninterpreted symbol, possibly with user given code
    newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO ()
    newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO ()
    newUninterpreted st :: State
    st nm :: String
    nm t :: SBVType
    t mbCode :: Maybe [String]
    mbCode
      | String -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null String
    nm Bool -> Bool -> Bool
    || Bool -> Bool
    not Bool
    enclosed Bool -> Bool -> Bool
    && (Bool -> Bool
    not (Char -> Bool
    isAlpha (String -> Char
    forall a. [a] -> a
    head String
    nm)) Bool -> Bool -> Bool
    || Bool -> Bool
    not ((Char -> Bool) -> String -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Char -> Bool
    validChar (ShowS
    forall a. [a] -> [a]
    tail String
    nm)))
      = String -> IO ()
    forall a. HasCallStack => String -> a
    error (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ "Bad uninterpreted constant name: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    nm String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ". Must be a valid identifier."
      | Bool
    True = do UIMap
    uiMap <- IORef UIMap -> IO UIMap
    forall a. IORef a -> IO a
    readIORef (State -> IORef UIMap
    rUIMap State
    st)
                  case String
    nm String -> UIMap -> Maybe SBVType
    forall k a. Ord k => k -> Map k a -> Maybe a
    `Map.lookup` UIMap
    uiMap of
                    Just t' :: SBVType
    t' -> SBVType -> IO () -> IO ()
    forall r. SBVType -> r -> r
    checkType SBVType
    t' (() -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())
                    Nothing -> do State
    -> (State -> IORef UIMap) -> (UIMap -> UIMap) -> IO () -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef UIMap
    rUIMap (String -> SBVType -> UIMap -> UIMap
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert String
    nm SBVType
    t)
                                            (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ State -> (IncState -> IORef UIMap) -> (UIMap -> UIMap) -> IO ()
    forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
    modifyIncState State
    st IncState -> IORef UIMap
    rNewUIs (\newUIs :: UIMap
    newUIs -> case String
    nm String -> UIMap -> Maybe SBVType
    forall k a. Ord k => k -> Map k a -> Maybe a
    `Map.lookup` UIMap
    newUIs of
                                                                                      Just t' :: SBVType
    t' -> SBVType -> UIMap -> UIMap
    forall r. SBVType -> r -> r
    checkType SBVType
    t' UIMap
    newUIs
                                                                                      Nothing -> String -> SBVType -> UIMap -> UIMap
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert String
    nm SBVType
    t UIMap
    newUIs)

                                  -- No need to record the code in interactive mode: CodeGen doesn't use interactive
                                  Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Maybe [String] -> Bool
    forall a. Maybe a -> Bool
    isJust Maybe [String]
    mbCode) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ State
    -> (State -> IORef CgMap) -> (CgMap -> CgMap) -> IO () -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef CgMap
    rCgMap (String -> [String] -> CgMap -> CgMap
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert String
    nm (Maybe [String] -> [String]
    forall a. HasCallStack => Maybe a -> a
    fromJust Maybe [String]
    mbCode)) (() -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())
      where checkType :: SBVType -> r -> r
            checkType :: SBVType -> r -> r
    checkType t' :: SBVType
    t' cont :: r
    cont
              | SBVType
    t SBVType -> SBVType -> Bool
    forall a. Eq a => a -> a -> Bool
    /= SBVType
    t' = String -> r
    forall a. HasCallStack => String -> a
    error (String -> r) -> String -> r
    forall a b. (a -> b) -> a -> b
    $  "Uninterpreted constant " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    nm String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " used at incompatible types\n"
                                String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "      Current type      : " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SBVType -> String
    forall a. Show a => a -> String
    show SBVType
    t String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "\n"
                                String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "      Previously used at: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SBVType -> String
    forall a. Show a => a -> String
    show SBVType
    t'
              | Bool
    True    = r
    cont

            validChar :: Char -> Bool
    validChar x :: Char
    x = Char -> Bool
    isAlphaNum Char
    x Bool -> Bool -> Bool
    || Char
    x Char -> String -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` "_"
            enclosed :: Bool
    enclosed    = String -> Char
    forall a. [a] -> a
    head String
    nm Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == '|' Bool -> Bool -> Bool
    && String -> Char
    forall a. [a] -> a
    last String
    nm Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == '|' Bool -> Bool -> Bool
    && String -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    nm Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 2 Bool -> Bool -> Bool
    && Bool -> Bool
    not ((Char -> Bool) -> String -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (Char -> String -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` "|\\") (ShowS
    forall a. [a] -> [a]
    tail (ShowS
    forall a. [a] -> [a]
    init String
    nm)))

    -- | Add a new sAssert based constraint
    addAssertion :: State -> Maybe CallStack -> String -> SV -> IO ()
    addAssertion :: State -> Maybe CallStack -> String -> SV -> IO ()
    addAssertion st :: State
    st cs :: Maybe CallStack
    cs msg :: String
    msg cond :: SV
    cond = State
    -> (State -> IORef [(String, Maybe CallStack, SV)])
    -> ([(String, Maybe CallStack, SV)]
        -> [(String, Maybe CallStack, SV)])
    -> IO ()
    -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef [(String, Maybe CallStack, SV)]
    rAsserts ((String
    msg, Maybe CallStack
    cs, SV
    cond)(String, Maybe CallStack, SV)
    -> [(String, Maybe CallStack, SV)]
    -> [(String, Maybe CallStack, SV)]
    forall a. a -> [a] -> [a]
    :)
                                            (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> IO ()
    forall a. [String] -> a
    noInteractive [ "Named assertions (sAssert):"
                                                            , "  Tag: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    msg
                                                            , "  Loc: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String -> (CallStack -> String) -> Maybe CallStack -> String
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe "Unknown" CallStack -> String
    forall a. Show a => a -> String
    show Maybe CallStack
    cs
                                                            ]

    -- | Create an internal variable, which acts as an input but isn't visible to the user.
    -- Such variables are existentially quantified in a SAT context, and universally quantified
    -- in a proof context.
    internalVariable :: State -> Kind -> IO SV
    internalVariable :: State -> Kind -> IO SV
    internalVariable st :: State
    st k :: Kind
    k = do (sv :: SV
    sv, nm :: String
    nm) <- State -> Kind -> IO NamedSymVar
    newSV State
    st Kind
    k
                               SBVRunMode
    rm <- IORef SBVRunMode -> IO SBVRunMode
    forall a. IORef a -> IO a
    readIORef (State -> IORef SBVRunMode
    runMode State
    st)
                               let q :: Quantifier
    q = case SBVRunMode
    rm of
                                         SMTMode  _ _ True  _ -> Quantifier
    EX
                                         SMTMode  _ _ False _ -> Quantifier
    ALL
                                         CodeGen              -> Quantifier
    ALL
                                         Concrete{}           -> Quantifier
    ALL
                                   n :: String
    n = "__internal_sbv_" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    nm
                                   v :: NamedSymVar
    v = (SV
    sv, String
    n)
                               State
    -> (State
        -> IORef
             (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String))
    -> ((([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
        -> (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String))
    -> IO ()
    -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State
    -> IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    rinps (([(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)])
    -> ([(Quantifier, NamedSymVar)], [NamedSymVar])
    -> ([(Quantifier, NamedSymVar)], [NamedSymVar])
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (b, d) (c, d)
    first ((Quantifier
    q, NamedSymVar
    v) (Quantifier, NamedSymVar)
    -> [(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)]
    forall a. a -> [a] -> [a]
    :) (([(Quantifier, NamedSymVar)], [NamedSymVar])
     -> ([(Quantifier, NamedSymVar)], [NamedSymVar]))
    -> (Set String -> Set String)
    -> (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    -> (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** String -> Set String -> Set String
    forall a. Ord a => a -> Set a -> Set a
    Set.insert String
    n)
                                         (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ State
    -> (IncState -> IORef [NamedSymVar])
    -> ([NamedSymVar] -> [NamedSymVar])
    -> IO ()
    forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
    modifyIncState State
    st IncState -> IORef [NamedSymVar]
    rNewInps (\newInps :: [NamedSymVar]
    newInps -> case Quantifier
    q of
                                                                                     EX -> NamedSymVar
    v NamedSymVar -> [NamedSymVar] -> [NamedSymVar]
    forall a. a -> [a] -> [a]
    : [NamedSymVar]
    newInps
                                                                                     -- I don't think the following can actually happen
                                                                                     -- but just be safe:
                                                                                     ALL  -> [String] -> [NamedSymVar]
    forall a. [String] -> a
    noInteractive [ "Internal universally quantified variable creation:"
                                                                                                           , "  Named: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    nm
                                                                                                           ])
                               SV -> IO SV
    forall (m :: * -> *) a. Monad m => a -> m a
    return SV
    sv
    {-# INLINE internalVariable #-}

    -- | Create a new SV
    newSV :: State -> Kind -> IO (SV, String)
    newSV :: State -> Kind -> IO NamedSymVar
    newSV st :: State
    st k :: Kind
    k = do Int
    ctr <- State -> IO Int
    incrementInternalCounter State
    st
                    let sv :: SV
    sv = Kind -> NodeId -> SV
    SV Kind
    k (Int -> NodeId
    NodeId Int
    ctr)
                    State -> Kind -> IO ()
    registerKind State
    st Kind
    k
                    NamedSymVar -> IO NamedSymVar
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SV
    sv, 's' Char -> ShowS
    forall a. a -> [a] -> [a]
    : Int -> String
    forall a. Show a => a -> String
    show Int
    ctr)
    {-# INLINE newSV #-}

    -- | Register a new kind with the system, used for uninterpreted sorts.
    -- NB: Is it safe to have new kinds in query mode? It could be that
    -- the new kind might introduce a constraint that effects the logic. For
    -- instance, if we're seeing 'Double' for the first time and using a BV
    -- logic, then things would fall apart. But this should be rare, and hopefully
    -- the success-response checking mechanism will catch the rare cases where this
    -- is an issue. In either case, the user can always arrange for the right
    -- logic by calling 'Data.SBV.setLogic' appropriately, so it seems safe to just
    -- allow for this.
    registerKind :: State -> Kind -> IO ()
    registerKind :: State -> Kind -> IO ()
    registerKind st :: State
    st k :: Kind
    k
      | KUninterpreted sortName :: String
    sortName _ <- Kind
    k, (Char -> Char) -> ShowS
    forall a b. (a -> b) -> [a] -> [b]
    map Char -> Char
    toLower String
    sortName String -> [String] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [String]
    smtLibReservedNames
      = String -> IO ()
    forall a. HasCallStack => String -> a
    error (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ "SBV: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    sortName String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " is a reserved sort; please use a different name."
      | Bool
    True
      = do -- Adding a kind to the incState is tricky; we only need to add it
           --     *    If it's an uninterpreted sort that's not already in the general state
           --     * OR If it's a tuple-sort whose cardinality isn't already in the general state
           --     * OR If it's a list that's not already in the general state (so we can send the flatten commands)

           Set Kind
    existingKinds <- IORef (Set Kind) -> IO (Set Kind)
    forall a. IORef a -> IO a
    readIORef (State -> IORef (Set Kind)
    rUsedKinds State
    st)

           State
    -> (State -> IORef (Set Kind))
    -> (Set Kind -> Set Kind)
    -> IO ()
    -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef (Set Kind)
    rUsedKinds (Kind -> Set Kind -> Set Kind
    forall a. Ord a => a -> Set a -> Set a
    Set.insert Kind
    k) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ do

                              -- Why do we discriminate here? Because the incremental context is sensitive to the
                              -- order: In particular, if an uninterpreted kind is already in there, we don't
                              -- want to re-add because double-declaration would be wrong. See 'cvtInc' for details.
                              let needsAdding :: Bool
    needsAdding = case Kind
    k of
                                                  KUninterpreted{} -> Kind
    k Kind -> Set Kind -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` Set Kind
    existingKinds
                                                  KList{}          -> Kind
    k Kind -> Set Kind -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` Set Kind
    existingKinds
                                                  KTuple nks :: [Kind]
    nks       -> [Kind] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Kind]
    nks Int -> [Int] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` [[Kind] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Kind]
    oks | KTuple oks :: [Kind]
    oks <- Set Kind -> [Kind]
    forall a. Set a -> [a]
    Set.toList Set Kind
    existingKinds]
                                                  KMaybe{}         -> Kind
    k Kind -> Set Kind -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` Set Kind
    existingKinds
                                                  KEither{}        -> Kind
    k Kind -> Set Kind -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` Set Kind
    existingKinds
                                                  _                -> Bool
    False

                              Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    needsAdding (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ State
    -> (IncState -> IORef (Set Kind))
    -> (Set Kind -> Set Kind)
    -> IO ()
    forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
    modifyIncState State
    st IncState -> IORef (Set Kind)
    rNewKinds (Kind -> Set Kind -> Set Kind
    forall a. Ord a => a -> Set a -> Set a
    Set.insert Kind
    k)

           -- Don't forget to register subkinds!
           case Kind
    k of
             KBool          {}    -> () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
             KBounded       {}    -> () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
             KUnbounded     {}    -> () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
             KReal          {}    -> () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
             KUninterpreted {}    -> () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
             KFloat         {}    -> () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
             KDouble        {}    -> () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
             KChar          {}    -> () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
             KString        {}    -> () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
             KList          ek :: Kind
    ek    -> State -> Kind -> IO ()
    registerKind State
    st Kind
    ek
             KSet           ek :: Kind
    ek    -> State -> Kind -> IO ()
    registerKind State
    st Kind
    ek
             KTuple         eks :: [Kind]
    eks   -> (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]
    eks
             KMaybe         ke :: Kind
    ke    -> State -> Kind -> IO ()
    registerKind State
    st Kind
    ke
             KEither        k1 :: Kind
    k1 k2 :: Kind
    k2 -> (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
    k1, Kind
    k2]

    -- | Register a new label with the system, making sure they are unique and have no '|'s in them
    registerLabel :: String -> State -> String -> IO ()
    registerLabel :: String -> State -> String -> IO ()
    registerLabel whence :: String
    whence st :: State
    st nm :: String
    nm
      | (Char -> Char) -> ShowS
    forall a b. (a -> b) -> [a] -> [b]
    map Char -> Char
    toLower String
    nm String -> [String] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [String]
    smtLibReservedNames
      = String -> IO ()
    err "is a reserved string; please use a different name."
      | '|' Char -> String -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` String
    nm
      = String -> IO ()
    err "contains the character `|', which is not allowed!"
      | '\\' Char -> String -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` String
    nm
      = String -> IO ()
    err "contains the character `\\', which is not allowed!"
      | Bool
    True
      = do Set String
    old <- IORef (Set String) -> IO (Set String)
    forall a. IORef a -> IO a
    readIORef (IORef (Set String) -> IO (Set String))
    -> IORef (Set String) -> IO (Set String)
    forall a b. (a -> b) -> a -> b
    $ State -> IORef (Set String)
    rUsedLbls State
    st
           if String
    nm String -> Set String -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set String
    old
              then String -> IO ()
    err "is used multiple times. Please do not use duplicate names!"
              else State
    -> (State -> IORef (Set String))
    -> (Set String -> Set String)
    -> IO ()
    -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef (Set String)
    rUsedLbls (String -> Set String -> Set String
    forall a. Ord a => a -> Set a -> Set a
    Set.insert String
    nm) (() -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())

      where err :: String -> IO ()
    err w :: String
    w = String -> IO ()
    forall a. HasCallStack => String -> a
    error (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ "SBV (" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    whence String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "): " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    nm String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    w

    -- | Create a new constant; hash-cons as necessary
    newConst :: State -> CV -> IO SV
    newConst :: State -> CV -> IO SV
    newConst st :: State
    st c :: CV
    c = do
      CnstMap
    constMap <- IORef CnstMap -> IO CnstMap
    forall a. IORef a -> IO a
    readIORef (State -> IORef CnstMap
    rconstMap State
    st)
      case CV
    c CV -> CnstMap -> Maybe SV
    forall k a. Ord k => k -> Map k a -> Maybe a
    `Map.lookup` CnstMap
    constMap of
        -- NB. Unlike in 'newExpr', we don't have to make sure the returned sv
        -- has the kind we asked for, because the constMap stores the full CV
        -- which already has a kind field in it.
        Just sv :: SV
    sv -> SV -> IO SV
    forall (m :: * -> *) a. Monad m => a -> m a
    return SV
    sv
        Nothing -> do (sv :: SV
    sv, _) <- State -> Kind -> IO NamedSymVar
    newSV State
    st (CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    c)
                      let ins :: CnstMap -> CnstMap
    ins = CV -> SV -> CnstMap -> CnstMap
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert CV
    c SV
    sv
                      State
    -> (State -> IORef CnstMap)
    -> (CnstMap -> CnstMap)
    -> IO ()
    -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef CnstMap
    rconstMap CnstMap -> CnstMap
    ins (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ State
    -> (IncState -> IORef CnstMap) -> (CnstMap -> CnstMap) -> IO ()
    forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
    modifyIncState State
    st IncState -> IORef CnstMap
    rNewConsts CnstMap -> CnstMap
    ins
                      SV -> IO SV
    forall (m :: * -> *) a. Monad m => a -> m a
    return SV
    sv
    {-# INLINE newConst #-}

    -- | Create a new table; hash-cons as necessary
    getTableIndex :: State -> Kind -> Kind -> [SV] -> IO Int
    getTableIndex :: State -> Kind -> Kind -> [SV] -> IO Int
    getTableIndex st :: State
    st at :: Kind
    at rt :: Kind
    rt elts :: [SV]
    elts = do
      let key :: (Kind, Kind, [SV])
    key = (Kind
    at, Kind
    rt, [SV]
    elts)
      TableMap
    tblMap <- IORef TableMap -> IO TableMap
    forall a. IORef a -> IO a
    readIORef (State -> IORef TableMap
    rtblMap State
    st)
      case (Kind, Kind, [SV])
    key (Kind, Kind, [SV]) -> TableMap -> Maybe Int
    forall k a. Ord k => k -> Map k a -> Maybe a
    `Map.lookup` TableMap
    tblMap of
        Just i :: Int
    i -> Int -> IO Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    i
        _      -> do let i :: Int
    i   = TableMap -> Int
    forall k a. Map k a -> Int
    Map.size TableMap
    tblMap
                         upd :: TableMap -> TableMap
    upd = (Kind, Kind, [SV]) -> Int -> TableMap -> TableMap
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert (Kind, Kind, [SV])
    key Int
    i
                     State
    -> (State -> IORef TableMap)
    -> (TableMap -> TableMap)
    -> IO ()
    -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef TableMap
    rtblMap TableMap -> TableMap
    upd (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ State
    -> (IncState -> IORef TableMap) -> (TableMap -> TableMap) -> IO ()
    forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
    modifyIncState State
    st IncState -> IORef TableMap
    rNewTbls TableMap -> TableMap
    upd
                     Int -> IO Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    i

    -- | Create a new expression; hash-cons as necessary
    newExpr :: State -> Kind -> SBVExpr -> IO SV
    newExpr :: State -> Kind -> SBVExpr -> IO SV
    newExpr st :: State
    st k :: Kind
    k app :: SBVExpr
    app = do
       let e :: SBVExpr
    e = SBVExpr -> SBVExpr
    reorder SBVExpr
    app
       ExprMap
    exprMap <- IORef ExprMap -> IO ExprMap
    forall a. IORef a -> IO a
    readIORef (State -> IORef ExprMap
    rexprMap State
    st)
       case SBVExpr
    e SBVExpr -> ExprMap -> Maybe SV
    forall k a. Ord k => k -> Map k a -> Maybe a
    `Map.lookup` ExprMap
    exprMap of
         -- NB. Check to make sure that the kind of the hash-consed value
         -- is the same kind as we're requesting. This might look unnecessary,
         -- at first, but `svSign` and `svUnsign` rely on this as we can
         -- get the same expression but at a different type. See
         -- <http://github.com/GaloisInc/cryptol/issues/566> as an example.
         Just sv :: SV
    sv | SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SV
    sv Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    k -> SV -> IO SV
    forall (m :: * -> *) a. Monad m => a -> m a
    return SV
    sv
         _                        -> do (sv :: SV
    sv, _) <- State -> Kind -> IO NamedSymVar
    newSV State
    st Kind
    k
                                        let append :: SBVPgm -> SBVPgm
    append (SBVPgm xs :: Seq (SV, SBVExpr)
    xs) = Seq (SV, SBVExpr) -> SBVPgm
    SBVPgm (Seq (SV, SBVExpr)
    xs Seq (SV, SBVExpr) -> (SV, SBVExpr) -> Seq (SV, SBVExpr)
    forall a. Seq a -> a -> Seq a
    S.|> (SV
    sv, SBVExpr
    e))
                                        State
    -> (State -> IORef SBVPgm) -> (SBVPgm -> SBVPgm) -> IO () -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef SBVPgm
    spgm SBVPgm -> SBVPgm
    append (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ State -> (IncState -> IORef SBVPgm) -> (SBVPgm -> SBVPgm) -> IO ()
    forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
    modifyIncState State
    st IncState -> IORef SBVPgm
    rNewAsgns SBVPgm -> SBVPgm
    append
                                        State
    -> (State -> IORef ExprMap)
    -> (ExprMap -> ExprMap)
    -> IO ()
    -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef ExprMap
    rexprMap (SBVExpr -> SV -> ExprMap -> ExprMap
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert SBVExpr
    e SV
    sv) (() -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())
                                        SV -> IO SV
    forall (m :: * -> *) a. Monad m => a -> m a
    return SV
    sv
    {-# INLINE newExpr #-}

    -- | Convert a symbolic value to an internal SV
    svToSV :: State -> SVal -> IO SV
    svToSV :: State -> SVal -> IO SV
    svToSV st :: State
    st (SVal _ (Left c :: CV
    c))  = State -> CV -> IO SV
    newConst State
    st CV
    c
    svToSV st :: State
    st (SVal _ (Right f :: Cached SV
    f)) = Cached SV -> State -> IO SV
    uncache Cached SV
    f State
    st

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

    -------------------------------------------------------------------------
    -- * Symbolic Computations
    -------------------------------------------------------------------------
    -- | A Symbolic computation. Represented by a reader monad carrying the
    -- state of the computation, layered on top of IO for creating unique
    -- references to hold onto intermediate results.

    -- | Computations which support symbolic operations
    class MonadIO m => MonadSymbolic m where
      symbolicEnv :: m State

      default symbolicEnv :: (MonadTrans t, MonadSymbolic m', m ~ t m') => m State
      symbolicEnv = m' State -> t m' State
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift m' State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv

    instance MonadSymbolic m             => MonadSymbolic (ExceptT e m)
    instance MonadSymbolic m             => MonadSymbolic (MaybeT m)
    instance MonadSymbolic m             => MonadSymbolic (ReaderT r m)
    instance MonadSymbolic m             => MonadSymbolic (SS.StateT s m)
    instance MonadSymbolic m             => MonadSymbolic (LS.StateT s m)
    instance (MonadSymbolic m, Monoid w) => MonadSymbolic (SW.WriterT w m)
    instance (MonadSymbolic m, Monoid w) => MonadSymbolic (LW.WriterT w m)

    -- | A generalization of 'Data.SBV.Symbolic'.
    newtype SymbolicT m a = SymbolicT { SymbolicT m a -> ReaderT State m a
    runSymbolicT :: ReaderT State m a }
                       deriving ( Functor (SymbolicT m)
    a -> SymbolicT m a
    Functor (SymbolicT m) =>
    (forall a. a -> SymbolicT m a)
    -> (forall a b.
        SymbolicT m (a -> b) -> SymbolicT m a -> SymbolicT m b)
    -> (forall a b c.
        (a -> b -> c) -> SymbolicT m a -> SymbolicT m b -> SymbolicT m c)
    -> (forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b)
    -> (forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m a)
    -> Applicative (SymbolicT m)
    SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    SymbolicT m a -> SymbolicT m b -> SymbolicT m a
    SymbolicT m (a -> b) -> SymbolicT m a -> SymbolicT m b
    (a -> b -> c) -> SymbolicT m a -> SymbolicT m b -> SymbolicT m c
    forall a. a -> SymbolicT m a
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m a
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall a b. SymbolicT m (a -> b) -> SymbolicT m a -> SymbolicT m b
    forall a b c.
    (a -> b -> c) -> SymbolicT m a -> SymbolicT m b -> SymbolicT m c
    forall (f :: * -> *).
    Functor f =>
    (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    forall (m :: * -> *). Applicative m => Functor (SymbolicT m)
    forall (m :: * -> *) a. Applicative m => a -> SymbolicT m a
    forall (m :: * -> *) a b.
    Applicative m =>
    SymbolicT m a -> SymbolicT m b -> SymbolicT m a
    forall (m :: * -> *) a b.
    Applicative m =>
    SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b.
    Applicative m =>
    SymbolicT m (a -> b) -> SymbolicT m a -> SymbolicT m b
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> c) -> SymbolicT m a -> SymbolicT m b -> SymbolicT m c
    <* :: SymbolicT m a -> SymbolicT m b -> SymbolicT m a
    $c<* :: forall (m :: * -> *) a b.
    Applicative m =>
    SymbolicT m a -> SymbolicT m b -> SymbolicT m a
    *> :: SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    $c*> :: forall (m :: * -> *) a b.
    Applicative m =>
    SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    liftA2 :: (a -> b -> c) -> SymbolicT m a -> SymbolicT m b -> SymbolicT m c
    $cliftA2 :: forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> c) -> SymbolicT m a -> SymbolicT m b -> SymbolicT m c
    <*> :: SymbolicT m (a -> b) -> SymbolicT m a -> SymbolicT m b
    $c<*> :: forall (m :: * -> *) a b.
    Applicative m =>
    SymbolicT m (a -> b) -> SymbolicT m a -> SymbolicT m b
    pure :: a -> SymbolicT m a
    $cpure :: forall (m :: * -> *) a. Applicative m => a -> SymbolicT m a
    $cp1Applicative :: forall (m :: * -> *). Applicative m => Functor (SymbolicT m)
    Applicative, a -> SymbolicT m b -> SymbolicT m a
    (a -> b) -> SymbolicT m a -> SymbolicT m b
    (forall a b. (a -> b) -> SymbolicT m a -> SymbolicT m b)
    -> (forall a b. a -> SymbolicT m b -> SymbolicT m a)
    -> Functor (SymbolicT m)
    forall a b. a -> SymbolicT m b -> SymbolicT m a
    forall a b. (a -> b) -> SymbolicT m a -> SymbolicT m b
    forall (m :: * -> *) a b.
    Functor m =>
    a -> SymbolicT m b -> SymbolicT m a
    forall (m :: * -> *) a b.
    Functor m =>
    (a -> b) -> SymbolicT m a -> SymbolicT m b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: a -> SymbolicT m b -> SymbolicT m a
    $c<$ :: forall (m :: * -> *) a b.
    Functor m =>
    a -> SymbolicT m b -> SymbolicT m a
    fmap :: (a -> b) -> SymbolicT m a -> SymbolicT m b
    $cfmap :: forall (m :: * -> *) a b.
    Functor m =>
    (a -> b) -> SymbolicT m a -> SymbolicT m b
    Functor, Applicative (SymbolicT m)
    a -> SymbolicT m a
    Applicative (SymbolicT m) =>
    (forall a b.
     SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b)
    -> (forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b)
    -> (forall a. a -> SymbolicT m a)
    -> Monad (SymbolicT m)
    SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall a. a -> SymbolicT m a
    forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *). Monad m => Applicative (SymbolicT m)
    forall (m :: * -> *) a. Monad m => a -> SymbolicT m a
    forall (m :: * -> *) a b.
    Monad m =>
    SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    forall (m :: * -> *) a b.
    Monad m =>
    SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    forall (m :: * -> *).
    Applicative m =>
    (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    return :: a -> SymbolicT m a
    $creturn :: forall (m :: * -> *) a. Monad m => a -> SymbolicT m a
    >> :: SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    $c>> :: forall (m :: * -> *) a b.
    Monad m =>
    SymbolicT m a -> SymbolicT m b -> SymbolicT m b
    >>= :: SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    $c>>= :: forall (m :: * -> *) a b.
    Monad m =>
    SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
    $cp1Monad :: forall (m :: * -> *). Monad m => Applicative (SymbolicT m)
    Monad, Monad (SymbolicT m)
    Monad (SymbolicT m) =>
    (forall a. IO a -> SymbolicT m a) -> MonadIO (SymbolicT m)
    IO a -> SymbolicT m a
    forall a. IO a -> SymbolicT m a
    forall (m :: * -> *).
    Monad m =>
    (forall a. IO a -> m a) -> MonadIO m
    forall (m :: * -> *). MonadIO m => Monad (SymbolicT m)
    forall (m :: * -> *) a. MonadIO m => IO a -> SymbolicT m a
    liftIO :: IO a -> SymbolicT m a
    $cliftIO :: forall (m :: * -> *) a. MonadIO m => IO a -> SymbolicT m a
    $cp1MonadIO :: forall (m :: * -> *). MonadIO m => Monad (SymbolicT m)
    MonadIO, m a -> SymbolicT m a
    (forall (m :: * -> *) a. Monad m => m a -> SymbolicT m a)
    -> MonadTrans SymbolicT
    forall (m :: * -> *) a. Monad m => m a -> SymbolicT m a
    forall (t :: (* -> *) -> * -> *).
    (forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
    lift :: m a -> SymbolicT m a
    $clift :: forall (m :: * -> *) a. Monad m => m a -> SymbolicT m a
    MonadTrans
                                , MonadError e, MonadState s, MonadWriter w
    #if MIN_VERSION_base(4,11,0)
                                , Monad (SymbolicT m)
    Monad (SymbolicT m) =>
    (forall a. String -> SymbolicT m a) -> MonadFail (SymbolicT m)
    String -> SymbolicT m a
    forall a. String -> SymbolicT m a
    forall (m :: * -> *).
    Monad m =>
    (forall a. String -> m a) -> MonadFail m
    forall (m :: * -> *). MonadFail m => Monad (SymbolicT m)
    forall (m :: * -> *) a. MonadFail m => String -> SymbolicT m a
    fail :: String -> SymbolicT m a
    $cfail :: forall (m :: * -> *) a. MonadFail m => String -> SymbolicT m a
    $cp1MonadFail :: forall (m :: * -> *). MonadFail m => Monad (SymbolicT m)
    Fail.MonadFail
    #endif
                                )

    -- | `MonadSymbolic` instance for `SymbolicT m`
    instance MonadIO m => MonadSymbolic (SymbolicT m) where
      symbolicEnv :: SymbolicT m State
    symbolicEnv = ReaderT State m State -> SymbolicT m State
    forall (m :: * -> *) a. ReaderT State m a -> SymbolicT m a
    SymbolicT ReaderT State m State
    forall r (m :: * -> *). MonadReader r m => m r
    ask

    -- | Map a computation over the symbolic transformer.
    mapSymbolicT :: (ReaderT State m a -> ReaderT State n b) -> SymbolicT m a -> SymbolicT n b
    mapSymbolicT :: (ReaderT State m a -> ReaderT State n b)
    -> SymbolicT m a -> SymbolicT n b
    mapSymbolicT f :: ReaderT State m a -> ReaderT State n b
    f = ReaderT State n b -> SymbolicT n b
    forall (m :: * -> *) a. ReaderT State m a -> SymbolicT m a
    SymbolicT (ReaderT State n b -> SymbolicT n b)
    -> (SymbolicT m a -> ReaderT State n b)
    -> SymbolicT m a
    -> SymbolicT n b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ReaderT State m a -> ReaderT State n b
    f (ReaderT State m a -> ReaderT State n b)
    -> (SymbolicT m a -> ReaderT State m a)
    -> SymbolicT m a
    -> ReaderT State n b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SymbolicT m a -> ReaderT State m a
    forall (m :: * -> *) a. SymbolicT m a -> ReaderT State m a
    runSymbolicT
    {-# INLINE mapSymbolicT #-}

    -- Have to define this one by hand, because we use ReaderT in the implementation
    instance MonadReader r m => MonadReader r (SymbolicT m) where
      ask :: SymbolicT m r
    ask = m r -> SymbolicT m r
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift m r
    forall r (m :: * -> *). MonadReader r m => m r
    ask
      local :: (r -> r) -> SymbolicT m a -> SymbolicT m a
    local f :: r -> r
    f = (ReaderT State m a -> ReaderT State m a)
    -> SymbolicT m a -> SymbolicT m a
    forall (m :: * -> *) a (n :: * -> *) b.
    (ReaderT State m a -> ReaderT State n b)
    -> SymbolicT m a -> SymbolicT n b
    mapSymbolicT ((ReaderT State m a -> ReaderT State m a)
     -> SymbolicT m a -> SymbolicT m a)
    -> (ReaderT State m a -> ReaderT State m a)
    -> SymbolicT m a
    -> SymbolicT m a
    forall a b. (a -> b) -> a -> b
    $ (m a -> m a) -> ReaderT State m a -> ReaderT State m a
    forall (m :: * -> *) a (n :: * -> *) b r.
    (m a -> n b) -> ReaderT r m a -> ReaderT r n b
    mapReaderT ((m a -> m a) -> ReaderT State m a -> ReaderT State m a)
    -> (m a -> m a) -> ReaderT State m a -> ReaderT State m a
    forall a b. (a -> b) -> a -> b
    $ (r -> r) -> m a -> m a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local r -> r
    f

    -- | `Symbolic` is specialization of `SymbolicT` to the `IO` monad. Unless you are using
    -- transformers explicitly, this is the type you should prefer.
    type Symbolic = SymbolicT IO

    -- | Create a symbolic value, based on the quantifier we have. If an
    -- explicit quantifier is given, we just use that. If not, then we
    -- pick the quantifier appropriately based on the run-mode.
    -- @randomCV@ is used for generating random values for this variable
    -- when used for @quickCheck@ or 'Data.SBV.Tools.GenTest.genTest' purposes.
    svMkSymVar :: Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
    svMkSymVar :: Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
    svMkSymVar = Bool
    -> Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
    svMkSymVarGen Bool
    False

    -- | Create an existentially quantified tracker variable
    svMkTrackerVar :: Kind -> String -> State -> IO SVal
    svMkTrackerVar :: Kind -> String -> State -> IO SVal
    svMkTrackerVar k :: Kind
    k nm :: String
    nm = Bool
    -> Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
    svMkSymVarGen Bool
    True (Quantifier -> Maybe Quantifier
    forall a. a -> Maybe a
    Just Quantifier
    EX) Kind
    k (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    nm)

    -- | Generalization of 'Data.SBV.sWordN'
    sWordN :: MonadSymbolic m => Int -> String -> m SVal
    sWordN :: Int -> String -> m SVal
    sWordN w :: Int
    w nm :: String
    nm = m State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv m State -> (State -> m SVal) -> m SVal
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO SVal -> m SVal
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SVal -> m SVal) -> (State -> IO SVal) -> State -> m SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
    svMkSymVar Maybe Quantifier
    forall a. Maybe a
    Nothing (Bool -> Int -> Kind
    KBounded Bool
    False Int
    w) (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    nm)

    -- | Generalization of 'Data.SBV.sWordN_'
    sWordN_ :: MonadSymbolic m => Int -> m SVal
    sWordN_ :: Int -> m SVal
    sWordN_ w :: Int
    w = m State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv m State -> (State -> m SVal) -> m SVal
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO SVal -> m SVal
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SVal -> m SVal) -> (State -> IO SVal) -> State -> m SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
    svMkSymVar Maybe Quantifier
    forall a. Maybe a
    Nothing (Bool -> Int -> Kind
    KBounded Bool
    False Int
    w) Maybe String
    forall a. Maybe a
    Nothing

    -- | Generalization of 'Data.SBV.sIntN'
    sIntN :: MonadSymbolic m => Int -> String -> m SVal
    sIntN :: Int -> String -> m SVal
    sIntN w :: Int
    w nm :: String
    nm = m State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv m State -> (State -> m SVal) -> m SVal
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO SVal -> m SVal
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SVal -> m SVal) -> (State -> IO SVal) -> State -> m SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
    svMkSymVar Maybe Quantifier
    forall a. Maybe a
    Nothing (Bool -> Int -> Kind
    KBounded Bool
    True Int
    w) (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    nm)

    -- | Generalization of 'Data.SBV.sIntN_'
    sIntN_ :: MonadSymbolic m => Int -> m SVal
    sIntN_ :: Int -> m SVal
    sIntN_ w :: Int
    w = m State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv m State -> (State -> m SVal) -> m SVal
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO SVal -> m SVal
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SVal -> m SVal) -> (State -> IO SVal) -> State -> m SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
    svMkSymVar Maybe Quantifier
    forall a. Maybe a
    Nothing (Bool -> Int -> Kind
    KBounded Bool
    True Int
    w) Maybe String
    forall a. Maybe a
    Nothing

    -- | Create a symbolic value, based on the quantifier we have. If an
    -- explicit quantifier is given, we just use that. If not, then we
    -- pick the quantifier appropriately based on the run-mode.
    -- @randomCV@ is used for generating random values for this variable
    -- when used for @quickCheck@ or 'Data.SBV.Tools.GenTest.genTest' purposes.
    svMkSymVarGen :: Bool -> Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
    svMkSymVarGen :: Bool
    -> Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
    svMkSymVarGen isTracker :: Bool
    isTracker mbQ :: Maybe Quantifier
    mbQ k :: Kind
    k mbNm :: Maybe String
    mbNm st :: State
    st = do
            SBVRunMode
    rm <- IORef SBVRunMode -> IO SBVRunMode
    forall a. IORef a -> IO a
    readIORef (State -> IORef SBVRunMode
    runMode State
    st)

            let varInfo :: String
    varInfo = case Maybe String
    mbNm of
                            Nothing -> ", of type " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                            Just nm :: String
    nm -> ", while defining " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " :: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k

                disallow :: String -> IO SVal
    disallow what :: String
    what  = String -> IO SVal
    forall a. HasCallStack => String -> a
    error (String -> IO SVal) -> String -> IO SVal
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV: Unsupported: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    what String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    varInfo String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " in mode: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SBVRunMode -> String
    forall a. Show a => a -> String
    show SBVRunMode
    rm

                noUI :: IO SVal -> IO SVal
    noUI cont :: IO SVal
    cont
                  | Kind -> Bool
    forall a. HasKind a => a -> Bool
    isUninterpreted Kind
    k  = String -> IO SVal
    disallow "Uninterpreted sorts"
                  | Bool
    True               = IO SVal
    cont

                mkS :: Quantifier -> IO SVal
    mkS q :: Quantifier
    q = do (sv :: SV
    sv, internalName :: String
    internalName) <- State -> Kind -> IO NamedSymVar
    newSV State
    st Kind
    k
                           let nm :: String
    nm = String -> Maybe String -> String
    forall a. a -> Maybe a -> a
    fromMaybe String
    internalName Maybe String
    mbNm
                           State -> Bool -> String -> Kind -> Quantifier -> SV -> IO SVal
    introduceUserName State
    st Bool
    isTracker String
    nm Kind
    k Quantifier
    q SV
    sv

                mkC :: CV -> IO SVal
    mkC cv :: CV
    cv = do State -> Kind -> IO ()
    registerKind State
    st Kind
    k
                            State
    -> (State -> IORef [(String, CV)])
    -> ([(String, CV)] -> [(String, CV)])
    -> IO ()
    -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef [(String, CV)]
    rCInfo ((String -> Maybe String -> String
    forall a. a -> Maybe a -> a
    fromMaybe "_" Maybe String
    mbNm, CV
    cv)(String, CV) -> [(String, CV)] -> [(String, CV)]
    forall a. a -> [a] -> [a]
    :) (() -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())
                            SVal -> IO SVal
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SVal -> IO SVal) -> SVal -> IO SVal
    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 CV
    cv)

            case (Maybe Quantifier
    mbQ, SBVRunMode
    rm) of
              (Just q :: Quantifier
    q,  SMTMode{}          ) -> Quantifier -> IO SVal
    mkS Quantifier
    q
              (Nothing, SMTMode _ _ isSAT :: Bool
    isSAT _) -> Quantifier -> IO SVal
    mkS (if Bool
    isSAT then Quantifier
    EX else Quantifier
    ALL)

              (Just EX, CodeGen{})           -> String -> IO SVal
    disallow "Existentially quantified variables"
              (_      , CodeGen)             -> IO SVal -> IO SVal
    noUI (IO SVal -> IO SVal) -> IO SVal -> IO SVal
    forall a b. (a -> b) -> a -> b
    $ Quantifier -> IO SVal
    mkS Quantifier
    ALL  -- code generation, pick universal

              (Just EX, Concrete Nothing)    -> String -> IO SVal
    disallow "Existentially quantified variables"
              (_      , Concrete Nothing)    -> IO SVal -> IO SVal
    noUI (Kind -> IO CV
    randomCV Kind
    k IO CV -> (CV -> IO SVal) -> IO SVal
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= CV -> IO SVal
    mkC)

              -- Model validation:
              (_      , Concrete (Just (_isSat :: Bool
    _isSat, env :: [((Quantifier, NamedSymVar), Maybe CV)]
    env))) ->
                            let bad :: String -> String -> a
    bad why :: String
    why conc :: String
    conc = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ ""
                                                               , "*** Data.SBV: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    why
                                                               , "***"
                                                               , "***   To turn validation off, use `cfg{validateModel = False}`"
                                                               , "***"
                                                               , "*** " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    conc
                                                               ]

                                cant :: String
    cant   = "Validation engine is not capable of handling this case. Failed to validate."
                                report :: String
    report = "Please report this as a bug in SBV!"

                            in if Kind -> Bool
    forall a. HasKind a => a -> Bool
    isUninterpreted Kind
    k
                               then String -> String -> IO SVal
    forall a. String -> String -> a
    bad ("Cannot validate models in the presence of uninterpeted kinds, saw: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k) String
    cant
                               else do (sv :: SV
    sv, internalName :: String
    internalName) <- State -> Kind -> IO NamedSymVar
    newSV State
    st Kind
    k

                                       let nm :: String
    nm = String -> Maybe String -> String
    forall a. a -> Maybe a -> a
    fromMaybe String
    internalName Maybe String
    mbNm
                                           nsv :: NamedSymVar
    nsv = (SV
    sv, String
    nm)

                                           cv :: CV
    cv = case [(Quantifier
    q, Maybe CV
    v) | ((q :: Quantifier
    q, nsv' :: NamedSymVar
    nsv'), v :: Maybe CV
    v) <- [((Quantifier, NamedSymVar), Maybe CV)]
    env, NamedSymVar
    nsv NamedSymVar -> NamedSymVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == NamedSymVar
    nsv'] of
                                                  []              -> if Bool
    isTracker
                                                                     then  -- The sole purpose of a tracker variable is to send the optimization
                                                                           -- directive to the solver, so we can name "expressions" that are minimized
                                                                           -- or maximized. There will be no constraints on these when we are doing
                                                                           -- the validation; in fact they will not even be used anywhere during a
                                                                           -- validation run. So, simply push a zero value that inhabits all metrics.
                                                                           Kind -> Integer -> CV
    forall a. Integral a => Kind -> a -> CV
    mkConstCV Kind
    k (0::Integer)
                                                                     else String -> String -> CV
    forall a. String -> String -> a
    bad ("Cannot locate variable: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (NamedSymVar, Kind) -> String
    forall a. Show a => a -> String
    show (NamedSymVar
    nsv, Kind
    k)) String
    report
                                                  [(ALL, _)]      -> -- We can stop here, as we can't really validate in the presence of a universal quantifier:
                                                                     -- we'd have to validate for each possible value. But that's more or less useless. Instead,
                                                                     -- just issue a warning and use 0 for this value.
                                                                     Kind -> Integer -> CV
    forall a. Integral a => Kind -> a -> CV
    mkConstCV Kind
    k (0::Integer)
                                                  [(EX, Nothing)] -> String -> String -> CV
    forall a. String -> String -> a
    bad ("Cannot locate model value of variable: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show (NamedSymVar -> String
    forall a b. (a, b) -> b
    snd NamedSymVar
    nsv)) String
    report
                                                  [(EX, Just c :: CV
    c)]  -> CV
    c
                                                  r :: [(Quantifier, Maybe CV)]
    r               -> String -> String -> CV
    forall a. String -> String -> a
    bad (   "Found multiple matching values for variable: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ NamedSymVar -> String
    forall a. Show a => a -> String
    show NamedSymVar
    nsv
                                                                          String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "\n*** " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [(Quantifier, Maybe CV)] -> String
    forall a. Show a => a -> String
    show [(Quantifier, Maybe CV)]
    r) String
    report

                                       CV -> IO SVal
    mkC CV
    cv

    -- | Introduce a new user name. We simply append a suffix if we have seen this variable before.
    introduceUserName :: State -> Bool -> String -> Kind -> Quantifier -> SV -> IO SVal
    introduceUserName :: State -> Bool -> String -> Kind -> Quantifier -> SV -> IO SVal
    introduceUserName st :: State
    st isTracker :: Bool
    isTracker nmOrig :: String
    nmOrig k :: Kind
    k q :: Quantifier
    q sv :: SV
    sv = do
            (_, old :: Set String
    old) <- IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    -> IO (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    forall a. IORef a -> IO a
    readIORef (State
    -> IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    rinps State
    st)

            let nm :: String
    nm  = String -> Set String -> String
    mkUnique String
    nmOrig Set String
    old

            if Bool
    isTracker Bool -> Bool -> Bool
    && Quantifier
    q Quantifier -> Quantifier -> Bool
    forall a. Eq a => a -> a -> Bool
    == Quantifier
    ALL
               then String -> IO SVal
    forall a. HasCallStack => String -> a
    error (String -> IO SVal) -> String -> IO SVal
    forall a b. (a -> b) -> a -> b
    $ "SBV: Impossible happened! A universally quantified tracker variable is being introduced: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    nm
               else do let newInp :: [NamedSymVar] -> [NamedSymVar]
    newInp olds :: [NamedSymVar]
    olds = case Quantifier
    q of
                                          EX  -> (SV
    sv, String
    nm) NamedSymVar -> [NamedSymVar] -> [NamedSymVar]
    forall a. a -> [a] -> [a]
    : [NamedSymVar]
    olds
                                          ALL -> [String] -> [NamedSymVar]
    forall a. [String] -> a
    noInteractive [ "Adding a new universally quantified variable: "
                                                               , "  Name      : " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    nm
                                                               , "  Kind      : " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                                                               , "  Quantifier: Universal"
                                                               , "  Node      : " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    sv
                                                               , "Only existential variables are supported in query mode."
                                                               ]
                       if Bool
    isTracker
                          then State
    -> (State
        -> IORef
             (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String))
    -> ((([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
        -> (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String))
    -> IO ()
    -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State
    -> IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    rinps (([NamedSymVar] -> [NamedSymVar])
    -> ([(Quantifier, NamedSymVar)], [NamedSymVar])
    -> ([(Quantifier, NamedSymVar)], [NamedSymVar])
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second ((SV
    sv, String
    nm) NamedSymVar -> [NamedSymVar] -> [NamedSymVar]
    forall a. a -> [a] -> [a]
    :) (([(Quantifier, NamedSymVar)], [NamedSymVar])
     -> ([(Quantifier, NamedSymVar)], [NamedSymVar]))
    -> (Set String -> Set String)
    -> (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    -> (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** String -> Set String -> Set String
    forall a. Ord a => a -> Set a -> Set a
    Set.insert String
    nm)
                                         (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> IO ()
    forall a. [String] -> a
    noInteractive ["Adding a new tracker variable in interactive mode: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    nm]
                          else State
    -> (State
        -> IORef
             (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String))
    -> ((([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
        -> (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String))
    -> IO ()
    -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State
    -> IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    rinps (([(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)])
    -> ([(Quantifier, NamedSymVar)], [NamedSymVar])
    -> ([(Quantifier, NamedSymVar)], [NamedSymVar])
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (b, d) (c, d)
    first ((Quantifier
    q, (SV
    sv, String
    nm)) (Quantifier, NamedSymVar)
    -> [(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)]
    forall a. a -> [a] -> [a]
    :) (([(Quantifier, NamedSymVar)], [NamedSymVar])
     -> ([(Quantifier, NamedSymVar)], [NamedSymVar]))
    -> (Set String -> Set String)
    -> (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    -> (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** String -> Set String -> Set String
    forall a. Ord a => a -> Set a -> Set a
    Set.insert String
    nm)
                                         (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ State
    -> (IncState -> IORef [NamedSymVar])
    -> ([NamedSymVar] -> [NamedSymVar])
    -> IO ()
    forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
    modifyIncState State
    st IncState -> IORef [NamedSymVar]
    rNewInps [NamedSymVar] -> [NamedSymVar]
    newInp
                       SVal -> IO SVal
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SVal -> IO SVal) -> SVal -> IO SVal
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (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 (m :: * -> *) a. Monad m => a -> m a
    return SV
    sv))

       where -- The following can be rather slow if we keep reusing the same prefix, but I doubt it'll be a problem in practice
             -- Also, the following will fail if we span the range of integers without finding a match, but your computer would
             -- die way ahead of that happening if that's the case!
             mkUnique :: String -> Set String -> String
    mkUnique prefix :: String
    prefix names :: Set String
    names = [String] -> String
    forall a. [a] -> a
    head ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ (String -> Bool) -> [String] -> [String]
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile (String -> Set String -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set String
    names) (String
    prefix String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String
    prefix String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "_" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i | Int
    i <- [(0::Int)..]])

    -- | Generalization of 'Data.SBV.runSymbolic'
    runSymbolic :: MonadIO m => SBVRunMode -> SymbolicT m a -> m (a, Result)
    runSymbolic :: SBVRunMode -> SymbolicT m a -> m (a, Result)
    runSymbolic currentRunMode :: SBVRunMode
    currentRunMode (SymbolicT c :: ReaderT State m a
    c) = do
       State
    st <- IO State -> m State
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO State -> m State) -> IO State -> m State
    forall a b. (a -> b) -> a -> b
    $ do
         UTCTime
    currTime  <- IO UTCTime
    getCurrentTime
         IORef SBVRunMode
    rm        <- SBVRunMode -> IO (IORef SBVRunMode)
    forall a. a -> IO (IORef a)
    newIORef SBVRunMode
    currentRunMode
         IORef Int
    ctr       <- Int -> IO (IORef Int)
    forall a. a -> IO (IORef a)
    newIORef (-2) -- start from -2; False and True will always occupy the first two elements
         IORef [(String, CV)]
    cInfo     <- [(String, CV)] -> IO (IORef [(String, CV)])
    forall a. a -> IO (IORef a)
    newIORef []
         IORef [(String, CV -> Bool, SV)]
    observes  <- [(String, CV -> Bool, SV)] -> IO (IORef [(String, CV -> Bool, SV)])
    forall a. a -> IO (IORef a)
    newIORef []
         IORef SBVPgm
    pgm       <- SBVPgm -> IO (IORef SBVPgm)
    forall a. a -> IO (IORef a)
    newIORef (Seq (SV, SBVExpr) -> SBVPgm
    SBVPgm Seq (SV, SBVExpr)
    forall a. Seq a
    S.empty)
         IORef ExprMap
    emap      <- ExprMap -> IO (IORef ExprMap)
    forall a. a -> IO (IORef a)
    newIORef ExprMap
    forall k a. Map k a
    Map.empty
         IORef CnstMap
    cmap      <- CnstMap -> IO (IORef CnstMap)
    forall a. a -> IO (IORef a)
    newIORef CnstMap
    forall k a. Map k a
    Map.empty
         IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    inps      <- (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    -> IO
         (IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String))
    forall a. a -> IO (IORef a)
    newIORef (([], []), Set String
    forall a. Set a
    Set.empty)
         IORef [SV]
    outs      <- [SV] -> IO (IORef [SV])
    forall a. a -> IO (IORef a)
    newIORef []
         IORef TableMap
    tables    <- TableMap -> IO (IORef TableMap)
    forall a. a -> IO (IORef a)
    newIORef TableMap
    forall k a. Map k a
    Map.empty
         IORef ArrayMap
    arrays    <- ArrayMap -> IO (IORef ArrayMap)
    forall a. a -> IO (IORef a)
    newIORef ArrayMap
    forall a. IntMap a
    IMap.empty
         IORef FArrayMap
    fArrays   <- FArrayMap -> IO (IORef FArrayMap)
    forall a. a -> IO (IORef a)
    newIORef FArrayMap
    forall a. IntMap a
    IMap.empty
         IORef UIMap
    uis       <- UIMap -> IO (IORef UIMap)
    forall a. a -> IO (IORef a)
    newIORef UIMap
    forall k a. Map k a
    Map.empty
         IORef CgMap
    cgs       <- CgMap -> IO (IORef CgMap)
    forall a. a -> IO (IORef a)
    newIORef CgMap
    forall k a. Map k a
    Map.empty
         IORef [(String, [String])]
    axioms    <- [(String, [String])] -> IO (IORef [(String, [String])])
    forall a. a -> IO (IORef a)
    newIORef []
         IORef (Cache SV)
    swCache   <- Cache SV -> IO (IORef (Cache SV))
    forall a. a -> IO (IORef a)
    newIORef Cache SV
    forall a. IntMap a
    IMap.empty
         IORef (Cache ArrayIndex)
    aiCache   <- Cache ArrayIndex -> IO (IORef (Cache ArrayIndex))
    forall a. a -> IO (IORef a)
    newIORef Cache ArrayIndex
    forall a. IntMap a
    IMap.empty
         IORef (Cache FArrayIndex)
    faiCache  <- Cache FArrayIndex -> IO (IORef (Cache FArrayIndex))
    forall a. a -> IO (IORef a)
    newIORef Cache FArrayIndex
    forall a. IntMap a
    IMap.empty
         IORef (Set Kind)
    usedKinds <- Set Kind -> IO (IORef (Set Kind))
    forall a. a -> IO (IORef a)
    newIORef Set Kind
    forall a. Set a
    Set.empty
         IORef (Set String)
    usedLbls  <- Set String -> IO (IORef (Set String))
    forall a. a -> IO (IORef a)
    newIORef Set String
    forall a. Set a
    Set.empty
         IORef (Seq (Bool, [(String, String)], SV))
    cstrs     <- Seq (Bool, [(String, String)], SV)
    -> IO (IORef (Seq (Bool, [(String, String)], SV)))
    forall a. a -> IO (IORef a)
    newIORef Seq (Bool, [(String, String)], SV)
    forall a. Seq a
    S.empty
         IORef [SMTOption]
    smtOpts   <- [SMTOption] -> IO (IORef [SMTOption])
    forall a. a -> IO (IORef a)
    newIORef []
         IORef [Objective (SV, SV)]
    optGoals  <- [Objective (SV, SV)] -> IO (IORef [Objective (SV, SV)])
    forall a. a -> IO (IORef a)
    newIORef []
         IORef [(String, Maybe CallStack, SV)]
    asserts   <- [(String, Maybe CallStack, SV)]
    -> IO (IORef [(String, Maybe CallStack, SV)])
    forall a. a -> IO (IORef a)
    newIORef []
         IORef IncState
    istate    <- IncState -> IO (IORef IncState)
    forall a. a -> IO (IORef a)
    newIORef (IncState -> IO (IORef IncState))
    -> IO IncState -> IO (IORef IncState)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< IO IncState
    newIncState
         IORef (Maybe QueryState)
    qstate    <- Maybe QueryState -> IO (IORef (Maybe QueryState))
    forall a. a -> IO (IORef a)
    newIORef Maybe QueryState
    forall a. Maybe a
    Nothing
         State -> IO State
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (State -> IO State) -> State -> IO State
    forall a b. (a -> b) -> a -> b
    $ State :: SVal
    -> UTCTime
    -> IORef SBVRunMode
    -> IORef IncState
    -> IORef [(String, CV)]
    -> IORef [(String, CV -> Bool, SV)]
    -> IORef Int
    -> IORef (Set Kind)
    -> IORef (Set String)
    -> IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    -> IORef (Seq (Bool, [(String, String)], SV))
    -> IORef [SV]
    -> IORef TableMap
    -> IORef SBVPgm
    -> IORef CnstMap
    -> IORef ExprMap
    -> IORef ArrayMap
    -> IORef FArrayMap
    -> IORef UIMap
    -> IORef CgMap
    -> IORef [(String, [String])]
    -> IORef [SMTOption]
    -> IORef [Objective (SV, SV)]
    -> IORef [(String, Maybe CallStack, SV)]
    -> IORef (Cache SV)
    -> IORef (Cache ArrayIndex)
    -> IORef (Cache FArrayIndex)
    -> IORef (Maybe QueryState)
    -> State
    State { runMode :: IORef SBVRunMode
    runMode      = IORef SBVRunMode
    rm
                      , startTime :: UTCTime
    startTime    = UTCTime
    currTime
                      , pathCond :: SVal
    pathCond     = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KBool (CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left CV
    trueCV)
                      , rIncState :: IORef IncState
    rIncState    = IORef IncState
    istate
                      , rCInfo :: IORef [(String, CV)]
    rCInfo       = IORef [(String, CV)]
    cInfo
                      , rObservables :: IORef [(String, CV -> Bool, SV)]
    rObservables = IORef [(String, CV -> Bool, SV)]
    observes
                      , rctr :: IORef Int
    rctr         = IORef Int
    ctr
                      , rUsedKinds :: IORef (Set Kind)
    rUsedKinds   = IORef (Set Kind)
    usedKinds
                      , rUsedLbls :: IORef (Set String)
    rUsedLbls    = IORef (Set String)
    usedLbls
                      , rinps :: IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    rinps        = IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    inps
                      , routs :: IORef [SV]
    routs        = IORef [SV]
    outs
                      , rtblMap :: IORef TableMap
    rtblMap      = IORef TableMap
    tables
                      , spgm :: IORef SBVPgm
    spgm         = IORef SBVPgm
    pgm
                      , rconstMap :: IORef CnstMap
    rconstMap    = IORef CnstMap
    cmap
                      , rArrayMap :: IORef ArrayMap
    rArrayMap    = IORef ArrayMap
    arrays
                      , rFArrayMap :: IORef FArrayMap
    rFArrayMap   = IORef FArrayMap
    fArrays
                      , rexprMap :: IORef ExprMap
    rexprMap     = IORef ExprMap
    emap
                      , rUIMap :: IORef UIMap
    rUIMap       = IORef UIMap
    uis
                      , rCgMap :: IORef CgMap
    rCgMap       = IORef CgMap
    cgs
                      , raxioms :: IORef [(String, [String])]
    raxioms      = IORef [(String, [String])]
    axioms
                      , rSVCache :: IORef (Cache SV)
    rSVCache     = IORef (Cache SV)
    swCache
                      , rAICache :: IORef (Cache ArrayIndex)
    rAICache     = IORef (Cache ArrayIndex)
    aiCache
                      , rFAICache :: IORef (Cache FArrayIndex)
    rFAICache    = IORef (Cache FArrayIndex)
    faiCache
                      , rConstraints :: IORef (Seq (Bool, [(String, String)], SV))
    rConstraints = IORef (Seq (Bool, [(String, String)], SV))
    cstrs
                      , rSMTOptions :: IORef [SMTOption]
    rSMTOptions  = IORef [SMTOption]
    smtOpts
                      , rOptGoals :: IORef [Objective (SV, SV)]
    rOptGoals    = IORef [Objective (SV, SV)]
    optGoals
                      , rAsserts :: IORef [(String, Maybe CallStack, SV)]
    rAsserts     = IORef [(String, Maybe CallStack, SV)]
    asserts
                      , rQueryState :: IORef (Maybe QueryState)
    rQueryState   = IORef (Maybe QueryState)
    qstate
                      }
       SV
    _ <- IO SV -> m SV
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SV -> m SV) -> IO SV -> m SV
    forall a b. (a -> b) -> a -> b
    $ State -> CV -> IO SV
    newConst State
    st CV
    falseCV -- s(-2) == falseSV
       SV
    _ <- IO SV -> m SV
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SV -> m SV) -> IO SV -> m SV
    forall a b. (a -> b) -> a -> b
    $ State -> CV -> IO SV
    newConst State
    st CV
    trueCV  -- s(-1) == trueSV
       a
    r <- ReaderT State m a -> State -> m a
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT ReaderT State m a
    c State
    st
       Result
    res <- IO Result -> m Result
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Result -> m Result) -> IO Result -> m Result
    forall a b. (a -> b) -> a -> b
    $ State -> IO Result
    extractSymbolicSimulationState State
    st

       -- Clean-up after ourselves
       Maybe QueryState
    qs <- IO (Maybe QueryState) -> m (Maybe QueryState)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (Maybe QueryState) -> m (Maybe QueryState))
    -> IO (Maybe QueryState) -> m (Maybe QueryState)
    forall a b. (a -> b) -> a -> b
    $ IORef (Maybe QueryState) -> IO (Maybe QueryState)
    forall a. IORef a -> IO a
    readIORef (IORef (Maybe QueryState) -> IO (Maybe QueryState))
    -> IORef (Maybe QueryState) -> IO (Maybe QueryState)
    forall a b. (a -> b) -> a -> b
    $ State -> IORef (Maybe QueryState)
    rQueryState State
    st
       case Maybe QueryState
    qs of
         Nothing                         -> () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
         Just QueryState{IO ()
    queryTerminate :: IO ()
    queryTerminate :: QueryState -> IO ()
    queryTerminate} -> IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO ()
    queryTerminate

       (a, Result) -> m (a, Result)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a
    r, Result
    res)

    -- | Grab the program from a running symbolic simulation state.
    extractSymbolicSimulationState :: State -> IO Result
    extractSymbolicSimulationState :: State -> IO Result
    extractSymbolicSimulationState st :: State
    st@State{ spgm :: State -> IORef SBVPgm
    spgm=IORef SBVPgm
    pgm, rinps :: State
    -> IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    rinps=IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    inps, routs :: State -> IORef [SV]
    routs=IORef [SV]
    outs, rtblMap :: State -> IORef TableMap
    rtblMap=IORef TableMap
    tables, rArrayMap :: State -> IORef ArrayMap
    rArrayMap=IORef ArrayMap
    arrays, rUIMap :: State -> IORef UIMap
    rUIMap=IORef UIMap
    uis, raxioms :: State -> IORef [(String, [String])]
    raxioms=IORef [(String, [String])]
    axioms
                                           , rAsserts :: State -> IORef [(String, Maybe CallStack, SV)]
    rAsserts=IORef [(String, Maybe CallStack, SV)]
    asserts, rUsedKinds :: State -> IORef (Set Kind)
    rUsedKinds=IORef (Set Kind)
    usedKinds, rCgMap :: State -> IORef CgMap
    rCgMap=IORef CgMap
    cgs, rCInfo :: State -> IORef [(String, CV)]
    rCInfo=IORef [(String, CV)]
    cInfo, rConstraints :: State -> IORef (Seq (Bool, [(String, String)], SV))
    rConstraints=IORef (Seq (Bool, [(String, String)], SV))
    cstrs
                                           , rObservables :: State -> IORef [(String, CV -> Bool, SV)]
    rObservables=IORef [(String, CV -> Bool, SV)]
    observes
                                           } = do
       SBVPgm rpgm :: Seq (SV, SBVExpr)
    rpgm  <- IORef SBVPgm -> IO SBVPgm
    forall a. IORef a -> IO a
    readIORef IORef SBVPgm
    pgm
       ([(Quantifier, NamedSymVar)], [NamedSymVar])
    inpsO <- ([(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)]
    forall a. [a] -> [a]
    reverse ([(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)])
    -> ([NamedSymVar] -> [NamedSymVar])
    -> ([(Quantifier, NamedSymVar)], [NamedSymVar])
    -> ([(Quantifier, NamedSymVar)], [NamedSymVar])
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** [NamedSymVar] -> [NamedSymVar]
    forall a. [a] -> [a]
    reverse) (([(Quantifier, NamedSymVar)], [NamedSymVar])
     -> ([(Quantifier, NamedSymVar)], [NamedSymVar]))
    -> ((([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
        -> ([(Quantifier, NamedSymVar)], [NamedSymVar]))
    -> (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    -> ([(Quantifier, NamedSymVar)], [NamedSymVar])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    -> ([(Quantifier, NamedSymVar)], [NamedSymVar])
    forall a b. (a, b) -> a
    fst ((([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
     -> ([(Quantifier, NamedSymVar)], [NamedSymVar]))
    -> IO (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    -> IO ([(Quantifier, NamedSymVar)], [NamedSymVar])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    -> IO (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    forall a. IORef a -> IO a
    readIORef IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    inps
       [SV]
    outsO <- [SV] -> [SV]
    forall a. [a] -> [a]
    reverse ([SV] -> [SV]) -> IO [SV] -> IO [SV]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IORef [SV] -> IO [SV]
    forall a. IORef a -> IO a
    readIORef IORef [SV]
    outs

       let swap :: (b, a) -> (a, b)
    swap  (a :: b
    a, b :: a
    b)              = (a
    b, b
    a)
           cmp :: (a, b) -> (a, b) -> Ordering
    cmp   (a :: a
    a, _) (b :: a
    b, _)       = a
    a a -> a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare` a
    b
           arrange :: (a, (b, c, b)) -> ((a, b, c), b)
    arrange (i :: a
    i, (at :: b
    at, rt :: c
    rt, es :: b
    es)) = ((a
    i, b
    at, c
    rt), b
    es)

       [(SV, CV)]
    cnsts <- ((SV, CV) -> (SV, CV) -> Ordering) -> [(SV, CV)] -> [(SV, CV)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (SV, CV) -> (SV, CV) -> Ordering
    forall a b b. Ord a => (a, b) -> (a, b) -> Ordering
    cmp ([(SV, CV)] -> [(SV, CV)])
    -> (CnstMap -> [(SV, CV)]) -> CnstMap -> [(SV, CV)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((CV, SV) -> (SV, CV)) -> [(CV, SV)] -> [(SV, CV)]
    forall a b. (a -> b) -> [a] -> [b]
    map (CV, SV) -> (SV, CV)
    forall b a. (b, a) -> (a, b)
    swap ([(CV, SV)] -> [(SV, CV)])
    -> (CnstMap -> [(CV, SV)]) -> CnstMap -> [(SV, CV)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CnstMap -> [(CV, SV)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (CnstMap -> [(SV, CV)]) -> IO CnstMap -> IO [(SV, CV)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IORef CnstMap -> IO CnstMap
    forall a. IORef a -> IO a
    readIORef (State -> IORef CnstMap
    rconstMap State
    st)
       [((Int, Kind, Kind), [SV])]
    tbls  <- ((Int, (Kind, Kind, [SV])) -> ((Int, Kind, Kind), [SV]))
    -> [(Int, (Kind, Kind, [SV]))] -> [((Int, Kind, Kind), [SV])]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int, (Kind, Kind, [SV])) -> ((Int, Kind, Kind), [SV])
    forall a b c b. (a, (b, c, b)) -> ((a, b, c), b)
    arrange ([(Int, (Kind, Kind, [SV]))] -> [((Int, Kind, Kind), [SV])])
    -> (TableMap -> [(Int, (Kind, Kind, [SV]))])
    -> TableMap
    -> [((Int, Kind, Kind), [SV])]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Int, (Kind, Kind, [SV]))
     -> (Int, (Kind, Kind, [SV])) -> Ordering)
    -> [(Int, (Kind, Kind, [SV]))] -> [(Int, (Kind, Kind, [SV]))]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (Int, (Kind, Kind, [SV])) -> (Int, (Kind, Kind, [SV])) -> Ordering
    forall a b b. Ord a => (a, b) -> (a, b) -> Ordering
    cmp ([(Int, (Kind, Kind, [SV]))] -> [(Int, (Kind, Kind, [SV]))])
    -> (TableMap -> [(Int, (Kind, Kind, [SV]))])
    -> TableMap
    -> [(Int, (Kind, Kind, [SV]))]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (((Kind, Kind, [SV]), Int) -> (Int, (Kind, Kind, [SV])))
    -> [((Kind, Kind, [SV]), Int)] -> [(Int, (Kind, Kind, [SV]))]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Kind, Kind, [SV]), Int) -> (Int, (Kind, Kind, [SV]))
    forall b a. (b, a) -> (a, b)
    swap ([((Kind, Kind, [SV]), Int)] -> [(Int, (Kind, Kind, [SV]))])
    -> (TableMap -> [((Kind, Kind, [SV]), Int)])
    -> TableMap
    -> [(Int, (Kind, Kind, [SV]))]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TableMap -> [((Kind, Kind, [SV]), Int)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (TableMap -> [((Int, Kind, Kind), [SV])])
    -> IO TableMap -> IO [((Int, Kind, Kind), [SV])]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IORef TableMap -> IO TableMap
    forall a. IORef a -> IO a
    readIORef IORef TableMap
    tables
       [(Int, ArrayInfo)]
    arrs  <- ArrayMap -> [(Int, ArrayInfo)]
    forall a. IntMap a -> [(Int, a)]
    IMap.toAscList (ArrayMap -> [(Int, ArrayInfo)])
    -> IO ArrayMap -> IO [(Int, ArrayInfo)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IORef ArrayMap -> IO ArrayMap
    forall a. IORef a -> IO a
    readIORef IORef ArrayMap
    arrays
       [(String, SBVType)]
    unint <- UIMap -> [(String, SBVType)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (UIMap -> [(String, SBVType)])
    -> IO UIMap -> IO [(String, SBVType)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IORef UIMap -> IO UIMap
    forall a. IORef a -> IO a
    readIORef IORef UIMap
    uis
       [(String, [String])]
    axs   <- [(String, [String])] -> [(String, [String])]
    forall a. [a] -> [a]
    reverse ([(String, [String])] -> [(String, [String])])
    -> IO [(String, [String])] -> IO [(String, [String])]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IORef [(String, [String])] -> IO [(String, [String])]
    forall a. IORef a -> IO a
    readIORef IORef [(String, [String])]
    axioms
       Set Kind
    knds  <- IORef (Set Kind) -> IO (Set Kind)
    forall a. IORef a -> IO a
    readIORef IORef (Set Kind)
    usedKinds
       [(String, [String])]
    cgMap <- CgMap -> [(String, [String])]
    forall k a. Map k a -> [(k, a)]
    Map.toList (CgMap -> [(String, [String])])
    -> IO CgMap -> IO [(String, [String])]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IORef CgMap -> IO CgMap
    forall a. IORef a -> IO a
    readIORef IORef CgMap
    cgs

       [(String, CV)]
    traceVals   <- [(String, CV)] -> [(String, CV)]
    forall a. [a] -> [a]
    reverse ([(String, CV)] -> [(String, CV)])
    -> IO [(String, CV)] -> IO [(String, CV)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IORef [(String, CV)] -> IO [(String, CV)]
    forall a. IORef a -> IO a
    readIORef IORef [(String, CV)]
    cInfo
       [(String, CV -> Bool, SV)]
    observables <- [(String, CV -> Bool, SV)] -> [(String, CV -> Bool, SV)]
    forall a. [a] -> [a]
    reverse ([(String, CV -> Bool, SV)] -> [(String, CV -> Bool, SV)])
    -> IO [(String, CV -> Bool, SV)] -> IO [(String, CV -> Bool, SV)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IORef [(String, CV -> Bool, SV)] -> IO [(String, CV -> Bool, SV)]
    forall a. IORef a -> IO a
    readIORef IORef [(String, CV -> Bool, SV)]
    observes
       Seq (Bool, [(String, String)], SV)
    extraCstrs  <- IORef (Seq (Bool, [(String, String)], SV))
    -> IO (Seq (Bool, [(String, String)], SV))
    forall a. IORef a -> IO a
    readIORef IORef (Seq (Bool, [(String, String)], SV))
    cstrs
       [(String, Maybe CallStack, SV)]
    assertions  <- [(String, Maybe CallStack, SV)] -> [(String, Maybe CallStack, SV)]
    forall a. [a] -> [a]
    reverse ([(String, Maybe CallStack, SV)]
     -> [(String, Maybe CallStack, SV)])
    -> IO [(String, Maybe CallStack, SV)]
    -> IO [(String, Maybe CallStack, SV)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IORef [(String, Maybe CallStack, SV)]
    -> IO [(String, Maybe CallStack, SV)]
    forall a. IORef a -> IO a
    readIORef IORef [(String, Maybe CallStack, SV)]
    asserts

       Result -> IO Result
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Result -> IO Result) -> Result -> IO Result
    forall a b. (a -> b) -> a -> b
    $ Set Kind
    -> [(String, CV)]
    -> [(String, CV -> Bool, SV)]
    -> [(String, [String])]
    -> ([(Quantifier, NamedSymVar)], [NamedSymVar])
    -> [(SV, CV)]
    -> [((Int, Kind, Kind), [SV])]
    -> [(Int, ArrayInfo)]
    -> [(String, SBVType)]
    -> [(String, [String])]
    -> SBVPgm
    -> Seq (Bool, [(String, String)], SV)
    -> [(String, Maybe CallStack, SV)]
    -> [SV]
    -> Result
    Result Set Kind
    knds [(String, CV)]
    traceVals [(String, CV -> Bool, SV)]
    observables [(String, [String])]
    cgMap ([(Quantifier, NamedSymVar)], [NamedSymVar])
    inpsO [(SV, CV)]
    cnsts [((Int, Kind, Kind), [SV])]
    tbls [(Int, ArrayInfo)]
    arrs [(String, SBVType)]
    unint [(String, [String])]
    axs (Seq (SV, SBVExpr) -> SBVPgm
    SBVPgm Seq (SV, SBVExpr)
    rpgm) Seq (Bool, [(String, String)], SV)
    extraCstrs [(String, Maybe CallStack, SV)]
    assertions [SV]
    outsO

    -- | Generalization of 'Data.SBV.addNewSMTOption'
    addNewSMTOption :: MonadSymbolic m => SMTOption -> m ()
    addNewSMTOption :: SMTOption -> m ()
    addNewSMTOption o :: SMTOption
    o = do State
    st <- m State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv
                           IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ State
    -> (State -> IORef [SMTOption])
    -> ([SMTOption] -> [SMTOption])
    -> IO ()
    -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef [SMTOption]
    rSMTOptions (SMTOption
    oSMTOption -> [SMTOption] -> [SMTOption]
    forall a. a -> [a] -> [a]
    :) (() -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())

    -- | Generalization of 'Data.SBV.imposeConstraint'
    imposeConstraint :: MonadSymbolic m => Bool -> [(String, String)] -> SVal -> m ()
    imposeConstraint :: Bool -> [(String, String)] -> SVal -> m ()
    imposeConstraint isSoft :: Bool
    isSoft attrs :: [(String, String)]
    attrs c :: SVal
    c = do State
    st <- m State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv
                                         SBVRunMode
    rm <- IO SBVRunMode -> m SBVRunMode
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SBVRunMode -> m SBVRunMode) -> IO SBVRunMode -> m SBVRunMode
    forall a b. (a -> b) -> a -> b
    $ IORef SBVRunMode -> IO SBVRunMode
    forall a. IORef a -> IO a
    readIORef (State -> IORef SBVRunMode
    runMode State
    st)

                                         case SBVRunMode
    rm of
                                           CodeGen -> String -> m ()
    forall a. HasCallStack => String -> a
    error "SBV: constraints are not allowed in code-generation"
                                           _       -> IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do (String -> IO ()) -> [String] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (String -> State -> String -> IO ()
    registerLabel "Constraint" State
    st) [String
    nm | (":named",  nm :: String
    nm) <- [(String, String)]
    attrs]
                                                                  State -> Bool -> [(String, String)] -> SVal -> IO ()
    internalConstraint State
    st Bool
    isSoft [(String, String)]
    attrs SVal
    c

    -- | Require a boolean condition to be true in the state. Only used for internal purposes.
    internalConstraint :: State -> Bool -> [(String, String)] -> SVal -> IO ()
    internalConstraint :: State -> Bool -> [(String, String)] -> SVal -> IO ()
    internalConstraint st :: State
    st isSoft :: Bool
    isSoft attrs :: [(String, String)]
    attrs b :: SVal
    b = do SV
    v <- State -> SVal -> IO SV
    svToSV State
    st SVal
    b

                                              SBVRunMode
    rm <- IO SBVRunMode -> IO SBVRunMode
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SBVRunMode -> IO SBVRunMode) -> IO SBVRunMode -> IO SBVRunMode
    forall a b. (a -> b) -> a -> b
    $ IORef SBVRunMode -> IO SBVRunMode
    forall a. IORef a -> IO a
    readIORef (State -> IORef SBVRunMode
    runMode State
    st)

                                              -- Are we running validation? If so, we always want to
                                              -- add the constraint for debug purposes. Otherwie
                                              -- we only add it if it's interesting; i.e., not directly
                                              -- true or has some attributes.
                                              let isValidating :: Bool
    isValidating = case SBVRunMode
    rm of
                                                                   SMTMode _ _ _ cfg :: SMTConfig
    cfg -> SMTConfig -> Bool
    validationRequested SMTConfig
    cfg
                                                                   CodeGen           -> Bool
    False
                                                                   Concrete Nothing  -> Bool
    False
                                                                   Concrete (Just _) -> Bool
    True   -- The case when we *are* running the validation

                                              let c :: (Bool, [(String, String)], SV)
    c           = (Bool
    isSoft, [(String, String)]
    attrs, SV
    v)
                                                  interesting :: Bool
    interesting = SV
    v SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    /= SV
    trueSV Bool -> Bool -> Bool
    || Bool -> Bool
    not ([(String, String)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(String, String)]
    attrs)

                                              Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Bool
    isValidating Bool -> Bool -> Bool
    || Bool
    interesting) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $
                                                   State
    -> (State -> IORef (Seq (Bool, [(String, String)], SV)))
    -> (Seq (Bool, [(String, String)], SV)
        -> Seq (Bool, [(String, String)], SV))
    -> IO ()
    -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef (Seq (Bool, [(String, String)], SV))
    rConstraints (Seq (Bool, [(String, String)], SV)
    -> (Bool, [(String, String)], SV)
    -> Seq (Bool, [(String, String)], SV)
    forall a. Seq a -> a -> Seq a
    S.|> (Bool, [(String, String)], SV)
    c)
                                                                (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ State
    -> (IncState -> IORef (Seq (Bool, [(String, String)], SV)))
    -> (Seq (Bool, [(String, String)], SV)
        -> Seq (Bool, [(String, String)], SV))
    -> IO ()
    forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
    modifyIncState State
    st IncState -> IORef (Seq (Bool, [(String, String)], SV))
    rNewConstraints (Seq (Bool, [(String, String)], SV)
    -> (Bool, [(String, String)], SV)
    -> Seq (Bool, [(String, String)], SV)
    forall a. Seq a -> a -> Seq a
    S.|> (Bool, [(String, String)], SV)
    c)

    -- | Generalization of 'Data.SBV.addSValOptGoal'
    addSValOptGoal :: MonadSymbolic m => Objective SVal -> m ()
    addSValOptGoal :: Objective SVal -> m ()
    addSValOptGoal obj :: Objective SVal
    obj = do State
    st <- m State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv

                            -- create the tracking variable here for the metric
                            let mkGoal :: String -> SVal -> m (SV, SV)
    mkGoal nm :: String
    nm orig :: SVal
    orig = IO (SV, SV) -> m (SV, SV)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SV, SV) -> m (SV, SV)) -> IO (SV, SV) -> m (SV, SV)
    forall a b. (a -> b) -> a -> b
    $ do SV
    origSV  <- State -> SVal -> IO SV
    svToSV State
    st SVal
    orig
                                                             SVal
    track   <- Kind -> String -> State -> IO SVal
    svMkTrackerVar (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    orig) String
    nm State
    st
                                                             SV
    trackSV <- State -> SVal -> IO SV
    svToSV State
    st SVal
    track
                                                             (SV, SV) -> IO (SV, SV)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SV
    origSV, SV
    trackSV)

                            let walk :: Objective SVal -> m (Objective (SV, SV))
    walk (Minimize          nm :: String
    nm v :: SVal
    v)     = String -> (SV, SV) -> Objective (SV, SV)
    forall a. String -> a -> Objective a
    Minimize String
    nm                     ((SV, SV) -> Objective (SV, SV))
    -> m (SV, SV) -> m (Objective (SV, SV))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> SVal -> m (SV, SV)
    mkGoal String
    nm SVal
    v
                                walk (Maximize          nm :: String
    nm v :: SVal
    v)     = String -> (SV, SV) -> Objective (SV, SV)
    forall a. String -> a -> Objective a
    Maximize String
    nm                     ((SV, SV) -> Objective (SV, SV))
    -> m (SV, SV) -> m (Objective (SV, SV))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> SVal -> m (SV, SV)
    mkGoal String
    nm SVal
    v
                                walk (AssertWithPenalty nm :: String
    nm v :: SVal
    v mbP :: Penalty
    mbP) = ((SV, SV) -> Penalty -> Objective (SV, SV))
    -> Penalty -> (SV, SV) -> Objective (SV, SV)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (String -> (SV, SV) -> Penalty -> Objective (SV, SV)
    forall a. String -> a -> Penalty -> Objective a
    AssertWithPenalty String
    nm) Penalty
    mbP ((SV, SV) -> Objective (SV, SV))
    -> m (SV, SV) -> m (Objective (SV, SV))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> SVal -> m (SV, SV)
    mkGoal String
    nm SVal
    v

                            Objective (SV, SV)
    obj' <- Objective SVal -> m (Objective (SV, SV))
    walk Objective SVal
    obj
                            IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ State
    -> (State -> IORef [Objective (SV, SV)])
    -> ([Objective (SV, SV)] -> [Objective (SV, SV)])
    -> IO ()
    -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef [Objective (SV, SV)]
    rOptGoals (Objective (SV, SV)
    obj' Objective (SV, SV) -> [Objective (SV, SV)] -> [Objective (SV, SV)]
    forall a. a -> [a] -> [a]
    :)
                                               (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> IO ()
    forall a. [String] -> a
    noInteractive [ "Adding an optimization objective:"
                                                               , "  Objective: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Objective SVal -> String
    forall a. Show a => a -> String
    show Objective SVal
    obj
                                                               ]

    -- | Generalization of 'Data.SBV.outputSVal'
    outputSVal :: MonadSymbolic m => SVal -> m ()
    outputSVal :: SVal -> m ()
    outputSVal (SVal _ (Left c :: CV
    c)) = do
      State
    st <- m State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv
      SV
    sv <- IO SV -> m SV
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SV -> m SV) -> IO SV -> m SV
    forall a b. (a -> b) -> a -> b
    $ State -> CV -> IO SV
    newConst State
    st CV
    c
      IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ State -> (State -> IORef [SV]) -> ([SV] -> [SV]) -> IO () -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef [SV]
    routs (SV
    svSV -> [SV] -> [SV]
    forall a. a -> [a] -> [a]
    :) (() -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())
    outputSVal (SVal _ (Right f :: Cached SV
    f)) = do
      State
    st <- m State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv
      SV
    sv <- IO SV -> m SV
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SV -> m SV) -> IO SV -> m SV
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> State -> IO SV
    uncache Cached SV
    f State
    st
      IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ State -> (State -> IORef [SV]) -> ([SV] -> [SV]) -> IO () -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef [SV]
    routs (SV
    svSV -> [SV] -> [SV]
    forall a. a -> [a] -> [a]
    :) (() -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())

    ---------------------------------------------------------------------------------
    -- * Cached values
    ---------------------------------------------------------------------------------

    -- | We implement a peculiar caching mechanism, applicable to the use case in
    -- implementation of SBV's.  Whenever we do a state based computation, we do
    -- not want to keep on evaluating it in the then-current state. That will
    -- produce essentially a semantically equivalent value. Thus, we want to run
    -- it only once, and reuse that result, capturing the sharing at the Haskell
    -- level. This is similar to the "type-safe observable sharing" work, but also
    -- takes into the account of how symbolic simulation executes.
    --
    -- See Andy Gill's type-safe obervable sharing trick for the inspiration behind
    -- this technique: <http://ku-fpg.github.io/files/Gill-09-TypeSafeReification.pdf>
    --
    -- Note that this is *not* a general memo utility!
    newtype Cached a = Cached (State -> IO a)

    -- | Cache a state-based computation
    cache :: (State -> IO a) -> Cached a
    cache :: (State -> IO a) -> Cached a
    cache = (State -> IO a) -> Cached a
    forall a. (State -> IO a) -> Cached a
    Cached

    -- | Uncache a previously cached computation
    uncache :: Cached SV -> State -> IO SV
    uncache :: Cached SV -> State -> IO SV
    uncache = (State -> IORef (Cache SV)) -> Cached SV -> State -> IO SV
    forall a. (State -> IORef (Cache a)) -> Cached a -> State -> IO a
    uncacheGen State -> IORef (Cache SV)
    rSVCache

    -- | An SMT array index is simply an int value
    newtype ArrayIndex = ArrayIndex { ArrayIndex -> Int
    unArrayIndex :: Int } deriving (ArrayIndex -> ArrayIndex -> Bool
    (ArrayIndex -> ArrayIndex -> Bool)
    -> (ArrayIndex -> ArrayIndex -> Bool) -> Eq ArrayIndex
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: ArrayIndex -> ArrayIndex -> Bool
    $c/= :: ArrayIndex -> ArrayIndex -> Bool
    == :: ArrayIndex -> ArrayIndex -> Bool
    $c== :: ArrayIndex -> ArrayIndex -> Bool
    Eq, Eq ArrayIndex
    Eq ArrayIndex =>
    (ArrayIndex -> ArrayIndex -> Ordering)
    -> (ArrayIndex -> ArrayIndex -> Bool)
    -> (ArrayIndex -> ArrayIndex -> Bool)
    -> (ArrayIndex -> ArrayIndex -> Bool)
    -> (ArrayIndex -> ArrayIndex -> Bool)
    -> (ArrayIndex -> ArrayIndex -> ArrayIndex)
    -> (ArrayIndex -> ArrayIndex -> ArrayIndex)
    -> Ord ArrayIndex
    ArrayIndex -> ArrayIndex -> Bool
    ArrayIndex -> ArrayIndex -> Ordering
    ArrayIndex -> ArrayIndex -> ArrayIndex
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: ArrayIndex -> ArrayIndex -> ArrayIndex
    $cmin :: ArrayIndex -> ArrayIndex -> ArrayIndex
    max :: ArrayIndex -> ArrayIndex -> ArrayIndex
    $cmax :: ArrayIndex -> ArrayIndex -> ArrayIndex
    >= :: ArrayIndex -> ArrayIndex -> Bool
    $c>= :: ArrayIndex -> ArrayIndex -> Bool
    > :: ArrayIndex -> ArrayIndex -> Bool
    $c> :: ArrayIndex -> ArrayIndex -> Bool
    <= :: ArrayIndex -> ArrayIndex -> Bool
    $c<= :: ArrayIndex -> ArrayIndex -> Bool
    < :: ArrayIndex -> ArrayIndex -> Bool
    $c< :: ArrayIndex -> ArrayIndex -> Bool
    compare :: ArrayIndex -> ArrayIndex -> Ordering
    $ccompare :: ArrayIndex -> ArrayIndex -> Ordering
    $cp1Ord :: Eq ArrayIndex
    Ord)

    -- | We simply show indexes as the underlying integer
    instance Show ArrayIndex where
      show :: ArrayIndex -> String
    show (ArrayIndex i :: Int
    i) = Int -> String
    forall a. Show a => a -> String
    show Int
    i

    -- | A functional array index is simply an int value
    newtype FArrayIndex = FArrayIndex { FArrayIndex -> Int
    unFArrayIndex :: Int } deriving (FArrayIndex -> FArrayIndex -> Bool
    (FArrayIndex -> FArrayIndex -> Bool)
    -> (FArrayIndex -> FArrayIndex -> Bool) -> Eq FArrayIndex
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: FArrayIndex -> FArrayIndex -> Bool
    $c/= :: FArrayIndex -> FArrayIndex -> Bool
    == :: FArrayIndex -> FArrayIndex -> Bool
    $c== :: FArrayIndex -> FArrayIndex -> Bool
    Eq, Eq FArrayIndex
    Eq FArrayIndex =>
    (FArrayIndex -> FArrayIndex -> Ordering)
    -> (FArrayIndex -> FArrayIndex -> Bool)
    -> (FArrayIndex -> FArrayIndex -> Bool)
    -> (FArrayIndex -> FArrayIndex -> Bool)
    -> (FArrayIndex -> FArrayIndex -> Bool)
    -> (FArrayIndex -> FArrayIndex -> FArrayIndex)
    -> (FArrayIndex -> FArrayIndex -> FArrayIndex)
    -> Ord FArrayIndex
    FArrayIndex -> FArrayIndex -> Bool
    FArrayIndex -> FArrayIndex -> Ordering
    FArrayIndex -> FArrayIndex -> FArrayIndex
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: FArrayIndex -> FArrayIndex -> FArrayIndex
    $cmin :: FArrayIndex -> FArrayIndex -> FArrayIndex
    max :: FArrayIndex -> FArrayIndex -> FArrayIndex
    $cmax :: FArrayIndex -> FArrayIndex -> FArrayIndex
    >= :: FArrayIndex -> FArrayIndex -> Bool
    $c>= :: FArrayIndex -> FArrayIndex -> Bool
    > :: FArrayIndex -> FArrayIndex -> Bool
    $c> :: FArrayIndex -> FArrayIndex -> Bool
    <= :: FArrayIndex -> FArrayIndex -> Bool
    $c<= :: FArrayIndex -> FArrayIndex -> Bool
    < :: FArrayIndex -> FArrayIndex -> Bool
    $c< :: FArrayIndex -> FArrayIndex -> Bool
    compare :: FArrayIndex -> FArrayIndex -> Ordering
    $ccompare :: FArrayIndex -> FArrayIndex -> Ordering
    $cp1Ord :: Eq FArrayIndex
    Ord)

    -- | We simply show indexes as the underlying integer
    instance Show FArrayIndex where
      show :: FArrayIndex -> String
    show (FArrayIndex i :: Int
    i) = Int -> String
    forall a. Show a => a -> String
    show Int
    i

    -- | Uncache, retrieving SMT array indexes
    uncacheAI :: Cached ArrayIndex -> State -> IO ArrayIndex
    uncacheAI :: Cached ArrayIndex -> State -> IO ArrayIndex
    uncacheAI = (State -> IORef (Cache ArrayIndex))
    -> Cached ArrayIndex -> State -> IO ArrayIndex
    forall a. (State -> IORef (Cache a)) -> Cached a -> State -> IO a
    uncacheGen State -> IORef (Cache ArrayIndex)
    rAICache

    -- | Uncache, retrieving Functional array indexes
    uncacheFAI :: Cached FArrayIndex -> State -> IO FArrayIndex
    uncacheFAI :: Cached FArrayIndex -> State -> IO FArrayIndex
    uncacheFAI = (State -> IORef (Cache FArrayIndex))
    -> Cached FArrayIndex -> State -> IO FArrayIndex
    forall a. (State -> IORef (Cache a)) -> Cached a -> State -> IO a
    uncacheGen State -> IORef (Cache FArrayIndex)
    rFAICache

    -- | Generic uncaching. Note that this is entirely safe, since we do it in the IO monad.
    uncacheGen :: (State -> IORef (Cache a)) -> Cached a -> State -> IO a
    uncacheGen :: (State -> IORef (Cache a)) -> Cached a -> State -> IO a
    uncacheGen getCache :: State -> IORef (Cache a)
    getCache (Cached f :: State -> IO a
    f) st :: State
    st = do
            let rCache :: IORef (Cache a)
    rCache = State -> IORef (Cache a)
    getCache State
    st
            Cache a
    stored <- IORef (Cache a) -> IO (Cache a)
    forall a. IORef a -> IO a
    readIORef IORef (Cache a)
    rCache
            StableName (State -> IO a)
    sn <- State -> IO a
    f (State -> IO a)
    -> IO (StableName (State -> IO a))
    -> IO (StableName (State -> IO a))
    forall a b. a -> b -> b
    `seq` (State -> IO a) -> IO (StableName (State -> IO a))
    forall a. a -> IO (StableName a)
    makeStableName State -> IO a
    f
            let h :: Int
    h = StableName (State -> IO a) -> Int
    forall a. StableName a -> Int
    hashStableName StableName (State -> IO a)
    sn
            case (Int
    h Int -> Cache a -> Maybe [(StableName (State -> IO a), a)]
    forall a. Int -> IntMap a -> Maybe a
    `IMap.lookup` Cache a
    stored) Maybe [(StableName (State -> IO a), a)]
    -> ([(StableName (State -> IO a), a)] -> Maybe a) -> Maybe a
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= (StableName (State -> IO a)
    sn StableName (State -> IO a)
    -> [(StableName (State -> IO a), a)] -> Maybe a
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    `lookup`) of
              Just r :: a
    r  -> a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    r
              Nothing -> do a
    r <- State -> IO a
    f State
    st
                            a
    r a -> IO () -> IO ()
    forall a b. a -> b -> b
    `seq` IORef (Cache a) -> (Cache a -> Cache a) -> IO ()
    forall a. IORef a -> (a -> a) -> IO ()
    R.modifyIORef' IORef (Cache a)
    rCache (([(StableName (State -> IO a), a)]
     -> [(StableName (State -> IO a), a)]
     -> [(StableName (State -> IO a), a)])
    -> Int -> [(StableName (State -> IO a), a)] -> Cache a -> Cache a
    forall a. (a -> a -> a) -> Int -> a -> IntMap a -> IntMap a
    IMap.insertWith [(StableName (State -> IO a), a)]
    -> [(StableName (State -> IO a), a)]
    -> [(StableName (State -> IO a), a)]
    forall a. [a] -> [a] -> [a]
    (++) Int
    h [(StableName (State -> IO a)
    sn, a
    r)])
                            a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    r

    -- | Representation of SMTLib Program versions. As of June 2015, we're dropping support
    -- for SMTLib1, and supporting SMTLib2 only. We keep this data-type around in case
    -- SMTLib3 comes along and we want to support 2 and 3 simultaneously.
    data SMTLibVersion = SMTLib2
                       deriving (SMTLibVersion
    SMTLibVersion -> SMTLibVersion -> Bounded SMTLibVersion
    forall a. a -> a -> Bounded a
    maxBound :: SMTLibVersion
    $cmaxBound :: SMTLibVersion
    minBound :: SMTLibVersion
    $cminBound :: SMTLibVersion
    Bounded, Int -> SMTLibVersion
    SMTLibVersion -> Int
    SMTLibVersion -> [SMTLibVersion]
    SMTLibVersion -> SMTLibVersion
    SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]
    SMTLibVersion -> SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]
    (SMTLibVersion -> SMTLibVersion)
    -> (SMTLibVersion -> SMTLibVersion)
    -> (Int -> SMTLibVersion)
    -> (SMTLibVersion -> Int)
    -> (SMTLibVersion -> [SMTLibVersion])
    -> (SMTLibVersion -> SMTLibVersion -> [SMTLibVersion])
    -> (SMTLibVersion -> SMTLibVersion -> [SMTLibVersion])
    -> (SMTLibVersion
        -> SMTLibVersion -> SMTLibVersion -> [SMTLibVersion])
    -> Enum SMTLibVersion
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    enumFromThenTo :: SMTLibVersion -> SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]
    $cenumFromThenTo :: SMTLibVersion -> SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]
    enumFromTo :: SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]
    $cenumFromTo :: SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]
    enumFromThen :: SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]
    $cenumFromThen :: SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]
    enumFrom :: SMTLibVersion -> [SMTLibVersion]
    $cenumFrom :: SMTLibVersion -> [SMTLibVersion]
    fromEnum :: SMTLibVersion -> Int
    $cfromEnum :: SMTLibVersion -> Int
    toEnum :: Int -> SMTLibVersion
    $ctoEnum :: Int -> SMTLibVersion
    pred :: SMTLibVersion -> SMTLibVersion
    $cpred :: SMTLibVersion -> SMTLibVersion
    succ :: SMTLibVersion -> SMTLibVersion
    $csucc :: SMTLibVersion -> SMTLibVersion
    Enum, SMTLibVersion -> SMTLibVersion -> Bool
    (SMTLibVersion -> SMTLibVersion -> Bool)
    -> (SMTLibVersion -> SMTLibVersion -> Bool) -> Eq SMTLibVersion
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: SMTLibVersion -> SMTLibVersion -> Bool
    $c/= :: SMTLibVersion -> SMTLibVersion -> Bool
    == :: SMTLibVersion -> SMTLibVersion -> Bool
    $c== :: SMTLibVersion -> SMTLibVersion -> Bool
    Eq, Int -> SMTLibVersion -> ShowS
    [SMTLibVersion] -> ShowS
    SMTLibVersion -> String
    (Int -> SMTLibVersion -> ShowS)
    -> (SMTLibVersion -> String)
    -> ([SMTLibVersion] -> ShowS)
    -> Show SMTLibVersion
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [SMTLibVersion] -> ShowS
    $cshowList :: [SMTLibVersion] -> ShowS
    show :: SMTLibVersion -> String
    $cshow :: SMTLibVersion -> String
    showsPrec :: Int -> SMTLibVersion -> ShowS
    $cshowsPrec :: Int -> SMTLibVersion -> ShowS
    Show)

    -- | The extension associated with the version
    smtLibVersionExtension :: SMTLibVersion -> String
    smtLibVersionExtension :: SMTLibVersion -> String
    smtLibVersionExtension SMTLib2 = "smt2"

    -- | Representation of an SMT-Lib program. In between pre and post goes the refuted models
    data SMTLibPgm = SMTLibPgm SMTLibVersion [String]

    instance NFData SMTLibVersion where rnf :: SMTLibVersion -> ()
    rnf a :: SMTLibVersion
    a               = SMTLibVersion
    a SMTLibVersion -> () -> ()
    forall a b. a -> b -> b
    `seq` ()
    instance NFData SMTLibPgm     where rnf :: SMTLibPgm -> ()
    rnf (SMTLibPgm v :: SMTLibVersion
    v p :: [String]
    p) = SMTLibVersion -> ()
    forall a. NFData a => a -> ()
    rnf SMTLibVersion
    v () -> () -> ()
    forall a b. a -> b -> b
    `seq` [String] -> ()
    forall a. NFData a => a -> ()
    rnf [String]
    p

    instance Show SMTLibPgm where
      show :: SMTLibPgm -> String
    show (SMTLibPgm _ pre :: [String]
    pre) = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate "\n" [String]
    pre

    -- Other Technicalities..
    instance NFData CV where
      rnf :: CV -> ()
    rnf (CV x :: Kind
    x y :: CVal
    y) = Kind
    x Kind -> () -> ()
    forall a b. a -> b -> b
    `seq` CVal
    y CVal -> () -> ()
    forall a b. a -> b -> b
    `seq` ()

    instance NFData GeneralizedCV where
      rnf :: GeneralizedCV -> ()
    rnf (ExtendedCV e :: ExtCV
    e) = ExtCV
    e ExtCV -> () -> ()
    forall a b. a -> b -> b
    `seq` ()
      rnf (RegularCV  c :: CV
    c) = CV
    c CV -> () -> ()
    forall a b. a -> b -> b
    `seq` ()

    #if MIN_VERSION_base(4,9,0)
    #else
    -- Can't really force this, but not a big deal
    instance NFData CallStack where
      rnf _ = ()
    #endif

    instance NFData Result where
      rnf :: Result -> ()
    rnf (Result kindInfo :: Set Kind
    kindInfo qcInfo :: [(String, CV)]
    qcInfo obs :: [(String, CV -> Bool, SV)]
    obs cgs :: [(String, [String])]
    cgs inps :: ([(Quantifier, NamedSymVar)], [NamedSymVar])
    inps consts :: [(SV, CV)]
    consts tbls :: [((Int, Kind, Kind), [SV])]
    tbls arrs :: [(Int, ArrayInfo)]
    arrs uis :: [(String, SBVType)]
    uis axs :: [(String, [String])]
    axs pgm :: SBVPgm
    pgm cstr :: Seq (Bool, [(String, String)], SV)
    cstr asserts :: [(String, Maybe CallStack, SV)]
    asserts outs :: [SV]
    outs)
            = Set Kind -> ()
    forall a. NFData a => a -> ()
    rnf Set Kind
    kindInfo () -> () -> ()
    forall a b. a -> b -> b
    `seq` [(String, CV)] -> ()
    forall a. NFData a => a -> ()
    rnf [(String, CV)]
    qcInfo  () -> () -> ()
    forall a b. a -> b -> b
    `seq` [(String, CV -> Bool, SV)] -> ()
    forall a. NFData a => a -> ()
    rnf [(String, CV -> Bool, SV)]
    obs    () -> () -> ()
    forall a b. a -> b -> b
    `seq` [(String, [String])] -> ()
    forall a. NFData a => a -> ()
    rnf [(String, [String])]
    cgs
                           () -> () -> ()
    forall a b. a -> b -> b
    `seq` ([(Quantifier, NamedSymVar)], [NamedSymVar]) -> ()
    forall a. NFData a => a -> ()
    rnf ([(Quantifier, NamedSymVar)], [NamedSymVar])
    inps    () -> () -> ()
    forall a b. a -> b -> b
    `seq` [(SV, CV)] -> ()
    forall a. NFData a => a -> ()
    rnf [(SV, CV)]
    consts () -> () -> ()
    forall a b. a -> b -> b
    `seq` [((Int, Kind, Kind), [SV])] -> ()
    forall a. NFData a => a -> ()
    rnf [((Int, Kind, Kind), [SV])]
    tbls
                           () -> () -> ()
    forall a b. a -> b -> b
    `seq` [(Int, ArrayInfo)] -> ()
    forall a. NFData a => a -> ()
    rnf [(Int, ArrayInfo)]
    arrs    () -> () -> ()
    forall a b. a -> b -> b
    `seq` [(String, SBVType)] -> ()
    forall a. NFData a => a -> ()
    rnf [(String, SBVType)]
    uis    () -> () -> ()
    forall a b. a -> b -> b
    `seq` [(String, [String])] -> ()
    forall a. NFData a => a -> ()
    rnf [(String, [String])]
    axs
                           () -> () -> ()
    forall a b. a -> b -> b
    `seq` SBVPgm -> ()
    forall a. NFData a => a -> ()
    rnf SBVPgm
    pgm     () -> () -> ()
    forall a b. a -> b -> b
    `seq` Seq (Bool, [(String, String)], SV) -> ()
    forall a. NFData a => a -> ()
    rnf Seq (Bool, [(String, String)], SV)
    cstr   () -> () -> ()
    forall a b. a -> b -> b
    `seq` [(String, Maybe CallStack, SV)] -> ()
    forall a. NFData a => a -> ()
    rnf [(String, Maybe CallStack, SV)]
    asserts
                           () -> () -> ()
    forall a b. a -> b -> b
    `seq` [SV] -> ()
    forall a. NFData a => a -> ()
    rnf [SV]
    outs
    instance NFData Kind         where rnf :: Kind -> ()
    rnf a :: Kind
    a          = Kind -> () -> ()
    forall a b. a -> b -> b
    seq Kind
    a ()
    instance NFData ArrayContext where rnf :: ArrayContext -> ()
    rnf a :: ArrayContext
    a          = ArrayContext -> () -> ()
    forall a b. a -> b -> b
    seq ArrayContext
    a ()
    instance NFData SV           where rnf :: SV -> ()
    rnf a :: SV
    a          = SV -> () -> ()
    forall a b. a -> b -> b
    seq SV
    a ()
    instance NFData SBVExpr      where rnf :: SBVExpr -> ()
    rnf a :: SBVExpr
    a          = SBVExpr -> () -> ()
    forall a b. a -> b -> b
    seq SBVExpr
    a ()
    instance NFData Quantifier   where rnf :: Quantifier -> ()
    rnf a :: Quantifier
    a          = Quantifier -> () -> ()
    forall a b. a -> b -> b
    seq Quantifier
    a ()
    instance NFData SBVType      where rnf :: SBVType -> ()
    rnf a :: SBVType
    a          = SBVType -> () -> ()
    forall a b. a -> b -> b
    seq SBVType
    a ()
    instance NFData SBVPgm       where rnf :: SBVPgm -> ()
    rnf a :: SBVPgm
    a          = SBVPgm -> () -> ()
    forall a b. a -> b -> b
    seq SBVPgm
    a ()
    instance NFData (Cached a)   where rnf :: Cached a -> ()
    rnf (Cached f :: State -> IO a
    f) = State -> IO a
    f (State -> IO a) -> () -> ()
    forall a b. a -> b -> b
    `seq` ()
    instance NFData SVal         where rnf :: SVal -> ()
    rnf (SVal x :: Kind
    x y :: Either CV (Cached SV)
    y) = Kind -> ()
    forall a. NFData a => a -> ()
    rnf Kind
    x () -> () -> ()
    forall a b. a -> b -> b
    `seq` Either CV (Cached SV) -> ()
    forall a. NFData a => a -> ()
    rnf Either CV (Cached SV)
    y

    instance NFData SMTResult where
      rnf :: SMTResult -> ()
    rnf (Unsatisfiable _ xs :: Maybe [String]
    xs   ) = Maybe [String] -> ()
    forall a. NFData a => a -> ()
    rnf Maybe [String]
    xs
      rnf (Satisfiable _   xs :: SMTModel
    xs   ) = SMTModel -> ()
    forall a. NFData a => a -> ()
    rnf SMTModel
    xs
      rnf (SatExtField _   xs :: SMTModel
    xs   ) = SMTModel -> ()
    forall a. NFData a => a -> ()
    rnf SMTModel
    xs
      rnf (Unknown _       xs :: SMTReasonUnknown
    xs   ) = SMTReasonUnknown -> ()
    forall a. NFData a => a -> ()
    rnf SMTReasonUnknown
    xs
      rnf (ProofError _    xs :: [String]
    xs mr :: Maybe SMTResult
    mr) = [String] -> ()
    forall a. NFData a => a -> ()
    rnf [String]
    xs () -> () -> ()
    forall a b. a -> b -> b
    `seq` Maybe SMTResult -> ()
    forall a. NFData a => a -> ()
    rnf Maybe SMTResult
    mr

    instance NFData SMTModel where
      rnf :: SMTModel -> ()
    rnf (SMTModel objs :: [(String, GeneralizedCV)]
    objs bndgs :: Maybe [((Quantifier, NamedSymVar), Maybe CV)]
    bndgs assocs :: [(String, CV)]
    assocs uifuns :: [(String, (SBVType, ([([CV], CV)], CV)))]
    uifuns) = [(String, GeneralizedCV)] -> ()
    forall a. NFData a => a -> ()
    rnf [(String, GeneralizedCV)]
    objs () -> () -> ()
    forall a b. a -> b -> b
    `seq` Maybe [((Quantifier, NamedSymVar), Maybe CV)] -> ()
    forall a. NFData a => a -> ()
    rnf Maybe [((Quantifier, NamedSymVar), Maybe CV)]
    bndgs () -> () -> ()
    forall a b. a -> b -> b
    `seq` [(String, CV)] -> ()
    forall a. NFData a => a -> ()
    rnf [(String, CV)]
    assocs () -> () -> ()
    forall a b. a -> b -> b
    `seq` [(String, (SBVType, ([([CV], CV)], CV)))] -> ()
    forall a. NFData a => a -> ()
    rnf [(String, (SBVType, ([([CV], CV)], CV)))]
    uifuns

    instance NFData SMTScript where
      rnf :: SMTScript -> ()
    rnf (SMTScript b :: String
    b m :: [String]
    m) = String -> ()
    forall a. NFData a => a -> ()
    rnf String
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` [String] -> ()
    forall a. NFData a => a -> ()
    rnf [String]
    m

    -- | Translation tricks needed for specific capabilities afforded by each solver
    data SolverCapabilities = SolverCapabilities {
             SolverCapabilities -> Bool
    supportsQuantifiers        :: Bool           -- ^ Supports SMT-Lib2 style quantifiers?
           , SolverCapabilities -> Bool
    supportsUninterpretedSorts :: Bool           -- ^ Supports SMT-Lib2 style uninterpreted-sorts
           , SolverCapabilities -> Bool
    supportsUnboundedInts      :: Bool           -- ^ Supports unbounded integers?
           , SolverCapabilities -> Bool
    supportsReals              :: Bool           -- ^ Supports reals?
           , SolverCapabilities -> Bool
    supportsApproxReals        :: Bool           -- ^ Supports printing of approximations of reals?
           , SolverCapabilities -> Bool
    supportsIEEE754            :: Bool           -- ^ Supports floating point numbers?
           , SolverCapabilities -> Bool
    supportsSets               :: Bool           -- ^ Supports set operations?
           , SolverCapabilities -> Bool
    supportsOptimization       :: Bool           -- ^ Supports optimization routines?
           , SolverCapabilities -> Bool
    supportsPseudoBooleans     :: Bool           -- ^ Supports pseudo-boolean operations?
           , SolverCapabilities -> Bool
    supportsCustomQueries      :: Bool           -- ^ Supports interactive queries per SMT-Lib?
           , SolverCapabilities -> Bool
    supportsGlobalDecls        :: Bool           -- ^ Supports global declarations? (Needed for push-pop.)
           , SolverCapabilities -> Bool
    supportsDataTypes          :: Bool           -- ^ Supports datatypes?
           , SolverCapabilities -> Maybe [String]
    supportsFlattenedModels    :: Maybe [String] -- ^ Supports flattened model output? (With given config lines.)
           }

    -- | Rounding mode to be used for the IEEE floating-point operations.
    -- Note that Haskell's default is 'RoundNearestTiesToEven'. If you use
    -- a different rounding mode, then the counter-examples you get may not
    -- match what you observe in Haskell.
    data RoundingMode = RoundNearestTiesToEven  -- ^ Round to nearest representable floating point value.
                                                -- If precisely at half-way, pick the even number.
                                                -- (In this context, /even/ means the lowest-order bit is zero.)
                      | RoundNearestTiesToAway  -- ^ Round to nearest representable floating point value.
                                                -- If precisely at half-way, pick the number further away from 0.
                                                -- (That is, for positive values, pick the greater; for negative values, pick the smaller.)
                      | RoundTowardPositive     -- ^ Round towards positive infinity. (Also known as rounding-up or ceiling.)
                      | RoundTowardNegative     -- ^ Round towards negative infinity. (Also known as rounding-down or floor.)
                      | RoundTowardZero         -- ^ Round towards zero. (Also known as truncation.)
                      deriving (RoundingMode -> RoundingMode -> Bool
    (RoundingMode -> RoundingMode -> Bool)
    -> (RoundingMode -> RoundingMode -> Bool) -> Eq RoundingMode
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: RoundingMode -> RoundingMode -> Bool
    $c/= :: RoundingMode -> RoundingMode -> Bool
    == :: RoundingMode -> RoundingMode -> Bool
    $c== :: RoundingMode -> RoundingMode -> Bool
    Eq, Eq RoundingMode
    Eq RoundingMode =>
    (RoundingMode -> RoundingMode -> Ordering)
    -> (RoundingMode -> RoundingMode -> Bool)
    -> (RoundingMode -> RoundingMode -> Bool)
    -> (RoundingMode -> RoundingMode -> Bool)
    -> (RoundingMode -> RoundingMode -> Bool)
    -> (RoundingMode -> RoundingMode -> RoundingMode)
    -> (RoundingMode -> RoundingMode -> RoundingMode)
    -> Ord RoundingMode
    RoundingMode -> RoundingMode -> Bool
    RoundingMode -> RoundingMode -> Ordering
    RoundingMode -> RoundingMode -> RoundingMode
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: RoundingMode -> RoundingMode -> RoundingMode
    $cmin :: RoundingMode -> RoundingMode -> RoundingMode
    max :: RoundingMode -> RoundingMode -> RoundingMode
    $cmax :: RoundingMode -> RoundingMode -> RoundingMode
    >= :: RoundingMode -> RoundingMode -> Bool
    $c>= :: RoundingMode -> RoundingMode -> Bool
    > :: RoundingMode -> RoundingMode -> Bool
    $c> :: RoundingMode -> RoundingMode -> Bool
    <= :: RoundingMode -> RoundingMode -> Bool
    $c<= :: RoundingMode -> RoundingMode -> Bool
    < :: RoundingMode -> RoundingMode -> Bool
    $c< :: RoundingMode -> RoundingMode -> Bool
    compare :: RoundingMode -> RoundingMode -> Ordering
    $ccompare :: RoundingMode -> RoundingMode -> Ordering
    $cp1Ord :: Eq RoundingMode
    Ord, Int -> RoundingMode -> ShowS
    [RoundingMode] -> ShowS
    RoundingMode -> String
    (Int -> RoundingMode -> ShowS)
    -> (RoundingMode -> String)
    -> ([RoundingMode] -> ShowS)
    -> Show RoundingMode
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [RoundingMode] -> ShowS
    $cshowList :: [RoundingMode] -> ShowS
    show :: RoundingMode -> String
    $cshow :: RoundingMode -> String
    showsPrec :: Int -> RoundingMode -> ShowS
    $cshowsPrec :: Int -> RoundingMode -> ShowS
    Show, ReadPrec [RoundingMode]
    ReadPrec RoundingMode
    Int -> ReadS RoundingMode
    ReadS [RoundingMode]
    (Int -> ReadS RoundingMode)
    -> ReadS [RoundingMode]
    -> ReadPrec RoundingMode
    -> ReadPrec [RoundingMode]
    -> Read RoundingMode
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    readListPrec :: ReadPrec [RoundingMode]
    $creadListPrec :: ReadPrec [RoundingMode]
    readPrec :: ReadPrec RoundingMode
    $creadPrec :: ReadPrec RoundingMode
    readList :: ReadS [RoundingMode]
    $creadList :: ReadS [RoundingMode]
    readsPrec :: Int -> ReadS RoundingMode
    $creadsPrec :: Int -> ReadS RoundingMode
    Read, Typeable RoundingMode
    DataType
    Constr
    Typeable RoundingMode =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> RoundingMode -> c RoundingMode)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c RoundingMode)
    -> (RoundingMode -> Constr)
    -> (RoundingMode -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c RoundingMode))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c RoundingMode))
    -> ((forall b. Data b => b -> b) -> RoundingMode -> RoundingMode)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r)
    -> (forall u. (forall d. Data d => d -> u) -> RoundingMode -> [u])
    -> (forall u.
        Int -> (forall d. Data d => d -> u) -> RoundingMode -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode)
    -> Data RoundingMode
    RoundingMode -> DataType
    RoundingMode -> Constr
    (forall b. Data b => b -> b) -> RoundingMode -> RoundingMode
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> RoundingMode -> c RoundingMode
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c RoundingMode
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> RoundingMode -> u
    forall u. (forall d. Data d => d -> u) -> RoundingMode -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c RoundingMode
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> RoundingMode -> c RoundingMode
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c RoundingMode)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c RoundingMode)
    $cRoundTowardZero :: Constr
    $cRoundTowardNegative :: Constr
    $cRoundTowardPositive :: Constr
    $cRoundNearestTiesToAway :: Constr
    $cRoundNearestTiesToEven :: Constr
    $tRoundingMode :: DataType
    gmapMo :: (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
    gmapMp :: (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
    gmapM :: (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
    gmapQi :: Int -> (forall d. Data d => d -> u) -> RoundingMode -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RoundingMode -> u
    gmapQ :: (forall d. Data d => d -> u) -> RoundingMode -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> RoundingMode -> [u]
    gmapQr :: (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
    gmapQl :: (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
    gmapT :: (forall b. Data b => b -> b) -> RoundingMode -> RoundingMode
    $cgmapT :: (forall b. Data b => b -> b) -> RoundingMode -> RoundingMode
    dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c RoundingMode)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c RoundingMode)
    dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c RoundingMode)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c RoundingMode)
    dataTypeOf :: RoundingMode -> DataType
    $cdataTypeOf :: RoundingMode -> DataType
    toConstr :: RoundingMode -> Constr
    $ctoConstr :: RoundingMode -> Constr
    gunfold :: (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c RoundingMode
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c RoundingMode
    gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> RoundingMode -> c RoundingMode
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> RoundingMode -> c RoundingMode
    $cp1Data :: Typeable RoundingMode
    G.Data, RoundingMode
    RoundingMode -> RoundingMode -> Bounded RoundingMode
    forall a. a -> a -> Bounded a
    maxBound :: RoundingMode
    $cmaxBound :: RoundingMode
    minBound :: RoundingMode
    $cminBound :: RoundingMode
    Bounded, Int -> RoundingMode
    RoundingMode -> Int
    RoundingMode -> [RoundingMode]
    RoundingMode -> RoundingMode
    RoundingMode -> RoundingMode -> [RoundingMode]
    RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode]
    (RoundingMode -> RoundingMode)
    -> (RoundingMode -> RoundingMode)
    -> (Int -> RoundingMode)
    -> (RoundingMode -> Int)
    -> (RoundingMode -> [RoundingMode])
    -> (RoundingMode -> RoundingMode -> [RoundingMode])
    -> (RoundingMode -> RoundingMode -> [RoundingMode])
    -> (RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode])
    -> Enum RoundingMode
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    enumFromThenTo :: RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode]
    $cenumFromThenTo :: RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode]
    enumFromTo :: RoundingMode -> RoundingMode -> [RoundingMode]
    $cenumFromTo :: RoundingMode -> RoundingMode -> [RoundingMode]
    enumFromThen :: RoundingMode -> RoundingMode -> [RoundingMode]
    $cenumFromThen :: RoundingMode -> RoundingMode -> [RoundingMode]
    enumFrom :: RoundingMode -> [RoundingMode]
    $cenumFrom :: RoundingMode -> [RoundingMode]
    fromEnum :: RoundingMode -> Int
    $cfromEnum :: RoundingMode -> Int
    toEnum :: Int -> RoundingMode
    $ctoEnum :: Int -> RoundingMode
    pred :: RoundingMode -> RoundingMode
    $cpred :: RoundingMode -> RoundingMode
    succ :: RoundingMode -> RoundingMode
    $csucc :: RoundingMode -> RoundingMode
    Enum)

    -- | 'RoundingMode' kind
    instance HasKind RoundingMode

    -- | Solver configuration. See also 'Data.SBV.z3', 'Data.SBV.yices', 'Data.SBV.cvc4', 'Data.SBV.boolector', 'Data.SBV.mathSAT', etc.
    -- which are instantiations of this type for those solvers, with reasonable defaults. In particular, custom configuration can be
    -- created by varying those values. (Such as @z3{verbose=True}@.)
    --
    -- Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does
    -- not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to
    -- emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite
    -- precision value on the screen. The field 'printRealPrec' controls the printing precision, by specifying the number of digits after
    -- the decimal point. The default value is 16, but it can be set to any positive integer.
    --
    -- When printing, SBV will add the suffix @...@ at the and of a real-value, if the given bound is not sufficient to represent the real-value
    -- exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it
    -- is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation
    -- of the real value is not finite, i.e., if it is not rational.
    --
    -- The 'printBase' field can be used to print numbers in base 2, 10, or 16. If base 2 or 16 is used, then floating-point values will
    -- be printed in their internal memory-layout format as well, which can come in handy for bit-precise analysis.
    data SMTConfig = SMTConfig {
             SMTConfig -> Bool
    verbose                     :: Bool           -- ^ Debug mode
           , SMTConfig -> Timing
    timing                      :: Timing         -- ^ Print timing information on how long different phases took (construction, solving, etc.)
           , SMTConfig -> Int
    printBase                   :: Int            -- ^ Print integral literals in this base (2, 10, and 16 are supported.)
           , SMTConfig -> Int
    printRealPrec               :: Int            -- ^ Print algebraic real values with this precision. (SReal, default: 16)
           , SMTConfig -> String
    satCmd                      :: String         -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics.
           , SMTConfig -> Maybe Int
    allSatMaxModelCount         :: Maybe Int      -- ^ In a 'Data.SBV.allSat' call, return at most this many models. If nothing, return all.
           , SMTConfig -> Bool
    allSatPrintAlong            :: Bool           -- ^ In a 'Data.SBV.allSat' call, print models as they are found.
           , SMTConfig -> Bool
    satTrackUFs                 :: Bool           -- ^ In a 'Data.SBV.sat' call, should we try to extract values of uninterpreted functions?
           , SMTConfig -> String -> Bool
    isNonModelVar               :: String -> Bool -- ^ When constructing a model, ignore variables whose name satisfy this predicate. (Default: (const False), i.e., don't ignore anything)
           , SMTConfig -> Bool
    validateModel               :: Bool           -- ^ If set, SBV will attempt to validate the model it gets back from the solver.
           , SMTConfig -> Bool
    optimizeValidateConstraints :: Bool           -- ^ Validate optimization results. NB: Does NOT make sure the model is optimal, just checks they satisfy the constraints.
           , SMTConfig -> Maybe String
    transcript                  :: Maybe FilePath -- ^ If Just, the entire interaction will be recorded as a playable file (for debugging purposes mostly)
           , SMTConfig -> SMTLibVersion
    smtLibVersion               :: SMTLibVersion  -- ^ What version of SMT-lib we use for the tool
           , SMTConfig -> SMTSolver
    solver                      :: SMTSolver      -- ^ The actual SMT solver.
           , SMTConfig -> Bool
    allowQuantifiedQueries      :: Bool           -- ^ Should we permit use of quantifiers in the query mode? (Default: False. See <http://github.com/LeventErkok/sbv/issues/459> for why.)
           , SMTConfig -> RoundingMode
    roundingMode                :: RoundingMode   -- ^ Rounding mode to use for floating-point conversions
           , SMTConfig -> [SMTOption]
    solverSetOptions            :: [SMTOption]    -- ^ Options to set as we start the solver
           , SMTConfig -> Bool
    ignoreExitCode              :: Bool           -- ^ If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess.
           , SMTConfig -> Maybe String
    redirectVerbose             :: Maybe FilePath -- ^ Redirect the verbose output to this file if given. If Nothing, stdout is implied.
           }

    -- | Returns true if we have to perform validation
    validationRequested :: SMTConfig -> Bool
    validationRequested :: SMTConfig -> Bool
    validationRequested SMTConfig{Bool
    validateModel :: Bool
    validateModel :: SMTConfig -> Bool
    validateModel, Bool
    optimizeValidateConstraints :: Bool
    optimizeValidateConstraints :: SMTConfig -> Bool
    optimizeValidateConstraints} = Bool
    validateModel Bool -> Bool -> Bool
    || Bool
    optimizeValidateConstraints

    -- We're just seq'ing top-level here, it shouldn't really matter. (i.e., no need to go deeper.)
    instance NFData SMTConfig where
      rnf :: SMTConfig -> ()
    rnf SMTConfig{} = ()

    -- | A model, as returned by a solver
    data SMTModel = SMTModel {
           SMTModel -> [(String, GeneralizedCV)]
    modelObjectives :: [(String, GeneralizedCV)]                     -- ^ Mapping of symbolic values to objective values.
         , SMTModel -> Maybe [((Quantifier, NamedSymVar), Maybe CV)]
    modelBindings   :: Maybe [((Quantifier, NamedSymVar), Maybe CV)] -- ^ Mapping of input variables as reported by the solver. Only collected if model validation is requested.
         , SMTModel -> [(String, CV)]
    modelAssocs     :: [(String, CV)]                                -- ^ Mapping of symbolic values to constants.
         , SMTModel -> [(String, (SBVType, ([([CV], CV)], CV)))]
    modelUIFuns     :: [(String, (SBVType, ([([CV], CV)], CV)))]     -- ^ Mapping of uninterpreted functions to association lists in the model.
                                                                            -- Note that an uninterpreted constant (function of arity 0) will be stored
                                                                            -- in the 'modelAssocs' field.
         }
         deriving Int -> SMTModel -> ShowS
    [SMTModel] -> ShowS
    SMTModel -> String
    (Int -> SMTModel -> ShowS)
    -> (SMTModel -> String) -> ([SMTModel] -> ShowS) -> Show SMTModel
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [SMTModel] -> ShowS
    $cshowList :: [SMTModel] -> ShowS
    show :: SMTModel -> String
    $cshow :: SMTModel -> String
    showsPrec :: Int -> SMTModel -> ShowS
    $cshowsPrec :: Int -> SMTModel -> ShowS
    Show

    -- | The result of an SMT solver call. Each constructor is tagged with
    -- the 'SMTConfig' that created it so that further tools can inspect it
    -- and build layers of results, if needed. For ordinary uses of the library,
    -- this type should not be needed, instead use the accessor functions on
    -- it. (Custom Show instances and model extractors.)
    data SMTResult = Unsatisfiable SMTConfig (Maybe [String])            -- ^ Unsatisfiable. If unsat-cores are enabled, they will be returned in the second parameter.
                   | Satisfiable   SMTConfig SMTModel                    -- ^ Satisfiable with model
                   | SatExtField   SMTConfig SMTModel                    -- ^ Prover returned a model, but in an extension field containing Infinite/epsilon
                   | Unknown       SMTConfig SMTReasonUnknown            -- ^ Prover returned unknown, with the given reason
                   | ProofError    SMTConfig [String] (Maybe SMTResult)  -- ^ Prover errored out, with possibly a bogus result

    -- | A script, to be passed to the solver.
    data SMTScript = SMTScript {
              SMTScript -> String
    scriptBody  :: String   -- ^ Initial feed
            , SMTScript -> [String]
    scriptModel :: [String] -- ^ Continuation script, to extract results
            }

    -- | An SMT engine
    type SMTEngine =  forall res.
                      SMTConfig         -- ^ current configuration
                   -> State             -- ^ the state in which to run the engine
                   -> String            -- ^ program
                   -> (State -> IO res) -- ^ continuation
                   -> IO res

    -- | Solvers that SBV is aware of
    data Solver = Z3
                | Yices
                | Boolector
                | CVC4
                | MathSAT
                | ABC
                deriving (Int -> Solver -> ShowS
    [Solver] -> ShowS
    Solver -> String
    (Int -> Solver -> ShowS)
    -> (Solver -> String) -> ([Solver] -> ShowS) -> Show Solver
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Solver] -> ShowS
    $cshowList :: [Solver] -> ShowS
    show :: Solver -> String
    $cshow :: Solver -> String
    showsPrec :: Int -> Solver -> ShowS
    $cshowsPrec :: Int -> Solver -> ShowS
    Show, Int -> Solver
    Solver -> Int
    Solver -> [Solver]
    Solver -> Solver
    Solver -> Solver -> [Solver]
    Solver -> Solver -> Solver -> [Solver]
    (Solver -> Solver)
    -> (Solver -> Solver)
    -> (Int -> Solver)
    -> (Solver -> Int)
    -> (Solver -> [Solver])
    -> (Solver -> Solver -> [Solver])
    -> (Solver -> Solver -> [Solver])
    -> (Solver -> Solver -> Solver -> [Solver])
    -> Enum Solver
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    enumFromThenTo :: Solver -> Solver -> Solver -> [Solver]
    $cenumFromThenTo :: Solver -> Solver -> Solver -> [Solver]
    enumFromTo :: Solver -> Solver -> [Solver]
    $cenumFromTo :: Solver -> Solver -> [Solver]
    enumFromThen :: Solver -> Solver -> [Solver]
    $cenumFromThen :: Solver -> Solver -> [Solver]
    enumFrom :: Solver -> [Solver]
    $cenumFrom :: Solver -> [Solver]
    fromEnum :: Solver -> Int
    $cfromEnum :: Solver -> Int
    toEnum :: Int -> Solver
    $ctoEnum :: Int -> Solver
    pred :: Solver -> Solver
    $cpred :: Solver -> Solver
    succ :: Solver -> Solver
    $csucc :: Solver -> Solver
    Enum, Solver
    Solver -> Solver -> Bounded Solver
    forall a. a -> a -> Bounded a
    maxBound :: Solver
    $cmaxBound :: Solver
    minBound :: Solver
    $cminBound :: Solver
    Bounded)

    -- | An SMT solver
    data SMTSolver = SMTSolver {
             SMTSolver -> Solver
    name           :: Solver                -- ^ The solver in use
           , SMTSolver -> String
    executable     :: String                -- ^ The path to its executable
           , SMTSolver -> ShowS
    preprocess     :: String -> String      -- ^ Each line sent to the solver will be passed through this function (typically id)
           , SMTSolver -> SMTConfig -> [String]
    options        :: SMTConfig -> [String] -- ^ Options to provide to the solver
           , SMTSolver
    -> forall res.
       SMTConfig -> State -> String -> (State -> IO res) -> IO res
    engine         :: SMTEngine             -- ^ The solver engine, responsible for interpreting solver output
           , SMTSolver -> SolverCapabilities
    capabilities   :: SolverCapabilities    -- ^ Various capabilities of the solver
           }

    -- | Query execution context
    data QueryContext = QueryInternal       -- ^ Triggered from inside SBV
                      | QueryExternal       -- ^ Triggered from user code

    -- | Show instance for 'QueryContext', for debugging purposes
    instance Show QueryContext where
       show :: QueryContext -> String
    show QueryInternal = "Internal Query"
       show QueryExternal = "User Query"

    {-# ANN type FPOp ("HLint: ignore Use camelCase" :: String) #-}
    {-# ANN type PBOp ("HLint: ignore Use camelCase" :: String) #-}
    {-# ANN type OvOp ("HLint: ignore Use camelCase" :: String) #-}