packages feed

sbv 0.9.24 → 1.0

raw patch · 50 files changed

+1572/−1072 lines, 50 files

Files

@@ -1,4 +1,4 @@-Copyright (c) 2010-2011, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2010-2012, Levent Erkok (erkokl@gmail.com) All rights reserved.  The sbv library is distributed with the BSD3 license. See the LICENSE file
Data/SBV.hs view
@@ -20,7 +20,7 @@ -- -- >>> prove $ forAll ["x"] $ \x -> x `shiftL` 2 .== (x :: SWord8) -- Falsifiable. Counter-example:---   x = 128 :: SWord8+--   x = 51 :: SWord8 -- -- The function 'prove' has the following type: --@@ -166,6 +166,9 @@   , minimize, maximize, optimize   , minimizeWith, maximizeWith, optimizeWith +  -- * Computing expected values+  , expectedValue, expectedValueWith+   -- * Model extraction   -- $modelExtraction @@ -175,7 +178,7 @@    -- ** Programmable model extraction   -- $programmableExtraction-  , SatModel(..), Modelable(..), displayModels+  , SatModel(..), Modelable(..), displayModels, extractModels    -- * SMT Interface: Configurations and solvers   , SMTConfig(..), OptimizeOpts(..), SMTSolver(..), yices, z3, defaultSMTCfg@@ -187,14 +190,14 @@   , compileToSMTLib    -- * Test case generation-  , genTest, CW(..), Size(..)+  , genTest, getTestValues, TestVectors, TestStyle(..), renderTest, CW(..), Size(..), cwToBool    -- * Code generation from symbolic programs   -- $cCodeGeneration   , SBVCodeGen    -- ** Setting code-generation options-  , cgPerformRTCs, cgSetDriverValues, cgGenerateDriver+  , cgPerformRTCs, cgSetDriverValues, cgGenerateDriver, cgGenerateMakefile    -- ** Designating inputs   , cgInput, cgInputArr@@ -220,17 +223,18 @@   ) where  import Data.SBV.BitVectors.Data-import Data.SBV.BitVectors.GenTest 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 import Data.SBV.BitVectors.Splittable import Data.SBV.BitVectors.STree import Data.SBV.Compilers.C import Data.SBV.Compilers.CodeGen import Data.SBV.Provers.Prover+import Data.SBV.Tools.GenTest+import Data.SBV.Tools.ExpectedValue+import Data.SBV.Tools.Optimize+import Data.SBV.Tools.Polynomial import Data.SBV.Utils.Boolean import Data.Bits import Data.Word@@ -423,15 +427,28 @@ A probabilistic constraint (see 'pConstrain') attaches a probability threshold for the constraint to be considered. For instance: -  @'pConstrain' 0.8 c@+  @+     'pConstrain' 0.8 c+  @ -will add the constraint @c@ 80% of the time. This variant is useful for 'genTest' and 'quickCheck' functions,-where we want to filter the test cases according to some probability distribution, to make sure that the test-vectors-are drawn from interesting subsets of the input space.+will make sure that the condition @c@ is satisfied 80% of the time (and correspondingly, falsified 20%+of the time), in expectation. This variant is useful for 'genTest' and 'quickCheck' functions, where we+want to filter the test cases according to some probability distribution, to make sure that the test-vectors+are drawn from interesting subsets of the input space. For instance, if we were to generate 100 test cases+with the above constraint, we'd expect about 80 of them to satisfy the condition @c@, while about 20 of them+will fail it. +The following properties hold:++  @+    'constrain'      = 'pConstrain' 1+    'pConstrain' t c = 'pConstrain' (1-t) (not c)+  @+ Note that while 'constrain' can be used freely, 'pConstrain' is only allowed in the contexts of-'genTest' or 'quickCheck'. Calls to 'pConstrain' in a prove/sat call will be rejected as it makes no sense.-Also, 'constrain' and 'pConstrain' calls during code-generation will also be rejected, for similar reasons.+'genTest' or 'quickCheck'. Calls to 'pConstrain' in a prove/sat call will be rejected as SBV does not+deal with probabilistic constraints when it comes to satisfiability and proofs.+Also, both 'constrain' and 'pConstrain' calls during code-generation will also be rejected, for similar reasons. -}  {-# ANN module "HLint: ignore Use import/export shortcut" #-}
Data/SBV/BitVectors/Data.hs view
@@ -22,7 +22,7 @@  ( SBool, SWord8, SWord16, SWord32, SWord64  , SInt8, SInt16, SInt32, SInt64, SInteger  , SymWord(..)- , CW(..), cwSameType, cwIsBit, cwToBool, constrain, pConstrain+ , CW(..), cwSameType, cwIsBit, cwToBool  , mkConstCW ,liftCW2, mapCW, mapCW2  , SW(..), trueSW, falseSW, trueCW, falseCW  , SBV(..), NodeId(..), mkSymSBV@@ -30,7 +30,8 @@  , sbvToSW, sbvToSymSW  , SBVExpr(..), newExpr  , cache, uncache, uncacheAI, HasSignAndSize(..)- , Op(..), NamedSymVar, UnintKind(..), getTableIndex, Pgm, Symbolic, runSymbolic, runSymbolic', State, inProofMode, SBVRunMode(..), Size(..), Outputtable(..), Result(..), getTraceInfo, getConstraints+ , Op(..), NamedSymVar, UnintKind(..), getTableIndex, Pgm, Symbolic, runSymbolic, runSymbolic', State, inProofMode, SBVRunMode(..), Size(..), Outputtable(..), Result(..)+ , getTraceInfo, getConstraints, addConstraint  , SBVType(..), newUninterpreted, unintFnUIKind, addAxiom  , Quantifier(..), needsExistentials  , SMTLibPgm(..), SMTLibVersion(..)@@ -72,6 +73,7 @@ cwIsBit :: CW -> Bool cwIsBit x = not (hasSign x) && not (isInfPrec x) && intSizeOf x == 1 +-- | Convert a CW to a Haskell boolean cwToBool :: CW -> Bool cwToBool x = cwVal x /= 0 @@ -357,11 +359,17 @@         external (ArrayMerge{})  = False  -- | Different means of running a symbolic piece of code-data SBVRunMode = Proof Bool  -- ^ Symbolic simulation mode, for proof purposes. Bool is True if it's a sat instance-                | CodeGen     -- ^ Code generation mode-                | Concrete    -- ^ Concrete simulation mode+data SBVRunMode = Proof Bool      -- ^ Symbolic simulation mode, for proof purposes. Bool is True if it's a sat instance+                | CodeGen         -- ^ Code generation mode+                | Concrete StdGen -- ^ Concrete simulation mode. The StdGen is for the pConstrain acceptance in cross runs +isConcreteMode :: SBVRunMode -> Bool+isConcreteMode (Concrete _) = True+isConcreteMode (Proof{})    = False+isConcreteMode CodeGen      = False+ data State  = State { runMode       :: SBVRunMode+                    , rStdGen       :: IORef StdGen                     , rCInfo        :: IORef [(String, CW)]                     , rctr          :: IORef Int                     , rInfPrec      :: IORef Bool@@ -382,9 +390,9 @@  inProofMode :: State -> Bool inProofMode s = case runMode s of-                  Proof{}  -> True-                  CodeGen  -> False-                  Concrete -> False+                  Proof{}    -> True+                  CodeGen    -> False+                  Concrete{} -> False  -- | The "Symbolic" value. Either a constant (@Left@) or a symbolic -- value (@Right Cached@). Note that caching is essential for making@@ -422,7 +430,7 @@ -- | Infinite precision signed symbolic value type SInteger = SBV Integer --- Needed to satisfy the Num hierarchy+-- Not particularly "desirable", but will do if needed instance Show (SBV a) where   show (SBV _                     (Left c))  = show c   show (SBV (_  , Size Nothing)   (Right _)) = "<symbolic> :: SInteger"@@ -446,6 +454,12 @@               i `seq` writeIORef (rctr s) i               return ctr +throwDice :: State -> IO Double+throwDice st = do g <- readIORef (rStdGen st)+                  let (r, g') = randomR (0, 1) g+                  writeIORef (rStdGen st) g'+                  return r+ newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO () newUninterpreted st nm t mbCode   | null nm || not (isAlpha (head nm)) || not (all validChar (tail nm))@@ -520,17 +534,17 @@         st <- ask         let q = case (mbQ, runMode st) of                   (Just x,  _)           -> x   -- user given, just take it-                  (Nothing, Concrete)    -> ALL -- concrete simulation, pick universal+                  (Nothing, Concrete{})  -> ALL -- concrete simulation, pick universal                   (Nothing, Proof True)  -> EX  -- sat mode, pick existential                   (Nothing, Proof False) -> ALL -- proof mode, pick universal                   (Nothing, CodeGen)     -> ALL -- code generation, pick universal         case runMode st of-          Concrete | q == EX -> case mbNm of-                                  Nothing -> error $ "Cannot quick-check in the presence of existential variables, type: " ++ showType (undefined :: SBV a)-                                  Just nm -> error $ "Cannot quick-check in the presence of existential variable " ++ nm ++ " :: " ++ showType (undefined :: SBV a)-          Concrete           -> do v@(SBV _ (Left cw)) <- liftIO randomIO-                                   liftIO $ modifyIORef (rCInfo st) ((maybe "_" id mbNm, cw):)-                                   return v+          Concrete _ | q == EX -> case mbNm of+                                    Nothing -> error $ "Cannot quick-check in the presence of existential variables, type: " ++ showType (undefined :: SBV a)+                                    Just nm -> error $ "Cannot quick-check in the presence of existential variable " ++ nm ++ " :: " ++ showType (undefined :: SBV a)+          Concrete _           -> do v@(SBV _ (Left cw)) <- liftIO randomIO+                                     liftIO $ modifyIORef (rCInfo st) ((maybe "_" id mbNm, cw):)+                                     return v           _          -> do ctr <- liftIO $ incCtr st                            let nm = maybe ('s':show ctr) id mbNm                                sw = SW sgnsz (NodeId ctr)@@ -560,6 +574,12 @@           liftIO $ modifyIORef (routs st) (sw:)           return i +instance Outputtable a => Outputtable [a] where+  output = mapM output++instance Outputtable () where+  output = return+ instance (Outputtable a, Outputtable b) => Outputtable (a, b) where   output = mlift2 (,) output output @@ -613,7 +633,11 @@    aiCache <- newIORef IMap.empty    infPrec <- newIORef False    cstrs   <- newIORef []+   rGen    <- case currentRunMode of+                Concrete g -> newIORef g+                _          -> newStdGen >>= newIORef    let st = State { runMode      = currentRunMode+                  , rStdGen      = rGen                   , rCInfo       = cInfo                   , rctr         = ctr                   , rInfPrec     = infPrec@@ -829,32 +853,27 @@ mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b mkSFunArray = SFunArray ------------------------------------------------------------------------------------- | Adding arbitrary constraints.-----------------------------------------------------------------------------------constrain :: SBool -> Symbolic ()-constrain c = do-        st <- ask-        liftIO $ do v <- sbvToSW st c-                    modifyIORef (rConstraints st) (v:) ------------------------------------------------------------------------------------- | Adding a probabilistic constraint. The 'Double' argument is the probability--- threshold. A threshold of '0' would mean the constraint is ignored, while a--- threshold of '1' means the constraint is always added. Probabilistic constraints--- are useful for 'genTest' and 'quickCheck' calls where we restrict our attention--- to /interesting/ parts of the input domain.-----------------------------------------------------------------------------------pConstrain :: Double -> SBool -> Symbolic ()-pConstrain t c+-- | Handling constraints+imposeConstraint :: SBool -> Symbolic ()+imposeConstraint c = do st <- ask+                        case runMode st of+                          CodeGen -> error "SBV: constraints are not allowed in code-generation"+                          _       -> do liftIO $ do v <- sbvToSW st c+                                                    modifyIORef (rConstraints st) (v:)++addConstraint :: Maybe Double -> SBool -> SBool -> Symbolic ()+addConstraint Nothing  c _  = imposeConstraint c+addConstraint (Just t) c c'   | t < 0 || t > 1   = error $ "SBV: pConstrain: Invalid probability threshold: " ++ show t ++ ", must be in [0, 1]."   | True   = do st <- ask-       case runMode st of-         Concrete -> when (t > 0) $ do r <- liftIO $ randomRIO (0, 1)-                                       when (r <= t) $ constrain c-         _        -> error "SBV: pConstrain only allowed in 'genTest' or 'quickCheck' contexts."+       when (not (isConcreteMode (runMode st))) $ error "SBV: pConstrain only allowed in 'genTest' or 'quickCheck' contexts."+       case () of+         () | t > 0 && t < 1 -> liftIO (throwDice st) >>= \d -> imposeConstraint (if d <= t then c else c')+            | t > 0          -> imposeConstraint c+            | True           -> imposeConstraint c'  --------------------------------------------------------------------------------- -- * Cached values
− Data/SBV/BitVectors/GenTest.hs 
@@ -1,37 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Data.SBV.BitVectors.GenTest--- Copyright   :  (c) Levent Erkok--- License     :  BSD3--- Maintainer  :  erkokl@gmail.com--- Stability   :  experimental--- Portability :  portable------ Test generation from symbolic programs--------------------------------------------------------------------------------module Data.SBV.BitVectors.GenTest (genTest) where--import Data.Maybe (fromMaybe)--import Data.SBV.BitVectors.Data---- | Generate a set of concrete test values from a symbolic program. The output--- can be rendered as test vectors in different languages as necessary. Use the--- function 'output' call to indicate what fields should be in the test result.--- (Also see 'constrain' and 'pConstrain' for filtering acceptable test values.)-genTest :: Int -> Symbolic () -> IO [([CW], [CW])]-genTest n m = gen 0 []-  where gen i sofar-         | i == n = return (reverse sofar)-         | True   = do mbT <- tc-                       case mbT of-                        Nothing -> gen i     sofar-                        Just t  -> gen (i+1) (t:sofar)-        tc = do (_, Result _ tvals _ _ cs _ _ _ _ _ cstrs os) <- runSymbolic' Concrete m-                let cval = fromMaybe (error "Cannot generate tests in the presence of uninterpeted constants!") . (`lookup` cs)-                    cond = all (cwToBool . cval) cstrs-                    io   = (map snd tvals, map cval os)-                if cond-                   then return $ Just io-                   else return Nothing
Data/SBV/BitVectors/Model.hs view
@@ -23,6 +23,7 @@     Mergeable(..), EqSymbolic(..), OrdSymbolic(..), BVDivisible(..), Uninterpreted(..)   , bitValue, setBitTo, allEqual, allDifferent, oneIf, blastBE, blastLE   , lsb, msb, SBVUF, sbvUFName, genFinVar, genFinVar_, forall, forall_, exists, exists_+  , constrain, pConstrain   )   where @@ -37,7 +38,7 @@  import Test.QuickCheck                           (Testable(..), Arbitrary(..)) import qualified Test.QuickCheck         as QC   (whenFail)-import qualified Test.QuickCheck.Monadic as QC   (monadicIO, run, pre)+import qualified Test.QuickCheck.Monadic as QC   (monadicIO, run) import System.Random  import Data.SBV.BitVectors.Data@@ -541,7 +542,7 @@ -- a concrete argument for obvious reasons. Other variants (succ, pred, [x..]) etc are similarly -- limited. While symbolic variants can be defined for many of these, they will just diverge -- as final sizes cannot be determined statically.-instance (Bounded a, Integral a, Num a, SymWord a) => Enum (SBV a) where+instance (Show a, Bounded a, Integral a, Num a, SymWord a) => Enum (SBV a) where   succ x     | v == (maxBound :: a) = error $ "Enum.succ{" ++ showType x ++ "}: tried to take `succ' of maxBound"     | True                 = fromIntegral $ v + 1@@ -735,9 +736,11 @@                       () | swt == falseSW -> sbvToSW st b                       () -> do swa <- sbvToSW st a                                swb <- sbvToSW st b-                               if swa == swb-                                  then return swa-                                  else newExpr st sgnsz (SBVApp Ite [swt, swa, swb])+                               case () of+                                 () | swa == swb                      -> return swa+                                 () | swa == trueSW && swb == falseSW -> return swt+                                 () | swa == falseSW && swa == trueSW -> newExpr st sgnsz (SBVApp Not [swt])+                                 ()                                   -> newExpr st sgnsz (SBVApp Ite [swt, swa, swb])   -- Custom version of select that translates to SMT-Lib tables at the base type of words   select xs err ind     | Just i <- unliteral ind@@ -1126,6 +1129,20 @@   sbvUninterpret mbCgData nm = let (h, f) = sbvUninterpret (uc7 `fmap` mbCgData) nm in (h, \(arg0, arg1, arg2, arg3, arg4, arg5, arg6) -> f arg0 arg1 arg2 arg3 arg4 arg5 arg6)     where uc7 (cs, fn) = (cs, \a b c d e f g -> fn (a, b, c, d, e, f, g)) +---------------------------------------------------------------------------------+-- | Adding arbitrary constraints.+---------------------------------------------------------------------------------+constrain :: SBool -> Symbolic ()+constrain c = addConstraint Nothing c (bnot c)++---------------------------------------------------------------------------------+-- | Adding a probabilistic constraint. The 'Double' argument is the probability+-- threshold. Probabilistic constraints are useful for 'genTest' and 'quickCheck'+-- calls where we restrict our attention to /interesting/ parts of the input domain.+---------------------------------------------------------------------------------+pConstrain :: Double -> SBool -> Symbolic ()+pConstrain t c = addConstraint (Just t) c (bnot c)+ -- Quickcheck interface on symbolic-booleans.. instance Testable SBool where   property (SBV _ (Left b)) = property (cwToBool b)@@ -1133,21 +1150,17 @@  instance Testable (Symbolic SBool) where   property m = QC.whenFail (putStrLn msg) $ QC.monadicIO test-    where test = do mbDie <- QC.run $ do-                                (r, Result _ tvals _ _ cs _ _ _ _ _ cstrs _) <- runSymbolic' Concrete m-                                let cval = fromMaybe (error "Cannot quick-check in the presence of uninterpeted constants!") . (`lookup` cs)-                                    cond = all (cwToBool . cval) cstrs-                                when (isSymbolic r) $ error $ "Cannot quick-check in the presence of uninterpreted constants! (" ++ show r ++ ")"-                                if cond-                                   then if r `isConcretely` id-                                           then return $ Just True-                                           else do putStrLn $ complain tvals-                                                   return Nothing-                                   else return $ Just False-                    case mbDie of-                      Just True  -> return ()           -- test successfull, continue-                      Just False -> QC.pre False        -- precondition failed, ignore-                      Nothing    -> fail "Falsifiable"  -- property failed, die+    where runOnce g = do (r, Result _ tvals _ _ cs _ _ _ _ _ cstrs _) <- runSymbolic' (Concrete g) m+                         let cval = fromMaybe (error "Cannot quick-check in the presence of uninterpeted constants!") . (`lookup` cs)+                             cond = all (cwToBool . cval) cstrs+                         when (isSymbolic r) $ error $ "Cannot quick-check in the presence of uninterpreted constants! (" ++ show r ++ ")"+                         if cond then if r `isConcretely` id+                                         then return False+                                         else do putStrLn $ complain tvals+                                                 return True+                                 else runOnce g -- cstrs failed, go again+          test = do die <- QC.run $ newStdGen >>= runOnce+                    when die $ fail "Falsifiable"           msg = "*** SBV: See the custom counter example reported above."           complain []     = "*** SBV Counter Example: Predicate contains no universally quantified variables."           complain qcInfo = intercalate "\n" $ "*** SBV Counter Example:" : map (("  " ++) . info) qcInfo
− Data/SBV/BitVectors/Optimize.hs 
@@ -1,108 +0,0 @@--------------------------------------------------------------------------------- |--- 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 (OptimizeOpts(..), optimize, optimizeWith, minimize, minimizeWith, maximize, maximizeWith) where--import Data.Maybe (fromJust)--import Data.SBV.BitVectors.Data-import Data.SBV.BitVectors.Model (OrdSymbolic(..), EqSymbolic(..))-import Data.SBV.Provers.Prover   (satWith, z3)-import Data.SBV.SMT.SMT          (SatModel, getModel, SMTConfig(..))-import Data.SBV.Utils.Boolean---- | Optimizer configuration. Note that iterative and quantified approaches are in general not interchangeable.--- For instance, iterative solutions will loop infinitely when there is no optimal value, but quantified solutions--- can handle such problems. Of course, quantified problems are harder for SMT solvers, naturally.-data OptimizeOpts = Iterative  Bool   -- ^ Iteratively search. if True, it will be reporting progress-                  | Quantified        -- ^ Use quantifiers---- | Symbolic optimization. Generalization on 'minimize' and 'maximize' that allows arbitrary--- cost functions and comparisons.-optimizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c)-             => SMTConfig                         -- ^ SMT configuration-             -> OptimizeOpts                      -- ^ Optimization options-             -> (SBV c -> SBV c -> SBool)         -- ^ comparator-             -> ([SBV a] -> SBV c)                -- ^ cost function-             -> Int                               -- ^ how many elements?-             -> ([SBV a] -> SBool)                -- ^ validity constraint-             -> IO (Maybe [a])-optimizeWith cfg (Iterative chatty) = iterOptimize chatty cfg-optimizeWith cfg Quantified         = quantOptimize cfg---- | Variant of 'optimizeWith' using z3-optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])-optimize = optimizeWith z3---- | Variant of 'maximize' allowing the use of a user specified solver.-maximizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])-maximizeWith cfg opts = optimizeWith cfg opts (.>=)---- | Maximizes a cost function with respect to a constraint. Examples:------   >>> maximize Quantified sum 3 (bAll (.< (10 :: SInteger)))---   Just [9,9,9]-maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])-maximize = maximizeWith z3---- | Variant of 'minimize' allowing the use of a user specified solver.-minimizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])-minimizeWith cfg opts = optimizeWith cfg opts (.<=)---- | Minimizes a cost function with respect to a constraint. Examples:------   >>> minimize Quantified sum 3 (bAll (.> (10 :: SInteger)))---   Just [11,11,11]-minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])-minimize = minimizeWith z3---- | Optimization using quantifiers-quantOptimize :: (SatModel a, SymWord a) => SMTConfig -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])-quantOptimize cfg cmp cost n valid = do-           m <- satWith cfg $ do xs <- mkExistVars  n-                                 ys <- mkForallVars n-                                 return $ valid xs &&& (valid ys ==> cost xs `cmp` cost ys)-           case getModel m of-              Right (True, _)  -> error "SBV: Backend solver reported \"unknown\""-              Right (False, a) -> return $ Just a-              Left _           -> return Nothing---- | Optimization using iteration-iterOptimize :: (SatModel a, Show a, SymWord a, Show c, SymWord c) =>  Bool -> SMTConfig -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])-iterOptimize chatty cfg cmp cost n valid = do-        msg "Trying to find a satisfying solution."-        m <- satWith cfg $ valid `fmap` mkExistVars n-        case getModel m of-          Left _ -> return Nothing-          Right (True, _)  -> error "SBV: Backend solver reported \"unknown\""-          Right (False, a) -> do msg $ "First solution found: " ++ show a-                                 let c = cost (map literal a)-                                 msg $ "Initial value is    : " ++ show (fromJust (unliteral c))-                                 msg "Starting iterative search."-                                 go (1::Int) a c-  where msg m | chatty = putStrLn $ "*** " ++ m-              | True   = return ()-        go i curSol curCost = do-                msg $ "Round " ++ show i ++ " ****************************"-                m <- satWith cfg $ do xs <- mkExistVars n-                                      return $ let c = cost xs in valid xs &&& (c `cmp` curCost &&& c ./= curCost)-                case getModel m of-                  Left _ -> do msg "The current solution is optimal. Terminating search."-                               return $ Just curSol-                  Right (True, _)  -> error "SBV: Backend solver reported \"unknown\""-                  Right (False, a) -> do msg $ "Solution: " ++ show a-                                         let c = cost (map literal a)-                                         msg $ "Value   : " ++ show (fromJust (unliteral c))-                                         go (i+1) a c
− Data/SBV/BitVectors/Polynomial.hs 
@@ -1,238 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Data.SBV.BitVectors.Polynomials--- Copyright   :  (c) Levent Erkok--- License     :  BSD3--- Maintainer  :  erkokl@gmail.com--- Stability   :  experimental--- Portability :  portable------ Implementation of polynomial arithmetic--------------------------------------------------------------------------------{-# LANGUAGE TypeSynonymInstances #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE PatternGuards #-}--module Data.SBV.BitVectors.Polynomial (Polynomial(..), crc, crcBV) where--import Data.Bits  (Bits(..))-import Data.List  (genericTake)-import Data.Maybe (fromJust)-import Data.Word  (Word8, Word16, Word32, Word64)--import Data.SBV.BitVectors.Data-import Data.SBV.BitVectors.Model-import Data.SBV.BitVectors.Splittable-import Data.SBV.Utils.Boolean---- | Implements polynomial addition, multiplication, division, and modulus operations--- over GF(2^n).  NB. Similar to 'bvQuotRem', division by @0@ is interpreted as follows:------     @x `pDivMod` 0 = (0, x)@------ for all @x@ (including @0@)------ Minimal complete definiton: 'pMult', 'pDivMod', 'showPolynomial'-class Bits a => Polynomial a where- -- | Given bit-positions to be set, create a polynomial- -- For instance- --- --     @polynomial [0, 1, 3] :: SWord8@- -- - -- will evaluate to @11@, since it sets the bits @0@, @1@, and @3@. Mathematicans would write this polynomial- -- as @x^3 + x + 1@. And in fact, 'showPoly' will show it like that.- polynomial :: [Int] -> a- -- | Add two polynomials in GF(2^n)- pAdd  :: a -> a -> a- -- | Multiply two polynomials in GF(2^n), and reduce it by the irreducible specified by- -- the polynomial as specified by coefficients of the third argument. Note that the third- -- argument is specifically left in this form as it is usally in GF(2^(n+1)), which is not available in our- -- formalism. (That is, we would need SWord9 for SWord8 multiplication, etc.) Also note that we do not- -- support symbolic irreducibles, which is a minor shortcoming. (Most GF's will come with fixed irreducibles,- -- so this should not be a problem in practice.)- --- -- Passing [] for the third argument will multiply the polynomials and then ignore the higher bits that won't- -- fit into the resulting size.- pMult :: (a, a, [Int]) -> a- -- | Divide two polynomials in GF(2^n), see above note for division by 0- pDiv  :: a -> a -> a- -- | Compute modulus of two polynomials in GF(2^n), see above note for modulus by 0- pMod  :: a -> a -> a- -- | Division and modulus packed together- pDivMod :: a -> a -> (a, a)- -- | Display a polynomial like a mathematician would (over the monomial @x@), with a type- showPoly :: a -> String- -- | Display a polynomial like a mathematician would (over the monomial @x@), the first argument- -- controls if the final type is shown as well.- showPolynomial :: Bool -> a -> String-- -- defaults.. Minumum complete definition: pMult, pDivMod, showPolynomial- polynomial = foldr (flip setBit) 0- pAdd       = xor- pDiv x y   = fst (pDivMod x y)- pMod x y   = snd (pDivMod x y)- showPoly   = showPolynomial False---instance Polynomial Word8   where {showPolynomial   = sp;           pMult = lift polyMult; pDivMod = liftC polyDivMod}-instance Polynomial Word16  where {showPolynomial   = sp;           pMult = lift polyMult; pDivMod = liftC polyDivMod}-instance Polynomial Word32  where {showPolynomial   = sp;           pMult = lift polyMult; pDivMod = liftC polyDivMod}-instance Polynomial Word64  where {showPolynomial   = sp;           pMult = lift polyMult; pDivMod = liftC polyDivMod}-instance Polynomial SWord8  where {showPolynomial b = liftS (sp b); pMult = polyMult;      pDivMod = polyDivMod}-instance Polynomial SWord16 where {showPolynomial b = liftS (sp b); pMult = polyMult;      pDivMod = polyDivMod}-instance Polynomial SWord32 where {showPolynomial b = liftS (sp b); pMult = polyMult;      pDivMod = polyDivMod}-instance Polynomial SWord64 where {showPolynomial b = liftS (sp b); pMult = polyMult;      pDivMod = polyDivMod}--lift :: SymWord a => ((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a-lift f (x, y, z) = fromJust $ unliteral $ f (literal x, literal y, z)-liftC :: SymWord a => (SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)-liftC f x y = let (a, b) = f (literal x) (literal y) in (fromJust (unliteral a), fromJust (unliteral b))-liftS :: SymWord a => (a -> String) -> SBV a -> String-liftS f s-  | Just x <- unliteral s = f x-  | True                  = show s---- | Pretty print as a polynomial-sp :: Bits a => Bool -> a -> String-sp st a- | null cs = '0' : t- | True    = foldr (\x y -> sh x ++ " + " ++ y) (sh (last cs)) (init cs) ++ t- where t | st   = " :: GF(2^" ++ show n ++ ")"-         | True = ""-       n  = bitSize a-       is = [n-1, n-2 .. 0]-       cs = map fst $ filter snd $ zip is (map (testBit a) is)-       sh 0 = "1"-       sh 1 = "x"-       sh i = "x^" ++ show i---- | Add two polynomials-addPoly :: [SBool] -> [SBool] -> [SBool]-addPoly xs    []      = xs-addPoly []    ys      = ys-addPoly (x:xs) (y:ys) = x <+> y : addPoly xs ys--ites :: SBool -> [SBool] -> [SBool] -> [SBool]-ites s xs ys- | Just t <- unliteral s- = if t then xs else ys- | True- = go xs ys- where go [] []         = []-       go []     (b:bs) = ite s false b : go [] bs-       go (a:as) []     = ite s a false : go as []-       go (a:as) (b:bs) = ite s a b : go as bs---- | 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)-  | 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 = 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-   | 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        = intSizeOf x-         (d, r)    = mdp (blastLE x) (blastLE y)---- conservative over-approximation of the degree-degree :: [SBool] -> Int-degree xs = walk (length xs - 1) $ reverse xs-  where walk n []     = n-        walk n (b:bs)-         | Just t <- unliteral b-         = if t then n else walk (n-1) bs-         | True-         = n -- over-estimate--mdp :: [SBool] -> [SBool] -> ([SBool], [SBool])-mdp xs ys = go (length ys - 1) (reverse ys)-  where degTop  = degree xs-        go _ []     = error "SBV.Polynomial.mdp: Impossible happened; exhausted ys before hitting 0"-        go n (b:bs)-         | n == 0   = (reverse qs, rs)-         | True     = let (rqs, rrs) = go (n-1) bs-                      in (ites b (reverse qs) rqs, ites b rs rrs)-         where degQuot = degTop - n-               ys' = replicate degQuot false ++ ys-               (qs, rs) = divx (degQuot+1) degTop xs ys'---- return the element at index i; if not enough elements, return false--- N.B. equivalent to '(xs ++ repeat false) !! i', but more efficient-idx :: [SBool] -> Int -> SBool-idx []     _ = false-idx (x:_)  0 = x-idx (_:xs) i = idx xs (i-1)--divx :: Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])-divx n _ xs _ | n <= 0 = ([], xs)-divx n i xs ys'        = (q:qs, rs)-  where q        = xs `idx` i-        xs'      = ites q (xs `addPoly` ys') xs-        (qs, rs) = divx (n-1) (i-1) xs' (tail ys')---- | Compute CRCs over bit-vectors. The call @crcBV n m p@ computes--- the CRC of the message @m@ with respect to polynomial @p@. The--- inputs are assumed to be blasted big-endian. The number--- @n@ specifies how many bits of CRC is needed. Note that @n@--- is actually the degree of the polynomial @p@, and thus it seems--- redundant to pass it in. However, in a typical proof context,--- the polynomial can be symbolic, so we cannot compute the degree--- easily. While this can be worked-around by generating code that--- accounts for all possible degrees, the resulting code would--- be unnecessarily big and complicated, and much harder to reason--- with. (Also note that a CRC is just the remainder from the--- polynomial division, but this routine is much faster in practice.)------ NB. The @n@th bit of the polynomial @p@ /must/ be set for the CRC--- to be computed correctly. Note that the polynomial argument 'p' will--- not even have this bit present most of the time, as it will typically--- contain bits @0@ through @n-1@ as usual in the CRC literature. The higher--- order @n@th bit is simply assumed to be set, as it does not make--- sense to use a polynomial of a lesser degree. This is usually not a problem--- since CRC polynomials are designed and expressed this way.------ NB. The literature on CRC's has many variants on how CRC's are computed.--- We follow the painless guide (<http://www.ross.net/crc/download/crc_v3.txt>)--- and compute the CRC as follows:------     * Extend the message 'm' by adding 'n' 0 bits on the right------     * Divide the polynomial thus obtained by the 'p'------     * The remainder is the CRC value.------ There are many variants on final XOR's, reversed polynomials etc., so--- it is essential to double check you use the correct /algorithm/.-crcBV :: Int -> [SBool] -> [SBool] -> [SBool]-crcBV n m p = take n $ go (replicate n false) (m ++ replicate n false)-  where mask = drop (length p - n) p-        go c []     = c-        go c (b:bs) = go next bs-          where c' = drop 1 c ++ [b]-                next = ite (head c) (zipWith (<+>) c' mask) c'---- | 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-  | 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
@@ -13,7 +13,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeSynonymInstances #-} -module Data.SBV.BitVectors.PrettyNum (PrettyNum(..), readBin, shex, sbin) where+module Data.SBV.BitVectors.PrettyNum (PrettyNum(..), readBin, shex, shexI, sbin, sbinI) where  import Data.Char  (ord) import Data.Int   (Int8, Int16, Int32, Int64)@@ -83,7 +83,7 @@   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, Int) -> a -> String+shex :: (Show a, 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@@ -106,7 +106,7 @@        pre | shPre = "0x"            | True  = "" -sbin :: (Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String+sbin :: (Show a, 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@@ -131,7 +131,7 @@ pad :: Int -> String -> String pad l s = replicate (l - length s) '0' ++ s -s2, s16 :: Integral a => a -> String+s2, s16 :: (Show a, Integral a) => a -> String s2  v = showIntAtBase 2 dig v "" where dig = fromJust . flip lookup [(0, '0'), (1, '1')] s16 v = showHex v ""
Data/SBV/Compilers/C.hs view
@@ -19,9 +19,9 @@ 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.Random+import Text.PrettyPrint.HughesPJ  import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.PrettyNum (shex)@@ -96,7 +96,7 @@    -- 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]))+  where result = CgPgmBundle $ filt [ ("Makefile",  (CgMakefile flags, [genMake (cgGenDriver cfg) 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))@@ -104,8 +104,10 @@         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+        filt xs  = [c | c@(_, (k, _)) <- xs, need k]+          where need k | isCgDriver   k = cgGenDriver cfg+                       | isCgMakefile k = cgGenMakefile cfg+                       | True           = True         nmd      = nm ++ "_driver"         sig      = pprCFunHeader mbISize nm ins outs mbRet         ins      = cgInputs st@@ -153,12 +155,12 @@ -- | Renders as "s0", etc, or the corresponding constant showSW :: Maybe Int -> [(SW, CW)] -> SW -> Doc showSW mbISize consts sw-  | sw == falseSW                 = text "0"-  | sw == trueSW                  = text "1"+  | sw == falseSW                 = text "false"+  | sw == trueSW                  = text "true"   | Just cw <- sw `lookup` consts = showConst mbISize cw   | True                          = text $ show sw --- | Words as it would be defined in the standard header stdint.h+-- | Words as it would map to a C word pprCWord :: Bool -> (Bool, Int) -> Doc pprCWord cnst sgsz = (if cnst then text "const" else empty) <+> text (showCType sgsz) @@ -188,7 +190,7 @@ --   Note that this automatically takes care of the boolean (1-bit) value problem, since it --   shows the result as an integer, which is OK as far as C is concerned. mkConst :: Integer -> (Bool, Int) -> Doc-mkConst i   (False,  1) = integer i+mkConst i   (False,  1) = text (if i == 0 then "false" else "true") mkConst i   (False,  8) = integer i mkConst i   (True,   8) = integer i mkConst i t@(False, 16) = text (shex False True t i) <> text "U"@@ -255,9 +257,12 @@   $$ text ""   $$ text "#include <inttypes.h>"   $$ text "#include <stdint.h>"+  $$ text "#include <stdbool.h>"   $$ text ""+  $$ text "/* The boolean type */"+  $$ text "typedef bool SBool;"+  $$ text ""   $$ text "/* Unsigned bit-vectors */"-  $$ text "typedef uint8_t  SBool  ;"   $$ text "typedef uint8_t  SWord8 ;"   $$ text "typedef uint16_t SWord16;"   $$ text "typedef uint32_t SWord32;"@@ -290,6 +295,7 @@               $$ text ""               $$ text "#include <inttypes.h>"               $$ text "#include <stdint.h>"+              $$ text "#include <stdbool.h>"               $$ text "#include <stdio.h>"        header =  text "#include" <+> doubleQuotes (nm <> text ".h")               $$ text ""@@ -380,6 +386,7 @@               $$ text ""               $$ text "#include <inttypes.h>"               $$ text "#include <stdint.h>"+              $$ text "#include <stdbool.h>"        header = text "#include" <+> doubleQuotes (nm <> text ".h")        post   = text ""              $$ vcat (map codeSeg cgs)@@ -461,7 +468,7 @@         p Not [a]           -- be careful about booleans, bitwise complement is not correct for them!           | s == 1-          = parens (text "~" <> a) <+> text "&" <+> text "0x01U"+          = text "!" <> a           | True           = text "~" <> a           where s = cSizeOf mbISize (head opArgs)@@ -555,9 +562,10 @@  -- | Merge a bunch of bundles to generate code for a library mergeToLib :: String -> [CgPgmBundle] -> CgPgmBundle-mergeToLib libName bundles = CgPgmBundle $ sources ++ libHeader : [libDriver | anyDriver] ++ [libMake]+mergeToLib libName bundles = CgPgmBundle $ sources ++ libHeader : [libDriver | anyDriver] ++ [libMake | anyMake]   where files       = concat [fs | CgPgmBundle fs <- bundles]         sigs        = concat [ss | (_, (CgHeader ss, _)) <- files]+        anyMake     = not (null [() | (_, (CgMakefile{}, _)) <- files])         drivers     = [ds | (_, (CgDriver, ds)) <- files]         anyDriver   = not (null drivers)         mkFlags     = nub (concat [xs | (_, (CgMakefile xs, _)) <- files])@@ -620,6 +628,7 @@             $$ text ""             $$ text "#include <inttypes.h>"             $$ text "#include <stdint.h>"+            $$ text "#include <stdbool.h>"             $$ text "#include <stdio.h>"             $$ inc         mkDFun (f, [_pre, _header, body, _post]) = [header, body, post]
Data/SBV/Compilers/CodeGen.hs view
@@ -17,11 +17,12 @@  import Control.Monad.Trans import Control.Monad.State.Lazy-import Data.Char (toLower)-import Data.List (nub, isPrefixOf, intercalate, (\\))-import System.Directory (createDirectory, doesDirectoryExist, doesFileExist)-import System.FilePath ((</>))-import Text.PrettyPrint.HughesPJ (Doc, render, vcat)+import Data.Char                 (toLower, isSpace)+import Data.List                 (nub, isPrefixOf, intercalate, (\\))+import System.Directory          (createDirectory, doesDirectoryExist, doesFileExist)+import System.FilePath           ((</>))+import Text.PrettyPrint.HughesPJ (Doc, vcat)+import qualified Text.PrettyPrint.HughesPJ as P (render)  import Data.SBV.BitVectors.Data @@ -32,15 +33,16 @@  -- | 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+          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+        , cgGenMakefile :: Bool          -- ^ If 'True', will generate a makefile         }  -- | 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, cgInteger = Nothing, cgDriverVals = [], cgGenDriver = True }+defaultCgConfig = CgConfig { cgRTC = False, cgInteger = Nothing, cgDriverVals = [], cgGenDriver = True, cgGenMakefile = True }  -- | Abstraction of target language values data CgVal = CgAtomic SW@@ -96,11 +98,15 @@   | 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+-- | Should we generate a driver program? Default: 'True'. When a library is generated, it will have -- a driver if any of the contituent functions has a driver. (See 'compileToCLib'.) cgGenerateDriver :: Bool -> SBVCodeGen () cgGenerateDriver b = modify (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgGenDriver = b } }) +-- | Should we generate a Makefile? Default: 'True'.+cgGenerateMakefile :: Bool -> SBVCodeGen ()+cgGenerateMakefile b = modify (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgGenMakefile = b } })+ -- | Sets driver program run time values, useful for generating programs with fixed drivers for testing. Default: None, i.e., use random values. cgSetDriverValues :: [Integer] -> SBVCodeGen () cgSetDriverValues vs = modify (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgDriverVals = vs } })@@ -180,12 +186,16 @@ isCgDriver CgDriver = True isCgDriver _        = False +isCgMakefile :: CgPgmKind -> Bool+isCgMakefile CgMakefile{} = True+isCgMakefile _            = False+ instance Show CgPgmBundle where    show (CgPgmBundle fs) = intercalate "\n" $ map showFile fs  showFile :: (FilePath, (CgPgmKind, [Doc])) -> String showFile (f, (_, ds)) =  "== BEGIN: " ++ show f ++ " ================\n"-                      ++ render (vcat ds)+                      ++ render' (vcat ds)                       ++ "== END: " ++ show f ++ " =================="  codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen () -> IO CgPgmBundle@@ -219,4 +229,10 @@                 else putStrLn "Aborting."   where renderFile (f, (_, ds)) = do let fn = dirName </> f                                      putStrLn $ "Generating: " ++ show fn ++ ".."-                                     writeFile fn (render (vcat ds))+                                     writeFile fn (render' (vcat ds))++-- Pretty's render might have "leading" white-space in empty lines, eliminate:+render' :: Doc -> String+render' = unlines . map clean . lines . P.render+  where clean x | all isSpace x = ""+                | True          = x
Data/SBV/Examples/BitPrecise/Legato.hs view
@@ -283,7 +283,7 @@  -- | The correctness theorem. --   On a decent MacBook Pro, this proof takes about 3 minutes with the 'SFunArray' memory model---   and about 30 minutes with the 'SArray' model.+--   and about 30 minutes with the 'SArray' model, using yices as the SMT solver correctnessTheorem :: IO ThmResult correctnessTheorem = proveWith yices{timing = True} $     forAll ["mem", "addrX", "x", "addrY", "y", "addrLow", "regX", "regA", "memVals", "flagC", "flagZ"]
Data/SBV/Examples/BitPrecise/PrefixSum.hs view
@@ -127,9 +127,11 @@ -- -- Also, the unit @0@ is clearly not a left-unit for @flOp@, as the third -- equation for @flOp@ will simply map many elements to @0@.+-- (NB. We need to use yices for this proof as the uninterpreted function+-- examples are only supported through the yices interface currently.) thm3 :: IO ThmResult-thm3 = prove $ do args :: PowerList SWord32 <- mkForallVars 8-                  return $ ps (u, op) args .== lf (u, op) args+thm3 = proveWith yices $ do args :: PowerList SWord32 <- mkForallVars 8+                            return $ ps (u, op) args .== lf (u, op) args   where op :: SWord32 -> SWord32 -> SWord32         op = uninterpret "flOp"         u :: SWord32
Data/SBV/Examples/CodeGeneration/AddSub.hs view
@@ -18,113 +18,120 @@ addSub :: SWord8 -> SWord8 -> (SWord8, SWord8) addSub x y = (x+y, x-y) --- | Generate C code for addSub. This will place the files in a directory called @genAddSub@,--- generating the following files:------ File: @Makefile@------ > # Makefile for addSub. 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: addSub_driver--- > --- > addSub.o: addSub.c addSub.h--- > 	${CC} ${CCFLAGS} -c $< -o $@--- > --- > addSub_driver.o: addSub_driver.c--- > 	${CC} ${CCFLAGS} -c $< -o $@--- > --- > addSub_driver: addSub.o addSub_driver.o--- > 	${CC} ${CCFLAGS} $^ -o $@--- > --- > clean:--- > 	rm -f *.o--- > --- > veryclean: clean--- > 	rm -f addSub_driver------ File: @addSub.h@------ > /* Header file for addSub. Automatically generated by SBV. Do not edit! */--- > --- > #ifndef __addSub__HEADER_INCLUDED__--- > #define __addSub__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: */--- > void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,--- >             SWord8 *dif);--- > --- > #endif /* __addSub__HEADER_INCLUDED__ */------ File: @addSub.c@------ > /* File: "addSub.c". Automatically generated by SBV. Do not edit! */--- > --- > #include <inttypes.h>--- > #include <stdint.h>--- > #include "addSub.h"--- > --- > void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,--- >             SWord8 *dif)--- > {--- >   const SWord8 s0 = x;--- >   const SWord8 s1 = y;--- >   const SWord8 s2 = s0 + s1;--- >   const SWord8 s3 = s0 - s1;--- >   --- >   *sum = s2;--- >   *dif = s3;--- > }------ File: @addSub_driver.c@+-- | Generate C code for addSub. Here's the output showing the generated C code: ----- > /* Example driver program for addSub. */--- > /* Automatically generated by SBV. Edit as you see fit! */--- > --- > #include <inttypes.h>--- > #include <stdint.h>--- > #include <stdio.h>--- > #include "addSub.h"--- > --- > int main(void)--- > {--- >   SWord8 sum;--- >   SWord8 dif;--- >   --- >   addSub(132, 241, &sum, &dif);--- >   --- >   printf("addSub(132, 241, &sum, &dif) ->\n");--- >   printf("  sum = %"PRIu8"\n", sum);--- >   printf("  dif = %"PRIu8"\n", dif);--- >   --- >   return 0;--- > }+-- >>> genAddSub+-- == BEGIN: "Makefile" ================+-- # Makefile for addSub. Automatically generated by SBV. Do not edit!+-- <BLANKLINE>+-- # include any user-defined .mk file in the current directory.+-- -include *.mk+-- <BLANKLINE>+-- CC=gcc+-- CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer+-- <BLANKLINE>+-- all: addSub_driver+-- <BLANKLINE>+-- addSub.o: addSub.c addSub.h+-- 	${CC} ${CCFLAGS} -c $< -o $@+-- <BLANKLINE>+-- addSub_driver.o: addSub_driver.c+-- 	${CC} ${CCFLAGS} -c $< -o $@+-- <BLANKLINE>+-- addSub_driver: addSub.o addSub_driver.o+-- 	${CC} ${CCFLAGS} $^ -o $@+-- <BLANKLINE>+-- clean:+-- 	rm -f *.o+-- <BLANKLINE>+-- veryclean: clean+-- 	rm -f addSub_driver+-- == END: "Makefile" ==================+-- == BEGIN: "addSub.h" ================+-- /* Header file for addSub. Automatically generated by SBV. Do not edit! */+-- <BLANKLINE>+-- #ifndef __addSub__HEADER_INCLUDED__+-- #define __addSub__HEADER_INCLUDED__+-- <BLANKLINE>+-- #include <inttypes.h>+-- #include <stdint.h>+-- #include <stdbool.h>+-- <BLANKLINE>+-- /* The boolean type */+-- typedef bool SBool;+-- <BLANKLINE>+-- /* Unsigned bit-vectors */+-- typedef uint8_t  SWord8 ;+-- typedef uint16_t SWord16;+-- typedef uint32_t SWord32;+-- typedef uint64_t SWord64;+-- <BLANKLINE>+-- /* Signed bit-vectors */+-- typedef int8_t  SInt8 ;+-- typedef int16_t SInt16;+-- typedef int32_t SInt32;+-- typedef int64_t SInt64;+-- <BLANKLINE>+-- /* Entry point prototype: */+-- void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,+--             SWord8 *dif);+-- <BLANKLINE>+-- #endif /* __addSub__HEADER_INCLUDED__ */+-- == END: "addSub.h" ==================+-- == BEGIN: "addSub_driver.c" ================+-- /* Example driver program for addSub. */+-- /* Automatically generated by SBV. Edit as you see fit! */+-- <BLANKLINE>+-- #include <inttypes.h>+-- #include <stdint.h>+-- #include <stdbool.h>+-- #include <stdio.h>+-- #include "addSub.h"+-- <BLANKLINE>+-- int main(void)+-- {+--   SWord8 sum;+--   SWord8 dif;+-- <BLANKLINE>+--   addSub(132, 241, &sum, &dif);+-- <BLANKLINE>+--   printf("addSub(132, 241, &sum, &dif) ->\n");+--   printf("  sum = %"PRIu8"\n", sum);+--   printf("  dif = %"PRIu8"\n", dif);+-- <BLANKLINE>+--   return 0;+-- }+-- == END: "addSub_driver.c" ==================+-- == BEGIN: "addSub.c" ================+-- /* File: "addSub.c". Automatically generated by SBV. Do not edit! */+-- <BLANKLINE>+-- #include <inttypes.h>+-- #include <stdint.h>+-- #include <stdbool.h>+-- #include "addSub.h"+-- <BLANKLINE>+-- void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,+--             SWord8 *dif)+-- {+--   const SWord8 s0 = x;+--   const SWord8 s1 = y;+--   const SWord8 s2 = s0 + s1;+--   const SWord8 s3 = s0 - s1;+-- <BLANKLINE>+--   *sum = s2;+--   *dif = s3;+-- }+-- == END: "addSub.c" ================== -- genAddSub :: IO ()-genAddSub = compileToC (Just "xx") "addSub" $ do+genAddSub = compileToC outDir "addSub" $ do         x <- cgInput "x"         y <- cgInput "y"+        -- leave the cgDriverVals call out for generating a driver with random values+        cgSetDriverValues [132, 241]         let (s, d) = addSub x y         cgOutput "sum" s         cgOutput "dif" d+ where -- use Just "dirName" for putting the output to the named directory+       -- otherwise, it'll go to standard output+       outDir = Nothing
Data/SBV/Examples/CodeGeneration/GCD.hs view
@@ -81,6 +81,7 @@ -- >  -- > #include <inttypes.h> -- > #include <stdint.h>+-- > #include <stdbool.h> -- > #include "sgcd.h" -- >  -- > SWord8 sgcd(const SWord8 x, const SWord8 y)
Data/SBV/Examples/CodeGeneration/PopulationCount.hs view
@@ -40,8 +40,8 @@ -- go 8 bits at a time instead of one by one, by using a precomputed table -- of population-count values for each byte. This algorithm /loops/ only -- 8 times, and hence is at least 8 times more efficient.-popCount :: SWord64 -> SWord8-popCount inp = go inp 0 0+popCountFast :: SWord64 -> SWord8+popCountFast inp = go inp 0 0   where go :: SWord64 -> Int -> SWord8 -> SWord8         go _ 8 c = c         go x i c = go (x `shiftR` 8) (i+1) (c + select pop8 0 (x .&. 0xff))@@ -57,19 +57,20 @@ -----------------------------------------------------------------------------  {- $VerificationIntro-We prove that `popCount` and `popCountSlow` are functionally equivalent.-This is essential as we will automatically generate C code from `popCount`,+We prove that `popCountFast` and `popCountSlow` are functionally equivalent.+This is essential as we will automatically generate C code from `popCountFast`, and we would like to make sure that the fast version is correct with respect to the slower reference version. -}  -- | States the correctness of faster population-count algorithm, with respect--- to the reference slow version. We have:+-- to the reference slow version. (We use yices here as it's quite fast for+-- this problem. Z3 seems to take much longer.) We have: ----- >>> prove fastPopCountIsCorrect+-- >>> proveWith yices fastPopCountIsCorrect -- Q.E.D. fastPopCountIsCorrect :: SWord64 -> SBool-fastPopCountIsCorrect x = popCount x .== popCountSlow x+fastPopCountIsCorrect x = popCountFast x .== popCountSlow x  ----------------------------------------------------------------------------- -- * Code generation@@ -79,142 +80,145 @@ -- generate C code to compute population-counts for us. This action will generate all the -- C files that you will need, including a driver program for test purposes. ----- Below is the generated header file for `popCount`:------ > /* Header file for popCount. Automatically generated by SBV. Do not edit! */--- > --- > #ifndef __popCount__HEADER_INCLUDED__--- > #define __popCount__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: */--- > SWord8 popCount(const SWord64 x);--- > --- > #endif /* __popCount__HEADER_INCLUDED__ */------ The generated C function. Note how the Haskell list `pop8` is turned into a look-up--- table automatically (see @table0@ below) in the C code.------ > /* File: "popCount.c". Automatically generated by SBV. Do not edit! */--- > --- > #include <inttypes.h>--- > #include <stdint.h>--- > #include "popCount.h"--- > --- > SWord8 popCount(const SWord64 x)--- > {--- >   const SWord64 s0 = x;--- >   static const SWord8 table0[] = {--- >       0, 1, 1, 2, 1, 2, 2, 3, 1, 2, 2, 3, 2, 3, 3, 4, 1, 2, 2, 3, 2, 3,--- >       3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4,--- >       3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 1, 2,--- >       2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5,--- >       3, 4, 4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5,--- >       5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 1, 2, 2, 3,--- >       2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4,--- >       4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6,--- >       3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 2, 3, 3, 4, 3, 4,--- >       4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6,--- >       5, 6, 6, 7, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 4, 5,--- >       5, 6, 5, 6, 6, 7, 5, 6, 6, 7, 6, 7, 7, 8--- >   };--- >   const SWord64 s11 = s0 & 0x00000000000000ffULL;--- >   const SWord8  s12 = table0[s11];--- >   const SWord64 s13 = s0 >> 8;--- >   const SWord64 s14 = 0x00000000000000ffULL & s13;--- >   const SWord8  s15 = table0[s14];--- >   const SWord8  s16 = s12 + s15;--- >   const SWord64 s17 = s13 >> 8;--- >   const SWord64 s18 = 0x00000000000000ffULL & s17;--- >   const SWord8  s19 = table0[s18];--- >   const SWord8  s20 = s16 + s19;--- >   const SWord64 s21 = s17 >> 8;--- >   const SWord64 s22 = 0x00000000000000ffULL & s21;--- >   const SWord8  s23 = table0[s22];--- >   const SWord8  s24 = s20 + s23;--- >   const SWord64 s25 = s21 >> 8;--- >   const SWord64 s26 = 0x00000000000000ffULL & s25;--- >   const SWord8  s27 = table0[s26];--- >   const SWord8  s28 = s24 + s27;--- >   const SWord64 s29 = s25 >> 8;--- >   const SWord64 s30 = 0x00000000000000ffULL & s29;--- >   const SWord8  s31 = table0[s30];--- >   const SWord8  s32 = s28 + s31;--- >   const SWord64 s33 = s29 >> 8;--- >   const SWord64 s34 = 0x00000000000000ffULL & s33;--- >   const SWord8  s35 = table0[s34];--- >   const SWord8  s36 = s32 + s35;--- >   const SWord64 s37 = s33 >> 8;--- >   const SWord64 s38 = 0x00000000000000ffULL & s37;--- >   const SWord8  s39 = table0[s38];--- >   const SWord8  s40 = s36 + s39;--- >   --- >   return s40;--- > }------ SBV will also generate a driver program for test purposes. The driver will call--- the generated function with random values. (It is also possible to instruct SBV--- to use prescribed values, see the function `compileToC''.)------ > /* Example driver program for popCount. */--- > /* Automatically generated by SBV. Edit as you see fit! */--- > --- > #include <inttypes.h>--- > #include <stdint.h>--- > #include <stdio.h>--- > #include "popCount.h"--- > --- > int main(void)--- > {--- >   const SWord8 __result = popCount(0x000000007016b176ULL);--- >   --- >   printf("popCount(0x000000007016b176ULL) = %"PRIu8"\n", __result);--- >   --- >   return 0;--- > }------ And a @Makefile@ to simplify compilation:+-- Below is the generated header file for `popCountFast`: ----- > # Makefile for popCount. 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: popCount_driver--- > --- > popCount.o: popCount.c popCount.h--- > 	${CC} ${CCFLAGS} -c $< -o $@--- > --- > popCount_driver.o: popCount_driver.c--- > 	${CC} ${CCFLAGS} -c $< -o $@--- > --- > popCount_driver: popCount.o popCount_driver.o--- > 	${CC} ${CCFLAGS} $^ -o $@--- > --- > clean:--- > 	rm -f *.o--- > --- > veryclean: clean--- >	rm -f popCount_driver+-- >>> genPopCountInC+-- == BEGIN: "Makefile" ================+-- # Makefile for popCount. Automatically generated by SBV. Do not edit!+-- <BLANKLINE>+-- # include any user-defined .mk file in the current directory.+-- -include *.mk+-- <BLANKLINE>+-- CC=gcc+-- CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer+-- <BLANKLINE>+-- all: popCount_driver+-- <BLANKLINE>+-- popCount.o: popCount.c popCount.h+-- 	${CC} ${CCFLAGS} -c $< -o $@+-- <BLANKLINE>+-- popCount_driver.o: popCount_driver.c+-- 	${CC} ${CCFLAGS} -c $< -o $@+-- <BLANKLINE>+-- popCount_driver: popCount.o popCount_driver.o+-- 	${CC} ${CCFLAGS} $^ -o $@+-- <BLANKLINE>+-- clean:+-- 	rm -f *.o+-- <BLANKLINE>+-- veryclean: clean+-- 	rm -f popCount_driver+-- == END: "Makefile" ==================+-- == BEGIN: "popCount.h" ================+-- /* Header file for popCount. Automatically generated by SBV. Do not edit! */+-- <BLANKLINE>+-- #ifndef __popCount__HEADER_INCLUDED__+-- #define __popCount__HEADER_INCLUDED__+-- <BLANKLINE>+-- #include <inttypes.h>+-- #include <stdint.h>+-- #include <stdbool.h>+-- <BLANKLINE>+-- /* The boolean type */+-- typedef bool SBool;+-- <BLANKLINE>+-- /* Unsigned bit-vectors */+-- typedef uint8_t  SWord8 ;+-- typedef uint16_t SWord16;+-- typedef uint32_t SWord32;+-- typedef uint64_t SWord64;+-- <BLANKLINE>+-- /* Signed bit-vectors */+-- typedef int8_t  SInt8 ;+-- typedef int16_t SInt16;+-- typedef int32_t SInt32;+-- typedef int64_t SInt64;+-- <BLANKLINE>+-- /* Entry point prototype: */+-- SWord8 popCount(const SWord64 x);+-- <BLANKLINE>+-- #endif /* __popCount__HEADER_INCLUDED__ */+-- == END: "popCount.h" ==================+-- == BEGIN: "popCount_driver.c" ================+-- /* Example driver program for popCount. */+-- /* Automatically generated by SBV. Edit as you see fit! */+-- <BLANKLINE>+-- #include <inttypes.h>+-- #include <stdint.h>+-- #include <stdbool.h>+-- #include <stdio.h>+-- #include "popCount.h"+-- <BLANKLINE>+-- int main(void)+-- {+--   const SWord8 __result = popCount(0x1b02e143e4f0e0e5ULL);+-- <BLANKLINE>+--   printf("popCount(0x1b02e143e4f0e0e5ULL) = %"PRIu8"\n", __result);+-- <BLANKLINE>+--   return 0;+-- }+-- == END: "popCount_driver.c" ==================+-- == BEGIN: "popCount.c" ================+-- /* File: "popCount.c". Automatically generated by SBV. Do not edit! */+-- <BLANKLINE>+-- #include <inttypes.h>+-- #include <stdint.h>+-- #include <stdbool.h>+-- #include "popCount.h"+-- <BLANKLINE>+-- SWord8 popCount(const SWord64 x)+-- {+--   const SWord64 s0 = x;+--   static const SWord8 table0[] = {+--       0, 1, 1, 2, 1, 2, 2, 3, 1, 2, 2, 3, 2, 3, 3, 4, 1, 2, 2, 3, 2, 3,+--       3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4,+--       3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 1, 2,+--       2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5,+--       3, 4, 4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5,+--       5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 1, 2, 2, 3,+--       2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4,+--       4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6,+--       3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 2, 3, 3, 4, 3, 4,+--       4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6,+--       5, 6, 6, 7, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 4, 5,+--       5, 6, 5, 6, 6, 7, 5, 6, 6, 7, 6, 7, 7, 8+--   };+--   const SWord64 s11 = s0 & 0x00000000000000ffULL;+--   const SWord8  s12 = table0[s11];+--   const SWord64 s13 = s0 >> 8;+--   const SWord64 s14 = 0x00000000000000ffULL & s13;+--   const SWord8  s15 = table0[s14];+--   const SWord8  s16 = s12 + s15;+--   const SWord64 s17 = s13 >> 8;+--   const SWord64 s18 = 0x00000000000000ffULL & s17;+--   const SWord8  s19 = table0[s18];+--   const SWord8  s20 = s16 + s19;+--   const SWord64 s21 = s17 >> 8;+--   const SWord64 s22 = 0x00000000000000ffULL & s21;+--   const SWord8  s23 = table0[s22];+--   const SWord8  s24 = s20 + s23;+--   const SWord64 s25 = s21 >> 8;+--   const SWord64 s26 = 0x00000000000000ffULL & s25;+--   const SWord8  s27 = table0[s26];+--   const SWord8  s28 = s24 + s27;+--   const SWord64 s29 = s25 >> 8;+--   const SWord64 s30 = 0x00000000000000ffULL & s29;+--   const SWord8  s31 = table0[s30];+--   const SWord8  s32 = s28 + s31;+--   const SWord64 s33 = s29 >> 8;+--   const SWord64 s34 = 0x00000000000000ffULL & s33;+--   const SWord8  s35 = table0[s34];+--   const SWord8  s36 = s32 + s35;+--   const SWord64 s37 = s33 >> 8;+--   const SWord64 s38 = 0x00000000000000ffULL & s37;+--   const SWord8  s39 = table0[s38];+--   const SWord8  s40 = s36 + s39;+-- <BLANKLINE>+--   return s40;+-- }+-- == END: "popCount.c" ================== genPopCountInC :: IO () genPopCountInC = compileToC Nothing "popCount" $ do+        cgSetDriverValues [0x1b02e143e4f0e0e5]  -- remove this line to get a random test value         x <- cgInput "x"-        cgReturn $ popCount x+        cgReturn $ popCountFast x
Data/SBV/Examples/Puzzles/U2Bridge.hs view
@@ -249,16 +249,16 @@ -- Checking for solutions with 5 moves. -- Solution #1:  --  0 --> Edge, Bono---  2 <-- Edge---  4 --> Larry, Adam--- 14 <-- Bono+--  2 <-- Bono+--  3 --> Larry, Adam+-- 13 <-- Edge -- 15 --> Edge, Bono -- Total time: 17 -- Solution #2:  --  0 --> Edge, Bono---  2 <-- Bono---  3 --> Larry, Adam--- 13 <-- Edge+--  2 <-- Edge+--  4 --> Larry, Adam+-- 14 <-- Bono -- 15 --> Edge, Bono -- Total time: 17 -- Found: 2 solutions with 5 moves.
Data/SBV/Examples/Uninterpreted/Function.hs view
@@ -26,11 +26,12 @@ thmGood x y z = x .== y+2 ==> f x z .== f (y + 2) z  -- | Asserts that @f@ is commutative; which is not necessarily true!--- Indeed, the SMT solver (Yices in this case) returns a counter-example--- function that is not commutative. We have:+-- Indeed, the SMT solver returns a counter-example function that is+-- not commutative. (Note that we have to use Yices as Z3 function+-- counterexamples are not yet supported by sbv.) We have: -- ----- >>> prove $ forAll ["x", "y"] thmBad+-- >>> proveWith yices $ forAll ["x", "y"] thmBad -- Falsifiable. Counter-example: --   x = 0 :: SWord8 --   y = 128 :: SWord8
Data/SBV/Provers/Prover.hs view
@@ -27,7 +27,7 @@        , sat, satWith        , allSat, allSatWith        , isVacuous, isVacuousWith-       , SatModel(..), Modelable(..), displayModels+       , SatModel(..), Modelable(..), displayModels, extractModels        , yices, z3, defaultSMTCfg        , compileToSMTLib        ) where@@ -49,17 +49,20 @@ import qualified Data.SBV.Provers.Z3    as Z3 import Data.SBV.Utils.TDiff +mkConfig :: SMTSolver -> Bool -> SMTConfig+mkConfig s isSMTLib2 = SMTConfig {verbose = False, timing = False, timeOut = Nothing, printBase = 10, smtFile = Nothing, solver = s, useSMTLib2 = isSMTLib2}+ -- | Default configuration for the Yices SMT Solver. yices :: SMTConfig-yices = SMTConfig {verbose = False, timing = False, timeOut = Nothing, printBase = 10, smtFile = Nothing, solver = Yices.yices, useSMTLib2 = False}+yices = mkConfig Yices.yices False  -- | Default configuration for the Z3 SMT solver z3 :: SMTConfig-z3 = yices { solver = Z3.z3, useSMTLib2 = True }+z3 = mkConfig Z3.z3 True --- | The default solver used by SBV. This is currently set to yices.+-- | The default solver used by SBV. This is currently set to z3. defaultSMTCfg :: SMTConfig-defaultSMTCfg = yices+defaultSMTCfg = z3  -- | A predicate is a symbolic program that returns a (symbolic) boolean value. For all intents and -- purposes, it can be treated as an n-ary function from symbolic-values to a boolean. The 'Symbolic'@@ -396,7 +399,7 @@         let msg = when (verbose config) . putStrLn . ("** " ++)             isTiming = timing config         msg "Starting symbolic simulation.."-        res <- timeIf isTiming "problem construction" $ runSymbolic isSat $ forAll_ predicate >>= output+        res <- timeIf isTiming "problem construction" $ runSymbolic isSat $ (if isSat then forSome_ else forAll_) predicate >>= output         msg $ "Generated symbolic trace:\n" ++ show res         msg "Translating to SMT-Lib.."         runProofOn converter config isSat comments res
Data/SBV/Provers/Yices.hs view
@@ -10,10 +10,13 @@ -- The connection to the Yices SMT solver ----------------------------------------------------------------------------- -{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE PatternGuards       #-}+{-# LANGUAGE ScopedTypeVariables #-}  module Data.SBV.Provers.Yices(yices) where +import qualified Control.Exception as C+ import Data.Char          (isDigit) import Data.List          (sortBy, isPrefixOf, intercalate, transpose, partition) import Data.Maybe         (mapMaybe, isNothing, fromJust)@@ -34,8 +37,8 @@          -- , options    = ["-tc", "-smt", "-e"]   -- For Yices1          , options    = ["-m", "-f"]  -- For Yices2          , engine     = \cfg _isSat qinps modelMap _skolemMap pgm -> do-                                execName <-                getEnv "SBV_YICES"          `catch` (\_ -> return (executable (solver cfg)))-                                execOpts <- (words `fmap`  getEnv "SBV_YICES_OPTIONS") `catch` (\_ -> return (options (solver cfg)))+                                execName <-                getEnv "SBV_YICES"          `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))+                                execOpts <- (words `fmap`  getEnv "SBV_YICES_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg)))                                 let cfg' = cfg { solver = (solver cfg) {executable = execName, options = addTimeOut (timeOut cfg) execOpts} }                                     script = SMTScript { scriptBody = pgm, scriptModel = Nothing }                                 standardSolver cfg' script id (ProofError cfg) (interpretSolverOutput cfg (extractMap (map snd qinps) modelMap))
Data/SBV/Provers/Z3.hs view
@@ -11,9 +11,12 @@ -----------------------------------------------------------------------------  {-# LANGUAGE PatternGuards #-}+{-# LANGUAGE ScopedTypeVariables #-}  module Data.SBV.Provers.Z3(z3) where +import qualified Control.Exception as C+ import Data.Char          (isDigit, toLower) import Data.List          (sortBy, intercalate, isPrefixOf) import System.Environment (getEnv)@@ -40,8 +43,8 @@          , executable = "z3"          , options    = map (optionPrefix:) ["in", "smt2"]          , engine     = \cfg isSat qinps modelMap skolemMap pgm -> do-                                execName <-               getEnv "SBV_Z3"          `catch` (\_ -> return (executable (solver cfg)))-                                execOpts <- (words `fmap` getEnv "SBV_Z3_OPTIONS") `catch` (\_ -> return (options (solver cfg)))+                                execName <-               getEnv "SBV_Z3"          `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))+                                execOpts <- (words `fmap` getEnv "SBV_Z3_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg)))                                 let cfg' = cfg { solver = (solver cfg) {executable = execName, options = addTimeOut (timeOut cfg) execOpts} }                                     script = SMTScript { scriptBody = "(set-option :mbqi true)\n" ++ pgm, scriptModel = Just (cont skolemMap)}                                 standardSolver cfg' script cleanErrs (ProofError cfg) (interpretSolverOutput cfg (extractMap isSat qinps modelMap . zipWith match skolemMap))@@ -66,8 +69,7 @@        addTimeOut Nothing  o   = o        addTimeOut (Just i) o          | i < 0               = error $ "Z3: Timeout value must be non-negative, received: " ++ show i-         | S.os == "linux"     = o ++ ["-T:" ++ show i]-         | True                = o ++ ["/T:" ++ show i]+         | True                = o ++ [optionPrefix : "T:" ++ show i]  extractMap :: Bool -> [(Quantifier, NamedSymVar)] -> [(String, UnintKind)] -> [String] -> SMTModel extractMap isSat qinps _modelMap solverLines =
Data/SBV/SMT/SMT.hs view
@@ -248,6 +248,11 @@                      Right (_, b) -> Just b                      _            -> Nothing +-- | Return all the models from an 'allSat' call, similar to 'extractModel' but+-- is suitable for the case of multiple results.+extractModels :: SatModel a => AllSatResult -> [a]+extractModels (AllSatResult (_, xs)) = [ms | Right (_, ms) <- map getModel xs]+ instance Modelable ThmResult where   getModel    (ThmResult r) = getModel r   modelExists (ThmResult r) = modelExists r
+ Data/SBV/Tools/ExpectedValue.hs view
@@ -0,0 +1,85 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.Tools.ExpectedValue+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+-- Portability :  portable+--+-- Computing the expected value of a symbolic variable+-----------------------------------------------------------------------------++{-# LANGUAGE PatternGuards #-}+module Data.SBV.Tools.ExpectedValue (expectedValue, expectedValueWith) where++import Control.DeepSeq (rnf)+import System.Random   (newStdGen, StdGen)+import Numeric++import Data.SBV.BitVectors.Data++-- | Generalized version of 'expectedValue', allowing the user to specify the+-- warm-up count and the convergence factor. Maximum iteration count can also+-- be specified, at which point convergence won't be sought. The boolean controls verbosity.+expectedValueWith :: Outputtable a => Bool -> Int -> Maybe Int -> Double -> Symbolic a -> IO [Double]+expectedValueWith verbose warmupCount mbMaxIter epsilon m+  | warmupCount < 0 || epsilon < 0+  = error $ "SBV.expectedValue: warmup count and epsilon both must be non-negative, received: " ++ show (warmupCount, epsilon)+  | True+  = warmup warmupCount (repeat 0) >>= go warmupCount+  where progress s | not verbose = return ()+                   | True        = putStr $ "\r*** " ++ s+        warmup :: Int -> [Integer] -> IO [Integer]+        warmup 0 v = do progress $ "Warmup complete, performed " ++ show warmupCount ++ " rounds.\n"+                        return v+        warmup n v = do progress $ "Performing warmup, round: " ++ show (warmupCount - n)+                        g <- newStdGen+                        t <- runOnce g+                        let v' = zipWith (+) v t+                        rnf v' `seq` warmup (n-1) v'+        runOnce :: StdGen -> IO [Integer]+        runOnce g = do (_, Result _ _ _ _ cs _ _ _ _ _ cstrs os) <- runSymbolic' (Concrete g) (m >>= output)+                       let cval o = case o `lookup` cs of+                                      Nothing -> error "SBV.expectedValue: Cannot compute expected-values in the presence of uninterpreted constants!"+                                      Just cw -> case (cwSigned cw, cwSize cw) of+                                                   (True,  Size Nothing ) -> error "Cannot compute expected-values for unbounded integer results."+                                                   (False, Size (Just 1)) -> if cwToBool cw then 1 else 0+                                                   _                      -> cwVal cw+                       if all ((== 1) . cval) cstrs+                          then return $ map cval os+                          else runOnce g -- constraint not satisfied try again with the same set of constraints+        go :: Int -> [Integer] -> IO [Double]+        go cases curSums+         | Just n <- mbMaxIter, n < curRound+         = do progress "\n"+              progress "Maximum iteration count reached, stopping.\n"+              return curEVs+         | True+         = do g <- newStdGen+              t <- runOnce g+              let newSums  = zipWith (+) curSums t+                  newEVs = map ev' newSums+                  diffs  = zipWith (\x y -> abs (x - y)) newEVs curEVs+              if all (< epsilon) diffs+                 then do progress $ "Converges with epsilon " ++ show epsilon ++ " after " ++ show curRound ++ " rounds.\n"+                         return newEVs+                 else do progress $ "Tuning, round: " ++ show curRound ++ " (margin: " ++ showFFloat (Just 6) (maximum (0:diffs)) "" ++ ")"+                         go newCases newSums+         where curRound = cases - warmupCount+               newCases = cases + 1+               ev, ev' :: Integer -> Double+               ev  x  = fromIntegral x / fromIntegral cases+               ev' x  = fromIntegral x / fromIntegral newCases+               curEVs = map ev curSums++-- | Given a symbolic computation that produces a value, compute the+-- expected value that value would take if this computation is run+-- with its free variables drawn from uniform distributions of its+-- respective values, satisfying the given constraints specified by+-- 'constrain' and 'pConstrain' calls. This is equivalent to calling+-- 'expectedValueWith' the following parameters: verbose, warm-up+-- round count of @10000@, no maximum iteration count, and with+-- convergence margin @0.0001@.+expectedValue :: Outputtable a => Symbolic a -> IO [Double]+expectedValue = expectedValueWith True 10000 Nothing 0.0001
+ Data/SBV/Tools/GenTest.hs view
@@ -0,0 +1,259 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.Tools.GenTest+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+-- Portability :  portable+--+-- Test generation from symbolic programs+-----------------------------------------------------------------------------++module Data.SBV.Tools.GenTest (genTest, TestVectors, getTestValues, renderTest, TestStyle(..)) where++import Data.Bits     (testBit)+import Data.Char     (isAlpha, toUpper)+import Data.Maybe    (fromMaybe)+import Data.List     (intercalate, groupBy)+import System.Random++import Data.SBV.BitVectors.Data+import Data.SBV.BitVectors.PrettyNum++-- | Type of test vectors (abstract)+newtype TestVectors = TV [([CW], [CW])]++-- | Retrieve the test vectors for further processing. This function+-- is useful in cases where 'renderTest' is not sufficient and custom+-- output (or further preprocessing) is needed.+getTestValues :: TestVectors -> [([CW], [CW])]+getTestValues (TV vs) = vs++-- | Generate a set of concrete test values from a symbolic program. The output+-- can be rendered as test vectors in different languages as necessary. Use the+-- function 'output' call to indicate what fields should be in the test result.+-- (Also see 'constrain' and 'pConstrain' for filtering acceptable test values.)+genTest :: Outputtable a => Int -> Symbolic a -> IO TestVectors+genTest n m = gen 0 []+  where gen i sofar+         | i == n = return $ TV $ reverse sofar+         | True   = do g <- newStdGen+                       t <- tc g+                       gen (i+1) (t:sofar)+        tc g = do (_, Result _ tvals _ _ cs _ _ _ _ _ cstrs os) <- runSymbolic' (Concrete g) (m >>= output)+                  let cval = fromMaybe (error "Cannot generate tests in the presence of uninterpeted constants!") . (`lookup` cs)+                      cond = all (cwToBool . cval) cstrs+                  if cond+                     then return (map snd tvals, map cval os)+                     else tc g  -- try again, with the same set of constraints++-- | Test output style+data TestStyle = Haskell String                     -- ^ As a Haskell value with given name+               | C       String                     -- ^ As a C array of structs with given name+               | Forte   String Bool ([Int], [Int]) -- ^ As a Forte/Verilog value with given name.+                                                    -- If the boolean is True then vectors are blasted big-endian, otherwise little-endian+                                                    -- The indices are the split points on bit-vectors for input and output values++-- | Render the test as a Haskell value with the given name @n@.+renderTest :: TestStyle -> TestVectors -> String+renderTest (Haskell n)    (TV vs) = haskell n vs+renderTest (C n)          (TV vs) = c       n vs+renderTest (Forte n b ss) (TV vs) = forte   n b ss vs++haskell :: String -> [([CW], [CW])] -> String+haskell vname vs = intercalate "\n" $ [ "-- Automatically generated by SBV. Do not edit!"+                                      , ""+                                      , "module " ++ modName ++ "(" ++ n ++ ") where"+                                      , ""+                                      ]+                                   ++ imports+                                   ++ [ n ++ " :: " ++ getType vs+                                      , n ++ " = [ " ++ intercalate ("\n" ++ pad ++  ", ") (map mkLine vs), pad ++ "]"+                                      ]+  where n | null vname                 = "testVectors"+          | not (isAlpha (head vname)) = "tv" ++ vname+          | True                       = vname+        imports+          | null vs               = []+          | needsInt && needsWord = ["import Data.Int", "import Data.Word", ""]+          | needsInt              = ["import Data.Int", ""]+          | needsWord             = ["import Data.Word", ""]+          | True                  = []+          where ((is, os):_) = vs+                params       = is ++ os+                needsInt     = any isSW params+                needsWord    = any isUW params+                isSW cw      =      cwSigned cw  && cwSize cw /= Size Nothing && cwSize cw /= Size (Just 1)+                isUW cw      = not (cwSigned cw) && cwSize cw /= Size Nothing && cwSize cw /= Size (Just 1)+        modName = let (f:r) = n in toUpper f : r+        pad = replicate (length n + 3) ' '+        getType []         = "[a]"+        getType ((i, o):_) = "[(" ++ mapType typeOf i ++ ", " ++ mapType typeOf o ++ ")]"+        mkLine  (i, o)     = "("  ++ mapType valOf  i ++ ", " ++ mapType valOf  o ++ ")"+        mapType f cws = mkTuple $ map f $ groupBy (\c1 c2 -> (cwSigned c1, cwSize c1) == (cwSigned c2, cwSize c2)) cws+        mkTuple [x] = x+        mkTuple xs  = "(" ++ intercalate ", " xs ++ ")"+        typeOf []    = "()"+        typeOf [x]   = t x+        typeOf (x:_) = "[" ++ t x ++ "]"+        valOf  []    = "()"+        valOf  [x]   = s x+        valOf  xs    = "[" ++ intercalate ", " (map s xs) ++ "]"+        t cw = case (cwSigned cw, cwSize cw) of+                  (False, Size (Just  1)) -> "Bool"+                  (False, Size (Just  8)) -> "Word8"+                  (False, Size (Just 16)) -> "Word16"+                  (False, Size (Just 32)) -> "Word32"+                  (False, Size (Just 64)) -> "Word64"+                  (True,  Size (Just  8)) -> "Int8"+                  (True,  Size (Just 16)) -> "Int16"+                  (True,  Size (Just 32)) -> "Int32"+                  (True,  Size (Just 64)) -> "Int64"+                  (True,  Size Nothing)   -> "Integer"+                  _                       -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw+        s cw = case (cwSigned cw, cwSize cw) of+                  (False, Size (Just 1)) -> take 5 (show (cwToBool cw) ++ repeat ' ')+                  (sgn, Size (Just sz))  -> shex  False True (sgn, sz) (cwVal cw)+                  (_,   Size Nothing)    -> shexI False True           (cwVal cw)++c :: String -> [([CW], [CW])] -> String+c n vs = intercalate "\n" $+              [ "/* Automatically generated by SBV. Do not edit! */"+              , ""+              , "#include <stdio.h>"+              , "#include <inttypes.h>"+              , "#include <stdint.h>"+              , "#include <stdbool.h>"+              , ""+              , "/* The boolean type */"+              , "typedef bool SBool;"+              , ""+              , "/* Unsigned bit-vectors */"+              , "typedef uint8_t  SWord8 ;"+              , "typedef uint16_t SWord16;"+              , "typedef uint32_t SWord32;"+              , "typedef uint64_t SWord64;"+              , ""+              , "/* Signed bit-vectors */"+              , "typedef int8_t  SInt8 ;"+              , "typedef int16_t SInt16;"+              , "typedef int32_t SInt32;"+              , "typedef int64_t SInt64;"+              , ""+              , "typedef struct {"+              , "  struct {"+              ]+           ++ (if null vs then [] else zipWith (mkField "i") (fst (head vs)) [(0::Int)..])+           ++ [ "  } input;"+              , "  struct {"+              ]+           ++ (if null vs then [] else zipWith (mkField "o") (snd (head vs)) [(0::Int)..])+           ++ [ "  } output;"+              , "} " ++ n ++ "TestVector;"+              , ""+              , n ++ "TestVector " ++ n ++ "[] = {"+              ]+           ++ ["      " ++ intercalate "\n    , " (map mkLine vs)]+           ++ [ "};"+              , ""+              , "int " ++ n ++ "Length = " ++ show (length vs) ++ ";"+              , ""+              , "/* Stub driver showing the test values, replace with code that uses the test vectors. */"+              , "int main(void)"+              , "{"+              , "  int i;"+              , "  for(i = 0; i < " ++ n ++ "Length; ++i)"+              , "  {"+              , "    " ++ outLine+              , "  }"+              , ""+              , "  return 0;"+              , "}"+              ]+  where mkField p cw i = "    " ++ t ++ " " ++ p ++ show i ++ ";"+            where t = case (cwSigned cw, cwSize cw) of+                        (False, Size (Just  1)) -> "SBool"+                        (False, Size (Just  8)) -> "SWord8"+                        (False, Size (Just 16)) -> "SWord16"+                        (False, Size (Just 32)) -> "SWord32"+                        (False, Size (Just 64)) -> "SWord64"+                        (True,  Size (Just  8)) -> "SInt8"+                        (True,  Size (Just 16)) -> "SInt16"+                        (True,  Size (Just 32)) -> "SInt32"+                        (True,  Size (Just 64)) -> "SInt64"+                        (True,  Size Nothing)   -> error "SBV.rendertest: Unbounded integers are not supported when generating C test-cases."+                        _                       -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw+        mkLine (is, os) = "{{" ++ intercalate ", " (map v is) ++ "}, {" ++ intercalate ", " (map v os) ++ "}}"+        v cw = case (cwSigned cw, cwSize cw) of+                  (False, Size (Just 1)) -> if cwToBool cw then "true " else "false"+                  (sgn, Size (Just sz))  -> shex  False True (sgn, sz) (cwVal cw)+                  (_,   Size Nothing)    -> shexI False True           (cwVal cw)+        outLine+          | null vs = "printf(\"\");"+          | True    = "printf(\"%*d. " ++ fmtString ++ "\\n\", " ++ show (length (show (length vs - 1))) ++ ", i"+                    ++ concatMap ("\n           , " ++ ) (zipWith inp is [(0::Int)..] ++ zipWith out os [(0::Int)..])+                    ++ ");"+          where (is, os) = head vs+                inp cw i = mkBool cw (n ++ "[i].input.i"  ++ show i)+                out cw i = mkBool cw (n ++ "[i].output.o" ++ show i)+                mkBool cw s = case (cwSigned cw, cwSize cw) of+                                (False, Size (Just 1)) -> "(" ++ s ++ " == true) ? \"true \" : \"false\""+                                _                      -> s+                fmtString = unwords (map fmt is) ++ " -> " ++ unwords (map fmt os)+        fmt cw = case (cwSigned cw, cwSize cw) of+                    (False, Size (Just  1)) -> "%s"+                    (False, Size (Just  8)) -> "0x%02\"PRIx8\""+                    (False, Size (Just 16)) -> "0x%04\"PRIx16\"U"+                    (False, Size (Just 32)) -> "0x%08\"PRIx32\"UL"+                    (False, Size (Just 64)) -> "0x%016\"PRIx64\"ULL"+                    (True,  Size (Just  8)) -> "%\"PRId8\""+                    (True,  Size (Just 16)) -> "%\"PRId16\""+                    (True,  Size (Just 32)) -> "%\"PRId32\"L"+                    (True,  Size (Just 64)) -> "%\"PRId64\"LL"+                    (True,  Size Nothing)   -> error "SBV.rendertest: Unsupported unbounded integers for C generation."+                    _                       -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw++forte :: String -> Bool -> ([Int], [Int]) -> [([CW], [CW])] -> String+forte vname bigEndian ss vs = intercalate "\n" $ [ "// Automatically generated by SBV. Do not edit!"+                                             , "let " ++ n ++ " ="+                                             , "   let c s = val [_, r] = str_split s \"'\" in " ++ blaster+                                             ]+                                          ++ [ "   in [ " ++ intercalate "\n      , " (map mkLine vs)+                                             , "      ];"+                                             ]+  where n | null vname                 = "testVectors"+          | not (isAlpha (head vname)) = "tv" ++ vname+          | True                       = vname+        blaster+         | bigEndian = "map (\\s. s == \"1\") (explode (string_tl r))"+         | True      = "rev (map (\\s. s == \"1\") (explode (string_tl r)))"+        toF True  = '1'+        toF False = '0'+        blast cw = case (cwSigned cw, cwSize cw) of+                     (False, Size (Just  1)) -> [toF (cwToBool cw)]+                     (False, Size (Just  8)) -> xlt  8 (cwVal cw)+                     (False, Size (Just 16)) -> xlt 16 (cwVal cw)+                     (False, Size (Just 32)) -> xlt 32 (cwVal cw)+                     (False, Size (Just 64)) -> xlt 64 (cwVal cw)+                     (True,  Size (Just  8)) -> xlt  8 (cwVal cw)+                     (True,  Size (Just 16)) -> xlt 16 (cwVal cw)+                     (True,  Size (Just 32)) -> xlt 32 (cwVal cw)+                     (True,  Size (Just 64)) -> xlt 64 (cwVal cw)+                     (True,  Size Nothing)   -> error "SBV.rendertest: Unbounded integers are not supported when generating Forte test-cases."+                     _                       -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw+        xlt s v = [toF (testBit v i) | i <- [s-1, s-2 .. 0]]+        mkLine  (i, o) = "("  ++ mkTuple (form (fst ss) (concatMap blast i)) ++ ", " ++ mkTuple (form (snd ss) (concatMap blast o)) ++ ")"+        mkTuple []  = "()"+        mkTuple [x] = x+        mkTuple xs  = "(" ++ intercalate ", " xs ++ ")"+        form []     [] = []+        form []     bs = error $ "SBV.renderTest: Mismatched index in stream, extra " ++ show (length bs) ++ " bit(s) remain."+        form (i:is) bs+          | length bs < i = error $ "SBV.renderTest: Mismatched index in stream, was looking for " ++ show i ++ " bit(s), but only " ++ show i ++ " remains."+          | i == 1        = let b:r = bs+                                v   = if b == '1' then "T" else "F"+                            in v : form is r+          | True          = let (f, r) = splitAt i bs+                                v      = "c \"" ++ show i ++ "'b" ++ f ++ "\""+                            in v : form is r
+ Data/SBV/Tools/Optimize.hs view
@@ -0,0 +1,108 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.Tools.Optimize+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+-- Portability :  portable+--+-- SMT based optimization+-----------------------------------------------------------------------------++{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeSynonymInstances #-}++module Data.SBV.Tools.Optimize (OptimizeOpts(..), optimize, optimizeWith, minimize, minimizeWith, maximize, maximizeWith) where++import Data.Maybe (fromJust)++import Data.SBV.BitVectors.Data+import Data.SBV.BitVectors.Model (OrdSymbolic(..), EqSymbolic(..))+import Data.SBV.Provers.Prover   (satWith, z3)+import Data.SBV.SMT.SMT          (SatModel, getModel, SMTConfig(..))+import Data.SBV.Utils.Boolean++-- | Optimizer configuration. Note that iterative and quantified approaches are in general not interchangeable.+-- For instance, iterative solutions will loop infinitely when there is no optimal value, but quantified solutions+-- can handle such problems. Of course, quantified problems are harder for SMT solvers, naturally.+data OptimizeOpts = Iterative  Bool   -- ^ Iteratively search. if True, it will be reporting progress+                  | Quantified        -- ^ Use quantifiers++-- | Symbolic optimization. Generalization on 'minimize' and 'maximize' that allows arbitrary+-- cost functions and comparisons.+optimizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c)+             => SMTConfig                         -- ^ SMT configuration+             -> OptimizeOpts                      -- ^ Optimization options+             -> (SBV c -> SBV c -> SBool)         -- ^ comparator+             -> ([SBV a] -> SBV c)                -- ^ cost function+             -> Int                               -- ^ how many elements?+             -> ([SBV a] -> SBool)                -- ^ validity constraint+             -> IO (Maybe [a])+optimizeWith cfg (Iterative chatty) = iterOptimize chatty cfg+optimizeWith cfg Quantified         = quantOptimize cfg++-- | Variant of 'optimizeWith' using z3+optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])+optimize = optimizeWith z3++-- | Variant of 'maximize' allowing the use of a user specified solver.+maximizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])+maximizeWith cfg opts = optimizeWith cfg opts (.>=)++-- | Maximizes a cost function with respect to a constraint. Examples:+--+--   >>> maximize Quantified sum 3 (bAll (.< (10 :: SInteger)))+--   Just [9,9,9]+maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])+maximize = maximizeWith z3++-- | Variant of 'minimize' allowing the use of a user specified solver.+minimizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])+minimizeWith cfg opts = optimizeWith cfg opts (.<=)++-- | Minimizes a cost function with respect to a constraint. Examples:+--+--   >>> minimize Quantified sum 3 (bAll (.> (10 :: SInteger)))+--   Just [11,11,11]+minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])+minimize = minimizeWith z3++-- | Optimization using quantifiers+quantOptimize :: (SatModel a, SymWord a) => SMTConfig -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])+quantOptimize cfg cmp cost n valid = do+           m <- satWith cfg $ do xs <- mkExistVars  n+                                 ys <- mkForallVars n+                                 return $ valid xs &&& (valid ys ==> cost xs `cmp` cost ys)+           case getModel m of+              Right (True, _)  -> error "SBV: Backend solver reported \"unknown\""+              Right (False, a) -> return $ Just a+              Left _           -> return Nothing++-- | Optimization using iteration+iterOptimize :: (SatModel a, Show a, SymWord a, Show c, SymWord c) =>  Bool -> SMTConfig -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])+iterOptimize chatty cfg cmp cost n valid = do+        msg "Trying to find a satisfying solution."+        m <- satWith cfg $ valid `fmap` mkExistVars n+        case getModel m of+          Left _ -> return Nothing+          Right (True, _)  -> error "SBV: Backend solver reported \"unknown\""+          Right (False, a) -> do msg $ "First solution found: " ++ show a+                                 let c = cost (map literal a)+                                 msg $ "Initial value is    : " ++ show (fromJust (unliteral c))+                                 msg "Starting iterative search."+                                 go (1::Int) a c+  where msg m | chatty = putStrLn $ "*** " ++ m+              | True   = return ()+        go i curSol curCost = do+                msg $ "Round " ++ show i ++ " ****************************"+                m <- satWith cfg $ do xs <- mkExistVars n+                                      return $ let c = cost xs in valid xs &&& (c `cmp` curCost &&& c ./= curCost)+                case getModel m of+                  Left _ -> do msg "The current solution is optimal. Terminating search."+                               return $ Just curSol+                  Right (True, _)  -> error "SBV: Backend solver reported \"unknown\""+                  Right (False, a) -> do msg $ "Solution: " ++ show a+                                         let c = cost (map literal a)+                                         msg $ "Value   : " ++ show (fromJust (unliteral c))+                                         go (i+1) a c
+ Data/SBV/Tools/Polynomial.hs view
@@ -0,0 +1,238 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.BitVectors.Polynomials+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+-- Portability :  portable+--+-- Implementation of polynomial arithmetic+-----------------------------------------------------------------------------++{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PatternGuards #-}++module Data.SBV.Tools.Polynomial (Polynomial(..), crc, crcBV) where++import Data.Bits  (Bits(..))+import Data.List  (genericTake)+import Data.Maybe (fromJust)+import Data.Word  (Word8, Word16, Word32, Word64)++import Data.SBV.BitVectors.Data+import Data.SBV.BitVectors.Model+import Data.SBV.BitVectors.Splittable+import Data.SBV.Utils.Boolean++-- | Implements polynomial addition, multiplication, division, and modulus operations+-- over GF(2^n).  NB. Similar to 'bvQuotRem', division by @0@ is interpreted as follows:+--+--     @x `pDivMod` 0 = (0, x)@+--+-- for all @x@ (including @0@)+--+-- Minimal complete definiton: 'pMult', 'pDivMod', 'showPolynomial'+class Bits a => Polynomial a where+ -- | Given bit-positions to be set, create a polynomial+ -- For instance+ --+ --     @polynomial [0, 1, 3] :: SWord8@+ -- + -- will evaluate to @11@, since it sets the bits @0@, @1@, and @3@. Mathematicans would write this polynomial+ -- as @x^3 + x + 1@. And in fact, 'showPoly' will show it like that.+ polynomial :: [Int] -> a+ -- | Add two polynomials in GF(2^n)+ pAdd  :: a -> a -> a+ -- | Multiply two polynomials in GF(2^n), and reduce it by the irreducible specified by+ -- the polynomial as specified by coefficients of the third argument. Note that the third+ -- argument is specifically left in this form as it is usally in GF(2^(n+1)), which is not available in our+ -- formalism. (That is, we would need SWord9 for SWord8 multiplication, etc.) Also note that we do not+ -- support symbolic irreducibles, which is a minor shortcoming. (Most GF's will come with fixed irreducibles,+ -- so this should not be a problem in practice.)+ --+ -- Passing [] for the third argument will multiply the polynomials and then ignore the higher bits that won't+ -- fit into the resulting size.+ pMult :: (a, a, [Int]) -> a+ -- | Divide two polynomials in GF(2^n), see above note for division by 0+ pDiv  :: a -> a -> a+ -- | Compute modulus of two polynomials in GF(2^n), see above note for modulus by 0+ pMod  :: a -> a -> a+ -- | Division and modulus packed together+ pDivMod :: a -> a -> (a, a)+ -- | Display a polynomial like a mathematician would (over the monomial @x@), with a type+ showPoly :: a -> String+ -- | Display a polynomial like a mathematician would (over the monomial @x@), the first argument+ -- controls if the final type is shown as well.+ showPolynomial :: Bool -> a -> String++ -- defaults.. Minumum complete definition: pMult, pDivMod, showPolynomial+ polynomial = foldr (flip setBit) 0+ pAdd       = xor+ pDiv x y   = fst (pDivMod x y)+ pMod x y   = snd (pDivMod x y)+ showPoly   = showPolynomial False+++instance Polynomial Word8   where {showPolynomial   = sp;           pMult = lift polyMult; pDivMod = liftC polyDivMod}+instance Polynomial Word16  where {showPolynomial   = sp;           pMult = lift polyMult; pDivMod = liftC polyDivMod}+instance Polynomial Word32  where {showPolynomial   = sp;           pMult = lift polyMult; pDivMod = liftC polyDivMod}+instance Polynomial Word64  where {showPolynomial   = sp;           pMult = lift polyMult; pDivMod = liftC polyDivMod}+instance Polynomial SWord8  where {showPolynomial b = liftS (sp b); pMult = polyMult;      pDivMod = polyDivMod}+instance Polynomial SWord16 where {showPolynomial b = liftS (sp b); pMult = polyMult;      pDivMod = polyDivMod}+instance Polynomial SWord32 where {showPolynomial b = liftS (sp b); pMult = polyMult;      pDivMod = polyDivMod}+instance Polynomial SWord64 where {showPolynomial b = liftS (sp b); pMult = polyMult;      pDivMod = polyDivMod}++lift :: SymWord a => ((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a+lift f (x, y, z) = fromJust $ unliteral $ f (literal x, literal y, z)+liftC :: SymWord a => (SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)+liftC f x y = let (a, b) = f (literal x) (literal y) in (fromJust (unliteral a), fromJust (unliteral b))+liftS :: SymWord a => (a -> String) -> SBV a -> String+liftS f s+  | Just x <- unliteral s = f x+  | True                  = show s++-- | Pretty print as a polynomial+sp :: Bits a => Bool -> a -> String+sp st a+ | null cs = '0' : t+ | True    = foldr (\x y -> sh x ++ " + " ++ y) (sh (last cs)) (init cs) ++ t+ where t | st   = " :: GF(2^" ++ show n ++ ")"+         | True = ""+       n  = bitSize a+       is = [n-1, n-2 .. 0]+       cs = map fst $ filter snd $ zip is (map (testBit a) is)+       sh 0 = "1"+       sh 1 = "x"+       sh i = "x^" ++ show i++-- | Add two polynomials+addPoly :: [SBool] -> [SBool] -> [SBool]+addPoly xs    []      = xs+addPoly []    ys      = ys+addPoly (x:xs) (y:ys) = x <+> y : addPoly xs ys++ites :: SBool -> [SBool] -> [SBool] -> [SBool]+ites s xs ys+ | Just t <- unliteral s+ = if t then xs else ys+ | True+ = go xs ys+ where go [] []         = []+       go []     (b:bs) = ite s false b : go [] bs+       go (a:as) []     = ite s a false : go as []+       go (a:as) (b:bs) = ite s a b : go as bs++-- | 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)+  | 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 = 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+   | 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        = intSizeOf x+         (d, r)    = mdp (blastLE x) (blastLE y)++-- conservative over-approximation of the degree+degree :: [SBool] -> Int+degree xs = walk (length xs - 1) $ reverse xs+  where walk n []     = n+        walk n (b:bs)+         | Just t <- unliteral b+         = if t then n else walk (n-1) bs+         | True+         = n -- over-estimate++mdp :: [SBool] -> [SBool] -> ([SBool], [SBool])+mdp xs ys = go (length ys - 1) (reverse ys)+  where degTop  = degree xs+        go _ []     = error "SBV.Polynomial.mdp: Impossible happened; exhausted ys before hitting 0"+        go n (b:bs)+         | n == 0   = (reverse qs, rs)+         | True     = let (rqs, rrs) = go (n-1) bs+                      in (ites b (reverse qs) rqs, ites b rs rrs)+         where degQuot = degTop - n+               ys' = replicate degQuot false ++ ys+               (qs, rs) = divx (degQuot+1) degTop xs ys'++-- return the element at index i; if not enough elements, return false+-- N.B. equivalent to '(xs ++ repeat false) !! i', but more efficient+idx :: [SBool] -> Int -> SBool+idx []     _ = false+idx (x:_)  0 = x+idx (_:xs) i = idx xs (i-1)++divx :: Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])+divx n _ xs _ | n <= 0 = ([], xs)+divx n i xs ys'        = (q:qs, rs)+  where q        = xs `idx` i+        xs'      = ites q (xs `addPoly` ys') xs+        (qs, rs) = divx (n-1) (i-1) xs' (tail ys')++-- | Compute CRCs over bit-vectors. The call @crcBV n m p@ computes+-- the CRC of the message @m@ with respect to polynomial @p@. The+-- inputs are assumed to be blasted big-endian. The number+-- @n@ specifies how many bits of CRC is needed. Note that @n@+-- is actually the degree of the polynomial @p@, and thus it seems+-- redundant to pass it in. However, in a typical proof context,+-- the polynomial can be symbolic, so we cannot compute the degree+-- easily. While this can be worked-around by generating code that+-- accounts for all possible degrees, the resulting code would+-- be unnecessarily big and complicated, and much harder to reason+-- with. (Also note that a CRC is just the remainder from the+-- polynomial division, but this routine is much faster in practice.)+--+-- NB. The @n@th bit of the polynomial @p@ /must/ be set for the CRC+-- to be computed correctly. Note that the polynomial argument 'p' will+-- not even have this bit present most of the time, as it will typically+-- contain bits @0@ through @n-1@ as usual in the CRC literature. The higher+-- order @n@th bit is simply assumed to be set, as it does not make+-- sense to use a polynomial of a lesser degree. This is usually not a problem+-- since CRC polynomials are designed and expressed this way.+--+-- NB. The literature on CRC's has many variants on how CRC's are computed.+-- We follow the painless guide (<http://www.ross.net/crc/download/crc_v3.txt>)+-- and compute the CRC as follows:+--+--     * Extend the message 'm' by adding 'n' 0 bits on the right+--+--     * Divide the polynomial thus obtained by the 'p'+--+--     * The remainder is the CRC value.+--+-- There are many variants on final XOR's, reversed polynomials etc., so+-- it is essential to double check you use the correct /algorithm/.+crcBV :: Int -> [SBool] -> [SBool] -> [SBool]+crcBV n m p = take n $ go (replicate n false) (m ++ replicate n false)+  where mask = drop (length p - n) p+        go c []     = c+        go c (b:bs) = go next bs+          where c' = drop 1 c ++ [b]+                next = ite (head c) (zipWith (<+>) c' mask) c'++-- | 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+  | 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
LICENSE view
@@ -1,6 +1,6 @@ SBV: A library for Symbolic Bitvectors -Copyright (c) 2010-2011, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2010-2012, Levent Erkok (erkokl@gmail.com) All rights reserved.  Redistribution and use in source and binary forms, with or without
README view
@@ -62,7 +62,8 @@   - used in synthesis (the `sat` function with existentials)   - optimized with respect to cost functions (the 'optimize', 'maximize', and 'minimize' functions)   - quick-checked-  - used in concrete test case generation (the 'genTest' function)+  - used in concrete test case generation (the 'genTest' function), rendered as values in various+    languages, including Haskell and C.  If a predicate is not valid, `prove` will return a counterexample: An  assignment to inputs such that the predicate fails. The `sat` function will@@ -79,25 +80,25 @@  The SBV library is designed to work with any SMT-Lib compliant SMT-solver, although integration with individual solvers require some library work.-Currently, we fully support the [Yices](http://yices.csl.sri.com) SMT solver from SRI,-and the [Z3](http://research.microsoft.com/en-us/um/redmond/projects/z3/)-SMT solver from Microsoft.+Currently, we fully support +the [Z3](http://research.microsoft.com/en-us/um/redmond/projects/z3/) SMT solver from Microsoft,+and +the [Yices](http://yices.csl.sri.com) SMT solver from SRI. Both solvers are available for Windows, Linux, and Mac OSX.  Prerequisites =============-You **should** [download](http://yices.csl.sri.com/download-yices2.shtml)-and install Yices (version 2.X) on your machine, and-make sure the "yices" executable is in your path before using the sbv library,-as it is the current default solver. Alternatively, you can specify the location-of yices executable in the environment variable `SBV_YICES` and the options to yices-in `SBV_YICES_OPTIONS`. The default for the latter is `"-m -f"`.+You **should** have at least one of +Z3 [(download)](http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html), or+Yices [(download)](http://yices.csl.sri.com/download-yices2.shtml) (version 2.X) +installed on your machine, preferably both. Note that z3 is the default solver used by 'sat',+'allSat', 'prove', etc. commands. To use "yices", use the 'satWith', 'proveWith', 'allSatWith' variants. -SBV can also use Microsoft's Z3 SMT solver as a-backend [(download)](http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html).-The environment variables `SBV_Z3` and `SBV_Z3_OPTIONS` can be used for choosing executable location-and custom options.  The default for the latter is `"/in /smt2"` on Windows and `"-in -smt2"`-on Mac and Linux. You should download Z3 version 3.2 or later.+Make sure the executables for the solvers are in your path. Alternatively, you can specify the location+of the yices executable in the environment variable `SBV_YICES` and the options to yices in `SBV_YICES_OPTIONS`.+(The default for the latter is `"-m -f"`). Similarly the environment variables `SBV_Z3` and `SBV_Z3_OPTIONS` can+be used for choosing executable location and custom options for Z3.  (The default for the latter is+`"/in /smt2"` on Windows and `"-in -smt2"` on Mac and Linux. You should use Z3 version 3.2 or later.)  Examples =========
RELEASENOTES view
@@ -1,6 +1,33 @@ Hackage: <http://hackage.haskell.org/package/sbv> GitHub:  <http://github.com/LeventErkok/sbv> +Latest Hackage released version: 1.0++======================================================================+Version 1.0, 2012-02-13++ Library:+  * Z3 is now the "default" SMT solver. Yices is still available, but+    has to be specifically selected. (Use satWith, allSatWith, proveWith, etc.)+  * Better handling of the pConstrain probability threshold for test+    case generation and quickCheck purposes.+  * Add 'renderTest', which accompanies 'genTest' to render test+    vectors as Haskell/C/Forte program segments.+  * Add 'expectedValue' which can compute the expected value of+    a symbolic value under the given constraints. Useful for statistical+    analysis and probability computations.+  * When saturating provable values, use forAll_ for proofs and forSome_+    for sat/allSat. (Previously we were allways using forAll_, which is+    not incorrect but less intuitive.)+  * add function:+      extractModels :: SatModel a => AllSatResult -> [a]+    which simplifies accessing allSat results greatly.+ Code-generation:+  * add "cgGenerateMakefile" which allows the user to choose if SBV+    should generate a Makefile. (default: True)+ Other+  * Changes to make it compile with GHC 7.4.1.+ ====================================================================== Version 0.9.24, 2011-12-28
SBVUnitTest/GoldFiles/U2Bridge.gold view
@@ -3,13 +3,13 @@   s1 = 1 :: SWord8   s2 = 0 :: SWord8   s3 = True-  s4 = 1 :: SWord8+  s4 = 0 :: SWord8   s5 = 0 :: SWord8   s6 = False   s7 = 3 :: SWord8   s8 = 2 :: SWord8   s9 = True-  s10 = 0 :: SWord8+  s10 = 1 :: SWord8   s11 = 0 :: SWord8   s12 = False   s13 = 1 :: SWord8
SBVUnitTest/GoldFiles/addSub.gold view
@@ -32,9 +32,12 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> +/* The boolean type */+typedef bool SBool;+ /* Unsigned bit-vectors */-typedef uint8_t  SBool  ; typedef uint8_t  SWord8 ; typedef uint16_t SWord16; typedef uint32_t SWord32;@@ -58,6 +61,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include <stdio.h> #include "addSub.h" @@ -65,9 +69,9 @@ {   SWord8 sum;   SWord8 dif;-  +   addSub(76, 92, &sum, &dif);-  +   printf("addSub(76, 92, &sum, &dif) ->\n");   printf("  sum = %"PRIu8"\n", sum);   printf("  dif = %"PRIu8"\n", dif);@@ -80,6 +84,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include "addSub.h"  void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,@@ -89,7 +94,7 @@   const SWord8 s1 = y;   const SWord8 s2 = s0 + s1;   const SWord8 s3 = s0 - s1;-  +   *sum = s2;   *dif = s3; }
SBVUnitTest/GoldFiles/aes128Dec.gold view
@@ -32,9 +32,12 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> +/* The boolean type */+typedef bool SBool;+ /* Unsigned bit-vectors */-typedef uint8_t  SBool  ; typedef uint8_t  SWord8 ; typedef uint16_t SWord16; typedef uint32_t SWord32;@@ -57,6 +60,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include <stdio.h> #include "aes128Dec.h" @@ -65,25 +69,25 @@   const SWord32 pt[4] = {       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL   };-  +   printf("Contents of input array pt:\n");   int pt_ctr;   for(pt_ctr = 0; pt_ctr < 4 ; ++pt_ctr)     printf("  pt[%d] = 0x%08"PRIx32"UL\n", pt_ctr ,pt[pt_ctr]);-  +   const SWord32 key[4] = {       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL   };-  +   printf("Contents of input array key:\n");   int key_ctr;   for(key_ctr = 0; key_ctr < 4 ; ++key_ctr)     printf("  key[%d] = 0x%08"PRIx32"UL\n", key_ctr ,key[key_ctr]);-  +   SWord32 ct[4];-  +   aes128Dec(pt, key, ct);-  +   printf("aes128Dec(pt, key, ct) ->\n");   int ct_ctr;   for(ct_ctr = 0; ct_ctr < 4 ; ++ct_ctr)@@ -97,6 +101,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include "aes128Dec.h"  void aes128Dec(const SWord32 *pt, const SWord32 *key, SWord32 *ct)@@ -2591,7 +2596,7 @@   const SWord16 s3368 = (((SWord16) s3365) << 8) | ((SWord16) s3367);   const SWord32 s3369 = (((SWord32) s3363) << 16) | ((SWord32) s3368);   const SWord32 s3370 = s7 ^ s3369;-  +   ct[0] = s3330;   ct[1] = s3344;   ct[2] = s3358;
SBVUnitTest/GoldFiles/aes128Enc.gold view
@@ -32,9 +32,12 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> +/* The boolean type */+typedef bool SBool;+ /* Unsigned bit-vectors */-typedef uint8_t  SBool  ; typedef uint8_t  SWord8 ; typedef uint16_t SWord16; typedef uint32_t SWord32;@@ -57,6 +60,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include <stdio.h> #include "aes128Enc.h" @@ -65,25 +69,25 @@   const SWord32 pt[4] = {       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL   };-  +   printf("Contents of input array pt:\n");   int pt_ctr;   for(pt_ctr = 0; pt_ctr < 4 ; ++pt_ctr)     printf("  pt[%d] = 0x%08"PRIx32"UL\n", pt_ctr ,pt[pt_ctr]);-  +   const SWord32 key[4] = {       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL   };-  +   printf("Contents of input array key:\n");   int key_ctr;   for(key_ctr = 0; key_ctr < 4 ; ++key_ctr)     printf("  key[%d] = 0x%08"PRIx32"UL\n", key_ctr ,key[key_ctr]);-  +   SWord32 ct[4];-  +   aes128Enc(pt, key, ct);-  +   printf("aes128Enc(pt, key, ct) ->\n");   int ct_ctr;   for(ct_ctr = 0; ct_ctr < 4 ; ++ct_ctr)@@ -97,6 +101,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include "aes128Enc.h"  void aes128Enc(const SWord32 *pt, const SWord32 *key, SWord32 *ct)@@ -1149,7 +1154,7 @@   const SWord32 s2036 = (((SWord32) s2030) << 16) | ((SWord32) s2035);   const SWord32 s2037 = s1972 ^ s2024;   const SWord32 s2038 = s2036 ^ s2037;-  +   ct[0] = s1995;   ct[1] = s2010;   ct[2] = s2025;
SBVUnitTest/GoldFiles/aes128Lib.gold view
@@ -3,6 +3,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include "aes128Lib.h"  void aes128KeySchedule(const SWord32 *key, SWord32 *encKS,@@ -1644,7 +1645,7 @@   const SWord8  s1779 = s1773 ^ s1778;   const SWord16 s1780 = (((SWord16) s1772) << 8) | ((SWord16) s1779);   const SWord32 s1781 = (((SWord32) s1765) << 16) | ((SWord32) s1780);-  +   encKS[0] = s0;   encKS[1] = s1;   encKS[2] = s2;@@ -1740,6 +1741,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include "aes128Lib.h"  void aes128BlockEncrypt(const SWord32 *pt, const SWord32 *xkey,@@ -2643,7 +2645,7 @@   const SWord16 s1886 = (((SWord16) s1883) << 8) | ((SWord16) s1885);   const SWord32 s1887 = (((SWord32) s1881) << 16) | ((SWord32) s1886);   const SWord32 s1888 = s47 ^ s1887;-  +   ct[0] = s1848;   ct[1] = s1862;   ct[2] = s1876;@@ -2655,6 +2657,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include "aes128Lib.h"  void aes128BlockDecrypt(const SWord32 *ct, const SWord32 *xkey,@@ -3558,7 +3561,7 @@   const SWord16 s1886 = (((SWord16) s1883) << 8) | ((SWord16) s1885);   const SWord32 s1887 = (((SWord32) s1881) << 16) | ((SWord32) s1886);   const SWord32 s1888 = s47 ^ s1887;-  +   pt[0] = s1848;   pt[1] = s1862;   pt[2] = s1876;@@ -3573,9 +3576,12 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> +/* The boolean type */+typedef bool SBool;+ /* Unsigned bit-vectors */-typedef uint8_t  SBool  ; typedef uint8_t  SWord8 ; typedef uint16_t SWord16; typedef uint32_t SWord32;@@ -3603,6 +3609,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include <stdio.h> #include "aes128Lib.h" @@ -3611,17 +3618,17 @@   const SWord32 key[4] = {       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL   };-  +   printf("Contents of input array key:\n");   int key_ctr;   for(key_ctr = 0; key_ctr < 4 ; ++key_ctr)     printf("  key[%d] = 0x%08"PRIx32"UL\n", key_ctr ,key[key_ctr]);-  +   SWord32 encKS[44];   SWord32 decKS[44];-  +   aes128KeySchedule(key, encKS, decKS);-  +   printf("aes128KeySchedule(key, encKS, decKS) ->\n");   int encKS_ctr;   for(encKS_ctr = 0; encKS_ctr < 44 ; ++encKS_ctr)@@ -3636,12 +3643,12 @@   const SWord32 pt[4] = {       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL   };-  +   printf("Contents of input array pt:\n");   int pt_ctr;   for(pt_ctr = 0; pt_ctr < 4 ; ++pt_ctr)     printf("  pt[%d] = 0x%08"PRIx32"UL\n", pt_ctr ,pt[pt_ctr]);-  +   const SWord32 xkey[44] = {       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL,       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL,@@ -3655,16 +3662,16 @@       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL,       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL   };-  +   printf("Contents of input array xkey:\n");   int xkey_ctr;   for(xkey_ctr = 0; xkey_ctr < 44 ; ++xkey_ctr)     printf("  xkey[%d] = 0x%08"PRIx32"UL\n", xkey_ctr ,xkey[xkey_ctr]);-  +   SWord32 ct[4];-  +   aes128BlockEncrypt(pt, xkey, ct);-  +   printf("aes128BlockEncrypt(pt, xkey, ct) ->\n");   int ct_ctr;   for(ct_ctr = 0; ct_ctr < 4 ; ++ct_ctr)@@ -3676,12 +3683,12 @@   const SWord32 ct[4] = {       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL   };-  +   printf("Contents of input array ct:\n");   int ct_ctr;   for(ct_ctr = 0; ct_ctr < 4 ; ++ct_ctr)     printf("  ct[%d] = 0x%08"PRIx32"UL\n", ct_ctr ,ct[ct_ctr]);-  +   const SWord32 xkey[44] = {       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL,       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL,@@ -3695,16 +3702,16 @@       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL,       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL   };-  +   printf("Contents of input array xkey:\n");   int xkey_ctr;   for(xkey_ctr = 0; xkey_ctr < 44 ; ++xkey_ctr)     printf("  xkey[%d] = 0x%08"PRIx32"UL\n", xkey_ctr ,xkey[xkey_ctr]);-  +   SWord32 pt[4];-  +   aes128BlockDecrypt(ct, xkey, pt);-  +   printf("aes128BlockDecrypt(ct, xkey, pt) ->\n");   int pt_ctr;   for(pt_ctr = 0; pt_ctr < 4 ; ++pt_ctr)@@ -3717,19 +3724,20 @@   printf("** Driver run for aes128KeySchedule:\n");   printf("====================================\n");   aes128KeySchedule_driver();-  +   printf("=====================================\n");   printf("** Driver run for aes128BlockEncrypt:\n");   printf("=====================================\n");   aes128BlockEncrypt_driver();-  +   printf("=====================================\n");   printf("** Driver run for aes128BlockDecrypt:\n");   printf("=====================================\n");   aes128BlockDecrypt_driver();-  +   return 0;-}== END: "aes128Lib_driver.c" ==================+}+== END: "aes128Lib_driver.c" ================== == BEGIN: "Makefile" ================ # Makefile for aes128Lib. Automatically generated by SBV. Do not edit!
SBVUnitTest/GoldFiles/cgUninterpret.gold view
@@ -32,9 +32,12 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> +/* The boolean type */+typedef bool SBool;+ /* Unsigned bit-vectors */-typedef uint8_t  SBool  ; typedef uint8_t  SWord8 ; typedef uint16_t SWord16; typedef uint32_t SWord32;@@ -57,6 +60,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include <stdio.h> #include "tstShiftLeft.h" @@ -65,15 +69,15 @@   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;@@ -84,6 +88,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include "tstShiftLeft.h"  /* User specified custom code for "SBV_SHIFTLEFT" */@@ -99,7 +104,7 @@   const SWord32 s4 = /* Uninterpreted function */ SBV_SHIFTLEFT(s1,                                                                 s2);   const SWord32 s5 = s3 + s4;-  +   return s5; } == END: "tstShiftLeft.c" ==================
SBVUnitTest/GoldFiles/codeGen1.gold view
@@ -32,9 +32,12 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> +/* The boolean type */+typedef bool SBool;+ /* Unsigned bit-vectors */-typedef uint8_t  SBool  ; typedef uint8_t  SWord8 ; typedef uint16_t SWord16; typedef uint32_t SWord32;@@ -58,6 +61,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include <stdio.h> #include "foo.h" @@ -80,18 +84,18 @@       0x0000000000000000LL, 0x0000000000000000LL, 0x0000000000000000LL,       0x0000000000000000LL, 0x0000000000000000LL, 0x0000000000000000LL   };-  +   printf("Contents of input array xArr:\n");   int xArr_ctr;   for(xArr_ctr = 0; xArr_ctr < 45 ; ++xArr_ctr)     printf("  xArr[%d] = %"PRId64"LL\n", xArr_ctr ,xArr[xArr_ctr]);-  +   SWord16 z;   SInt16 zArr[7];   SInt64 yArr[45];-  +   const SInt16 __result = foo(0x0000, xArr, &z, zArr, yArr);-  +   printf("foo(0x0000, xArr, &z, zArr, yArr) = %"PRId16"\n", __result);   printf("  z = 0x%04"PRIx16"U\n", z);   int zArr_ctr;@@ -109,6 +113,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include "foo.h"  SInt16 foo(const SInt16 x, const SInt64 *xArr, SWord16 *z,@@ -162,7 +167,7 @@   const SInt64 s45 = xArr[44];   const SInt16 s48 = s0 + 0x0001;   const SInt16 s50 = s0 * 0x0002;-  +   *z = 0x0005U;   zArr[0] = s48;   zArr[1] = s48;
SBVUnitTest/GoldFiles/crcUSB5_1.gold view
@@ -32,9 +32,12 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> +/* The boolean type */+typedef bool SBool;+ /* Unsigned bit-vectors */-typedef uint8_t  SBool  ; typedef uint8_t  SWord8 ; typedef uint16_t SWord16; typedef uint32_t SWord32;@@ -57,13 +60,14 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include <stdio.h> #include "crcUSB5.h"  int main(void) {   const SWord16 __result = crcUSB5(0xfedcU);-  +   printf("crcUSB5(0xfedcU) = 0x%04"PRIx16"U\n", __result);    return 0;@@ -74,6 +78,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include "crcUSB5.h"  SWord16 crcUSB5(const SWord16 msg)@@ -101,77 +106,72 @@   const SBool   s31 = 0x0000U != s30;   const SWord16 s33 = s0 & 0x0001U;   const SBool   s34 = 0x0000U != s33;-  const SBool   s35 = (~s13) & 0x01U;+  const SBool   s35 = !s13;   const SBool   s36 = s4 ? s35 : s13;-  const SBool   s37 = (~s16) & 0x01U;+  const SBool   s37 = !s16;   const SBool   s38 = s7 ? s37 : s16;-  const SBool   s39 = (~s19) & 0x01U;+  const SBool   s39 = !s19;   const SBool   s40 = s4 ? s39 : s19;-  const SBool   s41 = (~s40) & 0x01U;+  const SBool   s41 = !s40;   const SBool   s42 = s10 ? s41 : s40;-  const SBool   s43 = (~s22) & 0x01U;+  const SBool   s43 = !s22;   const SBool   s44 = s7 ? s43 : s22;-  const SBool   s45 = (~s44) & 0x01U;+  const SBool   s45 = !s44;   const SBool   s46 = s36 ? s45 : s44;-  const SBool   s47 = (~s25) & 0x01U;+  const SBool   s47 = !s25;   const SBool   s48 = s10 ? s47 : s25;-  const SBool   s49 = (~s48) & 0x01U;+  const SBool   s49 = !s48;   const SBool   s50 = s38 ? s49 : s48;-  const SBool   s51 = (~s28) & 0x01U;+  const SBool   s51 = !s28;   const SBool   s52 = s36 ? s51 : s28;-  const SBool   s53 = (~s52) & 0x01U;+  const SBool   s53 = !s52;   const SBool   s54 = s42 ? s53 : s52;-  const SBool   s55 = (~s31) & 0x01U;+  const SBool   s55 = !s31;   const SBool   s56 = s38 ? s55 : s31;-  const SBool   s57 = (~s56) & 0x01U;+  const SBool   s57 = !s56;   const SBool   s58 = s46 ? s57 : s56;-  const SBool   s59 = (~s34) & 0x01U;+  const SBool   s59 = !s34;   const SBool   s60 = s42 ? s59 : s34;-  const SBool   s61 = (~s60) & 0x01U;+  const SBool   s61 = !s60;   const SBool   s62 = s50 ? s61 : s60;-  const SBool   s63 = s46 ? 1 : 0;-  const SBool   s64 = (~s63) & 0x01U;-  const SBool   s65 = s54 ? s64 : s63;-  const SBool   s66 = s50 ? 1 : 0;-  const SBool   s67 = (~s66) & 0x01U;-  const SBool   s68 = s58 ? s67 : s66;-  const SBool   s69 = s54 ? 1 : 0;-  const SBool   s70 = (~s69) & 0x01U;-  const SBool   s71 = s62 ? s70 : s69;-  const SBool   s72 = s58 ? 1 : 0;-  const SBool   s73 = s62 ? 1 : 0;-  const SWord16 s74 = s73 ? 0x0001U : 0x0000U;-  const SWord16 s75 = 0x0002U | s74;-  const SWord16 s76 = s72 ? s75 : s74;-  const SWord16 s77 = 0x0004U | s76;-  const SWord16 s78 = s71 ? s77 : s76;-  const SWord16 s79 = 0x0008U | s78;-  const SWord16 s80 = s68 ? s79 : s78;-  const SWord16 s81 = 0x0010U | s80;-  const SWord16 s82 = s65 ? s81 : s80;-  const SWord16 s83 = 0x0020U | s82;-  const SWord16 s84 = s34 ? s83 : s82;-  const SWord16 s85 = 0x0040U | s84;-  const SWord16 s86 = s31 ? s85 : s84;-  const SWord16 s87 = 0x0080U | s86;-  const SWord16 s88 = s28 ? s87 : s86;-  const SWord16 s89 = 0x0100U | s88;-  const SWord16 s90 = s25 ? s89 : s88;-  const SWord16 s91 = 0x0200U | s90;-  const SWord16 s92 = s22 ? s91 : s90;-  const SWord16 s93 = 0x0400U | s92;-  const SWord16 s94 = s19 ? s93 : s92;-  const SWord16 s96 = s94 | 0x0800U;-  const SWord16 s97 = s16 ? s96 : s94;-  const SWord16 s99 = s97 | 0x1000U;-  const SWord16 s100 = s13 ? s99 : s97;-  const SWord16 s102 = s100 | 0x2000U;-  const SWord16 s103 = s10 ? s102 : s100;-  const SWord16 s105 = s103 | 0x4000U;-  const SWord16 s106 = s7 ? s105 : s103;-  const SWord16 s108 = s106 | 0x8000U;-  const SWord16 s109 = s4 ? s108 : s106;-  -  return s109;+  const SBool   s63 = !s46;+  const SBool   s64 = s54 ? s63 : s46;+  const SBool   s65 = !s50;+  const SBool   s66 = s58 ? s65 : s50;+  const SBool   s67 = !s54;+  const SBool   s68 = s62 ? s67 : s54;+  const SWord16 s69 = s62 ? 0x0001U : 0x0000U;+  const SWord16 s70 = 0x0002U | s69;+  const SWord16 s71 = s58 ? s70 : s69;+  const SWord16 s72 = 0x0004U | s71;+  const SWord16 s73 = s68 ? s72 : s71;+  const SWord16 s74 = 0x0008U | s73;+  const SWord16 s75 = s66 ? s74 : s73;+  const SWord16 s76 = 0x0010U | s75;+  const SWord16 s77 = s64 ? s76 : s75;+  const SWord16 s78 = 0x0020U | s77;+  const SWord16 s79 = s34 ? s78 : s77;+  const SWord16 s80 = 0x0040U | s79;+  const SWord16 s81 = s31 ? s80 : s79;+  const SWord16 s82 = 0x0080U | s81;+  const SWord16 s83 = s28 ? s82 : s81;+  const SWord16 s84 = 0x0100U | s83;+  const SWord16 s85 = s25 ? s84 : s83;+  const SWord16 s86 = 0x0200U | s85;+  const SWord16 s87 = s22 ? s86 : s85;+  const SWord16 s88 = 0x0400U | s87;+  const SWord16 s89 = s19 ? s88 : s87;+  const SWord16 s91 = s89 | 0x0800U;+  const SWord16 s92 = s16 ? s91 : s89;+  const SWord16 s94 = s92 | 0x1000U;+  const SWord16 s95 = s13 ? s94 : s92;+  const SWord16 s97 = s95 | 0x2000U;+  const SWord16 s98 = s10 ? s97 : s95;+  const SWord16 s100 = s98 | 0x4000U;+  const SWord16 s101 = s7 ? s100 : s98;+  const SWord16 s103 = s101 | 0x8000U;+  const SWord16 s104 = s4 ? s103 : s101;++  return s104; } == END: "crcUSB5.c" ==================
SBVUnitTest/GoldFiles/crcUSB5_2.gold view
@@ -32,9 +32,12 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> +/* The boolean type */+typedef bool SBool;+ /* Unsigned bit-vectors */-typedef uint8_t  SBool  ; typedef uint8_t  SWord8 ; typedef uint16_t SWord16; typedef uint32_t SWord32;@@ -57,13 +60,14 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include <stdio.h> #include "crcUSB5.h"  int main(void) {   const SWord16 __result = crcUSB5(0xfedcU);-  +   printf("crcUSB5(0xfedcU) = 0x%04"PRIx16"U\n", __result);    return 0;@@ -74,6 +78,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include "crcUSB5.h"  SWord16 crcUSB5(const SWord16 msg)@@ -88,95 +93,95 @@   const SBool   s11 = 0x0000U != s10;   const SWord16 s13 = s1 & 0x1000U;   const SBool   s14 = 0x0000U != s13;-  const SBool   s15 = (~s14) & 0x01U;+  const SBool   s15 = !s14;   const SBool   s16 = s5 ? s15 : s14;   const SWord16 s18 = s1 & 0x0800U;   const SBool   s19 = 0x0000U != s18;-  const SBool   s20 = (~s19) & 0x01U;+  const SBool   s20 = !s19;   const SBool   s21 = s8 ? s20 : s19;   const SWord16 s23 = s1 & 0x0400U;   const SBool   s24 = 0x0000U != s23;-  const SBool   s25 = (~s24) & 0x01U;+  const SBool   s25 = !s24;   const SBool   s26 = s5 ? s25 : s24;-  const SBool   s27 = (~s26) & 0x01U;+  const SBool   s27 = !s26;   const SBool   s28 = s11 ? s27 : s26;   const SWord16 s30 = s1 & 0x0200U;   const SBool   s31 = 0x0000U != s30;-  const SBool   s32 = (~s31) & 0x01U;+  const SBool   s32 = !s31;   const SBool   s33 = s8 ? s32 : s31;-  const SBool   s34 = (~s33) & 0x01U;+  const SBool   s34 = !s33;   const SBool   s35 = s16 ? s34 : s33;   const SWord16 s37 = s1 & 0x0100U;   const SBool   s38 = 0x0000U != s37;-  const SBool   s39 = (~s38) & 0x01U;+  const SBool   s39 = !s38;   const SBool   s40 = s11 ? s39 : s38;-  const SBool   s41 = (~s40) & 0x01U;+  const SBool   s41 = !s40;   const SBool   s42 = s21 ? s41 : s40;   const SWord16 s44 = s1 & 0x0080U;   const SBool   s45 = 0x0000U != s44;-  const SBool   s46 = (~s45) & 0x01U;+  const SBool   s46 = !s45;   const SBool   s47 = s16 ? s46 : s45;-  const SBool   s48 = (~s47) & 0x01U;+  const SBool   s48 = !s47;   const SBool   s49 = s28 ? s48 : s47;   const SWord16 s51 = s1 & 0x0040U;   const SBool   s52 = 0x0000U != s51;-  const SBool   s53 = (~s52) & 0x01U;+  const SBool   s53 = !s52;   const SBool   s54 = s21 ? s53 : s52;-  const SBool   s55 = (~s54) & 0x01U;+  const SBool   s55 = !s54;   const SBool   s56 = s35 ? s55 : s54;   const SWord16 s58 = s1 & 0x0020U;   const SBool   s59 = 0x0000U != s58;-  const SBool   s60 = (~s59) & 0x01U;+  const SBool   s60 = !s59;   const SBool   s61 = s28 ? s60 : s59;-  const SBool   s62 = (~s61) & 0x01U;+  const SBool   s62 = !s61;   const SBool   s63 = s42 ? s62 : s61;-  const SBool   s64 = (~s5) & 0x01U;+  const SBool   s64 = !s5;   const SBool   s65 = s5 ? s64 : s5;-  const SBool   s66 = (~s8) & 0x01U;+  const SBool   s66 = !s8;   const SBool   s67 = s8 ? s66 : s8;-  const SBool   s68 = (~s11) & 0x01U;+  const SBool   s68 = !s11;   const SBool   s69 = s11 ? s68 : s11;-  const SBool   s70 = (~s16) & 0x01U;+  const SBool   s70 = !s16;   const SBool   s71 = s16 ? s70 : s16;-  const SBool   s72 = (~s21) & 0x01U;+  const SBool   s72 = !s21;   const SBool   s73 = s21 ? s72 : s21;-  const SBool   s74 = (~s28) & 0x01U;+  const SBool   s74 = !s28;   const SBool   s75 = s28 ? s74 : s28;-  const SBool   s76 = (~s35) & 0x01U;+  const SBool   s76 = !s35;   const SBool   s77 = s35 ? s76 : s35;-  const SBool   s78 = (~s42) & 0x01U;+  const SBool   s78 = !s42;   const SBool   s79 = s42 ? s78 : s42;-  const SBool   s80 = (~s49) & 0x01U;+  const SBool   s80 = !s49;   const SBool   s81 = s49 ? s80 : s49;-  const SBool   s82 = (~s56) & 0x01U;+  const SBool   s82 = !s56;   const SBool   s83 = s56 ? s82 : s56;-  const SBool   s84 = (~s63) & 0x01U;+  const SBool   s84 = !s63;   const SBool   s85 = s63 ? s84 : s63;   const SWord16 s87 = s1 & 0x0010U;   const SBool   s88 = 0x0000U != s87;-  const SBool   s89 = (~s88) & 0x01U;+  const SBool   s89 = !s88;   const SBool   s90 = s35 ? s89 : s88;-  const SBool   s91 = (~s90) & 0x01U;+  const SBool   s91 = !s90;   const SBool   s92 = s49 ? s91 : s90;   const SWord16 s94 = s1 & 0x0008U;   const SBool   s95 = 0x0000U != s94;-  const SBool   s96 = (~s95) & 0x01U;+  const SBool   s96 = !s95;   const SBool   s97 = s42 ? s96 : s95;-  const SBool   s98 = (~s97) & 0x01U;+  const SBool   s98 = !s97;   const SBool   s99 = s56 ? s98 : s97;   const SWord16 s101 = s1 & 0x0004U;   const SBool   s102 = 0x0000U != s101;-  const SBool   s103 = (~s102) & 0x01U;+  const SBool   s103 = !s102;   const SBool   s104 = s49 ? s103 : s102;-  const SBool   s105 = (~s104) & 0x01U;+  const SBool   s105 = !s104;   const SBool   s106 = s63 ? s105 : s104;   const SWord16 s108 = s1 & 0x0002U;   const SBool   s109 = 0x0000U != s108;-  const SBool   s110 = (~s109) & 0x01U;+  const SBool   s110 = !s109;   const SBool   s111 = s56 ? s110 : s109;   const SWord16 s113 = s1 & 0x0001U;   const SBool   s114 = 0x0000U != s113;-  const SBool   s115 = (~s114) & 0x01U;+  const SBool   s115 = !s114;   const SBool   s116 = s63 ? s115 : s114;   const SWord16 s117 = s116 ? 0x0001U : 0x0000U;   const SWord16 s118 = 0x0002U | s117;@@ -210,7 +215,7 @@   const SWord16 s146 = 0x8000U | s145;   const SWord16 s147 = s65 ? s146 : s145;   const SWord16 s148 = s1 | s147;-  +   return s148; } == END: "crcUSB5.c" ==================
SBVUnitTest/GoldFiles/fib1.gold view
@@ -32,9 +32,12 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> +/* The boolean type */+typedef bool SBool;+ /* Unsigned bit-vectors */-typedef uint8_t  SBool  ; typedef uint8_t  SWord8 ; typedef uint16_t SWord16; typedef uint32_t SWord32;@@ -57,13 +60,14 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include <stdio.h> #include "fib1.h"  int main(void) {   const SWord64 __result = fib1(0x000000000000000cULL);-  +   printf("fib1(0x000000000000000cULL) = 0x%016"PRIx64"ULL\n", __result);    return 0;@@ -74,6 +78,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include "fib1.h"  SWord64 fib1(const SWord64 n)@@ -207,7 +212,7 @@   const SWord64 s244 = s6 ? 0x0000000000000001ULL : s243;   const SWord64 s245 = s4 ? 0x0000000000000001ULL : s244;   const SWord64 s246 = s2 ? 0x0000000000000000ULL : s245;-  +   return s246; } == END: "fib1.c" ==================
SBVUnitTest/GoldFiles/fib2.gold view
@@ -32,9 +32,12 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> +/* The boolean type */+typedef bool SBool;+ /* Unsigned bit-vectors */-typedef uint8_t  SBool  ; typedef uint8_t  SWord8 ; typedef uint16_t SWord16; typedef uint32_t SWord32;@@ -57,13 +60,14 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include <stdio.h> #include "fib2.h"  int main(void) {   const SWord64 __result = fib2(0x0000000000000014ULL);-  +   printf("fib2(0x0000000000000014ULL) = 0x%016"PRIx64"ULL\n", __result);    return 0;@@ -74,6 +78,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include "fib2.h"  SWord64 fib2(const SWord64 n)@@ -114,7 +119,7 @@       0x000003af9a19bbd9ULL, 0x000005f6c7b064e2ULL, 0x000009a661ca20bbULL   };   const SWord64 s65 = s0 >= 65 ? 0x0000000000000000ULL : table0[s0];-  +   return s65; } == END: "fib2.c" ==================
SBVUnitTest/GoldFiles/gcd.gold view
@@ -32,9 +32,12 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> +/* The boolean type */+typedef bool SBool;+ /* Unsigned bit-vectors */-typedef uint8_t  SBool  ; typedef uint8_t  SWord8 ; typedef uint16_t SWord16; typedef uint32_t SWord32;@@ -57,13 +60,14 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include <stdio.h> #include "sgcd.h"  int main(void) {   const SWord8 __result = sgcd(55, 154);-  +   printf("sgcd(55, 154) = %"PRIu8"\n", __result);    return 0;@@ -74,6 +78,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include "sgcd.h"  SWord8 sgcd(const SWord8 x, const SWord8 y)@@ -126,7 +131,7 @@   const SWord8 s46 = s9 ? s5 : s45;   const SWord8 s47 = s6 ? s1 : s46;   const SWord8 s48 = s3 ? s0 : s47;-  +   return s48; } == END: "sgcd.c" ==================
SBVUnitTest/GoldFiles/legato_c.gold view
@@ -32,9 +32,12 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> +/* The boolean type */+typedef bool SBool;+ /* Unsigned bit-vectors */-typedef uint8_t  SBool  ; typedef uint8_t  SWord8 ; typedef uint16_t SWord16; typedef uint32_t SWord32;@@ -58,6 +61,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include <stdio.h> #include "legatoMult.h" @@ -65,9 +69,9 @@ {   SWord8 hi;   SWord8 lo;-  +   legatoMult(87, 92, &hi, &lo);-  +   printf("legatoMult(87, 92, &hi, &lo) ->\n");   printf("  hi = %"PRIu8"\n", hi);   printf("  lo = %"PRIu8"\n", lo);@@ -80,6 +84,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include "legatoMult.h"  void legatoMult(const SWord8 x, const SWord8 y, SWord8 *hi,@@ -89,22 +94,22 @@   const SWord8 s1 = y;   const SWord8 s3 = s0 & 1;   const SBool  s5 = s3 != 0;-  const SBool  s6 = 0 == s5;+  const SBool  s6 = false == s5;   const SWord8 s7 = (s0 >> 1) | (s0 << 7);   const SWord8 s9 = s7 & 127;   const SWord8 s10 = 1 & s9;   const SBool  s11 = 0 != s10;-  const SBool  s12 = 0 == s11;+  const SBool  s12 = false == s11;   const SWord8 s13 = (s9 >> 1) | (s9 << 7);   const SWord8 s14 = 127 & s13;   const SWord8 s15 = 1 & s14;   const SBool  s16 = 0 != s15;-  const SBool  s17 = 0 == s16;+  const SBool  s17 = false == s16;   const SWord8 s18 = (s14 >> 1) | (s14 << 7);   const SWord8 s19 = 127 & s18;   const SWord8 s20 = 1 & s19;   const SBool  s21 = 0 != s20;-  const SBool  s22 = 0 == s21;+  const SBool  s22 = false == s21;   const SWord8 s24 = s5 ? 128 : 0;   const SWord8 s25 = 1 & s24;   const SBool  s26 = 0 != s25;@@ -117,7 +122,7 @@   const SWord8 s33 = s29 ? s31 : s32;   const SWord8 s34 = 1 & s33;   const SBool  s35 = 0 != s34;-  const SBool  s36 = 0 == s35;+  const SBool  s36 = false == s35;   const SWord8 s37 = (s24 >> 1) | (s24 << 7);   const SWord8 s38 = 128 | s37;   const SWord8 s39 = 127 & s37;@@ -136,7 +141,7 @@   const SWord8 s52 = s48 ? s50 : s51;   const SWord8 s53 = 1 & s52;   const SBool  s54 = 0 != s53;-  const SBool  s55 = 0 == s54;+  const SBool  s55 = false == s54;   const SWord8 s56 = (s40 >> 1) | (s40 << 7);   const SWord8 s57 = 128 | s56;   const SWord8 s58 = 127 & s56;@@ -155,7 +160,7 @@   const SWord8 s71 = s67 ? s69 : s70;   const SWord8 s72 = 1 & s71;   const SBool  s73 = 0 != s72;-  const SBool  s74 = 0 == s73;+  const SBool  s74 = false == s73;   const SWord8 s75 = (s59 >> 1) | (s59 << 7);   const SWord8 s76 = 128 | s75;   const SWord8 s77 = 127 & s75;@@ -174,7 +179,7 @@   const SWord8 s90 = s86 ? s88 : s89;   const SWord8 s91 = 1 & s90;   const SBool  s92 = 0 != s91;-  const SBool  s93 = 0 == s92;+  const SBool  s93 = false == s92;   const SWord8 s94 = (s78 >> 1) | (s78 << 7);   const SWord8 s95 = 128 | s94;   const SWord8 s96 = 127 & s94;@@ -279,7 +284,7 @@   const SWord8 s195 = s194 ? s88 : s89;   const SWord8 s196 = 1 & s195;   const SBool  s197 = 0 != s196;-  const SBool  s198 = 0 == s197;+  const SBool  s198 = false == s197;   const SBool  s199 = s189 < s1;   const SBool  s200 = s189 < s78;   const SBool  s201 = s199 | s200;@@ -388,7 +393,7 @@   const SWord8 s304 = s303 ? s69 : s70;   const SWord8 s305 = 1 & s304;   const SBool  s306 = 0 != s305;-  const SBool  s307 = 0 == s306;+  const SBool  s307 = false == s306;   const SBool  s308 = s298 < s1;   const SBool  s309 = s298 < s59;   const SBool  s310 = s308 | s309;@@ -410,7 +415,7 @@   const SWord8 s326 = s322 ? s324 : s325;   const SWord8 s327 = 1 & s326;   const SBool  s328 = 0 != s327;-  const SBool  s329 = 0 == s328;+  const SBool  s329 = false == s328;   const SWord8 s330 = (s314 >> 1) | (s314 << 7);   const SWord8 s331 = 128 | s330;   const SWord8 s332 = 127 & s330;@@ -515,7 +520,7 @@   const SWord8 s431 = s430 ? s324 : s325;   const SWord8 s432 = 1 & s431;   const SBool  s433 = 0 != s432;-  const SBool  s434 = 0 == s433;+  const SBool  s434 = false == s433;   const SBool  s435 = s425 < s1;   const SBool  s436 = s425 < s314;   const SBool  s437 = s435 | s436;@@ -625,7 +630,7 @@   const SWord8 s541 = s540 ? s50 : s51;   const SWord8 s542 = 1 & s541;   const SBool  s543 = 0 != s542;-  const SBool  s544 = 0 == s543;+  const SBool  s544 = false == s543;   const SBool  s545 = s535 < s1;   const SBool  s546 = s535 < s40;   const SBool  s547 = s545 | s546;@@ -647,7 +652,7 @@   const SWord8 s563 = s559 ? s561 : s562;   const SWord8 s564 = 1 & s563;   const SBool  s565 = 0 != s564;-  const SBool  s566 = 0 == s565;+  const SBool  s566 = false == s565;   const SWord8 s567 = (s551 >> 1) | (s551 << 7);   const SWord8 s568 = 128 | s567;   const SWord8 s569 = 127 & s567;@@ -666,7 +671,7 @@   const SWord8 s582 = s578 ? s580 : s581;   const SWord8 s583 = 1 & s582;   const SBool  s584 = 0 != s583;-  const SBool  s585 = 0 == s584;+  const SBool  s585 = false == s584;   const SWord8 s586 = (s570 >> 1) | (s570 << 7);   const SWord8 s587 = 128 | s586;   const SWord8 s588 = 127 & s586;@@ -771,7 +776,7 @@   const SWord8 s687 = s686 ? s580 : s581;   const SWord8 s688 = 1 & s687;   const SBool  s689 = 0 != s688;-  const SBool  s690 = 0 == s689;+  const SBool  s690 = false == s689;   const SBool  s691 = s681 < s1;   const SBool  s692 = s681 < s570;   const SBool  s693 = s691 | s692;@@ -880,7 +885,7 @@   const SWord8 s796 = s795 ? s561 : s562;   const SWord8 s797 = 1 & s796;   const SBool  s798 = 0 != s797;-  const SBool  s799 = 0 == s798;+  const SBool  s799 = false == s798;   const SBool  s800 = s790 < s1;   const SBool  s801 = s790 < s551;   const SBool  s802 = s800 | s801;@@ -902,7 +907,7 @@   const SWord8 s818 = s814 ? s816 : s817;   const SWord8 s819 = 1 & s818;   const SBool  s820 = 0 != s819;-  const SBool  s821 = 0 == s820;+  const SBool  s821 = false == s820;   const SWord8 s822 = (s806 >> 1) | (s806 << 7);   const SWord8 s823 = 128 | s822;   const SWord8 s824 = 127 & s822;@@ -1007,7 +1012,7 @@   const SWord8 s923 = s922 ? s816 : s817;   const SWord8 s924 = 1 & s923;   const SBool  s925 = 0 != s924;-  const SBool  s926 = 0 == s925;+  const SBool  s926 = false == s925;   const SBool  s927 = s917 < s1;   const SBool  s928 = s917 < s806;   const SBool  s929 = s927 | s928;@@ -1118,7 +1123,7 @@   const SWord8 s1034 = s1033 ? s31 : s32;   const SWord8 s1035 = 1 & s1034;   const SBool  s1036 = 0 != s1035;-  const SBool  s1037 = 0 == s1036;+  const SBool  s1037 = false == s1036;   const SBool  s1038 = s1028 < s1;   const SBool  s1039 = s1028 < s24;   const SBool  s1040 = s1038 | s1039;@@ -1140,7 +1145,7 @@   const SWord8 s1056 = s1052 ? s1054 : s1055;   const SWord8 s1057 = 1 & s1056;   const SBool  s1058 = 0 != s1057;-  const SBool  s1059 = 0 == s1058;+  const SBool  s1059 = false == s1058;   const SWord8 s1060 = (s1044 >> 1) | (s1044 << 7);   const SWord8 s1061 = 128 | s1060;   const SWord8 s1062 = 127 & s1060;@@ -1159,7 +1164,7 @@   const SWord8 s1075 = s1071 ? s1073 : s1074;   const SWord8 s1076 = 1 & s1075;   const SBool  s1077 = 0 != s1076;-  const SBool  s1078 = 0 == s1077;+  const SBool  s1078 = false == s1077;   const SWord8 s1079 = (s1063 >> 1) | (s1063 << 7);   const SWord8 s1080 = 128 | s1079;   const SWord8 s1081 = 127 & s1079;@@ -1178,7 +1183,7 @@   const SWord8 s1094 = s1090 ? s1092 : s1093;   const SWord8 s1095 = 1 & s1094;   const SBool  s1096 = 0 != s1095;-  const SBool  s1097 = 0 == s1096;+  const SBool  s1097 = false == s1096;   const SWord8 s1098 = (s1082 >> 1) | (s1082 << 7);   const SWord8 s1099 = 128 | s1098;   const SWord8 s1100 = 127 & s1098;@@ -1283,7 +1288,7 @@   const SWord8 s1199 = s1198 ? s1092 : s1093;   const SWord8 s1200 = 1 & s1199;   const SBool  s1201 = 0 != s1200;-  const SBool  s1202 = 0 == s1201;+  const SBool  s1202 = false == s1201;   const SBool  s1203 = s1193 < s1;   const SBool  s1204 = s1193 < s1082;   const SBool  s1205 = s1203 | s1204;@@ -1392,7 +1397,7 @@   const SWord8 s1308 = s1307 ? s1073 : s1074;   const SWord8 s1309 = 1 & s1308;   const SBool  s1310 = 0 != s1309;-  const SBool  s1311 = 0 == s1310;+  const SBool  s1311 = false == s1310;   const SBool  s1312 = s1302 < s1;   const SBool  s1313 = s1302 < s1063;   const SBool  s1314 = s1312 | s1313;@@ -1414,7 +1419,7 @@   const SWord8 s1330 = s1326 ? s1328 : s1329;   const SWord8 s1331 = 1 & s1330;   const SBool  s1332 = 0 != s1331;-  const SBool  s1333 = 0 == s1332;+  const SBool  s1333 = false == s1332;   const SWord8 s1334 = (s1318 >> 1) | (s1318 << 7);   const SWord8 s1335 = 128 | s1334;   const SWord8 s1336 = 127 & s1334;@@ -1519,7 +1524,7 @@   const SWord8 s1435 = s1434 ? s1328 : s1329;   const SWord8 s1436 = 1 & s1435;   const SBool  s1437 = 0 != s1436;-  const SBool  s1438 = 0 == s1437;+  const SBool  s1438 = false == s1437;   const SBool  s1439 = s1429 < s1;   const SBool  s1440 = s1429 < s1318;   const SBool  s1441 = s1439 | s1440;@@ -1629,7 +1634,7 @@   const SWord8 s1545 = s1544 ? s1054 : s1055;   const SWord8 s1546 = 1 & s1545;   const SBool  s1547 = 0 != s1546;-  const SBool  s1548 = 0 == s1547;+  const SBool  s1548 = false == s1547;   const SBool  s1549 = s1539 < s1;   const SBool  s1550 = s1539 < s1044;   const SBool  s1551 = s1549 | s1550;@@ -1651,7 +1656,7 @@   const SWord8 s1567 = s1563 ? s1565 : s1566;   const SWord8 s1568 = 1 & s1567;   const SBool  s1569 = 0 != s1568;-  const SBool  s1570 = 0 == s1569;+  const SBool  s1570 = false == s1569;   const SWord8 s1571 = (s1555 >> 1) | (s1555 << 7);   const SWord8 s1572 = 128 | s1571;   const SWord8 s1573 = 127 & s1571;@@ -1670,7 +1675,7 @@   const SWord8 s1586 = s1582 ? s1584 : s1585;   const SWord8 s1587 = 1 & s1586;   const SBool  s1588 = 0 != s1587;-  const SBool  s1589 = 0 == s1588;+  const SBool  s1589 = false == s1588;   const SWord8 s1590 = (s1574 >> 1) | (s1574 << 7);   const SWord8 s1591 = 128 | s1590;   const SWord8 s1592 = 127 & s1590;@@ -1775,7 +1780,7 @@   const SWord8 s1691 = s1690 ? s1584 : s1585;   const SWord8 s1692 = 1 & s1691;   const SBool  s1693 = 0 != s1692;-  const SBool  s1694 = 0 == s1693;+  const SBool  s1694 = false == s1693;   const SBool  s1695 = s1685 < s1;   const SBool  s1696 = s1685 < s1574;   const SBool  s1697 = s1695 | s1696;@@ -1884,7 +1889,7 @@   const SWord8 s1800 = s1799 ? s1565 : s1566;   const SWord8 s1801 = 1 & s1800;   const SBool  s1802 = 0 != s1801;-  const SBool  s1803 = 0 == s1802;+  const SBool  s1803 = false == s1802;   const SBool  s1804 = s1794 < s1;   const SBool  s1805 = s1794 < s1555;   const SBool  s1806 = s1804 | s1805;@@ -1906,7 +1911,7 @@   const SWord8 s1822 = s1818 ? s1820 : s1821;   const SWord8 s1823 = 1 & s1822;   const SBool  s1824 = 0 != s1823;-  const SBool  s1825 = 0 == s1824;+  const SBool  s1825 = false == s1824;   const SWord8 s1826 = (s1810 >> 1) | (s1810 << 7);   const SWord8 s1827 = 128 | s1826;   const SWord8 s1828 = 127 & s1826;@@ -2011,7 +2016,7 @@   const SWord8 s1927 = s1926 ? s1820 : s1821;   const SWord8 s1928 = 1 & s1927;   const SBool  s1929 = 0 != s1928;-  const SBool  s1930 = 0 == s1929;+  const SBool  s1930 = false == s1929;   const SBool  s1931 = s1921 < s1;   const SBool  s1932 = s1921 < s1810;   const SBool  s1933 = s1931 | s1932;@@ -2123,7 +2128,7 @@   const SWord8 s2039 = s2037 ? s2038 : s19;   const SWord8 s2040 = 1 & s2039;   const SBool  s2041 = 0 != s2040;-  const SBool  s2042 = 0 == s2041;+  const SBool  s2042 = false == s2041;   const SWord8 s2043 = (s1 >> 1) | (s1 << 7);   const SWord8 s2044 = 127 & s2043;   const SWord8 s2045 = 1 & s2044;@@ -2140,7 +2145,7 @@   const SWord8 s2056 = s2052 ? s2054 : s2055;   const SWord8 s2057 = 1 & s2056;   const SBool  s2058 = 0 != s2057;-  const SBool  s2059 = 0 == s2058;+  const SBool  s2059 = false == s2058;   const SWord8 s2060 = (s2044 >> 1) | (s2044 << 7);   const SWord8 s2061 = 128 | s2060;   const SWord8 s2062 = 127 & s2060;@@ -2159,7 +2164,7 @@   const SWord8 s2075 = s2071 ? s2073 : s2074;   const SWord8 s2076 = 1 & s2075;   const SBool  s2077 = 0 != s2076;-  const SBool  s2078 = 0 == s2077;+  const SBool  s2078 = false == s2077;   const SWord8 s2079 = (s2063 >> 1) | (s2063 << 7);   const SWord8 s2080 = 128 | s2079;   const SWord8 s2081 = 127 & s2079;@@ -2178,7 +2183,7 @@   const SWord8 s2094 = s2090 ? s2092 : s2093;   const SWord8 s2095 = 1 & s2094;   const SBool  s2096 = 0 != s2095;-  const SBool  s2097 = 0 == s2096;+  const SBool  s2097 = false == s2096;   const SWord8 s2098 = (s2082 >> 1) | (s2082 << 7);   const SWord8 s2099 = 128 | s2098;   const SWord8 s2100 = 127 & s2098;@@ -2197,7 +2202,7 @@   const SWord8 s2113 = s2109 ? s2111 : s2112;   const SWord8 s2114 = 1 & s2113;   const SBool  s2115 = 0 != s2114;-  const SBool  s2116 = 0 == s2115;+  const SBool  s2116 = false == s2115;   const SWord8 s2117 = (s2101 >> 1) | (s2101 << 7);   const SWord8 s2118 = 128 | s2117;   const SWord8 s2119 = 127 & s2117;@@ -2302,7 +2307,7 @@   const SWord8 s2218 = s2217 ? s2111 : s2112;   const SWord8 s2219 = 1 & s2218;   const SBool  s2220 = 0 != s2219;-  const SBool  s2221 = 0 == s2220;+  const SBool  s2221 = false == s2220;   const SBool  s2222 = s2212 < s1;   const SBool  s2223 = s2212 < s2101;   const SBool  s2224 = s2222 | s2223;@@ -2411,7 +2416,7 @@   const SWord8 s2327 = s2326 ? s2092 : s2093;   const SWord8 s2328 = 1 & s2327;   const SBool  s2329 = 0 != s2328;-  const SBool  s2330 = 0 == s2329;+  const SBool  s2330 = false == s2329;   const SBool  s2331 = s2321 < s1;   const SBool  s2332 = s2321 < s2082;   const SBool  s2333 = s2331 | s2332;@@ -2433,7 +2438,7 @@   const SWord8 s2349 = s2345 ? s2347 : s2348;   const SWord8 s2350 = 1 & s2349;   const SBool  s2351 = 0 != s2350;-  const SBool  s2352 = 0 == s2351;+  const SBool  s2352 = false == s2351;   const SWord8 s2353 = (s2337 >> 1) | (s2337 << 7);   const SWord8 s2354 = 128 | s2353;   const SWord8 s2355 = 127 & s2353;@@ -2538,7 +2543,7 @@   const SWord8 s2454 = s2453 ? s2347 : s2348;   const SWord8 s2455 = 1 & s2454;   const SBool  s2456 = 0 != s2455;-  const SBool  s2457 = 0 == s2456;+  const SBool  s2457 = false == s2456;   const SBool  s2458 = s2448 < s1;   const SBool  s2459 = s2448 < s2337;   const SBool  s2460 = s2458 | s2459;@@ -2648,7 +2653,7 @@   const SWord8 s2564 = s2563 ? s2073 : s2074;   const SWord8 s2565 = 1 & s2564;   const SBool  s2566 = 0 != s2565;-  const SBool  s2567 = 0 == s2566;+  const SBool  s2567 = false == s2566;   const SBool  s2568 = s2558 < s1;   const SBool  s2569 = s2558 < s2063;   const SBool  s2570 = s2568 | s2569;@@ -2670,7 +2675,7 @@   const SWord8 s2586 = s2582 ? s2584 : s2585;   const SWord8 s2587 = 1 & s2586;   const SBool  s2588 = 0 != s2587;-  const SBool  s2589 = 0 == s2588;+  const SBool  s2589 = false == s2588;   const SWord8 s2590 = (s2574 >> 1) | (s2574 << 7);   const SWord8 s2591 = 128 | s2590;   const SWord8 s2592 = 127 & s2590;@@ -2689,7 +2694,7 @@   const SWord8 s2605 = s2601 ? s2603 : s2604;   const SWord8 s2606 = 1 & s2605;   const SBool  s2607 = 0 != s2606;-  const SBool  s2608 = 0 == s2607;+  const SBool  s2608 = false == s2607;   const SWord8 s2609 = (s2593 >> 1) | (s2593 << 7);   const SWord8 s2610 = 128 | s2609;   const SWord8 s2611 = 127 & s2609;@@ -2794,7 +2799,7 @@   const SWord8 s2710 = s2709 ? s2603 : s2604;   const SWord8 s2711 = 1 & s2710;   const SBool  s2712 = 0 != s2711;-  const SBool  s2713 = 0 == s2712;+  const SBool  s2713 = false == s2712;   const SBool  s2714 = s2704 < s1;   const SBool  s2715 = s2704 < s2593;   const SBool  s2716 = s2714 | s2715;@@ -2903,7 +2908,7 @@   const SWord8 s2819 = s2818 ? s2584 : s2585;   const SWord8 s2820 = 1 & s2819;   const SBool  s2821 = 0 != s2820;-  const SBool  s2822 = 0 == s2821;+  const SBool  s2822 = false == s2821;   const SBool  s2823 = s2813 < s1;   const SBool  s2824 = s2813 < s2574;   const SBool  s2825 = s2823 | s2824;@@ -2925,7 +2930,7 @@   const SWord8 s2841 = s2837 ? s2839 : s2840;   const SWord8 s2842 = 1 & s2841;   const SBool  s2843 = 0 != s2842;-  const SBool  s2844 = 0 == s2843;+  const SBool  s2844 = false == s2843;   const SWord8 s2845 = (s2829 >> 1) | (s2829 << 7);   const SWord8 s2846 = 128 | s2845;   const SWord8 s2847 = 127 & s2845;@@ -3030,7 +3035,7 @@   const SWord8 s2946 = s2945 ? s2839 : s2840;   const SWord8 s2947 = 1 & s2946;   const SBool  s2948 = 0 != s2947;-  const SBool  s2949 = 0 == s2948;+  const SBool  s2949 = false == s2948;   const SBool  s2950 = s2940 < s1;   const SBool  s2951 = s2940 < s2829;   const SBool  s2952 = s2950 | s2951;@@ -3141,7 +3146,7 @@   const SWord8 s3057 = s3056 ? s2054 : s2055;   const SWord8 s3058 = 1 & s3057;   const SBool  s3059 = 0 != s3058;-  const SBool  s3060 = 0 == s3059;+  const SBool  s3060 = false == s3059;   const SBool  s3061 = s3051 < s1;   const SBool  s3062 = s3051 < s2044;   const SBool  s3063 = s3061 | s3062;@@ -3163,7 +3168,7 @@   const SWord8 s3079 = s3075 ? s3077 : s3078;   const SWord8 s3080 = 1 & s3079;   const SBool  s3081 = 0 != s3080;-  const SBool  s3082 = 0 == s3081;+  const SBool  s3082 = false == s3081;   const SWord8 s3083 = (s3067 >> 1) | (s3067 << 7);   const SWord8 s3084 = 128 | s3083;   const SWord8 s3085 = 127 & s3083;@@ -3182,7 +3187,7 @@   const SWord8 s3098 = s3094 ? s3096 : s3097;   const SWord8 s3099 = 1 & s3098;   const SBool  s3100 = 0 != s3099;-  const SBool  s3101 = 0 == s3100;+  const SBool  s3101 = false == s3100;   const SWord8 s3102 = (s3086 >> 1) | (s3086 << 7);   const SWord8 s3103 = 128 | s3102;   const SWord8 s3104 = 127 & s3102;@@ -3201,7 +3206,7 @@   const SWord8 s3117 = s3113 ? s3115 : s3116;   const SWord8 s3118 = 1 & s3117;   const SBool  s3119 = 0 != s3118;-  const SBool  s3120 = 0 == s3119;+  const SBool  s3120 = false == s3119;   const SWord8 s3121 = (s3105 >> 1) | (s3105 << 7);   const SWord8 s3122 = 128 | s3121;   const SWord8 s3123 = 127 & s3121;@@ -3306,7 +3311,7 @@   const SWord8 s3222 = s3221 ? s3115 : s3116;   const SWord8 s3223 = 1 & s3222;   const SBool  s3224 = 0 != s3223;-  const SBool  s3225 = 0 == s3224;+  const SBool  s3225 = false == s3224;   const SBool  s3226 = s3216 < s1;   const SBool  s3227 = s3216 < s3105;   const SBool  s3228 = s3226 | s3227;@@ -3415,7 +3420,7 @@   const SWord8 s3331 = s3330 ? s3096 : s3097;   const SWord8 s3332 = 1 & s3331;   const SBool  s3333 = 0 != s3332;-  const SBool  s3334 = 0 == s3333;+  const SBool  s3334 = false == s3333;   const SBool  s3335 = s3325 < s1;   const SBool  s3336 = s3325 < s3086;   const SBool  s3337 = s3335 | s3336;@@ -3437,7 +3442,7 @@   const SWord8 s3353 = s3349 ? s3351 : s3352;   const SWord8 s3354 = 1 & s3353;   const SBool  s3355 = 0 != s3354;-  const SBool  s3356 = 0 == s3355;+  const SBool  s3356 = false == s3355;   const SWord8 s3357 = (s3341 >> 1) | (s3341 << 7);   const SWord8 s3358 = 128 | s3357;   const SWord8 s3359 = 127 & s3357;@@ -3542,7 +3547,7 @@   const SWord8 s3458 = s3457 ? s3351 : s3352;   const SWord8 s3459 = 1 & s3458;   const SBool  s3460 = 0 != s3459;-  const SBool  s3461 = 0 == s3460;+  const SBool  s3461 = false == s3460;   const SBool  s3462 = s3452 < s1;   const SBool  s3463 = s3452 < s3341;   const SBool  s3464 = s3462 | s3463;@@ -3652,7 +3657,7 @@   const SWord8 s3568 = s3567 ? s3077 : s3078;   const SWord8 s3569 = 1 & s3568;   const SBool  s3570 = 0 != s3569;-  const SBool  s3571 = 0 == s3570;+  const SBool  s3571 = false == s3570;   const SBool  s3572 = s3562 < s1;   const SBool  s3573 = s3562 < s3067;   const SBool  s3574 = s3572 | s3573;@@ -3674,7 +3679,7 @@   const SWord8 s3590 = s3586 ? s3588 : s3589;   const SWord8 s3591 = 1 & s3590;   const SBool  s3592 = 0 != s3591;-  const SBool  s3593 = 0 == s3592;+  const SBool  s3593 = false == s3592;   const SWord8 s3594 = (s3578 >> 1) | (s3578 << 7);   const SWord8 s3595 = 128 | s3594;   const SWord8 s3596 = 127 & s3594;@@ -3693,7 +3698,7 @@   const SWord8 s3609 = s3605 ? s3607 : s3608;   const SWord8 s3610 = 1 & s3609;   const SBool  s3611 = 0 != s3610;-  const SBool  s3612 = 0 == s3611;+  const SBool  s3612 = false == s3611;   const SWord8 s3613 = (s3597 >> 1) | (s3597 << 7);   const SWord8 s3614 = 128 | s3613;   const SWord8 s3615 = 127 & s3613;@@ -3798,7 +3803,7 @@   const SWord8 s3714 = s3713 ? s3607 : s3608;   const SWord8 s3715 = 1 & s3714;   const SBool  s3716 = 0 != s3715;-  const SBool  s3717 = 0 == s3716;+  const SBool  s3717 = false == s3716;   const SBool  s3718 = s3708 < s1;   const SBool  s3719 = s3708 < s3597;   const SBool  s3720 = s3718 | s3719;@@ -3907,7 +3912,7 @@   const SWord8 s3823 = s3822 ? s3588 : s3589;   const SWord8 s3824 = 1 & s3823;   const SBool  s3825 = 0 != s3824;-  const SBool  s3826 = 0 == s3825;+  const SBool  s3826 = false == s3825;   const SBool  s3827 = s3817 < s1;   const SBool  s3828 = s3817 < s3578;   const SBool  s3829 = s3827 | s3828;@@ -3929,7 +3934,7 @@   const SWord8 s3845 = s3841 ? s3843 : s3844;   const SWord8 s3846 = 1 & s3845;   const SBool  s3847 = 0 != s3846;-  const SBool  s3848 = 0 == s3847;+  const SBool  s3848 = false == s3847;   const SWord8 s3849 = (s3833 >> 1) | (s3833 << 7);   const SWord8 s3850 = 128 | s3849;   const SWord8 s3851 = 127 & s3849;@@ -4034,7 +4039,7 @@   const SWord8 s3950 = s3949 ? s3843 : s3844;   const SWord8 s3951 = 1 & s3950;   const SBool  s3952 = 0 != s3951;-  const SBool  s3953 = 0 == s3952;+  const SBool  s3953 = false == s3952;   const SBool  s3954 = s3944 < s1;   const SBool  s3955 = s3944 < s3833;   const SBool  s3956 = s3954 | s3955;@@ -6409,7 +6414,7 @@   const SWord8 s6325 = s17 ? s6041 : s6324;   const SWord8 s6326 = s12 ? s5758 : s6325;   const SWord8 s6327 = s6 ? s5191 : s6326;-  +   *hi = s4056;   *lo = s6327; }
SBVUnitTest/GoldFiles/popCount1.gold view
@@ -32,9 +32,12 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> +/* The boolean type */+typedef bool SBool;+ /* Unsigned bit-vectors */-typedef uint8_t  SBool  ; typedef uint8_t  SWord8 ; typedef uint16_t SWord16; typedef uint32_t SWord32;@@ -57,13 +60,14 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include <stdio.h> #include "popCount.h"  int main(void) {   const SWord8 __result = popCount(0x0123456789abcdefULL);-  +   printf("popCount(0x0123456789abcdefULL) = %"PRIu8"\n", __result);    return 0;@@ -74,6 +78,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include "popCount.h"  SWord8 popCount(const SWord64 x)@@ -123,7 +128,7 @@   const SWord64 s38 = 0x00000000000000ffULL & s37;   const SWord8  s39 = table0[s38];   const SWord8  s40 = s36 + s39;-  +   return s40; } == END: "popCount.c" ==================
SBVUnitTest/GoldFiles/popCount2.gold view
@@ -32,9 +32,12 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> +/* The boolean type */+typedef bool SBool;+ /* Unsigned bit-vectors */-typedef uint8_t  SBool  ; typedef uint8_t  SWord8 ; typedef uint16_t SWord16; typedef uint32_t SWord32;@@ -57,13 +60,14 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include <stdio.h> #include "popCount.h"  int main(void) {   const SWord8 __result = popCount(0x0123456789abcdefULL);-  +   printf("popCount(0x0123456789abcdefULL) = %"PRIu8"\n", __result);    return 0;@@ -74,6 +78,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include "popCount.h"  SWord8 popCount(const SWord64 x)@@ -123,7 +128,7 @@   const SWord64 s38 = 0x00000000000000ffULL & s37;   const SWord8  s39 = s38 >= 256 ? 0 : table0[s38];   const SWord8  s40 = s36 + s39;-  +   return s40; } == END: "popCount.c" ==================
SBVUnitTest/GoldFiles/selChecked.gold view
@@ -32,9 +32,12 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> +/* The boolean type */+typedef bool SBool;+ /* Unsigned bit-vectors */-typedef uint8_t  SBool  ; typedef uint8_t  SWord8 ; typedef uint16_t SWord16; typedef uint32_t SWord32;@@ -57,13 +60,14 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include <stdio.h> #include "selChecked.h"  int main(void) {   const SWord8 __result = selChecked(65);-  +   printf("selChecked(65) = %"PRIu8"\n", __result);    return 0;@@ -74,6 +78,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include "selChecked.h"  SWord8 selChecked(const SWord8 x)@@ -84,7 +89,7 @@        1, s3   };   const SWord8 s5 = s0 >= 2 ? 3 : table0[s0];-  +   return s5; } == END: "selChecked.c" ==================
SBVUnitTest/GoldFiles/selUnchecked.gold view
@@ -32,9 +32,12 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> +/* The boolean type */+typedef bool SBool;+ /* Unsigned bit-vectors */-typedef uint8_t  SBool  ; typedef uint8_t  SWord8 ; typedef uint16_t SWord16; typedef uint32_t SWord32;@@ -57,13 +60,14 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include <stdio.h> #include "selUnChecked.h"  int main(void) {   const SWord8 __result = selUnChecked(65);-  +   printf("selUnChecked(65) = %"PRIu8"\n", __result);    return 0;@@ -74,6 +78,7 @@  #include <inttypes.h> #include <stdint.h>+#include <stdbool.h> #include "selUnChecked.h"  SWord8 selUnChecked(const SWord8 x)@@ -84,7 +89,7 @@        1, s3   };   const SWord8 s5 = table0[s0];-  +   return s5; } == END: "selUnChecked.c" ==================
SBVUnitTest/SBVUnitTest.hs view
@@ -13,15 +13,12 @@ module Main(main) where  import Control.Monad        (unless, when)-import System.Directory     (doesDirectoryExist, findExecutable)-import System.Environment   (getArgs, getEnv)+import System.Directory     (doesDirectoryExist)+import System.Environment   (getArgs) import System.Exit          (exitWith, ExitCode(..)) import System.FilePath      ((</>))-import System.Process       (readProcessWithExitCode) import Test.HUnit           (Test(..), Counts(..), runTestTT) -import Data.List            (isPrefixOf)-import Data.SBV             (yices, SMTSolver(..), SMTConfig(..)) import Data.Version         (showVersion) import SBVTest              (SBVTestSuite(..), generateGoldCheck) import Paths_sbv            (getDataDir, version)@@ -135,35 +132,6 @@                                    putStrLn "*** Cannot run test cases, exiting."                                    exitWith $ ExitFailure 1 -checkYices :: IO ()-checkYices = do ex <- getEnv "SBV_YICES" `catch` (\_ -> return (executable (solver yices)))-                mbP <- findExecutable ex-                case mbP of-                  Nothing -> do putStrLn $ "*** Cannot find default SMT solver executable for " ++ nm-                                putStrLn $ "*** Please make sure the executable " ++ show ex-                                putStrLn   "*** is installed and is in your path."-                                putStrLn   "*** Cannot run test cases, exiting."-                                exitWith $ ExitFailure 1-                  Just p  -> do putStrLn $ "*** Using solver : " ++ nm ++ " (" ++ show p ++ ")"-                                checkYicesVersion p- where nm = name (solver yices)--checkYicesVersion :: FilePath -> IO ()-checkYicesVersion p =-        do (ec, yOut, _yErr) <- readProcessWithExitCode p ["-V"] ""-           case ec of-             ExitFailure _ -> do putStrLn "*** Cannot determine Yices version. Please install Yices version 2.X first."-                                 exitWith $ ExitFailure 1-             ExitSuccess   -> do let isYices1 = "1." `isPrefixOf` yOut -- crude test; might fail..-                                 when isYices1 $ putStrLn "*** Yices version 1.X is detected. Version 2.X is strongly recommended!"-                                 opts <- getEnv "SBV_YICES_OPTIONS" `catch` (\_ -> return (unwords (options (solver yices))))-                                 when (isYices1 && opts /= "-tc -smt -e") $ do-                                           putStrLn "*** Either install Yices 2.X, or set the environment variable:"-                                           putStrLn "***     SBV_YICES_OPTIONS=\"-tc -smt -e\""-                                           putStrLn "*** To use Yices 1.X with SBV."-                                           putStrLn "*** However, upgrading to Yices 2.X is highly recommended!"-                                           exitWith $ ExitFailure 1- allTargets :: [String] allTargets = map fst testCollection @@ -176,7 +144,6 @@         do mapM_ checkTgt targets            putStrLn $ "*** Starting SBV unit tests..\n*** Gold files at: " ++ show gd            checkGoldDir gd-           checkYices            cts <- runTestTT $ TestList $ map mkTst [c | (tc, c) <- testCollection, select tc]            decide shouldCreate cts   where mkTst (SBVTestSuite f) = f $ generateGoldCheck gd shouldCreate
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where  buildTime :: String-buildTime = "Wed Dec 28 00:11:15 PST 2011"+buildTime = "Sun Feb 12 23:26:02 PST 2012"
SBVUnitTest/TestSuite/Basics/Arithmetic.hs view
@@ -21,25 +21,27 @@ -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test $-        genBinTest "+"                (+)-     ++ genBinTest "-"                (-)-     ++ genBinTest "*"                (*)-     ++ genUnTest  "negate"           negate-     ++ genUnTest  "abs"              abs-     ++ genUnTest  "signum"           signum-     ++ genBinTest ".&."              (.&.)-     ++ genBinTest ".|."              (.|.)-     ++ genBinTest "xor"              xor-     ++ genUnTest  "complement"       complement-     ++ genIntTest "shift"            shift-     ++ genIntTest "rotate"           rotate-     ++ genIntTest "setBit"           setBit-     ++ genIntTest "clearBit"         clearBit-     ++ genIntTest "complementBit"    complementBit-     ++ genIntTest "shiftL"           shiftL-     ++ genIntTest "shiftR"           shiftR-     ++ genIntTest "rotateL"          rotateL-     ++ genIntTest "rotateR"          rotateR+        genBinTest  "+"                (+)+     ++ genBinTest  "-"                (-)+     ++ genBinTest  "*"                (*)+     ++ genUnTest   "negate"           negate+     ++ genUnTest   "abs"              abs+     ++ genUnTest   "signum"           signum+     ++ genBinTest  ".&."              (.&.)+     ++ genBinTest  ".|."              (.|.)+     ++ genBinTest  "xor"              xor+     ++ genUnTest   "complement"       complement+     ++ genIntTest  "shift"            shift+     ++ genIntTest  "rotate"           rotate+     ++ genIntTestS "setBit"           setBit+     ++ genIntTestS "clearBit"         clearBit+     ++ genIntTestS "complementBit"    complementBit+     ++ genIntTest  "shift"            shift+     ++ genIntTestS "shiftL"           shiftL+     ++ genIntTestS "shiftR"           shiftR+     ++ genIntTest  "rotate"           rotate+     ++ genIntTestS "rotateL"          rotateL+     ++ genIntTestS "rotateR"          rotateR      ++ genBlasts      ++ genCasts @@ -85,6 +87,20 @@   where pair (t, x, y, a) b       = (t, x, y, show a, show b, show (fromIntegral a `asTypeOf` b) == show b)         mkTest (t, x, y, a, b, s) = "arithmetic-" ++ nm ++ "." ++ t ++ "_" ++ x ++ "_" ++ y ++ "_" ++ a ++ "_" ++ b ~: s `showsAs` "True"         is = [-10 .. 10]++genIntTestS :: String -> (forall a. Bits a => a -> Int -> a) -> [Test]+genIntTestS nm op = map mkTest $+        zipWith pair [("u8",  show x, show y, x `op` y) | x <- w8s,  y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw8s,  y <- [0 .. (bitSize x - 1)]]+     ++ zipWith pair [("u16", show x, show y, x `op` y) | x <- w16s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw16s, y <- [0 .. (bitSize x - 1)]]+     ++ zipWith pair [("u32", show x, show y, x `op` y) | x <- w32s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw32s, y <- [0 .. (bitSize x - 1)]]+     ++ zipWith pair [("u64", show x, show y, x `op` y) | x <- w64s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw64s, y <- [0 .. (bitSize x - 1)]]+     ++ zipWith pair [("s8",  show x, show y, x `op` y) | x <- i8s,  y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si8s,  y <- [0 .. (bitSize x - 1)]]+     ++ zipWith pair [("s16", show x, show y, x `op` y) | x <- i16s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si16s, y <- [0 .. (bitSize x - 1)]]+     ++ zipWith pair [("s32", show x, show y, x `op` y) | x <- i32s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si32s, y <- [0 .. (bitSize x - 1)]]+     ++ zipWith pair [("s64", show x, show y, x `op` y) | x <- i64s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si64s, y <- [0 .. (bitSize x - 1)]]+     ++ zipWith pair [("iUB", show x, show y, x `op` y) | x <- iUBs, y <- [0 .. 10]]              [x `op` y | x <- siUBs, y <- [0 .. 10             ]]+  where pair (t, x, y, a) b       = (t, x, y, show a, show b, show (fromIntegral a `asTypeOf` b) == show b)+        mkTest (t, x, y, a, b, s) = "arithmetic-" ++ nm ++ "." ++ t ++ "_" ++ x ++ "_" ++ y ++ "_" ++ a ++ "_" ++ b ~: s `showsAs` "True"  genBlasts :: [Test] genBlasts = map mkTest $
SBVUnitTest/TestSuite/CodeGeneration/PopulationCount.hs view
@@ -28,4 +28,4 @@                   cgSetDriverValues [0x0123456789ABCDEF]                   cgPerformRTCs b                   x <- cgInput "x"-                  cgReturn $ popCount x+                  cgReturn $ popCountFast x
sbv.cabal view
@@ -1,5 +1,5 @@ Name:          sbv-Version:       0.9.24+Version:       1.0 Category:      Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis:      Symbolic bit vectors: Bit-precise verification and automatic C-code generation. Description:   Express properties about bit-precise Haskell programs and automatically prove@@ -46,7 +46,8 @@                .                  * quick-checked                .-                 * used in concrete test case generation (the 'genTest' function)+                 * used in concrete test case generation (the 'genTest' function), rendered as values in various+                   languages, including Haskell and C.                .                Predicates can have both existential and universal variables. Use of                alternating quantifiers provides considerable expressive power.@@ -126,10 +127,7 @@                   , Data.SBV.Examples.Uninterpreted.AUF                   , Data.SBV.Examples.Uninterpreted.Function   Other-modules   : Data.SBV.BitVectors.Data-                  , Data.SBV.BitVectors.GenTest                   , Data.SBV.BitVectors.Model-                  , Data.SBV.BitVectors.Optimize-                  , Data.SBV.BitVectors.Polynomial                   , Data.SBV.BitVectors.PrettyNum                   , Data.SBV.BitVectors.SignCast                   , Data.SBV.BitVectors.Splittable@@ -144,6 +142,10 @@                   , Data.SBV.Provers.SExpr                   , Data.SBV.Provers.Yices                   , Data.SBV.Provers.Z3+                  , Data.SBV.Tools.ExpectedValue+                  , Data.SBV.Tools.GenTest+                  , Data.SBV.Tools.Optimize+                  , Data.SBV.Tools.Polynomial                   , Data.SBV.Utils.Boolean                   , Data.SBV.Utils.TDiff                   , Data.SBV.Utils.Lib