diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,16 @@ * Hackage: * GitHub: -* Latest Hackage released version: 5.2, 2015-10-12 +* Latest Hackage released version: 5.3, 2015-10-20 + +### Version 5.3, 2015-10-20 + + * Main point of this release to make SBV compile with GHC 7.8 again, to accommodate mainly + for Cryptol. As Cryptol moves to GHC >= 7.10, we intend to remove the "compatibility" changes + again. Thanks to Adam Foltzer for the patch. + + * Minor mods to how bitvector equality/inequality are translated to SMTLib. No user visible + impact. ### Version 5.2, 2015-10-12 diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -107,6 +107,12 @@ {-# LANGUAGE FlexibleInstances #-} +-- TODO: remove OverlappingInstances and these warning suppressions +-- once support is dropped for GHC 7.8 +{-# OPTIONS_GHC -fno-warn-deprecated-flags #-} +{-# OPTIONS_GHC -fno-warn-unrecognised-pragmas #-} +{-# LANGUAGE OverlappingInstances #-} + module Data.SBV ( -- * Programming with symbolic values -- $progIntro diff --git a/Data/SBV/BitVectors/Data.hs b/Data/SBV/BitVectors/Data.hs --- a/Data/SBV/BitVectors/Data.hs +++ b/Data/SBV/BitVectors/Data.hs @@ -67,6 +67,9 @@ import Data.SBV.BitVectors.Concrete import Data.SBV.BitVectors.Symbolic +import Prelude () +import Prelude.Compat + -- | A class for capturing values that have a sign and a size (finite or infinite) -- minimal complete definition: kindOf. This class can be automatically derived -- for data-types that have a 'Data' instance; this is useful for creating uninterpreted diff --git a/Data/SBV/BitVectors/Model.hs b/Data/SBV/BitVectors/Model.hs --- a/Data/SBV/BitVectors/Model.hs +++ b/Data/SBV/BitVectors/Model.hs @@ -854,10 +854,12 @@ -- this operation. One issue is how division by 0 behaves. The verification -- technology requires total functions, and there are several design choices -- here. We follow Isabelle/HOL approach of assigning the value 0 for division --- by 0. Therefore, we impose the following law: +-- by 0. Therefore, we impose the following pair of laws: -- --- @ x `sQuotRem` 0 = (0, x) @ --- @ x `sDivMod` 0 = (0, x) @ +-- @ +-- x `sQuotRem` 0 = (0, x) +-- x `sDivMod` 0 = (0, x) +-- @ -- -- Note that our instances implement this law even when @x@ is @0@ itself. -- diff --git a/Data/SBV/BitVectors/Symbolic.hs b/Data/SBV/BitVectors/Symbolic.hs --- a/Data/SBV/BitVectors/Symbolic.hs +++ b/Data/SBV/BitVectors/Symbolic.hs @@ -63,6 +63,7 @@ import Data.Maybe (isJust, fromJust, fromMaybe) import qualified Data.Generics as G (Data(..)) +import qualified Data.Typeable as T (Typeable) import qualified Data.IntMap as IMap (IntMap, empty, size, toAscList, lookup, insert, insertWith) import qualified Data.Map as Map (Map, empty, toList, size, insert, lookup) import qualified Data.Set as Set (Set, empty, toList, insert) @@ -75,6 +76,9 @@ import Data.SBV.BitVectors.Kind import Data.SBV.BitVectors.Concrete +import Prelude () +import Prelude.Compat + -- | A symbolic node id newtype NodeId = NodeId Int deriving (Eq, Ord) @@ -1019,7 +1023,7 @@ | RoundTowardPositive -- ^ Round towards positive infinity. (Also known as rounding-up or ceiling.) | RoundTowardNegative -- ^ Round towards negative infinity. (Also known as rounding-down or floor.) | RoundTowardZero -- ^ Round towards zero. (Also known as truncation.) - deriving (Eq, Ord, Show, Read, G.Data, Bounded, Enum) + deriving (Eq, Ord, Show, Read, T.Typeable, G.Data, Bounded, Enum) -- | Solver configuration. See also 'z3', 'yices', 'cvc4', 'boolector', 'mathSAT', etc. which are instantiations of this type for those solvers, with -- reasonable defaults. In particular, custom configuration can be created by varying those values. (Such as @z3{verbose=True}@.) diff --git a/Data/SBV/Compilers/CodeGen.hs b/Data/SBV/Compilers/CodeGen.hs --- a/Data/SBV/Compilers/CodeGen.hs +++ b/Data/SBV/Compilers/CodeGen.hs @@ -14,8 +14,9 @@ module Data.SBV.Compilers.CodeGen where +import Control.Monad (filterM, replicateM, unless) import Control.Monad.Trans -import Control.Monad.State.Lazy +import Control.Monad.State.Lazy (MonadState, StateT(..), modify) import Data.Char (toLower, isSpace) import Data.List (nub, isPrefixOf, intercalate, (\\)) import System.Directory (createDirectory, doesDirectoryExist, doesFileExist) @@ -26,6 +27,9 @@ import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.Symbolic (svToSymSW, svMkSymVar, outputSVal) + +import Prelude () +import Prelude.Compat -- | Abstract over code generation for different languages class CgTarget a where diff --git a/Data/SBV/Dynamic.hs b/Data/SBV/Dynamic.hs --- a/Data/SBV/Dynamic.hs +++ b/Data/SBV/Dynamic.hs @@ -62,7 +62,7 @@ -- ** Proving properties , proveWith -- ** Checking satisfiability - , satWith + , satWith, allSatWith -- * Proving properties using multiple solvers , proveWithAll, proveWithAny, satWithAll, satWithAny -- * Model extraction @@ -130,7 +130,7 @@ import qualified Data.SBV as SBV (SBool, proveWithAll, proveWithAny, satWithAll, satWithAny) import qualified Data.SBV.BitVectors.Data as SBV (SBV(..)) import qualified Data.SBV.BitVectors.Model as SBV (isSatisfiableInCurrentPath) -import qualified Data.SBV.Provers.Prover as SBV (proveWith, satWith, compileToSMTLib, generateSMTBenchmarks) +import qualified Data.SBV.Provers.Prover as SBV (proveWith, satWith, allSatWith, compileToSMTLib, generateSMTBenchmarks) import qualified Data.SBV.SMT.SMT as SBV (Modelable(getModel, getModelDictionary)) -- | Reduce a condition (i.e., try to concretize it) under the given path @@ -170,6 +170,10 @@ -- | Find a satisfying assignment using the given SMT-solver satWith :: SMTConfig -> Symbolic SVal -> IO SatResult satWith cfg s = SBV.satWith cfg (fmap toSBool s) + +-- | Find all satisfying assignments using the given SMT-solver +allSatWith :: SMTConfig -> Symbolic SVal -> IO AllSatResult +allSatWith cfg s = SBV.allSatWith cfg (fmap toSBool s) -- | Prove a property with multiple solvers, running them in separate threads. The -- results will be returned in the order produced. diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -349,10 +349,8 @@ lift1B bOp vOp | boolOp = lift1 bOp | True = lift1 vOp - eqBV sgn sbvs - | boolOp = lift2 "=" sgn sbvs - | True = "(= " ++ lift2 "bvcomp" sgn sbvs ++ " #b1)" - neqBV sgn sbvs = "(not " ++ eqBV sgn sbvs ++ ")" + eqBV = lift2 "=" + neqBV = lift2 "distinct" equal sgn sbvs | doubleOp = lift2 "fp.eq" sgn sbvs | floatOp = lift2 "fp.eq" sgn sbvs diff --git a/SBVUnitTest/SBVUnitTestBuildTime.hs b/SBVUnitTest/SBVUnitTestBuildTime.hs --- a/SBVUnitTest/SBVUnitTestBuildTime.hs +++ b/SBVUnitTest/SBVUnitTestBuildTime.hs @@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String -buildTime = "Sun Oct 11 23:08:47 PDT 2015" +buildTime = "Tue Oct 20 20:01:47 PDT 2015" diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,5 +1,5 @@ Name: sbv -Version: 5.2 +Version: 5.3 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 @@ -30,7 +30,6 @@ other-extensions: BangPatterns DefaultSignatures DeriveDataTypeable - DeriveAnyClass FlexibleContexts FlexibleInstances FunctionalDependencies @@ -45,7 +44,10 @@ TupleSections TypeOperators TypeSynonymInstances - Build-Depends : base >= 4 && < 5 + if impl(ghc >= 7.10.1) + other-extensions: DeriveAnyClass + Build-Depends : base >= 4.7 && < 5 + , base-compat >= 0.6 , array, async, containers, deepseq, directory, filepath, old-time , pretty, process, mtl, QuickCheck, random, syb, data-binary-ieee754 , crackNum @@ -58,43 +60,44 @@ , Data.SBV.Bridge.ABC , Data.SBV.Dynamic , Data.SBV.Internals - , Data.SBV.Examples.BitPrecise.BitTricks - , Data.SBV.Examples.BitPrecise.Legato - , Data.SBV.Examples.BitPrecise.MergeSort - , Data.SBV.Examples.BitPrecise.MultMask - , Data.SBV.Examples.BitPrecise.PrefixSum - , Data.SBV.Examples.CodeGeneration.AddSub - , Data.SBV.Examples.CodeGeneration.CRC_USB5 - , Data.SBV.Examples.CodeGeneration.Fibonacci - , Data.SBV.Examples.CodeGeneration.GCD - , Data.SBV.Examples.CodeGeneration.PopulationCount - , Data.SBV.Examples.CodeGeneration.Uninterpreted - , Data.SBV.Examples.Crypto.AES - , Data.SBV.Examples.Crypto.RC4 - , Data.SBV.Examples.Existentials.CRCPolynomial - , Data.SBV.Examples.Existentials.Diophantine - , Data.SBV.Examples.Misc.Enumerate - , Data.SBV.Examples.Misc.Floating - , Data.SBV.Examples.Misc.ModelExtract - , Data.SBV.Examples.Misc.Word4 - , Data.SBV.Examples.Polynomials.Polynomials - , Data.SBV.Examples.Puzzles.Birthday - , Data.SBV.Examples.Puzzles.Coins - , Data.SBV.Examples.Puzzles.Counts - , Data.SBV.Examples.Puzzles.DogCatMouse - , Data.SBV.Examples.Puzzles.Euler185 - , Data.SBV.Examples.Puzzles.Fish - , Data.SBV.Examples.Puzzles.MagicSquare - , Data.SBV.Examples.Puzzles.NQueens - , Data.SBV.Examples.Puzzles.SendMoreMoney - , Data.SBV.Examples.Puzzles.Sudoku - , Data.SBV.Examples.Puzzles.U2Bridge - , Data.SBV.Examples.Uninterpreted.AUF - , Data.SBV.Examples.Uninterpreted.Deduce - , Data.SBV.Examples.Uninterpreted.Function - , Data.SBV.Examples.Uninterpreted.Shannon - , Data.SBV.Examples.Uninterpreted.Sort - , Data.SBV.Examples.Uninterpreted.UISortAllSat + if impl(ghc >= 7.10.1) + exposed-modules : Data.SBV.Examples.BitPrecise.BitTricks + , Data.SBV.Examples.BitPrecise.Legato + , Data.SBV.Examples.BitPrecise.MergeSort + , Data.SBV.Examples.BitPrecise.MultMask + , Data.SBV.Examples.BitPrecise.PrefixSum + , Data.SBV.Examples.CodeGeneration.AddSub + , Data.SBV.Examples.CodeGeneration.CRC_USB5 + , Data.SBV.Examples.CodeGeneration.Fibonacci + , Data.SBV.Examples.CodeGeneration.GCD + , Data.SBV.Examples.CodeGeneration.PopulationCount + , Data.SBV.Examples.CodeGeneration.Uninterpreted + , Data.SBV.Examples.Crypto.AES + , Data.SBV.Examples.Crypto.RC4 + , Data.SBV.Examples.Existentials.CRCPolynomial + , Data.SBV.Examples.Existentials.Diophantine + , Data.SBV.Examples.Misc.Enumerate + , Data.SBV.Examples.Misc.Floating + , Data.SBV.Examples.Misc.ModelExtract + , Data.SBV.Examples.Misc.Word4 + , Data.SBV.Examples.Polynomials.Polynomials + , Data.SBV.Examples.Puzzles.Birthday + , Data.SBV.Examples.Puzzles.Coins + , Data.SBV.Examples.Puzzles.Counts + , Data.SBV.Examples.Puzzles.DogCatMouse + , Data.SBV.Examples.Puzzles.Euler185 + , Data.SBV.Examples.Puzzles.Fish + , Data.SBV.Examples.Puzzles.MagicSquare + , Data.SBV.Examples.Puzzles.NQueens + , Data.SBV.Examples.Puzzles.SendMoreMoney + , Data.SBV.Examples.Puzzles.Sudoku + , Data.SBV.Examples.Puzzles.U2Bridge + , Data.SBV.Examples.Uninterpreted.AUF + , Data.SBV.Examples.Uninterpreted.Deduce + , Data.SBV.Examples.Uninterpreted.Function + , Data.SBV.Examples.Uninterpreted.Shannon + , Data.SBV.Examples.Uninterpreted.Sort + , Data.SBV.Examples.Uninterpreted.UISortAllSat Other-modules : Data.SBV.BitVectors.AlgReals , Data.SBV.BitVectors.Concrete , Data.SBV.BitVectors.Data @@ -131,12 +134,16 @@ Executable SBVUnitTests default-language: Haskell2010 ghc-options : -Wall - other-extensions: Rank2Types + other-extensions: DeriveAnyClass + Rank2Types RankNTypes ScopedTypeVariables TupleSections - Build-depends : base >= 4 && < 5 + if impl(ghc >= 7.10.1) + Build-depends : base >= 4.8 && < 5 , HUnit, directory, filepath, process, syb, sbv, data-binary-ieee754 + else + Buildable : False Hs-Source-Dirs : SBVUnitTest main-is : SBVUnitTest.hs Other-modules : SBVUnitTestBuildTime @@ -206,8 +213,11 @@ type : exitcode-stdio-1.0 default-language: Haskell2010 ghc-options : -Wall -with-rtsopts=-K64m - Build-depends : base >= 4 && < 5 + if impl(ghc >= 7.10.1) + Build-depends : base >= 4.8 && < 5 , HUnit, directory, filepath, syb, sbv, data-binary-ieee754 + else + Buildable : False Hs-Source-Dirs : SBVUnitTest main-is : SBVBasicTests.hs Other-modules : SBVBasicTests