packages feed

sbv 4.3 → 4.4

raw patch · 39 files changed

+266/−202 lines, 39 filesdep +crackNum

Dependencies added: crackNum

Files

CHANGES.md view
@@ -1,7 +1,36 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub:  <http://leventerkok.github.com/sbv/> -* 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
Data/SBV.hs view
@@ -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:
Data/SBV/BitVectors/Concrete.hs view
@@ -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
Data/SBV/BitVectors/Data.hs view
@@ -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
Data/SBV/BitVectors/Model.hs view
@@ -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
Data/SBV/BitVectors/PrettyNum.hs view
@@ -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
Data/SBV/BitVectors/Symbolic.hs view
@@ -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 _)) = "<symbolic> :: " ++ show k+  show (SVal KBool (Left c))  = showCW False c+  show (SVal k     (Left c))  = showCW False c ++ " :: " ++ show k+  show (SVal k     (Right _)) =         "<symbolic> :: " ++ 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.
Data/SBV/Examples/BitPrecise/PrefixSum.hs view
@@ -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
Data/SBV/Examples/Misc/Floating.hs view
@@ -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;
Data/SBV/Examples/Puzzles/Coins.hs view
@@ -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
Data/SBV/Examples/Puzzles/DogCatMouse.hs view
@@ -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
Data/SBV/Examples/Uninterpreted/Function.hs view
@@ -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
Data/SBV/SMT/SMTLib2.hs view
@@ -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
SBVUnitTest/GoldFiles/auf-1.gold view
@@ -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
SBVUnitTest/GoldFiles/basic-1_1.gold view
@@ -1,1 +1,1 @@-5 :: SWord8+5 :: Word8
SBVUnitTest/GoldFiles/basic-1_2.gold view
@@ -1,1 +1,1 @@-5 :: SWord8+5 :: Word8
SBVUnitTest/GoldFiles/basic-1_3.gold view
@@ -1,1 +1,1 @@-25 :: SWord8+25 :: Word8
SBVUnitTest/GoldFiles/basic-1_4.gold view
@@ -1,1 +1,1 @@-25 :: SWord8+25 :: Word8
SBVUnitTest/GoldFiles/basic-1_5.gold view
@@ -1,1 +1,1 @@-4 :: SWord8+4 :: Word8
SBVUnitTest/GoldFiles/basic-2_1.gold view
@@ -3,7 +3,7 @@ CONSTANTS   s_2 = False   s_1 = True-  s1 = 3 :: SWord8+  s1 = 3 :: Word8 TABLES ARRAYS UNINTERPRETED CONSTANTS
SBVUnitTest/GoldFiles/basic-2_2.gold view
@@ -3,7 +3,7 @@ CONSTANTS   s_2 = False   s_1 = True-  s1 = 9 :: SWord8+  s1 = 9 :: Word8 TABLES ARRAYS UNINTERPRETED CONSTANTS
SBVUnitTest/GoldFiles/basic-2_3.gold view
@@ -3,7 +3,7 @@ CONSTANTS   s_2 = False   s_1 = True-  s1 = 3 :: SWord8+  s1 = 3 :: Word8 TABLES ARRAYS UNINTERPRETED CONSTANTS
SBVUnitTest/GoldFiles/basic-2_4.gold view
@@ -3,7 +3,7 @@ CONSTANTS   s_2 = False   s_1 = True-  s1 = 3 :: SWord8+  s1 = 3 :: Word8 TABLES ARRAYS UNINTERPRETED CONSTANTS
SBVUnitTest/GoldFiles/basic-2_5.gold view
@@ -1,1 +1,1 @@-4 :: SWord8+4 :: Word8
SBVUnitTest/GoldFiles/basic-3_5.gold view
@@ -4,7 +4,7 @@ CONSTANTS   s_2 = False   s_1 = True-  s2 = 1 :: SWord8+  s2 = 1 :: Word8 TABLES ARRAYS UNINTERPRETED CONSTANTS
SBVUnitTest/GoldFiles/basic-4_5.gold view
@@ -3,7 +3,7 @@ CONSTANTS   s_2 = False   s_1 = True-  s1 = 1 :: SWord8+  s1 = 1 :: Word8 TABLES ARRAYS UNINTERPRETED CONSTANTS
SBVUnitTest/GoldFiles/basic-5_5.gold view
@@ -4,7 +4,7 @@ CONSTANTS   s_2 = False   s_1 = True-  s2 = 1 :: SWord8+  s2 = 1 :: Word8 TABLES ARRAYS UNINTERPRETED CONSTANTS
SBVUnitTest/GoldFiles/ccitt.gold view
@@ -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
SBVUnitTest/GoldFiles/coins.gold view
@@ -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
SBVUnitTest/GoldFiles/counts.gold view
@@ -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
SBVUnitTest/GoldFiles/crcPolyExist.gold view
@@ -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
SBVUnitTest/GoldFiles/dogCatMouse.gold view
@@ -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.
SBVUnitTest/GoldFiles/euler185.gold view
@@ -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.
SBVUnitTest/GoldFiles/higher-9.gold view
@@ -1,2 +1,2 @@ Falsifiable. Counter-example:-  s0 = 128 :: SWord8+  s0 = 128 :: Word8
SBVUnitTest/GoldFiles/legato.gold view
@@ -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
SBVUnitTest/GoldFiles/temperature.gold view
@@ -1,5 +1,5 @@ Solution #1:-  s0 = 28 :: SInteger+  s0 = 28 :: Integer Solution #2:-  s0 = 16 :: SInteger+  s0 = 16 :: Integer Found 2 different solutions.
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -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"
SBVUnitTest/TestSuite/Puzzles/DogCatMouse.hs view
@@ -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
sbv.cabal view
@@ -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: <http://leventerkok.github.com/sbv/>-               .-               Release notes: <http://github.com/LeventErkok/sbv/blob/master/CHANGES.md>  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