module Language.Hasmtlib.Internal.Expr.Num where

import Prelude hiding (div, mod, quotRem, rem, quot, divMod)
import Language.Hasmtlib.Internal.Expr
import Language.Hasmtlib.Integraled
import Language.Hasmtlib.Type.SMTSort
import Language.Hasmtlib.Iteable
import Language.Hasmtlib.Equatable
import Language.Hasmtlib.Orderable
import GHC.TypeNats

instance Num (Expr IntSort) where
   fromInteger :: Integer -> Expr 'IntSort
fromInteger = Value 'IntSort -> Expr 'IntSort
forall (t :: SMTSort). Value t -> Expr t
Constant (Value 'IntSort -> Expr 'IntSort)
-> (Integer -> Value 'IntSort) -> Integer -> Expr 'IntSort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Value 'IntSort
HaskellType 'IntSort -> Value 'IntSort
IntValue
   {-# INLINE fromInteger #-}
   (Constant (IntValue HaskellType 'IntSort
0)) + :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
+ Expr 'IntSort
y = Expr 'IntSort
y
   Expr 'IntSort
x + (Constant (IntValue HaskellType 'IntSort
0)) = Expr 'IntSort
x
   (Constant (IntValue HaskellType 'IntSort
x)) + (Constant (IntValue HaskellType 'IntSort
y)) = Value 'IntSort -> Expr 'IntSort
forall (t :: SMTSort). Value t -> Expr t
Constant (HaskellType 'IntSort -> Value 'IntSort
IntValue (Integer
HaskellType 'IntSort
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
HaskellType 'IntSort
y))
   Expr 'IntSort
x + Expr 'IntSort
y = Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall (t :: SMTSort).
Num (HaskellType t) =>
Expr t -> Expr t -> Expr t
Plus Expr 'IntSort
x Expr 'IntSort
y
   {-# INLINE (+) #-}
   Expr 'IntSort
x - :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
- (Constant (IntValue HaskellType 'IntSort
0)) = Expr 'IntSort
x
   (Constant (IntValue HaskellType 'IntSort
x)) - (Constant (IntValue HaskellType 'IntSort
y)) = Value 'IntSort -> Expr 'IntSort
forall (t :: SMTSort). Value t -> Expr t
Constant (HaskellType 'IntSort -> Value 'IntSort
IntValue (Integer
HaskellType 'IntSort
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
HaskellType 'IntSort
y))
   Expr 'IntSort
x - Expr 'IntSort
y = Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall (t :: SMTSort).
Num (HaskellType t) =>
Expr t -> Expr t -> Expr t
Plus Expr 'IntSort
x (Expr 'IntSort -> Expr 'IntSort
forall (t :: SMTSort). Num (HaskellType t) => Expr t -> Expr t
Neg Expr 'IntSort
y)
   {-# INLINE (-) #-}
   (Constant (IntValue HaskellType 'IntSort
0)) * :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
* Expr 'IntSort
_ = Expr 'IntSort
0
   Expr 'IntSort
_ * (Constant (IntValue HaskellType 'IntSort
0)) = Expr 'IntSort
0
   (Constant (IntValue HaskellType 'IntSort
1)) * Expr 'IntSort
y = Expr 'IntSort
y
   Expr 'IntSort
x * (Constant (IntValue HaskellType 'IntSort
1)) = Expr 'IntSort
x
   (Constant (IntValue HaskellType 'IntSort
x)) * (Constant (IntValue HaskellType 'IntSort
y)) = Value 'IntSort -> Expr 'IntSort
forall (t :: SMTSort). Value t -> Expr t
Constant (HaskellType 'IntSort -> Value 'IntSort
IntValue (Integer
HaskellType 'IntSort
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
HaskellType 'IntSort
y))
   Expr 'IntSort
x * Expr 'IntSort
y = Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall (t :: SMTSort).
Num (HaskellType t) =>
Expr t -> Expr t -> Expr t
Mul Expr 'IntSort
x Expr 'IntSort
y
   {-# INLINE (*) #-}
   negate :: Expr 'IntSort -> Expr 'IntSort
negate      = Expr 'IntSort -> Expr 'IntSort
forall (t :: SMTSort). Num (HaskellType t) => Expr t -> Expr t
Neg
   {-# INLINE negate #-}
   abs :: Expr 'IntSort -> Expr 'IntSort
abs         = Expr 'IntSort -> Expr 'IntSort
forall (t :: SMTSort). Num (HaskellType t) => Expr t -> Expr t
Abs
   {-# INLINE abs #-}
   signum :: Expr 'IntSort -> Expr 'IntSort
signum Expr 'IntSort
x    = Expr 'BoolSort -> Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall b a. Iteable b a => b -> a -> a -> a
ite (Expr 'IntSort
x Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall a. Equatable a => a -> a -> Expr 'BoolSort
=== Expr 'IntSort
0) Expr 'IntSort
0 (Expr 'IntSort -> Expr 'IntSort) -> Expr 'IntSort -> Expr 'IntSort
forall a b. (a -> b) -> a -> b
$ Expr 'BoolSort -> Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall b a. Iteable b a => b -> a -> a -> a
ite (Expr 'IntSort
x Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
<? Expr 'IntSort
0) (-Expr 'IntSort
1) Expr 'IntSort
1
   {-# INLINE signum #-}

instance Num (Expr RealSort) where
   fromInteger :: Integer -> Expr 'RealSort
fromInteger = Value 'RealSort -> Expr 'RealSort
forall (t :: SMTSort). Value t -> Expr t
Constant (Value 'RealSort -> Expr 'RealSort)
-> (Integer -> Value 'RealSort) -> Integer -> Expr 'RealSort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Value 'RealSort
HaskellType 'RealSort -> Value 'RealSort
RealValue (Double -> Value 'RealSort)
-> (Integer -> Double) -> Integer -> Value 'RealSort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral
   {-# INLINE fromInteger #-}
   (Constant (RealValue HaskellType 'RealSort
0)) + :: Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
+ Expr 'RealSort
y = Expr 'RealSort
y
   Expr 'RealSort
x + (Constant (RealValue HaskellType 'RealSort
0)) = Expr 'RealSort
x
   (Constant (RealValue HaskellType 'RealSort
x)) + (Constant (RealValue HaskellType 'RealSort
y)) = Value 'RealSort -> Expr 'RealSort
forall (t :: SMTSort). Value t -> Expr t
Constant (HaskellType 'RealSort -> Value 'RealSort
RealValue (Double
HaskellType 'RealSort
x Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
HaskellType 'RealSort
y))
   Expr 'RealSort
x + Expr 'RealSort
y = Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
forall (t :: SMTSort).
Num (HaskellType t) =>
Expr t -> Expr t -> Expr t
Plus Expr 'RealSort
x Expr 'RealSort
y
   {-# INLINE (+) #-}
   Expr 'RealSort
x - :: Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
- (Constant (RealValue HaskellType 'RealSort
0)) = Expr 'RealSort
x
   (Constant (RealValue HaskellType 'RealSort
x)) - (Constant (RealValue HaskellType 'RealSort
y)) = Value 'RealSort -> Expr 'RealSort
forall (t :: SMTSort). Value t -> Expr t
Constant (HaskellType 'RealSort -> Value 'RealSort
RealValue (Double
HaskellType 'RealSort
x Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
HaskellType 'RealSort
y))
   Expr 'RealSort
x - Expr 'RealSort
y = Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
forall (t :: SMTSort).
Num (HaskellType t) =>
Expr t -> Expr t -> Expr t
Plus Expr 'RealSort
x (Expr 'RealSort -> Expr 'RealSort
forall (t :: SMTSort). Num (HaskellType t) => Expr t -> Expr t
Neg Expr 'RealSort
y)
   {-# INLINE (-) #-}
   (Constant (RealValue HaskellType 'RealSort
0)) * :: Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
* Expr 'RealSort
_ = Expr 'RealSort
0
   Expr 'RealSort
_ * (Constant (RealValue HaskellType 'RealSort
0)) = Expr 'RealSort
0
   (Constant (RealValue HaskellType 'RealSort
1)) * Expr 'RealSort
y = Expr 'RealSort
y
   Expr 'RealSort
x * (Constant (RealValue HaskellType 'RealSort
1)) = Expr 'RealSort
x
   (Constant (RealValue HaskellType 'RealSort
x)) * (Constant (RealValue HaskellType 'RealSort
y)) = Value 'RealSort -> Expr 'RealSort
forall (t :: SMTSort). Value t -> Expr t
Constant (HaskellType 'RealSort -> Value 'RealSort
RealValue (Double
HaskellType 'RealSort
x Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
HaskellType 'RealSort
y))
   Expr 'RealSort
x * Expr 'RealSort
y = Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
forall (t :: SMTSort).
Num (HaskellType t) =>
Expr t -> Expr t -> Expr t
Mul Expr 'RealSort
x Expr 'RealSort
y
   {-# INLINE (*) #-}
   negate :: Expr 'RealSort -> Expr 'RealSort
negate      = Expr 'RealSort -> Expr 'RealSort
forall (t :: SMTSort). Num (HaskellType t) => Expr t -> Expr t
Neg
   {-# INLINE negate #-}
   abs :: Expr 'RealSort -> Expr 'RealSort
abs         = Expr 'RealSort -> Expr 'RealSort
forall (t :: SMTSort). Num (HaskellType t) => Expr t -> Expr t
Abs
   {-# INLINE abs #-}
   signum :: Expr 'RealSort -> Expr 'RealSort
signum Expr 'RealSort
x    = Expr 'BoolSort
-> Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
forall b a. Iteable b a => b -> a -> a -> a
ite (Expr 'RealSort
x Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
forall a. Equatable a => a -> a -> Expr 'BoolSort
=== Expr 'RealSort
0) Expr 'RealSort
0 (Expr 'RealSort -> Expr 'RealSort)
-> Expr 'RealSort -> Expr 'RealSort
forall a b. (a -> b) -> a -> b
$ Expr 'BoolSort
-> Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
forall b a. Iteable b a => b -> a -> a -> a
ite (Expr 'RealSort
x Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
<? Expr 'RealSort
0) (-Expr 'RealSort
1) Expr 'RealSort
1
   {-# INLINE signum #-}

instance KnownNat n => Num (Expr (BvSort n)) where
   fromInteger :: Integer -> Expr ('BvSort n)
fromInteger = Value ('BvSort n) -> Expr ('BvSort n)
forall (t :: SMTSort). Value t -> Expr t
Constant (Value ('BvSort n) -> Expr ('BvSort n))
-> (Integer -> Value ('BvSort n)) -> Integer -> Expr ('BvSort n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bitvec n -> Value ('BvSort n)
HaskellType ('BvSort n) -> Value ('BvSort n)
forall (n :: Nat). HaskellType ('BvSort n) -> Value ('BvSort n)
BvValue (Bitvec n -> Value ('BvSort n))
-> (Integer -> Bitvec n) -> Integer -> Value ('BvSort n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Bitvec n
forall a. Num a => Integer -> a
fromInteger
   {-# INLINE fromInteger #-}
   (Constant (BvValue HaskellType ('BvSort n)
0)) + :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
+ Expr ('BvSort n)
y = Expr ('BvSort n)
y
   Expr ('BvSort n)
x + (Constant (BvValue HaskellType ('BvSort n)
0)) = Expr ('BvSort n)
x
   (Constant (BvValue HaskellType ('BvSort n)
x)) + (Constant (BvValue HaskellType ('BvSort n)
y)) = Value ('BvSort n) -> Expr ('BvSort n)
forall (t :: SMTSort). Value t -> Expr t
Constant (HaskellType ('BvSort n) -> Value ('BvSort n)
forall (n :: Nat). HaskellType ('BvSort n) -> Value ('BvSort n)
BvValue (Bitvec n
HaskellType ('BvSort n)
x Bitvec n -> Bitvec n -> Bitvec n
forall a. Num a => a -> a -> a
+ Bitvec n
HaskellType ('BvSort n)
y))
   Expr ('BvSort n)
x + Expr ('BvSort n)
y = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvAdd Expr ('BvSort n)
x Expr ('BvSort n)
y
   {-# INLINE (+) #-}
   Expr ('BvSort n)
x - :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
- (Constant (BvValue HaskellType ('BvSort n)
0)) = Expr ('BvSort n)
x
   (Constant (BvValue HaskellType ('BvSort n)
x)) - (Constant (BvValue HaskellType ('BvSort n)
y)) = Value ('BvSort n) -> Expr ('BvSort n)
forall (t :: SMTSort). Value t -> Expr t
Constant (HaskellType ('BvSort n) -> Value ('BvSort n)
forall (n :: Nat). HaskellType ('BvSort n) -> Value ('BvSort n)
BvValue (Bitvec n
HaskellType ('BvSort n)
x Bitvec n -> Bitvec n -> Bitvec n
forall a. Num a => a -> a -> a
- Bitvec n
HaskellType ('BvSort n)
y))
   Expr ('BvSort n)
x - Expr ('BvSort n)
y = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvSub Expr ('BvSort n)
x Expr ('BvSort n)
y
   {-# INLINE (-) #-}
   (Constant (BvValue HaskellType ('BvSort n)
0)) * :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
* Expr ('BvSort n)
_ = Expr ('BvSort n)
0
   Expr ('BvSort n)
_ * (Constant (BvValue HaskellType ('BvSort n)
0)) = Expr ('BvSort n)
0
   (Constant (BvValue HaskellType ('BvSort n)
1)) * Expr ('BvSort n)
y = Expr ('BvSort n)
y
   Expr ('BvSort n)
x * (Constant (BvValue HaskellType ('BvSort n)
1)) = Expr ('BvSort n)
x
   (Constant (BvValue HaskellType ('BvSort n)
x)) * (Constant (BvValue HaskellType ('BvSort n)
y)) = Value ('BvSort n) -> Expr ('BvSort n)
forall (t :: SMTSort). Value t -> Expr t
Constant (HaskellType ('BvSort n) -> Value ('BvSort n)
forall (n :: Nat). HaskellType ('BvSort n) -> Value ('BvSort n)
BvValue (Bitvec n
HaskellType ('BvSort n)
x Bitvec n -> Bitvec n -> Bitvec n
forall a. Num a => a -> a -> a
* Bitvec n
HaskellType ('BvSort n)
y))
   Expr ('BvSort n)
x * Expr ('BvSort n)
y = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvMul Expr ('BvSort n)
x Expr ('BvSort n)
y
   {-# INLINE (*) #-}
   abs :: Expr ('BvSort n) -> Expr ('BvSort n)
abs         = Expr ('BvSort n) -> Expr ('BvSort n)
forall a. a -> a
id
   {-# INLINE abs #-}
   signum :: Expr ('BvSort n) -> Expr ('BvSort n)
signum Expr ('BvSort n)
_    = Expr ('BvSort n)
0
   {-# INLINE signum #-}

instance Fractional (Expr RealSort) where
  fromRational :: Rational -> Expr 'RealSort
fromRational = Value 'RealSort -> Expr 'RealSort
forall (t :: SMTSort). Value t -> Expr t
Constant (Value 'RealSort -> Expr 'RealSort)
-> (Rational -> Value 'RealSort) -> Rational -> Expr 'RealSort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Value 'RealSort
HaskellType 'RealSort -> Value 'RealSort
RealValue (Double -> Value 'RealSort)
-> (Rational -> Double) -> Rational -> Value 'RealSort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Double
forall a. Fractional a => Rational -> a
fromRational
  {-# INLINE fromRational #-}
  Expr 'RealSort
x / :: Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
/ (Constant (RealValue HaskellType 'RealSort
1)) = Expr 'RealSort
x
  (Constant (RealValue HaskellType 'RealSort
0)) / Expr 'RealSort
_ = Expr 'RealSort
0
  (Constant (RealValue HaskellType 'RealSort
x)) / (Constant (RealValue HaskellType 'RealSort
y)) = Value 'RealSort -> Expr 'RealSort
forall (t :: SMTSort). Value t -> Expr t
Constant (HaskellType 'RealSort -> Value 'RealSort
RealValue (Double
HaskellType 'RealSort
x Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
HaskellType 'RealSort
y))
  Expr 'RealSort
x / Expr 'RealSort
y          = Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
Div Expr 'RealSort
x Expr 'RealSort
y
  {-# INLINE (/) #-}

instance Floating (Expr RealSort) where
    pi :: Expr 'RealSort
pi    = Expr 'RealSort
Pi
    {-# INLINE pi #-}
    exp :: Expr 'RealSort -> Expr 'RealSort
exp   = Expr 'RealSort -> Expr 'RealSort
Exp
    {-# INLINE exp #-}
    log :: Expr 'RealSort -> Expr 'RealSort
log   = [Char] -> Expr 'RealSort -> Expr 'RealSort
forall a. HasCallStack => [Char] -> a
error [Char]
"SMT-Solvers currently do not support log"
    sqrt :: Expr 'RealSort -> Expr 'RealSort
sqrt  = Expr 'RealSort -> Expr 'RealSort
Sqrt
    {-# INLINE sqrt #-}
    sin :: Expr 'RealSort -> Expr 'RealSort
sin   = Expr 'RealSort -> Expr 'RealSort
Sin
    {-# INLINE sin #-}
    cos :: Expr 'RealSort -> Expr 'RealSort
cos   = Expr 'RealSort -> Expr 'RealSort
Cos
    {-# INLINE cos #-}
    tan :: Expr 'RealSort -> Expr 'RealSort
tan   = Expr 'RealSort -> Expr 'RealSort
Tan
    {-# INLINE tan #-}
    asin :: Expr 'RealSort -> Expr 'RealSort
asin  = Expr 'RealSort -> Expr 'RealSort
Asin
    {-# INLINE asin #-}
    acos :: Expr 'RealSort -> Expr 'RealSort
acos  = Expr 'RealSort -> Expr 'RealSort
Acos
    {-# INLINE acos #-}
    atan :: Expr 'RealSort -> Expr 'RealSort
atan  = Expr 'RealSort -> Expr 'RealSort
Atan
    {-# INLINE atan #-}
    sinh :: Expr 'RealSort -> Expr 'RealSort
sinh  = [Char] -> Expr 'RealSort -> Expr 'RealSort
forall a. HasCallStack => [Char] -> a
error [Char]
"SMT-Solver currently do not support sinh"
    cosh :: Expr 'RealSort -> Expr 'RealSort
cosh  = [Char] -> Expr 'RealSort -> Expr 'RealSort
forall a. HasCallStack => [Char] -> a
error [Char]
"SMT-Solver currently do not support cosh"
    tanh :: Expr 'RealSort -> Expr 'RealSort
tanh  = [Char] -> Expr 'RealSort -> Expr 'RealSort
forall a. HasCallStack => [Char] -> a
error [Char]
"SMT-Solver currently do not support tanh"
    asinh :: Expr 'RealSort -> Expr 'RealSort
asinh = [Char] -> Expr 'RealSort -> Expr 'RealSort
forall a. HasCallStack => [Char] -> a
error [Char]
"SMT-Solver currently do not support asinh"
    acosh :: Expr 'RealSort -> Expr 'RealSort
acosh = [Char] -> Expr 'RealSort -> Expr 'RealSort
forall a. HasCallStack => [Char] -> a
error [Char]
"SMT-Solver currently do not support acosh"
    atanh :: Expr 'RealSort -> Expr 'RealSort
atanh = [Char] -> Expr 'RealSort -> Expr 'RealSort
forall a. HasCallStack => [Char] -> a
error [Char]
"SMT-Solver currently do not support atanh"

instance Integraled (Expr IntSort) where
  quot :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
quot = Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
IDiv
  {-# INLINE quot #-}
  rem :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
rem  = Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
Mod
  {-# INLINE rem #-}
  div :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
div  = Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
IDiv
  {-# INLINE div #-}
  mod :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
mod  = Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
Mod
  {-# INLINE mod #-}
  quotRem :: Expr 'IntSort -> Expr 'IntSort -> (Expr 'IntSort, Expr 'IntSort)
quotRem Expr 'IntSort
x Expr 'IntSort
y = (Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall a. Integraled a => a -> a -> a
quot Expr 'IntSort
x Expr 'IntSort
y, Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall a. Integraled a => a -> a -> a
rem Expr 'IntSort
x Expr 'IntSort
y)
  {-# INLINE quotRem #-}
  divMod :: Expr 'IntSort -> Expr 'IntSort -> (Expr 'IntSort, Expr 'IntSort)
divMod Expr 'IntSort
x Expr 'IntSort
y  = (Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall a. Integraled a => a -> a -> a
div Expr 'IntSort
x Expr 'IntSort
y, Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall a. Integraled a => a -> a -> a
mod Expr 'IntSort
x Expr 'IntSort
y)
  {-# INLINE divMod #-}

instance KnownNat n => Integraled (Expr (BvSort n)) where
  quot :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
quot        = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvuDiv
  {-# INLINE quot #-}
  rem :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
rem         = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvuRem
  {-# INLINE rem #-}
  div :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
div         = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvuDiv
  {-# INLINE div #-}
  mod :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
mod         = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvuRem
  {-# INLINE mod #-}
  quotRem :: Expr ('BvSort n)
-> Expr ('BvSort n) -> (Expr ('BvSort n), Expr ('BvSort n))
quotRem Expr ('BvSort n)
x Expr ('BvSort n)
y = (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall a. Integraled a => a -> a -> a
quot Expr ('BvSort n)
x Expr ('BvSort n)
y, Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall a. Integraled a => a -> a -> a
rem Expr ('BvSort n)
x Expr ('BvSort n)
y)
  {-# INLINE quotRem #-}
  divMod :: Expr ('BvSort n)
-> Expr ('BvSort n) -> (Expr ('BvSort n), Expr ('BvSort n))
divMod Expr ('BvSort n)
x Expr ('BvSort n)
y  = (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall a. Integraled a => a -> a -> a
div Expr ('BvSort n)
x Expr ('BvSort n)
y, Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall a. Integraled a => a -> a -> a
mod Expr ('BvSort n)
x Expr ('BvSort n)
y)
  {-# INLINE divMod #-}