grisette-0.5.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.

Constructors

Overflow 
Underflow 
DivideByZero 

Instances

Instances details
Exception ArithException

Since: base-4.0.0.0

Instance details

Defined in GHC.Exception.Type

Methods

toException :: ArithException -> SomeException #

fromException :: SomeException -> Maybe ArithException #

displayException :: ArithException -> String #

Show ArithException

Since: base-4.0.0.0

Instance details

Defined in GHC.Exception.Type

Methods

showsPrec :: Int -> ArithException -> ShowS #

show :: ArithException -> String #

showList :: [ArithException] -> ShowS #

Eq ArithException

Since: base-3.0

Instance details

Defined in GHC.Exception.Type

Methods

(==) :: ArithException -> ArithException -> Bool #

(/=) :: ArithException -> ArithException -> Bool #

Ord ArithException

Since: base-3.0

Instance details

Defined in GHC.Exception.Type

Methods

compare :: ArithException -> ArithException -> Ordering #

(<) :: ArithException -> ArithException -> Bool #

(<=) :: ArithException -> ArithException -> Bool #

(>) :: ArithException -> ArithException -> Bool #

(>=) :: ArithException -> ArithException -> Bool #

max :: ArithException -> ArithException -> ArithException #

min :: ArithException -> ArithException -> ArithException #

Mergeable ArithException Source # 
Instance details

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

Methods

rootStrategy :: MergingStrategy ArithException Source #

TransformError ArithException AssertionError Source # 
Instance details

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

Methods

transformError :: ArithException -> AssertionError Source #

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

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

Methods

safeDiv :: Int16 -> Int16 -> m Int16 Source #

safeMod :: Int16 -> Int16 -> m Int16 Source #

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

safeQuot :: Int16 -> Int16 -> m Int16 Source #

safeRem :: Int16 -> Int16 -> m Int16 Source #

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

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

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

Methods

safeDiv :: Int32 -> Int32 -> m Int32 Source #

safeMod :: Int32 -> Int32 -> m Int32 Source #

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

safeQuot :: Int32 -> Int32 -> m Int32 Source #

safeRem :: Int32 -> Int32 -> m Int32 Source #

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

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

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

Methods

safeDiv :: Int64 -> Int64 -> m Int64 Source #

safeMod :: Int64 -> Int64 -> m Int64 Source #

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

safeQuot :: Int64 -> Int64 -> m Int64 Source #

safeRem :: Int64 -> Int64 -> m Int64 Source #

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

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

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

Methods

safeDiv :: Int8 -> Int8 -> m Int8 Source #

safeMod :: Int8 -> Int8 -> m Int8 Source #

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

safeQuot :: Int8 -> Int8 -> m Int8 Source #

safeRem :: Int8 -> Int8 -> m Int8 Source #

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

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

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

Methods

safeDiv :: Word16 -> Word16 -> m Word16 Source #

safeMod :: Word16 -> Word16 -> m Word16 Source #

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

safeQuot :: Word16 -> Word16 -> m Word16 Source #

safeRem :: Word16 -> Word16 -> m Word16 Source #

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

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

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

Methods

safeDiv :: Word32 -> Word32 -> m Word32 Source #

safeMod :: Word32 -> Word32 -> m Word32 Source #

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

safeQuot :: Word32 -> Word32 -> m Word32 Source #

safeRem :: Word32 -> Word32 -> m Word32 Source #

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

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

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

Methods

safeDiv :: Word64 -> Word64 -> m Word64 Source #

safeMod :: Word64 -> Word64 -> m Word64 Source #

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

safeQuot :: Word64 -> Word64 -> m Word64 Source #

safeRem :: Word64 -> Word64 -> m Word64 Source #

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

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

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

Methods

safeDiv :: Word8 -> Word8 -> m Word8 Source #

safeMod :: Word8 -> Word8 -> m Word8 Source #

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

safeQuot :: Word8 -> Word8 -> m Word8 Source #

safeRem :: Word8 -> Word8 -> m Word8 Source #

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

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

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

Methods

safeDiv :: SymInteger -> SymInteger -> m SymInteger Source #

safeMod :: SymInteger -> SymInteger -> m SymInteger Source #

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

safeQuot :: SymInteger -> SymInteger -> m SymInteger Source #

safeRem :: SymInteger -> SymInteger -> m SymInteger Source #

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

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

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

Methods

safeDiv :: Integer -> Integer -> m Integer Source #

safeMod :: Integer -> Integer -> m Integer Source #

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

safeQuot :: Integer -> Integer -> m Integer Source #

safeRem :: Integer -> Integer -> m Integer Source #

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

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

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

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) => SafeDivision ArithException Word m Source # 
Instance details

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

Methods

safeDiv :: Word -> Word -> m Word Source #

safeMod :: Word -> Word -> m Word Source #

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

safeQuot :: Word -> Word -> m Word Source #

safeRem :: Word -> Word -> m Word Source #

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

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

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

Methods

safeAdd :: Int16 -> Int16 -> m Int16 Source #

safeNeg :: Int16 -> m Int16 Source #

safeSub :: Int16 -> Int16 -> m Int16 Source #

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

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

Methods

safeAdd :: Int32 -> Int32 -> m Int32 Source #

safeNeg :: Int32 -> m Int32 Source #

safeSub :: Int32 -> Int32 -> m Int32 Source #

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

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

Methods

safeAdd :: Int64 -> Int64 -> m Int64 Source #

safeNeg :: Int64 -> m Int64 Source #

safeSub :: Int64 -> Int64 -> m Int64 Source #

(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

Methods

safeAdd :: Word16 -> Word16 -> m Word16 Source #

safeNeg :: Word16 -> m Word16 Source #

safeSub :: Word16 -> Word16 -> m Word16 Source #

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

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

Methods

safeAdd :: Word32 -> Word32 -> m Word32 Source #

safeNeg :: Word32 -> m Word32 Source #

safeSub :: Word32 -> Word32 -> m Word32 Source #

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

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

Methods

safeAdd :: Word64 -> Word64 -> m Word64 Source #

safeNeg :: Word64 -> m Word64 Source #

safeSub :: Word64 -> Word64 -> m Word64 Source #

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

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

Methods

safeAdd :: Word8 -> Word8 -> m Word8 Source #

safeNeg :: Word8 -> m Word8 Source #

safeSub :: Word8 -> Word8 -> m Word8 Source #

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

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

Methods

safeAdd :: SymInteger -> SymInteger -> m SymInteger Source #

safeNeg :: SymInteger -> m SymInteger Source #

safeSub :: SymInteger -> SymInteger -> m SymInteger Source #

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

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

Methods

safeAdd :: Integer -> Integer -> m Integer Source #

safeNeg :: Integer -> m Integer Source #

safeSub :: Integer -> Integer -> m Integer Source #

(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) => SafeSymRotate ArithException Int16 m Source # 
Instance details

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

Methods

safeSymRotateL :: Int16 -> Int16 -> m Int16 Source #

safeSymRotateR :: Int16 -> Int16 -> m Int16 Source #

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

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

Methods

safeSymRotateL :: Int32 -> Int32 -> m Int32 Source #

safeSymRotateR :: Int32 -> Int32 -> m Int32 Source #

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

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

Methods

safeSymRotateL :: Int64 -> Int64 -> m Int64 Source #

safeSymRotateR :: Int64 -> Int64 -> m Int64 Source #

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

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

Methods

safeSymRotateL :: Int8 -> Int8 -> m Int8 Source #

safeSymRotateR :: Int8 -> Int8 -> m Int8 Source #

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

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

Methods

safeSymRotateL :: Word16 -> Word16 -> m Word16 Source #

safeSymRotateR :: Word16 -> Word16 -> m Word16 Source #

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

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

Methods

safeSymRotateL :: Word32 -> Word32 -> m Word32 Source #

safeSymRotateR :: Word32 -> Word32 -> m Word32 Source #

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

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

Methods

safeSymRotateL :: Word64 -> Word64 -> m Word64 Source #

safeSymRotateR :: Word64 -> Word64 -> m Word64 Source #

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

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

Methods

safeSymRotateL :: Word8 -> Word8 -> m Word8 Source #

safeSymRotateR :: Word8 -> Word8 -> m Word8 Source #

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

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

Methods

safeSymRotateL :: Int -> Int -> m Int Source #

safeSymRotateR :: Int -> Int -> m Int Source #

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

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

Methods

safeSymRotateL :: Word -> Word -> m Word Source #

safeSymRotateR :: Word -> Word -> m Word Source #

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

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

Methods

safeSymShiftL :: Int16 -> Int16 -> m Int16 Source #

safeSymShiftR :: Int16 -> Int16 -> m Int16 Source #

safeSymStrictShiftL :: Int16 -> Int16 -> m Int16 Source #

safeSymStrictShiftR :: Int16 -> Int16 -> m Int16 Source #

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

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

Methods

safeSymShiftL :: Int32 -> Int32 -> m Int32 Source #

safeSymShiftR :: Int32 -> Int32 -> m Int32 Source #

safeSymStrictShiftL :: Int32 -> Int32 -> m Int32 Source #

safeSymStrictShiftR :: Int32 -> Int32 -> m Int32 Source #

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

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

Methods

safeSymShiftL :: Int64 -> Int64 -> m Int64 Source #

safeSymShiftR :: Int64 -> Int64 -> m Int64 Source #

safeSymStrictShiftL :: Int64 -> Int64 -> m Int64 Source #

safeSymStrictShiftR :: Int64 -> Int64 -> m Int64 Source #

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

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

Methods

safeSymShiftL :: Int8 -> Int8 -> m Int8 Source #

safeSymShiftR :: Int8 -> Int8 -> m Int8 Source #

safeSymStrictShiftL :: Int8 -> Int8 -> m Int8 Source #

safeSymStrictShiftR :: Int8 -> Int8 -> m Int8 Source #

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

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

Methods

safeSymShiftL :: Word16 -> Word16 -> m Word16 Source #

safeSymShiftR :: Word16 -> Word16 -> m Word16 Source #

safeSymStrictShiftL :: Word16 -> Word16 -> m Word16 Source #

safeSymStrictShiftR :: Word16 -> Word16 -> m Word16 Source #

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

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

Methods

safeSymShiftL :: Word32 -> Word32 -> m Word32 Source #

safeSymShiftR :: Word32 -> Word32 -> m Word32 Source #

safeSymStrictShiftL :: Word32 -> Word32 -> m Word32 Source #

safeSymStrictShiftR :: Word32 -> Word32 -> m Word32 Source #

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

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

Methods

safeSymShiftL :: Word64 -> Word64 -> m Word64 Source #

safeSymShiftR :: Word64 -> Word64 -> m Word64 Source #

safeSymStrictShiftL :: Word64 -> Word64 -> m Word64 Source #

safeSymStrictShiftR :: Word64 -> Word64 -> m Word64 Source #

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

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

Methods

safeSymShiftL :: Word8 -> Word8 -> m Word8 Source #

safeSymShiftR :: Word8 -> Word8 -> m Word8 Source #

safeSymStrictShiftL :: Word8 -> Word8 -> m Word8 Source #

safeSymStrictShiftR :: Word8 -> Word8 -> m Word8 Source #

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

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

Methods

safeSymShiftL :: Int -> Int -> m Int Source #

safeSymShiftR :: Int -> Int -> m Int Source #

safeSymStrictShiftL :: Int -> Int -> m Int Source #

safeSymStrictShiftR :: Int -> Int -> m Int Source #

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

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

Methods

safeSymShiftL :: Word -> Word -> m Word Source #

safeSymShiftR :: Word -> Word -> m Word Source #

safeSymStrictShiftL :: Word -> Word -> m Word Source #

safeSymStrictShiftR :: Word -> Word -> m Word Source #

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

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

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) => SafeDivision ArithException (WordN n) m Source # 
Instance details

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

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) => SafeDivision ArithException (SymIntN n) m Source # 
Instance details

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

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) => SafeDivision ArithException (SymWordN n) m Source # 
Instance details

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

