packages feed

sbv 5.3 → 5.4

raw patch · 76 files changed

+597/−184 lines, 76 filesdep ~basedep ~deepseq

Dependency ranges changed: base, deepseq

Files

CHANGES.md view
@@ -1,8 +1,25 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub:  <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 5.3, 2015-10-20+* Latest Hackage released version: 5.4, 2015-11-09 +### Version 5.4, 2015-11-09++  * Add 'sAssert', which allows users to pepper their code with boolean conditions, much like+    the usual ASSERT calls. Note that the semantics of an 'sAssert' is that it is a NOOP, i.e.,+    it simply returns its final argument. Use in coordination with 'safe' and 'safeWith', see below.++  * Implement 'safe' and 'safeWith', which statically determine all calls to 'sAssert'+    being safe to execute. Any vilations will be flagged. ++  * SBV->C: Translate 'sAssert' calls to dynamic checks in the generated C code. If this is+    not desired, use the 'cgIgnoreSAssert' function to turn it off.++  * Add 'isSafe': Which converts a 'SafeResult' to a 'Bool', when we are only interested+    in a boolean result.++  * Add Data/SBV/Examples/Misc/NoDiv0 to demonstrate the use of the 'safe' function.+ ### Version 5.3, 2015-10-20    * Main point of this release to make SBV compile with GHC 7.8 again, to accommodate mainly@@ -918,7 +935,7 @@      can now specify the corresponding C code and SBV will simply      call the "native" functions instead of generating it. This      enables interfacing with other C programs. See the functions:-     cgAddPrototype, cgAddDecl, and cgAddLDFlags.+     cgAddPrototype, cgAddDecl, cgAddLDFlags    Examples:
Data/SBV.hs view
@@ -28,11 +28,11 @@ -- @ -- -- The class 'Provable' comes with instances for n-ary predicates, for arbitrary n.--- The predicates are just regular Haskell functions over symbolic signed and unsigned--- bit-vectors. Functions for checking satisfiability ('sat' and 'allSat') are also+-- The predicates are just regular Haskell functions over symbolic types listed below.+-- Functions for checking satisfiability ('sat' and 'allSat') are also -- provided. ----- In particular, the sbv library introduces the types:+-- The sbv library introduces the following symbolic types: -- --   * 'SBool': Symbolic Booleans (bits). --@@ -105,13 +105,13 @@ -- get in touch if there is a solver you'd like to see included. --------------------------------------------------------------------------------- -{-# LANGUAGE FlexibleInstances    #-}+{-# LANGUAGE FlexibleInstances #-}  -- TODO: remove OverlappingInstances and these warning suppressions -- once support is dropped for GHC 7.8-{-# OPTIONS_GHC -fno-warn-deprecated-flags #-}+{-# OPTIONS_GHC -fno-warn-deprecated-flags     #-} {-# OPTIONS_GHC -fno-warn-unrecognised-pragmas #-}-{-# LANGUAGE OverlappingInstances #-}+{-# LANGUAGE OverlappingInstances              #-}  module Data.SBV (   -- * Programming with symbolic values@@ -192,7 +192,7 @@   -- * Enumerations   -- $enumerations -  -- * Properties, proofs, and satisfiability+  -- * Properties, proofs, satisfiability, and safety   -- $proveIntro    -- ** Predicates@@ -201,6 +201,9 @@   , prove, proveWith, isTheorem, isTheoremWith   -- ** Checking satisfiability   , sat, satWith, isSatisfiable, isSatisfiableWith+  -- ** Checking safety+  -- $safeIntro+  , sAssert, safe, safeWith, isSafe, SExecutable(..)   -- ** Finding all satisfying assignments   , allSat, allSatWith   -- ** Satisfying a sequence of boolean conditions@@ -228,7 +231,7 @@    -- ** Inspecting proof results   -- $resultTypes-  , ThmResult(..), SatResult(..), AllSatResult(..), SMTResult(..)+  , ThmResult(..), SatResult(..), SafeResult(..), AllSatResult(..), SMTResult(..)    -- ** Programmable model extraction   -- $programmableExtraction@@ -264,7 +267,7 @@   , cgReturn, cgReturnArr    -- ** Code generation with uninterpreted functions-  , cgAddPrototype, cgAddDecl, cgAddLDFlags+  , cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert    -- ** Code generation with 'SInteger' and 'SReal' types   -- $unboundedCGen@@ -354,6 +357,11 @@    where try s = async $ what s a >>= \r -> return (name (solver s), r)          go []  = return []          go as  = do (d, r) <- waitAny as+                     -- The following filter works because the Eq instance on Async+                     -- checks the thread-id; so we know that we're removing the+                     -- correct solver from the list. This also allows for+                     -- running the same-solver (with different options), since+                     -- they will get different thread-ids.                      rs <- unsafeInterleaveIO $ go (filter (/= d) as)                      return (r : rs) @@ -481,6 +489,45 @@ Note that the function 'sbvAvailableSolvers' will return all the installed solvers, which can be used as the first argument to all these functions, if you simply want to try all available solvers on a machine. -}++{- $safeIntro++The 'sAssert' function allow users to introduce invariants through-out their code to make sure+certain properties hold at all times. This is another mechanism to provide further documentation/contract info+into SBV code. The functions 'safe' and 'safeWith' can then be used to statically discharge these proof assumptions.+If a violation is found, SBV will print a model showing which inputs lead to the invariant being violated.++Here's a simple example. Let's assume we have a function that does subtraction, and requires its+first argument to be larger than the second:++>>> let sub x y = sAssert Nothing "sub: x >= y must hold!" (x .>= y) (x - y)++Clearly, this function is not safe, as there's nothing that ensures us to pass a larger second argument.+We can use 'safe' to statically see if such a violation is possible before we use this function elsewhere.++>>> safe (sub :: SInt8 -> SInt8 -> SInt8)+[sub: x >= y must hold!: Violated. Model:+  s0 = -128 :: Int8+  s1 = -127 :: Int8]++What happens if we make sure to arrange for this invariant? Consider this version:++>>> let safeSub x y = ite (x .>= y) (sub x y) 0++Clearly, 'safeSub' must be safe. And indeed, SBV can prove that:++>>> safe (safeSub :: SInt8 -> SInt8 -> SInt8)+[sub: x >= y must hold!: No violations detected]++Note how we used 'sub' and 'safeSub' polymorphically. We only need to monomorphise our types when a proof+attempt is done, as we did in the 'safe' calls.++If required, the user can pass a 'CallStack' through the first argument to 'sAssert', which will be used+by SBV to print a diagnostic info to pinpoint the failure.++Also see "Data.SBV.Examples.Misc.NoDiv0" for the classic div-by-zero example.+-}+  {- $optimizeIntro Symbolic optimization. A call of the form:
Data/SBV/BitVectors/Data.hs view
@@ -35,10 +35,10 @@  , SBVExpr(..), newExpr  , cache, Cached, uncache, uncacheAI, HasKind(..)  , Op(..), FPOp(..), NamedSymVar, getTableIndex- , SBVPgm(..), Symbolic, runSymbolic, runSymbolic', State, getPathCondition, extendPathCondition+ , SBVPgm(..), Symbolic, SExecutable(..), runSymbolic, runSymbolic', State, getPathCondition, extendPathCondition  , inProofMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..)  , Logic(..), SMTLibLogic(..)- , getTraceInfo, getConstraints, addConstraint, internalVariable, internalConstraint, isCodeGenMode+ , addConstraint, internalVariable, internalConstraint, isCodeGenMode  , SBVType(..), newUninterpreted, addAxiom  , Quantifier(..), needsExistentials  , SMTLibPgm(..), SMTLibVersion(..), smtLibVersionExtension@@ -53,7 +53,7 @@ import Control.Monad.Trans  (liftIO) import Data.Int             (Int8, Int16, Int32, Int64) import Data.Word            (Word8, Word16, Word32, Word64)-import Data.List            (elemIndex)+import Data.List            (elemIndex, intercalate) import Data.Maybe           (fromMaybe)  import qualified Data.Generics as G    (Data(..))@@ -514,3 +514,100 @@  instance NFData a => NFData (SBV a) where   rnf (SBV x) = rnf x `seq` ()++-- | Symbolically executable program fragments. This class is mainly used for 'safe' calls, and is sufficently populated internally to cover most use+-- cases. Users can extend it as they wish to allow 'safe' checks for SBV programs that return/take types that are user-defined.+class SExecutable a where+   sName_ :: a -> Symbolic ()+   sName  :: [String] -> a -> Symbolic ()++instance NFData a => SExecutable (Symbolic a) where+   sName_   a = a >>= \r -> rnf r `seq` return ()+   sName []   = sName_+   sName xs   = error $ "SBV.SExecutable.sName: Extra unmapped name(s): " ++ intercalate ", " xs++instance NFData a => SExecutable (SBV a) where+   sName_   v = sName_ (output v)+   sName xs v = sName xs (output v)++-- Unit output+instance SExecutable () where+   sName_   () = sName_   (output ())+   sName xs () = sName xs (output ())++-- List output+instance (NFData a, SymWord a) => SExecutable [SBV a] where+   sName_   vs = sName_   (output vs)+   sName xs vs = sName xs (output vs)++-- 2 Tuple output+instance (NFData a, SymWord a, NFData b, SymWord b) => SExecutable (SBV a, SBV b) where+  sName_ (a, b) = sName_ (output a >> output b)+  sName _       = sName_++-- 3 Tuple output+instance (NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c) => SExecutable (SBV a, SBV b, SBV c) where+  sName_ (a, b, c) = sName_ (output a >> output b >> output c)+  sName _          = sName_++-- 4 Tuple output+instance (NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d) => SExecutable (SBV a, SBV b, SBV c, SBV d) where+  sName_ (a, b, c, d) = sName_ (output a >> output b >> output c >> output c >> output d)+  sName _             = sName_++-- 5 Tuple output+instance (NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e) where+  sName_ (a, b, c, d, e) = sName_ (output a >> output b >> output c >> output d >> output e)+  sName _                = sName_++-- 6 Tuple output+instance (NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) where+  sName_ (a, b, c, d, e, f) = sName_ (output a >> output b >> output c >> output d >> output e >> output f)+  sName _                   = sName_++-- 7 Tuple output+instance (NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f, NFData g, SymWord g) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) where+  sName_ (a, b, c, d, e, f, g) = sName_ (output a >> output b >> output c >> output d >> output e >> output f >> output g)+  sName _                      = sName_++-- Functions+instance (SymWord a, SExecutable p) => SExecutable (SBV a -> p) where+   sName_        k = forall_   >>= \a -> sName_   $ k a+   sName (s:ss)  k = forall s  >>= \a -> sName ss $ k a+   sName []      k = sName_ k++-- 2 Tuple input+instance (SymWord a, SymWord b, SExecutable p) => SExecutable ((SBV a, SBV b) -> p) where+  sName_        k = forall_  >>= \a -> sName_   $ \b -> k (a, b)+  sName (s:ss)  k = forall s >>= \a -> sName ss $ \b -> k (a, b)+  sName []      k = sName_ k++-- 3 Tuple input+instance (SymWord a, SymWord b, SymWord c, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c) -> p) where+  sName_       k  = forall_  >>= \a -> sName_   $ \b c -> k (a, b, c)+  sName (s:ss) k  = forall s >>= \a -> sName ss $ \b c -> k (a, b, c)+  sName []     k  = sName_ k++-- 4 Tuple input+instance (SymWord a, SymWord b, SymWord c, SymWord d, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d) -> p) where+  sName_        k = forall_  >>= \a -> sName_   $ \b c d -> k (a, b, c, d)+  sName (s:ss)  k = forall s >>= \a -> sName ss $ \b c d -> k (a, b, c, d)+  sName []      k = sName_ k++-- 5 Tuple input+instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) where+  sName_        k = forall_  >>= \a -> sName_   $ \b c d e -> k (a, b, c, d, e)+  sName (s:ss)  k = forall s >>= \a -> sName ss $ \b c d e -> k (a, b, c, d, e)+  sName []      k = sName_ k++-- 6 Tuple input+instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) where+  sName_        k = forall_  >>= \a -> sName_   $ \b c d e f -> k (a, b, c, d, e, f)+  sName (s:ss)  k = forall s >>= \a -> sName ss $ \b c d e f -> k (a, b, c, d, e, f)+  sName []      k = sName_ k++-- 7 Tuple input+instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) where+  sName_        k = forall_  >>= \a -> sName_   $ \b c d e f g -> k (a, b, c, d, e, f, g)+  sName (s:ss)  k = forall s >>= \a -> sName ss $ \b c d e f g -> k (a, b, c, d, e, f, g)+  sName []      k = sName_ k
Data/SBV/BitVectors/Model.hs view
@@ -29,6 +29,7 @@   , sWord32s, sWord64, sWord64s, sInt8, sInt8s, sInt16, sInt16s, sInt32, sInt32s, sInt64   , sInt64s, sInteger, sIntegers, sReal, sReals, sFloat, sFloats, sDouble, sDoubles, slet   , sIntegerToSReal, label+  , sAssert   , liftQRem, liftDMod, symbolicMergeWithKind   , genLiteral, genFromCW, genMkSymVar   , isSatisfiableInCurrentPath@@ -39,6 +40,8 @@ import Control.Monad.Reader (ask) import Control.Monad.Trans  (liftIO) +import GHC.Stack+ import Data.Array      (Array, Ix, listArray, elems, bounds, rangeSize) import Data.Bits       (Bits(..)) import Data.Int        (Int8, Int16, Int32, Int64)@@ -1098,6 +1101,20 @@   | Just r <- unliteral t = if r then a else b   | True                  = symbolicMerge False t a b +-- | Symbolic assert. Check that the given boolean condition is always true in the given path. The+-- optional first argument can be used to provide call-stack info via GHC's location facilities.+sAssert :: HasKind a => Maybe CallStack -> String -> SBool -> SBV a -> SBV a+sAssert cs msg cond x = SBV $ SVal k $ Right $ cache r+  where k     = kindOf x+        r st  = do xsw <- sbvToSW st x+                   let pc = getPathCondition st+                       -- We're checking if there are any cases where the path-condition holds, but not the condition+                       -- Any violations of this, should be signaled, i.e., whenever the following formula is satisfiable+                       mustNeverHappen = pc &&& bnot cond+                   cnd <- sbvToSW st mustNeverHappen+                   addAssertion st cs msg cnd+                   return xsw+ -- | Merge two symbolic values, at kind @k@, possibly @force@'ing the branches to make -- sure they do not evaluate to the same result. This should only be used for internal purposes; -- as default definitions provided should suffice in many cases. (i.e., End users should@@ -1537,7 +1554,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{resTraces=tvals, resConsts=cs, resConstraints=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 ++ ")"
Data/SBV/BitVectors/Symbolic.hs view
@@ -42,8 +42,7 @@   , SBVPgm(..), Symbolic, runSymbolic, runSymbolic', State   , inProofMode, SBVRunMode(..), Result(..)   , Logic(..), SMTLibLogic(..)-  , getTraceInfo, getConstraints-  , addSValConstraint, internalConstraint, internalVariable+  , addAssertion, addSValConstraint, internalConstraint, internalVariable   , SMTLibPgm(..), SMTLibVersion(..), smtLibVersionExtension   , SolverCapabilities(..)   , extractSymbolicSimulationState@@ -62,6 +61,8 @@ import Data.List            (intercalate, sortBy) import Data.Maybe           (isJust, fromJust, fromMaybe) +import GHC.Stack+ import qualified Data.Generics as G    (Data(..)) import qualified Data.Typeable as T    (Typeable) import qualified Data.IntMap   as IMap (IntMap, empty, size, toAscList, lookup, insert, insertWith)@@ -275,33 +276,27 @@ type NamedSymVar = (SW, String)  -- | Result of running a symbolic computation-data Result = Result (Set.Set Kind)                -- kinds used in the program-                     [(String, CW)]                -- quick-check counter-example information (if any)-                     [(String, [String])]          -- uninterpeted code segments-                     [(Quantifier, NamedSymVar)]   -- inputs (possibly existential)-                     [(SW, CW)]                    -- constants-                     [((Int, Kind, Kind), [SW])]   -- tables (automatically constructed) (tableno, index-type, result-type) elts-                     [(Int, ArrayInfo)]            -- arrays (user specified)-                     [(String, SBVType)]           -- uninterpreted constants-                     [(String, [String])]          -- axioms-                     SBVPgm                        -- assignments-                     [SW]                          -- additional constraints (boolean)-                     [SW]                          -- outputs---- | Extract the constraints from a result-getConstraints :: Result -> [SW]-getConstraints (Result _ _ _ _ _ _ _ _ _ _ cstrs _) = cstrs---- | Extract the traced-values from a result (quick-check)-getTraceInfo :: Result -> [(String, CW)]-getTraceInfo (Result _ tvals _ _ _ _ _ _ _ _ _ _) = tvals+data Result = Result { reskinds       :: Set.Set Kind                     -- ^ kinds used in the program+                     , resTraces      :: [(String, CW)]                   -- ^ quick-check counter-example information (if any)+                     , resUISegs      :: [(String, [String])]             -- ^ uninterpeted code segments+                     , resInputs      :: [(Quantifier, NamedSymVar)]      -- ^ inputs (possibly existential)+                     , resConsts      :: [(SW, CW)]                       -- ^ constants+                     , resTables      :: [((Int, Kind, Kind), [SW])]      -- ^ tables (automatically constructed) (tableno, index-type, result-type) elts+                     , resArrays      :: [(Int, ArrayInfo)]               -- ^ arrays (user specified)+                     , resUOConsts    :: [(String, SBVType)]              -- ^ uninterpreted constants+                     , resAxioms      :: [(String, [String])]             -- ^ axioms+                     , resAsgns       :: SBVPgm                           -- ^ assignments+                     , resConstraints :: [SW]                             -- ^ additional constraints (boolean)+                     , resAssertions  :: [(String, Maybe CallStack, SW)]  -- ^ assertions+                     , resOutputs     :: [SW]                             -- ^ outputs+                     }  -- | Show instance for 'Result'. Only for debugging purposes. instance Show Result where-  show (Result _ _ _ _ cs _ _ [] [] _ [] [r])+  show (Result _ _ _ _ cs _ _ [] [] _ [] _ [r])     | Just c <- r `lookup` cs     = show c-  show (Result kinds _ cgs is cs ts as uis axs xs cstrs os)  = intercalate "\n" $+  show (Result kinds _ cgs is cs ts as uis axs xs cstrs asserts os)  = intercalate "\n" $                    (if null usorts then [] else "SORTS" : map ("  " ++) usorts)                 ++ ["INPUTS"]                 ++ map shn is@@ -321,6 +316,8 @@                 ++ map (\(s, e) -> "  " ++ shs s ++ " = " ++ show e) (F.toList (pgmAssignments xs))                 ++ ["CONSTRAINTS"]                 ++ map (("  " ++) . show) cstrs+                ++ ["ASSERTIONS"]+                ++ map (("  "++) . shAssert) asserts                 ++ ["OUTPUTS"]                 ++ map (("  " ++) . show) os     where usorts = [sh s t | KUserSort s t <- Set.toList kinds]@@ -343,6 +340,7 @@                         | True     = ", aliasing " ++ show nm           shui (nm, t) = "  [uninterpreted] " ++ nm ++ " :: " ++ show t           shax (nm, ss) = "  -- user defined axiom: " ++ nm ++ "\n  " ++ intercalate "\n  " ss+          shAssert (nm, stk, p) = "  -- assertion: " ++ nm ++ " " ++ maybe "[No location]" showCallStack stk ++ ": " ++ show p  -- | The context of a symbolic array as created data ArrayContext = ArrayFree (Maybe SW)     -- ^ A new array, with potential initializer for each cell@@ -421,6 +419,7 @@                     , rUIMap       :: IORef UIMap                     , rCgMap       :: IORef CgMap                     , raxioms      :: IORef [(String, [String])]+                    , rAsserts     :: IORef [(String, Maybe CallStack, SW)]                     , rSWCache     :: IORef (Cache SW)                     , rAICache     :: IORef (Cache Int)                     }@@ -513,6 +512,10 @@                         when (isJust mbCode) $ modifyIORef (rCgMap st) (Map.insert nm (fromJust mbCode))   where validChar x = isAlphaNum x || x `elem` "_" +-- | Add a new sAssert based constraint+addAssertion :: State -> Maybe CallStack -> String -> SW -> IO ()+addAssertion st cs msg cond = modifyIORef (rAsserts st) ((msg, cs, cond):)+ -- | Create an internal variable, which acts as an input but isn't visible to the user. -- Such variables are existentially quantified in a SAT context, and universally quantified -- in a proof context.@@ -685,6 +688,7 @@    aiCache   <- newIORef IMap.empty    usedKinds <- newIORef Set.empty    cstrs     <- newIORef []+   asserts   <- newIORef []    rGen      <- case currentRunMode of                   Concrete g -> newIORef g                   _          -> newStdGen >>= newIORef@@ -707,6 +711,7 @@                   , rSWCache     = swCache                   , rAICache     = aiCache                   , rConstraints = cstrs+                  , rAsserts     = asserts                   }    _ <- newConst st falseCW -- s(-2) == falseSW    _ <- newConst st trueCW  -- s(-1) == trueSW@@ -718,7 +723,7 @@ -- instance when implementing 'sBranch'. extractSymbolicSimulationState :: State -> IO Result extractSymbolicSimulationState st@State{ spgm=pgm, rinps=inps, routs=outs, rtblMap=tables, rArrayMap=arrays, rUIMap=uis, raxioms=axioms-                                       , rUsedKinds=usedKinds, rCgMap=cgs, rCInfo=cInfo, rConstraints = cstrs} = do+                                       , rAsserts=asserts, rUsedKinds=usedKinds, rCgMap=cgs, rCInfo=cInfo, rConstraints=cstrs} = do    SBVPgm rpgm  <- readIORef pgm    inpsO <- reverse `fmap` readIORef inps    outsO <- reverse `fmap` readIORef outs@@ -734,7 +739,8 @@    cgMap <- Map.toList `fmap` readIORef cgs    traceVals <- reverse `fmap` readIORef cInfo    extraCstrs <- reverse `fmap` readIORef cstrs-   return $ Result knds traceVals cgMap inpsO cnsts tbls arrs unint axs (SBVPgm rpgm) extraCstrs outsO+   assertions <- reverse `fmap` readIORef asserts+   return $ Result knds traceVals cgMap inpsO cnsts tbls arrs unint axs (SBVPgm rpgm) extraCstrs assertions outsO  -- | Handling constraints imposeConstraint :: SVal -> Symbolic ()@@ -911,9 +917,9 @@ smtLibVersionExtension SMTLib2 = "smt2"  -- | Representation of an SMT-Lib program. In between pre and post goes the refuted models-data SMTLibPgm = SMTLibPgm SMTLibVersion  ( [(String, SW)]          -- alias table-                                          , [String]                -- pre: declarations.-                                          , [String])               -- post: formula+data SMTLibPgm = SMTLibPgm SMTLibVersion  ( [(String, SW)]  -- alias table+                                          , [String]        -- pre: declarations.+                                          , [String])       -- post: formula instance NFData SMTLibVersion where rnf a = seq a () instance NFData SMTLibPgm     where rnf a = seq a () @@ -924,12 +930,16 @@ instance NFData CW where   rnf (CW x y) = x `seq` y `seq` () +-- Can't really force this, but not a big deal+instance NFData CallStack where+  rnf _ = ()+ instance NFData Result where-  rnf (Result kindInfo qcInfo cgs inps consts tbls arrs uis axs pgm cstr outs)-        = rnf kindInfo `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 kindInfo qcInfo cgs inps consts tbls arrs uis axs pgm cstr asserts outs)+        = rnf kindInfo `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 asserts `seq` rnf outs instance NFData Kind          where rnf a = seq a () instance NFData ArrayContext  where rnf a = seq a () instance NFData SW            where rnf a = seq a ()
Data/SBV/Bridge/ABC.hs view
@@ -25,13 +25,13 @@   -- * ABC specific interface   sbvCurrentSolver   -- ** Proving, checking satisfiability-  , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable+  , prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable   -- ** Optimization routines   , optimize, minimize, maximize   , module Data.SBV   ) where -import Data.SBV hiding (prove, sat, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)+import Data.SBV hiding (prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)  -- | Current solver instance, pointing to abc. sbvCurrentSolver :: SMTConfig@@ -48,6 +48,12 @@     => a                -- ^ Property to check     -> IO SatResult     -- ^ Response of the SMT Solver, containing the model if found sat = satWith sbvCurrentSolver++-- | Check all 'sAssert' calls are safe, using ABC+safe :: SExecutable a+    => a                -- ^ Program containing sAssert calls+    -> IO [SafeResult]+safe = safeWith sbvCurrentSolver  -- | Find all satisfying solutions, using ABC allSat :: Provable a
Data/SBV/Bridge/Boolector.hs view
@@ -25,7 +25,7 @@   -- * Boolector specific interface   sbvCurrentSolver   -- ** Proving, checking satisfiability-  , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable+  , prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable   -- ** Optimization routines   , optimize, minimize, maximize   -- * Non-Boolector specific SBV interface@@ -33,51 +33,57 @@   , module Data.SBV   ) where -import Data.SBV hiding (prove, sat, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)+import Data.SBV hiding (prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver) --- | Current solver instance, pointing to cvc4.+-- | Current solver instance, pointing to Boolector. sbvCurrentSolver :: SMTConfig sbvCurrentSolver = boolector --- | Prove theorems, using the CVC4 SMT solver+-- | Prove theorems, using the Boolector SMT solver prove :: Provable a       => a              -- ^ Property to check       -> IO ThmResult   -- ^ Response from the SMT solver, containing the counter-example if found prove = proveWith sbvCurrentSolver --- | Find satisfying solutions, using the CVC4 SMT solver+-- | Find satisfying solutions, using the Boolector SMT solver sat :: Provable a     => a                -- ^ Property to check     -> IO SatResult     -- ^ Response of the SMT Solver, containing the model if found sat = satWith sbvCurrentSolver --- | Find all satisfying solutions, using the CVC4 SMT solver+-- | Check all 'sAssert' calls are safe, using the Boolector SMT solver+safe :: SExecutable a+    => a                -- ^ Program containing sAssert calls+    -> IO [SafeResult]+safe = safeWith sbvCurrentSolver++-- | Find all satisfying solutions, using the Boolector SMT solver allSat :: Provable a        => a                -- ^ Property to check        -> IO AllSatResult  -- ^ List of all satisfying models allSat = allSatWith sbvCurrentSolver --- | Check vacuity of the explicit constraints introduced by calls to the 'constrain' function, using the CVC4 SMT solver+-- | Check vacuity of the explicit constraints introduced by calls to the 'constrain' function, using the Boolector SMT solver isVacuous :: Provable a           => a             -- ^ Property to check           -> IO Bool       -- ^ True if the constraints are unsatisifiable isVacuous = isVacuousWith sbvCurrentSolver --- | Check if the statement is a theorem, with an optional time-out in seconds, using the CVC4 SMT solver+-- | Check if the statement is a theorem, with an optional time-out in seconds, using the Boolector SMT solver isTheorem :: Provable a           => Maybe Int          -- ^ Optional time-out, specify in seconds           -> a                  -- ^ Property to check           -> IO (Maybe Bool)    -- ^ Returns Nothing if time-out expires isTheorem = isTheoremWith sbvCurrentSolver --- | Check if the statement is satisfiable, with an optional time-out in seconds, using the CVC4 SMT solver+-- | Check if the statement is satisfiable, with an optional time-out in seconds, using the Boolector SMT solver isSatisfiable :: Provable a               => Maybe Int       -- ^ Optional time-out, specify in seconds               -> a               -- ^ Property to check               -> IO (Maybe Bool) -- ^ Returns Nothing if time-out expiers isSatisfiable = isSatisfiableWith sbvCurrentSolver --- | Optimize cost functions, using the CVC4 SMT solver+-- | Optimize cost functions, using the Boolector SMT solver optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)          => OptimizeOpts                -- ^ Parameters to optimization (Iterative, Quantified, etc.)          -> (SBV c -> SBV c -> SBool)   -- ^ Betterness check: This is the comparison predicate for optimization@@ -87,7 +93,7 @@          -> IO (Maybe [a])              -- ^ Returns Nothing if there is no valid solution, otherwise an optimal solution optimize = optimizeWith sbvCurrentSolver --- | Minimize cost functions, using the CVC4 SMT solver+-- | Minimize cost functions, using the Boolector SMT solver minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)          => OptimizeOpts                -- ^ Parameters to optimization (Iterative, Quantified, etc.)          -> ([SBV a] -> SBV c)          -- ^ Cost function to minimize@@ -96,7 +102,7 @@          -> IO (Maybe [a])              -- ^ Returns Nothing if there is no valid solution, otherwise an optimal solution minimize = minimizeWith sbvCurrentSolver --- | Maximize cost functions, using the CVC4 SMT solver+-- | Maximize cost functions, using the Boolector SMT solver maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)          => OptimizeOpts                -- ^ Parameters to optimization (Iterative, Quantified, etc.)          -> ([SBV a] -> SBV c)          -- ^ Cost function to maximize
Data/SBV/Bridge/CVC4.hs view
@@ -25,7 +25,7 @@   -- * CVC4 specific interface   sbvCurrentSolver   -- ** Proving, checking satisfiability-  , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable+  , prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable   -- ** Optimization routines   , optimize, minimize, maximize   -- * Non-CVC4 specific SBV interface@@ -33,7 +33,7 @@   , module Data.SBV   ) where -import Data.SBV hiding (prove, sat, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)+import Data.SBV hiding (prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)  -- | Current solver instance, pointing to cvc4. sbvCurrentSolver :: SMTConfig@@ -50,6 +50,12 @@     => a                -- ^ Property to check     -> IO SatResult     -- ^ Response of the SMT Solver, containing the model if found sat = satWith sbvCurrentSolver++-- | Check all 'sAssert' calls are safe, using the CVC4 SMT solver+safe :: SExecutable a+    => a                -- ^ Program containing sAssert calls+    -> IO [SafeResult]+safe = safeWith sbvCurrentSolver  -- | Find all satisfying solutions, using the CVC4 SMT solver allSat :: Provable a
Data/SBV/Bridge/MathSAT.hs view
@@ -25,7 +25,7 @@   -- * MathSAT specific interface   sbvCurrentSolver   -- ** Proving, checking satisfiability-  , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable+  , prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable   -- ** Optimization routines   , optimize, minimize, maximize   -- * Non-MathSAT specific SBV interface@@ -33,51 +33,57 @@   , module Data.SBV   ) where -import Data.SBV hiding (prove, sat, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)+import Data.SBV hiding (prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver) --- | Current solver instance, pointing to cvc4.+-- | Current solver instance, pointing to MathSAT. sbvCurrentSolver :: SMTConfig sbvCurrentSolver = mathSAT --- | Prove theorems, using the CVC4 SMT solver+-- | Prove theorems, using the MathSAT SMT solver prove :: Provable a       => a              -- ^ Property to check       -> IO ThmResult   -- ^ Response from the SMT solver, containing the counter-example if found prove = proveWith sbvCurrentSolver --- | Find satisfying solutions, using the CVC4 SMT solver+-- | Find satisfying solutions, using the MathSAT SMT solver sat :: Provable a     => a                -- ^ Property to check     -> IO SatResult     -- ^ Response of the SMT Solver, containing the model if found sat = satWith sbvCurrentSolver --- | Find all satisfying solutions, using the CVC4 SMT solver+-- | Check all 'sAssert' calls are safe, using the MathSAT SMT solver+safe :: SExecutable a+    => a                -- ^ Program containing sAssert calls+    -> IO [SafeResult]+safe = safeWith sbvCurrentSolver++-- | Find all satisfying solutions, using the MathSAT SMT solver allSat :: Provable a        => a                -- ^ Property to check        -> IO AllSatResult  -- ^ List of all satisfying models allSat = allSatWith sbvCurrentSolver --- | Check vacuity of the explicit constraints introduced by calls to the 'constrain' function, using the CVC4 SMT solver+-- | Check vacuity of the explicit constraints introduced by calls to the 'constrain' function, using the MathSAT SMT solver isVacuous :: Provable a           => a             -- ^ Property to check           -> IO Bool       -- ^ True if the constraints are unsatisifiable isVacuous = isVacuousWith sbvCurrentSolver --- | Check if the statement is a theorem, with an optional time-out in seconds, using the CVC4 SMT solver+-- | Check if the statement is a theorem, with an optional time-out in seconds, using the MathSAT SMT solver isTheorem :: Provable a           => Maybe Int          -- ^ Optional time-out, specify in seconds           -> a                  -- ^ Property to check           -> IO (Maybe Bool)    -- ^ Returns Nothing if time-out expires isTheorem = isTheoremWith sbvCurrentSolver --- | Check if the statement is satisfiable, with an optional time-out in seconds, using the CVC4 SMT solver+-- | Check if the statement is satisfiable, with an optional time-out in seconds, using the MathSAT SMT solver isSatisfiable :: Provable a               => Maybe Int       -- ^ Optional time-out, specify in seconds               -> a               -- ^ Property to check               -> IO (Maybe Bool) -- ^ Returns Nothing if time-out expiers isSatisfiable = isSatisfiableWith sbvCurrentSolver --- | Optimize cost functions, using the CVC4 SMT solver+-- | Optimize cost functions, using the MathSAT SMT solver optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)          => OptimizeOpts                -- ^ Parameters to optimization (Iterative, Quantified, etc.)          -> (SBV c -> SBV c -> SBool)   -- ^ Betterness check: This is the comparison predicate for optimization@@ -87,7 +93,7 @@          -> IO (Maybe [a])              -- ^ Returns Nothing if there is no valid solution, otherwise an optimal solution optimize = optimizeWith sbvCurrentSolver --- | Minimize cost functions, using the CVC4 SMT solver+-- | Minimize cost functions, using the MathSAT SMT solver minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)          => OptimizeOpts                -- ^ Parameters to optimization (Iterative, Quantified, etc.)          -> ([SBV a] -> SBV c)          -- ^ Cost function to minimize@@ -96,7 +102,7 @@          -> IO (Maybe [a])              -- ^ Returns Nothing if there is no valid solution, otherwise an optimal solution minimize = minimizeWith sbvCurrentSolver --- | Maximize cost functions, using the CVC4 SMT solver+-- | Maximize cost functions, using the MathSAT SMT solver maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)          => OptimizeOpts                -- ^ Parameters to optimization (Iterative, Quantified, etc.)          -> ([SBV a] -> SBV c)          -- ^ Cost function to maximize
Data/SBV/Bridge/Yices.hs view
@@ -25,7 +25,7 @@   -- * Yices specific interface   sbvCurrentSolver   -- ** Proving, checking satisfiability-  , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable+  , prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable   -- ** Optimization routines   , optimize, minimize, maximize   -- * Non-Yices specific SBV interface@@ -33,7 +33,7 @@   , module Data.SBV   ) where -import Data.SBV hiding (prove, sat, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)+import Data.SBV hiding (prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)  -- | Current solver instance, pointing to yices. sbvCurrentSolver :: SMTConfig@@ -50,6 +50,12 @@     => a                -- ^ Property to check     -> IO SatResult     -- ^ Response of the SMT Solver, containing the model if found sat = satWith sbvCurrentSolver++-- | Check all 'sAssert' calls are safe, using the Yices SMT solver+safe :: SExecutable a+    => a                -- ^ Program containing sAssert calls+    -> IO [SafeResult]+safe = safeWith sbvCurrentSolver  -- | Find all satisfying solutions, using the Yices SMT solver allSat :: Provable a
Data/SBV/Bridge/Z3.hs view
@@ -25,7 +25,7 @@   -- * Z3 specific interface   sbvCurrentSolver   -- ** Proving, checking satisfiability-  , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable+  , prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable   -- ** Optimization routines   , optimize, minimize, maximize   -- * Non-Z3 specific SBV interface@@ -33,7 +33,7 @@   , module Data.SBV   ) where -import Data.SBV hiding (prove, sat, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)+import Data.SBV hiding (prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)  -- | Current solver instance, pointing to z3. sbvCurrentSolver :: SMTConfig@@ -50,6 +50,12 @@     => a                -- ^ Property to check     -> IO SatResult     -- ^ Response of the SMT Solver, containing the model if found sat = satWith sbvCurrentSolver++-- | Check all 'sAssert' calls are safe, using the Z3 SMT solver+safe :: SExecutable a+    => a                -- ^ Program containing sAssert calls+    -> IO [SafeResult]+safe = safeWith sbvCurrentSolver  -- | Find all satisfying solutions, using the Z3 SMT solver allSat :: Provable a
Data/SBV/Compilers/C.hs view
@@ -27,6 +27,9 @@ import Data.SBV.BitVectors.PrettyNum (shex, showCFloat, showCDouble) import Data.SBV.Compilers.CodeGen +import GHC.Stack+import GHC.SrcLoc+ --------------------------------------------------------------------------- -- * API ---------------------------------------------------------------------------@@ -270,6 +273,8 @@   $$ text "#ifndef" <+> tag   $$ text "#define" <+> tag   $$ text ""+  $$ text "#include <stdio.h>"+  $$ text "#include <stdlib.h>"   $$ text "#include <inttypes.h>"   $$ text "#include <stdint.h>"   $$ text "#include <stdbool.h>"@@ -399,7 +404,7 @@  -- | Generate the C program genCProg :: CgConfig -> String -> Doc -> Result -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> Doc -> [Doc]-genCProg cfg fn proto (Result kindInfo _tvals cgs ins preConsts tbls arrs _ _ (SBVPgm asgns) cstrs _) inVars outVars mbRet extDecls+genCProg cfg fn proto (Result kindInfo _tvals cgs ins preConsts tbls arrs _ _ (SBVPgm asgns) cstrs origAsserts _) inVars outVars mbRet extDecls   | isNothing (cgInteger cfg) && KUnbounded `Set.member` kindInfo   = error $ "SBV->C: Unbounded integers are not supported by the C compiler."           ++ "\nUse 'cgIntegerSize' to specify a fixed size for SInteger representation."@@ -416,7 +421,9 @@   = error "SBV->C: Cannot compile functions with existentially quantified variables."   | True   = [pre, header, post]- where usorts = [s | KUserSort s _ <- Set.toList kindInfo, s /= "RoundingMode"] -- No support for any sorts other than RoundingMode!+ where asserts | cgIgnoreAsserts cfg = []+               | True                = origAsserts+       usorts = [s | KUserSort s _ <- Set.toList kindInfo, s /= "RoundingMode"] -- No support for any sorts other than RoundingMode!        pre    =  text "/* File:" <+> doubleQuotes (nm <> text ".c") <> text ". Automatically generated by SBV. Do not edit! */"               $$ text ""        header = text "#include" <+> doubleQuotes (nm <> text ".h")@@ -427,7 +434,7 @@              $$ text "{"              $$ text ""              $$ nest 2 (   vcat (concatMap (genIO True . (\v -> (isAlive v, v))) inVars)-                        $$ vcat (merge (map genTbl tbls) (map genAsgn assignments))+                        $$ vcat (merge (map genTbl tbls) (map genAsgn assignments) (map genAssert asserts))                         $$ sepIf (not (null assignments) || not (null tbls))                         $$ vcat (concatMap (genIO False) (zip (repeat True) outVars))                         $$ maybe empty mkRet mbRet@@ -486,14 +493,30 @@        genAsgn :: (SW, SBVExpr) -> (Int, Doc)        genAsgn (sw, n) = (getNodeId sw, ppExpr cfg consts n (declSW typeWidth sw) (declSWNoConst typeWidth sw) <> 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]-       merge []               as                  = map snd as-       merge ts               []                  = map snd ts-       merge ts@((i, t):trest) as@((i', a):arest)-         | i < i'                                 = t : merge trest as-         | True                                   = a : merge ts arest+       -- merge tables intermixed with assignments and assertions, paying attention to putting tables as+       -- early as possible and tables right after.. Note that the assignment list (second argument) is sorted on its order+       merge :: [(Int, Doc)] -> [(Int, Doc)] -> [(Int, Doc)] -> [Doc]+       merge tables asgnments asrts = map snd $ merge2 asrts (merge2 tables asgnments)+         where merge2 []               as                  = as+               merge2 ts               []                  = ts+               merge2 ts@((i, t):trest) as@((i', a):arest)+                 | i < i'                                 = (i,  t)  : merge2 trest as+                 | True                                   = (i', a) : merge2 ts arest+       genAssert (msg, cs, sw) = (getNodeId sw, doc)+         where doc =     text "/* ASSERTION:" <+> text msg+                     $$  maybe empty (vcat . map text) (locInfo (getCallStack `fmap` cs))+                     $$  text " */"+                     $$  text "if" <> parens (showSW cfg consts sw)+                     $$  text "{"+                     $+$ nest 2 (vcat [errOut, text "exit(-1);"])+                     $$  text "}"+                     $$  text ""+               errOut = text $ "fprintf(stderr, \"%s:%d:ASSERTION FAILED: " ++ msg ++ "\\n\", __FILE__, __LINE__);"+               locInfo (Just ps) = let loc (f, sl) = concat [srcLocFile sl, ":", show (srcLocStartLine sl), ":", show (srcLocStartCol sl), ":", f ]+                                   in case map loc ps of+                                         []     -> Nothing+                                         (f:rs) -> Just $ (" * SOURCE   : " ++ f) : map (" *            " ++)  rs+               locInfo _         = Nothing  handleIEEE :: FPOp -> [(SW, CW)] -> [(SW, Doc)] -> Doc -> Doc handleIEEE w consts as var = cvt w
Data/SBV/Compilers/CodeGen.hs view
@@ -38,17 +38,25 @@  -- | 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)-        , 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+          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+        , cgIgnoreAsserts :: Bool               -- ^ If 'True', will ignore 'sAssert' calls         }  -- | 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, cgReal = Nothing, cgDriverVals = [], cgGenDriver = True, cgGenMakefile = True }+defaultCgConfig = CgConfig { cgRTC           = False+                           , cgInteger       = Nothing+                           , cgReal          = Nothing+                           , cgDriverVals    = []+                           , cgGenDriver     = True+                           , cgGenMakefile   = True+                           , cgIgnoreAsserts = False+                           }  -- | Abstraction of target language values data CgVal = CgAtomic SW@@ -68,13 +76,13 @@ -- | Initial configuration for code-generation initCgState :: CgState initCgState = CgState {-          cgInputs       = []-        , cgOutputs      = []-        , cgReturns      = []-        , cgPrototypes   = []-        , cgDecls        = []-        , cgLDFlags      = []-        , cgFinalConfig  = defaultCgConfig+          cgInputs        = []+        , cgOutputs       = []+        , cgReturns       = []+        , cgPrototypes    = []+        , cgDecls         = []+        , cgLDFlags       = []+        , cgFinalConfig   = defaultCgConfig         }  -- | The code-generation monad. Allows for precise layout of input values@@ -141,6 +149,10 @@ -- | Sets driver program run time values, useful for generating programs with fixed drivers for testing. Default: None, i.e., use random values. cgSetDriverValues :: [Integer] -> SBVCodeGen () cgSetDriverValues vs = modify (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgDriverVals = vs } })++-- | Ignore assertions (those generated by 'sAssert' calls) in the generated C code+cgIgnoreSAssert :: Bool -> SBVCodeGen ()+cgIgnoreSAssert b = modify (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgIgnoreAsserts = b } })  -- | Adds the given lines to the header file generated, useful for generating programs with uninterpreted functions. cgAddPrototype :: [String] -> SBVCodeGen ()
Data/SBV/Dynamic.hs view
@@ -63,12 +63,14 @@   , proveWith   -- ** Checking satisfiability   , satWith, allSatWith+  -- ** Checking safety+  , safeWith   -- * Proving properties using multiple solvers   , proveWithAll, proveWithAny, satWithAll, satWithAny   -- * Model extraction    -- ** Inspecting proof results-  , ThmResult(..), SatResult(..), AllSatResult(..), SMTResult(..)+  , ThmResult(..), SatResult(..), SafeResult(..), AllSatResult(..), SMTResult(..)    -- ** Programmable model extraction   , genParse, getModel, getModelDictionary@@ -76,7 +78,7 @@   , SMTConfig(..), SMTLibVersion(..), SMTLibLogic(..), Logic(..), OptimizeOpts(..), Solver(..), SMTSolver(..), boolector, cvc4, yices, z3, mathSAT, abc, defaultSolverConfig, sbvCurrentSolver, defaultSMTCfg, sbvCheckSolverInstallation, sbvAvailableSolvers    -- * Symbolic computations-  , outputSVal{-, SymWord(..)-}+  , outputSVal    -- * Getting SMT-Lib output (for offline analysis)   , compileToSMTLib, generateSMTBenchmarks@@ -96,7 +98,7 @@   , svCgReturn, svCgReturnArr    -- ** Code generation with uninterpreted functions-  , cgAddPrototype, cgAddDecl, cgAddLDFlags+  , cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert    -- ** Code generation with 'SInteger' and 'SReal' types   , cgIntegerSize, cgSRealType, CgSRealType(..)@@ -118,19 +120,19 @@   , svCgOutput, svCgOutputArr   , svCgReturn, svCgReturnArr   , cgPerformRTCs, cgSetDriverValues, cgGenerateDriver, cgGenerateMakefile-  , cgAddPrototype, cgAddDecl, cgAddLDFlags+  , cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert   , cgIntegerSize, cgSRealType, CgSRealType(..)   ) import Data.SBV.Compilers.C    (compileToC, compileToCLib) import Data.SBV.Provers.Prover (boolector, cvc4, yices, z3, mathSAT, abc, defaultSMTCfg)-import Data.SBV.SMT.SMT        (ThmResult(..), SatResult(..), AllSatResult(..), genParse)+import Data.SBV.SMT.SMT        (ThmResult(..), SatResult(..), SafeResult(..), AllSatResult(..), genParse) import Data.SBV.Tools.Optimize (OptimizeOpts(..)) import Data.SBV                (sbvCurrentSolver, sbvCheckSolverInstallation, defaultSolverConfig, sbvAvailableSolvers)  import qualified Data.SBV                  as SBV (SBool, proveWithAll, proveWithAny, satWithAll, satWithAny) import qualified Data.SBV.BitVectors.Data  as SBV (SBV(..)) import qualified Data.SBV.BitVectors.Model as SBV (isSatisfiableInCurrentPath)-import qualified Data.SBV.Provers.Prover   as SBV (proveWith, satWith, allSatWith, compileToSMTLib, generateSMTBenchmarks)+import qualified Data.SBV.Provers.Prover   as SBV (proveWith, satWith, safeWith, allSatWith, compileToSMTLib, generateSMTBenchmarks) import qualified Data.SBV.SMT.SMT          as SBV (Modelable(getModel, getModelDictionary))  -- | Reduce a condition (i.e., try to concretize it) under the given path@@ -170,6 +172,10 @@ -- | Find a satisfying assignment using the given SMT-solver satWith :: SMTConfig -> Symbolic SVal -> IO SatResult satWith cfg s = SBV.satWith cfg (fmap toSBool s)++-- | Check safety using the given SMT-solver+safeWith :: SMTConfig -> Symbolic SVal -> IO [SafeResult]+safeWith cfg s = SBV.safeWith cfg (fmap toSBool s)  -- | Find all satisfying assignments using the given SMT-solver allSatWith :: SMTConfig -> Symbolic SVal -> IO AllSatResult
Data/SBV/Examples/BitPrecise/PrefixSum.hs view
@@ -130,6 +130,7 @@ --   s17 :: SWord8 = s13 + s16 --   s18 :: SWord8 = s11 + s17 -- CONSTRAINTS+-- ASSERTIONS -- OUTPUTS --   s0 --   s8@@ -174,6 +175,7 @@ --   s13 :: SWord8 = s6 + s12 --   s14 :: SWord8 = s7 + s13 -- CONSTRAINTS+-- ASSERTIONS -- OUTPUTS --   s0 --   s8
Data/SBV/Examples/CodeGeneration/AddSub.hs view
@@ -52,6 +52,8 @@ -- #ifndef __addSub__HEADER_INCLUDED__ -- #define __addSub__HEADER_INCLUDED__ -- <BLANKLINE>+-- #include <stdio.h>+-- #include <stdlib.h> -- #include <inttypes.h> -- #include <stdint.h> -- #include <stdbool.h>
Data/SBV/Examples/CodeGeneration/GCD.hs view
@@ -78,6 +78,8 @@ -- -- > /* File: "sgcd.c". Automatically generated by SBV. Do not edit! */ -- > +-- > #include <stdio.h>+-- > #include <stdlib.h> -- > #include <inttypes.h> -- > #include <stdint.h> -- > #include <stdbool.h>
Data/SBV/Examples/CodeGeneration/PopulationCount.hs view
@@ -114,6 +114,8 @@ -- #ifndef __popCount__HEADER_INCLUDED__ -- #define __popCount__HEADER_INCLUDED__ -- <BLANKLINE>+-- #include <stdio.h>+-- #include <stdlib.h> -- #include <inttypes.h> -- #include <stdint.h> -- #include <stdbool.h>
Data/SBV/Examples/Misc/Floating.hs view
@@ -145,22 +145,23 @@ -- -- >>> roundingAdd -- Satisfiable. Model:---   rm = RoundNearestTiesToAway :: RoundingMode---   x  = 2.0644195e19 :: Float---   y  = -2.1974389e18 :: Float+--   rm = RoundTowardZero :: RoundingMode+--   x  = 7.984373 :: Float+--   y  = -2.1684042e-19 :: Float --+-- (Note that depending on your version of Z3, you might get a different result.) -- Unfortunately we can't directly validate this result at the Haskell level, as Haskell only supports -- 'RoundNearestTiesToEven'. We have: ----- >>> (2.0644195e19 + (-2.1974389e18)) :: Float--- 1.8446757e19+-- >>> (7.984373 + (-2.1684042e-19)) :: Float+-- 7.984373 ----- While we cannot directly see the result when the mode is 'RoundNearestTiesToAway' in Haskell, we can use+-- While we cannot directly see the result when the mode is 'RoundTowardZero' in Haskell, we can use -- SBV to provide us with that result thusly: ----- >>> sat $ \z -> z .== fpAdd sRoundNearestTiesToAway 2.0644195e19 (-2.1974389e18 :: SFloat)+-- >>> sat $ \z -> z .== fpAdd sRoundTowardZero 7.984373 (-2.1684042e-19 :: SFloat) -- Satisfiable. Model:---   s0 = 1.8446755e19 :: Float+--   s0 = 7.9843726 :: Float -- -- We can see why these two resuls are indeed different. To see why, one would have to convert the -- individual numbers to Float's, which would induce rounding-errors, add them up, and round-back;
+ Data/SBV/Examples/Misc/NoDiv0.hs view
@@ -0,0 +1,46 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.Examples.Misc.NoDiv0+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+--+-- Demonstrates SBV's assertion checking facilities+-----------------------------------------------------------------------------++{-# LANGUAGE ImplicitParams #-}++module Data.SBV.Examples.Misc.NoDiv0 where++import Data.SBV+import GHC.Stack++-- | A simple variant of division, where we explicitly require the+-- caller to make sure the divisor is not 0.+checkedDiv :: (?loc :: CallStack) => SInt32 -> SInt32 -> SInt32+checkedDiv x y = sAssert (Just ?loc)+                         "Divisor should not be 0"+                         (y ./= 0)+                         (x `sDiv` y)++-- | Check whether an arbitrary call to 'checkedDiv' is safe. Clearly, we do not expect+-- this to be safe:+--+-- >>> test1+-- [Data/SBV/Examples/Misc/NoDiv0.hs:22:32:?loc,+--  Data/SBV/Examples/Misc/NoDiv0.hs:37:14:checkedDiv: Divisor should not be 0: Violated. Model:+--   s0 = 0 :: Int32+--   s1 = 0 :: Int32]+--+test1 :: IO [SafeResult]+test1 = safe checkedDiv++-- | Repeat the test, except this time we explicitly protect against the bad case. We have:+--+-- >>> test2+-- [Data/SBV/Examples/Misc/NoDiv0.hs:22:32:?loc,+--  Data/SBV/Examples/Misc/NoDiv0.hs:46:41:checkedDiv: Divisor should not be 0: No violations detected]+--+test2 :: IO [SafeResult]+test2 = safe $ \x y -> ite (y .== 0) 3 (checkedDiv x y)
Data/SBV/Examples/Puzzles/U2Bridge.hs view
@@ -241,16 +241,16 @@ -- Checking for solutions with 5 moves. -- Solution #1:  --  0 --> Edge, Bono---  2 <-- Edge---  4 --> Larry, Adam--- 14 <-- Bono+--  2 <-- Bono+--  3 --> Larry, Adam+-- 13 <-- Edge -- 15 --> Edge, Bono -- Total time: 17 -- Solution #2:  --  0 --> Edge, Bono---  2 <-- Bono---  3 --> Larry, Adam--- 13 <-- Edge+--  2 <-- Edge+--  4 --> Larry, Adam+-- 14 <-- Bono -- 15 --> Edge, Bono -- Total time: 17 -- Found: 2 solutions with 5 moves.
Data/SBV/Provers/Prover.hs view
@@ -17,10 +17,11 @@  module Data.SBV.Provers.Prover (          SMTSolver(..), SMTConfig(..), Predicate, Provable(..)-       , ThmResult(..), SatResult(..), AllSatResult(..), SMTResult(..)+       , ThmResult(..), SatResult(..), SafeResult(..), AllSatResult(..), SMTResult(..)        , isSatisfiable, isSatisfiableWith, isTheorem, isTheoremWith        , prove, proveWith        , sat, satWith+       , safe, safeWith, isSafe        , allSat, allSatWith        , isVacuous, isVacuousWith        , SatModel(..), Modelable(..), displayModels, extractModels@@ -36,6 +37,9 @@ import System.Time      (getClockTime) import System.IO.Unsafe (unsafeInterleaveIO) +import GHC.Stack+import GHC.SrcLoc+ import qualified Data.Set as Set (Set, toList)  import Data.SBV.BitVectors.Data@@ -245,6 +249,10 @@ sat :: Provable a => a -> IO SatResult sat = satWith defaultSMTCfg +-- | Check that all the 'sAssert' calls are safe, equivalent to @'safeWith' 'defaultSMTCfg'@+safe :: SExecutable a => a -> IO [SafeResult]+safe = safeWith defaultSMTCfg+ -- | Return all satisfying assignments for a predicate, equivalent to @'allSatWith' 'defaultSMTCfg'@. -- Satisfying assignments are constructed lazily, so they will be available as returned by the solver -- and on demand.@@ -311,7 +319,7 @@         let comments = ["Created on " ++ show t]             cvt = case version of                     SMTLib2 -> toSMTLib2-        (_, _, _, smtLibPgm) <- simulate cvt defaultSMTCfg isSat comments a+        (_, _, _, _, smtLibPgm) <- simulate cvt defaultSMTCfg isSat comments a         let out = show smtLibPgm         return $ out ++ "\n(check-sat)\n" @@ -338,14 +346,39 @@   where cvt = case smtLibVersion config of                 SMTLib2 -> toSMTLib2 +-- | Check if any of the assertions can be violated+safeWith :: SExecutable a => SMTConfig -> a -> IO [SafeResult]+safeWith cfg a = do+        res@Result{resAssertions=asserts} <- runSymbolic (True, cfg) $ sName_ a >>= output+        mapM (verify res) asserts+  where locInfo (Just ps) = Just $ let loc (f, sl) = concat [srcLocFile sl, ":", show (srcLocStartLine sl), ":", show (srcLocStartCol sl), ":", f]+                                   in intercalate ",\n " (map loc ps)+        locInfo _         = Nothing+        verify res (msg, cs, cond) = do SatResult result <- runProofOn cvt cfg True [] pgm >>= callSolver True msg SatResult cfg+                                        return $ SafeResult (locInfo (getCallStack `fmap` cs), msg, result)+           where pgm = res { resInputs  = [(EX, n) | (_, n) <- resInputs res]   -- make everything existential+                           , resOutputs = [cond]+                           }+                 cvt = case smtLibVersion cfg of+                         SMTLib2 -> toSMTLib2++-- | Check if a safe-call was safe or not, turning a 'SafeResult' to a Bool.+isSafe :: SafeResult -> Bool+isSafe (SafeResult (_, _, result)) = case result of+                                       Unsatisfiable{} -> True+                                       Satisfiable{}   -> False+                                       Unknown{}       -> False   -- conservative+                                       ProofError{}    -> False   -- conservative+                                       TimeOut{}       -> False   -- conservative+ -- | Determine if the constraints are vacuous using the given SMT-solver isVacuousWith :: Provable a => SMTConfig -> a -> IO Bool isVacuousWith config a = do-        Result ki tr uic is cs ts as uis ax asgn cstr _ <- runSymbolic (True, config) $ forAll_ a >>= output+        Result ki tr uic is cs ts as uis ax asgn cstr asserts _ <- runSymbolic (True, config) $ 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 ki tr uic is' cs ts as uis ax asgn cstr [trueSW]+                        res' = Result ki tr uic is' cs ts as uis ax asgn cstr asserts [trueSW]                         cvt  = case smtLibVersion config of                                  SMTLib2 -> toSMTLib2                     SatResult result <- runProofOn cvt config True [] res' >>= callSolver True "Checking Satisfiability.." SatResult config@@ -362,7 +395,7 @@         let converter  = case smtLibVersion config of                            SMTLib2 -> toSMTLib2         msg "Checking Satisfiability, all solutions.."-        sbvPgm@(qinps, _, ki, _) <- simulate converter config True [] p+        sbvPgm@(qinps, _, ki, _, _) <- simulate converter config True [] p         let usorts = [s | us@(KUserSort s _) <- Set.toList ki, isFree us]                 where isFree (KUserSort _ (Left _, _)) = True                       isFree _                         = False@@ -389,7 +422,7 @@                                                Unsatisfiable _               -> return []                                                Satisfiable   _ model         -> cont model                                                Unknown       _ model         -> cont model-        invoke nonEqConsts n (qinps, skolemMap, _, smtLibPgm) = do+        invoke nonEqConsts n (qinps, skolemMap, _, _, smtLibPgm) = do                msg $ "Looking for solution " ++ show n                case addNonEqConstraints (roundingMode config) qinps nonEqConsts smtLibPgm of                  Nothing ->  -- no new constraints added, stop@@ -401,14 +434,15 @@         updateName i cfg = cfg{smtFile = upd `fmap` smtFile cfg}                where upd nm = let (b, e) = splitExtension nm in b ++ "_allSat_" ++ show i ++ e -type SMTProblem = ( [(Quantifier, NamedSymVar)]         -- inputs-                  , [Either SW (SW, [SW])]              -- skolem-map-                  , Set.Set Kind                        -- kinds used-                  , SMTLibPgm                           -- SMTLib representation+type SMTProblem = ( [(Quantifier, NamedSymVar)]      -- inputs+                  , [Either SW (SW, [SW])]           -- skolem-map+                  , Set.Set Kind                     -- kinds used+                  , [(String, Maybe CallStack, SW)]  -- assertions+                  , SMTLibPgm                        -- SMTLib representation                   )  callSolver :: Bool -> String -> (SMTResult -> b) -> SMTConfig -> SMTProblem -> IO b-callSolver isSat checkMsg wrap config (qinps, skolemMap, _, smtLibPgm) = do+callSolver isSat checkMsg wrap config (qinps, skolemMap, _, _, smtLibPgm) = do        let msg = when (verbose config) . putStrLn . ("** " ++)        msg checkMsg        let finalPgm = intercalate "\n" (pre ++ post) where SMTLibPgm _ (_, pre, post) = smtLibPgm@@ -432,7 +466,7 @@         let isTiming   = timing config             solverCaps = capabilities (solver config)         in case res of-             Result ki _qcInfo _codeSegs is consts tbls arrs uis axs pgm cstrs [o@(SW KBool _)] ->+             Result ki _qcInfo _codeSegs is consts tbls arrs uis axs pgm cstrs assertions [o@(SW KBool _)] ->                timeIf isTiming "translation"                 $ let skolemMap = skolemize (if isSat then is else map flipQ is)                            where flipQ (ALL, x) = (EX, x)@@ -442,8 +476,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, skolemMap, ki, converter (roundingMode config) (useLogic config) solverCaps ki isSat comments is skolemMap consts tbls arrs uis axs pgm cstrs o)-             Result _kindInfo _qcInfo _codeSegs _is _consts _tbls _arrs _uis _axs _pgm _cstrs os -> case length os of+                  in return (is, skolemMap, ki, assertions, converter (roundingMode config) (useLogic config) solverCaps ki isSat comments is skolemMap consts tbls arrs uis axs pgm cstrs o)+             Result{resOutputs = 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@@ -456,11 +490,11 @@ internalSATCheck cfg condInPath st msg = do    sw <- sbvToSW st condInPath    () <- forceSWArg sw-   Result ki tr uic is cs ts as uis ax asgn cstr _ <- extractSymbolicSimulationState st+   Result ki tr uic is cs ts as uis ax asgn cstr assertions _ <- extractSymbolicSimulationState st    let -- Construct the corresponding sat-checker for the branch. Note that we need to        -- forget about the quantifiers and just use an "exist", as we're looking for a        -- point-satisfiability check here; whatever the original program was.-       pgm = Result ki tr uic [(EX, n) | (_, n) <- is] cs ts as uis ax asgn cstr [sw]+       pgm = Result ki tr uic [(EX, n) | (_, n) <- is] cs ts as uis ax asgn cstr assertions [sw]        cvt = case smtLibVersion cfg of                 SMTLib2 -> toSMTLib2    runProofOn cvt cfg True [] pgm >>= callSolver True msg SatResult cfg
Data/SBV/SMT/SMT.hs view
@@ -55,6 +55,9 @@ -- The reason for having a separate 'SatResult' is to have a more meaningful 'Show' instance. newtype SatResult    = SatResult    SMTResult +-- | A 'safe' call results in a 'SafeResult'+newtype SafeResult   = SafeResult   (Maybe String, String, SMTResult)+ -- | An 'allSat' call results in a 'AllSatResult'. The boolean says whether -- we should warn the user about prefix-existentials. newtype AllSatResult = AllSatResult (Bool, [SMTResult])@@ -70,6 +73,14 @@   show (SatResult r) = showSMTResult "Unsatisfiable"                                      "Unknown"     "Unknown. Potential model:\n"                                      "Satisfiable" "Satisfiable. Model:\n" r++-- | User friendly way of printing safety results+instance Show SafeResult where+   show (SafeResult (mbLoc, msg, r)) = showSMTResult (tag "No violations detected")+                                                     (tag "Unknown")  (tag "Unknown. Potential violating model:\n")+                                                     (tag "Violated") (tag "Violated. Model:\n") r+        where loc   = maybe "" (++ ": ") mbLoc+              tag s = loc ++ msg ++ ": " ++ s  -- | The Show instance of AllSatResults. Note that we have to be careful in being lazy enough -- as the typical use case is to pull results out as they become available.
Data/SBV/SMT/SMTLib.hs view
@@ -16,26 +16,25 @@ import Data.SBV.BitVectors.Data import Data.SBV.Provers.SExpr import qualified Data.SBV.SMT.SMTLib2 as SMT2- import qualified Data.Set as Set (Set, member, toList)  -- | An instance of SMT-Lib converter; instantiated for SMT-Lib v1 and v2. (And potentially for newer versions in the future.)-type SMTLibConverter =  RoundingMode                -- ^ User selected rounding mode to be used for floating point arithmetic-                     -> Maybe Logic                 -- ^ User selected logic to use. If Nothing, pick automatically.-                     -> SolverCapabilities          -- ^ Capabilities of the backend solver targeted-                     -> Set.Set Kind                -- ^ Kinds used in the problem-                     -> Bool                        -- ^ is this a sat problem?-                     -> [String]                    -- ^ extra comments to place on top-                     -> [(Quantifier, NamedSymVar)] -- ^ inputs and aliasing names-                     -> [Either SW (SW, [SW])]      -- ^ skolemized inputs-                     -> [(SW, CW)]                  -- ^ constants-                     -> [((Int, Kind, Kind), [SW])] -- ^ auto-generated tables-                     -> [(Int, ArrayInfo)]          -- ^ user specified arrays-                     -> [(String, SBVType)]         -- ^ uninterpreted functions/constants-                     -> [(String, [String])]        -- ^ user given axioms-                     -> SBVPgm                      -- ^ assignments-                     -> [SW]                        -- ^ extra constraints-                     -> SW                          -- ^ output variable+type SMTLibConverter =  RoundingMode                 -- ^ User selected rounding mode to be used for floating point arithmetic+                     -> Maybe Logic                  -- ^ User selected logic to use. If Nothing, pick automatically.+                     -> SolverCapabilities           -- ^ Capabilities of the backend solver targeted+                     -> Set.Set Kind                 -- ^ Kinds used in the problem+                     -> Bool                         -- ^ is this a sat problem?+                     -> [String]                     -- ^ extra comments to place on top+                     -> [(Quantifier, NamedSymVar)]  -- ^ inputs and aliasing names+                     -> [Either SW (SW, [SW])]       -- ^ skolemized inputs+                     -> [(SW, CW)]                   -- ^ constants+                     -> [((Int, Kind, Kind), [SW])]  -- ^ auto-generated tables+                     -> [(Int, ArrayInfo)]           -- ^ user specified arrays+                     -> [(String, SBVType)]          -- ^ uninterpreted functions/constants+                     -> [(String, [String])]         -- ^ user given axioms+                     -> SBVPgm                       -- ^ assignments+                     -> [SW]                         -- ^ extra constraints+                     -> SW                           -- ^ output variable                      -> SMTLibPgm  -- | Convert to SMTLib-2 format
Data/SBV/Tools/ExpectedValue.hs view
@@ -38,7 +38,7 @@                         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
Data/SBV/Tools/GenTest.hs view
@@ -42,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
README.md view
@@ -1,22 +1,6 @@--<table>-  <tr>-    <th>Travis Build</th><th>Hackage</th>-  </tr>-  <tr>-   -    <td>-       <a href="https://secure.travis-ci.org/LeventErkok/sbv"><img src="https://secure.travis-ci.org/LeventErkok/sbv.png?branch=master"></img></a>-    </td>-    -    <td>-       <a href="http://hackage.haskell.org/package/sbv"><img src="https://budueba.com/hackage/sbv"></img></a>-    </td>-   -  </tr>-</table>+## SBV: SMT Based Verification in Haskell -SBV: SMT Based Verification in Haskell-======================================+[![Hackage version](http://img.shields.io/hackage/v/sbv.svg?label=Hackage)](http://hackage.haskell.org/package/sbv)+    [![Build Status](http://img.shields.io/travis/LeventErkok/sbv.svg?label=Build)](http://travis-ci.org/LeventErkok/sbv)  Please see: http://leventerkok.github.com/sbv/
SBVUnitTest/GoldFiles/U2Bridge.gold view
@@ -3,13 +3,13 @@   s1  = Edge :: U2Member   s2  = Bono :: U2Member   s3  = True-  s4  = Edge :: U2Member+  s4  = Bono :: U2Member   s5  = Bono :: U2Member   s6  = False   s7  = Larry :: U2Member   s8  = Adam :: U2Member   s9  = True-  s10 = Bono :: U2Member+  s10 = Edge :: U2Member   s11 = Bono :: U2Member   s12 = False   s13 = Edge :: U2Member
SBVUnitTest/GoldFiles/addSub.gold view
@@ -30,6 +30,8 @@ #ifndef __addSub__HEADER_INCLUDED__ #define __addSub__HEADER_INCLUDED__ +#include <stdio.h>+#include <stdlib.h> #include <inttypes.h> #include <stdint.h> #include <stdbool.h>
SBVUnitTest/GoldFiles/aes128Dec.gold view
@@ -30,6 +30,8 @@ #ifndef __aes128Dec__HEADER_INCLUDED__ #define __aes128Dec__HEADER_INCLUDED__ +#include <stdio.h>+#include <stdlib.h> #include <inttypes.h> #include <stdint.h> #include <stdbool.h>
SBVUnitTest/GoldFiles/aes128Enc.gold view
@@ -30,6 +30,8 @@ #ifndef __aes128Enc__HEADER_INCLUDED__ #define __aes128Enc__HEADER_INCLUDED__ +#include <stdio.h>+#include <stdlib.h> #include <inttypes.h> #include <stdint.h> #include <stdbool.h>
SBVUnitTest/GoldFiles/aes128Lib.gold view
@@ -3565,6 +3565,8 @@ #ifndef __aes128Lib__HEADER_INCLUDED__ #define __aes128Lib__HEADER_INCLUDED__ +#include <stdio.h>+#include <stdlib.h> #include <inttypes.h> #include <stdint.h> #include <stdbool.h>
SBVUnitTest/GoldFiles/auf-1.gold view
@@ -28,5 +28,6 @@   s16 :: SBool = s11 == s15   s17 :: SBool = s6 | s16 CONSTRAINTS+ASSERTIONS OUTPUTS   s17
SBVUnitTest/GoldFiles/basic-2_1.gold view
@@ -14,5 +14,6 @@   s3 :: SWord8 = s1 - s0   s4 :: SWord8 = s2 * s3 CONSTRAINTS+ASSERTIONS OUTPUTS   s4
SBVUnitTest/GoldFiles/basic-2_2.gold view
@@ -13,5 +13,6 @@   s2 :: SWord8 = s0 * s0   s3 :: SWord8 = s1 - s2 CONSTRAINTS+ASSERTIONS OUTPUTS   s3
SBVUnitTest/GoldFiles/basic-2_3.gold view
@@ -13,5 +13,6 @@   s2 :: SWord8 = s0 + s1   s3 :: SWord8 = s2 * s2 CONSTRAINTS+ASSERTIONS OUTPUTS   s3
SBVUnitTest/GoldFiles/basic-2_4.gold view
@@ -13,5 +13,6 @@   s2 :: SWord8 = s0 + s1   s3 :: SWord8 = s2 * s2 CONSTRAINTS+ASSERTIONS OUTPUTS   s3
SBVUnitTest/GoldFiles/basic-3_1.gold view
@@ -14,5 +14,6 @@   s3 :: SWord8 = s0 - s1   s4 :: SWord8 = s2 * s3 CONSTRAINTS+ASSERTIONS OUTPUTS   s4
SBVUnitTest/GoldFiles/basic-3_2.gold view
@@ -14,5 +14,6 @@   s3 :: SWord8 = s1 * s1   s4 :: SWord8 = s2 - s3 CONSTRAINTS+ASSERTIONS OUTPUTS   s4
SBVUnitTest/GoldFiles/basic-3_3.gold view
@@ -13,5 +13,6 @@   s2 :: SWord8 = s0 + s1   s3 :: SWord8 = s2 * s2 CONSTRAINTS+ASSERTIONS OUTPUTS   s3
SBVUnitTest/GoldFiles/basic-3_4.gold view
@@ -13,5 +13,6 @@   s2 :: SWord8 = s0 + s1   s3 :: SWord8 = s2 * s2 CONSTRAINTS+ASSERTIONS OUTPUTS   s3
SBVUnitTest/GoldFiles/basic-3_5.gold view
@@ -13,5 +13,6 @@ DEFINE   s3 :: SWord8 = s0 + s2 CONSTRAINTS+ASSERTIONS OUTPUTS   s3
SBVUnitTest/GoldFiles/basic-4_1.gold view
@@ -13,5 +13,6 @@   s2 :: SWord8 = s0 - s0   s3 :: SWord8 = s1 * s2 CONSTRAINTS+ASSERTIONS OUTPUTS   s3
SBVUnitTest/GoldFiles/basic-4_2.gold view
@@ -12,5 +12,6 @@   s1 :: SWord8 = s0 * s0   s2 :: SWord8 = s1 - s1 CONSTRAINTS+ASSERTIONS OUTPUTS   s2
SBVUnitTest/GoldFiles/basic-4_3.gold view
@@ -12,5 +12,6 @@   s1 :: SWord8 = s0 + s0   s2 :: SWord8 = s1 * s1 CONSTRAINTS+ASSERTIONS OUTPUTS   s2
SBVUnitTest/GoldFiles/basic-4_4.gold view
@@ -12,5 +12,6 @@   s1 :: SWord8 = s0 + s0   s2 :: SWord8 = s1 * s1 CONSTRAINTS+ASSERTIONS OUTPUTS   s2
SBVUnitTest/GoldFiles/basic-4_5.gold view
@@ -12,5 +12,6 @@ DEFINE   s2 :: SWord8 = s0 + s1 CONSTRAINTS+ASSERTIONS OUTPUTS   s2
SBVUnitTest/GoldFiles/basic-5_1.gold view
@@ -14,6 +14,7 @@   s3 :: SWord8 = s0 - s0   s4 :: SWord8 = s2 * s3 CONSTRAINTS+ASSERTIONS OUTPUTS   s1   s4
SBVUnitTest/GoldFiles/basic-5_2.gold view
@@ -13,6 +13,7 @@   s2 :: SWord8 = s0 * s0   s3 :: SWord8 = s2 - s2 CONSTRAINTS+ASSERTIONS OUTPUTS   s1   s3
SBVUnitTest/GoldFiles/basic-5_3.gold view
@@ -13,6 +13,7 @@   s2 :: SWord8 = s0 + s0   s3 :: SWord8 = s2 * s2 CONSTRAINTS+ASSERTIONS OUTPUTS   s1   s3
SBVUnitTest/GoldFiles/basic-5_4.gold view
@@ -13,6 +13,7 @@   s2 :: SWord8 = s0 + s0   s3 :: SWord8 = s2 * s2 CONSTRAINTS+ASSERTIONS OUTPUTS   s1   s3
SBVUnitTest/GoldFiles/basic-5_5.gold view
@@ -13,6 +13,7 @@ DEFINE   s3 :: SWord8 = s0 + s2 CONSTRAINTS+ASSERTIONS OUTPUTS   s1   s3
SBVUnitTest/GoldFiles/ccitt.gold view
@@ -1827,5 +1827,6 @@   s1816 :: SBool = s1814 > s1815   s1817 :: SBool = s8 | s1816 CONSTRAINTS+ASSERTIONS OUTPUTS   s1817
SBVUnitTest/GoldFiles/cgUninterpret.gold view
@@ -30,6 +30,8 @@ #ifndef __tstShiftLeft__HEADER_INCLUDED__ #define __tstShiftLeft__HEADER_INCLUDED__ +#include <stdio.h>+#include <stdlib.h> #include <inttypes.h> #include <stdint.h> #include <stdbool.h>
SBVUnitTest/GoldFiles/codeGen1.gold view
@@ -30,6 +30,8 @@ #ifndef __foo__HEADER_INCLUDED__ #define __foo__HEADER_INCLUDED__ +#include <stdio.h>+#include <stdlib.h> #include <inttypes.h> #include <stdint.h> #include <stdbool.h>
SBVUnitTest/GoldFiles/coins.gold view
@@ -911,5 +911,6 @@   s539   s541   s550+ASSERTIONS OUTPUTS   s552
SBVUnitTest/GoldFiles/counts.gold view
@@ -1700,5 +1700,6 @@   s1689 :: SBool = s394 & s1688   s1690 :: SBool = s234 & s1689 CONSTRAINTS+ASSERTIONS OUTPUTS   s1690
SBVUnitTest/GoldFiles/crcPolyExist.gold view
@@ -3481,5 +3481,6 @@   s3470 :: SBool = s12 | s3469   s3471 :: SBool = s7 & s3470 CONSTRAINTS+ASSERTIONS OUTPUTS   s3471
SBVUnitTest/GoldFiles/crcUSB5_1.gold view
@@ -30,6 +30,8 @@ #ifndef __crcUSB5__HEADER_INCLUDED__ #define __crcUSB5__HEADER_INCLUDED__ +#include <stdio.h>+#include <stdlib.h> #include <inttypes.h> #include <stdint.h> #include <stdbool.h>
SBVUnitTest/GoldFiles/crcUSB5_2.gold view
@@ -30,6 +30,8 @@ #ifndef __crcUSB5__HEADER_INCLUDED__ #define __crcUSB5__HEADER_INCLUDED__ +#include <stdio.h>+#include <stdlib.h> #include <inttypes.h> #include <stdint.h> #include <stdbool.h>
SBVUnitTest/GoldFiles/fib1.gold view
@@ -30,6 +30,8 @@ #ifndef __fib1__HEADER_INCLUDED__ #define __fib1__HEADER_INCLUDED__ +#include <stdio.h>+#include <stdlib.h> #include <inttypes.h> #include <stdint.h> #include <stdbool.h>
SBVUnitTest/GoldFiles/fib2.gold view
@@ -30,6 +30,8 @@ #ifndef __fib2__HEADER_INCLUDED__ #define __fib2__HEADER_INCLUDED__ +#include <stdio.h>+#include <stdlib.h> #include <inttypes.h> #include <stdint.h> #include <stdbool.h>
SBVUnitTest/GoldFiles/floats_cgen.gold view
@@ -1316,6 +1316,8 @@ #ifndef __floatCodeGen__HEADER_INCLUDED__ #define __floatCodeGen__HEADER_INCLUDED__ +#include <stdio.h>+#include <stdlib.h> #include <inttypes.h> #include <stdint.h> #include <stdbool.h>
SBVUnitTest/GoldFiles/gcd.gold view
@@ -30,6 +30,8 @@ #ifndef __sgcd__HEADER_INCLUDED__ #define __sgcd__HEADER_INCLUDED__ +#include <stdio.h>+#include <stdlib.h> #include <inttypes.h> #include <stdint.h> #include <stdbool.h>
SBVUnitTest/GoldFiles/iteTest1.gold view
@@ -10,4 +10,5 @@ AXIOMS DEFINE CONSTRAINTS+ASSERTIONS OUTPUTS
SBVUnitTest/GoldFiles/iteTest2.gold view
@@ -10,4 +10,5 @@ AXIOMS DEFINE CONSTRAINTS+ASSERTIONS OUTPUTS
SBVUnitTest/GoldFiles/iteTest3.gold view
@@ -10,4 +10,5 @@ AXIOMS DEFINE CONSTRAINTS+ASSERTIONS OUTPUTS
SBVUnitTest/GoldFiles/legato.gold view
@@ -8955,5 +8955,6 @@   s8944 :: SBool = s8940 == s8943   s8945 :: SBool = s15 | s8944 CONSTRAINTS+ASSERTIONS OUTPUTS   s8945
SBVUnitTest/GoldFiles/legato_c.gold view
@@ -30,6 +30,8 @@ #ifndef __legatoMult__HEADER_INCLUDED__ #define __legatoMult__HEADER_INCLUDED__ +#include <stdio.h>+#include <stdlib.h> #include <inttypes.h> #include <stdint.h> #include <stdbool.h>
SBVUnitTest/GoldFiles/merge.gold view
@@ -30,6 +30,8 @@ #ifndef __merge__HEADER_INCLUDED__ #define __merge__HEADER_INCLUDED__ +#include <stdio.h>+#include <stdlib.h> #include <inttypes.h> #include <stdint.h> #include <stdbool.h>
SBVUnitTest/GoldFiles/popCount1.gold view
@@ -30,6 +30,8 @@ #ifndef __popCount__HEADER_INCLUDED__ #define __popCount__HEADER_INCLUDED__ +#include <stdio.h>+#include <stdlib.h> #include <inttypes.h> #include <stdint.h> #include <stdbool.h>
SBVUnitTest/GoldFiles/popCount2.gold view
@@ -30,6 +30,8 @@ #ifndef __popCount__HEADER_INCLUDED__ #define __popCount__HEADER_INCLUDED__ +#include <stdio.h>+#include <stdlib.h> #include <inttypes.h> #include <stdint.h> #include <stdbool.h>
SBVUnitTest/GoldFiles/selChecked.gold view
@@ -30,6 +30,8 @@ #ifndef __selChecked__HEADER_INCLUDED__ #define __selChecked__HEADER_INCLUDED__ +#include <stdio.h>+#include <stdlib.h> #include <inttypes.h> #include <stdint.h> #include <stdbool.h>
SBVUnitTest/GoldFiles/selUnchecked.gold view
@@ -30,6 +30,8 @@ #ifndef __selUnChecked__HEADER_INCLUDED__ #define __selUnChecked__HEADER_INCLUDED__ +#include <stdio.h>+#include <stdlib.h> #include <inttypes.h> #include <stdint.h> #include <stdbool.h>
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where  buildTime :: String-buildTime = "Tue Oct 20 20:01:47 PDT 2015"+buildTime = "Mon Nov  9 17:48:14 PST 2015"
sbv.cabal view
@@ -1,5 +1,5 @@ Name:          sbv-Version:       5.3+Version:       5.4 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@@ -79,6 +79,7 @@                     , Data.SBV.Examples.Misc.Enumerate                     , Data.SBV.Examples.Misc.Floating                     , Data.SBV.Examples.Misc.ModelExtract+                    , Data.SBV.Examples.Misc.NoDiv0                     , Data.SBV.Examples.Misc.Word4                     , Data.SBV.Examples.Polynomials.Polynomials                     , Data.SBV.Examples.Puzzles.Birthday