sbv 14.4 → 14.5

raw patch · 19 files changed

+624/−58 lines, 19 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGES.md +37/−0
• Data/SBV.hs +8/−2
• Data/SBV/Core/Model.hs +156/−11
• Data/SBV/Core/Operations.hs +29/−12
• Data/SBV/Core/Symbolic.hs +1/−0
• Data/SBV/List.hs +3/−3
• Data/SBV/Provers/Prover.hs +1/−0
• Data/SBV/Rational.hs +185/−1
• Data/SBV/SMT/SMTLib2.hs +40/−17
• Data/SBV/Trans.hs +4/−2
• Data/SBV/Utils/Numeric.hs +29/−0
• SBVTestSuite/TestSuite/Basics/ArithSolver.hs +122/−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

@@ -1,6 +1,43 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub:  <http://github.com/LeventErkok/sbv> +### Version 14.5, 2026-07-26++  * Add `sRationalToSReal` and `sRealToSRational`, converting between symbolic rationals and+    reals. The rational-to-real direction is always exact. The real-to-rational direction is+    exact for reals that are rational (introducing a defining constraint for symbolic inputs);+    note that applying it to an irrational value renders the problem unsatisfiable.++  * Add the `smtLib2Compliant` field to `SMTConfig` (default: `True`), controlling whether SBV+    asks the solver to be strictly SMTLib2 compliant. Turning it off can help with solvers (e.g.,+    z3) that otherwise mishandle overloaded operators when integers and reals are mixed in the+    same problem.++  * Add `sRealToSIntegerRM` and `sRationalToSIntegerRM`, which convert a real/rational to an+    integer using a symbolic rounding-mode argument, along with the helper `sCaseRoundingMode`+    for dispatching on a symbolic `SRoundingMode`. Thanks to Ryan Scott for the implementation.++  * [BACKWARDS COMPATIBILITY] The real-to-integer flooring function `sRealToSInteger` has been+    renamed to `sRealToSIntegerFloor`, for consistency with the new `sRealToSIntegerCeiling`,+    `sRealToSIntegerTruncate`, etc. (and with the rational counterparts below). If you use+    `sRealToSInteger`, simply replace it with `sRealToSIntegerFloor`; the behavior is unchanged.++  * Export the individual real-to-integer and rational-to-integer rounding functions, in addition+    to the rounding-mode-dispatched versions above: `sRealToSIntegerFloor`, `sRealToSIntegerCeiling`,+    `sRealToSIntegerTruncate`, `sRealToSIntegerRoundAway`, `sRealToSIntegerRoundToEven`, and the+    rational counterparts `sRationalToSIntegerFloor`, `sRationalToSIntegerCeiling`,+    `sRationalToSIntegerTruncate`, `sRationalToSIntegerRoundAway`, and `sRationalToSIntegerRoundToEven`.++  * Fix `svDivide` (i.e., `/` on unbounded integers in `Data.SBV.Dynamic`), which used flooring+    (`div`) on concrete integers instead of the Euclidean division that its symbolic counterpart+    (and `svQuot`) implements. The two now agree, always yielding a non-negative remainder.+    Thanks to Ryan Scott for the report.++  * Improve the Haddocks for `sQuot`, `sDiv`, `sRem`, `sMod`, and related functions, clarifying+    the truncating- vs. flooring-division distinction and documenting that the `Data.SBV.Dynamic`+    operations `svQuot`, `svRem`, and `svQuotRem` behave differently from their `s`-prefixed+    counterparts on unbounded integers. Thanks to Ryan Scott for the implementation.+ ### Version 14.4, 2026-07-03    * Add `curry` and `uncurry` (for symbolic 2-tuples) and `curry3` and `uncurry3` (for

@@ -230,9 +230,15 @@   , fpFromInteger   -- ** Rationals   , SRational, (.%)+  , sRationalToSIntegerFloor, sRationalToSIntegerCeiling, sRationalToSIntegerTruncate+  , sRationalToSIntegerRoundAway, sRationalToSIntegerRoundToEven, sRationalToSIntegerRM+  , sRationalToSReal, sRealToSRational   -- ** Algebraic reals   -- $algReals-  , SReal, AlgReal(..), sRealToSInteger, algRealToRational, RealPoint(..), realPoint, RationalCV(..)+  , SReal, AlgReal(..)+  , sRealToSIntegerFloor, sRealToSIntegerCeiling, sRealToSIntegerTruncate+  , sRealToSIntegerRoundAway, sRealToSIntegerRoundToEven, sRealToSIntegerRM+  , algRealToRational, RealPoint(..), realPoint, RationalCV(..)   -- ** Characters, Strings and Regular Expressions   -- $strings   , SChar, SString@@ -329,7 +335,7 @@   -- * IEEE-floating point numbers   , IEEEFloating(..), RoundingMode(..), SRoundingMode, nan, infinity, sNaN, sInfinity   -- ** Rounding modes-  , sRoundNearestTiesToEven, sRoundNearestTiesToAway, sRoundTowardPositive, sRoundTowardNegative, sRoundTowardZero, sRNE, sRNA, sRTP, sRTN, sRTZ+  , sRoundNearestTiesToEven, sRoundNearestTiesToAway, sRoundTowardPositive, sRoundTowardNegative, sRoundTowardZero, sRNE, sRNA, sRTP, sRTN, sRTZ, sCaseRoundingMode   -- ** Conversion to/from floats   -- $conversionNote   , IEEEFloatConvertible(..)

