diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,31 @@ * Hackage: * GitHub: +### Version 14.2, 2026-06-05 + + * Fix float to integer conversions, which were ignoring the rounding mode previously. Thanks to + Ryan Scott for the report. + + * Fix the implementation of properFraction for arbitrary-sized floats. Thanks to Ryan Scott + for the report and the fix. + + * Fix a bug in pCase, where SBV was over-approximating the bound variables, causing the + unused-variable warning checker to flag branches unnecessarily in generated code. + + * New TP example: Run-length encoding roundtrip (`Documentation.SBV.Examples.TP.RunLength`). + Proves that `decode (encode xs) == xs` for a run-length encode/decode pair. + + * New TP example: Two-stack queue (`Documentation.SBV.Examples.TP.Queue`). + Proves that a queue implemented with two lists (front/back) correctly implements + FIFO semantics via an abstraction function. + + * New cabal flag `compile_examples` (default: True) controls whether the + `Documentation.SBV.Examples.*` modules are built as part of the library. + Disable with `-f-compile_examples` when using SBV as a dependency to skip + compiling the example modules. Thanks to Robin Webbers for the contribution. + + * Add more floating-point operations to `Data.SBV.Dynamic`. Thanks to Ryan Scott for the patch. + ### Version 14.1, 2026-05-04 * [BACKWARDS COMPATIBILITY] Removed `tpRibbon`. The ribbon length for TP proof diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -1341,7 +1341,7 @@ same thing! Same goes for Haskell, which seems to convert via Int64, but we do not model that behavior in SBV as it doesn't seem to be intentional nor well documented. -You can check for @NaN@, @oo@ and @-oo@, using the predicates 'fpIsNaN', 'fpIsInfinite', +You can check for @NaN@, @oo@ and @-oo@, using the predicates 'Data.SBV.Core.Floating.fpIsNaN', 'Data.SBV.Core.Floating.fpIsInfinite', and 'fpIsPositive', 'fpIsNegative' predicates, respectively; and do the proper conversion based on your needs. (0 is a good choice, as are min/max bounds of the target type.) diff --git a/Data/SBV/Core/Concrete.hs b/Data/SBV/Core/Concrete.hs --- a/Data/SBV/Core/Concrete.hs +++ b/Data/SBV/Core/Concrete.hs @@ -444,6 +444,40 @@ mkConstCV k@KTuple{} a = error $ "Unexpected call to mkConstCV (" ++ show k ++ ") with value: " ++ show (toInteger a) mkConstCV k@KArray{} a = error $ "Unexpected call to mkConstCV (" ++ show k ++ ") with value: " ++ show (toInteger a) +-- | Create a constant value from a floating-point value. +fpConstCV :: + -- | Must be 'KFloat', 'KDouble', or 'KFP'. + Kind -> + -- | The constant to use when the kind is 'KFloat'. + Float -> + -- | The constant to use when the kind is 'KDouble'. + Double -> + -- | The constant to make when the kind is 'KFP', where the 'Int's represent + -- the exponent and significand sizes. + (Int -> Int -> FP) -> + CV +fpConstCV k cf cd cfp = + case k of + KFloat -> CV k $ CFloat cf + KDouble -> CV k $ CDouble cd + KFP eb sb -> CV k $ CFP $ cfp eb sb + + KVar{} -> unexpected + KBool{} -> unexpected + KBounded{} -> unexpected + KUnbounded{} -> unexpected + KReal{} -> unexpected + KRational{} -> unexpected + KChar{} -> unexpected + KString{} -> unexpected + KApp{} -> unexpected + KADT{} -> unexpected + KList{} -> unexpected + KSet{} -> unexpected + KTuple{} -> unexpected + KArray{} -> unexpected + where unexpected = error $ "Data.SBV.fpConstCV: Unexpected kind: " ++ show k + -- | Generate a random constant value ('CVal') of the correct kind. We error out for a completely uninterpreted type. randomCVal :: Kind -> IO CVal randomCVal k = diff --git a/Data/SBV/Core/Floating.hs b/Data/SBV/Core/Floating.hs --- a/Data/SBV/Core/Floating.hs +++ b/Data/SBV/Core/Floating.hs @@ -40,7 +40,7 @@ import Data.SBV.Core.AlgReals (isExactRational) import Data.SBV.Core.Sized -import Data.SBV.Core.SizedFloats +import Data.SBV.Core.SizedFloats hiding (fpIsNaN, fpIsZero) import Data.SBV.Core.Data import Data.SBV.Core.Kind @@ -679,12 +679,7 @@ -- Map SBV's rounding modes to LibBF's rmToRM :: SRoundingMode -> Maybe RoundMode -rmToRM srm = cvt <$> unliteral srm - where cvt RoundNearestTiesToEven = NearEven - cvt RoundNearestTiesToAway = NearAway - cvt RoundTowardPositive = ToPosInf - cvt RoundTowardNegative = ToNegInf - cvt RoundTowardZero = ToZero +rmToRM srm = roundingModeToRoundMode <$> unliteral srm -- | Lift a 1 arg Big-float op lift1FP :: forall eb sb. ValidFloat eb sb => 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 @@ -266,12 +266,11 @@ isConcretely _ _ = False instance SymVal RoundingMode where - literal s = SBV $ SVal kRoundingMode $ Left $ CV kRoundingMode $ CADT (show s, []) - fromCV (CV k (CADT (s, []))) - | k == kRoundingMode - , Just mode <- s `lookup` [(show m, m) | m <- [minBound .. maxBound :: RoundingMode]] - = mode - fromCV c = error $ "SymVal.RoundingMode: Unexpected non-rounding mode value: " ++ show c + literal = SBV . svRoundingMode + fromCV c = + case cvAsRoundingMode c of + Just mode -> mode + Nothing -> error $ "SymVal.RoundingMode: Unexpected non-rounding mode value: " ++ show c -- | Symbolic variant of 'RoundNearestTiesToEven' sRoundNearestTiesToEven :: SRoundingMode 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 @@ -12,6 +12,7 @@ {-# LANGUAGE BangPatterns #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} +{-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -Wall -Werror #-} @@ -19,9 +20,12 @@ ( -- ** Basic constructors svTrue, svFalse, svBool - , svInteger, svFloat, svDouble, svFloatingPoint, svReal, svEnumFromThenTo, svString, svChar + , svInteger, svFloat, svDouble, svFloatingPoint, svRoundingMode + , svReal, svEnumFromThenTo, svString, svChar -- ** Basic destructors - , svAsBool, svAsInteger, svNumerator, svDenominator + , svAsBool, svAsInteger + , svAsFloat, svAsDouble, svAsFP, svAsRoundingMode, cvAsRoundingMode + , svNumerator, svDenominator -- ** Basic operations , svPlus, svTimes, svMinus, svUNeg, svAbs, svSignum , svDivide, svQuot, svRem, svQuotRem, svDivides @@ -34,6 +38,13 @@ , svSelect , svSign, svUnsign, svSetBit, svWordFromBE, svWordFromLE , svExp, svFromIntegral + , svFPNaN, svFPInf, svFPZero + , svFPFromIntegerLit, svFPFromRationalLit + , svFPIsZero, svFPIsInfinite, svFPIsNegative, svFPIsPositive + , svFPIsNaN, svFPIsNormal, svFPIsSubnormal + , svFPAdd, svFPSub, svFPMul, svFPDiv, svFPRem, svFPMin, svFPMax + , svFPFMA, svFPAbs, svFPNeg, svFPRoundToIntegral, svFPSqrt + , svCastToFP, svCastFromFP -- ** Overflows , svMkOverflow1, svMkOverflow2 -- ** Derived operations @@ -43,6 +54,7 @@ , svBarrelRotateLeft, svBarrelRotateRight , svBlastLE, svBlastBE , svAddConstant, svIncrement, svDecrement + , svSWord32AsFloat, svSWord64AsDouble, svSWordAsFloatingPoint , svFloatAsSWord32, svDoubleAsSWord64, svFloatingPointAsSWord -- Utils , mkSymOp @@ -63,7 +75,7 @@ import Data.Ratio -import Data.SBV.Utils.Numeric (fpIsEqualObjectH, floatToWord, doubleToWord) +import Data.SBV.Utils.Numeric (RoundingMode(..), {-fp2fp,-} fpIsEqualObjectH, fpIsNormalizedH, fpMaxH, fpMinH, fpRemH, fpRoundToIntegralH, floatToWord, doubleToWord, wordToFloat, wordToDouble) import LibBF @@ -99,6 +111,10 @@ svFloatingPoint f@(FP eb sb _) = SVal k (Left $! CV k (CFP f)) where k = KFP eb sb +-- | Convert from a rounding mode +svRoundingMode :: RoundingMode -> SVal +svRoundingMode s = SVal kRoundingMode $ Left $ CV kRoundingMode $ CADT (show s, []) + -- | Convert from a String svString :: String -> SVal svString s = SVal KString (Left $! CV KString (CString s)) @@ -124,6 +140,35 @@ svAsInteger (SVal _ (Left (CV _ (CInteger n)))) = Just n svAsInteger _ = Nothing +-- | Extract a float from a concrete value. +svAsFloat :: SVal -> Maybe Float +svAsFloat (SVal _ (Left (CV _ (CFloat f)))) = Just f +svAsFloat _ = Nothing + +-- | Extract a double from a concrete value. +svAsDouble :: SVal -> Maybe Double +svAsDouble (SVal _ (Left (CV _ (CDouble d)))) = Just d +svAsDouble _ = Nothing + +-- | Extract an t'FP' from a concrete value. +svAsFP :: SVal -> Maybe FP +svAsFP (SVal _ (Left (CV _ (CFP fp)))) = Just fp +svAsFP _ = Nothing + +-- | Extract a rounding mode from an t'SVal'. +svAsRoundingMode :: SVal -> Maybe RoundingMode +svAsRoundingMode (SVal _ (Left cv)) = cvAsRoundingMode cv +svAsRoundingMode _ = Nothing + +-- | Extract a rounding mode from a t'CV'. +cvAsRoundingMode :: CV -> Maybe RoundingMode +cvAsRoundingMode (CV k (CADT (s, []))) + | k == kRoundingMode + , mbMode <- s `lookup` [(show m, m) | m <- [minBound .. maxBound :: RoundingMode]] + = mbMode +cvAsRoundingMode _ + = Nothing + -- | Grab the numerator of an SReal, if available svNumerator :: SVal -> Maybe Integer svNumerator (SVal KReal (Left (CV KReal (CAlgReal (AlgRational True r))))) = Just $ numerator r @@ -1011,6 +1056,260 @@ y st = do xsw <- svToSV st x newExpr st kTo (SBVApp (KindCast kFrom kTo) [xsw]) +-- | Create a NaN floating-point value of the given kind. +svFPNaN :: Kind -> SVal +svFPNaN k = SVal k $ Left $ fpConstCV k nan nan fpNaN + where + nan :: forall a. Floating a => a + nan = 0/0 + +-- | Create an infinite floating-point value of the given kind. If the 'Bool' +-- argument is 'True', then use negative infinity; otherwise, use positive +-- infinity. +svFPInf :: Kind -> Bool -> SVal +svFPInf k neg = SVal k $ Left $ fpConstCV k signedInfinity signedInfinity (fpInf neg) + where + infinity :: forall a. Floating a => a + infinity = 1/0 + + signedInfinity :: forall a. Floating a => a + signedInfinity = if neg then -infinity else infinity + +-- | Create a NaN infinity value of the given kind. If the 'Bool' argument is +-- 'True', then use negative infinity; otherwise, use positive infinity. +svFPZero :: Kind -> Bool -> SVal +svFPZero k neg = SVal k $ Left $ fpConstCV k signedZero signedZero (fpZero neg) + where + signedZero :: forall a. Num a => a + signedZero = if neg then -0 else 0 + +-- | Create a float-point value of the given kind from an 'Integer' literal. +svFPFromIntegerLit :: Kind -> Integer -> SVal +svFPFromIntegerLit k r = SVal k $ Left $ fpConstCV k (fromInteger r) (fromInteger r) (\eb sb -> fpFromInteger eb sb r) + +-- | Create a float-point value of the given kind from a 'Rational' literal. +svFPFromRationalLit :: Kind -> Rational -> SVal +svFPFromRationalLit k r = SVal k $ Left $ fpConstCV k (fromRational r) (fromRational r) (\eb sb -> fpFromRational eb sb r) + +-- | Is the given floating-point value a zero value? +svFPIsZero :: SVal -> SVal +svFPIsZero = liftFPPred (mkSymOp1 (IEEEFP FP_IsZero)) isZero isZero fpIsZero + where + isZero :: forall a. RealFloat a => a -> Bool + isZero x = x == 0 + +-- | Is the given floating-point value infinite? +svFPIsInfinite :: SVal -> SVal +svFPIsInfinite = liftFPPred (mkSymOp1 (IEEEFP FP_IsInfinite)) isInfinite isInfinite fpIsInf + +-- | Is the given floating-point value negative? +svFPIsNegative :: SVal -> SVal +svFPIsNegative = liftFPPred (mkSymOp1 (IEEEFP FP_IsNegative)) isNegative isNegative fpIsNeg + where + isNegative :: forall a. RealFloat a => a -> Bool + isNegative x = x < 0 || isNegativeZero x + +-- | Is the given floating-point value positive? +svFPIsPositive :: SVal -> SVal +svFPIsPositive = liftFPPred (mkSymOp1 (IEEEFP FP_IsPositive)) isPositive isPositive fpIsPos + where + isPositive :: forall a. RealFloat a => a -> Bool + isPositive x = x >= 0 && not (isNegativeZero x) + +-- | Is the given floating-point value a NaN value? +svFPIsNaN :: SVal -> SVal +svFPIsNaN = liftFPPred (mkSymOp1 (IEEEFP FP_IsNaN)) isNaN isNaN fpIsNaN + +-- | Is the given floating-point value \"normal\"? That is, is the value not +-- zero, infinite, NaN, or subnormal? +svFPIsNormal :: SVal -> SVal +svFPIsNormal = liftFPPred (mkSymOp1 (IEEEFP FP_IsNormal)) fpIsNormalizedH fpIsNormalizedH fpIsNormal + +-- | Is the given floating-point value subnormal (i.e., denormalized)? +svFPIsSubnormal :: SVal -> SVal +svFPIsSubnormal = liftFPPred (mkSymOp1 (IEEEFP FP_IsSubnormal)) isDenormalized isDenormalized fpIsSubnormal + +-- | Floating-point addition. +svFPAdd :: SVal -- ^ Rounding mode + -> SVal -> SVal -> SVal +svFPAdd = liftFPSymRM2 "add" (mkSymOp3 (IEEEFP FP_Add)) (+) (+) fpAdd + +-- | Floating-point subtraction. +svFPSub :: SVal -- ^ Rounding mode + -> SVal -> SVal -> SVal +svFPSub = liftFPSymRM2 "sub" (mkSymOp3 (IEEEFP FP_Sub)) (-) (-) fpSub + +-- | Floating-point multiplication. +svFPMul :: SVal -- ^ Rounding mode + -> SVal -> SVal -> SVal +svFPMul = liftFPSymRM2 "mul" (mkSymOp3 (IEEEFP FP_Mul)) (*) (*) fpMul + +-- | Floating-point division. +svFPDiv :: SVal -- ^ Rounding mode + -> SVal -> SVal -> SVal +svFPDiv = liftFPSymRM2 "div" (mkSymOp3 (IEEEFP FP_Div)) (/) (/) fpDiv + +-- | Floating-point remainder. +svFPRem :: SVal -> SVal -> SVal +svFPRem = liftFPSym2 "rem" (mkSymOp (IEEEFP FP_Rem)) fpRemH fpRemH (fpRem RoundNearestTiesToEven) + +-- | Floating-point minimum. +svFPMin :: SVal -> SVal -> SVal +svFPMin = liftFPSym2 "min" (mkSymOp (IEEEFP FP_Min)) fpMinH fpMinH fpMin + +-- | Floating-point maximum. +svFPMax :: SVal -> SVal -> SVal +svFPMax = liftFPSym2 "max" (mkSymOp (IEEEFP FP_Max)) fpMaxH fpMaxH fpMax + +-- | Floating-point fused-multipy-add (FMA). + +-- Note that this operation is defined somewhat unusually because Haskell lacks +-- a native FMA operation to use for concrete evaluation of 'Float's and +-- 'Double's. See https://github.com/LeventErkok/sbv/issues/777 for more +-- discussion. As such, concrete FMA evaluation is only supported for t'FP' +-- values. +svFPFMA :: SVal -- ^ Rounding mode + -> SVal -> SVal -> SVal -> SVal +svFPFMA (svAsRoundingMode -> Just rm) + (SVal k (Left (cvVal -> CFP a))) + (SVal _ (Left (cvVal -> CFP b))) + (SVal _ (Left (cvVal -> CFP c))) = + SVal k $ Left $ CV k $ CFP $ fpFMA rm a b c +svFPFMA rm a@(SVal k _) b c = SVal k $ Right $ cache ca + where ca st = do svrm <- svToSV st rm + sva <- svToSV st a + svb <- svToSV st b + svc <- svToSV st c + newExpr st k (SBVApp (IEEEFP FP_FMA) [svrm, sva, svb, svc]) + +-- | Floating-point absolute value. +svFPAbs :: SVal -> SVal +svFPAbs = liftFPSym1 "abs" (mkSymOp1 (IEEEFP FP_Abs)) abs abs fpAbs + +-- | Floating-point negation. +svFPNeg :: SVal -> SVal +svFPNeg = liftFPSym1 "negate" (mkSymOp1 (IEEEFP FP_Neg)) negate negate fpNeg + +-- | Round the given floating-point value to the nearest integer (represented +-- as a float with a zero decimal component) using the given rounding mode. +svFPRoundToIntegral :: SVal -- ^ Rounding mode + -> SVal -> SVal +svFPRoundToIntegral = liftFPSymRM1 "roundToIntegral" (mkSymOp (IEEEFP FP_RoundToIntegral)) fpRoundToIntegralH fpRoundToIntegralH fpRoundInt + +-- | Floating-point square root. +svFPSqrt :: SVal -- ^ Rounding mode + -> SVal -> SVal +svFPSqrt = liftFPSymRM1 "sqrt" (mkSymOp (IEEEFP FP_Sqrt)) sqrt sqrt fpSqrt + +-- | Cast an t'FP' value to a t'CV' of the given floating-point 'Kind' using the +-- given 'RoundingMode'. This will error if given a non-floating-point 'Kind'. +cvCastFromFP :: Kind -> RoundingMode -> FP -> CV +cvCastFromFP kindTo rm fp = + fpConstCV + kindTo + (fpToFloat rm (fpRoundFloat 8 24 rm fp)) + (fpToDouble rm (fpRoundFloat 11 53 rm fp)) + (\eb sb -> fpRoundFloat eb sb rm fp) + +-- | Cast a 'Rational' value to a t'CV' of the given floating-point 'Kind'. This +-- will error if given a non-floating-point 'Kind'. +cvCastFromRational :: Kind -> Rational -> CV +cvCastFromRational kindTo r = + fpConstCV + kindTo + (fromRational r) + (fromRational r) + (\eb sb -> fpFromRational eb sb r) + +-- | Convert a 'CVal' to an t'FP' value of the appropriate size. This will error +-- if the 'CVal' is not a floating-point value. +cvalToFP :: CVal -> FP +cvalToFP (CFloat f) = fpFromFloat 8 24 f +cvalToFP (CDouble d) = fpFromDouble 11 53 d +cvalToFP (CFP fp) = fp +cvalToFP _ = error "cvalToFP: non-float value" + +-- | Convert a value to a floating-point value. The type being converted from +-- must be one of 'KFloat', 'KDouble', 'KFP', 'KBounded', 'KUnbounded', or +-- 'KReal'. +-- +-- Note that converting from a 'KBounded' value returns a float with the same +-- numeric value as the input bitvector. For a conversion that returns a float +-- with the same bit pattern as the input bitvector, see 'svSWord32AsFloat', +-- 'svSWord64AsDouble', and 'svSWordAsFloatingPoint'. +svCastToFP :: Kind -- ^ The kind to cast to. Must be a floating-point kind. + -> SVal -- ^ Rounding mode + -> SVal -- ^ The value to be casted. + -> SVal +svCastToFP kindTo (svAsRoundingMode -> Just rm) x@(SVal kindFrom (Left (CV _ x'))) + | kindFrom == kindTo + = x + + | KFloat {} <- kindFrom + = fpCastFromFloat + | KDouble {} <- kindFrom + = fpCastFromFloat + | KFP {} <- kindFrom + = fpCastFromFloat + + | RoundNearestTiesToEven <- rm + , KBounded {} <- kindFrom + , CInteger w <- x' + = fpCastFromIntegral w + | RoundNearestTiesToEven <- rm + , KUnbounded {} <- kindFrom + , CInteger i <- x' + = fpCastFromIntegral i + + | RoundNearestTiesToEven <- rm + , CAlgReal r <- x' + , isExactRational r + = SVal kindTo $ Left $ cvCastFromRational kindTo $ toRational r + where fpCastFromFloat :: SVal + fpCastFromFloat = SVal kindTo $ Left $ cvCastFromFP kindTo rm $ cvalToFP x' + + fpCastFromIntegral :: forall a. Integral a => a -> SVal + fpCastFromIntegral = + SVal kindTo . Left . cvCastFromRational kindTo . fromIntegral +svCastToFP kindTo rm x@(SVal kindFrom _) + = SVal kindTo $ Right $ cache y + where y st = do svrm <- svToSV st rm + svx <- svToSV st x + mkSymOp (IEEEFP (FP_Cast kindFrom kindTo svrm)) st kindTo svrm svx + +-- | Convert a floating-point value to a value of a different type. The type to +-- convert to must be one of 'KFloat', 'KDouble', 'KFP', 'KBounded', +-- 'KUnbounded', or 'KReal'. +-- +-- Note that converting to 'KBounded' returns a bitvector with the same numeric +-- value as the input float (appropriately rounded). For a lossless conversion +-- that returns a bitvector with the same bit pattern as the input float, see +-- 'svFloatAsSWord32', 'svDoubleAsSWord64', and 'svFloatingPointAsSWord'. +svCastFromFP :: Kind -- ^ The kind to cast to. + -> SVal -- ^ Rounding mode + -> SVal -- ^ The value to be casted. Must be a floating-point value. + -> SVal +svCastFromFP kindTo (svAsRoundingMode -> Just rm) x@(SVal kindFrom (Left (CV _ x'))) + | kindFrom == kindTo + = x + + | KFloat {} <- kindTo + = fpCastToFloat + | KDouble {} <- kindTo + = fpCastToFloat + | KFP {} <- kindTo + = fpCastToFloat + -- No constant-folding for KBounded, KUnbounded, or KReal, as each of these + -- conversions are partial. Rather than painstakingly check which inputs are + -- valid, we simply defer to the underlying SMT-LIB operations. + where fpCastToFloat :: SVal + fpCastToFloat = SVal kindTo $ Left $ cvCastFromFP kindTo rm $ cvalToFP x' +svCastFromFP kindTo rm x@(SVal kindFrom _) + = SVal kindTo $ Right $ cache y + where y st = do svrm <- svToSV st rm + svx <- svToSV st x + mkSymOp (IEEEFP (FP_Cast kindFrom kindTo svrm)) st kindTo svrm svx + -------------------------------------------------------------------------------- -- Derived operations @@ -1367,6 +1666,102 @@ liftSym2 _ okCV opCR opCI opCF opCD opFP opRA (SVal k (Left a)) (SVal _ (Left b)) | and [f a b | f <- okCV] = SVal k . Left $! mapCV2 opCR opCI opCF opCD opFP opRA a b liftSym2 opS _ _ _ _ _ _ _ a@(SVal k _) b = SVal k $ Right $ liftSV2 opS k a b +-- | Lift a unary floating-point operation that can work over 'Float', +-- 'Double', and t'FP' values. +liftFPSym1 :: String + -> (State -> Kind -> SV -> IO SV) + -> (Float -> Float) + -> (Double -> Double) + -> (FP -> FP) + -> SVal -> SVal +liftFPSym1 o _ opCF opCD opFP (SVal k (Left a)) + = SVal k . Left $! mapCV (noRealUnary o) (noIntUnary o) opCF opCD opFP (noRatUnary o) a +liftFPSym1 _ opS _ _ _ a@(SVal k _) = SVal k $ Right $ cache c + where c st = do sva <- svToSV st a + opS st k sva + +-- | Like 'liftFPSym1', but with an explicit rounding mode. Note that concrete +-- evaluation of 'Float's or 'Double's is only supported when the +-- 'RoundNearestTiesToEven' rounding mode is used (see the Haddocks for +-- 'floatDoubleRneCheck'). +liftFPSymRM1 :: String + -> (State -> Kind -> SV -> SV -> IO SV) + -> (Float -> Float) + -> (Double -> Double) + -> (RoundingMode -> FP -> FP) + -> SVal -> SVal -> SVal +liftFPSymRM1 o _ opCF opCD opFP rm (SVal k (Left a)) + | Just rm'@RoundNearestTiesToEven <- svAsRoundingMode rm + , floatDoubleRneCheck rm' a + = SVal k . Left $! mapCV (noRealUnary o) (noIntUnary o) opCF opCD (opFP rm') (noRatUnary o) a +liftFPSymRM1 _ opS _ _ _ rm a@(SVal k _) = SVal k $ Right $ cache c + where c st = do svrm <- svToSV st rm + sva <- svToSV st a + opS st k svrm sva + +-- | Lift a binary floating-point operation that can work over 'Float', +-- 'Double', and t'FP' values. +liftFPSym2 :: String + -> (State -> Kind -> SV -> SV -> IO SV) + -> (Float -> Float -> Float) + -> (Double -> Double -> Double) + -> (FP -> FP -> FP) + -> SVal -> SVal -> SVal +liftFPSym2 o _ opCF opCD opFP (SVal k (Left a)) (SVal _ (Left b)) + = SVal k . Left $! mapCV2 (noReal o) (noInt o) opCF opCD opFP (noRat o) a b +liftFPSym2 _ opS _ _ _ a@(SVal k _) b = SVal k $ Right $ cache c + where c st = do sva <- svToSV st a + svb <- svToSV st b + opS st k sva svb + +-- | Like 'liftFPSym2', but with an explicit rounding mode. Note that concrete +-- evaluation of 'Float's or 'Double's is only supported when the +-- 'RoundNearestTiesToEven' rounding mode is used (see the Haddocks for +-- 'floatDoubleRneCheck'). +liftFPSymRM2 :: String + -> (State -> Kind -> SV -> SV -> SV -> IO SV) + -> (Float -> Float -> Float) + -> (Double -> Double -> Double) + -> (RoundingMode -> FP -> FP -> FP) + -> SVal -> SVal -> SVal -> SVal +liftFPSymRM2 o _ opCF opCD opFP rm (SVal k (Left a)) (SVal _ (Left b)) + | Just rm'@RoundNearestTiesToEven <- svAsRoundingMode rm + , floatDoubleRneCheck rm' a + = SVal k . Left $! mapCV2 (noReal o) (noInt o) opCF opCD (opFP rm') (noRat o) a b +liftFPSymRM2 _ opS _ _ _ rm a@(SVal k _) b = SVal k $ Right $ cache c + where c st = do svrm <- svToSV st rm + sva <- svToSV st a + svb <- svToSV st b + opS st k svrm sva svb + +-- | Lift a unary floating-point predicate that can work over 'Float', +-- 'Double', and t'FP' values. +liftFPPred :: (State -> Kind -> SV -> IO SV) + -> (Float -> Bool) + -> (Double -> Bool) + -> (FP -> Bool) + -> SVal -> SVal +liftFPPred _ opCF opCD opFP (SVal k (Left a)) = + case cvVal a of + CFloat f -> svBool $ opCF f + CDouble d -> svBool $ opCD d + CFP fp -> svBool $ opFP fp + + CAlgReal {} -> unexpected + CInteger {} -> unexpected + CRational {} -> unexpected + CChar {} -> unexpected + CString {} -> unexpected + CList {} -> unexpected + CSet {} -> unexpected + CADT {} -> unexpected + CTuple {} -> unexpected + CArray {} -> unexpected + where unexpected = error $ "Data.SBV.liftFPPred: Unexpected kind: " ++ show k +liftFPPred opS _ _ _ a = SVal KBool $ Right $ cache c + where c st = do sva <- svToSV st a + opS st KBool sva + -- | Create a symbolic two argument operation; with shortcut optimizations mkSymOpSC :: (SV -> SV -> Maybe SV) -> Op -> State -> Kind -> SV -> SV -> IO SV mkSymOpSC shortCut op st k a b = maybe (newExpr st k (SBVApp op [a, b])) pure (shortCut a b) @@ -1381,6 +1776,9 @@ mkSymOp1 :: Op -> State -> Kind -> SV -> IO SV mkSymOp1 = mkSymOp1SC (const Nothing) +mkSymOp3 :: Op -> State -> Kind -> SV -> SV -> SV -> IO SV +mkSymOp3 op st k a b c = newExpr st k (SBVApp op [a, b, c]) + -- | Predicate to check if a value is concrete isConcrete :: SVal -> Bool isConcrete (SVal _ Left{}) = True @@ -1443,6 +1841,26 @@ rationalSBVCheck (SVal KReal (Left a)) (SVal KReal (Left b)) = rationalCheck a b rationalSBVCheck _ _ = True +-- | Predicate to check if a concrete 'Float' or 'Double' value uses the +-- 'RoundNearestTiesToEven' rounding mode. This is necessary because we assume +-- this rounding mode when concretely evaluating 'Float's and 'Double's, so +-- concrete evaluation is not supported for other rounding modes. +-- +-- Note that this check skips concrete t'FP' values, which support concrete +-- evaluation with any rounding mode. +floatDoubleRneCheck :: RoundingMode -> CV -> Bool +floatDoubleRneCheck rm cv = + case cvKind cv of + KFloat -> rmIsRne + KDouble -> rmIsRne + _ -> True + where + rmIsRne | RoundNearestTiesToEven <- rm = True + | otherwise = False + +noInt :: String -> Integer -> Integer -> a +noInt o a b = error $ "SBV.Integer." ++ o ++ ": Unexpected arguments: " ++ show (a, b) + noReal :: String -> AlgReal -> AlgReal -> a noReal o a b = error $ "SBV.AlgReal." ++ o ++ ": Unexpected arguments: " ++ show (a, b) @@ -1458,6 +1876,9 @@ noRat:: String -> Rational -> Rational -> a noRat o a b = error $ "SBV.Rational." ++ o ++ ": Unexpected arguments: " ++ show (a, b) +noIntUnary :: String -> Integer -> a +noIntUnary o a = error $ "SBV.Integer." ++ o ++ ": Unexpected argument: " ++ show a + noRealUnary :: String -> AlgReal -> a noRealUnary o a = error $ "SBV.AlgReal." ++ o ++ ": Unexpected argument: " ++ show a @@ -1507,6 +1928,59 @@ walk ((lti, eqi) : rest) = lti `svOr` (eqi `svAnd` walk rest) svToSV st $ walk $ zipWith chkElt [1..] ks + +-- | Convert an 'Data.SBV.SWord32' to an 'Data.SBV.SFloat', preserving the +-- bit-correspondence. Note that since the representation for @NaN@s are not +-- unique, there are multiple word values for which this function will return a +-- single, distinguished @NaN@ value. +svSWord32AsFloat :: SVal -> SVal +svSWord32AsFloat w@(SVal kindFrom x) + | KBounded _ 32 <- kindFrom + = case x of + Left (CV _ (CInteger w')) + -> SVal kindTo $ Left $ CV kindTo $ CFloat $ wordToFloat $ fromInteger w' + _ -> SVal kindTo $ Right $ cache y + | otherwise + = error $ "svSWord32AsFloat: not a 32-bit word type: " ++ show kindFrom + where kindTo = KFloat + y st = do svw <- svToSV st w + mkSymOp1 (IEEEFP (FP_Reinterpret kindFrom kindTo)) st kindTo svw + +-- | Convert an 'Data.SBV.SWord64' to an 'Data.SBV.SDouble', preserving the +-- bit-correspondence. Note that since the representation for @NaN@s are not +-- unique, there are multiple word values for which this function will return a +-- single, distinguished @NaN@ value. +svSWord64AsDouble :: SVal -> SVal +svSWord64AsDouble w@(SVal kindFrom x) + | KBounded _ 64 <- kindFrom + = case x of + Left (CV _ (CInteger w')) + -> SVal kindTo $ Left $ CV kindTo $ CDouble $ wordToDouble $ fromInteger w' + _ -> SVal kindTo $ Right $ cache y + | otherwise + = error $ "svSWord64AsDouble: not a 64-bit word type: " ++ show kindFrom + where kindTo = KDouble + y st = do svw <- svToSV st w + mkSymOp1 (IEEEFP (FP_Reinterpret kindFrom kindTo)) st kindTo svw + +-- | Convert a word to a float (using the given exponent and significand sizes) +-- containing the word's corresponding bit pattern. Note that since the +-- representation for @NaN@s are not unique, there are multiple word values for +-- which this function will return a single, distinguished @NaN@ value. +svSWordAsFloatingPoint :: Int -- ^ Exponent size + -> Int -- ^ Significand size + -> SVal -> SVal +svSWordAsFloatingPoint eb sb w@(SVal kindFrom x) + | KBounded _ _ <- kindFrom + = case x of + Left (CV _ (CInteger w')) + -> SVal kindTo $ Left $ CV kindTo $ CFP $ fpFromBits eb sb $ fromInteger w' + _ -> SVal kindTo $ Right $ cache y + | otherwise + = error $ "svSWordAsFloatingPoint: non-word type: " ++ show kindFrom + where kindTo = KFP eb sb + y st = do svw <- svToSV st w + mkSymOp1 (IEEEFP (FP_Reinterpret kindFrom kindTo)) st kindTo svw -- | Convert an 'Data.SBV.SFloat' to an 'Data.SBV.SWord32', preserving the bit-correspondence. Note that since the -- representation for @NaN@s are not unique, this function will return a symbolic value when given a diff --git a/Data/SBV/Core/SizedFloats.hs b/Data/SBV/Core/SizedFloats.hs --- a/Data/SBV/Core/SizedFloats.hs +++ b/Data/SBV/Core/SizedFloats.hs @@ -23,13 +23,22 @@ FloatingPoint(..), FP(..), FPHalf, FPBFloat, FPSingle, FPDouble, FPQuad -- * Constructing values - , fpFromRawRep, fpFromBigFloat, fpNaN, fpInf, fpZero + , fpFromRawRep, fpFromBigFloat, fpFromBits, fpNaN, fpInf, fpZero -- * Operations - , fpFromInteger, fpFromRational, fpFromFloat, fpFromDouble, fpEncodeFloat + , fpFromInteger, fpFromRational, fpFromFloat, fpFromDouble + , fpToFloat, fpToDouble + , fpEncodeFloat + , fpIsFinite, fpIsInf, fpIsZero, fpIsNaN + , fpIsNormal, fpIsSubnormal, fpIsNeg, fpIsPos + , fpNeg, fpAbs, fpSignum + , fpAdd, fpSub, fpMul, fpDiv, fpPow, fpRem, fpSqrt, fpFMA + , fpRoundFloat, fpRoundInt + , fpMax, fpMin -- * Internal operations , arbFPIsEqualObjectH, arbFPCompareObjectH, fprToSMTLib2, mkBFOpts, bfToString, bfRemoveRedundantExp + , roundingModeToRoundMode ) where import Data.Char (intToDigit) @@ -42,7 +51,7 @@ import Numeric import Data.SBV.Core.Kind -import Data.SBV.Utils.Numeric (floatToWord) +import Data.SBV.Utils.Numeric (RoundingMode(..), floatToWord, fp2fp) import LibBF (BigFloat, BFOpts, RoundMode, Status, BFRep(..), BFNum(..), bfToRep, Sign(Neg)) import qualified LibBF as BF @@ -207,11 +216,15 @@ fpFromBigFloat :: Int -> Int -> BigFloat -> FP fpFromBigFloat eb sb r = FP eb sb $ fst $ BF.bfRoundFloat (mkBFOpts eb sb BF.NearEven) r +-- | Convert an integer to a big-float, preserving the bit-correspondence. +fpFromBits :: Int -> Int -> Integer -> FP +fpFromBits eb sb val = FP eb sb $ BF.bfFromBits (mkBFOpts eb sb BF.NearEven) val + -- | Convert from an sign/exponent/mantissa representation to a float. The values are the integers -- representing the bit-patterns of these values, i.e., the raw representation. We assume that these -- integers fit into the ranges given, i.e., no overflow checking is done here. fpFromRawRep :: Bool -> (Integer, Int) -> (Integer, Int) -> FP -fpFromRawRep sign (e, eb) (s, sb) = FP eb sb $ BF.bfFromBits (mkBFOpts eb sb BF.NearEven) val +fpFromRawRep sign (e, eb) (s, sb) = fpFromBits eb sb val where es, val :: Integer es = (e `shiftL` (sb - 1)) .|. s val | sign = (1 `shiftL` (eb + sb - 1)) .|. es @@ -293,23 +306,23 @@ -- | Num instance for big-floats instance Num FP where - (+) = lift2 BF.bfAdd - (-) = lift2 BF.bfSub - (*) = lift2 BF.bfMul - abs = lift1 BF.bfAbs - signum = lift1 bfSignum + (+) = fpAdd RoundNearestTiesToEven + (-) = fpSub RoundNearestTiesToEven + (*) = fpMul RoundNearestTiesToEven + abs = fpAbs + signum = fpSignum fromInteger i = error $ "FP.fromInteger: Not supported for arbitrary floats. Use fpFromInteger instead, specifying the precision. Called on: " ++ show i - negate = lift1 BF.bfNeg + negate = fpNeg -- | Fractional instance for big-floats instance Fractional FP where fromRational = error "FP.fromRational: Not supported for arbitrary floats. Use fpFromRational instead, specifying the precision" - (/) = lift2 BF.bfDiv + (/) = fpDiv RoundNearestTiesToEven -- | Floating instance for big-floats instance Floating FP where - sqrt (FP eb sb a) = FP eb sb $ fst $ BF.bfSqrt (mkBFOpts eb sb BF.NearEven) a - FP eb sb a ** FP _ _ b = FP eb sb $ fst $ BF.bfPow (mkBFOpts eb sb BF.NearEven) a b + sqrt = fpSqrt RoundNearestTiesToEven + (**) = fpPow RoundNearestTiesToEven pi = unsupported "Floating.FP.pi" exp = unsupported "Floating.FP.exp" @@ -335,11 +348,11 @@ where v :: Integer v = 2 ^ ((fromIntegral eb :: Integer) - 1) - isNaN (FP _ _ r) = BF.bfIsNaN r - isInfinite (FP _ _ r) = BF.bfIsInf r - isDenormalized (FP eb sb r) = BF.bfIsSubnormal (mkBFOpts eb sb BF.NearEven) r - isNegativeZero (FP _ _ r) = BF.bfIsZero r && BF.bfIsNeg r - isIEEE _ = True + isNaN = fpIsNaN + isInfinite = fpIsInf + isDenormalized = fpIsSubnormal + isNegativeZero f = fpIsZero f && fpIsNeg f + isIEEE _ = True decodeFloat i@(FP _ _ r) = case BF.bfToRep r of BF.BFNaN -> decodeFloat (0/0 :: Double) @@ -360,6 +373,123 @@ where n' :: Integer n' = (2 :: Integer) ^ abs (fromIntegral n :: Integer) +-- | Is a big-float finite? +fpIsFinite :: FP -> Bool +fpIsFinite (FP _ _ r) = BF.bfIsFinite r + +-- | Is a big-float infinite? +fpIsInf :: FP -> Bool +fpIsInf (FP _ _ r) = BF.bfIsInf r + +-- | Is a big-float a zero value? +fpIsZero :: FP -> Bool +fpIsZero (FP _ _ r) = BF.bfIsZero r + +-- | Is a big-float a NaN value? +fpIsNaN :: FP -> Bool +fpIsNaN (FP _ _ r) = BF.bfIsNaN r + +-- | Is a big-float \"normal\"? That is, is the value not zero, infinite, NaN, +-- or subnormal? +fpIsNormal :: FP -> Bool +fpIsNormal (FP eb sb r) = BF.bfIsNormal (mkBFOpts eb sb BF.NearEven) r + +-- | Is a big-float subnormal (i.e., denormalized)? +fpIsSubnormal :: FP -> Bool +fpIsSubnormal (FP eb sb r) = BF.bfIsSubnormal (mkBFOpts eb sb BF.NearEven) r + +-- | Is a big-float negative? +fpIsNeg :: FP -> Bool +fpIsNeg (FP _ _ r) = BF.bfIsNeg r + +-- | Is a big-float positive? +fpIsPos :: FP -> Bool +fpIsPos (FP _ _ r) = BF.bfIsPos r + +-- | Big-float negation. +fpNeg :: FP -> FP +fpNeg = lift1 BF.bfNeg + +-- | Big-float absolute value. +fpAbs :: FP -> FP +fpAbs = lift1 BF.bfAbs + +-- | Big-float signum. +fpSignum :: FP -> FP +fpSignum = lift1 bfSignum + +-- | Big-float addition. +fpAdd :: RoundingMode -> FP -> FP -> FP +fpAdd = liftRM2 BF.bfAdd + +-- | Big-float subtraction. +fpSub :: RoundingMode -> FP -> FP -> FP +fpSub = liftRM2 BF.bfSub + +-- | Big-float multiplication. +fpMul :: RoundingMode -> FP -> FP -> FP +fpMul = liftRM2 BF.bfMul + +-- | Big-float division. +fpDiv :: RoundingMode -> FP -> FP -> FP +fpDiv = liftRM2 BF.bfDiv + +-- | Big-float exponentiation. +fpPow :: RoundingMode -> FP -> FP -> FP +fpPow = liftRM2 BF.bfPow + +-- | Big-float remainder. +fpRem :: RoundingMode -> FP -> FP -> FP +fpRem = liftRM2 BF.bfRem + +-- | Big-float square root. +fpSqrt :: RoundingMode -> FP -> FP +fpSqrt = liftRM1 BF.bfSqrt + +-- | Big-float fused-multiply-add (FMA). +fpFMA :: RoundingMode -> FP -> FP -> FP -> FP +fpFMA = liftRM3 BF.bfFMA + +-- | Round a big-float to a float of the given exponent and significand sizes +-- using the given rounding mode. +fpRoundFloat :: Int -> Int -> RoundingMode -> FP -> FP +fpRoundFloat eb sb rm (FP _ _ r) = FP eb sb $ fst $ BF.bfRoundFloat (mkBFOpts eb sb (roundingModeToRoundMode rm)) r + +-- | Round a big-float to the nearest integer (represented as a big-float with +-- a zero decimal component) using the given rounding mode. +fpRoundInt :: RoundingMode -> FP -> FP +fpRoundInt rm (FP eb sa a) = FP eb sa $ fst $ BF.bfRoundInt (roundingModeToRoundMode rm) a + +-- | SMTLib compliant definition for 'Data.SBV.fpMax'. This is very nearly +-- identical to 'Data.SBV.Utils.Numeric.fpMaxH', except that this uses +-- 'fpIsZero' instead of checking for equality against a @0@ literal. (The +-- latter is not supported for t'FP' values as t'FP' does not implement +-- 'fromInteger'.) +fpMax :: FP -> FP -> FP +fpMax x y + | isNaN x = y + | isNaN y = x + | (isN0 x && isP0 y) || (isN0 y && isP0 x) = error "fpMax: Called with alternating-sign 0's. Not supported" + | x > y = x + | True = y + where isN0 = isNegativeZero + isP0 a = fpIsZero a && not (isN0 a) + +-- | SMTLib compliant definition for 'Data.SBV.fpMin'. This is very nearly +-- identical to 'Data.SBV.Utils.Numeric.fpMinH', except that this uses +-- 'fpIsZero' instead of checking for equality against a @0@ literal. (The +-- latter is not supported for t'FP' values as t'FP' does not implement +-- 'fromInteger'.) +fpMin :: FP -> FP -> FP +fpMin x y + | isNaN x = y + | isNaN y = x + | (isN0 x && isP0 y) || (isN0 y && isP0 x) = error "fpMin: Called with alternating-sign 0's. Not supported" + | x < y = x + | True = y + where isN0 = isNegativeZero + isP0 a = fpIsZero a && not (isN0 a) + -- | Real instance for big-floats. Beware, not that well tested! instance Real FP where toRational i @@ -370,7 +500,7 @@ -- | Real-frac instance for big-floats. Beware, not that well tested! instance RealFrac FP where properFraction (FP eb sb r) = (getInt r', FP eb sb r - FP eb sb r') - where (r', _) = BF.bfRoundInt BF.ToNegInf r + where (r', _) = BF.bfRoundInt BF.ToZero r getInt x = case BF.bfToRep x of BF.BFNaN -> error $ "Data.SBV.FloatingPoint.properFraction: Failed to convert: " ++ show (r, x) BF.BFRep s n -> case n of @@ -450,10 +580,18 @@ lift1 :: (BigFloat -> BigFloat) -> FP -> FP lift1 f (FP eb sb a) = fpFromBigFloat eb sb $ f a --- Lift a binary operation. Here we don't call fpFromBigFloat, because the result is correctly rounded. -lift2 :: (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)) -> FP -> FP -> FP -lift2 f (FP eb sb a) (FP _ _ b) = FP eb sb $ fst $ f (mkBFOpts eb sb BF.NearEven) a b +-- | Lift a unary operation that returns a big-float and a status. +liftRM1 :: (BFOpts -> BigFloat -> (BigFloat, Status)) -> RoundingMode -> FP -> FP +liftRM1 f rm (FP eb sb a) = FP eb sb $ fst $ f (mkBFOpts eb sb (roundingModeToRoundMode rm)) a +-- | Lift a binary operation that returns a big-float and a status. +liftRM2 :: (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)) -> RoundingMode -> FP -> FP -> FP +liftRM2 f rm (FP eb sb a) (FP _ _ b) = FP eb sb $ fst $ f (mkBFOpts eb sb (roundingModeToRoundMode rm)) a b + +-- | Lift a trinary operation that returns a big-float and a status. +liftRM3 :: (BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status)) -> RoundingMode -> FP -> FP -> FP -> FP +liftRM3 f rm (FP eb sb a) (FP _ _ b) (FP _ _ c) = FP eb sb $ fst $ f (mkBFOpts eb sb (roundingModeToRoundMode rm)) a b c + -- | Convert from a IEEE float. fpFromFloat :: Int -> Int -> Float -> FP fpFromFloat 8 24 f = let fw = floatToWord f @@ -465,3 +603,19 @@ fpFromDouble :: Int -> Int -> Double -> FP fpFromDouble 11 53 d = FP 11 54 $ BF.bfFromDouble d fpFromDouble eb sb d = error $ "SBV.fpFromDouble: Unexpected input: " ++ show (eb, sb, d) + +-- | Convert to a IEEE float using the given rounding mode. +fpToFloat :: RoundingMode -> FP -> Float +fpToFloat rm (FP _ _ r) = fp2fp $ fst $ BF.bfToDouble (roundingModeToRoundMode rm) r + +-- | Convert to a IEEE double using the given rounding mode. +fpToDouble :: RoundingMode -> FP -> Double +fpToDouble rm (FP _ _ r) = fst $ BF.bfToDouble (roundingModeToRoundMode rm) r + +-- | Map SBV's rounding modes to LibBF's. +roundingModeToRoundMode :: RoundingMode -> RoundMode +roundingModeToRoundMode RoundNearestTiesToEven = BF.NearEven +roundingModeToRoundMode RoundNearestTiesToAway = BF.NearAway +roundingModeToRoundMode RoundTowardPositive = BF.ToPosInf +roundingModeToRoundMode RoundTowardNegative = BF.ToNegInf +roundingModeToRoundMode RoundTowardZero = BF.ToZero diff --git a/Data/SBV/Dynamic.hs b/Data/SBV/Dynamic.hs --- a/Data/SBV/Dynamic.hs +++ b/Data/SBV/Dynamic.hs @@ -32,7 +32,9 @@ -- *** Integer literals , svInteger, svAsInteger -- *** Float literals - , svFloat, svDouble, svFloatingPoint + , svFloat, svDouble, svFloatingPoint, svAsFloat, svAsDouble, svAsFP + -- *** Rounding mode literals + , svRoundingMode, svAsRoundingMode -- *** Algebraic reals (only from rationals) , svReal, svNumerator, svDenominator -- *** Symbolic equality @@ -63,6 +65,16 @@ , svBarrelRotateLeft, svBarrelRotateRight , svWordFromBE, svWordFromLE , svBlastLE, svBlastBE + -- *** Floating-point operations + , svFPNaN, svFPInf, svFPZero + , svFPFromIntegerLit, svFPFromRationalLit + , svFPIsZero, svFPIsInfinite, svFPIsNegative, svFPIsPositive + , svFPIsNaN, svFPIsNormal, svFPIsSubnormal + , svFPAdd, svFPSub, svFPMul, svFPDiv, svFPRem, svFPMin, svFPMax + , svFPFMA, svFPAbs, svFPNeg, svFPRoundToIntegral, svFPSqrt + , svCastToFP, svCastFromFP + , svSWord32AsFloat, svSWord64AsDouble, svSWordAsFloatingPoint + , svFloatAsSWord32, svDoubleAsSWord64, svFloatingPointAsSWord -- ** Conditionals: Mergeable values , svIte, svLazyIte, svSymbolicMerge -- * Uninterpreted sorts, constants, and functions diff --git a/Data/SBV/SCase.hs b/Data/SBV/SCase.hs --- a/Data/SBV/SCase.hs +++ b/Data/SBV/SCase.hs @@ -1042,7 +1042,7 @@ allCases <- concat <$> zipWithM (matchToPair scrut) (offsets ++ repeat Unknown) matches loc <- location checkWildcard "pCase" loc allCases - allPairs <- processProofCases scrut [] Nothing Map.empty [] allCases + allPairs <- processProofCases scrut [] Nothing [] allCases let casesName = mkName "cases" impliesName = mkName "==>" mkPair (g, r) = InfixE (Just g) (VarE impliesName) (Just r) @@ -1054,11 +1054,7 @@ cstrs <- getCstrs mbt typ checkWildcard "pCase" loc cases checkArities "pCase" typ cstrs cases - let allGrdVars :: Map.Map Name (Set Name) - allGrdVars = Map.fromListWith Set.union - [ (nm, maybe Set.empty freeVars mbG) - | CMatch _ nm _ mbG _ _ <- cases ] - allPairs <- processProofCases scrut cstrs mbt allGrdVars [] cases + allPairs <- processProofCases scrut cstrs mbt [] cases let casesName = mkName "cases" impliesName = mkName "==>" mkPair (g, r) = InfixE (Just g) (VarE impliesName) (Just r) @@ -1104,7 +1100,7 @@ allCases <- concat <$> zipWithM (matchToPair scrut) (offsets ++ repeat Unknown) matches loc <- location checkWildcard "pCase" loc allCases - allPairs <- processProofCases scrut [] Nothing Map.empty [] allCases + allPairs <- processProofCases scrut [] Nothing [] allCases let casesName = mkName "cases" impliesName = mkName "==>" mkPair (g, r) = InfixE (Just g) (VarE impliesName) (Just r) @@ -1168,13 +1164,7 @@ buildProofCase :: Exp -> String -> Maybe BuiltinType -> [Case] -> ExpQ buildProofCase scrut typ mbt cases = do cstrs <- getCstrs mbt typ - -- Collect guard variables for each constructor across all arms - -- (needed to suppress false "unused binding" warnings for guard-only variables) - let allGrdVars :: Map.Map Name (Set Name) - allGrdVars = Map.fromListWith Set.union - [ (nm, maybe Set.empty freeVars mbG) - | CMatch _ nm _ mbG _ _ <- cases ] - allPairs <- processProofCases scrut cstrs mbt allGrdVars [] cases + allPairs <- processProofCases scrut cstrs mbt [] cases let casesName = mkName "cases" impliesName = mkName "==>" mkPair (g, r) = InfixE (Just g) (VarE impliesName) (Just r) @@ -1192,77 +1182,88 @@ -- * fullGuard = the complete guard expression (used for wildcard De Morgan negation) -- * userGuardOnly = Just the user guard part (used for same-constructor negation), -- Nothing if unguarded (same-constructor arms don't negate unguarded matches) -processProofCases :: Exp -> [(Name, [Type])] -> Maybe BuiltinType -> Map.Map Name (Set Name) -> [(Maybe Name, Exp, Maybe Exp)] -> [Case] -> Q [(Exp, Exp)] -processProofCases _ _ _ _ _ [] = pure [] -processProofCases scrut cstrs mbt allGrdVars priorGuards (c:rest) = case c of - CWild _ mbG rhs -> do - -- Wildcard: negate the disjunction of ALL prior full guards (De Morgan) - let allGuards = [g | (_, g, _) <- priorGuards] - baseGuard = negateAllGuards allGuards - finalGuard = case mbG of - Nothing -> baseGuard - Just g -> sAndAll [baseGuard, g] - rest' <- processProofCases scrut cstrs mbt allGrdVars (priorGuards ++ [(Nothing, finalGuard, Nothing)]) rest - pure $ (finalGuard, rhs) : rest' +processProofCases :: Exp -> [(Name, [Type])] -> Maybe BuiltinType -> [(Maybe Name, Exp, Maybe Exp)] -> [Case] -> Q [(Exp, Exp)] +processProofCases scrut cstrs mbt priorGuards0 cases0 = go priorGuards0 cases0 + where + -- Aggregate, per constructor, the variables used in any guard or RHS across all arms with that constructor. + -- A pattern var used in *some* same-constructor arm but not in *this* arm's RHS is dropped from the + -- RHS bindings (the guard handles its own bindings via 'grdBindings'), avoiding false unused-binding + -- warnings. A pattern var truly unused everywhere is kept so GHC can flag the user oversight. + cstrUsedVars :: Map.Map Name (Set Name) + cstrUsedVars = Map.fromListWith Set.union + [ (nm, allUsed) | CMatch _ nm _ _ _ allUsed <- cases0 ] - CMatch _o nm mbp mbG rhs _allUsed -> do - let ts = case lookupBase nm cstrs of - Just t -> t - Nothing -> error $ "pCase: impossible: unknown constructor " ++ nameBase nm - pats = fromMaybe (map (const WildP) ts) mbp + go _ [] = pure [] + go priorGuards (c:rest) = case c of + CWild _ mbG rhs -> do + -- Wildcard: negate the disjunction of ALL prior full guards (De Morgan) + let allGuards = [g | (_, g, _) <- priorGuards] + baseGuard = negateAllGuards allGuards + finalGuard = case mbG of + Nothing -> baseGuard + Just g -> sAndAll [baseGuard, g] + rest' <- go (priorGuards ++ [(Nothing, finalGuard, Nothing)]) rest + pure $ (finalGuard, rhs) : rest' - -- Build let-bindings for pattern variables - args = [(i, mkAccessorFor mbt nm i scrut) | (i, _) <- zip [(1 :: Int) ..] ts] - bindings = [ ValD (VarP v) (NormalB acc) [] - | (i, acc) <- args, VarP v <- [pats !! (i - 1)] ] + CMatch _o nm mbp mbG rhs _allUsed -> do + let ts = case lookupBase nm cstrs of + Just t -> t + Nothing -> error $ "pCase: impossible: unknown constructor " ++ nameBase nm + pats = fromMaybe (map (const WildP) ts) mbp - testerGuard = mkTesterFor mbt nm scrut + -- Build let-bindings for pattern variables + args = [(i, mkAccessorFor mbt nm i scrut) | (i, _) <- zip [(1 :: Int) ..] ts] + bindings = [ ValD (VarP v) (NormalB acc) [] + | (i, acc) <- args, VarP v <- [pats !! (i - 1)] ] - -- For list cons patterns in pCase, add a destructuring equality: - -- scrut .=== head scrut .: tail scrut - -- Lists use SMT Seq (not declare-datatypes), so the solver doesn't automatically - -- know that xs = head xs .: tail xs from sNot (null xs). We must add an explicit - -- equality to give the solver this information, mirroring what 'split' does. - -- All other types (ADTs, Maybe, Either, Tuple) use declare-datatypes and get - -- these axioms for free. - -- NB. For nested list cons patterns, the same equality is added by 'flattenCons'. - destructEq - | Just BTList <- mbt, nameBase nm == ":" - = let hd = AppE (VarE (sbvName "Data.SBV.List" "head")) scrut - tl = AppE (VarE (sbvName "Data.SBV.List" "tail")) scrut - in [foldl1 AppE [VarE '(.===), scrut, InfixE (Just hd) (VarE '(.:)) (Just tl)]] - | True - = [] + testerGuard = mkTesterFor mbt nm scrut - -- Only negate prior USER guards for the SAME constructor (others are mutually exclusive) - sameUserGuards = [ ug | (Just cn, _, Just ug) <- priorGuards, sameBase cn nm ] - negPriors = map (AppE (VarE 'sNot)) sameUserGuards + -- For list cons patterns in pCase, add a destructuring equality: + -- scrut .=== head scrut .: tail scrut + -- Lists use SMT Seq (not declare-datatypes), so the solver doesn't automatically + -- know that xs = head xs .: tail xs from sNot (null xs). We must add an explicit + -- equality to give the solver this information, mirroring what 'split' does. + -- All other types (ADTs, Maybe, Either, Tuple) use declare-datatypes and get + -- these axioms for free. + -- NB. For nested list cons patterns, the same equality is added by 'flattenCons'. + destructEq + | Just BTList <- mbt, nameBase nm == ":" + = let hd = AppE (VarE (sbvName "Data.SBV.List" "head")) scrut + tl = AppE (VarE (sbvName "Data.SBV.List" "tail")) scrut + in [foldl1 AppE [VarE '(.===), scrut, InfixE (Just hd) (VarE '(.:)) (Just tl)]] + | True + = [] - -- Build the final guard (wrap user guard in bindings so pattern vars are in scope) - grdVars = maybe Set.empty freeVars mbG - grdBindings = filter (\case - ValD (VarP v) _ _ -> v `Set.member` grdVars - _ -> True) bindings - guardParts = [testerGuard] ++ destructEq ++ negPriors ++ maybe [] (pure . addLocals grdBindings) mbG - finalGuard = sAndAll guardParts + -- Only negate prior USER guards for the SAME constructor (others are mutually exclusive) + sameUserGuards = [ ug | (Just cn, _, Just ug) <- priorGuards, sameBase cn nm ] + negPriors = map (AppE (VarE 'sNot)) sameUserGuards - -- Wrap RHS with let-bindings; include all bindings except those - -- used in any guard of the same constructor but not in this RHS - -- (to avoid false "unused" warnings from GHC for guard-only variables) - cstrGrdVars = Map.findWithDefault Set.empty nm allGrdVars - rhsVars = freeVars rhs - rhs' = addLocals (filter (\case - ValD (VarP v) _ _ -> not (v `Set.member` cstrGrdVars) || v `Set.member` rhsVars - _ -> True) bindings) rhs + -- Build the final guard (wrap user guard in bindings so pattern vars are in scope) + grdVars = maybe Set.empty freeVars mbG + grdBindings = filter (\case + ValD (VarP v) _ _ -> v `Set.member` grdVars + _ -> True) bindings + guardParts = [testerGuard] ++ destructEq ++ negPriors ++ maybe [] (pure . addLocals grdBindings) mbG + finalGuard = sAndAll guardParts - -- Track: full guard for wildcard negation, user guard for same-constructor negation - userGuardOnly = case mbG of - Just g -> Just (addLocals grdBindings g) - Nothing -> Nothing - priorGuards' = priorGuards ++ [(Just nm, finalGuard, userGuardOnly)] + -- Wrap RHS with let-bindings. Keep a binding when the variable is used in this RHS, OR when + -- it isn't used in any same-constructor arm (so GHC can warn about a truly unused pattern var). + -- Drop it when used in some same-constructor arm but not here, to avoid spurious warnings. + cstrUsed = Map.findWithDefault Set.empty nm cstrUsedVars + rhsVars = freeVars rhs + rhs' = addLocals (filter (\case + ValD (VarP v) _ _ -> v `Set.member` rhsVars + || not (v `Set.member` cstrUsed) + _ -> True) bindings) rhs - rest' <- processProofCases scrut cstrs mbt allGrdVars priorGuards' rest - pure $ (finalGuard, rhs') : rest' + -- Track: full guard for wildcard negation, user guard for same-constructor negation + userGuardOnly = case mbG of + Just g -> Just (addLocals grdBindings g) + Nothing -> Nothing + priorGuards' = priorGuards ++ [(Just nm, finalGuard, userGuardOnly)] + + rest' <- go priorGuards' rest + pure $ (finalGuard, rhs') : rest' -- | Negate the disjunction of all given guards using De Morgan: sNot (g1 .|| g2 .|| ...) negateAllGuards :: [Exp] -> Exp 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 @@ -1210,7 +1210,7 @@ -- To go and back from Ints, we detour through reals cast KUnbounded (KFP eb sb) a = "(_ to_fp " <> size (eb, sb) <> ") " <> rm <> " (to_real " <> a <> ")" - cast KFP{} KUnbounded a = "to_int (fp.to_real " <> a <> ")" + cast KFP{} KUnbounded a = "to_int (fp.to_real (fp.roundToIntegral " <> rm <> " " <> a <> "))" -- To floats cast (KBounded False _) (KFP eb sb) a = addRM a $ "(_ to_fp_unsigned " <> size (eb, sb) <> ")" diff --git a/Data/SBV/Set.hs b/Data/SBV/Set.hs --- a/Data/SBV/Set.hs +++ b/Data/SBV/Set.hs @@ -294,8 +294,8 @@ -- -- >>> prove $ \x -> isFull (observe "set" (x `delete` (full :: SSet Integer))) -- Falsifiable. Counter-example: --- s0 = 2 :: Integer --- set = U - {2} :: {Integer} +-- s0 = 0 :: Integer +-- set = U - {0} :: {Integer} -- -- >>> isFull (full :: SSet Integer) -- True diff --git a/Documentation/SBV/Examples/Puzzles/Murder.hs b/Documentation/SBV/Examples/Puzzles/Murder.hs --- a/Documentation/SBV/Examples/Puzzles/Murder.hs +++ b/Documentation/SBV/Examples/Puzzles/Murder.hs @@ -87,10 +87,10 @@ -- | Solve the puzzle. We have: -- -- >>> killer --- Alice 47 Bar Female Bystander --- Husband 46 Beach Male Killer --- Brother 47 Beach Male Victim --- Daughter 20 Alone Female Bystander +-- Alice 48 Bar Female Bystander +-- Husband 47 Beach Male Killer +-- Brother 48 Beach Male Victim +-- Daughter 21 Alone Female Bystander -- Son 20 Bar Male Bystander -- -- That is, Alice's brother was the victim and Alice's husband was the killer. diff --git a/Documentation/SBV/Examples/Queries/Abducts.hs b/Documentation/SBV/Examples/Queries/Abducts.hs --- a/Documentation/SBV/Examples/Queries/Abducts.hs +++ b/Documentation/SBV/Examples/Queries/Abducts.hs @@ -23,9 +23,9 @@ -- -- >>> example -- Got: (define-fun abd () Bool (= s1 2)) --- Got: (define-fun abd () Bool (and (= s1 1) (<= s1 s0))) --- Got: (define-fun abd () Bool (and (<= 1 s0) (= s1 s0))) --- Got: (define-fun abd () Bool (and (<= s1 (+ s0 s0)) (<= 1 s1))) +-- Got: (define-fun abd () Bool (and (= s1 1) (= s1 s0))) +-- Got: (define-fun abd () Bool (and (= s0 2) (= s1 1))) +-- Got: (define-fun abd () Bool (and (<= 1 s0) (= s1 1))) -- -- Note that @s0@ refers to @x@ and @s1@ refers to @y@ above. You can verify -- that adding any of these will ensure @x + y >= 2@. diff --git a/Documentation/SBV/Examples/TP/Queue.hs b/Documentation/SBV/Examples/TP/Queue.hs new file mode 100644 --- /dev/null +++ b/Documentation/SBV/Examples/TP/Queue.hs @@ -0,0 +1,197 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Documentation.SBV.Examples.TP.Queue +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer: erkokl@gmail.com +-- Stability : experimental +-- +-- A classic functional queue implemented with two stacks (lists). The front +-- list holds elements ready for dequeue; the back list accumulates new +-- elements in reverse. We prove that this representation faithfully +-- implements a FIFO queue by showing: +-- +-- (1) Enqueue appends to the abstract queue. +-- (2) Enqueuing a sequence of elements and reading out the abstraction +-- gives back the original sequence. +-- (3) Dequeue retrieves the front of the abstract queue. +----------------------------------------------------------------------------- + +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE OverloadedLists #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeAbstractions #-} +{-# LANGUAGE TypeApplications #-} + +{-# OPTIONS_GHC -Wall -Werror #-} + +module Documentation.SBV.Examples.TP.Queue where + +import Prelude hiding (length, head, tail, null, reverse, (++), fst, snd) + +import Data.SBV +import Data.SBV.List +import Data.SBV.Tuple +import Data.SBV.TP + +#ifdef DOCTEST +-- $setup +-- >>> :set -XOverloadedLists +-- >>> :set -XTypeApplications +-- >>> import Data.SBV +-- >>> import Data.SBV.Tuple +-- >>> import Data.SBV.TP +#endif + +-- * Queue representation + +-- | A queue is a pair @(front, back)@ representing the abstract list +-- @front ++ reverse back@. +type Queue a = STuple [a] [a] + +-- | Abstraction function: the list a queue represents. +-- +-- >>> toList (tuple ([1,2,3], [6,5,4])) :: SList Integer +-- [1,2,3,4,5,6] :: [SInteger] +toList :: SymVal a => Queue a -> SList a +toList q = [sCase| q of + (f, b) -> f ++ reverse b + |] + +-- | The empty queue. +-- +-- >>> toList (emptyQ @Integer) +-- [] :: [SInteger] +emptyQ :: SymVal a => Queue a +emptyQ = tuple ([], []) + +-- | Enqueue: add an element to the back. +-- +-- >>> toList (enqueue (tuple ([1,2], [4,3])) 5) :: SList Integer +-- [1,2,3,4,5] :: [SInteger] +enqueue :: SymVal a => Queue a -> SBV a -> Queue a +enqueue q x = [sCase| q of + (f, b) -> tuple (f, x .: b) + |] + +-- | Enqueue all elements of a list, left to right. +-- +-- >>> toList (enqueueAll (emptyQ @Integer) [1,2,3]) +-- [1,2,3] :: [SInteger] +enqueueAll :: SymVal a => Queue a -> SList a -> Queue a +enqueueAll = smtFunction "enqueueAll" + $ \q xs -> [sCase| xs of + [] -> q + x : rest -> enqueueAll (enqueue q x) rest + |] + +-- | Dequeue: remove and return the front element. When the front list +-- is empty, we reverse the back list into the front first. +-- Precondition: the queue is non-empty. +-- +-- >>> let (v, q') = untuple (dequeue (tuple ([1,2,3], [6,5,4]) :: Queue Integer)) in (v, toList q') +-- (1 :: SInteger,[2,3,4,5,6] :: [SInteger]) +-- >>> let (v, q') = untuple (dequeue (tuple ([], [3,2,1]) :: Queue Integer)) in (v, toList q') +-- (1 :: SInteger,[2,3] :: [SInteger]) +dequeue :: forall a. SymVal a => Queue a -> STuple a ([a], [a]) +dequeue q = [sCase| q of + (x : xs, t) -> tuple (x, tuple (xs, t)) + ([], t) -> case reverse t of + y : ys -> tuple (y, tuple (ys, [])) + -- unreachable: both front and back are empty + _ -> tuple (some "dead" (const sTrue), tuple ([], [])) + |] + +-- * Correctness + +-- | @toList (enqueue q x) == toList q ++ [x]@ +-- +-- Enqueue appends to the abstract list. +-- +-- >>> runTP $ enqueueCorrect @Integer +-- Lemma: enqueueCorrect Q.E.D. +-- Functions proven terminating: sbv.reverse +-- [Proven] enqueueCorrect :: Ɐf ∷ [Integer] → Ɐb ∷ [Integer] → Ɐx ∷ Integer → Bool +enqueueCorrect :: forall a. SymVal a => TP (Proof (Forall "f" [a] -> Forall "b" [a] -> Forall "x" a -> SBool)) +enqueueCorrect = + lemma "enqueueCorrect" + (\(Forall @"f" f) (Forall @"b" b) (Forall @"x" x) -> + toList (enqueue (tuple (f, b)) x) .== toList (tuple (f, b)) ++ [x]) + [] + +-- | @toList (enqueueAll q xs) == toList q ++ xs@ +-- +-- Enqueuing a sequence of elements appends the whole sequence to the +-- abstract list. This is the key invariant of the two-stack representation. +-- +-- >>> runTP $ enqueueAllCorrect @Integer +-- Lemma: enqueueCorrect Q.E.D. +-- Inductive lemma: enqueueAllCorrect +-- Step: Base Q.E.D. +-- Step: 1 Q.E.D. +-- Step: 2 Q.E.D. +-- Step: 3 Q.E.D. +-- Result: Q.E.D. +-- Functions proven terminating: enqueueAll, sbv.reverse +-- [Proven] enqueueAllCorrect :: Ɐxs ∷ [Integer] → Ɐf ∷ [Integer] → Ɐb ∷ [Integer] → Bool +enqueueAllCorrect :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "f" [a] -> Forall "b" [a] -> SBool)) +enqueueAllCorrect = do + + eqC <- enqueueCorrect @a + + induct "enqueueAllCorrect" + (\(Forall @"xs" xs) (Forall @"f" f) (Forall @"b" b) -> + toList (enqueueAll (tuple (f, b)) xs) .== (f ++ reverse b) ++ xs) $ + \ih (x, xs) f b -> [] + |- toList (enqueueAll (tuple (f, b)) (x .: xs)) + =: toList (enqueueAll (tuple (f, x .: b)) xs) + ?? ih `at` (Inst @"f" f, Inst @"b" (x .: b)) + =: (f ++ reverse (x .: b)) ++ xs + ?? eqC + =: (f ++ reverse b) ++ (x .: xs) + =: qed + +-- | @toList (enqueueAll emptyQ xs) == xs@ +-- +-- Starting from an empty queue, enqueuing a list of elements produces +-- a queue whose abstract contents is that same list. This demonstrates +-- the fundamental FIFO property: elements come out in the order they went in. +-- +-- >>> runTP $ fifo @Integer +-- Lemma: enqueueAllCorrect Q.E.D. +-- Lemma: fifo +-- Step: 1 Q.E.D. +-- Step: 2 Q.E.D. +-- Result: Q.E.D. +-- Functions proven terminating: enqueueAll, sbv.reverse +-- [Proven] fifo :: Ɐxs ∷ [Integer] → Bool +fifo :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool)) +fifo = do + eaC <- recall (enqueueAllCorrect @a) + + calc "fifo" + (\(Forall xs) -> toList (enqueueAll emptyQ xs) .== xs) $ + \xs -> [] |- toList (enqueueAll emptyQ xs) + ?? eaC `at` (Inst @"xs" xs, Inst @"f" ([] :: SList a), Inst @"b" ([] :: SList a)) + =: reverse [] ++ xs + =: xs + =: qed + +-- | Dequeue from a non-empty queue gives the head of the abstract list, +-- and the remaining queue represents the tail. +-- +-- >>> runTP $ dequeueCorrect @Integer +-- Lemma: dequeueCorrect Q.E.D. +-- Functions proven terminating: sbv.reverse +-- [Proven] dequeueCorrect :: Ɐf ∷ [Integer] → Ɐb ∷ [Integer] → Bool +dequeueCorrect :: forall a. SymVal a => TP (Proof (Forall "f" [a] -> Forall "b" [a] -> SBool)) +dequeueCorrect = + lemma "dequeueCorrect" + (\(Forall @"f" f) (Forall @"b" b) -> + sNot (null (toList (tuple (f, b)))) + .=> let (v, q) = untuple (dequeue (tuple (f, b))) + l = toList (tuple (f, b)) + in v .== head l .&& toList q .== tail l) + [] diff --git a/Documentation/SBV/Examples/TP/RunLength.hs b/Documentation/SBV/Examples/TP/RunLength.hs new file mode 100644 --- /dev/null +++ b/Documentation/SBV/Examples/TP/RunLength.hs @@ -0,0 +1,198 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Documentation.SBV.Examples.TP.RunLength +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer: erkokl@gmail.com +-- Stability : experimental +-- +-- Proving that run-length decoding inverts encoding. We define: +-- +-- * @encode@: groups consecutive equal elements into (value, count) pairs +-- * @decode@: expands each pair back into a run of elements +-- +-- and prove @decode (encode xs) == xs@ for all finite lists @xs@. +----------------------------------------------------------------------------- + +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE OverloadedLists #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeAbstractions #-} +{-# LANGUAGE TypeApplications #-} + +{-# OPTIONS_GHC -Wall -Werror #-} + +module Documentation.SBV.Examples.TP.RunLength where + +import Prelude hiding (length, head, tail, null, reverse, (++), replicate, fst, snd) + +import Data.SBV +import Data.SBV.List +import Data.SBV.Tuple +import Data.SBV.TP + +#ifdef DOCTEST +-- $setup +-- >>> :set -XOverloadedLists +-- >>> :set -XTypeApplications +-- >>> import Data.SBV +-- >>> import Data.SBV.Tuple +-- >>> import Data.SBV.TP +#endif + +-- * Definitions + +-- | Run-length decode: expand each (value, count) pair into a run of that element. +-- +-- >>> decode (tuple (1,3) .: tuple (2,2) .: tuple (3,1) .: []) :: SList Integer +-- [1,1,1,2,2,3] :: [SInteger] +-- >>> decode ([] :: SList (Integer, Integer)) +-- [] :: [SInteger] +decode :: forall a. SymVal a => SList (a, Integer) -> SList a +decode = smtFunction "decode" + $ \ps -> [sCase| ps of + [] -> [] + (e, c) : rest -> replicate c e ++ decode rest + |] + +-- | Prepend an element to a run-length encoded list. If the head run has the +-- same value, we increment its count; otherwise we create a new singleton run. +-- +-- >>> encodeCons 1 (encode [1,1,2,2]) :: SList (Integer, Integer) +-- [(1,3),(2,2)] :: [(SInteger, SInteger)] +-- >>> encodeCons 5 (encode [1,1,2,2]) :: SList (Integer, Integer) +-- [(5,1),(1,2),(2,2)] :: [(SInteger, SInteger)] +encodeCons :: forall a. SymVal a => SBV a -> SList (a, Integer) -> SList (a, Integer) +encodeCons = smtFunction "encodeCons" + $ \x ps -> [sCase| ps of + [] -> [tuple (x, 1)] + (e, c) : rest | x .== e -> tuple (x, c + 1) .: rest + | True -> tuple (x, 1) .: ps + |] + +-- | Run-length encode: fold from the right, using 'encodeCons' to merge +-- each element into the growing encoding. +-- +-- >>> encode [1,1,1,2,2,3] :: SList (Integer, Integer) +-- [(1,3),(2,2),(3,1)] :: [(SInteger, SInteger)] +-- >>> encode ([] :: SList Integer) +-- [] :: [(SInteger, SInteger)] +-- >>> encode [4] :: SList (Integer, Integer) +-- [(4,1)] :: [(SInteger, SInteger)] +encode :: forall a. SymVal a => SList a -> SList (a, Integer) +encode = smtFunction "encode" + $ \xs -> [sCase| xs of + [] -> [] + x : rest -> encodeCons x (encode rest) + |] + +-- * Correctness + +-- | @decode (encode xs) == xs@ +-- +-- The proof proceeds by induction on @xs@. The key helper shows that +-- decoding after 'encodeCons' is the same as consing the element, +-- provided the head count in the encoded list is positive (which +-- 'encode' always guarantees). +-- +-- >>> runTPWith cvc5 $ correctness @Integer +-- Lemma: decodeEncodeCons +-- Step: 1 (3 way case split) +-- Step: 1.1.1 Q.E.D. +-- Step: 1.1.2 Q.E.D. +-- Step: 1.1.3 Q.E.D. +-- Step: 1.1.4 Q.E.D. +-- Step: 1.2.1 Q.E.D. +-- Step: 1.2.2 Q.E.D. +-- Step: 1.2.3 Q.E.D. +-- Step: 1.2.4 Q.E.D. +-- Step: 1.3.1 Q.E.D. +-- Step: 1.3.2 Q.E.D. +-- Step: 1.Completeness Q.E.D. +-- Result: Q.E.D. +-- Inductive lemma: encodeHeadPos +-- Step: Base Q.E.D. +-- Step: 1 (3 way case split) +-- Step: 1.1 Q.E.D. +-- Step: 1.2.1 Q.E.D. +-- Step: 1.2.2 Q.E.D. +-- Step: 1.2.3 Q.E.D. +-- Step: 1.3 Q.E.D. +-- Step: 1.Completeness Q.E.D. +-- Result: Q.E.D. +-- Inductive lemma (strong): rleCorrect +-- Step: Measure is non-negative Q.E.D. +-- Step: 1 (2 way case split) +-- Step: 1.1 Q.E.D. +-- Step: 1.2.1 Q.E.D. +-- Step: 1.2.2 Q.E.D. +-- Step: 1.2.3 Q.E.D. +-- Step: 1.2.4 Q.E.D. +-- Step: 1.Completeness Q.E.D. +-- Result: Q.E.D. +-- Functions proven terminating: decode, encode, sbv.replicate +-- [Proven] rleCorrect :: Ɐxs ∷ [Integer] → Bool +correctness :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool)) +correctness = do + + -- Key helper: encodeCons followed by decode is the same as consing. + -- The condition ensures the head count is positive so that + -- replicate (n+1) unfolds correctly. + helper <- calc "decodeEncodeCons" + (\(Forall @"x" (x :: SBV a)) (Forall @"ps" ps) -> + (null ps .|| snd (head ps) .>= 1) + .=> decode (encodeCons x ps) .== x .: decode ps) $ + \x ps -> [null ps .|| snd (head ps) .>= 1] + |- decode (encodeCons x ps) + =: [pCase| ps of + [] -> decode [tuple (x, 1)] + =: replicate 1 x ++ decode [] + =: [x] ++ decode [] + =: x .: decode [] + =: qed + ((e, c) : ecs) | x .== e -> decode (tuple (x, c + 1) .: ecs) + =: replicate (c + 1) x ++ decode ecs + =: x .: replicate c x ++ decode ecs + =: x .: decode (tuple (e, c) .: ecs) + =: qed + | True -> decode (tuple (x, 1) .: ps) + =: x .: decode ps + =: qed + |] + + -- encode always produces a list whose head (if any) has count >= 1 + -- (This is needed as a precondition for helper above.) + encPos <- induct "encodeHeadPos" + (\(Forall @"xs" (xs :: SList a)) -> + null (encode xs) .|| snd (head (encode xs)) .>= 1) $ + \ih (x, xs) -> [] + |- (null (encodeCons x (encode xs)) .|| snd (head (encodeCons x (encode xs))) .>= 1) + =: cases [ null (encode xs) ==> trivial + , sNot (null (encode xs)) .&& x .== fst (head (encode xs)) + ==> snd (head (encodeCons x (encode xs))) .>= 1 + =: snd (head (encode xs)) + 1 .>= 1 + ?? ih + =: sTrue + =: qed + , sNot (null (encode xs)) .&& x ./= fst (head (encode xs)) + ==> trivial + ] + + -- Main theorem: decode . encode == id + sInduct "rleCorrect" + (\(Forall xs) -> decode @a (encode xs) .== xs) + (length @a, []) $ + \ih xs -> [] |- decode (encode xs) + =: [pCase| xs of + [] -> trivial + whole@(x : ys) -> decode (encode whole) + =: decode (encodeCons x (encode ys)) + ?? helper `at` (Inst @"x" x, Inst @"ps" (encode ys)) + ?? encPos `at` Inst @"xs" ys + =: x .: decode (encode ys) + ?? ih `at` Inst @"xs" ys + =: x .: ys + =: qed + |] diff --git a/SBVTestSuite/GoldFiles/adt06.gold b/SBVTestSuite/GoldFiles/adt06.gold --- a/SBVTestSuite/GoldFiles/adt06.gold +++ b/SBVTestSuite/GoldFiles/adt06.gold @@ -94,10 +94,10 @@ [SEND] (get-value (s0)) [RECV] ((s0 (AMaybe (Just (mkSBVTuple3 2.0 (fp #b0 #x00 #b00000000000000000000001) - (mkSBVTuple2 (Right (fp #b0 #x01 #b00000000000010000000000)) + (mkSBVTuple2 (Right (fp #b0 #x00 #b00000000000000000100000)) (seq.unit true))))))) -getValue: AMaybe (Just (2.0,1.0e-45,(Right 1.1756378e-38,[True]))) +getValue: AMaybe (Just (2.0,1.0e-45,(Right 4.5e-44,[True]))) DONE *** Solver : Z3 *** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/doctest_sanity.gold b/SBVTestSuite/GoldFiles/doctest_sanity.gold --- a/SBVTestSuite/GoldFiles/doctest_sanity.gold +++ b/SBVTestSuite/GoldFiles/doctest_sanity.gold @@ -1,3 +1,3 @@ -Total: 1198; Tried: 1198; Skipped: 0; Success: 1198; Errors: 0; Failures 0 -Examples: 1061; Tried: 1061; Skipped: 0; Success: 1061; Errors: 0; Failures 0 -Setup: 137; Tried: 137; Skipped: 0; Success: 137; Errors: 0; Failures 0 +Total: 1226; Tried: 1226; Skipped: 0; Success: 1226; Errors: 0; Failures 0 +Examples: 1079; Tried: 1079; Skipped: 0; Success: 1079; Errors: 0; Failures 0 +Setup: 147; Tried: 147; Skipped: 0; Success: 147; Errors: 0; Failures 0 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.1:Data.SBV.TP.TP.TPProofGen - (SBV Bool) [sbv-14.1:Data.SBV.TP.TP.Helper] () + with actual type: sbv-14.2:Data.SBV.TP.TP.TPProofGen + (SBV Bool) [sbv-14.2: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.1:Data.SBV.TP.TP.TPProofGen - a0 [sbv-14.1:Data.SBV.TP.TP.Helper] () + with actual type: sbv-14.2:Data.SBV.TP.TP.TPProofGen + a0 [sbv-14.2: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_6989586621679034926"))) + (symWithKind "unmatched_sCase_Maybe_6989586621679034958"))) 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_6989586621679034926"))) + (symWithKind "unmatched_sCase_Maybe_6989586621679034958"))) 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_6989586621679034888"))) + (symWithKind "unmatched_sCase_Either_6989586621679034920"))) 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_6989586621679081419")))))) + (symWithKind "unmatched_sCase_Expr_6989586621679081453")))))) 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.1 +Version : 14.2 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 @@ -28,6 +28,11 @@ default : False manual : True +flag compile_examples + description: Compile examples for documentation. + default : True + manual : True + source-repository head type : git location: https://github.com/LeventErkok/sbv.git @@ -145,144 +150,149 @@ , Data.SBV.Tools.WeakestPreconditions , Data.SBV.Trans , Data.SBV.Trans.Control - , Documentation.SBV.Examples.ADT.Expr - , Documentation.SBV.Examples.ADT.Param - , Documentation.SBV.Examples.ADT.Types - , Documentation.SBV.Examples.BitPrecise.BitTricks - , Documentation.SBV.Examples.BitPrecise.BrokenSearch - , Documentation.SBV.Examples.BitPrecise.Legato - , Documentation.SBV.Examples.BitPrecise.MergeSort - , Documentation.SBV.Examples.BitPrecise.PEXT_PDEP - , Documentation.SBV.Examples.BitPrecise.PrefixSum - , Documentation.SBV.Examples.CodeGeneration.AddSub - , Documentation.SBV.Examples.CodeGeneration.CRC_USB5 - , Documentation.SBV.Examples.CodeGeneration.Fibonacci - , Documentation.SBV.Examples.CodeGeneration.GCD - , Documentation.SBV.Examples.CodeGeneration.PopulationCount - , Documentation.SBV.Examples.CodeGeneration.Uninterpreted - , Documentation.SBV.Examples.Crypto.AES - , Documentation.SBV.Examples.Crypto.RC4 - , Documentation.SBV.Examples.Crypto.Prince - , Documentation.SBV.Examples.Crypto.SHA - , Documentation.SBV.Examples.DeltaSat.DeltaSat - , Documentation.SBV.Examples.Existentials.Diophantine - , Documentation.SBV.Examples.Lists.Fibonacci - , Documentation.SBV.Examples.Lists.BoundedMutex - , Documentation.SBV.Examples.Lists.CountOutAndTransfer - , Documentation.SBV.Examples.Misc.Definitions - , Documentation.SBV.Examples.Misc.Enumerate - , Documentation.SBV.Examples.Misc.FirstOrderLogic - , Documentation.SBV.Examples.Misc.Floating - , Documentation.SBV.Examples.Misc.LambdaArray - , Documentation.SBV.Examples.Misc.ModelExtract - , Documentation.SBV.Examples.Misc.NestedArray - , Documentation.SBV.Examples.Misc.Auxiliary - , Documentation.SBV.Examples.Misc.NoDiv0 - , Documentation.SBV.Examples.Misc.Newtypes - , Documentation.SBV.Examples.Misc.Polynomials - , Documentation.SBV.Examples.Misc.ProgramPaths - , Documentation.SBV.Examples.Misc.SetAlgebra - , Documentation.SBV.Examples.Misc.SoftConstrain - , Documentation.SBV.Examples.Misc.Tuple - , Documentation.SBV.Examples.Optimization.Enumerate - , Documentation.SBV.Examples.Optimization.ExtField - , Documentation.SBV.Examples.Optimization.LinearOpt - , Documentation.SBV.Examples.Optimization.Production - , Documentation.SBV.Examples.Optimization.VM - , Documentation.SBV.Examples.ProofTools.AddHorn - , Documentation.SBV.Examples.ProofTools.BMC - , Documentation.SBV.Examples.ProofTools.Fibonacci - , Documentation.SBV.Examples.ProofTools.Strengthen - , Documentation.SBV.Examples.ProofTools.Sum - , Documentation.SBV.Examples.WeakestPreconditions.Append - , Documentation.SBV.Examples.WeakestPreconditions.Basics - , Documentation.SBV.Examples.WeakestPreconditions.Fib - , Documentation.SBV.Examples.WeakestPreconditions.GCD - , Documentation.SBV.Examples.WeakestPreconditions.IntDiv - , Documentation.SBV.Examples.WeakestPreconditions.IntSqrt - , Documentation.SBV.Examples.WeakestPreconditions.Length - , Documentation.SBV.Examples.WeakestPreconditions.Sum - , Documentation.SBV.Examples.Puzzles.AOC_2021_24 - , Documentation.SBV.Examples.Puzzles.Birthday - , Documentation.SBV.Examples.Puzzles.Coins - , Documentation.SBV.Examples.Puzzles.Counts - , Documentation.SBV.Examples.Puzzles.DieHard - , Documentation.SBV.Examples.Puzzles.DogCatMouse - , Documentation.SBV.Examples.Puzzles.Drinker - , Documentation.SBV.Examples.Puzzles.Euler185 - , Documentation.SBV.Examples.Puzzles.Fish - , Documentation.SBV.Examples.Puzzles.Garden - , Documentation.SBV.Examples.Puzzles.HexPuzzle - , Documentation.SBV.Examples.Puzzles.Jugs - , Documentation.SBV.Examples.Puzzles.KnightsAndKnaves - , Documentation.SBV.Examples.Puzzles.LadyAndTigers - , Documentation.SBV.Examples.Puzzles.MagicSquare - , Documentation.SBV.Examples.Puzzles.Murder - , Documentation.SBV.Examples.Puzzles.Newspaper - , Documentation.SBV.Examples.Puzzles.NQueens - , Documentation.SBV.Examples.Puzzles.Orangutans - , Documentation.SBV.Examples.Puzzles.Rabbits - , Documentation.SBV.Examples.Puzzles.SendMoreMoney - , Documentation.SBV.Examples.Puzzles.SquareBirthday - , Documentation.SBV.Examples.Puzzles.Sudoku - , Documentation.SBV.Examples.Puzzles.Tower - , Documentation.SBV.Examples.Puzzles.U2Bridge - , Documentation.SBV.Examples.Queries.Abducts - , Documentation.SBV.Examples.Queries.AllSat - , Documentation.SBV.Examples.Queries.UnsatCore - , Documentation.SBV.Examples.Queries.FourFours - , Documentation.SBV.Examples.Queries.GuessNumber - , Documentation.SBV.Examples.Queries.CaseSplit - , Documentation.SBV.Examples.Queries.Enums - , Documentation.SBV.Examples.Queries.Interpolants - , Documentation.SBV.Examples.Queries.Concurrency - , Documentation.SBV.Examples.Strings.RegexCrossword - , Documentation.SBV.Examples.Strings.SQLInjection - , Documentation.SBV.Examples.TP.Ackermann - , Documentation.SBV.Examples.TP.Basics - , Documentation.SBV.Examples.TP.BinarySearch - , Documentation.SBV.Examples.TP.CaseSplit - , Documentation.SBV.Examples.TP.Coins - , Documentation.SBV.Examples.TP.Collatz - , Documentation.SBV.Examples.TP.ConstFold - , Documentation.SBV.Examples.TP.Countdown - , Documentation.SBV.Examples.TP.Fibonacci - , Documentation.SBV.Examples.TP.GCD - , Documentation.SBV.Examples.TP.InsertionSort - , Documentation.SBV.Examples.TP.Kadane - , Documentation.SBV.Examples.TP.Kleene - , Documentation.SBV.Examples.TP.Lists - , Documentation.SBV.Examples.TP.McCarthy91 - , Documentation.SBV.Examples.TP.Majority - , Documentation.SBV.Examples.TP.MergeSort - , Documentation.SBV.Examples.TP.MutualCorecursion - , Documentation.SBV.Examples.TP.NatStream - , Documentation.SBV.Examples.TP.Numeric - , Documentation.SBV.Examples.TP.Peano - , Documentation.SBV.Examples.TP.PigeonHole - , Documentation.SBV.Examples.TP.PowerMod - , Documentation.SBV.Examples.TP.Primes - , Documentation.SBV.Examples.TP.QuickSort - , Documentation.SBV.Examples.TP.RevAcc - , Documentation.SBV.Examples.TP.Reverse - , Documentation.SBV.Examples.TP.ShefferStroke - , Documentation.SBV.Examples.TP.SortHelpers - , Documentation.SBV.Examples.TP.Sqrt2IsIrrational - , Documentation.SBV.Examples.TP.StrongInduction - , Documentation.SBV.Examples.TP.SumReverse - , Documentation.SBV.Examples.TP.Tao - , Documentation.SBV.Examples.TP.TautologyChecker - , Documentation.SBV.Examples.TP.UpDown - , Documentation.SBV.Examples.TP.VM - , Documentation.SBV.Examples.Transformers.SymbolicEval - , Documentation.SBV.Examples.Uninterpreted.AUF - , Documentation.SBV.Examples.Uninterpreted.Deduce - , Documentation.SBV.Examples.Uninterpreted.EUFLogic - , Documentation.SBV.Examples.Uninterpreted.Function - , Documentation.SBV.Examples.Uninterpreted.Multiply - , Documentation.SBV.Examples.Uninterpreted.Shannon - , Documentation.SBV.Examples.Uninterpreted.Sort - , Documentation.SBV.Examples.Uninterpreted.UISortAllSat + + if flag(compile_examples) + Exposed-modules : Documentation.SBV.Examples.ADT.Expr + , Documentation.SBV.Examples.ADT.Param + , Documentation.SBV.Examples.ADT.Types + , Documentation.SBV.Examples.BitPrecise.BitTricks + , Documentation.SBV.Examples.BitPrecise.BrokenSearch + , Documentation.SBV.Examples.BitPrecise.Legato + , Documentation.SBV.Examples.BitPrecise.MergeSort + , Documentation.SBV.Examples.BitPrecise.PEXT_PDEP + , Documentation.SBV.Examples.BitPrecise.PrefixSum + , Documentation.SBV.Examples.CodeGeneration.AddSub + , Documentation.SBV.Examples.CodeGeneration.CRC_USB5 + , Documentation.SBV.Examples.CodeGeneration.Fibonacci + , Documentation.SBV.Examples.CodeGeneration.GCD + , Documentation.SBV.Examples.CodeGeneration.PopulationCount + , Documentation.SBV.Examples.CodeGeneration.Uninterpreted + , Documentation.SBV.Examples.Crypto.AES + , Documentation.SBV.Examples.Crypto.RC4 + , Documentation.SBV.Examples.Crypto.Prince + , Documentation.SBV.Examples.Crypto.SHA + , Documentation.SBV.Examples.DeltaSat.DeltaSat + , Documentation.SBV.Examples.Existentials.Diophantine + , Documentation.SBV.Examples.Lists.Fibonacci + , Documentation.SBV.Examples.Lists.BoundedMutex + , Documentation.SBV.Examples.Lists.CountOutAndTransfer + , Documentation.SBV.Examples.Misc.Definitions + , Documentation.SBV.Examples.Misc.Enumerate + , Documentation.SBV.Examples.Misc.FirstOrderLogic + , Documentation.SBV.Examples.Misc.Floating + , Documentation.SBV.Examples.Misc.LambdaArray + , Documentation.SBV.Examples.Misc.ModelExtract + , Documentation.SBV.Examples.Misc.NestedArray + , Documentation.SBV.Examples.Misc.Auxiliary + , Documentation.SBV.Examples.Misc.NoDiv0 + , Documentation.SBV.Examples.Misc.Newtypes + , Documentation.SBV.Examples.Misc.Polynomials + , Documentation.SBV.Examples.Misc.ProgramPaths + , Documentation.SBV.Examples.Misc.SetAlgebra + , Documentation.SBV.Examples.Misc.SoftConstrain + , Documentation.SBV.Examples.Misc.Tuple + , Documentation.SBV.Examples.Optimization.Enumerate + , Documentation.SBV.Examples.Optimization.ExtField + , Documentation.SBV.Examples.Optimization.LinearOpt + , Documentation.SBV.Examples.Optimization.Production + , Documentation.SBV.Examples.Optimization.VM + , Documentation.SBV.Examples.ProofTools.AddHorn + , Documentation.SBV.Examples.ProofTools.BMC + , Documentation.SBV.Examples.ProofTools.Fibonacci + , Documentation.SBV.Examples.ProofTools.Strengthen + , Documentation.SBV.Examples.ProofTools.Sum + , Documentation.SBV.Examples.WeakestPreconditions.Append + , Documentation.SBV.Examples.WeakestPreconditions.Basics + , Documentation.SBV.Examples.WeakestPreconditions.Fib + , Documentation.SBV.Examples.WeakestPreconditions.GCD + , Documentation.SBV.Examples.WeakestPreconditions.IntDiv + , Documentation.SBV.Examples.WeakestPreconditions.IntSqrt + , Documentation.SBV.Examples.WeakestPreconditions.Length + , Documentation.SBV.Examples.WeakestPreconditions.Sum + , Documentation.SBV.Examples.Puzzles.AOC_2021_24 + , Documentation.SBV.Examples.Puzzles.Birthday + , Documentation.SBV.Examples.Puzzles.Coins + , Documentation.SBV.Examples.Puzzles.Counts + , Documentation.SBV.Examples.Puzzles.DieHard + , Documentation.SBV.Examples.Puzzles.DogCatMouse + , Documentation.SBV.Examples.Puzzles.Drinker + , Documentation.SBV.Examples.Puzzles.Euler185 + , Documentation.SBV.Examples.Puzzles.Fish + , Documentation.SBV.Examples.Puzzles.Garden + , Documentation.SBV.Examples.Puzzles.HexPuzzle + , Documentation.SBV.Examples.Puzzles.Jugs + , Documentation.SBV.Examples.Puzzles.KnightsAndKnaves + , Documentation.SBV.Examples.Puzzles.LadyAndTigers + , Documentation.SBV.Examples.Puzzles.MagicSquare + , Documentation.SBV.Examples.Puzzles.Murder + , Documentation.SBV.Examples.Puzzles.Newspaper + , Documentation.SBV.Examples.Puzzles.NQueens + , Documentation.SBV.Examples.Puzzles.Orangutans + , Documentation.SBV.Examples.Puzzles.Rabbits + , Documentation.SBV.Examples.Puzzles.SendMoreMoney + , Documentation.SBV.Examples.Puzzles.SquareBirthday + , Documentation.SBV.Examples.Puzzles.Sudoku + , Documentation.SBV.Examples.Puzzles.Tower + , Documentation.SBV.Examples.Puzzles.U2Bridge + , Documentation.SBV.Examples.Queries.Abducts + , Documentation.SBV.Examples.Queries.AllSat + , Documentation.SBV.Examples.Queries.UnsatCore + , Documentation.SBV.Examples.Queries.FourFours + , Documentation.SBV.Examples.Queries.GuessNumber + , Documentation.SBV.Examples.Queries.CaseSplit + , Documentation.SBV.Examples.Queries.Enums + , Documentation.SBV.Examples.Queries.Interpolants + , Documentation.SBV.Examples.Queries.Concurrency + , Documentation.SBV.Examples.Strings.RegexCrossword + , Documentation.SBV.Examples.Strings.SQLInjection + , Documentation.SBV.Examples.TP.Ackermann + , Documentation.SBV.Examples.TP.Basics + , Documentation.SBV.Examples.TP.BinarySearch + , Documentation.SBV.Examples.TP.CaseSplit + , Documentation.SBV.Examples.TP.Coins + , Documentation.SBV.Examples.TP.Collatz + , Documentation.SBV.Examples.TP.ConstFold + , Documentation.SBV.Examples.TP.Countdown + , Documentation.SBV.Examples.TP.Fibonacci + , Documentation.SBV.Examples.TP.GCD + , Documentation.SBV.Examples.TP.InsertionSort + , Documentation.SBV.Examples.TP.Kadane + , Documentation.SBV.Examples.TP.Kleene + , Documentation.SBV.Examples.TP.Lists + , Documentation.SBV.Examples.TP.McCarthy91 + , Documentation.SBV.Examples.TP.Majority + , Documentation.SBV.Examples.TP.MergeSort + , Documentation.SBV.Examples.TP.MutualCorecursion + , Documentation.SBV.Examples.TP.NatStream + , Documentation.SBV.Examples.TP.Numeric + , Documentation.SBV.Examples.TP.Peano + , Documentation.SBV.Examples.TP.PigeonHole + , Documentation.SBV.Examples.TP.PowerMod + , Documentation.SBV.Examples.TP.Primes + , Documentation.SBV.Examples.TP.Queue + , Documentation.SBV.Examples.TP.QuickSort + , Documentation.SBV.Examples.TP.RevAcc + , Documentation.SBV.Examples.TP.Reverse + , Documentation.SBV.Examples.TP.RunLength + , Documentation.SBV.Examples.TP.ShefferStroke + , Documentation.SBV.Examples.TP.SortHelpers + , Documentation.SBV.Examples.TP.Sqrt2IsIrrational + , Documentation.SBV.Examples.TP.StrongInduction + , Documentation.SBV.Examples.TP.SumReverse + , Documentation.SBV.Examples.TP.Tao + , Documentation.SBV.Examples.TP.TautologyChecker + , Documentation.SBV.Examples.TP.UpDown + , Documentation.SBV.Examples.TP.VM + , Documentation.SBV.Examples.Transformers.SymbolicEval + , Documentation.SBV.Examples.Uninterpreted.AUF + , Documentation.SBV.Examples.Uninterpreted.Deduce + , Documentation.SBV.Examples.Uninterpreted.EUFLogic + , Documentation.SBV.Examples.Uninterpreted.Function + , Documentation.SBV.Examples.Uninterpreted.Multiply + , Documentation.SBV.Examples.Uninterpreted.Shannon + , Documentation.SBV.Examples.Uninterpreted.Sort + , Documentation.SBV.Examples.Uninterpreted.UISortAllSat + other-modules : Data.SBV.Client , Data.SBV.Client.BaseIO , Data.SBV.Core.AlgReals