Copyright	(c) Sirui Lu 2021-2023
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	Trustworthy
Language	Haskell2010

Grisette.Core.Data.Class.SafeArith

Contents

Symbolic integer operations

Description

Synopsis

data ArithException
- = Overflow
- | Underflow
- | LossOfPrecision
- | DivideByZero
- | Denormal
- | RatioZeroDenominator
class (SOrd a, Num a, Mergeable a, Mergeable e) => SafeDivision e a | a -> e where
- safeDiv :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a
- safeMod :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a
- safeDivMod :: (MonadError e uf, MonadUnion uf) => a -> a -> uf (a, a)
- safeQuot :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a
- safeRem :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a
- safeQuotRem :: (MonadError e uf, MonadUnion uf) => a -> a -> uf (a, a)
- safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a
- safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a
- safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf (a, a)
- safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a
- safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a
- safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf (a, a)
class (SOrd a, Num a, Mergeable a, Mergeable e) => SafeLinearArith e a | a -> e where
- safeAdd :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a
- safeNeg :: (MonadError e uf, MonadUnion uf) => a -> uf a
- safeMinus :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a
- safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a
- safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> uf a
- safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a
class (Num a, SEq a, SOrd a, Solvable Integer a) => SymIntegerOp a

Symbolic integer operations

data ArithException #

Arithmetic exceptions.

Constructors

