sbv 1.3 → 1.4
raw patch · 39 files changed
+2116/−878 lines, 39 filesdep +sbv
Dependencies added: sbv
Files
- Data/SBV.hs +46/−7
- Data/SBV/BitVectors/AlgReals.hs +201/−0
- Data/SBV/BitVectors/Data.hs +260/−165
- Data/SBV/BitVectors/Model.hs +488/−263
- Data/SBV/BitVectors/PrettyNum.hs +31/−13
- Data/SBV/BitVectors/STree.hs +6/−4
- Data/SBV/BitVectors/SignCast.hs +14/−6
- Data/SBV/BitVectors/Splittable.hs +20/−18
- Data/SBV/Compilers/C.hs +26/−18
- Data/SBV/Compilers/CodeGen.hs +15/−8
- Data/SBV/Examples/BitPrecise/MergeSort.hs +95/−0
- Data/SBV/Examples/Existentials/Diophantine.hs +131/−0
- Data/SBV/Examples/Puzzles/Counts.hs +8/−9
- Data/SBV/Examples/Puzzles/DogCatMouse.hs +13/−22
- Data/SBV/Examples/Puzzles/Euler185.hs +5/−5
- Data/SBV/Examples/Puzzles/Sudoku.hs +7/−7
- Data/SBV/Internals.hs +6/−11
- Data/SBV/Provers/Prover.hs +15/−3
- Data/SBV/Provers/SExpr.hs +45/−12
- Data/SBV/Provers/Yices.hs +2/−2
- Data/SBV/Provers/Z3.hs +53/−31
- Data/SBV/SMT/SMT.hs +62/−38
- Data/SBV/SMT/SMTLib.hs +22/−14
- Data/SBV/SMT/SMTLib1.hs +42/−33
- Data/SBV/SMT/SMTLib2.hs +101/−83
- Data/SBV/Tools/ExpectedValue.hs +6/−4
- Data/SBV/Tools/GenTest.hs +82/−64
- Data/SBV/Tools/Polynomial.hs +9/−3
- Data/SBV/Utils/Lib.hs +7/−0
- README +5/−5
- RELEASENOTES +57/−2
- SBVUnitTest/GoldFiles/dogCatMouse.gold +3/−3
- SBVUnitTest/GoldFiles/merge.gold +152/−0
- SBVUnitTest/SBVUnitTest.hs +6/−4
- SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
- SBVUnitTest/TestSuite/Basics/Arithmetic.hs +47/−2
- SBVUnitTest/TestSuite/Puzzles/DogCatMouse.hs +8/−5
- SBVUnitTest/TestSuite/Puzzles/U2Bridge.hs +2/−2
- sbv.cabal +17/−11
Data/SBV.hs view
@@ -10,9 +10,9 @@ -- (The sbv library is hosted at <http://github.com/LeventErkok/sbv>. -- Comments, bug reports, and patches are always welcome.) ----- SBV: Symbolic Bit Vectors in Haskell+-- SBV: SMT Based Verification ----- Express properties about bit-precise Haskell programs and automatically prove+-- Express properties about Haskell programs and automatically prove -- them using SMT solvers. -- -- >>> prove $ \x -> x `shiftL` 2 .== 4 * (x :: SWord8)@@ -52,8 +52,8 @@ -- very similar to their concrete counterparts. In particular these types belong to the -- standard classes 'Num', 'Bits', custom versions of 'Eq' ('EqSymbolic') -- and 'Ord' ('OrdSymbolic'), along with several other custom classes for simplifying--- bit-precise programming with symbolic values. The framework takes full advantage--- of Haskell's type inference to avoid many common mistakes.+-- programming with symbolic values. The framework takes full advantage of Haskell's type+-- inference to avoid many common mistakes. -- -- Furthermore, predicates (i.e., functions that return 'SBool') built out of -- these types can also be:@@ -95,6 +95,15 @@ -- *** Signed unbounded integers -- $unboundedLimitations , SInteger+ -- *** Signed algebraic reals+ -- $algReals+ , SReal, AlgReal+ -- ** Creating a symbolic variable+ -- $createSym+ , sBool, sWord8, sWord16, sWord32, sWord64, sInt8, sInt16, sInt32, sInt64, sInteger+ -- ** Creating a list of symbolic variables+ -- $createSyms+ , sBools, sWord8s, sWord16s, sWord32s, sWord64s, sInt8s, sInt16s, sInt32s, sInt64s, sIntegers, sReal, sReals -- *** Abstract SBV type , SBV -- *** Arrays of symbolic values@@ -120,6 +129,8 @@ , EqSymbolic(..) -- ** Symbolic ordering , OrdSymbolic(..)+ -- ** Symbolic numbers+ , SNum -- ** Division , BVDivisible(..) -- ** The Boolean class@@ -146,6 +157,8 @@ , sat, satWith, isSatisfiable, isSatisfiableWithin -- ** Finding all satisfying assignments , allSat, allSatWith, numberOfModels+ -- ** Satisfying a sequence of boolean conditions+ , solve -- ** Adding constraints -- $constrainIntro , constrain, pConstrain@@ -181,7 +194,7 @@ , compileToSMTLib, generateSMTBenchmarks -- * Test case generation- , genTest, getTestValues, TestVectors, TestStyle(..), renderTest, CW(..), Size(..), cwToBool+ , genTest, getTestValues, TestVectors, TestStyle(..), renderTest, CW(..), Kind(..), cwToBool -- * Code generation from symbolic programs -- $cCodeGeneration@@ -211,8 +224,10 @@ , module Data.Bits , module Data.Word , module Data.Int+ , module Data.Ratio ) where +import Data.SBV.BitVectors.AlgReals import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.Model import Data.SBV.BitVectors.PrettyNum@@ -228,8 +243,9 @@ import Data.SBV.Tools.Polynomial import Data.SBV.Utils.Boolean import Data.Bits-import Data.Word import Data.Int+import Data.Ratio+import Data.Word -- Haddock section documentation {- $progIntro@@ -329,9 +345,19 @@ {- $moduleExportIntro The SBV library exports the following modules wholesale, as user programs will have to import these-three modules to make any sensible use of the SBV functionality.+modules to make any sensible use of the SBV functionality. -} +{- $createSym+These functions simplify declaring symbolic variables of various types. Strictly speaking, they are just synonyms+for 'free' (specialized at the given type), but they might be easier to use.+-}++{- $createSyms+These functions simplify declaring a sequence symbolic variables of various types. Strictly speaking, they are just synonyms+for 'mapM' 'free' (specialized at the given type), but they might be easier to use.+-}+ {- $unboundedLimitations The SBV library supports unbounded signed integers with the type 'SInteger', which are not subject to overflow/underflow as it is the case with the bounded types, such as 'SWord8', 'SInt16', etc. However,@@ -349,6 +375,19 @@ Usual arithmetic ('+', '-', '*', 'bvQuotRem') and logical operations ('.<', '.<=', '.>', '.>=', '.==', './=') operations are supported for 'SInteger' fully, both in programming and verification modes.+-}++{- $algReals+Algebraic reals are roots of single-variable polynomials with rational coefficients. (See+<http://en.wikipedia.org/wiki/Algebraic_number>.) Note that algebraic reals are infinite+precision numbers, but they do not cover all /real/ numbers. (In particular, they cannot+represent transcendentals.) Some irrational numbers are algebraic (such as @sqrt 2@), while+others are not (such as pi and e).++SBV can deal with real numbers just fine, since the theory of reals is decidable. (See+<http://goedel.cs.uiowa.edu/smtlib/theories/Reals.smt2>.) In addition, by leveraging backend+solver capabilities, SBV can also represent and solve non-linear equations involving real-variables.+(For instance, the Z3 SMT solver, supports polynomial constraints on reals starting with v4.0.) -} {- $constrainIntro
+ Data/SBV/BitVectors/AlgReals.hs view
@@ -0,0 +1,201 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.SBV.BitVectors.AlgReals+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+-- Portability : portable+--+-- Algrebraic reals in Haskell.+-----------------------------------------------------------------------------++{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}++module Data.SBV.BitVectors.AlgReals (AlgReal, mkPolyReal, algRealToSMTLib2, algRealToHaskell, mergeAlgReals) where++import Data.List (sortBy, isPrefixOf, partition)+import Data.Ratio ((%), numerator, denominator)+import Data.Function (on)+import System.Random++-- | Algebraic reals. Note that the representation is left abstract. We represent+-- rational results explicitly, while the roots-of-polynomials are represented+-- implicitly by their defining equation+data AlgReal = AlgRational Bool Rational -- bool says it's exact (i.e., SMT-solver did not return it with ? at the end.)+ | AlgPolyRoot (Integer, Polynomial) -- which root+ (Maybe String) -- approximate decimal representation with given precision, if available++-- | A univariate polynomial, represented simply as a+-- coefficient list. For instance, "5x^3 + 2x - 5" is+-- represented as [(5, 3), (2, 1), (-5, 0)]+newtype Polynomial = Polynomial [(Integer, Integer)]++-- | Construct a poly-root real with a given approximate value (either as a decimal, or polynomial-root)+mkPolyReal :: Either (Bool, String) (Integer, [(Integer, Integer)]) -> AlgReal+mkPolyReal (Left (exact, str))+ = case (str, break (== '.') str) of+ ("", (_, _)) -> AlgRational exact 0+ (_, (x, '.':y)) -> AlgRational exact (read (x++y) % (10 ^ length y))+ (_, (x, _)) -> AlgRational exact (read x % 1)+mkPolyReal (Right (k, coeffs))+ = AlgPolyRoot (k, Polynomial (normalize coeffs)) Nothing+ where normalize :: [(Integer, Integer)] -> [(Integer, Integer)]+ normalize = merge . reverse . sortBy (compare `on` snd)+ merge [] = []+ merge [x] = [x]+ merge ((a, b):r@((c, d):xs))+ | b == d = merge ((a+c, b):xs)+ | True = (a, b) : merge r++instance Show Polynomial where+ show (Polynomial xs) = chkEmpty (join (concat [term p | p@(_, x) <- xs, x /= 0])) ++ " = " ++ show c+ where c = -1 * head ([k | (k, 0) <- xs] ++ [0])+ term ( 0, _) = []+ term ( 1, 1) = [ "x"]+ term ( 1, p) = [ "x^" ++ show p]+ term (-1, 1) = ["-x"]+ term (-1, p) = ["-x^" ++ show p]+ term (k, 1) = [show k ++ "x"]+ term (k, p) = [show k ++ "x^" ++ show p]+ join [] = ""+ join (k:ks) = k ++ s ++ join ks+ where s = case ks of+ [] -> ""+ (y:_) | "-" `isPrefixOf` y -> ""+ | "+" `isPrefixOf` y -> ""+ | True -> "+"+ chkEmpty s = if null s then "0" else s++instance Show AlgReal where+ show (AlgRational exact a) = showRat exact a+ show (AlgPolyRoot (i, p) mbApprox) = "root(" ++ show i ++ ", " ++ show p ++ ")" ++ maybe "" app mbApprox+ where app v | last v == '?' = " = " ++ init v ++ "..."+ | True = " = " ++ v++-- lift unary op through an exact rational, otherwise bail+lift1 :: String -> (Rational -> Rational) -> AlgReal -> AlgReal+lift1 _ o (AlgRational e a) = AlgRational e (o a)+lift1 nm _ a = error $ "AlgReal." ++ nm ++ ": unsupported argument: " ++ show a++-- lift binary op through exact rationals, otherwise bail+lift2 :: String -> (Rational -> Rational -> Rational) -> AlgReal -> AlgReal -> AlgReal+lift2 _ o (AlgRational True a) (AlgRational True b) = AlgRational True (a `o` b)+lift2 nm _ a b = error $ "AlgReal." ++ nm ++ ": unsupported arguments: " ++ show (a, b)++-- The idea in the instances below is that we will fully support operations+-- on "AlgRational" AlgReals, but leave everything else undefined. When we are+-- on the Haskell side, the AlgReal's are *not* reachable. They only represent+-- return values from SMT solvers, which we should *not* need to manipulate.+instance Eq AlgReal where+ AlgRational True a == AlgRational True b = a == b+ a == b = error $ "AlgReal.==: unsupported arguments: " ++ show (a, b)++instance Ord AlgReal where+ AlgRational True a `compare` AlgRational True b = a `compare` b+ a `compare` b = error $ "AlgReal.compare: unsupported arguments: " ++ show (a, b)++instance Num AlgReal where+ (+) = lift2 "+" (+)+ (*) = lift2 "*" (*)+ (-) = lift2 "-" (-)+ negate = lift1 "negate" negate+ abs = lift1 "abs" abs+ signum = lift1 "signum" signum+ fromInteger = AlgRational True . fromInteger++instance Fractional AlgReal where+ (/) = lift2 "/" (/)+ fromRational = AlgRational True++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')++instance Random AlgReal where+ random g = let (a, g') = random g in (AlgRational True a, g')+ randomR (AlgRational True l, AlgRational True h) g = let (a, g') = randomR (l, h) g in (AlgRational True a, g')+ randomR lh _ = error $ "AlgReal.randomR: unsupported bounds: " ++ show lh++-- | Render an 'AlgReal' as an SMTLib2 value. Only supports rationals for the time being.+algRealToSMTLib2 :: AlgReal -> String+algRealToSMTLib2 (AlgRational True r)+ | m == 0 = "0.0"+ | m < 0 = "(- (/ " ++ show (abs m) ++ ".0 " ++ show n ++ ".0))"+ | True = "(/ " ++ show m ++ ".0 " ++ show n ++ ".0)"+ where (m, n) = (numerator r, denominator r)+algRealToSMTLib2 r@(AlgRational False _)+ = error $ "SBV: Unexpected inexact rational to be converted to SMTLib2: " ++ show r+algRealToSMTLib2 (AlgPolyRoot (i, Polynomial xs) _) = "(root-obj (+ " ++ unwords (concatMap term xs) ++ ") " ++ show i ++ ")"+ where term (0, _) = []+ term (k, 0) = [coeff k]+ term (1, 1) = ["x"]+ term (1, p) = ["(^ x " ++ show p ++ ")"]+ term (k, 1) = ["(* " ++ coeff k ++ " x)"]+ term (k, p) = ["(* " ++ coeff k ++ " (^ x " ++ show p ++ "))"]+ coeff n | n < 0 = "(- " ++ show (abs n) ++ ")"+ | True = show n++-- | Render an 'AlgReal' as a Haskell value. Only supports rationals, since there is no corresponding+-- standard Haskell type that can represent root-of-polynomial variety.+algRealToHaskell :: AlgReal -> String+algRealToHaskell (AlgRational True r) = "((" ++ show r ++ ") :: Rational)"+algRealToHaskell r = error $ "SBV.algRealToHaskell: Unsupported argument: " ++ show r++-- Try to show a rational precisely if we can, with finite number of+-- digits. Otherwise, show it as a rational value.+showRat :: Bool -> Rational -> String+showRat exact r = p $ case f25 (denominator r) [] of+ Nothing -> show r -- bail out, not precisely representable with finite digits+ Just (noOfZeros, num) -> let present = length num+ in neg $ case noOfZeros `compare` present of+ LT -> let (b, a) = splitAt (present - noOfZeros) num in b ++ "." ++ if null a then "0" else a+ EQ -> "0." ++ num+ GT -> "0." ++ replicate (noOfZeros - present) '0' ++ num+ where p = if exact then id else (++ "...")+ neg = if r < 0 then ('-':) else id+ -- factor a number in 2's and 5's if possible+ -- If so, it'll return the number of digits after the zero+ -- to reach the next power of 10, and the numerator value scaled+ -- appropriately and shown as a string+ f25 :: Integer -> [Integer] -> Maybe (Int, String)+ f25 1 sofar = let (ts, fs) = partition (== 2) sofar+ [lts, lfs] = map length [ts, fs]+ noOfZeros = lts `max` lfs+ in Just (noOfZeros, show (abs (numerator r) * factor ts fs))+ f25 v sofar = let (q2, r2) = v `quotRem` 2+ (q5, r5) = v `quotRem` 5+ in case (r2, r5) of+ (0, _) -> f25 q2 (2 : sofar)+ (_, 0) -> f25 q5 (5 : sofar)+ _ -> Nothing+ -- compute the next power of 10 we need to get to+ factor [] fs = product [2 | _ <- fs]+ factor ts [] = product [5 | _ <- ts]+ factor (_:ts) (_:fs) = factor ts fs++-- | Merge the representation of two algebraic reals, one assumed to be+-- in polynomial form, the other in decimal. Arguments can be the same+-- kind, so long as they are both rationals and equivalent; if not there+-- must be one that is precise. It's an error to pass anything+-- else to this function! (Used in reconstructing SMT counter-example values with reals).+mergeAlgReals :: String -> AlgReal -> AlgReal -> AlgReal+mergeAlgReals _ f@(AlgRational exact r) (AlgPolyRoot kp Nothing)+ | exact = f+ | True = AlgPolyRoot kp (Just (showRat False r))+mergeAlgReals _ (AlgPolyRoot kp Nothing) f@(AlgRational exact r)+ | exact = f+ | True = AlgPolyRoot kp (Just (showRat False r))+mergeAlgReals _ f@(AlgRational e1 r1) s@(AlgRational e2 r2)+ | (e1, r1) == (e2, r2) = f+ | e1 = f+ | e2 = s+mergeAlgReals m _ _ = error m
Data/SBV/BitVectors/Data.hs view
@@ -20,7 +20,7 @@ module Data.SBV.BitVectors.Data ( SBool, SWord8, SWord16, SWord32, SWord64- , SInt8, SInt16, SInt32, SInt64, SInteger+ , SInt8, SInt16, SInt32, SInt64, SInteger, SReal , SymWord(..) , CW(..), cwSameType, cwIsBit, cwToBool , mkConstCW ,liftCW2, mapCW, mapCW2@@ -29,8 +29,8 @@ , ArrayContext(..), ArrayInfo, SymArray(..), SFunArray(..), mkSFunArray, SArray(..), arrayUIKind , sbvToSW, sbvToSymSW , SBVExpr(..), newExpr- , cache, uncache, uncacheAI, HasSignAndSize(..)- , Op(..), NamedSymVar, UnintKind(..), getTableIndex, Pgm, Symbolic, runSymbolic, runSymbolic', State, inProofMode, SBVRunMode(..), Size(..), Outputtable(..), Result(..)+ , cache, uncache, uncacheAI, HasKind(..)+ , Op(..), NamedSymVar, UnintKind(..), getTableIndex, Pgm, Symbolic, runSymbolic, runSymbolic', State, inProofMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..) , getTraceInfo, getConstraints, addConstraint , SBVType(..), newUninterpreted, unintFnUIKind, addAxiom , Quantifier(..), needsExistentials@@ -46,7 +46,7 @@ import Data.Word (Word8, Word16, Word32, Word64) import Data.IORef (IORef, newIORef, modifyIORef, readIORef, writeIORef) import Data.List (intercalate, sortBy)-import Data.Maybe (isJust, fromJust, fromMaybe)+import Data.Maybe (isJust, fromJust) import qualified Data.IntMap as IMap (IntMap, empty, size, toAscList, lookup, insert, insertWith) import qualified Data.Map as Map (Map, empty, toList, size, insert, lookup)@@ -56,72 +56,103 @@ import System.Mem.StableName import System.Random +import Data.SBV.BitVectors.AlgReals import Data.SBV.Utils.Lib -- | 'CW' represents a concrete word of a fixed size: -- Endianness is mostly irrelevant (see the 'FromBits' class). -- For signed words, the most significant digit is considered to be the sign.-data CW = CW { cwSigned :: !Bool -- ^ Is the word signed?- , cwSize :: !Size -- ^ Size of the word (unbounded if Nothing)- , cwVal :: !Integer -- ^ The underlying value, represented as a Haskell 'Integer'+data CW = CW { cwKind :: !Kind -- ^ Kind of the word+ , cwVal :: !(Either AlgReal Integer) -- ^ The underlying value, represented as either an algebraic real (for SReal), or a Haskell 'Integer' (everything else) } deriving (Eq, Ord) +-- | Are two CW's of the same type? cwSameType :: CW -> CW -> Bool-cwSameType x y = cwSigned x == cwSigned y && cwSize x == cwSize y+cwSameType x y = cwKind x == cwKind y +-- | Is this a bit? cwIsBit :: CW -> Bool-cwIsBit x = not (hasSign x) && not (isInfPrec x) && intSizeOf x == 1+cwIsBit x = case cwKind x of+ KBounded False 1 -> True+ _ -> False -- | Convert a CW to a Haskell boolean cwToBool :: CW -> Bool-cwToBool x = cwVal x /= 0+cwToBool x = cwVal x /= Right 0 +-- | Normalize a CW. Essentially performs modular arithmetic to make sure the+-- value can fit in the given bit-size. Note that this is rather tricky for+-- negative values, due to asymmetry. (i.e., an 8-bit negative number represents+-- values in the range -128 to 127; thus we have to be careful on the negative side.) normCW :: CW -> CW-normCW x- | isInfPrec x = x- | True = x { cwVal = norm }- where sz = intSizeOf x- norm | sz == 0 = 0- | cwSigned x = let rg = 2 ^ (sz - 1)- in case divMod (cwVal x) rg of- (a, b) | even a -> b- (_, b) -> b - rg- | True = cwVal x `mod` (2 ^ sz)+normCW c@(CW (KBounded signed sz) (Right v)) = c { cwVal = Right norm }+ where norm | sz == 0 = 0+ | signed = let rg = 2 ^ (sz - 1)+ in case divMod v rg of+ (a, b) | even a -> b+ (_, b) -> b - rg+ | True = v `mod` (2 ^ sz)+normCW c = c -newtype Size = Size { unSize :: Maybe Int }- deriving (Eq, Ord)+-- | Kind of symbolic value+data Kind = KBounded Bool Int+ | KUnbounded+ | KReal+ deriving (Eq, Ord) +instance Show Kind where+ show (KBounded False 1) = "SBool"+ show (KBounded False n) = "SWord" ++ show n+ show (KBounded True n) = "SInt" ++ show n+ show KUnbounded = "SInteger"+ show KReal = "SReal"++-- | A symbolic node id newtype NodeId = NodeId Int deriving (Eq, Ord)-data SW = SW (Bool, Size) NodeId deriving (Eq, Ord) +-- | A symbolic word, tracking it's signedness and size.+data SW = SW Kind NodeId deriving (Eq, Ord)++-- | Quantifiers: forall or exists. Note that we allow+-- arbitrary nestings. data Quantifier = ALL | EX deriving Eq +-- | Are there any existential quantifiers? needsExistentials :: [Quantifier] -> Bool needsExistentials = (EX `elem`) -falseSW, trueSW :: SW-falseSW = SW (False, Size (Just 1)) $ NodeId (-2)-trueSW = SW (False, Size (Just 1)) $ NodeId (-1)+-- | Constant False as a SW. Note that this value always occupies slot -2.+falseSW :: SW+falseSW = SW (KBounded False 1) $ NodeId (-2) -falseCW, trueCW :: CW-falseCW = CW False (Size (Just 1)) 0-trueCW = CW False (Size (Just 1)) 1+-- | Constant False as a SW. Note that this value always occupies slot -1.+trueSW :: SW+trueSW = SW (KBounded False 1) $ NodeId (-1) -newtype SBVType = SBVType [(Bool, Size)]+-- | Constant False as a CW. We represent it using the integer value 0.+falseCW :: CW+falseCW = CW (KBounded False 1) (Right 0)++-- | Constant True as a CW. We represent it using the integer value 1.+trueCW :: CW+trueCW = CW (KBounded False 1) (Right 1)++-- | A simple type for SBV computations, used mainly for uninterpreted constants.+-- We keep track of the signedness/size of the arguments. A non-function will+-- have just one entry in the list.+newtype SBVType = SBVType [Kind] deriving (Eq, Ord) --- how many arguments does the type take?+-- | how many arguments does the type take? typeArity :: SBVType -> Int typeArity (SBVType xs) = length xs - 1 instance Show SBVType where show (SBVType []) = error "SBV: internal error, empty SBVType"- show (SBVType xs) = intercalate " -> " $ map sh xs- where sh (_, Size Nothing) = "SInteger"- sh (False, Size (Just 1)) = "SBool"- sh (s, Size (Just sz)) = (if s then "SInt" else "SWord") ++ show sz+ show (SBVType xs) = intercalate " -> " $ map show xs +-- | Symbolic operations data Op = Plus | Times | Minus | Quot | Rem -- quot and rem are unsigned only | Equal | NotEqual@@ -131,71 +162,92 @@ | Shl Int | Shr Int | Rol Int | Ror Int | Extract Int Int -- Extract i j: extract bits i to j. Least significant bit is 0 (big-endian) | Join -- Concat two words to form a bigger one, in the order given- | LkUp (Int, (Bool, Size), (Bool, Size), Int) !SW !SW -- (table-index, arg-type, res-type, length of the table) index out-of-bounds-value+ | 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 | ArrRead Int | Uninterpreted String deriving (Eq, Ord) +-- | A symbolic expression data SBVExpr = SBVApp !Op ![SW] deriving (Eq, Ord) ---- minimal complete definition: sizeOf, hasSign-class HasSignAndSize a where- sizeOf :: a -> Size+-- | A class for capturing values that have a sign and a size (finite or infinite)+-- minimal complete definition: kindOf+class HasKind a where+ kindOf :: a -> Kind hasSign :: a -> Bool intSizeOf :: a -> Int- isInfPrec :: a -> Bool+ isBounded :: a -> Bool+ isReal :: a -> Bool+ isInteger :: a -> Bool showType :: a -> String- showType a- | isInfPrec a = "SInteger"- | not (hasSign a) && intSizeOf a == 1 = "SBool"- | True = (if hasSign a then "SInt" else "SWord") ++ show (intSizeOf a)- isInfPrec = maybe True (const False) . unSize . sizeOf- intSizeOf = fromMaybe (error "SBV.HasSignAndSize.bitSize((S)Integer)") . unSize . sizeOf+ -- defaults+ hasSign x = case kindOf x of+ KBounded b _ -> b+ KUnbounded -> True+ KReal -> True+ intSizeOf x = case kindOf x of+ KBounded _ s -> s+ KUnbounded -> error "SBV.HasKind.intSizeOf((S)Integer)"+ KReal -> error "SBV.HasKind.intSizeOf((S)Real)"+ isBounded x = case kindOf x of+ KBounded{} -> True+ KUnbounded -> False+ KReal -> False+ isReal x = case kindOf x of+ KBounded{} -> False+ KUnbounded -> False+ KReal -> True+ isInteger x = case kindOf x of+ KBounded{} -> False+ KUnbounded -> True+ KReal -> False+ showType = show . kindOf -instance HasSignAndSize Bool where {sizeOf _ = Size (Just 1) ; hasSign _ = False}-instance HasSignAndSize Int8 where {sizeOf _ = Size (Just 8) ; hasSign _ = True }-instance HasSignAndSize Word8 where {sizeOf _ = Size (Just 8) ; hasSign _ = False}-instance HasSignAndSize Int16 where {sizeOf _ = Size (Just 16); hasSign _ = True }-instance HasSignAndSize Word16 where {sizeOf _ = Size (Just 16); hasSign _ = False}-instance HasSignAndSize Int32 where {sizeOf _ = Size (Just 32); hasSign _ = True }-instance HasSignAndSize Word32 where {sizeOf _ = Size (Just 32); hasSign _ = False}-instance HasSignAndSize Int64 where {sizeOf _ = Size (Just 64); hasSign _ = True }-instance HasSignAndSize Word64 where {sizeOf _ = Size (Just 64); hasSign _ = False}-instance HasSignAndSize Integer where {sizeOf _ = Size Nothing; hasSign _ = True}+instance HasKind Bool where kindOf _ = KBounded False 1+instance HasKind Int8 where kindOf _ = KBounded True 8+instance HasKind Word8 where kindOf _ = KBounded False 8+instance HasKind Int16 where kindOf _ = KBounded True 16+instance HasKind Word16 where kindOf _ = KBounded False 16+instance HasKind Int32 where kindOf _ = KBounded True 32+instance HasKind Word32 where kindOf _ = KBounded False 32+instance HasKind Int64 where kindOf _ = KBounded True 64+instance HasKind Word64 where kindOf _ = KBounded False 64+instance HasKind Integer where kindOf _ = KUnbounded+instance HasKind AlgReal where kindOf _ = KReal -liftCW :: (Integer -> b) -> CW -> b-liftCW f x = f (cwVal x)+-- | Lift a unary function thruough a CW+liftCW :: (AlgReal -> b) -> (Integer -> b) -> CW -> b+liftCW f g = either f g . cwVal -liftCW2 :: (Integer -> Integer -> b) -> CW -> CW -> b-liftCW2 f x y | cwSameType x y = f (cwVal x) (cwVal y)-liftCW2 _ a b = error $ "SBV.liftCW2: impossible, incompatible args received: " ++ show (a, b)+-- | Lift a binary function through a CW+liftCW2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> CW -> CW -> b+liftCW2 f g x y = case (cwVal x, cwVal y) of+ (Left a, Left b) -> f a b+ (Right a, Right b) -> g a b+ _ -> error $ "SBV.liftCW2: impossible, incompatible args received: " ++ show (x, y) -mapCW :: (Integer -> Integer) -> CW -> CW-mapCW f x = normCW $ x { cwVal = f (cwVal x) }+-- | Map a unary function through a CW+mapCW :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> CW -> CW+mapCW f g x = normCW $ CW (cwKind x) (either (Left . f) (Right . g) (cwVal x)) -mapCW2 :: (Integer -> Integer -> Integer) -> CW -> CW -> CW-mapCW2 f x y- | cwSameType x y = normCW $ CW (cwSigned x) (cwSize y) (f (cwVal x) (cwVal y))-mapCW2 _ a b = error $ "SBV.mapCW2: impossible, incompatible args received: " ++ show (a, b)+-- | Map a binary function through a CW+mapCW2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> CW -> CW -> CW+mapCW2 f g x y = case (cwSameType x y, cwVal x, cwVal y) of+ (True, Left a, Left b) -> normCW $ CW (cwKind x) (Left (f a b))+ (True, Right a, Right b) -> normCW $ CW (cwKind x) (Right (g a b))+ _ -> error $ "SBV.mapCW2: impossible, incompatible args received: " ++ show (x, y) -instance HasSignAndSize CW where- intSizeOf = maybe (error "attempting to compute size of SInteger") id . unSize . cwSize- sizeOf = cwSize- hasSign = cwSigned- isInfPrec = maybe True (const False) . unSize . cwSize+instance HasKind CW where+ kindOf = cwKind -instance HasSignAndSize SW where- sizeOf (SW (_, s) _) = s- intSizeOf (SW (_, mbs) _) = maybe (error "attempting to compute size of SInteger") id $ unSize mbs- isInfPrec (SW (_, mbs) _) = maybe True (const False) $ unSize mbs- hasSign (SW (b, _) _) = b+instance HasKind SW where+ kindOf (SW k _) = k instance Show CW where show w | cwIsBit w = show (cwToBool w)- show w = liftCW show w ++ " :: " ++ showType w+ show w = liftCW show show w ++ " :: " ++ showType w instance Show SW where show (SW _ (NodeId n))@@ -210,11 +262,7 @@ show (Extract i j) = "choose [" ++ show i ++ ":" ++ show j ++ "]" show (LkUp (ti, at, rt, l) i e) = "lookup(" ++ tinfo ++ ", " ++ show i ++ ", " ++ show e ++ ")"- where tinfo = "table" ++ show ti ++ "(" ++ mkT at ++ " -> " ++ mkT rt ++ ", " ++ show l ++ ")"- mkT (_, Size Nothing) = "SInteger"- mkT (b, Size (Just s))- | s == 1 = "SBool"- | True = if b then "SInt" else "SWord" ++ show s+ 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 (Uninterpreted i) = "uninterpreted_" ++ i@@ -231,6 +279,8 @@ , (Join, "#") ] +-- | To improve hash-consing, take advantage of commutative operators by+-- reordering their arguments. reorder :: SBVExpr -> SBVExpr reorder s = case s of SBVApp op [a, b] | isCommutative op && a > b -> SBVApp op [b, a]@@ -248,7 +298,7 @@ show (SBVApp op args) = unwords (show op : map show args) -- | A program is a sequence of assignments-type Pgm = S.Seq (SW, SBVExpr)+type Pgm = S.Seq (SW, SBVExpr) -- | 'NamedSymVar' pairs symbolic words and user given/automatically generated names type NamedSymVar = (SW, String)@@ -259,22 +309,24 @@ deriving Show -- | Result of running a symbolic computation-data Result = Result Bool -- contains unbounded integers- [(String, CW)] -- quick-check counter-example information (if any)- [(String, [String])] -- uninterpeted code segments- [(Quantifier, NamedSymVar)] -- inputs (possibly existential)- [(SW, CW)] -- constants- [((Int, (Bool, Size), (Bool, Size)), [SW])] -- tables (automatically constructed) (tableno, index-type, result-type) elts- [(Int, ArrayInfo)] -- arrays (user specified)- [(String, SBVType)] -- uninterpreted constants- [(String, [String])] -- axioms- Pgm -- assignments- [SW] -- additional constraints (boolean)- [SW] -- outputs+data Result = Result Bool -- contains unbounded integers+ [(String, CW)] -- quick-check counter-example information (if any)+ [(String, [String])] -- uninterpeted code segments+ [(Quantifier, NamedSymVar)] -- inputs (possibly existential)+ [(SW, CW)] -- constants+ [((Int, Kind, Kind), [SW])] -- tables (automatically constructed) (tableno, index-type, result-type) elts+ [(Int, ArrayInfo)] -- arrays (user specified)+ [(String, SBVType)] -- uninterpreted constants+ [(String, [String])] -- axioms+ Pgm -- assignments+ [SW] -- additional constraints (boolean)+ [SW] -- outputs +-- | Extract the constraints from a result getConstraints :: Result -> [SW] getConstraints (Result _ _ _ _ _ _ _ _ _ _ cstrs _) = cstrs +-- | Extract the traced-values from a result (quick-check) getTraceInfo :: Result -> [(String, CW)] getTraceInfo (Result _ tvals _ _ _ _ _ _ _ _ _ _) = tvals @@ -304,7 +356,7 @@ ++ ["OUTPUTS"] ++ map ((" " ++) . show) os where shs sw = show sw ++ " :: " ++ showType sw- sht ((i, at, rt), es) = " Table " ++ show i ++ " : " ++ mkT at ++ "->" ++ mkT rt ++ " = " ++ show es+ sht ((i, at, rt), es) = " Table " ++ show i ++ " : " ++ show at ++ "->" ++ show rt ++ " = " ++ show es shc (sw, cw) = " " ++ show sw ++ " = " ++ show cw shcg (s, ss) = ("Variable: " ++ s) : map (" " ++) ss shn (q, (sw, nm)) = " " ++ ni ++ " :: " ++ showType sw ++ ex ++ alias@@ -313,22 +365,19 @@ | True = ", existential" alias | ni == nm = "" | True = ", aliasing " ++ show nm- sha (i, (nm, (ai, bi), ctx)) = " " ++ ni ++ " :: " ++ mkT ai ++ " -> " ++ mkT bi ++ alias+ sha (i, (nm, (ai, bi), ctx)) = " " ++ ni ++ " :: " ++ show ai ++ " -> " ++ show bi ++ alias ++ "\n Context: " ++ show ctx where ni = "array_" ++ show i alias | ni == nm = "" | True = ", aliasing " ++ show nm shui (nm, t) = " uninterpreted_" ++ nm ++ " :: " ++ show t shax (nm, ss) = " -- user defined axiom: " ++ nm ++ "\n " ++ intercalate "\n " ss- mkT (_, Size Nothing) = "SInteger"- mkT (b, Size (Just s))- | s == 1 = "SBool"- | True = if b then "SInt" else "SWord" ++ show s -data ArrayContext = ArrayFree (Maybe SW)- | ArrayReset Int SW- | ArrayMutate Int SW SW- | ArrayMerge SW Int Int+-- | The context of a symbolic array as created+data ArrayContext = ArrayFree (Maybe SW) -- ^ A new array, with potential initializer for each cell+ | ArrayReset Int SW -- ^ An array created from another array by fixing each element to another value+ | ArrayMutate Int SW SW -- ^ An array created by mutating another array at a given cell+ | ArrayMerge SW Int Int -- ^ An array created by symbolically merging two other arrays instance Show ArrayContext where show (ArrayFree Nothing) = " initialized with random elements"@@ -337,18 +386,35 @@ show (ArrayMutate i a b) = " cloned from array_" ++ show i ++ " with " ++ show a ++ " :: " ++ showType a ++ " |-> " ++ show b ++ " :: " ++ showType b show (ArrayMerge s i j) = " merged arrays " ++ show i ++ " and " ++ show j ++ " on condition " ++ show s +-- | Expression map, used for hash-consing type ExprMap = Map.Map SBVExpr SW++-- | Constants are stored in a map, for hash-consing type CnstMap = Map.Map CW SW-type TableMap = Map.Map [SW] (Int, (Bool, Size), (Bool, Size))-type ArrayInfo = (String, ((Bool, Size), (Bool, Size)), ArrayContext)++-- | Tables generated during a symbolic run+type TableMap = Map.Map [SW] (Int, Kind, Kind)++-- | Representation for symbolic arrays+type ArrayInfo = (String, (Kind, Kind), ArrayContext)++-- | Arrays generated during a symbolic run type ArrayMap = IMap.IntMap ArrayInfo++-- | Uninterpreted-constants generated during a symbolic run type UIMap = Map.Map String SBVType++-- | Code-segments for Uninterpreted-constants, as given by the user type CgMap = Map.Map String [String]++-- | Cached values, implementing sharing type Cache a = IMap.IntMap [(StableName (State -> IO a), a)] +-- | Convert an SBV-type to the kind-of uninterpreted value it represents unintFnUIKind :: (String, SBVType) -> (String, UnintKind) unintFnUIKind (s, t) = (s, UFun (typeArity t) s) +-- | Convert an array value type to the kind-of uninterpreted value it represents arrayUIKind :: (Int, ArrayInfo) -> Maybe (String, UnintKind) arrayUIKind (i, (nm, _, ctx)) | external ctx = Just ("array_" ++ show i, UArr 1 nm) -- arrays are always 1-dimensional in the SMT-land. (Unless encoded explicitly)@@ -363,16 +429,18 @@ | CodeGen -- ^ Code generation mode | Concrete StdGen -- ^ Concrete simulation mode. The StdGen is for the pConstrain acceptance in cross runs +-- | Is this a concrete run? (i.e., quick-check or test-generation like) isConcreteMode :: SBVRunMode -> Bool isConcreteMode (Concrete _) = True isConcreteMode (Proof{}) = False isConcreteMode CodeGen = False +-- | The state of the symbolic interpreter data State = State { runMode :: SBVRunMode , rStdGen :: IORef StdGen , rCInfo :: IORef [(String, CW)] , rctr :: IORef Int- , rInfPrec :: IORef Bool+ , rBounded :: IORef Bool , rinps :: IORef [(Quantifier, NamedSymVar)] , rConstraints :: IORef [SW] , routs :: IORef [SW]@@ -388,6 +456,7 @@ , rAICache :: IORef (Cache Int) } +-- | Are we running in proof mode? inProofMode :: State -> Bool inProofMode s = case runMode s of Proof{} -> True@@ -398,7 +467,7 @@ -- value (@Right Cached@). Note that caching is essential for making -- sure sharing is preserved. The parameter 'a' is phantom, but is -- extremely important in keeping the user interface strongly typed.-data SBV a = SBV !(Bool, Size) !(Either CW (Cached SW))+data SBV a = SBV !Kind !(Either CW (Cached SW)) -- | A symbolic boolean/bit type SBool = SBV Bool@@ -430,36 +499,40 @@ -- | Infinite precision signed symbolic value type SInteger = SBV Integer +-- | Infinite precision symbolic algebraic real value+type SReal = SBV AlgReal+ -- Not particularly "desirable", but will do if needed instance Show (SBV a) where- show (SBV _ (Left c)) = show c- show (SBV (_ , Size Nothing) (Right _)) = "<symbolic> :: SInteger"- show (SBV (sgn, Size (Just sz)) (Right _)) = "<symbolic> :: " ++ t- where t | not sgn && sz == 1 = "SBool"- | True = (if sgn then "SInt" else "SWord") ++ show sz+ show (SBV _ (Left c)) = show c+ show (SBV k (Right _)) = "<symbolic> :: " ++ show k +-- Equality constraint on SBV values. Not desirable since we can't really compare two+-- symbolic values, but will do. instance Eq (SBV a) where SBV _ (Left a) == SBV _ (Left b) = a == b a == b = error $ "Comparing symbolic bit-vectors; Use (.==) instead. Received: " ++ show (a, b) SBV _ (Left a) /= SBV _ (Left b) = a /= b a /= b = error $ "Comparing symbolic bit-vectors; Use (./=) instead. Received: " ++ show (a, b) -instance HasSignAndSize a => HasSignAndSize (SBV a) where- sizeOf _ = sizeOf (undefined :: a)- hasSign _ = hasSign (undefined :: a)+instance HasKind a => HasKind (SBV a) where+ kindOf _ = kindOf (undefined :: a) +-- | Increment the variable counter incCtr :: State -> IO Int incCtr s = do ctr <- readIORef (rctr s) let i = ctr + 1 i `seq` writeIORef (rctr s) i return ctr +-- | Generate a random value, for quick-check and test-gen purposes throwDice :: State -> IO Double throwDice st = do g <- readIORef (rStdGen st) let (r, g') = randomR (0, 1) g writeIORef (rStdGen st) g' return r +-- | Create a new uninterpreted symbol, possibly with user given code newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO () newUninterpreted st nm t mbCode | null nm || not (isAlpha (head nm)) || not (all validChar (tail nm))@@ -476,20 +549,20 @@ when (isJust mbCode) $ modifyIORef (rCgMap st) (Map.insert nm (fromJust mbCode)) where validChar x = isAlphaNum x || x `elem` "_" --- Create a new constant; hash-cons as necessary+-- | Create a new constant; hash-cons as necessary newConst :: State -> CW -> IO SW newConst st c = do constMap <- readIORef (rconstMap st) case c `Map.lookup` constMap of Just sw -> return sw Nothing -> do ctr <- incCtr st- let sw = SW (hasSign c, sizeOf c) (NodeId ctr)- when (isInfPrec sw) $ writeIORef (rInfPrec st) True+ let sw = SW (kindOf c) (NodeId ctr)+ when (not (isBounded sw)) $ writeIORef (rBounded st) False modifyIORef (rconstMap st) (Map.insert c sw) return sw --- Create a new table; hash-cons as necessary-getTableIndex :: State -> (Bool, Size) -> (Bool, Size) -> [SW] -> IO Int+-- | Create a new table; hash-cons as necessary+getTableIndex :: State -> Kind -> Kind -> [SW] -> IO Int getTableIndex st at rt elts = do tblMap <- readIORef (rtblMap st) case elts `Map.lookup` tblMap of@@ -498,24 +571,26 @@ modifyIORef (rtblMap st) (Map.insert elts (i, at, rt)) return i --- Create a constant word-mkConstCW :: Integral a => (Bool, Size) -> a -> CW-mkConstCW (signed, size) a = normCW $ CW signed size (toInteger a)+-- | Create a constant word+mkConstCW :: Integral a => Kind -> a -> CW+mkConstCW KReal a = normCW $ CW KReal (Left (fromInteger (toInteger a)))+mkConstCW k a = normCW $ CW k (Right (toInteger a)) --- Create a new expression; hash-cons as necessary-newExpr :: State -> (Bool, Size) -> SBVExpr -> IO SW-newExpr st sgnsz app = do+-- | Create a new expression; hash-cons as necessary+newExpr :: State -> Kind -> SBVExpr -> IO SW+newExpr st k app = do let e = reorder app exprMap <- readIORef (rexprMap st) case e `Map.lookup` exprMap of Just sw -> return sw Nothing -> do ctr <- incCtr st- let sw = SW sgnsz (NodeId ctr)- when (isInfPrec sw) $ writeIORef (rInfPrec st) True+ let sw = SW k (NodeId ctr)+ when (not (isBounded sw)) $ writeIORef (rBounded st) False modifyIORef (spgm st) (flip (S.|>) (sw, e)) modifyIORef (rexprMap st) (Map.insert e sw) return sw +-- | Convert a symbolic value to a symbolic-word sbvToSW :: State -> SBV a -> IO SW sbvToSW st (SBV _ (Left c)) = newConst st c sbvToSW st (SBV _ (Right f)) = uncache f st@@ -529,8 +604,10 @@ newtype Symbolic a = Symbolic (ReaderT State IO a) deriving (Functor, Monad, MonadIO, MonadReader State) -mkSymSBV :: forall a. (Random a, SymWord a) => Maybe Quantifier -> (Bool, Size) -> Maybe String -> Symbolic (SBV a)-mkSymSBV mbQ sgnsz mbNm = do+-- | Create a symbolic value, based on the quantifier we have. If an explicit quantifier is given, we just use that.+-- If not, then we pick existential for SAT calls and universal for everything else.+mkSymSBV :: forall a. (Random a, SymWord a) => Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a)+mkSymSBV mbQ k mbNm = do st <- ask let q = case (mbQ, runMode st) of (Just x, _) -> x -- user given, just take it@@ -547,19 +624,21 @@ return v _ -> do ctr <- liftIO $ incCtr st let nm = maybe ('s':show ctr) id mbNm- sw = SW sgnsz (NodeId ctr)- when (isInfPrec sw) $ liftIO $ writeIORef (rInfPrec st) True+ sw = SW k (NodeId ctr)+ when (not (isBounded sw)) $ liftIO $ writeIORef (rBounded st) False liftIO $ modifyIORef (rinps st) ((q, (sw, nm)):)- return $ SBV sgnsz $ Right $ cache (const (return sw))+ return $ SBV k $ Right $ cache (const (return sw)) +-- | Convert a symbolic value to an SW, inside the Symbolic monad sbvToSymSW :: SBV a -> Symbolic SW sbvToSymSW sbv = do st <- ask liftIO $ sbvToSW st sbv --- | Mark an interim result as an output. Useful when constructing Symbolic programs--- that return multiple values, or when the result is programmatically computed.+-- | A class representing what can be returned from a symbolic computation. class Outputtable a where+ -- | Mark an interim result as an output. Useful when constructing Symbolic programs+ -- that return multiple values, or when the result is programmatically computed. output :: a -> Symbolic a instance Outputtable (SBV a) where@@ -631,7 +710,7 @@ axioms <- newIORef [] swCache <- newIORef IMap.empty aiCache <- newIORef IMap.empty- infPrec <- newIORef False+ bounded <- newIORef True cstrs <- newIORef [] rGen <- case currentRunMode of Concrete g -> newIORef g@@ -640,7 +719,7 @@ , rStdGen = rGen , rCInfo = cInfo , rctr = ctr- , rInfPrec = infPrec+ , rBounded = bounded , rinps = inps , routs = outs , rtblMap = tables@@ -655,8 +734,8 @@ , rAICache = aiCache , rConstraints = cstrs }- _ <- newConst st (mkConstCW (False, Size (Just 1)) (0::Integer)) -- s(-2) == falseSW- _ <- newConst st (mkConstCW (False, Size (Just 1)) (1::Integer)) -- s(-1) == trueSW+ _ <- newConst st (mkConstCW (KBounded False 1) (0::Integer)) -- s(-2) == falseSW+ _ <- newConst st (mkConstCW (KBounded False 1) (1::Integer)) -- s(-1) == trueSW r <- runReaderT c st rpgm <- readIORef pgm inpsO <- reverse `fmap` readIORef inps@@ -668,11 +747,11 @@ arrs <- IMap.toAscList `fmap` readIORef arrays unint <- Map.toList `fmap` readIORef uis axs <- reverse `fmap` readIORef axioms- hasInfPrec <- readIORef infPrec+ allBounded <- readIORef bounded cgMap <- Map.toList `fmap` readIORef cgs traceVals <- reverse `fmap` readIORef cInfo extraCstrs <- reverse `fmap` readIORef cstrs- return $ (r, Result hasInfPrec traceVals cgMap inpsO cnsts tbls arrs unint axs rpgm extraCstrs outsO)+ return $ (r, Result (not allBounded) traceVals cgMap inpsO cnsts tbls arrs unint axs rpgm extraCstrs outsO) ------------------------------------------------------------------------------- -- * Symbolic Words@@ -683,7 +762,7 @@ -- provide the necessary bits. -- -- Minimal complete definiton: forall, forall_, exists, exists_, literal, fromCW-class (HasSignAndSize a, Ord a) => SymWord a where+class (HasKind a, Ord a) => SymWord a where -- | Create a user named input (universal) forall :: String -> Symbolic (SBV a) -- | Create an automatically named input@@ -702,6 +781,10 @@ free_ :: Symbolic (SBV a) -- | Create a bunch of free vars mkFreeVars :: Int -> Symbolic [SBV a]+ -- | Similar to free; Just a more convenient name+ symbolic :: String -> Symbolic (SBV a)+ -- | Similar to mkFreeVars; but automatically gives names based on the strings+ symbolics :: [String] -> Symbolic [SBV a] -- | Turn a literal constant to symbolic literal :: a -> SBV a -- | Extract a literal, if the value is concrete@@ -722,6 +805,8 @@ mkForallVars n = mapM (const forall_) [1 .. n] mkExistVars n = mapM (const exists_) [1 .. n] mkFreeVars n = mapM (const free_) [1 .. n]+ symbolic = free+ symbolics = mapM symbolic unliteral (SBV _ (Left c)) = Just $ fromCW c unliteral _ = Nothing isConcrete (SBV _ (Left _)) = True@@ -755,9 +840,9 @@ -- Minimal complete definition: All methods are required, no defaults. class SymArray array where -- | Create a new array, with an optional initial value- newArray_ :: (HasSignAndSize a, HasSignAndSize b) => Maybe (SBV b) -> Symbolic (array a b)+ newArray_ :: (HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (array a b) -- | Create a named new array, with an optional initial value- newArray :: (HasSignAndSize a, HasSignAndSize b) => String -> Maybe (SBV b) -> Symbolic (array a b)+ newArray :: (HasKind a, HasKind b) => String -> Maybe (SBV b) -> Symbolic (array a b) -- | Read the array element at @a@ readArray :: array a b -> SBV a -> SBV b -- | Reset all the elements of the array to the value @b@@@ -781,19 +866,21 @@ -- -- * Typically slower as it heavily relies on SMT-solving for the array theory ---data SArray a b = SArray ((Bool, Size), (Bool, Size)) (Cached ArrayIndex)+data SArray a b = SArray (Kind, Kind) (Cached ArrayIndex)++-- | An array index is simple an int value type ArrayIndex = Int -instance (HasSignAndSize a, HasSignAndSize b) => Show (SArray a b) where+instance (HasKind a, HasKind b) => Show (SArray a b) where show (SArray{}) = "SArray<" ++ showType (undefined :: a) ++ ":" ++ showType (undefined :: b) ++ ">" instance SymArray SArray where newArray_ = declNewSArray (\t -> "array_" ++ show t) newArray n = declNewSArray (const n)- readArray (SArray (_, bsgnsz) f) a = SBV bsgnsz $ Right $ cache r+ readArray (SArray (_, bk) f) a = SBV bk $ Right $ cache r where r st = do arr <- uncacheAI f st i <- sbvToSW st a- newExpr st bsgnsz (SBVApp (ArrRead arr) [i])+ newExpr st bk (SBVApp (ArrRead arr) [i]) resetArray (SArray ainfo f) b = SArray ainfo $ cache g where g st = do amap <- readIORef (rArrayMap st) val <- sbvToSW st b@@ -818,10 +905,11 @@ k `seq` modifyIORef (rArrayMap st) (IMap.insert k ("array_" ++ show k, ainfo, ArrayMerge ts ai bi)) return k -declNewSArray :: forall a b. (HasSignAndSize a, HasSignAndSize b) => (Int -> String) -> Maybe (SBV b) -> Symbolic (SArray a b)+-- | Declare a new symbolic array, with a potential initial value+declNewSArray :: forall a b. (HasKind a, HasKind b) => (Int -> String) -> Maybe (SBV b) -> Symbolic (SArray a b) declNewSArray mkNm mbInit = do- let asgnsz = (hasSign (undefined :: a), sizeOf (undefined :: a))- bsgnsz = (hasSign (undefined :: b), sizeOf (undefined :: b))+ let aknd = kindOf (undefined :: a)+ bknd = kindOf (undefined :: b) st <- ask amap <- liftIO $ readIORef $ rArrayMap st let i = IMap.size amap@@ -829,8 +917,8 @@ actx <- liftIO $ case mbInit of Nothing -> return $ ArrayFree Nothing Just ival -> sbvToSW st ival >>= \sw -> return $ ArrayFree (Just sw)- liftIO $ modifyIORef (rArrayMap st) (IMap.insert i (nm, (asgnsz, bsgnsz), actx))- return $ SArray (asgnsz, bsgnsz) $ cache $ const $ return i+ liftIO $ modifyIORef (rArrayMap st) (IMap.insert i (nm, (aknd, bknd), actx))+ return $ SArray (aknd, bknd) $ cache $ const $ return i -- | Arrays implemented internally as functions --@@ -846,14 +934,13 @@ -- data SFunArray a b = SFunArray (SBV a -> SBV b) -instance (HasSignAndSize a, HasSignAndSize b) => Show (SFunArray a b) where+instance (HasKind a, HasKind b) => Show (SFunArray a b) where show (SFunArray _) = "SFunArray<" ++ showType (undefined :: a) ++ ":" ++ showType (undefined :: b) ++ ">" -- | Lift a function to an array. Useful for creating arrays in a pure context. (Otherwise use `newArray`.) mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b mkSFunArray = SFunArray - -- | Handling constraints imposeConstraint :: SBool -> Symbolic () imposeConstraint c = do st <- ask@@ -862,6 +949,7 @@ _ -> do liftIO $ do v <- sbvToSW st c modifyIORef (rConstraints st) (v:) +-- | Add a constraint with a given probability addConstraint :: Maybe Double -> SBool -> SBool -> Symbolic () addConstraint Nothing c _ = imposeConstraint c addConstraint (Just t) c c'@@ -879,7 +967,7 @@ -- * Cached values --------------------------------------------------------------------------------- --- We implement a peculiar caching mechanism, applicable to the use case in+-- | We implement a peculiar caching mechanism, applicable to the use case in -- implementation of SBV's. Whenever we do a state based computation, we do -- not want to keep on evaluating it in the then-current state. That will -- produce essentially a semantically equivalent value. Thus, we want to run@@ -887,19 +975,25 @@ -- level. This is similar to the "type-safe observable sharing" work, but also -- takes into the account of how symbolic simulation executes. --+-- See Andy Gill's type-safe obervable sharing trick for the inspiration behind+-- this technique: <http://ittc.ku.edu/~andygill/paper.php?label=DSLExtract09>+-- -- Note that this is *not* a general memo utility!- newtype Cached a = Cached (State -> IO a) +-- | Cache a state-based computation cache :: (State -> IO a) -> Cached a cache = Cached +-- | Uncache a previously cached computation uncache :: Cached SW -> State -> IO SW uncache = uncacheGen rSWCache +-- | Uncache, retrieving array indexes uncacheAI :: Cached ArrayIndex -> State -> IO ArrayIndex uncacheAI = uncacheGen rAICache +-- | Generic uncaching. Note that this is entirely safe, since we do it in the IO monad. uncacheGen :: (State -> IORef (Cache a)) -> Cached a -> State -> IO a uncacheGen getCache (Cached f) st = do let rCache = getCache st@@ -912,12 +1006,13 @@ r `seq` modifyIORef rCache (IMap.insertWith (++) h [(sn, r)]) return r --- Representation of SMTLib Programs+-- | Representation of SMTLib Program versions, currently we only know of versions 1 and 2.+-- (NB. Eventually, we should just drop SMTLib1.) data SMTLibVersion = SMTLib1 | SMTLib2 deriving Eq --- in between pre and post goes the refuted models+-- | Representation of an SMT-Lib program. In between pre and post goes the refuted models data SMTLibPgm = SMTLibPgm SMTLibVersion ( [(String, SW)] -- alias table , [String] -- pre: declarations. , [String]) -- post: formula@@ -929,13 +1024,13 @@ -- Other Technicalities.. instance NFData CW where- rnf (CW x y z) = x `seq` y `seq` z `seq` ()+ rnf (CW x y) = x `seq` y `seq` () instance NFData Result where rnf (Result isInf qcInfo cgs inps consts tbls arrs uis axs pgm cstr outs) = rnf isInf `seq` rnf qcInfo `seq` rnf cgs `seq` rnf inps `seq` rnf consts `seq` rnf tbls `seq` rnf arrs `seq` rnf uis `seq` rnf axs `seq` rnf pgm `seq` rnf cstr `seq` rnf outs -instance NFData Size+instance NFData Kind instance NFData ArrayContext instance NFData Pgm instance NFData SW
Data/SBV/BitVectors/Model.hs view
@@ -22,10 +22,12 @@ {-# LANGUAGE Rank2Types #-} module Data.SBV.BitVectors.Model (- Mergeable(..), EqSymbolic(..), OrdSymbolic(..), BVDivisible(..), Uninterpreted(..)+ Mergeable(..), EqSymbolic(..), OrdSymbolic(..), BVDivisible(..), Uninterpreted(..), SNum , sbvTestBit, sbvPopCount, setBitTo, allEqual, allDifferent, oneIf, blastBE, blastLE- , lsb, msb, SBVUF, sbvUFName, genFinVar, genFinVar_, forall, forall_, exists, exists_- , constrain, pConstrain+ , lsb, msb, SBVUF, sbvUFName, genVar, genVar_, forall, forall_, exists, exists_+ , constrain, pConstrain, sBool, sBools, sWord8, sWord8s, sWord16, sWord16s, sWord32+ , sWord32s, sWord64, sWord64s, sInt8, sInt8s, sInt16, sInt16s, sInt32, sInt32s, sInt64+ , sInt64s, sInteger, sIntegers, sReal, sReals ) where @@ -34,7 +36,7 @@ import Data.Array (Array, Ix, listArray, elems, bounds, rangeSize) import Data.Bits (Bits(..)) import Data.Int (Int8, Int16, Int32, Int64)-import Data.List (genericLength, genericIndex, genericSplitAt, unzip4, unzip5, unzip6, unzip7, intercalate)+import Data.List (genericLength, genericIndex, unzip4, unzip5, unzip6, unzip7, intercalate) import Data.Maybe (fromMaybe) import Data.Word (Word8, Word16, Word32, Word64) @@ -43,197 +45,301 @@ import qualified Test.QuickCheck.Monadic as QC (monadicIO, run) import System.Random +import Data.SBV.BitVectors.AlgReals import Data.SBV.BitVectors.Data import Data.SBV.Utils.Boolean -liftSym1 :: (State -> (Bool, Size) -> SW -> IO SW) ->- (Integer -> Integer) -> SBV b -> SBV b-liftSym1 _ opC (SBV sgnsz (Left a)) = SBV sgnsz $ Left $ mapCW opC a-liftSym1 opS _ a@(SBV sgnsz _) = SBV sgnsz $ Right $ cache c+liftSym1 :: (State -> Kind -> SW -> IO SW) -> (AlgReal -> AlgReal) -> (Integer -> Integer) -> SBV b -> SBV b+liftSym1 _ opCR opCI (SBV k (Left a)) = SBV k $ Left $ mapCW opCR opCI a+liftSym1 opS _ _ a@(SBV k _) = SBV k $ Right $ cache c where c st = do swa <- sbvToSW st a- opS st sgnsz swa+ opS st k swa -liftSym2 :: (State -> (Bool, Size) -> SW -> SW -> IO SW) ->- (Integer -> Integer -> Integer) -> SBV b -> SBV b -> SBV b-liftSym2 _ opC (SBV sgnsz (Left a)) (SBV _ (Left b)) = SBV sgnsz $ Left $ mapCW2 opC a b-liftSym2 opS _ a@(SBV sgnsz _) b = SBV sgnsz $ Right $ cache c+liftSym2 :: (State -> Kind -> SW -> SW -> IO SW) -> (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> SBV b -> SBV b -> SBV b+liftSym2 _ opCR opCI (SBV k (Left a)) (SBV _ (Left b)) = SBV k $ Left $ mapCW2 opCR opCI a b+liftSym2 opS _ _ a@(SBV k _) b = SBV k $ Right $ cache c where c st = do sw1 <- sbvToSW st a sw2 <- sbvToSW st b- opS st sgnsz sw1 sw2+ opS st k sw1 sw2 -liftSym2B :: (State -> (Bool, Size) -> SW -> SW -> IO SW)- -> (Integer -> Integer -> Bool)- -> SBV b -> SBV b -> SBool-liftSym2B _ opC (SBV _ (Left a)) (SBV _ (Left b)) = literal (liftCW2 opC a b)-liftSym2B opS _ a b = SBV (False, Size (Just 1)) $ Right $ cache c+liftSym2B :: (State -> Kind -> SW -> SW -> IO SW) -> (AlgReal -> AlgReal -> Bool) -> (Integer -> Integer -> Bool) -> SBV b -> SBV b -> SBool+liftSym2B _ opCR opCI (SBV _ (Left a)) (SBV _ (Left b)) = literal (liftCW2 opCR opCI a b)+liftSym2B opS _ _ a b = SBV (KBounded False 1) $ Right $ cache c where c st = do sw1 <- sbvToSW st a sw2 <- sbvToSW st b- opS st (False, Size (Just 1)) sw1 sw2+ opS st (KBounded False 1) sw1 sw2 -liftSym1Bool :: (State -> (Bool, Size) -> SW -> IO SW)- -> (Bool -> Bool)+liftSym1Bool :: (State -> Kind -> SW -> IO SW) -> (Bool -> Bool) -> SBool -> SBool liftSym1Bool _ opC (SBV _ (Left a)) = literal $ opC $ cwToBool a-liftSym1Bool opS _ a = SBV (False, Size (Just 1)) $ Right $ cache c+liftSym1Bool opS _ a = SBV (KBounded False 1) $ Right $ cache c where c st = do sw <- sbvToSW st a- opS st (False, Size (Just 1)) sw+ opS st (KBounded False 1) sw -liftSym2Bool :: (State -> (Bool, Size) -> SW -> SW -> IO SW)- -> (Bool -> Bool -> Bool)- -> SBool -> SBool -> SBool+liftSym2Bool :: (State -> Kind -> SW -> SW -> IO SW) -> (Bool -> Bool -> Bool) -> SBool -> SBool -> SBool liftSym2Bool _ opC (SBV _ (Left a)) (SBV _ (Left b)) = literal (cwToBool a `opC` cwToBool b)-liftSym2Bool opS _ a b = SBV (False, Size (Just 1)) $ Right $ cache c+liftSym2Bool opS _ a b = SBV (KBounded False 1) $ Right $ cache c where c st = do sw1 <- sbvToSW st a sw2 <- sbvToSW st b- opS st (False, Size (Just 1)) sw1 sw2+ opS st (KBounded False 1) sw1 sw2 -mkSymOpSC :: (SW -> SW -> Maybe SW) -> Op -> State -> (Bool, Size) -> SW -> SW -> IO SW-mkSymOpSC shortCut op st sgnsz a b = maybe (newExpr st sgnsz (SBVApp op [a, b])) return (shortCut a b)+mkSymOpSC :: (SW -> SW -> Maybe SW) -> Op -> State -> Kind -> SW -> SW -> IO SW+mkSymOpSC shortCut op st k a b = maybe (newExpr st k (SBVApp op [a, b])) return (shortCut a b) -mkSymOp :: Op -> State -> (Bool, Size) -> SW -> SW -> IO SW+mkSymOp :: Op -> State -> Kind -> SW -> SW -> IO SW mkSymOp = mkSymOpSC (const (const Nothing)) -mkSymOp1SC :: (SW -> Maybe SW) -> Op -> State -> (Bool, Size) -> SW -> IO SW-mkSymOp1SC shortCut op st sgnsz a = maybe (newExpr st sgnsz (SBVApp op [a])) return (shortCut a)+mkSymOp1SC :: (SW -> Maybe SW) -> Op -> State -> Kind -> SW -> IO SW+mkSymOp1SC shortCut op st k a = maybe (newExpr st k (SBVApp op [a])) return (shortCut a) -mkSymOp1 :: Op -> State -> (Bool, Size) -> SW -> IO SW+mkSymOp1 :: Op -> State -> Kind -> SW -> IO SW mkSymOp1 = mkSymOp1SC (const Nothing) -- Symbolic-Word class instances -genFinVar :: (Random a, SymWord a) => Maybe Quantifier -> (Bool, Int) -> String -> Symbolic (SBV a)-genFinVar q (sg, sz) = mkSymSBV q (sg, Size (Just sz)) . Just+-- | Generate a finite symbolic bitvector, named+genVar :: (Random a, SymWord a) => Maybe Quantifier -> Kind -> String -> Symbolic (SBV a)+genVar q k = mkSymSBV q k . Just -genFinVar_ :: (Random a, SymWord a) => Maybe Quantifier -> (Bool, Int) -> Symbolic (SBV a)-genFinVar_ q (sg, sz) = mkSymSBV q (sg, Size (Just sz)) Nothing+-- | Generate a finite symbolic bitvector, unnamed+genVar_ :: (Random a, SymWord a) => Maybe Quantifier -> Kind -> Symbolic (SBV a)+genVar_ q k = mkSymSBV q k Nothing -genFinLiteral :: Integral a => (Bool, Int) -> a -> SBV b-genFinLiteral (sg, sz) = SBV s . Left . mkConstCW s- where s = (sg, Size (Just sz))+-- | Generate a finite constant bitvector+genLiteral :: Integral a => Kind -> a -> SBV b+genLiteral k = SBV k . Left . mkConstCW k +-- | Convert a constant to an integral value genFromCW :: Integral a => CW -> a-genFromCW x = fromInteger (cwVal x)+genFromCW (CW _ (Right x)) = fromInteger x+genFromCW c = error $ "genFromCW: Unsupported AlgReal value: " ++ show c instance SymWord Bool where- forall = genFinVar (Just ALL) (False, 1)- forall_ = genFinVar_ (Just ALL) (False, 1)- exists = genFinVar (Just EX) (False, 1)- exists_ = genFinVar_ (Just EX) (False, 1)- free = genFinVar Nothing (False, 1)- free_ = genFinVar_ Nothing (False, 1)- literal x = genFinLiteral (False, 1) (if x then (1::Integer) else 0)+ forall = genVar (Just ALL) (KBounded False 1)+ forall_ = genVar_ (Just ALL) (KBounded False 1)+ exists = genVar (Just EX) (KBounded False 1)+ exists_ = genVar_ (Just EX) (KBounded False 1)+ free = genVar Nothing (KBounded False 1)+ free_ = genVar_ Nothing (KBounded False 1)+ literal x = genLiteral (KBounded False 1) (if x then (1::Integer) else 0) fromCW = cwToBool mbMaxBound = Just maxBound mbMinBound = Just minBound instance SymWord Word8 where- forall = genFinVar (Just ALL) (False, 8)- forall_ = genFinVar_ (Just ALL) (False, 8)- exists = genFinVar (Just EX) (False, 8)- exists_ = genFinVar_ (Just EX) (False, 8)- free = genFinVar Nothing (False, 8)- free_ = genFinVar_ Nothing (False, 8)- literal = genFinLiteral (False, 8)+ forall = genVar (Just ALL) (KBounded False 8)+ forall_ = genVar_ (Just ALL) (KBounded False 8)+ exists = genVar (Just EX) (KBounded False 8)+ exists_ = genVar_ (Just EX) (KBounded False 8)+ free = genVar Nothing (KBounded False 8)+ free_ = genVar_ Nothing (KBounded False 8)+ literal = genLiteral (KBounded False 8) fromCW = genFromCW mbMaxBound = Just maxBound mbMinBound = Just minBound instance SymWord Int8 where- forall = genFinVar (Just ALL) (True, 8)- forall_ = genFinVar_ (Just ALL) (True, 8)- exists = genFinVar (Just EX) (True, 8)- exists_ = genFinVar_ (Just EX) (True, 8)- free = genFinVar Nothing (True, 8)- free_ = genFinVar_ Nothing (True, 8)- literal = genFinLiteral (True, 8)+ forall = genVar (Just ALL) (KBounded True 8)+ forall_ = genVar_ (Just ALL) (KBounded True 8)+ exists = genVar (Just EX) (KBounded True 8)+ exists_ = genVar_ (Just EX) (KBounded True 8)+ free = genVar Nothing (KBounded True 8)+ free_ = genVar_ Nothing (KBounded True 8)+ literal = genLiteral (KBounded True 8) fromCW = genFromCW mbMaxBound = Just maxBound mbMinBound = Just minBound instance SymWord Word16 where- forall = genFinVar (Just ALL) (False, 16)- forall_ = genFinVar_ (Just ALL) (False, 16)- exists = genFinVar (Just EX) (False, 16)- exists_ = genFinVar_ (Just EX) (False, 16)- free = genFinVar Nothing (False, 16)- free_ = genFinVar_ Nothing (False, 16)- literal = genFinLiteral (False, 16)+ forall = genVar (Just ALL) (KBounded False 16)+ forall_ = genVar_ (Just ALL) (KBounded False 16)+ exists = genVar (Just EX) (KBounded False 16)+ exists_ = genVar_ (Just EX) (KBounded False 16)+ free = genVar Nothing (KBounded False 16)+ free_ = genVar_ Nothing (KBounded False 16)+ literal = genLiteral (KBounded False 16) fromCW = genFromCW mbMaxBound = Just maxBound mbMinBound = Just minBound instance SymWord Int16 where- forall = genFinVar (Just ALL) (True, 16)- forall_ = genFinVar_ (Just ALL) (True, 16)- exists = genFinVar (Just EX) (True, 16)- exists_ = genFinVar_ (Just EX) (True, 16)- free = genFinVar Nothing (True, 16)- free_ = genFinVar_ Nothing (True, 16)- literal = genFinLiteral (True, 16)+ forall = genVar (Just ALL) (KBounded True 16)+ forall_ = genVar_ (Just ALL) (KBounded True 16)+ exists = genVar (Just EX) (KBounded True 16)+ exists_ = genVar_ (Just EX) (KBounded True 16)+ free = genVar Nothing (KBounded True 16)+ free_ = genVar_ Nothing (KBounded True 16)+ literal = genLiteral (KBounded True 16) fromCW = genFromCW mbMaxBound = Just maxBound mbMinBound = Just minBound instance SymWord Word32 where- forall = genFinVar (Just ALL) (False, 32)- forall_ = genFinVar_ (Just ALL) (False, 32)- exists = genFinVar (Just EX) (False, 32)- exists_ = genFinVar_ (Just EX) (False, 32)- free = genFinVar Nothing (False, 32)- free_ = genFinVar_ Nothing (False, 32)- literal = genFinLiteral (False, 32)+ forall = genVar (Just ALL) (KBounded False 32)+ forall_ = genVar_ (Just ALL) (KBounded False 32)+ exists = genVar (Just EX) (KBounded False 32)+ exists_ = genVar_ (Just EX) (KBounded False 32)+ free = genVar Nothing (KBounded False 32)+ free_ = genVar_ Nothing (KBounded False 32)+ literal = genLiteral (KBounded False 32) fromCW = genFromCW mbMaxBound = Just maxBound mbMinBound = Just minBound instance SymWord Int32 where- forall = genFinVar (Just ALL) (True, 32)- forall_ = genFinVar_ (Just ALL) (True, 32)- exists = genFinVar (Just EX) (True, 32)- exists_ = genFinVar_ (Just EX) (True, 32)- free = genFinVar Nothing (True, 32)- free_ = genFinVar_ Nothing (True, 32)- literal = genFinLiteral (True, 32)+ forall = genVar (Just ALL) (KBounded True 32)+ forall_ = genVar_ (Just ALL) (KBounded True 32)+ exists = genVar (Just EX) (KBounded True 32)+ exists_ = genVar_ (Just EX) (KBounded True 32)+ free = genVar Nothing (KBounded True 32)+ free_ = genVar_ Nothing (KBounded True 32)+ literal = genLiteral (KBounded True 32) fromCW = genFromCW mbMaxBound = Just maxBound mbMinBound = Just minBound instance SymWord Word64 where- forall = genFinVar (Just ALL) (False, 64)- forall_ = genFinVar_ (Just ALL) (False, 64)- exists = genFinVar (Just EX) (False, 64)- exists_ = genFinVar_ (Just EX) (False, 64)- free = genFinVar Nothing (False, 64)- free_ = genFinVar_ Nothing (False, 64)- literal = genFinLiteral (False, 64)+ forall = genVar (Just ALL) (KBounded False 64)+ forall_ = genVar_ (Just ALL) (KBounded False 64)+ exists = genVar (Just EX) (KBounded False 64)+ exists_ = genVar_ (Just EX) (KBounded False 64)+ free = genVar Nothing (KBounded False 64)+ free_ = genVar_ Nothing (KBounded False 64)+ literal = genLiteral (KBounded False 64) fromCW = genFromCW mbMaxBound = Just maxBound mbMinBound = Just minBound instance SymWord Int64 where- forall = genFinVar (Just ALL) (True, 64)- forall_ = genFinVar_ (Just ALL) (True, 64)- exists = genFinVar (Just EX) (True, 64)- exists_ = genFinVar_ (Just EX) (True, 64)- free = genFinVar Nothing (True, 64)- free_ = genFinVar_ Nothing (True, 64)- literal = genFinLiteral (True, 64)+ forall = genVar (Just ALL) (KBounded True 64)+ forall_ = genVar_ (Just ALL) (KBounded True 64)+ exists = genVar (Just EX) (KBounded True 64)+ exists_ = genVar_ (Just EX) (KBounded True 64)+ free = genVar Nothing (KBounded True 64)+ free_ = genVar_ Nothing (KBounded True 64)+ literal = genLiteral (KBounded True 64) fromCW = genFromCW mbMaxBound = Just maxBound mbMinBound = Just minBound instance SymWord Integer where- forall = mkSymSBV (Just ALL) (True, Size Nothing) . Just- forall_ = mkSymSBV (Just ALL) (True, Size Nothing) Nothing- exists = mkSymSBV (Just EX) (True, Size Nothing) . Just- exists_ = mkSymSBV (Just EX) (True, Size Nothing) Nothing- free = mkSymSBV Nothing (True, Size Nothing) . Just- free_ = mkSymSBV Nothing (True, Size Nothing) Nothing- literal = SBV (True, Size Nothing) . Left . mkConstCW (True, Size Nothing)+ forall = mkSymSBV (Just ALL) KUnbounded . Just+ forall_ = mkSymSBV (Just ALL) KUnbounded Nothing+ exists = mkSymSBV (Just EX) KUnbounded . Just+ exists_ = mkSymSBV (Just EX) KUnbounded Nothing+ free = mkSymSBV Nothing KUnbounded . Just+ free_ = mkSymSBV Nothing KUnbounded Nothing+ literal = SBV KUnbounded . Left . mkConstCW KUnbounded fromCW = genFromCW mbMaxBound = Nothing mbMinBound = Nothing +instance SymWord AlgReal where+ forall = mkSymSBV (Just ALL) KReal . Just+ forall_ = mkSymSBV (Just ALL) KReal Nothing+ exists = mkSymSBV (Just EX) KReal . Just+ exists_ = mkSymSBV (Just EX) KReal Nothing+ free = mkSymSBV Nothing KReal . Just+ free_ = mkSymSBV Nothing KReal Nothing+ literal = SBV KReal . Left . CW KReal . Left+ fromCW (CW _ (Left a)) = a+ fromCW c = error $ "SymWord.AlgReal: Unexpected non-real value: " ++ show c+ mbMaxBound = Nothing+ mbMinBound = Nothing++------------------------------------------------------------------------------------+-- * Smart constructors for creating symbolic values. These are not strictly+-- necessary, as they are mere aliases for 'symbolic' and 'symbolics', but +-- they nonetheless make programming easier.+------------------------------------------------------------------------------------+-- | Declare an 'SBool'+sBool :: String -> Symbolic SBool+sBool = symbolic++-- | Declare a list of 'SBool's+sBools :: [String] -> Symbolic [SBool]+sBools = symbolics++-- | Declare an 'SWord8'+sWord8 :: String -> Symbolic SWord8+sWord8 = symbolic++-- | Declare a list of 'SWord8's+sWord8s :: [String] -> Symbolic [SWord8]+sWord8s = symbolics++-- | Declare an 'SWord16'+sWord16 :: String -> Symbolic SWord16+sWord16 = symbolic++-- | Declare a list of 'SWord16's+sWord16s :: [String] -> Symbolic [SWord16]+sWord16s = symbolics++-- | Declare an 'SWord32'+sWord32 :: String -> Symbolic SWord32+sWord32 = symbolic++-- | Declare a list of 'SWord32's+sWord32s :: [String] -> Symbolic [SWord32]+sWord32s = symbolics++-- | Declare an 'SWord64'+sWord64 :: String -> Symbolic SWord64+sWord64 = symbolic++-- | Declare a list of 'SWord64's+sWord64s :: [String] -> Symbolic [SWord64]+sWord64s = symbolics++-- | Declare an 'SInt8'+sInt8 :: String -> Symbolic SInt8+sInt8 = symbolic++-- | Declare a list of 'SInt8's+sInt8s :: [String] -> Symbolic [SInt8]+sInt8s = symbolics++-- | Declare an 'SInt16'+sInt16 :: String -> Symbolic SInt16+sInt16 = symbolic++-- | Declare a list of 'SInt16's+sInt16s :: [String] -> Symbolic [SInt16]+sInt16s = symbolics++-- | Declare an 'SInt32'+sInt32 :: String -> Symbolic SInt32+sInt32 = symbolic++-- | Declare a list of 'SInt32's+sInt32s :: [String] -> Symbolic [SInt32]+sInt32s = symbolics++-- | Declare an 'SInt64'+sInt64 :: String -> Symbolic SInt64+sInt64 = symbolic++-- | Declare a list of 'SInt64's+sInt64s :: [String] -> Symbolic [SInt64]+sInt64s = symbolics++-- | Declare an 'SInteger'+sInteger:: String -> Symbolic SInteger+sInteger = symbolic++-- | Declare a list of 'SInteger's+sIntegers :: [String] -> Symbolic [SInteger]+sIntegers = symbolics++-- | Declare an 'SReal'+sReal:: String -> Symbolic SReal+sReal = symbolic++-- | Declare a list of 'SReal's+sReals :: [String] -> Symbolic [SReal]+sReals = symbolics+ -- | Symbolic Equality. Note that we can't use Haskell's 'Eq' class since Haskell insists on returning Bool -- Comparing symbolic values will necessarily return a symbolic value. --@@ -274,8 +380,8 @@ -} instance EqSymbolic (SBV a) where- (.==) = liftSym2B (mkSymOpSC (eqOpt trueSW) Equal) (==)- (./=) = liftSym2B (mkSymOpSC (eqOpt falseSW) NotEqual) (/=)+ (.==) = liftSym2B (mkSymOpSC (eqOpt trueSW) Equal) (==) (==)+ (./=) = liftSym2B (mkSymOpSC (eqOpt falseSW) NotEqual) (/=) (/=) eqOpt :: SW -> SW -> SW -> Maybe SW eqOpt w x y = if x == y then Just w else Nothing@@ -284,19 +390,19 @@ x .< y | Just mb <- mbMaxBound, x `isConcretely` (== mb) = false | Just mb <- mbMinBound, y `isConcretely` (== mb) = false- | True = liftSym2B (mkSymOpSC (eqOpt falseSW) LessThan) (<) x y+ | True = liftSym2B (mkSymOpSC (eqOpt falseSW) LessThan) (<) (<) x y x .<= y | Just mb <- mbMinBound, x `isConcretely` (== mb) = true | Just mb <- mbMaxBound, y `isConcretely` (== mb) = true- | True = liftSym2B (mkSymOpSC (eqOpt trueSW) LessEq) (<=) x y+ | True = liftSym2B (mkSymOpSC (eqOpt trueSW) LessEq) (<=) (<=) x y x .> y | Just mb <- mbMinBound, x `isConcretely` (== mb) = false | Just mb <- mbMaxBound, y `isConcretely` (== mb) = false- | True = liftSym2B (mkSymOpSC (eqOpt falseSW) GreaterThan) (>) x y+ | True = liftSym2B (mkSymOpSC (eqOpt falseSW) GreaterThan) (>) (>) x y x .>= y | Just mb <- mbMaxBound, x `isConcretely` (== mb) = true | Just mb <- mbMinBound, y `isConcretely` (== mb) = true- | True = liftSym2B (mkSymOpSC (eqOpt trueSW) GreaterEq) (>=) x y+ | True = liftSym2B (mkSymOpSC (eqOpt trueSW) GreaterEq) (>=) (>=) x y -- Bool instance EqSymbolic Bool where@@ -382,6 +488,31 @@ (a0, b0, c0, d0, e0, f0, g0) .< (a1, b1, c1, d1, e1, f1, g1) = (a0, b0, c0, d0, e0, f0) .< (a1, b1, c1, d1, e1, f1) ||| ((a0, b0, c0, d0, e0, f0) .== (a1, b1, c1, d1, e1, f1) &&& g0 .< g1) +-- | Symbolic Numbers. This is a simple class that simply incorporates all 'OrdSymbolic' and+-- 'Num' values together, simplifying writing polymorphic type-signatures that work for all+-- symbolic numbers, such as 'SWord8', 'SInt8' etc. For instance, we can write a generic+-- list-minimum function as follows:+--+-- @+-- mm :: SNum a => [a] -> a+-- mm = foldr1 (\a b -> ite (a .<= b) a b)+-- @+--+-- It is similar to the standard 'Num' class, except ranging over symbolic instances.+class (OrdSymbolic a, Num a) => SNum a++-- 'SNum' Instances, including all possible variants except 'SBool', since booleans+-- are not numbers.+instance SNum SWord8+instance SNum SWord16+instance SNum SWord32+instance SNum SWord64+instance SNum SInt8+instance SNum SInt16+instance SNum SInt32+instance SNum SInt64+instance SNum SInteger+ -- Boolean combinators instance Boolean SBool where true = literal True@@ -442,16 +573,16 @@ x + y | x `isConcretely` (== 0) = y | y `isConcretely` (== 0) = x- | True = liftSym2 (mkSymOp Plus) (+) x y+ | True = liftSym2 (mkSymOp Plus) (+) (+) x y x * y | x `isConcretely` (== 0) = 0 | y `isConcretely` (== 0) = 0 | x `isConcretely` (== 1) = y | y `isConcretely` (== 1) = x- | True = liftSym2 (mkSymOp Times) (*) x y+ | True = liftSym2 (mkSymOp Times) (*) (*) x y x - y | y `isConcretely` (== 0) = x- | True = liftSym2 (mkSymOp Minus) (-) x y+ | True = liftSym2 (mkSymOp Minus) (-) (-) x y abs a | hasSign a = ite (a .< 0) (-a) a | True = a@@ -459,6 +590,19 @@ | hasSign a = ite (a .< 0) (-1) (ite (a .== 0) 0 1) | True = oneIf (a ./= 0) +instance Fractional SReal where+ fromRational = literal . fromRational+ x / y = liftSym2 (mkSymOp Quot) (/) die x y+ where -- should never happen+ die = error $ "impossible: non-real value found in Fractional.SReal " ++ show (x, y)++-- Some operations will never be used on Reals, but we need fillers:+noReal :: String -> AlgReal -> AlgReal -> AlgReal+noReal o a b = error $ "SBV.AlgReal." ++ o ++ ": Unexpected arguments: " ++ show (a, b)++noRealUnary :: String -> AlgReal -> AlgReal+noRealUnary o a = error $ "SBV.AlgReal." ++ o ++ ": Unexpected argument: " ++ show a+ -- NB. In the optimizations below, use of -1 is valid as -- -1 has all bits set to True for both signed and unsigned values instance (Bits a, SymWord a) => Bits (SBV a) where@@ -467,38 +611,38 @@ | x `isConcretely` (== -1) = y | y `isConcretely` (== 0) = 0 | y `isConcretely` (== -1) = x- | True = liftSym2 (mkSymOp And) (.&.) x y+ | True = liftSym2 (mkSymOp And) (noReal ".&.") (.&.) x y x .|. y | x `isConcretely` (== 0) = y | x `isConcretely` (== -1) = -1 | y `isConcretely` (== 0) = x | y `isConcretely` (== -1) = -1- | True = liftSym2 (mkSymOp Or) (.|.) x y+ | True = liftSym2 (mkSymOp Or) (noReal ".|.") (.|.) x y x `xor` y | x `isConcretely` (== 0) = y | y `isConcretely` (== 0) = x- | True = liftSym2 (mkSymOp XOr) xor x y- complement = liftSym1 (mkSymOp1 Not) complement+ | True = liftSym2 (mkSymOp XOr) (noReal "xor") xor x y+ complement = liftSym1 (mkSymOp1 Not) (noRealUnary "Not") complement bitSize _ = intSizeOf (undefined :: a) isSigned _ = hasSign (undefined :: a) shiftL x y- | y < 0 = shiftR x (-y)- | y == 0 = x- | True = liftSym1 (mkSymOp1 (Shl y)) (`shiftL` y) x+ | y < 0 = shiftR x (-y)+ | y == 0 = x+ | True = liftSym1 (mkSymOp1 (Shl y)) (noRealUnary "shiftL") (`shiftL` y) x shiftR x y- | y < 0 = shiftL x (-y)- | y == 0 = x- | True = liftSym1 (mkSymOp1 (Shr y)) (`shiftR` y) x+ | y < 0 = shiftL x (-y)+ | y == 0 = x+ | True = liftSym1 (mkSymOp1 (Shr y)) (noRealUnary "shiftR") (`shiftR` y) x rotateL x y- | y < 0 = rotateR x (-y)- | y == 0 = x- | not (isInfPrec x) = let sz = bitSize x in liftSym1 (mkSymOp1 (Rol (y `mod` sz))) (rot True sz y) x- | True = shiftL x y -- for unbounded Integers, rotateL is the same as shiftL in Haskell+ | y < 0 = rotateR x (-y)+ | y == 0 = x+ | isBounded x = let sz = bitSize x in liftSym1 (mkSymOp1 (Rol (y `mod` sz))) (noRealUnary "rotateL") (rot True sz y) x+ | True = shiftL x y -- for unbounded Integers, rotateL is the same as shiftL in Haskell rotateR x y- | y < 0 = rotateL x (-y)- | y == 0 = x- | not (isInfPrec x) = let sz = bitSize x in liftSym1 (mkSymOp1 (Ror (y `mod` sz))) (rot False sz y) x- | True = shiftR x y -- for unbounded integers, rotateR is the same as shiftR in Haskell+ | y < 0 = rotateL x (-y)+ | y == 0 = x+ | isBounded x = let sz = bitSize x in liftSym1 (mkSymOp1 (Ror (y `mod` sz))) (noRealUnary "rotateR") (rot False sz y) x+ | True = shiftR x y -- for unbounded integers, rotateR is the same as shiftR in Haskell -- NB. testBit is *not* implementable on non-concrete symbolic words x `testBit` i | isConcrete x = (x .&. bit i) /= 0@@ -537,9 +681,10 @@ -- issue is with really-really large concrete 'SInteger' values sbvPopCount :: (Bits a, SymWord a) => SBV a -> SWord8 sbvPopCount x- | isConcrete x = go 0 x- | isInfPrec x = error "SBV.sbvPopCount: Called on an infinite precision symbolic value"- | True = sum [ite b 1 0 | b <- blastLE x]+ | isReal x = error "SBV.sbvPopCount: Called on a real value"+ | isConcrete x = go 0 x+ | not (isBounded x) = error "SBV.sbvPopCount: Called on an infinite precision symbolic value"+ | True = sum [ite b 1 0 | b <- blastLE x] where -- concrete case go !c 0 = c go !c w = go (c+1) (w .&. (w-1))@@ -553,8 +698,9 @@ -- | Little-endian blasting of a word into its bits. Also see the 'FromBits' class blastLE :: (Bits a, SymWord a) => SBV a -> [SBool] blastLE x- | isInfPrec x = error "SBV.blastLE: Called on an infinite precision value"- | True = map (sbvTestBit x) [0 .. (intSizeOf x)-1]+ | isReal x = error "SBV.blastLE: Called on a real value"+ | not (isBounded x) = error "SBV.blastLE: Called on an infinite precision value"+ | True = map (sbvTestBit x) [0 .. (intSizeOf x)-1] -- | Big-endian blasting of a word into its bits. Also see the 'FromBits' class blastBE :: (Bits a, SymWord a) => SBV a -> [SBool]@@ -567,8 +713,9 @@ -- | Most significant bit of a word, always stored at the last position msb :: (Bits a, SymWord a) => SBV a -> SBool msb x- | isInfPrec x = error "SBV.msb: Called on an infinite precision value"- | True = sbvTestBit x ((intSizeOf x) - 1)+ | isReal x = error "SBV.msb: Called on a real value"+ | not (isBounded x) = error "SBV.msb: Called on an infinite precision value"+ | True = sbvTestBit x ((intSizeOf x) - 1) -- Enum instance. These instances are suitable for use with concrete values, -- and will be less useful for symbolic values around. Note that `fromEnum` requires@@ -675,10 +822,10 @@ bvQuotRem x y = x `quotRem` y instance BVDivisible CW where- bvQuotRem x y- | cwSameType x y = let (r1, r2) = bvQuotRem (cwVal x) (cwVal y)- in (x { cwVal = r1 }, y { cwVal = r2 })- bvQuotRem x y = error $ "SBV.liftQRem: impossible, unexpected args received: " ++ show (x, y)+ bvQuotRem a b+ | Right x <- cwVal a, Right y <- cwVal b+ = let (r1, r2) = bvQuotRem x y in (a { cwVal = Right r1 }, b { cwVal = Right r2 })+ bvQuotRem a b = error $ "SBV.liftQRem: impossible, unexpected args received: " ++ show (a, b) instance BVDivisible SWord64 where bvQuotRem = liftQRem@@ -730,12 +877,21 @@ -- -- Minimal complete definition: 'symbolicMerge' class Mergeable a where- -- | Merge two values based on the condition+ -- | Merge two values based on the condition. This is intended+ -- to be a "structural" copy, walking down the values and merging+ -- recursively through the structure of @a@. In particular,+ -- symbolicMerge should *not* waste its time testing whether the+ -- condition might be a literal; that will be handled by 'ite'+ -- which should be used in all user code. In particular, any+ -- implementation of 'symbolicMerge' should just call 'symbolicMerge'+ -- recursively in the constituents of @a@, instead of 'ite'. symbolicMerge :: SBool -> a -> a -> a -- | Choose one or the other element, based on the condition. -- This is similar to 'symbolicMerge', but it has a default- -- implementation that makes sure it's short-cut if the condition is concrete- ite :: SBool -> a -> a -> a+ -- implementation that makes sure it's short-cut if the condition is concrete.+ -- The idea is that use symbolicMerge if you know the condition is symbolic,+ -- otherwise use ite, if there's a chance it might be concrete.+ ite :: 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@ -- overflows@@ -744,36 +900,104 @@ ite s a b | Just t <- unliteral s = if t then a else b | True = symbolicMerge s a b- select [] err _ = err+ -- 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+ -- "concrete" subwords: If an index is symbolic, then all its bits are+ -- symbolic as well. So, the binary search only pays off only if the indexed+ -- list is really humongous, which is not very common in general. (Also,+ -- for the case when the list is bit-vectors, we use SMT tables anyhow.) select xs err ind- | hasSign ind = ite (ind .< 0) err $ result- | True = result- where result = go xs $ reverse (zip [(0::Integer)..] bits)- bits = map (ind `sbvTestBit`) [0 .. bitSize ind - 1]- go [] _ = err- go (x:_) [] = x- go elts ((n, b):nbs) = let (ys, zs) = genericSplitAt ((2::Integer) ^ n) elts- in ite b (go zs nbs) (go ys nbs)+ | isReal ind = error "SBV.select: unsupported real valued select/index expression"+ | Just i <- unliteral ind = if i < 0 || i >= genericLength xs+ then err+ else xs `genericIndex` i+ | True = walk xs ind err+ where walk [] _ acc = acc+ walk (e:es) i acc = walk es (i-1) (ite (i .== 0) e acc) -- SBV instance SymWord a => Mergeable (SBV a) where- symbolicMerge t a b- | Just c1 <- unliteral a, Just c2 <- unliteral b, c1 == c2- = a- | True- = SBV sgnsz $ Right $ cache c- where sgnsz = (hasSign a, sizeOf a)+ -- the strict match and checking of literal equivalence is essential below,+ -- as otherwise we risk hanging onto huge closures and blow stack! This is+ -- against the feel that merging shouldn't look at branches if the test+ -- expression is constant. However, it's OK to do it this way since we+ -- expect "ite" to be used in such cases which already checks for that. That+ -- is the use case of the symbolicMerge should be when the test is symbolic.+ -- Of course, we do not have a way of enforcing that in the user code, but+ -- at least our library code respects that invariant.+ symbolicMerge t a@(SBV{}) b@(SBV{})+ | Just av <- unliteral a, Just bv <- unliteral b, av == bv+ = a+ | True+ = SBV k $ Right $ cache c+ where k = kindOf a c st = do swt <- sbvToSW st t case () of- () | swt == trueSW -> sbvToSW st a- () | swt == falseSW -> sbvToSW st b- () -> do swa <- sbvToSW st a- swb <- sbvToSW st b- case () of+ () | swt == trueSW -> sbvToSW st a -- these two cases should never be needed as we expect symbolicMerge to be+ () | swt == falseSW -> sbvToSW st b -- called with symbolic tests, but just in case..+ () -> do {- It is tempting to record the choice of the test expression here as we branch down to the 'then' and 'else' branches. That is,+ when we evaluate 'a', we can make use of the fact that the test expression is True, and similarly we can use the fact that it+ is False when b is evaluated. In certain cases this can cut down on symbolic simulation significantly, for instance if+ repetitive decisions are made in a recursive loop. Unfortunately, the implementation of this idea is quite tricky, due to+ our sharing based implementation. As the 'then' branch is evaluated, we will create many expressions that are likely going+ to be "reused" when the 'else' branch is executed. But, it would be *dead wrong* to share those values, as they were "cached"+ under the incorrect assumptions. To wit, consider the following:++ foo x y = ite (y .== 0) k (k+1)+ where k = ite (y .== 0) x (x+1)++ When we reduce the 'then' branch of the first ite, we'd record the assumption that y is 0. But while reducing the 'then' branch, we'd+ like to share 'k', which would evaluate (correctly) to 'x' under the given assumption. When we backtrack and evaluate the 'else'+ branch of the first ite, we'd see 'k' is needed again, and we'd look it up from our sharing map to find (incorrectly) that its value+ is 'x', which was stored there under the assumption that y was 0, which no longer holds. Clearly, this is unsound.++ A sound implementation would have to precisely track which assumptions were active at the time expressions get shared. That is,+ in the above example, we should record that the value of 'k' was cached under the assumption that 'y' is 0. While sound, this+ approach unfortunately leads to significant loss of valid sharing when the value itself had nothing to do with the assumption itself.+ To wit, consider:++ foo x y = ite (y .== 0) k (k+1)+ where k = x+5++ If we tracked the assumptions, we would recompute 'k' twice, since the branch assumptions would differ. Clearly, there is no need to+ re-compute 'k' in this case since its value is independent of y. Note that the whole SBV performance story is based on agressive sharing,+ and losing that would have other significant ramifications.++ The "proper" solution would be to track, with each shared computation, precisely which assumptions it actually *depends* on, rather+ than blindly recording all the assumptions present at that time. SBV's symbolic simulation engine clearly has all the info needed to do this+ properly, but the implementation is not straightforward at all. For each subexpression, we would need to chase down its dependencies+ transitively, which can require a lot of scanning of the generated program causing major slow-down; thus potentially defeating the+ whole purpose of sharing in the first place.++ Design choice: Keep it simple, and simply do not track the assumption at all. This will maximize sharing, at the cost of evaluating+ unreachable branches. I think the simplicity is more important at this point than efficiency.++ Also note that the user can avoid most such issues by properly combining if-then-else's with common conditions together. That is, the+ first program above should be written like this:++ foo x y = ite (y .== 0) x (x+2)++ In general, the following transformations should be done whenever possible:++ ite e1 (ite e1 e2 e3) e4 --> ite e1 e2 e4+ ite e1 e2 (ite e1 e3 e4) --> ite e1 e2 e4++ This is in accordance with the general rule-of-thumb stating conditionals should be avoided as much as possible. However, we might prefer+ the following:++ ite e1 (f e2 e4) (f e3 e5) --> f (ite e1 e2 e3) (ite e1 e4 e5)++ especially if this expression happens to be inside 'f's body itself (i.e., when f is recursive), since it reduces the number of+ recursive calls. Clearly, programming with symbolic simulation in mind is another kind of beast alltogether.+ -}+ swa <- sbvToSW st a -- evaluate 'then' branch+ swb <- sbvToSW st b -- evaluate 'else' branch+ case () of -- merge: () | swa == swb -> return swa () | swa == trueSW && swb == falseSW -> return swt- () | swa == falseSW && swb == trueSW -> newExpr st sgnsz (SBVApp Not [swt])- () -> newExpr st sgnsz (SBVApp Ite [swt, swa, swb])+ () | swa == falseSW && swb == trueSW -> newExpr st k (SBVApp Not [swt])+ () -> newExpr st k (SBVApp Ite [swt, swa, swb]) -- Custom version of select that translates to SMT-Lib tables at the base type of words select xs err ind | Just i <- unliteral ind@@ -781,17 +1005,17 @@ i' = fromIntegral i in if i' < 0 || i' >= genericLength xs then err else genericIndex xs i' select [] err _ = err- select xs err ind = SBV sgnszElt $ Right $ cache r- where sgnszInd = (hasSign ind, sizeOf ind)- sgnszElt = (hasSign err, sizeOf err)+ select xs err ind = SBV kElt $ Right $ cache r+ where kInd = kindOf ind+ kElt = kindOf err r st = do sws <- mapM (sbvToSW st) xs swe <- sbvToSW st err if all (== swe) sws -- off-chance that all elts are the same then return swe- else do idx <- getTableIndex st sgnszInd sgnszElt sws+ else do idx <- getTableIndex st kInd kElt sws swi <- sbvToSW st ind let len = length xs- newExpr st sgnszElt (SBVApp (LkUp (idx, sgnszInd, sgnszElt, len) swi swe) [])+ newExpr st kElt (SBVApp (LkUp (idx, kInd, kElt, len) swi swe) []) -- Unit instance Mergeable () where@@ -836,7 +1060,12 @@ -- Functions instance Mergeable b => Mergeable (a -> b) where symbolicMerge t f g = \x -> symbolicMerge t (f x) (g x)- select xs err ind = \x -> select (map ($ x) xs) (err x) ind+ {- Following definition, while correct, is utterly inefficient. Since the+ application is delayed, this hangs on to the inner list and all the+ impending merges, even when ind is concrete. Thus, it's much better to+ simply use the default definition for the function case.+ -}+ -- select xs err ind = \x -> select (map ($ x) xs) (err x) ind -- 2-Tuple instance (Mergeable a, Mergeable b) => Mergeable (a, b) where@@ -889,10 +1118,10 @@ -- SArrays are both "EqSymbolic" and "Mergeable" instance EqSymbolic (SArray a b) where- (SArray _ a) .== (SArray _ b) = SBV (False, Size (Just 1)) $ Right $ cache c+ (SArray _ a) .== (SArray _ b) = SBV (KBounded False 1) $ Right $ cache c where c st = do ai <- uncacheAI a st bi <- uncacheAI b st- newExpr st (False, Size (Just 1)) (SBVApp (ArrEq ai bi) [])+ newExpr st (KBounded False 1) (SBVApp (ArrEq ai bi) []) instance SymWord b => Mergeable (SArray a b) where symbolicMerge = mergeArrays@@ -958,138 +1187,138 @@ cgUninterpret nm code v = snd $ sbvUninterpret (Just (code, v)) nm -- Plain constants-instance HasSignAndSize a => Uninterpreted (SBV a) where+instance HasKind a => Uninterpreted (SBV a) where sbvUninterpret mbCgData nm | Just (_, v) <- mbCgData = (mkUFName nm, v)- | True = (mkUFName nm, SBV sgnsza $ Right $ cache result)- where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))+ | True = (mkUFName nm, SBV ka $ Right $ cache result)+ where ka = kindOf (undefined :: a) result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st v- | True = do newUninterpreted st nm (SBVType [sgnsza]) (fst `fmap` mbCgData)- newExpr st sgnsza $ SBVApp (Uninterpreted nm) []+ | True = do newUninterpreted st nm (SBVType [ka]) (fst `fmap` mbCgData)+ newExpr st ka $ SBVApp (Uninterpreted nm) [] -- Forcing an argument; this is a necessary evil to make sure all the arguments -- to an uninterpreted function are evaluated before called; the semantics of -- such functions is necessarily strict; deviating from Haskell's forceArg :: SW -> IO ()-forceArg (SW (b, s) n) = b `seq` s `seq` n `seq` return ()+forceArg (SW k n) = k `seq` n `seq` return () -- Functions of one argument-instance (SymWord b, HasSignAndSize a) => Uninterpreted (SBV b -> SBV a) where+instance (SymWord b, HasKind a) => Uninterpreted (SBV b -> SBV a) where sbvUninterpret mbCgData nm = (mkUFName nm, f) where f arg0 | Just (_, v) <- mbCgData, isConcrete arg0 = v arg0 | True- = SBV sgnsza $ Right $ cache result- where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))- sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))+ = SBV ka $ Right $ cache result+ where ka = kindOf (undefined :: a)+ kb = kindOf (undefined :: b) result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st (v arg0)- | True = do newUninterpreted st nm (SBVType [sgnszb, sgnsza]) (fst `fmap` mbCgData)+ | True = do newUninterpreted st nm (SBVType [kb, ka]) (fst `fmap` mbCgData) sw0 <- sbvToSW st arg0 mapM_ forceArg [sw0]- newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0]+ newExpr st ka $ SBVApp (Uninterpreted nm) [sw0] -- Functions of two arguments-instance (SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted (SBV c -> SBV b -> SBV a) where+instance (SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV c -> SBV b -> SBV a) where sbvUninterpret mbCgData nm = (mkUFName nm, f) where f arg0 arg1 | Just (_, v) <- mbCgData, isConcrete arg0, isConcrete arg1 = v arg0 arg1 | True- = SBV sgnsza $ Right $ cache result- where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))- sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))- sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))+ = SBV ka $ Right $ cache result+ where ka = kindOf (undefined :: a)+ kb = kindOf (undefined :: b)+ kc = kindOf (undefined :: c) result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st (v arg0 arg1)- | True = do newUninterpreted st nm (SBVType [sgnszc, sgnszb, sgnsza]) (fst `fmap` mbCgData)+ | True = do newUninterpreted st nm (SBVType [kc, kb, ka]) (fst `fmap` mbCgData) sw0 <- sbvToSW st arg0 sw1 <- sbvToSW st arg1 mapM_ forceArg [sw0, sw1]- newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1]+ newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1] -- Functions of three arguments-instance (SymWord d, SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) where+instance (SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) where sbvUninterpret mbCgData nm = (mkUFName nm, f) where f arg0 arg1 arg2 | Just (_, v) <- mbCgData, isConcrete arg0, isConcrete arg1, isConcrete arg2 = v arg0 arg1 arg2 | True- = SBV sgnsza $ Right $ cache result- where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))- sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))- sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))- sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))+ = SBV ka $ Right $ cache result+ where ka = kindOf (undefined :: a)+ kb = kindOf (undefined :: b)+ kc = kindOf (undefined :: c)+ kd = kindOf (undefined :: d) result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st (v arg0 arg1 arg2)- | True = do newUninterpreted st nm (SBVType [sgnszd, sgnszc, sgnszb, sgnsza]) (fst `fmap` mbCgData)+ | True = do newUninterpreted st nm (SBVType [kd, kc, kb, ka]) (fst `fmap` mbCgData) sw0 <- sbvToSW st arg0 sw1 <- sbvToSW st arg1 sw2 <- sbvToSW st arg2 mapM_ forceArg [sw0, sw1, sw2]- newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2]+ newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2] -- Functions of four arguments-instance (SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where+instance (SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where sbvUninterpret mbCgData nm = (mkUFName nm, f) where f arg0 arg1 arg2 arg3 | Just (_, v) <- mbCgData, isConcrete arg0, isConcrete arg1, isConcrete arg2, isConcrete arg3 = v arg0 arg1 arg2 arg3 | True- = SBV sgnsza $ Right $ cache result- where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))- sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))- sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))- sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))- sgnsze = (hasSign (undefined :: e), sizeOf (undefined :: e))+ = SBV ka $ Right $ cache result+ where ka = kindOf (undefined :: a)+ kb = kindOf (undefined :: b)+ kc = kindOf (undefined :: c)+ kd = kindOf (undefined :: d)+ ke = kindOf (undefined :: e) result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st (v arg0 arg1 arg2 arg3)- | True = do newUninterpreted st nm (SBVType [sgnsze, sgnszd, sgnszc, sgnszb, sgnsza]) (fst `fmap` mbCgData)+ | True = do newUninterpreted st nm (SBVType [ke, kd, kc, kb, ka]) (fst `fmap` mbCgData) sw0 <- sbvToSW st arg0 sw1 <- sbvToSW st arg1 sw2 <- sbvToSW st arg2 sw3 <- sbvToSW st arg3 mapM_ forceArg [sw0, sw1, sw2, sw3]- newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3]+ newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3] -- Functions of five arguments-instance (SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where+instance (SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where sbvUninterpret mbCgData nm = (mkUFName nm, f) where f arg0 arg1 arg2 arg3 arg4 | Just (_, v) <- mbCgData, isConcrete arg0, isConcrete arg1, isConcrete arg2, isConcrete arg3, isConcrete arg4 = v arg0 arg1 arg2 arg3 arg4 | True- = SBV sgnsza $ Right $ cache result- where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))- sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))- sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))- sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))- sgnsze = (hasSign (undefined :: e), sizeOf (undefined :: e))- sgnszf = (hasSign (undefined :: f), sizeOf (undefined :: f))+ = SBV ka $ Right $ cache result+ where ka = kindOf (undefined :: a)+ kb = kindOf (undefined :: b)+ kc = kindOf (undefined :: c)+ kd = kindOf (undefined :: d)+ ke = kindOf (undefined :: e)+ kf = kindOf (undefined :: f) result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st (v arg0 arg1 arg2 arg3 arg4)- | True = do newUninterpreted st nm (SBVType [sgnszf, sgnsze, sgnszd, sgnszc, sgnszb, sgnsza]) (fst `fmap` mbCgData)+ | True = do newUninterpreted st nm (SBVType [kf, ke, kd, kc, kb, ka]) (fst `fmap` mbCgData) sw0 <- sbvToSW st arg0 sw1 <- sbvToSW st arg1 sw2 <- sbvToSW st arg2 sw3 <- sbvToSW st arg3 sw4 <- sbvToSW st arg4 mapM_ forceArg [sw0, sw1, sw2, sw3, sw4]- newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4]+ newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4] -- Functions of six arguments-instance (SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where+instance (SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where sbvUninterpret mbCgData nm = (mkUFName nm, f) where f arg0 arg1 arg2 arg3 arg4 arg5 | Just (_, v) <- mbCgData, isConcrete arg0, isConcrete arg1, isConcrete arg2, isConcrete arg3, isConcrete arg4, isConcrete arg5 = v arg0 arg1 arg2 arg3 arg4 arg5 | True- = SBV sgnsza $ Right $ cache result- where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))- sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))- sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))- sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))- sgnsze = (hasSign (undefined :: e), sizeOf (undefined :: e))- sgnszf = (hasSign (undefined :: f), sizeOf (undefined :: f))- sgnszg = (hasSign (undefined :: g), sizeOf (undefined :: g))+ = SBV ka $ Right $ cache result+ where ka = kindOf (undefined :: a)+ kb = kindOf (undefined :: b)+ kc = kindOf (undefined :: c)+ kd = kindOf (undefined :: d)+ ke = kindOf (undefined :: e)+ kf = kindOf (undefined :: f)+ kg = kindOf (undefined :: g) result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st (v arg0 arg1 arg2 arg3 arg4 arg5)- | True = do newUninterpreted st nm (SBVType [sgnszg, sgnszf, sgnsze, sgnszd, sgnszc, sgnszb, sgnsza]) (fst `fmap` mbCgData)+ | True = do newUninterpreted st nm (SBVType [kg, kf, ke, kd, kc, kb, ka]) (fst `fmap` mbCgData) sw0 <- sbvToSW st arg0 sw1 <- sbvToSW st arg1 sw2 <- sbvToSW st arg2@@ -1097,27 +1326,27 @@ sw4 <- sbvToSW st arg4 sw5 <- sbvToSW st arg5 mapM_ forceArg [sw0, sw1, sw2, sw3, sw4, sw5]- newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5]+ newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5] -- Functions of seven arguments-instance (SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize a)+instance (SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where sbvUninterpret mbCgData nm = (mkUFName nm, f) where f arg0 arg1 arg2 arg3 arg4 arg5 arg6 | Just (_, v) <- mbCgData, isConcrete arg0, isConcrete arg1, isConcrete arg2, isConcrete arg3, isConcrete arg4, isConcrete arg5, isConcrete arg6 = v arg0 arg1 arg2 arg3 arg4 arg5 arg6 | True- = SBV sgnsza $ Right $ cache result- where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))- sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))- sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))- sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))- sgnsze = (hasSign (undefined :: e), sizeOf (undefined :: e))- sgnszf = (hasSign (undefined :: f), sizeOf (undefined :: f))- sgnszg = (hasSign (undefined :: g), sizeOf (undefined :: g))- sgnszh = (hasSign (undefined :: h), sizeOf (undefined :: h))+ = SBV ka $ Right $ cache result+ where ka = kindOf (undefined :: a)+ kb = kindOf (undefined :: b)+ kc = kindOf (undefined :: c)+ kd = kindOf (undefined :: d)+ ke = kindOf (undefined :: e)+ kf = kindOf (undefined :: f)+ kg = kindOf (undefined :: g)+ kh = kindOf (undefined :: h) result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6)- | True = do newUninterpreted st nm (SBVType [sgnszh, sgnszg, sgnszf, sgnsze, sgnszd, sgnszc, sgnszb, sgnsza]) (fst `fmap` mbCgData)+ | True = do newUninterpreted st nm (SBVType [kh, kg, kf, ke, kd, kc, kb, ka]) (fst `fmap` mbCgData) sw0 <- sbvToSW st arg0 sw1 <- sbvToSW st arg1 sw2 <- sbvToSW st arg2@@ -1126,53 +1355,49 @@ sw5 <- sbvToSW st arg5 sw6 <- sbvToSW st arg6 mapM_ forceArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6]- newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5, sw6]+ newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5, sw6] -- Uncurried functions of two arguments-instance (SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted ((SBV c, SBV b) -> SBV a) where+instance (SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV c, SBV b) -> SBV a) where sbvUninterpret mbCgData nm = let (h, f) = sbvUninterpret (uc2 `fmap` mbCgData) nm in (h, \(arg0, arg1) -> f arg0 arg1) where uc2 (cs, fn) = (cs, \a b -> fn (a, b)) -- Uncurried functions of three arguments-instance (SymWord d, SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) where+instance (SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) where sbvUninterpret mbCgData nm = let (h, f) = sbvUninterpret (uc3 `fmap` mbCgData) nm in (h, \(arg0, arg1, arg2) -> f arg0 arg1 arg2) where uc3 (cs, fn) = (cs, \a b c -> fn (a, b, c)) -- Uncurried functions of four arguments-instance (SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize a)+instance (SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) where sbvUninterpret mbCgData nm = let (h, f) = sbvUninterpret (uc4 `fmap` mbCgData) nm in (h, \(arg0, arg1, arg2, arg3) -> f arg0 arg1 arg2 arg3) where uc4 (cs, fn) = (cs, \a b c d -> fn (a, b, c, d)) -- Uncurried functions of five arguments-instance (SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize a)+instance (SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where sbvUninterpret mbCgData nm = let (h, f) = sbvUninterpret (uc5 `fmap` mbCgData) nm in (h, \(arg0, arg1, arg2, arg3, arg4) -> f arg0 arg1 arg2 arg3 arg4) where uc5 (cs, fn) = (cs, \a b c d e -> fn (a, b, c, d, e)) -- Uncurried functions of six arguments-instance (SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize a)+instance (SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where sbvUninterpret mbCgData nm = let (h, f) = sbvUninterpret (uc6 `fmap` mbCgData) nm in (h, \(arg0, arg1, arg2, arg3, arg4, arg5) -> f arg0 arg1 arg2 arg3 arg4 arg5) where uc6 (cs, fn) = (cs, \a b c d e f -> fn (a, b, c, d, e, f)) -- Uncurried functions of seven arguments-instance (SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize a)+instance (SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where sbvUninterpret mbCgData nm = let (h, f) = sbvUninterpret (uc7 `fmap` mbCgData) nm in (h, \(arg0, arg1, arg2, arg3, arg4, arg5, arg6) -> f arg0 arg1 arg2 arg3 arg4 arg5 arg6) where uc7 (cs, fn) = (cs, \a b c d e f g -> fn (a, b, c, d, e, f, g)) ---------------------------------------------------------------------------------- -- | Adding arbitrary constraints.---------------------------------------------------------------------------------- constrain :: SBool -> Symbolic () constrain c = addConstraint Nothing c (bnot c) ---------------------------------------------------------------------------------- -- | Adding a probabilistic constraint. The 'Double' argument is the probability -- threshold. Probabilistic constraints are useful for 'genTest' and 'quickCheck' -- calls where we restrict our attention to /interesting/ parts of the input domain.---------------------------------------------------------------------------------- pConstrain :: Double -> SBool -> Symbolic () pConstrain t c = addConstraint (Just t) c (bnot c)
Data/SBV/BitVectors/PrettyNum.hs view
@@ -61,21 +61,25 @@ {hexS = shexI True True; binS = sbinI True True; hex = shexI False False; bin = sbinI False False;} instance PrettyNum CW where- hexS cw | cwIsBit cw = hexS (cwToBool cw)- | isInfPrec cw = shexI True True (cwVal cw)- | True = shex True True (hasSign cw, intSizeOf cw) (cwVal cw)+ hexS cw | cwIsBit cw = hexS (cwToBool cw)+ | isReal cw = let Left w = cwVal cw in show w+ | not (isBounded cw) = let Right w = cwVal cw in shexI True True w+ | True = let Right w = cwVal cw in shex True True (hasSign cw, intSizeOf cw) w - binS cw | cwIsBit cw = binS (cwToBool cw)- | isInfPrec cw = sbinI True True (cwVal cw)- | True = sbin True True (hasSign cw, intSizeOf cw) (cwVal cw)+ binS cw | cwIsBit cw = binS (cwToBool cw)+ | isReal cw = let Left w = cwVal cw in show w+ | not (isBounded cw) = let Right w = cwVal cw in sbinI True True w+ | True = let Right w = cwVal cw in sbin True True (hasSign cw, intSizeOf cw) w - hex cw | cwIsBit cw = hexS (cwToBool cw)- | isInfPrec cw = shexI False False (cwVal cw)- | True = shex False False (hasSign cw, intSizeOf cw) (cwVal cw)+ hex cw | cwIsBit cw = hexS (cwToBool cw)+ | isReal cw = let Left w = cwVal cw in show w+ | not (isBounded cw) = let Right w = cwVal cw in shexI False False w+ | True = let Right w = cwVal cw in shex False False (hasSign cw, intSizeOf cw) w - bin cw | cwIsBit cw = binS (cwToBool cw)- | isInfPrec cw = sbinI False False (cwVal cw)- | True = sbin False False (hasSign cw, intSizeOf cw) (cwVal cw)+ bin cw | cwIsBit cw = binS (cwToBool cw)+ | isReal cw = let Left w = cwVal cw in show w+ | not (isBounded cw) = let Right w = cwVal cw in sbinI False False w+ | True = let Right w = cwVal cw in sbin False False (hasSign cw, intSizeOf cw) w instance (SymWord a, PrettyNum a) => PrettyNum (SBV a) where hexS s = maybe (show s) (hexS :: a -> String) $ unliteral s@@ -83,6 +87,10 @@ hex s = maybe (show s) (hex :: a -> String) $ unliteral s bin s = maybe (show s) (bin :: a -> String) $ unliteral s +-- | Show as a hexadecimal value. First bool controls whether type info is printed+-- while the second boolean controls wether 0x prefix is printed. The tuple is+-- the signedness and the bit-length of the input. The length of the string+-- will /not/ depend on the value, but rather the bit-length. shex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String shex shType shPre (signed, size) a | a < 0@@ -95,6 +103,9 @@ | True = "" l = (size + 3) `div` 4 +-- | Show as a hexadecimal value, integer version. Almost the same as shex above+-- except we don't have a bit-length so the length of the string will depend+-- on the actual value. shexI :: Bool -> Bool -> Integer -> String shexI shType shPre a | a < 0@@ -106,6 +117,7 @@ pre | shPre = "0x" | True = "" +-- | Similar to 'shex'; except in binary. sbin :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String sbin shType shPre (signed,size) a | a < 0@@ -117,6 +129,7 @@ pre | shPre = "0b" | True = "" +-- | Similar to 'shexI'; except in binary. sbinI :: Bool -> Bool -> Integer -> String sbinI shType shPre a | a < 0@@ -128,11 +141,16 @@ pre | shPre = "0b" | True = "" +-- | Pad a string to a given length. If the string is longer, then we don't drop anything. pad :: Int -> String -> String pad l s = replicate (l - length s) '0' ++ s -s2, s16 :: (Show a, Integral a) => a -> String+-- | Binary printer+s2 :: (Show a, Integral a) => a -> String s2 v = showIntAtBase 2 dig v "" where dig = fromJust . flip lookup [(0, '0'), (1, '1')]++-- | Hex printer+s16 :: (Show a, Integral a) => a -> String s16 v = showHex v "" -- | A more convenient interface for reading binary numbers, also supports negative numbers
Data/SBV/BitVectors/STree.hs view
@@ -38,8 +38,8 @@ deriving Show instance (SymWord e, Mergeable (SBV e)) => Mergeable (STree i e) where- symbolicMerge b (SLeaf i) (SLeaf j) = SLeaf (ite b i j)- symbolicMerge b (SBin l r) (SBin l' r') = SBin (ite b l l') (ite b r r')+ symbolicMerge b (SLeaf i) (SLeaf j) = SLeaf (symbolicMerge b i j)+ symbolicMerge b (SBin l r) (SBin l' r') = SBin (symbolicMerge b l l') (symbolicMerge b r r') symbolicMerge _ _ _ = error "SBV.STree.symbolicMerge: Impossible happened while merging states" -- | Reading a value. We bit-blast the index and descend down the full tree@@ -59,9 +59,11 @@ walk _ _ = error $ "SBV.STree.writeSTree: Impossible happened while reading: " ++ show i -- | Construct the fully balanced initial tree using the given values-mkSTree :: forall i e. HasSignAndSize i => [SBV e] -> STree i e+mkSTree :: forall i e. HasKind i => [SBV e] -> STree i e mkSTree ivals- | isInfPrec (undefined :: i)+ | isReal (undefined :: i)+ = error "SBV.STree.mkSTree: Cannot build a real-valued sized tree"+ | not (isBounded (undefined :: i)) = error "SBV.STree.mkSTree: Cannot build an infinitely large tree" | reqd /= given = error $ "SBV.STree.mkSTree: Required " ++ show reqd ++ " elements, received: " ++ show given
Data/SBV/BitVectors/SignCast.hs view
@@ -80,19 +80,27 @@ genericSign :: (Integral a, SymWord a, Num b, SymWord b) => SBV a -> SBV b genericSign x | Just c <- unliteral x = literal $ fromIntegral c- | True = SBV sgsz (Right (cache y))- where sgsz = (True, sizeOf x)+ | True = SBV k (Right (cache y))+ where k = case kindOf x of+ KBounded False n -> KBounded True n+ KBounded True _ -> error "Data.SBV.SignCast.genericSign: Called on signed value"+ KUnbounded -> error "Data.SBV.SignCast.genericSign: Called on unbounded value"+ KReal -> error "Data.SBV.SignCast.genericSign: Called on real value" y st = do xsw <- sbvToSW st x- newExpr st sgsz (SBVApp (Extract (intSizeOf x-1) 0) [xsw])+ newExpr st k (SBVApp (Extract (intSizeOf x-1) 0) [xsw]) -- Same comments as above, regarding the implementation. genericUnsign :: (Integral a, SymWord a, Num b, SymWord b) => SBV a -> SBV b genericUnsign x | Just c <- unliteral x = literal $ fromIntegral c- | True = SBV sgsz (Right (cache y))- where sgsz = (False, sizeOf x)+ | True = SBV k (Right (cache y))+ where k = case kindOf x of+ KBounded True n -> KBounded False n+ KBounded False _ -> error "Data.SBV.SignCast.genericUnSign: Called on unsigned value"+ KUnbounded -> error "Data.SBV.SignCast.genericUnSign: Called on unbounded value"+ KReal -> error "Data.SBV.SignCast.genericUnSign: Called on real value" y st = do xsw <- sbvToSW st x- newExpr st sgsz (SBVApp (Extract (intSizeOf x-1) 0) [xsw])+ newExpr st k (SBVApp (Extract (intSizeOf x-1) 0) [xsw]) -- symbolic instances instance SignCast SWord8 SInt8 where
Data/SBV/BitVectors/Splittable.hs view
@@ -63,53 +63,55 @@ extend b = 0 # b cwSplit :: (SymWord a, Num a) => CW -> (SBV a, SBV a)-cwSplit z = (literal x, literal y)- where (x,y) = genSplit (intSizeOf z `div` 2) (cwVal z)+cwSplit z@(CW _ (Right v)) = (literal x, literal y)+ where (x, y) = genSplit (intSizeOf z `div` 2) v+cwSplit z = error $ "SBV.cwSplit: Unsupported CW value: " ++ show z cwJoin :: (SymWord a, Num a) => CW -> CW -> SBV a-cwJoin x y = literal (genJoin (intSizeOf x) (cwVal x) (cwVal y))+cwJoin x@(CW _ (Right a)) (CW _ (Right b)) = literal (genJoin (intSizeOf x) a b)+cwJoin x y = error $ "SBV.cwJoin: Unsupported arguments: " ++ show (x, y) -- symbolic instances instance Splittable SWord64 SWord32 where split (SBV _ (Left z)) = cwSplit z- split z = (SBV (False, Size (Just 32)) (Right (cache x)), SBV (False, Size (Just 32)) (Right (cache y)))+ split z = (SBV (KBounded False 32) (Right (cache x)), SBV (KBounded False 32) (Right (cache y))) where x st = do zsw <- sbvToSW st z- newExpr st (False, Size (Just 32)) (SBVApp (Extract 63 32) [zsw])+ newExpr st (KBounded False 32) (SBVApp (Extract 63 32) [zsw]) y st = do zsw <- sbvToSW st z- newExpr st (False, Size (Just 32)) (SBVApp (Extract 31 0) [zsw])+ newExpr st (KBounded False 32) (SBVApp (Extract 31 0) [zsw]) (SBV _ (Left a)) # (SBV _ (Left b)) = cwJoin a b- a # b = SBV (False, Size (Just 64)) (Right (cache c))+ a # b = SBV (KBounded False 64) (Right (cache c)) where c st = do asw <- sbvToSW st a bsw <- sbvToSW st b- newExpr st (False, Size (Just 64)) (SBVApp Join [asw, bsw])+ newExpr st (KBounded False 64) (SBVApp Join [asw, bsw]) extend b = 0 # b instance Splittable SWord32 SWord16 where split (SBV _ (Left z)) = cwSplit z- split z = (SBV (False, Size (Just 16)) (Right (cache x)), SBV (False, Size (Just 16)) (Right (cache y)))+ split z = (SBV (KBounded False 16) (Right (cache x)), SBV (KBounded False 16) (Right (cache y))) where x st = do zsw <- sbvToSW st z- newExpr st (False, Size (Just 16)) (SBVApp (Extract 31 16) [zsw])+ newExpr st (KBounded False 16) (SBVApp (Extract 31 16) [zsw]) y st = do zsw <- sbvToSW st z- newExpr st (False, Size (Just 16)) (SBVApp (Extract 15 0) [zsw])+ newExpr st (KBounded False 16) (SBVApp (Extract 15 0) [zsw]) (SBV _ (Left a)) # (SBV _ (Left b)) = cwJoin a b- a # b = SBV (False, Size (Just 32)) (Right (cache c))+ a # b = SBV (KBounded False 32) (Right (cache c)) where c st = do asw <- sbvToSW st a bsw <- sbvToSW st b- newExpr st (False, Size (Just 32)) (SBVApp Join [asw, bsw])+ newExpr st (KBounded False 32) (SBVApp Join [asw, bsw]) extend b = 0 # b instance Splittable SWord16 SWord8 where split (SBV _ (Left z)) = cwSplit z- split z = (SBV (False, Size (Just 8)) (Right (cache x)), SBV (False, Size (Just 8)) (Right (cache y)))+ split z = (SBV (KBounded False 8) (Right (cache x)), SBV (KBounded False 8) (Right (cache y))) where x st = do zsw <- sbvToSW st z- newExpr st (False, Size (Just 8)) (SBVApp (Extract 15 8) [zsw])+ newExpr st (KBounded False 8) (SBVApp (Extract 15 8) [zsw]) y st = do zsw <- sbvToSW st z- newExpr st (False, Size (Just 8)) (SBVApp (Extract 7 0) [zsw])+ newExpr st (KBounded False 8) (SBVApp (Extract 7 0) [zsw]) (SBV _ (Left a)) # (SBV _ (Left b)) = cwJoin a b- a # b = SBV (False, Size (Just 16)) (Right (cache c))+ a # b = SBV (KBounded False 16) (Right (cache c)) where c st = do asw <- sbvToSW st a bsw <- sbvToSW st b- newExpr st (False, Size (Just 16)) (SBVApp Join [asw, bsw])+ newExpr st (KBounded False 16) (SBVApp Join [asw, bsw]) extend b = 0 # b -- | Unblasting a value from symbolic-bits. The bits can be given little-endian
Data/SBV/Compilers/C.hs view
@@ -87,6 +87,10 @@ dieUnbounded = error $ "SBV->C: Unbounded integers are not supported by the C compiler." ++ "\nUse 'cgIntegerSize' to specify a fixed size for SInteger representation." +-- Reals+dieReal :: a+dieReal = error "SBV->C: SReal values are not supported by the C compiler."+ -- Unsupported features, or features TBD tbd :: String -> a tbd msg = error $ "SBV->C: Not yet supported: " ++ msg@@ -125,10 +129,11 @@ xs -> vcat $ text "/* User given declarations: */" : map text xs ++ [text ""] flags = cgLDFlags st -cSizeOf :: Maybe Int -> HasSignAndSize a => a -> Int+cSizeOf :: Maybe Int -> HasKind a => a -> Int cSizeOf mbIntSize x- | not (isInfPrec x) = intSizeOf x- | True = fromMaybe dieUnbounded mbIntSize+ | isReal x = dieReal+ | isInteger x = fromMaybe dieUnbounded mbIntSize+ | True = intSizeOf x -- | Pretty print a functions type. If there is only one output, we compile it -- as a function that returns that value. Otherwise, we compile it as a void function@@ -149,7 +154,7 @@ -- | Renders as "const SWord8 s0", etc. the first parameter is the width of the typefield declSW :: Maybe Int -> Int -> SW -> Doc-declSW mbISize w sw@(SW (sg, _) _) = text "const" <+> pad (showCType (sg, cSizeOf mbISize sw)) <+> text (show sw)+declSW mbISize w sw = text "const" <+> pad (showCType (hasSign sw, cSizeOf mbISize sw)) <+> text (show sw) where pad s = text $ s ++ replicate (w - length s) ' ' -- | Renders as "s0", etc, or the corresponding constant@@ -204,7 +209,8 @@ -- | Show a constant showConst :: Maybe Int -> CW -> Doc-showConst mbISize cw = mkConst (cwVal cw) (hasSign cw, cSizeOf mbISize cw)+showConst mbISize cw@(CW _ (Right v)) = mkConst v (hasSign cw, cSizeOf mbISize cw)+showConst _mbISize cw = die $ "showConst: " ++ show cw -- | Generate a makefile. The first argument is True if we have a driver. genMake :: Bool -> String -> String -> [String] -> Doc@@ -425,14 +431,15 @@ | True = text entry <+> text "=" <+> showSW mbISize consts sw <> semi where entry = cNm ++ "[" ++ show i ++ "]" mkRet sw = text "return" <+> showSW mbISize consts sw <> semi- genTbl :: ((Int, (Bool, Size), (Bool, Size)), [SW]) -> (Int, Doc)- genTbl ((i, _, (sg, sz)), elts) = (location, static <+> pprCWord True (sg, szv) <+> text ("table" ++ show i) <> text "[] = {"- $$ nest 4 (fsep (punctuate comma (align (map (showSW mbISize consts) elts))))- $$ text "};")- where szv = case (mbISize, sz) of- (_, Size (Just v)) -> v- (Just is, Size Nothing) -> is- _ -> dieUnbounded+ genTbl :: ((Int, Kind, Kind), [SW]) -> (Int, Doc)+ genTbl ((i, _, k), elts) = (location, static <+> pprCWord True (sg, szv) <+> text ("table" ++ show i) <> text "[] = {"+ $$ nest 4 (fsep (punctuate comma (align (map (showSW mbISize consts) elts))))+ $$ text "};")+ where (sg, szv) = case (mbISize, k) of+ (_, KBounded b v) -> (b, v)+ (Just is, KUnbounded) -> (True, is)+ (Nothing, KUnbounded) -> dieUnbounded+ (_, KReal) -> dieReal static = if location == -1 then text "static" else empty location = maximum (-1 : map getNodeId elts) getNodeId s@(SW _ (NodeId n)) | isConst s = -1@@ -473,16 +480,17 @@ = text "~" <> a where s = cSizeOf mbISize (head opArgs) p Ite [a, b, c] = a <+> text "?" <+> b <+> text ":" <+> c- p (LkUp (t, (as, sizeAT), _, len) ind def) []+ p (LkUp (t, k, _, len) ind def) [] | not rtc = lkUp -- ignore run-time-checks per user request | needsCheckL && needsCheckR = cndLkUp checkBoth | needsCheckL = cndLkUp checkLeft | needsCheckR = cndLkUp checkRight | True = lkUp- where at = case (mbISize, sizeAT) of- (_, Size (Just v)) -> v- (Just i, Size Nothing) -> i- _ -> dieUnbounded+ where (as, at) = case (mbISize, k) of+ (_, KBounded b v) -> (b, v)+ (Just i, KUnbounded) -> (True, i)+ (Nothing, KUnbounded) -> dieUnbounded+ (_, KReal) -> dieReal [index, defVal] = map (showSW mbISize consts) [ind, def] lkUp = text "table" <> int t <> brackets (showSW mbISize consts ind) cndLkUp cnd = cnd <+> text "?" <+> defVal <+> text ":" <+> lkUp
Data/SBV/Compilers/CodeGen.hs view
@@ -48,6 +48,7 @@ data CgVal = CgAtomic SW | CgArray [SW] +-- | Code-generation state data CgState = CgState { cgInputs :: [(String, CgVal)] , cgOutputs :: [(String, CgVal)]@@ -58,6 +59,7 @@ , cgFinalConfig :: CgConfig } +-- | Initial configuration for code-generation initCgState :: CgState initCgState = CgState { cgInputs = []@@ -75,11 +77,11 @@ newtype SBVCodeGen a = SBVCodeGen (StateT CgState Symbolic a) deriving (Monad, MonadIO, MonadState CgState) --- Reach into symbolic monad..+-- | Reach into symbolic monad from code-generation liftSymbolic :: Symbolic a -> SBVCodeGen a liftSymbolic = SBVCodeGen . lift --- Reach into symbolic monad and output a value. Returns the corresponding SW+-- | Reach into symbolic monad and output a value. Returns the corresponding SW cgSBVToSW :: SBV a -> SBVCodeGen SW cgSBVToSW = liftSymbolic . sbvToSymSW @@ -182,22 +184,25 @@ | CgSource | CgDriver +-- | Is this a driver program? isCgDriver :: CgPgmKind -> Bool isCgDriver CgDriver = True isCgDriver _ = False +-- | Is this a make file? isCgMakefile :: CgPgmKind -> Bool isCgMakefile CgMakefile{} = True isCgMakefile _ = False instance Show CgPgmBundle where show (CgPgmBundle fs) = intercalate "\n" $ map showFile fs--showFile :: (FilePath, (CgPgmKind, [Doc])) -> String-showFile (f, (_, ds)) = "== BEGIN: " ++ show f ++ " ================\n"- ++ render' (vcat ds)- ++ "== END: " ++ show f ++ " =================="+ where showFile :: (FilePath, (CgPgmKind, [Doc])) -> String+ showFile (f, (_, ds)) = "== BEGIN: " ++ show f ++ " ================\n"+ ++ render' (vcat ds)+ ++ "== END: " ++ show f ++ " ==================" +-- | Generate code for a symbolic program, returning a Code-gen bundle, i.e., collection+-- of makefiles, source code, headers, etc. codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen () -> IO CgPgmBundle codeGen l cgConfig nm (SBVCodeGen comp) = do (((), st'), res) <- runSymbolic' CodeGen $ runStateT comp initCgState { cgFinalConfig = cgConfig }@@ -210,6 +215,7 @@ error $ "SBV.codeGen: " ++ show nm ++ " has following argument names duplicated: " ++ unwords dupNames return $ translate l (cgFinalConfig st) nm st res +-- | Render a code-gen bundle to a directory or to stdout renderCgPgmBundle :: Maybe FilePath -> CgPgmBundle -> IO () renderCgPgmBundle Nothing bundle = print bundle renderCgPgmBundle (Just dirName) (CgPgmBundle files) = do@@ -231,7 +237,8 @@ putStrLn $ "Generating: " ++ show fn ++ ".." writeFile fn (render' (vcat ds)) --- Pretty's render might have "leading" white-space in empty lines, eliminate:+-- | An alternative to Pretty's 'render', which might have "leading" white-space in empty lines. This version+-- eliminates such whitespace. render' :: Doc -> String render' = unlines . map clean . lines . P.render where clean x | all isSpace x = ""
+ Data/SBV/Examples/BitPrecise/MergeSort.hs view
@@ -0,0 +1,95 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.SBV.Examples.BitPrecise.MergeSort+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+-- Portability : portable+--+-- Symbolic implementation of merge-sort and its correctness.+-----------------------------------------------------------------------------++module Data.SBV.Examples.BitPrecise.MergeSort where++import Data.SBV++-----------------------------------------------------------------------------+-- * Implementing Merge-Sort+-----------------------------------------------------------------------------+-- | Element type of lists we'd like to sort. For simplicity, we'll just+-- use 'SWord8' here, but we can pick any symbolic type.+type E = SWord8++-- | Merging two given sorted lists, preserving the order.+merge :: [E] -> [E] -> [E]+merge [] ys = ys+merge xs [] = xs+merge xs@(x:xr) ys@(y:yr) = ite (x .< y) (x : merge xr ys) (y : merge xs yr)++-- | Simple merge-sort implementation. We simply divide the input list+-- in two two halves so long as it has at least two elements, sort+-- each half on its own, and then merge.+mergeSort :: [E] -> [E]+mergeSort [] = []+mergeSort [x] = [x]+mergeSort xs = merge (mergeSort th) (mergeSort bh)+ where (th, bh) = splitAt (length xs `div` 2) xs++-----------------------------------------------------------------------------+-- * Proving correctness+-- ${props}+-----------------------------------------------------------------------------+{- $props+There are two main parts to proving that a sorting algorithm is correct:++ * Prove that the output is non-decreasing++ * Prove that the output is a permutation of the input+-}++-- | Check whether a given sequence is non-decreasing.+nonDecreasing :: [E] -> SBool+nonDecreasing [] = true+nonDecreasing [_] = true+nonDecreasing (a:b:xs) = a .<= b &&& nonDecreasing (b:xs)++-- | Check whether two given sequences are permutations. We simply check that each sequence+-- is a subset of the other, when considered as a set. The check is slightly complicated+-- for the need to account for possibly duplicated elements.+isPermutationOf :: [E] -> [E] -> SBool+isPermutationOf as bs = go as (zip bs (repeat true)) &&& go bs (zip as (repeat true))+ where go [] _ = true+ go (x:xs) ys = let (found, ys') = mark x ys in found &&& go xs ys'+ -- Go and mark off an instance of 'x' in the list, if possible. We keep track+ -- of unmarked elements by associating a boolean bit. Note that we have to+ -- keep the lists equal size for the recursive result to merge properly.+ mark _ [] = (false, [])+ mark x ((y,v):ys) = ite (v &&& x .== y)+ (true, (y, bnot v):ys)+ (let (r, ys') = mark x ys in (r, (y,v):ys'))++-- | Asserting correctness of merge-sort for a list of the given size. Note that we can+-- only check correctness for fixed-size lists. Also, the proof will get more and more+-- complicated for the backend SMT solver as 'n' increases. A value around 5 or 6 should+-- be fairly easy to prove. For instance, we have:+--+-- >>> correctness 5+-- Q.E.D.+correctness :: Int -> IO ThmResult+correctness n = prove $ do xs <- mkFreeVars n+ let ys = mergeSort xs+ return $ nonDecreasing ys &&& isPermutationOf xs ys++-----------------------------------------------------------------------------+-- * Generating C code+-----------------------------------------------------------------------------++-- | Generate C code for merge-sorting an array of size 'n'. Again, we're restricted+-- to fixed size inputs. While the output is not how one would code merge sort in C+-- by hand, it's a faithful rendering of all the operations merge-sort would do as+-- described by it's Haskell counterpart.+codeGen :: Int -> IO ()+codeGen n = compileToC (Just ("mergeSort" ++ show n)) "mergeSort" $ do+ xs <- cgInputArr n "xs"+ cgOutputArr "ys" (mergeSort xs)
+ Data/SBV/Examples/Existentials/Diophantine.hs view
@@ -0,0 +1,131 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.SBV.Examples.Existentials.Diophantine+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+-- Portability : portable+--+-- Finding minimal natural number solutions to linear Diophantine equations,+-- using explicit quantification.+-----------------------------------------------------------------------------+module Data.SBV.Examples.Existentials.Diophantine where++import Data.SBV++--------------------------------------------------------------------------------------------------+-- * Representing solutions+--------------------------------------------------------------------------------------------------+-- | For a homogeneous problem, the solution is any linear combination of the resulting vectors.+-- For a non-homogeneous problem, the solution is any linear combination of the vectors in the+-- second component plus one of the vectors in the first component.+data Solution = Homogeneous [[Integer]]+ | NonHomogeneous [[Integer]] [[Integer]]+ deriving Show++--------------------------------------------------------------------------------------------------+-- * Solving diophantine equations+--------------------------------------------------------------------------------------------------+-- | ldn: Solve a (L)inear (D)iophantine equation, returning minimal solutions over (N)aturals.+-- The input is given as a rows of equations, with rhs values separated into a tuple.+ldn :: [([Integer], Integer)] -> IO Solution+ldn problem = do solution <- basis (map (map literal) m)+ if homogeneous+ then return $ Homogeneous solution+ else do let ones = [xs | (1:xs) <- solution]+ zeros = [xs | (0:xs) <- solution]+ return $ NonHomogeneous ones zeros+ where rhs = map snd problem+ lhs = map fst problem+ homogeneous = all (== 0) rhs+ m | homogeneous = lhs+ | True = zipWith (\x y -> -x : y) rhs lhs++-- | Find the basis solution. By definition, the basis has all non-trivial (i.e., non-0) solutions+-- that cannot be written as the sum of two other solutions. We use the mathematically equivalent+-- statement that a solution is in the basis if it's least according to the lexicographic+-- order using the ordinary less-than relation.+basis :: [[SInteger]] -> IO [[Integer]]+basis m = extractModels `fmap` allSat cond+ where cond = do as <- mkExistVars n+ bs <- mkForallVars n+ return $ ok as &&& (ok bs ==> as .== bs ||| bnot (bs `less` as))+ n = if null m then 0 else length (head m)+ ok xs = bAny (.> 0) xs &&& bAll (.>= 0) xs &&& bAnd [sum (zipWith (*) r xs) .== 0 | r <- m]+ as `less` bs = bAnd (zipWith (.<=) as bs) &&& bOr (zipWith (.<) as bs)++--------------------------------------------------------------------------------------------------+-- * Examples+--------------------------------------------------------------------------------------------------++-- | Solve the equation:+--+-- @2x + y - z = 2@+--+-- We have:+--+-- >>> test+-- NonHomogeneous [[0,2,0],[1,0,0]] [[0,1,1],[1,0,2]]+--+-- which means that the solutions are of the form:+--+-- @(0, 2, 0) + k (0, 1, 1) + k' (1, 0, 2) = (k', 2+k, k+2k')@+--+-- OR+--+-- @(1, 0, 0) + k (0, 1, 1) + k' (1, 0, 2) = (1+k', k, k+2k')@+--+-- for arbitrary @k@, @k'@. It's easy to see that these are really solutions+-- to the equation given. It's harder to see that they cover all possibilities,+-- but a moments thought reveals that is indeed the case.+test :: IO Solution+test = ldn [([2,1,-1], 2)]++-- | A puzzle: Five sailors and a monkey escape from a naufrage and reach an island with+-- coconuts. Before dawn, they gather a few of them and decide to sleep first and share+-- the next day. At night, however, one of them awakes, counts the nuts, makes five parts,+-- gives the remaining nut to the monkey, saves his share away, and sleeps. All other+-- sailors do the same, one by one. When they all wake up in the morning, they again make 5 shares,+-- and give the last remaining nut to the monkey. How many nuts were there at the beginning?+--+-- We can model this as a series of diophantine equations:+--+-- @+-- x_0 = 5 x_1 + 1+-- 4 x_1 = 5 x_2 + 1+-- 4 x_2 = 5 x_3 + 1+-- 4 x_3 = 5 x_4 + 1+-- 4 x_4 = 5 x_5 + 1+-- 4 x_5 = 5 x_6 + 1+-- @+--+-- We need to find to solve for x_0, over the naturals. We have:+--+-- >>> sailors+-- [15621,3124,2499,1999,1599,1279,1023]+--+-- That is:+--+-- @+-- * There was a total of 15621 coconuts+-- * 1st sailor: 15621 = 3124*5+1, leaving 15621-3124-1 = 12496+-- * 2nd sailor: 12496 = 2499*5+1, leaving 12496-2499-1 = 9996+-- * 3rd sailor: 9996 = 1999*5+1, leaving 9996-1999-1 = 7996+-- * 4th sailor: 7996 = 1599*5+1, leaving 7996-1599-1 = 6396+-- * 5th sailor: 6396 = 1279*5+1, leaving 6396-1279-1 = 5116+-- * In the morning, they had: 5116 = 1023*5+1.+-- @+--+-- Note that this is the minimum solution, that is, we are guaranteed that there's+-- no solution with less number of coconuts. In fact, any member of @[15625*k-4 | k <- [1..]]@+-- is a solution, i.e., so are @31246@, @46871@, @62496@, @78121@, etc.+sailors :: IO [Integer]+sailors = do NonHomogeneous (xs:_) _ <- ldn [ ([1, -5, 0, 0, 0, 0, 0], 1)+ , ([0, 4, -5 , 0, 0, 0, 0], 1)+ , ([0, 0, 4, -5 , 0, 0, 0], 1)+ , ([0, 0, 0, 4, -5, 0, 0], 1)+ , ([0, 0, 0, 0, 4, -5, 0], 1)+ , ([0, 0, 0, 0, 0, 4, -5], 1)+ ]+ return xs
Data/SBV/Examples/Puzzles/Counts.hs view
@@ -32,10 +32,9 @@ -- | We will assume each number can be represented by an 8-bit word, i.e., can be at most 128. type Count = SWord8-type Counts = [Count] -- | Given a number, increment the count array depending on the digits of the number-count :: Count -> Counts -> Counts+count :: Count -> [Count] -> [Count] count n cnts = ite (n .< 10) (upd n cnts) -- only one digit (ite (n .< 100)@@ -49,23 +48,23 @@ -- | Encoding of the puzzle. The solution is a sequence of 10 numbers -- for the occurrences of the digits such that if we count each digit, -- we find these numbers.-puzzle :: Counts -> SBool+puzzle :: [Count] -> SBool puzzle cnt = cnt .== last css where ones = replicate 10 1 -- all digits occur once to start with css = ones : zipWith count cnt css -- | Finds all two known solutions to this puzzle. We have: ----- >>> solve+-- >>> counts -- Solution #1 -- In this sentence, the number of occurrences of 0 is 1, of 1 is 11, of 2 is 2, of 3 is 1, of 4 is 1, of 5 is 1, of 6 is 1, of 7 is 1, of 8 is 1, of 9 is 1. -- Solution #2 -- In this sentence, the number of occurrences of 0 is 1, of 1 is 7, of 2 is 3, of 3 is 2, of 4 is 1, of 5 is 1, of 6 is 1, of 7 is 2, of 8 is 1, of 9 is 1. -- Found: 2 solution(s).-solve :: IO ()-solve = do res <- allSat $ puzzle `fmap` mkExistVars 10- cnt <- displayModels disp res- putStrLn $ "Found: " ++ show cnt ++ " solution(s)."+counts :: IO ()+counts = do res <- allSat $ puzzle `fmap` mkExistVars 10+ cnt <- displayModels disp res+ putStrLn $ "Found: " ++ show cnt ++ " solution(s)." where disp n (_, s) = do putStrLn $ "Solution #" ++ show n dispSolution s dispSolution :: [Word8] -> IO ()@@ -82,4 +81,4 @@ ++ ", of 8 is " ++ show (ns !! 8) ++ ", of 9 is " ++ show (ns !! 9) ++ "."-{-# ANN solve "HLint: ignore Use head" #-}+{-# ANN counts "HLint: ignore Use head" #-}
Data/SBV/Examples/Puzzles/DogCatMouse.hs view
@@ -18,29 +18,20 @@ import Data.SBV --- | Use 16-bit words to represent the counts, much larger than we actually need, but no harm.-type Count = SWord16---- | Codes the puzzle statement, more or less directly using SBV.-puzzle :: Count -> Count -> Count -> SBool-puzzle dog cat mouse =- dog .>= 1 &&& dog .<= 98 -- at least one dog and at most 98- &&& cat .>= 1 &&& cat .<= 98 -- ditto for cats- &&& mouse .>= 1 &&& mouse .<= 98 -- ditto for mice- &&& dog + cat + mouse .== 100 -- buy precisely 100 animals- &&& 1500 * dog + 100 * cat + 25 * mouse .== 10000 -- spend exactly 100 dollars (use cents since we don't have fractions)- -- | Prints the only solution: ----- >>> solve+-- >>> puzzle -- Solution #1:--- dog = 3 :: SWord16--- cat = 41 :: SWord16--- mouse = 56 :: SWord16+-- dog = 3 :: SInteger+-- cat = 41 :: SInteger+-- mouse = 56 :: SInteger -- This is the only solution.-solve :: IO AllSatResult-solve = allSat $ do- d <- exists "dog"- c <- exists "cat"- m <- exists "mouse"- return $ puzzle d c m+puzzle :: IO AllSatResult+puzzle = allSat $ do+ [dog, cat, mouse] <- sIntegers ["dog", "cat", "mouse"]+ solve [ dog .>= 1 -- at least one dog+ , cat .>= 1 -- at least one cat+ , mouse .>= 1 -- at least one mouse+ , dog + cat + mouse .== 100 -- buy precisely 100 animals+ , 1500 * dog + 100 * cat + 25 * mouse .== 10000 -- spend exactly 100 dollars (use cents since we don't have fractions)+ ]
Data/SBV/Examples/Puzzles/Euler185.hs view
@@ -40,11 +40,11 @@ -- | Print out the solution nicely. We have: ----- >>> solve+-- >>> solveEuler185 -- 4640261571849533 -- Number of solutions: 1-solve :: IO ()-solve = do res <- allSat euler185- cnt <- displayModels disp res- putStrLn $ "Number of solutions: " ++ show cnt+solveEuler185 :: IO ()+solveEuler185 = do res <- allSat euler185+ cnt <- displayModels disp res+ putStrLn $ "Number of solutions: " ++ show cnt where disp _ (_, ss) = putStrLn $ concatMap show (ss :: [Word8])
Data/SBV/Examples/Puzzles/Sudoku.hs view
@@ -52,12 +52,12 @@ ------------------------------------------------------------------- -- | Solve a given puzzle and print the results-solve :: Puzzle -> IO ()-solve p@(i, f) = do putStrLn "Solving the puzzle.."- model <- getModel `fmap` sat ((valid . f) `fmap` mkExistVars i)- case model of- Right sln -> dispSolution p sln- Left m -> putStrLn $ "Unsolvable puzzle: " ++ m+sudoku :: Puzzle -> IO ()+sudoku p@(i, f) = do putStrLn "Solving the puzzle.."+ model <- getModel `fmap` sat ((valid . f) `fmap` mkExistVars i)+ case model of+ Right sln -> dispSolution p sln+ Left m -> putStrLn $ "Unsolvable puzzle: " ++ m -- | Helper function to display results nicely, not really needed, but helps presentation dispSolution :: Puzzle -> (Bool, [Word8]) -> IO ()@@ -250,4 +250,4 @@ -- | Solve them all, this takes a fraction of a second to run for each case allPuzzles :: IO ()-allPuzzles = mapM_ solve [puzzle0, puzzle1, puzzle2, puzzle3, puzzle4, puzzle5, puzzle6]+allPuzzles = mapM_ sudoku [puzzle0, puzzle1, puzzle2, puzzle3, puzzle4, puzzle5, puzzle6]
Data/SBV/Internals.hs view
@@ -13,20 +13,15 @@ --------------------------------------------------------------------------------- module Data.SBV.Internals (- -- * Running symbolic programs /manually/- Result, SBVRunMode(..), runSymbolic, runSymbolic'- -- * Other internal structures useful for low-level programming- , SBV(..), HasSignAndSize(..), CW, mkConstCW, genFinVar, genFinVar_+ -- * Running symbolic programs /manually/+ Result, SBVRunMode(..), runSymbolic, runSymbolic'+ -- * Other internal structures useful for low-level programming+ , SBV(..), HasKind(..), CW, mkConstCW, genVar, genVar_ -- * Compilation to C , compileToC', compileToCLib', CgPgmBundle(..), CgPgmKind(..)- -- * Integrating with the test framework ) where -import Data.SBV.BitVectors.Data (Result, SBVRunMode(..), runSymbolic, runSymbolic', SBV(..), HasSignAndSize(..), CW, mkConstCW)-import Data.SBV.BitVectors.Model (genFinVar, genFinVar_)+import Data.SBV.BitVectors.Data (Result, SBVRunMode(..), runSymbolic, runSymbolic', SBV(..), HasKind(..), CW, mkConstCW)+import Data.SBV.BitVectors.Model (genVar, genVar_) import Data.SBV.Compilers.C (compileToC', compileToCLib') import Data.SBV.Compilers.CodeGen (CgPgmBundle(..), CgPgmKind(..))--{- $compileC-Lower level access to program bundles, for further processing of program bundles.--}
Data/SBV/Provers/Prover.hs view
@@ -27,6 +27,7 @@ , sat, satWith , allSat, allSatWith , isVacuous, isVacuousWith+ , solve , SatModel(..), Modelable(..), displayModels, extractModels , yices, z3, defaultSMTCfg , compileToSMTLib, generateSMTBenchmarks@@ -50,9 +51,10 @@ import qualified Data.SBV.Provers.Yices as Yices import qualified Data.SBV.Provers.Z3 as Z3 import Data.SBV.Utils.TDiff+import Data.SBV.Utils.Boolean mkConfig :: SMTSolver -> Bool -> [String] -> SMTConfig-mkConfig s isSMTLib2 tweaks = SMTConfig {verbose = False, timing = False, timeOut = Nothing, printBase = 10, smtFile = Nothing, solver = s, solverTweaks = tweaks, useSMTLib2 = isSMTLib2}+mkConfig s isSMTLib2 tweaks = SMTConfig {verbose = False, timing = False, timeOut = Nothing, printBase = 10, printRealPrec = 16, smtFile = Nothing, solver = s, solverTweaks = tweaks, useSMTLib2 = isSMTLib2} -- | Default configuration for the Yices SMT Solver. yices :: SMTConfig@@ -140,7 +142,7 @@ forSome [] k = forSome_ k -- Arrays (memory), only supported universally for the time being-instance (HasSignAndSize a, HasSignAndSize b, SymArray array, Provable p) => Provable (array a b -> p) where+instance (HasKind a, HasKind b, SymArray array, Provable p) => Provable (array a b -> p) where forAll_ k = newArray_ Nothing >>= \a -> forAll_ $ k a forAll (s:ss) k = newArray s Nothing >>= \a -> forAll ss $ k a forAll [] k = forAll_ k@@ -209,6 +211,16 @@ sat :: Provable a => a -> IO SatResult sat = satWith defaultSMTCfg +-- | Form the symbolic conjunction of a given list of boolean conditions. Useful in expressing+-- problems with constraints, like the following:+--+-- @+-- do [x, y, z] <- sIntegers [\"x\", \"y\", \"z\"]+-- solve [x .> 5, y + z .< x]+-- @+solve :: [SBool] -> Symbolic SBool+solve = return . bAnd+ -- | Return all satisfying assignments for a predicate, equivalent to @'allSatWith' 'defaultSMTCfg'@. -- Satisfying assignments are constructed lazily, so they will be available as returned by the solver -- and on demand.@@ -424,7 +436,7 @@ runProofOn converter config isSat comments res = let isTiming = timing config in case res of- Result hasInfPrec _qcInfo _codeSegs is consts tbls arrs uis axs pgm cstrs [o@(SW (False, Size (Just 1)) _)] ->+ Result hasInfPrec _qcInfo _codeSegs is consts tbls arrs uis axs pgm cstrs [o@(SW (KBounded False 1) _)] -> timeIf isTiming "translation" $ let uiMap = catMaybes (map arrayUIKind arrs) ++ map unintFnUIKind uis skolemMap = skolemize (if isSat then is else map flipQ is) where flipQ (ALL, x) = (EX, x)
Data/SBV/Provers/SExpr.hs view
@@ -7,22 +7,31 @@ -- Stability : experimental -- Portability : portable ----- Parsing of S-expressions (mainly used for parsing Yices output)+-- Parsing of S-expressions (mainly used for parsing SMT-Lib get-value output) ----------------------------------------------------------------------------- module Data.SBV.Provers.SExpr where import Control.Monad.Error () -- for Monad (Either String) instance import Data.Char (isDigit, ord)+import Data.List (isPrefixOf) import Numeric (readInt, readDec, readHex) -data SExpr = SCon String- | SNum Integer- | SApp [SExpr]+import Data.SBV.BitVectors.AlgReals +-- | ADT S-Expression format, suitable for representing get-model output of SMT-Lib+data SExpr = SCon String+ | SNum Integer+ | SReal AlgReal+ | SApp [SExpr]+ deriving Show++-- | Parse a string into an SExpr, potentially failing with an error message parseSExpr :: String -> Either String SExpr-parseSExpr inp = do (sexp, []) <- parse inpToks- return sexp+parseSExpr inp = do (sexp, extras) <- parse inpToks+ if null extras+ then return sexp+ else die "Extra tokens after valid input" where inpToks = let cln "" sofar = sofar cln ('(':r) sofar = cln r (" ( " ++ sofar) cln (')':r) sofar = cln r (" ) " ++ sofar)@@ -33,7 +42,8 @@ ++ "\n*** Input : <" ++ inp ++ ">" parse [] = die "ran out of tokens" parse ("(":toks) = do (f, r) <- parseApp toks []- return (SApp f, r)+ f' <- cvt (SApp f)+ return (f', r) parse (")":_) = die "extra tokens after close paren" parse [tok] = do t <- pTok tok return (t, [])@@ -44,11 +54,34 @@ parseApp r (f : sofar) parseApp (tok:toks) sofar = do t <- pTok tok parseApp toks (t : sofar)- pTok ('0':'b':r) = mkNum $ readInt 2 (`elem` "01") (\c -> ord c - ord '0') r- pTok ('b':'v':r) = mkNum $ readDec (takeWhile (/= '[') r)- pTok ('#':'b':r) = mkNum $ readInt 2 (`elem` "01") (\c -> ord c - ord '0') r- pTok ('#':'x':r) = mkNum $ readHex r- pTok n | all isDigit n = mkNum $ readDec n+ pTok ('0':'b':r) = mkNum $ readInt 2 (`elem` "01") (\c -> ord c - ord '0') r+ pTok ('b':'v':r) = mkNum $ readDec (takeWhile (/= '[') r)+ pTok ('#':'b':r) = mkNum $ readInt 2 (`elem` "01") (\c -> ord c - ord '0') r+ pTok ('#':'x':r) = mkNum $ readHex r+ pTok n+ | not (null n) && isDigit (head n)+ = if '.' `elem` n then getReal n+ else mkNum $ readDec n pTok n = return $ SCon n mkNum [(n, "")] = return $ SNum n mkNum _ = die "cannot read number"+ getReal n = return $ SReal $ mkPolyReal (Left (exact, n'))+ where exact = not ("?" `isPrefixOf` reverse n)+ n' | exact = n+ | True = init n+ -- simplify numbers and root-obj values+ cvt (SApp [SCon "/", SReal a, SReal b]) = return $ SReal (a / b)+ cvt (SApp [SCon "/", SReal a, SNum b]) = return $ SReal (a / fromInteger b)+ cvt (SApp [SCon "/", SNum a, SReal b]) = return $ SReal (fromInteger a / b)+ cvt (SApp [SCon "/", SNum a, SNum b]) = return $ SReal (fromInteger a / fromInteger b)+ cvt (SApp [SCon "-", SReal a]) = return $ SReal (-a)+ cvt (SApp [SCon "-", SNum a]) = return $ SNum (-a)+ cvt (SApp [SCon "root-obj", SApp (SCon "+":trms), SNum k]) = do ts <- mapM getCoeff trms+ return $ SReal $ mkPolyReal (Right (k, ts))+ cvt x = return x+ getCoeff (SApp [SCon "*", SNum k, SApp [SCon "^", SCon "x", SNum p]]) = return (k, p) -- kx^p+ getCoeff (SApp [SCon "*", SNum k, SCon "x" ] ) = return (k, 1) -- kx+ getCoeff ( SApp [SCon "^", SCon "x", SNum p] ) = return (1, p) -- x^p+ getCoeff ( SCon "x" ) = return (1, 1) -- x+ getCoeff ( SNum k ) = return (k, 0) -- k+ getCoeff x = die $ "Cannot parse a root-obj,\nProcessing term: " ++ show x
Data/SBV/Provers/Yices.hs view
@@ -80,8 +80,8 @@ matches -> error $ "SBV.Yices: Cannot uniquely identify value for " ++ 's':v ++ " in " ++ show matches isInput _ = Nothing- extract (SApp [SCon "=", SCon v, SNum i]) | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (hasSign s, sizeOf s) i))]- extract (SApp [SCon "=", SNum i, SCon v]) | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (hasSign s, sizeOf s) i))]+ extract (SApp [SCon "=", SCon v, SNum i]) | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (kindOf s) i))]+ extract (SApp [SCon "=", SNum i, SCon v]) | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (kindOf s) i))] extract _ = [] extractUnints :: [(String, UnintKind)] -> [String] -> [(UnintKind, [String])]
Data/SBV/Provers/Z3.hs view
@@ -18,10 +18,12 @@ import qualified Control.Exception as C import Data.Char (isDigit, toLower)-import Data.List (sortBy, intercalate, isPrefixOf)+import Data.Function (on)+import Data.List (sortBy, intercalate, isPrefixOf, groupBy) import System.Environment (getEnv) import qualified System.Info as S(os) +import Data.SBV.BitVectors.AlgReals import Data.SBV.BitVectors.Data import Data.SBV.Provers.SExpr import Data.SBV.SMT.SMT@@ -39,30 +41,43 @@ -- The default options are @\"\/in \/smt2\"@, which is valid for Z3 3.2. You can use the @SBV_Z3_OPTIONS@ environment variable to override the options. z3 :: SMTSolver z3 = SMTSolver {- name = "z3"- , executable = "z3"- , options = map (optionPrefix:) ["in", "smt2"]- , engine = \cfg isSat qinps modelMap skolemMap pgm -> do- execName <- getEnv "SBV_Z3" `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))- execOpts <- (words `fmap` getEnv "SBV_Z3_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg)))- let cfg' = cfg { solver = (solver cfg) {executable = execName, options = addTimeOut (timeOut cfg) execOpts} }- script = SMTScript {scriptBody = unlines (solverTweaks cfg') ++ pgm, scriptModel = Just (cont skolemMap)}- standardSolver cfg' script cleanErrs (ProofError cfg') (interpretSolverOutput cfg' (extractMap isSat qinps modelMap . zipWith match skolemMap))+ name = "z3"+ , executable = "z3"+ , options = map (optionPrefix:) ["in", "smt2"]+ , engine = \cfg isSat qinps modelMap skolemMap pgm -> do+ execName <- getEnv "SBV_Z3" `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))+ execOpts <- (words `fmap` getEnv "SBV_Z3_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg)))+ let cfg' = cfg { solver = (solver cfg) {executable = execName, options = addTimeOut (timeOut cfg) execOpts} }+ tweaks = case solverTweaks cfg' of+ [] -> ""+ ts -> unlines $ "; --- user given solver tweaks ---" : ts ++ ["; --- end of user given tweaks ---"]+ dlim = printRealPrec cfg'+ ppDecLim = "(set-option :pp-decimal-precision " ++ show dlim ++ ")\n"+ script = SMTScript {scriptBody = tweaks ++ ppDecLim ++ pgm, scriptModel = Just (cont skolemMap)}+ if dlim < 1+ then error $ "SBV.Z3: printRealPrec value should be at least 1, invalid value received: " ++ show dlim+ else standardSolver cfg' script cleanErrs (ProofError cfg') (interpretSolverOutput cfg' (extractMap isSat qinps modelMap . match skolemMap)) }- where cleanErrs = intercalate "\n" . filter (not . junk) . lines- junk s | "WARNING:" `isPrefixOf` s = True- junk _ = False- zero :: Size -> String- zero (Size Nothing) = "0"- zero (Size (Just 1)) = "#b0"- zero (Size (Just sz)) = "#x" ++ replicate (sz `div` 4) '0'- cont skolemMap = intercalate "\n" $ map extract skolemMap- where extract (Left s) = "(echo \"((" ++ show s ++ " " ++ zero (sizeOf s) ++ "))\")"- extract (Right (s, [])) = "(get-value (" ++ show s ++ "))"- extract (Right (s, ss)) = "(eval (" ++ show s ++ concat [' ' : zero (sizeOf a) | a <- ss] ++ "))"- match (Left _) l = l- match (Right (_, [])) l = l- match (Right (s, _)) l = "((" ++ show s ++ " " ++ l ++ "))"+ where -- Get rid of the following when z3_4.0 is out+ cleanErrs = intercalate "\n" . filter (not . junk) . lines+ junk = ("WARNING:" `isPrefixOf`)+ zero :: Kind -> String+ zero (KBounded False 1) = "#b0"+ zero (KBounded _ sz) = "#x" ++ replicate (sz `div` 4) '0'+ zero KUnbounded = "0"+ zero KReal = "0.0"+ cont skolemMap = intercalate "\n" $ concatMap extract skolemMap+ where extract (Left s) = ["(echo \"((" ++ show s ++ " " ++ zero (kindOf s) ++ "))\")"]+ extract (Right (s, [])) = let g = "(get-value (" ++ show s ++ "))" in getVal (kindOf s) g+ extract (Right (s, ss)) = let g = "(eval (" ++ show s ++ concat [' ' : zero (kindOf a) | a <- ss] ++ "))" in getVal (kindOf s) g+ getVal KReal g = ["(set-option :pp-decimal false)", g, "(set-option :pp-decimal true)", g]+ getVal _ g = [g]+ match skolemMap = zipWith annotate (concatMap dupRight skolemMap)+ where dupRight (Left s) = [Left s]+ dupRight (Right x) = [Right x, Right x]+ annotate (Left _) l = l+ annotate (Right (_, [])) l = l+ annotate (Right (s, _)) l = "((" ++ show s ++ " " ++ l ++ "))" addTimeOut Nothing o = o addTimeOut (Just i) o | i < 0 = error $ "Z3: Timeout value must be non-negative, received: " ++ show i@@ -70,12 +85,12 @@ extractMap :: Bool -> [(Quantifier, NamedSymVar)] -> [(String, UnintKind)] -> [String] -> SMTModel extractMap isSat qinps _modelMap solverLines =- SMTModel { modelAssocs = map snd $ sortByNodeId $ concatMap (getCounterExample inps) solverLines+ SMTModel { modelAssocs = map snd $ squashReals $ sortByNodeId $ concatMap (getCounterExample inps) solverLines , modelUninterps = [] , modelArrays = [] } where sortByNodeId :: [(Int, a)] -> [(Int, a)]- sortByNodeId = sortBy (\(x, _) (y, _) -> compare x y)+ sortByNodeId = sortBy (compare `on` fst) inps -- for "sat", display the prefix existentials. For completeness, we will drop -- only the trailing foralls. Exception: Don't drop anything if it's all a sequence of foralls | isSat = if all (== ALL) (map fst qinps)@@ -83,6 +98,14 @@ else map snd $ reverse $ dropWhile ((== ALL) . fst) $ reverse qinps -- for "proof", just display the prefix universals | True = map snd $ takeWhile ((== ALL) . fst) qinps+ squashReals :: [(Int, (String, CW))] -> [(Int, (String, CW))]+ squashReals = concatMap squash . groupBy ((==) `on` fst)+ where squash [(i, (n, cw1)), (_, (_, cw2))] = [(i, (n, mergeReals n cw1 cw2))]+ squash xs = xs+ mergeReals :: String -> CW -> CW -> CW+ mergeReals n (CW KReal (Left a)) (CW KReal (Left b)) = CW KReal (Left (mergeAlgReals (error (bad n a b)) a b))+ mergeReals n a b = error $ bad n a b+ bad n a b = "SBV.Z3: Cannot merge reals for variable: " ++ n ++ " received: " ++ show (a, b) getCounterExample :: [NamedSymVar] -> String -> [(Int, (String, CW))] getCounterExample inps line = either err extract (parseSExpr line)@@ -98,8 +121,7 @@ matches -> error $ "SBV.SMTLib2: Cannot uniquely identify value for " ++ 's':v ++ " in " ++ show matches isInput _ = Nothing- extract (SApp [SApp [SCon v, SNum i]])- | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (hasSign s, sizeOf s) i))]- extract (SApp [SApp [SCon v, SApp [SCon "-", SNum i]]])- | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (hasSign s, sizeOf s) (-i)))]- extract _ = []+ extract (SApp [SApp [SCon v, SNum i]]) | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (kindOf s) i))]+ extract (SApp [SApp [SCon v, SReal i]]) | Just (n, _, nm) <- isInput v = [(n, (nm, CW KReal (Left i)))]+ extract (SApp [SApp (SCon v : r)]) | Just{} <- isInput v = error $ "SBV.SMTLib2: Cannot extract value for " ++ show ('s':v) ++ ", received:\n\t" ++ show r+ extract _ = []
Data/SBV/SMT/SMT.hs view
@@ -29,22 +29,37 @@ import System.Exit (ExitCode(..)) import System.IO (hClose, hFlush, hPutStr, hGetContents, hGetLine) +import Data.SBV.BitVectors.AlgReals import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.PrettyNum import Data.SBV.Utils.TDiff --- | Solver configuration+-- | Solver configuration. See also 'z3' and 'yices', which are instantiations of this type for those solvers, with+-- reasonable defaults. In particular, custom configuration can be created by varying those values. (Such as @z3{verbose=True}@.)+--+-- Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does+-- not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to+-- emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite+-- precision value on the screen. The field 'printRealPrec' controls the printing precision, by specifying the number of digits after+-- the decimal point. The default value is 16, but it can be set to any positive integer.+--+-- When printing, SBV will add the suffix @...@ at the and of a real-value, if the given bound is not sufficient to represent the real-value+-- exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it+-- is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation+-- of the real value is not finite, i.e., if it is not rational. data SMTConfig = SMTConfig {- verbose :: Bool -- ^ Debug mode- , timing :: Bool -- ^ Print timing information on how long different phases took (construction, solving, etc.)- , timeOut :: Maybe Int -- ^ How much time to give to the solver. (In seconds)- , printBase :: Int -- ^ Print literals in this base- , solver :: SMTSolver -- ^ The actual SMT solver- , solverTweaks :: [String] -- ^ Additional lines of script to give to the solver (user specified)- , smtFile :: Maybe FilePath -- ^ If Just, the generated SMT script will be put in this file (for debugging purposes mostly)- , useSMTLib2 :: Bool -- ^ If True, we'll treat the solver as using SMTLib2 input format. Otherwise, SMTLib1+ verbose :: Bool -- ^ Debug mode+ , timing :: Bool -- ^ Print timing information on how long different phases took (construction, solving, etc.)+ , timeOut :: Maybe Int -- ^ How much time to give to the solver. (In seconds)+ , printBase :: Int -- ^ Print integral literals in this base (2, 8, and 10, and 16 are supported.)+ , printRealPrec :: Int -- ^ Print algebraic real values with this precision. (SReal, default: 16)+ , solverTweaks :: [String] -- ^ Additional lines of script to give to the solver (user specified)+ , smtFile :: Maybe FilePath -- ^ If Just, the generated SMT script will be put in this file (for debugging purposes mostly)+ , useSMTLib2 :: Bool -- ^ If True, we'll treat the solver as using SMTLib2 input format. Otherwise, SMTLib1+ , solver :: SMTSolver -- ^ The actual SMT solver. } +-- | An SMT engine type SMTEngine = SMTConfig -> Bool -> [(Quantifier, NamedSymVar)] -> [(String, UnintKind)] -> [Either SW (SW, [SW])] -> String -> IO SMTResult -- | An SMT solver@@ -80,6 +95,7 @@ , scriptModel :: Maybe String -- ^ Optional continuation script, if the result is sat } +-- | Extract the final configuration from a result resultConfig :: SMTResult -> SMTConfig resultConfig (Unsatisfiable c) = c resultConfig (Satisfiable c _) = c@@ -118,7 +134,6 @@ "Unknown" "Unknown. Potential model:\n" "Satisfiable" "Satisfiable. Model:\n" r - -- NB. The Show instance of AllSatResults have to be careful in being lazy enough -- as the typical use case is to pull results out as they become available. instance Show AllSatResult where@@ -133,8 +148,8 @@ 1 -> "This is the only solution." ++ uniqueWarn _ -> "Found " ++ show c ++ " different solutions." ++ uniqueWarn sh i c = (ok, showSMTResult "Unsatisfiable"- ("Unknown #" ++ show i ++ "(No assignment to variables returned)") "Unknown. Potential assignment:\n"- ("Solution #" ++ show i ++ " (No assignment to variables returned)") ("Solution #" ++ show i ++ ":\n") c)+ "Unknown" "Unknown. Potential model:\n"+ ("Solution #" ++ show i ++ ":\n[Backend solver returned no assignment to variables.]") ("Solution #" ++ show i ++ ":\n") c) where ok = case c of Satisfiable{} -> True _ -> False@@ -155,46 +170,50 @@ cvtModel :: (a -> Maybe b) -> Maybe (a, [CW]) -> Maybe (b, [CW]) cvtModel f x = x >>= \(a, r) -> f a >>= \b -> return (b, r) -genParse :: Integral a => (Bool, Size) -> [CW] -> Maybe (a, [CW])-genParse (signed, size) (x:r)- | hasSign x == signed && sizeOf x == size = Just (fromIntegral (cwVal x),r)-genParse _ _ = Nothing+-- | Parse a signed/sized value from a sequence of CWs+genParse :: Integral a => Kind -> [CW] -> Maybe (a, [CW])+genParse k (x@(CW _ (Right i)):r) | kindOf x == k = Just (fromIntegral i, r)+genParse _ _ = Nothing --- base case, that comes in handy if there are no real variables+-- | Base case, that comes in handy if there are no real variables instance SatModel () where parseCWs xs = return ((), xs) instance SatModel Bool where- parseCWs xs = do (x, r) <- genParse (False, Size (Just 1)) xs+ parseCWs xs = do (x, r) <- genParse (KBounded False 1) xs return ((x :: Integer) /= 0, r) instance SatModel Word8 where- parseCWs = genParse (False, Size (Just 8))+ parseCWs = genParse (KBounded False 8) instance SatModel Int8 where- parseCWs = genParse (True, Size (Just 8))+ parseCWs = genParse (KBounded True 8) instance SatModel Word16 where- parseCWs = genParse (False, Size (Just 16))+ parseCWs = genParse (KBounded False 16) instance SatModel Int16 where- parseCWs = genParse (True, Size (Just 16))+ parseCWs = genParse (KBounded True 16) instance SatModel Word32 where- parseCWs = genParse (False, Size (Just 32))+ parseCWs = genParse (KBounded False 32) instance SatModel Int32 where- parseCWs = genParse (True, Size (Just 32))+ parseCWs = genParse (KBounded True 32) instance SatModel Word64 where- parseCWs = genParse (False, Size (Just 64))+ parseCWs = genParse (KBounded False 64) instance SatModel Int64 where- parseCWs = genParse (True, Size (Just 64))+ parseCWs = genParse (KBounded True 64) instance SatModel Integer where- parseCWs = genParse (True, Size Nothing)+ parseCWs = genParse KUnbounded +instance SatModel AlgReal where+ parseCWs (CW KReal (Left i) : r) = Just (i, r)+ parseCWs _ = Nothing+ -- when reading a list; go as long as we can (maximal-munch) -- note that this never fails.. instance SatModel a => SatModel [a] where@@ -272,6 +291,7 @@ modelExists (Unknown{}) = False -- don't risk it modelExists _ = False +-- | Extract a model out, will throw error if parsing is unsuccessful parseModelOut :: SatModel a => SMTModel -> a parseModelOut m = case parseCWs [c | (_, c) <- modelAssocs m] of Just (x, []) -> x@@ -288,6 +308,7 @@ return $ last (0:inds) where display r i = disp i r >> return i +-- | Show an SMTResult; generic version showSMTResult :: String -> String -> String -> String -> String -> SMTResult -> String showSMTResult unsatMsg unkMsg unkMsgModel satMsg satMsgModel result = case result of Unsatisfiable _ -> unsatMsg@@ -300,12 +321,15 @@ TimeOut _ -> "*** Timeout" where cfg = resultConfig result +-- | Show a model in human readable form showModel :: SMTConfig -> SMTModel -> String-showModel cfg m = intercalate "\n" (map (shM cfg) assocs ++ concatMap shUI uninterps ++ concatMap shUA arrs)- where assocs = modelAssocs m- uninterps = modelUninterps m- arrs = modelArrays m+showModel cfg m = intercalate "\n" (map shM assocs ++ concatMap shUI uninterps ++ concatMap shUA arrs)+ where assocs = modelAssocs m+ uninterps = modelUninterps m+ arrs = modelArrays m+ shM (s, v) = " " ++ s ++ " = " ++ shCW cfg v +-- | Show a constant value, in the user-specified base shCW :: SMTConfig -> CW -> String shCW = sh . printBase where sh 2 = binS@@ -313,21 +337,19 @@ sh 16 = hexS sh n = \w -> show w ++ " -- Ignoring unsupported printBase " ++ show n ++ ", use 2, 10, or 16." -shM :: SMTConfig -> (String, CW) -> String-shM cfg (s, v) = " " ++ s ++ " = " ++ shCW cfg v---- very crude.. printing uninterpreted functions+-- | Print uninterpreted function values from models. Very, very crude.. shUI :: (String, [String]) -> [String] shUI (flong, cases) = (" -- uninterpreted: " ++ f) : map shC cases where tf = dropWhile (/= '_') flong f = if null tf then flong else tail tf shC s = " " ++ s --- very crude.. printing array values+-- | Print uninterpreted array values from models. Very, very crude.. shUA :: (String, [String]) -> [String] shUA (f, cases) = (" -- array: " ++ f) : map shC cases where shC s = " " ++ s +-- | Helper function to spin off to an SMT solver. pipeProcess :: Bool -> String -> String -> [String] -> SMTScript -> (String -> String) -> IO (Either String [String]) pipeProcess verb nm execName opts script cleanErrs = do mbExecPath <- findExecutable execName@@ -357,6 +379,8 @@ where clean = reverse . dropWhile isSpace . reverse . dropWhile isSpace line = replicate 78 '=' +-- | A standard solver interface. If the solver is SMT-Lib compliant, then this function should suffice in+-- communicating with it. standardSolver :: SMTConfig -> SMTScript -> (String -> String) -> ([String] -> a) -> ([String] -> a) -> IO a standardSolver config script cleanErrs failure success = do let msg = when (verbose config) . putStrLn . ("** " ++)@@ -376,8 +400,8 @@ Left e -> return $ failure (lines e) Right xs -> return $ success xs --- A variant of readProcessWithExitCode; except it knows about continuation strings--- and can speak SMT-Lib2 (just a little)+-- | A variant of 'readProcessWithExitCode'; except it knows about continuation strings+-- and can speak SMT-Lib2 (just a little). runSolver :: Bool -> FilePath -> [String] -> SMTScript -> IO (ExitCode, String, String) runSolver verb execPath opts script | isNothing $ scriptModel script
Data/SBV/SMT/SMTLib.hs view
@@ -17,32 +17,40 @@ import qualified Data.SBV.SMT.SMTLib1 as SMT1 import qualified Data.SBV.SMT.SMTLib2 as SMT2 -type SMTLibConverter = Bool -- ^ has infinite precision values- -> Bool -- ^ is this a sat problem?- -> [String] -- ^ extra comments to place on top- -> [(Quantifier, NamedSymVar)] -- ^ inputs and aliasing names- -> [Either SW (SW, [SW])] -- ^ skolemized inputs- -> [(SW, CW)] -- ^ constants- -> [((Int, (Bool, Size), (Bool, Size)), [SW])] -- ^ auto-generated tables- -> [(Int, ArrayInfo)] -- ^ user specified arrays- -> [(String, SBVType)] -- ^ uninterpreted functions/constants- -> [(String, [String])] -- ^ user given axioms- -> Pgm -- ^ assignments- -> [SW] -- ^ extra constraints- -> SW -- ^ output variable+-- | An instance of SMT-Lib converter; instantiated for SMT-Lib v1 and v2. (And potentially for+-- newer versions in the future.)+type SMTLibConverter = Bool -- ^ has infinite precision values+ -> Bool -- ^ is this a sat problem?+ -> [String] -- ^ extra comments to place on top+ -> [(Quantifier, NamedSymVar)] -- ^ inputs and aliasing names+ -> [Either SW (SW, [SW])] -- ^ skolemized inputs+ -> [(SW, CW)] -- ^ constants+ -> [((Int, Kind, Kind), [SW])] -- ^ auto-generated tables+ -> [(Int, ArrayInfo)] -- ^ user specified arrays+ -> [(String, SBVType)] -- ^ uninterpreted functions/constants+ -> [(String, [String])] -- ^ user given axioms+ -> Pgm -- ^ assignments+ -> [SW] -- ^ extra constraints+ -> SW -- ^ output variable -> SMTLibPgm -toSMTLib1, toSMTLib2 :: SMTLibConverter+-- | Convert to SMTLib-1 format+toSMTLib1 :: SMTLibConverter++-- | Convert to SMTLib-2 format+toSMTLib2 :: SMTLibConverter (toSMTLib1, toSMTLib2) = (cvt SMTLib1, cvt SMTLib2) where cvt v hasInfPrec isSat comments qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out = SMTLibPgm v (aliasTable, pre, post) where aliasTable = map (\(_, (x, y)) -> (y, x)) qinps converter = if v == SMTLib1 then SMT1.cvt else SMT2.cvt (pre, post) = converter hasInfPrec isSat comments qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out +-- | Add constraints generated from older models, used for querying new models addNonEqConstraints :: [(Quantifier, NamedSymVar)] -> [[(String, CW)]] -> SMTLibPgm -> Maybe String addNonEqConstraints _qinps cs p@(SMTLibPgm SMTLib1 _) = SMT1.addNonEqConstraints cs p addNonEqConstraints qinps cs p@(SMTLibPgm SMTLib2 _) = SMT2.addNonEqConstraints qinps cs p +-- | Interpret solver output based on SMT-Lib standard output responses interpretSolverOutput :: SMTConfig -> ([String] -> SMTModel) -> [String] -> SMTResult interpretSolverOutput cfg _ ("unsat":_) = Unsatisfiable cfg interpretSolverOutput cfg extractMap ("unknown":rest) = Unknown cfg $ extractMap rest
Data/SBV/SMT/SMTLib1.hs view
@@ -15,10 +15,11 @@ import qualified Data.Foldable as F (toList) import Data.List (intercalate)-import Data.Maybe (fromMaybe) import Data.SBV.BitVectors.Data +-- | Add constraints to generate /new/ models. This function is used to query the SMT-solver, while+-- disallowing a previous model. addNonEqConstraints :: [[(String, CW)]] -> SMTLibPgm -> Maybe String addNonEqConstraints nonEqConstraints (SMTLibPgm _ (aliasTable, pre, post)) = Just $ intercalate "\n" $ pre@@ -39,19 +40,20 @@ nonEq :: (String, CW) -> String nonEq (s, c) = "(not (= " ++ s ++ " " ++ cvtCW c ++ "))" -cvt :: Bool -- ^ has infinite precision values- -> Bool -- ^ is this a sat problem?- -> [String] -- ^ extra comments to place on top- -> [(Quantifier, NamedSymVar)] -- ^ inputs- -> [Either SW (SW, [SW])] -- ^ skolemized version of the inputs- -> [(SW, CW)] -- ^ constants- -> [((Int, (Bool, Size), (Bool, Size)), [SW])] -- ^ auto-generated tables- -> [(Int, ArrayInfo)] -- ^ user specified arrays- -> [(String, SBVType)] -- ^ uninterpreted functions/constants- -> [(String, [String])] -- ^ user given axioms- -> Pgm -- ^ assignments- -> [SW] -- ^ extra constraints- -> SW -- ^ output variable+-- | Translate a problem into an SMTLib1 script+cvt :: Bool -- ^ has infinite precision values+ -> Bool -- ^ is this a sat problem?+ -> [String] -- ^ extra comments to place on top+ -> [(Quantifier, NamedSymVar)] -- ^ inputs+ -> [Either SW (SW, [SW])] -- ^ skolemized version of the inputs+ -> [(SW, CW)] -- ^ constants+ -> [((Int, Kind, Kind), [SW])] -- ^ auto-generated tables+ -> [(Int, ArrayInfo)] -- ^ user specified arrays+ -> [(String, SBVType)] -- ^ uninterpreted functions/constants+ -> [(String, [String])] -- ^ user given axioms+ -> Pgm -- ^ assignments+ -> [SW] -- ^ extra constraints+ -> SW -- ^ output variable -> ([String], [String]) cvt hasInf isSat comments qinps _skolemInps consts tbls arrs uis axs asgnsSeq cstrs out | hasInf@@ -102,23 +104,25 @@ -- Currently we ignore the signedness of the arguments, as there appears to be no way -- to capture that in SMT-Lib; and likely it does not matter. Would be good to check -- explicitly though.-mkTable :: ((Int, (Bool, Size), (Bool, Size)), [SW]) -> [String]-mkTable ((i, (_, atSz), (_, rtSz)), elts) = (" :extrafuns ((" ++ t ++ " Array[" ++ show at ++ ":" ++ show rt ++ "]))") : zipWith mkElt elts [(0::Int)..]+mkTable :: ((Int, Kind, Kind), [SW]) -> [String]+mkTable ((i, ak, rk), elts) = (" :extrafuns ((" ++ t ++ " Array[" ++ show at ++ ":" ++ show rt ++ "]))") : zipWith mkElt elts [(0::Int)..] where t = "table" ++ show i mkElt x k = " :assumption (= (select " ++ t ++ " bv" ++ show k ++ "[" ++ show at ++ "]) " ++ show x ++ ")"- at = fromMaybe (die "Unbounded integers") (unSize atSz)- rt = fromMaybe (die "Unbounded integers") (unSize rtSz)+ (at, rt) = case (ak, rk) of+ (KBounded _ a, KBounded _ b) -> (a, b)+ _ -> die $ "mkTable: Unbounded table component: " ++ show (ak, rk) -- Unexpected input, or things we will probably never support die :: String -> a die msg = error $ "SBV->SMTLib1: Unexpected: " ++ msg declArray :: (Int, ArrayInfo) -> [String]-declArray (i, (_, ((_, atSz), (_, rtSz)), ctx)) = adecl : ctxInfo+declArray (i, (_, (ak, rk), ctx)) = adecl : ctxInfo where nm = "array_" ++ show i adecl = " :extrafuns ((" ++ nm ++ " Array[" ++ show at ++ ":" ++ show rt ++ "]))"- at = fromMaybe (die "Unbounded integers") (unSize atSz)- rt = fromMaybe (die "Unbounded integers") (unSize rtSz)+ (at, rt) = case (ak, rk) of+ (KBounded _ a, KBounded _ b) -> (a, b)+ _ -> die $ "declArray: Unbounded array component: " ++ show (ak, rk) ctxInfo = case ctx of ArrayFree Nothing -> [] ArrayFree (Just sw) -> declA sw@@ -151,15 +155,16 @@ cvtCnst :: (SW, CW) -> String cvtCnst (s, c) = " :assumption (= " ++ show s ++ " " ++ cvtCW c ++ ")" +-- no need to worry about Int/Real here as we don't support them with the SMTLib1 interface.. cvtCW :: CW -> String-cvtCW x | not (hasSign x) = "bv" ++ show (cwVal x) ++ "[" ++ show (intSizeOf x) ++ "]"+cvtCW x@(CW _ (Right v)) | not (hasSign x) = "bv" ++ show v ++ "[" ++ show (intSizeOf x) ++ "]" -- signed numbers (with 2's complement representation) is problematic -- since there's no way to put a bvneg over a positive number to get minBound.. -- Hence, we punt and use binary notation in that particular case-cvtCW x | cwVal x == least = mkMinBound (intSizeOf x)+cvtCW x@(CW _ (Right v)) | v == least = mkMinBound (intSizeOf x) where least = negate (2 ^ intSizeOf x)-cvtCW x = negIf (w < 0) $ "bv" ++ show (abs w) ++ "[" ++ show (intSizeOf x) ++ "]"- where w = cwVal x+cvtCW x@(CW _ (Right v)) = negIf (v < 0) $ "bv" ++ show (abs v) ++ "[" ++ show (intSizeOf x) ++ "]"+cvtCW x = error $ "SBV.SMTLib1.cvtCW: Unexpected CW: " ++ show x -- unbounded/real, shouldn't reach here negIf :: Bool -> String -> String negIf True a = "(bvneg " ++ a ++ ")"@@ -173,11 +178,12 @@ rot :: String -> Int -> SW -> String rot o c x = "(" ++ o ++ "[" ++ show c ++ "] " ++ show x ++ ")" +-- only used for bounded SWs shft :: String -> String -> Int -> SW -> String-shft oW oS c x= "(" ++ o ++ " " ++ show x ++ " " ++ cvtCW c' ++ ")"+shft oW oS c x = "(" ++ o ++ " " ++ show x ++ " " ++ cvtCW c' ++ ")" where s = hasSign x- c' = mkConstCW (s, sizeOf x) c- o = if hasSign x then oS else oW+ c' = mkConstCW (kindOf x) c+ o = if s then oS else oW cvtExp :: SBVExpr -> String cvtExp (SBVApp Ite [a, b, c]) = "(ite (= bv1[1] " ++ show a ++ ") " ++ show b ++ " " ++ show c ++ ")"@@ -185,17 +191,19 @@ cvtExp (SBVApp (Ror i) [a]) = rot "rotate_right" i a cvtExp (SBVApp (Shl i) [a]) = shft "bvshl" "bvshl" i a cvtExp (SBVApp (Shr i) [a]) = shft "bvlshr" "bvashr" i a-cvtExp (SBVApp (LkUp (t, (_, atSz), _, l) i e) [])+cvtExp (SBVApp (LkUp (t, ak, _, l) i e) []) | needsCheck = "(ite " ++ cond ++ show e ++ " " ++ lkUp ++ ")" | True = lkUp- where at = fromMaybe (die "Unbounded integers") (unSize atSz)+ where at = case ak of+ KBounded _ n -> n+ _ -> die $ "cvtExp: Unbounded lookup component" ++ show ak needsCheck = (2::Integer)^at > fromIntegral l lkUp = "(select table" ++ show t ++ " " ++ show i ++ ")" cond | hasSign i = "(or " ++ le0 ++ " " ++ gtl ++ ") " | True = gtl ++ " " (less, leq) = if hasSign i then ("bvslt", "bvsle") else ("bvult", "bvule")- mkCnst = cvtCW . mkConstCW (hasSign i, sizeOf i)+ mkCnst = cvtCW . mkConstCW (kindOf i) le0 = "(" ++ less ++ " " ++ show i ++ " " ++ mkCnst 0 ++ ")" gtl = "(" ++ leq ++ " " ++ mkCnst l ++ " " ++ show i ++ ")" cvtExp (SBVApp (Extract i j) [a]) = "(extract[" ++ show i ++ ":" ++ show j ++ "] " ++ show a ++ ")"@@ -240,5 +248,6 @@ cvtType :: SBVType -> String cvtType (SBVType []) = error "SBV.SMT.SMTLib1.cvtType: internal: received an empty type!" cvtType (SBVType xs) = unwords $ map sh xs- where sh (_, Size Nothing) = die "unbounded Integer"- sh (_, Size (Just s)) = "BitVec[" ++ show s ++ "]"+ where sh (KBounded _ s) = "BitVec[" ++ show s ++ "]"+ sh KUnbounded = die "unbounded Integer"+ sh KReal = die "real value"
Data/SBV/SMT/SMTLib2.hs view
@@ -20,8 +20,11 @@ import Data.List (intercalate, partition) import Numeric (showHex) +import Data.SBV.BitVectors.AlgReals import Data.SBV.BitVectors.Data +-- | Add constraints to generate /new/ models. This function is used to query the SMT-solver, while+-- disallowing a previous model. addNonEqConstraints :: [(Quantifier, NamedSymVar)] -> [[(String, CW)]] -> SMTLibPgm -> Maybe String addNonEqConstraints qinps allNonEqConstraints (SMTLibPgm _ (aliasTable, pre, post)) | null allNonEqConstraints@@ -54,24 +57,25 @@ tbd :: String -> a tbd e = error $ "SBV.SMTLib2: Not-yet-supported: " ++ e -cvt :: Bool -- ^ has infinite precision values- -> Bool -- ^ is this a sat problem?- -> [String] -- ^ extra comments to place on top- -> [(Quantifier, NamedSymVar)] -- ^ inputs- -> [Either SW (SW, [SW])] -- ^ skolemized version inputs- -> [(SW, CW)] -- ^ constants- -> [((Int, (Bool, Size), (Bool, Size)), [SW])] -- ^ auto-generated tables- -> [(Int, ArrayInfo)] -- ^ user specified arrays- -> [(String, SBVType)] -- ^ uninterpreted functions/constants- -> [(String, [String])] -- ^ user given axioms- -> Pgm -- ^ assignments- -> [SW] -- ^ extra constraints- -> SW -- ^ output variable+-- | Translate a problem into an SMTLib2 script+cvt :: Bool -- ^ has infinite precision values+ -> Bool -- ^ is this a sat problem?+ -> [String] -- ^ extra comments to place on top+ -> [(Quantifier, NamedSymVar)] -- ^ inputs+ -> [Either SW (SW, [SW])] -- ^ skolemized version inputs+ -> [(SW, CW)] -- ^ constants+ -> [((Int, Kind, Kind), [SW])] -- ^ auto-generated tables+ -> [(Int, ArrayInfo)] -- ^ user specified arrays+ -> [(String, SBVType)] -- ^ uninterpreted functions/constants+ -> [(String, [String])] -- ^ user given axioms+ -> Pgm -- ^ assignments+ -> [SW] -- ^ extra constraints+ -> SW -- ^ output variable -> ([String], [String]) cvt hasInf isSat comments _inps skolemInps consts tbls arrs uis axs asgnsSeq cstrs out = (pre, []) where -- the logic is an over-approaximation logic- | hasInf = ["; Has unbounded Integers; no logic specified."] -- combination, let the solver pick+ | hasInf = ["; Has unbounded values (Int/Real); no logic specified."] -- combination, let the solver pick | True = ["(set-logic " ++ qs ++ as ++ ufs ++ "BV)"] where qs | null foralls && null axs = "QF_" -- axioms are likely to contain quantifiers | True = ""@@ -81,10 +85,11 @@ | True = "UF" pre = ["; Automatically generated by SBV. Do not edit."] ++ map ("; " ++) comments- ++ logic ++ [ "(set-option :produce-models true)"+ , "(set-option :pp-decimal false)" , "; --- literal constants ---" ]+ ++ logic ++ map declConst consts ++ [ "; --- skolem constants ---" ] ++ [ "(declare-fun " ++ show s ++ " " ++ swFunType ss s ++ ")" | Right (s, ss) <- skolemInps]@@ -143,28 +148,28 @@ declAx :: (String, [String]) -> String declAx (nm, ls) = (";; -- user given axiom: " ++ nm ++ "\n ") ++ intercalate "\n" ls -constTable :: (((Int, (Bool, Size), (Bool, Size)), [SW]), [String]) -> [String]-constTable (((i, (_, atSz), (_, rtSz)), _elts), is) = decl : map wrap is+constTable :: (((Int, Kind, Kind), [SW]), [String]) -> [String]+constTable (((i, ak, rk), _elts), is) = decl : map wrap is where t = "table" ++ show i- decl = "(declare-fun " ++ t ++ " (" ++ smtType atSz ++ ") " ++ smtType rtSz ++ ")"+ decl = "(declare-fun " ++ t ++ " (" ++ smtType ak ++ ") " ++ smtType rk ++ ")" wrap s = "(assert " ++ s ++ ")" -skolemTable :: String -> (((Int, (Bool, Size), (Bool, Size)), [SW]), [String]) -> String-skolemTable qsIn (((i, (_, atSz), (_, rtSz)), _elts), _) = decl+skolemTable :: String -> (((Int, Kind, Kind), [SW]), [String]) -> String+skolemTable qsIn (((i, ak, rk), _elts), _) = decl where qs = if null qsIn then "" else qsIn ++ " " t = "table" ++ show i- decl = "(declare-fun " ++ t ++ " (" ++ qs ++ smtType atSz ++ ") " ++ smtType rtSz ++ ")"+ decl = "(declare-fun " ++ t ++ " (" ++ qs ++ smtType ak ++ ") " ++ smtType rk ++ ")" -- Left if all constants, Right if otherwise-genTableData :: SkolemMap -> (Bool, String) -> [SW] -> ((Int, (Bool, Size), (Bool, Size)), [SW]) -> Either [String] [String]-genTableData skolemMap (_quantified, args) consts ((i, (sa, at), (_, _rt)), elts)+genTableData :: SkolemMap -> (Bool, String) -> [SW] -> ((Int, Kind, Kind), [SW]) -> Either [String] [String]+genTableData skolemMap (_quantified, args) consts ((i, aknd, _), elts) | null post = Left (map (topLevel . snd) pre) | True = Right (map (nested . snd) (pre ++ post)) where ssw = cvtSW skolemMap (pre, post) = partition fst (zipWith mkElt elts [(0::Int)..]) t = "table" ++ show i mkElt x k = (isReady, (idx, ssw x))- where idx = cvtCW (mkConstCW (sa, at) k)+ where idx = cvtCW (mkConstCW aknd k) isReady = x `elem` consts topLevel (idx, v) = "(= (" ++ t ++ " " ++ idx ++ ") " ++ v ++ ")" nested (idx, v) = "(= (" ++ t ++ args ++ " " ++ idx ++ ") " ++ v ++ ")"@@ -174,7 +179,7 @@ -- The difficulty is with the ArrayReset/Mutate/Merge: We have to postpone an init if -- the components are themselves postponed, so this cannot be implemented as a simple map. declArray :: Bool -> [SW] -> SkolemMap -> (Int, ArrayInfo) -> ([String], [String])-declArray quantified consts skolemMap (i, (_, ((_, atSz), (_, rtSz)), ctx)) = (adecl : map wrap pre, map snd post)+declArray quantified consts skolemMap (i, (_, (aKnd, bKnd), ctx)) = (adecl : map wrap pre, map snd post) where topLevel = not quantified || case ctx of ArrayFree Nothing -> True ArrayFree (Just sw) -> sw `elem` consts@@ -188,7 +193,7 @@ = cvtSW skolemMap sw | True = tbd "Non-constant array initializer in a quantified context"- adecl = "(declare-fun " ++ nm ++ "() (Array " ++ smtType atSz ++ " " ++ smtType rtSz ++ "))"+ adecl = "(declare-fun " ++ nm ++ "() (Array " ++ smtType aKnd ++ " " ++ smtType bKnd ++ "))" ctxInfo = case ctx of ArrayFree Nothing -> [] ArrayFree (Just sw) -> declA sw@@ -196,27 +201,27 @@ ArrayMutate j a b -> [(all (`elem` consts) [a, b], "(= " ++ nm ++ " (store array_" ++ show j ++ " " ++ ssw a ++ " " ++ ssw b ++ "))")] ArrayMerge t j k -> [(t `elem` consts, "(= " ++ nm ++ " (ite (= #b1 " ++ ssw t ++ ") array_" ++ show j ++ " array_" ++ show k ++ "))")] declA sw = let iv = nm ++ "_freeInitializer"- in [ (True, "(declare-fun " ++ iv ++ "() " ++ smtType atSz ++ ")")+ in [ (True, "(declare-fun " ++ iv ++ "() " ++ smtType aKnd ++ ")") , (sw `elem` consts, "(= (select " ++ nm ++ " " ++ iv ++ ") " ++ ssw sw ++ ")") ] wrap (False, s) = s wrap (True, s) = "(assert " ++ s ++ ")" swType :: SW -> String-swType s = smtType (sizeOf s)+swType s = smtType (kindOf s) swFunType :: [SW] -> SW -> String swFunType ss s = "(" ++ unwords (map swType ss) ++ ") " ++ swType s -smtType :: Size -> String-smtType (Size Nothing) = "Int"-smtType (Size (Just sz)) = "(_ BitVec " ++ show sz ++ ")"+smtType :: Kind -> String+smtType (KBounded _ sz) = "(_ BitVec " ++ show sz ++ ")"+smtType KUnbounded = "Int"+smtType KReal = "Real" cvtType :: SBVType -> String cvtType (SBVType []) = error "SBV.SMT.SMTLib2.cvtType: internal: received an empty type!" cvtType (SBVType xs) = "(" ++ unwords (map smtType body) ++ ") " ++ smtType ret- where szs = map snd xs- (body, ret) = (init szs, last szs)+ where (body, ret) = (init xs, last xs) type SkolemMap = M.Map SW [SW] type TableMap = IM.IntMap String@@ -235,16 +240,19 @@ where pad n s = replicate (n - length s) '0' ++ s cvtCW :: CW -> String-cvtCW x | isInfPrec x = if w >= 0 then show w else "(- " ++ show (abs w) ++ ")"- where w = cwVal x-cvtCW x | not (hasSign x) = hex (intSizeOf x) (cwVal x)+cvtCW x | isReal x = algRealToSMTLib2 w+ where Left w = cwVal x+cvtCW x | not (isBounded x) = if w >= 0 then show w else "(- " ++ show (abs w) ++ ")"+ where Right w = cwVal x+cvtCW x | not (hasSign x) = hex (intSizeOf x) w+ where Right w = cwVal x -- signed numbers (with 2's complement representation) is problematic -- since there's no way to put a bvneg over a positive number to get minBound.. -- Hence, we punt and use binary notation in that particular case-cvtCW x | cwVal x == least = mkMinBound (intSizeOf x)+cvtCW x | cwVal x == Right least = mkMinBound (intSizeOf x) where least = negate (2 ^ intSizeOf x) cvtCW x = negIf (w < 0) $ hex (intSizeOf x) (abs w)- where w = cwVal x+ where Right w = cwVal x negIf :: Bool -> String -> String negIf True a = "(bvneg " ++ a ++ ")"@@ -260,38 +268,39 @@ | Just tn <- i `IM.lookup` m = tn | True = error $ "SBV.SMTLib2: Cannot locate table " ++ show i -unbounded :: SBVExpr -> a-unbounded expr = error $ "SBV.SMTLib2: Unsupported operation on unbounded integers: " ++ show expr- cvtExp :: SkolemMap -> TableMap -> SBVExpr -> String cvtExp skolemMap tableMap expr@(SBVApp _ arguments) = sh expr where ssw = cvtSW skolemMap- hasInfPrecArgs = any isInfPrec arguments- ensureBV = not hasInfPrecArgs || unbounded expr+ bvOp = all isBounded arguments+ intOp = any isInteger arguments+ realOp = any isReal arguments+ bad | intOp = error $ "SBV.SMTLib2: Unsupported operation on unbounded integers: " ++ show expr+ | True = error $ "SBV.SMTLib2: Unsupported operation on real values: " ++ show expr+ ensureBV = bvOp || bad lift2 o _ [x, y] = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")" lift2 o _ sbvs = error $ "SBV.SMTLib2.sh.lift2: Unexpected arguments: " ++ show (o, sbvs) lift2B oU oS sgn sbvs = "(ite " ++ lift2S oU oS sgn sbvs ++ " #b1 #b0)"- lift2S oU oS sgn sbvs- | sgn- = lift2 oS sgn sbvs- | True- = lift2 oU sgn sbvs+ lift2S oU oS sgn = lift2 (if sgn then oS else oU) sgn lift2N o sgn sbvs = "(bvnot " ++ lift2 o sgn sbvs ++ ")" lift1 o _ [x] = "(" ++ o ++ " " ++ x ++ ")" lift1 o _ sbvs = error $ "SBV.SMT.SMTLib2.sh.lift1: Unexpected arguments: " ++ show (o, sbvs) sh (SBVApp Ite [a, b, c]) = "(ite (= #b1 " ++ ssw a ++ ") " ++ ssw b ++ " " ++ ssw c ++ ")"- sh (SBVApp (LkUp (t, (_, atSz), _, l) i e) [])+ sh (SBVApp (LkUp (t, aKnd, _, l) i e) []) | needsCheck = "(ite " ++ cond ++ ssw e ++ " " ++ lkUp ++ ")" | True = lkUp- where needsCheck = maybe True (\at -> (2::Integer)^at > fromIntegral l) (unSize atSz)+ where needsCheck = case aKnd of+ KBounded _ n -> (2::Integer)^n > fromIntegral l+ KUnbounded -> True+ KReal -> error "SBV.SMT.SMTLib2.cvtExp: unexpected real valued index" lkUp = "(" ++ getTable tableMap t ++ " " ++ ssw i ++ ")" cond | hasSign i = "(or " ++ le0 ++ " " ++ gtl ++ ") " | True = gtl ++ " "- (less, leq) = case atSz of- Size Nothing -> ("<", "<=")- _ -> if hasSign i then ("bvslt", "bvsle") else ("bvult", "bvule")- mkCnst = cvtCW . mkConstCW (hasSign i, sizeOf i)+ (less, leq) = case aKnd of+ KBounded{} -> if hasSign i then ("bvslt", "bvsle") else ("bvult", "bvule")+ KUnbounded -> ("<", "<=")+ KReal -> ("<", "<=")+ mkCnst = cvtCW . mkConstCW (kindOf i) le0 = "(" ++ less ++ " " ++ ssw i ++ " " ++ mkCnst 0 ++ ")" gtl = "(" ++ leq ++ " " ++ mkCnst l ++ " " ++ ssw i ++ ")" sh (SBVApp (ArrEq i j) []) = "(ite (= array_" ++ show i ++ " array_" ++ show j ++") #b1 #b0)"@@ -300,19 +309,23 @@ sh (SBVApp (Uninterpreted nm) args) = "(uninterpreted_" ++ nm ++ " " ++ unwords (map ssw args) ++ ")" sh (SBVApp (Extract i j) [a]) | ensureBV = "((_ extract " ++ show i ++ " " ++ show j ++ ") " ++ ssw a ++ ")" sh (SBVApp (Rol i) [a])- | not hasInfPrecArgs = rot ssw "rotate_left" i a- | True = sh (SBVApp (Shl i) [a]) -- Haskell treats rotateL as shiftL for unbounded values+ | bvOp = rot ssw "rotate_left" i a+ | intOp = sh (SBVApp (Shl i) [a]) -- Haskell treats rotateL as shiftL for unbounded values+ | True = bad sh (SBVApp (Ror i) [a])- | not hasInfPrecArgs = rot ssw "rotate_right" i a- | True = sh (SBVApp (Shr i) [a]) -- Haskell treats rotateR as shiftR for unbounded values+ | bvOp = rot ssw "rotate_right" i a+ | intOp = sh (SBVApp (Shr i) [a]) -- Haskell treats rotateR as shiftR for unbounded values+ | True = bad sh (SBVApp (Shl i) [a])- | not hasInfPrecArgs = shft ssw "bvshl" "bvshl" i a- | i < 0 = sh (SBVApp (Shr (-i)) [a]) -- flip sign/direction- | True = "(* " ++ ssw a ++ " " ++ show (bit i :: Integer) ++ ")" -- Implement shiftL by multiplication by 2^i+ | bvOp = shft ssw "bvshl" "bvshl" i a+ | i < 0 = sh (SBVApp (Shr (-i)) [a]) -- flip sign/direction+ | intOp = "(* " ++ ssw a ++ " " ++ show (bit i :: Integer) ++ ")" -- Implement shiftL by multiplication by 2^i+ | True = bad sh (SBVApp (Shr i) [a])- | not hasInfPrecArgs = shft ssw "bvlshr" "bvashr" i a- | i < 0 = sh (SBVApp (Shl (-i)) [a]) -- flip sign/direction- | True = "(div " ++ ssw a ++ " " ++ show (bit i :: Integer) ++ ")" -- Implement shiftR by division by 2^i+ | bvOp = shft ssw "bvlshr" "bvashr" i a+ | i < 0 = sh (SBVApp (Shl (-i)) [a]) -- flip sign/direction+ | intOp = "(div " ++ ssw a ++ " " ++ show (bit i :: Integer) ++ ")" -- Implement shiftR by division by 2^i+ | True = bad sh (SBVApp op args) | Just f <- lookup op smtBVOpTable, ensureBV = f (any hasSign args) (map ssw args)@@ -326,12 +339,12 @@ , (Join, lift2 "concat") ] sh inp@(SBVApp op args)- | hasInfPrecArgs- = case lookup op smtOpIntTable of- Just f -> f True (map ssw args)- _ -> unbounded inp- | Just f <- lookup op smtOpBVTable+ | intOp, Just f <- lookup op smtOpIntTable+ = f True (map ssw args)+ | bvOp, Just f <- lookup op smtOpBVTable = f (any hasSign args) (map ssw args)+ | realOp, Just f <- lookup op smtOpRealTable+ = f (any hasSign args) (map ssw args) | True = error $ "SBV.SMT.SMTLib2.cvtExp.sh: impossible happened; can't translate: " ++ show inp where smtOpBVTable = [ (Plus, lift2 "bvadd")@@ -346,18 +359,23 @@ , (LessEq, lift2B "bvule" "bvsle") , (GreaterEq, lift2B "bvuge" "bvsge") ]- smtOpIntTable = [ (Plus, lift2 "+")- , (Minus, lift2 "-")- , (Times, lift2 "*")- , (Quot, lift2 "div")- , (Rem, lift2 "mod")- , (Equal, lift2B "=" "=")- , (NotEqual, lift2B "distinct" "distinct")- , (LessThan, lift2B "<" "<")- , (GreaterThan, lift2B ">" ">")- , (LessEq, lift2B "<=" "<=")- , (GreaterEq, lift2B ">=" ">=")- ]+ smtOpRealTable = smtIntRealShared+ ++ [ (Quot, lift2 "/")+ ]+ smtOpIntTable = smtIntRealShared+ ++ [ (Quot, lift2 "div")+ , (Rem, lift2 "mod")+ ]+ smtIntRealShared = [ (Plus, lift2 "+")+ , (Minus, lift2 "-")+ , (Times, lift2 "*")+ , (Equal, lift2B "=" "=")+ , (NotEqual, lift2B "distinct" "distinct")+ , (LessThan, lift2B "<" "<")+ , (GreaterThan, lift2B ">" ">")+ , (LessEq, lift2B "<=" "<=")+ , (GreaterEq, lift2B ">=" ">=")+ ] rot :: (SW -> String) -> String -> Int -> SW -> String rot ssw o c x = "((_ " ++ o ++ " " ++ show c ++ ") " ++ ssw x ++ ")"@@ -365,5 +383,5 @@ shft :: (SW -> String) -> String -> String -> Int -> SW -> String shft ssw oW oS c x = "(" ++ o ++ " " ++ ssw x ++ " " ++ cvtCW c' ++ ")" where s = hasSign x- c' = mkConstCW (s, sizeOf x) c- o = if hasSign x then oS else oW+ c' = mkConstCW (kindOf x) c+ o = if s then oS else oW
Data/SBV/Tools/ExpectedValue.hs view
@@ -42,10 +42,12 @@ runOnce g = do (_, Result _ _ _ _ cs _ _ _ _ _ cstrs os) <- runSymbolic' (Concrete g) (m >>= output) let cval o = case o `lookup` cs of Nothing -> error "SBV.expectedValue: Cannot compute expected-values in the presence of uninterpreted constants!"- Just cw -> case (cwSigned cw, cwSize cw) of- (True, Size Nothing ) -> error "Cannot compute expected-values for unbounded integer results."- (False, Size (Just 1)) -> if cwToBool cw then 1 else 0- _ -> cwVal cw+ Just cw -> case (cwKind cw, cwVal cw) of+ (KBounded False 1, _) -> if cwToBool cw then 1 else 0+ (KBounded{}, Right v) -> v+ (KUnbounded, Right v) -> v+ (KReal, _) -> error "Cannot compute expected-values for real valued results."+ _ -> error $ "SBV.expectedValueWith: Unexpected CW: " ++ show cw if all ((== 1) . cval) cstrs then return $ map cval os else runOnce g -- constraint not satisfied try again with the same set of constraints
Data/SBV/Tools/GenTest.hs view
@@ -14,10 +14,12 @@ import Data.Bits (testBit) import Data.Char (isAlpha, toUpper)-import Data.Maybe (fromMaybe)+import Data.Function (on) import Data.List (intercalate, groupBy)+import Data.Maybe (fromMaybe) import System.Random +import Data.SBV.BitVectors.AlgReals import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.PrettyNum @@ -79,19 +81,28 @@ | needsInt && needsWord = ["import Data.Int", "import Data.Word", ""] | needsInt = ["import Data.Int", ""] | needsWord = ["import Data.Word", ""]+ | needsRatio = ["import Data.Ratio"] | True = [] where ((is, os):_) = vs params = is ++ os needsInt = any isSW params needsWord = any isUW params- isSW cw = cwSigned cw && cwSize cw /= Size Nothing && cwSize cw /= Size (Just 1)- isUW cw = not (cwSigned cw) && cwSize cw /= Size Nothing && cwSize cw /= Size (Just 1)+ needsRatio = any isR params+ isR cw = case kindOf cw of+ KReal -> True+ _ -> False+ isSW cw = case kindOf cw of+ KBounded True _ -> True+ _ -> False+ isUW cw = case kindOf cw of+ KBounded False sz -> sz > 1+ _ -> False modName = let (f:r) = n in toUpper f : r pad = replicate (length n + 3) ' ' getType [] = "[a]" getType ((i, o):_) = "[(" ++ mapType typeOf i ++ ", " ++ mapType typeOf o ++ ")]" mkLine (i, o) = "(" ++ mapType valOf i ++ ", " ++ mapType valOf o ++ ")"- mapType f cws = mkTuple $ map f $ groupBy (\c1 c2 -> (cwSigned c1, cwSize c1) == (cwSigned c2, cwSize c2)) cws+ mapType f cws = mkTuple $ map f $ groupBy ((==) `on` kindOf) cws mkTuple [x] = x mkTuple xs = "(" ++ intercalate ", " xs ++ ")" typeOf [] = "()"@@ -100,22 +111,24 @@ valOf [] = "()" valOf [x] = s x valOf xs = "[" ++ intercalate ", " (map s xs) ++ "]"- t cw = case (cwSigned cw, cwSize cw) of- (False, Size (Just 1)) -> "Bool"- (False, Size (Just 8)) -> "Word8"- (False, Size (Just 16)) -> "Word16"- (False, Size (Just 32)) -> "Word32"- (False, Size (Just 64)) -> "Word64"- (True, Size (Just 8)) -> "Int8"- (True, Size (Just 16)) -> "Int16"- (True, Size (Just 32)) -> "Int32"- (True, Size (Just 64)) -> "Int64"- (True, Size Nothing) -> "Integer"- _ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw- s cw = case (cwSigned cw, cwSize cw) of- (False, Size (Just 1)) -> take 5 (show (cwToBool cw) ++ repeat ' ')- (sgn, Size (Just sz)) -> shex False True (sgn, sz) (cwVal cw)- (_, Size Nothing) -> shexI False True (cwVal cw)+ t cw = case kindOf cw of+ KBounded False 1 -> "Bool"+ KBounded False 8 -> "Word8"+ KBounded False 16 -> "Word16"+ KBounded False 32 -> "Word32"+ KBounded False 64 -> "Word64"+ KBounded True 8 -> "Int8"+ KBounded True 16 -> "Int16"+ KBounded True 32 -> "Int32"+ KBounded True 64 -> "Int64"+ KUnbounded -> "Integer"+ KReal -> error $ "SBV.renderTest: Unsupported real valued test value: " ++ show cw+ _ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw+ s cw = case cwKind cw of+ KBounded False 1 -> take 5 (show (cwToBool cw) ++ repeat ' ')+ KBounded sgn sz -> let Right w = cwVal cw in shex False True (sgn, sz) w+ KUnbounded -> let Right w = cwVal cw in shexI False True w+ KReal -> let Left w = cwVal cw in algRealToHaskell w c :: String -> [([CW], [CW])] -> String c n vs = intercalate "\n" $@@ -172,23 +185,25 @@ , "}" ] where mkField p cw i = " " ++ t ++ " " ++ p ++ show i ++ ";"- where t = case (cwSigned cw, cwSize cw) of- (False, Size (Just 1)) -> "SBool"- (False, Size (Just 8)) -> "SWord8"- (False, Size (Just 16)) -> "SWord16"- (False, Size (Just 32)) -> "SWord32"- (False, Size (Just 64)) -> "SWord64"- (True, Size (Just 8)) -> "SInt8"- (True, Size (Just 16)) -> "SInt16"- (True, Size (Just 32)) -> "SInt32"- (True, Size (Just 64)) -> "SInt64"- (True, Size Nothing) -> error "SBV.rendertest: Unbounded integers are not supported when generating C test-cases."- _ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw+ where t = case cwKind cw of+ KBounded False 1 -> "SBool"+ KBounded False 8 -> "SWord8"+ KBounded False 16 -> "SWord16"+ KBounded False 32 -> "SWord32"+ KBounded False 64 -> "SWord64"+ KBounded True 8 -> "SInt8"+ KBounded True 16 -> "SInt16"+ KBounded True 32 -> "SInt32"+ KBounded True 64 -> "SInt64"+ KUnbounded -> error "SBV.renderTest: Unbounded integers are not supported when generating C test-cases."+ KReal -> error "SBV.renderTest: Real values are not supported when generating C test-cases."+ _ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw mkLine (is, os) = "{{" ++ intercalate ", " (map v is) ++ "}, {" ++ intercalate ", " (map v os) ++ "}}"- v cw = case (cwSigned cw, cwSize cw) of- (False, Size (Just 1)) -> if cwToBool cw then "true " else "false"- (sgn, Size (Just sz)) -> shex False True (sgn, sz) (cwVal cw)- (_, Size Nothing) -> shexI False True (cwVal cw)+ v cw = case cwKind cw of+ KBounded False 1 -> if cwToBool cw then "true " else "false"+ KBounded sgn sz -> let Right w = cwVal cw in shex False True (sgn, sz) w+ KUnbounded -> let Right w = cwVal cw in shexI False True w+ KReal -> error "SBV.renderTest: Real values are not supported when generating C test-cases." outLine | null vs = "printf(\"\");" | True = "printf(\"%*d. " ++ fmtString ++ "\\n\", " ++ show (length (show (length vs - 1))) ++ ", i"@@ -197,22 +212,23 @@ where (is, os) = head vs inp cw i = mkBool cw (n ++ "[i].input.i" ++ show i) out cw i = mkBool cw (n ++ "[i].output.o" ++ show i)- mkBool cw s = case (cwSigned cw, cwSize cw) of- (False, Size (Just 1)) -> "(" ++ s ++ " == true) ? \"true \" : \"false\""- _ -> s+ mkBool cw s = case cwKind cw of+ KBounded False 1 -> "(" ++ s ++ " == true) ? \"true \" : \"false\""+ _ -> s fmtString = unwords (map fmt is) ++ " -> " ++ unwords (map fmt os)- fmt cw = case (cwSigned cw, cwSize cw) of- (False, Size (Just 1)) -> "%s"- (False, Size (Just 8)) -> "0x%02\"PRIx8\""- (False, Size (Just 16)) -> "0x%04\"PRIx16\"U"- (False, Size (Just 32)) -> "0x%08\"PRIx32\"UL"- (False, Size (Just 64)) -> "0x%016\"PRIx64\"ULL"- (True, Size (Just 8)) -> "%\"PRId8\""- (True, Size (Just 16)) -> "%\"PRId16\""- (True, Size (Just 32)) -> "%\"PRId32\"L"- (True, Size (Just 64)) -> "%\"PRId64\"LL"- (True, Size Nothing) -> error "SBV.rendertest: Unsupported unbounded integers for C generation."- _ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw+ fmt cw = case cwKind cw of+ KBounded False 1 -> "%s"+ KBounded False 8 -> "0x%02\"PRIx8\""+ KBounded False 16 -> "0x%04\"PRIx16\"U"+ KBounded False 32 -> "0x%08\"PRIx32\"UL"+ KBounded False 64 -> "0x%016\"PRIx64\"ULL"+ KBounded True 8 -> "%\"PRId8\""+ KBounded True 16 -> "%\"PRId16\""+ KBounded True 32 -> "%\"PRId32\"L"+ KBounded True 64 -> "%\"PRId64\"LL"+ KUnbounded -> error "SBV.renderTest: Unsupported unbounded integers for C generation."+ KReal -> error "SBV.renderTest: Unsupported real valued values for C generation."+ _ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw forte :: String -> Bool -> ([Int], [Int]) -> [([CW], [CW])] -> String forte vname bigEndian ss vs = intercalate "\n" $ [ "// Automatically generated by SBV. Do not edit!"@@ -230,19 +246,21 @@ | True = "rev (map (\\s. s == \"1\") (explode (string_tl r)))" toF True = '1' toF False = '0'- blast cw = case (cwSigned cw, cwSize cw) of- (False, Size (Just 1)) -> [toF (cwToBool cw)]- (False, Size (Just 8)) -> xlt 8 (cwVal cw)- (False, Size (Just 16)) -> xlt 16 (cwVal cw)- (False, Size (Just 32)) -> xlt 32 (cwVal cw)- (False, Size (Just 64)) -> xlt 64 (cwVal cw)- (True, Size (Just 8)) -> xlt 8 (cwVal cw)- (True, Size (Just 16)) -> xlt 16 (cwVal cw)- (True, Size (Just 32)) -> xlt 32 (cwVal cw)- (True, Size (Just 64)) -> xlt 64 (cwVal cw)- (True, Size Nothing) -> error "SBV.rendertest: Unbounded integers are not supported when generating Forte test-cases."- _ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw- xlt s v = [toF (testBit v i) | i <- [s-1, s-2 .. 0]]+ blast cw = case cwKind cw of+ KBounded False 1 -> [toF (cwToBool cw)]+ KBounded False 8 -> xlt 8 (cwVal cw)+ KBounded False 16 -> xlt 16 (cwVal cw)+ KBounded False 32 -> xlt 32 (cwVal cw)+ KBounded False 64 -> xlt 64 (cwVal cw)+ KBounded True 8 -> xlt 8 (cwVal cw)+ KBounded True 16 -> xlt 16 (cwVal cw)+ KBounded True 32 -> xlt 32 (cwVal cw)+ KBounded True 64 -> xlt 64 (cwVal cw)+ KReal -> error "SBV.renderTest: Real values are not supported when generating Forte test-cases."+ KUnbounded -> error "SBV.renderTest: Unbounded integers are not supported when generating Forte test-cases."+ _ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw+ xlt s (Right v) = [toF (testBit v i) | i <- [s-1, s-2 .. 0]]+ xlt _ (Left r) = error $ "SBV.renderTest.Forte: Unexpected real value: " ++ show r mkLine (i, o) = "(" ++ mkTuple (form (fst ss) (concatMap blast i)) ++ ", " ++ mkTuple (form (snd ss) (concatMap blast o)) ++ ")" mkTuple [] = "()" mkTuple [x] = x
Data/SBV/Tools/Polynomial.hs view
@@ -129,7 +129,9 @@ -- See the remarks for the 'pMult' function for this design choice polyMult :: (Bits a, SymWord a, FromBits (SBV a)) => (SBV a, SBV a, [Int]) -> SBV a polyMult (x, y, red)- | isInfPrec x+ | isReal x+ = error $ "SBV.polyMult: Received a real value: " ++ show x+ | not (isBounded x) = error $ "SBV.polyMult: Received infinite precision value: " ++ show x | True = fromBitsLE $ genericTake sz $ r ++ repeat false@@ -142,7 +144,9 @@ polyDivMod :: (Bits a, SymWord a, FromBits (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a) polyDivMod x y- | isInfPrec x+ | isReal x+ = error $ "SBV.polyDivMod: Received a real value: " ++ show x+ | not (isBounded x) = error $ "SBV.polyDivMod: Received infinite precision value: " ++ show x | True = ite (y .== 0) (0, x) (adjust d, adjust r)@@ -231,7 +235,9 @@ -- 'Int' argument plays the same role as the one in the 'crcBV' function. crc :: (FromBits (SBV a), FromBits (SBV b), Bits a, Bits b, SymWord a, SymWord b) => Int -> SBV a -> SBV b -> SBV b crc n m p- | isInfPrec m || isInfPrec p+ | isReal m || isReal p+ = error $ "SBV.crc: Received a real value: " ++ show (m, p)+ | not (isBounded m) || not (isBounded p) = error $ "SBV.crc: Received an infinite precision value: " ++ show (m, p) | True = fromBitsBE $ replicate (sz - n) false ++ crcBV n (blastBE m) (blastBE p)
Data/SBV/Utils/Lib.hs view
@@ -12,23 +12,30 @@ module Data.SBV.Utils.Lib where +-- | Monadic lift over 2-tuples mlift2 :: Monad m => (a' -> b' -> r) -> (a -> m a') -> (b -> m b') -> (a, b) -> m r mlift2 k f g (a, b) = f a >>= \a' -> g b >>= \b' -> return $ k a' b' +-- | Monadic lift over 3-tuples mlift3 :: Monad m => (a' -> b' -> c' -> r) -> (a -> m a') -> (b -> m b') -> (c -> m c') -> (a, b, c) -> m r mlift3 k f g h (a, b, c) = f a >>= \a' -> g b >>= \b' -> h c >>= \c' -> return $ k a' b' c' +-- | Monadic lift over 4-tuples mlift4 :: Monad m => (a' -> b' -> c' -> d' -> r) -> (a -> m a') -> (b -> m b') -> (c -> m c') -> (d -> m d') -> (a, b, c, d) -> m r mlift4 k f g h i (a, b, c, d) = f a >>= \a' -> g b >>= \b' -> h c >>= \c' -> i d >>= \d' -> return $ k a' b' c' d' +-- | Monadic lift over 5-tuples mlift5 :: Monad m => (a' -> b' -> c' -> d' -> e' -> r) -> (a -> m a') -> (b -> m b') -> (c -> m c') -> (d -> m d') -> (e -> m e') -> (a, b, c, d, e) -> m r mlift5 k f g h i j (a, b, c, d, e) = f a >>= \a' -> g b >>= \b' -> h c >>= \c' -> i d >>= \d' -> j e >>= \e' -> return $ k a' b' c' d' e' +-- | Monadic lift over 6-tuples mlift6 :: Monad m => (a' -> b' -> c' -> d' -> e' -> f' -> r) -> (a -> m a') -> (b -> m b') -> (c -> m c') -> (d -> m d') -> (e -> m e') -> (f -> m f') -> (a, b, c, d, e, f) -> m r mlift6 k f g h i j l (a, b, c, d, e, y) = f a >>= \a' -> g b >>= \b' -> h c >>= \c' -> i d >>= \d' -> j e >>= \e' -> l y >>= \y' -> return $ k a' b' c' d' e' y' +-- | Monadic lift over 7-tuples mlift7 :: Monad m => (a' -> b' -> c' -> d' -> e' -> f' -> g' -> r) -> (a -> m a') -> (b -> m b') -> (c -> m c') -> (d -> m d') -> (e -> m e') -> (f -> m f') -> (g -> m g') -> (a, b, c, d, e, f, g) -> m r mlift7 k f g h i j l m (a, b, c, d, e, y, z) = f a >>= \a' -> g b >>= \b' -> h c >>= \c' -> i d >>= \d' -> j e >>= \e' -> l y >>= \y' -> m z >>= \z' -> return $ k a' b' c' d' e' y' z' +-- | Monadic lift over 8-tuples mlift8 :: Monad m => (a' -> b' -> c' -> d' -> e' -> f' -> g' -> h' -> r) -> (a -> m a') -> (b -> m b') -> (c -> m c') -> (d -> m d') -> (e -> m e') -> (f -> m f') -> (g -> m g') -> (h -> m h') -> (a, b, c, d, e, f, g, h) -> m r mlift8 k f g h i j l m n (a, b, c, d, e, y, z, w) = f a >>= \a' -> g b >>= \b' -> h c >>= \c' -> i d >>= \d' -> j e >>= \e' -> l y >>= \y' -> m z >>= \z' -> n w >>= \w' -> return $ k a' b' c' d' e' y' z' w'
README view
@@ -1,8 +1,7 @@-SBV: Symbolic Bit Vectors in Haskell-====================================+SBV: SMT Based Verification+============================ -Express properties about bit-precise Haskell programs and automatically prove-them using SMT solvers.+Express properties about Haskell programs and automatically prove them using SMT solvers. ```haskell $ ghci -XScopedTypeVariables@@ -44,6 +43,7 @@ - `SWord8`, `SWord16`, `SWord32`, `SWord64`: Symbolic Words (unsigned) - `SInt8`, `SInt16`, `SInt32`, `SInt64`: Symbolic Ints (signed) - `SInteger`: Symbolic unbounded integers (signed)+ - `SReal`: Symbolic infinite precision algebraic reals (signed) - Arrays of symbolic values - Symbolic polynomials over GF(2^n ), polynomial arithmetic, and CRCs - Uninterpreted constants and functions over symbolic values, with user@@ -129,5 +129,5 @@ Thanks ====== The following people reported bugs, provided comments/feedback, or contributed to the development of SBV in various ways:-Ian Blumenfeld, Ian Calvert, Iavor Diatchki, Tom Hawkins, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson,+Ian Blumenfeld, Ian Calvert, Iavor Diatchki, John Erickson, Tom Hawkins, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson, and Nis Wegmann.
RELEASENOTES view
@@ -1,10 +1,65 @@ Hackage: <http://hackage.haskell.org/package/sbv> GitHub: <http://github.com/LeventErkok/sbv> -Latest Hackage released version: 1.3+Latest Hackage released version: 1.4 -Version 1.3, 2012-02-25 ======================================================================+Version 1.4, 2012-05-10+ + The major change in this release is the support for symbolic algebraic reals: SReal.+ See http://en.wikipedia.org/wiki/Algebraic_number for details. In brief, algebraic+ reals are solutions to univariate polynomials with rational coefficients. The arithmetic+ on algebraic reals is precise, with no approximation errors. Note that algebraic reals+ are a proper subset of all reals, in particular transcendental numbers are not+ representable in this way. (For instance, "sqrt 2" is algebraic, but pi, e are not.)+ However, algebraic reals is a superset of rationals, so SBV now also supports symbolic+ rationals as well.+ + You *should* use Z3 v4.0 when working with real numbers. While the interface will+ work with older versions of Z3 (or other SMT solvers in general), it uses Z3's+ root-obj construct to retrieve and query algebraic reals.++ While SReal values have infinite precision, printing such values is not trivial since+ we might need an infinite number of digits if the result happens to be irrational. The+ user controls printing precision, by specifying how many digits after the decimal point+ should be printed. The default number of decimal digits to print is 10. (See the+ 'printRealPrec' field of SMT-solver configuration.)++ The acronym SBV used to stand for Symbolic Bit Vectors. However, SBV has grown beyond+ bit-vectors, especially with the addition of support for SInteger and SReal types and+ other code-generation utilities. Therefore, "SMT Based Verification" is now a better fit+ for the expansion of the acronym SBV.++ Other notable changes in the library:+ * Add functions s[TYPE] and s[TYPE]s for each symbolic type we support (i.e.,+ sBool, sBools, sWord8, sWord8s, etc.), to create symbolic variables of the+ right kind. Strictly speaking these are just synonyms for 'free'+ and 'mapM free' (plural versions), so they aren't adding any additional+ power. Except, they are specialized at their respective types, and might be+ easier to remember.+ * Add function solve, which is merely a synonym for (return . bAnd), but+ it simplifies expressing problems.+ * Add class SNum, which simplifies writing polymorphic code over symbolic values+ * Increase haddock coverage metrics+ * Major code refactoring around symbolic kinds+ * SMTLib2: Emit ":produce-models" call before setting the logic, as required+ by the SMT-Lib2 standard. [Patch provided by arrowdodger on github, thanks!]++ Bugs fixed:+ * [Performance] Use a much simpler default definition for "select": While the+ older version (based on binary search on the bits of the indexer) was correct,+ it created unnecessarily big expressions. Since SBV does not have a notion+ of concrete subwords, the binary-search trick was not bringing any advantage+ in any case. Instead, we now simply use a linear walk over the elements.++ Examples:+ * Change dog-cat-mouse example to use SInteger for the counts+ * Add merge-sort example: Data.SBV.Examples.BitPrecise.MergeSort+ * Add diophantine solver example: Data.SBV.Examples.Existentials.Diophantine++======================================================================+Version 1.3, 2012-02-25+ * Workaround cabal/hackage issue, functionally the same as release 1.2 below
SBVUnitTest/GoldFiles/dogCatMouse.gold view
@@ -1,5 +1,5 @@ Solution #1:- d = 3 :: SWord16- c = 41 :: SWord16- m = 56 :: SWord16+ dog = 3 :: SInteger+ cat = 41 :: SInteger+ mouse = 56 :: SInteger This is the only solution.
+ SBVUnitTest/GoldFiles/merge.gold view
@@ -0,0 +1,152 @@+== BEGIN: "Makefile" ================+# Makefile for merge. Automatically generated by SBV. Do not edit!++# include any user-defined .mk file in the current directory.+-include *.mk++CC=gcc+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer++all: merge_driver++merge.o: merge.c merge.h+ ${CC} ${CCFLAGS} -c $< -o $@++merge_driver.o: merge_driver.c+ ${CC} ${CCFLAGS} -c $< -o $@++merge_driver: merge.o merge_driver.o+ ${CC} ${CCFLAGS} $^ -o $@++clean:+ rm -f *.o++veryclean: clean+ rm -f merge_driver+== END: "Makefile" ==================+== BEGIN: "merge.h" ================+/* Header file for merge. Automatically generated by SBV. Do not edit! */++#ifndef __merge__HEADER_INCLUDED__+#define __merge__HEADER_INCLUDED__++#include <inttypes.h>+#include <stdint.h>+#include <stdbool.h>++/* The boolean type */+typedef bool SBool;++/* Unsigned bit-vectors */+typedef uint8_t SWord8 ;+typedef uint16_t SWord16;+typedef uint32_t SWord32;+typedef uint64_t SWord64;++/* Signed bit-vectors */+typedef int8_t SInt8 ;+typedef int16_t SInt16;+typedef int32_t SInt32;+typedef int64_t SInt64;++/* Entry point prototype: */+void merge(const SWord8 *xs, SWord8 *ys);++#endif /* __merge__HEADER_INCLUDED__ */+== END: "merge.h" ==================+== BEGIN: "merge_driver.c" ================+/* Example driver program for merge. */+/* Automatically generated by SBV. Edit as you see fit! */++#include <inttypes.h>+#include <stdint.h>+#include <stdbool.h>+#include <stdio.h>+#include "merge.h"++int main(void)+{+ const SWord8 xs[5] = {+ 10, 6, 4, 82, 71+ };++ printf("Contents of input array xs:\n");+ int xs_ctr;+ for(xs_ctr = 0; xs_ctr < 5 ; ++xs_ctr)+ printf(" xs[%d] = %"PRIu8"\n", xs_ctr ,xs[xs_ctr]);++ SWord8 ys[5];++ merge(xs, ys);++ printf("merge(xs, ys) ->\n");+ int ys_ctr;+ for(ys_ctr = 0; ys_ctr < 5 ; ++ys_ctr)+ printf(" ys[%d] = %"PRIu8"\n", ys_ctr ,ys[ys_ctr]);++ return 0;+}+== END: "merge_driver.c" ==================+== BEGIN: "merge.c" ================+/* File: "merge.c". Automatically generated by SBV. Do not edit! */++#include <inttypes.h>+#include <stdint.h>+#include <stdbool.h>+#include "merge.h"++void merge(const SWord8 *xs, SWord8 *ys)+{+ const SWord8 s0 = xs[0];+ const SWord8 s1 = xs[1];+ const SWord8 s2 = xs[2];+ const SWord8 s3 = xs[3];+ const SWord8 s4 = xs[4];+ const SBool s5 = s0 < s1;+ const SWord8 s6 = s5 ? s0 : s1;+ const SBool s7 = s3 < s4;+ const SWord8 s8 = s7 ? s3 : s4;+ const SBool s9 = s2 < s8;+ const SWord8 s10 = s9 ? s2 : s8;+ const SBool s11 = s6 < s10;+ const SWord8 s12 = s11 ? s6 : s10;+ const SWord8 s13 = s5 ? s1 : s0;+ const SBool s14 = s13 < s10;+ const SWord8 s15 = s14 ? s13 : s10;+ const SWord8 s16 = s7 ? s4 : s3;+ const SBool s17 = s2 < s16;+ const SWord8 s18 = s17 ? s2 : s16;+ const SWord8 s19 = s9 ? s8 : s18;+ const SBool s20 = s6 < s19;+ const SWord8 s21 = s20 ? s6 : s19;+ const SWord8 s22 = s11 ? s15 : s21;+ const SBool s23 = s13 < s19;+ const SWord8 s24 = s23 ? s13 : s19;+ const SWord8 s25 = s14 ? s10 : s24;+ const SWord8 s26 = s17 ? s16 : s2;+ const SWord8 s27 = s9 ? s16 : s26;+ const SBool s28 = s6 < s27;+ const SWord8 s29 = s28 ? s6 : s27;+ const SWord8 s30 = s20 ? s24 : s29;+ const SWord8 s31 = s11 ? s25 : s30;+ const SBool s32 = s13 < s27;+ const SWord8 s33 = s32 ? s13 : s27;+ const SWord8 s34 = s23 ? s19 : s33;+ const SWord8 s35 = s14 ? s19 : s34;+ const SWord8 s36 = s28 ? s33 : s6;+ const SWord8 s37 = s20 ? s34 : s36;+ const SWord8 s38 = s11 ? s35 : s37;+ const SWord8 s39 = s32 ? s27 : s13;+ const SWord8 s40 = s23 ? s27 : s39;+ const SWord8 s41 = s14 ? s27 : s40;+ const SWord8 s42 = s28 ? s39 : s13;+ const SWord8 s43 = s20 ? s40 : s42;+ const SWord8 s44 = s11 ? s41 : s43;++ ys[0] = s12;+ ys[1] = s22;+ ys[2] = s31;+ ys[3] = s38;+ ys[4] = s44;+}+== END: "merge.c" ==================
SBVUnitTest/SBVUnitTest.hs view
@@ -15,7 +15,7 @@ import Control.Monad (unless, when) import System.Directory (doesDirectoryExist) import System.Environment (getArgs)-import System.Exit (exitWith, ExitCode(..))+import System.Exit (exitWith, exitSuccess, ExitCode(..)) import System.FilePath ((</>)) import Test.HUnit (Test(..), Counts(..), runTestTT) @@ -35,7 +35,8 @@ import qualified TestSuite.Basics.QRem as T02_06(testSuite) import qualified TestSuite.BitPrecise.BitTricks as T03_01(testSuite) import qualified TestSuite.BitPrecise.Legato as T03_02(testSuite)-import qualified TestSuite.BitPrecise.PrefixSum as T03_03(testSuite)+import qualified TestSuite.BitPrecise.MergeSort as T03_03(testSuite)+import qualified TestSuite.BitPrecise.PrefixSum as T03_04(testSuite) import qualified TestSuite.CRC.CCITT as T04_01(testSuite) import qualified TestSuite.CRC.CCITT_Unidir as T04_02(testSuite) import qualified TestSuite.CRC.GenPoly as T04_03(testSuite)@@ -77,7 +78,8 @@ , ("qrem", T02_06.testSuite) , ("bitTricks", T03_01.testSuite) , ("legato", T03_02.testSuite)- , ("prefixSum", T03_03.testSuite)+ , ("mergeSort", T03_03.testSuite)+ , ("prefixSum", T03_04.testSuite) , ("ccitt", T04_01.testSuite) , ("ccitt2", T04_02.testSuite) , ("genPoly", T04_03.testSuite)@@ -163,5 +165,5 @@ then do if shouldCreate then putStrLn $ "All " ++ show c ++ " test cases executed in gold-file generation mode." else putStrLn $ "All " ++ show c ++ " test cases successfully passed."- exitWith ExitSuccess+ exitSuccess else exitWith $ ExitFailure 2
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String-buildTime = "Sat Feb 25 12:36:27 PST 2012"+buildTime = "Wed May 9 22:17:47 PDT 2012"
SBVUnitTest/TestSuite/Basics/Arithmetic.hs view
@@ -10,7 +10,8 @@ -- Test suite for basic concrete arithmetic ----------------------------------------------------------------------------- -{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE TupleSections #-} module TestSuite.Basics.Arithmetic(testSuite) where @@ -21,7 +22,8 @@ -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test $- genBinTest "+" (+)+ genReals+ ++ genBinTest "+" (+) ++ genBinTest "-" (-) ++ genBinTest "*" (*) ++ genUnTest "negate" negate@@ -29,6 +31,12 @@ ++ genUnTest "signum" signum ++ genBinTest ".&." (.&.) ++ genBinTest ".|." (.|.)+ ++ genBoolTest "<" (<) (.<)+ ++ genBoolTest "<=" (<=) (.<=)+ ++ genBoolTest ">" (>) (.>)+ ++ genBoolTest ">=" (>=) (.>=)+ ++ genBoolTest "==" (==) (.==)+ ++ genBoolTest "/=" (/=) (./=) ++ genBinTest "xor" xor ++ genUnTest "complement" complement ++ genIntTest "shift" shift@@ -59,6 +67,20 @@ where pair (x, y, a) b = (x, y, show (fromIntegral a `asTypeOf` b) == show b) mkTest (x, y, s) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: s `showsAs` "True" +genBoolTest :: String -> (forall a. Ord a => a -> a -> Bool) -> (forall a. OrdSymbolic a => a -> a -> SBool) -> [Test]+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]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- w16s, y <- w16s] [x `opS` y | x <- sw16s, y <- sw16s]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- w32s, y <- w32s] [x `opS` y | x <- sw32s, y <- sw32s]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- w64s, y <- w64s] [x `opS` y | x <- sw64s, y <- sw64s]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- i8s, y <- i8s ] [x `opS` y | x <- si8s, y <- si8s]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- i16s, y <- i16s] [x `opS` y | x <- si16s, y <- si16s]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- i32s, y <- i32s] [x `opS` y | x <- si32s, y <- si32s]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- i64s, y <- i64s] [x `opS` y | x <- si64s, y <- si64s]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- iUBs, y <- iUBs] [x `opS` y | x <- siUBs, y <- siUBs]+ where pair (x, y, a) b = (x, y, Just a == unliteral b)+ mkTest (x, y, s) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: s `showsAs` "True"+ genUnTest :: String -> (forall a. Bits a => a -> a) -> [Test] genUnTest nm op = map mkTest $ zipWith pair [(show x, op x) | x <- w8s ] [op x | x <- sw8s ]@@ -144,6 +166,21 @@ ++ [(show x, unsignCast x .== fromBitsLE (blastLE x)) | x <- si64s] where mkTest (x, r) = "cast-" ++ show x ~: r `showsAs` "True" +genReals :: [Test]+genReals = map mkTest $+ map ("+",) (zipWith pair [(show x, show y, x + y) | x <- rs, y <- rs ] [x + y | x <- srs, y <- srs ])+ ++ map ("-",) (zipWith pair [(show x, show y, x - y) | x <- rs, y <- rs ] [x - y | x <- srs, y <- srs ])+ ++ map ("*",) (zipWith pair [(show x, show y, x * y) | x <- rs, y <- rs ] [x * y | x <- srs, y <- srs ])+ ++ map ("<",) (zipWith pair [(show x, show y, x < y) | x <- rs, y <- rs ] [x .< y | x <- srs, y <- srs ])+ ++ map ("<=",) (zipWith pair [(show x, show y, x <= y) | x <- rs, y <- rs ] [x .<= y | x <- srs, y <- srs ])+ ++ map (">",) (zipWith pair [(show x, show y, x > y) | x <- rs, y <- rs ] [x .> y | x <- srs, y <- srs ])+ ++ map (">=",) (zipWith pair [(show x, show y, x >= y) | x <- rs, y <- rs ] [x .>= y | x <- srs, y <- srs ])+ ++ map ("==",) (zipWith pair [(show x, show y, x == y) | x <- rs, y <- rs ] [x .== y | x <- srs, y <- srs ])+ ++ map ("/=",) (zipWith pair [(show x, show y, x /= y) | x <- rs, y <- rs ] [x ./= y | x <- srs, y <- srs ])+ ++ map ("/",) (zipWith pair [(show x, show y, x / y) | x <- rs, y <- rs, y /= 0] [x / y | x <- srs, y <- srs, unliteral y /= Just 0])+ where pair (x, y, a) b = (x, y, Just a == unliteral b)+ mkTest (nm, (x, y, s)) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: s `showsAs` "True"+ -- Concrete test data xsSigned, xsUnsigned :: (Num a, Enum a, Bounded a) => [a] xsUnsigned = take 5 (iterate (1+) minBound) ++ take 5 (iterate (\x -> x-1) maxBound)@@ -202,3 +239,11 @@ siUBs :: [SInteger] siUBs = map literal iUBs++rs :: [AlgReal]+rs = [fromRational (i % d) | i <- is, d <- ds]+ where is = [-1000000 .. -999998] ++ [-2 .. 2] ++ [999998 .. 1000001]+ ds = [2 .. 5] ++ [98 .. 102] ++ [999998 .. 1000000]++srs :: [SReal]+srs = map literal rs
SBVUnitTest/TestSuite/Puzzles/DogCatMouse.hs view
@@ -13,7 +13,7 @@ module TestSuite.Puzzles.DogCatMouse(testSuite) where import Data.SBV-import Data.SBV.Examples.Puzzles.DogCatMouse+-- import Data.SBV.Examples.Puzzles.DogCatMouse -- everything defined here import SBVTest @@ -22,7 +22,10 @@ testSuite = mkTestSuite $ \goldCheck -> test [ "dog cat mouse" ~: allSat p `goldCheck` "dogCatMouse.gold" ]- where p = do d <- exists "d"- c <- exists "c"- m <- exists "m"- return $ puzzle d c m+ where p = do [dog, cat, mouse] <- sIntegers ["dog", "cat", "mouse"]+ solve [ dog .>= 1 -- at least one dog+ , cat .>= 1 -- at least one cat+ , mouse .>= 1 -- at least one mouse+ , dog + cat + mouse .== 100 -- buy precisely 100 animals+ , 1500 * dog + 100 * cat + 25 * mouse .== 10000 -- spend exactly 100 dollars (use cents since we don't have fractions)+ ]
SBVUnitTest/TestSuite/Puzzles/U2Bridge.hs view
@@ -24,9 +24,9 @@ , "U2Bridge-2" ~: assert $ (0 ==) `fmap` count 2 , "U2Bridge-3" ~: assert $ (0 ==) `fmap` count 3 , "U2Bridge-4" ~: assert $ (0 ==) `fmap` count 4- , "U2Bridge-5" ~: solve 5 `goldCheck` "U2Bridge.gold"+ , "U2Bridge-5" ~: slv 5 `goldCheck` "U2Bridge.gold" , "U2Bridge-6" ~: assert $ (0 ==) `fmap` count 6 ] where act = do b <- exists_; p1 <- exists_; p2 <- exists_; return (b, p1, p2) count n = numberOfModels $ isValid `fmap` mapM (const act) [1..(n::Int)]- solve n = sat $ isValid `fmap` mapM (const act) [1..(n::Int)]+ slv n = sat $ isValid `fmap` mapM (const act) [1..(n::Int)]
sbv.cabal view
@@ -1,11 +1,11 @@ Name: sbv-Version: 1.3+Version: 1.4 Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT-Synopsis: Symbolic bit vectors: Bit-precise verification and automatic C-code generation.-Description: Express properties about bit-precise Haskell programs and automatically prove- them using SMT solvers. Automatically generate C programs from Haskell functions.- The SBV library adds support for symbolic bit vectors, allowing formal models of- bit-precise programs to be created.+Synopsis: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.+Description: Express properties about Haskell programs and automatically prove them using SMT+ (Satisfiability Modulo Theories) solvers. Automatically generate C programs from+ Haskell functions. The SBV library adds support for symbolic bit vectors and other+ symbolic types, allowing formal models of Haskell programs to be created. . > $ ghci -XScopedTypeVariables > Prelude> :m Data.SBV@@ -25,6 +25,8 @@ . * 'SInteger': Symbolic unbounded integers (signed) .+ * 'SReal': Symbolic algebraic reals (signed)+ . * 'SArray', 'SFunArray': Flat arrays of symbolic values . * 'STree': Full binary trees of symbolic values (for fast symbolic access)@@ -64,8 +66,8 @@ bug reports, and patches are always welcome. . The following people reported bugs, provided comments/feedback, or contributed to the- development of SBV in various ways: Ian Blumenfeld, Ian Calvert, Iavor Diatchki,- Tom Hawkins, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson, and Nis Wegmann.+ development of SBV in various ways: Ian Blumenfeld, Ian Calvert, Iavor Diatchki, John+ Erickson, Tom Hawkins, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson, and Nis Wegmann. . Release notes can be seen at: <http://github.com/LeventErkok/sbv/blob/master/RELEASENOTES>. @@ -78,7 +80,7 @@ Bug-reports: http://github.com/LeventErkok/sbv/issues Maintainer: Levent Erkok (erkokl@gmail.com) Build-Type: Simple-Cabal-Version: >= 1.6+Cabal-Version: >= 1.8 Data-Files: SBVUnitTest/GoldFiles/*.gold Extra-Source-Files: INSTALL, README, COPYRIGHT, RELEASENOTES @@ -105,6 +107,7 @@ , Data.SBV.Internals , Data.SBV.Examples.BitPrecise.BitTricks , Data.SBV.Examples.BitPrecise.Legato+ , Data.SBV.Examples.BitPrecise.MergeSort , Data.SBV.Examples.BitPrecise.PrefixSum , Data.SBV.Examples.CodeGeneration.AddSub , Data.SBV.Examples.CodeGeneration.CRC_USB5@@ -115,6 +118,7 @@ , Data.SBV.Examples.Crypto.AES , Data.SBV.Examples.Crypto.RC4 , Data.SBV.Examples.Existentials.CRCPolynomial+ , Data.SBV.Examples.Existentials.Diophantine , Data.SBV.Examples.Polynomials.Polynomials , Data.SBV.Examples.Puzzles.Coins , Data.SBV.Examples.Puzzles.Counts@@ -126,7 +130,8 @@ , Data.SBV.Examples.Puzzles.U2Bridge , Data.SBV.Examples.Uninterpreted.AUF , Data.SBV.Examples.Uninterpreted.Function- Other-modules : Data.SBV.BitVectors.Data+ Other-modules : Data.SBV.BitVectors.AlgReals+ , Data.SBV.BitVectors.Data , Data.SBV.BitVectors.Model , Data.SBV.BitVectors.PrettyNum , Data.SBV.BitVectors.SignCast@@ -157,7 +162,8 @@ , HUnit >= 1.2.4.2 , filepath >= 1.1.0.4 , process >= 1.0.1.3- Hs-Source-Dirs : SBVUnitTest, .+ , sbv+ Hs-Source-Dirs : SBVUnitTest main-is : SBVUnitTest.hs Other-modules : SBVUnitTestBuildTime , SBVTest