sbv 14.2 → 14.3
raw patch · 24 files changed
+372/−144 lines, 24 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
+ Data.SBV: enumFromThenToH :: EnumSymbolic a => SBV a -> SBV a -> SBV a -> Maybe Integer -> SList a
+ Data.SBV.List: enumFromThenToH :: EnumSymbolic a => SBV a -> SBV a -> SBV a -> Maybe Integer -> SList a
Files
- CHANGES.md +26/−0
- Data/SBV/Core/Model.hs +44/−4
- Data/SBV/Core/Symbolic.hs +28/−18
- Data/SBV/List.hs +132/−55
- Data/SBV/SEnum.hs +52/−2
- Data/SBV/SMT/SMT.hs +25/−13
- Data/SBV/SMT/SMTLib2.hs +3/−2
- Data/SBV/Utils/Numeric.hs +1/−1
- Documentation/SBV/Examples/ADT/Param.hs +2/−2
- Documentation/SBV/Examples/TP/Basics.hs +31/−0
- Documentation/SBV/Examples/TP/Lists.hs +2/−2
- Documentation/SBV/Examples/TP/Numeric.hs +4/−11
- SBVTestSuite/GoldFiles/adt_gen00.gold +4/−4
- SBVTestSuite/GoldFiles/adt_pgen00.gold +4/−4
- SBVTestSuite/GoldFiles/exceptionLocal1.gold +2/−8
- SBVTestSuite/GoldFiles/exceptionLocal2.gold +2/−8
- SBVTestSuite/GoldFiles/exceptionRemote1.gold +1/−1
- SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.stderr +2/−2
- SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.stderr +2/−2
- SBVTestSuite/TestSuite/CompileTests/SCase/SCase101.stderr +1/−1
- SBVTestSuite/TestSuite/CompileTests/SCase/SCase59.stderr +1/−1
- SBVTestSuite/TestSuite/CompileTests/SCase/SCase66.stderr +1/−1
- SBVTestSuite/TestSuite/CompileTests/SCase/SCase89.stderr +1/−1
- sbv.cabal +1/−1
CHANGES.md view
@@ -1,6 +1,32 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://github.com/LeventErkok/sbv> +### Version 14.3, 2026-06-19++ * Improve fpRoundToIntegralH to remove redundant internal check. Thanks to Ryan Scott for the report.++ * Add support for arctan/arcsin/arccos in CVC5. Thanks to Ryan Scott for pointing out support for it.++ * Improved backed-solver communication so that if a solver returns an error message SBV now makes+ sure it gets captured and displayed properly before the solver-process itselfs terminates.++ * Drop support for pi as an SReal: The whole premise of SReal is it represents algebraic-reals+ (i.e., those that are roots of polynomials) exactly. But pi is not representable as such, since+ it's transcendental. Older versions of SBV used an approximation, but that's confusing to say+ the least, and downright wrong. Note that you can still use pi at floating-point types, where+ precision loss is built into the semantics.++ * Fix the enumeration quasi-quoter for a zero step: `[sEnum| 1, 1 .. 5 |]` is now the+ (semantically infinite) list of 1's, instead of the empty list.++ * Soundness fix for termination measures: a real-valued measure is now rejected at compile+ time. The reals are not well-ordered (an infinite descending chain like 1, 1/2, 1/4, ...+ never reaches a minimum), so a non-negative, strictly-decreasing real measure does not+ imply termination. Use an integer-valued measure instead.++ * Termination measures may now be given over the bounded bit-vector types (`Word8`..`Word64`,+ `Int8`..`Int64`, `WordN n`, `IntN n`), in addition to the integer/float types supported before.+ ### Version 14.2, 2026-06-05 * Fix float to integer conversions, which were ignoring the rounding mode previously. Thanks to
Data/SBV/Core/Model.hs view
@@ -1230,6 +1230,20 @@ instance Zero Integer where zero = literal 0 +-- | Bounded bit-vectors as measures. These are all sound: each is a finite type, so a+-- non-negative, strictly-decreasing chain of values is necessarily finite. (The default+-- @nonNeg x = x .>= 0@ works for both the unsigned and signed cases.)+instance Zero Word8 where zero = literal 0+instance Zero Word16 where zero = literal 0+instance Zero Word32 where zero = literal 0+instance Zero Word64 where zero = literal 0+instance Zero Int8 where zero = literal 0+instance Zero Int16 where zero = literal 0+instance Zero Int32 where zero = literal 0+instance Zero Int64 where zero = literal 0+instance (KnownNat n, BVIsNonZero n) => Zero (WordN n) where zero = literal 0+instance (KnownNat n, BVIsNonZero n) => Zero (IntN n) where zero = literal 0+ -- NB. We would like to use 'Data.SBV.Tuple.untuple' in the 'nonNeg' definitions below, -- but 'Data.SBV.Tuple' imports 'Data.SBV.Core.Model', creating a circular dependency. -- So we extract components at the SVal level using 'TupleAccess' directly.@@ -1262,9 +1276,19 @@ instance Zero Double where zero = literal 0 --- | An algebraic real as a measure-instance Zero AlgReal where- zero = literal 0+-- | Algebraic reals are /not/ permitted as measures, and we reject them at compile time.+-- The reals are dense, hence not well-ordered: a merely non-negative and strictly-decreasing+-- real measure does not imply termination (e.g. the chain @1, 1\/2, 1\/4, ...@ descends forever+-- without reaching a minimum). Use an integer-valued measure instead.+instance TypeError ( 'Text "A termination measure may not have a real-valued result."+ ':$$: 'Text ""+ ':$$: 'Text "The reals are not well-ordered: an infinite descending chain such as"+ ':$$: 'Text "1, 1/2, 1/4, ... has no least element, so a non-negative and strictly"+ ':$$: 'Text "decreasing real measure does not imply termination."+ ':$$: 'Text ""+ ':$$: 'Text "Use an integer-valued measure instead (e.g. a count of remaining steps)."+ ) => Zero AlgReal where+ zero = error "Data.SBV.Zero(AlgReal): unreachable" -- | A floating-point as a measure instance ValidFloat eb sb => Zero (FloatingPoint eb sb) where@@ -2882,7 +2906,23 @@ -- we do not constant fold these values (except for pi), as Haskell doesn't really have any means of computing -- them for arbitrary rationals. instance {-# OVERLAPPING #-} Floating SReal where- pi = fromRational . toRational $ (pi :: Double) -- Perhaps not good enough?+ -- Should we support pi? It's a transcendental value, and our SReal type has no way of representing+ -- this quantity with the required fidelity. (SReal can only support roots of polynomials and rationals+ -- correctly, not transcendentals.) One option is to use an approximation here. But that goes against the+ -- whole idea of Real being infinitely precise. Another option is to see if the solver has support for it, such+ -- as CVC5, which has the constant real.pi. Alas, that has its problems: In models CVC5 uses real.pi as a+ -- model value, which we have no way of properly supporting back as a Haskell value. Worse: It uses it in+ -- expressions like 1 + real.pi, which we don't have an evaluator for. So, we simply say not supported.+ -- If you want it for reals, you'll have to plugin your own "approximation" for it, and thus be aware of the+ -- limitations of that choice.+ pi = error $ unlines [ ""+ , "*** Data.SBV.SReal: Cannot represent pi as an SReal value."+ , "***"+ , "*** Usual trick is to use an approximation if that suits your purpose,"+ , "*** or use solver-specific constants when applicable. Please get in touch"+ , "*** if you'd like to explore ideas here."+ ]+ exp = lift1SReal NR_Exp log = lift1SReal NR_Log sqrt = lift1SReal NR_Sqrt
Data/SBV/Core/Symbolic.hs view
@@ -57,7 +57,7 @@ , MonadQuery(..), QueryT(..), Query, QueryState(..), QueryContext(..) , SMTScript(..), Solver(..), SMTSolver(..), SMTResult(..), SMTModel(..), SMTConfig(..), TPOptions(..), SMTEngine , validationRequested, outputSVal, ProgInfo(..), mustIgnoreVar, getRootState- , LambdaInfo(..)+ , LambdaInfo(..), showNROp ) where import Control.DeepSeq (NFData(..))@@ -321,7 +321,8 @@ show FP_IsNegative = "fp.isNegative" show FP_IsPositive = "fp.isPositive" --- | Non-linear operations+-- | Non-linear operations. We do *not* on purpose deriving Show here, nor give a show instance,+-- since different solvers call these functions with different names. data NROp = NR_Sin | NR_Cos | NR_Tan@@ -337,22 +338,31 @@ | NR_Pow deriving (Eq, Ord, G.Data, NFData, Generic) --- | The show instance carefully arranges for these to be printed as it can be understood by dreal-instance Show NROp where- show NR_Sin = "sin"- show NR_Cos = "cos"- show NR_Tan = "tan"- show NR_ASin = "asin"- show NR_ACos = "acos"- show NR_ATan = "atan"- show NR_Sinh = "sinh"- show NR_Cosh = "cosh"- show NR_Tanh = "tanh"- show NR_Sqrt = "sqrt"- show NR_Exp = "exp"- show NR_Log = "log"- show NR_Pow = "pow"+-- | Show a non-linear op. Unfortunately this can't be generically done since different+-- solvers use different names for some of these ops.+showNROp :: Solver -> NROp -> String+showNROp slvr = sh+ where sh NR_Sin = "sin"+ sh NR_Cos = "cos"+ sh NR_Tan = "tan"+ sh NR_ASin = arc ++ "sin"+ sh NR_ACos = arc ++ "cos"+ sh NR_ATan = arc ++ "tan"+ sh NR_Sinh = "sinh"+ sh NR_Cosh = "cosh"+ sh NR_Tanh = "tanh"+ sh NR_Sqrt = "sqrt"+ sh NR_Exp = "exp"+ sh NR_Log = "log"+ sh NR_Pow = "pow" + -- DReal uses asin/acos etc. CVC5 uses arcsin. Other solvers probably+ -- don't even support these. But this isn't the right place to bail-out+ -- about it; so we just put "arc" following CVC5 here.+ arc = case slvr of+ DReal -> "a"+ _ -> "arc"+ -- | Pseudo-boolean operations data PBOp = PB_AtMost Int -- ^ At most k | PB_AtLeast Int -- ^ At least k@@ -583,7 +593,7 @@ show (IEEEFP w) = show w - show (NonLinear w) = show w+ show (NonLinear w) = showNROp DReal w -- Just use DReal here, only used for debugging show (PseudoBoolean p) = show p
Data/SBV/List.hs view
@@ -1200,6 +1200,16 @@ -- | @`enumFromThenTo` m n@. Symbolic version of @[m, m' .. n]@ enumFromThenTo :: SymVal a => SBV a -> SBV a -> SBV a -> SList a + -- | @`enumFromThenTo`@ with an optionally statically-known integer step. The sEnum quasiquoter+ -- supplies @`Just` d@ for @[m, m' .. n]@ when @m'@ is @m@ shifted by a compile-time integer+ -- constant (e.g. @[m, m-1 .. n]@ gives @-1@); otherwise it supplies `Nothing`. Instances with+ -- exact arithmetic (integers, reals) use the hint to constant-fold the step, so the @step == 0@+ -- infinite-list branch (and its productive helper) drops out; every other instance ignores the+ -- hint and falls back to 'enumFromThenTo', preserving its exact semantics. Not meant to be called+ -- directly; the default is correct for any instance.+ enumFromThenToH :: SymVal a => SBV a -> SBV a -> SBV a -> Maybe Integer -> SList a+ enumFromThenToH from thn to _ = enumFromThenTo from thn to+ -- | 'EnumSymbolic' instance for words instance {-# OVERLAPPABLE #-} (SymVal a, Bounded a, Integral a, Num a, Num (SBV a)) => EnumSymbolic a where succ = smtFunction "EnumSymbolic.succ" (\x -> ite (x .== maxBound) (some "EnumSymbolic.succ.maxBound" (const sTrue)) (x+1))@@ -1232,23 +1242,34 @@ toEnum = id fromEnum = id - enumFrom n = enumFromThen n (n+1)- enumFromTo n = enumFromThenTo n (n+1)+ enumFrom n = enumFromThen n (n+1)+ enumFromTo n m = enumFromThenToInteger n m 1 enumFromThen x y = go x (y-x) where go = smtProductiveFunction "EnumSymbolic.Integer.enumFromThen" $ \start delta -> start .: go (start+delta) delta - enumFromThenTo x y z = ite (delta .>= 0) (up x delta z) (down x delta z)- where delta = y - x+ enumFromThenTo x y z = enumFromThenToInteger x z (y - x) - up, down :: SInteger -> SInteger -> SInteger -> SList Integer- up = smtFunctionWithMeasure "EnumSymbolic.Integer.enumFromThenTo.up"- (\start _d end -> 0 `smax` (end - start + 1), [])- $ \start d end -> ite (start .> end .|| d .<= 0) [] (start .: up (start + d) d end)- down = smtFunctionWithMeasure "EnumSymbolic.Integer.enumFromThenTo.down"- (\start _d end -> 0 `smax` (start - end + 1), [])- $ \start d end -> ite (start .< end .|| d .>= 0) [] (start .: down (start + d) d end)+ enumFromThenToH x y z mStep = enumFromThenToInteger x z (maybe (y - x) fromIntegral mStep) +-- When the step is 0 (i.e., y == x), Haskell produces an infinite list of x's+-- if x <= z, and the empty list otherwise. We mirror that here.+enumFromThenToInteger :: SInteger -> SInteger -> SInteger -> SList Integer+enumFromThenToInteger x z delta = ite (delta .== 0)+ (ite (x .<= z) (enumFromThen x x) [])+ $ ite (delta .> 0) (up x delta z) (down x delta z)+ where -- The d==0 case is handled: 'up'/'down' are only *called* with d>0/d<0 (the d==0 case+ -- is routed to the infinite-list branch above), and the guard's @d .<= 0@/@d .>= 0@ test+ -- puts @d>0@/@d<0@ into the reaching condition, so measure verification never sees d==0.+ -- (The integer measure does not divide by d, so there's no zero-denominator to worry about.)+ up, down :: SInteger -> SInteger -> SInteger -> SList Integer+ up = smtFunctionWithMeasure "EnumSymbolic.Integer.enumFromThenTo.up"+ (\start _d end -> 0 `smax` (end - start + 1), [])+ $ \start d end -> ite (start .> end .|| d .<= 0) [] (start .: up (start + d) d end)+ down = smtFunctionWithMeasure "EnumSymbolic.Integer.enumFromThenTo.down"+ (\start _d end -> 0 `smax` (start - end + 1), [])+ $ \start d end -> ite (start .< end .|| d .>= 0) [] (start .: down (start + d) d end)+ -- | 'EnumSymbolic instance for 'Float'. Note that the termination requirement as defined by the Haskell standard for floats state: -- > For Float and Double, the semantics of the enumFrom family is given by the rules for Int above, -- > except that the list terminates when the elements become greater than @e3 + i/2@ for positive increment @i@,@@ -1260,23 +1281,39 @@ toEnum = sFromIntegral fromEnum = fromSFloat sRTZ - enumFrom n = enumFromThen n (n+1)- enumFromTo n = enumFromThenTo n (n+1)+ enumFrom n = enumFromThen n (n+1)+ enumFromTo n m = enumFromThenToFloat n m 1 enumFromThen x y = go 0 x (y-x) where go = smtProductiveFunction "EnumSymbolic.Float.enumFromThen" $ \k n d -> (n + k * d) .: go (k+1) n d - enumFromThenTo x y zIn = ite (delta .>= 0) (up 0 x delta z) (down 0 x delta z)- where delta, z :: SFloat- delta = y - x- z = zIn + delta / 2+ enumFromThenTo x y zIn = enumFromThenToFloat x zIn (y - x) - up, down :: SFloat -> SFloat -> SFloat -> SFloat -> SList Float- up = smtFunctionWithMeasure "EnumSymbolic.Float.enumFromThenTo.up" (\k n d end -> 0 `smax` (end - (n + k * d)), [])- $ \k n d end -> let c = n + k * d in ite (c .> end) [] (c .: up (k+1) n d end)- down = smtFunctionWithMeasure "EnumSymbolic.Float.enumFromThenTo.down" (\k n d end -> 0 `smax` ((n + k * d) - end), [])- $ \k n d end -> let c = n + k * d in ite (c .< end) [] (c .: down (k+1) n d end)+-- When the step is 0 (i.e., y == x), Haskell produces an infinite list of x's+-- if x <= z, and the empty list otherwise. We mirror that here.+enumFromThenToFloat :: SFloat -> SFloat -> SFloat -> SList Float+enumFromThenToFloat x zIn delta = ite (delta .== 0)+ (ite (x .<= z) (enumFromThen x x) [])+ $ ite (delta .> 0) (up 0 x delta z) (down 0 x delta z)+ where z :: SFloat+ z = zIn + delta / 2 + -- Unlike the Integer/AlgReal instances, these are NOT given a termination measure:+ -- floating-point enumeration is genuinely partial. The step @k * d@ can saturate (once+ -- @k * d@ falls below the ULP of @n@, or once the float @k@ itself stops incrementing),+ -- so for some inputs @n + k * d@ never exceeds @end@ and the recursion does not terminate+ -- -- exactly as Haskell's own float enumeration diverges in those cases. A termination+ -- measure would therefore be unsound: no measure can certify termination of a function+ -- that does not always terminate. Instead we mark these productive -- each recursive call+ -- is guarded by a cons, so the definition is well-formed corecursion (finite when the+ -- enumeration terminates, infinite when it saturates). The d==0 case never reaches here:+ -- it is routed to the infinite-list branch above.+ up, down :: SFloat -> SFloat -> SFloat -> SFloat -> SList Float+ up = smtProductiveFunction "EnumSymbolic.Float.enumFromThenTo.up"+ $ \k n d end -> let c = n + k * d in ite (c .> end) [] (c .: up (k+1) n d end)+ down = smtProductiveFunction "EnumSymbolic.Float.enumFromThenTo.down"+ $ \k n d end -> let c = n + k * d in ite (c .< end) [] (c .: down (k+1) n d end)+ -- | 'EnumSymbolic instance for 'Double' instance {-# OVERLAPPING #-} EnumSymbolic Double where succ x = x + 1@@ -1285,23 +1322,33 @@ toEnum = sFromIntegral fromEnum = fromSDouble sRTZ - enumFrom n = enumFromThen n (n+1)- enumFromTo n = enumFromThenTo n (n+1)+ enumFrom n = enumFromThen n (n+1)+ enumFromTo n m = enumFromThenToDouble n m 1 enumFromThen x y = go 0 x (y-x) where go = smtProductiveFunction "EnumSymbolic.Double.enumFromThen" $ \k n d -> (n + k * d) .: go (k+1) n d - enumFromThenTo x y zIn = ite (delta .>= 0) (up 0 x delta z) (down 0 x delta z)- where delta, z :: SDouble- delta = y - x- z = zIn + delta / 2+ enumFromThenTo x y zIn = enumFromThenToDouble x zIn (y - x) - up, down :: SDouble -> SDouble -> SDouble -> SDouble -> SList Double- up = smtFunctionWithMeasure "EnumSymbolic.Double.enumFromThenTo.up" (\k n d end -> 0 `smax` (end - (n + k * d)), [])- $ \k n d end -> let c = n + k * d in ite (c .> end) [] (c .: up (k+1) n d end)- down = smtFunctionWithMeasure "EnumSymbolic.Double.enumFromThenTo.down" (\k n d end -> 0 `smax` ((n + k * d) - end), [])- $ \k n d end -> let c = n + k * d in ite (c .< end) [] (c .: down (k+1) n d end)+-- When the step is 0 (i.e., y == x), Haskell produces an infinite list of x's+-- if x <= z, and the empty list otherwise. We mirror that here.+enumFromThenToDouble :: SDouble -> SDouble -> SDouble -> SList Double+enumFromThenToDouble x zIn delta = ite (delta .== 0)+ (ite (x .<= z) (enumFromThen x x) [])+ $ ite (delta .> 0) (up 0 x delta z) (down 0 x delta z)+ where z :: SDouble+ z = zIn + delta / 2 + -- See the Float instance for why these are productive rather than measured:+ -- floating-point enumeration is genuinely partial (the @k * d@ step can saturate), so a+ -- termination measure would be unsound. Each recursive call is guarded by a cons, so the+ -- definition is well-formed corecursion. The d==0 case is routed to the branch above.+ up, down :: SDouble -> SDouble -> SDouble -> SDouble -> SList Double+ up = smtProductiveFunction "EnumSymbolic.Double.enumFromThenTo.up"+ $ \k n d end -> let c = n + k * d in ite (c .> end) [] (c .: up (k+1) n d end)+ down = smtProductiveFunction "EnumSymbolic.Double.enumFromThenTo.down"+ $ \k n d end -> let c = n + k * d in ite (c .< end) [] (c .: down (k+1) n d end)+ -- | 'EnumSymbolic instance for arbitrary floats instance {-# OVERLAPPING #-} ValidFloat eb sb => EnumSymbolic (FloatingPoint eb sb) where succ x = x + 1@@ -1310,23 +1357,33 @@ toEnum = sFromIntegral fromEnum = fromSFloatingPoint sRTZ - enumFrom n = enumFromThen n (n+1)- enumFromTo n = enumFromThenTo n (n+1)+ enumFrom n = enumFromThen n (n+1)+ enumFromTo n m = enumFromThenToFloatingPoint n m 1 enumFromThen x y = go 0 x (y-x) where go = smtProductiveFunction "EnumSymbolic.FloatingPoint.enumFromThen" $ \k n d -> (n + k * d) .: go (k+1) n d - enumFromThenTo x y zIn = ite (delta .>= 0) (up 0 x delta z) (down 0 x delta z)- where delta, z :: SFloatingPoint eb sb- delta = y - x- z = zIn + delta / 2+ enumFromThenTo x y zIn = enumFromThenToFloatingPoint x zIn (y - x) - up, down :: SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SList (FloatingPoint eb sb)- up = smtFunctionWithMeasure "EnumSymbolic.FloatingPoint.enumFromThenTo.up" (\k n d end -> 0 `smax` (end - (n + k * d)), [])- $ \k n d end -> let c = n + k * d in ite (c .> end) [] (c .: up (k+1) n d end)- down = smtFunctionWithMeasure "EnumSymbolic.FloatingPoint.enumFromThenTo.down" (\k n d end -> 0 `smax` ((n + k * d) - end), [])- $ \k n d end -> let c = n + k * d in ite (c .< end) [] (c .: down (k+1) n d end)+-- When the step is 0 (i.e., y == x), Haskell produces an infinite list of x's+-- if x <= z, and the empty list otherwise. We mirror that here.+enumFromThenToFloatingPoint :: forall eb sb. ValidFloat eb sb => SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SList (FloatingPoint eb sb)+enumFromThenToFloatingPoint x zIn delta = ite (delta .== 0)+ (ite (x .<= z) (enumFromThen x x) [])+ $ ite (delta .> 0) (up 0 x delta z) (down 0 x delta z)+ where z :: SFloatingPoint eb sb+ z = zIn + delta / 2 + -- See the Float instance for why these are productive rather than measured:+ -- floating-point enumeration is genuinely partial (the @k * d@ step can saturate), so a+ -- termination measure would be unsound. Each recursive call is guarded by a cons, so the+ -- definition is well-formed corecursion. The d==0 case is routed to the branch above.+ up, down :: SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SList (FloatingPoint eb sb)+ up = smtProductiveFunction "EnumSymbolic.FloatingPoint.enumFromThenTo.up"+ $ \k n d end -> let c = n + k * d in ite (c .> end) [] (c .: up (k+1) n d end)+ down = smtProductiveFunction "EnumSymbolic.FloatingPoint.enumFromThenTo.down"+ $ \k n d end -> let c = n + k * d in ite (c .< end) [] (c .: down (k+1) n d end)+ -- | 'EnumSymbolic instance for arbitrary AlgReal. We don't have to use the multiplicative trick here -- since alg-reals are precise. But, following rational in Haskell, we do use the stopping point of @z + delta / 2@. instance {-# OVERLAPPING #-} EnumSymbolic AlgReal where@@ -1336,22 +1393,42 @@ toEnum = sFromIntegral fromEnum = sRealToSIntegerTruncate - enumFrom n = enumFromThen n (n+1)- enumFromTo n = enumFromThenTo n (n+1)+ enumFrom n = enumFromThen n (n+1)+ enumFromTo n m = enumFromThenToAlgReal n m 1 enumFromThen x y = go x (y-x) where go = smtProductiveFunction "EnumSymbolic.AlgReal.enumFromThen" $ \start delta -> start .: go (start+delta) delta - enumFromThenTo x y zIn = ite (delta .>= 0) (up x delta z) (down x delta z)- where delta, z :: SReal- delta = y - x- z = zIn + delta / 2+ enumFromThenTo x y zIn = enumFromThenToAlgReal x zIn (y - x) - up, down :: SReal -> SReal -> SReal -> SList AlgReal- up = smtFunctionWithMeasure "EnumSymbolic.AlgReal.enumFromThenTo.up" (\start _d end -> 0 `smax` (end - start + 1), [])- $ \start d end -> ite (start .> end .|| d .<= 0) [] (start .: up (start + d) d end)- down = smtFunctionWithMeasure "EnumSymbolic.AlgReal.enumFromThenTo.down" (\start _d end -> 0 `smax` (start - end + 1), [])- $ \start d end -> ite (start .< end .|| d .>= 0) [] (start .: down (start + d) d end)+ enumFromThenToH x y zIn mStep = enumFromThenToAlgReal x zIn (maybe (y - x) fromIntegral mStep)++-- When the step is 0 (i.e., y == x), Haskell produces an infinite list of x's+-- if x <= z, and the empty list otherwise. We mirror that here.+enumFromThenToAlgReal :: SReal -> SReal -> SReal -> SList AlgReal+enumFromThenToAlgReal x zIn delta = ite (delta .== 0)+ (ite (x .<= z) (enumFromThen x x) [])+ $ ite (delta .> 0) (up x delta z) (down x delta z)+ where z :: SReal+ z = zIn + delta / 2++ -- The measure is the number of remaining recursive steps, which is an INTEGER:+ -- @floor ((end - start) / d) + 1@ (clamped at 0). A real-valued measure would be+ -- unsound here, since the reals are not well-ordered (an infinite descending chain+ -- like 1, 1/2, 1/4, ... never reaches a minimum). 'sRealToSInteger' is @floor@, and+ -- @(end - start) / d@ is non-negative in both the up (d>0) and down (d<0) regimes, so+ -- the same expression serves both.+ --+ -- The d==0 case is handled: 'up'/'down' are only *called* with d>0/d<0 (the d==0 case is+ -- routed to the infinite-list branch above), and for measure *verification* the guard's+ -- @d .<= 0@/@d .>= 0@ test puts @d>0@/@d<0@ into the reaching condition, so the decrease+ -- obligation never sees d==0; the @0 `smax`@ keeps non-negativity vacuously true even for+ -- the unreachable zero-denominator value of @(end - start) / d@.+ up, down :: SReal -> SReal -> SReal -> SList AlgReal+ up = smtFunctionWithMeasure "EnumSymbolic.AlgReal.enumFromThenTo.up" (\start d end -> 0 `smax` (sRealToSInteger ((end - start) / d) + 1), [])+ $ \start d end -> ite (start .> end .|| d .<= 0) [] (start .: up (start + d) d end)+ down = smtFunctionWithMeasure "EnumSymbolic.AlgReal.enumFromThenTo.down" (\start d end -> 0 `smax` (sRealToSInteger ((end - start) / d) + 1), [])+ $ \start d end -> ite (start .< end .|| d .>= 0) [] (start .: down (start + d) d end) -- | Lookup. If we can't find, then the result is unspecified. --
Data/SBV/SEnum.hs view
@@ -39,7 +39,7 @@ import Data.Char (isSpace) import Prelude hiding (enumFrom, enumFromThen, enumFromTo, enumFromThenTo)-import Data.SBV.List (enumFrom, enumFromThen, enumFromTo, enumFromThenTo)+import Data.SBV.List (enumFrom, enumFromThen, enumFromTo, enumFromThenToH) import Control.Monad (unless) import Data.List (isInfixOf, intercalate)@@ -108,7 +108,13 @@ ([a], Nothing) -> varE 'enumFrom `appE` parseHaskellExpr loc a ([a, b], Nothing) -> varE 'enumFromThen `appE` parseHaskellExpr loc a `appE` parseHaskellExpr loc b ([a], Just c) -> varE 'enumFromTo `appE` parseHaskellExpr loc a `appE` parseHaskellExpr loc c- ([a, b], Just c) -> varE 'enumFromThenTo `appE` parseHaskellExpr loc a `appE` parseHaskellExpr loc b `appE` parseHaskellExpr loc c+ ([a, b], Just c) -> do ea <- parseHaskellExpr loc a+ eb <- parseHaskellExpr loc b+ ec <- parseHaskellExpr loc c+ -- Pass the from/then step as a hint when it's a statically-known integer+ -- (e.g. @[m, m-1 .. n]@ => @-1@). Exact-arithmetic instances fold it; the+ -- rest ignore it. See 'constStep'.+ varE 'enumFromThenToH `appE` pure ea `appE` pure eb `appE` pure ec `appE` liftMStep (constStep ea eb) _ -> errorWithLoc loc $ unlines [ "Data.SBV.Enum: Invalid format. Use one of:" , ""@@ -117,6 +123,50 @@ , " [sEnum| a .. c |]" , " [sEnum| a, b .. c |]" ]++-- | Read a parsed expression as @base + offset@: a single opaque atom plus an integer constant.+-- @Nothing@ base means the whole thing is a pure integer constant. We only look through @+@ and @-@+-- of integer literals; anything else is treated as an atom. This is intentionally a single-base+-- peel, not a general linear normalizer -- it's exactly enough to recognize @m@, @m-1@, @m+k@, etc.+peel :: Exp -> (Maybe Exp, Integer)+peel (LitE (IntegerL n)) = (Nothing, n)+peel (ParensE e) = peel e+peel (SigE e _) = peel e+peel (InfixE (Just l) (VarE op) (Just (LitE (IntegerL n)))) = shift op l n+peel (UInfixE l (VarE op) (LitE (IntegerL n))) = shift op l n+peel (InfixE (Just (LitE (IntegerL n))) (VarE op) (Just r)) | base op == "+" = add (peel r) n+peel (UInfixE (LitE (IntegerL n)) (VarE op) r) | base op == "+" = add (peel r) n+peel e = (Just e, 0)++-- | Helper for 'peel': fold a @base <op> lit@ where @op@ is @+@ or @-@.+shift :: Name -> Exp -> Integer -> (Maybe Exp, Integer)+shift op l n = case base op of+ "+" -> add (peel l) n+ "-" -> add (peel l) (negate n)+ _ -> (Just (UInfixE l (VarE op) (LitE (IntegerL n))), 0)++-- | Add a constant to a peeled @(base, offset)@.+add :: (Maybe Exp, Integer) -> Integer -> (Maybe Exp, Integer)+add (b, k) n = (b, k + n)++-- | Unqualified name of an operator (haskell-src-meta may leave it unqualified, so compare by base).+base :: Name -> String+base = nameBase++-- | The from->then step @then - from@, when it's a statically-known integer (same atom on both+-- sides, so the atoms cancel). Returns @Nothing@ for genuinely-symbolic steps (distinct atoms),+-- in which case the quasiquoter falls back to the ordinary, hint-free behavior.+constStep :: Exp -> Exp -> Maybe Integer+constStep from thn+ | bf == bt = Just (kt - kf)+ | otherwise = Nothing+ where (bf, kf) = peel from+ (bt, kt) = peel thn++-- | Splice a @`Maybe` `Integer`@ step hint into the generated call.+liftMStep :: Maybe Integer -> Q Exp+liftMStep Nothing = conE 'Nothing+liftMStep (Just n) = conE 'Just `appE` litE (integerL n) -- | Parses a string into a Haskell TH Exp using haskell-src-meta parseHaskellExpr :: Loc -> String -> Q Exp
Data/SBV/SMT/SMT.hs view
@@ -85,7 +85,7 @@ ) import Data.SBV.Utils.PrettyNum-import Data.SBV.Utils.Lib (joinArgs, splitArgs, needsBars, showText)+import Data.SBV.Utils.Lib (joinArgs, splitArgs, needsBars, showText, unQuote) import Data.SBV.Utils.SExpr (parenDeficit, nameSupply) import qualified System.Timeout as Timeout (timeout)@@ -773,17 +773,25 @@ defaultLineTO = Just (scaler defaultLineTimeOut) -- Default SBVException with solver config baked in; callers override fields as needed- solverException desc = SBVException { sbvExceptionDescription = desc- , sbvExceptionSent = Nothing- , sbvExceptionExpected = Nothing- , sbvExceptionReceived = Nothing- , sbvExceptionStdOut = Nothing- , sbvExceptionStdErr = Nothing- , sbvExceptionExitCode = Nothing- , sbvExceptionConfig = cfg { solver = (solver cfg) { executable = execPath } }- , sbvExceptionReason = Nothing- , sbvExceptionHint = Nothing- }+ solverException desc =+ let (errOut, description)+ | "(error" `isPrefixOf` desc+ = ( Just $ unQuote (dropWhile isSpace (dropWhile (not . isSpace) (init desc)))+ , "Unexpected solver error"+ )+ | True+ = (Nothing, desc)+ in SBVException { sbvExceptionDescription = description+ , sbvExceptionSent = Nothing+ , sbvExceptionExpected = Nothing+ , sbvExceptionReceived = Nothing+ , sbvExceptionStdOut = Nothing+ , sbvExceptionStdErr = errOut+ , sbvExceptionExitCode = Nothing+ , sbvExceptionConfig = cfg { solver = (solver cfg) { executable = execPath } }+ , sbvExceptionReason = Nothing+ , sbvExceptionHint = Nothing+ } (send, ask, getResponseFromSolver, terminateSolver, cleanUp, pid) <- do (inh, outh, errh, pid) <- runInteractiveProcess execPath opts Nothing Nothing@@ -856,7 +864,11 @@ pure $ dropWhile isSpace <$> mbCts in case timeOutToUse of- Nothing -> SolverRegular <$> getFullLine+ Nothing -> do l <- getFullLine+ -- If we see the line starting with error, we're about to die, so give up:+ pure $ if "(error" `isPrefixOf` l+ then SolverException l+ else SolverRegular l Just t -> do r <- Timeout.timeout t getFullLine case r of Just l -> pure $ SolverRegular l
Data/SBV/SMT/SMTLib2.hs view
@@ -35,7 +35,7 @@ import Data.SBV.SMT.Utils -import Data.SBV.Core.Symbolic ( QueryContext(..), SetOp(..), getUserName, getUserName', getSV, regExpToSMTString, NROp(..)+import Data.SBV.Core.Symbolic ( QueryContext(..), SetOp(..), getUserName, getUserName', getSV, regExpToSMTString, NROp(..), showNROp , SMTDef(..), SMTLambda(..), ResultInp(..), ProgInfo(..), SpecialRelOp(..), ADTOp(..) ) @@ -917,7 +917,8 @@ sh (SBVApp (NonLinear NR_Pow) [a, b]) | isZ3 || isCVC5 = "(^ " <> cvtSV a <> " " <> cvtSV b <> ")" - sh (SBVApp (NonLinear w) args) = "(" <> showText w <> " " <> T.unwords (map cvtSV args) <> ")"+ sh (SBVApp (NonLinear w) []) = T.pack (showNROp (name (solver cfg)) w)+ sh (SBVApp (NonLinear w) args) = "(" <> T.pack (showNROp (name (solver cfg)) w) <> " " <> T.unwords (map cvtSV args) <> ")" sh (SBVApp (PseudoBoolean pb) args) | hasPB = handlePB pb args'
Data/SBV/Utils/Numeric.hs view
@@ -92,7 +92,7 @@ | isNaN x = x | x == 0 = x | isInfinite x = x- | i == 0 = if x < 0 || isNegativeZero x then -0.0 else 0.0+ | i == 0 = if x < 0 then -0.0 else 0.0 | True = fromInteger i where i :: Integer i = round x
Documentation/SBV/Examples/ADT/Param.hs view
@@ -155,9 +155,9 @@ -- | Query mode example. -- -- >>> queryE--- e1: (let h = (-3 * -1) in (1 * h))+-- e1: (let a = (-3 * (8 + -7)) in ((a * (4 + a)) * -1)) -- e2: -2--- e3: (let d = 368 % 369 in d)+-- e3: (let h = 257 % 258 in h) queryE :: IO () queryE = runSMT $ do e1 :: SExpr String Integer <- free "e1"
Documentation/SBV/Examples/TP/Basics.hs view
@@ -295,6 +295,37 @@ r <- prove $ \x -> badM x .== badM x print r +-- | A termination measure is only a valid argument for termination if it takes values in a+-- /well-founded/ order: one with no infinite descending chains. Being non-negative and strictly+-- decreasing then forces the recursion to stop. The integers (bounded below by @0@) are well-founded,+-- but the reals are /not/: the chain @1, 1\/2, 1\/4, ...@ descends forever without ever reaching a+-- minimum. So a real-valued measure proves nothing.+--+-- Consider this Zeno-style non-terminating recursion: for any @x > 0@, the argument @x \/ 2@ is+-- again positive, so it never reaches the base case. Yet the measure @0 `smax` x@ is non-negative+-- and strictly decreases at the recursive call (@x \/ 2 < x@). Accepting it would mean certifying a+-- non-terminating function as terminating, which can be used to derive falsehoods.+--+-- @+-- zeno :: SReal -> SReal+-- zeno = smtFunctionWithMeasure \"zeno\" (\\x -> 0 \`smax\` x, [])+-- $ \\x -> ite (x .<= 0) 0 (zeno (x \/ 2))+-- @+--+-- SBV rules this out /at compile time/: the 'Data.SBV.Zero' class gates which types may be used as+-- measures, and there is deliberately no instance for algebraic reals. So the definition above does+-- not type-check, reporting:+--+-- @+-- • A termination measure may not have a real-valued result.+--+-- The reals are not well-ordered: an infinite descending chain such as+-- 1, 1\/2, 1\/4, ... has no least element, so a non-negative and strictly+-- decreasing real measure does not imply termination.+--+-- Use an integer-valued measure instead (e.g. a count of remaining steps).+-- @+ -- * Axioms and consistency -- | SBV checks that recursive functions defined via 'smtFunction' terminate, verifying a termination measure, which
Documentation/SBV/Examples/TP/Lists.hs view
@@ -375,7 +375,7 @@ -- Step: 1.2.4 Q.E.D. -- Step: 1.Completeness Q.E.D. -- Result: Q.E.D.--- Functions proven terminating: EnumSymbolic.Integer.enumFromThenTo.down, EnumSymbolic.Integer.enumFromThenTo.up+-- Functions proven terminating: EnumSymbolic.Integer.enumFromThenTo.up -- [Proven] enumLen :: Ɐn ∷ Integer → Ɐm ∷ Integer → Bool enumLen :: TP (Proof (Forall "n" Integer -> Forall "m" Integer -> SBool)) enumLen =@@ -396,7 +396,7 @@ -- -- The proof uses the metric @|m-n|@. ----- >>> runTP $ revNM+-- >>> runTP revNM -- Inductive lemma (strong): helper -- Step: Measure is non-negative Q.E.D. -- Step: 1 Q.E.D.
Documentation/SBV/Examples/TP/Numeric.hs view
@@ -76,8 +76,7 @@ -- Step: 2 Q.E.D. -- Step: 3 Q.E.D. -- Result: Q.E.D.--- Functions proven terminating:--- EnumSymbolic.Integer.enumFromThenTo.down, EnumSymbolic.Integer.enumFromThenTo.up, sbv.foldr+-- Functions proven terminating: EnumSymbolic.Integer.enumFromThenTo.down, sbv.foldr -- [Proven] sum_correct :: Ɐn ∷ Integer → Bool sumProof :: TP (Proof (Forall "n" Integer -> SBool)) sumProof = induct "sum_correct"@@ -103,9 +102,7 @@ -- Step: 5 Q.E.D. -- Step: 6 Q.E.D. -- Result: Q.E.D.--- Functions proven terminating:--- EnumSymbolic.Integer.enumFromThenTo.down, EnumSymbolic.Integer.enumFromThenTo.up,--- sbv.foldr, sbv.map+-- Functions proven terminating: EnumSymbolic.Integer.enumFromThenTo.down, sbv.foldr, sbv.map -- [Proven] sumSquare_correct :: Ɐn ∷ Integer → Bool sumSquareProof :: TP (Proof (Forall "n" Integer -> SBool)) sumSquareProof = do@@ -155,9 +152,7 @@ -- Step: 1 Q.E.D. -- Step: 2 Q.E.D. -- Result: Q.E.D.--- Functions proven terminating:--- EnumSymbolic.Integer.enumFromThenTo.down, EnumSymbolic.Integer.enumFromThenTo.up,--- sbv.foldr, sumCubed+-- Functions proven terminating: EnumSymbolic.Integer.enumFromThenTo.down, sbv.foldr, sumCubed -- [Proven] nicomachus :: Ɐn ∷ Integer → Bool nicomachus :: TP (Proof (Forall "n" Integer -> SBool)) nicomachus = do@@ -291,9 +286,7 @@ -- Step: 6 Q.E.D. -- Step: 7 Q.E.D. -- Result: Q.E.D.--- Functions proven terminating:--- EnumSymbolic.Integer.enumFromThenTo.down, EnumSymbolic.Integer.enumFromThenTo.up,--- sbv.foldr, sbv.map+-- Functions proven terminating: EnumSymbolic.Integer.enumFromThenTo.down, sbv.foldr, sbv.map -- [Proven] sumMulFactorial :: Ɐn ∷ Integer → Bool sumMulFactorial :: TP (Proof (Forall "n" Integer -> SBool)) sumMulFactorial = do
SBVTestSuite/GoldFiles/adt_gen00.gold view
@@ -267,11 +267,11 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (Let "y"- (Add (Val (- 2)) (Mul (Val (- 1)) (Val 3)))- (Let "a" (Val 13) (Add (Add (Val (- 3)) (Val 2)) (Var "a"))))))+[RECV] ((s0 (Let "m"+ (Add (Val 1) (Mul (Val (- 2)) (Val 0)))+ (Let "k" (Val 11) (Add (Add (Val (- 1)) (Val 2)) (Var "k")))))) -Got: (let y = (-2 + (-1 * 3)) in (let a = 13 in ((-3 + 2) + a)))+Got: (let m = (1 + (-2 * 0)) in (let k = 11 in ((-1 + 2) + k))) DONE *** Solver : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/adt_pgen00.gold view
@@ -267,11 +267,11 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (Let "s"- (Let "i" (Val 1) (Mul (Val 2) (Add (Var "i") (Var "i"))))- (Let "a" (Val 9) (Add (Val 3) (Var "a"))))))+[RECV] ((s0 (Let "l"+ (Let "n" (Val (- 1)) (Mul (Val (- 2)) (Add (Var "n") (Var "n"))))+ (Let "d" (Val 4) (Add (Add (Var "d") (Var "d")) (Var "d")))))) -Got: (let s = (let i = 1 in (2 * (i + i))) in (let a = 9 in (3 + a)))+Got: (let l = (let n = -1 in (-2 * (n + n))) in (let d = 4 in ((d + d) + d))) DONE *** Solver : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/exceptionLocal1.gold view
@@ -48,17 +48,11 @@ [GOOD] (define-fun s31 () (_ BitVec 32) (bvmul s30 s30)) [GOOD] (define-fun s32 () (_ BitVec 32) (bvmul s31 s31)) [GOOD] (define-fun s33 () (_ BitVec 32) (bvmul s32 s32))-[FAIL] (define-fun s34 () (_ BitVec 32) (bvmul s33 s33)) CAUGHT SMT EXCEPTION-*** Data.SBV: Unexpected non-success response from Yices:+*** Data.SBV: Unexpected solver error: *** *** Sent : (define-fun s34 () (_ BitVec 32) (bvmul s33 s33))-*** Expected : success-*** Received : (error "at line 40, column 35: in bvmul: maximal polynomial degree exceeded") ***-*** Exit code : ExitSuccess+*** Stderr : at line 40, column 35: in bvmul: maximal polynomial degree exceeded *** Executable: /usr/local/bin/yices-smt2 *** Options : --incremental-***-*** Reason : Check solver response for further information. If your code is correct,-*** please report this as an issue either with SBV or the solver itself!
SBVTestSuite/GoldFiles/exceptionLocal2.gold view
@@ -11,17 +11,11 @@ [GOOD] ; --- literal constants --- [GOOD] (define-fun s1 () Real (/ 2.0 1.0)) [GOOD] ; --- top level inputs ----[FAIL] (declare-fun s0 () Real) ; tracks user variable "x" CAUGHT SMT EXCEPTION-*** Data.SBV: Unexpected non-success response from Z3:+*** Data.SBV: Unexpected solver error: *** *** Sent : (declare-fun s0 () Real) ; tracks user variable "x"-*** Expected : success-*** Received : (error "line 8 column 23: logic does not support reals") ***-*** Exit code : ExitFailure (-15)+*** Stderr : line 8 column 23: logic does not support reals *** Executable: /usr/local/bin/z3 *** Options : -nw -in -smt2-***-*** Reason : Check solver response for further information. If your code is correct,-*** please report this as an issue either with SBV or the solver itself!
SBVTestSuite/GoldFiles/exceptionRemote1.gold view
@@ -1,3 +1,3 @@ -FINAL: "OK, we got: Unexpected response from the solver, context: assert"+FINAL: "OK, we got: Unexpected solver error" DONE!
SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.stderr view
@@ -15,8 +15,8 @@ (isLet e ==> (e .== e =: qed))] PCase17.hs:18:14: error: [GHC-83865] " Couldn't match expected type: Proof SBool- with actual type: sbv-14.2:Data.SBV.TP.TP.TPProofGen- (SBV Bool) [sbv-14.2:Data.SBV.TP.TP.Helper] ()+ with actual type: sbv-14.3:Data.SBV.TP.TP.TPProofGen+ (SBV Bool) [sbv-14.3:Data.SBV.TP.TP.Helper] () " In the expression: cases [(isZero e ==> (e .== e =: qed)), (isNum e ==> (e .== e =: qed)),
SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.stderr view
@@ -15,8 +15,8 @@ (isLet e ==> undefined)] PCase38.hs:12:14: error: [GHC-83865] " Couldn't match expected type: Proof SBool- with actual type: sbv-14.2:Data.SBV.TP.TP.TPProofGen- a0 [sbv-14.2:Data.SBV.TP.TP.Helper] ()+ with actual type: sbv-14.3:Data.SBV.TP.TP.TPProofGen+ a0 [sbv-14.3:Data.SBV.TP.TP.Helper] () " In the expression: cases [(isZero e ==> undefined), (isNum e ==> undefined),
SBVTestSuite/TestSuite/CompileTests/SCase/SCase101.stderr view
@@ -28,4 +28,4 @@ ((\ _ -> 1) (Data.SBV.Maybe.getJust_1 m)) (ite (Data.SBV.Maybe.isNothing m) 0- (symWithKind "unmatched_sCase_Maybe_6989586621679034958")))+ (symWithKind "unmatched_sCase_Maybe_6989586621679035004")))
SBVTestSuite/TestSuite/CompileTests/SCase/SCase59.stderr view
@@ -24,4 +24,4 @@ ((\ _ -> Data.SBV.Either.isRight (Data.SBV.Maybe.getJust_1 m)) (Data.SBV.Maybe.getJust_1 m))) ((\ _ -> 1) (Data.SBV.Maybe.getJust_1 m))- (symWithKind "unmatched_sCase_Maybe_6989586621679034958")))+ (symWithKind "unmatched_sCase_Maybe_6989586621679035004")))
SBVTestSuite/TestSuite/CompileTests/SCase/SCase66.stderr view
@@ -30,4 +30,4 @@ (ite (Data.SBV.Either.isRight e) ((\ _ -> 1) (Data.SBV.Either.getRight_1 e))- (symWithKind "unmatched_sCase_Either_6989586621679034920")))+ (symWithKind "unmatched_sCase_Either_6989586621679034966")))
SBVTestSuite/TestSuite/CompileTests/SCase/SCase89.stderr view
@@ -40,4 +40,4 @@ (isVar e) ((\ _ -> 1) (getVar_1 e)) (ite (isLet e) ((\ _ _ _ -> 3) (getLet_1 e) (getLet_2 e) (getLet_3 e))- (symWithKind "unmatched_sCase_Expr_6989586621679081453"))))))+ (symWithKind "unmatched_sCase_Expr_6989586621679081499"))))))
sbv.cabal view
@@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv-Version : 14.2+Version : 14.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