diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,23 @@ * Hackage: * GitHub: -* Latest Hackage released version: 5.12, 2016-06-06 +* Latest Hackage released version: 5.13, 2016-10-29 + +### Version 5.13, 2016-10-29 + + * Fix broken links, thanks to Stephan Renatus for the patch. + + * Code generation: Create directory path if it does not exist. Thanks to Robert Dockins + for the patch. + + * Generalize the type of sFromIntegral, dropping the Bits requirement. In turn, this + allowed us to remove sIntegerToSReal, since sFromIntegral can be used instead. + + * Add support for sRealToSInteger. (Essentially the floor function for SReal.) + + * Several space-leaks fixed for better performance. Patch contributed by Robert Dockins. + + * Improved Random instance for Rational. Thanks to Joe Leslie-Hurd for the idea. ### Version 5.12, 2016-06-06 diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -131,7 +131,7 @@ , sFloatAsSWord32, sWord32AsSFloat, sDoubleAsSWord64, sWord64AsSDouble, blastSFloat, blastSDouble -- *** Signed algebraic reals -- $algReals - , SReal, AlgReal, sIntegerToSReal + , SReal, AlgReal, sRealToSInteger -- ** Creating a symbolic variable -- $createSym , sBool, sWord8, sWord16, sWord32, sWord64, sInt8, sInt16, sInt32, sInt64, sInteger, sReal, sFloat, sDouble diff --git a/Data/SBV/BitVectors/AlgReals.hs b/Data/SBV/BitVectors/AlgReals.hs --- a/Data/SBV/BitVectors/AlgReals.hs +++ b/Data/SBV/BitVectors/AlgReals.hs @@ -136,14 +136,18 @@ toRational x = error $ "AlgReal.toRational: Argument cannot be represented as a rational value: " ++ algRealToHaskell x instance Random Rational where - random g = let (a, g') = random g - (b, g'') = random g' - in (a % b, g'') - -- this may not be quite kosher, but will do for our purposes (test-generation, mainly) - randomR (l, h) g = let (ln, ld) = (numerator l, denominator l) - (hn, hd) = (numerator h, denominator h) - (a, g') = randomR (ln*hd, hn*ld) g - in (a % (ld * hd), g') + random g = (a % b', g'') + where (a, g') = random g + (b, g'') = random g' + b' = if 0 < b then b else 1 - b -- ensures 0 < b + + randomR (l, h) g = (r * d + l, g'') + where (b, g') = random g + b' = if 0 < b then b else 1 - b -- ensures 0 < b + (a, g'') = randomR (0, b') g' + + r = a % b' + d = h - l instance Random AlgReal where random g = let (a, g') = random g in (AlgRational True a, g') diff --git a/Data/SBV/BitVectors/Concrete.hs b/Data/SBV/BitVectors/Concrete.hs --- a/Data/SBV/BitVectors/Concrete.hs +++ b/Data/SBV/BitVectors/Concrete.hs @@ -20,11 +20,11 @@ import Data.SBV.BitVectors.AlgReals -- | A constant value -data CWVal = CWAlgReal AlgReal -- ^ algebraic real - | CWInteger Integer -- ^ bit-vector/unbounded integer - | CWFloat Float -- ^ float - | CWDouble Double -- ^ double - | CWUserSort (Maybe Int, String) -- ^ value of an uninterpreted/user kind. The Maybe Int shows index position for enumerations +data CWVal = CWAlgReal !AlgReal -- ^ algebraic real + | CWInteger !Integer -- ^ bit-vector/unbounded integer + | CWFloat !Float -- ^ float + | CWDouble !Double -- ^ double + | CWUserSort !(Maybe Int, String) -- ^ value of an uninterpreted/user kind. The Maybe Int shows index position for enumerations -- | Eq instance for CWVal. Note that we cannot simply derive Eq/Ord, since CWAlgReal doesn't have proper -- instances for these when values are infinitely precise reals. However, we do diff --git a/Data/SBV/BitVectors/Kind.hs b/Data/SBV/BitVectors/Kind.hs --- a/Data/SBV/BitVectors/Kind.hs +++ b/Data/SBV/BitVectors/Kind.hs @@ -23,7 +23,7 @@ -- | Kind of symbolic value data Kind = KBool - | KBounded Bool Int + | KBounded !Bool !Int | KUnbounded | KReal | KUserSort String (Either String [String]) @@ -39,6 +39,7 @@ kindRank (KUserSort s _) = Right (Right s) kindRank KFloat = Left 3 kindRank KDouble = Left 4 +{-# INLINE kindRank #-} -- | We want to equate user-sorts only by name instance Eq Kind where diff --git a/Data/SBV/BitVectors/Model.hs b/Data/SBV/BitVectors/Model.hs --- a/Data/SBV/BitVectors/Model.hs +++ b/Data/SBV/BitVectors/Model.hs @@ -30,7 +30,7 @@ , constrain, pConstrain, sBool, sBools, sWord8, sWord8s, sWord16, sWord16s, sWord32 , sWord32s, sWord64, sWord64s, sInt8, sInt8s, sInt16, sInt16s, sInt32, sInt32s, sInt64 , sInt64s, sInteger, sIntegers, sReal, sReals, sFloat, sFloats, sDouble, sDoubles, slet - , sIntegerToSReal, label + , sRealToSInteger, label , sAssert , liftQRem, liftDMod, symbolicMergeWithKind , genLiteral, genFromCW, genMkSymVar @@ -300,13 +300,19 @@ sDoubles :: [String] -> Symbolic [SDouble] sDoubles = symbolics --- | Promote an SInteger to an SReal -sIntegerToSReal :: SInteger -> SReal -sIntegerToSReal x - | Just i <- unliteral x = literal $ fromInteger i - | True = SBV (SVal KReal (Right (cache y))) +-- | Convert an SReal to an SInteger. That is, it computes the +-- largest integer @n@ that satisfies @sIntegerToSReal n <= r@ +-- essentially giving us the @floor@. +-- +-- For instance, @1.3@ will be @1@, but @-1.3@ will be @-2@. +sRealToSInteger :: SReal -> SInteger +sRealToSInteger x + | Just i <- unliteral x, isExactRational i + = literal $ floor (toRational i) + | True + = SBV (SVal KUnbounded (Right (cache y))) where y st = do xsw <- sbvToSW st x - newExpr st KReal (SBVApp (IntCast KUnbounded KReal) [xsw]) + newExpr st KUnbounded (SBVApp (KindCast KReal KUnbounded) [xsw]) -- | label: Label the result of an expression. This is essentially a no-op, but useful as it generates a comment in the generated C/SMT-Lib code. -- Note that if the argument is a constant, then the label is dropped completely, per the usual constant folding strategy. @@ -679,7 +685,7 @@ setBitTo x i b = ite b (setBit x i) (clearBit x i) -- | Conversion between integral-symbolic values, akin to Haskell's fromIntegral -sFromIntegral :: forall a b. (Integral a, HasKind a, Num a, Bits a, SymWord a, HasKind b, Num b, Bits b, SymWord b) => SBV a -> SBV b +sFromIntegral :: forall a b. (Integral a, HasKind a, Num a, SymWord a, HasKind b, Num b, SymWord b) => SBV a -> SBV b sFromIntegral x | isReal x = error "SBV.sFromIntegral: Called on a real value" -- can't really happen due to types, but being overcautious @@ -691,7 +697,7 @@ kFrom = kindOf x kTo = kindOf (undefined :: b) y st = do xsw <- sbvToSW st x - newExpr st kTo (SBVApp (IntCast kFrom kTo) [xsw]) + newExpr st kTo (SBVApp (KindCast kFrom kTo) [xsw]) -- | Generalization of 'shiftL', when the shift-amount is symbolic. Since Haskell's -- 'shiftL' only takes an 'Int' as the shift amount, it cannot be used when we have diff --git a/Data/SBV/BitVectors/Operations.hs b/Data/SBV/BitVectors/Operations.hs --- a/Data/SBV/BitVectors/Operations.hs +++ b/Data/SBV/BitVectors/Operations.hs @@ -30,7 +30,7 @@ , svIte, svLazyIte, svSymbolicMerge , svSelect , svSign, svUnsign, svSetBit, svWordFromBE, svWordFromLE - , svExp + , svExp, svFromIntegral -- ** Derived operations , svToWord1, svFromWord1, svTestBit , svShiftLeft, svShiftRight @@ -67,19 +67,19 @@ -- | Convert from an Integer. svInteger :: Kind -> Integer -> SVal -svInteger k n = SVal k (Left (mkConstCW k n)) +svInteger k n = SVal k (Left $! mkConstCW k n) -- | Convert from a Float svFloat :: Float -> SVal -svFloat f = SVal KFloat (Left (CW KFloat (CWFloat f))) +svFloat f = SVal KFloat (Left $! CW KFloat (CWFloat f)) -- | Convert from a Float svDouble :: Double -> SVal -svDouble d = SVal KDouble (Left (CW KDouble (CWDouble d))) +svDouble d = SVal KDouble (Left $! CW KDouble (CWDouble d)) -- | Convert from a Rational svReal :: Rational -> SVal -svReal d = SVal KReal (Left (CW KReal (CWAlgReal (fromRational d)))) +svReal d = SVal KReal (Left $! CW KReal (CWAlgReal (fromRational d))) -------------------------------------------------------------------------------- -- Basic destructors @@ -391,9 +391,9 @@ svExtract :: Int -> Int -> SVal -> SVal svExtract i j x@(SVal (KBounded s _) _) | i < j - = SVal k (Left (CW k (CWInteger 0))) + = SVal k (Left $! CW k (CWInteger 0)) | SVal _ (Left (CW _ (CWInteger v))) <- x - = SVal k (Left (normCW (CW k (CWInteger (v `shiftR` j))))) + = SVal k (Left $! normCW (CW k (CWInteger (v `shiftR` j)))) | True = SVal k (Right (cache y)) where k = KBounded s (i - j + 1) @@ -407,7 +407,7 @@ | i == 0 = y | j == 0 = x | Left (CW _ (CWInteger m)) <- a, Left (CW _ (CWInteger n)) <- b - = SVal k (Left (CW k (CWInteger (m `shiftL` j .|. n)))) + = SVal k (Left $! CW k (CWInteger (m `shiftL` j .|. n))) | True = SVal k (Right (cache z)) where @@ -571,6 +571,18 @@ svUnsign :: SVal -> SVal svUnsign = svChangeSign False +-- | Convert a symbolic bitvector from one integral kind to another. +svFromIntegral :: Kind -> SVal -> SVal +svFromIntegral kTo x + | Just v <- svAsInteger x + = svInteger kTo v + | True + = result + where result = SVal kTo (Right (cache y)) + kFrom = kindOf x + y st = do xsw <- svToSW st x + newExpr st kTo (SBVApp (KindCast kFrom kTo) [xsw]) + -------------------------------------------------------------------------------- -- Derived operations @@ -671,7 +683,7 @@ noUnint2 x y = error $ "Unexpected binary operation called on uninterpreted/enumerated values: " ++ show (x, y) liftSym1 :: (State -> Kind -> SW -> IO SW) -> (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> SVal -> SVal -liftSym1 _ opCR opCI opCF opCD (SVal k (Left a)) = SVal k $ Left $ mapCW opCR opCI opCF opCD noUnint a +liftSym1 _ opCR opCI opCF opCD (SVal k (Left a)) = SVal k . Left $! mapCW opCR opCI opCF opCD noUnint a liftSym1 opS _ _ _ _ a@(SVal k _) = SVal k $ Right $ cache c where c st = do swa <- svToSW st a opS st k swa @@ -683,8 +695,8 @@ opS st k sw1 sw2 liftSym2 :: (State -> Kind -> SW -> SW -> IO SW) -> (CW -> CW -> Bool) -> (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float) -> (Double -> Double -> Double) -> SVal -> SVal -> SVal -liftSym2 _ okCW opCR opCI opCF opCD (SVal k (Left a)) (SVal _ (Left b)) | okCW a b = SVal k $ Left $ mapCW2 opCR opCI opCF opCD noUnint2 a b -liftSym2 opS _ _ _ _ _ a@(SVal k _) b = SVal k $ Right $ liftSW2 opS k a b +liftSym2 _ okCW opCR opCI opCF opCD (SVal k (Left a)) (SVal _ (Left b)) | okCW a b = SVal k . Left $! mapCW2 opCR opCI opCF opCD noUnint2 a b +liftSym2 opS _ _ _ _ _ a@(SVal k _) b = SVal k $ Right $ liftSW2 opS k a b liftSym2B :: (State -> Kind -> SW -> SW -> IO SW) -> (CW -> CW -> Bool) -> (AlgReal -> AlgReal -> Bool) -> (Integer -> Integer -> Bool) -> (Float -> Float -> Bool) -> (Double -> Double -> Bool) -> ((Maybe Int, String) -> (Maybe Int, String) -> Bool) -> SVal -> SVal -> SVal liftSym2B _ okCW opCR opCI opCF opCD opUI (SVal _ (Left a)) (SVal _ (Left b)) | okCW a b = svBool (liftCW2 opCR opCI opCF opCD opUI a b) diff --git a/Data/SBV/BitVectors/Symbolic.hs b/Data/SBV/BitVectors/Symbolic.hs --- a/Data/SBV/BitVectors/Symbolic.hs +++ b/Data/SBV/BitVectors/Symbolic.hs @@ -83,7 +83,7 @@ newtype NodeId = NodeId Int deriving (Eq, Ord) -- | A symbolic word, tracking it's signedness and size. -data SW = SW Kind NodeId deriving (Eq, Ord) +data SW = SW !Kind !NodeId deriving (Eq, Ord) instance HasKind SW where kindOf (SW k _) = k @@ -139,7 +139,7 @@ | LkUp (Int, Kind, Kind, Int) !SW !SW -- (table-index, arg-type, res-type, length of the table) index out-of-bounds-value | ArrEq Int Int -- Array equality | ArrRead Int - | IntCast Kind Kind + | KindCast Kind Kind | Uninterpreted String | Label String -- Essentially no-op; useful for code generation to emit comments. | IEEEFP FPOp -- Floating-point ops, categorized separately @@ -174,7 +174,7 @@ -- this mapping stays correct through SMTLib changes. The only exception -- is FP_Cast; where we handle different source/origins explicitly later on. instance Show FPOp where - show (FP_Cast f t r) = "(FP_Cast: " ++ show f ++ " -> " ++ show t ++ "using RM [" ++ show r ++ "])" + show (FP_Cast f t r) = "(FP_Cast: " ++ show f ++ " -> " ++ show t ++ ", using RM [" ++ show r ++ "])" show (FP_Reinterpret f t) = case (f, t) of (KBounded False 32, KFloat) -> "(_ to_fp 8 24)" (KBounded False 64, KDouble) -> "(_ to_fp 11 53)" @@ -213,7 +213,7 @@ where tinfo = "table" ++ show ti ++ "(" ++ show at ++ " -> " ++ show rt ++ ", " ++ show l ++ ")" show (ArrEq i j) = "array_" ++ show i ++ " == array_" ++ show j show (ArrRead i) = "select array_" ++ show i - show (IntCast fr to) = "cast_" ++ show fr ++ "_" ++ show to + show (KindCast fr to) = "cast_" ++ show fr ++ "_" ++ show to show (Uninterpreted i) = "[uninterpreted] " ++ i show (Label s) = "[label] " ++ s show (IEEEFP w) = show w diff --git a/Data/SBV/Compilers/C.hs b/Data/SBV/Compilers/C.hs --- a/Data/SBV/Compilers/C.hs +++ b/Data/SBV/Compilers/C.hs @@ -633,7 +633,7 @@ p (ArrEq _ _) _ = tbd "User specified arrays (ArrEq)" p (Label s) [a] = a <+> text "/*" <+> text s <+> text "*/" p (IEEEFP w) as = handleIEEE w consts (zip opArgs as) var - p (IntCast _ to) [a] = parens (text (show to)) <+> a + p (KindCast _ to) [a] = parens (text (show to)) <+> a p (Uninterpreted s) [] = text "/* Uninterpreted constant */" <+> text s p (Uninterpreted s) as = text "/* Uninterpreted function */" <+> text s <> parens (fsep (punctuate comma as)) p (Extract i j) [a] = extract i j (head opArgs) a diff --git a/Data/SBV/Compilers/CodeGen.hs b/Data/SBV/Compilers/CodeGen.hs --- a/Data/SBV/Compilers/CodeGen.hs +++ b/Data/SBV/Compilers/CodeGen.hs @@ -19,8 +19,9 @@ import Control.Monad.State.Lazy (MonadState, StateT(..), modify) import Data.Char (toLower, isSpace) import Data.List (nub, isPrefixOf, intercalate, (\\)) -import System.Directory (createDirectory, doesDirectoryExist, doesFileExist) +import System.Directory (createDirectoryIfMissing, doesDirectoryExist, doesFileExist) import System.FilePath (()) +import System.IO (hFlush, stdout) import Text.PrettyPrint.HughesPJ (Doc, vcat) import qualified Text.PrettyPrint.HughesPJ as P (render) @@ -307,13 +308,14 @@ renderCgPgmBundle (Just dirName) (CgPgmBundle _ files) = do b <- doesDirectoryExist dirName unless b $ do putStrLn $ "Creating directory " ++ show dirName ++ ".." - createDirectory dirName + createDirectoryIfMissing True dirName dups <- filterM (\fn -> doesFileExist (dirName fn)) (map fst files) goOn <- case dups of [] -> return True _ -> do putStrLn $ "Code generation would override the following " ++ (if length dups == 1 then "file:" else "files:") mapM_ (\fn -> putStrLn ('\t' : fn)) dups putStr "Continue? [yn] " + hFlush stdout resp <- getLine return $ map toLower resp `isPrefixOf` "yes" if goOn then do mapM_ renderFile files diff --git a/Data/SBV/Dynamic.hs b/Data/SBV/Dynamic.hs --- a/Data/SBV/Dynamic.hs +++ b/Data/SBV/Dynamic.hs @@ -34,7 +34,7 @@ , svInteger, svAsInteger -- *** Float literals , svFloat, svDouble - -- ** Algrebraic reals (only from rationals) + -- *** Algebraic reals (only from rationals) , svReal, svNumerator, svDenominator -- *** Symbolic equality , svEqual, svNotEqual @@ -53,6 +53,8 @@ , svExtract, svJoin -- *** Sign-casting , svSign, svUnsign + -- *** Numeric conversions + , svFromIntegral -- *** Indexed lookups , svSelect -- *** Word-level operations diff --git a/Data/SBV/Examples/BitPrecise/BitTricks.hs b/Data/SBV/Examples/BitPrecise/BitTricks.hs --- a/Data/SBV/Examples/BitPrecise/BitTricks.hs +++ b/Data/SBV/Examples/BitPrecise/BitTricks.hs @@ -7,38 +7,38 @@ -- Stability : experimental -- -- Checks the correctness of a few tricks from the large collection found in: --- +-- ----------------------------------------------------------------------------- module Data.SBV.Examples.BitPrecise.BitTricks where import Data.SBV --- | Formalizes +-- | Formalizes fastMinCorrect :: SInt32 -> SInt32 -> SBool fastMinCorrect x y = m .== fm where m = ite (x .< y) x y fm = y `xor` ((x `xor` y) .&. (-(oneIf (x .< y)))); --- | Formalizes +-- | Formalizes fastMaxCorrect :: SInt32 -> SInt32 -> SBool fastMaxCorrect x y = m .== fm where m = ite (x .< y) y x fm = x `xor` ((x `xor` y) .&. (-(oneIf (x .< y)))); --- | Formalizes +-- | Formalizes oppositeSignsCorrect :: SInt32 -> SInt32 -> SBool oppositeSignsCorrect x y = r .== os where r = (x .< 0 &&& y .>= 0) ||| (x .>= 0 &&& y .< 0) os = (x `xor` y) .< 0 --- | Formalizes +-- | Formalizes conditionalSetClearCorrect :: SBool -> SWord32 -> SWord32 -> SBool conditionalSetClearCorrect f m w = r .== r' where r = ite f (w .|. m) (w .&. complement m) r' = w `xor` ((-(oneIf f) `xor` w) .&. m); --- | Formalizes +-- | Formalizes powerOfTwoCorrect :: SWord32 -> SBool powerOfTwoCorrect v = f .== s where f = (v ./= 0) &&& ((v .&. (v-1)) .== 0); diff --git a/Data/SBV/Examples/Misc/Enumerate.hs b/Data/SBV/Examples/Misc/Enumerate.hs --- a/Data/SBV/Examples/Misc/Enumerate.hs +++ b/Data/SBV/Examples/Misc/Enumerate.hs @@ -38,9 +38,9 @@ -- -- >>> elts -- Solution #1: --- s0 = A :: E --- Solution #2: -- s0 = B :: E +-- Solution #2: +-- s0 = A :: E -- Solution #3: -- s0 = C :: E -- Found 3 different solutions. diff --git a/Data/SBV/Examples/Puzzles/DogCatMouse.hs b/Data/SBV/Examples/Puzzles/DogCatMouse.hs --- a/Data/SBV/Examples/Puzzles/DogCatMouse.hs +++ b/Data/SBV/Examples/Puzzles/DogCatMouse.hs @@ -34,4 +34,4 @@ , dog + cat + mouse .== 100 -- buy precisely 100 animals , 15 `per` dog + 1 `per` cat + 0.25 `per` mouse .== 100 -- spend exactly 100 dollars ] - where p `per` q = p * sIntegerToSReal q + where p `per` q = p * (sFromIntegral q :: SReal) diff --git a/Data/SBV/Examples/Puzzles/U2Bridge.hs b/Data/SBV/Examples/Puzzles/U2Bridge.hs --- a/Data/SBV/Examples/Puzzles/U2Bridge.hs +++ b/Data/SBV/Examples/Puzzles/U2Bridge.hs @@ -249,18 +249,18 @@ -- Checking for solutions with 3 moves. -- Checking for solutions with 4 moves. -- Checking for solutions with 5 moves. --- Solution #1: --- 0 --> Edge, Bono --- 2 <-- Bono --- 3 --> Larry, Adam --- 13 <-- Edge --- 15 --> Edge, Bono --- Total time: 17 --- Solution #2: +-- Solution #1: -- 0 --> Edge, Bono -- 2 <-- Edge -- 4 --> Larry, Adam -- 14 <-- Bono +-- 15 --> Edge, Bono +-- Total time: 17 +-- Solution #2: +-- 0 --> Edge, Bono +-- 2 <-- Bono +-- 3 --> Larry, Adam +-- 13 <-- Edge -- 15 --> Edge, Bono -- Total time: 17 -- Found: 2 solutions with 5 moves. diff --git a/Data/SBV/Internals.hs b/Data/SBV/Internals.hs --- a/Data/SBV/Internals.hs +++ b/Data/SBV/Internals.hs @@ -13,30 +13,29 @@ module Data.SBV.Internals ( -- * Running symbolic programs /manually/ - Result(..), SBVRunMode(..), Symbolic, runSymbolic, runSymbolic' - -- * Other internal structures useful for low-level programming - , SBV(..), slet, CW(..), Kind(..), HasKind(..), CWVal(..), AlgReal(..), Quantifier(..), mkConstCW, genVar, genVar_ - , liftQRem, liftDMod, symbolicMergeWithKind - , cache, sbvToSW, newExpr, normCW, SBVExpr(..), Op(..) - , SBVType(..), newUninterpreted, forceSWArg + Result(..), SBVRunMode(..) + -- * Internal structures useful for low-level programming + , module Data.SBV.BitVectors.Data -- * Operations useful for instantiating SBV type classes - , genLiteral, genFromCW, genMkSymVar, checkAndConvert, genParse, showModel, SMTModel(..), smtLibReservedNames + , genLiteral, genFromCW, genMkSymVar, checkAndConvert, genParse, showModel, SMTModel(..), liftQRem, liftDMod -- * Polynomial operations that operate on bit-vectors , ites, mdp, addPoly -- * Compilation to C - , compileToC', compileToCLib', CgPgmBundle(..), CgPgmKind(..) + , compileToC', compileToCLib' + -- * Code generation primitives + , module Data.SBV.Compilers.CodeGen -- * Various math utilities around floats , module Data.SBV.Utils.Numeric ) where -import Data.SBV.BitVectors.Data ( Result(..), Symbolic, SBVRunMode(..), runSymbolic, runSymbolic', SBV(..), CW(..), Kind(..), HasKind(..), CWVal(..) - , AlgReal(..), Quantifier(..), mkConstCW, cache, sbvToSW, newExpr, normCW, SBVExpr(..), Op(..), SBVType(..) - , newUninterpreted, forceSWArg, SMTModel(..)) -import Data.SBV.BitVectors.Model (genVar, genVar_, slet, liftQRem, liftDMod, symbolicMergeWithKind, genLiteral, genFromCW, genMkSymVar) +import Data.SBV.BitVectors.Data +import Data.SBV.BitVectors.Model (genLiteral, genFromCW, genMkSymVar) import Data.SBV.BitVectors.Splittable (checkAndConvert) +import Data.SBV.BitVectors.Model (liftQRem, liftDMod) import Data.SBV.Compilers.C (compileToC', compileToCLib') -import Data.SBV.Compilers.CodeGen (CgPgmBundle(..), CgPgmKind(..)) +import Data.SBV.Compilers.CodeGen import Data.SBV.SMT.SMT (genParse, showModel) -import Data.SBV.SMT.SMTLibNames (smtLibReservedNames) import Data.SBV.Tools.Polynomial (ites, mdp, addPoly) import Data.SBV.Utils.Numeric + +{-# ANN module ("HLint: ignore Use import/export shortcut" :: String) #-} diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs --- a/Data/SBV/SMT/SMT.hs +++ b/Data/SBV/SMT/SMT.hs @@ -546,7 +546,7 @@ executeSolver `C.onException` (terminateProcess pid >> waitForProcess pid) -- | In case the SMT-Lib solver returns a response over multiple lines, compress them so we have --- each S-Expression spanning only a single line. We'll ignore things line parentheses inside quotes +-- each S-Expression spanning only a single line. We'll ignore things like parentheses inside quotes -- etc., as it should not be an issue mergeSExpr :: [String] -> [String] mergeSExpr [] = [] 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 @@ -238,9 +238,10 @@ t = "table" ++ show i mkElt x k = (isReady, (idx, ssw x)) where idx = cvtCW rm (mkConstCW aknd k) - isReady = x `elem` consts + isReady = x `Set.member` constsSet topLevel (idx, v) = "(= (" ++ t ++ " " ++ idx ++ ") " ++ v ++ ")" nested (idx, v) = "(= (" ++ t ++ args ++ " " ++ idx ++ ") " ++ v ++ ")" + constsSet = Set.fromList consts -- TODO: We currently do not support non-constant arrays when quantifiers are present, as -- we might have to skolemize those. Implement this properly. @@ -395,7 +396,7 @@ mkCnst = cvtCW rm . mkConstCW (kindOf i) le0 = "(" ++ less ++ " " ++ ssw i ++ " " ++ mkCnst 0 ++ ")" gtl = "(" ++ leq ++ " " ++ mkCnst l ++ " " ++ ssw i ++ ")" - sh (SBVApp (IntCast f t) [a]) = handleIntCast f t (ssw a) + sh (SBVApp (KindCast f t) [a]) = handleKindCast f t (ssw a) sh (SBVApp (ArrEq i j) []) = "(= array_" ++ show i ++ " array_" ++ show j ++")" sh (SBVApp (ArrRead i) [a]) = "(select array_" ++ show i ++ " " ++ ssw a ++ ")" sh (SBVApp (Uninterpreted nm) []) = nm @@ -581,9 +582,9 @@ c' = mkConstCW (kindOf x) c o = if s then oS else oW --- Various integer casts -handleIntCast :: Kind -> Kind -> String -> String -handleIntCast kFrom kTo a +-- Various casts +handleKindCast :: Kind -> Kind -> String -> String +handleKindCast kFrom kTo a | kFrom == kTo = a | True @@ -598,9 +599,13 @@ KBounded _ n -> i2b n _ -> noCast + KReal -> case kTo of + KUnbounded -> "(to_int " ++ a ++ ")" + _ -> noCast + _ -> noCast - where noCast = error $ "SBV.SMTLib2: Unexpected integer cast from: " ++ show kFrom ++ " to " ++ show kTo + where noCast = error $ "SBV.SMTLib2: Unexpected cast from: " ++ show kFrom ++ " to " ++ show kTo fromBV upConv m n | n > m = upConv (n - m) diff --git a/SBVUnitTest/GoldFiles/U2Bridge.gold b/SBVUnitTest/GoldFiles/U2Bridge.gold --- a/SBVUnitTest/GoldFiles/U2Bridge.gold +++ b/SBVUnitTest/GoldFiles/U2Bridge.gold @@ -3,13 +3,13 @@ s1 = Edge :: U2Member s2 = Bono :: U2Member s3 = True :: Bool - s4 = Bono :: U2Member + s4 = Edge :: U2Member s5 = Bono :: U2Member s6 = False :: Bool s7 = Larry :: U2Member s8 = Adam :: U2Member s9 = True :: Bool - s10 = Edge :: U2Member + s10 = Bono :: U2Member s11 = Bono :: U2Member s12 = False :: Bool s13 = Edge :: U2Member diff --git a/SBVUnitTest/GoldFiles/temperature.gold b/SBVUnitTest/GoldFiles/temperature.gold --- a/SBVUnitTest/GoldFiles/temperature.gold +++ b/SBVUnitTest/GoldFiles/temperature.gold @@ -1,5 +1,5 @@ Solution #1: - s0 = 16 :: Integer -Solution #2: s0 = 28 :: Integer +Solution #2: + s0 = 16 :: Integer Found 2 different solutions. diff --git a/SBVUnitTest/SBVUnitTestBuildTime.hs b/SBVUnitTest/SBVUnitTestBuildTime.hs --- a/SBVUnitTest/SBVUnitTestBuildTime.hs +++ b/SBVUnitTest/SBVUnitTestBuildTime.hs @@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String -buildTime = "Mon Jun 6 17:13:43 PDT 2016" +buildTime = "Sat Oct 29 10:15:43 PDT 2016" diff --git a/SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs b/SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs --- a/SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs +++ b/SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs @@ -160,7 +160,7 @@ where mkTest (x, r) = "intCast-" ++ x ~: r `showsAs` "True" lhs x = sFromIntegral (literal x) rhs x = literal (fromIntegral x) - cast :: forall a. (Show a, Integral a, Bits a, SymWord a) => [a] -> [(String, SBool)] + cast :: forall a. (Show a, Integral a, SymWord a) => [a] -> [(String, SBool)] cast xs = toWords xs ++ toInts xs toWords xs = [(show x, lhs x .== (rhs x :: SWord8 )) | x <- xs] ++ [(show x, lhs x .== (rhs x :: SWord16)) | x <- xs] diff --git a/SBVUnitTest/TestSuite/Basics/ArithSolver.hs b/SBVUnitTest/TestSuite/Basics/ArithSolver.hs --- a/SBVUnitTest/TestSuite/Basics/ArithSolver.hs +++ b/SBVUnitTest/TestSuite/Basics/ArithSolver.hs @@ -171,7 +171,7 @@ ++ cast i8s ++ cast i16s ++ cast i32s ++ cast i64s ++ cast iUBs where mkTest (x, t) = "sIntCast-" ++ x ~: assert t - cast :: forall a. (Show a, Integral a, Bits a, SymWord a) => [a] -> [(String, IO Bool)] + cast :: forall a. (Show a, Integral a, SymWord a) => [a] -> [(String, IO Bool)] cast xs = toWords xs ++ toInts xs toWords xs = [(show x, mkThm x (fromIntegral x :: Word8 )) | x <- xs] ++ [(show x, mkThm x (fromIntegral x :: Word16)) | x <- xs] diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,5 +1,5 @@ Name: sbv -Version: 5.12 +Version: 5.13 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