packages feed

sbv 0.9.22 → 0.9.23

raw patch · 61 files changed

+1193/−527 lines, 61 files

Files

Data/SBV.hs view
@@ -101,6 +101,11 @@   , SWord8, SWord16, SWord32, SWord64   -- *** Signed symbolic bit-vectors   , SInt8, SInt16, SInt32, SInt64+  -- *** Signed unbounded integers+  -- $unboundedLimitations+  , SInteger+  -- *** Abstract SBV type+  , SBV   -- *** Arrays of symbolic values   , SymArray(..), SArray, SFunArray, mkSFunArray   -- *** Full binary trees@@ -151,6 +156,10 @@   -- ** Finding all satisfying assignments   , allSat, allSatWith, numberOfModels +  -- * Optimization+  -- $optimizeIntro+  , minimize, maximize, optimize+   -- * Model extraction   -- $modelExtraction @@ -188,7 +197,7 @@   , cgReturn, cgReturnArr    -- ** Code generation with uninterpreted functions-  , cgAddPrototype, cgAddDecl, cgAddLDFlags+  , cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIntegerSize    -- ** Compilation to C   , compileToC, compileToCLib@@ -203,6 +212,7 @@  import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.Model+import Data.SBV.BitVectors.Optimize import Data.SBV.BitVectors.PrettyNum import Data.SBV.BitVectors.Polynomial import Data.SBV.BitVectors.SignCast@@ -253,6 +263,30 @@ system where arbitrary SMT solvers can be used. -} +{- $optimizeIntro+Symbolic optimization. A call of the form:++    @minimize cost n valid@++returns @Just xs@, such that:++   * @xs@ has precisely @n@ elements++   * @valid xs@ holds++   * @cost xs@ is minimal. That is, for all sequences @ys@ that satisfy the first two criteria above, @cost xs .<= cost ys@ holds.++If there is no such sequence, then 'minimize' will return 'Nothing'.++The function 'maximize' is similar, except the comparator is '.>='. So the value returned has the largest cost (or value, in that case).++The function 'optimize' allows the user to give a custom comparison function.++Logically, the SBV optimization engine satisfies the following predicate:++   @exists xs. forall ys. valid xs && (valid ys ``implies`` (cost xs ``cmp`` cost ys))@+-}+ {- $modelExtraction The default 'Show' instances for prover calls provide all the counter-example information in a human-readable form and should be sufficient for most casual uses of sbv. However, tools built@@ -284,4 +318,23 @@ {- $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.+-}++{- $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,+some bit-vector based operations are /not/ supported for the 'SInteger' type while in the verification mode. That+is, you can use these operations on 'SInteger' values during normal programming/simulation.+but the SMT translation will not support these operations since there corresponding operations are not supported in SMT-Lib.+Note that this should rarely be a problem in practice, as these operations are mostly meaningful on fixed-size+bit-vectors. The operations that are restricted to bounded word/int sizes are:++   * Rotations and shifts: 'rotateL', 'rotateR', 'shiftL', 'shiftR'++   * Bitwise logical ops: '.&.', '.|.', 'xor', 'complement'++   * Extraction and concatenation: 'split', '#', and 'extend' (see the 'Splittable' class)++Usual arithmetic ('+', '-', '*', 'bvQuotRem') and logical operations ('.<', '.<=', '.>', '.>=', '.==', './=') operations are+supported for 'SInteger' fully, both in programming and verification modes. -}
Data/SBV/BitVectors/Data.hs view
@@ -20,7 +20,7 @@  module Data.SBV.BitVectors.Data  ( SBool, SWord8, SWord16, SWord32, SWord64- , SInt8, SInt16, SInt32, SInt64+ , SInt8, SInt16, SInt32, SInt64, SInteger  , SymWord(..)  , CW, cwVal, cwSameType, cwIsBit, cwToBool  , mkConstCW ,liftCW2, mapCW, mapCW2@@ -30,13 +30,14 @@  , sbvToSW, sbvToSymSW  , SBVExpr(..), newExpr  , cache, uncache, uncacheAI, HasSignAndSize(..)- , Op(..), NamedSymVar, UnintKind(..), getTableIndex, Pgm, Symbolic, runSymbolic, runSymbolic', State, Size, Outputtable(..), Result(..)+ , Op(..), NamedSymVar, UnintKind(..), getTableIndex, Pgm, Symbolic, runSymbolic, runSymbolic', State, inCodeGenMode, Size(..), Outputtable(..), Result(..)  , SBVType(..), newUninterpreted, unintFnUIKind, addAxiom  , Quantifier(..), needsExistentials  , SMTLibPgm(..), SMTLibVersion(..)  ) where  import Control.DeepSeq                 (NFData(..))+import Control.Monad                   (when) import Control.Monad.Reader            (MonadReader, ReaderT, ask, runReaderT) import Control.Monad.Trans             (MonadIO, liftIO) import Data.Char                       (isAlpha, isAlphaNum)@@ -44,6 +45,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)  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)@@ -65,21 +67,26 @@ cwSameType x y = cwSigned x == cwSigned y && cwSize x == cwSize y  cwIsBit :: CW -> Bool-cwIsBit x = not (cwSigned x) && cwSize x == 1+cwIsBit x = not (hasSign x) && not (isInfPrec x) && intSizeOf x == 1  cwToBool :: CW -> Bool cwToBool x = cwVal x /= 0  normCW :: CW -> CW-normCW x = x { cwVal = norm }-  where norm | cwSize x == 0  = 0-             | cwSigned x     = let rg = 2 ^ (cwSize x - 1)-                                in case divMod (cwVal x) rg of-                                    (a, b) | even a -> b-                                    (_, b)          -> b - rg-             | True           = cwVal x `mod` (2 ^ cwSize x)+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) -type Size      = Int+newtype Size   = Size { unSize :: Maybe Int }+               deriving (Eq, Ord)+ newtype NodeId = NodeId Int deriving (Eq, Ord) data SW        = SW (Bool, Size) NodeId deriving (Eq, Ord) @@ -89,12 +96,12 @@ needsExistentials = (EX `elem`)  falseSW, trueSW :: SW-falseSW = SW (False, 1) $ NodeId (-2)-trueSW  = SW (False, 1) $ NodeId (-1)+falseSW = SW (False, Size (Just 1)) $ NodeId (-2)+trueSW  = SW (False, Size (Just 1)) $ NodeId (-1)  falseCW, trueCW :: CW-falseCW = CW False 1 0-trueCW  = CW False 1 1+falseCW = CW False (Size (Just 1)) 0+trueCW  = CW False (Size (Just 1)) 1  newtype SBVType = SBVType [(Bool, Size)]              deriving (Eq, Ord)@@ -106,8 +113,9 @@ instance Show SBVType where   show (SBVType []) = error "SBV: internal error, empty SBVType"   show (SBVType xs) = intercalate " -> " $ map sh xs-    where sh (False, 1) = "SBool"-          sh (s, sz)    = (if s then "SInt" else "SWord") ++ show sz+    where sh (_,     Size Nothing)   = "SInteger"+          sh (False, Size (Just 1))  = "SBool"+          sh (s,     Size (Just sz)) = (if s then "SInt" else "SWord") ++ show sz  data Op = Plus | Times | Minus         | Quot | Rem -- quot and rem are unsigned only@@ -118,31 +126,36 @@         | 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, Int), (Bool, Int), Int) !SW !SW   -- (table-index, arg-type, res-type, length of the table) index out-of-bounds-value+        | LkUp (Int, (Bool, Size), (Bool, Size), 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)+ data SBVExpr = SBVApp !Op ![SW]              deriving (Eq, Ord)  class HasSignAndSize a where-  sizeOf   :: a -> Size-  hasSign  :: a -> Bool-  showType :: a -> String+  sizeOf     :: a -> Size+  intSizeOf  :: a -> Int+  hasSign    :: a -> Bool+  isInfPrec  :: a -> Bool+  showType   :: a -> String   showType a-    | not (hasSign a) && sizeOf a == 1 = "SBool"-    | True                             = (if hasSign a then "SInt" else "SWord") ++ show (sizeOf a)+    | isInfPrec a                         = "SInteger"+    | not (hasSign a) && intSizeOf a == 1 = "SBool"+    | True                                = (if hasSign a then "SInt" else "SWord") ++ show (intSizeOf a) -instance HasSignAndSize Bool   where {sizeOf _ =  1; hasSign _ = False}-instance HasSignAndSize Int8   where {sizeOf _ =  8; hasSign _ = True }-instance HasSignAndSize Word8  where {sizeOf _ =  8; hasSign _ = False}-instance HasSignAndSize Int16  where {sizeOf _ = 16; hasSign _ = True }-instance HasSignAndSize Word16 where {sizeOf _ = 16; hasSign _ = False}-instance HasSignAndSize Int32  where {sizeOf _ = 32; hasSign _ = True }-instance HasSignAndSize Word32 where {sizeOf _ = 32; hasSign _ = False}-instance HasSignAndSize Int64  where {sizeOf _ = 64; hasSign _ = True }-instance HasSignAndSize Word64 where {sizeOf _ = 64; hasSign _ = False}+instance HasSignAndSize Bool    where {sizeOf _ = Size (Just 1) ; intSizeOf _ =  1; isInfPrec _ = False; hasSign _ = False}+instance HasSignAndSize Int8    where {sizeOf _ = Size (Just 8) ; intSizeOf _ =  8; isInfPrec _ = False; hasSign _ = True }+instance HasSignAndSize Word8   where {sizeOf _ = Size (Just 8) ; intSizeOf _ =  8; isInfPrec _ = False; hasSign _ = False}+instance HasSignAndSize Int16   where {sizeOf _ = Size (Just 16); intSizeOf _ = 16; isInfPrec _ = False; hasSign _ = True }+instance HasSignAndSize Word16  where {sizeOf _ = Size (Just 16); intSizeOf _ = 16; isInfPrec _ = False; hasSign _ = False}+instance HasSignAndSize Int32   where {sizeOf _ = Size (Just 32); intSizeOf _ = 32; isInfPrec _ = False; hasSign _ = True }+instance HasSignAndSize Word32  where {sizeOf _ = Size (Just 32); intSizeOf _ = 32; isInfPrec _ = False; hasSign _ = False}+instance HasSignAndSize Int64   where {sizeOf _ = Size (Just 64); intSizeOf _ = 64; isInfPrec _ = False; hasSign _ = True }+instance HasSignAndSize Word64  where {sizeOf _ = Size (Just 64); intSizeOf _ = 64; isInfPrec _ = False; hasSign _ = False}+instance HasSignAndSize Integer where {sizeOf _ = Size Nothing; intSizeOf _ = error "attempting to compute size of Integer"; isInfPrec _ = True; hasSign _ = True}  liftCW :: (Integer -> b) -> CW -> b liftCW f x = f (cwVal x)@@ -160,12 +173,16 @@ mapCW2 _ a b = error $ "SBV.mapCW2: impossible, incompatible args received: " ++ show (a, b)  instance HasSignAndSize CW where-  sizeOf  = cwSize-  hasSign = cwSigned+  intSizeOf = maybe (error "attempting to compute size of SInteger") id . unSize . cwSize+  sizeOf    = cwSize+  hasSign   = cwSigned+  isInfPrec = maybe True (const False) . unSize . cwSize  instance HasSignAndSize SW where-  sizeOf  (SW (_, s) _) = s-  hasSign (SW (b, _) _) = b+  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 Show CW where   show w | cwIsBit w = show (cwToBool w)@@ -184,7 +201,11 @@   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 ++ "(" ++ show at ++ " -> " ++ show rt ++ ", " ++ show l ++ ")"+        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   show (ArrEq i j)   = "array_" ++ show i ++ " == array_" ++ show j   show (ArrRead i)   = "select array_" ++ show i   show (Uninterpreted i) = "uninterpreted_" ++ i@@ -229,20 +250,22 @@  deriving Show  -- | Result of running a symbolic computation-data Result = Result [(Quantifier, NamedSymVar)]                -- inputs (possibly existential)-                     [(SW, CW)]                                 -- constants-                     [((Int, (Bool, Int), (Bool, Int)), [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]                                       -- outputs+data Result = Result Bool                                         -- contains unbounded integers+                     [(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]                                         -- outputs  instance Show Result where-  show (Result _ cs _ _ [] [] _ [r])+  show (Result _ _ _ cs _ _ [] [] _ [r])     | Just c <- r `lookup` cs     = show c-  show (Result is cs ts as uis axs xs os)  = intercalate "\n" $+  show (Result _ cgs is cs ts as uis axs xs os)  = intercalate "\n" $                    ["INPUTS"]                 ++ map shn is                 ++ ["CONSTANTS"]@@ -253,6 +276,8 @@                 ++ map sha as                 ++ ["UNINTERPRETED CONSTANTS"]                 ++ map shui uis+                ++ ["USER GIVEN CODE SEGMENTS"]+                ++ concatMap shcg cgs                 ++ ["AXIOMS"]                 ++ map shax axs                 ++ ["DEFINE"]@@ -260,8 +285,9 @@                 ++ ["OUTPUTS"]                 ++ map (("  " ++) . show) os     where shs sw = show sw ++ " :: " ++ showType sw-          sht ((i, at, rt), es)  = "  Table " ++ show i ++ " : " ++ show at ++ "->" ++ show rt ++ " = " ++ show es+          sht ((i, at, rt), es)  = "  Table " ++ show i ++ " : " ++ mkT at ++ "->" ++ mkT 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             where ni = show sw                   ex | q == ALL = ""@@ -270,14 +296,15 @@                         | True     = ", aliasing " ++ show nm           sha (i, (nm, (ai, bi), ctx)) = "  " ++ ni ++ " :: " ++ mkT ai ++ " -> " ++ mkT bi ++ alias                                        ++ "\n     Context: "     ++ show ctx-            where mkT (b, s)-                   | s == 1  = "SBool"-                   | True    = if b then "SInt" else "SWord" ++ show s-                  ni = "array_" ++ show i+            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@@ -293,10 +320,11 @@  type ExprMap   = Map.Map SBVExpr SW type CnstMap   = Map.Map CW SW-type TableMap  = Map.Map [SW] (Int, (Bool, Int), (Bool, Int))+type TableMap  = Map.Map [SW] (Int, (Bool, Size), (Bool, Size)) type ArrayInfo = (String, ((Bool, Size), (Bool, Size)), ArrayContext) type ArrayMap  = IMap.IntMap ArrayInfo type UIMap     = Map.Map String SBVType+type CgMap     = Map.Map String [String] type Cache a   = IMap.IntMap [(StableName (State -> IO a), a)]  unintFnUIKind :: (String, SBVType) -> (String, UnintKind)@@ -311,18 +339,21 @@         external (ArrayMutate{}) = False         external (ArrayMerge{})  = False -data State  = State { rctr       :: IORef Int-                    , rinps      :: IORef [(Quantifier, NamedSymVar)]-                    , routs      :: IORef [SW]-                    , rtblMap    :: IORef TableMap-                    , spgm       :: IORef Pgm-                    , rconstMap  :: IORef CnstMap-                    , rexprMap   :: IORef ExprMap-                    , rArrayMap  :: IORef ArrayMap-                    , rUIMap     :: IORef UIMap-                    , raxioms    :: IORef [(String, [String])]-                    , rSWCache   :: IORef (Cache SW)-                    , rAICache   :: IORef (Cache Int)+data State  = State { inCodeGenMode :: Bool+                    , rctr          :: IORef Int+                    , rInfPrec      :: IORef Bool+                    , rinps         :: IORef [(Quantifier, NamedSymVar)]+                    , routs         :: IORef [SW]+                    , rtblMap       :: IORef TableMap+                    , spgm          :: IORef Pgm+                    , rconstMap     :: IORef CnstMap+                    , rexprMap      :: IORef ExprMap+                    , rArrayMap     :: IORef ArrayMap+                    , rUIMap        :: IORef UIMap+                    , rCgMap        :: IORef CgMap+                    , raxioms       :: IORef [(String, [String])]+                    , rSWCache      :: IORef (Cache SW)+                    , rAICache      :: IORef (Cache Int)                     }  -- | The "Symbolic" value. Either a constant (@Left@) or a symbolic@@ -358,10 +389,14 @@ -- | 64-bit signed symbolic value, 2's complement representation type SInt64  = SBV Int64 +-- | Infinite precision signed symbolic value+type SInteger = SBV Integer+ -- Needed to satisfy the Num hierarchy instance Show (SBV a) where-  show (SBV _         (Left c))  = show c-  show (SBV (sgn, sz) (Right _)) = "<symbolic> :: " ++ t+  show (SBV _                     (Left c))  = show c+  show (SBV (_  , Size Nothing)   (Right _)) = "<symbolic> :: SInteger"+  show (SBV (sgn, Size (Just sz)) (Right _)) = "<symbolic> :: " ++ t                 where t | not sgn && sz == 1 = "SBool"                         | True               = (if sgn then "SInt" else "SWord") ++ show sz @@ -372,8 +407,10 @@   a /= b = error $ "Comparing symbolic bit-vectors; Use (./=) instead. Received: " ++ show (a, b)  instance HasSignAndSize (SBV a) where-  sizeOf  (SBV (_, s) _) = s-  hasSign (SBV (b, _) _) = b+  sizeOf    (SBV (_, mbs) _) = mbs+  intSizeOf (SBV (_, mbs) _) = maybe (error "attempting to compute size of SInteger") id $ unSize mbs+  isInfPrec (SBV (_, mbs) _) = maybe True (const False) $ unSize mbs+  hasSign   (SBV (b, _) _)   = b  incCtr :: State -> IO Int incCtr s = do ctr <- readIORef (rctr s)@@ -381,9 +418,9 @@               i `seq` writeIORef (rctr s) i               return ctr -newUninterpreted :: State -> String -> SBVType -> IO ()-newUninterpreted st nm t-  | null nm || not (isAlpha (head nm)) || not (all isAlphaNum (tail nm))+newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO ()+newUninterpreted st nm t mbCode+  | null nm || not (isAlpha (head nm)) || not (all validChar (tail nm))   = error $ "Bad uninterpreted constant name: " ++ show nm ++ ". Must be a valid identifier."   | True = do         uiMap <- readIORef (rUIMap st)@@ -393,7 +430,9 @@                                 ++ "      Current type      : " ++ show t ++ "\n"                                 ++ "      Previously used at: " ++ show t'                      else return ()-          Nothing -> modifyIORef (rUIMap st) (Map.insert nm t)+          Nothing -> do modifyIORef (rUIMap st) (Map.insert nm t)+                        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 newConst :: State -> CW -> IO SW@@ -403,11 +442,12 @@     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                   modifyIORef (rconstMap st) (Map.insert c sw)                   return sw  -- Create a new table; hash-cons as necessary-getTableIndex :: State -> (Bool, Int) -> (Bool, Int) -> [SW] -> IO Int+getTableIndex :: State -> (Bool, Size) -> (Bool, Size) -> [SW] -> IO Int getTableIndex st at rt elts = do   tblMap <- readIORef (rtblMap st)   case elts `Map.lookup` tblMap of@@ -429,6 +469,7 @@      Just sw -> return sw      Nothing -> do ctr <- incCtr st                    let sw = SW sgnsz (NodeId ctr)+                   when (isInfPrec sw) $ writeIORef (rInfPrec st) True                    modifyIORef (spgm st)     (flip (S.|>) (sw, e))                    modifyIORef (rexprMap st) (Map.insert e sw)                    return sw@@ -452,6 +493,7 @@         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         liftIO $ modifyIORef (rinps st) ((q, (sw, nm)):)         return $ SBV sgnsz $ Right $ cache (const (return sw)) @@ -508,12 +550,11 @@  -- | Run a symbolic computation and return a 'Result' runSymbolic :: Symbolic a -> IO Result-runSymbolic c = do (_, r) <- runSymbolic' c-                   return r+runSymbolic c = snd `fmap` runSymbolic' False c  -- | Run a symbolic computation, and return a extra value paired up with the 'Result'-runSymbolic' :: Symbolic a -> IO (a, Result)-runSymbolic' (Symbolic c) = do+runSymbolic' :: Bool -> Symbolic a -> IO (a, Result)+runSymbolic' cgMode (Symbolic c) = do    ctr     <- newIORef (-2) -- start from -2; False and True will always occupy the first two elements    pgm     <- newIORef S.empty    emap    <- newIORef Map.empty@@ -523,24 +564,29 @@    tables  <- newIORef Map.empty    arrays  <- newIORef IMap.empty    uis     <- newIORef Map.empty+   cgs     <- newIORef Map.empty    axioms  <- newIORef []    swCache <- newIORef IMap.empty    aiCache <- newIORef IMap.empty-   let st = State { rctr      = ctr-                  , rinps     = inps-                  , routs     = outs-                  , rtblMap   = tables-                  , spgm      = pgm-                  , rconstMap = cmap-                  , rArrayMap = arrays-                  , rexprMap  = emap-                  , rUIMap    = uis-                  , raxioms   = axioms-                  , rSWCache  = swCache-                  , rAICache  = aiCache+   infPrec <- newIORef False+   let st = State { inCodeGenMode = cgMode+                  , rctr          = ctr+                  , rInfPrec      = infPrec+                  , rinps         = inps+                  , routs         = outs+                  , rtblMap       = tables+                  , spgm          = pgm+                  , rconstMap     = cmap+                  , rArrayMap     = arrays+                  , rexprMap      = emap+                  , rUIMap        = uis+                  , rCgMap        = cgs+                  , raxioms       = axioms+                  , rSWCache      = swCache+                  , rAICache      = aiCache                   }-   _ <- newConst st (mkConstCW (False,1) (0::Integer)) -- s(-2) == falseSW-   _ <- newConst st (mkConstCW (False,1) (1::Integer)) -- s(-1) == trueSW+   _ <- newConst st (mkConstCW (False, Size (Just 1)) (0::Integer)) -- s(-2) == falseSW+   _ <- newConst st (mkConstCW (False, Size (Just 1)) (1::Integer)) -- s(-1) == trueSW    r <- runReaderT c st    rpgm  <- readIORef pgm    inpsR <- readIORef inps@@ -552,7 +598,9 @@    arrs  <- IMap.toAscList `fmap` readIORef arrays    unint <- Map.toList `fmap` readIORef uis    axs   <- reverse `fmap` readIORef axioms-   return $ (r, Result (reverse inpsR) cnsts tbls arrs unint axs rpgm (reverse outsR))+   hasInfPrec <- readIORef infPrec+   cgMap <- Map.toList `fmap` readIORef cgs+   return $ (r, Result hasInfPrec cgMap (reverse inpsR) cnsts tbls arrs unint axs rpgm (reverse outsR))  ------------------------------------------------------------------------------- -- * Symbolic Words@@ -563,7 +611,7 @@ -- provide the necessary bits. -- -- Minimal complete definiton: forall, forall_, exists, exists_, literal, fromCW-class (Bounded a, Ord a) => SymWord a where+class Ord a => SymWord a where   -- | Create a user named input (universal)   forall :: String -> Symbolic (SBV a)   -- | Create an automatically named input@@ -588,6 +636,9 @@   isSymbolic :: SBV a -> Bool   -- | Does it concretely satisfy the given predicate?   isConcretely :: SBV a -> (a -> Bool) -> Bool+  -- | max/minbounds, if available. Note that we don't want+  -- to impose "Bounded" on our class as Integer is not Bounded but it is a SymWord+  mbMaxBound, mbMinBound :: Maybe a    -- minimal complete definiton: forall, forall_, exists, exists_, literal, fromCW   mkForallVars n = mapM (const forall_) [1 .. n]@@ -775,9 +826,10 @@   rnf (CW x y z) = x `seq` y `seq` z `seq` ()  instance NFData Result where-  rnf (Result inps consts tbls arrs uis axs pgm outs)-        = rnf inps `seq` rnf consts `seq` rnf tbls `seq` rnf arrs `seq` rnf uis `seq` rnf axs `seq` rnf pgm `seq` rnf outs+  rnf (Result isInf cgs inps consts tbls arrs uis axs pgm outs)+        = rnf isInf `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 outs +instance NFData Size instance NFData ArrayContext instance NFData Pgm instance NFData SW
Data/SBV/BitVectors/Model.hs view
@@ -22,7 +22,7 @@ module Data.SBV.BitVectors.Model (     Mergeable(..), EqSymbolic(..), OrdSymbolic(..), BVDivisible(..), Uninterpreted(..)   , bitValue, setBitTo, allEqual, allDifferent, oneIf, blastBE, blastLE-  , lsb, msb, SBVUF, sbvUFName, genVar, genVar_, forall, forall_, exists, exists_+  , lsb, msb, SBVUF, sbvUFName, genFinVar, genFinVar_, forall, forall_, exists, exists_   )   where @@ -55,27 +55,27 @@           -> (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, 1) $ Right $ cache c+liftSym2B opS _   a                b                = SBV (False, Size (Just 1)) $ Right $ cache c   where c st = do sw1 <- sbvToSW st a                   sw2 <- sbvToSW st b-                  opS st (False, 1) sw1 sw2+                  opS st (False, Size (Just 1)) sw1 sw2  liftSym1Bool :: (State -> (Bool, Size) -> SW -> IO SW)              -> (Bool -> Bool)              -> SBool -> SBool liftSym1Bool _   opC (SBV _ (Left a)) = literal $ opC $ cwToBool a-liftSym1Bool opS _   a                = SBV (False, 1) $ Right $ cache c+liftSym1Bool opS _   a                = SBV (False, Size (Just 1)) $ Right $ cache c   where c st = do sw <- sbvToSW st a-                  opS st (False, 1) sw+                  opS st (False, Size (Just 1)) sw  liftSym2Bool :: (State -> (Bool, Size) -> 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, 1) $ Right $ cache c+liftSym2Bool opS _   a                b                = SBV (False, Size (Just 1)) $ Right $ cache c   where c st = do sw1 <- sbvToSW st a                   sw2 <- sbvToSW st b-                  opS st (False, 1) sw1 sw2+                  opS st (False, Size (Just 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)@@ -91,90 +91,119 @@  -- Symbolic-Word class instances -genVar :: Quantifier -> (Bool, Size) -> String -> Symbolic (SBV a)-genVar q s = mkSymSBV q s . Just+genFinVar :: Quantifier -> (Bool, Int) -> String -> Symbolic (SBV a)+genFinVar q (sg, sz) = mkSymSBV q (sg, Size (Just sz)) . Just -genVar_ :: Quantifier -> (Bool, Size) -> Symbolic (SBV a)-genVar_ b s = mkSymSBV b s Nothing+genFinVar_ :: Quantifier -> (Bool, Int) -> Symbolic (SBV a)+genFinVar_ b (sg, sz) = mkSymSBV b (sg, Size (Just sz)) Nothing -genLiteral :: Integral a => (Bool,Size) -> a -> SBV b-genLiteral s  = SBV s . Left . mkConstCW s+genFinLiteral :: Integral a => (Bool, Int) -> a -> SBV b+genFinLiteral (sg, sz)  = SBV s . Left . mkConstCW s+  where s = (sg, Size (Just sz))  genFromCW :: Integral a => CW -> a genFromCW x = fromInteger (cwVal x)  instance SymWord Bool where-  forall    = genVar  ALL (False, 1)-  forall_   = genVar_ ALL (False, 1)-  exists    = genVar  EX  (False, 1)-  exists_   = genVar_ EX  (False, 1)-  literal x = genLiteral (False, 1) (if x then (1::Integer) else 0)-  fromCW    = cwToBool+  forall     = genFinVar  ALL (False, 1)+  forall_    = genFinVar_ ALL (False, 1)+  exists     = genFinVar  EX  (False, 1)+  exists_    = genFinVar_ EX  (False, 1)+  literal x  = genFinLiteral (False, 1) (if x then (1::Integer) else 0)+  fromCW     = cwToBool+  mbMaxBound = Just maxBound+  mbMinBound = Just minBound  instance SymWord Word8 where-  forall  = genVar   ALL (False, 8)-  forall_ = genVar_  ALL (False, 8)-  exists  = genVar   EX  (False, 8)-  exists_ = genVar_  EX  (False, 8)-  literal = genLiteral (False, 8)-  fromCW  = genFromCW+  forall     = genFinVar   ALL (False, 8)+  forall_    = genFinVar_  ALL (False, 8)+  exists     = genFinVar   EX  (False, 8)+  exists_    = genFinVar_  EX  (False, 8)+  literal    = genFinLiteral (False, 8)+  fromCW     = genFromCW+  mbMaxBound = Just maxBound+  mbMinBound = Just minBound  instance SymWord Int8 where-  forall  = genVar   ALL (True, 8)-  forall_ = genVar_  ALL (True, 8)-  exists  = genVar   EX  (True, 8)-  exists_ = genVar_  EX  (True, 8)-  literal = genLiteral (True, 8)-  fromCW  = genFromCW+  forall     = genFinVar   ALL (True, 8)+  forall_    = genFinVar_  ALL (True, 8)+  exists     = genFinVar   EX  (True, 8)+  exists_    = genFinVar_  EX  (True, 8)+  literal    = genFinLiteral (True, 8)+  fromCW     = genFromCW+  mbMaxBound = Just maxBound+  mbMinBound = Just minBound  instance SymWord Word16 where-  forall  = genVar   ALL (False, 16)-  forall_ = genVar_  ALL (False, 16)-  exists  = genVar   EX  (False, 16)-  exists_ = genVar_  EX  (False, 16)-  literal = genLiteral (False, 16)-  fromCW  = genFromCW+  forall     = genFinVar   ALL (False, 16)+  forall_    = genFinVar_  ALL (False, 16)+  exists     = genFinVar   EX  (False, 16)+  exists_    = genFinVar_  EX  (False, 16)+  literal    = genFinLiteral (False, 16)+  fromCW     = genFromCW+  mbMaxBound = Just maxBound+  mbMinBound = Just minBound  instance SymWord Int16 where-  forall  = genVar   ALL (True, 16)-  forall_ = genVar_  ALL (True, 16)-  exists  = genVar   EX  (True, 16)-  exists_ = genVar_  EX  (True, 16)-  literal = genLiteral (True, 16)-  fromCW  = genFromCW+  forall     = genFinVar   ALL (True, 16)+  forall_    = genFinVar_  ALL (True, 16)+  exists     = genFinVar   EX  (True, 16)+  exists_    = genFinVar_  EX  (True, 16)+  literal    = genFinLiteral (True, 16)+  fromCW     = genFromCW+  mbMaxBound = Just maxBound+  mbMinBound = Just minBound  instance SymWord Word32 where-  forall  = genVar   ALL (False, 32)-  forall_ = genVar_  ALL (False, 32)-  exists  = genVar   EX  (False, 32)-  exists_ = genVar_  EX  (False, 32)-  literal = genLiteral (False, 32)-  fromCW  = genFromCW+  forall     = genFinVar   ALL (False, 32)+  forall_    = genFinVar_  ALL (False, 32)+  exists     = genFinVar   EX  (False, 32)+  exists_    = genFinVar_  EX  (False, 32)+  literal    = genFinLiteral (False, 32)+  fromCW     = genFromCW+  mbMaxBound = Just maxBound+  mbMinBound = Just minBound  instance SymWord Int32 where-  forall  = genVar   ALL (True, 32)-  forall_ = genVar_  ALL (True, 32)-  exists  = genVar   EX  (True, 32)-  exists_ = genVar_  EX  (True, 32)-  literal = genLiteral (True, 32)-  fromCW  = genFromCW+  forall     = genFinVar   ALL (True, 32)+  forall_    = genFinVar_  ALL (True, 32)+  exists     = genFinVar   EX  (True, 32)+  exists_    = genFinVar_  EX  (True, 32)+  literal    = genFinLiteral (True, 32)+  fromCW     = genFromCW+  mbMaxBound = Just maxBound+  mbMinBound = Just minBound  instance SymWord Word64 where-  forall  = genVar   ALL (False, 64)-  forall_ = genVar_  ALL (False, 64)-  exists  = genVar   EX  (False, 64)-  exists_ = genVar_  EX  (False, 64)-  literal = genLiteral (False, 64)-  fromCW  = genFromCW+  forall     = genFinVar   ALL (False, 64)+  forall_    = genFinVar_  ALL (False, 64)+  exists     = genFinVar   EX  (False, 64)+  exists_    = genFinVar_  EX  (False, 64)+  literal    = genFinLiteral (False, 64)+  fromCW     = genFromCW+  mbMaxBound = Just maxBound+  mbMinBound = Just minBound  instance SymWord Int64 where-  forall  = genVar   ALL (True, 64)-  forall_ = genVar_  ALL (True, 64)-  exists  = genVar   EX  (True, 64)-  exists_ = genVar_  EX  (True, 64)-  literal = genLiteral (True, 64)-  fromCW  = genFromCW+  forall     = genFinVar   ALL (True, 64)+  forall_    = genFinVar_  ALL (True, 64)+  exists     = genFinVar   EX  (True, 64)+  exists_    = genFinVar_  EX  (True, 64)+  literal    = genFinLiteral (True, 64)+  fromCW     = genFromCW+  mbMaxBound = Just maxBound+  mbMinBound = Just minBound +instance SymWord Integer where+  forall     = mkSymSBV ALL (True, Size Nothing) . Just+  forall_    = mkSymSBV ALL (True, Size Nothing) Nothing+  exists     = mkSymSBV EX  (True, Size Nothing) . Just+  exists_    = mkSymSBV EX  (True, Size Nothing) Nothing+  literal    = SBV (True, Size Nothing) . Left . mkConstCW (True, Size Nothing)+  fromCW     = genFromCW+  mbMaxBound = Nothing+  mbMinBound = Nothing+ -- | 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. --@@ -223,21 +252,21 @@  instance SymWord a => OrdSymbolic (SBV a) where   x .< y-    | x `isConcretely` (== maxBound) = false-    | y `isConcretely` (== minBound) = false-    | True                           = liftSym2B (mkSymOpSC (eqOpt falseSW) LessThan)    (<)  x y+    | Just mb <- mbMaxBound, x `isConcretely` (== mb) = false+    | Just mb <- mbMinBound, y `isConcretely` (== mb) = false+    | True                                            = liftSym2B (mkSymOpSC (eqOpt falseSW) LessThan)    (<)  x y   x .<= y-    | x `isConcretely` (== minBound) = true-    | y `isConcretely` (== maxBound) = true-    | True                           = liftSym2B (mkSymOpSC (eqOpt trueSW) LessEq)       (<=) x y+    | Just mb <- mbMinBound, x `isConcretely` (== mb) = true+    | Just mb <- mbMaxBound, y `isConcretely` (== mb) = true+    | True                                            = liftSym2B (mkSymOpSC (eqOpt trueSW) LessEq)       (<=) x y   x .> y-    | x `isConcretely` (== minBound) = false-    | y `isConcretely` (== maxBound) = false-    | True                           = liftSym2B (mkSymOpSC (eqOpt falseSW) GreaterThan) (>)  x y+    | Just mb <- mbMinBound, x `isConcretely` (== mb) = false+    | Just mb <- mbMaxBound, y `isConcretely` (== mb) = false+    | True                                            = liftSym2B (mkSymOpSC (eqOpt falseSW) GreaterThan) (>)  x y   x .>= y-    | x `isConcretely` (== maxBound) = true-    | y `isConcretely` (== minBound) = true-    | True                           = liftSym2B (mkSymOpSC (eqOpt trueSW) GreaterEq)    (>=) x y+    | Just mb <- mbMaxBound, x `isConcretely` (== mb) = true+    | Just mb <- mbMinBound, y `isConcretely` (== mb) = true+    | True                                            = liftSym2B (mkSymOpSC (eqOpt trueSW) GreaterEq)    (>=) x y  -- Bool instance EqSymbolic Bool where@@ -418,8 +447,9 @@     | x `isConcretely` (== 0)  = y     | y `isConcretely` (== 0)  = x     | True                     = liftSym2 (mkSymOp  XOr) xor x y-  complement               = liftSym1 (mkSymOp1 Not) complement-  bitSize  (SBV (_ ,s) _)  = s+  complement = liftSym1 (mkSymOp1 Not) complement+  bitSize  (SBV (_, Size (Just s)) _) = s+  bitSize  (SBV (_, Size Nothing)  _) = error "Data.Bits.bitSize(Integer)"   isSigned (SBV (b, _) _)  = b   shiftL x y     | y < 0                = shiftR x (-y)@@ -460,7 +490,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 = map (bitValue x) [0 .. (sizeOf x)-1]+blastLE x+ | isInfPrec x = error "SBV.blastLE: Called on an infinite precision value"+ | True        = map (bitValue 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]@@ -472,7 +504,9 @@  -- | Most significant bit of a word, always stored at the last position msb :: (Bits a, SymWord a) => SBV a -> SBool-msb x = bitValue x ((sizeOf x) - 1)+msb x+ | isInfPrec x = error "SBV.msb: Called on an infinite precision value"+ | True        = bitValue 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@@ -546,18 +580,34 @@   bvQuotRem x 0 = (0, x)   bvQuotRem x y = x `quotRem` y +instance BVDivisible Int64 where+  bvQuotRem x 0 = (0, x)+  bvQuotRem x y = x `quotRem` y+ instance BVDivisible Word32 where   bvQuotRem x 0 = (0, x)   bvQuotRem x y = x `quotRem` y +instance BVDivisible Int32 where+  bvQuotRem x 0 = (0, x)+  bvQuotRem x y = x `quotRem` y+ instance BVDivisible Word16 where   bvQuotRem x 0 = (0, x)   bvQuotRem x y = x `quotRem` y +instance BVDivisible Int16 where+  bvQuotRem x 0 = (0, x)+  bvQuotRem x y = x `quotRem` y+ instance BVDivisible Word8 where   bvQuotRem x 0 = (0, x)   bvQuotRem x y = x `quotRem` y +instance BVDivisible Int8 where+  bvQuotRem x 0 = (0, x)+  bvQuotRem x y = x `quotRem` y+ instance BVDivisible Integer where   bvQuotRem x 0 = (0, x)   bvQuotRem x y = x `quotRem` y@@ -571,15 +621,30 @@ instance BVDivisible SWord64 where   bvQuotRem = liftQRem +instance BVDivisible SInt64 where+  bvQuotRem = liftQRem+ instance BVDivisible SWord32 where   bvQuotRem = liftQRem +instance BVDivisible SInt32 where+  bvQuotRem = liftQRem+ instance BVDivisible SWord16 where   bvQuotRem = liftQRem +instance BVDivisible SInt16 where+  bvQuotRem = liftQRem+ instance BVDivisible SWord8 where   bvQuotRem = liftQRem +instance BVDivisible SInt8 where+  bvQuotRem = liftQRem++instance BVDivisible SInteger where+  bvQuotRem = liftQRem+ liftQRem :: (SymWord a, Num a, BVDivisible a) => SBV a -> SBV a -> (SBV a, SBV a) liftQRem x y = ite (y .== 0) (0, x) (qr x y)   where qr (SBV sgnsz (Left a)) (SBV _ (Left b)) = let (q, r) = bvQuotRem a b in (SBV sgnsz (Left q), SBV sgnsz (Left r))@@ -760,10 +825,10 @@  -- SArrays are both "EqSymbolic" and "Mergeable" instance EqSymbolic (SArray a b) where-  (SArray _ a) .== (SArray _ b) = SBV (False, 1) $ Right $ cache c+  (SArray _ a) .== (SArray _ b) = SBV (False, Size (Just 1)) $ Right $ cache c     where c st = do ai <- uncacheAI a st                     bi <- uncacheAI b st-                    newExpr st (False, 1) (SBVApp (ArrEq ai bi) [])+                    newExpr st (False, Size (Just 1)) (SBVApp (ArrEq ai bi) [])  instance SymWord b => Mergeable (SArray a b) where   symbolicMerge = mergeArrays@@ -814,16 +879,29 @@   -- | Uninterpret a value, but also get a handle to the resulting object. This handle   -- can be used to add axioms for this object. (See 'addAxiom'.)   uninterpretWithHandle :: String -> (SBVUF, a)+  -- | Uninterpret a value, only for the purposes of code-generation. For execution+  -- and verification the value is used as is. For code-generation, the alternate+  -- definition is used. This is useful when we want to take advantage of native+  -- libraries on the target languages.+  cgUninterpret :: String -> [String] -> a -> a+  -- | Most generalized form of uninterpretation, this function should not be needed+  -- by end-user-code, but is rather useful for the library development.+  sbvUninterpret :: Maybe ([String], a) -> String -> (SBVUF, a) -  -- minimal complete definition: 'uninterpretWithHandle'-  uninterpret = snd . uninterpretWithHandle+  -- minimal complete definition: 'sbvUninterpret'+  uninterpret             = snd . uninterpretWithHandle+  uninterpretWithHandle   = sbvUninterpret Nothing+  cgUninterpret nm code v = snd $ sbvUninterpret (Just (code, v)) nm  -- Plain constants instance HasSignAndSize a => Uninterpreted (SBV a) where-  uninterpretWithHandle nm = (mkUFName nm, SBV sgnsza $ Right $ cache result)+  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))-          result st = do newUninterpreted st nm (SBVType [sgnsza])-                         newExpr st sgnsza $ SBVApp (Uninterpreted nm) []+          result st | Just (_, v) <- mbCgData, not (inCodeGenMode st) = sbvToSW st v+                    | True = do newUninterpreted st nm (SBVType [sgnsza]) (fst `fmap` mbCgData)+                                newExpr st sgnsza $ 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@@ -832,87 +910,116 @@ forceArg (SW (b, s) n) = b `seq` s `seq` n `seq` return ()  -- Functions of one argument-instance (HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV b -> SBV a) where-  uninterpretWithHandle nm = (mkUFName nm, f)-    where f arg0 = SBV sgnsza $ Right $ cache result+instance (SymWord b, HasSignAndSize b, HasSignAndSize 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))-                 result st = do newUninterpreted st nm (SBVType [sgnszb, sgnsza])-                                sw0 <- sbvToSW st arg0-                                mapM_ forceArg [sw0]-                                newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0]+                 result st | Just (_, v) <- mbCgData, not (inCodeGenMode st) = sbvToSW st (v arg0)+                           | True = do newUninterpreted st nm (SBVType [sgnszb, sgnsza]) (fst `fmap` mbCgData)+                                       sw0 <- sbvToSW st arg0+                                       mapM_ forceArg [sw0]+                                       newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0]  -- Functions of two arguments-instance (HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV c -> SBV b -> SBV a) where-  uninterpretWithHandle nm = (mkUFName nm, f)-    where f arg0 arg1 = SBV sgnsza $ Right $ cache result+instance (SymWord c, SymWord b, HasSignAndSize c, HasSignAndSize b, HasSignAndSize 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))-                 result st = do newUninterpreted st nm (SBVType [sgnszc, sgnszb, sgnsza])-                                sw0 <- sbvToSW st arg0-                                sw1 <- sbvToSW st arg1-                                mapM_ forceArg [sw0, sw1]-                                newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1]+                 result st | Just (_, v) <- mbCgData, not (inCodeGenMode st) = sbvToSW st (v arg0 arg1)+                           | True = do newUninterpreted st nm (SBVType [sgnszc, sgnszb, sgnsza]) (fst `fmap` mbCgData)+                                       sw0 <- sbvToSW st arg0+                                       sw1 <- sbvToSW st arg1+                                       mapM_ forceArg [sw0, sw1]+                                       newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1]  -- Functions of three arguments-instance (HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) where-  uninterpretWithHandle nm = (mkUFName nm, f)-    where f arg0 arg1 arg2 = SBV sgnsza $ Right $ cache result+instance (SymWord d, SymWord c, SymWord b, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize 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))-                 result st = do newUninterpreted st nm (SBVType [sgnszd, sgnszc, sgnszb, sgnsza])-                                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]+                 result st | Just (_, v) <- mbCgData, not (inCodeGenMode st) = sbvToSW st (v arg0 arg1 arg2)+                           | True = do newUninterpreted st nm (SBVType [sgnszd, sgnszc, sgnszb, sgnsza]) (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]  -- Functions of four arguments-instance (HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)+instance (SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)             => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where-  uninterpretWithHandle nm = (mkUFName nm, f)-    where f arg0 arg1 arg2 arg3 = SBV sgnsza $ Right $ cache result+  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))-                 result st = do newUninterpreted st nm (SBVType [sgnsze, sgnszd, sgnszc, sgnszb, sgnsza])-                                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]+                 result st | Just (_, v) <- mbCgData, not (inCodeGenMode st) = sbvToSW st (v arg0 arg1 arg2 arg3)+                           | True = do newUninterpreted st nm (SBVType [sgnsze, sgnszd, sgnszc, sgnszb, sgnsza]) (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]  -- Functions of five arguments-instance (HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)+instance (SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)             => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where-  uninterpretWithHandle nm = (mkUFName nm, f)-    where f arg0 arg1 arg2 arg3 arg4 = SBV sgnsza $ Right $ cache result+  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))-                 result st = do newUninterpreted st nm (SBVType [sgnszf, sgnsze, sgnszd, sgnszc, sgnszb, sgnsza])-                                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]+                 result st | Just (_, v) <- mbCgData, not (inCodeGenMode st) = sbvToSW st (v arg0 arg1 arg2 arg3 arg4)+                           | True = do newUninterpreted st nm (SBVType [sgnszf, sgnsze, sgnszd, sgnszc, sgnszb, sgnsza]) (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]  -- Functions of six arguments-instance (HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)+instance (SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)             => Uninterpreted (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where-  uninterpretWithHandle nm = (mkUFName nm, f)-    where f arg0 arg1 arg2 arg3 arg4 arg5 = SBV sgnsza $ Right $ cache result+  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))@@ -920,21 +1027,26 @@                  sgnsze = (hasSign (undefined :: e), sizeOf (undefined :: e))                  sgnszf = (hasSign (undefined :: f), sizeOf (undefined :: f))                  sgnszg = (hasSign (undefined :: g), sizeOf (undefined :: g))-                 result st = do newUninterpreted st nm (SBVType [sgnszg, sgnszf, sgnsze, sgnszd, sgnszc, sgnszb, sgnsza])-                                sw0 <- sbvToSW st arg0-                                sw1 <- sbvToSW st arg1-                                sw2 <- sbvToSW st arg2-                                sw3 <- sbvToSW st arg3-                                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]+                 result st | Just (_, v) <- mbCgData, not (inCodeGenMode 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)+                                       sw0 <- sbvToSW st arg0+                                       sw1 <- sbvToSW st arg1+                                       sw2 <- sbvToSW st arg2+                                       sw3 <- sbvToSW st arg3+                                       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]  -- Functions of seven arguments-instance (HasSignAndSize h, HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)+instance (SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize h, HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)             => Uninterpreted (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where-  uninterpretWithHandle nm = (mkUFName nm, f)-    where f arg0 arg1 arg2 arg3 arg4 arg5 arg6 = SBV sgnsza $ Right $ cache result+  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))@@ -943,41 +1055,48 @@                  sgnszf = (hasSign (undefined :: f), sizeOf (undefined :: f))                  sgnszg = (hasSign (undefined :: g), sizeOf (undefined :: g))                  sgnszh = (hasSign (undefined :: h), sizeOf (undefined :: h))-                 result st = do newUninterpreted st nm (SBVType [sgnszh, sgnszg, sgnszf, sgnsze, sgnszd, sgnszc, sgnszb, sgnsza])-                                sw0 <- sbvToSW st arg0-                                sw1 <- sbvToSW st arg1-                                sw2 <- sbvToSW st arg2-                                sw3 <- sbvToSW st arg3-                                sw4 <- sbvToSW st arg4-                                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]+                 result st | Just (_, v) <- mbCgData, not (inCodeGenMode 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)+                                      sw0 <- sbvToSW st arg0+                                      sw1 <- sbvToSW st arg1+                                      sw2 <- sbvToSW st arg2+                                      sw3 <- sbvToSW st arg3+                                      sw4 <- sbvToSW st arg4+                                      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]  -- Uncurried functions of two arguments-instance (HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV c, SBV b) -> SBV a) where-  uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1) -> f arg0 arg1)+instance (SymWord c, SymWord b, HasSignAndSize c, HasSignAndSize b, HasSignAndSize 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 (HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) where-  uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1, arg2) -> f arg0 arg1 arg2)+instance (SymWord d, SymWord c, SymWord b, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize 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 (HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)+instance (SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)             => Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) where-  uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1, arg2, arg3) -> f arg0 arg1 arg2 arg3)+  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 (HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)+instance (SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)             => Uninterpreted ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where-  uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1, arg2, arg3, arg4) -> f arg0 arg1 arg2 arg3 arg4)+  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 (HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)+instance (SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)             => Uninterpreted ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where-  uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1, arg2, arg3, arg4, arg5) -> f arg0 arg1 arg2 arg3 arg4 arg5)+  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 (HasSignAndSize h, HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)+instance (SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize h, HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)             => Uninterpreted ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where-  uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1, arg2, arg3, arg4, arg5, arg6) -> f arg0 arg1 arg2 arg3 arg4 arg5 arg6)+  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))
+ Data/SBV/BitVectors/Optimize.hs view
@@ -0,0 +1,59 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.BitVectors.Optimize+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+-- Portability :  portable+--+-- Number representations in hex/bin+-----------------------------------------------------------------------------++{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeSynonymInstances #-}++module Data.SBV.BitVectors.Optimize (optimize, minimize, maximize) where++import Data.SBV.BitVectors.Data+import Data.SBV.BitVectors.Model (OrdSymbolic(..))+import Data.SBV.Provers.Prover   (satWith, z3)+import Data.SBV.SMT.SMT          (SatModel, getModel)+import Data.SBV.Utils.Boolean++-- | Symbolic optimization. Generalization on 'minimize' and 'maximize' that allows arbitrary+-- cost functions and comparisons.+optimize :: (SatModel a, SymWord a)+         => (cost -> cost -> SBool)           -- ^ comparator+         -> ([SBV a] -> cost)                 -- ^ cost function+         -> Int                               -- ^ how many elements?+         -> ([SBV a] -> SBool)                -- ^ validity constraint+         -> IO (Maybe [a])+optimize cmp cost n valid = do+        m <- satWith z3 $ do+                xs <- mkExistVars  n+                ys <- mkForallVars n+                return $ valid xs &&& (valid ys ==> cost xs `cmp` cost ys)+        case getModel m of+          Right (False, a) -> return $ Just a+          _                -> return Nothing++-- | Maximizes a cost function with respect to a constraint. Examples:+--+--   >>> maximize sum 3 (bAll (.< (10 :: SInteger)))+--   Just [9,9,9]+--+--   >>> maximize sum 3 (bAll (.> (10 :: SInteger)))+--   Nothing+maximize :: (SatModel a, SymWord a, OrdSymbolic cost) => ([SBV a] -> cost) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])+maximize = optimize (.>=)++-- | Minimizes a cost function with respect to a constraint. Examples:+--+--   >>> minimize sum 3 (bAll (.> (10 :: SInteger)))+--   Just [11,11,11]+--+--   >>> minimize sum 3 (bAll (.< (10 :: SInteger)))+--   Nothing+minimize :: (SatModel a, SymWord a, OrdSymbolic cost) => ([SBV a] -> cost) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])+minimize = optimize (.<=)
Data/SBV/BitVectors/Polynomial.hs view
@@ -128,19 +128,27 @@ -- | Multiply two polynomials and reduce by the third (concrete) irreducible, given by its coefficients. -- 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) = fromBitsLE $ genericTake sz $ r ++ repeat false+polyMult (x, y, red)+  | isInfPrec x+  = error $ "SBV.polyMult: Received infinite precision value: " ++ show x+  | True+  = fromBitsLE $ genericTake sz $ r ++ repeat false   where (_, r) = mdp ms rs         ms = genericTake (2*sz) $ mul (blastLE x) (blastLE y) [] ++ repeat false         rs = genericTake (2*sz) $ [if i `elem` red then true else false |  i <- [0 .. foldr max 0 red] ] ++ repeat false-        sz = sizeOf x+        sz = intSizeOf x         mul _  []     ps = ps         mul as (b:bs) ps = mul (false:as) bs (ites b (as `addPoly` ps) ps)  polyDivMod :: (Bits a, SymWord a, FromBits (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a)-polyDivMod x y = ite (y .== 0) (0, x) (adjust d, adjust r)+polyDivMod x y+   | isInfPrec x+   = error $ "SBV.polyDivMod: Received infinite precision value: " ++ show x+   | True+   = ite (y .== 0) (0, x) (adjust d, adjust r)    where adjust xs = fromBitsLE $ genericTake sz $ xs ++ repeat false-         sz     = sizeOf x-         (d, r) = mdp (blastLE x) (blastLE y)+         sz        = intSizeOf x+         (d, r)    = mdp (blastLE x) (blastLE y)  -- conservative over-approximation of the degree degree :: [SBool] -> Int@@ -222,5 +230,9 @@ -- | Compute CRC's over polynomials, i.e., symbolic words. The first -- '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 = fromBitsBE $ replicate (sz - n) false ++ crcBV n (blastBE m) (blastBE p)-  where sz = sizeOf p+crc n m p+  | isInfPrec m || isInfPrec p+  = error $ "SBV.crc: Received an infinite precision value: " ++ show (m, p)+  | True+  = fromBitsBE $ replicate (sz - n) false ++ crcBV n (blastBE m) (blastBE p)+  where sz = intSizeOf p
Data/SBV/BitVectors/PrettyNum.hs view
@@ -57,19 +57,25 @@   {hexS = shex True True (False,64); binS = sbin True True (False,64); hex = shex False False (False,64); bin = sbin False False (False,64);} instance PrettyNum Int64  where   {hexS = shex True True (True,64);  binS = sbin True True (True,64) ; hex = shex False False (True,64);  bin = sbin False False (True,64) ;}+instance PrettyNum Integer where+  {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)-  hexS cw               = shex True True (hasSign cw, sizeOf cw) (cwVal cw)+  hexS cw | cwIsBit cw   = hexS (cwToBool cw)+          | isInfPrec cw = shexI True True (cwVal cw)+          | True         = shex True True (hasSign cw, intSizeOf cw) (cwVal cw) -  binS cw | cwIsBit cw  = binS (cwToBool cw)-  binS cw               = sbin True True (hasSign cw, sizeOf cw) (cwVal cw)+  binS cw | cwIsBit cw   = binS (cwToBool cw)+          | isInfPrec cw = sbinI True True (cwVal cw)+          | True         = sbin True True (hasSign cw, intSizeOf cw) (cwVal cw)    hex cw | cwIsBit cw   = hexS (cwToBool cw)-  hex cw                = shex False False (hasSign cw, sizeOf cw) (cwVal cw)+         | isInfPrec cw = shexI False False (cwVal cw)+         | True         = shex False False (hasSign cw, intSizeOf cw) (cwVal cw)    bin cw | cwIsBit cw   = binS (cwToBool cw)-  bin cw                = sbin False False (hasSign cw, sizeOf cw) (cwVal cw)+         | isInfPrec cw = sbinI False False (cwVal cw)+         | True         = sbin False False (hasSign cw, intSizeOf cw) (cwVal cw)  instance (SymWord a, PrettyNum a) => PrettyNum (SBV a) where   hexS s = maybe (show s) (hexS :: a -> String) $ unliteral s@@ -77,25 +83,47 @@   hex  s = maybe (show s) (hex :: a -> String)  $ unliteral s   bin  s = maybe (show s) (bin :: a -> String)  $ unliteral s -shex :: (Integral a) => Bool -> Bool -> (Bool, Size) -> a -> String+shex :: (Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String shex shType shPre (signed, size) a  | a < 0  = "-" ++ pre ++ pad l (s16 (abs (fromIntegral a :: Integer)))  ++ t  | True- =  pre ++ pad l (s16 a) ++ t+ = pre ++ pad l (s16 a) ++ t  where t | shType = " :: " ++ (if signed then "Int" else "Word") ++ show size          | True   = ""        pre | shPre = "0x"            | True  = ""        l = (size + 3) `div` 4 -sbin :: (Integral a) => Bool -> Bool -> (Bool, Size) -> a -> String+shexI :: Bool -> Bool -> Integer -> String+shexI shType shPre a+ | a < 0+ = "-" ++ pre ++ s16 (abs a)  ++ t+ | True+ = pre ++ s16 a ++ t+ where t | shType = " :: Integer"+         | True   = ""+       pre | shPre = "0x"+           | True  = ""++sbin :: (Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String sbin shType shPre (signed,size) a  | a < 0  = "-" ++ pre ++ pad size (s2 (abs (fromIntegral a :: Integer)))  ++ t  | True- =  pre ++ pad size (s2 a) ++ t+ = pre ++ pad size (s2 a) ++ t  where t | shType = " :: " ++ (if signed then "Int" else "Word") ++ show size+         | True   = ""+       pre | shPre = "0b"+           | True  = ""++sbinI :: Bool -> Bool -> Integer -> String+sbinI shType shPre a+ | a < 0+ = "-" ++ pre ++ s2 (abs a) ++ t+ | True+ =  pre ++ s2 a ++ t+ where t | shType = " :: Integer"          | True   = ""        pre | shPre = "0b"            | True  = ""
Data/SBV/BitVectors/STree.hs view
@@ -61,9 +61,13 @@ -- | Construct the fully balanced initial tree using the given values mkSTree :: forall i e. HasSignAndSize i => [SBV e] -> STree i e mkSTree ivals-  | reqd /= given = error $ "SBV.STree.mkSTree: Required " ++ show reqd ++ " elements, received: " ++ show given-  | True          = go ivals-  where reqd = 2 ^ sizeOf (undefined :: i)+  | isInfPrec (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+  | True+  = go ivals+  where reqd = 2 ^ intSizeOf (undefined :: i)         given = length ivals         go []  = error "SBV.STree.mkSTree: Impossible happened, ran out of elements"         go [l] = SLeaf l
Data/SBV/BitVectors/SignCast.hs view
@@ -81,18 +81,18 @@ genericSign x   | Just c <- unliteral x = literal $ fromIntegral c   | True                  = SBV sgsz (Right (cache y))-     where sgsz@(_, sz) = (True, sizeOf x)+     where sgsz = (True, sizeOf x)            y st = do xsw <- sbvToSW st x-                     newExpr st sgsz (SBVApp (Extract (sz-1) 0) [xsw])+                     newExpr st sgsz (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@(_, sz) = (False, sizeOf x)+     where sgsz = (False, sizeOf x)            y st = do xsw <- sbvToSW st x-                     newExpr st sgsz (SBVApp (Extract (sz-1) 0) [xsw])+                     newExpr st sgsz (SBVApp (Extract (intSizeOf x-1) 0) [xsw])  -- symbolic instances instance SignCast SWord8 SInt8 where
Data/SBV/BitVectors/Splittable.hs view
@@ -64,52 +64,52 @@  cwSplit :: (SymWord a, Num a) => CW -> (SBV a, SBV a) cwSplit z = (literal x, literal y)-  where (x,y) = genSplit (sizeOf z `div` 2) (cwVal z)+  where (x,y) = genSplit (intSizeOf z `div` 2) (cwVal z)  cwJoin :: (SymWord a, Num a) => CW -> CW -> SBV a-cwJoin x y = literal (genJoin (sizeOf x) (cwVal x) (cwVal y))+cwJoin x y = literal (genJoin (intSizeOf x) (cwVal x) (cwVal y))  -- symbolic instances instance Splittable SWord64 SWord32 where   split (SBV _ (Left z)) = cwSplit z-  split z                = (SBV (False, 32) (Right (cache x)), SBV (False, 32) (Right (cache y)))+  split z                = (SBV (False, Size (Just 32)) (Right (cache x)), SBV (False, Size (Just 32)) (Right (cache y)))     where x st = do zsw <- sbvToSW st z-                    newExpr st (False, 32) (SBVApp (Extract 63 32) [zsw])+                    newExpr st (False, Size (Just 32)) (SBVApp (Extract 63 32) [zsw])           y st = do zsw <- sbvToSW st z-                    newExpr st (False, 32) (SBVApp (Extract 31  0) [zsw])+                    newExpr st (False, Size (Just 32)) (SBVApp (Extract 31  0) [zsw])   (SBV _ (Left a)) # (SBV _ (Left b)) = cwJoin a b-  a # b = SBV (False, 64) (Right (cache c))+  a # b = SBV (False, Size (Just 64)) (Right (cache c))     where c st = do asw <- sbvToSW st a                     bsw <- sbvToSW st b-                    newExpr st (False, 64) (SBVApp Join [asw, bsw])+                    newExpr st (False, Size (Just 64)) (SBVApp Join [asw, bsw])   extend b = 0 # b  instance Splittable SWord32 SWord16 where   split (SBV _ (Left z)) = cwSplit z-  split z                = (SBV (False, 16) (Right (cache x)), SBV (False, 16) (Right (cache y)))+  split z                = (SBV (False, Size (Just 16)) (Right (cache x)), SBV (False, Size (Just 16)) (Right (cache y)))     where x st = do zsw <- sbvToSW st z-                    newExpr st (False, 16) (SBVApp (Extract 31 16) [zsw])+                    newExpr st (False, Size (Just 16)) (SBVApp (Extract 31 16) [zsw])           y st = do zsw <- sbvToSW st z-                    newExpr st (False, 16) (SBVApp (Extract 15  0) [zsw])+                    newExpr st (False, Size (Just 16)) (SBVApp (Extract 15  0) [zsw])   (SBV _ (Left a)) # (SBV _ (Left b)) = cwJoin a b-  a # b = SBV (False, 32) (Right (cache c))+  a # b = SBV (False, Size (Just 32)) (Right (cache c))     where c st = do asw <- sbvToSW st a                     bsw <- sbvToSW st b-                    newExpr st (False, 32) (SBVApp Join [asw, bsw])+                    newExpr st (False, Size (Just 32)) (SBVApp Join [asw, bsw])   extend b = 0 # b  instance Splittable SWord16 SWord8 where   split (SBV _ (Left z)) = cwSplit z-  split z                = (SBV (False, 8) (Right (cache x)), SBV (False, 8) (Right (cache y)))+  split z                = (SBV (False, Size (Just 8)) (Right (cache x)), SBV (False, Size (Just 8)) (Right (cache y)))     where x st = do zsw <- sbvToSW st z-                    newExpr st (False, 8) (SBVApp (Extract 15 8) [zsw])+                    newExpr st (False, Size (Just 8)) (SBVApp (Extract 15 8) [zsw])           y st = do zsw <- sbvToSW st z-                    newExpr st (False, 8) (SBVApp (Extract  7 0) [zsw])+                    newExpr st (False, Size (Just 8)) (SBVApp (Extract  7 0) [zsw])   (SBV _ (Left a)) # (SBV _ (Left b)) = cwJoin a b-  a # b = SBV (False, 16) (Right (cache c))+  a # b = SBV (False, Size (Just 16)) (Right (cache c))     where c st = do asw <- sbvToSW st a                     bsw <- sbvToSW st b-                    newExpr st (False, 16) (SBVApp Join [asw, bsw])+                    newExpr st (False, Size (Just 16)) (SBVApp Join [asw, bsw])   extend b = 0 # b  -- | Unblasting a value from symbolic-bits. The bits can be given little-endian
Data/SBV/Compilers/C.hs view
@@ -14,16 +14,17 @@  module Data.SBV.Compilers.C(compileToC, compileToCLib, compileToC', compileToCLib') where -import Data.Char (isSpace)-import Data.List (nub)-import Data.Maybe (isJust)-import qualified Data.Foldable as F (toList)+import Control.DeepSeq               (rnf)+import Data.Char                     (isSpace)+import Data.List                     (nub)+import Data.Maybe                    (isJust, fromMaybe, isNothing)+import qualified Data.Foldable as F  (toList) import Text.PrettyPrint.HughesPJ-import System.FilePath (takeBaseName, replaceExtension)+import System.FilePath               (takeBaseName, replaceExtension) import System.Random  import Data.SBV.BitVectors.Data-import Data.SBV.BitVectors.PrettyNum(shex)+import Data.SBV.BitVectors.PrettyNum (shex) import Data.SBV.Compilers.CodeGen  ---------------------------------------------------------------------------@@ -81,22 +82,32 @@ die :: String -> a die msg = error $ "SBV->C: Unexpected: " ++ msg +-- Unbounded int+dieUnbounded :: a+dieUnbounded = error $    "SBV->C: Unbounded integers are not supported by the C compiler."+                     ++ "\nUse 'cgIntegerSize' to specify a fixed size for SInteger representation."+ -- Unsupported features, or features TBD tbd :: String -> a tbd msg = error $ "SBV->C: Not yet supported: " ++ msg  cgen :: CgConfig -> String -> CgState -> Result -> CgPgmBundle-cgen cfg nm st sbvProg = CgPgmBundle $ filt [ ("Makefile",  (CgMakefile flags, [genMake driver nm nmd flags]))-                                            , (nm  ++ ".h", (CgHeader [sig],   [genHeader nm [sig] extProtos]))-                                            , (nmd ++ ".c", (CgDriver,         genDriver randVals nm ins outs mbRet))-                                            , (nm  ++ ".c", (CgSource,         genCProg rtc nm sig sbvProg ins outs mbRet extDecls))-                                            ]-  where rtc      = cgRTC cfg+cgen cfg nm st sbvProg+   -- we rnf the sig to make sure any exceptions in type conversion pop-out early enough+   -- this is purely cosmetic, of course..+   = rnf (render sig) `seq` result+  where result = CgPgmBundle $ filt [ ("Makefile",  (CgMakefile flags, [genMake driver nm nmd flags]))+                                    , (nm  ++ ".h", (CgHeader [sig],   [genHeader nm [sig] extProtos]))+                                    , (nmd ++ ".c", (CgDriver,         genDriver mbISize randVals nm ins outs mbRet))+                                    , (nm  ++ ".c", (CgSource,         genCProg rtc mbISize nm sig sbvProg ins outs mbRet extDecls))+                                    ]+        rtc      = cgRTC cfg+        mbISize  = cgInteger cfg         randVals = cgDriverVals cfg         driver   = cgGenDriver cfg         filt xs  = if driver then xs else filter (not . isCgDriver . fst . snd) xs         nmd      = nm ++ "_driver"-        sig      = pprCFunHeader nm ins outs mbRet+        sig      = pprCFunHeader mbISize nm ins outs mbRet         ins      = cgInputs st         outs     = cgOutputs st         mbRet    = case cgReturns st of@@ -112,34 +123,39 @@                      xs -> vcat $ text "/* User given declarations: */" : map text xs ++ [text ""]         flags    = cgLDFlags st +cSizeOf :: Maybe Int -> HasSignAndSize a => a -> Int+cSizeOf mbIntSize x+  | not (isInfPrec x) = intSizeOf x+  | True              = fromMaybe dieUnbounded mbIntSize+ -- | 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 -- that takes return values as pointers to be updated.-pprCFunHeader :: String -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> Doc-pprCFunHeader fn ins outs mbRet = retType <+> text fn <> parens (fsep (punctuate comma (map mkParam ins ++ map mkPParam outs)))+pprCFunHeader :: Maybe Int -> String -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> Doc+pprCFunHeader mbISize fn ins outs mbRet = retType <+> text fn <> parens (fsep (punctuate comma (map (mkParam mbISize) ins ++ map (mkPParam mbISize) outs)))   where retType = case mbRet of                    Nothing -> text "void"-                   Just sw -> pprCWord False (hasSign sw, sizeOf sw)+                   Just sw -> pprCWord False (hasSign sw, cSizeOf mbISize sw) -mkParam, mkPParam :: (String, CgVal) -> Doc-mkParam  (n, CgAtomic sw)     = let sgsz = (hasSign sw, sizeOf sw) in pprCWord True  sgsz <+> text n-mkParam  (_, CgArray  [])     = die "mkParam: CgArray with no elements!"-mkParam  (n, CgArray  (sw:_)) = let sgsz = (hasSign sw, sizeOf sw) in pprCWord True  sgsz <+> text "*" <> text n-mkPParam (n, CgAtomic sw)     = let sgsz = (hasSign sw, sizeOf sw) in pprCWord False sgsz <+> text "*" <> text n-mkPParam (_, CgArray  [])     = die "mPkParam: CgArray with no elements!"-mkPParam (n, CgArray  (sw:_)) = let sgsz = (hasSign sw, sizeOf sw) in pprCWord False sgsz <+> text "*" <> text n+mkParam, mkPParam :: Maybe Int -> (String, CgVal) -> Doc+mkParam  mbISize (n, CgAtomic sw)     = let sgsz = (hasSign sw, cSizeOf mbISize sw) in pprCWord True  sgsz <+> text n+mkParam  _       (_, CgArray  [])     = die "mkParam: CgArray with no elements!"+mkParam  mbISize (n, CgArray  (sw:_)) = let sgsz = (hasSign sw, cSizeOf mbISize sw) in pprCWord True  sgsz <+> text "*" <> text n+mkPParam mbISize (n, CgAtomic sw)     = let sgsz = (hasSign sw, cSizeOf mbISize sw) in pprCWord False sgsz <+> text "*" <> text n+mkPParam _       (_, CgArray  [])     = die "mPkParam: CgArray with no elements!"+mkPParam mbISize (n, CgArray  (sw:_)) = let sgsz = (hasSign sw, cSizeOf mbISize sw) in pprCWord False sgsz <+> text "*" <> text n  -- | Renders as "const SWord8 s0", etc. the first parameter is the width of the typefield-declSW :: Int -> SW -> Doc-declSW w sw@(SW sgsz _) = text "const" <+> pad (showCType sgsz) <+> text (show sw)+declSW :: Maybe Int -> Int -> SW -> Doc+declSW mbISize w sw@(SW (sg, _) _) = text "const" <+> pad (showCType (sg, cSizeOf mbISize sw)) <+> text (show sw)   where pad s = text $ s ++ replicate (w - length s) ' '  -- | Renders as "s0", etc, or the corresponding constant-showSW :: [(SW, CW)] -> SW -> Doc-showSW consts sw+showSW :: Maybe Int -> [(SW, CW)] -> SW -> Doc+showSW mbISize consts sw   | sw == falseSW                 = text "0"   | sw == trueSW                  = text "1"-  | Just cw <- sw `lookup` consts = showConst cw+  | Just cw <- sw `lookup` consts = showConst mbISize cw   | True                          = text $ show sw  -- | Words as it would be defined in the standard header stdint.h@@ -185,8 +201,8 @@ mkConst i   (s, sz)     = die $ "Constant " ++ show i ++ " at type " ++ (if s then "SInt" else "SWord") ++ show sz  -- | Show a constant-showConst :: CW -> Doc-showConst cw = mkConst (cwVal cw) (hasSign cw, sizeOf cw)+showConst :: Maybe Int -> CW -> Doc+showConst mbISize cw = mkConst (cwVal cw) (hasSign cw, cSizeOf mbISize cw)  -- | Generate a makefile. The first argument is True if we have a driver. genMake :: Bool -> String -> String -> [String] -> Doc@@ -267,8 +283,8 @@ sepIf b = if b then text "" else empty  -- | Generate an example driver program-genDriver :: [Integer] -> String -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> [Doc]-genDriver randVals fn inps outs mbRet = [pre, header, body, post]+genDriver :: Maybe Int -> [Integer] -> String -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> [Doc]+genDriver mbISize randVals fn inps outs mbRet = [pre, header, body, post]  where pre    =  text "/* Example driver program for" <+> nm <> text ". */"               $$ text "/* Automatically generated by SBV. Edit as you see fit! */"               $$ text ""@@ -286,7 +302,7 @@                       $$ call                       $$ text ""                       $$ (case mbRet of-                              Just sw -> text "printf" <> parens (printQuotes (fcall <+> text "=" <+> specifier (hasSign sw, sizeOf sw) <> text "\\n")+                              Just sw -> text "printf" <> parens (printQuotes (fcall <+> text "=" <+> specifier (hasSign sw, cSizeOf mbISize sw) <> text "\\n")                                                                               <> comma <+> resultVar) <> semi                               Nothing -> text "printf" <> parens (printQuotes (fcall <+> text "->\\n")) <> semi)                       $$ vcat (map display outs)@@ -307,7 +323,7 @@           where l          = length sws                 (frs, srs) = splitAt l rs        mkRVal sw r = mkConst ival sgsz-         where sgsz@(sg, sz) = (hasSign sw, sizeOf sw)+         where sgsz@(sg, sz) = (hasSign sw, cSizeOf mbISize sw)                ival | r >= minVal && r <= maxVal = r                     | not sg                     = r `mod` (2^sz)                     | True                       = (r `mod` (2^sz)) - (2^(sz-1))@@ -320,27 +336,27 @@                                  | True   = expSz-1        mkInp (_,  _, CgAtomic{})         = empty  -- constant, no need to declare        mkInp (_,  n, CgArray [])         = die $ "Unsupported empty array value for " ++ show n-       mkInp (vs, n, CgArray sws@(sw:_)) =  pprCWord True (hasSign sw, sizeOf sw) <+> text n <> brackets (int (length sws)) <+> text "= {"+       mkInp (vs, n, CgArray sws@(sw:_)) =  pprCWord True (hasSign sw, cSizeOf mbISize sw) <+> text n <> brackets (int (length sws)) <+> text "= {"                                                       $$ nest 4 (fsep (punctuate comma (align vs)))                                                       $$ text "};"                                          $$ text ""                                          $$ text "printf" <> parens (printQuotes (text "Contents of input array" <+> text n <> text ":\\n")) <> semi                                          $$ display (n, CgArray sws)                                          $$ text ""-       mkOut (v, CgAtomic sw)            = let sgsz = (hasSign sw, sizeOf sw) in pprCWord False sgsz <+> text v <> semi+       mkOut (v, CgAtomic sw)            = let sgsz = (hasSign sw, cSizeOf mbISize sw) in pprCWord False sgsz <+> text v <> semi        mkOut (v, CgArray [])             = die $ "Unsupported empty array value for " ++ show v-       mkOut (v, CgArray sws@(sw:_))     = pprCWord False (hasSign sw, sizeOf sw) <+> text v <> brackets (int (length sws)) <> semi+       mkOut (v, CgArray sws@(sw:_))     = pprCWord False (hasSign sw, cSizeOf mbISize sw) <+> text v <> brackets (int (length sws)) <> semi        resultVar = text "__result"        call = case mbRet of                 Nothing -> fcall <> semi-                Just sw -> pprCWord True (hasSign sw, sizeOf sw) <+> resultVar <+> text "=" <+> fcall <> semi+                Just sw -> pprCWord True (hasSign sw, cSizeOf mbISize sw) <+> resultVar <+> text "=" <+> fcall <> semi        fcall = nm <> parens (fsep (punctuate comma (map mkCVal pairedInputs ++ map mkOVal outs)))        mkCVal ([v], _, CgAtomic{}) = v        mkCVal (vs,  n, CgAtomic{}) = die $ "Unexpected driver value computed for " ++ show n ++ render (hcat vs)        mkCVal (_,   n, CgArray{})  = text n        mkOVal (n, CgAtomic{})      = text "&" <> text n        mkOVal (n, CgArray{})       = text n-       display (n, CgAtomic sw)         = text "printf" <> parens (printQuotes (text " " <+> text n <+> text "=" <+> specifier (hasSign sw, sizeOf sw)+       display (n, CgAtomic sw)         = text "printf" <> parens (printQuotes (text " " <+> text n <+> text "=" <+> specifier (hasSign sw, cSizeOf mbISize sw)                                                                                 <> text "\\n") <> comma <+> text n) <> semi        display (n, CgArray [])         =  die $ "Unsupported empty array value for " ++ show n        display (n, CgArray sws@(sw:_)) =   text "int" <+> nctr <> semi@@ -350,11 +366,12 @@                   where nctr      = text n <> text "_ctr"                         entry     = text n <> text "[" <> nctr <> text "]"                         entrySpec = text n <> text "[%d]"-                        spec      = specifier (hasSign sw, sizeOf sw)+                        spec      = specifier (hasSign sw, cSizeOf mbISize sw)  -- | Generate the C program-genCProg :: Bool -> String -> Doc -> Result -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> Doc -> [Doc]-genCProg rtc fn proto (Result ins preConsts tbls arrs _ _ asgns _) inVars outVars mbRet extDecls+genCProg :: Bool -> Maybe Int -> String -> Doc -> Result -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> Doc -> [Doc]+genCProg rtc mbISize fn proto (Result hasInfPrec cgs ins preConsts tbls arrs _ _ asgns _) inVars outVars mbRet extDecls+  | isNothing mbISize && hasInfPrec = dieUnbounded   | not (null arrs)                 = tbd "User specified arrays"   | needsExistentials (map fst ins) = error "SBV->C: Cannot compile functions with existentially quantified variables."   | True                            = [pre, header, post]@@ -364,6 +381,7 @@               $$ text "#include <stdint.h>"        header = text "#include" <+> doubleQuotes (nm <> text ".h")        post   = text ""+             $$ vcat (map codeSeg cgs)              $$ extDecls              $$ proto              $$ text "{"@@ -378,7 +396,10 @@              $$ text ""        nm = text fn        assignments = F.toList asgns-       typeWidth = getMax 0 [len (hasSign s, sizeOf s) | (s, _) <- assignments]+       codeSeg (fnm, ls) =  text "/* User specified custom code for" <+> doubleQuotes (text fnm) <+> text "*/"+                         $$ vcat (map text ls)+                         $$ text ""+       typeWidth = getMax 0 [len (hasSign s, cSizeOf mbISize s) | (s, _) <- assignments]                 where len (False, 1) = 5 -- SBool                       len (False, n) = 5 + length (show n) -- SWordN                       len (True,  n) = 4 + length (show n) -- SIntN@@ -388,24 +409,28 @@        consts = (falseSW, falseCW) : (trueSW, trueCW) : preConsts        isConst s = isJust (lookup s consts)        genIO :: Bool -> (String, CgVal) -> [Doc]-       genIO True  (cNm, CgAtomic sw) = [declSW typeWidth sw  <+> text "=" <+> text cNm         <> semi]-       genIO False (cNm, CgAtomic sw) = [text "*" <> text cNm <+> text "=" <+> showSW consts sw <> semi]+       genIO True  (cNm, CgAtomic sw) = [declSW mbISize typeWidth sw  <+> text "=" <+> text cNm <> semi]+       genIO False (cNm, CgAtomic sw) = [text "*" <> text cNm <+> text "=" <+> showSW mbISize consts sw <> semi]        genIO isInp (cNm, CgArray sws) = zipWith genElt sws [(0::Int)..]          where genElt sw i-                 | isInp = declSW typeWidth sw <+> text "=" <+> text entry       <> semi-                 | True  = text entry          <+> text "=" <+> showSW consts sw <> semi+                 | isInp = declSW mbISize typeWidth sw <+> text "=" <+> text entry       <> semi+                 | True  = text entry                  <+> text "=" <+> showSW mbISize consts sw <> semi                  where entry = cNm ++ "[" ++ show i ++ "]"-       mkRet sw = text "return" <+> showSW consts sw <> semi-       genTbl :: ((Int, (Bool, Int), (Bool, Int)), [SW]) -> (Int, Doc)-       genTbl ((i, _, (sg, sz)), elts) =  (location, static <+> pprCWord True (sg, sz) <+> text ("table" ++ show i) <> text "[] = {"-                                                     $$ nest 4 (fsep (punctuate comma (align (map (showSW consts) elts))))+       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 static   = if location == -1 then text "static" else empty+         where szv = case (mbISize, sz) of+                       (_,       Size (Just v)) -> v+                       (Just is, Size Nothing)  -> is+                       _                        -> dieUnbounded+               static   = if location == -1 then text "static" else empty                location = maximum (-1 : map getNodeId elts)        getNodeId s@(SW _ (NodeId n)) | isConst s = -1                                      | True      = n        genAsgn :: (SW, SBVExpr) -> (Int, Doc)-       genAsgn (sw, n) = (getNodeId sw, declSW typeWidth sw <+> text "=" <+> ppExpr rtc consts n <> semi)+       genAsgn (sw, n) = (getNodeId sw, declSW mbISize typeWidth sw <+> text "=" <+> ppExpr mbISize rtc consts n <> semi)        -- merge tables intermixed with assignments, paying attention to putting tables as        -- early as possible.. Note that the assignment list (second argument) is sorted on its order        merge :: [(Int, Doc)] -> [(Int, Doc)] -> [Doc]@@ -415,8 +440,8 @@          | i < i'                                 = t : merge trest as          | True                                   = a : merge ts arest -ppExpr :: Bool -> [(SW, CW)] -> SBVExpr -> Doc-ppExpr rtc consts (SBVApp op opArgs) = p op (map (showSW consts) opArgs)+ppExpr :: Maybe Int -> Bool -> [(SW, CW)] -> SBVExpr -> Doc+ppExpr mbISize rtc consts (SBVApp op opArgs) = p op (map (showSW mbISize consts) opArgs)   where cBinOps = [ (Plus, "+"), (Times, "*"), (Minus, "-")                   , (Equal, "=="), (NotEqual, "!=")                   , (LessThan, "<"), (GreaterThan, ">"), (LessEq, "<="), (GreaterEq, ">=")@@ -426,28 +451,32 @@         p (ArrEq _ _)       _  = tbd "User specified arrays (ArrEq)"         p (Uninterpreted s) [] = text "/* Uninterpreted constant */" <+> text s         p (Uninterpreted s) as = text "/* Uninterpreted function */" <+> text s <> parens (fsep (punctuate comma as))-        p (Extract i j) [a]    = extract i j (let s = head opArgs in (hasSign s, sizeOf s)) a-        p Join [a, b]          = join (let (s1 : s2 : _) = opArgs in ((hasSign s1, sizeOf s1), (hasSign s2, sizeOf s2), a, b))-        p (Rol i) [a]          = rotate True  i a (let s = head opArgs in (hasSign s, sizeOf s))-        p (Ror i) [a]          = rotate False i a (let s = head opArgs in (hasSign s, sizeOf s))-        p (Shl i) [a]          = shift True  i a (let s = head opArgs in (hasSign s, sizeOf s))-        p (Shr i) [a]          = shift False i a (let s = head opArgs in (hasSign s, sizeOf s))+        p (Extract i j) [a]    = extract i j (let s = head opArgs in (hasSign s, cSizeOf mbISize s)) a+        p Join [a, b]          = join (let (s1 : s2 : _) = opArgs in ((hasSign s1, cSizeOf mbISize s1), (hasSign s2, cSizeOf mbISize s2), a, b))+        p (Rol i) [a]          = rotate True  i a (let s = head opArgs in (hasSign s, cSizeOf mbISize s))+        p (Ror i) [a]          = rotate False i a (let s = head opArgs in (hasSign s, cSizeOf mbISize s))+        p (Shl i) [a]          = shift True  i a (let s = head opArgs in (hasSign s, cSizeOf mbISize s))+        p (Shr i) [a]          = shift False i a (let s = head opArgs in (hasSign s, cSizeOf mbISize s))         p Not [a]           -- be careful about booleans, bitwise complement is not correct for them!           | s == 1           = parens (text "~" <> a) <+> text "&" <+> text "0x01U"           | True           = text "~" <> a-          where s = sizeOf (head opArgs)+          where s = cSizeOf mbISize (head opArgs)         p Ite [a, b, c] = a <+> text "?" <+> b <+> text ":" <+> c-        p (LkUp (t, (as, at), _, len) ind def) []+        p (LkUp (t, (as, sizeAT), _, 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 [index, defVal] = map (showSW consts) [ind, def]-                lkUp = text "table" <> int t <> brackets (showSW consts ind)+          where at = case (mbISize, sizeAT) of+                        (_,      Size (Just v)) -> v+                        (Just i, Size Nothing)  -> i+                        _                       -> dieUnbounded+                [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                 checkLeft  = index <+> text "< 0"                 checkRight = index <+> text ">=" <+> int len
Data/SBV/Compilers/CodeGen.hs view
@@ -33,13 +33,14 @@ -- | Options for code-generation. data CgConfig = CgConfig {           cgRTC        :: Bool          -- ^ If 'True', perform run-time-checks for index-out-of-bounds or shifting-by-large values etc.+        , cgInteger    :: Maybe Int     -- ^ Bit-size to use for representing SInteger (if any)         , cgDriverVals :: [Integer]     -- ^ Values to use for the driver program generated, useful for generating non-random drivers.         , cgGenDriver  :: Bool          -- ^ If 'True', will generate a driver program         }  -- | Default options for code generation. The run-time checks are turned-off, and the driver values are completely random. defaultCgConfig :: CgConfig-defaultCgConfig = CgConfig { cgRTC = False, cgDriverVals = [], cgGenDriver = True }+defaultCgConfig = CgConfig { cgRTC = False, cgInteger = Nothing, cgDriverVals = [], cgGenDriver = True }  -- | Abstraction of target language values data CgVal = CgAtomic SW@@ -84,6 +85,17 @@ cgPerformRTCs :: Bool -> SBVCodeGen () cgPerformRTCs b = modify (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgRTC = b } }) +-- | Sets number of bits to be used for representing the 'SInteger' type in the generated C code.+-- The argument must be one of @8@, @16@, @32@, or @64@. Note that this is essentially unsafe as+-- the semantics of unbounded Haskell integers becomes reduced to the corresponding bit size, as+-- typical in most C implementations.+cgIntegerSize :: Int -> SBVCodeGen ()+cgIntegerSize i+  | i `notElem` [8, 16, 32, 64]+  = error $ "SBV.cgIntegrerSize: Argument must be one of 8, 16, 32, or 64. Received: " ++ show i+  | True+  = modify (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgInteger = Just i }})+ -- | Should we generate a driver program? Default: 'True'. When a library is generated, then it will have -- a driver if any of the contituent functions has a driver. (See 'compileToCLib'.) cgGenerateDriver :: Bool -> SBVCodeGen ()@@ -178,7 +190,7 @@  codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen () -> IO CgPgmBundle codeGen l cgConfig nm (SBVCodeGen comp) = do-   (((), st'), res) <- runSymbolic' $ runStateT comp initCgState { cgFinalConfig = cgConfig }+   (((), st'), res) <- runSymbolic' True $ runStateT comp initCgState { cgFinalConfig = cgConfig }    let st = st' { cgInputs       = reverse (cgInputs st')                 , cgOutputs      = reverse (cgOutputs st')                 }
Data/SBV/Examples/BitPrecise/PrefixSum.hs view
@@ -234,6 +234,7 @@ -- TABLES -- ARRAYS -- UNINTERPRETED CONSTANTS+-- USER GIVEN CODE SEGMENTS -- AXIOMS -- DEFINE --   s8 :: SWord8 = s0 + s1@@ -280,6 +281,7 @@ -- TABLES -- ARRAYS -- UNINTERPRETED CONSTANTS+-- USER GIVEN CODE SEGMENTS -- AXIOMS -- DEFINE --   s8 :: SWord8 = s0 + s1
Data/SBV/Examples/CRC/CCITT.hs view
@@ -55,7 +55,7 @@ hw4 = do res <- allSat hw4has84Inhabitants          cnt <- displayModels disp res          putStrLn $ "Found: " ++ show cnt ++ " solution(s)."-   where disp :: Int -> (Word32, Word16, Word32, Word16) -> IO ()-         disp i (sh, sl, rh, rl) = do putStrLn $ "Solution #" ++ show i ++ ": "-                                      putStrLn $ "  Sent    : " ++ binS (mkFrame (literal sh, literal sl))-                                      putStrLn $ "  Received: " ++ binS (mkFrame (literal rh, literal rl))+   where disp :: Int -> (Bool, (Word32, Word16, Word32, Word16)) -> IO ()+         disp i (_, (sh, sl, rh, rl)) = do putStrLn $ "Solution #" ++ show i ++ ": "+                                           putStrLn $ "  Sent    : " ++ binS (mkFrame (literal sh, literal sl))+                                           putStrLn $ "  Received: " ++ binS (mkFrame (literal rh, literal rl))
+ Data/SBV/Examples/CodeGeneration/Uninterpreted.hs view
@@ -0,0 +1,58 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.Examples.CodeGeneration.Uninterpreted+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+-- Portability :  portable+--+-- Demonstrates the use of uninterpreted functions for the purposes of+-- code generation. This facility is important when we want to take+-- advantage of native libraries in the target platform, or when we'd+-- like to hand-generate code for certain functions for various+-- purposes, such as efficiency, or reliability.+-----------------------------------------------------------------------------++module Data.SBV.Examples.CodeGeneration.Uninterpreted where++import Data.SBV++-- | A definition of shiftLeft that can deal with variable length shifts.+-- (Note that the ``shiftL`` method from the 'Bits' class requires an 'Int' shift+-- amount.) Unfortunately, this'll generate rather clumsy C code due to the+-- use of tables etc., so we uninterpret it for code generation purposes+-- using the 'cgUninterpret' function.+shiftLeft :: SWord32 -> SWord32 -> SWord32+shiftLeft = cgUninterpret "SBV_SHIFTLEFT" cCode hCode+  where -- the C code we'd like SBV to spit out when generating code. Note that this is+        -- arbitrary C code. In this case we just used a macro, but it could be a function,+        -- text that includes files etc. It should essentially bring the name SBV_SHIFTLEFT+        -- used above into scope when compiled. If no code is needed, one can also just+        -- provide the empty list for the same effect. Also see 'cgAddDecl', 'cgAddLDFlags',+        -- and 'cgAddPrototype' functions for further variations.+        cCode = ["#define SBV_SHIFTLEFT(x, y) ((x) << (y))"]+        -- the Haskell code we'd like SBV to use when running inside Haskell or when+        -- translated to SMTLib for verification purposes. This is good old Haskell+        -- code, as one would typically write.+        hCode x y = select [x * literal (bit b) | b <- [0.. bitSize x - 1]] (literal 0) y++-- | Test function that uses shiftLeft defined above. When used as a normal Haskell function+-- or in verification the definition is fully used, i.e., no uninterpretation happens. To wit,+-- we have:+--+--  >>> tstShiftLeft 3 4 5+--  224 :: SWord32+--+--  >>> prove $ \x y -> tstShiftLeft x y 0 .== x + y+--  Q.E.D.+tstShiftLeft ::  SWord32 -> SWord32 -> SWord32 -> SWord32+tstShiftLeft x y z = x `shiftLeft` z + y `shiftLeft` z++-- | Generate C code for "tstShiftLeft". In this case, SBV will *use* the user given definition+-- verbatim, instead of generating code for it. (Also see the functions 'cgAddDecl', 'cgAddLDFlags',+-- and 'cgAddPrototype'.)+genCCode :: IO ()+genCCode = compileToC Nothing "tst" $ do+                [x, y, z] <- cgInputArr 3 "vs"+                cgReturn $ tstShiftLeft x y z
Data/SBV/Examples/Existentials/CRCPolynomial.hs view
@@ -75,8 +75,8 @@                         return $ bitValue p 0 &&& crcGood hd p s r                 cnt <- displayModels disp res                 putStrLn $ "Found: " ++ show cnt ++ " polynomail(s)."-        where disp :: Int -> Word16 -> IO ()-              disp n s = do putStrLn $ "Polynomial #" ++ show n ++ ". x^16 + " ++ showPolynomial False s+        where disp :: Int -> (Bool, Word16) -> IO ()+              disp n (_, s) = do putStrLn $ "Polynomial #" ++ show n ++ ". x^16 + " ++ showPolynomial False s  -- | Find and display all degree 16 polynomials with hamming distance at least 4, for 48 bit messages. --
Data/SBV/Examples/Puzzles/Counts.hs view
@@ -66,8 +66,8 @@ solve = 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+  where disp n (_, s) = do putStrLn $ "Solution #" ++ show n+                           dispSolution s         dispSolution :: [Word8] -> IO ()         dispSolution ns = putStrLn soln           where soln =  "In this sentence, the number of occurrences"
Data/SBV/Examples/Puzzles/Euler185.hs view
@@ -47,4 +47,4 @@ solve = do res <- allSat euler185            cnt <- displayModels disp res            putStrLn $ "Number of solutions: " ++ show cnt-   where disp _ ss = putStrLn $ concatMap show (ss :: [Word8])+   where disp _ (_, ss) = putStrLn $ concatMap show (ss :: [Word8])
Data/SBV/Examples/Puzzles/MagicSquare.hs view
@@ -62,7 +62,7 @@               cnt <- displayModels disp res               putStrLn $ "Found: " ++ show cnt ++ " solution(s)."    where n2 = n * n-         disp i model+         disp i (_, model)           | lmod /= n2           = error $ "Impossible! Backend solver returned " ++ show n ++ " values, was expecting: " ++ show lmod           | True
Data/SBV/Examples/Puzzles/NQueens.hs view
@@ -37,8 +37,8 @@               res <- allSat $ isValid n `fmap` mkExistVars n               cnt <- displayModels disp res               putStrLn $ "Found: " ++ show cnt ++ " solution(s)."-   where disp i s = do putStr $ "Solution #" ++ show i ++ ": "-                       dispSolution s+   where disp i (_, s) = do putStr $ "Solution #" ++ show i ++ ": "+                            dispSolution s          dispSolution :: [Word8] -> IO ()          dispSolution model            | lmod /= n = error $ "Impossible! Backend solver returned " ++ show lmod ++ " values, was expecting: " ++ show n
Data/SBV/Examples/Puzzles/PowerSet.hs view
@@ -28,7 +28,7 @@                  cnt <- displayModels disp res                  putStrLn $ "Found: " ++ show cnt ++ " subset(s)."      where n = length xs-           disp i ss+           disp i (_, ss)             | length ss /= n = error $ "Expected " ++ show n ++ " results; got: " ++ show (length ss)             | True           = putStrLn $ "Subset #" ++ show i ++ ": " ++ show (concat (zipWith pick ss xs))            pick True a  = [a]
Data/SBV/Examples/Puzzles/Sudoku.hs view
@@ -60,8 +60,8 @@                       Left m    -> putStrLn $ "Unsolvable puzzle: " ++ m  -- | Helper function to display results nicely, not really needed, but helps presentation-dispSolution :: Puzzle -> [Word8] -> IO ()-dispSolution (i, f) fs+dispSolution :: Puzzle -> (Bool, [Word8]) -> IO ()+dispSolution (i, f) (_, fs)   | lmod /= i = error $ "Impossible! Backend solver returned " ++ show lmod ++ " values, was expecting: " ++ show i   | True      = do putStrLn "Final board:"                    mapM_ printRow final
Data/SBV/Examples/Puzzles/Temperature.hs view
@@ -34,7 +34,7 @@ solve = do res <- allSat $ revOf `fmap` exists_            cnt <- displayModels disp res            putStrLn $ "Found " ++ show cnt ++ " solutions."-     where disp :: Int -> Word16 -> IO ()-           disp _ x = putStrLn $ " " ++ show x ++ "C --> " ++ show (round f :: Integer) ++ "F (exact value: " ++ show f ++ "F)"+     where disp :: Int -> (Bool, Word16) -> IO ()+           disp _ (_, x) = putStrLn $ " " ++ show x ++ "C --> " ++ show (round f :: Integer) ++ "F (exact value: " ++ show f ++ "F)"               where f :: Double                     f  = 32 + (9 * fromIntegral x) / 5
Data/SBV/Examples/Puzzles/U2Bridge.hs view
@@ -221,8 +221,8 @@                           else do putStrLn $ "Found: " ++ show cnt ++ " solution" ++ plu cnt ++ " with " ++ show n ++ " move" ++ plu n ++ "."                                   return True   where plu v = if v == 1 then "" else "s"-        disp :: Int -> [(Bool, U2Member, U2Member)] -> IO ()-        disp i ss+        disp :: Int -> (Bool, [(Bool, U2Member, U2Member)]) -> IO ()+        disp i (_, ss)          | lss /= n = error $ "Expected " ++ show n ++ " results; got: " ++ show lss          | True     = do putStrLn $ "Solution #" ++ show i ++ ": "                          go False 0 ss
Data/SBV/Internals.hs view
@@ -16,7 +16,7 @@    -- * Running symbolic programs /manually/     Result, runSymbolic     -- * Other internal structures useful for low-level programming-  , SBV(..), HasSignAndSize(..), CW, mkConstCW, genVar, genVar_+  , SBV(..), HasSignAndSize(..), CW, mkConstCW, genFinVar, genFinVar_   -- * Compilation to C   , compileToC', compileToCLib', CgPgmBundle(..), CgPgmKind(..)     -- * Integrating with the test framework@@ -25,7 +25,7 @@   ) where  import Data.SBV.BitVectors.Data   (Result, runSymbolic, SBV(..), HasSignAndSize(..), CW, mkConstCW)-import Data.SBV.BitVectors.Model  (genVar, genVar_)+import Data.SBV.BitVectors.Model  (genFinVar, genFinVar_) import Data.SBV.Compilers.C       (compileToC', compileToCLib') import Data.SBV.Compilers.CodeGen (CgPgmBundle(..), CgPgmKind(..)) import Data.SBV.Utils.SBVTest
Data/SBV/Provers/Prover.hs view
@@ -305,7 +305,7 @@         msg $ "Generated symbolic trace:\n" ++ show res         msg "Translating to SMT-Lib.."         case res of-          Result is consts tbls arrs uis axs pgm [o@(SW (False, 1) _)] | sizeOf o == 1 ->+          Result hasInfPrec _codeSegs is consts tbls arrs uis axs pgm [o@(SW (False, Size (Just 1)) _)] ->              timeIf isTiming "translation" $ do 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)@@ -315,8 +315,8 @@                                                                 where go []                   (_,  sofar) = reverse sofar                                                                       go ((ALL, (v, _)):rest) (us, sofar) = go rest (v:us, Left v : sofar)                                                                       go ((EX,  (v, _)):rest) (us, sofar) = go rest (us,   Right (v, reverse us) : sofar)-                                                return (is, uiMap, skolemMap, converter isSat comments is skolemMap consts tbls arrs uis axs pgm o)-          Result _is _consts _tbls _arrs _uis _axs _pgm os -> case length os of+                                                return (is, uiMap, skolemMap, converter hasInfPrec isSat comments is skolemMap consts tbls arrs uis axs pgm o)+          Result _hasInfPrec _codeSegs _is _consts _tbls _arrs _uis _axs _pgm os -> case length os of                         0  -> error $ "Impossible happened, unexpected non-outputting result\n" ++ show res                         1  -> error $ "Impossible happened, non-boolean output in " ++ show os                                     ++ "\nDetected while generating the trace:\n" ++ show res
Data/SBV/Provers/Z3.hs view
@@ -40,13 +40,15 @@                                 standardSolver cfg' script cleanErrs (ProofError cfg) (interpretSolverOutput cfg (extractMap isSat qinps modelMap . zipWith match skolemMap))          }  where -- This is quite crude and failure prone.. But is necessary to get z3 working through Wine on Mac+       -- TODO: get rid of this once there's a native Z3 release        cleanErrs = intercalate "\n" . filter (not . junk) . lines        junk "fixme:heap:HeapSetInformation 0x0 1 0x0 0" = True        junk s | "WARNING:" `isPrefixOf` s               = True        junk _                                           = False-       zero :: Int -> String-       zero 1  = "#b0"-       zero sz = "#x" ++ replicate (sz `div` 4) '0'+       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 ++ "))"@@ -90,5 +92,8 @@                                  matches -> error $  "SBV.SMTLib2: Cannot uniquely identify value for "                                                   ++ 's':v ++ " in "  ++ show matches         isInput _       = Nothing-        extract (S_App [S_App [S_Con v, S_Num i]]) | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (hasSign s, sizeOf s) i))]-        extract _                                                                 = []+        extract (S_App [S_App [S_Con v, S_Num i]])+                | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (hasSign s, sizeOf s) i))]+        extract (S_App [S_App [S_Con v, S_App [S_Con "-", S_Num i]]])+                | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (hasSign s, sizeOf s) (-i)))]+        extract _                              = []
Data/SBV/SMT/SMT.hs view
@@ -21,7 +21,7 @@ import Control.Monad      (when, zipWithM) import Data.Char          (isSpace) import Data.Int           (Int8, Int16, Int32, Int64)-import Data.List          (intercalate, isPrefixOf)+import Data.List          (intercalate, isPrefixOf, isInfixOf) import Data.Maybe         (isNothing, fromJust) import Data.Word          (Word8, Word16, Word32, Word64) import System.Directory   (findExecutable)@@ -160,33 +160,36 @@ genParse _ _ = Nothing  instance SatModel Bool where-  parseCWs xs = do (x,r) <- genParse (False,1) xs+  parseCWs xs = do (x,r) <- genParse (False, Size (Just 1)) xs                    return ((x :: Integer) /= 0, r)  instance SatModel Word8 where-  parseCWs = genParse (False,8)+  parseCWs = genParse (False, Size (Just 8))  instance SatModel Int8 where-  parseCWs = genParse (True,8)+  parseCWs = genParse (True, Size (Just 8))  instance SatModel Word16 where-  parseCWs = genParse (False,16)+  parseCWs = genParse (False, Size (Just 16))  instance SatModel Int16 where-  parseCWs = genParse (True,16)+  parseCWs = genParse (True, Size (Just 16))  instance SatModel Word32 where-  parseCWs = genParse (False,32)+  parseCWs = genParse (False, Size (Just 32))  instance SatModel Int32 where-  parseCWs = genParse (True,32)+  parseCWs = genParse (True, Size (Just 32))  instance SatModel Word64 where-  parseCWs = genParse (False,64)+  parseCWs = genParse (False, Size (Just 64))  instance SatModel Int64 where-  parseCWs = genParse (True,64)+  parseCWs = genParse (True, Size (Just 64)) +instance SatModel Integer where+  parseCWs = genParse (True, Size Nothing)+ -- when reading a list; go as long as we can (maximal-munch) -- note that this never fails.. instance SatModel a => SatModel [a] where@@ -228,20 +231,25 @@                    return ((a, b, c, d, e, f, g), hs)  -- | Given an 'SMTResult', extract an arbitrarily typed model from it, given a 'SatModel' instance-getModel :: SatModel a => SatResult -> Either String a-getModel (SatResult (Unsatisfiable _)) = Left "SatModel.getModel: Unsatisfiable result"-getModel (SatResult (Unknown _ _))     = error "Impossible! Backend solver returned unknown for Bit-vector problem!"+-- The first argument is "True" if this is an alleged model+getModel :: SatModel a => SatResult -> Either String (Bool, a)+getModel (SatResult (Unsatisfiable _)) = Left "SBV.getModel: Unsatisfiable result"+getModel (SatResult (Unknown _ m))     = Right (True, extractModel m) getModel (SatResult (ProofError _ s))  = error $ unlines $ "Backend solver complains: " : s getModel (SatResult (TimeOut _))       = Left "Timeout"-getModel (SatResult (Satisfiable _ m)) = case parseCWs [c | (_, c) <- modelAssocs m] of-                                           Just (x, []) -> Right x-                                           Just (_, ys) -> error $ "SBV.getModel: Partially constructed model; remaining elements: " ++ show ys-                                           Nothing      -> error $ "SBV.getModel: Cannot construct a model from: " ++ show m+getModel (SatResult (Satisfiable _ m)) = Right (False, extractModel m) +extractModel :: SatModel a => SMTModel -> a+extractModel m = case parseCWs [c | (_, c) <- modelAssocs m] of+                   Just (x, []) -> x+                   Just (_, ys) -> error $ "SBV.getModel: Partially constructed model; remaining elements: " ++ show ys+                   Nothing      -> error $ "SBV.getModel: Cannot construct a model from: " ++ show m+ -- | Given an 'allSat' call, we typically want to iterate over it and print the results in sequence. The -- 'displayModels' function automates this task by calling 'disp' on each result, consecutively. The first--- 'Int' argument to 'disp' 'is the current model number.-displayModels :: SatModel a => (Int -> a -> IO ()) -> AllSatResult -> IO Int+-- 'Int' argument to 'disp' 'is the current model number. The second argument is a tuple, where the first+-- element indicates whether the model is alleged (i.e., if the solver is not sure, returing Unknown)+displayModels :: SatModel a => (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int displayModels disp (AllSatResult (_, ms)) = do     inds <- zipWithM display [a | Right a <- map (getModel . SatResult) ms] [(1::Int)..]     return $ last (0:inds)@@ -358,11 +366,15 @@                                    hClose outh                                    hClose errh                                    ex <- waitForProcess pid-                                   return (ex, r ++ "\n" ++ out, err)+                                   -- if the status is unknown, prepare for the possibility of not having a model+                                   -- TBD: This is rather crude and potentially Z3 specific+                                   if "unknown" `isPrefixOf` r && "error" `isInfixOf` (out ++ err)+                                      then return (ExitSuccess, r               , "")+                                      else return (ex,          r ++ "\n" ++ out, err)                 return (send, ask, cleanUp)       mapM_ send (lines (scriptBody script))       r <- ask "(check-sat)"-      when ("sat" `isPrefixOf` r) $ do+      when (any (`isPrefixOf` r) ["sat", "unknown"]) $ do         let mls = lines (fromJust (scriptModel script))         when verb $ do putStrLn "** Sending the following model extraction commands:"                        mapM_ putStrLn mls
Data/SBV/SMT/SMTLib.hs view
@@ -17,12 +17,13 @@ import qualified Data.SBV.SMT.SMTLib1 as SMT1 import qualified Data.SBV.SMT.SMTLib2 as SMT2 -type SMTLibConverter =  Bool                                        -- ^ is this a sat problem?+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, Int), (Bool, Int)), [SW])]   -- ^ auto-generated tables+                     -> [((Int, (Bool, Size), (Bool, Size)), [SW])] -- ^ auto-generated tables                      -> [(Int, ArrayInfo)]                          -- ^ user specified arrays                      -> [(String, SBVType)]                         -- ^ uninterpreted functions/constants                      -> [(String, [String])]                        -- ^ user given axioms@@ -32,10 +33,10 @@  toSMTLib1, toSMTLib2 :: SMTLibConverter (toSMTLib1, toSMTLib2) = (cvt SMTLib1, cvt SMTLib2)-  where cvt v isSat comments qinps skolemMap consts tbls arrs uis axs asgnsSeq out = SMTLibPgm v (aliasTable, pre, post)+  where cvt v hasInfPrec isSat comments qinps skolemMap consts tbls arrs uis axs asgnsSeq 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 isSat comments qinps skolemMap consts tbls arrs uis axs asgnsSeq out+               (pre, post) = converter hasInfPrec isSat comments qinps skolemMap consts tbls arrs uis axs asgnsSeq out  addNonEqConstraints :: [(Quantifier, NamedSymVar)] -> [[(String, CW)]] -> SMTLibPgm -> Maybe String addNonEqConstraints _qinps cs p@(SMTLibPgm SMTLib1 _) = SMT1.addNonEqConstraints cs p
Data/SBV/SMT/SMTLib1.hs view
@@ -14,7 +14,8 @@ module Data.SBV.SMT.SMTLib1(cvt, addNonEqConstraints) where  import qualified Data.Foldable as F (toList)-import Data.List (intercalate)+import Data.List  (intercalate)+import Data.Maybe (fromMaybe)  import Data.SBV.BitVectors.Data @@ -38,19 +39,22 @@ nonEq :: (String, CW) -> String nonEq (s, c) = "(not (= " ++ s ++ " " ++ cvtCW c ++ "))" -cvt :: Bool                                        -- ^ is this a sat problem?+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, Int), (Bool, Int)), [SW])]   -- ^ auto-generated tables+    -> [((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                                          -- ^ output variable     -> ([String], [String])-cvt isSat comments qinps _skolemInps consts tbls arrs uis axs asgnsSeq out+cvt hasInf isSat comments qinps _skolemInps consts tbls arrs uis axs asgnsSeq out+  | hasInf+  = error "SBV: The chosen solver does not support infinite precision values. (Use z3 instead.)"   | not ((isSat && allExistential) || (not isSat && allUniversal))   = error "SBV: The chosen solver does not support quantified variables. (Use z3 instead.)"   | True@@ -94,15 +98,23 @@ -- 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, Int), (Bool, Int)), [SW]) -> [String]-mkTable ((i, (_, at), (_, rt)), elts) = (" :extrafuns ((" ++ t ++ " Array[" ++ show at ++ ":" ++ show rt ++ "]))") : zipWith mkElt elts [(0::Int)..]+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)..]   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) +-- 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, (_, ((_, at), (_, rt)), ctx)) = adecl : ctxInfo+declArray (i, (_, ((_, atSz), (_, rtSz)), 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)         ctxInfo = case ctx of                     ArrayFree Nothing   -> []                     ArrayFree (Just sw) -> declA sw@@ -127,7 +139,7 @@  -- SMTLib represents signed/unsigned quantities with the same type decl :: SW -> String-decl s = " :extrafuns  ((" ++ show s ++ " BitVec[" ++ show (sizeOf s) ++ "]))"+decl s = " :extrafuns  ((" ++ show s ++ " BitVec[" ++ show (intSizeOf s) ++ "]))"  cvtAsgn :: (SW, SBVExpr) -> String cvtAsgn (s, e) = " :assumption (= " ++ show s ++ " " ++ cvtExp e ++ ")"@@ -136,13 +148,13 @@ cvtCnst (s, c) = " :assumption (= " ++ show s ++ " " ++ cvtCW c ++ ")"  cvtCW :: CW -> String-cvtCW x | not (hasSign x) = "bv" ++ show (cwVal x) ++ "[" ++ show (sizeOf x) ++ "]"+cvtCW x | not (hasSign x) = "bv" ++ show (cwVal x) ++ "[" ++ 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 (sizeOf x)-  where least = negate (2 ^ sizeOf x)-cvtCW x = negIf (w < 0) $ "bv" ++ show (abs w) ++ "[" ++ show (sizeOf x) ++ "]"+cvtCW x | cwVal x == 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  negIf :: Bool -> String -> String@@ -169,10 +181,11 @@ 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, (_, at), _, l) i e) [])+cvtExp (SBVApp (LkUp (t, (_, atSz), _, l) i e) [])   | needsCheck = "(ite " ++ cond ++ show e ++ " " ++ lkUp ++ ")"   | True       = lkUp-  where needsCheck = (2::Integer)^at > fromIntegral l+  where at = fromMaybe (die "Unbounded integers") (unSize atSz)+        needsCheck = (2::Integer)^at > fromIntegral l         lkUp = "(select table" ++ show t ++ " " ++ show i ++ ")"         cond          | hasSign i = "(or " ++ le0 ++ " " ++ gtl ++ ") "@@ -222,4 +235,5 @@ cvtType :: SBVType -> String cvtType (SBVType []) = error "SBV.SMT.SMTLib1.cvtType: internal: received an empty type!" cvtType (SBVType xs) = unwords $ map sh xs-  where sh (_, s) = "BitVec[" ++ show s ++ "]"+  where sh (_, Size Nothing)  = die "unbounded Integer"+        sh (_, Size (Just s)) = "BitVec[" ++ show s ++ "]"
Data/SBV/SMT/SMTLib2.hs view
@@ -53,21 +53,24 @@ tbd :: String -> a tbd e = error $ "SBV.SMTLib2: Not-yet-supported: " ++ e -cvt :: Bool                                        -- ^ is this a sat problem?+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, Int), (Bool, Int)), [SW])]   -- ^ auto-generated tables+    -> [((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                                          -- ^ output variable     -> ([String], [String])-cvt isSat comments _inps skolemInps consts tbls arrs uis axs asgnsSeq out = (pre, [])+cvt hasInf isSat comments _inps skolemInps consts tbls arrs uis axs asgnsSeq out = (pre, [])   where -- the logic is an over-approaximation-        logic = qs ++ as ++ ufs+        logic+          | hasInf = ["; Has unbounded Integers; 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                     = ""                 as  | null arrs                = ""@@ -76,17 +79,17 @@                     | True                     = "UF"         pre  =  ["; Automatically generated by SBV. Do not edit."]              ++ map ("; " ++) comments-             ++ [ "(set-logic " ++ logic ++ "BV)"-                , "(set-option :produce-models true)"+             ++ logic+             ++ [ "(set-option :produce-models true)"                 , "; --- literal constants ---"                 ]              ++ map declConst consts              ++ [ "; --- skolem constants ---" ]-             ++ [ "(declare-fun " ++ show s ++ " " ++ smtFunType ss s ++ ")" | Right (s, ss) <- skolemInps]+             ++ [ "(declare-fun " ++ show s ++ " " ++ swFunType ss s ++ ")" | Right (s, ss) <- skolemInps]              ++ [ "; --- constant tables ---" ]              ++ concatMap constTable constTables              ++ [ "; --- skolemized tables ---" ]-             ++ map (skolemTable (unwords (map smtType foralls))) skolemTables+             ++ map (skolemTable (unwords (map swType foralls))) skolemTables              ++ [ "; --- arrays ---" ]              ++ concat arrayConstants              ++ [ "; --- uninterpreted constants ---" ]@@ -97,7 +100,7 @@              ++ [if null foralls                  then "(assert ; no quantifiers"                  else "(assert (forall (" ++ intercalate "\n                 "-                                             ["(" ++ show s ++ " " ++ smtType s ++ ")" | s <- foralls] ++ ")"]+                                             ["(" ++ show s ++ " " ++ swType s ++ ")" | s <- foralls] ++ ")"]              ++ map (letAlign . mkLet) asgns              ++ map letAlign (if null delayedEqualities then [] else ("(and " ++ deH) : map (align 5) deTs)              ++ [ impAlign (letAlign assertOut) ++ replicate noOfCloseParens ')' ]@@ -123,7 +126,7 @@                 mkSkTable    (((t, _, _), _), _) = (t, "table" ++ show t ++ forallArgs)         asgns = F.toList asgnsSeq         mkLet (s, e) = "(let ((" ++ show s ++ " " ++ cvtExp skolemMap tableMap e ++ "))"-        declConst (s, c) = "(define-fun " ++ show s ++ " " ++ smtFunType [] s ++ " " ++ cvtCW c ++ ")"+        declConst (s, c) = "(define-fun " ++ show s ++ " " ++ swFunType [] s ++ " " ++ cvtCW c ++ ")"  declUI :: (String, SBVType) -> [String] declUI (i, t) = ["(declare-fun uninterpreted_" ++ i ++ " " ++ cvtType t ++ ")"]@@ -132,22 +135,20 @@ declAx :: (String, [String]) -> String declAx (nm, ls) = (";; -- user given axiom: " ++ nm ++ "\n   ") ++ intercalate "\n" ls -constTable :: (((Int, (Bool, Int), (Bool, Int)), [SW]), [String]) -> [String]-constTable (((i, (_, at), (_, rt)), _elts), is) = decl : map wrap is+constTable :: (((Int, (Bool, Size), (Bool, Size)), [SW]), [String]) -> [String]+constTable (((i, (_, atSz), (_, rtSz)), _elts), is) = decl : map wrap is   where t       = "table" ++ show i-        bv sz   = "(_ BitVec " ++ show sz ++ ")"-        decl    = "(declare-fun " ++ t ++ " (" ++ bv at ++ ") " ++ bv rt ++ ")"+        decl    = "(declare-fun " ++ t ++ " (" ++ smtType atSz ++ ") " ++ smtType rtSz ++ ")"         wrap  s = "(assert " ++ s ++ ")" -skolemTable :: String -> (((Int, (Bool, Int), (Bool, Int)), [SW]), [String]) -> String-skolemTable qs (((i, (_, at), (_, rt)), _elts), _) = decl+skolemTable :: String -> (((Int, (Bool, Size), (Bool, Size)), [SW]), [String]) -> String+skolemTable qs (((i, (_, atSz), (_, rtSz)), _elts), _) = decl   where t         = "table" ++ show i-        bv sz     = "(_ BitVec " ++ show sz ++ ")"-        decl      = "(declare-fun " ++ t ++ " (" ++ qs ++ " " ++ bv at ++ ") " ++ bv rt ++ ")"+        decl      = "(declare-fun " ++ t ++ " (" ++ qs ++ " " ++ smtType atSz ++ ") " ++ smtType rtSz ++ ")"  -- Left if all constants, Right if otherwise-genTableData :: SkolemMap -> (Bool, String) -> [SW] -> ((Int, (Bool, Int), (Bool, Int)), [SW]) -> Either [String] [String]-genTableData skolemMap (quantified, args) consts ((i, (sa, at), (_, _rt)), elts)+genTableData :: SkolemMap -> (Bool, String) -> [SW] -> ((Int, (Bool, Size), (Bool, Size)), [SW]) -> Either [String] [String]+genTableData skolemMap (_quantified, args) consts ((i, (sa, at), (_, _rt)), elts)   | null post = Left  (map (topLevel . snd) pre)   | True      = Right (map (nested   . snd) (pre ++ post))   where ssw = cvtSW skolemMap@@ -155,7 +156,7 @@         t           = "table" ++ show i         mkElt x k   = (isReady, (idx, ssw x))           where idx = cvtCW (mkConstCW (sa, at) k)-                isReady = not quantified || x `elem` consts+                isReady = x `elem` consts         topLevel (idx, v) = "(= (" ++ t ++ " " ++ idx ++ ") " ++ v ++ ")"         nested   (idx, v) = "(= (" ++ t ++ args ++ " " ++ idx ++ ") " ++ v ++ ")" @@ -164,7 +165,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, (_, ((_, at), (_, rt)), ctx)) = (adecl : map wrap pre, map snd post)+declArray quantified consts skolemMap (i, (_, ((_, atSz), (_, rtSz)), ctx)) = (adecl : map wrap pre, map snd post)   where topLevel = not quantified || case ctx of                                        ArrayFree Nothing -> True                                        ArrayFree (Just sw) -> sw `elem` consts@@ -178,7 +179,7 @@          = cvtSW skolemMap sw          | True          = tbd "Non-constant array initializer in a quantified context"-        adecl = "(declare-fun " ++ nm ++ "() (Array (_ BitVec " ++ show at ++ ") (_ BitVec " ++ show rt ++ ")))"+        adecl = "(declare-fun " ++ nm ++ "() (Array " ++ smtType atSz ++ " " ++ smtType rtSz ++ "))"         ctxInfo = case ctx of                     ArrayFree Nothing   -> []                     ArrayFree (Just sw) -> declA sw@@ -186,23 +187,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 ++ "() (_ BitVec " ++ show at ++ "))")+                   in [ (True,             "(declare-fun " ++ iv ++ "() " ++ smtType atSz ++ ")")                       , (sw `elem` consts, "(= (select " ++ nm ++ " " ++ iv ++ ") " ++ ssw sw ++ ")")                       ]         wrap (False, s) = s         wrap (True, s)  = "(assert " ++ s ++ ")" -smtType :: SW -> String-smtType s = "(_ BitVec " ++ show (sizeOf s) ++ ")"+swType :: SW -> String+swType s = smtType (sizeOf s) -smtFunType :: [SW] -> SW -> String-smtFunType ss s = "(" ++ unwords (map smtType ss) ++ ") " ++ smtType 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 ++ ")"+ cvtType :: SBVType -> String cvtType (SBVType []) = error "SBV.SMT.SMTLib2.cvtType: internal: received an empty type!"-cvtType (SBVType xs) = "(" ++ unwords (map sh body) ++ ") " ++ sh ret-  where (body, ret) = (init xs, last xs)-        sh (_, s)   = "(_ BitVec " ++ show s ++ ")"+cvtType (SBVType xs) = "(" ++ unwords (map smtType body) ++ ") " ++ smtType ret+  where szs         = map snd xs+        (body, ret) = (init szs, last szs)  type SkolemMap = M.Map  SW [SW] type TableMap  = IM.IntMap String@@ -221,13 +226,15 @@   where pad n s = replicate (n - length s) '0' ++ s  cvtCW :: CW -> String-cvtCW x | not (hasSign x) = hex (sizeOf x) (cwVal x)+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) -- 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 (sizeOf x)-  where least = negate (2 ^ sizeOf x)-cvtCW x = negIf (w < 0) $ hex (sizeOf x) (abs w)+cvtCW x | cwVal x == least = mkMinBound (intSizeOf x)+  where least = negate (2 ^ intSizeOf x)+cvtCW x = negIf (w < 0) $ hex (intSizeOf x) (abs w)   where w = cwVal x  negIf :: Bool -> String -> String@@ -244,63 +251,92 @@   | 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 = sh expr+cvtExp skolemMap tableMap expr@(SBVApp _ arguments) = sh expr   where ssw = cvtSW skolemMap+        hasInfPrecArgs = any isInfPrec arguments+        ensureBV       = not hasInfPrecArgs || unbounded expr+        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+          | sgn+          = "(ite " ++ lift2 oS sgn sbvs ++ " #b1 #b0)"+          | True+          = "(ite " ++ lift2 oU sgn sbvs ++ " #b1 #b0)"+        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)+        -- Group 1: Same translation, regardless BV/Int         sh (SBVApp Ite [a, b, c]) = "(ite (= #b1 " ++ ssw a ++ ") " ++ ssw b ++ " " ++ ssw c ++ ")"-        sh (SBVApp (Rol i) [a])   = rot ssw "rotate_left"  i a-        sh (SBVApp (Ror i) [a])   = rot ssw "rotate_right" i a-        sh (SBVApp (Shl i) [a])   = shft ssw "bvshl"  "bvshl"  i a-        sh (SBVApp (Shr i) [a])   = shft ssw "bvlshr" "bvashr" i a-        sh (SBVApp (LkUp (t, (_, at), _, l) i e) [])+        sh (SBVApp (LkUp (t, (_, atSz), _, l) i e) [])           | needsCheck = "(ite " ++ cond ++ ssw e ++ " " ++ lkUp ++ ")"           | True       = lkUp-          where needsCheck = (2::Integer)^at > fromIntegral l+          where needsCheck = maybe True (\at -> (2::Integer)^at > fromIntegral l) (unSize atSz)                 lkUp = "(" ++ getTable tableMap t ++ " " ++ ssw i ++ ")"                 cond                  | hasSign i = "(or " ++ le0 ++ " " ++ gtl ++ ") "                  | True      = gtl ++ " "-                (less, leq) = if hasSign i then ("bvslt", "bvsle") else ("bvult", "bvule")+                (less, leq) = case atSz of+                                 Size Nothing -> ("<", "<=")+                                 _            -> if hasSign i then ("bvslt", "bvsle") else ("bvult", "bvule")                 mkCnst = cvtCW . mkConstCW (hasSign i, sizeOf i)                 le0  = "(" ++ less ++ " " ++ ssw i ++ " " ++ mkCnst 0 ++ ")"                 gtl  = "(" ++ leq  ++ " " ++ mkCnst l ++ " " ++ ssw i ++ ")"-        sh (SBVApp (Extract i j) [a]) = "((_ extract " ++ show i ++ " " ++ show j ++ ") " ++ ssw a ++ ")"         sh (SBVApp (ArrEq i j) []) = "(ite (= array_" ++ show i ++ " array_" ++ show j ++") #b1 #b0)"         sh (SBVApp (ArrRead i) [a]) = "(select array_" ++ show i ++ " " ++ ssw a ++ ")"         sh (SBVApp (Uninterpreted nm) [])   = "uninterpreted_" ++ nm         sh (SBVApp (Uninterpreted nm) args) = "(uninterpreted_" ++ nm ++ " " ++ unwords (map ssw args) ++ ")"+        -- Group 2: Only supported for BV+        sh (SBVApp (Rol i) [a])       | ensureBV = rot  ssw "rotate_left"  i a+        sh (SBVApp (Ror i) [a])       | ensureBV = rot  ssw "rotate_right" i a+        sh (SBVApp (Shl i) [a])       | ensureBV = shft ssw "bvshl"  "bvshl"  i a+        sh (SBVApp (Shr i) [a])       | ensureBV = shft ssw "bvlshr" "bvashr" i a+        sh (SBVApp (Extract i j) [a]) | ensureBV = "((_ extract " ++ show i ++ " " ++ show j ++ ") " ++ ssw a ++ ")"+        sh (SBVApp op args)+          | Just f <- lookup op smtBVOpTable, ensureBV+          = f (any hasSign args) (map ssw args)+          where smtBVOpTable = [ (And,  lift2 "bvand")+                               , (Or,   lift2 "bvor")+                               , (XOr,  lift2 "bvxor")+                               , (Not,  lift1 "bvnot")+                               , (Join, lift2 "concat")+                               ]         sh inp@(SBVApp op args)-          | Just f <- lookup op smtOpTable+          | hasInfPrecArgs+          = case lookup op smtOpIntTable of+              Just f -> f True (map ssw args)+              _      -> unbounded inp+          | Just f <- lookup op smtOpBVTable           = f (any hasSign args) (map ssw args)           | True-          = error $ "SBV.SMT.SMTLib2.sh: impossible happened; can't translate: " ++ show inp-          where 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-                  | sgn-                  = "(ite " ++ lift2 oS sgn sbvs ++ " #b1 #b0)"-                  | True-                  = "(ite " ++ lift2 oU sgn sbvs ++ " #b1 #b0)"-                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)-                smtOpTable = [ (Plus,          lift2   "bvadd")-                             , (Minus,         lift2   "bvsub")-                             , (Times,         lift2   "bvmul")-                             , (Quot,          lift2   "bvudiv")-                             , (Rem,           lift2   "bvurem")-                             , (Equal,         lift2   "bvcomp")-                             , (NotEqual,      lift2N  "bvcomp")-                             , (LessThan,      lift2B  "bvult" "bvslt")-                             , (GreaterThan,   lift2B  "bvugt" "bvsgt")-                             , (LessEq,        lift2B  "bvule" "bvsle")-                             , (GreaterEq,     lift2B  "bvuge" "bvsge")-                             , (And,           lift2   "bvand")-                             , (Or,            lift2   "bvor")-                             , (XOr,           lift2   "bvxor")-                             , (Not,           lift1   "bvnot")-                             , (Join,          lift2   "concat")-                             ]+          = error $ "SBV.SMT.SMTLib2.cvtExp.sh: impossible happened; can't translate: " ++ show inp+          where smtOpBVTable  = [ (Plus,          lift2   "bvadd")+                                , (Minus,         lift2   "bvsub")+                                , (Times,         lift2   "bvmul")+                                , (Quot,          lift2   "bvudiv")+                                , (Rem,           lift2   "bvurem")+                                , (Equal,         lift2   "bvcomp")+                                , (NotEqual,      lift2N  "bvcomp")+                                , (LessThan,      lift2B  "bvult" "bvslt")+                                , (GreaterThan,   lift2B  "bvugt" "bvsgt")+                                , (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  ">=" ">=")+                                ]  rot :: (SW -> String) -> String -> Int -> SW -> String rot ssw o c x = "((_ " ++ o ++ " " ++ show c ++ ") " ++ ssw x ++ ")"
+ Data/SBV/TestSuite/CodeGeneration/Uninterpreted.hs view
@@ -0,0 +1,26 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.TestSuite.CodeGeneration.Uninterpreted+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+-- Portability :  portable+--+-- Test suite for Data.SBV.Examples.CodeGeneration.Uninterpreted+-----------------------------------------------------------------------------+module Data.SBV.TestSuite.CodeGeneration.Uninterpreted(testSuite) where++import Data.SBV+import Data.SBV.Internals+import Data.SBV.Examples.CodeGeneration.Uninterpreted++-- Test suite+testSuite :: SBVTestSuite+testSuite = mkTestSuite $ \goldCheck -> test [+   "cgUninterpret" ~: genC `goldCheck` "cgUninterpret.gold"+ ]+ where genC = compileToC' "tstShiftLeft" $ do+                  cgSetDriverValues [1, 2, 3]+                  [x, y, z] <- cgInputArr 3 "vs"+                  cgReturn $ tstShiftLeft x y z
README view
@@ -39,6 +39,7 @@   - `SBool`: Symbolic Booleans (bits)   - `SWord8`, `SWord16`, `SWord32`, `SWord64`: Symbolic Words (unsigned)   - `SInt8`,  `SInt16`,  `SInt32`,  `SInt64`: Symbolic Ints (signed)+  - `SInteger`: Symbolic unbounded integers (signed)   - Arrays of symbolic values   - Symbolic polynomials over GF(2^n ), polynomial arithmetic, and CRCs   - Uninterpreted constants and functions over symbolic values, with user@@ -50,11 +51,12 @@ 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. -Furthermore, predicates (i.e., functions that return `SBool`) built out of these types can also be:+Furthermore, functions built out of these types can also be:    - proven correct via an external SMT solver (the `prove` function)   - checked for satisfiability (the `sat`, and `allSat` functions)   - used in synthesis (the `sat` function with existentials)+  - optimized with respect to cost functions (the 'optimize', 'maximize', and 'minimize' functions)   - quick-checked  If a predicate is not valid, `prove` will return a counterexample: An
SBVUnitTest/GoldFiles/auf-1.gold view
@@ -12,6 +12,7 @@ ARRAYS UNINTERPRETED CONSTANTS   uninterpreted_f :: SWord32 -> SWord64+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s4 :: SWord32 = s0 + s3
SBVUnitTest/GoldFiles/basic-2_1.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s2 :: SWord8 = s0 + s1
SBVUnitTest/GoldFiles/basic-2_2.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s2 :: SWord8 = s0 * s0
SBVUnitTest/GoldFiles/basic-2_3.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s2 :: SWord8 = s0 + s1
SBVUnitTest/GoldFiles/basic-2_4.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s2 :: SWord8 = s0 + s1
SBVUnitTest/GoldFiles/basic-3_1.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s2 :: SWord8 = s0 + s1
SBVUnitTest/GoldFiles/basic-3_2.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s2 :: SWord8 = s0 * s0
SBVUnitTest/GoldFiles/basic-3_3.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s2 :: SWord8 = s0 + s1
SBVUnitTest/GoldFiles/basic-3_4.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s2 :: SWord8 = s0 + s1
SBVUnitTest/GoldFiles/basic-3_5.gold view
@@ -8,6 +8,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s3 :: SWord8 = s0 + s2
SBVUnitTest/GoldFiles/basic-4_1.gold view
@@ -6,6 +6,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s1 :: SWord8 = s0 + s0
SBVUnitTest/GoldFiles/basic-4_2.gold view
@@ -6,6 +6,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s1 :: SWord8 = s0 * s0
SBVUnitTest/GoldFiles/basic-4_3.gold view
@@ -6,6 +6,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s1 :: SWord8 = s0 + s0
SBVUnitTest/GoldFiles/basic-4_4.gold view
@@ -6,6 +6,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s1 :: SWord8 = s0 + s0
SBVUnitTest/GoldFiles/basic-4_5.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s2 :: SWord8 = s0 + s1
SBVUnitTest/GoldFiles/basic-5_1.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s2 :: SWord8 = s0 + s0
SBVUnitTest/GoldFiles/basic-5_2.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s2 :: SWord8 = s0 * s0
SBVUnitTest/GoldFiles/basic-5_3.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s2 :: SWord8 = s0 + s0
SBVUnitTest/GoldFiles/basic-5_4.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s2 :: SWord8 = s0 + s0
SBVUnitTest/GoldFiles/basic-5_5.gold view
@@ -8,6 +8,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s3 :: SWord8 = s0 + s2
SBVUnitTest/GoldFiles/ccitt.gold view
@@ -78,6 +78,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s4 :: SBool = s0 == s2
+ SBVUnitTest/GoldFiles/cgUninterpret.gold view
@@ -0,0 +1,105 @@+== BEGIN: "Makefile" ================+# Makefile for tstShiftLeft. 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: tstShiftLeft_driver++tstShiftLeft.o: tstShiftLeft.c tstShiftLeft.h+	${CC} ${CCFLAGS} -c $< -o $@++tstShiftLeft_driver.o: tstShiftLeft_driver.c+	${CC} ${CCFLAGS} -c $< -o $@++tstShiftLeft_driver: tstShiftLeft.o tstShiftLeft_driver.o+	${CC} ${CCFLAGS} $^ -o $@++clean:+	rm -f *.o++veryclean: clean+	rm -f tstShiftLeft_driver+== END: "Makefile" ==================+== BEGIN: "tstShiftLeft.h" ================+/* Header file for tstShiftLeft. Automatically generated by SBV. Do not edit! */++#ifndef __tstShiftLeft__HEADER_INCLUDED__+#define __tstShiftLeft__HEADER_INCLUDED__++#include <inttypes.h>+#include <stdint.h>++/* Unsigned bit-vectors */+typedef uint8_t  SBool  ;+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: */+SWord32 tstShiftLeft(const SWord32 *vs);++#endif /* __tstShiftLeft__HEADER_INCLUDED__ */+== END: "tstShiftLeft.h" ==================+== BEGIN: "tstShiftLeft_driver.c" ================+/* Example driver program for tstShiftLeft. */+/* Automatically generated by SBV. Edit as you see fit! */++#include <inttypes.h>+#include <stdint.h>+#include <stdio.h>+#include "tstShiftLeft.h"++int main(void)+{+  const SWord32 vs[3] = {+      0x00000001UL, 0x00000002UL, 0x00000003UL+  };+  +  printf("Contents of input array vs:\n");+  int vs_ctr;+  for(vs_ctr = 0; vs_ctr < 3 ; ++vs_ctr)+    printf("  vs[%d] = 0x%08"PRIx32"UL\n", vs_ctr ,vs[vs_ctr]);+  +  +  const SWord32 __result = tstShiftLeft(vs);+  +  printf("tstShiftLeft(vs) = 0x%08"PRIx32"UL\n", __result);++  return 0;+}+== END: "tstShiftLeft_driver.c" ==================+== BEGIN: "tstShiftLeft.c" ================+/* File: "tstShiftLeft.c". Automatically generated by SBV. Do not edit! */++#include <inttypes.h>+#include <stdint.h>+#include "tstShiftLeft.h"++/* User specified custom code for "SBV_SHIFTLEFT" */+#define SBV_SHIFTLEFT(x, y) ((x) << (y))++SWord32 tstShiftLeft(const SWord32 *vs)+{+  const SWord32 s0 = vs[0];+  const SWord32 s1 = vs[1];+  const SWord32 s2 = vs[2];+  const SWord32 s3 = /* Uninterpreted function */ SBV_SHIFTLEFT(s0,+                                                                s2);+  const SWord32 s4 = /* Uninterpreted function */ SBV_SHIFTLEFT(s1,+                                                                s2);+  const SWord32 s5 = s3 + s4;+  +  return s5;+}+== END: "tstShiftLeft.c" ==================
SBVUnitTest/GoldFiles/counts.gold view
@@ -27,6 +27,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s11 :: SBool = s9 < s10
SBVUnitTest/GoldFiles/crcPolyExist.gold view
@@ -63,6 +63,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s6 :: SWord16 = s0 & s5
SBVUnitTest/GoldFiles/legato.gold view
@@ -20,6 +20,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS AXIOMS DEFINE   s10 :: SBool = s0 /= s2
SBVUnitTest/GoldFiles/prefixSum_16.gold view
@@ -23,6 +23,7 @@ UNINTERPRETED CONSTANTS   uninterpreted_flOp :: SWord32 -> SWord32 -> SWord32   uninterpreted_u :: SWord32+USER GIVEN CODE SEGMENTS AXIOMS   -- user defined axiom: flOp is associative   :assumption (forall (?x BitVec[32]) (?y BitVec[32]) (?z BitVec[32])
SBVUnitTest/SBVUnitTest.hs view
@@ -51,6 +51,7 @@ import qualified Data.SBV.TestSuite.CodeGeneration.Fibonacci       as T05_04(testSuite) import qualified Data.SBV.TestSuite.CodeGeneration.GCD             as T05_05(testSuite) import qualified Data.SBV.TestSuite.CodeGeneration.PopulationCount as T05_06(testSuite)+import qualified Data.SBV.TestSuite.CodeGeneration.Uninterpreted   as T05_07(testSuite) import qualified Data.SBV.TestSuite.Crypto.AES                     as T06_01(testSuite) import qualified Data.SBV.TestSuite.Crypto.RC4                     as T06_02(testSuite) import qualified Data.SBV.TestSuite.Existentials.CRCPolynomial     as T07_01(testSuite)@@ -91,6 +92,7 @@      , ("fib",         T05_04.testSuite)      , ("gcd",         T05_05.testSuite)      , ("popCount",    T05_06.testSuite)+     , ("cgUninterp",  T05_07.testSuite)      , ("aes",         T06_01.testSuite)      , ("rc4",         T06_02.testSuite)      , ("existPoly",   T07_01.testSuite)@@ -112,7 +114,7 @@ -- No user serviceable parts below..  main :: IO ()-main = do putStrLn $ "*** SBVUnitTester, built: " ++ buildTime+main = do putStrLn $ "*** SBVUnitTester, version time stamp: " ++ buildTime           tgts <- getArgs           case tgts of             [x] | x `elem` ["-h", "--help", "-?"]
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -2,4 +2,4 @@ module SBVUnitTest.SBVUnitTestBuildTime (buildTime) where  buildTime :: String-buildTime = "Sun Nov 13 11:20:47 PST 2011"+buildTime = "Sun Dec  4 21:09:15 PST 2011"
sbv.cabal view
@@ -1,5 +1,5 @@ Name:          sbv-Version:       0.9.22+Version:       0.9.23 Category:      Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math Synopsis:      Symbolic bit vectors: Bit-precise verification and automatic C-code generation. Description:   Express properties about bit-precise Haskell programs and automatically prove@@ -23,6 +23,8 @@                .                  * 'SInt8',  'SInt16',  'SInt32',  'SInt64': Symbolic Ints (signed)                .+                 * 'SInteger': Symbolic unbounded integers (signed)+               .                  * 'SArray', 'SFunArray': Flat arrays of symbolic values                .                  * 'STree': Full binary trees of symbolic values (for fast symbolic access)@@ -32,17 +34,22 @@                  * Uninterpreted constants and functions over symbolic values, with user                    defined SMT-Lib axioms                .-               Predicates (i.e., functions that return 'SBool') built out of-               these types can be:+               Functions built out of these types can be:                .                  * proven correct via an external SMT solver (the 'prove' function)                .-                 * checked for satisfiability (the 'sat', 'allSat', and 'qbvf' functions)+                 * checked for satisfiability (the 'sat', and 'allSat' functions)                .-                 * used in synthesis (the 'qbvf' function)+                 * used in synthesis (the 'sat' function with existential variables)                .+                 * optimized with respect to cost functions (the 'optimize', 'maximize', and 'minimize' functions)+               .                  * quick-checked                .+               Predicates can have both existential and universal variables. Use of+               alternating quantifiers provides considerable expressive power.+               Furthermore, existential variables allow synthesis via model generation.+               .                The SBV library can also compile Haskell functions that manipulate symbolic                values directly to C, rendering them as straight-line C programs.                .@@ -101,6 +108,7 @@                   , Data.SBV.Examples.CodeGeneration.Fibonacci                   , Data.SBV.Examples.CodeGeneration.GCD                   , Data.SBV.Examples.CodeGeneration.PopulationCount+                  , Data.SBV.Examples.CodeGeneration.Uninterpreted                   , Data.SBV.Examples.Crypto.AES                   , Data.SBV.Examples.Crypto.RC4                   , Data.SBV.Examples.Existentials.CRCPolynomial@@ -116,6 +124,7 @@                   , Data.SBV.Examples.Uninterpreted.Function   Other-modules   : Data.SBV.BitVectors.Data                   , Data.SBV.BitVectors.Model+                  , Data.SBV.BitVectors.Optimize                   , Data.SBV.BitVectors.Polynomial                   , Data.SBV.BitVectors.PrettyNum                   , Data.SBV.BitVectors.SignCast@@ -165,6 +174,7 @@                   , Data.SBV.TestSuite.CodeGeneration.Fibonacci                   , Data.SBV.TestSuite.CodeGeneration.GCD                   , Data.SBV.TestSuite.CodeGeneration.PopulationCount+                  , Data.SBV.TestSuite.CodeGeneration.Uninterpreted                   , Data.SBV.TestSuite.Crypto.AES                   , Data.SBV.TestSuite.Crypto.RC4                   , Data.SBV.TestSuite.Existentials.CRCPolynomial