diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -10,9 +10,9 @@ -- (The sbv library is hosted at . -- 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 +.) 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 +.) 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 diff --git a/Data/SBV/BitVectors/AlgReals.hs b/Data/SBV/BitVectors/AlgReals.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/BitVectors/AlgReals.hs @@ -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 diff --git a/Data/SBV/BitVectors/Data.hs b/Data/SBV/BitVectors/Data.hs --- a/Data/SBV/BitVectors/Data.hs +++ b/Data/SBV/BitVectors/Data.hs @@ -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 _)) = " :: SInteger" - show (SBV (sgn, Size (Just sz)) (Right _)) = " :: " ++ 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 _)) = " :: " ++ 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: +-- -- 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 diff --git a/Data/SBV/BitVectors/Model.hs b/Data/SBV/BitVectors/Model.hs --- a/Data/SBV/BitVectors/Model.hs +++ b/Data/SBV/BitVectors/Model.hs @@ -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) diff --git a/Data/SBV/BitVectors/PrettyNum.hs b/Data/SBV/BitVectors/PrettyNum.hs --- a/Data/SBV/BitVectors/PrettyNum.hs +++ b/Data/SBV/BitVectors/PrettyNum.hs @@ -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 diff --git a/Data/SBV/BitVectors/STree.hs b/Data/SBV/BitVectors/STree.hs --- a/Data/SBV/BitVectors/STree.hs +++ b/Data/SBV/BitVectors/STree.hs @@ -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 diff --git a/Data/SBV/BitVectors/SignCast.hs b/Data/SBV/BitVectors/SignCast.hs --- a/Data/SBV/BitVectors/SignCast.hs +++ b/Data/SBV/BitVectors/SignCast.hs @@ -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 diff --git a/Data/SBV/BitVectors/Splittable.hs b/Data/SBV/BitVectors/Splittable.hs --- a/Data/SBV/BitVectors/Splittable.hs +++ b/Data/SBV/BitVectors/Splittable.hs @@ -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 diff --git a/Data/SBV/Compilers/C.hs b/Data/SBV/Compilers/C.hs --- a/Data/SBV/Compilers/C.hs +++ b/Data/SBV/Compilers/C.hs @@ -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 diff --git a/Data/SBV/Compilers/CodeGen.hs b/Data/SBV/Compilers/CodeGen.hs --- a/Data/SBV/Compilers/CodeGen.hs +++ b/Data/SBV/Compilers/CodeGen.hs @@ -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 = "" diff --git a/Data/SBV/Examples/BitPrecise/MergeSort.hs b/Data/SBV/Examples/BitPrecise/MergeSort.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Examples/BitPrecise/MergeSort.hs @@ -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) diff --git a/Data/SBV/Examples/Existentials/Diophantine.hs b/Data/SBV/Examples/Existentials/Diophantine.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Examples/Existentials/Diophantine.hs @@ -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 diff --git a/Data/SBV/Examples/Puzzles/Counts.hs b/Data/SBV/Examples/Puzzles/Counts.hs --- a/Data/SBV/Examples/Puzzles/Counts.hs +++ b/Data/SBV/Examples/Puzzles/Counts.hs @@ -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" #-} diff --git a/Data/SBV/Examples/Puzzles/DogCatMouse.hs b/Data/SBV/Examples/Puzzles/DogCatMouse.hs --- a/Data/SBV/Examples/Puzzles/DogCatMouse.hs +++ b/Data/SBV/Examples/Puzzles/DogCatMouse.hs @@ -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) + ] diff --git a/Data/SBV/Examples/Puzzles/Euler185.hs b/Data/SBV/Examples/Puzzles/Euler185.hs --- a/Data/SBV/Examples/Puzzles/Euler185.hs +++ b/Data/SBV/Examples/Puzzles/Euler185.hs @@ -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]) diff --git a/Data/SBV/Examples/Puzzles/Sudoku.hs b/Data/SBV/Examples/Puzzles/Sudoku.hs --- a/Data/SBV/Examples/Puzzles/Sudoku.hs +++ b/Data/SBV/Examples/Puzzles/Sudoku.hs @@ -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] diff --git a/Data/SBV/Internals.hs b/Data/SBV/Internals.hs --- a/Data/SBV/Internals.hs +++ b/Data/SBV/Internals.hs @@ -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. --} diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs --- a/Data/SBV/Provers/Prover.hs +++ b/Data/SBV/Provers/Prover.hs @@ -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) diff --git a/Data/SBV/Provers/SExpr.hs b/Data/SBV/Provers/SExpr.hs --- a/Data/SBV/Provers/SExpr.hs +++ b/Data/SBV/Provers/SExpr.hs @@ -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 diff --git a/Data/SBV/Provers/Yices.hs b/Data/SBV/Provers/Yices.hs --- a/Data/SBV/Provers/Yices.hs +++ b/Data/SBV/Provers/Yices.hs @@ -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])] diff --git a/Data/SBV/Provers/Z3.hs b/Data/SBV/Provers/Z3.hs --- a/Data/SBV/Provers/Z3.hs +++ b/Data/SBV/Provers/Z3.hs @@ -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 _ = [] diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs --- a/Data/SBV/SMT/SMT.hs +++ b/Data/SBV/SMT/SMT.hs @@ -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 diff --git a/Data/SBV/SMT/SMTLib.hs b/Data/SBV/SMT/SMTLib.hs --- a/Data/SBV/SMT/SMTLib.hs +++ b/Data/SBV/SMT/SMTLib.hs @@ -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 diff --git a/Data/SBV/SMT/SMTLib1.hs b/Data/SBV/SMT/SMTLib1.hs --- a/Data/SBV/SMT/SMTLib1.hs +++ b/Data/SBV/SMT/SMTLib1.hs @@ -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" diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -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 diff --git a/Data/SBV/Tools/ExpectedValue.hs b/Data/SBV/Tools/ExpectedValue.hs --- a/Data/SBV/Tools/ExpectedValue.hs +++ b/Data/SBV/Tools/ExpectedValue.hs @@ -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 diff --git a/Data/SBV/Tools/GenTest.hs b/Data/SBV/Tools/GenTest.hs --- a/Data/SBV/Tools/GenTest.hs +++ b/Data/SBV/Tools/GenTest.hs @@ -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 diff --git a/Data/SBV/Tools/Polynomial.hs b/Data/SBV/Tools/Polynomial.hs --- a/Data/SBV/Tools/Polynomial.hs +++ b/Data/SBV/Tools/Polynomial.hs @@ -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) diff --git a/Data/SBV/Utils/Lib.hs b/Data/SBV/Utils/Lib.hs --- a/Data/SBV/Utils/Lib.hs +++ b/Data/SBV/Utils/Lib.hs @@ -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' diff --git a/README b/README --- a/README +++ b/README @@ -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. diff --git a/RELEASENOTES b/RELEASENOTES --- a/RELEASENOTES +++ b/RELEASENOTES @@ -1,10 +1,65 @@ Hackage: GitHub: -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 diff --git a/SBVUnitTest/GoldFiles/dogCatMouse.gold b/SBVUnitTest/GoldFiles/dogCatMouse.gold --- a/SBVUnitTest/GoldFiles/dogCatMouse.gold +++ b/SBVUnitTest/GoldFiles/dogCatMouse.gold @@ -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. diff --git a/SBVUnitTest/GoldFiles/merge.gold b/SBVUnitTest/GoldFiles/merge.gold new file mode 100644 --- /dev/null +++ b/SBVUnitTest/GoldFiles/merge.gold @@ -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 +#include +#include + +/* 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 +#include +#include +#include +#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 +#include +#include +#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" ================== diff --git a/SBVUnitTest/SBVUnitTest.hs b/SBVUnitTest/SBVUnitTest.hs --- a/SBVUnitTest/SBVUnitTest.hs +++ b/SBVUnitTest/SBVUnitTest.hs @@ -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 diff --git a/SBVUnitTest/SBVUnitTestBuildTime.hs b/SBVUnitTest/SBVUnitTestBuildTime.hs --- a/SBVUnitTest/SBVUnitTestBuildTime.hs +++ b/SBVUnitTest/SBVUnitTestBuildTime.hs @@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String -buildTime = "Sat Feb 25 12:36:27 PST 2012" +buildTime = "Wed May 9 22:17:47 PDT 2012" diff --git a/SBVUnitTest/TestSuite/Basics/Arithmetic.hs b/SBVUnitTest/TestSuite/Basics/Arithmetic.hs --- a/SBVUnitTest/TestSuite/Basics/Arithmetic.hs +++ b/SBVUnitTest/TestSuite/Basics/Arithmetic.hs @@ -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 diff --git a/SBVUnitTest/TestSuite/Puzzles/DogCatMouse.hs b/SBVUnitTest/TestSuite/Puzzles/DogCatMouse.hs --- a/SBVUnitTest/TestSuite/Puzzles/DogCatMouse.hs +++ b/SBVUnitTest/TestSuite/Puzzles/DogCatMouse.hs @@ -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) + ] diff --git a/SBVUnitTest/TestSuite/Puzzles/U2Bridge.hs b/SBVUnitTest/TestSuite/Puzzles/U2Bridge.hs --- a/SBVUnitTest/TestSuite/Puzzles/U2Bridge.hs +++ b/SBVUnitTest/TestSuite/Puzzles/U2Bridge.hs @@ -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)] diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -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: . @@ -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