@@ -49,6 +49,7 @@   , sFloatingPoint, sFloatingPoint_, sFloatingPoints   , sRoundNearestTiesToEven, sRoundNearestTiesToAway, sRoundTowardPositive, sRoundTowardNegative, sRoundTowardZero   , sRNE, sRNA, sRTP, sRTN, sRTZ+  , sCaseRoundingMode   , sChar, sChar_, sChars, sString, sString_, sStrings, sList, sList_, sLists   , sRational, sRational_, sRationals   , SymTuple, sTuple, sTuple_, sTuples@@ -57,7 +58,9 @@   , sDivides   , solve   , slet-  , sRealToSInteger, sRealToSIntegerTruncate, label, observe, observeIf, sObserve+  , sRealToSIntegerFloor, sRealToSIntegerCeiling, sRealToSIntegerTruncate+  , sRealToSIntegerRoundAway, sRealToSIntegerRoundToEven, sRealToSIntegerRM+  , label, observe, observeIf, sObserve   , sAssert   , liftQRem, liftDMod, symbolicMergeWithKind   , genLiteral, genFromCV, genMkSymVar@@ -132,7 +135,7 @@ import Data.SBV.SMT.SMT        (ThmResult(..), showModel) import Data.SBV.SMT.Utils      (debug) -import Data.SBV.Utils.Numeric (fpIsEqualObjectH)+import Data.SBV.Utils.Numeric (fpIsEqualObjectH, roundAway)  import Data.IORef (readIORef, writeIORef, modifyIORef') import System.Mem.StableName (makeStableName, hashStableName)@@ -312,7 +315,23 @@ sRTZ :: SRoundingMode sRTZ = sRoundTowardZero +-- | Case analyzer for the type 'RoundingMode'.+sCaseRoundingMode ::+  Mergeable r => r              -- ^ What to return in the 'sRoundNearestTiesToEven' case.+              -> r              -- ^ What to return in the 'sRoundNearestTiesToAway' case.+              -> r              -- ^ What to return in the 'sRoundTowardPositive' case.+              -> r              -- ^ What to return in the 'sRoundTowardNegative' case.+              -> r              -- ^ What to return in the 'sRoundTowardZero' case.+              -> SRoundingMode+              -> r+sCaseRoundingMode fRNE fRNA fRTP fRTN fRTZ rm =+  ite (rm .== sRNE) fRNE $+  ite (rm .== sRNA) fRNA $+  ite (rm .== sRTP) fRTP $+  ite (rm .== sRTN) fRTN+                    fRTZ + instance SymVal Char where   mkSymVal                = genMkSymVar KChar   literal c               = SBV . SVal KChar . Left . CV KChar $ CChar c@@ -852,25 +871,140 @@ solve :: MonadSymbolic m => [SBool] -> m SBool solve = pure . sAnd --- | Convert an SReal to an SInteger. That is, it computes the--- largest integer @n@ that satisfies @sIntegerToSReal n <= r@--- essentially giving us the @floor@.+-- | Convert an SReal to an SInteger, @floor@ version. That is, it computes the+-- largest integer @n@ that satisfies @sIntegerToSReal n <= r@. -- -- For instance, @1.3@ will be @1@, but @-1.3@ will be @-2@.-sRealToSInteger :: SReal -> SInteger-sRealToSInteger x+--+-- See 'sRealToSIntegerRM' to select the rounding mode with a symbolic 'SRoundingMode'.+sRealToSIntegerFloor :: SReal -> SInteger+sRealToSIntegerFloor x   | Just i <- unliteral x, isExactRational i-  = literal $ floor (toRational i)+  = literal $ floor $ toRational i   | True   = SBV (SVal KUnbounded (Right (cache y)))   where y st = do xsv <- sbvToSV st x                   newExpr st KUnbounded (SBVApp (KindCast KReal KUnbounded) [xsv]) --- | Convert an SReal to an SInteger, truncating version. Truncate simply chops of the+-- | Convert an SReal to an SInteger, @ceiling@ version. That is, it computes+-- the smallest integer @n@ that satisfies @r <= sIntegerToSReal n@.+--+-- For instance, @1.3@ will be @2@, but @-1.3@ will be @-1@.+--+-- See 'sRealToSIntegerRM' to select the rounding mode with a symbolic 'SRoundingMode'.+sRealToSIntegerCeiling :: SReal -> SInteger+sRealToSIntegerCeiling x+  | Just i <- unliteral x, isExactRational i+  = literal $ ceiling $ toRational i+  | True+  = - sRealToSIntegerFloor (-x)++-- | Convert an SReal to an SInteger, truncating version. Truncate simply chops off the -- fractional part, essentially rounding towards zero.+--+-- For instance, @1.3@ will be @1@, and @-1.3@ will be @-1@.+--+-- See 'sRealToSIntegerRM' to select the rounding mode with a symbolic 'SRoundingMode'. sRealToSIntegerTruncate :: SReal -> SInteger-sRealToSIntegerTruncate x = ite (x .>= 0) (sRealToSInteger x) (- sRealToSInteger (-x))+sRealToSIntegerTruncate x+  | Just i <- unliteral x, isExactRational i+  = literal $ truncate $ toRational i+  | True+  = ite (x .>= 0) (sRealToSIntegerFloor x) (sRealToSIntegerCeiling x) +-- | Convert an SReal to an SInteger by converting to the nearest integer. If+-- there is a tie (i.e., if the fractional component of the SReal is equal to+-- 0.5), then round away from zero.+--+-- For instance:+--+-- * @1.3@ will be @1@+-- * @1.5@ will be @2@ (because @abs 1 < abs 2@)+-- * @1.7@ will be @2@+-- * @2.3@ will be @2@+-- * @2.5@ will be @3@ (because @abs 2 < abs 3@)+-- * @2.7@ will be @3@+-- * @-1.3@ will be @-1@+-- * @-1.5@ will be @-2@ (because @abs (-1) < abs (-2)@)+-- * @-1.7@ will be @-2@+-- * @-2.3@ will be @-2@+-- * @-2.5@ will be @-3@ (because @abs (-2) < abs (-3)@)+-- * @-2.7@ will be @-3@+--+-- See 'sRealToSIntegerRM' to select the rounding mode with a symbolic 'SRoundingMode'.+sRealToSIntegerRoundAway :: SReal -> SInteger+sRealToSIntegerRoundAway x+  | Just i <- unliteral x, isExactRational i+  = literal $ roundAway (toRational i)+  | True+  = ite+      (x .>= 0)+      (sRealToSIntegerFloor   (x + half))+      (sRealToSIntegerCeiling (x - half))+  where+    half :: SReal+    half = 0.5++-- | Convert an SReal to an SInteger by converting to the nearest integer. If+-- there is a tie (i.e., if the fractional component of the SReal is equal to+-- 0.5), then round to the nearest even integer.+--+-- For instance:+--+-- * @1.3@ will be @1@+-- * @1.5@ will be @2@ (because @2@ is even)+-- * @1.7@ will be @2@+-- * @2.3@ will be @2@+-- * @2.5@ will be @2@ (because @2@ is even)+-- * @2.7@ will be @3@+-- * @-1.3@ will be @-1@+-- * @-1.5@ will be @-2@ (because @-2@ is even)+-- * @-1.7@ will be @-2@+-- * @-2.3@ will be @-2@+-- * @-2.5@ will be @-2@ (because @-2@ is even)+-- * @-2.7@ will be @-3@+--+-- See 'sRealToSIntegerRM' to select the rounding mode with a symbolic 'SRoundingMode'.+sRealToSIntegerRoundToEven :: SReal -> SInteger+sRealToSIntegerRoundToEven x+  | Just i <- unliteral x, isExactRational i+  = literal $ round $ toRational i+  | True+  = ite (diff .< half) lo $+    ite (diff .> half) hi $+    ite (sDivides 2 lo) lo hi+  where+    half :: SReal+    half = 0.5++    lo, hi :: SInteger+    lo = sRealToSIntegerFloor x+    hi = lo+1++    diff :: SReal+    diff = x - sFromIntegral lo++-- | Convert an 'SReal' to an 'SInteger' according to the supplied+-- 'SRoundingMode'. This dispatches to 'sRealToSIntegerRoundToEven',+-- 'sRealToSIntegerRoundAway', 'sRealToSIntegerCeiling', 'sRealToSIntegerFloor',+-- and 'sRealToSIntegerTruncate' for the round-nearest-even, round-nearest-away,+-- round-toward-positive, round-toward-negative, and round-toward-zero modes+-- respectively.+--+-- Note that we re-use the 'SRoundingMode' type here, even though+-- 'SRoundingMode' is normally associated with floating-point operations. The+-- floating-point resemblance is superficial, as this function does not use any+-- floating-point functionality behind the scenes.+sRealToSIntegerRM :: SRoundingMode -> SReal -> SInteger+sRealToSIntegerRM rm x =+  sCaseRoundingMode+    (sRealToSIntegerRoundToEven x)+    (sRealToSIntegerRoundAway   x)+    (sRealToSIntegerCeiling     x)+    (sRealToSIntegerFloor       x)+    (sRealToSIntegerTruncate    x)+    rm+ -- | label: Label the result of an expression. This is essentially a no-op, but useful as it generates a comment in the generated C/SMT-Lib code. -- Note that if the argument is a constant, then the label is dropped completely, per the usual constant folding strategy. Compare this to 'observe' -- which is good for printing counter-examples.@@ -3250,7 +3384,18 @@ -- -- Note that our instances implement this law even when @x@ is @0@ itself. ----- NB. 'quot' truncates toward zero, while 'div' truncates toward negative infinity.+-- NB. 'sQuot' truncates toward zero (i.e., it implements truncating division),+-- while 'sDiv' truncates toward negative infinity (i.e., it implements+-- flooring division). These match the conventions of Haskell's 'quot' and+-- 'div' functions, respectively.+--+-- Similarly, 'sRem' and 'sMod' match the conventions of Haskell's 'rem' and+-- 'mod' functions, respectively. That is:+--+-- @+--      (x `sQuot` y)*y + (x `sRem` y) .== x+--      (x `sDiv`  y)*y + (x `sMod` y) .== x+-- @ -- -- === C code generation of division operations --

@@ -75,7 +75,7 @@  import Data.Ratio -import Data.SBV.Utils.Numeric (RoundingMode(..), {-fp2fp,-} fpIsEqualObjectH, fpIsNormalizedH, fpMaxH, fpMinH, fpRemH, fpRoundToIntegralH, floatToWord, doubleToWord, wordToFloat, wordToDouble)+import Data.SBV.Utils.Numeric (RoundingMode(..), divEucl, modEucl, {-fp2fp,-} fpIsEqualObjectH, fpIsNormalizedH, fpMaxH, fpMinH, fpRemH, fpRoundToIntegralH, floatToWord, doubleToWord, wordToFloat, wordToDouble)  import LibBF @@ -238,12 +238,16 @@         z = SVal k $ Left $ mkConstCV k (0 :: Integer)         i = SVal k $ Left $ mkConstCV k (1 :: Integer) --- | Division.+-- | Division. For integers, this behaves like 'svQuot', except that this+-- ensures @'svQuot' a 0 = a@. svDivide :: SVal -> SVal -> SVal-svDivide = liftSym2 (mkSymOp Quot) [rationalCheck] (/) idiv (/) (/) (/) (/)-   where idiv x 0 = x-         idiv x y = x `div` y+svDivide x y = liftSym2 (mkSymOp Quot) [rationalCheck] (/) idiv (/) (/) (/) (/) x y+   where isInteger = kindOf x == KUnbounded +         idiv a 0 = a+         idiv a b | isInteger = a `divEucl` b+                  | True      = a `quot` b+ -- | Divides predicate svDivides :: Integer -> SVal -> SVal svDivides n v@@ -316,6 +320,12 @@ -- non-negative remainder). For unsigned bitvectors, it is "bvudiv"; -- and for signed bitvectors it is "bvsdiv", which rounds toward zero. -- Note that this variant does not respect the division/reminder by 0. That's handled at the SBV level.+--+-- Note that despite the similarities in their names, the semantics of 'svQuot'+-- are different from those of the higher-level 'Data.SBV.sQuot' function when dealing+-- with unbounded integers. 'svQuot' implements Euclidean division (which+-- always has a non-negative remainder), whereas 'Data.SBV.sQuot' implements truncating+-- division (which may have a negative remainder). svQuot :: SVal -> SVal -> SVal svQuot x y   | not isInteger && isConcreteZero x = x@@ -327,15 +337,22 @@   where     isInteger = kindOf x == KUnbounded -    quot' a b | isInteger = div a (abs b) * signum b+    quot' a b | isInteger = divEucl a b               | True      = quot a b  -- | Remainder: Overloaded operation whose meaning depends on the kind at which -- it is used: For unbounded integers, it corresponds to the SMT-Lib--- "mod" operator (always non-negative). For unsigned bitvectors, it--- is "bvurem"; and for signed bitvectors it is "bvsrem", which rounds--- toward zero (sign of remainder matches that of @x@). Division by 0 is--- defined s.t. @x/0 = 0@, which holds even when @x@ itself is @0@.+-- "mod" operator ("Euclidean" modular division, which always has a+-- non-negative remainder). For unsigned bitvectors, it is "bvurem"; and for+-- signed bitvectors it is "bvsrem", which rounds toward zero (sign of+-- remainder matches that of @x@). Division by 0 is defined s.t. @x/0 = 0@,+-- which holds even when @x@ itself is @0@.+--+-- Note that despite the similarities in their names, the semantics of 'svRem'+-- are different from those of the higher-level 'Data.SBV.sRem' function when dealing+-- with unbounded integers. 'svRem' implements Euclidean modular division+-- (which always has a non-negative remainder), whereas 'Data.SBV.sRem' implements+-- truncating modular division (which may have a negative remainder). svRem :: SVal -> SVal -> SVal svRem x y   | not isInteger && isConcreteZero x = x@@ -347,10 +364,10 @@   where     isInteger = kindOf x == KUnbounded -    rem' a b | isInteger = mod a (abs b)+    rem' a b | isInteger = modEucl a b              | True      = rem a b --- | Combination of quot and rem+-- | Combination of 'svQuot' and 'svRem' svQuotRem :: SVal -> SVal -> (SVal, SVal) svQuotRem x y = (x `svQuot` y, x `svRem` y) 