Overflow
Underflow
LossOfPrecision
DivideByZero
Denormal
RatioZeroDenominator	Since: base-4.6.0.0

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.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy ArithException Source #
TransformError ArithException AssertionError Source #
Instance details Defined in Grisette.Core.Control.Exception Methods transformError :: ArithException -> AssertionError Source #
SafeDivision ArithException Int16 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Int16 -> Int16 -> uf Int16 Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Int16 -> Int16 -> uf Int16 Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Int16 -> Int16 -> uf (Int16, Int16) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Int16 -> Int16 -> uf Int16 Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Int16 -> Int16 -> uf Int16 Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Int16 -> Int16 -> uf (Int16, Int16) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int16 -> Int16 -> uf Int16 Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int16 -> Int16 -> uf Int16 Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int16 -> Int16 -> uf (Int16, Int16) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int16 -> Int16 -> uf Int16 Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int16 -> Int16 -> uf Int16 Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int16 -> Int16 -> uf (Int16, Int16) Source #
SafeDivision ArithException Int32 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Int32 -> Int32 -> uf Int32 Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Int32 -> Int32 -> uf Int32 Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Int32 -> Int32 -> uf (Int32, Int32) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Int32 -> Int32 -> uf Int32 Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Int32 -> Int32 -> uf Int32 Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Int32 -> Int32 -> uf (Int32, Int32) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int32 -> Int32 -> uf Int32 Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int32 -> Int32 -> uf Int32 Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int32 -> Int32 -> uf (Int32, Int32) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int32 -> Int32 -> uf Int32 Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int32 -> Int32 -> uf Int32 Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int32 -> Int32 -> uf (Int32, Int32) Source #
SafeDivision ArithException Int64 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Int64 -> Int64 -> uf Int64 Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Int64 -> Int64 -> uf Int64 Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Int64 -> Int64 -> uf (Int64, Int64) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Int64 -> Int64 -> uf Int64 Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Int64 -> Int64 -> uf Int64 Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Int64 -> Int64 -> uf (Int64, Int64) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int64 -> Int64 -> uf Int64 Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int64 -> Int64 -> uf Int64 Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int64 -> Int64 -> uf (Int64, Int64) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int64 -> Int64 -> uf Int64 Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int64 -> Int64 -> uf Int64 Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int64 -> Int64 -> uf (Int64, Int64) Source #
SafeDivision ArithException Int8 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Int8 -> Int8 -> uf Int8 Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Int8 -> Int8 -> uf Int8 Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Int8 -> Int8 -> uf (Int8, Int8) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Int8 -> Int8 -> uf Int8 Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Int8 -> Int8 -> uf Int8 Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Int8 -> Int8 -> uf (Int8, Int8) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int8 -> Int8 -> uf Int8 Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int8 -> Int8 -> uf Int8 Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int8 -> Int8 -> uf (Int8, Int8) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int8 -> Int8 -> uf Int8 Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int8 -> Int8 -> uf Int8 Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int8 -> Int8 -> uf (Int8, Int8) Source #
SafeDivision ArithException Word16 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Word16 -> Word16 -> uf Word16 Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Word16 -> Word16 -> uf Word16 Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Word16 -> Word16 -> uf (Word16, Word16) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Word16 -> Word16 -> uf Word16 Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Word16 -> Word16 -> uf Word16 Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Word16 -> Word16 -> uf (Word16, Word16) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word16 -> Word16 -> uf Word16 Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word16 -> Word16 -> uf Word16 Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word16 -> Word16 -> uf (Word16, Word16) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word16 -> Word16 -> uf Word16 Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word16 -> Word16 -> uf Word16 Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word16 -> Word16 -> uf (Word16, Word16) Source #
SafeDivision ArithException Word32 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Word32 -> Word32 -> uf Word32 Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Word32 -> Word32 -> uf Word32 Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Word32 -> Word32 -> uf (Word32, Word32) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Word32 -> Word32 -> uf Word32 Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Word32 -> Word32 -> uf Word32 Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Word32 -> Word32 -> uf (Word32, Word32) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word32 -> Word32 -> uf Word32 Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word32 -> Word32 -> uf Word32 Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word32 -> Word32 -> uf (Word32, Word32) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word32 -> Word32 -> uf Word32 Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word32 -> Word32 -> uf Word32 Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word32 -> Word32 -> uf (Word32, Word32) Source #
SafeDivision ArithException Word64 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Word64 -> Word64 -> uf Word64 Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Word64 -> Word64 -> uf Word64 Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Word64 -> Word64 -> uf (Word64, Word64) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Word64 -> Word64 -> uf Word64 Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Word64 -> Word64 -> uf Word64 Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Word64 -> Word64 -> uf (Word64, Word64) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word64 -> Word64 -> uf Word64 Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word64 -> Word64 -> uf Word64 Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word64 -> Word64 -> uf (Word64, Word64) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word64 -> Word64 -> uf Word64 Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word64 -> Word64 -> uf Word64 Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word64 -> Word64 -> uf (Word64, Word64) Source #
SafeDivision ArithException Word8 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Word8 -> Word8 -> uf Word8 Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Word8 -> Word8 -> uf Word8 Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Word8 -> Word8 -> uf (Word8, Word8) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Word8 -> Word8 -> uf Word8 Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Word8 -> Word8 -> uf Word8 Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Word8 -> Word8 -> uf (Word8, Word8) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word8 -> Word8 -> uf Word8 Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word8 -> Word8 -> uf Word8 Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word8 -> Word8 -> uf (Word8, Word8) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word8 -> Word8 -> uf Word8 Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word8 -> Word8 -> uf Word8 Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word8 -> Word8 -> uf (Word8, Word8) Source #
SafeDivision ArithException SymInteger Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf SymInteger Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf SymInteger Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf (SymInteger, SymInteger) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf SymInteger Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf SymInteger Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf (SymInteger, SymInteger) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf (SymInteger, SymInteger) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf (SymInteger, SymInteger) Source #
SafeDivision ArithException Integer Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Integer -> Integer -> uf Integer Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Integer -> Integer -> uf Integer Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Integer -> Integer -> uf (Integer, Integer) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Integer -> Integer -> uf Integer Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Integer -> Integer -> uf Integer Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Integer -> Integer -> uf (Integer, Integer) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Integer -> Integer -> uf Integer Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Integer -> Integer -> uf Integer Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Integer -> Integer -> uf (Integer, Integer) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Integer -> Integer -> uf Integer Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Integer -> Integer -> uf Integer Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Integer -> Integer -> uf (Integer, Integer) Source #
SafeDivision ArithException Int Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf (Int, Int) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf (Int, Int) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf (Int, Int) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf (Int, Int) Source #
SafeDivision ArithException Word Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Word -> Word -> uf Word Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Word -> Word -> uf Word Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Word -> Word -> uf (Word, Word) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Word -> Word -> uf Word Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Word -> Word -> uf Word Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Word -> Word -> uf (Word, Word) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word -> Word -> uf Word Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word -> Word -> uf Word Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word -> Word -> uf (Word, Word) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word -> Word -> uf Word Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word -> Word -> uf Word Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word -> Word -> uf (Word, Word) Source #
SafeLinearArith ArithException Int16 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Int16 -> Int16 -> uf Int16 Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Int16 -> uf Int16 Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Int16 -> Int16 -> uf Int16 Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int16 -> Int16 -> uf Int16 Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int16 -> uf Int16 Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int16 -> Int16 -> uf Int16 Source #
SafeLinearArith ArithException Int32 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Int32 -> Int32 -> uf Int32 Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Int32 -> uf Int32 Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Int32 -> Int32 -> uf Int32 Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int32 -> Int32 -> uf Int32 Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int32 -> uf Int32 Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int32 -> Int32 -> uf Int32 Source #
SafeLinearArith ArithException Int64 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Int64 -> Int64 -> uf Int64 Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Int64 -> uf Int64 Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Int64 -> Int64 -> uf Int64 Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int64 -> Int64 -> uf Int64 Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int64 -> uf Int64 Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int64 -> Int64 -> uf Int64 Source #
SafeLinearArith ArithException Int8 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Int8 -> Int8 -> uf Int8 Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Int8 -> uf Int8 Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Int8 -> Int8 -> uf Int8 Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int8 -> Int8 -> uf Int8 Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int8 -> uf Int8 Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int8 -> Int8 -> uf Int8 Source #
SafeLinearArith ArithException Word16 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Word16 -> Word16 -> uf Word16 Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Word16 -> uf Word16 Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Word16 -> Word16 -> uf Word16 Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word16 -> Word16 -> uf Word16 Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word16 -> uf Word16 Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word16 -> Word16 -> uf Word16 Source #
SafeLinearArith ArithException Word32 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Word32 -> Word32 -> uf Word32 Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Word32 -> uf Word32 Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Word32 -> Word32 -> uf Word32 Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word32 -> Word32 -> uf Word32 Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word32 -> uf Word32 Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word32 -> Word32 -> uf Word32 Source #
SafeLinearArith ArithException Word64 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Word64 -> Word64 -> uf Word64 Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Word64 -> uf Word64 Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Word64 -> Word64 -> uf Word64 Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word64 -> Word64 -> uf Word64 Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word64 -> uf Word64 Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word64 -> Word64 -> uf Word64 Source #
SafeLinearArith ArithException Word8 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Word8 -> Word8 -> uf Word8 Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Word8 -> uf Word8 Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Word8 -> Word8 -> uf Word8 Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word8 -> Word8 -> uf Word8 Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word8 -> uf Word8 Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word8 -> Word8 -> uf Word8 Source #
SafeLinearArith ArithException SymInteger Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf SymInteger Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> uf SymInteger Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf SymInteger Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> uf SymInteger Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger Source #
SafeLinearArith ArithException Integer Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Integer -> Integer -> uf Integer Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Integer -> uf Integer Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Integer -> Integer -> uf Integer Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Integer -> Integer -> uf Integer Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Integer -> uf Integer Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Integer -> Integer -> uf Integer Source #
SafeLinearArith ArithException Int Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Int -> uf Int Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> uf Int Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source #
SafeLinearArith ArithException Word Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Word -> Word -> uf Word Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Word -> uf Word Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Word -> Word -> uf Word Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word -> Word -> uf Word Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word -> uf Word Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word -> Word -> uf Word Source #
(KnownNat n, 1 <= n) => SafeDivision ArithException (IntN n) Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n, IntN n) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n, IntN n) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n, IntN n) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n, IntN n) Source #
(KnownNat n, 1 <= n) => SafeDivision ArithException (WordN n) Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n, WordN n) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n, WordN n) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n, WordN n) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n, WordN n) Source #
(KnownNat n, 1 <= n) => SafeDivision ArithException (SymIntN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n, SymIntN n) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n, SymIntN n) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n, SymIntN n) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n, SymIntN n) Source #
(KnownNat n, 1 <= n) => SafeDivision ArithException (SymWordN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n, SymWordN n) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n, SymWordN n) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n, SymWordN n) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n, SymWordN n) Source #
(KnownNat n, 1 <= n) => SafeLinearArith ArithException (IntN n) Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> uf (IntN n) Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> uf (IntN n) Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source #
(KnownNat n, 1 <= n) => SafeLinearArith ArithException (WordN n) Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> uf (WordN n) Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> uf (WordN n) Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source #
(KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymIntN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> uf (SymIntN n) Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> uf (SymIntN n) Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source #
(KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymWordN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> uf (SymWordN n) Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> uf (SymWordN n) Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n) Source #
SafeDivision (Either BitwidthMismatch ArithException) SomeIntN Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeDivMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source # safeQuot :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeQuotRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source #
SafeDivision (Either BitwidthMismatch ArithException) SomeWordN Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeDivMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source # safeQuot :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeQuotRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source #
SafeLinearArith (Either BitwidthMismatch ArithException) SomeIntN Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeNeg :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> uf SomeIntN Source # safeMinus :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> uf SomeIntN Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source #
SafeLinearArith (Either BitwidthMismatch ArithException) SomeWordN Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeNeg :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> uf SomeWordN Source # safeMinus :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> uf SomeWordN Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source #

class (SOrd a, Num a, Mergeable a, Mergeable e) => SafeDivision e a | a -> e where Source #

Safe division with monadic error handling in multi-path execution. These procedures throw an exception when the divisor is zero. The result should be able to handle errors with MonadError.

Minimal complete definition

(safeDivMod | safeDiv, safeMod), (safeDivMod' | safeDiv', safeMod')

Methods

safeDiv :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a Source #

Safe signed div with monadic error handling in multi-path execution.

>>> safeDiv (ssym "a") (ssym "b") :: ExceptT ArithException UnionM SymInteger
ExceptT {If (= b 0) (Left divide by zero) (Right (div a b))}

safeMod :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a Source #

Safe signed mod with monadic error handling in multi-path execution.

>>> safeMod (ssym "a") (ssym "b") :: ExceptT ArithException UnionM SymInteger
ExceptT {If (= b 0) (Left divide by zero) (Right (mod a b))}

safeDivMod :: (MonadError e uf, MonadUnion uf) => a -> a -> uf (a, a) Source #

Safe signed divMod with monadic error handling in multi-path execution.

>>> safeDivMod (ssym "a") (ssym "b") :: ExceptT ArithException UnionM (SymInteger, SymInteger)
ExceptT {If (= b 0) (Left divide by zero) (Right ((div a b),(mod a b)))}

safeQuot :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a Source #

Safe signed quot with monadic error handling in multi-path execution.

safeRem :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a Source #

Safe signed rem with monadic error handling in multi-path execution.

safeQuotRem :: (MonadError e uf, MonadUnion uf) => a -> a -> uf (a, a) Source #

Safe signed quotRem with monadic error handling in multi-path execution.

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a Source #

Safe signed div with monadic error handling in multi-path execution. The error is transformed.

>>> safeDiv' (const ()) (ssym "a") (ssym "b") :: ExceptT () UnionM SymInteger
ExceptT {If (= b 0) (Left ()) (Right (div a b))}

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a Source #

Safe signed mod with monadic error handling in multi-path execution. The error is transformed.

>>> safeMod' (const ()) (ssym "a") (ssym "b") :: ExceptT () UnionM SymInteger
ExceptT {If (= b 0) (Left ()) (Right (mod a b))}

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf (a, a) Source #

Safe signed divMod with monadic error handling in multi-path execution. The error is transformed.

>>> safeDivMod' (const ()) (ssym "a") (ssym "b") :: ExceptT () UnionM (SymInteger, SymInteger)
ExceptT {If (= b 0) (Left ()) (Right ((div a b),(mod a b)))}

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a Source #

Safe signed quot with monadic error handling in multi-path execution. The error is transformed.

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a Source #

Safe signed rem with monadic error handling in multi-path execution. The error is transformed.

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf (a, a) Source #

Safe signed quotRem with monadic error handling in multi-path execution. The error is transformed.

Instances

Instances details

SafeDivision ArithException Int16 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Int16 -> Int16 -> uf Int16 Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Int16 -> Int16 -> uf Int16 Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Int16 -> Int16 -> uf (Int16, Int16) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Int16 -> Int16 -> uf Int16 Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Int16 -> Int16 -> uf Int16 Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Int16 -> Int16 -> uf (Int16, Int16) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int16 -> Int16 -> uf Int16 Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int16 -> Int16 -> uf Int16 Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int16 -> Int16 -> uf (Int16, Int16) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int16 -> Int16 -> uf Int16 Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int16 -> Int16 -> uf Int16 Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int16 -> Int16 -> uf (Int16, Int16) Source #
SafeDivision ArithException Int32 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Int32 -> Int32 -> uf Int32 Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Int32 -> Int32 -> uf Int32 Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Int32 -> Int32 -> uf (Int32, Int32) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Int32 -> Int32 -> uf Int32 Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Int32 -> Int32 -> uf Int32 Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Int32 -> Int32 -> uf (Int32, Int32) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int32 -> Int32 -> uf Int32 Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int32 -> Int32 -> uf Int32 Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int32 -> Int32 -> uf (Int32, Int32) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int32 -> Int32 -> uf Int32 Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int32 -> Int32 -> uf Int32 Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int32 -> Int32 -> uf (Int32, Int32) Source #
SafeDivision ArithException Int64 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Int64 -> Int64 -> uf Int64 Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Int64 -> Int64 -> uf Int64 Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Int64 -> Int64 -> uf (Int64, Int64) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Int64 -> Int64 -> uf Int64 Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Int64 -> Int64 -> uf Int64 Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Int64 -> Int64 -> uf (Int64, Int64) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int64 -> Int64 -> uf Int64 Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int64 -> Int64 -> uf Int64 Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int64 -> Int64 -> uf (Int64, Int64) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int64 -> Int64 -> uf Int64 Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int64 -> Int64 -> uf Int64 Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int64 -> Int64 -> uf (Int64, Int64) Source #
SafeDivision ArithException Int8 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Int8 -> Int8 -> uf Int8 Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Int8 -> Int8 -> uf Int8 Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Int8 -> Int8 -> uf (Int8, Int8) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Int8 -> Int8 -> uf Int8 Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Int8 -> Int8 -> uf Int8 Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Int8 -> Int8 -> uf (Int8, Int8) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int8 -> Int8 -> uf Int8 Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int8 -> Int8 -> uf Int8 Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int8 -> Int8 -> uf (Int8, Int8) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int8 -> Int8 -> uf Int8 Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int8 -> Int8 -> uf Int8 Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int8 -> Int8 -> uf (Int8, Int8) Source #
SafeDivision ArithException Word16 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Word16 -> Word16 -> uf Word16 Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Word16 -> Word16 -> uf Word16 Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Word16 -> Word16 -> uf (Word16, Word16) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Word16 -> Word16 -> uf Word16 Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Word16 -> Word16 -> uf Word16 Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Word16 -> Word16 -> uf (Word16, Word16) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word16 -> Word16 -> uf Word16 Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word16 -> Word16 -> uf Word16 Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word16 -> Word16 -> uf (Word16, Word16) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word16 -> Word16 -> uf Word16 Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word16 -> Word16 -> uf Word16 Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word16 -> Word16 -> uf (Word16, Word16) Source #
SafeDivision ArithException Word32 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Word32 -> Word32 -> uf Word32 Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Word32 -> Word32 -> uf Word32 Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Word32 -> Word32 -> uf (Word32, Word32) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Word32 -> Word32 -> uf Word32 Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Word32 -> Word32 -> uf Word32 Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Word32 -> Word32 -> uf (Word32, Word32) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word32 -> Word32 -> uf Word32 Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word32 -> Word32 -> uf Word32 Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word32 -> Word32 -> uf (Word32, Word32) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word32 -> Word32 -> uf Word32 Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word32 -> Word32 -> uf Word32 Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word32 -> Word32 -> uf (Word32, Word32) Source #
SafeDivision ArithException Word64 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Word64 -> Word64 -> uf Word64 Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Word64 -> Word64 -> uf Word64 Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Word64 -> Word64 -> uf (Word64, Word64) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Word64 -> Word64 -> uf Word64 Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Word64 -> Word64 -> uf Word64 Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Word64 -> Word64 -> uf (Word64, Word64) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word64 -> Word64 -> uf Word64 Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word64 -> Word64 -> uf Word64 Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word64 -> Word64 -> uf (Word64, Word64) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word64 -> Word64 -> uf Word64 Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word64 -> Word64 -> uf Word64 Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word64 -> Word64 -> uf (Word64, Word64) Source #
SafeDivision ArithException Word8 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Word8 -> Word8 -> uf Word8 Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Word8 -> Word8 -> uf Word8 Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Word8 -> Word8 -> uf (Word8, Word8) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Word8 -> Word8 -> uf Word8 Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Word8 -> Word8 -> uf Word8 Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Word8 -> Word8 -> uf (Word8, Word8) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word8 -> Word8 -> uf Word8 Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word8 -> Word8 -> uf Word8 Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word8 -> Word8 -> uf (Word8, Word8) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word8 -> Word8 -> uf Word8 Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word8 -> Word8 -> uf Word8 Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word8 -> Word8 -> uf (Word8, Word8) Source #
SafeDivision ArithException SymInteger Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf SymInteger Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf SymInteger Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf (SymInteger, SymInteger) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf SymInteger Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf SymInteger Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf (SymInteger, SymInteger) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf (SymInteger, SymInteger) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf (SymInteger, SymInteger) Source #
SafeDivision ArithException Integer Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Integer -> Integer -> uf Integer Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Integer -> Integer -> uf Integer Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Integer -> Integer -> uf (Integer, Integer) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Integer -> Integer -> uf Integer Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Integer -> Integer -> uf Integer Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Integer -> Integer -> uf (Integer, Integer) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Integer -> Integer -> uf Integer Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Integer -> Integer -> uf Integer Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Integer -> Integer -> uf (Integer, Integer) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Integer -> Integer -> uf Integer Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Integer -> Integer -> uf Integer Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Integer -> Integer -> uf (Integer, Integer) Source #
SafeDivision ArithException Int Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf (Int, Int) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf (Int, Int) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf (Int, Int) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf (Int, Int) Source #
SafeDivision ArithException Word Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Word -> Word -> uf Word Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => Word -> Word -> uf Word Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Word -> Word -> uf (Word, Word) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Word -> Word -> uf Word Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => Word -> Word -> uf Word Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Word -> Word -> uf (Word, Word) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word -> Word -> uf Word Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word -> Word -> uf Word Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word -> Word -> uf (Word, Word) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word -> Word -> uf Word Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word -> Word -> uf Word Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word -> Word -> uf (Word, Word) Source #
(KnownNat n, 1 <= n) => SafeDivision ArithException (IntN n) Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n, IntN n) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n, IntN n) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n, IntN n) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n, IntN n) Source #
(KnownNat n, 1 <= n) => SafeDivision ArithException (WordN n) Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n, WordN n) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n, WordN n) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n, WordN n) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n, WordN n) Source #
(KnownNat n, 1 <= n) => SafeDivision ArithException (SymIntN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n, SymIntN n) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n, SymIntN n) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n, SymIntN n) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n, SymIntN n) Source #
(KnownNat n, 1 <= n) => SafeDivision ArithException (SymWordN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n, SymWordN n) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n, SymWordN n) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n, SymWordN n) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n, SymWordN n) Source #
SafeDivision (Either BitwidthMismatch ArithException) SomeIntN Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeDivMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source # safeQuot :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeQuotRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source #
SafeDivision (Either BitwidthMismatch ArithException) SomeWordN Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeDivMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source # safeQuot :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeQuotRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source #

