Browse files

comments about quot/rem etc.

  • Loading branch information...
1 parent cfdc455 commit ed72f8cfff0f880eb13558cc2e7e1d8ca22fdf06 @LeventErkok committed Aug 28, 2012
Showing with 6 additions and 2 deletions.
  1. +1 −1 Data/SBV/BitVectors/Data.hs
  2. +2 −0 Data/SBV/BitVectors/Model.hs
  3. +2 −0 Data/SBV/Compilers/C.hs
  4. +1 −1 SBVUnitTest/SBVUnitTestBuildTime.hs
View
2 Data/SBV/BitVectors/Data.hs
@@ -163,7 +163,7 @@ instance Show SBVType where
-- | Symbolic operations
data Op = Plus | Times | Minus
- | Quot | Rem -- quot and rem are unsigned only
+ | Quot | Rem
| Equal | NotEqual
| LessThan | GreaterThan | LessEq | GreaterEq
| Ite
View
2 Data/SBV/BitVectors/Model.hs
@@ -745,6 +745,8 @@ enumCvt w x = case unliteral x of
--
-- Note that our instances implement this law even when @x@ is @0@ itself.
--
+-- NB. 'quot' truncates toward zero, while 'div' truncates toward negative infinity.
+--
-- Minimal complete definition: 'sQuotRem', 'sDivMod'
class SDivisible a where
sQuotRem :: a -> a -> (a, a)
View
2 Data/SBV/Compilers/C.hs
@@ -507,6 +507,8 @@ ppExpr cfg consts (SBVApp op opArgs) = p op (map (showSW cfg consts) opArgs)
Just i -> (True, canOverflow True i)
KUninterpreted s -> die $ "Uninterpreted sort: " ++ s
-- Div/Rem should be careful on 0, in the SBV world x `div` 0 is 0, x `rem` 0 is x
+ -- NB: Quot is supposed to truncate toward 0; Not clear to me if C guarantees this behavior.
+ -- Brief googling suggests C99 does indeed truncate toward 0, but other C compilers might differ.
p Quot [a, b] = parens (b <+> text "== 0") <+> text "?" <+> text "0" <+> text ":" <+> parens (a <+> text "/" <+> b)
p Rem [a, b] = parens (b <+> text "== 0") <+> text "?" <+> a <+> text ":" <+> parens (a <+> text "%" <+> b)
p o [a, b]
View
2 SBVUnitTest/SBVUnitTestBuildTime.hs
@@ -2,4 +2,4 @@
module SBVUnitTestBuildTime (buildTime) where
buildTime :: String
-buildTime = "Tue Aug 28 22:07:31 PDT 2012"
+buildTime = "Tue Aug 28 22:37:47 PDT 2012"

0 comments on commit ed72f8c

Please sign in to comment.