sbv 10.0 → 10.1
raw patch · 4 files changed
+10/−6 lines, 4 filesdep ~mtl
Dependency ranges changed: mtl
Files
- CHANGES.md +2/−2
- Data/SBV/Internals.hs +2/−2
- Documentation/SBV/Examples/Puzzles/Sudoku.hs +4/−0
- sbv.cabal +2/−2
CHANGES.md view
@@ -1,9 +1,9 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://leventerkok.github.io/sbv/> -* Latest Hackage released version: 10.0, 2023-04-14+* Latest Hackage released version: 10.1, 2023-04-14 -### Version 10.0, 2023-04-14+### Version 10.1, 2023-04-14 * [BACKWARDS COMPATIBILITY] SBV now handles quantifiers in a much more disciplined way. All of the previous ways of creating quantified variables (i.e., the functions sbvForall, sbvExists, universal, existential) are
Data/SBV/Internals.hs view
@@ -35,7 +35,7 @@ -- * Operations useful for instantiating SBV type classes , genLiteral, genFromCV, CV(..), genMkSymVar, genParse, showModel, SMTModel(..), liftQRem, liftDMod, registerKind, svToSV- , ProvableM(), SatisfiableM()+ , ProvableM(), SatisfiableM(), UICodeKind(..) -- * Compilation to C, extras , compileToC', compileToCLib'@@ -72,7 +72,7 @@ import Data.SBV.Core.Kind (BVIsNonZero, ValidFloat) import Data.SBV.Core.Sized (SWord) import Data.SBV.Core.Model (genLiteral, genFromCV, genMkSymVar, liftQRem, liftDMod)-import Data.SBV.Core.Symbolic (IStage(..), QueryContext(..), MonadQuery, addSValOptGoal, registerKind, VarContext(..), svToSV, mkNewState)+import Data.SBV.Core.Symbolic (IStage(..), QueryContext(..), MonadQuery, addSValOptGoal, registerKind, VarContext(..), svToSV, mkNewState, UICodeKind(..)) import Data.SBV.Core.Floating ( sFloatAsComparableSWord32, sDoubleAsComparableSWord64, sFloatingPointAsComparableSWord)
Documentation/SBV/Examples/Puzzles/Sudoku.hs view
@@ -9,13 +9,17 @@ -- The Sudoku solver, quintessential SMT solver example! ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleContexts #-} {-# OPTIONS_GHC -Wall -Werror #-} module Documentation.SBV.Examples.Puzzles.Sudoku where +#if MIN_VERSION_base(4,18,0) import Control.Monad (when)+#endif+ import Control.Monad.State.Lazy import Data.List (transpose)
sbv.cabal view
@@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv-Version : 10.0+Version : 10.1 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@@ -21,7 +21,7 @@ Data-Files : SBVTestSuite/GoldFiles/*.gold Extra-Source-Files : INSTALL, README.md, COPYRIGHT, CHANGES.md -Tested-With : GHC==9.4.4+Tested-With : GHC==9.6.1 source-repository head type: git