diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,25 @@ * Hackage: * GitHub: -* Latest Hackage released version: 3.3 +* Latest Hackage released version: 3.4 + +### Version 3.4, 2014-12-21 + + * This release is mainly addressing floating-point changes in SMT-Lib. + + * Track changes in the QF_FPA logic standard; new constants and alike. If you are + using the floating-point logic, then you need a relatively new version of Z3 + installed (4.3.3 or newer). + + * Add unary-negation as an explicit operator. Previously, we merely used the "0-x" + semantics; but with floating point, this does not hold as 0-0 is 0, and is not -0! + (Note that negative-zero is a valid floating point value, that is different than + positive-zero; yet it compares equal to it. Sigh..) + + * Similarly, add abs as a native method; to make sure we map it to fp.abs for + floating point values. + + * Test suite improvements ### Version 3.3, 2014-12-05 diff --git a/Data/SBV/BitVectors/Data.hs b/Data/SBV/BitVectors/Data.hs --- a/Data/SBV/BitVectors/Data.hs +++ b/Data/SBV/BitVectors/Data.hs @@ -226,7 +226,7 @@ show (SBVType xs) = intercalate " -> " $ map show xs -- | Symbolic operations -data Op = Plus | Times | Minus +data Op = Plus | Times | Minus | UNeg | Abs | Quot | Rem | Equal | NotEqual | LessThan | GreaterThan | LessEq | GreaterEq @@ -246,13 +246,13 @@ -- might be confusing. This function will *not* be uninterpreted in reality, as QF_FPA will define it. It's -- a bit of a shame, but much easier to implement it this way. smtLibSquareRoot :: Op -smtLibSquareRoot = Uninterpreted "squareRoot" +smtLibSquareRoot = Uninterpreted "fp.sqrt" -- | SMT-Lib's fusedMA over floats/doubles. Similar to the 'smtLibSquareRoot'. Note that we cannot implement -- this function in Haskell as precision loss would be inevitable. Maybe Haskell will eventually add this op -- to the Num class. smtLibFusedMA :: Op -smtLibFusedMA = Uninterpreted "fusedMA" +smtLibFusedMA = Uninterpreted "fp.fma" -- | A symbolic expression data SBVExpr = SBVApp !Op ![SW] @@ -392,7 +392,7 @@ show op | Just s <- op `lookup` syms = s | True = error "impossible happened; can't find op!" - where syms = [ (Plus, "+"), (Times, "*"), (Minus, "-") + where syms = [ (Plus, "+"), (Times, "*"), (Minus, "-"), (UNeg, "-"), (Abs, "abs") , (Quot, "quot") , (Rem, "rem") , (Equal, "=="), (NotEqual, "/=") @@ -746,7 +746,7 @@ = error $ "SBV: " ++ show sortName ++ " is a reserved sort; please use a different name." | True = modifyIORef (rUsedKinds st) (Set.insert k) - where reserved = ["Int", "Real", "List", "Array", "Bool", "NUMERAL", "DECIMAL", "STRING", "FP"] -- Reserved by SMT-Lib + where reserved = ["Int", "Real", "List", "Array", "Bool", "NUMERAL", "DECIMAL", "STRING", "FP", "FloatingPoint"] -- Reserved by SMT-Lib -- | Create a new constant; hash-cons as necessary newConst :: State -> CW -> IO SW diff --git a/Data/SBV/BitVectors/Model.hs b/Data/SBV/BitVectors/Model.hs --- a/Data/SBV/BitVectors/Model.hs +++ b/Data/SBV/BitVectors/Model.hs @@ -624,12 +624,15 @@ x - y | y `isConcretely` (== 0) = x | True = liftSym2 (mkSymOp Minus) rationalCheck (-) (-) (-) (-) x y - abs a - | hasSign a = ite (a .< 0) (-a) a - | True = a + -- Abs is problematic for floating point, due to -0; case, so we carefully shuttle it down + -- to the solver to avoid the can of worms. (Alternative would be to do an if-then-else here.) + abs = liftSym1 (mkSymOp1 Abs) abs abs abs abs signum a | hasSign a = ite (a .< 0) (-1) (ite (a .== 0) 0 1) | True = oneIf (a ./= 0) + -- negate is tricky because on double/float -0 is different than 0; so we + -- just cannot rely on its default definition; which would be 0-0, which is not -0! + negate = liftSym1 (mkSymOp1 UNeg) (\x -> -x) (\x -> -x) (\x -> -x) (\x -> -x) instance (SymWord a, Fractional a) => Fractional (SBV a) where fromRational = literal . fromRational diff --git a/Data/SBV/BitVectors/PrettyNum.hs b/Data/SBV/BitVectors/PrettyNum.hs --- a/Data/SBV/BitVectors/PrettyNum.hs +++ b/Data/SBV/BitVectors/PrettyNum.hs @@ -207,21 +207,21 @@ showSMTFloat :: RoundingMode -> Float -> String showSMTFloat rm f | isNaN f = as "NaN" - | isInfinite f, f < 0 = as "minusInfinity" - | isInfinite f = as "plusInfinity" - | isNegativeZero f = "(- ((_ asFloat 8 24) " ++ smtRoundingMode rm ++ " (/ 0 1)))" - | True = "((_ asFloat 8 24) " ++ smtRoundingMode rm ++ " " ++ toSMTLibRational (toRational f) ++ ")" - where as s = "(as " ++ s ++ " (_ FP 8 24))" + | isInfinite f, f < 0 = as "-oo" + | isInfinite f = as "+oo" + | isNegativeZero f = "(fp.neg ((_ to_fp 8 24) " ++ smtRoundingMode rm ++ " (/ 0 1)))" + | True = "((_ to_fp 8 24) " ++ smtRoundingMode rm ++ " " ++ toSMTLibRational (toRational f) ++ ")" + where as s = "(as " ++ s ++ " (_ FloatingPoint 8 24))" -- | A version of show for doubles that generates correct SMTLib literals using the rounding mode showSMTDouble :: RoundingMode -> Double -> String showSMTDouble rm d | isNaN d = as "NaN" - | isInfinite d, d < 0 = as "minusInfinity" - | isInfinite d = as "plusInfinity" - | isNegativeZero d = "(- ((_ asFloat 11 53) " ++ smtRoundingMode rm ++ " (/ 0 1)))" - | True = "((_ asFloat 11 53) " ++ smtRoundingMode rm ++ " " ++ toSMTLibRational (toRational d) ++ ")" - where as s = "(as " ++ s ++ " (_ FP 11 53))" + | isInfinite d, d < 0 = as "-oo" + | isInfinite d = as "+oo" + | isNegativeZero d = "(fp.neg ((_ to_fp 11 53) " ++ smtRoundingMode rm ++ " (/ 0 1)))" + | True = "((_ to_fp 11 53) " ++ smtRoundingMode rm ++ " " ++ toSMTLibRational (toRational d) ++ ")" + where as s = "(as " ++ s ++ " (_ FloatingPoint 11 53))" -- | Show a rational in SMTLib format toSMTLibRational :: Rational -> String diff --git a/Data/SBV/Compilers/C.hs b/Data/SBV/Compilers/C.hs --- a/Data/SBV/Compilers/C.hs +++ b/Data/SBV/Compilers/C.hs @@ -487,18 +487,18 @@ , (Equal, "=="), (NotEqual, "!="), (LessThan, "<"), (GreaterThan, ">"), (LessEq, "<="), (GreaterEq, ">=") , (And, "&"), (Or, "|"), (XOr, "^") ] - uninterpret "squareRoot" as = let f = case kindOf (head opArgs) of + uninterpret "fp.sqrt" as = let f = case kindOf (head opArgs) of KFloat -> text "sqrtf" KDouble -> text "sqrt" k -> die $ "squareRoot on unexpected kind: " ++ show k - in f <> parens (fsep (punctuate comma as)) - uninterpret "fusedMA" as = let f = case kindOf (head opArgs) of + in f <> parens (fsep (punctuate comma as)) + uninterpret "fp.fma" as = let f = case kindOf (head opArgs) of KFloat -> text "fmaf" KDouble -> text "fma" k -> die $ "fusedMA on unexpected kind: " ++ show k - in f <> parens (fsep (punctuate comma as)) - uninterpret s [] = text "/* Uninterpreted constant */" <+> text s - uninterpret s as = text "/* Uninterpreted function */" <+> text s <> parens (fsep (punctuate comma as)) + in f <> parens (fsep (punctuate comma as)) + uninterpret s [] = text "/* Uninterpreted constant */" <+> text s + uninterpret s as = text "/* Uninterpreted function */" <+> text s <> parens (fsep (punctuate comma as)) p (ArrRead _) _ = tbd "User specified arrays (ArrRead)" p (ArrEq _ _) _ = tbd "User specified arrays (ArrEq)" p (Uninterpreted s) as = uninterpret s as @@ -542,6 +542,12 @@ -- 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 UNeg [a] = parens (text "-" <+> a) + p Abs [a] = let f = case kindOf (head opArgs) of + KFloat -> text "fabsf" + KDouble -> text "fabs" + _ -> text "abs" + in f <> parens a p o [a, b] | Just co <- lookup o cBinOps = a <+> text co <+> b diff --git a/Data/SBV/Examples/Existentials/Diophantine.hs b/Data/SBV/Examples/Existentials/Diophantine.hs --- a/Data/SBV/Examples/Existentials/Diophantine.hs +++ b/Data/SBV/Examples/Existentials/Diophantine.hs @@ -67,7 +67,7 @@ -- We have: -- -- >>> test --- NonHomogeneous [[0,2,0],[1,0,0]] [[1,0,2],[0,1,1]] +-- NonHomogeneous [[0,2,0],[1,0,0]] [[0,1,1],[1,0,2]] -- -- which means that the solutions are of the form: -- diff --git a/Data/SBV/Examples/Misc/Floating.hs b/Data/SBV/Examples/Misc/Floating.hs --- a/Data/SBV/Examples/Misc/Floating.hs +++ b/Data/SBV/Examples/Misc/Floating.hs @@ -26,16 +26,16 @@ -- -- >>> prove assocPlus -- Falsifiable. Counter-example: --- s0 = -Infinity :: SFloat --- s1 = Infinity :: SFloat --- s2 = -9.403955e-38 :: SFloat +-- s0 = -7.888609e-31 :: SFloat +-- s1 = 3.944307e-31 :: SFloat +-- s2 = NaN :: SFloat -- -- Indeed: -- --- >>> let i = 1/0 :: Float --- >>> ((-i) + i) + (-9.403955e-38) :: Float +-- >>> let i = 0/0 :: Float +-- >>> ((-7.888609e-31 + 3.944307e-31) + i) :: Float -- NaN --- >>> (-i) + (i + (-9.403955e-38)) :: Float +-- >>> (-7.888609e-31 + (3.944307e-31 + i)) :: Float -- NaN -- -- But keep in mind that @NaN@ does not equal itself in the floating point world! We have: @@ -54,18 +54,18 @@ -- -- >>> assocPlusRegular -- Falsifiable. Counter-example: --- x = 1.5775295e-30 :: SFloat --- y = 1.92593e-34 :: SFloat --- z = -2.1521e-41 :: SFloat +-- x = -3.7777752e22 :: SFloat +-- y = -1.180801e18 :: SFloat +-- z = 9.4447324e21 :: SFloat -- -- Indeed, we have: -- --- >>> (1.5775295e-30 + 1.92593e-34) + (-2.1521e-41) :: Float --- 1.5777222e-30 --- >>> 1.5775295e-30 + (1.92593e-34 + (-2.1521e-41)) :: Float --- 1.577722e-30 +-- >>> ((-3.7777752e22 + (-1.180801e18)) + 9.4447324e21) :: Float +-- -2.83342e22 +-- >>> (-3.7777752e22 + ((-1.180801e18) + 9.4447324e21)) :: Float +-- -2.8334201e22 -- --- Note the loss of precision in the second expression. +-- Note the loss of precision in the first expression. assocPlusRegular :: IO ThmResult assocPlusRegular = prove $ do [x, y, z] <- sFloats ["x", "y", "z"] let lhs = x+(y+z) @@ -85,17 +85,17 @@ -- -- >>> nonZeroAddition -- Falsifiable. Counter-example: --- a = -4.0 :: SFloat --- b = 4.5918e-41 :: SFloat +-- a = 2.1474839e10 :: SFloat +-- b = -7.275957e-11 :: SFloat -- -- Indeed, we have: -- --- >>> -4.0 + 4.5918e-41 == (-4.0 :: Float) +-- >>> 2.1474839e10 + (-7.275957e-11) == (2.1474839e10 :: Float) -- True -- -- But: -- --- >>> 4.5918e-41 == (0 :: Float) +-- >>> -7.275957e-11 == (0 :: Float) -- False -- nonZeroAddition :: IO ThmResult @@ -116,13 +116,13 @@ -- -- >>> multInverse -- Falsifiable. Counter-example: --- a = 1.3625818045773776e-308 :: SDouble +-- a = 1.2354518252390238e308 :: SDouble -- -- Indeed, we have: -- --- >>> let a = 1.3625818045773776e-308 :: Double +-- >>> let a = 1.2354518252390238e308 :: Double -- >>> a * (1/a) --- 0.9999999999999999 +-- 0.9999999999999998 multInverse :: IO ThmResult multInverse = prove $ do a <- sDouble "a" constrain $ isFPPoint a diff --git a/Data/SBV/Provers/SExpr.hs b/Data/SBV/Provers/SExpr.hs --- a/Data/SBV/Provers/SExpr.hs +++ b/Data/SBV/Provers/SExpr.hs @@ -83,8 +83,10 @@ cvt (EApp [ECon "_", ENum a, ENum _b]) = return $ ENum a cvt (EApp [ECon "root-obj", EApp (ECon "+":trms), ENum k]) = do ts <- mapM getCoeff trms return $ EReal $ mkPolyReal (Right (k, ts)) - cvt (EApp [ECon "as", n, EApp [ECon "_", ECon "FP", ENum 11, ENum 53]]) = getDouble n - cvt (EApp [ECon "as", n, EApp [ECon "_", ECon "FP", ENum 8, ENum 24]]) = getFloat n + cvt (EApp [ECon "as", n, EApp [ECon "_", ECon "FloatingPoint", ENum 11, ENum 53]]) = getDouble n + cvt (EApp [ECon "as", n, EApp [ECon "_", ECon "FloatingPoint", ENum 8, ENum 24]]) = getFloat n + cvt (EApp [ECon "as", n, ECon "Float64"]) = getDouble n + cvt (EApp [ECon "as", n, ECon "Float32"]) = getFloat n cvt x = return x getCoeff (EApp [ECon "*", ENum k, EApp [ECon "^", ECon "x", ENum p]]) = return (k, p) -- kx^p getCoeff (EApp [ECon "*", ENum k, ECon "x" ] ) = return (k, 1) -- kx @@ -95,18 +97,28 @@ getDouble (ECon s) = case (s, rdFP (dropWhile (== '+') s)) of ("plusInfinity", _ ) -> return $ EDouble infinity ("minusInfinity", _ ) -> return $ EDouble (-infinity) + ("oo", _ ) -> return $ EDouble infinity + ("-oo", _ ) -> return $ EDouble (-infinity) + ("zero", _ ) -> return $ EDouble 0 + ("-zero", _ ) -> return $ EDouble (-0) ("NaN", _ ) -> return $ EDouble nan (_, Just v) -> return $ EDouble v - _ -> die $ "Cannot parse a double value from: " ++ s + _ -> die $ "Cannot parse a double value from: " ++ s + getDouble (EApp [_, s, _, _]) = getDouble s getDouble (EReal r) = return $ EDouble $ fromRat $ toRational r getDouble x = die $ "Cannot parse a double value from: " ++ show x getFloat (ECon s) = case (s, rdFP (dropWhile (== '+') s)) of ("plusInfinity", _ ) -> return $ EFloat infinity ("minusInfinity", _ ) -> return $ EFloat (-infinity) + ("oo", _ ) -> return $ EFloat infinity + ("-oo", _ ) -> return $ EFloat (-infinity) + ("zero", _ ) -> return $ EFloat 0 + ("-zero", _ ) -> return $ EFloat (-0) ("NaN", _ ) -> return $ EFloat nan (_, Just v) -> return $ EFloat v - _ -> die $ "Cannot parse a float value from: " ++ s + _ -> die $ "Cannot parse a float value from: " ++ s getFloat (EReal r) = return $ EFloat $ fromRat $ toRational r + getFloat (EApp [_, s, _, _]) = getFloat s getFloat x = die $ "Cannot parse a float value from: " ++ show x -- | Parses the Z3 floating point formatted numbers like so: 1.321p5/1.2123e9 etc. diff --git a/Data/SBV/SMT/SMTLib1.hs b/Data/SBV/SMT/SMTLib1.hs --- a/Data/SBV/SMT/SMTLib1.hs +++ b/Data/SBV/SMT/SMTLib1.hs @@ -207,6 +207,13 @@ cvtExp (SBVApp (Extract i j) [a]) = "(extract[" ++ show i ++ ":" ++ show j ++ "] " ++ show a ++ ")" cvtExp (SBVApp (ArrEq i j) []) = "(= array_" ++ show i ++ " array_" ++ show j ++")" cvtExp (SBVApp (ArrRead i) [a]) = "(select array_" ++ show i ++ " " ++ show a ++ ")" +cvtExp (SBVApp Abs [a]) + | hasSign a = "(ite " ++ ltz ++ " " ++ na ++ " " ++ sa ++ ")" + | True = sa + where sa = show a + na = "(bvneg " ++ sa ++ ")" + z = cvtCW (mkConstCW (kindOf a) (0::Integer)) + ltz = "(bvslt " ++ sa ++ " " ++ z ++ ")" cvtExp (SBVApp (Uninterpreted nm) []) = "uninterpreted_" ++ nm cvtExp (SBVApp (Uninterpreted nm) args) = "(uninterpreted_" ++ nm ++ " " ++ unwords (map show args) ++ ")" cvtExp inp@(SBVApp op args) @@ -269,6 +276,7 @@ , (And, lift2B "and" "bvand") , (Or, lift2B "or" "bvor") , (Not, lift1B "not" "bvnot") + , (UNeg, lift1B "not" "bvneg") , (XOr, lift2B "xor" "bvxor") , (Join, lift2 "concat") ] diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -269,8 +269,8 @@ smtType (KBounded _ sz) = "(_ BitVec " ++ show sz ++ ")" smtType KUnbounded = "Int" smtType KReal = "Real" -smtType KFloat = "(_ FP 8 24)" -smtType KDouble = "(_ FP 11 53)" +smtType KFloat = "(_ FloatingPoint 8 24)" +smtType KDouble = "(_ FloatingPoint 11 53)" smtType (KUninterpreted s) = s cvtType :: SBVType -> String @@ -347,8 +347,19 @@ lift2 o _ [x, y] = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")" lift2 o _ sbvs = error $ "SBV.SMTLib2.sh.lift2: Unexpected arguments: " ++ show (o, sbvs) -- lift a binary operation with rounding-mode added; used for floating-point arithmetic - lift2WM o | doubleOp || floatOp = lift2 (addRM o) - | True = lift2 o + lift2WM o fo | doubleOp || floatOp = lift2 (addRM fo) + | True = lift2 o + lift1FP o fo | doubleOp || floatOp = lift1 fo + | True = lift1 o + liftAbs sgned args | doubleOp || floatOp = lift1 "fp.abs" sgned args + | intOp = lift1 "abs" sgned args + | bvOp, sgned = mkAbs (head args) "bvslt" "bvneg" + | bvOp = head args + | True = mkAbs (head args) "<" "-" + where mkAbs x cmp neg = "(ite " ++ ltz ++ " " ++ nx ++ " " ++ x ++ ")" + where ltz = "(" ++ cmp ++ " " ++ x ++ " " ++ z ++ ")" + nx = "(" ++ neg ++ " " ++ x ++ ")" + z = cvtCW rm (mkConstCW (kindOf (head arguments)) (0::Integer)) lift2B bOp vOp | boolOp = lift2 bOp | True = lift2 vOp @@ -360,14 +371,16 @@ | True = "(= " ++ lift2 "bvcomp" sgn sbvs ++ " #b1)" neqBV sgn sbvs = "(not " ++ eqBV sgn sbvs ++ ")" equal sgn sbvs - | doubleOp = lift2 "==" sgn sbvs - | floatOp = lift2 "==" sgn sbvs + | doubleOp = lift2 "fp.eq" sgn sbvs + | floatOp = lift2 "fp.eq" sgn sbvs | True = lift2 "=" sgn sbvs notEqual sgn sbvs | doubleOp = "(not " ++ equal sgn sbvs ++ ")" | floatOp = "(not " ++ equal sgn sbvs ++ ")" | True = lift2 "distinct" sgn sbvs lift2S oU oS sgn = lift2 (if sgn then oS else oU) sgn + lift2Cmp o fo | doubleOp || floatOp = lift2 fo + | True = lift2 o lift1 o _ [x] = "(" ++ o ++ " " ++ x ++ ")" lift1 o _ sbvs = error $ "SBV.SMT.SMTLib2.sh.lift1: Unexpected arguments: " ++ show (o, sbvs) sh (SBVApp Ite [a, b, c]) = "(ite " ++ ssw a ++ " " ++ ssw b ++ " " ++ ssw c ++ ")" @@ -391,8 +404,8 @@ KBounded{} -> if hasSign i then ("bvslt", "bvsle") else ("bvult", "bvule") KUnbounded -> ("<", "<=") KReal -> ("<", "<=") - KFloat -> ("<", "<=") - KDouble -> ("<", "<=") + KFloat -> ("fp.lt", "fp.leq") + KDouble -> ("fp.lt", "fp.geq") KUninterpreted s -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected uninterpreted valued index: " ++ s mkCnst = cvtCW rm . mkConstCW (kindOf i) le0 = "(" ++ less ++ " " ++ ssw i ++ " " ++ mkCnst 0 ++ ")" @@ -402,7 +415,7 @@ sh (SBVApp (Uninterpreted nm) []) = nm sh (SBVApp (Uninterpreted nm) args) = "(" ++ nm' ++ " " ++ unwords (map ssw args) ++ ")" where -- slight hack needed here to take advantage of custom floating-point functions.. sigh. - fpSpecials = ["squareRoot", "fusedMA"] + fpSpecials = ["fp.sqrt", "fusedMA"] nm' | (floatOp || doubleOp) && (nm `elem` fpSpecials) = addRM nm | True = nm sh (SBVApp (Extract 0 0) [a]) -- special SInteger -> SReal conversion @@ -457,6 +470,8 @@ where smtOpBVTable = [ (Plus, lift2 "bvadd") , (Minus, lift2 "bvsub") , (Times, lift2 "bvmul") + , (UNeg, lift1B "not" "bvneg") + , (Abs, liftAbs) , (Quot, lift2S "bvudiv" "bvsdiv") , (Rem, lift2S "bvurem" "bvsrem") , (Equal, eqBV) @@ -479,23 +494,25 @@ swp [x, y] = [y, x] swp xs = error $ "SBV.SMT.SMTLib2.boolComps.swp: Impossible happened, incorrect arity (expected 2): " ++ show xs smtOpRealTable = smtIntRealShared - ++ [ (Quot, lift2WM "/") + ++ [ (Quot, lift2WM "/" "fp.div") ] smtOpIntTable = smtIntRealShared ++ [ (Quot, lift2 "div") , (Rem, lift2 "mod") ] smtOpFloatDoubleTable = smtIntRealShared - ++ [(Quot, lift2WM "/")] - smtIntRealShared = [ (Plus, lift2WM "+") - , (Minus, lift2WM "-") - , (Times, lift2WM "*") + ++ [(Quot, lift2WM "/" "fp.div")] + smtIntRealShared = [ (Plus, lift2WM "+" "fp.add") + , (Minus, lift2WM "-" "fp.sub") + , (Times, lift2WM "*" "fp.mul") + , (UNeg, lift1FP "-" "fp.neg") + , (Abs, liftAbs) , (Equal, equal) , (NotEqual, notEqual) - , (LessThan, lift2S "<" "<") - , (GreaterThan, lift2S ">" ">") - , (LessEq, lift2S "<=" "<=") - , (GreaterEq, lift2S ">=" ">=") + , (LessThan, lift2Cmp "<" "fp.lt") + , (GreaterThan, lift2Cmp ">" "fp.gt") + , (LessEq, lift2Cmp "<=" "fp.leq") + , (GreaterEq, lift2Cmp ">=" "fp.geq") ] -- equality is the only thing that works on uninterpreted sorts uninterpretedTable = [ (Equal, lift2S "=" "=" True) diff --git a/SBVUnitTest/GoldFiles/temperature.gold b/SBVUnitTest/GoldFiles/temperature.gold --- a/SBVUnitTest/GoldFiles/temperature.gold +++ b/SBVUnitTest/GoldFiles/temperature.gold @@ -1,5 +1,5 @@ Solution #1: - s0 = 16 :: SInteger -Solution #2: s0 = 28 :: SInteger +Solution #2: + s0 = 16 :: SInteger Found 2 different solutions. diff --git a/SBVUnitTest/SBVUnitTestBuildTime.hs b/SBVUnitTest/SBVUnitTestBuildTime.hs --- a/SBVUnitTest/SBVUnitTestBuildTime.hs +++ b/SBVUnitTest/SBVUnitTestBuildTime.hs @@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String -buildTime = "Fri Dec 5 00:41:13 PST 2014" +buildTime = "Sun Dec 21 15:07:02 PST 2014" diff --git a/SBVUnitTest/TestSuite/Basics/ArithSolver.hs b/SBVUnitTest/TestSuite/Basics/ArithSolver.hs --- a/SBVUnitTest/TestSuite/Basics/ArithSolver.hs +++ b/SBVUnitTest/TestSuite/Basics/ArithSolver.hs @@ -218,20 +218,30 @@ genDoubles = genIEEE754 "genDoubles" ds genIEEE754 :: (RealFloat a, Show a, SymWord a, Ord a, Floating a) => String -> [a] -> [Test] -genIEEE754 origin vs = map mkTest $ [("+", show x, show y, mkThm2 (+) x y (x + y)) | x <- vs, y <- vs ] - ++ [("-", show x, show y, mkThm2 (-) x y (x - y)) | x <- vs, y <- vs ] - ++ [("*", show x, show y, mkThm2 (*) x y (x * y)) | x <- vs, y <- vs ] - ++ [("/", show x, show y, mkThm2 (/) x y (x / y)) | x <- vs, y <- vs, y /= 0] - ++ [("<", show x, show y, mkThm2C False (.<) x y (x < y)) | x <- vs, y <- vs ] - ++ [("<=", show x, show y, mkThm2C False (.<=) x y (x <= y)) | x <- vs, y <- vs ] - ++ [(">", show x, show y, mkThm2C False (.>) x y (x > y)) | x <- vs, y <- vs ] - ++ [(">=", show x, show y, mkThm2C False (.>=) x y (x >= y)) | x <- vs, y <- vs ] - ++ [("==", show x, show y, mkThm2C False (.==) x y (x == y)) | x <- vs, y <- vs ] - ++ [("/=", show x, show y, mkThm2C True (./=) x y (x /= y)) | x <- vs, y <- vs ] - where mkTest (nm, x, y, t) = origin ++ ".arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t +genIEEE754 origin vs = map tst1 uns ++ map tst2 bins + where uns = [("abs", show x, mkThm1 abs x (abs x)) | x <- vs] + ++ [("negate", show x, mkThm1 negate x (negate x)) | x <- vs] + ++ [("signum", show x, mkThm1 signum x (signum x)) | x <- tail vs] -- TODO: Remove tail, skipping over NaN due to GHC bug + bins = [("+", show x, show y, mkThm2 (+) x y (x + y)) | x <- vs, y <- vs ] + ++ [("-", show x, show y, mkThm2 (-) x y (x - y)) | x <- vs, y <- vs ] + ++ [("*", show x, show y, mkThm2 (*) x y (x * y)) | x <- vs, y <- vs ] + ++ [("/", show x, show y, mkThm2 (/) x y (x / y)) | x <- vs, y <- vs, y /= 0] + ++ [("<", show x, show y, mkThm2C False (.<) x y (x < y)) | x <- vs, y <- vs ] + ++ [("<=", show x, show y, mkThm2C False (.<=) x y (x <= y)) | x <- vs, y <- vs ] + ++ [(">", show x, show y, mkThm2C False (.>) x y (x > y)) | x <- vs, y <- vs ] + ++ [(">=", show x, show y, mkThm2C False (.>=) x y (x >= y)) | x <- vs, y <- vs ] + ++ [("==", show x, show y, mkThm2C False (.==) x y (x == y)) | x <- vs, y <- vs ] + ++ [("/=", show x, show y, mkThm2C True (./=) x y (x /= y)) | x <- vs, y <- vs ] + tst2 (nm, x, y, t) = origin ++ ".arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t + tst1 (nm, x, t) = origin ++ ".arithmetic-" ++ nm ++ "." ++ x ~: assert t eqF v val | isNaN val = constrain $ isSNaN v | True = constrain $ v .== literal val + mkThm1 op x r = isThm $ do a <- free "x" + eqF a x + return $ if isNaN r + then isSNaN (op a) + else literal r .== op a mkThm2 op x y r = isThm $ do [a, b] <- mapM free ["x", "y"] eqF a x eqF b y @@ -313,8 +323,8 @@ -- Admittedly paltry test-cases for float/double fs :: [Float] -fs = nan : -infinity : infinity : 0 : [-5.0, -4.7 .. 5] ++ [5] +fs = nan : -infinity : infinity : 0 : -0 : [-5.0, -4.1 .. 5] ++ [5] ds :: [Double] -ds = nan : -infinity : infinity : 0 : [-5.0, -4.7 .. 5] ++ [5] +ds = nan : -infinity : infinity : 0 : -0 : [-5.0, -4.1 .. 5] ++ [5] {-# ANN module "HLint: ignore Reduce duplication" #-} diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,5 +1,5 @@ Name: sbv -Version: 3.3 +Version: 3.4 Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description: Express properties about Haskell programs and automatically prove them using SMT