diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,43 @@ * Hackage: * GitHub: +### 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 diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -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(..) diff --git a/Data/SBV/Core/Model.hs b/Data/SBV/Core/Model.hs --- a/Data/SBV/Core/Model.hs +++ b/Data/SBV/Core/Model.hs @@ -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 -- diff --git a/Data/SBV/Core/Operations.hs b/Data/SBV/Core/Operations.hs --- a/Data/SBV/Core/Operations.hs +++ b/Data/SBV/Core/Operations.hs @@ -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) diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs --- a/Data/SBV/Core/Symbolic.hs +++ b/Data/SBV/Core/Symbolic.hs @@ -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 diff --git a/Data/SBV/List.hs b/Data/SBV/List.hs --- a/Data/SBV/List.hs +++ b/Data/SBV/List.hs @@ -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. diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs --- a/Data/SBV/Provers/Prover.hs +++ b/Data/SBV/Provers/Prover.hs @@ -107,6 +107,7 @@ , optimizeValidateConstraints = False , roundingMode = RoundNearestTiesToEven , solverSetOptions = startOpts + , smtLib2Compliant = True , ignoreExitCode = False , redirectVerbose = Nothing , firstifyUniqueLen = 10 diff --git a/Data/SBV/Rational.hs b/Data/SBV/Rational.hs --- a/Data/SBV/Rational.hs +++ b/Data/SBV/Rational.hs @@ -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 diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -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 <> ")" diff --git a/Data/SBV/Trans.hs b/Data/SBV/Trans.hs --- a/Data/SBV/Trans.hs +++ b/Data/SBV/Trans.hs @@ -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(..) diff --git a/Data/SBV/Utils/Numeric.hs b/Data/SBV/Utils/Numeric.hs --- a/Data/SBV/Utils/Numeric.hs +++ b/Data/SBV/Utils/Numeric.hs @@ -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 diff --git a/SBVTestSuite/TestSuite/Basics/ArithSolver.hs b/SBVTestSuite/TestSuite/Basics/ArithSolver.hs --- a/SBVTestSuite/TestSuite/Basics/ArithSolver.hs +++ b/SBVTestSuite/TestSuite/Basics/ArithSolver.hs @@ -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] diff --git a/SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.stderr b/SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.stderr --- a/SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.stderr +++ b/SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.stderr @@ -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)), diff --git a/SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.stderr b/SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.stderr --- a/SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.stderr +++ b/SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.stderr @@ -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), diff --git a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase101.stderr b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase101.stderr --- a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase101.stderr +++ b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase101.stderr @@ -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"))) diff --git a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase59.stderr b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase59.stderr --- a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase59.stderr +++ b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase59.stderr @@ -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"))) diff --git a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase66.stderr b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase66.stderr --- a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase66.stderr +++ b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase66.stderr @@ -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"))) diff --git a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase89.stderr b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase89.stderr --- a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase89.stderr +++ b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase89.stderr @@ -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")))))) diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -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