grisette-0.11.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2024
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellTrustworthy
LanguageHaskell2010

Grisette.Internal.Core.Data.Class.SafeLinearArith

Description

 
Synopsis

Documentation

data ArithException #

Arithmetic exceptions.

Instances

Instances details
Exception ArithException

@since base-4.0.0.0

Instance details

Defined in GHC.Internal.Exception.Type

Show ArithException

@since base-4.0.0.0

Instance details

Defined in GHC.Internal.Exception.Type

Eq ArithException

@since base-3.0

Instance details

Defined in GHC.Internal.Exception.Type

Ord ArithException

@since base-3.0

Instance details

Defined in GHC.Internal.Exception.Type

Mergeable ArithException Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.Mergeable

TransformError ArithException AssertionError Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.Error

(MonadError ArithException m, TryMerge m) => SafeFdiv ArithException AlgReal m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFdiv

(MonadError ArithException m, MonadUnion m) => SafeFdiv ArithException SymAlgReal m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFdiv

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Int16 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Int32 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Int64 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Int8 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

Methods

safeAdd :: Int8 -> Int8 -> m Int8 Source #

safeNeg :: Int8 -> m Int8 Source #

safeSub :: Int8 -> Int8 -> m Int8 Source #

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Word16 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Word32 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Word64 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Word8 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException SymInteger m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Integer m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Int m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

Methods

safeAdd :: Int -> Int -> m Int Source #

safeNeg :: Int -> m Int Source #

safeSub :: Int -> Int -> m Int Source #

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Word m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

Methods

safeAdd :: Word -> Word -> m Word Source #

safeNeg :: Word -> m Word Source #

safeSub :: Word -> Word -> m Word Source #

(MonadError ArithException m, MonadUnion m) => SafeLogBase ArithException SymAlgReal m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLogBase

(MonadError ArithException m, TryMerge m) => SafeSymRotate ArithException Int16 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate

(MonadError ArithException m, TryMerge m) => SafeSymRotate ArithException Int32 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate

(MonadError ArithException m, TryMerge m) => SafeSymRotate ArithException Int64 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate

(MonadError ArithException m, TryMerge m) => SafeSymRotate ArithException Int8 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate

(MonadError ArithException m, TryMerge m) => SafeSymRotate ArithException Word16 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate

(MonadError ArithException m, TryMerge m) => SafeSymRotate ArithException Word32 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate

(MonadError ArithException m, TryMerge m) => SafeSymRotate ArithException Word64 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate

(MonadError ArithException m, TryMerge m) => SafeSymRotate ArithException Word8 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate

(MonadError ArithException m, TryMerge m) => SafeSymRotate ArithException Int m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate

(MonadError ArithException m, TryMerge m) => SafeSymRotate ArithException Word m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate

(MonadError ArithException m, TryMerge m) => SafeSymShift ArithException Int16 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymShift

(MonadError ArithException m, TryMerge m) => SafeSymShift ArithException Int32 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymShift

(MonadError ArithException m, TryMerge m) => SafeSymShift ArithException Int64 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymShift

(MonadError ArithException m, TryMerge m) => SafeSymShift ArithException Int8 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymShift

(MonadError ArithException m, TryMerge m) => SafeSymShift ArithException Word16 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymShift

(MonadError ArithException m, TryMerge m) => SafeSymShift ArithException Word32 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymShift

(MonadError ArithException m, TryMerge m) => SafeSymShift ArithException Word64 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymShift

(MonadError ArithException m, TryMerge m) => SafeSymShift ArithException Word8 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymShift

(MonadError ArithException m, TryMerge m) => SafeSymShift ArithException Int m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymShift

(MonadError ArithException m, TryMerge m) => SafeSymShift ArithException Word m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymShift

(MonadError ArithException m, TryMerge m) => SafeDiv ArithException Int16 m Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv

(MonadError ArithException m, TryMerge m) => SafeDiv ArithException Int32 m Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv

(MonadError ArithException m, TryMerge m) => SafeDiv ArithException Int64 m Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv

(MonadError ArithException m, TryMerge m) => SafeDiv ArithException Int8 m Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv

(MonadError ArithException m, TryMerge m) => SafeDiv ArithException Word16 m Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv

(MonadError ArithException m, TryMerge m) => SafeDiv ArithException Word32 m Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv

(MonadError ArithException m, TryMerge m) => SafeDiv ArithException Word64 m Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv

(MonadError ArithException m, TryMerge m) => SafeDiv ArithException Word8 m Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv

(MonadUnion m, MonadError ArithException m) => SafeDiv ArithException SymInteger m Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv

(MonadError ArithException m, TryMerge m) => SafeDiv ArithException Integer m Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv

(MonadError ArithException m, TryMerge m) => SafeDiv ArithException Int m Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv

Methods

safeDiv :: Int -> Int -> m Int Source #

safeMod :: Int -> Int -> m Int Source #

safeDivMod :: Int -> Int -> m (Int, Int) Source #

safeQuot :: Int -> Int -> m Int Source #

safeRem :: Int -> Int -> m Int Source #

safeQuotRem :: Int -> Int -> m (Int, Int) Source #

(MonadError ArithException m, TryMerge m) => SafeDiv ArithException Word m Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv

(MonadError ArithException m, UnifiedBranching 'S m) => UnifiedSafeDiv 'S ArithException SymInteger m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

(MonadError ArithException m, UnifiedBranching mode m) => UnifiedSafeDiv mode ArithException Integer m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

(MonadError ArithException m, UnifiedBranching 'S m) => UnifiedSafeFdiv 'S ArithException SymAlgReal m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFdiv

(MonadError ArithException m, UnifiedBranching mode m) => UnifiedSafeFdiv mode ArithException AlgReal m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFdiv

(MonadError ArithException m, UnifiedBranching 'S m) => UnifiedSafeLinearArith 'S ArithException SymInteger m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

(MonadError ArithException m, UnifiedBranching mode m) => UnifiedSafeLinearArith mode ArithException Integer m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeDiv 'S ArithException (SymIntN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeDiv 'S ArithException (SymWordN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeDiv mode ArithException (IntN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

Methods

withBaseSafeDiv :: (SafeDiv ArithException (IntN n) m => r) -> r Source #

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeDiv mode ArithException (WordN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

Methods

withBaseSafeDiv :: (SafeDiv ArithException (WordN n) m => r) -> r Source #

(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeLinearArith 'S ArithException (SymIntN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeLinearArith 'S ArithException (SymWordN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeLinearArith mode ArithException (IntN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeLinearArith mode ArithException (WordN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeSymRotate 'S ArithException (SymIntN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeSymRotate 'S ArithException (SymWordN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeSymRotate mode ArithException (IntN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeSymRotate mode ArithException (WordN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeSymShift 'S ArithException (SymIntN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeSymShift 'S ArithException (SymWordN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeSymShift mode ArithException (IntN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeSymShift mode ArithException (WordN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (IntN n) m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

Methods

safeAdd :: IntN n -> IntN n -> m (IntN n) Source #

safeNeg :: IntN n -> m (IntN n) Source #

safeSub :: IntN n -> IntN n -> m (IntN n) Source #

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (WordN n) m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

Methods

safeAdd :: WordN n -> WordN n -> m (WordN n) Source #

safeNeg :: WordN n -> m (WordN n) Source #

safeSub :: WordN n -> WordN n -> m (WordN n) Source #

(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymIntN n) m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

Methods

safeAdd :: SymIntN n -> SymIntN n -> m (SymIntN n) Source #

safeNeg :: SymIntN n -> m (SymIntN n) Source #

safeSub :: SymIntN n -> SymIntN n -> m (SymIntN n) Source #

(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymWordN n) m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

Methods

safeAdd :: SymWordN n -> SymWordN n -> m (SymWordN n) Source #

safeNeg :: SymWordN n -> m (SymWordN n) Source #

safeSub :: SymWordN n -> SymWordN n -> m (SymWordN n) Source #

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymRotate ArithException (IntN n) m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate

Methods

safeSymRotateL :: IntN n -> IntN n -> m (IntN n) Source #

safeSymRotateR :: IntN n -> IntN n -> m (IntN n) Source #

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymRotate ArithException (WordN n) m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate

Methods

safeSymRotateL :: WordN n -> WordN n -> m (WordN n) Source #

safeSymRotateR :: WordN n -> WordN n -> m (WordN n) Source #

(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeSymRotate ArithException (SymIntN n) m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymRotate ArithException (SymWordN n) m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymShift ArithException (IntN n) m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymShift

Methods

safeSymShiftL :: IntN n -> IntN n -> m (IntN n) Source #

safeSymShiftR :: IntN n -> IntN n -> m (IntN n) Source #

safeSymStrictShiftL :: IntN n -> IntN n -> m (IntN n) Source #

safeSymStrictShiftR :: IntN n -> IntN n -> m (IntN n) Source #

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymShift ArithException (WordN n) m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymShift

Methods

safeSymShiftL :: WordN n -> WordN n -> m (WordN n) Source #

safeSymShiftR :: WordN n -> WordN n -> m (WordN n) Source #

safeSymStrictShiftL :: WordN n -> WordN n -> m (WordN n) Source #

safeSymStrictShiftR :: WordN n -> WordN n -> m (WordN n) Source #

(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeSymShift ArithException (SymIntN n) m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymShift

(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeSymShift ArithException (SymWordN n) m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeSymShift

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeDiv ArithException (IntN n) m Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv

Methods

safeDiv :: IntN n -> IntN n -> m (IntN n) Source #

safeMod :: IntN n -> IntN n -> m (IntN n) Source #

safeDivMod :: IntN n -> IntN n -> m (IntN n, IntN n) Source #

safeQuot :: IntN n -> IntN n -> m (IntN n) Source #

safeRem :: IntN n -> IntN n -> m (IntN n) Source #

safeQuotRem :: IntN n -> IntN n -> m (IntN n, IntN n) Source #

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeDiv ArithException (WordN n) m Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv

Methods

safeDiv :: WordN n -> WordN n -> m (WordN n) Source #

safeMod :: WordN n -> WordN n -> m (WordN n) Source #

safeDivMod :: WordN n -> WordN n -> m (WordN n, WordN n) Source #

safeQuot :: WordN n -> WordN n -> m (WordN n) Source #

safeRem :: WordN n -> WordN n -> m (WordN n) Source #

safeQuotRem :: WordN n -> WordN n -> m (WordN n, WordN n) Source #

(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeDiv ArithException (SymIntN n) m Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv

Methods

safeDiv :: SymIntN n -> SymIntN n -> m (SymIntN n) Source #

safeMod :: SymIntN n -> SymIntN n -> m (SymIntN n) Source #

safeDivMod :: SymIntN n -> SymIntN n -> m (SymIntN n, SymIntN n) Source #

safeQuot :: SymIntN n -> SymIntN n -> m (SymIntN n) Source #

safeRem :: SymIntN n -> SymIntN n -> m (SymIntN n) Source #

safeQuotRem :: SymIntN n -> SymIntN n -> m (SymIntN n, SymIntN n) Source #

(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeDiv ArithException (SymWordN n) m Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeDiv 'S (Either SomeBVException ArithException) SomeSymIntN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeDiv 'S (Either SomeBVException ArithException) SomeSymWordN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeDiv mode (Either SomeBVException ArithException) SomeIntN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeDiv mode (Either SomeBVException ArithException) SomeWordN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeLinearArith 'S (Either SomeBVException ArithException) SomeSymIntN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeLinearArith 'S (Either SomeBVException ArithException) SomeSymWordN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeLinearArith mode (Either SomeBVException ArithException) SomeIntN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeLinearArith mode (Either SomeBVException ArithException) SomeWordN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeSymRotate 'S (Either SomeBVException ArithException) SomeSymIntN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeSymRotate 'S (Either SomeBVException ArithException) SomeSymWordN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymRotate mode (Either SomeBVException ArithException) SomeIntN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymRotate mode (Either SomeBVException ArithException) SomeWordN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeSymShift 'S (Either SomeBVException ArithException) SomeSymIntN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeSymShift 'S (Either SomeBVException ArithException) SomeSymWordN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymShift mode (Either SomeBVException ArithException) SomeIntN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymShift mode (Either SomeBVException ArithException) SomeWordN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

class (MonadError e m, TryMerge m, Mergeable a) => SafeLinearArith e a (m :: Type -> Type) where Source #

Safe division with monadic error handling in multi-path execution. These procedures throw an exception when overflow or underflow happens. The result should be able to handle errors with MonadError.

Methods

safeAdd :: a -> a -> m a Source #

Safe + with monadic error handling in multi-path execution. Overflows or underflows are treated as errors.

>>> safeAdd (ssym "a") (ssym "b") :: ExceptT ArithException Union SymInteger
ExceptT {Right (+ a b)}
>>> safeAdd (ssym "a") (ssym "b") :: ExceptT ArithException Union (SymIntN 4)
ExceptT {If (ite (< 0x0 a) (&& (< 0x0 b) (< (+ a b) 0x0)) (&& (< a 0x0) (&& (< b 0x0) (<= 0x0 (+ a b))))) (If (< 0x0 a) (Left arithmetic overflow) (Left arithmetic underflow)) (Right (+ a b))}

safeNeg :: a -> m a Source #

Safe negate with monadic error handling in multi-path execution. Overflows or underflows are treated as errors.

>>> safeNeg (ssym "a") :: ExceptT ArithException Union SymInteger
ExceptT {Right (- a)}
>>> safeNeg (ssym "a") :: ExceptT ArithException Union (SymIntN 4)
ExceptT {If (= a 0x8) (Left arithmetic overflow) (Right (- a))}

safeSub :: a -> a -> m a Source #

Safe - with monadic error handling in multi-path execution. Overflows or underflows are treated as errors.

>>> safeSub (ssym "a") (ssym "b") :: ExceptT ArithException Union SymInteger
ExceptT {Right (+ a (- b))}
>>> safeSub (ssym "a") (ssym "b") :: ExceptT ArithException Union (SymIntN 4)
ExceptT {If (ite (<= 0x0 a) (&& (< b 0x0) (< (+ a (- b)) 0x0)) (&& (< a 0x0) (&& (< 0x0 b) (< 0x0 (+ a (- b)))))) (If (<= 0x0 a) (Left arithmetic overflow) (Left arithmetic underflow)) (Right (+ a (- b)))}

Instances

Instances details
(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Int16 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Int32 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Int64 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Int8 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

Methods

safeAdd :: Int8 -> Int8 -> m Int8 Source #

safeNeg :: Int8 -> m Int8 Source #

safeSub :: Int8 -> Int8 -> m Int8 Source #

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Word16 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Word32 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Word64 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Word8 m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException SymInteger m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Integer m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Int m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

Methods

safeAdd :: Int -> Int -> m Int Source #

safeNeg :: Int -> m Int Source #

safeSub :: Int -> Int -> m Int Source #

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Word m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

Methods

safeAdd :: Word -> Word -> m Word Source #

safeNeg :: Word -> m Word Source #

safeSub :: Word -> Word -> m Word Source #

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (IntN n) m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

Methods

safeAdd :: IntN n -> IntN n -> m (IntN n) Source #

safeNeg :: IntN n -> m (IntN n) Source #

safeSub :: IntN n -> IntN n -> m (IntN n) Source #

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (WordN n) m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

Methods

safeAdd :: WordN n -> WordN n -> m (WordN n) Source #

safeNeg :: WordN n -> m (WordN n) Source #

safeSub :: WordN n -> WordN n -> m (WordN n) Source #

(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymIntN n) m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

Methods

safeAdd :: SymIntN n -> SymIntN n -> m (SymIntN n) Source #

safeNeg :: SymIntN n -> m (SymIntN n) Source #

safeSub :: SymIntN n -> SymIntN n -> m (SymIntN n) Source #

(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymWordN n) m Source # 
Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith

Methods

safeAdd :: SymWordN n -> SymWordN n -> m (SymWordN n) Source #

safeNeg :: SymWordN n -> m (SymWordN n) Source #

safeSub :: SymWordN n -> SymWordN n -> m (SymWordN n) Source #

(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeLinearArith e (bv n) (ExceptT e m), MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e, forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => SafeLinearArith (Either SomeBVException e) (SomeBV bv) m Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

safeAdd :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source #

safeNeg :: SomeBV bv -> m (SomeBV bv) Source #

safeSub :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source #