diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,36 @@ * Hackage: * GitHub: -* Latest Hackage released version: 4.3, 2015-04-10 +* Latest Hackage released version: 4.4, 2015-04-13 + +### Version 4.4, 2015-04-13 + + * Hook-up crackNum package; so counter-examples involving floats and + doubles can be printed in detail when the printBase is chosen to be + 2 or 16. (With base 10, we still get the simple output.) + + ``` + Prelude Data.SBV> satWith z3{printBase=2} $ \x -> x .== (2::SFloat) + Satisfiable. Model: + s0 = 2.0 :: Float + 3 2 1 0 + 1 09876543 21098765432109876543210 + S ---E8--- ----------F23---------- + Binary: 0 10000000 00000000000000000000000 + Hex: 4000 0000 + Precision: SP + Sign: Positive + Exponent: 1 (Stored: 128, Bias: 127) + Value: +2.0 (NORMAL) + ``` + + * Change how we print type info; for models insted of SType just print Type (i.e., + for SWord8, instead print Word8) which makes more sense and is more consistent. + This change should be mostly relevant as how we see the counter-example output. + + * Fix long standing bug #75, where we now support arrays with Boolean source/targets. + This is not a very commonly used case, but by letting the solver pick the logic, + we now allow arrays to be uniformly supported. ### Version 4.3, 2015-04-10 diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -19,7 +19,7 @@ -- -- >>> prove $ \x -> x `shiftL` 2 .== 2 * (x :: SWord8) -- Falsifiable. Counter-example: --- s0 = 32 :: SWord8 +-- s0 = 32 :: Word8 -- -- The function 'prove' has the following type: -- @@ -609,15 +609,15 @@ >>> prove $ \x y -> sub x y .>= (0 :: SInt16) *** Exception: Assertion failure: "sub: x >= y must hold!" - s0 = -32768 :: SInt16 - s1 = -32767 :: SInt16 + s0 = -32768 :: Int16 + s1 = -32767 :: Int16 Of course, we can use, 'safe' to statically see if such a violation is possible before we attempt a proof: >>> safe (sub :: SInt8 -> SInt8 -> SInt8) Assertion failure: "sub: x >= y must hold!" - s0 = -128 :: SInt8 - s1 = -127 :: SInt8 + s0 = -128 :: Int8 + s1 = -127 :: Int8 What happens if we make sure to arrange for this invariant? Consider this version: diff --git a/Data/SBV/BitVectors/Concrete.hs b/Data/SBV/BitVectors/Concrete.hs --- a/Data/SBV/BitVectors/Concrete.hs +++ b/Data/SBV/BitVectors/Concrete.hs @@ -153,8 +153,18 @@ -- | Show instance for 'CW'. instance Show CW where - show w | cwIsBit w = show (cwToBool w) - show w = liftCW show show show show snd w ++ " :: " ++ show (cwKind w) + show = showCW True + +-- | Show a CW, with kind info if bool is True. Note that bits never get their type printed +-- as it is more or less useless. (i.e., No need to say SBool for True and False) +showCW :: Bool -> CW -> String +showCW _ w | cwIsBit w = show (cwToBool w) +showCW shk w = liftCW show show show show snd w ++ kInfo + where kInfo | shk = " :: " ++ shKind (cwKind w) + | True = "" + shKind k@(KUserSort {}) = show k + shKind k | ('S':sk) <- show k = sk + shKind k = show k -- | Create a constant word from an integral. mkConstCW :: Integral a => Kind -> a -> CW 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 @@ -79,7 +79,7 @@ hasSign :: a -> Bool intSizeOf :: a -> Int isBoolean :: a -> Bool - isBounded :: a -> Bool + isBounded :: a -> Bool -- NB. This really means word/int; i.e., Real/Float will test False isReal :: a -> Bool isFloat :: a -> Bool isDouble :: a -> Bool @@ -129,6 +129,9 @@ instance HasKind AlgReal where kindOf _ = KReal instance HasKind Float where kindOf _ = KFloat instance HasKind Double where kindOf _ = KDouble + +instance HasKind Kind where + kindOf = id instance HasKind CW where kindOf = cwKind 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 @@ -372,7 +372,7 @@ | True = result `is` fVal where result = sWord32ToSFloat wVal a `is` b = (checkNaN a &&& checkNaN b) ||| (a .== b) - checkNaN = liftFPPredicate "fp.isNaN" isNaN + checkNaN = liftFPPredicate "fp.isNaN" isNaN -- | 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. @@ -382,7 +382,7 @@ | True = result `is` fVal where result = sWord64ToSDouble wVal a `is` b = (checkNaN a &&& checkNaN b) ||| (a .== b) - checkNaN = liftFPPredicate "fp.isNaN" isNaN + checkNaN = liftFPPredicate "fp.isNaN" isNaN -- | 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 function relationally, much like 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 @@ -26,6 +26,8 @@ import Data.Word (Word8, Word16, Word32, Word64) import Numeric (showIntAtBase, showHex, readInt) +import Data.Numbers.CrackNum (floatToFP, doubleToFP) + import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.AlgReals (algRealToSMTLib2) @@ -66,24 +68,32 @@ instance PrettyNum CW where hexS cw | cwIsBit cw = hexS (cwToBool cw) - | isReal cw = let CWAlgReal w = cwVal cw in show w + | isFloat cw = let CWFloat f = cwVal cw in show f ++ " :: Float\n" ++ show (floatToFP f) + | isDouble cw = let CWDouble d = cwVal cw in show d ++ " :: Double\n" ++ show (doubleToFP d) + | isReal cw = let CWAlgReal w = cwVal cw in show w ++ " :: Real" | not (isBounded cw) = let CWInteger w = cwVal cw in shexI True True w - | isUninterpreted cw = show cw + | isUninterpreted cw = show cw ++ " :: " ++ show (cwKind cw) | True = let CWInteger w = cwVal cw in shex True True (hasSign cw, intSizeOf cw) w binS cw | cwIsBit cw = binS (cwToBool cw) - | isReal cw = let CWAlgReal w = cwVal cw in show w + | isFloat cw = let CWFloat f = cwVal cw in show f ++ " :: Float\n" ++ show (floatToFP f) + | isDouble cw = let CWDouble d = cwVal cw in show d ++ " :: Double\n" ++ show (doubleToFP d) + | isReal cw = let CWAlgReal w = cwVal cw in show w ++ " :: Real" | not (isBounded cw) = let CWInteger w = cwVal cw in sbinI True True w - | isUninterpreted cw = show cw + | isUninterpreted cw = show cw ++ " :: " ++ show (cwKind cw) | True = let CWInteger w = cwVal cw in sbin True True (hasSign cw, intSizeOf cw) w hex cw | cwIsBit cw = hexS (cwToBool cw) + | isFloat cw = let CWFloat f = cwVal cw in show f + | isDouble cw = let CWDouble d = cwVal cw in show d | isReal cw = let CWAlgReal w = cwVal cw in show w | not (isBounded cw) = let CWInteger w = cwVal cw in shexI False False w | isUninterpreted cw = show cw | True = let CWInteger w = cwVal cw in shex False False (hasSign cw, intSizeOf cw) w bin cw | cwIsBit cw = binS (cwToBool cw) + | isFloat cw = let CWFloat f = cwVal cw in show f + | isDouble cw = let CWDouble d = cwVal cw in show d | isReal cw = let CWAlgReal w = cwVal cw in show w | not (isBounded cw) = let CWInteger w = cwVal cw in sbinI False False w | isUninterpreted cw = show cw 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 @@ -427,9 +427,13 @@ svSigned x = kindHasSign (svKind x) -- | Show instance for 'SVal'. Not particularly "desirable", but will do if needed +-- NB. We do not show the type info on constant KBool values, since there's no +-- implicit "fromBoolean" applied to Booleans in Haskell; and thus a statement +-- of the form "True :: SBool" is just meaningless. (There should be a fromBoolean!) instance Show SVal where - show (SVal _ (Left c)) = show c - show (SVal k (Right _)) = " :: " ++ show k + show (SVal KBool (Left c)) = showCW False c + show (SVal k (Left c)) = showCW False c ++ " :: " ++ show k + show (SVal k (Right _)) = " :: " ++ show k -- | Equality constraint on SBV values. Not desirable since we can't really compare two -- symbolic values, but will do. @@ -965,12 +969,15 @@ -- exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it -- is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation -- of the real value is not finite, i.e., if it is not rational. +-- +-- The 'printBase' field can be used to print numbers in base 2, 10, or 16. If base 2 or 16 is used, then floating-point values will +-- be printed in their internal memory-layout format as well, which can come in handy for bit-precise analysis. data SMTConfig = SMTConfig { verbose :: Bool -- ^ Debug mode , timing :: Bool -- ^ Print timing information on how long different phases took (construction, solving, etc.) , sBranchTimeOut :: Maybe Int -- ^ How much time to give to the solver for each call of 'sBranch' check. (In seconds. Default: No limit.) , timeOut :: Maybe Int -- ^ How much time to give to the solver. (In seconds. Default: No limit.) - , printBase :: Int -- ^ Print integral literals in this base (2, 8, 10, and 16 are supported.) + , printBase :: Int -- ^ Print integral literals in this base (2, 10, and 16 are supported.) , printRealPrec :: Int -- ^ Print algebraic real values with this precision. (SReal, default: 16) , solverTweaks :: [String] -- ^ Additional lines of script to give to the solver (user specified) , satCmd :: String -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics. diff --git a/Data/SBV/Examples/BitPrecise/PrefixSum.hs b/Data/SBV/Examples/BitPrecise/PrefixSum.hs --- a/Data/SBV/Examples/BitPrecise/PrefixSum.hs +++ b/Data/SBV/Examples/BitPrecise/PrefixSum.hs @@ -100,14 +100,14 @@ -- -- >>> thm3 -- Falsifiable. Counter-example: --- s0 = 0 :: SWord32 --- s1 = 0 :: SWord32 --- s2 = 0 :: SWord32 --- s3 = 0 :: SWord32 --- s4 = 1073741824 :: SWord32 --- s5 = 0 :: SWord32 --- s6 = 0 :: SWord32 --- s7 = 0 :: SWord32 +-- s0 = 0 :: Word32 +-- s1 = 0 :: Word32 +-- s2 = 0 :: Word32 +-- s3 = 0 :: Word32 +-- s4 = 1073741824 :: Word32 +-- s5 = 0 :: Word32 +-- s6 = 0 :: Word32 +-- s7 = 0 :: Word32 -- -- uninterpreted: u -- u = 0 -- -- uninterpreted: flOp 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 @@ -28,9 +28,9 @@ -- -- >>> prove assocPlus -- Falsifiable. Counter-example: --- s0 = -9.62965e-35 :: SFloat --- s1 = Infinity :: SFloat --- s2 = -Infinity :: SFloat +-- s0 = -9.62965e-35 :: Float +-- s1 = Infinity :: Float +-- s2 = -Infinity :: Float -- -- Indeed: -- @@ -56,9 +56,9 @@ -- -- >>> assocPlusRegular -- Falsifiable. Counter-example: --- x = -1.0491915e7 :: SFloat --- y = 1967115.5 :: SFloat --- z = 982003.94 :: SFloat +-- x = -1.0491915e7 :: Float +-- y = 1967115.5 :: Float +-- z = 982003.94 :: Float -- -- Indeed, we have: -- @@ -87,8 +87,8 @@ -- -- >>> nonZeroAddition -- Falsifiable. Counter-example: --- a = -2.0 :: SFloat --- b = -3.0e-45 :: SFloat +-- a = -2.0 :: Float +-- b = -3.0e-45 :: Float -- -- Indeed, we have: -- @@ -118,7 +118,7 @@ -- -- >>> multInverse -- Falsifiable. Counter-example: --- a = -2.0445642768532407e154 :: SDouble +-- a = -2.0445642768532407e154 :: Double -- -- Indeed, we have: -- @@ -146,8 +146,8 @@ -- >>> roundingAdd -- Satisfiable. Model: -- rm = RoundTowardPositive :: RoundingMode --- x = 246080.08 :: SFloat --- y = 16255.999 :: SFloat +-- x = 246080.08 :: Float +-- y = 16255.999 :: Float -- -- Unfortunately we can't directly validate this result at the Haskell level, as Haskell only supports -- 'RoundNearestTiesToEven'. We have: @@ -160,7 +160,7 @@ -- -- >>> sat $ \z -> z .== fpAdd sRoundTowardPositive 246080.08 (16255.999::SFloat) -- Satisfiable. Model: --- s0 = 262336.1 :: SFloat +-- s0 = 262336.1 :: Float -- -- We can see why these two resuls are indeed different. To see why, one would have to convert the -- individual numbers to Float's, which would induce rounding-errors, add them up, and round-back; diff --git a/Data/SBV/Examples/Puzzles/Coins.hs b/Data/SBV/Examples/Puzzles/Coins.hs --- a/Data/SBV/Examples/Puzzles/Coins.hs +++ b/Data/SBV/Examples/Puzzles/Coins.hs @@ -81,12 +81,12 @@ -- -- >>> puzzle -- Satisfiable. Model: --- c1 = 50 :: SWord16 --- c2 = 25 :: SWord16 --- c3 = 10 :: SWord16 --- c4 = 10 :: SWord16 --- c5 = 10 :: SWord16 --- c6 = 10 :: SWord16 +-- c1 = 50 :: Word16 +-- c2 = 25 :: Word16 +-- c3 = 10 :: Word16 +-- c4 = 10 :: Word16 +-- c5 = 10 :: Word16 +-- c6 = 10 :: Word16 -- -- i.e., your friend has 4 dimes, a quarter, and a half dollar. puzzle :: IO SatResult 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,9 +21,9 @@ -- -- >>> puzzle -- Solution #1: --- dog = 3 :: SInteger --- cat = 41 :: SInteger --- mouse = 56 :: SInteger +-- dog = 3 :: Integer +-- cat = 41 :: Integer +-- mouse = 56 :: Integer -- This is the only solution. puzzle :: IO AllSatResult puzzle = allSat $ do diff --git a/Data/SBV/Examples/Uninterpreted/Function.hs b/Data/SBV/Examples/Uninterpreted/Function.hs --- a/Data/SBV/Examples/Uninterpreted/Function.hs +++ b/Data/SBV/Examples/Uninterpreted/Function.hs @@ -33,8 +33,8 @@ -- -- >>> proveWith yicesSMT09 $ forAll ["x", "y"] thmBad -- Falsifiable. Counter-example: --- x = 0 :: SWord8 --- y = 128 :: SWord8 +-- x = 0 :: Word8 +-- y = 128 :: Word8 -- -- uninterpreted: f -- f 128 0 = 32768 -- f _ _ = 0 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 @@ -97,12 +97,13 @@ -> ([String], [String]) cvt rm smtLogic solverCaps kindInfo isSat comments inputs skolemInps consts tbls arrs uis axs (SBVPgm asgnsSeq) cstrs out = (pre, []) where -- the logic is an over-approaximation - hasInteger = KUnbounded `Set.member` kindInfo - hasReal = KReal `Set.member` kindInfo - hasFloat = KFloat `Set.member` kindInfo - hasDouble = KDouble `Set.member` kindInfo - hasBVs = not $ null [() | KBounded{} <- Set.toList kindInfo] - usorts = [(s, dt) | KUserSort s dt <- Set.toList kindInfo] + hasInteger = KUnbounded `Set.member` kindInfo + hasReal = KReal `Set.member` kindInfo + hasFloat = KFloat `Set.member` kindInfo + hasDouble = KDouble `Set.member` kindInfo + hasBVs = not $ null [() | KBounded{} <- Set.toList kindInfo] + usorts = [(s, dt) | KUserSort s dt <- Set.toList kindInfo] + hasNonBVArrays = (not . null) [() | (_, (_, (k1, k2), _)) <- arrs, not (isBounded k1 && isBounded k2)] logic | Just l <- smtLogic = ["(set-logic " ++ show l ++ ") ; NB. User specified."] @@ -110,10 +111,15 @@ = if hasBVs then ["(set-logic QF_FPBV)"] else ["(set-logic QF_FP)"] - | hasInteger || hasReal || not (null usorts) - = case mbDefaultLogic solverCaps of - Nothing -> ["; Has unbounded values (Int/Real) or uninterpreted sorts; no logic specified."] -- combination, let the solver pick - Just l -> ["(set-logic " ++ l ++ ")"] + | hasInteger || hasReal || not (null usorts) || hasNonBVArrays + = let why | hasInteger = "has unbounded values" + | hasReal = "has algebraic reals" + | not (null usorts) = "has user-defined sorts" + | hasNonBVArrays = "has non-bitvector arrays" + | True = "cannot determine the SMTLib-logic to use" + in case mbDefaultLogic solverCaps of + Nothing -> ["; " ++ why ++ ", no logic specified."] + Just l -> ["(set-logic " ++ l ++ "); " ++ why ++ ", using solver-default logic."] | True = ["(set-logic " ++ qs ++ as ++ ufs ++ "BV)"] where qs | null foralls && null axs = "QF_" -- axioms are likely to contain quantifiers diff --git a/SBVUnitTest/GoldFiles/auf-1.gold b/SBVUnitTest/GoldFiles/auf-1.gold --- a/SBVUnitTest/GoldFiles/auf-1.gold +++ b/SBVUnitTest/GoldFiles/auf-1.gold @@ -5,9 +5,9 @@ CONSTANTS s_2 = False s_1 = True - s3 = 2 :: SWord32 - s9 = 3 :: SWord32 - s13 = 1 :: SWord32 + s3 = 2 :: Word32 + s9 = 3 :: Word32 + s13 = 1 :: Word32 TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/basic-1_1.gold b/SBVUnitTest/GoldFiles/basic-1_1.gold --- a/SBVUnitTest/GoldFiles/basic-1_1.gold +++ b/SBVUnitTest/GoldFiles/basic-1_1.gold @@ -1,1 +1,1 @@ -5 :: SWord8 +5 :: Word8 diff --git a/SBVUnitTest/GoldFiles/basic-1_2.gold b/SBVUnitTest/GoldFiles/basic-1_2.gold --- a/SBVUnitTest/GoldFiles/basic-1_2.gold +++ b/SBVUnitTest/GoldFiles/basic-1_2.gold @@ -1,1 +1,1 @@ -5 :: SWord8 +5 :: Word8 diff --git a/SBVUnitTest/GoldFiles/basic-1_3.gold b/SBVUnitTest/GoldFiles/basic-1_3.gold --- a/SBVUnitTest/GoldFiles/basic-1_3.gold +++ b/SBVUnitTest/GoldFiles/basic-1_3.gold @@ -1,1 +1,1 @@ -25 :: SWord8 +25 :: Word8 diff --git a/SBVUnitTest/GoldFiles/basic-1_4.gold b/SBVUnitTest/GoldFiles/basic-1_4.gold --- a/SBVUnitTest/GoldFiles/basic-1_4.gold +++ b/SBVUnitTest/GoldFiles/basic-1_4.gold @@ -1,1 +1,1 @@ -25 :: SWord8 +25 :: Word8 diff --git a/SBVUnitTest/GoldFiles/basic-1_5.gold b/SBVUnitTest/GoldFiles/basic-1_5.gold --- a/SBVUnitTest/GoldFiles/basic-1_5.gold +++ b/SBVUnitTest/GoldFiles/basic-1_5.gold @@ -1,1 +1,1 @@ -4 :: SWord8 +4 :: Word8 diff --git a/SBVUnitTest/GoldFiles/basic-2_1.gold b/SBVUnitTest/GoldFiles/basic-2_1.gold --- a/SBVUnitTest/GoldFiles/basic-2_1.gold +++ b/SBVUnitTest/GoldFiles/basic-2_1.gold @@ -3,7 +3,7 @@ CONSTANTS s_2 = False s_1 = True - s1 = 3 :: SWord8 + s1 = 3 :: Word8 TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/basic-2_2.gold b/SBVUnitTest/GoldFiles/basic-2_2.gold --- a/SBVUnitTest/GoldFiles/basic-2_2.gold +++ b/SBVUnitTest/GoldFiles/basic-2_2.gold @@ -3,7 +3,7 @@ CONSTANTS s_2 = False s_1 = True - s1 = 9 :: SWord8 + s1 = 9 :: Word8 TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/basic-2_3.gold b/SBVUnitTest/GoldFiles/basic-2_3.gold --- a/SBVUnitTest/GoldFiles/basic-2_3.gold +++ b/SBVUnitTest/GoldFiles/basic-2_3.gold @@ -3,7 +3,7 @@ CONSTANTS s_2 = False s_1 = True - s1 = 3 :: SWord8 + s1 = 3 :: Word8 TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/basic-2_4.gold b/SBVUnitTest/GoldFiles/basic-2_4.gold --- a/SBVUnitTest/GoldFiles/basic-2_4.gold +++ b/SBVUnitTest/GoldFiles/basic-2_4.gold @@ -3,7 +3,7 @@ CONSTANTS s_2 = False s_1 = True - s1 = 3 :: SWord8 + s1 = 3 :: Word8 TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/basic-2_5.gold b/SBVUnitTest/GoldFiles/basic-2_5.gold --- a/SBVUnitTest/GoldFiles/basic-2_5.gold +++ b/SBVUnitTest/GoldFiles/basic-2_5.gold @@ -1,1 +1,1 @@ -4 :: SWord8 +4 :: Word8 diff --git a/SBVUnitTest/GoldFiles/basic-3_5.gold b/SBVUnitTest/GoldFiles/basic-3_5.gold --- a/SBVUnitTest/GoldFiles/basic-3_5.gold +++ b/SBVUnitTest/GoldFiles/basic-3_5.gold @@ -4,7 +4,7 @@ CONSTANTS s_2 = False s_1 = True - s2 = 1 :: SWord8 + s2 = 1 :: Word8 TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/basic-4_5.gold b/SBVUnitTest/GoldFiles/basic-4_5.gold --- a/SBVUnitTest/GoldFiles/basic-4_5.gold +++ b/SBVUnitTest/GoldFiles/basic-4_5.gold @@ -3,7 +3,7 @@ CONSTANTS s_2 = False s_1 = True - s1 = 1 :: SWord8 + s1 = 1 :: Word8 TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/basic-5_5.gold b/SBVUnitTest/GoldFiles/basic-5_5.gold --- a/SBVUnitTest/GoldFiles/basic-5_5.gold +++ b/SBVUnitTest/GoldFiles/basic-5_5.gold @@ -4,7 +4,7 @@ CONSTANTS s_2 = False s_1 = True - s2 = 1 :: SWord8 + s2 = 1 :: Word8 TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/ccitt.gold b/SBVUnitTest/GoldFiles/ccitt.gold --- a/SBVUnitTest/GoldFiles/ccitt.gold +++ b/SBVUnitTest/GoldFiles/ccitt.gold @@ -6,76 +6,76 @@ CONSTANTS s_2 = False s_1 = True - s13 = 0 :: SWord1 - s1686 = 0 :: SWord8 - s1687 = 1 :: SWord8 - s1815 = 3 :: SWord8 - s9 = 0 :: SWord16 - s525 = 1 :: SWord64 - s526 = 0 :: SWord64 - s528 = 2 :: SWord64 - s531 = 4 :: SWord64 - s534 = 8 :: SWord64 - s537 = 16 :: SWord64 - s540 = 32 :: SWord64 - s543 = 64 :: SWord64 - s546 = 128 :: SWord64 - s549 = 256 :: SWord64 - s552 = 512 :: SWord64 - s555 = 1024 :: SWord64 - s558 = 2048 :: SWord64 - s561 = 4096 :: SWord64 - s564 = 8192 :: SWord64 - s567 = 16384 :: SWord64 - s570 = 32768 :: SWord64 - s573 = 65536 :: SWord64 - s576 = 131072 :: SWord64 - s579 = 262144 :: SWord64 - s582 = 524288 :: SWord64 - s585 = 1048576 :: SWord64 - s588 = 2097152 :: SWord64 - s591 = 4194304 :: SWord64 - s594 = 8388608 :: SWord64 - s597 = 16777216 :: SWord64 - s600 = 33554432 :: SWord64 - s603 = 67108864 :: SWord64 - s606 = 134217728 :: SWord64 - s609 = 268435456 :: SWord64 - s612 = 536870912 :: SWord64 - s615 = 1073741824 :: SWord64 - s618 = 2147483648 :: SWord64 - s621 = 4294967296 :: SWord64 - s624 = 8589934592 :: SWord64 - s627 = 17179869184 :: SWord64 - s630 = 34359738368 :: SWord64 - s633 = 68719476736 :: SWord64 - s636 = 137438953472 :: SWord64 - s639 = 274877906944 :: SWord64 - s642 = 549755813888 :: SWord64 - s645 = 1099511627776 :: SWord64 - s648 = 2199023255552 :: SWord64 - s651 = 4398046511104 :: SWord64 - s654 = 8796093022208 :: SWord64 - s657 = 17592186044416 :: SWord64 - s660 = 35184372088832 :: SWord64 - s663 = 70368744177664 :: SWord64 - s666 = 140737488355328 :: SWord64 - s669 = 281474976710656 :: SWord64 - s672 = 562949953421312 :: SWord64 - s675 = 1125899906842624 :: SWord64 - s678 = 2251799813685248 :: SWord64 - s681 = 4503599627370496 :: SWord64 - s684 = 9007199254740992 :: SWord64 - s687 = 18014398509481984 :: SWord64 - s690 = 36028797018963968 :: SWord64 - s693 = 72057594037927936 :: SWord64 - s696 = 144115188075855872 :: SWord64 - s699 = 288230376151711744 :: SWord64 - s702 = 576460752303423488 :: SWord64 - s705 = 1152921504606846976 :: SWord64 - s708 = 2305843009213693952 :: SWord64 - s711 = 4611686018427387904 :: SWord64 - s714 = 9223372036854775808 :: SWord64 + s13 = 0 :: Word1 + s1686 = 0 :: Word8 + s1687 = 1 :: Word8 + s1815 = 3 :: Word8 + s9 = 0 :: Word16 + s525 = 1 :: Word64 + s526 = 0 :: Word64 + s528 = 2 :: Word64 + s531 = 4 :: Word64 + s534 = 8 :: Word64 + s537 = 16 :: Word64 + s540 = 32 :: Word64 + s543 = 64 :: Word64 + s546 = 128 :: Word64 + s549 = 256 :: Word64 + s552 = 512 :: Word64 + s555 = 1024 :: Word64 + s558 = 2048 :: Word64 + s561 = 4096 :: Word64 + s564 = 8192 :: Word64 + s567 = 16384 :: Word64 + s570 = 32768 :: Word64 + s573 = 65536 :: Word64 + s576 = 131072 :: Word64 + s579 = 262144 :: Word64 + s582 = 524288 :: Word64 + s585 = 1048576 :: Word64 + s588 = 2097152 :: Word64 + s591 = 4194304 :: Word64 + s594 = 8388608 :: Word64 + s597 = 16777216 :: Word64 + s600 = 33554432 :: Word64 + s603 = 67108864 :: Word64 + s606 = 134217728 :: Word64 + s609 = 268435456 :: Word64 + s612 = 536870912 :: Word64 + s615 = 1073741824 :: Word64 + s618 = 2147483648 :: Word64 + s621 = 4294967296 :: Word64 + s624 = 8589934592 :: Word64 + s627 = 17179869184 :: Word64 + s630 = 34359738368 :: Word64 + s633 = 68719476736 :: Word64 + s636 = 137438953472 :: Word64 + s639 = 274877906944 :: Word64 + s642 = 549755813888 :: Word64 + s645 = 1099511627776 :: Word64 + s648 = 2199023255552 :: Word64 + s651 = 4398046511104 :: Word64 + s654 = 8796093022208 :: Word64 + s657 = 17592186044416 :: Word64 + s660 = 35184372088832 :: Word64 + s663 = 70368744177664 :: Word64 + s666 = 140737488355328 :: Word64 + s669 = 281474976710656 :: Word64 + s672 = 562949953421312 :: Word64 + s675 = 1125899906842624 :: Word64 + s678 = 2251799813685248 :: Word64 + s681 = 4503599627370496 :: Word64 + s684 = 9007199254740992 :: Word64 + s687 = 18014398509481984 :: Word64 + s690 = 36028797018963968 :: Word64 + s693 = 72057594037927936 :: Word64 + s696 = 144115188075855872 :: Word64 + s699 = 288230376151711744 :: Word64 + s702 = 576460752303423488 :: Word64 + s705 = 1152921504606846976 :: Word64 + s708 = 2305843009213693952 :: Word64 + s711 = 4611686018427387904 :: Word64 + s714 = 9223372036854775808 :: Word64 TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/coins.gold b/SBVUnitTest/GoldFiles/coins.gold --- a/SBVUnitTest/GoldFiles/coins.gold +++ b/SBVUnitTest/GoldFiles/coins.gold @@ -8,15 +8,15 @@ CONSTANTS s_2 = False s_1 = True - s1 = 1 :: SWord16 - s3 = 5 :: SWord16 - s5 = 10 :: SWord16 - s7 = 25 :: SWord16 - s9 = 50 :: SWord16 - s11 = 100 :: SWord16 - s84 = 0 :: SWord16 - s88 = 95 :: SWord16 - s551 = 115 :: SWord16 + s1 = 1 :: Word16 + s3 = 5 :: Word16 + s5 = 10 :: Word16 + s7 = 25 :: Word16 + s9 = 50 :: Word16 + s11 = 100 :: Word16 + s84 = 0 :: Word16 + s88 = 95 :: Word16 + s551 = 115 :: Word16 TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/counts.gold b/SBVUnitTest/GoldFiles/counts.gold --- a/SBVUnitTest/GoldFiles/counts.gold +++ b/SBVUnitTest/GoldFiles/counts.gold @@ -12,18 +12,18 @@ CONSTANTS s_2 = False s_1 = True - s10 = 10 :: SWord8 - s12 = 0 :: SWord8 - s32 = 2 :: SWord8 - s33 = 1 :: SWord8 - s35 = 100 :: SWord8 - s555 = 3 :: SWord8 - s716 = 4 :: SWord8 - s877 = 5 :: SWord8 - s1038 = 6 :: SWord8 - s1199 = 7 :: SWord8 - s1360 = 8 :: SWord8 - s1521 = 9 :: SWord8 + s10 = 10 :: Word8 + s12 = 0 :: Word8 + s32 = 2 :: Word8 + s33 = 1 :: Word8 + s35 = 100 :: Word8 + s555 = 3 :: Word8 + s716 = 4 :: Word8 + s877 = 5 :: Word8 + s1038 = 6 :: Word8 + s1199 = 7 :: Word8 + s1360 = 8 :: Word8 + s1521 = 9 :: Word8 TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/crcPolyExist.gold b/SBVUnitTest/GoldFiles/crcPolyExist.gold --- a/SBVUnitTest/GoldFiles/crcPolyExist.gold +++ b/SBVUnitTest/GoldFiles/crcPolyExist.gold @@ -7,10 +7,10 @@ CONSTANTS s_2 = False s_1 = True - s6 = 0 :: SWord1 - s18 = 1 :: SWord8 - s3340 = 0 :: SWord8 - s3468 = 4 :: SWord8 + s6 = 0 :: Word1 + s18 = 1 :: Word8 + s3340 = 0 :: Word8 + s3468 = 4 :: Word8 TABLES ARRAYS UNINTERPRETED CONSTANTS 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 :: SInteger - cat = 41 :: SInteger - mouse = 56 :: SInteger + 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,18 +1,18 @@ Solution #1: - s0 = 4 :: SWord8 - s1 = 6 :: SWord8 - s2 = 4 :: SWord8 - s3 = 0 :: SWord8 - s4 = 2 :: SWord8 - s5 = 6 :: SWord8 - s6 = 1 :: SWord8 - s7 = 5 :: SWord8 - s8 = 7 :: SWord8 - s9 = 1 :: SWord8 - s10 = 8 :: SWord8 - s11 = 4 :: SWord8 - s12 = 9 :: SWord8 - s13 = 5 :: SWord8 - s14 = 3 :: SWord8 - s15 = 3 :: SWord8 + 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 + s13 = 5 :: Word8 + s14 = 3 :: Word8 + s15 = 3 :: Word8 This is the only solution. diff --git a/SBVUnitTest/GoldFiles/higher-9.gold b/SBVUnitTest/GoldFiles/higher-9.gold --- a/SBVUnitTest/GoldFiles/higher-9.gold +++ b/SBVUnitTest/GoldFiles/higher-9.gold @@ -1,2 +1,2 @@ Falsifiable. Counter-example: - s0 = 128 :: SWord8 + s0 = 128 :: Word8 diff --git a/SBVUnitTest/GoldFiles/legato.gold b/SBVUnitTest/GoldFiles/legato.gold --- a/SBVUnitTest/GoldFiles/legato.gold +++ b/SBVUnitTest/GoldFiles/legato.gold @@ -12,11 +12,11 @@ CONSTANTS s_2 = False s_1 = True - s19 = 0 :: SWord1 - s17 = 0 :: SWord8 - s24 = 128 :: SWord8 - s26 = 127 :: SWord8 - s16 = 256 :: SWord16 + s19 = 0 :: Word1 + s17 = 0 :: Word8 + s24 = 128 :: Word8 + s26 = 127 :: Word8 + s16 = 256 :: Word16 TABLES ARRAYS UNINTERPRETED CONSTANTS 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 = 28 :: SInteger + s0 = 28 :: Integer Solution #2: - s0 = 16 :: SInteger + s0 = 16 :: Integer 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 = "Thu Apr 9 22:23:13 PDT 2015" +buildTime = "Sun Apr 12 21:51:24 PDT 2015" diff --git a/SBVUnitTest/TestSuite/Puzzles/DogCatMouse.hs b/SBVUnitTest/TestSuite/Puzzles/DogCatMouse.hs --- a/SBVUnitTest/TestSuite/Puzzles/DogCatMouse.hs +++ b/SBVUnitTest/TestSuite/Puzzles/DogCatMouse.hs @@ -19,7 +19,7 @@ -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \goldCheck -> test [ - "dog cat mouse" ~: allSat p `goldCheck` "dogCatMouse.gold" + "dog_cat_mouse" ~: allSat p `goldCheck` "dogCatMouse.gold" ] where p = do [dog, cat, mouse] <- sIntegers ["dog", "cat", "mouse"] solve [ dog .>= 1 -- at least one dog diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,13 +1,11 @@ Name: sbv -Version: 4.3 +Version: 4.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 (Satisfiability Modulo Theories) solvers. . For details, please see: - . - Release notes: Copyright: Levent Erkok, 2010-2015 License: BSD3 @@ -49,6 +47,7 @@ Build-Depends : base >= 4 && < 5 , array, async, containers, deepseq, directory, filepath, old-time , pretty, process, mtl, QuickCheck, random, syb, data-binary-ieee754 + , crackNum Exposed-modules : Data.SBV , Data.SBV.Bridge.Boolector , Data.SBV.Bridge.CVC4