diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,58 @@ * Hackage: * GitHub: -* Latest Hackage released version: 5.0, 2015-09-22 +* Latest Hackage released version: 5.1, 2015-10-10 + +### Version 5.1, 2015-10-10 + + * fpMin, fpMax: If these functions receive +0/-0 as their two arguments, i.e., both + zeros but alternating signs in any order, then SMTLib requires the output to be + nondeterministicly chosen. Previously, we fixed this result as +0 following the + interpretation in Z3, but Z3 recently changed and now incorporates the nondeterministic + output. SBV similarly changed to allow for non-determinism here. + + * Change the types of the following Floating-point operations: + + * sFloatAsSWord32, sFloatAsSWord32, blastSFloat, blastSDouble + + These were previously coded as relations, since NaN values were not representable + in the target domain uniquely. While it was OK, it was hard to use them. We now + simply implement these as functions, and they are underspecified if the inputs + are NaNs: In those cases, we simply get a symbolic output. The new types are: + + * sFloatAsSWord32 :: SFloat -> SWord32 + * sDoubleAsSWord64 :: SDouble -> SWord64 + * blastSFloat :: SFloat -> (SBool, [SBool], [SBool]) + * blastSDouble :: SDouble -> (SBool, [SBool], [SBool]) + + * MathSAT backend: Use the SMTLib interpretation of fp.min/fp.max by passing the + "-theory.fp.minmax_zero_mode=4" argument explicitly. + + * Fix a bug in hash-consing of floating-point constants, where we were confusing +0 and + -0 since we were using them as keys into the map though they compare equal. We now + explicitly keep track of the negative-zero status to make sure this confusion does + not arise. Note that this bug only exhibited itself in rare occurrences of both + constants being present in a benchmark; a true corner case. Note that @NaN@ values + are also interesting in this context: Since NaN /= NaN, we never hash-cons floating + point constants that have the value NaN. But that is actually OK; it is a bit wasteful + in case you have a lot of NaN constants around, but there is no soundness issue: We + just waste a little bit of space. + + * Remove the functions `allSatWithAny` and `allSatWithAll`. These two variants do *not* + make sense when run with multiple solvers, as they internally sequentialize the solutions + due to the nature of `allSat`. Not really needed anyhow; so removed. The variants + `satWithAny/All` and `proveWithAny/All` are still available. + + * Export SMTLibVersion from the library, forgotten export needed by Cryptol. Thanks to Adam + Foltzer for the patch. + + * Slightly modify model-outputs so the variables are aligned vertically. (Only matters + if we have model-variable names that are of differing length.) + + * Move to Travis-CI "docker" based infrastructure for builds + + * Enable local builds to use the Herbie plugin. Currently SBV does not have any + expressions that can benefit from Herbie, but it is nice to have this support in general. ### Version 5.0, 2015-09-22 diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -207,7 +207,7 @@ -- * Proving properties using multiple solvers -- $multiIntro - , proveWithAll, proveWithAny, satWithAll, satWithAny, allSatWithAll, allSatWithAny + , proveWithAll, proveWithAny, satWithAll, satWithAny -- * Optimization -- $optimizeIntro @@ -230,7 +230,7 @@ , getModelDictionaries, getModelValues, getModelUninterpretedValues -- * SMT Interface: Configurations and solvers - , SMTConfig(..), SMTLibLogic(..), Logic(..), OptimizeOpts(..), Solver(..), SMTSolver(..), boolector, cvc4, yices, z3, mathSAT, abc, defaultSolverConfig, sbvCurrentSolver, defaultSMTCfg, sbvCheckSolverInstallation, sbvAvailableSolvers + , SMTConfig(..), SMTLibVersion(..), SMTLibLogic(..), Logic(..), OptimizeOpts(..), Solver(..), SMTSolver(..), boolector, cvc4, yices, z3, mathSAT, abc, defaultSolverConfig, sbvCurrentSolver, defaultSMTCfg, sbvCheckSolverInstallation, sbvAvailableSolvers -- * Symbolic computations , Symbolic, output, SymWord(..) @@ -371,16 +371,6 @@ satWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, SatResult) satWithAny = (`sbvWithAny` satWith) --- | Find all satisfying assignments to a property with multiple solvers, running them in separate threads. Only --- the result of the first one to finish will be returned, remaining threads will be killed. -allSatWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, AllSatResult)] -allSatWithAll = (`sbvWithAll` allSatWith) - --- | Find all satisfying assignments to a property with multiple solvers, running them in separate threads. Only --- the result of the first one to finish will be returned, remaining threads will be killed. -allSatWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, AllSatResult) -allSatWithAny = (`sbvWithAny` allSatWith) - -- | Equality as a proof method. Allows for -- very concise construction of equivalence proofs, which is very typical in -- bit-precise proofs. @@ -471,13 +461,13 @@ backends at the same time. Each function comes in two variants, one that returns the results from all solvers, the other that returns the fastest one. -The @All@ variants, (i.e., 'proveWithAll', 'satWithAll', 'allSatWithAll') run all solvers and +The @All@ variants, (i.e., 'proveWithAll', 'satWithAll') run all solvers and return all the results. SBV internally makes sure that the result is lazily generated; so, the order of solvers given does not matter. In other words, the order of results will follow the order of the solvers as they finish, not as given by the user. These variants are useful when you want to make sure multiple-solvers agree (or disagree!) on a given problem. -The @Any@ variants, (i.e., 'proveWithAny', 'satWithAny', 'allSatWithAny') will run all the solvers +The @Any@ variants, (i.e., 'proveWithAny', 'satWithAny') will run all the solvers in parallel, and return the results of the first one finishing. The other threads will then be killed. These variants are useful when you do not care if the solvers produce the same result, but rather want to get the solution as quickly as possible, taking advantage of modern many-core machines. 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 @@ -38,7 +38,7 @@ , SBVPgm(..), Symbolic, runSymbolic, runSymbolic', State, getPathCondition, extendPathCondition , inProofMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..) , Logic(..), SMTLibLogic(..) - , getTraceInfo, getConstraints, addConstraint + , getTraceInfo, getConstraints, addConstraint, internalVariable, internalConstraint, isCodeGenMode , SBVType(..), newUninterpreted, addAxiom , Quantifier(..), needsExistentials , SMTLibPgm(..), SMTLibVersion(..), smtLibVersionExtension diff --git a/Data/SBV/BitVectors/Floating.hs b/Data/SBV/BitVectors/Floating.hs --- a/Data/SBV/BitVectors/Floating.hs +++ b/Data/SBV/BitVectors/Floating.hs @@ -121,8 +121,8 @@ fpSqrt = lift1 FP_Sqrt (Just sqrt) . Just fpRem = lift2 FP_Rem (Just fpRemH) Nothing fpRoundToIntegral = lift1 FP_RoundToIntegral (Just fpRoundToIntegralH) . Just - fpMin = lift2 FP_Min (Just fpMinH) Nothing - fpMax = lift2 FP_Max (Just fpMaxH) Nothing + fpMin = liftMM FP_Min (Just fpMinH) Nothing + fpMax = liftMM FP_Max (Just fpMaxH) Nothing fpIsEqualObject = lift2B FP_ObjEqual (Just fpIsEqualObjectH) Nothing fpIsNormal = lift1B FP_IsNormal fpIsNormalizedH fpIsSubnormal = lift1B FP_IsSubnormal isDenormalized @@ -325,6 +325,25 @@ args <- addRM st mbRm [swa, swb] newExpr st k (SBVApp (IEEEFP w) args) +-- | Lift min/max: Note that we protect against constant folding if args are alternating sign 0's, since +-- SMTLib is deliberately nondeterministic in this case +liftMM :: (SymWord a, RealFloat a) => FPOp -> Maybe (a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a +liftMM w mbOp mbRm a b + | Just v1 <- unliteral a + , Just v2 <- unliteral b + , not ((isN0 v1 && isP0 v2) || (isP0 v1 && isN0 v2)) -- If not +0/-0 or -0/+0 + , Just cv <- concEval2 mbOp mbRm a b + = cv + | True + = SBV $ SVal k $ Right $ cache r + where isN0 = isNegativeZero + isP0 x = x == 0 && not (isN0 x) + k = kindOf a + r st = do swa <- sbvToSW st a + swb <- sbvToSW st b + args <- addRM st mbRm [swa, swb] + newExpr st k (SBVApp (IEEEFP w) args) + -- | Lift a 2 arg FP-op, producing bool lift2B :: (SymWord a, Floating a) => FPOp -> Maybe (a -> a -> Bool) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBool lift2B w mbOp mbRm a b @@ -351,51 +370,62 @@ args <- addRM st mbRm [swa, swb, swc] newExpr st k (SBVApp (IEEEFP w) args) --- | Relationally assert the equivalence between an 'SFloat' and an 'SWord32', when the bit-pattern --- is interpreted as either type. Useful when analyzing components of a floating point number. Note --- that this cannot be written as a function, since IEEE754 NaN values are not unique. That is, --- given a float, there isn't a unique sign/mantissa/exponent that we can match it to. --- --- The use case would be code of the form: --- --- @ --- do w <- free_ --- constrain $ sFloatToSWord32 f w --- ... --- @ +-- | Convert an 'SFloat' to an 'SWord32', preserving the bit-correspondence. Note that since the +-- representation for @NaN@s are not unique, this function will return a symbolic value when given a +-- concrete @NaN@. -- --- At which point the variable @w@ can be used to access the bits of the float 'f'. -sFloatAsSWord32 :: SFloat -> SWord32 -> SBool -sFloatAsSWord32 fVal wVal - | Just f <- unliteral fVal, not (isNaN f) = wVal .== literal (DB.floatToWord f) - | True = fVal `fpIsEqualObject` sWord32AsSFloat wVal +-- Implementation note: Since there's no corresponding function in SMTLib for conversion to +-- bit-representation due to partiality, we use a translation trick by allocating a new word variable, +-- converting it to float, and requiring it to be equivalent to the input. In code-generation mode, we simply map +-- it to a simple conversion. +sFloatAsSWord32 :: SFloat -> SWord32 +sFloatAsSWord32 fVal + | Just f <- unliteral fVal, not (isNaN f) + = literal (DB.floatToWord f) + | True + = SBV (SVal w32 (Right (cache y))) + where w32 = KBounded False 32 + y st | isCodeGenMode st + = do f <- sbvToSW st fVal + newExpr st w32 (SBVApp (IEEEFP (FP_Reinterpret KFloat w32)) [f]) + | True + = do n <- internalVariable st w32 + ysw <- newExpr st KFloat (SBVApp (IEEEFP (FP_Reinterpret w32 KFloat)) [n]) + internalConstraint st $ unSBV $ fVal `fpIsEqualObject` SBV (SVal KFloat (Right (cache (\_ -> return ysw)))) + return n --- | Relationally assert the equivalence between an 'SDouble' and an 'SWord64', when the bit-pattern --- is interpreted as either type. See the comments for 'sFloatToSWord32' for details. -sDoubleAsSWord64 :: SDouble -> SWord64 -> SBool -sDoubleAsSWord64 fVal wVal - | Just f <- unliteral fVal, not (isNaN f) = wVal .== literal (DB.doubleToWord f) - | True = fVal `fpIsEqualObject` sWord64AsSDouble wVal +-- | Convert an 'SDouble' to an 'SWord64', preserving the bit-correspondence. Note that since the +-- representation for @NaN@s are not unique, this function will return a symbolic value when given a +-- concrete @NaN@. +-- +-- See the implementation note for 'sFloatAsSWord32', as it applies here as well. +sDoubleAsSWord64 :: SDouble -> SWord64 +sDoubleAsSWord64 fVal + | Just f <- unliteral fVal, not (isNaN f) + = literal (DB.doubleToWord f) + | True + = SBV (SVal w64 (Right (cache y))) + where w64 = KBounded False 64 + y st | isCodeGenMode st + = do f <- sbvToSW st fVal + newExpr st w64 (SBVApp (IEEEFP (FP_Reinterpret KDouble w64)) [f]) + | True + = do n <- internalVariable st w64 + ysw <- newExpr st KDouble (SBVApp (IEEEFP (FP_Reinterpret w64 KDouble)) [n]) + internalConstraint st $ unSBV $ fVal `fpIsEqualObject` SBV (SVal KDouble (Right (cache (\_ -> return ysw)))) + return n --- | Relationally extract the sign\/exponent\/mantissa of a single-precision float. Due to the --- non-unique representation of NaN's, we have to do this relationally, much like --- 'sFloatAsSWord32'. -blastSFloat :: SFloat -> (SBool, [SBool], [SBool]) -> SBool -blastSFloat fVal (s, expt, mant) - | length expt /= 8 || length mant /= 23 = error "SBV.blastSFloat: Need 8-bit expt and 23 bit mantissa" - | True = sFloatAsSWord32 fVal wVal - where bits = s : expt ++ mant - wVal = sum [ite b (2^c) 0 | (b, c) <- zip bits (reverse [(0::Word32) .. 31])] +-- | Extract the sign\/exponent\/mantissa of a single-precision float. The output will have +-- 8 bits in the second argument for exponent, and 23 in the third for the mantissa. +blastSFloat :: SFloat -> (SBool, [SBool], [SBool]) +blastSFloat = extract . sFloatAsSWord32 + where extract x = (sTestBit x 31, sExtractBits x [30, 29 .. 23], sExtractBits x [22, 21 .. 0]) --- | Relationally extract the sign\/exponent\/mantissa of a double-precision float. Due to the --- non-unique representation of NaN's, we have to do this relationally, much like --- 'sDoubleAsSWord64'. -blastSDouble :: SDouble -> (SBool, [SBool], [SBool]) -> SBool -blastSDouble fVal (s, expt, mant) - | length expt /= 11 || length mant /= 52 = error "SBV.blastSDouble: Need 11-bit expt and 52 bit mantissa" - | True = sDoubleAsSWord64 fVal wVal - where bits = s : expt ++ mant - wVal = sum [ite b (2^c) 0 | (b, c) <- zip bits (reverse [(0::Word64) .. 63])] +-- | Extract the sign\/exponent\/mantissa of a single-precision float. The output will have +-- 11 bits in the second argument for exponent, and 52 in the third for the mantissa. +blastSDouble :: SDouble -> (SBool, [SBool], [SBool]) +blastSDouble = extract . sDoubleAsSWord64 + where extract x = (sTestBit x 63, sExtractBits x [62, 61 .. 52], sExtractBits x [51, 50 .. 0]) -- | Reinterpret the bits in a 32-bit word as a single-precision floating point number sWord32AsSFloat :: SWord32 -> SFloat diff --git a/Data/SBV/BitVectors/Symbolic.hs b/Data/SBV/BitVectors/Symbolic.hs --- a/Data/SBV/BitVectors/Symbolic.hs +++ b/Data/SBV/BitVectors/Symbolic.hs @@ -33,7 +33,7 @@ , svMkSymVar , ArrayContext(..), ArrayInfo , svToSW, svToSymSW, forceSWArg - , SBVExpr(..), newExpr + , SBVExpr(..), newExpr, isCodeGenMode , Cached, cache, uncache , ArrayIndex, uncacheAI , NamedSymVar @@ -43,7 +43,7 @@ , inProofMode, SBVRunMode(..), Result(..) , Logic(..), SMTLibLogic(..) , getTraceInfo, getConstraints - , addSValConstraint + , addSValConstraint, internalConstraint, internalVariable , SMTLibPgm(..), SMTLibVersion(..), smtLibVersionExtension , SolverCapabilities(..) , extractSymbolicSimulationState @@ -356,8 +356,8 @@ -- | Expression map, used for hash-consing type ExprMap = Map.Map SBVExpr SW --- | Constants are stored in a map, for hash-consing -type CnstMap = Map.Map CW SW +-- | Constants are stored in a map, for hash-consing. The bool is needed to tell -0 from +0, sigh +type CnstMap = Map.Map (Bool, CW) SW -- | Kinds used in the program; used for determining the final SMT-Lib logic to pick type KindSet = Set.Set Kind @@ -386,11 +386,19 @@ | Concrete StdGen -- ^ Concrete simulation mode. The StdGen is for the pConstrain acceptance in cross runs. -- | Is this a concrete run? (i.e., quick-check or test-generation like) -isConcreteMode :: SBVRunMode -> Bool -isConcreteMode (Concrete _) = True -isConcreteMode (Proof{}) = False -isConcreteMode CodeGen = False +isConcreteMode :: State -> Bool +isConcreteMode State{runMode} = case runMode of + Concrete{} -> True + Proof{} -> False + CodeGen -> False +-- | Is this a CodeGen run? (i.e., generating code) +isCodeGenMode :: State -> Bool +isCodeGenMode State{runMode} = case runMode of + Concrete{} -> False + Proof{} -> False + CodeGen -> True + -- | The state of the symbolic interpreter data State = State { runMode :: SBVRunMode , pathCond :: SVal -- ^ kind KBool @@ -501,6 +509,18 @@ when (isJust mbCode) $ modifyIORef (rCgMap st) (Map.insert nm (fromJust mbCode)) where validChar x = isAlphaNum x || x `elem` "_" +-- | Create an internal variable, which acts as an input but isn't visible to the user. +-- Such variables are existentially quantified in a SAT context, and universally quantified +-- in a proof context. +internalVariable :: State -> Kind -> IO SW +internalVariable st k = do (sw, nm) <- newSW st k + let q = case runMode st of + Proof (True, _) -> EX + _ -> ALL + modifyIORef (rinps st) ((q, (sw, "__internal_sbv_" ++ nm)):) + return sw +{-# INLINE internalVariable #-} + -- | Create a new SW newSW :: State -> Kind -> IO (SW, String) newSW st k = do ctr <- incCtr st @@ -521,15 +541,23 @@ reserved = ["Int", "Real", "List", "Array", "Bool", "NUMERAL", "DECIMAL", "STRING", "FP", "FloatingPoint", "fp"] -- Reserved by SMT-Lib -- | Create a new constant; hash-cons as necessary +-- NB. For each constant, we also store weather it's negative-0 or not, +-- as otherwise +0 == -0 and thus we'd confuse those entries. That's a +-- bummer as we incur an extra boolean for this rare case, but it's simple +-- and hopefully we don't generate a ton of constants in general. newConst :: State -> CW -> IO SW newConst st c = do constMap <- readIORef (rconstMap st) - case c `Map.lookup` constMap of + let key = (isNeg0 (cwVal c), c) + case key `Map.lookup` constMap of Just sw -> return sw Nothing -> do let k = cwKind c (sw, _) <- newSW st k - modifyIORef (rconstMap st) (Map.insert c sw) + modifyIORef (rconstMap st) (Map.insert key sw) return sw + where isNeg0 (CWFloat f) = isNegativeZero f + isNeg0 (CWDouble d) = isNegativeZero d + isNeg0 _ = False {-# INLINE newConst #-} -- | Create a new table; hash-cons as necessary @@ -690,9 +718,10 @@ SBVPgm rpgm <- readIORef pgm inpsO <- reverse `fmap` readIORef inps outsO <- reverse `fmap` readIORef outs - let swap (a, b) = (b, a) - cmp (a, _) (b, _) = a `compare` b - cnsts <- (sortBy cmp . map swap . Map.toList) `fmap` readIORef (rconstMap st) + let swap (a, b) = (b, a) + swapc ((_, a), b) = (b, a) + cmp (a, _) (b, _) = a `compare` b + cnsts <- (sortBy cmp . map swapc . Map.toList) `fmap` readIORef (rconstMap st) tbls <- (sortBy (\((x, _, _), _) ((y, _, _), _) -> x `compare` y) . map swap . Map.toList) `fmap` readIORef tables arrs <- IMap.toAscList `fmap` readIORef arrays unint <- Map.toList `fmap` readIORef uis @@ -708,9 +737,13 @@ imposeConstraint c = do st <- ask case runMode st of CodeGen -> error "SBV: constraints are not allowed in code-generation" - _ -> liftIO $ do v <- svToSW st c - modifyIORef (rConstraints st) (v:) + _ -> liftIO $ internalConstraint st c +-- | Require a boolean condition to be true in the state. Only used for internal purposes. +internalConstraint :: State -> SVal -> IO () +internalConstraint st b = do v <- svToSW st b + modifyIORef (rConstraints st) (v:) + -- | Add a constraint with a given probability addSValConstraint :: Maybe Double -> SVal -> SVal -> Symbolic () addSValConstraint Nothing c _ = imposeConstraint c @@ -719,7 +752,7 @@ = error $ "SBV: pConstrain: Invalid probability threshold: " ++ show t ++ ", must be in [0, 1]." | True = do st <- ask - unless (isConcreteMode (runMode st)) $ error "SBV: pConstrain only allowed in 'genTest' or 'quickCheck' contexts." + unless (isConcreteMode st) $ error "SBV: pConstrain only allowed in 'genTest' or 'quickCheck' contexts." case () of () | t > 0 && t < 1 -> liftIO (throwDice st) >>= \d -> imposeConstraint (if d <= t then c else c') | t > 0 -> imposeConstraint c 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 @@ -515,6 +515,8 @@ cvt (FP_Reinterpret f t) = case (f, t) of (KBounded False 32, KFloat) -> cast $ cpy "sizeof(SFloat)" (KBounded False 64, KDouble) -> cast $ cpy "sizeof(SDouble)" + (KFloat, KBounded False 32) -> cast $ cpy "sizeof(SWord32)" + (KDouble, KBounded False 64) -> cast $ cpy "sizeof(SWord64)" _ -> die $ "Reinterpretation from : " ++ show f ++ " to " ++ show t where cpy sz = \[a] -> let alhs = text "&" <> var arhs = text "&" <> a @@ -576,8 +578,10 @@ dispatch (fOp, dOp) = pickOp (fOp, dOp) fpArgs cast f = f (map snd fpArgs) - -- In SMT-Lib, fpMin/fpMax return +0 when given +0/-0 as the two arguments. (In any order.) - -- In C, the second argument is returned. So, wrap around an if-then-else to avoid discrepancy: + -- In SMT-Lib, fpMin/fpMax is underspecified when given +0/-0 as the two arguments. (In any order.) + -- In C, the second argument is returned. (I think, might depend on the architecture, optimizations etc.). + -- We'll translate it so that we deterministically return +0. + -- There's really no good choice here. wrapMinMax k a b s = parens cond <+> text "?" <+> zero <+> text ":" <+> s where zero = text $ if k == KFloat then showCFloat 0 else showCDouble 0 cond = parens (text "FP_ZERO == fpclassify" <> parens a) -- a is zero diff --git a/Data/SBV/Dynamic.hs b/Data/SBV/Dynamic.hs --- a/Data/SBV/Dynamic.hs +++ b/Data/SBV/Dynamic.hs @@ -64,7 +64,7 @@ -- ** Checking satisfiability , satWith -- * Proving properties using multiple solvers - , proveWithAll, proveWithAny, satWithAll, satWithAny, allSatWithAll, allSatWithAny + , proveWithAll, proveWithAny, satWithAll, satWithAny -- * Model extraction -- ** Inspecting proof results @@ -73,7 +73,7 @@ -- ** Programmable model extraction , genParse, getModel, getModelDictionary -- * SMT Interface: Configurations and solvers - , SMTConfig(..), SMTLibLogic(..), Logic(..), OptimizeOpts(..), Solver(..), SMTSolver(..), boolector, cvc4, yices, z3, mathSAT, abc, defaultSolverConfig, sbvCurrentSolver, defaultSMTCfg, sbvCheckSolverInstallation, sbvAvailableSolvers + , SMTConfig(..), SMTLibVersion(..), SMTLibLogic(..), Logic(..), OptimizeOpts(..), Solver(..), SMTSolver(..), boolector, cvc4, yices, z3, mathSAT, abc, defaultSolverConfig, sbvCurrentSolver, defaultSMTCfg, sbvCheckSolverInstallation, sbvAvailableSolvers -- * Symbolic computations , outputSVal{-, SymWord(..)-} @@ -127,7 +127,7 @@ import Data.SBV.Tools.Optimize (OptimizeOpts(..)) import Data.SBV (sbvCurrentSolver, sbvCheckSolverInstallation, defaultSolverConfig, sbvAvailableSolvers) -import qualified Data.SBV as SBV (SBool, proveWithAll, proveWithAny, satWithAll, satWithAny, allSatWithAll, allSatWithAny) +import qualified Data.SBV as SBV (SBool, proveWithAll, proveWithAny, satWithAll, satWithAny) import qualified Data.SBV.BitVectors.Data as SBV (SBV(..)) import qualified Data.SBV.BitVectors.Model as SBV (isSatisfiableInCurrentPath) import qualified Data.SBV.Provers.Prover as SBV (proveWith, satWith, compileToSMTLib, generateSMTBenchmarks) @@ -193,20 +193,6 @@ -- to finish will be returned, remaining threads will be killed. satWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, SatResult) satWithAny cfgs s = SBV.satWithAny cfgs (fmap toSBool s) - --- | Find all satisfying assignments to a property with multiple --- solvers, running them in separate threads. Only the result of the --- first one to finish will be returned, remaining threads will be --- killed. -allSatWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, AllSatResult)] -allSatWithAll cfgs s = SBV.allSatWithAll cfgs (fmap toSBool s) - --- | Find all satisfying assignments to a property with multiple --- solvers, running them in separate threads. Only the result of the --- first one to finish will be returned, remaining threads will be --- killed. -allSatWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, AllSatResult) -allSatWithAny cfgs s = SBV.allSatWithAny cfgs (fmap toSBool s) -- | Extract a model, the result is a tuple where the first argument (if True) -- indicates whether the model was "probable". (i.e., if the solver returned unknown.) 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 @@ -146,8 +146,8 @@ -- >>> roundingAdd -- Satisfiable. Model: -- rm = RoundNearestTiesToAway :: RoundingMode --- x = 2.0644195e19 :: Float --- y = -2.1974389e18 :: Float +-- x = 2.0644195e19 :: Float +-- y = -2.1974389e18 :: Float -- -- Unfortunately we can't directly validate this result at the Haskell level, as Haskell only supports -- 'RoundNearestTiesToEven'. We have: diff --git a/Data/SBV/Examples/Puzzles/Birthday.hs b/Data/SBV/Examples/Puzzles/Birthday.hs --- a/Data/SBV/Examples/Puzzles/Birthday.hs +++ b/Data/SBV/Examples/Puzzles/Birthday.hs @@ -138,7 +138,7 @@ -- -- >>> cheryl -- Solution #1: --- birthDay = 16 :: Word8 +-- birthDay = 16 :: Word8 -- birthMonth = 7 :: Word8 -- This is the only solution. cheryl :: IO () diff --git a/Data/SBV/Examples/Puzzles/DogCatMouse.hs b/Data/SBV/Examples/Puzzles/DogCatMouse.hs --- a/Data/SBV/Examples/Puzzles/DogCatMouse.hs +++ b/Data/SBV/Examples/Puzzles/DogCatMouse.hs @@ -21,8 +21,8 @@ -- -- >>> puzzle -- Solution #1: --- dog = 3 :: Integer --- cat = 41 :: Integer +-- dog = 3 :: Integer +-- cat = 41 :: Integer -- mouse = 56 :: Integer -- This is the only solution. puzzle :: IO AllSatResult diff --git a/Data/SBV/Examples/Uninterpreted/UISortAllSat.hs b/Data/SBV/Examples/Uninterpreted/UISortAllSat.hs --- a/Data/SBV/Examples/Uninterpreted/UISortAllSat.hs +++ b/Data/SBV/Examples/Uninterpreted/UISortAllSat.hs @@ -51,17 +51,17 @@ -- -- >>> genLs -- Solution #1: --- l = L!val!0 :: L +-- l = L!val!0 :: L -- l0 = L!val!0 :: L -- l1 = L!val!1 :: L -- l2 = L!val!2 :: L -- Solution #2: --- l = L!val!2 :: L +-- l = L!val!2 :: L -- l0 = L!val!0 :: L -- l1 = L!val!1 :: L -- l2 = L!val!2 :: L -- Solution #3: --- l = L!val!1 :: L +-- l = L!val!1 :: L -- l0 = L!val!0 :: L -- l1 = L!val!1 :: L -- l2 = L!val!2 :: L diff --git a/Data/SBV/Provers/MathSAT.hs b/Data/SBV/Provers/MathSAT.hs --- a/Data/SBV/Provers/MathSAT.hs +++ b/Data/SBV/Provers/MathSAT.hs @@ -23,7 +23,7 @@ mathSAT = SMTSolver { name = MathSAT , executable = "mathsat" - , options = ["-input=smt2"] + , options = ["-input=smt2", "-theory.fp.minmax_zero_mode=4"] , engine = standardEngine "SBV_MATHSAT" "SBV_MATHSAT_OPTIONS" addTimeOut standardModel , capabilities = SolverCapabilities { capSolverName = "MathSAT" diff --git a/Data/SBV/Provers/Z3.hs b/Data/SBV/Provers/Z3.hs --- a/Data/SBV/Provers/Z3.hs +++ b/Data/SBV/Provers/Z3.hs @@ -86,7 +86,7 @@ extractMap :: Bool -> [(Quantifier, NamedSymVar)] -> [String] -> SMTModel extractMap isSat qinps solverLines = - SMTModel { modelAssocs = map snd $ squashReals $ sortByNodeId $ concatMap (interpretSolverModelLine inps) solverLines } + SMTModel { modelAssocs = map snd $ squashReals $ sortByNodeId $ concatMap (interpretSolverModelLine inps) solverLines } where sortByNodeId :: [(Int, a)] -> [(Int, a)] sortByNodeId = sortBy (compare `on` fst) inps -- for "sat", display the prefix existentials. For completeness, we will drop diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs --- a/Data/SBV/SMT/SMT.hs +++ b/Data/SBV/SMT/SMT.hs @@ -333,10 +333,15 @@ TimeOut _ -> "*** Timeout" where cfg = resultConfig result --- | Show a model in human readable form +-- | Show a model in human readable form. Ignore bindings to those variables that start +-- with "__internal_sbv_"; as these are only for internal purposes showModel :: SMTConfig -> SMTModel -> String -showModel cfg m = intercalate "\n" $ map shM $ modelAssocs m - where shM (s, v) = " " ++ s ++ " = " ++ shCW cfg v +showModel cfg m = intercalate "\n" $ map shM interesting + where interesting = filter (not . ignore) $ modelAssocs m + ignore (s, _) = "__internal_sbv_" `isPrefixOf` s + width = maximum (0 : map (length . fst) interesting) + shM (s, v) = " " ++ align s ++ " = " ++ shCW cfg v + align s = s ++ replicate (width - length s) ' ' -- | Show a constant value, in the user-specified base shCW :: SMTConfig -> CW -> String diff --git a/Data/SBV/Utils/Numeric.hs b/Data/SBV/Utils/Numeric.hs --- a/Data/SBV/Utils/Numeric.hs +++ b/Data/SBV/Utils/Numeric.hs @@ -29,25 +29,27 @@ -- -- So, we codify here what the Z3 (SMTLib) is implementing for fpMax. -- The discrepancy with Haskell is that the NaN propagation doesn't work in Haskell --- The discrepancy with x86 is that given +0/-0, x86 returns the second argument; SMTLib returns +0 +-- The discrepancy with x86 is that given +0/-0, x86 returns the second argument; SMTLib is non-deterministic fpMaxH :: RealFloat a => a -> a -> a fpMaxH x y - | isNaN x = y - | isNaN y = x - | isNegativeZero x && isNegativeZero y = -0.0 - | (x == 0) && (y == 0) = 0.0 -- Corresponds to SMTLib. For x86 semantics, we'd return 'y' here. (Matters when x=+0, y=-0 or vice versa) - | x > y = x - | True = y + | isNaN x = y + | isNaN y = x + | (isN0 x && isP0 y) || (isN0 y && isP0 x) = error "fpMaxH: Called with alternating-sign 0's. Not supported" + | x > y = x + | True = y + where isN0 = isNegativeZero + isP0 a = a == 0 && not (isN0 a) -- | SMTLib compliant definition for 'fpMin'. See the comments for 'fpMax'. fpMinH :: RealFloat a => a -> a -> a fpMinH x y - | isNaN x = y - | isNaN y = x - | isNegativeZero x && isNegativeZero y = -0.0 - | (x == y) && (y == 0) = 0.0 -- Corresponds to SMTLib. For x86 semantics, we'd return 'y' here. (Matters when x=+0, y=-0 or vice versa) - | x < y = x - | True = y + | isNaN x = y + | isNaN y = x + | (isN0 x && isP0 y) || (isN0 y && isP0 x) = error "fpMinH: Called with alternating-sign 0's. Not supported" + | x < y = x + | True = y + where isN0 = isNegativeZero + isP0 a = a == 0 && not (isN0 a) -- | Convert double to float and back. Essentially @fromRational . toRational@ -- except careful on NaN, Infinities, and -0. diff --git a/SBVUnitTest/Examples/Basics/BasicTests.hs b/SBVUnitTest/Examples/Basics/BasicTests.hs --- a/SBVUnitTest/Examples/Basics/BasicTests.hs +++ b/SBVUnitTest/Examples/Basics/BasicTests.hs @@ -45,3 +45,7 @@ f3 x y = (x+y)*(x+y) f4 x y = let z = x + y in z * z f5 x _ = x + 1 + +{-# ANN f1 "NoHerbie" #-} +{-# ANN f2 "NoHerbie" #-} +{-# ANN f3 "NoHerbie" #-} diff --git a/SBVUnitTest/Examples/Basics/ProofTests.hs b/SBVUnitTest/Examples/Basics/ProofTests.hs --- a/SBVUnitTest/Examples/Basics/ProofTests.hs +++ b/SBVUnitTest/Examples/Basics/ProofTests.hs @@ -45,3 +45,8 @@ print =<< sat (do x <- exists "x" y <- exists "y" return $ f1 x y .== f3 x (y:: SWord8)) -- yes, 0;0 + +{-# ANN f1 "NoHerbie" #-} +{-# ANN f2 "NoHerbie" #-} +{-# ANN f3 "NoHerbie" #-} +{-# ANN f4 "NoHerbie" #-} diff --git a/SBVUnitTest/GoldFiles/U2Bridge.gold b/SBVUnitTest/GoldFiles/U2Bridge.gold --- a/SBVUnitTest/GoldFiles/U2Bridge.gold +++ b/SBVUnitTest/GoldFiles/U2Bridge.gold @@ -1,14 +1,14 @@ Satisfiable. Model: - s0 = False - s1 = Edge :: U2Member - s2 = Bono :: U2Member - s3 = True - s4 = Edge :: U2Member - s5 = Bono :: U2Member - s6 = False - s7 = Larry :: U2Member - s8 = Adam :: U2Member - s9 = True + s0 = False + s1 = Edge :: U2Member + s2 = Bono :: U2Member + s3 = True + s4 = Edge :: U2Member + s5 = Bono :: U2Member + s6 = False + s7 = Larry :: U2Member + s8 = Adam :: U2Member + s9 = True s10 = Bono :: U2Member s11 = Bono :: U2Member s12 = False diff --git a/SBVUnitTest/GoldFiles/dogCatMouse.gold b/SBVUnitTest/GoldFiles/dogCatMouse.gold --- a/SBVUnitTest/GoldFiles/dogCatMouse.gold +++ b/SBVUnitTest/GoldFiles/dogCatMouse.gold @@ -1,5 +1,5 @@ Solution #1: - dog = 3 :: Integer - cat = 41 :: Integer + dog = 3 :: Integer + cat = 41 :: Integer mouse = 56 :: Integer This is the only solution. diff --git a/SBVUnitTest/GoldFiles/euler185.gold b/SBVUnitTest/GoldFiles/euler185.gold --- a/SBVUnitTest/GoldFiles/euler185.gold +++ b/SBVUnitTest/GoldFiles/euler185.gold @@ -1,14 +1,14 @@ Solution #1: - s0 = 4 :: Word8 - s1 = 6 :: Word8 - s2 = 4 :: Word8 - s3 = 0 :: Word8 - s4 = 2 :: Word8 - s5 = 6 :: Word8 - s6 = 1 :: Word8 - s7 = 5 :: Word8 - s8 = 7 :: Word8 - s9 = 1 :: Word8 + s0 = 4 :: Word8 + s1 = 6 :: Word8 + s2 = 4 :: Word8 + s3 = 0 :: Word8 + s4 = 2 :: Word8 + s5 = 6 :: Word8 + s6 = 1 :: Word8 + s7 = 5 :: Word8 + s8 = 7 :: Word8 + s9 = 1 :: Word8 s10 = 8 :: Word8 s11 = 4 :: Word8 s12 = 9 :: Word8 diff --git a/SBVUnitTest/GoldFiles/floats_cgen.gold b/SBVUnitTest/GoldFiles/floats_cgen.gold --- a/SBVUnitTest/GoldFiles/floats_cgen.gold +++ b/SBVUnitTest/GoldFiles/floats_cgen.gold @@ -745,14 +745,12 @@ #include "floatCodeGen.h" -SBool fromFP_SFloat_SWord32(const SFloat a, const SWord32 b) +SWord32 fromFP_SFloat_SWord32(const SFloat a) { const SFloat s0 = a; - const SWord32 s1 = b; - SFloat s2; memcpy(&s2, &s1, sizeof(SFloat)); - const SBool s3 = isnan(s0) ? isnan(s2) : (signbit(s0) && (s0 == 0)) ? (signbit(s2) && (s2 == 0)) : (signbit(s2) && (s2 == 0)) ? (signbit(s0) && (s0 == 0)) : (s0 == s2); + SWord32 s1; memcpy(&s1, &s0, sizeof(SWord32)); - return s3; + return s1; } == END: "fromFP_SFloat_SWord32.c" ================== == BEGIN: "fromFP_SDouble_SWord64.c" ================ @@ -760,14 +758,12 @@ #include "floatCodeGen.h" -SBool fromFP_SDouble_SWord64(const SDouble a, const SWord64 b) +SWord64 fromFP_SDouble_SWord64(const SDouble a) { const SDouble s0 = a; - const SWord64 s1 = b; - SDouble s2; memcpy(&s2, &s1, sizeof(SDouble)); - const SBool s3 = isnan(s0) ? isnan(s2) : (signbit(s0) && (s0 == 0)) ? (signbit(s2) && (s2 == 0)) : (signbit(s2) && (s2 == 0)) ? (signbit(s0) && (s0 == 0)) : (s0 == s2); + SWord64 s1; memcpy(&s1, &s0, sizeof(SWord64)); - return s3; + return s1; } == END: "fromFP_SDouble_SWord64.c" ================== == BEGIN: "f_FP_Abs.c" ================ @@ -1406,8 +1402,8 @@ SReal fromFP_DoubleTo_Real(const SDouble a); SFloat fromFP_SWord32_SFloat(const SWord32 a); SDouble fromFP_SWord64_SDouble(const SWord64 a); -SBool fromFP_SFloat_SWord32(const SFloat a, const SWord32 b); -SBool fromFP_SDouble_SWord64(const SDouble a, const SWord64 b); +SWord32 fromFP_SFloat_SWord32(const SFloat a); +SWord64 fromFP_SDouble_SWord64(const SDouble a); SFloat f_FP_Abs(const SFloat a); SDouble d_FP_Abs(const SDouble a); SFloat f_FP_Neg(const SFloat a); @@ -1811,18 +1807,16 @@ void fromFP_SFloat_SWord32_driver(void) { - const SBool __result = fromFP_SFloat_SWord32(42.0F, - 0x0000002bUL); + const SWord32 __result = fromFP_SFloat_SWord32(42.0F); - printf("fromFP_SFloat_SWord32(42.0F, 0x0000002bUL) = %d\n", __result); + printf("fromFP_SFloat_SWord32(42.0F) = 0x%08"PRIx32"UL\n", __result); } void fromFP_SDouble_SWord64_driver(void) { - const SBool __result = fromFP_SDouble_SWord64(42.0, - 0x000000000000002bULL); + const SWord64 __result = fromFP_SDouble_SWord64(42.0); - printf("fromFP_SDouble_SWord64(42.0, 0x000000000000002bULL) = %d\n", __result); + printf("fromFP_SDouble_SWord64(42.0) = 0x%016"PRIx64"ULL\n", __result); } void f_FP_Abs_driver(void) 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 = "Mon Sep 21 22:01:46 PDT 2015" +buildTime = "Sat Oct 10 21:03:50 PDT 2015" diff --git a/SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs b/SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs --- a/SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs +++ b/SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs @@ -21,7 +21,7 @@ import Data.Maybe(fromJust, fromMaybe) import SBVTest -import qualified Data.Binary.IEEE754 as DB (wordToFloat, wordToDouble) +import qualified Data.Binary.IEEE754 as DB (wordToFloat, wordToDouble, floatToWord, doubleToWord) ghcBitSize :: Bits a => a -> Int ghcBitSize x = fromMaybe (error "SBV.ghcBitSize: Unexpected non-finite usage!") (bitSizeMaybe x) @@ -284,11 +284,11 @@ ++ floatRun2M "fpDiv" (/) fpDiv comb ++ doubleRun2M "fpDiv" (/) fpDiv comb - ++ floatRun2 "fpMin" fpMinH fpMin comb - ++ doubleRun2 "fpMin" fpMinH fpMin comb + ++ floatRunMM "fpMin" fpMinH fpMin comb + ++ doubleRunMM "fpMin" fpMinH fpMin comb - ++ floatRun2 "fpMax" fpMaxH fpMax comb - ++ doubleRun2 "fpMax" fpMaxH fpMax comb + ++ floatRunMM "fpMax" fpMaxH fpMax comb + ++ doubleRunMM "fpMax" fpMaxH fpMax comb ++ floatRun2 "fpRem" fpRemH fpRem comb ++ doubleRun2 "fpRem" fpRemH fpRem comb @@ -351,8 +351,8 @@ ++ map cvtTest [("reinterp_Word32_Float", show x, sWord32AsSFloat (literal x), literal (DB.wordToFloat x)) | x <- w32s] ++ map cvtTest [("reinterp_Word64_Double", show x, sWord64AsSDouble (literal x), literal (DB.wordToDouble x)) | x <- w64s] - ++ map cvtTestI [("reinterp_Float_Word32", show x, sFloatAsSWord32 (sWord32AsSFloat (literal x)) (literal x), literal true) | x <- w32s] - ++ map cvtTestI [("reinterp_Double_Word64", show x, sDoubleAsSWord64 (sWord64AsSDouble (literal x)) (literal x), literal true) | x <- w64s] + ++ map cvtTestI [("reinterp_Float_Word32", show x, sFloatAsSWord32 (literal x), literal (DB.floatToWord x)) | x <- fs, not (isNaN x)] -- Not unique for NaN + ++ map cvtTestI [("reinterp_Double_Word64", show x, sDoubleAsSWord64 (literal x), literal (DB.doubleToWord x)) | x <- ds, not (isNaN x)] -- Not unique for NaN floatRun1 nm f g cmb = map (nm,) [cmb (x, f x, extract (g (literal x))) | x <- fs] doubleRun1 nm f g cmb = map (nm,) [cmb (x, f x, extract (g (literal x))) | x <- ds] @@ -362,6 +362,10 @@ doubleRun2 nm f g cmb = map (nm,) [cmb (x, y, f x y, extract (g (literal x) (literal y))) | x <- ds, y <- ds] floatRun2M nm f g cmb = map (nm,) [cmb (x, y, f x y, extract (g sRNE (literal x) (literal y))) | x <- fs, y <- fs] doubleRun2M nm f g cmb = map (nm,) [cmb (x, y, f x y, extract (g sRNE (literal x) (literal y))) | x <- ds, y <- ds] + floatRunMM nm f g cmb = map (nm,) [cmb (x, y, f x y, extract (g (literal x) (literal y))) | x <- fs, y <- fs, not (alt0 x y || alt0 y x)] + doubleRunMM nm f g cmb = map (nm,) [cmb (x, y, f x y, extract (g (literal x) (literal y))) | x <- ds, y <- ds, not (alt0 x y || alt0 y x)] + -- fpMin/fpMax: skip +0/-0 case as this is underspecified + alt0 x y = isNegativeZero x && y == 0 && not (isNegativeZero y) uTests = map mkTest1 $ concatMap (checkPred fs sfs) predicates ++ concatMap (checkPred ds sds) predicates extract :: SymWord a => SBV a -> a 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 @@ -17,7 +17,7 @@ module TestSuite.Basics.ArithSolver(testSuite) where import Data.Maybe (fromMaybe, fromJust) -import qualified Data.Binary.IEEE754 as DB (wordToFloat, wordToDouble) +import qualified Data.Binary.IEEE754 as DB (wordToFloat, wordToDouble, floatToWord, doubleToWord) import Data.SBV import Data.SBV.Internals @@ -33,6 +33,7 @@ genReals ++ genFloats ++ genDoubles + ++ genFPConverts ++ genQRems ++ genBinTest True "+" (+) ++ genBinTest True "-" (-) @@ -209,8 +210,7 @@ genDoubles = genIEEE754 "genDoubles" ds genIEEE754 :: (IEEEFloating a, Show a, Ord a) => String -> [a] -> [Test] -genIEEE754 origin vs = map tst1 [("fpCast_" ++ nm, x, y) | (nm, x, y) <- converts] - ++ map tst1 [("pred_" ++ nm, x, y) | (nm, x, y) <- preds] +genIEEE754 origin vs = map tst1 [("pred_" ++ nm, x, y) | (nm, x, y) <- preds] ++ map tst1 [("unary_" ++ nm, x, y) | (nm, x, y) <- uns] ++ map tst2 [("binary_" ++ nm, x, y, r) | (nm, x, y, r) <- bins] where uns = [("abs", show x, mkThm1 abs x (abs x)) | x <- vs] @@ -236,8 +236,8 @@ ++ [("fpSub", show x, show y, mkThm2 (m fpSub) x y ((-) x y)) | x <- vs, y <- vs] ++ [("fpMul", show x, show y, mkThm2 (m fpMul) x y ((*) x y)) | x <- vs, y <- vs] ++ [("fpDiv", show x, show y, mkThm2 (m fpDiv) x y ((/) x y)) | x <- vs, y <- vs] - ++ [("fpMin", show x, show y, mkThm2 fpMin x y (fpMinH x y)) | x <- vs, y <- vs] - ++ [("fpMax", show x, show y, mkThm2 fpMax x y (fpMaxH x y)) | x <- vs, y <- vs] + ++ [("fpMin", show x, show y, mkThm2 fpMin x y (fpMinH x y)) | x <- vs, y <- vs, not (alt0 x y || alt0 y x)] + ++ [("fpMax", show x, show y, mkThm2 fpMax x y (fpMaxH x y)) | x <- vs, y <- vs, not (alt0 x y || alt0 y x)] ++ [("fpIsEqualObject", show x, show y, mkThm2P fpIsEqualObject x y (fpIsEqualObjectH x y)) | x <- vs, y <- vs] ++ [("fpRem", show x, show y, mkThm2 fpRem x y (fpRemH x y)) | x <- vsFPRem, y <- vsFPRem] @@ -246,7 +246,75 @@ | origin == "genDoubles" = [nan, infinity, 0, 0.5, -infinity, -0, -0.5] | True = vs - converts = [("toFP_Int8_ToFloat", show x, mkThmC (m toSFloat) x (fromRational (toRational x))) | x <- i8s ] + -- fpMin/fpMax: skip +0/-0 case as this is underspecified + alt0 x y = isNegativeZero x && y == 0 && not (isNegativeZero y) + + m f = f sRNE + + preds = [(pn, show x, mkThmP ps x (pc x)) | (pn, ps, pc) <- predicates, x <- vs + -- Work around GHC bug, see issue #138 + -- Remove the following line when fixed. + , not (pn == "fpIsPositiveZero" && isNegativeZero x) + ] + 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 $ fpIsNaN v + | isNegativeZero val = constrain $ fpIsNegativeZero v + | val == 0 = constrain $ fpIsPositiveZero v + | isInfinite val && val > 0 = constrain $ fpIsInfinite v &&& fpIsPositive v + | isInfinite val && val < 0 = constrain $ fpIsInfinite v &&& fpIsNegative v + | True = constrain $ v .== literal val + + -- Quickly pick which solver to use. Currently z3 or mathSAT supports FP + fpProver :: SMTConfig + fpProver = z3 -- mathSAT + + fpThm :: Provable a => a -> IO Bool + fpThm p = fromJust `fmap` isTheoremWith fpProver Nothing p + + mkThmP op x r = fpThm $ do a <- free "x" + eqF a x + return $ literal r .== op a + + mkThm2P op x y r = fpThm $ do [a, b] <- mapM free ["x", "y"] + eqF a x + eqF b y + return $ literal r .== a `op` b + + mkThm1 op x r = fpThm $ do a <- free "x" + eqF a x + return $ literal r `fpIsEqualObject` op a + + mkThm2 op x y r = fpThm $ do [a, b] <- mapM free ["x", "y"] + eqF a x + eqF b y + return $ literal r `fpIsEqualObject` (a `op` b) + + mkThm2C neq op x y r = fpThm $ do [a, b] <- mapM free ["x", "y"] + eqF a x + eqF b y + return $ if isNaN x || isNaN y + then (if neq then a `op` b else bnot (a `op` b)) + else literal r .== a `op` b + + predicates :: (IEEEFloating a) => [(String, SBV a -> SBool, a -> Bool)] + predicates = [ ("fpIsNormal", fpIsNormal, fpIsNormalizedH) + , ("fpIsSubnormal", fpIsSubnormal, isDenormalized) + , ("fpIsZero", fpIsZero, (== 0)) + , ("fpIsInfinite", fpIsInfinite, isInfinite) + , ("fpIsNaN", fpIsNaN, isNaN) + , ("fpIsNegative", fpIsNegative, \x -> x < 0 || isNegativeZero x) + , ("fpIsPositive", fpIsPositive, \x -> x >= 0 && not (isNegativeZero x)) + , ("fpIsNegativeZero", fpIsNegativeZero, isNegativeZero) + , ("fpIsPositiveZero", fpIsPositiveZero, \x -> x == 0 && not (isNegativeZero x)) + , ("fpIsPoint", fpIsPoint, \x -> not (isNaN x || isInfinite x)) + ] + +genFPConverts :: [Test] +genFPConverts = map tst1 [("fpCast_" ++ nm, x, y) | (nm, x, y) <- converts] + where converts = [("toFP_Int8_ToFloat", show x, mkThmC (m toSFloat) x (fromRational (toRational x))) | x <- i8s ] ++ [("toFP_Int16_ToFloat", show x, mkThmC (m toSFloat) x (fromRational (toRational x))) | x <- i16s] ++ [("toFP_Int32_ToFloat", show x, mkThmC (m toSFloat) x (fromRational (toRational x))) | x <- i32s] ++ [("toFP_Int64_ToFloat", show x, mkThmC (m toSFloat) x (fromRational (toRational x))) | x <- i64s] @@ -305,18 +373,12 @@ ++ [("reinterp_Word32_Float", show x, mkThmC sWord32AsSFloat x (DB.wordToFloat x)) | x <- w32s] ++ [("reinterp_Word64_Double", show x, mkThmC sWord64AsSDouble x (DB.wordToDouble x)) | x <- w64s] - ++ [("reinterp_Float_Word32", show x, mkIso sFloatAsSWord32 sWord32AsSFloat x) | x <- w32s] - ++ [("reinterp_Double_Word64", show x, mkIso sDoubleAsSWord64 sWord64AsSDouble x) | x <- w64s] + ++ [("reinterp_Float_Word32", show x, mkThmP sFloatAsSWord32 x (DB.floatToWord x)) | x <- fs, not (isNaN x)] -- Not unique for NaN + ++ [("reinterp_Double_Word64", show x, mkThmP sDoubleAsSWord64 x (DB.doubleToWord x)) | x <- ds, not (isNaN x)] -- Not unique for NaN m f = f sRNE - preds = [(pn, show x, mkThmP ps x (pc x)) | (pn, ps, pc) <- predicates, x <- vs - -- Work around GHC bug, see issue #138 - -- Remove the following line when fixed. - , not (pn == "fpIsPositiveZero" && isNegativeZero x) - ] - tst2 (nm, x, y, t) = origin ++ ".arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t - tst1 (nm, x, t) = origin ++ ".arithmetic-" ++ nm ++ "." ++ x ~: assert t + tst1 (nm, x, t) = "fpConverts.arithmetic-" ++ nm ++ "." ++ x ~: assert t eqF v val | isNaN val = constrain $ fpIsNaN v @@ -333,19 +395,10 @@ fpThm :: Provable a => a -> IO Bool fpThm p = fromJust `fmap` isTheoremWith fpProver Nothing p - mkIso f g i = fpThm $ do a <- free "x" - constrain $ a .== literal i - return (f (g a) a :: SBool) - mkThmP op x r = fpThm $ do a <- free "x" eqF a x return $ literal r .== op a - mkThm2P op x y r = fpThm $ do [a, b] <- mapM free ["x", "y"] - eqF a x - eqF b y - return $ literal r .== a `op` b - mkThm1 op x r = fpThm $ do a <- free "x" eqF a x return $ literal r `fpIsEqualObject` op a @@ -357,31 +410,6 @@ mkThmC' op x r = fpThm $ do a <- free "x" eqF a x return $ literal r .== op a - - mkThm2 op x y r = fpThm $ do [a, b] <- mapM free ["x", "y"] - eqF a x - eqF b y - return $ literal r `fpIsEqualObject` (a `op` b) - - mkThm2C neq op x y r = fpThm $ do [a, b] <- mapM free ["x", "y"] - eqF a x - eqF b y - return $ if isNaN x || isNaN y - then (if neq then a `op` b else bnot (a `op` b)) - else literal r .== a `op` b - - predicates :: (IEEEFloating a) => [(String, SBV a -> SBool, a -> Bool)] - predicates = [ ("fpIsNormal", fpIsNormal, fpIsNormalizedH) - , ("fpIsSubnormal", fpIsSubnormal, isDenormalized) - , ("fpIsZero", fpIsZero, (== 0)) - , ("fpIsInfinite", fpIsInfinite, isInfinite) - , ("fpIsNaN", fpIsNaN, isNaN) - , ("fpIsNegative", fpIsNegative, \x -> x < 0 || isNegativeZero x) - , ("fpIsPositive", fpIsPositive, \x -> x >= 0 && not (isNegativeZero x)) - , ("fpIsNegativeZero", fpIsNegativeZero, isNegativeZero) - , ("fpIsPositiveZero", fpIsPositiveZero, \x -> x == 0 && not (isNegativeZero x)) - , ("fpIsPoint", fpIsPoint, \x -> not (isNaN x || isInfinite x)) - ] genQRems :: [Test] genQRems = map mkTest $ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- w8s, y <- w8s ] diff --git a/SBVUnitTest/TestSuite/CodeGeneration/Floats.hs b/SBVUnitTest/TestSuite/CodeGeneration/Floats.hs --- a/SBVUnitTest/TestSuite/CodeGeneration/Floats.hs +++ b/SBVUnitTest/TestSuite/CodeGeneration/Floats.hs @@ -97,8 +97,8 @@ , test1 "fromFP_SWord32_SFloat" (sWord32AsSFloat :: SWord32 -> SFloat) , test1 "fromFP_SWord64_SDouble" (sWord64AsSDouble :: SWord64 -> SDouble) - , test2 "fromFP_SFloat_SWord32" (sFloatAsSWord32 :: SFloat -> SWord32 -> SBool) - , test2 "fromFP_SDouble_SWord64" (sDoubleAsSWord64 :: SDouble -> SWord64 -> SBool) + , test1 "fromFP_SFloat_SWord32" (sFloatAsSWord32 :: SFloat -> SWord32) + , test1 "fromFP_SDouble_SWord64" (sDoubleAsSWord64 :: SDouble -> SWord64) , test1 "f_FP_Abs" (abs :: SFloat -> SFloat) , test1 "d_FP_Abs" (abs :: SDouble -> SDouble) diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,5 +1,5 @@ Name: sbv -Version: 5.0 +Version: 5.1 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