grisette 0.13.0.0 → 0.13.0.1
raw patch · 3 files changed
+57/−34 lines, 3 filesdep ~sbvPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependency ranges changed: sbv
API changes (from Hackage documentation)
- Grisette.Backend: [generateHOEquivs] :: SMTConfig -> Bool
- Grisette.Backend: [kdOptions] :: SMTConfig -> KDOptions
+ Grisette.Backend: [firstifyUniqueLen] :: SMTConfig -> Int
+ Grisette.Backend: [tpOptions] :: SMTConfig -> TPOptions
- Grisette.Backend: SMTConfig :: Bool -> Timing -> Int -> Int -> Bool -> [(String, Integer)] -> String -> Maybe Int -> Bool -> Bool -> (String -> Bool) -> Bool -> Bool -> Maybe FilePath -> SMTLibVersion -> Maybe Double -> SMTSolver -> [String] -> RoundingMode -> [SMTOption] -> Bool -> Maybe FilePath -> Bool -> KDOptions -> SMTConfig
+ Grisette.Backend: SMTConfig :: Bool -> Timing -> Int -> Int -> Bool -> [(String, Integer)] -> String -> Maybe Int -> Bool -> Bool -> (String -> Bool) -> Bool -> Bool -> Maybe FilePath -> SMTLibVersion -> Maybe Double -> SMTSolver -> [String] -> RoundingMode -> [SMTOption] -> Bool -> Maybe FilePath -> Int -> TPOptions -> SMTConfig
Files
- README.md +2/−2
- grisette.cabal +32/−32
- src/Grisette/Internal/SymPrim/FP.hs +23/−0
README.md view
@@ -59,14 +59,14 @@ ```yaml extra-deps:- - grisette-0.13.0.0+ - grisette-0.13.0.1 ``` and in your `package.yaml` file: ```yaml dependencies:- - grisette >= 0.13 < 0.14+ - grisette >= 0.13.0.1 < 0.14 ``` #### Quick start template with `stack new`
grisette.cabal view
@@ -1,37 +1,37 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.38.0.+-- This file has been generated from package.yaml by hpack version 0.37.0. -- -- see: https://github.com/sol/hpack -name: grisette-version: 0.13.0.0-synopsis: Symbolic evaluation as a library-description: Grisette is a reusable symbolic evaluation library for Haskell. By- translating programs into constraints, Grisette can help the development of- program reasoning tools, including verification, synthesis, and more.- .- The "Grisette" module exports all the core APIs for building a symbolic- evaluation tool. A high-level overview of the module structures are available- there.- .- A detailed introduction to Grisette is available at "Grisette.Core". More- lifted libraries are provided in @Grisette.Lib.*@ modules.- .- The "Grisette.Unified" module offers an experimental unified interface for- symbolic and concrete evaluation. This module should be imported qualified.- .- For more details, please checkout the README and - [tutorials](https://github.com/lsrcz/grisette/tree/main/tutorials).-category: Formal Methods, Theorem Provers, Symbolic Computation, SMT-homepage: https://github.com/lsrcz/grisette#readme-bug-reports: https://github.com/lsrcz/grisette/issues-author: Sirui Lu, Rastislav Bodík-maintainer: Sirui Lu (siruilu@cs.washington.edu)-copyright: 2021-2024 Sirui Lu-license: BSD3-license-file: LICENSE-build-type: Simple+name: grisette+version: 0.13.0.1+synopsis: Symbolic evaluation as a library+description: Grisette is a reusable symbolic evaluation library for Haskell. By+ translating programs into constraints, Grisette can help the development of+ program reasoning tools, including verification, synthesis, and more.+ .+ The "Grisette" module exports all the core APIs for building a symbolic+ evaluation tool. A high-level overview of the module structures are available+ there.+ .+ A detailed introduction to Grisette is available at "Grisette.Core". More+ lifted libraries are provided in @Grisette.Lib.*@ modules.+ .+ The "Grisette.Unified" module offers an experimental unified interface for+ symbolic and concrete evaluation. This module should be imported qualified.+ .+ For more details, please checkout the README and + [tutorials](https://github.com/lsrcz/grisette/tree/main/tutorials).+category: Formal Methods, Theorem Provers, Symbolic Computation, SMT+homepage: https://github.com/lsrcz/grisette#readme+bug-reports: https://github.com/lsrcz/grisette/issues+author: Sirui Lu, Rastislav Bodík+maintainer: Sirui Lu (siruilu@cs.washington.edu)+copyright: 2021-2024 Sirui Lu+license: BSD3+license-file: LICENSE+build-type: Simple tested-with: GHC == 8.10.7 , GHC == 9.0.2@@ -329,7 +329,7 @@ , mtl >=2.2.2 && <2.4 , parallel >=3.2.2 && <3.3 , prettyprinter >=1.5.0 && <1.8- , sbv >=8.17 && <12+ , sbv >=8.17 && <13 , stm ==2.5.* , template-haskell >=2.16 && <2.24 , text >=1.2.4.1 && <2.2@@ -378,7 +378,7 @@ , mtl >=2.2.2 && <2.4 , parallel >=3.2.2 && <3.3 , prettyprinter >=1.5.0 && <1.8- , sbv >=8.17 && <12+ , sbv >=8.17 && <13 , stm ==2.5.* , template-haskell >=2.16 && <2.24 , text >=1.2.4.1 && <2.2@@ -499,7 +499,7 @@ , mtl >=2.2.2 && <2.4 , parallel >=3.2.2 && <3.3 , prettyprinter >=1.5.0 && <1.8- , sbv >=8.17 && <12+ , sbv >=8.17 && <13 , stm ==2.5.* , template-haskell >=2.16 && <2.24 , test-framework >=0.8.2 && <0.9
src/Grisette/Internal/SymPrim/FP.hs view
@@ -219,6 +219,7 @@ <> " sb `elem` [2 .. 4611686018427387902]\n\n" <> " Given type falls outside of this range, or the sizes are not known naturals." +#if MIN_VERSION_sbv(12,0,0) -- | Provide an (unsafe) type-level proof that the given floating-point type is -- valid. withUnsafeValidFP ::@@ -229,6 +230,27 @@ in if checkDynamicValidFP eb sb then case unsafeAxiom @True @( ((CmpNat eb 2 == 'EQ) || (CmpNat eb 2 == 'GT))+ && ( ((CmpNat eb 29 == 'EQ) || (CmpNat eb 29 == 'LT))+ && ( ((CmpNat sb 2 == 'EQ) || (CmpNat sb 2 == 'GT))+ && ( (CmpNat sb 1073741822 == 'EQ)+ || (CmpNat sb 1073741822 == 'LT)+ )+ )+ )+ ) of+ Refl -> r+ else error invalidFPMessage+#else+-- | Provide an (unsafe) type-level proof that the given floating-point type is+-- valid.+withUnsafeValidFP ::+ forall eb sb r. (KnownNat eb, KnownNat sb) => ((ValidFP eb sb) => r) -> r+withUnsafeValidFP r =+ let eb = natVal (Proxy @eb)+ sb = natVal (Proxy @sb)+ in if checkDynamicValidFP eb sb+ then case unsafeAxiom @True+ @( ((CmpNat eb 2 == 'EQ) || (CmpNat eb 2 == 'GT)) && ( ((CmpNat eb 61 == 'EQ) || (CmpNat eb 61 == 'LT)) && ( ((CmpNat sb 2 == 'EQ) || (CmpNat sb 2 == 'GT)) && ( (CmpNat sb 4611686018427387902 == 'EQ)@@ -239,6 +261,7 @@ ) of Refl -> r else error invalidFPMessage+#endif -- | IEEE 754 floating-point number with @eb@ exponent bits and @sb@ significand -- bits.