diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,8 +1,15 @@ * Hackage: * GitHub: -* Latest Hackage released version: 9.8.2, 2024-03-23 +### Version 9.12.1, 2025-03-12 + * Changes required to compile with GHC 9.12.1 + * Add support for CVC5, DReal, OpenSMT, and Bitwuzla as backend solvers + * Bump up sbv dependence to >= 11.4 +### Version 9.10.1, 2024-01-05 + * Changes required to compile with GHC 9.10.1 + * Bump up sbv dependence to >= 10.10 + ### Version 9.8.2, 2024-01-05 * Changes required to compile with GHC 9.8.2 * Bump up sbv dependence to >= 10.7 @@ -34,23 +41,19 @@ * Bump up sbv dependence to >= 8.8 ### Version 0.11, 2019-01-14 - * Changes required to compile with GHC 8.6.3 * Bump up sbv dependence to >= 8.0 * Clean-up/improve test cases ### Version 0.10, 2017-07-29 - * Changes required to compile with GHC 8.2.1/8.2.2. * Bump up sbv dependence to >= 7.4 ### Version 0.9, 2017-07-19 - * Sync-up with recent modifications to SBV. No user visible changes. * Bump up sbv dependence to >= 7.0 ### Version 0.8, 2017-01-12 - * Fix broken links, thanks to Stephan Renatus for the patch. * Add the 'Proved' type, which allows for easily tagging a type for proof, without the need for an explicit annotation. Thanks to Nickolas Fotopoulos @@ -58,12 +61,10 @@ * Bump up sbv dependence to > 5.14 ### Version 0.7, 2016-06-06 - * Compile with GHC-8.0. Plugin at least requires GHC-8.0.1 and SBV 5.12 * Fix a few dead links ### Version 0.6, 2016-01-01 - * Support for list expressions of the form [x .. y] and [x, y .. z]; so long as the x, y, and z are all concrete. * Simplify some of the expressions in BitTricks using @@ -71,7 +72,6 @@ * Added more proofs to the BitTricks example ### Version 0.5, 2015-12-26 - * Allow higher-order (i.e., function) arguments to theorems. * Rework uninterpreted functions, generalize types * Simplify cabal file; no need to ship gold-files for tests @@ -79,7 +79,6 @@ * Add bit-tricks example "Data/SBV/Plugin/Examples/BitTricks.hs" ### Version 0.4, 2015-12-24 - * Support for case-alternatives producing lists/tuples and functions. In the list case, we require that both alternatives produce equal-length lists, as otherwise @@ -87,7 +86,6 @@ * More test cases. ### Version 0.3, 2015-12-21 - * Added the micro-controller example, adapted from the original SBV variant by Anthony Cowley: @@ -95,14 +93,12 @@ compiling the plugin itself! ### Version 0.2, 2015-12-21 - * Further fleshing of internals * Support for case-expressions * Support for uninterpreted types/functions * Lots of test cases, refactoring. ### Version 0.1, 2015-12-06 - * Basic functionality. Initial design exploration. * The plugin functional on base values, but there are a lot of rough edges around the details. diff --git a/Data/SBV/Plugin/Analyze.hs b/Data/SBV/Plugin/Analyze.hs --- a/Data/SBV/Plugin/Analyze.hs +++ b/Data/SBV/Plugin/Analyze.hs @@ -26,7 +26,7 @@ import Data.IORef -import Data.Char (isAlpha, isAlphaNum, toLower, isUpper) +import Data.Char (isAlpha, isAlphaNum, isUpper) import Data.List (intercalate, partition, nub, nubBy, sort, sortOn, isPrefixOf) import Data.Maybe (listToMaybe, fromMaybe) @@ -265,7 +265,7 @@ k <- getType noSrcSpan t nm <- mkValidName (showSDoc flags (ppr e)) case k of - KBase b -> return $ Base $ S.svUninterpreted b nm (S.UINone True) [] + KBase b -> return $ Base $ S.svUninterpreted b (S.UIGiven nm) (S.UINone True) [] _ -> error $ "Impossible: The type for literal resulted in non base kind: " ++ sh (e, k) tgo tFun orig@App{} = do @@ -533,7 +533,7 @@ bArgs = concatMap mkArg (reverse args) mkRes :: String -> SKind -> Eval [S.SVal] - mkRes n (KBase b) = return [S.svUninterpreted b n (S.UINone True) bArgs] + mkRes n (KBase b) = return [S.svUninterpreted b (S.UIGiven n) (S.UINone True) bArgs] mkRes n (KTup bs) = concat `fmap` zipWithM mkRes [n ++ "_" ++ show i | i <- [(1 :: Int) .. ]] bs mkRes n (KLst b) = do ls <- case mbListSize of Just i -> return i @@ -568,7 +568,7 @@ | True = nm unSMT nm - | map toLower nm `elem` S.smtLibReservedNames + | S.isReserved nm = if not (null nm) && isUpper (hd "unSMT" nm) then "sbv" ++ nm else "sbv_" ++ nm diff --git a/Data/SBV/Plugin/Common.hs b/Data/SBV/Plugin/Common.hs --- a/Data/SBV/Plugin/Common.hs +++ b/Data/SBV/Plugin/Common.hs @@ -102,8 +102,12 @@ , (Yices, S.yices) , (Boolector, S.boolector) , (CVC4, S.cvc4) + , (CVC5, S.cvc5) , (MathSAT, S.mathSAT) , (ABC, S.abc) + , (DReal, S.dReal) + , (OpenSMT, S.openSMT) + , (Bitwuzla, S.bitwuzla) ] -- | The kinds used by the plugin diff --git a/Data/SBV/Plugin/Data.hs b/Data/SBV/Plugin/Data.hs --- a/Data/SBV/Plugin/Data.hs +++ b/Data/SBV/Plugin/Data.hs @@ -15,7 +15,7 @@ module Data.SBV.Plugin.Data where -import Data.Data (Data, Typeable) +import Data.Data (Data) -- | Plugin options. Note that we allow picking multiple solvers, which -- will all be run in parallel. You can pick and choose any number of them, @@ -33,14 +33,18 @@ | Yices -- ^ Use Yices | Boolector -- ^ Use Boolector | CVC4 -- ^ Use CVC4 + | CVC5 -- ^ Use CVC5 + | DReal -- ^ Use DReal | MathSAT -- ^ Use MathSAT + | OpenSMT -- ^ Use OpenSMT | ABC -- ^ Use ABC + | Bitwuzla -- ^ Use Bitwuzla | AnySolver -- ^ Run all installed solvers in parallel, and report the result from the first to finish - deriving (Show, Eq, Data, Typeable) + deriving (Show, Eq, Data) -- | The actual annotation. newtype SBVAnnotation = SBV {options :: [SBVOption]} - deriving (Eq, Data, Typeable) + deriving (Eq, Data) -- | A property annotation, using default options. sbv :: SBVAnnotation diff --git a/Data/SBV/Plugin/Env.hs b/Data/SBV/Plugin/Env.hs --- a/Data/SBV/Plugin/Env.hs +++ b/Data/SBV/Plugin/Env.hs @@ -12,6 +12,7 @@ {-# LANGUAGE MagicHash #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE TemplateHaskellQuotes #-} +{-# LANGUAGE UnboxedTuples #-} {-# OPTIONS_GHC -Wall -Werror #-} @@ -219,7 +220,7 @@ -- | These types show up during uninterpretation, but are not really "interesting" as they -- are singly inhabited. uninterestingTypes :: CoreM [Type] -uninterestingTypes = map varType `fmap` mapM (grabTH lookupId) ['void#] +uninterestingTypes = map varType `fmap` mapM (grabTH lookupId) ['(# #)] -- | Certain things are just too special, as they uniformly apply to uninterpreted types. buildSpecials :: CoreM Specials diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -61,22 +61,25 @@ by comma separating them. ```haskell -data SBVOption = - IgnoreFailure -- ^ Continue even if proof fails - | Skip String -- ^ Skip the proof. Can be handy for properties that we currently do not want to focus on. - | Verbose -- ^ Produce verbose output, good for debugging - | Debug -- ^ Produce really verbose output, use only when things go really wrong! - | QuickCheck -- ^ Perform quickCheck - | Uninterpret -- ^ Uninterpret this binding for proof purposes - | Names [String] -- ^ Use these names for the arguments; need not be exhaustive - | ListSize Int -- ^ If a list-input is found, use this length. If not specified, we will complain! - | Z3 -- ^ Use Z3 - | Yices -- ^ Use Yices - | Boolector -- ^ Use Boolector - | CVC4 -- ^ Use CVC4 - | MathSAT -- ^ Use MathSAT - | ABC -- ^ Use ABC - | AnySolver -- ^ Run all installed solvers in parallel, and report the result from the first to finish +data SBVOption = IgnoreFailure -- ^ Continue even if proof fails + | Skip String -- ^ Skip the proof. Can be handy for properties that we currently do not want to focus on. + | Verbose -- ^ Produce verbose output, good for debugging + | Debug -- ^ Produce really verbose output, use only when things go really wrong! + | QuickCheck -- ^ Perform quickCheck + | Uninterpret -- ^ Uninterpret this binding for proof purposes + | Names [String] -- ^ Use these names for the arguments; need not be exhaustive + | ListSize Int -- ^ If a list-input is found, use this length. If not specified, we will complain! + | Z3 -- ^ Use Z3 + | Yices -- ^ Use Yices + | Boolector -- ^ Use Boolector + | CVC4 -- ^ Use CVC4 + | CVC5 -- ^ Use CVC5 + | DReal -- ^ Use DReal + | MathSAT -- ^ Use MathSAT + | OpenSMT -- ^ Use OpenSMT + | ABC -- ^ Use ABC + | Bitwuzla -- ^ Use Bitwuzla + | AnySolver -- ^ Run all installed solvers in parallel, and report the result from the first to finish ``` ### Using SBVPlugin from GHCi diff --git a/sbvPlugin.cabal b/sbvPlugin.cabal --- a/sbvPlugin.cabal +++ b/sbvPlugin.cabal @@ -1,6 +1,6 @@ Cabal-Version : 2.2 Name : sbvPlugin -Version : 9.10.1 +Version : 9.12.1 Category : Formal methods, Theorem provers, Math, SMT, Symbolic Computation Synopsis : Formally prove properties of Haskell programs using SBV/SMT Description : GHC plugin for proving properties over Haskell functions using SMT solvers, based @@ -18,7 +18,7 @@ Build-Type : Simple Extra-Source-Files: INSTALL, README.md, COPYRIGHT, CHANGES.md -Tested-With : GHC==9.10.1 +Tested-With : GHC==9.12.1 source-repository head type: git @@ -34,8 +34,8 @@ , Data.SBV.Plugin.Examples.MergeSort , Data.SBV.Plugin.Examples.MicroController build-depends : base >= 4.19 && < 5 - , sbv >= 10.10 - , ghc >= 9.10.1 + , sbv >= 11.4 + , ghc >= 9.12.1 , ghc-prim , containers , mtl