sbv 0.9.10 → 0.9.11
raw patch · 4 files changed
+36/−14 lines, 4 filessetup-changed
Files
- Data/SBV/BitVectors/Data.hs +1/−1
- Data/SBV/TestSuite/Puzzles/Euler185.hs +23/−0
- Setup.hs +10/−12
- sbv.cabal +2/−1
Data/SBV/BitVectors/Data.hs view
@@ -113,7 +113,7 @@ | ArrRead Int | Uninterpreted String deriving (Eq, Ord)-data SBVExpr = SBVApp {-# UNPACK #-} !Op {-# UNPACK #-} ![SW]+data SBVExpr = SBVApp !Op ![SW] deriving (Eq, Ord) class HasSignAndSize a where
+ Data/SBV/TestSuite/Puzzles/Euler185.hs view
@@ -0,0 +1,23 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.SBV.TestSuite.Puzzles.Euler185+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+-- Portability : portable+--+-- Test suite for Data.SBV.Examples.Puzzles.Euler185+-----------------------------------------------------------------------------++module Data.SBV.TestSuite.Puzzles.Euler185(testSuite) where++import Data.SBV+import Data.SBV.Internals+import Data.SBV.Examples.Puzzles.Euler185++-- Test suite+testSuite :: SBVTestSuite+testSuite = mkTestSuite $ \goldCheck -> test [+ "euler185" ~: allSat euler185 `goldCheck` "euler185.gold"+ ]
Setup.hs view
@@ -13,9 +13,8 @@ {-# OPTIONS_GHC -Wall #-} module Main(main) where -import Control.Monad (when) import Distribution.PackageDescription (executables, modulePath, package, maintainer, customFieldsBI, homepage, exeName, buildInfo)-import Distribution.Simple (defaultMainWithHooks, simpleUserHooks, runTests, postInst)+import Distribution.Simple (defaultMainWithHooks, simpleUserHooks, postInst) import Distribution.Simple.LocalBuildInfo (LocalBuildInfo(..)) import Distribution.Text (display) import System.Directory (findExecutable)@@ -25,7 +24,7 @@ import Data.SBV.Provers.Prover (SMTSolver(..), yices) main :: IO ()-main = defaultMainWithHooks simpleUserHooks{ runTests = unittest True, postInst = unittest False}+main = defaultMainWithHooks simpleUserHooks{ postInst = unittest } where checkDefSolver = do let ex = executable yices nm = name yices@@ -35,7 +34,7 @@ putStrLn $ "*** The executable " ++ show ex ++ " must be in your path." putStrLn $ "*** Do not forget to install " ++ nm ++ "!" Just _ -> return ()- unittest forced _ _ _ lbi = do+ unittest _ _ _ lbi = do let testers = [ex | ex <- executables pkgDesc, modulePath ex == "SBVUnitTest/SBVUnitTest.hs"] case testers of [tp] -> runTester tp@@ -47,14 +46,13 @@ report exitWith $ ExitFailure 1 runTester tp = do- when (not forced) $- case lookup "x-run-unittests" (customFieldsBI (buildInfo tp)) of- Just "False" -> do checkDefSolver- putStrLn "*** Please run \"SBVUnitTests\" executable to perform unit-tests."- putStrLn $ "*** Package " ++ sbvName ++ " installed successfully. Enjoy!"- putStrLn $ "*** Further info: " ++ homepage pkgDesc- exitWith ExitSuccess- _ -> return ()+ case lookup "x-run-unittests" (customFieldsBI (buildInfo tp)) of+ Just "False" -> do checkDefSolver+ putStrLn "*** Please run \"SBVUnitTests\" executable to perform unit-tests."+ putStrLn $ "*** Package " ++ sbvName ++ " installed successfully. Enjoy!"+ putStrLn $ "*** Further info: " ++ homepage pkgDesc+ exitWith ExitSuccess+ _ -> return () mbP <- findExecutable $ exeName tp case mbP of Nothing -> bailOut
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 0.9.10+Version: 0.9.11 Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math Synopsis: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers. Description: Express properties about bit-precise Haskell programs and automatically prove@@ -139,6 +139,7 @@ , Data.SBV.TestSuite.PrefixSum.PrefixSum , Data.SBV.TestSuite.Polynomials.Polynomials , Data.SBV.TestSuite.Puzzles.DogCatMouse+ , Data.SBV.TestSuite.Puzzles.Euler185 , Data.SBV.TestSuite.Puzzles.MagicSquare , Data.SBV.TestSuite.Puzzles.NQueens , Data.SBV.TestSuite.Puzzles.PowerSet