Grisette.Core.Data.Class.Integer

Symbolic integer operations

data ArithException

Arithmetic exceptions.

Constructors

Overflow

Underflow

LossOfPrecision

DivideByZero

Denormal

RatioZeroDenominator

Since: base-4.6.0.0

Instances

Exception ArithException

Since: base-4.0.0.0

Defined in GHC.Exception.Type

Methods

toException :: ArithException -> SomeException

fromException :: SomeException -> Maybe ArithException

displayException :: ArithException -> String

Show ArithException

Since: base-4.0.0.0

Defined in GHC.Exception.Type

Methods

showsPrec :: Int -> ArithException -> ShowS

show :: ArithException -> String

showList :: [ArithException] -> ShowS

Eq ArithException

Since: base-3.0

Defined in GHC.Exception.Type

Methods

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

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

Ord ArithException

Since: base-3.0

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

TransformError ArithException AssertionError

Defined in Grisette.Core.Control.Exception

Methods

transformError :: ArithException -> AssertionError

class SignedDivMod a where

Safe signed div and mod with monadic error handling in multi-path execution. These procedures show throw DivideByZero exception when the divisor is zero. The result should be able to handle errors with MonadError, and the error type should be compatible with ArithException (see TransformError for more details).

Methods

divs :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a

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

>>> divs (ssym "a") (ssym "b") :: ExceptT AssertionError UnionM SymInteger
ExceptT {If (= b 0) (Left AssertionError) (Right (div a b))}

mods :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a

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

>>> mods (ssym "a") (ssym "b") :: ExceptT AssertionError UnionM SymInteger
ExceptT {If (= b 0) (Left AssertionError) (Right (mod a b))}

Instances

SignedDivMod (Sym Integer)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

divs :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => Sym Integer -> Sym Integer -> uf (Sym Integer)

mods :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => Sym Integer -> Sym Integer -> uf (Sym Integer)

class UnsignedDivMod a where

Safe unsigned div and mod with monadic error handling in multi-path execution. These procedures show throw DivideByZero exception when the divisor is zero. The result should be able to handle errors with MonadError, and the error type should be compatible with ArithException (see TransformError for more details).

Methods

udivs :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a

umods :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a

class SignedQuotRem a where

Safe signed quot and rem with monadic error handling in multi-path execution. These procedures show throw DivideByZero exception when the divisor is zero. The result should be able to handle errors with MonadError, and the error type should be compatible with ArithException (see TransformError for more details).

Methods

quots :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a

rems :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a

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

Aggregation for the operations on symbolic integer types

Instances

SymIntegerOp (Sym Integer)

Defined in Grisette.IR.SymPrim.Data.SymPrim