sbv 5.9 → 5.10
raw patch · 16 files changed
+144/−87 lines, 16 files
Files
- CHANGES.md +76/−63
- Data/SBV.hs +2/−2
- Data/SBV/BitVectors/Data.hs +1/−1
- Data/SBV/BitVectors/Operations.hs +45/−5
- Data/SBV/BitVectors/Symbolic.hs +1/−1
- Data/SBV/Dynamic.hs +4/−1
- Data/SBV/Examples/Existentials/Diophantine.hs +1/−1
- Data/SBV/Examples/Misc/Floating.hs +3/−3
- Data/SBV/Examples/Puzzles/Counts.hs +1/−1
- Data/SBV/Examples/Puzzles/U2Bridge.hs +1/−1
- Data/SBV/SMT/SMTLib2.hs +1/−1
- Data/SBV/Tools/Polynomial.hs +1/−2
- INSTALL +1/−1
- README.md +4/−2
- SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
- sbv.cabal +1/−1
CHANGES.md view
@@ -1,8 +1,21 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 5.9, 2016-01-05+* Latest Hackage released version: 5.10, 2016-01-14 +### Version 5.10, 2016-01-14++ * Documentation: Fix a bunch of dead http links. Thanks to Andres Sicard-Ramirez+ for reporting.++ * Additions to the Dynamic API:++ * svSetBit : set a given bit+ * svBlastLE, svBlastBE : Bit-blast to big/little endian+ * svWordFromLE, svWordFromBE: Unblast from big/little endian+ * svAddConstant : Add a constant to an SVal+ * svIncrement, svDecrement : Add/subtract 1 from an SVal+ ### Version 5.9, 2016-01-05 * Default definition for 'symbolicMerge', which allows types that are@@ -41,8 +54,8 @@ ### Version 5.6, 2015-12-06 * Minor changes to how we print models:- * Align by the type- * Always print the type (previously we were skipping for Bool)+ * Align by the type+ * Always print the type (previously we were skipping for Bool) * Rework how SBV properties are quick-checked; much more usable and robust @@ -51,10 +64,10 @@ programmable API. (The dynamic version is called svQuickCheck) * Several changes/additions in support of the sbvPlugin development:- * Data.SBV.Dynamic: Define/export svFloat/svDouble/sReal/sNumerator/sDenominator- * Data.SBV.Internals: Export constructors of Result, SMTModel,- and the function showModel- * Simplify how Uninterpreted-types are internally represented.+ * Data.SBV.Dynamic: Define/export svFloat/svDouble/sReal/sNumerator/sDenominator+ * Data.SBV.Internals: Export constructors of Result, SMTModel,+ and the function showModel+ * Simplify how Uninterpreted-types are internally represented. ### Version 5.5, 2015-11-10 @@ -216,9 +229,9 @@ * fpRem : remainder * fpRoundToIntegral: truncating round - * fpMin : min- * fpMax : max- * fpIsEqualObject : FP equality as object (i.e., NaN equals NaN, +0 does not equal -0, etc.)+ * fpMin : min+ * fpMax : max+ * fpIsEqualObject : FP equality as object (i.e., NaN equals NaN, +0 does not equal -0, etc.) This brings SBV up-to par with everything supported by the SMT-Lib FP theory. @@ -317,11 +330,11 @@ * sRealToSFloat * sRealToSDouble * Between SWord32 and SFloat- * sWord32ToSFloat- * sFloatToSWord32+ * sWord32ToSFloat+ * sFloatToSWord32 * Between SWord64 and SDouble. (Relational, due to non-unique NaNs)- * sWord64ToSDouble- * sDoubleToSWord64+ * sWord64ToSDouble+ * sDoubleToSWord64 * From float to sign/exponent/mantissa fields: (Relational, due to non-unique NaNs) * blastSFloat * blastSDouble@@ -373,7 +386,7 @@ * Tracking changes in the SMT-Lib floating-point theory. If you are using symbolic floating-point types (i.e., SFloat and SDouble), then you should upgrade to this version and also get a very latest (unstable)- Z3 release. See http://smtlib.cs.uiowa.edu/theories/FloatingPoint.smt2+ Z3 release. See http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml for details. * Introduce a new class, 'RoundingFloat', which supports floating-point@@ -489,7 +502,7 @@ ### Version 3.1, 2014-07-12 - NB: GHC 7.8.1 and 7.8.2 has a serious bug (https://ghc.haskell.org/trac/ghc/ticket/9078)+ NB: GHC 7.8.1 and 7.8.2 has a serious bug <https://ghc.haskell.org/trac/ghc/ticket/9078> that causes SBV to crash under heavy/repeated calls. The bug is addressed in GHC 7.8.3; so upgrading to GHC 7.8.3 is essential for using SBV! @@ -498,33 +511,33 @@ * Using multiple-SMT solvers in parallel: * Added functions that let the user run multiple solvers, using asynchronous threads. All results can be obtained (proveWithAll, proveWithAny, satWithAll),- or SBV can return the fastest result (satWithAny, allSatWithAll, allSatWithAny).- These functions are good for playing with multiple-solvers, especially on- machines with multiple-cores.+ or SBV can return the fastest result (satWithAny, allSatWithAll, allSatWithAny).+ These functions are good for playing with multiple-solvers, especially on+ machines with multiple-cores. * Add function: sbvAvailableSolvers; which returns the list of solvers currently available, as installed on the machine we are running. (Not the list that SBV- supports, but those that are actually available at run-time.) This function- is useful with the multi-solve API.+ supports, but those that are actually available at run-time.) This function+ is useful with the multi-solve API. * Implement sBranch: * sBranch is a variant of 'ite' that consults the external SMT solver to see if a given branch condition is satisfiable- before evaluating it. This can make certain "otherwise recursive- and thus not-symbolically-terminating inputs" amenable to symbolic- simulation, if termination can be established this way. Needless- to say, this problem is always decidable as far as SBV programs- are concerned, but it does not mean the decision procedure is cheap!- Use with care. + before evaluating it. This can make certain otherwise recursive+ and thus not-symbolically-terminating inputs amenable to symbolic+ simulation, if termination can be established this way. Needless+ to say, this problem is always decidable as far as SBV programs+ are concerned, but it does not mean the decision procedure is cheap!+ Use with care. * sBranchTimeOut config parameter can be used to curtail long runs when sBranch is used. Of course, if time-out happens, SBV will- assume the branch is feasible, in which case symbolic-termination- may come back to bite you.)+ assume the branch is feasible, in which case symbolic-termination+ may come back to bite you.) * New API: * Add predicate 'isSNaN' which allows testing 'SFloat'/'SDouble' values for nan-ness. This is similar to the Prelude function 'isNaN', except- the Prelude version requires a RealFrac instance, which unfortunately is- not currently implementable for cases. (Requires trigonometric functions etc.)- Thus, we provide 'isSNaN' separately (along with the already existing- 'isFPPoint') to simplify reasoning with floating-point.+ the Prelude version requires a RealFrac instance, which unfortunately is+ not currently implementable for cases. (Requires trigonometric functions etc.)+ Thus, we provide 'isSNaN' separately (along with the already existing+ 'isFPPoint') to simplify reasoning with floating-point. * Examples: * Add Data/SBV/Examples/Misc/SBranch.hs, to illustrate the use of sBranch. * Bug fixes:@@ -573,7 +586,7 @@ * Other: * Allow users to specify the SMT-Lib logic to use, if necessary. SBV will still pick the logic automatically, but users can now override that choice.- Comes in handy when playing with custom logics.+ Comes in handy when playing with custom logics. * Bug fixes: * Address allsat-laziness issue (#78 in github issue tracker). Essentially, simplify how all-sat is called so we can avoid calling the solver for@@ -622,20 +635,20 @@ ### Version 2.9, 2013-01-02 - - Add support for the CVC4 SMT solver from New York University and- the University of Iowa. (http://cvc4.cs.nyu.edu/).+ * Add support for the CVC4 SMT solver from New York University and+ the University of Iowa. <http://cvc4.cs.nyu.edu/>. NB. Z3 remains the default solver for SBV. To use CVC4, use the *With variants of the interface (i.e., proveWith, satWith, ..) by passing cvc4 as the solver argument. (Similarly, use 'yices' as the argument for the *With functions for invoking yices.)- - Latest release of Yices calls the SMT-Lib based solver executable+ * Latest release of Yices calls the SMT-Lib based solver executable yices-smt. Updated the default value of the executable to have this name for ease of use.- - Add an extra boolean flag to compileToSMTLib and generateSMTBenchmarks+ * Add an extra boolean flag to compileToSMTLib and generateSMTBenchmarks functions to control if the translation should keep the query as is (for SAT cases), or negate it (for PROVE cases). Previously, this value was hard-coded to do the PROVE case only.- - Add bridge modules, to simplify use of different solvers. You can now say:+ * Add bridge modules, to simplify use of different solvers. You can now say: import Data.SBV.Bridge.CVC4 import Data.SBV.Bridge.Yices@@ -646,22 +659,22 @@ 'defaultSMTSolver' refers to z3 (currently), and 'sbvCurrentSolver' refers to the chosen solver as determined by the imported module. (The latter is useful for modifying options to the SMT solver in an solver-agnostic way.)- - Various improvements to Z3 model parsing routines.- - New web page for SBV: http://leventerkok.github.com/sbv/ is now online.+ * Various improvements to Z3 model parsing routines.+ * New web page for SBV: http://leventerkok.github.com/sbv/ is now online. ### Version 2.8, 2012-11-29 - - Rename the SNum class to SIntegral, and make it index over regular+ * Rename the SNum class to SIntegral, and make it index over regular types. This makes it much more useful, simplifying coding of polymorphic symbolic functions over integral types, which is the common case.- - Add the functions:- - sbvShiftLeft- - sbvShiftRight+ * Add the functions:+ * sbvShiftLeft+ * sbvShiftRight which can accommodate unsigned symbolic shift amounts. Note that one cannot use the Haskell shiftL/shiftR functions from the Bits class since they are hard-wired to take 'Int' values as the shift amounts only.- - Add a new function 'sbvArithShiftRight', which is the same as+ * Add a new function 'sbvArithShiftRight', which is the same as a shift-right, except it uses the MSB of the input as the bit to fill in (instead of always filling in with 0 bits). Note that this is the same as shiftRight for signed values, but differs from a shiftRight@@ -670,44 +683,44 @@ types and logical for unsigned ones.) This variant is designed for use cases when one uses the underlying unsigned SMT-Lib representation to implement custom signed operations, for instance.- - Several typo fixes.+ * Several typo fixes. ### Version 2.7, 2012-10-21 - - Add missing QuickCheck instance for SReal- - When dealing with concrete SReals, make sure to operate+ * Add missing QuickCheck instance for SReal+ * When dealing with concrete SReals, make sure to operate only on exact algebraic reals on the Haskell side, leaving true algebraic reals (i.e., those that are roots of polynomials that cannot be expressed as a rational) symbolic. This avoids issues with functions that we cannot implement directly on the Haskell side, like exact square-roots.- - Documentation tweaks, typo fixes etc.- - Rename BVDivisible class to SDivisible; since SInteger+ * Documentation tweaks, typo fixes etc.+ * Rename BVDivisible class to SDivisible; since SInteger is also an instance of this class, and SDivisible is a more appropriate name to start with. Also add sQuot and sRem methods; along with sDivMod, sDiv, and sMod, with usual semantics. - - Improve test suite, adding many constant-folding tests+ * Improve test suite, adding many constant-folding tests and start using cabal based tests (--enable-tests option.) ### Versions 2.4, 2.5, and 2.6: Around mid October 2012 - - Workaround issues related hackage compilation, in particular to the+ * Workaround issues related hackage compilation, in particular to the problem with the new containers package release, which does provide an NFData instance for sequences.- - Add explicit Num requirements when necessary, as the Bits class+ * Add explicit Num requirements when necessary, as the Bits class no longer does this.- - Remove dependency on the hackage package strict-concurrency, as+ * Remove dependency on the hackage package strict-concurrency, as hackage can no longer compile it due to some dependency mismatch.- - Add forgotten Real class instance for the type 'AlgReal'- - Stop putting bounds on hackage dependencies, as they cause+ * Add forgotten Real class instance for the type 'AlgReal'+ * Stop putting bounds on hackage dependencies, as they cause more trouble then they actually help. (See the discussion- here: http://www.haskell.org/pipermail/haskell-cafe/2012-July/102352.html.)+ here: <http://www.haskell.org/pipermail/haskell-cafe/2012-July/102352.html>.) ### Version 2.3, 2012-07-20 - - Maintanence release, no new features.- - Tweak cabal dependencies to avoid using packages that are newer+ * Maintanence release, no new features.+ * Tweak cabal dependencies to avoid using packages that are newer than those that come with ghc-7.4.2. Apparently this is a no-no that breaks many things, see the discussion in this thread: http://www.haskell.org/pipermail/haskell-cafe/2012-July/102352.html@@ -716,8 +729,8 @@ ### Version 2.2, 2012-07-17 - - Maintanence release, no new features.- - Update cabal dependencies, in particular fix the+ * Maintanence release, no new features.+ * Update cabal dependencies, in particular fix the regression with respect to latest version of the containers package. @@ -1088,7 +1101,7 @@ ### Version 0.9.14, 2011-03-19 - - Reimplement sharing using Stable names, inspired+ * Reimplement sharing using Stable names, inspired by the Data.Reify techniques. This avoids tricks with unsafe memory stashing, and hence is safe. Thus, issues with respect to CAFs are now resolved.
Data/SBV.hs view
@@ -96,7 +96,7 @@ -- -- * Yices from SRI: <http://yices.csl.sri.com/> ----- * Z3 from Microsoft: <http://z3.codeplex.com/>+-- * Z3 from Microsoft: <http://github.com/Z3Prover/z3/wiki> -- -- SBV also allows calling these solvers in parallel, either getting results from multiple solvers -- or returning the fastest one. (See 'proveWithAll', 'proveWithAny', etc.)@@ -655,7 +655,7 @@ others are not (such as pi and e). SBV can deal with real numbers just fine, since the theory of reals is decidable. (See-<http://smtlib.cs.uiowa.edu/theories/Reals.smt2>.) In addition, by leveraging backend+<http://smtlib.cs.uiowa.edu/theories-Reals.shtml>.) In addition, by leveraging backend solver capabilities, SBV can also represent and solve non-linear equations involving real-variables. (For instance, the Z3 SMT solver, supports polynomial constraints on reals starting with v4.0.) -}
Data/SBV/BitVectors/Data.hs view
@@ -379,7 +379,7 @@ -- Merging pushes the if-then-else choice down on to elements mergeArrays :: SymWord b => SBV Bool -> array a b -> array a b -> array a b --- | Arrays implemented in terms of SMT-arrays: <http://smtlib.cs.uiowa.edu/theories/ArraysEx.smt2>+-- | Arrays implemented in terms of SMT-arrays: <http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml> -- -- * Maps directly to SMT-lib arrays --
Data/SBV/BitVectors/Operations.hs view
@@ -9,6 +9,8 @@ -- Constructors and basic operations on symbolic values ----------------------------------------------------------------------------- +{-# LANGUAGE BangPatterns #-}+ module Data.SBV.BitVectors.Operations ( -- ** Basic constructors@@ -27,12 +29,14 @@ , svUninterpreted , svIte, svLazyIte, svSymbolicMerge , svSelect- , svSign, svUnsign+ , svSign, svUnsign, svSetBit, svWordFromBE, svWordFromLE , svExp -- ** Derived operations , svToWord1, svFromWord1, svTestBit , svShiftLeft, svShiftRight , svRotateLeft, svRotateRight+ , svBlastLE, svBlastBE+ , svAddConstant, svIncrement, svDecrement ) where @@ -156,11 +160,47 @@ svExp :: SVal -> SVal -> SVal svExp b e | hasSign (kindOf e) = error "svExp: exponentiation only works with unsigned exponents" | True = prod $ zipWith (\use n -> svIte use n one)- (blastLE e)+ (svBlastLE e) (iterate (\x -> svTimes x x) b)- where blastLE x = map (svTestBit x) [0 .. intSizeOf x - 1]- prod = foldr svTimes one- one = svInteger (kindOf b) 1+ where prod = foldr svTimes one+ one = svInteger (kindOf b) 1++-- | Bit-blast: Little-endian. Assumes the input is a bit-vector.+svBlastLE :: SVal -> [SVal]+svBlastLE x = map (svTestBit x) [0 .. intSizeOf x - 1]++-- | Set a given bit at index+svSetBit :: SVal -> Int -> SVal+svSetBit x i = x `svXOr` svInteger (kindOf x) (bit i :: Integer)++-- | Bit-blast: Big-endian. Assumes the input is a bit-vector.+svBlastBE :: SVal -> [SVal]+svBlastBE = reverse . svBlastLE++-- | Un-bit-blast from big-endian representation to a word of the right size.+-- The input is assumed to be unsigned.+svWordFromLE :: [SVal] -> SVal+svWordFromLE bs = go zero 0 bs+ where zero = svInteger (KBounded False (length bs)) 0+ go !acc _ [] = acc+ go !acc !i (x:xs) = go (svIte x (svSetBit acc i) acc) (i+1) xs++-- | Un-bit-blast from little-endian representation to a word of the right size.+-- The input is assumed to be unsigned.+svWordFromBE :: [SVal] -> SVal+svWordFromBE = svWordFromLE . reverse++-- | Add a constant value:+svAddConstant :: Integral a => SVal -> a -> SVal+svAddConstant x i = x `svPlus` svInteger (kindOf x) (fromIntegral i)++-- | Increment:+svIncrement :: SVal -> SVal+svIncrement x = svAddConstant x (1::Integer)++-- | Decrement:+svDecrement :: SVal -> SVal+svDecrement x = svAddConstant x (-1 :: Integer) -- | Quotient: Overloaded operation whose meaning depends on the kind at which -- it is used: For unbounded integers, it corresponds to the SMT-Lib
Data/SBV/BitVectors/Symbolic.hs view
@@ -772,7 +772,7 @@ -- * Symbolic Arrays --------------------------------------------------------------------------------- --- | Arrays implemented in terms of SMT-arrays: <http://smtlib.cs.uiowa.edu/theories/ArraysEx.smt2>+-- | Arrays implemented in terms of SMT-arrays: <http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml> -- -- * Maps directly to SMT-lib arrays --
Data/SBV/Dynamic.hs view
@@ -45,6 +45,7 @@ -- *** Arithmetic operations , svPlus, svTimes, svMinus, svUNeg, svAbs , svDivide, svQuot, svRem, svExp+ , svAddConstant, svIncrement, svDecrement -- *** Logical operations , svAnd, svOr, svXOr, svNot , svShl, svShr, svRol, svRor@@ -55,9 +56,11 @@ -- *** Indexed lookups , svSelect -- *** Word-level operations- , svToWord1, svFromWord1, svTestBit+ , svToWord1, svFromWord1, svTestBit, svSetBit , svShiftLeft, svShiftRight , svRotateLeft, svRotateRight+ , svWordFromBE, svWordFromLE+ , svBlastLE, svBlastBE -- ** Conditionals: Mergeable values , svIte, svLazyIte, svSymbolicMerge , svIsSatisfiableInCurrentPath
Data/SBV/Examples/Existentials/Diophantine.hs view
@@ -46,7 +46,7 @@ -- statement that a solution is in the basis if it's least according to the lexicographic -- order using the ordinary less-than relation. (NB. We explicitly tell z3 to use the logic -- AUFLIA for this problem, as the BV solver that is chosen automatically has a performance--- issue. See: https://z3.codeplex.com/workitem/88.)+-- issue. See: <https://z3.codeplex.com/workitem/88>.) basis :: [[SInteger]] -> IO [[Integer]] basis m = extractModels `fmap` allSatWith z3{useLogic = Just (PredefinedLogic AUFLIA)} cond where cond = do as <- mkExistVars n
Data/SBV/Examples/Misc/Floating.hs view
@@ -118,13 +118,13 @@ -- -- >>> multInverse -- Falsifiable. Counter-example:--- a = 1.1058928764217435e308 :: Double+-- a = -7.883512939128398e-261 :: Double -- -- Indeed, we have: ----- >>> let a = 1.1058928764217435e308 :: Double+-- >>> let a = -7.883512939128398e-261 :: Double -- >>> a * (1/a)--- 0.9999999999999998+-- 0.9999999999999999 multInverse :: IO ThmResult multInverse = prove $ do a <- sDouble "a" constrain $ fpIsPoint a
Data/SBV/Examples/Puzzles/Counts.hs view
@@ -21,7 +21,7 @@ -- -- * Douglas Hofstadter, Metamagical Themes, pg. 27. ----- * <http://www.lboro.ac.uk/departments/ma/gallery/selfref/index.html>+-- * <http://mathcentral.uregina.ca/mp/archives/previous2002/dec02sol.html> -- -----------------------------------------------------------------------------
Data/SBV/Examples/Puzzles/U2Bridge.hs view
@@ -6,7 +6,7 @@ -- Maintainer : erkokl@gmail.com -- Stability : experimental ----- The famous U2 bridge crossing puzzle: <http://www.brainj.net/puzzle.php?id=u2>+-- The famous U2 bridge crossing puzzle: <http://www.braingle.com/brainteasers/515/u2.html> ----------------------------------------------------------------------------- {-# LANGUAGE DeriveAnyClass #-}
Data/SBV/SMT/SMTLib2.hs view
@@ -506,7 +506,7 @@ ] -------------------------------------------------------------------------------------------------- Casts supported by SMTLib. (From: http://smtlib.cs.uiowa.edu/theories/FloatingPoint.smt2)+-- Casts supported by SMTLib. (From: <http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml>) -- ; from another floating point sort -- ((_ to_fp eb sb) RoundingMode (_ FloatingPoint mb nb) (_ FloatingPoint eb sb)) --
Data/SBV/Tools/Polynomial.hs view
@@ -216,8 +216,7 @@ -- since CRC polynomials are designed and expressed this way. -- -- NB. The literature on CRC's has many variants on how CRC's are computed.--- We follow the painless guide (<http://www.ross.net/crc/download/crc_v3.txt>)--- and compute the CRC as follows:+-- We follow the following simple procedure: -- -- * Extend the message 'm' by adding 'n' 0 bits on the right --
INSTALL view
@@ -12,7 +12,7 @@ highly recommended that you run this program to ensure everything is working correctly. In particular, you will first need to install Z3, the default SMT solver used by sbv, from Microsoft. (You can get it-from http://github.com/Z3Prover/z3.)+from <http://github.com/Z3Prover/z3>.) Please make sure that the "z3" executable is in your path. Once you have installed sbv, you can use it in your Haskell programs
README.md view
@@ -1,6 +1,8 @@ ## SBV: SMT Based Verification in Haskell -[](http://hackage.haskell.org/package/sbv)- [](http://travis-ci.org/LeventErkok/sbv)+[]+ (http://hackage.haskell.org/package/sbv)+[]+ (http://travis-ci.org/LeventErkok/sbv) Please see: http://leventerkok.github.com/sbv/
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String-buildTime = "Tue Jan 5 17:59:03 PST 2016"+buildTime = "Thu Jan 14 21:27:52 PST 2016"
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 5.9+Version: 5.10 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