diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,36 @@ * Hackage: * GitHub: +### 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 diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -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: diff --git a/Data/SBV/Client.hs b/Data/SBV/Client.hs --- a/Data/SBV/Client.hs +++ b/Data/SBV/Client.hs @@ -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 diff --git a/Data/SBV/Core/Data.hs b/Data/SBV/Core/Data.hs --- a/Data/SBV/Core/Data.hs +++ b/Data/SBV/Core/Data.hs @@ -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)) diff --git a/Data/SBV/Core/Floating.hs b/Data/SBV/Core/Floating.hs --- a/Data/SBV/Core/Floating.hs +++ b/Data/SBV/Core/Floating.hs @@ -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 diff --git a/Data/SBV/Core/Model.hs b/Data/SBV/Core/Model.hs --- a/Data/SBV/Core/Model.hs +++ b/Data/SBV/Core/Model.hs @@ -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 diff --git a/Data/SBV/Core/Operations.hs b/Data/SBV/Core/Operations.hs --- a/Data/SBV/Core/Operations.hs +++ b/Data/SBV/Core/Operations.hs @@ -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) diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs --- a/Data/SBV/Core/Symbolic.hs +++ b/Data/SBV/Core/Symbolic.hs @@ -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 diff --git a/Data/SBV/List.hs b/Data/SBV/List.hs --- a/Data/SBV/List.hs +++ b/Data/SBV/List.hs @@ -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 diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs --- a/Data/SBV/Provers/Prover.hs +++ b/Data/SBV/Provers/Prover.hs @@ -109,6 +109,7 @@ , firstifyUniqueLen = 10 , tpOptions = TPOptions { ribbonLength = 40 , quiet = False + , printAsms = False , printStats = False , cacheProofs = False } diff --git a/Data/SBV/Rational.hs b/Data/SBV/Rational.hs --- a/Data/SBV/Rational.hs +++ b/Data/SBV/Rational.hs @@ -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" -} diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -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) diff --git a/Data/SBV/TP.hs b/Data/SBV/TP.hs --- a/Data/SBV/TP.hs +++ b/Data/SBV/TP.hs @@ -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 diff --git a/Data/SBV/TP/List.hs b/Data/SBV/TP/List.hs --- a/Data/SBV/TP/List.hs +++ b/Data/SBV/TP/List.hs @@ -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. diff --git a/Data/SBV/TP/TP.hs b/Data/SBV/TP/TP.hs --- a/Data/SBV/TP/TP.hs +++ b/Data/SBV/TP/TP.hs @@ -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" -} diff --git a/Data/SBV/TP/Utils.hs b/Data/SBV/TP/Utils.hs --- a/Data/SBV/TP/Utils.hs +++ b/Data/SBV/TP/Utils.hs @@ -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 }} diff --git a/Data/SBV/Tools/Range.hs b/Data/SBV/Tools/Range.hs --- a/Data/SBV/Tools/Range.hs +++ b/Data/SBV/Tools/Range.hs @@ -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 [] diff --git a/Documentation/SBV/Examples/Lists/BoundedMutex.hs b/Documentation/SBV/Examples/Lists/BoundedMutex.hs --- a/Documentation/SBV/Examples/Lists/BoundedMutex.hs +++ b/Documentation/SBV/Examples/Lists/BoundedMutex.hs @@ -12,6 +12,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedLists #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} diff --git a/Documentation/SBV/Examples/Misc/Enumerate.hs b/Documentation/SBV/Examples/Misc/Enumerate.hs --- a/Documentation/SBV/Examples/Misc/Enumerate.hs +++ b/Documentation/SBV/Examples/Misc/Enumerate.hs @@ -14,6 +14,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} diff --git a/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs b/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs --- a/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs +++ b/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs @@ -14,6 +14,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} diff --git a/Documentation/SBV/Examples/Optimization/Enumerate.hs b/Documentation/SBV/Examples/Optimization/Enumerate.hs --- a/Documentation/SBV/Examples/Optimization/Enumerate.hs +++ b/Documentation/SBV/Examples/Optimization/Enumerate.hs @@ -12,6 +12,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} diff --git a/Documentation/SBV/Examples/Puzzles/Birthday.hs b/Documentation/SBV/Examples/Puzzles/Birthday.hs --- a/Documentation/SBV/Examples/Puzzles/Birthday.hs +++ b/Documentation/SBV/Examples/Puzzles/Birthday.hs @@ -37,6 +37,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} diff --git a/Documentation/SBV/Examples/Puzzles/Fish.hs b/Documentation/SBV/Examples/Puzzles/Fish.hs --- a/Documentation/SBV/Examples/Puzzles/Fish.hs +++ b/Documentation/SBV/Examples/Puzzles/Fish.hs @@ -31,6 +31,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} diff --git a/Documentation/SBV/Examples/Puzzles/Garden.hs b/Documentation/SBV/Examples/Puzzles/Garden.hs --- a/Documentation/SBV/Examples/Puzzles/Garden.hs +++ b/Documentation/SBV/Examples/Puzzles/Garden.hs @@ -30,6 +30,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} diff --git a/Documentation/SBV/Examples/Puzzles/HexPuzzle.hs b/Documentation/SBV/Examples/Puzzles/HexPuzzle.hs --- a/Documentation/SBV/Examples/Puzzles/HexPuzzle.hs +++ b/Documentation/SBV/Examples/Puzzles/HexPuzzle.hs @@ -38,6 +38,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} diff --git a/Documentation/SBV/Examples/Puzzles/KnightsAndKnaves.hs b/Documentation/SBV/Examples/Puzzles/KnightsAndKnaves.hs --- a/Documentation/SBV/Examples/Puzzles/KnightsAndKnaves.hs +++ b/Documentation/SBV/Examples/Puzzles/KnightsAndKnaves.hs @@ -14,6 +14,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} diff --git a/Documentation/SBV/Examples/Puzzles/Orangutans.hs b/Documentation/SBV/Examples/Puzzles/Orangutans.hs --- a/Documentation/SBV/Examples/Puzzles/Orangutans.hs +++ b/Documentation/SBV/Examples/Puzzles/Orangutans.hs @@ -14,6 +14,7 @@ {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE OverloadedRecordDot #-} diff --git a/Documentation/SBV/Examples/Queries/Enums.hs b/Documentation/SBV/Examples/Queries/Enums.hs --- a/Documentation/SBV/Examples/Queries/Enums.hs +++ b/Documentation/SBV/Examples/Queries/Enums.hs @@ -11,6 +11,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} diff --git a/Documentation/SBV/Examples/TP/Basics.hs b/Documentation/SBV/Examples/TP/Basics.hs --- a/Documentation/SBV/Examples/TP/Basics.hs +++ b/Documentation/SBV/Examples/TP/Basics.hs @@ -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 () diff --git a/Documentation/SBV/Examples/TP/BinarySearch.hs b/Documentation/SBV/Examples/TP/BinarySearch.hs --- a/Documentation/SBV/Examples/TP/BinarySearch.hs +++ b/Documentation/SBV/Examples/TP/BinarySearch.hs @@ -6,7 +6,7 @@ -- Maintainer: erkokl@gmail.com -- Stability : experimental -- --- Proving binary search correct +-- Proving binary search correct. ----------------------------------------------------------------------------- {-# LANGUAGE DataKinds #-} diff --git a/Documentation/SBV/Examples/TP/GCD.hs b/Documentation/SBV/Examples/TP/GCD.hs new file mode 100644 --- /dev/null +++ b/Documentation/SBV/Examples/TP/GCD.hs @@ -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" -} diff --git a/Documentation/SBV/Examples/TP/InsertionSort.hs b/Documentation/SBV/Examples/TP/InsertionSort.hs --- a/Documentation/SBV/Examples/TP/InsertionSort.hs +++ b/Documentation/SBV/Examples/TP/InsertionSort.hs @@ -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 -------------------------------------------------------------------------------------------- diff --git a/Documentation/SBV/Examples/TP/Majority.hs b/Documentation/SBV/Examples/TP/Majority.hs --- a/Documentation/SBV/Examples/TP/Majority.hs +++ b/Documentation/SBV/Examples/TP/Majority.hs @@ -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) diff --git a/Documentation/SBV/Examples/TP/MergeSort.hs b/Documentation/SBV/Examples/TP/MergeSort.hs --- a/Documentation/SBV/Examples/TP/MergeSort.hs +++ b/Documentation/SBV/Examples/TP/MergeSort.hs @@ -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 -------------------------------------------------------------------------------------------- diff --git a/Documentation/SBV/Examples/TP/QuickSort.hs b/Documentation/SBV/Examples/TP/QuickSort.hs --- a/Documentation/SBV/Examples/TP/QuickSort.hs +++ b/Documentation/SBV/Examples/TP/QuickSort.hs @@ -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) diff --git a/Documentation/SBV/Examples/TP/Reverse.hs b/Documentation/SBV/Examples/TP/Reverse.hs --- a/Documentation/SBV/Examples/TP/Reverse.hs +++ b/Documentation/SBV/Examples/TP/Reverse.hs @@ -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 diff --git a/Documentation/SBV/Examples/TP/SortHelpers.hs b/Documentation/SBV/Examples/TP/SortHelpers.hs --- a/Documentation/SBV/Examples/TP/SortHelpers.hs +++ b/Documentation/SBV/Examples/TP/SortHelpers.hs @@ -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)) [] diff --git a/Documentation/SBV/Examples/TP/Sqrt2IsIrrational.hs b/Documentation/SBV/Examples/TP/Sqrt2IsIrrational.hs --- a/Documentation/SBV/Examples/TP/Sqrt2IsIrrational.hs +++ b/Documentation/SBV/Examples/TP/Sqrt2IsIrrational.hs @@ -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. -- diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -181,6 +181,7 @@ Adam Foltzer, Joshua Gancher, Remy Goldschmidt, +Jan Grant, Brad Hardy, Tom Hawkins, Greg Horn, diff --git a/SBVTestSuite/GoldFiles/doctest_sanity.gold b/SBVTestSuite/GoldFiles/doctest_sanity.gold --- a/SBVTestSuite/GoldFiles/doctest_sanity.gold +++ b/SBVTestSuite/GoldFiles/doctest_sanity.gold @@ -1,3 +1,3 @@ -Total: 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 diff --git a/SBVTestSuite/GoldFiles/queryArrays12.gold b/SBVTestSuite/GoldFiles/queryArrays12.gold --- a/SBVTestSuite/GoldFiles/queryArrays12.gold +++ b/SBVTestSuite/GoldFiles/queryArrays12.gold @@ -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" diff --git a/SBVTestSuite/GoldFiles/queryArrays13.gold b/SBVTestSuite/GoldFiles/queryArrays13.gold --- a/SBVTestSuite/GoldFiles/queryArrays13.gold +++ b/SBVTestSuite/GoldFiles/queryArrays13.gold @@ -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" diff --git a/SBVTestSuite/GoldFiles/queryArrays14.gold b/SBVTestSuite/GoldFiles/queryArrays14.gold --- a/SBVTestSuite/GoldFiles/queryArrays14.gold +++ b/SBVTestSuite/GoldFiles/queryArrays14.gold @@ -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" diff --git a/SBVTestSuite/GoldFiles/queryArrays15.gold b/SBVTestSuite/GoldFiles/queryArrays15.gold --- a/SBVTestSuite/GoldFiles/queryArrays15.gold +++ b/SBVTestSuite/GoldFiles/queryArrays15.gold @@ -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" diff --git a/SBVTestSuite/GoldFiles/queryArrays16.gold b/SBVTestSuite/GoldFiles/queryArrays16.gold --- a/SBVTestSuite/GoldFiles/queryArrays16.gold +++ b/SBVTestSuite/GoldFiles/queryArrays16.gold @@ -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" diff --git a/SBVTestSuite/GoldFiles/queryArrays17.gold b/SBVTestSuite/GoldFiles/queryArrays17.gold --- a/SBVTestSuite/GoldFiles/queryArrays17.gold +++ b/SBVTestSuite/GoldFiles/queryArrays17.gold @@ -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" diff --git a/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs b/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs --- a/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs +++ b/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs @@ -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 diff --git a/SBVTestSuite/TestSuite/Basics/ArithNoSolver2.hs b/SBVTestSuite/TestSuite/Basics/ArithNoSolver2.hs --- a/SBVTestSuite/TestSuite/Basics/ArithNoSolver2.hs +++ b/SBVTestSuite/TestSuite/Basics/ArithNoSolver2.hs @@ -15,6 +15,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} diff --git a/SBVTestSuite/TestSuite/Basics/ArithSolver.hs b/SBVTestSuite/TestSuite/Basics/ArithSolver.hs --- a/SBVTestSuite/TestSuite/Basics/ArithSolver.hs +++ b/SBVTestSuite/TestSuite/Basics/ArithSolver.hs @@ -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] diff --git a/SBVTestSuite/TestSuite/Basics/Set.hs b/SBVTestSuite/TestSuite/Basics/Set.hs --- a/SBVTestSuite/TestSuite/Basics/Set.hs +++ b/SBVTestSuite/TestSuite/Basics/Set.hs @@ -11,6 +11,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} diff --git a/SBVTestSuite/TestSuite/Basics/Tuple.hs b/SBVTestSuite/TestSuite/Basics/Tuple.hs --- a/SBVTestSuite/TestSuite/Basics/Tuple.hs +++ b/SBVTestSuite/TestSuite/Basics/Tuple.hs @@ -12,6 +12,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} diff --git a/SBVTestSuite/TestSuite/Queries/Enums.hs b/SBVTestSuite/TestSuite/Queries/Enums.hs --- a/SBVTestSuite/TestSuite/Queries/Enums.hs +++ b/SBVTestSuite/TestSuite/Queries/Enums.hs @@ -11,6 +11,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} diff --git a/SBVTestSuite/TestSuite/Queries/FreshVars.hs b/SBVTestSuite/TestSuite/Queries/FreshVars.hs --- a/SBVTestSuite/TestSuite/Queries/FreshVars.hs +++ b/SBVTestSuite/TestSuite/Queries/FreshVars.hs @@ -11,6 +11,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedLists #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} diff --git a/SBVTestSuite/TestSuite/Queries/Uninterpreted.hs b/SBVTestSuite/TestSuite/Queries/Uninterpreted.hs --- a/SBVTestSuite/TestSuite/Queries/Uninterpreted.hs +++ b/SBVTestSuite/TestSuite/Queries/Uninterpreted.hs @@ -11,6 +11,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv -Version : 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