sbv 5.12 → 5.13

raw patch · 24 files changed

+137/−90 lines, 24 files

Files

• CHANGES.md +17/−1
• Data/SBV.hs +1/−1
• Data/SBV/BitVectors/AlgReals.hs +12/−8
• Data/SBV/BitVectors/Concrete.hs +5/−5
• Data/SBV/BitVectors/Kind.hs +2/−1
• Data/SBV/BitVectors/Model.hs +15/−9
• Data/SBV/BitVectors/Operations.hs +23/−11
• Data/SBV/BitVectors/Symbolic.hs +4/−4
• Data/SBV/Compilers/C.hs +1/−1
• Data/SBV/Compilers/CodeGen.hs +4/−2
• Data/SBV/Dynamic.hs +3/−1
• Data/SBV/Examples/BitPrecise/BitTricks.hs +6/−6
• Data/SBV/Examples/Misc/Enumerate.hs +2/−2
• Data/SBV/Examples/Puzzles/DogCatMouse.hs +1/−1
• Data/SBV/Examples/Puzzles/U2Bridge.hs +8/−8
• Data/SBV/Internals.hs +13/−14
• Data/SBV/SMT/SMT.hs +1/−1
• Data/SBV/SMT/SMTLib2.hs +11/−6
• SBVUnitTest/GoldFiles/U2Bridge.gold +2/−2
• SBVUnitTest/GoldFiles/temperature.gold +2/−2
• SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
• SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs +1/−1
• SBVUnitTest/TestSuite/Basics/ArithSolver.hs +1/−1
• sbv.cabal +1/−1

@@ -1,7 +1,23 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub:  <http://leventerkok.github.com/sbv/> -* 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 

@@ -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

@@ -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')

@@ -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

@@ -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

@@ -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

@@ -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)

@@ -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

@@ -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

@@ -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

@@ -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

@@ -7,38 +7,38 @@ -- Stability   :  experimental -- -- Checks the correctness of a few tricks from the large collection found in:---      <http://graphics.stanford.edu/~seander/bithacks.html>+--      <https://graphics.stanford.edu/~seander/bithacks.html> -----------------------------------------------------------------------------  module Data.SBV.Examples.BitPrecise.BitTricks where  import Data.SBV --- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax>+-- | Formalizes <https://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax> 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 <http://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax>+-- | Formalizes <https://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax> 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 <http://graphics.stanford.edu/~seander/bithacks.html#DetectOppositeSigns>+-- | Formalizes <https://graphics.stanford.edu/~seander/bithacks.html#DetectOppositeSigns> 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 <http://graphics.stanford.edu/~seander/bithacks.html#ConditionalSetOrClearBitsWithoutBranching>+-- | Formalizes <https://graphics.stanford.edu/~seander/bithacks.html#ConditionalSetOrClearBitsWithoutBranching> 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 <http://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2>+-- | Formalizes <https://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2> powerOfTwoCorrect :: SWord32 -> SBool powerOfTwoCorrect v = f .== s   where f = (v ./= 0) &&& ((v .&. (v-1)) .== 0);

@@ -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.

@@ -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)

@@ -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.

@@ -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) #-}

@@ -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 []       = []

@@ -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)

@@ -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

@@ -1,5 +1,5 @@ Solution #1:-  s0 = 16 :: Integer-Solution #2:   s0 = 28 :: Integer+Solution #2:+  s0 = 16 :: Integer Found 2 different solutions.

@@ -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"

@@ -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]

@@ -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]

@@ -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