packages feed

sbv 2.0 → 2.1

raw patch · 116 files changed

+1035/−758 lines, 116 filesdep +sybsetup-changed

Dependencies added: syb

Files

Data/SBV.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- (The sbv library is hosted at <http://github.com/LeventErkok/sbv>. -- Comments, bug reports, and patches are always welcome.)@@ -35,19 +34,21 @@ -- -- In particular, the sbv library introduces the types: -----   * 'SBool': Symbolic Booleans (bits)+--   * 'SBool': Symbolic Booleans (bits). -----   * 'SWord8', 'SWord16', 'SWord32', 'SWord64': Symbolic Words (unsigned)+--   * 'SWord8', 'SWord16', 'SWord32', 'SWord64': Symbolic Words (unsigned). -----   * 'SInt8',  'SInt16',  'SInt32',  'SInt64': Symbolic Ints (signed)+--   * 'SInt8',  'SInt16',  'SInt32',  'SInt64': Symbolic Ints (signed). -----   * 'SArray', 'SFunArray': Flat arrays of symbolic values+--   * 'SArray', 'SFunArray': Flat arrays of symbolic values. -----   * Symbolic polynomials over GF(2^n), polynomial arithmetic, and CRCs+--   * Symbolic polynomials over GF(2^n), polynomial arithmetic, and CRCs. -- --   * Uninterpreted constants and functions over symbolic values, with user---     defined SMT-Lib axioms+--     defined SMT-Lib axioms. --+--   * Uninterpreted sorts, and proofs over such sorts, potentially with axioms.+-- -- The user can construct ordinary Haskell programs using these types, which behave -- very similar to their concrete counterparts. In particular these types belong to the -- standard classes 'Num', 'Bits', custom versions of 'Eq' ('EqSymbolic') @@ -103,7 +104,7 @@   , sBool, sWord8, sWord16, sWord32, sWord64, sInt8, sInt16, sInt32, sInt64, sInteger   -- ** Creating a list of symbolic variables   -- $createSyms-  , sBools, sWord8s, sWord16s, sWord32s, sWord64s, sInt8s, sInt16s, sInt32s, sInt64s, sIntegers, sReal, sReals+  , sBools, sWord8s, sWord16s, sWord32s, sWord64s, sInt8s, sInt16s, sInt32s, sInt64s, sIntegers, sReal, sReals, toSReal   -- *** Abstract SBV type   , SBV   -- *** Arrays of symbolic values@@ -139,13 +140,11 @@   , bAnd, bOr, bAny, bAll   -- ** Pretty-printing and reading numbers in Hex & Binary   , PrettyNum(..), readBin-  -- * Uninterpreted constants and functions-  , Uninterpreted(..)-  -- ** Accessing the handle-  , SBVUF, sbvUFName-  -- ** Adding axioms-  , addAxiom +  -- * Uninterpreted sorts, constants, and functions+  -- $uninterpreted+  , Uninterpreted(..), addAxiom+   -- * Properties, proofs, and satisfiability   -- $proveIntro @@ -194,7 +193,7 @@   , compileToSMTLib, generateSMTBenchmarks    -- * Test case generation-  , genTest, getTestValues, TestVectors, TestStyle(..), renderTest, CW(..), Kind(..), cwToBool+  , genTest, getTestValues, TestVectors, TestStyle(..), renderTest, CW(..), HasKind(..), Kind(..), cwToBool    -- * Code generation from symbolic programs   -- $cCodeGeneration@@ -213,8 +212,12 @@   , cgReturn, cgReturnArr    -- ** Code generation with uninterpreted functions-  , cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIntegerSize+  , cgAddPrototype, cgAddDecl, cgAddLDFlags +  -- ** Code generation with 'SInteger' and 'SReal' types+  -- $unboundedCGen+  , cgIntegerSize, cgSRealType, CgSRealType(..)+   -- ** Compilation to C   , compileToC, compileToCLib @@ -251,13 +254,13 @@ {- $progIntro The SBV library is really two things: -  * A framework for writing bit-precise programs in Haskell+  * A framework for writing symbolic programs in Haskell, i.e., programs operating on+    symbolic values along with the usual concrete counterparts. -  * A framework for proving properties of such programs using SMT solvers+  * A framework for proving properties of such programs using SMT solvers. -In this first section we will look at the constructs that will let us construct such-programs in Haskell. The goal is to have a "seamless" experience, i.e., program in-the usual Haskell style without distractions of symbolic coding. While Haskell helps+The programming goal of SBV is to provide a /seamless/ experience, i.e., let people program+in the usual Haskell style without distractions of symbolic coding. While Haskell helps in some aspects (the 'Num' and 'Bits' classes simplify coding), it makes life harder in others. For instance, @if-then-else@ only takes 'Bool' as a test in Haskell, and comparisons ('>' etc.) only return 'Bool's. Clearly we would like these values to be@@ -343,6 +346,17 @@ these characteristics make them suitable for use in hard real-time systems, as well as in traditional computing. -} +{- $unboundedCGen+The types 'SInteger' and 'SReal' are unbounded quantities that have no direct counterparts in the C language. Therefore,+it is not possible to generate standard C code for SBV programs using these types, unless custom libraries are available. To+overcome this, SBV allows the user to explicitly set what the corresponding types should be for these two cases, using+the functions below. Note that while these mappings will produce valid C code, the resulting code will be subject to+overflow/underflows for 'SInteger', and rounding for 'SReal', so there is an implicit loss of precision.++If the user does /not/ specify these mappings, then SBV will+refuse to compile programs that involve these types.+-}+ {- $moduleExportIntro The SBV library exports the following modules wholesale, as user programs will have to import these modules to make any sensible use of the SBV functionality.@@ -479,6 +493,31 @@ '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.+-}++{- $uninterpreted+Users can introduce new uninterpreted sorts simply by defining a data-type in Haskell and registering it as such. The+following example demonstrates:++  @+     data B = B deriving (Eq, Ord, Data, Typeable)+     instance SymWord  B+     instance HasKind  B+  @++(Note that you'll also need to use the language pragma @DeriveDataTypeable@, and import @Data.Generics@ for the above to work.) ++Once GHC implements derivable user classes (<http://hackage.haskell.org/trac/ghc/ticket/5462>), we will be able to simplify this to:++  @+     data B = B deriving (Eq, Ord, Data, Typeable, SymWord, HasKind)+  @++This is all it takes to introduce 'B' as an uninterpreted sort in SBV, which makes the type @SBV B@ automagically become available as the type+of symbolic values that ranges over 'B' values.++Uninterpreted functions over both uninterpreted and regular sorts can be declared using the facilities introduced by+the 'Uninterpreted' class. -}  {-# ANN module "HLint: ignore Use import/export shortcut" #-}
Data/SBV/BitVectors/AlgReals.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Algrebraic reals in Haskell. -----------------------------------------------------------------------------@@ -14,7 +13,7 @@ {-# LANGUAGE TypeSynonymInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -module Data.SBV.BitVectors.AlgReals (AlgReal, mkPolyReal, algRealToSMTLib2, algRealToHaskell, mergeAlgReals) where+module Data.SBV.BitVectors.AlgReals (AlgReal(..), mkPolyReal, algRealToSMTLib2, algRealToHaskell, mergeAlgReals) where  import Data.List     (sortBy, isPrefixOf, partition) import Data.Ratio    ((%), numerator, denominator)
Data/SBV/BitVectors/Data.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Internal data-structures for the sbv library -----------------------------------------------------------------------------@@ -17,12 +16,13 @@ {-# LANGUAGE ScopedTypeVariables        #-} {-# LANGUAGE FlexibleInstances          #-} {-# LANGUAGE PatternGuards              #-}+{-# LANGUAGE DefaultSignatures          #-}  module Data.SBV.BitVectors.Data  ( SBool, SWord8, SWord16, SWord32, SWord64  , SInt8, SInt16, SInt32, SInt64, SInteger, SReal  , SymWord(..)- , CW(..), cwSameType, cwIsBit, cwToBool+ , CW(..), CWVal(..), cwSameType, cwIsBit, cwToBool  , mkConstCW ,liftCW2, mapCW, mapCW2  , SW(..), trueSW, falseSW, trueCW, falseCW  , SBV(..), NodeId(..), mkSymSBV@@ -37,16 +37,17 @@  , SMTLibPgm(..), SMTLibVersion(..)  ) where -import Control.DeepSeq                 (NFData(..))-import Control.Monad                   (when)-import Control.Monad.Reader            (MonadReader, ReaderT, ask, runReaderT)-import Control.Monad.Trans             (MonadIO, liftIO)-import Data.Char                       (isAlpha, isAlphaNum)-import Data.Int                        (Int8, Int16, Int32, Int64)-import Data.Word                       (Word8, Word16, Word32, Word64)-import Data.IORef                      (IORef, newIORef, modifyIORef, readIORef, writeIORef)-import Data.List                       (intercalate, sortBy)-import Data.Maybe                      (isJust, fromJust)+import Control.DeepSeq      (NFData(..))+import Control.Monad        (when)+import Control.Monad.Reader (MonadReader, ReaderT, ask, runReaderT)+import Control.Monad.Trans  (MonadIO, liftIO)+import Data.Char            (isAlpha, isAlphaNum)+import Data.Generics        (Data(..), dataTypeName, dataTypeOf, tyconUQname)+import Data.Int             (Int8, Int16, Int32, Int64)+import Data.Word            (Word8, Word16, Word32, Word64)+import Data.IORef           (IORef, newIORef, modifyIORef, readIORef, writeIORef)+import Data.List            (intercalate, sortBy)+import Data.Maybe           (isJust, fromJust)  import qualified Data.IntMap   as IMap (IntMap, empty, size, toAscList, lookup, insert, insertWith) import qualified Data.Map      as Map  (Map, empty, toList, size, insert, lookup)@@ -59,11 +60,17 @@ import Data.SBV.BitVectors.AlgReals import Data.SBV.Utils.Lib +-- | A constant value+data CWVal = CWAlgReal       AlgReal    -- ^ algebraic real+           | CWInteger       Integer    -- ^ bit-vector/unbounded integer+           | CWUninterpreted String     -- ^ value of an uninterpreted kind+           deriving (Eq, Ord)+ -- | 'CW' represents a concrete word of a fixed size: -- Endianness is mostly irrelevant (see the 'FromBits' class). -- For signed words, the most significant digit is considered to be the sign.-data CW = CW { cwKind   :: !Kind                     -- ^ Kind of the word-             , cwVal    :: !(Either AlgReal Integer) -- ^ The underlying value, represented as either an algebraic real (for SReal), or a Haskell 'Integer' (everything else)+data CW = CW { cwKind   :: !Kind+             , cwVal    :: !CWVal              }         deriving (Eq, Ord) @@ -77,16 +84,16 @@               KBounded False 1 -> True               _                -> False --- | Convert a CW to a Haskell boolean+-- | Convert a CW to a Haskell boolean (NB. Assumes input is well-kinded) cwToBool :: CW -> Bool-cwToBool x = cwVal x /= Right 0+cwToBool x = cwVal x /= CWInteger 0  -- | Normalize a CW. Essentially performs modular arithmetic to make sure the -- value can fit in the given bit-size. Note that this is rather tricky for -- negative values, due to asymmetry. (i.e., an 8-bit negative number represents -- values in the range -128 to 127; thus we have to be careful on the negative side.) normCW :: CW -> CW-normCW c@(CW (KBounded signed sz) (Right v)) = c { cwVal = Right norm }+normCW c@(CW (KBounded signed sz) (CWInteger v)) = c { cwVal = CWInteger norm }  where norm | sz == 0 = 0             | signed  = let rg = 2 ^ (sz - 1)                         in case divMod v rg of@@ -99,6 +106,7 @@ data Kind = KBounded Bool Int           | KUnbounded           | KReal+          | KUninterpreted String           deriving (Eq, Ord)  instance Show Kind where@@ -107,6 +115,7 @@   show (KBounded True n)  = "SInt"  ++ show n   show KUnbounded         = "SInteger"   show KReal              = "SReal"+  show (KUninterpreted s) = s  -- | A symbolic node id newtype NodeId = NodeId Int deriving (Eq, Ord)@@ -132,11 +141,11 @@  -- | Constant False as a CW. We represent it using the integer value 0. falseCW :: CW-falseCW = CW (KBounded False 1) (Right 0)+falseCW = CW (KBounded False 1) (CWInteger 0)  -- | Constant True as a CW. We represent it using the integer value 1. trueCW :: CW-trueCW  = CW (KBounded False 1) (Right 1)+trueCW  = CW (KBounded False 1) (CWInteger 1)  -- | A simple type for SBV computations, used mainly for uninterpreted constants. -- We keep track of the signedness/size of the arguments. A non-function will@@ -173,38 +182,43 @@              deriving (Eq, Ord)  -- | A class for capturing values that have a sign and a size (finite or infinite)--- minimal complete definition: kindOf+-- minimal complete definition: kindOf. This class can be automatically derived+-- for data-types that have a 'Data' instance; this is useful for creating uninterpreted+-- sorts. class HasKind a where-  kindOf     :: a -> Kind-  hasSign    :: a -> Bool-  intSizeOf  :: a -> Int-  isBounded  :: a -> Bool-  isReal     :: a -> Bool-  isInteger  :: a -> Bool-  showType   :: a -> String+  kindOf          :: a -> Kind+  hasSign         :: a -> Bool+  intSizeOf       :: a -> Int+  isBounded       :: a -> Bool+  isReal          :: a -> Bool+  isInteger       :: a -> Bool+  isUninterpreted :: a -> Bool+  showType        :: a -> String   -- defaults   hasSign x = case kindOf x of-                KBounded b _ -> b-                KUnbounded   -> True-                KReal        -> True+                  KBounded b _     -> b+                  KUnbounded       -> True+                  KReal            -> True+                  KUninterpreted{} -> False   intSizeOf x = case kindOf x of-                  KBounded _ s -> s-                  KUnbounded   -> error "SBV.HasKind.intSizeOf((S)Integer)"-                  KReal        -> error "SBV.HasKind.intSizeOf((S)Real)"-  isBounded x = case kindOf x of-                  KBounded{} -> True-                  KUnbounded -> False-                  KReal      -> False-  isReal x    = case kindOf x of-                  KBounded{} -> False-                  KUnbounded -> False-                  KReal      -> True-  isInteger x = case kindOf x of-                  KBounded{} -> False-                  KUnbounded -> True-                  KReal      -> False+                  KBounded _ s     -> s+                  KUnbounded       -> error "SBV.HasKind.intSizeOf((S)Integer)"+                  KReal            -> error "SBV.HasKind.intSizeOf((S)Real)"+                  KUninterpreted s -> error $ "SBV.HasKind.intSizeOf: Uninterpreted sort: " ++ s+  isBounded       x | KBounded{}       <- kindOf x = True+                    | True                         = False+  isReal          x | KReal{}          <- kindOf x = True+                    | True                         = False+  isInteger      x  | KUnbounded{}     <- kindOf x = True+                    | True                         = False+  isUninterpreted x | KUninterpreted{} <- kindOf x = True+                    | True                         = False   showType = show . kindOf +  -- default signature for uninterpreted kinds+  default kindOf :: Data a => a -> Kind+  kindOf = KUninterpreted . tyconUQname . dataTypeName . dataTypeOf+ instance HasKind Bool    where kindOf _ = KBounded False 1 instance HasKind Int8    where kindOf _ = KBounded True  8 instance HasKind Word8   where kindOf _ = KBounded False 8@@ -218,26 +232,33 @@ instance HasKind AlgReal where kindOf _ = KReal  -- | Lift a unary function thruough a CW-liftCW :: (AlgReal -> b) -> (Integer -> b) -> CW -> b-liftCW f g = either f g . cwVal+liftCW :: (AlgReal -> b) -> (Integer -> b) -> (String -> b) -> CW -> b+liftCW f _ _ (CW _ (CWAlgReal v))       = f v+liftCW _ g _ (CW _ (CWInteger v))       = g v+liftCW _ _ h (CW _ (CWUninterpreted v)) = h v  -- | Lift a binary function through a CW-liftCW2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> CW -> CW -> b-liftCW2 f g x y = case (cwVal x, cwVal y) of-                    (Left a, Left b)   -> f a b-                    (Right a, Right b) -> g a b-                    _                  -> error $ "SBV.liftCW2: impossible, incompatible args received: " ++ show (x, y)+liftCW2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> (String -> String -> b) -> CW -> CW -> b+liftCW2 f g h x y = case (cwVal x, cwVal y) of+                      (CWAlgReal a,       CWAlgReal b)       -> f a b+                      (CWInteger a,       CWInteger b)       -> g a b+                      (CWUninterpreted a, CWUninterpreted b) -> h a b+                      _                                      -> error $ "SBV.liftCW2: impossible, incompatible args received: " ++ show (x, y)  -- | Map a unary function through a CW-mapCW :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> CW -> CW-mapCW f g x  = normCW $ CW (cwKind x) (either (Left . f) (Right . g) (cwVal x))+mapCW :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> (String -> String) -> CW -> CW+mapCW f g h x  = normCW $ CW (cwKind x) $ case cwVal x of+                                            CWAlgReal a       -> CWAlgReal       (f a)+                                            CWInteger a       -> CWInteger       (g a)+                                            CWUninterpreted a -> CWUninterpreted (h a)  -- | Map a binary function through a CW-mapCW2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> CW -> CW -> CW-mapCW2 f g x y = case (cwSameType x y, cwVal x, cwVal y) of-                   (True, Left a,  Left b)  -> normCW $ CW (cwKind x) (Left  (f a b))-                   (True, Right a, Right b) -> normCW $ CW (cwKind x) (Right (g a b))-                   _                        -> error $ "SBV.mapCW2: impossible, incompatible args received: " ++ show (x, y)+mapCW2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (String -> String -> String) -> CW -> CW -> CW+mapCW2 f g h x y = case (cwSameType x y, cwVal x, cwVal y) of+                     (True, CWAlgReal a,       CWAlgReal b)       -> normCW $ CW (cwKind x) (CWAlgReal       (f a b))+                     (True, CWInteger a,       CWInteger b)       -> normCW $ CW (cwKind x) (CWInteger       (g a b))+                     (True, CWUninterpreted a, CWUninterpreted b) -> normCW $ CW (cwKind x) (CWUninterpreted (h a b))+                     _                        -> error $ "SBV.mapCW2: impossible, incompatible args received: " ++ show (x, y)  instance HasKind CW where   kindOf = cwKind@@ -247,7 +268,7 @@  instance Show CW where   show w | cwIsBit w = show (cwToBool w)-  show w             = liftCW show show w ++ " :: " ++ showType w+  show w             = liftCW show show id w ++ " :: " ++ showType w  instance Show SW where   show (SW _ (NodeId n))@@ -265,7 +286,7 @@         where tinfo = "table" ++ show ti ++ "(" ++ show at ++ " -> " ++ show rt ++ ", " ++ show l ++ ")"   show (ArrEq i j)   = "array_" ++ show i ++ " == array_" ++ show j   show (ArrRead i)   = "select array_" ++ show i-  show (Uninterpreted i) = "uninterpreted_" ++ i+  show (Uninterpreted i) = "[uninterpreted] " ++ i   show op     | Just s <- op `lookup` syms = s     | True                       = error "impossible happened; can't find op!"@@ -309,7 +330,8 @@  deriving Show  -- | Result of running a symbolic computation-data Result = Result Bool                          -- contains unbounded integers+data Result = Result (Bool, Bool)                  -- contains unbounded integers/reals+                     [String]                      -- uninterpreted sorts                      [(String, CW)]                -- quick-check counter-example information (if any)                      [(String, [String])]          -- uninterpeted code segments                      [(Quantifier, NamedSymVar)]   -- inputs (possibly existential)@@ -324,18 +346,19 @@  -- | Extract the constraints from a result getConstraints :: Result -> [SW]-getConstraints (Result _ _ _ _ _ _ _ _ _ _ cstrs _) = cstrs+getConstraints (Result _ _ _ _ _ _ _ _ _ _ _ cstrs _) = cstrs  -- | Extract the traced-values from a result (quick-check) getTraceInfo :: Result -> [(String, CW)]-getTraceInfo (Result _ tvals _ _ _ _ _ _ _ _ _ _) = tvals+getTraceInfo (Result _ _ tvals _ _ _ _ _ _ _ _ _ _) = tvals  instance Show Result where-  show (Result _ _ _ _ cs _ _ [] [] _ [] [r])+  show (Result _ _ _ _ _ cs _ _ [] [] _ [] [r])     | Just c <- r `lookup` cs     = show c-  show (Result _ _ cgs is cs ts as uis axs xs cstrs os)  = intercalate "\n" $-                   ["INPUTS"]+  show (Result _ sorts _ cgs is cs ts as uis axs xs cstrs os)  = intercalate "\n" $+                   (if null sorts then [] else "SORTS" : map ("  " ++) sorts)+                ++ ["INPUTS"]                 ++ map shn is                 ++ ["CONSTANTS"]                 ++ map shc cs@@ -370,7 +393,7 @@             where ni = "array_" ++ show i                   alias | ni == nm = ""                         | True     = ", aliasing " ++ show nm-          shui (nm, t) = "  uninterpreted_" ++ nm ++ " :: " ++ show t+          shui (nm, t) = "  [uninterpreted] " ++ nm ++ " :: " ++ show t           shax (nm, ss) = "  -- user defined axiom: " ++ nm ++ "\n  " ++ intercalate "\n  " ss  -- | The context of a symbolic array as created@@ -440,7 +463,7 @@                     , rStdGen       :: IORef StdGen                     , rCInfo        :: IORef [(String, CW)]                     , rctr          :: IORef Int-                    , rBounded      :: IORef Bool+                    , rUnBounded    :: IORef (Bool, Bool)     -- SInteger, SReal                     , rinps         :: IORef [(Quantifier, NamedSymVar)]                     , rConstraints  :: IORef [SW]                     , routs         :: IORef [SW]@@ -454,6 +477,7 @@                     , raxioms       :: IORef [(String, [String])]                     , rSWCache      :: IORef (Cache SW)                     , rAICache      :: IORef (Cache Int)+                    , rSorts        :: IORef [String]                     }  -- | Are we running in proof mode?@@ -556,10 +580,15 @@   case c `Map.lookup` constMap of     Just sw -> return sw     Nothing -> do ctr <- incCtr st-                  let sw = SW (kindOf c) (NodeId ctr)-                  when (not (isBounded sw)) $ writeIORef (rBounded st) False+                  let k = kindOf c+                      sw = SW k (NodeId ctr)+                  () <- case kindOf c of+                         KUnbounded -> modifyIORef (rUnBounded st) (\(_, y) -> (True, y))+                         KReal      -> modifyIORef (rUnBounded st) (\(x, _) -> (x, True))+                         _          -> return ()                   modifyIORef (rconstMap st) (Map.insert c sw)                   return sw+{-# INLINE newConst #-}  -- | Create a new table; hash-cons as necessary getTableIndex :: State -> Kind -> Kind -> [SW] -> IO Int@@ -573,8 +602,8 @@  -- | Create a constant word mkConstCW :: Integral a => Kind -> a -> CW-mkConstCW KReal a = normCW $ CW KReal (Left  (fromInteger (toInteger a)))-mkConstCW k     a = normCW $ CW k     (Right (toInteger a))+mkConstCW KReal a = normCW $ CW KReal (CWAlgReal (fromInteger (toInteger a)))+mkConstCW k     a = normCW $ CW k     (CWInteger (toInteger a))  -- | Create a new expression; hash-cons as necessary newExpr :: State -> Kind -> SBVExpr -> IO SW@@ -585,10 +614,14 @@      Just sw -> return sw      Nothing -> do ctr <- incCtr st                    let sw = SW k (NodeId ctr)-                   when (not (isBounded sw)) $ writeIORef (rBounded st) False+                   () <- case k of+                          KUnbounded -> modifyIORef (rUnBounded st) (\(_, y) -> (True, y))+                          KReal      -> modifyIORef (rUnBounded st) (\(x, _) -> (x, True))+                          _          -> return ()                    modifyIORef (spgm st)     (flip (S.|>) (sw, e))                    modifyIORef (rexprMap st) (Map.insert e sw)                    return sw+{-# INLINE newExpr #-}  -- | Convert a symbolic value to a symbolic-word sbvToSW :: State -> SBV a -> IO SW@@ -625,7 +658,10 @@           _          -> do ctr <- liftIO $ incCtr st                            let nm = maybe ('s':show ctr) id mbNm                                sw = SW k (NodeId ctr)-                           when (not (isBounded sw)) $ liftIO $ writeIORef (rBounded st) False+                           () <- case k of+                                   KUnbounded -> liftIO $ modifyIORef (rUnBounded st) (\(_, y) -> (True, y))+                                   KReal      -> liftIO $ modifyIORef (rUnBounded st) (\(x, _) -> (x, True))+                                   _          -> return ()                            liftIO $ modifyIORef (rinps st) ((q, (sw, nm)):)                            return $ SBV k $ Right $ cache (const (return sw)) @@ -680,8 +716,10 @@ instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f, Outputtable g, Outputtable h) => Outputtable (a, b, c, d, e, f, g, h) where   output = mlift8 (,,,,,,,) output output output output output output output output --- | Add a user specified axiom to the generated SMT-Lib file. Note that the input is a--- mere string; we perform no checking on the input that it's well-formed or is sensical.+-- | Add a user specified axiom to the generated SMT-Lib file. The first argument is a mere+-- string, use for commenting purposes. The second argument is intended to hold the multiple-lines+-- of the axiom text as expressed in SMT-Lib notation. Note that we perform no checks on the axiom+-- itself, to see whether it's actually well-formed or is sensical by any means. -- A separate formalization of SMT-Lib would be very useful here. addAxiom :: String -> [String] -> Symbolic () addAxiom nm ax = do@@ -696,30 +734,31 @@ -- | Run a symbolic computation, and return a extra value paired up with the 'Result' runSymbolic' :: SBVRunMode -> Symbolic a -> IO (a, Result) runSymbolic' currentRunMode (Symbolic c) = do-   ctr     <- newIORef (-2) -- start from -2; False and True will always occupy the first two elements-   cInfo   <- newIORef []-   pgm     <- newIORef S.empty-   emap    <- newIORef Map.empty-   cmap    <- newIORef Map.empty-   inps    <- newIORef []-   outs    <- newIORef []-   tables  <- newIORef Map.empty-   arrays  <- newIORef IMap.empty-   uis     <- newIORef Map.empty-   cgs     <- newIORef Map.empty-   axioms  <- newIORef []-   swCache <- newIORef IMap.empty-   aiCache <- newIORef IMap.empty-   bounded <- newIORef True-   cstrs   <- newIORef []-   rGen    <- case currentRunMode of-                Concrete g -> newIORef g-                _          -> newStdGen >>= newIORef+   ctr       <- newIORef (-2) -- start from -2; False and True will always occupy the first two elements+   cInfo     <- newIORef []+   pgm       <- newIORef S.empty+   emap      <- newIORef Map.empty+   cmap      <- newIORef Map.empty+   inps      <- newIORef []+   outs      <- newIORef []+   tables    <- newIORef Map.empty+   arrays    <- newIORef IMap.empty+   uis       <- newIORef Map.empty+   cgs       <- newIORef Map.empty+   axioms    <- newIORef []+   swCache   <- newIORef IMap.empty+   aiCache   <- newIORef IMap.empty+   unbounded <- newIORef (False, False)+   cstrs     <- newIORef []+   sorts     <- newIORef []+   rGen      <- case currentRunMode of+                  Concrete g -> newIORef g+                  _          -> newStdGen >>= newIORef    let st = State { runMode      = currentRunMode                   , rStdGen      = rGen                   , rCInfo       = cInfo                   , rctr         = ctr-                  , rBounded     = bounded+                  , rUnBounded   = unbounded                   , rinps        = inps                   , routs        = outs                   , rtblMap      = tables@@ -733,6 +772,7 @@                   , rSWCache     = swCache                   , rAICache     = aiCache                   , rConstraints = cstrs+                  , rSorts       = sorts                   }    _ <- newConst st (mkConstCW (KBounded False 1) (0::Integer)) -- s(-2) == falseSW    _ <- newConst st (mkConstCW (KBounded False 1) (1::Integer)) -- s(-1) == trueSW@@ -747,11 +787,12 @@    arrs  <- IMap.toAscList `fmap` readIORef arrays    unint <- Map.toList `fmap` readIORef uis    axs   <- reverse `fmap` readIORef axioms-   allBounded <- readIORef bounded+   boundInfo <- readIORef unbounded    cgMap <- Map.toList `fmap` readIORef cgs    traceVals <- reverse `fmap` readIORef cInfo-   extraCstrs   <- reverse `fmap` readIORef cstrs-   return $ (r, Result (not allBounded) traceVals cgMap inpsO cnsts tbls arrs unint axs rpgm extraCstrs outsO)+   extraCstrs <- reverse `fmap` readIORef cstrs+   usorts <- reverse `fmap` readIORef sorts+   return $ (r, Result boundInfo usorts traceVals cgMap inpsO cnsts tbls arrs unint axs rpgm extraCstrs outsO)  ------------------------------------------------------------------------------- -- * Symbolic Words@@ -760,8 +801,6 @@ -- to be fed to a symbolic program. Note that these methods are typically not needed -- in casual uses with 'prove', 'sat', 'allSat' etc, as default instances automatically -- provide the necessary bits.------ Minimal complete definiton: forall, forall_, exists, exists_, literal, fromCW class (HasKind a, Ord a) => SymWord a where   -- | Create a user named input (universal)   forall :: String -> Symbolic (SBV a)@@ -800,8 +839,18 @@   -- | max/minbounds, if available. Note that we don't want   -- to impose "Bounded" on our class as Integer is not Bounded but it is a SymWord   mbMaxBound, mbMinBound :: Maybe a+  -- | One stop allocator+  mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV a) -  -- minimal complete definiton: forall, forall_, exists, exists_, free, free_, literal, fromCW+  -- minimal complete definiton, Nothing.+  -- Giving no instances is ok when defining an uninterpreted sort, but otherwise you really+  -- want to define: mbMaxBound, mbMinBound, literal, fromCW, mkSymWord+  forall   = mkSymWord (Just ALL) . Just+  forall_  = mkSymWord (Just ALL)   Nothing+  exists   = mkSymWord (Just EX)  . Just+  exists_  = mkSymWord (Just EX)    Nothing+  free     = mkSymWord Nothing    . Just+  free_    = mkSymWord Nothing      Nothing   mkForallVars n = mapM (const forall_) [1 .. n]   mkExistVars n  = mapM (const exists_) [1 .. n]   mkFreeVars n   = mapM (const free_)   [1 .. n]@@ -815,7 +864,34 @@   isConcretely s p     | Just i <- unliteral s = p i     | True                  = False+  -- Followings, you really want to define them unless the instance is for an uninterpreted sort+  mbMaxBound = Nothing+  mbMinBound = Nothing+  literal x = error $ "Cannot create symbolic literals for kind: " ++ show (kindOf x)+  fromCW cw = error $ "Cannot convert CW " ++ show cw ++ " to kind " ++ show (kindOf (undefined :: a)) +  default mkSymWord :: Data a => Maybe Quantifier -> Maybe String -> Symbolic (SBV a)+  mkSymWord mbQ mbNm = do+        let sortName = tyconUQname . dataTypeName . dataTypeOf $ (undefined :: a)+        st <- ask+        let -- TBD: Is this list comprehensive?+            reserved = ["Int", "Real", "List", "Array", "Bool"]+        when (sortName `elem` reserved) $ error $ "SBV.registerSort: " ++ show sortName ++ " is a reserved sort; please use a different name"+        curSorts <- liftIO $ readIORef (rSorts st)+        when (sortName `notElem` curSorts) $ liftIO $ modifyIORef (rSorts st) (sortName :)+        let k = KUninterpreted sortName+            q = case (mbQ, runMode st) of+                  (Just x,  _)           -> x+                  (Nothing, Proof True)  -> EX+                  (Nothing, Proof False) -> ALL+                  (Nothing, Concrete{})  -> error $ "SBV.registerSort: Uninterpreted sort " ++ sortName ++ " can not be used in concrete simulation mode."+                  (Nothing, CodeGen)     -> error $ "SBV.registerSort: Uninterpreted sort " ++ sortName ++ " can not be used in code-generation mode."+        ctr <- liftIO $ incCtr st+        let sw = SW k (NodeId ctr)+            nm = maybe ('s':show ctr) id mbNm+        liftIO $ modifyIORef (rinps st) ((q, (sw, nm)):)+        return $ SBV k $ Right $ cache (const (return sw))+ instance (Random a, SymWord a) => Random (SBV a) where   randomR (l, h) g = case (unliteral l, unliteral h) of                        (Just lb, Just hb) -> let (v, g') = randomR (lb, hb) g in (literal (v :: a), g')@@ -1027,8 +1103,11 @@   rnf (CW x y) = x `seq` y `seq` ()  instance NFData Result where-  rnf (Result isInf qcInfo cgs inps consts tbls arrs uis axs pgm cstr outs)-        = rnf isInf `seq` rnf qcInfo `seq` rnf cgs `seq` rnf inps `seq` rnf consts `seq` rnf tbls `seq` rnf arrs `seq` rnf uis `seq` rnf axs `seq` rnf pgm `seq` rnf cstr `seq` rnf outs+  rnf (Result isInf sorts qcInfo cgs inps consts tbls arrs uis axs pgm cstr outs)+        = rnf isInf `seq` rnf sorts `seq` rnf qcInfo `seq` rnf cgs+                    `seq` rnf inps  `seq` rnf consts `seq` rnf tbls+                    `seq` rnf arrs  `seq` rnf uis    `seq` rnf axs+                    `seq` rnf pgm   `seq` rnf cstr   `seq` rnf outs  instance NFData Kind instance NFData ArrayContext
Data/SBV/BitVectors/Model.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Instance declarations for our symbolic world -----------------------------------------------------------------------------@@ -24,10 +23,10 @@ module Data.SBV.BitVectors.Model (     Mergeable(..), EqSymbolic(..), OrdSymbolic(..), BVDivisible(..), Uninterpreted(..), SNum   , sbvTestBit, sbvPopCount, setBitTo, allEqual, allDifferent, oneIf, blastBE, blastLE-  , lsb, msb, SBVUF, sbvUFName, genVar, genVar_, forall, forall_, exists, exists_+  , lsb, msb, genVar, genVar_, forall, forall_, exists, exists_   , constrain, pConstrain, sBool, sBools, sWord8, sWord8s, sWord16, sWord16s, sWord32   , sWord32s, sWord64, sWord64s, sInt8, sInt8s, sInt16, sInt16s, sInt32, sInt32s, sInt64-  , sInt64s, sInteger, sIntegers, sReal, sReals+  , sInt64s, sInteger, sIntegers, sReal, sReals, toSReal, slet   )   where @@ -49,21 +48,27 @@ import Data.SBV.BitVectors.Data import Data.SBV.Utils.Boolean +noUnint  :: String -> a+noUnint x = error $ "Unexpected operation called on uninterpreted value: " ++ show x++noUnint2 :: String -> String -> a+noUnint2 x y = error $ "Unexpected binary operation called on uninterpreted values: " ++ show (x, y)+ liftSym1 :: (State -> Kind -> SW -> IO SW) -> (AlgReal -> AlgReal) -> (Integer -> Integer) -> SBV b -> SBV b-liftSym1 _   opCR opCI   (SBV k (Left a)) = SBV k $ Left  $ mapCW opCR opCI a+liftSym1 _   opCR opCI   (SBV k (Left a)) = SBV k $ Left  $ mapCW opCR opCI noUnint a liftSym1 opS _    _    a@(SBV k _)        = SBV k $ Right $ cache c    where c st = do swa <- sbvToSW st a                    opS st k swa  liftSym2 :: (State -> Kind -> SW -> SW -> IO SW) -> (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> SBV b -> SBV b -> SBV b-liftSym2 _   opCR opCI   (SBV k (Left a)) (SBV _ (Left b)) = SBV k $ Left  $ mapCW2 opCR opCI a b+liftSym2 _   opCR opCI   (SBV k (Left a)) (SBV _ (Left b)) = SBV k $ Left  $ mapCW2 opCR opCI noUnint2 a b liftSym2 opS _    _    a@(SBV k _)        b                = SBV k $ Right $ cache c   where c st = do sw1 <- sbvToSW st a                   sw2 <- sbvToSW st b                   opS st k sw1 sw2  liftSym2B :: (State -> Kind -> SW -> SW -> IO SW) -> (AlgReal -> AlgReal -> Bool) -> (Integer -> Integer -> Bool) -> SBV b -> SBV b -> SBool-liftSym2B _   opCR opCI (SBV _ (Left a)) (SBV _ (Left b)) = literal (liftCW2 opCR opCI a b)+liftSym2B _   opCR opCI (SBV _ (Left a)) (SBV _ (Left b)) = literal (liftCW2 opCR opCI noUnint2 a b) liftSym2B opS _    _    a                b                = SBV (KBounded False 1) $ Right $ cache c   where c st = do sw1 <- sbvToSW st a                   sw2 <- sbvToSW st b@@ -111,139 +116,89 @@  -- | Convert a constant to an integral value genFromCW :: Integral a => CW -> a-genFromCW (CW _ (Right x)) = fromInteger x-genFromCW c                = error $ "genFromCW: Unsupported AlgReal value: " ++ show c+genFromCW (CW _ (CWInteger x)) = fromInteger x+genFromCW c                    = error $ "genFromCW: Unsupported non-integral value: " ++ show c +-- | Generically make a symbolic var+genMkSymVar :: (Random a, SymWord a) => Kind -> Maybe Quantifier -> Maybe String -> Symbolic (SBV a)+genMkSymVar k mbq Nothing  = genVar_ mbq k+genMkSymVar k mbq (Just s) = genVar  mbq k s+ instance SymWord Bool where-  forall     = genVar  (Just ALL) (KBounded False 1)-  forall_    = genVar_ (Just ALL) (KBounded False 1)-  exists     = genVar  (Just EX)  (KBounded False 1)-  exists_    = genVar_ (Just EX)  (KBounded False 1)-  free       = genVar  Nothing    (KBounded False 1)-  free_      = genVar_ Nothing    (KBounded False 1)-  literal x  = genLiteral (KBounded False 1) (if x then (1::Integer) else 0)+  mkSymWord  = genMkSymVar (KBounded False 1)+  literal x  = genLiteral  (KBounded False 1) (if x then (1::Integer) else 0)   fromCW     = cwToBool   mbMaxBound = Just maxBound   mbMinBound = Just minBound  instance SymWord Word8 where-  forall     = genVar   (Just ALL) (KBounded False 8)-  forall_    = genVar_  (Just ALL) (KBounded False 8)-  exists     = genVar   (Just EX)  (KBounded False 8)-  exists_    = genVar_  (Just EX)  (KBounded False 8)-  free       = genVar   Nothing    (KBounded False 8)-  free_      = genVar_  Nothing    (KBounded False 8)-  literal    = genLiteral (KBounded False 8)+  mkSymWord  = genMkSymVar (KBounded False 8)+  literal    = genLiteral  (KBounded False 8)   fromCW     = genFromCW   mbMaxBound = Just maxBound   mbMinBound = Just minBound  instance SymWord Int8 where-  forall     = genVar   (Just ALL) (KBounded True 8)-  forall_    = genVar_  (Just ALL) (KBounded True 8)-  exists     = genVar   (Just EX)  (KBounded True 8)-  exists_    = genVar_  (Just EX)  (KBounded True 8)-  free       = genVar   Nothing    (KBounded True 8)-  free_      = genVar_  Nothing    (KBounded True 8)-  literal    = genLiteral (KBounded True 8)+  mkSymWord  = genMkSymVar (KBounded True 8)+  literal    = genLiteral  (KBounded True 8)   fromCW     = genFromCW   mbMaxBound = Just maxBound   mbMinBound = Just minBound  instance SymWord Word16 where-  forall     = genVar   (Just ALL) (KBounded False 16)-  forall_    = genVar_  (Just ALL) (KBounded False 16)-  exists     = genVar   (Just EX)  (KBounded False 16)-  exists_    = genVar_  (Just EX)  (KBounded False 16)-  free       = genVar   Nothing    (KBounded False 16)-  free_      = genVar_  Nothing    (KBounded False 16)-  literal    = genLiteral (KBounded False 16)+  mkSymWord  = genMkSymVar (KBounded False 16)+  literal    = genLiteral  (KBounded False 16)   fromCW     = genFromCW   mbMaxBound = Just maxBound   mbMinBound = Just minBound  instance SymWord Int16 where-  forall     = genVar   (Just ALL) (KBounded True 16)-  forall_    = genVar_  (Just ALL) (KBounded True 16)-  exists     = genVar   (Just EX)  (KBounded True 16)-  exists_    = genVar_  (Just EX)  (KBounded True 16)-  free       = genVar   Nothing    (KBounded True 16)-  free_      = genVar_  Nothing    (KBounded True 16)-  literal    = genLiteral (KBounded True 16)+  mkSymWord  = genMkSymVar (KBounded True 16)+  literal    = genLiteral  (KBounded True 16)   fromCW     = genFromCW   mbMaxBound = Just maxBound   mbMinBound = Just minBound  instance SymWord Word32 where-  forall     = genVar   (Just ALL) (KBounded False 32)-  forall_    = genVar_  (Just ALL) (KBounded False 32)-  exists     = genVar   (Just EX)  (KBounded False 32)-  exists_    = genVar_  (Just EX)  (KBounded False 32)-  free       = genVar   Nothing    (KBounded False 32)-  free_      = genVar_  Nothing    (KBounded False 32)-  literal    = genLiteral (KBounded False 32)+  mkSymWord  = genMkSymVar (KBounded False 32)+  literal    = genLiteral  (KBounded False 32)   fromCW     = genFromCW   mbMaxBound = Just maxBound   mbMinBound = Just minBound  instance SymWord Int32 where-  forall     = genVar   (Just ALL) (KBounded True 32)-  forall_    = genVar_  (Just ALL) (KBounded True 32)-  exists     = genVar   (Just EX)  (KBounded True 32)-  exists_    = genVar_  (Just EX)  (KBounded True 32)-  free       = genVar   Nothing    (KBounded True 32)-  free_      = genVar_  Nothing    (KBounded True 32)-  literal    = genLiteral (KBounded True 32)+  mkSymWord  = genMkSymVar (KBounded True 32)+  literal    = genLiteral  (KBounded True 32)   fromCW     = genFromCW   mbMaxBound = Just maxBound   mbMinBound = Just minBound  instance SymWord Word64 where-  forall     = genVar   (Just ALL) (KBounded False 64)-  forall_    = genVar_  (Just ALL) (KBounded False 64)-  exists     = genVar   (Just EX)  (KBounded False 64)-  exists_    = genVar_  (Just EX)  (KBounded False 64)-  free       = genVar   Nothing    (KBounded False 64)-  free_      = genVar_  Nothing    (KBounded False 64)-  literal    = genLiteral (KBounded False 64)+  mkSymWord  = genMkSymVar (KBounded False 64)+  literal    = genLiteral  (KBounded False 64)   fromCW     = genFromCW   mbMaxBound = Just maxBound   mbMinBound = Just minBound  instance SymWord Int64 where-  forall     = genVar   (Just ALL) (KBounded True 64)-  forall_    = genVar_  (Just ALL) (KBounded True 64)-  exists     = genVar   (Just EX)  (KBounded True 64)-  exists_    = genVar_  (Just EX)  (KBounded True 64)-  free       = genVar   Nothing    (KBounded True 64)-  free_      = genVar_  Nothing    (KBounded True 64)-  literal    = genLiteral (KBounded True 64)+  mkSymWord  = genMkSymVar (KBounded True 64)+  literal    = genLiteral  (KBounded True 64)   fromCW     = genFromCW   mbMaxBound = Just maxBound   mbMinBound = Just minBound  instance SymWord Integer where-  forall     = mkSymSBV (Just ALL) KUnbounded . Just-  forall_    = mkSymSBV (Just ALL) KUnbounded Nothing-  exists     = mkSymSBV (Just EX)  KUnbounded . Just-  exists_    = mkSymSBV (Just EX)  KUnbounded Nothing-  free       = mkSymSBV Nothing    KUnbounded . Just-  free_      = mkSymSBV Nothing    KUnbounded Nothing+  mkSymWord  = genMkSymVar KUnbounded   literal    = SBV KUnbounded . Left . mkConstCW KUnbounded   fromCW     = genFromCW   mbMaxBound = Nothing   mbMinBound = Nothing  instance SymWord AlgReal where-  forall     = mkSymSBV (Just ALL) KReal . Just-  forall_    = mkSymSBV (Just ALL) KReal Nothing-  exists     = mkSymSBV (Just EX)  KReal . Just-  exists_    = mkSymSBV (Just EX)  KReal Nothing-  free       = mkSymSBV Nothing    KReal . Just-  free_      = mkSymSBV Nothing    KReal Nothing-  literal    = SBV KReal . Left . CW KReal . Left-  fromCW (CW _ (Left a)) = a-  fromCW c               = error $ "SymWord.AlgReal: Unexpected non-real value: " ++ show c+  mkSymWord  = genMkSymVar KReal+  literal    = SBV KReal . Left . CW KReal . CWAlgReal+  fromCW (CW _ (CWAlgReal a)) = a+  fromCW c                    = error $ "SymWord.AlgReal: Unexpected non-real value: " ++ show c   mbMaxBound = Nothing   mbMinBound = Nothing @@ -340,6 +295,14 @@ sReals :: [String] -> Symbolic [SReal] sReals = symbolics +-- | Promote an SInteger to an SReal+toSReal :: SInteger -> SReal+toSReal x+  | Just i <- unliteral x = literal $ fromInteger i+  | True                  = SBV KReal (Right (cache y))+  where y st = do xsw <- sbvToSW st x+                  newExpr st KReal (SBVApp (Extract 0 0) [xsw]) -- special encoding!+ -- | Symbolic Equality. Note that we can't use Haskell's 'Eq' class since Haskell insists on returning Bool -- Comparing symbolic values will necessarily return a symbolic value. --@@ -823,8 +786,8 @@  instance BVDivisible CW where   bvQuotRem a b-    | Right x <- cwVal a, Right y <- cwVal b-    = let (r1, r2) = bvQuotRem x y in (a { cwVal = Right r1 }, b { cwVal = Right r2 })+    | CWInteger x <- cwVal a, CWInteger y <- cwVal b+    = let (r1, r2) = bvQuotRem x y in (a { cwVal = CWInteger r1 }, b { cwVal = CWInteger r2 })   bvQuotRem a b = error $ "SBV.liftQRem: impossible, unexpected args received: " ++ show (a, b)  instance BVDivisible SWord64 where@@ -1140,20 +1103,6 @@ instance SymWord b => Mergeable (SFunArray a b) where   symbolicMerge = mergeArrays --- | An uninterpreted function handle. This is the handle to be used for--- adding axioms about uninterpreted constants/functions. Note that--- we will leave this abstract for safety purposes-newtype SBVUF = SBVUF String---- | Get the name associated with the uninterpreted-value; useful when--- constructing axioms about this UI.-sbvUFName :: SBVUF -> String-sbvUFName (SBVUF s) = s---- The name we use for translating the UF constants to SMT-Lib..-mkUFName :: String -> SBVUF-mkUFName nm = SBVUF $ "uninterpreted_" ++ nm- -- | Uninterpreted constants and functions. An uninterpreted constant is -- a value that is indexed by its name. The only property the prover assumes -- about these values are that they are equivalent to themselves; i.e., (for@@ -1162,16 +1111,13 @@ -- operations that are /irrelevant/ for the purposes of the proof; i.e., when -- the proofs can be performed without any knowledge about the function itself. ----- Minimal complete definition: 'uninterpretWithHandle'. However, most instances in+-- Minimal complete definition: 'sbvUninterpret'. However, most instances in -- practice are already provided by SBV, so end-users should not need to define their -- own instances. class Uninterpreted a where   -- | Uninterpret a value, receiving an object that can be used instead. Use this version   -- when you do not need to add an axiom about this value.   uninterpret :: String -> a-  -- | Uninterpret a value, but also get a handle to the resulting object. This handle-  -- can be used to add axioms for this object. (See 'addAxiom'.)-  uninterpretWithHandle :: String -> (SBVUF, a)   -- | Uninterpret a value, only for the purposes of code-generation. For execution   -- and verification the value is used as is. For code-generation, the alternate   -- definition is used. This is useful when we want to take advantage of native@@ -1179,18 +1125,17 @@   cgUninterpret :: String -> [String] -> a -> a   -- | Most generalized form of uninterpretation, this function should not be needed   -- by end-user-code, but is rather useful for the library development.-  sbvUninterpret :: Maybe ([String], a) -> String -> (SBVUF, a)+  sbvUninterpret :: Maybe ([String], a) -> String -> a    -- minimal complete definition: 'sbvUninterpret'-  uninterpret             = snd . uninterpretWithHandle-  uninterpretWithHandle   = sbvUninterpret Nothing-  cgUninterpret nm code v = snd $ sbvUninterpret (Just (code, v)) nm+  uninterpret             = sbvUninterpret Nothing+  cgUninterpret nm code v = sbvUninterpret (Just (code, v)) nm  -- Plain constants instance HasKind a => Uninterpreted (SBV a) where   sbvUninterpret mbCgData nm-     | Just (_, v) <- mbCgData = (mkUFName nm, v)-     | True                    = (mkUFName nm, SBV ka $ Right $ cache result)+     | Just (_, v) <- mbCgData = v+     | True                    = SBV ka $ Right $ cache result     where ka = kindOf (undefined :: a)           result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st v                     | True = do newUninterpreted st nm (SBVType [ka]) (fst `fmap` mbCgData)@@ -1204,7 +1149,7 @@  -- Functions of one argument instance (SymWord b, HasKind a) => Uninterpreted (SBV b -> SBV a) where-  sbvUninterpret mbCgData nm = (mkUFName nm, f)+  sbvUninterpret mbCgData nm = f     where f arg0            | Just (_, v) <- mbCgData, isConcrete arg0            = v arg0@@ -1220,7 +1165,7 @@  -- Functions of two arguments instance (SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV c -> SBV b -> SBV a) where-  sbvUninterpret mbCgData nm = (mkUFName nm, f)+  sbvUninterpret mbCgData nm = f     where f arg0 arg1            | Just (_, v) <- mbCgData, isConcrete arg0, isConcrete arg1            = v arg0 arg1@@ -1238,7 +1183,7 @@  -- Functions of three arguments instance (SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) where-  sbvUninterpret mbCgData nm = (mkUFName nm, f)+  sbvUninterpret mbCgData nm = f     where f arg0 arg1 arg2            | Just (_, v) <- mbCgData, isConcrete arg0, isConcrete arg1, isConcrete arg2            = v arg0 arg1 arg2@@ -1258,7 +1203,7 @@  -- Functions of four arguments instance (SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where-  sbvUninterpret mbCgData nm = (mkUFName nm, f)+  sbvUninterpret mbCgData nm = f     where f arg0 arg1 arg2 arg3            | Just (_, v) <- mbCgData, isConcrete arg0, isConcrete arg1, isConcrete arg2, isConcrete arg3            = v arg0 arg1 arg2 arg3@@ -1280,7 +1225,7 @@  -- Functions of five arguments instance (SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where-  sbvUninterpret mbCgData nm = (mkUFName nm, f)+  sbvUninterpret mbCgData nm = f     where f arg0 arg1 arg2 arg3 arg4            | Just (_, v) <- mbCgData, isConcrete arg0, isConcrete arg1, isConcrete arg2, isConcrete arg3, isConcrete arg4            = v arg0 arg1 arg2 arg3 arg4@@ -1304,7 +1249,7 @@  -- Functions of six arguments instance (SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where-  sbvUninterpret mbCgData nm = (mkUFName nm, f)+  sbvUninterpret mbCgData nm = f     where f arg0 arg1 arg2 arg3 arg4 arg5            | Just (_, v) <- mbCgData, isConcrete arg0, isConcrete arg1, isConcrete arg2, isConcrete arg3, isConcrete arg4, isConcrete arg5            = v arg0 arg1 arg2 arg3 arg4 arg5@@ -1331,7 +1276,7 @@ -- Functions of seven arguments instance (SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a)             => Uninterpreted (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where-  sbvUninterpret mbCgData nm = (mkUFName nm, f)+  sbvUninterpret mbCgData nm = f     where f arg0 arg1 arg2 arg3 arg4 arg5 arg6            | Just (_, v) <- mbCgData, isConcrete arg0, isConcrete arg1, isConcrete arg2, isConcrete arg3, isConcrete arg4, isConcrete arg5, isConcrete arg6            = v arg0 arg1 arg2 arg3 arg4 arg5 arg6@@ -1359,36 +1304,36 @@  -- Uncurried functions of two arguments instance (SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV c, SBV b) -> SBV a) where-  sbvUninterpret mbCgData nm = let (h, f) = sbvUninterpret (uc2 `fmap` mbCgData) nm in (h, \(arg0, arg1) -> f arg0 arg1)+  sbvUninterpret mbCgData nm = let f = sbvUninterpret (uc2 `fmap` mbCgData) nm in \(arg0, arg1) -> f arg0 arg1     where uc2 (cs, fn) = (cs, \a b -> fn (a, b))  -- Uncurried functions of three arguments instance (SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) where-  sbvUninterpret mbCgData nm = let (h, f) = sbvUninterpret (uc3 `fmap` mbCgData) nm in (h, \(arg0, arg1, arg2) -> f arg0 arg1 arg2)+  sbvUninterpret mbCgData nm = let f = sbvUninterpret (uc3 `fmap` mbCgData) nm in \(arg0, arg1, arg2) -> f arg0 arg1 arg2     where uc3 (cs, fn) = (cs, \a b c -> fn (a, b, c))  -- Uncurried functions of four arguments instance (SymWord e, SymWord d, SymWord c, SymWord b, HasKind a)             => Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) where-  sbvUninterpret mbCgData nm = let (h, f) = sbvUninterpret (uc4 `fmap` mbCgData) nm in (h, \(arg0, arg1, arg2, arg3) -> f arg0 arg1 arg2 arg3)+  sbvUninterpret mbCgData nm = let f = sbvUninterpret (uc4 `fmap` mbCgData) nm in \(arg0, arg1, arg2, arg3) -> f arg0 arg1 arg2 arg3     where uc4 (cs, fn) = (cs, \a b c d -> fn (a, b, c, d))  -- Uncurried functions of five arguments instance (SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a)             => Uninterpreted ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where-  sbvUninterpret mbCgData nm = let (h, f) = sbvUninterpret (uc5 `fmap` mbCgData) nm in (h, \(arg0, arg1, arg2, arg3, arg4) -> f arg0 arg1 arg2 arg3 arg4)+  sbvUninterpret mbCgData nm = let f = sbvUninterpret (uc5 `fmap` mbCgData) nm in \(arg0, arg1, arg2, arg3, arg4) -> f arg0 arg1 arg2 arg3 arg4     where uc5 (cs, fn) = (cs, \a b c d e -> fn (a, b, c, d, e))  -- Uncurried functions of six arguments instance (SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a)             => Uninterpreted ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where-  sbvUninterpret mbCgData nm = let (h, f) = sbvUninterpret (uc6 `fmap` mbCgData) nm in (h, \(arg0, arg1, arg2, arg3, arg4, arg5) -> f arg0 arg1 arg2 arg3 arg4 arg5)+  sbvUninterpret mbCgData nm = let f = sbvUninterpret (uc6 `fmap` mbCgData) nm in \(arg0, arg1, arg2, arg3, arg4, arg5) -> f arg0 arg1 arg2 arg3 arg4 arg5     where uc6 (cs, fn) = (cs, \a b c d e f -> fn (a, b, c, d, e, f))  -- Uncurried functions of seven arguments instance (SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a)             => Uninterpreted ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where-  sbvUninterpret mbCgData nm = let (h, f) = sbvUninterpret (uc7 `fmap` mbCgData) nm in (h, \(arg0, arg1, arg2, arg3, arg4, arg5, arg6) -> f arg0 arg1 arg2 arg3 arg4 arg5 arg6)+  sbvUninterpret mbCgData nm = let f = sbvUninterpret (uc7 `fmap` mbCgData) nm in \(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.@@ -1408,7 +1353,7 @@  instance Testable (Symbolic SBool) where   property m = QC.whenFail (putStrLn msg) $ QC.monadicIO test-    where runOnce g = do (r, Result _ tvals _ _ cs _ _ _ _ _ cstrs _) <- runSymbolic' (Concrete g) m+    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 ++ ")"@@ -1425,3 +1370,16 @@             where maxLen = maximum (0:[length s | (s, _) <- qcInfo])                   shN s = s ++ replicate (maxLen - length s) ' '                   info (n, cw) = shN n ++ " = " ++ show cw++-- | Explicit sharing combinator. The SBV library has internal caching/hash-consing mechanisms+-- built in, based on Andy Gill's type-safe obervable sharing technique (see: <http://ittc.ku.edu/~andygill/paper.php?label=DSLExtract09>).+-- However, there might be times where being explicit on the sharing can help, especially in experimental code. The 'slet' combinator+-- ensures that its first argument is computed once and passed on to its continuation, explicitly indicating the intent of sharing. Most+-- use cases of the SBV library should simply use Haskell's @let@ construct for this purpose.+slet :: (HasKind a, HasKind b) => SBV a -> (SBV a -> SBV b) -> SBV b+slet x f = SBV k $ Right $ cache r+    where k    = kindOf (undefined `asTypeOf` f x)+          r st = do xsw <- sbvToSW st x+                    let xsbv = SBV (kindOf x) (Right (cache (const (return xsw))))+                        res  = f xsbv+                    sbvToSW st res
Data/SBV/BitVectors/PrettyNum.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Number representations in hex/bin -----------------------------------------------------------------------------@@ -62,30 +61,34 @@  instance PrettyNum CW where   hexS cw | cwIsBit cw         = hexS (cwToBool cw)-          | isReal cw          = let Left w = cwVal cw in show w-          | not (isBounded cw) = let Right w = cwVal cw in shexI True True w-          | True               = let Right w = cwVal cw in shex  True True (hasSign cw, intSizeOf cw) w+          | isReal cw          = let CWAlgReal w = cwVal cw in show w+          | not (isBounded cw) = let CWInteger w = cwVal cw in shexI True True w+          | isUninterpreted cw = show cw+          | True               = let CWInteger w = cwVal cw in shex  True True (hasSign cw, intSizeOf cw) w    binS cw | cwIsBit cw         = binS (cwToBool cw)-          | isReal cw          = let Left w = cwVal cw in show w-          | not (isBounded cw) = let Right w = cwVal cw in sbinI True True w-          | True               = let Right w = cwVal cw in sbin  True True (hasSign cw, intSizeOf cw) w+          | isReal cw          = let CWAlgReal w = cwVal cw in show w+          | not (isBounded cw) = let CWInteger w = cwVal cw in sbinI True True w+          | isUninterpreted cw = show cw+          | True               = let CWInteger w = cwVal cw in sbin  True True (hasSign cw, intSizeOf cw) w    hex cw | cwIsBit cw         = hexS (cwToBool cw)-         | isReal cw          = let Left w = cwVal cw in show w-         | not (isBounded cw) = let Right w = cwVal cw in shexI False False w-         | True               = let Right w = cwVal cw in shex  False False (hasSign cw, intSizeOf cw) w+         | isReal cw          = let CWAlgReal w = cwVal cw in show w+         | not (isBounded cw) = let CWInteger w = cwVal cw in shexI False False w+         | isUninterpreted cw = show cw+         | True               = let CWInteger w = cwVal cw in shex  False False (hasSign cw, intSizeOf cw) w    bin cw | cwIsBit cw         = binS (cwToBool cw)-         | isReal cw          = let Left w = cwVal cw in show w-         | not (isBounded cw) = let Right w = cwVal cw in sbinI False False w-         | True               = let Right w = cwVal cw in sbin  False False (hasSign cw, intSizeOf cw) w+         | isReal cw          = let CWAlgReal w = cwVal cw in show w+         | not (isBounded cw) = let CWInteger w = cwVal cw in sbinI False False w+         | isUninterpreted cw = show cw+         | True               = let CWInteger w = cwVal cw in sbin  False False (hasSign cw, intSizeOf cw) w  instance (SymWord a, PrettyNum a) => PrettyNum (SBV a) where   hexS s = maybe (show s) (hexS :: a -> String) $ unliteral s   binS s = maybe (show s) (binS :: a -> String) $ unliteral s-  hex  s = maybe (show s) (hex :: a -> String)  $ unliteral s-  bin  s = maybe (show s) (bin :: a -> String)  $ unliteral s+  hex  s = maybe (show s) (hex  :: a -> String) $ unliteral s+  bin  s = maybe (show s) (bin  :: a -> String) $ unliteral s  -- | Show as a hexadecimal value. First bool controls whether type info is printed -- while the second boolean controls wether 0x prefix is printed. The tuple is
Data/SBV/BitVectors/STree.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Implementation of full-binary symbolic trees, providing logarithmic -- time access to elements. Both reads and writes are supported.
Data/SBV/BitVectors/SignCast.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Implementation of casting between signed/unsigned variants of the -- same type.@@ -86,6 +85,7 @@                  KBounded True  _ -> error "Data.SBV.SignCast.genericSign: Called on signed value"                  KUnbounded       -> error "Data.SBV.SignCast.genericSign: Called on unbounded value"                  KReal            -> error "Data.SBV.SignCast.genericSign: Called on real value"+                 KUninterpreted s -> error $ "Data.SBV.SignCast.genericSign: Called on unintepreted sort " ++ s            y st = do xsw <- sbvToSW st x                      newExpr st k (SBVApp (Extract (intSizeOf x-1) 0) [xsw]) @@ -99,6 +99,7 @@                  KBounded False _ -> error "Data.SBV.SignCast.genericUnSign: Called on unsigned value"                  KUnbounded       -> error "Data.SBV.SignCast.genericUnSign: Called on unbounded value"                  KReal            -> error "Data.SBV.SignCast.genericUnSign: Called on real value"+                 KUninterpreted s -> error $ "Data.SBV.SignCast.genericUnSign: Called on unintepreted sort " ++ s            y st = do xsw <- sbvToSW st x                      newExpr st k (SBVApp (Extract (intSizeOf x-1) 0) [xsw])
Data/SBV/BitVectors/Splittable.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Implementation of bit-vector concatanetation and splits -----------------------------------------------------------------------------@@ -63,12 +62,12 @@   extend b = 0 # b  cwSplit :: (SymWord a, Num a) => CW -> (SBV a, SBV a)-cwSplit z@(CW _ (Right v)) = (literal x, literal y)+cwSplit z@(CW _ (CWInteger v)) = (literal x, literal y)   where (x, y) = genSplit (intSizeOf z `div` 2) v cwSplit z = error $ "SBV.cwSplit: Unsupported CW value: " ++ show z  cwJoin :: (SymWord a, Num a) => CW -> CW -> SBV a-cwJoin x@(CW _ (Right a)) (CW _ (Right b)) = literal (genJoin (intSizeOf x) a b)+cwJoin x@(CW _ (CWInteger a)) (CW _ (CWInteger b)) = literal (genJoin (intSizeOf x) a b) cwJoin x y = error $ "SBV.cwJoin: Unsupported arguments: " ++ show (x, y)  -- symbolic instances
Data/SBV/Compilers/C.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Compilation of symbolic programs to C -----------------------------------------------------------------------------@@ -16,14 +15,15 @@  import Control.DeepSeq               (rnf) import Data.Char                     (isSpace)-import Data.List                     (nub)-import Data.Maybe                    (isJust, fromMaybe, isNothing)+import Data.List                     (nub, intercalate)+import Data.Maybe                    (isJust, isNothing, fromJust) import qualified Data.Foldable as F  (toList) import System.FilePath               (takeBaseName, replaceExtension) import System.Random import Text.PrettyPrint.HughesPJ  import Data.SBV.BitVectors.Data+import Data.SBV.BitVectors.AlgReals import Data.SBV.BitVectors.PrettyNum (shex) import Data.SBV.Compilers.CodeGen @@ -82,38 +82,30 @@ die :: String -> a die msg = error $ "SBV->C: Unexpected: " ++ msg --- Unbounded int-dieUnbounded :: a-dieUnbounded = error $    "SBV->C: Unbounded integers are not supported by the C compiler."-                     ++ "\nUse 'cgIntegerSize' to specify a fixed size for SInteger representation."---- Reals-dieReal :: a-dieReal = error "SBV->C: SReal values are not supported by the C compiler."- -- Unsupported features, or features TBD tbd :: String -> a tbd msg = error $ "SBV->C: Not yet supported: " ++ msg  cgen :: CgConfig -> String -> CgState -> Result -> CgPgmBundle cgen cfg nm st sbvProg-   -- we rnf the sig to make sure any exceptions in type conversion pop-out early enough+   -- we rnf the main pg and 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 (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))-                                    ]-        rtc      = cgRTC cfg-        mbISize  = cgInteger cfg+   = rnf (render sig) `seq` rnf (render (vcat body)) `seq` result+  where result = CgPgmBundle bundleKind+                        $ filt [ ("Makefile",  (CgMakefile flags, [genMake (cgGenDriver cfg) nm nmd flags]))+                               , (nm  ++ ".h", (CgHeader [sig],   [genHeader bundleKind nm [sig] extProtos]))+                               , (nmd ++ ".c", (CgDriver,         genDriver cfg randVals nm ins outs mbRet))+                               , (nm  ++ ".c", (CgSource,         body))+                               ]+        body = genCProg cfg nm sig sbvProg ins outs mbRet extDecls+        bundleKind = (cgInteger cfg, cgReal cfg)         randVals = cgDriverVals cfg         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+        sig      = pprCFunHeader nm ins outs mbRet         ins      = cgInputs st         outs     = cgOutputs st         mbRet    = case cgReturns st of@@ -129,88 +121,92 @@                      xs -> vcat $ text "/* User given declarations: */" : map text xs ++ [text ""]         flags    = cgLDFlags st -cSizeOf :: Maybe Int -> HasKind a => a -> Int-cSizeOf mbIntSize x-  | isReal x    = dieReal-  | isInteger x = fromMaybe dieUnbounded mbIntSize-  | True        = intSizeOf x- -- | Pretty print a functions type. If there is only one output, we compile it -- as a function that returns that value. Otherwise, we compile it as a void function -- that takes return values as pointers to be updated.-pprCFunHeader :: Maybe Int -> String -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> Doc-pprCFunHeader mbISize fn ins outs mbRet = retType <+> text fn <> parens (fsep (punctuate comma (map (mkParam mbISize) ins ++ map (mkPParam mbISize) outs)))+pprCFunHeader :: String -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> Doc+pprCFunHeader fn ins outs mbRet = retType <+> text fn <> parens (fsep (punctuate comma (map mkParam ins ++ map mkPParam outs)))   where retType = case mbRet of                    Nothing -> text "void"-                   Just sw -> pprCWord False (hasSign sw, cSizeOf mbISize sw)+                   Just sw -> pprCWord False sw -mkParam, mkPParam :: Maybe Int -> (String, CgVal) -> Doc-mkParam  mbISize (n, CgAtomic sw)     = let sgsz = (hasSign sw, cSizeOf mbISize sw) in pprCWord True  sgsz <+> text n-mkParam  _       (_, CgArray  [])     = die "mkParam: CgArray with no elements!"-mkParam  mbISize (n, CgArray  (sw:_)) = let sgsz = (hasSign sw, cSizeOf mbISize sw) in pprCWord True  sgsz <+> text "*" <> text n-mkPParam mbISize (n, CgAtomic sw)     = let sgsz = (hasSign sw, cSizeOf mbISize sw) in pprCWord False sgsz <+> text "*" <> text n-mkPParam _       (_, CgArray  [])     = die "mPkParam: CgArray with no elements!"-mkPParam mbISize (n, CgArray  (sw:_)) = let sgsz = (hasSign sw, cSizeOf mbISize sw) in pprCWord False sgsz <+> text "*" <> text n+mkParam, mkPParam :: (String, CgVal) -> Doc+mkParam  (n, CgAtomic sw)     = pprCWord True  sw <+> text n+mkParam  (_, CgArray  [])     = die "mkParam: CgArray with no elements!"+mkParam  (n, CgArray  (sw:_)) = pprCWord True  sw <+> text "*" <> text n+mkPParam (n, CgAtomic sw)     = pprCWord False sw <+> text "*" <> text n+mkPParam (_, CgArray  [])     = die "mPkParam: CgArray with no elements!"+mkPParam (n, CgArray  (sw:_)) = pprCWord False sw <+> text "*" <> text n  -- | Renders as "const SWord8 s0", etc. the first parameter is the width of the typefield-declSW :: Maybe Int -> Int -> SW -> Doc-declSW mbISize w sw = text "const" <+> pad (showCType (hasSign sw, cSizeOf mbISize sw)) <+> text (show sw)+declSW :: Int -> SW -> Doc+declSW w sw = text "const" <+> pad (showCType sw) <+> text (show sw)   where pad s = text $ s ++ replicate (w - length s) ' '  -- | Renders as "s0", etc, or the corresponding constant-showSW :: Maybe Int -> [(SW, CW)] -> SW -> Doc-showSW mbISize consts sw+showSW :: CgConfig -> [(SW, CW)] -> SW -> Doc+showSW cfg consts sw   | sw == falseSW                 = text "false"   | sw == trueSW                  = text "true"-  | Just cw <- sw `lookup` consts = showConst mbISize cw+  | Just cw <- sw `lookup` consts = mkConst cfg cw   | True                          = text $ show sw  -- | 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)+pprCWord :: HasKind a => Bool -> a -> Doc+pprCWord cnst v = (if cnst then text "const" else empty) <+> text (showCType v) -showCType :: (Bool, Int) -> String-showCType (False, 1) = "SBool"-showCType (s, sz)-  | sz `elem` [8, 16, 32, 64] = t-  | True                      = die $ "Non-regular bitvector type: " ++ t- where t = (if s then "SInt" else "SWord") ++ show sz+showCType :: HasKind a => a -> String+showCType = show . kindOf  -- | The printf specifier for the type-specifier :: (Bool, Int) -> Doc-specifier (False,  1) = text "%d"-specifier (False,  8) = text "%\"PRIu8\""-specifier (True,   8) = text "%\"PRId8\""-specifier (False, 16) = text "0x%04\"PRIx16\"U"-specifier (True,  16) = text "%\"PRId16\""-specifier (False, 32) = text "0x%08\"PRIx32\"UL"-specifier (True,  32) = text "%\"PRId32\"L"-specifier (False, 64) = text "0x%016\"PRIx64\"ULL"-specifier (True,  64) = text "%\"PRId64\"LL"-specifier (s, sz)     = die $ "Format specifier at type " ++ (if s then "SInt" else "SWord") ++ show sz+specifier :: CgConfig -> SW -> Doc+specifier cfg sw = case kindOf sw of+                     KBounded b i     -> spec (b, i)+                     KUnbounded       -> spec (True, fromJust (cgInteger cfg))+                     KReal            -> specF (fromJust (cgReal cfg))+                     KUninterpreted s -> die $ "uninterpreted sort: " ++ s+  where spec :: (Bool, Int) -> Doc+        spec (False,  1) = text "%d"+        spec (False,  8) = text "%\"PRIu8\""+        spec (True,   8) = text "%\"PRId8\""+        spec (False, 16) = text "0x%04\"PRIx16\"U"+        spec (True,  16) = text "%\"PRId16\""+        spec (False, 32) = text "0x%08\"PRIx32\"UL"+        spec (True,  32) = text "%\"PRId32\"L"+        spec (False, 64) = text "0x%016\"PRIx64\"ULL"+        spec (True,  64) = text "%\"PRId64\"LL"+        spec (s, sz)     = die $ "Format specifier at type " ++ (if s then "SInt" else "SWord") ++ show sz+        specF :: CgSRealType -> Doc+        specF CgFloat      = text "%f"+        specF CgDouble     = text "%f"+        specF CgLongDouble = text "%Lf"  -- | Make a constant value of the given type. We don't check for out of bounds here, as it should not be needed. --   There are many options here, using binary, decimal, etc. We simply --   8-bit or less constants using decimal; otherwise we use hex. --   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) = 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"-mkConst i t@(True,  16) = text (shex False True t i)-mkConst i t@(False, 32) = text (shex False True t i) <> text "UL"-mkConst i t@(True,  32) = text (shex False True t i) <> text "L"-mkConst i t@(False, 64) = text (shex False True t i) <> text "ULL"-mkConst i t@(True,  64) = text (shex False True t i) <> text "LL"-mkConst i   (True,  1)  = die $ "Signed 1-bit value " ++ show i-mkConst i   (s, sz)     = die $ "Constant " ++ show i ++ " at type " ++ (if s then "SInt" else "SWord") ++ show sz+mkConst :: CgConfig -> CW -> Doc+mkConst cfg  (CW KReal (CWAlgReal (AlgRational _ r))) = double (fromRational r :: Double) <> sRealSuffix (fromJust (cgReal cfg))+  where sRealSuffix CgFloat      = text "F"+        sRealSuffix CgDouble     = empty+        sRealSuffix CgLongDouble = text "L"+mkConst cfg (CW KUnbounded       (CWInteger i)) = showSizedConst i (True, fromJust (cgInteger cfg))+mkConst _   (CW (KBounded sg sz) (CWInteger i)) = showSizedConst i (sg,   sz)+mkConst _   cw                                  = die $ "mkConst: " ++ show cw --- | Show a constant-showConst :: Maybe Int -> CW -> Doc-showConst mbISize  cw@(CW _ (Right v)) = mkConst v (hasSign cw, cSizeOf mbISize cw)-showConst _mbISize cw                  = die $ "showConst: " ++ show cw+showSizedConst :: Integer -> (Bool, Int) -> Doc+showSizedConst i   (False,  1) = text (if i == 0 then "false" else "true")+showSizedConst i   (False,  8) = integer i+showSizedConst i   (True,   8) = integer i+showSizedConst i t@(False, 16) = text (shex False True t i) <> text "U"+showSizedConst i t@(True,  16) = text (shex False True t i)+showSizedConst i t@(False, 32) = text (shex False True t i) <> text "UL"+showSizedConst i t@(True,  32) = text (shex False True t i) <> text "L"+showSizedConst i t@(False, 64) = text (shex False True t i) <> text "ULL"+showSizedConst i t@(True,  64) = text (shex False True t i) <> text "LL"+showSizedConst i   (True,  1)  = die $ "Signed 1-bit value " ++ show i+showSizedConst i   (s, sz)     = die $ "Constant " ++ show i ++ " at type " ++ (if s then "SInt" else "SWord") ++ show sz  -- | Generate a makefile. The first argument is True if we have a driver. genMake :: Bool -> String -> String -> [String] -> Doc@@ -254,8 +250,8 @@        nmdo = nmd <> text ".o"  -- | Generate the header-genHeader :: String -> [Doc] -> Doc -> Doc-genHeader fn sigs protos =+genHeader :: (Maybe Int, Maybe CgSRealType) -> String -> [Doc] -> Doc -> Doc+genHeader (ik, rk) fn sigs protos =      text "/* Header file for" <+> nm <> text ". Automatically generated by SBV. Do not edit! */"   $$ text ""   $$ text "#ifndef" <+> tag@@ -280,6 +276,8 @@   $$ text "typedef int32_t SInt32;"   $$ text "typedef int64_t SInt64;"   $$ text ""+  $$ imapping+  $$ rmapping   $$ text ("/* Entry point prototype" ++ plu ++ ": */")   $$ vcat (map (<> semi) sigs)   $$ text ""@@ -289,13 +287,25 @@  where nm  = text fn        tag = text "__" <> nm <> text "__HEADER_INCLUDED__"        plu = if length sigs /= 1 then "s" else ""+       imapping = case ik of+                    Nothing -> empty+                    Just i  ->    text "/* User requested mapping for SInteger.                                 */"+                               $$ text "/* NB. Loss of precision: Target type is subject to modular arithmetic. */"+                               $$ text ("typedef SInt" ++ show i ++ " SInteger;")+                               $$ text ""+       rmapping = case rk of+                    Nothing -> empty+                    Just t  ->    text "/* User requested mapping for SReal.                          */"+                               $$ text "/* NB. Loss of precision: Target type is subject to rounding. */"+                               $$ text ("typedef " ++ show t ++ " SReal;")+                               $$ text ""  sepIf :: Bool -> Doc sepIf b = if b then text "" else empty  -- | Generate an example driver program-genDriver :: Maybe Int -> [Integer] -> String -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> [Doc]-genDriver mbISize randVals fn inps outs mbRet = [pre, header, body, post]+genDriver :: CgConfig -> [Integer] -> String -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> [Doc]+genDriver cfg randVals fn inps outs mbRet = [pre, header, body, post]  where pre    =  text "/* Example driver program for" <+> nm <> text ". */"               $$ text "/* Automatically generated by SBV. Edit as you see fit! */"               $$ text ""@@ -314,7 +324,7 @@                       $$ call                       $$ text ""                       $$ (case mbRet of-                              Just sw -> text "printf" <> parens (printQuotes (fcall <+> text "=" <+> specifier (hasSign sw, cSizeOf mbISize sw) <> text "\\n")+                              Just sw -> text "printf" <> parens (printQuotes (fcall <+> text "=" <+> specifier cfg sw <> text "\\n")                                                                               <> comma <+> resultVar) <> semi                               Nothing -> text "printf" <> parens (printQuotes (fcall <+> text "->\\n")) <> semi)                       $$ vcat (map display outs)@@ -334,41 +344,30 @@           | True                                            = (map (mkRVal sw) frs, n, a) : matchRands srs cs           where l          = length sws                 (frs, srs) = splitAt l rs-       mkRVal sw r = mkConst ival sgsz-         where sgsz@(sg, sz) = (hasSign sw, cSizeOf mbISize sw)-               ival | r >= minVal && r <= maxVal = r-                    | not sg                     = r `mod` (2^sz)-                    | True                       = (r `mod` (2^sz)) - (2^(sz-1))-                    where expSz, expSz', minVal, maxVal :: Integer-                          expSz  = 2^(sz-1)-                          expSz' = 2*expSz-                          minVal | not sg = 0-                                 | True   = -expSz-                          maxVal | not sg = expSz'-1-                                 | True   = expSz-1+       mkRVal sw r = mkConst cfg $ mkConstCW (kindOf sw) r        mkInp (_,  _, CgAtomic{})         = empty  -- constant, no need to declare        mkInp (_,  n, CgArray [])         = die $ "Unsupported empty array value for " ++ show n-       mkInp (vs, n, CgArray sws@(sw:_)) =  pprCWord True (hasSign sw, cSizeOf mbISize sw) <+> text n <> brackets (int (length sws)) <+> text "= {"+       mkInp (vs, n, CgArray sws@(sw:_)) =  pprCWord True sw <+> text n <> brackets (int (length sws)) <+> text "= {"                                                       $$ nest 4 (fsep (punctuate comma (align vs)))                                                       $$ text "};"                                          $$ text ""                                          $$ text "printf" <> parens (printQuotes (text "Contents of input array" <+> text n <> text ":\\n")) <> semi                                          $$ display (n, CgArray sws)                                          $$ text ""-       mkOut (v, CgAtomic sw)            = let sgsz = (hasSign sw, cSizeOf mbISize sw) in pprCWord False sgsz <+> text v <> semi+       mkOut (v, CgAtomic sw)            = pprCWord False sw <+> text v <> semi        mkOut (v, CgArray [])             = die $ "Unsupported empty array value for " ++ show v-       mkOut (v, CgArray sws@(sw:_))     = pprCWord False (hasSign sw, cSizeOf mbISize sw) <+> text v <> brackets (int (length sws)) <> semi+       mkOut (v, CgArray sws@(sw:_))     = pprCWord False sw <+> text v <> brackets (int (length sws)) <> semi        resultVar = text "__result"        call = case mbRet of                 Nothing -> fcall <> semi-                Just sw -> pprCWord True (hasSign sw, cSizeOf mbISize sw) <+> resultVar <+> text "=" <+> fcall <> semi+                Just sw -> pprCWord True sw <+> resultVar <+> text "=" <+> fcall <> semi        fcall = nm <> parens (fsep (punctuate comma (map mkCVal pairedInputs ++ map mkOVal outs)))        mkCVal ([v], _, CgAtomic{}) = v        mkCVal (vs,  n, CgAtomic{}) = die $ "Unexpected driver value computed for " ++ show n ++ render (hcat vs)        mkCVal (_,   n, CgArray{})  = text n        mkOVal (n, CgAtomic{})      = text "&" <> text n        mkOVal (n, CgArray{})       = text n-       display (n, CgAtomic sw)         = text "printf" <> parens (printQuotes (text " " <+> text n <+> text "=" <+> specifier (hasSign sw, cSizeOf mbISize sw)+       display (n, CgAtomic sw)         = text "printf" <> parens (printQuotes (text " " <+> text n <+> text "=" <+> specifier cfg sw                                                                                 <> text "\\n") <> comma <+> text n) <> semi        display (n, CgArray [])         =  die $ "Unsupported empty array value for " ++ show n        display (n, CgArray sws@(sw:_)) =   text "int" <+> nctr <> semi@@ -378,17 +377,28 @@                   where nctr      = text n <> text "_ctr"                         entry     = text n <> text "[" <> nctr <> text "]"                         entrySpec = text n <> text "[%d]"-                        spec      = specifier (hasSign sw, cSizeOf mbISize sw)+                        spec      = specifier cfg sw  -- | Generate the C program-genCProg :: Bool -> Maybe Int -> String -> Doc -> Result -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> Doc -> [Doc]-genCProg rtc mbISize fn proto (Result hasInfPrec _ cgs ins preConsts tbls arrs _ _ asgns cstrs _) inVars outVars mbRet extDecls-  | isNothing mbISize && hasInfPrec = dieUnbounded-  | not (null cstrs)                = tbd "Explicit constraints"-  | not (null arrs)                 = tbd "User specified arrays"-  | needsExistentials (map fst ins) = error "SBV->C: Cannot compile functions with existentially quantified variables."-  | True                            = [pre, header, post]- where pre    = text "/* File:" <+> doubleQuotes (nm <> text ".c") <> text ". Automatically generated by SBV. Do not edit! */"+genCProg :: CgConfig -> String -> Doc -> Result -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> Doc -> [Doc]+genCProg cfg fn proto (Result (hasIntegers, hasReals) usorts _tvals cgs ins preConsts tbls arrs _ _ asgns cstrs _) inVars outVars mbRet extDecls+  | isNothing (cgInteger cfg) && hasIntegers+  = error $ "SBV->C: Unbounded integers are not supported by the C compiler."+          ++ "\nUse 'cgIntegerSize' to specify a fixed size for SInteger representation."+  | isNothing (cgReal cfg) && hasReals+  = error $ "SBV->C: SReal values are not supported by the C compiler."+          ++ "\nUse 'cgSRealType' to specify a custom type for SReal representation."+  | not (null usorts)+  = error $ "SBV->C: Cannot compile functions with uninterpreted sorts: " ++ intercalate ", " usorts+  | not (null cstrs)+  = tbd "Explicit constraints"+  | not (null arrs)+  = tbd "User specified arrays"+  | needsExistentials (map fst ins)+  = error "SBV->C: Cannot compile functions with existentially quantified variables."+  | True+  = [pre, header, post]+ where pre    =  text "/* File:" <+> doubleQuotes (nm <> text ".c") <> text ". Automatically generated by SBV. Do not edit! */"               $$ text ""               $$ text "#include <inttypes.h>"               $$ text "#include <stdint.h>"@@ -413,39 +423,37 @@        codeSeg (fnm, ls) =  text "/* User specified custom code for" <+> doubleQuotes (text fnm) <+> text "*/"                          $$ vcat (map text ls)                          $$ text ""-       typeWidth = getMax 0 [len (hasSign s, cSizeOf mbISize s) | (s, _) <- assignments]-                where len (False, 1) = 5 -- SBool-                      len (False, n) = 5 + length (show n) -- SWordN-                      len (True,  n) = 4 + length (show n) -- SIntN-                      getMax 7 _      = 7  -- 7 is the max we can get with SWord64, so don't bother looking any further+       typeWidth = getMax 0 [len (kindOf s) | (s, _) <- assignments]+                where len (KReal{})          = 5+                      len (KUnbounded{})     = 8+                      len (KBounded False 1) = 5 -- SBool+                      len (KBounded False n) = 5 + length (show n) -- SWordN+                      len (KBounded True  n) = 4 + length (show n) -- SIntN+                      len (KUninterpreted s) = die $ "Uninterpreted sort: " ++ s+                      getMax 8 _      = 8  -- 8 is the max we can get with SInteger, so don't bother looking any further                       getMax m []     = m                       getMax m (x:xs) = getMax (m `max` x) xs        consts = (falseSW, falseCW) : (trueSW, trueCW) : preConsts        isConst s = isJust (lookup s consts)        genIO :: Bool -> (String, CgVal) -> [Doc]-       genIO True  (cNm, CgAtomic sw) = [declSW mbISize typeWidth sw  <+> text "=" <+> text cNm <> semi]-       genIO False (cNm, CgAtomic sw) = [text "*" <> text cNm <+> text "=" <+> showSW mbISize consts sw <> semi]+       genIO True  (cNm, CgAtomic sw) = [declSW typeWidth sw  <+> text "=" <+> text cNm <> semi]+       genIO False (cNm, CgAtomic sw) = [text "*" <> text cNm <+> text "=" <+> showSW cfg consts sw <> semi]        genIO isInp (cNm, CgArray sws) = zipWith genElt sws [(0::Int)..]          where genElt sw i-                 | isInp = declSW mbISize typeWidth sw <+> text "=" <+> text entry       <> semi-                 | True  = text entry                  <+> text "=" <+> showSW mbISize consts sw <> semi+                 | isInp = declSW typeWidth sw <+> text "=" <+> text entry       <> semi+                 | True  = text entry          <+> text "=" <+> showSW cfg consts sw <> semi                  where entry = cNm ++ "[" ++ show i ++ "]"-       mkRet sw = text "return" <+> showSW mbISize consts sw <> semi+       mkRet sw = text "return" <+> showSW cfg consts sw <> semi        genTbl :: ((Int, Kind, Kind), [SW]) -> (Int, Doc)-       genTbl ((i, _, k), elts) =  (location, static <+> pprCWord True (sg, szv) <+> text ("table" ++ show i) <> text "[] = {"-                                              $$ nest 4 (fsep (punctuate comma (align (map (showSW mbISize consts) elts))))+       genTbl ((i, _, k), elts) =  (location, static <+> text "const" <+> text (show k) <+> text ("table" ++ show i) <> text "[] = {"+                                              $$ nest 4 (fsep (punctuate comma (align (map (showSW cfg consts) elts))))                                               $$ text "};")-         where (sg, szv) = case (mbISize, k) of-                            (_,       KBounded b v) -> (b, v)-                            (Just is, KUnbounded)   -> (True, is)-                            (Nothing, KUnbounded)   -> dieUnbounded-                            (_,       KReal)        -> dieReal-               static   = if location == -1 then text "static" else empty+         where static   = if location == -1 then text "static" else empty                location = maximum (-1 : map getNodeId elts)        getNodeId s@(SW _ (NodeId n)) | isConst s = -1                                      | True      = n        genAsgn :: (SW, SBVExpr) -> (Int, Doc)-       genAsgn (sw, n) = (getNodeId sw, declSW mbISize typeWidth sw <+> text "=" <+> ppExpr mbISize rtc consts n <> semi)+       genAsgn (sw, n) = (getNodeId sw, declSW typeWidth sw <+> text "=" <+> ppExpr cfg consts n <> semi)        -- merge tables intermixed with assignments, paying attention to putting tables as        -- early as possible.. Note that the assignment list (second argument) is sorted on its order        merge :: [(Int, Doc)] -> [(Int, Doc)] -> [Doc]@@ -455,30 +463,27 @@          | i < i'                                 = t : merge trest as          | True                                   = a : merge ts arest -ppExpr :: Maybe Int -> Bool -> [(SW, CW)] -> SBVExpr -> Doc-ppExpr mbISize rtc consts (SBVApp op opArgs) = p op (map (showSW mbISize consts) opArgs)-  where cBinOps = [ (Plus, "+"), (Times, "*"), (Minus, "-")-                  , (Equal, "=="), (NotEqual, "!=")-                  , (LessThan, "<"), (GreaterThan, ">"), (LessEq, "<="), (GreaterEq, ">=")+ppExpr :: CgConfig -> [(SW, CW)] -> SBVExpr -> Doc+ppExpr cfg consts (SBVApp op opArgs) = p op (map (showSW cfg consts) opArgs)+  where rtc = cgRTC cfg+        cBinOps = [ (Plus, "+"),  (Times, "*"), (Minus, "-")+                  , (Equal, "=="), (NotEqual, "!="), (LessThan, "<"), (GreaterThan, ">"), (LessEq, "<="), (GreaterEq, ">=")                   , (And, "&"), (Or, "|"), (XOr, "^")                   ]         p (ArrRead _)       _  = tbd "User specified arrays (ArrRead)"         p (ArrEq _ _)       _  = tbd "User specified arrays (ArrEq)"         p (Uninterpreted s) [] = text "/* Uninterpreted constant */" <+> text s         p (Uninterpreted s) as = text "/* Uninterpreted function */" <+> text s <> parens (fsep (punctuate comma as))-        p (Extract i j) [a]    = extract i j (let s = head opArgs in (hasSign s, cSizeOf mbISize s)) a-        p Join [a, b]          = join (let (s1 : s2 : _) = opArgs in ((hasSign s1, cSizeOf mbISize s1), (hasSign s2, cSizeOf mbISize s2), a, b))-        p (Rol i) [a]          = rotate True  i a (let s = head opArgs in (hasSign s, cSizeOf mbISize s))-        p (Ror i) [a]          = rotate False i a (let s = head opArgs in (hasSign s, cSizeOf mbISize s))-        p (Shl i) [a]          = shift True  i a (let s = head opArgs in (hasSign s, cSizeOf mbISize s))-        p (Shr i) [a]          = shift False i a (let s = head opArgs in (hasSign s, cSizeOf mbISize s))-        p Not [a]-          -- be careful about booleans, bitwise complement is not correct for them!-          | s == 1-          = text "!" <> a-          | True-          = text "~" <> a-          where s = cSizeOf mbISize (head opArgs)+        p (Extract i j) [a]    = extract i j (head opArgs) a+        p Join [a, b]          = join (let (s1 : s2 : _) = opArgs in (s1, s2, a, b))+        p (Rol i) [a]          = rotate True  i a (head opArgs)+        p (Ror i) [a]          = rotate False i a (head opArgs)+        p (Shl i) [a]          = shift  True  i a (head opArgs)+        p (Shr i) [a]          = shift  False i a (head opArgs)+        p Not [a]              = case kindOf (head opArgs) of+                                   -- be careful about booleans, bitwise complement is not correct for them!+                                   KBounded False 1 -> text "!" <> a+                                   _                -> text "~" <> a         p Ite [a, b, c] = a <+> text "?" <+> b <+> text ":" <+> c         p (LkUp (t, k, _, len) ind def) []           | not rtc                    = lkUp -- ignore run-time-checks per user request@@ -486,19 +491,21 @@           | needsCheckL                = cndLkUp checkLeft           | needsCheckR                = cndLkUp checkRight           | True                       = lkUp-          where (as, at) = case (mbISize, k) of-                            (_,       KBounded b v) -> (b, v)-                            (Just i,  KUnbounded)   -> (True, i)-                            (Nothing, KUnbounded)   -> dieUnbounded-                            (_,       KReal)        -> dieReal-                [index, defVal] = map (showSW mbISize consts) [ind, def]-                lkUp = text "table" <> int t <> brackets (showSW mbISize consts ind)+          where [index, defVal] = map (showSW cfg consts) [ind, def]+                lkUp = text "table" <> int t <> brackets (showSW cfg consts ind)                 cndLkUp cnd = cnd <+> text "?" <+> defVal <+> text ":" <+> lkUp                 checkLeft  = index <+> text "< 0"                 checkRight = index <+> text ">=" <+> int len                 checkBoth  = parens (checkLeft <+> text "||" <+> checkRight)-                (needsCheckL, needsCheckR) | as   = (True,  (2::Integer)^(at-1)-1  >= fromIntegral len)-                                           | True = (False, (2::Integer)^at    -1  >= fromIntegral len)+                canOverflow True  sz = (2::Integer)^(sz-1)-1 >= fromIntegral len+                canOverflow False sz = (2::Integer)^sz    -1 >= fromIntegral len+                (needsCheckL, needsCheckR) = case k of+                                               KBounded sg sz   -> (sg, canOverflow sg sz)+                                               KReal            -> die "array index with real value"+                                               KUnbounded       -> case cgInteger cfg of+                                                                     Nothing -> (True, True) -- won't matter, it'll be rejected later+                                                                     Just i  -> (True, canOverflow True i)+                                               KUninterpreted s -> die $ "Uninterpreted sort: " ++ s         -- Div/Rem should be careful on 0, in the SBV world x `div` 0 is 0, x `rem` 0 is x         p Quot [a, b] = parens (b <+> text "== 0") <+> text "?" <+> text "0" <+> text ":" <+> parens (a <+> text "/" <+> b)         p Rem  [a, b] = parens (b <+> text "== 0") <+> text "?" <+>    a     <+> text ":" <+> parens (a <+> text "%" <+> b)@@ -506,47 +513,54 @@           | Just co <- lookup o cBinOps           = a <+> text co <+> b         p o args = die $ "Received operator " ++ show o ++ " applied to " ++ show args-        shift toLeft i a (sg, sz)-          | i < 0   = shift (not toLeft) (-i) a (sg, sz)+        shift toLeft i a s+          | i < 0   = shift (not toLeft) (-i) a s           | i == 0  = a-          | i >= sz = mkConst 0 (sg, sz)-          | True    = a <+> text cop <+> int i+          | True    = case kindOf s of+                        KBounded _ sz | i >= sz -> mkConst cfg $ mkConstCW (kindOf s) (0::Integer)+                        KReal                   -> tbd $ "Shift for real quantity: " ++ show (toLeft, i, s)+                        _                       -> a <+> text cop <+> int i           where cop | toLeft = "<<"                     | True   = ">>"-        rotate toLeft i a (True, sz)-          = tbd $ "Rotation of signed words at size " ++ show (toLeft, i, a, sz)-        rotate toLeft i a (False, sz)-          | i < 0   = rotate (not toLeft) (-i) a (False, sz)+        rotate toLeft i a s+          | i < 0   = rotate (not toLeft) (-i) a s           | i == 0  = a-          | i >= sz = rotate toLeft (i `mod` sz) a (False, sz)-          | True    =     parens (a <+> text cop  <+> int i)-                      <+> text "|"-                      <+> parens (a <+> text cop' <+> int (sz - i))+          | True    = case kindOf s of+                        KBounded True _             -> tbd $ "Rotation of signed quantities: " ++ show (toLeft, i, s)+                        KBounded False sz | i >= sz -> rotate toLeft (i `mod` sz) a s+                        KBounded False sz           ->     parens (a <+> text cop  <+> int i)+                                                      <+> text "|"+                                                      <+> parens (a <+> text cop' <+> int (sz - i))+                        KUnbounded                  -> shift toLeft i a s -- For SInteger, rotate is the same as shift in Haskell+                        _                           -> tbd $ "Rotation for unbounded quantity: " ++ show (toLeft, i, s)           where (cop, cop') | toLeft = ("<<", ">>")                             | True   = (">>", "<<")         -- TBD: below we only support the values that SBV actually currently generates.         -- we would need to add new ones if we generate others. (Check instances in Data/SBV/BitVectors/Splittable.hs).-        extract 63 32 (False, 64) a = text "(SWord32)" <+> parens (a <+> text ">> 32")-        extract 31  0 (False, 64) a = text "(SWord32)" <+> a-        extract 31 16 (False, 32) a = text "(SWord16)" <+> parens (a <+> text ">> 16")-        extract 15  0 (False, 32) a = text "(SWord16)" <+> a-        extract 15  8 (False, 16) a = text "(SWord8)"  <+> parens (a <+> text ">> 8")-        extract  7  0 (False, 16) a = text "(SWord8)"  <+> a-        -- the followings are used by sign-conversions. (Check instances in Data/SBV/BitVectors/SignCast.hs).-        extract 63  0 (False, 64) a = text "(SInt64)"  <+> a-        extract 63  0 (True,  64) a = text "(SWord64)" <+> a-        extract 31  0 (False, 32) a = text "(SInt32)"  <+> a-        extract 31  0 (True,  32) a = text "(SWord32)" <+> a-        extract 15  0 (False, 16) a = text "(SInt16)"  <+> a-        extract 15  0 (True,  16) a = text "(SWord16)" <+> a-        extract  7  0 (False,  8) a = text "(SInt8)"   <+> a-        extract  7  0 (True,   8) a = text "(SWord8)"  <+> a-        extract  i  j (sg, sz)    _ = tbd $ "extract with " ++ show (i, j, (sg, sz))+        extract hi lo i a = case (hi, lo, kindOf i) of+                              ( 0,  0, KUnbounded)        -> text "(SReal)" <+> a  -- special SInteger -> SReal conversion+                              (63, 32, KBounded False 64) -> text "(SWord32)" <+> parens (a <+> text ">> 32")+                              (31,  0, KBounded False 64) -> text "(SWord32)" <+> a+                              (31, 16, KBounded False 32) -> text "(SWord16)" <+> parens (a <+> text ">> 16")+                              (15,  0, KBounded False 32) -> text "(SWord16)" <+> a+                              (15,  8, KBounded False 16) -> text "(SWord8)"  <+> parens (a <+> text ">> 8")+                              ( 7,  0, KBounded False 16) -> text "(SWord8)"  <+> a+                              -- the followings are used by sign-conversions. (Check instances in Data/SBV/BitVectors/SignCast.hs).+                              (63,  0, KBounded False 64) -> text "(SInt64)"  <+> a+                              (63,  0, KBounded True  64) -> text "(SWord64)" <+> a+                              (31,  0, KBounded False 32) -> text "(SInt32)"  <+> a+                              (31,  0, KBounded True  32) -> text "(SWord32)" <+> a+                              (15,  0, KBounded False 16) -> text "(SInt16)"  <+> a+                              (15,  0, KBounded True  16) -> text "(SWord16)" <+> a+                              ( 7,  0, KBounded False  8) -> text "(SInt8)"   <+> a+                              ( 7,  0, KBounded True   8) -> text "(SWord8)"  <+> a+                              ( _,  _, k                ) -> tbd $ "extract with " ++ show (hi, lo, k, i)         -- TBD: ditto here for join, just like extract above-        join ((False,  8), (False,  8), a, b) = parens (parens (text "(SWord16)" <+> a) <+> text "<< 8")  <+> text "|" <+> parens (text "(SWord16)" <+> b)-        join ((False, 16), (False, 16), a, b) = parens (parens (text "(SWord32)" <+> a) <+> text "<< 16") <+> text "|" <+> parens (text "(SWord32)" <+> b)-        join ((False, 32), (False, 32), a, b) = parens (parens (text "(SWord64)" <+> a) <+> text "<< 32") <+> text "|" <+> parens (text "(SWord64)" <+> b)-        join (sgsz1, sgsz2, _, _)             = tbd $ "join with " ++ show (sgsz1, sgsz2)+        join (i, j, a, b) = case (kindOf i, kindOf j) of+                              (KBounded False  8, KBounded False  8) -> parens (parens (text "(SWord16)" <+> a) <+> text "<< 8")  <+> text "|" <+> parens (text "(SWord16)" <+> b)+                              (KBounded False 16, KBounded False 16) -> parens (parens (text "(SWord32)" <+> a) <+> text "<< 16") <+> text "|" <+> parens (text "(SWord32)" <+> b)+                              (KBounded False 32, KBounded False 32) -> parens (parens (text "(SWord64)" <+> a) <+> text "<< 32") <+> text "|" <+> parens (text "(SWord64)" <+> b)+                              (k1,                k2)                -> tbd $ "join with " ++ show ((k1, i), (k2, j))  -- same as doubleQuotes, except we have to make sure there are no line breaks.. -- Otherwise breaks the generated code.. sigh@@ -570,8 +584,16 @@  -- | Merge a bunch of bundles to generate code for a library mergeToLib :: String -> [CgPgmBundle] -> CgPgmBundle-mergeToLib libName bundles = CgPgmBundle $ sources ++ libHeader : [libDriver | anyDriver] ++ [libMake | anyMake]-  where files       = concat [fs | CgPgmBundle fs <- bundles]+mergeToLib libName bundles+  | length nubKinds /= 1+  = error $  "Cannot merge programs with differing SInteger/SReal mappings. Received the following kinds:\n"+          ++ unlines (map show nubKinds)+  | True+  = CgPgmBundle bundleKind $ sources ++ libHeader : [libDriver | anyDriver] ++ [libMake | anyMake]+  where kinds       = [k | CgPgmBundle k _ <- bundles]+        nubKinds    = nub kinds+        bundleKind  = head nubKinds+        files       = concat [fs | CgPgmBundle _ fs <- bundles]         sigs        = concat [ss | (_, (CgHeader ss, _)) <- files]         anyMake     = not (null [() | (_, (CgMakefile{}, _)) <- files])         drivers     = [ds | (_, (CgDriver, ds)) <- files]@@ -579,7 +601,7 @@         mkFlags     = nub (concat [xs | (_, (CgMakefile xs, _)) <- files])         sources     = [(f, (CgSource, [pre, libHInclude, post])) | (f, (CgSource, [pre, _, post])) <- files]         sourceNms   = map fst sources-        libHeader   = (libName ++ ".h", (CgHeader sigs, [genHeader libName sigs empty]))+        libHeader   = (libName ++ ".h", (CgHeader sigs, [genHeader bundleKind libName sigs empty]))         libHInclude = text "#include" <+> text (show (libName ++ ".h"))         libMake     = ("Makefile", (CgMakefile mkFlags, [genLibMake anyDriver libName sourceNms mkFlags]))         libDriver   = (libName ++ "_driver.c", (CgDriver, mergeDrivers libName libHInclude (zip (map takeBaseName sourceNms) drivers)))
Data/SBV/Compilers/CodeGen.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Code generation utilities -----------------------------------------------------------------------------@@ -33,16 +32,17 @@  -- | 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-        , cgGenMakefile :: Bool          -- ^ If 'True', will generate a makefile+          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)+        , cgReal        :: Maybe CgSRealType  -- ^ Type to use for representing SReal (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, cgGenMakefile = True }+defaultCgConfig = CgConfig { cgRTC = False, cgInteger = Nothing, cgReal = Nothing, cgDriverVals = [], cgGenDriver = True, cgGenMakefile = True }  -- | Abstraction of target language values data CgVal = CgAtomic SW@@ -96,10 +96,33 @@ cgIntegerSize :: Int -> SBVCodeGen () cgIntegerSize i   | i `notElem` [8, 16, 32, 64]-  = error $ "SBV.cgIntegrerSize: Argument must be one of 8, 16, 32, or 64. Received: " ++ show i+  = error $ "SBV.cgIntegerSize: Argument must be one of 8, 16, 32, or 64. Received: " ++ show i   | True   = modify (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgInteger = Just i }}) +-- | Possible mappings for the 'SReal' type when translated to C. Used in conjunction+-- with the function 'cgSRealType'. Note that the particular characteristics of the+-- mapped types depend on the platform and the compiler used for compiling the generated+-- C program. See <http://en.wikipedia.org/wiki/C_data_types> for details.+data CgSRealType = CgFloat      -- ^ @float@+                 | CgDouble     -- ^ @double@+                 | CgLongDouble -- ^ @long double@+                 deriving Eq++-- As they would be used in a C program+instance Show CgSRealType where+  show CgFloat      = "float"+  show CgDouble     = "double"+  show CgLongDouble = "long double"++-- | Sets the C type to be used for representing the 'SReal' type in the generated C code.+-- The setting can be one of C's @"float"@, @"double"@, or @"long double"@, types, depending+-- on the precision needed. Note that this is essentially unsafe as the semantics of+-- infinite precision SReal values becomes reduced to the corresponding floating point type in+-- C, and hence it is subject to rounding errors.+cgSRealType :: CgSRealType -> SBVCodeGen ()+cgSRealType rt = modify (\s -> s {cgFinalConfig = (cgFinalConfig s) { cgReal = Just rt }})+ -- | 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 ()@@ -125,7 +148,7 @@                                  new = if null old then ss else old ++ [""] ++ ss                              in s { cgDecls = new }) --- | Adds the given words to the compiler options in the generated Makefile, useful for linking extra stuff in+-- | Adds the given words to the compiler options in the generated Makefile, useful for linking extra stuff in. cgAddLDFlags :: [String] -> SBVCodeGen () cgAddLDFlags ss = modify (\s -> s { cgLDFlags = cgLDFlags s ++ ss }) @@ -176,7 +199,7 @@   where sz = length vs  -- | Representation of a collection of generated programs.-newtype CgPgmBundle = CgPgmBundle [(FilePath, (CgPgmKind, [Doc]))]+data CgPgmBundle = CgPgmBundle (Maybe Int, Maybe CgSRealType) [(FilePath, (CgPgmKind, [Doc]))]  -- | Different kinds of "files" we can produce. Currently this is quite "C" specific. data CgPgmKind = CgMakefile [String]@@ -195,7 +218,7 @@ isCgMakefile _            = False  instance Show CgPgmBundle where-   show (CgPgmBundle fs) = intercalate "\n" $ map showFile fs+   show (CgPgmBundle _ fs) = intercalate "\n" $ map showFile fs     where showFile :: (FilePath, (CgPgmKind, [Doc])) -> String           showFile (f, (_, ds)) =  "== BEGIN: " ++ show f ++ " ================\n"                                 ++ render' (vcat ds)@@ -217,8 +240,8 @@  -- | Render a code-gen bundle to a directory or to stdout renderCgPgmBundle :: Maybe FilePath -> CgPgmBundle -> IO ()-renderCgPgmBundle Nothing        bundle              = print bundle-renderCgPgmBundle (Just dirName) (CgPgmBundle files) = do+renderCgPgmBundle Nothing        bundle                = print bundle+renderCgPgmBundle (Just dirName) (CgPgmBundle _ files) = do         b <- doesDirectoryExist dirName         unless b $ do putStrLn $ "Creating directory " ++ show dirName ++ ".."                       createDirectory dirName
Data/SBV/Examples/BitPrecise/BitTricks.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Checks the correctness of a few tricks from the large collection found in: --      <http://graphics.stanford.edu/~seander/bithacks.html>
Data/SBV/Examples/BitPrecise/Legato.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- An encoding and correctness proof of Legato's multiplier in Haskell. Bill Legato came -- up with an interesting way to multiply two 8-bit numbers on Mostek, as described here:
Data/SBV/Examples/BitPrecise/MergeSort.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Symbolic implementation of merge-sort and its correctness. -----------------------------------------------------------------------------
Data/SBV/Examples/BitPrecise/PrefixSum.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- The PrefixSum algorithm over power-lists and proof of -- the Ladner-Fischer implementation.@@ -145,39 +144,29 @@ genPrefixSumInstance :: Int -> Symbolic SBool genPrefixSumInstance n = do      args :: PowerList SWord32 <- mkForallVars n-     addAxiom "flOp is associative"     $ assocAxiom (sbvUFName opH)-     addAxiom "u is left-unit for flOp" $ leftUnitAxiom (sbvUFName opH) (sbvUFName uH)+     addAxiom "flOp is associative"     assocAxiom+     addAxiom "u is left-unit for flOp" leftUnitAxiom      return $ ps (u, op) args .== lf (u, op) args   where op :: SWord32 -> SWord32 -> SWord32-        opH :: SBVUF-        (opH, op) = uninterpretWithHandle "flOp"+        op = uninterpret "flOp"         u  :: SWord32-        uH :: SBVUF-        (uH, u)  = uninterpretWithHandle "u"-        -- this is the brittle part; but it'll have to do until we get a proper-        -- DSL for expressing SMT-axioms..-        mkCall :: String -> String -> String -> String-        mkCall o x y = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")"-        assocAxiom :: String -> [String]-        assocAxiom o = [+        u  = uninterpret "u"+        -- axioms.. These are a bit brittle. Note that we have to+        -- refer to the uninterpreted symbols with the prefix "uninterpreted_" when+        -- used with the SMTLib1 interface to avoid any collision. This is admittedly+        -- ugly, but it'll do till we get a sub-DSL for writing proper axioms (if ever)+        assocAxiom :: [String]+        assocAxiom = [              ":assumption (forall (?x BitVec[32]) (?y BitVec[32]) (?z BitVec[32])"-           , "                    (= " ++ lhs-           , "                       " ++ rhs+           , "                    (= (uninterpreted_flOp ?x (uninterpreted_flOp ?y ?z))"+           , "                       (uninterpreted_flOp (uninterpreted_flOp ?x ?y) ?z)"            , "                    )"            , "            )"           ]-          where lhs = mkCall o (mkCall o "?x" "?y") "?z"-                rhs = mkCall o "?x" (mkCall o "?y" "?z")-        leftUnitAxiom :: String -> String -> [String]-        leftUnitAxiom o ue = [-            ":assumption (forall (?x BitVec[32])"-          , "                    (= " ++ lhs-          , "                       " ++ rhs-          , "                    )"-          , "            )"+        leftUnitAxiom :: [String]+        leftUnitAxiom = [+            ":assumption (forall (?x BitVec[32]) (= (uninterpreted_flOp uninterpreted_u ?x) ?x))"           ]-          where lhs = "(" ++ o ++ " " ++ ue ++ " " ++ "?x" ++ ")"-                rhs = "?x"  -- | Prove the generic problem for powerlists of given sizes. Note that -- this will only work for Yices-1. This is due to the fact that Yices-2@@ -309,3 +298,5 @@ scanlTrace n = gen >>= print   where gen = runSymbolic True $ do args :: [SWord8] <- mkForallVars n                                     mapM_ output $ ps (0, (+)) args++{-# ANN module "HLint: ignore Reduce duplication" #-}
Data/SBV/Examples/CodeGeneration/AddSub.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Simple code generation example. -----------------------------------------------------------------------------
Data/SBV/Examples/CodeGeneration/CRC_USB5.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Computing the CRC symbolically, using the USB polynomial. We also -- generating C code for it as well. This example demonstrates the
Data/SBV/Examples/CodeGeneration/Fibonacci.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Computing Fibonacci numbers and generating C code. Inspired by Lee Pike's -- original implementation, modified for inclusion in the package. It illustrates
Data/SBV/Examples/CodeGeneration/GCD.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Computing GCD symbolically, and generating C code for it. This example -- illustrates symbolic termination related issues when programming with
Data/SBV/Examples/CodeGeneration/PopulationCount.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Computing population-counts (number of set bits) and autimatically -- generating C code.
Data/SBV/Examples/CodeGeneration/Uninterpreted.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Demonstrates the use of uninterpreted functions for the purposes of -- code generation. This facility is important when we want to take
Data/SBV/Examples/Crypto/AES.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- An implementation of AES (Advanced Encryption Standard), using SBV. -- For details on AES, see FIPS-197: <http://csrc.nist.gov/publications/fips/fips197/fips-197.pdf>.
Data/SBV/Examples/Crypto/RC4.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- An implementation of RC4 (AKA Rivest Cipher 4 or Alleged RC4/ARC4), -- using SBV. For information on RC4, see: <http://en.wikipedia.org/wiki/RC4>.
Data/SBV/Examples/Existentials/CRCPolynomial.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- This program demonstrates the use of the existentials and the QBVF (quantified -- bit-vector solver). We generate CRC polynomials of degree 16 that can be used
Data/SBV/Examples/Existentials/Diophantine.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Finding minimal natural number solutions to linear Diophantine equations, -- using explicit quantification.
Data/SBV/Examples/Polynomials/Polynomials.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Simple usage of polynomials over GF(2^n), using Rijndael's -- finite field: <http://en.wikipedia.org/wiki/Finite_field_arithmetic#Rijndael.27s_finite_field>
Data/SBV/Examples/Puzzles/Coins.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Solves the following puzzle: --
Data/SBV/Examples/Puzzles/Counts.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Consider the sentence: --
Data/SBV/Examples/Puzzles/DogCatMouse.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Puzzle: --   Spend exactly 100 dollars and buy exactly 100 animals.@@ -29,9 +28,10 @@ puzzle :: IO AllSatResult puzzle = allSat $ do            [dog, cat, mouse] <- sIntegers ["dog", "cat", "mouse"]-           solve [ dog   .>= 1                                   -- at least one dog-                 , cat   .>= 1                                   -- at least one cat-                 , mouse .>= 1                                   -- at least one mouse-                 , dog + cat + mouse .== 100                     -- buy precisely 100 animals-                 , 1500 * dog + 100 * cat + 25 * mouse .== 10000 -- spend exactly 100 dollars (use cents since we don't have fractions)+           solve [ dog   .>= 1                                           -- at least one dog+                 , cat   .>= 1                                           -- at least one cat+                 , mouse .>= 1                                           -- at least one mouse+                 , dog + cat + mouse .== 100                             -- buy precisely 100 animals+                 , 15 `per` dog + 1 `per` cat + 0.25 `per` mouse .== 100 -- spend exactly 100 dollars                  ]+  where p `per` q = p * toSReal q
Data/SBV/Examples/Puzzles/Euler185.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- A solution to Project Euler problem #185: <http://projecteuler.net/index.php?section=problems&id=185> -----------------------------------------------------------------------------
Data/SBV/Examples/Puzzles/MagicSquare.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Solves the magic-square puzzle. An NxN magic square is one where all entries -- are filled with numbers from 1 to NxN such that sums of all rows, columns
Data/SBV/Examples/Puzzles/NQueens.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Solves the NQueens puzzle: <http://en.wikipedia.org/wiki/Eight_queens_puzzle> -----------------------------------------------------------------------------
Data/SBV/Examples/Puzzles/Sudoku.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- The Sudoku solver, quintessential SMT solver example! -----------------------------------------------------------------------------
Data/SBV/Examples/Puzzles/U2Bridge.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- The famous U2 bridge crossing puzzle: <http://www.brainj.net/puzzle.php?id=u2> -----------------------------------------------------------------------------
Data/SBV/Examples/Uninterpreted/AUF.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Formalizes and proves the following theorem, about arithmetic, -- uninterpreted functions, and arrays. (For reference, see <http://research.microsoft.com/en-us/um/redmond/projects/z3/fmcad06-slides.pdf>
+ Data/SBV/Examples/Uninterpreted/Deduce.hs view
@@ -0,0 +1,95 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.Examples.Uninterpreted.Deduce+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+--+-- Demonstrates uninterpreted sorts and how they can be used for deduction.+-- This example is inspired by the discussion at <http://stackoverflow.com/questions/10635783/using-axioms-for-deductions-in-z3>,+-- essentially showing how to show the required deduction using SBV.+-----------------------------------------------------------------------------++{-# LANGUAGE DeriveDataTypeable #-}++module Data.SBV.Examples.Uninterpreted.Deduce where++import Data.Generics+import Data.SBV++-- we will have our own "uninterpreted" functions corresponding+-- to not/or/and, so hide their Prelude counterparts.+import Prelude hiding (not, or, and)++-----------------------------------------------------------------------------+-- * Representing uninterpreted booleans+-----------------------------------------------------------------------------++-- | The uninterpreted sort 'B', corresponding to the carrier.+data B = B deriving (Eq, Ord, Data, Typeable)+instance SymWord  B+instance HasKind  B++-- | Handy shortcut for the type of symbolic values over 'B'+type SB = SBV B++-----------------------------------------------------------------------------+-- * Uninterpreted connectives over 'B'+-----------------------------------------------------------------------------++-- | Uninterpreted logical connective 'and'+and :: SB -> SB -> SB+and = uninterpret "AND"++-- | Uninterpreted logical connective 'or'+or :: SB -> SB -> SB+or  = uninterpret "OR"++-- | Uninterpreted logical connective 'not'+not :: SB -> SB+not = uninterpret "NOT"++-----------------------------------------------------------------------------+-- * Axioms of the logical system+-----------------------------------------------------------------------------++-- | Distributivity of OR over AND, as an axiom in terms of+-- the uninterpreted functions we have introduced. Note how+-- variables range over the uninterpreted sort 'B'.+ax1 :: [String]+ax1 = [ "(assert (forall ((p B) (q B) (r B))"+      , "   (= (AND (OR p q) (OR p r))"+      , "      (OR p (AND q r)))))"+      ]++-- | One of De Morgan's laws, again as an axiom in terms+-- of our uninterpeted logical connectives.+ax2 :: [String]+ax2 = [ "(assert (forall ((p B) (q B))"+      , "   (= (NOT (OR p q))"+      , "      (AND (NOT p) (NOT q)))))"+      ]++-- | Double negation axiom, similar to the above.+ax3 :: [String]+ax3 = ["(assert (forall ((p B)) (= (NOT (NOT p)) p)))"]++-----------------------------------------------------------------------------+-- * Demonstrated deduction+-----------------------------------------------------------------------------++-- | Proves the equivalence @NOT (p OR (q AND r)) == (NOT p AND NOT q) OR (NOT p AND NOT r)@,+-- following from the axioms we have specified above. We have:+--+-- >>> test+-- Q.E.D.+test :: IO ThmResult+test = prove $ do addAxiom "OR distributes over AND" ax1+                  addAxiom "de Morgan"               ax2+                  addAxiom "double negation"         ax3+                  p <- free "p"+                  q <- free "q"+                  r <- free "r"+                  return $   not (p `or` (q `and` r))+                         .== (not p `and` not q) `or` (not p `and` not r)
Data/SBV/Examples/Uninterpreted/Function.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Demonstrates function counter-examples -----------------------------------------------------------------------------
+ Data/SBV/Examples/Uninterpreted/Sort.hs view
@@ -0,0 +1,55 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.Examples.Uninterpreted.Sort+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+--+-- Demonstrates uninterpreted sorts, together with axioms.+-----------------------------------------------------------------------------++{-# LANGUAGE DeriveDataTypeable #-}++module Data.SBV.Examples.Uninterpreted.Sort where++import Data.Generics+import Data.SBV++-- | A new data-type that we expect to use in an uninterpreted fashion+-- in the backend SMT solver. Note the custom @deriving@ clause, which+-- takes care of most of the boilerplate.+data Q = Q deriving (Eq, Ord, Data, Typeable)++-- | We need 'SymWord' and 'HasKind' instances, but default definitions+-- are always sufficient for uninterpreted sorts, so all we do is to+-- declare them as such. Note that, starting with GHC 7.6.1, we will+-- be able to simply derive these classes as well. (See <http://hackage.haskell.org/trac/ghc/ticket/5462>.)+instance SymWord Q+instance HasKind Q++-- | Declare an uninterpreted function that works over Q's+f :: SBV Q -> SBV Q+f = uninterpret "f"++-- | A satisfiable example, stating that there is an element of the domain+-- 'Q' such that 'f' returns a different element. Note that this is valid only+-- when the domain 'Q' has at least two elements. We have:+--+-- >>> t1+-- Satisfiable. Model:+--   x = Q!val!0 :: Q+t1 :: IO SatResult+t1 = sat $ do x <- free "x"+              return $ f x ./= x++-- | This is a variant on the first example, except we also add an axiom+-- for the sort, stating that the domain 'Q' has only one element. In this case+-- the problem naturally becomes unsat. We have:+--+-- >>> t2+-- Unsatisfiable+t2 :: IO SatResult+t2 = sat $ do x <- free "x"+              addAxiom "Q" ["(assert (forall ((x Q) (y Q)) (= x y)))"]+              return $ f x ./= x
Data/SBV/Internals.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Low level functions to access the SBV infrastructure, for developers who -- want to build further tools on top of SBV. End-users of the library@@ -16,12 +15,12 @@   -- * Running symbolic programs /manually/   Result, SBVRunMode(..), runSymbolic, runSymbolic'   -- * Other internal structures useful for low-level programming-  , SBV(..), HasKind(..), CW, mkConstCW, genVar, genVar_+  , SBV(..), slet, CW, mkConstCW, genVar, genVar_   -- * Compilation to C   , compileToC', compileToCLib', CgPgmBundle(..), CgPgmKind(..)   ) where -import Data.SBV.BitVectors.Data   (Result, SBVRunMode(..), runSymbolic, runSymbolic', SBV(..), HasKind(..), CW, mkConstCW)-import Data.SBV.BitVectors.Model  (genVar, genVar_)+import Data.SBV.BitVectors.Data   (Result, SBVRunMode(..), runSymbolic, runSymbolic', SBV(..), CW, mkConstCW)+import Data.SBV.BitVectors.Model  (genVar, genVar_, slet) import Data.SBV.Compilers.C       (compileToC', compileToCLib') import Data.SBV.Compilers.CodeGen (CgPgmBundle(..), CgPgmKind(..))
Data/SBV/Provers/Prover.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Provable abstraction and the connection to SMT solvers -----------------------------------------------------------------------------@@ -38,7 +37,7 @@  import Control.Concurrent             (forkIO) import Control.Concurrent.Chan.Strict (newChan, writeChan, getChanContents)-import Control.Monad                  (when)+import Control.Monad                  (when, unless) import Data.List                      (intercalate) import Data.Maybe                     (fromJust, isJust, catMaybes) import System.FilePath                (addExtension)@@ -324,7 +323,7 @@         t <- getClockTime         let comments = ["Created on " ++ show t]             cvt = if smtLib2 then toSMTLib2 else toSMTLib1-        (_, _, _, smtLibPgm) <- simulate cvt defaultSMTCfg False comments a+        (_, _, _, _, smtLibPgm) <- simulate cvt defaultSMTCfg False comments a         let out = show smtLibPgm         if smtLib2 -- append check-sat in case of smtLib2            then return $ out ++ "\n(check-sat)\n"@@ -354,11 +353,11 @@ -- | Determine if the constraints are vacuous using the given SMT-solver isVacuousWith :: Provable a => SMTConfig -> a -> IO Bool isVacuousWith config a = do-        Result ub tr uic is cs ts as uis ax asgn cstr _ <- runSymbolic True $ forAll_ a >>= output+        Result ub us tr uic is cs ts as uis ax asgn cstr _ <- runSymbolic True $ forAll_ a >>= output         case cstr of            [] -> return False -- no constraints, no need to check            _  -> do let is'  = [(EX, i) | (_, i) <- is] -- map all quantifiers to "exists" for the constraint check-                        res' = Result ub tr uic is' cs ts as uis ax asgn cstr [trueSW]+                        res' = Result ub us tr uic is' cs ts as uis ax asgn cstr [trueSW]                         cvt  = if useSMTLib2 config then toSMTLib2 else toSMTLib1                     SatResult result <- runProofOn cvt config True [] res' >>= callSolver True "Checking Satisfiability.." SatResult config                     case result of@@ -373,7 +372,9 @@ allSatWith config p = do         let converter = if useSMTLib2 config then toSMTLib2 else toSMTLib1         msg "Checking Satisfiability, all solutions.."-        sbvPgm@(qinps, _, _, _) <- simulate converter config True [] p+        sbvPgm@(qinps, _, _, usorts, _) <- simulate converter config True [] p+        unless (null usorts) $ error $  "SBV.allSat: All-sat calls are not supported in the presence of uninterpreted sorts: " ++ unwords usorts+                                     ++ "\n    Only 'sat' and 'prove' calls are available when uninterpreted sorts are used."         resChan <- newChan         let add  = writeChan resChan . Just             stop = writeChan resChan Nothing@@ -402,7 +403,7 @@                                             Unsatisfiable _                 -> stop                                             Satisfiable _ model             -> add r >> loop (n+1) (modelAssocs model : nonEqConsts)                                             Unknown     _ model             -> add r >> loop (n+1) (modelAssocs model : nonEqConsts)-        invoke nonEqConsts n (qinps, modelMap, skolemMap, smtLibPgm) = do+        invoke nonEqConsts n (qinps, modelMap, skolemMap, _, smtLibPgm) = do                msg $ "Looking for solution " ++ show n                case addNonEqConstraints qinps nonEqConsts smtLibPgm of                  Nothing ->  -- no new constraints added, stop@@ -412,8 +413,15 @@                                      msg "Done.."                                      return $ Just $ SatResult smtAnswer -callSolver :: Bool -> String -> (SMTResult -> b) -> SMTConfig -> ([(Quantifier, NamedSymVar)], [(String, UnintKind)], [Either SW (SW, [SW])], SMTLibPgm) -> IO b-callSolver isSat checkMsg wrap config (qinps, modelMap, skolemMap, smtLibPgm) = do+type SMTProblem = ( [(Quantifier, NamedSymVar)]         -- inputs+                  , [(String, UnintKind)]               -- model-map+                  , [Either SW (SW, [SW])]              -- skolem-map+                  , [String]                            -- uninterpreted sorts+                  , SMTLibPgm                           -- SMTLib representation+                  )++callSolver :: Bool -> String -> (SMTResult -> b) -> SMTConfig -> SMTProblem -> IO b+callSolver isSat checkMsg wrap config (qinps, modelMap, skolemMap, _, smtLibPgm) = do        let msg = when (verbose config) . putStrLn . ("** " ++)        msg checkMsg        let finalPgm = intercalate "\n" (pre ++ post) where SMTLibPgm _ (_, pre, post) = smtLibPgm@@ -422,7 +430,7 @@        msg "Done.."        return $ wrap smtAnswer -simulate :: Provable a => SMTLibConverter -> SMTConfig -> Bool -> [String] -> a -> IO ([(Quantifier, NamedSymVar)], [(String, UnintKind)], [Either SW (SW, [SW])], SMTLibPgm)+simulate :: Provable a => SMTLibConverter -> SMTConfig -> Bool -> [String] -> a -> IO SMTProblem simulate converter config isSat comments predicate = do         let msg = when (verbose config) . putStrLn . ("** " ++)             isTiming = timing config@@ -432,11 +440,11 @@         msg "Translating to SMT-Lib.."         runProofOn converter config isSat comments res -runProofOn :: SMTLibConverter -> SMTConfig -> Bool -> [String] -> Result -> IO ([(Quantifier, NamedSymVar)], [(String, UnintKind)], [Either SW (SW, [SW])], SMTLibPgm)+runProofOn :: SMTLibConverter -> SMTConfig -> Bool -> [String] -> Result -> IO SMTProblem runProofOn converter config isSat comments res =         let isTiming = timing config         in case res of-             Result hasInfPrec _qcInfo _codeSegs is consts tbls arrs uis axs pgm cstrs [o@(SW (KBounded False 1) _)] ->+             Result boundInfo usorts _qcInfo _codeSegs is consts tbls arrs uis axs pgm cstrs [o@(SW (KBounded False 1) _)] ->                timeIf isTiming "translation" $ let uiMap     = catMaybes (map arrayUIKind arrs) ++ map unintFnUIKind uis                                                    skolemMap = skolemize (if isSat then is else map flipQ is)                                                         where flipQ (ALL, x) = (EX, x)@@ -446,8 +454,8 @@                                                                 where go []                   (_,  sofar) = reverse sofar                                                                       go ((ALL, (v, _)):rest) (us, sofar) = go rest (v:us, Left v : sofar)                                                                       go ((EX,  (v, _)):rest) (us, sofar) = go rest (us,   Right (v, reverse us) : sofar)-                                               in return (is, uiMap, skolemMap, converter hasInfPrec isSat comments is skolemMap consts tbls arrs uis axs pgm cstrs o)-             Result _hasInfPrec _qcInfo _codeSegs _is _consts _tbls _arrs _uis _axs _pgm _cstrs os -> case length os of+                                               in return (is, uiMap, skolemMap, usorts, converter boundInfo isSat comments usorts is skolemMap consts tbls arrs uis axs pgm cstrs o)+             Result _boundInfo _us _qcInfo _codeSegs _is _consts _tbls _arrs _uis _axs _pgm _cstrs os -> case length os of                            0  -> error $ "Impossible happened, unexpected non-outputting result\n" ++ show res                            1  -> error $ "Impossible happened, non-boolean output in " ++ show os                                        ++ "\nDetected while generating the trace:\n" ++ show res
Data/SBV/Provers/SExpr.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Parsing of S-expressions (mainly used for parsing SMT-Lib get-value output) -----------------------------------------------------------------------------
Data/SBV/Provers/Yices.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- The connection to the Yices SMT solver -----------------------------------------------------------------------------
Data/SBV/Provers/Z3.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- The connection to the Z3 SMT solver -----------------------------------------------------------------------------@@ -66,6 +65,7 @@        zero (KBounded _     sz) = "#x" ++ replicate (sz `div` 4) '0'        zero KUnbounded          = "0"        zero KReal               = "0.0"+       zero (KUninterpreted s)  = error $ "SBV.Z3.zero: Unexpected uninterpreted sort: " ++ s        cont skolemMap = intercalate "\n" $ concatMap extract skolemMap         where extract (Left s)        = ["(echo \"((" ++ show s ++ " " ++ zero (kindOf s) ++ "))\")"]               extract (Right (s, [])) = let g = "(get-value (" ++ show s ++ "))" in getVal (kindOf s) g@@ -103,7 +103,7 @@           where squash [(i, (n, cw1)), (_, (_, cw2))] = [(i, (n, mergeReals n cw1 cw2))]                 squash xs = xs                 mergeReals :: String -> CW -> CW -> CW-                mergeReals n (CW KReal (Left a)) (CW KReal (Left b)) = CW KReal (Left (mergeAlgReals (error (bad n a b)) a b))+                mergeReals n (CW KReal (CWAlgReal a)) (CW KReal (CWAlgReal b)) = CW KReal (CWAlgReal (mergeAlgReals (error (bad n a b)) a b))                 mergeReals n a b = error $ bad n a b                 bad n a b = "SBV.Z3: Cannot merge reals for variable: " ++ n ++ " received: " ++ show (a, b) @@ -122,6 +122,7 @@                                                   ++ 's':v ++ " in "  ++ show matches         isInput _       = Nothing         extract (SApp [SApp [SCon v, SNum i]])  | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (kindOf s) i))]-        extract (SApp [SApp [SCon v, SReal i]]) | Just (n, _, nm) <- isInput v = [(n, (nm, CW KReal (Left i)))]-        extract (SApp [SApp (SCon v : r)])      | Just{}          <- isInput v = error $ "SBV.SMTLib2: Cannot extract value for " ++ show ('s':v) ++ ", received:\n\t" ++  show r+        extract (SApp [SApp [SCon v, SReal i]]) | Just (n, _, nm) <- isInput v = [(n, (nm, CW KReal      (CWAlgReal i)))]+        extract (SApp [SApp [SCon v, SCon i]])  | Just (n, s, nm) <- isInput v = [(n, (nm, CW (kindOf s) (CWUninterpreted i)))]+        extract (SApp [SApp (SCon v : r)])      | Just{}          <- isInput v = error $ "SBV.SMTLib2: Cannot extract value for " ++ show v ++ ", received:\n\t" ++  show r         extract _                                                              = []
Data/SBV/SMT/SMT.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Abstraction of SMT solvers -----------------------------------------------------------------------------@@ -172,8 +171,8 @@  -- | Parse a signed/sized value from a sequence of CWs genParse :: Integral a => Kind -> [CW] -> Maybe (a, [CW])-genParse k (x@(CW _ (Right i)):r) | kindOf x == k = Just (fromIntegral i, r)-genParse _ _                                      = Nothing+genParse k (x@(CW _ (CWInteger i)):r) | kindOf x == k = Just (fromIntegral i, r)+genParse _ _                                          = Nothing  -- | Base case, that comes in handy if there are no real variables instance SatModel () where@@ -211,8 +210,8 @@   parseCWs = genParse KUnbounded  instance SatModel AlgReal where-  parseCWs (CW KReal (Left i) : r) = Just (i, r)-  parseCWs _                       = Nothing+  parseCWs (CW KReal (CWAlgReal i) : r) = Just (i, r)+  parseCWs _                            = Nothing  -- when reading a list; go as long as we can (maximal-munch) -- note that this never fails..@@ -398,7 +397,7 @@     msg $ nmSolver ++ " output:\n" ++ either id (intercalate "\n") contents     case contents of       Left e   -> return $ failure (lines e)-      Right xs -> return $ success xs+      Right xs -> return $ success (mergeSExpr xs)  -- | A variant of 'readProcessWithExitCode'; except it knows about continuation strings -- and can speak SMT-Lib2 (just a little).@@ -437,3 +436,23 @@                        mapM_ putStrLn mls         mapM_ send mls       cleanUp r++-- | In case the SMT-Lib solver returns a response over multiple lines, compress them so we have+-- each S-Expression spanning only a single line. We'll ignore things line parentheses inside quotes+-- etc., as it should not be an issue+mergeSExpr :: [String] -> [String]+mergeSExpr []       = []+mergeSExpr (x:xs)+ | d == 0 = x : mergeSExpr xs+ | True   = let (f, r) = grab d xs in unwords (x:f) : mergeSExpr r+ where d = parenDiff x+       parenDiff :: String -> Int+       parenDiff = go 0+         where go i ""       = i+               go i ('(':cs) = let i'= i+1 in i' `seq` go i' cs+               go i (')':cs) = let i'= i-1 in i' `seq` go i' cs+               go i (_  :cs) = go i cs+       grab i ls+         | i <= 0    = ([], ls)+       grab _ []     = ([], [])+       grab i (l:ls) = let (a, b) = grab (i+parenDiff l) ls in (l:a, b)
Data/SBV/SMT/SMTLib.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Conversion of symbolic programs to SMTLib format -----------------------------------------------------------------------------@@ -19,9 +18,10 @@  -- | An instance of SMT-Lib converter; instantiated for SMT-Lib v1 and v2. (And potentially for -- newer versions in the future.)-type SMTLibConverter =  Bool                        -- ^ has infinite precision values+type SMTLibConverter =  (Bool, Bool)                -- ^ has unbounded integers/reals                      -> Bool                        -- ^ is this a sat problem?                      -> [String]                    -- ^ extra comments to place on top+                     -> [String]                    -- ^ uninterpreted sorts                      -> [(Quantifier, NamedSymVar)] -- ^ inputs and aliasing names                      -> [Either SW (SW, [SW])]      -- ^ skolemized inputs                      -> [(SW, CW)]                  -- ^ constants@@ -40,10 +40,10 @@ -- | Convert to SMTLib-2 format toSMTLib2 :: SMTLibConverter (toSMTLib1, toSMTLib2) = (cvt SMTLib1, cvt SMTLib2)-  where cvt v hasInfPrec isSat comments qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out = SMTLibPgm v (aliasTable, pre, post)+  where cvt v boundedInfo isSat comments sorts qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out = SMTLibPgm v (aliasTable, pre, post)          where aliasTable  = map (\(_, (x, y)) -> (y, x)) qinps                converter   = if v == SMTLib1 then SMT1.cvt else SMT2.cvt-               (pre, post) = converter hasInfPrec isSat comments qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out+               (pre, post) = converter boundedInfo isSat comments sorts qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out  -- | Add constraints generated from older models, used for querying new models addNonEqConstraints :: [(Quantifier, NamedSymVar)] -> [[(String, CW)]] -> SMTLibPgm -> Maybe String
Data/SBV/SMT/SMTLib1.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Conversion of symbolic programs to SMTLib format, Using v1 of the standard -----------------------------------------------------------------------------@@ -41,9 +40,10 @@ nonEq (s, c) = "(not (= " ++ s ++ " " ++ cvtCW c ++ "))"  -- | Translate a problem into an SMTLib1 script-cvt :: Bool                         -- ^ has infinite precision values+cvt :: (Bool, Bool)                 -- ^ has infinite precision integers/reals     -> Bool                         -- ^ is this a sat problem?     -> [String]                     -- ^ extra comments to place on top+    -> [String]                     -- ^ uninterpreted sorts     -> [(Quantifier, NamedSymVar)]  -- ^ inputs     -> [Either SW (SW, [SW])]       -- ^ skolemized version of the inputs     -> [(SW, CW)]                   -- ^ constants@@ -55,11 +55,15 @@     -> [SW]                         -- ^ extra constraints     -> SW                           -- ^ output variable     -> ([String], [String])-cvt hasInf isSat comments qinps _skolemInps consts tbls arrs uis axs asgnsSeq cstrs out-  | hasInf-  = error "SBV: The chosen solver does not support infinite precision values. (Use z3 instead.)"+cvt (hasIntegers, hasReals) isSat comments sorts qinps _skolemInps consts tbls arrs uis axs asgnsSeq cstrs out+  | hasIntegers+  = error "SBV: Unbounded integers are not supported in the SMTLib1/yices interface. (Use z3 instead.)"+  | hasReals+  = error "SBV: The real value domain is not supported in the SMTLib1/yices interface. (Use z3 instead.)"   | not ((isSat && allExistential) || (not isSat && allUniversal))   = error "SBV: The chosen solver does not support quantified variables. (Use z3 instead.)"+  | not (null sorts)+  = error "SBV: The chosen solver does not support unintepreted sorts. (Use z3 instead.)"   | True   = (pre, post)   where quantifiers    = map fst qinps@@ -157,13 +161,13 @@  -- no need to worry about Int/Real here as we don't support them with the SMTLib1 interface.. cvtCW :: CW -> String-cvtCW x@(CW _ (Right v)) | not (hasSign x) = "bv" ++ show v ++ "[" ++ show (intSizeOf x) ++ "]"+cvtCW x@(CW _ (CWInteger v)) | not (hasSign x) = "bv" ++ show v ++ "[" ++ show (intSizeOf x) ++ "]" -- signed numbers (with 2's complement representation) is problematic -- since there's no way to put a bvneg over a positive number to get minBound.. -- Hence, we punt and use binary notation in that particular case-cvtCW x@(CW _ (Right v))  | v == least = mkMinBound (intSizeOf x)+cvtCW x@(CW _ (CWInteger v))  | v == least = mkMinBound (intSizeOf x)   where least = negate (2 ^ intSizeOf x)-cvtCW x@(CW _ (Right v)) = negIf (v < 0) $ "bv" ++ show (abs v) ++ "[" ++ show (intSizeOf x) ++ "]"+cvtCW x@(CW _ (CWInteger v)) = negIf (v < 0) $ "bv" ++ show (abs v) ++ "[" ++ show (intSizeOf x) ++ "]" cvtCW x = error $ "SBV.SMTLib1.cvtCW: Unexpected CW: " ++ show x -- unbounded/real, shouldn't reach here  negIf :: Bool -> String -> String@@ -248,6 +252,7 @@ cvtType :: SBVType -> String cvtType (SBVType []) = error "SBV.SMT.SMTLib1.cvtType: internal: received an empty type!" cvtType (SBVType xs) = unwords $ map sh xs-  where sh (KBounded _ s) = "BitVec[" ++ show s ++ "]"-        sh KUnbounded     = die "unbounded Integer"-        sh KReal          = die "real value"+  where sh (KBounded _ s)     = "BitVec[" ++ show s ++ "]"+        sh KUnbounded         = die "unbounded Integer"+        sh KReal              = die "real value"+        sh (KUninterpreted s) = die $ "uninterpreted sort: " ++ s
Data/SBV/SMT/SMTLib2.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Conversion of symbolic programs to SMTLib format, Using v2 of the standard -----------------------------------------------------------------------------@@ -58,9 +57,10 @@ tbd e = error $ "SBV.SMTLib2: Not-yet-supported: " ++ e  -- | Translate a problem into an SMTLib2 script-cvt :: Bool                         -- ^ has infinite precision values+cvt :: (Bool, Bool)                 -- ^ has infinite precision values     -> Bool                         -- ^ is this a sat problem?     -> [String]                     -- ^ extra comments to place on top+    -> [String]                     -- ^ uninterpreted sorts     -> [(Quantifier, NamedSymVar)]  -- ^ inputs     -> [Either SW (SW, [SW])]       -- ^ skolemized version inputs     -> [(SW, CW)]                   -- ^ constants@@ -72,11 +72,13 @@     -> [SW]                         -- ^ extra constraints     -> SW                           -- ^ output variable     -> ([String], [String])-cvt hasInf isSat comments _inps skolemInps consts tbls arrs uis axs asgnsSeq cstrs out = (pre, [])+cvt (hasInteger, hasReal) isSat comments sorts _inps skolemInps consts tbls arrs uis axs asgnsSeq cstrs out = (pre, [])   where -- the logic is an over-approaximation         logic-          | hasInf = ["; Has unbounded values (Int/Real); no logic specified."]   -- combination, let the solver pick-          | True   = ["(set-logic " ++ qs ++ as ++ ufs ++ "BV)"]+           | hasInteger || hasReal || not (null sorts)+           = ["; Has unbounded values (Int/Real) or sorts; no logic specified."]   -- combination, let the solver pick+           | True+           = ["(set-logic " ++ qs ++ as ++ ufs ++ "BV)"]           where qs  | null foralls && null axs = "QF_"  -- axioms are likely to contain quantifiers                     | True                     = ""                 as  | null arrs                = ""@@ -87,9 +89,11 @@              ++ map ("; " ++) comments              ++ [ "(set-option :produce-models true)"                 , "(set-option :pp-decimal false)"-                , "; --- literal constants ---"                 ]              ++ logic+             ++ [ "; --- uninterpreted sorts ---" ]+             ++ map declSort sorts+             ++ [ "; --- literal constants ---" ]              ++ map declConst consts              ++ [ "; --- skolem constants ---" ]              ++ [ "(declare-fun " ++ show s ++ " " ++ swFunType ss s ++ ")" | Right (s, ss) <- skolemInps]@@ -140,13 +144,14 @@         asgns = F.toList asgnsSeq         mkLet (s, e) = "(let ((" ++ show s ++ " " ++ cvtExp skolemMap tableMap e ++ "))"         declConst (s, c) = "(define-fun " ++ show s ++ " " ++ swFunType [] s ++ " " ++ cvtCW c ++ ")"+        declSort s = "(declare-sort " ++ s ++ ")"  declUI :: (String, SBVType) -> [String]-declUI (i, t) = ["(declare-fun uninterpreted_" ++ i ++ " " ++ cvtType t ++ ")"]+declUI (i, t) = ["(declare-fun " ++ i ++ " " ++ cvtType t ++ ")"]  -- NB. We perform no check to as to whether the axiom is meaningful in any way. declAx :: (String, [String]) -> String-declAx (nm, ls) = (";; -- user given axiom: " ++ nm ++ "\n   ") ++ intercalate "\n" ls+declAx (nm, ls) = (";; -- user given axiom: " ++ nm ++ "\n") ++ intercalate "\n" ls  constTable :: (((Int, Kind, Kind), [SW]), [String]) -> [String] constTable (((i, ak, rk), _elts), is) = decl : map wrap is@@ -214,9 +219,10 @@ swFunType ss s = "(" ++ unwords (map swType ss) ++ ") " ++ swType s  smtType :: Kind -> String-smtType (KBounded _ sz) = "(_ BitVec " ++ show sz ++ ")"-smtType KUnbounded      = "Int"-smtType KReal           = "Real"+smtType (KBounded _ sz)    = "(_ BitVec " ++ show sz ++ ")"+smtType KUnbounded         = "Int"+smtType KReal              = "Real"+smtType (KUninterpreted s) = s  cvtType :: SBVType -> String cvtType (SBVType []) = error "SBV.SMT.SMTLib2.cvtType: internal: received an empty type!"@@ -240,19 +246,21 @@   where pad n s = replicate (n - length s) '0' ++ s  cvtCW :: CW -> String+cvtCW x | isUninterpreted x = s+  where CWUninterpreted s = cwVal x cvtCW x | isReal x = algRealToSMTLib2 w-  where Left w = cwVal x+  where CWAlgReal w = cwVal x cvtCW x | not (isBounded x) = if w >= 0 then show w else "(- " ++ show (abs w) ++ ")"-  where Right w = cwVal x+  where CWInteger w = cwVal x cvtCW x | not (hasSign x) = hex (intSizeOf x) w-  where Right w = cwVal x+  where CWInteger w = cwVal x -- signed numbers (with 2's complement representation) is problematic -- since there's no way to put a bvneg over a positive number to get minBound.. -- Hence, we punt and use binary notation in that particular case-cvtCW x | cwVal x == Right least = mkMinBound (intSizeOf x)+cvtCW x | cwVal x == CWInteger least = mkMinBound (intSizeOf x)   where least = negate (2 ^ intSizeOf x) cvtCW x = negIf (w < 0) $ hex (intSizeOf x) (abs w)-  where Right w = cwVal x+  where CWInteger w = cwVal x  negIf :: Bool -> String -> String negIf True  a = "(bvneg " ++ a ++ ")"@@ -289,24 +297,29 @@           | needsCheck = "(ite " ++ cond ++ ssw e ++ " " ++ lkUp ++ ")"           | True       = lkUp           where needsCheck = case aKnd of-                              KBounded _ n -> (2::Integer)^n > fromIntegral l-                              KUnbounded   -> True-                              KReal        -> error "SBV.SMT.SMTLib2.cvtExp: unexpected real valued index"+                              KBounded _ n     -> (2::Integer)^n > fromIntegral l+                              KUnbounded       -> True+                              KReal            -> error "SBV.SMT.SMTLib2.cvtExp: unexpected real valued index"+                              KUninterpreted s -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected uninterpreted valued index: " ++ s                 lkUp = "(" ++ getTable tableMap t ++ " " ++ ssw i ++ ")"                 cond                  | hasSign i = "(or " ++ le0 ++ " " ++ gtl ++ ") "                  | True      = gtl ++ " "                 (less, leq) = case aKnd of-                                KBounded{} -> if hasSign i then ("bvslt", "bvsle") else ("bvult", "bvule")-                                KUnbounded -> ("<", "<=")-                                KReal      -> ("<", "<=")+                                KBounded{}       -> if hasSign i then ("bvslt", "bvsle") else ("bvult", "bvule")+                                KUnbounded       -> ("<", "<=")+                                KReal            -> ("<", "<=")+                                KUninterpreted s -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected uninterpreted valued index: " ++ s                 mkCnst = cvtCW . mkConstCW (kindOf i)                 le0  = "(" ++ less ++ " " ++ ssw i ++ " " ++ mkCnst 0 ++ ")"                 gtl  = "(" ++ leq  ++ " " ++ mkCnst l ++ " " ++ ssw i ++ ")"         sh (SBVApp (ArrEq i j) []) = "(ite (= array_" ++ show i ++ " array_" ++ show j ++") #b1 #b0)"         sh (SBVApp (ArrRead i) [a]) = "(select array_" ++ show i ++ " " ++ ssw a ++ ")"-        sh (SBVApp (Uninterpreted nm) [])   = "uninterpreted_" ++ nm-        sh (SBVApp (Uninterpreted nm) args) = "(uninterpreted_" ++ nm ++ " " ++ unwords (map ssw args) ++ ")"+        sh (SBVApp (Uninterpreted nm) [])   = nm+        sh (SBVApp (Uninterpreted nm) args) = "(" ++ nm ++ " " ++ unwords (map ssw args) ++ ")"+        sh (SBVApp (Extract 0 0) [a])   -- special SInteger -> SReal conversion+          | kindOf a == KUnbounded+          = "(to_real " ++ ssw a ++ ")"         sh (SBVApp (Extract i j) [a]) | ensureBV = "((_ extract " ++ show i ++ " " ++ show j ++ ") " ++ ssw a ++ ")"         sh (SBVApp (Rol i) [a])            | bvOp  = rot  ssw "rotate_left"  i a@@ -345,6 +358,8 @@           = f (any hasSign args) (map ssw args)           | realOp, Just f <- lookup op smtOpRealTable           = f (any hasSign args) (map ssw args)+          | Just f <- lookup op uninterpretedTable+          = f (map ssw args)           | True           = error $ "SBV.SMT.SMTLib2.cvtExp.sh: impossible happened; can't translate: " ++ show inp           where smtOpBVTable  = [ (Plus,          lift2   "bvadd")@@ -376,6 +391,10 @@                                     , (LessEq,        lift2B  "<=" "<=")                                     , (GreaterEq,     lift2B  ">=" ">=")                                     ]+                -- equality is the only thing that works on uninterpreted sorts+                uninterpretedTable = [ (Equal,    lift2B "="        "="        True)+                                     , (NotEqual, lift2B "distinct" "distinct" True)+                                     ]  rot :: (SW -> String) -> String -> Int -> SW -> String rot ssw o c x = "((_ " ++ o ++ " " ++ show c ++ ") " ++ ssw x ++ ")"
Data/SBV/Tools/ExpectedValue.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Computing the expected value of a symbolic variable -----------------------------------------------------------------------------@@ -39,15 +38,15 @@                         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)+        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 (cwKind cw, cwVal cw) of-                                                   (KBounded False 1, _) -> if cwToBool cw then 1 else 0-                                                   (KBounded{}, Right v) -> v-                                                   (KUnbounded, Right v) -> v-                                                   (KReal, _)            -> error "Cannot compute expected-values for real valued results."-                                                   _                     -> error $ "SBV.expectedValueWith: Unexpected CW: " ++ show cw+                                                   (KBounded False 1, _)     -> if cwToBool cw then 1 else 0+                                                   (KBounded{}, CWInteger v) -> v+                                                   (KUnbounded, CWInteger v) -> v+                                                   (KReal, _)                -> error "Cannot compute expected-values for real valued results."+                                                   _                         -> error $ "SBV.expectedValueWith: Unexpected CW: " ++ show cw                        if all ((== 1) . cval) cstrs                           then return $ map cval os                           else runOnce g -- constraint not satisfied try again with the same set of constraints
Data/SBV/Tools/GenTest.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test generation from symbolic programs -----------------------------------------------------------------------------@@ -43,7 +42,7 @@          | 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)+        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@@ -123,12 +122,14 @@                  KBounded True  64 -> "Int64"                  KUnbounded        -> "Integer"                  KReal             -> error $ "SBV.renderTest: Unsupported real valued test value: " ++ show cw+                 KUninterpreted us -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us                  _                 -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw         s cw = case cwKind cw of                   KBounded False 1  -> take 5 (show (cwToBool cw) ++ repeat ' ')-                  KBounded sgn   sz -> let Right w = cwVal cw in shex  False True (sgn, sz) w-                  KUnbounded        -> let Right w = cwVal cw in shexI False True           w-                  KReal             -> let Left w  = cwVal cw in algRealToHaskell w+                  KBounded sgn   sz -> let CWInteger w = cwVal cw in shex  False True (sgn, sz) w+                  KUnbounded        -> let CWInteger w = cwVal cw in shexI False True           w+                  KReal             -> let CWAlgReal w = cwVal cw in algRealToHaskell w+                  KUninterpreted us -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us  c :: String -> [([CW], [CW])] -> String c n vs = intercalate "\n" $@@ -197,13 +198,15 @@                         KBounded True  64 -> "SInt64"                         KUnbounded        -> error "SBV.renderTest: Unbounded integers are not supported when generating C test-cases."                         KReal             -> error "SBV.renderTest: Real values are not supported when generating C test-cases."+                        KUninterpreted us -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us                         _                 -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw         mkLine (is, os) = "{{" ++ intercalate ", " (map v is) ++ "}, {" ++ intercalate ", " (map v os) ++ "}}"         v cw = case cwKind cw of-                  KBounded False 1 -> if cwToBool cw then "true " else "false"-                  KBounded sgn sz  -> let Right w = cwVal cw in shex  False True (sgn, sz) w-                  KUnbounded       -> let Right w = cwVal cw in shexI False True           w-                  KReal            -> error "SBV.renderTest: Real values are not supported when generating C test-cases."+                  KBounded False 1  -> if cwToBool cw then "true " else "false"+                  KBounded sgn sz   -> let CWInteger w = cwVal cw in shex  False True (sgn, sz) w+                  KUnbounded        -> let CWInteger w = cwVal cw in shexI False True           w+                  KUninterpreted us -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us+                  KReal             -> error "SBV.renderTest: Real values are not supported when generating C test-cases."         outLine           | null vs = "printf(\"\");"           | True    = "printf(\"%*d. " ++ fmtString ++ "\\n\", " ++ show (length (show (length vs - 1))) ++ ", i"@@ -259,8 +262,9 @@                      KReal             -> error "SBV.renderTest: Real values are not supported when generating Forte test-cases."                      KUnbounded        -> error "SBV.renderTest: Unbounded integers are not supported when generating Forte test-cases."                      _                 -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw-        xlt s (Right v) = [toF (testBit v i) | i <- [s-1, s-2 .. 0]]-        xlt _ (Left r)  = error $ "SBV.renderTest.Forte: Unexpected real value: " ++ show r+        xlt s (CWInteger v)        = [toF (testBit v i) | i <- [s-1, s-2 .. 0]]+        xlt _ (CWAlgReal r)        = error $ "SBV.renderTest.Forte: Unexpected real value: " ++ show r+        xlt _ (CWUninterpreted r)  = error $ "SBV.renderTest.Forte: Unexpected uninterpreted value: " ++ show r         mkLine  (i, o) = "("  ++ mkTuple (form (fst ss) (concatMap blast i)) ++ ", " ++ mkTuple (form (snd ss) (concatMap blast o)) ++ ")"         mkTuple []  = "()"         mkTuple [x] = x
Data/SBV/Tools/Optimize.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- SMT based optimization -----------------------------------------------------------------------------
Data/SBV/Tools/Polynomial.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Implementation of polynomial arithmetic -----------------------------------------------------------------------------
Data/SBV/Utils/Boolean.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Abstraction of booleans. Unfortunately, Haskell makes Bool's very hard to -- work with, by making it a fixed-data type. This is our workaround
Data/SBV/Utils/Lib.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Misc helpers -----------------------------------------------------------------------------
Data/SBV/Utils/TDiff.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Runs an IO computation printing the time it took to run it -----------------------------------------------------------------------------
README view
@@ -1,5 +1,5 @@-SBV: SMT Based Verification-============================+SBV: SMT Based Verification in Haskell+======================================  Express properties about Haskell programs and automatically prove them using SMT solvers. @@ -39,15 +39,15 @@ The Haskell sbv library provides support for dealing with Symbolic Bit Vectors in Haskell. It introduces the types: -  - `SBool`: Symbolic Booleans (bits)-  - `SWord8`, `SWord16`, `SWord32`, `SWord64`: Symbolic Words (unsigned)-  - `SInt8`,  `SInt16`,  `SInt32`,  `SInt64`: Symbolic Ints (signed)-  - `SInteger`: Symbolic unbounded integers (signed)-  - `SReal`: Symbolic infinite precision algebraic reals (signed)-  - Arrays of symbolic values-  - Symbolic polynomials over GF(2^n ), polynomial arithmetic, and CRCs-  - Uninterpreted constants and functions over symbolic values, with user-    defined SMT-Lib axioms+  - `SBool`: Symbolic Booleans (bits).+  - `SWord8`, `SWord16`, `SWord32`, `SWord64`: Symbolic Words (unsigned).+  - `SInt8`,  `SInt16`,  `SInt32`,  `SInt64`: Symbolic Ints (signed).+  - `SInteger`: Symbolic unbounded integers (signed).+  - `SReal`: Symbolic infinite precision algebraic reals (signed).+  - Arrays of symbolic values.+  - Symbolic polynomials over GF(2^n ), polynomial arithmetic, and CRCs.+  - Uninterpreted constants and functions over symbolic values, with user defined axioms.+  - Uninterpreted sorts, and proofs over such sorts, potentially with axioms.  The user can construct ordinary Haskell programs using these types, which behave very similar to their concrete counterparts. In particular these types belong to the
RELEASENOTES view
@@ -1,7 +1,29 @@ Hackage: <http://hackage.haskell.org/package/sbv> GitHub:  <http://github.com/LeventErkok/sbv> -Latest Hackage released version: 2.0+Latest Hackage released version: 2.1++======================================================================+Version 2.1, 2012-05-24++ Library:+  - Add support for uninterpreted sorts, together with user defined+    domain axioms. See Data.SBV.Examples.Uninterpreted.Sort+    and Data.SBV.Examples.Uninterpreted.Deduce for basic examples of+    this feature.+  - Add support for C code-generation with SReals. The user picks+    one of 3 possible C types for the SReal type: CgFloat, CgDouble+    or CgLongDouble, using the function cgSRealType. Naturally, the+    resulting C program will suffer a loss of precision, as it will+    be subject to IEE-754 rounding as implied by the underlying type.+  - Add toSReal :: SInteger -> SReal, which can be used to promote+    symbolic integers to reals. Comes handy in mixed integer/real+    computations.+ Examples:+  - Recast the dog-cat-mouse example to use the solver over reals.+  - Add Data.SBV.Examples.Uninterpreted.Sort, and+        Data.SBV.Examples.Uninterpreted.Deduce+    for illustrating uninterpreted sorts and axioms.  ====================================================================== Version 2.0, 2012-05-10
SBVUnitTest/Examples/Arrays/Memory.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Simple memory abstraction and properties -----------------------------------------------------------------------------
SBVUnitTest/Examples/Basics/BasicTests.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Basic tests of the sbv library -----------------------------------------------------------------------------
SBVUnitTest/Examples/Basics/Higher.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Testing function equality -----------------------------------------------------------------------------
SBVUnitTest/Examples/Basics/Index.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Testing the select function -----------------------------------------------------------------------------
SBVUnitTest/Examples/Basics/ProofTests.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Basic proofs -----------------------------------------------------------------------------
SBVUnitTest/Examples/Basics/QRem.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Testing the qrem (quote-rem) function -----------------------------------------------------------------------------
SBVUnitTest/Examples/CRC/CCITT.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- CRC checks, hamming distance, etc. -----------------------------------------------------------------------------
SBVUnitTest/Examples/CRC/CCITT_Unidir.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Similar to CCITT. It shows that the CCITT is still HD 3 -- even if we consider only uni-directional errors
SBVUnitTest/Examples/CRC/GenPoly.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Finds good polynomials for CRC's -----------------------------------------------------------------------------
SBVUnitTest/Examples/CRC/Parity.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Parity check as CRC's -----------------------------------------------------------------------------
SBVUnitTest/Examples/CRC/USB5.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- The USB5 CRC implementation -----------------------------------------------------------------------------
SBVUnitTest/Examples/Puzzles/PowerSet.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Computes the powerset of a givenset -----------------------------------------------------------------------------
SBVUnitTest/Examples/Puzzles/Temperature.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Puzzle: --   What 2 digit fahrenheit/celcius values are reverses of each other?
SBVUnitTest/Examples/Uninterpreted/Uninterpreted.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Testing uninterpreted functions -----------------------------------------------------------------------------
SBVUnitTest/GoldFiles/auf-1.gold view
@@ -11,7 +11,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS-  uninterpreted_f :: SWord32 -> SWord64+  [uninterpreted] f :: SWord32 -> SWord64 USER GIVEN CODE SEGMENTS AXIOMS DEFINE@@ -21,10 +21,10 @@   s7 :: SWord32 = s1 - s3   s8 :: SBool = s0 == s7   s10 :: SWord32 = if s8 then s9 else s2-  s11 :: SWord64 = uninterpreted_f s10+  s11 :: SWord64 = [uninterpreted] f s10   s12 :: SWord32 = s1 - s0   s14 :: SWord32 = s12 + s13-  s15 :: SWord64 = uninterpreted_f s14+  s15 :: SWord64 = [uninterpreted] f s14   s16 :: SBool = s11 == s15   s17 :: SBool = s6 | s16 CONSTRAINTS
SBVUnitTest/GoldFiles/prefixSum_16.gold view
@@ -21,83 +21,79 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS-  uninterpreted_flOp :: SWord32 -> SWord32 -> SWord32-  uninterpreted_u :: SWord32+  [uninterpreted] flOp :: SWord32 -> SWord32 -> SWord32+  [uninterpreted] u :: SWord32 USER GIVEN CODE SEGMENTS AXIOMS   -- user defined axiom: flOp is associative   :assumption (forall (?x BitVec[32]) (?y BitVec[32]) (?z BitVec[32])-                      (= (uninterpreted_flOp (uninterpreted_flOp ?x ?y) ?z)-                         (uninterpreted_flOp ?x (uninterpreted_flOp ?y ?z))+                      (= (uninterpreted_flOp ?x (uninterpreted_flOp ?y ?z))+                         (uninterpreted_flOp (uninterpreted_flOp ?x ?y) ?z)                       )               )   -- user defined axiom: u is left-unit for flOp-  :assumption (forall (?x BitVec[32])-                      (= (uninterpreted_flOp uninterpreted_u ?x)-                         ?x-                      )-              )+  :assumption (forall (?x BitVec[32]) (= (uninterpreted_flOp uninterpreted_u ?x) ?x)) DEFINE-  s16 :: SWord32 = uninterpreted_u-  s17 :: SWord32 = s16 uninterpreted_flOp s0+  s16 :: SWord32 = [uninterpreted] u+  s17 :: SWord32 = s16 [uninterpreted] flOp s0   s18 :: SBool = s0 == s17-  s19 :: SWord32 = s0 uninterpreted_flOp s1-  s20 :: SWord32 = s16 uninterpreted_flOp s19+  s19 :: SWord32 = s0 [uninterpreted] flOp s1+  s20 :: SWord32 = s16 [uninterpreted] flOp s19   s21 :: SBool = s19 == s20-  s22 :: SWord32 = s19 uninterpreted_flOp s2-  s23 :: SWord32 = s20 uninterpreted_flOp s2+  s22 :: SWord32 = s19 [uninterpreted] flOp s2+  s23 :: SWord32 = s20 [uninterpreted] flOp s2   s24 :: SBool = s22 == s23-  s25 :: SWord32 = s22 uninterpreted_flOp s3-  s26 :: SWord32 = s2 uninterpreted_flOp s3-  s27 :: SWord32 = s19 uninterpreted_flOp s26-  s28 :: SWord32 = s16 uninterpreted_flOp s27+  s25 :: SWord32 = s22 [uninterpreted] flOp s3+  s26 :: SWord32 = s2 [uninterpreted] flOp s3+  s27 :: SWord32 = s19 [uninterpreted] flOp s26+  s28 :: SWord32 = s16 [uninterpreted] flOp s27   s29 :: SBool = s25 == s28-  s30 :: SWord32 = s25 uninterpreted_flOp s4-  s31 :: SWord32 = s28 uninterpreted_flOp s4+  s30 :: SWord32 = s25 [uninterpreted] flOp s4+  s31 :: SWord32 = s28 [uninterpreted] flOp s4   s32 :: SBool = s30 == s31-  s33 :: SWord32 = s30 uninterpreted_flOp s5-  s34 :: SWord32 = s4 uninterpreted_flOp s5-  s35 :: SWord32 = s28 uninterpreted_flOp s34+  s33 :: SWord32 = s30 [uninterpreted] flOp s5+  s34 :: SWord32 = s4 [uninterpreted] flOp s5+  s35 :: SWord32 = s28 [uninterpreted] flOp s34   s36 :: SBool = s33 == s35-  s37 :: SWord32 = s33 uninterpreted_flOp s6-  s38 :: SWord32 = s35 uninterpreted_flOp s6+  s37 :: SWord32 = s33 [uninterpreted] flOp s6+  s38 :: SWord32 = s35 [uninterpreted] flOp s6   s39 :: SBool = s37 == s38-  s40 :: SWord32 = s37 uninterpreted_flOp s7-  s41 :: SWord32 = s6 uninterpreted_flOp s7-  s42 :: SWord32 = s34 uninterpreted_flOp s41-  s43 :: SWord32 = s27 uninterpreted_flOp s42-  s44 :: SWord32 = s16 uninterpreted_flOp s43+  s40 :: SWord32 = s37 [uninterpreted] flOp s7+  s41 :: SWord32 = s6 [uninterpreted] flOp s7+  s42 :: SWord32 = s34 [uninterpreted] flOp s41+  s43 :: SWord32 = s27 [uninterpreted] flOp s42+  s44 :: SWord32 = s16 [uninterpreted] flOp s43   s45 :: SBool = s40 == s44-  s46 :: SWord32 = s40 uninterpreted_flOp s8-  s47 :: SWord32 = s44 uninterpreted_flOp s8+  s46 :: SWord32 = s40 [uninterpreted] flOp s8+  s47 :: SWord32 = s44 [uninterpreted] flOp s8   s48 :: SBool = s46 == s47-  s49 :: SWord32 = s46 uninterpreted_flOp s9-  s50 :: SWord32 = s8 uninterpreted_flOp s9-  s51 :: SWord32 = s44 uninterpreted_flOp s50+  s49 :: SWord32 = s46 [uninterpreted] flOp s9+  s50 :: SWord32 = s8 [uninterpreted] flOp s9+  s51 :: SWord32 = s44 [uninterpreted] flOp s50   s52 :: SBool = s49 == s51-  s53 :: SWord32 = s49 uninterpreted_flOp s10-  s54 :: SWord32 = s51 uninterpreted_flOp s10+  s53 :: SWord32 = s49 [uninterpreted] flOp s10+  s54 :: SWord32 = s51 [uninterpreted] flOp s10   s55 :: SBool = s53 == s54-  s56 :: SWord32 = s53 uninterpreted_flOp s11-  s57 :: SWord32 = s10 uninterpreted_flOp s11-  s58 :: SWord32 = s50 uninterpreted_flOp s57-  s59 :: SWord32 = s44 uninterpreted_flOp s58+  s56 :: SWord32 = s53 [uninterpreted] flOp s11+  s57 :: SWord32 = s10 [uninterpreted] flOp s11+  s58 :: SWord32 = s50 [uninterpreted] flOp s57+  s59 :: SWord32 = s44 [uninterpreted] flOp s58   s60 :: SBool = s56 == s59-  s61 :: SWord32 = s56 uninterpreted_flOp s12-  s62 :: SWord32 = s59 uninterpreted_flOp s12+  s61 :: SWord32 = s56 [uninterpreted] flOp s12+  s62 :: SWord32 = s59 [uninterpreted] flOp s12   s63 :: SBool = s61 == s62-  s64 :: SWord32 = s61 uninterpreted_flOp s13-  s65 :: SWord32 = s12 uninterpreted_flOp s13-  s66 :: SWord32 = s59 uninterpreted_flOp s65+  s64 :: SWord32 = s61 [uninterpreted] flOp s13+  s65 :: SWord32 = s12 [uninterpreted] flOp s13+  s66 :: SWord32 = s59 [uninterpreted] flOp s65   s67 :: SBool = s64 == s66-  s68 :: SWord32 = s64 uninterpreted_flOp s14-  s69 :: SWord32 = s66 uninterpreted_flOp s14+  s68 :: SWord32 = s64 [uninterpreted] flOp s14+  s69 :: SWord32 = s66 [uninterpreted] flOp s14   s70 :: SBool = s68 == s69-  s71 :: SWord32 = s68 uninterpreted_flOp s15-  s72 :: SWord32 = s14 uninterpreted_flOp s15-  s73 :: SWord32 = s65 uninterpreted_flOp s72-  s74 :: SWord32 = s58 uninterpreted_flOp s73-  s75 :: SWord32 = s43 uninterpreted_flOp s74+  s71 :: SWord32 = s68 [uninterpreted] flOp s15+  s72 :: SWord32 = s14 [uninterpreted] flOp s15+  s73 :: SWord32 = s65 [uninterpreted] flOp s72+  s74 :: SWord32 = s58 [uninterpreted] flOp s73+  s75 :: SWord32 = s43 [uninterpreted] flOp s74   s76 :: SBool = s71 == s75   s77 :: SBool = s70 & s76   s78 :: SBool = s67 & s77
SBVUnitTest/SBVTest.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Integration with HUnit-based test suite for SBV -----------------------------------------------------------------------------
SBVUnitTest/SBVUnitTest.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- SBV library unit-test program -----------------------------------------------------------------------------
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where  buildTime :: String-buildTime = "Thu May 10 00:22:26 PDT 2012"+buildTime = "Wed May 23 20:53:39 PDT 2012"
SBVUnitTest/TestSuite/Arrays/Memory.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Examples.Arrays.Memory -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Basics/Arithmetic.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for basic concrete arithmetic -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Basics/BasicTests.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Examples.Basics.BasicTests -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Basics/Higher.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Examples.Basics.Higher -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Basics/Index.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Examples.Basics.Index -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Basics/ProofTests.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Examples.Basics.ProofTests -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Basics/QRem.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Examples.Basics.QRem -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/BitPrecise/BitTricks.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.BitPrecise.BitTricks -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/BitPrecise/Legato.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.BitPrecise.Legato -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/BitPrecise/MergeSort.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.BitPrecise.MergeSort -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/BitPrecise/PrefixSum.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.PrefixSum.PrefixSum -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/CRC/CCITT.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Examples.CRC.CCITT -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/CRC/CCITT_Unidir.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Examples.CRC.CCITT_Unidir -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/CRC/GenPoly.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Examples.CRC.GenPoly -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/CRC/Parity.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Examples.CRC.Parity -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/CRC/USB5.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Examples.CRC.USB5 -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/CodeGeneration/AddSub.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.CodeGeneration.AddSub -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/CodeGeneration/CRC_USB5.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.CodeGeneration.CRC_USB5 -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/CodeGeneration/CgTests.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for code-generation features -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/CodeGeneration/Fibonacci.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.CodeGeneration.Fibonacci -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/CodeGeneration/GCD.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.CodeGeneration.GCD -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/CodeGeneration/PopulationCount.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.CodeGeneration.PopulationCount -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/CodeGeneration/Uninterpreted.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.CodeGeneration.Uninterpreted -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Crypto/AES.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.Crypto.AES -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Crypto/RC4.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.Crypto.RC4 -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Existentials/CRCPolynomial.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.Existentials.CRCPolynomial -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Polynomials/Polynomials.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.Polynomials.Polynomials -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Puzzles/Coins.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.Puzzles.Coins -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Puzzles/Counts.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.Puzzles.Counts -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Puzzles/DogCatMouse.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.Puzzles.DogCatMouse -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Puzzles/Euler185.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.Puzzles.Euler185 -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Puzzles/MagicSquare.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.Puzzles.MagicSquare -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Puzzles/NQueens.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.Puzzles.NQueens -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Puzzles/PowerSet.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Examples.Puzzles.PowerSet -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Puzzles/Sudoku.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.Puzzles.Sudoku -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Puzzles/Temperature.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Examples.Puzzles.Temperature -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Puzzles/U2Bridge.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.Puzzles.U2Bridge -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Uninterpreted/AUF.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Data.SBV.Examples.Uninterpreted.AUF -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Uninterpreted/Function.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Testsuite for Data.SBV.Examples.Uninterpreted.Function -----------------------------------------------------------------------------
SBVUnitTest/TestSuite/Uninterpreted/Uninterpreted.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Test suite for Examples.Uninterpreted.Uninterpreted -----------------------------------------------------------------------------
Setup.hs view
@@ -5,7 +5,6 @@ -- License     :  BSD3 -- Maintainer  :  erkokl@gmail.com -- Stability   :  experimental--- Portability :  portable -- -- Setup module for the sbv library -----------------------------------------------------------------------------
sbv.cabal view
@@ -1,5 +1,5 @@ Name:          sbv-Version:       2.0+Version:       2.1 Category:      Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis:      SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description:   Express properties about Haskell programs and automatically prove them using SMT@@ -33,9 +33,10 @@                .                  * Symbolic polynomials over GF(2^n), and polynomial arithmetic                .-                 * Uninterpreted constants and functions over symbolic values, with user-                   defined SMT-Lib axioms+                 * Uninterpreted constants and functions over symbolic values, with user defined axioms.                .+                 * Uninterpreted sorts, and proofs over such sorts, potentially with axioms.+               .                Functions built out of these types can be:                .                  * proven correct via an external SMT solver (the 'prove' function)@@ -44,12 +45,13 @@                .                  * used in synthesis (the 'sat' function with existential variables)                .-                 * optimized with respect to cost functions (the 'optimize', 'maximize', and 'minimize' functions)+                 * optimized with respect to cost functions (the 'optimize', 'maximize',+                 and 'minimize' functions)                .                  * quick-checked                .-                 * used in concrete test case generation (the 'genTest' function), rendered as values in various-                   languages, including Haskell and C.+                 * 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.@@ -67,7 +69,8 @@                .                The following people reported bugs, provided comments/feedback, or contributed to the                development of SBV in various ways: Ian Blumenfeld, Ian Calvert, Iavor Diatchki, John-               Erickson, Tom Hawkins, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson, and Nis Wegmann.+               Erickson, Tom Hawkins, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson, and+               Nis Wegmann.                .                Release notes can be seen at: <http://github.com/LeventErkok/sbv/blob/master/RELEASENOTES>. @@ -90,6 +93,25 @@  Library   ghc-options     : -Wall+  other-extensions: BangPatterns+                    CPP+                    -- DefaultSignatures flag is not present in cabal 1.14.0; so ignore for the time being+                    -- DefaultSignatures+                    DeriveDataTypeable+                    FlexibleContexts+                    FlexibleInstances+                    FunctionalDependencies+                    GeneralizedNewtypeDeriving+                    MultiParamTypeClasses+                    OverlappingInstances+                    ParallelListComp+                    PatternGuards+                    Rank2Types+                    RankNTypes+                    ScopedTypeVariables+                    TupleSections+                    TypeOperators+                    TypeSynonymInstances   Build-Depends   : array               >= 0.3.0.1                   , base                >= 3 && < 5                   , containers          >= 0.3.0.0@@ -103,6 +125,7 @@                   , QuickCheck          >= 2.4.0.1                   , random              >= 1.0.1.1                   , strict-concurrency  >= 0.2.4.1+                  , syb                 >= 0.3.6   Exposed-modules : Data.SBV                   , Data.SBV.Internals                   , Data.SBV.Examples.BitPrecise.BitTricks@@ -129,7 +152,9 @@                   , Data.SBV.Examples.Puzzles.Sudoku                   , Data.SBV.Examples.Puzzles.U2Bridge                   , Data.SBV.Examples.Uninterpreted.AUF+                  , Data.SBV.Examples.Uninterpreted.Deduce                   , Data.SBV.Examples.Uninterpreted.Function+                  , Data.SBV.Examples.Uninterpreted.Sort   Other-modules   : Data.SBV.BitVectors.AlgReals                   , Data.SBV.BitVectors.Data                   , Data.SBV.BitVectors.Model@@ -157,6 +182,10 @@  Executable SBVUnitTests   ghc-options     : -Wall+  other-extensions: Rank2Types+                    RankNTypes+                    ScopedTypeVariables+                    TupleSections   Build-depends   : base      >= 3 && < 5                   , directory >= 1.0.1.1                   , HUnit     >= 1.2.4.2