class (SOrd a, Num a, Mergeable a, Mergeable e) => SafeLinearArith e a | a -> e 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 :: (MonadError e uf, MonadUnion uf) => a -> a -> uf 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 :: (MonadError e uf, MonadUnion uf) => a -> uf 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))}

safeMinus :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a Source #

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

>>> safeMinus (ssym "a") (ssym "b") :: ExceptT ArithException UnionM SymInteger
ExceptT {Right (+ a (- b))}
>>> safeMinus (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)))}

safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a Source #

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

safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> uf a Source #

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

safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a Source #

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

Instances

Instances details

SafeLinearArith ArithException Int16 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Int16 -> Int16 -> uf Int16 Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Int16 -> uf Int16 Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Int16 -> Int16 -> uf Int16 Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int16 -> Int16 -> uf Int16 Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int16 -> uf Int16 Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int16 -> Int16 -> uf Int16 Source #
SafeLinearArith ArithException Int32 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Int32 -> Int32 -> uf Int32 Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Int32 -> uf Int32 Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Int32 -> Int32 -> uf Int32 Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int32 -> Int32 -> uf Int32 Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int32 -> uf Int32 Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int32 -> Int32 -> uf Int32 Source #
SafeLinearArith ArithException Int64 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Int64 -> Int64 -> uf Int64 Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Int64 -> uf Int64 Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Int64 -> Int64 -> uf Int64 Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int64 -> Int64 -> uf Int64 Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int64 -> uf Int64 Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int64 -> Int64 -> uf Int64 Source #
SafeLinearArith ArithException Int8 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Int8 -> Int8 -> uf Int8 Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Int8 -> uf Int8 Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Int8 -> Int8 -> uf Int8 Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int8 -> Int8 -> uf Int8 Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int8 -> uf Int8 Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int8 -> Int8 -> uf Int8 Source #
SafeLinearArith ArithException Word16 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Word16 -> Word16 -> uf Word16 Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Word16 -> uf Word16 Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Word16 -> Word16 -> uf Word16 Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word16 -> Word16 -> uf Word16 Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word16 -> uf Word16 Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word16 -> Word16 -> uf Word16 Source #
SafeLinearArith ArithException Word32 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Word32 -> Word32 -> uf Word32 Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Word32 -> uf Word32 Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Word32 -> Word32 -> uf Word32 Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word32 -> Word32 -> uf Word32 Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word32 -> uf Word32 Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word32 -> Word32 -> uf Word32 Source #
SafeLinearArith ArithException Word64 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Word64 -> Word64 -> uf Word64 Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Word64 -> uf Word64 Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Word64 -> Word64 -> uf Word64 Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word64 -> Word64 -> uf Word64 Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word64 -> uf Word64 Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word64 -> Word64 -> uf Word64 Source #
SafeLinearArith ArithException Word8 Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Word8 -> Word8 -> uf Word8 Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Word8 -> uf Word8 Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Word8 -> Word8 -> uf Word8 Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word8 -> Word8 -> uf Word8 Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word8 -> uf Word8 Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word8 -> Word8 -> uf Word8 Source #
SafeLinearArith ArithException SymInteger Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf SymInteger Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> uf SymInteger Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf SymInteger Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> uf SymInteger Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger Source #
SafeLinearArith ArithException Integer Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Integer -> Integer -> uf Integer Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Integer -> uf Integer Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Integer -> Integer -> uf Integer Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Integer -> Integer -> uf Integer Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Integer -> uf Integer Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Integer -> Integer -> uf Integer Source #
SafeLinearArith ArithException Int Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Int -> uf Int Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> uf Int Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source #
SafeLinearArith ArithException Word Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Word -> Word -> uf Word Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Word -> uf Word Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Word -> Word -> uf Word Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word -> Word -> uf Word Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word -> uf Word Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Word -> Word -> uf Word Source #
(KnownNat n, 1 <= n) => SafeLinearArith ArithException (IntN n) Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> uf (IntN n) Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> uf (IntN n) Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source #
(KnownNat n, 1 <= n) => SafeLinearArith ArithException (WordN n) Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> uf (WordN n) Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> uf (WordN n) Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source #
(KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymIntN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> uf (SymIntN n) Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> uf (SymIntN n) Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source #
(KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymWordN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> uf (SymWordN n) Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n) Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> uf (SymWordN n) Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n) Source #
SafeLinearArith (Either BitwidthMismatch ArithException) SomeIntN Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeNeg :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> uf SomeIntN Source # safeMinus :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> uf SomeIntN Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source #
SafeLinearArith (Either BitwidthMismatch ArithException) SomeWordN Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeNeg :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> uf SomeWordN Source # safeMinus :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> uf SomeWordN Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source #

class (Num a, SEq a, SOrd a, Solvable Integer a) => SymIntegerOp a Source #

Aggregation for the operations on symbolic integer types

Instances

Instances details

SymIntegerOp SymInteger Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim