sbv 3.1 → 3.2
raw patch · 20 files changed
+452/−219 lines, 20 files
Files
- CHANGES.md +34/−2
- Data/SBV.hs +5/−3
- Data/SBV/BitVectors/Data.hs +1/−1
- Data/SBV/BitVectors/Model.hs +214/−164
- Data/SBV/BitVectors/STree.hs +3/−3
- Data/SBV/Compilers/C.hs +13/−2
- Data/SBV/Examples/BitPrecise/Legato.hs +4/−4
- Data/SBV/Examples/Puzzles/U2Bridge.hs +10/−10
- Data/SBV/Provers/Boolector.hs +2/−2
- Data/SBV/Provers/Prover.hs +29/−10
- Data/SBV/SMT/SMTLib1.hs +17/−2
- Data/SBV/SMT/SMTLib2.hs +14/−0
- SBVUnitTest/GoldFiles/iteTest1.gold +13/−0
- SBVUnitTest/GoldFiles/iteTest2.gold +13/−0
- SBVUnitTest/GoldFiles/iteTest3.gold +13/−0
- SBVUnitTest/SBVBasicTests.hs +16/−9
- SBVUnitTest/SBVTestCollection.hs +6/−4
- SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
- SBVUnitTest/TestSuite/Basics/IteTest.hs +41/−0
- sbv.cabal +3/−2
CHANGES.md view
@@ -1,13 +1,45 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 3.1+* Latest Hackage released version: 3.2 +### Version 3.2, 2014-11-18++ * Implement 'sAssert'. This adds conditional symbolic simulation, by ensuring arbitrary+ boolean conditions hold during simulation; similar to ASSERT calls in other languages.+ Note that failures will be detected at symbolic-simulation time, i.e., each assert will+ generate a call to the external solver to ensure that the condition is never violated.+ If violation is possible the user will get an error, indicating the failure conditions.++ * Also implement 'sAssertCont' which allows for a programmatic way to extract/display results+ for consumers of 'sAssert'. While the latter simply calls 'error' in case of an assertion+ violation, the 'sAssertCont' variant takes a continuation which can be used to program+ how the results should be interpreted/displayed. (This is useful for libraries built on top of+ SBV.) Note that the type of the continuation is such that execution should still stop, i.e.,+ once an assertion violation is detected, symbolic simulation will never continue.++ * Rework/simplify the 'Mergeable' class to make sure 'sBranch' is sufficiently lazy+ in case of structural merges. The original implementation was only+ lazy at the Word instance, but not at lists/tuples etc. Thanks to Brian Huffman+ for reporting this bug.++ * Add a few constant-folding optimizations for 'sDiv'and 'sRem'++ * Boolector: Modify output parser to conform to the new Boolector output format. This+ means that you need at least v2.0.0 of Boolector installed if you want to use that+ particular solver.++ * Fix long-standing translation bug regarding boolean Ord class comparisons. (i.e., + 'False > True' etc.) While Haskell allows for this, SMT-Lib does not; and hence+ we have to be careful in translating. Thanks to Brian Huffman for reporting.++ * C code generation: Correctly translate square-root and fusedMA functions to C.+ ### 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!+ in GHC 7.8.3; so upgrading to GHC 7.8.3 is essential for using SBV! New features/bug-fixes in v3.1:
Data/SBV.hs view
@@ -155,7 +155,9 @@ -- ** Polynomial arithmetic and CRCs , Polynomial(..), crcBV, crc -- ** Conditionals: Mergeable values- , Mergeable(..)+ , Mergeable(..), ite, iteLazy, sBranch+ -- ** Conditional symbolic simulation+ , sAssert, sAssertCont -- ** Symbolic equality , EqSymbolic(..) -- ** Symbolic ordering@@ -219,7 +221,7 @@ , getModelDictionaries, getModelValues, getModelUninterpretedValues -- * SMT Interface: Configurations and solvers- , SMTConfig(..), SMTLibLogic(..), Logic(..), OptimizeOpts(..), Solver(..), SMTSolver(..), boolector, cvc4, yices, z3, mathSAT, sbvCurrentSolver, defaultSMTCfg, sbvCheckSolverInstallation, sbvAvailableSolvers+ , SMTConfig(..), SMTLibLogic(..), Logic(..), OptimizeOpts(..), Solver(..), SMTSolver(..), boolector, cvc4, yices, z3, mathSAT, defaultSolverConfig, sbvCurrentSolver, defaultSMTCfg, sbvCheckSolverInstallation, sbvAvailableSolvers -- * Symbolic computations , Symbolic, output, SymWord(..)@@ -329,7 +331,7 @@ Unsatisfiable _ -> return True _ -> return False --- The default configs+-- | The default configs corresponding to supported SMT solvers defaultSolverConfig :: Solver -> SMTConfig defaultSolverConfig Z3 = z3 defaultSolverConfig Yices = yices
Data/SBV/BitVectors/Data.hs view
@@ -1369,7 +1369,7 @@ , 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.)+ , printBase :: Int -- ^ Print integral literals in this base (2, 8, 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.
Data/SBV/BitVectors/Model.hs view
@@ -22,7 +22,7 @@ module Data.SBV.BitVectors.Model ( Mergeable(..), EqSymbolic(..), OrdSymbolic(..), SDivisible(..), Uninterpreted(..), SIntegral- , sbvTestBit, sbvPopCount, setBitTo, sbvShiftLeft, sbvShiftRight, sbvSignedShiftArithRight+ , ite, iteLazy, sBranch, sAssert, sAssertCont, sbvTestBit, sbvPopCount, setBitTo, sbvShiftLeft, sbvShiftRight, sbvSignedShiftArithRight , allEqual, allDifferent, inRange, sElem, oneIf, blastBE, blastLE, fullAdder, fullMultiplier , lsb, msb, genVar, genVar_, forall, forall_, exists, exists_ , constrain, pConstrain, sBool, sBools, sWord8, sWord8s, sWord16, sWord16s, sWord32@@ -41,6 +41,8 @@ import Data.Maybe (fromMaybe) import Data.Word (Word8, Word16, Word32, Word64) +import qualified Data.Map as M+ import Test.QuickCheck (Testable(..), Arbitrary(..)) import qualified Test.QuickCheck as QC (whenFail) import qualified Test.QuickCheck.Monadic as QC (monadicIO, run)@@ -50,12 +52,10 @@ 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)+import Data.SBV.Provers.Prover (isSBranchFeasibleInState, isConditionSatisfiable, isVacuous, prove, defaultSMTCfg)+import Data.SBV.SMT.SMT (SatResult(..), ThmResult, showModel, getModelDictionary) -- | 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@@ -1082,7 +1082,19 @@ sDivMod = liftDMod liftQRem :: (SymWord a, Num a, SDivisible a) => SBV a -> SBV a -> (SBV a, SBV a)-liftQRem x y = ite (y .== 0) (0, x) (qr x y)+liftQRem x y+ | x `isConcretely` (== 0)+ = (0, 0)+ | y `isConcretely` (== 1)+ = (x, 0)+{-------------------------------+ - N.B. The seemingly innocuous variant when y == -1 only holds if the type is signed;+ - and also is problematic around the minBound.. So, we refrain from that optimization+ | y `isConcretely` (== -1)+ = (-x, 0)+--------------------------------}+ | True+ = ite (y .== 0) (0, x) (qr x y) where qr (SBV sgnsz (Left a)) (SBV _ (Left b)) = let (q, r) = sQuotRem a b in (SBV sgnsz (Left q), SBV sgnsz (Left r)) qr a@(SBV sgnsz _) b = (SBV sgnsz (Right (cache (mk Quot))), SBV sgnsz (Right (cache (mk Rem)))) where mk o st = do sw1 <- sbvToSW st a@@ -1091,7 +1103,19 @@ -- Conversion from quotRem (truncate to 0) to divMod (truncate towards negative infinity) liftDMod :: (SymWord a, Num a, SDivisible a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a)-liftDMod x y = ite (y .== 0) (0, x) $ ite (signum r .== negate (signum y)) (q-1, r+y) qr+liftDMod x y+ | x `isConcretely` (== 0)+ = (0, 0)+ | y `isConcretely` (== 1)+ = (x, 0)+{-------------------------------+ - N.B. The seemingly innocuous variant when y == -1 only holds if the type is signed;+ - and also is problematic around the minBound.. So, we refrain from that optimization+ | y `isConcretely` (== -1)+ = (-x, 0)+--------------------------------}+ | True+ = ite (y .== 0) (0, x) $ ite (signum r .== negate (signum y)) (q-1, r+y) qr where qr@(q, r) = x `sQuotRem` y -- SInteger instance for quotRem/divMod are tricky!@@ -1130,48 +1154,16 @@ -- -- Minimal complete definition: 'symbolicMerge' class Mergeable a where- -- | Merge two values based on the condition. This is intended- -- to be a "structural" copy, walking down the values and merging- -- recursively through the structure of @a@. In particular,- -- symbolicMerge should *not* waste its time testing whether the- -- condition might be a literal; that will be handled by 'ite'- -- which should be used in all user code. In particular, any- -- implementation of 'symbolicMerge' should just call 'symbolicMerge'- -- recursively in the constituents of @a@, instead of 'ite'.- symbolicMerge :: SBool -> a -> a -> a- -- | Choose one or the other element, based on the condition.- -- This is similar to 'symbolicMerge', but it has a default- -- implementation that makes sure it's short-cut if the condition is concrete.- -- 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+ -- | Merge two values based on the condition. The first argument states+ -- whether we force the then-and-else branches before the merging, at the+ -- word level. This is an efficiency concern; one that we'd rather not+ -- make but unfortunately necessary for getting symbolic simulation+ -- working efficiently.+ symbolicMerge :: Bool -> 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 select :: (SymWord b, Num b) => [a] -> a -> SBV b -> a- -- default definitions- 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@@ -1185,118 +1177,172 @@ where walk [] _ acc = acc walk (e:es) i acc = walk es (i-1) (ite (i .== 0) e acc) ++-- | If-then-else. This is by definition 'symbolicMerge' with both+-- branches forced. This is typically the desired behavior, but also+-- see 'iteLazy' should you need more laziness.+ite :: Mergeable a => SBool -> a -> a -> a+ite t a b+ | Just r <- unliteral t = if r then a else b+ | True = symbolicMerge True t a b++-- | A Lazy version of ite, which does not force its arguments. This might+-- cause issues for symbolic simulation with large thunks around, so use with+-- care.+iteLazy :: Mergeable a => SBool -> a -> a -> a+iteLazy t a b+ | Just r <- unliteral t = if r then a else b+ | True = symbolicMerge False t a b++-- | 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 :: Mergeable a => SBool -> a -> a -> a+sBranch t a b+ | Just r <- unliteral c = if r then a else b+ | True = symbolicMerge False c a b+ where c = reduceInPathCondition t++-- | Symbolic assert. Check that the given boolean condition is always true in the given path.+-- Otherwise symbolic simulation will stop with a run-time error.+sAssert :: Mergeable a => String -> SBool -> a -> a+sAssert msg = sAssertCont msg defCont+ where die m = error $ intercalate "\n" $ ("Assertion failure: " ++ show msg) : m+ defCont _ Nothing = die ["*** Fails in all assignments to inputs"]+ defCont cfg (Just md) = die [showModel cfg (SMTModel (M.toList md) [] [])]++-- | Symbolic assert with a programmable continuation. Check that the given boolean condition is always true in the given path.+-- Otherwise symbolic simulation will transfer the failing model to the given continuation. The+-- continuation takes the @SMTConfig@, and a possible model: If it receives @Nothing@, then it means that the condition+-- fails for all assignments to inputs. Otherwise, it'll receive @Just@ a dictionary that maps the+-- input variables to the appropriate @CW@ values that exhibit the failure. Note that the continuation+-- has no option but to display the result in some fashion and call error, due to its restricted type.+sAssertCont :: Mergeable a => String -> (forall b. SMTConfig -> Maybe (M.Map String CW) -> b) -> SBool -> a -> a+sAssertCont msg cont t a+ | Just r <- unliteral t = if r then a else cont defaultSMTCfg Nothing+ | True = symbolicMerge False cond a (die ["SBV.error: Internal-error, cannot happen: Reached false branch in checked s-Assert."])+ where k = kindOf t+ cond = SBV k $ Right $ cache c+ die m = error $ intercalate "\n" $ ("Assertion failure: " ++ show msg) : m+ c st = do let pc = getPathCondition st+ chk = pc &&& bnot t+ mbModel <- isConditionSatisfiable st chk+ case mbModel of+ Just (r@(SatResult (Satisfiable cfg _))) -> cont cfg $ Just $ getModelDictionary r+ _ -> return trueSW+ -- SBV instance SymWord a => Mergeable (SBV a) where- -- 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- CWInteger i -> if i < 0 || i >= genericLength xs- then err- else xs `genericIndex` i- _ -> error "SBV.select: unsupported real valued select/index expression"- select xs err ind = SBV kElt $ Right $ cache r- where kInd = kindOf ind- kElt = kindOf err- r st = do sws <- mapM (sbvToSW st) xs- swe <- sbvToSW st err- if all (== swe) sws -- off-chance that all elts are the same- then return swe- else do idx <- getTableIndex st kInd kElt sws- swi <- sbvToSW st ind- 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:+ symbolicMerge force t a b+ | Just r <- unliteral t+ = if r then a else 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)+ 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.+ 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:+ 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+ 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.+ 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.+ 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.+ 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:+ 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)+ foo x y = ite (y .== 0) x (x+2) - In general, the following transformations should be done whenever possible:+ 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+ 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:+ 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)+ 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])+ 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])+ -- 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+ CWInteger i -> if i < 0 || i >= genericLength xs+ then err+ else xs `genericIndex` i+ _ -> error "SBV.select: unsupported real valued select/index expression"+ select xs err ind = SBV kElt $ Right $ cache r+ where kInd = kindOf ind+ kElt = kindOf err+ r st = do sws <- mapM (sbvToSW st) xs+ swe <- sbvToSW st err+ if all (== swe) sws -- off-chance that all elts are the same+ then return swe+ else do idx <- getTableIndex st kInd kElt sws+ swi <- sbvToSW st ind+ let len = length xs+ newExpr st kElt (SBVApp (LkUp (idx, kInd, kElt, len) swi swe) []) -- Unit instance Mergeable () where- symbolicMerge _ _ _ = ()+ symbolicMerge _ _ _ _ = () select _ _ _ = () -- Mergeable instances for List/Maybe/Either/Array are useful, but can@@ -1305,38 +1351,38 @@ -- Lists instance Mergeable a => Mergeable [a] where- symbolicMerge t xs ys- | lxs == lys = zipWith (symbolicMerge t) xs ys+ symbolicMerge f t xs ys+ | lxs == lys = zipWith (symbolicMerge f t) xs ys | True = error $ "SBV.Mergeable.List: No least-upper-bound for lists of differing size " ++ show (lxs, lys) where (lxs, lys) = (length xs, length ys) -- Maybe instance Mergeable a => Mergeable (Maybe a) where- symbolicMerge _ Nothing Nothing = Nothing- symbolicMerge t (Just a) (Just b) = Just $ symbolicMerge t a b- symbolicMerge _ a b = error $ "SBV.Mergeable.Maybe: No least-upper-bound for " ++ show (k a, k b)+ symbolicMerge _ _ Nothing Nothing = Nothing+ symbolicMerge f t (Just a) (Just b) = Just $ symbolicMerge f t a b+ symbolicMerge _ _ a b = error $ "SBV.Mergeable.Maybe: No least-upper-bound for " ++ show (k a, k b) where k Nothing = "Nothing" k _ = "Just" -- Either instance (Mergeable a, Mergeable b) => Mergeable (Either a b) where- symbolicMerge t (Left a) (Left b) = Left $ symbolicMerge t a b- symbolicMerge t (Right a) (Right b) = Right $ symbolicMerge t a b- symbolicMerge _ a b = error $ "SBV.Mergeable.Either: No least-upper-bound for " ++ show (k a, k b)+ symbolicMerge f t (Left a) (Left b) = Left $ symbolicMerge f t a b+ symbolicMerge f t (Right a) (Right b) = Right $ symbolicMerge f t a b+ symbolicMerge _ _ a b = error $ "SBV.Mergeable.Either: No least-upper-bound for " ++ show (k a, k b) where k (Left _) = "Left" k (Right _) = "Right" -- Arrays instance (Ix a, Mergeable b) => Mergeable (Array a b) where- symbolicMerge t a b- | ba == bb = listArray ba (zipWith (symbolicMerge t) (elems a) (elems b))+ symbolicMerge f t a b+ | ba == bb = listArray ba (zipWith (symbolicMerge f t) (elems a) (elems b)) | True = error $ "SBV.Mergeable.Array: No least-upper-bound for rangeSizes" ++ show (k ba, k bb) where [ba, bb] = map bounds [a, b] k = rangeSize -- Functions instance Mergeable b => Mergeable (a -> b) where- symbolicMerge t f g x = symbolicMerge t (f x) (g x)+ symbolicMerge f t g h x = symbolicMerge f t (g x) (h x) {- Following definition, while correct, is utterly inefficient. Since the application is delayed, this hangs on to the inner list and all the impending merges, even when ind is concrete. Thus, it's much better to@@ -1346,43 +1392,43 @@ -- 2-Tuple instance (Mergeable a, Mergeable b) => Mergeable (a, b) where- symbolicMerge t (i0, i1) (j0, j1) = (i i0 j0, i i1 j1)- where i a b = symbolicMerge t a b+ symbolicMerge f t (i0, i1) (j0, j1) = (i i0 j0, i i1 j1)+ where i a b = symbolicMerge f t a b select xs (err1, err2) ind = (select as err1 ind, select bs err2 ind) where (as, bs) = unzip xs -- 3-Tuple instance (Mergeable a, Mergeable b, Mergeable c) => Mergeable (a, b, c) where- symbolicMerge t (i0, i1, i2) (j0, j1, j2) = (i i0 j0, i i1 j1, i i2 j2)- where i a b = symbolicMerge t a b+ symbolicMerge f t (i0, i1, i2) (j0, j1, j2) = (i i0 j0, i i1 j1, i i2 j2)+ where i a b = symbolicMerge f t a b select xs (err1, err2, err3) ind = (select as err1 ind, select bs err2 ind, select cs err3 ind) where (as, bs, cs) = unzip3 xs -- 4-Tuple instance (Mergeable a, Mergeable b, Mergeable c, Mergeable d) => Mergeable (a, b, c, d) where- symbolicMerge t (i0, i1, i2, i3) (j0, j1, j2, j3) = (i i0 j0, i i1 j1, i i2 j2, i i3 j3)- where i a b = symbolicMerge t a b+ symbolicMerge f t (i0, i1, i2, i3) (j0, j1, j2, j3) = (i i0 j0, i i1 j1, i i2 j2, i i3 j3)+ where i a b = symbolicMerge f t a b select xs (err1, err2, err3, err4) ind = (select as err1 ind, select bs err2 ind, select cs err3 ind, select ds err4 ind) where (as, bs, cs, ds) = unzip4 xs -- 5-Tuple instance (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e) => Mergeable (a, b, c, d, e) where- symbolicMerge t (i0, i1, i2, i3, i4) (j0, j1, j2, j3, j4) = (i i0 j0, i i1 j1, i i2 j2, i i3 j3, i i4 j4)- where i a b = symbolicMerge t a b+ symbolicMerge f t (i0, i1, i2, i3, i4) (j0, j1, j2, j3, j4) = (i i0 j0, i i1 j1, i i2 j2, i i3 j3, i i4 j4)+ where i a b = symbolicMerge f t a b select xs (err1, err2, err3, err4, err5) ind = (select as err1 ind, select bs err2 ind, select cs err3 ind, select ds err4 ind, select es err5 ind) where (as, bs, cs, ds, es) = unzip5 xs -- 6-Tuple instance (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f) => Mergeable (a, b, c, d, e, f) where- symbolicMerge t (i0, i1, i2, i3, i4, i5) (j0, j1, j2, j3, j4, j5) = (i i0 j0, i i1 j1, i i2 j2, i i3 j3, i i4 j4, i i5 j5)- where i a b = symbolicMerge t a b+ symbolicMerge f t (i0, i1, i2, i3, i4, i5) (j0, j1, j2, j3, j4, j5) = (i i0 j0, i i1 j1, i i2 j2, i i3 j3, i i4 j4, i i5 j5)+ where i a b = symbolicMerge f t a b select xs (err1, err2, err3, err4, err5, err6) ind = (select as err1 ind, select bs err2 ind, select cs err3 ind, select ds err4 ind, select es err5 ind, select fs err6 ind) where (as, bs, cs, ds, es, fs) = unzip6 xs -- 7-Tuple instance (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f, Mergeable g) => Mergeable (a, b, c, d, e, f, g) where- symbolicMerge t (i0, i1, i2, i3, i4, i5, i6) (j0, j1, j2, j3, j4, j5, j6) = (i i0 j0, i i1 j1, i i2 j2, i i3 j3, i i4 j4, i i5 j5, i i6 j6)- where i a b = symbolicMerge t a b+ symbolicMerge f t (i0, i1, i2, i3, i4, i5, i6) (j0, j1, j2, j3, j4, j5, j6) = (i i0 j0, i i1 j1, i i2 j2, i i3 j3, i i4 j4, i i5 j5, i i6 j6)+ where i a b = symbolicMerge f t a b select xs (err1, err2, err3, err4, err5, err6, err7) ind = (select as err1 ind, select bs err2 ind, select cs err3 ind, select ds err4 ind, select es err5 ind, select fs err6 ind, select gs err7 ind) where (as, bs, cs, ds, es, fs, gs) = unzip7 xs @@ -1400,8 +1446,10 @@ bi <- uncacheAI b st newExpr st KBool (SBVApp (ArrEq ai bi) []) +-- When merging arrays; we'll ignore the force argument. This is arguably+-- the right thing to do as we've too many things and likely we want to keep it efficient. instance SymWord b => Mergeable (SArray a b) where- symbolicMerge = mergeArrays+ symbolicMerge _ = mergeArrays -- SFunArrays are only "Mergeable". Although a brute -- force equality can be defined, any non-toy instance@@ -1412,10 +1460,12 @@ readArray (SFunArray f) = f resetArray (SFunArray _) a = SFunArray $ const a writeArray (SFunArray f) a b = SFunArray (\a' -> ite (a .== a') b (f a'))- mergeArrays t (SFunArray f) (SFunArray g) = SFunArray (\x -> ite t (f x) (g x))+ mergeArrays t (SFunArray g) (SFunArray h) = SFunArray (\x -> ite t (g x) (h x)) +-- When merging arrays; we'll ignore the force argument. This is arguably+-- the right thing to do as we've too many things and likely we want to keep it efficient. instance SymWord b => Mergeable (SFunArray a b) where- symbolicMerge = mergeArrays+ symbolicMerge _ = mergeArrays -- | Uninterpreted constants and functions. An uninterpreted constant is -- a value that is indexed by its name. The only property the prover assumes
Data/SBV/BitVectors/STree.hs view
@@ -37,9 +37,9 @@ deriving Show instance (SymWord e, Mergeable (SBV e)) => Mergeable (STree i e) where- symbolicMerge b (SLeaf i) (SLeaf j) = SLeaf (symbolicMerge b i j)- symbolicMerge b (SBin l r) (SBin l' r') = SBin (symbolicMerge b l l') (symbolicMerge b r r')- symbolicMerge _ _ _ = error "SBV.STree.symbolicMerge: Impossible happened while merging states"+ symbolicMerge f b (SLeaf i) (SLeaf j) = SLeaf (symbolicMerge f b i j)+ symbolicMerge f b (SBin l r) (SBin l' r') = SBin (symbolicMerge f b l l') (symbolicMerge f b r r')+ symbolicMerge _ _ _ _ = error "SBV.STree.symbolicMerge: Impossible happened while merging states" -- | Reading a value. We bit-blast the index and descend down the full tree -- according to bit-values.
Data/SBV/Compilers/C.hs view
@@ -487,10 +487,21 @@ , (Equal, "=="), (NotEqual, "!="), (LessThan, "<"), (GreaterThan, ">"), (LessEq, "<="), (GreaterEq, ">=") , (And, "&"), (Or, "|"), (XOr, "^") ]+ uninterpret "squareRoot" as = let f = case kindOf (head opArgs) of+ KFloat -> text "sqrtf"+ KDouble -> text "sqrt"+ k -> die $ "squareRoot on unexpected kind: " ++ show k+ in f <> parens (fsep (punctuate comma as))+ uninterpret "fusedMA" as = let f = case kindOf (head opArgs) of+ KFloat -> text "fmaf"+ KDouble -> text "fma"+ k -> die $ "fusedMA on unexpected kind: " ++ show k+ in f <> parens (fsep (punctuate comma as))+ uninterpret s [] = text "/* Uninterpreted constant */" <+> text s+ uninterpret s as = text "/* Uninterpreted function */" <+> text s <> parens (fsep (punctuate comma as)) p (ArrRead _) _ = tbd "User specified arrays (ArrRead)" p (ArrEq _ _) _ = tbd "User specified arrays (ArrEq)"- p (Uninterpreted s) [] = text "/* Uninterpreted constant */" <+> text s- p (Uninterpreted s) as = text "/* Uninterpreted function */" <+> text s <> parens (fsep (punctuate comma as))+ p (Uninterpreted s) as = uninterpret s as p (Extract i j) [a] = extract i j (head opArgs) a p Join [a, b] = join (let (s1 : s2 : _) = opArgs in (s1, s2, a, b)) p (Rol i) [a] = rotate True i a (head opArgs)
Data/SBV/Examples/BitPrecise/Legato.hs view
@@ -81,10 +81,10 @@ -- | '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)- , flags = symbolicMerge b (flags m1) (flags m2)- }+ symbolicMerge f b m1 m2 = Mostek { memory = symbolicMerge f b (memory m1) (memory m2)+ , registers = symbolicMerge f b (registers m1) (registers m2)+ , flags = symbolicMerge f b (flags m1) (flags m2)+ } ------------------------------------------------------------------ -- * Low-level operations
Data/SBV/Examples/Puzzles/U2Bridge.hs view
@@ -94,13 +94,13 @@ -- | 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)- , lBono = symbolicMerge t (lBono s1) (lBono s2)- , lEdge = symbolicMerge t (lEdge s1) (lEdge s2)- , lAdam = symbolicMerge t (lAdam s1) (lAdam s2)- , lLarry = symbolicMerge t (lLarry s1) (lLarry s2)- }+ symbolicMerge f t s1 s2 = Status { time = symbolicMerge f t (time s1) (time s2)+ , flash = symbolicMerge f t (flash s1) (flash s2)+ , lBono = symbolicMerge f t (lBono s1) (lBono s2)+ , lEdge = symbolicMerge f t (lEdge s1) (lEdge s2)+ , lAdam = symbolicMerge f t (lAdam s1) (lAdam s2)+ , lLarry = symbolicMerge f t (lLarry s1) (lLarry s2)+ } -- | A puzzle move is modeled as a state-transformer type Move a = State Status a@@ -108,12 +108,12 @@ -- | 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+ symbolicMerge f t a b = do s <- get let (ar, s1) = runState a s (br, s2) = runState b s- put $ symbolicMerge t s1 s2- return $ symbolicMerge t ar br+ put $ symbolicMerge f t s1 s2+ return $ symbolicMerge f t ar br -- | Read the state via an accessor function peek :: (Status -> a) -> Move a
Data/SBV/Provers/Boolector.hs view
@@ -79,7 +79,7 @@ -- Boolector outputs in a non-parenthesized way; and also puts x's for don't care bits: cvt :: String -> String cvt s = case words s of- [var, val] -> "((" ++ var ++ " #b" ++ map tr val ++ "))"- _ -> s -- good-luck..+ [_, val, var] -> "((" ++ var ++ " #b" ++ map tr val ++ "))"+ _ -> s -- good-luck.. where tr 'x' = '0' tr x = x
Data/SBV/Provers/Prover.hs view
@@ -27,12 +27,13 @@ , boolector, cvc4, yices, z3, mathSAT, defaultSMTCfg , compileToSMTLib, generateSMTBenchmarks , isSBranchFeasibleInState+ , isConditionSatisfiable ) where import Control.Monad (when, unless) import Control.Monad.Trans (liftIO) import Data.List (intercalate)-import Data.Maybe (mapMaybe, fromMaybe)+import Data.Maybe (mapMaybe, fromMaybe, isJust) import System.FilePath (addExtension, splitExtension) import System.Time (getClockTime) import System.IO.Unsafe (unsafeInterleaveIO)@@ -443,17 +444,35 @@ 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+ check <- internalSATCheck cfg st cond ("sBranch: Checking " ++ show branch ++ " feasibility") 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++-- | Check if a boolean condition is satisfiable in the current state. If so, it returns such a satisfying assignment+isConditionSatisfiable :: State -> SBool -> IO (Maybe SatResult)+isConditionSatisfiable st cond = do+ let cfg = fromMaybe defaultSMTCfg (getSBranchRunConfig st)+ msg = when (verbose cfg) . putStrLn . ("** " ++)+ check <- internalSATCheck cfg st cond "sAssert: Checking satisfiability"+ res <- case check of+ r@(SatResult (Satisfiable{})) -> return $ Just r+ SatResult (Unsatisfiable _) -> return Nothing+ _ -> error $ "sAssert: Unexpected external result: " ++ show check+ msg $ "sAssert: Conclusion: " ++ if isJust res then "Satisfiable" else "Unsatisfiable"+ return res++-- | Check the boolean SAT of an internal condition in the current execution state+internalSATCheck :: SMTConfig -> State -> SBool -> String -> IO SatResult+internalSATCheck cfg st cond msg = do+ 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+ runProofOn cvt cfg True [] pgm >>= callSolver True msg SatResult cfg
Data/SBV/SMT/SMTLib1.hs view
@@ -210,11 +210,14 @@ cvtExp (SBVApp (Uninterpreted nm) []) = "uninterpreted_" ++ nm cvtExp (SBVApp (Uninterpreted nm) args) = "(uninterpreted_" ++ nm ++ " " ++ unwords (map show args) ++ ")" cvtExp inp@(SBVApp op args)+ | allBools, Just f <- lookup op boolComps+ = f (map show args) | Just f <- lookup op smtOpTable- = f (any hasSign args) (all isBoolean args) (map show args)+ = f (any hasSign args) allBools (map show args) | True = error $ "SBV.SMT.SMTLib1.cvtExp: impossible happened; can't translate: " ++ show inp- where lift2 o _ _ [x, y] = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")"+ where allBools = all isBoolean args+ lift2 o _ _ [x, y] = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")" lift2 o _ _ sbvs = error $ "SBV.SMTLib1.cvtExp.lift2: Unexpected arguments: " ++ show (o, sbvs) lift2S oU oS sgn isB sbvs | sgn@@ -240,6 +243,18 @@ | True = "(= " ++ lift2 "bvcomp" sgn isB sbvs ++ " bv1[1])" neq sgn isB sbvs = "(not " ++ eq sgn isB sbvs ++ ")"+ -- Boolean comparisons.. SMTLib's bool type doesn't do comparisons, but Haskell does.. Sigh+ boolComps = [ (LessThan, blt)+ , (GreaterThan, blt . swp)+ , (LessEq, blq)+ , (GreaterEq, blq . swp)+ ]+ where blt [x, y] = "(and (not " ++ x ++ ") " ++ y ++ ")"+ blt xs = error $ "SBV.SMT.SMTLib1.boolComps.blt: Impossible happened, incorrect arity (expected 2): " ++ show xs+ blq [x, y] = "(or (not " ++ x ++ ") " ++ y ++ ")"+ blq xs = error $ "SBV.SMT.SMTLib1.boolComps.blq: Impossible happened, incorrect arity (expected 2): " ++ show xs+ swp [x, y] = [y, x]+ swp xs = error $ "SBV.SMT.SMTLib1.boolComps.swp: Impossible happened, incorrect arity (expected 2): " ++ show xs smtOpTable = [ (Plus, lift2 "bvadd") , (Minus, lift2 "bvsub") , (Times, lift2 "bvmul")
Data/SBV/SMT/SMTLib2.hs view
@@ -442,6 +442,8 @@ sh inp@(SBVApp op args) | intOp, Just f <- lookup op smtOpIntTable = f True (map ssw args)+ | boolOp, Just f <- lookup op boolComps+ = f (map ssw args) | bvOp, Just f <- lookup op smtOpBVTable = f (any hasSign args) (map ssw args) | realOp, Just f <- lookup op smtOpRealTable@@ -464,6 +466,18 @@ , (LessEq, lift2S "bvule" "bvsle") , (GreaterEq, lift2S "bvuge" "bvsge") ]+ -- Boolean comparisons.. SMTLib's bool type doesn't do comparisons, but Haskell does.. Sigh+ boolComps = [ (LessThan, blt)+ , (GreaterThan, blt . swp)+ , (LessEq, blq)+ , (GreaterEq, blq . swp)+ ]+ where blt [x, y] = "(and (not " ++ x ++ ") " ++ y ++ ")"+ blt xs = error $ "SBV.SMT.SMTLib2.boolComps.blt: Impossible happened, incorrect arity (expected 2): " ++ show xs+ blq [x, y] = "(or (not " ++ x ++ ") " ++ y ++ ")"+ blq xs = error $ "SBV.SMT.SMTLib2.boolComps.blq: Impossible happened, incorrect arity (expected 2): " ++ show xs+ swp [x, y] = [y, x]+ swp xs = error $ "SBV.SMT.SMTLib2.boolComps.swp: Impossible happened, incorrect arity (expected 2): " ++ show xs smtOpRealTable = smtIntRealShared ++ [ (Quot, lift2WM "/") ]
+ SBVUnitTest/GoldFiles/iteTest1.gold view
@@ -0,0 +1,13 @@+INPUTS+ s0 :: SWord8, aliasing "x"+CONSTANTS+ s_2 = False+ s_1 = True+TABLES+ARRAYS+UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS+AXIOMS+DEFINE+CONSTRAINTS+OUTPUTS
+ SBVUnitTest/GoldFiles/iteTest2.gold view
@@ -0,0 +1,13 @@+INPUTS+ s0 :: SWord8, aliasing "x"+CONSTANTS+ s_2 = False+ s_1 = True+TABLES+ARRAYS+UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS+AXIOMS+DEFINE+CONSTRAINTS+OUTPUTS
+ SBVUnitTest/GoldFiles/iteTest3.gold view
@@ -0,0 +1,13 @@+INPUTS+ s0 :: SWord8, aliasing "x"+CONSTANTS+ s_2 = False+ s_1 = True+TABLES+ARRAYS+UNINTERPRETED CONSTANTS+USER GIVEN CODE SEGMENTS+AXIOMS+DEFINE+CONSTRAINTS+OUTPUTS
SBVUnitTest/SBVBasicTests.hs view
@@ -47,18 +47,25 @@ run :: FilePath -> IO () run gd = do putStrLn $ "*** Starting SBV basic tests..\n*** Gold files at: " ++ show gd checkGoldDir gd- (cts, _) <- runTestText (PutText put ()) $ TestList $ map (mkTst . snd) testCollection- hPutStrLn stderr $ showCounts cts- decide cts- where mkTst (SBVTestSuite f) = f $ generateGoldCheck gd False- put s _ st = length s `seq` return st+ let collections = map (mkTst . snd) testCollection+ cNames = map fst testCollection+ putStrLn $ "*** Running " ++ show (length collections) ++ " test categories."+ runEach 1 (zip cNames collections)+ where runEach :: Int -> [(String, Test)] -> IO ()+ runEach _ [] = exitSuccess+ runEach i ((n, tc):tcs) = do putStrLn $ "Starting category: " ++ show n+ (cts, _) <- runTestText (PutText put ()) tc+ hPutStrLn stderr $ showCounts cts+ decide n cts+ runEach (i+1) tcs+ mkTst (SBVTestSuite f) = f $ generateGoldCheck gd False+ put _ _ = return -decide :: Counts -> IO ()-decide (Counts c t e f) = do+decide :: String -> Counts -> IO ()+decide cat (Counts c t e f) = do when (c /= t) $ putStrLn $ "*** Not all test cases were tried. (Only tested " ++ show t ++ " of " ++ show c ++ ")" when (e /= 0) $ putStrLn $ "*** " ++ show e ++ " (of " ++ show c ++ ") test cases in error." when (f /= 0) $ putStrLn $ "*** " ++ show f ++ " (of " ++ show c ++ ") test cases failed." if c == t && e == 0 && f == 0- then do putStrLn $ "All " ++ show c ++ " test cases successfully passed."- exitSuccess+ then putStrLn $ "All " ++ show c ++ " test cases in category " ++ show cat ++ " successfully passed." else exitWith $ ExitFailure 2
SBVUnitTest/SBVTestCollection.hs view
@@ -20,8 +20,9 @@ import qualified TestSuite.Basics.BasicTests as T02_03(testSuite) import qualified TestSuite.Basics.Higher as T02_04(testSuite) import qualified TestSuite.Basics.Index as T02_05(testSuite)-import qualified TestSuite.Basics.ProofTests as T02_06(testSuite)-import qualified TestSuite.Basics.QRem as T02_07(testSuite)+import qualified TestSuite.Basics.IteTest as T02_06(testSuite)+import qualified TestSuite.Basics.ProofTests as T02_07(testSuite)+import qualified TestSuite.Basics.QRem as T02_08(testSuite) import qualified TestSuite.BitPrecise.BitTricks as T03_01(testSuite) import qualified TestSuite.BitPrecise.Legato as T03_02(testSuite) import qualified TestSuite.BitPrecise.MergeSort as T03_03(testSuite)@@ -70,8 +71,9 @@ , ("basic", False, T02_03.testSuite) , ("higher", True, T02_04.testSuite) , ("index", True, T02_05.testSuite)- , ("proof", True, T02_06.testSuite)- , ("qrem", True, T02_07.testSuite)+ , ("ite", True, T02_06.testSuite)+ , ("proof", True, T02_07.testSuite)+ , ("qrem", True, T02_08.testSuite) , ("bitTricks", True, T03_01.testSuite) , ("legato", False, T03_02.testSuite) , ("mergeSort", False, T03_03.testSuite)
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String-buildTime = "Fri Jul 11 22:53:51 PDT 2014"+buildTime = "Tue Nov 18 18:03:52 PST 2014"
+ SBVUnitTest/TestSuite/Basics/IteTest.hs view
@@ -0,0 +1,41 @@+-----------------------------------------------------------------------------+-- |+-- Module : TestSuite.Basics.IteTest+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Test various incarnations of ite/iteLazy/sBranch+-----------------------------------------------------------------------------++module TestSuite.Basics.IteTest(testSuite) where++import Data.SBV+import Data.SBV.Internals++import SBVTest++chk1 :: (SBool -> SBool -> SBool -> SBool) -> SWord8 -> SBool+chk1 cond x = cond (x .== x) true undefined++chk2 :: (SBool -> [SBool] -> [SBool] -> [SBool]) -> SWord8 -> SBool+chk2 cond x = head (cond (x .== x) [true] [undefined])++chk3 :: (SBool -> (SBool, SBool) -> (SBool, SBool) -> (SBool, SBool)) -> SWord8 -> SBool+chk3 cond x = fst (cond (x .== x) (true, undefined::SBool) (undefined, undefined))++-- Test suite+testSuite :: SBVTestSuite+testSuite = mkTestSuite $ \goldCheck -> test [+ "ite-1" ~: rs (chk1 ite) `goldCheck` "iteTest1.gold"+ , "ite-2" ~: rs (chk2 ite) `goldCheck` "iteTest2.gold"+ , "ite-3" ~: rs (chk3 ite) `goldCheck` "iteTest3.gold"+ , "ite-4" ~: assert =<< isThm (chk1 iteLazy)+ , "ite-5" ~: assert =<< isThm (chk2 iteLazy)+ , "ite-6" ~: assert =<< isThm (chk3 iteLazy)+ , "ite-7" ~: assert =<< isThm (chk1 sBranch)+ , "ite-8" ~: assert =<< isThm (chk2 sBranch)+ , "ite-9" ~: assert =<< isThm (chk3 sBranch)+ ]+ where rs f = runSymbolic (True, Nothing) $ forAll ["x"] f
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 3.1+Version: 3.2 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@@ -150,6 +150,7 @@ , TestSuite.Basics.BasicTests , TestSuite.Basics.Higher , TestSuite.Basics.Index+ , TestSuite.Basics.IteTest , TestSuite.Basics.ProofTests , TestSuite.Basics.QRem , TestSuite.BitPrecise.BitTricks@@ -191,7 +192,7 @@ Test-Suite SBVBasicTests type : exitcode-stdio-1.0 default-language: Haskell2010- ghc-options : -Wall+ ghc-options : -Wall -with-rtsopts=-K64m Build-depends : base >= 4 && < 5 , HUnit, directory, filepath, syb, sbv Hs-Source-Dirs : SBVUnitTest