Methods

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

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

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

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

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

safeQuotRem :: SymWordN n -> SymWordN n -> m (SymWordN n, SymWordN n) 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 #

(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

Methods

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

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

(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

Methods

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

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

(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

Methods

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

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

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

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

(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

Methods

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

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

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

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

class (MonadError e m, TryMerge m, Mergeable a) => SafeLinearArith e a m 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 UnionM SymInteger
ExceptT {Right (+ a b)}
>>> safeAdd (ssym "a") (ssym "b") :: ExceptT ArithException UnionM (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 UnionM SymInteger
ExceptT {Right (- a)}
>>> safeNeg (ssym "a") :: ExceptT ArithException UnionM (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 UnionM SymInteger
ExceptT {Right (+ a (- b))}
>>> safeSub (ssym "a") (ssym "b") :: ExceptT ArithException UnionM (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

Methods

safeAdd :: Int16 -> Int16 -> m Int16 Source #

safeNeg :: Int16 -> m Int16 Source #

safeSub :: Int16 -> Int16 -> m Int16 Source #

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

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

Methods

safeAdd :: Int32 -> Int32 -> m Int32 Source #

safeNeg :: Int32 -> m Int32 Source #

safeSub :: Int32 -> Int32 -> m Int32 Source #

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

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

Methods

safeAdd :: Int64 -> Int64 -> m Int64 Source #

safeNeg :: Int64 -> m Int64 Source #

safeSub :: Int64 -> Int64 -> m Int64 Source #

(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

Methods

safeAdd :: Word16 -> Word16 -> m Word16 Source #

safeNeg :: Word16 -> m Word16 Source #

safeSub :: Word16 -> Word16 -> m Word16 Source #

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

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

Methods

safeAdd :: Word32 -> Word32 -> m Word32 Source #

safeNeg :: Word32 -> m Word32 Source #

safeSub :: Word32 -> Word32 -> m Word32 Source #

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

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

Methods

safeAdd :: Word64 -> Word64 -> m Word64 Source #

safeNeg :: Word64 -> m Word64 Source #

safeSub :: Word64 -> Word64 -> m Word64 Source #

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

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

Methods

safeAdd :: Word8 -> Word8 -> m Word8 Source #

safeNeg :: Word8 -> m Word8 Source #

safeSub :: Word8 -> Word8 -> m Word8 Source #

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

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

Methods

safeAdd :: SymInteger -> SymInteger -> m SymInteger Source #

safeNeg :: SymInteger -> m SymInteger Source #

safeSub :: SymInteger -> SymInteger -> m SymInteger Source #

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

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

Methods

safeAdd :: Integer -> Integer -> m Integer Source #

safeNeg :: Integer -> m Integer Source #

safeSub :: Integer -> Integer -> m Integer Source #

(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 BitwidthMismatch e) m, TryMerge m, Mergeable e) => SafeLinearArith (Either BitwidthMismatch 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 #