sbv 3.0 → 3.1
raw patch · 46 files changed
+1021/−507 lines, 46 filesdep +asyncdep ~basedep ~deepseq
Dependencies added: async
Dependency ranges changed: base, deepseq
Files
- CHANGES.md +51/−1
- Data/SBV.hs +170/−9
- Data/SBV/BitVectors/Data.hs +161/−30
- Data/SBV/BitVectors/Model.hs +205/−109
- Data/SBV/BitVectors/PrettyNum.hs +0/−1
- Data/SBV/BitVectors/SignCast.hs +2/−0
- Data/SBV/Compilers/C.hs +5/−3
- Data/SBV/Compilers/CodeGen.hs +4/−2
- Data/SBV/Examples/BitPrecise/Legato.hs +1/−0
- Data/SBV/Examples/BitPrecise/PrefixSum.hs +4/−4
- Data/SBV/Examples/CodeGeneration/Uninterpreted.hs +10/−1
- Data/SBV/Examples/Misc/Floating.hs +2/−2
- Data/SBV/Examples/Misc/SBranch.hs +73/−0
- Data/SBV/Examples/Polynomials/Polynomials.hs +6/−6
- Data/SBV/Examples/Puzzles/U2Bridge.hs +6/−0
- Data/SBV/Examples/Uninterpreted/Deduce.hs +4/−0
- Data/SBV/Examples/Uninterpreted/Sort.hs +2/−0
- Data/SBV/Examples/Uninterpreted/UISortAllSat.hs +4/−2
- Data/SBV/Provers/Boolector.hs +1/−1
- Data/SBV/Provers/CVC4.hs +2/−2
- Data/SBV/Provers/MathSAT.hs +2/−2
- Data/SBV/Provers/Prover.hs +46/−123
- Data/SBV/Provers/SExpr.hs +3/−4
- Data/SBV/Provers/Yices.hs +1/−1
- Data/SBV/Provers/Z3.hs +3/−3
- Data/SBV/SMT/SMT.hs +81/−120
- Data/SBV/SMT/SMTLib.hs +0/−1
- Data/SBV/SMT/SMTLib1.hs +2/−2
- Data/SBV/SMT/SMTLib2.hs +16/−7
- Data/SBV/Tools/ExpectedValue.hs +4/−4
- Data/SBV/Tools/GenTest.hs +8/−8
- Data/SBV/Tools/Optimize.hs +1/−1
- Data/SBV/Tools/Polynomial.hs +5/−0
- README.md +18/−0
- SBVUnitTest/Examples/Basics/BasicTests.hs +16/−16
- SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
- SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs +16/−8
- SBVUnitTest/TestSuite/Basics/ArithSolver.hs +70/−20
- SBVUnitTest/TestSuite/BitPrecise/Legato.hs +2/−2
- SBVUnitTest/TestSuite/BitPrecise/PrefixSum.hs +1/−1
- SBVUnitTest/TestSuite/CRC/CCITT.hs +1/−1
- SBVUnitTest/TestSuite/Existentials/CRCPolynomial.hs +1/−1
- SBVUnitTest/TestSuite/Puzzles/Coins.hs +5/−4
- SBVUnitTest/TestSuite/Puzzles/Counts.hs +1/−1
- SBVUnitTest/TestSuite/Uninterpreted/AUF.hs +1/−1
- sbv.cabal +3/−2
CHANGES.md view
@@ -1,7 +1,57 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 3.0+* Latest Hackage released version: 3.1++### Version 3.1, 2014-07-12+ + NB: GHC 7.8.1 and 7.8.2 has a serious bug (https://ghc.haskell.org/trac/ghc/ticket/9078)+ that causes SBV to crash under heavy/repeated calls. The bug is addressed+ in GHC 7.8.3; so upgrading to 7.8.3 is essential for using SBV!++ New features/bug-fixes in v3.1:++ * Using multiple-SMT solvers in parallel:+ * Added functions that let the user run multiple solvers, using asynchronous+ threads. All results can be obtained (proveWithAll, proveWithAny, satWithAll),+ or SBV can return the fastest result (satWithAny, allSatWithAll, allSatWithAny).+ These functions are good for playing with multiple-solvers, especially on+ machines with multiple-cores.+ * Add function: sbvAvailableSolvers; which returns the list of solvers currently+ available, as installed on the machine we are running. (Not the list that SBV+ supports, but those that are actually available at run-time.) This function+ is useful with the multi-solve API.+ * Implement sBranch:+ * sBranch is a variant of 'ite' that consults the external+ SMT solver to see if a given branch condition is satisfiable+ before evaluating it. This can make certain "otherwise recursive+ and thus not-symbolically-terminating inputs" amenable to symbolic+ simulation, if termination can be established this way. Needless+ to say, this problem is always decidable as far as SBV programs+ are concerned, but it does not mean the decision procedure is cheap!+ Use with care. + * sBranchTimeOut config parameter can be used to curtail long runs when+ sBranch is used. Of course, if time-out happens, SBV will+ assume the branch is feasible, in which case symbolic-termination+ may come back to bite you.)+ * New API:+ * Add predicate 'isSNaN' which allows testing 'SFloat'/'SDouble' values+ for nan-ness. This is similar to the Prelude function 'isNaN', except+ the Prelude version requires a RealFrac instance, which unfortunately is+ not currently implementable for cases. (Requires trigonometric functions etc.)+ Thus, we provide 'isSNaN' separately (along with the already existing+ 'isFPPoint') to simplify reasoning with floating-point.+ * Examples:+ * Add Data/SBV/Examples/Misc/SBranch.hs, to illustrate the use of sBranch.+ * Bug fixes:+ * Fix pipe-blocking issue, which exhibited itself in the presence of+ large numbers of variables (> 10K or so). See github issue #86. Thanks+ to Philipp Meyer for the fine report.+ * Misc:+ * Add missing SFloat/SDouble instances for SatModel class+ * Explicitly support KBool as a kind, separating it from "KUnbounded False 1".+ Thanks to Brian Huffman for contributing the changes. This should have no+ user-visible impact, but comes in handy for internal reasons. ### Version 3.0, 2014-02-16
Data/SBV.hs view
@@ -96,10 +96,16 @@ -- -- * MathSAT from Fondazione Bruno Kessler and DISI-University of Trento: <http://mathsat.fbk.eu/> --+-- SBV also allows calling these solvers in parallel, either getting results from multiple solvers+-- or returning the fastest one. (See 'proveWithAll', 'proveWithAny', etc.)+-- -- Support for other compliant solvers can be added relatively easily, please -- get in touch if there is a solver you'd like to see included. --------------------------------------------------------------------------------- +{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE OverlappingInstances #-}+ module Data.SBV ( -- * Programming with symbolic values -- $progIntro@@ -117,7 +123,7 @@ , SInteger -- *** IEEE-floating point numbers -- $floatingPoints- , SFloat, SDouble, RoundingMode(..), nan, infinity, sNaN, sInfinity, fusedMA, isFPPoint+ , SFloat, SDouble, RoundingMode(..), nan, infinity, sNaN, sInfinity, fusedMA, isSNaN, isFPPoint -- *** Signed algebraic reals -- $algReals , SReal, AlgReal, toSReal@@ -188,6 +194,10 @@ -- ** Checking constraint vacuity , isVacuous, isVacuousWith + -- * Proving properties using multiple solvers+ -- $multiIntro+ , proveWithAll, proveWithAny, satWithAll, satWithAny, allSatWithAll, allSatWithAny+ -- * Optimization -- $optimizeIntro , minimize, maximize, optimize@@ -209,7 +219,7 @@ , getModelDictionaries, getModelValues, getModelUninterpretedValues -- * SMT Interface: Configurations and solvers- , SMTConfig(..), SMTLibLogic(..), Logic(..), OptimizeOpts(..), SMTSolver(..), boolector, cvc4, yices, z3, mathSAT, sbvCurrentSolver, defaultSMTCfg, sbvCheckSolverInstallation+ , SMTConfig(..), SMTLibLogic(..), Logic(..), OptimizeOpts(..), Solver(..), SMTSolver(..), boolector, cvc4, yices, z3, mathSAT, sbvCurrentSolver, defaultSMTCfg, sbvCheckSolverInstallation, sbvAvailableSolvers -- * Symbolic computations , Symbolic, output, SymWord(..)@@ -255,6 +265,10 @@ , module Data.Ratio ) where +import Control.Monad (filterM)+import Control.Concurrent.Async (async, waitAny, waitAnyCancel)+import System.IO.Unsafe (unsafeInterleaveIO) -- only used safely!+ import Data.SBV.BitVectors.AlgReals import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.Model@@ -282,13 +296,140 @@ sbvCurrentSolver :: SMTConfig sbvCurrentSolver = z3 +-- | Note that the floating point value NaN does not compare equal to itself,+-- so we need a special recognizer for that. Haskell provides the isNaN predicate+-- with the `RealFrac` class, which unfortunately is not currently implementable for+-- symbolic cases. (Requires trigonometric functions etc.) Thus, we provide this+-- recognizer separately. Note that the definition simply tests equality against+-- itself, which fails for NaN. Who said equality for floating point was reflexive?+isSNaN :: (Floating a, SymWord a) => SBV a -> SBool+isSNaN x = x ./= x+ -- | We call a FP number FPPoint if it is neither NaN, nor +/- infinity.--- Note that we cannot use == to test for this, as NaN does not compare equal to itself. isFPPoint :: (Floating a, SymWord a) => SBV a -> SBool isFPPoint x = x .== x -- gets rid of NaN's &&& x .< sInfinity -- gets rid of +inf &&& x .> -sInfinity -- gets rid of -inf +-- | Form the symbolic conjunction of a given list of boolean conditions. Useful in expressing+-- problems with constraints, like the following:+--+-- @+-- do [x, y, z] <- sIntegers [\"x\", \"y\", \"z\"]+-- solve [x .> 5, y + z .< x]+-- @+solve :: [SBool] -> Symbolic SBool+solve = return . bAnd++-- | Check whether the given solver is installed and is ready to go. This call does a+-- simple call to the solver to ensure all is well.+sbvCheckSolverInstallation :: SMTConfig -> IO Bool+sbvCheckSolverInstallation cfg = do ThmResult r <- proveWith cfg $ \x -> (x+x) .== ((x*2) :: SWord8)+ case r of+ Unsatisfiable _ -> return True+ _ -> return False++-- The default configs+defaultSolverConfig :: Solver -> SMTConfig+defaultSolverConfig Z3 = z3+defaultSolverConfig Yices = yices+defaultSolverConfig Boolector = boolector+defaultSolverConfig CVC4 = cvc4+defaultSolverConfig MathSAT = mathSAT++-- | Return the known available solver configs, installed on your machine.+sbvAvailableSolvers :: IO [SMTConfig]+sbvAvailableSolvers = filterM sbvCheckSolverInstallation (map defaultSolverConfig [minBound .. maxBound])++sbvWithAny :: Provable a => [SMTConfig] -> (SMTConfig -> a -> IO b) -> a -> IO (Solver, b)+sbvWithAny [] _ _ = error "SBV.withAny: No solvers given!"+sbvWithAny solvers what a = snd `fmap` (mapM try solvers >>= waitAnyCancel)+ where try s = async $ what s a >>= \r -> return (name (solver s), r)++sbvWithAll :: Provable a => [SMTConfig] -> (SMTConfig -> a -> IO b) -> a -> IO [(Solver, b)]+sbvWithAll solvers what a = mapM try solvers >>= (unsafeInterleaveIO . go)+ where try s = async $ what s a >>= \r -> return (name (solver s), r)+ go [] = return []+ go as = do (d, r) <- waitAny as+ rs <- unsafeInterleaveIO $ go (filter (/= d) as)+ return (r : rs)++-- | Prove a property with multiple solvers, running them in separate threads. The+-- results will be returned in the order produced.+proveWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, ThmResult)]+proveWithAll = (`sbvWithAll` proveWith)++-- | Prove a property with multiple solvers, running them in separate threads. Only+-- the result of the first one to finish will be returned, remaining threads will be killed.+proveWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, ThmResult)+proveWithAny = (`sbvWithAny` proveWith)++-- | Find a satisfying assignment to a property with multiple solvers, running them in separate threads. The+-- results will be returned in the order produced.+satWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, SatResult)]+satWithAll = (`sbvWithAll` satWith)++-- | Find a satisfying assignment to a property with multiple solvers, running them in separate threads. Only+-- the result of the first one to finish will be returned, remaining threads will be killed.+satWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, SatResult)+satWithAny = (`sbvWithAny` satWith)++-- | Find all satisfying assignments to a property with multiple solvers, running them in separate threads. Only+-- the result of the first one to finish will be returned, remaining threads will be killed.+allSatWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, AllSatResult)]+allSatWithAll = (`sbvWithAll` allSatWith)++-- | Find all satisfying assignments to a property with multiple solvers, running them in separate threads. Only+-- the result of the first one to finish will be returned, remaining threads will be killed.+allSatWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, AllSatResult)+allSatWithAny = (`sbvWithAny` allSatWith)++-- | Equality as a proof method. Allows for+-- very concise construction of equivalence proofs, which is very typical in+-- bit-precise proofs.+infix 4 ===+class Equality a where+ (===) :: a -> a -> IO ThmResult++instance (SymWord a, EqSymbolic z) => Equality (SBV a -> z) where+ k === l = prove $ \a -> k a .== l a++instance (SymWord a, SymWord b, EqSymbolic z) => Equality (SBV a -> SBV b -> z) where+ k === l = prove $ \a b -> k a b .== l a b++instance (SymWord a, SymWord b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) where+ k === l = prove $ \a b -> k (a, b) .== l (a, b)++instance (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z) where+ k === l = prove $ \a b c -> k a b c .== l a b c++instance (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z) where+ k === l = prove $ \a b c -> k (a, b, c) .== l (a, b, c)++instance (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z) where+ k === l = prove $ \a b c d -> k a b c d .== l a b c d++instance (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z) where+ k === l = prove $ \a b c d -> k (a, b, c, d) .== l (a, b, c, d)++instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) where+ k === l = prove $ \a b c d e -> k a b c d e .== l a b c d e++instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) where+ k === l = prove $ \a b c d e -> k (a, b, c, d, e) .== l (a, b, c, d, e)++instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) where+ k === l = prove $ \a b c d e f -> k a b c d e f .== l a b c d e f++instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) where+ k === l = prove $ \a b c d e f -> k (a, b, c, d, e, f) .== l (a, b, c, d, e, f)++instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) where+ k === l = prove $ \a b c d e f g -> k a b c d e f g .== l a b c d e f g++instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) where+ k === l = prove $ \a b c d e f g -> k (a, b, c, d, e, f, g) .== l (a, b, c, d, e, f, g)+ -- Haddock section documentation {- $progIntro The SBV library is really two things:@@ -318,12 +459,32 @@ or how different logics operate. The details are hidden behind the SBV framework, providing Haskell programmers with a clean API that is unencumbered by the details of individual solvers. To that end, we use the SMT-Lib standard (<http://goedel.cs.uiowa.edu/smtlib/>)-to communicate with arbitrary SMT solvers. Unfortunately,-the SMT-Lib version 1.X does not standardize how models are communicated back from solvers, so-there is some work in parsing individual SMT solver output. The 2.X version of the SMT-Lib-standard (not yet implemented by SMT solvers widely, unfortunately) will bring new standard features-for getting models; at which time the SBV framework can be modified into a truly plug-and-play-system where arbitrary SMT solvers can be used.+to communicate with arbitrary SMT solvers.+-}++{- $multiIntro+On a multi-core machine, it might be desirable to try a given property using multiple SMT solvers,+using parallel threads. Even with machines with single-cores, threading can be helpful if you+want to try out multiple-solvers but do not know which one would work the best+for the problem at hand ahead of time.++The functions in this section allow proving/satisfiability-checking with multiple+backends at the same time. Each function comes in two variants, one that+returns the results from all solvers, the other that returns the fastest one.++The @All@ variants, (i.e., 'proveWithAll', 'satWithAll', 'allSatWithAll') run all solvers and+return all the results. SBV internally makes sure that the result is lazily generated; so,+the order of solvers given does not matter. In other words, the order of results will follow+the order of the solvers as they finish, not as given by the user. These variants are useful when you+want to make sure multiple-solvers agree (or disagree!) on a given problem.++The @Any@ variants, (i.e., 'proveWithAny', 'satWithAny', 'allSatWithAny') will run all the solvers+in parallel, and return the results of the first one finishing. The other threads will then be killed. These variants+are useful when you do not care if the solvers produce the same result, but rather want to get the+solution as quickly as possible, taking advantage of modern many-core machines.++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. -} {- $optimizeIntro
Data/SBV/BitVectors/Data.hs view
@@ -17,6 +17,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE NamedFieldPuns #-} module Data.SBV.BitVectors.Data ( SBool, SWord8, SWord16, SWord32, SWord64@@ -28,19 +29,23 @@ , SW(..), trueSW, falseSW, trueCW, falseCW, normCW , SBV(..), NodeId(..), mkSymSBV , ArrayContext(..), ArrayInfo, SymArray(..), SFunArray(..), mkSFunArray, SArray(..), arrayUIKind- , sbvToSW, sbvToSymSW+ , sbvToSW, sbvToSymSW, forceSWArg , SBVExpr(..), newExpr , cache, Cached, uncache, uncacheAI, HasKind(..)- , Op(..), NamedSymVar, UnintKind(..), getTableIndex, SBVPgm(..), Symbolic, runSymbolic, runSymbolic', State, inProofMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..)+ , Op(..), NamedSymVar, UnintKind(..), getTableIndex, SBVPgm(..), Symbolic, runSymbolic, runSymbolic', State, getPathCondition, extendPathCondition+ , inProofMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..) , Logic(..), SMTLibLogic(..) , getTraceInfo, getConstraints, addConstraint , SBVType(..), newUninterpreted, unintFnUIKind, addAxiom , Quantifier(..), needsExistentials , SMTLibPgm(..), SMTLibVersion(..) , SolverCapabilities(..)+ , extractSymbolicSimulationState+ , SMTScript(..), Solver(..), SMTSolver(..), SMTResult(..), SMTModel(..), SMTConfig(..), getSBranchRunConfig ) where import Control.DeepSeq (NFData(..))+import Control.Applicative (Applicative) import Control.Monad (when) import Control.Monad.Reader (MonadReader, ReaderT, ask, runReaderT) import Control.Monad.Trans (MonadIO, liftIO)@@ -58,6 +63,7 @@ import qualified Data.Foldable as F (toList) import qualified Data.Sequence as S (Seq, empty, (|>)) +import System.Exit (ExitCode(..)) import System.Mem.StableName import System.Random @@ -128,8 +134,8 @@ -- | Is this a bit? cwIsBit :: CW -> Bool cwIsBit x = case cwKind x of- KBounded False 1 -> True- _ -> False+ KBool -> True+ _ -> False -- | Convert a CW to a Haskell boolean (NB. Assumes input is well-kinded) cwToBool :: CW -> Bool@@ -150,7 +156,8 @@ normCW c = c -- | Kind of symbolic value-data Kind = KBounded Bool Int+data Kind = KBool+ | KBounded Bool Int | KUnbounded | KReal | KUninterpreted String@@ -159,7 +166,7 @@ deriving (Eq, Ord) instance Show Kind where- show (KBounded False 1) = "SBool"+ show KBool = "SBool" show (KBounded False n) = "SWord" ++ show n show (KBounded True n) = "SInt" ++ show n show KUnbounded = "SInteger"@@ -174,6 +181,12 @@ -- | A symbolic word, tracking it's signedness and size. data SW = SW Kind NodeId deriving (Eq, Ord) +-- | Forcing an argument; this is a necessary evil to make sure all the arguments+-- to an uninterpreted function and sBranch test conditions are evaluated before called;+-- the semantics of uinterpreted functions is necessarily strict; deviating from Haskell's+forceSWArg :: SW -> IO ()+forceSWArg (SW k n) = k `seq` n `seq` return ()+ -- | Quantifiers: forall or exists. Note that we allow -- arbitrary nestings. data Quantifier = ALL | EX deriving Eq@@ -184,19 +197,19 @@ -- | Constant False as a SW. Note that this value always occupies slot -2. falseSW :: SW-falseSW = SW (KBounded False 1) $ NodeId (-2)+falseSW = SW KBool $ NodeId (-2) -- | Constant False as a SW. Note that this value always occupies slot -1. trueSW :: SW-trueSW = SW (KBounded False 1) $ NodeId (-1)+trueSW = SW KBool $ NodeId (-1) -- | Constant False as a CW. We represent it using the integer value 0. falseCW :: CW-falseCW = CW (KBounded False 1) (CWInteger 0)+falseCW = CW KBool (CWInteger 0) -- | Constant True as a CW. We represent it using the integer value 1. trueCW :: CW-trueCW = CW (KBounded False 1) (CWInteger 1)+trueCW = CW KBool (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@@ -263,6 +276,7 @@ showType :: a -> String -- defaults hasSign x = case kindOf x of+ KBool -> False KBounded b _ -> b KUnbounded -> True KReal -> True@@ -270,13 +284,14 @@ KDouble -> True KUninterpreted{} -> False intSizeOf x = case kindOf x of+ KBool -> error "SBV.HasKind.intSizeOf((S)Bool)" KBounded _ s -> s KUnbounded -> error "SBV.HasKind.intSizeOf((S)Integer)" KReal -> error "SBV.HasKind.intSizeOf((S)Real)" KFloat -> error "SBV.HasKind.intSizeOf((S)Float)" KDouble -> error "SBV.HasKind.intSizeOf((S)Double)" KUninterpreted s -> error $ "SBV.HasKind.intSizeOf: Uninterpreted sort: " ++ s- isBoolean x | KBounded False 1 <- kindOf x = True+ isBoolean x | KBool{} <- kindOf x = True | True = False isBounded x | KBounded{} <- kindOf x = True | True = False@@ -296,7 +311,7 @@ default kindOf :: Data a => a -> Kind kindOf = KUninterpreted . tyconUQname . dataTypeName . dataTypeOf -instance HasKind Bool where kindOf _ = KBounded False 1+instance HasKind Bool where kindOf _ = KBool instance HasKind Int8 where kindOf _ = KBounded True 8 instance HasKind Word8 where kindOf _ = KBounded False 8 instance HasKind Int16 where kindOf _ = KBounded True 16@@ -538,9 +553,9 @@ external (ArrayMerge{}) = False -- | Different means of running a symbolic piece of code-data SBVRunMode = Proof Bool -- ^ Symbolic simulation mode, for proof purposes. Bool is True if it's a sat instance- | CodeGen -- ^ Code generation mode- | Concrete StdGen -- ^ Concrete simulation mode. The StdGen is for the pConstrain acceptance in cross runs+data SBVRunMode = Proof (Bool, Maybe SMTConfig) -- ^ Symbolic simulation mode, for proof purposes. Bool is True if it's a sat instance. SMTConfig is used for 'sBranch' calls.+ | CodeGen -- ^ Code generation mode+ | Concrete StdGen -- ^ Concrete simulation mode. The StdGen is for the pConstrain acceptance in cross runs -- | Is this a concrete run? (i.e., quick-check or test-generation like) isConcreteMode :: SBVRunMode -> Bool@@ -550,6 +565,7 @@ -- | The state of the symbolic interpreter data State = State { runMode :: SBVRunMode+ , pathCond :: SBool , rStdGen :: IORef StdGen , rCInfo :: IORef [(String, CW)] , rctr :: IORef Int@@ -569,6 +585,14 @@ , rAICache :: IORef (Cache Int) } +-- | Get the current path condition+getPathCondition :: State -> SBool+getPathCondition = pathCond++-- | Extend the path condition with the given test value.+extendPathCondition :: State -> (SBool -> SBool) -> State+extendPathCondition st f = st{pathCond = f (pathCond st)}+ -- | Are we running in proof mode? inProofMode :: State -> Bool inProofMode s = case runMode s of@@ -576,6 +600,12 @@ CodeGen -> False Concrete{} -> False +-- | If in proof mode, get the underlying configuration (used for 'sBranch')+getSBranchRunConfig :: State -> Maybe SMTConfig+getSBranchRunConfig st = case runMode st of+ Proof (_, s) -> s+ _ -> Nothing+ -- | The "Symbolic" value. Either a constant (@Left@) or a symbolic -- value (@Right Cached@). Note that caching is essential for making -- sure sharing is preserved. The parameter 'a' is phantom, but is@@ -742,6 +772,7 @@ -- | Create a constant word from an integral mkConstCW :: Integral a => Kind -> a -> CW+mkConstCW KBool a = normCW $ CW KBool (CWInteger (toInteger a)) mkConstCW k@(KBounded{}) a = normCW $ CW k (CWInteger (toInteger a)) mkConstCW KUnbounded a = normCW $ CW KUnbounded (CWInteger (toInteger a)) mkConstCW KReal a = normCW $ CW KReal (CWAlgReal (fromInteger (toInteger a)))@@ -774,7 +805,7 @@ -- state of the computation, layered on top of IO for creating unique -- references to hold onto intermediate results. newtype Symbolic a = Symbolic (ReaderT State IO a)- deriving (Functor, Monad, MonadIO, MonadReader State)+ deriving (Applicative, Functor, Monad, MonadIO, MonadReader State) -- | Create a symbolic value, based on the quantifier we have. If an explicit quantifier is given, we just use that. -- If not, then we pick existential for SAT calls and universal for everything else.@@ -782,11 +813,11 @@ mkSymSBV mbQ k mbNm = do st <- ask let q = case (mbQ, runMode st) of- (Just x, _) -> x -- user given, just take it- (Nothing, Concrete{}) -> ALL -- concrete simulation, pick universal- (Nothing, Proof True) -> EX -- sat mode, pick existential- (Nothing, Proof False) -> ALL -- proof mode, pick universal- (Nothing, CodeGen) -> ALL -- code generation, pick universal+ (Just x, _) -> x -- user given, just take it+ (Nothing, Concrete{}) -> ALL -- concrete simulation, pick universal+ (Nothing, Proof (True, _)) -> EX -- sat mode, pick existential+ (Nothing, Proof (False, _)) -> ALL -- proof mode, pick universal+ (Nothing, CodeGen) -> ALL -- code generation, pick universal case runMode st of Concrete _ | q == EX -> case mbNm of Nothing -> error $ "Cannot quick-check in the presence of existential variables, type: " ++ showType (undefined :: SBV a)@@ -862,7 +893,7 @@ -- | Run a symbolic computation in Proof mode and return a 'Result'. The boolean -- argument indicates if this is a sat instance or not.-runSymbolic :: Bool -> Symbolic a -> IO Result+runSymbolic :: (Bool, Maybe SMTConfig) -> Symbolic a -> IO Result runSymbolic b c = snd `fmap` runSymbolic' (Proof b) c -- | Run a symbolic computation, and return a extra value paired up with the 'Result'@@ -888,6 +919,7 @@ Concrete g -> newIORef g _ -> newStdGen >>= newIORef let st = State { runMode = currentRunMode+ , pathCond = SBV KBool (Left trueCW) , rStdGen = rGen , rCInfo = cInfo , rctr = ctr@@ -906,9 +938,17 @@ , rAICache = aiCache , rConstraints = cstrs }- _ <- newConst st (mkConstCW (KBounded False 1) (0::Integer)) -- s(-2) == falseSW- _ <- newConst st (mkConstCW (KBounded False 1) (1::Integer)) -- s(-1) == trueSW+ _ <- newConst st falseCW -- s(-2) == falseSW+ _ <- newConst st trueCW -- s(-1) == trueSW r <- runReaderT c st+ res <- extractSymbolicSimulationState st+ return (r, res)++-- | Grab the program from a running symbolic simulation state. This is useful for internal purposes, for+-- 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 SBVPgm rpgm <- readIORef pgm inpsO <- reverse `fmap` readIORef inps outsO <- reverse `fmap` readIORef outs@@ -923,7 +963,7 @@ cgMap <- Map.toList `fmap` readIORef cgs traceVals <- reverse `fmap` readIORef cInfo extraCstrs <- reverse `fmap` readIORef cstrs- return $ (r, Result knds traceVals cgMap inpsO cnsts tbls arrs unint axs (SBVPgm rpgm) extraCstrs outsO)+ return $ Result knds traceVals cgMap inpsO cnsts tbls arrs unint axs (SBVPgm rpgm) extraCstrs outsO ------------------------------------------------------------------------------- -- * Symbolic Words@@ -1008,11 +1048,11 @@ let k = KUninterpreted sortName liftIO $ registerKind st k let q = case (mbQ, runMode st) of- (Just x, _) -> x- (Nothing, Proof True) -> EX- (Nothing, Proof False) -> ALL- (Nothing, Concrete{}) -> error $ "SBV: Uninterpreted sort " ++ sortName ++ " can not be used in concrete simulation mode."- (Nothing, CodeGen) -> error $ "SBV: Uninterpreted sort " ++ sortName ++ " can not be used in code-generation mode."+ (Just x, _) -> x+ (Nothing, Proof (True, _)) -> EX+ (Nothing, Proof (False, _)) -> ALL+ (Nothing, Concrete{}) -> error $ "SBV: Uninterpreted sort " ++ sortName ++ " can not be used in concrete simulation mode."+ (Nothing, CodeGen) -> error $ "SBV: 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@@ -1248,6 +1288,16 @@ rnf (SBV x y) = rnf x `seq` rnf y `seq` () instance NFData SBVPgm +instance NFData SMTResult where+ rnf (Unsatisfiable _) = ()+ rnf (Satisfiable _ xs) = rnf xs `seq` ()+ rnf (Unknown _ xs) = rnf xs `seq` ()+ rnf (ProofError _ xs) = rnf xs `seq` ()+ rnf (TimeOut _) = ()++instance NFData SMTModel where+ rnf (SMTModel assocs unints uarrs) = rnf assocs `seq` rnf unints `seq` rnf uarrs `seq` ()+ -- | SMT-Lib logics. If left unspecified SBV will pick the logic based on what it determines is needed. However, the -- user can override this choice using the 'useLogic' parameter to the configuration. This is especially handy if -- one is experimenting with custom logics that might be supported on new solvers.@@ -1300,3 +1350,84 @@ , supportsFloats :: Bool -- ^ Does the solver support single-precision floating point numbers? , supportsDoubles :: Bool -- ^ Does the solver support double-precision floating point numbers? }++-- | Solver configuration. See also 'z3', 'yices', 'cvc4', 'boolector', 'mathSAT', etc. which are instantiations of this type for those solvers, with+-- reasonable defaults. In particular, custom configuration can be created by varying those values. (Such as @z3{verbose=True}@.)+--+-- Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does+-- not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to+-- emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite+-- precision value on the screen. The field 'printRealPrec' controls the printing precision, by specifying the number of digits after+-- the decimal point. The default value is 16, but it can be set to any positive integer.+--+-- When printing, SBV will add the suffix @...@ at the and of a real-value, if the given bound is not sufficient to represent the real-value+-- exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it+-- is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation+-- of the real value is not finite, i.e., if it is not rational.+data SMTConfig = SMTConfig {+ verbose :: Bool -- ^ Debug mode+ , timing :: Bool -- ^ Print timing information on how long different phases took (construction, solving, etc.)+ , sBranchTimeOut :: Maybe Int -- ^ How much time to give to the solver for each call of 'sBranch' check. (In seconds. Default: No limit.)+ , timeOut :: Maybe Int -- ^ How much time to give to the solver. (In seconds. Default: No limit.)+ , printBase :: Int -- ^ Print integral literals in this base (2, 8, and 10, and 16 are supported.)+ , printRealPrec :: Int -- ^ Print algebraic real values with this precision. (SReal, default: 16)+ , solverTweaks :: [String] -- ^ Additional lines of script to give to the solver (user specified)+ , satCmd :: String -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics.+ , smtFile :: Maybe FilePath -- ^ If Just, the generated SMT script will be put in this file (for debugging purposes mostly)+ , useSMTLib2 :: Bool -- ^ If True, we'll treat the solver as using SMTLib2 input format. Otherwise, SMTLib1+ , solver :: SMTSolver -- ^ The actual SMT solver.+ , roundingMode :: RoundingMode -- ^ Rounding mode to use for floating-point conversions+ , useLogic :: Maybe Logic -- ^ If Nothing, pick automatically. Otherwise, either use the given one, or use the custom string.+ }++instance Show SMTConfig where+ show = show . solver++-- | A model, as returned by a solver+data SMTModel = SMTModel {+ modelAssocs :: [(String, CW)] -- ^ Mapping of symbolic values to constants.+ , modelArrays :: [(String, [String])] -- ^ Arrays, very crude; only works with Yices.+ , modelUninterps :: [(String, [String])] -- ^ Uninterpreted funcs; very crude; only works with Yices.+ }+ deriving Show++-- | The result of an SMT solver call. Each constructor is tagged with+-- the 'SMTConfig' that created it so that further tools can inspect it+-- and build layers of results, if needed. For ordinary uses of the library,+-- this type should not be needed, instead use the accessor functions on+-- it. (Custom Show instances and model extractors.)+data SMTResult = Unsatisfiable SMTConfig -- ^ Unsatisfiable+ | Satisfiable SMTConfig SMTModel -- ^ Satisfiable with model+ | Unknown SMTConfig SMTModel -- ^ Prover returned unknown, with a potential (possibly bogus) model+ | ProofError SMTConfig [String] -- ^ Prover errored out+ | TimeOut SMTConfig -- ^ Computation timed out (see the 'timeout' combinator)++-- | A script, to be passed to the solver.+data SMTScript = SMTScript {+ scriptBody :: String -- ^ Initial feed+ , scriptModel :: Maybe String -- ^ Optional continuation script, if the result is sat+ }++-- | An SMT engine+type SMTEngine = SMTConfig -> Bool -> [(Quantifier, NamedSymVar)] -> [(String, UnintKind)] -> [Either SW (SW, [SW])] -> String -> IO SMTResult++-- | Solvers that SBV is aware of+data Solver = Z3+ | Yices+ | Boolector+ | CVC4+ | MathSAT+ deriving (Show, Enum, Bounded)++-- | An SMT solver+data SMTSolver = SMTSolver {+ name :: Solver -- ^ The solver in use+ , executable :: String -- ^ The path to its executable+ , options :: [String] -- ^ Options to provide to the solver+ , engine :: SMTEngine -- ^ The solver engine, responsible for interpreting solver output+ , xformExitCode :: ExitCode -> ExitCode -- ^ Should we re-interpret exit codes. Most solvers behave rationally, i.e., id will do. Some (like CVC4) don't.+ , capabilities :: SolverCapabilities -- ^ Various capabilities of the solver+ }++instance Show SMTSolver where+ show = show . name
Data/SBV/BitVectors/Model.hs view
@@ -50,6 +50,23 @@ import Data.SBV.BitVectors.Data import Data.SBV.Utils.Boolean +import Data.SBV.Provers.Prover (isSBranchFeasibleInState)++-- The following two imports are only needed because of the doctest expressions we have. Sigh..+-- It might be a good idea to reorg some of the content to avoid this.+import Data.SBV.Provers.Prover (isVacuous, prove)+import Data.SBV.SMT.SMT (ThmResult)++-- | Newer versions of GHC (Starting with 7.8 I think), distinguishes between FiniteBits and Bits classes.+-- We should really use FiniteBitSize for SBV which would make things better. In the interim, just work+-- around pesky warnings..+ghcBitSize :: Bits a => a -> Int+#if __GLASGOW_HASKELL__ >= 708+ghcBitSize x = maybe (error "SBV.ghcBitSize: Unexpected non-finite usage!") id (bitSizeMaybe x)+#else+ghcBitSize = bitSize+#endif+ noUnint :: String -> a noUnint x = error $ "Unexpected operation called on uninterpreted value: " ++ show x @@ -74,20 +91,20 @@ liftSym2B :: (State -> Kind -> SW -> SW -> IO SW) -> (CW -> CW -> Bool) -> (AlgReal -> AlgReal -> Bool) -> (Integer -> Integer -> Bool) -> (Float -> Float -> Bool) -> (Double -> Double -> Bool) -> SBV b -> SBV b -> SBool liftSym2B _ okCW opCR opCI opCF opCD (SBV _ (Left a)) (SBV _ (Left b)) | okCW a b = literal (liftCW2 opCR opCI opCF opCD noUnint2 a b)-liftSym2B opS _ _ _ _ _ a b = SBV (KBounded False 1) $ Right $ liftSW2 opS (KBounded False 1) a b+liftSym2B opS _ _ _ _ _ a b = SBV KBool $ Right $ liftSW2 opS KBool a b liftSym1Bool :: (State -> Kind -> SW -> IO SW) -> (Bool -> Bool) -> SBool -> SBool liftSym1Bool _ opC (SBV _ (Left a)) = literal $ opC $ cwToBool a-liftSym1Bool opS _ a = SBV (KBounded False 1) $ Right $ cache c+liftSym1Bool opS _ a = SBV KBool $ Right $ cache c where c st = do sw <- sbvToSW st a- opS st (KBounded False 1) sw+ opS st KBool sw liftSym2Bool :: (State -> Kind -> SW -> SW -> IO SW) -> (Bool -> Bool -> Bool) -> SBool -> SBool -> SBool liftSym2Bool _ opC (SBV _ (Left a)) (SBV _ (Left b)) = literal (cwToBool a `opC` cwToBool b)-liftSym2Bool opS _ a b = SBV (KBounded False 1) $ Right $ cache c+liftSym2Bool opS _ a b = SBV KBool $ Right $ cache c where c st = do sw1 <- sbvToSW st a sw2 <- sbvToSW st b- opS st (KBounded False 1) sw1 sw2+ opS st KBool sw1 sw2 mkSymOpSC :: (SW -> SW -> Maybe SW) -> Op -> State -> Kind -> SW -> SW -> IO SW mkSymOpSC shortCut op st k a b = maybe (newExpr st k (SBVApp op [a, b])) return (shortCut a b)@@ -126,8 +143,8 @@ genMkSymVar k mbq (Just s) = genVar mbq k s instance SymWord Bool where- mkSymWord = genMkSymVar (KBounded False 1)- literal x = genLiteral (KBounded False 1) (if x then (1::Integer) else 0)+ mkSymWord = genMkSymVar KBool+ literal x = genLiteral KBool (if x then (1::Integer) else 0) fromCW = cwToBool mbMaxBound = Just maxBound mbMinBound = Just minBound@@ -730,6 +747,9 @@ | True = liftSym2 (mkSymOp XOr) (const (const True)) (noReal "xor") xor (noFloat "xor") (noDouble "xor") x y complement = liftSym1 (mkSymOp1 Not) (noRealUnary "complement") complement (noFloatUnary "complement") (noDoubleUnary "complement") bitSize _ = intSizeOf (undefined :: a)+#if __GLASGOW_HASKELL__ >= 708+ bitSizeMaybe _ = Just $ intSizeOf (undefined :: a)+#endif isSigned _ = hasSign (undefined :: a) bit i = 1 `shiftL` i shiftL x y@@ -743,12 +763,12 @@ rotateL x y | y < 0 = rotateR x (-y) | y == 0 = x- | isBounded x = let sz = bitSize x in liftSym1 (mkSymOp1 (Rol (y `mod` sz))) (noRealUnary "rotateL") (rot True sz y) (noFloatUnary "rotateL") (noDoubleUnary "rotateL") x+ | isBounded x = let sz = ghcBitSize x in liftSym1 (mkSymOp1 (Rol (y `mod` sz))) (noRealUnary "rotateL") (rot True sz y) (noFloatUnary "rotateL") (noDoubleUnary "rotateL") x | True = shiftL x y -- for unbounded Integers, rotateL is the same as shiftL in Haskell rotateR x y | y < 0 = rotateL x (-y) | y == 0 = x- | isBounded x = let sz = bitSize x in liftSym1 (mkSymOp1 (Ror (y `mod` sz))) (noRealUnary "rotateR") (rot False sz y) (noFloatUnary "rotateR") (noDoubleUnary "rotateR") x+ | isBounded x = let sz = ghcBitSize x in liftSym1 (mkSymOp1 (Ror (y `mod` sz))) (noRealUnary "rotateR") (rot False sz y) (noFloatUnary "rotateR") (noDoubleUnary "rotateR") x | True = shiftR x y -- for unbounded integers, rotateR is the same as shiftR in Haskell -- NB. testBit is *not* implementable on non-concrete symbolic words x `testBit` i@@ -806,7 +826,7 @@ sbvShiftLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a sbvShiftLeft x i | isSigned i = error "sbvShiftLeft: shift amount should be unsigned"- | True = select [x `shiftL` k | k <- [0 .. bitSize x - 1]] 0 i+ | True = select [x `shiftL` k | k <- [0 .. ghcBitSize x - 1]] 0 i -- | Generalization of 'shiftR', when the shift-amount is symbolic. Since Haskell's -- 'shiftR' only takes an 'Int' as the shift amount, it cannot be used when we have@@ -818,7 +838,7 @@ sbvShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a sbvShiftRight x i | isSigned i = error "sbvShiftRight: shift amount should be unsigned"- | True = select [x `shiftR` k | k <- [0 .. bitSize x - 1]] 0 i+ | True = select [x `shiftR` k | k <- [0 .. ghcBitSize x - 1]] 0 i -- | Arithmetic shift-right with a symbolic unsigned shift amount. This is equivalent -- to 'sbvShiftRight' when the argument is signed. However, if the argument is unsigned,@@ -853,14 +873,14 @@ fullMultiplier :: SIntegral a => SBV a -> SBV a -> (SBV a, SBV a) fullMultiplier a b | isSigned a = error "fullMultiplier: only works on unsigned numbers"- | True = (go (bitSize a) 0 a, a*b)+ | True = (go (ghcBitSize a) 0 a, a*b) where go 0 p _ = p go n p x = let (c, p') = ite (lsb x) (fullAdder p b) (false, p) (o, p'') = shiftIn c p' (_, x') = shiftIn o x in go (n-1) p'' x' shiftIn k v = (lsb v, mask .|. (v `shiftR` 1))- where mask = ite k (bit (bitSize v - 1)) 0+ where mask = ite k (bit (ghcBitSize v - 1)) 0 -- | Little-endian blasting of a word into its bits. Also see the 'FromBits' class. blastLE :: (Num a, Bits a, SymWord a) => SBV a -> [SBool]@@ -1125,6 +1145,24 @@ -- The idea is that use symbolicMerge if you know the condition is symbolic, -- otherwise use ite, if there's a chance it might be concrete. ite :: SBool -> a -> a -> a+ -- | Branch on a condition, much like 'ite'. The exception is that SBV will+ -- check to make sure if the test condition is feasible by making an external+ -- call to the SMT solver. Note that this can be expensive, thus we shall use+ -- a time-out value ('sBranchTimeOut'). There might be zero, one, or two such+ -- external calls per 'sBranch' call:+ --+ -- - If condition is statically known to be True/False: 0 calls+ -- - In this case, we simply constant fold..+ --+ -- - If condition is determined to be unsatisfiable : 1 call+ -- - In this case, we know then-branch is infeasible, so just take the else-branch+ --+ -- - If condition is determined to be satisfable : 2 calls+ -- - In this case, we know then-branch is feasible, but we still have to check if the else-branch is+ --+ -- In summary, 'sBranch' calls can be expensive, but they can help with the so-called symbolic-termination+ -- problem. See "Data.SBV.Examples.Misc.SBranch" for an example.+ sBranch :: SBool -> a -> a -> a -- | Total indexing operation. @select xs default index@ is intuitively -- the same as @xs !! index@, except it evaluates to @default@ if @index@ -- overflows@@ -1133,6 +1171,7 @@ ite s a b | Just t <- unliteral s = if t then a else b | True = symbolicMerge s a b+ sBranch s = ite (reduceInPathCondition s) -- NB. Earlier implementation of select used the binary-search trick -- on the index to chop down the search space. While that is a good trick -- in general, it doesn't work for SBV since we do not have any notion of@@ -1148,86 +1187,14 @@ -- SBV instance SymWord a => Mergeable (SBV a) where- -- the strict match and checking of literal equivalence is essential below,- -- as otherwise we risk hanging onto huge closures and blow stack! This is- -- against the feel that merging shouldn't look at branches if the test- -- expression is constant. However, it's OK to do it this way since we- -- expect "ite" to be used in such cases which already checks for that. That- -- is the use case of the symbolicMerge should be when the test is symbolic.- -- Of course, we do not have a way of enforcing that in the user code, but- -- at least our library code respects that invariant.- symbolicMerge t a@(SBV{}) b@(SBV{})- | Just av <- unliteral a, Just bv <- unliteral b, rationalSBVCheck a b, av == bv- = a- | True- = SBV k $ Right $ cache c- where k = kindOf a- c st = do swt <- sbvToSW st t- case () of- () | swt == trueSW -> sbvToSW st a -- these two cases should never be needed as we expect symbolicMerge to be- () | swt == falseSW -> sbvToSW st b -- called with symbolic tests, but just in case..- () -> do {- It is tempting to record the choice of the test expression here as we branch down to the 'then' and 'else' branches. That is,- when we evaluate 'a', we can make use of the fact that the test expression is True, and similarly we can use the fact that it- is False when b is evaluated. In certain cases this can cut down on symbolic simulation significantly, for instance if- repetitive decisions are made in a recursive loop. Unfortunately, the implementation of this idea is quite tricky, due to- our sharing based implementation. As the 'then' branch is evaluated, we will create many expressions that are likely going- to be "reused" when the 'else' branch is executed. But, it would be *dead wrong* to share those values, as they were "cached"- under the incorrect assumptions. To wit, consider the following:-- foo x y = ite (y .== 0) k (k+1)- where k = ite (y .== 0) x (x+1)-- When we reduce the 'then' branch of the first ite, we'd record the assumption that y is 0. But while reducing the 'then' branch, we'd- like to share 'k', which would evaluate (correctly) to 'x' under the given assumption. When we backtrack and evaluate the 'else'- branch of the first ite, we'd see 'k' is needed again, and we'd look it up from our sharing map to find (incorrectly) that its value- is 'x', which was stored there under the assumption that y was 0, which no longer holds. Clearly, this is unsound.-- A sound implementation would have to precisely track which assumptions were active at the time expressions get shared. That is,- in the above example, we should record that the value of 'k' was cached under the assumption that 'y' is 0. While sound, this- approach unfortunately leads to significant loss of valid sharing when the value itself had nothing to do with the assumption itself.- To wit, consider:-- foo x y = ite (y .== 0) k (k+1)- where k = x+5-- If we tracked the assumptions, we would recompute 'k' twice, since the branch assumptions would differ. Clearly, there is no need to- re-compute 'k' in this case since its value is independent of y. Note that the whole SBV performance story is based on agressive sharing,- and losing that would have other significant ramifications.-- The "proper" solution would be to track, with each shared computation, precisely which assumptions it actually *depends* on, rather- than blindly recording all the assumptions present at that time. SBV's symbolic simulation engine clearly has all the info needed to do this- properly, but the implementation is not straightforward at all. For each subexpression, we would need to chase down its dependencies- transitively, which can require a lot of scanning of the generated program causing major slow-down; thus potentially defeating the- whole purpose of sharing in the first place.-- Design choice: Keep it simple, and simply do not track the assumption at all. This will maximize sharing, at the cost of evaluating- unreachable branches. I think the simplicity is more important at this point than efficiency.-- Also note that the user can avoid most such issues by properly combining if-then-else's with common conditions together. That is, the- first program above should be written like this:-- foo x y = ite (y .== 0) x (x+2)-- In general, the following transformations should be done whenever possible:-- ite e1 (ite e1 e2 e3) e4 --> ite e1 e2 e4- ite e1 e2 (ite e1 e3 e4) --> ite e1 e2 e4-- This is in accordance with the general rule-of-thumb stating conditionals should be avoided as much as possible. However, we might prefer- the following:-- ite e1 (f e2 e4) (f e3 e5) --> f (ite e1 e2 e3) (ite e1 e4 e5)-- especially if this expression happens to be inside 'f's body itself (i.e., when f is recursive), since it reduces the number of- recursive calls. Clearly, programming with symbolic simulation in mind is another kind of beast alltogether.- -}- swa <- sbvToSW st a -- evaluate 'then' branch- swb <- sbvToSW st b -- evaluate 'else' branch- case () of -- merge:- () | swa == swb -> return swa- () | swa == trueSW && swb == falseSW -> return swt- () | swa == falseSW && swb == trueSW -> newExpr st k (SBVApp Not [swt])- () -> newExpr st k (SBVApp Ite [swt, swa, swb])+ -- sBranch is essentially the default method, but we are careful in not forcing the+ -- arguments as ite does, since sBranch is expected to be used when one of the+ -- branches is likely to be in a branch that's recursively evaluated.+ sBranch s a b+ | Just t <- unliteral sReduced = if t then a else b+ | True = symbolicWordMerge False sReduced a b+ where sReduced = reduceInPathCondition s+ symbolicMerge = symbolicWordMerge True -- Custom version of select that translates to SMT-Lib tables at the base type of words select xs err ind | SBV _ (Left c) <- ind = case cwVal c of@@ -1247,6 +1214,86 @@ let len = length xs newExpr st kElt (SBVApp (LkUp (idx, kInd, kElt, len) swi swe) []) +-- symbolically merge two SBV words, based on the boolean condition given.+-- The first argument controls whether we want to reduce the branches+-- separately first, which avoids hanging onto huge thunks, and is usually+-- the right thing to do for ite. But we precisely do not want to do that+-- in case of sBranch, which is the case when one of the branches (typically+-- the "else" branch is hanging off of a recursive call.+symbolicWordMerge :: SymWord a => Bool -> SBool -> SBV a -> SBV a -> SBV a+symbolicWordMerge force t a b+ | force, Just av <- unliteral a, Just bv <- unliteral b, rationalSBVCheck a b, av == bv+ = a+ | True+ = SBV k $ Right $ cache c+ where k = kindOf a+ c st = do swt <- sbvToSW st t+ case () of+ () | swt == trueSW -> sbvToSW st a -- these two cases should never be needed as we expect symbolicMerge to be+ () | swt == falseSW -> sbvToSW st b -- called with symbolic tests, but just in case..+ () -> do {- It is tempting to record the choice of the test expression here as we branch down to the 'then' and 'else' branches. That is,+ when we evaluate 'a', we can make use of the fact that the test expression is True, and similarly we can use the fact that it+ is False when b is evaluated. In certain cases this can cut down on symbolic simulation significantly, for instance if+ repetitive decisions are made in a recursive loop. Unfortunately, the implementation of this idea is quite tricky, due to+ our sharing based implementation. As the 'then' branch is evaluated, we will create many expressions that are likely going+ to be "reused" when the 'else' branch is executed. But, it would be *dead wrong* to share those values, as they were "cached"+ under the incorrect assumptions. To wit, consider the following:++ foo x y = ite (y .== 0) k (k+1)+ where k = ite (y .== 0) x (x+1)++ When we reduce the 'then' branch of the first ite, we'd record the assumption that y is 0. But while reducing the 'then' branch, we'd+ like to share 'k', which would evaluate (correctly) to 'x' under the given assumption. When we backtrack and evaluate the 'else'+ branch of the first ite, we'd see 'k' is needed again, and we'd look it up from our sharing map to find (incorrectly) that its value+ is 'x', which was stored there under the assumption that y was 0, which no longer holds. Clearly, this is unsound.++ A sound implementation would have to precisely track which assumptions were active at the time expressions get shared. That is,+ in the above example, we should record that the value of 'k' was cached under the assumption that 'y' is 0. While sound, this+ approach unfortunately leads to significant loss of valid sharing when the value itself had nothing to do with the assumption itself.+ To wit, consider:++ foo x y = ite (y .== 0) k (k+1)+ where k = x+5++ If we tracked the assumptions, we would recompute 'k' twice, since the branch assumptions would differ. Clearly, there is no need to+ re-compute 'k' in this case since its value is independent of y. Note that the whole SBV performance story is based on agressive sharing,+ and losing that would have other significant ramifications.++ The "proper" solution would be to track, with each shared computation, precisely which assumptions it actually *depends* on, rather+ than blindly recording all the assumptions present at that time. SBV's symbolic simulation engine clearly has all the info needed to do this+ properly, but the implementation is not straightforward at all. For each subexpression, we would need to chase down its dependencies+ transitively, which can require a lot of scanning of the generated program causing major slow-down; thus potentially defeating the+ whole purpose of sharing in the first place.++ Design choice: Keep it simple, and simply do not track the assumption at all. This will maximize sharing, at the cost of evaluating+ unreachable branches. I think the simplicity is more important at this point than efficiency.++ Also note that the user can avoid most such issues by properly combining if-then-else's with common conditions together. That is, the+ first program above should be written like this:++ foo x y = ite (y .== 0) x (x+2)++ In general, the following transformations should be done whenever possible:++ ite e1 (ite e1 e2 e3) e4 --> ite e1 e2 e4+ ite e1 e2 (ite e1 e3 e4) --> ite e1 e2 e4++ This is in accordance with the general rule-of-thumb stating conditionals should be avoided as much as possible. However, we might prefer+ the following:++ ite e1 (f e2 e4) (f e3 e5) --> f (ite e1 e2 e3) (ite e1 e4 e5)++ especially if this expression happens to be inside 'f's body itself (i.e., when f is recursive), since it reduces the number of+ recursive calls. Clearly, programming with symbolic simulation in mind is another kind of beast alltogether.+ -}+ swa <- sbvToSW (st `extendPathCondition` (&&& t)) a -- evaluate 'then' branch+ swb <- sbvToSW (st `extendPathCondition` (&&& bnot t)) b -- evaluate 'else' branch+ case () of -- merge:+ () | swa == swb -> return swa+ () | swa == trueSW && swb == falseSW -> return swt+ () | swa == falseSW && swb == trueSW -> newExpr st k (SBVApp Not [swt])+ () -> newExpr st k (SBVApp Ite [swt, swa, swb])+ -- Unit instance Mergeable () where symbolicMerge _ _ _ = ()@@ -1348,10 +1395,10 @@ -- SArrays are both "EqSymbolic" and "Mergeable" instance EqSymbolic (SArray a b) where- (SArray _ a) .== (SArray _ b) = SBV (KBounded False 1) $ Right $ cache c+ (SArray _ a) .== (SArray _ b) = SBV KBool $ Right $ cache c where c st = do ai <- uncacheAI a st bi <- uncacheAI b st- newExpr st (KBounded False 1) (SBVApp (ArrEq ai bi) [])+ newExpr st KBool (SBVApp (ArrEq ai bi) []) instance SymWord b => Mergeable (SArray a b) where symbolicMerge = mergeArrays@@ -1408,12 +1455,6 @@ | True = do newUninterpreted st nm (SBVType [ka]) (fst `fmap` mbCgData) newExpr st ka $ SBVApp (Uninterpreted nm) [] --- Forcing an argument; this is a necessary evil to make sure all the arguments--- to an uninterpreted function are evaluated before called; the semantics of--- such functions is necessarily strict; deviating from Haskell's-forceArg :: SW -> IO ()-forceArg (SW k n) = k `seq` n `seq` return ()- -- Functions of one argument instance (SymWord b, HasKind a) => Uninterpreted (SBV b -> SBV a) where sbvUninterpret mbCgData nm = f@@ -1427,7 +1468,7 @@ result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st (v arg0) | True = do newUninterpreted st nm (SBVType [kb, ka]) (fst `fmap` mbCgData) sw0 <- sbvToSW st arg0- mapM_ forceArg [sw0]+ mapM_ forceSWArg [sw0] newExpr st ka $ SBVApp (Uninterpreted nm) [sw0] -- Functions of two arguments@@ -1445,7 +1486,7 @@ | True = do newUninterpreted st nm (SBVType [kc, kb, ka]) (fst `fmap` mbCgData) sw0 <- sbvToSW st arg0 sw1 <- sbvToSW st arg1- mapM_ forceArg [sw0, sw1]+ mapM_ forceSWArg [sw0, sw1] newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1] -- Functions of three arguments@@ -1465,7 +1506,7 @@ sw0 <- sbvToSW st arg0 sw1 <- sbvToSW st arg1 sw2 <- sbvToSW st arg2- mapM_ forceArg [sw0, sw1, sw2]+ mapM_ forceSWArg [sw0, sw1, sw2] newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2] -- Functions of four arguments@@ -1487,7 +1528,7 @@ sw1 <- sbvToSW st arg1 sw2 <- sbvToSW st arg2 sw3 <- sbvToSW st arg3- mapM_ forceArg [sw0, sw1, sw2, sw3]+ mapM_ forceSWArg [sw0, sw1, sw2, sw3] newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3] -- Functions of five arguments@@ -1511,7 +1552,7 @@ sw2 <- sbvToSW st arg2 sw3 <- sbvToSW st arg3 sw4 <- sbvToSW st arg4- mapM_ forceArg [sw0, sw1, sw2, sw3, sw4]+ mapM_ forceSWArg [sw0, sw1, sw2, sw3, sw4] newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4] -- Functions of six arguments@@ -1537,7 +1578,7 @@ sw3 <- sbvToSW st arg3 sw4 <- sbvToSW st arg4 sw5 <- sbvToSW st arg5- mapM_ forceArg [sw0, sw1, sw2, sw3, sw4, sw5]+ mapM_ forceSWArg [sw0, sw1, sw2, sw3, sw4, sw5] newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5] -- Functions of seven arguments@@ -1566,7 +1607,7 @@ sw4 <- sbvToSW st arg4 sw5 <- sbvToSW st arg5 sw6 <- sbvToSW st arg6- mapM_ forceArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6]+ mapM_ forceSWArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6] newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5, sw6] -- Uncurried functions of two arguments@@ -1603,7 +1644,39 @@ 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.+-- | Adding arbitrary constraints. When adding constraints, one has to be careful about+-- making sure they are not inconsistent. The function 'isVacuous' can be use for this purpose.+-- Here is an example. Consider the following predicate:+--+-- >>> let pred = do { x <- forall "x"; constrain $ x .< x; return $ x .>= (5 :: SWord8) }+--+-- This predicate asserts that all 8-bit values are larger than 5, subject to the constraint that the+-- values considered satisfy @x .< x@, i.e., they are less than themselves. Since there are no values that+-- satisfy this constraint, the proof will pass vacuously:+--+-- >>> prove pred+-- Q.E.D.+--+-- We can use 'isVacuous' to make sure to see that the pass was vacuous:+--+-- >>> isVacuous pred+-- True+--+-- While the above example is trivial, things can get complicated if there are multiple constraints with+-- non-straightforward relations; so if constraints are used one should make sure to check the predicate+-- is not vacuously true. Here's an example that is not vacuous:+--+-- >>> let pred' = do { x <- forall "x"; constrain $ x .> 6; return $ x .>= (5 :: SWord8) }+--+-- This time the proof passes as expected:+--+-- >>> prove pred'+-- Q.E.D.+--+-- And the proof is not vacuous:+--+-- >>> isVacuous pred'+-- False constrain :: SBool -> Symbolic () constrain c = addConstraint Nothing c (bnot c) @@ -1613,6 +1686,25 @@ pConstrain :: Double -> SBool -> Symbolic () pConstrain t c = addConstraint (Just t) c (bnot c) +-- | Boolean symbolic reduction. See if we can reduce a boolean condition to true/false+-- using the path context information, by making external calls to the SMT solvers. Used in the+-- implementation of 'sBranch'.+reduceInPathCondition :: SBool -> SBool+reduceInPathCondition b+ | isConcrete b = b -- No reduction is needed, already a concrete value+ | True = SBV k $ Right $ cache c+ where k = kindOf b+ c st = do -- Now that we know our boolean is not obviously true/false. Need to make an external+ -- call to the SMT solver to see if we can prove it is necessarily one of those+ let pc = getPathCondition st+ satTrue <- isSBranchFeasibleInState st "then" (pc &&& b)+ if not satTrue+ then return falseSW -- condition is not satisfiable; so it must be necessarily False.+ else do satFalse <- isSBranchFeasibleInState st "else" (pc &&& bnot b)+ if not satFalse -- negation of the condition is not satisfiable; so it must be necessarily True.+ then return trueSW+ else sbvToSW st b -- condition is not necessarily always True/False. So, keep symbolic.+ -- Quickcheck interface on symbolic-booleans.. instance Testable SBool where property (SBV _ (Left b)) = property (cwToBool b)@@ -1650,6 +1742,10 @@ let xsbv = SBV (kindOf x) (Right (cache (const (return xsw)))) res = f xsbv sbvToSW st res++-- We use 'isVacuous' and 'prove' only for the "test" section in this file, and GHC complains about that. So, this shuts it up.+__unused :: a+__unused = error "__unused" (isVacuous :: SBool -> IO Bool) (prove :: SBool -> IO ThmResult) {-# ANN module "HLint: ignore Eta reduce" #-} {-# ANN module "HLint: ignore Reduce duplication" #-}
Data/SBV/BitVectors/PrettyNum.hs view
@@ -27,7 +27,6 @@ import Numeric (showIntAtBase, showHex, readInt) import Data.SBV.BitVectors.Data-import Data.SBV.BitVectors.Model () -- instances only -- | PrettyNum class captures printing of numbers in hex and binary formats; also supporting negative numbers. --
Data/SBV/BitVectors/SignCast.hs view
@@ -81,6 +81,7 @@ | Just c <- unliteral x = literal $ fromIntegral c | True = SBV k (Right (cache y)) where k = case kindOf x of+ KBool -> error "Data.SBV.SignCast.genericSign: Called on boolean value" KBounded False n -> KBounded True n KBounded True _ -> error "Data.SBV.SignCast.genericSign: Called on signed value" KUnbounded -> error "Data.SBV.SignCast.genericSign: Called on unbounded value"@@ -97,6 +98,7 @@ | Just c <- unliteral x = literal $ fromIntegral c | True = SBV k (Right (cache y)) where k = case kindOf x of+ KBool -> error "Data.SBV.SignCast.genericUnSign: Called on boolean value" KBounded True n -> KBounded False n KBounded False _ -> error "Data.SBV.SignCast.genericUnSign: Called on unsigned value" KUnbounded -> error "Data.SBV.SignCast.genericUnSign: Called on unbounded value"
Data/SBV/Compilers/C.hs view
@@ -161,6 +161,7 @@ -- | The printf specifier for the type specifier :: CgConfig -> SW -> Doc specifier cfg sw = case kindOf sw of+ KBool -> spec (False, 1) KBounded b i -> spec (b, i) KUnbounded -> spec (True, fromJust (cgInteger cfg)) KReal -> specF (fromJust (cgReal cfg))@@ -442,7 +443,7 @@ len (KFloat{}) = 6 -- SFloat len (KDouble{}) = 7 -- SDouble len (KUnbounded{}) = 8- len (KBounded False 1) = 5 -- SBool+ len KBool = 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@@ -498,8 +499,8 @@ 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+ KBool -> 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@@ -516,6 +517,7 @@ canOverflow True sz = (2::Integer)^(sz-1)-1 >= fromIntegral len canOverflow False sz = (2::Integer)^sz -1 >= fromIntegral len (needsCheckL, needsCheckR) = case k of+ KBool -> (False, canOverflow False (1::Int)) KBounded sg sz -> (sg, canOverflow sg sz) KReal -> die "array index with real value" KFloat -> die "array index with float value"
Data/SBV/Compilers/CodeGen.hs view
@@ -16,6 +16,7 @@ import Control.Monad.Trans import Control.Monad.State.Lazy+import Control.Applicative (Applicative) import Data.Char (toLower, isSpace) import Data.List (nub, isPrefixOf, intercalate, (\\)) import System.Directory (createDirectory, doesDirectoryExist, doesFileExist)@@ -75,7 +76,7 @@ -- reference parameters (for returning composite values in languages such as C), -- and return values. newtype SBVCodeGen a = SBVCodeGen (StateT CgState Symbolic a)- deriving (Monad, MonadIO, MonadState CgState)+ deriving (Applicative, Functor, Monad, MonadIO, MonadState CgState) -- | Reach into symbolic monad from code-generation liftSymbolic :: Symbolic a -> SBVCodeGen a@@ -109,7 +110,7 @@ | CgLongDouble -- ^ @long double@ deriving Eq --- As they would be used in a C program+-- | 'Show' instance for 'cgSRealType' displays values as they would be used in a C program instance Show CgSRealType where show CgFloat = "float" show CgDouble = "double"@@ -217,6 +218,7 @@ isCgMakefile CgMakefile{} = True isCgMakefile _ = False +-- | A simple way to print bundles, mostly for debugging purposes. instance Show CgPgmBundle where show (CgPgmBundle _ fs) = intercalate "\n" $ map showFile fs where showFile :: (FilePath, (CgPgmKind, [Doc])) -> String
Data/SBV/Examples/BitPrecise/Legato.hs view
@@ -79,6 +79,7 @@ -- | Programs are essentially state transformers (on the machine state) type Program = Mostek -> Mostek +-- | 'Mergeable' instance of 'Mostek' simply pushes the merging into record fields. instance Mergeable Mostek where symbolicMerge b m1 m2 = Mostek { memory = symbolicMerge b (memory m1) (memory m2) , registers = symbolicMerge b (registers m1) (registers m2)
Data/SBV/Examples/BitPrecise/PrefixSum.hs view
@@ -263,8 +263,8 @@ -- s18 ladnerFischerTrace :: Int -> IO () ladnerFischerTrace n = gen >>= print- where gen = runSymbolic True $ do args :: [SWord8] <- mkForallVars n- mapM_ output $ lf (0, (+)) args+ where gen = runSymbolic (True, Nothing) $ do args :: [SWord8] <- mkForallVars n+ mapM_ output $ lf (0, (+)) args -- | Trace generator for the reference spec. It clearly demonstrates that the reference -- implementation fewer operations, but is not parallelizable at all:@@ -308,7 +308,7 @@ -- scanlTrace :: Int -> IO () scanlTrace n = gen >>= print- where gen = runSymbolic True $ do args :: [SWord8] <- mkForallVars n- mapM_ output $ ps (0, (+)) args+ where gen = runSymbolic (True, Nothing) $ do args :: [SWord8] <- mkForallVars n+ mapM_ output $ ps (0, (+)) args {-# ANN module "HLint: ignore Reduce duplication" #-}
Data/SBV/Examples/CodeGeneration/Uninterpreted.hs view
@@ -13,6 +13,8 @@ -- purposes, such as efficiency, or reliability. ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-}+ module Data.SBV.Examples.CodeGeneration.Uninterpreted where import Data.SBV@@ -34,7 +36,14 @@ -- the Haskell code we'd like SBV to use when running inside Haskell or when -- translated to SMTLib for verification purposes. This is good old Haskell -- code, as one would typically write.- hCode x = select [x * literal (bit b) | b <- [0.. bitSize x - 1]] (literal 0)+ hCode x = select [x * literal (bit b) | b <- [0.. bs x - 1]] (literal 0)+#if __GLASGOW_HASKELL__ >= 708+ bs x = maybe (error "SBV.Example.CodeGeneration.Uninterpreted.shiftLeft: Unexpected non-finite usage!") id (bitSizeMaybe x)+#else+ bs = bitSize+#endif++ -- | Test function that uses shiftLeft defined above. When used as a normal Haskell function -- or in verification the definition is fully used, i.e., no uninterpretation happens. To wit,
Data/SBV/Examples/Misc/Floating.hs view
@@ -116,11 +116,11 @@ -- -- >>> multInverse -- Falsifiable. Counter-example:--- a = 1.3999060872492817e-308 :: SDouble+-- a = 1.3625818045773776e-308 :: SDouble -- -- Indeed, we have: ----- >>> let a = 1.3999060872492817e-308 :: Double+-- >>> let a = 1.3625818045773776e-308 :: Double -- >>> a * (1/a) -- 0.9999999999999999 multInverse :: IO ThmResult
+ Data/SBV/Examples/Misc/SBranch.hs view
@@ -0,0 +1,73 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.SBV.Examples.Misc.SBranch+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Illustrates the use of 'sBranch', as a means of dealing with certain cases+-- of the symbolic-termination problem.+-----------------------------------------------------------------------------++module Data.SBV.Examples.Misc.SBranch where++import Data.SBV++-- | A fast implementation of population-count. Note that SBV already provides+-- this functionality via 'sbvPopCount', using simple expansion and counting+-- algorithm. 'sbvPopCount' is linear in the size of the input, i.e., a 32-bit+-- word would take 32 additions. This implementation here is /faster/ in the+-- sense that it takes as many additions as there are set-bits in the given word.+--+-- Of course, the issue is that this definition is recursive, and the usual+-- definition via 'ite' would never symbolically terminate: Recursion is done+-- on the input argument: In each recursive call, we /reduce/ the value @n@+-- to @n .&. (n-1)@. This eliminates one set-bit in the input. However, this+-- claim is far from obvious. By the use of 'sBranch' we tell SBV to call+-- the SMT solver in each test to ensure we only evaluate the branches we need,+-- thus avoiding the symbolic-termination issue. In a sense, the SMT solvers+-- proves that the implementation terminates for all valid inputs.+--+-- Note that replacing 'sBranch' in this implementation with 'ite' would cause+-- symbolic-termination to loop forever. Of course, this does /not/ mean that+-- 'sBranch' is fast: It is costly to make external calls to the solver for+-- each branch, so use with care.+bitCount :: SWord32 -> SWord8+bitCount = go 0+ where go c n = sBranch (n .== 0) c (go (c+1) (n .&. (n-1)))++-- | Prove that the 'bitCount' function implemented here is equivalent to+-- the internal "slower" implementation. We have:+--+-- >>> prop+-- Q.E.D.+prop :: IO ThmResult+prop = prove $ \n -> bitCount n .== sbvPopCount n++-- | Illustrates the use of path-conditions in avoiding infeasible paths in symbolic+-- simulation. If we used 'ite' instead of 'sBranch' in the else-branch of the+-- implementation of 'path' symbolic simulation would have encountered the 'error' call, and+-- hence would have failed. But 'sBranch' keeps track of the path condition, and can+-- successfully determine that this path will never be taken, and hence avoids the problem.+-- Note that we can freely mix/match 'ite' and 'sBranch' calls; path conditions will be+-- tracked in both cases. In fact, use of 'ite' is advisable if we know for a fact that+-- both branches are feasible, as it avoids the external call. 'sBranch' will have the+-- same result, albeit it'll cost more.+path :: SWord8 -> SWord8+path x = ite (x .> 5)+ 10+ (sBranch (x .> 10)+ (error "this case is not reachable!") -- NB. x .> 5 fails, so can't be .> 10 here+ 20)++-- | Prove that 'path' always produces either @10@ or @20@, i.e., symbolic simulation will+-- not fail due to the 'error' call. We have:+--+-- >>> pathCheck+-- Q.E.D.+--+-- Were we to use 'ite' instead of 'sBranch' in the implementation of 'path', this expression+-- would have caused an exception to be raised at symbolic simulation time.+pathCheck :: IO ThmResult+pathCheck = prove $ \n -> let pn = path n in pn .== 10 ||| pn .== 20
Data/SBV/Examples/Polynomials/Polynomials.hs view
@@ -37,22 +37,22 @@ -- Note that the irreducible itself is not in GF28! It has a degree of 8. -- -- NB. You can use the 'showPoly' function to print polynomials nicely, as a mathematician would write.-(<*>) :: GF28 -> GF28 -> GF28-a <*> b = pMult (a, b, [8, 4, 3, 1, 0])+gfMult :: GF28 -> GF28 -> GF28+a `gfMult` b = pMult (a, b, [8, 4, 3, 1, 0]) -- | States that the unit polynomial @1@, is the unit element multUnit :: GF28 -> SBool-multUnit x = (x <*> unit) .== x+multUnit x = (x `gfMult` unit) .== x where unit = polynomial [0] -- x@0 -- | States that multiplication is commutative multComm :: GF28 -> GF28 -> SBool-multComm x y = (x <*> y) .== (y <*> x)+multComm x y = (x `gfMult` y) .== (y `gfMult` x) -- | States that multiplication is associative, note that associativity -- proofs are notoriously hard for SAT/SMT solvers multAssoc :: GF28 -> GF28 -> GF28 -> SBool-multAssoc x y z = ((x <*> y) <*> z) .== (x <*> (y <*> z))+multAssoc x y z = ((x `gfMult` y) `gfMult` z) .== (x `gfMult` (y `gfMult` z)) -- | States that the usual multiplication rule holds over GF(2^n) polynomials -- Checks:@@ -65,7 +65,7 @@ -- defined to be 0 and the remainder is the numerator. -- (Note that addition is simply `xor` in GF(2^8).) polyDivMod :: GF28 -> GF28 -> SBool-polyDivMod x y = ite (y .== 0) ((0, x) .== (a, b)) (x .== y <*> a `xor` b)+polyDivMod x y = ite (y .== 0) ((0, x) .== (a, b)) (x .== (y `gfMult` a) `xor` b) where (a, b) = x `pDivMod` y -- | Queries
Data/SBV/Examples/Puzzles/U2Bridge.hs view
@@ -91,6 +91,8 @@ , lLarry = here } +-- | Mergeable instance for 'Status' simply walks down the structure fields and+-- merges them. instance Mergeable Status where symbolicMerge t s1 s2 = Status { time = symbolicMerge t (time s1) (time s2) , flash = symbolicMerge t (flash s1) (flash s2)@@ -103,6 +105,8 @@ -- | A puzzle move is modeled as a state-transformer type Move a = State Status a +-- | Mergeable instance for 'Move' simply pushes the merging the data after run of each branch+-- starting from the same state. instance Mergeable a => Mergeable (Move a) where symbolicMerge t a b = do s <- get@@ -198,6 +202,8 @@ zigZag _ [] = true zigZag w (f:rest) = w .== f &&& zigZag (bnot w) rest +-- | The SatModel instance makes it easy to build models, mapping words to U2 members+-- in the way we designated. instance SatModel U2Member where parseCWs as = cvtModel cvtCW $ parseCWs as where cvtCW :: Word8 -> Maybe U2Member
Data/SBV/Examples/Uninterpreted/Deduce.hs view
@@ -28,7 +28,11 @@ -- | The uninterpreted sort 'B', corresponding to the carrier. data B = B deriving (Eq, Ord, Data, Typeable)++-- | Default instance declaration for 'SymWord' instance SymWord B++-- | Default instance declaration for 'HasKind' instance HasKind B -- | Handy shortcut for the type of symbolic values over 'B'
Data/SBV/Examples/Uninterpreted/Sort.hs view
@@ -26,6 +26,8 @@ -- 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++-- | 'HasKind' instance is again straightforward, no specific implementation needed. instance HasKind Q -- | Declare an uninterpreted function that works over Q's
Data/SBV/Examples/Uninterpreted/UISortAllSat.hs view
@@ -26,9 +26,11 @@ | Cons Int L deriving (Eq, Ord, Data, Typeable) --- | Declare instances to make 'L' a usable uninterpreted sort. Note that default--- definitions suffice in each case.+-- | Declare instances to make 'L' a usable uninterpreted sort. First we need the+-- 'SymWord' instance, with the default definition sufficing. instance SymWord L++-- | Similarly, 'HasKind's default implementation is sufficient. instance HasKind L -- | An uninterpreted "classify" function. Really, we only care about
Data/SBV/Provers/Boolector.hs view
@@ -29,7 +29,7 @@ -- The default options are @\"-m --smt2\"@. You can use the @SBV_BOOLECTOR_OPTIONS@ environment variable to override the options. boolector :: SMTSolver boolector = SMTSolver {- name = "boolector"+ name = Boolector , executable = "boolector" , options = ["-m", "--smt2"] , engine = \cfg _isSat qinps modelMap _skolemMap pgm -> do
Data/SBV/Provers/CVC4.hs view
@@ -30,7 +30,7 @@ -- The default options are @\"--lang smt\"@. You can use the @SBV_CVC4_OPTIONS@ environment variable to override the options. cvc4 :: SMTSolver cvc4 = SMTSolver {- name = "cvc4"+ name = CVC4 , executable = "cvc4" , options = ["--lang", "smt"] , engine = \cfg isSat qinps modelMap skolemMap pgm -> do@@ -57,7 +57,7 @@ } } where zero :: Kind -> String- zero (KBounded False 1) = "#b0"+ zero KBool = "false" zero (KBounded _ sz) = "#x" ++ replicate (sz `div` 4) '0' zero KUnbounded = "0" zero KReal = "0.0"
Data/SBV/Provers/MathSAT.hs view
@@ -28,7 +28,7 @@ -- The default options are @\"-input=smt2\"@. You can use the @SBV_MATHSAT_OPTIONS@ environment variable to override the options. mathSAT :: SMTSolver mathSAT = SMTSolver {- name = "MathSAT"+ name = MathSAT , executable = "mathsat" , options = ["-input=smt2"] , engine = \cfg _isSat qinps modelMap skolemMap pgm -> do@@ -56,7 +56,7 @@ } } where zero :: Kind -> String- zero (KBounded False 1) = "#b0"+ zero KBool = "false" zero (KBounded _ sz) = "#x" ++ replicate (sz `div` 4) '0' zero KUnbounded = "0" zero KReal = "0.0"
Data/SBV/Provers/Prover.hs view
@@ -18,30 +18,28 @@ SMTSolver(..), SMTConfig(..), Predicate, Provable(..) , ThmResult(..), SatResult(..), AllSatResult(..), SMTResult(..) , isSatisfiable, isSatisfiableWith, isTheorem, isTheoremWith- , Equality(..) , prove, proveWith , sat, satWith , allSat, allSatWith , isVacuous, isVacuousWith- , solve , SatModel(..), Modelable(..), displayModels, extractModels , getModelDictionaries, getModelValues, getModelUninterpretedValues , boolector, cvc4, yices, z3, mathSAT, defaultSMTCfg , compileToSMTLib, generateSMTBenchmarks- , sbvCheckSolverInstallation+ , isSBranchFeasibleInState ) where -import Control.Monad (when, unless)-import Data.List (intercalate)-import Data.Maybe (mapMaybe)-import System.FilePath (addExtension, splitExtension)-import System.Time (getClockTime)-import System.IO.Unsafe (unsafeInterleaveIO)+import Control.Monad (when, unless)+import Control.Monad.Trans (liftIO)+import Data.List (intercalate)+import Data.Maybe (mapMaybe, fromMaybe)+import System.FilePath (addExtension, splitExtension)+import System.Time (getClockTime)+import System.IO.Unsafe (unsafeInterleaveIO) import qualified Data.Set as Set (Set, toList) import Data.SBV.BitVectors.Data-import Data.SBV.BitVectors.Model import Data.SBV.SMT.SMT import Data.SBV.SMT.SMTLib import qualified Data.SBV.Provers.Boolector as Boolector@@ -50,21 +48,21 @@ import qualified Data.SBV.Provers.Z3 as Z3 import qualified Data.SBV.Provers.MathSAT as MathSAT import Data.SBV.Utils.TDiff-import Data.SBV.Utils.Boolean mkConfig :: SMTSolver -> Bool -> [String] -> SMTConfig-mkConfig s isSMTLib2 tweaks = SMTConfig { verbose = False- , timing = False- , timeOut = Nothing- , printBase = 10- , printRealPrec = 16- , smtFile = Nothing- , solver = s- , solverTweaks = tweaks- , useSMTLib2 = isSMTLib2- , satCmd = "(check-sat)"- , roundingMode = RoundNearestTiesToEven- , useLogic = Nothing+mkConfig s isSMTLib2 tweaks = SMTConfig { verbose = False+ , timing = False+ , sBranchTimeOut = Nothing+ , timeOut = Nothing+ , printBase = 10+ , printRealPrec = 16+ , smtFile = Nothing+ , solver = s+ , solverTweaks = tweaks+ , useSMTLib2 = isSMTLib2+ , satCmd = "(check-sat)"+ , roundingMode = RoundNearestTiesToEven+ , useLogic = Nothing } -- | Default configuration for the Boolector SMT solver@@ -234,16 +232,6 @@ sat :: Provable a => a -> IO SatResult sat = satWith defaultSMTCfg --- | Form the symbolic conjunction of a given list of boolean conditions. Useful in expressing--- problems with constraints, like the following:------ @--- do [x, y, z] <- sIntegers [\"x\", \"y\", \"z\"]--- solve [x .> 5, y + z .< x]--- @-solve :: [SBool] -> Symbolic SBool-solve = return . bAnd- -- | Return all satisfying assignments for a predicate, equivalent to @'allSatWith' 'defaultSMTCfg'@. -- Satisfying assignments are constructed lazily, so they will be available as returned by the solver -- and on demand.@@ -255,40 +243,8 @@ allSat :: Provable a => a -> IO AllSatResult allSat = allSatWith defaultSMTCfg --- | Check if the given constraints are satisfiable, equivalent to @'isVacuousWith' 'defaultSMTCfg'@. This--- call can be used to ensure that the specified constraints (via 'constrain') are satisfiable, i.e., that--- the proof involving these constraints is not passing vacuously. Here is an example. Consider the following--- predicate:------ >>> let pred = do { x <- forall "x"; constrain $ x .< x; return $ x .>= (5 :: SWord8) }------ This predicate asserts that all 8-bit values are larger than 5, subject to the constraint that the--- values considered satisfy @x .< x@, i.e., they are less than themselves. Since there are no values that--- satisfy this constraint, the proof will pass vacuously:------ >>> prove pred--- Q.E.D.------ We can use 'isVacuous' to make sure to see that the pass was vacuous:------ >>> isVacuous pred--- True------ While the above example is trivial, things can get complicated if there are multiple constraints with--- non-straightforward relations; so if constraints are used one should make sure to check the predicate--- is not vacuously true. Here's an example that is not vacuous:------ >>> let pred' = do { x <- forall "x"; constrain $ x .> 6; return $ x .>= (5 :: SWord8) }------ This time the proof passes as expected:------ >>> prove pred'--- Q.E.D.------ And the proof is not vacuous:------ >>> isVacuous pred'--- False+-- | Check if the given constraints are satisfiable, equivalent to @'isVacuousWith' 'defaultSMTCfg'@.+-- See the function 'constrain' for an example use of 'isVacuous'. isVacuous :: Provable a => a -> IO Bool isVacuous = isVacuousWith defaultSMTCfg @@ -373,7 +329,7 @@ -- | 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 $ forAll_ a >>= output+ Result ki tr uic is cs ts as uis ax asgn cstr _ <- runSymbolic (True, Just 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@@ -451,7 +407,7 @@ let msg = when (verbose config) . putStrLn . ("** " ++) isTiming = timing config msg "Starting symbolic simulation.."- res <- timeIf isTiming "problem construction" $ runSymbolic isSat $ (if isSat then forSome_ else forAll_) predicate >>= output+ res <- timeIf isTiming "problem construction" $ runSymbolic (isSat, Just config) $ (if isSat then forSome_ else forAll_) predicate >>= output msg $ "Generated symbolic trace:\n" ++ show res msg "Translating to SMT-Lib.." runProofOn converter config isSat comments res@@ -461,7 +417,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 (KBounded False 1) _)] ->+ Result ki _qcInfo _codeSegs is consts tbls arrs uis axs pgm cstrs [o@(SW KBool _)] -> timeIf isTiming "translation" $ let uiMap = mapMaybe arrayUIKind arrs ++ map unintFnUIKind uis skolemMap = skolemize (if isSat then is else map flipQ is)@@ -481,56 +437,23 @@ ++ "\nDetected while generating the trace:\n" ++ show res ++ "\n*** Check calls to \"output\", they are typically not needed!" --- | Check whether the given solver is installed and is ready to go. This call does a--- simple call to the solver to ensure all is well.-sbvCheckSolverInstallation :: SMTConfig -> IO Bool-sbvCheckSolverInstallation cfg = do ThmResult r <- proveWith cfg $ \x -> (x+x) .== ((x*2) :: SWord8)- case r of- Unsatisfiable _ -> return True- _ -> return False---- | Equality as a proof method. Allows for--- very concise construction of equivalence proofs, which is very typical in--- bit-precise proofs.-infix 4 ===-class Equality a where- (===) :: a -> a -> IO ThmResult--instance (SymWord a, EqSymbolic z) => Equality (SBV a -> z) where- k === l = prove $ \a -> k a .== l a--instance (SymWord a, SymWord b, EqSymbolic z) => Equality (SBV a -> SBV b -> z) where- k === l = prove $ \a b -> k a b .== l a b--instance (SymWord a, SymWord b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) where- k === l = prove $ \a b -> k (a, b) .== l (a, b)--instance (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z) where- k === l = prove $ \a b c -> k a b c .== l a b c--instance (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z) where- k === l = prove $ \a b c -> k (a, b, c) .== l (a, b, c)--instance (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z) where- k === l = prove $ \a b c d -> k a b c d .== l a b c d--instance (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z) where- k === l = prove $ \a b c d -> k (a, b, c, d) .== l (a, b, c, d)--instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) where- k === l = prove $ \a b c d e -> k a b c d e .== l a b c d e--instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) where- k === l = prove $ \a b c d e -> k (a, b, c, d, e) .== l (a, b, c, d, e)--instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) where- k === l = prove $ \a b c d e f -> k a b c d e f .== l a b c d e f--instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) where- k === l = prove $ \a b c d e f -> k (a, b, c, d, e, f) .== l (a, b, c, d, e, f)--instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) where- k === l = prove $ \a b c d e f g -> k a b c d e f g .== l a b c d e f g--instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) where- k === l = prove $ \a b c d e f g -> k (a, b, c, d, e, f, g) .== l (a, b, c, d, e, f, g)+-- | Check if a branch condition is feasible in the current state+isSBranchFeasibleInState :: State -> String -> SBool -> IO Bool+isSBranchFeasibleInState st branch cond = do+ let cfg = let pickedConfig = fromMaybe defaultSMTCfg (getSBranchRunConfig st)+ in pickedConfig { timeOut = sBranchTimeOut pickedConfig }+ msg = when (verbose cfg) . putStrLn . ("** " ++)+ sw <- sbvToSW st cond+ () <- forceSWArg sw+ Result ki tr uic is cs ts as uis ax asgn cstr _ <- liftIO $ 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]+ cvt = if useSMTLib2 cfg then toSMTLib2 else toSMTLib1+ check <- runProofOn cvt cfg True [] pgm >>= callSolver True ("sBranch: Checking " ++ show branch ++ " feasibility") SatResult cfg+ res <- case check of+ SatResult (Unsatisfiable _) -> return False+ _ -> return True -- No risks, even if it timed-our or anything else, we say it's feasible+ msg $ "sBranch: Conclusion: " ++ if res then "Feasible" else "Unfeasible"+ return res
Data/SBV/Provers/SExpr.hs view
@@ -11,10 +11,9 @@ module Data.SBV.Provers.SExpr where -import Control.Monad.Error () -- for Monad (Either String) instance-import Data.Char (isDigit, ord)-import Data.List (isPrefixOf)-import Numeric (readInt, readDec, readHex, fromRat)+import Data.Char (isDigit, ord)+import Data.List (isPrefixOf)+import Numeric (readInt, readDec, readHex, fromRat) import Data.SBV.BitVectors.AlgReals import Data.SBV.BitVectors.Data (nan, infinity)
Data/SBV/Provers/Yices.hs view
@@ -31,7 +31,7 @@ -- The default options are @\"-m -f\"@, which is valid for Yices 2.1 series. You can use the @SBV_YICES_OPTIONS@ environment variable to override the options. yices :: SMTSolver yices = SMTSolver {- name = "Yices"+ name = Yices , executable = "yices-smt" -- , options = ["-tc", "-smt", "-e"] -- For Yices1 , options = ["-m", "-f"] -- For Yices2
Data/SBV/Provers/Z3.hs view
@@ -39,7 +39,7 @@ -- The default options are @\"-in -smt2\"@, which is valid for Z3 4.1. You can use the @SBV_Z3_OPTIONS@ environment variable to override the options. z3 :: SMTSolver z3 = SMTSolver {- name = "z3"+ name = Z3 , executable = "z3" , options = map (optionPrefix:) ["in", "smt2"] , engine = \cfg isSat qinps modelMap skolemMap pgm -> do@@ -72,7 +72,7 @@ where cleanErrs = intercalate "\n" . filter (not . junk) . lines junk = ("WARNING:" `isPrefixOf`) zero :: RoundingMode -> Kind -> String- zero _ (KBounded False 1) = "#b0"+ zero _ KBool = "false" zero _ (KBounded _ sz) = "#x" ++ replicate (sz `div` 4) '0' zero _ KUnbounded = "0" zero _ KReal = "0.0"@@ -89,7 +89,7 @@ extract (Left s) = ["(echo \"((" ++ show s ++ " " ++ zero rm (kindOf s) ++ "))\")"] extract (Right (s, [])) = let g = "(get-value (" ++ show s ++ "))" in getVal (kindOf s) g extract (Right (s, ss)) = let g = "(get-value ((" ++ show s ++ concat [' ' : zero rm (kindOf a) | a <- ss] ++ ")))" in getVal (kindOf s) g- getVal KReal g = ["(set-option :pp.decimal false)", g, "(set-option :pp.decimal true)", g]+ getVal KReal g = ["(set-option :pp.decimal false) " ++ g, "(set-option :pp.decimal true) " ++ g] getVal _ g = [g] addTimeOut Nothing o = o addTimeOut (Just i) o
Data/SBV/SMT/SMT.hs view
@@ -16,15 +16,13 @@ import qualified Control.Exception as C import Control.Concurrent (newEmptyMVar, takeMVar, putMVar, forkIO)-import Control.DeepSeq (NFData(..)) import Control.Monad (when, zipWithM) import Data.Char (isSpace) import Data.Int (Int8, Int16, Int32, Int64) import Data.List (intercalate, isPrefixOf, isInfixOf)-import Data.Maybe (isNothing, fromJust) import Data.Word (Word8, Word16, Word32, Word64) import System.Directory (findExecutable)-import System.Process (readProcessWithExitCode, runInteractiveProcess, waitForProcess)+import System.Process (runInteractiveProcess, waitForProcess, terminateProcess) import System.Exit (ExitCode(..)) import System.IO (hClose, hFlush, hPutStr, hGetContents, hGetLine) @@ -35,72 +33,6 @@ import Data.SBV.BitVectors.PrettyNum import Data.SBV.Utils.TDiff --- | Solver configuration. See also 'z3', 'yices', 'cvc4', and 'boolector, which are instantiations of this type for those solvers, with--- reasonable defaults. In particular, custom configuration can be created by varying those values. (Such as @z3{verbose=True}@.)------ Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does--- not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to--- emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite--- precision value on the screen. The field 'printRealPrec' controls the printing precision, by specifying the number of digits after--- the decimal point. The default value is 16, but it can be set to any positive integer.------ When printing, SBV will add the suffix @...@ at the and of a real-value, if the given bound is not sufficient to represent the real-value--- exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it--- is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation--- of the real value is not finite, i.e., if it is not rational.-data SMTConfig = SMTConfig {- verbose :: Bool -- ^ Debug mode- , timing :: Bool -- ^ Print timing information on how long different phases took (construction, solving, etc.)- , timeOut :: Maybe Int -- ^ How much time to give to the solver. (In seconds)- , printBase :: Int -- ^ Print integral literals in this base (2, 8, and 10, and 16 are supported.)- , printRealPrec :: Int -- ^ Print algebraic real values with this precision. (SReal, default: 16)- , solverTweaks :: [String] -- ^ Additional lines of script to give to the solver (user specified)- , satCmd :: String -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics.- , smtFile :: Maybe FilePath -- ^ If Just, the generated SMT script will be put in this file (for debugging purposes mostly)- , useSMTLib2 :: Bool -- ^ If True, we'll treat the solver as using SMTLib2 input format. Otherwise, SMTLib1- , solver :: SMTSolver -- ^ The actual SMT solver.- , roundingMode :: RoundingMode -- ^ Rounding mode to use for floating-point conversions- , useLogic :: Maybe Logic -- ^ If Nothing, pick automatically. Otherwise, either use the given one, or use the custom string.- }---- | An SMT engine-type SMTEngine = SMTConfig -> Bool -> [(Quantifier, NamedSymVar)] -> [(String, UnintKind)] -> [Either SW (SW, [SW])] -> String -> IO SMTResult---- | An SMT solver-data SMTSolver = SMTSolver {- name :: String -- ^ Printable name of the solver- , executable :: String -- ^ The path to its executable- , options :: [String] -- ^ Options to provide to the solver- , engine :: SMTEngine -- ^ The solver engine, responsible for interpreting solver output- , xformExitCode :: ExitCode -> ExitCode -- ^ Should we re-interpret exit codes. Most solvers behave rationally, i.e., id will do. Some (like CVC4) don't.- , capabilities :: SolverCapabilities -- ^ Various capabilities of the solver- }---- | A model, as returned by a solver-data SMTModel = SMTModel {- modelAssocs :: [(String, CW)] -- ^ Mapping of symbolic values to constants.- , modelArrays :: [(String, [String])] -- ^ Arrays, very crude; only works with Yices.- , modelUninterps :: [(String, [String])] -- ^ Uninterpreted funcs; very crude; only works with Yices.- }- deriving Show---- | The result of an SMT solver call. Each constructor is tagged with--- the 'SMTConfig' that created it so that further tools can inspect it--- and build layers of results, if needed. For ordinary uses of the library,--- this type should not be needed, instead use the accessor functions on--- it. (Custom Show instances and model extractors.)-data SMTResult = Unsatisfiable SMTConfig -- ^ Unsatisfiable- | Satisfiable SMTConfig SMTModel -- ^ Satisfiable with model- | Unknown SMTConfig SMTModel -- ^ Prover returned unknown, with a potential (possibly bogus) model- | ProofError SMTConfig [String] -- ^ Prover errored out- | TimeOut SMTConfig -- ^ Computation timed out (see the 'timeout' combinator)---- | A script, to be passed to the solver.-data SMTScript = SMTScript {- scriptBody :: String -- ^ Initial feed- , scriptModel :: Maybe String -- ^ Optional continuation script, if the result is sat- }- -- | Extract the final configuration from a result resultConfig :: SMTResult -> SMTConfig resultConfig (Unsatisfiable c) = c@@ -109,16 +41,6 @@ resultConfig (ProofError c _) = c resultConfig (TimeOut c) = c -instance NFData SMTResult where- rnf (Unsatisfiable _) = ()- rnf (Satisfiable _ xs) = rnf xs `seq` ()- rnf (Unknown _ xs) = rnf xs `seq` ()- rnf (ProofError _ xs) = rnf xs `seq` ()- rnf (TimeOut _) = ()--instance NFData SMTModel where- rnf (SMTModel assocs unints uarrs) = rnf assocs `seq` rnf unints `seq` rnf uarrs `seq` ()- -- | A 'prove' call results in a 'ThmResult' newtype ThmResult = ThmResult SMTResult @@ -130,17 +52,19 @@ -- we should warn the user about prefix-existentials. newtype AllSatResult = AllSatResult (Bool, [SMTResult]) +-- | User friendly way of printing theorem results instance Show ThmResult where show (ThmResult r) = showSMTResult "Q.E.D." "Unknown" "Unknown. Potential counter-example:\n" "Falsifiable" "Falsifiable. Counter-example:\n" r +-- | User friendly way of printing satisfiablity results instance Show SatResult where show (SatResult r) = showSMTResult "Unsatisfiable" "Unknown" "Unknown. Potential model:\n" "Satisfiable" "Satisfiable. Model:\n" r --- NB. The Show instance of AllSatResults have to be careful in being lazy enough+-- | 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. instance Show AllSatResult where show (AllSatResult (e, xs)) = go (0::Int) xs@@ -181,47 +105,69 @@ 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+-- | Base case for 'SatModel' at unit type. Comes in handy if there are no real variables. instance SatModel () where parseCWs xs = return ((), xs) +-- | 'Bool' as extracted from a model instance SatModel Bool where- parseCWs xs = do (x, r) <- genParse (KBounded False 1) xs+ parseCWs xs = do (x, r) <- genParse KBool xs return ((x :: Integer) /= 0, r) +-- | 'Word8' as extracted from a model instance SatModel Word8 where parseCWs = genParse (KBounded False 8) +-- | 'Int8' as extracted from a model instance SatModel Int8 where parseCWs = genParse (KBounded True 8) +-- | 'Word16' as extracted from a model instance SatModel Word16 where parseCWs = genParse (KBounded False 16) +-- | 'Int16' as extracted from a model instance SatModel Int16 where parseCWs = genParse (KBounded True 16) +-- | 'Word32' as extracted from a model instance SatModel Word32 where parseCWs = genParse (KBounded False 32) +-- | 'Int32' as extracted from a model instance SatModel Int32 where parseCWs = genParse (KBounded True 32) +-- | 'Word64' as extracted from a model instance SatModel Word64 where parseCWs = genParse (KBounded False 64) +-- | 'Int64' as extracted from a model instance SatModel Int64 where parseCWs = genParse (KBounded True 64) +-- | 'Integer' as extracted from a model instance SatModel Integer where parseCWs = genParse KUnbounded +-- | 'AlgReal' as extracted from a model instance SatModel AlgReal where 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..+-- | 'Float' as extracted from a model+instance SatModel Float where+ parseCWs (CW KFloat (CWFloat i) : r) = Just (i, r)+ parseCWs _ = Nothing++-- | 'Double' as extracted from a model+instance SatModel Double where+ parseCWs (CW KDouble (CWDouble i) : r) = Just (i, r)+ parseCWs _ = Nothing++-- | A list of values as extracted from a model. When reading a list, we+-- go as long as we can (maximal-munch). Note that this never fails, as+-- we can always return the empty list! instance SatModel a => SatModel [a] where parseCWs [] = Just ([], []) parseCWs xs = case parseCWs xs of@@ -230,31 +176,37 @@ Nothing -> Just ([], ys) Nothing -> Just ([], xs) +-- | Tuples extracted from a model instance (SatModel a, SatModel b) => SatModel (a, b) where parseCWs as = do (a, bs) <- parseCWs as (b, cs) <- parseCWs bs return ((a, b), cs) +-- | 3-Tuples extracted from a model instance (SatModel a, SatModel b, SatModel c) => SatModel (a, b, c) where parseCWs as = do (a, bs) <- parseCWs as ((b, c), ds) <- parseCWs bs return ((a, b, c), ds) +-- | 4-Tuples extracted from a model instance (SatModel a, SatModel b, SatModel c, SatModel d) => SatModel (a, b, c, d) where parseCWs as = do (a, bs) <- parseCWs as ((b, c, d), es) <- parseCWs bs return ((a, b, c, d), es) +-- | 5-Tuples extracted from a model instance (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e) => SatModel (a, b, c, d, e) where parseCWs as = do (a, bs) <- parseCWs as ((b, c, d, e), fs) <- parseCWs bs return ((a, b, c, d, e), fs) +-- | 6-Tuples extracted from a model instance (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f) => SatModel (a, b, c, d, e, f) where parseCWs as = do (a, bs) <- parseCWs as ((b, c, d, e, f), gs) <- parseCWs bs return ((a, b, c, d, e, f), gs) +-- | 7-Tuples extracted from a model instance (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f, SatModel g) => SatModel (a, b, c, d, e, f, g) where parseCWs as = do (a, bs) <- parseCWs as ((b, c, d, e, f, g), hs) <- parseCWs bs@@ -304,16 +256,19 @@ getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String] getModelUninterpretedValues s (AllSatResult (_, xs)) = map (s `getModelUninterpretedValue`) xs +-- | 'ThmResult' as a generic model provider instance Modelable ThmResult where getModel (ThmResult r) = getModel r modelExists (ThmResult r) = modelExists r getModelDictionary (ThmResult r) = getModelDictionary r +-- | 'SatResult' as a generic model provider instance Modelable SatResult where getModel (SatResult r) = getModel r modelExists (SatResult r) = modelExists r getModelDictionary (SatResult r) = getModelDictionary r +-- | 'SMTResult' as a generic model provider instance Modelable SMTResult where getModel (Unsatisfiable _) = Left "SBV.getModel: Unsatisfiable result" getModel (Unknown _ m) = Right (True, parseModelOut m)@@ -388,8 +343,9 @@ where shC s = " " ++ s -- | Helper function to spin off to an SMT solver.-pipeProcess :: SMTConfig -> String -> String -> [String] -> SMTScript -> (String -> String) -> IO (Either String [String])-pipeProcess cfg nm execName opts script cleanErrs = do+pipeProcess :: SMTConfig -> String -> [String] -> SMTScript -> (String -> String) -> IO (Either String [String])+pipeProcess cfg execName opts script cleanErrs = do+ let nm = show (name (solver cfg)) mbExecPath <- findExecutable execName case mbExecPath of Nothing -> return $ Left $ "Unable to locate executable for " ++ nm@@ -428,13 +384,13 @@ exec = executable smtSolver opts = options smtSolver isTiming = timing config- nmSolver = name smtSolver+ nmSolver = show (name smtSolver) msg $ "Calling: " ++ show (unwords (exec:opts)) case smtFile config of Nothing -> return () Just f -> do msg $ "Saving the generated script in file: " ++ show f writeFile f (scriptBody script)- contents <- timeIf isTiming nmSolver $ pipeProcess config nmSolver exec opts script cleanErrs+ contents <- timeIf isTiming nmSolver $ pipeProcess config exec opts script cleanErrs msg $ nmSolver ++ " output:\n" ++ either id (intercalate "\n") contents case contents of Left e -> return $ failure (lines e)@@ -444,41 +400,46 @@ -- and can speak SMT-Lib2 (just a little). runSolver :: SMTConfig -> FilePath -> [String] -> SMTScript -> IO (ExitCode, String, String) runSolver cfg execPath opts script- | isNothing $ scriptModel script- = let checkCmd | useSMTLib2 cfg = '\n' : satCmd cfg- | True = ""- in readProcessWithExitCode execPath opts (scriptBody script ++ checkCmd)- | True- = do (send, ask, cleanUp) <- do+ = do (send, ask, cleanUp, pid) <- do (inh, outh, errh, pid) <- runInteractiveProcess execPath opts Nothing Nothing let send l = hPutStr inh (l ++ "\n") >> hFlush inh- recv = hGetLine outh `C.catch` (\(_ :: C.SomeException) -> return "")+ recv = hGetLine outh ask l = send l >> recv- cleanUp r = do outMVar <- newEmptyMVar- out <- hGetContents outh- _ <- forkIO $ C.evaluate (length out) >> putMVar outMVar ()- err <- hGetContents errh- _ <- forkIO $ C.evaluate (length err) >> putMVar outMVar ()- hClose inh- takeMVar outMVar- takeMVar outMVar- hClose outh- hClose errh- ex <- waitForProcess pid- -- if the status is unknown, prepare for the possibility of not having a model- -- TBD: This is rather crude and potentially Z3 specific- return $ if "unknown" `isPrefixOf` r && "error" `isInfixOf` (out ++ err)- then (ExitSuccess, r , "")- else (ex, r ++ "\n" ++ out, err)- return (send, ask, cleanUp)- mapM_ send (lines (scriptBody script))- r <- ask $ satCmd cfg- when (any (`isPrefixOf` r) ["sat", "unknown"]) $ do- let mls = lines (fromJust (scriptModel script))- when (verbose cfg) $ do putStrLn "** Sending the following model extraction commands:"- mapM_ putStrLn mls- mapM_ send mls- cleanUp r+ cleanUp response+ = do hClose inh+ outMVar <- newEmptyMVar+ out <- hGetContents outh+ _ <- forkIO $ C.evaluate (length out) >> putMVar outMVar ()+ err <- hGetContents errh+ _ <- forkIO $ C.evaluate (length err) >> putMVar outMVar ()+ takeMVar outMVar+ takeMVar outMVar+ hClose outh+ hClose errh+ ex <- waitForProcess pid+ return $ case response of+ Nothing -> (ex, out, err)+ Just (r, vals) -> -- if the status is unknown, prepare for the possibility of not having a model+ -- TBD: This is rather crude and potentially Z3 specific+ let finalOut = intercalate "\n" (r : vals)+ in if "unknown" `isPrefixOf` r && "error" `isInfixOf` (out ++ err)+ then (ExitSuccess, finalOut , "")+ else (ex, finalOut ++ "\n" ++ out, err)+ return (send, ask, cleanUp, pid)+ let executeSolver = do mapM_ send (lines (scriptBody script))+ response <- case scriptModel script of+ Nothing -> do send $ satCmd cfg+ return Nothing+ Just ls -> do r <- ask $ satCmd cfg+ vals <- if any (`isPrefixOf` r) ["sat", "unknown"]+ then do let mls = lines ls+ when (verbose cfg) $ do putStrLn "** Sending the following model extraction commands:"+ mapM_ putStrLn mls+ mapM ask mls+ else return []+ return $ Just (r, vals)+ cleanUp response+ executeSolver `C.onException` terminateProcess pid -- | 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
Data/SBV/SMT/SMTLib.hs view
@@ -14,7 +14,6 @@ import Data.Char (isDigit) import Data.SBV.BitVectors.Data-import Data.SBV.SMT.SMT import Data.SBV.Provers.SExpr import qualified Data.SBV.SMT.SMTLib1 as SMT1 import qualified Data.SBV.SMT.SMTLib2 as SMT2
Data/SBV/SMT/SMTLib1.hs view
@@ -154,7 +154,7 @@ -- no need to worry about Int/Real here as we don't support them with the SMTLib1 interface.. cvtCW :: CW -> String-cvtCW (CW (KBounded False 1) (CWInteger v)) = if v == 0 then "false" else "true"+cvtCW (CW KBool (CWInteger v)) = if v == 0 then "false" else "true" 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..@@ -263,7 +263,7 @@ cvtType (SBVType xs) = unwords $ map kindType xs kindType :: Kind -> String-kindType (KBounded False 1) = "Bool"+kindType KBool = "Bool" kindType (KBounded _ s) = "BitVec[" ++ show s ++ "]" kindType KUnbounded = die "unbounded Integer" kindType KReal = die "real value"
Data/SBV/SMT/SMTLib2.hs view
@@ -13,6 +13,7 @@ module Data.SBV.SMT.SMTLib2(cvt, addNonEqConstraints) where import Data.Bits (bit)+import Data.Char (intToDigit) import Data.Function (on) import Data.Ord (comparing) import qualified Data.Foldable as F (toList)@@ -20,7 +21,7 @@ import qualified Data.IntMap as IM import qualified Data.Set as Set import Data.List (intercalate, partition, groupBy, sortBy)-import Numeric (showHex)+import Numeric (showIntAtBase, showHex) import Data.SBV.BitVectors.AlgReals import Data.SBV.BitVectors.Data@@ -264,7 +265,7 @@ swFunType ss s = "(" ++ unwords (map swType ss) ++ ") " ++ swType s smtType :: Kind -> String-smtType (KBounded False 1) = "Bool"+smtType KBool = "Bool" smtType (KBounded _ sz) = "(_ BitVec " ++ show sz ++ ")" smtType KUnbounded = "Int" smtType KReal = "Real"@@ -287,11 +288,16 @@ | True = show s --- NB. The following works with SMTLib2 since all sizes are multiples of 4 (or just 1, which is specially handled)+-- Carefully code hex numbers, SMTLib is picky about lengths of hex constants. For the time+-- being, SBV only supports sizes that are multiples of 4, but the below code is more robust+-- in case of future extensions to support arbitrary sizes. hex :: Int -> Integer -> String hex 1 v = "#b" ++ show v-hex sz v = "#x" ++ pad (sz `div` 4) (showHex v "")- where pad n s = replicate (n - length s) '0' ++ s+hex sz v+ | sz `mod` 4 == 0 = "#x" ++ pad (sz `div` 4) (showHex v "")+ | True = "#b" ++ pad sz (showBin v "")+ where pad n s = replicate (n - length s) '0' ++ s+ showBin = showIntAtBase 2 intToDigit cvtCW :: RoundingMode -> CW -> String cvtCW rm x@@ -335,7 +341,8 @@ boolOp = all isBoolean arguments bad | intOp = error $ "SBV.SMTLib2: Unsupported operation on unbounded integers: " ++ show expr | True = error $ "SBV.SMTLib2: Unsupported operation on real values: " ++ show expr- ensureBV = bvOp || bad+ ensureBVOrBool = bvOp || boolOp || bad+ ensureBV = bvOp || bad addRM s = s ++ " " ++ smtRoundingMode rm lift2 o _ [x, y] = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")" lift2 o _ sbvs = error $ "SBV.SMTLib2.sh.lift2: Unexpected arguments: " ++ show (o, sbvs)@@ -368,6 +375,7 @@ | needsCheck = "(ite " ++ cond ++ ssw e ++ " " ++ lkUp ++ ")" | True = lkUp where needsCheck = case aKnd of+ KBool -> (2::Integer) > fromIntegral l KBounded _ n -> (2::Integer)^n > fromIntegral l KUnbounded -> True KReal -> error "SBV.SMT.SMTLib2.cvtExp: unexpected real valued index"@@ -379,6 +387,7 @@ | hasSign i = "(or " ++ le0 ++ " " ++ gtl ++ ") " | True = gtl ++ " " (less, leq) = case aKnd of+ KBool -> error "SBV.SMT.SMTLib2.cvtExp: unexpected boolean valued index" KBounded{} -> if hasSign i then ("bvslt", "bvsle") else ("bvult", "bvule") KUnbounded -> ("<", "<=") KReal -> ("<", "<=")@@ -419,7 +428,7 @@ | intOp = "(div " ++ ssw a ++ " " ++ show (bit i :: Integer) ++ ")" -- Implement shiftR by division by 2^i | True = bad sh (SBVApp op args)- | Just f <- lookup op smtBVOpTable, ensureBV+ | Just f <- lookup op smtBVOpTable, ensureBVOrBool = f (any hasSign args) (map ssw args) where -- The first 4 operators below do make sense for Integer's in Haskell, but there's -- no obvious counterpart for them in the SMTLib translation.
Data/SBV/Tools/ExpectedValue.hs view
@@ -22,13 +22,13 @@ -- warm-up count and the convergence factor. Maximum iteration count can also -- be specified, at which point convergence won't be sought. The boolean controls verbosity. expectedValueWith :: Outputtable a => Bool -> Int -> Maybe Int -> Double -> Symbolic a -> IO [Double]-expectedValueWith verbose warmupCount mbMaxIter epsilon m+expectedValueWith chatty warmupCount mbMaxIter epsilon m | warmupCount < 0 || epsilon < 0 = error $ "SBV.expectedValue: warmup count and epsilon both must be non-negative, received: " ++ show (warmupCount, epsilon) | True = warmup warmupCount (repeat 0) >>= go warmupCount- where progress s | not verbose = return ()- | True = putStr $ "\r*** " ++ s+ where progress s | not chatty = return ()+ | True = putStr $ "\r*** " ++ s warmup :: Int -> [Integer] -> IO [Integer] warmup 0 v = do progress $ "Warmup complete, performed " ++ show warmupCount ++ " rounds.\n" return v@@ -42,7 +42,7 @@ 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+ (KBool, _) -> 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."
Data/SBV/Tools/GenTest.hs view
@@ -111,7 +111,7 @@ valOf [x] = s x valOf xs = "[" ++ intercalate ", " (map s xs) ++ "]" t cw = case kindOf cw of- KBounded False 1 -> "Bool"+ KBool -> "Bool" KBounded False 8 -> "Word8" KBounded False 16 -> "Word16" KBounded False 32 -> "Word32"@@ -127,7 +127,7 @@ 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 ' ')+ KBool -> take 5 (show (cwToBool cw) ++ repeat ' ') 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 KFloat -> let CWFloat w = cwVal cw in showHFloat w@@ -198,7 +198,7 @@ ] where mkField p cw i = " " ++ t ++ " " ++ p ++ show i ++ ";" where t = case cwKind cw of- KBounded False 1 -> "SBool"+ KBool -> "SBool" KBounded False 8 -> "SWord8" KBounded False 16 -> "SWord16" KBounded False 32 -> "SWord32"@@ -215,7 +215,7 @@ _ -> 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"+ KBool -> 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 KFloat -> let CWFloat w = cwVal cw in showCFloat w@@ -231,11 +231,11 @@ inp cw i = mkBool cw (n ++ "[i].input.i" ++ show i) out cw i = mkBool cw (n ++ "[i].output.o" ++ show i) mkBool cw s = case cwKind cw of- KBounded False 1 -> "(" ++ s ++ " == true) ? \"true \" : \"false\""- _ -> s+ KBool -> "(" ++ s ++ " == true) ? \"true \" : \"false\""+ _ -> s fmtString = unwords (map fmt is) ++ " -> " ++ unwords (map fmt os) fmt cw = case cwKind cw of- KBounded False 1 -> "%s"+ KBool -> "%s" KBounded False 8 -> "0x%02\"PRIx8\"" KBounded False 16 -> "0x%04\"PRIx16\"U" KBounded False 32 -> "0x%08\"PRIx32\"UL"@@ -267,7 +267,7 @@ toF True = '1' toF False = '0' blast cw = case cwKind cw of- KBounded False 1 -> [toF (cwToBool cw)]+ KBool -> [toF (cwToBool cw)] KBounded False 8 -> xlt 8 (cwVal cw) KBounded False 16 -> xlt 16 (cwVal cw) KBounded False 32 -> xlt 32 (cwVal cw)
Data/SBV/Tools/Optimize.hs view
@@ -19,7 +19,7 @@ import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.Model (OrdSymbolic(..), EqSymbolic(..)) import Data.SBV.Provers.Prover (satWith, defaultSMTCfg)-import Data.SBV.SMT.SMT (SatModel, getModel, SMTConfig(..))+import Data.SBV.SMT.SMT (SatModel, getModel) import Data.SBV.Utils.Boolean -- | Optimizer configuration. Note that iterative and quantified approaches are in general not interchangeable.
Data/SBV/Tools/Polynomial.hs view
@@ -9,6 +9,7 @@ -- Implementation of polynomial arithmetic ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE PatternGuards #-}@@ -100,7 +101,11 @@ | True = foldr (\x y -> sh x ++ " + " ++ y) (sh (last cs)) (init cs) ++ t where t | st = " :: GF(2^" ++ show n ++ ")" | True = ""+#if __GLASGOW_HASKELL__ >= 708+ n = maybe (error "SBV.Polynomial.sp: Unexpected non-finite usage!") id (bitSizeMaybe a)+#else n = bitSize a+#endif is = [n-1, n-2 .. 0] cs = map fst $ filter snd $ zip is (map (testBit a) is) sh 0 = "1"
README.md view
@@ -1,3 +1,21 @@++<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 ======================================
SBVUnitTest/Examples/Basics/BasicTests.hs view
@@ -21,22 +21,22 @@ test0 f = f (3 :: Word8) 2 test1, test2, test3, test4, test5 :: (forall a. Num a => (a -> a -> a)) -> IO Result-test1 f = runSymbolic True $ do let x = literal (3 :: Word8)- y = literal (2 :: Word8)- output $ f x y-test2 f = runSymbolic True $ do let x = literal (3 :: Word8)- y :: SWord8 <- forall "y"- output $ f x y-test3 f = runSymbolic True $ do x :: SWord8 <- forall "x"- y :: SWord8 <- forall "y"- output $ f x y-test4 f = runSymbolic True $ do x :: SWord8 <- forall "x"- output $ f x x-test5 f = runSymbolic True $ do x :: SWord8 <- forall "x"- let r = f x x- q :: SWord8 <- forall "q"- _ <- output q- output r+test1 f = runSymbolic (True, Nothing) $ do let x = literal (3 :: Word8)+ y = literal (2 :: Word8)+ output $ f x y+test2 f = runSymbolic (True, Nothing) $ do let x = literal (3 :: Word8)+ y :: SWord8 <- forall "y"+ output $ f x y+test3 f = runSymbolic (True, Nothing) $ do x :: SWord8 <- forall "x"+ y :: SWord8 <- forall "y"+ output $ f x y+test4 f = runSymbolic (True, Nothing) $ do x :: SWord8 <- forall "x"+ output $ f x x+test5 f = runSymbolic (True, Nothing) $ do x :: SWord8 <- forall "x"+ let r = f x x+ q :: SWord8 <- forall "q"+ _ <- output q+ output r f1, f2, f3, f4, f5 :: Num a => a -> a -> a f1 x y = (x+y)*(x-y)
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String-buildTime = "Sun Feb 16 15:11:29 PST 2014"+buildTime = "Fri Jul 11 22:53:51 PDT 2014"
SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs view
@@ -12,6 +12,7 @@ {-# LANGUAGE Rank2Types #-} {-# LANGUAGE TupleSections #-}+{-# LANGUAGE CPP #-} module TestSuite.Basics.ArithNoSolver(testSuite) where @@ -19,6 +20,13 @@ import SBVTest +ghcBitSize :: Bits a => a -> Int+#if __GLASGOW_HASKELL__ >= 708+ghcBitSize x = maybe (error "SBV.ghcBitSize: Unexpected non-finite usage!") id (bitSizeMaybe x)+#else+ghcBitSize = bitSize+#endif+ -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test $@@ -114,14 +122,14 @@ genIntTestS :: String -> (forall a. (Num a, Bits a) => a -> Int -> a) -> [Test] genIntTestS nm op = map mkTest $- zipWith pair [("u8", show x, show y, x `op` y) | x <- w8s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw8s, y <- [0 .. (bitSize x - 1)]]- ++ zipWith pair [("u16", show x, show y, x `op` y) | x <- w16s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw16s, y <- [0 .. (bitSize x - 1)]]- ++ zipWith pair [("u32", show x, show y, x `op` y) | x <- w32s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw32s, y <- [0 .. (bitSize x - 1)]]- ++ zipWith pair [("u64", show x, show y, x `op` y) | x <- w64s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw64s, y <- [0 .. (bitSize x - 1)]]- ++ zipWith pair [("s8", show x, show y, x `op` y) | x <- i8s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si8s, y <- [0 .. (bitSize x - 1)]]- ++ zipWith pair [("s16", show x, show y, x `op` y) | x <- i16s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si16s, y <- [0 .. (bitSize x - 1)]]- ++ zipWith pair [("s32", show x, show y, x `op` y) | x <- i32s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si32s, y <- [0 .. (bitSize x - 1)]]- ++ zipWith pair [("s64", show x, show y, x `op` y) | x <- i64s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si64s, y <- [0 .. (bitSize x - 1)]]+ zipWith pair [("u8", show x, show y, x `op` y) | x <- w8s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- sw8s, y <- [0 .. (ghcBitSize x - 1)]]+ ++ zipWith pair [("u16", show x, show y, x `op` y) | x <- w16s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- sw16s, y <- [0 .. (ghcBitSize x - 1)]]+ ++ zipWith pair [("u32", show x, show y, x `op` y) | x <- w32s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- sw32s, y <- [0 .. (ghcBitSize x - 1)]]+ ++ zipWith pair [("u64", show x, show y, x `op` y) | x <- w64s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- sw64s, y <- [0 .. (ghcBitSize x - 1)]]+ ++ zipWith pair [("s8", show x, show y, x `op` y) | x <- i8s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- si8s, y <- [0 .. (ghcBitSize x - 1)]]+ ++ zipWith pair [("s16", show x, show y, x `op` y) | x <- i16s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- si16s, y <- [0 .. (ghcBitSize x - 1)]]+ ++ zipWith pair [("s32", show x, show y, x `op` y) | x <- i32s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- si32s, y <- [0 .. (ghcBitSize x - 1)]]+ ++ zipWith pair [("s64", show x, show y, x `op` y) | x <- i64s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- si64s, y <- [0 .. (ghcBitSize x - 1)]] ++ zipWith pair [("iUB", show x, show y, x `op` y) | x <- iUBs, y <- [0 .. 10]] [x `op` y | x <- siUBs, y <- [0 .. 10 ]] where pair (t, x, y, a) b = (t, x, y, show a, show b, show (fromIntegral a `asTypeOf` b) == show b) mkTest (t, x, y, a, b, s) = "arithCF-" ++ nm ++ "." ++ t ++ "_" ++ x ++ "_" ++ y ++ "_" ++ a ++ "_" ++ b ~: s `showsAs` "True"
SBVUnitTest/TestSuite/Basics/ArithSolver.hs view
@@ -13,6 +13,7 @@ {-# LANGUAGE Rank2Types #-} {-# LANGUAGE TupleSections #-}+{-# LANGUAGE CPP #-} module TestSuite.Basics.ArithSolver(testSuite) where @@ -20,10 +21,19 @@ import SBVTest +ghcBitSize :: Bits a => a -> Int+#if __GLASGOW_HASKELL__ >= 708+ghcBitSize x = maybe (error "SBV.ghcBitSize: Unexpected non-finite usage!") id (bitSizeMaybe x)+#else+ghcBitSize = bitSize+#endif+ -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test $ genReals+ ++ genFloats+ ++ genDoubles ++ genQRems ++ genBinTest True "+" (+) ++ genBinTest True "-" (-)@@ -66,7 +76,7 @@ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- i32s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- i64s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | unboundedOK, x <- iUBs, y <- iUBs]- where mkTest (x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t+ where mkTest (x, y, t) = "genBinTest.arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t mkThm2 x y r = isThm $ do [a, b] <- mapM free ["x", "y"] constrain $ a .== literal x constrain $ b .== literal y@@ -82,7 +92,7 @@ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- i32s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- i64s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- iUBs, y <- iUBs]- where mkTest (x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t+ where mkTest (x, y, t) = "genBoolTest.arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t mkThm2 x y r = isThm $ do [a, b] <- mapM free ["x", "y"] constrain $ a .== literal x constrain $ b .== literal y@@ -98,7 +108,7 @@ ++ [(show x, mkThm x (op x)) | x <- i32s] ++ [(show x, mkThm x (op x)) | x <- i64s] ++ [(show x, mkThm x (op x)) | unboundedOK, x <- iUBs]- where mkTest (x, t) = "arithmetic-" ++ nm ++ "." ++ x ~: assert t+ where mkTest (x, t) = "genUnTest.arithmetic-" ++ nm ++ "." ++ x ~: assert t mkThm x r = isThm $ do a <- free "x" constrain $ a .== literal x return $ literal r .== op a@@ -113,7 +123,7 @@ ++ [("s32", show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- is] ++ [("s64", show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- is] ++ [("iUB", show x, show y, mkThm2 x y (x `op` y)) | x <- iUBs, y <- is]- where mkTest (l, x, y, t) = "arithmetic-" ++ nm ++ "." ++ l ++ "_" ++ x ++ "_" ++ y ~: assert t+ where mkTest (l, x, y, t) = "genIntTest.arithmetic-" ++ nm ++ "." ++ l ++ "_" ++ x ++ "_" ++ y ~: assert t is = [-10 .. 10] mkThm2 x y r = isThm $ do a <- free "x" constrain $ a .== literal x@@ -121,16 +131,16 @@ genIntTestS :: Bool -> String -> (forall a. (Num a, Bits a) => a -> Int -> a) -> [Test]-genIntTestS unboundedOK nm op = map mkTest $ [("u8", show x, show y, mkThm2 x y (x `op` y)) | x <- w8s, y <- [0 .. (bitSize x - 1)]]- ++ [("u16", show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- [0 .. (bitSize x - 1)]]- ++ [("u32", show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- [0 .. (bitSize x - 1)]]- ++ [("u64", show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- [0 .. (bitSize x - 1)]]- ++ [("s8", show x, show y, mkThm2 x y (x `op` y)) | x <- i8s, y <- [0 .. (bitSize x - 1)]]- ++ [("s16", show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- [0 .. (bitSize x - 1)]]- ++ [("s32", show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- [0 .. (bitSize x - 1)]]- ++ [("s64", show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- [0 .. (bitSize x - 1)]]+genIntTestS unboundedOK nm op = map mkTest $ [("u8", show x, show y, mkThm2 x y (x `op` y)) | x <- w8s, y <- [0 .. (ghcBitSize x - 1)]]+ ++ [("u16", show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- [0 .. (ghcBitSize x - 1)]]+ ++ [("u32", show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- [0 .. (ghcBitSize x - 1)]]+ ++ [("u64", show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- [0 .. (ghcBitSize x - 1)]]+ ++ [("s8", show x, show y, mkThm2 x y (x `op` y)) | x <- i8s, y <- [0 .. (ghcBitSize x - 1)]]+ ++ [("s16", show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- [0 .. (ghcBitSize x - 1)]]+ ++ [("s32", show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- [0 .. (ghcBitSize x - 1)]]+ ++ [("s64", show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- [0 .. (ghcBitSize x - 1)]] ++ [("iUB", show x, show y, mkThm2 x y (x `op` y)) | unboundedOK, x <- iUBs, y <- [0 .. 10]]- where mkTest (l, x, y, t) = "arithmetic-" ++ nm ++ "." ++ l ++ "_" ++ x ++ "_" ++ y ~: assert t+ where mkTest (l, x, y, t) = "genIntTestS.arithmetic-" ++ nm ++ "." ++ l ++ "_" ++ x ++ "_" ++ y ~: assert t mkThm2 x y r = isThm $ do a <- free "x" constrain $ a .== literal x return $ literal r .== a `op` y@@ -152,7 +162,7 @@ ++ [(show x, mkThm fromBitsBE blastBE x) | x <- w64s] ++ [(show x, mkThm fromBitsLE blastLE x) | x <- i64s] ++ [(show x, mkThm fromBitsBE blastBE x) | x <- i64s]- where mkTest (x, t) = "blast-" ++ show x ~: assert t+ where mkTest (x, t) = "genBlasts.blast-" ++ show x ~: assert t mkThm from to v = isThm $ do a <- free "x" constrain $ a .== literal v return $ a .== from (to a)@@ -176,7 +186,7 @@ ++ [(show x, mkFEq unsignCast (fromBitsLE . blastLE) x) | x <- i16s] ++ [(show x, mkFEq unsignCast (fromBitsLE . blastLE) x) | x <- i32s] ++ [(show x, mkFEq unsignCast (fromBitsLE . blastLE) x) | x <- i64s]- where mkTest (x, t) = "cast-" ++ show x ~: assert t+ where mkTest (x, t) = "genCasts.cast-" ++ show x ~: assert t mkThm from to v = isThm $ do a <- free "x" constrain $ a .== literal v return $ a .== from (to a)@@ -195,12 +205,46 @@ ++ [(">=", show x, show y, mkThm2 (.>=) x y (x >= y)) | x <- rs, y <- rs ] ++ [("==", show x, show y, mkThm2 (.==) x y (x == y)) | x <- rs, y <- rs ] ++ [("/=", show x, show y, mkThm2 (./=) x y (x /= y)) | x <- rs, y <- rs ]- where mkTest (nm, x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t+ where mkTest (nm, x, y, t) = "genReals.arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t mkThm2 op x y r = isThm $ do [a, b] <- mapM free ["x", "y"] constrain $ a .== literal x constrain $ b .== literal y return $ literal r .== a `op` b +genFloats :: [Test]+genFloats = genIEEE754 "genFloats" fs++genDoubles :: [Test]+genDoubles = genIEEE754 "genDoubles" ds++genIEEE754 :: (RealFloat a, Show a, SymWord a, Ord a, Floating a) => String -> [a] -> [Test]+genIEEE754 origin vs = map mkTest $ [("+", show x, show y, mkThm2 (+) x y (x + y)) | x <- vs, y <- vs ]+ ++ [("-", show x, show y, mkThm2 (-) x y (x - y)) | x <- vs, y <- vs ]+ ++ [("*", show x, show y, mkThm2 (*) x y (x * y)) | x <- vs, y <- vs ]+ ++ [("/", show x, show y, mkThm2 (/) x y (x / y)) | x <- vs, y <- vs, y /= 0]+ ++ [("<", show x, show y, mkThm2C False (.<) x y (x < y)) | x <- vs, y <- vs ]+ ++ [("<=", show x, show y, mkThm2C False (.<=) x y (x <= y)) | x <- vs, y <- vs ]+ ++ [(">", show x, show y, mkThm2C False (.>) x y (x > y)) | x <- vs, y <- vs ]+ ++ [(">=", show x, show y, mkThm2C False (.>=) x y (x >= y)) | x <- vs, y <- vs ]+ ++ [("==", show x, show y, mkThm2C False (.==) x y (x == y)) | x <- vs, y <- vs ]+ ++ [("/=", show x, show y, mkThm2C True (./=) x y (x /= y)) | x <- vs, y <- vs ]+ where mkTest (nm, x, y, t) = origin ++ ".arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t+ eqF v val+ | isNaN val = constrain $ isSNaN v+ | True = constrain $ v .== literal val+ mkThm2 op x y r = isThm $ do [a, b] <- mapM free ["x", "y"]+ eqF a x+ eqF b y+ return $ if isNaN r+ then isSNaN (a `op` b)+ else literal r .== a `op` b+ mkThm2C neq op x y r = isThm $ do [a, b] <- mapM free ["x", "y"]+ eqF a x+ eqF b y+ return $ if isNaN x || isNaN y+ then (if neq then a `op` b else bnot (a `op` b))+ else literal r .== a `op` b+ genQRems :: [Test] genQRems = map mkTest $ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- w8s, y <- w8s ] ++ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- w16s, y <- w16s]@@ -222,7 +266,7 @@ ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- iUBs, y <- iUBs] where divMod' x y = if y == 0 then (0, x) else x `divMod` y quotRem' x y = if y == 0 then (0, x) else x `quotRem` y- mkTest (nm, x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t+ mkTest (nm, x, y, t) = "genQRems.arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t mkThm2 op x y (e1, e2) = isThm $ do [a, b] <- mapM free ["x", "y"] constrain $ a .== literal x constrain $ b .== literal y@@ -263,8 +307,14 @@ iUBs = [-1000000] ++ [-1 .. 1] ++ [1000000] rs :: [AlgReal]-rs = [fromRational (i % d) | i <- is, d <- ds]- where is = [-1000000] ++ [-1 .. 1] ++ [10000001]- ds = [5,100,1000000]+rs = [fromRational (i % d) | i <- is, d <- dens]+ where is = [-1000000] ++ [-1 .. 1] ++ [10000001]+ dens = [5,100,1000000] +-- Admittedly paltry test-cases for float/double+fs :: [Float]+fs = nan : -infinity : infinity : 0 : [-5.0, -4.7 .. 5] ++ [5]++ds :: [Double]+ds = nan : -infinity : infinity : 0 : [-5.0, -4.7 .. 5] ++ [5] {-# ANN module "HLint: ignore Reduce duplication" #-}
SBVUnitTest/TestSuite/BitPrecise/Legato.hs view
@@ -23,8 +23,8 @@ "legato-1" ~: legatoPgm `goldCheck` "legato.gold" , "legato-2" ~: legatoC `goldCheck` "legato_c.gold" ]- where legatoPgm = runSymbolic True $ forAll ["mem", "addrX", "x", "addrY", "y", "addrLow", "regX", "regA", "memVals", "flagC", "flagZ"] legatoIsCorrect- >>= output+ where legatoPgm = runSymbolic (True, Nothing) $ forAll ["mem", "addrX", "x", "addrY", "y", "addrLow", "regX", "regA", "memVals", "flagC", "flagZ"] legatoIsCorrect+ >>= output legatoC = compileToC' "legatoMult" $ do cgSetDriverValues [87, 92] cgPerformRTCs True
SBVUnitTest/TestSuite/BitPrecise/PrefixSum.hs view
@@ -22,5 +22,5 @@ testSuite = mkTestSuite $ \goldCheck -> test [ "prefixSum1" ~: assert =<< isThm (flIsCorrect 8 (0, (+))) , "prefixSum2" ~: assert =<< isThm (flIsCorrect 16 (0, smax))- , "prefixSum3" ~: runSymbolic True (genPrefixSumInstance 16 >>= output) `goldCheck` "prefixSum_16.gold"+ , "prefixSum3" ~: runSymbolic (True, Nothing) (genPrefixSumInstance 16 >>= output) `goldCheck` "prefixSum_16.gold" ]
SBVUnitTest/TestSuite/CRC/CCITT.hs view
@@ -22,4 +22,4 @@ testSuite = mkTestSuite $ \goldCheck -> test [ "ccitt" ~: crcPgm `goldCheck` "ccitt.gold" ]- where crcPgm = runSymbolic True $ forAll_ crcGood >>= output+ where crcPgm = runSymbolic (True, Nothing) $ forAll_ crcGood >>= output
SBVUnitTest/TestSuite/Existentials/CRCPolynomial.hs view
@@ -22,7 +22,7 @@ testSuite = mkTestSuite $ \goldCheck -> test [ "crcPolyExist" ~: pgm `goldCheck` "crcPolyExist.gold" ]- where pgm = runSymbolic True $ do+ where pgm = runSymbolic (True, Nothing) $ do p <- exists "poly" s <- do sh <- forall "sh" sl <- forall "sl"
SBVUnitTest/TestSuite/Puzzles/Coins.hs view
@@ -22,7 +22,8 @@ testSuite = mkTestSuite $ \goldCheck -> test [ "coins" ~: coinsPgm `goldCheck` "coins.gold" ]- where coinsPgm = runSymbolic True $ do cs <- mapM mkCoin [1..6]- mapM_ constrain [c s | s <- combinations cs, length s >= 2, c <- [c1, c2, c3, c4, c5, c6]]- constrain $ bAnd $ zipWith (.>=) cs (tail cs)- output $ sum cs .== 115+ where coinsPgm = runSymbolic (True, Nothing) $ do+ cs <- mapM mkCoin [1..6]+ mapM_ constrain [c s | s <- combinations cs, length s >= 2, c <- [c1, c2, c3, c4, c5, c6]]+ constrain $ bAnd $ zipWith (.>=) cs (tail cs)+ output $ sum cs .== 115
SBVUnitTest/TestSuite/Puzzles/Counts.hs view
@@ -22,5 +22,5 @@ testSuite = mkTestSuite $ \goldCheck -> test [ "counts" ~: countPgm `goldCheck` "counts.gold" ]- where countPgm = runSymbolic True $ forAll_ puzzle' >>= output+ where countPgm = runSymbolic (True, Nothing) $ forAll_ puzzle' >>= output puzzle' d0 d1 d2 d3 d4 d5 d6 d7 d8 d9 = puzzle [d0, d1, d2, d3, d4, d5, d6, d7, d8, d9]
SBVUnitTest/TestSuite/Uninterpreted/AUF.hs view
@@ -24,4 +24,4 @@ , "auf-1" ~: assert =<< isThm thm2 , "auf-2" ~: pgm `goldCheck` "auf-1.gold" ]- where pgm = runSymbolic True $ forAll ["x", "y", "a", "initVal"] thm1 >>= output+ where pgm = runSymbolic (True, Nothing) $ forAll ["x", "y", "a", "initVal"] thm1 >>= output
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 3.0+Version: 3.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@@ -47,7 +47,7 @@ TypeOperators TypeSynonymInstances Build-Depends : base >= 4 && < 5- , array, containers, deepseq, directory, filepath, old-time+ , array, async, containers, deepseq, directory, filepath, old-time , pretty, process, mtl, QuickCheck, random, syb Exposed-modules : Data.SBV , Data.SBV.Bridge.Boolector@@ -71,6 +71,7 @@ , Data.SBV.Examples.Existentials.CRCPolynomial , Data.SBV.Examples.Existentials.Diophantine , Data.SBV.Examples.Misc.Floating+ , Data.SBV.Examples.Misc.SBranch , Data.SBV.Examples.Misc.ModelExtract , Data.SBV.Examples.Polynomials.Polynomials , Data.SBV.Examples.Puzzles.Coins