sbv 3.3 → 3.4
raw patch · 14 files changed
+160/−86 lines, 14 files
Files
- CHANGES.md +19/−1
- Data/SBV/BitVectors/Data.hs +5/−5
- Data/SBV/BitVectors/Model.hs +6/−3
- Data/SBV/BitVectors/PrettyNum.hs +10/−10
- Data/SBV/Compilers/C.hs +12/−6
- Data/SBV/Examples/Existentials/Diophantine.hs +1/−1
- Data/SBV/Examples/Misc/Floating.hs +21/−21
- Data/SBV/Provers/SExpr.hs +16/−4
- Data/SBV/SMT/SMTLib1.hs +8/−0
- Data/SBV/SMT/SMTLib2.hs +35/−18
- SBVUnitTest/GoldFiles/temperature.gold +2/−2
- SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
- SBVUnitTest/TestSuite/Basics/ArithSolver.hs +23/−13
- sbv.cabal +1/−1
CHANGES.md view
@@ -1,7 +1,25 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://leventerkok.github.com/sbv/> -* 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
Data/SBV/BitVectors/Data.hs view
@@ -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
Data/SBV/BitVectors/Model.hs view
@@ -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
Data/SBV/BitVectors/PrettyNum.hs view
@@ -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
Data/SBV/Compilers/C.hs view
@@ -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
Data/SBV/Examples/Existentials/Diophantine.hs view
@@ -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: --
Data/SBV/Examples/Misc/Floating.hs view
@@ -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
Data/SBV/Provers/SExpr.hs view
@@ -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.
Data/SBV/SMT/SMTLib1.hs view
@@ -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") ]
Data/SBV/SMT/SMTLib2.hs view
@@ -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)
SBVUnitTest/GoldFiles/temperature.gold view
@@ -1,5 +1,5 @@ Solution #1:- s0 = 16 :: SInteger-Solution #2: s0 = 28 :: SInteger+Solution #2:+ s0 = 16 :: SInteger Found 2 different solutions.
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -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"
SBVUnitTest/TestSuite/Basics/ArithSolver.hs view
@@ -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" #-}
sbv.cabal view
@@ -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