sbv 1.4 → 2.0

raw patch · 4 files changed

+40/−5 lines, 4 files

Files

• RELEASENOTES +8/−3
• SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
• SBVUnitTest/TestSuite/BitPrecise/MergeSort.hs +29/−0
• sbv.cabal +2/−1

@@ -1,12 +1,12 @@ Hackage: <http://hackage.haskell.org/package/sbv> GitHub:  <http://github.com/LeventErkok/sbv> -Latest Hackage released version: 1.4+Latest Hackage released version: 2.0  ======================================================================-Version 1.4, 2012-05-10+Version 2.0, 2012-05-10   -  The major change in this release is the support for symbolic algebraic reals: SReal.+  This is a major release of SBV, adding support for symbolic algebraic reals: SReal.   See http://en.wikipedia.org/wiki/Algebraic_number for details. In brief, algebraic   reals are solutions to univariate polynomials with rational coefficients. The arithmetic   on algebraic reals is precise, with no approximation errors. Note that algebraic reals@@ -56,6 +56,11 @@    * Change dog-cat-mouse example to use SInteger for the counts    * Add merge-sort example: Data.SBV.Examples.BitPrecise.MergeSort    * Add diophantine solver example: Data.SBV.Examples.Existentials.Diophantine++======================================================================+Version 1.4, 2012-05-10++   * Interim release for test purposes  ====================================================================== Version 1.3, 2012-02-25

@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where  buildTime :: String-buildTime = "Wed May  9 22:17:47 PDT 2012"+buildTime = "Thu May 10 00:22:26 PDT 2012"

@@ -0,0 +1,29 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  TestSuite.BitPrecise.MergeSort+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+-- Portability :  portable+--+-- Test suite for Data.SBV.Examples.BitPrecise.MergeSort+-----------------------------------------------------------------------------++module TestSuite.BitPrecise.MergeSort where++import Data.SBV+import Data.SBV.Internals+import Data.SBV.Examples.BitPrecise.MergeSort++import SBVTest++-- Test suite+testSuite :: SBVTestSuite+testSuite = mkTestSuite $ \goldCheck -> test [+   "mergeSort" ~: mergeC `goldCheck` "merge.gold"+ ]+ where mergeC = compileToC' "merge" $ do+                   cgSetDriverValues [10, 6, 4, 82, 71]+                   xs <- cgInputArr 5 "xs"+                   cgOutputArr "ys" (mergeSort xs)

@@ -1,5 +1,5 @@ Name:          sbv-Version:       1.4+Version:       2.0 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@@ -190,6 +190,7 @@                   , TestSuite.Basics.QRem                   , TestSuite.BitPrecise.BitTricks                   , TestSuite.BitPrecise.Legato+                  , TestSuite.BitPrecise.MergeSort                   , TestSuite.BitPrecise.PrefixSum                   , TestSuite.CodeGeneration.AddSub                   , TestSuite.CodeGeneration.CgTests