@@ -2229,6 +2229,7 @@        , extraArgs                   :: [String]            -- ^ Extra command line arguments to pass to the solver.        , roundingMode                :: RoundingMode        -- ^ Rounding mode to use for floating-point calculations. Defaults to RNE.        , solverSetOptions            :: [SMTOption]         -- ^ Options to set as we start the solver+       , smtLib2Compliant            :: Bool                -- ^ Ask the solver to be strictly SMTLib2 compliant. (Default: True.)        , ignoreExitCode              :: Bool                -- ^ If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess.        , redirectVerbose             :: Maybe FilePath      -- ^ Redirect the verbose output to this file if given. If Nothing, stdout is implied.        , firstifyUniqueLen           :: Int                 -- ^ Unique length used for firstified higher-order function names

@@ -1415,7 +1415,7 @@         -- 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+        -- like 1, 1/2, 1/4, ... never reaches a minimum). 'sRealToSIntegerFloor' 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.         --@@ -1425,9 +1425,9 @@         -- 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), [])+        up   = smtFunctionWithMeasure "EnumSymbolic.AlgReal.enumFromThenTo.up"   (\start d end -> 0 `smax` (sRealToSIntegerFloor ((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), [])+        down = smtFunctionWithMeasure "EnumSymbolic.AlgReal.enumFromThenTo.down" (\start d end -> 0 `smax` (sRealToSIntegerFloor ((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.

@@ -107,6 +107,7 @@                                             , optimizeValidateConstraints = False                                             , roundingMode                = RoundNearestTiesToEven                                             , solverSetOptions            = startOpts+                                            , smtLib2Compliant            = True                                             , ignoreExitCode              = False                                             , redirectVerbose             = Nothing                                             , firstifyUniqueLen           = 10

@@ -17,12 +17,20 @@ module Data.SBV.Rational (     -- * Constructing rationals       (.%)-  ) where+    -- * Rounding rationals+    , sRationalToSIntegerFloor, sRationalToSIntegerCeiling, sRationalToSIntegerTruncate+    , sRationalToSIntegerRoundAway, sRationalToSIntegerRoundToEven, sRationalToSIntegerRM+    -- * Converting between rationals and reals+    , sRationalToSReal, sRealToSRational+    ) where  import qualified Data.Ratio as R +import Data.SBV.Core.AlgReals (isExactRational) import Data.SBV.Core.Data import Data.SBV.Core.Model+import Data.SBV.Core.Symbolic (newInternalVariable)+import Data.SBV.Utils.Numeric (roundAway)  infixl 7 .% @@ -42,6 +50,165 @@                    b <- sbvToSV st bot                    newExpr st KRational $ SBVApp RationalConstructor [t, b] +-- | Convert an SRational to an SInteger, @floor@ version. That is, it computes+-- the largest integer @n@ that satisfies @(n .% 1) <= r@.+--+-- For instance, @1.3@ will be @1@, but @-1.3@ will be @-2@.+--+-- See 'sRationalToSIntegerRM' to select the rounding mode with a symbolic 'SRoundingMode'.+sRationalToSIntegerFloor :: SRational -> SInteger+-- NB: We use @sDiv@ below because it implements division that truncates+-- towards negative infinity, which is exactly what @floor@ needs.+sRationalToSIntegerFloor = lift1 floor (uncurry sDiv)++-- | Convert an SRational to an SInteger, @ceiling@ version. That is, it+-- computes the smallest integer @n@ that satisfies @r <= (n .% 1)@.+--+-- For instance, @1.3@ will be @2@, but @-1.3@ will be @-1@.+--+-- See 'sRationalToSIntegerRM' to select the rounding mode with a symbolic 'SRoundingMode'.+sRationalToSIntegerCeiling :: SRational -> SInteger+sRationalToSIntegerCeiling x+  | Just i <- unliteral x+  = literal $ ceiling i+  | True+  = - (sRationalToSIntegerFloor (- x))++-- | Convert an SRational to an SInteger, truncating version. Truncate simply+-- chops off the fractional part, essentially rounding towards zero.+--+-- For instance, @1.3@ will be @1@, and @-1.3@ will be @-1@.+--+-- See 'sRationalToSIntegerRM' to select the rounding mode with a symbolic 'SRoundingMode'.+sRationalToSIntegerTruncate :: SRational -> SInteger+sRationalToSIntegerTruncate x+  | Just i <- unliteral x+  = literal $ truncate i+  | True+  = ite (x .>= 0) (sRationalToSIntegerFloor x) (sRationalToSIntegerCeiling x)++-- | Convert an SRational to an SInteger by converting to the nearest integer.+-- If there is a tie (i.e., if the fractional component of the SRational is+-- equal to 0.5), then round away from zero.+--+-- For instance:+--+-- * @1.3@ will be @1@+-- * @1.5@ will be @2@ (because @abs 1 < abs 2@)+-- * @1.7@ will be @2@+-- * @2.3@ will be @2@+-- * @2.5@ will be @3@ (because @abs 2 < abs 3@)+-- * @2.7@ will be @3@+-- * @-1.3@ will be @-1@+-- * @-1.5@ will be @-2@ (because @abs (-1) < abs (-2)@)+-- * @-1.7@ will be @-2@+-- * @-2.3@ will be @-2@+-- * @-2.5@ will be @-3@ (because @abs (-2) < abs (-3)@)+-- * @-2.7@ will be @-3@+--+-- See 'sRationalToSIntegerRM' to select the rounding mode with a symbolic 'SRoundingMode'.+sRationalToSIntegerRoundAway :: SRational -> SInteger+sRationalToSIntegerRoundAway x+  | Just i <- unliteral x+  = literal $ roundAway i+  | True+  = ite+      (x .>= 0)+      (sRationalToSIntegerFloor   (x + half))+      (sRationalToSIntegerCeiling (x - half))+  where+    half :: SRational+    half = 0.5++-- | Convert an SRational to an SInteger by converting to the nearest integer.+-- If there is a tie (i.e., if the fractional component of the SRational is+-- equal to 0.5), then round to the nearest even integer.+--+-- For instance:+--+-- * @1.3@ will be @1@+-- * @1.5@ will be @2@ (because @2@ is even)+-- * @1.7@ will be @2@+-- * @2.3@ will be @2@+-- * @2.5@ will be @2@ (because @2@ is even)+-- * @2.7@ will be @3@+-- * @-1.3@ will be @-1@+-- * @-1.5@ will be @-2@ (because @-2@ is even)+-- * @-1.7@ will be @-2@+-- * @-2.3@ will be @-2@+-- * @-2.5@ will be @-2@ (because @-2@ is even)+-- * @-2.7@ will be @-3@+--+-- See 'sRationalToSIntegerRM' to select the rounding mode with a symbolic 'SRoundingMode'.+sRationalToSIntegerRoundToEven :: SRational -> SInteger+sRationalToSIntegerRoundToEven x+  | Just i <- unliteral x+  = literal $ round i+  | True+  = ite (diff .< half) lo $+    ite (diff .> half) hi $+    ite (sDivides 2 lo) lo hi+  where+    half :: SRational+    half = 0.5++    lo, hi :: SInteger+    lo = sRationalToSIntegerFloor x+    hi = lo+1++    diff :: SRational+    diff = x - (lo .% 1)++-- | Convert an 'SRational' to an 'SInteger' according to the supplied+-- 'SRoundingMode'. This dispatches to 'sRationalToSIntegerRoundToEven',+-- 'sRationalToSIntegerRoundAway', 'sRationalToSIntegerCeiling',+-- 'sRationalToSIntegerFloor', and 'sRationalToSIntegerTruncate' for the+-- round-nearest-even, round-nearest-away, round-toward-positive,+-- round-toward-negative, and round-toward-zero modes respectively.+--+-- Note that we re-use the 'SRoundingMode' type here, even though+-- 'SRoundingMode' is normally associated with floating-point operations. The+-- floating-point resemblance is superficial, as this function does not use any+-- floating-point functionality behind the scenes.+sRationalToSIntegerRM :: SRoundingMode -> SRational -> SInteger+sRationalToSIntegerRM rm x =+  sCaseRoundingMode+    (sRationalToSIntegerRoundToEven x)+    (sRationalToSIntegerRoundAway x)+    (sRationalToSIntegerCeiling x)+    (sRationalToSIntegerFloor x)+    (sRationalToSIntegerTruncate x)+    rm++-- | Convert an 'SRational' to an 'SReal'. This conversion is always exact: the+-- rational @t .% b@ maps to the real @t \/ b@. (Recall that denominators are+-- always positive, so no division-by-zero can arise here.)+sRationalToSReal :: SRational -> SReal+sRationalToSReal = lift1 fromRational (\(t, b) -> sFromIntegral t / sFromIntegral b)++-- | Convert an 'SReal' to an 'SRational'. The conversion is /exact/ for reals+-- that are rational: a concrete rational is converted directly, while a+-- symbolic (or non-literal) real is handled by introducing a fresh symbolic+-- rational @r@ and constraining @'sRationalToSReal' r '.==' x@. Thus, whenever+-- the input real is representable as the ratio of two integers, the result+-- denotes exactly that same value---no precision is lost.+--+-- Note the caveat implied by this encoding: if the input real is /irrational/+-- (i.e., not expressible as a ratio of two integers), then the introduced+-- equality constraint is unsatisfiable, which renders the entire problem+-- @UNSAT@. In other words, using this function is an implicit assertion that+-- its argument is a rational number.+sRealToSRational :: SReal -> SRational+sRealToSRational x+  | Just v <- unliteral x, isExactRational v+  = literal (toRational v)+  | True+  = SBV $ SVal KRational $ Right $ cache res+  where res st = do n <- newInternalVariable st KRational+                    let r = SBV (SVal KRational (Right (cache (const (pure n))))) :: SRational+                    internalConstraint st False [] $ unSBV $ sRationalToSReal r .== x+                    pure n+ -- | Get the numerator. Note that this is always symbolic since we don't have a concrete representation. -- Furthermore this is only used internally and is not exported to the user, since it is not canonical. doNotExport_numerator :: SRational -> SInteger@@ -65,6 +232,23 @@   abs            = lift1 abs    (\(t, b) -> abs    t .% b)   negate         = lift1 negate (\(t, b) -> negate t .% b)   signum a       = ite (a .> 0) 1 $ ite (a .< 0) (-1) 0++-- | Fractional instance for SRational. Just like the 'Num' instance, division is+-- implemented at the SBV level via cross-multiplication, since SMTLib has no direct+-- support for our rational representation. Note that we keep the denominator positive:+-- dividing by @t2 .% b2@ multiplies the denominator by @t2@, which may be negative, so+-- we flip the signs of both parts when needed. Following the SBV convention for reals,+-- division by zero is defined to be zero.+--+-- We mark this @OVERLAPPING@ as it takes precedence over the generic instance in "Data.SBV.Core.Model",+-- which would otherwise try to translate rational division as an SMTLib @Quot@ (which doesn't exist for our rationals).+instance {-# OVERLAPPING #-} Fractional SRational where+  fromRational = literal . fromRational+  a / b        = ite (b .== 0) 0 (lift2 (/) divRat a b)+    where divRat (t1, b1) (t2, b2) = ite (t2 .> 0) (        num .%         den)+                                                   (negate  num .% negate  den)+             where num = t1 * b2+                   den = b1 * t2  -- | Symbolic ordering for SRational. Note that denominators are always positive. instance OrdSymbolic SRational where

@@ -229,7 +229,7 @@                     : concat [map T.pack flattenConfig | any needsFlattening kindInfo, Just flattenConfig <- [supportsFlattenedModels solverCaps]]          -- process all other settings we're given. If an option cannot be repeated, we only take the last one.-        userSettings = map (setSMTOption cfg) $ filter (not . isLogic) $ foldr comb [] $ solverSetOptions cfg+        userSettings = filter (not . T.null) $ map (setSMTOption cfg) $ filter (not . isLogic) $ foldr comb [] $ solverSetOptions cfg            where -- Logic is already processed, so drop it:                  isLogic SetLogic{} = True                  isLogic _          = False@@ -1250,7 +1250,25 @@          ascribe nm k = "(as " <> nm <> " " <> smtType k <> ")" --- Various casts+-- | Handle a kind-cast. This function only needs to cover the conversions that the type-safe API can actually+-- produce; the dynamic 'Data.SBV.Dynamic.svFromIntegral' can request other combinations, which we reject with an error.+--+-- The type-safe generators of a 'KindCast' are:+--+--     * 'Data.SBV.sFromIntegral' : @Integral a => SBV a -> SBV b@. The source is 'Integral', so it is always 'KBounded'+--       or 'KUnbounded'; the target is any @Num@/@SymVal@ kind (bounded, unbounded, real, rational, or float/double/FP).+--     * 'Data.SBV.sRealToSIntegerFloor': only ever emits @KReal -> KUnbounded@.+--     * shift-amount adjustment: only ever emits @KBounded -> KBounded@.+--+-- So the reachable (from, to) pairs are exactly:+--+--     * @KBounded   -> {KBounded, KUnbounded, KReal, KRational, KFloat/KDouble/KFP}@+--     * @KUnbounded -> {KBounded, KUnbounded, KReal, KRational, KFloat/KDouble/KFP}@+--     * @KReal      -> KUnbounded@+--+-- All of these are handled below (float/double/FP targets are routed through 'handleFPCast' via @tryFPCast@). Note+-- that a real or rational can never be a source (reals only appear via 'Data.SBV.sRealToSIntegerFloor', which targets 'KUnbounded';+-- rationals are not 'Integral'), so those directions are unreachable and left to 'error'. handleKindCast :: Kind -> Kind -> Text -> Text handleKindCast kFrom kTo a   | kFrom == kTo@@ -1258,6 +1276,8 @@   | True   = case kFrom of       KBounded s m -> case kTo of+                        KReal        -> handleKindCast KUnbounded KReal     (handleKindCast kFrom KUnbounded a)+                        KRational    -> handleKindCast KUnbounded KRational (handleKindCast kFrom KUnbounded a)                         KBounded _ n -> fromBV (if s then signExtend else zeroExtend) m n                         KUnbounded   -> if s then "(sbv_to_int " <> a <> ")"                                              else "(ubv_to_int " <> a <> ")"@@ -1266,6 +1286,7 @@       KUnbounded   -> case kTo of                         KReal        -> "(to_real " <> a <> ")"                         KBounded _ n -> "((_ int_to_bv " <> showText n <> ") " <> a <> ")"+                        KRational    -> "(SBV.Rational " <> a <> " 1)"                         _            -> tryFPCast        KReal        -> case kTo of@@ -1316,21 +1337,23 @@ -- | Translate an option setting to SMTLib. Note the SetLogic/SetInfo discrepancy. setSMTOption :: SMTConfig -> SMTOption -> Text setSMTOption cfg = set-  where set (DiagnosticOutputChannel   f) = opt   [":diagnostic-output-channel",   showText f]-        set (ProduceAssertions         b) = opt   [":produce-assertions",          smtBool b]-        set (ProduceAssignments        b) = opt   [":produce-assignments",         smtBool b]-        set (ProduceProofs             b) = opt   [":produce-proofs",              smtBool b]-        set (ProduceInterpolants       b) = opt   [":produce-interpolants",        smtBool b]-        set (ProduceUnsatAssumptions   b) = opt   [":produce-unsat-assumptions",   smtBool b]-        set (ProduceUnsatCores         b) = opt   [":produce-unsat-cores",         smtBool b]-        set (ProduceAbducts            b) = opt   [":produce-abducts",             smtBool b]-        set (RandomSeed                i) = opt   [":random-seed",                 showText i]-        set (ReproducibleResourceLimit i) = opt   [":reproducible-resource-limit", showText i]-        set (SMTVerbosity              i) = opt   [":verbosity",                   showText i]-        set (OptionKeyword          k as) = opt   (T.pack k : map T.pack as)-        set (SetLogic                  l) = logicString cfg l-        set (SetInfo                k as) = info  (T.pack k : map T.pack as)-        set (SetTimeOut                i) = opt   $ timeOut i+  where set (DiagnosticOutputChannel   f)           = opt [":diagnostic-output-channel",   showText f]+        set (ProduceAssertions         b)           = opt [":produce-assertions",          smtBool b]+        set (ProduceAssignments        b)           = opt [":produce-assignments",         smtBool b]+        set (ProduceProofs             b)           = opt [":produce-proofs",              smtBool b]+        set (ProduceInterpolants       b)           = opt [":produce-interpolants",        smtBool b]+        set (ProduceUnsatAssumptions   b)           = opt [":produce-unsat-assumptions",   smtBool b]+        set (ProduceUnsatCores         b)           = opt [":produce-unsat-cores",         smtBool b]+        set (ProduceAbducts            b)           = opt [":produce-abducts",             smtBool b]+        set (RandomSeed                i)           = opt [":random-seed",                 showText i]+        set (ReproducibleResourceLimit i)           = opt [":reproducible-resource-limit", showText i]+        set (SMTVerbosity              i)           = opt [":verbosity",                   showText i]+        set (OptionKeyword ":smtlib2_compliant" _)+          | not (smtLib2Compliant cfg)              = ""+        set (OptionKeyword          k as)           = opt (T.pack k : map T.pack as)+        set (SetLogic                  l)           = logicString cfg l+        set (SetInfo                k as)           = info (T.pack k : map T.pack as)+        set (SetTimeOut                i)           = opt $ timeOut i          opt   xs = "(set-option " <> T.unwords xs <> ")"         info  xs = "(set-info "   <> T.unwords xs <> ")"

@@ -33,7 +33,9 @@   -- ** Floating point numbers   , SFloat, SDouble, SFloatingPoint   -- ** Algebraic reals-  , SReal, AlgReal, sRealToSInteger+  , SReal, AlgReal+  , sRealToSIntegerFloor, sRealToSIntegerCeiling, sRealToSIntegerTruncate+  , sRealToSIntegerRoundAway, sRealToSIntegerRoundToEven, sRealToSIntegerRM   -- ** Characters, Strings and Regular Expressions   , SChar, SString   -- ** Symbolic lists@@ -71,7 +73,7 @@   -- * IEEE-floating point numbers   , IEEEFloating(..), RoundingMode(..), SRoundingMode, nan, infinity, sNaN, sInfinity   -- ** Rounding modes-  , sRoundNearestTiesToEven, sRoundNearestTiesToAway, sRoundTowardPositive, sRoundTowardNegative, sRoundTowardZero, sRNE, sRNA, sRTP, sRTN, sRTZ+  , sRoundNearestTiesToEven, sRoundNearestTiesToAway, sRoundTowardPositive, sRoundTowardNegative, sRoundTowardZero, sRNE, sRNA, sRTP, sRTN, sRTZ, sCaseRoundingMode   -- ** Conversion to/from floats   , IEEEFloatConvertible(..) 

@@ -16,6 +16,8 @@  module Data.SBV.Utils.Numeric (            fpMaxH, fpMinH, fp2fp, fpRemH, fpRoundToIntegralH, fpIsEqualObjectH, fpCompareObjectH, fpIsNormalizedH+         , roundAway+         , divEucl, modEucl          , floatToWord, wordToFloat, doubleToWord, wordToDouble          , RoundingMode(..), smtRoundingMode          ) where@@ -124,6 +126,33 @@ -- and also this is not simply the negation of isDenormalized! fpIsNormalizedH :: RealFloat a => a -> Bool fpIsNormalizedH x = not (isDenormalized x || isInfinite x || isNaN x || x == 0)++-- | @'roundAway' x@ returns the nearest integer to @x@; the integer furthest+-- away from @0@ if @x@ is equidistant between two integers.++-- This implementation is taken directly from the @fp-ieee@ library. Somewhat+-- surprisingly, 'roundAway' is not a method of the 'RealFrac' class!+roundAway :: (RealFrac a, Integral b) => a -> b+roundAway x = case properFraction x of+                -- x == n + f, signum x == signum f, 0 <= abs f < 1+                (n,r) -> if abs r < 0.5 then+                           n+                         else+                           if r < 0 then+                             n - 1+                           else+                             n + 1++-- | Euclidean division. @'divEucl' a b@ returns the integer @q@ satisfying the+-- equations @a = (b * q) + r@ and @0 <= r < abs b@, where @'modEucl' a b = r@.+divEucl :: Integral a => a -> a -> a+divEucl a b = div a (abs b) * signum b++-- | Euclidean modular division. @'modEucl' a b@ returns the integer @r@+-- satisfying the equations @a = (b * q) + r@ and @0 <= r < abs b@, where+-- @'divEucl' a b = q@.+modEucl :: Integral a => a -> a -> a+modEucl a b = mod a (abs b)  ------------------------------------------------------------------------- -- Reinterpreting float/double as word32/64 and back. Here, we use the

@@ -85,6 +85,7 @@      ++ genLists      ++ genEnums      ++ misc+     ++ realRatConvs      )  genExtends :: [TestTree]@@ -388,7 +389,7 @@ genDoubles :: [TestTree] genDoubles = genIEEE754 "genDoubles" ds -genIEEE754 :: (IEEEFloating a, OrdSymbolic (SBV a), Num (SBV a), Show a) => String -> [a] -> [TestTree]+genIEEE754 :: (IEEEFloating a, OrdSymbolic (SBV a), Num (SBV a), Fractional (SBV a), Show a) => String -> [a] -> [TestTree] genIEEE754 origin vs =  [tst1 ("pred_"   ++ nm, x, y)    | (nm, x, y)    <- preds]                      ++ [tst1 ("unary_"  ++ nm, x, y)    | (nm, x, y)    <- uns]                      ++ [tst2 ("binary_" ++ nm, x, y, r) | (nm, x, y, r) <- bins]@@ -921,6 +922,126 @@  where -- https://stackoverflow.com/questions/69033969/trivial-rationals-problems-without-variables-in-sbv-solver-in-haskell        t1 = do _xs <- sRationals []                constrain $ (5.%1:: SRational) .<= (5.%1:: SRational)++realRatConvs :: [TestTree]+realRatConvs = [ testCase "realConv1" $ assertIsThm $ respectsLe sRealToSIntegerRM+               , testCase "realConv2" $ assertIsThm realFloorCorrect+               , testCase "realConv3" $ assertIsThm realFloorCorrect2+               , testCase "realConv4" $ assertIsThm realCeilingCorrect+               , testCase "realConv5" $ assertIsThm realCeilingCorrect2+               , testCase "realConv6" $ assertIsThm $ realRoundNearest sRNE+               , testCase "realConv7" $ assertIsThm $ realRoundNearest sRNA+               , testCase "realConv8" $ assertIsThm realRneTieEven+               , testCase "realConv9" $ assertIsThm realRnaTieAway++               , testCase "ratConv1"  $ assertIsThm $ respectsLe sRationalToSIntegerRM+               , testCase "ratConv2"  $ assertIsThm rationalFloorCorrect+               , testCase "ratConv3"  $ assertIsThm rationalFloorCorrect2+               , testCase "ratConv4"  $ assertIsThm rationalCeilingCorrect+               , testCase "ratConv5"  $ assertIsThm rationalCeilingCorrect2+               , testCase "ratConv6"  $ assertIsThm $ ratRoundNearest sRNE+               , testCase "ratConv7"  $ assertIsThm $ ratRoundNearest sRNA+               , testCase "ratConv8"  $ assertIsThm ratRneTieEven+               , testCase "ratConv9"  $ assertIsThm ratRnaTieAway++               -- z3 struggles with this in the compliant mode so we turn compliance off for these two+               , testCase "ratRealRoundTrip1" $ assert $ isTheoremWith z3{smtLib2Compliant = False} ratToRealToRat+               , testCase "ratRealRoundTrip2" $ assert $ isTheoremWith z3{smtLib2Compliant = False} realToRatToReal++               , testCase "convertCov1" $ assertIsSat (\x y -> sFromIntegral @Word8   @Integer  x .== y)+               , testCase "convertCov2" $ assertIsSat (\x y -> sFromIntegral @Integer @Word8    x .== y)+               , testCase "convertCov3" $ assertIsSat (\x y -> sFromIntegral @Integer @AlgReal  x .== y)+               , testCase "convertCov4" $ assertIsSat (\x y -> sFromIntegral @Integer @Float    x .== y)+               , testCase "convertCov5" $ assertIsSat (\x y -> sFromIntegral @Word8   @Float    x .== y)+               , testCase "convertCov6" $ assertIsSat (\x y -> sFromIntegral @Integer @Rational x .== y)+               , testCase "convertCov7" $ assertIsSat (\x y -> sFromIntegral @Word8   @AlgReal  x .== y)+               , testCase "convertCov8" $ assertIsSat (\x y -> sFromIntegral @Word8   @Rational x .== y)+               , testCase "convertCov9" $ assertIsSat $ \(x :: SRational) (y :: SRational) (r :: SRational) -> (x / y) .== r++               , testCase "ratDiv1" $ assertIsThm ratDivCancels+               , testCase "ratDiv2" $ assertIsThm ratDivByZero+               ]+ where -- (x <= y) ==> (round x <= round y)+       respectsLe :: OrdSymbolic a => (SRoundingMode -> a -> SInteger) -> SRoundingMode -> a -> a -> SBool+       respectsLe rnd rm x y = (x .<= y) .=> (rnd rm x .<= rnd rm y)++       -- floor x <= x+       realFloorCorrect :: SReal -> SBool+       realFloorCorrect x = sFromIntegral (sRealToSIntegerRM sRTN x) .<= x++       -- (x <= y) ==> (x <= floor y) [where x is an Integer]+       realFloorCorrect2 :: SInteger -> SReal -> SBool+       realFloorCorrect2 x y = (sFromIntegral x .<= y) .=> (x .<= sRealToSIntegerRM sRTN y)++       -- ceiling x >= x+       realCeilingCorrect :: SReal -> SBool+       realCeilingCorrect x = sFromIntegral (sRealToSIntegerRM sRTP x) .>= x++       -- (x >= y) ==> (x >= ceiling y) [where x is an integer]+       realCeilingCorrect2 :: SInteger -> SReal -> SBool+       realCeilingCorrect2 x y = (sFromIntegral x .>= y) .=> (x .>= sRealToSIntegerRM sRTP y)++       -- Rounding to nearest is within 1/2 of the input (holds for both round-to-even and round-away).+       realRoundNearest :: SRoundingMode -> SReal -> SBool+       realRoundNearest rm x = abs (sFromIntegral (sRealToSIntegerRM rm x) - x) .<= 0.5++       -- On a tie (x = k + 1/2), round-to-even produces an even integer.+       realRneTieEven :: SInteger -> SBool+       realRneTieEven k = sDivides 2 (sRealToSIntegerRM sRNE x)+         where x = sFromIntegral k + 0.5 :: SReal++       -- On a tie (x = k + 1/2), round-away picks the integer further from zero.+       realRnaTieAway :: SInteger -> SBool+       realRnaTieAway k = sRealToSIntegerRM sRNA x .== ite (x .>= 0) (k+1) k+         where x = sFromIntegral k + 0.5 :: SReal++       -- floor x <= x+       rationalFloorCorrect :: SRational -> SBool+       rationalFloorCorrect x = (sRationalToSIntegerRM sRTN x .% 1) .<= x++       -- (x <= y) ==> (x <= floor y) [where x is an integer]+       rationalFloorCorrect2 :: SInteger -> SRational -> SBool+       rationalFloorCorrect2 x y = ((x .% 1) .<= y) .=> (x .<= sRationalToSIntegerRM sRTN y)++       -- (x >= y) ==> (x >= ceiling y) [where x is an integer]+       rationalCeilingCorrect2 :: SInteger -> SRational -> SBool+       rationalCeilingCorrect2 x y = ((x .% 1) .>= y) .=> (x .>= sRationalToSIntegerRM sRTP y)++       -- ceiling x >= x+       rationalCeilingCorrect :: SRational -> SBool+       rationalCeilingCorrect x = (sRationalToSIntegerRM sRTP x .% 1) .>= x++       -- Rounding to nearest is within 1/2 of the input (holds for both round-to-even and round-away).+       ratRoundNearest :: SRoundingMode -> SRational -> SBool+       ratRoundNearest rm x = abs ((sRationalToSIntegerRM rm x .% 1) - x) .<= (1 .% 2)++       -- On a tie (x = k + 1/2), round-to-even produces an even integer.+       ratRneTieEven :: SInteger -> SBool+       ratRneTieEven k = sDivides 2 (sRationalToSIntegerRM sRNE x)+         where x = (2*k+1) .% 2++       -- On a tie (x = k + 1/2), round-away picks the integer further from zero.+       ratRnaTieAway :: SInteger -> SBool+       ratRnaTieAway k = sRationalToSIntegerRM sRNA x .== ite (x .>= 0) (k+1) k+         where x = (2*k+1) .% 2++       -- Division cancels: for a non-zero divisor, (x / y) * y == x.+       ratDivCancels :: SRational -> SRational -> SBool+       ratDivCancels x y = (y ./= 0) .=> ((x / y) * y .== x)++       -- Division by zero is defined to be zero, matching the SBV convention for reals.+       ratDivByZero :: SRational -> SRational -> SBool+       ratDivByZero x y = (y .== 0) .=> ((x / y) .== 0)++       -- rational -> real -> rational is the identity: no precision is lost.+       ratToRealToRat :: SRational -> SBool+       ratToRealToRat x = sRealToSRational (sRationalToSReal x) .== x++       -- real -> rational -> real is the identity. Recall that sRealToSRational+       -- implicitly asserts that its argument is rational, so this holds for+       -- every (well-defined) real here.+       realToRatToReal :: SReal -> SBool+       realToRatToReal x = sRationalToSReal (sRealToSRational x) .== x  -- Test these with make test TGT=sEnum_ genEnums :: [TestTree]

@@ -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.4:Data.SBV.TP.TP.TPProofGen-                                      (SBV Bool) [sbv-14.4:Data.SBV.TP.TP.Helper] ()+                  with actual type: sbv-14.5:Data.SBV.TP.TP.TPProofGen+                                      (SBV Bool) [sbv-14.5:Data.SBV.TP.TP.Helper] ()     " In the expression:         cases           [(isZero e ==> (e .== e =: qed)), (isNum e ==> (e .== e =: qed)),

@@ -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.4:Data.SBV.TP.TP.TPProofGen-                                      a0 [sbv-14.4:Data.SBV.TP.TP.Helper] ()+                  with actual type: sbv-14.5:Data.SBV.TP.TP.TPProofGen+                                      a0 [sbv-14.5:Data.SBV.TP.TP.Helper] ()     " In the expression:         cases           [(isZero e ==> undefined), (isNum e ==> undefined),

@@ -28,4 +28,4 @@          ((\ _ -> 1) (Data.SBV.Maybe.getJust_1 m))          (ite             (Data.SBV.Maybe.isNothing m) 0-            (symWithKind "unmatched_sCase_Maybe_6989586621679035008")))+            (symWithKind "unmatched_sCase_Maybe_6989586621679035040")))

@@ -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_6989586621679035008")))+            (symWithKind "unmatched_sCase_Maybe_6989586621679035040")))

@@ -30,4 +30,4 @@          (ite             (Data.SBV.Either.isRight e)             ((\ _ -> 1) (Data.SBV.Either.getRight_1 e))-            (symWithKind "unmatched_sCase_Either_6989586621679034970")))+            (symWithKind "unmatched_sCase_Either_6989586621679035002")))

@@ -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_6989586621679080570"))))))+                     (symWithKind "unmatched_sCase_Expr_6989586621679080602"))))))

@@ -1,7 +1,7 @@ Cabal-Version: 2.2  Name        : sbv-Version     : 14.4+Version     : 14.5 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