sbv 0.9.19 → 0.9.20
raw patch · 2 files changed
+27/−1 lines, 2 files
Files
- Data/SBV/TestSuite/Puzzles/Counts.hs +25/−0
- sbv.cabal +2/−1
+ Data/SBV/TestSuite/Puzzles/Counts.hs view
@@ -0,0 +1,25 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.SBV.TestSuite.Puzzles.Counts+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+-- Portability : portable+--+-- Test suite for Data.SBV.Examples.Puzzles.Counts+-----------------------------------------------------------------------------++module Data.SBV.TestSuite.Puzzles.Counts(testSuite) where++import Data.SBV+import Data.SBV.Internals+import Data.SBV.Examples.Puzzles.Counts++-- Test suite+testSuite :: SBVTestSuite+testSuite = mkTestSuite $ \goldCheck -> test [+ "counts" ~: countPgm `goldCheck` "counts.gold"+ ]+ where countPgm = runSymbolic $ forAll_ puzzle' >>= output+ puzzle' d0 d1 d2 d3 d4 d5 d6 d7 d8 d9 = puzzle [d0, d1, d2, d3, d4, d5, d6, d7, d8, d9]
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 0.9.19+Version: 0.9.20 Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math Synopsis: Symbolic bit vectors: Bit-precise verification and automatic C-code generation. Description: Express properties about bit-precise Haskell programs and automatically prove@@ -166,6 +166,7 @@ , Data.SBV.TestSuite.CRC.Parity , Data.SBV.TestSuite.CRC.USB5 , Data.SBV.TestSuite.Polynomials.Polynomials+ , Data.SBV.TestSuite.Puzzles.Counts , Data.SBV.TestSuite.Puzzles.DogCatMouse , Data.SBV.TestSuite.Puzzles.Euler185 , Data.SBV.TestSuite.Puzzles.MagicSquare