Remove the "round-to-zero" versions of integer division and modulus,

since we're going to restrict signed division to bitvectors.
This commit is contained in:
Rob Dockins 2020-03-19 17:30:14 -07:00
parent 72cf1ccd18
commit 20ad7e8e86
4 changed files with 3 additions and 37 deletions

View File

@ -66,7 +66,7 @@ class MonadIO (SEval sym) => Backend sym where
-- | Merge the two given computations according to the predicate. -- | Merge the two given computations according to the predicate.
mergeEval :: mergeEval ::
sym -> sym ->
(SBit sym -> a -> a -> SEval sym a) {- ^ A merge operation on values -} -> (SBit sym -> a -> a -> SEval sym a) {- ^ A merge operation on values -} ->
SBit sym {- ^ The condition -} -> SBit sym {- ^ The condition -} ->
SEval sym a {- ^ The "then" computation -} -> SEval sym a {- ^ The "then" computation -} ->
SEval sym a {- ^ The "else" computation -} -> SEval sym a {- ^ The "else" computation -} ->
@ -411,24 +411,6 @@ class MonadIO (SEval sym) => Backend sym where
SInteger sym -> SInteger sym ->
SEval sym (SInteger sym) SEval sym (SInteger sym)
-- | Integer division, rounding toward zero. It is illegal to
-- call with a second argument concretely equal to 0.
-- Same semantics as Haskell's @quot@ operation.
intDivRTZ ::
sym ->
SInteger sym ->
SInteger sym ->
SEval sym (SInteger sym)
-- | Integer modulus, with division rounding toward zero. It is illegal to
-- call with a second argument concretely equal to 0.
-- Same semantics as Haskell's @rem@ operation.
intModRTZ ::
sym ->
SInteger sym ->
SInteger sym ->
SEval sym (SInteger sym)
-- | Integer exponentiation. The second argument must be non-negative. -- | Integer exponentiation. The second argument must be non-negative.
intExp :: intExp ::
sym -> sym ->

View File

@ -304,12 +304,6 @@ instance Backend Concrete where
intMod sym x y = intMod sym x y =
do assertSideCondition sym (y /= 0) DivideByZero do assertSideCondition sym (y /= 0) DivideByZero
pure $! x `mod` y pure $! x `mod` y
intDivRTZ sym x y =
do assertSideCondition sym (y /= 0) DivideByZero
pure $! x `quot` y
intModRTZ sym x y =
do assertSideCondition sym (y /= 0) DivideByZero
pure $! x `rem` y
intExp sym x y = intExp sym x y =
do assertSideCondition sym (y >= 0) NegativeExponent do assertSideCondition sym (y >= 0) NegativeExponent
pure $! x ^ y pure $! x ^ y

View File

@ -316,14 +316,14 @@ sdivV :: Backend sym => sym -> Binary sym
sdivV sym = arithBinary sym opw opi opz sdivV sym = arithBinary sym opw opi opz
where where
opw _w x y = wordSignedDiv sym x y opw _w x y = wordSignedDiv sym x y
opi x y = intDivRTZ sym x y opi x y = intDiv sym x y
opz m x y = znDiv sym m x y opz m x y = znDiv sym m x y
smodV :: Backend sym => sym -> Binary sym smodV :: Backend sym => sym -> Binary sym
smodV sym = arithBinary sym opw opi opz smodV sym = arithBinary sym opw opi opz
where where
opw _w x y = wordSignedMod sym x y opw _w x y = wordSignedMod sym x y
opi x y = intModRTZ sym x y opi x y = intMod sym x y
opz m x y = znMod sym m x y opz m x y = znMod sym m x y
expV :: Backend sym => sym -> Binary sym expV :: Backend sym => sym -> Binary sym

View File

@ -297,16 +297,6 @@ instance Backend SBV where
assertSideCondition sym (svNot (svEqual b z)) DivideByZero assertSideCondition sym (svNot (svEqual b z)) DivideByZero
pure $! svRem a b -- TODO! Fix this: see issue #662 pure $! svRem a b -- TODO! Fix this: see issue #662
intDivRTZ sym a b =
do let z = svInteger KUnbounded 0
assertSideCondition sym (svNot (svEqual b z)) DivideByZero
pure $! svQuot a b -- TODO! Fix this: see issue #662
intModRTZ sym a b =
do let z = svInteger KUnbounded 0
assertSideCondition sym (svNot (svEqual b z)) DivideByZero
pure $! svQuot a b -- TODO! Fix this: see issue #662
intExp sym a b = intExp sym a b =
do let z = svInteger KUnbounded 0 do let z = svInteger KUnbounded 0
assertSideCondition sym (svLessEq z b) NegativeExponent assertSideCondition sym (svLessEq z b) NegativeExponent