sbvPlugin 9.10.1 → 9.12.1
raw patch · 7 files changed
+48/−40 lines, 7 filesdep ~ghcdep ~sbv
Dependency ranges changed: ghc, sbv
Files
- CHANGES.md +8/−12
- Data/SBV/Plugin/Analyze.hs +4/−4
- Data/SBV/Plugin/Common.hs +4/−0
- Data/SBV/Plugin/Data.hs +7/−3
- Data/SBV/Plugin/Env.hs +2/−1
- README.md +19/−16
- sbvPlugin.cabal +4/−4
CHANGES.md view
@@ -1,8 +1,15 @@ * Hackage: <http://hackage.haskell.org/package/sbvPlugin> * GitHub: <http://github.com/LeventErkok/sbvPlugin> -* 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: <http://acowley.github.io/NYHUG/FunctionalRoboticist.pdf>@@ -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.
Data/SBV/Plugin/Analyze.hs view
@@ -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
Data/SBV/Plugin/Common.hs view
@@ -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
Data/SBV/Plugin/Data.hs view
@@ -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
Data/SBV/Plugin/Env.hs view
@@ -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
README.md view
@@ -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
sbvPlugin.cabal view
@@ -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