sbv 12.1 → 12.2
raw patch · 55 files changed
+1476/−466 lines, 55 files
Files
- CHANGES.md +30/−0
- Data/SBV.hs +5/−1
- Data/SBV/Client.hs +11/−3
- Data/SBV/Core/Data.hs +2/−1
- Data/SBV/Core/Floating.hs +21/−23
- Data/SBV/Core/Model.hs +54/−14
- Data/SBV/Core/Operations.hs +21/−15
- Data/SBV/Core/Symbolic.hs +1/−0
- Data/SBV/List.hs +1/−1
- Data/SBV/Provers/Prover.hs +1/−0
- Data/SBV/Rational.hs +61/−4
- Data/SBV/SMT/SMTLib2.hs +1/−49
- Data/SBV/TP.hs +5/−2
- Data/SBV/TP/List.hs +3/−2
- Data/SBV/TP/TP.hs +32/−6
- Data/SBV/TP/Utils.hs +20/−6
- Data/SBV/Tools/Range.hs +2/−2
- Documentation/SBV/Examples/Lists/BoundedMutex.hs +1/−0
- Documentation/SBV/Examples/Misc/Enumerate.hs +1/−0
- Documentation/SBV/Examples/Misc/FirstOrderLogic.hs +1/−0
- Documentation/SBV/Examples/Optimization/Enumerate.hs +1/−0
- Documentation/SBV/Examples/Puzzles/Birthday.hs +1/−0
- Documentation/SBV/Examples/Puzzles/Fish.hs +1/−0
- Documentation/SBV/Examples/Puzzles/Garden.hs +1/−0
- Documentation/SBV/Examples/Puzzles/HexPuzzle.hs +1/−0
- Documentation/SBV/Examples/Puzzles/KnightsAndKnaves.hs +1/−0
- Documentation/SBV/Examples/Puzzles/Orangutans.hs +1/−0
- Documentation/SBV/Examples/Queries/Enums.hs +1/−0
- Documentation/SBV/Examples/TP/Basics.hs +2/−2
- Documentation/SBV/Examples/TP/BinarySearch.hs +1/−1
- Documentation/SBV/Examples/TP/GCD.hs +999/−0
- Documentation/SBV/Examples/TP/InsertionSort.hs +4/−3
- Documentation/SBV/Examples/TP/Majority.hs +3/−3
- Documentation/SBV/Examples/TP/MergeSort.hs +4/−3
- Documentation/SBV/Examples/TP/QuickSort.hs +28/−14
- Documentation/SBV/Examples/TP/Reverse.hs +22/−53
- Documentation/SBV/Examples/TP/SortHelpers.hs +4/−3
- Documentation/SBV/Examples/TP/Sqrt2IsIrrational.hs +6/−6
- README.md +1/−0
- SBVTestSuite/GoldFiles/doctest_sanity.gold +3/−3
- SBVTestSuite/GoldFiles/queryArrays12.gold +0/−35
- SBVTestSuite/GoldFiles/queryArrays13.gold +0/−35
- SBVTestSuite/GoldFiles/queryArrays14.gold +0/−35
- SBVTestSuite/GoldFiles/queryArrays15.gold +0/−35
- SBVTestSuite/GoldFiles/queryArrays16.gold +0/−35
- SBVTestSuite/GoldFiles/queryArrays17.gold +0/−35
- SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs +56/−18
- SBVTestSuite/TestSuite/Basics/ArithNoSolver2.hs +1/−0
- SBVTestSuite/TestSuite/Basics/ArithSolver.hs +51/−15
- SBVTestSuite/TestSuite/Basics/Set.hs +1/−0
- SBVTestSuite/TestSuite/Basics/Tuple.hs +1/−0
- SBVTestSuite/TestSuite/Queries/Enums.hs +1/−0
- SBVTestSuite/TestSuite/Queries/FreshVars.hs +1/−0
- SBVTestSuite/TestSuite/Queries/Uninterpreted.hs +1/−0
- sbv.cabal +4/−3
CHANGES.md view
@@ -1,6 +1,36 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://github.com/LeventErkok/sbv> +### Version 12.2, 2025-08-15++ * Fix floating-point constant-folding code, which inadvertently constant-folded for symbolic rounding modes.++ * Euclidian modulus/division does not restrict division by 0. Following SMTLib, we allow sEDiv and sEMod+ to underconstrain the value if the divisor is 0. The main motivation for this is to allow for direct translation+ to SMTLib for these operations where solvers perform much better. Fixed the code to avoid unintended constant+ folding for the euclidian case.++ * Add missing Num instance for SRational and beef up test suite. Thanks to Jan Grant for reporting.++ * [BACKWARDS COMPATIBILITY] Reworked OrdSymbolic and Numeric instances, making them more robust. While this should+ be mostly invisible to end-users, you might have to add an extra 'FlexibleInstances' pragma that wasn't needed+ before. Please get in touch if you see inadvertent effects due to uses of symbolic ordering.++ * TP: Add tpAsms, which explicitly prints the assumption-proving step for each proof transition. Default is False,+ as assumptions are typically simple to prove. But if you use complicated booleans, this step can come in handy+ in seeing where a proof gets stuck.++ * TP: Add 'recall': Which turns of printing for a TP computation. This allows for non-verbose output in proof-scripts+ when we reuse an old proof. Note that this is safe: We still run the proof mentioned so any failures in it will+ be caught; it's just that we do it quietly to reduce verbosity in the re-calling proof.++ * TP: Add '|->': This is similar to '|-', except it applies to a boolean-chain of reasoning where each step is+ equivalent to the conjunction of the previous and the next. This allows for concise expression of boolean+ reasoning steps. See gcdAdd in Documentation.SBV.Examples.TP.GCD for an example.++ * Added Documentation.SBV.Examples.TP.GCD, which proves correctness and several other properties of Euclidian+ GCD algorithm. We also prove subtraction based and the so-called binary-GCD algorithms correct.+ ### Version 12.1, 2025-07-11 * Add missing instances for strong-equality, extending it to lists/Maybe etc. (Only impacts floats and structures
Data/SBV.hs view
@@ -165,6 +165,7 @@ -- See "Data.SBV.TP" for the API, and -- -- - "Documentation.SBV.Examples.TP.BinarySearch"+-- - "Documentation.SBV.Examples.TP.GCD" -- - "Documentation.SBV.Examples.TP.InsertionSort" -- - "Documentation.SBV.Examples.TP.MergeSort" -- - "Documentation.SBV.Examples.TP.QuickSort"@@ -226,7 +227,7 @@ , SFPQuad, FPQuad , fpFromInteger -- ** Rationals- , SRational+ , SRational, (.%) -- ** Algebraic reals -- $algReals , SReal, AlgReal(..), sRealToSInteger, algRealToRational, RealPoint(..), realPoint, RationalCV(..)@@ -548,6 +549,8 @@ import Data.SBV.List (EnumSymbolic(..)) import Data.SBV.SEnum (sEnum) +import Data.SBV.Rational+ #ifdef DOCTEST --- $setup --- >>> :set -XDataKinds -XFlexibleContexts -XTypeApplications -XRankNTypes@@ -1148,6 +1151,7 @@ > LANGUAGE StandaloneDeriving > LANGUAGE DeriveDataTypeable > LANGUAGE DeriveAnyClass+> LANGUAGE FlexibleInstances and your own declaration must have instances of 'Enum' and 'Bounded'. (The instances can be derived, as above.) This will automatically introduce the type:
Data/SBV/Client.hs view
@@ -46,7 +46,8 @@ #endif import Data.SBV.Core.Data-import Data.SBV.Core.Model () -- instances only+import Data.SBV.Core.Model+import Data.SBV.Core.Operations import Data.SBV.Provers.Prover -- | Check whether the given solver is installed and is ready to go. This call does a@@ -89,7 +90,8 @@ -- | Turn a name into a symbolic type. If first argument is true, then we're doing an enumeration, otherwise it's an uninterpreted type declareSymbolic :: Bool -> TH.Name -> TH.Q [TH.Dec] declareSymbolic isEnum typeName = do- let typeCon = TH.conT typeName+ let typeCon = TH.conT typeName+ sTypeCon = TH.conT ''SBV `TH.appT` typeCon cstrs <- if isEnum then ensureEnumeration typeName else ensureEmptyData typeName@@ -145,10 +147,16 @@ enumFromTo n m = SL.map SL.toEnum (SL.enumFromTo (SL.fromEnum n) (SL.fromEnum m)) enumFromThenTo n m t = SL.map SL.toEnum (SL.enumFromThenTo (SL.fromEnum n) (SL.fromEnum m) (SL.fromEnum t))++ instance OrdSymbolic $sTypeCon where+ SBV a .< SBV b = SBV (a `svLessThan` b)+ SBV a .<= SBV b = SBV (a `svLessEq` b)+ SBV a .> SBV b = SBV (a `svGreaterThan` b)+ SBV a .>= SBV b = SBV (a `svGreaterEq` b) |] else pure [] - sType <- TH.conT ''SBV `TH.appT` typeCon+ sType <- sTypeCon let declConstructor c = ((nm, bnm), [sig, def]) where bnm = TH.nameBase c
Data/SBV/Core/Data.hs view
@@ -825,7 +825,8 @@ negate (SBV a) = SBV $ svUNeg a; \ } --- Derive basic instances we need+-- Derive basic instances we need. NB. We don't give the SRational instance here. It's handled+-- in Data/SBV/Rational due to representation issues. MKSNUM((), SInteger, KUnbounded) MKSNUM((), SWord8, (KBounded False 8)) MKSNUM((), SWord16, (KBounded False 16))
Data/SBV/Core/Floating.hs view
@@ -32,7 +32,7 @@ , svFloatingPointAsSWord ) where -import Control.Monad (when)+import Control.Monad (when, guard) import Data.Bits (testBit) import Data.Int (Int8, Int16, Int32, Int64)@@ -344,34 +344,34 @@ -- From and To are the same when the source is an arbitrary float! fromSFloatingPoint = toSFloatingPoint +-- | Is this RM safe to concretely calculate with? OK if there's no RM for this op, or if it is RNE+safeRM :: Maybe SRoundingMode -> Bool+safeRM Nothing = True+safeRM (Just srm) | Just RoundNearestTiesToEven <- unliteral srm = True+ | True = False+ -- | Concretely evaluate one arg function, if rounding mode is RoundNearestTiesToEven and we have enough concrete data concEval1 :: SymVal a => Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> Maybe (SBV a) concEval1 mbOp mbRm a = do op <- mbOp v <- unliteral a- case unliteral =<< mbRm of- Nothing -> (Just . literal) (op v)- Just RoundNearestTiesToEven -> (Just . literal) (op v)- _ -> Nothing+ guard (safeRM mbRm)+ pure $ literal (op v) -- | Concretely evaluate two arg function, if rounding mode is RoundNearestTiesToEven and we have enough concrete data concEval2 :: SymVal a => Maybe (a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe (SBV a) concEval2 mbOp mbRm a b = do op <- mbOp v1 <- unliteral a v2 <- unliteral b- case unliteral =<< mbRm of- Nothing -> (Just . literal) (v1 `op` v2)- Just RoundNearestTiesToEven -> (Just . literal) (v1 `op` v2)- _ -> Nothing+ guard (safeRM mbRm)+ pure $ literal (v1 `op` v2) -- | Concretely evaluate a bool producing two arg function, if rounding mode is RoundNearestTiesToEven and we have enough concrete data concEval2B :: SymVal a => Maybe (a -> a -> Bool) -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe SBool concEval2B mbOp mbRm a b = do op <- mbOp v1 <- unliteral a v2 <- unliteral b- case unliteral =<< mbRm of- Nothing -> (Just . literal) (v1 `op` v2)- Just RoundNearestTiesToEven -> (Just . literal) (v1 `op` v2)- _ -> Nothing+ guard (safeRM mbRm)+ pure $ literal (v1 `op` v2) -- | Concretely evaluate two arg function, if rounding mode is RoundNearestTiesToEven and we have enough concrete data concEval3 :: SymVal a => Maybe (a -> a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a -> Maybe (SBV a)@@ -379,10 +379,8 @@ v1 <- unliteral a v2 <- unliteral b v3 <- unliteral c- case unliteral =<< mbRm of- Nothing -> (Just . literal) (op v1 v2 v3)- Just RoundNearestTiesToEven -> (Just . literal) (op v1 v2 v3)- _ -> Nothing+ guard (safeRM mbRm)+ pure $ literal (op v1 v2 v3) -- | Add the converted rounding mode if given as an argument addRM :: State -> Maybe SRoundingMode -> [SV] -> IO [SV]@@ -731,12 +729,12 @@ -- Sized-floats have a special instance, since it can handle arbitrary rounding modes when it matters. instance ValidFloat eb sb => IEEEFloating (FloatingPoint eb sb) where- fpAdd = lift2FP bfAdd (lift2 FP_Add (Just (+)))- fpSub = lift2FP bfSub (lift2 FP_Sub (Just (-)))- fpMul = lift2FP bfMul (lift2 FP_Mul (Just (*)))- fpDiv = lift2FP bfDiv (lift2 FP_Div (Just (/)))- fpFMA = lift3FP bfFMA (lift3 FP_FMA Nothing)- fpSqrt = lift1FP bfSqrt (lift1 FP_Sqrt (Just sqrt))+ fpAdd = lift2FP bfAdd (lift2 FP_Add (Just (+)))+ fpSub = lift2FP bfSub (lift2 FP_Sub (Just (-)))+ fpMul = lift2FP bfMul (lift2 FP_Mul (Just (*)))+ fpDiv = lift2FP bfDiv (lift2 FP_Div (Just (/)))+ fpFMA = lift3FP bfFMA (lift3 FP_FMA Nothing)+ fpSqrt = lift1FP bfSqrt (lift1 FP_Sqrt (Just sqrt)) fpRoundToIntegral rm a | Just (FloatingPoint (FP ei si v)) <- unliteral a
Data/SBV/Core/Model.hs view
@@ -1014,19 +1014,55 @@ val <- sbvToSV st value newExpr st k (SBVApp WriteArray [arr, keyVal, val]) --- | If comparison is over something SMTLib can handle, just translate it. Otherwise desugar.-instance (Ord a, SymVal a) => OrdSymbolic (SBV a) where- a@(SBV x) .< b@(SBV y) | smtComparable "<" a b = SBV (svLessThan x y)- | True = SBV (svStructuralLessThan x y)+-- We don't want to do a generic OrdSymbolic (SBV a) instance; since that would be dangerous, like the case+-- for Num. So, we explicitly define for each type we care about. - a@(SBV x) .<= b@(SBV y) | smtComparable ".<=" a b = SBV (svLessEq x y)- | True = a .< b .|| a .== b+#define MKSORD(CSTR, TYPE) \+instance CSTR => OrdSymbolic TYPE where { \+ a@(SBV x) .< b@(SBV y) | smtComparable "<" a b = SBV (svLessThan x y) \+ | True = SBV (svStructuralLessThan x y); \+ \+ a@(SBV x) .<= b@(SBV y) | smtComparable ".<=" a b = SBV (svLessEq x y) \+ | True = a .< b .|| a .== b; \+ \+ a@(SBV x) .> b@(SBV y) | smtComparable ">" a b = SBV (svGreaterThan x y) \+ | True = b .< a; \+ \+ a@(SBV x) .>= b@(SBV y) | smtComparable ">=" a b = SBV (svGreaterEq x y) \+ | True = b .<= a; \+} \ - a@(SBV x) .> b@(SBV y) | smtComparable ">" a b = SBV (svGreaterThan x y)- | True = b .< a+-- Derive basic instances we need. NB. We don't give the SRational instance here. It's handled+-- in Data/SBV/Rational due to representation issues.+MKSORD((), SInteger)+MKSORD((), SWord8)+MKSORD((), SWord16)+MKSORD((), SWord32)+MKSORD((), SWord64)+MKSORD((), SInt8)+MKSORD((), SInt16)+MKSORD((), SInt32)+MKSORD((), SInt64)+MKSORD((), SFloat)+MKSORD((), SChar)+MKSORD((SymVal a), (SMaybe a))+MKSORD((SymVal a), (SList a))+MKSORD((SymVal a, SymVal b), (SEither a b))+MKSORD((), SDouble)+MKSORD((), SReal)+MKSORD((KnownNat n, BVIsNonZero n), (SWord n))+MKSORD((KnownNat n, BVIsNonZero n), (SInt n))+MKSORD((ValidFloat eb sb), (SFloatingPoint eb sb)) - a@(SBV x) .>= b@(SBV y) | smtComparable ">=" a b = SBV (svGreaterEq x y)- | True = b .<= a+-- Tuples+MKSORD((SymVal a, SymVal b), (SBV (a, b)))+MKSORD((SymVal a, SymVal b, SymVal c), (SBV (a, b, c)))+MKSORD((SymVal a, SymVal b, SymVal c, SymVal d), (SBV (a, b, c, d)))+MKSORD((SymVal a, SymVal b, SymVal c, SymVal d, SymVal e), (SBV (a, b, c, d, e)))+MKSORD((SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f), (SBV (a, b, c, d, e, f)))+MKSORD((SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g), (SBV (a, b, c, d, e, f, g)))+MKSORD((SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h), (SBV (a, b, c, d, e, f, g, h)))+#undef MKSORD -- Is this a type that's comparable by underlying translation to SMTLib? -- Note that we allow concrete versions to go through unless the type is a set, as there's really no reason not to.@@ -1230,7 +1266,7 @@ -- | Finite bit-length symbolic values. Essentially the same as 'SIntegral', but further leaves out 'Integer'. Loosely -- based on Haskell's @FiniteBits@ class, but with more methods defined and structured differently to fit into the -- symbolic world view. Minimal complete definition: 'sFiniteBitSize'.-class (Ord a, SymVal a, Num a, Num (SBV a), Bits a) => SFiniteBits a where+class (Ord a, SymVal a, Num a, Num (SBV a), OrdSymbolic (SBV a), Bits a) => SFiniteBits a where -- | Bit size. sFiniteBitSize :: SBV a -> Int -- | Least significant bit of a word, always stored at index 0.@@ -2140,11 +2176,13 @@ sEDivMod :: SInteger -> SInteger -> (SInteger, SInteger) sEDivMod a b = (a `sEDiv` b, a `sEMod` b) --- | Euclidian division.+-- | Euclidian division. Note that unlike regular division, Euclidian division by @0@+-- is unconstrained. i.e., it can take any value whatsoever. sEDiv :: SInteger -> SInteger -> SInteger sEDiv (SBV a) (SBV b) = SBV $ a `svQuot` b --- | Euclidian modulus.+-- | Euclidian modulus. Note that unlike regular modulus, Euclidian division by @0@+-- is unconstrained. i.e., it can take any value whatsoever. sEMod :: SInteger -> SInteger -> SInteger sEMod (SBV a) (SBV b) = SBV $ a `svRem` b @@ -2178,10 +2216,12 @@ -- make but unfortunately necessary for getting symbolic simulation -- working efficiently. symbolicMerge :: Bool -> SBool -> a -> a -> a+ -- | Total indexing operation. @select xs default index@ is intuitively -- the same as @xs !! index@, except it evaluates to @default@ if @index@ -- underflows/overflows.- select :: (Ord b, SymVal b, Num b, Num (SBV b)) => [a] -> a -> SBV b -> a+ select :: (Ord b, SymVal b, Num b, Num (SBV b), OrdSymbolic (SBV b)) => [a] -> a -> SBV b -> a+ -- NB. Earlier implementation of select used the binary-search trick -- on the index to chop down the search space. While that is a good trick -- in general, it doesn't work for SBV since we do not have any notion of
Data/SBV/Core/Operations.hs view
@@ -268,18 +268,21 @@ -- "div" operator ("Euclidean" division, which always has a -- non-negative remainder). For unsigned bitvectors, it is "bvudiv"; -- and for signed bitvectors it is "bvsdiv", which rounds toward zero.--- Division by 0 is defined s.t. @x/0 = 0@, which holds even when @x@ itself is @0@.+-- Note that this variant does not respect the division/reminder by 0. That's handled at the SBV level. svQuot :: SVal -> SVal -> SVal svQuot x y- | isConcreteZero x = x- | isConcreteZero y = svInteger (kindOf x) 0- | isConcreteOne y = x- | True = liftSym2 (mkSymOp Quot) [nonzeroCheck]- (noReal "quot") quot' (noFloat "quot") (noDouble "quot") (noFP "quot") (noRat "quot") x y+ | not isInteger && isConcreteZero x = x+ | not isInteger && isConcreteZero y = svInteger (kindOf x) 0+ | not isInteger && isConcreteOne y = x+ | True+ = liftSym2 (mkSymOp Quot) [nonzeroCheck]+ (noReal "quot") quot' (noFloat "quot") (noDouble "quot") (noFP "quot") (noRat "quot") x y where- quot' a b | kindOf x == KUnbounded = div a (abs b) * signum b- | otherwise = quot a b+ isInteger = kindOf x == KUnbounded + quot' a b | isInteger = div a (abs b) * signum b+ | otherwise = 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@@ -288,14 +291,17 @@ -- defined s.t. @x/0 = 0@, which holds even when @x@ itself is @0@. svRem :: SVal -> SVal -> SVal svRem x y- | isConcreteZero x = x- | isConcreteZero y = x- | isConcreteOne y = svInteger (kindOf x) 0- | True = liftSym2 (mkSymOp Rem) [nonzeroCheck]- (noReal "rem") rem' (noFloat "rem") (noDouble "rem") (noFP "rem") (noRat "rem") x y+ | not isInteger && isConcreteZero x = x+ | not isInteger && isConcreteZero y = x+ | not isInteger && isConcreteOne y = svInteger (kindOf x) 0+ | True+ = liftSym2 (mkSymOp Rem) [nonzeroCheck]+ (noReal "rem") rem' (noFloat "rem") (noDouble "rem") (noFP "rem") (noRat "rem") x y where- rem' a b | kindOf x == KUnbounded = mod a (abs b)- | otherwise = rem a b+ isInteger = kindOf x == KUnbounded++ rem' a b | isInteger = mod a (abs b)+ | otherwise = rem a b -- | Combination of quot and rem svQuotRem :: SVal -> SVal -> (SVal, SVal)
Data/SBV/Core/Symbolic.hs view
@@ -2232,6 +2232,7 @@ data TPOptions = TPOptions { ribbonLength :: Int -- ^ Line length for TP proofs , quiet :: Bool -- ^ No messages what-so-ever for successful steps. (Will print if something fails)+ , printAsms :: Bool -- ^ Print assumptions as they are proven as separate steps. , printStats :: Bool -- ^ Print time/statistics. If quiet is True, then measureTime is ignored. , cacheProofs :: Bool -- ^ Treat lemma names as unique, and cache the results. Default: False. Note that this -- feature is unsound unless you make sure (by some other mechanism) that your lemma names
Data/SBV/List.hs view
@@ -242,7 +242,7 @@ -- Q.E.D. -- >>> sat $ \(l :: SList Word16) -> length l .>= 2 .&& listToListAt l 0 ./= listToListAt l (length l - 1) -- Satisfiable. Model:--- s0 = [0,64] :: [Word16]+-- s0 = [0,32] :: [Word16] listToListAt :: SymVal a => SList a -> SInteger -> SList a listToListAt s offset = subList s offset 1
Data/SBV/Provers/Prover.hs view
@@ -109,6 +109,7 @@ , firstifyUniqueLen = 10 , tpOptions = TPOptions { ribbonLength = 40 , quiet = False+ , printAsms = False , printStats = False , cacheProofs = False }
Data/SBV/Rational.hs view
@@ -9,8 +9,10 @@ -- Symbolic rationals, corresponds to Haskell's 'Rational' type ----------------------------------------------------------------------------- -{-# OPTIONS_GHC -Wall -Werror #-}+{-# LANGUAGE FlexibleInstances #-} +{-# OPTIONS_GHC -Wall -Werror -Wno-orphans #-}+ module Data.SBV.Rational ( -- * Constructing rationals (.%)@@ -19,15 +21,15 @@ import qualified Data.Ratio as R import Data.SBV.Core.Data-import Data.SBV.Core.Model () -- instances only+import Data.SBV.Core.Model infixl 7 .% -- | Construct a symbolic rational from a given numerator and denominator. Note that -- it is not possible to deconstruct a rational by taking numerator and denominator -- fields, since we do not represent them canonically. (This is due to the fact that--- SMTLib has no functions to compute the GCD. One can use the maximization engine--- to compute the GCD of numbers, but not as a function.)+-- SMTLib has no functions to compute the GCD. While we can define a recursive function+-- to do so, it would almost always imply non-decidability for even the simplest queries.) (.%) :: SInteger -> SInteger -> SRational top .% bot | Just t <- unliteral top@@ -38,3 +40,58 @@ where res st = do t <- sbvToSV st top b <- sbvToSV st bot newExpr st KRational $ SBVApp RationalConstructor [t, b]++-- | 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+doNotExport_numerator x = SBV $ SVal KUnbounded $ Right $ cache res+ where res st = do xv <- sbvToSV st x+ newExpr st KUnbounded $ SBVApp (Uninterpreted "sbv.rat.numerator") [xv]++-- | 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_denominator :: SRational -> SInteger+doNotExport_denominator x = SBV $ SVal KUnbounded $ Right $ cache res+ where res st = do xv <- sbvToSV st x+ newExpr st KUnbounded $ SBVApp (Uninterpreted "sbv.rat.denominator") [xv]++-- | Num instance for SRational. Note that denominators are always positive.+instance Num SRational where+ fromInteger i = SBV $ SVal KRational $ Left $ mkConstCV KRational (fromIntegral i :: Integer)+ (+) = lift2 (+) (\(t1, b1) (t2, b2) -> (t1 * b2 + t2 * b1) .% (b1 * b2))+ (-) = lift2 (-) (\(t1, b1) (t2, b2) -> (t1 * b2 - t2 * b1) .% (b1 * b2))+ (*) = lift2 (*) (\(t1, b1) (t2, b2) -> (t1 * t2 ) .% (b1 * b2))+ 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++-- | Symbolic ordering for SRational. Note that denominators are always positive.+instance OrdSymbolic SRational where+ (.<) = lift2 (<) (\(t1, b1) (t2, b2) -> (t1 * b2) .< (b1 * t2))+ (.<=) = lift2 (<=) (\(t1, b1) (t2, b2) -> (t1 * b2) .<= (b1 * t2))+ (.>) = lift2 (>) (\(t1, b1) (t2, b2) -> (t1 * b2) .> (b1 * t2))+ (.>=) = lift2 (>=) (\(t1, b1) (t2, b2) -> (t1 * b2) .>= (b1 * t2))++-- | Get the top and bottom parts. Internal only; do not export!+doNotExport_getTB :: SRational -> (SInteger, SInteger)+doNotExport_getTB a = (doNotExport_numerator a, doNotExport_denominator a)++-- | Lift a function over one rational+lift1 :: SymVal t => (Rational -> t) -> ((SInteger, SInteger) -> SBV t) -> SRational -> SBV t+lift1 cf f a+ | Just va <- unliteral a+ = literal (cf va)+ | True+ = f (doNotExport_getTB a)++-- | Lift a function over two rationals+lift2 :: SymVal t => (Rational -> Rational -> t) -> ((SInteger, SInteger) -> (SInteger, SInteger) -> SBV t) -> SRational -> SRational -> SBV t+lift2 cf f a b+ | Just va <- unliteral a, Just vb <- unliteral b+ = literal (va `cf` vb)+ | True+ = f (doNotExport_getTB a) (doNotExport_getTB b)++{- HLint ignore type doNotExport_numerator "Use camelCase" -}+{- HLint ignore type doNotExport_denominator "Use camelCase" -}+{- HLint ignore type doNotExport_getTB "Use camelCase" -}
Data/SBV/SMT/SMTLib2.hs view
@@ -388,41 +388,6 @@ , "(define-fun sbv.rat.notEq ((x SBVRational) (y SBVRational)) Bool" , " (not (sbv.rat.eq x y))" , ")"- , ""- , "(define-fun sbv.rat.lt ((x SBVRational) (y SBVRational)) Bool"- , " (< (* (sbv.rat.numerator x) (sbv.rat.denominator y))"- , " (* (sbv.rat.denominator x) (sbv.rat.numerator y)))"- , ")"- , ""- , "(define-fun sbv.rat.leq ((x SBVRational) (y SBVRational)) Bool"- , " (<= (* (sbv.rat.numerator x) (sbv.rat.denominator y))"- , " (* (sbv.rat.denominator x) (sbv.rat.numerator y)))"- , ")"- , ""- , "(define-fun sbv.rat.plus ((x SBVRational) (y SBVRational)) SBVRational"- , " (SBV.Rational (+ (* (sbv.rat.numerator x) (sbv.rat.denominator y))"- , " (* (sbv.rat.denominator x) (sbv.rat.numerator y)))"- , " (* (sbv.rat.denominator x) (sbv.rat.denominator y)))"- , ")"- , ""- , "(define-fun sbv.rat.minus ((x SBVRational) (y SBVRational)) SBVRational"- , " (SBV.Rational (- (* (sbv.rat.numerator x) (sbv.rat.denominator y))"- , " (* (sbv.rat.denominator x) (sbv.rat.numerator y)))"- , " (* (sbv.rat.denominator x) (sbv.rat.denominator y)))"- , ")"- , ""- , "(define-fun sbv.rat.times ((x SBVRational) (y SBVRational)) SBVRational"- , " (SBV.Rational (* (sbv.rat.numerator x) (sbv.rat.numerator y))"- , " (* (sbv.rat.denominator x) (sbv.rat.denominator y)))"- , ")"- , ""- , "(define-fun sbv.rat.uneg ((x SBVRational)) SBVRational"- , " (SBV.Rational (* (- 1) (sbv.rat.numerator x)) (sbv.rat.denominator x))"- , ")"- , ""- , "(define-fun sbv.rat.abs ((x SBVRational)) SBVRational"- , " (SBV.Rational (abs (sbv.rat.numerator x)) (sbv.rat.denominator x))"- , ")" ] -- | Convert in a query context.@@ -1075,25 +1040,12 @@ , (GreaterEq, lift2Cmp ">=" "fp.geq") ] - ratOpTable = [ (Plus, lift2Rat "sbv.rat.plus")- , (Minus, lift2Rat "sbv.rat.minus")- , (Times, lift2Rat "sbv.rat.times")- , (UNeg, liftRat "sbv.rat.uneg")- , (Abs, liftRat "sbv.rat.abs")- , (Equal True, lift2Rat "sbv.rat.eq")+ ratOpTable = [ (Equal True, lift2Rat "sbv.rat.eq") , (Equal False, lift2Rat "sbv.rat.eq") , (NotEqual, lift2Rat "sbv.rat.notEq")- , (LessThan, lift2Rat "sbv.rat.lt")- , (GreaterThan, lift2Rat "sbv.rat.lt" . swap)- , (LessEq, lift2Rat "sbv.rat.leq")- , (GreaterEq, lift2Rat "sbv.rat.leq" . swap) ] where lift2Rat o [x, y] = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")" lift2Rat o sbvs = error $ "SBV.SMTLib2.sh.lift2Rat: Unexpected arguments: " ++ show (o, sbvs)- liftRat o [x] = "(" ++ o ++ " " ++ x ++ ")"- liftRat o sbvs = error $ "SBV.SMTLib2.sh.lift2Rat: Unexpected arguments: " ++ show (o, sbvs)- swap [x, y] = [y, x]- swap sbvs = error $ "SBV.SMTLib2.sh.swap: Unexpected arguments: " ++ show sbvs -- equality and comparisons are the only thing that works on uninterpreted sorts and pretty much everything else uninterpretedTable = [ (Equal True, lift2S "=" "=" True)
Data/SBV/TP.hs view
@@ -45,10 +45,10 @@ , sorry -- * Running TP proofs- , TP, runTP, runTPWith, tpQuiet, tpRibbon, tpStats, tpCache+ , TP, runTP, runTPWith, tpQuiet, tpRibbon, tpStats, tpAsms, tpCache -- * Starting a calculation proof- , (|-), (⊢)+ , (|-), (⊢), (|->) -- * Sequence of calculation steps , (=:), (≡)@@ -67,6 +67,9 @@ -- * Displaying intermediate values of expressions , disp++ -- * Recall an old proof, quietly proving it+ , recall ) where import Data.SBV.TP.TP
Data/SBV/TP/List.hs view
@@ -173,9 +173,10 @@ -- This property comes from Richard Bird's "Pearls of functional Algorithm Design" book, chapter 2. -- Note that it is not exactly as stated there, as the definition of @tail@ Bird uses is different -- than the standard Haskell function @tails@: Bird's version does not return the empty list as the--- tail. So, we slightly modify it to fit the standard definition.+-- tail. So, we slightly modify it to fit the standard definition. (NB. z3 is finicky on this+-- problem, while cvc5 works much better.) ----- >>> runTP $ tailsAppend @Integer+-- >>> runTPWith cvc5 $ tailsAppend @Integer -- Inductive lemma: base case -- Step: Base Q.E.D. -- Step: 1 Q.E.D.
Data/SBV/TP/TP.hs view
@@ -32,10 +32,11 @@ , induct, inductWith , sInduct, sInductWith , sorry- , TP, runTP, runTPWith, tpQuiet, tpRibbon, tpStats, tpCache- , (|-), (⊢), (=:), (≡), (??), (∵), split, split2, cases, (==>), (⟹), qed, trivial, contradiction+ , TP, runTP, runTPWith, tpQuiet, tpRibbon, tpStats, tpAsms, tpCache+ , (|-), (|->), (⊢), (=:), (≡), (??), (∵), split, split2, cases, (==>), (⟹), qed, trivial, contradiction , qc, qcWith , disp+ , recall ) where import Data.SBV@@ -44,7 +45,7 @@ import qualified Data.SBV.Core.Symbolic as S (sObserve) import Data.SBV.Core.Operations (svEqual)-import Data.SBV.Control hiding (getProof)+import Data.SBV.Control hiding (getProof, (|->)) import Data.SBV.TP.Kernel import Data.SBV.TP.Utils@@ -242,7 +243,7 @@ , isCached = False } - where SMTConfig{tpOptions = TPOptions{printStats}} = cfg+ where SMTConfig{tpOptions = TPOptions{printStats, printAsms}} = cfg isEnd ProofEnd{} = True isEnd ProofStep{} = False@@ -314,8 +315,8 @@ -- First prove the assumptions, if there are any. We stay quiet, unless timing is asked for (quietCfg, finalizer)- | printStats = (cfg, finish [] [])- | True = (cfg{tpOptions = (tpOptions cfg) {quiet = True}}, const (pure ()))+ | printStats || printAsms = (cfg, finish [] [])+ | True = (cfg{tpOptions = (tpOptions cfg) {quiet = True}}, const (pure ())) as = concatMap getHelperAssumes hs ss = getHelperText hs@@ -1443,6 +1444,17 @@ bs |- p = (sAnd bs, p) infixl 0 |- +-- | Start an implicational proof, with the given hypothesis. Use @[]@ as the+-- first argument if the calculation holds unconditionally. Each step will be a cascading+-- chain of conjunctions of the previous, starting from @sTrue@.+(|->) :: [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)+bs |-> p = (sAnd bs, xform sTrue p)+ where xform :: SBool -> TPProofGen SBool [Helper] () -> TPProofGen SBool [Helper] ()+ xform conj (ProofStep a hs r) = let ca = conj .&& a in ProofStep ca hs (xform ca r)+ xform conj (ProofBranch b bh ss) = ProofBranch b bh [(bc, xform conj r) | (bc, r) <- ss]+ xform _ (ProofEnd b hs ) = ProofEnd b hs+infixl 0 |->+ -- | Alternative unicode for `|-`. (⊢) :: [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a) (⊢) = (|-)@@ -1503,5 +1515,19 @@ (⟹) :: SBool -> TPProofRaw a -> (SBool, TPProofRaw a) (⟹) = (==>) infix 0 ⟹++-- | Recalling a proof. This essentially sets the verbose output off during this proof. Note that+-- if we're doing stats, we ignore this as the whole point of doing stats is to see steps in detail.+recall :: String -> TP (Proof a) -> TP (Proof a)+recall nm prf = do+ cfg <- getTPConfig+ if printStats (tpOptions cfg)+ then prf+ else do tab <- liftIO $ startTP cfg (verbose cfg) "Lemma" 0 (TPProofOneShot nm [])+ setTPConfig cfg{tpOptions = (tpOptions cfg) {quiet = True}}+ r@Proof{proofOf = ProofObj{dependencies}} <- prf+ setTPConfig cfg+ liftIO $ finishTP cfg ("Q.E.D." ++ concludeModulo dependencies) (tab, Nothing) []+ pure r {- HLint ignore module "Eta reduce" -}
Data/SBV/TP/Utils.hs view
@@ -24,11 +24,11 @@ module Data.SBV.TP.Utils ( TP, runTP, runTPWith, Proof(..), ProofObj(..), assumptionFromProof, sorry, quickCheckProof- , startTP, finishTP, getTPState, getTPConfig, tpGetNextUnique, TPState(..), TPStats(..), RootOfTrust(..)+ , startTP, finishTP, getTPState, getTPConfig, setTPConfig, tpGetNextUnique, TPState(..), TPStats(..), RootOfTrust(..) , TPProofContext(..), message, updStats, rootOfTrust, concludeModulo , ProofTree(..), TPUnique(..), showProofTree, showProofTreeHTML, shortProofName , withProofCache- , tpQuiet, tpRibbon, tpStats, tpCache+ , tpQuiet, tpRibbon, tpAsms, tpStats, tpCache ) where import Control.Monad.Reader (ReaderT, runReaderT, MonadReader, ask, liftIO)@@ -76,7 +76,7 @@ -- | Extra state we carry in a TP context data TPState = TPState { stats :: IORef TPStats , proofCache :: IORef (Map (String, TypeRep) ProofObj)- , config :: SMTConfig+ , config :: IORef SMTConfig } -- | Monad for running TP proofs in.@@ -86,7 +86,8 @@ -- | If caches are enabled, see if we cached this proof and return it; otherwise generate it, cache it, and return it withProofCache :: forall a. Typeable a => String -> TP (Proof a) -> TP (Proof a) withProofCache nm genProof = do- TPState{proofCache, config = cfg@SMTConfig {tpOptions = TPOptions {cacheProofs}}} <- getTPState+ TPState{proofCache, config} <- getTPState+ cfg@SMTConfig {tpOptions = TPOptions {cacheProofs}} <- liftIO $ readIORef config let key = (nm, typeOf (Proxy @a)) @@ -118,7 +119,8 @@ runTPWith cfg@SMTConfig{tpOptions = TPOptions{printStats}} (TP f) = do rStats <- newIORef $ TPStats { noOfCheckSats = 0, solverElapsed = 0, qcElapsed = 0 } rCache <- newIORef Map.empty- (mbT, r) <- timeIf printStats $ runReaderT f TPState {config = cfg, stats = rStats, proofCache = rCache}+ rCfg <- newIORef cfg+ (mbT, r) <- timeIf printStats $ runReaderT f TPState {config = rCfg, stats = rStats, proofCache = rCache} case mbT of Nothing -> pure () Just t -> do TPStats noOfCheckSats solverTime qcElapsed <- readIORef rStats@@ -143,8 +145,14 @@ -- | get the configuration getTPConfig :: TP SMTConfig-getTPConfig = config <$> getTPState+getTPConfig = do rCfg <- config <$> getTPState+ liftIO (readIORef rCfg) +-- | set the configuration+setTPConfig :: SMTConfig -> TP ()+setTPConfig cfg = do st <- getTPState+ liftIO (writeIORef (config st) cfg)+ -- | Update stats updStats :: MonadIO m => TPState -> (TPStats -> TPStats) -> m () updStats TPState{stats} u = liftIO $ modifyIORef' stats u@@ -455,3 +463,9 @@ -- inherit the caching behavior settings from the surrounding environment. tpCache :: SMTConfig -> SMTConfig tpCache cfg = cfg{tpOptions = (tpOptions cfg) { cacheProofs = True }}++-- | When proving assumptions for each step, print them as well. Normally, SBV doesn't+-- print assumptions in each proof step, though it does prove them as they are typically trivial.+-- But in certain cases seeing them would be helpful.+tpAsms :: SMTConfig -> SMTConfig+tpAsms cfg = cfg{tpOptions = (tpOptions cfg) { printAsms = True }}
Data/SBV/Tools/Range.hs view
@@ -101,11 +101,11 @@ -- [(-oo,0.0]] -- >>> ranges $ \(x :: SWord 4) -> 2*x .== 4 -- [[2,3),(9,10]]-ranges :: forall a. (Ord a, Num a, SymVal a, SatModel a, Metric a, SymVal (MetricSpace a), SatModel (MetricSpace a)) => (SBV a -> SBool) -> IO [Range a]+ranges :: forall a. (OrdSymbolic (SBV a), Num a, SymVal a, SatModel a, Metric a, SymVal (MetricSpace a), SatModel (MetricSpace a)) => (SBV a -> SBool) -> IO [Range a] ranges = rangesWith defaultSMTCfg -- | Compute ranges, using the given solver configuration.-rangesWith :: forall a. (Ord a, Num a, SymVal a, SatModel a, Metric a, SymVal (MetricSpace a), SatModel (MetricSpace a)) => SMTConfig -> (SBV a -> SBool) -> IO [Range a]+rangesWith :: forall a. (OrdSymbolic (SBV a), Num a, SymVal a, SatModel a, Metric a, SymVal (MetricSpace a), SatModel (MetricSpace a)) => SMTConfig -> (SBV a -> SBool) -> IO [Range a] rangesWith cfg prop = do mbBounds <- getInitialBounds case mbBounds of Nothing -> return []
Documentation/SBV/Examples/Lists/BoundedMutex.hs view
@@ -12,6 +12,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedLists #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-}
Documentation/SBV/Examples/Misc/Enumerate.hs view
@@ -14,6 +14,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-}
Documentation/SBV/Examples/Misc/FirstOrderLogic.hs view
@@ -14,6 +14,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-}
Documentation/SBV/Examples/Optimization/Enumerate.hs view
@@ -12,6 +12,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-}
Documentation/SBV/Examples/Puzzles/Birthday.hs view
@@ -37,6 +37,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-}
Documentation/SBV/Examples/Puzzles/Fish.hs view
@@ -31,6 +31,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-}
Documentation/SBV/Examples/Puzzles/Garden.hs view
@@ -30,6 +30,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-}
Documentation/SBV/Examples/Puzzles/HexPuzzle.hs view
@@ -38,6 +38,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-}
@@ -14,6 +14,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-}
Documentation/SBV/Examples/Puzzles/Orangutans.hs view
@@ -14,6 +14,7 @@ {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE OverloadedRecordDot #-}
Documentation/SBV/Examples/Queries/Enums.hs view
@@ -11,6 +11,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-}
Documentation/SBV/Examples/TP/Basics.hs view
@@ -261,7 +261,7 @@ -- Lemma: badRevLen -- *** Failed to prove badRevLen. -- Falsifiable. Counter-example:--- xs = [14,11,14] :: [Integer]+-- xs = [17,17,17] :: [Integer] badRevLen :: IO () badRevLen = runTP $ void $ lemma "badRevLen"@@ -277,7 +277,7 @@ -- Lemma: badLengthProof -- *** Failed to prove badLengthProof. -- Falsifiable. Counter-example:--- xs = [15,11,13,16,27,42] :: [Integer]+-- xs = [12,15,20,24,33,42] :: [Integer] -- imp = 42 :: Integer -- spec = 6 :: Integer badLengthProof :: IO ()
Documentation/SBV/Examples/TP/BinarySearch.hs view
@@ -6,7 +6,7 @@ -- Maintainer: erkokl@gmail.com -- Stability : experimental ----- Proving binary search correct+-- Proving binary search correct. ----------------------------------------------------------------------------- {-# LANGUAGE DataKinds #-}
+ Documentation/SBV/Examples/TP/GCD.hs view
@@ -0,0 +1,999 @@+-----------------------------------------------------------------------------+-- |+-- Module : Documentation.SBV.Examples.TP.GCD+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer: erkokl@gmail.com+-- Stability : experimental+--+-- We define three different versions of the GCD algorithm: (1) Regular+-- version using the modulus operator, (2) the more basic version using+-- subtraction, and (3) the so called binary GCD. We prove that the modulus+-- based algorithm correct, i.e., that it calculates the greatest-common-divisor+-- of its arguments. We then prove that the other two variants are equivalent+-- to this version, thus establishing their correctness as well.+-----------------------------------------------------------------------------++{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE TypeApplications #-}++{-# OPTIONS_GHC -Wall -Werror #-}++module Documentation.SBV.Examples.TP.GCD where++import Prelude hiding (gcd)++import Data.SBV+import Data.SBV.TP+import Data.SBV.Tuple++#ifdef DOCTEST+-- $setup+-- >>> import Data.SBV.TP+#endif++-- * Calculating GCD++-- | @nGCD@ is the version of GCD that works on non-negative integers.+--+-- Ideally, we should make this function local to @gcd@, but then we can't refer to it explicitly in our proofs.+--+-- Note on maximality: Note that, by definition @gcd 0 0 = 0@. Since any number divides @0@,+-- there is no greatest common divisor for the pair @(0, 0)@. So, maximality here is meant+-- to be in terms of divisibility. That is, any divisor of @a@ and @b@ will also divide their @gcd@.+nGCD :: SInteger -> SInteger -> SInteger+nGCD = smtFunction "nGCD" $ \a b -> ite (b .== 0) a (nGCD b (a `sEMod` b))++-- | Generalized GCD, working for all integers. We simply call @nGCD@ with the absolute value of the arguments.+gcd :: SInteger -> SInteger -> SInteger+gcd a b = nGCD (abs a) (abs b)++-- * Basic properties++-- | \(\gcd\, a\ b \geq 0\)+--+-- ==== __Proof__+-- >>> runTP gcdNonNegative+-- Inductive lemma (strong): nonNegativeNGCD+-- 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.Completeness Q.E.D.+-- Result: Q.E.D.+-- Lemma: nonNegative Q.E.D.+-- [Proven] nonNegative :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool+gcdNonNegative :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))+gcdNonNegative = do+ -- We first prove over nGCD, using strong induction with the measure @a+b@.+ nn <- sInduct "nonNegativeNGCD"+ (\(Forall a) (Forall b) -> a .>= 0 .&& b .>= 0 .=> nGCD a b .>= 0)+ (\_a b -> b) $+ \ih a b -> [a .>= 0, b .>= 0]+ |- cases [ b .== 0 ==> trivial+ , b ./= 0 ==> nGCD a b .>= 0+ =: nGCD b (a `sEMod` b) .>= 0+ ?? ih `at` (Inst @"a" b, Inst @"b" (a `sEMod` b))+ =: sTrue+ =: qed+ ]++ lemma "nonNegative"+ (\(Forall a) (Forall b) -> gcd a b .>= 0)+ [proofOf nn]++-- | \(\gcd\, a\ b=0\implies a=0\land b=0\)+--+-- ==== __Proof__+-- >>> runTP gcdZero+-- Inductive lemma (strong): nGCDZero+-- 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.Completeness Q.E.D.+-- Result: Q.E.D.+-- Lemma: gcdZero Q.E.D.+-- [Proven] gcdZero :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool+gcdZero :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))+gcdZero = do++ -- First prove over nGCD:+ nGCDZero <-+ sInduct "nGCDZero"+ (\(Forall @"a" a) (Forall @"b" b) -> a .>= 0 .&& b .>= 0 .&& nGCD a b .== 0 .=> a .== 0 .&& b .== 0)+ (\_a b -> b) $+ \ih a b -> [a .>= 0, b .>= 0]+ |- (nGCD a b .== 0 .=> a .== 0 .&& b .== 0)+ =: cases [ b .== 0 ==> trivial+ , b .> 0 ==> (nGCD b (a `sEMod` b) .== 0 .=> a .== 0 .&& b .== 0)+ ?? ih `at` (Inst @"a" b, Inst @"b" (a `sEMod` b))+ =: sTrue+ =: qed+ ]++ lemma "gcdZero"+ (\(Forall @"a" a) (Forall @"b" b) -> gcd a b .== 0 .=> a .== 0 .&& b .== 0) + [proofOf nGCDZero]++-- | \(\gcd\, a\ b=\gcd\, b\ a\)+--+-- ==== __Proof__+-- >>> runTP commutative+-- Lemma: nGCDCommutative+-- Step: 1 Q.E.D.+-- Result: Q.E.D.+-- Lemma: commutative+-- Step: 1 Q.E.D.+-- Result: Q.E.D.+-- [Proven] commutative :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool+commutative :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))+commutative = do+ -- First prove over nGCD. Simple enough proof, but quantifiers and recursive functions+ -- cause z3 to diverge. So, we have to explicitly write it out.+ nGCDComm <-+ calc "nGCDCommutative"+ (\(Forall @"a" a) (Forall @"b" b) -> a .>= 0 .&& b .>= 0 .=> nGCD a b .== nGCD b a) $+ \a b -> [a .>= 0, b .>= 0]+ |- nGCD a b+ =: nGCD b a+ =: qed++ -- It's unfortunate we have to spell this out explicitly, a simple lemma call+ -- that uses the above proof doesn't converge.+ calc "commutative"+ (\(Forall a) (Forall b) -> gcd a b .== gcd b a) $+ \a b -> [] |- gcd a b+ ?? nGCDComm+ =: gcd b a+ =: qed++-- | \(\gcd\,(-a)\,b = \gcd\,a\,b = \gcd\,a\,(-b)\)+--+-- ==== __Proof__+-- >>> runTP negGCD+-- Lemma: negGCD Q.E.D.+-- [Proven] negGCD :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool+negGCD :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))+negGCD = lemma "negGCD" (\(Forall a) (Forall b) -> let g = gcd a b in gcd (-a) b .== g .&& g .== gcd a (-b)) []++-- | \( \gcd\,a\,0 = \gcd\,0\,a = |a| \land \gcd\,0\,0 = 0\)+--+-- ==== __Proof__+-- >>> runTP zeroGCD+-- Lemma: negGCD Q.E.D.+-- [Proven] negGCD :: Ɐa ∷ Integer → Bool+zeroGCD :: TP (Proof (Forall "a" Integer -> SBool))+zeroGCD = lemma "negGCD" (\(Forall a) -> gcd a 0 .== gcd 0 a .&& gcd 0 a .== abs a .&& gcd 0 0 .== 0) []++-- * Even and odd++-- | Is the given integer even?+isEven :: SInteger -> SBool+isEven = (2 `sDivides`)++-- | Is the given integer odd?+isOdd :: SInteger -> SBool+isOdd = sNot . isEven++-- * Divisibility++-- | Divides relation. By definition we @0@ only divides @0@. (But every number divides @0@).+dvd :: SInteger -> SInteger -> SBool+a `dvd` b = ite (a .== 0) (b .== 0) (b `sEMod` a .== 0)++-- | \(a \mid |b| \iff a \mid b\)+--+-- A number divides another exactly when it also divides its absolute value. While this property+-- seems obvious, I was unable to get z3 to prove it. Even CVC5 needs a bit of help to guide it through+-- the case split on @b@.+--+-- ==== __Proof__+-- >>> runTP dvdAbs+-- Lemma: dvdAbs_l2r+-- Step: 1 (2 way case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- Lemma: dvdAbs_r2l+-- Step: 1 (2 way case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- Lemma: dvdAbs Q.E.D.+-- [Proven] dvdAbs :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool+dvdAbs :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))+dvdAbs = do+ l2r <- calcWith cvc5 "dvdAbs_l2r"+ (\(Forall @"a" a) (Forall @"b" b) -> a `dvd` abs b .=> a `dvd` b) $+ \a b -> [a `dvd` abs b]+ |- cases [ b .< 0 ==> sTrue =: qed+ , b .>= 0 ==> sTrue =: qed+ ]++ r2l <- calcWith cvc5 "dvdAbs_r2l"+ (\(Forall @"a" a) (Forall @"b" b) -> a `dvd` b .=> a `dvd` abs b) $+ \a b -> [a `dvd` b]+ |- cases [ b .< 0 ==> sTrue =: qed+ , b .>= 0 ==> sTrue =: qed+ ]++ lemma "dvdAbs"+ (\(Forall @"a" a) (Forall @"b" b) -> a `dvd` b .== a `dvd` abs b)+ [proofOf l2r, proofOf r2l]++-- | \(d \mid a \implies d \mid ka\)+--+-- ==== __Proof__+-- >>> runTP dvdMul+-- Lemma: dvdMul+-- Step: 1 (2 way case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- [Proven] dvdMul :: Ɐd ∷ Integer → Ɐa ∷ Integer → Ɐk ∷ Integer → Bool+dvdMul :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> Forall "k" Integer -> SBool))+dvdMul = calc "dvdMul"+ (\(Forall d) (Forall a) (Forall k) -> d `dvd` a .=> d `dvd` (k*a)) $+ \d a k -> [d `dvd` a]+ |- cases [ d .== 0 ==> d `dvd` (k*a)+ ?? a .== 0+ =: sTrue+ =: qed+ , d ./= 0 ==> d `dvd` (k*a)+ ?? a .== d * a `sEDiv` d+ =: d `dvd` (k * d * a `sEDiv` d)+ =: qed+ ]++-- | \(d \mid (2a + 1) \implies \mathrm{isOdd}(d)\)+--+-- ==== __Proof__+-- >>> runTP dvdOddThenOdd+-- Lemma: dvdOddThenOdd+-- 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.Completeness Q.E.D.+-- Result: Q.E.D.+-- [Proven] dvdOddThenOdd :: Ɐd ∷ Integer → Ɐa ∷ Integer → Bool+dvdOddThenOdd :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool))+dvdOddThenOdd = calc "dvdOddThenOdd"+ (\(Forall d) (Forall a) -> d `dvd` (2*a+1) .=> isOdd d) $+ \d a -> [d `dvd` (2*a+1)]+ |- cases [ isOdd d ==> trivial+ , isEven d ==> (2 * (d `sEDiv` 2)) `dvd` (2*a+1)+ =: 2 `dvd` (2*a+1)+ =: contradiction+ ]++-- | \(\mathrm{isOdd}(d) \land d \mid 2a \implies d \mid a\)+--+-- ==== __Proof__+-- >>> runTP dvdEvenWhenOdd+-- Lemma: dvdEvenWhenOdd+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Step: 5 Q.E.D.+-- Step: 6 Q.E.D.+-- Step: 7 Q.E.D.+-- Result: Q.E.D.+-- [Proven] dvdEvenWhenOdd :: Ɐd ∷ Integer → Ɐa ∷ Integer → Bool+dvdEvenWhenOdd :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool))+dvdEvenWhenOdd = calc "dvdEvenWhenOdd"+ (\(Forall d) (Forall a) -> isOdd d .&& d `dvd` (2*a) .=> d `dvd` a) $+ \d a -> [isOdd d, d `dvd` (2*a)]+ |-> let t = (d - 1) `sEDiv` 2+ m = (2*a) `sEDiv` d+ in sTrue++ -- Observe that d = 2t+1 and 2a = dm+ =: d .== 2*t + 1 .&& 2*a .== d*m++ -- So, 2a == (2t+1)m holds+ =: 2*a .== (2*t+1) * m++ -- Arithmetic gives us+ =: 2*a .== 2*t*m + m .&& 2*(a-t*m) .== m++ -- So, we now now m is even+ =: 2 `sDivides` m++ -- Give that divisor a name:+ =: let n = m `sEDiv` 2++ -- It follows that 2a = d(2n) = 2(dn)+ in 2*a .== d * (2 * n) .&& 2 * a .== 2 * (d * n)++ -- From which we can conclude a = dn+ =: a .== d * n++ -- Thus we can deduce d must divide a+ =: d `dvd` a++ -- Done!+ =: qed++-- | \(d \mid a \land d \mid b \implies d \mid (a + b)\)+--+-- ==== __Proof__+-- >>> runTP dvdSum1+-- Lemma: dvdSum1+-- 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.Completeness Q.E.D.+-- Result: Q.E.D.+-- [Proven] dvdSum1 :: Ɐd ∷ Integer → Ɐa ∷ Integer → Ɐb ∷ Integer → Bool+dvdSum1 :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> Forall "b" Integer -> SBool))+dvdSum1 =+ calc "dvdSum1"+ (\(Forall d) (Forall a) (Forall b) -> d `dvd` a .&& d `dvd` b .=> d `dvd` (a + b)) $+ \d a b -> [d `dvd` a .&& d `dvd` b]+ |- cases [ a .== 0 .|| b .== 0 ==> trivial+ , a ./= 0 .&& b ./= 0 ==> d `dvd` (a + b)+ =: d `dvd` (a `sEDiv` d * d + b `sEDiv` d * d)+ =: d `dvd` (d * (a `sEDiv` d + b `sEDiv` d))+ =: sTrue+ =: qed+ ]++-- | \(d \mid (a + b) \land d \mid b \implies d \mid a \)+--+-- ==== __Proof__+-- >>> runTP dvdSum2+-- Lemma: dvdSum2+-- 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.Completeness Q.E.D.+-- Result: Q.E.D.+-- [Proven] dvdSum2 :: Ɐd ∷ Integer → Ɐa ∷ Integer → Ɐb ∷ Integer → Bool+dvdSum2 :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> Forall "b" Integer -> SBool))+dvdSum2 =+ calc "dvdSum2"+ (\(Forall d) (Forall a) (Forall b) -> d `dvd` (a + b) .&& d `dvd` b .=> d `dvd` a) $+ \d a b -> [d `dvd` (a + b) .&& d `dvd` b]+ |- cases [ d .== 0 ==> trivial+ , d ./= 0 ==> let k1 = (a + b) `sEDiv` d+ k2 = b `sEDiv` d+ in a `sEDiv` d+ =: (a + b - b) `sEDiv` d+ =: (k1 * d - k2 * d) `sEDiv` d+ =: (k1 - k2) * d `sEDiv` d+ =: qed+ ]++-- * Correctness of GCD++-- | \(\gcd\,a\,b \mid a \land \gcd\,a\,b \mid b\)+--+-- GCD of two numbers divide these numbers. This is part one of the proof, where we are+-- not concerned with maximality. Our goal is to show that the calculated gcd divides both inputs.+--+-- ==== __Proof__+-- >>> runTP gcdDivides+-- Lemma: dvdAbs Q.E.D.+-- Lemma: helper+-- Step: 1 Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma (strong): dvdNGCD+-- 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.Completeness Q.E.D.+-- Result: Q.E.D.+-- Lemma: gcdDivides Q.E.D.+-- [Proven] gcdDivides :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool+gcdDivides :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))+gcdDivides = do++ dAbs <- recall "dvdAbs" dvdAbs++ -- Helper about divisibility. If x|b and x| a%b, then x|a.+ helper <- calc "helper"+ (\(Forall @"a" a) (Forall @"b" b) (Forall @"x" x) ->+ b ./= 0 .&& x `dvd` b .&& x `dvd` (a `sEMod` b)+ .=> -----------------------------------------------+ x `dvd` a+ ) $+ \a b x -> [b ./= 0, x `dvd` b, x `dvd` (a `sEMod` b)]+ |- x `dvd` a+ ?? a `sEDiv` x .== (a `sEDiv` b) * (b `sEDiv` x) + (a `sEMod` b) `sEDiv` x+ =: sTrue+ =: qed++ -- Use strong induction to prove divisibility over non-negative numbers.+ dNGCD <- sInduct "dvdNGCD"+ (\(Forall @"a" a) (Forall @"b" b) -> a .>= 0 .&& b .>= 0 .=> nGCD a b `dvd` a .&& nGCD a b `dvd` b)+ (\_a b -> b) $+ \ih a b -> [a .>= 0, b .>= 0]+ |- let g = nGCD a b+ in g `dvd` a .&& g `dvd` b+ =: cases [ b .== 0 ==> trivial+ , b .> 0 ==> let g' = nGCD b (a `sEMod` b)+ in g' `dvd` a .&& g' `dvd` b+ ?? ih `at` (Inst @"a" b, Inst @"b" (a `sEMod` b))+ ?? helper+ =: sTrue+ =: qed+ ]++ -- Now generalize to arbitrary integers.+ lemma"gcdDivides"+ (\(Forall a) (Forall b) -> gcd a b `dvd` a .&& gcd a b `dvd` b)+ [proofOf dAbs, proofOf dNGCD]++-- | \(x \mid a \land x \mid b \implies x \mid \gcd\,a\,b\)+--+-- Maximality. Any divisor of the inputs divides the GCD.+--+-- ==== __Proof__+-- >>> runTP gcdMaximal+-- Lemma: dvdAbs Q.E.D.+-- Lemma: eDiv Q.E.D.+-- Lemma: helper+-- Step: 1 (x `dvd` a && x `dvd` b) Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma (strong): mNGCD+-- 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.Completeness Q.E.D.+-- Result: Q.E.D.+-- Lemma: gcdMaximal+-- Step: 1 (2 way case split)+-- Step: 1.1.1 Q.E.D.+-- Step: 1.1.2 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- [Proven] gcdMaximal :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐx ∷ Integer → Bool+gcdMaximal :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "x" Integer -> SBool))+gcdMaximal = do++ dAbs <- recall "dvdAbs" dvdAbs++ eDiv <- lemma "eDiv"+ (\(Forall @"x" x) (Forall @"y" y) -> y ./= 0 .=> x .== (x `sEDiv` y) * y + x `sEMod` y)+ []++ -- Helper: If x|a, x|b then x|a%b.+ helper <- calc "helper"+ (\(Forall @"a" a) (Forall @"b" b) (Forall @"x" x) ->+ x ./= 0 .&& b ./= 0 .&& x `dvd` a .&& x `dvd` b+ .=> -----------------------------------------------+ x `dvd` (a `sEMod` b)+ ) $+ \a b x -> [x ./= 0, b ./= 0, x `dvd` a, x `dvd` b]+ |- x `dvd` (a `sEMod` b)+ ?? "x `dvd` a && x `dvd` b"+ =: let k1 = a `sDiv` x+ k2 = b `sDiv` x+ in x `dvd` ((k1*x) `sEMod` (k2*x))+ ?? eDiv `at` (Inst @"x" (k1*x), Inst @"y" (k2*x))+ =: x `dvd` ((k1*x) - ((k1*x) `sEDiv` (k2*x)) * (k2*x))+ =: sTrue+ =: qed++ -- Now prove maximality for non-negative integers:+ mNGCD <- sInduct "mNGCD"+ (\(Forall @"a" a) (Forall @"b" b) (Forall @"x" x) ->+ a .>= 0 .&& b .>= 0 .&& x `dvd` a .&& x `dvd` b .=> x `dvd` nGCD a b)+ (\_a b _x -> b) $+ \ih a b x -> let g = nGCD a b+ in [a .>= 0, b .>= 0, x `dvd` a .&& x `dvd` b]+ |- x `dvd` g+ =: cases [ b .== 0 ==> trivial+ , b .> 0 ==> x `dvd` nGCD b (a `sEMod` b)+ ?? ih `at` (Inst @"a" b, Inst @"b" (a `sEMod` b), Inst @"x" x)+ ?? helper+ =: sTrue+ =: qed+ ]++ -- Generalize to arbitrary integers:+ calc "gcdMaximal"+ (\(Forall @"a" a) (Forall @"b" b) (Forall @"x" x) -> x `dvd` a .&& x `dvd` b .=> x `dvd` gcd a b) $+ \a b x -> [x `dvd` a, x `dvd` b]+ |- x `dvd` gcd a b+ =: cases [ abs a .>= abs b ==> x `dvd` nGCD (abs a) (abs b)+ ?? mNGCD `at` (Inst @"a" (abs a), Inst @"b" (abs b), Inst @"x" x)+ ?? dAbs `at` (Inst @"a" x, Inst @"b" a)+ ?? dAbs `at` (Inst @"a" x, Inst @"b" b)+ =: sTrue+ =: qed+ , abs a .< abs b ==> x `dvd` nGCD (abs b) (abs a)+ ?? mNGCD `at` (Inst @"a" (abs b), Inst @"b" (abs a), Inst @"x" x)+ ?? dAbs `at` (Inst @"a" x, Inst @"b" a)+ ?? dAbs `at` (Inst @"a" x, Inst @"b" b)+ =: sTrue+ =: qed+ ]++-- | \(\gcd\,a\,b \mid a \land \gcd\,a\,b \mid b \land (x \mid a \land x \mid b \implies x \mid \gcd\,a\,b)\)+--+-- Putting it all together: GCD divides both arguments, and its maximal.+--+-- ==== __Proof__+-- >>> runTP gcdCorrect+-- Lemma: gcdDivides Q.E.D.+-- Lemma: gcdMaximal Q.E.D.+-- Lemma: gcdCorrect+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Result: Q.E.D.+-- [Proven] gcdCorrect :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool+gcdCorrect :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))+gcdCorrect = do+ divides <- recall "gcdDivides" gcdDivides+ maximal <- recall "gcdMaximal" gcdMaximal++ calc "gcdCorrect"+ (\(Forall a) (Forall b) ->+ let g = gcd a b+ in g `dvd` a+ .&& g `dvd` b+ .&& quantifiedBool (\(Forall x) -> x `dvd` a .&& x `dvd` b .=> x `dvd` g)+ ) $+ \a b -> []+ |- let g = gcd a b+ m = quantifiedBool (\(Forall x) -> x `dvd` a .&& x `dvd` b .=> x `dvd` g)+ in g `dvd` a .&& g `dvd` b .&& m+ ?? divides `at` (Inst @"a" a, Inst @"b" b)+ =: m+ ?? maximal+ =: sTrue+ =: qed++-- | \(\bigl((a \neq 0 \lor b \neq 0) \land x \mid a \land x \mid b \bigr) \implies x \leq \gcd\,a\,b\)+--+-- Additionally prove that GCD is really maximum, i.e., it is the largest in the regular sense. Note+-- that we have to make an exception for @gcd 0 0@ since by definition the GCD is @0@, which is clearly+-- not the largest divisor of @0@ and @0@. (Since any number is a GCD for the pair @(0, 0)@, there is+-- no maximum.)+--+-- ==== __Proof__+-- >>> runTP gcdLargest+-- Lemma: gcdMaximal Q.E.D.+-- Lemma: gcdZero Q.E.D.+-- Lemma: gcdNonNegative Q.E.D.+-- Lemma: gcdLargest+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Result: Q.E.D.+-- [Proven] gcdLargest :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐx ∷ Integer → Bool+gcdLargest :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "x" Integer -> SBool))+gcdLargest = do+ maximal <- recall "gcdMaximal" gcdMaximal+ zero <- recall "gcdZero" gcdZero+ nn <- recall "gcdNonNegative" gcdNonNegative++ calc "gcdLargest"+ (\(Forall a) (Forall b) (Forall x) -> (a ./= 0 .|| b ./= 0) .&& x `dvd` a .&& x `dvd` b .=> x .<= gcd a b) $+ \a b x -> [(a ./= 0 .|| b ./= 0) .&& x `dvd` a, x `dvd` b]+ |- x .<= gcd a b+ ?? maximal `at` (Inst @"a" a, Inst @"b" b, Inst @"x" x)+ =: (x `dvd` gcd a b .=> x .<= gcd a b)+ ?? zero `at` (Inst @"a" a, Inst @"b" b)+ ?? nn `at` (Inst @"a" a, Inst @"b" b)+ =: sTrue+ =: qed++-- * Other GCD Facts++-- | \(\gcd\, a\, b = \gcd\, (a + b)\, b\)+--+-- ==== __Proof__+-- >>> runTP gcdAdd+-- Lemma: dvdSum1 Q.E.D.+-- Lemma: dvdSum2 Q.E.D.+-- Lemma: gcdDivides Q.E.D.+-- Lemma: gcdLargest Q.E.D.+-- Lemma: gcdAdd+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Step: 5 Q.E.D.+-- Step: 6 Q.E.D.+-- Step: 7 Q.E.D.+-- Result: Q.E.D.+-- [Proven] gcdAdd :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool+gcdAdd :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))+gcdAdd = do++ dSum1 <- recall "dvdSum1" dvdSum1+ dSum2 <- recall "dvdSum2" dvdSum2+ divides <- recall "gcdDivides" gcdDivides+ largest <- recall "gcdLargest" gcdLargest++ calc "gcdAdd"+ (\(Forall @"a" a) (Forall @"b" b) -> gcd a b .== gcd (a + b) b) $+ \a b -> [] |-> let g1 = gcd a b+ g2 = gcd (a + b) b+ in sTrue++ -- First use the divides property to conclude that g1 divides a and b+ ?? divides `at` (Inst @"a" a, Inst @"b" b)+ =: g1 `dvd` a .&& g1 `dvd` b++ -- Same for g2 for a+b and b+ ?? divides `at` (Inst @"a" (a + b), Inst @"b" b)+ =: g2 `dvd` (a+b) .&& g2 `dvd` b++ -- Use dSum1 to show g1 divides a+b+ ?? dSum1 `at` (Inst @"d" g1, Inst @"a" a, Inst @"b" b)+ =: g1 `dvd` (a+b)++ -- Similarly, use dSum2 to show g2 divides a+ ?? dSum2 `at` (Inst @"d" g2, Inst @"a" a, Inst @"b" b)+ =: g2 `dvd` a++ -- Now use largest to show g1 >= g2+ ?? largest `at` (Inst @"a" a, Inst @"b" b, Inst @"x" g2)+ =: g1 .>= g2++ -- But again via largest, we can show g2 >= g1+ ?? largest `at` (Inst @"a" (a+b), Inst @"b" b, Inst @"x" g1)+ =: g2 .>= g1++ -- Finally conclude g1 = g2, since both are greater-than-equal to each other:+ =: g1 .== g2+ =: qed++-- | \(\gcd\, (2a)\, (2b) = 2 (\gcd\,a\, b)\)+--+-- ==== __Proof__+-- >>> runTP gcdEvenEven+-- Lemma: modEE Q.E.D.+-- Inductive lemma (strong): nGCDEvenEven+-- 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.+-- Lemma: gcdEvenEven+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Result: Q.E.D.+-- [Proven] gcdEvenEven :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool+gcdEvenEven :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))+gcdEvenEven = do++ modEE <- lemma "modEE"+ (\(Forall @"a" a) (Forall @"b" b) -> b ./= 0 .=> (2 * a) `sEMod` (2 * b) .== 2 * (a `sEMod` b))+ []++ nGCDEvenEven <- sInduct "nGCDEvenEven"+ (\(Forall @"a" a) (Forall @"b" b) -> a .>= 0 .&& b .>= 0 .=> nGCD (2*a) (2*b) .== 2 * nGCD a b)+ (\_a b -> b) $+ \ih a b -> [a .>= 0, b .>= 0]+ |- nGCD (2*a) (2*b)+ =: cases [ b .== 0 ==> trivial+ , b ./= 0 ==> nGCD (2 * a) (2 * b)+ =: nGCD (2 * b) ((2 * a) `sEMod` (2 * b))+ ?? modEE `at` (Inst @"a" a, Inst @"b" b)+ =: nGCD (2 * b) (2 * (a `sEMod` b))+ ?? ih+ =: 2 * nGCD a b+ =: qed+ ]++ calc "gcdEvenEven"+ (\(Forall a) (Forall b) -> gcd (2*a) (2*b) .== 2 * gcd a b) $+ \a b -> [] |- gcd (2*a) (2*b)+ =: nGCD (abs (2*a)) (abs (2*b))+ =: nGCD (2 * abs a) (2 * abs b)+ ?? nGCDEvenEven `at` (Inst @"a" (abs a), Inst @"b" (abs b))+ =: 2 * nGCD (abs a) (abs b)+ =: 2 * gcd a b+ =: qed++-- | \(\gcd\, (2a+1)\, (2b) = \gcd\,(2a+1)\, b\)+--+-- ==== __Proof__+-- >>> runTP gcdOddEven+-- Lemma: gcdDivides Q.E.D.+-- Lemma: gcdLargest Q.E.D.+-- Lemma: dvdMul Q.E.D.+-- Lemma: dvdOddThenOdd Q.E.D.+-- Lemma: dvdEvenWhenOdd Q.E.D.+-- Lemma: gcdOddEven+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Step: 5 Q.E.D.+-- Step: 6 Q.E.D.+-- Step: 7 Q.E.D.+-- Step: 8 Q.E.D.+-- Result: Q.E.D.+-- [Proven] gcdOddEven :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool+gcdOddEven :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))+gcdOddEven = do++ divides <- recall "gcdDivides" gcdDivides+ largest <- recall "gcdLargest" gcdLargest+ dMul <- recall "dvdMul" dvdMul+ dOddThenOdd <- recall "dvdOddThenOdd" dvdOddThenOdd+ dEvenWhenOdd <- recall "dvdEvenWhenOdd" dvdEvenWhenOdd++ calc "gcdOddEven"+ (\(Forall a) (Forall b) -> gcd (2*a+1) (2*b) .== gcd (2*a+1) b) $+ \a b -> [] |-> let g1 = gcd (2*a+1) (2*b)+ g2 = gcd (2*a+1) b+ in sTrue++ -- First use the divides property to conclude that g1 divides both 2*a+1 and 2*b+ ?? divides `at` (Inst @"a" (2*a+1), Inst @"b" (2*b))+ =: g1 `dvd` (2*a+1) .&& g1 `dvd` (2*b)++ -- Same for g2, for 2*a+1 and b+ ?? divides `at` (Inst @"a" (2*a+1), Inst @"b" b)+ =: g2 `dvd` (2*a+1) .&& g2 `dvd` b++ -- By arithmetic, g2 divides 2*b+ ?? dMul `at` (Inst @"d" g2, Inst @"a" b, Inst @"k" 2)+ =: g2 `dvd` (2*b)++ -- Observe that g1 must be odd+ ?? dOddThenOdd `at` (Inst @"d" g1, Inst @"a" a)+ =: isOdd g1++ -- Conclude that g1 must divide b+ ?? dEvenWhenOdd `at` (Inst @"d" g1, Inst @"a" b)+ =: g1 `dvd` b++ -- Now use largest to show g1 >= g2+ ?? largest `at` (Inst @"a" (2*a+1), Inst @"b" (2*b), Inst @"x" g2)+ =: g1 .>= g2++ -- But again via largest, we can show g2 >= g1+ ?? largest `at` (Inst @"a" (2*a+1), Inst @"b" b, Inst @"x" g1)+ =: g2 .>= g1++ -- Finally conclude g1 = g2 since both are greater-than-equal to each other:+ =: g1 .== g2+ =: qed++-- * GCD via subtraction++-- | @nGCDSub@ is the original verision of Euclid, which uses subtraction instead of modulus. This is the version that+-- works on non-negative numbers. It has the precondition that @a >= b >= 0@, and maintains this invariant in each+-- recursive call.+nGCDSub :: SInteger -> SInteger -> SInteger+nGCDSub = smtFunction "nGCDSub" $ \a b -> ite (a .== b) a+ $ ite (a .== 0) b+ $ ite (b .== 0) a+ $ ite (a .> b) (nGCDSub (a - b) b)+ (nGCDSub a (b - a))++-- | Generalized version of subtraction based GCD, working over all integers.+gcdSub :: SInteger -> SInteger -> SInteger+gcdSub a b = nGCDSub (abs a) (abs b)++-- | \(\mathrm{gcdSub}\, a\, b = \gcd\, a\, b\)+--+-- Instead of proving @gcdSub@ correct, we'll simply show that it is equivalent to @gcd@, hence it has+-- all the properties we already established.+--+-- ==== __Proof__+-- >>> runTP gcdSubEquiv+-- Lemma: commutative Q.E.D.+-- Lemma: gcdAdd Q.E.D.+-- Inductive lemma (strong): nGCDSubEquiv+-- Step: Measure is non-negative Q.E.D.+-- Step: 1 (5 way case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2 Q.E.D.+-- Step: 1.3 Q.E.D.+-- Step: 1.4.1 Q.E.D.+-- Step: 1.4.2 Q.E.D.+-- Step: 1.4.3 Q.E.D.+-- Step: 1.5.1 Q.E.D.+-- Step: 1.5.2 Q.E.D.+-- Step: 1.5.3 Q.E.D.+-- Step: 1.5.4 Q.E.D.+-- Step: 1.5.5 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- Lemma: gcdSubEquiv+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Result: Q.E.D.+-- [Proven] gcdSubEquiv :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool+gcdSubEquiv :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))+gcdSubEquiv = do++ -- We'll be using the commutativity of GCD and the gcdAdd property+ comm <- recall "commutative" commutative+ addG <- recall "gcdAdd" gcdAdd++ -- First prove over the non-negative numbers:+ nEq <- sInduct "nGCDSubEquiv"+ (\(Forall @"a" a) (Forall @"b" b) -> a .>= 0 .&& b .>= 0 .=> nGCDSub a b .== nGCD a b)+ (\a b -> a + b) $+ \ih a b -> [a .>= 0, b .>= 0]+ |- nGCDSub a b+ =: cases [ a .== b ==> nGCD a b =: qed+ , a .== 0 ==> nGCD a b =: qed+ , b .== 0 ==> nGCD a b =: qed+ , a .> b .&& b ./= 0 ==> nGCDSub (a - b) b+ ?? ih+ =: nGCD (a - b) b+ ?? addG `at` (Inst @"a" (a - b), Inst @"b" b)+ =: nGCD a b+ =: qed+ , a .< b .&& a ./= 0 ==> nGCDSub a (b - a)+ ?? ih+ =: nGCD a (b - a)+ ?? comm+ =: nGCD (b - a) a+ ?? addG `at` (Inst @"a" (b - a), Inst @"b" a)+ =: nGCD b a+ ?? comm+ =: nGCD a b+ =: qed+ ]++ -- Now prove over all integers+ calcWith cvc5 "gcdSubEquiv"+ (\(Forall a) (Forall b) -> gcd a b .== gcdSub a b) $+ \a b -> [] |- gcd a b+ =: nGCD (abs a) (abs b)+ ?? nEq `at` (Inst @"a" (abs a), Inst @"b" (abs b))+ =: nGCDSub (abs a) (abs b)+ =: gcdSub a b+ =: qed++-- * Binary GCD++-- | @nGCDBin@ is the binary GCD algorithm that works on non-negative numbers.+nGCDBin :: SInteger -> SInteger -> SInteger+nGCDBin = smtFunction "nGCDBin" $ \a b -> ite (a .== 0) b+ $ ite (b .== 0) a+ $ ite (isEven a .&& isEven b) (2 * nGCDBin (a `sEDiv` 2) (b `sEDiv` 2))+ $ ite (isOdd a .&& isEven b) ( nGCDBin a (b `sEDiv` 2))+ $ ite (a .<= b) ( nGCDBin a (b - a))+ ( nGCDBin (a - b) b)+-- | Generalized version that works on arbitrary integers.+gcdBin :: SInteger -> SInteger -> SInteger+gcdBin a b = nGCDBin (abs a) (abs b)++-- | \(\mathrm{gcdBin}\, a\, b = \gcd\, a\, b\)+--+-- Instead of proving @gcdBin@ correct, we'll simply show that it is equivalent to @gcd@, hence it has+-- all the properties we already established.+--+-- ==== __Proof__+-- >>> runTP gcdBinEquiv+-- Lemma: gcdEvenEven Q.E.D.+-- Lemma: gcdOddEven Q.E.D.+-- Lemma: gcdAdd Q.E.D.+-- Lemma: commutative Q.E.D.+-- Inductive lemma (strong): nGCDBinEquiv+-- Step: Measure is non-negative Q.E.D.+-- Step: 1 (5 way case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2 Q.E.D.+-- Step: 1.3.1 Q.E.D.+-- Step: 1.3.2 Q.E.D.+-- Step: 1.3.3 Q.E.D.+-- Step: 1.4.1 Q.E.D.+-- Step: 1.4.2 Q.E.D.+-- Step: 1.4.3 Q.E.D.+-- Step: 1.5 (3 way case split)+-- Step: 1.5.1 Q.E.D.+-- Step: 1.5.2.1 Q.E.D.+-- Step: 1.5.2.2 Q.E.D.+-- Step: 1.5.2.3 Q.E.D.+-- Step: 1.5.2.4 Q.E.D.+-- Step: 1.5.2.5 Q.E.D.+-- Step: 1.5.2.6 Q.E.D.+-- Step: 1.5.3.1 Q.E.D.+-- Step: 1.5.3.2 Q.E.D.+-- Step: 1.5.3.3 Q.E.D.+-- Step: 1.5.3.4 Q.E.D.+-- Step: 1.5.Completeness Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- Lemma: gcdBinEquiv+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Result: Q.E.D.+-- [Proven] gcdBinEquiv :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool+gcdBinEquiv :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))+gcdBinEquiv = do+ gEvenEven <- recall "gcdEvenEven" gcdEvenEven+ gOddEven <- recall "gcdOddEven" gcdOddEven+ gAdd <- recall "gcdAdd" gcdAdd+ comm <- recall "commutative" commutative++ -- First prove over the non-negative numbers:+ nEq <- sInduct "nGCDBinEquiv"+ (\(Forall @"a" a) (Forall @"b" b) -> a .>= 0 .&& b .>= 0 .=> nGCDBin a b .== nGCD a b)+ (\a b -> tuple (a, b)) $+ \ih a b -> [a .>= 0, b .>= 0]+ |- nGCDBin a b+ =: cases [ a .== 0 ==> trivial+ , b .== 0 ==> trivial+ , isEven a .&& isEven b ==> 2 * nGCDBin (a `sEDiv` 2) (b `sEDiv` 2)+ ?? ih `at` (Inst @"a" (a `sEDiv` 2), Inst @"b" (b `sEDiv` 2))+ =: 2 * nGCD (a `sEDiv` 2) (b `sEDiv` 2)+ ?? a .== 2 * a `sEDiv` 2+ ?? b .== 2 * b `sEDiv` 2+ ?? gEvenEven `at` (Inst @"a" (a `sEDiv` 2), Inst @"b" (b `sEDiv` 2))+ =: nGCD a b+ =: qed+ , isOdd a .&& isEven b ==> nGCDBin a (b `sEDiv` 2)+ ?? ih `at` (Inst @"a" a, Inst @"b" (b `sEDiv` 2))+ =: nGCD a (b `sEDiv` 2)+ ?? a .== 2 * ((a-1) `sEDiv` 2) + 1+ ?? b .== 2 * b `sEDiv` 2+ ?? gOddEven `at` (Inst @"a" ((a-1) `sEDiv` 2), Inst @"b" (b `sEDiv` 2))+ =: nGCD a b+ =: qed+ , isOdd b ==> cases [ a .== 0 ==> trivial+ , a ./= 0 .&& a .<= b ==> nGCDBin a b+ =: nGCDBin a (b - a)+ ?? ih `at` (Inst @"a" a, Inst @"b" (b - a))+ =: nGCD a (b - a)+ ?? comm `at` (Inst @"a" a, Inst @"b" (b - a))+ =: nGCD (b - a) a+ ?? gAdd `at` (Inst @"a" (b - a), Inst @"b" a)+ =: nGCD b a+ ?? comm `at` (Inst @"a" b, Inst @"b" a)+ =: nGCD a b+ =: qed+ , a .> b ==> nGCDBin a b+ =: nGCDBin (a - b) b+ ?? ih `at` (Inst @"a" (a - b), Inst @"b" b)+ =: nGCD (a - b) b+ ?? gAdd `at` (Inst @"a" a, Inst @"b" (-b))+ =: nGCD a b+ =: qed+ ]+ ]++ -- Now prove over all integers+ calcWith cvc5 "gcdBinEquiv"+ (\(Forall a) (Forall b) -> gcd a b .== gcdBin a b) $+ \a b -> [] |- gcd a b+ =: nGCD (abs a) (abs b)+ ?? nEq `at` (Inst @"a" (abs a), Inst @"b" (abs b))+ =: nGCDBin (abs a) (abs b)+ =: gcdBin a b+ =: qed++{- HLint ignore gcdSubEquiv "Avoid lambda" -}+{- HLint ignore gcdBinEquiv "Use curry" -}
Documentation/SBV/Examples/TP/InsertionSort.hs view
@@ -11,6 +11,7 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedLists #-} {-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeApplications #-}@@ -36,13 +37,13 @@ -- * Insertion sort -- | Insert an element into an already sorted list in the correct place.-insert :: (Ord a, SymVal a) => SBV a -> SList a -> SList a+insert :: (OrdSymbolic (SBV a), SymVal a) => SBV a -> SList a -> SList a insert = smtFunction "insert" $ \e l -> ite (null l) [e] $ let (x, xs) = uncons l in ite (e .<= x) (e .: x .: xs) (x .: insert e xs) -- | Insertion sort, using 'insert' above to successively insert the elements.-insertionSort :: (Ord a, SymVal a) => SList a -> SList a+insertionSort :: (OrdSymbolic (SBV a), SymVal a) => SList a -> SList a insertionSort = smtFunction "insertionSort" $ \l -> ite (null l) nil $ let (x, xs) = uncons l in insert x (insertionSort xs)@@ -110,7 +111,7 @@ -- Result: Q.E.D. -- Lemma: insertionSortIsCorrect Q.E.D. -- [Proven] insertionSortIsCorrect :: Ɐxs ∷ [Integer] → Bool-correctness :: forall a. (Ord a, SymVal a) => IO (Proof (Forall "xs" [a] -> SBool))+correctness :: forall a. (OrdSymbolic (SBV a), Eq a, SymVal a) => IO (Proof (Forall "xs" [a] -> SBool)) correctness = runTPWith (tpRibbon 45 cvc5) $ do --------------------------------------------------------------------------------------------
Documentation/SBV/Examples/TP/Majority.hs view
@@ -102,15 +102,15 @@ -- Helper definition let isMajority :: SBV a -> SList a -> SBool- isMajority e xs = length xs `sEDiv` 2 .< TP.count e xs+ isMajority e xs = length xs `sEDiv` 2 .< howMany e xs -- First prove the generalized majority theorem majorityGeneral <- induct "majorityGeneral" (\(Forall @"xs" xs) (Forall @"i" i) (Forall @"e" (e :: SBV a)) (Forall @"c" c)- -> i .>= 0 .&& (length xs + i) `sEDiv` 2 .< ite (e .== c) i 0 + TP.count e xs .=> majority c i xs .== e) $+ -> i .>= 0 .&& (length xs + i) `sEDiv` 2 .< ite (e .== c) i 0 + howMany e xs .=> majority c i xs .== e) $ \ih (x, xs) i e c ->- [i .>= 0, (length (x .: xs) + i) `sEDiv` 2 .< ite (e .== c) i 0 + TP.count e (x .: xs)]+ [i .>= 0, (length (x .: xs) + i) `sEDiv` 2 .< ite (e .== c) i 0 + howMany e (x .: xs)] |- majority c i (x .: xs) =: cases [ i .== 0 ==> majority x 1 xs ?? ih `at` (Inst @"i" 1, Inst @"e" e, Inst @"c" x)
Documentation/SBV/Examples/TP/MergeSort.hs view
@@ -11,6 +11,7 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedLists #-} {-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeApplications #-}@@ -38,7 +39,7 @@ -- * Merge sort -- | Merge two already sorted lists into another-merge :: (Ord a, SymVal a) => SList a -> SList a -> SList a+merge :: (OrdSymbolic (SBV a), SymVal a) => SList a -> SList a -> SList a merge = smtFunction "merge" $ \l r -> ite (null l) r $ ite (null r) l $ let (a, as) = uncons l@@ -46,7 +47,7 @@ in ite (a .<= b) (a .: merge as r) (b .: merge l bs) -- | Merge sort, using 'merge' above to successively sort halved input-mergeSort :: (Ord a, SymVal a) => SList a -> SList a+mergeSort :: (OrdSymbolic (SBV a), SymVal a) => SList a -> SList a mergeSort = smtFunction "mergeSort" $ \l -> ite (length l .<= 1) l $ let (h1, h2) = splitAt (length l `sEDiv` 2) l in merge (mergeSort h1) (mergeSort h2)@@ -121,7 +122,7 @@ -- Result: Q.E.D. -- Lemma: mergeSortIsCorrect Q.E.D. -- [Proven] mergeSortIsCorrect :: Ɐxs ∷ [Integer] → Bool-correctness :: forall a. (Ord a, SymVal a) => IO (Proof (Forall "xs" [a] -> SBool))+correctness :: forall a. (OrdSymbolic (SBV a), SymVal a) => IO (Proof (Forall "xs" [a] -> SBool)) correctness = runTPWith (tpRibbon 60 z3) $ do --------------------------------------------------------------------------------------------
Documentation/SBV/Examples/TP/QuickSort.hs view
@@ -14,6 +14,7 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedLists #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeAbstractions #-}@@ -42,7 +43,7 @@ -- * Quick sort -- | Quick-sort, using the first element as pivot.-quickSort :: (Ord a, SymVal a) => SList a -> SList a+quickSort :: (OrdSymbolic (SBV a), SymVal a) => SList a -> SList a quickSort = smtFunction "quickSort" $ \l -> ite (null l) nil (let (x, xs) = uncons l@@ -52,7 +53,7 @@ -- | We define @partition@ as an explicit function. Unfortunately, we can't just replace this -- with @\pivot xs -> Data.List.SBV.partition (.< pivot) xs@ because that would create a firstified version of partition -- with a free-variable captured, which isn't supported due to higher-order limitations in SMTLib.-partition :: (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]+partition :: (OrdSymbolic (SBV a), SymVal a) => SBV a -> SList a -> STuple [a] [a] partition = smtFunction "partition" $ \pivot xs -> ite (null xs) (tuple (nil, nil)) (let (a, as) = uncons xs@@ -135,9 +136,10 @@ -- Result: Q.E.D. -- Inductive lemma: partitionFstLT -- Step: Base Q.E.D.--- Step: 1 Q.E.D.--- Step: 2 (push llt down) Q.E.D.--- Step: 3 Q.E.D.+-- Step: 1 (unroll partition) Q.E.D.+-- Step: 2 (push fst down, simplify) Q.E.D.+-- Step: 3 (push llt down) Q.E.D.+-- Step: 4 Q.E.D. -- Result: Q.E.D. -- Inductive lemma: partitionSndGE -- Step: Base Q.E.D.@@ -195,6 +197,10 @@ -- 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.2.5 Q.E.D.+-- Step: 1.2.6 Q.E.D.+-- Step: 1.2.7 Q.E.D. -- Result: Q.E.D. -- Inductive lemma (strong): sortIsNonDecreasing -- Step: Measure is non-negative Q.E.D.@@ -256,7 +262,7 @@ -- │ └╴sublistIfPerm -- └╴nonDecreasingMerge -- [Proven] quickSortIsCorrect :: Ɐxs ∷ [Integer] → Bool-correctness :: forall a. (Ord a, SymVal a) => IO (Proof (Forall "xs" [a] -> SBool))+correctness :: forall a. (Eq a, OrdSymbolic (SBV a), SymVal a) => IO (Proof (Forall "xs" [a] -> SBool)) correctness = runTPWith (tpRibbon 60 z3) $ do --------------------------------------------------------------------------------------------@@ -369,13 +375,15 @@ partitionFstLT <- inductWith cvc5 "partitionFstLT" (\(Forall l) (Forall pivot) -> llt pivot (fst (partition pivot l))) $ \ih (a, as) pivot -> [] |- llt pivot (fst (partition pivot (a .: as)))- =: llt pivot (ite (a .< pivot)- (a .: fst (partition pivot as))- ( fst (partition pivot as)))+ ?? "unroll partition"+ =: let (lo, hi) = untuple (partition pivot as)+ in llt pivot (fst (ite (a .< pivot)+ (tuple (a .: lo, hi))+ (tuple (lo, a .: hi))))+ ?? "push fst down, simplify"+ =: llt pivot (ite (a .< pivot) (a .: lo) lo) ?? "push llt down"- =: ite (a .< pivot)- (a .< pivot .&& llt pivot (fst (partition pivot as)))- ( llt pivot (fst (partition pivot as)))+ =: ite (a .< pivot) (llt pivot (a .: lo)) (llt pivot lo) ?? ih =: sTrue =: qed@@ -520,8 +528,14 @@ [nonDecreasing (x .: xs), llt pivot xs, nonDecreasing ys, lge pivot ys] |- nonDecreasing (x .: xs ++ [pivot] ++ ys) =: split xs trivial- (\a as -> nonDecreasing (x .: a .: as ++ [pivot] ++ ys)- =: x .<= a .&& nonDecreasing (a .: as ++ [pivot] ++ ys)+ (\a as -> nonDecreasing (x .: (a .: as) ++ [pivot] ++ ys)+ =: nonDecreasing (x .: a .: (as ++ [pivot] ++ ys))+ =: x .<= a .&& nonDecreasing (a .: (as ++ [pivot] ++ ys))+ =: nonDecreasing (a .: (as ++ [pivot] ++ ys))+ =: nonDecreasing ((a .: as) ++ [pivot] ++ ys)+ =: nonDecreasing (xs ++ [pivot] ++ ys)+ -- This hint shouldn't be necessary, but it makes the proof go faster!+ ?? nonDecreasing xs ?? ih =: sTrue =: qed)
Documentation/SBV/Examples/TP/Reverse.hs view
@@ -36,6 +36,7 @@ #ifdef DOCTEST -- $setup -- >>> :set -XTypeApplications+-- >>> import Data.SBV.TP #endif -- * Reversing with no auxiliaries@@ -53,46 +54,11 @@ -- | Correctness the function 'rev'. We have: ----- >>> correctness @Integer--- Inductive lemma: revLen--- Step: Base Q.E.D.--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Step: 3 Q.E.D.--- Step: 4 Q.E.D.--- Result: Q.E.D.--- Inductive lemma: revApp--- Step: Base Q.E.D.--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Step: 3 Q.E.D.--- Step: 4 Q.E.D.--- Step: 5 Q.E.D.--- Result: Q.E.D.--- Inductive lemma: revApp--- Step: Base Q.E.D.--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Step: 3 Q.E.D.--- Step: 4 Q.E.D.--- Step: 5 Q.E.D.--- Result: Q.E.D.+-- >>> runTP $ correctness @Integer+-- Lemma: revLen Q.E.D.+-- Lemma: revApp Q.E.D. -- Lemma: revSnoc Q.E.D.--- Inductive lemma: revApp--- Step: Base Q.E.D.--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Step: 3 Q.E.D.--- Step: 4 Q.E.D.--- Step: 5 Q.E.D.--- Result: Q.E.D.--- Inductive lemma: revRev--- Step: Base Q.E.D.--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Step: 3 Q.E.D.--- Step: 4 Q.E.D.--- Result: Q.E.D.+-- Lemma: revRev Q.E.D. -- Inductive lemma (strong): revCorrect -- Step: Measure is non-negative Q.E.D. -- Step: 1 (2 way full case split)@@ -103,26 +69,27 @@ -- Step: 1.2.2.2 Q.E.D. -- Step: 1.2.2.3 Q.E.D. -- Step: 1.2.2.4 Q.E.D.--- Step: 1.2.2.5 (simplify head) Q.E.D.--- Step: 1.2.2.6 Q.E.D.--- Step: 1.2.2.7 (simplify tail) Q.E.D.--- Step: 1.2.2.8 Q.E.D.+-- Step: 1.2.2.5 Q.E.D.+-- Step: 1.2.2.6 (simplify head) Q.E.D.+-- Step: 1.2.2.7 Q.E.D.+-- Step: 1.2.2.8 (simplify tail) Q.E.D. -- Step: 1.2.2.9 Q.E.D. -- Step: 1.2.2.10 Q.E.D.--- Step: 1.2.2.11 (substitute) Q.E.D.--- Step: 1.2.2.12 Q.E.D.+-- Step: 1.2.2.11 Q.E.D.+-- Step: 1.2.2.12 (substitute) Q.E.D. -- Step: 1.2.2.13 Q.E.D. -- Step: 1.2.2.14 Q.E.D.+-- Step: 1.2.2.15 Q.E.D. -- Result: Q.E.D. -- [Proven] revCorrect :: Ɐxs ∷ [Integer] → Bool-correctness :: forall a. SymVal a => IO (Proof (Forall "xs" [a] -> SBool))-correctness = runTP $ do+correctness :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))+correctness = do - -- Import a few helpers from "Data.SBV.TP.List"- revLen <- TP.revLen @a- revApp <- TP.revApp @a- revSnoc <- TP.revSnoc @a- revRev <- TP.revRev @a+ -- Quietly import a few helpers from "Data.SBV.TP.List"+ revLen <- recall "revLen" $ TP.revLen @a+ revApp <- recall "revApp" $ TP.revApp @a+ revSnoc <- recall "revSnoc" $ TP.revSnoc @a+ revRev <- recall "revRev" $ TP.revRev @a sInductWith cvc5 "revCorrect" (\(Forall xs) -> rev xs .== reverse xs)@@ -132,6 +99,8 @@ (\a as -> split as trivial (\_ _ -> head (rev as) .: rev (a .: rev (tail (rev as))) ?? ih `at` Inst @"xs" as+ =: head (reverse as) .: rev (a .: rev (tail (rev as)))+ ?? ih `at` Inst @"xs" as =: head (reverse as) .: rev (a .: rev (tail (reverse as))) ?? ih `at` Inst @"xs" (tail (rev as)) =: head (reverse as) .: rev (a .: rev (tail (reverse as)))@@ -154,7 +123,7 @@ =: b .: reverse (a .: w) ?? "substitute" =: last as .: reverse (a .: init as)- ?? revApp `at` (Inst @"xs" (init as), Inst @"ys" [last as])+ ?? revApp `at` (Inst @"xs" (a .: init as), Inst @"ys" [last as]) =: reverse (a .: init as ++ [last as]) =: reverse (a .: as) =: reverse xs
Documentation/SBV/Examples/TP/SortHelpers.hs view
@@ -11,6 +11,7 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -33,7 +34,7 @@ #endif -- | A predicate testing whether a given list is non-decreasing.-nonDecreasing :: (Ord a, SymVal a) => SList a -> SBool+nonDecreasing :: (OrdSymbolic (SBV a), SymVal a) => SList a -> SBool nonDecreasing = smtFunction "nonDecreasing" $ \l -> null l .|| null (tail l) .|| let (x, l') = uncons l (y, _) = uncons l'@@ -48,7 +49,7 @@ -- >>> runTP $ nonDecrTail @Integer -- Lemma: nonDecrTail Q.E.D. -- [Proven] nonDecrTail :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool-nonDecrTail :: forall a. (Ord a, SymVal a) => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))+nonDecrTail :: forall a. (OrdSymbolic (SBV a), SymVal a) => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool)) nonDecrTail = lemma "nonDecrTail" (\(Forall x) (Forall xs) -> nonDecreasing (x .: xs) .=> nonDecreasing xs) []@@ -58,7 +59,7 @@ -- >>> runTP $ nonDecrIns @Integer -- Lemma: nonDecrInsert Q.E.D. -- [Proven] nonDecrInsert :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool-nonDecrIns :: forall a. (Ord a, SymVal a) => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))+nonDecrIns :: forall a. (OrdSymbolic (SBV a), SymVal a) => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool)) nonDecrIns = lemma "nonDecrInsert" (\(Forall x) (Forall xs) -> nonDecreasing xs .&& sNot (null xs) .&& x .<= head xs .=> nonDecreasing (x .: xs)) []
Documentation/SBV/Examples/TP/Sqrt2IsIrrational.hs view
@@ -36,12 +36,12 @@ -- Using these helpers, we can argue: -- -- (4) Start with the premise @a^2 = 2b^2@.--- (5) Thus, @a^2@ must be even. (Since it equals @2b^2@ by 4.)--- (6) Thus, @a@ must be even. (Using 2 and 5.)--- (7) Thus, @a^2@ must be divisible by @4@. (Using 3 and 6. That is, @2b^2 == 4K@ for some @K@.)--- (8) Thus, @b^2@ must be even. (Using 7, and @b^2 = 2K@.)--- (9) Thus, @b@ must be even. (Using 2 and 8.)--- (10) Since @a@ and @b@ are both even, they cannot be co-prime. (Using 6 and 9.)+-- (5) Thus, @a^2@ must be even. (Since it equals @2b^2@ by (4).)+-- (6) Thus, @a@ must be even. (Using (2) and (5).)+-- (7) Thus, @a^2@ must be divisible by @4@. (Using (3) and (6). That is, @2b^2 == 4K@ for some @K@.)+-- (8) Thus, @b^2@ must be even. (Using (7), and @b^2 = 2K@.)+-- (9) Thus, @b@ must be even. (Using (2) and (8).)+-- (10) Since @a@ and @b@ are both even, they cannot be co-prime. (Using (6) and (9).) -- -- Note that our proof is mostly about the first 3 facts above, then z3 and TP fills in the rest. --
README.md view
@@ -181,6 +181,7 @@ Adam Foltzer, Joshua Gancher, Remy Goldschmidt,+Jan Grant, Brad Hardy, Tom Hawkins, Greg Horn,
SBVTestSuite/GoldFiles/doctest_sanity.gold view
@@ -1,3 +1,3 @@-Total: 998; Tried: 998; Skipped: 0; Success: 998; Errors: 0; Failures 0-Examples: 890; Tried: 890; Skipped: 0; Success: 890; Errors: 0; Failures 0-Setup: 108; Tried: 108; Skipped: 0; Success: 108; Errors: 0; Failures 0+Total: 1020; Tried: 1020; Skipped: 0; Success: 1020; Errors: 0; Failures 0+Examples: 910; Tried: 910; Skipped: 0; Success: 910; Errors: 0; Failures 0+Setup: 110; Tried: 110; Skipped: 0; Success: 110; Errors: 0; Failures 0
SBVTestSuite/GoldFiles/queryArrays12.gold view
@@ -22,41 +22,6 @@ [GOOD] (define-fun sbv.rat.notEq ((x SBVRational) (y SBVRational)) Bool (not (sbv.rat.eq x y)) )--[GOOD] (define-fun sbv.rat.lt ((x SBVRational) (y SBVRational)) Bool- (< (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- )--[GOOD] (define-fun sbv.rat.leq ((x SBVRational) (y SBVRational)) Bool- (<= (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- )--[GOOD] (define-fun sbv.rat.plus ((x SBVRational) (y SBVRational)) SBVRational- (SBV.Rational (+ (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- (* (sbv.rat.denominator x) (sbv.rat.denominator y)))- )--[GOOD] (define-fun sbv.rat.minus ((x SBVRational) (y SBVRational)) SBVRational- (SBV.Rational (- (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- (* (sbv.rat.denominator x) (sbv.rat.denominator y)))- )--[GOOD] (define-fun sbv.rat.times ((x SBVRational) (y SBVRational)) SBVRational- (SBV.Rational (* (sbv.rat.numerator x) (sbv.rat.numerator y))- (* (sbv.rat.denominator x) (sbv.rat.denominator y)))- )--[GOOD] (define-fun sbv.rat.uneg ((x SBVRational)) SBVRational- (SBV.Rational (* (- 1) (sbv.rat.numerator x)) (sbv.rat.denominator x))- )--[GOOD] (define-fun sbv.rat.abs ((x SBVRational)) SBVRational- (SBV.Rational (abs (sbv.rat.numerator x)) (sbv.rat.denominator x))- ) [GOOD] ; --- literal constants --- [GOOD] ; --- top level inputs --- [GOOD] (declare-fun s0 () (Array SBVRational Int)) ; tracks user variable "x"
SBVTestSuite/GoldFiles/queryArrays13.gold view
@@ -22,41 +22,6 @@ [GOOD] (define-fun sbv.rat.notEq ((x SBVRational) (y SBVRational)) Bool (not (sbv.rat.eq x y)) )--[GOOD] (define-fun sbv.rat.lt ((x SBVRational) (y SBVRational)) Bool- (< (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- )--[GOOD] (define-fun sbv.rat.leq ((x SBVRational) (y SBVRational)) Bool- (<= (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- )--[GOOD] (define-fun sbv.rat.plus ((x SBVRational) (y SBVRational)) SBVRational- (SBV.Rational (+ (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- (* (sbv.rat.denominator x) (sbv.rat.denominator y)))- )--[GOOD] (define-fun sbv.rat.minus ((x SBVRational) (y SBVRational)) SBVRational- (SBV.Rational (- (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- (* (sbv.rat.denominator x) (sbv.rat.denominator y)))- )--[GOOD] (define-fun sbv.rat.times ((x SBVRational) (y SBVRational)) SBVRational- (SBV.Rational (* (sbv.rat.numerator x) (sbv.rat.numerator y))- (* (sbv.rat.denominator x) (sbv.rat.denominator y)))- )--[GOOD] (define-fun sbv.rat.uneg ((x SBVRational)) SBVRational- (SBV.Rational (* (- 1) (sbv.rat.numerator x)) (sbv.rat.denominator x))- )--[GOOD] (define-fun sbv.rat.abs ((x SBVRational)) SBVRational- (SBV.Rational (abs (sbv.rat.numerator x)) (sbv.rat.denominator x))- ) [GOOD] ; --- literal constants --- [GOOD] ; --- top level inputs --- [GOOD] (declare-fun s0 () (Array Int SBVRational)) ; tracks user variable "x"
SBVTestSuite/GoldFiles/queryArrays14.gold view
@@ -22,41 +22,6 @@ [GOOD] (define-fun sbv.rat.notEq ((x SBVRational) (y SBVRational)) Bool (not (sbv.rat.eq x y)) )--[GOOD] (define-fun sbv.rat.lt ((x SBVRational) (y SBVRational)) Bool- (< (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- )--[GOOD] (define-fun sbv.rat.leq ((x SBVRational) (y SBVRational)) Bool- (<= (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- )--[GOOD] (define-fun sbv.rat.plus ((x SBVRational) (y SBVRational)) SBVRational- (SBV.Rational (+ (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- (* (sbv.rat.denominator x) (sbv.rat.denominator y)))- )--[GOOD] (define-fun sbv.rat.minus ((x SBVRational) (y SBVRational)) SBVRational- (SBV.Rational (- (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- (* (sbv.rat.denominator x) (sbv.rat.denominator y)))- )--[GOOD] (define-fun sbv.rat.times ((x SBVRational) (y SBVRational)) SBVRational- (SBV.Rational (* (sbv.rat.numerator x) (sbv.rat.numerator y))- (* (sbv.rat.denominator x) (sbv.rat.denominator y)))- )--[GOOD] (define-fun sbv.rat.uneg ((x SBVRational)) SBVRational- (SBV.Rational (* (- 1) (sbv.rat.numerator x)) (sbv.rat.denominator x))- )--[GOOD] (define-fun sbv.rat.abs ((x SBVRational)) SBVRational- (SBV.Rational (abs (sbv.rat.numerator x)) (sbv.rat.denominator x))- ) [GOOD] ; --- literal constants --- [GOOD] ; --- top level inputs --- [GOOD] (declare-fun s0 () (Array SBVRational SBVRational)) ; tracks user variable "x"
SBVTestSuite/GoldFiles/queryArrays15.gold view
@@ -22,41 +22,6 @@ [GOOD] (define-fun sbv.rat.notEq ((x SBVRational) (y SBVRational)) Bool (not (sbv.rat.eq x y)) )--[GOOD] (define-fun sbv.rat.lt ((x SBVRational) (y SBVRational)) Bool- (< (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- )--[GOOD] (define-fun sbv.rat.leq ((x SBVRational) (y SBVRational)) Bool- (<= (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- )--[GOOD] (define-fun sbv.rat.plus ((x SBVRational) (y SBVRational)) SBVRational- (SBV.Rational (+ (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- (* (sbv.rat.denominator x) (sbv.rat.denominator y)))- )--[GOOD] (define-fun sbv.rat.minus ((x SBVRational) (y SBVRational)) SBVRational- (SBV.Rational (- (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- (* (sbv.rat.denominator x) (sbv.rat.denominator y)))- )--[GOOD] (define-fun sbv.rat.times ((x SBVRational) (y SBVRational)) SBVRational- (SBV.Rational (* (sbv.rat.numerator x) (sbv.rat.numerator y))- (* (sbv.rat.denominator x) (sbv.rat.denominator y)))- )--[GOOD] (define-fun sbv.rat.uneg ((x SBVRational)) SBVRational- (SBV.Rational (* (- 1) (sbv.rat.numerator x)) (sbv.rat.denominator x))- )--[GOOD] (define-fun sbv.rat.abs ((x SBVRational)) SBVRational- (SBV.Rational (abs (sbv.rat.numerator x)) (sbv.rat.denominator x))- ) [GOOD] ; --- literal constants --- [GOOD] ; --- top level inputs --- [GOOD] (declare-fun s0 () (Array SBVRational String)) ; tracks user variable "x"
SBVTestSuite/GoldFiles/queryArrays16.gold view
@@ -22,41 +22,6 @@ [GOOD] (define-fun sbv.rat.notEq ((x SBVRational) (y SBVRational)) Bool (not (sbv.rat.eq x y)) )--[GOOD] (define-fun sbv.rat.lt ((x SBVRational) (y SBVRational)) Bool- (< (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- )--[GOOD] (define-fun sbv.rat.leq ((x SBVRational) (y SBVRational)) Bool- (<= (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- )--[GOOD] (define-fun sbv.rat.plus ((x SBVRational) (y SBVRational)) SBVRational- (SBV.Rational (+ (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- (* (sbv.rat.denominator x) (sbv.rat.denominator y)))- )--[GOOD] (define-fun sbv.rat.minus ((x SBVRational) (y SBVRational)) SBVRational- (SBV.Rational (- (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- (* (sbv.rat.denominator x) (sbv.rat.denominator y)))- )--[GOOD] (define-fun sbv.rat.times ((x SBVRational) (y SBVRational)) SBVRational- (SBV.Rational (* (sbv.rat.numerator x) (sbv.rat.numerator y))- (* (sbv.rat.denominator x) (sbv.rat.denominator y)))- )--[GOOD] (define-fun sbv.rat.uneg ((x SBVRational)) SBVRational- (SBV.Rational (* (- 1) (sbv.rat.numerator x)) (sbv.rat.denominator x))- )--[GOOD] (define-fun sbv.rat.abs ((x SBVRational)) SBVRational- (SBV.Rational (abs (sbv.rat.numerator x)) (sbv.rat.denominator x))- ) [GOOD] ; --- literal constants --- [GOOD] ; --- top level inputs --- [GOOD] (declare-fun s0 () (Array String SBVRational)) ; tracks user variable "x"
SBVTestSuite/GoldFiles/queryArrays17.gold view
@@ -25,41 +25,6 @@ [GOOD] (define-fun sbv.rat.notEq ((x SBVRational) (y SBVRational)) Bool (not (sbv.rat.eq x y)) )--[GOOD] (define-fun sbv.rat.lt ((x SBVRational) (y SBVRational)) Bool- (< (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- )--[GOOD] (define-fun sbv.rat.leq ((x SBVRational) (y SBVRational)) Bool- (<= (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- )--[GOOD] (define-fun sbv.rat.plus ((x SBVRational) (y SBVRational)) SBVRational- (SBV.Rational (+ (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- (* (sbv.rat.denominator x) (sbv.rat.denominator y)))- )--[GOOD] (define-fun sbv.rat.minus ((x SBVRational) (y SBVRational)) SBVRational- (SBV.Rational (- (* (sbv.rat.numerator x) (sbv.rat.denominator y))- (* (sbv.rat.denominator x) (sbv.rat.numerator y)))- (* (sbv.rat.denominator x) (sbv.rat.denominator y)))- )--[GOOD] (define-fun sbv.rat.times ((x SBVRational) (y SBVRational)) SBVRational- (SBV.Rational (* (sbv.rat.numerator x) (sbv.rat.numerator y))- (* (sbv.rat.denominator x) (sbv.rat.denominator y)))- )--[GOOD] (define-fun sbv.rat.uneg ((x SBVRational)) SBVRational- (SBV.Rational (* (- 1) (sbv.rat.numerator x)) (sbv.rat.denominator x))- )--[GOOD] (define-fun sbv.rat.abs ((x SBVRational)) SBVRational- (SBV.Rational (abs (sbv.rat.numerator x)) (sbv.rat.denominator x))- ) [GOOD] ; --- literal constants --- [GOOD] ; --- top level inputs --- [GOOD] (declare-fun s0 () (Array (SBVTuple2 String SBVRational) (SBVTuple2 SBVRational String))) ; tracks user variable "x"
SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs view
@@ -45,31 +45,47 @@ ++ genUnTest "negate" negate ++ genUnTest "abs" abs ++ genUnTest "signum" signum- ++ genBinTest ".&." (.&.)- ++ genBinTest ".|." (.|.)+ ++ genBitTest ".&." (.&.)+ ++ genBitTest ".|." (.|.) ++ genBoolTest "<" (<) (.<) ++ genBoolTest "<=" (<=) (.<=) ++ genBoolTest ">" (>) (.>) ++ genBoolTest ">=" (>=) (.>=) ++ genBoolTest "==" (==) (.==) ++ genBoolTest "/=" (/=) (./=)- ++ genBinTest "xor" xor- ++ genUnTest "complement" complement+ ++ genBitTest "xor" xor+ ++ genUnTestBit "complement" complement -genBinTest :: String -> (forall a. (Num a, Bits a) => a -> a -> a) -> [TestTree]+genBinTest :: String -> (forall a. Num a => a -> a -> a) -> [TestTree] genBinTest nm op = map mkTest $- zipWith pair [(show x, show y, x `op` y) | x <- w8s, y <- w8s ] [x `op` y | x <- sw8s, y <- sw8s ]- ++ zipWith pair [(show x, show y, x `op` y) | x <- w16s, y <- w16s] [x `op` y | x <- sw16s, y <- sw16s]- ++ zipWith pair [(show x, show y, x `op` y) | x <- w32s, y <- w32s] [x `op` y | x <- sw32s, y <- sw32s]- ++ zipWith pair [(show x, show y, x `op` y) | x <- w64s, y <- w64s] [x `op` y | x <- sw64s, y <- sw64s]- ++ zipWith pair [(show x, show y, x `op` y) | x <- i8s, y <- i8s ] [x `op` y | x <- si8s, y <- si8s ]- ++ zipWith pair [(show x, show y, x `op` y) | x <- i16s, y <- i16s] [x `op` y | x <- si16s, y <- si16s]- ++ zipWith pair [(show x, show y, x `op` y) | x <- i32s, y <- i32s] [x `op` y | x <- si32s, y <- si32s]- ++ zipWith pair [(show x, show y, x `op` y) | x <- i64s, y <- i64s] [x `op` y | x <- si64s, y <- si64s]- ++ zipWith pair [(show x, show y, x `op` y) | x <- iUBs, y <- iUBs] [x `op` y | x <- siUBs, y <- siUBs]- where pair (x, y, a) b = (x, y, show (fromIntegral a `asTypeOf` b) == show b)+ zipWith pair [(show x, show y, literal (x `op` y)) | x <- w8s, y <- w8s ] [x `op` y | x <- sw8s, y <- sw8s ]+ ++ zipWith pair [(show x, show y, literal (x `op` y)) | x <- w16s, y <- w16s] [x `op` y | x <- sw16s, y <- sw16s]+ ++ zipWith pair [(show x, show y, literal (x `op` y)) | x <- w32s, y <- w32s] [x `op` y | x <- sw32s, y <- sw32s]+ ++ zipWith pair [(show x, show y, literal (x `op` y)) | x <- w64s, y <- w64s] [x `op` y | x <- sw64s, y <- sw64s]+ ++ zipWith pair [(show x, show y, literal (x `op` y)) | x <- i8s, y <- i8s ] [x `op` y | x <- si8s, y <- si8s ]+ ++ zipWith pair [(show x, show y, literal (x `op` y)) | x <- i16s, y <- i16s] [x `op` y | x <- si16s, y <- si16s]+ ++ zipWith pair [(show x, show y, literal (x `op` y)) | x <- i32s, y <- i32s] [x `op` y | x <- si32s, y <- si32s]+ ++ zipWith pair [(show x, show y, literal (x `op` y)) | x <- i64s, y <- i64s] [x `op` y | x <- si64s, y <- si64s]+ ++ zipWith pair [(show x, show y, literal (x `op` y)) | x <- iUBs, y <- iUBs] [x `op` y | x <- siUBs, y <- siUBs]+ ++ zipWith pair [(show x, show y, literal (x `op` y)) | x <- rs, y <- rs] [x `op` y | x <- srs, y <- srs]+ ++ zipWith pair [(show x, show y, literal (x `op` y)) | x <- ras, y <- ras] [x `op` y | x <- sras, y <- sras]+ where pair (x, y, a) b = (x, y, a == b) mkTest (x, y, s) = testCase ("arithCF-" ++ nm ++ "." ++ x ++ "_" ++ y) (s `showsAs` "True") +genBitTest :: String -> (forall a. (Num a, Bits a) => a -> a -> a) -> [TestTree]+genBitTest nm op = map mkTest $+ zipWith pair [(show x, show y, literal (x `op` y)) | x <- w8s, y <- w8s ] [x `op` y | x <- sw8s, y <- sw8s ]+ ++ zipWith pair [(show x, show y, literal (x `op` y)) | x <- w16s, y <- w16s] [x `op` y | x <- sw16s, y <- sw16s]+ ++ zipWith pair [(show x, show y, literal (x `op` y)) | x <- w32s, y <- w32s] [x `op` y | x <- sw32s, y <- sw32s]+ ++ zipWith pair [(show x, show y, literal (x `op` y)) | x <- w64s, y <- w64s] [x `op` y | x <- sw64s, y <- sw64s]+ ++ zipWith pair [(show x, show y, literal (x `op` y)) | x <- i8s, y <- i8s ] [x `op` y | x <- si8s, y <- si8s ]+ ++ zipWith pair [(show x, show y, literal (x `op` y)) | x <- i16s, y <- i16s] [x `op` y | x <- si16s, y <- si16s]+ ++ zipWith pair [(show x, show y, literal (x `op` y)) | x <- i32s, y <- i32s] [x `op` y | x <- si32s, y <- si32s]+ ++ zipWith pair [(show x, show y, literal (x `op` y)) | x <- i64s, y <- i64s] [x `op` y | x <- si64s, y <- si64s]+ ++ zipWith pair [(show x, show y, literal (x `op` y)) | x <- iUBs, y <- iUBs] [x `op` y | x <- siUBs, y <- siUBs]+ where pair (x, y, a) b = (x, y, a == b)+ mkTest (x, y, s) = testCase ("arithCF-" ++ nm ++ "." ++ x ++ "_" ++ y) (s `showsAs` "True")+ genBoolTest :: String -> (forall a. Ord a => a -> a -> Bool) -> (forall a. OrdSymbolic a => a -> a -> SBool) -> [TestTree] genBoolTest nm op opS = map mkTest $ zipWith pair [(show x, show y, x `op` y) | x <- w8s, y <- w8s ] [x `opS` y | x <- sw8s, y <- sw8s ]@@ -87,12 +103,28 @@ ++ zipWith pair [(show x, show y, toL x `op` toL y) | x <- ssm, y <- ssm ] [x `opS` y | x <- ssm, y <- ssm ] ++ zipWith pair [(show x, show y, toL x `op` toL y) | x <- sse, y <- sse ] [x `opS` y | x <- sse, y <- sse ] ++ zipWith pair [(show x, show y, toL x `op` toL y) | x <- sst, y <- sst ] [x `opS` y | x <- sst, y <- sst ]+ ++ zipWith pair [(show x, show y, toL x `op` toL y) | x <- sras, y <- sras] [x `opS` y | x <- sras, y <- sras ] where pair (x, y, a) b = (x, y, Just a == unliteral b) mkTest (x, y, s) = testCase ("arithCF-" ++ nm ++ "." ++ x ++ "_" ++ y) (s `showsAs` "True") toL x = fromMaybe (error "genBoolTest: Cannot extract a literal!") (unliteral x) -genUnTest :: String -> (forall a. (Num a, Bits a) => a -> a) -> [TestTree]+genUnTest :: String -> (forall a. Num a => a -> a) -> [TestTree] genUnTest nm op = map mkTest $+ zipWith pair [(show x, literal (op x)) | x <- w8s ] [op x | x <- sw8s ]+ ++ zipWith pair [(show x, literal (op x)) | x <- w16s] [op x | x <- sw16s]+ ++ zipWith pair [(show x, literal (op x)) | x <- w32s] [op x | x <- sw32s]+ ++ zipWith pair [(show x, literal (op x)) | x <- w64s] [op x | x <- sw64s]+ ++ zipWith pair [(show x, literal (op x)) | x <- i8s ] [op x | x <- si8s ]+ ++ zipWith pair [(show x, literal (op x)) | x <- i16s] [op x | x <- si16s]+ ++ zipWith pair [(show x, literal (op x)) | x <- i32s] [op x | x <- si32s]+ ++ zipWith pair [(show x, literal (op x)) | x <- i64s] [op x | x <- si64s]+ ++ zipWith pair [(show x, literal (op x)) | x <- iUBs] [op x | x <- siUBs]+ ++ zipWith pair [(show x, literal (op x)) | x <- ras] [op x | x <- sras]+ where pair (x, a) b = (x, a == b)+ mkTest (x, s) = testCase ("arithCF-" ++ nm ++ "." ++ x) (s `showsAs` "True")++genUnTestBit :: String -> (forall a. (Num a, Bits a) => a -> a) -> [TestTree]+genUnTestBit nm op = map mkTest $ zipWith pair [(show x, op x) | x <- w8s ] [op x | x <- sw8s ] ++ zipWith pair [(show x, op x) | x <- w16s] [op x | x <- sw16s] ++ zipWith pair [(show x, op x) | x <- w32s] [op x | x <- sw32s]@@ -374,10 +406,16 @@ siUBs :: [SInteger] siUBs = map literal iUBs -rs :: [AlgReal]-rs = [fromRational (i % d) | i <- nums, d <- dens]+ras :: [Rational]+ras = [i % d | i <- nums, d <- dens] where nums = [-1000000 .. -999998] ++ [-2 .. 2] ++ [999998 .. 1000001] dens = [2 .. 5] ++ [98 .. 102] ++ [999998 .. 1000000]++sras :: [SRational]+sras = map literal ras++rs :: [AlgReal]+rs = map fromRational ras srs :: [SReal] srs = map literal rs
SBVTestSuite/TestSuite/Basics/ArithNoSolver2.hs view
@@ -15,6 +15,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-}
SBVTestSuite/TestSuite/Basics/ArithSolver.hs view
@@ -16,6 +16,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -40,8 +41,6 @@ import qualified Data.SBV.Char as SC import qualified Data.SBV.List as SL -import Data.SBV.Rational- data Day = Mon | Tue | Wed | Thu | Fri | Sat | Sun deriving (Bounded, Enum, Eq) mkSymbolicEnumeration ''Day @@ -62,16 +61,16 @@ ++ genUnTest True "negate" negate ++ genUnTest True "abs" abs ++ genUnTest True "signum" signum- ++ genBinTest False ".&." (.&.)- ++ genBinTest False ".|." (.|.)+ ++ genBitTest False ".&." (.&.)+ ++ genBitTest False ".|." (.|.) ++ genBoolTest "<" (<) (.<) ++ genBoolTest "<=" (<=) (.<=) ++ genBoolTest ">" (>) (.>) ++ genBoolTest ">=" (>=) (.>=) ++ genBoolTest "==" (==) (.==) ++ genBoolTest "/=" (/=) (./=)- ++ genBinTest False "xor" xor- ++ genUnTest False "complement" complement+ ++ genBitTest False "xor" xor+ ++ genUnTestBit False "complement" complement ++ genIntTest False "setBit" setBit ++ genIntTest False "clearBit" clearBit ++ genIntTest False "complementBit" complementBit@@ -125,7 +124,7 @@ | True = return False -genBinTest :: Bool -> String -> (forall a. (Num a, Bits a) => a -> a -> a) -> [TestTree]+genBinTest :: Bool -> String -> (forall a. Num a => a -> a -> a) -> [TestTree] genBinTest unboundedOK nm op = map mkTest $ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w8s, y <- w8s ] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- w16s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- w32s]@@ -134,6 +133,7 @@ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- i16s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- i32s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- i64s]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- rs, y <- rs] ++ [(show x, show y, mkThm2 x y (x `op` y)) | unboundedOK, x <- iUBs, y <- iUBs] where mkTest (x, y, t) = testCase ("genBinTest.arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y) (assert t) mkThm2 x y r = isTheorem $ do [a, b] <- mapM free ["x", "y"]@@ -141,6 +141,22 @@ constrain $ b .== literal y return $ literal r .== a `op` b +genBitTest :: Bool -> String -> (forall a. (Num a, Bits a) => a -> a -> a) -> [TestTree]+genBitTest unboundedOK nm op = map mkTest $ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w8s, y <- w8s ]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- w16s]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- w32s]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- w64s]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i8s, y <- i8s ]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- i16s]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- i32s]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- i64s]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | unboundedOK, x <- iUBs, y <- iUBs]+ where mkTest (x, y, t) = testCase ("genBitTest.arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y) (assert t)+ mkThm2 x y r = isTheorem $ do [a, b] <- mapM free ["x", "y"]+ constrain $ a .== literal x+ constrain $ b .== literal y+ return $ literal r .== a `op` b+ genBoolTest :: String -> (forall a. Ord a => a -> a -> Bool) -> (forall a. OrdSymbolic a => a -> a -> SBool) -> [TestTree] genBoolTest nm op opS = map mkTest $ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w8s, y <- w8s ] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- w16s ]@@ -155,6 +171,7 @@ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- fs, y <- fs ] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- ds, y <- ds ] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- ss, y <- ss ]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- rs, y <- rs ] ++ [(show x, show y, mkThm2L x y (x `op` y)) | nm `elem` allowedListComps, x <- sl, y <- sl ] ++ [(show x, show y, mkThm2M x y (x `op` y)) | x <- sm, y <- sm ] ++ [(show x, show y, mkThm2E x y (x `op` y)) | x <- se, y <- se ]@@ -184,7 +201,7 @@ constrain $ b .== literal y return $ literal r .== a `opS` b -genUnTest :: Bool -> String -> (forall a. (Num a, Bits a) => a -> a) -> [TestTree]+genUnTest :: Bool -> String -> (forall a. Num a => a -> a) -> [TestTree] genUnTest unboundedOK nm op = map mkTest $ [(show x, mkThm x (op x)) | x <- w8s ] ++ [(show x, mkThm x (op x)) | x <- w16s] ++ [(show x, mkThm x (op x)) | x <- w32s]@@ -193,12 +210,28 @@ ++ [(show x, mkThm x (op x)) | x <- i16s] ++ [(show x, mkThm x (op x)) | x <- i32s] ++ [(show x, mkThm x (op x)) | x <- i64s]+ ++ [(show x, mkThm x (op x)) | x <- rs ] ++ [(show x, mkThm x (op x)) | unboundedOK, x <- iUBs] where mkTest (x, t) = testCase ("genUnTest.arithmetic-" ++ nm ++ "." ++ x) (assert t) mkThm x r = isTheorem $ do a <- free "x" constrain $ a .== literal x return $ literal r .== op a +genUnTestBit :: Bool -> String -> (forall a. (Num a, Bits a) => a -> a) -> [TestTree]+genUnTestBit unboundedOK nm op = map mkTest $ [(show x, mkThm x (op x)) | x <- w8s ]+ ++ [(show x, mkThm x (op x)) | x <- w16s]+ ++ [(show x, mkThm x (op x)) | x <- w32s]+ ++ [(show x, mkThm x (op x)) | x <- w64s]+ ++ [(show x, mkThm x (op x)) | x <- i8s ]+ ++ [(show x, mkThm x (op x)) | x <- i16s]+ ++ [(show x, mkThm x (op x)) | x <- i32s]+ ++ [(show x, mkThm x (op x)) | x <- i64s]+ ++ [(show x, mkThm x (op x)) | unboundedOK, x <- iUBs]+ where mkTest (x, t) = testCase ("genUnTestBit.arithmetic-" ++ nm ++ "." ++ x) (assert t)+ mkThm x r = isTheorem $ do a <- free "x"+ constrain $ a .== literal x+ return $ literal r .== op a+ genIntTest :: Bool -> String -> (forall a. (Num a, Bits a) => (a -> Int -> a)) -> [TestTree] genIntTest overSized nm op = map mkTest $ [("u8", show x, show y, mkThm2 x y (x `op` y)) | x <- w8s, y <- is (intSizeOf x)]@@ -363,7 +396,7 @@ genDoubles :: [TestTree] genDoubles = genIEEE754 "genDoubles" ds -genIEEE754 :: (IEEEFloating a, Num (SBV a), Show a) => String -> [a] -> [TestTree]+genIEEE754 :: (IEEEFloating a, OrdSymbolic (SBV a), Num (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]@@ -843,7 +876,10 @@ iUBs = [-1000000] ++ [-1 .. 1] ++ [1000000] ars :: [AlgReal]-ars = [fromRational (i % d) | i <- is, d <- dens]+ars = map fromRational rs++rs :: [Ratio Integer]+rs = [i % d | i <- is, d <- dens] where is = [-1000000] ++ [-1 .. 1] ++ [10000001] dens = [5,100,1000000] @@ -914,7 +950,7 @@ ++ [mkTest2 "fromTo" s t (fromTo [s..t ] s t) | s <- doubles , t <- doubles ] ++ [mkTest2 "fromTo" s t (fromTo [s..t ] s t) | s <- fps , t <- fps ] ++ [mkTest2 "fromTo" s t (fromTo [s..t ] s t) | s <- lcs , t <- lcs ]- ++ [mkTest2 "fromTo" s t (fromTo [s..t ] s t) | s <- rs , t <- rs ]+ ++ [mkTest2 "fromTo" s t (fromTo [s..t ] s t) | s <- rrs , t <- rrs ] -- Only bounded for fromThen, otherwise infinite (or too big for chars) ++ [mkTest2 "fromThen" s t (fromThen [s, t.. ] s t) | s <- univ @(WordN 4), t <- univ @(WordN 4), s /= t]@@ -933,7 +969,7 @@ ++ [mkTest3 "fromThenTo" s t u (fromThenTo [s, t..u] s t u) | s <- doubles , t <- doubles , s /= t, u <- doubles ] ++ [mkTest3 "fromThenTo" s t u (fromThenTo [s, t..u] s t u) | s <- fps , t <- fps , s /= t, u <- fps ] ++ [mkTest3 "fromThenTo" s t u (fromThenTo [s, t..u] s t u) | s <- lcs , t <- lcs , s /= t, u <- lcs ]- ++ [mkTest3 "fromThenTo" s t u (fromThenTo [s, t..u] s t u) | s <- rs , t <- rs , s /= t, u <- rs ]+ ++ [mkTest3 "fromThenTo" s t u (fromThenTo [s, t..u] s t u) | s <- rrs , t <- rrs , s /= t, u <- rrs ] where mkTest1 pre a = testCase ("sEnum_" ++ pre ++ "_|" ++ show (kindOf a) ++ "|_" ++ show a) mkTest2 pre a b = testCase ("sEnum_" ++ pre ++ "_|" ++ show (kindOf a) ++ "|_" ++ show (a, b))@@ -1000,9 +1036,9 @@ fps = [] -- This one works, but is way too slow. So we further reduce the range- rs :: [AlgReal]- -- rs = [-3.4, -3.2 .. 3.5]- rs = [-0.4, -0.2 .. 0.4]+ rrs :: [AlgReal]+ -- rrs = [-3.4, -3.2 .. 3.5]+ rrs = [-0.4, -0.2 .. 0.4] -- don't add min/max bounds here. causes too big lists. lcs :: [Char]
SBVTestSuite/TestSuite/Basics/Set.hs view
@@ -11,6 +11,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-}
SBVTestSuite/TestSuite/Basics/Tuple.hs view
@@ -12,6 +12,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-}
SBVTestSuite/TestSuite/Queries/Enums.hs view
@@ -11,6 +11,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-}
SBVTestSuite/TestSuite/Queries/FreshVars.hs view
@@ -11,6 +11,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedLists #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-}
SBVTestSuite/TestSuite/Queries/Uninterpreted.hs view
@@ -11,6 +11,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-}
sbv.cabal view
@@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv-Version : 12.1+Version : 12.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@@ -27,8 +27,8 @@ manual : True source-repository head- type: git- location: git://github.com/LeventErkok/sbv.git+ type : git+ location: https://github.com/LeventErkok/sbv.git common common-settings default-language: Haskell2010@@ -239,6 +239,7 @@ , Documentation.SBV.Examples.TP.BinarySearch , Documentation.SBV.Examples.TP.CaseSplit , Documentation.SBV.Examples.TP.Fibonacci+ , Documentation.SBV.Examples.TP.GCD , Documentation.SBV.Examples.TP.InsertionSort , Documentation.SBV.Examples.TP.Kleene , Documentation.SBV.Examples.TP.McCarthy91